Franziskus Kiefer

@mikkelmilo is right, Rust has an advanced out-of-order handling whereas ML-based languages like Coq or F* require the source code to be ordered by forward dependency. Inside the compiler, I...

The verification backends should be run on CI to ensure that they don't break - [ ] Add F* CI - [ ] Run make in the fstar directory -...

The CI needs ~45 minutes to finish because it's running a lot of wycheproof tests on slow specs. For better engineering experience this time has to get down.

Support non-conventional capitalization in the backends

3

In order write hacspecs that are as close as possible to RFCs and other specifications it is sometimes necessary to deviate from the Rust conventions for capitalizing variables, functions etc....

Warn on integer casting only when necessary

1

hacspec currently warns every time an integer is casted, e.g ```rust type MyU32 = u32; let x = MyU32(8u32); let y = x as u128; ``` will lead to the...

Don't require `Default` on `Seq<T>`

2

Requiring `T: Default` on `Seq is limiting especially because it makes it impossible to put enums into sequences. Instead the following approach should be used. (There's another way to solve...

https://github.com/hacspec/hacspec/blob/203000726c87afce24f3187ac51cd59feea44ec2/lib/src/seq.rs#L195-L197

Because the typechecker currently expects a block in the else branch `else if` can't be used. ``` error[Hacspec]: block of statements expected in the else branch in Hacspec ```

With crate A defining ```rust #[derive(Default)] pub struct X(u32); ``` and crate B using it ```rust use A::*; pub struct Y(Seq); ``` the F* translation panics with ``` > Successfully...

Typechecker doesn't import dependencies of dependencies

1

Assume we have a crate X that uses crate Y, which uses the hacspec library. In crate X, calling a function on a type alias defined in crate Y that...