hax `aes` crate: the frontend loops indefinitely

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

May 22 '24 07:05 W95Psp

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

May 23 '24 11:05 sonmarcho

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.

Jul 29 '24 08:07 W95Psp

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.

Sep 28 '24 02:09 github-actions[bot]

This is still a problem, a759a1a87e11a3100e605f0312831596a0543dfb doesn't help

Oct 02 '24 08:10 W95Psp

Still there after #970

Oct 07 '24 15:10 W95Psp

@Nadrieril mostly fixed the bug with its PR #996! So it was just extremely slow because it was re-doing things again and again.

This pseudo-loop was hiding another bug; I have a fix, will push a PR soon. But the aes crate now extract in under 40 seconds! Thanks @Nadrieril!

Oct 14 '24 12:10 W95Psp

Let's close this. The extraction now works: the extraction itself takes around 40s, but the haxmeta/JSON business takes around 4 minutes on my laptop...

Let's see how we can improve that:

https://github.com/hacspec/hax/issues/1001

Oct 14 '24 15:10 W95Psp