papers/zoo-poai-consensus/sections/23-implementation-status.tex

\section{Implementation Status}
\label{sec:impl-status}

We state plainly what is built and tested versus what is designed, so the paper's claims
can be checked against code. The repository contains executable reference implementations
for the activation-trace commitment, proof-bearing forward, graph fixtures, challenger,
and EVM enforcement. These surfaces test the construction; they are not the active A-Chain
consensus path. A complete production model path, data availability, consensus admission
and finality, metering, nullification, and P3Q settlement remain integration work. Test
counts below are snapshots of named suites, not claims of live mining.

\subsection{Built and tested: the Freivalds core}

The matmul verifier of Section~\ref{sec:freivalds} is implemented as a backend-agnostic,
dependency-light module (\texttt{hanzo-engine/src/poi.rs}, whose only external dependency
is \texttt{sha3}). It realizes the construction exactly as specified: arithmetic over the
Mersenne field $\mathbb{F}_p$ with $p = 2^{61}-1$, run on the engine's \emph{exact integer
accumulator} (\texttt{exact\_matmul}, a whole-$K$ $i64$ reduction with no cross-block
$f32$ rescale), with the Freivalds identity $A(Br) = Cr$ evaluated by left/right
matrix--vector products (\texttt{freivalds\_verify}) and deterministic, beacon-bound
challenge derivation. Being dependency-free of the forward pass, its soundness is testable
in isolation. The \texttt{poi.rs} suite is \textbf{7/7 passing}, and each test pins a claim
from Section~\ref{sec:freivalds}:

\begin{itemize}[leftmargin=1.4em]
\item \texttt{test\_honest\_matmul\_passes} --- an honest $C = AB$ passes every challenge
vector (zero false rejection; the exact-integer guarantee).
\item \texttt{test\_tampered\_output\_is\_caught} --- flipping a single output entry
($50 \to 51$) is caught (Theorem~\ref{thm:freivalds-one} soundness).
\item \texttt{test\_larger\_random\_matmul\_catches\_sparse\_cheat} --- in a
$16\times24 \cdot 24\times16$ product, a single buried off-by-one is caught; the
\emph{sparse-cheat} case that motivates challenging every layer.
\item \texttt{test\_negative\_entries\_field\_reduction} --- signed int8 operands reduce
correctly into $[0,p)$ (Euclidean remainder), and a tampered negative-entry product is
caught.
\item \texttt{test\_challenge\_derivation\_deterministic} --- prover and verifier derive
the \emph{identical} challenge from the same seed; different seeds give different
challenges (the reproducibility half of anti-replay, Lemma~\ref{lem:anti-replay}).
\item \texttt{test\_wrong\_dims\_rejected} --- a shape mismatch fails \emph{closed} rather
than reading out of bounds.
\item \texttt{test\_derive\_challenges\_keccak\_golden\_parity} --- the keccak challenge
derivation matches the Go verifier \emph{byte-for-byte} against a pinned golden hex vector;
if either side's keccak or $\mathrm{BE}_{32}(j)\,\|\,\mathrm{BE}_{64}(i)$ encoding drifts,
this test (and its Go twin \texttt{TestDeriveChallengesGolden}) breaks. This is what
guarantees a Rust-emitted proof verifies against the on-chain Go verifier unchanged.
\end{itemize}

\subsection{Built and tested: the transcript, the proof-bearing forward, the graph}

The wire that the earlier draft marked ``designed'' is implemented as three further
modules, all in \texttt{hanzo-engine/src/}, all tested.

\paragraph{Activation-trace transcript and challenger (\texttt{poi\_transcript.rs}, 8/8).}
A forward pass commits each proof-bearing matmul as a keccak Merkle leaf over its
exact-integer $(A,B,C)$ (\texttt{matmul\_leaf}, domain tag
\texttt{"hanzo/poi/matmul-leaf/v1"}); the root is the \texttt{transcriptRoot} the prover
posts. The challenger derives a beacon-unpredictable matmul \emph{index}
($\keccak(\text{beacon}\,\|\,\text{root})\bmod L$), has the prover open it (reveal
$(A,B,C)$ plus a Merkle inclusion proof), checks the operands were the committed ones, and
Freivalds-checks $C=A\cdot B$ with $k$ beacon-bound vectors (\texttt{verify\_opening}). The
Merkle fold (odd levels duplicate the last node; index fold $\mathsf{even}\!\to\!
\keccak(node\|sib)$, $\mathsf{odd}\!\to\!\keccak(sib\|node)$) is identical to
\texttt{AIMiner.\_verifyMerkle}, so a proof built here verifies on-chain. The suite
proves honest passes verify under every beacon, a fabricated $C$ is caught, a swapped-in
$C$ fails Merkle inclusion, and the root binds every operand.

