# CPC proof checking and replay

Status: deferred follow-up to the proof retrieval API. The implementation details
below refer to cvc5 1.3.4, the version pinned by this binding.

`Solver::get_proof_cpc()` retrieves a proof after an unsatisfiable result. Checking
that proof is separate work. A sufficiently detailed certificate records the
derivation, allowing a checker to validate its steps without repeating the
original SMT search. Checking still requires computation, and proof size and rule
side conditions affect its cost.

Ethos already performs this replay for CPC. It uses its own engine to interpret
the CPC rules and supporting programs defined in Eunoia signature files. Its
authors identify reducing the trusted code base and supporting user-defined
calculi as design goals. Ethos is not formally verified; its engine, dependencies,
and the soundness of the selected rule signatures remain part of the trust
assumptions. See the [Ethos paper](https://link.springer.com/chapter/10.1007/978-3-032-32589-1_19).

Reusing cvc5's internal checker would also be a reasonable way to avoid repeated
search. It could catch errors in proof construction and solver bookkeeping.
However, any reused checking, rewriting, or arithmetic routines would remain
trusted. For example, if a buggy simplifier both produces and validates a rewrite,
replay through that routine could accept the same mistake. An independent
implementation provides another opportunity to catch it. Independence is an
additional assurance goal, not a prerequisite for replay.

cvc5 1.3.4 has an internal `ProofChecker` that checks individual rule applications,
but its public API does not expose a CPC importer or a standalone replay entry
point. `--check-proofs` checks proofs generated by the solver after solving; it
does not load a certificate to bypass search. CPC printing also transforms some
internal rules and terms, so importing it requires more than reversing a text
serialization. These are implementation observations, not a documented maintainer
explanation for omitting a replay API. See the pinned
[checker interface](https://github.com/cvc5/cvc5/blob/cvc5-1.3.4/src/proof/proof_checker.h),
[proof-checking option](https://github.com/cvc5/cvc5/blob/cvc5-1.3.4/src/options/smt_options.toml),
and [CPC printer](https://github.com/cvc5/cvc5/blob/cvc5-1.3.4/src/proof/eo/eo_printer.cpp).

A replay implementation using cvc5 internals would need to:

1. Parse CPC declarations, terms, proof references, and assumption scopes.
2. Map exported CPC rules and arguments to supported internal checks, accounting
   for transformations made by the printer.
3. Validate each step using previously checked premises, reject unsupported or
   trusted steps, and ensure the final result is a refutation of the supplied
   problem with all temporary assumptions discharged.
4. Expose recoverable errors through a binding and test malformed proofs, altered
   conclusions, wrong input assumptions, and supported theory combinations.

These effort estimates assume one engineer familiar with SMT and compiler
implementation, including testing. They exclude formal verification and matching
Ethos's performance. They are planning estimates, not measured delivery times.

| Approach | Estimated effort |
| --- | --- |
| Integrate the existing Ethos executable | 3-10 engineering days |
| Independent MoonBit checker for selected Boolean and equality rules | 2-4 weeks |
| Independent MoonBit checker for selected Boolean, uninterpreted-function, and linear-arithmetic proofs | 8-12 weeks |
| General Eunoia checker in MoonBit, reusing CPC signatures | 4-8 months |
| CPC importer using cvc5's internal checker | Needs a prototype before estimating; rule mapping and private API coupling are the main uncertainties |

Any integration must distinguish checking individual steps from establishing the
intended theorem. It must bind proof assumptions to the original problem, require
the expected final contradiction, and handle proof holes explicitly. In the
Ethos revision selected by cvc5 1.3.4, `correct` alone does not guarantee that the
proof concludes `false`. Unsupported cvc5 rules may be exported as `trust` steps
and produce an `incomplete` result. Pin compatible checker and signature versions,
and use trusted signature files rather than accepting arbitrary rule declarations
from a certificate. See the
[pinned Ethos manual](https://github.com/cvc5/ethos/blob/221641668d75eaffd308e0511d63962cea937110/user_manual.md)
and [cvc5 CPC documentation](https://cvc5.github.io/docs/cvc5-1.3.4/proofs/output_cpc.html).