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;
• d ← rand s: sample uniformly from [0, regs s] into register d;
• 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, with its statement forms, their expansions and the tactic ram_eval. Only the category wramStmt and the syntax abbreviation wramBlock are global, since Lean cannot scope them; without the open, wramStmt has no rules, so they parse nothing. The 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).

Tactics

• ram_eval, ram_eval n (scoped, like the notation): 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, by omega from the Fits hypotheses in context (Cslib.WordRAM.reduceFits), so that a bound implied by a fact such as Fits w (base + n) needs no statement of its own, or else by the given simp lemmas. Programs given by name are unfolded by passing their definitions among the simp lemmas, as in ram_eval [myProgram, h]. When it fails, the error names the failing step: the goal has neither form, a given simp lemma does not elaborate, simp cannot evaluate the program, the interpreter returns none, a condition remains undecided (shown), or omega cannot prove the instruction bound (shown). Under try and first, which discard the message, it fails without this replay, at the cost of the attempt alone. ram_eval and ram_exact_eval both expand to the internal tactic ram_eval_core, which holds the shared steps; they differ only in their simp set, ram_eval_simps or ram_exact_eval_simps, whose lemmas for the instructions of the basis differ. The sets are filled, and so indexed, once (ram_eval_simp_set), so a call indexes only the simp lemmas it is given.

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.«wramStmt_←Rand__» : Lean.ParserDescr

Sample uniformly from [0, regs s] into a register.

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). Whether a written number fits a word is decided by omega from the Fits hypotheses in context (Cslib.WordRAM.reduceFits), or by the given simp lemmas.

On failure the error names the step that failed: the goal has neither form, a given simp lemma does not elaborate, simp cannot evaluate the program (pass its definition, as in ram_eval [myProgram]), the interpreter returns none (a fault, or too few loop iterations), a branch or Fits condition remains (shown), or omega cannot prove the instruction bound (shown). Under try or first, which discard the message, it fails without working out which step.

def Cslib.WordRAM.ramEvalCore : Lean.ParserDescr

Internal: the symbolic execution behind ram_eval and ram_exact_eval. The string names the calling tactic in error messages and the number is the loop fuel; the identifier names the simp set that evaluates the program, ram_eval_simps or ram_exact_eval_simps, and the list holds the caller's simp lemmas.

def Cslib.WordRAM.ramEvalSimp : Lean.ParserDescr

Internal: simp +decide only with the simp set set (ram_eval_simps or ram_exact_eval_simps), the simplification procedures of ram_eval (Cslib.WordRAM.RamEval.simprocs), and the given simp lemmas. It is simp +decide only [l₁, …, lₙ, args] for the lemmas l₁, …, lₙ with which ram_eval_simp_set filled set, but it does not index them again.

def Cslib.WordRAM.ramEvalSimpSet : Lean.ParserDescr

Internal: fill the empty simp set set with the entries that simp only [names] builds from the simp lemmas and definitions names, in their order, so that ram_eval_simp set [args] is simp +decide only [names, args]. Simplification procedures belong in Cslib.WordRAM.RamEval.simprocs.

def Cslib.WordRAM.RamEval.simprocs : List (Lean.Name × Bool)

The simplification procedures of ram_eval and ram_exact_eval, in the order in which they are added, with true for those that rewrite after visiting the subterms (post). They are added by name on each call, since the builtin ones cannot be tagged into a simp set in a module.

def Cslib.WordRAM.RamEval.mkContext (set : Lean.Name) (stx : Lean.TSyntax `tactic) : Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.MkSimpContextResult

The simp context of ram_eval_simp set [args], given stx := simp +decide only [args]: the context that mkSimpContext builds for simp +decide only [l₁, …, lₙ, args], where ram_eval_simp_set filled set with l₁, …, lₙ, and simprocs come among the lᵢ. The theorems of set are taken as indexed, and args are elaborated into the same tree, so simp searches one tree, as it does for the literal list.

def Cslib.WordRAM.ramEvalSimpSetFor : Lean.ParserDescr

Internal: fill the simp set set of ram_eval (ram_eval_simps) or ram_exact_eval (ram_exact_eval_simps), given the simp lemmas basis that evaluate the instructions of the basis. The simplification procedures among the lemmas are Cslib.WordRAM.RamEval.simprocs.