κ-improvement development, part 30: item-language primitives

-- OpenAI-preprint / κ-improvement development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_K_Defs29

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.KFV24Proc
/-!
# KFV §28: the uniform rounds and Lemma 16 (forward and opposite) as fixed IL code

* `layC e14`: the run-time dispatcher of the layer of round `h` (on `gH`): prefix (`h < b`),
  chunk (`h < ℓ - 1`, the Proposition 14 call `e14`), top. **`layerU_layC`**.
* `rndF`, `rndO`: forward round (`layer ; J_E`) and opposite round (`J_{-E} ; layer`).
* `fwdC e14`, `oppC e14`: `gH` is pushed (`ℓ` resp. `0`), a unary loop of `ℓ` rounds on the frame
  stacks `qX, qB, qZ` updates it, and it is popped. **`fwdC_ok`**, **`oppC_ok`**: they compute
  `procQc` / `procQIc` of the paper's layout (Lemma 16 computed forward / opposite procedure).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT AModel Butterfly

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-! ## The code -/

/-- `h - b` (negative iff prefix round). -/
def eHB : Ex HS := .add (.reg gH) (.neg (.reg gBb))

/-- `h + 1 - ℓ` (negative iff not the top round). -/
def eHL : Ex HS := .add (.add (.reg gH) (.lit 1)) (.neg (.reg gLl))

/-- The layer of the current round. -/
def layC (e14 : Fin Pp) : IStmt HS Pp :=
  iteI eHB (fcode preC) (iteI eHL (chunkC e14) NLogN.KFV.topC)

/-- A forward round. -/
def rndF (e14 : Fin Pp) : IStmt HS Pp := .seq (layC e14) (twistU false)

/-- An opposite round. -/
def rndO (e14 : Fin Pp) : IStmt HS Pp := .seq (twistU true) (layC e14)

/-- `gH ← gH + d`. -/
def stepH (d : ℤ) : RS := .asg gH (.add (.reg gH) (.lit d))

/-- The forward procedure (rounds `ℓ-1, …, 0`). -/
def fwdC (e14 : Fin Pp) : IStmt HS Pp :=
  .seq (fcode (.push gH (.reg gLl)))
    (.seq (rptX gLl qX NLogN.KFV.qB qZ (.seq (fcode (stepH (-1))) (NLogN.KFV.rndF e14))) (fcode (.pop gH)))

/-- The opposite procedure (rounds `0, …, ℓ-1`). -/
def oppC (e14 : Fin Pp) : IStmt HS Pp :=
  .seq (fcode (.push gH (.lit 0)))
    (.seq (rptX gLl qX NLogN.KFV.qB qZ (.seq (rndO e14) (fcode (stepH 1)))) (fcode (.pop gH)))

/-! ## Contexts -/

/-- The context of the procedures: a round frame (any round register) and `p, W, Z`. -/
def PCtx (L : LP) (fl : List Bool) (p W Z : ℕ) (s : IState HS) : Prop :=
  ∃ s1 fG rG h0, s = encK s1 fG ∧ GRegs s1 fG L h0 ∧ fG gLG = fl.map fv ++ rG ∧
    (∀ j ∈ twFree, fG j = []) ∧ XR s p W Z

/-- The context of a round. -/
def RX (L : LP) (fl : List Bool) (h p W Z : ℕ) (s : IState HS) : Prop :=
  RCtx L fl h s ∧ XR s p W Z

/-- Cost of `stepH d`. -/
def cStepH (d : ℤ) (B : ℕ) : ℕ := ((Ex.add (.reg gH) (.lit d) : Ex HS).size + 1) * 2000 * (B + 2)

/-! ## The dispatcher -/

section Paper

open Synth GlueLayout GlueP14 GlueError

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- Cost of the layer of round `h` (the branch taken). -/
def cLayC (h W B cCh : ℕ) : ℕ :=
  cIteB 4 B + cIteB 6 B +
    (if h < bb ℓ K then cLeafR (ePre.size + (Ex.reg NLogN.KFV.gD : Ex HS).size + eSpre.size)
      (NLogN.KFV.preP D ℓ K long h) D (sufP D ℓ K long h) ℓ W B
    else if h < ℓ - 1 then cCh
    else cTopC D ℓ K long ((Ex.lit 0 : Ex HS).size + (Ex.reg gNL : Ex HS).size +
      (Ex.add (.reg gNn) (.neg (.reg gNL)) : Ex HS).size) W B)

/-- The chunk rounds are implemented by `chunkC e14`. -/
def ChunkU (I : List Sym) (iprog : Fin Pp → IStmt HS Pp) (e14 : Fin Pp) (hK : 0 < K) (hℓ : 1 ≤ ℓ)
    (p W Z cCh : ℕ) : Prop :=
  ∀ h, bb ℓ K ≤ h → h < ℓ - 1 →
    LayerU (r := 2 ^ ℓ) I iprog (RX (pLP D ℓ K long) (flOf D long) h p W Z) (chunkC e14)
      (layerQc p (paperSel D ℓ K long hK hℓ h)) (2 ^ NLogN.KFV.nB D ℓ K long) p W cCh

/-- The bound `U` of the twists. -/
def TwB (U : ℕ) : Prop :=
  D ≤ U ∧ (tgtL D ℓ K long).length ≤ U ∧ 3 * 2 ^ (ℓ + 1) ≤ U ∧
    2 ^ (tgtL D ℓ K long).length + 1 ≤ U ∧ D * ℓ ≤ U

/-- Cost of a forward round. -/
def cRndF (h W B cCh U : ℕ) : ℕ :=
  cLayC D ℓ K long h W B cCh + cTwistU (tgtL D ℓ K long).length ℓ D h
    (genG (pLP D ℓ K long) (flOf D long) false h).length W (zsz (U : ℤ))

/-- Cost of an opposite round. -/
def cRndO (h W B cCh U : ℕ) : ℕ :=
  cTwistU (tgtL D ℓ K long).length ℓ D h
    (genG (pLP D ℓ K long) (flOf D long) true h).length W (zsz (U : ℤ)) + cLayC D ℓ K long h W B cCh

/-- Cost of the forward procedure. -/
def cFwd (W B cCh U : ℕ) : ℕ :=
  ((Ex.reg gLl : Ex HS).size + 1) * 10 ^ 7 * (B + 2) ^ 2 +
    (((∑ k ∈ Finset.range ℓ, (cStepH (-1) B + cRndF D ℓ K long (ℓ - 1 - k) W B cCh U + 64)) +
      60 + cRpt ℓ + (dupCost (zsz (ℓ : ℤ)) + 17)) + (2 * B + 2))

/-- Cost of the opposite procedure. -/
def cOpp (W B cCh U : ℕ) : ℕ :=
  ((Ex.lit 0 : Ex HS).size + 1) * 10 ^ 7 * (B + 2) ^ 2 +
    (((∑ k ∈ Finset.range ℓ, (cRndO D ℓ K long k W B cCh U + cStepH 1 B + 64)) +
      60 + cRpt ℓ + (dupCost (zsz (ℓ : ℤ)) + 17)) + (2 * B + 2))

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV28LayStep
/-!
# KFV §31: one layout primitive on the record array

The records `xs` (shape `binSh n`, each `r` coefficients) are stored as `zs` (shape
`binSh n ++ [r]`) and on stack `0` as `gflat zs` (shape `binSh n ++ [r, 2]`).  A layout
primitive `o` acts on the records by `pull (binSh n) (permIdx o.inv)`.

* `recRep_pull`, `gb_pull`, `disk_pull`: the stored array of the pulled records is the pull of
  the stored array by `extA n g` (`g` on the first `n` digits, the rest fixed).
* `gflat_pull_ext`: `gflat` of it is again a pull by `extA n g`.
* `extA_mv`: for the single move `mv c (c+δ)` (and its inverse) `extA` is `KIL.swapMid`, the
  address map of KFC `bwdF`/`fwdF`.
* `pull_ext_xch`: for the exchange `xch i j K`, the pull of the stored array is the field swap
  `swapPos 1 3` on `[2^i, 2^K, 2^{j-i-K}, 2^K, 2^{n-j-K} r]`, the input of the Lemma 12 entry.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul KIL KFB KFH Synth AModel AModelL12

/-- `g` on the first `n` digits, the rest unchanged. -/
def extA (n : ℕ) (g : List ℕ → List ℕ) (a : List ℕ) : List ℕ := g (a.take n) ++ a.drop n

