Macros§
- coq_
expr - coq_
unsafe_ expr - fstar_
expr - fstar_
unsafe_ expr - int
- loop_
invariant - proverif_
expr - proverif_
unsafe_ expr
Attribute Macros§
- attributes
- coq_
after - coq_
before - coq_
replace - ensures
- exclude
- fstar_
after - fstar_
before - fstar_
options - fstar_
replace - fstar_
verification_ status - impl_
fn_ decoration - include
- lemma
- opaque
- opaque_
type - process_
init - process_
read - process_
write - protocol_
messages - proverif_
after - proverif_
before - proverif_
replace - pv_
constructor - pv_
handwritten - refinement_
type - requires
- trait_
fn_ decoration - transparent