proofs/proof-of-inference-emission.tex

\documentclass[11pt]{article}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{booktabs}
\usepackage{enumitem}
\usepackage{hyperref}
\usepackage{longtable}
\usepackage[margin=1in]{geometry}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}{Definition}
\newtheorem{remark}{Remark}
\newtheorem{obligation}{Proof obligation}

\newcommand{\Fp}{\mathbb{F}_p}
\newcommand{\keccak}{\mathsf{keccak}}
\newcommand{\bydef}{\triangleq}

\title{Proof-of-Inference: End-to-End Emission and On-Chain Enforcement\\
\large The activation-trace commitment that makes ``no real compute, no mint'' a theorem, not a hope}
\author{Zoo Labs Foundation \\ Hanzo AI \\ Lux Network}
\date{}

\begin{document}
\maketitle

\begin{abstract}
A companion proof established that the Freivalds matrix-product verifier over $\Fp$, $p=2^{61}-1$,
catches a fabricated product $C\neq A\cdot B$ with probability $\geq 1-1/p$ per challenge vector,
with \emph{zero} false rejection over an exact integer accumulator. That primitive was correct but
\emph{unwired}: nothing fed it operands from a real forward pass, so an adversary could mint by
committing to an output it never computed. This paper closes that gap. We define an
\emph{activation-trace transcript} --- a keccak Merkle commitment over the exact-integer operands of
each proof-bearing matmul of a forward pass --- and a permissionless \emph{challenger} that opens a
beacon-selected matmul and Freivalds-checks it. We prove (Theorem~\ref{thm:e2e}) that a prover who
returns any output not produced by the committed computation is caught except with probability
$\leq (1/p)^k$, and that an honest prover is \emph{never} slashable (Theorem~\ref{thm:honest}). We
give a proof-bearing forward (the \texttt{ProvableLinear} layer) whose returned value \emph{is} the
committed exact-integer result, eliminating the float-shadow unsoundness; an on-chain witness
(\texttt{ComputeWitnessLib}) and a native precompile (\texttt{aivmbridge} selector
\texttt{0x12000000}) that run the check in the EVM with no off-chain trust; and a slash gate
(\texttt{OptimisticEvidence}) that pays a bond to a challenger \emph{only} on a verified fraud. Every
result is implemented and tested across four languages (Rust prover, Go verifier, Solidity contract,
Go precompile) with byte-identical commitments and a pinned cross-language challenge vector;
\S\ref{sec:impl} tabulates the suite, including an adversarial red-team battery that exercises each
attack the theorems forbid.
\end{abstract}

\section{Setting and the gap this closes}

An LLM forward pass is, to $\sim$95\% of its arithmetic, a sequence of matrix multiplications
$C^{(\ell)} = A^{(\ell)} B^{(\ell)}$, $\ell = 1,\dots,L$. Proof-of-Inference binds a coin reward to
having \emph{performed} that arithmetic. The verifier is Freivalds' check~\cite{freivalds}: for a
random $r$, test $A(Br)\stackrel{?}{=}Cr$ over $\Fp$ in $O(tk+kn+tn)$ --- an order cheaper than
recomputing $C$ --- catching $C\neq AB$ with probability $\geq 1-1/p$.

We work over the Mersenne prime $p = 2^{61}-1$ on the \emph{exact integer accumulator} of the int8
matmul path ($i8\times i8 \to i64$, whole-$K$, no cross-block float reduction). Integer arithmetic is
bit-identical across CPU/GPU/backends, giving zero false rejection. The companion paper proves the
single-product soundness; we take it as Lemma~\ref{lem:freivalds} and build the system that feeds it.

\begin{lemma}[Single-product soundness, companion]\label{lem:freivalds}
For integer matrices $A\in\mathbb{Z}^{t\times k}, B\in\mathbb{Z}^{k\times n}, C\in\mathbb{Z}^{t\times n}$
reduced into $\Fp$ entrywise, and $k$ challenge vectors $r_1,\dots,r_k$ drawn uniformly and
independently from $\Fp^{\,n}$: if $C = AB$ then $A(Br_j)=Cr_j$ for all $j$ (zero false reject); if
$C\neq AB$ then $\Pr[\,\forall j:\, A(Br_j)=Cr_j\,] \leq (1/p)^k$.
\end{lemma}

