Define and implement a stable proof format for verified checking #43
Description
Varisat's own proof format is intentionally unspecified and without stability guarantees (so it can always be kept in sync with all implemented techniques).
I do want to support checking proofs with formally verified proof checkers though. So far that is possible by using LRAT proofs. Some planned features are incompatible with the LRAT format though (#30, #31, and others that don't have issues yet).
My plan here is to define a stable proof format that corresponds to the CheckedProofStep type. This is simpler than the internal proof format (unique IDs instead of hashes, no duplicated clauses, several different types of internal steps map to the same type of checked step). Hopefully this makes it practical to keep a formally verified proof checker compatible with this.