Symbolic execution of structured word-RAM code

Cslib.WordRAM.WP w c x Q states that the structured program c leads from x to some data y within some number T of instructions such that Q y T. It is the weakest-precondition form of Cslib.WordRAM.ExecWithin: its rules run backwards through a program, one instruction at a time, and hand the rest of the program the data in closed form. A goal ∃ y, ExecWithin w c x y T ∧ P y is the special case WP w c x fun y t => t ≤ T ∧ P y (Cslib.WordRAM.WP.exists_execWithin). Cslib.WordRAM.WP.Exact is the same form of Cslib.WordRAM.Exec, for specifications that state the exact instruction count: ∃ y, Exec w c x y T ∧ P y is WP.Exact w c x fun y t => t = T ∧ P y, and its rules have the same names and premises.

The tactic wram_exec applies these rules along the syntax of the program. It is meant for the straight-line glue of correctness proofs, between loops and calls of subprograms with their own specifications: it executes data instructions and conditionals, and stops at a loop, at a random sample and at a program given by name, leaving the goal WP w c y Q with the data y reached. Cslib.WordRAM.WP.of_execWithin then continues from a specification of c, and wram_exec resumes on the remaining program; on a WP.Exact goal, Cslib.WordRAM.WP.Exact.of_exec continues from an exact specification. At a loop whose condition holds, Cslib.WordRAM.WP.loop_iter continues into its body, leaving at its end the loop again from the data reached, where an induction hypothesis applies; Cslib.WordRAM.WP.Exact.loop_iter is the same rule for exact counts.

The registers and memory cells an instruction reads are simplified as it executes, with the simp set wram_simps. Reads after Cslib.WordRAM.Data.set and Cslib.WordRAM.Data.write reduce by the simplification procedures Cslib.WordRAM.Data.reduceRegs and Cslib.WordRAM.Data.reduceMem. The first compares register names by evaluation when they are literals, and otherwise by hypotheses j ≠ i, j ∉ Set.range f, Function.Injective f and instances of ∀ xs, a ≠ b, such as ∀ i j, src i ≠ tmp j for two renamed banks, or by the discharger on their values, as for Fin.castAdd and names ⟨k + 9, _⟩; the second asks the discharger whether two addresses are equal. Memory that is not read at an address, such as an argument of a definition, becomes Function.update (Cslib.WordRAM.Data.reduceWriteMem). The given simp lemmas rewrite the values, so facts such as x.regs zeroP = 0 replace the registers of the initial data. A conditional takes the branch its simplified condition decides, by simp or by the discharger, and otherwise splits into both alternatives with the hypothesis hc; wram_exec -split stops there instead, so that Cslib.WordRAM.WP.cut can join the alternatives before the rest of the program. Side conditions of instructions (Fits w v, a subtrahend at most its minuend, a nonzero divisor) are proved by simp or the discharger; the others remain as goals, after the main goals, tagged hfit, hle or hb.

Every side condition goes through the same steps (Cslib.WordRAM.WP.Exec.discharge): a proposition without free variables, such as a comparison of register names, is decided by evaluation and is never passed on when it is false; a hypothesis of the same statement proves it; only then does the discharger run. By default it is fits on a word-size bound, which uses the Fits facts in context, and omega on anything else. The search for a hypothesis compares statements syntactically, because unifying arithmetic with every hypothesis of a long proof costs more than the discharger.

wram_simp simplifies the reads in the postcondition left at the end, and wram_bounded proves that the data reached is word-sized; Cslib.WordRAM.WP.bounded assumes this instead at the end of a program.

Main definitions

• Cslib.WordRAM.WP: the weakest-precondition form of ExecWithin.
• Cslib.WordRAM.WP.Exact: the weakest-precondition form of Exec, with exact counts.
• wram_exec: symbolic execution of the straight-line parts of structured code.
• wram_simp: reads of registers and memory after writes, with the simp set of wram_exec.
• wram_bounded: word-sizedness of data built by writes.
• Cslib.WordRAM.Data.reduceRegs, Cslib.WordRAM.Data.reduceMem, Cslib.WordRAM.Data.reduceWriteMem: simplification procedures reading registers and memory after writes; Cslib.WordRAM.Basis.reduceInterp, evaluating an operation of a basis.

Main results

