gradiente.ai

Author

Omar U. Espejel Starknet Foundation

Former machine learning engineer at Hugging Face; now working on crypto and AI at Starknet Foundation.

Published

· 17 min

Updated

TL;DR

  • A Mixture-of-Experts layer stores many feed-forward networks, scores all of them, and activates only a few for each token.
  • That saves ordinary inference work, but it creates a proof problem: a server must not be allowed to invent the route that is cheapest or most convenient to prove.
  • SparseProve binds one chain: input, all router scores, canonical top-k route, registered expert weights, selected nonlinear computation, and output.
  • The paper's structural result concerns checked expert-apply invocations. Fixed receipt work, routing work, nonlinear traces, and the proof backend still have real costs.
  • The current receipt covers a production-shaped MoE feed-forward block, not attention or a complete language model.

This essay starts where Why Transformer Decode Is a Natural STARK Trace ends. That primer explains why token-by-token inference can be written as a checked execution trace. Here, the question becomes narrower: what happens when the model itself chooses which part of that trace should execute?

Suppose a language model is processing the word bank.

In one sentence, bank means a place that holds money.

In another, it means the side of a river.

A normal transformer sends both token states through the same feed-forward network. A Mixture-of-Experts layer has another option: it can keep several feed-forward networks and choose a small subset for each token.

That choice is useful because the model can store more capacity than it activates at once.

It is also a trust problem.

If a remote server says, “I chose experts E2 and E4,” how do we know those are the experts its router actually chose? And if the server provides a cryptographic proof, how do we know the proof connects the router’s decision to the exact expert weights and output?

This essay builds that chain one picture at a time.

The recurring toy layer has:

  • eight routed experts, E0 through E7;
  • a router that selects two;
  • one always-on shared feed-forward network;
  • and one public tie rule.

The fixed scores select E2 and E4. Keep an eye on E6: it ties with E4 at the selection boundary, so the tie rule matters.

The short version

Sparse computation is easy if you trust the route. SparseProve is about proving the route and the selected computation as one receipt.

First, one feed-forward path

A transformer layer has two large parts:

  1. attention, which moves information between token positions;
  2. a feed-forward network, which transforms each token state.

This essay focuses on the second part.

A feed-forward network, or FFN, takes a vector of numbers and returns another vector. The vector is the model’s internal representation of the token at this point in the network.

In a normal dense layer, every token uses the same FFN weights.

A dense feed-forward layer compared with a mixture-of-experts layer The dense layer sends every token through one feed-forward network. The mixture-of-experts layer first uses a router to choose from eight routed expert networks. Start with the feed-forward part of a transformer layer The attention block is outside this picture. We are changing only the feed-forward path. normal feed-forward layer token state x one FFN same weights for every token one available path, one applied path mixture-of-experts layer token x router chooses paths E0E1 E2E3 E4E5 E6E7 many available paths, a few applied paths An expert is a feed-forward network, not a person or an agent.
One layer, two designs A normal transformer layer has one feed-forward path. An MoE layer keeps several possible paths and adds a router that chooses among them.

The word expert can make the next design sound more mysterious than it is.

An expert is an FFN with its own weights. It is not a person, an agent, or a separate model that talks to the other experts. The layer simply has several candidate FFNs where a dense layer had one.

The architecture now needs a rule for choosing a path.

That rule is the router.

Then, many possible paths

For each token state, the router produces one score for every routed expert.

A higher score means the router prefers that expert for this token. If the policy is top-2, the two winning scores define the routed path.

Some MoE designs also include shared computation. In the DeepSeekMoE-style architecture used by SparseProve, this is one widened shared feed-forward network that runs for every token. It is not another router candidate.

The routed experts provide conditional capacity.

The shared network provides an always-on path.

Together they produce the MoE block’s output.

This design appears in models because it separates two quantities that are identical in a dense FFN:

  • installed capacity: all the expert weights stored in the layer;
  • activated computation: the expert weights used for this token.

The model can increase the first without increasing the second at the same rate.

That is the basic promise of MoE.

Follow one token through the router

Here are the eight scores we will use throughout the essay.

E2 has the highest score, 0.91.

E4 and E6 both have 0.78.

The public policy says:

Select two experts. If two scores are equal at the boundary, choose the smaller expert index.

So E2 gets the first slot. E4 gets the second because 4 < 6.

