Module recheck 

R1 — an independent proof-term re-checker (the de Bruijn criterion taken seriously).

The kernel’s infer_type is the entire trust base. This module is a SECOND, deliberately separate implementation of the CIC type checker: trust then rests on two small independent kernels agreeing, not on one. For the independence to be meaningful the two must not share their checking logic — so this re-checker uses a DIFFERENT term representation (de Bruijn indices, no names) with its own reduction and its own cumulative conversion. A variable-capture or substitution bug in the main kernel’s name-based machinery would surface here as a type error rather than slipping through identically — Logos’s analog of lean4checker/nanoda.

Scope: the CIC logical core — Sort/Var/Global/Pi/Lambda/App/Lit (incl. BigInt/Nat literal arithmetic and the Nat↔Peano bridge) with β/ι/ζ/δ-reduction and cumulative conversion — PLUS the inductive eliminator Match (coverage, per-constructor case typing via de Bruijn telescope instantiation, ι-reduction, large-elimination restriction) AND both single (Fix) and MUTUAL (MutualFix) fixpoints, each with an INDEPENDENT structural-termination guard. Transparent definitions ARE δ-unfolded during whnf; only axioms/constructors/inductives stay opaque. The only fragment reported HONESTLY as ReCheckError::Unsupported — rather than silently passed — is Hole (an unelaborated metavariable) and a match on an inductive this checker cannot resolve: such a proof is single-checked by the main kernel and double_check says so. The re-checker never reports a term as independently verified unless it actually verified every part of it.

Enums

DoubleCheck

The verdict of cross-checking a term with BOTH kernels.

ReCheckError

Why the re-checker could not produce a verdict, split by soundness meaning.

Functions

double_check

Cross-check term against both infer_type and recheck.

recheck

Independently re-check term in ctx, returning its inferred type on success.