• Cslib.WordRAM.WP.exists_execWithin, Cslib.WordRAM.WP.execWithin: back to ExecWithin.
• Cslib.WordRAM.WP.seq, Cslib.WordRAM.WP.branch_lt, Cslib.WordRAM.WP.branch_eq, Cslib.WordRAM.WP.copy, Cslib.WordRAM.WP.load, Cslib.WordRAM.WP.store, …: the rules for each construct, with the values read given in closed form.
• Cslib.WordRAM.WP.cut: an intermediate assertion, to join the alternatives of a conditional before the rest of a program.
• Cslib.WordRAM.WP.bounded: the data reached from word-sized data is word-sized.
• Cslib.WordRAM.WP.name: a name for the data reached, at a stop.
• Cslib.WordRAM.WP.loop_iter, Cslib.WordRAM.WP.Exact.loop_iter: an iteration of a loop whose condition holds, to continue into its body at a stop.
• Cslib.WordRAM.WP.Exact.exists_exec, Cslib.WordRAM.WP.Exact.exec: back to Exec; the rules Cslib.WordRAM.WP.Exact.seq, Cslib.WordRAM.WP.Exact.const, … are those of WP, and Cslib.WordRAM.WP.Exact.toWP weakens an exact count to a bound.

Reading registers and memory after writes

theorem Cslib.WordRAM.Data.set_regs_self {r : ℕ} (x : Data r) (i : Fin r) (v : ℕ) : (x.set i v).regs i = v

Reading the register just set.

theorem Cslib.WordRAM.Data.set_regs_of_ne {r : ℕ} {x : Data r} {i j : Fin r} (h : j ≠ i) (v : ℕ) : (x.set i v).regs j = x.regs j

Reading another register than the one set.

theorem Cslib.WordRAM.Data.set_regs_of_eq {r : ℕ} {x : Data r} {i j : Fin r} (h : j = i) (v : ℕ) : (x.set i v).regs j = v

Reading the register just set, under a name equal to it.

theorem Cslib.WordRAM.Data.write_regs_apply {r : ℕ} (x : Data r) (a v : ℕ) (j : Fin r) : (x.write a v).regs j = x.regs j

Reading a register after a write to memory.

theorem Cslib.WordRAM.Data.set_mem_apply {r : ℕ} (x : Data r) (i : Fin r) (v b : ℕ) : (x.set i v).mem b = x.mem b

Reading memory after setting a register.

theorem Cslib.WordRAM.Data.write_mem_self {r : ℕ} (x : Data r) (a v : ℕ) : (x.write a v).mem a = v

Reading the memory cell just written.

theorem Cslib.WordRAM.Data.write_mem_of_eq {r : ℕ} {x : Data r} {a b : ℕ} (h : b = a) (v : ℕ) : (x.write a v).mem b = v

Reading the memory cell just written, at an address equal to it.

theorem Cslib.WordRAM.Data.write_mem_of_ne {r : ℕ} {x : Data r} {a b : ℕ} (h : b ≠ a) (v : ℕ) : (x.write a v).mem b = x.mem b

Reading another memory cell than the one written.

Weakest preconditions

def Cslib.WordRAM.WP {B : Basis} {r : ℕ} (w : ℕ) (c : Code B r) (x : Data r) (Q : Data r → ℕ → Prop) : Prop

WP w c x Q: at word size w, the structured program c leads from data x to some data y within some number T of instructions such that Q y T.

