feat: cake_lpr interface

[JamesGallicchio]

Interface out to a verified solver (cake_lpr)!

This PR is partially an exploration of how to improve trust at the critical connection point from the Lean kernel to proof checkers.

How do we automatically verify (when Lean is compiling) that the CNF we claim to be UNSAT is the same CNF as the one checked by a proof checker?

current answer:

• Hash the CNF
• A macro calls a trusted proof checker and gets UNSAT
• We store that hash in the Lean file and insert an axiom that the CNF is UNSAT
• on future invocations it just looks at the hash without going out to get the UNSAT result

we might actually be able to run Cayden's checker via native_decide such that the only axiom is reduceBool_correct or whatever it is called!

for cube&conquer results, this becomes more complicated and I don't know how to give a good trust story.