Compositional certificates and fun_prop automation for register-word glue

This module re-exports CslibFrontier.Computability.WordRAM.Glue.Basic and provides the staged comparison-operand selection combinators (GlueComputes.stage_pair, GlueComputes.ite_eq_staged, GlueComputes.ite_lt_staged) together with the @[fun_prop] closure rules on GlueComputable.

Main results

• GlueComputes.stage_pair, GlueComputes.ite_eq_staged, GlueComputes.ite_lt_staged: staged-operand selection with explicit guard and branch costs.
• GlueComputable.proj, GlueComputable.const, GlueComputable.comp, GlueComputable.comp_many: register projections, constants, and scalar/vector composition.
• GlueComputable.ite_eq, GlueComputable.ite_lt: lazy branch selection on equality and < between input registers, which stages nothing and so imposes no envelope obligation on them.
• GlueComputable.ite_eq_staged, GlueComputable.ite_lt_staged: lazy branch selection on equality and < between arbitrary certified computed operands.
• GlueComputable.add, GlueComputable.sub, GlueComputable.mul, GlueComputable.div, GlueComputable.mod, GlueComputable.and, GlueComputable.or, GlueComputable.xor, GlueComputable.shiftLeft, GlueComputable.shiftRight (and *_standard): exact- and standard-basis binary closure rules.

theorem Cslib.WordRAM.GlueComputes.stage_pair {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound lhs rhs : (Fin k → ℕ) → ℕ} {Q : (Fin (k + 2) → ℕ) → Prop} {h : (Fin (k + 2) → ℕ) → ℕ} {tl tr tc : ℕ} (hl : GlueComputes B P lhs bound tl) (hr : GlueComputes B P rhs bound tr) (hc : GlueComputes B Q h (fun (v' : Fin (k + 2) → ℕ) => bound (v' ∘ Fin.castAdd 2)) tc) (hQ : ∀ (v : Fin k → ℕ), P v → Q fun (i : Fin (k + 2)) => Fin.addCases v ![lhs v, rhs v] i) : GlueComputes B P (fun (v : Fin k → ℕ) => h fun (i : Fin (k + 2)) => Fin.addCases v ![lhs v, rhs v] i) bound (tl + tr + tc)

Stage two computed words into fresh scratch slots and run a (k + 2)-input computation over the original k input registers together with the two staged words, without copying the original input registers.

theorem Cslib.WordRAM.GlueComputes.ite_eq_staged {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound lhs rhs f g : (Fin k → ℕ) → ℕ} {tl tr tf tg : ℕ} (hl : GlueComputes B P lhs bound tl) (hr : GlueComputes B P rhs bound tr) (hf : GlueComputes B (fun (v : Fin k → ℕ) => P v ∧ lhs v = rhs v) f bound tf) (hg : GlueComputes B (fun (v : Fin k → ℕ) => P v ∧ ¬lhs v = rhs v) g bound tg) : GlueComputes B P (fun (v : Fin k → ℕ) => if lhs v = rhs v then f v else g v) bound (tl + tr + (max tf tg + 3))

Select between two computations by equality of two computed words. Both guard operands are staged once before the branch, and only the selected branch is executed.

theorem Cslib.WordRAM.GlueComputes.ite_lt_staged {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound lhs rhs f g : (Fin k → ℕ) → ℕ} {tl tr tf tg : ℕ} (hl : GlueComputes B P lhs bound tl) (hr : GlueComputes B P rhs bound tr) (hf : GlueComputes B (fun (v : Fin k → ℕ) => P v ∧ lhs v < rhs v) f bound tf) (hg : GlueComputes B (fun (v : Fin k → ℕ) => P v ∧ ¬lhs v < rhs v) g bound tg) : GlueComputes B P (fun (v : Fin k → ℕ) => if lhs v < rhs v then f v else g v) bound (tl + tr + (max tf tg + 3))

Select between two computations by unsigned comparison of two computed words. Both guard operands are staged once before the branch, and only the selected branch is executed.

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

Register projections are found without searching for a budget.

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

Constants are found without searching for a budget.

theorem Cslib.WordRAM.GlueComputable.comp {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f : (Fin k → ℕ) → ℕ} {h : ℕ → ℕ} {b : (Fin 1 → ℕ) → ℕ} {Q : (Fin 1 → ℕ) → Prop} (hf : GlueComputable B f P bound) (hh : GlueComputable B (fun (v : Fin 1 → ℕ) => h (v 0)) Q b) (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) : GlueComputable B (fun (v : Fin k → ℕ) => h (f v)) P bound

Reuse a named scalar computation after another computation, with explicit domain and envelope implications. This rule searches for the two functions, never for a budget.

theorem Cslib.WordRAM.GlueComputable.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 → ℕ} (hh : GlueComputable B h Q b) (hg : ∀ (i : Fin m), GlueComputable B (fun (v : Fin k → ℕ) => g v i) P bound) (hQ : ∀ (v : Fin k → ℕ), P v → Q (g v)) (hb : ∀ (v : Fin k → ℕ), P v → b (g v) ≤ bound v) : GlueComputable B (fun (v : Fin k → ℕ) => h (g v)) P bound

