Explicit-budget certificates for register-word glue

This module certifies finite, memory-independent glue in the existing WordRAM.Code language. An emitter takes possibly repeated input registers and a disjoint fresh scratch bank. Its code and instruction budget are chosen before the input values and word width. This follows the emit-and-frame pattern of Multiword.Circuit, specialized to physical words; it does not use that compiler's standard-basis wide-arithmetic semantics for exact-basis operations.

The admissible-input predicate and one envelope for executed values remain explicit. In particular, increasing the width does not justify exact subtraction below zero or a zero divisor. Selection runs only its chosen alternative. Width reads, memory instructions, loops and random sampling are excluded. This is the word-glue component of realization, not a compiler for memory clients or algorithms. The certificate asserts successful execution on its stated domain; it does not assert a converse about executions outside that domain.

Inputs are already in the supplied registers. Their installation, scratch reservation and a final halt are not charged here; the surrounding realization must charge them. Constants, copies, ALU instructions and branch overhead inside the emitted code are charged normally. The interface and closure results are original; the underlying model is WordRAM.Structured.

Main definitions

• Code.IsGlue: the memory-independent, width-independent finite fragment of existing code.
• GlueComputes: a framed scalar computation with an explicit uniform instruction budget.
• GlueComputable: the same contract with only the instruction budget existentially hidden.
• GlueComputes.Witness: retain specified scalar scratch and code under that same contract.

Main results

• GlueComputes.proj, GlueComputes.const: register projections and constants.
• GlueComputes.binary, GlueComputes.comp_many, GlueComputes.select: compositional emission.
• GlueComputes.realize: instantiate the emitter with a concrete finite register layout.
• GlueComputes.mono: explicit weakening of the value envelope and instruction budget.

def Cslib.WordRAM.Code.IsGlue {B : Basis} {r : ℕ} : Code B r → Prop

The register-only finite fragment of Code. Conditions may select a branch, but no loop, memory access, random choice or word-width read is permitted. This is a predicate on the existing language, not a second program syntax.

theorem Cslib.WordRAM.Code.IsGlue.not_readsWidth {B : Basis} {r : ℕ} {c : Code B r} (h : c.IsGlue) : ¬c.ReadsWidth

Register glue does not read the word width, so existing execution monotonicity applies.

def Cslib.WordRAM.GlueComputes.Spec {k : ℕ} (B : Basis) (P : (Fin k → ℕ) → Prop) (f bound : (Fin k → ℕ) → ℕ) (time n : ℕ) (emit : {r : ℕ} → (Fin k → Fin r) → (Fin (n + 1) → Fin r) → Code B r) : Prop

The uniform native contract shared by existential and retained scalar certificates. Inputs may alias; only the scratch bank is fresh and injective. No whole-state boundedness premise is added to the scalar interface.

def Cslib.WordRAM.GlueComputes {k : ℕ} (B : Basis) (P : (Fin k → ℕ) → Prop) (f bound : (Fin k → ℕ) → ℕ) (time : ℕ) : Prop

A scalar register function has a fixed emitter and instruction budget. bound is one top-level value envelope, and P is the fixed admissibility predicate. The scratch bank is fresh and injectively placed; input registers may repeat. Output is in scratch slot zero, memory is unchanged, and registers outside scratch retain their initial contents. Neither the emitter nor the budget may depend on run-time values or the word width.

def Cslib.WordRAM.GlueComputable {k : ℕ} (B : Basis) (f : (Fin k → ℕ) → ℕ) (P : (Fin k → ℕ) → Prop) (bound : (Fin k → ℕ) → ℕ) : Prop

Syntax-directed automation hides only the uniform budget and emitter witness. The basis, admissibility predicate, scalar function and value envelope remain visible parameters.

structure Cslib.WordRAM.GlueComputes.Witness {k : ℕ} (B : Basis) (P : (Fin k → ℕ) → Prop) (f bound : (Fin k → ℕ) → ℕ) (time : ℕ) : Type

A specified scalar emitter with the same contract as GlueComputes. The envelope, scratch and code are retained as data before every runtime value, width and register layout.

• scratchSize : ℕ

  Auxiliary slots, in addition to the scalar result slot.

• code {r : ℕ} : (Fin k → Fin r) → (Fin (self.scratchSize + 1) → Fin r) → Code B r

  The uniform scalar emitter.