section Pull

variable {α : Type*}

end Pull

section Rec

variable {r F : ℕ}

end Rec

/-! ## Single moves are `swapMid` -/

/-! ## Exchanges are Lemma 12 swaps -/

end NLogN.KFV

end

section
-- Source module: Solutions.KFV29LayIL
/-!
# KFV §32: the layout primitives as fixed IL code

* `mvB eA eF eC`: the single move `mv c (c+δ)` on the stored records (`c, δ` and the exponent of
  the trailing block computed by `eA, eF, eC` at run time): KFUU's `mvBU` (KFC `bwdF`) with
  `qX, qB, qZ ← 2^c, 2^δ, 2^{e+ℓ+1}`. **`mvB_run`**.
* `mvF eA eG eC`: the inverse move, KFUU's `mvFU` (KFC `fwdF`). **`mvF_run`**.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-! ## Single moves -/

/-- The three block sizes. -/
def mvPush (eA eF eC : Ex HS) : RS :=
  .seq (.push qX (.pow2 eA)) (.seq (.push NLogN.KFV.qB (.pow2 eF)) (.push qZ (.pow2 eC)))

def mvPop : RS := .seq (.pop qZ) (.seq (.pop NLogN.KFV.qB) (.pop qX))

/-- The move `mv c (c+δ)` (`bwdF`). -/
def mvB (eA eF eC : Ex HS) : IStmt HS Pp :=
  .seq (fcode (mvPush eA eF eC)) (.seq KFUU.mvBU (fcode mvPop))

/-- The inverse move (`fwdF`). -/
def mvF (eA eG eC : Ex HS) : IStmt HS Pp :=
  .seq (fcode (mvPush eA eG eC)) (.seq KFUU.mvFU (fcode mvPop))

/-- Register overhead of a move. -/
def cMvR (eA eF eC : Ex HS) (B : ℕ) : ℕ :=
  ((eA.size + 2) + (eF.size + 2) + (eC.size + 2)) * 10 ^ 7 * (B + 2) ^ 2 + 3 * (2 * B + 2)

/-- Cost of a move. -/
def cMvB (eA eF eC : Ex HS) (c δ E W B : ℕ) : ℕ :=
  cMvR eA eF eC B + cBwdF (2 ^ c) 2 (2 ^ δ) (2 ^ E) W + KFUU.cK3 (2 ^ c) (2 ^ δ) (2 ^ E)

/-- Cost of an inverse move. -/
def cMvF (eA eF eC : Ex HS) (c δ E W B : ℕ) : ℕ :=
  cMvR eA eF eC B + cFwdF (2 ^ c) 2 (2 ^ δ) (2 ^ E) W + KFUU.cK3 (2 ^ c) (2 ^ δ) (2 ^ E)

/-- Expressions not reading the move registers. -/
def MvSafe (e : Ex HS) : Prop := e.Clean ∧ ∀ x ∈ e.regs, x ≠ qX ∧ x ≠ NLogN.KFV.qB ∧ x ≠ qZ ∧ x ≠ 0

/-- The frame after the three pushes. -/
def mvFr (v : List ℤ) (a b c : ℕ) : Fin HS → List ℤ :=
  Function.update (Function.update (Function.update (o0 v) qX [((2 ^ a : ℕ) : ℤ)])
    NLogN.KFV.qB [((2 ^ b : ℕ) : ℤ)]) qZ [((2 ^ c : ℕ) : ℤ)]

/-- The stored array after a move with address map `σ`. -/
def zMv (n r : ℕ) (σ : ℕ → ℕ) (zs : List GI) : List GI :=
  pull (binSh n ++ [r]) (binSh n ++ [r]) (extA n (permIdx σ)) 0 zs

end NLogN.KFV

end

section
-- Source module: Solutions.KFV31LayOps
/-!
# KFV §34: the layout moves in the closed forms the IL loops generate

* `genOps1`: `genOps` with a single (possibly trivial) move `mv c (c + |T| δ)` per triple
  (`|T| ≤ 1`); **`applyN_genOps1`**: same arrangement (`mv c c` is the identity);
  **`genOps1_eq`**: closed form by prefix sums.
* `ops1` (one move per axis, `rank`/`flag` closed forms), `ops2` (one move per `k < b D`),
  `ops3 = xchOps …` and **`applyN_lay3`**: `applyN (ops1 ++ ops2 ++ ops3) initL = tgtL`.
* `iterL_runArr`: a loop applying `runArr (g k)` in iteration `k` is `runArr` of the
  concatenation.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace NLogN.KFV

open Synth AModel AModelL12

/-! ## Single-move passes -/

def tL (x : List ℕ × List ℕ × List ℕ) : ℕ := x.2.1.length

def uvL (x : List ℕ × List ℕ × List ℕ) : ℕ := x.1.length + x.2.2.length

/-- One move per triple. -/
def genOps1 : ℕ → ℕ → List (List ℕ × List ℕ × List ℕ) → List LOp
  | _, _, [] => []
  | c, d, (U, T, V) :: xs =>
    LOp.mv c (c + T.length * (d + U.length)) :: genOps1 (c + T.length) (d + U.length + V.length) xs

/-! ## Ranges -/

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- The flag of axis `k` as a number. -/
def fbk (k : ℕ) : ℕ := if h : k < D then (if long ⟨k, h⟩ then 1 else 0) else 0

/-- The number of long axes before `k`. -/
def rkS (k : ℕ) : ℕ := ((List.range k).map (fbk D long)).sum

/-- Phase 1 in closed form. -/
def ops1 : List LOp :=
  (List.range D).map fun k => LOp.mv (rkS D long k) (rkS D long k + fbk D long k * (k * (ℓ - 1)))

/-- The `δ` of the move `k` of phase 2. -/
def dl2 (k : ℕ) : ℕ := k % D * (qq ℓ K * K + (bb ℓ K - 1 - k / D)) + qq ℓ K * K

/-- Phase 2 in closed form. -/
def ops2 : List LOp :=
  (List.range (bb ℓ K * D)).map fun k =>
    LOp.mv (nLong D long + k) (nLong D long + k + dl2 D ℓ K k)

/-- Phase 3. -/
def ops3 : List LOp := xchOps (srcT D (qq ℓ K)) (D * qq ℓ K) K (lstL D ℓ K long)

end Paper

/-! ## Loops of primitives -/

end NLogN.KFV

end

section
-- Source module: Solutions.KFV32LayLoop1
/-!
# KFV §35: phase 1 of the layout (the tops of the long axes) as a fixed IL loop

