diff --git a/ATTESTATION-RUNBOOK.md b/ATTESTATION-RUNBOOK.md index 9790ca5..706f3e5 100644 --- a/ATTESTATION-RUNBOOK.md +++ b/ATTESTATION-RUNBOOK.md @@ -79,7 +79,7 @@ NEW_SIZE = 13 | Forgejo mirrors | `https://zkdefi.org/saymrwulf/.git` (anonymously readable) | pull-synced by server cron nightly 03:00 UTC (`/home/admin/cloud/bin/reconcile-mirrors.py`, log `.reconcile.log`); verify per step A5 | | log public key | `lean-transparency-log/provider.ed25519.pub` (PEM) | fingerprint `874c8a00…a56a` in `log-metadata.json` | | log PRIVATE key | **RESOLVED 2026-07-12**: laptop-side, mode 0600, inside a gitignored state dir of the pacta working tree (exact path in operator-private notes, deliberately not in this public file); public half byte-matches `provider.ed25519.pub`. NOT on the droplet. encrypted SD backup exists (A3b, operator, 2026-07-14) | A3 done; A3b done | -| producer driver | **RESOLVED 2026-07-12**: it exists and is committed — pacta's `provider/` CLI (`python3 -m pacta_provider`: `check` → signed attestation; `log-append` → leaf + signed STH + receipt; `log-publish` → public face). Heads are signed with `signing_backend: verified-dalek-serial` (the dogfooded verified signer), `self_inclusion: verified`. Only the per-run orchestration was session work | see step A4 (rehearsal, not reconstruction) | +| producer driver | **RESOLVED 2026-07-12**: it exists and is committed — pacta's `provider/` CLI (`python3 -m pacta_provider`: `check` → signed attestation; `log-append` → leaf + signed STH + receipt; `log-publish` → public face). Heads are signed with `signing_backend: verified-dalek-serial` (the dogfooded signer binary built from the verify-path-proven dalek fork; the signing operation itself is not proven — clarification added 2026-08-08, the event is unchanged), `self_inclusion: verified`. Only the per-run orchestration was session work | see step A4 (rehearsal, not reconstruction) | | server deployment | the private infrastructure repo (github, `master`) — since `a186bac` includes the ltl vhost/service/reconstruct.py, md5-verified == droplet | see its `DEPLOY.md` § "The LTL service" | --- diff --git a/README.md b/README.md index cd91cf7..2a03c11 100644 --- a/README.md +++ b/README.md @@ -35,8 +35,10 @@ 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. -Reviewed across **six** external adversarial rounds (GPT-5.6 + a second -Claude; zero broken theorems in any round; both approved). The audit +Reviewed across **six** external adversarial rounds through the entry-13 +freeze (GPT-5.6 + a second Claude; zero broken theorems in any round; both +approved), plus the estate-wide rounds 7–9 whose accumulator findings are +harvested in the private register and fixed here. 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 @@ -44,8 +46,10 @@ pinned allowlist — 222 constants, 61 human-reviewed cones, self-tested by `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. +**0 divergences since the sn==0 fix**, pacta `ddbb5a4`, 2026-07-23 — gap 14 +is CLOSED; the historical 3,867 one-sided divergence family is preserved at +tag `vulnerable/sn0-consistency-fd2f6ba`. Still finite-family testing, not +extensional equality — the open deployment boundary is gap 15). Doc counts are asserted by check.sh Phase 3c. How the append was done — release tuple, preflight, candidate-inspection gate, and the 12→13 structural rehearsal — is recorded in [ATTESTATION-RUNBOOK.md](ATTESTATION-RUNBOOK.md). diff --git a/STATEMENT-MAP.md b/STATEMENT-MAP.md index c89c388..34fecf2 100644 --- a/STATEMENT-MAP.md +++ b/STATEMENT-MAP.md @@ -29,11 +29,11 @@ This map is the review surface. | Lemma 2, whole-tree instance | `extractMTH` + `extractMTH_correct` | Descent | sha256 (+choice) | | Lemma 2, ConsRec instance (Thm 3 steps 1–2) | `consRecBinding` | Binding3 | sha256 (+choice) | | Theorem 2 (inclusion soundness, explicit 𝓔) | `extractIncl` + `extractIncl_correct` | Extract | sha256 (+choice) | -| Theorem 3 (consistency soundness, explicit 𝓔′) | `extractCons` + `extractCons_correct`; `extractCons_correct_paper` at the paper's exact quantifiers (n₀=0 discharged); `acceptCons_sound` routes it through the named `acceptCons` predicate (size bound derived from acceptance via `consRec_some_le`). Covers the MECHANIZED accept set; transfer to the deployed verifier is conditional on the pinned-pair side condition of gap 14 | Theorem3 | sha256 (+choice) | +| Theorem 3 (consistency soundness, explicit 𝓔′) | `extractCons` + `extractCons_correct`; `extractCons_correct_paper` at the paper's exact quantifiers (n₀=0 discharged); `acceptCons_sound` routes it through the named `acceptCons` predicate (size bound derived from acceptance via `consRec_some_le`). Covers the MECHANIZED accept set; transfer to the deployed verifier is conditional on the deployment refinement invariant of gap 15 (gap 14 closed 2026-07-23) | Theorem3 | sha256 (+choice) | | Prop 1(1) (pin monotonicity + prefix) | `pinAccept`, `pinAccept_monotone`, `pin_prefix_correct` | PinStore | sha256 (+choice) | | Prop 1(2), Merkle share | `fork_distinct` (different roots ⇒ different content); transferability = signature layer, out of scope | PinStore | sha256 | | non-vacuity guards (anti-pigeonhole) | `extractIncl_nonvacuous`, `extractMTH_nonvacuous`, `extractCons_nonvacuous`, `pin_prefix_nonvacuous` | Extract/Descent/Theorem3/PinStore | sha256 | -| definition fidelity vs deployed verifier | `fidelity/` harness: MTH==merkle_root, Path==inclusion_proof, verifier agreement 230,271 inclusion + 230,016 consistency over the pinned case families — **not extensional equality**: the lied-size family (73,573 cases) pins the known one-sided divergence of gap 14 (3,867 expected, deployed-accepts-only, direction asserted) | fidelity | (testing) | +| definition fidelity vs deployed verifier | `fidelity/` harness: MTH==merkle_root, Path==inclusion_proof, verifier agreement 230,271 inclusion + 230,016 consistency over the pinned case families — **not extensional equality**: the lied-size family (73,573 cases) pins **0 divergences** at the current subject (post-`ddbb5a4` pacta, see PACTA-PIN.sha256; gap 14 closed 2026-07-23 — the historical 3,867 one-sided family is recorded in its closure note) | fidelity | (testing) | Note on "assumption-free" (paper §10(i)): `incl_complete`'s cone lists `LTLAcc.sha256`, but the theorem assumes **no property** of it — it @@ -66,7 +66,7 @@ cross-checked against the inventory's independently computed cones. 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 fourteen +`verification/selftest_audit.sh` attacks the gate with fifteen injection cases (attributed/indented/private/instance declarations, a nested namespace reusing an audited basename, a smuggled axiom, a deleted declaration, and unmanifested Proofs/ and gen/ modules) — each diff --git a/docs/optimistic-accountability.md b/docs/optimistic-accountability.md index 38fee2a..f37d494 100644 --- a/docs/optimistic-accountability.md +++ b/docs/optimistic-accountability.md @@ -145,8 +145,9 @@ rollup metaphor to be remarkable. - Mechanized statements: `STATEMENT-MAP.md` (this repo); the fraud- proof-generator reading of Theorem 3 is `extractCons_correct` + - `acceptCons_sound`; scope boundaries in `KNOWN-GAPS.md` (esp. gap 14: - the deployed-verifier side condition; gap 4: the signature layer, + `acceptCons_sound`; scope boundaries in `KNOWN-GAPS.md` (esp. gap 15: + the deployment refinement invariant — gap 14, the historical deployed-verifier + divergence, closed 2026-07-23; gap 4: the signature layer, where equivocation-evidence transferability lives). - Deployed anatomy: leaf → `entries/NNNNNN.json`; head → `latest-sth.json` (+ `sth-history.jsonl`); the head is signed by the