Produce explanations of why a verified program is correct

[copilot-language]

Produce explanations of why a verified program is correct

[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 (#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 (#37)
• Anything else?

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