A router scores eight experts and selects E2 and E4 All eight router scores are shown. E2 has score 0.91. E4 and E6 tie at 0.78, and the smaller-index policy selects E4. E2, E4, and the shared network feed the output. One token, eight scores, two routed experts We will keep these labels, scores, and colors for the rest of the essay. router score for every routed expert E00.14 E10.37 E20.91 E30.22 E40.78 E50.08 E60.78 E70.31 E4 wins the 0.78 tie because 4 < 6 paths applied for this token E2 highest router score E4 canonical boundary tie winner shared FFN always runs weighted output Public policy: top-2, break equal scores by the smaller expert index.
The recurring example The router scores all eight experts. Top-2 selects E2, then E4 wins the boundary tie with E6 because the public policy prefers the smaller index. The shared network always runs.

Why show all eight scores instead of only the winners?

Because “E2 and E4 have good scores” is not the same claim as “E2 and E4 are the canonical top-2.”

The second claim compares the winners with every other candidate.

It also needs a numeric interpretation. A proof system works with field elements, where arithmetic wraps around a large modulus. The router policy works with bounded integers, where -1 must remain negative and 10 must remain greater than 9.

SparseProve therefore binds the score range and comparison policy. Otherwise a value that wraps in the field could pretend to satisfy an integer comparison.

The route is not just two labels. It is the result of:

  • all expert scores;
  • a selected count;
  • an integer range;
  • and a deterministic tie policy.
Canonical top-k resolves a tie at the selection boundary E2 is first with score 0.91. E4 and E6 tie at 0.78 for the second slot. The public smallest-index rule selects E4, making the route unique. Top-2 is ambiguous until the tie rule is public The second slot has two equal candidates. Canonical routing turns the set into one verifier-derived answer. selection boundary E2 = 0.91 slot 1 E4 = 0.78 candidate for slot 2 E6 = 0.78 candidate for slot 2 public rule: if scores tie, choose the smaller index E4 and E6 have the same score. Since 4 < 6, E4 owns slot 2. unique canonical route [E2, E4] A receipt also range-binds the integer scores, so field wraparound cannot fake the comparisons.
Canonical ties The policy is part of the verified statement. Equal scores do not give the prover freedom to choose whichever branch is convenient.

This canonical rule is small, but it closes an important degree of freedom.

Without it, E4 and E6 are both valid second choices. The prover could choose whichever branch makes a later claim easier.

With it, the verifier derives one answer: [E2, E4].

What sparse means here

The layer stores eight routed FFNs.

This token activates two of them.

That is conditional sparsity: most available expert paths are inactive for this particular input.

The shared network still runs, so the activated path contains three feed-forward computations in our toy layer:

  • E2;
  • E4;
  • the shared FFN.
Eight installed experts compared with two activated experts and one shared network E2 and E4 are highlighted among eight installed routed experts. One always-on shared feed-forward network is also active. A materialize-all path would apply all eight routed experts and the shared network. Sparsity separates model capacity from work on this token Eight routed networks are installed. Only the selected route is activated. installed routed experts E0E1 E2E3 E4E5 E6E7 idleidle activeidle activeidle tie losesidle combine routed outputs E2 + E4, using route weights shared feed-forward network one always-on widened path activated route 2 routed + 1 shared the expert paths this token actually uses materialize-all comparison 8 routed + 1 shared a baseline that applies every available path This is a computation count, not yet a whole-proof speedup.
Installed is not activated The layer stores eight routed experts but applies only E2 and E4 for this token, plus the shared network. This is the conditional computation a receipt must justify.

This picture does not say the whole proof costs one third as much.

The router still scores all eight experts. The proof still has commitments, openings, transcript challenges, and backend work. The nonlinear expert block also contains more than one matrix multiplication.

The narrower point is the one MoE was designed to create:

applying the routed experts can follow the selected route instead of materializing every routed expert.

That distinction grows as a model installs more experts while keeping top-k small.

It disappears on a dense model.

The server must not choose its own proof path

Why ask for a receipt at all?

If the model runs on your own machine, you can inspect the code and recompute the layer. If it runs on someone else’s accelerator, you usually receive only an answer.

Re-running a large model defeats the purpose of outsourcing it.

A cryptographic proof offers another boundary. The server constructs evidence from the detailed computation. A much smaller verifier checks that evidence against a public statement.

