ATTESTATION-RUNBOOK.md

@@ -24,8 +24,8 @@ Agent Appendix at the end. Every step ends in a mechanical check.
 | **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. |
 | **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`. At execution time: 12 leaves (indices 0–11), head root `bcd15f9d…`, frozen. NOW (post-execution): 13 leaves, head root `3488a2d0…`, entry 13 live. |
+| **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 attestation of the corpus itself. APPENDED 2026-07-16 as leaf index 12 (leaf hash `8cb258d6…`); this runbook is the record of that execution. |
+| **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). |
 
 ## 2a. Release tuple (the single source of immutable identifiers)
@@ -80,7 +80,7 @@ NEW_SIZE         = 13
 | 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) |
-| 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" |
+| 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" |
 
 ---
 
@@ -375,7 +375,7 @@ 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 (the private infra repo's DEPLOY.md
+`git pull` in `app/` is NOT enough (PersonalCloudServer DEPLOY.md
 § "The LTL service").
 ```
 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
@@ -422,7 +422,7 @@ concrete object, not an unbound assertion).
 - 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 the private infra repo
+  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.

KNOWN-GAPS.md

@@ -1,12 +1,5 @@
 # Known gaps and scope boundaries (honest ledger)
 
-**Numbering note (2026-07-19):** "paper §N" references in this ledger
-use the archived system report's numbering ("The Lean Transparency
-Log", https://ltl.zkdefi.org/paper/v0.2), which this corpus was built
-against. The current paper at /paper has a different structure; in
-particular its §5.3/§5.4 are unrelated to the §5.3/§5.4 cited in gap
-14/15 below.
-
 Deliberate, documented, and none silent. Reviewers should verify this
 list is COMPLETE, not merely that the items are acceptable.
 

README.md

@@ -1,11 +1,7 @@
 # ltl-accumulator-verified
 
