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, Cslib.WordRAM.Code.size, Cslib.WordRAM.Code.ReadsWidth, Cslib.WordRAM.Code.IsRandFree: structured programs over a basis, the length of the flat program they compile to, whether a program reads the word size, and whether it avoids Code.rand.
• Cslib.WordRAM.Exec, Cslib.WordRAM.ExecWithin: executions with an exact instruction count, and within a time bound.
• Cslib.WordRAM.Code.evalLoop, Cslib.WordRAM.Code.eval: an interpreter with a budget of loop iterations.
• Cslib.WordRAM.Op.dest, Cslib.WordRAM.Code.Preserves: written register of a data instruction and register preservation predicate.
• Cslib.WordRAM.Data.comap, Cslib.WordRAM.Data.extend, Cslib.WordRAM.Op.rename, Cslib.WordRAM.Cond.rename, 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.ExecWithin.loop_potential: the loop rule with an invariant and a potential that pays for iterations of different times.
• 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 and random-sampling 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.

• rand {B : Basis} {r : ℕ} (dst src : Fin r) : Code B r

  Sample uniformly from [0, regs src] into dst under randomized execution.

@[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

Decidability of whether a structured program reads the word size.

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

A structured program is rand-free if it contains no Code.rand node.

@[instance_reducible]

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

Decidability of whether a structured program is rand-free.

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

An exact execution of n instructions is also an execution within n instructions.

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

Setting register d to a fitting constant v takes one instruction.

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

An ALU operation whose result v fits in a word takes one instruction.

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

Copying register s into register d takes one instruction.

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

Loading the memory cell at register a into register d takes one instruction.

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

Storing register s into the memory cell at register a takes one instruction.

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

A standard binary operation whose result fits in a word takes one instruction.

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

Reading the word size w into register d takes one instruction.

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₂

Monotonicity of ExecWithin in the instruction budget.

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

A single data instruction executes within one instruction.

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₂)

Sequencing adds the instruction bounds of the two subprograms.

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)

Taking the positive branch of a conditional adds one instruction to the bound.

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)

Taking the negative branch of a conditional adds two instructions to the bound.

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

Exiting a loop when the condition fails takes at most two instructions.

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)

One loop iteration followed by the rest of the loop adds T₁ + 2 instructions to the bound.

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.

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

Loop rule, invariant and potential. If every state x satisfying the invariant I and the condition is led by the body to a state y satisfying I, within a number T of instructions with T + 2 + Φ y ≤ Φ x, then from a state satisfying I the loop terminates within Φ x + 2 instructions, in a state satisfying I where the condition fails. The two extra instructions of each iteration are the condition test and the jump back; the time of the body may differ between iterations, as long as the potential Φ pays for it.

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

Setting register d to a fitting constant v executes within one instruction.

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

An ALU operation whose result v fits in a word executes within one instruction.

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

Copying register s into register d executes within one instruction.

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

Loading the memory cell at register a into register d executes within one instruction.

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

Storing register s into the memory cell at register a executes within one instruction.

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

A standard binary operation whose result fits in a word executes within one instruction.

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

Reading the word size w into register d executes within one instruction.

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_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

If the bounded-fuel interpreter returns (y, n) with n ≤ T, then c executes within T instructions.

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

A binary operation writes its destination register d.

@[simp]

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

The word-size instruction writes its destination register 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)

Decidability of whether a structured program preserves register 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

Any register preserved by c retains its value across a bounded execution.

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)

Renaming a binary operation renames its destination and operand registers.

@[simp]

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

Renaming the word-size instruction renames its destination register.

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

Register renaming preserves the compiled program 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)

Reading register i of x.comap f reads register f i of x.

@[simp]

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

Data.comap leaves memory unchanged.

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.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)

A renamed condition holds on x if and only if the original condition holds on x.comap f.

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))

Evaluating a renamed instruction along an injective register map f commutes with comap and extend.

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

Bounded-time execution of a program renamed along an injective register map f.

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

A program that does not read the word size executes within the same bound at any larger word size.

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

Bounded-time executions preserve word-sized data.