Lucas Franceschino

Performance blow up

3

Consider the following (repetitive) module: ```fstar module Test #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open FStar.Mul assume new val u32: Type0 assume new val u16: Type0 assume new val...

cryspen/hax#1749 introduces a change in the naming scheme of the impl expressions; this needs to be reflected in libcrux. Instead of using hashes, we now use indexed names, which should...

Propagate ML-DSA pre- and post-conditions for encoding in `traits.rs`

5

https://github.com/cryspen/libcrux/pull/997 added pre/posts and proofs to AVX2 encoding, but we still need to propagate the pre/post to traits.rs, and make sure the pre/posts are compatible and easy to propagate. See...

feat(docs): CONTRIBUTING.md: add guidelines for hax

2

This PR adds guidelines for hax.

Rust Engine: missing pieces of information in `FullDef` items

2

This issue exists to collect information about missing pieces of data for transitioning from an HIR-based importer to a `FullDef` importer. - `TyFnSignature`: we need the patterns on the parameters,...

We have a test that checks the website and whether the tutorial examples work. But when it fails, we don't get notified, so we often just ignore it.

`cargo-hax`: add a `--single-file` to `cargo hax`

4

`--single-flag` should be incompatible with `-C` and will use the rustc custom driver directly, without cargo Thanks @Nadrieril for the idea :)

Requires and ensures: allow multiple per function

4

Currently, the engine will tell the use it's illegal to add multiple `requires` or `ensures`. We want to allow that and build conjunctions instead. ```rust #[hax_lib::requires(true)] #[hax_lib::requires(true)] fn f() {}...