paper/README.md tells a visitor that ltl.pdf is the submitted version
frozen during review, that v0.1/v0.2 are superseded history, and that
v0.3-v0.9 live in git history. Also corrects the stale web.py comment
that labeled the live pdf 'v0.3 reinvention' (it is the v0.9 submitted
version). No served bytes change; the comment fix reaches the droplet
with the next routine app update.
The estate doc audit scoped itself to *.md and missed the text a site visitor
actually reads: the string constants in webdocs.py. Fixed here, verified by
RENDERING the page from the live 19-leaf state and checking each block:
- The SVG head label reads "Ed25519 + SLH-DSA" when the live head is
dual-signed, "Ed25519" when it is not — computed, not asserted.
- The trust-anchor card now carries BOTH keys the same way: full PEM,
SHA-256 fingerprint, raw endpoint (/v1/log-slhdsa-public-key), mirror
comparison link. The Ed25519 key stays the required anchor; the SLH-DSA
key is the additive post-quantum one, and the card says whose proof
subject its verify path is (leaf 18).
- The registered homepage overclaim (register: homepage-stdlib-claim) is
closed: "stdlib-only" wording replaced with the truth — stdlib hashing,
signature checks shell out to the openssl binary, fails closed without.
- "one signature and ~N hashes" became "one REQUIRED signature (Ed25519;
heads from tree 14 add an additive post-quantum SLH-DSA signature)".
- The paper card is reframed (frozen under review, describes the 16 July
snapshot, "then-thirteen-leaf") and followed by a new reader-guidance
card (operator-ordered): the paper-era prefix is unchanged inside the
live history — leaves 0-12 byte-identical, the paper's head still
head #5 of sth-history — verify.py --all checks both eras at once; the
advances are additive (44-cert re-attestations, leaf 18, dual-signed
heads, ABSENT on older heads by design); and the 3,867 divergence the
paper honestly reports has since been CLOSED (sn==0 fix, 2026-07-23,
pinned count now 0) — both the divergence and the fix are part of the
retained record.
Layout fact the render surfaced: the served log dir must contain the .pub
files (that is what /v1/log-public-key reads); the SLH-DSA pub joins the
Ed25519 one there. Suite 152/0/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
/v1/log-slhdsa-public-key, mirroring /v1/log-public-key exactly: same route
shape, same two-independent-locations TOFU rule (site copy + git mirror
copy). The operator decision of 2026-08-06 required the SLH-DSA public key
published like the Ed25519 key; the mirror half shipped with the tree-19
publication, this is the site half. Suite 152/0/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Nine parallel readers audited every doc against measured ground truth; every
finding was re-verified against the file before any edit, and the sweep fixed
by PROPERTY, not by flag — wording the readers caught in one repo was hunted
in all siblings (the two-button README sentence existed in all four forks,
not the three flagged; likewise the cone-overclaim in TRUSTED-BASE item 1).
This repo: see the diff. Records were not rewritten; clarifications are
dated. Doc-only except where noted in the estate summary; every gated doc
change was followed by a green button run.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The consumer verifier now judges the slh_dsa block on every head. The status
taxonomy is the design decision, so it is spelled out and each arm tested:
ABSENT head predates the second signature — allowed (additive posture,
operator decision 2026-08-06); an append-only log keeps history.
VALID verified against provider.slhdsa.pub.
INVALID present and wrong — HARD FAILURE. A bad signature is never a
degradation.
WRONG-KEY head names a different key than the mirror ships — hard failure.
NO-PUBKEY head claims the signature, mirror ships no key — broken
publication, hard failure.
TOOLING OpenSSL < 3.5 cannot read SLH-DSA keys — honest degradation:
one loud NOTE, never counted as verified, never failed; the
required Ed25519 checks still gate the result.
verify_selftest.py gains two adversarial cases, both mutating a full mirror
copy: one flipped signature byte must fail naming slh_dsa:INVALID; deleting
provider.slhdsa.pub while heads claim the signature must fail NO-PUBKEY. On
mirrors without slh blocks the cases record as not-applicable rather than
silently passing. First selftest run caught my own marker bug — the case
grepped for the stored failure string, which is never printed, instead of
the printed status; the printed line is now the assertion target.
README template: SLH-DSA key row, honesty paragraph (verification proven for
both algorithms, signing for neither; leaves Ed25519-signed at issuance
only), and the hardcoded head size is GONE — the README now names no tree
size at all, so this staleness class dies with the instance (it said "tree
size 13" and would have shipped that under a 19-leaf head).
Template is deliberately ahead of the published mirror until the next
publication, which overwrites the mirror from here (the sync rule's
intended direction for pre-publication work). Proven against the scratch
19-leaf mirror: verify.py --all RESULT OK [full] with ABSENT on heads 8-13
and VALID on 14-19; selftest 13/13 GREEN. Backward compat proven against a
copy of the live 13-leaf mirror: RESULT OK [full], selftest GREEN with the
slh cases n/a. Suite 152/0/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
append_attestation and latest_sth pass the keys to make_signed_tree_head so
every head minted during an append cycle carries the dual signature; publish
ships provider.slhdsa.pub beside the Ed25519 key the moment it exists. All
three parameters optional and defaulting to absent: a caller without SLH-DSA
keys gets exactly the previous behaviour, heads carrying the honest
not-configured slot. Suite 152/0/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Closes the two halves of replay-pipeline-lags-hardened-forks.
(1) The generic replay compiled every .lean under verification/, including the
P1-b kernel-gate instruments (Proofs/Inventory*.lean) that read other modules'
object files via readModuleData and only run inside the button's environment;
it died with "object file does not exist". New RepoConfig.replay_exclude
(globs, per repo, in the config where a reviewer sees them) filters the
compile; every exclusion actually applied is recorded in the attestation's
replay.instruments_excluded, so the LEAF discloses what its replay did not
compile — a silent exclusion here would be the estate's oldest defect class.
The replay checks the certificates; the deeper self-auditing gates are the
repository's own and run there.
(2) The ed25519 profile's default list still carried the 16 pre-hardening
certificates, so a successful replay would have attested 16 and the whole
16->44 point of the re-attestation would have been lost silently. Each fork
entry now carries its own 44 — 27 main + 4 apex + 13 scalar — MEASURED from
the fork's two buttons (CERTS arrays; apex recovered by the same pattern
Phase 3c itself uses), never hand-typed. Correction to the plan on the way
through: the plan said 40; the apex tier makes it 44.
Suite: 152 passed, 0 failed, 0 skipped.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
REAL DEFECT found by the operator-ordered doc-freshness audit:
published_assets.py still carried the PRE-HARDENING fail-open verify.py
and the pre-Tier-2 README as the templates that log-publish drops into
the mirror — the next publish would have silently overwritten the
round-13-hardened fail-closed verifier and the corrected README with
the old versions. Fixed:
- published_assets.py regenerated from the canonical mirror files
(byte-identity verified by round-trip exec), now also carrying
verify_selftest.py; SYNC RULE documented in the module docstring.
- transparency_log.publish() now writes verify_selftest.py too.
- NEW tests/test_published_assets.py pins the security-critical markers
(fail-closed FATAL, RECEIPT_TYPE, verify_receipt, --all receipt
coverage, required fingerprint) so template drift fails CI instead of
shipping.
- test_web_and_witness updated to the hardened verifier's markers —
the published test log now passes FULL signature mode end to end
('RESULT: OK [full]'), a stronger assertion than the old string.
Doc refresh in the same pass:
- llms.txt: thirteen leaves + entry-13 self-attestation + fail-closed
verifier; paper line -> new title, 23 pages, v0.2/v0.1 archives.
- Course (generator + generated 06b notebook): 'the git hash IS the
content hash' -> 'the commit pins the exact source tree';
'irrevocably part of the log every other agent sees' -> 'committed to
the log's signed view, which any agent can compare' (the two Tier-2
scope corrections had never reached the teaching material).
- test_paper_verifiers.py docstring rescoped: its 164k counts are the
archived v0.2 report's citation; the current paper cites the corpus
harness and makes no extensional-equality claim.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Round-15 reconciliation: both reviewers ran the mandated rendered-PDF
gate (all 22 pages each, acts stated). They CONFLICTED on one checkable
fact: GPT found the transport figure's s label on the wrong node (the
computed [4,8) parent instead of the consumed [6,8) proof value); the
Fable reviewer certified 'dashed consumed s over [6,8)'. Adjudicated
against the tikz source: GPT RIGHT — my drawing contradicted its own
caption; Fable's script verified the instance's mathematics but misread
the label placement. Fixed (s -> p67 dashed; q47 -> plain computed
node) and CONFIRMED BY RE-RENDER.
GPT's second blocker also real and fixed: Definition 2(i) claimed
'unique accepted opening' (witness uniqueness) where Game PB proves
leaf-value binding — clause (i) now 'an authentic signed view and a
uniquely determined leaf value at its claimed position'; Appendix A row
aligned ('authentic opening with a position-bound leaf value').
Layout (all confirmed by rendered inspection): figure relocated after
the transport introduction (no longer floats between Theorem 4's
statement and proof); Lemma 4's full statement held together
(samepage); Appendix C given its own page — heading + scope warning +
complete code + Appendix D on p23 (clearpage; 22 -> 23 pages).
GPT optionals adopted: abstract 'one project-specific uninterpreted
SHA-256 boundary axiom'; adaptive-oracle sentence defining Q; corollary
overhead phrasing; PB-vs-mirror bridge sentence in the mapping
paragraph; 'bespoke bar' lead-in dropped; Table 1 ragged-right columns.
Declined with reasons recorded: Lemma-4 sub-case itemization and
renaming the composition theorem (both reviewers' optional-only notes;
churn risk at the frozen gate outweighs gain).
Gate status by the reviewers' own words: Fable round 15 'nothing
blocks' x3 with full evidence discipline; GPT 'after the two
correctness fixes and the three layout fixes ... nothing blocks
submission on correctness or readability grounds' — all five applied
and render-verified. 0 overfull, suite 115 green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Operator-ordered UX audit (full linear read + every page rendered and
visually inspected + both reviewers' 'visually clear' certifications
spot-checked). Scope: no theorem, proof, or scope sentence changed in
meaning.
BUGS FIXED (both missed by both round-12/13/14 reviewers):
- Deployment figure: leaf 11 was CLIPPED to 'clea' by the overlapping
1.3cm 'accumulator' box — box now standard width, label 'accum.'
Verified fixed by render.
- The sentence 'Leaf 12 attests the accumulator corpus at commit' was
split from its hash by a float/page break, stranding the bare commit
after the figure — now wrapped in samepage. Verified by render.
- 'signing- library' hyphenation artifact in §6.3.
READER AIDS (for adjacent-field experts; verifiability up, rigor
untouched):
- Notation summary table (12 rows) at the end of §4, right before the
security analysis that uses every symbol.
- NEW transport figure (now Fig. 2): the 6->8 instance with the opening
path (red), frontier values A,B (blue), consumed proof value (dashed),
kept siblings (orange), and the r0/P0 assembly inset — §5.4's five
pages previously had zero figures. Hand-verified by render;
referenced from the transport-algorithm paragraph.
- 'Games at a glance' table (game/adversary/secrets/wins-by/consequence)
after the §5.4 intro.
- One-sentence reading guide at the top of §5.4.
- 2->3 tie-in after the transport proof (the log's own transition as the
smallest growth case; seam subsection gains a label).
- 'assumption cone' defined at first use (§2.1).
DE-SEDIMENTATION (three review rounds of accreted hedges, reorganized
with all semantic content kept):
- §5.4 intro: one 14-line wall -> four short paragraphs (context /
two levels / non-interactivity), duplicated hardness sentence merged.
- HIST game: definition crisp, commentary moved to a parenthetical.
- Abstract: ~15% tighter (inventory numbers -> '61 human-reviewed
certificates over a single uninterpreted SHA-256 axiom'; run-on
split). All boundary/honesty sentences retained.
22 pages, 0 overfull, suite 115 green. Deployment figure renumbered
2->3 (no numeric figure cross-references existed).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Round-14 verdicts: the Claude reviewer CONCEDED its round-13 FORK
objection in writing ('I WAS WRONG', with the correct reasoning after
attempting the demanded counterexample) and passed everything
('nothing blocks x3') — but its 'chi genuinely encoded in the payload'
certification silently swapped pk out of the tuple, missing exactly
GPT's blocker 1. GPT verified the transport induction branch-by-branch
(sound) and found three real integration blockers, all independently
confirmed here before fixing:
- B1: chi contained pk and was claimed payload-encoded; the deployed
payload does NOT carry the key (it is an external verification
parameter) and the game fixed chi before KeyGen created pk. Now:
chi_enc = (log id, schema/type tags, hash-alg) is the encoded
context; chi = (chi_enc, pk) is set after KeyGen; all game texts
(syntax, injectivity lemma, HEAD, FORK/Ev) rescoped accordingly.
- B2: context scoping propagated to the three sites still stating the
cross-log-flawed form: Definition 2 clause (iii), Proposition 1
(statement + proof), and the Appendix A fork row — plus clause (i)
redefined as opening uniqueness under an authentic view (the
'position-bound' ambiguity), the App-A membership row aligned, and a
NEW App-A row for full-mirror recomputation (verify.py --all).
- B3: the security corollary no longer treats the epistemic
human-ignorance premise as a contradictable assumption. It is now
'Constructive security consequence': explicit feasible winner =>
explicitly given, equally feasible collision finder (stated costs);
HEAD/FORK => one EUF-CMA forgery, no loss; the human-ignorance
reading is an engineering judgment stated as such. Intro sentence
aligned.
Minor round-14 items adopted: kbelow citation corrected to the exact
corpus theorem kbelow_prefix_eq (Consistency.lean:48 — it EXISTS;
GPT's claim that no literally-named lemma exists was wrong, my memory
was right); payload-injectivity proof covers the timestamp string and
is scoped to the specified serializer; HIST chain re-termed
'head values, Merkle-level, authentication is HEAD's job'; transcript-
length cost sentence in Theorem 5; 'strong induction' clause;
DGHS-adaptation positioning sentence ('not a bespoke bar' — worded
'adapt', per GPT round 13's own caution against 'specialization').
21 pages, 0 overfull, suite 115 green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Reconciliation first: the two round-13 reviews CONTRADICT on FORK.
Opus (flagged mid-review as flipped, per operator): 'frame-resistance
unsound as stated' because payloads carry timestamps. GPT: 'the right
EUF-CMA form.' Independent re-derivation sides with GPT: a winning head
needs a VALID SIGNATURE on its never-queried exact payload bytes — a
forgery regardless of timestamp; Opus's no-forgery scenario never
produces the valid signature it presupposes, and its own fix paragraph
concedes the win condition already means exact-payload freshness. Its
real residue (the (n,r)-injectivity parenthetical was a red herring in
that proof) is adopted: the parenthetical is gone, injectivity is now
its own lemma where it belongs.
GPT findings, all verified then fixed:
- Theorem 5 formal error (CONFIRMED): the proof applied transport to
same-size transitions outside the lemma's n0<n1 hypothesis, and the
lemma's last line smuggled that case. Lemma restated for n0<=n1 with
the equal case explicit; HIST proof now case-splits (equal: Ext
forces equal roots, opening carries over; growth: transport).
- Prefix transport (CONFIRMED under-proved; Opus concurs): the frontier
narrative is replaced by a FULL induction over the ConsRec recursion,
with the verifier recursions displayed, the value-equality invariant
(rho = y) threaded exactly as the corpus's extractConsNode analysis
identified, explicit P0 assembly per branch, the no-mismatched-
stopping-points argument (shapes are integer-determined), and the
power-of-two split-stability step credited to the corpus's mechanized
kbelow lemma.
- FORK cross-log framing flaw (CONFIRMED): evidence predicate now
context-scoped — fixed chi = (log id, schema/type, hash-alg, pk)
declared once, encoded in every head; one key running two logs can no
longer be classified as equivocating. Prose corrected to
'issued-message attribution' (no more 'never equivocated' oracle
mismatch).
- HEAD-AUTH game added (CONFIRMED gap): outsider forging one ordinary
head reduces to EUF-CMA; G1's forgery leg is now discharged by an
actual game, closing the network-attacker hole.
- Two-level formalization (CONFIRMED): Definition 3 = collision-
extractable accountability (unconditional, explicit reductions with
stated costs); NEW security corollary = what human-ignorance CR +
EUF-CMA + correct key + fixed context then rule out. Extractability
no longer masquerades as hardness.
- Composition mapping made precise: G1 narrowed to authentic position
binding (HEAD + PB opening-uniqueness; full-list membership is a
system property of the published mirror, said so); G2 split into
syntactic pin rule vs semantic HIST content; monotone-extensions and
payload-injectivity as one-line lemmas; HIST game syntax lists C_i
and 0<=a<b<=k; Adv defined for the two keyed games; PB cost notes
retained intermediates; Rogaway bibitem gains the DOI (211-228
reconfirmed by GPT: Springer/DBLP vs the author's list-page typo).
21 pages, 0 overfull, suite 115 green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
New \S5.4 'Scheme-level games and a composition theorem' (operator
order: third attempt targets an IACR venue):
- Game PB (position binding): two accepting openings of different
leaves at one (m,n,r) -> explicit B_pb outputs a SHA-256 collision
in <= 2(ceil(log2 n)+1) hash evaluations (two-transcript top-down
comparison; 32-byte widths make argument pairs recoverable).
- Lemma (prefix transport): an accepted ConsRec transcript plus an
accepting opening at m<n0 under the NEW head yields a collision or
an assembled accepting opening under the OLD head (frontier
comparison + old-root spine assembly; degenerate power-of-two case
handled).
- Game HIST (local history binding): pin-rule chains + contradictory
openings at any two accepted heads -> collision, by transport
induction + PB. Supplies the multi-step closure at paper level.
- Game FORK: evidence completeness by construction; frame resistance
reduces to EUF-CMA. Win condition deliberately over canonical
PAYLOADS, not heads — a second signature on an already-signed
payload is not an EUF-CMA forgery (SUF/EUF trap caught in the
self-audit pass before integration).
- Policy separation as a deterministic lemma (per GPT B6's own
suggestion), formal Definition 3, and Theorem 7: the construction
is an accountable replay-distribution scheme.
- Fixed-function SHA-256 handled per Rogaway's human-ignorance
treatment (new citation, arXiv-API/DBLP/Springer-verified: VIETCRYPT,
LNCS 4341, pp. 211-228, 2006 — note Rogaway's own page carries a
221- typo): every hash statement is an explicit reduction, the
scheme-level continuation of the named-extractor discipline.
- Games are non-interactive BECAUSE the operator-adversary holds the
signing key (no secrets, no oracles) — stated in the section,
mirroring the deployment's non-interactive verification.
- Honesty anchored: scope remark + new coverage-table row (two-
transcript comparisons and prefix transport are paper-level, not
mechanized); Definition 2 re-badged informal with pointer; DGHS
two-transcript lineage credited in related work.
19 pages, 0 overfull, suite 115 green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
All five GPT blockers, independently confirmed against source before
any edit, plus the real subset of the Opus findings:
- B1/M5: every strict-superset/strictly-more/larger-acceptance-set
claim (5 sites incl. two that wrap across source lines) replaced by
witnessed non-equivalence + pinned-family language; the Remark now
states explicitly that no global inclusion relation is claimed.
- B2: the optimistic-accountability/fraud-proof paragraph is REMOVED
(operator: bloat; GPT: technically wrong — consumers do not accept
by default, and a collision refutes the hash assumption rather than
attributing operator misconduct). The careful long-form analogy
stays in ltl-accumulator-verified/docs/optimistic-accountability.md.
- B3/M7: claim matrix — kernel-observation row split into operator-
CLAIMS (established) vs kernel-ACTUALLY-produced (not
cryptographically established); EUF-CMA/CR added where load-bearing.
- B4: artifact + Appendix C sentences now describe the upgraded
verifier (lean-transparency-log 52179bd: --all covers every
published receipt, binding fields required; 11-case adversarial
selftest GREEN).
- B5: pin-store sketch gains the equal-size/equal-root case via
whole-tree binding.
- M1 detached-signature honesty; M2 abstract axiom-name-sets +
compared-views narrowing; M3 kernel time -> end-to-end replay time;
M4+F4 consumers -> 'Consumer prototypes and version exactness'
(implemented prototype, informal check, explicit non-evaluation
disclaimer); M6 Appendix C listing fails closed on short proofs
(take() guard, verified empirically); M8-partial two alternatives-
table cells + design-taxonomy prose paragraph (also closes Opus F1
orphaned header); M9/F5 single experience report; M10 policy-
separation row in the coverage table; M11 27-line portability
number restored; F2 abstract 'via differential testing'; F3 linking
clause after the consistency theorem; Option-valued notation note
(both reviewers); GPT terminology sentence after Definition 2.
17 pages, 0 overfull, dead-phrase sweep clean. Suite 115 green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Executes the approved reinvention outline, using the round-11 GPT-5.6
draft as base material; the operator remains the author of record and
this pass is the authorial fact-check + completion of that draft. New
title: 'Accountable Distribution of Machine-Checked Correctness
Evidence: A Transparency Model and the Lean Transparency Log' (16 pp).
Old 19-page system report archived byte-identical as v0.2
(paper/ltl-v0.2.{tex,pdf}, served at /paper/v0.2; v0.1 unchanged).
Every factual claim in the draft was verified against the estate before
adoption: 222 inventoried constants + 61 reviewed cones (README:36),
all four fidelity counts, the gap-14 lied-size witness reproduced
empirically (deployed verify_consistency(1,3,R2,R3,P)=True while the
recursive model rejects; honest 2->3 True/True), all four apex theorem
names greped from the dalek repo, the entry-13 scope block now quoted
VERBATIM (was silently trimmed), the new klaus2026 citation confirmed
real via the arXiv API (author order corrected to Klaus, Conejero,
Tolmach), remaining 20 bibitems byte-identical to the F10-verified set.
Author corrections beyond the draft: 'opaque SHA-256 function' ->
uninterpreted/boundary AXIOM (matches axiom sha256 : List UInt8 -> Hash);
STH field list now matches the deployed head (adds type tag); lied-size
mechanism sentence from the gap ledger; six-published-heads (sizes 8-13)
mirror honesty; consumers subsection (warden + Swiss Post family-level
negative) per outline item 7; optimistic-accountability related-work
paragraph per outline item 8; fifteen-gap ledger pointer per outline
item 9; verify.py fail-closed tie-ins in artifact availability and
appendix C; wired the six uncited bibitems (lean4, pnueli, eddsa,
rfc8032, edwards+twisted, easycrypt); certificate listing gains the
deployed 'diagnostics' field. Build: 16 pages, 0 overfull, 0 undefined.
web.py: /paper/v0.2 route + loader. webdocs: paper card rewritten for
v0.3 with both archived versions linked. Suite 115 green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- §5/N1: the '16/16 proven' pill was hardcoded — false for the
accumulator (61 certs). Now computed proven/total from each
component's newest leaf (forks show 16/16, accumulator 61/61).
- §2: 'the only thing you take on trust' → 'sole cryptographic identity
anchor; truth rests on each leaf's stated assumptions' (both the top
card and the download table).
- §3: 'the signature vouches for the code that produced it' → the signed
tree CONTAINS an attestation of the reported signing source; execution
provenance is reported, not proven; provenance fields are unsigned
metadata.
- §9: 'irrevocably part of the log every other customer sees' → this
signed head commits it to THIS view; comparison exposes split views.
- §4.4: witness 'never equivocated' → a retained view that can EXPOSE a
conflicting head; one clone cannot prove no split view.
- §10: 'the git hash is the content hash' → the commit identifies the
committed git tree, not deps/toolchain/artifacts.
- §6: live-site 'twelve-leaf deployment' blurb → 'live deployment'.
Suite 115 green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Found by the entry-13 12->13 rehearsal: build_attestation emitted
subject/environment/replay/certificates but NO scope — the profile's
guarantees/exclusions/deployment_constraints (which carry a repo's
known_status scoped-claim wording and known_exclusions) reached only
the claim card, never the published leaf. So the round-6 requirement
that entry 13's LEAF carry its scoped attestation text was unmet by the
code; a reviewer who checked the claim card saw the wording that the
leaf did not contain. Added a 'scope' block
(guarantees/exclusions/deployment_constraints) to the leaf; pure text,
safe to publish, validator is additive. Two provider tests assert the
block exists and that a repo's known_status/known_exclusions reach it.
Suite 115 passed.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
All six originated from the author's own adversarial read-through:
1. SS9: retrievability decay — leaves whose pinned commits are no longer
distributed (0-7 post-rewrite) decay to historical record.
2. SS4.3: why-a-tree — per-item signatures cannot evidence deletion,
expose forks, or provide pinnable state; dishonesty-evidence, not
scale, is the motivation.
3. SS1: curve/signature crate parenthetical (one implementation).
4. SS8: ~1,800s/fork corroborated by inter-leaf issued_at spacing
(within-run gaps 29m35s-30m40s).
5. SS5.1: git commit ids are hardened SHA-1 — said before a referee
says it.
6. App A box fidelity: logical-vs-canonical order declared; ellipsis
markers inside cert objects and at attestation level (covers
diagnostics + inner schema_version); '(14 more)' -> '(14
certificates elided)'.
Visual inspection: all changed pages (1,5,6,13,15,16,17) plus spill
pages 18-19 read with own eyes; p.19 is a light final page (App D
table), accepted over spacing tricks. 106 tests green, accumulator
untouched. Page-count refs updated (webdocs, llms.txt).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Review A (second Fable instance, delivered via USB, findings re-verified
by me against the tex before adoption; its frontier lemma re-derived from
scratch before applying):
- THE REAL FIX: Lemma 2's hash-fold definition did not cover its own two
uses (Root recomputes only along the leaf's root path; ConsRec bottoms
out at the [0,n0) decomposition and consumes the pinned root, which the
old Steps 1-2 never pinned - incl. the degenerate case where the first
component IS the pinned root alone). Now: folds shaped by a connected
sub-tree S containing the root, children outside S consumed as opaque
inputs, conclusion pins emitted values AND all consumed inputs; Thm 2
names its S; Thm 3 pins the consumed anchor and handles the degenerate
case; Lemma 1's role stated honestly.
- dangling R4/R5 taxonomy labels removed; G3/Prop 2 statements now match
their own veto-proof (deny-only, everywhere); Table 1 caption counts
boundary+standard-three; r1 defined as raw signature bytes (T1's whole
point); Contribution 4 'embedded in every signature' -> 'published
alongside'; Figure 1 redrawn in the exact RFC 9162 shape for n=12;
Solana error-type nit; App D namespace elision noted.
Review B (GPT-5.6, positions defended 2026-07-10, concessions adopted):
- abstract + G2 narrowed to what Prop 1 proves (same-size evidence +
monotonicity), unequal-size split views routed through the public leaf
mirror; residual-trust sentence stated at honest width (checkout, deps,
binding, parsing in the trusted observation pipeline); freshness
declared an availability policy (freeze attacks not prevented);
self-reference verb 'ensures' -> 'enforces and records' + signature
reveals nothing about the producing program; novelty softened to
'we are unaware of'; 25-line/150-line accounting in one breath;
missing-oracle-axiom = refuse-to-classify drift (keeping the oracle
argument); mechanization tone softened; head-encoding reality
documented (versioned canonical JSON w/ log id - system was ahead of
the paper); NEW claim-matrix table (Table 2) decomposing every consumer
conclusion into mechanism + residual assumption, incl. two deliberate
not-established rows.
Open questions from Review A resolved: black_box 27 lines are per-lemma
trusted-base bookkeeping (no published cone contains black_box -
verified); T4 x=0 edge case now stated precisely (roots coincide, set
sign bit rejected per RFC 8032, covered by the iff over extracted code;
Lean sqrt_core handles x=0 explicitly); Cheval pages (DBLP-verified)
restored alongside Review A's DOI.
18 pages, 106 tests green, accumulator untouched (12 leaves).
webdocs/llms.txt page counts updated.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Two Fable-5 inventory agents cross-checked every empirical claim in the
paper against code/deployed log, and every external pointer against the
live internet. Fixes on both sides:
CODE (system brought up to the paper's claims):
- SECURITY: pin-store mutation (incl. permanent poisoning) was reachable
via receipts whose head signature FAILED verification in two of three
consumer paths (attestation.py, cli.py) - an unauthenticated forged
head at the pinned size could poison a consumer's pin forever and
pollute the equivocation-evidence pair with an unverifiable head,
contradicting SS5.4's 'validly signed' precondition and Prop 1.
Both paths now gate the store on a verified Ed25519 head signature
(logclient.py already did). Regression test added.
- Prop 2 made literally true: _normalize_certificate now derives the
cleanliness verdict purely from (observed cone, local allowed set) in
EVERY branch; the operator's axiom_status label is never copied (was
passed through for non-proven certs), missing cone => unverifiable
always. Labels can deny, never grant. Test added.
- webdocs: '/v1/sth-history: every head ever signed' -> 'the published
head history'.
PAPER (claims brought down to reality):
- 'every head ever signed' -> the signed head history since publication
began (heads for sizes 1-7 predate the mirror and were not retained).
- Run-3 bullet: 'independently checkable by diffing the two commit
trees' was no longer reproducible (pre-rewrite objects discarded);
now states the log-internal corroboration (identical cert lists and
cones across leaves 4-7 vs 8-11) and that tree diffs are not public.
- Appendix A leaf block now actually verbatim: scheme
openssl-ed25519, verified_backend serial/u64, real Lean version
(4.30.0-rc2) instead of 4.x.y placeholder, leaf's actual axiom order
(finalize/new/update), machine_protection note quoted, elisions
marked; preamble wording matches.
- Appendix C upstream boundary reordered to check.sh's verbatim order.
- '27 lines - all annotation' -> honest description (axiom-list entries
+ operation reordering from one fork's black_box barrier).
- Prop 2 proof + App A: status label consulted only negatively.
- SS7: provenance fields noted as outside the signed payload; consumer
chain relies on none of them.
- Bibliography: all 20 entries verified against DBLP/RFC-editor - zero
errors; added missing page numbers to 6 entries; thebibliography
width 19->20. All URLs verified public; no PlanetMacro leakage.
17 pages, 106 tests green, accumulator untouched (tree_size 12).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Not size for its own sake; each addition is a definition, proof, figure,
or measurement the genre expects and the rejection implied:
- §2: the signature apex given real depth — the four tiers stated as an
explicit lifting ladder T1-T4 (byte apex -> canonical half-lift ->
injectivity/point-eq via non-square d -> constructive full lift), each
naming the one new mathematical fact; the corpus's actual achievement,
previously an appendix bullet list
- §4: scheme-syntax Definition (KeyGen/Append/ProveIncl/VerifyIncl/
ProveCons/VerifyCons/Verdict) in DGHS style, so the goals name real
algorithms; new subsection making the observation-not-verdict /
requirements-card idea explicit (the system's distinguishing claim)
- §5.3: the consistency verifier DEFINED (recursive ConsRec form),
closing the gap where Theorem 3 previously reasoned about an
undefined verifier — differential-tested == deployed RFC verifier on
5508 cases (honest + 4 mutation classes, n<=256)
- §6: Theorem 3 now a FULL proof (was a sketch), factored through a
shared Lemma 2 (Root binding) that both soundness theorems use
- §8: Figure 1 (the twelve-leaf tree w/ grey failure leaves + 3-run
braces) reinstated and improved; Table 1 (per-fork files/boundary/
diff/hash-shape) replacing a prose paragraph
- App D slimmed to the verbatim Lean theorem-name mapping (no longer
duplicates §2)
Both recursive verifiers regression-tested against deployed code. 102
tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Removal (user decision): paper/ltl-v0.0.{tex,pdf} deleted; /paper/v0.0
route removed; test now asserts 404 for it; /paper/v0.1 stays for
citability and is linked from the docs card.
Audit findings from re-reviewing the last session's work, all fixed:
- Appendix A claimed 'all other fields are verbatim' over elided
placeholder values - reworded to state exactly what is elided vs
verbatim (a paper about exactness cannot say verbatim over an ellipsis)
- LTL docs paper card still described the 4-page v1 (old title, old
scope) - now the revised title, 14 pages, proofs summary, v0.1 link
- llms.txt paper line updated to the revised title
- paper/eprint-submission.md rewritten as the RESUBMISSION kit: new
title/abstract, message-to-editors change note, form-not-email
guidance, author-only checklist
102 tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Paper:
- v2 (12->14pp: appendices) promoted to paper/ltl.tex; v1 kept as
ltl-v0.1.tex, pseudonymous variant as ltl-v0.0.tex (identity-clean)
- filled from verified artifacts: App C (3 verbatim per-fork boundaries:
dalek 11 / hash3 8 / anza 7), App D (real 4-tier ladder + parser
hypotheses; the other agent's 'Tier 3/4' guess corrected), App A (real
leaf 8 structure); §8 now twelve leaves / three runs incl. the
history-rewrite absorption (a live G2 demonstration); §7 self-check
index 4->8; Limitations count fixed; two overfull math displays fixed
- title/author/ORCID unchanged from the revision
Hosting: web.py serves /paper (current), /paper/v0.1 (prior named),
/paper/v0.0 (pseudonymous) - older versions unlisted in the endpoint
index; test added.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The lecture-11 framing where customers actually land: the allowed-axioms
list as a card the customer owns and can rewrite; verdicts re-derived
against THEIR copy; stricter card => itemized gap => relax / walk away /
grow the supply. Links to lecture 11 for the executable walk-through.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Generic mechanism: bare-name PDFs placed in the log directory's site/
folder are served by name, checked LAST in the route chain (can never
shadow an API route), traversal-safe, noindex, and deliberately absent
from the endpoint index and the docs page - the operator decides who
receives a link. Tested: serve, unlisted-in-404, traversal rejected.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The provider public key is the one thing a consumer takes on trust;
hiding it behind /log-public-key inverted the page's priorities. New
'The trust anchor - pin this key' section at the top of the docs page
shows the PEM in full with its SHA-256 fingerprint, the mirror-compare
instruction, and the raw endpoint for scripts. Honest 'missing' card if
a deployment lacks the key. Test asserts the page renders the key.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Socratic audit findings, all verified against artifacts:
- 'zero lines between structurally identical forks' was FALSE: risc0 vs
betrusted differ by 27 lines (all annotation, documenting the risc0
fork's black_box trusted-base entry). Corrected to the true number.
- '~64 Lean files per fork' over-rounded anza's 58. Now '58-64'.
- completeness parenthetical now states both hypotheses (a=-1 square, d
non-square), not just d.
- 'key published in two independent locations' was ASPIRATIONAL: the
site served only a fingerprint. New /log-public-key endpoint serves
the key bytes; docs-page artifact-1 row links both copies; test added.
Verified exactly and kept: 215-line parser diff (FromBytesSpec), 121-line
signature-glue diff (SigApexSpec), byte-identical x4 math files incl. the
carry-telescope file, 11-axiom upstream boundary, 16 certs/leaf, 153-line
mirror verifier, leaf fields (toolchain + machine_protection), all 17 refs.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- Title: 'LTL: Lean Transparency Log'; subtitle now 'Distributing
Machine-Checked Proof Evidence through a Recursively Self-Certifying
Merkle Log' (the log carries the certificates of the code that signs
the log - recursion named, marketing dropped)
- Author: Olaf Horvath, contact Olaf.Horvath@zkdefi.org, single URL
ltl.zkdefi.org (redundant zkdefi.org line removed)
- PDF rebuilt (4 pages), page 1 visually inspected
- title echoes updated: llms.txt, LTL docs-page paper card
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- web.py: /paper (and /paper/ltl.pdf) serve the committed PDF, loaded
once at startup from the repo checkout; listed in the 404 endpoint
index; covered by the web roundtrip test
- docs page: 'The paper' card linking the PDF
- DEPLOY.md: the second witness mirror belongs on a host the operator
does NOT control (a self-hosted mirror adds no equivocation defense)
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- serve/webdocs/cli default to base_path='' (own subdomain, root serving)
- webdocs link builder handles the empty base like web.py already did
- all docs, paper, notebook 06b, and published-mirror README point at
https://ltl.zkdefi.org; DEPLOY.md rewritten for subdomain + redirect
- tests: root mount is the production shape; one test keeps exercising
the path-mounted variant
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The /docs route is now a real landing site (still one self-contained
HTML, inline CSS + inline SVG, zero external assets):
- One-sentence definition up top: what the LTL is and the cost
asymmetry it exists for (one signature + a few hashes in
milliseconds vs hours of theorem proving).
- THE GRAPHIC: the accumulator itself, rendered server-side from the
LIVE log at page load - real leaf hashes, real internal nodes, the
real root and signature. Green leaves are boundary-exact verified
attestations; grey leaves are the historical audit-failure entries,
labeled "kept forever - an append-only ledger does not erase its bad
day". The signature box names the dogfood backend and the provider's
self-inclusion check (the signature vouches for the code; the tree
vouches for the signature's code).
- "What do I download?" - exactly three artifacts, numbered, each with
what-it-is and where: (1) provider.ed25519.pub, the sole trust
anchor, cross-checkable between this site and the GitHub mirror;
(2) the attestation = the claim; (3) the receipt = the proof of
inclusion. Plus the maximal-benefit path: clone the mirror, run
verify.py --all, become a witness.
- Three usage lanes (quick check / zero-install audit / autonomous
agent), the API, and the means / does-NOT-mean cards.
Rendered against the real 8-leaf log and content-asserted in tests'
presence. 54/54 green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Socratic pass over everything this public repo reveals, adversary-first:
- DEPLOY.md no longer names the hosting provider or the server's other
software inventory (that sentence was NEW public information - the
site's front page does not advertise it). It now states its own
redaction policy up front, leads with a Caddy proxy config (matching
what the target site actually fronts with), adds rate-limiting and
proxy timeouts for the stdlib backend, generalizes the second-mirror
section, and gains an explicit key-hygiene section (the signing key
never touches the public server; a compromised box has nothing to
rotate).
- Future attestations stop leaking provider-machine paths: the
machine_protection guard path is recorded repo-relative and the Lean
project dir is recorded in its configured env-var form, never
machine-resolved. (The 12 already-published leaves containing local
home paths are immutable by design - severity assessed low: a local
username on a non-addressable dev box, no credentials - and an
append-only log does not rewrite its history.)
Audited clean: no keys, tokens, or credential-named files anywhere in
git history; no public IPs; loopback-only binds; commit identity is the
owner's long-standing public one. 54/54 tests.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Three synchronized faces of one log - transport orthogonal to trust:
- PUBLISHED GIT MIRROR: log-publish exports the public face (one file
per leaf so git history mirrors log history; the FULL STH history as
the witness channel; per-component attestations + receipts; the
provider public key; a standalone stdlib-only verify.py and customer
README). Live at github.com/saymrwulf/lean-transparency-log (genesis:
8 leaves incl. the honest failed-run entries, dogfood-signed head).
- ONLINE SERVICE (pacta_provider serve): read-only, zero-dependency
HTTP with CT-style endpoints under a base path for
zkdefi.org/lean-transparency-log - /v1/sth, /v1/sth-history,
/v1/sth-consistency?first=N, /v1/proof, /v1/attestation, /v1/entries,
/v1/metadata, /healthz - plus self-contained customer documentation
at /docs (current state, attested components, API, the verify-
without-trusting-this-site path, and the means/does-NOT-mean
boundary). The process never loads private keys: heads are signed
offline; a compromised server can withhold or replay (pinning +
freshness detect both) but never forge. STH history now recorded
append-only by the provider (with a backfill head signed for the
existing log).
- AGENT ONLINE CLIENT: pacta log-fetch (download evidence; explicitly
UNVERIFIED until receipt-verify runs - transport is not trust) and
pacta sth-refresh (fetch head, verify signature, advance the pin via
an online consistency proof from the pinned size; fail closed).
- WITNESSES: pacta witness-audit over a clone of the published mirror
recomputes every prefix root from the public leaves and checks every
historical head + signature - no consistency proofs needed when the
leaves are public. Tampering one published entry trips both the
leaf-hash check and the prefix-root check (tested). verify.py gives
customers the same audit with zero installation.
- DEPLOY.md: the complete server-session checklist for zkdefi.org -
reconstruct the servable log FROM the published mirror (the server
stays in witness trust-position), hardened systemd unit, nginx/Caddy
path routing, Forgejo mirror setup, the provider->world update
cycle, and remote smoke tests.
Validated end-to-end on the REAL log: all 10 endpoints, online-fetched
proof re-verified locally through the dogfood verifier with pinning,
online pin refresh, publish + witness audit green, tamper caught,
standalone verify.py green in the published clone. 54/54 tests.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The dogfood principle now runs in BOTH directions. Agents already
verified signatures through the proven dalek path; now the provider
SIGNS with it too, and proves to itself that the signing code is in its
own log before every signature:
- dogfood binary gains a `sign` mode (seed over stdin, never argv;
ed25519_dalek::SigningKey from the same pinned merkleized workspace).
Honesty ledger unchanged: the library's VERIFY path is
certificate-covered; its signing path is declared trusted base - but
it is the ATTESTED artifact, not an un-attested third implementation.
- sign_payload_ed25519_detailed: signing dispatch mirroring the verify
dispatch; the backend that actually signed is recorded in every
attestation signature block and STH.
- THE SELF-REFERENTIAL CHECK: before signing any tree head, the
provider runs the SAME Merkle inclusion verification an agent runs -
against the very tree it is about to sign - for the newest leaf
attesting the signing library itself, and embeds the result in the
signature block:
signing_provenance:
signing_backend: verified-dalek-serial
signing_library_component: dalek-ed25519-verified
signing_library_source_commit: aa0f6ab...
self_inclusion: verified
signing_library_leaf_index: 4
signing_library_certificates_proven: 16/16
A root signature that names the leaf vouching for the code that
produced it. First-append chicken-and-egg is handled honestly
(self_inclusion: library_not_in_log).
- Evidence refreshed: all four receipts re-issued under dogfood-signed
STHs; the full agent verify loop re-run green.
50/50 tests (new signing roundtrip test, skip-safe where unbuilt).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
pacta's replay invoked `lake env lean` bare - on the reference machine
that is exactly the pattern that once OOM-crashed the host (see the
corpus' POSTMORTEM). New RepoConfig.lean_guard (set for all five repos
in examples/repos.yaml: verification/lean-guard): when configured,
every compile and axiom audit runs `lake env <guard> <file> --root=...`
instead of bare lean - hard memory cap via systemd scope + lean -M,
core pinning, timeout, single-flight lock, free-RAM preflight with the
Guard-3a retry ladder, all tuned via LEAN_MEM_MB / LEAN_MIN_FREE_MB /
LEAN_MEM_WAIT_SEC / LEAN_TIMEOUT / LEAN_MAX_CORES. Provider
attestations now record a machine_protection block naming the guard
(or "UNGUARDED"). Smoke-tested live on the real dalek repo: clamping
trace visible, compile green. 49/49 tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A transparency log without split-view defense is just a signature with
extra steps: the provider could serve one tree to the agent and another
to the world, or roll the log back, and standalone receipt verification
would never notice. The primitives (RFC 9162 consistency proofs) were
already implemented and correct; this closes the loop on the AGENT side.
- src/pacta/sthstore.py: a local STH pin store. Unknown log -> pin
(trust-on-first-use, recorded as such). Same tree size -> the root
must match the pin byte-for-byte; a mismatch is named EQUIVOCATION
and is a hard rejection. Larger tree -> a consistency proof FROM THE
PINNED SIZE is required and verified before the pin advances
(receipts already embed a from-previous anchor; the anchor's root is
itself checked against the pin so a lying anchor cannot bridge a
split view). Smaller tree -> LOG ROLLBACK, hard rejection.
- Freshness policy: --max-sth-age-seconds rejects stale (or
future-dated) tree heads - an old-but-valid STH can hide later
entries.
- Wired into receipt-verify, claims, and agent (--sth-store,
--consistency-proof, --max-sth-age-seconds); evidence records the
pin action; any accountability failure fails the receipt closed.
- Provider: log-consistency --from-size N (serve proofs for pinning
agents whose pin is older than the receipt's embedded anchor) and
log-audit (monitor self-check: recompute the tree, verify the stored
STH and per-entry leaf hashes).
Live drill in this commit's validation: pin-on-first-use -> matched ->
grown-with-proof advance -> a real forged same-size split view REJECTED
with the equivocation diagnostic -> freshness rejection -> clean
self-audit. tests/test_sthstore.py covers pin/match/equivocation,
growth-without-proof, lying consistency anchors, rollback, freshness.
45/45 tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The verified corpus completed its phase 2 on 2026-07-06: every ed25519
fork now carries FOUR button-enforced apex tiers up to the full lift
(accept <=> decompress(R) = [k](-A)+[s]B as points), the complete scalar
layer, and the constructive encoding/decoding chain. pacta was calibrated
to the pre-apex corpus and - worse - had no vocabulary for
boundary-audited certificates: its axiom audit knew only "clean = exactly
the three standard axioms", so the apex tiers would have scored dirty.
New vocabulary:
- Profile.certificate_axioms: per-certificate ALLOWED axiom sets;
expected_axioms_for(cert) resolves each certificate's own boundary.
- RepoConfig.apex_boundary: a simple per-fork key (dalek-wrappers /
hash3 / anza) expanded by the ed25519 profile into the exact
per-tier allowed sets. AUTHORITY NOTE in profiles/ed25519.py: each
repo's check.sh Phase 3b is the enforcement point; if the button and
this table disagree, the button wins.
- run_axiom_audit compares each certificate against ITS allowed set;
deviation in EITHER direction (extra axiom or missing boundary
axiom) is dirty.
New risk reality:
- R4 is now reachable: full four-tier apex + constructive chain +
scalar arithmetic, all proven with cones pinned to their documented
boundaries. R4 always carries explicit residual blockers (SHA-512
oracle, hypothesis-parametric wire parses, translation faithfulness,
no side-channel/build assurance - those gate R5).
- R3 unchanged (arithmetic pair) and now explains exactly which apex
certificates are missing for R4.
Attestation trust model hardened:
- The provider is trusted for its OBSERVATION, never its VERDICT:
axiom_status is re-derived locally from observed_axioms against the
agent's own boundary policy. A provider that labels a dirty cone
"clean" gains nothing; "proven" with no observed axioms is
"unverifiable".
- Partial attestations degrade instead of being rejected: uncovered
certificates stay unproven and the score caps accordingly (an
arithmetic-only attestation still authorizes an R3 library capsule,
never a wallet).
Also: scripts/mini_pytest.py - a dependency-free test runner (tmp_path,
raises, monkeypatch, capsys) for hosts without pytest; examples
regenerated FROM the tool (dalek/anza fixtures now R4, 16 certs; new
full four-tier attestation example); tests updated + new
tests/test_boundaries.py (lying-provider, missing-boundary-axiom,
partial-coverage cases). 40/40 tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
