import Song.Native.X86.Step /-! # Song's Cell multiplication program: the fixed byte image `CELL-MUL1` as the fixed bytes `4989fa4c0fafd24889f0480fafc14c01d0480faff24889fa480fafd14801f2c3`, 32 bytes, sha256 `18182b7f7526d5625693ed9c6d002f43ca39fe969a06e9a1c7d6ea8cb8334b8a`. That assignment is the one `artifacts/W0-I35/findings.tsv` rows `A01`-`A10` and `IMG-CELL-MUL1` derived, checked against GNU as 2.47 and against the linked static image on that host, and adopted here unchanged so the ledger's own single-instruction controls (`plan/ledger.tsv` row `CELL-MACHINE`, and `W0-I35` `CTL-1`/`CTL-3`) keep landing on `imul rdx, rcx` at image offset 24, its `0F AF` opcode byte at offset 26 and its ModRM byte `D1` at offset 27. The bytes are written here as **data**, not recomputed by the encoder. `W0-I35` `F10` is the reason: `Song.Native.X86.Codec.encodeProgram` composed over `encode` would reproduce this hex by construction, so an encoder round trip is consistency and not evidence. The independent anchor is the literal list `mulImage`, and `mulImage_eq_programBytes` is stated separately as that consistency theorem. The per-instruction table below then reads the *literal* list back through Song's own decoder, which is the direction that can fail. ## Register allocation and the frame it costs `(a0, a1, b0, b1)` arrive in `RDI, RSI, RDX, RCX` and the result returns in `RAX` then `RDX` (the frozen contract, README "Program and ABI"). `R10` is the one scratch the contract names. This allocation also writes `RSI` (row `A06`) and `RDX` (row `A07`), which is permitted only because the psABI makes both caller-saved; `W0-I35` `F06` records it and the classification is tested, not proved. The write set is therefore `{RAX, RSI, RDX, R10}`, not the three registers `W0-I40/F04` proposed for its own candidate body. `Sigma = +1` is absent from the image by being equal to one, not by being ignored: slot 0 is `a0*b0 + a1*b1` and slot 1 is `a0*b1 + a1*b0`, which is the `sigma = +1` specialisation of `ringMul`. Nothing here says anything about `Sigma = -1` or `Sigma = 0`. ## Totality of the image, and the one refusal it admits Every instruction boundary of `mulImage` decodes, with the instruction and the byte count this module's table states. Decoding is *not* total over every offset: `mulImage` is a register-only byte stream, so an offset that is not an instruction boundary lands in the middle of an encoding and may or may not be refused. `mulImage_refuses_at_2` pins one such refusal below the end of the image so the claim cannot be read as global decoder totality. What the trace reaches is the narrower and load-bearing statement: the ten boundaries are all decodable, `RET` is the tenth, and the only refusal a running machine can reach is the fetch past the image end, which `step_refuses_when_done` makes unreachable after `RET`. `Song.Native.Cell.Correct` proves that. -/ namespace Song.Native.Cell.Program open Song.Native.X86 (Ins Reg Word64) open Song.Native.X86.Codec (decode encode) open Song.Native.X86.Step (encodeProgram) /-! ### Decidable equality on the admitted instructions The per-instruction table below is stated as equations over `Option (Ins × Nat)`, so the kernel's `decide` needs a `Decidable` instance on `Ins`, which `Syntax.lean` does not provide (and which this row does not own). `insDecEq` decides by constructor and then field: the four constructors are disjoint, and `Reg = Fin 16` has decidable equality in Lean core. No axiom enters; the `#print axioms` result is recorded in the receipt. -/ /-- Decidable equality on the four admitted instructions, by constructor then field. -/ def insDecEq : (a b : Ins) → Decidable (a = b) | .mov d s, .mov d' s' => decidable_of_iff (d = d' ∧ s = s') (by constructor · intro h rw [h.1, h.2] · intro h cases h exact ⟨rfl, rfl⟩) | .imul d s, .imul d' s' => decidable_of_iff (d = d' ∧ s = s') (by constructor · intro h rw [h.1, h.2] · intro h cases h exact ⟨rfl, rfl⟩) | .add d s, .add d' s' => decidable_of_iff (d = d' ∧ s = s') (by constructor · intro h rw [h.1, h.2] · intro h cases h exact ⟨rfl, rfl⟩) | .ret, .ret => isTrue rfl | .mov _ _, .imul _ _ => isFalse (fun h => by cases h) | .mov _ _, .add _ _ => isFalse (fun h => by cases h) | .mov _ _, .ret => isFalse (fun h => by cases h) | .imul _ _, .mov _ _ => isFalse (fun h => by cases h) | .imul _ _, .add _ _ => isFalse (fun h => by cases h) | .imul _ _, .ret => isFalse (fun h => by cases h) | .add _ _, .mov _ _ => isFalse (fun h => by cases h) | .add _ _, .imul _ _ => isFalse (fun h => by cases h) | .add _ _, .ret => isFalse (fun h => by cases h) | .ret, .mov _ _ => isFalse (fun h => by cases h) | .ret, .imul _ _ => isFalse (fun h => by cases h) | .ret, .add _ _ => isFalse (fun h => by cases h) instance instDecidableEqIns : DecidableEq Ins := insDecEq /-! ### Named registers The architectural numbering is the model's: `Reg` is `Fin 16`, so `r8` through `r15` are 8 through 15 and need the REX extension bit. The names exist so a theorem can say which argument register and which result register it means. -/ /-- `RAX`, register 0. First result word of the return pair. -/ def rax : Reg := 0 /-- `RCX`, register 1. Carries `b1` on entry. -/ def rcx : Reg := 1 /-- `RDX`, register 2. Carries `b0` on entry and the second result word on exit. -/ def rdx : Reg := 2 /-- `RSI`, register 6. Carries `a1` on entry and is written by the third product. -/ def rsi : Reg := 6 /-- `RDI`, register 7. Carries `a0` on entry. -/ def rdi : Reg := 7 /-- `R10`, register 10. The scratch register the frozen contract names. -/ def r10 : Reg := 10 /-- `RAX` is register 0. -/ theorem rax_val : rax.val = 0 := rfl /-- `RCX` is register 1. -/ theorem rcx_val : rcx.val = 1 := rfl /-- `RDX` is register 2. -/ theorem rdx_val : rdx.val = 2 := rfl /-- `RSI` is register 6. -/ theorem rsi_val : rsi.val = 6 := rfl /-- `RDI` is register 7. -/ theorem rdi_val : rdi.val = 7 := rfl /-- `R10` is register 10. -/ theorem r10_val : r10.val = 10 := rfl /-! ### The body, as admitted instructions -/ /-- The ten instructions of `CELL-MUL1`, in image order. Each line names the offset its encoding occupies in `mulImage` and the `W0-I35` row that derived the bytes. * `0` `mov r10, rdi` (`A01`, `49 89 fa`) * `3` `imul r10, rdx` (`A02`, `4c 0f af d2`), the product `a0*b0` * `7` `mov rax, rsi` (`A03`, `48 89 f0`) * `10` `imul rax, rcx` (`A04`, `48 0f af c1`), the product `a1*b1` * `14` `add rax, r10` (`A05`, `4c 01 d0`), slot 0 is complete here * `17` `imul rsi, rdx` (`A06`, `48 0f af f2`), the product `a1*b0` * `21` `mov rdx, rdi` (`A07`, `48 89 fa`), `b0` is dead and `RDX` is recycled * `24` `imul rdx, rcx` (`A08`, `48 0f af d1`), the product `a0*b1` * `28` `add rdx, rsi` (`A09`, `48 01 f2`), slot 1 is complete here * `31` `ret` (`A10`, `c3`) Two operand orders are opposite and both are correct on hardware: `MOV` and `ADD` carry their destination in the ModRM `r/m` field, `IMUL` in the ModRM `reg` field. `Song.Native.X86.Ins` documents the split and the encoder in `Codec.lean` implements it. -/ def mulBody : List Ins := [ .mov 10 7, -- A01 mov r10, rdi .imul 10 2, -- A02 imul r10, rdx p00 = a0*b0 .mov 0 6, -- A03 mov rax, rsi .imul 0 1, -- A04 imul rax, rcx p11 = a1*b1 .add 0 10, -- A05 add rax, r10 slot0 = a0*b0 + a1*b1 .imul 6 2, -- A06 imul rsi, rdx p10 = a1*b0 .mov 2 7, -- A07 mov rdx, rdi .imul 2 1, -- A08 imul rdx, rcx p01 = a0*b1 .add 2 6, -- A09 add rdx, rsi slot1 = a0*b1 + a1*b0 .ret ] -- A10 ret /-- The image length in instructions. `mulBody` has exactly one `RET` and ten entries. -/ def bodyLength : Nat := 10 /-- `mulBody` has ten instructions. -/ theorem mulBody_length : mulBody.length = bodyLength := by decide /-- The byte image of a program: instructions encoded in order, no labels, no alignment, no relocation. README names this interface `program_bytes`; `Song.Native.X86.Step` already defines the same function as `encodeProgram` and `W0-I40/F05` records that one of the two names should be retired. This is an `abbrev`, so there is one definition and two names, and `programBytes_eq_encodeProgram` states that; retiring one is a lead decision, recorded in the receipt rather than taken here. -/ abbrev programBytes (p : List Ins) : List UInt8 := encodeProgram p /-- The two names for the byte image of a program are the same function. -/ theorem programBytes_eq_encodeProgram (p : List Ins) : programBytes p = encodeProgram p := rfl /-! ### The image, as fixed data -/ /-- `CELL-MUL1` as the fixed 32 bytes. This literal is the anchor; the encoder is checked against it, never the other way round. -/ def mulImage : List UInt8 := [ 0x49, 0x89, 0xFA, 0x4C, 0x0F, 0xAF, 0xD2, 0x48, 0x89, 0xF0, 0x48, 0x0F, 0xAF, 0xC1, 0x4C, 0x01, 0xD0, 0x48, 0x0F, 0xAF, 0xF2, 0x48, 0x89, 0xFA, 0x48, 0x0F, 0xAF, 0xD1, 0x48, 0x01, 0xF2, 0xC3 ] /-- The image is 32 bytes. -/ theorem mulImage_length : mulImage.length = 32 := by decide /-- The fixed bytes are what Song's own encoder produces for `mulBody`. This is consistency between two artifacts, and it is the direction that is *not* evidence: `W0-I35/F10`. The evidence direction is the per-instruction table below, which reads `mulImage` back. -/ theorem mulImage_eq_programBytes : mulImage = programBytes mulBody := by decide /-! ### Instruction boundaries and the byte counts `mulRip i` is where the `i`-th transition fetches from: the length of the encoder's output for the first `i` instructions. It is *defined* from the encoder, so it cannot drift from `mulBody`; the theorem below states that the ten values are the offsets the fixed bytes actually show. -/ /-- The fetch offset of transition `i`, derived from the encoder. -/ def mulRip (i : Nat) : Nat := ((mulBody.take i).flatMap encode).length /-- The ten instruction offsets of the fixed image: the entry offset `0`, the nine interior boundaries, and the image end. `mulRip 0` is the entry, `mulRip 1` through `mulRip 9` are the boundaries the transitions fetch from, and `mulRip 10` is the byte after the image. -/ theorem mulRip_table : (List.range 11).map mulRip = [0, 3, 7, 10, 14, 17, 21, 24, 28, 31, 32] := by decide /-- The tenth fetch offset is the end of the image, which is where `RET` sits. -/ theorem mulRip_end : mulRip bodyLength = mulImage.length := by decide /-! ### The per-instruction decode table Ten equations, one per instruction boundary, each read out of the literal `mulImage` through `Song.Native.X86.Codec.decode`. They are the form of the claim that can fail: the encoder control `W0-I35/CTL-1` turns the `0xAF` at offset 26 into `0x01`, and row `mulImage_decode_6` stops holding with `none` in place of a `some`. -/ /-- Offset 0: `mov r10, rdi`, `49 89 fa`, three bytes. -/ theorem mulImage_decode_0 : decode (mulImage.drop 0) = some (.mov 10 7, 3) := by decide /-- Offset 3: `imul r10, rdx`, `4c 0f af d2`, four bytes. -/ theorem mulImage_decode_1 : decode (mulImage.drop 3) = some (.imul 10 2, 4) := by decide /-- Offset 7: `mov rax, rsi`, `48 89 f0`, three bytes. -/ theorem mulImage_decode_2 : decode (mulImage.drop 7) = some (.mov 0 6, 3) := by decide /-- Offset 10: `imul rax, rcx`, `48 0f af c1`, four bytes. -/ theorem mulImage_decode_3 : decode (mulImage.drop 10) = some (.imul 0 1, 4) := by decide /-- Offset 14: `add rax, r10`, `4c 01 d0`, three bytes. -/ theorem mulImage_decode_4 : decode (mulImage.drop 14) = some (.add 0 10, 3) := by decide /-- Offset 17: `imul rsi, rdx`, `48 0f af f2`, four bytes. -/ theorem mulImage_decode_5 : decode (mulImage.drop 17) = some (.imul 6 2, 4) := by decide /-- Offset 21: `mov rdx, rdi`, `48 89 fa`, three bytes. -/ theorem mulImage_decode_6 : decode (mulImage.drop 21) = some (.mov 2 7, 3) := by decide /-- Offset 24: `imul rdx, rcx`, `48 0f af d1`, four bytes. The instruction both ledger controls mutate. -/ theorem mulImage_decode_7 : decode (mulImage.drop 24) = some (.imul 2 1, 4) := by decide /-- Offset 28: `add rdx, rsi`, `48 01 f2`, three bytes. -/ theorem mulImage_decode_8 : decode (mulImage.drop 28) = some (.add 2 6, 3) := by decide /-- Offset 31: `ret`, `c3`, one byte. -/ theorem mulImage_decode_9 : decode (mulImage.drop 31) = some (.ret, 1) := by decide /-! ### Totality of the image -/ /-- Every instruction boundary of the image decodes. The boundaries are the values `mulRip 0` through `mulRip 10`, which `mulRip_table` gives as `0, 0, 3, 7, 10, 14, 17, 21, 24, 28, 31`: the entry offset, then the nine interior boundaries, then the image end. This is per-instruction totality and it is not global decoder totality: `mulImage_refuses_at_2` and `mulImage_refuses_at_5` pin two offsets *inside* the image that are not boundaries and are refused. The trace visits boundaries and nothing else, which is why this is the totality claim the image needs. -/ theorem mulImage_decodes_at_rip : ∀ i : Nat, i < bodyLength → (decode (mulImage.drop (mulRip i))).isSome = true := by decide /-- The image's last instruction is `RET`, so the tenth transition is the near return and the image has nothing after it. -/ theorem mulImage_ends_with_ret : decode (mulImage.drop 31) = some (.ret, 1) := mulImage_decode_9 /-- Past the end of the image the decoder refuses. This is the single refusal the admitted trace can reach, and `Song.Native.Cell.Correct.mulBody_reaches_ret` shows the trace never takes it because `done` is already set. -/ theorem mulImage_end_refuses : decode (mulImage.drop mulImage.length) = none := by decide /-- Decoding is not total over *all* offsets: offset 2 is the `0xfa` ModRM byte of the first `mov` read as an opcode, which is outside the admitted set. Stated so that `mulImage_decodes_below` cannot be read as global decoder totality, and it is the negative witness that the table is a table of boundaries rather than a claim about the byte string. -/ theorem mulImage_refuses_at_2 : decode (mulImage.drop 2) = none := by decide /-- Offset 1 is inside the first `mov` and is **refused**: the `0x89` there is read as an opcode but the stream carries no `REX.W` prefix, and `Codec.decode` requires that prefix on every admitted arithmetic form, so the operand width is never assumed. On hardware `89 /r` without `REX` is the 32-bit `MOV`, a different instruction at a different width, and this slice admits only the 64-bit form — so the decoder returns `none` rather than reporting a width it did not read. This is the pair with `mulImage_refuses_at_2` above, and the pair is what keeps the boundary totality claim honest: both mid-stream offsets are refused, for two different named reasons — offset 2 is `0xfa` read as an opcode outside the admitted set, offset 1 is an admitted opcode with absent operand width. Neither reason is a fallback. It was `some (.mov 2 7, 3)` before the decoder required the width marker; the row `STRICT-WIDTH-DECODE` inverted it. -/ theorem mulImage_decodes_at_1 : decode (mulImage.drop 1) = none := by decide /-- Offset 5 is `0xaf` read as an opcode, likewise outside the admitted set. -/ theorem mulImage_refuses_at_5 : decode (mulImage.drop 5) = none := by decide /-! ### The shape of the body, stated as equations Each predicate enumerates all four `Ins` constructors. A catch-all `_` case compiles through a path that carries `propext`, and the native audit rule is a literally empty cone, so the exhaustive form is the one that can be certified. This was found by `gate audit` refusing `mulBody_four_imuls`, not by inspection. -/ /-- Is this instruction a `mov`? -/ def isMov : Ins → Bool | .mov _ _ => true | .imul _ _ => false | .add _ _ => false | .ret => false /-- Is this instruction an `imul`? -/ def isImul : Ins → Bool | .mov _ _ => false | .imul _ _ => true | .add _ _ => false | .ret => false /-- Is this instruction an `add`? -/ def isAdd : Ins → Bool | .mov _ _ => false | .imul _ _ => false | .add _ _ => true | .ret => false /-- Is this instruction a `ret`? -/ def isRet : Ins → Bool | .mov _ _ => false | .imul _ _ => false | .add _ _ => false | .ret => true /-- The destination of an `imul`, zero for anything else. Only applied to filtered instructions. -/ def imulDst : Ins → Nat | .mov _ _ => 0 | .imul d _ => d.val | .add _ _ => 0 | .ret => 0 /-- `mulBody` holds exactly four `imul` instructions. This is the frozen slice, not an optimisation: `W0-I35/F04`. `isImul` and its three siblings below enumerate all four constructors rather than using a catch-all `_`. That is not style: a wildcard case in a `match` over `Ins` brings `propext` into the definition, and `gate audit --mode native` refuses a nonempty cone on a native root. An exhaustive match compiles to the recursor alone and has an empty cone. Measured, both forms, on this file. -/ theorem mulBody_four_imuls : (mulBody.filter isImul).length = 4 := by decide /-- The four products go into four *distinct* registers, which is what "four independent `IMUL`s" means here: no accumulator is reused and no product is added into another. -/ theorem mulBody_imul_dsts : (mulBody.filter isImul).map imulDst = [10, 0, 6, 2] := by decide /-- Three `mov` instructions: the three preloads of a scratch or an accumulator. The width-64 policy is in the bytes as well as in the statement (`W0-I35/F01`), since every binary form carries a `REX.W` prefix. -/ theorem mulBody_mov_count : (mulBody.filter isMov).length = 3 := by decide /-- Exactly two `add` instructions, one per slot. -/ theorem mulBody_add_count : (mulBody.filter isAdd).length = 2 := by decide /-- Exactly one `ret`. -/ theorem mulBody_ret_count : (mulBody.filter isRet).length = 1 := by decide /-- Exactly one `ret`, and it is the last instruction. -/ theorem mulBody_ret_last : mulBody.reverse.head? = some (.ret : Ins) := by decide /-- The registers this body writes: `R10`, `RAX`, `RSI`, `RDX`. `RDI`, `RSI`'s value is overwritten by `A06` and `RDX`'s by `A07`, so all three of those are written; the callee-saved `RBX`, `RBP`, `RSP`, `R12`-`R15` are not, which is the psABI frame obligation satisfied by construction rather than by assertion. -/ def writeSet : List Reg := [r10, rax, rsi, rdx] /-- The write set is the four registers the body actually writes, by number. -/ theorem writeSet_val : writeSet.map (fun r => r.val) = [10, 0, 6, 2] := by decide /-- The register an instruction writes, or `none` for `ret` which names none. -/ def writeDest : Ins → Option Reg | .mov d _ => some d | .imul d _ => some d | .add d _ => some d | .ret => none /-- `mulBody` writes nothing outside `writeSet`: every destination the body names is a member. This is the frame obligation of the ABI contract as an equation over the admitted instructions, not as an assertion about a caller. -/ theorem mulBody_writes_subset_writeSet : ∀ d : Option Reg, d ∈ (mulBody.map writeDest).eraseDups → d = none ∨ d = some rax ∨ d = some rdx ∨ d = some rsi ∨ d = some r10 := by decide /-- The exact multiset of destinations, in image order: `R10, R10, RAX, RAX, RAX, RSI, RDX, RDX, RDX`, then the `ret`. `RSI` and `RDX` are *argument* registers and this allocation writes both, which is admissible only because the psABI makes them caller-saved (`W0-I35/F06`). -/ theorem mulBody_write_dests : mulBody.map writeDest = [some 10, some 10, some 0, some 0, some 0, some 6, some 2, some 2, some 2, none] := by decide end Song.Native.Cell.Program