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.14: the full-document eye pass completes the referee round

Browse source 
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.
This commit is contained in:
mrwulf 2026-08-17 12:54:08 +02:00
parent 3b13fdbfde
commit 7a6499c452
4 changed files with 14 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
paper/README.md
View file

@ -1,6 +1,6 @@
# Which file is current? # Which file is current?
**`ltl.pdf` / `ltl.tex` — the current paper (v0.13, revised August 2026).** **`ltl.pdf` / `ltl.tex` — the current paper (v0.14, 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
@ -10,7 +10,9 @@ verify-path instantiation, and its certificate appendix; v0.12 unified
entry numbering on 0-based leaf indices; v0.13 is the approachability entry numbering on 0-based leaf indices; v0.13 is the approachability
revision from an external-persona referee pass (house terms defined at revision from an external-persona referee pass (house terms defined at
first use, theorem statements carry their own scoping, notation first use, theorem statements carry their own scoping, notation
collisions resolved, FIPS 205 reference added). The 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). 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.

17
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.13}} \date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.14}}
\begin{document} \begin{document}
\maketitle \maketitle
@ -518,7 +518,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 \\
@ -936,9 +937,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
@ -949,7 +950,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$
@ -962,7 +963,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).}
@ -1031,7 +1032,7 @@ The LTL construction with the recursive verifiers of \S\ref{sec:security}
--- 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 --- 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}

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

@ -392,7 +392,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.13 — revised August&nbsp;2026</strong>; the version is printed on the (PDF, 25 pages, <strong>v0.14 — 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