ATTESTATION-RUNBOOK.md

@@ -1,14 +1,6 @@
 # ATTESTATION RUNBOOK — entry 13 (the log attests its own machinery)
 
-Status: **COMPLETE — entry 13 appended and live, 2026-07-16.**
+Status: **Phase A open, Phase B BLOCKED** (see gate at Phase B).
-Log tree 12→13; new root `3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d`;
-new leaf index 12, hash `8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a`
-(subject ltl-accumulator-verified@172a1d0, 61/61, mechanized-model scope,
-KNOWN-GAPS 14/15). log-clone commit `1726e8e`, pushed + deployed + live-
-consumer-verified (accepted:true, ed25519:verified). Evidence on SD
-outputs/entry13-append-evidence/. This runbook is retained as the record
-of how it was done. The log now carries kernel-checked proofs of its own
-accumulator machinery.
 This file is the single authoritative ToDo for everything that happens
 between now and the appending of leaf index 12 (the 13th entry, file
 `entries/000012.json`, tree size 12 → 13). It is written to be executed
@@ -22,37 +14,11 @@ Agent Appendix at the end. Every step ends in a mechanical check.
 | term | meaning |
 |---|---|
 | **operator** | The human running the log service (owner of ltl.zkdefi.org and its keys). NOT warden (warden is a consumer). All Phase-B actions are operator actions. |
-| **corpus** | `ltl-accumulator-verified` at freeze commit `172a1d0` (round-5 freeze — the reviewed subject; supersedes the earlier `2da0a79`) — the kernel-checked mechanization of paper §6. |
+| **corpus** | `ltl-accumulator-verified` at freeze commit `2da0a79` — the kernel-checked mechanization of paper §6. |
 | **the button** | `verification/check.sh`. Green means: printed `=== ATTESTATION GREEN (Lean + fidelity) ===` AND `echo $?` printed `0`. BOTH. Never judge from scrolled output. |
 | **the log** | Live service ltl.zkdefi.org + public mirror repo `lean-transparency-log`. Currently 12 leaves (indices 0–11), head root `bcd15f9d…`, FROZEN. |
 | **entry 13** | The next leaf: the attestation of the corpus itself. Does not exist yet. |
-| **kit round N** | The review package delivered to the external reviewers after freeze N. Round-1 kit = freeze `6e56414`; round 2 = `260ad64`; round 3 = `9972ab4`; round 4 = `2da0a79`; round 5 = `172a1d0`; round 6 = review of `172a1d0` + pacta producer (current). |
+| **kit round N** | The review package delivered to the external reviewers after freeze N. Round-1 kit = freeze `6e56414`; round 2 = `260ad64`; round 3 = `9972ab4`; round 4 = `2da0a79` (current). |
-
-## 2a. Release tuple (the single source of immutable identifiers)
-
-Phase B binds THESE exact identifiers. Every Phase-B command consumes
-them; any mismatch aborts. Filled from the round-6 rehearsal
-(2026-07-16); re-confirm each on the day (B0).
-
-```
-SUBJECT_COMMIT   = 172a1d0653f489d5b7cb73ac7942a57cbb496532   # corpus (round-5 freeze, reviewed r6)
-PACTA_CODE_BASE  = 8b1a325caaef6d3993d63d4c730eab03065e936b   # round-6-hardened
-                    producer: parser hardening + fail-closed classifier +
-                    leaf `scope` block + examples/repos.yaml entry + dead-code
-                    cleanup. The 12→13 rehearsal ran green on this producer.
-PACTA_COMMIT     = <the pacta working-tree HEAD at B2 time — MUST have
-                    `git diff PACTA_CODE_BASE HEAD -- src provider` EMPTY
-                    (producer code identical to the reviewed base; doc-only
-                    commits above it, e.g. paper/, are fine). Record the exact
-                    HEAD in the B6 evidence.>
-EXPECTED_OLD_SIZE= 12
-EXPECTED_OLD_ROOT= bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9
-KEY_FINGERPRINT  = 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a
-CONFIG           = pacta examples/repos.yaml, entry ltl-accumulator-verified (record its sha256 in B0)
-NEW_INDEX        = 12   (the 13th leaf)
-NEW_SIZE         = 13
-```
-
 
 ## 1. Iron rules (violating any of these is never correct)
 
