import Song.Native.Word

/-!
# Song's native Cell at Sigma = +1, width 64

A `Cell64` is two words side by side, first slot then second. `cellMul1` is the two-slot
algebra `R[x]/(x^2 - sigma)` at `sigma = +1`: `(a + b x)(c + d x) = (ac + bd) + (ad + bc) x`.
Sigma is a parameter of the contract, not of this file; `+1` is the specialisation the
adjudicated first slice fixes, and the omitted `sigma` term is the reason there is no
fifth argument here (README's contract block says so).

`cellAdd` is componentwise. Both are total and allocate nothing: one product per slot,
then one sum per slot. Four multiplications and two additions per cell product, all at
width 64 with one `%` each.

Nothing in this module imports the corpus. The relation to `Apeiron.Trichotomy.AnyRing` is
`Song.Canonical.CellBridge`, which is the only tree allowed to import it.
-/

namespace Song
namespace Native

-- Song's native Cell namespace.
namespace Cell

open Word

/-- A native cell at width 64: two words, first slot then second slot. -/
abbrev Cell64 : Type := Word64 × Word64

/-- Cell multiplication at `sigma = +1`, wrapping: first slot `ac + bd`, second slot
`ad + bc`. Four word products and two word sums. -/
def cellMul1 (a b : Cell64) : Cell64 :=
  (wadd (wmul a.1 b.1) (wmul a.2 b.2), wadd (wmul a.1 b.2) (wmul a.2 b.1))

/-- Cell addition, componentwise. -/
def cellAdd (a b : Cell64) : Cell64 := (wadd a.1 b.1, wadd a.2 b.2)

/-- Read a pair of counting numbers as a cell. Wraps each slot. -/
def cellOfNat (k l : Nat) : Cell64 := (wordOfNat k, wordOfNat l)

/-- Cell multiplication does not depend on the order of the two cells. This is the
counterpart of `Apeiron.Trichotomy.AnyRing.ringMul_comm`, proved at the word carrier with
no instance and no import. -/
theorem cellMul1_comm (a b : Cell64) : cellMul1 a b = cellMul1 b a := by
  apply Prod.ext
  · show wadd (wmul a.1 b.1) (wmul a.2 b.2) = wadd (wmul b.1 a.1) (wmul b.2 a.2)
    rw [wmul_comm a.1 b.1, wmul_comm a.2 b.2]
  · show wadd (wmul a.1 b.2) (wmul a.2 b.1) = wadd (wmul b.1 a.2) (wmul b.2 a.1)
    rw [wmul_comm a.1 b.2, wmul_comm a.2 b.1, wadd_comm (wmul b.1 a.2) (wmul b.2 a.1)]

/-- Adding two sums slot by slot, so a `cellAdd` can be rebracketed across two cells. -/
theorem wadd_wadd (a b c d : Word64) :
    wadd (wadd a b) (wadd c d) = wadd (wadd a c) (wadd b d) := by
  calc
    wadd (wadd a b) (wadd c d)
        = wadd a (wadd b (wadd c d)) := wadd_assoc _ _ _
    _ = wadd a (wadd (wadd b c) d) :=
        congrArg (fun t => wadd a t) (wadd_assoc b c d).symm
    _ = wadd a (wadd (wadd c b) d) :=
        congrArg (fun t : Word64 => wadd a (wadd t d))
          (show wadd b c = wadd c b from wadd_comm b c)
    _ = wadd (wadd a (wadd c b)) d := (wadd_assoc _ _ _).symm
    _ = wadd (wadd (wadd a c) b) d :=
        congrArg (fun t => wadd t d) (wadd_assoc a c b).symm
    _ = wadd (wadd a c) (wadd b d) := wadd_assoc _ _ _

/-- Cell multiplication spreads across a sum of cells in the second operand. Counterpart
of `Apeiron.Trichotomy.AnyRing.ringMul_distrib_add`; this is the law an injection term
needs when a composed affine step is folded into one step. -/
theorem cellMul1_add (a b c : Cell64) :
    cellMul1 a (cellAdd b c) = cellAdd (cellMul1 a b) (cellMul1 a c) := by
  apply Prod.ext
  · show wadd (wmul a.1 (wadd b.1 c.1)) (wmul a.2 (wadd b.2 c.2))
      = wadd (wadd (wmul a.1 b.1) (wmul a.2 b.2)) (wadd (wmul a.1 c.1) (wmul a.2 c.2))
    rw [wmul_add, wmul_add, wadd_wadd]
  · show wadd (wmul a.1 (wadd b.2 c.2)) (wmul a.2 (wadd b.1 c.1))
      = wadd (wadd (wmul a.1 b.2) (wmul a.2 b.1)) (wadd (wmul a.1 c.2) (wmul a.2 c.1))
    rw [wmul_add, wmul_add, wadd_wadd]

/-- The ratified asymmetric witness: `(2,3) * (5,7) = (31,29)` at `sigma = +1`. Slot 0 is
`2*5 + 3*7 = 31` and slot 1 is `2*7 + 3*5 = 29`. No wrapping occurs, so this also shows
the two slots are read in the stated order: swapping `b` into slot 0's second factor gives
`2*5 - 3*7` and this value cannot survive the swap. -/
theorem cellMul1_witness :
    cellMul1 (cellOfNat 2 3) (cellOfNat 5 7) = cellOfNat 31 29 := by decide

end Cell

end Native
end Song