mirror of
https://github.com/luxfi/dex.git
synced 2026-09-24 00:26:31 +00:00
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]>