site QA sweep: the paper section tells today's truth, old drafts retired

Operator finding 2026-08-15: the live site still said 'v0.9 — frozen
while under journal review' and advertised the superseded v0.1/v0.2
drafts. Fixed at the source:
- webdocs.py paper card: v0.10, revised August 2026 (version now also
  printed on the PDF title page); the divergence description gains its
  closure (the sn=0 conjunct, zero divergences, three-way regression);
  the freeze-era reconciliation card shrunk to a tight snapshot-vs-today
  paragraph; fragile '12 Jupyter lectures' count dropped
- web.py: /paper serves the current paper only; all old-variant routes
  404 (git history retains the drafts); ltl-v0.1/v0.2 files removed from
  the working tree, paper/README updated
- ltl.tex: title page now reads 'Revised: August 2026 — v0.10' (the
  version travels IN the PDF, per operator order); rebuilt
- tests updated to ENFORCE the retirement (all old variants must 404);
  full suite 152 passed

paper/README.md

@@ -1,15 +1,17 @@
 # Which file is current?
 
-**`ltl.pdf` / `ltl.tex` — the current paper.** This is the version
+**`ltl.pdf` / `ltl.tex` — the current paper (v0.10, revised August 2026).**
-submitted to the journal on 2026-07-17 and now frozen during review; the
+The review process concluded in August 2026; this revision folds in the
-live copy served at <https://ltl.zkdefi.org/paper> is byte-identical.
+corrections queued during the freeze (certificate-count update, the
+closed consistency-verifier divergence with its `sn = 0` root cause, a
+replay-harness-integrity limitation, and an added claim-matrix row). The
+version submitted for review (July 17, 2026, sha256 `7f140356…`) is
+preserved unchanged in this repository's git history. The live copy at
+<https://ltl.zkdefi.org/paper> serves the current revision.
 
-The other files are kept as honest history, not as reading material:
+Superseded early drafts (v0.1, v0.2) were removed from the working tree
-
+on 2026-08-15; like every prior state of this folder, they remain
-| File | What it is |
+retrievable from this repository's git history.
-|---|---|
-| `ltl-v0.1.pdf` / `.tex` | early 4-page draft (July 2026), superseded |
-| `ltl-v0.2.pdf` / `.tex` | 19-page system-report draft, superseded by a full rewrite |
 
 Revisions v0.3–v0.9 were successive overwrites of `ltl.tex`; they live in
 this repository's git history. v0.9 is the submitted version — the

paper/ltl-v0.1.tex

