README: soften 'first' claim to 'unaware of a precedent', scope to the model (round-10 GPT §8)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

ATTESTATION-RUNBOOK.md

@@ -1,6 +1,14 @@
 # ATTESTATION RUNBOOK — entry 13 (the log attests its own machinery)
 
-Status: **Phase A open, Phase B BLOCKED** (see gate at Phase B).
+Status: **COMPLETE — entry 13 appended and live, 2026-07-16.**
+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
@@ -14,11 +22,37 @@ 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 `2da0a79` — the kernel-checked mechanization of paper §6. |
+| **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. |
 | **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` (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`; round 5 = `172a1d0`; round 6 = review of `172a1d0` + pacta producer (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)
 
@@ -34,23 +68,23 @@ Agent Appendix at the end. Every step ends in a mechanical check.
    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-12, round-4 freeze)
+## 2. Facts (as of 2026-07-16, post round-6)
 
 | artifact | where | state |
 |---|---|---|
-| corpus | github.com/saymrwulf/ltl-accumulator-verified | `2da0a79`, pushed, working tree clean |
+| corpus | github.com/saymrwulf/ltl-accumulator-verified | **`172a1d0`** (round-5 freeze; = SUBJECT_COMMIT §2a), pushed, clean. `2da0a79` was the round-4 freeze — superseded. |
-| review kit round 4 | SD `outputs/accumulator-review-kit-round4/` | delivered (corpus tarball sha `2963acbb…`, per-file `CORPUS-MANIFEST.sha256`) |
+| 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` |
 | log mirror repo | github.com/saymrwulf/lean-transparency-log | `ec12dda` (12 leaves; unchanged since paper submission) |
-| pacta | github.com/saymrwulf/proof-aware-crypto-tooling-agent | `3d81d53` (change-frozen during paper processing) |
+| 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`. |
 | 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. **No second copy exists** — see step A3b | A3 done; A3b done (operator, 2026-07-14) |
+| 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) |
 | 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 — do now / while waiting for the IACR decision
+## PHASE A — preparation (complete except A2)
 
 ### A1. Reviewer confirmations of round 4 — **DONE (2026-07-15)**
 Both round-4 reviews are on the SD card. Claude reviewer: "Nothing