\paragraph{The gap.} Lemma~\ref{lem:freivalds} is about \emph{operands}. The unsoundness the audit
found was that nothing in the deployed system ever produced operands from a real model: the verifier
had zero callers, and the mint gate accepted any non-empty ``witness''. So a prover committed an
output hash with no computation behind it and minted. Everything below is the missing wire.

\section{The activation-trace transcript}\label{sec:transcript}

\begin{definition}[Matmul leaf]
For a matmul with exact integer operands $(A,B,C)$, its leaf is
\[
\mathsf{leaf}(A,B,C) \bydef \keccak\big(\,\texttt{DOM} \,\|\, \mathsf{enc}(A) \,\|\, \mathsf{enc}(B) \,\|\, \mathsf{enc}(C)\,\big),
\]
where $\mathsf{enc}(M) = \mathrm{BE}_{32}(\text{rows})\,\|\,\mathrm{BE}_{32}(\text{cols})\,\|\,\big(\mathrm{BE}_{64}(M_{ij})\big)_{ij}$ is the
canonical row-major serialization and $\texttt{DOM}=\texttt{``hanzo/poi/matmul-leaf/v1''}$.
\end{definition}

\begin{definition}[Transcript and root]
A forward pass commits its proof-bearing matmuls $(A^{(\ell)},B^{(\ell)},C^{(\ell)})_{\ell=1}^{L}$ as
the leaf vector $(\mathsf{leaf}_\ell)_{\ell}$. The \emph{transcript root} $\rho$ is the keccak binary
Merkle root over those leaves (odd levels duplicate the last node; the index fold is
$\mathsf{even}\!\to\!\keccak(node\|sib)$, $\mathsf{odd}\!\to\!\keccak(sib\|node)$, identical to the
deployed \texttt{\_verifyMerkle}). The prover posts $\rho$ on-chain alongside its claimed output.
\end{definition}

\begin{definition}[Opening]
To \emph{open} index $\ell$, the prover reveals $(A^{(\ell)},B^{(\ell)},C^{(\ell)})$ and the Merkle
path $\pi_\ell$. The opening is \emph{included} iff folding $\mathsf{leaf}(A^{(\ell)},B^{(\ell)},C^{(\ell)})$ with
$\pi_\ell$ under the index reproduces $\rho$.
\end{definition}