theorem Cslib.WordRAM.WP.of_execWithin {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {T : ℕ} {Q : Data r → ℕ → Prop} (h : ExecWithin w c x y T) (hQ : Q y T) : WP w c x Q

Continue from an execution of c within T instructions.

theorem Cslib.WordRAM.WP.mono {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {Q Q' : Data r → ℕ → Prop} (h : WP w c x Q) (hQ : ∀ (y : Data r) (T : ℕ), Q y T → Q' y T) : WP w c x Q'

Weaken the postcondition.

theorem Cslib.WordRAM.WP.name {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} (h : ∀ (y : Data r), y = x → WP w c y Q) : WP w c x Q

Name the data reached: continue from a variable y with the equation y = x, for instance to state the hypotheses of a specification of a subprogram.

theorem Cslib.WordRAM.WP.bounded {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} (hx : Data.Bounded w x) (h : WP w c x fun (y : Data r) (T : ℕ) => Data.Bounded w y → Q y T) : WP w c x Q

Executions from word-sized data reach word-sized data, so the postcondition may assume it.

theorem Cslib.WordRAM.WP.exists_execWithin {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {T : ℕ} {P : Data r → Prop} (h : WP w c x fun (y : Data r) (t : ℕ) => t ≤ T ∧ P y) : ∃ (y : Data r), ExecWithin w c x y T ∧ P y

A run within a bound T reaching data with property P.

theorem Cslib.WordRAM.WP.execWithin {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {T : ℕ} (h : WP w c x fun (y' : Data r) (t : ℕ) => t ≤ T ∧ y' = y) : ExecWithin w c x y T

A run within a bound T reaching the given data y.

theorem Cslib.WordRAM.WP.seq {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} (h : WP w c₁ x fun (y : Data r) (T₁ : ℕ) => WP w c₂ y fun (z : Data r) (T₂ : ℕ) => Q z (T₂ + T₁)) : WP w (c₁.seq c₂) x Q

Run c₁, then c₂ from the data it reaches, adding the instruction counts. The count of c₁ is added last, so that the counts of a sequence accumulate as (T + 1) + 1, with the numerals on the right, rather than 1 + (1 + T): deciding whether such a sum is a given variable takes time exponential in its length.

theorem Cslib.WordRAM.WP.cut {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} (R : Data r → ℕ → Prop) (h : WP w c x R) (hR : ∀ (y : Data r) (T : ℕ), R y T → Q y T) : WP w c x Q

Run c to data satisfying an intermediate assertion R, and continue from any such data: the join point of the alternatives of a conditional before the rest of a program.

theorem Cslib.WordRAM.WP.branch {B : Basis} {r w : ℕ} {pos neg : Code B r} {cond : Cond r} {x : Data r} {Q : Data r → ℕ → Prop} (hpos : cond.Holds x → WP w pos x fun (y : Data r) (T : ℕ) => Q y (T + 1)) (hneg : ¬cond.Holds x → WP w neg x fun (y : Data r) (T : ℕ) => Q y (T + 2)) : WP w (Code.branch cond pos neg) x Q

A conditional, by cases on its condition.

theorem Cslib.WordRAM.WP.branch_lt {B : Basis} {r w : ℕ} {pos neg : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} {i j : Fin r} {a b : ℕ} (hi : x.regs i = a) (hj : x.regs j = b) (hpos : a < b → WP w pos x fun (y : Data r) (T : ℕ) => Q y (T + 1)) (hneg : ¬a < b → WP w neg x fun (y : Data r) (T : ℕ) => Q y (T + 2)) : WP w (Code.branch (Cond.lt i j) pos neg) x Q

A conditional on x.regs i < x.regs j, with the compared values in closed form.

theorem Cslib.WordRAM.WP.branch_eq {B : Basis} {r w : ℕ} {pos neg : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} {i j : Fin r} {a b : ℕ} (hi : x.regs i = a) (hj : x.regs j = b) (hpos : a = b → WP w pos x fun (y : Data r) (T : ℕ) => Q y (T + 1)) (hneg : ¬a = b → WP w neg x fun (y : Data r) (T : ℕ) => Q y (T + 2)) : WP w (Code.branch (Cond.eq i j) pos neg) x Q

A conditional on x.regs i = x.regs j, with the compared values in closed form.

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

An iteration of a loop whose condition holds: run the body, then the loop again from the data it reaches. The test and the jump back count two instructions, as in ExecWithin.loop_iter; the count of the body is added last, as in WP.seq.

Data instructions

Each rule names the values the instruction reads (hi, hj, hs, ha) and computes (hv), so that the continuation h receives them in closed form.

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

Setting register d to a fitting constant v.

theorem Cslib.WordRAM.WP.copy {B : Basis} {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d s : Fin r} {v : ℕ} (hs : x.regs s = v) (h : Q (x.set d v) 1) : WP w (Code.op (Op.copy d s)) x Q

Copying register s, which holds v, into register d.

theorem Cslib.WordRAM.WP.load {B : Basis} {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d a : Fin r} {u v : ℕ} (ha : x.regs a = u) (hv : x.mem u = v) (h : Q (x.set d v) 1) : WP w (Code.op (Op.load d a)) x Q

Loading the memory cell at address u, held by register a, into register d.

theorem Cslib.WordRAM.WP.store {B : Basis} {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {s a : Fin r} {u v : ℕ} (ha : x.regs a = u) (hs : x.regs s = v) (h : Q (x.write u v) 1) : WP w (Code.op (Op.store a s)) x Q

Storing register s, which holds v, at address u, held by register a.

theorem Cslib.WordRAM.WP.bin {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d i j : Fin r} {u v b' : ℕ} {f : BinOp} (hi : x.regs i = u) (hj : x.regs j = b') (hv : f.eval u b' = v) (hfit : Fits w v) (h : Q (x.set d v) 1) : WP w (Code.op (Op.bin f d i j)) x Q

A standard binary operation on registers holding u and b', with fitting value v.

theorem Cslib.WordRAM.WP.width {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d : Fin r} (h : Q (x.set d w) 1) : WP w (Code.op (Op.width d)) x Q

Reading the word size into register d.

theorem Cslib.WordRAM.WP.exactBin {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d i j : Fin r} {u v b' : ℕ} {f : BinOp} (hi : x.regs i = u) (hj : x.regs j = b') (hv : f.evalExact u b' = some v) (hfit : Fits w v) (h : Q (x.set d v) 1) : WP w (Code.op (Op.exactBin f d i j)) x Q

An exact binary operation on registers holding u and b', defined with fitting value v.

theorem Cslib.WordRAM.WP.exactSub {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d i j : Fin r} {u v b' : ℕ} (hi : x.regs i = u) (hj : x.regs j = b') (hle : b' ≤ u) (hv : u - b' = v) (hfit : Fits w v) (h : Q (x.set d v) 1) : WP w (Code.op (Op.exactBin BinOp.sub d i j)) x Q

An exact subtraction u - b', defined since b' ≤ u.

theorem Cslib.WordRAM.WP.exactDiv {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d i j : Fin r} {u v b' : ℕ} (hi : x.regs i = u) (hj : x.regs j = b') (hb : b' ≠ 0) (hv : u / b' = v) (hfit : Fits w v) (h : Q (x.set d v) 1) : WP w (Code.op (Op.exactBin BinOp.div d i j)) x Q

An exact division u / b', defined since b' ≠ 0.

theorem Cslib.WordRAM.WP.exactMod {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d i j : Fin r} {u v b' : ℕ} (hi : x.regs i = u) (hj : x.regs j = b') (hb : b' ≠ 0) (hv : u % b' = v) (hfit : Fits w v) (h : Q (x.set d v) 1) : WP w (Code.op (Op.exactBin BinOp.mod d i j)) x Q

An exact remainder u % b', defined since b' ≠ 0.

theorem Cslib.WordRAM.WP.exactWidth {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d : Fin r} (h : Q (x.set d w) 1) : WP w (Code.op (Op.exactWidth d)) x Q

Reading the word size into register d, over the exact basis.

theorem Cslib.WordRAM.WP.alu {B : Basis} {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d : Fin r} {v : ℕ} {f : B.Op} {args : Fin (B.Arity f) → Fin r} (hv : (B.interp w f fun (a : Fin (B.Arity f)) => x.regs (args a)) = some v) (hfit : Fits w v) (h : Q (x.set d v) 1) : WP w (Code.op (Op.alu f d args)) x Q

An operation f of any basis on the registers args, with fitting value v, as over Basis.additive; hv evaluates f on the values of the registers.

Exact instruction counts

def Cslib.WordRAM.WP.Exact {B : Basis} {r : ℕ} (w : ℕ) (c : Code B r) (x : Data r) (Q : Data r → ℕ → Prop) : Prop

WP.Exact w c x Q: at word size w, the structured program c leads from data x to some data y in exactly some number T of instructions such that Q y T. It is the weakest-precondition form of Cslib.WordRAM.Exec, with the same rules as Cslib.WordRAM.WP; a goal ∃ y, Exec w c x y T ∧ P y is the special case WP.Exact w c x fun y t => t = T ∧ P y.

theorem Cslib.WordRAM.WP.Exact.of_exec {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {T : ℕ} {Q : Data r → ℕ → Prop} (h : Exec w c x y T) (hQ : Q y T) : Exact w c x Q

Continue from an execution of c in exactly T instructions.

theorem Cslib.WordRAM.WP.Exact.mono {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {Q Q' : Data r → ℕ → Prop} (h : Exact w c x Q) (hQ : ∀ (y : Data r) (T : ℕ), Q y T → Q' y T) : Exact w c x Q'

Weaken the postcondition.

theorem Cslib.WordRAM.WP.Exact.toWP {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} (h : Exact w c x Q) : WP w c x Q

An exact count is in particular a bound.

theorem Cslib.WordRAM.WP.Exact.name {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} (h : ∀ (y : Data r), y = x → Exact w c y Q) : Exact w c x Q

Name the data reached: continue from a variable y with the equation y = x.

theorem Cslib.WordRAM.WP.Exact.bounded {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} (hx : Data.Bounded w x) (h : Exact w c x fun (y : Data r) (T : ℕ) => Data.Bounded w y → Q y T) : Exact w c x Q

Executions from word-sized data reach word-sized data, so the postcondition may assume it.

theorem Cslib.WordRAM.WP.Exact.exists_exec {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {T : ℕ} {P : Data r → Prop} (h : Exact w c x fun (y : Data r) (t : ℕ) => t = T ∧ P y) : ∃ (y : Data r), Exec w c x y T ∧ P y

A run in exactly T instructions reaching data with property P.

theorem Cslib.WordRAM.WP.Exact.exec {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {T : ℕ} (h : Exact w c x fun (y' : Data r) (t : ℕ) => t = T ∧ y' = y) : Exec w c x y T

A run in exactly T instructions reaching the given data y.

theorem Cslib.WordRAM.WP.Exact.seq {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} (h : Exact w c₁ x fun (y : Data r) (T₁ : ℕ) => Exact w c₂ y fun (z : Data r) (T₂ : ℕ) => Q z (T₂ + T₁)) : Exact w (c₁.seq c₂) x Q

Run c₁, then c₂ from the data it reaches, adding the instruction counts, the count of c₁ last, as in WP.seq.

theorem Cslib.WordRAM.WP.Exact.cut {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} (R : Data r → ℕ → Prop) (h : Exact w c x R) (hR : ∀ (y : Data r) (T : ℕ), R y T → Q y T) : Exact w c x Q

Run c to data satisfying an intermediate assertion R, and continue from any such data.

theorem Cslib.WordRAM.WP.Exact.branch {B : Basis} {r w : ℕ} {pos neg : Code B r} {cond : Cond r} {x : Data r} {Q : Data r → ℕ → Prop} (hpos : cond.Holds x → Exact w pos x fun (y : Data r) (T : ℕ) => Q y (T + 1)) (hneg : ¬cond.Holds x → Exact w neg x fun (y : Data r) (T : ℕ) => Q y (T + 2)) : Exact w (Code.branch cond pos neg) x Q

A conditional, by cases on its condition.

theorem Cslib.WordRAM.WP.Exact.branch_lt {B : Basis} {r w : ℕ} {pos neg : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} {i j : Fin r} {a b : ℕ} (hi : x.regs i = a) (hj : x.regs j = b) (hpos : a < b → Exact w pos x fun (y : Data r) (T : ℕ) => Q y (T + 1)) (hneg : ¬a < b → Exact w neg x fun (y : Data r) (T : ℕ) => Q y (T + 2)) : Exact w (Code.branch (Cond.lt i j) pos neg) x Q

A conditional on x.regs i < x.regs j, with the compared values in closed form.

theorem Cslib.WordRAM.WP.Exact.branch_eq {B : Basis} {r w : ℕ} {pos neg : Code B r} {x : Data r} {Q : Data r → ℕ → Prop} {i j : Fin r} {a b : ℕ} (hi : x.regs i = a) (hj : x.regs j = b) (hpos : a = b → Exact w pos x fun (y : Data r) (T : ℕ) => Q y (T + 1)) (hneg : ¬a = b → Exact w neg x fun (y : Data r) (T : ℕ) => Q y (T + 2)) : Exact w (Code.branch (Cond.eq i j) pos neg) x Q

A conditional on x.regs i = x.regs j, with the compared values in closed form.

theorem Cslib.WordRAM.WP.Exact.loop_iter {B : Basis} {r w : ℕ} {cond : Cond r} {x : Data r} {Q : Data r → ℕ → Prop} {body : Code B r} (hc : cond.Holds x) (h : Exact w body x fun (y : Data r) (T₁ : ℕ) => Exact w (Code.loop cond body) y fun (z : Data r) (T₂ : ℕ) => Q z (T₂ + T₁ + 2)) : Exact w (Code.loop cond body) x Q

An iteration of a loop whose condition holds: run the body, then the loop again from the data it reaches, adding the two counts and the two instructions of the test and the jump back.

theorem Cslib.WordRAM.WP.Exact.const {B : Basis} {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d : Fin r} {v : ℕ} (hfit : Fits w v) (h : Q (x.set d v) 1) : Exact w (Code.op (Op.const d v)) x Q

Setting register d to a fitting constant v.

theorem Cslib.WordRAM.WP.Exact.copy {B : Basis} {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d s : Fin r} {v : ℕ} (hs : x.regs s = v) (h : Q (x.set d v) 1) : Exact w (Code.op (Op.copy d s)) x Q

Copying register s, which holds v, into register d.

theorem Cslib.WordRAM.WP.Exact.load {B : Basis} {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d a : Fin r} {u v : ℕ} (ha : x.regs a = u) (hv : x.mem u = v) (h : Q (x.set d v) 1) : Exact w (Code.op (Op.load d a)) x Q

Loading the memory cell at address u, held by register a, into register d.

theorem Cslib.WordRAM.WP.Exact.store {B : Basis} {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {s a : Fin r} {u v : ℕ} (ha : x.regs a = u) (hs : x.regs s = v) (h : Q (x.write u v) 1) : Exact w (Code.op (Op.store a s)) x Q

Storing register s, which holds v, at address u, held by register a.

theorem Cslib.WordRAM.WP.Exact.bin {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d i j : Fin r} {u v b' : ℕ} {f : BinOp} (hi : x.regs i = u) (hj : x.regs j = b') (hv : f.eval u b' = v) (hfit : Fits w v) (h : Q (x.set d v) 1) : Exact w (Code.op (Op.bin f d i j)) x Q

A standard binary operation on registers holding u and b', with fitting value v.

theorem Cslib.WordRAM.WP.Exact.width {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d : Fin r} (h : Q (x.set d w) 1) : Exact w (Code.op (Op.width d)) x Q

Reading the word size into register d.

theorem Cslib.WordRAM.WP.Exact.exactBin {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d i j : Fin r} {u v b' : ℕ} {f : BinOp} (hi : x.regs i = u) (hj : x.regs j = b') (hv : f.evalExact u b' = some v) (hfit : Fits w v) (h : Q (x.set d v) 1) : Exact w (Code.op (Op.exactBin f d i j)) x Q

An exact binary operation on registers holding u and b', defined with fitting value v.

theorem Cslib.WordRAM.WP.Exact.exactSub {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d i j : Fin r} {u v b' : ℕ} (hi : x.regs i = u) (hj : x.regs j = b') (hle : b' ≤ u) (hv : u - b' = v) (hfit : Fits w v) (h : Q (x.set d v) 1) : Exact w (Code.op (Op.exactBin BinOp.sub d i j)) x Q

An exact subtraction u - b', defined since b' ≤ u.

theorem Cslib.WordRAM.WP.Exact.exactDiv {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d i j : Fin r} {u v b' : ℕ} (hi : x.regs i = u) (hj : x.regs j = b') (hb : b' ≠ 0) (hv : u / b' = v) (hfit : Fits w v) (h : Q (x.set d v) 1) : Exact w (Code.op (Op.exactBin BinOp.div d i j)) x Q

An exact division u / b', defined since b' ≠ 0.

theorem Cslib.WordRAM.WP.Exact.exactMod {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d i j : Fin r} {u v b' : ℕ} (hi : x.regs i = u) (hj : x.regs j = b') (hb : b' ≠ 0) (hv : u % b' = v) (hfit : Fits w v) (h : Q (x.set d v) 1) : Exact w (Code.op (Op.exactBin BinOp.mod d i j)) x Q

An exact remainder u % b', defined since b' ≠ 0.

theorem Cslib.WordRAM.WP.Exact.exactWidth {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d : Fin r} (h : Q (x.set d w) 1) : Exact w (Code.op (Op.exactWidth d)) x Q

Reading the word size into register d, over the exact basis.

theorem Cslib.WordRAM.WP.Exact.alu {B : Basis} {r w : ℕ} {x : Data r} {Q : Data r → ℕ → Prop} {d : Fin r} {v : ℕ} {f : B.Op} {args : Fin (B.Arity f) → Fin r} (hv : (B.interp w f fun (a : Fin (B.Arity f)) => x.regs (args a)) = some v) (hfit : Fits w v) (h : Q (x.set d v) 1) : Exact w (Code.op (Op.alu f d args)) x Q

An operation f of any basis on the registers args, with fitting value v, as over Basis.additive; hv evaluates f on the values of the registers.

The tactic

Reads and side conditions

def Cslib.WordRAM.WP.Exec.regValue? (r i : Lean.Expr) : Lean.MetaM (Option ℕ)

The value of the register name i : Fin r when it has no free variables and evaluates to a literal, as (3 : Fin 4) and abbreviations for ⟨3, _⟩ do.

def Cslib.WordRAM.WP.Exec.decideClosed? (p : Lean.Expr) : Lean.MetaM (Option (Option Lean.Expr))

A proof of the proposition p, which has no free variables, by evaluating its Decidable instance: some (some h) if it evaluates to true, some none if it evaluates to false, and none if p has free variables or metavariables, has no instance, or does not evaluate.

def Cslib.WordRAM.WP.Exec.assumption? (p : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

A hypothesis of type p, compared syntactically, so that the search costs no unification.

def Cslib.WordRAM.WP.Exec.discharge (tac : Lean.Meta.Simp.Discharge) (p : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Expr)

The discharger of wram_exec and wram_simp. A proposition without free variables, such as a comparison of register names, is decided by evaluation and is not passed on if it is false; otherwise a hypothesis of the same type proves it, or else the discharger tac of the call.

def Cslib.WordRAM.WP.Exec.reduceRegsStep (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Read a register after Data.set and Data.write, one layer at a time. Register names that evaluate to literals are compared by evaluation; others are equal when they are the same term or unfold to constructors with the same value, and different by regNe?.

def Cslib.WordRAM.WP.Exec.reduceMemStep (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Read memory after Data.set and Data.write, one layer at a time. Two addresses are equal when they are the same term; otherwise the discharger decides them, first unequal, then equal. A read after a write it cannot decide is final, so that reduceWriteMemStep leaves it alone.

def Cslib.WordRAM.WP.Exec.closesWith (tac : Lean.TSyntax `tactic) (g : Lean.MVarId) : Lean.Elab.Tactic.TacticM Bool

Close the goal g with the tactic tac, or restore the state and report failure.

def Cslib.WordRAM.Data.reduceRegs : Lean.Meta.Simp.Simproc

simp procedure reading a register after Data.set and Data.write. Register names that evaluate to literals are compared by evaluation; others by hypotheses j ≠ i, j ∉ Set.range f, Function.Injective f and instances of ∀ xs, a ≠ b, or by the discharger on their values. It is a pre-procedure (↓), so that the data is not simplified first.

def Cslib.WordRAM.Data.reduceMem : Lean.Meta.Simp.Simproc

simp procedure reading memory after Data.set and Data.write, deciding whether two addresses are equal with the discharger.

def Cslib.WordRAM.Data.reduceWriteMem : Lean.Meta.Simp.Simproc

simp procedure rewriting the memory after Data.write, when it is not read at an address, to Function.update (Data.write_mem), for instance as the argument of a definition.

def Cslib.WordRAM.Basis.reduceInterp : Lean.Meta.Simp.DSimproc

simp procedure evaluating an operation B.interp w f vals of a basis given by a definition, such as Basis.additive, when it unfolds to a value some v (WP.alu). It is a pre-procedure (↓), so that it sees the basis before simplification unfolds it.

partial def Cslib.WordRAM.WP.Exec.headBetaAll (e : Lean.Expr) : Lean.Expr

Beta-reduce the head of e until it is no longer a λ-abstraction applied to arguments.

structure Cslib.WordRAM.WP.Exec.Config : Type

The simplification context of one wram_exec call, the discharger for side conditions, and the goals the call leaves for them.

• ctx : Lean.Meta.Simp.Context

  The simp context.

• simprocs : Lean.Meta.Simp.SimprocsArray

  The simprocs.

• simpDischarge : Lean.Meta.Simp.Discharge

  The discharger of conditional simp lemmas.

• disch : Lean.TSyntax `tactic

  The discharger of side conditions and branch conditions.

• sideGoals : IO.Ref (Array Lean.MVarId)

  The side conditions left as goals.

• steps : IO.Ref ℕ

  The number of rules applied.

• split : Bool

  Whether to split a conditional that is not decided, rather than stop at it.

def Cslib.WordRAM.WP.Exec.simpExpr (cfg : Config) (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Simplify e with the simp set of the call.

def Cslib.WordRAM.WP.Exec.tryProve (cfg : Config) (prove : Lean.MVarId → Lean.Elab.Tactic.TacticM Bool) (p : Lean.Expr) : Lean.Elab.Tactic.TacticM (Option Lean.Expr × Lean.Meta.Simp.Result)

Prove the proposition p by simplification to True, by evaluation if it has no free variables, by a hypothesis of its type, or by prove. Returns the proof, or the simplification of p.

def Cslib.WordRAM.WP.Exec.applyRule (cfg : Config) (g : Lean.MVarId) (rule : Lean.Name) : Lean.MetaM (Array (Lean.Name × Lean.Expr))

Apply rule to the goal g, returning its arguments with the names of their binders.

def Cslib.WordRAM.WP.Exec.evalPremise (cfg : Config) (arg lhs rhs : Lean.Expr) : Lean.MetaM Unit

Evaluate the premise arg : lhs = rhs by simplifying lhs and unifying the result with rhs, which determines the values it names.

def Cslib.WordRAM.WP.Exec.sidePremise (cfg : Config) (tag : Lean.Name) (arg : Lean.Expr) : Lean.Elab.Tactic.TacticM Unit

Prove the side condition arg, or leave its simplification as a goal tagged tag.

def Cslib.WordRAM.WP.Exec.premiseGoal (arg : Lean.Expr) (tag : Lean.Name) : Lean.MetaM Lean.MVarId

A fresh goal, with the given tag, for the premise arg, whose statement is beta-reduced.

def Cslib.WordRAM.WP.Exec.opRule? (o : Lean.Expr) : Option Lean.Name

The rule executing the data instruction o, if there is one.

partial def Cslib.WordRAM.WP.Exec.walk (cfg : Config) (g : Lean.MVarId) : Lean.Elab.Tactic.TacticM (Array Lean.MVarId)

Execute the program of the goal g : WP w c x Q, or g : WP.Exact w c x Q, instruction by instruction, and return the goals where execution stops: Q y T at the end of the program, and WP w c' y Q' (respectively WP.Exact w c' y Q') at a loop, a random sample or a program given by name.

partial def Cslib.WordRAM.WP.Exec.step (cfg : Config) (g : Lean.MVarId) (rule : Lean.Name) : Lean.Elab.Tactic.TacticM (Array Lean.MVarId)

Apply the rule rule to g: evaluate the values it reads, prove or leave its side conditions, and continue with its continuation h.

partial def Cslib.WordRAM.WP.Exec.branch (cfg : Config) (g : Lean.MVarId) (rule : Lean.Name) : Lean.Elab.Tactic.TacticM (Array Lean.MVarId)

Apply the conditional rule rule to g: evaluate the compared values, take the branch that simp or the discharger decides, and otherwise continue in both with the hypothesis hc, or stop at the conditional if cfg.split is false.

def Cslib.WordRAM.WP.Exec.toWP (g : Lean.MVarId) : Lean.MetaM (Lean.MVarId × Bool × Bool)

Turn a goal ∃ y, ExecWithin w c x y T ∧ P y, ExecWithin w c x y T or ∃ y T, ExecWithin w c x y T ∧ Q y T into a WP goal, and the same goals with Exec into a WP.Exact goal. Returns the new goal, whether its postcondition states the data reached, t ≤ T ∧ y' = y (respectively t = T ∧ y' = y), and whether it counts instructions exactly.

def Cslib.WordRAM.WP.Exec.closeBound (cfg : Config) (eq exact : Bool) (g : Lean.MVarId) : Lean.Elab.Tactic.TacticM (Option Lean.MVarId)

At the end of a program, prove a leading instruction bound t ≤ T of the postcondition, or an instruction count t = T if exact, by omega, and leave the rest, unless eq and it is an equation between data closed by reducible rfl.

def Cslib.WordRAM.WP.Exec.boundedHyps (w : Lean.Expr) : Lean.MetaM (Array (Lean.Expr × Lean.Expr))

The hypotheses x.Bounded w, with the data x of each.

def Cslib.WordRAM.WP.Exec.fitsOfBounded? (w v : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Prove Fits w v from a hypothesis x.Bounded w when v is a register or memory cell of x: syntactically, or else up to unfolding, as for a field of a state read from x.

partial def Cslib.WordRAM.WP.Exec.boundedGoals (g : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

The goals wram_bounded leaves from the goal g. Word-sizedness of data built by Data.set and Data.write reduces to that of the data written to, and to the fitting conditions of the values written; a goal that is a hypothesis is closed by it, and a value read from data with a hypothesis x.Bounded w fits by that hypothesis.

def Cslib.WordRAM.WP.Exec.simpCall (disch : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (args : Array Lean.Syntax) : Lean.MacroM (Lean.TSyntax `tactic)

The simp call of wram_exec and wram_simp: the simp set wram_simps, the simplification procedures of arithmetic on numerals, and the given lemmas args, with the side conditions of lemmas proved by disch.

def Cslib.WordRAM.WP.Exec.withSimpContext {α : Type} (disch : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (args : Array Lean.Syntax) (k : Lean.Meta.Simp.Context → Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.Discharge → Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

Run k with the simp context of a wram_exec or wram_simp call, whose discharger is WP.Exec.discharge around the tactic disch.

def Cslib.WordRAM.wramExec : Lean.ParserDescr

wram_exec symbolically executes structured word-RAM code (Cslib.WordRAM.Code) on a goal ∃ y, ExecWithin w c x y T ∧ P y, ExecWithin w c x y T or Cslib.WordRAM.WP w c x Q. It runs the data instructions and conditionals of c in order, with the data in closed form, until the end of the program, where t ≤ T ∧ P y (respectively t ≤ T ∧ y' = y, or Q y t) remains for the data y and instruction count t reached; a leading bound t ≤ T is closed by omega when it can. It stops at a loop, a random sample or a program given by name, leaving WP w c' y Q': continue with refine WP.of_execWithin h ?_ from a specification h of c', then wram_exec again. Unfold programs given by name to execute them instead.

On the exact-count goals ∃ y, Exec w c x y T ∧ P y, Exec w c x y T and Cslib.WordRAM.WP.Exact w c x Q it works the same way with the rules of WP.Exact: the count t = T is closed by omega when it can, and refine WP.Exact.of_exec h ?_ continues from an exact specification h at a stop.

• wram_exec [h₁, h₂] adds simp lemmas for the values read, typically the contents of the registers of x, such as x.regs zeroP = 0, and the memory cells it reads.
• wram_exec (disch := tac) sets the discharger, by default fits on a word-size bound and omega on anything else. It proves side conditions (Fits w v, b ≤ a for an exact subtraction, a nonzero divisor), decides conditions of branches, and decides whether two memory addresses are equal. Register names, and side conditions without free variables, are decided by evaluation, and a side condition that is a hypothesis is proved by it, before tac runs. A lemma such as hfit : ∀ v, v ≤ b → Fits w v among the given lemmas proves fitting conditions with tac.

A conditional neither simp nor the discharger decides splits into both alternatives, tagged pos and neg, with the hypothesis hc on the compared values; wram_exec -split stops at it instead, leaving WP w (.branch …) y Q', for instance to join the alternatives with WP.cut. Side conditions that remain are left as goals after the main ones, tagged by the premise they come from (hfit, hle, hb).

def Cslib.WordRAM.wramSimp : Lean.ParserDescr

wram_simp [h₁, h₂] simplifies reads of registers and memory after Data.set and Data.write with the simp set of wram_exec, typically in the postcondition wram_exec leaves. wram_simp (disch := tac) sets the discharger, by default fits on a word-size bound and omega on anything else, and wram_simp at h works on hypotheses.

def Cslib.WordRAM.wramBounded : Lean.ParserDescr

wram_bounded proves y.Bounded w for data y built by Data.set and Data.write from data x with a hypothesis x.Bounded w. It proves the fitting conditions of values read from x and of those stated by a hypothesis, and leaves those of the other written values as goals.

def Cslib.WordRAM.WP.Exec.dischOf (d? : Option (Lean.TSyntax `Lean.Parser.Tactic.discharger)) : Lean.MacroM (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

The discharger of a wram_exec or wram_simp call: the given one, or by default fits on a word-size bound and omega on anything else.