Skip to content

ACGN v2.12

Choose a tag to compare

View all tags
@AlexandervonWu AlexandervonWu released this 07 Sep 19:34
· 10 commits to aislop since this release
v2.12
59045ea

ACGN v2.12

An assurance and reproducibility update. This release does not change the
production canonicalizer, distance metric, rewarder, or certificate semantics,
and does not claim a new experimental run.

New assurance work

  • Finite Java-to-Lean container replay and compiler-extracted Boolean
    smart-construction correspondence, each with explicit scope and retained
    historical input hashes.
  • Five bounded ledger gaps repaired: P2-02 (nominal policy fields), A2-06
    (JOIN interior guard), P2-05 (single root port), P1-10 (zero-argument CALL),
    and P5-15 (built-in identity and empty cardinality).
  • Two identical clean builds of the five-claim package: 77 general and 93
    generated Lean theorems, 370,365 assertions in the five new Java tests, and
    17 required rejection controls per build.
  • Explicit A-01 rejection when authoritative decomposition evidence is
    missing. The full ledger remains INCOMPLETE: 92 ready requirements and
    128 diagnostics (127 original diagnostics plus the exposed A-01 blocker).

The full bounded Java suite and standalone producer/verifier harness passed.
Certificate coverage remains bounded and fixture-scoped: 1 VERIFIED,
2 UNCHECKABLE, 0 REJECTED. These results do not establish whole-parser,
whole-JVM, or whole-corpus semantic verification.

Provenance

  • Final packaging/tag commit: 59045ead958b5f8397100c39ab68557a3cb05399
  • Exact-commit Actions: https://github.com/AlexandervonWu/ACGN/actions/runs/34155260001
  • Five-claim closure input root:
    1e34a74d3b5be4e39af665571123907e27950b24dabd43a4b63d5594752c5825
  • Unchanged result-producing source commit:
    fbd9b1497a9036c55780da777f56581bc1c6bcec
  • Unchanged clean publication run:
    df4d8d4c-6265-4fe7-88d5-3aceee60398b

All 5,808 manifest-bound imported files verified unchanged. The dataset and
empirical result trees are unchanged from v2.11. Reviewers must run
git lfs pull when using the full repository. Rewards and correlations remain
those of the v2.11 clean run with pool size 100; they were not recomputed here.

Assets

  • acgn-experiments.jar: the unrecompiled, byte-identical archived v2.11 JAR,
    2,292,989 bytes; SHA-256
    361b33ef56f6ccb1089a7a6fdda2a92bf621e501166c5a1c73330a0cc1686807.
  • acgn-v2.12-assurance.tar.gz: tagged source, dependencies, proofs,
    bounded-check scripts, and evidence; 50,772,717 bytes; SHA-256
    e5a5880f98248acd67616e5c62af41c6ce48ca324bfcc26f8ae027d6d61ae938.
    This is an assurance package, excluding the corpus/results and frontend.
    Its extracted files match the verified five-claim input manifest exactly.
  • SHA256SUMS: checksums for both assets; SHA-256
    f6aa68717fba3d1b04a0c77819306de600c486ddd5504f7546a2bfda3b4e4dcf.

Publication CI caught an isolated-working-directory toolchain-selection bug
in the new proof runner. The release fixes it by explicitly selecting and
checking Lean 4.33.0 in both proof directories, retains the earlier evidence
as superseded, and includes a fresh two-build replay. No tag was published
from either failed or cancelled candidate. The two older refinement/container
runners require a Git checkout for Git HEAD provenance; the release guide
distinguishes those commands from the archive-compatible five-claim runner.

See the release guide
and bounded repair report
for reproduction commands, proof boundaries, and retained evidence.

Recommended next obligations

All of these remain PARTIAL/DIRECT; this release does not mark them proved.

  1. P2-06: exact flat element/result type equality through instantiation and
    substitution, reusing the single-root-port extractor.
  2. A2-01: general left-to-right JOIN/ARROW chain construction and replay.
  3. A2-02: general chain length and duplicate-occurrence count preservation,
    sharing A2-01's traversal model but retaining a separate obligation.
  4. P1-08: executable CALL validation at arbitrary arity, including proof
    that the CALL path cannot use another visit as a fallback.
  5. P1-05: argument-order preservation from parser occurrences through
    retained certification-source IR and ordered certified endpoints.

P2-06 is the recommended first target. A-01 remains a specification blocker:
its missing authoritative parent contracts cannot be supplied by more examples
or an otherwise well-formed theorem-name registry.

Assets 5
Loading