-Lean 4 mechanization of the security analysis (§6) of the system
+Lean 4 mechanization of the security analysis (§6) of the paper
-report "The Lean Transparency Log" (archived at
+"The Lean Transparency Log" (https://ltl.zkdefi.org/paper): the Merkle
-https://ltl.zkdefi.org/paper/v0.2 — the version this corpus was built
-against; the current paper, "Accountable Distribution of Machine-Checked
-Correctness Evidence" at https://ltl.zkdefi.org/paper, presents these
-results in its §5 and carries this corpus as entry 13): the Merkle
 accumulator's own correctness and soundness theorems, kernel-checked, in
 the same discipline as the four `*-ed25519-verified` subject corpora.
 
@@ -30,8 +26,7 @@ its own **scope** block: what is kernel-checked is the mechanized model
 KNOWN-GAPS 14/15 — the leaf does not claim the deployed verifier is
 formally verified.
 
-All paper-§6/§10 mechanization targets (v0.2 numbering) are
+All paper-§6/§10 mechanization targets are kernel-checked; the audit
-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.

STATEMENT-MAP.md

@@ -1,18 +1,10 @@
 # Statement map: paper §6 ↔ Lean corpus
 
-**Numbering note (2026-07-19):** every paper reference in this map uses
-the numbering of the archived system report — "The Lean Transparency
-Log", https://ltl.zkdefi.org/paper/v0.2 — whose §6 this corpus
-mechanized verbatim and whose §10 scopes the mechanization to items
-i–v. The current paper ("Accountable Distribution of Machine-Checked
-Correctness Evidence", https://ltl.zkdefi.org/paper) presents the same
-results in its §5.1–5.2 under different theorem numbers and cites this
-corpus in its §7.2 coverage table; do not match the numbers below
-against it.
-
 The kernel guarantees every proof below; what a reviewer must vet is the
 **statements** — that each Lean theorem says what the paper's item says.
-This map is the review surface.
+This map is the review surface. Paper = "The Lean Transparency Log"
+(https://ltl.zkdefi.org/paper), §6 and §10 (which scopes the
+mechanization to items i–v).
 
 | paper item | Lean name | file | cone |
 |---|---|---|---|

docs/optimistic-accountability.md

@@ -1,18 +1,12 @@
 # Optimistic by construction: what the LTL holds, and what it shares with rollups
 
-Status: long-form source. Entry 13 (leaf index 12, hash `8cb258d6…`,
+Status: published. The condensed blog version is live at
-subject `ltl-accumulator-verified@172a1d0`) is live under head
+blog.zkdefi.org ("The log notarizes itself — entry 13", 2026-07-16),
-`tree size 13, root 3488a2d0…`, verifiable at ltl.zkdefi.org/v1/sth.
+and the closing claim — "the log carries kernel-checked proofs of its
-
+own machinery" — is now literally true: entry 13 (leaf index 12, hash
-Framing note (2026-07-19): Part II was revised to match the precise
+`8cb258d6…`, subject `ltl-accumulator-verified@172a1d0`) is live under
-treatment used in the paper. The rollup resemblance is a **bounded
+head `tree size 13, root 3488a2d0…`, verifiable at
-analogy**, not a strict claim: the collision extractors are *reduction
+ltl.zkdefi.org/v1/sth. This essay remains the long-form source.
-witnesses* against SHA-256's collision resistance, not on-protocol
-fraud proofs that convict the operator; a fabricated leaf is caught
-only by *off-protocol* independent replay. Earlier drafts overstated
-this ("fraud proof in the strict sense", "cannot fail to convict"); the
-overstatement is corrected here and the paper omits the analogy from
-its body entirely.
 
 ---
 
@@ -58,88 +52,70 @@ contract is wise; the notary makes it impossible to later dispute
 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 (a bounded analogy)
+## 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 compact,
+proof; safety comes from anyone's ability to produce a fraud proof
-transferable evidence of a specific fault from public data, and from
+from public data, and from punishment when they do. The LTL — like its
-punishment when they do. The LTL — like its direct ancestor,
+direct ancestor, Certificate Transparency (RFC 9162) — is built on the
-Certificate Transparency (RFC 9162) — sits at the same design *point*:
+same bet: record everything append-only, and make misbehavior generate
-record everything append-only, and make misbehavior produce publicly
+publicly verifiable, transferable evidence.
-verifiable evidence. The correspondence is a genuine and useful
-analogy, and — this is the part worth getting right — it is an analogy
-with three honest disanalogies, not an equivalence. The precise
-version is what makes it interesting.
 
-There are two very different "faults" a reader tends to conflate, and
+The fraud-proof analogue exists in the LTL at two distinct layers:
-the LTL treats them differently.
 
-**Fault 1 — the operator rewrites or forks the log's own history.**
+**1. Log-layer fraud (operator rewrites or forks history).** Here the
-This is the layer this corpus mechanized, and it is where the
+resemblance is nearly literal, and it is exactly what this corpus
-resemblance is strongest — but the mechanized result is a *reduction*,
+mechanized. Theorem 3 (`extractCons_correct` / `acceptCons_sound`)
-not a courtroom verdict. Theorem 3 (`extractCons_correct` /
+states: if the verifier accepts a consistency proof between a pinned
-`acceptCons_sound`) states: if the verifier accepts a consistency proof
+head and a rewritten history, the named extractor **outputs a SHA-256
-between a pinned head and a rewritten history, the named extractor
+collision as two concrete byte strings**. That is a fraud proof in the
-**outputs a SHA-256 collision as two concrete byte strings**. Read that
+strict sense — and a constructive one: the adversary's own accepted
-statement exactly. It does not say "the operator is guilty"; it says
+messages are compiled into the evidence against them. Equivocation has
-"accepting this would break SHA-256." The extractor is a reduction
+the same shape: two conflicting signed heads ARE the fraud proof, and
-witness: it converts a successful attack on the log's structure into a
+the consumer's pin-store is the watchtower that collects them. Even
-concrete refutation of the hash function's collision resistance. Under
+the rollup's liveness assumption transfers: someone must actually
-the standing assumption that no such collision is feasible, the attack
+watch (a pinned consumer, a mirror, a `witness-audit` run). An
-therefore cannot succeed in the first place — which is a *stronger and
+unwatched log, like an unwatched rollup, is safe only on paper.
-cleaner* guarantee than a fraud proof that convicts after the fact.
-Equivocation is the one place the operator is directly on the hook:
-two conflicting signed heads at the same size, in one log context, are
-transferable evidence attributable to the key holder (this reduces to signature
-unforgeability, not to collision resistance) — the closest analogue to
-a rollup fraud proof against the sequencer, and the consumer's
-pin-store is the watchtower that collects it. The liveness assumption
-transfers cleanly: 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.
 
-**Fault 2 — a leaf's content is simply false** (the operator lies about
+**2. Claim-layer fraud (a leaf's content is a lie).** The log does not
-a Lean result it never actually observed). This is the optimistic part,
+validate Lean proofs on append — it records the claim. That is the
-and it is the honest limit of the whole design: the cryptography does
+optimistic part. The fraud proof here is **replay**: the leaf pins
-**not** catch it. The Merkle machinery faithfully commits and orders a
+everything needed to re-run the check, and the failed replay is the
-false statement exactly as it would a true one — it notarizes, it does
+demonstration. Two properties compare favorably with rollups: the
-not referee. What catches a false leaf is **independent replay**: the
+challenge window is *infinite* (append-only preserves the crime scene
-leaf pins the commit and toolchain, so anyone can re-run the check, and
+forever — a false leaf cannot be reverted, only exposed, and its
-a failed replay is the demonstration. But replay is *off-protocol* —
+permanence is the exposure), and no adjudicator is needed — the fraud
-it is not a challenge transaction the log adjudicates; it is work a
+proof is reproducible by every reader independently.
-third party does with a theorem prover, and the log's only contribution
-is to make the claim precise enough to be replayable and impossible to
-later unsay. Two properties do compare favorably: the challenge window
-is effectively infinite (append-only preserves the record forever — a
-false leaf cannot be reverted, only exposed), and no privileged
-adjudicator exists — every reader replays independently.
 
-**The three disanalogies, stated plainly.** (1) The consistency and
+**Where the analogy honestly stops: enforcement.** A rollup's fraud
-inclusion extractors are reduction witnesses against a cryptographic
+proof triggers protocol-native consequences — state reverts, bonds are
-assumption, not on-protocol fraud proofs against the operator — a false
+slashed, money moves. The LTL has no bond, no slashing, no revert.
-opening refutes SHA-256, it does not by itself prove misconduct. (2)
+Evidence leads to out-of-band consequences (consumers stop trusting;
-Detecting a fabricated *leaf* requires off-protocol independent replay;
+the evidence is publicized), exactly as in CT, where the "slash" is a
-the log defines no challenge transaction, adjudicator, or compact proof
+browser distrusting a CA. Same detection architecture, different
-that a replay observation was fabricated. (3) There is no bond, no
+enforcement layer: cryptographic accountability with reputational
-slashing, no revert: consequences are reputational and out-of-band —
+rather than economic stakes. Bolting on economic slashing would
-consumers stop trusting and the evidence is publicized — exactly as in
+require on-chain adjudication of "the Lean replay failed" — a
-CT, where the "slash" is a browser distrusting a CA. Bolting on
+fraud-proof VM able to run a proof checker; theoretically the same
-economic slashing would require an on-chain adjudicator able to run a
+construction rollups use, practically a research program. The
-proof checker inside a fault-proof VM; theoretically the same
+pragmatic dual, implemented in this estate, is consumer-side defense:
-construction rollups use, practically a research program. The dual this
+warden's quorum of independently attested verifiers, instead of
-estate actually implements is consumer-side defense: warden's quorum of
+prover-side bonding.
-independently attested verifiers, instead of prover-side bonding.
 
-**What entry 13 does close.** Set the analogy aside and state the plain
+**The inversion worth savoring.** Rollup design treats "optimistic +
-fact: the log now carries, as one of its own leaves, a kernel-checked
+fraud proofs" and "validity proofs" as competing answers for the same
-mechanization of the very soundness arguments its accumulator relies
+object. This stack uses both, one inside the other: each leaf's
-on — the extractors, the consistency binding, the per-step pin safety
+*payload* is validity-proven in the strongest available sense (the
-— scoped honestly to the recursive model (not the deployed verifier;
+Lean kernel — no optimism, no challenge window), while the *envelope*
-see `KNOWN-GAPS.md`). Whatever one calls that machinery, its proofs are
+carrying it is optimistic/accountability-style. And entry 13 closes a
-now inside the ledger it protects, verifiable end to end by anyone with
+loop that optimistic rollups themselves aspire to and largely lack:
-a stock toolchain. That is the loop worth savoring, and it needs no
+**formally verified fraud-proof machinery**. The mechanized theorems
-rollup metaphor to be remarkable.
+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
+very ledger it protects.
 
 ## Pointers (for the eventual blog rendering)