\paragraph{Sound emission (\texttt{poi\_forward.rs}, 3/3).} The audit's CC-01 was that the
value a layer \emph{returns} must be the value it \emph{commits}. \texttt{ProvableLinear}
makes this hold by construction: it quantizes $x$ per-row to int8, forms $C=\bar x\cdot
W^\top$ on the exact $i64$ accumulator, commits $(\bar x, W^\top, C)$, and returns
$\mathrm{dequant}(C)$---so a challenger's Freivalds over the committed operands re-checks
the \emph{same} computation that produced the output, not an $f32$ shadow that disagrees
with it. \texttt{test\_provable\_ffn\_emits\_verifiable\_transcript} runs a real SwiGLU FFN
($\texttt{gate}/\texttt{up}/\texttt{down}$) under emission and verifies every committed
matmul; \texttt{test\_output\_is\_the\_committed\_value} confirms the returned $y$ equals
$\mathrm{dequant}(\text{committed } C)$ to within float tolerance (the output-binding
property, proved in the emission companion~\cite{poiemission}).

\paragraph{Full-graph composition (\texttt{poi\_graph.rs}, 9/9).} A prover could commit
correct matmuls computed on \emph{unrelated} inputs; \texttt{GraphTrace} closes this with a
typed computation trace over hash-named activations. Each op commits
$(\mathsf{kind}\,\|\,\text{input commitments}\,\|\,\mathsf{params}\,\|\,\text{output
commitment})$; \emph{chaining} (every input is a prior output or a declared input) is
checked from the leaves alone, and \emph{local correctness} re-checks each op---\textsc{MatMul}
by Freivalds, the deterministic glue (\textsc{Add}, \textsc{ReLU}, \textsc{Scale},
\textsc{TopKRoute} under the canonical lowest-index tie-break, \textsc{Gather},
\textsc{Softmax} as a pure fixed-point integer reduction, \textsc{Transpose}) by direct
recomputation. The suite emits and verifies a real MoE block (router $\to$ top-$k$ $\to$
gather $\to$ expert up/down matmuls $\to$ residual), the attention spine
($QK^\top\to$ scale $\to$ integer softmax $\to\cdot V$), and---with the one
\textsc{Transpose} op a backward pass adds---a full SGD training step, catching a fabricated
gradient by Freivalds exactly as a faked inference output
(\texttt{test\_training\_step\_is\_just\_a\_graph}). This is the code behind the canon
``inference, embedding, and training are graphs, not three proof systems.''

\paragraph{Adversarial red-team battery (\texttt{tests/poi\_adversarial.rs}, 11/11).} Each
test plays the attacker. The eight attacks---fabricate the final output, fabricate a hidden
intermediate matmul, a sparse deep cheat, swap the output at open time, tamper an input at
open time, pre-fit $C$ to a guessed challenge, a griefer's fabricated opening, and a
quantization lie ($y\neq\mathrm{dequant}(C)$)---are each \emph{caught}; the three defenses
(two honest machines emit the byte-identical root, an honest forward verifies under every
beacon, a shape mismatch fails closed) confirm zero false rejection. The pre-fit test is the
load-bearing one for the beacon: a forgery tuned to a guessed $r_1$ passes $r_1$ and fails a
fresh beacon-derived $r_2$.

Jointly the engine carries \textbf{27 unit tests (\texttt{poi.rs} 7, \texttt{poi\_transcript.rs}
8, \texttt{poi\_forward.rs} 3, \texttt{poi\_graph.rs} 9) plus 11 adversarial tests = 38
passing}.

\subsection{Built and tested: the two determinism prerequisites}

The exact-integer Freivalds check is bit-exact only if the surrounding decode is
reproducible; Section~\ref{sec:freivalds}'s determinism contract names the two places a
naive runtime injects nondeterminism, and both are closed in the engine. The
\emph{lowest-token-id argmax tie-break} (\texttt{hanzo-engine/src/sampler.rs}) breaks a
greedy-decoding logit tie to the lowest token id via a strict ``$>$'' scan, correcting
Rust's \texttt{Iterator::max\_by} (which returns the \emph{last} maximal element); the
\emph{canonical MoE routing top-$k$} (\texttt{hanzo-engine/src/ops.rs}, and its in-graph
twin \texttt{top\_k\_indices} in \texttt{poi\_graph.rs}) orders each row by score descending
then expert-index ascending under a total order, so prover and verifier select identical
experts (a different expert is a different sub-network). These are the routing analog of the
argmax tie-break and are what make the ``re-derive and compare'' premise actual rather than
aspirational for the greedy and MoE-routing cases.

