zkFMI
日本語

Audit machinery

The property at the centre is that neither whether a request was made nor which market it was for may be told apart from outside, while a computing node's misbehaviour remains detectable. Every number here is generated from measurement JSON; none was typed by hand.

source: qomm/AUDIT.md · artifacts: audit_slots.json, transport.json, quote_proof.json, three_times.json, multi_asset.json, rounds.json, stages.json, rounds_by_channel.json, prep_split.json

A cover slot and a real slot leave the same trace

A secret is_real bit goes into the circuit and is never branched on. The shape of the circuit does not change; the bit decides only whether the makers' state moves.

roundssent per partywall clock, median
real slot28622.2045 MB1.6493 s
cover slot28622.2045 MB1.6390 s

Compiler statistics, runtime round count and bytes sent all agree. The 0.0103 s wall-clock gap is smaller than the 0.0852 s spread seen when the same condition is repeated. This is the trace of the MPC job; the path from a user to the nodes is measured separately below.

Three kinds of audit, and slashing by the nature of the fault

Correctness of the computation is a per-slot digest of the result; contradictory signatures are two receipts; failure to answer is a deadline and an absence. Without a rule that every node emits a receipt every slot whether or not there was a real request, "it did not answer" cannot be shown to a third party. Dropping an eligible maker is caught by fixing the set to a single digest in advance; no hash is computed inside the circuit.

fault injected (7 nodes, 6 slots, quorum 5)nodeslotslashed
equivocation211,000,000
forked state (the same double signature, counted again)21500,000
omitted makers32500,000
stale state43250,000
missing receipt5450,000

All detected, none missed, no honest node accused. A double signature is self-contained evidence that admits no excuse, so it is heaviest; a missing receipt happens to honest nodes too, so it is lightest. The weights are relative; the absolute bond follows from an estimate of what misbehaving could earn, which is a deployment decision.

From user to node: fixed cadence and relay hops

  • Fixed cadence. One message of the same length to each node every slot, whether or not there is an order. In a design that speaks only when it needs to, speaking is itself the announcement.
  • Additive secret sharing. Split into one share per node before leaving the device. A single share alone is uniform noise.
  • Relay hops. Each hop holds until the slot boundary and reshuffles. The first hop knows the sender's address; the second knows only the first.
hopssent per user per slotorigin-linking AUCone relay can recover an orderslot wall clock
12,121 B0.500false27.8 ms
22,121 B0.500false49.3 ms
32,121 B0.500false69.3 ms

A user who sent an order and one who did not send the same bytes. The batch a node sees is the same regardless of how active anyone was. Each hop is a real socket at about 4.4 ms; a single hop lets the relay see the user's IP, so two or more is recommended. If a relay colludes with its own node, that one share is linkable; recovering the order needs every node to collude.

Proving the computation was right

A sigma protocol's response is linear in the witness, so a quorum of nodes can assemble a proof an ordinary verifier accepts while no one of them holds the witness. A general-purpose SNARK has no such structure, which is why collaborative SNARKs run the whole prover inside MPC. The statement: applying the committed policy to the committed request yields key_i for each maker, and the disclosed winner is the minimum of those. Minimality and membership together say exactly that the returned price is the best.

makersproveverifywinner matches the cleartext minimum
462 ms19 mstrue
8124 ms36 mstrue
16247 ms71 mstrue

Linear in the number of makers. It fits a 60-second disclosure or a one-second RFS update; it does not fit under 200 ms. Six forgeries are tried and rejected: a winner swapped to a non-minimal maker, an expired maker that cannot win, a request nobody can fill answering "no quote", the winning maker switched off, minimality proofs swapped between makers, and minimality for a false winner (a value of −1 outside the range).

What is assembled jointly is one Pedersen opening: a scalar dealt to seven nodes and one sigma proof built from a quorum of them (4.8 ms at quorum 3, 20.2 ms at 7). The quote proof's range proofs do not share that linearity, because extracting bits needs the value, so the joint figures are a lower bound on a fully assembled proof. Below the threshold the assembled proof does not verify, and that is checked too.

The prover's shares are the circuit's shares. Until the circuit kept them, the shares reached the prover by a route of their own, and a proof about numbers that merely agree with a computation is not a proof about the computation. This was the largest thing the design asserted rather than showed. Each node now writes its share of the winner and the persistence layer reads them back; every subset of three agrees, two do not recover it, and one flipped bit is noticed. The binding page is the rest of that story.

The pricing rule as a language

A maker's rule must reference only permitted inputs, must not use a user's identity or address as a pricing input, and must have a bounded output range. These are static properties of a program, so they are a checker's job and not a proof's. The instructions are + − ×, comparison, and, and min max clamp signed. No division, no loop, no indexing, no attribute access. The grammar is written out rather than borrowed, so the subset is what the parser accepts and nothing else.

# the price rule a market maker registers, and nothing else
param ask_level[-2000,2000], spread[2,400], slope[0,16], invcoef[0,8], maxqty[1,1000]
param expiry[0,1000000], active[0,1], use_ref[1,1]
state inv[-4000,4000]
input qty[1,400], ref_mid[90000,110000], now[0,1000000]

