paper v0.4: round-12 fix batch — both reviews absorbed, every blocker verified before fixing

All five GPT blockers, independently confirmed against source before
any edit, plus the real subset of the Opus findings:
- B1/M5: every strict-superset/strictly-more/larger-acceptance-set
  claim (5 sites incl. two that wrap across source lines) replaced by
  witnessed non-equivalence + pinned-family language; the Remark now
  states explicitly that no global inclusion relation is claimed.
- B2: the optimistic-accountability/fraud-proof paragraph is REMOVED
  (operator: bloat; GPT: technically wrong — consumers do not accept
  by default, and a collision refutes the hash assumption rather than
  attributing operator misconduct). The careful long-form analogy
  stays in ltl-accumulator-verified/docs/optimistic-accountability.md.
- B3/M7: claim matrix — kernel-observation row split into operator-
  CLAIMS (established) vs kernel-ACTUALLY-produced (not
  cryptographically established); EUF-CMA/CR added where load-bearing.
- B4: artifact + Appendix C sentences now describe the upgraded
  verifier (lean-transparency-log 52179bd: --all covers every
  published receipt, binding fields required; 11-case adversarial
  selftest GREEN).
- B5: pin-store sketch gains the equal-size/equal-root case via
  whole-tree binding.
- M1 detached-signature honesty; M2 abstract axiom-name-sets +
  compared-views narrowing; M3 kernel time -> end-to-end replay time;
  M4+F4 consumers -> 'Consumer prototypes and version exactness'
  (implemented prototype, informal check, explicit non-evaluation
  disclaimer); M6 Appendix C listing fails closed on short proofs
  (take() guard, verified empirically); M8-partial two alternatives-
  table cells + design-taxonomy prose paragraph (also closes Opus F1
  orphaned header); M9/F5 single experience report; M10 policy-
  separation row in the coverage table; M11 27-line portability
  number restored; F2 abstract 'via differential testing'; F3 linking
  clause after the consistency theorem; Option-valued notation note
  (both reviewers); GPT terminology sentence after Definition 2.
17 pages, 0 overfull, dead-phrase sweep clean. Suite 115 green.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

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 \quad (v0.3)}
+\date{July 2026 \quad (v0.4)}
 
 \begin{document}
 \maketitle
@@ -63,11 +63,11 @@ verifier and without reducing the result to an opaque provider label?
 We define \emph{accountable replay attestation}. A specialized operator performs
 an expensive replay once and publishes a structured observation through a
 signed append-only log. Consumers verify a signed tree head and logarithmic
-inclusion proof, pin history, and apply their own policy to the exact assumptions
+inclusion proof, pin history, and apply their own policy to the exact reported axiom-name sets
-reported for each theorem. The construction does not prove that the operator's
+for each theorem. The construction does not prove that the operator's
 observation is true. It makes the claim immutable within a signed view,
-comparable across consumers, and attributable when incompatible views are
+comparable across consumers, and attributable when incompatible signed views
-presented.
+are compared.
 
 We instantiate the model as the Lean Transparency Log (LTL), using Lean~4 replay
 attestations and an RFC~9162 Merkle tree. We give explicit
@@ -76,9 +76,9 @@ consumer pinning and policy boundaries, and evaluate a live deployment over four
 production Ed25519 codebases. The public log contains thirteen leaves; its thirteenth
 leaf attests a Lean mechanization of the accumulator's own security arguments
 (222 inventoried environment constants, 61 human-reviewed assumption cones,
-and a single uninterpreted SHA-256 axiom). The mechanization also exposed a nontrivial implementation
+and a single uninterpreted SHA-256 axiom). The mechanization effort also exposed, via differential testing, a nontrivial
-boundary: the deployed iterative consistency verifier is not extensionally
+implementation boundary: the deployed iterative consistency verifier is not
-equal to the stricter recursive model on malformed size claims. The leaf records
+extensionally equal to the recursive model on malformed size claims. The leaf records
 this limitation explicitly. The resulting contribution is a cryptographic
 distribution model for machine-checked correctness evidence, together with an
 end-to-end deployed instantiation that carries scoped proofs about its own
