rustc-like error messages for failed proofs

[Kixunil]

I think I know how creusot could get error messages that look completely like rustc and would hugely improve developer experience. I'm also willing to take a shot at it if I get a green light for it, including adding a dependency on an error-message-rendering library. I have an experience with codespan_reporting as I already used it in two projects but recently I found out that rustc uses annotate-snippets which is most likely better choice and I'm totally willing to try to use it. It shouldn't be super hard anyway.

What I imagine is messages like this:

error: cannot prove assertion
 --> src/foo.rs:5:1
  |
5 | proof_assert!(foo@ == bar@);
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ 
  | |
  | |
  | This assertion could not be proven
  |

Or more complex

error: cannot prove precondition `x < 42`
 --> src/foo.rs:7:1
  |
7 | foo(x);
  | ^^^^^^
  | |
  | |
  | The function call with unprovable precondition
  |
note: the precondition was defined here
 --> src/foo.rs:2:3
  |
2 | #[requires(arg < 42)]
  |   ^^^^^^^^^^^^^^^^^^
  |   |
  |   |
  |   This precondition could not be proven
  |

(I'm not sure how hard would it be to substitute the arguments as the example does though. But even if I couldn't do it that would still be way better than the current situation.)

[Lysxia]

I think that's a reasonable proposal and I'm happy to let you work on this. You've covered the matter of displaying the error, but there is also the task of getting the right source locations out of why3/why3find (previously #1902 but I never got around to writing down these details).

1. why3find prove has the -x flag for this, so you could try to just parse its output as a starting point,
2. but it doesn't necessarily report the most relevant locations if the better ones have been lost from splitting or normalizing the goal. That may require a bit of hacking on why3find to recover.
3. It may also be worth getting why3find to output this information in a conventional format to make parsing simpler and more robust.

Does this still sound approachable to you?

[Kixunil]

I was thinking more about just parsing the files which seem to be already in reasonably robust formats. Also I didn't intend to make it fully perfect right away, just try to get something working and see how it goes. Reminds me, that might need some additional dependencies on xml or whatever else is relevant.

[Lysxia]

What files do you mean? proof.json and why3session.xml contain no location information.

[Kixunil]

IIUC, those files contain the information about which checks passed and that should be possible to cross-reference with the coma files.

[Lysxia]

I see. That doesn't seem straightforward to me, but maybe you'll surprise me. Any progress on this issue is welcome.

[jhjourdan]

If you want to use the coma file and match it with the proof.json file, I am afraid you will have essentially to reimplement the VCGen of Coma, in a compatible manner, which is not easy in the first place and then will cause maintainable issues.

I'm happy if you want to work on this, and I agree that the current situation wrt locations is not good. However I need to warn you that this is not an easy problem. In many situations (ex. closures), it is difficult to track down the location of a VC, and actually quite often there are several locations to report for one VC...

[Kixunil]

Yeah, I did a bunch of digging around and found that probably the best way would be to emit our own json with the span mappings and load it afterwards. Then the deserializer becomes just a call into serde. And from what I've seen we need to match it against proof.json which has a tree structure.

I'm not familiar with the rustc codebase so if you think this approach would be good maybe we should split the tasks - you generate the mapping and I do the rest. Or, if you don't have time for it, at least a bunch of explaining where to put it etc would help me.

[Lysxia]

I don't think creusot-rustc can emit span information that would directly match the structure of proof.json. The structure of proof.json really depends on how Why3 interprets Coma programs. Hence it's easier to get that information out of why3find prove -x. This approach also has the advantage that it can be handled outside of creusot-rustc, so this requires zero knowledge of the rustc API. It would all happen in cargo-creusot which is a self-contained Rust program.

[Kixunil]

OK, I can try the -x thing but the help says it's just for tty, so I have strong doubts there.

[jhjourdan]

Alternatively you could link with Why3/why3find and use the internal API

[Kixunil]

After looking into it, I concluded that it'd take me way too much time to do everything myself and tasked an LLM to write the span extracting part and only wrote the message emitting myself. It seems to work mostly, I'm just figuring out some things around invariants and whatnot. Is it OK for you to submit such code? I will review it myself before submission to the best of my ability. This shouldn't be a critical part anyway. Of course I will respect if you don't want to spend time on that.

[jhjourdan]

The main issue here is maintainability. If nobody in the world understand (ever understood) the code, it's unlikely we will be able to maintain it correctly. So, if it is not too large, not too invasive and reasonably clear, why not... But I have to say that I am not particularly inclined to accept such piece of code.

[Kixunil]

Good point, I will make sure to understand and document it properly. It is extremely uninvasive - currently I don't even have it as a part of cargo-creusot but as a standalone tool to make the development easier.