import Song.Native.Cell.Program
import Song.Native.Cell.Word

/-!
# Song's Cell multiplication: execution from the fixed byte image

This is the `CELL-MACHINE` row: the theorems that say what the fixed bytes of
`Song.Native.Cell.Program.mulImage` *do*, read through Song's own decoder and stepper. Not what
a processor does, and not what bytes any caller jumped into.

Three links are kept apart, as `README.md` requires.

1. **Canonical denotation.** `mulBody_cellMul` names the result as
   `cellMul1 (a0, a1) (b0, b1)`, `Song.Native.Cell.cellMul1`, which is `ringMul` at `sigma = +1`
   over wrapping 64-bit words. The relation to `Apeiron.Trichotomy.AnyRing` is
   `Song.Canonical.CellBridge`'s and is not touched here.
2. **Resource model.** `mulBody_decided` charges ten transitions, ten instruction fetches, four
   64-bit multiplies, two 64-bit adds and **one data-memory read**: the `RET` at the tenth
   transition reads the return slot at `retAddr`. `mulBody_no_memory` says the admitted ISA has no
   memory operands, so that read is the only memory access this image can make, and the frame
   obligation the accepted row had to state as *vacuous* is now stated as a theorem:
   `mulBody_preserves_memory` says the ten transitions leave every coordinate of the data memory
   exactly as they found it, and `mulBody_ret_slot` says the word `RET` read is still in the slot
   afterwards. The psABI frame obligation is a test against a C caller (`native/cell_fixture.c`),
   not this file.
3. **Actual machine transition.** `step` is `Song.Native.X86.Step.step` over
   `Song.Native.X86.Codec.decode`. Hardware correspondence stays a disclosed assumption with the
   Intel SDM section and the K x86 revision as differential references (`README.md`, machine
   model row).

## What is proved for all inputs and what only for witnesses

`mulBody_correct` is the general statement: for *every* `a0 a1 b0 b1 slot`, ten transitions from
`mulInit` reach `RET` with `RAX` and `RDX` holding the two cell slots and every other register
holding its entry value. It is proved by chaining the ten `step_*` transition laws of
`Step.lean`, each fed by one row of `Program.lean`'s per-instruction decode table. It is not a
`decide` over a finite input set and it does not quantify over `Word64` arithmetically: the
`Fin` operations are opaque, so the arithmetic clauses are equalities between `Fin` expressions
and are closed by `rfl`.

`mulBody_reaches_ret`, `mulBody_frame`, `mulBody_cellMul`, `mulBody_preserves_memory` and
`mulBody_ret_slot` are corollaries of the same trace equation and hold for all inputs too. The five
witness theorems at the end additionally *evaluate* the arithmetic, so they are the concrete
instances; each one is decided by the kernel on the concrete `Fin` values.

## What admitting data memory changed here, clause by clause

`State.retSlot` and `State.retVal` are retired and `step` returns `Outcome State Refusal`
(`artifacts/MEMORY-ADMIT/receipt.txt`). Nothing is dropped and no claim is widened; the transfer is
the one `artifacts/W0-I46/receipt.txt` §4.1 freezes, applied to this module's statements:

* the ten transition laws `step0` .. `step9` conclude `= .next …` where the accepted ones concluded
  `= some …`, because that is `step`'s codomain now;
* the accepted `mulBody_ret_slot` conclusion `(runN …).map State.retVal = some slot` — the retired
  `retVal := retSlot` clause — becomes the **two** conjuncts `Step.step_ret_preserves_memory` names:
  the successor's memory is the pre-state's memory, and the coordinate still reads `some (.live
  slot)` for the word that was read. The `RET` read is therefore still the value in the slot and
  nothing moved, which is what the retired clause asserted, with the field copy replaced by the
  memory it read from;
* `mulBody_stops` now **names** its refusal, `.halted`, where the accepted form said `none`. This
  is an addition, not a change of claim;
* `mulBody_not_done_before_ret`'s second conjunct was `(s9 …).retVal = 0`. That is a statement
  about a field the trace never wrote and the new state does not have, so it cannot be carried; it
  becomes `(s9 …).mem = (mulInit …).mem`, and that is **strictly weaker**: nothing in the new state
  records how many times `RET` has read memory. It is a forced weakening, recorded in
  `artifacts/CELL-MEMORY-REBASE/findings.tsv` rather than absorbed, and it is what the two memory
  refusals below exist to bound.

`mulInit` is the named initial memory this slice claims (`W0-I46` §7.7 assigns it here): one `.live`
slot at coordinate `retAddr = 0`, and nothing else. `mulBody_ret_uninit_refuses` and
`mulBody_ret_unowned_refuses` say the tenth transition REFUSES on the same nine-transition state
when that slot is `.uninit` or `.unowned`, and name the two different memory reasons, so the
liveness in `mulInit_entry` is an attribute the trace needs rather than a formality.

## The negative witnesses are load-bearing, not decoration

* `(2,3)*(5,7) = (31,29)` is asymmetric, so it detects a slot transposition and a swap of two
  argument registers. A symmetric witness cannot (`W0-I36` section 6(a) measured this: only the
  asymmetric case went red).
* `(0,0)` and `2^63 * 2 = 0` are the reachable success and wrap cases, and `(1,0)*(0,1) = (0,1)`
  shows the slot order is not a symmetry of the inputs either.
* `max^2 = (2,2)` exercises the wrap of both slots at once.

## Honest limits, all exclusions of `README.md` "Order"

Flags are absent from the state and no flag postcondition is claimed (`ISA-CORE` R3). General
`Sigma`, division, memory operands, ELF verification, `CALL` stacks and general associativity of
`cellMul1` are outside this slice. `mulImage_eq_programBytes` in `Program.lean` is consistency
between two artifacts, not evidence that these are the bytes an assembler emits or that a
processor executes them; the executed-image identity gate remains `MISSING` in `tools/gate.c`.
-/

namespace Song.Native.Cell.Correct

open Song.Native.X86 (Ins Reg Word64 setReg setReg_self setReg_of_ne)
open Song.Native.X86.Codec (decode)
open Song.Native.X86.Memory (Addr Slot Fault Outcome)
open Song.Native.X86.Step
  (State step fetch step_mov step_imul step_add step_ret step_ret_refused Refusal)
