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
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
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§

Abstraction
Marks a type as abstractable: its values can be mapped to an idealized version of the type. For instance, machine integers, which have bounds, can be mapped to mathematical integers.
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.
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.