search

AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification
Apache License 2.0
62 stars 15 forks source link

CI: build Kyber's extracted C #238

Open pnmadelaine opened 3 weeks ago

pnmadelaine commented 3 weeks ago

It seems that there is a mismatch between type aliases generated by eurydice and what the handwritten C code in ml-kem is expecting:

/run/github-runner/charon-ci/charon/charon/libcrux-ml-kem/c/tests/sha3.cc:72:3: error: ‘libcrux_ml_kem_types_MlKemKeyPair____2400size_t__1184size_t’ was not declared in this scope; did you mean ‘libcrux_ml_kem_types_MlKemPublicKey____1184size_t’?
Nadrieril commented 3 weeks ago

It seems that there is a mismatch between type aliases generated by eurydice and what the handwritten C code in ml-kem is expecting

This will need to get fixed before we can merge

pnmadelaine commented 3 weeks ago

@Nadrieril well this is a libcrux issue, isn't it?

Nadrieril commented 3 weeks ago

Yes indeed, so this PR is blocked until we figure out what to change in eurydice or libcrux