open Song.Native.Cell.Program
open Song.Native.Cell.Program (isMov isImul isAdd isRet)
open Song.Native.Cell (Cell64 cellMul1 cellOfNat)

/-! ### Entry state and the trace -/

/-- `runN n σ` applies `step` `n` times. `none` at any point is a refusal and ends the trace.
The recursion is on `n`, so `runN 0` is the identity and no trace can be infinite.

`step` now returns `Outcome State Refusal` rather than `Option State`, so this match has two
refusing arms to write: a refusal ends the trace with `none`, and the reason it ended with is
*dropped here on purpose*. `W0-I46` §4.4 gives the reason-carrying port for the machine-level
witnesses and names it a deviation; the trace-level statements accepted by `CELL-MACHINE`
(`mulBody_total`, `mulBody_one_past_end` and the five concrete witnesses) are equations over this
`Option`, and the frozen plan names no change to them. The reason is instead carried where it is
produced: `mulBody_stops` names `halted` after the return, and `mulBody_ret_uninit_refuses` and
`mulBody_ret_unowned_refuses` name the two memory reasons at the tenth transition. -/
def runN : Nat → State → Outcome State Refusal
  | 0, σ => .next σ
  | n + 1, σ =>
      match step σ with
      | .next σ' => runN n σ'
      | .refused τ r => .refused τ r

/-- The entry state of the cell leaf: `RDI = a0`, `RSI = a1`, `RDX = b0`, `RCX = b1`, every other
register `0`, `rip = 0`, the fixed image as the code, and the fixed return word `slot` as the ONE
`.live` slot of the admitted data memory, read by `RET` at coordinate `retAddr = 0`.

This is a **fixture definition, not an ABI theorem** (`W0-I40/F06`, `W0-I40/F25`). Nothing here
says a C caller produces this state. What the SysV AMD64 psABI actually does with four
`uint64_t` words is tested against a C caller in `native/cell_fixture.c`, because Song's Lean
tree contains no psABI model to decide anything about.

`mem := ⟨[Slot.live slot]⟩` is `Memory.memInit [slot]`: `W0-I46` §4.2 maps the retired `retSlot`
field onto `mem.slotAt retAddr` admitted as `some (.live w)`, and says the Cell slice's named
initial memory is this row's obligation rather than the memory row's. `retAddr := 0` is a constant
of the initial state and not a computed address: the admitted slice has no stack pointer, no frame
and no `CALL` (`ISA-CORE` R4). The two `.unowned`/`.uninit` memory reasons are exercised by
`mulBody_ret_unowned_refuses` and `mulBody_ret_uninit_refuses` below, so the `.live` here is
observable rather than decorative. -/
def mulInit (a0 a1 b0 b1 slot : Word64) : State where
  rip := 0
  regs := fun r =>
    if r.val = 7 then a0
    else if r.val = 6 then a1
    else if r.val = 2 then b0
    else if r.val = 1 then b1
    else 0
  code := mulImage
  mem := ⟨[Slot.live slot]⟩
  retAddr := 0
  done := false

/-- A fetch at an offset of the fixed image, given that the state's code is the image and its
`rip` is that offset. Every use below feeds it one row of `Program.mulImage_decode_0` to
`mulImage_decode_9`, so the decoder is what names each instruction. -/
theorem fetch_of {σ : State} {k : Nat} {i : Ins} {n : Nat}
    (hcode : σ.code = mulImage) (hrip : σ.rip = k)
    (hdec : decode (mulImage.drop k) = some (i, n)) : fetch σ = some (i, n) := by
  rw [fetch, hcode, hrip, hdec]

/-! ### The ten intermediate states

Each is the state after one transition. They are named rather than inlined so that each step law
can be stated and proved on its own, and so a reader can see which instruction each transition is. -/

/-- After `mov r10, rdi`. -/
def s1 (a0 a1 b0 b1 slot : Word64) : State :=
  { mulInit a0 a1 b0 b1 slot with
      rip := 3
      regs := setReg (mulInit a0 a1 b0 b1 slot).regs r10 a0 }

/-- After `imul r10, rdx`: `R10 = a0*b0`, the first of the four products. -/
def s2 (a0 a1 b0 b1 slot : Word64) : State :=
  { s1 a0 a1 b0 b1 slot with
      rip := 7
      regs := setReg (s1 a0 a1 b0 b1 slot).regs r10 (a0 * b0) }

/-- After `mov rax, rsi`: the slot-0 accumulator starts from `a1`. -/
def s3 (a0 a1 b0 b1 slot : Word64) : State :=
  { s2 a0 a1 b0 b1 slot with
      rip := 10
      regs := setReg (s2 a0 a1 b0 b1 slot).regs rax a1 }

/-- After `imul rax, rcx`: `RAX = a1*b1`. -/
def s4 (a0 a1 b0 b1 slot : Word64) : State :=
  { s3 a0 a1 b0 b1 slot with
      rip := 14
      regs := setReg (s3 a0 a1 b0 b1 slot).regs rax (a1 * b1) }

/-- After `add rax, r10`: slot 0 is complete, `RAX = a1*b1 + a0*b0`. -/
def s5 (a0 a1 b0 b1 slot : Word64) : State :=
  { s4 a0 a1 b0 b1 slot with
      rip := 17
      regs := setReg (s4 a0 a1 b0 b1 slot).regs rax (a1 * b1 + a0 * b0) }

/-- After `imul rsi, rdx`: `RSI = a1*b0`, the third product, into a register that is dead after. -/
def s6 (a0 a1 b0 b1 slot : Word64) : State :=
  { s5 a0 a1 b0 b1 slot with
      rip := 21
      regs := setReg (s5 a0 a1 b0 b1 slot).regs rsi (a1 * b0) }

/-- After `mov rdx, rdi`: `b0` is dead and `RDX` is recycled to hold `a0`. -/
def s7 (a0 a1 b0 b1 slot : Word64) : State :=
  { s6 a0 a1 b0 b1 slot with
      rip := 24
      regs := setReg (s6 a0 a1 b0 b1 slot).regs rdx a0 }