\subsection{Built and tested: the candidate canonical Go verifier}

The verifier intended for A-Chain integration is a dependency-light Go package living beside the canonical
\texttt{Keccak256} (\texttt{luxfi/crypto/poi}): \texttt{Verify}/\texttt{VerifyMulti} over
$\mathbb{F}_p$ ($p=2^{61}-1$) on the exact integer accumulator, the transcript and
\texttt{VerifyOpening}, the wire codec, and keccak \texttt{DeriveChallenges}. The engine's
\texttt{poi.rs} is the prover-side mirror; the two agree byte-for-byte, enforced by the
shared golden challenge vector (\texttt{TestDeriveChallengesGolden}, the Go twin of the
Rust parity test above). The suite is \textbf{23/23 passing}, including the honest-opening,
fabricated-output-caught, swapped-reveal-caught, Merkle-index-fold, sparse-cheat,
encode/decode round-trip, wire-fuzz, oversized-dims-rejected, griefer-cannot-frame, and
pre-fit-challenge cases---the Go-side mirror of the Rust adversarial battery, plus a
verification-throughput scaling test.

\subsection{Built and tested: reference EVM enforcement surfaces}

The reference witness is verified in the EVM, not asserted by a watcher. These contracts
live in \texttt{luxfi/standard} (\texttt{contracts/ai/\{governance,mining,token,compute,relay,registry\}/}); the eight Proof-of-AI
suites total \textbf{87 tests passing} (\texttt{forge test}), distributed as follows.

\begin{itemize}[leftmargin=1.4em]
\item \textbf{\texttt{ComputeWitnessLib.sol} (5/5).} Freivalds over $\mathbb{F}_p$ via
\texttt{mulmod}/\texttt{addmod}, the Merkle fold, and the beacon challenge, byte-identical
to the prover (same domain tag, same $(\text{rows},\text{cols},\text{data})$ serialization,
same fold, same derivation). \texttt{verifyOpening} accepts a genuine opening;
\texttt{provesFraud} is its complement---inclusion $\wedge\,\neg\mathsf{Freivalds}$---the
predicate a challenger exhibits to slash. Opened dimensions are capped
(\texttt{MAX\_DIM}) so a griefer cannot submit an unbounded opening.
\item \textbf{\texttt{OptimisticEvidence.sol} (18/18).} The commit/challenge/slash state
machine: \texttt{submit} escrows a bond and opens a window with the commit block recorded
as the challenge beacon (\texttt{blockhash(commitBlock)}---fixed after the prover signed,
so it cannot pre-fit a dodging $C$); \texttt{challenge} re-checks inclusion $+$ Freivalds
on-chain via \texttt{provesFraud} and, only on a verified discrepancy, marks the commitment
\textsc{Fraudulent} and pays the bond to the challenger; \texttt{reclaim} returns the bond
after an un-challenged window. The state machine is one-shot per \texttt{reportData} (a
slashed liar cannot re-post), a zero bond is rejected (a liar always has skin in the game),
and effects precede the single pull-of-funds (no reentrancy re-claim).
\item \textbf{\texttt{AIMiner.sol} (12/12).} A reference mint gate, \emph{fail-closed}:
\texttt{mine} requires receipt shape $+$ finality $+$ Merkle inclusion under an accepted
root $+$ a \texttt{ComputeProof} binding the receipt's own measured model/prompt/output,
and reverts (\texttt{ProofGateUnavailable}) if no verifier is wired---so a forged root alone
cannot mint. The subsidy goes to the bound requester, is clamped to the vested halving
allowance, and is one-shot per intent.
\item \textbf{\texttt{ComputeProofEnforcement.t.sol} (19/19).} The end-to-end enforcement
that a proofless or mis-bound mint is rejected and a correctly-bound one succeeds, across
the proof-type profiles.
\item \textbf{\texttt{AICoin.sol} (11/11).} A legacy capped/halving token fixture:
$\texttt{MAX\_SUBSIDY}=10^9$ \textsc{ai}, $\texttt{HALVING\_PERIOD}=4\ \text{years}$, the
slope halving each epoch and the cumulative mint structurally bounded by
$\text{allowed}(t)\le\text{MAX}$. Its $10^9$ parameter is not the canonical \textsc{AI}
monetary policy; production must use the approved $2$ trillion allocation and common
A-Chain issuance schedule described in the Hanzo AI Chain specification.
\item \textbf{\texttt{AIComputeRegistry.t.sol} (6/6).} A reference no-double-mint ledger.
Production uses the A-Chain job/nullifier key; a tuple of model, prompt, and output is not a
sufficient consensus identity by itself.
\item \textbf{\texttt{MinerStakeRegistry.sol} (8/8).} A miner bonds capital in proportion to
declared capacity; the fraud-proof verifier slashes on a proven discrepancy with a cooldown
that is the fraud window.
\item \textbf{\texttt{L3Registry.sol} (8/8).} A Zoo application-directory fixture. It
may discover receipt consumers, but has no work-admission, finalization, or mining authority.
\end{itemize}