@@ -68,23 +34,23 @@ NEW_SIZE         = 13
    pass." A failed check means the run is over.
 5. IACR/editor correspondence never enters any git repo (SD card only).
 
-## 2. Facts (as of 2026-07-16, post round-6)
+## 2. Facts (as of 2026-07-12, round-4 freeze)
 
 | artifact | where | state |
 |---|---|---|
-| corpus | github.com/saymrwulf/ltl-accumulator-verified | **`172a1d0`** (round-5 freeze; = SUBJECT_COMMIT §2a), pushed, clean. `2da0a79` was the round-4 freeze — superseded. |
+| corpus | github.com/saymrwulf/ltl-accumulator-verified | `2da0a79`, pushed, working tree clean |
-| review kits | SD `outputs/accumulator-review-kit-round{2..6}/` | round 6 (pre-attestation sign-off) delivered 2026-07-16; corpus tarball `18fbd697…` + `CORPUS-MANIFEST.sha256` |
+| review kit round 4 | SD `outputs/accumulator-review-kit-round4/` | delivered (corpus tarball sha `2963acbb…`, per-file `CORPUS-MANIFEST.sha256`) |
 | log mirror repo | github.com/saymrwulf/lean-transparency-log | `ec12dda` (12 leaves; unchanged since paper submission) |
