The simp set of wram_exec

The simp set used by wram_exec and wram_simp in CslibFrontier.Computability.WordRAM.SymbolicExec, declared in a file of its own because an attribute cannot be used in the file declaring it. Lemmas and simplification procedures are tagged where they are proved. A simp set is indexed once, when its lemmas are tagged, so a call that uses it does not index its lemmas again; wram_exec and wram_simp run often in a long proof.

Main definitions

• wram_simps: reads of registers and memory after writes, and arithmetic identities.

def Parser.Attr.wram_simps_proc : Lean.ParserDescr

Simplification procedure

def Parser.Attr.wram_simps : Lean.ParserDescr

The simp set wram_simps reads registers and memory after Data.set and Data.write, and simplifies arithmetic identities, for wram_exec and wram_simp.