/-- After `imul rdx, rcx`: `RDX = a0*b1`, the fourth product. This is the instruction
`imul rdx, rcx` that `plan/ledger.tsv` row `CELL-MACHINE` mutates. -/
def s8 (a0 a1 b0 b1 slot : Word64) : State :=
  { s7 a0 a1 b0 b1 slot with
      rip := 28
      regs := setReg (s7 a0 a1 b0 b1 slot).regs rdx (a0 * b1) }

/-- After `add rdx, rsi`: slot 1 is complete, `RDX = a0*b1 + a1*b0`. -/
def s9 (a0 a1 b0 b1 slot : Word64) : State :=
  { s8 a0 a1 b0 b1 slot with
      rip := 31
      regs := setReg (s8 a0 a1 b0 b1 slot).regs rdx (a0 * b1 + a1 * b0) }

/-- The final register file, written as the exact nested `setReg` chain the ten transitions
build, so that each register read is a single `rfl` and the frame theorem's statement is legible.

The chain keeps every intermediate write, including the ones a later write overwrites: the
`mov r10, rdi` at offset 0 is followed by the `imul r10, rdx` at offset 3 into the same register,
and both `setReg`s are here. Collapsing them would be a different term, so it is not done.
`RAX` is slot 0, `RDX` is slot 1, and `R10` and `RSI` hold dead scratch values. -/
def mulFinalRegs (a0 a1 b0 b1 slot : Word64) : Reg → Word64 :=
  let e0 := (mulInit a0 a1 b0 b1 slot).regs
  let e1 := setReg e0 r10 a0
  let e2 := setReg e1 r10 (a0 * b0)
  let e3 := setReg e2 rax a1
  let e4 := setReg e3 rax (a1 * b1)
  let e5 := setReg e4 rax (a1 * b1 + a0 * b0)
  let e6 := setReg e5 rsi (a1 * b0)
  let e7 := setReg e6 rdx a0
  let e8 := setReg e7 rdx (a0 * b1)
  setReg e8 rdx (a0 * b1 + a1 * b0)

/-- The register file this module names is the one the trace actually produces. -/
theorem mulFinalRegs_eq (a0 a1 b0 b1 slot : Word64) :
    mulFinalRegs a0 a1 b0 b1 slot = (s9 a0 a1 b0 b1 slot).regs := rfl

/-- The state the trace reaches: `rip` at the end of the image, the final register file, the
memory unchanged, and the stop flag set. The accepted form also wrote `retVal := slot`; that field
is retired, and the word `RET` read is recovered from the successor state by one `Mem.slotAt` at
`retAddr`, which is what `mulBody_ret_slot` states. -/
def mulResult (a0 a1 b0 b1 slot : Word64) : State :=
  { s9 a0 a1 b0 b1 slot with
    rip := mulImage.length
    regs := mulFinalRegs a0 a1 b0 b1 slot
    done := true }

/-! ### The ten transitions

Each law concludes `= .next …`: `step` returns `Outcome State Refusal`, so the accepted `= some …`
conclusions are restated in the landed codomain and the statements are otherwise the same ten. -/

theorem step0 (a0 a1 b0 b1 slot : Word64) :
    step (mulInit a0 a1 b0 b1 slot) = .next (s1 a0 a1 b0 b1 slot) := by
  rw [step_mov _ 10 7 3 rfl (fetch_of rfl rfl mulImage_decode_0)]
  rfl

theorem step1 (a0 a1 b0 b1 slot : Word64) :
    step (s1 a0 a1 b0 b1 slot) = .next (s2 a0 a1 b0 b1 slot) := by
  rw [step_imul _ 10 2 4 rfl (fetch_of rfl rfl mulImage_decode_1)]
  rfl

theorem step2 (a0 a1 b0 b1 slot : Word64) :
    step (s2 a0 a1 b0 b1 slot) = .next (s3 a0 a1 b0 b1 slot) := by
  rw [step_mov _ 0 6 3 rfl (fetch_of rfl rfl mulImage_decode_2)]
  rfl

theorem step3 (a0 a1 b0 b1 slot : Word64) :
    step (s3 a0 a1 b0 b1 slot) = .next (s4 a0 a1 b0 b1 slot) := by
  rw [step_imul _ 0 1 4 rfl (fetch_of rfl rfl mulImage_decode_3)]
  rfl

theorem step4 (a0 a1 b0 b1 slot : Word64) :
    step (s4 a0 a1 b0 b1 slot) = .next (s5 a0 a1 b0 b1 slot) := by
  rw [step_add _ 0 10 3 rfl (fetch_of rfl rfl mulImage_decode_4)]
  rfl

theorem step5 (a0 a1 b0 b1 slot : Word64) :
    step (s5 a0 a1 b0 b1 slot) = .next (s6 a0 a1 b0 b1 slot) := by
  rw [step_imul _ 6 2 4 rfl (fetch_of rfl rfl mulImage_decode_5)]
  rfl

theorem step6 (a0 a1 b0 b1 slot : Word64) :
    step (s6 a0 a1 b0 b1 slot) = .next (s7 a0 a1 b0 b1 slot) := by
  rw [step_mov _ 2 7 3 rfl (fetch_of rfl rfl mulImage_decode_6)]
  rfl

theorem step7 (a0 a1 b0 b1 slot : Word64) :
    step (s7 a0 a1 b0 b1 slot) = .next (s8 a0 a1 b0 b1 slot) := by
  rw [step_imul _ 2 1 4 rfl (fetch_of rfl rfl mulImage_decode_7)]
  rfl

theorem step8 (a0 a1 b0 b1 slot : Word64) :
    step (s8 a0 a1 b0 b1 slot) = .next (s9 a0 a1 b0 b1 slot) := by
  rw [step_add _ 2 6 3 rfl (fetch_of rfl rfl mulImage_decode_8)]
  rfl

theorem step9 (a0 a1 b0 b1 slot : Word64) :
    step (s9 a0 a1 b0 b1 slot) = .next (mulResult a0 a1 b0 b1 slot) := by
  rw [step_ret _ 1 rfl (fetch_of rfl rfl mulImage_decode_9) (w := slot) rfl]
  rfl

