Sync harness to the no-hint proof-synthesis run; add results + reproduce docs - #2
Open
oliversssf2 wants to merge 2 commits into
Open
Sync harness to the no-hint proof-synthesis run; add results + reproduce docs#2oliversssf2 wants to merge 2 commits into
oliversssf2 wants to merge 2 commits into
Conversation
…EADME Bring the public tool up to the Montgomery-era harness state that the no-hint whole-crate proof-synthesis run used, so the code and the gate suite match the reported result: - run.py / run_layer.py / launch.sh / admit.py / lib / skills synced to that state; the full integrity-gate suite is now public: git-recovery, frozen-edit, and forbidden-construct join the existing spec-drift, axiom-drift, tooling-drift, sibling-verify, and admit-count gates. - add run_proofonly_layers.sh (the whole-crate proof-only sweep runner) and the check_false_contract skill, with tests. - peel machinery is intentionally out of scope for this update. README: - add a Results section (no-hint whole-crate synthesis on curve25519-dalek: 1,430/1,433 non-axiom obligations closed, 3 residual shared with the human reference, 2,493 verified / 0 errors, $748.02 recorded API cost as a lower bound with the excluded re-prove pass disclosed); - add a Reproducing-and-auditing section pinning the model, Verus rev, start and finished trees, and the two-check (correctness + coverage) audit; - expand Integrity gates from three to the full suite; drop the stale "~1k LOC" framing (the repo's own CLAUDE.md already notes the harness grew past that). Example paths scrubbed to /path/to/... . py_compile clean on all Python files; the toolchain-free unit tests pass. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
lib/admits._AXIOM_FN_RE (and the axiom-name variant) matched pub/broadcast/ open/closed before `proof fn axiom_*`, but not `pub(crate)`. Two `pub(crate) proof fn axiom_xdbl/xadd_projective_correct` in the curve25519-dalek montgomery lemmas were therefore miscounted as real obligations, so the harness/`admit_inventory` residual read 2 higher than the census-accurate count. With the fix, a whole-crate census of the no-hint result tree reads the correct 3 non-axiom gaps (matching the reported result), and `admit_inventory` on the montgomery lemmas reports 0 non-axiom / 9 axiom. No effect on any proof: the pre-fix counter only ever over-counted axioms as actionable (conservative for the COMPLETE gate). tests/test_admits_pubcrate.py pins it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this does
Brings the public tool up to the harness state the no-hint whole-crate proof-synthesis run used (the Montgomery-era dev state), and documents the result.
Code
run.py/run_layer.py/launch.sh/admit.py/lib/skillssynced to that state; the full integrity-gate suite is now public:git-recovery,frozen-edit, andforbidden-constructjoin the existing spec-drift, axiom-drift, tooling-drift, sibling-verify, and admit-count gates.run_proofonly_layers.sh(the whole-crate proof-only sweep runner) andskills/check_false_contract.py, with tests.pub(crate) proof fn axiom_*were miscounted as real obligations (the regex acceptedpub/open/… but notpub(crate)), so the residual read 2 high. Fixed + regression test. No effect on any proof — the miscount only ever over-counted axioms as actionable, which is conservative for theCOMPLETEgate.README
Verified (against Verus
0.2026.01.14.88f7396)cargo verus= 2,493 verified, 0 errors; non-axiom census = 3 — matching the reported result.Review notes
CLAUDE.mdalready notes the harness grew past ~1k). Reword to taste.nohints-proventrees and per-round records as "released with the paper's artifact." That artifact (and/or a publiccurve25519-dalekfork) has to be published for the steps to be fully followable — this repo ships the tool, not those trees.AGENTS.md,demo/, internaldocs/*,results/, spec-gen launchers, the peel manifests; example paths scrubbed to/path/to/….pub(crate)counter fix should probably also land in the dev harness.🤖 Generated with Claude Code