diff --git a/ATTESTATION-RUNBOOK.md b/ATTESTATION-RUNBOOK.md index 2fe3311..508c29e 100644 --- a/ATTESTATION-RUNBOOK.md +++ b/ATTESTATION-RUNBOOK.md @@ -52,15 +52,17 @@ Agent Appendix at the end. Every step ends in a mechanical check. ## PHASE A — do now / while waiting for the IACR decision -### A1. Reviewer confirmations of round 4 -Deliver the round-4 kit (already on SD) to both reviewers. Required -outcome, in their words: GPT-5.6's conditional approval stands with the -round-4 evidence (its conditions 2 and 3 — recorded hashes, fresh -button run by exit code — are satisfied by `CORPUS-MANIFEST.sha256` and -`check-transcript.txt` in the kit); the Claude reviewer confirms F1* -was absorbed faithfully (gap 14 + lied-size family + banner scoping). -**Check:** two written reviews on the SD card saying so. If either -finds anything new: run another revision round first; do not proceed. +### A1. Reviewer confirmations of round 4 — **DONE (2026-07-15)** +Both round-4 reviews are on the SD card. Claude reviewer: "Nothing +blocks the freeze… no remaining findings on the corpus itself" +(re-executed everything hostile, incl. deliberately breaking the +lied-size tripwires — both broke the run as designed — and the first +paper↔Lean cross-check, faithful). GPT-5.6: "Approve after minor +documentation fixes" for an attestation SCOPED TO THE MECHANIZED MODEL +(see the B2 wording requirement below); its principal finding (the +deployment refinement invariant is unmechanized) is now KNOWN-GAPS +gap 15. The round-5 housekeeping freeze addressed both reviewers' +remaining documentation items. ### A2. The author's read (the one step only the operator can do) Read, in this order, against the paper's §6 and §10: @@ -173,8 +175,24 @@ GREEN`, `exit=0`. Any other outcome: STOP (iron rule 4). Fresh clone of `lean-transparency-log`, driver runs once, produces: `entries/000012.json`, updated `latest-sth.json` (tree_size 13), one new line in `sth-history.jsonl`, one new receipt. + +**REQUIRED ATTESTATION SCOPE (round-4 GPT §11 — this wording is a gate +condition, not a suggestion).** The leaf's human-readable claim text +must be scoped to the mechanized model, in substance: + +> This corpus kernel-checks the listed theorems about the mechanized +> recursive accumulator model. Correspondence with the deployed +> inclusion verifier is supported by finite differential testing over +> the pinned families. The deployed consistency verifier is not +> extensionally equal to the model; applying the mechanized soundness +> result to the deployed consumer flow additionally relies on an +> unmechanized authentic-size/root invariant (KNOWN-GAPS 14/15). + +The leaf must NOT say or imply "the deployed verifier is formally +verified." **Check:** `git status` shows exactly those four paths changed/added, -nothing else. `pacta witness-audit` on the clone exits 0. +nothing else. The claim text above appears in the attestation. +`pacta witness-audit` on the clone exits 0. ### B3. Consumer's-eye check before publishing From a DIFFERENT directory with the old pin (size 12): diff --git a/KNOWN-GAPS.md b/KNOWN-GAPS.md index 34279bb..a7423cf 100644 --- a/KNOWN-GAPS.md +++ b/KNOWN-GAPS.md @@ -92,15 +92,37 @@ list is COMPLETE, not merely that the items are acceptable. identically. Consequences: (a) fidelity between the two consistency verifiers is agreement over the pinned case families, NOT extensional equality — the harness's lied-size family pins the - boundary (73,573 cases, 3,867 expected divergences, direction - asserted one-sided); (b) Theorem 3 / `acceptCons_sound` cover the - MECHANIZED accept set, and their soundness transfers to the deployed - verifier only under the side condition that the consumer's - `(n₀, r₀)` is an authentic pinned pair and `n₁` is the authentic - size of the tree behind `r₁` — which pacta's pin-store flow supplies - by construction (`n₀` comes from the consumer's own pin, never from - the peer; `(n₁, r₁)` arrive together in one signed head). No - exploitability against that flow is claimed or ruled out here; - assessing it requires the signature/STH layer (gap 4). No pacta code - change is made (deployed behavior matches upstream RFC 9162 - implementations; the consumer flow enforces the side condition). + boundary (73,573 cases: lied old size exhaustive for n < 60, lied + new size at fixed offsets n−1/n+1/n+7; 3,867 expected divergences, + direction asserted one-sided per case); (b) Theorem 3 / + `acceptCons_sound` cover the MECHANIZED accept set. The exhibited + divergence is outside the intended pin-store input invariant; + applying the mechanized soundness result to the deployed flow + therefore additionally ASSUMES that the deployed state machine + always binds each root to its authentic size and exposes no + alternate invocation path — an invariant that is NOT mechanized in + this corpus (gap 15). Where the invariant's witnesses live: paper + §5.3 (the signed head binds `(n₁, r₁)` together under one + signature) and §5.4 (the pin `(n₀, r₀)` comes from the consumer's + own store, never from the peer), implemented in the pacta repo at + `src/pacta/sthstore.py` and `src/pacta/logclient.py` — code OUTSIDE + the supplied fidelity target (review R4-3/GPT-4). No exploitability + against that flow is claimed or ruled out here; assessing it + requires the signature/STH layer (gap 4). No pacta code change is + made (deployed behavior matches upstream RFC 9162 implementations). +15. **Deployment refinement invariant unmechanized** (round-4 GPT, its + principal finding — split out from gap 14 because it carries the + deployed-soundness claim). The corpus proves soundness of the + mechanized `acceptCons`; it does NOT prove the refinement + `AuthenticPair(n₀,r₀,D₀) ∧ AuthenticPair(n₁,r₁,D₁) ∧ + verify_consistency(…) → acceptCons(…)`. The operational invariant + (authentic-size/root binding via the signed-head + pin-store flow) + is relied upon but unverified, and the consumer flow implementing it + is not in the supplied fidelity target. Consequently any attestation + of this corpus must be scoped to the MECHANIZED model: "the deployed + consistency verifier is formally verified" is NOT a claim this + corpus supports. Closure paths (roadmap, operator decision, post + paper-freeze): (A) make the deployed verifier adopt + ConsRec-equivalent acceptance; or (B) mechanize the signed-head + + pin-store state machine and prove the refinement; or (C) keep the + boundary and this scoped claim permanently. diff --git a/README.md b/README.md index 6d1ae49..8082d0b 100644 --- a/README.md +++ b/README.md @@ -11,14 +11,19 @@ All paper-§10 mechanization targets are kernel-checked; the audit surface is defined and green (`verification/check.sh`, exit 0). See [STATEMENT-MAP.md](STATEMENT-MAP.md) for the paper↔Lean review surface and [KNOWN-GAPS.md](KNOWN-GAPS.md) for the honest scope ledger. -Revised after review round 1 (GPT-5.6 + second Claude) and round 2: -the audit surface is now an environment-derived inventory -(`Proofs/Inventory.lean` + pinned allowlist, self-tested by -`selftest_audit.sh`), the review kit's fidelity target is -self-contained, `acceptIncl` routes Theorems 1–2, fidelity families -extended (230,271 / 230,016). No changes until the external review -completes. The finished certificates' attestation into the LTL is a -separate, explicitly-authorized operator decision. +Revised across four external review rounds (GPT-5.6 + a second Claude, +adversarial; zero broken theorems in any round; both approved after +round 4). The audit surface is an environment-derived inventory +(`Proofs/Inventory.lean` + pinned allowlist — 222 constants, +61 human-reviewed cones, self-tested by `selftest_audit.sh`); the review +kit is push-button reproducible (`run_bare.sh`, self-contained fidelity +target); `acceptIncl`/`acceptCons_sound` route the theorems through the +named acceptance predicates; fidelity = agreement over pinned families +(230,271 + 230,016 baseline; 73,573 lied-size boundary cases with +3,867 expected one-sided divergences — KNOWN-GAPS gaps 14/15, not +extensional equality). Doc counts are asserted by check.sh Phase 3c. +The finished certificates' attestation into the LTL is a separate, +explicitly-authorized operator decision, scoped per the runbook. | layer | content | status | |---|---|---| @@ -28,7 +33,7 @@ separate, explicitly-authorized operator decision. | L4 | frontier binding content (Lemma 2) | **done as specializations** — inlined in the extractor walk (`extractIncl`), whole-tree (`extractMTH`), ConsRec (`consRecBinding`); the standalone `Root` receipt-uniqueness instance was deleted with the vacuous `root_binding` in S3.5 and deliberately NOT restored (optional, unused — KNOWN-GAPS gap 3) | | L5 | inclusion soundness = EXPLICIT extractor `extractIncl` (Theorem 2) | **done, non-vacuous** | | L6a | descent extractor `extractMTH` (Theorem 3 step 3 = Lemma 2, whole-tree instance) | **done, non-vacuous** | -| L6b | Theorem 3 (consistency soundness): `consRecBinding` (steps 1–2) + `extractCons`/`extractCons_correct` (+ `_paper` at the paper's exact quantifiers) | **done, non-vacuous** | +| L6b | Theorem 3 (consistency soundness): `consRecBinding` (steps 1–2) + `extractCons`/`extractCons_correct` (+ `_paper` at the paper's exact quantifiers; `acceptCons_sound` routes it through the named `acceptCons` predicate, size bound derived from acceptance via `consRec_some_le`) | **done, non-vacuous** | | L6c | pin-store state machine safety (Proposition 1): `pinAccept_monotone`, `pin_prefix_correct`, `fork_distinct` | **done, non-vacuous** (per-step; multi-step chain = gap 7) | ## Discipline (identical to the subject corpora) diff --git a/RESPONSE-TO-REVIEWERS.md b/RESPONSE-TO-REVIEWERS.md index 2a54e2e..50c9cd8 100644 --- a/RESPONSE-TO-REVIEWERS.md +++ b/RESPONSE-TO-REVIEWERS.md @@ -1,119 +1,90 @@ -# Response to reviewers — round 4 +# Response to reviewers — round 5 (housekeeping) -Corpus: `ltl-accumulator-verified`. Round-3 reviews received against the -round-3 freeze `9972ab4`: GPT-5.6 (conditional approval, one portability -finding) and the round-3 Claude reviewer's Socratic addendum (one new -confirmed finding, four reinstated ones). Every claim was independently -re-verified by the operator before any change. This round contains ONE -new theorem, one harness family, and packaging/scoping fixes. No -existing theorem statement or proof changed. +Round-4 reviews received against `2da0a79`: the Claude reviewer +("Round 4 is the cleanest round this corpus has had… Nothing blocks the +freeze; no remaining findings on the corpus itself") and GPT-5.6 +("Approve after minor documentation fixes", scoped-attestation +condition). No theorem, proof, or Lean surface changed this round — +this is the documentation-and-guardrails round both reviewers asked +for. -## The headline: F1* (Claude addendum) — CONFIRMED and absorbed +## Disposition -The addendum demonstrated that the deployed `verify_consistency` and -the mechanized `ConsRec` acceptance are **not extensionally equal**: -the deployed RFC 9162 iterative verifier accepts honest proofs under -lied size claims (witness: `verify_consistency(1, 3, R2, R3, P(2→3)) = -True`; ConsRec rejects). Reproduced exactly on the operator machine -against deployed pacta: same witness, same 3,405 divergences for -n < 60, same strictly one-sided direction (the mechanized model is the -stricter; inclusion diverges nowhere under identical abuse), same -power-of-two seeding mechanism in the deployed source. +### Stale counts, third recurrence (Claude R4-1/R4-2 = GPT §6) — fixed STRUCTURALLY -Absorbed as follows: +All `218/59` occurrences are now `222/61` (STATEMENT-MAP footer, the +check.sh comment, README status), and — the structural part R4-1 +demanded — **check.sh gained Phase 3c (doc-consistency)**: the audit +counts in STATEMENT-MAP and README are asserted against the allowlist +and the CONES table, and the four fidelity pins quoted in the +STATEMENT-MAP are asserted against the harness's own pinned constants, +on every button press. Stale-count drift is now a red button, not an +erratum. README status paragraph rewritten to round-4 reality +(lied-size family, `acceptCons_sound`, both approvals); the L6b row +names `acceptCons_sound`. -- **KNOWN-GAPS gap 14**: full statement — witness, mechanism, - one-sidedness, and the soundness-transfer side condition (the - consumer's `(n₀, r₀)` is an authentic pinned pair and `n₁` is the - authentic size behind `r₁`), which pacta's pin-store flow supplies by - construction. No exploitability against that flow is claimed or ruled - out; that assessment belongs to the signature/STH layer (gap 4). -- **Harness**: new lied-size family — 73,573 boundary cases (lied old - size exhaustive for n < 60, lied new size sampled), 3,867 expected - divergences PINNED, and the one-sided direction asserted on every - case: a single `lean=True / deployed=False` instance fails the run. - These families would have caught F1* in round 1; now they guard it - forever. -- **Banner**: `FIDELITY GREEN` now reads "agreement over the pinned - case families (not extensional equality; KNOWN-GAPS gap 14)". The - STATEMENT-MAP fidelity row and Theorem-3 row carry the same scoping. -- **No pacta code change.** The deployed behavior matches upstream - RFC 9162 implementations; the consumer flow enforces the side - condition (`n₀` comes from the consumer's own pin, never from the - peer; `(n₁, r₁)` arrive together in one signed head). pacta also - remains change-frozen during paper processing. +### The deployment bridge (GPT §2/§3/§4, its principal finding) — adopted in full -## F2 — `acceptCons` routed through zero theorems (CONFIRMED, fixed) +- **Gap 14 reworded** to GPT's evidence-vs-inference formulation: the + exhibited divergence is outside the intended pin-store input + invariant; applying the mechanized soundness result to the deployed + flow additionally ASSUMES the authentic-size/root binding — "is + assumed", not "transfers". The invariant's witnesses are now cited by + name (paper §5.3/§5.4; pacta `src/pacta/sthstore.py`, + `src/pacta/logclient.py` — outside the fidelity target), per Claude + R4-3. +- **New gap 15**: "Deployment refinement invariant unmechanized" — the + bridge gets its own named boundary, with the unproven refinement + spelled out and the three closure paths (adopt ConsRec semantics in + deployment / mechanize the state machine and prove refinement / keep + the scoped claim) recorded as a post-paper-freeze operator decision. +- **Attestation language is now a runbook GATE**: the exact scoped + wording from GPT §11 is embedded in ATTESTATION-RUNBOOK step B2 as a + required check — entry 13 cannot be written as "the deployed verifier + is formally verified." -New theorem `acceptCons_sound` (Theorem3.lean): soundness stated over -the named `acceptCons` predicate the harness tests — the consistency -twin of round-2's `acceptIncl_sound`. The `n₀ = 0` disjunct is -discharged from the non-prefix premise; the size bound `n₀ ≤ n₁` is -derived from ConsRec acceptance itself via the new lemma -`consRec_some_le` (the `n₀ > n` branch returns `none`), so the caller -owes nothing beyond acceptance + wrong-prefix. Cones (read from -`#print axioms`, as always): `consRec_some_le` = [propext, -LTLAcc.sha256, Quot.sound]; `acceptCons_sound` = [propext, -Classical.choice, LTLAcc.sha256, Quot.sound]. Both are in CONES, -AxiomCheck, and the inventory allowlist (218 → 222 constants; the diff -is exactly the two theorems plus their two generated auxiliaries). +### Toolchain enforcement (GPT §5) — fixed -## F3 — Lean-side kit reproducibility (CONFIRMED, fixed) +`run_bare.sh` now fail-closes on both the Lean version (`4.30.0-rc2`) +and the exact compiler commit (`3dc1a088…`); `BARE RUN GREEN` is +reserved for the pinned toolchain, exactly as recommended. -`verification/lean-toolchain` now pins `leanprover/lean4:v4.30.0-rc2`, -and `verification/run_bare.sh` is the reviewer's standalone runner: -plain public `lean`, no lake, no Aeneas checkout — compile all modules, -print all cones, run the inventory gate. Verified green on this machine -(under the operator's memory-cap discipline): 61 cone lines, 222 -constants, gate green. check.sh remains the operator's button. +### Banner wording (GPT §8) — adopted -## F4 — regex metacharacters in Phase 3b (CONFIRMED, fixed) +The per-family line now reads `consistency baseline family: … all +agree`, so a detached quotation cannot suggest global equivalence. -The `PINNED BUT NOT INVENTORIED` check now uses awk field equality -instead of a regex containing the constant name; the module-manifest -greps were already `-F`. Dots no longer act as wildcards anywhere in -the gate. +### Fidelity-target provenance (GPT §7) — REFUTED, with a courtesy fix -## F5 — kit hygiene (CONFIRMED, fixed; one sharpening) +The round-4 target tarball demonstrably contains `MANIFEST.sha256` +(six per-file SHA-256 entries) and `TARGET-PROVENANCE.md` (repo URL, +pinned commit `3d81d53`, verification instructions, extraction and run +commands) at its root — `tar tzf` lists both. The review appears to +have counted only the `.py` files. No packaging change was required; +as a courtesy, the round-5 kit ALSO ships both files unpacked beside +the tarball so they cannot be missed. (The project's discipline cuts +both ways: reviewer findings are re-verified too, and this one did not +reproduce.) -The stray `.pyc` was worse than reported: it was **git-tracked**, which -is why `git archive` shipped it. Untracked; `__pycache__/`/`*.pyc` -gitignored. The round-4 kit gives the corpus tarball the same treatment -as the pacta target: `MANIFEST.sha256` over every file in the archive -plus the pinned public commit and repo URL — this also implements -GPT's governance condition (publish hashes of the audit-critical -files; they are all in the archive the manifest covers). +### Wording nit (Claude R4-5) — adopted -## GPT §7 — hard-coded toolchain bootstrap (CONFIRMED, fixed) +Gap 14 now says "lied new size at fixed offsets n−1/n+1/n+7" — +determinism advertised, not obscured. -`AENEAS_ENV` override with a clear FATAL message in both check.sh and -selftest_audit.sh, exactly as recommended; default unchanged for the -operator. Together with F3 this closes the "reviewer-friendly -push-button" gap: reviewers get `run_bare.sh`, operators keep the -guarded button. +### Paper queue (Claude R4-4 + GPT §11) — recorded -## GPT §9 — paper-language conditions - -Adopted into the paper-cycle queue verbatim (they overlap the queue -built across rounds 1–3), plus F1*'s two additions: the fidelity -sentence must say "finite differential testing over pinned families, -extensional equality is false for consistency (one-sided)", and -Theorem 3's deployment claim must carry the pinned-pair side condition. -The paper is edited in its own cycle, not in this corpus. - -## Reviewer-process note (kept, per this project's candor convention) - -The round-3 Claude reviewer's self-analysis (Q1–Q7) found its own -"confirmed/verified" inflations and then did what the drill demands: -applied constructive-witness standards to its own strongest doubt and -produced F1*. Its round-3.5 addendum is the strongest single review -artifact this corpus has received. The operator re-verified every claim -in it anyway — trust nothing, including good news. +Added to the camera-ready queue: §10(v) "total correctness of the +pin-store state machine" must be scoped to what gaps 4/7/10 delimit; +Remark 1's "will carry" must get the gap-3 specializations rewording +when the corpus is cited as delivered; and the paper may not describe +Theorem 3 as mechanized "for the deployed verifier" without the gap-15 +qualification. ## What did NOT change -All pre-existing theorem statements and proofs; the axiom boundary -(single opaque `sha256`); the 230,271/230,016 family pins; the live -transparency log (12 leaves, root `bcd15f9d…`); deployed pacta. -Attestation remains blocked pending the ePrint decision, the author's -read, and an explicit operator order. +Every Lean file, the allowlist, the gate, the self-test, the fidelity +pins (230,271 / 230,016 / 73,573 / 3,867), the axiom boundary, the +live log (12 leaves, `bcd15f9d…`), deployed pacta. Attestation remains +gated on the ePrint decision, the operator's read (A2), the rehearsal +(A4), and an explicit operator order — with the B2 scope wording now +part of the gate. diff --git a/STATEMENT-MAP.md b/STATEMENT-MAP.md index fecc1cb..d522e93 100644 --- a/STATEMENT-MAP.md +++ b/STATEMENT-MAP.md @@ -46,14 +46,18 @@ hypothesis, nor that no other classical argument could reach the conclusion on some restricted domain. Audit surface (enforced by `verification/check.sh`, exit 0 = green): -the FULL compiled environment of the corpus modules — 218 constants, +the FULL compiled environment of the corpus modules — 222 constants, read from the Lean environment by `Proofs/Inventory.lean` (fully qualified names, kinds, axiom cones) and pinned in `verification/inventory-allowlist.txt`, diffed fail-closed both directions on every run (round-3 replacement for the round-2 source-regex -gate, which GPT H1 showed was evadable). The 59 human-reviewed statement +gate, which GPT H1 showed was evadable). The 61 human-reviewed statement cones above are additionally checked via `#print axioms` and cross-checked against the inventory's independently computed cones. +(These two counts, and the fidelity pins in the table above, are +asserted against the allowlist/CONES/harness by check.sh Phase 3c on +every run — stale-count drift is now a red button, not an erratum: +review R4-1, after three consecutive rounds of hand-edit failures.) `verification/selftest_audit.sh` attacks the gate with nine injection cases (attributed/indented/private/instance declarations, a nested namespace reusing an audited basename, a smuggled axiom, a deleted diff --git a/verification/check.sh b/verification/check.sh index da35e09..82bcd30 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -26,8 +26,9 @@ PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor Theore # Certificates and their exact expected cones (observed via #print axioms, # never guessed; any drift in EITHER direction is a failure). # AUDIT SURFACE: Phase 3b pins the FULL environment of the corpus modules -# (inventory-allowlist.txt, 218 constants incl. compiler-generated -# auxiliaries); the 59 entries below are the human-reviewed statement +# (inventory-allowlist.txt, every compiler-generated auxiliary included — +# the count is pinned by the allowlist itself and asserted against the +# docs in Phase 3c); the entries below are the human-reviewed statement # surface, additionally queried through #print axioms in Phase 3 and # cross-checked against the inventory's independently computed cones. declare -A CONES=( @@ -248,6 +249,33 @@ done [ "$COVFAIL" = 0 ] && echo " coverage complete: environment == allowlist, CONES cross-checked" [ "$COVFAIL" = 0 ] || { echo "COVERAGE FAILED"; FAIL=1; } [ "$FAIL" = 0 ] || exit 1 + +# -- Phase 3c: documentation consistency (review R4-1: hand-maintained ------ +# counts went stale three rounds running — so the docs' numbers are now +# ASSERTED against their sources: allowlist, CONES, and the fidelity pins. +echo "=== Phase 3c: doc-consistency ===" +DOCFAIL=0 +NALLOW=$(grep -c '^INV|' "$HERE/inventory-allowlist.txt") +NCONES=${#CONES[@]} +SMAP="$HERE/../STATEMENT-MAP.md" +RDME="$HERE/../README.md" +grep -qF "$NALLOW constants" "$SMAP" || { echo " DOC DRIFT: STATEMENT-MAP lacks '$NALLOW constants'"; DOCFAIL=1; } +grep -qF "$NCONES human-reviewed" "$SMAP" || { echo " DOC DRIFT: STATEMENT-MAP lacks '$NCONES human-reviewed'"; DOCFAIL=1; } +grep -qF "$NALLOW constants" "$RDME" || { echo " DOC DRIFT: README lacks '$NALLOW constants'"; DOCFAIL=1; } +grep -qF "$NCONES human-reviewed" "$RDME" || { echo " DOC DRIFT: README lacks '$NCONES human-reviewed'"; DOCFAIL=1; } +# fidelity pins quoted in the docs must equal the harness's pinned constants +for n in $(python3 -c " +import re +src = open('$HERE/fidelity/run_fidelity.py').read() +vals = [re.search(r'assert ti == ([0-9_]+)', src).group(1), + re.search(r'assert tc == ([0-9_]+)', src).group(1), + re.search(r'LIED_PIN_TOTAL = ([0-9_]+)', src).group(1), + re.search(r'LIED_PIN_DIV = ([0-9_]+)', src).group(1)] +print(' '.join(f'{int(v.replace(chr(95),\"\")):,}' for v in vals))"); do + grep -qF "$n" "$SMAP" || { echo " DOC DRIFT: STATEMENT-MAP lacks fidelity pin '$n'"; DOCFAIL=1; } +done +[ "$DOCFAIL" = 0 ] && echo " docs agree with allowlist ($NALLOW), CONES ($NCONES), fidelity pins" +[ "$DOCFAIL" = 0 ] || { echo "DOC-CONSISTENCY FAILED"; exit 1; } # -- Phase 4: definition fidelity (Lean defs vs deployed pacta verifiers) -- echo "=== Phase 4: definition fidelity ===" PACTA_SRC="${PACTA_SRC:-$HERE/../../proof-aware-crypto-tooling-agent/src}" diff --git a/verification/fidelity/run_fidelity.py b/verification/fidelity/run_fidelity.py index b293bf2..ab0177b 100644 --- a/verification/fidelity/run_fidelity.py +++ b/verification/fidelity/run_fidelity.py @@ -167,7 +167,7 @@ def main(): ti, rc, pc = inclusion() print(f" inclusion: {ti} verifier cases, {rc} MTH==merkle_root, {pc} Path==inclusion_proof — all agree") tc = consistency() - print(f" consistency: {tc} verifier cases (incl. honest), MTH checks — all agree") + print(f" consistency baseline family: {tc} verifier cases (incl. honest), MTH checks — all agree") tl, dl = lied_sizes() print(f" lied-sizes: {tl} boundary cases, {dl} EXPECTED divergences, all deployed-accepts-only (gap 14)") # pinned counts (identical generation to the paper's harness) diff --git a/verification/run_bare.sh b/verification/run_bare.sh index 03a1454..51d2378 100755 --- a/verification/run_bare.sh +++ b/verification/run_bare.sh @@ -21,6 +21,17 @@ command -v lean >/dev/null || { echo "FATAL: no 'lean' on PATH (want $(cat "$HER echo "toolchain: $(lean --version)" echo "pinned: $(cat "$HERE/lean-toolchain")" +# Fail-closed toolchain check (review round 4, GPT §5): BARE RUN GREEN is +# reserved for the pinned version AND Lean commit — a different toolchain +# must not be able to print the green marker. +EXPECTED_VERSION="4.30.0-rc2" +EXPECTED_COMMIT="3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc" +ACTUAL="$(lean --version)" +grep -qF "version $EXPECTED_VERSION" <<<"$ACTUAL" || { + echo "FATAL: toolchain version mismatch (want $EXPECTED_VERSION): $ACTUAL"; exit 1; } +grep -qF "commit $EXPECTED_COMMIT" <<<"$ACTUAL" || { + echo "FATAL: toolchain commit mismatch (want $EXPECTED_COMMIT): $ACTUAL"; exit 1; } + export LEAN_PATH="${LEAN_PATH:+$LEAN_PATH:}$HERE/gen:$HERE" echo "=== compile (gen + 9 proof modules) ==="