feat(dlv): Step 4 — G1-G4 enforced, and the live market path binds to bound-but-unrealized - #834
Merged
Merged
Conversation
…nforce them on Step 4 requirement 3. 2c-B froze four conjuncts over MarketTerms field 6 and deferred them for a stated reason: their operand did not exist, and nothing was permitted to fabricate one to make a vector pass. The producer supplied the operand; this is the half that checks it, and the half a foreign verifier runs. G1 operation_bytes decode under DlvSettleOperationPreimageV1, all bytes consumed G2 canonical re-encode reproduces the carried bytes exactly G3 discriminator 26 and mode Unilateral G4 relationship_chain_tip_v2 over the carried inputs == trader_successor Placement follows the two rulings that constrain it rather than convenience. NOT the generic CCB decoder: the owner ruled the chain-tip recomputation is successor-evidence validity rather than byte decoding, and putting it there would make every decode of any bundle hash a foreign grammar. NOT the C4 walk: 2c-C4 says these gate the bundle's structural validity, not the economic walk, which treats the bytes as opaque. The sibling conjunct that IS in-bundle structure, embedded_parent == trader_parent, stays where it was, enforced at construction and decode. Errors are structured, one arm per conjunct, so the arm IS the finding. G4 carries both the carried and the recomputed successor, because "these differ" is the whole content of that refusal. The discriminator is read before decoding, so a close preimage arriving where a settle belongs reports as a wrong tag rather than as an undecodable blob. The producer now verifies its own output. G1-G4 hold there by construction, so the check can only fire if the construction stops being what it claims — which is exactly when a silent divergence would otherwise begin. It also means this is not a verifier sitting uncalled: a producer that cannot pass the check a foreign party runs has no business emitting a bundle. Teeth, including the two requirement 10 names: - a single altered operation byte is rejected. The test flips byte 10, inside vault_id, deliberately: the bytes stay decodable and canonically re-encodable so G1-G3 all pass and G4 is the conjunct actually under test. My first attempt flipped the last byte, which is mode, and proved G3 instead — the failure is worth recording because a mutation test that fires the wrong gate looks identical to one that works. - a supplied successor different from the recomputed one is rejected, and the refusal reports both values. - trailing bytes, a wrong discriminator, empty bytes, and a bilateral settle are each refused separately. The bilateral case re-derives the tip first so ONLY the mode is wrong, or G4 would fire and the test would prove nothing about G3. dsm dlv::market 15/15, ccb 18/18, conformance 12/12. make lint green; production safety checks green. Scope: this does NOT lift the market emission refusal. Requirements 1, 2 and 4-10 — the live bind path to bound-but-unrealized — are next, and realization stays unreachable until 2c-D.
cryptskii
changed the title
cryptskii
added a commit
that referenced
this pull request
Sep 10, 2026
…zed (RE-OPENED — lost from #834's merge) (#836) * feat(dlv): enforce 2c-B's G1-G4, now that genuine operands exist to enforce them on Step 4 requirement 3. 2c-B froze four conjuncts over MarketTerms field 6 and deferred them for a stated reason: their operand did not exist, and nothing was permitted to fabricate one to make a vector pass. The producer supplied the operand; this is the half that checks it, and the half a foreign verifier runs. G1 operation_bytes decode under DlvSettleOperationPreimageV1, all bytes consumed G2 canonical re-encode reproduces the carried bytes exactly G3 discriminator 26 and mode Unilateral G4 relationship_chain_tip_v2 over the carried inputs == trader_successor Placement follows the two rulings that constrain it rather than convenience. NOT the generic CCB decoder: the owner ruled the chain-tip recomputation is successor-evidence validity rather than byte decoding, and putting it there would make every decode of any bundle hash a foreign grammar. NOT the C4 walk: 2c-C4 says these gate the bundle's structural validity, not the economic walk, which treats the bytes as opaque. The sibling conjunct that IS in-bundle structure, embedded_parent == trader_parent, stays where it was, enforced at construction and decode. Errors are structured, one arm per conjunct, so the arm IS the finding. G4 carries both the carried and the recomputed successor, because "these differ" is the whole content of that refusal. The discriminator is read before decoding, so a close preimage arriving where a settle belongs reports as a wrong tag rather than as an undecodable blob. The producer now verifies its own output. G1-G4 hold there by construction, so the check can only fire if the construction stops being what it claims — which is exactly when a silent divergence would otherwise begin. It also means this is not a verifier sitting uncalled: a producer that cannot pass the check a foreign party runs has no business emitting a bundle. Teeth, including the two requirement 10 names: - a single altered operation byte is rejected. The test flips byte 10, inside vault_id, deliberately: the bytes stay decodable and canonically re-encodable so G1-G3 all pass and G4 is the conjunct actually under test. My first attempt flipped the last byte, which is mode, and proved G3 instead — the failure is worth recording because a mutation test that fires the wrong gate looks identical to one that works. - a supplied successor different from the recomputed one is rejected, and the refusal reports both values. - trailing bytes, a wrong discriminator, empty bytes, and a bilateral settle are each refused separately. The bilateral case re-derives the tip first so ONLY the mode is wrong, or G4 would fire and the test would prove nothing about G3. dsm dlv::market 15/15, ccb 18/18, conformance 12/12. make lint green; production safety checks green. Scope: this does NOT lift the market emission refusal. Requirements 1, 2 and 4-10 — the live bind path to bound-but-unrealized — are next, and realization stays unreachable until 2c-D. * feat(dlv): the live market path binds, and stops at bound-but-unrealized Step 4, requirements 1, 2, 4, 5, 8 and part of 10. The refusal that stood here was correct for exactly as long as its reason held: a canonical market bundle needs the trader's prepared successor and its evidence, and no producer could make them. 5c-2 Step 2 built that producer, so the reason is spent and keeping the refusal would itself have become the stale thing. What the route now does, in this order and not another: sign the settle the signature is INSIDE the bytes the chain tip hashes, so a settle cannot be signed after the advance prepare, purely no writes, no head install — it exists to learn the embedded parent and the entropy the tip covers, both the device's own produce prepare_market_successor RECOMPUTES the successor from those exact bytes; market_terms runs G1-G4 over its own output cross-check the producer's successor must equal the prepare's own. They compute it by the same rule from the same inputs, so a disagreement means one is not doing what it says, and binding a successor this device would not advance to is worth refusing hardest derive the successor from the AUTHENTICATED V_n, by the rule every verifier applies publish, fence, bind all inside bind_settlement, which publishes the canonical bundle to a quorum of the vault's COMMITTED storage set and refuses before any fence or binding round if that is not durable Requirement 4 needed no new code: publication-before-binding with a quorum, and a failed publication leaving no bind, no fence and no rival excluded, were already implemented inside bind_settlement ahead of place_fence. The live path uses that ordering rather than reimplementing it. Requirement 5: the fence is keyed on the TRADER's own chain and parent, never the vault's. A market settle consumes the trader's sovereign chain position; reusing the close path's vault-keyed identity would fence the wrong thing. Both tests assert the absence of a vault-keyed row, which is the checkable half of that. Requirement 2 needed plumbing, because the operands died at a scope boundary. The composition's owner identity and the vault's fee are now carried on SettleTerms, and the checked amounts come from the re-simulation that proved them rather than a second narrowing — the narrowing's own comment says a second site is how the difference gets minted. AmmVerifyOutcome returns them instead of discarding them. WHAT THIS DOES NOT LIFT. Realization. No balance moves, no head advances, no reserves move, no receipt is published, and the fence is not released. Ruling R1 and V3 put the acceptance witness, fence release, receipt publication and the realized frontier behind 2c-D, and nothing here reaches any of them. Binding a trade is not settling it. The two tests that asserted the refusal now assert the end state instead, both halves separately, because "it bound" and "it did not realize" fail in opposite directions. The foreign-trader test is the one that matters most: a device holding no owner record and no owner signature binds a trade against the owner's liquidity while the owner is offline, and still cannot realize it. A re-submission of the same trade is now accepted rather than refused, and that is asserted: the generation is bound by that very trade, and a trader retrying after a dropped response must not be told the vault is taken by someone else. The three operator docs banded earlier said market settlement was deployment-blocked. That is no longer true, so their banners are rewritten rather than left to mislead in the opposite direction from before. dsm_sdk: dlv_routes 37/37, vault_state_composition 22/22, route_commit_sdk 43/43, settlement_bind 7/7, binding_occupancy 10/10, settlement_resume 2/2 — all serial. make lint green; production safety checks green. Still owed in Step 4: requirement 6's second half (running the accepted-successor and economic-admission path after COMMIT), and the remaining requirement 10 controls. The trader's advance is deliberately NOT committed here, so nothing it would credit exists yet to be mistaken for realization.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Step 4, in two parts on one branch. Requirements 1, 2, 3, 4, 5, 8 and part of 10.
Part 1 — the deferred conjuncts (requirement 3)
2c-B froze
G1–G4overMarketTermsfield 6 and deferred them because their operand did not exist. #833 supplied it.Placement follows the rulings, not convenience: not the generic decoder (the owner ruled the chain-tip recomputation is successor-evidence validity, not byte decoding), and not the C4 walk (which treats these bytes as opaque). The producer now verifies its own output, so this is not a verifier sitting uncalled.
Part 2 — the live path (requirements 1, 2, 4, 5, 8)
The refusal was correct for exactly as long as its reason held. The producer spent that reason, so keeping it would itself have become the stale thing.
The order is the substance:
G1–G4run over the outputV_n, by the rule every verifier appliesbind_settlementRequirement 4 needed no new code. Publication to a quorum of the vault's committed set, ahead of any fence or binding round, with a failed publication leaving no bind, no fence and no rival excluded, was already implemented. The live path uses that ordering rather than reimplementing it.
Requirement 5: the fence is keyed on the trader's own chain and parent, never the vault's. Both tests assert the absence of a vault-keyed row.
Requirement 2 needed plumbing: the owner identity and vault fee died at a scope boundary, and the checked amounts were discarded. They now travel on the settle terms, and the amounts come from the re-simulation that proved them rather than a second narrowing — the narrowing's own comment says a second site is how the difference gets minted.
What this does not lift
Realization. No balance moves, no head advances, no reserves move, no receipt is published, the fence is not released. Rulings R1 and V3 put all of that behind 2c-D and nothing here reaches it.
The two tests that asserted the refusal now assert the end state, both halves separately, because "it bound" and "it did not realize" fail in opposite directions. The foreign-trader case is the one that matters: a device with no owner record and no owner signature binds against the owner's liquidity while the owner is offline, and still cannot realize it.
Re-submitting the same trade is now accepted rather than refused, and that is asserted — a trader retrying after a dropped response must not be told the vault is taken by someone else.
The three operator docs banded in #822 said settlement was deployment-blocked. Rewritten rather than left to mislead in the opposite direction.
Verification
dsmdlv::market15/15 ·ccb18/18 · conformance 12/12.dsm_sdkdlv_routes 37/37 · composition 22/22 · route_commit 43/43 · bind 7/7 · occupancy 10/10 · resume 2/2, all serial.make lintgreen; safety checks green.Still owed in Step 4
Requirement 6's second half — running the accepted-successor and economic-admission path after commit — and the remaining requirement 10 controls. The trader's advance is deliberately not committed here, so nothing it would credit exists yet to be mistaken for realization.