langston-barrett
commented
1 month ago This PR moves in the direction of deduplicating code that proves goals. In the future, it would be nice to improve these helpers by:
- Allowing "fast failure" on conjunctions of goals (i.e., not attempting to prove the RHS if the LHS is disproved)
- Parallelization and timeouts of solver queries (see the ambient-verifier link above)
- Use of
push/popin an online solver, rather than distributing assumptions into goals
We check proof obligations that come from Crucible a lot:
https://github.com/GaloisInc/crucible/blob/f9760bdb9921523848efc9889fbd72bd6dea506e/crucible-symio/tests/TestMain.hs#L151C3-L151C31
https://github.com/GaloisInc/macaw/blob/645754178a034c22e97aac49a962c99b387aaa01/symbolic/src/Data/Macaw/Symbolic/Testing.hs#L330
https://github.com/GaloisInc/surveyor/blob/96b6748d811bc2ab9ef330307a324bd00e04819f/crux-dbg/src/Crux/Debug/LLVM/Overrides.hs#L161
https://github.com/GaloisInc/mss/blob/ca97f1bc6b296b30bcccad3b4098544d91427103/grackle/src/Grackle/Overrides/Utils.hs#L84
https://github.com/GaloisInc/ambient-verifier/blob/eab04abb9750825a25ec0cbe0379add63f05f6c6/src/Ambient/Verifier/Prove.hs#L137
As seen above, most of these instances use somewhat low-level What4 functions, and require thinking about the encoding of proof assumptions and obligations into a SMT-compatible format (in particular, they inline the material conditional). This PR introduces more high-level helpers. Doing so required a bit of refactoring.