Refinements

[W95Psp]

This PR adds support for defining refinement types from Rust via the new macro hax::refinement_type.

A refinement type in Rust is a newtype annotated with a boolean predicate (the refinement). Such a new type is "collapsed" at extraction: it is translated in F* as a type synonym with a refinement.

The proc-macro hax::refinement_type can be used to turn a struct into a refinement, if the struct consists of one private and unnamed field of some base type T. The proc-macro hax::refinement_type takes one argument: a refinement, that is, a boolean predicate on Ts.

Refinement types in Rust are explicit, you have to YourRefinement::new to introduce the refinement, and refine_value.value() to eliminate the refinement.

Elimination can be made mostly implicit in Rust: the methods of the base type can often be implemented on the newtype, and the macro derives the deref trait, which can help to inherit methods as well.

Encoding in F*

In F*, the methods deref, value and new disappear completely: for instance, calls <e>.value() are translated to <e>.

Motivation

Regular type constructions (i.e. structs or enums) help building wider types: the type (u8, bool) is "twice as wide" as u8.

In contrast, refinement types help making types smaller: for instance, one can define a OddU8 type that holds only u8 machine integers which are odd.

This is especially useful for doing proofs: values come with properties attached to them.

Simple examples

• Even numbers

#[hax::refinement_type(|x| x % 2 == 0)]
struct Even(u16);

• Strings with no space

#[hax::refinement_type(|x| !x.chars().any(|ch| ch == ' '))]
struct NoE(String);

• Modular inverse

#[hax_lib::refinement_type(|n| (n as u128 * MOD as u128) % MOD as u128 == 1)]
struct ModInverse<const MOD: u32>(u32);

(normalized) field element

Let's assume we represent elements of the field of 2347 elements. We can define a refinement type that enforces its value are between 0 and 2347 very easily.

#[hax::refinement_type(|x| x <= 2347)]
struct FieldElement(u16);

Compression factor in Kyber

In Kyber, decompress_ciphertext_coefficient for instance takes a parameter coefficient_bits which should be 4, 5, 10 or 11. This constraint is repeated as a pre-conditions multiple times.

This can now be encoded very easily as a refinement type:

#[hax::refinement_type(|x| x == 4 || x == 5 || x == 10 || x == 11)]
struct CompressionFactor(u8);

(note we could also encode that as an enum here)

Bounded integers

See PR #606.

Other

This can be useful for serialization (say you hold a buffer you are writing onto and a cursor, you might want the cursor to always be in bounds), maybe for loop invariants (we can imagine using ghost variables, allow mutation, etc.).

TODO:

• add tests;
• rename value into get
• add a refine helper so that we can do inner_value.refine()

[franziskuskiefer]

I'm not sure I understand this interface.

#[hax::refinement_type(|x| x >= MIN && x <= MAX)]
struct BoundedU8<const MIN: u8, const MAX: u8>(u8);

Why do we need to repeat the MIN and MAX?
We need something that allows us to write

fn some_fun(val: BoundedU16<4, 15>) -> u16;
fn other_fun(state: [u8; 16], index: BoundedUsize<0, 15>) -> [u8; 16];

Is this supposed to be used in a bounded integer library then?
Because this doesn't look like it is what should be used by a consumer like libcrux directly.

I see there's #642. That probably need to go together with this one to see how useful this really is.

[karthikbhargavan]

I see there's #642. That probably need to go together with this one to see how useful this really is.

We did a couple of rounds of trying to improve the description and try to make it self-contained, but clearly it still needs some work and is not very clear.

This is not the bounded integer PR. That one is #642 and yes, that one should provide a super-intuitive user-facing API.
This PR is for more expert use. It allows proof-oriented programmers to define general refinement types.
The reason it has been created now is that this PR is used as an internal mechanism to define the Bounded integers in #642.

But more generally, with this PR, you can define types with any formula attached to it. E.g. even numbers, multiples of 16, refined structs etc. For now, its main use will be in #642 which shake out bugs and usability concerns.

[W95Psp]

Yes, as Karthik said, this PR brings support for user-defined refinement types, not bounded integers.
This PR is essentially about the engine: it adds all the logic and transformations required for refinement types.

Thus, this PR brings no special ergonomic around refinement types in Rust, it's the barebone thing.

The part about bounded integers is just about exemplifying this PR: in two lines of Rust, with this PR, we're able to get minimal bounded integers. But that's the purpose of #606 to bring the Rust library (with nice ergonomics) for bounded integers.

[franziskuskiefer]

Thus, this PR brings no special ergonomic around refinement types in Rust, it's the barebone thing.

Ok so you're saying there's no way right now for me to judge whether this doing what we need it to do. I'll wait for the other PR then.

Also, there's no issue connected to this PR. What issue is this working towards, or fixing?

[spitters]

This looks exciting. Have you considered how it should work in other backends? (CC: @cmester0 )
How does it compare to flux?

[W95Psp]

Thanks @spitters, we should chat to see how to land that in Coq indeed! :)

I'm gonna add some more examples and motivation to this PR. It should be reviewable on its own.

[spitters]

@W95Psp I imagine all the refinement types can be proven automatically in F*. It would be interesting to see whether one can do the same in Coq (and lean, EC, ...)

[franziskuskiefer]

Thanks for the update. I left a couple inline comments.
The two interesting things are

• I still don't understand the doubling of things like bounds. Why is this needed (I don't think it is), or a good design?
• The way this needs to be used is too verbose.

I wonder if this is really something that should be exposed to the user, i.e. something that should be generally available in hax_lib. We can do this in a follow-up. But please file something to investigate what should be available by default and what should go behind feature flags or into a separate crate.