Native branching in memory-client realizations

The branch test reads only the encoded live words. Both alternatives have uniform emitters; only the selected alternative's domain, fit obligations and local work are required at runtime. The two-instruction allowance includes the jump on the negative path.

Main definitions

• test: interpret an existing native condition on a word-vector environment.

Main results

• test_rename: a renamed native condition tests the words in its source registers.
• branchPrefix_layout, branch_cost_le: prefix-bank layout, frame weakening and cost relaxation.
• Realizes.Witness.branch: retain a native conditional with one shared temporary bank.
• Realizes.branch: erase the supplied branch witness when only existence is needed.

def Cslib.WordRAM.Realization.test {k : ℕ} (c : Cond k) (v : Fin k → ℕ) : Prop

The existing native condition observes the encoded words, without inspecting memory.

@[instance_reducible]

instance Cslib.WordRAM.Realization.instDecidableTest {k : ℕ} (c : Cond k) (v : Fin k → ℕ) : Decidable (test c v)

theorem Cslib.WordRAM.Realization.test_rename {k r : ℕ} (c : Cond k) (src : Fin k → Fin r) (x : Data r) (v : Fin k → ℕ) (h : x.regs ∘ src = v) : (Cond.rename src c).Holds x ↔ test c v

A renamed condition holds of native data exactly when it holds of the words in its source registers.

theorem Cslib.WordRAM.Realization.branchPrefix_layout {r k m M : ℕ} {frontier : Fin r} {src : Fin k → Fin r} {tmp : Fin M → Fin r} (h : m ≤ M) (hi : Function.Injective tmp) (hd : ∀ (i : Fin k) (j : Fin M), src i ≠ tmp j) (hf : ∀ (j : Fin M), tmp j ≠ frontier) : Function.Injective (tmp ∘ Fin.castLE h) ∧ (∀ (i : Fin k) (j : Fin m), src i ≠ (tmp ∘ Fin.castLE h) j) ∧ (∀ (j : Fin m), (tmp ∘ Fin.castLE h) j ≠ frontier) ∧ ∀ {x y : Data r}, (∀ (i : Fin r), i ≠ frontier → (∀ (j : Fin m), (tmp ∘ Fin.castLE h) j ≠ i) → y.regs i = x.regs i) → ∀ (i : Fin r), i ≠ frontier → (∀ (j : Fin M), tmp j ≠ i) → y.regs i = x.regs i

Restricting a temporary bank tmp to a prefix Fin.castLE h preserves injectivity and disjointness from src and frontier, and weakens a prefix frame to a frame on tmp.

theorem Cslib.WordRAM.Realization.branch_cost_le {C Cp Cn t t' e : ℕ} (hC : C ≤ max Cp Cn) (ht : t ≤ t') (he : e ≤ 2) : C * (t + 1) + e ≤ (max Cp Cn + 2) * (t' + 1)

Relax a branch alternative's cost C * (t + 1) + e (with e ≤ 2 control steps) under max Cp Cn + 2 and an enlarged work bound t ≤ t'.

def Cslib.WordRAM.Realization.Realizes.Witness.branch {B : Basis} {δ α : Type} {k l : ℕ} {pos neg : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safePos safeNeg : ℕ → δ → DataStructure.Memory.State → Prop} {workPos workNeg : δ → DataStructure.Memory.State → ℕ} (c : Cond k) (hp : Witness B pos input output safePos workPos) (hn : Witness B neg input output safeNeg workNeg) : Witness B (fun (d : δ) => if test c (input d) then pos d else neg d) input output (fun (w : ℕ) (d : δ) (s : DataStructure.Memory.State) => if test c (input d) then safePos w d s else safeNeg w d s) fun (d : δ) (s : DataStructure.Memory.State) => (if test c (input d) then workPos d s else workNeg d s) + 2

Both alternatives reuse the same temporary prefix: only the larger scratch bank is reserved. The native conditional charges control and requires only the selected domain/work; the supplied code and resource fields remain data before all runtime values.

theorem Cslib.WordRAM.Realization.Realizes.branch {B : Basis} {δ α : Type} {k l : ℕ} {pos neg : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safePos safeNeg : ℕ → δ → DataStructure.Memory.State → Prop} {workPos workNeg : δ → DataStructure.Memory.State → ℕ} (c : Cond k) (hp : Realizes B pos input output safePos workPos) (hn : Realizes B neg input output safeNeg workNeg) : Realizes B (fun (d : δ) => if test c (input d) then pos d else neg d) input output (fun (w : ℕ) (d : δ) (s : DataStructure.Memory.State) => if test c (input d) then safePos w d s else safeNeg w d s) fun (d : δ) (s : DataStructure.Memory.State) => (if test c (input d) then workPos d s else workNeg d s) + 2

Both branch emitters precede all runtime values. Shared result slots and disjointness from live inputs are synthesized internally; the entry domain and work charge select the actual path.

theorem Cslib.WordRAM.Realization.RealizesBounded.branch {B : Basis} {δ α : Type} {k l : ℕ} {pos neg : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safePos safeNeg : ℕ → δ → DataStructure.Memory.State → Prop} {workPos workNeg : δ → DataStructure.Memory.State → ℕ} (c : Cond k) (hp : RealizesBounded B pos input output safePos workPos) (hn : RealizesBounded B neg input output safeNeg workNeg) : RealizesBounded B (fun (d : δ) => if test c (input d) then pos d else neg d) input output (fun (w : ℕ) (d : δ) (s : DataStructure.Memory.State) => if test c (input d) then safePos w d s else safeNeg w d s) fun (d : δ) (s : DataStructure.Memory.State) => (if test c (input d) then workPos d s else workNeg d s) + 2

Frontier-bounded conditional realization.

theorem Cslib.WordRAM.Realization.RealizesBounded.branch₀ {B : Basis} {δ α : Type} {k l : ℕ} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {pos neg : δ → DataStructure.Memory.Prog α} {safePos safeNeg : ℕ → δ → DataStructure.Memory.State → Prop} (c : Cond k) (hp : RealizesBounded B pos input output safePos fun (x : δ) (x_1 : DataStructure.Memory.State) => 0) (hn : RealizesBounded B neg input output safeNeg fun (x : δ) (x_1 : DataStructure.Memory.State) => 0) : RealizesBounded B (fun (d : δ) => if test c (input d) then pos d else neg d) input output (fun (w : ℕ) (d : δ) (s : DataStructure.Memory.State) => if test c (input d) then safePos w d s else safeNeg w d s) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Frontier-bounded branching with the test and jump absorbed (work = 0).