\begin{lemma}[Binding]\label{lem:binding}
Under collision resistance of $\keccak$, an opening at index $\ell$ that is included under $\rho$
reveals exactly the operands the prover committed at $\ell$: producing an included opening with any
$(A',B',C')\neq(A^{(\ell)},B^{(\ell)},C^{(\ell)})$ requires a keccak collision.
\end{lemma}
\begin{proof}
Inclusion forces $\mathsf{leaf}(A',B',C')$ to equal the committed leaf at $\ell$ (the Merkle path and
index are fixed by $\rho$ and a second pre-image at any internal node is a collision). Equal leaves
with distinct operands is a collision of $\keccak$ on the encoded operand string, since $\mathsf{enc}$
is injective (fixed-width, length-prefixed). \qed
\end{proof}

\section{The challenger and end-to-end soundness}\label{sec:challenger}

\begin{definition}[Beacon-bound challenge]
Given a public, post-commitment beacon $\beta$ (\S\ref{sec:beacon}), the challenge for index $\ell$ is
$r_{j,i} = \mathrm{BE}_{64}\big(\keccak(\sigma \,\|\, \mathrm{BE}_{32}(j) \,\|\, \mathrm{BE}_{64}(i))[0{:}8]\big)\bmod p$
with seed $\sigma=\keccak(\beta\|\rho\|\mathrm{BE}_{64}(\ell))$, for $j<k$, $i<n$. Modeling $\keccak$ as a
random oracle, the $r_j$ are uniform and independent in $\Fp^{\,n}$ and are fixed only \emph{after}
$\rho$ is committed.
\end{definition}

\begin{definition}[$\mathsf{VerifyOpening}$, $\mathsf{ProvesFraud}$]
$\mathsf{VerifyOpening}(\rho,\beta,\text{op}) = \mathsf{included}(\text{op},\rho) \wedge
\mathsf{Freivalds}_k(A,B,C)$ with the beacon-bound challenge. The fraud predicate is its dual on the
correctness bit: $\mathsf{ProvesFraud}=\mathsf{included}\wedge\neg\mathsf{Freivalds}_k$.
\end{definition}

\begin{theorem}[A fabricated matmul is provable]\label{thm:e2e}
Suppose the prover's committed transcript contains, at some index $\ell$, a matmul with
$C^{(\ell)}\neq A^{(\ell)}B^{(\ell)}$. Then a challenger that opens $\ell$ produces a witness for which
$\mathsf{ProvesFraud}=\mathsf{true}$ except with probability $\leq (1/p)^k$ over the beacon. With
$k=2$ and $p=2^{61}-1$ this failure probability is $\leq 2^{-122}$.
\end{theorem}
\begin{proof}
The honest opening of $\ell$ is included (Lemma~\ref{lem:binding} gives inclusion for the committed
operands), so $\mathsf{included}=\mathsf{true}$. Because $C^{(\ell)}\neq A^{(\ell)}B^{(\ell)}$,
Lemma~\ref{lem:freivalds} gives $\Pr[\mathsf{Freivalds}_k=\mathsf{true}]\leq (1/p)^k$, hence
$\neg\mathsf{Freivalds}_k$ holds except with that probability, and $\mathsf{ProvesFraud}=\mathsf{true}$.
The beacon is drawn after $\rho$ is fixed, so the prover cannot have chosen $C^{(\ell)}$ to satisfy
the specific challenge (the pre-fit attack of \S\ref{sec:beacon}). \qed
\end{proof}

\begin{corollary}[No-compute $\Rightarrow$ provable fraud]
A permissionless watcher that re-executes the committed trace off-chain finds every index where
$C^{(\ell)}\neq A^{(\ell)}B^{(\ell)}$ \emph{deterministically} (it recomputes $A^{(\ell)}B^{(\ell)}$ in
the clear) and opens one. Thus any forward pass whose committed output was not actually computed
contains at least one such $\ell$ and is slashable except with probability $\leq(1/p)^k$.
\end{corollary}

\begin{theorem}[An honest prover is never slashable]\label{thm:honest}
If every committed matmul satisfies $C^{(\ell)}=A^{(\ell)}B^{(\ell)}$, then for every index $\ell$,
every beacon $\beta$, and every (even adversarially chosen) opening submitted by a griefer,
$\mathsf{ProvesFraud}=\mathsf{false}$.
\end{theorem}
\begin{proof}
A griefer's opening either (i) reveals the committed operands, in which case
$\mathsf{Freivalds}_k=\mathsf{true}$ by zero-false-reject (Lemma~\ref{lem:freivalds}), so
$\neg\mathsf{Freivalds}_k=\mathsf{false}$; or (ii) reveals different operands, in which case
$\mathsf{included}=\mathsf{false}$ except for a keccak collision (Lemma~\ref{lem:binding}). Either way
$\mathsf{ProvesFraud}=\mathsf{included}\wedge\neg\mathsf{Freivalds}_k=\mathsf{false}$. \qed
\end{proof}

\section{Sound emission: the output is the committed value}\label{sec:forward}

Theorems~\ref{thm:e2e}--\ref{thm:honest} bind \emph{committed matmuls}. They are only meaningful if the
value the model \emph{returns} is determined by those matmuls. The \texttt{ProvableLinear} layer makes
this hold by construction.

\begin{definition}[Proof-bearing linear]
For int8 weights $W\in[-127,127]^{\,o\times m}$ with public per-row dequant scales $s^W\in\mathbb{R}^o$,
the layer on input $x\in\mathbb{R}^{t\times m}$ computes the per-row symmetric int8 quantization
$(\bar x, s^x)=\mathsf{quant}(x)$ (deterministic: $s^x_r=\max_j|x_{rj}|/127$,
$\bar x_{rj}=\mathrm{round}(x_{rj}/s^x_r)$), forms $C=\bar x\,W^\top$ on the exact $i64$ accumulator,
commits $(\bar x, W^\top, C)$, and returns $y_{ro}=C_{ro}\,s^x_r\,s^W_o$.
\end{definition}

\begin{proposition}[Output binding]\label{prop:output}
The returned $y$ is a fixed, public function $\mathsf{dequant}(\cdot)$ of the committed $C$ and the
committed/public scales. Hence any party can recompute $y$ from the opened final-layer $C$ and reject
a prover that claims a different output; and two honest executions emit byte-identical transcripts.
\end{proposition}
\begin{proof}
$\mathsf{quant}$ and $\mathsf{dequant}$ are deterministic given $x$ and the public scales, and $C$ is
the exact integer product (no floating-point reduction), so it is reproducible across backends.
$y=\mathsf{dequant}(C)$ is then determined by the committed $C$; equality of two honest runs follows
from determinism of every step. \qed
\end{proof}

\begin{remark}[Why exact integer, not a float shadow]
A kernel that accumulates int8 block dots in \texttt{f32} (the common fast path) is non-associative and
not bit-identical across hardware; committing its $i64$ ``shadow'' would commit a computation different
from the returned value, breaking Proposition~\ref{prop:output}. \texttt{ProvableLinear} therefore
\emph{is} the computation: the returned value is dequantized directly from the committed exact $C$. The
throughput cost of the exact accumulator is the price of a reproducible proof and is paid only on
proof-bearing inferences.
\end{remark}

\section{Full-graph composition: chaining across attention and MoE}\label{sec:graph}

Theorem~\ref{thm:e2e} binds each matmul; Proposition~\ref{prop:output} binds the output to the
final matmul. What remains is to bind the \emph{whole graph}: a prover could commit correct matmuls
computed on \emph{unrelated} inputs --- a transcript that verifies per-matmul but is not a real
forward pass on the committed prompt. We close this with a typed computation trace.

\begin{definition}[Computation trace]
A trace is a sequence of typed ops $o_1,\dots,o_T$ over hash-named activations. Each op commits a
leaf $\keccak(\texttt{DOM}_{\mathrm{op}}\,\|\,\mathsf{kind}\,\|\,(\mathsf{cm}(I))_{I\in\mathrm{in}(o)}\,\|\,\mathsf{params}\,\|\,\mathsf{cm}(\mathrm{out}(o)))$,
where $\mathsf{cm}(\cdot)=\keccak(\texttt{DOM}_{\mathrm{act}}\|\mathsf{enc}(\cdot))$ names an activation
tensor. Op kinds are \textsc{MatMul} (verified by Freivalds), and the deterministic, exact-integer
glue \textsc{Add} (residual), \textsc{ReLU}, \textsc{Scale} ($1/\sqrt d$), \textsc{TopKRoute} (MoE
router, canonical tie-break), \textsc{Gather} (expert dispatch). The trace root is the keccak Merkle
root over the op leaves.
\end{definition}

\begin{definition}[Well-formed; locally correct]
A trace is \emph{well-formed} if every op's input names are the declared trace input or the output
name of an earlier op. An op is \emph{locally correct} if, opened, its revealed tensors match its
committed input/output names and it recomputes correctly: \textsc{MatMul} by Freivalds under the
beacon-bound challenge; a glue op by direct recomputation of its deterministic function.
\end{definition}

\begin{theorem}[Composition]\label{thm:compose}
If a trace is well-formed and every op is locally correct, then the committed final activation equals
the deterministic forward pass $\Phi$ applied to the committed input $x_0$. Conversely, if the
committed output is not $\Phi(x_0)$, then some op is either not well-formed (caught from the leaves)
or not locally correct (caught on opening, except with probability $\leq(1/p)^k$ for a \textsc{MatMul}).
\end{theorem}
\begin{proof}
Order the ops topologically (the trace order suffices). Induct on $i$ that op $o_i$'s output tensor
equals $o_i$'s true function applied to the true values of its inputs. Base: $o_1$'s inputs are the
declared $x_0$ (well-formedness), so local correctness gives $\mathrm{out}(o_1)=o_1(x_0)$, the true
value. Step: $o_i$'s inputs are earlier outputs (well-formedness), which by the inductive hypothesis
are their true values; local correctness then gives $\mathrm{out}(o_i)$ the true value. Hence the
final output is $\Phi(x_0)$. The converse is the contrapositive: a wrong output forces a wrong op,
caught by the corresponding check (Lemma~\ref{lem:freivalds} bounds the \textsc{MatMul} case). \qed
\end{proof}

\begin{remark}[Coverage]
Attention's spine $\mathrm{ctx}=\mathrm{softmax}(QK^\top/\sqrt d)\,V$ is two \textsc{MatMul}s and a
\textsc{Scale} ($QK^\top$, scale, then $\cdot V$); an MoE block is \textsc{MatMul} (router) $\to$
\textsc{TopKRoute} $\to$ \textsc{Gather} $\to$ \textsc{MatMul} (up) $\to$ \textsc{ReLU} $\to$
\textsc{MatMul} (down) $\to$ \textsc{Add}. Both are well-formed traces in the implementation, every op
of which verifies (\S\ref{sec:impl}). The softmax normalization is a \textsc{Softmax} op realized as a
\emph{deterministic fixed-point integer} reduction (Q16, max-shift for stability, an I-BERT-style
integer $\exp$): pure-integer, hence bit-reproducible across backends, so the challenger recomputes it
and checks the committed output exactly --- the attention block is the complete spine
$QK^\top\!\to$ scale $\to$ softmax $\to\cdot V$, with no floating-point reduction anywhere in the
committed trace.
\end{remark}

\section{The post-commitment beacon}\label{sec:beacon}

Soundness (Theorem~\ref{thm:e2e}) requires the challenge to be unpredictable when the prover chooses
$C$. If the seed depended only on $\rho$ (which the prover knows), a prover could fabricate
$C'=AB+\Delta$ with $\Delta r=0$ for the resulting $r$ and pass. We therefore bind the beacon to a
value fixed \emph{after} the prover's commitment is mined: $\beta=\keccak(\mathsf{blockhash}(b_0)\,\|\,\mathsf{id})$
where $b_0$ is the commitment's block. A transaction cannot contain its own block's hash, so a prover
choosing $C$ before signing cannot predict $\beta$; $\mathsf{blockhash}$ is available for $256$ blocks,
bounding the challenge window. The pre-fit attack is exactly attack~6 of the red-team battery
(\S\ref{sec:impl}): a forgery tuned to a guessed $r_1$ is shown to pass $r_1$ and fail a fresh $r_2$.

\section{On-chain enforcement, with no off-chain trust}\label{sec:onchain}

The witness is checked in the EVM, not asserted by a watcher. Two implementations share one wire
format and one field:
\begin{itemize}[leftmargin=1.4em]
\item \textbf{Reference (Solidity).} \texttt{ComputeWitnessLib.verifyOpening} runs Freivalds over $\Fp$
via \texttt{mulmod}/\texttt{addmod} plus the Merkle fold and the beacon challenge, byte-identical to
the prover. Cost is $O(tk+kn+tn)$ field ops --- affordable for a bounded slice; a full layer is
challenged in slices.
\item \textbf{Native (precompile).} \texttt{aivmbridge} at \texttt{0x0300\dots0004}, selector
\texttt{0x12000000}, decodes the opening wire and calls the canonical Go verifier, returning
$(\mathsf{included}\,|\,\mathsf{freivaldsOK}\!\ll\!1)$. Gas is $\text{base}+\text{(field ops)}\cdot c$,
priced so a $256$-wide slice costs $\sim$1M gas and a $4096$-wide layer is unaffordable, forcing
bounded slices; \texttt{RequiredGas} equals the metered consumption.
\end{itemize}

\begin{proposition}[Gate soundness]\label{prop:gate}
The slash gate \texttt{OptimisticEvidence.challenge} transitions a commitment to \textsc{Fraudulent}
and pays the bond to the caller \emph{iff} $\mathsf{ProvesFraud}$ holds for an opening under the
committed root and the commit-block beacon. Consequently (Theorems~\ref{thm:e2e},~\ref{thm:honest}) a
fabricated forward pass is slashable except with probability $\leq(1/p)^k$, and an honest prover is
never slashable.
\end{proposition}
\begin{proof}
By inspection the gate calls $\mathsf{ProvesFraud}$ with $\beta=\mathsf{blockhash}(\text{commitBlock})$
and slashes exactly on its truth, within the open window (after which the commitment finalizes). The
two theorems then transfer. \qed
\end{proof}

\section{Implementation and adversarial evidence}\label{sec:impl}

Every definition and theorem above is realized in code, with the commitment, the field, the Merkle
fold, and the challenge derivation \emph{byte-identical} across the prover, the watcher, the contract,
and the precompile (enforced by a pinned cross-language golden vector that breaks one suite if either
side drifts). The honest path is exercised on a real SwiGLU FFN forward; the adversarial path on a
battery that instantiates each attack the theorems forbid.

\begin{longtable}{@{}p{0.30\textwidth}p{0.50\textwidth}r@{}}
\toprule
Component & What it realizes & Tests \\
\midrule
\texttt{hanzo-engine/poi.rs} & exact matmul; keccak; Go-parity challenge derivation; Freivalds & \\
\texttt{hanzo-engine/poi\_transcript.rs} & leaf, Merkle root/proof, \texttt{verify\_opening} (\S\ref{sec:transcript}--\ref{sec:challenger}) & \\
\texttt{hanzo-engine/poi\_forward.rs} & \texttt{ProvableLinear}, \texttt{prove} (\S\ref{sec:forward}) & 18/18 \\
\texttt{hanzo-engine/poi\_graph.rs} & \texttt{GraphTrace}, typed ops incl.\ fixed-point softmax, chaining (\S\ref{sec:graph}) & 8/8 \\
\texttt{crypto/promptseal} (Go) & post-quantum (X-Wing) prompt seal (\S\ref{sec:conf}) & 6/6 \\
\texttt{crypto/attestation} (Go) & TEE quote verifier: ECDSA + x509 chain + binding (Prop.~\ref{prop:custody}) & 6/6 \\
\texttt{crypto/poi} (Go) & transcript + \texttt{VerifyOpening} + wire codec + adversarial + scaling (\S\ref{sec:scale}) & pass \\
\texttt{ComputeWitnessLib.sol} & on-chain Freivalds + Merkle + beacon (\S\ref{sec:onchain}) & 5/5 \\
\texttt{OptimisticEvidence.sol} & the slash gate, \texttt{ProvesFraud}-driven (Prop.~\ref{prop:gate}) & 18/18 \\
\texttt{aivmbridge} precompile & native verification, selector \texttt{0x12} & 5/5 \\
\texttt{tests/poi\_adversarial.rs} & red-team battery (below) & pass \\
\bottomrule
\end{longtable}

\paragraph{Red-team battery (each maps to a theorem).}
\begin{enumerate}[leftmargin=1.6em,itemsep=1pt]
\item Fabricate the final-layer output $\Rightarrow$ caught (Thm.~\ref{thm:e2e}).
\item Fabricate a hidden intermediate matmul $\Rightarrow$ caught when opened; honest layers still verify.
\item Sparse deep cheat (one wrong entry in a $256$-deep matmul) $\Rightarrow$ caught.
\item Swap the output at open time $\Rightarrow$ Merkle inclusion fails (Lemma~\ref{lem:binding}).
\item Tamper an input at open time $\Rightarrow$ inclusion fails (the leaf binds $A$).
\item Pre-fit $C$ to a \emph{guessed} challenge $r_1$ $\Rightarrow$ passes $r_1$, fails the beacon-fresh
$r_2$ (\S\ref{sec:beacon}).
\item Griefer submits a fabricated opening not under the honest root $\Rightarrow$ cannot slash
(Thm.~\ref{thm:honest}).
\item Quantization lie (claim $y\neq\mathsf{dequant}(C)$) $\Rightarrow$ detectable by public recompute
(Prop.~\ref{prop:output}).
\item Determinism: two honest machines emit the byte-identical root (zero false reject).
\item Honest forward verifies under \emph{every} beacon.
\end{enumerate}

\section{Confidentiality: the operator never sees plaintext}\label{sec:conf}

Soundness binds \emph{correctness}; it says nothing about \emph{who sees the prompt}. The default
path handed the winning operator the plaintext prompt by hash. We close this (audit G9) with a
single-shot sealing envelope: each operator publishes a KEM public key in its registry entry, and the
requester seals the prompt to it.

\begin{definition}[Prompt seal]
With operator key pair $(\mathsf{pk},\mathsf{sk})$, the requester computes
$\mathsf{seal}(\mathsf{pk},m,\mathrm{aad}) = \mathsf{enc}\,\|\,\mathsf{HPKE.Seal}(\mathsf{pk},\mathrm{info},\mathrm{aad},m)$,
RFC~9180 base mode with \textbf{X-Wing} (the hybrid X25519 $+$ ML-KEM-768 KEM), HKDF-SHA256, and
ChaCha20-Poly1305, the associated data $\mathrm{aad}$ bound to the request (the $\mathsf{intentID}$).
Only $\mathsf{sk}$, inside the operator's compute boundary, opens it. The hybrid KEM makes the seal
\emph{post-quantum}: confidentiality holds if \emph{either} X25519 or ML-KEM-768 is unbroken, so a
future quantum adversary that breaks X25519 still cannot recover $m$.
\end{definition}

\begin{remark}[The whole scheme is post-quantum]
The proof layer needs no upgrade: Freivalds soundness (Lemma~\ref{lem:freivalds}) is
\emph{information-theoretic} (it holds against an unbounded, hence quantum, adversary), and the
commitments are keccak (PQ-secure up to Grover, i.e.\ $128$-bit PQ at keccak-256). The staking layer is
ML-DSA. With the X-Wing seal, every layer of the system is post-quantum.
\end{remark}

\begin{proposition}[Confidentiality]\label{prop:conf}
Under the IND-CCA2 security of the HPKE suite: (i) a passive observer, and any operator other than the
intended recipient, learns nothing about $m$ beyond its length; (ii) two seals of the same prompt are
computationally indistinguishable (fresh ephemeral key per seal); (iii) any modification of the sealed
blob, or use under a different $\mathrm{aad}$, causes $\mathsf{open}$ to fail (AEAD authentication), so
a sealed prompt cannot be replayed under another request.
\end{proposition}
\begin{proof}
Each property is the corresponding HPKE guarantee in base mode: (i) and (ii) are KEM/DEM IND-CCA2
secrecy with a fresh encapsulation; (iii) is AEAD integrity over $(\mathrm{aad},\text{ciphertext})$.
The wrapper adds only the length-prefixed encapsulated key, which is part of the HPKE ciphertext. \qed
\end{proof}

This makes delegated operation non-custodial \emph{on the wire}: the prompt is ciphertext to everyone
but the chosen operator. Custody \emph{inside} the operator's boundary is closed by binding the
confidentiality key to an attested enclave.

\begin{definition}[Attestation quote]
A quote is $(\mathsf{measure},\mathsf{rd},\mathsf{cert},\mathsf{chain},\sigma)$: an enclave measurement
$\mathsf{measure}$, report data $\mathsf{rd}$, an attestation-key certificate $\mathsf{cert}$ with chain
$\mathsf{chain}$, and an ECDSA-P256 signature $\sigma$ over $(\mathsf{measure}\,\|\,\mathsf{rd})$. It
\emph{verifies for key} $\mathsf{pk}$ under policy $(\mathcal{R},\mathcal{M})$ iff (1) $\mathsf{cert}$
chains through $\mathsf{chain}$ to a pinned root in $\mathcal{R}$; (2) $\sigma$ verifies under
$\mathsf{cert}$'s key; (3) $\mathsf{measure}\in\mathcal{M}$; and (4) $\mathsf{rd}=\mathrm{H}(\mathsf{pk})$.
\end{definition}

\begin{proposition}[In-enclave custody]\label{prop:custody}
If a quote verifies for the operator's confidentiality key $\mathsf{pk}$ under a policy whose roots are
the genuine vendor CA and whose allow-list is the audited enclave image, then the holder of the
corresponding $\mathsf{sk}$ is that enclave image running on genuine hardware. Composed with
Proposition~\ref{prop:conf}: a prompt sealed to $\mathsf{pk}$ is decryptable \emph{only} inside the
attested enclave --- custody end to end, no plaintext outside verified code.
\end{proposition}
\begin{proof}
(1) forces the attestation key to be vendor-certified (hardware genuineness); (2) binds the report to
that key; (3) forces the audited image; (4) binds $\mathsf{pk}$ into the signed report, so the key was
generated and held inside that enclave. An adversary lacking the vendor key fails (1) (its own
well-formed quote is rejected); altering the image after signing fails (2); a different key fails (4).
By Prop.~\ref{prop:conf} only $\mathsf{sk}$ opens the seal, and $\mathsf{sk}$ lives only in the enclave.
\qed
\end{proof}

\section{Scaling: verification is per-node-independent}\label{sec:scale}

A node verifies an opening with \emph{no} coordination --- $\mathsf{VerifyOpening}$ is a pure function
of the opening, root, and beacon. So the network is embarrassingly parallel: $N$ nodes contribute $N\times$
aggregate verification capacity at constant per-proof latency, and security \emph{strengthens} with $N$
because a fabricated matmul is caught if \emph{any} honest node opens it. Measured single-node latency
on a $64\times128\times64$ challenged slice is $\approx 1.8$\,ms ($\approx 540$ verifications/s/node);
the per-node-independent projection is:

\begin{center}
\begin{tabular}{@{}rrrr@{}}
\toprule
nodes & aggregate verif./s & per-proof latency & $\Pr[\text{fraud caught} \mid 10\%\text{ honest}]$ \\
\midrule
1 & $5.4\times10^{2}$ & $1.8$\,ms & $0.100$ \\
10 & $5.4\times10^{3}$ & $1.8$\,ms & $0.651$ \\
100 & $5.4\times10^{4}$ & $1.8$\,ms & $0.9999$ \\
1000 & $5.4\times10^{5}$ & $1.8$\,ms & $1.000$ \\
\bottomrule
\end{tabular}
\end{center}

\noindent The last column is $1-(1-h)^{N}$ for an honest fraction $h=0.1$ of $N$ nodes independently
spot-checking: detection is near-certain by $N=100$. Throughput is linear because nodes are separate
machines with no shared state; the cost the network pays per challenged matmul is one Freivalds check,
which is why a single bounded slice suffices regardless of model size.

\section{Scope: what is proven and what is assumed}

\begin{itemize}[leftmargin=1.4em]
\item \textbf{Proven (here, on code).} Per-matmul soundness end to end (Thm.~\ref{thm:e2e});
no-false-slash (Thm.~\ref{thm:honest}); output binding for the proof-bearing linear
(Prop.~\ref{prop:output}); \emph{full-graph composition} across attention and MoE including the
fixed-point softmax (Thm.~\ref{thm:compose}, \S\ref{sec:graph}); \emph{post-quantum prompt
confidentiality} (Prop.~\ref{prop:conf}); \emph{in-enclave custody} via attestation
(Prop.~\ref{prop:custody}); on-chain enforcement with native and reference verifiers
(Prop.~\ref{prop:gate}); per-node-independent linear scaling (\S\ref{sec:scale}); cross-language byte
parity.
\item \textbf{Assumed.} Collision/pre-image resistance and random-oracle behavior of $\keccak$; the
field bound of Lemma~\ref{lem:freivalds} (companion); IND-CCA2 of the (post-quantum, X-Wing) HPKE suite
(Prop.~\ref{prop:conf}); unforgeability of ECDSA-P256 and a genuine pinned vendor CA for attestation
(Prop.~\ref{prop:custody}); an honest majority of block producers for the $\mathsf{blockhash}$ beacon
over the challenge window (a stronger VRF beacon strengthens this without changing the theorems).
\item \textbf{Out of scope (named, not hidden).} Platform-specific quote \emph{parsing} (the SGX/TDX
DCAP and SEV-SNP byte layouts map into the canonical quote of \S\ref{sec:conf}; this paper owns the
verification soundness, not each vendor's wire format).
\end{itemize}

\begin{thebibliography}{9}
\bibitem{freivalds} R.~Freivalds, \emph{Probabilistic machines can use less running time}, IFIP
Congress, 1977.
\end{thebibliography}

\end{document}