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.15: the dichotomy named, the question aligned

Browse source 
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.
This commit is contained in:
mrwulf 2026-08-17 13:40:39 +02:00
parent ca2a59f8a7
commit 469a962825
4 changed files with 11 additions and 6 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.14, 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
@ -12,7 +12,9 @@ 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); v0.14 completes that pass after a collisions resolved, FIPS 205 reference added); v0.14 completes that pass after a
full-document eye inspection of the published PDF (notation-table rows 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 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.

9
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.14}} \date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.15}}
\begin{document} \begin{document}
\maketitle \maketitle
@ -112,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
@ -123,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

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

@ -397,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.14 — 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