Notation for structured word-RAM programs

ram[ s₁; s₂; … ] writes a structured program (Cslib.WordRAM.Code) as a sequence of statements, one per data instruction, in the style of word-RAM pseudocode. Registers are named by identifiers, for instance local abbreviations of elements of Fin r. The statements are:

• d ← #v: set register d to the constant v;
• d ← s: copy register s into register d;
• d ← i + j, and likewise -, *, /, %, &&&, |||, ^^^, <<<, >>>: a binary operation (Cslib.WordRAM.BinOp) on registers i and j;
• d ← *a, *a ← s: load from and store to the memory cell whose address is in register a;
• d ← width%: set register d to the word size;
• if i = j then [ … ] else [ … ], if i < j then [ … ] else [ … ]: a conditional;
• while i = j do [ … ], while i < j do [ … ]: a loop;
• ⟪c⟫: the structured program c, for instance a subroutine.

The notation unfolds to the constructors of Cslib.WordRAM.Code, so it adds nothing to the semantics. The binary operations and width% are instructions of the standard basis (Cslib.WordRAM.Op.bin, Cslib.WordRAM.Op.width); the other statements work over every basis. It is scoped: open Cslib.WordRAM enables it. Its statement forms follow the word-RAM notation of Algolean. Its only new tokens are ram[, width% and the internal ram_stmt% and ram_block%, so it reserves no identifiers: ram and width remain ordinary names.

Main definitions

• ram[ s₁; s₂; … ]: scoped notation for structured word-RAM programs (Cslib.WordRAM.Code).
• ram_eval: symbolic execution tactic for Cslib.WordRAM.ExecWithin and Cslib.WordRAM.Exec goals.

Tactics

• ram_eval, ram_eval n: symbolic execution. On a goal Cslib.WordRAM.ExecWithin w c x y T or Cslib.WordRAM.Exec w c x y T, it runs the interpreter Cslib.WordRAM.Code.eval on c and x with simp, allowing each loop n iterations (default 0, for loop-free code), and closes the goal when the result is y within (exactly, for Exec) T instructions; with y a metavariable, it determines y. Which constants and results fit a word is decided for numerals and otherwise taken from the given simp lemmas, stated with Cslib.WordRAM.Fits. Programs given by name are unfolded by passing their definitions among the simp lemmas, as in ram_eval [myProgram, h].

References

• S. Srinivas et al., Algolean

def Cslib.WordRAM.wramStmt.quot : Lean.ParserDescr

def Lean.Parser.Category.wramStmt : Category

A statement of a structured word-RAM program.

def Cslib.WordRAM.wramBlock : Lean.ParserDescr

A block of statements, separated by semicolons.

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

A structured word-RAM program, written as a block of statements.

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

Internal: a nested block of statements, as a structured program.

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

Internal: a single statement, as a structured program.

def Cslib.WordRAM.«wramStmt_←#_» : Lean.ParserDescr

Set a register to a constant.

def Cslib.WordRAM.«wramStmt_←_» : Lean.ParserDescr

Copy a register.

def Cslib.WordRAM.«wramStmt_←_+_» : Lean.ParserDescr

Addition.

def Cslib.WordRAM.«wramStmt_←_-_» : Lean.ParserDescr

Truncated subtraction.

def Cslib.WordRAM.«wramStmt_←_*_» : Lean.ParserDescr

Multiplication.

def Cslib.WordRAM.«wramStmt_←_/_» : Lean.ParserDescr

Division.

def Cslib.WordRAM.«wramStmt_←_%_» : Lean.ParserDescr

Remainder.

def Cslib.WordRAM.«wramStmt_←_&&&_» : Lean.ParserDescr

Bitwise and.

def Cslib.WordRAM.«wramStmt_←_|||_» : Lean.ParserDescr

Bitwise or.

def Cslib.WordRAM.«wramStmt_←_^^^_» : Lean.ParserDescr

Bitwise exclusive or.

def Cslib.WordRAM.«wramStmt_←_<<<_» : Lean.ParserDescr

Shift left.

def Cslib.WordRAM.«wramStmt_←_>>>_» : Lean.ParserDescr

Shift right.

def Cslib.WordRAM.«wramStmt_←*_» : Lean.ParserDescr

Load from the memory cell whose address is in a register.

def Cslib.WordRAM.«wramStmt*_←_» : Lean.ParserDescr

Store to the memory cell whose address is in a register.

def Cslib.WordRAM.«wramStmt_←Width%» : Lean.ParserDescr

Read the word size.

def Cslib.WordRAM.«wramStmtIf_=_Then_Else_» : Lean.ParserDescr

A conditional on the equality of two registers.

def Cslib.WordRAM.«wramStmtIf_<_Then_Else_» : Lean.ParserDescr

A conditional on the comparison of two registers.

def Cslib.WordRAM.«wramStmtWhile_=_Do_» : Lean.ParserDescr

A loop while two registers are equal.

def Cslib.WordRAM.«wramStmtWhile_<_Do_» : Lean.ParserDescr

A loop while one register is smaller than another.

def Cslib.WordRAM.«wramStmt⟪_⟫» : Lean.ParserDescr

A structured program given as a term.

def Cslib.WordRAM.ramEval : Lean.ParserDescr

Symbolically execute structured code 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.