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

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

import Definitions.Def_IntMul_Kappa_K_Defs19

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.KFWSub
/-!
# KFW: literals read from registers (the uniformity meta-theorem for register programs)

A uniform register program `U` reads its run-time parameters from registers (tops of stacks).
`RS.sub σ U` replaces each register `i` with `σ i = some v` by the literal `v`; the result is
the (non-uniform) program with baked-in literals, for which a spec is usually already proved.

**`FSp.of_sub`**: if `FSp (U.sub σ) s t c`, the registers of `σ` hold their values in `s`
(`Agree σ s`) and `U` never writes them, then `FSp U s t (400 c)`.  Also `fok_of_sub`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFW

open IntMul RS KFD

/-- Substitute literals for the registers of `σ`. -/
def Ex.sub (σ : Fin HS → Option ℤ) : Ex HS → Ex HS
  | .reg i => match σ i with
    | some v => .lit v
    | none => .reg i
  | .lit c => .lit c
  | .add a b => .add (Ex.sub σ a) (Ex.sub σ b)
  | .neg a => .neg (Ex.sub σ a)
  | .mul a b => .mul (Ex.sub σ a) (Ex.sub σ b)
  | .shl a b => .shl (Ex.sub σ a) (Ex.sub σ b)
  | .quo a b => .quo (Ex.sub σ a) (Ex.sub σ b)
  | .rem a b => .rem (Ex.sub σ a) (Ex.sub σ b)
  | .pow2 a => .pow2 (Ex.sub σ a)
  | .sel c x y => .sel (Ex.sub σ c) (Ex.sub σ x) (Ex.sub σ y)
  | .ndiv a b => .ndiv (Ex.sub σ a) (Ex.sub σ b)
  | .nmod a b => .nmod (Ex.sub σ a) (Ex.sub σ b)

/-- Substitute literals for the registers of `σ` in a register program. -/
def RS.sub (σ : Fin HS → Option ℤ) : RS → RS
  | .skip => .skip
  | .asg i e => .asg i (Ex.sub σ e)
  | .push i e => .push i (Ex.sub σ e)
  | .pop i => .pop i
  | .seq a b => .seq (RS.sub σ a) (RS.sub σ b)
  | .ite c a b => .ite (Ex.sub σ c) (RS.sub σ a) (RS.sub σ b)
  | .rep i n b => .rep i (Ex.sub σ n) (RS.sub σ b)

/-- The registers of `σ` hold their values. -/
def Agree (σ : Fin HS → Option ℤ) (s : IState HS) : Prop :=
  ∀ i v, σ i = some v → ∃ L, s.G i = .int v :: L

section ExLemmas

variable (σ : Fin HS → Option ℤ) {s : IState HS}

end ExLemmas

/-- The registers of `σ` are clean (not expression scratch). -/
def SClean (σ : Fin HS → Option ℤ) : Prop := ∀ i, (σ i).isSome → i ∉ zX.all

/-- The registers of `σ` are not written by `p`. -/
def NoW (σ : Fin HS → Option ℤ) (p : RS) : Prop := ∀ i ∈ p.writes, σ i = none

end NLogN.KFW

end

section
-- Source module: Solutions.KFWBase
/-!
# KFW: header refinement, uniform leaves, parameters in the background

* `HRef p p' X`: `p'` is `p` with some (non-loop) pushes of literals `v` replaced by closed
  expressions of value `v`; `HRef.fsp`: `FSp p s t c → FSp p' s t (c + X)`.
* `RS.sub_id`: substituting registers a program never touches changes nothing.
* `FSp.uni`: `FSp O s t c`, `HRef O (U.sub σ) X`, the registers of `σ` hold their values and are
  not written ⇒ `FSp U s t (400 (c + X))` (and `fok U` from `fok O`).
* `encK_pushSt`, `agree_pushSt`, **`leafPush`**: a uniform leaf `withPushI pl (fcode U)` from the
  non-uniform spec of `O` on the background with the pushed parameters.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFW

open IntMul RS KFD KIL

/-! ## Header refinement -/

/-- `p'` is `p` with some top-level pushes of literals replaced by closed expressions. -/
inductive HRef : RS → RS → ℕ → Prop
  | refl (p : RS) : HRef p p 0
  | seq {a a' b b' : RS} {X Y : ℕ} : HRef a a' X → HRef b b' Y → HRef (.seq a b) (.seq a' b') (X + Y)
  | ite {c : Ex HS} {a a' b b' : RS} {X Y : ℕ} : HRef a a' X → HRef b b' Y →
      HRef (.ite c a b) (.ite c a' b') (X + Y)
  | push {i : Fin HS} {v : ℤ} {e : Ex HS} {X : ℕ} : e.regs = [] → (∀ s, e.eval s = v) →
      (∀ s, e.ok s) → (∀ s, e.cost s ≤ X) → HRef (.push i (.lit v)) (.push i e) X
  | mono {p p' : RS} {X Y : ℕ} : HRef p p' X → X ≤ Y → HRef p p' Y

/-! ## Substitution of untouched registers -/

/-! ## Uniform register programs -/

/-! ## Pushed parameters in the background -/

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

end NLogN.KFW

end