-| pacta (producer) | github.com/saymrwulf/proof-aware-crypto-tooling-agent | change-freeze LIFTED 2026-07-16 (IACR decided). Producer for entry 13 = `PACTA_COMMIT` (§2a): the commit carrying the round-6 parser hardening + fail-closed classifier + leaf `scope` block + `examples/repos.yaml` entry. NOT the old `3d81d53`. |
+| pacta | github.com/saymrwulf/proof-aware-crypto-tooling-agent | `3d81d53` (change-frozen during paper processing) |
 | Forgejo mirrors | `https://zkdefi.org/saymrwulf/<repo>.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 |
+| 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. **No second copy exists** — see step A3b | A3 done; A3b done (operator, 2026-07-14) |
 | 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) |
 | server deployment | private repo `PersonalCloudServer` (github, `master`) — since `a186bac` includes the ltl vhost/service/reconstruct.py, md5-verified == droplet | see its `DEPLOY.md` § "The LTL service" |
 
 ---
 
-## PHASE A — preparation (complete except A2)
+## PHASE A — do now / while waiting for the IACR decision
 
 ### A1. Reviewer confirmations of round 4 — **DONE (2026-07-15)**
 Both round-4 reviews are on the SD card. Claude reviewer: "Nothing
@@ -102,11 +68,7 @@ remaining documentation items.
 Read, in this order, against the paper's §6 and §10:
 1. `STATEMENT-MAP.md` — every row: does the Lean statement say what
    the paper's item says?
-2. `KNOWN-GAPS.md` — all **15** entries (confirm the count on the day:
+2. `KNOWN-GAPS.md` — all 14 entries: is each acceptable to publish?
-   `grep -cE '^[0-9]+\.' KNOWN-GAPS.md` → 15): is each acceptable to
-   publish? Gap 15 (deployment refinement invariant unmechanized) is
-   the one that most constrains the leaf's claim — read it last and
-   deliberately.
 No proofs need reading; the kernel checked those. Budget one evening.
 **Check:** operator writes one line — "statement map and gaps read and
 accepted, <date>" — into the SD card notes (NOT into a repo, to keep
@@ -131,57 +93,29 @@ openssl pkey -in <CANDIDATE_PRIVATE_KEY> -pubout \
 operator's private notes (never in git). Do not copy the key anywhere,
 do not print it, do not change its permissions.
 
-### A4. Structural 12→13 rehearsal — **DONE (round 6, 2026-07-16)**
+### A4. Rehearse and document the append invocation (revised 2026-07-12)
-The first A4 rehearsal (a one-leaf log from scratch) was rejected by
+Correction to this runbook's first version: the producer driver is NOT
-round-6 review: it exercised the invocation but NOT the 12→13
+lost session work — it is the committed `pacta_provider` CLI in pacta's
-transition. Redone as a structural 12→13 rehearsal (GPT Method B:
+`provider/` tree (`check` emits the signed attestation; `log-append`
-throwaway key on a disposable COPY of the real operational state).
+appends the leaf and signs the new head via `make_signed_tree_head`,
-Transcript on SD (`entry13-rehearsal-12to13_20260716-…_e1a15aab.txt`),
+using the verified-dalek-serial dogfood signer; `log-publish` exports
-throwaway state destroyed. Verified end to end:
+the public face that `lean-transparency-log` and the droplet's
-- disposable copy of `provider/state/transparency-log-main` roots to
+`published/` carry; `serve` never touches keys). Leaves 8–11 were
-  `bcd15f9d…` == live (the real append base);
+produced exactly this way. What was never persisted is only the
-- candidate from the clean-room subject `172a1d0` + pinned producer:
+per-run orchestration (the loop + flags).
-  61/61 proven+clean, and the **scoped wording is IN THE LEAF's `scope`
-  block** (subject/certs/scope all inspected — this is the B2b gate,
-  rehearsed);
-- append 12→13 → tree_size 13, leaf index 12;
-- prefix immutability: entries 0..11 byte-identical to the predecessor;
-- consistency 12→13 accepted by BOTH the deployed verifier AND the
-  mechanized model.
 
-Three real defects were found and fixed by this rehearsal before it
+To do before the IACR decision arrives:
-went green:
+1. Write down, in operator-private notes, the exact `pacta_provider
-1. re-APPENDING published entries double-wraps them (`log-append`
+   check` / `log-append` / `log-publish` invocation for the subject
-   wraps its input; published `leaf` fields are already wrapped) —
+   `ltl-accumulator-verified @ 2da0a79` (flags per the leaves-8–11
-   wrong root. The published face itself rebuilds the tree fine; the
+   pattern; key/pub paths from A3's notes).
-   append base must nonetheless be the operational state
+2. Rehearse it against a THROWAWAY copy of the log state.
-   (`provider/state/transparency-log-main`), which stores unwrapped
+**Check (rehearsal, throwaway copy only):** `pacta witness-audit` on
-   attestations. Now B0 checks exactly this.
+the throwaway export exits 0 — every prefix root recomputed, every
-2. pacta axiom parser mis-attributed cones to axiom-free certificates
+historical STH + signature verified, including the new one. The
-   and matched names by substring (the accumulator is the first subject
+throwaway copy is then DELETED (its head was signed with the real key
-   with axiom-free certs) — fixed + record-scoped + fail-closed
+over a rehearsal tree — it must never be published or retained; if
-   classification (pacta round-6 hardening; 6 regression tests).
+retention is wanted for study, rehearse with a throwaway KEY instead).
-3. the attestation LEAF did not carry its scope block at all — the
-   scoped wording reached only the claim card. Fixed: `build_attestation`
-   now emits `scope` (guarantees/exclusions/deployment_constraints).
-
-Version-controlled artifacts for the real run: pacta
-`examples/repos.yaml` entry `ltl-accumulator-verified` (61 certs w/
-per-cert cones, nine `axiom_imports`, `known_status` = the scoped
-wording), plus the round-6 pacta commit (`PACTA_COMMIT`, §2a). The real
-B-phase run differs only in: real key/pub paths (A3 notes),
-`--log-dir provider/state/transparency-log-main`, `log-publish
---git-dir <lean-transparency-log clone>`, and — the one thing the
-rehearsal could NOT do under a throwaway key — full-history
-witness-audit under the PRODUCTION key (that is B0 + B3's job).
-
-Background (retained): the producer driver was never lost session work
-— it is the committed `pacta_provider` CLI (`check` → signed
-attestation; `log-append` → leaf + head via `make_signed_tree_head`,
-verified-dalek-serial signer; `log-publish` → public face; `serve`
-keyless). Leaves 8–11 were produced this way; only the per-run
-orchestration was ephemeral, and it is now the version-controlled
-`examples/repos.yaml` entry + this runbook's B-steps.
 
 ### A3b. Back up the signing key — **DONE (operator, confirmed 2026-07-14)**
 Completed by the operator; the procedure below is retained as the
@@ -218,109 +152,33 @@ server cron needs attention (`/home/admin/cloud/.reconcile.log`).
 
 ## PHASE B — the append (BLOCKED until the gate below is fully open)
 
-**GATE — all six, no exceptions, no substitutions:**
+**GATE — all five, no exceptions, no substitutions:**
 - [ ] A1 done (both reviewers confirmed, in writing, on SD)
-- [ ] A2 done (author read of all **15** KNOWN-GAPS entries, dated note)
+- [ ] A2 done (author read, dated note)
-- [ ] A3 done (KEY CONFIRMED) + A3b (encrypted backup)
+- [ ] A3 done (KEY CONFIRMED)
-- [ ] A4 done (structural **12→13** rehearsal green — round 6)
+- [ ] A4 done (driver committed + rehearsal witness-audit exit 0)
-- [ ] B0 passed on the day (live predecessor state re-verified)
+- [ ] The IACR decision has arrived AND the operator has given an
-- [ ] The operator has given an explicit, fresh order to append — in
+      explicit, fresh order to append — in words, on that day.
-      words, on that day. A past intention does NOT count. (The IACR
+      A past "we'll do it after acceptance" does NOT count.
-      decision arrived 2026-07-16, rejected; per operator it no longer
-      gates — so this reduces to the fresh order.)
-
-Set the release tuple (§2a) into the shell first; every step reads it:
-```
-SUBJECT_COMMIT=172a1d0653f489d5b7cb73ac7942a57cbb496532
-PACTA_COMMIT=<pacta commit with the round-6 hardening + repos.yaml entry>
-EXPECTED_OLD_SIZE=12
-EXPECTED_OLD_ROOT=bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9
-```
-
-### B0. Preflight the live predecessor state (NEW — round-6 GPT §10)
-An append-only system must re-read its actual predecessor, not trust a
-Facts table. Fresh clone of `lean-transparency-log`; verify ALL of:
-- exactly `$EXPECTED_OLD_SIZE` NUMBERED leaves `entries/[0-9]*.json`
-  (NOT `ls entries/ | wc -l` — `entries/` also holds per-component
-  `<component>.attestation.json` convenience pointers; the live log has
-  12 numbered leaves + 4 named pointers = 16 files. The tree size is the
-  numbered count and the STH's `tree_size`, never the file count);
-- `latest-sth.json` tree_size == `$EXPECTED_OLD_SIZE`;
-- its full `root_hash` == `$EXPECTED_OLD_ROOT`;
-- the STH signature verifies under `provider.ed25519.pub`
-  (fingerprint == `KEY_FINGERPRINT`);
-- `pacta witness-audit --published-dir <clone>` exits 0 (every prefix
-  root + every historical STH signature — real key, so this passes here
-  where the rehearsal could not);
-- live service agrees: `curl -s https://ltl.zkdefi.org/v1/sth` returns
-  the same size and root;
-- GitHub mirror head == local clone head;
-- the operator's operational state
-  (`provider/state/transparency-log-main`) has `$EXPECTED_OLD_SIZE`
-  entries and roots to `$EXPECTED_OLD_ROOT` (this IS the append base.
-  The published face DOES rebuild the tree — hash each stored `leaf`
-  as-is; witness-audit does exactly that. The trap the round-6
-  rehearsal hit is different: published entries store the WRAPPED leaf,
-  and feeding them back through `log-append` wraps them AGAIN —
-  double-wrapped leaves, wrong root. Appends therefore run ONLY against
-  the operational state, which stores unwrapped attestations);
-- no partial entry 13 exists anywhere (no `entries/000012.json`, no
-  size-13 head).
-**Check:** every bullet true. Any mismatch: STOP.
 
 ### B1. Clean-room re-verification of the subject
 ```
 git clone https://github.com/saymrwulf/ltl-accumulator-verified /tmp/attest-13
-cd /tmp/attest-13 && git checkout $SUBJECT_COMMIT
+cd /tmp/attest-13 && git checkout 2da0a79
-test -z "$(git status --porcelain)"        # clean tree
 cd verification && ./check.sh ; echo "exit=$?"
 ```
-**Check:** clean tree; prints `=== ATTESTATION GREEN (Lean + fidelity)
+**Check:** prints `=== ATTESTATION GREEN (Lean + fidelity) ===` and
-===` and `exit=0`. Then `./selftest_audit.sh ; echo "exit=$?"` →
+`exit=0`. Then `./selftest_audit.sh ; echo "exit=$?"` → `SELF-TEST
-`SELF-TEST GREEN`, `exit=0`. Archive the check transcript; record its
+GREEN`, `exit=0`. Any other outcome: STOP (iron rule 4).
-sha256 (bound into evidence per B6). Any other outcome: STOP.
 
-### B1b. Pin the producer (NEW — round-6 GPT §4; corrected during execution)
+### B2. Run the driver (from A4) against the REAL log repo clone
-The leaf is generated by pacta AND signed by the verified-dalek-serial
+Fresh clone of `lean-transparency-log`, driver runs once, produces:
-dogfood binary using the private key — BOTH the built binary
+`entries/000012.json`, updated `latest-sth.json` (tree_size 13),
-(`dogfood/state/`) and the key (`provider/state/local-provider/`) live
+one new line in `sth-history.jsonl`, one new receipt.
-only in the operator's working tree, NOT in a bare clone. So the
-producer for B2/B3 is the operator's pacta WORKING TREE, verified to be:
-```
-git -C <pacta working tree> rev-parse HEAD          # == $PACTA_COMMIT
-git -C <pacta working tree> status --porcelain   | grep -v '^??' | wc -l                           # == 0 (tracked clean)
-ls dogfood/state/*.provenance.json                  # dogfood binary present
-python3 scripts/mini_pytest.py                      # full green (needs the binary)
-```
-**Check:** HEAD == `$PACTA_COMMIT`; no tracked modifications; dogfood
-binary present; suite green. (A fresh clone will FAIL the wallet
-dogfood-signer test — that test needs the built binary; it is
-orthogonal to the log path. Verify the log-relevant modules explicitly
-if in doubt: `test_lean.py`, `test_provider.py`, `test_web_and_witness.py`.)
 
-### B2. Generate the candidate attestation (do NOT append yet)
+**REQUIRED ATTESTATION SCOPE (round-4 GPT §11 — this wording is a gate
-Using the pinned producer (the operator's pacta working tree at
+condition, not a suggestion).** The leaf's human-readable claim text
-`$PACTA_COMMIT`, verified in B1b) and its
+must be scoped to the mechanized model, in substance:
-`examples/repos.yaml` entry `ltl-accumulator-verified`, run
-`pacta_provider check` against the clean-room subject `/tmp/entry13/attest-13`
-(A4's rehearsed invocation, real key/pub from A3's notes). NOTE: the
-candidate emerges PROVIDER-SIGNED (check signs at generation — that is
-fine and reversible); what must not happen before inspection is the
-APPEND. Nothing enters the log in this step.
-
-### B2b. Candidate-leaf inspection gate (NEW — round-6 GPT §5, both reviewers)
-Before any append, mechanically require of the generated attestation:
-- `subject.component == ltl-accumulator-verified`
-- `subject.repo_url ==` the expected URL
-- `subject.repo_commit == $SUBJECT_COMMIT` (FULL sha)
-- 61 certificates; all `status == proven`; all `axiom_status == clean`
-- `scope.deployment_constraints` contains the REQUIRED scoped wording
-  (below) and does NOT contain "deployed verifier is formally verified"
-- `scope.exclusions` contains the boundary exclusions (SHA-256 CR,
-  gaps 14/15, gap 4)
-
-REQUIRED ATTESTATION SCOPE (round-4 GPT §11; now carried by the LEAF's
-`scope` block — round-6 fix — not merely the claim card):
 
 > This corpus kernel-checks the listed theorems about the mechanized
 > recursive accumulator model. Correspondence with the deployed
@@ -330,89 +188,47 @@ REQUIRED ATTESTATION SCOPE (round-4 GPT §11; now carried by the LEAF's
 > result to the deployed consumer flow additionally relies on an
 > unmechanized authentic-size/root invariant (KNOWN-GAPS 14/15).
 
-**Check:** all assertions pass; record the candidate's pre-append sha256.
+The leaf must NOT say or imply "the deployed verifier is formally
-Any failure: STOP (do not append a leaf you could not inspect).
+verified."
+**Check:** `git status` shows exactly those four paths changed/added,
+nothing else. The claim text above appears in the attestation.
+`pacta witness-audit` on the clone exits 0.
 
-### B3. Append 12→13 against the operational state
+### B3. Consumer's-eye check before publishing
-`pacta_provider log-append --log-dir provider/state/transparency-log-main`
+From a DIFFERENT directory with the old pin (size 12):
-with the inspected candidate; then `log-publish --git-dir <B0's log
+`pacta sth-refresh` against the local clone (or after B4, the live
-clone>`. Produces `entries/000012.json`, updated `latest-sth.json`
+URL) must verify the signature, verify consistency 12 → 13, and
-(tree_size 13), one new `sth-history.jsonl` line, one new receipt.
+advance the pin. **Check:** exit 0, pin now 13. This exercises the
-**Check (exact-path + prefix immutability — corrected empirically on
+exact theorems of the corpus one last time, on the real data.
-the live-state clone 2026-07-16; the round-6 "exactly 4 paths" was
-WRONG — `publish` regenerates every component's inclusion-proof receipt
-against the NEW head, which is correct CT behavior, not tampering):**
-the publish clone's `git status --porcelain` shows EXACTLY these, and
-nothing else:
-```
-?? entries/000012.json                              # the new leaf
-?? entries/ltl-accumulator-verified.attestation.json # new component pointer
-?? receipts/ltl-accumulator-verified.receipt.json    # new component receipt
- M latest-sth.json                                   # tree_size 12→13
- M sth-history.jsonl                                 # one line appended
- M receipts/anza-ed25519-verified.receipt.json       # ) inclusion proofs
- M receipts/betrusted-ed25519-verified.receipt.json  # ) recomputed vs the
- M receipts/dalek-ed25519-verified.receipt.json      # ) size-13 head —
- M receipts/risc0-ed25519-verified.receipt.json      # ) EXPECTED, correct
-```
-INVARIANTS (any violation = STOP):
-- `entries/000000.json`..`000011.json` byte-identical to the pre-run clone;
-- the 4 existing `entries/<component>.attestation.json` byte-identical
-  (their attestation content is stable; only receipts move with the head);
-- `provider.ed25519.pub` UNCHANGED (the real key is the same key — if this
-  shows M, the WRONG key signed: STOP);
-- `sth-history.jsonl`: all prior lines unchanged, exactly one appended;
-- the new head's root == the root the append computed;
-- `pacta witness-audit` on the clone exits 0 (real key — full history,
-  incl. every historical STH signature, verifies).
 
-### B3b. Consumer's-eye 12→13 (round-6: independent pin advance)
+### B4. Publish
-From a DIFFERENT directory holding the OLD pin (size 12, root
-`$EXPECTED_OLD_ROOT`): `pacta sth-refresh` against the clone must
-verify the new head signature, verify consistency 12→13, and advance
-the pin to 13. **Check:** exit 0, pin now 13.
-
-### B4. Publish (the single irreversible step)
 The droplet serves the log from a DERIVED dir (`~/cloud/ltl/log`),
 rebuilt from a content mirror (`~/cloud/ltl/published`) — a bare
-`git pull` in `app/` is NOT enough (PersonalCloudServer DEPLOY.md
+`git pull` in `app/` is NOT enough (see PersonalCloudServer DEPLOY.md
-§ "The LTL service").
+§ "The LTL service" for the layout).
 ```
-cd <log clone> && git add -A && git commit -m "log update: leaf 12 - attestation of ltl-accumulator-verified@$SUBJECT_COMMIT (mechanized-model scope; KNOWN-GAPS 14/15)" && git push origin main
+cd <log clone> && git add -A && git commit -m "log update: leaf 12 - attestation of ltl-accumulator-verified@2da0a79 (paper §6 mechanization)" && git push origin main
 ssh admin@zkdefi.org
-  cd ~/cloud/ltl/app && git pull                          # code/paper (usually no-op)
+  cd ~/cloud/ltl/app && git pull                          # code/paper (usually no-op here)
+  # refresh published/ with the new log content, e.g.:
   git clone --depth 1 https://github.com/saymrwulf/lean-transparency-log /tmp/ltl-pub \
     && rsync -a --exclude .git /tmp/ltl-pub/ ~/cloud/ltl/published/ && rm -rf /tmp/ltl-pub
   cd ~/cloud/ltl && python3 reconstruct.py                # re-derive log/
   cd ~/cloud && docker compose restart ltl
 ```
 **Check:** `curl -s https://ltl.zkdefi.org/v1/sth` returns
-`"tree_size": 13` and the same root the append computed. This is the
+`"tree_size": 13` and the same root the driver computed.
-first and only irreversible action; everything before it was on
-disposable clones.
 
 ### B5. Live end-to-end verification
 `pacta log-fetch` + `pacta receipt-verify` for the new entry against
 the live service; `pacta sth-refresh` from a size-12 pin against the
 live URL. **Check:** all exit 0.
 
-### B6. Mirrors and archive (bind the evidence — round-6 GPT §7/§8)
+### B6. Mirrors and archive
 Forgejo picks the push up on the nightly cron (or trigger manually per
-A5); verify head equality. To the SD card under `outputs/` with the
+A5); verify head equality. Copy the new leaf, STH, and receipt to the
-standing `_<timestamp>_<hash8>` naming, archive a SANITIZED run record
+SD card under `outputs/` with the standing `_<timestamp>_<hash8>`
-(NO private key material) containing at least:
+naming. **Check:** SD hashes match the repo files.
-```
-subject_commit, pacta_commit, config_sha256,
-candidate_attestation_sha256 (pre-append), B1_check_transcript_sha256 + marker + exit,
-fidelity pins (230271/230016/73573/3867),
-old_size/old_root, new_index/new_size/new_root, new_leaf_hash,
-STH signature status, receipt verification, 12→13 consistency result,
-witness_audit result, consumer pin 12→13.
-```
-Plus the new leaf, STH, and receipt themselves. **Check:** SD hashes
-match the repo files; the record names the exact B1 fidelity-evidence
-digest (so the leaf's "finite differential testing" clause points at a
-concrete object, not an unbound assertion).
 
 ### B7. Aftermath (same day)
 - Update the paper's camera-ready wording per the queued list (Lemma-2