@@ -68,7 +102,11 @@ 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 14 entries: is each acceptable to publish?
+2. `KNOWN-GAPS.md` — all **15** entries (confirm the count on the day:
+   `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
@@ -93,29 +131,57 @@ 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. Rehearse and document the append invocation (revised 2026-07-12)
+### A4. Structural 12→13 rehearsal — **DONE (round 6, 2026-07-16)**
-Correction to this runbook's first version: the producer driver is NOT
+The first A4 rehearsal (a one-leaf log from scratch) was rejected by
-lost session work — it is the committed `pacta_provider` CLI in pacta's
+round-6 review: it exercised the invocation but NOT the 12→13
-`provider/` tree (`check` emits the signed attestation; `log-append`
+transition. Redone as a structural 12→13 rehearsal (GPT Method B:
-appends the leaf and signs the new head via `make_signed_tree_head`,
+throwaway key on a disposable COPY of the real operational state).
-using the verified-dalek-serial dogfood signer; `log-publish` exports
+Transcript on SD (`entry13-rehearsal-12to13_20260716-…_e1a15aab.txt`),
-the public face that `lean-transparency-log` and the droplet's
+throwaway state destroyed. Verified end to end:
-`published/` carry; `serve` never touches keys). Leaves 8–11 were
+- disposable copy of `provider/state/transparency-log-main` roots to
-produced exactly this way. What was never persisted is only the
+  `bcd15f9d…` == live (the real append base);
-per-run orchestration (the loop + flags).
+- candidate from the clean-room subject `172a1d0` + pinned producer:
+  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.
 
-To do before the IACR decision arrives:
+Three real defects were found and fixed by this rehearsal before it
-1. Write down, in operator-private notes, the exact `pacta_provider
+went green:
-   check` / `log-append` / `log-publish` invocation for the subject
+1. re-APPENDING published entries double-wraps them (`log-append`
-   `ltl-accumulator-verified @ 2da0a79` (flags per the leaves-8–11
+   wraps its input; published `leaf` fields are already wrapped) —
-   pattern; key/pub paths from A3's notes).
+   wrong root. The published face itself rebuilds the tree fine; the
-2. Rehearse it against a THROWAWAY copy of the log state.
+   append base must nonetheless be the operational state
-**Check (rehearsal, throwaway copy only):** `pacta witness-audit` on
+   (`provider/state/transparency-log-main`), which stores unwrapped
-the throwaway export exits 0 — every prefix root recomputed, every
+   attestations. Now B0 checks exactly this.
-historical STH + signature verified, including the new one. The
+2. pacta axiom parser mis-attributed cones to axiom-free certificates
-throwaway copy is then DELETED (its head was signed with the real key
+   and matched names by substring (the accumulator is the first subject
-over a rehearsal tree — it must never be published or retained; if
+   with axiom-free certs) — fixed + record-scoped + fail-closed
-retention is wanted for study, rehearse with a throwaway KEY instead).
+   classification (pacta round-6 hardening; 6 regression tests).
+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
@@ -152,33 +218,109 @@ server cron needs attention (`/home/admin/cloud/.reconcile.log`).
 
 ## PHASE B — the append (BLOCKED until the gate below is fully open)
 
-**GATE — all five, no exceptions, no substitutions:**
+**GATE — all six, no exceptions, no substitutions:**
 - [ ] A1 done (both reviewers confirmed, in writing, on SD)
-- [ ] A2 done (author read, dated note)
+- [ ] A2 done (author read of all **15** KNOWN-GAPS entries, dated note)
-- [ ] A3 done (KEY CONFIRMED)
+- [ ] A3 done (KEY CONFIRMED) + A3b (encrypted backup)
-- [ ] A4 done (driver committed + rehearsal witness-audit exit 0)
+- [ ] A4 done (structural **12→13** rehearsal green — round 6)
-- [ ] The IACR decision has arrived AND the operator has given an
+- [ ] B0 passed on the day (live predecessor state re-verified)
-      explicit, fresh order to append — in words, on that day.
+- [ ] The operator has given an explicit, fresh order to append — in
-      A past "we'll do it after acceptance" does NOT count.
+      words, on that day. A past intention does NOT count. (The IACR
+      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 2da0a79
+cd /tmp/attest-13 && git checkout $SUBJECT_COMMIT
+test -z "$(git status --porcelain)"        # clean tree
 cd verification && ./check.sh ; echo "exit=$?"
 ```
-**Check:** prints `=== ATTESTATION GREEN (Lean + fidelity) ===` and
+**Check:** clean tree; prints `=== ATTESTATION GREEN (Lean + fidelity)
-`exit=0`. Then `./selftest_audit.sh ; echo "exit=$?"` → `SELF-TEST
+===` and `exit=0`. Then `./selftest_audit.sh ; echo "exit=$?"` →
-GREEN`, `exit=0`. Any other outcome: STOP (iron rule 4).
+`SELF-TEST GREEN`, `exit=0`. Archive the check transcript; record its
+sha256 (bound into evidence per B6). Any other outcome: STOP.
 
-### B2. Run the driver (from A4) against the REAL log repo clone
+### B1b. Pin the producer (NEW — round-6 GPT §4; corrected during execution)
-Fresh clone of `lean-transparency-log`, driver runs once, produces:
+The leaf is generated by pacta AND signed by the verified-dalek-serial
-`entries/000012.json`, updated `latest-sth.json` (tree_size 13),
+dogfood binary using the private key — BOTH the built binary
-one new line in `sth-history.jsonl`, one new receipt.
+(`dogfood/state/`) and the key (`provider/state/local-provider/`) live
+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`.)
 
-**REQUIRED ATTESTATION SCOPE (round-4 GPT §11 — this wording is a gate
+### B2. Generate the candidate attestation (do NOT append yet)
-condition, not a suggestion).** The leaf's human-readable claim text
+Using the pinned producer (the operator's pacta working tree at
-must be scoped to the mechanized model, in substance:
+`$PACTA_COMMIT`, verified in B1b) and its
+`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
@@ -188,47 +330,89 @@ must be scoped to the mechanized model, in substance:
 > 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
+**Check:** all assertions pass; record the candidate's pre-append sha256.
-verified."
+Any failure: STOP (do not append a leaf you could not inspect).
-**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. Consumer's-eye check before publishing
+### B3. Append 12→13 against the operational state
-From a DIFFERENT directory with the old pin (size 12):
+`pacta_provider log-append --log-dir provider/state/transparency-log-main`
-`pacta sth-refresh` against the local clone (or after B4, the live
+with the inspected candidate; then `log-publish --git-dir <B0's log
-URL) must verify the signature, verify consistency 12 → 13, and
+clone>`. Produces `entries/000012.json`, updated `latest-sth.json`
-advance the pin. **Check:** exit 0, pin now 13. This exercises the
+(tree_size 13), one new `sth-history.jsonl` line, one new receipt.
-exact theorems of the corpus one last time, on the real data.
+**Check (exact-path + prefix immutability — corrected empirically on
+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).
 
-### B4. Publish
+### B3b. Consumer's-eye 12→13 (round-6: independent pin advance)
+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 (see PersonalCloudServer DEPLOY.md
+`git pull` in `app/` is NOT enough (PersonalCloudServer DEPLOY.md
-§ "The LTL service" for the layout).
+§ "The LTL service").
 ```
-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
+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
 ssh admin@zkdefi.org
-  cd ~/cloud/ltl/app && git pull                          # code/paper (usually no-op here)
+  cd ~/cloud/ltl/app && git pull                          # code/paper (usually no-op)
-  # 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 driver computed.
+`"tree_size": 13` and the same root the append computed. This is the
+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
+### B6. Mirrors and archive (bind the evidence — round-6 GPT §7/§8)
 Forgejo picks the push up on the nightly cron (or trigger manually per
-A5); verify head equality. Copy the new leaf, STH, and receipt to the
+A5); verify head equality. To the SD card under `outputs/` with the
-SD card under `outputs/` with the standing `_<timestamp>_<hash8>`
+standing `_<timestamp>_<hash8>` naming, archive a SANITIZED run record
-naming. **Check:** SD hashes match the repo files.
+(NO private key material) containing at least:
+```
+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,25 +5,45 @@ 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: **FROZEN for external review** (corpus complete)
+## Status: **ATTESTED — LTL entry 13, live (2026-07-16)**
 
-All paper-§10 mechanization targets are kernel-checked; the audit surface
+This corpus is now itself a leaf of the log it describes. It was appended
-is defined and green (`verification/check.sh`, exit 0). See
+as **entry 13** of the Lean Transparency Log (freeze `172a1d0`), so the
+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.
-Revised across four external review rounds (GPT-5.6 + a second Claude,
+Reviewed across **six** external adversarial rounds (GPT-5.6 + a second
-adversarial; zero broken theorems in any round; both approved after
+Claude; zero broken theorems in any round; both approved). The audit
-round 4). The audit surface is an environment-derived inventory
+surface is an environment-derived inventory (`Proofs/Inventory.lean` +
-(`Proofs/Inventory.lean` + pinned allowlist — 222 constants,
+pinned allowlist — 222 constants, 61 human-reviewed cones, self-tested by
-61 human-reviewed cones, self-tested by `selftest_audit.sh`); the review
+`selftest_audit.sh`); the review kit is push-button reproducible
-kit is push-button reproducible (`run_bare.sh`, self-contained fidelity
+(`run_bare.sh`, self-contained fidelity target);
-target); `acceptIncl`/`acceptCons_sound` route the theorems through the
+`acceptIncl`/`acceptCons_sound` route the theorems through the named
-named acceptance predicates; fidelity = agreement over pinned families
+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,
+How the append was done — release tuple, preflight, candidate-inspection
-explicitly-authorized operator decision, scoped per the runbook.
+gate, and the 12→13 structural rehearsal — is recorded in
+[ATTESTATION-RUNBOOK.md](ATTESTATION-RUNBOOK.md).
 
 | layer | content | status |
 |---|---|---|

docs/optimistic-accountability.md

@@ -1,10 +1,12 @@
 # Optimistic by construction: what the LTL holds, and what it shares with rollups
 
-Status: essay / parked blog-post source. Per the operator's decision,
+Status: published. The condensed blog version is live at
-the blog version publishes only AFTER entry 13 is live (runbook B7),
+blog.zkdefi.org ("The log notarizes itself — entry 13", 2026-07-16),
-when the closing claim — "the log carries kernel-checked proofs of its
+and the closing claim — "the log carries kernel-checked proofs of its
-own machinery" — becomes literally true and the post can end with a
+own machinery" — is now literally true: entry 13 (leaf index 12, hash
-link to a live leaf the reader can verify in one command.
+`8cb258d6…`, subject `ltl-accumulator-verified@172a1d0`) is live under
+head `tree size 13, root 3488a2d0…`, verifiable at
+ltl.zkdefi.org/v1/sth. This essay remains the long-form source.
 
 ---
 
@@ -112,8 +114,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 will carry one for its own — inside the very
+interpreters; this log carries one for its own — entry 13, inside the
-ledger it protects.
+very ledger it protects.
 
 ## Pointers (for the eventual blog rendering)