Structured word-RAM programs

Flat programs (Cslib.WordRAM.Program) are lists of instructions with numeric jump targets, which is inconvenient to write and to reason about. A structured program (Cslib.WordRAM.Code) is built from data instructions by sequencing, conditionals and while loops on the comparisons of Cslib.WordRAM.Cond. It has a big-step semantics (Cslib.WordRAM.Exec) that counts exactly the instructions of the flat program it compiles to (Cslib.WordRAM.Code.assemble, Cslib.WordRAM.Exec.runs): a conditional costs one branch instruction, plus a jump when the second alternative runs, and a loop costs a branch and a jump per test. No rule executes a Lean function as one instruction.

Proofs about structured programs mostly need upper bounds on time rather than exact counts, and Cslib.WordRAM.ExecWithin packages these. Its rules compose like Hoare logic, with time bounds added along sequences:

• Cslib.WordRAM.ExecWithin.const, ….alu, ….copy, ….load, ….store: forward rules for the data instructions, with the resulting data in closed form, and ….bin, ….width for the operations of the standard basis;
• Cslib.WordRAM.ExecWithin.seq, ….branch_pos, ….branch_neg: sequencing and conditionals;
• Cslib.WordRAM.ExecWithin.loop: a loop through an explicit family of states, and Cslib.WordRAM.ExecWithin.loop_invariant: a loop with an invariant and a decreasing measure, whose iterations are counted by the measure.

Loop-free code can instead be executed symbolically: Cslib.WordRAM.Code.eval is a structurally recursive interpreter, so simp and decide evaluate it, and Cslib.WordRAM.Exec.of_eval turns its result into an execution.

Subprograms are reused through Cslib.WordRAM.Code.rename, which runs a program on any injectively chosen registers of a larger register file and leaves the others untouched (Cslib.WordRAM.Exec.rename).

Main definitions

• Cslib.WordRAM.Code: structured programs over a basis, and Cslib.WordRAM.Code.size, the length of the flat program they compile to.
• Cslib.WordRAM.Exec, Cslib.WordRAM.ExecWithin: executions with an exact instruction count, and within a time bound.
• Cslib.WordRAM.Code.eval: an interpreter with a budget of loop iterations.
• Cslib.WordRAM.Code.rename: running a program on other registers.

Main results

• Cslib.WordRAM.Exec.unique: executions are deterministic.
• Cslib.WordRAM.Exec.of_eval: the interpreter only finds executions.
• Cslib.WordRAM.ExecWithin.loop_invariant: the loop rule with an invariant and a measure.
• Cslib.WordRAM.Exec.regs_eq: registers that a program never writes keep their contents.
• Cslib.WordRAM.Exec.rename: renamed programs run on the chosen registers.
• Cslib.WordRAM.Exec.mono_width, Cslib.WordRAM.Exec.bounded: a program that does not read the word size runs in the same way at every larger word size, and executions keep data word-sized.

References

• MIT–ULB CompGeom Group, Undecidability of tiling with a tromino; the structured programs, their cost-exact semantics, register preservation and register embedding are adapted from its accompanying Lean formalization.

Structured programs

inductive Cslib.WordRAM.Code (B : Basis) (r : ℕ) : Type

Structured programs: data instructions combined by sequencing, conditionals and loops.

• op {B : Basis} {r : ℕ} (o : Op B r) : Code B r

  A data instruction.

• seq {B : Basis} {r : ℕ} (c₁ c₂ : Code B r) : Code B r

  Run c₁, then c₂.

• branch {B : Basis} {r : ℕ} (c : Cond r) (pos neg : Code B r) : Code B r

  Run pos if c holds, and neg otherwise.

• loop {B : Basis} {r : ℕ} (c : Cond r) (body : Code B r) : Code B r

  Run body while c holds.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableEqCode {B✝ : Basis} {r✝ : ℕ} : DecidableEq (Code B✝ r✝)

def Cslib.WordRAM.instDecidableEqCode.decEq {B✝ : Basis} {r✝ : ℕ} (x✝ x✝¹ : Code B✝ r✝) : Decidable (x✝ = x✝¹)

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

The length of the flat program a structured program compiles to.

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

A structured program reads the word size if one of its instructions does.

