Certified finite-result word glue

A finite family of scalar GlueComputes certificates realizes one faithfully encoded result. Supplied scalar witnesses retain their scratch and code before every runtime input and word width. The proposition-only frontend selects witnesses by classical choice instead. All coordinates reuse a static auxiliary bank disjoint from the output slots, and each computed coordinate is copied into its final slot. Both those copies and the empty-vector case are charged.

optionWords supplies the shared two-word result convention needed by memory-stack and queue clients: none is (0,0) and some v is (1,v). The payload is not incremented, so the largest fitting word remains representable. boolWords retains a zero slot for active-loop tests; a true tag still requires the visible word-fit condition for 1.

Main definitions

• optionWordsWith: a presence tag over any faithful payload-word encoding.
• optionWords: a faithful tag/payload encoding of optional natural words.
• boolWords: a Boolean tag with a retained zero slot for native comparisons.

Main results

• Realizes.Witness.glueVectorOfScalars: retain supplied scalar code and its maximum bank.
• Realizes.Witness.glueVector, Realizes.glueVector: realize a finite result using certified scalar coordinate computations, retaining or erasing the witness data.
• Realizes.addWords, Realizes.increment, Realizes.decrement: charged scalar word arithmetic.
• Realizes.returnNone, Realizes.returnSome: charged optional-word results.

This is a realization rule over the existing memory client and structured native code, not an additional program syntax or execution judgment.

def Cslib.WordRAM.Realization.optionWordsWith {α : Type} {l : ℕ} (payload : α ↪ Fin l → ℕ) : Option α ↪ Fin (l + 1) → ℕ

Prefix a faithful payload encoding by a presence tag. Missing payload words are zero; present payload words retain their values. No decoder or payload-fit bound is implicit.

@[simp]

theorem Cslib.WordRAM.Realization.optionWordsWith_none {α : Type} {l : ℕ} (payload : α ↪ Fin l → ℕ) : (optionWordsWith payload) none = fun (i : Fin (l + 1)) => Fin.cases 0 (fun (x : Fin l) => 0) i

@[simp]

theorem Cslib.WordRAM.Realization.optionWordsWith_some {α : Type} {l : ℕ} (payload : α ↪ Fin l → ℕ) (a : α) : (optionWordsWith payload) (some a) = fun (i : Fin (l + 1)) => Fin.cases 1 (payload a) i

def Cslib.WordRAM.Realization.optionWords : Option ℕ ↪ Fin 2 → ℕ

A presence tag and unshifted payload distinguish none from every some v.

@[simp]

theorem Cslib.WordRAM.Realization.optionWords_none : optionWords none = ![0, 0]

@[simp]

theorem Cslib.WordRAM.Realization.optionWords_some (v : ℕ) : optionWords (some v) = ![1, v]