The long-axis flags are the bits of the mask register `gMk` (`mkOf`). Iteration `k < D` of a
unary loop moves the bit at position `rank + flag·k(ℓ-1)` to position `rank` (`mvB`), then
`rank += flag`, `k += 1` (registers `gRk`, `gI`).  **`ph1_ok`**: the loop computes
`runArr n 0 (ops1 …)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-! ## The mask -/

/-- Bits `b_0, b_1, …` as the number `Σ b_i 2^i`. -/
def mkOf : List Bool → ℕ
  | [] => 0
  | b :: bs => (if b then 1 else 0) + 2 * mkOf bs

/-! ## Registers -/

abbrev gMk : Fin HS := 53

/-- `r` holds `v` on top. -/
def RT (s : IState HS) (r : Fin HS) (v : ℤ) : Prop := ∃ L, s.G r = .int v :: L

/-- The layout registers on a base state. -/
structure LRg (s : IState HS) (L : LP) (mk W : ℕ) : Prop where
  d : RT s NLogN.KFV.gD L.D
  l : RT s gLl L.ℓ
  k : RT s gKk L.K
  b : RT s gBb L.b
  q : RT s gQq L.q
  nl : RT s gNL L.nL
  st : RT s gLst L.Lst
  n : RT s gNn L.n
  m : RT s gMk mk
  w : RT s gWw W

def lRegs : List (Fin HS) := [NLogN.KFV.gD, gLl, gKk, gBb, gQq, gNL, gLst, gNn, gMk, gWw]

/-- The loop frame stacks of the layout loops. -/
abbrev fA : Fin HS := tbQ
abbrev fC : Fin HS := tbN
abbrev fD : Fin HS := tbM

/-! ## The code of phase 1 -/

/-- The flag of axis `k = gI`. -/
def eFl : Ex HS := .nmod (.ndiv (.reg gMk) (.pow2 (.reg NLogN.KFV.gI))) (.lit 2)

def eA1 : Ex HS := .reg gRk

def eF1 : Ex HS := .mul eFl (.mul (.reg NLogN.KFV.gI) (.add (.reg gLl) (.lit (-1))))

/-- `n - c - δ + ℓ`. -/
def eCm (eA eF : Ex HS) : Ex HS := .add (.add (.reg gNn) (.neg eA)) (.add (.neg eF) (.reg gLl))

def up1 : RS := .seq (.asg gRk (.add (.reg gRk) eFl)) (.asg NLogN.KFV.gI (.add (.reg NLogN.KFV.gI) (.lit 1)))

def body1 : IStmt HS Pp := .seq (mvB eA1 eF1 (eCm eA1 eF1)) (fcode up1)

def ph1 : IStmt HS Pp :=
  .seq (fcode (.seq (.push NLogN.KFV.gI (.lit 0)) (.push gRk (.lit 0))))
    (.seq (KFT.rptX NLogN.KFV.gD fA NLogN.KFV.fC fD body1) (fcode (.seq (.pop gRk) (.pop NLogN.KFV.gI))))

/-! ## The loop body -/

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- The loop frame of phase 1 at iteration `k`. -/
def F1 (k : ℕ) : Fin HS → List ℤ :=
  Function.update (Function.update (fun _ => []) NLogN.KFV.gI [(k : ℤ)]) gRk [(rkS D long k : ℤ)]

/-- The move of iteration `k`. -/
def op1 (k : ℕ) : LOp :=
  LOp.mv (rkS D long k) (rkS D long k + fbk D long k * (k * (ℓ - 1)))

/-- The record array after phase 1's iteration `k`. -/
noncomputable def cBody1 (n W B : ℕ) (k : ℕ) : ℕ :=
  cMvB eA1 eF1 (eCm eA1 eF1) (rkS D long k) (fbk D long k * (k * (ℓ - 1)))
    (n - (rkS D long k + fbk D long k * (k * (ℓ - 1))) + ℓ) W B +
    ((((Ex.reg gRk).add eFl).size + 1) * 10 ^ 7 * (B + 2) ^ 2 +
      (((Ex.reg NLogN.KFV.gI).add (Ex.lit 1)).size + 1) * 10 ^ 7 * (B + 2) ^ 2)

/-- Cost of phase 1. -/
noncomputable def cPh1 (n W B : ℕ) : ℕ :=
  2 * (2 * 10 ^ 7 * (B + 2) ^ 2) +
    ((∑ k ∈ Finset.range D, (cBody1 D ℓ long n W B k + 64)) + 60 + cRpt D +
      (dupCost (zsz (D : ℤ)) + 17)) + 2 * (2 * B + 2)

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV46KronStage
/-!
# KFV §49: the Kronecker stage with its parameters (`kronS`)

`kronS pM = kPushS ; kronU pM ; kPopS`. From the registers `p` (`gPp`), `ℓ` (`gLl`) and `n`
(`gNn`) of the base, `kPushS` pushes the record-product parameters of `kronU` (`b = 2p + ℓ + 3`,
`r = 2^ℓ`, `ρ = ℓ`) on `50 … 55`, `N = 2^n` on `vRH`, `2 N r` on `vT` and `0` on `vZ`; `kPopS`
removes them. **`kronS_runs`**: on `N` records `zf` over `zg` (both disk records at scale
`2^p`), the stage leaves `kmulN r p ℓ N zf zg`, which stores `zipWith (ppq r p) xf xg`
(again disk records, `p + 1`-bit).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul KIL KFD KFT KFB KFC KFH RS

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-- The digit width of the Kronecker products. -/
def kb (p ℓ : ℕ) : ℕ := 2 * p + ℓ + 3

def eKb : Ex HS := .add (.add (.reg gPp) (.reg gPp)) (.add (.reg gLl) (.lit 3))

def eKG : Ex HS :=
  .ndiv (.mul (.pow2 (.reg gPp)) (.add (.pow2 (.mul eKb (.pow2 (.reg gLl)))) (.lit (-1))))
    (.add (.pow2 eKb) (.lit (-1)))

def eKJ : Ex HS := .pow2 (.mul eKb (.add (.pow2 (.reg gLl)) (.pow2 (.reg gLl))))

def eKT : Ex HS := .pow2 (.add (.add (.reg gNn) (.reg gLl)) (.lit 1))

/-- The parameter pushes. -/
def kPushS : RS :=
  .seq (.push kc (.pow2 (.reg gPp))) <|
  .seq (.push kr (.pow2 (.reg gLl))) <|
  .seq (.push kK eKG) <|
  .seq (.push kB (.pow2 eKb)) <|
  .seq (.push kJ eKJ) <|
  .seq (.push kD (.pow2 (.add (.reg gPp) (.reg gLl)))) <|
  .seq (.push vRH (.pow2 (.reg gNn))) <|
  .seq (.push NLogN.KFV.vT eKT) <|
  .push vZ (.lit 0)

/-- The parameter pops. -/
def kPopS : RS :=
  .seq (.pop vZ) <| .seq (.pop NLogN.KFV.vT) <| .seq (.pop vRH) <| .seq (.pop kD) <| .seq (.pop kJ) <|
  .seq (.pop kB) <| .seq (.pop kK) <| .seq (.pop kr) (.pop kc)

/-- The Kronecker stage. -/
def kronS (pM : Fin Pp) : IStmt HS Pp := .seq (fcode kPushS) (.seq (kronU pM) (fcode kPopS))

/-- The parameter frame. -/
def fK (p ℓ n : ℕ) (j : Fin HS) : List ℤ :=
  if j = kc then [(2 : ℤ) ^ p]
  else if j = kr then [((2 ^ ℓ : ℕ) : ℤ)]
  else if j = kK then [kG (NLogN.KFV.kb p ℓ) (2 ^ ℓ) ((2 : ℤ) ^ p)]
  else if j = kB then [(2 : ℤ) ^ NLogN.KFV.kb p ℓ]
  else if j = kJ then [((2 : ℤ) ^ NLogN.KFV.kb p ℓ) ^ (2 * 2 ^ ℓ)]
  else if j = kD then [(2 : ℤ) ^ (p + ℓ)]
  else if j = vRH then [((2 ^ n : ℕ) : ℤ)]
  else if j = NLogN.KFV.vT then [((2 * (2 ^ n * 2 ^ ℓ) : ℕ) : ℤ)]
  else if j = vZ then [0]
  else []

/-! ## Arithmetic -/

/-! ## Records -/

/-! ## The stage -/

/-- Cost of the Kronecker stage. -/
def cKronS (p ℓ n BK φ : ℕ) : ℕ :=
  100 * 10 ^ 7 * (BK + 2) ^ 2 + (cKron (2 ^ n) (2 ^ ℓ) p (NLogN.KFV.kb p ℓ) ℓ φ + 9 * (2 * BK + 2))

end NLogN.KFV

end

section
-- Source module: Solutions.KFV47Scale
/-!
# KFV §50: the scaling pass `× 2^n` (`scaleS`)

`scaleS` multiplies every integer of the `M = 2 N r` integers on top of stack `0` by `2^n`
(`n` on `gNn`, `N = 2^n`, `r = 2^ℓ`): it pushes `2^n` (on `vRH`) and `M` (on `vT`), runs a
counted loop of linear-cost shifts `push sT (shl (reg 0) (reg vRH)) ; pop 0`, moves the result
back and pops. **`scaleS_runs`**.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul KIL KFD KFT KFB KFC KFH RS

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-- The scratch stack of the scaling pass (and of the array shuttle). -/
abbrev sT : Fin HS := 37

/-- The shift of one item. -/
def eSh : Ex HS := .shl (.reg 0) (.reg vRH)

def shBody : RS := .seq (.push NLogN.KFV.sT eSh) (.pop 0)

/-- The scaling pass. -/
def scaleR : RS :=
  .seq (.push vRH (.pow2 (.reg gNn))) <|
  .seq (.push NLogN.KFV.vT eKT) <|
  .seq (.rep NLogN.KFV.vL (.reg NLogN.KFV.vT) shBody) <|
  .seq (NLogN.mvK NLogN.KFV.sT 0 NLogN.KFV.vL (.reg NLogN.KFV.vT)) <|
  .seq (.pop NLogN.KFV.vT) (.pop vRH)

def scaleS : IStmt HS Pp := fcode scaleR

/-- The scaled Gaussian integer. -/
def scG (n : ℕ) (z : GI) : GI := (z.1 * 2 ^ n, z.2 * 2 ^ n)

/-- Cost of the scaling pass. -/
def cScale (M B : ℕ) : ℕ :=
  20 * 10 ^ 7 * (B + 2) ^ 2 + (cLp M (8000 * (B + 2) + (2 * B + 2)) B + cLp M (250 * (B + 2)) B +
    2 * (2 * B + 2))

end NLogN.KFV

end

section
-- Source module: Solutions.KFV48Shut
/-!
# KFV §51: moving an array between stack `0` and `sT` (`shR`)

`shR X Y = push vT (2 N r) ; mvK X Y vL vT ; pop vT` moves the `2 N r` integers on top of `X`
(reversed) onto `Y`. **`shut_runs`**.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul KIL KFD KFT KFB KFC KFH RS

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-- The array move. -/
def shR (X Y : Fin HS) : RS := .seq (.push NLogN.KFV.vT eKT) (.seq (NLogN.mvK X Y NLogN.KFV.vL (.reg NLogN.KFV.vT)) (.pop NLogN.KFV.vT))

/-- Its cost. -/
def cShut (M B : ℕ) : ℕ := 10 * 10 ^ 7 * (B + 2) ^ 2 + (cLp M (250 * (B + 2)) B + (2 * B + 2))

end NLogN.KFV

end

section
-- Source module: Solutions.KFV49Core
/-!
# KFV §52: the core of the Proposition 18 program (two arrays)

On a base `encK s fB` (registers in `fB`, `sT` free), with the data `zf` over `zg` on stack `0`:

`core = F ; shR 0 sT ; F ; shR sT 0 ; kronS ; O ; scaleS`

runs the forward layer program `F` on `f` (the top array), parks it on `sT`, runs `F` on `g`,
brings `f` back on top, multiplies pointwise (`kronS`), runs the opposite layer program `O` and
scales by `2^n`. **`core_runs`**: the result stores `(O (zipWith ppq (F xf) (F xg))).map (2^n • ·)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul KIL KFD KFT KFB KFC KFH RS

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-- The core of the Proposition 18 program. -/
def core18 (cF cO : IStmt HS Pp) (pM : Fin Pp) : IStmt HS Pp :=
  .seq cF (.seq (fcode (shR 0 NLogN.KFV.sT)) (.seq cF (.seq (fcode (shR NLogN.KFV.sT 0)) (.seq (kronS pM)
    (.seq cO scaleS)))))