The public statement is the contract between them. It says which model block, input, policy, and output the proof is about.

But a smaller verifier creates a design obligation: every important object must actually connect to that statement. Hashing a label outside the proof does not create that connection.

Now imagine a dishonest server.

It receives the same token state and has the same model. But instead of proving the route implied by all router scores, it asserts a different pair.

It might omit a high-scoring expert.

It might exploit an unspecified tie.

It might use the right labels but substitute different weights.

It could still compute a perfectly consistent output for that false path. A proof of only the selected matrix arithmetic would accept the wrong question.

A dishonest server claims a route that does not match the router scores The honest route selects E2 and E4. A dishonest route omits E2 and claims E4 and E6. A receipt must bind all router scores to the canonical route and reject the substitution. An output can be consistent with the wrong route Checking only the selected experts is not enough. The receipt must prove why those experts were selected. route implied by the scores all scores E2 .91 | E4 .78 | E6 .78 | ... E2 highest score E4 tie policy winner accepted route: [E2, E4] route asserted by a dishonest server claimed story omit the highest-scoring E2 path E4 still plausible alone E6 wrong canonical tie choice claimed route: [E4, E6] The verifier must derive the route from the complete bound score vector.
The trust problem A proof of expert arithmetic does not prove the route. SparseProve binds the complete score vector, the public tie policy, the derived route, and the selected computation.

This is the central mistake to avoid:

“The server correctly evaluated E4 and E6” does not imply “the model chose E4 and E6.”

The first is an arithmetic claim.

The second is a selection claim over all candidates.

A useful MoE receipt needs both.

SparseProve uses Rank-and-Route for this selection boundary. At a high level, the proof classifies every score as:

  • above the threshold;
  • equal to the threshold;
  • or below the threshold.

It counts how many are above and how many equal the threshold. A prefix count then chooses exactly the first required tied indices.

In our example:

  • E2 is above the boundary;
  • E4 and E6 equal the boundary;
  • one tied expert is still needed;
  • E4 appears first.

The verifier checks those facts under the public integer range. The server does not get to send an unexamined list of expert IDs.

There is a second router output: the route weights.

The selected experts are not always added equally. SparseProve derives fixed-point Q0.15 weights from a softmax denominator over the full public score vector, then keeps the entries for E2 and E4.

That full denominator matters. Looking only at selected scores could make their weights seem valid even when another hidden score should have changed the probability distribution. The verifier therefore derives the selected set and its selected weights from the same complete router output.

One receipt must bind the whole chain

A cryptographic proof does not automatically explain what it means.

The verified statement has to name the objects being connected:

  • the input;
  • the numeric policy;
  • the router relation and all scores;
  • the canonical route;
  • the selected route weights;
  • the registered expert matrices;
  • the selected and shared nonlinear computation;
  • and the output.

SparseProve treats those handoffs as one receipt boundary.

The complete SparseProve receipt chain for one mixture-of-experts layer The public input and registered model produce all router scores. A public top-2 and tie policy derives E2 and E4. Registered selected weights drive gate, up, activation, product, and down equations. Route weights and a shared feed-forward path combine into a requantized output. The receipt binds every handoff. The receipt is a chain, not a sticker on the final output Every arrow is an obligation. If one handoff is not bound, the prover can switch stories in the middle. VERIFIED STATEMENT input token state x and numeric policy router relation all eight raw scores canonical route top-2 gives E2, E4 route weights Q0.15, verifier-derived registered E2 weights gate, up, down matrices authenticated against registry registered E4 weights gate, up, down matrices authenticated against registry shared FFN weights one widened network always in the relation selected and shared SwiGLU equations + bounded output accumulation gate -> SiLU lookup -> multiply by up -> down -> route-weighted sum -> requantize verified MoE-layer output y
The whole receipt SparseProve checks the route and the computation selected by that route as one statement. Separate public policy and registry fields prevent a model digest from silently standing in for data it does not bind.

The word receipt is useful because it is narrower than “the AI was correct.”

Think of an ordinary receipt. It connects a store, a list of items, prices, and a total. It does not prove the products were good or that buying them was wise.

A SparseProve receipt connects a model block, input, route, selected computation, and output. It does not prove that the language model is truthful or safe.

It also does not rely on one final hash to carry the whole meaning.

