Round-six κ development, definitions part 24

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_Kappa_K_Defs4
import Definitions.Def_IntMul_Kappa_K_Defs7
import Definitions.Def_IntMul_Kappa_K_Defs6
import Definitions.Def_IntMul_Kappa_R6_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs3
import Definitions.Def_IntMul_Kappa_K_Defs8

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.R6CxMerge
/-!
# NC3: the PR #15 whole-residual merge

For a linearly independent family `v₁, …, v_ρ` in `𝔽₂^m` (e.g. an orthonormal residual basis of
a Proposition 8 edge) and signs `ε_k = ±1`, the edge operator
`∏_k (aI + bX_{v_k})^{ε_k}` (on every column: `colT (∏ Tk ε_k v_k)`) is conjugate, by a word of
binary row additions `P` (an element of `GL_m(𝔽₂)` sending `v_k ↦ e_{h_k}`), to
`(-i)^{|N||κ|} Z_N C^{⊗(S × κ)} Z_N` with `S = {h_k}` (`|S| = ρ`) and `N = {h_k : ε_k = -1}`:
**one** forward child call of width `ρ`.

* `conj_rowAdds`: conjugation of a kernel product by row additions (15).
* `kernels_single`: kernels on distinct unit vectors `e_{h_k}` = the slot family (they live on
  distinct slots and commute).
* `exists_rowAdds`: every independent family is sent to distinct unit vectors by a word of row
  additions (basis extension + `gl_f2_row_additions`).
* **`merge_identity`** (operator form) and **`merge_chunk`** (step form: row additions, one
  child `child w S neg`, row additions reversed).
* `mergedChunk`, `mergedChunk_den`, `mergedChunk_widths`: the chosen chunk for a kernel list
  `L` (in `P8Lift.frameSteps` form) with independent vectors; `mergedChunk_den_frameSteps`:
  same denotation as the single-slot chunks `frameSteps w L`, but child widths `[|L|]`
  instead of `|L|` ones. Orthonormal version `lin_indep_of_orthonormal`.
* `edgeStepsH`: the merged frame change of a Proposition 8 edge (`EdgeP`): denotation
  `wireOp w (PhiK (qL V - qL U))` as `P8Lift.edgeSteps`, one child of width `Fd V U`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx

open Matrix Finset Complex Butterfly P8Lift

variable {m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ]

/-! ## Row-addition words -/

/-! ## Kernels on distinct unit vectors -/

/-! ## Existence of the row-addition word -/

/-! ## The merge identity -/

/-! ## Step form -/

section Steps

variable {R : Type} [Fintype R] [DecidableEq R]

lemma prod_finRange_get (L : List (ℤ × (Fin m → ZMod 2))) :
    ((List.finRange L.length).map fun k => Tk (L.get k).1 (L.get k).2) =
      L.map fun p => Tk p.1 p.2 := by
  conv_rhs => rw [← List.map_get_finRange L]
  rw [List.map_map]; rfl

end Steps

/-! ## Merged Proposition 8 edges -/

end IntMul.Kappa.R6.Cx

end

section
-- Source module: Solutions.R6CxNetEdge
/-!
# Merged frame changes for any number of address bits `m` (NC3, generic `m`)

`R6CxMerge.edgeStepsH` is stated for `m = h³` (through `NetComplexP8.EdgeP` on `Vc h`). Here the
same construction over `Fin m → ZMod 2` for any `m` (needed for `m = h² = 576`), with the edge
hypothesis `NetComplexP8.EdgeOK` (generic in `m`) and `NetComplexP8.edge_kernel`.

* `edgeStepsM w V U`: one merged chunk (row additions, one child of width `Fd V U`, row
  additions undone) on wire `w`;
