Unreachable place in Rust AST on `tvix/nix-compat` - ImplExprPredNotFound

[RaitoBezarius]

Hi there,

I have been playing with the Aeneas pipeline for my own projects, notably as I am a Tvix developer (https://tvix.dev/), I was curious if I could extract some of the Nix utilities and pure algebra stuff to Lean.

After https://github.com/hacspec/hax/pull/579, I tested again and obtained this interesting trace: https://0x0.st/X-Q9.txt.

I guess the interesting error is the last one about the AST expectations being violated, unfortunately, I'm not sure having a repro will be easy, but I will look if it has a relationship with https://crates.io/crates/nom and whether I can figure out something.

Tvix can be found at: https://github.com/tvlfyi/tvix -- I tested this against the nix-compat crate. My experimental branch for Aeneas & Hax: https://github.com/RaitoBezarius/hax/tree/experimentations & https://github.com/RaitoBezarius/charon/tree/experimentations.

[W95Psp]

Hi, thanks for the bug report! (especially on a crate like tvix :smiley: that's a very nice project!)

I looked a bit into that, tested on commit 52b9acd: running cargo hax json -k mir-built on this gives me the following output: https://gist.github.com/W95Psp/583b2072c8c702ea47b11a7105d8bfe7

Seems like the function definition fn parse_escaped_bstr(i: &[u8]) -> IResult<&[u8], BString> { is causing the bug (parser.rs line 15). I guess that's nom's complexity hiding in IResult that yields an interesting bound. It is related to https://github.com/hacspec/hax/issues/474 and its fix https://github.com/hacspec/hax/pull/648, but also to PR #495 (which, sadly, doesn't fix that bug).

We should take some time to minimize here (by coming up with some explicit, simplier type instead of IResult<..>)

[github-actions[bot]]

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.

[RaitoBezarius]

Still a problem.