The post-quantum cross-layer root relay \texttt{AChainRootOracle.sol} (an ML-DSA validator
quorum replacing a trusted single relayer; Section~\ref{sec:l3-settlement}) and the
leaderless operator-quorum governance (\texttt{AIGovernor},
\texttt{AIParams}, with \texttt{AIExecute}/\texttt{AIApproval}) are likewise
implemented in the same standard library and carry their own passing suites; we cite them
as candidate surfaces with which the settlement path composes,
without re-tabulating their tests here.

\subsection{Designed, not yet built}

The honest remaining work is now a named, smaller set; none of the following is implemented
at the time of writing.

\begin{enumerate}[leftmargin=1.6em]
\item \textbf{Production consensus integration.} Normal serving-path transcript emission,
artifact availability, full-graph coverage, economic metering, A-Chain job admission,
finalized proof gating, nullifier consumption, and P3Q settlement are not yet one live path.
Shadow/replay P3Q stages have no mint authority.
\item \textbf{RepOps (pinned reduction tree).} The deterministic-floating-point mode for the
fp16/bf16/fp8 tier (Section~\ref{sec:repops}) is designed and proven sound
(\cite{poisoundness}); the quantized integer path is what is built and is what the \Zoo{}
zoo ships. Exact Freivalds over the current $f8q8$ fast path (which sums int8 block dots in
$f32$ across blocks) would false-reject honest cross-hardware provers; the proof path
instead uses \texttt{exact\_matmul}'s whole-$K$ $i64$ reduction, and the floating-point tier
awaits the RepOps cross-block pinning.
\item \textbf{The sequential-chaining proof.} Binding consecutive recurrent states (and,
identically, consecutive diffusion latents) in the commitment
(Sections~\ref{sec:ssm-proof}, \ref{sec:diffusion}) is designed and proven sound modulo its
discharge obligation (\cite{poisoundness}). The \emph{forward}/\textsc{Transpose} graph that
covers dense, attention, MoE, and training is built (above); the per-step state seam for
state-space and diffusion models is the remaining emission work.
\item \textbf{Emission of the long-tail architectures.} The families the test suite
exercises (dense/SwiGLU, attention with integer softmax, MoE, training) emit and verify; the
remaining model-zoo families inherit the same proof obligations (\cite{poisoundness},
Theorem on whole-zoo coverage) but are not yet wired to emit a transcript. This is breadth
of integration, not a missing technique: no third core verification method is required.
\end{enumerate}

\begin{remark}[What the tested system does and does not establish]
The cited Rust, Go, and Solidity tests establish that the
\emph{mathematical heart}---``you cannot claim the matmul without doing it''---is
implemented correctly over the exact integer accumulator, that it \emph{emits} from a real
forward/graph and \emph{composes} across attention, MoE, and a training step, that the
challenger and the on-chain witness re-check it byte-identically in two more languages, and
that a reference mint gate can fail closed. What they do \emph{not} establish is a live
A-Chain mining path, production data availability and metering, P3Q settlement, the
floating-point tier (RepOps), or emission of architectures outside the tested set. We keep the boundary explicit, in keeping with the decomplecting
discipline of the rest of the paper: the verifier is a value (a pure function of operands
and a challenge), the emission supplies those operands from a real pass, and the on-chain
gate consumes the result---three separable concerns, each now built where this paper's
earlier draft had only the first.
\end{remark}