end NLogN.KFV

end

section
-- Source module: Solutions.KFV33LayLoop2
/-!
# KFV §36: phase 2 of the layout (the low bits) as a fixed IL loop

Iteration `k < b D` (`u = k / D`, `i = k mod D`) moves the bit at
`nL + k + i (qK + b - 1 - u) + qK` to `nL + k` (`mvB`). The count `b D` is pushed on `gT`, the
iteration index is `gI`. **`ph2_ok`**: the loop computes `runArr n 0 (ops2 …)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-! ## The code -/

def eA2 : Ex HS := .add (.reg gNL) (.reg NLogN.KFV.gI)

def eU2 : Ex HS := .ndiv (.reg NLogN.KFV.gI) (.reg NLogN.KFV.gD)

def eQK : Ex HS := .mul (.reg gQq) (.reg gKk)

def eF2 : Ex HS :=
  .add (.mul (.nmod (.reg NLogN.KFV.gI) (.reg NLogN.KFV.gD)) (.add eQK (.add (.reg gBb) (.add (.lit (-1)) (.neg eU2)))))
    eQK

def stepI : RS := .asg NLogN.KFV.gI (.add (.reg NLogN.KFV.gI) (.lit 1))

def body2 : IStmt HS Pp := .seq (mvB eA2 eF2 (eCm eA2 eF2)) (fcode stepI)

def ph2 : IStmt HS Pp :=
  .seq (fcode (.seq (.push NLogN.KFV.gT (.mul (.reg gBb) (.reg NLogN.KFV.gD))) (.push NLogN.KFV.gI (.lit 0))))
    (.seq (KFT.rptX NLogN.KFV.gT fA NLogN.KFV.fC fD body2) (fcode (.seq (.pop NLogN.KFV.gI) (.pop NLogN.KFV.gT))))

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- The loop frame of phase 2. -/
def F2 (N k : ℕ) : Fin HS → List ℤ :=
  Function.update (Function.update (fun _ => []) NLogN.KFV.gT [(N : ℤ)]) NLogN.KFV.gI [(k : ℤ)]

def op2 (k : ℕ) : LOp := LOp.mv (nLong D long + k) (nLong D long + k + dl2 D ℓ K k)

noncomputable def cBody2 (n W B : ℕ) (k : ℕ) : ℕ :=
  cMvB eA2 eF2 (eCm eA2 eF2) (nLong D long + k) (dl2 D ℓ K k)
    (n - (nLong D long + k + dl2 D ℓ K k) + ℓ) W B +
    (((Ex.reg NLogN.KFV.gI).add (Ex.lit 1)).size + 1) * 10 ^ 7 * (B + 2) ^ 2

/-- Cost of phase 2. -/
noncomputable def cPh2 (n W B : ℕ) : ℕ :=
  (4 * 10 ^ 7 * (B + 2) ^ 2 + 2 * 10 ^ 7 * (B + 2) ^ 2) +
    ((∑ k ∈ Finset.range (bb ℓ K * D), (cBody2 D ℓ K long n W B k + 64)) + 60 + cRpt (bb ℓ K * D) +
      (dupCost (zsz ((bb ℓ K * D : ℕ) : ℤ)) + 17)) + 2 * (2 * B + 2)

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV30LayX
/-!
# KFV §33: the chunk exchange as fixed IL code

* `SwOK I iprog eSw dW Kc`: the uniform Lemma 12 entry (`KFM.SwapNeed` in a given table).
* `pushL i es`, `popN i m`: push a list of expressions onto `i` / pop `m` entries.
* `xchC eSw dW eE eK eM eI eW`: push the descriptor
  `descSw W K 1 3 [2^i, 2^K, 2^m, 2^K, 2^E]`, call the entry, pop it.
  **`xchC_run`**: the exchange `xch i j K` (`m = j - i - K`, `E = n - j - K + ℓ`) on the stored
  records.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-- The uniform Lemma 12 entry `eSw` (descriptor on `dW`). -/
def SwOK (I : List Sym) (iprog : Fin Pp → IStmt HS Pp) (eSw : Fin Pp) (dW : Fin HS) (Kc : ℝ) :
    Prop :=
  ∀ (u w : ℕ) (sh : Shape) (p q : ℕ), 1 ≤ u → (∀ a ∈ sh, 1 ≤ a) →
    p < q → q < sh.length → sh.getD p 0 = 2 ^ u → sh.getD q 0 = 2 ^ u →
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dW → f j = []) →
    f dW = KFM.descSw w u p q sh →
    f 0 = gflat zs ++ l → zs.length = vol sh → NLogN.KFB.GB w zs →
    ∃ c : ℕ, IRuns I iprog (.call eSw) (encK s f)
        (encK s (Function.update f 0 (gflat (pull sh sh (swapPos p q) 0 zs) ++ l))) c ∧
      (c : ℝ) ≤ Kc * (((w : ℝ) + 1) * ((vol sh : ℝ) + 1) * (u : ℝ) ^ KFS.τS +
        (((sh.length + 1) * (Nat.size (vol sh) + w + u + 1) ^ 2 : ℕ) : ℝ))

/-! ## Pushing and popping lists -/

def pushL (i : Fin HS) : List (Ex HS) → RS
  | [] => .skip
  | e :: es => .seq (.push i e) (pushL i es)

def popN (i : Fin HS) : ℕ → RS
  | 0 => .skip
  | m + 1 => .seq (.pop i) (popN i m)

/-- Cost of a list of pushes. -/
def cPushL (B : ℕ) (es : List (Ex HS)) : ℕ := (es.map fun e => (e.size + 1) * 10 ^ 7 * (B + 2) ^ 2).sum + 1

/-! ## The exchange -/

/-- The descriptor pushes (`2^E` first, `W` last on top). -/
def xchEs (eE eK eM eI eW : Ex HS) : List (Ex HS) :=
  [.pow2 eE, .pow2 eK, .pow2 eM, .pow2 eK, .pow2 eI, .lit 5, .lit 3, .lit 1, eK, eW]

/-- **The chunk exchange.** -/
def xchC (eSw : Fin Pp) (dW : Fin HS) (eE eK eM eI eW : Ex HS) : IStmt HS Pp :=
  .seq (fcode (NLogN.KFV.pushL dW (xchEs eE eK eM eI eW))) (.seq (.call eSw) (fcode (popN dW 10)))

/-- The 5-field shape of the exchange. -/
def sh5 (i K m E : ℕ) : Shape := [2 ^ i, 2 ^ K, 2 ^ m, 2 ^ K, 2 ^ E]

/-- Cost of an exchange. -/
noncomputable def cXch (Kc : ℝ) (eE eK eM eI eW : Ex HS) (n ℓ K W B : ℕ) : ℕ :=
  cPushL B (xchEs eE eK eM eI eW) +
    ⌈Kc * (((W : ℝ) + 1) * ((2 ^ (n + ℓ) : ℕ) + 1) * (K : ℝ) ^ KFS.τS +
      (((5 + 1) * (Nat.size (2 ^ (n + ℓ)) + W + K + 1) ^ 2 : ℕ) : ℝ))⌉₊ + (10 * (2 * B + 2) + 1)

/-- Expressions not reading `dW`. -/
def DSafe (dW : Fin HS) (e : Ex HS) : Prop := e.Clean ∧ ∀ r ∈ e.regs, r ≠ dW

end NLogN.KFV

end

section
-- Source module: Solutions.KFV34LayLoop3
/-!
# KFV §37: phase 3 of the layout (the chunk exchanges) as a fixed IL loop

Iteration `t < N = D q`: the chase `x ← src t; N times (x ← src x while x < t)` runs in the
register `gV` (an `RS` counter loop on `gT2`), then, unless `x = t`, the chunks `t` and `x`
(after the prefix `Lst`) are exchanged by the Lemma 12 entry (`xchC`).
**`ph3_ok`**: the loop computes `runArr n 0 (ops3 …)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-! ## Selections -/

