diff --git a/ATTESTATION-RUNBOOK.md b/ATTESTATION-RUNBOOK.md index 0b34a3b..3e36326 100644 --- a/ATTESTATION-RUNBOOK.md +++ b/ATTESTATION-RUNBOOK.md @@ -215,6 +215,12 @@ 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. --- diff --git a/docs/optimistic-accountability.md b/docs/optimistic-accountability.md new file mode 100644 index 0000000..f1f02ab --- /dev/null +++ b/docs/optimistic-accountability.md @@ -0,0 +1,130 @@ +# 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.