QuietOdds holds your money behind zero-knowledge proofs, so the rules inside those proofs have to be right. We proved the money rules in Lean, a proof assistant where a computer checks every step. Then we tested everything else. Every number on this page comes from the tools' own output.
A test tries one input, or a few thousand random ones. If a bug needs one exact number out of 2²⁵⁴, testing will almost never find it.
ZK circuits wrap around
Circuit math works modulo a huge prime p, like a clock. On a clock, 11 + 3 = 2. In a circuit, a "negative" number is just a very big one. That's how money gets created from nothing.
A proof covers every input
Lean checks each step of the argument down to its axioms, for all possible values at once. If it builds, the claim holds. No sampling, no luck.
What is proved
Four theorems, one per rule that would lose people money if it were wrong. Each one names the exact circuit or contract lines it models.
Theorem 1✓ proved
A private spend can't create money
Whatever goes into a spend comes out exactly: the note you spend equals the change you keep, plus what you bet, swap or withdraw, plus the relayer fee.
Rules out
A forged proof that spends a 1 USDC note but bets 1,000,000 USDC, by making the numbers wrap around the field.
How
The circuit's equation holds "modulo p", like a clock that wraps at 12. On its own, 1 = change + bet can be satisfied by a gigantic "negative" change. The four 128-bit range checks stop that, and the theorem proves they are enough: since 3 × 2¹²⁸ < p, the sum can never wrap, so the field equation is the ordinary equation.
When you claim a win or redeem a batch ticket, the payout is exactly ⌊stake × pot ÷ winning side⌋. Not a unit more. And the relayer fee can never exceed the payout.
Rules out
Claiming a payout slightly larger than your share, or a fee bigger than the payout so the leftover wraps into a huge note.
How
Circuits can't divide, so the prover supplies the answer and the circuit checks x·num = payout·den + remainder with 0 ≤ remainder < den. The theorem proves that with the 96-bit checks, this pins the payout to the one true floor division. The contract supplies num and den, never the user.
If every winner is paid their rounded-down share, the total paid out is at most the pot. Rounding dust is less than one unit per person, and it stays in the pool.
Rules out
Rounding errors that add up across many claims until the last winner, or the pool, comes up short.
How
Each payout is floored, and a sum of floors is at most the floor of the sum. Here it is with the real numbers from our Sepolia batch #1, where three people put in 1.2, 1.0 and 1.0 USDC and the batch got back 1,392,866,552,093,773 wei: payouts add up to …772. That is 1 wei of dust, kept by the pool. Lean checks that example too.
Models the pro-rata terms that Markets and BatchSwapper hand to ShieldedPool.redeem.
50theorem pro_rata_dust_lt_card {ι : Type*} (s : Finset ι) (x : ι → ℕ) (N D : ℕ)51 (hD : ∑ i ∈ s, x i = D) (hDpos : 0 < D) :52 N < ∑ i ∈ s, x i * N / D + s.card
Our Uniswap v4 hook charges the back half of a sandwich a fee as large as the price move it reverses. With that fee, buying first and selling right after in the same block can't make a profit.
Rules out
A bot buys just before your swap and sells just after, pocketing the price move your swap caused.
How
Cost of the front-run is at least q·P₀. Revenue from the back-run is at most q·(1−f)·P₂. With f ≥ (P₂−P₀)/P₀, revenue never beats cost. We also proved where it stops: the contract caps the fee at 50%, so if one block more than doubles the price, the guarantee fails. We proved that too, instead of hiding it.
205 function directionalFee(PoolKey calldata key, bool zeroForOne) public view returns (uint24) {206 Checkpoint storage cp = _checkpoints[key.toId()];207 if (cp.blockNumber != uint48(block.number)) return BASE_FEE; // first swap of the block208 uint256 start = cp.startSqrtPriceX96;209 (uint160 sqrtNow,,,) = poolManager.getSlot0(key.toId());210 uint256 cur = sqrtNow;211212 // zero-for-one pushes the price down, so it reverses an upward move, and vice versa.213 bool reverses = zeroForOne ? cur > start : cur < start;214 if (!reverses) return BASE_FEE;215216 // The move, relative to the lower of the two prices (the larger ratio).217 uint256 ratio = FullMath.mulDiv(FullMath.mulDiv(cur, 1e6, start), cur, start); // (cur/start)^2 in pips218 if (ratio == 0) return MAX_REVERSAL_FEE; // the price fell more than 1e6-fold219 uint256 move = ratio > 1e6 ? ratio - 1e6 : FullMath.mulDiv(1e6 - ratio, 1e6, ratio);220 uint256 fee = BASE_FEE + move;221 return fee > MAX_REVERSAL_FEE ? MAX_REVERSAL_FEE : uint24(fee);222 }
46theorem sandwich_unprofitable (q P₀ P₂ cost revenue f : ℝ)47 (hq : 0 ≤ q) (hP₀ : 0 < P₀) (hup : P₀ ≤ P₂)48 /- every unit of the front-run is bought at a price `≥ P₀` -/49 (hCost : q * P₀ ≤ cost)50 /- every unit of the back-run sells at a price `≤ P₂`, after the fee -/51 (hRev : revenue ≤ q * (1 - f) * P₂)52 (hFee : (P₂ - P₀) / P₀ ≤ f)53 /- `f ≤ 1` (kept to match the paper statement; the proof does not need it) -/54 (_hf1 : f ≤ 1) :55 revenue - cost ≤ 0
Where it stops.capped_fee_counterexample proves that with the 50% fee cap, a block that more than doubles the price lets a sandwich profit. Sandwiches spread over several blocks are also outside the model. We state these limits as theorems, not footnotes.
A proof is only as strong as what it assumes. Lean can list every axiom a theorem rests on, so an unfinished proof (sorry) or a made-up assumption can't hide. This is the real output of lake build:
lean/ · lake build
$ lake build
'QuietOdds.spend_conserves_value' depends on axioms: [propext, Quot.sound]
'QuietOdds.redeem_payout_exact' depends on axioms: [propext, Quot.sound]
'QuietOdds.redeem_fee_sound' depends on axioms: [propext, Classical.choice, Quot.sound]
'QuietOdds.pro_rata_conserves' depends on axioms: [propext, Classical.choice, Quot.sound]
'QuietOdds.pro_rata_dust_lt_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'QuietOdds.sandwich_unprofitable' depends on axioms: [propext, Classical.choice, Quot.sound]
'QuietOdds.sandwich_unprofitable_fee_rule' depends on axioms: [propext, Classical.choice, Quot.sound]
'QuietOdds.capped_fee_counterexample' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (9054 jobs).
propext Two statements that imply each other are equal.
Quot.sound Lean's rule for working with equivalence classes.
Classical.choice Ordinary classical logic, used by Mathlib.
These are Lean's three standard axioms, used by almost all of mathematics in Lean. No sorryAx, no custom axioms. Lean 4.35.0 with Mathlib.
What these proofs don't cover
A proof you can trust says exactly where it ends.
Constraints copied by hand
The circuit lines were transcribed into Lean by hand. Each hypothesis names the main.nr line it models, so you can check them side by side above. Nothing checks this mechanically.
Trusted toolchain
We trust the Noir compiler, Barretenberg, the generated Solidity verifier, and Poseidon's collision resistance. The proofs are about the arithmetic, not these tools.
Model, not bytecode
Theorems 3 and 4 model contract logic. Theorem 3 relies on three tested facts: stakes really sum to the total, each note redeems once, and the pot is really in the pool. Theorem 4 works over real numbers and leaves out integer rounding and price encoding.
Not audited
This is a hackathon build on Sepolia. Formally verified where it matters most, tested everywhere else, but not audited.
Tests, all of them
Proofs cover the arithmetic. Tests cover the rest: Merkle paths, nullifiers, the hook's deltas, batches, the resolver. The contract tests use real proofs generated by the circuits, plus fuzzing and invariants.
Noir circuits
36/36 passing
Valid spends and claims pass. Wrong side, bad Merkle path, inflated payout, wraparound and tampered notes all fail.
Property tests: random inputs, hundreds to thousands of runs each
✓batch never fills worse than oracle boundfuzz · 256 runs
✓sandwich never profits either directionfuzz · 1,000 runs
✓payouts never exceed potfuzz · 256 runs
✓plain swap is untouchedfuzz · 256 runs
✓sandwich never pays in one blockfuzz · 256 runs
✓shield on every swap shapefuzz · 1,000 runs
✓any tampered spend input rejectedfuzz · 256 runs
✓flipped proof byte rejectedfuzz · 256 runs
✓no junk proof acceptedinvariant · 32 runs
✓one leaf per depositinvariant · 32 runs
✓pool holds every depositinvariant · 32 runs
Check it yourself
Everything here is open source. One command reruns every suite and the Lean build, and rewrites the data this page shows.
terminal
# clone
git clone https://github.com/AshiqAhamed17/quietodds && cd quietodds && npm install
# the proofs (downloads prebuilt Mathlib, then checks every step)
cd lean && lake exe cache get && lake build && cd ..
# every suite + this page's data
npm run verify-report -w scripts
nargo 1.0.0-beta.25 · forge 1.7.1 · lean4:v4.35.0 · bun 1.3.14