/-! ## The code -/

/-- `src y = (y mod D) q + y / D`. -/
def srcE (y : Ex HS) : Ex HS := .add (.mul (.nmod y (.reg NLogN.KFV.gD)) (.reg gQq)) (.ndiv y (.reg NLogN.KFV.gD))

/-- One chase step. -/
def chStep : RS := .asg NLogN.KFV.gV (.sel (.add (.reg NLogN.KFV.gV) (.neg (.reg NLogN.KFV.gI))) (NLogN.KFV.srcE (.reg NLogN.KFV.gV)) (.reg NLogN.KFV.gV))

/-- The chase. -/
def chase : RS := .seq (.push NLogN.KFV.gV (NLogN.KFV.srcE (.reg NLogN.KFV.gI))) (.rep gT2 (.reg NLogN.KFV.gT) chStep)

/-- `x - t - 1`. -/
def eCnd : Ex HS := .add (.add (.reg NLogN.KFV.gV) (.neg (.reg NLogN.KFV.gI))) (.lit (-1))

/-- `i = |Lst| + t K`. -/
def eI3 : Ex HS := .add (.reg gLst) (.mul (.reg NLogN.KFV.gI) (.reg gKk))

/-- `j - i - K = (x - t - 1) K`. -/
def eM3 : Ex HS := .mul eCnd (.reg gKk)

/-- `n - j - K + ℓ`, `j = |Lst| + x K`. -/
def eE3 : Ex HS :=
  .add (.add (.reg gNn) (.neg (.add (.reg gLst) (.mul (.add (.reg NLogN.KFV.gV) (.lit 1)) (.reg gKk)))))
    (.reg gLl)

def post3 : RS := .seq (.pop NLogN.KFV.gV) stepI

def body3 (eSw : Fin Pp) (dW : Fin HS) : IStmt HS Pp :=
  .seq (fcode chase)
    (.seq (iteI eCnd .skip (xchC eSw dW eE3 (.reg gKk) eM3 eI3 (.reg gWw))) (fcode post3))

def ph3 (eSw : Fin Pp) (dW : Fin HS) : IStmt HS Pp :=
  .seq (fcode (.seq (.push NLogN.KFV.gT (.mul (.reg NLogN.KFV.gD) (.reg gQq))) (.push NLogN.KFV.gI (.lit 0))))
    (.seq (KFT.rptX NLogN.KFV.gT fA NLogN.KFV.fC fD (body3 eSw dW)) (fcode (.seq (.pop NLogN.KFV.gI) (.pop NLogN.KFV.gT))))

/-! ## The chase -/

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- The source of a chunk position. -/
abbrev srcP : ℕ → ℕ := srcT D (qq ℓ K)

/-- The chase value after `j` steps. -/
def xC (t j : ℕ) : ℕ := chF (NLogN.KFV.srcP D ℓ K) t j (NLogN.KFV.srcP D ℓ K t)

/-- The cost of one chase step. -/
def cStep (B : ℕ) : ℕ :=
  (((Ex.sel (.add (.reg NLogN.KFV.gV) (.neg (.reg NLogN.KFV.gI))) (NLogN.KFV.srcE (.reg NLogN.KFV.gV)) (.reg NLogN.KFV.gV)) : Ex HS).size + 1) *
    10 ^ 7 * (B + 2) ^ 2

/-- The cost of the chase. -/
def cChase (N B : ℕ) : ℕ :=
  ((NLogN.KFV.srcE (.reg NLogN.KFV.gI)).size + 1) * 10 ^ 7 * (B + 2) ^ 2 +
    (((Ex.reg NLogN.KFV.gT : Ex HS).size + 1) * 2000 * (B + 2) + N * (cStep B + 8000 * (B + 2) + 30) + 32)

/-- The exchanges of step `t`. -/
def opX (t : ℕ) : List LOp := opT (NLogN.KFV.srcP D ℓ K) (D * qq ℓ K) K (lstL D ℓ K long) t

/-- Cost of one phase-3 step. -/
noncomputable def cBody3 (Kc : ℝ) (n W B t : ℕ) : ℕ :=
  100 * cChase (D * qq ℓ K) B + cIteB eCnd.size B +
    (if xT (NLogN.KFV.srcP D ℓ K) (D * qq ℓ K) t = t then 1 else
      cXch Kc eE3 (.reg gKk) eM3 eI3 (.reg gWw) n ℓ K W B) +
    ((2 * B + 2) + (((Ex.reg NLogN.KFV.gI).add (Ex.lit 1)).size + 1) * 10 ^ 7 * (B + 2) ^ 2)

/-- The registers phase 3 reads. -/
def r3 : List (Fin HS) := [NLogN.KFV.gV, NLogN.KFV.gI, gLst, gKk, gNn, gLl, gWw]

/-- Cost of phase 3. -/
noncomputable def cPh3 (Kc : ℝ) (n W B : ℕ) : ℕ :=
  (4 * 10 ^ 7 * (B + 2) ^ 2 + 2 * 10 ^ 7 * (B + 2) ^ 2) +
    ((∑ t ∈ Finset.range (D * qq ℓ K), (cBody3 D ℓ K Kc n W B t + 64)) + 60 + cRpt (D * qq ℓ K) +
      (dupCost (zsz ((D * qq ℓ K : ℕ) : ℤ)) + 17)) + 2 * (2 * B + 2)

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV35LayIn
/-!
# KFV §38: the layout-in program (three phases) as one `LayerU`

`layIn = ph1 ; ph2 ; ph3`. The three primitive lists are well formed (`ops1_wf`, `ops2_wf`,
`ops3_wf`), so the composed run is the `pull` by `relabel initL tgtL` (`runArr_eq_pull_init`,
`applyN_lay3`). **`layIn_ok`**.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-- The layout-in program. -/
def layIn (eSw : Fin Pp) (dW : Fin HS) : IStmt HS Pp := .seq ph1 (.seq ph2 (ph3 eSw dW))

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- Cost of the layout-in program. -/
noncomputable def cLayIn (Kc : ℝ) (n W B : ℕ) : ℕ :=
  cPh1 D ℓ long n W B + (cPh2 D ℓ K long n W B + cPh3 D ℓ K Kc n W B)

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV36LayRev
/-!
# KFV §39: running a layout schedule backwards

`runArrR n d ops` applies the primitives of `ops` in reverse order, each by its forward position
map (`pull` by `permIdx o.idx`): it undoes `runArr` (**`runArrR_runArr`**), hence it is the `pull`
by the reverse relabelling (**`runArrR_eq_pull`**). **`runArrR_flatMap_range`**: a schedule given
as a `flatMap` over `range N` runs backwards as an `iterL` loop over the reversed index.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open Synth AModel AModelL12