@[instance_reducible]

instance Cslib.WordRAM.Code.decidableReadsWidth {B : Basis} {r : ℕ} (c : Code B r) : Decidable c.ReadsWidth

Executions

inductive Cslib.WordRAM.Exec {B : Basis} {r : ℕ} (w : ℕ) : Code B r → Data r → Data r → ℕ → Prop

Exec w c x y n: at word size w, the structured program c leads from data x to data y executing exactly n instructions of the flat program it compiles to.

• op {B : Basis} {r w : ℕ} {o : Op B r} {x y : Data r} : Op.eval w o x = some y → Exec w (Code.op o) x y 1

  A data instruction is one instruction.

• seq {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x y z : Data r} {m n : ℕ} : Exec w c₁ x y m → Exec w c₂ y z n → Exec w (c₁.seq c₂) x z (m + n)

  Sequencing adds the instruction counts.

• branch_pos {B : Basis} {r w : ℕ} {c : Cond r} {pos neg : Code B r} {x y : Data r} {n : ℕ} : c.Holds x → Exec w pos x y n → Exec w (Code.branch c pos neg) x y (n + 1)

  The first alternative of a conditional costs one branch instruction.

• branch_neg {B : Basis} {r w : ℕ} {c : Cond r} {pos neg : Code B r} {x y : Data r} {n : ℕ} : ¬c.Holds x → Exec w neg x y n → Exec w (Code.branch c pos neg) x y (n + 2)

  The second alternative of a conditional costs a branch and a jump.

• loop_exit {B : Basis} {r w : ℕ} {c : Cond r} {body : Code B r} {x : Data r} : ¬c.Holds x → Exec w (Code.loop c body) x x 2

  Leaving a loop costs a branch and a jump.

• loop_iter {B : Basis} {r w : ℕ} {c : Cond r} {body : Code B r} {x y z : Data r} {m n : ℕ} : c.Holds x → Exec w body x y m → Exec w (Code.loop c body) y z n → Exec w (Code.loop c body) x z (m + n + 2)

  An iteration of a loop costs its body, a branch and a jump back.

def Cslib.WordRAM.ExecWithin {B : Basis} {r : ℕ} (w : ℕ) (c : Code B r) (x y : Data r) (T : ℕ) : Prop

ExecWithin w c x y T: at word size w, the structured program c leads from data x to data y within T instructions.

