Module tactic_cert 

Independent verification of reflected ring, linear-arithmetic, and congruence goals.

The second kernel uses these checks for tactic computations and their derivation conclusions. Linear arithmetic and congruence emit certificates and replay them; ring uses exact Kronecker substitution rather than polynomial normalization. None calls the first kernel’s arithmetic engines or reflected-syntax reader.

A successful check corroborates the primitive’s success constructor. Failure means the independent checker has no verdict; it never licenses an error reduction. The proof crate re-exports this module for certificate producers and clients.

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.

Enums

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.

Functions

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.