CatCrypt Simp Attribute Declarations

This file declares the named simp sets used by CatCrypt tactics.

Important: register_simp_attr creates simp attributes that cannot be used in the same file they are declared in. This file must be imported by any file that wants to tag lemmas with these attributes.

Simp sets

• ssprove_simpl - SPComp normalization (monad laws, dead code, contraction)
• ssprove_eval - Deep→shallow bridge evaluation lemmas

def Parser.Attr.ssprove_simpl_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.ssprove_simpl : Lean.ParserDescr

ssprove_simpl is the named simp set for normalizing SPComp terms.

Collects lemmas for:

• Monad laws (bind associativity, pure/bind identity)
• Dead code elimination (unused sample, get, pure)
• Contraction rules (duplicate get, put, put-get)
• Copy propagation (set-get same location)

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.ssprove_eval : Lean.ParserDescr

ssprove_eval is the named simp set for deep→shallow bridge evaluation.

Collects lemmas for evaluating RawCode into SPComp.

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.ssprove_eval_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.