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>
R6-B1 (Claude, executed end-to-end): provenness was decided by a
WHOLE-OUTPUT 'no axioms' sentence, so an axiom-free certificate whose
line was entirely absent still scored proven+clean ([]==[]). The
reviewer drove a doctored 60-line output through the real gate and got
61/61 with domsep never audited. Classification is now extracted into
classify_certificates(): proven iff the certificate's OWN anchor was
parsed (axiom-free anchors populate []); absent certs are
unknown/failed + not_checked — never clean. This also fail-closes the
typo'd-future-cert case (R6-C2).
GPT §6: parse_axiom_output is now RECORD-scoped — anchors delimit
records, a cone bracket is accepted only inside its own record, missing
or truncated brackets yield MISSING (fail closed) instead of borrowing
the next certificate's bracket, and cones may wrap arbitrarily (the
old fixed 16-line window was a latent overflow for the 11-axiom
ed25519 apex cones on this estate). Anchor names are captured between
the exact quotes Lean prints.
Six new regression tests (absent-axiom-free-not-clean, missing-bracket
no-steal, truncated cone, >16-line wrap, duplicate anchor, interleaved
diagnostics). Suite: 114 passed / 0 failed.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Rehearsed end-to-end 2026-07-16 (throwaway key + throwaway log):
compile via the corpus's lean-guard, 61/61 certificates proven with
byte-exact cones (post parser fix 34a0457), append, publish,
witness-audit ok. kind merkle_accumulator uses the generic profile —
everything comes from this entry: the 61 fully-qualified certificates
with per-certificate cones (generated from the corpus's CONES table),
the nine Proofs.* axiom_imports (required — without them the generated
audit file has no imports and lean-guard rejects it), and known_status
carrying the REQUIRED scoped attestation wording (runbook B2 gate /
round-4 GPT §11): the mechanized model is verified; deployed
consistency correspondence relies on the unmechanized authentic-pair
invariant (KNOWN-GAPS 14/15).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Found by the entry-13 rehearsal (the accumulator corpus is the first
subject with axiom-free certificates — every fork certificate carries
at least the boundary axiom, so this path was never exercised):
- an axiom-free certificate ('X' does not depend on any axioms) was
parsed by opening a 16-line window and taking the first bracket in
it — which belongs to the NEXT certificate. domsep/Hash/
instDecidableEqHash/take_append_drop were reported with their
neighbors' cones and flagged dirty.
- certificate names were matched as bare substrings, so 'Foo' could
anchor on the line for 'Foo_bar'. Now anchored on the exact quoted
name Lean prints.
The no-axioms decision is now made on the anchor line itself, before
any window. Two regression tests added (steal-next-cone, exact-name);
suite 108 passed / 0 failed.
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>
The editor-correspondence kit does not belong in the public artifact repo.
Path gitignored to prevent re-adding. History purge follows.
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>
Makes the paper's pin-store safety proposition true in the deployed code:
- the full signed STH is retained at pin and at each advance (not just
size+root), so on equivocation both conflicting heads are transferable,
signature-verifiable evidence;
- any equivocation (same-size root mismatch, or a consistency anchor
disagreeing with the pin) persists poisoned=true with both signed
heads and refuses ALL further operations for that log, restart-proof
and independent of the update flag;
- rollback unchanged. 102 tests (was 100): poison persistence, evidence
transferability, full-head retention.
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>
Consolidates the consumer-side trust framing that was scattered across
notebooks 05/06b and WALLET.md into one on-ramp: the allowed-axioms list
as a requirements card you own and can write yourself; measurement vs
publication vs judgment (operator/log/you); the three honest outcomes
when your card is stricter than the supply (relax itemized / walk away /
grow the supply). Executable: a self-written card is shown to equal the
real APEX_BOUNDARIES cone exactly (supply == wish: True), and a strict
no-oracle card is REFUSED with the real SHA-512/wire gap itemized.
Registered in course map + notebook test; 101 tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The bundled offline-showcase evidence now pins the current repository
commits (dalek 33fb8bb, anza 25b73f1, risc0 d3318b6, betrusted 7b9ef53)
and their fresh receipts (log tree_size 12). R4 gate verified to open on
it; 100 tests green.
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 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>
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>
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>
Correctness:
- ledger: single-flight fcntl lock over read-modify-append + fsync. Two
concurrent writers previously could fork the hash chain (read same tail,
same prev_hash). New test races 8 threads x6 appends; chain stays intact
with contiguous indices.
- small-order list: the order-8 encodings were hand-typed and unverifiable
and diverged from the canonical libsodium blocklist. A BOGUS entry is the
only dangerous direction (it down-grades a real tamper to a note, skipping
the latch), so the list is now the certain-low-order set only (y in
{0,1,-1}, reduced/non-reduced, both sign bits); order-8 edges escalate to
tamper until a derived list lands. Fail-safe asymmetry documented + tested.
- freshness: removed a tautological .
Non-functional:
- quorum members now run concurrently (ThreadPoolExecutor): a verify costs
one member's latency, not the sum (~17ms for 4 members, live).
- Wallet.quorum() memoized per state_dir: binary swap-detection hashes run
once at assembly, not on every verify; documented rationale.
85 tests green; live 4-fork wallet re-verified end-to-end.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Self-contained dark-theme product page: the one idea, the trust-posture
asymmetry, the firewall diagram, the four deployment profiles, and the
non-claims. Also published as an artifact.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
pacta wallet init/status/card/verify-ledger and the stdio MCP server
all confirmed working end-to-end against the four-fork R4 wallet.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- walletmcp.py: stdlib stdio JSON-RPC MCP server; 7 outcome-first tools
with strict schemas; errors are structured (code/missing/remediation),
never prose; results carry evidence (structuredContent)
- custodycard.py: A2A-style card sharpened to self-proving - embeds each
member's LTL inclusion proof + STH so a counterparty recomputes trust
instead of believing it; proof-of-posture nonce challenge returns a
firewalled, signed posture attestation with the full quorum trail
- cli.py:
- verified end-to-end on the live wallet: all 7 MCP tools, structured
refusal on bad input, and a counterparty recomputing all 4 inclusion
proofs + STH signatures from the card alone (no operator trust)
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- Wallet.init is the R4 gate in executable form: per member, the built
binary's source commit must match an attestation whose verdicts are
re-derived locally, scored >= R4, and Merkle-bound to a verified STH
under the log key (explicit --trusted-provider required, never inferred)
- append-only hash-chained ledger; latch semantics (tamper => custody
frozen; unlatch is a deliberate operator act recorded with a note)
- outbound: intent envelope bound to payload bytes -> signer (local
dogfood or airgap/Precursor-style outbox) -> quorum firewall; a
rejected self-signature is quarantined, never released, and latches
- refusal receipts: signed machine-actionable artifacts (code, missing,
remediation); unsigned-by-design while latched
- live end-to-end against ltl.zkdefi.org: 4 members R4 (leaves 4-7),
release firewall unanimous-accept, inbound unanimous-accept, refusal
signed, ledger chain verified
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- dogfood/quorum/verify-{dalek,anza,risc0,betrusted}: verify-only crates
built from the pinned proven source workspaces (serial backends pinned
per fork; anza entry is the certificate-covered verify_sha512, not the
default Zebra-lineage verify())
- src/pacta/quorum.py: unanimity-required acceptance, divergence
taxonomy (semantic-edge vs unexplained/tamper), small-order/canonicity
edge flags, per-member provenance sidecars with binary hashes
- live smoke: 4/4 members agree on accept and reject
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 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>
The pacta repository is now public on GitHub. The server's app/ was
re-cloned from it (previously shipped via tar+scp while private), so the
production update path is now pure git pull for both app and published
log - no code shipping. Verified live after the switch: internal healthz
and the public docs site both 200, tree size 8. DEPLOY.md runbook
simplified accordingly.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Deployed from the provider notebook over the dedicated deploy key. The
host runs a compose stack, so the LTL joined it as a read-only container
(read_only: true, :ro volumes, no published ports, compose-network-only)
rather than the host-systemd variant; the domain's Caddy site block
gained a path handle that precedes the existing catch-all, validated in
a throwaway container before reload, with timestamped backups of both
config files. The servable log dir is reconstructed FROM the published
GitHub mirror (the server holds witness-grade data only - no keys).
Live smoke over the public internet from the provider machine: /docs
(the SVG site), /v1/sth, /healthz (tree size 8) all 200; the existing
service on the domain unaffected; and the complete agent flow ran
against the production URL - log-fetch, receipt-verify through the
dogfood verifier with a fresh pin store and freshness policy, and
sth-refresh confirming pin consistency online.
DEPLOY.md now leads with the as-built compose record + update runbook
(reconstruct.py helper installed server-side); the original systemd
variant is kept for docker-less deployments. 54/54 tests.
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>
Completes the piece dropped from the previous commit by a failed patch
anchor. All cells re-executed; 50/50 tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The trust architecture has exactly two roles and the curriculum now
mirrors that split structurally - the conceptual burden is the design,
stated as such to the student:
- 06a THE PROVIDER'S SIDE (singleton). Domain banner in the provider's
voice. The full build pipeline run live in a scratch log made from
the REAL attestations: verify (Lean replay = the leaf-making step,
the only expensive one - the shipped evidence IS its output) -> leaf
(0x00 domain separation) -> tree -> STH signed via the MERKLEIZED
LIBRARY -> the self-inclusion check embedded in the signature block.
A generated SVG draws the student's own tree: leaves, internal
nodes, root, and the signature box, framed in the provider's domain
color. Closes with the singleton-vs-many justification table
(key/cost/obligation asymmetry) and exercises.
- 06b THE AGENT'S SIDE (one of many). Domain banner in the agent's
voice: you own the public key, the evidence files, ~25 lines of
hashing - and explicitly NO Lean. The COMPLETE RFC 9162 inclusion
verifier is implemented from scratch in one cell (hashlib only, no
pacta imports for the core) and run against the REAL dalek receipt
(leaf 4 of 8, three siblings, dogfood-signed root); then the STH
signature, the provider's signing_provenance read and interpreted
(why the agent still re-checks inclusion itself), the pin store, and
an SVG of the real log with the agent's path highlighted against the
grey leaves it never needs. Cost line: ~4 hashes + 1 signature.
- Lecture 06 now routes students into the pair and states the mirror
rule ("if you cannot say which notebook a step belongs to, you have
not understood the step"); lecture 09 records that dogfood now runs
in BOTH directions; course map + README updated.
Every cell of 06a/06b/09 executed against the real evidence before
commit (SVGs render in Jupyter, fail soft in plain exec). One
generation bug found and fixed: a single-backslash \\x00 in the
generator produced a literal NUL byte in a cell. 50/50 tests green
with the notebook inventory at twelve.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