@@ -167,9 +167,11 @@ constants, 61 human-reviewed certificate cones, and a single uninterpreted
 SHA-256 axiom.
 \item \textbf{A negative deployment result.}
 Differential testing found that the deployed iterative RFC-style consistency
-verifier accepts strictly more malformed size/root combinations than the
+verifier and the recursive model proved in Lean are not extensionally equal:
-recursive model proved in Lean. We characterize 3,867 one-sided divergences in
+there are malformed size/root combinations accepted only by the deployed
-73,573 boundary tests and scope the public attestation accordingly.
+verifier. We characterize 3,867 divergences in 73,573 pinned boundary tests
+--- every one deployed-accepts-only --- and scope the public attestation
+accordingly.
 \end{enumerate}
 
 \paragraph{Non-claims.}
@@ -212,7 +214,9 @@ an individual record follows from signature verification, but four properties
 are absent:
 \begin{enumerate}[leftmargin=1.7em,itemsep=2pt]
 \item no signed value commits to the ordered set of all records;
-\item deletion or replacement of an old result leaves no cryptographic trace;
+\item the signer commits to no complete ordered history, so omission or
+replacement is not detectable by a fresh consumer and carries no compact
+consistency proof;
 \item two consumers cannot compare a single compact view identifier;
 \item a consumer cannot demand that its previously accepted history only grow.
 \end{enumerate}
@@ -222,6 +226,17 @@ deployment size, logarithmic proof size is not the decisive benefit;
 
 \subsection{Design alternatives}
 
