saymrwulf/proof-aware-crypto-tooling-agent
1
0
Fork 0
mirror of https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git synced 2026-09-03 19:53:43 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Compare commits

base: saymrwulf:b497b00c732c704b8710c857b88d726cc7d0d186
Branches Tags
saymrwulf:main
saymrwulf:fix/consistency-terminal-check
saymrwulf:vulnerable/sn0-consistency-fd2f6ba
...
compare: saymrwulf:469a9628250252d5e07a1d31eb7894e909f7f466
Branches Tags
saymrwulf:main
saymrwulf:fix/consistency-terminal-check
saymrwulf:vulnerable/sn0-consistency-fd2f6ba

17 commits
b497b00c73 ... 469a962825

Author SHA1 Message Date
mrwulf
469a962825 paper v0.15: the dichotomy named, the question aligned 
Two edits. (1) The alternatives paragraph of section 1 now states the
frame the site opens with, in paper register: each alternative fails on
one of two sides — checking cost stays with the consumer, or it
disappears because belief in a label is demanded — and the primitive
studied occupies the point between. (2) The introduction's italic
question said 'opaque provider verdict' where the abstract says
'label'; aligned to label, consistent with the v0.13 verdict/label
separation. Gate green, 25pp, page 2 eye-checked.
 2026-08-17 13:40:39 +02:00
mrwulf
ca2a59f8a7 site: the one argument opens the page — three sentences, the dilemma and our point between 
Operator order: the top value add as three sentences at the very top.
S1 names the two failure modes every alternative has (cost stays with
you, or belief is demanded); S2 places this site at the unique point
between (proof results as cheap as one signature + a handful of hashes,
without turning them into trust); S3 states the guarantee (permanently
recorded, key-bound, assumption-scoped — never believed, only held
accountable). The what-is-here paragraph follows concretely; the old
cost paragraph is absorbed (say it once).
 2026-08-17 13:27:05 +02:00
mrwulf
7a6499c452 paper v0.14: the full-document eye pass completes the referee round 
Operator order: every page of the PUBLISHED PDF inspected by eye, all
25. The flip surfaced two referee items the v0.13 batch had missed:
(1) the notation summary lacked rows for the consistency proof C and
the flag b (both load-bearing from Theorem 3 through Lemma 4) — added,
with Ext pointing at its defining subsection; the gate rejected the
first, too-wide row (130pt overfull) and the shortened one passed;
(2) the HIST chain length still shared the letter k with the Merkle
split point on facing pages — renamed to ell through the game,
Theorem 5, its proof, and Theorem 8's cost term. Gate green: v0.14,
25pp; pages 8 and 13 re-eyed; suite 156.
 2026-08-17 12:54:08 +02:00
