Franziskus Kiefer
Franziskus Kiefer
Due to the `no_std` changes the resolver 2, which is used in edition 2021, hacspec can't be used in crates with the newer edition. The only way to solve this...
The snippet below fails with ``` error[Hacspec]: the variable current_8668 is not present in the context | | Result::::Err(_) => current, | ^^^^^^^ ``` ```rust pub fn result_and( current: Result,...
The library has grown a lot and contains a lot of unnecessary functionality and complexity. This issue tracks cleaning it up. It also has to be decided what to put...
In order to write useful data structures and make it easier to implement parameterized mechanisms, e.g. SHA2-256, SHA2-384, etc, hacspec should support some form of generics.
Including enums from a different module doesn't work. [failing test](https://github.com/hacspec/hacspec/compare/typechecker-module-identifier-bug) that produces the following output. ``` error[Hacspec]: identifier is not a constant --> /Users/franziskus/repos/hacspec/language/test-crate/src/submod1/another_submod1_file.rs:8:5 | 8 | Result::::Err(Error::First) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```rust p256_point_mul_base(P256Scalar::from_byte_seq_be(x)) ``` gets translated to https://github.com/hacspec/hacspec/blob/1d0442aae931a83577bc2b4a14dc12dd78baf0f4/fstar/Hacspec.Tls.Cryptolib.fst#L136-L137
The following code throws an error. ```rust pub fn do_something() { let mut bytes = ByteSeq::new(5); let len = bytes.len(); for i in 0..len { let (first_byte, remainder) = bytes.split_off(1);...
Similarly to #97 it would be great to have an attribute like `#[unsafe_hacspec]` that can be added to functions in hacspec that * have a signature that's in hacspec *...
When setting a custom `crate-type` in the Cargo.toml the typechecker fails with ``` thread 'main' panicked at 'No target in the Cargo.toml', src/main.rs:261:10 ``` To reproduce add a section like...