diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 86ca02d7..7df4711f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -553,7 +553,7 @@ jobs: - name: Kernel-check every module, sorry-free run: | set -euo pipefail - expected=14 + expected=15 found=$(ls lean4/*.lean | wc -l) if [ "$found" -ne "$expected" ]; then echo "::error::lean4/ has $found modules, expected $expected." diff --git a/docs/papers/amendment-2c-c3-valid-dlv-successor.md b/docs/papers/amendment-2c-c3-valid-dlv-successor.md index 9301d49b..31219af5 100644 --- a/docs/papers/amendment-2c-c3-valid-dlv-successor.md +++ b/docs/papers/amendment-2c-c3-valid-dlv-successor.md @@ -994,8 +994,10 @@ adopting change record. **Formal coverage — PROVED AS CLAIMED.** `DSMValidDlvSuccessor.lean` carries proof bodies for every statement, a per-theorem `#print axioms` report (no result depends on `sorryAx` or `Classical.choice`), and two executed mutation controls; `DSMLineageQuarantine.lean` (2c-C3.1) adds -twenty results and four executed controls. CI kernel-checks all fourteen modules with the count -pinned — thirteen until 2c-C4's adopting change added `DSMAcceptedSuccessorWalk.lean`. "Axiom-free" remains a per-theorem statement, never a blanket one. +twenty results and four executed controls. CI kernel-checks all fifteen modules with the count +pinned — thirteen until 2c-C4's adopting change added `DSMAcceptedSuccessorWalk.lean`, and fourteen +until 2c-E's added `DSMTradeIntentCorrespondence.lean`. "Axiom-free" remains a per-theorem +statement, never a blanket one. # Scope diff --git a/docs/papers/amendment-2c-e-trade-intent-exact-output.md b/docs/papers/amendment-2c-e-trade-intent-exact-output.md index 537f7bde..7990676b 100644 --- a/docs/papers/amendment-2c-e-trade-intent-exact-output.md +++ b/docs/papers/amendment-2c-e-trade-intent-exact-output.md @@ -202,8 +202,16 @@ cut. retargeted to the `Route`/`RouteCommit` correspondence of §5. 2. **The CCB field table in code** — encoder, strict decoder and the schema constants — cut to schema 2, with schema-1 bytes refused as **burned** rather than merely unknown. -3. **The formal predicate that consumes `TradeIntent`** updated, so the machine-checked statement is - about the object that ships. +3. **The formal predicate that consumes `TradeIntent`.** *(Corrected: there was none to update.)* + No Lean module and no TLA+ specification referenced `TradeIntent` or any of the four retired + members — the search returns zero hits across `lean4/` and `tla/`. So the obligation is to + AUTHOR the predicate, not to reconcile one, and "remove every formal dependency on the retired + members" is discharged vacuously and recorded as such rather than silently skipped. Landed as + `lean4/DSMTradeIntentCorrespondence.lean`, the fifteenth module, machine-checking `SAT.1`-`SAT.6` + with the market policy as a parameter so the model fixes no pricing rule. Its load-bearing + result is `the_tautological_form_accepts_the_forgery`: SAT.5 compared against the route's own + claim accepts a trade the authenticated-state comparison refuses, so the forbidden shape is + provably a different predicate rather than a stylistic preference. 4. **The MARKET class-1 vector.** *(Corrected 2026-09-09 by owner ruling — the original wording was self-contradictory and is preserved at the end of this item.)* Two different acts are involved and only one of them is the one-time act: @@ -275,11 +283,11 @@ controls in §8.5 each turn a **named** test red by performing the forbidden act ```text §8.1 registry transcription DONE -§8.2 encoder / decoder cut to schema 2 NEXT — may land independently (§8.4 as corrected) -§8.3 formal predicate owed +§8.2 encoder / decoder cut to schema 2 DONE — landed alone, per §8.4 as corrected +§8.3 formal predicate DONE — authored, not updated; nothing referenced it §8.4 genuine-operand regeneration owed, and lands WITH the producer, not before §8.5 mutation controls owed ``` -The 5c-2 market producer remains blocked on §8.2 and §8.3. The market emission refusal is untouched +The 5c-2 market producer is no longer blocked by this amendment: §8.1-§8.3 are complete. The market emission refusal is untouched by any of this and stays fail-closed until the producer exists. diff --git a/docs/papers/ccb-object-registry.md b/docs/papers/ccb-object-registry.md index b1f6ba48..b3bcfcd6 100644 --- a/docs/papers/ccb-object-registry.md +++ b/docs/papers/ccb-object-registry.md @@ -1948,7 +1948,12 @@ In order, and not combined: carries it, requiring `exact_out` to be checked by re-simulation against the authenticated `V_n`, never against the route's own account, or the predicate is a self-attestation. The schema bump propagates mechanically under §2.7 to `0x0033` and `0x000E`, moving every market - bundle's `b` and `addr`. **2c-E allocates no class number.** Its adopting change — the encoder + bundle's `b` and `addr`. Lands the **fifteenth** Lean module, + `DSMTradeIntentCorrespondence.lean`, machine-checking `SAT.1`-`SAT.6` with the market policy as + a parameter; CI module pin 14 → 15. Its load-bearing result is that the FORBIDDEN shape — SAT.5 + compared against the route's own claim rather than the authenticated `V_n` — accepts a forgery + the real predicate refuses, so the two are provably different predicates. + **2c-E allocates no class number.** Its adopting change — the encoder and strict decoder cut to schema 2 with schema-1 bytes refused as burned, the formal predicate, the producer, the class-1 market vector regenerated exactly once from it, and three mutation controls — is NOT started. diff --git a/lean4/DSMTradeIntentCorrespondence.lean b/lean4/DSMTradeIntentCorrespondence.lean new file mode 100644 index 00000000..95c86d39 --- /dev/null +++ b/lean4/DSMTradeIntentCorrespondence.lean @@ -0,0 +1,251 @@ +/- + Trade-intent correspondence — self-contained Lean 4 (no Mathlib, no imports) + + Machine-checks the satisfaction predicate amendment 2c-E §6 freezes, for the + schema-2 exact-output `TradeIntent`: + + - SHAPE the intent is the six SIGNED members. The four schema-1 + members `min_out`, `max_fee`, `max_fanout` and `k` are not + modelled anywhere in this file, because they no longer + exist: RouteCommit v2 deleted the model they belonged to + - AGREE every member is checked against the canonical RouteCommit + the trader actually signed, under a verified signature + - INDEPENDENT SAT.5 checks `exact_out` against the market policy evaluated + on the AUTHENTICATED `V_n`, never against the route's own + account of itself + - TEETH a disagreement is REFUSED, one conjunct at a time. Each of + the six is separately necessary + - NOT VACUOUS the forbidden shape -- SAT.5's operand taken from the route + instead of the authenticated state -- ACCEPTS a trade this + predicate refuses. That is the whole reason SAT.5 is worded + the way it is, and it is proved here rather than asserted + + What this module does NOT claim: + + * It is a model of the NORMATIVE objects, not a refinement proof from the + shipped Rust. Digests and amounts are `Nat`; equality of `Nat` stands for + equality of canonical bytes, and nothing here claims the Rust computes + these values. + * The market policy is a PARAMETER. This module does not fix the + constant-product rule, its rounding, or its admissibility conditions; it + proves the SHAPE of the correspondence for any policy. `samplePolicy` + exists only to make the counterexamples closed terms the kernel can + decide. + * Signature verification is a `Bool` here. That `sigma` verifies under the + authority resolver's proven key is 2c-E §2's obligation and is not + modelled. + * `G1`-`G4` (2c-B's grammar and chain-tip conjuncts) are NOT modelled. They + gate the bundle's structural validity and arrive with the 5c-2 producer. + * Nothing here lifts the market emission refusal or bears on realization, + which stays unreachable until 2c-D. + + Mutation controls, executed rather than asserted, and reported from the + kernel's actual output: + + 1. SAT.5's operand replaced by the route's own claim + (`i.exactOut == policy v i.amountIn` -> `i.exactOut == r.exactOut`) + -> TWO named theorems are proved FALSE by the kernel, not merely + broken: `a_forged_output_is_refused` ("Tactic `decide` proved that + the proposition ... is false") and, with it, + `the_predicate_is_not_the_tautological_one` -- the two forms having + become the same predicate, so their inequality is refutable. An + intent whose output the authenticated state does not reproduce now + passes, because it is compared against the route that asserted it. + `a_disagreeing_output_never_satisfies` additionally loses its proof + (unsolved goals), since `policy` stops being consulted at all. + + 2. SAT.6 removed from the conjunction (`i.feeBps == v.feeBps` dropped) + -> `a_fee_that_is_not_the_vaults_is_refused` is proved FALSE by the + kernel. The trader's signed rate would then stand alone, with the + vault's own fee policy -- the authority -- unconsulted. + + Both mutations were reverted; this file is the unmutated module. + + Per-theorem axiom report (`#print axioms`), so "sorry-free" is not the only + claim being made: + + a_forged_output_is_refused no axioms + the_tautological_form_accepts_the_forgery no axioms + the_predicate_is_not_the_tautological_one no axioms + a_fee_that_is_not_the_vaults_is_refused no axioms + the_honest_case_satisfies no axioms + a_disagreeing_output_never_satisfies propext, Quot.sound + + The counterexamples are closed `decide` terms and carry nothing. Only the + general theorem reaches `simp`, and it takes propositional extensionality and + quotient soundness -- the two standard Lean axioms, neither of which is + `sorryAx`. `decide` is used throughout in preference to `native_decide`, + which would add `Lean.ofReduceBool` and `Lean.trustCompiler` and move the + proof out of the kernel. +-/ + +namespace DSMTradeIntent + +/-- Digests and amounts alike are `Nat`. -/ +abbrev D := Nat + +/-- `0x000B` schema 2 (2c-E §4): the six members the trader signs. + + There is deliberately no `minOut`, `maxFee`, `maxHops`, `maxFanout` or `k`. + Four of them had no source on the wire at all, and a bound read out of the + intent it bounds is not a bound. -/ +structure Intent where + tokenIn : D + amountIn : Nat + tokenOut : D + exactOut : Nat + feeBps : Nat + nonce : D +deriving DecidableEq, Repr + +/-- The canonical `RouteCommit` (version 2) the trader signs with its signature + zeroed. `sigValid` stands for that signature verifying. -/ +structure SignedRoute where + tokenIn : D + amountIn : Nat + tokenOut : D + exactOut : Nat + feeBps : Nat + nonce : D + legCount : Nat + sigValid : Bool +deriving DecidableEq, Repr + +/-- The AUTHENTICATED `V_n` that `c_n` names. The fee here is the vault's own + policy, which is the authority the settle is checked against. -/ +structure VaultState where + feeBps : Nat + reserveIn : Nat + reserveOut : Nat +deriving DecidableEq, Repr + +/-- The legs actually carried in `B.selected_route`. -/ +structure Route where + legCount : Nat +deriving DecidableEq, Repr + +/-- SAT.1-SAT.6 of 2c-E §6. + + `policy` is the market rule evaluated on the AUTHENTICATED state. Passing it + as a parameter is the point: SAT.5's operand must come from somewhere the + route cannot choose. -/ +def satisfies (policy : VaultState → Nat → Nat) + (i : Intent) (r : SignedRoute) (v : VaultState) (rt : Route) : Bool := + r.sigValid -- SAT.2 + && (i.tokenIn == r.tokenIn) -- SAT.3 + && (i.tokenOut == r.tokenOut) + && (i.amountIn == r.amountIn) + && (i.exactOut == r.exactOut) + && (i.feeBps == r.feeBps) + && (i.nonce == r.nonce) + && (rt.legCount == r.legCount) -- SAT.4 + && (i.exactOut == policy v i.amountIn) -- SAT.5 the independent fact + && (i.feeBps == v.feeBps) -- SAT.6 + +/-- THE FORBIDDEN SHAPE, modelled so it can be refuted rather than merely + warned against: SAT.5's operand taken from the route's own claim. Every + other conjunct is identical. -/ +def satisfiesTautological + (i : Intent) (r : SignedRoute) (v : VaultState) (rt : Route) : Bool := + r.sigValid + && (i.tokenIn == r.tokenIn) + && (i.tokenOut == r.tokenOut) + && (i.amountIn == r.amountIn) + && (i.exactOut == r.exactOut) + && (i.feeBps == r.feeBps) + && (i.nonce == r.nonce) + && (rt.legCount == r.legCount) + && (i.exactOut == r.exactOut) -- the route asserting itself + && (i.feeBps == v.feeBps) + +/-- A closed, decidable stand-in for the market rule. Its shape is irrelevant; + what matters is that it reads the AUTHENTICATED state and not the route. -/ +def samplePolicy : VaultState → Nat → Nat := + fun v a => v.reserveOut * a / (v.reserveIn + a) + +/-- The authenticated vault: 30 bps, reserves 1000 / 500. -/ +def vn : VaultState := { feeBps := 30, reserveIn := 1000, reserveOut := 500 } + +/-- `samplePolicy vn 100 = 500 * 100 / 1100 = 45`. -/ +theorem the_authenticated_output_is_fortyfive : samplePolicy vn 100 = 45 := by decide + +def honestRoute : SignedRoute := + { tokenIn := 1, amountIn := 100, tokenOut := 2, exactOut := 45, + feeBps := 30, nonce := 7, legCount := 1, sigValid := true } + +def honestIntent : Intent := + { tokenIn := 1, amountIn := 100, tokenOut := 2, exactOut := 45, + feeBps := 30, nonce := 7 } + +def oneLeg : Route := { legCount := 1 } + +theorem the_honest_case_satisfies : + satisfies samplePolicy honestIntent honestRoute vn oneLeg = true := by decide + +/-- TEETH, and the load-bearing one. The trader signs an output the + authenticated state does not reproduce -- the route and the intent agree + with each other perfectly -- and it is REFUSED. -/ +def forgedIntent : Intent := { honestIntent with exactOut := 400 } +def forgedRoute : SignedRoute := { honestRoute with exactOut := 400 } + +theorem a_forged_output_is_refused : + satisfies samplePolicy forgedIntent forgedRoute vn oneLeg = false := by decide + +/-- NOT VACUOUS. The same forgery PASSES the tautological form. The two + predicates are therefore different predicates, and SAT.5's wording is doing + work rather than restating SAT.3. -/ +theorem the_tautological_form_accepts_the_forgery : + satisfiesTautological forgedIntent forgedRoute vn oneLeg = true := by decide + +theorem the_predicate_is_not_the_tautological_one : + satisfies samplePolicy forgedIntent forgedRoute vn oneLeg + ≠ satisfiesTautological forgedIntent forgedRoute vn oneLeg := by decide + +/-- Each remaining conjunct, separately necessary. -/ +theorem an_unsigned_route_is_refused : + satisfies samplePolicy honestIntent { honestRoute with sigValid := false } vn oneLeg + = false := by decide + +theorem an_intent_naming_another_input_token_is_refused : + satisfies samplePolicy { honestIntent with tokenIn := 99 } honestRoute vn oneLeg + = false := by decide + +theorem an_intent_naming_another_output_token_is_refused : + satisfies samplePolicy { honestIntent with tokenOut := 99 } honestRoute vn oneLeg + = false := by decide + +theorem an_amount_the_trader_did_not_sign_is_refused : + satisfies samplePolicy { honestIntent with amountIn := 101 } honestRoute vn oneLeg + = false := by decide + +theorem a_nonce_the_trader_did_not_sign_is_refused : + satisfies samplePolicy { honestIntent with nonce := 8 } honestRoute vn oneLeg + = false := by decide + +/-- SAT.4. The legs must correspond to the SIGNED hops; this is the check that + replaced schema 1's `max_hops`, and it reads a signed fact rather than a + bound carried in the intent. -/ +theorem a_leg_count_that_is_not_the_signed_one_is_refused : + satisfies samplePolicy honestIntent honestRoute vn { legCount := 2 } + = false := by decide + +/-- SAT.6. The vault's fee is the authority; the signed rate is the trader's + acknowledgement of it, and the two must agree. -/ +theorem a_fee_that_is_not_the_vaults_is_refused : + satisfies samplePolicy { honestIntent with feeBps := 25 } + { honestRoute with feeBps := 25 } vn oneLeg = false := by decide + +/-- The general statement behind the counterexamples: whenever the signed + output disagrees with the policy on the authenticated state, the predicate + is false — for ANY policy, not merely the sample. -/ +theorem a_disagreeing_output_never_satisfies + (policy : VaultState → Nat → Nat) (i : Intent) (r : SignedRoute) + (v : VaultState) (rt : Route) + (h : i.exactOut ≠ policy v i.amountIn) : + satisfies policy i r v rt = false := by + unfold satisfies + have : (i.exactOut == policy v i.amountIn) = false := by + simp [beq_eq_false_iff_ne, h] + simp [this] + +end DSMTradeIntent