papers/morpheus/onepagers/lp-313-verifiable-inference.tex

\documentclass[10pt,a4paper]{article}
\usepackage{../shared/proposal}
\usepackage[utf8]{inputenc}\usepackage[T1]{fontenc}
\usepackage{amsmath,amssymb}\usepackage{listings}\usepackage{xcolor}
\input{../shared/lstlang}

\newcommand{\code}[1]{\texttt{\small #1}}
\setlength{\emergencystretch}{3em}

\begin{document}

\proposalhead{Verifiable Inference}{%
Settlement is a function of elapsed time alone. Which model answered is a field
in the provider's local config that no counterparty reads and no contract
records.}{LP-313}

\noindent\textbf{What the contract measures.}
Provider revenue is \code{pricePerSecond} times session duration
(\code{IBidStorage.sol:14}, \code{SessionRouter.sol:374}). Nothing in that
product refers to tokens produced, weights loaded, or the machine that answered.
The map from an on-chain \code{modelId} to the upstream that serves it is a
config field (\code{aiengine/ai\_engine.go:64}). So serving a 7B where a 70B was
advertised is not an attack on the protocol but a
configuration choice that keeps the whole cost difference and leaves no artifact.
Per-second pricing makes the incentive continuous and unmetered: adverse
selection in textbook form.

\vspace{0.35ex}
\noindent\textbf{Three questions that get merged.}
\emph{Is the box genuine?} You answer this, and answer it well: 5{,}439 lines
binding TDX \code{report\_data} to a TLS SPKI digest, with the NVIDIA
\code{eat\_nonce} compared in constant time. One caveat. \code{VerifyQuote}
(\code{verifier.go:565}) POSTs the quote to a third party's
\code{/api/quote-parse} and infers validity from the JSON it gets back, and the
measurement registry is fetched unsigned from a CDN mirror because the
upstream repository ``was removed'' (\code{artifacts\_registry.go:18}). The one
question you answer rests on a rented root of trust whose artifacts already 404. \emph{Did inference happen at all?} Nothing answers this. \emph{Are these
the advertised weights?} HideNSeek attempted it; last commit 2024-07-29,
\code{main.py} is zero bytes.

\vspace{0.35ex}
\noindent\textbf{Mechanism, cheapest layer first.}
\emph{Commit.} Add \code{bytes32 modelCommitment} to \code{Bid}: the hash of a
canonical manifest fixing weight digests, quantization, tokenizer and serving
config. One \code{SSTORE} per bid, none per request. A zero commitment stays
legal and pledges nothing, which honestly describes every bid today. It detects
nothing on its own; it makes substitution decidable, which is what the other two
layers need. \emph{Bind.} The 64
\code{report\_data} bytes are fully allocated, so change what the GPU nonce
\emph{is} rather than the layout:
$\texttt{gpuNonce} = \mathsf{SHA256}(\texttt{"mor-gpu-nonce-v1"} \| c \| \rho)$,
with fresh $\rho$ published beside the quote, so freshness holds, the CPU-GPU
check is untouched, and the Intel-signed quote now covers $c$. Per
response, the enclave's TLS key signs
$(\texttt{sessionId}, i, c, \mathsf{H}(x), \mathsf{H}(y))$ and the Merkle root of
those leaves rides in the close-out receipt. Without a TEE it degrades to a plain
\code{secp256k1} signature over the same statement, which is still adjudicable.
\emph{Probe.} Sample sessions with known-answer challenges, slash on
contradiction.

\vspace{0.35ex}
\noindent\textbf{Sizing the probe budget.}
Let $\gamma$ be what substitution saves as a fraction of epoch revenue, $\lambda$
the slashed fraction of stake, $\beta$ the chance one probe catches it. Expected penalty exceeds expected saving when
$m \ge \beta^{-1}\ln\!\big(\lambda/(\lambda-\gamma)\big)$ probes per provider per
epoch; at $\gamma = 0.9$, $\lambda = 1$, $\beta = 0.3$ that is eight. The bound
carries no traffic term: the duty cycle falls as $1/\text{volume}$, so the scheme
gets cheaper as the market grows. It also requires $\lambda > \gamma$: stake
smaller than the prize deters nothing at any probe rate. That is affordable
because the bond exists already:
\code{\_claimForProvider} clamps epoch earnings to
\code{provider.stake - provider.limitPeriodEarned} (\code{SessionRouter.sol:383}),
so revenue and stake are denominated the same way.

\begin{stake}{What Morpheus gets}
  \item A claim consumers can filter on, and a floor under price competition
        against providers who do not run what they advertise.
  \item \code{Provider.stake} becomes a bond rather than a withdrawal delay, and
        attestation starts contributing to the payment decision.
  \item A specification implementable without adopting Lux or Hanzo software.
\end{stake}

\begin{stake}{What we get, stated plainly}
  \item A market whose model claims are checkable, which is our precondition for
        routing production traffic into it.
  \item We contribute the manifest encoder, verifier reference and probe harness,
        plus ML-DSA precompiles for receipts that outlive \code{secp256k1}.
\end{stake}

\noindent\textbf{First step, and who takes it.}
Whoever owns the \code{Marketplace} facet opens a PR adding
\code{modelCommitment} to \code{Bid} and \code{postModelBid}, emitted in
\code{MarketplaceBidPosted} (\code{IMarketplace.sol:8}). A facet replacement is
what EIP-2535 is for: one 5-of-9 Safe transaction, no change to settlement
arithmetic, no open session at risk. Nobody has to verify anything on day one;
consumers can filter from the first event.

\vspace{0.35ex}
\noindent\textbf{What this does not solve.}
None of it proves the arithmetic was right. An enclave that loads the pledged
weights and then truncates the attention window still produces a valid receipt,
and proving inference in zero knowledge is out of reach at these model sizes.

\vspace{0.6ex}
\noindent{\color{muted}\footnotesize\sffamily
LP-313, full paper available. Every citation checked against the working tree.
\quad\textbullet\quad \texttt{[email protected]}}

\end{document}