karthikbhargavan
karthikbhargavan
Specify and verify the sampling functions
Verify Ntt algorithms in `Ntt`
- [ ] https://github.com/cryspen/libcrux/blob/8cc3152db28d011f078e9e344d4421ec851cce9b/src/kem/kyber/arithmetic.rs#L68 The cast to i16 makes the call to `get_n_least_significant_bits` unnecessary - [ ] https://github.com/cryspen/libcrux/blob/8cc3152db28d011f078e9e344d4421ec851cce9b/src/kem/kyber/constant_time_ops.rs#L14 The `value |` seems to be unnecessary - [ ] https://github.com/cryspen/libcrux/blob/8cc3152db28d011f078e9e344d4421ec851cce9b/src/kem/kyber/constant_time_ops.rs#L54 Here...
- [ ] Get it through charon - [ ] Get it through eurydice - [ ] Cleanup C code - [ ] Improve C code - [x] #145 -...
Add C extraction to libcrux CI. - [ ] script for extraction (add to `hax-driver`) - [ ] add script to CI * Opam setup * Get and build karamel...
Not all the code we have in libcrux is verified (e.g. SHA-2 and x25519 from libjade) and we may want to add other partially-verified code in the future. Our policy...
When adding a constraint of the form `T: Copy`, rustc always adds a second constraint `T:Copy+Clone`. Consequently, the generated typeclass in F* has both constraints (to be solved). However, the...
When translating Rust trait implementations `impl`s, hax puts the entire implementation into the interface file. This has two bad effects: - first, we cannot abstract away from the implementation, and...
traits of the form: ``` trait T: A + B { } ``` get translated to ``` class T (v_Self:Type) = { [@@@ FStar.Tactics.Typeclasses.no_method]_super_16550665238208597986:t_A v_Self; [@@@ FStar.Tactics.Typeclasses.no_method]_super_9181983936900423582:t_B v_Self; } ```...
Currently our F* models of `Rand_core`, `std`, and `alloc` are all inside `proof-libs/fstar/core` They should be in their own folders. cf #574