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 #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 😃 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 #474 and its fix #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]

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.

[W95Psp]

Hi, can you try to reproduce on main? I suspect #1008 fixed this issue.
I'm not able to test on my side, I've got errors related to rustc versions or something.

[W95Psp]

Let's close, this should not be an issue any more.
If the bug is still there, please re open.

[RaitoBezarius]

Apologies, I have been quite busy but whenever I have the time, I will report back, thanks Lucas! :) -- Ryan Lahfa

…

On Wed, Oct 23, 2024 at 9:25 AM Lucas Franceschino ***@***.***> wrote: Let's close, this should not be an issue any more. If the bug is still there, please re open. — Reply to this email directly, view it on GitHub <#604 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AACMZRFM7TPZJLKCNBYFIVTZ45FMZAVCNFSM6AAAAABGEURU3SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMZRGEZTGMJSGM> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[W95Psp]

No worries, thank you 😃