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>
Responds to the converged positioning diagnosis (GPT-5.6 post-mortem +
round-6 reviewer): inverted structure — trust-decomposition model
first, design-space comparison section, LTL as instantiation, gap
14/15 presented as a located-and-fenced result, entry 13 as Exhibit A
(the only-this-paper claim; rewrite finalizes AFTER the append so the
abstract cites the live leaf). Lists what moves out, venue sequencing
(arXiv then CPP/ITP/SCORED/RWC), and the success criterion (the
thought-experiment polarity flip). Old ltl.tex remains hosted as the
system report; queued wording fixes are absorbed by the rewrite.
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>
Read all 18 rendered pages with own eyes (per author order: never trust
tex->pdf as a given). Found: this portable TeX install's format ships a
broken righthyphenmin (verified: \showhyphens{its} -> 'it-s'), which
produced 'a receipt for a leaf is it-/s index' on p.7. Fixed globally
(\lefthyphenmin=2 \righthyphenmin=3); document-wide rescan shows zero
short-tail breaks. Everything else verified as intended: title block,
narrowed abstract, T1-T4 with x=0 note, Def 1, G1-G3, honest-width 4.4,
ConsRec display, frontier Lemma 2, Thm 2/3, claim matrix (auto-numbered
Table 1, refs consistent), exact 8|4 Figure 1, forks Table 2 caption,
acknowledgments both assistants, all 20 refs w/ pages, App A verbatim
values, App B code block, App C boundary order, App D namespace note.
18 pages, 106 tests green, accumulator untouched.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- Acknowledgments now disclose BOTH assistants: GPT (OpenAI) provided an
adversarial review that shaped the manuscript (it did not develop
corpora/tooling - the acknowledgment stays literally true). The .tex
header already credited Review B publicly; the ack now matches.
- ...signed_tree_head.v1 elision replaced with the real type string
pacta.transparency.signed_tree_head.v1 (matches the live head).
- G2: the public-mirror escape hatch marked witness-dependent (SS9
cross-ref) - closes the loop for a hostile reader.
18 pages, 106 tests green, accumulator untouched.
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>
Adversarial re-read of the security section found three exposition gaps
(no math errors, but the kind a referee pounces on), all fixed:
- Lemma 2 (Root binding): Theorem 3 Step 1 asserted 'every proof node
consumed is genuine', but the lemma's STATED conclusion only mentioned
values F emits, not siblings F consumes. Strengthened case (ii) to pin
the consumed siblings explicitly (it follows from argument-pair
coincidence, now stated, not just proved).
- Theorem 3 Step 3: 'hash-fold over itself' named the wrong object — for
Lemma 2, T_{D1[0:n0]} must be a hash-fold over T_{D0}; justified by
equal size => identical shape, leaf inputs = D1[0:n0].
- §7: 'self-referential without being circular' was asserted; now argued
via the explicit acyclic verification order (pin key -> check sig ->
verify inclusion by hashes -> optionally rebuild+recheck source), no
step consuming its own output.
17 pages, refs resolve, 104 tests green (verifier defs untouched).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Re-auditing the prior (Opus-produced) depth pass adversarially found and
fixed three genuine issues:
1. OVERCLAIM (serious): §5.3 said the consistency verifier was
differential-tested 'on all (n0,n1) with n1<=256' but the script only
SAMPLED sizes (5,508 cases). Ran the genuinely exhaustive test — all
1<=n0<=n1<=256, honest + 4 mutations — 164,224 invocations, and the
inclusion verifier likewise (164,479). Paper now states the true scope
and counts; both are pinned in a new CI test (test_paper_verifiers.py,
104 tests) so the numbers cannot rot.
2. PROOF IMPRECISION: Lemma 2 (Root binding) was applied to ConsRec's
first component, which PASSES THROUGH (no hnode) at some levels and so
is not the hash-fold the lemma needs. Reworked: Lemma 2 now defined
over 'hash-folds' only; Theorem 3 restructured into 3 clean steps that
put only the full-hashing second component through the lemma, then
argue algebraically + one honest-tree collision. Also hoisted Lemma 2
above Theorem 2 and made Theorem 2 invoke it (was inlined), so the
'two theorems share the lemma' remark is now true; deduped the remark.
3. MISLABELED TABLE: Table 1's 'files vs upstream' column actually held
line-diffs against different baselines. Dropped it for clean comparable
columns (files / apex axioms / SHA-512 shape); the diff story stays in
the portability paragraph where each baseline is named.
17 pages, all refs resolve, 104 tests green.
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 LTL does not mechanize cryptographic security proofs (EasyCrypt and
relatives own that bridge, now cited); it bridges the adjacent, mostly
empty gap - type-theory-certified artifacts have no distribution
infrastructure, and cryptographic transparency infrastructure has never
carried kernel-checked mathematics. Fit maintained at 4 pages (bottom
margin 1.95cm, bibliography scriptsize); pages 1 and 4 visually
inspected; 18 references.
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>
Chosen from the shortlist; states the two-traditions loop directly and
drops the jargon. PDF rebuilt (4 pages), page 1 visually inspected.
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>
- 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 real-name + affiliation combination de-pseudonymizes the owner's
other public surfaces; reverted on their notice. History purge of the
prior commit awaits explicit authorization.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Review feedback applied:
- Author: Olaf Horvath.
- New "What the certificates state" block in the introduction - the
actual mathematics the Lean proving is about, kept compact: the
radix-51 denotation, a representative two-clause specification
(value + invariant preservation for mul), the complete twisted
Edwards addition law with the d-non-square completeness fact, and
both apex tiers as single-line equivalences
(accept <=> compress([s]B-[k]A) = R; accept <=> decompress(R) =
[k](-A)+[s]B) with the hash oracle's role stated inline.
- The figure was genuinely broken (leaf boxes overlapped - box width
exceeded spacing - and the annotation collided with a node); this
time it was inspected VISUALLY, not just for build warnings.
Redrawn as a full-width figure*: generous spacing, grey failed-run
leaves labeled "retained forever", bold leaf 4, the dashed
self-certification loop routed through clear space, and the float
relocated in source so it lands on page 3 beside the deployment
section instead of drifting to the references page.
- Held the 4-page line through prose trims (intro paragraphs, related
work, deployment opening) and a compact accept() notation; zero
build errors, one 0.66pt overfull in a bibliography line.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
paper/ltl.tex + built PDF: "LTL: the Lean Transparency Log -
Distributing Machine-Checked Proof Evidence via an Authenticated Data
Structure Signed by Its Own Certified Artifact". Exactly four pages,
two-column, self-contained (embedded bibliography, TikZ figure of the
real 8-leaf log with the self-certifying signature loop).
Structure: intro (the consumption-economics argument), the LTL
(roles, replay-attestation leaves, boundary-exact auditing,
observation-not-verdict, pinning + git witness), the self-certifying
signature (with the honest verify-path/signing-path distinction),
deployment & evidence (the failure leaves as a feature; the full
assumption enumeration; the proof-portability observation with real
divergence numbers), related work (Rekor/CT/PCC/CONIKS/in-toto
engaged head-on; Cheval-Moreira-Ryan as the complementary direction -
"they verify the log; we log the verification"), limitations, and the
next-step agenda (Lean-verified RFC 9162 verifiers with SHA-256
collision resistance as a documented boundary axiom, certificates
entering the log they defend; EverCrypt/verified-Merkle prior art
credited).
Claim discipline verified on the rendered text: zero hype vocabulary,
explicit does-not-establish list, full trusted-base enumeration,
single-operator/TOFU/prototype-scale limitations stated, AI drafting
assistance acknowledged. References verified against the literature
(Sigstore CCS'22, Aeneas ICFP'22, HACL* CCS'17, Fiat-Crypto S&P'19,
EverCrypt S&P'20, in-toto USENIX'19, CONIKS USENIX'15, RFC
6962/9162/8032, Necula POPL'97, Lean 4 CADE-28, Bernstein et al.).
Footnote acknowledges the linear-temporal-logic acronym collision.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
