Notation for structured word-RAM programs over the exact basis

ram_exact[ s₁; s₂; … ] is ram[ s₁; s₂; … ] over the exact basis Cslib.WordRAM.Basis.exact: it has the same statements, but a binary operation d ← i - j, d ← i / j, … is the instruction Cslib.WordRAM.Op.exactBin, which faults where its exact value is undefined (subtraction below zero, division and remainder by zero), and d ← width% is Cslib.WordRAM.Op.exactWidth. The tactic ram_exact_eval is ram_eval for such programs.

The notation, with its expansions and the tactic, is scoped to Cslib.WordRAM, alongside the wramStmt statement syntax of Complexity/Computability/WordRAM/Notation.lean.

Main definitions

• ram_exact[ s₁; s₂; … ]: structured word-RAM programs over the exact basis.
• ram_exact_eval: symbolic execution of such programs.

Tactics

• ram_exact_eval, ram_exact_eval n: as ram_eval. A subtraction runs when the simp lemmas show that its right operand is at most its left one, and a division or remainder when they show that its divisor is nonzero.

References

The statements are those of the ram[ notation (WordRAM.Notation), whose forms follow the word-RAM notation of Algolean.

def Cslib.WordRAM.«termRam_exact[_;]» : Lean.ParserDescr

A structured word-RAM program over the exact basis, written as a block of statements.

def Cslib.WordRAM.«termRam_exact_block%_» : Lean.ParserDescr

Internal: a nested block of statements, as a structured program over the exact basis.

def Cslib.WordRAM.«termRam_exact_stmt%_» : Lean.ParserDescr

Internal: a single statement, as a structured program over the exact basis.

def Cslib.WordRAM.ramExactEval : Lean.ParserDescr

Symbolically execute structured code over the exact basis on a goal ExecWithin w c x y T or Exec w c x y T, allowing each loop the given number of iterations (default 0), and deciding with the given simp lemmas which written numbers fit a word, which subtractions stay at or above zero, and which divisors are nonzero.