A hash can make a byte string tamper-evident. It cannot, by itself, prove that a score came from a matrix multiplication or that E4’s label corresponds to a particular matrix.

Those are algebraic and authentication checks:

  • the router relation connects input and router weights to every score;
  • Rank-and-Route connects every score to one canonical selected set;
  • the registry connects selected expert IDs to selected matrices;
  • the nonlinear trace connects those matrices to expert outputs;
  • the bounded accumulation connects those outputs to y.

The chain is useful because each link has one job.

There are two different kinds of binding inside this chain.

First, the route must match the complete router output and tie policy.

Second, the expert labels must match the matrices registered for this model.

The second condition prevents another substitution:

call a cheap or altered matrix “E4,” prove arithmetic with it, and attach the real E4 label afterward.

Selected expert weights must match a registered model commitment On the accepted side, E2 and E4 weight leaves authenticate to the registered expert root. On the rejected side, a substituted E4-prime leaf produces a different root. Separate policy and lookup-table identities remain separate fields. The right route with the wrong weights is still the wrong computation Authentication connects expert identity to the matrices used inside the proof. registered selected weights E2 matrices gate | up | down E4 matrices gate | up | down expert registry root matches public statement substituted expert weights E2 matrices registered leaf E4' matrices unregistered substitute different root receipt rejects Kept separate in the statement expert registry | numeric policy | SiLU table identity | proof configuration
Registered weights The route names E2 and E4; the registry proves which gate, up, and down matrices those names mean. Other policy objects keep their own identities instead of hiding under one vague model label.

The figure deliberately keeps several identities separate.

An expert registry root binds expert matrices.

The numeric policy binds scales, ranges, and requantization.

The SiLU table has its own identity.

The proof configuration has its own verifier checks.

A single field called model should not be assumed to bind all of those objects unless the verified statement explicitly makes that connection.

What runs inside E2 and E4

We can now look inside one selected expert.

SparseProve’s production-shaped block follows the SwiGLU pattern used by modern MoE models. The input travels down two parallel paths:

  1. a gate projection;
  2. an up projection.

The gate result passes through the SiLU activation. That activated value multiplies the up result. A down projection maps the product back to the transformer’s hidden dimension.

The nonlinear SwiGLU computation inside selected expert E2 The token state enters gate and up projections in parallel. The gate result is requantized and looked up in a SiLU table. It multiplies the requantized up result, then passes through a down projection to produce expert output z. Route weighting happens after the expert output. Inside selected expert E2 An expert is not one matrix multiplication. SparseProve checks the nonlinear feed-forward block. token x gate projection x W_gate,E2 up projection x W_up,E2 SiLU lookup table[R_gate(...)] x multiply down projection h W_down,E2 expert output z_E2 Bounded integer policy at every conversion requantize gate | requantize up | requantize product | range-check accumulators The route weight is applied to z_E2 later, when the selected expert outputs are combined.
Selected expert E2 Gate and up projections remain separate until after the activation. Only the down projection is linear enough to group across tokens.

The letters in the figure correspond to four integer relations:

gate = requantize(x * W_gate)
up   = requantize(x * W_up)
hidden = requantize(SiLU(gate) * up)
z    = hidden * W_down

The route weight is applied to z later, when selected routed outputs and the shared output are accumulated.

This ordering matters for batching.

Gate, activation, and product are nonlinear. They remain defined for each selected token-expert edge.

The down projection is linear. Across several tokens, selected work for the same expert can be combined before applying that expert’s down matrix. The paper calls this grouped expert application.

Grouping does not make the nonlinear witness disappear. It amortizes the linear suffix when tokens touch overlapping experts.

Imagine four tokens all select E2.

An independent path restricts E2’s down matrix once for every token. The grouped path first combines the four token-side hidden vectors using transcript coefficients, then restricts E2’s down matrix once for that combined vector.

If those tokens touch E2, E4, and E7 in total, the grouped suffix follows three unique routed experts rather than all token-expert pairs.

How much this helps depends on route occupancy. Concentrated routes reuse more down matrices. Dispersed routes touch more unique experts. That is why the paper treats the observed number of unique experts as evidence instead of assuming every trained router behaves like uniform random selection.

The SiLU step needs one more explanation.

