Repository navigation
Produce explanations of why a verified program is correct #23
Description
Currently, programs that copilot-verifier marks as correct are indicated by a lack of error messages being printed. This, however, doesn't give a sense to the user as to why a program is correct. We should investigate what it would take to equip copilot-verifier with the ability to produce human-readable explanations of what the verifier did in the course of proving a program is correct.
In very broad strokes, I imagine this would require taking ahold of the ProvedGoals that Crux returns after simulation and analyzing them to determine what explanations to produce. There are likely some finer details to work around, however.
Activity
Support logging raw SMT solver interactions
RyanGlScott commentedon Mar 15, 2023
The first step towards producing a cogent explanation of why a proof is correct is to plumb the necessary information into places that are easy to access. Currently, the following information is tucked away under the hood of the verifier, and we should bring it to the surface:
It might make sense to open smaller issues for each of these subtasks as we work on them.
Support logging raw SMT solver interactions
Support logging raw SMT solver interactions
Log information about proof goals with Noisy verbosity
Log information about proof goals with Noisy verbosity
Log information about proof goals with Noisy verbosity
Log information about proof goals with Noisy verbosity