theorem Cslib.WordRAM.Exec.unique {B : Basis} {r w : ℕ} {c : Code B r} {x y y' : Data r} {n n' : ℕ} (h : Exec w c x y n) (h' : Exec w c x y' n') : y = y' ∧ n = n'

Executions are deterministic.

theorem Cslib.WordRAM.Exec.within {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {n : ℕ} (h : Exec w c x y n) : ExecWithin w c x y n

Data instructions

Each data instruction leads to explicitly given data in one instruction. Only constants and operations need the written number to fit a word.

theorem Cslib.WordRAM.Exec.const {B : Basis} {r w : ℕ} {x : Data r} {d : Fin r} {v : ℕ} (h : Fits w v) : Exec w (Code.op (Op.const d v)) x (x.set d v) 1

theorem Cslib.WordRAM.Exec.alu {B : Basis} {r w : ℕ} {x : Data r} {d : Fin r} {f : B.Op} {args : Fin (B.Arity f) → Fin r} {v : ℕ} (hf : B.interp w f (x.regs ∘ args) = some v) (h : Fits w v) : Exec w (Code.op (Op.alu f d args)) x (x.set d v) 1

theorem Cslib.WordRAM.Exec.copy {B : Basis} {r w : ℕ} {x : Data r} {d s : Fin r} : Exec w (Code.op (Op.copy d s)) x (x.set d (x.regs s)) 1

theorem Cslib.WordRAM.Exec.load {B : Basis} {r w : ℕ} {x : Data r} {d a : Fin r} : Exec w (Code.op (Op.load d a)) x (x.set d (x.mem (x.regs a))) 1

theorem Cslib.WordRAM.Exec.store {B : Basis} {r w : ℕ} {x : Data r} {a s : Fin r} : Exec w (Code.op (Op.store a s)) x (x.write (x.regs a) (x.regs s)) 1

theorem Cslib.WordRAM.Exec.bin {r w : ℕ} {x : Data r} {d i j : Fin r} {f : BinOp} (h : Fits w (f.eval (x.regs i) (x.regs j))) : Exec w (Code.op (Op.bin f d i j)) x (x.set d (f.eval (x.regs i) (x.regs j))) 1

theorem Cslib.WordRAM.Exec.width {r w : ℕ} {x : Data r} {d : Fin r} : Exec w (Code.op (Op.width d)) x (x.set d w) 1

theorem Cslib.WordRAM.Exec.loop_once {B : Basis} {r w : ℕ} {c : Cond r} {body : Code B r} {x y : Data r} {m : ℕ} (hc : c.Holds x) (h : Exec w body x y m) (hy : ¬c.Holds y) : Exec w (Code.loop c body) x y (m + 4)

A loop whose condition holds initially and fails after one body execution runs in m + 4 instructions.

theorem Cslib.WordRAM.Exec.loop {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} (xs : ℕ → Data r) (k T : ℕ) (hc : ∀ i < k, cond.Holds (xs i)) (hk : ¬cond.Holds (xs k)) (hbody : ∀ i < k, Exec w body (xs i) (xs (i + 1)) T) : Exec w (Code.loop cond body) (xs 0) (xs k) (k * (T + 2) + 2)

A loop through the states xs 0, …, xs k: the condition holds at the first k of them and fails at the last, and the body leads from each to the next in T instructions.

Time bounds

theorem Cslib.WordRAM.ExecWithin.mono {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {T T₂ : ℕ} (h : ExecWithin w c x y T) (hT : T ≤ T₂) : ExecWithin w c x y T₂

theorem Cslib.WordRAM.ExecWithin.op {B : Basis} {r w : ℕ} {x y : Data r} {o : Op B r} (h : Op.eval w o x = some y) : ExecWithin w (Code.op o) x y 1

theorem Cslib.WordRAM.ExecWithin.seq {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x y z : Data r} {T₁ T₂ : ℕ} (h₁ : ExecWithin w c₁ x y T₁) (h₂ : ExecWithin w c₂ y z T₂) : ExecWithin w (c₁.seq c₂) x z (T₁ + T₂)

theorem Cslib.WordRAM.ExecWithin.branch_pos {B : Basis} {r w : ℕ} {pos neg : Code B r} {cond : Cond r} {x y : Data r} {T : ℕ} (hc : cond.Holds x) (h : ExecWithin w pos x y T) : ExecWithin w (Code.branch cond pos neg) x y (T + 1)

theorem Cslib.WordRAM.ExecWithin.branch_neg {B : Basis} {r w : ℕ} {pos neg : Code B r} {cond : Cond r} {x y : Data r} {T : ℕ} (hc : ¬cond.Holds x) (h : ExecWithin w neg x y T) : ExecWithin w (Code.branch cond pos neg) x y (T + 2)

theorem Cslib.WordRAM.ExecWithin.branch {B : Basis} {r w : ℕ} {pos neg : Code B r} {cond : Cond r} {x y : Data r} {T : ℕ} (hpos : cond.Holds x → ExecWithin w pos x y T) (hneg : ¬cond.Holds x → ExecWithin w neg x y T) : ExecWithin w (Code.branch cond pos neg) x y (T + 2)

A conditional, with one time bound for both alternatives.

theorem Cslib.WordRAM.ExecWithin.loop_exit {B : Basis} {r w : ℕ} {body : Code B r} {cond : Cond r} {x : Data r} (hc : ¬cond.Holds x) : ExecWithin w (Code.loop cond body) x x 2

theorem Cslib.WordRAM.ExecWithin.loop_iter {B : Basis} {r w : ℕ} {body : Code B r} {cond : Cond r} {x y z : Data r} {T₁ T₂ : ℕ} (hc : cond.Holds x) (h₁ : ExecWithin w body x y T₁) (h₂ : ExecWithin w (Code.loop cond body) y z T₂) : ExecWithin w (Code.loop cond body) x z (T₁ + T₂ + 2)

theorem Cslib.WordRAM.ExecWithin.loop_once {B : Basis} {r w : ℕ} {body : Code B r} {cond : Cond r} {x y : Data r} {T : ℕ} (hc : cond.Holds x) (h : ExecWithin w body x y T) (hy : ¬cond.Holds y) : ExecWithin w (Code.loop cond body) x y (T + 4)

A loop whose condition holds initially and fails after one body execution runs within T + 4 instructions.

theorem Cslib.WordRAM.ExecWithin.loop {B : Basis} {r w : ℕ} {body : Code B r} {cond : Cond r} (xs : ℕ → Data r) (k T : ℕ) (hc : ∀ i < k, cond.Holds (xs i)) (hk : ¬cond.Holds (xs k)) (hbody : ∀ i < k, ExecWithin w body (xs i) (xs (i + 1)) T) : ExecWithin w (Code.loop cond body) (xs 0) (xs k) (k * (T + 2) + 2)

Loop rule, explicit states. If the condition holds at xs 0, …, xs (k - 1) and fails at xs k, and the body leads from each state to the next within T instructions, the loop leads from xs 0 to xs k within k (T + 2) + 2 instructions.

theorem Cslib.WordRAM.ExecWithin.loop_invariant {B : Basis} {r w : ℕ} {body : Code B r} {cond : Cond r} {x : Data r} (I : Data r → Prop) (μ : Data r → ℕ) {T : ℕ} (hbody : ∀ (x : Data r), I x → cond.Holds x → ∃ (y : Data r), ExecWithin w body x y T ∧ I y ∧ μ y < μ x) (hx : I x) : ∃ (y : Data r), ExecWithin w (Code.loop cond body) x y (μ x * (T + 2) + 2) ∧ I y ∧ ¬cond.Holds y

Loop rule, invariant and measure. If every state satisfying the invariant I and the condition is led by the body, within T instructions, to a state satisfying I with a smaller measure μ, then from a state satisfying I the loop terminates within μ x (T + 2) + 2 instructions, in a state satisfying I where the condition fails.

Data instructions

theorem Cslib.WordRAM.ExecWithin.const {B : Basis} {r w : ℕ} {x : Data r} {d : Fin r} {v : ℕ} (h : Fits w v) : ExecWithin w (Code.op (Op.const d v)) x (x.set d v) 1

theorem Cslib.WordRAM.ExecWithin.alu {B : Basis} {r w : ℕ} {x : Data r} {d : Fin r} {f : B.Op} {args : Fin (B.Arity f) → Fin r} {v : ℕ} (hf : B.interp w f (x.regs ∘ args) = some v) (h : Fits w v) : ExecWithin w (Code.op (Op.alu f d args)) x (x.set d v) 1

theorem Cslib.WordRAM.ExecWithin.copy {B : Basis} {r w : ℕ} {x : Data r} {d s : Fin r} : ExecWithin w (Code.op (Op.copy d s)) x (x.set d (x.regs s)) 1

theorem Cslib.WordRAM.ExecWithin.load {B : Basis} {r w : ℕ} {x : Data r} {d a : Fin r} : ExecWithin w (Code.op (Op.load d a)) x (x.set d (x.mem (x.regs a))) 1

theorem Cslib.WordRAM.ExecWithin.store {B : Basis} {r w : ℕ} {x : Data r} {a s : Fin r} : ExecWithin w (Code.op (Op.store a s)) x (x.write (x.regs a) (x.regs s)) 1

theorem Cslib.WordRAM.ExecWithin.bin {r w : ℕ} {x : Data r} {d i j : Fin r} {f : BinOp} (h : Fits w (f.eval (x.regs i) (x.regs j))) : ExecWithin w (Code.op (Op.bin f d i j)) x (x.set d (f.eval (x.regs i) (x.regs j))) 1

theorem Cslib.WordRAM.ExecWithin.width {r w : ℕ} {x : Data r} {d : Fin r} : ExecWithin w (Code.op (Op.width d)) x (x.set d w) 1

Symbolic execution

def Cslib.WordRAM.Code.evalLoop {r : ℕ} (c : Cond r) (body : Data r → Option (Data r × ℕ)) : ℕ → Data r → Option (Data r × ℕ)

Run a loop with condition c and body semantics body, for at most fuel iterations.

def Cslib.WordRAM.Code.eval {B : Basis} {r : ℕ} (w fuel : ℕ) : Code B r → Data r → Option (Data r × ℕ)

Run a structured program at word size w, allowing each loop at most fuel iterations per entry: some (y, n) if it leads to y executing n instructions, and none if it faults or runs out of iterations. The definition is structurally recursive, so simp and decide evaluate it.

theorem Cslib.WordRAM.Exec.of_evalLoop {B : Basis} {r w : ℕ} {c : Cond r} {body : Code B r} {f : Data r → Option (Data r × ℕ)} (hf : ∀ {x y : Data r} {n : ℕ}, f x = some (y, n) → Exec w body x y n) {fuel : ℕ} {x y : Data r} {n : ℕ} (h : Code.evalLoop c f fuel x = some (y, n)) : Exec w (Code.loop c body) x y n

theorem Cslib.WordRAM.Exec.of_eval {B : Basis} {r w fuel : ℕ} {c : Code B r} {x y : Data r} {n : ℕ} (h : Code.eval w fuel c x = some (y, n)) : Exec w c x y n

The interpreter only finds executions.

theorem Cslib.WordRAM.ExecWithin.of_eval {B : Basis} {r w fuel : ℕ} {c : Code B r} {x y : Data r} {n T : ℕ} (h : Code.eval w fuel c x = some (y, n)) (hn : n ≤ T) : ExecWithin w c x y T

Registers a program does not write

def Cslib.WordRAM.Op.dest {B : Basis} {r : ℕ} : Op B r → Option (Fin r)

The register a data instruction writes, if any.

@[simp]

theorem Cslib.WordRAM.Op.dest_bin {r : ℕ} (f : BinOp) (d i j : Fin r) : (bin f d i j).dest = some d

@[simp]

theorem Cslib.WordRAM.Op.dest_width {r : ℕ} (d : Fin r) : (width d).dest = some d

def Cslib.WordRAM.Code.Preserves {B : Basis} {r : ℕ} (i : Fin r) : Code B r → Prop

No instruction of the program writes register i.

@[instance_reducible]

instance Cslib.WordRAM.Code.decidablePreserves {B : Basis} {r : ℕ} (i : Fin r) (c : Code B r) : Decidable (Preserves i c)

theorem Cslib.WordRAM.Op.regs_eq {B : Basis} {r w : ℕ} {o : Op B r} {x y : Data r} {i : Fin r} (hi : o.dest ≠ some i) (h : eval w o x = some y) : y.regs i = x.regs i

theorem Cslib.WordRAM.Exec.regs_eq {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {n : ℕ} {i : Fin r} (h : Exec w c x y n) (hi : Code.Preserves i c) : y.regs i = x.regs i

Register preservation. A register that no instruction of a program writes keeps its contents.

theorem Cslib.WordRAM.ExecWithin.regs_eq {B : Basis} {r w T : ℕ} {c : Code B r} {x y : Data r} {i : Fin r} (h : ExecWithin w c x y T) (hi : Code.Preserves i c) : y.regs i = x.regs i

Running a program on other registers

A program over r registers runs on r' registers through an injective choice f : Fin r → Fin r': register i of the program is register f i of the larger file. The other registers keep their contents, so a caller can keep its own state across the call.

def Cslib.WordRAM.Data.comap {r r' : ℕ} (f : Fin r → Fin r') (x : Data r') : Data r

The data seen through the registers chosen by f.

noncomputable def Cslib.WordRAM.Data.extend {r r' : ℕ} (f : Fin r → Fin r') (y : Data r) (x : Data r') : Data r'

Data y written back to the registers chosen by f, the other registers taken from x.

def Cslib.WordRAM.Op.rename {B : Basis} {r r' : ℕ} (f : Fin r → Fin r') : Op B r → Op B r'

Run the data instruction on the registers chosen by f.

@[simp]

theorem Cslib.WordRAM.Op.rename_bin {r r' : ℕ} (f : Fin r → Fin r') (g : BinOp) (d i j : Fin r) : rename f (bin g d i j) = bin g (f d) (f i) (f j)

@[simp]

theorem Cslib.WordRAM.Op.rename_width {r r' : ℕ} (f : Fin r → Fin r') (d : Fin r) : rename f (width d) = width (f d)

def Cslib.WordRAM.Cond.rename {r r' : ℕ} (f : Fin r → Fin r') : Cond r → Cond r'

Test the condition on the registers chosen by f.

def Cslib.WordRAM.Code.rename {B : Basis} {r r' : ℕ} (f : Fin r → Fin r') : Code B r → Code B r'

Run the structured program on the registers chosen by f.

@[simp]

theorem Cslib.WordRAM.Code.size_rename {B : Basis} {r r' : ℕ} (f : Fin r → Fin r') (c : Code B r) : (rename f c).size = c.size

@[simp]

theorem Cslib.WordRAM.Data.comap_regs {r r' : ℕ} {f : Fin r → Fin r'} (x : Data r') (i : Fin r) : (comap f x).regs i = x.regs (f i)

@[simp]

theorem Cslib.WordRAM.Data.comap_mem {r r' : ℕ} {f : Fin r → Fin r'} (x : Data r') : (comap f x).mem = x.mem

theorem Cslib.WordRAM.Data.comap_extend {r r' : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) (y : Data r) (x : Data r') : comap f (extend f y x) = y

theorem Cslib.WordRAM.Data.extend_extend {r r' : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) (y z : Data r) (x : Data r') : extend f z (extend f y x) = extend f z x

theorem Cslib.WordRAM.Data.extend_comap {r r' : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) (x : Data r') : extend f (comap f x) x = x

theorem Cslib.WordRAM.Data.extend_set {r r' : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) (y : Data r) (x : Data r') (i : Fin r) (v : ℕ) : extend f (y.set i v) x = (extend f y x).set (f i) v

theorem Cslib.WordRAM.Data.extend_write {r r' : ℕ} {f : Fin r → Fin r'} (y : Data r) (x : Data r') (a v : ℕ) : extend f (y.write a v) x = (extend f y x).write a v

theorem Cslib.WordRAM.Cond.holds_rename {r r' : ℕ} {f : Fin r → Fin r'} (c : Cond r) (x : Data r') : (rename f c).Holds x ↔ c.Holds (Data.comap f x)

theorem Cslib.WordRAM.Op.eval_rename {B : Basis} {r r' : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) (o : Op B r) (w : ℕ) (x : Data r') : eval w (rename f o) x = Option.map (fun (y : Data r) => Data.extend f y x) (eval w o (Data.comap f x))

theorem Cslib.WordRAM.Exec.rename {B : Basis} {r r' : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) {w : ℕ} {c : Code B r} {x : Data r'} {y : Data r} {n : ℕ} (h : Exec w c (Data.comap f x) y n) : Exec w (Code.rename f c) x (Data.extend f y x) n

Renaming. A program run on the registers chosen by an injective f does what it does on its own registers, with the same instruction count, and leaves the other registers unchanged.

theorem Cslib.WordRAM.ExecWithin.rename {B : Basis} {r r' : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) {w T : ℕ} {c : Code B r} {x : Data r'} {y : Data r} (h : ExecWithin w c (Data.comap f x) y T) : ExecWithin w (Code.rename f c) x (Data.extend f y x) T

Word sizes and word bounds

theorem Cslib.WordRAM.Exec.mono_width {B : Basis} {r w w' : ℕ} {c : Code B r} {x y : Data r} {n : ℕ} (hc : ¬c.ReadsWidth) (h : Exec w c x y n) (hw : w ≤ w') : Exec w' c x y n

Word-size monotonicity. A program that does not read the word size runs in the same way at every larger word size.

theorem Cslib.WordRAM.ExecWithin.mono_width {B : Basis} {r w w' T : ℕ} {c : Code B r} {x y : Data r} (hc : ¬c.ReadsWidth) (h : ExecWithin w c x y T) (hw : w ≤ w') : ExecWithin w' c x y T

theorem Cslib.WordRAM.Exec.bounded {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {n : ℕ} (h : Exec w c x y n) (hx : Data.Bounded w x) : Data.Bounded w y

Executions keep data word-sized.

theorem Cslib.WordRAM.ExecWithin.bounded {B : Basis} {r w T : ℕ} {c : Code B r} {x y : Data r} (h : ExecWithin w c x y T) (hx : Data.Bounded w x) : Data.Bounded w y