@@ -1,481 +0,0 @@
-\documentclass[10pt,twocolumn]{article}
-\usepackage[margin=1.7cm,bottom=1.95cm]{geometry}
-\usepackage[T1]{fontenc}
-\usepackage{lmodern}
-\usepackage{microtype}
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{booktabs}
-\usepackage{tikz}
-\usetikzlibrary{arrows.meta}
-\usepackage[hidelinks]{hyperref}
-\usepackage{xcolor}
-\newcommand{\code}[1]{\texttt{\small #1}}
-% poor-man's semantic brackets (stmaryrd unavailable in minimal TeX trees)
-\newcommand{\den}[1]{[\![#1]\!]}
-\setlength{\columnsep}{0.8cm}
-
-\title{\textbf{LTL: Lean Transparency Log}\\[2pt]
-\large Where Deductive and Cryptographic Proof Vouch for Each Other}
-\author{Olaf Horvath\\ \small \texttt{Olaf.Horvath@zkdefi.org} --- \url{ltl.zkdefi.org} --- \href{https://orcid.org/0009-0004-8008-5805}{ORCID 0009-0004-8008-5805}}
-\date{July 2026}
-
-\begin{document}
-\maketitle
-
-\begin{abstract}
-Interactive theorem provers can certify the functional correctness of
-deployed cryptographic code, but the resulting assurance is expensive to
-\emph{consume}: re-checking a realistic proof corpus takes a proof
-toolchain and hours of kernel time, which excludes almost every
-downstream user, including autonomous agents that must decide which
-cryptographic library to trust. We describe the \emph{Lean Transparency
-Log} (LTL)\footnote{Not to be confused with linear temporal
-logic~\cite{pnueli77}; the collision is acknowledged and, in a paper
-about verification, difficult to resist.}, a deployed RFC~9162-style
-transparency log whose leaves are \emph{replay attestations}: signed
-statements that the Lean~4 proofs of a specific Rust repository, at a
-specific git commit, re-check with exactly their documented axiom sets.
-Consumers verify one signature and a logarithmic inclusion proof in
-milliseconds; the hours of kernel time are paid once, by the log
-operator. Three design decisions distinguish the LTL from prior
-attestation transparency systems: (i)~consumers re-derive verification
-verdicts locally from the \emph{observed axiom cones} carried in each
-attestation, so the operator is trusted for observations, never for
-verdicts; (ii)~axiom cones are matched against per-theorem
-\emph{documented boundaries} exactly, in both directions; and (iii)~the
-log's tree heads are signed by a binary built from the very Ed25519
-implementation whose correctness certificates are leaves of the log, and
-each signature embeds the operator's own Merkle self-check of that leaf.
-We report a small production deployment covering four verified
-production Ed25519 implementations, describe what the accumulated
-evidence does and does not establish, and outline the natural next step:
-verifying the log's own proof-checking algorithms in Lean and entering
-those certificates into the log they defend.
-\end{abstract}
-
-\section{Introduction}
-\label{sec:intro}
-
-Formal verification of deployed cryptographic code has matured from
-research prototypes to substantial artifacts: verified-by-construction
-libraries such as HACL*~\cite{hacl} and Fiat-Crypto~\cite{fiatcrypto}
-ship in mainstream software, and post-hoc verification pipelines such as
-Aeneas~\cite{aeneas} make it possible to state and prove theorems about
-\emph{existing} production Rust code. The corpus underlying this paper
-is of the latter kind: four production Ed25519
-implementations---upstream \code{curve25519-dalek}/\code{ed25519-dalek}
-and three deployed forks (Solana, RISC~Zero, Betrusted)---each carry
-Lean~4~\cite{lean4} certificates, proven against that fork's own
-extracted model, covering field arithmetic over $\mathbb{F}_{2^{255}-19}$,
-the complete twisted Edwards laws~\cite{bernsteinlange,twisted}, scalar
-arithmetic mod $\ell$, encoding/decoding with constructive point
-decompression, and a four-tier characterization of signature
-verification~\cite{ed25519,rfc8032} whose strongest tier states: the
-extracted verifier accepts iff the signature's $R$ component decompresses
-to a valid curve point equal to $[k](-A)+[s]B$.
-
-\paragraph{What the certificates state.} Concretely, the corpus is a
-stack of theorems about extracted code, each stated through a
-\emph{denotation} from machine representation to mathematics. Field
-elements are five 51-bit limbs denoting
-$\den{(a_0,\dots,a_4)}=\sum_i a_i2^{51i}\bmod p$, and every
-operation carries a two-clause specification---the value is right
-\emph{and} the representation invariant is preserved, e.g.
-\begin{align*}
-\footnotesize
-\forall a\,b.\ &\mathrm{bnd}\,a \Rightarrow \mathrm{bnd}\,b \Rightarrow{}\\[-2pt]
-&\exists c.\ \code{mul}\,a\,b = \code{ok}\,c \,\wedge\, \mathrm{bnd}\,c
-\,\wedge\, \den{c} = \den{a}\cdot\den{b}.
-\end{align*}
-Point operations are proven to implement the complete twisted Edwards
-addition law on
-$E : -x^2+y^2 = 1+d\,x^2y^2$ over $\mathbb{F}_p$,
-\begin{equation*}
-\small
-(x_1,y_1)+(x_2,y_2)=
-\Bigl(\tfrac{x_1y_2+x_2y_1}{1+d\,x_1x_2y_1y_2},\;
-\tfrac{y_1y_2+x_1x_2}{1-d\,x_1x_2y_1y_2}\Bigr),
-\end{equation*}
-including the completeness fact that makes it branch-free ($a=-1$ is a
-square and $d$ a non-square in $\mathbb{F}_p$, so the denominators never
-vanish~\cite{bernsteinlange}).
-At the apex, writing $\code{accept}(A,m,R,s)$ for ``the extracted
-verifier returns \code{ok}'', with $k$ the scalar produced by the hash
-oracle $H(R,A,m)$ and no properties assumed of $H$, the byte-level tier
-states
-\begin{equation*}
-\footnotesize
-\code{accept}(A,m,R,s) \;\Leftrightarrow\; \code{compress}([s]B-[k]A) = R,
-\end{equation*}
-and the strongest tier lifts byte equality to the group:
-\begin{equation*}
-\footnotesize
-\code{accept}(A,m,R,s) \;\Leftrightarrow\; \code{decompress}(R) = [k](-A)+[s]B,
-\end{equation*}
-with decompression itself proven (exact byte parsing, the
-$(p{+}3)/8$-power square root, sign-bit root selection). Each theorem's
-axiom cone is pinned exactly---the standard three below the apex, the
-enumerated oracle boundary at the apex tiers.
-
-The economics of \emph{consuming} such evidence are poor: re-checking
-one fork's certificates takes $\approx$30 minutes of Lean kernel time
-and a pinned toolchain. A wallet, a package manager, or an autonomous
-agent choosing a cryptographic backend cannot pay this per
-decision---and need not: a deterministic re-check yields a fact that can
-be attested once and distributed.
-
-This is the classic transparency-log trade---Certificate
-Transparency~\cite{rfc6962,rfc9162} for certificate issuance, Sigstore's
-Rekor~\cite{sigstore} for signing events and supply-chain
-attestations~\cite{intoto}, key transparency~\cite{coniks}, checksum
-databases---applied to a payload with different trust semantics:
-\emph{evidence of machine-checked mathematical truth, together with its
-exact assumption set}. We claim no novelty for any component (the hash
-structure and proof algorithms are RFC~9162 verbatim); the contribution
-is the composition, its trust model, and a deployed, reproducible
-instance. The LTL does not mechanize cryptographic security
-proofs---that inter-disciplinary bridge is already being built by
-EasyCrypt and its relatives~\cite{easycrypt}. It bridges the adjacent,
-mostly empty gap: type-theory-certified artifacts have no distribution
-infrastructure, and cryptographic transparency infrastructure has never
-carried kernel-checked mathematics---each discipline solving the
-other's problem.
-
-\S\ref{sec:log} describes the log and its trust model,
-\S\ref{sec:dogfood} the self-referential signing loop,
-\S\ref{sec:deploy} the deployment and what its evidence establishes,
-and \S\ref{sec:next} the verification agenda for the log itself.
-
-\section{The Lean Transparency Log}
-\label{sec:log}
-
-\begin{figure*}[t]
-\centering
-\begin{tikzpicture}[every node/.style={font=\small}]
-  \tikzset{box/.style={draw, rounded corners=2pt, minimum width=1.6cm, minimum height=0.56cm}}
-  % leaves: 0-3 failed run (gray), 4-7 verified (black)
-  \foreach \i/\c in {0/gray, 1/gray, 2/gray, 3/gray, 4/black, 5/black, 6/black, 7/black}
-    \node[box, draw=\c, text=\c] (l\i) at (\i*2.05,0) {leaf \i};
-  \node[box, draw=black, very thick, fill=black!6] at (4*2.05,0) {\textbf{leaf 4}};
-  \node[text=gray, font=\footnotesize] at (3*2.05/2 - 1.02,-0.62) {failed-audit run --- retained forever};
-  \node[font=\footnotesize] at (5.5*2.05 + 0.35,-0.62) {verified attestations (16/16, boundary-exact)};
-  % internal nodes
-  \foreach \i in {0,...,3}
-    \node[box] (m\i) at (\i*4.1+1.025,1.25) {node};
-  \foreach \i in {0,1}
-    \node[box] (n\i) at (\i*8.2+3.075,2.5) {node};
-  \node[box, thick] (root) at (7.175,3.75) {root};
-  \foreach \a/\b in {l0/m0, l1/m0, l2/m1, l3/m1, l4/m2, l5/m2, l6/m3, l7/m3,
-                     m0/n0, m1/n0, m2/n1, m3/n1, n0/root, n1/root}
-    \draw[gray!70] (\a) -- (\b);
-  % signature head
-  \node[box, thick, minimum width=5.2cm] (sig) at (7.175,4.95)
-    {signed tree head: $\mathrm{Ed25519}(\mathrm{root})$};
-  \draw[-{Stealth}] (root) -- (sig);
-  % the self-certification loop, routed through clear space on the right
-  \draw[-{Stealth}, thick, dashed]
-    (sig.east) .. controls (13.2,4.95) and (12.4,1.6) .. (l4.north east);
-  \node[align=left, font=\footnotesize, anchor=west] at (12.45,3.1)
-    {signed by the binary built\\ from the source attested at\\ leaf 4; the operator verifies\\ that leaf's inclusion first};
-\end{tikzpicture}
-\caption{The deployed 8-leaf log. Leaves 0--3 record an early replay whose
-audit step failed (two tooling defects, since fixed); an append-only ledger
-retains them. The tree head is signed by a binary built from the
-implementation attested at leaf 4, and each signature embeds the operator's
-own inclusion check of that leaf against the tree being signed.}
-\label{fig:loop}
-\end{figure*}
-
-\paragraph{Roles.} The system has exactly two roles with deliberately
-asymmetric costs and capabilities. The \emph{operator} (one per log)
-owns a Lean toolchain, replays proof corpora, holds the log's signing
-key, and bears append-only obligations. \emph{Consumers} (unbounded)
-hold the operator's public key, receive small evidence files, and verify
-with $\approx$25 lines of standard-library code. Nothing a consumer does
-requires a theorem prover.
-
-\paragraph{Leaves: replay attestations.} A leaf is the canonical JSON
-serialization of an attestation recording: the subject repository URL
-and \emph{git commit} (which cryptographically pins the entire source
-tree); the toolchain versions; the resource-control regime under which
-the replay ran; and, per certificate, its name, replay status, and the
-\emph{observed axiom cone}---the exact output of Lean's
-\code{\#print axioms} for that theorem. For the corpus above each
-attestation carries 16 certificates.
-
-\paragraph{Boundary-exact auditing.} Every certificate has a
-\emph{documented} allowed axiom set. Foundational certificates must
-carry exactly Lean's three standard axioms
-(\code{propext}, \code{Classical.choice}, \code{Quot.sound}); the four
-signature-tier certificates additionally carry a per-fork, explicitly
-enumerated boundary (an opaque SHA-512 oracle and opaque wire-format
-types---e.g., eleven axioms in total for the upstream fork). A cone is
-\emph{clean} iff it equals its allowed set; deviation in either
-direction---an unexpected axiom, or a missing boundary axiom---is
-flagged. Each source repository enforces the same discipline in its own
-check scripts; the log mirrors those sets and treats the repositories'
-scripts as authoritative.
-
-\paragraph{Observation, not verdict.} Attestations include the
-operator's pass/fail judgment, but consumers ignore it: the consumer's
-tooling re-derives every verdict locally by comparing the
-\emph{observed} cone against the consumer's own copy of the allowed
-sets. An operator that labels a dirty cone ``clean'' gains nothing; an
-attestation that omits observed cones is treated as unverifiable. This
-narrows the trust placed in the operator to: ``the reported
-\code{\#print axioms} output is what the kernel printed for this commit.''
-
-\paragraph{Tree, heads, receipts.} Leaves are accumulated in an
-RFC~9162 Merkle tree ($\mathrm{SHA}$-256 with $0x00/0x01$
-leaf/node domain separation). The operator signs tree heads; consumers
-receive a \emph{receipt}: leaf index, sibling path, and the signed head.
-Consumers additionally maintain a local pin store: same-size heads must
-match the pinned root exactly (a mismatch is reported as equivocation
-and is unrecoverable); growth requires a verified consistency proof from
-the pinned size; shrinkage is rejected. A freshness policy bounds head
-age. The full log is also published as a git repository (one file per
-leaf, plus every head ever signed), so any cloner can recompute every
-prefix root from the public leaves and audit the complete head history
-without consistency proofs---a low-infrastructure witness
-mechanism~\cite{rfc9162}; a standalone $\approx$150-line
-standard-library verifier ships in the mirror.
-
-\section{The self-certifying signature}
-\label{sec:dogfood}
-
-Tree heads are Ed25519 signatures, and this creates an opportunity for
-coherence: the log \emph{contains} correctness certificates for an
-Ed25519 implementation. The LTL's heads are therefore signed by a binary
-built from the pinned source tree of exactly the implementation attested
-in the log (serial backend pinned, matching the verified extraction),
-and---before signing---the operator runs the same Merkle inclusion
-verification a consumer runs, on the newest leaf attesting the signing
-implementation, against the tree about to be signed. The verdict is
-embedded in the signature block:
-
-{\small
-\begin{verbatim}
-signing_backend: verified-dalek-serial
-signing_library_source_commit: aa0f6ab...
-signing_library_leaf_index: 4
-signing_library_certificates_proven: 16/16
-self_inclusion: verified
-\end{verbatim}}
-
-\noindent The signature vouches for the tree; the tree vouches for the
-code that produced the signature; and the two vouchings are different
-proof modalities (cryptographic and deductive), so the loop is
-self-referential without being circular
-(Fig.~\ref{fig:loop}). We state the honest extent of this claim
-precisely: the Lean certificates cover the \emph{verification} path of
-the library (the theorems' subject is the extraction image of that
-path); the \emph{signing} path is not covered by any certificate and is
-declared trusted base---the design merely ensures the trusted signing
-code is the attested artifact rather than an unrelated third
-implementation, and that consumers can check as much. Signature
-\emph{verification} on consumer machines can optionally run through the
-same certified-source binary, with the backend that actually ran
-recorded in every result and a fail-closed policy flag available.
-First-append bootstrapping is handled honestly: heads signed before the
-signing library's attestation enters the log record
-\code{self\_inclusion:\ library\_not\_in\_log}.
-
-
-
-\section{Deployment and evidence}
-\label{sec:deploy}
-
-The LTL is deployed\footnote{Service:
-\url{https://ltl.zkdefi.org} (read-only HTTP API and
-documentation). Mirror: \url{https://github.com/saymrwulf/lean-transparency-log}.
-Operator/consumer tooling and a twelve-lecture course:
-\url{https://github.com/saymrwulf/proof-aware-crypto-tooling-agent}. The
-underlying proof corpora are in the \code{saymrwulf/*-ed25519-verified}
-repositories; every claim in this paper is re-checkable from these
-artifacts.} with eight leaves: one attestation per fork from each of two
-full replay runs (58--64 Lean files and $\approx$1{,}800\,s per
-fork, under hard memory caps and core pinning). In the second run all
-four forks reported 16/16 certificates proven with boundary-exact cones,
-pinned to exact commits. The first run is deliberately still in the log: its audit step
-failed due to two defects in the \emph{operator tooling} (a path issue
-and a parser that mishandled Lean's line-wrapped axiom lists for the
-eleven-axiom cones), and the operator signed attestations recording the
-failure rather than suppressing the run. We consider the resulting
-ledger---four failure leaves permanently beside four success
-leaves---a feature of the trust model, and note that both defects were
-fail-closed: valid proofs were rejected; invalid ones were never
-accepted.
-
-\paragraph{What a verified receipt establishes.} Under the assumptions
-enumerated below, a consumer who verifies a receipt knows: \emph{the
-operator whose key I pinned attests that the Lean certificates of
-repository $X$ at commit $Y$ re-check, with per-certificate observed
-axiom cones as included---and this statement is part of the log
-presented to every other consumer}. Combined with local verdict
-re-derivation, this yields source-level assurance for the pinned
-commit. It deliberately does \emph{not} establish: correctness of any
-binary (consumers build from the pinned source; compilers are trusted
-base), correctness of SHA-512 (an opaque oracle in the theorems),
-correctness of the wire-format parsers (their outcomes are hypotheses of
-the signature tiers), signing-side correctness, or side-channel
-properties. The assumption set, in full: the Lean kernel and its three
-axioms plus mathlib; faithfulness of the Charon/Aeneas
-extraction~\cite{aeneas}; each fork's documented oracle boundary;
-operator key custody and the trust-on-first-use key distribution
-(mitigated by publishing the key in two independent locations);
-collision resistance of SHA-256 for the log; unforgeability of Ed25519
-for the heads; and the consumer's own $\approx$25-line verifier.
-
-\paragraph{An observational by-product: proof portability.} Because the
-four corpora prove the same theorems against four independent
-extractions, the diff between proof files measures how portable proofs
-are across real forks. Pure-mathematics files (e.g., a carry-telescope
-lemma file) are byte-identical across all four; extraction-facing proof
-scripts diverge sharply where the forks' code or the extractor's naming
-differs (e.g., 215 changed lines for the byte-parser proofs on the two
-forks whose extraction produces a closure-based loader; 121 lines for
-the signature-glue proofs on the same-crate fork; 27 lines---all
-annotation---between the two structurally closest forks, documenting the
-one fork's \code{black\_box} optimization barrier). Per-target
-verification, in other words, is doing measurable work exactly where the
-targets actually differ.
-
-\section{Related work}
-\label{sec:related}
-
-Certificate Transparency~\cite{rfc6962,rfc9162} supplies the data
-structure and proof algorithms, used here unchanged. Rekor within
-Sigstore~\cite{sigstore} is the closest deployed system: a transparency
-log over signing events and supply-chain attestations such as
-in-toto~\cite{intoto} link metadata; its payloads attest \emph{process}
-(who signed, how an artifact was built), whereas LTL leaves attest
-kernel-checked \emph{mathematical statements together with their
-assumption sets}, and the consumer re-derives verdicts rather than
-trusting labels. Key transparency~\cite{coniks} and checksum databases
-share the pattern with different payloads. Proof-carrying
-code~\cite{pcc} ships proofs to consumers who check them; the LTL serves
-consumers who cannot run any checker, replacing proof transport with
-attestation, inclusion, and signature---at the cost of trusting the
-operator's kernel run, a cost the design minimizes but does not
-eliminate. Cheval, Moreira and Ryan formally verify transparency
-protocols themselves~\cite{cheval}; our direction is the complement
-(we log the verification), and \S\ref{sec:next} proposes meeting in the
-middle. Verified Merkle tree \emph{implementations} exist, notably in
-EverCrypt~\cite{evercrypt}; \S\ref{sec:next} builds on that precedent
-rather than claiming it.
-
-\section{Limitations and next steps}
-\label{sec:next}
-
-\paragraph{Limitations.} The deployment is small (one operator, eight
-leaves, four subject repositories) and the operator is a single party;
-split-view defense currently rests on consumer-side pinning plus the
-public git mirror rather than an independent witness network. Key
-distribution is trust-on-first-use. The signing path of the dogfood
-binary is unverified (declared, not proven). The corpus itself stops at
-source-level assurance---reproducible builds and side-channel evidence
-remain open---and ML-DSA slots in the head format are deliberately
-recorded as unavailable rather than backed by an unverified
-implementation.
-
-\paragraph{Verifying the accumulator itself.} The natural next step
-applies the corpus's own discipline to the log's cryptographic half,
-which is currently the \emph{unproven} half of the composition. All of
-the following are tractable Lean targets: (i)~completeness of the
-RFC~9162 inclusion verifier (honest proofs verify---no assumptions);
-(ii)~\emph{soundness as an explicit reduction}: an accepting inclusion
-proof for a leaf outside the tree yields a SHA-256 collision, making
-collision resistance a documented boundary axiom audited exactly like
-the SHA-512 oracle in the Ed25519 tiers; (iii)~the analogous statement
-for the consistency verifier (acceptance implies prefix, modulo
-collisions); (iv)~domain separation as a lemma; and (v)~total
-correctness of the consumer's pin-store state machine (equivocation
-detection, rollback rejection). Verified Merkle implementations in
-F*~\cite{evercrypt} and algorithm verifications in other systems show
-these proofs are well within reach; the LTL-specific closure is
-\emph{where the certificates go}: into the log they defend, checked by
-the certified checker they specify, alongside a consumer policy flag
-requiring the certified verifier. At that point both proving traditions
-in the composition run on certified code, and the remaining trusted base
-is two hash assumptions, a compiler, an extraction pipeline, and one
-key.
-
-\paragraph*{Acknowledgments.} The proof corpora, tooling, deployment,
-and this paper were produced with substantial assistance from Claude
-(Anthropic). All claims are enforced by the referenced check scripts and
-are independently re-checkable from the public artifacts.
-
-\begin{thebibliography}{19}\scriptsize
-\setlength{\itemsep}{1pt}
-
-\bibitem{rfc6962} B.~Laurie, A.~Langley, E.~K\"asper.
-\emph{Certificate Transparency}. RFC 6962, 2013.
-
-\bibitem{rfc9162} B.~Laurie, E.~Messeri, R.~Stradling.
-\emph{Certificate Transparency Version 2.0}. RFC 9162, 2021.
-
-\bibitem{sigstore} Z.~Newman, J.~S.~Meyers, S.~Torres-Arias.
-Sigstore: Software Signing for Everybody.
-\emph{ACM CCS}, pp.~2353--2367, 2022.
-
-\bibitem{intoto} S.~Torres-Arias, H.~Afzali, T.~K.~Kuppusamy,
-R.~Curtmola, J.~Cappos. in-toto: Providing farm-to-table guarantees for
-bits and bytes. \emph{USENIX Security}, 2019.
-
-\bibitem{coniks} M.~S.~Melara, A.~Blankstein, J.~Bonneau,
-E.~W.~Felten, M.~J.~Freedman. CONIKS: Bringing Key Transparency to End
-Users. \emph{USENIX Security}, 2015.
-
-\bibitem{pcc} G.~C.~Necula. Proof-Carrying Code.
-\emph{ACM POPL}, pp.~106--119, 1997.
-
-\bibitem{cheval} V.~Cheval, J.~Moreira, M.~Ryan.
-Automatic verification of transparency protocols.
-\emph{IEEE EuroS\&P}, 2023. arXiv:2303.04500.
-
-\bibitem{easycrypt} G.~Barthe, B.~Gr\'egoire, S.~Heraud,
-S.~Zanella~B\'eguelin. Computer-Aided Security Proofs for the Working
-Cryptographer. \emph{CRYPTO}, LNCS 6841, pp.~71--90, 2011.
-
-\bibitem{aeneas} S.~Ho, J.~Protzenko.
-Aeneas: Rust verification by functional translation.
-\emph{Proc.\ ACM Program.\ Lang.} 6 (ICFP): 711--741, 2022.
-
-\bibitem{lean4} L.~de~Moura, S.~Ullrich.
-The Lean 4 Theorem Prover and Programming Language.
-\emph{CADE-28}, LNCS 12699, pp.~625--635, 2021.
-
-\bibitem{hacl} J.-K.~Zinzindohou\'e, K.~Bhargavan, J.~Protzenko,
-B.~Beurdouche. HACL*: A Verified Modern Cryptographic Library.
-\emph{ACM CCS}, 2017.
-
-\bibitem{evercrypt} J.~Protzenko et al.
-EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
-\emph{IEEE S\&P}, 2020.
-
-\bibitem{fiatcrypto} A.~Erbsen, J.~Philipoom, J.~Gross, R.~Sloan,
-A.~Chlipala. Simple High-Level Code for Cryptographic Arithmetic---With
-Proofs, Without Compromises. \emph{IEEE S\&P}, pp.~1202--1219, 2019.
-
-\bibitem{ed25519} D.~J.~Bernstein, N.~Duif, T.~Lange, P.~Schwabe,
-B.-Y.~Yang. High-speed high-security signatures.
-\emph{J.\ Cryptographic Engineering} 2(2): 77--89, 2012.
-
-\bibitem{rfc8032} S.~Josefsson, I.~Liusvaara.
-\emph{Edwards-Curve Digital Signature Algorithm (EdDSA)}. RFC 8032, 2017.
-
-\bibitem{bernsteinlange} D.~J.~Bernstein, T.~Lange.
-Faster addition and doubling on elliptic curves.
-\emph{ASIACRYPT}, LNCS 4833, pp.~29--50, 2007.
-
-\bibitem{twisted} D.~J.~Bernstein, P.~Birkner, M.~Joye, T.~Lange,
-C.~Peters. Twisted Edwards curves.
-\emph{AFRICACRYPT}, LNCS 5023, pp.~389--405, 2008.
-
-\bibitem{pnueli77} A.~Pnueli. The temporal logic of programs.
-\emph{IEEE FOCS}, pp.~46--57, 1977.
-
-\end{thebibliography}
-
-\end{document}

paper/ltl.tex

@@ -47,7 +47,7 @@ showstringspaces=false,breaklines=true,xleftmargin=.5em,xrightmargin=.5em}
 \large A Transparency Model and the Lean Transparency Log}
 \author{Olaf Horvath\\
 \small Olaf.Horvath@zkdefi.org \quad ORCID 0009-0004-8008-5805}
-\date{July 2026}
+\date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.10}}
 
 \begin{document}
 \maketitle
@@ -174,7 +174,11 @@ verifier and the recursive model proved in Lean are not extensionally equal:
 there are malformed size/root combinations accepted only by the deployed
 verifier. We characterize 3,867 divergences in 73,573 pinned boundary tests
 --- every one deployed-accepts-only --- and scope the public attestation
-accordingly.
+accordingly. (Post-submission closure, July 2026: the divergence was traced to
+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
+pinned family, confirmed by a three-way regression against an independent
+faithful RFC transliteration.)
 \end{enumerate}
 
 \paragraph{Non-claims.}
@@ -375,7 +379,8 @@ EUF-CMA security of the head-signature scheme, and correct initial acquisition
 of the operator public key.
 
 The model deliberately does not cryptographically exclude fabricated kernel
-observations. That is a statement about a physical execution on the operator's
+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
 machine. The mechanism instead makes the claimed execution target precise
 enough for a third party to replay.
 
@@ -621,6 +626,10 @@ reconstruction with the supplied old root and consults the size claims only as
 bit-navigation state, so several distinct old-size claims navigate one proof
 identically. In 73,573 lied-size boundary cases, 3,867 divergences were
 observed; all were one-sided (deployed accepts, recursive model rejects).
+The root cause was later identified and closed: the deployed loop omitted
+RFC~9162 \S2.1.4.2 Step~7's terminal $sn=0$ condition; with the conjunct
+restored the pinned family shows zero divergences (three-way regression:
+deployed verifier, recursive model, independent RFC transliteration).
 
 The intended consumer flow binds $(n_0,r_0)$ in local persistent state and
 binds $(n_1,r_1)$ together in a signed head. The present corpus does not prove
@@ -1045,7 +1054,9 @@ for a large class of safe Rust programs~\cite{aeneas}. A recent independent
 experience report likewise applies a Rust-to-Lean pipeline to cryptographic
 code~\cite{klaus2026}.
 
-Each fork's corpus contains sixteen reviewed certificates covering:
+Each fork's corpus contained sixteen reviewed certificates at the
+historical leaves studied here (the corpora have since grown to forty-four
+per fork --- the log records both generations as separate leaves), covering:
 \begin{itemize}[leftmargin=1.6em,itemsep=2pt]
 \item five-limb field arithmetic over $\Fp$ with value and bound preservation;
 \item complete twisted-Edwards group operations~\cite{edwards,twisted};
@@ -1224,7 +1235,9 @@ stable regression boundary.
 
 \begin{remark}[Model/deployment seam]
 For malformed size claims, the deployed iterative verifier and the recursive
-model are not extensionally equal. In all 3,867 divergences observed across
+model are not extensionally equal (figures are the pre-closure measurement;
+the $sn=0$ restoration reduces the divergence count in this family to zero).
+In all 3,867 divergences observed across
 the pinned families the deployed verifier accepted and the model rejected; the
 reverse direction was not observed, and no global inclusion relation between
 the two acceptance sets is claimed.
@@ -1307,6 +1320,14 @@ A malicious operator can fabricate a replay report. Signatures and Merkle
 proofs make the lie attributable and persistent; they do not make it true.
 Targeted independent replay is the corrective mechanism.
 
+\paragraph{Replay-harness integrity.}
+A wrong observation needs no malice: a defective replay harness --- a bug in
+the audit driver, a fail-open guard, a truncated transcript --- produces the
+same evidentiary damage as a dishonest operator, with the same accountability
+answer (the record is attributable and persistent; independent replay corrects
+it). The subject corpus's adversarial gate self-tests exist for exactly this
+reason and reduce, but cannot eliminate, the exposure.
+
 \paragraph{Theorem identity.}
 Names and repository commits are not canonical semantic identifiers, and
 commit identifiers are SHA-1-based --- a weaker binding than the log's own
@@ -1494,6 +1515,7 @@ Equal-size unequal roots in one log context conflict & two valid signatures & co
 Observed cone matches local boundary policy & exact set equality & semantic identity of named declarations \\
 Operator claims the kernel produced the observation & attestation signature and leaf inclusion & correct provider key; EUF-CMA \\
 Kernel actually produced the recorded observation & not cryptographically established; independently checkable by replay & operator and replay-pipeline honesty, or faithful independent replay \\
+Recorded cone was produced by an audit that performed its checks & not established --- the audit driver is itself part of the replay pipeline & audit-gate integrity; adversarial gate self-tests reduce this exposure, they do not eliminate it \\
 Source corresponds to deployed binary & not established & reproducible build and compiler assurance \\
 Claimed signer implementation produced STH & not established & execution provenance \\
 \bottomrule

provider/src/pacta_provider/web.py

@@ -45,17 +45,11 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
 
             if route in ("/", "/docs"):
                 self._send_html(docs_html)
-            elif route in ("/paper", "/paper/ltl.pdf",
+            elif route in ("/paper", "/paper/ltl.pdf"):
-                           "/paper/v0.1", "/paper/v0.1/ltl.pdf",
+                # /paper serves the current paper only (v0.10, revised
-                           "/paper/v0.2", "/paper/v0.2/ltl.pdf"):
+                # August 2026). Superseded drafts were retired from the
-                # /paper is the current paper; /paper/v0.N are prior versions,
+                # site 2026-08-15; git history retains them.
-                # preserved for citability, linked from the docs page.
+                body = paper_pdfs.get("current")
-                variant = "current"
-                if route.startswith("/paper/v0.1"):
-                    variant = "v0.1"
-                elif route.startswith("/paper/v0.2"):
-                    variant = "v0.2"
-                body = paper_pdfs.get(variant)
                 if body is None:
                     self._send(404, {"error": f"paper ({variant}) not available on this deployment"})
                     return
@@ -235,9 +229,7 @@ def serve(
         docs_html = render_docs(log, base_path)
     paper_dir = Path(__file__).resolve().parents[3] / "paper"
     variants = {
-        "current": paper_dir / "ltl.pdf",       # v0.9 submitted version, under review
+        "current": paper_dir / "ltl.pdf",       # v0.10, revised August 2026
-        "v0.1": paper_dir / "ltl-v0.1.pdf",     # prior 4-page version
-        "v0.2": paper_dir / "ltl-v0.2.pdf",     # prior 19-page system report
     }
     paper_pdfs = {name: p.read_bytes() for name, p in variants.items() if p.is_file()}
     handler = make_handler(log, base_path, docs_html, paper_pdfs)

provider/src/pacta_provider/webdocs.py

@@ -318,40 +318,27 @@ our roadmap.</strong> (The full walk-through is lecture&nbsp;11 in the
 <h2>The paper</h2>
 <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>
-(PDF, 23 pages, v0.9 — <strong>frozen while under journal review</strong>; it describes the
+(PDF, 23 pages, <strong>v0.10 — revised August&nbsp;2026</strong>; the version is printed on the
-log as of its 16&nbsp;July&nbsp;2026 snapshot) — 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
 acceptance), collision-extracting soundness for inclusion and consistency, scheme-level
 accountability GAMES with an explicit composition theorem (head authenticity, position
 binding, history binding with a fully proved prefix-transport induction, context-scoped
 fork evidence — all discharged by named reductions), the policy boundary where
-operator labels can veto but never grant acceptance, the then-thirteen-leaf deployment
+operator labels can veto but never grant acceptance, and the measured model/deployment
-whose entry 13 attests the accumulator's own mechanized model, and the measured
+divergence reported as a result rather than hidden — now together with its closure: the
-model/deployment divergence (3,867 lied-size cases, every one accepted only by the
+divergence traced to one omitted RFC&nbsp;9162 conjunct (Step&nbsp;7's <code>sn&nbsp;=&nbsp;0</code>),
-deployed verifier) reported as a result rather than hidden.
+zero divergences after the one-line restoration, confirmed by a three-way regression.</div>
-<span class="muted">Previous versions: <a href="{base}/paper/v0.2">v0.2</a> (19 pages, the
-system report) · <a href="{base}/paper/v0.1">v0.1</a> (4 pages).</span></div>
 
-<div class="card"><strong>Reading the paper against today's log.</strong> The paper is frozen
+<div class="card"><strong>The paper's snapshot vs. today's log.</strong> The paper analyses
-under review; the log is append-only and has kept moving. Nothing the paper describes was
+the log's 16&nbsp;July&nbsp;2026 snapshot — thirteen leaves, still leaves&nbsp;0–12 today,
-altered, so every number in it remains checkable against the live history: the thirteen leaves
+byte-identical, its pinned head still head&nbsp;#5 of <code>sth-history.jsonl</code>. Everything
-it analyses are still leaves 0–12, byte-identical, and the head it pins (tree&nbsp;13, root
+since is additive: the four Ed25519 corpora re-attested at 44 certificates each
-<code>3488a2d0…</code>) is still head&nbsp;#5 of <code>sth-history.jsonl</code> —
+(leaves&nbsp;13–16), the accumulator's hardened model (leaf&nbsp;17), the first post-quantum
+subject (leaf&nbsp;18), and dual-signed heads from tree&nbsp;14 on.
 <code>python3 verify.py --all</code> re-verifies the paper-era prefix together with everything
-after it. What has moved since the snapshot is additive: leaves&nbsp;13–16 re-attest the four
+after it.</div>
-Ed25519 libraries at 44 certificates each (the paper's sixteen-certificate corpora describe the
-leaf&nbsp;8–11 generation, which those leaves still record); leaf&nbsp;17 re-attests the
-accumulator's mechanized model at its hardened state; and leaf&nbsp;18 is the log's first
-post-quantum subject, the SLH-DSA-SHA2-128s verify path. Heads from tree&nbsp;14 on carry an
-additive SLH-DSA signature beside the Ed25519 signature the paper describes; earlier heads have
-none, by design, and the verifier reports them as <code>ABSENT</code> rather than failing them.
-One result has changed in the good direction: the 3,867-case model/deployment divergence the
-paper honestly reports was closed on 23&nbsp;July&nbsp;2026 (the <code>sn==0</code> fix); the
-current pinned divergence count is 0, and both the divergence and its fix are part of the
-retained record. Where the paper and the live log disagree on a number, the paper is describing
-its snapshot — and the log's history contains that snapshot, unchanged, inside it.</div>
 
 <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 course (12 Jupyter
+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>
-lectures) live in the <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a>.</p>
 </body></html>"""

tests/test_paper_verifiers.py

@@ -1,5 +1,5 @@
 """Historical regression pin from the archived v0.2 system report
-(hosted at /paper/v0.2), which cited these exact differential-testing
+(retrievable from paper/ git history; retired from the site 2026-08-15), which cited these exact differential-testing
 counts (164,479 inclusion; 164,224 consistency) for its recursive forms
 against the deployed iterative RFC 9162 verifiers over these families.
 The CURRENT paper makes no extensional-equality claim: it cites the

tests/test_web_and_witness.py

@@ -63,16 +63,16 @@ def test_web_endpoints_and_online_proof_roundtrip(tmp_path):
         with urllib.request.urlopen(base + "/paper", timeout=10) as r:
             assert r.headers["Content-Type"] == "application/pdf"
             assert r.read(5) == b"%PDF-"
-        # the prior paper version stays reachable for citability
+        with urllib.request.urlopen(base + "/paper/ltl.pdf", timeout=10) as r:
-        for path in ("/paper/ltl.pdf", "/paper/v0.1"):
+            assert r.read(5) == b"%PDF-"
-            with urllib.request.urlopen(base + path, timeout=10) as r:
+        # superseded drafts were retired from the site 2026-08-15 (git
-                assert r.read(5) == b"%PDF-", path
+        # history retains them); every old variant route must 404
-        # the removed pseudonymous version must be gone entirely
+        for gone in ("/paper/v0.0", "/paper/v0.1", "/paper/v0.2"):
-        try:
+            try:
-            urllib.request.urlopen(base + "/paper/v0.0", timeout=10)
+                urllib.request.urlopen(base + gone, timeout=10)
-            raise AssertionError("expected 404 for removed /paper/v0.0")
+                raise AssertionError(f"expected 404 for retired {gone}")
-        except urllib.error.HTTPError as exc:
+            except urllib.error.HTTPError as exc:
-            assert exc.code == 404
+                assert exc.code == 404, gone
         # the site's copy of the trust anchor (TOFU: two independent locations)
         with urllib.request.urlopen(base + "/log-public-key", timeout=10) as r:
             assert r.read() == (tmp_path / "k.pub").read_bytes()