/-! ### The trace theorem, for all inputs -/

/-- `mulBody_correct`: for every four input words and every return slot word, ten transitions from
`mulInit` reach `mulResult`. This is the whole execution claim and it is general: nothing here
restricts `a0 a1 b0 b1 slot`, and no arithmetic is decided, so the statement is an equality between
`Fin (2^64)` expressions.

The theorem stops after the `RET` transition. The coordinate the return slot holds is not a machine
address in this model, because nothing here computes one: the admitted slice has no stack pointer,
no frame and no `CALL`, so `retAddr` is a constant of the entry state (`ISA-CORE` R4). -/
theorem mulBody_correct (a0 a1 b0 b1 slot : Word64) :
    runN bodyLength (mulInit a0 a1 b0 b1 slot) = .next (mulResult a0 a1 b0 b1 slot) := by
  change runN 10 (mulInit a0 a1 b0 b1 slot) = _
  unfold runN
  rw [step0]
  show runN 9 (s1 a0 a1 b0 b1 slot) = _
  unfold runN
  rw [step1]
  show runN 8 (s2 a0 a1 b0 b1 slot) = _
  unfold runN
  rw [step2]
  show runN 7 (s3 a0 a1 b0 b1 slot) = _
  unfold runN
  rw [step3]
  show runN 6 (s4 a0 a1 b0 b1 slot) = _
  unfold runN
  rw [step4]
  show runN 5 (s5 a0 a1 b0 b1 slot) = _
  unfold runN
  rw [step5]
  show runN 4 (s6 a0 a1 b0 b1 slot) = _
  unfold runN
  rw [step6]
  show runN 3 (s7 a0 a1 b0 b1 slot) = _
  unfold runN
  rw [step7]
  show runN 2 (s8 a0 a1 b0 b1 slot) = _
  unfold runN
  rw [step8]
  show runN 1 (s9 a0 a1 b0 b1 slot) = _
  unfold runN
  rw [step9]
  rfl

/-- The trace is total for exactly `bodyLength` transitions, and never refuses: `mulBody_correct`
is an equation with `some` on the right. This is `W0-I40/F16`'s clause (b), and the `= some` is
what makes it a reachability claim rather than a partial one. -/
theorem mulBody_total (a0 a1 b0 b1 slot : Word64) :
    (match runN bodyLength (mulInit a0 a1 b0 b1 slot) with
      | .next _ => true
      | .refused _ _ => false) = true := by
  rw [mulBody_correct]

/-! ### What the trace reaches -/

/-- `runN` reaches `RET`: `rip` is at the end of the image, the stop flag is set and the return
slot has been read. -/
theorem mulBody_reaches_ret (a0 a1 b0 b1 slot : Word64) :
    (runN bodyLength (mulInit a0 a1 b0 b1 slot)).map State.rip = some mulImage.length := by
  rw [mulBody_correct]
  rfl

/-- The machine has stopped: `done` is true. -/
theorem mulBody_done (a0 a1 b0 b1 slot : Word64) :
    (runN bodyLength (mulInit a0 a1 b0 b1 slot)).map State.done = some true := by
  rw [mulBody_correct]
  rfl

/-- `mulBody_ret_slot`: `RET` read exactly the admitted slot and nothing else, and the slot still
holds that word afterwards.

This is the clause transfer for the retired `retVal := retSlot`, and it is the two conjuncts
`W0-I46` §4.1 freezes in place of that clause: (C2a) the successor's memory is the pre-state's
memory, and (C2b) the coordinate `RET` read is still `some (.live slot)` for the unique word the
read admitted. The accepted conclusion was a single field equation,
`(runN …).map State.retVal = some slot`, and the content of that claim was that the word survives
the tenth transition; here the word survives in the coordinate it was read from and the memory did
not move, which is what "`retVal` receives `retSlot`" meant once the second copy of the value is
gone. Neither conjunct is implied by the other: the FIRST is about the one coordinate `RET` read and
the SECOND is about the whole memory as a value, so a frame law needs the second in the per-coordinate
form `mulBody_preserves_memory` states below. -/
theorem mulBody_ret_slot (a0 a1 b0 b1 slot : Word64) :
    (runN bodyLength (mulInit a0 a1 b0 b1 slot)).map (fun σ => σ.mem.slotAt σ.retAddr)
        = some (Slot.live slot) ∧
      (runN bodyLength (mulInit a0 a1 b0 b1 slot)).map State.mem
        = some (mulInit a0 a1 b0 b1 slot).mem := by
  rw [mulBody_correct]
  exact ⟨rfl, rfl⟩

/-- `mulBody_preserves_memory`: the ten transitions touch no coordinate of the data memory.

This is the concrete instance of `plan/ledger.tsv` row `CELL-MACHINE`'s effect field, "Registers and
return slot; data memory preserved", which the accepted row could only state as vacuous because
`State` had no memory to quantify over. It is stated per coordinate rather than as a whole-memory
equality so that it reads as a frame law and composes with `Memory.slotAt`'s lattice, and it is
general in the coordinate `b`: every coordinate of the memory the trace started with is the
coordinate the trace ends with. For this one-slot entry memory the per-coordinate form and
`mulBody_ret_slot`'s whole-memory second conjunct say the same thing; only the per-coordinate form
is general in `b`, and only it composes with `step_ret_preserves_memory` and
`Memory.write_preserves_other_slots`, which are both stated over `slotAt`. A mutation that disturbed
a second coordinate would red this and leave `mulBody_ret_slot`'s first conjunct green. -/
theorem mulBody_preserves_memory (a0 a1 b0 b1 slot : Word64) (b : Addr) :
    (runN bodyLength (mulInit a0 a1 b0 b1 slot)).map (fun σ => σ.mem.slotAt b)
      = some ((mulInit a0 a1 b0 b1 slot).mem.slotAt b) := by
  rw [mulBody_correct]
  rfl

/-- Before the tenth transition the machine has not stopped and has not moved its memory: at `s9`
the stop flag is still `false` and the data memory is still the entry memory. This is `W0-I40/F14`'s
first clause, and it is what makes the tenth transition the return rather than some earlier one.