* `edgeStepsM_den`: denotation `wireOp w (PhiK (qL V - qL U))`;
* `edgeStepsM_widths`: child widths `[Fd V U]` (none if `Fd V U = 0`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx

open Matrix Finset Complex Butterfly P8Lift NetComplexP8 NetComplexLabels

variable {m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ]
variable {R : Type} [Fintype R] [DecidableEq R]

/-- Kernel list spec for an edge `U → V` over `Fin m`. -/
def KerSpecM (V U : Submodule (ZMod 2) (Fin m → ZMod 2)) (L : List (ℤ × (Fin m → ZMod 2))) : Prop :=
  (∀ p ∈ L, (p.1 = 1 ∨ p.1 = -1) ∧ p.2 ≠ 0) ∧ L.length = Fd V U ∧
    (∀ g, NetComplexInterface.PhiQ (qL V - qL U) g = L.foldr (fun p g' => NetComplexPhase.transK p.1 p.2 g') g) ∧
    ∃ B : Finset (Fin m → ZMod 2), NetComplexOrtho.Orthonormal2 B ∧ L.map Prod.snd = B.toList

/-- The orthonormal kernel list chosen for an edge. -/
noncomputable def kersM (V U : Submodule (ZMod 2) (Fin m → ZMod 2)) : List (ℤ × (Fin m → ZMod 2)) := by
  classical
  exact if hh : ∃ L, KerSpecM V U L then Classical.choose hh else []

/-- The merged frame change of an edge `U → V` on wire `w` (any `m`). -/
noncomputable def edgeStepsM (w : R) (V U : Submodule (ZMod 2) (Fin m → ZMod 2)) : List (HStep R m) :=
  mergedChunk w (kersM V U)

end IntMul.Kappa.R6.Cx

end

section
-- Source module: Solutions.R6CxNetSim
/-!
# Chunk programs with phase frames (the physical simulation, any wire type)

A **chunk** at label `V` first moves some wires to `V` (each move `U → V` is one merged frame
change `edgeStepsM`, needing `EdgeOK V U`), then applies elementary scalar gates
`z_dst += c · z_src` (pointwise on the addresses) whose two wires are at `V`.

* `Inv lab Λ F`: the physical state `F` is the logical state `Λ` in the frames `Φ_{q_{lab w}}`.
* `chunk_sim` / `prog_sim`: a valid chunk (program) maps `Inv lab Λ F` to
  `Inv lab' (runOps ops Λ) (den · F)`.
* `prog_widths`: the child widths are the residual dimensions `Fd V U` of the moves.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx

open Matrix Finset Complex Butterfly P8Lift NetComplexP8 NetComplexLabels

variable {m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ]
variable {R : Type} [Fintype R] [DecidableEq R]

/-- Labels: subspaces of `𝔽₂^m`. -/
abbrev Lab (m : ℕ) := Submodule (ZMod 2) (Fin m → ZMod 2)

/-- An elementary scalar gate `z_dst += c · z_src`. -/
structure GOp (R : Type) where
  dst : R
  src : R
  c : ℂ

/-- Its matrix on the roles. -/
def GOp.mat (o : GOp R) : Matrix R R ℂ := 1 + Matrix.single o.dst o.src o.c

/-- A chunk: label, moves (wire, old label), elementary gates. -/
structure GChunk (R : Type) (m : ℕ) where
  V : Lab m
  mv : List (R × Lab m)
  ops : List (GOp R)

/-- The steps of a list of moves to `V`. -/
noncomputable def mvSteps (V : Lab m) (mv : List (R × Lab m)) : List (HStep R m) :=
  mv.flatMap fun p => edgeStepsM p.1 V p.2

/-- The steps of a chunk. -/
noncomputable def GChunk.steps (C : GChunk R m) : List (HStep R m) :=
  mvSteps C.V C.mv ++ C.ops.map fun o => HStep.gate o.mat

/-- Labels after the moves to `V`. -/
def mvLab (V : Lab m) : List (R × Lab m) → (R → Lab m) → R → Lab m
  | [], lab => lab
  | p :: mv, lab => mvLab V mv (Function.update lab p.1 V)

/-- Moves are valid: each claimed old label is the current one, and each edge is OK. -/
def MvValid (V : Lab m) : List (R × Lab m) → (R → Lab m) → Prop
  | [], _ => True
  | p :: mv, lab => lab p.1 = p.2 ∧ EdgeOK V p.2 ∧ MvValid V mv (Function.update lab p.1 V)

/-- A valid chunk. -/
def GChunk.Valid (C : GChunk R m) (lab : R → Lab m) : Prop :=
  MvValid C.V C.mv lab ∧ ∀ o ∈ C.ops, mvLab C.V C.mv lab o.dst = C.V ∧ mvLab C.V C.mv lab o.src = C.V

/-- One logical gate. -/
def runOp {Vt : Type*} [AddCommGroup Vt] [Module ℂ Vt] (Λ : R → Vt) (o : GOp R) : R → Vt :=
  Function.update Λ o.dst (Λ o.dst + o.c • Λ o.src)

/-- Logical gates in order. -/
def runOps {Vt : Type*} [AddCommGroup Vt] [Module ℂ Vt] (ops : List (GOp R)) (Λ : R → Vt) : R → Vt :=
  ops.foldl runOp Λ

/-- The invariant: physical = frame of logical, wire by wire. -/
def Inv (lab : R → Lab m) (Λ : R → Addr m κ → ℂ) (F : R × Addr m κ → ℂ) : Prop :=
  ∀ w, (fun x => F (w, x)) = PhiK (qL (lab w)) *ᵥ Λ w

/-! ## Programs -/

/-- Steps of a chunk program. -/
noncomputable def progSteps (cs : List (GChunk R m)) : List (HStep R m) := cs.flatMap GChunk.steps

/-- Labels after a chunk program. -/
def progLab : List (GChunk R m) → (R → Lab m) → R → Lab m
  | [], lab => lab
  | C :: cs, lab => progLab cs (mvLab C.V C.mv lab)

/-- Validity of a chunk program. -/
def ProgValid : List (GChunk R m) → (R → Lab m) → Prop
  | [], _ => True
  | C :: cs, lab => C.Valid lab ∧ ProgValid cs (mvLab C.V C.mv lab)

/-- All logical gates of a program. -/
def progOps (cs : List (GChunk R m)) : List (GOp R) := cs.flatMap GChunk.ops

/-! ## Child widths -/

/-- The residual widths of a list of moves. -/
noncomputable def mvWidths (V : Lab m) (mv : List (R × Lab m)) : List ℕ :=
  mv.flatMap fun p => if Fd V p.2 = 0 then [] else [Fd V p.2]

/-- Widths of a program. -/
noncomputable def progWidths (cs : List (GChunk R m)) : List ℕ := cs.flatMap fun C => mvWidths C.V C.mv

end IntMul.Kappa.R6.Cx

end

section
-- Source module: Solutions.R6CxNetBT
/-!
# A kernel-friendly finite map `ℕ → ℕ` (packed-leaf binary tree)

Depth-8 binary tree, 256 slots of 40 bits per leaf: capacity 65536 keys, values `< 2^40`.
`gget_gset`: reading back a write; `wf_gset`: writes keep the shape.
-/

namespace IntMul.Kappa.R6.Cx.NetBT

inductive BT where
  | leaf (v : ℕ)
  | node (l r : BT)

/-- `2^40`. -/
def SM : ℕ := 1099511627776

def lget (v j : ℕ) : ℕ := (v >>> (40 * j)) % SM
def lset (v j x : ℕ) : ℕ := v ^^^ ((lget v j ^^^ x) <<< (40 * j))

def BT.get : BT → ℕ → ℕ → ℕ
  | .leaf v, _, j => lget v j
  | .node l r, p, j => cond (Nat.beq (p % 2) 0) (l.get (p / 2) j) (r.get (p / 2) j)

def BT.set : BT → ℕ → ℕ → ℕ → BT
  | .leaf v, _, j, x => .leaf (lset v j x)
  | .node l r, p, j, x =>
    cond (Nat.beq (p % 2) 0) (.node (l.set (p / 2) j x) r) (.node l (r.set (p / 2) j x))

def BT.wf : ℕ → BT → Bool
  | 0, .leaf _ => true
  | d + 1, .node l r => BT.wf d l && BT.wf d r
  | _, _ => false

def gget (t : BT) (i : ℕ) : ℕ := t.get (i / 256) (i % 256)
def gset (t : BT) (i x : ℕ) : BT := t.set (i / 256) (i % 256) x

/-- Capacity of the depth-8 tree. -/
def CAP : ℕ := 65536

/-- Structural equality. -/
def BT.beq : BT → BT → Bool
  | .leaf a, .leaf b => Nat.beq a b
  | .node l r, .node l' r' => BT.beq l l' && BT.beq r r'
  | _, _ => false

end IntMul.Kappa.R6.Cx.NetBT

end

section
-- Source module: Solutions.R6CxNetLoc
/-!
# Local chunk programs with code labels, generated and checked in the kernel

A `Spec` is a chunk to be performed at label code `V` on the listed wires (each wire not yet at
`V` is moved there) with elementary gates `(dst, src, k)` (`z_dst += (k/2) z_src`).
`progRun` generates the chunk list (moves computed from a `BT` code state); `progChk` checks it
with a Boolean move checker `mvOK` and accumulates the packed width histogram.

`prog_valid`: if the check passes and the move checker is sound for a labelling `lab` and an
injective wire map `ι`, the mapped chunk program (`mapProg`) is `ProgValid` for every global
labelling corresponding to the initial state, and the final global labelling corresponds to the
final state (other roles untouched).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx.NetLoc

open NetBT NetComplexP8

structure Spec where
  V : ℕ
  ws : List ℕ
  ops : List (ℕ × ℕ × ℤ)

structure LChunk where
  V : ℕ
  mv : List (ℕ × ℕ)
  ops : List (ℕ × ℕ × ℤ)

/-- Moves of the wires `ws` to `V` from the state `t`. -/
def mvRun (V : ℕ) : List ℕ → BT → List (ℕ × ℕ) × BT
  | [], t => ([], t)
  | w :: ws, t =>
    let o := gget t w
    cond (Nat.beq o V) (mvRun V ws t) (let r := mvRun V ws (gset t w V); ((w, o) :: r.1, r.2))

/-- The generated chunks and the final state. -/
def progRun : List Spec → BT → List LChunk × BT
  | [], t => ([], t)
  | s :: ss, t =>
    let r := mvRun s.V s.ws t
    let q := progRun ss r.2
    (⟨s.V, r.1, s.ops⟩ :: q.1, q.2)

/-- `2^20`. -/
def HB : ℕ := 1048576

/-- Packed width histogram of moves. -/
def hsum (wd : ℕ → ℕ → ℕ → ℕ) (V : ℕ) : List (ℕ × ℕ) → ℕ
  | [] => 0
  | p :: l => HB ^ wd p.1 p.2 V + hsum wd V l

/-- One chunk is OK (given its moves `mv` and the state `t'` after the moves). -/
def chunkOK (nl : ℕ) (mvOK : ℕ → ℕ → ℕ → Bool) (s : Spec) (mv : List (ℕ × ℕ)) (t' : BT) : Bool :=
  Nat.blt s.V SM && !(Nat.beq (s.V % 4) 3) && s.ws.all (fun w => Nat.blt w nl) &&
    mv.all (fun p => mvOK p.1 p.2 s.V) &&
    s.ops.all (fun o => Nat.blt o.1 nl && Nat.blt o.2.1 nl && Nat.beq (gget t' o.1) s.V &&
      Nat.beq (gget t' o.2.1) s.V)

/-- Check: (all OK, packed histogram, number of moves, final state). -/
def progChk (nl : ℕ) (mvOK : ℕ → ℕ → ℕ → Bool) (wd : ℕ → ℕ → ℕ → ℕ) :
    List Spec → BT → Bool × ℕ × ℕ × BT
  | [], t => (true, 0, 0, t)
  | s :: ss, t =>
    let r := mvRun s.V s.ws t
    let q := progChk nl mvOK wd ss r.2
    (chunkOK nl mvOK s r.1 r.2 && q.1, hsum wd s.V r.1 + q.2.1, r.1.length + q.2.2.1, q.2.2.2)

/-! ## Semantics of `mvRun` -/

/-! ## Mapping to global chunks -/

variable {R : Type} [DecidableEq R]

/-- The global chunk of a local chunk (`labV`: chunk label codes; `lab w c`: label of wire `w`
holding code `c`). -/
noncomputable def mapChunk (ι : ℕ → R) (labV : ℕ → Lab 576) (lab : ℕ → ℕ → Lab 576) (C : LChunk) : GChunk R 576 :=
  ⟨labV C.V, C.mv.map (fun p => (ι p.1, lab p.1 p.2)),
    C.ops.map (fun o => ⟨ι o.1, ι o.2.1, ((o.2.2 : ℂ) / 2)⟩)⟩

noncomputable def mapProg (ι : ℕ → R) (labV : ℕ → Lab 576) (lab : ℕ → ℕ → Lab 576) (cs : List LChunk) :
    List (GChunk R 576) := cs.map (mapChunk ι labV lab)

/-- Correspondence of a global labelling with a code state. -/
def Corr (nl : ℕ) (ι : ℕ → R) (lab : ℕ → ℕ → Lab 576) (t : BT) (g : R → Lab 576) : Prop :=
  ∀ w < nl, g (ι w) = lab w (gget t w)

/-- Hypotheses on the local frame. -/
structure Frame (nl : ℕ) (ι : ℕ → R) (labV : ℕ → Lab 576) (lab : ℕ → ℕ → Lab 576)
    (mvOK : ℕ → ℕ → ℕ → Bool) : Prop where
  cap : nl ≤ CAP
  inj : ∀ w < nl, ∀ w' < nl, ι w = ι w' → w = w'
  labV_eq : ∀ w c, c % 4 ≠ 3 → lab w c = labV c
  sound : ∀ w o V, w < nl → V % 4 ≠ 3 → mvOK w o V = true → EdgeOK (labV V) (lab w o)

/-- The width function is the residual width of the checked moves. -/
def WidthOK (nl : ℕ) (labV : ℕ → Lab 576) (lab : ℕ → ℕ → Lab 576) (mvOK : ℕ → ℕ → ℕ → Bool)
    (wd : ℕ → ℕ → ℕ → ℕ) : Prop :=
  ∀ w o V, w < nl → V % 4 ≠ 3 → mvOK w o V = true → Fd (labV V) (lab w o) = wd w o V

variable {nl : ℕ} {ι : ℕ → R} {labV : ℕ → Lab 576} {lab : ℕ → ℕ → Lab 576}
  {mvOK : ℕ → ℕ → ℕ → Bool} {wd : ℕ → ℕ → ℕ → ℕ}

/-! ## Widths -/

/-- The move widths of a generated program (local view). -/
def progMvW (wd : ℕ → ℕ → ℕ → ℕ) (cs : List LChunk) : List ℕ :=
  cs.flatMap fun C => C.mv.map fun p => wd p.1 p.2 C.V

/-! ## Packed histograms -/

/-- Packed form of a histogram `[(w, n_w)]`. -/
def packH (H : List (ℕ × ℕ)) : ℕ := (H.map fun p => p.2 * HB ^ p.1).sum

/-- Count of `k` in a histogram. -/
def cntH (H : List (ℕ × ℕ)) (k : ℕ) : ℕ := (H.map fun p => if p.1 = k then p.2 else 0).sum

/-! ## Kernel-efficient check (tail recursive, forced accumulators) -/

/-- `x`, after forcing `n` to a literal (kernel evaluation is call-by-name). -/
def force {α : Sort*} (n : ℕ) (x : α) : α := cond (Nat.beq n 0) x x

@[simp] lemma force_eq {α : Sort*} (n : ℕ) (x : α) : force n x = x := by
  unfold force; cases Nat.beq n 0 <;> rfl

end IntMul.Kappa.R6.Cx.NetLoc

end

section
-- Source module: Solutions.R6CxNetF2
/-!
# Labels of the `h = 24` local program: codes over `𝔽₂^24` and a sound Boolean edge checker

A label code (`Code`) is one of

* `coord X`: `span {e_p : p ∈ X}`;
* `psp a b C`: `span {e_a + e_b + e_c : c ∈ C}` (a "pair span"; a line `⟨t⟩` is `psp p q {r}`);
* `perp t`: `⟨t⟩^⊥` (a triple `t`);
* `ext k`: boundary labels of stage two (decoded elsewhere).

Vectors are 24-bit naturals (`bitv`). `edgeB new old = true` implies
`NetComplexP8.EdgeOK (dec new) (dec old)` (`edgeB_sound`), with `finrank (dec c) = dimC c`
(`finrank_dec`). All functions are kernel-friendly (straight-line bit operations, SWAR popcount).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx.NetF2

open Matrix Finset Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8

abbrev V24 := Fin 24 → ZMod 2

/-! ## Popcount -/

/-- Number of set bits among the low `k` bits. -/
def cntK (k n : ℕ) : ℕ := ∑ i : Fin k, if n.testBit i then 1 else 0

/-- Recursive popcount (for `decide`). -/
def pcRec : ℕ → ℕ → ℕ
  | 0, _ => 0
  | k + 1, n => pcRec k n + (if n.testBit k then 1 else 0)

/-- SWAR popcount of a 12-bit number. -/
def swar12 (x : ℕ) : ℕ :=
  let a := x - ((x >>> 1) &&& 1365)
  let b := (a &&& 819) + ((a >>> 2) &&& 819)
  let c := (b + (b >>> 4)) &&& 3855
  (c &&& 255) + (c >>> 8)

/-- `f x` for all `x < n` (kernel-friendly loop). -/
def allLT (f : ℕ → Bool) : ℕ → Bool
  | 0 => true
  | n + 1 => f n && allLT f n

/-- Popcount of the low 24 bits. -/
def pc24 (n : ℕ) : ℕ := swar12 (n &&& 4095) + swar12 ((n >>> 12) &&& 4095)

/-! ## Vectors -/

/-- The vector of the low 24 bits of `n`. -/
def bitv (n : ℕ) : V24 := fun i => if n.testBit i then 1 else 0

/-- The unit vector `e_n` (zero if `n ≥ 24`). -/
def ev (n : ℕ) : V24 := fun i => if (i : ℕ) = n then 1 else 0

/-! ## Subspaces -/

/-- Generators `e_p`, `p ∈ X`. -/
def gC (X : ℕ) : Finset V24 := (univ.filter fun i : Fin 24 => X.testBit i).image fun i : Fin 24 => ev (i : ℕ)

/-- Generators `e_a + e_b + e_c`, `c ∈ C`. -/
def gP (a b C : ℕ) : Finset V24 :=
  (univ.filter fun c : Fin 24 => C.testBit c).image fun c : Fin 24 => ev a + ev b + ev (c : ℕ)

def coordSp (X : ℕ) : Submodule (ZMod 2) V24 := Submodule.span (ZMod 2) ↑(gC X)
def pspSp (a b C : ℕ) : Submodule (ZMod 2) V24 := Submodule.span (ZMod 2) ↑(gP a b C)
def perpSp (t : ℕ) : Submodule (ZMod 2) V24 := orth 1 (ZMod 2 ∙ bitv t)

/-- Nondegeneracy conditions of a pair span. -/
def PspOK (a b C : ℕ) : Prop := a < 24 ∧ b < 24 ∧ a ≠ b ∧ C.testBit a = false ∧ C.testBit b = false

/-! ## Codes and the Boolean checker -/

/-- Label codes. -/
inductive Code where
  | coord (X : ℕ)
  | psp (a b C : ℕ)
  | perp (t : ℕ)
  | ext (k : ℕ)

/-- Decoding a natural-number code `kind + 4 * payload`. -/
def Code.ofNat (c : ℕ) : Code :=
  cond (Nat.beq (c % 4) 0) (.coord (c / 4))
    (cond (Nat.beq (c % 4) 1) (.psp (c / 4 % 32) (c / 128 % 32) (c / 4096))
      (cond (Nat.beq (c % 4) 2) (.perp (c / 4)) (.ext (c / 4))))

/-- The subspace of a code (`ext` codes decode to `⊥` here; they are boundary labels). -/
def dec : Code → Submodule (ZMod 2) V24
  | .coord X => coordSp X
  | .psp a b C => pspSp a b C
  | .perp t => perpSp t
  | .ext _ => ⊥

/-- `2^24 - 1`. -/
def FULL : ℕ := 16777215

/-- Membership of the vector `w` in the label `V`. -/
def memB : Code → ℕ → Bool
  | .coord X, w => Nat.beq (w &&& (FULL ^^^ X)) 0
  | .psp a b C, w =>
    let D := w &&& (FULL ^^^ (2 ^ a ||| 2 ^ b))
    let pd := pc24 D % 2
    Nat.beq (D &&& (FULL ^^^ C)) 0 && Nat.beq (cond (w.testBit a) 1 0) pd &&
      Nat.beq (cond (w.testBit b) 1 0) pd
  | .perp t, w => Nat.beq (pc24 (w &&& t) % 2) 0
  | .ext _, _ => false

/-- `w` is orthogonal to the label. -/
def orthB (w : ℕ) : Code → Bool
  | .coord X => Nat.beq (w &&& X) 0
  | .psp a b C => cond ((w.testBit a).xor (w.testBit b)) (Nat.beq (C &&& (FULL ^^^ w)) 0)
      (Nat.beq (w &&& C) 0)
  | .perp t => Nat.beq w t
  | .ext _ => false

/-- Inclusion of labels. -/
def leB : Code → Code → Bool
  | .coord X, .coord Y => Nat.beq (X &&& (FULL ^^^ Y)) 0
  | .coord X, .psp _ _ _ => Nat.beq (X &&& FULL) 0
  | .coord X, .perp t => Nat.beq (X &&& t) 0
  | .psp a b C, .coord Y => Nat.beq ((2 ^ a ||| 2 ^ b ||| C) &&& (FULL ^^^ Y)) 0
  | .psp a b C, .psp a' b' C' =>
    (Nat.beq a a' && Nat.beq b b' && Nat.beq (C &&& (FULL ^^^ C')) 0) ||
      (Nat.beq (pc24 C) 1 && memB (.psp a' b' C') (2 ^ a ||| 2 ^ b ||| C))
  | .psp a b C, .perp t => cond ((t.testBit a).xor (t.testBit b)) (Nat.beq (C &&& (FULL ^^^ t)) 0)
      (Nat.beq (C &&& t) 0)
  | .perp _, .coord Y => Nat.beq Y FULL
  | _, _ => false

/-- Well-formed nondegenerate codes. -/
def okC : Code → Bool
  | .coord _ => true
  | .psp a b C => Nat.blt a 24 && Nat.blt b 24 && !(Nat.beq a b) && !(C.testBit a) && !(C.testBit b)
  | .perp t => Nat.beq (pc24 t) 3
  | .ext _ => false

/-- Dimension of a code. -/
def dimC : Code → ℕ
  | .coord X => pc24 X
  | .psp _ _ C => pc24 C
  | .perp _ => 23
  | .ext _ => 0

/-- Lowest set bit of a 24-bit number. -/
def lowbit (n : ℕ) : ℕ := n &&& (16777216 - n)

/-- Support bound of a label. -/
def xU : Code → ℕ
  | .coord X => X
  | .psp a b C => 2 ^ a ||| 2 ^ b ||| C
  | .perp _ => FULL
  | .ext _ => 0

/-- The witness candidate for an increasing edge `U → V` (checked by `witOK`). -/
def cand (U V : Code) : ℕ :=
  match V with
  | .coord Y =>
    let r := Y &&& (FULL ^^^ xU U)
    cond (Nat.beq r 0) (match U with
      | .psp a _ C => 2 ^ a ||| C
      | .perp t => t
      | _ => 0) (lowbit r)
  | .psp a b C =>
    let CU := xU U &&& (FULL ^^^ (2 ^ a ||| 2 ^ b))
    2 ^ a ||| 2 ^ b ||| lowbit (C &&& (FULL ^^^ CU))
  | .perp t => lowbit (FULL &&& (FULL ^^^ t) &&& (FULL ^^^ xU U))
  | .ext _ => 0

/-- A witness: a unit vector of `V` orthogonal to `U`. -/
def witOK (U V : Code) (w : ℕ) : Bool := memB V w && Nat.beq (pc24 w % 2) 1 && orthB w U

/-- **The edge checker** (head `V`, tail `U`). -/
def edgeB (V U : Code) : Bool :=
  okC V && okC U && ((leB U V && witOK U V (cand U V)) || (leB V U && witOK V U (cand V U)))

/-! ## Soundness -/

end IntMul.Kappa.R6.Cx.NetF2

end

section
-- Source module: Solutions.R6CxNetSpec
/-!
# The two local stage programs of the `h = 24` complex network, as chunk specs

Local wires (`nloc = 2v + R + 24 = 53280`): `x t = t`, `y S = v + S`, `a q = 2v + q`,
`m j = 2v + R + j` (`v = 2024` triples, `R = 49208` scratch slots). The data (`Dat`) is the
gate DAG `L` of S. Jain's producer (gates with their label codes), its readout pieces, the
retained slots, the triple masks and line codes. Coefficients are doubled (`k` means `k/2`).
-/

namespace IntMul.Kappa.R6.Cx.NetSpec

open NetLoc NetF2

def NV : ℕ := 2024
def NR : ℕ := 49208
def NL : ℕ := 53280

def xw (t : ℕ) : ℕ := t
def yw (S : ℕ) : ℕ := Nat.add 2024 S
def aw (q : ℕ) : ℕ := Nat.add 4048 q
def mw (j : ℕ) : ℕ := Nat.add 53256 j

/-- The `b`-bit word `i` of `D`. -/
def wget (D b i : ℕ) : ℕ := Nat.mod (Nat.shiftRight D (Nat.mul b i)) (Nat.pow 2 b)

structure Gate where
  code : ℕ
  ins : List ℕ
  outs : List ℕ

/-- The first `k` 16-bit words of `n`, and the rest. -/
def takeW (k : ℕ) : ℕ → List ℕ × ℕ :=
  Nat.rec (motive := fun _ => ℕ → List ℕ × ℕ) (fun n => ([], n))
    (fun _ ih n => let r := ih (Nat.shiftRight n 16); (Nat.mod n 65536 :: r.1, r.2)) k

/-- Gate records `[code (48 bits), #ins, #outs, ins, outs]` (16-bit words). -/
def decG (f : ℕ) : ℕ → List Gate :=
  Nat.rec (motive := fun _ => ℕ → List Gate) (fun _ => [])
    (fun _ ih n => cond (Nat.beq n 0) []
      (let n1 := Nat.shiftRight n 48
       let r1 := takeW (Nat.mod n1 65536) (Nat.shiftRight n1 32)
       let r2 := takeW (Nat.mod (Nat.shiftRight n1 16) 65536) r1.2
       ⟨Nat.mod n 281474976710656, r1.1, r2.1⟩ :: ih r2.2)) f

/-- Piece records per triple: `[#pieces, (slot, cf + 1)...]` (16-bit words). -/
def pairsP : List ℕ → List (ℕ × ℤ)
  | q :: c :: l => (q, (c : ℤ) - 1) :: pairsP l
  | _ => []

def decP (f : ℕ) : ℕ → List (List (ℕ × ℤ)) :=
  Nat.rec (motive := fun _ => ℕ → List (List (ℕ × ℤ))) (fun _ => [])
    (fun _ ih n => cond (Nat.beq n 0) []
      (let r := takeW (Nat.mul 2 (Nat.mod n 65536)) (Nat.shiftRight n 16)
       pairsP r.1 :: ih r.2)) f

/-- The data of the network. -/
structure Dat where
  tvD : ℕ
  lcD : ℕ
  srcD : ℕ
  rsD : ℕ
  tiD : ℕ
  gD : List ℕ
  pD : List ℕ

variable (d : Dat)

def Dat.tv (t : ℕ) : ℕ := wget d.tvD 24 t
def Dat.lc (t : ℕ) : ℕ := wget d.lcD 40 t
def Dat.src (t : ℕ) : ℕ := wget d.srcD 16 t
def Dat.rs (j : ℕ) : ℕ := wget d.rsD 16 j
def Dat.ti (j : ℕ) : ℕ := wget d.tiD 40 j

def gatesOf (gD : List ℕ) : List Gate := gD.flatMap (decG 4096)
def Dat.gates : List Gate := gatesOf d.gD
def Dat.pieces : List (List (ℕ × ℤ)) := d.pD.flatMap (decP 4096)

/-- `TOP` and `perp t` codes. -/
def TOPC : ℕ := 4 * 16777215
def perpC (tv : ℕ) : ℕ := 2 + 4 * tv

/-- The ops of one gate: `a_piv += a_in`, then `a_o += a_piv`. -/
def gops (g : Gate) : List (ℕ × ℕ × ℤ) :=
  ((match g.ins with
    | [p, i] => [(aw p, aw i, (2 : ℤ))]
    | _ => []) : List (ℕ × ℕ × ℤ)) ++ g.outs.tail.map (fun o => (aw o, aw (g.ins.headD 0), (2 : ℤ)))

def negOps (l : List (ℕ × ℕ × ℤ)) : List (ℕ × ℕ × ℤ) := (l.map fun o => (o.1, o.2.1, -o.2.2)).reverse

def Lops (gs : List Gate) : List (ℕ × ℕ × ℤ) := gs.flatMap gops

/-- Doubled centre coefficients `(j, k)` of the triple with mask `tv`. -/
def centreL (tv : ℕ) : List (ℕ × ℤ) :=
  cond (tv.testBit 23) ((23, -19) :: ((List.range 23).filter (fun i => !tv.testBit i)).map (·, 1))
    ((23, 2) :: ((List.range 23).filter (fun i => tv.testBit i)).map (·, -1))

def centreOps (sg : ℤ) (srcw : ℕ → ℕ) : List (ℕ × ℕ × ℤ) :=
  (List.range NV).flatMap fun S => (centreL (d.tv S)).map fun p => (yw S, srcw p.1, sg * p.2)

def pieceOpsS (sg : ℤ) (S : ℕ) (ps : List (ℕ × ℤ)) : List (ℕ × ℕ × ℤ) :=
  ps.map fun p => (yw S, aw p.1, sg * p.2)

def injOps (sg : ℤ) : List (ℕ × ℕ × ℤ) :=
  ((List.range NV).zip d.pieces).flatMap fun p => pieceOpsS sg p.1 p.2

def pieceSpecs (sg : ℤ) : List Spec :=
  ((List.range NV).zip d.pieces).map fun p =>
    ⟨perpC (d.tv p.1), yw p.1 :: p.2.map (fun q => aw q.1), pieceOpsS sg p.1 p.2⟩

def gateSpec (g : Gate) : Spec := ⟨g.code, (g.ins ++ g.outs).map aw, gops g⟩
def gateSpecInv (g : Gate) : Spec := ⟨g.code, (g.ins ++ g.outs).map aw, negOps (gops g)⟩

def xSpec (lab : ℕ → ℕ) (k : ℤ) (t : ℕ) : Spec := ⟨lab t, [aw (d.src t), xw t], [(aw (d.src t), xw t, k)]⟩

def copySpecs : List Spec :=
  (List.range 24).map fun j => ⟨d.ti j, [aw (d.rs j), mw j], [(mw j, aw (d.rs j), 2)]⟩

def allA : List ℕ := (List.range NR).map aw
def allY : List ℕ := (List.range NV).map yw
def allM : List ℕ := (List.range 24).map mw

/-! ## Stage one -/

/-- The readout of the dirty scratch is removed first (one chunk at `⊥`). -/
def pre1 : List Spec :=
  [⟨0, allA ++ allY, Lops d.gates ++ centreOps d (-1) (fun j => aw (d.rs j)) ++ injOps d (-1) ++
    negOps (Lops d.gates)⟩] ++ (List.range NV).map (xSpec d d.lc 2)

def gates1 (gD : List ℕ) : List Spec := (gatesOf gD).map gateSpec

def post1a : List Spec := copySpecs d ++ [⟨0, allM ++ allY, centreOps d 1 mw⟩] ++ pieceSpecs d 1

def post1b : List Spec :=
  [⟨TOPC, allA, negOps (Lops d.gates)⟩,
    ⟨TOPC, (List.range NV).map (fun t => aw (d.src t)) ++ (List.range NV).map xw,
      (List.range NV).map fun t => (aw (d.src t), xw t, -2)⟩]

def post1 : List Spec := post1a d ++ post1b d

def specs1 : List Spec := pre1 d ++ gates1 d.gD ++ post1 d

/-! ## Stage two -/

def pre2a : List Spec := (List.range NV).map (xSpec d (fun _ => TOPC) 2) ++ [⟨TOPC, allA, Lops d.gates⟩]

def pre2b : List Spec := pieceSpecs d (-1) ++ copySpecs d ++ [⟨0, allM ++ allY, centreOps d (-1) mw⟩]

def pre2 : List Spec := pre2a d ++ pre2b d

def gates2 (gD : List ℕ) : List Spec := (gatesOf gD).reverse.map gateSpecInv

def post2 : List Spec :=
  (List.range NV).map (xSpec d d.lc (-2)) ++
    [⟨0, allA ++ allY, Lops d.gates ++ injOps d 1 ++ centreOps d 1 (fun j => aw (d.rs j)) ++
      negOps (Lops d.gates)⟩]

def specs2 : List Spec := pre2 d ++ gates2 d.gD ++ post2 d

/-! ## Move checkers, widths and initial states -/

def dist (a b : ℕ) : ℕ := a - b + (b - a)

def mvOK1 (_w o V : ℕ) : Bool := edgeB (Code.ofNat V) (Code.ofNat o)
def wd1 (_w o V : ℕ) : ℕ := dist (dimC (Code.ofNat V)) (dimC (Code.ofNat o))

/-- Boundary moves of stage two (`o = ext k`). -/
def extOK (w k V : ℕ) : Bool :=
  cond (Nat.beq k 0) (Nat.beq V TOPC)
    (cond (Nat.beq k 1) (Nat.blt w NV && Nat.beq V TOPC)
      (cond (Nat.beq k 2) (Nat.ble NV w && Nat.blt w (2 * NV) && Nat.beq V (perpC (d.tv (w - NV))))
        false))

def mvOK2 (w o V : ℕ) : Bool :=
  cond (Nat.beq (o % 4) 3) (extOK d w (o / 4) V) (edgeB (Code.ofNat V) (Code.ofNat o))

def wd2 (_w o V : ℕ) : ℕ :=
  cond (Nat.beq (o % 4) 3) (cond (Nat.beq (o / 4) 0) 552 529)
    (dist (dimC (Code.ofNat V)) (dimC (Code.ofNat o)))

def init1 (w : ℕ) : ℕ :=
  cond (Nat.blt w NV) (d.lc w) (cond (Nat.blt w (2 * NV + NR)) 0 (d.ti (w - (2 * NV + NR))))

def init2 (w : ℕ) : ℕ :=
  cond (Nat.blt w NV) 7 (cond (Nat.blt w (2 * NV)) 11
    (cond (Nat.blt w (2 * NV + NR)) 3 (d.ti (w - (2 * NV + NR)))))

end IntMul.Kappa.R6.Cx.NetSpec

end

section
-- Source module: Solutions.R6CxNetTensor
/-!
# Lifting local labels of `𝔽₂^24` to `𝔽₂^576 = 𝔽₂^24 ⊗ 𝔽₂^24`

* `tens x y` (`x ⊗ y`), `ιR t : x ↦ x ⊗ t`, `ιL t : y ↦ t ⊗ y`; for a unit `t` both are isometries.
* Stage one (invocation `t`): `lift1 t L = L ⊗ t`; stage two: `lift2 t L = D0 t ⊔ t ⊗ L^⊥` with
  `D0 t = (t ⊗ 𝔽₂^24)^⊥`.
* `edge_lift1` / `edge_lift2`: local `EdgeOK` edges lift; `Fd_lift1` / `Fd_lift2`: residual widths
  are unchanged.
* Boundary edges (`up_E1` … `up_E5`) and the endpoint identity `lift2_line`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx.NetT

open Matrix Finset Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8 NetF2

abbrev V576 := Fin 576 → ZMod 2
abbrev L24 := Submodule (ZMod 2) V24
abbrev L576 := Submodule (ZMod 2) V576

/-- Index `(i, j) ↦ j + 24 i`. -/
def e2 : Fin 24 × Fin 24 ≃ Fin 576 := finProdFinEquiv

/-- `x ⊗ y`. -/
def tens (x y : V24) : V576 := fun k => x (e2.symm k).1 * y (e2.symm k).2

/-- `x ↦ x ⊗ t`. -/
def ιR (t : V24) : V24 →ₗ[ZMod 2] V576 where
  toFun x := tens x t
  map_add' x y := by funext k; simp [tens, add_mul]
  map_smul' c _ := by funext k; simp [tens, mul_assoc]

/-- `y ↦ t ⊗ y`. -/
def ιL (t : V24) : V24 →ₗ[ZMod 2] V576 where
  toFun y := tens t y
  map_add' x y := by funext k; simp [tens, mul_add]
  map_smul' c _ := by funext k; simp [tens]; ring

@[simp] lemma ιR_apply (t x : V24) : ιR t x = tens x t := rfl
@[simp] lemma ιL_apply (t y : V24) : ιL t y = tens t y := rfl

/-- An isometry. -/
def IsoM (ι : V24 →ₗ[ZMod 2] V576) : Prop := ∀ x y, ι x ⬝ᵥ ι y = x ⬝ᵥ y

variable {ι : V24 →ₗ[ZMod 2] V576}

/-! ## The two lifts -/

def lift1 (t : V24) (L : L24) : L576 := L.map (ιR t)

/-- `D0 t = (t ⊗ 𝔽₂^24)^⊥`. -/
def D0 (t : V24) : L576 := orth 1 ((⊤ : L24).map (ιL t))

def lift2 (t : V24) (L : L24) : L576 := D0 t ⊔ (orth 1 L).map (ιL t)

variable {t : V24}

/-! ## Boundary edges -/

/-- The line `⟨u⟩` and its complement. -/
def lineM {n : ℕ} (u : Fin n → ZMod 2) : Submodule (ZMod 2) (Fin n → ZMod 2) := ZMod 2 ∙ u

/-- `e_p ⊗ e_q`. -/
def evv (p q : Fin 24) : V576 := tens (ev p) (ev q)

end IntMul.Kappa.R6.Cx.NetT

end

section
-- Source module: Solutions.R6CxNetFrame
/-!
# Local frames of the two stage invocations

Stage one, invocation `b`: code `c` means `lift1 t_b (dec c)`. Stage two, invocation `a`: code `c`
means `lift2 t_a (dec c)`, except the boundary codes `ext k` of the incoming wires:
`ext 0` (fresh scratch) `= ⊥`, `ext 1` on `x_b` `= lift1 t_b (perp t_a)` (stage-one `y` output),
`ext 2` on `y_S` `= lift1 t_S ⊤` (stage-one `x` output).

`frame1` / `frame2`: the `NetLoc.Frame` hypotheses (move soundness via `edgeB_sound`, the lifts and
the boundary edges E1–E3); `width1` / `width2`: `WidthOK`.
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Cx.NetFr

open Matrix Finset Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8 NetF2 NetT NetLoc
  NetSpec

/-! ## Triple vectors -/

/-- The data facts on the triple masks. -/
structure TriOK (d : Dat) : Prop where
  pc : ∀ S < NV, cntK 24 (d.tv S) = 3
  line : ∀ S < NV, NetF2.dec (Code.ofNat (d.lc S)) = lineM (bitv (d.tv S))

variable {d : Dat}

/-- The triple vector `t_S`. -/
def tb (d : Dat) (S : ℕ) : V24 := bitv (d.tv S)

/-! ## Stage one -/

/-- Labels of stage-one invocation `b`. -/
def labV1 (d : Dat) (b : ℕ) (c : ℕ) : L576 := lift1 (tb d b) (NetF2.dec (Code.ofNat c))

/-! ## Stage two -/

/-- Chunk labels of stage-two invocation `a`. -/
def labV2 (d : Dat) (a : ℕ) (c : ℕ) : L576 := lift2 (tb d a) (NetF2.dec (Code.ofNat c))

/-- Boundary labels `ext k` of stage-two invocation `a` on wire `w`. -/
def extLab (d : Dat) (a w k : ℕ) : L576 :=
  if k = 0 then ⊥ else if k = 1 then lift1 (tb d w) (NetF2.dec (Code.ofNat (perpC (d.tv a))))
  else lift1 (tb d (w - NV)) (NetF2.dec (Code.ofNat TOPC))

/-- Wire labels of stage-two invocation `a`. -/
def lab2 (d : Dat) (a w c : ℕ) : L576 := if c % 4 = 3 then extLab d a w (c / 4) else labV2 d a c

end IntMul.Kappa.R6.Cx.NetFr

end

section
-- Source module: Solutions.R6CxNetRoles
/-!
# Global roles of the complex network and the invocation maps

Data roles (`W = 2N + 2vR`): `X(a,b)`, `Y(a,b)` (`a, b < v`), `A1(b,q)`, `A2(a,q)` (`q < R`).
Temporaries (`T = 48v + N`): `M1(b,j)`, `M2(a,j)` (`j < 24`), `τ(a,b)`.

`ι1 b` maps the local wires of stage-one invocation `b` (`x_t ↦ X(t,b)`, `y_S ↦ Y(S,b)`,
`a_q ↦ A1(b,q)`, `m_j ↦ M1(b,j)`), `ι2 a` those of stage-two invocation `a`
(`x_b ↦ Y(a,b)`, `y_S ↦ X(a,S)`, `a_q ↦ A2(a,q)`, `m_j ↦ M2(a,j)`). `g0`: the initial labels.
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Cx.NetFr

open Matrix Finset Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8 NetF2 NetT NetLoc
  NetSpec

def NN : ℕ := NV * NV
def Wn : ℕ := 207387136
def Tn : ℕ := 4193728

/-- The roles. -/
abbrev Rl := Fin Wn ⊕ Fin Tn

def rW (n : ℕ) : Rl := Sum.inl ⟨n % Wn, Nat.mod_lt _ (by norm_num [Wn])⟩
def rT (n : ℕ) : Rl := Sum.inr ⟨n % Tn, Nat.mod_lt _ (by norm_num [Tn])⟩

/-! ## Role indices -/

def xI (a b : ℕ) : ℕ := a * NV + b
def yI (a b : ℕ) : ℕ := NN + a * NV + b
def a1I (b q : ℕ) : ℕ := 2 * NN + b * NR + q
def a2I (a q : ℕ) : ℕ := 2 * NN + NV * NR + a * NR + q
def m1I (b j : ℕ) : ℕ := 24 * b + j
def m2I (a j : ℕ) : ℕ := 24 * NV + 24 * a + j
def τI (a b : ℕ) : ℕ := 48 * NV + a * NV + b

def Xr (a b : ℕ) : Rl := rW (xI a b)
def Yr (a b : ℕ) : Rl := rW (yI a b)
def A1r (b q : ℕ) : Rl := rW (a1I b q)
def A2r (a q : ℕ) : Rl := rW (a2I a q)
def M1r (b j : ℕ) : Rl := rT (m1I b j)
def M2r (a j : ℕ) : Rl := rT (m2I a j)
def τr (a b : ℕ) : Rl := rT (τI a b)

/-- Stage-one invocation `b`. -/
def ι1 (b w : ℕ) : Rl :=
  if w < NV then Xr w b else if w < 2 * NV then Yr (w - NV) b
  else if w < 2 * NV + NR then A1r b (w - 2 * NV) else M1r b (w - (2 * NV + NR))

/-- Stage-two invocation `a`. -/
def ι2 (a w : ℕ) : Rl :=
  if w < NV then Yr a w else if w < 2 * NV then Xr a (w - NV)
  else if w < 2 * NV + NR then A2r a (w - 2 * NV) else M2r a (w - (2 * NV + NR))

/-- A numeric code of a role (injective). -/
def rc : Rl → ℕ
  | Sum.inl n => n.val
  | Sum.inr n => Wn + n.val

lemma rc_rW {n : ℕ} (h : n < Wn) : rc (rW n) = n := by simp [rc, rW, Nat.mod_eq_of_lt h]

/-- The numeric code of `ι1 b w`. -/
def f1 (b w : ℕ) : ℕ :=
  if w < NV then xI w b else if w < 2 * NV then yI (w - NV) b
  else if w < 2 * NV + NR then a1I b (w - 2 * NV) else Wn + m1I b (w - (2 * NV + NR))

def f2 (a w : ℕ) : ℕ :=
  if w < NV then yI a w else if w < 2 * NV then xI a (w - NV)
  else if w < 2 * NV + NR then a2I a (w - 2 * NV) else Wn + m2I a (w - (2 * NV + NR))

/-- Decoding the numeric code of a stage-one role: `(b, w)`. -/
def d1 (n : ℕ) : ℕ × ℕ :=
  if n < NN then (n % NV, n / NV)
  else if n < 2 * NN then ((n - NN) % NV, NV + (n - NN) / NV)
  else if n < Wn then ((n - 2 * NN) / NR, 2 * NV + (n - 2 * NN) % NR)
  else ((n - Wn) / 24, 2 * NV + NR + (n - Wn) % 24)

/-- Decoding the numeric code of a stage-two role: `(a, w)`. -/
def d2 (n : ℕ) : ℕ × ℕ :=
  if n < NN then (n / NV, NV + n % NV)
  else if n < 2 * NN then ((n - NN) / NV, (n - NN) % NV)
  else if n < Wn then ((n - (2 * NN + NV * NR)) / NR, 2 * NV + (n - (2 * NN + NV * NR)) % NR)
  else ((n - (Wn + 24 * NV)) / 24, 2 * NV + NR + (n - (Wn + 24 * NV)) % 24)

end IntMul.Kappa.R6.Cx.NetFr

end

section
-- Source module: Solutions.R6CxNetDataMDec
/-!
# Snapshot chunk decoder for the mask value trees
-/

namespace IntMul.Kappa.R6.Cx.NetMask

open NetBT NetLoc

/-- Stream decoder for snapshot literals: a subtree of depth `d` whose leaves (in order) are stored
as `(12-bit length, value)` records, low first. -/
def decS (d : ℕ) : (BT → ℕ → BT) → ℕ → BT :=
  Nat.rec (motive := fun _ => (BT → ℕ → BT) → ℕ → BT)
    (fun k n => k (.leaf (Nat.mod (Nat.shiftRight n 12) (Nat.pow 2 (Nat.mod n 4096))))
      (Nat.shiftRight (Nat.shiftRight n 12) (Nat.mod n 4096)))
    (fun _ ih k n => ih (fun l n' => force n' (ih (fun r n'' => k (.node l r) n'') n')) n) d

/-- A depth-6 chunk of a snapshot (the low 64 bits are a random salt: the kernel hashes a
numeral by its low bits, and colliding hashes make its caches quadratic). -/
def QS (n : ℕ) : BT := decS 6 (fun t _ => t) (Nat.shiftRight n 64)

end IntMul.Kappa.R6.Cx.NetMask

end

section
-- Source module: Solutions.R6CxNetFast
/-!
# A kernel-fast form of `progChk` (moves only)

`progK` runs the moves of a spec list in continuation-passing style, with recursor-based tree
access written in raw `Nat` primitives and forced accumulators (kernel evaluation is
call-by-name). The op condition of `chunkOK` is not evaluated: it follows from `OpsIn` (every op
wire is one of the spec's wires, hence at `V` after the moves).

`progK_sound`: a passing `progK` gives a passing `progChk`, and the continuation holds at the
final state with the accumulated packed histogram and move count.
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Cx.NetFast

noncomputable section

open NetBT NetLoc

def lgetR (v j : ℕ) : ℕ := Nat.mod (Nat.shiftRight v (Nat.mul 40 j)) SM
def lsetR (v j x : ℕ) : ℕ := Nat.xor v (Nat.shiftLeft (Nat.xor (lgetR v j) x) (Nat.mul 40 j))

def getR (t : BT) : ℕ → ℕ → ℕ :=
  BT.rec (motive := fun _ => ℕ → ℕ → ℕ) (fun v _ j => lgetR v j)
    (fun _ _ ihl ihr p j => cond (Nat.beq (Nat.mod p 2) 0) (ihl (Nat.div p 2) j) (ihr (Nat.div p 2) j)) t

def setR (t : BT) : ℕ → ℕ → ℕ → BT :=
  BT.rec (motive := fun _ => ℕ → ℕ → ℕ → BT) (fun v _ j x => .leaf (lsetR v j x))
    (fun l r ihl ihr p j x => cond (Nat.beq (Nat.mod p 2) 0) (.node (ihl (Nat.div p 2) j x) r)
      (.node l (ihr (Nat.div p 2) j x))) t

def ggR (t : BT) (i : ℕ) : ℕ := getR t (Nat.div i 256) (Nat.mod i 256)
def gsR (t : BT) (i x : ℕ) : BT := setR t (Nat.div i 256) (Nat.mod i 256) x

/-- Structural equality, recursor form. -/
def beqR (a : BT) : BT → Bool :=
  BT.rec (motive := fun _ => BT → Bool)
    (fun v b => BT.rec (motive := fun _ => Bool) (fun w => Nat.beq v w) (fun _ _ _ _ => false) b)
    (fun _ _ ihl ihr b => BT.rec (motive := fun _ => Bool) (fun _ => false)
      (fun l' r' _ _ => ihl l' && ihr r') b) a

/-- Moves of `ws` to `V`, then the continuation `k`. -/
def mvK (nl : ℕ) (mvOK : ℕ → ℕ → ℕ → Bool) (wd : ℕ → ℕ → ℕ → ℕ) (V : ℕ) (k : BT → ℕ → ℕ → Bool)
    (ws : List ℕ) : BT → ℕ → ℕ → Bool :=
  List.rec (motive := fun _ => BT → ℕ → ℕ → Bool) k
    (fun w _ ih t h c =>
      cond (Nat.blt w nl)
        (let o := ggR t w
         cond (Nat.beq o V) (ih t h c)
          (cond (mvOK w o V)
            (let t' := gsR t w V
             let h' := Nat.add (Nat.pow HB (wd w o V)) h
             let c' := Nat.succ c
             force h' (force c' (ih t' h' c'))) false)) false) ws

/-- The spec list, then the continuation `k`. -/
def progK (nl : ℕ) (mvOK : ℕ → ℕ → ℕ → Bool) (wd : ℕ → ℕ → ℕ → ℕ) (k : BT → ℕ → ℕ → Bool)
    (ss : List Spec) : BT → ℕ → ℕ → Bool :=
  List.rec (motive := fun _ => BT → ℕ → ℕ → Bool) k
    (fun s _ ih t h c =>
      cond (Nat.blt s.V SM && !(Nat.beq (Nat.mod s.V 4) 3)) (mvK nl mvOK wd s.V ih s.ws t h c) false) ss

/-- The final continuation of a checked segment: packed histogram `H`, `C` moves, final state `S`. -/
def finK (H C : ℕ) (S : BT) (t : BT) (h c : ℕ) : Bool := Nat.beq h H && Nat.beq c C && beqR t S

/-- Every op wire of a spec is one of its wires. -/
def OpsIn (s : Spec) : Prop := ∀ o ∈ s.ops, o.1 ∈ s.ws ∧ o.2.1 ∈ s.ws

end

end IntMul.Kappa.R6.Cx.NetFast

end

section
-- Source module: Solutions.R6CxNetMask
/-!
# The scalar identity of the local program by a kernel mask simulation

The gate DAG `L` of the local program is run on **spread** inputs: slot `src t` receives
`256^t` (the coefficient vector `e_t` in base 256), each gate op `a_q += a_r` adds the encoded
vectors, and every intermediate vector is checked to have digits in `{0, 1}` (`Nat.land v LO = v`).
The readout check compares `∑ k · a` with `2 · 256^S` for every triple `S`.

* `vget` / `vset`: one value per leaf of a binary tree (recursor form, raw primitives).
* `enc f = ∑_{t < NV} f t · 256^t`; `simK_sound`: the kernel run encodes `runP ops C`, the run on
  coefficient vectors, and keeps all digits in `{0, 1}`.
* `readChk_sound`: the readout identity on coefficient vectors.
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Cx.NetMask

open NetBT NetSpec NetLoc Finset

noncomputable section

/-! ## Value trees -/

def vget (t : BT) : ℕ → ℕ :=
  BT.rec (motive := fun _ => ℕ → ℕ) (fun v _ => v)
    (fun _ _ ihl ihr p => cond (Nat.beq (Nat.mod p 2) 0) (ihl (Nat.div p 2)) (ihr (Nat.div p 2))) t

def vset (t : BT) : ℕ → ℕ → BT :=
  BT.rec (motive := fun _ => ℕ → ℕ → BT) (fun _ _ x => .leaf x)
    (fun l r ihl ihr p x => cond (Nat.beq (Nat.mod p 2) 0) (.node (ihl (Nat.div p 2) x) r)
      (.node l (ihr (Nat.div p 2) x))) t

/-- The zero tree of depth `d` (recursor form). -/
def mkR (d : ℕ) : BT := Nat.rec (motive := fun _ => BT) (.leaf 0) (fun _ ih => .node ih ih) d

/-! ## Bit vectors -/

/-- The 0/1 coefficient vector of the bits of `v`. -/
def bvec (v : ℕ) : ℕ → ℕ := fun u => if v.testBit u then 1 else 0

/-! ## The run on coefficient vectors and its kernel form -/

/-- Gate ops on slots `a_q += a_r`. -/
def runP (ops : List (ℕ × ℕ)) (C : ℕ → ℕ → ℕ) : ℕ → ℕ → ℕ :=
  ops.foldl (fun C o => Function.update C o.1 (C o.1 + C o.2)) C

/-- The kernel run (slots `< NR`, the two summands have disjoint supports). -/
def simK (k : BT → Bool) (ops : List (ℕ × ℕ)) : BT → Bool :=
  List.rec (motive := fun _ => BT → Bool) k
    (fun o _ ih t =>
      cond (Nat.blt o.1 NR && Nat.blt o.2 NR && !(Nat.beq o.1 o.2))
        (let a := vget t o.1
         let b := vget t o.2
         cond (Nat.beq (Nat.land a b) 0) (ih (vset t o.1 (Nat.lor a b))) false) false) ops

/-- Tree `t` holds the coefficient vectors `C` as bit vectors (slots `< 2^16`). -/
def Enc (t : BT) (C : ℕ → ℕ → ℕ) : Prop := t.wf 16 = true ∧ ∀ q < 2 ^ 16, C q = bvec (vget t q)

/-! ## Placement of the inputs -/

/-- `C₀`: slot `src t` receives `e_t`, for `t < n`. -/
def place (src : ℕ → ℕ) : ℕ → ℕ → ℕ → ℕ
  | 0 => fun _ _ => 0
  | n + 1 => Function.update (place src n) (src n) (place src n (src n) + fun t => if t = n then 1 else 0)

/-- Kernel form of the placement. -/
def placeK (src : ℕ → ℕ) (n : ℕ) : BT :=
  Nat.rec (motive := fun _ => BT) (mkR 16)
    (fun t ih => vset ih (src t) (Nat.lor (vget ih (src t)) (Nat.pow 2 t))) n

/-! ## The readout check (bit-sliced counters) -/

/-- Add the bit vector `c` to the bit-sliced counter `ps` (planes, low first). -/
def add1 : List ℕ → ℕ → List ℕ
  | [], _ => []
  | p :: ps, c => Nat.xor p c :: add1 ps (Nat.land p c)

/-- The counter value at position `u`. -/
def cnt : List ℕ → ℕ → ℕ
  | [], _ => 0
  | p :: ps, u => bvec p u + 2 * cnt ps u

/-- Add `c` to the counter `k` times. -/
def addK (c : ℕ) (k : ℕ) (ps : List ℕ) : List ℕ := Nat.rec (motive := fun _ => List ℕ) ps (fun _ ih => add1 ih c) k

/-- Accumulate the terms `(slot, k)` (`k⁺` copies, or `k⁻` copies when `neg`). -/
def accK (t : BT) (neg : Bool) (L : List (ℕ × ℤ)) : List ℕ → List ℕ :=
  List.rec (motive := fun _ => List ℕ → List ℕ) (fun ps => ps)
    (fun p _ ih ps => ih (addK (vget t p.1) (Int.toNat (cond neg (-p.2) p.2)) ps)) L

/-- The weight of a sign class. -/
def wK (neg : Bool) (L : List (ℕ × ℤ)) : ℕ := (L.map fun p => Int.toNat (cond neg (-p.2) p.2)).sum

def beqL : List ℕ → List ℕ → Bool
  | [], [] => true
  | a :: l, b :: l' => Nat.beq a b && beqL l l'
  | _, _ => false

/-- Six zero planes (counters `< 64`). -/
def Z6 : List ℕ := [0, 0, 0, 0, 0, 0]

/-- The readout of triple `S` is `2 e_S` (terms `(slot, doubled coefficient)`, slots `< NR`). -/
def rdS (t : BT) (S : ℕ) (L : List (ℕ × ℤ)) : Bool :=
  L.all (fun p => Nat.blt p.1 NR) && Nat.blt (wK false L) 62 && Nat.blt (wK true L) 62 &&
    beqL (accK t false L Z6) (add1 (add1 (accK t true L Z6) (Nat.pow 2 S)) (Nat.pow 2 S))

/-- All elements. -/
def allR {α : Type} (p : α → Bool) (l : List α) : Bool :=
  List.rec (motive := fun _ => Bool) true (fun a _ ih => p a && ih) l

/-! ## The check for the data -/

/-- Slot form of the gate ops. -/
def gq (g : Gate) : List (ℕ × ℕ) :=
  (match g.ins with
    | [p, i] => [(p, i)]
    | _ => []) ++ g.outs.tail.map (fun o => (o, g.ins.headD 0))

/-- Readout terms `(S, [(slot, doubled coefficient)])` of stage one. -/
def rdTerms (d : Dat) : List (ℕ × List (ℕ × ℤ)) :=
  ((List.range NV).zip d.pieces).map fun p =>
    (p.1, (centreL (d.tv p.1)).map (fun c => (d.rs c.1, c.2)) ++ p.2)

/-- The slot ops of a gate data segment. -/
def gqs (gD : List ℕ) : List (ℕ × ℕ) := (gatesOf gD).flatMap gq

end

end IntMul.Kappa.R6.Cx.NetMask

end

section
-- Source module: Solutions.R6CxNetScal
/-!
# The scalar effect of the local stage programs

Local ops `(dst, src, k)` act by `z_dst += (k/2) z_src` (`runL`). Generic facts: linearity,
commuting with linear maps, inverses (`negOps`), parallel blocks (`padd`), relabelling to global
roles (`runOps_map`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx.NetScal

open NetSpec NetMask Finset

variable {Vt : Type*} [AddCommGroup Vt] [Module ℂ Vt]

/-- The coefficient of a local op. -/
noncomputable def cf (o : ℕ × ℕ × ℤ) : ℂ := (o.2.2 : ℂ) / 2

noncomputable def stepL (Λ : ℕ → Vt) (o : ℕ × ℕ × ℤ) : ℕ → Vt :=
  Function.update Λ o.1 (Λ o.1 + cf o • Λ o.2.1)

noncomputable def runL (l : List (ℕ × ℕ × ℤ)) (Λ : ℕ → Vt) : ℕ → Vt := l.foldl stepL Λ

@[simp] lemma runL_nil (Λ : ℕ → Vt) : runL [] Λ = Λ := rfl

/-- Wires written by `l`. -/
def dsts (l : List (ℕ × ℕ × ℤ)) : List ℕ := l.map (·.1)

/-- The effect of a parallel block. -/
noncomputable def padd (l : List (ℕ × ℕ × ℤ)) (Λ : ℕ → Vt) : ℕ → Vt :=
  fun w => Λ w + (l.map fun o => if o.1 = w then cf o • Λ o.2.1 else 0).sum

/-! ## Relabelling to global roles -/

variable {R : Type} [DecidableEq R]

/-- The global op of a local op. -/
noncomputable def toG (ι : ℕ → R) (o : ℕ × ℕ × ℤ) : GOp R := ⟨ι o.1, ι o.2.1, cf o⟩

end IntMul.Kappa.R6.Cx.NetScal

end

section
-- Source module: Solutions.R6CxNetEff
/-!
# The scalar effect of the two stage programs

For the local wires (`x_t = t`, `y_S = 2024 + S`, `a_q = 4048 + q`, `m_j = 53256 + j`) and any state
`Λ` with clean temporaries (`Λ (m_j) = 0`), the ops of `specs1` give `y_S ↦ y_S + x_S` and those of
`specs2` give `y_S ↦ y_S − x_S`, while `x` and the dirty scratch `a` are restored. The data enter
through `DatOK` (checked by the kernel) and the mask identity `MaskOK` (`R6CxNetMaskAll`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx.NetEff

open NetSpec NetMask NetScal NetLoc Finset

/-! ## List sums -/

/-! ## Wires -/

/-! ## Placement -/

/-! ## Gate ops on coefficient vectors -/

variable {Vt : Type*} [AddCommGroup Vt] [Module ℂ Vt]

/-- Slot ops `(q, r)` as local ops `a_q += a_r` (`k = 2`, coefficient `1`). -/
def slotOps (l : List (ℕ × ℕ)) : List (ℕ × ℕ × ℤ) := l.map fun o => (aw o.1, aw o.2, 2)

/-! ## Readouts -/

variable (d : Dat)

/-- The readout terms of triple `S`: `(slot, doubled coefficient)`. -/
def rdL (S : ℕ) : List (ℕ × ℤ) := (centreL (d.tv S)).map (fun c => (d.rs c.1, c.2)) ++ d.pieces.getD S []

/-- The readout value of triple `S` on a state. -/
noncomputable def rdV (Λ : ℕ → Vt) (S : ℕ) : Vt := ((rdL d S).map fun p => ((p.2 : ℂ) / 2) • Λ (aw p.1)).sum

/-! ## Junk functions and the gate block -/

/-- `J` vanishes on the scratch wires `a_q`, `q < NR`. -/
def OffA (J : ℕ → Vt) : Prop := ∀ q < NR, J (aw q) = 0

/-- The gate data facts used here. -/
def GOK (gl : List (ℕ × ℕ)) : Prop := ∀ o ∈ gl, o.1 < NR ∧ o.2 < NR ∧ o.1 ≠ o.2

/-! ## Parallel blocks -/

/-- The increment of a parallel block. -/
noncomputable def dl (l : List (ℕ × ℕ × ℤ)) (Λ : ℕ → Vt) : ℕ → Vt :=
  fun w => (l.map fun o => if o.1 = w then cf o • Λ o.2.1 else 0).sum

/-! ## The blocks of the stage programs -/

/-- `a_{src t} += (k/2) x_t`. -/
def XS (k : ℤ) : List (ℕ × ℕ × ℤ) := (List.range NV).map fun t => (aw (d.src t), xw t, k)

/-- `m_j += a_{rs j}`. -/
def CP : List (ℕ × ℕ × ℤ) := (List.range 24).map fun j => (mw j, aw (d.rs j), 2)

/-- A readout block. -/
def RB (sg : ℤ) (srcw : ℕ → ℕ) : List (ℕ × ℕ × ℤ) := centreOps d sg srcw ++ injOps d sg

/-- The readout with centre wires `srcw`. -/
noncomputable def rdVs (srcw : ℕ → ℕ) (Λ : ℕ → Vt) (S : ℕ) : Vt :=
  ((centreL (d.tv S)).map fun c => ((c.2 : ℂ) / 2) • Λ (srcw c.1)).sum +
    ((d.pieces.getD S []).map fun p => ((p.2 : ℂ) / 2) • Λ (aw p.1)).sum

/-! ## Facts about the blocks -/

/-- The mask identity (checked by the kernel in `R6CxNetMaskAll`). -/
def MaskOK : Prop :=
  ∀ S < NV, ∀ u, ((rdL d S).map fun p => p.2 * (runP (d.gates.flatMap gq) (place d.src NV) p.1 u : ℤ)).sum =
    if u = S then 2 else 0

/-- Readout slots are in range. -/
def RdOK : Prop := (∀ j < 24, d.rs j < NR) ∧ ∀ S < NV, ∀ p ∈ d.pieces.getD S [], p.1 < NR

/-! ## The op lists of the stages -/

/-! ## Stage effects -/

/-- Centre and piece parts of the readout. -/
noncomputable def cPart (srcw : ℕ → ℕ) (Λ : ℕ → Vt) (S : ℕ) : Vt :=
  ((centreL (d.tv S)).map fun c => ((c.2 : ℂ) / 2) • Λ (srcw c.1)).sum
noncomputable def pPart (Λ : ℕ → Vt) (S : ℕ) : Vt :=
  ((d.pieces.getD S []).map fun p => ((p.2 : ℂ) / 2) • Λ (aw p.1)).sum

end IntMul.Kappa.R6.Cx.NetEff

end

section
-- Source module: Solutions.R6CxNetRaw
/-!
# Raw-primitive forms of the label checkers (for kernel evaluation)

The checkers of `NetF2` / `NetSpec` written with `Nat.land`, `Nat.shiftRight`, ... directly
(no type-class instances to unfold), with equality lemmas to the originals.
-/

namespace IntMul.Kappa.R6.Cx.NetRaw

open NetF2 NetSpec

def tbR (m n : ℕ) : Bool := !(Nat.beq (Nat.land 1 (Nat.shiftRight m n)) 0)

def swarR (x : ℕ) : ℕ :=
  let a := Nat.sub x (Nat.land (Nat.shiftRight x 1) 1365)
  let b := Nat.add (Nat.land a 819) (Nat.land (Nat.shiftRight a 2) 819)
  let c := Nat.land (Nat.add b (Nat.shiftRight b 4)) 3855
  Nat.add (Nat.land c 255) (Nat.shiftRight c 8)

def pcR (n : ℕ) : ℕ := Nat.add (swarR (Nat.land n 4095)) (swarR (Nat.land (Nat.shiftRight n 12) 4095))

def FULLR : ℕ := 16777215

def memR : Code → ℕ → Bool
  | .coord X, w => Nat.beq (Nat.land w (Nat.xor FULLR X)) 0
  | .psp a b C, w =>
    let D := Nat.land w (Nat.xor FULLR (Nat.lor (Nat.pow 2 a) (Nat.pow 2 b)))
    let pd := Nat.mod (pcR D) 2
    Nat.beq (Nat.land D (Nat.xor FULLR C)) 0 && Nat.beq (cond (tbR w a) 1 0) pd &&
      Nat.beq (cond (tbR w b) 1 0) pd
  | .perp t, w => Nat.beq (Nat.mod (pcR (Nat.land w t)) 2) 0
  | .ext _, _ => false

def orthR (w : ℕ) : Code → Bool
  | .coord X => Nat.beq (Nat.land w X) 0
  | .psp a b C => cond (Bool.xor (tbR w a) (tbR w b)) (Nat.beq (Nat.land C (Nat.xor FULLR w)) 0)
      (Nat.beq (Nat.land w C) 0)
  | .perp t => Nat.beq w t
  | .ext _ => false

def leR : Code → Code → Bool
  | .coord X, .coord Y => Nat.beq (Nat.land X (Nat.xor FULLR Y)) 0
  | .coord X, .psp _ _ _ => Nat.beq (Nat.land X FULLR) 0
  | .coord X, .perp t => Nat.beq (Nat.land X t) 0
  | .psp a b C, .coord Y => Nat.beq (Nat.land (Nat.lor (Nat.lor (Nat.pow 2 a) (Nat.pow 2 b)) C) (Nat.xor FULLR Y)) 0
  | .psp a b C, .psp a' b' C' =>
    (Nat.beq a a' && Nat.beq b b' && Nat.beq (Nat.land C (Nat.xor FULLR C')) 0) ||
      (Nat.beq (pcR C) 1 && memR (.psp a' b' C') (Nat.lor (Nat.lor (Nat.pow 2 a) (Nat.pow 2 b)) C))
  | .psp a b C, .perp t => cond (Bool.xor (tbR t a) (tbR t b)) (Nat.beq (Nat.land C (Nat.xor FULLR t)) 0)
      (Nat.beq (Nat.land C t) 0)
  | .perp _, .coord Y => Nat.beq Y FULLR
  | _, _ => false

def okR : Code → Bool
  | .coord _ => true
  | .psp a b C => Nat.blt a 24 && Nat.blt b 24 && !(Nat.beq a b) && !(tbR C a) && !(tbR C b)
  | .perp t => Nat.beq (pcR t) 3
  | .ext _ => false

def dimR : Code → ℕ
  | .coord X => pcR X
  | .psp _ _ C => pcR C
  | .perp _ => 23
  | .ext _ => 0

def lowbitR (n : ℕ) : ℕ := Nat.land n (Nat.sub 16777216 n)

def xUR : Code → ℕ
  | .coord X => X
  | .psp a b C => Nat.lor (Nat.lor (Nat.pow 2 a) (Nat.pow 2 b)) C
  | .perp _ => FULLR
  | .ext _ => 0

def candR (U V : Code) : ℕ :=
  match V with
  | .coord Y =>
    let r := Nat.land Y (Nat.xor FULLR (xUR U))
    cond (Nat.beq r 0) (match U with
      | .psp a _ C => Nat.lor (Nat.pow 2 a) C
      | .perp t => t
      | _ => 0) (lowbitR r)
  | .psp a b C =>
    let CU := Nat.land (xUR U) (Nat.xor FULLR (Nat.lor (Nat.pow 2 a) (Nat.pow 2 b)))
    Nat.lor (Nat.lor (Nat.pow 2 a) (Nat.pow 2 b)) (lowbitR (Nat.land C (Nat.xor FULLR CU)))
  | .perp t => lowbitR (Nat.land (Nat.land FULLR (Nat.xor FULLR t)) (Nat.xor FULLR (xUR U)))
  | .ext _ => 0

def witR (U V : Code) (w : ℕ) : Bool := memR V w && Nat.beq (Nat.mod (pcR w) 2) 1 && orthR w U

def edgeR (V U : Code) : Bool :=
  okR V && okR U && ((leR U V && witR U V (candR U V)) || (leR V U && witR V U (candR V U)))

def ofNatR (c : ℕ) : Code :=
  cond (Nat.beq (Nat.mod c 4) 0) (.coord (Nat.div c 4))
    (cond (Nat.beq (Nat.mod c 4) 1) (.psp (Nat.mod (Nat.div c 4) 32) (Nat.mod (Nat.div c 128) 32) (Nat.div c 4096))
      (cond (Nat.beq (Nat.mod c 4) 2) (.perp (Nat.div c 4)) (.ext (Nat.div c 4))))

def distR (a b : ℕ) : ℕ := Nat.add (Nat.sub a b) (Nat.sub b a)

def mvOK1R (_w o V : ℕ) : Bool := edgeR (ofNatR V) (ofNatR o)
def wd1R (_w o V : ℕ) : ℕ := distR (dimR (ofNatR V)) (dimR (ofNatR o))

variable (d : Dat)

def mvOK2R (w o V : ℕ) : Bool :=
  cond (Nat.beq (Nat.mod o 4) 3) (extOK d w (Nat.div o 4) V) (edgeR (ofNatR V) (ofNatR o))

def wd2R (w o V : ℕ) : ℕ :=
  cond (Nat.beq (Nat.mod o 4) 3) (cond (Nat.beq (Nat.div o 4) 0) 552 529) (wd1R w o V)

end IntMul.Kappa.R6.Cx.NetRaw

end

section
-- Source module: Solutions.R6CxNetChk1_0
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 0 of stage 1 (`{1: 2024}`). -/
def H1_0 : ℕ := 0x7e800000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_1
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 1 of stage 1 (`{1: 13804, 2: 1439, 3: 452, 5: 678, 6: 281}`). -/
def H1_1 : ℕ := 0x119002a600000001c40059f035ec00000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_2
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 2 of stage 1 (`{1: 1332, 2: 3827, 3: 428, 5: 652, 6: 421, 4: 1564, 8: 1049, 10: 352, 12: 322, 16: 201, 20: 32, 14: 224, 18: 72}`). -/
def H1_2 : ℕ := 0x20000000004800000000c900000000e000000001420000000160000000041900000001a50028c0061c001ac00ef30053400000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_3
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 3 of stage 1 (`{4: 775, 12: 270, 8: 251, 16: 223, 2: 2184, 22: 11, 18: 280, 20: 180, 14: 228, 7: 355, 9: 160, 5: 126, 13: 120, 11: 130, 15: 130, 6: 230, 17: 234, 10: 110, 19: 139, 3: 78, 1: 4}`). -/
def H1_3 : ℕ := 0xb00000000b40008b00118000ea000df00082000e4000780010e000820006e000a0000fb00163000e60007e003070004e008880000400000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_4
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 4 of stage 1 (`{2: 1861, 17: 328, 14: 263, 1: 156, 3: 442, 5: 508, 7: 497, 9: 224, 4: 1050, 13: 168, 11: 182, 15: 182, 6: 322, 8: 322, 10: 154, 19: 334, 12: 140, 16: 70}`). -/
def H1_4 : ℕ := 0x14e000000014800046000b600107000a80008c000b60009a000e000142001f100142001fc0041a001ba007450009c00000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_5
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 5 of stage 1 (`{2: 2084, 19: 434, 14: 266, 17: 301, 1: 512, 3: 584, 5: 642, 7: 426, 9: 192, 4: 900, 13: 144, 11: 156, 15: 156, 6: 276, 8: 276, 10: 132, 12: 120, 16: 60}`). -/
def H1_5 : ℕ := 0x1b2000000012d0003c0009c0010a00090000780009c00084000c000114001aa00114002820038400248008240020000000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_6
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 6 of stage 1 (`{2: 2465, 14: 203, 19: 393, 17: 244, 1: 1088, 3: 656, 5: 714, 7: 404, 9: 182, 4: 803, 13: 130, 11: 146, 15: 139, 6: 245, 8: 246, 10: 112, 12: 100, 16: 50}`). -/
def H1_6 : ℕ := 0x18900000000f4000320008b000cb00082000640009200070000b6000f600194000f5002ca0032300290009a10044000000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_7
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 7 of stage 1 (`{4: 693, 15: 15, 13: 14, 8: 624, 2: 2334, 17: 44, 6: 626, 7: 22, 11: 10, 12: 616, 19: 60, 9: 10, 10: 616, 16: 606, 14: 636, 18: 1260, 20: 99, 1: 144}`). -/
def H1_7 : ℕ := 0x630003c004ec0002c0025e0000f0027c0000e002680000a002680000a00270000160027200000002b5000000091e0009000000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_8
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 8 of stage 1 (`{2: 2420, 18: 1526, 20: 99, 4: 594, 6: 594, 8: 594, 10: 594, 12: 594, 14: 593, 16: 592, 1: 686}`). -/
def H1_8 : ℕ := 0x6300000005f600000002500000000251000000025200000002520000000252000000025200000002520000000974002ae00000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_9
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 9 of stage 1 (`{2: 2239, 14: 395, 16: 396, 18: 1262, 20: 457, 4: 394, 6: 394, 8: 394, 10: 394, 12: 394, 1: 1637, 19: 99}`). -/
def H1_9 : ℕ := 0x1c900063004ee000000018c000000018b000000018a000000018a000000018a000000018a000000018a00000008bf0066500000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_10
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 10 of stage 1 (`{1: 2456, 2: 1936, 20: 1743, 19: 341, 4: 6, 6: 6, 8: 6, 10: 6, 12: 6, 14: 6, 16: 6, 18: 369}`). -/
def H1_10 : ℕ := 0x6cf0015500171000000000600000000060000000006000000000600000000060000000006000000000600000007900099800000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_11
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 11 of stage 1 (`{2: 3657, 18: 2343, 20: 2398, 1: 468, 4: 66, 6: 66, 8: 66, 10: 66, 12: 66, 14: 66, 16: 66}`). -/
def H1_11 : ℕ := 0x95e000000092700000000420000000042000000004200000000420000000042000000004200000000420000000e49001d400000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_12
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 12 of stage 1 (`{23: 2047, 24: 1, 3: 9856, 4: 480, 18: 240, 22: 7832, 5: 1760, 6: 24, 10: 48}`). -/
def H1_12 : ℕ := 0x1007ff01e98000000000000000000f0000000000000000000000000000000000000003000000000000000000018006e0001e002680000000000000000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk1_13
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 13 of stage 1 (`{16: 945, 7: 1944, 5: 3080, 1: 20332, 4: 5886, 20: 618, 22: 3036, 18: 892, 14: 792, 12: 767, 10: 904, 8: 1161, 6: 3336, 19: 1560, 15: 576, 17: 1368, 9: 768, 11: 624, 13: 576, 2: 36, 23: 2024}`). -/
def H1_13 : ℕ := 0x7e800bdc000000026a006180037c00558003b1002400031800240002ff002700038800300004890079800d0800c08016fe000000002404f6c00000

end IntMul.Kappa.R6.Cx.NetData

end