hax-lib: introduce a Prop abstraction

[karthikbhargavan]

This PR introduces a Prop type for use in formulas.
It also cleans up the structure of hax-lib a little.

[W95Psp]

I wonder if we should not add a prelude to hax-lib.
Exporting everything in the hax_lib namespace feels a bit aggressive.

Instead, we could have a hax_lib::prelude module that re-exports every name that make sense to have top-level, i.e. not assert (which overrides core's assert).

[karthikbhargavan]

I have tested this on libcrux and it works well.
It will unblock cryspen/libcrux#788
So let's review and get this in.

[karthikbhargavan]

@maximebuyse it would be good to check that this PR will not break PQ11 or Sandwich.

[karthikbhargavan]

I wonder if we should not add a prelude to hax-lib. Exporting everything in the hax_lib namespace feels a bit aggressive.

As a user, I would really not have to know too much about the structure of hax_lib, so a single namespace seems fine to me? Or else we could break it into a couple of name spaces but let's do it soon or else it will be painful to refactor later.

[W95Psp]

Yeah, but exposing everything top-level is not so nice either: it's polluting context.
If you want to use both std's assert and Int for instance, you'd have to use hax_lib::{Int, Abstraction, Concretization}.

A prelude would be nice to import automatically traits: use hax_lib::prelude::* could import all the traits, and maybe a few other items whose name are explicitely referring to proofs or hax (e.g. fstar!).

I think preludes are pretty common in the Rust ecosystem, so I don't think this will be unintuitive for users.

[maximebuyse]

All good for PQ11 and Sandwich