Lucas Franceschino
Lucas Franceschino
In the presence of universe variables, `tcresolve` doesn't work. Consider the following module: ```fstar module Bug class foo (t: Type0): Type = { u: Type } // or this explicit...
The version of F* in the CI is too old, thus the code in `extraction-edited` doesn't typecheck. Solutions: - wait for a new F* release (I asked on F*'s slack);...
To reproduce, clone https://github.com/RustCrypto/block-ciphers at commit ae1892c8, and `cargo hax json` on crate `aes`. This behavior is the same for libsignal, which uses the crate `aes`. @franziskuskiefer and I looked...
Reproducer: ```rust fn uints() -> impl Iterator { vec![0u64].into_iter() } fn main() { let mut hello = uints(); hello.next(); } ``` [Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/latest-main/gist=79e3245eef4c026224b317283b165caa) Crashes with:...
To reproduce, run `RUST_BACKTRACE=1 cargo hax json` on the `cipher` crate of the repo https://github.com/RustCrypto/traits at commit [b2e31d8df29](https://github.com/RustCrypto/traits/commit/b2e31d8df293026390b6315c10844eed8b54a185). Backtrace: ``` error: internal compiler error: compiler/rustc_middle/src/ty/subst.rs:901:9: type parameter `T/#1` (T/1) out...
On Friday I experimented a bit with Inkscape to make a logo for hax, any thoughts? :smile: . . [View readme](https://github.com/hacspec/hax/blob/c31c177d109719dc10be0737e70f35263d6788ba/README.md)