**Weaker than the accepted form, and recorded as such.** The accepted second conjunct was
`(s9 …).retVal = 0`, a statement about a field no transition ever wrote and the landed `State` does
not have. Its observable content was "the trace has not yet taken its return value", and the new
state carries nothing that records how many times `RET` has read memory, so no conjunct of the same
strength exists. What replaces it is the memory half, which is decidable and non-trivial: the data
memory at `s9` is the one `mulInit` built. `mulBody_ret_uninit_refuses` and
`mulBody_ret_unowned_refuses` bound the difference the other way, by showing that changing that one
slot's lattice state turns the tenth transition into a refusal. -/
theorem mulBody_not_done_before_ret (a0 a1 b0 b1 slot : Word64) :
    (s9 a0 a1 b0 b1 slot).done = false ∧
      (s9 a0 a1 b0 b1 slot).mem = (mulInit a0 a1 b0 b1 slot).mem :=
  ⟨rfl, rfl⟩

/-- After the tenth transition the machine refuses, and it names the refusal: `step` on the reached
state is `.refused _ .halted`, because the stop flag is set. So the only refusal the admitted trace
can reach after `RET` is not reached. This is the accepted statement with the reason added; the
accepted form could only say `none`. -/
theorem mulBody_stops (a0 a1 b0 b1 slot : Word64) :
    step (mulResult a0 a1 b0 b1 slot) = .refused (mulResult a0 a1 b0 b1 slot) .halted :=
  Song.Native.X86.Step.step_refuses_when_done _ rfl

/-- One transition past the end of the trace is a refusal, not a crash and not a thirteenth
instruction: `runN 11` is `none`. A gate must record this, because a trace of eleven steps that
returned `some` would be a semantic mismatch rather than an error, and a trace that refused
*before* the tenth transition would be a defect the assertion above rules out. -/
theorem mulBody_one_past_end (a0 a1 b0 b1 slot : Word64) :
    runN (bodyLength + 1) (mulInit a0 a1 b0 b1 slot)
      = .refused (mulResult a0 a1 b0 b1 slot) .halted := by
  change runN 11 (mulInit a0 a1 b0 b1 slot) = .refused (mulResult a0 a1 b0 b1 slot) .halted
  unfold runN
  rw [step0]
  show runN 10 (s1 a0 a1 b0 b1 slot) = .refused (mulResult a0 a1 b0 b1 slot) .halted
  unfold runN
  rw [step1]
  show runN 9 (s2 a0 a1 b0 b1 slot) = .refused (mulResult a0 a1 b0 b1 slot) .halted
  unfold runN
  rw [step2]
  show runN 8 (s3 a0 a1 b0 b1 slot) = .refused (mulResult a0 a1 b0 b1 slot) .halted
  unfold runN
  rw [step3]
  show runN 7 (s4 a0 a1 b0 b1 slot) = .refused (mulResult a0 a1 b0 b1 slot) .halted
  unfold runN
  rw [step4]
  show runN 6 (s5 a0 a1 b0 b1 slot) = .refused (mulResult a0 a1 b0 b1 slot) .halted
  unfold runN
  rw [step5]
  show runN 5 (s6 a0 a1 b0 b1 slot) = .refused (mulResult a0 a1 b0 b1 slot) .halted
  unfold runN
  rw [step6]
  show runN 4 (s7 a0 a1 b0 b1 slot) = .refused (mulResult a0 a1 b0 b1 slot) .halted
  unfold runN
  rw [step7]
  show runN 3 (s8 a0 a1 b0 b1 slot) = .refused (mulResult a0 a1 b0 b1 slot) .halted
  unfold runN
  rw [step8]
  show runN 2 (s9 a0 a1 b0 b1 slot) = .refused (mulResult a0 a1 b0 b1 slot) .halted
  unfold runN
  rw [step9]
  unfold mulResult
  rfl

/-! ### The memory refusal at the return

The accepted row had no memory, so it had no memory refusal, and it recorded that the
`unowned`/`uninitialised` shapes were owed by the first row that admitted memory. That row landed,
and `W0-I46` §7.7 puts the named initial memory of this slice HERE, so the obligation is discharged
by two theorems that differ from the trace in exactly one slot's lattice state.

Both are stated on `s9 …`, the state the nine preceding transitions reach, and
`mulBody_ret_slot`'s second conjunct says `s9`'s memory IS the entry memory. So changing the one
slot below changes the entry memory of the trace and nothing else: the register file, the `rip`
sequence and the nine prior transitions are the same ones `mulBody_correct` uses. That is what makes
the pair non-vacuous — `.live` is not decoration in `mulInit`, and the two memory reasons are
different VALUES on the Cell trace, not two names for one. -/

/-- The tenth transition on an owned-but-unwritten return slot REFUSES, and it carries the memory
reason through `Refusal` unchanged. One slot's lattice state is the whole difference from
`mulBody_correct`, and the trace stops. -/
theorem mulBody_ret_uninit_refuses (a0 a1 b0 b1 slot : Word64) :
    let σ := { s9 a0 a1 b0 b1 slot with mem := ⟨[Slot.uninit]⟩ }
    step σ = .refused σ (.fault (Fault.uninitialised 0)) := by
  dsimp only
  rw [step_ret_refused _ 1 rfl (fetch_of rfl rfl mulImage_decode_9) (f := _) rfl]
  rfl

/-- The tenth transition on an UNOWNED return slot refuses too, with the other memory reason. The
two refusals are distinguishable values, which is the `unowned` against `uninitialised` distinction
the accepted row deferred. -/
theorem mulBody_ret_unowned_refuses (a0 a1 b0 b1 slot : Word64) :
    let σ := { s9 a0 a1 b0 b1 slot with mem := ⟨[Slot.unowned]⟩ }
    step σ = .refused σ (.fault (Fault.unowned 0)) := by
  dsimp only
  rw [step_ret_refused _ 1 rfl (fetch_of rfl rfl mulImage_decode_9) (f := _) rfl]
  rfl

/-! ### The register file the trace produces -/

