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

paper v0.12 + estate: one numbering, everywhere — 0-based leaf indices

Browse source 
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).
This commit is contained in:
mrwulf 2026-08-16 20:04:44 +02:00
parent 24809f8e4d
commit 2517d79f6e
5 changed files with 21 additions and 20 deletions
Show stats Download patch file Download diff file 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

7
paper/README.md
View file

@ -1,12 +1,13 @@
# 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.12, 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 unifies
entry numbering on 0-based leaf indices throughout. 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.

22
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.12}}
\begin{document} \begin{document}
\maketitle \maketitle
@ -146,7 +146,7 @@ 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 log's own accumulator arguments. Thus 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.
@ -171,7 +171,7 @@ 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 four-fork replay generations for the
Ed25519 codebases (the newest at 44 certificates per fork), two attestations Ed25519 codebases (the newest at 44 certificates per fork), 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:
@ -1051,7 +1051,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
@ -1249,7 +1249,7 @@ 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 abstract root-binding lemma from the paper is
@ -1269,7 +1269,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}
@ -1374,7 +1374,7 @@ 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.
@ -1446,7 +1446,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 +1460,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}
@ -1605,8 +1605,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

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

@ -319,7 +319,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.12 — 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,12 +330,12 @@ 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 <div class="card"><strong>Paper and log, one story.</strong> Since the August 2026 revisions the paper
describes this deployment as it runs — nineteen leaves, dual-signed heads, the 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 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 append-only and keeps growing past any paper revision; every number the paper states