Crate hax_lib

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

coq

Procedural macros for coq

fstar

Procedural macros for fstar

int

prop

proverif

Procedural macros for proverif

Macros

assert

assert_prop

assume

coq

debug_assert

fstar

loop_invariant

proverif

Traits

RefineAs

Refinement

Attribute Macros

attributes

ensures

exclude

impl_fn_decoration

include

lemma

opaque

opaque_type

process_init

process_read

process_write

protocol_messages

pv_constructor

pv_handwritten

refinement_type

requires

trait_fn_decoration

transparent