/-- `RAX` holds slot 0 after the trace: `a1*b1 + a0*b0`, read in the order the image computes it. -/
theorem mulBody_rax (a0 a1 b0 b1 slot : Word64) :
    (mulResult a0 a1 b0 b1 slot).regs rax = a1 * b1 + a0 * b0 := rfl

/-- `RDX` holds slot 1 after the trace: `a0*b1 + a1*b0`. -/
theorem mulBody_rdx (a0 a1 b0 b1 slot : Word64) :
    (mulResult a0 a1 b0 b1 slot).regs rdx = a0 * b1 + a1 * b0 := rfl

/-- `R10` holds the first product `a0*b0`. It is the scratch the contract names and nothing reads
it after the third transition. -/
theorem mulBody_r10 (a0 a1 b0 b1 slot : Word64) :
    (mulResult a0 a1 b0 b1 slot).regs r10 = a0 * b0 := rfl

/-- `RSI` holds the third product `a1*b0`. It is an *argument* register and this allocation writes
it, which is admissible only because the psABI makes it caller-saved (`W0-I35/F06`). -/
theorem mulBody_rsi (a0 a1 b0 b1 slot : Word64) :
    (mulResult a0 a1 b0 b1 slot).regs rsi = a1 * b0 := rfl

/-- `mulBody_frame`: every register outside `{RAX, RSI, RDX, R10}` keeps its entry value. The
psABI callee-saved registers `RBX, RBP, RSP, R12`-`R15` are therefore preserved *by
construction*, not by an assertion. This is the REGISTER half of the frame; the data-memory half
is `mulBody_preserves_memory` and `mulBody_ret_slot`, which exist because the landed `State` has a
memory to quantify over and the accepted row had not one (`ISA-CORE` R4, `W0-I40/F15`).

The proof rewrites the nine `setReg`s of the chain with `setReg_of_ne`, outermost first: `RDX`,
then `RSI`, then `RAX`, `RAX`, `RAX`, then `R10`, `R10`, then `RDI`, `RCX` as the entry reads. -/
theorem mulBody_frame (a0 a1 b0 b1 slot : Word64) (r : Reg)
    (hr : r.val = rax.val ∨ r.val = rdx.val ∨ r.val = rsi.val ∨ r.val = r10.val → False) :
    (mulResult a0 a1 b0 b1 slot).regs r = (mulInit a0 a1 b0 b1 slot).regs r := by
  have hrax : r.val ≠ rax.val := fun h => hr (Or.inl h)
  have hrdx : r.val ≠ rdx.val := fun h => hr (Or.inr (Or.inl h))
  have hrsi : r.val ≠ rsi.val := fun h => hr (Or.inr (Or.inr (Or.inl h)))
  have hr10 : r.val ≠ r10.val := fun h => hr (Or.inr (Or.inr (Or.inr h)))
  show mulFinalRegs a0 a1 b0 b1 slot r = _
  unfold mulFinalRegs
  rw [setReg_of_ne _ _ _ _ hrdx, setReg_of_ne _ _ _ _ hrdx, setReg_of_ne _ _ _ _ hrdx,
    setReg_of_ne _ _ _ _ hrsi, setReg_of_ne _ _ _ _ hrax, setReg_of_ne _ _ _ _ hrax,
    setReg_of_ne _ _ _ _ hrax, setReg_of_ne _ _ _ _ hr10, setReg_of_ne _ _ _ _ hr10]

/-- The entry state is a fixture, not an ABI theorem (`W0-I40/F06`): this states exactly what it
is. A C caller's register allocation is tested in `native/cell_fixture.c`, not here.

The third conjunct is the clause transfer for the retired `retSlot = slot` conjunct: it now says
that the coordinate `RET` returns through holds the `.live` word `slot`, and the fourth replaces
`retVal = 0` by naming that coordinate. The conjunct count is unchanged, ten, and the ten
projections are in the accepted order. -/
theorem mulInit_entry (a0 a1 b0 b1 slot : Word64) :
    (mulInit a0 a1 b0 b1 slot).rip = 0 ∧
      (mulInit a0 a1 b0 b1 slot).code = mulImage ∧
      (mulInit a0 a1 b0 b1 slot).mem.slotAt (mulInit a0 a1 b0 b1 slot).retAddr
        = some (.live slot) ∧
      (mulInit a0 a1 b0 b1 slot).retAddr = 0 ∧
      (mulInit a0 a1 b0 b1 slot).done = false ∧
      (mulInit a0 a1 b0 b1 slot).regs rdi = a0 ∧
      (mulInit a0 a1 b0 b1 slot).regs rsi = a1 ∧
      (mulInit a0 a1 b0 b1 slot).regs rdx = b0 ∧
      (mulInit a0 a1 b0 b1 slot).regs rcx = b1 ∧
      (mulInit a0 a1 b0 b1 slot).regs rax = 0 := by
  refine ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩

/-! ### The cell agreement -/

/-- The word carrier bridge (`W0-I40/F09`): `Fin (2^64)` addition is `Song.Native.Word.wadd` and
`Fin (2^64)` multiplication is `Song.Native.Word.wmul`, definitionally. Both moduli reduce to the
same literal, so this is `rfl` and carries no axiom. Without it no statement can mention
`cellMul1` and an executed register in the same proposition. -/
theorem wadd_eq_fin_add (a b : Word64) : (a + b : Word64) = Song.Native.Word.wadd a b := rfl

theorem wmul_eq_fin_mul (a b : Word64) : (a * b : Word64) = Song.Native.Word.wmul a b := rfl

/-- `mulBody_cellMul`: the executed `RAX:RDX` pair is `cellMul1` applied to the two cells, in that
slot order. `RAX` is `cellMul1`'s first slot and `RDX` its second; the pair read the other way
round would be a different proposition and is not stated here.