README.md

@@ -5,45 +5,25 @@ Lean 4 mechanization of the security analysis (§6) of the paper
 accumulator's own correctness and soundness theorems, kernel-checked, in
 the same discipline as the four `*-ed25519-verified` subject corpora.
 
-## Status: **ATTESTED — LTL entry 13, live (2026-07-16)**
+## Status: **FROZEN for external review** (corpus complete)
 
-This corpus is now itself a leaf of the log it describes. It was appended
+All paper-§10 mechanization targets are kernel-checked; the audit surface
-as **entry 13** of the Lean Transparency Log (freeze `172a1d0`), so the
+is defined and green (`verification/check.sh`, exit 0). See
-log carries kernel-checked proofs *about the accumulator model*
-underlying its own inclusion and consistency reasoning (a deployment we
-are unaware of a precedent for; scoped to the mechanized model, not the
-deployed verifier — see below). Live head after the append:
-tree size **13**, root
-`3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d`; this
-corpus is leaf index 12, hash
-`8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a`. The
-old 12-leaf head (`bcd15f9d…`) is a proven prefix; the 12→13 consistency
-transition is accepted by both the deployed verifier and the mechanized
-model. Fetch and verify it at
-[ltl.zkdefi.org/v1/sth](https://ltl.zkdefi.org/v1/sth). The leaf carries
-its own **scope** block: what is kernel-checked is the mechanized model
-(§6), and correspondence to the deployed verifier is scoped by
-KNOWN-GAPS 14/15 — the leaf does not claim the deployed verifier is
-formally verified.
-
-All paper-§6/§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.
-Reviewed across **six** external adversarial rounds (GPT-5.6 + a second
+Revised across four external review rounds (GPT-5.6 + a second Claude,
-Claude; zero broken theorems in any round; both approved). The audit
+adversarial; zero broken theorems in any round; both approved after
-surface is an environment-derived inventory (`Proofs/Inventory.lean` +
+round 4). The audit surface is an environment-derived inventory
-pinned allowlist — 222 constants, 61 human-reviewed cones, self-tested by
+(`Proofs/Inventory.lean` + pinned allowlist — 222 constants,
-`selftest_audit.sh`); the review kit is push-button reproducible
+61 human-reviewed cones, self-tested by `selftest_audit.sh`); the review
-(`run_bare.sh`, self-contained fidelity target);
+kit is push-button reproducible (`run_bare.sh`, self-contained fidelity
-`acceptIncl`/`acceptCons_sound` route the theorems through the named
+target); `acceptIncl`/`acceptCons_sound` route the theorems through the
-acceptance predicates; fidelity = agreement over pinned families
+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.
-How the append was done — release tuple, preflight, candidate-inspection
+The finished certificates' attestation into the LTL is a separate,
-gate, and the 12→13 structural rehearsal — is recorded in
+explicitly-authorized operator decision, scoped per the runbook.
-[ATTESTATION-RUNBOOK.md](ATTESTATION-RUNBOOK.md).
 
 | layer | content | status |
 |---|---|---|

docs/optimistic-accountability.md

@@ -1,12 +1,10 @@
 # Optimistic by construction: what the LTL holds, and what it shares with rollups
 
-Status: published. The condensed blog version is live at
+Status: essay / parked blog-post source. Per the operator's decision,
-blog.zkdefi.org ("The log notarizes itself — entry 13", 2026-07-16),
+the blog version publishes only AFTER entry 13 is live (runbook B7),
-and the closing claim — "the log carries kernel-checked proofs of its
+when the closing claim — "the log carries kernel-checked proofs of its
-own machinery" — is now literally true: entry 13 (leaf index 12, hash
+own machinery" — becomes literally true and the post can end with a
-`8cb258d6…`, subject `ltl-accumulator-verified@172a1d0`) is live under
+link to a live leaf the reader can verify in one command.
-head `tree size 13, root 3488a2d0…`, verifiable at
-ltl.zkdefi.org/v1/sth. This essay remains the long-form source.
 
 ---
 
@@ -114,8 +112,8 @@ loop that optimistic rollups themselves aspire to and largely lack:
 say precisely "this fraud-proof system cannot fail to convict" — any
 accepted rewrite yields the collision, constructively. Production
 rollups would love a kernel-checked proof of their fault-proof
-interpreters; this log carries one for its own — entry 13, inside the
+interpreters; this log will carry one for its own — inside the very
-very ledger it protects.
+ledger it protects.
 
 ## Pointers (for the eventual blog rendering)