• bound_spec (v : Fin k → ℕ) : P v → f v ≤ bound v

  The original visible value envelope.

• code_spec : Spec B P f bound time self.scratchSize fun {r : ℕ} => self.code

  The original native execution and memory/register-frame contract.

theorem Cslib.WordRAM.GlueComputes.Witness.toGlueComputes {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {f bound : (Fin k → ℕ) → ℕ} {time : ℕ} (h : Witness B P f bound time) : GlueComputes B P f bound time

Forget the specified code and scratch without changing the scalar contract.

noncomputable def Cslib.WordRAM.GlueComputes.Witness.ofGlueComputes {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {f bound : (Fin k → ℕ) → ℕ} {time : ℕ} (h : GlueComputes B P f bound time) : Witness B P f bound time

Existential-only fallback. The selected scratch and code need not equal those of any particular derivation; use a supplied Witness when their identities matter.

theorem Cslib.WordRAM.GlueComputes.computable {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {f bound : (Fin k → ℕ) → ℕ} {time : ℕ} (h : GlueComputes B P f bound time) : GlueComputable B f P bound

A checked explicit budget supplies the automation facade.

theorem Cslib.WordRAM.GlueComputes.realize {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {f bound : (Fin k → ℕ) → ℕ} {time : ℕ} (h : GlueComputes B P f bound time) : ∃ (n : ℕ) (code : Code B (k + (n + 1))), code.IsGlue ∧ ∀ (w : ℕ) (v : Fin k → ℕ) (mem : ℕ → ℕ), P v → Fits w (bound v) → ∃ (y : Data (k + (n + 1))), ExecWithin w code { regs := fun (i : Fin (k + (n + 1))) => Fin.addCases v (fun (x : Fin (n + 1)) => 0) i, mem := mem } y time ∧ y.regs (Fin.natAdd k 0) = f v ∧ y.mem = mem ∧ ∀ (i : Fin k), y.regs (Fin.castAdd (n + 1) i) = v i

A canonical finite register layout puts inputs first and fresh scratch after them. The same code and register count work for every valid input and width, and every initial memory is framed. The budget excludes a final halt; a later flat-program export must charge it.

theorem Cslib.WordRAM.GlueComputes.mono {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {f bound bound' : (Fin k → ℕ) → ℕ} {time time' : ℕ} (h : GlueComputes B P f bound time) (hb : ∀ (v : Fin k → ℕ), P v → bound v ≤ bound' v) (ht : time ≤ time') : GlueComputes B P f bound' time'

Weaken the envelope and instruction budget explicitly, outside syntax-directed search.

def Cslib.WordRAM.GlueComputes.Witness.proj {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound : (Fin k → ℕ) → ℕ} (i : Fin k) (hb : ∀ (v : Fin k → ℕ), P v → v i ≤ bound v) : Witness B P (fun (v : Fin k → ℕ) => v i) bound 1

Copy one input register. Its bound is checked against the common visible envelope.

theorem Cslib.WordRAM.GlueComputes.proj {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound : (Fin k → ℕ) → ℕ} (i : Fin k) (hb : ∀ (v : Fin k → ℕ), P v → v i ≤ bound v) : GlueComputes B P (fun (v : Fin k → ℕ) => v i) bound 1

Erase the retained projection certificate.

def Cslib.WordRAM.GlueComputes.Witness.const {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound : (Fin k → ℕ) → ℕ} (z : ℕ) (hb : ∀ (v : Fin k → ℕ), P v → z ≤ bound v) : Witness B P (fun (x : Fin k → ℕ) => z) bound 1

Write a fitting constant.

theorem Cslib.WordRAM.GlueComputes.const {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound : (Fin k → ℕ) → ℕ} (z : ℕ) (hb : ∀ (v : Fin k → ℕ), P v → z ≤ bound v) : GlueComputes B P (fun (x : Fin k → ℕ) => z) bound 1

Erase the retained constant certificate.

def Cslib.WordRAM.GlueComputes.Witness.binary {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g h : (Fin k → ℕ) → ℕ} {tf tg : ℕ} (hf : Witness B P f bound tf) (hg : Witness B P g bound tg) (op : B.Op) (args : Fin (B.Arity op) → Fin 2) (hop : ¬B.ReadsWidth op) (heval : ∀ (v : Fin k → ℕ), P v → ∀ (w : ℕ), (B.interp w op fun (i : Fin (B.Arity op)) => ![f v, g v] (args i)) = some (h v)) (hb : ∀ (v : Fin k → ℕ), P v → h v ≤ bound v) : Witness B P h bound (tf + tg + 1)

Apply a basis operation to two computed words. The operation may repeat or ignore either word in its argument vector. Its interpretation and domain are checked explicitly, at every width; no totalization of a partial basis operation is used. Intermediate executions share the same envelope, and their instruction costs are added without bound search.

@[simp]

theorem Cslib.WordRAM.GlueComputes.Witness.binary_scratchSize {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g h : (Fin k → ℕ) → ℕ} {tf tg : ℕ} (hf : Witness B P f bound tf) (hg : Witness B P g bound tg) (op : B.Op) (args : Fin (B.Arity op) → Fin 2) (hop : ¬B.ReadsWidth op) (heval : ∀ (v : Fin k → ℕ), P v → ∀ (w : ℕ), (B.interp w op fun (i : Fin (B.Arity op)) => ![f v, g v] (args i)) = some (h v)) (hb : ∀ (v : Fin k → ℕ), P v → h v ≤ bound v) : (hf.binary hg op args hop heval hb).scratchSize = hf.scratchSize + hg.scratchSize + 2

Binary composition retains the two disjoint operand banks and one result slot.

theorem Cslib.WordRAM.GlueComputes.binary {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g h : (Fin k → ℕ) → ℕ} {tf tg : ℕ} (hf : GlueComputes B P f bound tf) (hg : GlueComputes B P g bound tg) (op : B.Op) (args : Fin (B.Arity op) → Fin 2) (hop : ¬B.ReadsWidth op) (heval : ∀ (v : Fin k → ℕ), P v → ∀ (w : ℕ), (B.interp w op fun (i : Fin (B.Arity op)) => ![f v, g v] (args i)) = some (h v)) (hb : ∀ (v : Fin k → ℕ), P v → h v ≤ bound v) : GlueComputes B P h bound (tf + tg + 1)

Compose existential certificates using their choice-selected scalar witnesses. For specified scratch and code, use Witness.binary directly.

theorem Cslib.WordRAM.GlueComputes.reindex {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {f bound : (Fin k → ℕ) → ℕ} {time m : ℕ} {Q : (Fin m → ℕ) → Prop} {b : (Fin m → ℕ) → ℕ} (h : GlueComputes B P f bound time) (ρ : Fin k → Fin m) (hP : ∀ (v : Fin m → ℕ), Q v → P (v ∘ ρ)) (hb : ∀ (v : Fin m → ℕ), Q v → bound (v ∘ ρ) ≤ b v) : GlueComputes B Q (fun (v : Fin m → ℕ) => f (v ∘ ρ)) b time

Substitute a register map, including a map with repeated inputs. The emitter accepts arbitrary input layouts, so this substitution needs no staging copies or injectivity premise.

theorem Cslib.WordRAM.GlueComputes.comp_many {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound : (Fin k → ℕ) → ℕ} {m : ℕ} {Q : (Fin m → ℕ) → Prop} {h b : (Fin m → ℕ) → ℕ} {g : (Fin k → ℕ) → Fin m → ℕ} {tf : ℕ} {t : Fin m → ℕ} (hf : GlueComputes B Q h b tf) (hg : ∀ (i : Fin m), GlueComputes B P (fun (v : Fin k → ℕ) => g v i) bound (t i)) (hQ : ∀ (v : Fin k → ℕ), P v → Q (g v)) (hb : ∀ (v : Fin k → ℕ), P v → b (g v) ≤ bound v) : GlueComputes B P (fun (v : Fin k → ℕ) => h (g v)) bound ((List.ofFn t).sum + tf)

Substitute any finite vector of computed arguments into a routine. All component emitters, scratch banks and budgets are fixed before runtime inputs or widths. The forest runs in index order, preserving inputs and earlier results, and then runs the outer routine in its own bank. The one common envelope covers all components and dominates the outer envelope.

theorem Cslib.WordRAM.GlueComputes.comp {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {f bound : (Fin k → ℕ) → ℕ} {g b : (Fin 1 → ℕ) → ℕ} {Q : (Fin 1 → ℕ) → Prop} {tf tg : ℕ} (hf : GlueComputes B P f bound tf) (hg : GlueComputes B Q g b tg) (hQ : ∀ (v : Fin k → ℕ), P v → Q fun (x : Fin 1) => f v) (hb : ∀ (v : Fin k → ℕ), P v → (b fun (x : Fin 1) => f v) ≤ bound v) : GlueComputes B P (fun (v : Fin k → ℕ) => g fun (x : Fin 1) => f v) bound (tf + tg + 1)

Compose two scalar computations, passing the first result as the second computation's single input. Each stage keeps its own explicit domain and envelope; the caller proves the domain implication and envelope domination once.

theorem Cslib.WordRAM.GlueComputes.select {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound : (Fin k → ℕ) → ℕ} (cond : Cond k) {f g : (Fin k → ℕ) → ℕ} {tf tg : ℕ} (hf : GlueComputes B (fun (v : Fin k → ℕ) => P v ∧ cond.Holds { regs := v, mem := fun (x : ℕ) => 0 }) f bound tf) (hg : GlueComputes B (fun (v : Fin k → ℕ) => P v ∧ ¬cond.Holds { regs := v, mem := fun (x : ℕ) => 0 }) g bound tg) : GlueComputes B P (fun (v : Fin k → ℕ) => if cond.Holds { regs := v, mem := fun (x : ℕ) => 0 } then f v else g v) bound (max tf tg + 3)

Select between two computations by an existing register condition. Only the selected branch must satisfy its domain; the inactive branch may fault if executed.

theorem Cslib.WordRAM.GlueComputes.bin_standard {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} {tf tg : ℕ} (hf : GlueComputes Basis.standard P f bound tf) (hg : GlueComputes Basis.standard P g bound tg) (op : BinOp) (hb : ∀ (v : Fin k → ℕ), P v → op.eval (f v) (g v) ≤ bound v) : GlueComputes Basis.standard P (fun (v : Fin k → ℕ) => op.eval (f v) (g v)) bound (tf + tg + 1)

Standard binary operations use the basis's documented total natural-number semantics.

def Cslib.WordRAM.GlueComputes.Witness.binExact {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} {tf tg : ℕ} (hf : Witness Basis.exact P f bound tf) (hg : Witness Basis.exact P g bound tg) (op : BinOp) (hv : ∀ (v : Fin k → ℕ), P v → op.evalExact (f v) (g v) = some (op.eval (f v) (g v))) (hb : ∀ (v : Fin k → ℕ), P v → op.eval (f v) (g v) ≤ bound v) : Witness Basis.exact P (fun (v : Fin k → ℕ) => op.eval (f v) (g v)) bound (tf + tg + 1)

Retain exact binary code and scratch. Definedness of the partial operation on the fixed domain is still required separately from output fit.

@[simp]

theorem Cslib.WordRAM.GlueComputes.Witness.binExact_scratchSize {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} {tf tg : ℕ} (hf : Witness Basis.exact P f bound tf) (hg : Witness Basis.exact P g bound tg) (op : BinOp) (hv : ∀ (v : Fin k → ℕ), P v → op.evalExact (f v) (g v) = some (op.eval (f v) (g v))) (hb : ∀ (v : Fin k → ℕ), P v → op.eval (f v) (g v) ≤ bound v) : (hf.binExact hg op hv hb).scratchSize = hf.scratchSize + hg.scratchSize + 2

Exact binary witnesses retain the original operand-bank accounting without requiring clients to unfold the basis-dependent emitter.

theorem Cslib.WordRAM.GlueComputes.bin_exact {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} {tf tg : ℕ} (hf : GlueComputes Basis.exact P f bound tf) (hg : GlueComputes Basis.exact P g bound tg) (op : BinOp) (hv : ∀ (v : Fin k → ℕ), P v → op.evalExact (f v) (g v) = some (op.eval (f v) (g v))) (hb : ∀ (v : Fin k → ℕ), P v → op.eval (f v) (g v) ≤ bound v) : GlueComputes Basis.exact P (fun (v : Fin k → ℕ) => op.eval (f v) (g v)) bound (tf + tg + 1)

Exact binary operations require their interpretation to be defined on the fixed domain. Output fit alone cannot discharge underflow or a zero divisor.