hax_lib/
abstraction.rs

1/// Marks a type as abstractable: its values can be mapped to an
2/// idealized version of the type. For instance, machine integers,
3/// which have bounds, can be mapped to mathematical integers.
4///
5/// Each type can have only one abstraction.
6pub trait Abstraction {
7    /// What is the ideal type values should be mapped to?
8    type AbstractType;
9    /// Maps a concrete value to its abstract counterpart
10    fn lift(self) -> Self::AbstractType;
11}
12
13/// Marks a type as abstract: its values can be lowered to concrete
14/// values. This might panic.
15pub trait Concretization<T> {
16    /// Maps an abstract value and lowers it to its concrete counterpart.
17    fn concretize(self) -> T;
18}