mrwulf
3b13fdbfde paper v0.13: the Green-persona approachability revision 
A referee persona (deep crypto, shallow Lean, no prior drafts) read the
whole paper; all findings applied, ~40 edits, none touching technical
content:
- house terms defined at first use: certificate (in contributions),
  accumulator (= the log's Merkle tree + verifiers), signed view (4.2),
  pin rule/pin-store (named at their definition, 4.3), axiom cone as the
  one canonical synonym, loop-fidelity glossed, facade tied to its entry
  point, scope block named in 3.1, oracles marked 'uninterpreted
  function symbols, not random oracles'
- operator 'verdict' renamed label everywhere (Verdict stays the
  consumer algorithm); fork disambiguated (codebases vs fork evidence)
- notation: declarations T_i -> Theta_i (tier collision), HIST chain
  k kept but challenge scalar -> c and signature bytes -> R-bar
  (k/r_1 overloads resolved); tiers T1-T4 introduced in 6.1 body
- theorem-statement sensitivity: Thm 8 scoped to the recursive
  verifiers in the STATEMENT; Prop 1's 'exhibited' made conditional
  with pointer; Thm 3 carries its honest-pin note; Def 2(iii) gets the
  forgery caveat; Lemma 5 declared a restatement of Prop 2
- ghost references resolved (whole-tree root binding stated in place,
  twice); revision residue purged (Post-submission -> Subsequently
  closed; tense unified; hardened state, guarded replay, KNOWN-GAPS
  explained); 6.2 retitled 'A second instantiation'
- six triple-read sentences rewritten per referee (them-sentence,
  vacuous->trivially-by-counting with real non-vacuity guard wording,
  pin supplier, physical-execution antecedent, bridges-land, App E
  factorization)
- appendices A-D now each cited from the body; App D states its shared
  opaque boundary; FIPS 205 added to the bibliography [23] and cited
- abstract divergence sentence rewritten (divergence not 'boundary',
  past tense, closure named, 'the corresponding log entry')
Gate green: v0.13, 25pp; pages 1/16/25 eye-checked; suite 156.
 2026-08-17 11:53:40 +02:00
mrwulf
8ab1f85556 site polish: the last four coherence fixes (de-numbered claim binding, witness in plain words, R5 out of prose, legend without boundary-exact) 2026-08-17 11:01:05 +02:00
mrwulf
4b45ece97b site: the term-coherence pass — every word defined before use, every table self-describing 
Operator-caught: 'certificate' used before any definition, 'requirements
card' undefined, and the Attested-libraries table headed 'artifact 2 /
artifact 3' — numbers pointing at a DIFFERENT table. Fixed: certificates
defined in the Merkle intro (each leaf = one proof run, a batch of
certificates: one machine-checked theorem with its assumption list);
the requirements card is now 'a short plain-text file listing, by name,
the assumptions you accept'; table headers are self-describing (library
/ claim (attestation) / proof of inclusion (receipt) / certificates
proven); redundant gloss under the table dropped (say it once). My own
fresh re-read on top: 'head' glossed at first use, keys card says
'entry 18' (leaf comes later, at the Merkle mapping), 'Binds artifact 2'
de-numbered, 'become a witness' now plain ('hold the complete history
yourself, rung 1'), 'risk class R5' dropped from prose, the legend says
'every assumption list exactly as declared' instead of 'boundary-exact'.
 2026-08-17 10:58:56 +02:00
mrwulf
6fcaaaee42 site: the one-story card is gone; SHA-512 introduced where it first appears 
The 'Paper and log, one story' card served OUR revision history, not
the reader — removed without replacement. SHA-512 appeared unexplained;
now its first mention says why it exists in assumption lists at all
(the hash inside Ed25519, treated as an assumption, not as proven).
 2026-08-17 10:46:42 +02:00
mrwulf
c5268ef46c site language: 'additive' retired, sibling keys get sibling names 
Operator: 'additive' explains nothing to a newcomer, and Key 2 carried
its full parameter-set name while Key 1 was just 'Ed25519' — unequal
treatment. Now: 'Key 1 — Ed25519, required' / 'Key 2 — SLH-DSA
(FIPS 205), post-quantum'; the second signature is called exactly that,
'the second (post-quantum) signature'; parameter-set precision stays in
the artifacts where it belongs. Same cleanup in the OpenAPI summary and
the CLI help.
 2026-08-17 10:41:18 +02:00
mrwulf
bcbf929045 receipt-verify checks the post-quantum co-signature — the tool now does what rung 2 promises 
Operator-caught: rung 2 demanded both public keys while the shown
command consumed only the Ed25519 one — and the gap was real: pacta had
NO SLH-DSA head-signature check (only the mirror's verify.py had one;
'--require-signatures both' refers to the empty ML-DSA slot). New:
verify_receipt(slhdsa_public_key_path=...) verifies the additive
co-signature fail-closed (absent on pre-14 heads reports absent, not
failed; unavailable OpenSSL fails closed), CLI grows
--slhdsa-public-key, rung 2's command carries the flag and its muted
text explains both checks. Proven against the LIVE log: accepted:true,
slh_dsa:verified, ed25519 on the dogfood backend. New tamper test
flips a signature byte and must be rejected. Suite 156 green.
 2026-08-17 10:29:42 +02:00
mrwulf
fdfe217d57 site css: long hashes wrap on narrow viewports (overflow-wrap:anywhere on code; pre capped at 100%) — no page-level horizontal scroll at any width 2026-08-17 10:04:56 +02:00
mrwulf
42c244374a site rewrite v2 + OpenAPI: the undergrad-first page 
Operator critique, all points: no narrative opener (the page now begins
'This site is a public notary for machine-checked proofs...'); subjects
stated symmetrically and completely (signature-CHECKING code in four
Ed25519 libraries, an SLH-DSA implementation, and the log's own Merkle
machinery — the accumulator leaf was missing before); the redundant
'same thing, in one precise sentence' paragraph is gone; every ladder
rung now labels its preconditions ('You need: ...') before any command
and explains what the command does and what a green result means; no
forward references to the paper before its own section; the key card
opens 'Two keys sign everything in this log' — never again 'This key'
— with Key 1/Key 2 structure; the API box is REMOVED from the page and
replaced the industry-standard way: an OpenAPI 3 document served at
/openapi.json (new route + test), one footer line points to it; the
footer carries no commands; the paper card references rung 1 instead
of dropping a bare command. Suite 155 green.
 2026-08-17 10:02:06 +02:00
mrwulf
6c65a53775 site rewrite: the trust ladder is the page's spine 
Operator order: coherent, precise, accessible — an undergraduate CS
student must understand what the service provides, how to benefit, and
what to DO from each trust angle. The page now opens in plain terms
(what happened, why this site exists), keeps the precise one-sentence
as the second voice, and replaces 'Three ways to use it' with the
FIVE-rung trust ladder: (1) witness — hold the history honest, one
minute; (2) trust the reports, bind the operator — milliseconds;
(3) accept observations, reject judgment — re-derive verdicts from
recorded cones against your own card, the rung most people miss;
(4) replay the proofs yourself — ~30 min/library; (5) rebuild the whole
path — weeks, floor named (kernel/extractors/compiler; no rung 6).
Split-view comparison stated as orthogonal to all rungs. The API box is
demoted to 'For your tooling — the raw API' at the bottom with its
reason for existing stated (machine consumers; pacta builds on it).
All content guards keep their exact phrases; suite 154 green.
 2026-08-16 21:00:18 +02:00
mrwulf
6b16eee940 test: the key-section guard follows the corrected plural heading 
(The guard did its job — the suite was red after the heading fix and my
verification chain swallowed the exit code through a pipe and deployed
anyway. Chain hygiene restored: pipefail on every gate invocation.)
 2026-08-16 20:55:07 +02:00
mrwulf
43d7f00930 site: the key section's heading now matches its content — two anchors, one required, one additive 
Operator-caught logical fallacy: the h2 said 'pin this key' (singular)
and the card said 'sole identity anchor' while the same section
presents a second, additive post-quantum key ('sole' + 'Second anchor'
in one breath). The heading is now plural with the hierarchy stated;
'sole' became 'required' in both places it appeared; and 'exactly three
files' now names the optional fourth (the additive PQ key). Root cause:
the SLH-DSA block was APPENDED to the section in August without
re-reading the section against its own heading — local edit, no
whole-unit re-read.
 2026-08-16 20:47:07 +02:00
mrwulf
51a094182a site SVG: geometry that survives growth — adaptive leaf boxes, self-sizing head box 
Operator-caught, by eye: the accumulator graphic was designed for 8
leaves (fixed 112px boxes, fixed 380px head box) and has been a
shingled overlap since the log reached 19 on 2026-08-08; the head
caption spilled both sides after today's wording grew. Every 'site
verified' since was text-probes — nobody rendered pixels. Fixes:
leaf boxes now size to their span (rich >=100px, compact below, short
names, hash line dropped when narrow); the head box computes its width
from its longest line and carries the caption on two lines; edges
anchor to the actual box top. New regression test renders the tree at
8/19/33 leaves and asserts no two leaf rects overlap and the head
title fits its box. Suite 154 green. Eye-passed locally before deploy.
 2026-08-16 20:22:45 +02:00
mrwulf
2517d79f6e paper v0.12 + estate: one numbering, everywhere — 0-based leaf indices 
Operator order: the leaf-index convention adopted this morning must be
global. Paper1 now says leaf 12 in every place that said entry 13
(intro, contributions, section 7.2, related work, conclusion, artifact
availability, Appendix B retitled 'Deployed leaf-12 scope'); the
ordinal 'thirteenth entry' survives only as a gloss. v0.12, 25pp, gate
green, Appendix B page eye-checked. Site card follows (v0.12; revision
prose de-versioned so it cannot churn), paper/README history extended,
top README says leaf 12/17/18. reinvention-outline moved to the private
control repo earlier this commit-series (moat doctrine).
 2026-08-16 20:04:44 +02:00
mrwulf
24809f8e4d paper: retire the reinvention outline from the public shelf (steering material; retrievable from git history) 2026-08-16 20:00:20 +02:00
11 changed files with 443 additions and 296 deletions
Show stats Expand all files Collapse all files

6
README.md
View file

@ -212,12 +212,12 @@ The log uses:
The deployed instance ([ltl.zkdefi.org](https://ltl.zkdefi.org), The deployed instance ([ltl.zkdefi.org](https://ltl.zkdefi.org),
mirror [`lean-transparency-log`](https://github.com/saymrwulf/lean-transparency-log)) mirror [`lean-transparency-log`](https://github.com/saymrwulf/lean-transparency-log))
is live at **19 leaves** (2026-08-08). Entry 12 (2026-07-16) attests the log's own is live at **19 leaves** (2026-08-08). Leaf 12 (2026-07-16) attests the log's own
accumulator machinery — a kernel-checked mechanization of the log's accumulator machinery — a kernel-checked mechanization of the log's
security analysis ([`ltl-accumulator-verified`](https://github.com/saymrwulf/ltl-accumulator-verified)), security analysis ([`ltl-accumulator-verified`](https://github.com/saymrwulf/ltl-accumulator-verified)),
appended into the log itself and scoped to the mechanized model; entries appended into the log itself and scoped to the mechanized model; entries
13–16 re-attest the four Ed25519 forks at 44 certificates each, entry 17 13–16 re-attest the four Ed25519 forks at 44 certificates each, leaf 17
the accumulator's hardened model, and entry 18 the SLH-DSA verify path — the accumulator's hardened model, and leaf 18 the SLH-DSA verify path —
the log's first post-quantum entry. The the log's first post-quantum entry. The
producer path that generated it now emits a `scope` block into each leaf producer path that generated it now emits a `scope` block into each leaf
(guarantees / exclusions / deployment-constraints), so a leaf carries its (guarantees / exclusions / deployment-constraints), so a leaf carries its

14
paper/README.md
View file

@ -1,12 +1,20 @@
# Which file is current? # Which file is current?
**`ltl.pdf` / `ltl.tex` — the current paper (v0.11, revised August 2026).** **`ltl.pdf` / `ltl.tex` — the current paper (v0.15, revised August 2026).**
The review process concluded in August 2026. v0.10 folded in the The review process concluded in August 2026. v0.10 folded in the
corrections queued during the freeze (the closed consistency-verifier corrections queued during the freeze (the closed consistency-verifier
divergence with its `sn = 0` root cause, replay-harness-integrity divergence with its `sn = 0` root cause, replay-harness-integrity
limitation, claim-matrix row); v0.11 brings the paper up to the live limitation, claim-matrix row); v0.11 brought the paper up to the live
system: the nineteen-leaf dual-signed deployment, the SLH-DSA (FIPS 205) system: the nineteen-leaf dual-signed deployment, the SLH-DSA (FIPS 205)
verify-path instantiation, and its certificate appendix. The verify-path instantiation, and its certificate appendix; v0.12 unified
entry numbering on 0-based leaf indices; v0.13 is the approachability
revision from an external-persona referee pass (house terms defined at
first use, theorem statements carry their own scoping, notation
collisions resolved, FIPS 205 reference added); v0.14 completes that pass after a
full-document eye inspection of the published PDF (notation-table rows
for C and b, HIST chain length renamed to avoid the split-point k); v0.15 names the
two-sided dilemma explicitly in the introduction and aligns the
introduction's question with the abstract (label, not verdict). The
version submitted for review (July 17, 2026, sha256 `7f140356…`) is version submitted for review (July 17, 2026, sha256 `7f140356…`) is
preserved unchanged in this repository's git history. The live copy at preserved unchanged in this repository's git history. The live copy at
<https://ltl.zkdefi.org/paper> serves the current revision. <https://ltl.zkdefi.org/paper> serves the current revision.

BIN
paper/ltl.pdf
View file

Binary file not shown.

218
paper/ltl.tex
View file

@ -48,7 +48,7 @@ showstringspaces=false,breaklines=true,xleftmargin=.5em,xrightmargin=.5em}
\large A Transparency Model and the Lean Transparency Log} \large A Transparency Model and the Lean Transparency Log}
\author{Olaf Horvath\\ \author{Olaf Horvath\\
\small Olaf.Horvath@zkdefi.org \quad ORCID 0009-0004-8008-5805} \small Olaf.Horvath@zkdefi.org \quad ORCID 0009-0004-8008-5805}
\date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.11}} \date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.15}}
\begin{document} \begin{document}
\maketitle \maketitle
@ -82,11 +82,12 @@ project-specific uninterpreted SHA-256 boundary axiom) and, as its newest
entry, eleven certificates over the SLH-DSA-SHA2-128s verifier. Since tree entry, eleven certificates over the SLH-DSA-SHA2-128s verifier. Since tree
size 14 every signed head additionally carries a deterministic SLH-DSA size 14 every signed head additionally carries a deterministic SLH-DSA
co-signature --- produced with the parameter set whose verification path the co-signature --- produced with the parameter set whose verification path the
log itself attests. The mechanization effort also exposed, log itself attests. The mechanization effort also exposed, via
via differential testing, a nontrivial implementation boundary --- the differential testing, a nontrivial model/implementation divergence --- on
deployed iterative consistency verifier is not extensionally equal to the malformed size claims, the deployed iterative consistency verifier was not
recursive model on malformed size claims --- and the leaf records this extensionally equal to the recursive model proved in Lean (since closed;
limitation explicitly. The contribution is a cryptographic distribution this paper reports the pre-closure measurements) --- recorded explicitly
in the corresponding log entry. The contribution is a cryptographic distribution
model for machine-checked correctness evidence, with an end-to-end deployed model for machine-checked correctness evidence, with an end-to-end deployed
instantiation that carries scoped proofs about its own accountability instantiation that carries scoped proofs about its own accountability
machinery. machinery.
@ -111,7 +112,7 @@ This creates a problem that is logically downstream of proof construction:
\begin{quote} \begin{quote}
\emph{How can a consumer that cannot execute the prover obtain precise, \emph{How can a consumer that cannot execute the prover obtain precise,
accountable evidence about a proof replay, without collapsing the result into accountable evidence about a proof replay, without collapsing the result into
an opaque provider verdict?} an opaque provider label?}
\end{quote} \end{quote}
A detached signature on the word ``verified'' authenticates an issuer but does A detached signature on the word ``verified'' authenticates an issuer but does
@ -122,7 +123,10 @@ portability objective. Committees distribute trust but do not themselves fix
the semantics of the attested result. Succinct proofs of verifier execution the semantics of the attested result. Succinct proofs of verifier execution
would provide validity rather than mere accountability, but require a circuit or would provide validity rather than mere accountability, but require a circuit or
verified-VM representation of the prover and are not yet the deployment verified-VM representation of the prover and are not yet the deployment
assumption of the artifacts studied here. assumption of the artifacts studied here. Each alternative thus fails on
one of two sides: the cost of checking stays with the consumer, or it
disappears because belief in a label is demanded. The primitive studied
here occupies the point between.
We therefore study a narrower primitive: \emph{accountable delegation of We therefore study a narrower primitive: \emph{accountable delegation of
deterministic proof replay}. The operator still observes the replay. The deterministic proof replay}. The operator still observes the replay. The
@ -146,8 +150,10 @@ The Lean Transparency Log (LTL)\footnote{The acronym collides with linear
temporal logic~\cite{pnueli}; we note the collision once and rely on context.} temporal logic~\cite{pnueli}; we note the collision once and rely on context.}
is the complete instantiation evaluated in this paper. Its subjects are four is the complete instantiation evaluated in this paper. Its subjects are four
Rust Ed25519 codebases with Lean~4~\cite{lean4} certificates against extracted Rust Ed25519 codebases with Lean~4~\cite{lean4} certificates against extracted
models. Its thirteenth public leaf attests the Lean corpus models. Leaf 12 --- its thirteenth entry --- attests the Lean corpus
that mechanizes the log's own accumulator arguments. Thus the paper's central that mechanizes the security arguments of the log's own Merkle accumulator
(the tree of \S\ref{sec:construction} together with its inclusion and
consistency verifiers). The paper's central
claim survives replacement of Lean, Ed25519, or RFC~9162 by other components; claim survives replacement of Lean, Ed25519, or RFC~9162 by other components;
what is essential is the distribution and accountability model. what is essential is the distribution and accountability model.
@ -169,9 +175,9 @@ those observations with their own policy; operator labels can veto but cannot
grant acceptance. We state clearly that axiom-name equality is not semantic grant acceptance. We state clearly that axiom-name equality is not semantic
identity of theorem statements. identity of theorem statements.
\item \textbf{A deployed cryptographic case study.} \item \textbf{A deployed cryptographic case study.}
The log contains nineteen leaves: three four-fork replay generations for the The log contains nineteen leaves: three replay generations across the four
Ed25519 codebases (the newest at 44 certificates per fork), two attestations Ed25519 codebases (the newest at 44 certificates per fork; a \emph{certificate} throughout this paper is one theorem's kernel-checked proof together with its recorded axiom cone), two attestations
of the accumulator's own Lean corpus (entry 13 carries an environment-derived of the accumulator's own Lean corpus (leaf 12 carries an environment-derived
audit inventory of 222 compiled constants, 61 human-reviewed certificate audit inventory of 222 compiled constants, 61 human-reviewed certificate
cones, and a single uninterpreted SHA-256 axiom; leaf 17 re-attests the cones, and a single uninterpreted SHA-256 axiom; leaf 17 re-attests the
hardened state), and --- as leaf 18 --- the log's first post-quantum subject: hardened state), and --- as leaf 18 --- the log's first post-quantum subject:
@ -183,7 +189,7 @@ verifier and the recursive model proved in Lean are not extensionally equal:
there are malformed size/root combinations accepted only by the deployed there are malformed size/root combinations accepted only by the deployed
verifier. We characterize 3,867 divergences in 73,573 pinned boundary tests verifier. We characterize 3,867 divergences in 73,573 pinned boundary tests
--- every one deployed-accepts-only --- and scope the public attestation --- every one deployed-accepts-only --- and scope the public attestation
accordingly. (Post-submission closure, July 2026: the divergence was traced to accordingly. (Subsequently closed: the divergence was traced to
the deployed verifier omitting RFC~9162 \S2.1.4.2 Step~7's terminal the deployed verifier omitting RFC~9162 \S2.1.4.2 Step~7's terminal
$sn=0$ condition; restoring that one conjunct removes every divergence in the $sn=0$ condition; restoring that one conjunct removes every divergence in the
pinned family, confirmed by a three-way regression against an independent pinned family, confirmed by a three-way regression against an independent
@ -197,16 +203,18 @@ binary correspondence, compiler correctness, extraction faithfulness,
side-channel resistance, SHA-512 correctness, or execution provenance of the side-channel resistance, SHA-512 correctness, or execution provenance of the
signing binary. The present leaf schema identifies theorem declarations by signing binary. The present leaf schema identifies theorem declarations by
repository commit and name, not by a canonical digest of their elaborated Lean repository commit and name, not by a canonical digest of their elaborated Lean
types. These are explicit boundaries, not hidden qualifications. types. These are explicit boundaries, not hidden qualifications
(Appendix~\ref{app:matrix} tabulates every consumer-facing claim with its
establishing mechanism and remaining assumption).
\section{The distribution problem}\label{sec:problem} \section{The distribution problem}\label{sec:problem}
\subsection{Three evidence modes} \subsection{Three evidence modes}
Let a subject repository at commit $g$ contain theorem declarations Let a subject repository at commit $g$ contain theorem declarations
$T_1,\dots,T_q$. A deterministic verifier execution produces an observation $\Theta_1,\dots,\Theta_q$. A deterministic verifier execution produces an observation
$O_g$ containing success/failure and the reported assumption cone of each $O_g$ containing success/failure and the reported \emph{axiom cone} (synonymously, the observed axiom-name set) of each
$T_i$ --- the set of axioms the checked proof of $T_i$ ultimately rests on. There are three natural ways to consume this result. $\Theta_i$ --- the set of axioms the checked proof of $\Theta_i$ ultimately rests on. There are three natural ways to consume this result.
\begin{description}[leftmargin=1.5em,itemsep=4pt] \begin{description}[leftmargin=1.5em,itemsep=4pt]
\item[Direct replay.] The consumer reconstructs the verifier environment and \item[Direct replay.] The consumer reconstructs the verifier environment and
@ -293,7 +301,8 @@ A replay attestation $a$ contains at least
\] \]
where $N_i$ is a declaration name, $s_i$ is replay status, and $A_i$ is the where $N_i$ is a declaration name, $s_i$ is replay status, and $A_i$ is the
observed axiom-name set. The deployed schema additionally carries diagnostics, observed axiom-name set. The deployed schema additionally carries diagnostics,
resource controls, scope, and exclusions. resource controls, a machine-readable \emph{scope block} (the deployed
leaf-12 instance is quoted verbatim in Appendix~\ref{app:entry13}), and exclusions.
\begin{definition}[Attestation-transparency scheme] \begin{definition}[Attestation-transparency scheme]
An attestation-transparency scheme is a~\mbox{tuple} An attestation-transparency scheme is a~\mbox{tuple}
@ -304,7 +313,7 @@ An attestation-transparency scheme is a~\mbox{tuple}
over a hash function and signature scheme. $\mathsf{Append}$ commits the over a hash function and signature scheme. $\mathsf{Append}$ commits the
canonical serialization of an attestation as the next leaf and returns a signed canonical serialization of an attestation as the next leaf and returns a signed
tree head. $\mathsf{Verdict}$ is parameterized by consumer-local policy and tree head. $\mathsf{Verdict}$ is parameterized by consumer-local policy and
does not consume an operator verdict as positive evidence. does not consume an operator label as positive evidence.
\end{definition} \end{definition}
\begin{definition}[Accountable replay distribution] \begin{definition}[Accountable replay distribution]
@ -315,9 +324,10 @@ determined leaf value at its claimed position; (ii) a
consumer accepts a later view only as the same view or a verified extension; consumer accepts a later view only as the same view or a verified extension;
(iii) two valid equal-size heads with unequal roots, in one log and protocol (iii) two valid equal-size heads with unequal roots, in one log and protocol
context, form transferable evidence context, form transferable evidence
that the key holder signed incompatible views; and (iv) positive acceptance of that the key holder signed incompatible views, except under signature
forgery; and (iv) positive acceptance of
a theorem boundary is a function of recorded observations and consumer-local a theorem boundary is a function of recorded observations and consumer-local
policy, not of an operator verdict. policy, not of an operator label.
\end{definition} \end{definition}
The definition is intentionally an accountability property, not a validity The definition is intentionally an accountability property, not a validity
@ -389,8 +399,8 @@ of the operator public key.
The model deliberately does not cryptographically exclude fabricated kernel The model deliberately does not cryptographically exclude fabricated kernel
observations; the same holds when the operator's replay harness is defective observations; the same holds when the operator's replay harness is defective
rather than dishonest. That is a statement about a physical execution on the operator's rather than dishonest. Whether the kernel actually ran as claimed is a
machine. The mechanism instead makes the claimed execution target precise fact about a physical execution on the operator's machine. The mechanism instead makes the claimed execution target precise
enough for a third party to replay. enough for a third party to replay.
\subsection{Consumer goals} \subsection{Consumer goals}
@ -407,7 +417,7 @@ a later view only if it is the same view or a verified extension. Two valid
heads of equal size and unequal roots, in one log context, are transferable heads of equal size and unequal roots, in one log context, are transferable
evidence that the key holder signed incompatible views. Unequal-size forks evidence that the key holder signed incompatible views. Unequal-size forks
require retained history, gossip, or a witness. The transition discipline require retained history, gossip, or a witness. The transition discipline
itself is syntactic, enforced by the pin rule by construction; the semantic itself is syntactic, enforced by the pin rule (\S4.3) by construction; the semantic
content --- an opened position cannot change value across accepted views --- content --- an opened position cannot change value across accepted views ---
is a theorem (\S\ref{sec:games}). is a theorem (\S\ref{sec:games}).
\item[G3: Policy separation.] The operator's positive label cannot make a \item[G3: Policy separation.] The operator's positive label cannot make a
@ -459,15 +469,17 @@ consistency proofs are the RFC~9162 algorithms~\cite{ct2}.
A tree head contains schema-version and type tags, a log identifier, tree A tree head contains schema-version and type tags, a log identifier, tree
size, root hash, timestamp, and hash-algorithm identifier. The canonical JSON serialization of size, root hash, timestamp, and hash-algorithm identifier. The canonical JSON serialization of
those fields is signed with Ed25519. The log identifier and version tag prevent those fields is signed with Ed25519. The log identifier and version tag prevent
cross-log and cross-protocol replay. cross-log and cross-protocol replay. We call the leaf history a head
commits to a \emph{view}, and write \emph{signed view} for that history
as represented by its signed head.
Since tree size 14, every head additionally carries a \emph{deterministic} Since tree size 14, every head additionally carries a \emph{deterministic}
SLH-DSA-SHA2-128s (FIPS~205) signature over the same payload. The SLH-DSA-SHA2-128s (FIPS~205) signature over the same payload. The
co-signature is additive: the Ed25519 signature remains the one every co-signature is additive: the Ed25519 signature remains the one every
consumer must verify, and heads published before size 14 carry no consumer must verify, and heads published before size 14 carry no
post-quantum signature --- the standalone verifier reports them as absent post-quantum signature --- the standalone verifier reports the co-signature as
rather than failing them, because an append-only log keeps the history of absent on such heads rather than rejecting them: an append-only log
its own signature scheme. Determinism is chosen as an audit primitive: a necessarily preserves the history of its own signature-scheme upgrades. Determinism is chosen as an audit primitive: a
deterministic re-sign of the same payload is byte-comparable, so ``same deterministic re-sign of the same payload is byte-comparable, so ``same
input, same signature'' becomes a diff rather than an assurance. The input, same signature'' becomes a diff rather than an assurance. The
co-signature closes a further loop: its parameter set is exactly the one co-signature closes a further loop: its parameter set is exactly the one
@ -491,6 +503,9 @@ same-size fork evidence;
\item larger size: accept iff a consistency proof verifies, then update; \item larger size: accept iff a consistency proof verifies, then update;
\item smaller size: reject as rollback. \item smaller size: reject as rollback.
\end{itemize} \end{itemize}
We call this transition discipline the \emph{pin rule}, and the persisted
pair $(n_{\mathrm{pin}},r_{\mathrm{pin}})$ the \emph{pin-store}.
Freshness is an external availability policy. A persisted pin detects rollback Freshness is an external availability policy. A persisted pin detects rollback
relative to local history; it does not prove that a client sees the globally relative to local history; it does not prove that a client sees the globally
latest signed head. latest signed head.
@ -506,7 +521,8 @@ $D$, $d$, $m$, $n$ & leaf list; leaf bytes; leaf index; tree size \\
$\MTH(D)$;\ $k$ & Merkle root; split point (largest power of two below $n$) \\ $\MTH(D)$;\ $k$ & Merkle root; split point (largest power of two below $n$) \\
$\Path(m,D)$;\ $\Root(v,m,n,P)$ & inclusion path (leaf to root); path refold \\ $\Path(m,D)$;\ $\Root(v,m,n,P)$ & inclusion path (leaf to root); path refold \\
$\mathsf{Open}(d,m,n,P,r)$ & accepting opening: $m<n$ and $\Root(\hleaf(d),m,n,P)=r$ \\ $\mathsf{Open}(d,m,n,P,r)$ & accepting opening: $m<n$ and $\Root(\hleaf(d),m,n,P)=r$ \\
$\ConsRec$;\ $\mathsf{Ext}$ & recursive consistency verifier; pin-rule transition \\ $\ConsRec$;\ $\mathsf{Ext}$ & recursive consistency verifier; pin-rule transition (\S\ref{sec:games}) \\
$C$;\ $b$ & consistency proof; flag: old root is the pinned $r_0$ ($\top$) vs read from $C$ \\
$\Obs_a(c)$;\ $\Policy(c)$ & axiom names recorded in leaf $a$; consumer's allowed set \\ $\Obs_a(c)$;\ $\Policy(c)$ & axiom names recorded in leaf $a$; consumer's allowed set \\
$\chi_{\rm enc}$;\ $\chi=(\chi_{\rm enc},pk)$ & payload-encoded head context; full context with the key \\ $\chi_{\rm enc}$;\ $\chi=(\chi_{\rm enc},pk)$ & payload-encoded head context; full context with the key \\
$h=(n,r,t;\sigma)$;\ $\mathsf{Vf}_{pk}$ & signed head (size, root, timestamp); signature check \\ $h=(n,r,t;\sigma)$;\ $\mathsf{Vf}_{pk}$ & signed head (size, root, timestamp); signature check \\
@ -523,9 +539,10 @@ This section states the consumer-facing arguments in the form used by the Lean
mechanization. The proofs are elementary but explicit: successful false mechanization. The proofs are elementary but explicit: successful false
openings yield concrete SHA-256 collisions rather than appealing to an informal openings yield concrete SHA-256 collisions rather than appealing to an informal
``Merkle trees are secure'' statement. The explicitness is load-bearing: over a ``Merkle trees are secure'' statement. The explicitness is load-bearing: over a
fixed-width hash a bare ``some collision exists'' is vacuously true by fixed-width hash, ``some collision exists'' is trivially true by counting;
counting, so each soundness statement is about a named extractor function, and each soundness statement therefore names an explicit extractor function,
the corpus pins a machine-checked non-vacuity guard for every extractor. and the corpus pins a machine-checked guard that each extractor's output
really is a collision (distinct preimages, equal digests).
\subsection{Inclusion} \subsection{Inclusion}
@ -588,7 +605,9 @@ $|D_0|=n_0\le n_1=|D_1|$, $D_0\neq D_1[0{:}n_0]$, and
\ConsRec(n_0,n_1,C,\top,\MTH(D_0)) \ConsRec(n_0,n_1,C,\top,\MTH(D_0))
=(\MTH(D_0),\MTH(D_1)), =(\MTH(D_0),\MTH(D_1)),
\] \]
$\mathcal{E}_{\rm cons}(D_0,D_1,C)$ returns a SHA-256 collision. $\mathcal{E}_{\rm cons}(D_0,D_1,C)$ returns a SHA-256 collision. (The hypothesis supplies the honest
$\MTH(D_0)$ as the pinned value; \S5.3 measures the deployed flow, which
has no such mechanized supplier.)
\end{theorem} \end{theorem}
\begin{proof} \begin{proof}
The new-root component is a hash fold over the shape of the $n_1$ tree. Compare The new-root component is a hash fold over the shape of the $n_1$ tree. Compare
@ -602,13 +621,16 @@ collision.
\end{proof} \end{proof}
The theorem's hypothesis pins the honest old root $\MTH(D_0)$. The deployed The theorem's hypothesis pins the honest old root $\MTH(D_0)$. The deployed
flow has no mechanized supplier of that pin; the next subsection measures what flow contains nothing mechanized that guarantees the pinned value is the
the iterative verifier does when size claims alone steer its walk. honest old root; the next subsection measures the iterative verifier's
behavior when only the claimed sizes constrain its reconstruction.
\begin{proposition}[Pin-store safety] \begin{proposition}[Pin-store safety]
Assume EUF-CMA security of the head signature and collision resistance of Assume EUF-CMA security of the head signature and collision resistance of
SHA-256. A consumer following the pin transition accepts only a nondecreasing SHA-256. A consumer following the pin transition accepts only a nondecreasing
sequence of sizes whose exhibited leaf lists are prefix-related. Two accepted sequence of sizes; if leaf lists are exhibited for two accepted heads,
they are prefix-related except under collision (see the mapping paragraph
of \S\ref{sec:games}). Two accepted
heads under the same key, in one log context, with equal size and unequal heads under the same key, in one log context, with equal size and unequal
roots are transferable evidence that the key holder signed incompatible roots are transferable evidence that the key holder signed incompatible
views. views.
@ -616,7 +638,8 @@ views.
\begin{proof} \begin{proof}
Rollback is rejected syntactically. At equal size the transition is accepted Rollback is rejected syntactically. At equal size the transition is accepted
only with equal roots; if the two exhibited equal-length leaf lists differed, only with equal roots; if the two exhibited equal-length leaf lists differed,
whole-tree binding would extract a SHA-256 collision, so under collision whole-tree root binding (each root determines its committed leaf list up
to collision) would extract a SHA-256 collision, so under collision
resistance the lists are equal. A larger head is accepted only after a resistance the lists are equal. A larger head is accepted only after a
consistency proof, so non-prefix acceptance yields a collision by the previous consistency proof, so non-prefix acceptance yields a collision by the previous
theorem. Equal-size unequal roots in one log context, with valid signatures, are two theorem. Equal-size unequal roots in one log context, with valid signatures, are two
@ -630,7 +653,7 @@ certificate is a function only of $\Obs_a(c)$ and $\Policy(c)$. An operator
label cannot change a nonconforming observation into a conforming one. label cannot change a nonconforming observation into a conforming one.
\end{proposition} \end{proposition}
\begin{proof} \begin{proof}
The comparison is set equality and takes no positive operator verdict as input. The comparison is set equality and takes no positive operator label as input.
A deployment may conservatively treat an operator failure label as a veto, but A deployment may conservatively treat an operator failure label as a veto, but
a veto cannot grant acceptance. a veto cannot grant acceptance.
\end{proof} \end{proof}
@ -917,9 +940,9 @@ In the smallest growth case $2\to3$ --- the log's own transition in
old tree and $P_0$ is simply the opening's within-prefix tail. old tree and $P_0$ is simply the opening's within-prefix tail.
\paragraph{Game $\mathsf{HIST}$ (local history binding).} \paragraph{Game $\mathsf{HIST}$ (local history binding).}
$\mathcal{A}$ outputs a chain of head values $h_0,\dots,h_k$, transition $\mathcal{A}$ outputs a chain of head values $h_0,\dots,h_\ell$, transition
proofs $C_1,\dots,C_k$ with $\mathsf{Ext}(n_{i-1},r_{i-1},n_i,r_i,C_i)=1$ proofs $C_1,\dots,C_\ell$ with $\mathsf{Ext}(n_{i-1},r_{i-1},n_i,r_i,C_i)=1$
for every $1\le i\le k$, indices $0\le a<b\le k$, an index $m<n_a$, and for every $1\le i\le \ell$, indices $0\le a<b\le \ell$, an index $m<n_a$, and
openings with openings with
$\mathsf{Open}(d,m,n_a,P,r_a)=\mathsf{Open}(d',m,n_b,P',r_b)=1$ and $\mathsf{Open}(d,m,n_a,P,r_a)=\mathsf{Open}(d',m,n_b,P',r_b)=1$ and
$d\neq d'$. $\mathcal{A}$ wins iff everything verifies. (The chain is the $d\neq d'$. $\mathcal{A}$ wins iff everything verifies. (The chain is the
@ -930,7 +953,7 @@ transcripts regardless of provenance.)
\begin{theorem}[History binding]\label{thm:hist} \begin{theorem}[History binding]\label{thm:hist}
There is an explicit algorithm $\mathcal{B}_{\rm hist}$ that, whenever There is an explicit algorithm $\mathcal{B}_{\rm hist}$ that, whenever
$\mathcal{A}$ wins $\mathsf{HIST}$, outputs a SHA-256 collision, using $\mathcal{A}$ wins $\mathsf{HIST}$, outputs a SHA-256 collision, using
$O(k\log n_k)$ hash evaluations. $O(\ell\log n_\ell)$ hash evaluations.
\end{theorem} \end{theorem}
\begin{proof} \begin{proof}
By Lemma~\ref{lem:mono}, $m<n_a\le n_i$ for all $i\ge a$. Walk $t$ from $b$ By Lemma~\ref{lem:mono}, $m<n_a\le n_i$ for all $i\ge a$. Walk $t$ from $b$
@ -943,7 +966,7 @@ at $h_a$ yields two accepting openings of $d\neq d'$ at $m$ under
$(n_a,r_a)$, and Theorem~\ref{thm:pb} extracts the collision. Accepted $(n_a,r_a)$, and Theorem~\ref{thm:pb} extracts the collision. Accepted
transcripts have their RFC-determined logarithmic length --- malformed transcripts have their RFC-determined logarithmic length --- malformed
lengths reject --- so the walk costs at most the evaluations of replaying the lengths reject --- so the walk costs at most the evaluations of replaying the
$k$ transition transcripts and the two openings. $\ell$ transition transcripts and the two openings.
\end{proof} \end{proof}
\paragraph{Game $\mathsf{HEAD}$ (head authenticity).} \paragraph{Game $\mathsf{HEAD}$ (head authenticity).}
@ -989,7 +1012,7 @@ queried to the signing oracle; its valid signature is an existential forgery,
which $\mathcal{B}_{\rm fr}$ outputs. which $\mathcal{B}_{\rm fr}$ outputs.
\end{proof} \end{proof}
\begin{lemma}[Policy separation]\label{lem:policy} \begin{lemma}[Policy separation --- Proposition~2 restated for the scheme package]\label{lem:policy}
For every leaf $a$ and certificate $c$, the verdict computed by For every leaf $a$ and certificate $c$, the verdict computed by
$\mathsf{Verdict}$ equals $[\Obs_a(c)=\Policy(c)]$; it reads no operator $\mathsf{Verdict}$ equals $[\Obs_a(c)=\Policy(c)]$; it reads no operator
label, and acceptance consults the operator's status only as a veto. This is label, and acceptance consults the operator's status only as a veto. This is
@ -1008,11 +1031,11 @@ separation.
\end{definition} \end{definition}
\begin{theorem}[Collision-extractable accountability of the construction]\label{thm:main} \begin{theorem}[Collision-extractable accountability of the construction]\label{thm:main}
The LTL construction --- the RFC~9162 tree, the canonical signed heads of The LTL construction with the recursive verifiers of \S\ref{sec:security}
\S4.2 in their fixed context $\chi$, the pin rule of \S4.3, and the policy --- the RFC~9162 tree, the canonical signed heads of \S4.2 in their fixed context $\chi$, the pin rule of \S4.3, and the policy
verdict of \S\ref{sec:model} --- is collision-extractably accountable, with verdict of \S\ref{sec:model} --- is collision-extractably accountable, with
$\mathcal{B}_{\rm pb}$ ($\le 2(\lceil\log_2 n\rceil{+}1)$ hash evaluations), $\mathcal{B}_{\rm pb}$ ($\le 2(\lceil\log_2 n\rceil{+}1)$ hash evaluations),
$\mathcal{B}_{\rm hist}$ ($O(k\log n_k)$), and the one-forgery reductions $\mathcal{B}_{\rm hist}$ ($O(\ell\log n_\ell)$), and the one-forgery reductions
$\mathcal{B}_{\rm ha},\mathcal{B}_{\rm fr}$ of $\mathcal{B}_{\rm ha},\mathcal{B}_{\rm fr}$ of
Theorems~\ref{thm:pb}--\ref{thm:fork}. Theorems~\ref{thm:pb}--\ref{thm:fork}.
\end{theorem} \end{theorem}
@ -1051,7 +1074,7 @@ operator as first-class adversary, policy separation added.
\begin{remark}[What is mechanized, what is not]\label{rem:gamescope} \begin{remark}[What is mechanized, what is not]\label{rem:gamescope}
The games are stated for the scheme's specified verifiers --- the recursive The games are stated for the scheme's specified verifiers --- the recursive
model whose honest-reference specializations are kernel-checked in entry~13 model whose honest-reference specializations are kernel-checked in leaf~12
(the named extractors and per-step pin safety). The two-transcript (the named extractors and per-step pin safety). The two-transcript
comparisons and the transport induction are paper-level proofs in the same comparisons and the transport induction are paper-level proofs in the same
discipline --- the induction reuses the corpus's mechanized discipline --- the induction reuses the corpus's mechanized
@ -1088,52 +1111,58 @@ per fork --- the log records both generations as separate leaves), covering:
mathematical point equation. mathematical point equation.
\end{itemize} \end{itemize}
The signature apex can be summarized as follows. Let $k$ be the challenge The signature apex is organized as four tiers T1--T4
scalar produced by an opaque SHA-512 boundary and let $r_1$ be the raw $R$ bytes (Appendix~\ref{app:tiers}). Let $c$ be the challenge scalar produced by an opaque SHA-512 boundary and let $\bar R$ be the raw $R$ bytes
from the signature. The corpus separates: from the signature. The corpus separates:
\begin{description}[leftmargin=1.5em,itemsep=2pt] \begin{description}[leftmargin=1.5em,itemsep=2pt]
\item[T1:] acceptance iff the verifier's recomputed compressed bytes equal \item[T1:] acceptance iff the verifier's recomputed compressed bytes equal
$r_1$; $\bar R$;
\item[T2:] those recomputed bytes are the canonical encoding of \item[T2:] those recomputed bytes are the canonical encoding of
$[k](-A)+[s]B$; $[c](-A)+[s]B$;
\item[T3:] canonical encoding is injective on valid curve points; \item[T3:] canonical encoding is injective on valid curve points;
\item[T4:] acceptance iff constructive decompression of $R$ yields \item[T4:] acceptance iff constructive decompression of $R$ yields
$[k](-A)+[s]B$. $[c](-A)+[s]B$.
\end{description} \end{description}
The separation keeps residual assumptions visible. SHA-512 and selected The separation keeps residual assumptions visible. SHA-512 and selected
wire-format interfaces are opaque boundaries at the apex; lower arithmetic and wire-format interfaces are opaque boundaries at the apex; lower arithmetic and
group certificates use the foundational Lean axioms observed in the corpus. group certificates use the foundational Lean axioms observed in the corpus.
\subsection{The SLH-DSA verify path: the method on second terrain}\label{sec:slhdsa} \subsection{A second instantiation: the SLH-DSA verify path}\label{sec:slhdsa}
The second campaign extracts the verification path of SLH-DSA (FIPS~205, The second campaign extracts the verification path of SLH-DSA
(FIPS~205~\cite{fips205},
parameter set SHA2-128s) from a pinned pure-Rust implementation through the parameter set SHA2-128s) from a pinned pure-Rust implementation through the
same Charon/Aeneas route, starting from one monomorphic entry point with the same Charon/Aeneas route, starting from one monomorphic entry point with the
five hash primitives marked opaque at the extraction boundary. The corpus is five hash primitives marked opaque at the extraction boundary. The corpus is
eleven certificates: ten loop-fidelity theorems (chain walking, WOTS eleven certificates: ten \emph{loop-fidelity} theorems --- each stating
recomputation and checksum, XMSS and FORS Merkle ascent, hypertree layering, that an extracted loop computes the same value as a reference recursive
digit/byte plumbing) and an acceptance characterization, fold --- covering chain walking, WOTS recomputation and checksum, XMSS and
FORS Merkle ascent, hypertree layering, and digit/byte plumbing
(Appendix~\ref{app:slhtiers} lists each with its exact cone) and an acceptance characterization,
\code{slh_verify_128s_accepts_iff}: for every message digest, signature, and \code{slh_verify_128s_accepts_iff}: for every message digest, signature, and
public key at these parameters, the extracted verifier accepts exactly when public key at these parameters, the extracted verifier accepts exactly when
the recomputed hypertree root byte-equals the public key's root --- no other the recomputed hypertree root byte-equals the public key's root --- no other
acceptance path exists. acceptance path exists.
The terrain differs from Ed25519 in one structural way, and the leaf says so. The terrain differs from Ed25519 in one structural way, and the leaf says so.
The Ed25519 bridges land in an independent second semantics For Ed25519, each theorem relates extracted code to an independent
($\mathbb{Z}/p\mathbb{Z}$, which the proof library understands without ever mathematical semantics (arithmetic over $\mathbb{Z}/p\mathbb{Z}$,
seeing the extracted code); SLH-DSA verification is hash chains and Merkle formalized with no reference to the extracted code); SLH-DSA verification
nodes all the way down, so the reference folds are built from the same five is hash chains and Merkle nodes all the way down, so its reference
uninterpreted hash oracles (\code{h_msg}, \code{f}, \code{h}, specifications are folds over the same five uninterpreted hash oracles
\code{t_l}, \code{t_len}, modeling the SHA-256 instantiations) that the (\code{h_msg}, \code{f}, \code{h}, \code{t_l}, \code{t_len}, modeling
extracted loops call. Each loop certificate therefore makes the extracted the SHA-256 instantiations --- uninterpreted function symbols in the
logic, not random oracles) that the extracted loops call --- there is no
independent second semantics to land in. Each loop certificate therefore makes the extracted
control flow \emph{visible} --- small, sequential, checkable against the control flow \emph{visible} --- small, sequential, checkable against the
standard's algorithms --- while the reading of fold against FIPS~205 remains standard's algorithms --- while the reading of fold against FIPS~205 remains
a declared human step. The audit enforces every certificate's axiom set a declared human step. The audit enforces every certificate's axiom set
exactly in both directions, and the cone \emph{grows} up the pyramid --- exactly in both directions, and the cone \emph{grows} up the pyramid ---
pure bit arithmetic rests on the kernel alone; the apex carries all five pure bit arithmetic rests on the kernel alone; the apex carries all five
oracles (Appendix~\ref{app:slhtiers}). Scope, stated in the leaf: the proved oracles (Appendix~\ref{app:slhtiers}). Scope, stated in the leaf: the proved
subject is a monomorphic facade whose bridge to the deployed generic verifier subject is a monomorphic facade (the fixed-parameter entry point above)
whose bridge to the deployed generic verifier
is a 137-case differential test; one inner digit-extraction loop carries no is a 137-case differential test; one inner digit-extraction loop carries no
certificate; signing and key generation were never extracted. certificate; signing and key generation were never extracted.
@ -1181,13 +1210,15 @@ Every signed head issued since public mirroring began is retained --- twelve
heads, at tree sizes 8 through 19, dual-signed from size 14 on --- together heads, at tree sizes 8 through 19, dual-signed from size 14 on --- together
with every leaf and receipt, in an append-only Git mirror; a clone with every leaf and receipt, in an append-only Git mirror; a clone
re-verifies the entire log offline with the repository's standalone verifier. re-verifies the entire log offline with the repository's standalone verifier.
The first twelve leaves are three four-fork replay generations. Leaves 0--3 The first twelve leaves are three replay generations across the four
Ed25519 codebases. Leaves 0--3
record a failed audit run and remain permanently visible. Leaves 4--7 record a record a failed audit run and remain permanently visible. Leaves 4--7 record a
clean replay. Leaves 8--11 re-attest rewritten repository histories rather clean replay. Leaves 8--11 re-attest rewritten repository histories rather
than replacing the old leaves. Leaf 12 attests the accumulator's own Lean than replacing the old leaves. Leaf 12 attests the accumulator's own Lean
corpus (\S\ref{sec:deployment}, E3); leaves 13--16 re-attest the four corpus (\S\ref{sec:deployment}, E3); leaves 13--16 re-attest the four
Ed25519 corpora at 44 certificates each; leaf 17 re-attests the accumulator Ed25519 corpora at 44 certificates each; leaf 17 re-attests the accumulator
corpus at its hardened state; and leaf 18 attests the SLH-DSA-SHA2-128s corpus at its hardened state (the same corpus after closure of external
review findings); and leaf 18 attests the SLH-DSA-SHA2-128s
verification path --- the log's first post-quantum subject, and the scheme verification path --- the log's first post-quantum subject, and the scheme
that has co-signed every head since size 14. A leaf whose pinned commit ceases to be that has co-signed every head since size 14. A leaf whose pinned commit ceases to be
distributed decays from a replayable claim to a historical record; consumers distributed decays from a replayable claim to a historical record; consumers
@ -1249,10 +1280,11 @@ path. Heads are dual-signed from size 14 on.}
\subsection{Mechanization coverage} \subsection{Mechanization coverage}
Entry 13 is not a claim that the whole service is formally verified. The Lean Leaf 12 is not a claim that the whole service is formally verified. The Lean
corpus covers the recursive Merkle model, inclusion completeness and corpus covers the recursive Merkle model, inclusion completeness and
collision-extracting soundness, the consistency extractor, and the Merkle-layer collision-extracting soundness, the consistency extractor, and the Merkle-layer
share of pin-store safety. The abstract root-binding lemma from the paper is share of pin-store safety. The folklore whole-tree root-binding property (a root determines its
committed leaf list up to SHA-256 collision) is
mechanized through the specializations needed by the extractors rather than as mechanized through the specializations needed by the extractors rather than as
one quantified hash-fold theorem. Signature unforgeability, execution one quantified hash-fold theorem. Signature unforgeability, execution
provenance, the full signed-head state machine, asymptotic cost, and the provenance, the full signed-head state machine, asymptotic cost, and the
@ -1269,7 +1301,7 @@ Inclusion & completeness and named collision extractor & collision resistance in
Consistency & recursive-model soundness and extractor & no general consistency-completeness theorem \\ Consistency & recursive-model soundness and extractor & no general consistency-completeness theorem \\
Pinning & per-step monotonicity and prefix correctness & signature layer and multi-step closure external \\ Pinning & per-step monotonicity and prefix correctness & signature layer and multi-step closure external \\
Deployment refinement & finite differential harness & no theorem for iterative verifier under authentic-pair invariant \\ Deployment refinement & finite differential harness & no theorem for iterative verifier under authentic-pair invariant \\
Policy separation & deterministic tooling logic and regression tests & not mechanized in the entry-13 corpus \\ Policy separation & deterministic tooling logic and regression tests & not mechanized in the leaf-12 corpus \\
Scheme-level games (\S\ref{sec:games}) & paper-level explicit reductions & two-transcript comparisons and prefix transport not mechanized \\ Scheme-level games (\S\ref{sec:games}) & paper-level explicit reductions & two-transcript comparisons and prefix transport not mechanized \\
\bottomrule \bottomrule
\end{tabularx} \end{tabularx}
@ -1278,9 +1310,10 @@ Scheme-level games (\S\ref{sec:games}) & paper-level explicit reductions & two-t
\subsection{Cost and reproducibility} \subsection{Cost and reproducibility}
A replay of one Ed25519 fork requires approximately 30 minutes of end-to-end A replay of one Ed25519 fork requires approximately 30 minutes of end-to-end
guarded replay time under the pinned environment, a figure corroborated by the resource-guarded (memory- and time-capped) replay time under the pinned environment, a figure corroborated by the
inter-leaf issuance spacing visible in the published log. Receipt verification requires one Ed25519 inter-leaf issuance spacing visible in the published log. Receipt verification requires one Ed25519
signature and a logarithmic number of SHA-256 node computations. The signature and a logarithmic number of SHA-256 node computations (the
complete inclusion core is printed as Appendix~\ref{app:verifier}). The
accumulator corpus is independently reviewable with a pinned public Lean accumulator corpus is independently reviewable with a pinned public Lean
release; an environment-derived inventory fails closed on added, removed, or release; an environment-derived inventory fails closed on added, removed, or
axiom-smuggling declarations. axiom-smuggling declarations.
@ -1374,15 +1407,16 @@ about their replay.
\paragraph{Verification of transparency protocols.} \paragraph{Verification of transparency protocols.}
Cheval et al. mechanize transparency-protocol reasoning~\cite{cheval}. Cheval et al. mechanize transparency-protocol reasoning~\cite{cheval}.
The entry-13 corpus approaches the composition from the opposite direction: it The leaf-12 corpus approaches the composition from the opposite direction: it
mechanizes accumulator arguments and then logs that replay result. The mechanizes accumulator arguments and then logs that replay result. The
remaining refinement from the deployed state machine to the recursive model is remaining refinement from the deployed state machine to the recursive model is
explicitly open. explicitly open.
\section{Limitations and research agenda}\label{sec:limitations} \section{Limitations and research agenda}\label{sec:limitations}
The subject corpus maintains a numbered ledger of fifteen known gaps together The subject corpus maintains a numbered public file, \code{KNOWN-GAPS},
with their closure options; this section groups the load-bearing ones. of fifteen gaps with their closure options (the scope block of
Appendix~\ref{app:entry13} cites its items 14 and 15); this section groups the load-bearing ones.
\paragraph{Operator observation trust.} \paragraph{Operator observation trust.}
A malicious operator can fabricate a replay report. Signatures and Merkle A malicious operator can fabricate a replay report. Signatures and Merkle
@ -1416,7 +1450,7 @@ isolated clients to receive that view. Independent witnesses or gossip are the
natural next deployment step. natural next deployment step.
\paragraph{Consistency refinement.} \paragraph{Consistency refinement.}
The recursive model is proved; the iterative deployment diverges from it on The recursive model is proved; the iterative deployment diverged from it on
malformed inputs, every observed divergence being deployed-accepts-only. The strongest closure is either to deploy malformed inputs, every observed divergence being deployed-accepts-only. The strongest closure is either to deploy
$\ConsRec$-equivalent semantics or to mechanize the signed-head and pin-store $\ConsRec$-equivalent semantics or to mechanize the signed-head and pin-store
flow and prove the authentic-pair refinement theorem. flow and prove the authentic-pair refinement theorem.
@ -1446,7 +1480,7 @@ become attributable when compared.
The Lean Transparency Log demonstrates the complete construction. It amortizes The Lean Transparency Log demonstrates the complete construction. It amortizes
expensive replay over lightweight consumers, retains failed and superseded expensive replay over lightweight consumers, retains failed and superseded
observations, and carries a scoped attestation of the accumulator's own Lean observations, and carries a scoped attestation of the accumulator's own Lean
corpus as entry 13. Just as importantly, the mechanization and differential corpus as leaf 12. Just as importantly, the mechanization and differential
harness exposed a mismatch between the recursive model and the deployed harness exposed a mismatch between the recursive model and the deployed
consistency verifier. Recording that mismatch in the public leaf is not a consistency verifier. Recording that mismatch in the public leaf is not a
failure of the method; it is evidence that the trust decomposition is doing failure of the method; it is evidence that the trust decomposition is doing
@ -1460,7 +1494,7 @@ replay attestation provides an immediate infrastructure layer while those
stronger validity mechanisms are developed. stronger validity mechanisms are developed.
\section*{Artifact availability} \section*{Artifact availability}
The live service is \url{https://ltl.zkdefi.org}. Entry 13 has leaf hash The live service is \url{https://ltl.zkdefi.org}. Leaf 12 (the log's thirteenth entry) has leaf hash
\begin{center}\small\ttfamily \begin{center}\small\ttfamily
8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a 8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a
\end{center} \end{center}
@ -1486,7 +1520,7 @@ The author designed the system and is responsible for every claim. Claude
tooling, and manuscript review. Their output was not accepted as evidence; tooling, and manuscript review. Their output was not accepted as evidence;
claims were retained only after human review or reproducible artifact checks. claims were retained only after human review or reproducible artifact checks.
\begin{thebibliography}{22} \begin{thebibliography}{23}
\itemsep2pt \itemsep2pt
\bibitem{ct1} B. Laurie, A. Langley, E. K\"asper. Certificate Transparency. \bibitem{ct1} B. Laurie, A. Langley, E. K\"asper. Certificate Transparency.
RFC 6962, 2013. RFC 6962, 2013.
@ -1566,6 +1600,9 @@ Collision-Resistant Hashing without the Keys. VIETCRYPT, LNCS 4341, pp.
Verification Pipeline with AI Provers: An Experience Report. arXiv:2605.30106, Verification Pipeline with AI Provers: An Experience Report. arXiv:2605.30106,
2026. 2026.
\bibitem{fips205} National Institute of Standards and Technology.
Stateless Hash-Based Digital Signature Standard. FIPS 205, August 2024.
\end{thebibliography} \end{thebibliography}
% Appendix policy (declared 2026-08-16): the appendix block starts on a % Appendix policy (declared 2026-08-16): the appendix block starts on a
@ -1605,8 +1642,8 @@ Claimed signer implementation produced STH & not established & execution provena
\end{tabularx} \end{tabularx}
\end{center} \end{center}
\section{Deployed entry-13 scope}\label{app:entry13} \section{Deployed leaf-12 scope}\label{app:entry13}
The thirteenth public leaf contains the following deployment constraint, Leaf 12 contains the following deployment constraint,
quoted verbatim, in its machine-readable scope block: quoted verbatim, in its machine-readable scope block:
\begin{quote}\small \begin{quote}\small
Attestation scope: this corpus kernel-checks the listed theorems about the Attestation scope: this corpus kernel-checks the listed theorems about the
@ -1682,6 +1719,11 @@ T4 & constructive decompression lift & \code{verify_accepts_iff_decompress} \\
\end{tabular} \end{tabular}
\end{center} \end{center}
All four tiers share one opaque boundary --- the SHA-512 challenge hash
and the selected wire-format interfaces (\S\ref{sec:instantiation});
the arithmetic and group certificates beneath them rest on Lean's
foundational axioms alone.
\section{SLH-DSA verification certificates and their cones}\label{app:slhtiers} \section{SLH-DSA verification certificates and their cones}\label{app:slhtiers}
Eleven certificates over the extracted SLH-DSA-SHA2-128s verify path Eleven certificates over the extracted SLH-DSA-SHA2-128s verify path
@ -1715,10 +1757,10 @@ The oracles model the parameter set's SHA-256 hash-suite instantiations:
\code{h} (Merkle node), \code{t_l} and \code{t_len} (the WOTS and FORS \code{h} (Merkle node), \code{t_l} and \code{t_len} (the WOTS and FORS
compressors --- two axioms over what is one Rust primitive, deliberately compressors --- two axioms over what is one Rust primitive, deliberately
conservative, with the source's naming inversion against the standard's conservative, with the source's naming inversion against the standard's
$T_\ell$/$T_k$ documented at the declarations). The acceptance $T_\ell$/$T_k$ documented at the declarations). The acceptance characterization is proved directly from the verifier's
characterization is a structural factorization, not a composition of the structure, not by composing the ten loop theorems --- it would remain
loop theorems: it would remain provable if any of the ten were deleted, provable if any of the ten were deleted. Conversely, each loop
and each loop certificate is meaningful exactly to the extent its certificate carries assurance only insofar as a human has checked its
reference fold has been read against FIPS~205. reference fold against the corresponding FIPS~205 algorithm.
\end{document} \end{document}

122
paper/reinvention-outline.md
View file

@ -1,122 +0,0 @@
# Paper reinvention — working outline (post second ePrint rejection)
Status: approved direction (operator order 2026-07-16: "entry 13 and
paper reinvention"); this outline is the committed starting point for
the full rewrite. Diagnosis it responds to: both external analyses
(GPT-5.6 rejection post-mortem; round-6 reviewer aside) converge on
POSITIONING, not correctness — five papers compressed into one, the
novelty (trust decomposition) occupying less space than its supporting
machinery, and the honest "components unchanged" refrain reading as
"nothing new" in a thirty-second editorial skim.
## 0. The one sentence (everything else exists to support it)
> We define and instantiate a cryptographic distribution model for
> machine-checked correctness evidence, enabling lightweight consumers
> to obtain accountable assurance without executing the original
> verifier — and demonstrate it end to end with a deployed log that
> carries kernel-checked proofs of its own accountability machinery as
> an entry in itself.
The second clause is the only-this-paper claim; it becomes literally
true at entry 13 and the paper should be finalized AFTER that append so
the abstract can cite the live leaf.
## 1. Title candidates (working)
- "Accountable Distribution of Machine-Checked Correctness Evidence"
- "Transparency for Theorem Provers: Distributing Formal Verification
to Consumers Who Cannot Replay It"
- (subtitle either way): "…with a deployed log that notarizes the
proofs of its own machinery"
"The Lean Transparency Log" becomes the *system's* name, not the
paper's identity.
## 2. Inverted structure
1. **Problem.** Theorem provers solve the PRODUCTION of correctness
evidence; nothing standard solves scalable DISTRIBUTION and
CONSUMPTION by clients that cannot run the prover (no toolchain, no
hours of replay, no trust in the operator's word). State it as the
gap between "verified" and "verifiable by you."
2. **Model.** The trust decomposition, presented abstractly:
(a) producer performs expensive deterministic verification once;
(b) the result becomes a precise attestation object (subject commit,
toolchain, certificates with exact assumption cones, scope);
(c) a transparency structure supplies persistence, consistency, and
equivocation-evidence; (d) consumers apply policy locally without
executing the verifier; (e) the residual trust is enumerated, not
waved at. Define the accountability property: misbehavior
manufactures transferable evidence.
3. **Design space** (the section the old paper lacked). Position
against: reproducible replay services; succinct proofs of proof
checking (SNARKed kernels); checkpoint/cosigning committees;
witness cosigning; downloadable proof artifacts; proof-carrying
code; cached prover environments/containers. Axis of comparison:
consumer cost, operator trust, accountability (evidence on
misbehavior), incrementality, and what happens when the operator
disappears. The log wins on accountability-per-consumer-cost; be
honest where SNARKed checking would win (validity vs
accountability) and why it is not yet practical for a full kernel.
4. **Instantiation: the LTL.** Lean 4 + Aeneas corpora as producers;
Ed25519 heads signed by the dogfooded verified signer
(self_inclusion); RFC 9162 accumulator; pin-store consumers.
Compressed from old §4–5; the four ed25519 subject corpora become a
TABLE + pointer to project documentation, not sections.
5. **Security of the instantiation.** The mechanized model (61
certificates, single opaque-SHA-256 axiom, environment-derived audit
surface); Theorems 1–3 + Prop 1 in one page each of STATEMENT (the
proofs live in the repo; the paper sells the statements). Present
gap 14/15 as a RESULT, not a confession: the model/deployment seam
located, measured (3,867 one-sided divergences), fenced by pinned
tests, and bridged by an explicitly stated operational invariant —
this is what honest mechanization boundaries look like.
6. **Exhibit A: the log attests itself.** Entry 13 as the paper's
demonstration: the accountability machinery's own proofs, carried by
the machinery, verifiable end to end by one command from a stock
toolchain. Include the leaf hash + head root; a reader can check
inclusion in seconds.
7. **Deployment & consumers.** Live service; warden (quorum custody
wallet) as the internal consumer; Swiss Post e-voting PoC as the
prospective external consumer (dalek-family transport). Replay
economics (measured ~1,800 s/fork) as the cost the model amortizes.
8. **Related work.** CT lineage (RFC 6962/9162, CONIKS, sigstore);
optimistic-rollup analogy (accountability-over-validity; the
fraud-proof reading of Theorem 3 — from
ltl-accumulator-verified/docs/optimistic-accountability.md);
proof-carrying code; reproducible builds/SLSA; in-toto.
9. **Limitations** = the 15-gap ledger, grouped (assumption base /
scope lines / unmechanized bridge), each one sentence, pointer to
the repo ledger.
## 3. What moves OUT of the paper
- Ed25519 corpus construction details → project docs / possible
separate implementation report ("Paper C" in the GPT taxonomy).
- Curriculum, wallet internals, agent-native surfaces → out entirely.
- Appendix A/B verbatim-leaf material → shrink to one leaf excerpt
(entry 13 itself, naturally).
- The §8 operational-history narrative → compress to the
retrievability-decay paragraph + one table.
## 4. Sequencing & venues
1. Entry 13 lands (prerequisite for the abstract's second clause).
2. Rewrite per this outline (fresh tex, new title; old ltl.tex remains
hosted as the system report at /paper — versioned, not erased).
3. arXiv (cs.CR) immediately for timestamp + citability.
4. Venue: CPP/ITP (mechanization framing) or SCORED/SecDev
(supply-chain framing) or RWC talk (deployment framing) — decide
after the rewrite settles which face leads.
5. All queued wording fixes (Lemma-2 specializations, fidelity =
pinned families, §10(i)/(v), Remark 1, pinned-pair side condition)
are ABSORBED by the rewrite rather than patched into the old text.
## 5. Success criterion
A hurried editor can answer "what is the contribution?" from the title
+ first paragraph alone, and the thought-experiment inversion holds:
remove any single supporting component (Lean, Ed25519, RFC 9162) and
the CLAIM survives; remove the trust-decomposition model and nothing is
left. That is the opposite polarity of the rejected manuscript.

36
provider/src/pacta_provider/web.py
View file

@ -20,6 +20,39 @@ from .transparency_log import TransparencyLog
API_VERSION = "v1" API_VERSION = "v1"
def _openapi_document(base: str) -> dict:
"""The machine interface, described the industry-standard way (OpenAPI 3)
instead of a hand-written endpoint box on the human docs page."""
q = lambda name, desc, req=True: {"name": name, "in": "query", "required": req,
"description": desc, "schema": {"type": "string"}}
ok = {"200": {"description": "success"}}
return {
"openapi": "3.0.3",
"info": {"title": "Lean Transparency Log",
"description": "Read-only CT-style interface of the LTL. "
"Heads are signed offline; this service holds no key material.",
"version": API_VERSION},
"servers": [{"url": "https://ltl.zkdefi.org" + base}],
"paths": {
"/log-public-key": {"get": {"summary": "Required Ed25519 public key (PEM)", "responses": ok}},
"/log-slhdsa-public-key": {"get": {"summary": "Post-quantum SLH-DSA public key (PEM)", "responses": ok}},
"/healthz": {"get": {"summary": "Liveness and current tree size", "responses": ok}},
"/paper": {"get": {"summary": "The current paper (PDF)", "responses": ok}},
f"/{API_VERSION}/metadata": {"get": {"summary": "Log identity", "responses": ok}},
f"/{API_VERSION}/sth": {"get": {"summary": "Latest Signed Tree Head", "responses": ok}},
f"/{API_VERSION}/sth-history": {"get": {"summary": "Every Signed Tree Head ever issued (witness material)", "responses": ok}},
f"/{API_VERSION}/sth-consistency": {"get": {"summary": "Consistency proof from a pinned size",
"parameters": [q("first", "your pinned old tree size")], "responses": ok}},
f"/{API_VERSION}/proof": {"get": {"summary": "Inclusion proof (freshly issued receipt)",
"parameters": [q("component", "component name", False), q("leaf_hash", "leaf hash (hex)", False)], "responses": ok}},
f"/{API_VERSION}/attestation": {"get": {"summary": "Newest attestation for a component",
"parameters": [q("component", "component name")], "responses": ok}},
f"/{API_VERSION}/entries": {"get": {"summary": "Raw leaves in [start, end)",
"parameters": [q("start", "first index", False), q("end", "one past last index", False)], "responses": ok}},
},
}
def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdfs: dict[str, bytes] | None = None): def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdfs: dict[str, bytes] | None = None):
paper_pdfs = paper_pdfs or {} paper_pdfs = paper_pdfs or {}
@ -78,6 +111,8 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
self.send_header("Content-Length", str(len(body))) self.send_header("Content-Length", str(len(body)))
self.end_headers() self.end_headers()
self.wfile.write(body) self.wfile.write(body)
elif route == "/openapi.json":
self._send(200, _openapi_document(base))
elif route == "/healthz": elif route == "/healthz":
self._send(200, {"ok": True, "tree_size": len(log.entries())}) self._send(200, {"ok": True, "tree_size": len(log.entries())})
elif route == f"/{API_VERSION}/metadata": elif route == f"/{API_VERSION}/metadata":
@ -153,6 +188,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
f"{base}/log-public-key", f"{base}/log-public-key",
f"{base}/log-slhdsa-public-key", f"{base}/log-slhdsa-public-key",
f"{base}/healthz", f"{base}/healthz",
f"{base}/openapi.json",
f"{base}/{API_VERSION}/metadata", f"{base}/{API_VERSION}/metadata",
f"{base}/{API_VERSION}/sth", f"{base}/{API_VERSION}/sth",
f"{base}/{API_VERSION}/sth-history", f"{base}/{API_VERSION}/sth-history",

228
provider/src/pacta_provider/webdocs.py
View file

@ -21,7 +21,8 @@ _STYLE = """
h2{font-size:1.2rem;margin-top:2.6rem;border-bottom:2px solid var(--line);padding-bottom:.3rem} h2{font-size:1.2rem;margin-top:2.6rem;border-bottom:2px solid var(--line);padding-bottom:.3rem}
.tagline{font-size:1.05rem;color:var(--ink2);max-width:46rem} .tagline{font-size:1.05rem;color:var(--ink2);max-width:46rem}
code,pre{font-family:ui-monospace,Menlo,Consolas,monospace;background:#eef0f3;border-radius:4px} code,pre{font-family:ui-monospace,Menlo,Consolas,monospace;background:#eef0f3;border-radius:4px}
code{padding:.1rem .3rem;font-size:.9em} pre{padding:.9rem;overflow-x:auto;font-size:.85rem} code{padding:.1rem .3rem;font-size:.9em;overflow-wrap:anywhere}
pre{padding:.9rem;overflow-x:auto;font-size:.85rem;max-width:100%}
table{border-collapse:collapse;width:100%;font-size:.93rem;background:#fff} table{border-collapse:collapse;width:100%;font-size:.93rem;background:#fff}
td,th{border:1px solid var(--line);padding:.5rem .7rem;text-align:left;vertical-align:top} td,th{border:1px solid var(--line);padding:.5rem .7rem;text-align:left;vertical-align:top}
th{background:var(--accentbg)} th{background:var(--accentbg)}
@ -41,7 +42,6 @@ _STYLE = """
.sw{display:inline-block;width:.8rem;height:.8rem;border-radius:3px;vertical-align:-1px;margin-right:.3rem} .sw{display:inline-block;width:.8rem;height:.8rem;border-radius:3px;vertical-align:-1px;margin-right:.3rem}
""" """
def _leaf_ok(entry: LogEntry) -> bool: def _leaf_ok(entry: LogEntry) -> bool:
certificates = ((entry.leaf.get("attestation") or {}).get("certificates")) or [] certificates = ((entry.leaf.get("attestation") or {}).get("certificates")) or []
return bool(certificates) and all( return bool(certificates) and all(
@ -49,6 +49,11 @@ def _leaf_ok(entry: LogEntry) -> bool:
for certificate in certificates for certificate in certificates
) )
def _leaf_short(component: str) -> str:
"""Compact display name for a leaf box at small spans."""
return (component.replace("-ed25519-verified", "")
.replace("ltl-accumulator-verified", "accum")
.replace("fips205-slhdsa-verified", "slh-dsa"))
def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str, head_label: str = "Ed25519") -> str: def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str, head_label: str = "Ed25519") -> str:
"""The accumulator, drawn from its real leaves.""" """The accumulator, drawn from its real leaves."""
@ -77,10 +82,20 @@ def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str, head
ok = _leaf_ok(entry) ok = _leaf_ok(entry)
component = (((entry.leaf.get("attestation") or {}).get("subject")) or {}).get("component", "?") component = (((entry.leaf.get("attestation") or {}).get("subject")) or {}).get("component", "?")
fill, stroke = ("#e2f2e9", "#1e7f4f") if ok else ("#f4f4f6", "#8a93a0") fill, stroke = ("#e2f2e9", "#1e7f4f") if ok else ("#f4f4f6", "#8a93a0")
out.append(f'<rect x="{x-56}" y="{y-22}" width="112" height="44" rx="5" fill="{fill}" stroke="{stroke}" stroke-width="1.4"/>') # Boxes must FIT the per-leaf span at any tree size (the
out.append(f'<text x="{x}" y="{y-6}" text-anchor="middle" fill="#333">leaf {node_index}</text>') # 2026-08-16 lesson: fixed 112px boxes shingled at 19
short = escape(str(component).replace("-ed25519-verified", "")) # leaves). Rich boxes while they fit, compact ones after.
box_w = min(112.0, span * 0.94)
compact = box_w < 100
short = escape(_leaf_short(str(component)))
label = short if ok else f"{short} ✗" label = short if ok else f"{short} ✗"
if compact:
out.append(f'<rect x="{x-box_w/2:.1f}" y="{y-18}" width="{box_w:.1f}" height="36" rx="4" fill="{fill}" stroke="{stroke}" stroke-width="1.2"/>')
out.append(f'<text x="{x}" y="{y-4}" text-anchor="middle" fill="#333" font-size="8">leaf {node_index}</text>')
out.append(f'<text x="{x}" y="{y+9}" text-anchor="middle" fill="{stroke}" font-size="7">{label}</text>')
else:
out.append(f'<rect x="{x-box_w/2:.1f}" y="{y-22}" width="{box_w:.1f}" height="44" rx="5" fill="{fill}" stroke="{stroke}" stroke-width="1.4"/>')
out.append(f'<text x="{x}" y="{y-6}" text-anchor="middle" fill="#333">leaf {node_index}</text>')
out.append(f'<text x="{x}" y="{y+8}" text-anchor="middle" fill="{stroke}">{label}</text>') out.append(f'<text x="{x}" y="{y+8}" text-anchor="middle" fill="{stroke}">{label}</text>')
out.append(f'<text x="{x}" y="{y+19}" text-anchor="middle" fill="#999" font-size="9">{node.hex()[:10]}…</text>') out.append(f'<text x="{x}" y="{y+19}" text-anchor="middle" fill="#999" font-size="9">{node.hex()[:10]}…</text>')
else: else:
@ -91,16 +106,23 @@ def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str, head
for child in (2 * node_index, 2 * node_index + 1): for child in (2 * node_index, 2 * node_index + 1):
if (level_index - 1, child) in positions: if (level_index - 1, child) in positions:
cx, cy = positions[(level_index - 1, child)] cx, cy = positions[(level_index - 1, child)]
out.append(f'<line x1="{x}" y1="{y+15}" x2="{cx}" y2="{cy-22 if level_index==1 else cy-15}" stroke="#ccc"/>') leaf_top = 18 if len(entries) > 9 else 22
out.append(f'<line x1="{x}" y1="{y+15}" x2="{cx}" y2="{cy-leaf_top if level_index==1 else cy-15}" stroke="#ccc"/>')
root_x, root_y = positions[(len(levels) - 1, 0)] root_x, root_y = positions[(len(levels) - 1, 0)]
out.append(f'<rect x="{root_x-190}" y="{root_y-72}" width="380" height="34" rx="6" fill="#e2f2e9" stroke="#1e7f4f" stroke-width="1.6"/>') # The head box sizes itself to its longest line (the 2026-08-16
out.append(f'<text x="{root_x}" y="{root_y-58}" text-anchor="middle" fill="#1e7f4f" font-weight="bold">Signed Tree Head — {escape(head_label)}({root_hex[:12]}…)</text>') # lesson: a fixed 380px box let a growing caption spill both sides).
out.append(f'<text x="{root_x}" y="{root_y-46}" text-anchor="middle" fill="#1e7f4f" font-size="9">signed by: {escape(signing_backend)} (verify path attested; signing itself not proven)</text>') title = f"Signed Tree Head — {head_label}({root_hex[:12]}…)"
line2 = f"signed by: {signing_backend}"
line3 = "(verify path attested; signing itself not proven)"
head_w = max(len(title) * 7.0, len(line2) * 5.3, len(line3) * 5.3) + 28
out.append(f'<rect x="{root_x-head_w/2:.1f}" y="{root_y-84}" width="{head_w:.1f}" height="46" rx="6" fill="#e2f2e9" stroke="#1e7f4f" stroke-width="1.6"/>')
out.append(f'<text x="{root_x}" y="{root_y-70}" text-anchor="middle" fill="#1e7f4f" font-weight="bold">{escape(title)}</text>')
out.append(f'<text x="{root_x}" y="{root_y-58}" text-anchor="middle" fill="#1e7f4f" font-size="9">{escape(line2)}</text>')
out.append(f'<text x="{root_x}" y="{root_y-47}" text-anchor="middle" fill="#1e7f4f" font-size="9">{escape(line3)}</text>')
out.append(f'<line x1="{root_x}" y1="{root_y-38}" x2="{root_x}" y2="{root_y-15}" stroke="#1e7f4f" stroke-width="1.4"/>') out.append(f'<line x1="{root_x}" y1="{root_y-38}" x2="{root_x}" y2="{root_y-15}" stroke="#1e7f4f" stroke-width="1.4"/>')
out.append("</svg>") out.append("</svg>")
return "".join(out) return "".join(out)
def _trust_anchor_html(log: TransparencyLog, metadata: dict[str, Any], base: str, mirror: str) -> str: def _trust_anchor_html(log: TransparencyLog, metadata: dict[str, Any], base: str, mirror: str) -> str:
"""The provider public key, displayed in full on the front page. The key """The provider public key, displayed in full on the front page. The key
is the one thing a consumer takes on trust, once - hiding it behind a is the one thing a consumer takes on trust, once - hiding it behind a
@ -125,11 +147,10 @@ def _trust_anchor_html(log: TransparencyLog, metadata: dict[str, Any], base: str
slh_pem = escape(slh_path.read_text(encoding="utf-8").strip()) slh_pem = escape(slh_path.read_text(encoding="utf-8").strip())
slh_fp = _h.sha256(slh_path.read_bytes()).hexdigest() slh_fp = _h.sha256(slh_path.read_bytes()).hexdigest()
slh_block = f"""<hr style="border:none;border-top:1px solid #ddd;margin:.8rem 0"> slh_block = f"""<hr style="border:none;border-top:1px solid #ddd;margin:.8rem 0">
<p style="margin-top:0"><strong>Second, additive anchor — post-quantum.</strong> Heads from <p style="margin-top:0"><strong>Key&nbsp;2 — SLH-DSA (FIPS&nbsp;205), post-quantum.</strong> Heads from tree size&nbsp;14 on carry a second signature from this key;
tree&nbsp;14 on additionally carry a deterministic <strong>SLH-DSA-SHA2-128s</strong> (FIPS&nbsp;205) older heads legitimately have none — an append-only log keeps its history. Check it where your
signature over the same payload. The Ed25519 signature above remains the one every consumer must tooling allows (OpenSSL&nbsp;≥&nbsp;3.5). The kind of code that verifies such signatures is itself
check; this one is checked where tooling allows (OpenSSL&nbsp;≥&nbsp;3.5). Its verify path is the a proof subject of this log (entry&nbsp;18).</p>
proof subject of leaf&nbsp;18.</p>
<pre style="margin-bottom:.4rem">{slh_pem}</pre> <pre style="margin-bottom:.4rem">{slh_pem}</pre>
<p class="muted" style="margin:.2rem 0 0">SHA-256 fingerprint <code>{slh_fp}</code> <p class="muted" style="margin:.2rem 0 0">SHA-256 fingerprint <code>{slh_fp}</code>
&nbsp;·&nbsp; raw: <a href="{base}/log-slhdsa-public-key"><code>{base or ''}/log-slhdsa-public-key</code></a> &nbsp;·&nbsp; raw: <a href="{base}/log-slhdsa-public-key"><code>{base or ''}/log-slhdsa-public-key</code></a>
@ -137,20 +158,20 @@ proof subject of leaf&nbsp;18.</p>
else: else:
slh_block = "" slh_block = ""
return f"""<div class="card"> return f"""<div class="card">
<p style="margin-top:0">This key is the <strong>sole cryptographic identity anchor</strong>: it <p style="margin-top:0"><strong>Two keys sign everything in this log.</strong> Neither makes a
authenticates that these statements were made by the operator (the same party the artifacts call “the provider”). It does not, by itself, make claim <em>true</em>; they prove a claim comes from this operator, unchanged. Save your own copy
those statements true — each attestation's truth additionally rests on the replay, theorem, of both — that is called <em>pinning</em>: from then on you trust only what verifies against
extraction and toolchain assumptions stated in that leaf (one signed entry of the tree below). Every tree head and attestation is your saved copies. Fetch each key from this page AND from the independently hosted mirror and
signature-checked against this key. compare byte-for-byte; the copies must be identical. (The first fetch is trust-on-first-use;
Pin it (save your own copy; from then on trust only what checks against that copy), and compare this copy byte-for-byte with the independently hosted comparing two independent hosts is what bounds it.)</p>
<a href="{mirror}/blob/main/provider.ed25519.pub">mirror copy</a>; they must be identical. The first fetch is trust-on-first-use; the two-host byte-comparison is what bounds it.</p> <p><strong>Key&nbsp;1 — Ed25519, required.</strong> Every signed head and every attestation must
verify against it.</p>
<pre style="margin-bottom:.4rem">{pem}</pre> <pre style="margin-bottom:.4rem">{pem}</pre>
<p class="muted" style="margin:.2rem 0 0">SHA-256 fingerprint <code>{escape(fingerprint)}</code> <p class="muted" style="margin:.2rem 0 0">SHA-256 fingerprint <code>{escape(fingerprint)}</code>
&nbsp;·&nbsp; raw: <a href="{base}/log-public-key"><code>{base or ''}/log-public-key</code></a> &nbsp;·&nbsp; raw: <a href="{base}/log-public-key"><code>{base or ''}/log-public-key</code></a>
&nbsp;·&nbsp; <code>curl -s https://ltl.zkdefi.org/log-public-key</code></p> &nbsp;·&nbsp; <code>curl -s https://ltl.zkdefi.org/log-public-key</code></p>
{slh_block}</div>""" {slh_block}</div>"""
def render_docs(log: TransparencyLog, base_path: str) -> str: def render_docs(log: TransparencyLog, base_path: str) -> str:
base = "/" + base_path.strip("/") if base_path.strip("/") else "" base = "/" + base_path.strip("/") if base_path.strip("/") else ""
metadata = log.metadata() metadata = log.metadata()
@ -196,24 +217,100 @@ def render_docs(log: TransparencyLog, base_path: str) -> str:
· <a href="https://zkdefi.org/saymrwulf">code</a> · <a href="https://zkdefi.org/saymrwulf">code</a>
· <a href="https://zkdefi.com/">cv</a></p> · <a href="https://zkdefi.com/">cv</a></p>
<h1>LTL — the Lean Transparency Log</h1> <h1>LTL — the Lean Transparency Log</h1>
<p class="tagline"><strong>One sentence:</strong> a public, append-only Merkle <p><strong>Every known way of consuming formal verification fails on one of two
accumulator (a hash tree that only ever grows) of <em>signed statements that the <a href="https://lean-lang.org">Lean&nbsp;4</a> formal proofs of specific sides: either the cost stays with you (re-running a theorem prover), or the cost
cryptographic Rust libraries, at specific git commits, re-check by machine with exactly disappears because you are asked to believe a label. This site holds the point in
their documented assumptions</em> — so that you can trust a proof result by checking between — it makes machine-checked proof results as cheap to check as one
<strong>one required signature (Ed25519) and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in signature and a handful of hashes, without turning them into trust. Every claim
milliseconds</strong>, instead of running a theorem prover for hours.</p> the operator ever makes is recorded here permanently, bound to his key, and
scoped to its exact assumptions: he can never be believed, only held
accountable.</strong></p>
<h2>The trust anchor — pin this key</h2> <p>Concretely: a proof assistant — <a href="https://lean-lang.org">Lean&nbsp;4</a>, a
program that checks mathematical proofs mechanically — has verified precise
statements about the code that <em>checks signatures</em>: in four widely deployed
<strong>Ed25519</strong> libraries, in an implementation of <strong>SLH-DSA</strong>
(FIPS&nbsp;205, the hash-based post-quantum signature standard), and in <strong>the
Merkle-tree machinery of this log itself</strong>. Each completed proof check is one
signed, numbered entry that can never be altered or removed — {len(entries)} entries
so far, drawn live further down this page. How much of our work you re-verify is
your choice, from milliseconds to everything:</p>
<h2>Choose where you stand — the trust ladder</h2>
<div class="steps">
<div class="card"><strong>Hold a copy of the history.</strong> — anyone; one minute.<br>
You still trust: the content of every claim. You defeat: silent rewriting.<br>
You need: Python&nbsp;3 and the <code>openssl</code> command (preinstalled on most Linux and macOS systems).
<pre>git clone https://github.com/saymrwulf/lean-transparency-log &amp;&amp; cd lean-transparency-log &amp;&amp; python3 verify.py --all</pre>
<span class="muted">This fetches the log&rsquo;s public mirror — a git repository holding every entry
and every signed head ever issued (a head is the signed root fingerprint of the tree at a
given size) — and re-computes every hash and signature in it. A green
result means the history you now hold is internally consistent and signed. Keep the folder:
if the operator ever shows a different history to anyone else, your copy proves it. A log
that shows different histories to different people (a &ldquo;split view&rdquo;) survives only until
two holders compare.</span></div>
<div class="card"><strong>Check that a claim is real and binding.</strong> — milliseconds.<br>
You still trust: that the operator&rsquo;s recorded observation is honest.<br>
You need: four small files from the tables below — the two public keys, plus one library&rsquo;s
claim file (&ldquo;attestation&rdquo;) and its proof of inclusion (&ldquo;receipt&rdquo;).
<pre>pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub --slhdsa-public-key provider.slhdsa.pub</pre>
<span class="muted">Your machine checks the required Ed25519 signature, the second (post-quantum) signature
(needs OpenSSL&nbsp;≥&nbsp;3.5; drop the second flag to skip it), and
~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes — no proof assistant involved.
The <code>pacta</code> tool ships in the
<a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a>
(<code>pip install .</code> from a clone); about forty lines of ordinary Python do the same
check, and the mirror&rsquo;s <code>verify.py</code> contains exactly that core. Afterwards the
claim — which repository, which exact source version, which theorems, which assumptions —
is bound to the operator&rsquo;s key inside a history he can neither rewrite nor deny.</span></div>
<div class="card"><strong>Judge by your own standards.</strong> — minutes.<br>
Every entry records more than pass/fail: it lists the exact assumptions each proof rests on
(its <em>axiom cone</em>). So you may ignore the operator&rsquo;s verdicts entirely: write down
which assumptions <em>you</em> accept, and have your tooling compare list against list, name
by name. <code>pacta</code> automates the comparison; lecture&nbsp;11 of the Jupyter course (same
repository) teaches it step by step.
<span class="muted">Afterwards every verdict is your verdict — the operator&rsquo;s labels can at
most veto, never grant. The section &ldquo;You hold the ruler&rdquo; below is this rung in full.</span></div>
<div class="card"><strong>Re-run the proof check yourself.</strong> — about 30&nbsp;minutes per library.<br>
You still trust: that the published Lean statements mean what they say.<br>
You need: a Lean&nbsp;4 toolchain (free).
<span class="muted">Every attested repository ships one script, <code>verification/check.sh</code>.
Clone the repository at the exact source version recorded in its log entry and run the script:
the proof assistant re-checks every theorem on your machine and prints every assumption list.
The operator is now out of the loop entirely.</span></div>
<div class="card"><strong>Rebuild everything from source.</strong> — weeks.<br>
What remains trusted: Lean&rsquo;s proof kernel, the Rust-to-Lean translation tools (Charon and
Aeneas), and your compiler — the floor, which we name rather than hide.
<span class="muted">Every repository documents its full path: the pinned upstream Rust code,
the extraction script that regenerates the Lean definitions byte-for-byte, and the theorem
statements to read against the standards themselves (FIPS&nbsp;205, RFC&nbsp;9162, the curve
equations). Reproduce any part; compare with what is published. After this rung you no longer
need this site — that is the point. There is no rung&nbsp;6: even here you trust a kernel, a
compiler, and your hardware.</span></div>
</div>
<h2>Two keys sign this log — pin these keys</h2>
{_trust_anchor_html(log, metadata, base, mirror)} {_trust_anchor_html(log, metadata, base, mirror)}
<h2>The accumulator, live</h2> <h2>The accumulator, live</h2>
<p>The log is a <strong>Merkle tree</strong>: every entry (&ldquo;leaf&rdquo;) is hashed, hashes pair
up level by level, and a single 32-byte root fingerprints the entire history; the operator signs
that root. Changing any past entry would change the root — that is the tamper evidence. Each leaf
records one proof run: a batch of <strong>certificates</strong> — one machine-checked theorem
each, together with its exact assumption list. This
picture is computed from the live log at page render — the leaf hashes, nodes, root, and
signature are the real ones:</p>
{tree_svg} {tree_svg}
<p class="legend"> <p class="legend">
<span><span class="sw" style="background:#e2f2e9;border:1px solid #1e7f4f"></span>verified attestation (all certificates proven, axiom cones boundary-exact)</span> <span><span class="sw" style="background:#e2f2e9;border:1px solid #1e7f4f"></span>verified attestation — every certificate proven, every assumption list exactly as declared</span>
<span><span class="sw" style="background:#f4f4f6;border:1px solid #8a93a0"></span>historical audit-failure attestation — kept forever; an append-only ledger does not erase its bad day (leaves&nbsp;0–3: an early audit round that failed; leaves&nbsp;4–7 re-attest the same four libraries cleanly)</span> <span><span class="sw" style="background:#f4f4f6;border:1px solid #8a93a0"></span>historical audit-failure attestation — kept forever; an append-only ledger does not erase its bad day (leaves&nbsp;0–3: an early audit round that failed; leaves&nbsp;4–7 re-attest the same four libraries cleanly)</span>
</p> </p>
<p class="muted">Every box above is computed from the live log at page render — leaf hashes, <p class="muted">The library that signs the log is itself an entry in the log — what that entry proves is its <em>verify</em> path (no signing code is proven, here or anywhere) — and it checks its own entry before signing. In detail: before signing this
internal nodes, the root, and the signature are the real ones. The library that signs the log is itself an entry in the log — what that entry proves is its <em>verify</em> path (no signing code is proven, here or anywhere) — and it checks its own entry before signing. In detail: before signing this
root, the provider Merkle-verified its own signing library's leaf root, the provider Merkle-verified its own signing library's leaf
(index {provenance.get('signing_library_leaf_index','?')}, (index {provenance.get('signing_library_leaf_index','?')},
certificates {escape(str(provenance.get('signing_library_certificates_proven','?')))}) certificates {escape(str(provenance.get('signing_library_certificates_proven','?')))})
@ -225,11 +322,12 @@ log id <code>{escape(str(metadata.get('log_id',''))[:16])}…</code>.</p>
<h2>What do I download? — the three artifacts, unambiguously</h2> <h2>What do I download? — the three artifacts, unambiguously</h2>
<p>To benefit from the accumulator you need <strong>exactly three files</strong> per <p>To benefit from the accumulator you need <strong>exactly three files</strong> per
library, plus optionally the whole mirror. Nothing else.</p> library, plus optionally the post-quantum key
(<code>provider.slhdsa.pub</code>) and the whole mirror. Nothing else.</p>
<table> <table>
<tr><th>#</th><th>Artifact</th><th>What it is</th><th>Where</th></tr> <tr><th>#</th><th>Artifact</th><th>What it is</th><th>Where</th></tr>
<tr><td><b>1</b></td><td><code>provider.ed25519.pub</code></td> <tr><td><b>1</b></td><td><code>provider.ed25519.pub</code></td>
<td><strong>The identity anchor.</strong> The provider's public key — the sole cryptographic <td><strong>The identity anchor.</strong> The provider's public key — the required cryptographic
identity you pin. It authenticates the operator's statements; their truth rests on each leaf's identity you pin. It authenticates the operator's statements; their truth rests on each leaf's
stated assumptions. Fetch it from BOTH independent locations and compare; the copies must be stated assumptions. Fetch it from BOTH independent locations and compare; the copies must be
identical.</td> identical.</td>
@ -239,11 +337,13 @@ identical.</td>
which observed axiom cones (the exact set of assumptions each proof ultimately rests on), what machine protection — signed by the provider.</td> which observed axiom cones (the exact set of assumptions each proof ultimately rests on), what machine protection — signed by the provider.</td>
<td>table below, or <a href="{mirror}">mirror</a> <code>entries/</code></td></tr> <td>table below, or <a href="{mirror}">mirror</a> <code>entries/</code></td></tr>
<tr><td><b>3</b></td><td><code>&lt;library&gt;.receipt.json</code></td> <tr><td><b>3</b></td><td><code>&lt;library&gt;.receipt.json</code></td>
<td><strong>The proof of inclusion.</strong> Binds artifact&nbsp;2 into the signed tree: <td><strong>The proof of inclusion.</strong> Binds the claim into the signed tree:
leaf index, sibling hashes, the Signed Tree Head (STH). A one-page Python core verifies it — printed as Appendix&nbsp;C of the paper; the shipped <code>verify.py</code> wraps that core with full fail-closed binding checks (stdlib hashing; signature checks shell out to the <code>openssl</code> binary).</td> leaf index, sibling hashes, the Signed Tree Head (STH). About forty lines of ordinary
Python verify it; the mirror&rsquo;s <code>verify.py</code> contains exactly that core, wrapped in
fail-closed safety checks (stdlib hashing; signature checks shell out to the <code>openssl</code> binary).</td>
<td>table below, or <a href="{mirror}">mirror</a> <code>receipts/</code></td></tr> <td>table below, or <a href="{mirror}">mirror</a> <code>receipts/</code></td></tr>
<tr><td>+</td><td>the full mirror clone</td> <tr><td>+</td><td>the full mirror clone</td>
<td><strong>Maximal benefit: become a witness.</strong> Every leaf + every signed head <td><strong>Maximal benefit: hold the complete history yourself (rung&nbsp;1 of the ladder).</strong> Every leaf + every signed head
ever issued + <code>verify.py</code> (Python stdlib + the <code>openssl</code> binary for ever issued + <code>verify.py</code> (Python stdlib + the <code>openssl</code> binary for
signatures; fails closed without them). <code>python3 verify.py --all</code> signatures; fails closed without them). <code>python3 verify.py --all</code>
recomputes the entire tree and every historical head — you then hold a retained view that can recomputes the entire tree and every historical head — you then hold a retained view that can
@ -254,33 +354,8 @@ consumers.)</td>
</table> </table>
<h2>Attested libraries</h2> <h2>Attested libraries</h2>
<table><tr><th>component</th><th>artifact 2</th><th>artifact 3</th><th>status</th></tr>{rows}</table> <table><tr><th>library</th><th>claim (attestation)</th><th>proof of inclusion (receipt)</th><th>certificates proven</th></tr>{rows}</table>
<p class="muted">One certificate = one machine-checked theorem together with its exact assumption set (its axiom cone).</p>
<h2>Three ways to use it</h2>
<div class="steps">
<div class="card"><strong>Quick check</strong> (any machine, milliseconds): download
artifacts 1–3, then<br>
<code>pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub</code>
<br><span class="muted">No Lean, no Rust, no account. The <code>pacta</code> CLI ships in the <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a> (<code>pip install .</code> from a clone). Add <code>--sth-store pins.json</code> to remember every Signed Tree Head (STH) you accept — your defense against a split view (the operator showing different histories to different consumers).</span></div>
<div class="card"><strong>Zero-install audit</strong>: <code>git clone {mirror} &amp;&amp; cd lean-transparency-log &amp;&amp; python3 verify.py --all</code>
<br><span class="muted">Standard-library Python plus the system <code>openssl</code> binary (signature checks fail closed without it). You become a witness of the whole history.</span></div>
<div class="card"><strong>Autonomous agent</strong>: the <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta</a>
tool adds STH pinning, freshness policy, online refresh from this service, risk scoring
(R0–R5, six named residual-risk classes) with policy-gated consequences, and optionally verifies every signature through
the proof-attested Ed25519 code path itself (<code>--require-verified-verifier</code>).</div>
</div>
<h2>API</h2>
<pre>GET {base}/v1/sth latest Signed Tree Head
GET {base}/v1/sth-history the published head history (witness material)
GET {base}/v1/sth-consistency?first=N consistency proof from your pinned size
GET {base}/v1/proof?component=NAME inclusion proof (artifact 3, freshly issued)
GET {base}/v1/attestation?component=NAME the claim (artifact 2)
GET {base}/v1/entries?start=N&amp;end=M raw leaves
GET {base}/v1/metadata log identity
GET {base}/healthz</pre>
<h2>What a verified inclusion means — and what it does not</h2> <h2>What a verified inclusion means — and what it does not</h2>
<div class="card"><span class="pill ok">means</span> The provider whose key you hold <div class="card"><span class="pill ok">means</span> The provider whose key you hold
@ -292,16 +367,19 @@ view.</div>
proofs cover Rust <em>source</em>; clone the attested commit (the commit id identifies the proofs cover Rust <em>source</em>; clone the attested commit (the commit id identifies the
committed git tree — not external dependencies, toolchain downloads, or generated artifacts) and committed git tree — not external dependencies, toolchain downloads, or generated artifacts) and
build it yourself — compiler and build are declared trusted base (assumed, not proven) build it yourself — compiler and build are declared trusted base (assumed, not proven)
until the reproducible-builds program lands and retires risk class R5. Every attestation carries its full until the reproducible-builds program lands. Every attestation carries its full
residual-risk list — the enumerated assumptions inside its <code>attestation.json</code>. Honesty about the boundary is the product.</div> residual-risk list — the enumerated assumptions inside its <code>attestation.json</code>. Honesty about the boundary is the product.</div>
<h2>You hold the ruler</h2> <h2>You hold the ruler</h2>
<div class="card">The list of assumptions a certificate is <em>allowed</em> to rest on <div class="card">The list of assumptions a certificate is <em>allowed</em> to rest on
is not something this site hands you at verification time — it is a is not something this site hands you at verification time — it is a
<strong>requirements card</strong> that lives in <em>your</em> tooling, on <strong>requirements card</strong> — a short plain-text file listing, by name, the
assumptions you accept — that lives in <em>your</em> tooling, on
<em>your</em> disk, and that you can read in five minutes or rewrite from first <em>your</em> disk, and that you can read in five minutes or rewrite from first
principles: Lean's three foundational axioms, plus — for the signature tiers only (the top proof layers, where full signature verification is proven) — principles: Lean's three foundational axioms, plus — for the signature tiers only (the top proof layers, where full signature verification is proven) —
named placeholders for SHA-512 and the wire format. Your tooling ignores this named placeholders for SHA-512 (the hash function Ed25519 uses internally —
the proofs treat it as an assumption, not as proven) and the byte-level wire
format. Your tooling ignores this
operator's pass/fail labels entirely and re-derives every verdict by comparing the operator's pass/fail labels entirely and re-derives every verdict by comparing the
attestation's <em>observed</em> axiom list (its cone) against <em>your</em> card, name by name. attestation's <em>observed</em> axiom list (its cone) against <em>your</em> card, name by name.
The operator is trusted to copy down what the proof kernel printed — never to The operator is trusted to copy down what the proof kernel printed — never to
@ -319,7 +397,7 @@ our roadmap.</strong> (The full walk-through is lecture&nbsp;11 of the Jupyter c
<h2>The paper</h2> <h2>The paper</h2>
<div class="card"><a href="{base}/paper"><strong>Accountable Distribution of Machine-Checked <div class="card"><a href="{base}/paper"><strong>Accountable Distribution of Machine-Checked
Correctness Evidence: A Transparency Model and the Lean Transparency Log</strong></a> Correctness Evidence: A Transparency Model and the Lean Transparency Log</strong></a>
(PDF, 25 pages, <strong>v0.11 — revised August&nbsp;2026</strong>; the version is printed on the (PDF, 25 pages, <strong>v0.15 — revised August&nbsp;2026</strong>; the version is printed on the
title page) — the trust decomposition (expensive verification produces an title page) — the trust decomposition (expensive verification produces an
observation; transparency makes the observation accountable; consumer-local policy decides observation; transparency makes the observation accountable; consumer-local policy decides
acceptance), collision-extracting soundness for inclusion and consistency, scheme-level acceptance), collision-extracting soundness for inclusion and consistency, scheme-level
@ -330,18 +408,16 @@ operator labels can veto but never grant acceptance, and the measured model/depl
divergence reported as a result rather than hidden — now together with its closure: the divergence reported as a result rather than hidden — now together with its closure: the
divergence traced to one omitted RFC&nbsp;9162 conjunct (Step&nbsp;7's <code>sn&nbsp;=&nbsp;0</code>), divergence traced to one omitted RFC&nbsp;9162 conjunct (Step&nbsp;7's <code>sn&nbsp;=&nbsp;0</code>),
zero divergences after the one-line restoration, confirmed by a three-way regression. zero divergences after the one-line restoration, confirmed by a three-way regression.
New in v0.11: the deployment evaluated to its current nineteen-leaf, dual-signed state, an New in the August 2026 revisions: the deployment evaluated to its current nineteen-leaf, dual-signed state, an
instantiation section for the SLH-DSA (FIPS&nbsp;205) verify path — eleven certificates, instantiation section for the SLH-DSA (FIPS&nbsp;205) verify path — eleven certificates,
five uninterpreted hash oracles, exact cones — and a certificate appendix mirroring the five uninterpreted hash oracles, exact cones — and a certificate appendix mirroring the
Ed25519 tiers.</div> Ed25519 tiers.</div>
<div class="card"><strong>Paper and log, one story.</strong> Since v0.11 the paper
describes this deployment as it runs — nineteen leaves, dual-signed heads, the
post-quantum verify path as leaf&nbsp;18 with its own certificate appendix. The log is
append-only and keeps growing past any paper revision; every number the paper states
stays checkable against the retained history: <code>python3 verify.py --all</code>
re-verifies all of it, paper-era and after, from a clone of the mirror.</div>
<p class="muted">Log heads are signed offline; this service is read-only and holds no <p class="muted">Log heads are signed offline; this service is read-only and holds no
key material. Provider tooling, agent tooling, and the full Jupyter course live in the <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a>.</p> key material. Provider tooling, agent tooling, and the full Jupyter course live in the
<a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a>.
Software integrators: the machine interface behind every link on this page is described by the
OpenAPI document at <a href="{base}/openapi.json"><code>/openapi.json</code></a> — the
<code>pacta</code> tool builds on it (head pinning, freshness policy, risk scoring R0–R5).</p>
</body></html>""" </body></html>"""

4
src/pacta/cli.py
View file

@ -137,6 +137,7 @@ def build_parser() -> argparse.ArgumentParser:
receipt_verify.add_argument("--receipt", required=True) receipt_verify.add_argument("--receipt", required=True)
receipt_verify.add_argument("--log-public-key", required=True) receipt_verify.add_argument("--log-public-key", required=True)
receipt_verify.add_argument("--require-signatures", choices=["ed25519", "both"], default="ed25519") receipt_verify.add_argument("--require-signatures", choices=["ed25519", "both"], default="ed25519")
receipt_verify.add_argument("--slhdsa-public-key", help="Also verify the second (post-quantum, SLH-DSA) head signature against this public key (OpenSSL >= 3.5; heads before tree size 14 report absent, not failed).")
receipt_verify.add_argument("--sth-store", help="Path to the local STH pin store (split-view/rollback defense).") receipt_verify.add_argument("--sth-store", help="Path to the local STH pin store (split-view/rollback defense).")
receipt_verify.add_argument("--consistency-proof", help="File with a hex consistency proof from the pinned tree size (provider: log-consistency).") receipt_verify.add_argument("--consistency-proof", help="File with a hex consistency proof from the pinned tree size (provider: log-consistency).")
receipt_verify.add_argument("--max-sth-age-seconds", type=int, help="Reject signed tree heads older than this (freshness policy).") receipt_verify.add_argument("--max-sth-age-seconds", type=int, help="Reject signed tree heads older than this (freshness policy).")
@ -476,7 +477,8 @@ def cmd_score(args: argparse.Namespace) -> int:
def cmd_receipt_verify(args: argparse.Namespace) -> int: def cmd_receipt_verify(args: argparse.Namespace) -> int:
attestation = load_attestation(args.attestation) attestation = load_attestation(args.attestation)
receipt = load_receipt(args.receipt) receipt = load_receipt(args.receipt)
result = verify_receipt(attestation, receipt, args.log_public_key, require_signatures=args.require_signatures) result = verify_receipt(attestation, receipt, args.log_public_key, require_signatures=args.require_signatures,
slhdsa_public_key_path=args.slhdsa_public_key)
accountability_diagnostics = _log_accountability_checks( accountability_diagnostics = _log_accountability_checks(
receipt, receipt,
sth_store=args.sth_store, sth_store=args.sth_store,

24
src/pacta/transparency.py
View file

@ -256,6 +256,7 @@ def verify_receipt(
receipt: dict[str, Any], receipt: dict[str, Any],
log_public_key_path: str | Path, log_public_key_path: str | Path,
require_signatures: str = "ed25519", require_signatures: str = "ed25519",
slhdsa_public_key_path: str | Path | None = None,
) -> ReceiptVerificationResult: ) -> ReceiptVerificationResult:
diagnostics: list[str] = [] diagnostics: list[str] = []
if receipt.get("type") != RECEIPT_TYPE: if receipt.get("type") != RECEIPT_TYPE:
@ -266,6 +267,29 @@ def verify_receipt(
sth = receipt.get("sth") or {} sth = receipt.get("sth") or {}
sth_ok, sth_diagnostics, statuses = verify_signed_tree_head(sth, log_public_key_path, require_signatures=require_signatures) sth_ok, sth_diagnostics, statuses = verify_signed_tree_head(sth, log_public_key_path, require_signatures=require_signatures)
diagnostics.extend(sth_diagnostics) diagnostics.extend(sth_diagnostics)
if slhdsa_public_key_path is not None:
# The additive post-quantum co-signature (heads from tree size 14
# on). Absent on older heads is NOT a failure - an append-only log
# keeps its history; a present-but-bad signature fails closed.
from .slhdsa import verify_payload_slhdsa
slh = (sth.get("signatures") or {}).get("slh_dsa") or {}
if str(slh.get("status") or "absent") == "signed":
try:
slh_ok, slh_error = verify_payload_slhdsa(
signed_tree_head_payload(sth),
str(slh.get("signature_base64") or ""),
slhdsa_public_key_path,
)
except Exception as exc: # old OpenSSL, unreadable key: fail closed
slh_ok, slh_error = False, f"SLH-DSA verification unavailable: {exc}"
if slh_ok:
statuses["slh_dsa"] = "verified"
else:
statuses["slh_dsa"] = "failed"
diagnostics.append(f"SLH-DSA head co-signature did not verify: {slh_error}")
else:
statuses["slh_dsa"] = "absent"
try: try:
tree_size = int(receipt.get("tree_size")) tree_size = int(receipt.get("tree_size"))
leaf_index = int(receipt.get("leaf_index")) leaf_index = int(receipt.get("leaf_index"))

39
tests/test_transparency.py
View file

@ -145,3 +145,42 @@ def test_requiring_both_signatures_fails_without_ml_dsa_backend(tmp_path):
assert not result.accepted assert not result.accepted
assert result.signatures["ed25519"] == "verified" assert result.signatures["ed25519"] == "verified"
assert result.signatures["ml_dsa"] != "verified" assert result.signatures["ml_dsa"] != "verified"
def test_receipt_verify_checks_slhdsa_cosignature(tmp_path):
# Rung 2 of the site promises both head signatures are checkable;
# this binds the promise to the tool (operator-caught 2026-08-16).
import pytest
from pacta import slhdsa
try:
slhdsa.generate_slhdsa_keypair(tmp_path / "slh.key", tmp_path / "slh.pub")
except Exception:
pytest.skip("OpenSSL without SLH-DSA support on this host")
attestation, private_key, public_key = _signed_attestation(tmp_path)
from pacta.yamlio import dump_data
dump_data(attestation, tmp_path / "attestation.yaml")
log = TransparencyLog(tmp_path / "log")
log.init("local-test-provider", public_key)
receipt = log.append_attestation(
tmp_path / "attestation.yaml", private_key, public_key,
receipt_out=tmp_path / "receipt.yaml",
slhdsa_private_key_path=tmp_path / "slh.key",
slhdsa_public_key_path=tmp_path / "slh.pub",
)
result = verify_receipt(attestation, receipt, public_key,
slhdsa_public_key_path=tmp_path / "slh.pub")
assert result.accepted, result.diagnostics
assert result.signatures["slh_dsa"] == "verified"
tampered = __import__("copy").deepcopy(receipt)
sig = tampered["sth"]["signatures"]["slh_dsa"]["signature_base64"]
import base64 as _b64
raw = bytearray(_b64.b64decode(sig)); raw[0] ^= 0xFF
tampered["sth"]["signatures"]["slh_dsa"]["signature_base64"] = _b64.b64encode(bytes(raw)).decode()
bad = verify_receipt(attestation, tampered, public_key,
slhdsa_public_key_path=tmp_path / "slh.pub")
assert not bad.accepted
assert bad.signatures["slh_dsa"] == "failed"

44
tests/test_web_and_witness.py
View file

@ -80,7 +80,7 @@ def test_web_endpoints_and_online_proof_roundtrip(tmp_path):
with urllib.request.urlopen(base + "/docs", timeout=10) as r: with urllib.request.urlopen(base + "/docs", timeout=10) as r:
page = r.read().decode() page = r.read().decode()
assert "BEGIN PUBLIC KEY" in page assert "BEGIN PUBLIC KEY" in page
assert "pin this key" in page.lower() assert "pin these keys" in page.lower()
# operator-dropped documents: served by bare name, absent from the # operator-dropped documents: served by bare name, absent from the
# endpoint index, traversal-safe # endpoint index, traversal-safe
site = tmp_path / "log" / "site" site = tmp_path / "log" / "site"
@ -181,3 +181,45 @@ def test_webdocs_source_carries_no_stale_paper_claims():
# first-use glosses the page promised: STH and axiom cones # first-use glosses the page promised: STH and axiom cones
assert "Signed Tree Head (STH)" in text assert "Signed Tree Head (STH)" in text
assert "axiom cones (the exact set of assumptions" in text assert "axiom cones (the exact set of assumptions" in text
def test_svg_tree_boxes_never_overlap_or_spill():
# Regression for 2026-08-16: fixed-width leaf boxes shingled once the
# log outgrew the 8-leaf design, and a fixed head box let its caption
# spill. Render the tree at several sizes and assert geometry.
import re
from pacta_provider.webdocs import _svg_tree
class _E:
def __init__(self, i):
self.leaf_hash = f"{i:02x}" * 32
self.leaf = {"attestation": {"subject": {"component": "betrusted-ed25519-verified"},
"certificates": [{"status": "proven", "axiom_status": "clean"}]}}
for n in (8, 19, 33):
svg = _svg_tree([_E(i) for i in range(n)], "ab" * 32, "verified-dalek-serial")
rects = [(float(m.group(1)), float(m.group(2)), float(m.group(3)))
for m in re.finditer(r'<rect x="([-0-9.]+)" y="([0-9.]+)" width="([0-9.]+)"', svg)]
leaf_y = max(y for _, y, _ in rects)
leaves = sorted((x, w) for x, y, w in rects if y == leaf_y)
assert len(leaves) == n
for (x1, w1), (x2, _w2) in zip(leaves, leaves[1:]):
assert x1 + w1 <= x2 + 0.01, f"leaf boxes overlap at n={n}"
# head caption must fit its box: longest line estimated at 5.3px/char
head = re.search(r'<rect x="[-0-9.]+" y="[0-9.]+" width="([0-9.]+)" height="46"', svg)
title = re.search(r'font-weight="bold">([^<]+)</text>', svg).group(1)
assert len(title) * 7.0 <= float(head.group(1)), "head title spills"
def test_openapi_document_served_and_valid():
# The machine interface is published the industry-standard way
# (operator order 2026-08-16: no endpoint box on the human page).
import json as _json
from pacta_provider.web import _openapi_document
doc = _openapi_document("")
assert doc["openapi"].startswith("3.")
assert "/v1/sth" in doc["paths"] and "/log-public-key" in doc["paths"]
_json.dumps(doc) # serializable