Use model to simplify report

[yav]

This PR does the following:

• Adds a .mli file and some docs to the Explain and Report modules
• Modifies Explain to do simplify things based on the current model.
  • For constraints, we eliminate disjunctions, implications, and if-then-else, by eliminating the alternatives that are not viable in the model
  • For the resource hint, we eliminate constraints that are true in the model

[cp526]

Thanks! That looks like it should be very useful.

I wonder whether we might want to set it up so there's a switch in the top bar of the html that toggles between two views:
(1) Showing the state, including constraints and resources just as CN "knows" them, not specialised to the counterexample.
(2) The state specialised to the counterexample, including specialised versions of constraints and resources.

That could be quite easy to implement, by just always recording two versions of some of the components in Report.report, and letting the html switch between these.

The UI should (eventually) be useful for two purposes:

(a) For debugging a verification failure. Here I imagine (2) would often be really useful, to reduce the noise in what's displayed and to make it easier to understand the gap in the proof. One probably still wants to sometimes also see (1). For instance when the verification requires a new lemma, if that's an inductive fact, it might be useful to see (1) to work out how to generalise the current counterexample.

(b) A new CN user should be able to use the interactive UI to develop an intuition for how CN works: for instance by stepping through some (verified or unverified) example to see what CN "knows" at any point along the symbolic execution path. For this (1) is more useful than (2), because the point is not to understand a concrete failure.

Separately: it's probably useful to also be able to switch between showing specialised and non-specialised versions of the unproved constraint or missing resource causing the error (the extras component in Explain).

[cp526]

We might want to extend go to know about binders (and not try to evaluate those), so we can apply the evaluation to Forall and to iterated resources.

[PeterSewell]

+1 for that switch

…

On Sat, 10 Aug 2024 at 10:59, Christopher Pulte ***@***.***> wrote: Thanks! That looks like it should be very useful. I wonder whether we might want to set it up so there's a switch in the top bar of the html that toggles between two views: (1) Showing the state, including constraints and resources just as CN "knows" them, not specialised to the counterexample. (2) The state specialised to the counterexample, including specialised versions of constraints and resources. That could be quite easy to implement, by just always recording two versions of some of the components in Report.report, and letting the html switch between these. The UI should (eventually) be useful for two purposes: (a) For debugging a verification failure. Here I imagine (2) would often be really useful, to reduce the noise in what's displayed and to make it easier to understand the gap in the proof. One probably still wants to sometimes also see (1). For instance when the verification requires a new lemma, if that's an inductive fact, it might be useful to see (1) to work out how to generalise the current counterexample. (b) A new CN user should be able to use the interactive UI to develop an intuition for how CN works: for instance by stepping through some (verified or unverified) example to see what CN "knows" at any point along the symbolic execution path. For this (1) is more useful than (2), because the point is not to understand a concrete failure. Separately: it's probably useful to also be able to switch between showing specialised and non-specialised versions of the unproved constraint or missing resource causing the error (the extras component in Explain). — Reply to this email directly, view it on GitHub <#479 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZVJBQ7A5MNQTUU26HTZQXP75AVCNFSM6AAAAABMJHHBO2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEOBQG42DCMRWGQ> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[dc-mak]

Just for future reference, my preference is that comments should be there to explain why rather than what and variable names should be self explanatory as far as possible. If the variable name would end up being too long, then a short name plus a comment (e.g. as in lines 39-43) is good.