ATTESTATION-RUNBOOK.md

@@ -44,7 +44,7 @@ Agent Appendix at the end. Every step ends in a mechanical check.
 | 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. **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. **No second copy exists** — see step A3b | A3 done; A3b (backup) open |
 | 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" |
 
@@ -115,9 +115,7 @@ throwaway copy is then DELETED (its head was signed with the real key
 over a rehearsal tree — it must never be published or retained; if
 retention is wanted for study, rehearse with a throwaway KEY instead).
 
-### A3b. Back up the signing key — **DONE (operator, confirmed 2026-07-14)**
+### A3b. Back up the signing key (opened 2026-07-12 — the key has NO second copy)
-Completed by the operator; the procedure below is retained as the
-reference for future key-backup refreshes.
 The laptop file is the only copy in existence; a disk failure would
 freeze the log at its current size forever (still verifiable, never
 extendable). Operator-only: create an ENCRYPTED backup (e.g.
@@ -217,12 +215,6 @@ naming. **Check:** SD hashes match the repo files.
   specializations; fidelity = pinned-family testing, extensional
   equality false one-sided; Theorem-3 pinned-pair side condition;
   §10(i)/(v) phrasings) — paper repo, its own commit.
-- Publish the accumulator blog post: source parked at
-  `docs/optimistic-accountability.md` (this repo) — condense to the
-  blog's voice, END WITH A LINK TO THE LIVE LEAF (that is why it
-  waited), operator reviews, then one .md into PersonalCloudServer
-  `blog/posts/`, `build-blog.py`, rsync per its DEPLOY.md. Closes the
-  "one post per public repo" gap for this repo.
 - One-line note in this file: date, leaf hash, head root. Commit.
 
 ---

docs/optimistic-accountability.md

