Attribute Macro refinement_type

#[refinement_type]

Marks a newtype struct RefinedT(T); as a refinement type. The struct should have exactly one unnamed private field.

This macro takes one argument: a Prop proposition that refines values of type SomeType.

For example, the following type defines bounded u64 integers.

#[hax_lib::refinement_type(|x| x >= MIN && x <= MAX)]
pub struct BoundedU64<const MIN: u64, const MAX: u64>(u64);

This macro will generate an implementation of the [Deref] trait and of the [hax_lib::Refinement] type. Those two traits are the only interface to this newtype: one is allowed only to construct or destruct refined type via those smart constructors and destructors, ensuring the abstraction.

A refinement of a type T with a formula f can be seen as a box that contains a value of type T and a proof that this value satisfies the formula f.

In debug mode, the refinement will be checked at run-time. This requires the base type T to implement Clone. Pass a first parameter no_debug_runtime_check to disable this behavior.

When extracted via hax, this is interpreted in the backend as a refinement type: the use of such a type yields static proof obligations.