search

AeneasVerif / eurydice

Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
Apache License 2.0
21 stars 1 forks source link

Wrong code gen (map) #13

Closed franziskuskiefer closed 3 months ago

franziskuskiefer commented 3 months ago

Two places with invalid code gen (that may or may not be related). The diff in hacl-packages has manual fixes to the C code.

The code here

https://github.com/cryspen/libcrux/blob/66c2e554124e9e802ad99e724bb4e4da4f606dbf/libcrux-ml-kem/src/sampling.rs#L74-L104

gets compiled to

https://github.com/cryspen/hacl-packages/commit/e19a2375c2b15a9a3cc4d25a7eb7f06092d6d9e2#diff-0d8e4e786b25ff53506ee2584cdcf17926c6b18ee67d3c7a88405d7d7746db1cR7768-R7777

The map at the end is not compiled right.

Similarly,

https://github.com/cryspen/libcrux/blob/66c2e554124e9e802ad99e724bb4e4da4f606dbf/libcrux-ml-kem/src/polynomial.rs#L34-L40

gets compiled to

https://github.com/cryspen/hacl-packages/commit/9fb519da30bee5b9afbe83d2596e81f0967efbd8#diff-0d8e4e786b25ff53506ee2584cdcf17926c6b18ee67d3c7a88405d7d7746db1cR2456-R2461

msprotz commented 3 months ago

This is now fixed since mlkem works.