search

hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
179 stars 19 forks source link

`aes` crate: the frontend loops indefinitely #686

Open W95Psp opened 4 months ago

W95Psp commented 4 months ago

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 at it a bit yesterday (with RUST_LOG=trace cargo hax json, hax being compiled in debug mode), and it seems like some Sized trait obligations are resolved a HUGE number of times before killing the memory of the laptop it's running on. So probably there is somehow an infinite recursion or loop, but that definitively has to do with trait resolution.

Ccing @Nadrieril who had a very very similar issue a few weeks ago

sonmarcho commented 4 months ago

I think this is related: https://github.com/AeneasVerif/charon/issues/191

W95Psp commented 2 months ago

Strangely enough, PR https://github.com/hacspec/hax/pull/730 doesn't fix this issue but fixes the looping behavior in cipher, from https://github.com/RustCrypto/traits. So there are various bugs there.

github-actions[bot] commented 5 days ago

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

W95Psp commented 19 hours ago

This is still a problem, a759a1a87e11a3100e605f0312831596a0543dfb doesn't help