Franziskus Kiefer

The following enum shouldn't be valid in hacspec but passes the typechecker and is translated to F* (without the value). ```rust #[repr(u16)] pub enum MyEnum { First = 0x0010, }...

Recursion is currently not allowed in hacspec but the typechecker doesn't check it right now.

Having a template for hacspec crates with * the correct rustc version * haspec-lib dependency (and maybe more) would be nice.

In order to put enums into sequences they have to implement `Default`. The idea is to have an `implement_default_for_enum!(NameofEnumType,NameofEnumType::DefaultCase)` macro. And then I pick it up in the compiler and...

The typechecker isn't run on Windows CI right now.

In #139 we see the error ``` error[Hacspec]: operation not available for type Block --> hacspec/examples/aes-ccm/src/ccm_mode.rs:115:18 | 115 | b_curr = y_curr ^ b_curr; | ``` This works fine as...

We recently ran into the issue where we had sha256.rs ```Rust array!(Digest, 16); ``` lib.rs ```Rust use sha256::*; type Digest ByteSeq; fn foo() { let d = Digest::new(5); } ```...

Right now the P256 spec doesn't do any sort of input validation. - [ ] add point validation - [ ] add scalar validation (#137)

The problem is that `from_canvas` just forces the value into the scalar. Instead we have to check that the value is in `[1, order-1]` and return an error if not....

So this creates a `Seq` of size 0 doesn't it? Why do you need that in hacspec, since pushing elements to a Seq is forbidden ? _Originally posted by @denismerigoux...