Skip to content

ACGN v2.13

Choose a tag to compare

View all tags
@AlexandervonWu AlexandervonWu released this 07 Sep 20:50
· 9 commits to aislop since this release
v2.13
892e001

ACGN v2.13

An assurance-only continuation of v2.12, covering the next five obligations:

  • P2-06: exact flat element/result typing through a shared substitution.
  • A2-01: ordered dependent JOIN/ARROW sequence construction and replay.
  • A2-02: chain length and operand multiplicity preservation.
  • P1-08: arbitrary-arity CALL validation without neighboring-visit fallback.
  • P1-05: source argument order through the retained CALL boundaries.

Verified Evidence

The frozen five-claim package passed two clean builds with 1,026 identical artifacts per build, 48 general Lean theorems, 2,636 generated propositions, and all 21 required rejection controls per build. The three new Java tests execute 66,872 assertions per build; 33 runner and seven encoding unit tests pass. Independent bounded reviews and their repaired findings are retained in docs/obligation-repair/next-five/.

Input root: c627da30a64e66506a1dcb777fd94e9dcbee7e2b5a64ad7bcb7e37557d360da0.

A fresh replay from the extracted release bundle, without a Git checkout or a default elan toolchain, also passed both builds. All 1,026 artifact hashes per build matched the repository run.

The full bounded Java and standalone producer/verifier harnesses pass. The matrix now has 97 ready requirements and 123 diagnostics, compared with 92 and 128 in v2.12. These are proved models with bounded direct conformance, not whole-parser or whole-JVM refinement. The global matrix remains incomplete.

The standard certificate census remains 1 VERIFIED, 2 UNCHECKABLE, 0 REJECTED. Certificate coverage is bounded and fixture-scoped. Parsed local chain observations are distinct from the separate TEST_ONLY FULL-verifier fixtures; unsupported parsed exports are not relabeled certified.

Provenance

  • Final packaging/tag commit: 892e001ee9f81fc5cf9ac2f4984c4b8be474e18c.
  • Exact-commit CI: https://github.com/AlexandervonWu/ACGN/actions/runs/34159720543
  • Result-producing source commit: fbd9b1497a9036c55780da777f56581bc1c6bcec.
  • Publication run: df4d8d4c-6265-4fe7-88d5-3aceee60398b.
  • Production Java, experimental trees, certificate authority, and the archived experiment JAR are unchanged. All 5,808 manifest-bound publication outputs verify.
  • Existing reward results and correlations remain those of the v2.11 run with pool size 100; no experiments were rerun for this assurance release.

Reviewers using the full repository must run git lfs pull before checking the large empirical JSON files.

Reproduction

The source/proof bundle contains the bounded runners and dependencies, not the corpus/results or frontend. From the extracted bundle, with Java 17, Python 3, and installed Lean 4.33.0:

python3 -B scripts/run_next_obligation_repairs.py /tmp/acgn-v213-next-five

Use a fresh output directory. The new runner creates local deterministic TEST_ONLY Git provenance for its isolated verification snapshots, not publication authority. The two older container/refinement runners still require a Git checkout, as documented.

Assets

acgn-experiments.jar is the existing, unrecompiled v2.11 experiment JAR (2,292,989 bytes). acgn-v2.13-assurance.tar.gz is the tagged assurance source and evidence package (58,103,083 bytes). SHA256SUMS binds both assets.

361b33ef56f6ccb1089a7a6fdda2a92bf621e501166c5a1c73330a0cc1686807  acgn-experiments.jar
e2ea9ab0203f5f509c90f098cdaf32653f27cbe2f839af85c79e67e1a70f7b5c  acgn-v2.13-assurance.tar.gz
bebd1d17aaa2de1dd423ac4a9f76e26e7383b552eb065c88a72ed6700ac18549  SHA256SUMS
Assets 5
Loading