Crate hax_lib

Expand description

§hax library

This crate contains helpers that can be used when writing Rust code that is proven through the hax toolchain.

⚠️ The code in this crate has no effect when compiled without --cfg hax. hax sets this cfg automatically when extracting a crate; a regular cargo build leaves it unset.

§Main features

#[hax_lib::requires(...)] and #[hax_lib::ensures(...)]: pre- and postconditions on functions.
#[hax_lib::attributes]: enables requires/ensures on trait methods and refinements on struct fields.
hax_lib::loop_invariant!: loop invariants.
Prop and the logical operators forall, exists, implies: propositions beyond bool.
assume!, assert!, assert_prop!: assumptions and assertions for the backends.
fstar!, coq!, proverif!, …: inline backend code.

§Example

/// The addition in `sum` does not overflow.
fn no_overflow(x: &[u32], y: &[u32]) -> hax_lib::Prop {
    hax_lib::forall(|i: usize| {
        hax_lib::implies(
            i < x.len(),
            x[i] as u64 + y[i] as u64 <= u32::MAX as u64,
        )
    })
}

#[hax_lib::requires(hax_lib::Prop::from(x.len() == y.len()) & no_overflow(&x, &y))]
#[hax_lib::ensures(|result| result.len() == x.len())]
fn sum(x: Vec<u32>, y: Vec<u32>) -> Vec<u32> {
    hax_lib::assert!(x.len() == y.len());
    hax_lib::assert_prop!(no_overflow(&x, &y));
    x.into_iter().zip(y).map(|(x, y)| x + y).collect()
}

Re-exports§

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

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.
int
legacy_lean: Procedular macros that have an effect only for the backend legacy_lean.
prop
proverif: Procedular macros that have an effect only for the backend proverif.

Macros§

assert: Proxy to std::assert!. Compiled with hax, this is transformed into a assert in the backend.
assert_prop: Assert a logical proposition Prop: this exists only in the backends of hax. In Rust, this macro expands to an empty block { }.
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: Proxy to std::debug_assert!. Compiled with hax, this disappears.
fstar: Embed fstar expression inside a Rust expression. This macro takes only one argument: some raw fstar code as a string literal.
legacy_lean: Embed legacy_lean expression inside a Rust expression. This macro takes only one argument: some raw legacy_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§

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: A utilitary trait that provides a into_checked method on traits that have a refined counter part. This trait is parametrized by a type Target: a base type can be refined in multiple ways.
Refinement: A type that implements Refinement should be a newtype for a type T. The field holding the value of type T should be private, and Refinement should be the only interface to the type.

Attribute Macros§

attributes: Enable the following attributes 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.
ensures_ref: Same as ensures, but the closure takes the result by reference: the binder has type &T where T is the function’s return type.
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> [as <TRAIT>], <BODY>)], where <TRAIT> is the trait implemented by the enclosing impl block.
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. Where those future values sit relative to the result in the generated postcondition is backend-dependent, since each backend orders the tuple its functions return differently.
trait_fn_decoration: Internal macro for dealing with function decorations on fn items within a trait. See impl_fn_decoration.
transparent: Mark an item transparent: the extraction will not make it opaque regardless of the -i flag default.

Crate hax_lib

Crate hax_lib Copy item path

§hax library

§Main features

§Example

Re-exports§

Modules§

Macros§

Traits§

Attribute Macros§

Crate hax_lib