Module tactic_cert

Expand description

Certificate producers and independent checkers shared with the kernel rechecker.

Structs§

CcCert: A checkable proof that a goal’s conclusion follows from its hypotheses by congruence.
LiaCert: A refutation of a constraint system, as the multipliers that refute it.

CcStep: One step of an equality proof.
CertifiablePrimitive: A tactic reduction primitive a second kernel can now corroborate.
Syn: The object language’s four shapes, as this module reads them.

check_cc: Check a congruence proof against a goal.
check_lia: Check a Farkas certificate against a try_lia goal.
emit_cc: Search for a congruence proof of goal — UNTRUSTED.
emit_lia: Emit a Farkas certificate for a try_lia goal, or None when the search finds none.
syn_apply: SApp f x.
syn_binary: SApp (SApp (SName op) a) b.
syn_of_term: Read a kernel Term as reflected object syntax, or None if it is not one.
syn_typed_eq: SApp (SApp (SApp (SName "Eq") (SName ty)) a) b — the typed equation try_ring reads.
term_of_syn: The same reflected syntax as a kernel Term, so a caller can hand the FIRST kernel exactly the goal it handed this module — which is what makes a differential between the two a differential and not two different questions.
verify_cc: try_cc goal reduces to DccSolve goal, verified from a certificate this module both produced and then checked without reference to how it was produced.
verify_lia: try_lia goal reduces to DLiaSolve goal, verified from a certificate this module both produced and then checked without reference to how it was produced.
verify_ring: try_ring goal reduces to DRingSolve goal, verified here.