mirror of
https://github.com/luxfi/dex.git
synced 2026-09-24 00:26:31 +00:00
zeekayandHanzo Dev
aae6cd0857
Three separate proofs, none able to stand in for another:
cross-chain C + C->D + D + D->C constant token base units
D-local owned == available + reserved token base units
order-local original == open + reserved
+ traded + canceled LOTS
The units stay apart. Merging them is how a lot count gets added to a wei
balance and type-checks; the market's lot size connects the domains and
one test asserts the two numbers differ, so a future merge has to delete
an assertion rather than quietly succeed.
Four terms, not three. Open lots are restable and cancellable; reserved
lots are committed to a match already in flight. Collapsing them loses
the property that matters: Cancel takes the OPEN quantity only, because a
cancel reaching committed lots would let the same lots be cancelled and
traded, which is the order-book form of a double spend. The committed
remainder resolves when its match does, and the trader may cancel again
to retire whatever came back.
Cancel is a no-op on an order with nothing open rather than an error.
"Retire whatever you can" is the honest reading of the request, and
failing it would force callers to inspect state to avoid an error they
cannot prevent.
Every transition moves lots between two terms and never writes a total,
so conservation is a property of the shape. A 3000-step random run
asserts it after each: 548 trades, 451 cancels, 528 returns, 257 orders
replenished. The run replenishes exhausted orders deliberately — without
that it did 67 real transitions in 3000 steps, and a floor assertion now
fails if it degrades back to flattering the step count.
75 tests.
Co-authored-by: Hanzo Dev <[email protected]>