antumbra-lez

Integer-only constant-product bonding curve math for the Logos Execution Zone, written for λPrize RFP-015.

cargo test --release

50 tests green. The pricing library has no dependencies at all — the executor harness is a separate workspace — and #![forbid(unsafe_code)] throughout.

What this found

RFP-015's reference implementation says the invariant is k = Vt × Vc, computed and stored at creation. For any realistic 18-decimal token pair that number does not exist in a u128:

Vt = 1e9 tokens x 1e18 = 1e27
Vc = 1e6 tokens x 1e18 = 1e24
k  = 1e51                        u128::MAX = 3.4e38

So k cannot be stored as written, and every pricing call that divides by it needs a 256-bit intermediate. k_does_not_fit_in_u128_for_an_eighteen_decimal_pair asserts the overflow and then prices the pair anyway.

The fix is not a bigger field. k is never materialised. Each formula folds into one mul_div whose product is taken in 256 bits and whose quotient is proven to fit in 128:

buy      tokens_out = Vt - k/(Vc + C_in)  = Vt - mul_div(Vt, Vc, Vc + C_in)
inverse  C_in       = k/(Vt - Q) - Vc     = mul_div(Vt, Vc, Vt - Q) - Vc
sell     C_out      = Vc - k/(Vt + t_in)  = Vc - mul_div(Vc, Vt, Vt + t_in)

The identity is exact, so folding changes nothing about the invariant and removes the overflow.

Rounding is solvency

Every rounding decision favours the pool:

operation	quantity	direction	who keeps the dust
buy	tokens_out	down	the pool
inverse	C_in	up	the buyer pays it
sell	C_out	down	the pool

A quotient that rounds the other way is not a rounding bug, it is a withdrawal: it lets a trader extract value the invariant never created. a_buy_then_an_immediate_sell_never_profits is the property that closes the dust-loop drain.

The reference is a different language

tests/vectors/mul_div.txt is generated by tests/gen_vectors.py from Python's arbitrary-precision integers. A differential test whose reference shares the implementation's assumptions proves only that the implementation agrees with itself.

4,000 vectors, deliberately biased towards the hard cases — huge products, small divisors, and divisors sitting right at the 128-bit boundary. Half of them are cases where the exact quotient does not fit in 128 bits, and the implementation must refuse those by name rather than return a truncated number.

What the differential test caught

The first version of wide_div did this:

rem = (rem << 1) | bit;
if rem >= d { rem -= d; quo |= 1; }

rem << 1 overflows whenever rem carries its top bit, which happens for any large divisor — and Rust drops the bit silently in release builds. It mispriced roughly half the vectors. The fix reads the top bit before the shift; the comment in src/lib.rs records it, because the bug is more instructive than the fix.

This is also why Cargo.toml sets overflow-checks = true on the release profile: a missed checked_* should panic in a test rather than corrupt a reserve in production.

Where the guardrails are

• Dust. A one-unit buy is priced at the spot rate, not rounded to nothing, and never mints tokens out of rounding.
• Near exhaustion. The whole sale reserve must be quotable; a request beyond it is refused by name before any arithmetic runs.
• Creation. Vt > D is enforced rather than trusted — a curve created below it prices its last token at infinity.
• Slippage. Refused before any state moves, asserted by comparing the whole struct before and after.
• Two buckets. The sale reserve and the real collateral are accounted separately, and the_reserve_accounting_never_drifts asserts token conservation and that the pool never pays out more than it took in, over 24,000 randomised interleavings of buys and sells.

The weighted pool: a fractional power in integer arithmetic

src/weighted.rs is the other half, for RFP-016, whose swap formula carries a rational exponent:

tokens_out = Rt * (1 - (Rc / (Rc + C_in)) ^ (w_c / w_t))

x^e = exp(e * ln x) at a scale of 1e18, with argument reduction on both series. Two things in it are worth more than the code:

The reduction direction decides the precision. Reducing into [1, 2) gives -ln x = k*ln2 - ln m, a subtraction of two numbers both near 0.693 whenever x is near 1. At x = 0.99974 the difference is 0.00025 — three significant digits destroyed by cancellation, then multiplied by an exponent of up to 99. The first version did that and measured a worst error of 7e-12. Reducing into [1/2, 1) instead makes it k*ln2 + (-ln m), both terms non-negative. An addition cannot cancel.

The series length is a cycle budget, so it is a named constant. z = 1/3 exactly at x = 1/2 — the worst case, reached by every halving. Twelve terms leaves a 1e-13 tail; twenty-four puts it below 1e-19, at twelve more 256-bit multiplications per call.

Measured against 2,500 vectors from Python's decimal at 60 significant digits, biased towards x within 1e-3 of one, x down at 1e-18, and weight ratios from 99/1 to 1/99:

	worst absolute error, scale 1e18
