hax_lib

Module proc_macros

Source
Expand description

This module re-exports macros from hax-lib-macros since a proc-macro crate cannot export anything but procedural macros.

Modules§

coq
Procedular macros that have an effect only for the backend coq.
fstar
Procedular macros that have an effect only for the backend fstar.
proverif
Procedular macros that have an effect only for the backend proverif.

Macros§

coq
Embed coq expression inside a Rust expression. This macro takes only one argument: some raw coq code as a string literal.
fstar
Embed fstar expression inside a Rust expression. This macro takes only one argument: some raw fstar code as a string literal.
loop_decreases
Must be used to prove termination of while loops. This takes an expression that should be a usize that decreases at every iteration
loop_invariant
Add an invariant to a loop which deals with an index. The invariant cannot refer to any variable introduced within the loop. An invariant is a closure that takes one argument, the index, and returns a proposition.
proverif
Embed proverif expression inside a Rust expression. This macro takes only one argument: some raw proverif code as a string literal.

Attribute Macros§

attributes
Enable the following attrubutes in the annotated item and sub-items.
decreases
Provide a measure for a function: this measure will be used once extracted in a backend for checking termination. The expression that decreases can be of any type. (TODO: this is probably as it is true only for F*, see #297)
ensures
Add a logical postcondition to a function. Note you can use the forall and exists operators.
exclude
Exclude this item from the Hax translation.
impl_fn_decoration
Internal macro for dealing with function decorations (#[decreases(...)], #[ensures(...)], #[requires(...)]) on fn items within an impl block. There is special handling since such functions might have a self argument: in such cases, we rewrite function decorations as #[impl_fn_decoration(<KIND>, <GENERICS>, <WHERE CLAUSE>, <SELF TYPE>, <BODY>)].
include
Include this item in the Hax translation.
lemma
Mark a Proof<{STATEMENT}>-returning function as a lemma, where STATEMENT is a Prop expression capturing any input variable. In the backends, this will generate a lemma with an empty proof.
opaque
Mark an item opaque: the extraction will assume the type without revealing its definition.
opaque_type
Mark an item opaque: the extraction will assume the type without revealing its definition.
process_init
A marker indicating a fn as a ProVerif process initialization.
process_read
A marker indicating a fn as a ProVerif process read.
process_write
A marker indicating a fn as a ProVerif process write.
protocol_messages
A marker indicating an enum as describing the protocol messages.
pv_constructor
A marker indicating a fn should be automatically translated to a ProVerif constructor.
pv_handwritten
A marker indicating a fn requires manual modelling in ProVerif.
refinement_type
Marks a newtype struct RefinedT(T); as a refinement type. The struct should have exactly one unnamed private field.
requires
Add a logical precondition to a function. In the case of a function that has one or more &mut inputs, in the ensures clause, you can refer to such an &mut input x as x for its “past” value and future(x) for its “future” value.
trait_fn_decoration
transparent
Mark an item transparent: the extraction will not make it opaque regardless of the -i flag default.