feat(2c-D): C2 — the realization and fence-release cutover - #856
Merged
Conversation
…r determined
Adds 2c-D §14 before the live path changes: the survey of what the cutover
touches, owner ruling C2-R1 (post-certification receipt handling) and C2-R2
(CORR.4 typed, the orientation requirement, Tier-1 intent satisfaction)
verbatim, the owner-apply boundary, and the determinations made under them:
- D-a Tier 1 is re-sourced as 2c-E §6 SAT.1-SAT.6; the 5-c-1 gate C2 deletes
was its only enforcement point.
- D-b "durably published" is quorum publication of a frozen artifact.
- D-c TA_B is located through a non-authoritative locator keyed by b.
- D-d PartialPendingRealization is deleted with its only constructor.
- D-e the self-referential receipt verifier is deleted; Req 21.16 is the
only receipt verifier.
- D-f the completion resumes and never retries: the SAME bound, advanced
settlement is re-certified, its exact receipt published at quorum, and
its exact fence released — no bind round, transition or admission.
- D-g conformance repair: later generations draw reserve provenance from the
composed DLV frontier (owner baseline + certified successors), as the
SoFi model requires, and the route preflights that rule before binding.
Implements 2c-D §14 (owner rulings C2-R1 and C2-R2, frozen in the preceding docs commit). A market settlement is now realized end to end on the live route: preflight reserve provenance (the same rule admission applies) -> bind -> trader advance, admitted; TA_B + locator published -> compose with the locally built V1 as Req 21.16 EVIDENCE -> a fold that may_certify() for exactly b -> freeze V1 for the vault's set, sweep, require quorum publication -> SuccessorAccepted at the fence the binding placed The route answers `realized:<b>` or `bound-unrealized:<b>`. Anything short of a certified fold plus quorum publication leaves the settlement bound and unrealized with the fence held; the QuorumBind COMMIT stays authoritative. Core (dsm): - successor_validity: CORR.4 typed one equality per field; orientation before any derivation; the accepted market successor derived from the lineage-verified DlvSettle; Tier-1 intent satisfaction (2c-E SAT.1-SAT.6) re-sourced into the walk (D-a). IndependentRealization::from_parts takes correspondence, the §7 BundleAcceptanceWitness and IntentSatisfaction. - PartialPendingRealization and may_fold() deleted with their only constructor; C3Verdict::class() is total (D-d). - verify_trader_settlement_receipt deleted with the two ReceiptError variants only it produced (D-e). Req 21.16 is the only receipt verifier. - dlv::composed_history: the SoFi composed-state rule as reserve provenance (D-g, conformance repair). DlvReserveConsumption provenance accepted only owner reserve leaves at exactly the consumed generation, which only the owner's own apply produces, so no delegated market could pass generation 0 with its LP away. Now: owner leaves back ONE baseline generation; past it, V_n must be exactly the composed state at c_n, reached from that baseline through certified, linked, consecutive successors. The history comes from a resolver method that fails closed by default. - decode_trader_acceptance; ValidatedPeerTransition carries embedded_parent. SDK (dsm_sdk): - the composition walk certifies market folds and folds nothing that fails may_certify(); the 5-c-1 MarketRealization path is deleted. It can compose UP TO a requested state without reading its binding (NotObserved), which keeps the provenance of settlement n from depending on settlement n. - complete_settlement: the one completion path — recover the exact frozen V1 or build it once, certify, publish at quorum, release exactly, idempotent. - D-f: resume_settlement_completion finishes the SAME bound, advanced settlement from its fence row and re-hashed bundle; run from storage sync. No binding round, transition, admission or new settlement. - the settle route preflights reserve provenance BEFORE bind_settlement with the same rule, so a trade admission would refuse never strands a generation. - TA_B is located by b through a non-authoritative locator (D-c). - settlement_receipt_codec is transport only (C2-R1 point 8). - dlv.reconcile and unapplied_settlements_for_vault act only on the exact certified fold (C2-R1 point 6). - the walk's local receipt candidate is used only for its own settlement. Tests: settle-dependent route tests drive realization through the route; the admission-skipping fixture is kept only as an explicit uncertified bypass for a negative test; lp_offline proves three generations realize with the LP absent; new controls for D-f (a)-(e), the owner-apply boundary, a receipt below quorum, the pre-bind refusal, and the composed-state rule (b-h).
cryptskii
added a commit
that referenced
this pull request
Sep 11, 2026
…venance, and a walk that folds only what certifies (#857) C2 (#856) changed three things the Lean tree did not yet say. This brings the models to the code, as the formal models are kept alongside it. - DSMSettlementCompletion.lean (new, 17th module): the one completion pass the settle route and D-f's resume share. Proves the fence is released only after the exact receipt is at quorum and only in a certifiable pass; below quorum or uncertified it stays held; a receipt already at quorum is verified, not re-sent; a second pass changes nothing; a pass never changes b or the permitted successor. - DSMComposedReserveProvenance.lean (new, 18th module): D-g's rule — owner backing at one baseline generation, and past it a parent that is exactly the last state of a linked, consecutive history from that baseline. Proves soundness, that each conjunct is necessary, and that composition for provenance stops AT its target, so provenance of generation n never reads the state the settlement consuming n produces. - DSMAcceptedSuccessorWalk.lean: partialPendingRealization deleted (D-d). The walk folds exactly what certifies; a market successor without the 2c-D witness is not folded, and with it certifies. - DSMBundleAcceptance.lean: the banner no longer says fence release and Req 21.16 are owed. - CI: the Lean module pin moves 16 -> 18. - 2c-D §14: D-f and D-g name the modules that machine-check them. Mutation controls executed: seven, each with the kernel proving the named sample theorem false, each reverted and cmp-verified.
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.
2c-D C2 — the realization and fence-release cutover
C2 is the realization / fence-release cutover. Implements amendment 2c-D §14 (owner rulings C2-R1 and C2-R2, frozen verbatim in the first commit). A market settlement is now realized end to end on the live route, and nothing short of the complete certification predicate opens a market boundary.
dlv.unlockRoutedanswersrealized:<b>orbound-unrealized:<b>. Missing, unavailable, or below-quorum evidence leaves the settlement bound and unrealized with the fence held; present-and-failing evidence is INVALID. There is no timeout release, no fallback realization path, no receipt-as-authority shortcut, and no second way to build aBundleAcceptanceWitness.What changed
may_certify(). The 5-c-1MarketRealizationpath is deleted.dlv.reconcileandunapplied_settlements_for_vaultact only on the exact certified fold (C2-R1 point 6); the request names(vault, x)and every applied fact comes from the fold.fetch_receipt-> Absent / Unavailable / Malformed / Decoded (point 8).PartialPendingRealization+may_fold()(their only constructor was 5-c-1;class()is now total),verify_trader_settlement_receipt+ the twoReceiptErrorvariants only it produced, the legacyfetch_verified_receipt, and the bind-only settle fixture that bypassed completion.TraderAcceptanceLocatorV1(proto) locatesTA_Bbyb; non-authoritative (D-c).Required controls (PR C ruling) -> named tests
a_settled_market_publishes_its_acceptance_and_realizes,a_routed_settle_clears_every_gate_and_realizes,a_foreign_trader_clears_every_gate_and_realizes_its_settlementa_legacy_receipt_alone_does_not_realize_a_market_bundlea_present_but_malformed_acceptance_locator_is_invalid_not_absent;truncated_or_trailing_bytes_are_not_an_acceptance,a_nested_leaf_of_another_class_is_refused,decoded_bytes_meet_the_frozen_rejectionsban_acceptance_for_another_bundle_is_refuseda_path_that_folds_elsewhere_is_refusedeconomic_operation_idan_acceptance_naming_another_economic_operation_is_refused(new: the leaf sits where this operation's leaf belongs, so only §7 step 5's identity equality can refuse it)an_altered_path_is_refused,the_receipts_own_device_path_is_not_evidencea_path_checked_against_another_validated_root_is_refused,a_self_rooted_receipt_is_refused_though_its_own_device_path_proves_ita_settlement_whose_receipt_misses_quorum_stays_bound_and_keeps_its_fencecompile_faildoctests onCompleteValidity;the_acceptance_witness_has_exactly_one_construction_siteduplicate_binding_finality_quarantines_the_lineage_with_all_five_effectsan_owner_apply_applies_only_the_exact_certified_folda_rival_settle_on_a_committed_parent_is_excluded_and_changes_nothingMutation controls
Each control deletes or bypasses ONE gate, runs the named test that must go red by performing the forbidden action, then restores the file from a byte copy and verifies the restore with
cmp. All observed RED, all restored.leg_delta_out == output_amount)effects_that_are_not_the_routes_economics_do_not_correspondeffects_that_are_not_the_routes_economics_do_not_correspondonly_the_vaults_own_pair_in_a_permitted_orientation_is_tradablea_route_commit_signed_by_anyone_else_is_not_the_traders_intenta_route_that_is_not_the_signed_hop_is_refusedeconomic_operation_idequalityan_acceptance_naming_another_economic_operation_is_refuseda_settlement_whose_receipt_misses_quorum_stays_bound_and_keeps_its_fencea_completion_that_missed_quorum_is_finished_by_resuming_the_same_settlementan_owner_apply_applies_only_the_exact_certified_foldbind_settlementa_deterministic_provenance_failure_is_refused_before_bindinga_successor_missing_from_the_certified_history_authorizes_nothinga_skipped_generation_is_refuseda_wrong_parent_state_commitment_is_refusedaltered_reserves_are_refusedMS1 and MD1 exercise the one shared requirement in
complete_settlementfrom its two callers.D-f — completion resumes, it never retries
resume_settlement_completionfinishes the SAME bound, advanced settlement whose receipt missed quorum: it re-reads the fence at exactly (chain, parent,tx_id), fetches the bound bundle byband re-hashes it, requires the bundle's own parent and successor to be the fence's, takes the trade from the bound operation, and runs the one completion path (recover the exact frozen V1 or build it once → re-certify → quorum → exact release). No binding round, transition, admission or new settlement; never a cached-status or timeout release. Run from storage sync beside the close-intent resume.a_completion_that_missed_quorum_is_finished_by_resuming_the_same_settlementa_receipt_published_before_the_release_is_verified_and_the_same_fence_releaseda_resume_at_altered_coordinates_refuses_and_holds_the_fenceb/tx_id, parent, chain, bundle address, successor (and so operation id), or receipt facts: refused, fence held, nothing publishedan_uncertified_settlement_cannot_be_resumed_into_a_releasea_bypass_settlement_cannot_realize_owner_apply_or_release_its_fenceD-g — later generations draw reserve provenance from the composed frontier (conformance repair)
lp_offlineexposed thatDlvReserveConsumptionprovenance accepted only owner reserve leaves at exactly the consumed generation — produced only by the owner's own admitted apply — so no delegated market could pass generation 0 with its LP away, contrary to the SoFi composed-state model. The deleted bypass fixture had hidden it. The same rule now holds at every generation (dsm::dlv::composed_history::check_composed_reserve_provenance): the owner's proof backs ONE baseline generationg; atgthe parent states exactly those reserves; pastgthe parent must be exactly the composed state at its commitment, reached from that baseline through certified, linked, consecutive successors. No wire change, no new witness; owner catch-up stays optional synchronization.Non-circularity. Composition for provenance stops AT the requested state and never reads its binding (
FrontierBinding::NotObserved). Certifying settlement n establishesV_{n+1}; admitting settlement n+1 consumes it by composing up toc_{n+1}, which certifies only settlements < n+1. The recursion runs strictly down the generations.Bind-before-knowable-failure, fixed. The route used to bind first and only then learn that admission would refuse, stranding the generation. It now runs the same rule, over the same owner proof and composed history, BEFORE
bind_settlement.the_baseline_generation_is_provenanced_by_the_owners_leaves_alonelater_generations_are_provenanced_by_the_composed_history_with_the_lp_absent;lp_offline_market_advances_three_generations_and_lp_reconciles_each_once(route, three certified generations, no owner action between)a_successor_missing_from_the_certified_history_authorizes_nothinga_wrong_generation_is_refused,a_skipped_generation_is_refused; route probes inlp_offlinea_wrong_parent_state_commitment_is_refusedaltered_reserves_are_refusedlp_offlineprobe-behind (refused at the composed frontier; the register's exclusivity is the authority)a_deterministic_provenance_failure_is_refused_before_bindingKnown and recorded
dlv.unlockRoutedresultvaultIdBase32; it has carried<status>:<b>since 5c-2 Step 4. Filed as a separate task, untouched here.Verification
Toolchain pinned 1.98.0. Targeted, per edited module (the board runs in CI):
dsmlib, targeted modules (composed_history,provenance,peer_lineage,successor_validity,published_receipt,settlement_receipt_leaf,acceptance_verify): 75/0;dlv::composed_historyafter the gap-test strengthening: 9/0dsmdoctests (successor_validity, incl. thecompile_failguards): 6/0dsmintegration:economic_dlv_settle_provenance16/0,economic_admission_lifecycle18/0,economic_dlv_owner_apply_provenance8/0,economic_peer_evidence9/0,economic_provenance_semantics9/0,trader_acceptance_producer9/0,economic_provenance_wire18/0dsm_sdklib: codec, walk, locator, fence table, economic registers and every settle-dependent route test, incl.lp_offline(three certified generations, LP offline) and all D-f / preflight / bypass controls: 58/0cmp-verifiedcargo fmt --all -- --check: cleanmake lint: exit 0 (fmt --check + clippy --all-targets, pinned 1.98.0)ci/production_safety_checks.sh: exit 0 (clippy production safety checks + TLA+ formal verification passed)