/-- The schedule run backwards. -/
def runArrR {α : Type*} (n : ℕ) (d : α) (ops : List LOp) (xs : List α) : List α :=
  ops.reverse.foldl (fun acc o => pull (binSh n) (binSh n) (permIdx o.idx) d acc) xs

end NLogN.KFV

end

section
-- Source module: Solutions.KFV38LayOut1
/-!
# KFV §41: phase 1 of the layout, backwards, as a fixed IL loop

Iteration `j < D` (`k = D-1-j`): the registers `gI = k+1`, `gRk = rank(k+1)` are
first decremented (`gI ← gI - 1`, `gRk ← gRk - flag`), then the inverse move `mvF` puts the bit at
position `rank` back to `rank + flag·k(ℓ-1)`. **`ph1R_ok`**: the loop computes
`runArrR n 0 (ops1 …)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-! ## The code -/

def dn1 : RS := .seq (.asg NLogN.KFV.gI (.add (.reg NLogN.KFV.gI) (.lit (-1)))) (.asg gRk (.add (.reg gRk) (.neg eFl)))

def body1R : IStmt HS Pp := .seq (fcode dn1) (NLogN.KFV.mvF eA1 eF1 (eCm eA1 eF1))

def ph1R : IStmt HS Pp :=
  .seq (fcode (.seq (.push NLogN.KFV.gI (.reg NLogN.KFV.gD)) (.push gRk (.reg gNL))))
    (.seq (KFT.rptX NLogN.KFV.gD fA NLogN.KFV.fC fD body1R) (fcode (.seq (.pop gRk) (.pop NLogN.KFV.gI))))

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- Cost of the backward iteration `j`. -/
noncomputable def cBody1R (n W B : ℕ) (j : ℕ) : ℕ :=
  ((((Ex.reg NLogN.KFV.gI).add (Ex.lit (-1))).size + 1) * 10 ^ 7 * (B + 2) ^ 2 +
    (((Ex.reg gRk).add (Ex.neg eFl)).size + 1) * 10 ^ 7 * (B + 2) ^ 2) +
  cMvF eA1 eF1 (eCm eA1 eF1) (rkS D long (D - 1 - j))
    (fbk D long (D - 1 - j) * ((D - 1 - j) * (ℓ - 1)))
    (n - (rkS D long (D - 1 - j) + fbk D long (D - 1 - j) * ((D - 1 - j) * (ℓ - 1))) + ℓ) W B

/-- Cost of phase 1 backwards. -/
noncomputable def cPh1R (n W B : ℕ) : ℕ :=
  2 * (2 * 10 ^ 7 * (B + 2) ^ 2) +
    ((∑ j ∈ Finset.range D, (cBody1R D ℓ long n W B j + 64)) + 60 + cRpt D +
      (dupCost (zsz (D : ℤ)) + 17)) + 2 * (2 * B + 2)

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV39LayOut2
/-!
# KFV §42: phase 2 of the layout, backwards, as a fixed IL loop

Iteration `j < b D` (`k = bD-1-j`): `gI ← gI - 1` (from `k+1` to `k`), then the inverse move `mvF`
puts the bit at `nL + k` back to `nL + k + δ₂(k)`. **`ph2R_ok`**: the loop computes
`runArrR n 0 (ops2 …)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

def stepD : RS := .asg NLogN.KFV.gI (.add (.reg NLogN.KFV.gI) (.lit (-1)))

def body2R : IStmt HS Pp := .seq (fcode stepD) (NLogN.KFV.mvF eA2 eF2 (eCm eA2 eF2))

def ph2R : IStmt HS Pp :=
  .seq (fcode (.seq (.push NLogN.KFV.gT (.mul (.reg gBb) (.reg NLogN.KFV.gD))) (.push NLogN.KFV.gI (.mul (.reg gBb) (.reg NLogN.KFV.gD)))))
    (.seq (KFT.rptX NLogN.KFV.gT fA NLogN.KFV.fC fD body2R) (fcode (.seq (.pop NLogN.KFV.gI) (.pop NLogN.KFV.gT))))

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

noncomputable def cBody2R (n W B : ℕ) (j : ℕ) : ℕ :=
  (((Ex.reg NLogN.KFV.gI).add (Ex.lit (-1))).size + 1) * 10 ^ 7 * (B + 2) ^ 2 +
  cMvF eA2 eF2 (eCm eA2 eF2) (nLong D long + (bb ℓ K * D - 1 - j)) (dl2 D ℓ K (bb ℓ K * D - 1 - j))
    (n - (nLong D long + (bb ℓ K * D - 1 - j) + dl2 D ℓ K (bb ℓ K * D - 1 - j)) + ℓ) W B

/-- Cost of phase 2 backwards. -/
noncomputable def cPh2R (n W B : ℕ) : ℕ :=
  (4 * 10 ^ 7 * (B + 2) ^ 2 + 4 * 10 ^ 7 * (B + 2) ^ 2) +
    ((∑ j ∈ Finset.range (bb ℓ K * D), (cBody2R D ℓ K long n W B j + 64)) + 60 +
      cRpt (bb ℓ K * D) + (dupCost (zsz ((bb ℓ K * D : ℕ) : ℤ)) + 17)) + 2 * (2 * B + 2)

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV40LayOut3
/-!
# KFV §43: phase 3 of the layout, backwards, as a fixed IL loop