ask      = use_ref * ref_mid + ask_level + slope * qty + invcoef * inv
bid      = use_ref * ref_mid + ask_level - spread - slope * qty + invcoef * inv
eligible = (qty <= maxqty) and (expiry > now) and (active == 1)

Non-crossing is an identity rather than a check: ask − bid = spread + 2·slope·qty ≥ 2, so a crossed quote cannot be written. Two forms are registered, anchored to a reference price or absolute for markets with no usable benchmark (a corporate bond has no continuous mid to be an offset from); the maker's use_ref bit chooses, and the checker refuses a rule that declares a value it does not price with.

What the checker derives, with no proof involved: the output intervals of ask, bid and eligible, the maximum degree in the secrets (2), and the bit width the circuit needs (19 for both forms). The same declaration yields both the circuit's width and the content of the audit. One walk of the same tree produces the value and the proof together: 3 bit proofs, 12 product proofs, 11 range proofs, 28.9 ms to build and 32.2 ms to verify on Ed25519. A test checks that adding a term to the rule adds the corresponding proof. State-update rules are written in the same language and audit in about 30 ms.

Hiding which market the request is for

Splitting the MPC job per market would let which job ran announce the market. So one circuit serves every market and selects the reference price while it stays secret: ref = Σ_a (asset == a) · REF_TABLE[a], a secret bit times a public constant, which costs no multiplication. The round count is 64 from 1 to 32 assets; only traffic grows, by about 0.04 MB per asset. Across eight assets probed, rounds and bytes are identical and the answers differ. When few makers serve an asset the answer is "no quote", which is itself a hint about how thin the market is; the circuit runs the same shape and returns a sentinel.

Three times: priced, proved, settleable

one-way delaypricedprovedsettleabletotalmeets an audited 1 s RFS slot
1 ms961 ms+248 ms+71 ms1,281 msfalse
15 ms4,328 ms+248 ms+71 ms4,647 msfalse

An audited request-for-stream does not make a one-second slot. Completing the proof and reaching a quorum of receipts neither depends on the delay nor shrinks with a closer deployment. The remedies are a lighter proof in the number of makers, or setting the update interval to what is measured.

Where the rounds go, and what moves them

Where the MPC rounds go, 16 makers 0 10 20 30 40 rounds added inputs, reference,|price arithmetic: 10 10 inputs, reference, price arithmetic + direction|selection: 1 1 + direction selection + eligibility|gates: 9 9 + eligibility gates + binary|tournament: 32 32 + binary tournament
The tournament is 62% of the depth and the eligibility layer 17%; the pricing arithmetic is effectively nothing. Only sequential depth of comparisons matters. Artifact: stages.json.

The opening channel, the comparison chain, is 49 rounds under both malicious and semi-honest Shamir. Dropping malicious security takes rounds out of everything else (64 to 56) and cuts bytes by 3.53×: the security model is paid in bandwidth and the latency is owed to depth either way. Making each maker's market public and moving the expiry gate to the registration audit cuts traffic 45% and moves rounds only from 70 to 69. Preprocessing on disk leaves an online phase that is 16% of party 0's bytes and 71% of the rounds, measured with a trusted dealer that no deployment can run, so it establishes the size of the online phase and not the cost of building it.

Requests per MPC job against time per quote 0 1,000 2,000 3,000 4,000 1 2 4 8 16 32 requests in one job, Q (log scale) ms per quote ms per quote at 15 ms one way: requests in one job, Q (log scale) 1, 3,425 ms per quote at 15 ms one way: requests in one job, Q (log scale) 2, 1,839 ms per quote at 15 ms one way: requests in one job, Q (log scale) 4, 1,007 ms per quote at 15 ms one way: requests in one job, Q (log scale) 8, 574 ms per quote at 15 ms one way: requests in one job, Q (log scale) 16, 377 ms per quote at 15 ms one way: requests in one job, Q (log scale) 32, 284 ms per quote at 15 ms one way
Rounds belong to the job, not the request: 69 rounds at Q=1, 5.5 per quote at Q=32. The job itself takes 9.1 s at Q=32, so one user's wait rises as throughput improves. Artifact: rounds.json.

Rounds are a property of the job, not the request. Sharing the same comparison layers across Q requests divides the rounds per quote by Q, which fits the fixed-cadence slot design exactly. This is throughput, not one user's wait: a user's wait is capped by the slot period, so Q is chosen to match the arrival rate.

What is measured, built, and out of scope

itemstate
emit computations and receipts on a fixed cadence; real and cover slots leave the same tracemeasured
hide which market a request is formeasured
fix the eligible-maker set; detect omission, double signing, stale state, selective stallingmeasured
check the computation with a proof every time; nodes jointly build one verifiable openingmeasured
restrict the form of a pricing rule and derive its audit; audit the state-update rulemeasured
register a digest of the approved circuit and refuse substitutionbuilt
identify a node that emitted an inconsistent partial valuebuilt
relays over a real network, multiple hopsmeasured
secrecy after a trade, where settlement reveals market and sizeout of scope here; zkPI and DeFMI