Crate hax_lib

Crate hax_lib 

Source
Expand description

Hax-specific helpers for Rust programs. Those helpers are usually no-ops when compiled normally but meaningful when compiled under hax.

§Example:

use hax_lib::*;
fn sum(x: Vec<u32>, y: Vec<u32>) -> Vec<u32> {
  hax_lib::assume!(x.len() == y.len());
  hax_lib::assert!(x.len() >= 0);
  hax_lib::assert_prop!(forall(|i: usize| implies(i < x.len(), x[i] < 4242)));
  hax_lib::debug_assert!(exists(|i: usize| implies(i < x.len(), x[i] > 123)));
  x.into_iter().zip(y.into_iter()).map(|(x, y)| x + y).collect()
}

Re-exports§

pub use prop::*;
pub use int::*;

Modules§

abstraction 🔒
coq
Procedular macros that have an effect only for the backend coq.
fstar
Procedular macros that have an effect only for the backend fstar.
int
lean
Procedular macros that have an effect only for the backend lean.
proc_macros 🔒
This module re-exports macros from hax-lib-macros since a proc-macro crate cannot export anything but procedural macros.
prop
proverif
Procedular macros that have an effect only for the backend proverif.

Macros§

assert
assert_prop
assume
coq
Embed coq expression inside a Rust expression. This macro takes only one argument: some raw coq code as a string literal.
debug_assert
fstar
Embed fstar expression inside a Rust expression. This macro takes only one argument: some raw fstar code as a string literal.
int
lean
Embed lean expression inside a Rust expression. This macro takes only one argument: some raw lean 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.

Traits§

Concretization
Marks a type as abstract: its values can be lowered to concrete values. This might panic.
RefineAs
Refinement

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. This overrides any exclusion resulting of -i flag.
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.