papers/lux-aivm/lux-aivm.tex

\documentclass[11pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{listings}
\usepackage{xcolor}
\usepackage{geometry}
\usepackage{booktabs}

\geometry{margin=1in}
\setlength{\emergencystretch}{2em}

% listings has no built-in Rust or Solidity; define them so code blocks compile and highlight.
\lstdefinelanguage{Rust}{
  morekeywords={fn,let,mut,pub,struct,impl,for,in,return,vec,usize,i64,u64,Self,if,else,match,as,use,crate},
  sensitive=true,
  morecomment=[l]{//},
  morecomment=[s]{/*}{*/},
  morestring=[b]"
}
\lstdefinelanguage{Solidity}{
  morekeywords={function,internal,external,public,pure,view,returns,memory,calldata,uint256,int256,bytes32,bool,if,else,for,return,revert,struct,mapping,address,require,constant,immutable},
  sensitive=true,
  morecomment=[l]{//},
  morecomment=[s]{/*}{*/},
  morestring=[b]"
}
\lstset{
  basicstyle=\ttfamily\small,
  breaklines=true,
  frame=single,
  language=Go,
  keywordstyle=\color{blue},
  commentstyle=\color{gray},
  stringstyle=\color{red},
  showstringspaces=false
}

\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}
\newtheorem{property}{Property}

\hypersetup{
  pdftitle={AIVM: Proof of AI},
  pdfauthor={Lux Research},
  pdfsubject={A-Chain settlement for deterministic, verifiable AI computation},
  pdfkeywords={Proof of AI, AIVM, A-Chain, integer inference, Freivalds verification},
  colorlinks=true,
  linkcolor=blue!50!black,
  citecolor=blue!50!black,
  urlcolor=blue!60!black,
}

\title{AIVM: Proof of AI\\
\large The Settlement Primitive for Verifiable Machine Computation on Lux}

\author{Lux Research\thanks{[email protected]} \\ \textit{Hanzo Industries \quad Lux Industries \quad Zoo Labs Foundation} \\ \texttt{[email protected]}}

\date{June 2026}

\begin{document}

\maketitle

\begin{abstract}
We present the AIVM (AI Virtual Machine) and its settlement primitive, \emph{Proof of AI} (PoAI): a protocol for committing, challenging, and settling deterministic integer AI computation. A versioned kernel profile fixes the consensus-visible operator semantics while a canonical transcript binds the job, model, input, graph, output, metering, provider, and destination. The arithmetic core uses Freivalds' matrix-product verifier over the prime field $\mathbb{F}_p$, $p = 2^{61}-1$, on the exact-integer accumulator of a quantized \texttt{int8} matrix multiplication. Honest CPU and GPU implementations therefore agree byte-for-byte. For one committed matrix product, one unpredictable challenge has information-theoretic error at most $1/p \approx 2^{-61}$; two independent vectors reduce the local error to at most $2^{-122}$. This local bound is not, by itself, a whole-model bound: a graph protocol must additionally ensure coverage of every operation, or quantify random sampling and guarantee transcript data availability. The current implementation provides an optimistic commitment-and-fraud-proof backend plus unit-tested typed-graph components; production integration into a complete model pipeline remains work in progress.

The A-Chain runs the sole Proof-of-AI useful-work consensus. It admits a demand-backed job before mining, fixes the model and execution policy, verifies that the committed computation was actually performed, consumes a global work nullifier, and finalizes one canonical receipt. Z-Chain is the P3Q proof-compression and settlement rollup: it batches A-Chain receipt transitions into a Plonky3-derived, pairing-free STARK/FRI settlement proof. Lux Quasar orders and finalizes the A-Chain and Z-Chain state on the post-quantum base layer. A miner may choose a payout destination, but neither Z-Chain nor that destination independently admits raw work or decides that computation occurred. Other chains verify the Z-settled, PQ-finalized A-Chain receipt and release the authorized asset representation. This gives the network one issuance schedule and no-double-mint ledger while allowing permissionless CPU or GPU execution and omnichain payout.
\end{abstract}

\tableofcontents

\section{Introduction}

A blockchain settles claims about value because anyone can cheaply verify them. Bitcoin settles ``this work was done'' by making the work (a partial hash preimage) trivial to check and expensive to produce; the work itself is otherwise useless. The open question for a decentralized AI network is whether one can settle a far more valuable claim --- ``this AI computation was performed correctly'' --- with the same asymmetry: cheap to verify, expensive to fake, and \emph{the work is the product}.

The AIVM answers yes for a deliberately constrained execution domain. Its settlement primitive, Proof of AI, makes a single observation precise: most work in a quantized neural-network pass is matrix multiplication $C = A \cdot B$, and a matrix product is exactly the object Freivalds' 1977 algorithm verifies probabilistically more cheaply than recomputation~\cite{freivalds}. If the proof is anchored on the \emph{exact integer} accumulator of a canonical quantized model --- not a floating-point shadow that disagrees across hardware --- the local check becomes bit-exact and deterministic. The protocol then adds transcript binding, graph chaining, data availability, challenge coverage, and A-Chain settlement. Only after those layers succeed may one unit of accepted computation authorize subsidy once, under the A-Chain's global nullifier state.

\subsection{Contributions}

\begin{enumerate}
  \item \textbf{A common trace for supported inference, embedding, and training graphs (\S\ref{sec:graph}).} We define a typed deterministic-integer trace whose well-formedness plus verification of every operation imply, by induction, that the committed output equals execution on the committed input. This statement covers graphs expressible in the specified operation set; it is not a claim about arbitrary floating-point training stacks.
  \item \textbf{An information-theoretic local soundness core (\S\ref{sec:soundness}).} Freivalds over $\mathbb{F}_p$, $p = 2^{61}-1$, on an exact-integer accumulator, with error $1/p$ per independent challenge vector and zero false-reject for an honest matrix product. Hash commitments and signatures remain computational post-quantum assumptions of the complete protocol.
  \item \textbf{Cross-language byte parity (\S\ref{sec:parity}).} Rust and Go golden vectors share one field and challenge derivation, while a Solidity test verifies a Go-produced opening unchanged. This establishes wire compatibility of the tested fixtures, not production integration of every model kernel.
  \item \textbf{A-Chain PoAI useful-work consensus (\S\ref{sec:settlement}--\S\ref{sec:governance}).} A-Chain owns job admission, proof finality, the global work-nullifier set, and issuance authorization. Z-Chain rolls finalized receipts into P3Q settlement proofs; Lux provides post-quantum ordering and finality beneath both state machines. Destination chains consume certified receipts and do not run an independent PoAI acceptance path.
  \item \textbf{Bitcoin-shaped economics applied to accepted useful work (\S\ref{sec:economics}).} A capped, halving, deflationary issuance schedule whose subsidy is authorized only by finalized A-Chain work receipts. Demand establishes usefulness; the execution proof establishes computational correctness.
\end{enumerate}

\subsection{The shape of the system}

The reference contracts live at \texttt{luxfi/standard} under \texttt{contracts/ai/}, while the arithmetic core is mirrored in \texttt{hanzo-engine}, \texttt{luxfi/crypto}, and \texttt{ComputeWitnessLib.sol}. These components are at different maturity levels. The arithmetic, serialization, and small-graph tests are implemented; a production-scale proof emitted by a complete Zen model and consumed by A-Chain consensus is not yet the default inference path. The contracts are therefore reference mechanisms and test surfaces until A-Chain integration, data availability, challenge finality, and deployment wiring are complete.

\paragraph{Mining-authority invariant.} ``Mine into another chain'' means that an A-Chain job names a destination for settlement. It never means that Z-Chain or the destination chain runs PoAI, owns an independent mining spent set, or decides whether work occurred. A-Chain PoAI consensus finalizes exactly one issuance authorization; Z-Chain compresses and settles that authorization, and a destination adapter verifies it and releases the corresponding representation.

\paragraph{Three-layer finality and settlement.} PoAI is the A-Chain domain consensus that decides whether an admitted useful-compute claim is valid and final. Z-Chain is the P3Q settlement rollup that batches and proves finalized A-Chain receipt transitions; it is not a second work-admission or mining authority. Quasar supplies validator ordering, fork choice, and finality for the A-Chain and Z-Chain state, with activated post-quantum authentication securing the exported settlement root. Thus ``finalized by PoAI consensus,'' ``settled through P3Q,'' and ``secured by Lux consensus'' describe complementary layers, not competing leader-election mechanisms.

\subsection{Threat model}\label{sec:threat}

We assume compute providers may be Byzantine: they may return fabricated outputs, claim outputs they never computed, splice unrelated activations into a trace, withhold transcript data, replay one piece of work to many destinations, claim hardware they do not possess, or collude to extract subsidy without performing the work. We assume \textsc{keccak}-256 is collision- and preimage-resistant, ML-DSA is unforgeable, and A-Chain finality is not captured. The Freivalds equality test for one opened matrix product has information-theoretic error; the complete protocol does not, because commitment binding, authentication, data availability, challenge coverage, and consensus rely on additional assumptions. We require an unpredictable post-commitment public beacon and enough transcript availability for an honest challenger to reconstruct an inclusion proof before finality. Confidential TEE evidence is optional and has an explicit vendor trust assumption.

\section{The Soundness Core: Freivalds over a Prime Field}\label{sec:soundness}

\subsection{Why a matrix product is the right primitive}

Let a proof-bearing layer compute $C = A \cdot B$ with $A \in \mathbb{Z}^{t \times k}$, $B \in \mathbb{Z}^{k \times n}$, $C \in \mathbb{Z}^{t \times n}$. Recomputing $C$ to check it costs $O(t \cdot k \cdot n)$ --- exactly the work the prover did, so verification would be no cheaper than redoing the inference. Freivalds' insight is to check the product against a random vector $r \in \mathbb{F}_p^{n}$:
\begin{equation}\label{eq:freivalds}
  A \cdot (B \cdot r) \;\overset{?}{=}\; C \cdot r ,
\end{equation}
which costs $O(t k + k n + t n)$ --- three matrix-vector products, an order of magnitude cheaper than the matrix-matrix product. This asymmetry is the whole point: the model is enormous, the witness is one opened matmul, and the verifier does a fraction of the prover's work.

\subsection{The field and the exact-integer accumulator}

We evaluate \eqref{eq:freivalds} over the Mersenne prime field $\mathbb{F}_p$ with
\begin{equation}
  p = 2^{61} - 1 .
\end{equation}
The choice is deliberate. Each operand is an \texttt{int8} weight or activation reduced into $[0,p)$; the field is $61$ bits, so a single $128$-bit multiply of two reduced elements never overflows and a modular reduction by a Mersenne prime is cheap. In the on-chain mirror, $p$ is small enough that Solidity's \texttt{mulmod}/\texttt{addmod} stay exact under it.

Crucially, the operands are taken from the \emph{exact integer} accumulator of the engine's quantized matmul --- an $i8 \times i8 \to i64$ whole-$K$ accumulation with no cross-block floating-point rescale. The Rust prover documents and implements this as the proof-bearing GEMM~(\texttt{poi.rs}, \texttt{exact\_matmul}):

\begin{lstlisting}[language=Rust,caption={The exact-integer matmul; identical in Go (\texttt{crypto/poi.ExactMatmul}).}]
pub fn exact_matmul(a: &Mat, b: &Mat) -> Mat {
    let (t, k, n) = (a.rows, a.cols, b.cols);
    let mut c = vec![0i64; t * n];
    for i in 0..t { for j in 0..n {
        let mut acc: i64 = 0;
        for x in 0..k { acc += a.data[i*k + x] * b.data[x*n + j]; }
        c[i*n + j] = acc;
    }}
    Mat::new(t, n, c)
}
\end{lstlisting}

\begin{property}[Cross-backend determinism]\label{prop:det}
For operand and dimension bounds that prevent accumulator overflow, integer matrix multiplication incurs no rounding and all valid reduction orders produce the same value over $\mathbb{Z}$. Alternatively, an execution specification may define identical modular or saturating overflow semantics. Under one of those explicit policies, honest CPU and GPU implementations produce the bit-identical accumulator $C$.
\end{property}

This is the property the entire scheme stands on. A floating-point matmul may produce platform-dependent low bits, and a tolerance window complicates soundness. The production execution specification must therefore bind accumulator width, maximum inner dimension, overflow behavior, and dequantization rules rather than relying on the language's default integer or floating-point behavior.

\subsection{Soundness}

\begin{theorem}[Freivalds soundness over $\mathbb{F}_p$]\label{thm:freivalds}
Fix $A, B, C$ over $\mathbb{F}_p$ with $C \neq A \cdot B$. For $r$ drawn uniformly from $\mathbb{F}_p^{n}$,
\[
  \Pr_r\!\left[\, A(Br) = Cr \,\right] \;\le\; \frac{1}{p}.
\]
\end{theorem}

\begin{proof}
Let $D = C - A\cdot B \neq 0$ over $\mathbb{F}_p$. Then $A(Br) = Cr \iff Dr = 0$. Pick an entry $D_{i j} \neq 0$. Row $i$ of $Dr$ is the linear form $L(r) = \sum_{\ell} D_{i\ell}\, r_\ell$, which is not identically zero because $D_{i j} \neq 0$. Fix all coordinates of $r$ except $r_j$; then $L$ is a degree-one nonzero polynomial in the single variable $r_j$ over the field $\mathbb{F}_p$, so it has at most one root. Hence $\Pr[L(r) = 0] \le 1/p$, and $\Pr[Dr = 0] \le \Pr[(Dr)_i = 0] \le 1/p$. (This is the Schwartz--Zippel lemma~\cite{schwartz,zippel} specialized to degree one.)
\end{proof}

\begin{corollary}[Two challenges]\label{cor:two}
With $k$ independent challenge vectors, a fabricated $C$ passes all of them with probability at most $(1/p)^k$. For $p = 2^{61}-1$ and $k = 2$,
\[
  \left(\tfrac{1}{p}\right)^2 \;<\; 2^{-122}.
\]
\end{corollary}

The Go verifier states and enforces exactly this bound~(\texttt{crypto/poi/freivalds.go}): ``Soundness error is $1/p \sim 2^{-61}$ per challenge vector; $k=2$ vectors give $\le 2^{-122}$.''

\begin{theorem}[Post-quantum local equality test]\label{thm:pq}
The soundness of Theorem~\ref{thm:freivalds} and Corollary~\ref{cor:two}, conditioned on an unpredictable challenge and a binding opening, is information-theoretic: it is a counting argument over a finite field and invokes no computational hardness assumption. A computationally unbounded adversary gains no advantage against that equality test.
\end{theorem}

This is the structural reason the arithmetic core is post-quantum. The complete PoAI protocol additionally uses \textsc{keccak} commitments, ML-DSA authentication, A-Chain consensus, and an availability/challenge game. Those are computational or system assumptions and must not be collapsed into the local information-theoretic bound.

\begin{theorem}[Zero false-reject]\label{thm:zero-fr}
If $C = A \cdot B$ exactly over $\mathbb{Z}$ and every entry of $A, B, C$ is reduced into $[0,p)$ consistently, then \eqref{eq:freivalds} holds for \emph{every} $r$. Thus an honest prover is never rejected.
\end{theorem}

\begin{proof}
Field reduction is a ring homomorphism $\mathbb{Z} \to \mathbb{F}_p$; if $C = A \cdot B$ over $\mathbb{Z}$ then the identity holds after reduction, so $Dr = 0$ for all $r$. By Property~\ref{prop:det} the honest integer accumulator is reproducible, so the operands the verifier reduces are exactly the prover's.
\end{proof}

Theorem~\ref{thm:zero-fr} is what makes the scheme safe to put on the critical path of an economic system: an honest miner cannot be slashed by bad luck, and a challenger who submits a ``fraud proof'' against honest work simply finds the check passes.

\subsection{Challenge unpredictability}

A prover must not be able to pre-fit $(A,B,C)$ to a known $r$. The canonical Rust and Go derivation hashes a public, post-commitment beacon with the task and transcript root:
\[
  r[j][i] \;=\; \mathrm{BE\_u64}\!\big(\textsc{keccak}(\,\text{seed} \,\|\, \mathrm{BE32}(j) \,\|\, \mathrm{BE64}(i)\,)[\,0{:}8\,]\big) \bmod p,
\]
with $\text{seed} = \textsc{keccak}(\text{beacon} \,\|\, \text{task} \,\|\, \text{root})$. Because the beacon is fixed only \emph{after} the prover commits the root, the challenge is unpredictable at commit time; because the derivation is a pure function of public inputs, both sides reproduce it without interaction.

\subsection{From local checks to protocol soundness}\label{sec:coverage}

Freivalds answers ``is this opened matrix product correct?'' It does not answer ``did the verifier inspect the fraudulent operation?'' Suppose a trace contains $L$ operations, $b \ge 1$ of which are invalid, and the protocol samples $s$ operations independently and uniformly. The probability that sampling misses every invalid operation is
\[
  \left(1-\frac{b}{L}\right)^s .
\]
If each selected matrix product is checked with $k$ independent Freivalds vectors, a conservative acceptance bound is
\[
  \Pr[\text{accept invalid trace}]
  \;\le\;
  \left(1-\frac{b}{L}\right)^s + \frac{s}{p^k}.
\]
For a sparse one-operation fraud in a large graph, the sampling term dominates; quoting only $1/p^k$ would be incorrect. A protocol may instead use an optimistic fraud-proof game in which independent watchers re-execute the graph and may challenge \emph{any} invalid committed operation. In that design, security requires the complete transcript (or enough erasure-coded data to reconstruct it) to be available throughout the challenge window, plus a finality rule that prevents irreversible issuance before the challenge resolves.

The Go and Rust verifiers support multiple challenge vectors. The current Solidity witness derives one vector, so its local error is $1/p \approx 2^{-61}$, not $2^{-122}$. Production parameters must state both $s$ and $k$ and bind them in the A-Chain execution policy.

\subsection{What the core proves, and what it does not}

The Freivalds core proves a \emph{single opened} matmul output is genuine, conditioned on the commitment and challenge assumptions. Three gaps remain. First, a prover could commit correct matmuls on unrelated inputs; \S\ref{sec:graph} addresses this with graph chaining. Second, a prover could return a different value than it committed; \S\ref{sec:forward} binds the returned value to the accumulator. Third, a verifier may never inspect the bad operation; \S\ref{sec:coverage} makes that coverage term explicit. None of these checks proves that an answer is semantically true, useful, unbiased, or worth a particular reward. Demand-backed A-Chain job admission supplies usefulness; PoAI supplies execution accountability.

\subsection{Verified test evidence for the core}\label{sec:core-tests}

The Rust core (\texttt{poi.rs}) and the Go core (\texttt{crypto/poi}) each ship a soundness suite that we ran to completion:

\begin{table}[h]
\centering
\begin{tabular}{p{0.34\textwidth}p{0.46\textwidth}l}
\toprule
\textbf{Test} & \textbf{Asserts} & \textbf{Lang} \\
\midrule
Honest product & $C = A\!\cdot\!B$ passes every challenge & Rust/Go \\
Tampered output & one flipped entry of $C$ is rejected & Rust/Go \\
Signed reduction & negative int8 values reduce exactly & Rust \\
Sparse fabrication & one off-by-one entry in $16\!\times\!16$ is caught & Rust/Go \\
Challenge determinism & both sides derive identical $r$ & Rust \\
Shape mismatch & invalid dimensions fail closed & Rust/Go \\
Golden parity & Rust $r$ equals Go $r$ byte-for-byte & Rust/Go \\
\bottomrule
\end{tabular}
\caption{Representative soundness-core tests (all passing).}
\end{table}

At the recorded snapshot, the Go suite reported 22 passing tests and the Rust suite reported 27. A small Go fixture measured 1.13\,ms per opening, or 882 verifications/second on one test-host thread. Section~\ref{sec:evidence} states the limits of this measurement.

\section{The Transcript: Committing a Forward Pass}\label{sec:transcript}

A single matmul check is useless unless it is bound to a specific, committed computation. The transcript layer~(\texttt{poi\_transcript.rs}; Go mirror \texttt{crypto/poi/transcript.go}) makes ``no valid compute proof, no mint'' enforceable.

\subsection{Deterministic kernel profile and canonical transcript}

The consensus object is not an arbitrary GPU execution log.  Each A-Chain job names a
versioned \emph{deterministic kernel profile}: the admitted operator set, tensor layout,
integer widths, accumulator bounds, overflow behavior, reduction order, fixed-point
scales, rounding rule, tie-breaks, and canonical byte encoding.  A miner may implement
that profile on a CPU, GPU, or another accelerator, but an optimization is admissible only
when it produces the same profile bytes.  Hardware speed changes who can execute a job
economically; it does not change the computation A-Chain judges.

Execution emits one \emph{canonical transcript}.  Its header binds the A-Chain job and
policy epoch, profile version, model and runtime commitments, input root, declared graph,
output root, metering summary, miner, destination, and nonce.  Its ordered body binds every
typed operation to its input and output commitments.  The Merkle root of that serialization
is the portable receipt commitment consumed by the challenge game and, after PoAI finality,
by P3Q settlement.  This distinction matters: deterministic kernels define the function;
the canonical transcript proves which invocation of that function was claimed.

CPU/GPU ``parity'' is therefore a release conformance test, not a second consensus
mechanism.  Golden vectors must show that every supported backend produces byte-identical
kernel outputs, leaves, transcript roots, challenges, and openings.  A backend that fails a
vector is excluded from the profile; consensus never accepts a tolerance band to make the
backend fit.

\subsection{Commitment}

Each proof-bearing matmul is committed as a leaf binding its three exact-integer operands under a domain tag:
\[
  \mathrm{leaf} \;=\; \textsc{keccak}\big(\texttt{"hanzo/poi/matmul-leaf/v1"} \,\|\, \mathrm{mat}(A) \,\|\, \mathrm{mat}(B) \,\|\, \mathrm{mat}(C)\big),
\]
where $\mathrm{mat}(M) = \mathrm{BE32}(\text{rows}) \,\|\, \mathrm{BE32}(\text{cols}) \,\|\, (\text{each } M_{ij} \text{ as } \mathrm{BE64})$ is the canonical serialization. The leaves are folded into a binary \textsc{keccak}-Merkle root using the index-fold convention (even index $\to \textsc{keccak}(\text{node}\,\|\,\text{sibling})$, odd $\to \textsc{keccak}(\text{sibling}\,\|\,\text{node})$); odd levels duplicate the last node. This is the \emph{transcript root} the prover posts on-chain.

\subsection{Challenge and opening}

A challenger derives the index of the matmul to open from the beacon and root,
\[
  \text{index} \;=\; \textsc{keccak}(\text{beacon} \,\|\, \text{root})[\,0{:}8\,] \bmod \text{length},
\]
unpredictable before the prover commits the root. The prover \emph{opens} that index, revealing $(A,B,C)$ and the Merkle inclusion path. Verification is the conjunction of binding and correctness~(\texttt{verify\_opening}):
\begin{enumerate}
  \item \textbf{Binding (Merkle inclusion).} The revealed operands hash to the committed leaf at \texttt{index} under \texttt{root}. A prover who swaps in different operands fails here.
  \item \textbf{Correctness (Freivalds).} $C = A\cdot B$ under $k$ beacon-bound challenge vectors derived from $\textsc{keccak}(\text{beacon}\,\|\,\text{root}\,\|\,\mathrm{BE64}(\text{index}))$. A fabricated output fails here.
\end{enumerate}

\begin{lemma}[Opening soundness]\label{lem:opening}
For an opening that is Merkle-included under \texttt{root}, an honest $C=A\cdot B$ passes every challenge. If $C\neq A\cdot B$, it passes $k$ independent unpredictable Freivalds vectors with probability at most $1/p^k$. The Go and Rust paths commonly test $k=2$; the current Solidity path uses $k=1$.
\end{lemma}

This lemma is the local interface used by the off-chain watcher and on-chain fraud predicate. It says nothing about the chance that an invalid operation is opened; that is the separate coverage and availability problem of \S\ref{sec:coverage}.

\subsection{Sound forward pass: the returned value is the committed value}\label{sec:forward}

The transcript binds operands, but an honest-looking transcript is worthless if the layer \emph{returns} something other than what it committed. \texttt{ProvableLinear}~(\texttt{poi\_forward.rs}) closes this. It computes $y = \mathrm{dequant}(\mathrm{quant}(x) \cdot W_{i8})$ on the exact-integer accumulator, commits the operands $(A = x_{i8},\, B = W_{i8},\, C = x_{i8}\!\cdot\!W_{i8})$, and returns the dequantization of the \emph{committed} $C$:
\[
  y[t][o] \;=\; C[t][o] \cdot \text{xscale}[t] \cdot \text{wscale}[o],
\]
where the scales are public model parameters. Dequantization is therefore a public affine map of $C$.

\begin{theorem}[Output-commitment binding]\label{thm:output}
Committing $C$ and the canonical scale encoding commits the intended dequantized $y$. Exact consensus replay additionally requires a fixed-point dequantization and rounding specification; ordinary floating-point evaluation with a tolerance is not byte-exact across all backends.
\end{theorem}

The current output-binding test checks returned $y$ against $\mathrm{dequant}(\text{committed } C)$ with floating-point tolerance. That is useful engine evidence but is not a consensus determinism proof. A production proof-bearing output must remain integer or fixed-point through the committed decision boundary, or define a canonical bit-exact dequantizer. A separate SwiGLU fixture exercises three committed matmuls.

\section{Graph Composition for Deterministic Programs}\label{sec:graph}

\subsection{The gap the graph closes}

Per-matmul soundness still permits a prover to commit individually-correct matmuls computed on activations it never derived from the prompt --- splicing an unrelated tensor mid-stream. The graph layer~(\texttt{poi\_graph.rs}) makes the \emph{wiring} of the computation part of the commitment.

\begin{definition}[Computation trace]
A \texttt{GraphTrace} is a sequence of typed operations over hash-identified activations. An activation tensor $M$ is named by
\[
  \mathrm{act}(M)=\textsc{keccak}(\texttt{"hanzo/poi/activation/v1"}\,\|\,\mathrm{mat}(M)).
\]
Each operation commits a leaf binding its kind, input commitments, inline parameters, and output commitment. The trace also declares its input activations.
\end{definition}

The prototype operation set contains the following pure deterministic integer functions. It is sufficient for the included attention, MoE, and linear-SGD fixtures; production model support requires a complete manifest for every operator actually executed by the chosen architecture and optimizer.
\begin{center}
\begin{tabular}{ll}
\toprule
\textbf{Op} & \textbf{Semantics (exact integer)} \\
\midrule
\texttt{MatMul} & $C = A\cdot B$ --- the only Freivalds-checked op \\
\texttt{Add} & residual $\text{out} = x + y$ \\
\texttt{ReLU} & $\text{out} = \max(0, x)$ \\
\texttt{Scale} & $\text{out} = (x \cdot \text{num}) / \text{den}$ (e.g. attention's $1/\sqrt{d}$) \\
\texttt{TopKRoute} & MoE router: top-$k$ indices per row, lowest-index tie-break \\
\texttt{Gather} & expert dispatch: $\text{out}[i] = x[\text{idx}[i]]$ \\
\texttt{Softmax} & deterministic fixed-point (Q16) integer softmax \\
\texttt{Transpose} & $\text{out}[j][i] = x[i][j]$ --- the one op a backward pass adds \\
\bottomrule
\end{tabular}
\end{center}

The softmax is the one subtlety: a floating-point softmax is not reproducible across backends, so the trace uses a pure integer scheme (max-shift for stability, an I-BERT-style fixed-point exponential~\cite{ibert}, and an integer normalize) whose output is bit-identical for prover and challenger. The test \texttt{test\_int\_softmax\_is\_a\_valid\_distribution} confirms each row sums to $\approx 2^{16}$, is monotone in the logit, and is bit-reproducible.

\subsection{The two checks}

Verification of a trace composes two checks:
\begin{enumerate}
  \item \textbf{Well-formed (chaining).} Every operation's input commitments reference either a declared trace input or the output commitment of an \emph{earlier} operation. A break --- an op reading an activation no prior op produced --- is visible from the committed leaves alone, with no openings. \texttt{verify\_chaining} returns false on the first dangling reference.
  \item \textbf{Locally correct (per-op).} An opened operation recomputes its output from its inputs --- a \texttt{MatMul} by Freivalds under a beacon-bound challenge, a glue op (\texttt{Add}, \texttt{ReLU}, \texttt{Scale}, \texttt{TopKRoute}, \texttt{Gather}, \texttt{Softmax}, \texttt{Transpose}) by direct recomputation --- and the recomputed result's commitment equals the committed output.
\end{enumerate}

\subsection{Global soundness}

\begin{theorem}[Whole-graph soundness]\label{thm:graph}
If a trace is well-formed and every operation is locally correct, then the committed final output equals the deterministic forward pass applied to the committed input.
\end{theorem}

\begin{proof}
Induction over the topological order of the trace (the operations are recorded in execution order, which is a valid topological order). \emph{Base:} a declared input activation's committed value is, by definition, the true input. \emph{Step:} consider operation $o$ with inputs $u_1, \dots, u_m$. By chaining, each $u_\ell$ is either a declared input or the output of an earlier operation; by the inductive hypothesis its committed value is the true intermediate value. Local correctness of $o$ guarantees that the committed output of $o$ equals the operation applied to those true inputs. Since each op is the exact-integer deterministic function the reference forward pass uses, the committed output of $o$ is the true intermediate value at $o$. Applying the step to the final operation yields the claim.
\end{proof}

Because everything is exact integer, activation commitments and glue recomputation are reproducible. The fixtures express attention's $QK^{\top}$ and $AV$ products plus an MoE route, gather, expert, and combine sequence. The tests verify every operation in those standalone blocks, including integer softmax.

Theorem~\ref{thm:graph} is conditional: its antecedent says \emph{every} operation is locally correct. A verifier that checks only a sampled subset has not established that antecedent; its guarantee is instead the coverage bound of \S\ref{sec:coverage}. The current tests exercise standalone blocks and synthetic graphs, not a complete production Zen inference with transcript emission on the normal serving path.

\subsection{Training is a graph, not a separate proof system}\label{sec:training}

For the included linear-SGD fixture, the additional operation is \texttt{Transpose}: gradients are $\mathrm{d}A = \mathrm{d}C \cdot B^{\top}$ and $\mathrm{d}B = A^{\top} \cdot \mathrm{d}C$. The same \texttt{MatMul} kind and Freivalds check cover its forward and backward products. Real training systems additionally require optimizer state, normalization, loss functions, stochasticity policy, precision rules, distributed collectives, and overflow behavior to be specified as deterministic trace operations before they fall within the theorem.

\begin{corollary}[One proof framework for admitted graphs]\label{cor:one-system}
Inference, embedding, and training computations expressible entirely in the admitted deterministic operation set are instances of Theorem~\ref{thm:graph}. A fabricated opened gradient matmul is subject to the same local check as a fabricated opened inference matmul.
\end{corollary}

This is verified for the fixture: \texttt{test\_training\_step\_is\_just\_a\_graph} traces a linear-layer SGD step, checks the graph, verifies every op, and fabricates a weight gradient that Freivalds catches. An input commitment identifies declared data; it does not prove authorship, licensing, completeness, or real-world provenance. Those require separate evidence and policy.

\subsection{Adversarial test evidence}\label{sec:adversarial}

The graph module ships a battery of attack tests, each asserting a specific cheat is caught:

\begin{table}[h]
\centering
\begin{tabular}{p{0.32\textwidth}p{0.58\textwidth}}
\toprule
\textbf{Attack test} & \textbf{What it proves is caught} \\
\midrule
Chain splice & operation reads an unproduced activation \\
Output substitution & opening claims a different output \\
Fabricated matmul & committed matrix output is invalid \\
Forged softmax & attention weights are altered \\
Forged route & token is sent to a different expert \\
\bottomrule
\end{tabular}
\caption{Graph adversarial fixtures at the recorded implementation snapshot.}
\end{table}

Across the four \texttt{poi} source modules, \texttt{cargo test --lib poi} runs \textbf{27 tests, 0 failed} (Property~\ref{prop:det} through Corollary~\ref{cor:one-system} are exercised by name in this set).

\section{Cross-Implementation Conformance}\label{sec:parity}

A proof is only useful at settlement if the prover, the off-chain watcher, and the chain agree on every byte. PoAI is mirrored three ways and the mirrors are tested against each other, not merely asserted to match. These parity suites are engineering gates for an execution-profile release; they are not a user-facing proof tier and do not weaken the requirement for A-Chain PoAI finality.

\subsection{One hash, one field, one serialization}

All three implementations use Ethereum \textsc{keccak}-256, the field $p=2^{61}-1$, shared domain tags, canonical matrix serialization, the same Merkle fold, and the same challenge-index encoding. The Solidity arithmetic is pure and portable, although only an A-Chain-finalized receipt may authorize mining payout.

\subsection{The on-chain witness}\label{sec:witness}

\texttt{ComputeWitnessLib.sol} is the on-chain proof-of-inference witness check. Its core is Freivalds in pure Solidity, using \texttt{mulmod}/\texttt{addmod} under $p$ so the field arithmetic is exact:

\begin{lstlisting}[language=Solidity,caption={Freivalds over $\mathbb{F}_p$ on-chain (\texttt{ComputeWitnessLib.sol}).}]
function freivalds(Matrix memory a, Matrix memory b, Matrix memory c, uint256[] memory r)
    internal pure returns (bool)
{
    if (a.cols != b.rows || b.cols != c.cols || a.rows != c.rows || r.length != b.cols) return false;
    uint256[] memory br  = _matvec(b, r);   // length k
    uint256[] memory abr = _matvec(a, br);  // length t
    uint256[] memory cr  = _matvec(c, r);   // length t
    for (uint256 i = 0; i < abr.length; i++) if (abr[i] != cr[i]) return false;
    return true;
}
\end{lstlisting}

The library exposes two complementary predicates. \texttt{verifyOpening} returns true iff the opening is Merkle-included and Freivalds-valid. \texttt{provesFraud} returns true iff it is Merkle-included and Freivalds-invalid. The current Solidity implementation derives one challenge vector and accepts dense matrices with each dimension capped at $\texttt{MAX\_DIM}=1024$. That cap prevents unbounded allocation but does not make a worst-case opening inexpensive: calldata and hashing still include every element of $A$, $B$, and $C$. The repository describes bounded slicing, but the current whole-matrix leaf format does not yet provide a production slice-to-parent binding. Production deployment therefore requires either a committed tiling scheme, an A-Chain native verifier, or a succinct proof backend, together with measured gas and payload bounds.

\subsection{Proven parity}

Parity of the tested primitives is enforced by golden vectors shared by the engine, Go verifier, and Solidity witness suite. The Solidity suite checks:
\begin{itemize}
  \item \texttt{test\_LeafParityWithProver} --- the Solidity \texttt{matmulLeaf} equals the prover's leaf;
  \item \texttt{test\_GoOpeningVerifiesOnChain} --- an opening produced by the Go verifier verifies inside the EVM unchanged;
  \item \texttt{test\_FabricatedOutputCaughtOnChain} and \texttt{test\_SwappedRevealCaughtOnChain} --- the two attack classes are caught on-chain;
  \item \texttt{test\_FreivaldsOverField} --- the field arithmetic matches.
\end{itemize}
All five pass in the recorded suite. The strongest demonstrated end-to-end fixture is Go opening $\to$ Solidity verification; Rust $\leftrightarrow$ Go parity is established through shared golden vectors. A complete Rust model-run transcript consumed by A-Chain remains an integration milestone.

\section{The AIVM as the Lux Settlement Layer}\label{sec:settlement}

PoAI consensus establishes that useful work was actually done: usefulness comes from a pre-admitted, demand-backed job whose requested output and consumer are fixed before mining, while execution evidence binds the model, input, trace, metering, and output. The A-Chain is the only state machine allowed to decide that this mining claim is valid. It owns the job, usefulness policy, execution policy, challenge beacon, proof status, work nullifier, reward calculation, and final receipt. Z-Chain compresses and settles finalized receipt transitions through P3Q, and Quasar orders and finalizes both state machines. Other chains consume this finality; neither Z-Chain nor a destination is an alternate PoAI authority.

\subsection{Mining a proof into a coin}\label{sec:miner}

An A-Chain mining job binds a task identifier, accepted model and runtime, input commitment, proof policy, reward budget, expiration, destination chain, destination recipient, and nonce. The miner commits an execution transcript before the challenge beacon is known. A-Chain then performs, or accepts under its configured finality policy, the following checks:
\begin{enumerate}
  \item \textbf{Usefulness.} The job existed before the miner's result, was admitted under a demand or network-service policy, binds a real consumer and deliverable, and cannot be created and self-certified solely by the miner. This is a protocol definition of useful work, not a proof that an answer is universally true or socially valuable.
  \item \textbf{Binding.} The result binds the A-Chain job, model, runtime, input, output, miner, and destination selected before execution.
  \item \textbf{Execution evidence.} The configured backend verifies deterministic recomputation, an optimistic transcript after its challenge period, a succinct proof, or an approved attestation policy. A bare signature or output quorum may settle a paid subjective task but cannot authorize subsidy by itself.
  \item \textbf{PoAI finality.} Optimistic evidence is not final while a fraud window is open. No irreversible issuance receipt may be exported until PoAI consensus resolves every challenge and transcript-availability obligation.
  \item \textbf{Global uniqueness.} A-Chain consumes the job's canonical work nullifier atomically with finalization.
  \item \textbf{Receipt.} A-Chain emits one receipt containing the reward authorization and destination. The destination may release only that amount to only that recipient.
\end{enumerate}

The reference proof binding collapses the task, intent, model, prompt, open block, operator, output, and runtime into one \texttt{reportData}. In the canonical topology, that binding is judged and finalized on A-Chain. A Solidity deployment elsewhere is a receipt-verification or testing adapter, not a second mining authority. The current optimistic backend reports attestation while a challenge is pending, and the reference miner consumes that pending status. Production A-Chain issuance must instead require final backend state; slashing after an irreversible mint is not finality.

\subsection{The global no-double-mint ledger}\label{sec:registry}

The global no-double-mint set is A-Chain state. Its key is derived from the A-Chain job/challenge identity and the accepted proof commitment, not from a destination-local chain id. Finalizing the job consumes that key exactly once. A second result for the same mining challenge cannot produce a second issuance authorization, regardless of requested destination.

A key based only on $(\text{model},\text{prompt},\text{output})$ is insufficient as the canonical job identity: two legitimate paid jobs may deterministically request the same computation, while an attacker may try to pre-claim a predictable tuple. The A-Chain task identifier, challenge nonce, policy epoch, and receipt identifier provide explicit domain and lifecycle binding. Destination replay protection is then simple: each destination records the finalized A-Chain receipt/nullifier it has consumed. That local consumed set prevents replay of \emph{the same A-Chain authorization}; it does not decide whether work was valid.

\subsection{Post-quantum-rooted omnichain settlement}\label{sec:oracle}

The omnichain design uses Lux as the post-quantum root of useful-work truth:
\begin{enumerate}
  \item A-Chain PoAI consensus admits the job, verifies that the bound work was performed, consumes the global nullifier, and commits the final receipt under its receipt root.
  \item Z-Chain batches finalized A-Chain receipt transitions and, once the PoAI AIR and verifier are activated, verifies their Plonky3-derived P3Q STARK/FRI settlement proof. Z-Chain proves compression and settlement of A-Chain decisions; it does not admit mining jobs or validate an unrelated raw-work claim.
  \item Quasar finalizes the A-Chain receipt root, the corresponding Z-Chain settlement root, and the validator set. The activated PQ authentication policy certifies the roots and heights; selecting ML-DSA alone is insufficient without validator-key and threshold wiring.
  \item A native atomic boundary, Warp/Teleport message, or quorum-authenticated relay carries the Z-settled A-Chain receipt and inclusion proof to the destination named before mining.
  \item The destination verifies base-layer finality, Z-Chain settlement, A-Chain receipt inclusion, destination binding, amount, recipient, and local non-consumption, then releases the authorized representation exactly once.
\end{enumerate}

Before the P3Q PoAI circuit is activated, Z-Chain may record only an authenticated, already-final A-Chain receipt root; it MUST NOT represent that record as a succinct proof of the underlying work. Activation is fail-closed: the PoAI AIR, prover, verifier, recursion policy, and A-to-Z state-transition binding must be complete, audited, and enabled by protocol version before a P3Q proof can replace the direct finality path. A shadow or replay phase may compare candidate proof outputs against finalized receipts, but it has no mint authority. ``Staged activation'' is deployment safety, not a weaker proof accepted by consensus.

\texttt{AChainRootOracle.sol} is the reference EVM verifier for the direct, pre-rollup path: a quorum of A-Chain validators signs the root and height with ML-DSA, and anyone may relay it. The production omnichain adapter SHOULD verify the Z-settled commitment or a native proof of A-Chain/Z-Chain finality. A destination MUST NOT accept a raw \texttt{ComputeProof}, TEE quote, Freivalds opening, or miner signature as a substitute for that PQ-authenticated receipt. This is how mining can settle into any supported chain while Proof-of-AI consensus exists only on A-Chain.

\begin{property}[Authenticated A-Chain root]\label{prop:nation-state}
Forging an accepted root requires either breaking the configured authentication or violating A-Chain finality. This replaces a trusted single relayer with an authenticated finality proof; the precise security level depends on the deployed validator-set and threshold protocol, not merely on selecting ML-DSA as a signature algorithm.
\end{property}

This is verified by the \texttt{AChainRootOracle.t.sol} suite (7 tests, passing), which exercises quorum acceptance, sub-threshold rejection, non-ascending-key rejection, stale-height rejection, and unregistered-validator rejection.

\subsection{Bonded providers and automated slashing}\label{sec:stake}

\texttt{MinerStakeRegistry.sol} requires a miner to bond capital in proportion to the compute capacity it declares; the bond is skin in the game. Three orthogonal authorities, one per concern:
\begin{itemize}
  \item the \textbf{miner} controls its own bond (bond / request-unbond / withdraw), with a cooldown so a discrepancy can be proven before it exits;
  \item the \textbf{slasher} --- the compute-proof fraud verifier --- slashes a bond on a \emph{proven} discrepancy, with no vote, just the math (the on-chain consumer of \texttt{provesFraud});
  \item \textbf{governance} (a Safe) may blacklist a miner for off-protocol harm the math cannot catch.
\end{itemize}
A miner is \texttt{eligible} to mine iff bonded above a floor, bonded in proportion to declared capacity, not exiting, and not blacklisted. Slashing works \emph{during} the unbond cooldown, so a miner cannot dodge a fraud proof by exiting first.

\begin{property}[Operator-safe]\label{prop:operator-safe}
By Theorem~\ref{thm:zero-fr}, an honest miner's openings always verify, so \texttt{provesFraud} can never return true against honest work; the slasher therefore cannot slash an honest bond. Slashing is reachable only by a Merkle-included opening whose Freivalds check fails --- a genuinely fabricated matmul.
\end{property}

The recorded stake-registry suite covers bonding, the capacity floor, unbond cooldown, slasher authorization, and blacklist veto.

\section{Governance: A Leaderless Quorum of Operator LLMs}\label{sec:governance}

The AIVM is governed not by a council of humans but by the network's own node operators reasoning with their language models, settling canonical decisions on-chain. The design is decomplected across contracts, each one concern.

\subsection{Sortition: leaderless committee selection}\label{sec:sortition}

\texttt{Sortition.sol} selects a committee by cryptographic sortition. An operator is in the committee for a round iff its seeded ticket falls below a threshold sized so that, in expectation, $\sim\!\texttt{size}$ of \texttt{population} registered operators are selected:
\[
  \text{ticket} = \textsc{keccak}(\text{seed} \,\|\, \text{operator}), \qquad \text{selected} \iff \text{ticket} < \Big\lfloor \tfrac{2^{256}}{\text{population}} \Big\rfloor \cdot \text{size}.
\]
Selection probability is $\text{size}/\text{population}$, so an adversary controlling fraction $f$ of the population controls $\sim\! f$ of the committee. To control a \emph{majority} of a committee it must control a majority of the \emph{whole registered population}, not merely race to fill the first \texttt{size} slots. This is the equal-vote regime --- one operator, one ticket, no stake weighting, so a sub-threshold whale cannot buy disproportionate seats. The seed must be fixed \emph{after} operators commit and be unpredictable to them (a future block hash or VRF beacon); membership is one \textsc{keccak} per check, so no on-chain enumeration of the operator set is needed.

\begin{property}[Leaderless]\label{prop:leaderless}
There is no sequencer, no privileged operator, and no leader. Committee membership is determined by post-commitment public randomness; the structural Sybil bar is a population majority, and the economic bar is a non-refundable registration cost.
\end{property}

\texttt{Sortition.t.sol} verifies this with \texttt{test\_ExpectedCommitteeSize}, \texttt{test\_Deterministic}, and \texttt{test\_CaptureRequiresPopulationMajority} (all passing).

\subsection{Categorical decisions: AIGovernor}\label{sec:governor}

\texttt{AIGovernor.sol} produces a canonical YES/NO decision (with a confidence bucket) by aggregating signed, structured operator-LLM verdicts. Each verdict is authenticated by \texttt{ecrecover} over the exact canonical preimage, the recovered signer must equal the sender, signatures are low-$S$ with $v \in \{27,28\}$, and one verdict is admitted per operator per task. To defeat copying, a commit-reveal mode seals each operator's commit during a commit window and admits the reveal \emph{strictly after} the window closes, so no operator can observe a peer's revealed fields before its own commit is sealed; the commit is operator-bound. \texttt{settle} has no access modifier --- it is permissionless, gated only by the state machine and a deadline (so no one can front-run the threshold-th honest vote to suppress a forming quorum). The tally selects the largest group by consensus key; if it meets the threshold (a strict majority, $\ge n/2 + 1$), the decision settles. There is no leader anywhere in this path.

\subsection{Continuous values: AIParams}\label{sec:params}

Where the governor decides a categorical policy, \texttt{AIParams.sol} decides a continuous \emph{value}: each operator's LLM proposes a number within a declared range, and the chain settles to the \emph{median} of a quorum of proposals and makes it the live knob value. The median is deliberately unweighted --- one operator, one proposal --- and is Byzantine-robust to any minority below $50\%$. The committee is sortition-selected with a post-commitment seed (the open-block hash), the population is snapshotted at open, and \texttt{settle} is again permissionless. \texttt{AIParams.t.sol} (16 tests, passing) verifies the median computation, the in-range invariant, and the sortition gate.

\subsection{From a settled decision to an arbitrary on-chain action}\label{sec:execute}

\texttt{AIExecute.sol} is the single surface validator consensus uses to read and act on-chain, decomplected by risk into three tiers, one mechanism:
\begin{itemize}
  \item \textbf{Read.} Any getter is \texttt{staticcall}'d and handed back as a typed value (a bool, a number, an address, a word), so consensus can query arbitrary on-chain state structured.
  \item \textbf{Enact (Tier 1, no timelock).} A knob the validators have \emph{decided} in \texttt{AIParams} is spliced as the sole argument of \texttt{target.selector(value)}; a 32-byte word ABI-encodes to any single type, so one call sets a bool / uint / int / address / bytes32. Low-risk and idempotent because the value \emph{is} the consensus output.
  \item \textbf{Execute (Tier 2/3, windowed).} An \emph{arbitrary} operation --- any target, any method, any arguments, any native value --- that the validators approved by its hash, gated by a timelock window, predecessor ordering, one-shot replay protection, a guardian veto, and an optional policy guard.
\end{itemize}
The operation hash binds \texttt{chainid} and the executor instance, so an approval can never be replayed on another chain or another executor.

The authority for execution is supplied by \texttt{AIApproval.sol}, an adapter (not a second governor) that binds a settled YES verdict to an operation through a single identity:
\[
  \text{a Thought's promptHash} \;\equiv\; \text{the AIExecute operation hash.}
\]
So ``should consensus execute operation $X$?'' is literally the governance question the operators answered. An opener poses a Thought whose \texttt{promptHash} equals \texttt{hashOperation(op)}; the operators run their LLMs and settle; if the decision is \textsc{settled} with vote \textsc{yes}, anyone may permissionlessly \texttt{confirm} it, which stamps the approval at the current block time --- and \emph{that} timestamp is where the timelock window begins. There is no admin, no owner, and no override: a NO, abstain, unsettled, or non-existent Thought yields no approval, so \texttt{execute} reverts. The only path to an approval is a real quorum YES. \texttt{AIApproval.t.sol} (7 tests, passing) verifies the settled-YES binding, the one-shot guard, and the rejection of every non-YES state.

\subsection{Governance as a second proof of useful cognition}\label{sec:govmint}

Consensus itself can produce useful cognitive artifacts, but a vote is approximately one bit and a quorum signature proves agreement rather than execution. A governance participant may earn demand fees for an accepted judgment. Subsidy requires a separate proof-bearing A-Chain job that binds the participant's model, prompt, and output. \texttt{AIConsensusMiner.sol} is a reference contract for this conjunction; in the canonical topology it cannot create an independent mint seam on C or another destination. A-Chain finalizes the proof and consumes the same global issuance allowance used by every other mining job. \texttt{AIGovernanceBridge.sol} may index the resulting Proof-of-Thought receipt, but the receipt becomes subsidy-bearing only through A-Chain finality.

\section{Economics: Bitcoin-Shaped, Fair-Mined on Useful Work}\label{sec:economics}

\subsection{The issuance schedule}

The target AI monetary policy has two fixed pools:
\begin{itemize}
  \item $D = 1{,}000{,}000{,}000{,}000$ AI is allocated at genesis to the Hanzo DAO treasury. It is not mineable and cannot be reclassified as mining emission.
  \item $M = 1{,}000{,}000{,}000{,}000$ AI is reserved exclusively for PoAI miner and validator rewards. It has no discretionary mint path: every unit must fit the schedule and a finalized A-Chain receipt.
  \item total nominal supply is bounded by $S_{\max}=D+M=2{,}000{,}000{,}000{,}000$ AI before burns. Destination representations do not add supply.
\end{itemize}

The mining pool follows a Bitcoin-shaped geometric emission. Let $H$ be the governance-fixed halving interval in finalized A-Chain blocks (nominally four years), $k=\lfloor(h-h_0)/H\rfloor$ the era, and $f\in[0,1)$ progress through it. Within an era the aggregate allowance vests linearly and its slope halves at the next era:
\begin{equation}\label{eq:allowed}
  \text{allowedMining}(h) \;=\; M(1 - 2^{-k}) \;+\; f \cdot M 2^{-(k+1)} .
\end{equation}
Thus the first era may emit at most 500 billion AI, the second 250 billion, the third 125 billion, and so on. Jobs share the available era budget according to finalized useful work under the active reward policy; raw self-reported FLOPs do not determine payout.

\begin{theorem}[Capped, continuous, exact]\label{thm:cap}
$\text{allowedMining}(h_0)=0$; the allowance is continuous and increasing; and $\text{allowedMining}(h)\to M$. The geometric sum of era budgets is exactly $M$: $\sum_{k\ge0}M2^{-(k+1)}=M$. Consequently total nominal issuance never exceeds $D+M=2$ trillion AI, and burns can only reduce it.
\end{theorem}

The canonical settlement function clamps mining issuance to $\text{allowedMining}(h)-\text{mintedMining}$, so cumulative mining and validator rewards cannot exceed \eqref{eq:allowed}. Only the canonical ledger owns this counter. Destination contracts conserve against finalized A-Chain authorizations and canonical escrow; duplicating the counter and schedule on multiple EVMs would multiply supply and is forbidden. The current reference \texttt{AICoin.sol} still implements a legacy one-billion, no-preallocation schedule and must be upgraded and tested before this monetary policy can activate.

\subsection{Deflation}

\texttt{AICoin} is burnable, and the protocol burns a governed fraction of every settled fee. Net supply change per block is $\text{subsidy}(t) - \text{burn}(t)$; since $\text{subsidy} \to 0$ while fee burn persists under use, net supply turns deflationary once the chain is in steady use.

\subsection{Why this is the next Bitcoin}

Bitcoin's social contract is a capped asset whose issuance is earned by publicly verifiable work. PoAI applies that economic shape to demand-backed AI execution while preserving the distinct roles of A-Chain work consensus, Z-Chain P3Q settlement, and Lux Quasar finality:
\begin{itemize}
  \item \textbf{Capped with fair mining} (Theorem~\ref{thm:cap}): two trillion total, a fixed one-trillion DAO allocation, and a separate one-trillion proof-earned pool with halving and a deflationary tail.
  \item \textbf{Public and permissionless} (\S\ref{sec:miner}, \ref{sec:registry}): anyone may perform an open A-Chain job under its admission and proof policy; the finalized receipt binds the reward recipient and optional destination.
  \item \textbf{Leaderless} (Property~\ref{prop:leaderless}): no sequencer, no privileged operator; governance is sortition over the whole operator population.
  \item \textbf{Operator-safe} (Property~\ref{prop:operator-safe}): bond-and-slash, never exploitable against honest work, by the zero-false-reject theorem.
  \item \textbf{Post-quantum-oriented} (Theorem~\ref{thm:pq}, Property~\ref{prop:nation-state}): the local arithmetic check is information-theoretic, while commitments, authentication, and finality use explicitly stated post-quantum and consensus assumptions.
\end{itemize}
The intended difference is that the work is useful because an admitted job requests it. PoAI can establish execution accountability for supported deterministic graphs; it does not establish semantic truth or market value. A-Chain PoAI governs eligibility for AI-work rewards and subsidy, Z-Chain P3Q compresses and settles finalized receipt transitions, and Quasar secures and finalizes both chains.

\subsection{Why existing AI clouds participate}

PoAI is designed as an incremental revenue rail, not only a replacement marketplace. A centralized cloud, a decentralized provider, or an idle workstation may attach a job-specific transcript to inference, embedding, evaluation, or admitted training work it is already paid to run. The provider keeps its ordinary demand fee and, if PoAI consensus finalizes the evidence, earns a declining share of the mining allowance. The same adapter can accept open decentralized jobs when capacity would otherwise be idle.

This ``compute once, earn twice'' claim is valid only when proof capture is substantially cheaper than the original job and validators do not replay the full accelerator workload. Exact-integer commitments plus CPU-verifiable openings supply that asymmetry for supported operations: the provider performs an $O(n^3)$ matrix product, while a CPU checks a challenged product in $O(n^2)$ plus commitment overhead. Full-work accountability still requires graph binding, unpredictable post-commitment challenges, coverage or an activated succinct proof, transcript availability, and verifiable metering.

Subsidy eligibility must resist circular demand. A miner-created job, a self-reported GPU-hour, a copied output, or a customer signature alone cannot mint AI. The active policy must bind independent demand or a governed network-service budget, cap rewards per epoch, reject replay through the global nullifier, and make the reward no larger than the available schedule. These controls turn cloud workloads into public evidence without turning fake invoices into a mint.

\section{Verified Test Evidence (Aggregate)}\label{sec:evidence}

The following suites are implementation evidence for individual components. They are not evidence of a production end-to-end mining deployment.

\begin{table}[h]
\centering
\begin{tabular}{lrl}
\toprule
\textbf{Suite} & \textbf{Result} & \textbf{Command} \\
\midrule
\texttt{crypto/poi} (Go verifier) & 22 passed, 0 failed & \texttt{go test ./...} \\
\texttt{hanzo-engine} \texttt{poi} (Rust core) & 27 passed, 0 failed & \texttt{cargo test --lib poi} \\
\texttt{contracts/ai} (Solidity, 20 suites) & 256 passed, 0 failed & \texttt{forge test} \\
\bottomrule
\end{tabular}
\caption{Recorded component-test results at the paper's implementation snapshot. Counts may change as suites evolve.}
\end{table}

The recorded Go fixture measured 1.13\,ms per small opening on its test host. This is not an on-chain gas benchmark or a production-model benchmark. Before launch the project still requires a real Zen model to emit a complete transcript on the normal execution path, a published availability protocol, measured worst-case challenge payloads, a finalized-not-pending issuance gate, and an end-to-end A-Chain receipt exported to and consumed by a destination chain.

\section{Post-Quantum Primitives}\label{sec:pq}

The AIVM targets post-quantum security across its arithmetic, authentication, and transport layers. The following address assignments and candidate primitives are defined in the Lux precompile namespace; registration does not by itself establish production deployment or threshold-protocol maturity:

\begin{table}[h]
\centering
\small
\begin{tabular}{p{0.20\linewidth}p{0.17\linewidth}p{0.53\linewidth}}
\toprule
\textbf{Primitive} & \textbf{Address} & \textbf{Role} \\
\midrule
ML-KEM (FIPS 203) & \texttt{0x012201} & module-LWE KEM \\
ML-DSA (FIPS 204) & \texttt{0x012202} & module-LWE signature; the AChainRootOracle verifier \\
SLH-DSA (FIPS 205) & \texttt{0x012203} & hash-based signature \\
Pulsar & \texttt{0x012204} & module-LWE threshold research implementation \\
P3Q & \texttt{0x012205} & Plonky3-derived, pairing-free STARK/FRI settlement substrate \\
X-Wing KEM & \texttt{0x002221} & X25519 $+$ ML-KEM-768 hybrid (encapsulate) \\
\bottomrule
\end{tabular}
\caption{Post-quantum precompiles (verified addresses from each precompile's \texttt{contract.go}).}
\end{table}

The ML-DSA precompile is the intended verifier for authenticated A-Chain and Z-Chain root certificates. Production claims require node wiring, active validator keys, threshold policy, downgrade prevention, and deployment tests. P3Q supplies the Plonky3-derived, pairing-free STARK/FRI substrate intended for the Z-Chain settlement rollup, but the exact PoAI AIR, recursive batch policy, A-to-Z state binding, and end-to-end verifier remain work in progress until audited and activated. Pulsar remains threshold-signature research and must not be described as a deployed malicious-secure DKG/signing service until that protocol and its networking are complete.

Prompt confidentiality for proof-of-inference is provided by \texttt{luxfi/crypto/promptseal} --- a pure-Go HPKE envelope (not a precompile) that seals a user's prompt to an operator's registered public key under the X-Wing hybrid KEM (X25519 $+$ ML-KEM-768), HKDF-SHA256, and ChaCha20-Poly1305, with domain tag \texttt{"hanzo/poi/prompt-seal/v1"}. Hybrid means the seal stays confidential if \emph{either} X25519 \emph{or} ML-KEM-768 holds; only the chosen operator, inside its compute boundary, can open it. The matching on-chain surface is the X-Wing \emph{encapsulate} precompile at \texttt{0x002221}; key generation and decapsulation are intentionally excluded on-chain because they would expose secret material, and run off-chain in the \texttt{promptseal} library.

\section{Related Work}

\textbf{zkML.} Zero-knowledge proofs of ML inference~\cite{zkml} can provide succinct non-interactive verification, usually with substantial prover overhead and system-specific computational assumptions. Pairing-based constructions are not post-quantum. The Freivalds core is cheaper for one opened matrix product, but the complete optimistic system additionally pays for commitments, availability, watcher re-execution, and dispute latency. A fair comparison must measure the complete protocol on the same model and threat policy.

\textbf{Trusted execution environments.} TEE attestation assumes hardware, firmware, collateral, measurement, and revocation trust. The AIVM accommodates TEE evidence for confidential jobs, but the intended public deterministic path is hardware-independent exact-integer execution. That path is not production-final until transcript availability and A-Chain challenge finality are integrated.

\textbf{Optimistic rollups.} PoAI's fraud-proof structure --- commit a root, allow anyone to challenge an opening within a window, slash on a proven discrepancy --- shares optimistic rollups' philosophy~\cite{optimistic}, specialized to matrix computation where the fraud proof is a single Freivalds check with $O(\log n)$ Merkle overhead rather than a full re-execution.

\textbf{Proof of work.} Bitcoin~\cite{bitcoin} couples work directly to leader election and consensus security. A-Chain PoAI is instead a useful-work validity consensus: it determines that an admitted job was actually performed and may authorize issuance; Z-Chain P3Q compresses and settles that finalized state; Lux Quasar supplies base-layer ordering and finality. The computation is useful because a real, pre-admitted consumer job requests and consumes its result.

\textbf{Matrix-multiplication proof of work.} Komargodski and Weinstein~\cite{matmulpow} propose reusing arbitrary matrix multiplication for both an external workload and proof of work; BTX~\cite{btx} explores a header-derived finite-field MatMul instantiation. Deterministic kernels, canonical transcripts, cross-device parity tests, and staged proof activation are useful engineering patterns. A chain-derived matrix race, however, does not by itself settle a requested model execution: unless the product is bound to a demand-backed job, its utility is hardware adjacency rather than a consumed AI result. Exact replay also makes verification the same asymptotic order as execution, while delegating replay to signed GPU attestors adds an explicit trust assumption. AIVM therefore adopts deterministic integer computation and proof-friendly commitments without making AI execution the leader-election oracle. A-Chain PoAI consensus validates useful work; Z-Chain P3Q settles the proof batches; Lux supplies the PQ-secured base layer; destination chains consume the resulting receipt.

\section{Conclusion}

Proof of AI is a useful-work consensus: it validates that a pre-admitted, demand-backed AI job was actually executed and produced its committed result. Its strongest implemented primitive is an exact-integer Freivalds check with zero false-reject for an honest opened matrix product and information-theoretic local error. Typed graph commitments, cross-language fixtures, evidence backends, and settlement contracts extend that primitive, but their composition requires explicit coverage, availability, finality, and deployment assumptions. The A-Chain is the sole PoAI authority that admits mining jobs, finalizes proofs, consumes work nullifiers, and authorizes subsidy. Z-Chain is the P3Q proof-compression and settlement rollup for those finalized transitions, and Lux Quasar plus activated PQ authentication make the A/Z settlement root the omnichain base-layer fact. Other chains verify that receipt and route value; they never create an independent proof or supply schedule. The remaining engineering milestone is an end-to-end production model run whose transcript is available, challenged, finalized by A-Chain PoAI consensus, proven and settled through the activated P3Q rollup on Z-Chain, PQ-certified by Lux, and consumed exactly once at a destination. Until that test is green, this paper is a protocol and implementation report, not a claim of a completed production mining network.

\section*{Acknowledgments}

This work was supported by Hanzo Industries, Lux Industries, and the Zoo Labs Foundation. The canonical contract implementation lives at \texttt{luxfi/standard} under \texttt{contracts/ai/}; the soundness core lives in \texttt{hanzo-engine} (\texttt{src/poi*.rs}) and \texttt{luxfi/crypto} (\texttt{crypto/poi/}).

\begin{thebibliography}{9}

\bibitem{freivalds} R. Freivalds, \textit{Probabilistic machines can use less running time}, Information Processing (IFIP Congress), 1977, pp. 839--842.

\bibitem{schwartz} J. T. Schwartz, \textit{Fast probabilistic algorithms for verification of polynomial identities}, Journal of the ACM 27(4), 1980, pp. 701--717.

\bibitem{zippel} R. Zippel, \textit{Probabilistic algorithms for sparse polynomials}, in Symbolic and Algebraic Computation (EUROSAM), 1979, pp. 216--226.

\bibitem{ibert} S. Kim, A. Gholami, Z. Yao, M. W. Mahoney, K. Keutzer, \textit{I-BERT: Integer-only BERT Quantization}, ICML, 2021.

\bibitem{bitcoin} S. Nakamoto, \textit{Bitcoin: A Peer-to-Peer Electronic Cash System}, 2008.

\bibitem{matmulpow} I. Komargodski and O. Weinstein, \textit{Proofs of Useful Work from Arbitrary Matrix Multiplication}, arXiv:2504.09971, 2025.

\bibitem{btx} BTX Contributors, \textit{BTX Reference Node: MatMul Proof of Work}, \url{https://github.com/btxchain/btx}, accessed August 2026.

\bibitem{zkml} D. Kang, T. Hashimoto, I. Stoica, Y. Sun, \textit{Scaling up Trustless DNN Inference with Zero-Knowledge Proofs}, arXiv:2210.08674, 2022.

\bibitem{optimistic} H. Kalodner, S. Goldfeder, X. Chen, S. M. Weinberg, E. W. Felten, \textit{Arbitrum: Scalable, private smart contracts}, USENIX Security, 2018.

\bibitem{fips204} National Institute of Standards and Technology, \textit{FIPS 204: Module-Lattice-Based Digital Signature Standard (ML-DSA)}, 2024.

\bibitem{fips203} National Institute of Standards and Technology, \textit{FIPS 203: Module-Lattice-Based Key-Encapsulation Mechanism Standard (ML-KEM)}, 2024.

\bibitem{xwing} M. Barbosa, D. Connolly, et al., \textit{X-Wing: The Hybrid KEM You've Been Looking For}, IACR ePrint 2024/039, 2024.

\end{thebibliography}

\end{document}