ACGN v2.14
ACGN v2.14
Five more bounded assurance obligations are repaired: P1-06, P1-09,
P1-16, P2-19, and A2-04. These cover independent CALL arity/authority,
executable occurrence nonreuse, ordered and nested CALL representation,
complete registry/profile binding, and arbitrary-length guarded relational JOIN.
Evidence
- Five frozen claims VERIFIED in two clean builds, with 1,053 identical artifacts each.
- 74 new general Lean theorems, 166 imported theorem audits, and 1,414 generated replay propositions.
- 10,628 Java observations and 18,800 assertions across the three new tests.
- All 28 Lean negative controls and 26 source-mutation controls reject for their registered reasons in each build.
- 33 runner and 34 area encoder tests pass; independent bounded reviews and failed-candidate records are retained.
- The full matrix remains INCOMPLETE: 102 ready requirements and 118 diagnostics.
- Certificate coverage remains bounded and fixture-scoped: 1 verified, 2 uncheckable, 0 rejected.
These results are general model proofs plus bounded direct conformance under
an explicit trusted computing base, not universal Java/parser refinement or
corpus-wide certification. Original requirement statements/hashes are unchanged.
P1-19's independent source-occurrence authority and A-01's complete typed
contract registry remain open.
Provenance And Assets
- Packaging/tag commit:
91825cff2b7c4b460cb5bc6160bf2df4ff95b089. - Exact-commit Actions: https://github.com/AlexandervonWu/ACGN/actions/runs/34247620652
- Frozen assurance input root:
4d63586625ff6c0a4f5bc923ed19ecbb377b88d2c768ea504a39b965f9393003. - Result-producing source:
fbd9b1497a9036c55780da777f56581bc1c6bcec. - Publication run:
df4d8d4c-6265-4fe7-88d5-3aceee60398b. acgn-experiments.jaris the existing, unrecompiled v2.11 JAR: 2,292,989 bytes; SHA-256361b33ef56f6ccb1089a7a6fdda2a92bf621e501166c5a1c73330a0cc1686807.acgn-v2.14-assurance.tar.gzpackages this commit's source, local libraries, proofs, bounded runners, documentation, and evidence. It excludes the corpus, result trees, and frontend.SHA256SUMSbinds both attached assets. Verify it before use.
Production canonicalization, repair metrics, certificate semantics/authority,
the prior assurance packages, and all empirical trees remain unchanged. The
snapshot verifier checks the same 5,808 files. Rewards and correlations remain
those of the v2.11 pool-100 run; no experiments were rerun for v2.14.
Reviewers using the full repository must run git lfs pull before reading
the large experimental JSON files.
Reproduce
From the checkout or extracted assurance archive, with Java 17, Python 3,
and locally installed Lean 4.33.0:
python3 -B scripts/run_third_obligation_repairs.py /tmp/acgn-v214-third-five
python3 -B scripts/report_obligation_repairs.py --output /tmp/acgn-v214-obligationsUse fresh output directories outside the source tree. The third-five runner
creates two isolated builds, including deterministic TEST_ONLY Git provenance;
it supports an extracted archive without .git. The older container and
Java-Lean refinement runners still require a Git checkout.
The attached assurance archive was extracted and rerun locally without .git:
both clean builds VERIFIED all five claims at the same frozen input root.
Next Five Candidates
- P2-20: recursive flattening iff exact typed associativity evidence exists.
- A2-07: independent exact leaf type/view proofs and complete field controls.
- A2-11: complete dependent-chain index reconstruction across writer/verifier.
- P2-18: exact permutation, quotient, splice, and endpoint witness indices.
- P3-03: profile serialization and independent five-field fingerprint replay.
These are proposed work, not additional repairs completed in this release.
See docs/obligation-repair/third-five/README.md and
docs/obligation-repair/next-candidates-v2.14.md for evidence and boundaries.