A proof system does not conveniently evaluate an arbitrary floating-point curve. SparseProve uses a fixed table over a bounded signed input range. The proof checks that each gate input is in that range and that its output appears in the verifier-pinned table.

A pinned lookup table proves the SiLU activation over a bounded input range A signed gate value within the public range selects one row from a verifier-pinned SiLU table. The table identity and valid input range are part of the policy. Inputs outside the range and a substituted table are rejected. Nonlinear arithmetic becomes a small, named table check The verifier binds both the allowed input range and the identity of the SiLU table. requantized gate g = -3 inside signed-i12 range verifier-pinned SiLU table input output -5table[-5] -4table[-4] -3table[-3] -2table[-2] ...... checked activation SiLU(-3) fixed-point value rejected input outside the signed-i12 domain rejected same input with a substituted table identity
Pinned nonlinearity A lookup makes the nonlinear function finite and explicit. The table is useful only when its domain, scaling, and identity are verifier-bound.

The table is part of the meaning of the computation.

Changing the scale changes the numbers.

Changing the valid input range changes which activations are admitted.

Changing the table changes the function.

That is why “we used a lookup” is not enough. The receipt needs the table identity and numeric policy that make the lookup meaningful.

Lock the evidence before compressing it

Our toy token has two routed slots: E2 and E4.

A batch has many such slot-output vectors. Checking every connection separately would repeat verifier and transcript plumbing.

SparseProve compresses these claims with random linear combinations.

The order is the important part:

  1. the prover commits the slot-output columns;
  2. the transcript draws an unpredictable challenge;
  3. the proof combines the committed slots using powers of that challenge;
  4. the combined value must agree with the grouped down-projection claims and output accumulation.
Commit first, sample a challenge, then compress selected expert slots The prover commits the E2 and E4 slot-output columns before seeing random challenge rho. The challenge assigns unpredictable coefficients one and rho to the slots. A compressed claim links both committed slot vectors to the grouped down projection and final output. Choosing rho before commitment would let a dishonest prover cancel errors. Random compression is sound only in the right order The prover must lock the slot outputs before learning the coefficient used to combine them. 1. COMMIT slot 0: E2 outputs z[t, E2] for the batch slot 1: E4 outputs z[t, E4] for the batch commitment root C_slots 2. CHALLENGE transcript draws rho 3. COMPRESS + CHECK one random linear combination z_E2 + rho * z_E4 also batched across tokens must match grouped down claims and the output accumulation Why not challenge first? If rho were known before C_slots, a dishonest prover could choose two wrong slot vectors whose weighted errors cancel. Commitment removes that freedom before the random check is defined. This compresses verification claims. It does not erase the work needed to construct the selected nonlinear traces.
Commit, then challenge SparseProve uses post-commitment random linear combinations to connect selected expert slots, grouped linear work, and output columns without letting the prover tailor errors to the challenge.

Why does randomness help?

Suppose two slot vectors are wrong in different places. If the prover knew the combining coefficient in advance, it could choose the two errors so they cancel.

But the commitment comes first.

Once the vectors are locked, a fresh random coefficient is very unlikely to hide a nonzero disagreement. The paper counts this probability together with its other receipt-specific error terms.

This technique compresses checks.

It does not mean the prover performs no work for the selected experts. The nonlinear traces still have to be constructed and constrained.

Read the paper’s cost figure carefully

We can finally ask what work follows installed capacity and what work follows the activated route.

The paper makes a finite statement about its linear expert-apply primitive:

  • SparseProve invokes it for the selected routed experts and shared paths: k + s;
  • a materialize-all baseline invokes the same primitive for every routed and shared path: E + s.

For our toy layer, that is 3 invocations instead of 9.

SparseProve separates fixed receipt work, routing work, and selected expert-apply work A three-band cost picture shows fixed receipt work, routing work over all eight installed experts, and expert-apply invocations. SparseProve invokes the checked expert-apply primitive for E2, E4, and the shared network, three paths total. A materialize-all baseline invokes it for all eight routed experts and the shared network, nine paths total. This is an apply-count ratio, not a wall-clock speedup. Which proof work follows capacity, and which follows the route? The paper separates three costs so a structural count is not mistaken for an end-to-end benchmark. fixed receipt and model work statement binding | commitments | openings | FRI | proof-of-work | serialization | model-sized preprocessing in the current receipt routing work sees installed capacity E score every expert | range-bound scores | classify around the threshold | count and resolve the canonical top-k route checked expert-apply invocations in the linear core SparseProve route E2 E4 shared k + s = 2 + 1 = 3 materialize-all baseline E0E1E2E3 E4E5E6E7 + shared path E + s = 8 + 1 = 9 9 / 3 is an apply-only invocation ratio. Fixed, routing, nonlinear, and backend costs remain.
The paper's cost figure, unpacked The honest claim is finite and structural: this prover calls the checked linear expert-apply primitive for the activated route. It is not a theorem that the complete proof is three times faster.

