From 6e0361f1276e7e59638e6e8996a637ccfee09228 Mon Sep 17 00:00:00 2001 From: Cryptskii <47649969+cryptskii@users.noreply.github.com> Date: Wed, 9 Sep 2026 20:09:59 -0400 Subject: [PATCH] feat(formal): the trade-intent correspondence, and the proof that its forbidden shape is vacuous MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Amendment 2c-E §8.3. The obligation said the formal predicate consuming TradeIntent should be "updated" — there was none. Zero references across lean4/ and tla/, to TradeIntent or to any of the four retired members. So "remove every formal dependency on the retired members" is discharged vacuously, and it is recorded as vacuous in the amendment rather than silently ticked off. The real work was to author the predicate. DSMTradeIntentCorrespondence.lean is the fifteenth module and machine-checks SAT.1 through SAT.6 for the six-field exact-output intent. The market policy is a PARAMETER, so the model fixes no pricing rule, no rounding and no admissibility condition; it proves the SHAPE of the correspondence for any policy. A sample policy exists only to make the counterexamples closed terms the kernel can decide. The load-bearing result is the_tautological_form_accepts_the_forgery. The forbidden shape — SAT.5 compared against the route's own claim instead of the authenticated V_n — ACCEPTS a trade the real predicate refuses. The two are therefore provably different predicates, which is why SAT.5 is worded as it is. That was the specific risk in the ruling: an intent field defined as a function of the selected route makes the satisfaction check a self-attestation. Teeth, one conjunct at a time: an unsigned route, either token swapped, an unsigned amount, an unsigned nonce, a leg count that is not the signed one, and a fee that is not the vault's are each refused separately. The leg-count check is what replaced schema 1's max_hops, and it reads a signed fact rather than a bound carried in the intent it bounds. One general theorem rather than only examples: a disagreeing output never satisfies, for ANY policy. Two mutation controls, executed and reported from the kernel's actual output rather than predicted: - SAT.5's operand replaced by the route's claim turns TWO named theorems FALSE, not merely broken — a_forged_output_is_refused and, with it, the_predicate_is_not_the_tautological_one, since the two forms become one predicate. a_disagreeing_output_never_satisfies additionally loses its proof. - SAT.6 removed turns a_fee_that_is_not_the_vaults_is_refused FALSE. I had predicted the first would merely break the second theorem. The kernel refutes it, which is stronger, and the header now says what the kernel printed. Per-theorem axiom report included. Five results depend on no axioms at all; only the general theorem reaches simp and takes propext and Quot.sound. decide is used throughout rather than native_decide, which would add ofReduceBool and trustCompiler and move the proof out of the kernel. CI module pin 14 -> 15. Two stale live counts corrected; the 2c-C4 history entry saying it landed the fourteenth is left alone, because it records what was true then. All 15 modules kernel-check clean under -DwarningAsError=true, which is what the sorry-free claim rests on. make lint green; production safety checks green. --- .github/workflows/ci.yml | 2 +- .../amendment-2c-c3-valid-dlv-successor.md | 6 +- ...mendment-2c-e-trade-intent-exact-output.md | 18 +- docs/papers/ccb-object-registry.md | 7 +- lean4/DSMTradeIntentCorrespondence.lean | 251 ++++++++++++++++++ 5 files changed, 275 insertions(+), 9 deletions(-) create mode 100644 lean4/DSMTradeIntentCorrespondence.lean 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