Skip to content

ACGN v2.15

Choose a tag to compare

View all tags
@AlexandervonWu AlexandervonWu released this 09 Sep 02:56
· 4 commits to aislop since this release
v2.15
5eba7ca

ACGN v2.15

Closes the five bounded correspondence repairs P2-20, A2-07, A2-11, P2-18 and
P3-03. The work repaired three concrete certificate production/replay defects:
source-profile version drift, recursive splice ordering, and missing exact
intermediate types in dependent-chain exports. No new rewrite family is added.

The five-claim closure is VERIFIED under its declared trust boundary: two clean
builds, 1,076 identical artifacts per build, 66 general Lean theorems, 9,128
replay propositions/blocks, and all registered rejection checks passing.
The assurance archive also reproduces the same closure after extraction.
The broader Java suite includes 45 test entry points. Certificate census:
1 verified, 2 uncheckable, 0 rejected, with distinct parsed-source PAIR hashes
and unchanged fixture-scoped authority. This is bounded evidence, not complete
Java/parser refinement; the full matrix retains 111 diagnostics (107 ready requirements).

Fresh Full-Corpus Run

All four stages were rerun before publication, strictly serially, with 16 workers,
an 8 GiB heap, reward pool 100, and one unchanged experiment JAR:

  • 66,080 files; 61,598 eligible successes; 4,482 AST-identical skips.
  • 42,386 incorrect predicates ranked and rewarded; no parse, ranking or reward failures.
  • Zero incorrect nearest-truth zeroes in both Fast Rewrite and Certificate-Integrated IR.
  • Seven full-corpus ablation arms, zero failures or incorrect merges.
  • 4,088 claimed-equal pairs checked with bounded Alloy, no counterexamples/errors.
  • 5,500/5,500 capabilities captured by slotted, Fast Rewrite and Certificate-Integrated IR.
  • Six temporal capability solver checks remain explicitly inconclusive.

The 5,808 imported stage files pass their manifest hashes. Distance and equality
headline results are reproduced; runtime/memory have been remeasured. Rewards
are available for this run and remain finite sampled evidence, not semantic proofs.

Exact Provenance

  • Result-producing source: 8ad5fead39b687d2cadc79b01ac27743c1ece990 (clean).
  • Publication run: db9f89bf-0965-4d74-8080-d9191d5f1aec.
  • Packaging/tag commit: 5eba7ca15e29466e9ba813efb50c908f79f07cd9.
  • Closure: fourth-five-v1-58c1aae07b2d37dc.
  • Closure input root: 58c1aae07b2d37dc98459c7c9989cb942b0845ec1fce579b8ca19836b16a133b.
  • Exact-commit Actions.
  • Repair, evidence and limits.
  • Publication provenance.

Reviewers must run git lfs pull in the full checkout. The attached experiment
JAR is copied unchanged from the new completed run, not rebuilt from the packaging
commit. Earlier archived JARs/manifests remain unchanged. The assurance archive
contains source, libraries, proofs, runners and retained evidence; use the full
checkout for corpus, empirical result trees and frontend.

Verify both attached assets with sha256sum -c SHA256SUMS.

  • acgn-experiments.jar: 2,540,041 bytes; SHA-256 a053e40e64faa2ecffb0f4999b57aa661eae51933d6daf93a95d973144a71abf.
  • acgn-v2.15-assurance.tar.gz: SHA-256 358f34e10fd3624015ebff5fa5381fdd630aeeb7cfc347f325b280d12f14c3c0.
Assets 5
Loading