mirror of
https://github.com/luxfi/dex.git
synced 2026-09-24 00:26:31 +00:00
THE INVARIANT
An Execution may be reserved only against an accepted C parent. The unique
accepted child of that parent permanently decides the Execution: membership
means Trade; non-membership means Release. Neither C nor D reads the other
chain's live state during consensus execution.
CPARENT ACCEPTED-ONLY
Acceptance is the finality boundary, so an accepted P is guaranteed exactly one
accepted child, and that child decides every execution reserved against P. This
removes the abandoned-parent case entirely rather than handling it: there is no
proposed parent to abandon. It also collapses two questions — "did P win?" and
"which child of P won?" — into one.
AcceptedBlock is now a struct with unexported fields, produced only by
VerifyAcceptedBlock. Unexported fields alone still leave AcceptedBlock{}
constructible from outside, so a `verified` sentinel closes that hole and every
transition requires it. Symmetric with VerifiedExecution.
Never use local C state as the proof. Even co-located, different D validators
observe C advancement at different instants, so `localC.LastAccepted()` is not a
function of the block being executed. The local C VM is delivery; the
authenticated statement is consensus input — the same rule already proven in the
other direction.
THREE RULES, NO CLOCKS
Accepted(P) permits Reserve(E), E.CParent == P
Accepted(Q), Q.Parent==P, E in Q.ExecRoot permits Settle(E) -> Trade
Accepted(Q), Q.Parent==P, E not in root permits Release(E)
NON-INCLUSION IS FIRST-CLASS
Release is half the protocol, not a fallback, and it is the half that returns a
trader's liquidity. So ExecRoot is a sparse Merkle commitment over the 256-bit
ExecID keyspace where absence has the SAME proof shape as presence: the path to
the key, terminating in the empty leaf. One verifier, one code path, one bit of
difference. Leaf and node domains are separated against second-preimage
substitution, and the empty leaf is a distinct constant so absence cannot be
forged. Proofs carry a bitmap and omit empty siblings, so size tracks the
executions actually in the block, not the depth.
A useless reservation is still resolvable: if D reserves against P only after C
accepted Q, anyone can deliver Accepted(Q) plus non-inclusion and release it.
Correctness does not depend on D winning that race.
Also removes the last references to a flag day, which was never authorized —
0x9999 activated 2025-12-25 and settle_module is AlwaysOn. The wire-compatibility
test keeps its value and loses the dead concept from its name and prose.
24 tests passing in dexprotocol, dchain suite green.
Co-authored-by: Hanzo Dev <[email protected]>