+Table~\ref{tab:alternatives} places the construction among the natural
+alternatives, read as a design taxonomy rather than an empirical comparison.
+Local replay and proof transport keep semantic checking with the consumer at
+high operational cost; detached signatures and committees lower consumer cost
+but commit to no ordered history (a committee distributes trust in the
+observation; it does not by itself make the record's history accountable);
+succinct proofs of replay would upgrade accountability to validity at the
+price of proving the prover. LTL occupies the low-consumer-cost point that
+still binds an ordered, signed, pinnable history --- and deliberately does not
+buy validity of the observation itself.
+
 \begin{table}[t]
 \centering\small
 \begin{tabularx}{\textwidth}{@{}lXXXX@{}}
@@ -230,8 +245,8 @@ Mechanism & Consumer cost & Semantic checker & History accountability & Main res
 \midrule
 Local replay & high & consumer & local only & prover/toolchain deployment \\
 Proof transport / PCC & medium--high & consumer checker & optional & proof/checker portability \\
-Detached signed result & low & provider & none & replaceable history \\
+Detached signed result & low & provider & statement-level only & replaceable history \\
-Committee replay & low & committee & threshold-dependent & membership trust \\
+Committee replay & low & committee & none without an additional log & membership trust \\
 Succinct proof of replay & low & circuit/VM verifier & optional & proving the prover \\
 LTL & low & provider observes; consumer applies policy & signed append-only views & observation honesty \\
 \bottomrule
@@ -290,6 +305,8 @@ policy, not of an operator verdict.
 The definition is intentionally an accountability property, not a validity
 property. It says when conflicting claims become attributable; it does not
 cryptographically prove that the replay observation was honestly produced.
+Throughout, ``accountability'' means signed-view and history accountability;
+observation validity remains external to the mechanism.
 
 \begin{figure}[t]
 \centering
@@ -451,7 +468,10 @@ the corpus pins a machine-checked non-vacuity guard for every extractor.
 \subsection{Inclusion}
 
 Let $\Root(v,m,n,P)$ recursively fold value $v$ at position $m$ through proof
-path $P$ using the same largest-power-of-two decomposition as $\MTH$.
+path $P$ using the same largest-power-of-two decomposition as $\MTH$. Both
+$\Root$ and $\ConsRec$ are partial (the mechanization's \code{Option}):
+malformed shapes return a distinguished rejection value, and an equation such
+as $\Root(\cdot)=\MTH(D)$ asserts acceptance with that output.
 
 \begin{lemma}[Domain separation]
 For all byte strings $d$ and 32-byte values $x,y$,
@@ -519,6 +539,10 @@ through their identically shaped honest trees to extract the first hash
 collision.
 \end{proof}
 
+The theorem's hypothesis pins the honest old root $\MTH(D_0)$. The deployed
+flow has no mechanized supplier of that pin; the next subsection measures what
+the iterative verifier does when size claims alone steer its walk.
+
 \begin{proposition}[Pin-store safety]
 Assume EUF-CMA security of the head signature and collision resistance of
 SHA-256. A consumer following the pin transition accepts only a nondecreasing
@@ -527,7 +551,10 @@ heads under the same key with equal size and unequal roots are transferable
 evidence that the key holder signed incompatible views.
 \end{proposition}
 \begin{proof}
-Rollback is rejected syntactically. A larger head is accepted only after a
+Rollback is rejected syntactically. At equal size the transition is accepted
+only with equal roots; if the two exhibited equal-length leaf lists differed,
+whole-tree binding would extract a SHA-256 collision, so under collision
+resistance the lists are equal. A larger head is accepted only after a
 consistency proof, so non-prefix acceptance yields a collision by the previous
 theorem. Equal-size unequal roots with valid signatures are two conflicting
 statements attributable to the key holder, except under signature forgery.
@@ -548,8 +575,9 @@ a veto cannot grant acceptance.
 
 The Lean theorem covers the recursive predicate above. The deployed iterative
 verifier follows the familiar RFC bit-navigation algorithm. Differential
-testing discovered that the iterative verifier accepts a strict superset on
+testing discovered that the two verifiers are not extensionally equal on
-malformed size claims: for example, a valid proof for a $2\to3$ transition can
+malformed size claims, every observed divergence being accepted only by the
+iterative verifier: for example, a valid proof for a $2\to3$ transition can
 be accepted under the false old-size claim $1\to3$ when paired with the size-2
 root. The mechanism is elementary: the iterative algorithm seeds its
 reconstruction with the supplied old root and consults the size claims only as
@@ -574,9 +602,9 @@ three deployed forks: Solana/Anza, RISC~Zero, and Betrusted --- all
 implementations of Ed25519~\cite{eddsa,rfc8032}. Aeneas
 provides a functional translation route from Rust to theorem-prover models;
 its design uses Rust ownership information to avoid explicit memory reasoning
-for a large class of safe Rust programs~\cite{aeneas}. Recent independent
+for a large class of safe Rust programs~\cite{aeneas}. A recent independent
-experience reports likewise show increasing use of Rust-to-Lean pipelines for
+experience report likewise applies a Rust-to-Lean pipeline to cryptographic
-cryptographic code~\cite{klaus2026}.
+code~\cite{klaus2026}.
 
 Each fork's corpus contains sixteen reviewed certificates covering:
 \begin{itemize}[leftmargin=1.6em,itemsep=2pt]
@@ -720,15 +748,16 @@ Inclusion & completeness and named collision extractor & collision resistance in
 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 \\
 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 \\
 \bottomrule
 \end{tabularx}
 \end{center}
 
 \subsection{Cost and reproducibility}
 
-A replay of one Ed25519 fork requires approximately 30 minutes of Lean kernel
+A replay of one Ed25519 fork requires approximately 30 minutes of end-to-end
-time under the pinned environment, a figure corroborated by the inter-leaf
+guarded replay time under the pinned environment, a figure corroborated by the
-issuance spacing visible in the published log. Receipt verification requires one Ed25519
+inter-leaf issuance spacing visible in the published log. Receipt verification requires one Ed25519
 signature and a logarithmic number of SHA-256 node computations. The
 accumulator corpus is independently reviewable with a pinned public Lean
 release; an environment-derived inventory fails closed on added, removed, or
@@ -752,33 +781,37 @@ valuable purpose: it falsified an overbroad equivalence claim and supplied a
 stable regression boundary.
 
 \begin{remark}[Model/deployment seam]
-For malformed size claims, the deployed iterative verifier accepts a strict
+For malformed size claims, the deployed iterative verifier and the recursive
-superset of the recursive model. In all 3,867 observed divergences the deployed
+model are not extensionally equal. In all 3,867 divergences observed across
-verifier accepted and the model rejected; the reverse direction did not occur.
+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.
 The public attestation therefore scopes soundness to the recursive model and
 states the additional operational assumption: roots and sizes must be bound by
 the authenticated pin-store and signed-head flow. This invariant is not
 mechanized in the present corpus.
 \end{remark}
 
-\subsection{Consumers}
+\subsection{Consumer prototypes and version exactness}
 
-The deployed internal consumer is a quorum-custody signing service: its
+The implemented internal consumer is a quorum-custody signing prototype: its
 inbound boundary accepts a log-derived statement only when independently
 attested verifier backends agree, and its policy consumes recorded
-observations, never operator labels. A prospective external study
+observations, never operator labels. Separately, an informal check found a
-examined a production codebase whose vendored Ed25519 dependency matches an
+production codebase whose vendored Ed25519 dependency matches an attested
-attested subject at family level but not at the attested version. The model
+subject at family level but not at the attested version; the model treats a
-treats that as a useful negative: attestations are version-exact by
+family-level match as conferring nothing, because attestations are
-construction, and a family-level match confers nothing.
+version-exact by construction. Neither observation is an evaluation claim;
+both indicate how the policy boundary is consumed in practice.
 
 \subsection{Proof portability across forks}
 
 Pure mathematical lemmas are largely reusable, while extraction-facing scripts
 diverge where code structure and generated names diverge. In the deployed
-corpora, selected parser and signature-glue files show tens to hundreds of
+corpora, the RISC~Zero and Betrusted signature-layer proof files differ by 27
-changed lines across forks, whereas pure carry and field lemmas can remain
+changed lines (tracking one fork's optimization barrier and the forks'
-byte-identical. This supports a practical conclusion: verification is portable
+differing operation order), other extraction-facing files differ by tens to
+hundreds of lines, and pure carry and field lemmas remain byte-identical. This supports a practical conclusion: verification is portable
 above the representation boundary and target-specific where implementation
 structure actually differs.
 
@@ -819,16 +852,6 @@ mechanizes accumulator arguments and then logs that replay result. The
 remaining refinement from the deployed state machine to the recursive model is
 explicitly open.
 
-\paragraph{Optimistic accountability.}
-Architecturally the model is closest to optimistic designs that substitute
-accountability for validity: a claim is accepted by default, and safety rests
-on any observer's ability to produce compact transferable evidence of a
-specific fault. The extractors of Section~\ref{sec:security} play the role of
-fraud proofs --- a false inclusion or consistency opening does not merely fail
-verification, it yields a concrete SHA-256 collision attributable to the log.
-LTL occupies the same design point for verification evidence, with targeted
-independent replay as the challenge mechanism.
-
 \section{Limitations and research agenda}\label{sec:limitations}
 
 The subject corpus maintains a numbered ledger of fifteen known gaps together
@@ -858,8 +881,8 @@ isolated clients to receive that view. Independent witnesses or gossip are the
 natural next deployment step.
 
 \paragraph{Consistency refinement.}
-The recursive model is proved; the iterative deployment has a larger malformed-
+The recursive model is proved; the iterative deployment diverges from it on
-input acceptance set. The strongest closure is either to deploy
+malformed inputs, every observed divergence being deployed-accepts-only. The strongest closure is either to deploy
 $\ConsRec$-equivalent semantics or to mechanize the signed-head and pin-store
 flow and prove the authentic-pair refinement theorem.
 
@@ -916,9 +939,11 @@ The public artifacts are available at:
 \item accumulator mechanization: \href{https://github.com/saymrwulf/ltl-accumulator-verified}{\texttt{saymrwulf/ltl-accumulator-verified}};
 \item provider and consumer tooling: \href{https://github.com/saymrwulf/proof-aware-crypto-tooling-agent}{\texttt{saymrwulf/proof-aware-crypto-tooling-agent}}.
 \end{itemize}
-A clone of the mirror re-verifies every head, leaf, and receipt offline via
+A clone of the mirror re-verifies every numbered leaf, every published signed
-\code{python3 verify.py --all} (Python standard library plus an \code{openssl}
+head, and every published receipt offline via \code{python3 verify.py --all}
-binary; the verifier fails closed if signature checking is unavailable).
+(Python standard library plus an \code{openssl} binary; the verifier fails
+closed if signature checking is unavailable, and its adversarial self-test
+ships beside it).
 
 \section*{Acknowledgments}
 The author designed the system and is responsible for every claim. Claude
@@ -1012,12 +1037,13 @@ Verification Pipeline with AI Provers: An Experience Report. arXiv:2605.30106,
 \toprule
 Consumer conclusion & Established by & Remaining assumption \\
 \midrule
-Leaf occupies index $m$ under head $h$ & inclusion proof and signed head & SHA-256 collision resistance; correct public key \\
+Leaf occupies index $m$ under head $h$ & inclusion proof and signed head & SHA-256 collision resistance; correct public key; EUF-CMA of the head signature \\
 Head was authorized by the log identity & Ed25519 verification & correct key acquisition; EUF-CMA \\
-New pinned head extends old pinned head & consistency proof & recursive-model soundness; authentic size/root pairing for deployment \\
+New pinned head extends old pinned head & consistency proof & SHA-256 collision resistance; recursive-model soundness; authentic size/root pairing for deployment \\
-Equal-size unequal roots conflict & two valid signatures & both heads compared by a retaining observer \\
+Equal-size unequal roots conflict & two valid signatures & correct public key; EUF-CMA; operationally, a retaining observer must compare the heads \\
 Observed cone matches local boundary policy & exact set equality & semantic identity of named declarations \\
-Kernel produced the recorded observation & replay attestation & operator/replay-pipeline honesty or independent replay \\
+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 \\
 Source corresponds to deployed binary & not established & reproducible build and compiler assurance \\
 Claimed signer implementation produced STH & not established & execution provenance \\
 \bottomrule
@@ -1044,7 +1070,9 @@ The following code is only the Merkle inclusion core. A complete receipt
 verifier must additionally validate the signed tree head, log identifier,
 tree-size binding, public-key fingerprint or pinned key, leaf hash, and receipt
 schema. The published log-repository verifier implements that full binding
-list and fails closed when signature checking is unavailable.
+list for every published receipt --- the binding fields are required, never
+compare-if-present --- and fails closed when signature checking is
+unavailable.
 \begin{lstlisting}[language=Python]
 import hashlib
 
@@ -1060,17 +1088,20 @@ def h_node(left, right):
 def split_below(n):
     return 1 << ((n - 1).bit_length() - 1)
 
+def take(path, used):
+    if used >= len(path):
+        raise ValueError("proof exhausted")
+    return path[used]
+
 def root(value, index, size, path, used=0):
     if size == 1:
         return value, used
     k = split_below(size)
-    if used >= len(path):
-        raise ValueError("proof exhausted")
     if index < k:
         left, used = root(value, index, k, path, used)
-        return h_node(left, path[used]), used + 1
+        return h_node(left, take(path, used)), used + 1
     right, used = root(value, index-k, size-k, path, used)
-    return h_node(path[used], right), used + 1
+    return h_node(take(path, used), right), used + 1
 
 def verify_inclusion(leaf, index, size, path, expected_root):
     if size <= 0 or index < 0 or index >= size:

provider/src/pacta_provider/webdocs.py

@@ -292,13 +292,14 @@ 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, 16 pages, v0.3) — the trust decomposition (expensive verification produces an
+(PDF, 17 pages, v0.4 — revised after two independent round-12 reviews) — the trust
-observation; transparency makes the observation accountable; consumer-local policy decides
+decomposition (expensive verification produces an observation; transparency makes the
-acceptance), collision-extracting soundness for inclusion and consistency, the policy
+observation accountable; consumer-local policy decides acceptance), collision-extracting
-boundary where operator labels can veto but never grant acceptance, the live thirteen-leaf
+soundness for inclusion and consistency, the policy boundary where operator labels can veto
-deployment whose entry 13 attests the accumulator's own mechanized model, and the measured
+but never grant acceptance, the live thirteen-leaf deployment whose entry 13 attests the
-model/deployment seam (3,867 one-sided lied-size divergences) reported as a result rather
+accumulator's own mechanized model, and the measured model/deployment divergence (3,867
-than hidden.
+lied-size cases, every one accepted only by the deployed verifier) reported as a result
+rather than hidden.
 <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>