first version, decimal scale	6,976,874  (7e-12)
after both fixes	86  (8.6e-17)
binfixed, binary scale	13  (1.3e-17)

The residual error points the safe way. pow sits slightly above exact in about half the vectors; tokens_out = Rt * (1 - pow) then rounds a high pow into a low payout. The pool keeps the difference, which is the same rule the bonding curve follows.

Also asserted: pow is monotone in the exponent, so no weight in the schedule pays better than the weights either side of it; a bigger buy never gets a better rate; and weight_at returns the correct weight with no poke at all, checked at every tick of a thousand-second schedule — which is the RFP's own wording, "regardless of how recently the last poke occurred".

Vesting

src/vesting.rs covers RFP-017: three schedule shapes, the cancellation split, and milestone signalling. None of it needs an account model to be settled, so none of it waits for one.

Two properties are worth more than the code. Claims over a fully elapsed schedule sum to the total exactly — rounding each step down would normally strand dust, so the final step returns the total directly rather than dividing again; the two agree mathematically, but routing the end through the general branch would make exactness depend on a division being exact, which it is not. And the cancellation split is three-way: already-claimed, vested-but-unclaimed and unvested all come from one vested_at call so they cannot drift, with the test sweeping every cancellation instant, with and without a prior claim, asserting the three sum to the original total.

Nothing is cached. vested_at is a pure function of the schedule and a timestamp, the same choice weight_at makes, for the same reason: there is no stale value, so there is no stale-value bug.

What CI actually checks

Not just that the tests pass.

• cargo fmt --check and cargo clippy -D warnings.
• The suite in release, because the release profile sets overflow-checks = true; running it in debug would exercise different arithmetic from the one that ships.
• The committed vectors are regenerated and diffed against their generators. A vector file quietly edited to make a failing test pass would not survive this, and that is the failure mode a committed oracle actually has.
• The cycle table is re-measured and compared to zkvm/CYCLES.md. The document is quoted in grant proposals; a figure that drifts is a public claim that stopped being true, and nobody notices until someone reproduces it. So zkvm/verify_cycles.py fails the build instead.

Fees

src/fees.rs implements both collection models, because the two RFPs differ for a reason that decides the code. A bonding curve is demand-bounded — under 1.4% ever graduate — so its fee is per swap or it earns nothing. An LBP is time-bounded, so every sale reaches its end and an at-close fee is always collectible.

Every fee rounds up, against the party paying: the trader on a swap, the creator at close. And the ordering on a buy is asserted rather than commented — the fee comes off before pricing, so the curve prices c_in - fee. Taking it after would credit the curve with collateral the treasury removes, inflating the reserve by the fee on every trade; the test constructs both and asserts the correct one ends with less.

Both proposals ship at a zero rate with a governance switch, so the cap is compiled in: 1% per swap, 5% at close. A rate above it is refused by name, not clamped — silently clamping a misconfiguration hides it from the person who needs to see it.

Deployed

Three programs are live on the public LEZ testnet, and each deployment carries the same four facts: the commit it was frozen at, the ImageID, the deploy transaction and the block. That is the convention logos-co/lez-payment-streams sets for its own live program, and it is what makes a deployment checkable rather than asserted.

Program	Freeze commit	ImageID	Deploy	Block
antumbra_curve	b5aa3da	49db0fc9…a56fc510	f074ffe1…4d8c3855	17265
antumbra_lbp	b5aa3da	51f28557…b6c7a82d	fbfe7e39…7bbe4859	17266
antumbra_vesting	b5aa3da	4c6e62a5…af93ea7f	9b35fc31…d1691ee2	17267

An earlier set of the same three programs is still on chain and is what the RFP issues quote, because those are the ones that were driven rather than merely deployed: they are built by 8c09b33, and their ImageIDs are bcd6d07d…, 249648dc… and 26134c79…. Check an ImageID against the freeze commit rather than against main, or the numbers will disagree for a reason that is not a defect. DEPLOYMENTS.md has both tables, the reconciliation, and every transaction that drove them.

Status

This is the pricing core, not the program. The SPEL program, the private purchase path, the Basecamp mini-app and the CLI are the subject of the RFP-015 proposal this repository accompanies.

Licence

MIT OR Apache-2.0, at your option: LICENSE-MIT and LICENSE-APACHE.

Cycle cost

zkvm/ runs the whole kernel under the RISC0 3.0.5 executor and reports cycle_count() deltas per operation; results and their reading are in zkvm/CYCLES.md. A constant-product buy is 10,622 cycles, flat across trade sizes, against LEZ's 32M public-execution cap. A vesting claim is 8,808 and a milestone signal is 30. The fractional power went from 314,248 cycles to 27,181 by moving to a binary working scale — 11.6x faster and 6.6x more accurate at the same time, with the first attempt at that rewrite recorded alongside it because it was wrong in a way worth keeping.