This is intentionally not presented as “SparseProve is 3x faster.”

It is an apply-only invocation ratio against one explicit baseline.

The complete receipt also pays for:

  • fixed proof-backend work;
  • router projection and scores;
  • canonical routing;
  • nonlinear selected traces;
  • model and registry binding;
  • commitments and openings;
  • and serialization.

Some execution-following proof systems may already avoid applying inactive experts. Against those systems, the novelty is not “we discovered sparse execution.” It is the combination of sparse execution with a verifier-bound route.

That is the scientific question behind the benchmark work:

As installed capacity grows, does complete proof cost stay governed mainly by the conditional computation that actually executes?

The paper measures that question separately from the structural theorem. Keeping those lanes separate makes both results easier to trust.

What the current receipt means

SparseProve does not yet prove a complete language-model inference.

It proves a production-shaped MoE feed-forward block: router through selected and shared nonlinear expert output.

Attention, embeddings, sampling, and the rest of the model remain outside this receipt.

The current construction is publicly verifiable rather than zero knowledge. Its prover and verifier run end to end, but the paper does not claim concrete end-to-end security bits: the complete extraction, Circle-FRI, Fiat-Shamir, and grinding composition remains conditional.

What the current SparseProve receipt proves and does not prove The proved column lists the input-to-router relation, all router outputs, canonical top-2 route, registered selected and shared weights, selected and shared SwiGLU equations, and bounded MoE-layer output. The not-proved column lists attention and embeddings, full-model inference, model quality or factual truth, server freshness, physical non-execution of inactive experts, and a general system performance victory. Read the receipt at its actual boundary A narrow, explicit guarantee is more useful than a broad label such as "verified AI." the current receipt proves the bound input produces the raw router outputs under the public numeric policy all scores derive one canonical top-2 route including the E4 versus E6 tie E2, E4, and shared matrices are registered against the expert registry commitment selected and shared SwiGLU equations hold with pinned lookup and range policy route weights come from the full score vector rather than prover advice the bounded accumulation yields output y for this production-shaped MoE block it does not prove attention, embeddings, or a complete model this is one MoE feed-forward block that inactive experts were never run elsewhere only that their apply relations are not required here that the model is accurate, safe, or factual computation integrity is not model quality freshness for a unique user request applications must bind their own request context a full-model or end-to-end speedup theorem fixed and backend work still matters unconditional security for every configuration the paper states receipt-specific assumptions Verified claim: this input, this policy, this registered MoE block, this output.
Scope is part of soundness SparseProve is a receipt for conditional computation inside one MoE block. It is not a certificate for the model's truthfulness, a full transformer proof, or proof that no other computation occurred.

That boundary is a limitation, but it is also the point of the experiment.

The research isolates conditional computation and asks whether a proof can preserve its economics without trusting the condition.

The current answer is:

The route can be derived canonically from all router scores, bound to registered selected weights, and connected to the selected nonlinear computation and bounded output in one circle-STARK-based receipt.

A STARK is the proof system under this receipt. It lets a verifier check algebraic constraints over committed execution data without re-running the full witness computation. The implementation uses Stwo, a prover built around Mersenne-31 arithmetic and circle-domain commitments.

The longer-term goal is not simply “make a proof sparse.”

It is more precise:

make proof cost follow executed conditional computation while the condition itself remains inside the verified statement.

That principle applies beyond MoE.

Any system that chooses a small path from a large installed capacity faces the same question: who proves the choice?

For MoE, the answer begins with the chain we followed here:

all scores -> canonical route -> registered weights -> selected computation -> output.

That is what makes sparsity proof-carrying.

Next: open the receipt

Part 2 follows the same token through the proof itself: what gets committed, when the verifier draws challenges, what gets opened, and what the final receipt does and does not certify.