logicaffeine-kernel

A pure Calculus of Constructions type checker (CIC-flavoured: inductive types, fixpoints, pattern matching) plus a set of decision procedures — the small, trusted logical base everything else in the workspace must re-check against.

Part of the Logicaffeine workspace. Tier 1 — depends only on logicaffeine_base. Milner invariant: the kernel has no path to the lexicon, so it never sees English words. Adding vocabulary never recompiles the type checker.

Role in the workspace

The bottom of the proof stack. It is depended on by logicaffeine_compile, logicaffeine_proof, and the web/CLI apps; everything above it (parser, proof search, SMT oracles) is untrusted — it only proposes proof terms the kernel re-checks. See proof and verification for how proposals flow down to this trusted core.

The core insight is that terms, types, and proofs share one syntactic category. Everything is a Term: types (Nat : Type 0), values (zero : Nat), functions (λx:Nat. x), and proofs (refl : a = a).

Public API

use logicaffeine_kernel::{Context, Term, infer_type, is_subtype, normalize};

let ctx = Context::new();
let ty  = infer_type(&ctx, &term)?;        // bidirectional CIC inference
let sub = is_subtype(&ctx, &a, &b);        // cumulative subtyping (bool)
let nf  = normalize(&ctx, &term);          // beta/iota/delta/guarded-fix

Core types

• Term — Sort(Universe), Var, Global, Pi, Lambda, App, Match { discriminant, motive, cases }, Fix { name, body }, Lit(Literal), Hole.
• Universe — Prop | Type(u32). Cumulative: Prop ≤ Type(i), Type(i) ≤ Type(j) iff i ≤ j. Π is impredicative in Prop, so a universally-quantified FOL formula stays a Prop.
• Literal — Int(i64), Float(f64), Text(String), Duration(i64 ns), Date(i32 days), Moment(i64 ns UTC). Opaque; computed via ALU, not recursion.
• Context — typing context. Local bindings grow per binder (extend is an O(1) clone behind Arc); the global env (inductives, constructors + order, declarations/axioms, transparent definitions, auto-tactic hints) is Arc-shared.
• KernelError / KernelResult — unbound variable, type mismatch, non-function/non-type, bad motive / wrong case count, positivity and termination violations, certification errors, un-inferable hole.

Type checking

• infer_type — bidirectional CIC inference.
• is_subtype — cumulative subtyping (returns bool).
• normalize — fuel-limited (default 10000) beta/iota/delta + guarded-fix reduction; evaluates primitive ALU ops (add/sub/mul/div/mod, comparisons, ite) and the reflection builtins (syn_size, syn_max_var, syn_lift, syn_subst, syn_beta, syn_step, syn_eval, syn_quote, syn_diag).

Decision procedures

Each is a pub mod with a Rust entry point on Term (distinct from the prelude-registered try_* tactic terms below):

bitvector exhaustively machine-checks the bit-permutation identities for n = 1..=PROOF_WIDTH (16); edge-distance uniformity of the per-bit transport makes that a proof for all n (memoised via reflection_certificate).

Two algebraic-substrate modules build on ring: field_algebra proves identities over the prime field 𝔽_q of ML-KEM / ML-DSA, and word_ring proves them over the word ring ℤ/2ⁿ (Word8/Word16/Word32/Word64) — both discharged by the kernel's own decision procedures, so the certified-crypto arithmetic never trusts an external algebra system. eval is the call-by-value evaluator for the computational fragment (the engine behind native_decide), distinct from normalize's substitution-based reduction.

Elaboration and recursors

Two modules sit between the surface language and the trusted core: elaborate (R4) is the elaborator — metavariables, unification, and implicit-argument inference, so id 0 elaborates to id Nat 0 before the kernel ever sees it; recursor (R2) auto-derives the dependent eliminator I.rec for an inductive type, the way Lean/Coq generate recursors instead of making the user hand-write match/fix. Both propose terms the trusted checker still re-verifies.

Soundness gates

• positivity::check_positivity — strict positivity of inductives; rejects negative occurrences that would encode Russell's paradox.
• termination::check_termination — Coq-style syntactic guard for fixpoints (structural recursion); rejects fix f. f.

Standard library (prelude)

use logicaffeine_kernel::{prelude::StandardLibrary, Context};
let mut ctx = Context::new();
StandardLibrary::register(&mut ctx);

Installs Entity (FOL domain), Nat, Bool, TList, True, False, Not, Eq, And, Or, Ex, the primitive Int/Float/Text, the commutative-ring axioms for the opaque Int (the entire trusted arithmetic base), the reflection embedding (Syntax, Derivation), hardware ops, and the kernel-level tactic terms try_ring/try_lia/try_cc/try_omega/try_simp plus try_auto (sequencing simp → ring → cc → omega → lia).

Certificates (serde feature) — the De Bruijn criterion

certificate::{Certificate, recheck, PRELUDE_VERSION}, gated on serde. A Certificate carries only proof_term, claimed_type, and prelude_version — never a context. recheck rebuilds the trusted axiom context itself via StandardLibrary::register, infers the term's type, and requires it to be a subtype of the claim, so a certificate cannot smuggle in a bogus axiom (e.g. a free proof of False). The trusted surface of a re-check is this crate plus a JSON parser — no proof search, no SMT. The standalone recheck example reads a JSON certificate from a path:

cargo run -p logicaffeine-kernel --example recheck --features serde -- cert.json

Interface

interface is a vernacular text front-end (TermParser, parse_command/Command, literate_parser, Repl) for driving the kernel by hand — Definition/Check/Eval/Inductive commands and an English-like literate syntax. It builds Terms for the trusted core; it is not part of the trusted surface.

Feature flags

The trusted core stays dependency-free unless certificates are being (de)serialized.

Inductive checkers

The guards that keep user-declared inductive types sound:

• positivity — strict positivity checking for inductive types (no negative self-reference).
• termination — termination / guardedness checking for fixpoints.
• inductive_compile — the nested-inductive compiler (K3): an UNTRUSTED front-end for inductives that recur through other inductives, kernel-rechecked on the way back.

Dependencies

• Internal: logicaffeine-base — the only dependency; supplies UnionFind, re-used by the cc congruence-closure e-graph. No lexicon dependency (Milner invariant).
• External: serde (optional). serde_json is a dev-dependency only — it powers the recheck example and the certificate tests and never enters the published library's dependency graph.

License

Business Source License 1.1 — see LICENSE.md.

Docs index · Root README · Changelog