@@ -1,130 +0,0 @@
-# Optimistic by construction: what the LTL holds, and what it shares with rollups
-
-Status: essay / parked blog-post source. Per the operator's decision,
-the blog version publishes only AFTER entry 13 is live (runbook B7),
-when the closing claim — "the log carries kernel-checked proofs of its
-own machinery" — becomes literally true and the post can end with a
-link to a live leaf the reader can verify in one command.
-
----
-
-## Part I — What is actually inside the Merkle tree
-
-A persistent misreading of transparency logs is that they "contain the
-proofs." The LTL's tree contains none of the Lean mathematics. Each
-leaf is (the 32-byte hash of) a **verification-event record**: a
-signed attestation stating that the provider, at a given time, ran the
-proof checks on a named subject repository at an exact commit, with an
-exact toolchain, and observed a specific result — every certificate
-verified, each with an exactly-listed axiom cone. The records are
-published beside the tree (`entries/`); the proofs themselves live one
-hop further away, in the subject git repositories the records pin.
-
-So a leaf is a statement *about the operator's action* — "I verified
-X" — and on its face that sounds like "trust me." The design's whole
-point is the refinement that removes the trust: **the claim names its
-own evidence.** Because the leaf pins commit hash and toolchain,
-anyone can replay the verification and check the operator's statement.
-The log converts
-
-> "I guarantee I verified the proofs (which live elsewhere)"
-
-into
-
-> "I claim this, permanently and publicly, with enough detail that
-> anyone can catch me lying — and I can never unsay it, edit it, or
-> show a different history to someone else."
-
-Three layers, three distinct guarantees, and most confusion comes from
-expecting one layer to do another's job:
-
-| layer | guarantees | does NOT guarantee |
-|---|---|---|
-| Lean kernel (inside the subject repos) | the mathematics of the attested proofs is true, given the declared axioms | anything about what the operator later claims |
-| replay pin (leaf content) | the operator's claim is CHECKABLE — re-run the pinned commit and compare | that anyone has actually re-run it |
-| Merkle accumulator + signed heads | inclusion (Thms 1–2), append-only history (Thm 3), equivocation evidence (Prop 1): claims cannot be altered, hidden, or forked without producing cryptographic evidence | that any claim is TRUE — the ledger notarizes, it does not referee |
-
-The notary metaphor is exact: a notary does not check that your
-contract is wise; the notary makes it impossible to later dispute
-*what was stamped and when*, and the bound ledger makes tampering
-evident. The LTL is a notary whose every stamped page happens to carry
-instructions for independently re-checking the page's claim.
-
-## Part II — The optimistic-rollup resemblance (it is not a metaphor)
-
-Optimistic rollups rest on one bet: *claims are cheap to make and
-expensive to get away with*. A sequencer posts state roots without
-proof; safety comes from anyone's ability to produce a fraud proof
-from public data, and from punishment when they do. The LTL — like its
-direct ancestor, Certificate Transparency (RFC 9162) — is built on the
-same bet: record everything append-only, and make misbehavior generate
-publicly verifiable, transferable evidence.
-
-The fraud-proof analogue exists in the LTL at two distinct layers:
-
-**1. Log-layer fraud (operator rewrites or forks history).** Here the
-resemblance is nearly literal, and it is exactly what this corpus
-mechanized. Theorem 3 (`extractCons_correct` / `acceptCons_sound`)
-states: if the verifier accepts a consistency proof between a pinned
-head and a rewritten history, the named extractor **outputs a SHA-256
-collision as two concrete byte strings**. That is a fraud proof in the
-strict sense — and a constructive one: the adversary's own accepted
-messages are compiled into the evidence against them. Equivocation has
-the same shape: two conflicting signed heads ARE the fraud proof, and
-the consumer's pin-store is the watchtower that collects them. Even
-the rollup's liveness assumption transfers: someone must actually
-watch (a pinned consumer, a mirror, a `witness-audit` run). An
-unwatched log, like an unwatched rollup, is safe only on paper.
-
-**2. Claim-layer fraud (a leaf's content is a lie).** The log does not
-validate Lean proofs on append — it records the claim. That is the
-optimistic part. The fraud proof here is **replay**: the leaf pins
-everything needed to re-run the check, and the failed replay is the
-demonstration. Two properties compare favorably with rollups: the
-challenge window is *infinite* (append-only preserves the crime scene
-forever — a false leaf cannot be reverted, only exposed, and its
-permanence is the exposure), and no adjudicator is needed — the fraud
-proof is reproducible by every reader independently.
-
-**Where the analogy honestly stops: enforcement.** A rollup's fraud
-proof triggers protocol-native consequences — state reverts, bonds are
-slashed, money moves. The LTL has no bond, no slashing, no revert.
-Evidence leads to out-of-band consequences (consumers stop trusting;
-the evidence is publicized), exactly as in CT, where the "slash" is a
-browser distrusting a CA. Same detection architecture, different
-enforcement layer: cryptographic accountability with reputational
-rather than economic stakes. Bolting on economic slashing would
-require on-chain adjudication of "the Lean replay failed" — a
-fraud-proof VM able to run a proof checker; theoretically the same
-construction rollups use, practically a research program. The
-pragmatic dual, implemented in this estate, is consumer-side defense:
-warden's quorum of independently attested verifiers, instead of
-prover-side bonding.
-
-**The inversion worth savoring.** Rollup design treats "optimistic +
-fraud proofs" and "validity proofs" as competing answers for the same
-object. This stack uses both, one inside the other: each leaf's
-*payload* is validity-proven in the strongest available sense (the
-Lean kernel — no optimism, no challenge window), while the *envelope*
-carrying it is optimistic/accountability-style. And entry 13 closes a
-loop that optimistic rollups themselves aspire to and largely lack:
-**formally verified fraud-proof machinery**. The mechanized theorems
-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
-ledger it protects.
-
-## Pointers (for the eventual blog rendering)
-
-- 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,
-  where equivocation-evidence transferability lives).
-- Deployed anatomy: leaf → `entries/NNNNNN.json`; head →
-  `latest-sth.json` (+ `sth-history.jsonl`); the head is signed by the
-  dogfooded verified-dalek backend (`self_inclusion: verified`).
-- Lineage: RFC 9162 / Certificate Transparency — the original
-  accountability-over-validity system; the LTL is CT's discipline
-  applied to formal-verification claims.