diff --git a/paper/README.md b/paper/README.md index 80c49fa..6585783 100644 --- a/paper/README.md +++ b/paper/README.md @@ -1,6 +1,6 @@ # 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 corrections queued during the freeze (the closed consistency-verifier 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 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 +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 preserved unchanged in this repository's git history. The live copy at serves the current revision. diff --git a/paper/ltl.pdf b/paper/ltl.pdf index 211ad89..c1411b0 100644 Binary files a/paper/ltl.pdf and b/paper/ltl.pdf differ diff --git a/paper/ltl.tex b/paper/ltl.tex index 93aca56..3ba108f 100755 --- a/paper/ltl.tex +++ b/paper/ltl.tex @@ -48,7 +48,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 \\ {\normalsize Revised: August 2026 --- v0.14}} +\date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.15}} \begin{document} \maketitle @@ -112,7 +112,7 @@ This creates a problem that is logically downstream of proof construction: \begin{quote} \emph{How can a consumer that cannot execute the prover obtain precise, accountable evidence about a proof replay, without collapsing the result into -an opaque provider verdict?} +an opaque provider label?} \end{quote} 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 would provide validity rather than mere accountability, but require a circuit or 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 deterministic proof replay}. The operator still observes the replay. The diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index f308402..306578f 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -397,7 +397,7 @@ our roadmap. (The full walk-through is lecture 11 of the Jupyter c

The paper

Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log -(PDF, 25 pages, v0.14 — revised August 2026; the version is printed on the +(PDF, 25 pages, v0.15 — revised August 2026; the version is printed on the 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