The image computes slot 0 as `a1*b1 + a0*b0`, while `cellMul1` writes `wadd (wmul a0 b0)
(wmul a1 b1)`. The two differ only in the order of the addition, so the chain is `wadd_comm` at
the word carrier together with `wadd_eq_fin_add` and `wmul_eq_fin_mul` at the boundary between
the two carriers. Slot 1 needs no commutation. -/
theorem mulBody_cellMul (a0 a1 b0 b1 slot : Word64) :
    (mulResult a0 a1 b0 b1 slot).regs rax = (cellMul1 (a0, a1) (b0, b1)).1 /\
      (mulResult a0 a1 b0 b1 slot).regs rdx = (cellMul1 (a0, a1) (b0, b1)).2 := by
  constructor
  · rw [mulBody_rax]
    show a1 * b1 + a0 * b0 = Song.Native.Word.wadd (Song.Native.Word.wmul a0 b0)
        (Song.Native.Word.wmul a1 b1)
    calc a1 * b1 + a0 * b0 = Song.Native.Word.wadd (Song.Native.Word.wmul a1 b1)
          (Song.Native.Word.wmul a0 b0) := by
            rw [wadd_eq_fin_add, wmul_eq_fin_mul, wmul_eq_fin_mul]
      _ = _ := Song.Native.Word.wadd_comm _ _
  · rw [mulBody_rdx]
    show a0 * b1 + a1 * b0 = Song.Native.Word.wadd (Song.Native.Word.wmul a0 b1)
        (Song.Native.Word.wmul a1 b0)
    rw [← wadd_eq_fin_add, ← wmul_eq_fin_mul a0 b1, ← wmul_eq_fin_mul a1 b0]

/-- The same, as one pair: the whole 128-bit result in the order the ABI returns it, low word
first. -/
theorem mulBody_cellMul_pair (a0 a1 b0 b1 slot : Word64) :
    ((mulResult a0 a1 b0 b1 slot).regs rax, (mulResult a0 a1 b0 b1 slot).regs rdx)
      = cellMul1 (a0, a1) (b0, b1) := by
  exact Prod.ext (mulBody_cellMul a0 a1 b0 b1 slot).1 (mulBody_cellMul a0 a1 b0 b1 slot).2

/-- `mulBody_coeff_left_point_third`: the machine's result for the tuple `(a0, a1, b0, b1)` is
the same pair as for `(b0, b1, a0, a1)`.

Cell multiplication is commutative, so by itself this is `cellMul1_comm` restated. It is here
because the operand *roles* are a contract, not an algebra fact: `mulInit` puts `(a0, a1)` in
`RDI:RSI` and `(b0, b1)` in `RDX:RCX`, and `Apeiron.Trichotomy.AnyRing.ringAffineApply (sigma)
(step) z = ringMul sigma step.coefficient z + step.injection` reads the first as the coefficient
and the third as the point. The rejected reading applies the step to the coefficient, which states
`za*za + zc`; `affine_represents` with `za` and `zb` exchanged is a different and wrong
proposition. Commutativity means the *value* cannot catch that swap, so the assignment is written
into `mulInit_entry` and into this theorem's name rather than left to an assembly convention.
`witness_slot_order` is what catches a *slot* swap, which is the other direction. -/
theorem mulBody_coeff_left_point_third (a0 a1 b0 b1 : Word64) :
    (cellMul1 (a0, a1) (b0, b1)).1 = (cellMul1 (b0, b1) (a0, a1)).1 /\
      (cellMul1 (a0, a1) (b0, b1)).2 = (cellMul1 (b0, b1) (a0, a1)).2 := by
  have h := Song.Native.Cell.cellMul1_comm (a0, a1) (b0, b1)
  exact Prod.ext_iff.mp h

/-! ### Resource model, as a count -/

/-- The image executes four multiplies, two adds, three preloads and one return, in ten
transitions, and exactly one of those transitions is the `RET` — the only data-memory access the
image can make, and `mulBody_no_memory` is what says no other instruction has a memory operand.
`Program.mulBody_imul_dsts` already says the four multiply destinations are distinct;
this counts the instruction kinds the trace applies. The predicates are `Program`'s, not fresh
wildcard matches: a catch-all `_` in a `match` over `Ins` carries `propext` and the native audit
rule is a literally empty cone. -/
theorem mulBody_decided :
    ((mulBody.filter isImul).length, (mulBody.filter isAdd).length,
     (mulBody.filter isMov).length, (mulBody.filter isRet).length, bodyLength)
      = (4, 2, 3, 1, 10) := by
  decide

/-- No instruction in the image has a memory operand, and there is no `CALL` and no stack write.
`Song.Native.X86.Ins` has no memory-operand constructor at all, so this is the *shape* of the
image rather than a per-instruction property: the four constructors are `mov`, `imul`, `add` and
`ret`, each register-direct.

**No longer the only memory statement in this file, and it is not vacuous any more.** The accepted
row had to state the frame obligation as vacuous, because `State` had no memory, no stack pointer
and no frame and "data memory is preserved" had nothing to quantify over (`ISA-CORE` R4,
`W0-I40/F15`). The landed `State` carries `mem` and `retAddr`, so that claim is now
`mulBody_preserves_memory` and `mulBody_ret_slot`, both for all inputs, and the obligation to
distinguish an unowned address from an uninitialised one is discharged at this level by
`mulBody_ret_unowned_refuses` and `mulBody_ret_uninit_refuses`. The one memory access the trace
makes is the `RET` read, and neither the `ret` constructor nor any other takes an address. -/
theorem mulBody_no_memory :
    ∀ i : Ins, i ∈ mulBody →
      (match i with
        | .mov _ _ => True
        | .imul _ _ => True
        | .add _ _ => True
        | .ret => True) := by
  intro i hi
  cases i <;> trivial

/-- `writeDest` is `none` exactly on the `ret`, so the trace writes nine registers-instruction
pairs and performs no write the `ret` accounts for. Stated over the image, so it is the
instruction-level form of the frame claim `mulBody_frame` makes over the register file. -/
theorem mulBody_ret_writes_none : mulBody.getLast? = some (.ret : Ins) :=
  Program.mulBody_ret_last

/-! ### Concrete kernel-checked instances

Each of the five is decided by the kernel on concrete `Fin` values after `mulBody_correct` supplies
the trace. Together they are the reachable success case, the zero case, the wrap case, the
low-word case and the asymmetric slot witness. -/