theorem Cslib.WordRAM.Realization.optionWords_eq_optionWordsWith : optionWords = optionWordsWith (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding

The legacy scalar encoding is the one-word instance of optionWordsWith. Its original vector presentation is retained for existing definitional and simplification clients.

def Cslib.WordRAM.Realization.boolWords : Bool ↪ Fin 2 → ℕ

A Boolean tag with a retained zero slot supports native comparisons without immediates.

@[simp]

theorem Cslib.WordRAM.Realization.boolWords_false : boolWords false = ![0, 0]

@[simp]

theorem Cslib.WordRAM.Realization.boolWords_true : boolWords true = ![1, 0]

def Cslib.WordRAM.Realization.Realizes.Witness.glueVectorOfScalars {B : Basis} {δ α : Type} {k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (f : δ → α) (g bound : Fin l → (Fin k → ℕ) → ℕ) (time : Fin l → ℕ) {P : (Fin k → ℕ) → Prop} (hresult : ∀ (d : δ) (i : Fin l), output (f d) i = g i (input d)) (scalars : (i : Fin l) → GlueComputes.Witness B P (g i) (bound i) (time i)) : Witness B (fun (d : δ) => pure (f d)) input output (fun (w : ℕ) (d : δ) (x : DataStructure.Memory.State) => P (input d) ∧ ∀ (i : Fin l), Fits w (bound i (input d))) fun (x : δ) (x_1 : DataStructure.Memory.State) => ∑ i : Fin l, time i + l

Compute every output coordinate using supplied scalar code and a maximum auxiliary bank. The common domain and all coordinate envelopes remain visible, while code, exchange constant and scratch are uniform. A final neutral copy pays for the empty result without materializing a non-fitting constant.

noncomputable def Cslib.WordRAM.Realization.Realizes.Witness.glueVector {B : Basis} {δ α : Type} {k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (f : δ → α) (g bound : Fin l → (Fin k → ℕ) → ℕ) (time : Fin l → ℕ) {P : (Fin k → ℕ) → Prop} (hresult : ∀ (d : δ) (i : Fin l), output (f d) i = g i (input d)) (hcoord : ∀ (i : Fin l), GlueComputes B P (g i) (bound i) (time i)) : Witness B (fun (d : δ) => pure (f d)) input output (fun (w : ℕ) (d : δ) (x : DataStructure.Memory.State) => P (input d) ∧ ∀ (i : Fin l), Fits w (bound i (input d))) fun (x : δ) (x_1 : DataStructure.Memory.State) => ∑ i : Fin l, time i + l

Existential-only frontend to Witness.glueVectorOfScalars. Each scalar witness is choice-selected once, before runtime; no concrete scratch identity for that choice is asserted. The supplied-data entrypoint avoids this selection and retains its maximum auxiliary bank.

theorem Cslib.WordRAM.Realization.Realizes.glueVector {B : Basis} {δ α : Type} {k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (f : δ → α) (g bound : Fin l → (Fin k → ℕ) → ℕ) (time : Fin l → ℕ) {P : (Fin k → ℕ) → Prop} (hresult : ∀ (d : δ) (i : Fin l), output (f d) i = g i (input d)) (hcoord : ∀ (i : Fin l), GlueComputes B P (g i) (bound i) (time i)) : Realizes B (fun (d : δ) => pure (f d)) input output (fun (w : ℕ) (d : δ) (x : DataStructure.Memory.State) => P (input d) ∧ ∀ (i : Fin l), Fits w (bound i (input d))) fun (x : δ) (x_1 : DataStructure.Memory.State) => ∑ i : Fin l, time i + l

The existential realization of the retained explicitly budgeted vector witness.

theorem Cslib.WordRAM.Realization.Realizes.addWords {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i j : Fin k) : Realizes Basis.exact (fun (d : δ) => pure (input d i + input d j)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (w : ℕ) (d : δ) (x : DataStructure.Memory.State) => Fits w (input d i + input d j)) fun (x : δ) (x_1 : DataStructure.Memory.State) => 3

Add two input words when their sum fits; both projections and the addition are charged.

theorem Cslib.WordRAM.Realization.Realizes.increment {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i : Fin k) : Realizes Basis.exact (fun (d : δ) => pure (input d i + 1)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (w : ℕ) (d : δ) (x : DataStructure.Memory.State) => Fits w (input d i + 1)) fun (x : δ) (x_1 : DataStructure.Memory.State) => 3

Increment an input word with an explicit successor-fit condition and three local units.

theorem Cslib.WordRAM.Realization.Realizes.decrement {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i : Fin k) : Realizes Basis.exact (fun (d : δ) => pure (input d i - 1)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (w : ℕ) (d : δ) (x : DataStructure.Memory.State) => 1 ≤ input d i ∧ Fits w (input d i)) fun (x : δ) (x_1 : DataStructure.Memory.State) => 3

Defined subtraction of one keeps positivity and the input-word envelope explicit.

theorem Cslib.WordRAM.Realization.Realizes.returnNone {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) : Realizes Basis.exact (fun (x : δ) => pure none) input optionWords (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 4

Return the two zero words encoding none, charging both constants and output copies.

theorem Cslib.WordRAM.Realization.Realizes.returnSome {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (j : Fin k) : Realizes Basis.exact (fun (d : δ) => pure (some (input d j))) input optionWords (fun (w : ℕ) (d : δ) (x : DataStructure.Memory.State) => Fits w 1 ∧ Fits w (input d j)) fun (x : δ) (x_1 : DataStructure.Memory.State) => 4

Return a presence tag and unshifted input payload, with both word fits explicit.

theorem Cslib.WordRAM.Realization.RealizesBounded.glueVector {B : Basis} {δ α : Type} {k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (f : δ → α) (g bound : Fin l → (Fin k → ℕ) → ℕ) (time : Fin l → ℕ) {P : (Fin k → ℕ) → Prop} (hresult : ∀ (d : δ) (i : Fin l), output (f d) i = g i (input d)) (hcoord : ∀ (i : Fin l), GlueComputes B P (g i) (bound i) (time i)) : RealizesBounded B (fun (d : δ) => pure (f d)) input output (fun (w : ℕ) (d : δ) (x : DataStructure.Memory.State) => P (input d) ∧ ∀ (i : Fin l), Fits w (bound i (input d))) fun (x : δ) (x_1 : DataStructure.Memory.State) => ∑ i : Fin l, time i + l

Frontier-bounded realization of a finite result vector computed by scalar glue.

theorem Cslib.WordRAM.Realization.RealizesBounded.pure₀ {B : Basis} {δ α : Type} {k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (f : δ → α) (g : Fin l → (Fin k → ℕ) → ℕ) {P : (Fin k → ℕ) → Prop} {bound : (Fin k → ℕ) → ℕ} (need : ℕ → (Fin k → ℕ) → Prop) (hresult : ∀ (d : δ) (i : Fin l), output (f d) i = g i (input d)) (hcoord : ∀ (i : Fin l), GlueComputable B (g i) P bound) (hneed : ∀ (w : ℕ) (v : Fin k → ℕ), (∀ (i : Fin k), Fits w (v i)) → P v → need w v → Fits w (bound v)) : RealizesBounded B (fun (d : δ) => pure (f d)) input output (fun (w : ℕ) (d : δ) (x : DataStructure.Memory.State) => P (input d) ∧ need w (input d)) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Frontier-bounded pure₀ rule with absorbed native glue cost.