Produce explanations of why a verified program is correct

[RyanGlScott]

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.

[RyanGlScott]

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:

• Undefined behavior checks in Crucible
• Other Crucible assertions
• What4 formulae for the bullet points above
• Raw SMT solver interactions corresponding to the What4 formulae (Support logging raw SMT solver interactions #36)
• Equality checks between Copilot stream values and C array values
• Equality checks between trigger arguments on the Copilot and C side
• Checks that the trigger functions are invoked at the same times on the Copilot and C side
• Copilot line number information (Display Copilot-related line number information #37)
• Anything else?

It might make sense to open smaller issues for each of these subtasks as we work on them.