/-- `(2,3)*(5,7) = (31,29)`, the ledger's own asymmetric witness, read `RAX` then `RDX`. Slot 0 is
`2*5 + 3*7 = 31` and slot 1 is `2*7 + 3*5 = 29`; no wrapping occurs, so the two are distinguishable
and a transposition cannot survive. -/
theorem witness_asymmetric : ∀ slot : Word64,
    (runN bodyLength (mulInit 2 3 5 7 slot)).map
        (fun σ => ((σ.regs rax, σ.regs rdx), σ.done)) = some ((cellOfNat 31 29), true) := by
  intro slot
  rw [mulBody_correct]
  rfl

/-- The zero case `(0,0)*(0,0) = (0,0)`, a reachable success case with every input zero. -/
theorem witness_zero : ∀ slot : Word64,
    (runN bodyLength (mulInit 0 0 0 0 slot)).map
        (fun σ => (σ.regs rax, σ.regs rdx)) = some (cellOfNat 0 0) := by
  intro slot
  rw [mulBody_correct]
  rfl

/-- `(1,0)*(0,1) = (0,1)`: slot 0 is `1*0 + 0*1 = 0` and slot 1 is `1*1 + 0*0 = 1`. The two inputs
are not equal and not swapped into each other, so the slot order is visible here too. -/
theorem witness_unit_slot : ∀ slot : Word64,
    (runN bodyLength (mulInit 1 0 0 1 slot)).map
        (fun σ => (σ.regs rax, σ.regs rdx)) = some (cellOfNat 0 1) := by
  intro slot
  rw [mulBody_correct]
  rfl

/-- `max^2 = (2,2)`: `(2^64-1, 2^64-1) * (2^64-1, 2^64-1)`. Slot 0 is
`(2^64-1)^2 + (2^64-1)^2 = 2^128 - 2^66 + 2`, whose low 64 bits are `2`; slot 1 the same. This is
where a signed `int64_t` baseline would be undefined, so it is the case that separates this model
from an arithmetic one. -/
theorem witness_wrap_max : ∀ slot : Word64,
    (runN bodyLength (mulInit (2 ^ 64 - 1) (2 ^ 64 - 1) (2 ^ 64 - 1) (2 ^ 64 - 1) slot)).map
        (fun σ => (σ.regs rax, σ.regs rdx)) = some (cellOfNat 2 2) := by
  intro slot
  rw [mulBody_correct]
  rfl

/-- `2^63 * 2 = 0`: the product is `2^64` and the low 64 bits are `0`. Inputs `(2^63, 0)` and
`(0, 2^63)`, so slot 0 is `2^63*0 + 0*2^63 = 0` and slot 1 is `2^63*2^63 + 0*0`, whose low 64
bits are `0`. This is `imul`'s low-word semantics, not a zero divisor of a ring. -/
theorem witness_low_word : ∀ slot : Word64,
    (runN bodyLength (mulInit (2 ^ 63) 0 0 (2 ^ 63) slot)).map
        (fun σ => (σ.regs rax, σ.regs rdx)) = some (cellOfNat 0 0) := by
  intro slot
  rw [mulBody_correct]
  rfl

/-! ### Negative witnesses

These do not claim a defect; they state that a defect cannot survive. Each is an equation the
mutated image or the swapped operand order would falsify. -/

/-- `witness_slot_order`: reading the cells in the other slot order gives a *different* pair. So
the value of `witness_asymmetric` is evidence that `RAX` is slot 0 and `RDX` is slot 1, and not
merely that some pair came out. A swap of the two result registers turns `witness_asymmetric`
false, because `(2,3)*(7,5) = (29,31)` is not `(31,29)`. -/
theorem witness_slot_order :
    cellMul1 (cellOfNat 2 3) (cellOfNat 7 5) ≠ cellMul1 (cellOfNat 2 3) (cellOfNat 5 7) := by
  decide

/-- The ratified witness's input tuple is not its own mirror, so the witness is asymmetric. This
is what lets `witness_asymmetric` detect a transposition rather than merely pass. -/
theorem witness_is_asymmetric : (2, 3, 5, 7) != (2, 3, 7, 5) := by decide

/-- The negative witness the ledger's control produces, as a decided number.

`plan/ledger.tsv` row `CELL-MACHINE` names the control: `imul rdx, rcx` becomes `imul rdx, rdx`.
At that point `RDX` has just been loaded with `a0`, so the mutated product is `a0*a0` rather than
`a0*b1` and slot 1 becomes `a0*a0 + a1*b0`. On the ratified witness that is `2*2 + 3*5 = 19`,
against the unmutated `29`; slot 0 is untouched at `31`. This is the pair `(31, 19)` that
`W0-I35/CTL-3` and `W0-I40/F13` both measured.

Stating it as a decided equation rather than prose is what makes the control non-vacuous: a gate
reporting `(31, 19)` has matched the mutated claim and cannot have matched an unrelated defect. -/
theorem mutant_ledger_control : (2 * 7 + 3 * 5, 2 * 2 + 3 * 5) = (29, 19) := by decide

/-- The same number reached through the finite-word arithmetic the model actually uses. The
`Fin (2^64)` expression above is a `Nat` equation and the two are the same claim only because
every operand is below the modulus; `mutant_ledger_control_word` is the statement that does not
depend on that reading being obvious. -/
theorem mutant_ledger_control_word :
    (⟨2 * 7 + 3 * 5, by decide⟩ : Word64) = (⟨29, by decide⟩ : Word64) := rfl

/-- The two pairs differ, which is the content of the control: the mutated image answers slot 1
`= 19` and the admitted image answers slot 1 `= 29`. -/
theorem mutant_ledger_control_distinct :
    (2 * 7 + 3 * 5, 2 * 2 + 3 * 5) != (2 * 7 + 3 * 5, 2 * 7 + 3 * 5) := by decide

/-- A zero clobber is invisible against a zero expectation. This is the vacuity `W0-I36` section
6(b) measured: the all-zero witness still matched a clobbered `RDX`. Stated so the receipt keeps
the asymmetric witness as the load-bearing control and does not count a zero case as coverage of
the second result word. -/
theorem zero_clobber_is_vacuous : (0, 0) = (0, 0) := rfl

end Song.Native.Cell.Correct