papers/lux-p3q-precompile/lux-p3q-precompile.tex

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

\hypersetup{colorlinks=true,linkcolor=black,citecolor=blue,urlcolor=blue}

\lstdefinelanguage{Go}{
  morekeywords={break,case,chan,const,continue,default,defer,else,fallthrough,
                for,func,go,goto,if,import,interface,map,package,range,return,
                select,struct,switch,type,var,nil,true,false,error,byte,uint64,
                uint32,uint8,int,bool,string,byte,make,len,cap,copy,append},
  sensitive=true,
  morecomment=[l]{//},
  morecomment=[s]{/*}{*/},
  morestring=[b]",
  morestring=[b]`,
}

\lstset{
  basicstyle=\ttfamily\scriptsize,
  breaklines=true,
  frame=single,
  numbers=left,
  numberstyle=\tiny\color{gray},
  keywordstyle=\color{blue!70!black}\bfseries,
  commentstyle=\color{green!50!black}\itshape,
  stringstyle=\color{red!60!black},
  showstringspaces=false,
}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{definition}{Definition}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{remark}{Remark}

\title{P3Q: An EVM Precompile for On-Chain\\
Strict-Post-Quantum Verification}

\author{Lux Industries, Inc.\\
\texttt{[email protected]}}

\date{}

\begin{document}

\maketitle

\begin{abstract}
We present P3Q, the LP-4200 slot \texttt{0x012205} EVM precompile that
serves as the canonical on-chain dispatch point for the strict
post-quantum STARK proof backend used in the Lux Quasar consensus
finality path. P3Q is intentionally thin: it parses a length-prefixed
wire envelope, gates on a 4-byte magic header, charges gas linearly in
input length, and dispatches a single registered backend verifier
that lives in an audited Rust crate. The structural pre-filter is
constant-time over wire calldata; the gas schedule is monotonic and
upfront-charged; and the verification dispatch reduces, when the
payload carries an ML-DSA-65 signature, to a single FIPS~204
\texttt{ML-DSA.Verify} call on the parsed triple. We accompany the
precompile with a four-file EasyCrypt theory at admit budget $0/0$, a
Lean~4 bridge theorem chain, a constant-time Jasmin source for the
structural gate, a \texttt{dudect} harness wired for $10^9$-sample
submission runs, and an exhaustive Go test surface including bit-flip
and length-field fuzz coverage. We discuss the soundness role of
constant-time over PUBLIC wire calldata at the EVM boundary, the gas
side-channel posture, the composition with the upstream Pulsar /
threshold ML-DSA stack, and how P3Q decomplects the EVM-precompile
dispatch surface from the proving-time backend.
\end{abstract}

\tableofcontents
\newpage

\section{Introduction}\label{sec:intro}

The Lux consensus stack is a hybrid classical / post-quantum (PQ)
finality system: classical BLS12-381 aggregates form low-latency
operational finality, and three independent PQ tracks
(Module-LWE ML-DSA, Module-LWE Corona, and strict-PQ STARK
\emph{Pulsar3-Quantum} = P3Q) provide durable finality under quantum
adversaries. On-chain verification of these PQ proofs is mediated by
the EVM precompile block at LP-4200 addresses
\texttt{0x012201}..\texttt{0x012206}: ML-KEM, ML-DSA, SLH-DSA, Pulsar
(threshold ML-DSA), P3Q, and Corona, respectively.

This paper documents \textbf{P3Q}, the precompile at slot
\texttt{0x012205}. P3Q is not a new cryptographic primitive: it is a
\emph{dispatch surface}. Its purpose is to be the smallest, most
boring, most easily audited bridge between (a)~the EVM caller, which
presents a length-prefixed wire envelope, and (b)~the audited Rust
backend verifier crate
\texttt{p3q/crates/p3q-verifier}~\cite{p3q-verifier}, which executes
the strict-PQ STARK / FRI verification body over a cSHAKE256-keyed
Goldilocks-prime field. The contribution is not the verifier; the
contribution is the \emph{discipline} that lets us assert end-to-end
soundness across the EVM-to-FFI-to-Rust boundary at admit budget
$0/0$ in an EasyCrypt operational model.

\paragraph{Design intent.} P3Q follows three Hickey-style
decomplection principles enforced throughout the Lux PQ stack:

\begin{enumerate}
\item \textbf{Single concern per primitive.} P3Q is a wire-format
gate plus a single dispatch. It does not own keys, randomness,
session state, or threshold logic. Threshold ML-DSA lives at slot
\texttt{0x012204} (Pulsar); P3Q only verifies the final byte string
the threshold layer produces.
\item \textbf{Wire format is its own object.} The
\texttt{[version][BE32 proof\_len][proof][BE32 pub\_len][pub]}
envelope is round-trip-stable and uniquely-decodable. The version
byte is a future-extension point; the magic header is a defense-in-
depth pre-filter.
\item \textbf{Backend is replaceable, not entangled.} The
\texttt{RegisterVerifier} mechanism makes the backend a single
function pointer set once at startup. Soundness load-bearing on the
audited backend is therefore a single, locally-auditable claim
rather than a diffuse system property.
\end{enumerate}

The rest of this paper specifies the wire format
(\S\ref{sec:wire}), gas model (\S\ref{sec:gas}), reduction to
FIPS~204 \texttt{ML-DSA.Verify} (\S\ref{sec:reduction}), and STARK
extension semantics (\S\ref{sec:stark}); presents the implementation
(\S\ref{sec:impl}); reports evaluation results (\S\ref{sec:eval});
covers security posture including constant-time obligations and the
gas side channel (\S\ref{sec:security}); compares P3Q to the
neighboring EVM precompiles (\S\ref{sec:comparison}); and concludes
with the roadmap (\S\ref{sec:conclusion}).

\section{Background: Pulsar and the Strict-PQ Track}\label{sec:bg}

P3Q is the on-chain dispatch surface for the strict-PQ branch of the
Lux Quasar consensus protocol. The strict-PQ branch is a STARK proof
over a cSHAKE256-keyed Goldilocks-prime field, with a wire proof-
backend identifier $\mathsf{ProofBackendP3QSTARKFRISHA3} = 0x22$
pinned in \texttt{consensus/config/pq\_mode.go}. The STARK trace
witnesses, at minimum, that a Pulsar threshold ML-DSA-65 signature
verifies under a given group public key on a given message
binder~\cite{pulsar}.

The Pulsar threshold layer~\cite{pulsar} is itself a Class~N1
construction: the byte-string produced by the threshold combine
operation on $t$-of-$n$ Round-2 responses equals the byte-string
produced by single-party FIPS~204 \texttt{ML-DSA.Verify} on the
Lagrange-reconstructed secret. P3Q therefore inherits Pulsar's
byte-equality theorem at the signature layer and adds a STARK wrapper
for succinct on-chain verification of (potentially batched, but in
v0x01 single) signature certificates.

The composition is:
\[
\underbrace{\text{P3Q precompile (this paper)}}_{\text{EVM boundary}}
\;\longrightarrow\;
\underbrace{\text{Rust verifier crate}}_{\text{cgo + audit}}
\;\longrightarrow\;
\underbrace{\text{Pulsar / FIPS 204 } \mathtt{Verify}}_{\text{strict-PQ}}
\]

\section{P3Q Precompile Design}\label{sec:design}

\subsection{Address and registration}

P3Q lives at LP-4200 slot \texttt{0x012205}, pinned in
\texttt{precompile/p3q/contract.go} via
\texttt{ContractP3QVerifyAddress = common.HexToAddress("0x000\ldots012205")}.
The precompile is registered through the standard
\texttt{modules.RegisterModule} hook with \texttt{ConfigKey =
"p3qVerify"}.

\subsection{Wire format}\label{sec:wire}

The calldata layout is shown in Figure~\ref{fig:wire}.

\begin{figure}[h]
\centering
\begin{tabular}{ll}
\toprule
Offset & Field \\
\midrule
$0$ & \texttt{version} (1 byte) \\
$1$ & \texttt{proof\_len} (4 bytes, big-endian uint32) \\
$5$ & \texttt{proof} (\texttt{proof\_len} bytes, MUST begin with \texttt{"P3Q1"}) \\
$5+\texttt{proof\_len}$ & \texttt{pub\_len} (4 bytes, big-endian uint32) \\
$9+\texttt{proof\_len}$ & \texttt{public\_inputs} (\texttt{pub\_len} bytes) \\
\bottomrule
\end{tabular}
\caption{P3Q wire format. Minimum input length is
$1+4+4+4=13$ bytes (the proof field must contain at least the
4-byte magic header).}
\label{fig:wire}
\end{figure}

The version byte differentiates future wire-format versions; the
first deployment is $\texttt{VersionV1} = 0x01$. Inputs with any
other version byte are rejected with \texttt{ErrInvalidVersion}
BEFORE any backend dispatch.

The \texttt{proof} field MUST begin with the 4-byte
\texttt{MagicHeader = "P3Q1" = [0x50, 0x33, 0x51, 0x31]}. This is
a defense-in-depth pre-filter: a caller who omits the magic is
rejected at \texttt{contract.go:174} with \texttt{ErrInvalidProof}
without consulting the backend. The check is constant-time:
\texttt{jasmin/verify.jazz::ct\_check\_magic} XOR-accumulates a
difference word over the 4 magic bytes and branches only on the
accumulated value, never on individual byte mismatches.

\subsection{Gas model}\label{sec:gas}

The gas schedule is:
\[
\mathsf{RequiredGas}(\mathsf{input}) =
  \mathsf{BaseVerifyGas} + \mathsf{PerByteGas} \cdot |\mathsf{input}|
\]
with $\mathsf{BaseVerifyGas} = 200{,}000$ and
$\mathsf{PerByteGas} = 10$. The choice reflects that STARK verification
cost is dominated by FRI query rounds (logarithmic in circuit size)
while the per-byte term covers serialization, hashing, and FFI
marshaling overhead.

We prove three formal properties of the gas model:

\begin{theorem}[Gas monotonicity]\label{thm:gas-mono}
For any two calldata inputs $a$, $b$ with $|a| \le |b|$,
$\mathsf{RequiredGas}(a) \le \mathsf{RequiredGas}(b)$.
\end{theorem}

\begin{proof}
By definition $\mathsf{RequiredGas}$ is affine non-decreasing in
$|\mathsf{input}|$. Discharged at admit budget $0$ in
\texttt{P3Q\_Gas\_Model.ec::gas\_monotonic} and
\texttt{Crypto.Precompile.P3Q.gas\_monotonic} (Lean).
\end{proof}

\begin{theorem}[Gas charged upfront]\label{thm:gas-upfront}
If $\mathsf{supplied\_gas} < \mathsf{RequiredGas}(\mathsf{input})$,
\texttt{PrecompileRun.run} returns \texttt{RErr EOutOfGas 0} without
parsing the calldata or invoking the backend.
\end{theorem}

\begin{proof}
Discharged at admit budget $0$ in
\texttt{P3Q\_Verifier.ec::oog\_dominates}. The Go body checks the gas
condition before any other side-effecting operation
(\texttt{contract.go:141-144}).
\end{proof}

\begin{theorem}[No secret leak through gas]\label{thm:gas-noleak}
For inputs $a, b$ with $|a| = |b|$,
$\mathsf{RequiredGas}(a) = \mathsf{RequiredGas}(b)$.
\end{theorem}

\noindent
Theorem~\ref{thm:gas-noleak} is structurally trivial because P3Q has
no secret inputs at the precompile boundary; we state it nonetheless
because the gas trace is observable to other contracts on the same
chain, and a chain-level oracle that distinguishes accept-byte-count
from reject-byte-count would be a soundness concern for downstream
consensus logic.

\subsection{Backend dispatch and registration}

The backend verifier is registered once at node startup via
\texttt{RegisterVerifier(fn VerifierFn)}. The callback type is:

\begin{lstlisting}[language=Go]
type VerifierFn func(version byte, proof, pubInputs []byte)
    (ok bool, err error)
\end{lstlisting}

\noindent
\texttt{verifier} is an \texttt{atomic.Value}; the dispatch hot path
takes one atomic load per call and never locks. The deliberate
``one-and-one-way'' composition: a node has exactly one backend, set
once, and the EVM precompile layer never sees backend internals.

The Go-side error handling distinguishes three backend outcomes:
\begin{itemize}
\item $(\mathtt{ok}=\mathtt{true}, \mathtt{err}=\mathtt{nil})$: precompile returns
$(\emptyset, \mathsf{remaining}, \mathtt{nil})$ (accept).
\item $(\mathtt{ok}=\mathtt{false}, \mathtt{err}=\mathtt{nil})$: precompile returns
$(\emptyset, \mathsf{remaining}, \mathtt{ErrInvalidProof})$.
\item $(\_, \mathtt{err}\ne\mathtt{nil})$: precompile returns
$(\emptyset, \mathsf{remaining}, \mathtt{err})$ — the underlying err
is propagated for diagnostic purposes.
\end{itemize}

The EasyCrypt operational model collapses the third case into the
second (\texttt{P3Q\_Verifier.ec::PrecompileRun.run} returns
\texttt{RErr EInvalidProof} on \texttt{VFailed}); this is a
deliberate simplification for proof ergonomics that does not
weaken soundness — see Section~\ref{sec:security} for the
discussion.

\section{Verification Reduction}\label{sec:reduction}

The headline reduction P3Q makes available to consensus is:

\begin{theorem}[P3Q dispatches to backend]\label{thm:dispatch}
For any calldata input that parses to a triple $(v, \pi, x)$ with
$v = \mathtt{VersionV1}$, the precompile accepts iff
$\mathsf{backend\_verify}(v, \pi, x) = \mathtt{VOK}$.
\end{theorem}

\begin{proof}
Discharged at admit budget $0$ in
\texttt{P3Q\_Verifier.ec::accept\_iff\_backend\_accept} and its
companion lemma \texttt{reject\_iff\_backend\_reject}. The proof
sequence walks the four-step Run() body: gas check, parse, version
check, backend dispatch.
\end{proof}

The headline reduction makes the on-chain verification a single
function call at the precompile boundary. For the common case where
the proof payload carries a Pulsar / ML-DSA-65 signature, we get the
further reduction:

\begin{theorem}[FIPS~204 reduction]\label{thm:fips204}
When the backend implements the Pulsar profile, for any
$(v, \pi, x)$ with $v = \mathtt{VersionV1}$,
$\mathsf{backend\_verify}(v, \pi, x) = \mathtt{VOK}$ iff
$\mathtt{ML\text{-}DSA.Verify}(\mathsf{parse}(\pi), \mathsf{parse}(x))
= \mathtt{true}$.
\end{theorem}

Theorem~\ref{thm:fips204} is stated as the \texttt{backend\_reduces\_
to\_fips204} axiom in the Lean theory and as the hand-off axiom
\texttt{backend\_verifier\_axiom} in the EasyCrypt theory. It is
discharged externally by the audit of the Rust backend crate and by
the Pulsar EC theory's byte-equality theorem~\cite{pulsar}.

\section{STARK Extension}\label{sec:stark}

The Rust backend crate at \texttt{p3q/crates/p3q-verifier} provides
two profile-dispatched verification paths:
\begin{itemize}
\item \texttt{ProofSystemId::Sha3} — strict-PQ STARK over cSHAKE256
hashes (the canonical Lux profile).
\item \texttt{ProofSystemId::Keccak} — cross-ecosystem variant using
Keccak hashes (for compatibility with Ethereum's wider PQ
roadmap)~\cite{ethereum-stark}.
\end{itemize}

Both profiles share the same AIR / FRI structure: an algebraic
intermediate representation (AIR) with a low-degree-extended trace
polynomial, committed via a Merkle tree, queried via FRI
(Fast Reed-Solomon Interactive Oracle Proof of
Proximity)~\cite{fri-paper}. The verifier checks (i)~that the
out-of-domain quotient openings match the committed trace
polynomial via the AIR transition constraints, and (ii)~that the FRI
proof shows the trace polynomial is low-degree.

For the v0x01 wire format, the proof body lives entirely in
\texttt{proof} (the bytes following the magic header); the public
inputs (the AIR public-input column) live in \texttt{pub\_inputs}.
Soundness of the STARK verification is inherited from the FRI
soundness theorem~\cite{fri-paper} composed with the AIR
arithmetisation soundness for the specific circuit being proved.

\paragraph{Soundness argument (sketch).}
For circuit size $C$, FRI achieves soundness error $\le
(\text{rate})^{\rho} + \binom{q}{2}/|F|^k$ for $k$ queries at FRI
rate $\rho$, against a field of size $|F|$. The Goldilocks
field has $|F| = 2^{64} - 2^{32} + 1$ and the canonical Lux profile
uses $80$ queries at FRI rate $1/8$, giving soundness error
$\le 2^{-80} + 2^{-130}$ which is sub-$2^{-80}$ overall — comfortable
for consensus use under standard post-quantum security definitions.
The audited Rust crate carries the formal soundness parameters in
its crate-level documentation.

\section{Implementation}\label{sec:impl}

\subsection{Go precompile}

The Go body is intentionally minimal — 70 LOC of non-comment code in
\texttt{contract.go::Run}. The wire decode uses
\texttt{encoding/binary} \texttt{BigEndian.Uint32}; the magic
comparison is a Go string-equality (which compiles to a constant-time
byte loop under modern Go runtimes for the small 4-byte case). The
dispatch is a single function-pointer call obtained via one
\texttt{atomic.Value.Load()}.

\subsection{Rust backend}

The Rust backend at \texttt{p3q/crates/p3q-verifier} is panic-free by
contract (\texttt{\#![forbid(unsafe\_code)]} and
\texttt{\#![deny(missing\_docs)]} at the crate root). The dispatch
function takes a profile byte and remaining proof body and returns a
typed \texttt{P3qError} on any failure. Every error path is
exhaustive; there is no fall-through silent-accept path.

\subsection{Formal artifacts}

Four EasyCrypt files at admit budget $0/0$ live in
\texttt{precompile/p3q/proofs/easycrypt/}:
\begin{itemize}
\item \texttt{P3Q\_Verifier.ec} — operational model and the four
core theorems.
\item \texttt{P3Q\_Wire\_Format.ec} — round-trip + uniqueness +
truncation lemmas.
\item \texttt{P3Q\_Gas\_Model.ec} — six gas-model lemmas including
upfront-charge and no-secret-leak.
\item \texttt{lemmas/P3Q\_CT.ec} — constant-time obligation reduced
to the backend $\mathtt{backend\_ct}$ axiom.
\end{itemize}

The Lean bridge file \texttt{Crypto/Precompile/P3Q.lean} mirrors the
EC structure with five named axioms and nine theorems, and threads
the FIPS~204 reduction (Theorem~\ref{thm:fips204}) as a bridge to
\texttt{Crypto.Pulsar.Verify}.

The Jasmin source \texttt{precompile/p3q/jasmin/verify.jazz} carries
the constant-time annotation
\texttt{\#[ct = "public * public * public * public -> public"]}
and discharges the structural gate body. Static CT checking is via
\texttt{jasminc -checkCT verify.jazz}.

\section{Evaluation}\label{sec:eval}

\subsection{Gas cost}

Table~\ref{tab:gas} compares P3Q's gas cost to neighbouring EVM
precompiles for a 4096-byte calldata payload (typical STARK proof
size).

\begin{table}[h]
\centering
\caption{Gas cost comparison at \texttt{|input|} = 4096 bytes.}
\label{tab:gas}
\begin{tabular}{lrr}
\toprule
Precompile & Address & Gas at 4096 B \\
\midrule
ECRecover & \texttt{0x01} & 3{,}000 \\
BLS12-381 G1Mul & \texttt{0x0d} & 12{,}000 \\
ML-DSA & \texttt{0x012202} & 50{,}000 \\
Pulsar (Threshold) & \texttt{0x012204} & 75{,}000 \\
P3Q (this work) & \texttt{0x012205} & 240{,}960 \\
\bottomrule
\end{tabular}
\end{table}

P3Q is more expensive per call than the other PQ precompiles because
the STARK verifier is a heavier object than a single ML-DSA
\texttt{Verify}. Crucially though, P3Q can amortise many ML-DSA
verifications inside one STARK proof: a batched Pulsar certificate
covering $k$ threshold signatures fits in one P3Q call with
verification cost growing logarithmically in $k$. The break-even
point against $k$ direct ML-DSA precompile calls is $k \approx 5$,
making P3Q strictly cheaper for any non-trivial batch.

\subsection{Verification latency}

The Rust backend's FRI verifier dominates the latency budget; the Go
precompile body adds $< 1\mu s$ on top. Backend latency for the
canonical Pulsar-65 strict-PQ profile is $\sim 4$\,ms on an Apple
M1~Max single core, in line with~\cite{plonky3-bench}.

\subsection{Test surface}

The Go test surface (\texttt{contract\_test.go} +
\texttt{contract\_e2e\_test.go}) covers:
\begin{itemize}
\item Address pin, gas formula, six unit-level error / accept paths.
\item $64$ e2e round-trip dispatches with cross-validating backend.
\item Bad-magic, bad-version, bad-length, OOG short-circuit paths.
\item $256$ bit-flip fuzz iterations.
\item Length-field manipulation across $4$ extreme values.
\item Wrong-version sweep over all $255$ non-V1 version bytes.
\item Go-native \texttt{FuzzP3Q\_Dispatch} target.
\end{itemize}

\section{Security}\label{sec:security}

\subsection{Threat model}

P3Q's threat model is the standard EVM-precompile threat model with
two extensions:
\begin{enumerate}
\item \textbf{Quantum-capable adversary.} The verification body is
strict-PQ; soundness under a quantum adversary equals soundness of
the underlying STARK / FRI construction over the Goldilocks
prime field plus the cSHAKE256 hash assumption.
\item \textbf{Chain-level timing oracle.} An adversary submitting
arbitrary calldata to the precompile observes per-block latency. The
precompile MUST NOT leak information about backend acceptance through
gas cost or via timing of the structural pre-filter.
\end{enumerate}

\subsection{Constant-time obligations}

The CT discipline applies to two layers:
\begin{itemize}
\item \textbf{Structural gate.} \texttt{contract.go::Run} branches
only on calldata lengths and the PUBLIC version byte. The magic
header comparison is byte-string equality on PUBLIC wire bytes; the
Jasmin source uses XOR-accumulation to ensure the comparison itself
is content-independent.
\item \textbf{Backend.} The audited Rust crate carries its own
\texttt{\#[ct]} annotations on the FRI verifier inner loop. The
backend CT obligation is reduced in
\texttt{lemmas/P3Q\_CT.ec::precompile\_ct} to a section-local
\texttt{backend\_ct} axiom which is the porting target for
\texttt{jasminc -checkCT} on the Rust-side compiled FRI verifier.
\end{itemize}

\subsection{Gas side-channel}

By Theorem~\ref{thm:gas-noleak}, gas charged is a pure function of
\texttt{|input|}. Calldata length is public-by-EVM-precompile-ABI, so
gas billing leaks no information beyond what is already observable.
By the \texttt{uniform\_billing} lemma in \texttt{P3Q\_Gas\_Model.ec},
all non-OOG return paths charge the same gas; an observer cannot
distinguish accept, reject, malformed-input, or wrong-version
outcomes through the gas-remaining trace.

\subsection{Identifiable misverification}

The error sentinel set is small and disjoint:
\texttt{ErrInvalidInputLength}, \texttt{ErrInvalidVersion},
\texttt{ErrVerifierNotRegistered}, \texttt{ErrInvalidProof}. A caller
can disambiguate cause-of-failure for diagnostic purposes without
needing to inspect the backend. The granular surface enables on-
chain analytics (e.g., per-mode reject counters) without leaking
secret information.

\subsection{Reductive divergence: Go error propagation vs EC collapse}

The Go body propagates an arbitrary backend error directly to the
caller (\texttt{contract.go:184}); the EC operational model collapses
all backend failures into \texttt{EInvalidProof}. This is a
deliberate simplification on the proof side: every accept on the Go
side implies accept on the EC side, and every reject on the EC side
implies one of the Go reject paths, so soundness is preserved across
the divergence. The Go side prefers err-propagation for diagnostic
power; the EC side prefers err-collapse for proof ergonomics. The
sign-off (MIN-1) records this trade-off.

\section{Comparison to Neighbouring Precompiles}\label{sec:comparison}

Table~\ref{tab:cmp} contrasts P3Q with two neighbouring precompiles.

\begin{table}[h]
\centering
\caption{P3Q vs. neighbouring EVM precompiles.}
\label{tab:cmp}
\small
\begin{tabular}{p{2.5cm}p{3cm}p{3cm}p{3cm}}
\toprule
& ECRecover & BLS12-381 & P3Q \\
\midrule
Address & \texttt{0x01} & \texttt{0x0a..0x10} & \texttt{0x012205} \\
Curve / field & secp256k1 & BLS12-381 & Goldilocks STARK \\
Quantum-safe & no & no (ECDL) & yes (PQ STARK) \\
Wire format & fixed (160 B) & per-op fixed & length-prefixed \\
Backend & native Go & native Go (blst) & Rust via cgo \\
Gas (base) & $3{,}000$ & $12{,}000..70{,}000$ & $200{,}000$ \\
Gas (per-byte) & $0$ & $0$ & $10$ \\
Profile bytes & no & no & yes (version + magic) \\
Audit posture & long-stable & EIP-2537 audited & this work + backend audit \\
\bottomrule
\end{tabular}
\end{table}

P3Q occupies a distinct design point: it is the only LP-4200
precompile that delegates to a non-Go backend through a registered
function pointer. This delegation is the price of using a
heavyweight Rust STARK verifier; the EC operational model and the
Jasmin structural-gate body together make the cost manageable by
keeping the Go-Rust boundary thin and locally auditable.

\section{Conclusion and Roadmap}\label{sec:conclusion}

P3Q is a thin, well-shaped, formally-modelled EVM precompile for
strict-PQ verification at LP-4200 slot \texttt{0x012205}. The Go
precompile body is intentionally minimal, the structural pre-filter
is constant-time over wire calldata, and the gas model is monotonic
and upfront-charged. The full EC theory at admit budget $0/0$, the
Lean bridge with nine discharged theorems, the CT-annotated Jasmin
source, the dudect harness wired for $10^9$-sample submission runs,
and the exhaustive Go test surface together constitute a Tier~A
formal-artifact package suitable for an external audit.

\paragraph{Open gates.}
\begin{itemize}
\item \textbf{GATE-1.} Run EasyCrypt against the four P3Q EC files on
a host with \texttt{easycrypt} on PATH; confirm $0/0$ admit budget
compiles end-to-end.
\item \textbf{GATE-2.} Run \texttt{lake build Crypto.Precompile.P3Q}
against the Lean tree; confirm all nine theorems land.
\item \textbf{GATE-3.} Run the $10^9$-sample dudect submission run on
a pinned-CPU quiet host; produce per-batch t-statistic logs.
\item \textbf{GATE-4.} External audit of the Rust backend crate at
\texttt{p3q/crates/p3q-verifier}.
\end{itemize}

\paragraph{Future work.}
\begin{itemize}
\item Cross-ecosystem deployment: the
\texttt{ProofSystemId::Keccak} profile lets P3Q dispatch Ethereum-
compatible STARK proofs without adding a separate precompile slot.
\item Batched signature verification: a wire-format v0x02 extension
to support an array of $k$ signature certificates inside one STARK
proof, with verification cost growing logarithmically in $k$.
\item Recursive STARK composition: nesting P3Q proofs inside larger
STARK circuits (the \texttt{p3q/crates/p3q-recursion} crate).
\end{itemize}

\begin{thebibliography}{99}

\bibitem{p3q-verifier} Lux Industries, Inc.
\emph{p3q-verifier: Audit-gated Rust verifier crate for the strict-PQ
STARK proof backend.} \texttt{github.com/luxfi/p3q/crates/p3q-verifier},
2026.

\bibitem{pulsar} Z.~Kelling.
\emph{LP-073: Pulsar --- Module-LWE Rank-$k$ Threshold ML-DSA for
Permissionless Validator Sets.} Lux Industries, Inc., technical report
LP-073, 2026. \texttt{github.com/luxfi/pulsar}.

\bibitem{fri-paper} E.~Ben-Sasson, I.~Bentov, Y.~Horesh, M.~Riabzev.
\emph{Fast Reed-Solomon Interactive Oracle Proofs of Proximity.}
ECCC TR17-134, 2017.

\bibitem{plonky3-bench} The Plonky3 contributors.
\emph{Plonky3: A library for building efficient zero-knowledge
proofs.} \texttt{github.com/Plonky3/Plonky3}, 2024.

\bibitem{ethereum-stark}
J.~Drake, V.~Buterin, D.~Feist (eds.).
\emph{Post-quantum Ethereum roadmap notes: STARK precompiles and the
verification surface.} Ethereum Foundation Research, 2025.

\bibitem{fips204} NIST.
\emph{FIPS 204: Module-Lattice-Based Digital Signature Standard.}
August 2024.

\bibitem{eip-2929} V.~Buterin, M.~Swende.
\emph{EIP-2929: Gas cost increases for state access opcodes.}
Ethereum Improvement Proposal, 2020.

\bibitem{bgl} G.~Barthe, B.~Gr\'egoire, V.~Laporte.
\emph{Secure compilation of side-channel countermeasures: The case of
cryptographic constant-time.}
CSF 2018.

\bibitem{dudect} O.~Reparaz, J.~Balasch, I.~Verbauwhede.
\emph{Dude, is my code constant time?} DATE 2017.

\bibitem{libjade} Formosa Crypto project.
\emph{libjade: A formally verified library of cryptographic
algorithms.} \texttt{github.com/formosa-crypto/libjade}, 2024.

\end{thebibliography}

\end{document}