Files
dex/pkg/dexprotocol
zeekayandHanzo Dev 4fb53657b1 dexprotocol: quantity is conserved per order, asserted every transition
Exclusive() proves an ExecID cannot sit in two domains. It says nothing
about how much of an order has been committed, so D could certify ten
executions against one order for its full quantity — each individually
valid, correctly certified, correctly scoped — and settle whichever the C
successors happened to include. Every defect the last review turned up
was a conservation bug rather than a determinism bug, so this is tracked
rather than left as a property that happens to hold.

Per order: reserved + traded <= authorized. Reserving takes from
available, settling moves reserved to traded, releasing gives it back.
That last one is what makes a portable Order work at all — an order whose
execution lost the race is still live and matchable again, and a release
that failed to return the quantity would silently shrink every order that
ever lost one.

Conserved() recomputes both totals from the domains themselves rather
than restating the counters, so an accounting update that drifted from
the objects it summarises is caught instead of trusted. A random
400-step lifecycle asserts it plus Exclusive() after every transition:
36 reserved, 96 traded, 86 released in the recorded run.

Units are the book's lots, matching Execution.Quantity, never the order's
Input in token base units. The lot size is market metadata and stays out
of this package: a caller that knows the market converts once and passes
authorized in, and the value is checked for agreement across every
reservation so a second, different conversion cannot enlarge an order.

51 tests, up from 25 before the reshape.

Co-authored-by: Hanzo Dev <[email protected]>
2026-08-07 12:15:32 -07:00
..