Apply an opaque routine to any finite vector of computed local words. The component budgets are chosen uniformly, before the input/width quantifiers, and then summed explicitly.

theorem Cslib.WordRAM.GlueComputable.vec_cons {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f : (Fin k → ℕ) → ℕ} {m : ℕ} {g : (Fin k → ℕ) → Fin m → ℕ} (hf : GlueComputable B f P bound) (hg : ∀ (i : Fin m), GlueComputable B (fun (v : Fin k → ℕ) => g v i) P bound) (i : Fin (m + 1)) : GlueComputable B (fun (v : Fin k → ℕ) => Matrix.vecCons (f v) (g v) i) P bound

Indexing a finite tuple is compile-time routing, so it adds no runtime instruction.

theorem Cslib.WordRAM.GlueComputable.vec_single {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f : (Fin k → ℕ) → ℕ} (hf : GlueComputable B f P bound) (i : Fin 1) : GlueComputable B (fun (v : Fin k → ℕ) => ![f v] i) P bound

A singleton tuple has just its computed head; there is no empty-tail obligation.

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

Register-condition selection retains branch-specific domains.

theorem Cslib.WordRAM.GlueComputable.ite_eq {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (i j : Fin k) (hf : GlueComputable B f (fun (v : Fin k → ℕ) => P v ∧ v i = v j) bound) (hg : GlueComputable B g (fun (v : Fin k → ℕ) => P v ∧ ¬v i = v j) bound) : GlueComputable B (fun (v : Fin k → ℕ) => if v i = v j then f v else g v) P bound

Select by equality of input words, without evaluating the unchosen computation. The guard compares the input registers directly, so the operands need not fit the result envelope.

theorem Cslib.WordRAM.GlueComputable.ite_lt {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (i j : Fin k) (hf : GlueComputable B f (fun (v : Fin k → ℕ) => P v ∧ v i < v j) bound) (hg : GlueComputable B g (fun (v : Fin k → ℕ) => P v ∧ ¬v i < v j) bound) : GlueComputable B (fun (v : Fin k → ℕ) => if v i < v j then f v else g v) P bound

Select by unsigned comparison of input words. The guard compares the input registers directly, so the operands need not fit the result envelope.

theorem Cslib.WordRAM.GlueComputable.ite_eq_staged {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g lhs rhs : (Fin k → ℕ) → ℕ} (hl : GlueComputable B lhs P bound) (hr : GlueComputable B rhs P bound) (hf : GlueComputable B f (fun (v : Fin k → ℕ) => P v ∧ lhs v = rhs v) bound) (hg : GlueComputable B g (fun (v : Fin k → ℕ) => P v ∧ ¬lhs v = rhs v) bound) : GlueComputable B (fun (v : Fin k → ℕ) => if lhs v = rhs v then f v else g v) P bound

Select by equality of computed words, without evaluating the unchosen computation. Both operands are staged, so each must be certified within the result envelope; ite_eq handles direct input-register comparisons without that obligation.

theorem Cslib.WordRAM.GlueComputable.ite_lt_staged {B : Basis} {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g lhs rhs : (Fin k → ℕ) → ℕ} (hl : GlueComputable B lhs P bound) (hr : GlueComputable B rhs P bound) (hf : GlueComputable B f (fun (v : Fin k → ℕ) => P v ∧ lhs v < rhs v) bound) (hg : GlueComputable B g (fun (v : Fin k → ℕ) => P v ∧ ¬lhs v < rhs v) bound) : GlueComputable B (fun (v : Fin k → ℕ) => if lhs v < rhs v then f v else g v) P bound

Select by unsigned comparison of computed words, without evaluating the unchosen computation. Both operands are staged, so each must be certified within the result envelope; ite_lt handles direct input-register comparisons without that obligation.

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

The standard basis's binary operation rule.

theorem Cslib.WordRAM.GlueComputable.bin_exact {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.exact f P bound) (hg : GlueComputable Basis.exact g P bound) (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) : GlueComputable Basis.exact (fun (v : Fin k → ℕ) => op.eval (f v) (g v)) P bound

The exact basis's binary operation rule keeps its domain premise explicit.

theorem Cslib.WordRAM.GlueComputable.add {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.exact f P bound) (hg : GlueComputable Basis.exact g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v + g v ≤ bound v) : GlueComputable Basis.exact (fun (v : Fin k → ℕ) => f v + g v) P bound

Closure under exact-basis add; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.sub {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.exact f P bound) (hg : GlueComputable Basis.exact g P bound) (hv : ∀ (v : Fin k → ℕ), P v → g v ≤ f v) (hb : ∀ (v : Fin k → ℕ), P v → f v - g v ≤ bound v) : GlueComputable Basis.exact (fun (v : Fin k → ℕ) => f v - g v) P bound

Closure under exact-basis sub; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.mul {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.exact f P bound) (hg : GlueComputable Basis.exact g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v * g v ≤ bound v) : GlueComputable Basis.exact (fun (v : Fin k → ℕ) => f v * g v) P bound

Closure under exact-basis mul; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.div {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.exact f P bound) (hg : GlueComputable Basis.exact g P bound) (hv : ∀ (v : Fin k → ℕ), P v → g v ≠ 0) (hb : ∀ (v : Fin k → ℕ), P v → f v / g v ≤ bound v) : GlueComputable Basis.exact (fun (v : Fin k → ℕ) => f v / g v) P bound

Closure under exact-basis div; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.mod {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.exact f P bound) (hg : GlueComputable Basis.exact g P bound) (hv : ∀ (v : Fin k → ℕ), P v → g v ≠ 0) (hb : ∀ (v : Fin k → ℕ), P v → f v % g v ≤ bound v) : GlueComputable Basis.exact (fun (v : Fin k → ℕ) => f v % g v) P bound

Closure under exact-basis mod; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.and {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.exact f P bound) (hg : GlueComputable Basis.exact g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v &&& g v ≤ bound v) : GlueComputable Basis.exact (fun (v : Fin k → ℕ) => f v &&& g v) P bound

Closure under exact-basis and; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.or {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.exact f P bound) (hg : GlueComputable Basis.exact g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v ||| g v ≤ bound v) : GlueComputable Basis.exact (fun (v : Fin k → ℕ) => f v ||| g v) P bound

Closure under exact-basis or; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.xor {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.exact f P bound) (hg : GlueComputable Basis.exact g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v ^^^ g v ≤ bound v) : GlueComputable Basis.exact (fun (v : Fin k → ℕ) => f v ^^^ g v) P bound

Closure under exact-basis xor; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.shiftLeft {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.exact f P bound) (hg : GlueComputable Basis.exact g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v <<< g v ≤ bound v) : GlueComputable Basis.exact (fun (v : Fin k → ℕ) => f v <<< g v) P bound

Closure under exact-basis shiftLeft; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.shiftRight {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.exact f P bound) (hg : GlueComputable Basis.exact g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v >>> g v ≤ bound v) : GlueComputable Basis.exact (fun (v : Fin k → ℕ) => f v >>> g v) P bound

Closure under exact-basis shiftRight; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.add_standard {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.standard f P bound) (hg : GlueComputable Basis.standard g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v + g v ≤ bound v) : GlueComputable Basis.standard (fun (v : Fin k → ℕ) => f v + g v) P bound

Closure under standard-basis add; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.sub_standard {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.standard f P bound) (hg : GlueComputable Basis.standard g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v - g v ≤ bound v) : GlueComputable Basis.standard (fun (v : Fin k → ℕ) => f v - g v) P bound

Closure under standard-basis sub; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.mul_standard {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.standard f P bound) (hg : GlueComputable Basis.standard g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v * g v ≤ bound v) : GlueComputable Basis.standard (fun (v : Fin k → ℕ) => f v * g v) P bound

Closure under standard-basis mul; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.div_standard {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.standard f P bound) (hg : GlueComputable Basis.standard g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v / g v ≤ bound v) : GlueComputable Basis.standard (fun (v : Fin k → ℕ) => f v / g v) P bound

Closure under standard-basis div; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.mod_standard {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.standard f P bound) (hg : GlueComputable Basis.standard g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v % g v ≤ bound v) : GlueComputable Basis.standard (fun (v : Fin k → ℕ) => f v % g v) P bound

Closure under standard-basis mod; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.and_standard {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.standard f P bound) (hg : GlueComputable Basis.standard g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v &&& g v ≤ bound v) : GlueComputable Basis.standard (fun (v : Fin k → ℕ) => f v &&& g v) P bound

Closure under standard-basis and; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.or_standard {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.standard f P bound) (hg : GlueComputable Basis.standard g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v ||| g v ≤ bound v) : GlueComputable Basis.standard (fun (v : Fin k → ℕ) => f v ||| g v) P bound

Closure under standard-basis or; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.xor_standard {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.standard f P bound) (hg : GlueComputable Basis.standard g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v ^^^ g v ≤ bound v) : GlueComputable Basis.standard (fun (v : Fin k → ℕ) => f v ^^^ g v) P bound

Closure under standard-basis xor; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.shiftLeft_standard {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.standard f P bound) (hg : GlueComputable Basis.standard g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v <<< g v ≤ bound v) : GlueComputable Basis.standard (fun (v : Fin k → ℕ) => f v <<< g v) P bound

Closure under standard-basis shiftLeft; the common envelope also bounds this result.

theorem Cslib.WordRAM.GlueComputable.shiftRight_standard {k : ℕ} {P : (Fin k → ℕ) → Prop} {bound f g : (Fin k → ℕ) → ℕ} (hf : GlueComputable Basis.standard f P bound) (hg : GlueComputable Basis.standard g P bound) (hb : ∀ (v : Fin k → ℕ), P v → f v >>> g v ≤ bound v) : GlueComputable Basis.standard (fun (v : Fin k → ℕ) => f v >>> g v) P bound

Closure under standard-basis shiftRight; the common envelope also bounds this result.