Jonathan Protzenko

cargo-charon does not generate an llbc file upon a second invocation

1

you can reproduce by running cd libcrux/libcrux-ml-kem; ./c.sh; ./c.sh with the following revisions: ``` libcrux: 1366394ec8d5b63da49d33a69f73f164a3ec2cfa (on lucas/extract-intrinsics) charon: c7b2396375cec464fb1e1f27477890681697e3ad (on fix-203) everest/karamel: 04cb86b94f57c495b715d6e9f98e29352d72d5f3 (on protz_trait_methods) eurydice: 24b384be011a7bf793a32ec39aa36d365e60313d (on protz_trait_clauses)...

Confusion about the LLBC produced for a closure

5

```rust jonathan@verveine:~/Code/eurydice (protz_trait_clauses) $ \cat test/closure/src/main.rs fn f() -> [u8; 1] { let s = [0; 1]; let a: [u8; 1] = core::array::from_fn(|_| s[0]); a } fn main() { let...

Suboptimal placement of comment

4

Consider the following function (from mlkem): ```rust pub(crate) fn barrett_reduce_element(value: FieldElement) -> FieldElement { // hax_debug_assert!( // i32::from(value) > -BARRETT_R && i32::from(value) < BARRETT_R, // "value is {value}" // );...

Bug: ill-typed projection element

1

In Eurydice, I am traversing the Charon representation of the following function: https://github.com/cryspen/libcrux/blob/franziskus/mldsa-c-ci/libcrux-ml-dsa/src/simd/avx2.rs#L140-L142 To observe this, run `./boring.sh` in the `libcrux-ml-dsa` subdirectory, on an x64 machine (this code is disabled...

Clarify longest match behavior of the grammar

2

https://doc.rust-lang.org/reference/expressions.html claims `as` binds tighter than than `+` or `

Upgrade Z3 to 4.13.3

26

This is just an issue to discuss upgrading to Z3 4.13.3. Is this a good idea? I'm not sure. Pros: - no more emulation for Apple Silicon (4.8.5 does not...

Dependencies in karamel.opam seem quite out of date

2

I'm not sure we need ulex or even batteries anymore. I'm also wondering if there's a way to make the fstar dependency optional in case all we want to build...

from https://github.com/hacl-star/hacl-star/pull/1025 -- having files named identically can cause problems down the line, so it might be a good idea to have a different name for the internal headers, like...

Bug: duplication of basic-blocks for test conditions of the form e1 && e2 (control-flow reconstruction issue)

4

This: ``` fn h(x: &str) {} fn main() { { if true && true { h("foo") } else { h("bar") } } } ``` gets pretty-printed as: ``` // Full...

Bug: architecture-specific behavior

3

First OSX device, setup is as follows: ``` jonathan@absinthe:~/Code/eurydice (protz/preserve_const) $ uname -a Darwin absinthe 24.6.0 Darwin Kernel Version 24.6.0: Mon Jul 14 11:28:17 PDT 2025; root:xnu-11417.140.69~1/RELEASE_X86_64 x86_64 jonathan@absinthe:~/Code/eurydice (protz/preserve_const)...