Iteration `j < N = D q` (`t = N-1-j`): `gI ← gI - 1` (from `t+1` to `t`), the chase computes
`x = xT t`, and unless `x = t` the chunks `t` and `x` are exchanged again (an exchange is its own
inverse). **`ph3R_ok`**: the loop computes `runArrR n 0 (ops3 …)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

def body3R (eSw : Fin Pp) (dW : Fin HS) : IStmt HS Pp :=
  .seq (fcode stepD) (.seq (fcode chase)
    (.seq (iteI eCnd .skip (xchC eSw dW eE3 (.reg gKk) eM3 eI3 (.reg gWw))) (fcode (.pop NLogN.KFV.gV))))

def ph3R (eSw : Fin Pp) (dW : Fin HS) : IStmt HS Pp :=
  .seq (fcode (.seq (.push NLogN.KFV.gT (.mul (.reg NLogN.KFV.gD) (.reg gQq))) (.push NLogN.KFV.gI (.mul (.reg NLogN.KFV.gD) (.reg gQq)))))
    (.seq (KFT.rptX NLogN.KFV.gT fA NLogN.KFV.fC fD (body3R eSw dW)) (fcode (.seq (.pop NLogN.KFV.gI) (.pop NLogN.KFV.gT))))

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- Cost of one backward phase-3 step. -/
noncomputable def cBody3R (Kc : ℝ) (n W B j : ℕ) : ℕ :=
  (((Ex.reg NLogN.KFV.gI).add (Ex.lit (-1))).size + 1) * 10 ^ 7 * (B + 2) ^ 2 +
  (100 * cChase (D * qq ℓ K) B + cIteB eCnd.size B +
    (if xT (NLogN.KFV.srcP D ℓ K) (D * qq ℓ K) (D * qq ℓ K - 1 - j) = D * qq ℓ K - 1 - j then 1 else
      cXch Kc eE3 (.reg gKk) eM3 eI3 (.reg gWw) n ℓ K W B) +
    (2 * B + 2))

/-- Cost of phase 3 backwards. -/
noncomputable def cPh3R (Kc : ℝ) (n W B : ℕ) : ℕ :=
  (4 * 10 ^ 7 * (B + 2) ^ 2 + 4 * 10 ^ 7 * (B + 2) ^ 2) +
    ((∑ t ∈ Finset.range (D * qq ℓ K), (cBody3R D ℓ K Kc n W B t + 64)) + 60 + cRpt (D * qq ℓ K) +
      (dupCost (zsz ((D * qq ℓ K : ℕ) : ℤ)) + 17)) + 2 * (2 * B + 2)

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV41LayOut
/-!
# KFV §44: the layout-out program as one `LayerU`

`layOut = ph3R ; ph2R ; ph1R` runs the layout schedule backwards; it computes the `pull` by
`relabel tgtL initL` (`runArrR_eq_pull`). **`layOut_ok`**.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-- The layout-out program. -/
def layOut (eSw : Fin Pp) (dW : Fin HS) : IStmt HS Pp := .seq (ph3R eSw dW) (.seq ph2R ph1R)

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- Cost of the layout-out program. -/
noncomputable def cLayOut (Kc : ℝ) (n W B : ℕ) : ℕ :=
  cPh3R D ℓ K Kc n W B + (cPh2R D ℓ K long n W B + cPh1R D ℓ long n W B)

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV42LayCost
/-!
# KFV §45: the cost of the uniform layout programs

With `V = 2^{n+ℓ}` (the number of stored integers per record bit) and the overhead hypothesis
`10^12 (B+2)^3 + 16 cU B ≤ V`, every single move costs `≤ 10^5 (W+1) V` and every chunk step
`≤ (2 Kc + 5)(W+1)(V+1) K^τ`. Hence (**`cLayIn_le`**, **`cLayOut_le`**)
`cost ≤ (4·10^5 + 2 Kc + 5) (W+1) (V+1) ((D+1) K + p K^{τ-1})` whenever `D q K ≤ p`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

/-! ## Expression sizes -/

/-! ## One move -/

/-- The overhead hypothesis. -/
def OvOK (n ℓ B : ℕ) : Prop := 10 ^ 12 * (B + 2) ^ 3 + 16 * KFUU.cU B ≤ 2 ^ (n + ℓ)

/-! ## The phases -/

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-! ## Phase totals for the single moves -/

end Paper

/-! ## Phase 3 -/

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

end Paper

/-! ## One exchange -/

/-! ## The totals -/

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV43ErrNeed
/-!
# KFV §46: the error interface of Proposition 18 (`Err18Need`)

The uniform Proposition 18 program computes, on coefficient vectors (exactly, by `layIn_ok`,
`fwdC_ok`, the Kronecker pointwise step `ppq`, `oppC_ok`, the scaling by `M = 2^{Σ a_i}` and
`layOut_ok`), the list **`pipe18c`**:

  `Lout (M • procQIc (zipWith ppq (procQc (Lin xf)) (procQc (Lin xg))))`

with `Lin` / `Lout` the `pull`s by `relabel initL tgtL` / `relabel tgtL initL` (row-major ↔ the
paper's layout `paperLayout`). **`Err18Need`** is the pure error statement: this list is within
`2 N (3ℓ + 1) 2^{-p}` of `mrL` (the bound `P18IL` asks for), and `mrL` has coefficients of
modulus `≤ 1`. It follows from
`GlueProp18.prop18_error_paper` (with `√2 ≤ 2`, `Mv = N`) through `rrModel (2^ℓ - 1)`,
`co_procQ`, `co_procQI`, `co_ppq` and the row-major / layout correspondence.
-/

namespace NLogN.KFV

open Synth AModel GlueLayout

noncomputable section

/-- The axis lengths `t_i = 2^{a_i}` of the paper's parameters. -/
def ts18 (D ℓ : ℕ) (long : Fin D → Bool) : List ℕ := List.ofFn fun i : Fin D => 2 ^ al D ℓ long i

/-- The coefficient-level Proposition 18 pipeline computed by the uniform program. -/
def pipe18c (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool) (hK : 0 < K) (hℓ : 1 ≤ ℓ) (p : ℕ)
    (xf xg : List (Fin (2 ^ ℓ) → ℂ)) : List (Fin (2 ^ ℓ) → ℂ) :=
  let n := (tgtL D ℓ K long).length
  let Lin : List (Fin (2 ^ ℓ) → ℂ) → List (Fin (2 ^ ℓ) → ℂ) :=
    pull (binSh n) (binSh n) (relabel (initL D ℓ long) (tgtL D ℓ K long)) 0
  let Lout : List (Fin (2 ^ ℓ) → ℂ) → List (Fin (2 ^ ℓ) → ℂ) :=
    pull (binSh n) (binSh n) (relabel (tgtL D ℓ K long) (initL D ℓ long)) 0
  let F := procQc (r := 2 ^ ℓ) p (paperLayout D ℓ K long hK hℓ) ℓ (partAxes (al D ℓ long))
    (paperSel D ℓ K long hK hℓ) ℓ
  let G := procQIc (r := 2 ^ ℓ) p (paperLayout D ℓ K long hK hℓ) ℓ (partAxes (al D ℓ long))
    (paperSel D ℓ K long hK hℓ) ℓ
  Lout ((G (List.zipWith (ppq (2 ^ ℓ) p) (F (Lin xf)) (F (Lin xg)))).map
    fun v => (Mv (al D ℓ long) : ℂ) • v)

/-- **The error interface of Proposition 18** (pure mathematics; no IL). -/
def Err18Need : Prop :=
  ∀ (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool) (hK : 0 < K) (hℓ1 : 1 ≤ ℓ), 2 ≤ ℓ →
    1 ≤ qq ℓ K → ∀ (p : ℕ) (xf xg : List (Fin (2 ^ ℓ) → ℂ)),
    xf.length = (ts18 D ℓ long).prod → xg.length = (ts18 D ℓ long).prod →
    (∀ x ∈ xf, ‖x‖ ≤ 1) → (∀ x ∈ xg, ‖x‖ ≤ 1) →
    (pipe18c D ℓ K long hK hℓ1 p xf xg).length = (ts18 D ℓ long).prod ∧
    (∀ j < (ts18 D ℓ long).prod, ∀ k : Fin (2 ^ ℓ),
      ‖(KFM.mrL (2 ^ ℓ) (ts18 D ℓ long) xf xg).getD j 0 k‖ ≤ 1) ∧
    ∀ j < (ts18 D ℓ long).prod, ∀ k : Fin (2 ^ ℓ),
      ‖(pipe18c D ℓ K long hK hℓ1 p xf xg).getD j 0 k -
          (KFM.mrL (2 ^ ℓ) (ts18 D ℓ long) xf xg).getD j 0 k‖ ≤
        2 * (ts18 D ℓ long).prod * (3 * ℓ + 1) * (2 : ℝ)⁻¹ ^ p

end

end NLogN.KFV

end

section
-- Source module: Solutions.KFV44SetupNeed
/-!
# KFV §47: the setup interface of Proposition 18 (`Setup18Need`)

The uniform Proposition 18 program starts from the descriptor `desc18 p ℓ K ts` on stack
`dS18 = 33` and data on stack `0`, all other managed stacks empty. **`Setup18Need`** asks for two
fixed codes (no calls, any table):

* `setup` reads the descriptor and builds the register frame **`regs18 p ℓ K ts`** under the data:
  `encK s f ⟶ encK (encK s (regs18 …)) (o0 (f 0))`;
* `teardown` removes it again: `encK (encK s (regs18 …)) (o0 v) ⟶ encK s (update f 0 v)`;

each with cost `≤ Cs (|ts| + ℓ + K + zsz p + 2)^4`.

The frame (`D = |ts|`, flag `i` = "axis `i` is long" = `t_i = 2^ℓ`, `b = (ℓ-1) mod K`,
`q = (ℓ-1)/K`, `nL` = number of long axes, `Lst = nL + b D`, `n = Lst + D q K`):

| stack | `gD` 40 | `gLl` 41 | `gKk` 42 | `gBb` 43 | `gQq` 44 | `gNL` 45 | `gLst` 46 | `gNn` 47 |
|---|---|---|---|---|---|---|---|---|
| value | `[D]` | `[ℓ]` | `[K]` | `[b]` | `[q]` | `[nL]` | `[Lst]` | `[n]` |

| stack | `gH` 48 | `gLG` 49 | `gMk` 53 | `gPp` 30 | `gWw` 31 | `gZz` 32 | `dS18` 33 |
|---|---|---|---|---|---|---|---|
| value | `[0]` | `fl.map fv` (`-1` long, `0` short; axis 0 on top) | `[mkOf fl]` | `[p]` | `[p+2]` | `[n+ℓ+8]` | `desc18 p ℓ K ts` |

and `[]` on every other stack.
-/

namespace NLogN.KFV

open IntMul KIL Synth

/-- The descriptor stack of Proposition 18. -/
abbrev dS18 : Fin HS := 33

/-- The long-axis flags (`t_i = 2^ℓ`). -/
def fl18 (ℓ : ℕ) (ts : List ℕ) : List Bool := ts.map fun t => decide (t = 2 ^ ℓ)

/-- Number of long axes. -/
def nL18 (ℓ : ℕ) (ts : List ℕ) : ℕ := (fl18 ℓ ts).count true

/-- `Lst = nL + b D`. -/
def lst18 (ℓ K : ℕ) (ts : List ℕ) : ℕ := nL18 ℓ ts + bb ℓ K * ts.length

/-- `n = Lst + D q K`. -/
def n18 (ℓ K : ℕ) (ts : List ℕ) : ℕ := lst18 ℓ K ts + ts.length * qq ℓ K * K

/-- The register frame built by the setup. -/
def regs18 (p ℓ K : ℕ) (ts : List ℕ) (j : Fin HS) : List ℤ :=
  if j = NLogN.KFV.gD then [(ts.length : ℤ)]
  else if j = gLl then [(ℓ : ℤ)]
  else if j = gKk then [(K : ℤ)]
  else if j = gBb then [(bb ℓ K : ℤ)]
  else if j = gQq then [(qq ℓ K : ℤ)]
  else if j = gNL then [(nL18 ℓ ts : ℤ)]
  else if j = gLst then [(lst18 ℓ K ts : ℤ)]
  else if j = gNn then [(n18 ℓ K ts : ℤ)]
  else if j = gH then [0]
  else if j = gLG then (fl18 ℓ ts).map fv
  else if j = gMk then [(mkOf (fl18 ℓ ts) : ℤ)]
  else if j = gPp then [(p : ℤ)]
  else if j = gWw then [((p + 2 : ℕ) : ℤ)]
  else if j = gZz then [((n18 ℓ K ts + ℓ + 8 : ℕ) : ℤ)]
  else if j = dS18 then KFM.desc18 p ℓ K ts
  else []

/-- **The setup interface of Proposition 18.** -/
def Setup18Need : Prop :=
  ∃ (setup teardown : (Pp : ℕ) → IStmt HS Pp) (Cs : ℕ),
  ∀ {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (p ℓ K : ℕ) (ts : List ℕ),
    2 ≤ ℓ → 1 ≤ K → 1 ≤ ts.length → (∀ t ∈ ts, t = 2 ^ ℓ ∨ 2 * t = 2 ^ ℓ) →
    ∀ (s : IState HS) (f : Fin HS → List ℤ),
      (∀ j, j ≠ 0 → j ≠ dS18 → f j = []) → f dS18 = KFM.desc18 p ℓ K ts →
      (∃ c, IRuns Isym tbl (setup Pp) (encK s f) (encK (encK s (regs18 p ℓ K ts)) (o0 (f 0))) c ∧
        c ≤ Cs * (ts.length + ℓ + K + zsz (p : ℤ) + 2) ^ 4) ∧
      ∀ v : List ℤ, ∃ c, IRuns Isym tbl (teardown Pp) (encK (encK s (regs18 p ℓ K ts)) (o0 v))
        (encK s (Function.update f 0 v)) c ∧
        c ≤ Cs * (ts.length + ℓ + K + zsz (p : ℤ) + 2) ^ 4

end NLogN.KFV

end

section
-- Source module: Solutions.KFV50Base
/-!
# KFV §50: the base context of the Proposition 18 core

From the register frame `regs18 p ℓ K ts` (with `sT` overwritten by anything) we get the
contexts of the layout programs (`LRg`) and of the rounds (`PCtx`), for `D = |ts|` and
`long i = (t_i = 2^ℓ)`. **`base18_ctx`**.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

/-- The long flags of `ts`. -/
def long18 (ℓ : ℕ) (ts : List ℕ) : Fin ts.length → Bool := fun i => decide (ts[i] = 2 ^ ℓ)

end NLogN.KFV

end

section
-- Source module: Solutions.KFV51Fwd
/-!
# KFV §51: the two layer programs of the Proposition 18 core

* `fwd18 e14 eSw = layIn eSw 7 ; fwdC e14`: row-major → the paper's layout, then Lemma 16
  forward. **`fwd18_ok`**.
* `opp18 e14 eSw = oppC e14 ; layOut eSw 7`: Lemma 16 opposite, then back to row-major.
  **`opp18_ok`**.

Both on the context `Ctx18` (layout registers and a round frame), with the chunk rounds given by
`ChunkU` (from the uniform Proposition 14) and the exchanges by `SwOK` (descriptor on stack `7`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-- The descriptor stack of the exchanges. -/
abbrev dW18 : Fin HS := 7

/-- The forward layer program. -/
def fwd18 (e14 eSw : Fin Pp) : IStmt HS Pp := .seq (layIn eSw dW18) (fwdC e14)

/-- The opposite layer program. -/
def opp18 (e14 eSw : Fin Pp) : IStmt HS Pp := .seq (oppC e14) (layOut eSw dW18)

section Paper

open GlueLayout GlueP14 GlueError

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- The context of the layer programs. -/
def Ctx18 (p W Z : ℕ) (s : IState HS) : Prop :=
  LRg s (pLP D ℓ K long) (mkOf (flOf D long)) W ∧ PCtx (pLP D ℓ K long) (flOf D long) p W Z s

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV52Body
/-!
# KFV §52: the body of the uniform Proposition 18 program

`body18 su td e14 eSw pM = su ; core18 (fwd18 e14 eSw) (opp18 e14 eSw) pM ; td`.

**`body18_runs`**: from the descriptor `desc18 p ℓ K ts` on `dS18` and `zf` over `zg` on stack `0`
(all else empty, base `s` arbitrary), the body leaves `zh` (over the rest `l`) on stack `0` and
restores everything else; `zh` represents
`(Lout ∘ procQIc) (zipWith ppq ((procQc ∘ Lin) xf) ((procQc ∘ Lin) xg))` scaled by `2^n`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12 GlueLayout GlueP14 GlueError

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-- The body of the Proposition 18 procedure. -/
def body18 (su td : IStmt HS Pp) (e14 eSw pM : Fin Pp) : IStmt HS Pp :=
  .seq su (.seq (core18 (fwd18 e14 eSw) (opp18 e14 eSw) pM) td)

/-- Cost of the core. -/
noncomputable def cCore18 (kF kO n ℓ p B BK φ : ℕ) : ℕ :=
  kF + (cShut (2 * (2 ^ n * 2 ^ ℓ)) B + (kF + (cShut (2 * (2 ^ n * 2 ^ ℓ)) B +
    (cKronS p ℓ n BK φ + (kO + cScale (2 * (2 ^ n * 2 ^ ℓ)) B)))))

end NLogN.KFV

end

section
-- Source module: Solutions.KFMErr18a
/-!
# KFM Err18a: the row-major order and the paper's layout

The uniform Proposition 18 program (`KFV.pipe18c`) reads its row-major input by the `pull` along
`relabel initL tgtL` and writes its output by the `pull` along `relabel tgtL initL`. Here:

* `e18_enc_bits`, `e18_blocks`: a binary address made of `MSB`-first blocks encodes the row-major
  index whose digits are the blocks.
* `initArr`: the initial order `initL` is itself a slot arrangement.
* **`e18_relabel`**: for two slot arrangements, `relabel A B v = addrS A (coordS B v)`.
* `e18rho x`: the row-major index of a box point; **`e18rho_dig`** (its digits over `ts18` are the
  coordinates), `e18rho_lt`, **`e18rho_sub`** (`rho (x ⊖ k) = rmSub (rho x) (rho k)`).
* **`e18_lin`**, **`e18_lout`**: the two `pull`s in coordinates.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open Finset Butterfly AModel Synth GlueLayout

noncomputable section

/-! ## Binary blocks -/

/-! ## Slot arrangements -/

/-! ## The paper's two orders -/

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- The row-major index of a box point. -/
def e18rho (x : Fin D → ℕ) : ℕ :=
  encode (binSh (initL D ℓ long).length) (addrS D (initL D ℓ long) x)

/-- The `MSB`-first bits of coordinate `i`. -/
def e18blk (x : Fin D → ℕ) (i : Fin D) : List ℕ :=
  (List.range (al D ℓ long i)).reverse.map fun h => (getBit h (x i) : ℕ)

theorem e18_ts_len : (KFV.ts18 D ℓ long).length = D := by simp [KFV.ts18]

/-- Cyclic difference of box points. -/
def subB (a : Fin D → ℕ) (x k : Fin D → ℕ) : Fin D → ℕ := fun i => (x i + 2 ^ a i - k i) % 2 ^ a i

/-! ## The two `pull`s -/

/-- The box point of row-major index `j`. -/
def e18sig (j : ℕ) : Fin D → ℕ :=
  coordS D (al D ℓ long) (initL D ℓ long) (decode (binSh (initL D ℓ long).length) j)

end Paper

end

end NLogN.KFM

end