Crate logicaffeine_kernel

Expand description

§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):

Module	Proves	Entry point
`ring`	polynomial equalities	`reify` → `Polynomial::canonical_eq`
`lia`	linear inequalities (Fourier–Motzkin over ℚ)	`fourier_motzkin_unsat`
`omega`	exact integer arithmetic (discrete, GCD-normalized)	`omega_unsat`
`cc`	congruence closure over uninterpreted functions	`check_goal`
`simp`	rewriting / constant folding (fuel-limited)	`check_goal`
`bitvector`	reflection-symmetry identities (N-Queens)	`reflection_symmetry_proven`

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

Feature	Default	Effect
`serde`	off	derives `Serialize`/`Deserialize` on `Term`/`Literal`/`Universe` and compiles the `certificate` module + `recheck` example for proof-certificate (de)serialization

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

Re-exports§

pub use inductive_compile::NestedDecl;
pub use inductive_compile::NestedInfo;
pub use eval::eval_bool;
pub use eval::eval_bool_tree;
pub use eval::native_compile_bool;
pub use eval::native_compile_decide;
pub use eval::native_decide;
pub use elaborate::auto_bind_implicits;
pub use elaborate::bind_self_recursion;
pub use elaborate::elaborate;
pub use elaborate::elaborate_app;
pub use elaborate::elaborate_app_against;
pub use elaborate::elaborate_anon_ctor;
pub use elaborate::elaborate_dot;
pub use elaborate::elaborate_in;
pub use elaborate::fill_match_motives;
pub use elaborate::instantiate;
pub use elaborate::resolve_coercion;
pub use elaborate::resolve_instance;
pub use elaborate::surface_elaborate;
pub use elaborate::surface_elaborate_against;
pub use elaborate::unify;
pub use elaborate::unify_in;
pub use elaborate::MetaCtx;
pub use elaborate::ParamKind;
pub use elaborate::ANON_CTOR_MARKER;
pub use elaborate::DOT_MARKER;
pub use recheck::double_check;
pub use recheck::recheck;
pub use recheck::DoubleCheck;
pub use recheck::ReCheckError;
pub use recursor::derive_recursor;
pub use reify::VarInterner;

Modules§

bitvector: Bitvector reflection-symmetry decision procedure.
cc: Congruence Closure Tactic
elaborate: R4 — the elaborator: metavariables, unification, and implicit-argument inference.
eval: A call-by-value evaluator for the kernel’s computational fragment — the engine behind native_decide.
field_algebra: Kernel algebra for the prime field 𝔽_q of ML-KEM / ML-DSA — the certified arithmetic substrate (F2 seed).
inductive_compile: Nested-inductive compiler (K3) — the UNTRUSTED front-end for inductives that recur nested inside a container, RTree := rnode : TList RTree → RTree.
interface: Vernacular interface for the Kernel.
lia: Linear Integer Arithmetic via Fourier-Motzkin Elimination
omega: Omega Test: True Integer Arithmetic Decision Procedure
positivity: Strict positivity checking for inductive types.
prelude: Standard Library for the Kernel.
recheck: R1 — an independent proof-term re-checker (the de Bruijn criterion taken seriously).
recursor: R2 — auto-derived recursors (dependent eliminators) for inductive types.
reify: Shared reification substrate for the arithmetic decision procedures.
ring: Ring Tactic: Polynomial Equality by Normalization
simp: Simplifier Tactic
termination: Termination checking for fixpoints.
word_ring: Kernel ring proofs for the word ring ℤ/2ⁿ (Word8/Word16/Word32/Word64).

Structs§

BigInt: An exact, arbitrary-precision integer.
Context: Typing context: maps variable names to their types.
MutualInductive: One member of a MUTUAL inductive block: its name, arity sort, uniform parameter count, and constructors (name + full type). Constructor types may reference ANY member of the block — that is the whole point of a mutual declaration.
StructInfo: Metadata for a registered structure (record): its single constructor, how many leading type PARAMETERS it takes, and the projection function names in field order.

Enums§

KernelError: Errors that can occur during type checking.
Literal: Primitive literal values.
Term: Unified term representation.
Universe: Universe levels in the type hierarchy — a level EXPRESSION, so the kernel can be universe-POLYMORPHIC (R3). The concrete hierarchy is Prop : Type 1 : Type 2 : … with Prop ≤ Type i; on top of it, a level may mention universe VARIABLES, so one definition (id.{u} : Π(A : Sort u). A → A) is reusable at every level instead of duplicated per level.

Functions§

check_positivity_for_test: Strict-positivity check of a constructor type — exposed so tests can pin the paradox fence (negative occurrences rejected, positive functional fields accepted) directly.
defeq_for_test: Definitional equality of two terms — exposed for tests that pin conversion behaviour (structure eta, proof irrelevance) directly.
infer_type: Infer the type of a term in a context.
instantiate_universes: Instantiate universe variables throughout a term: substitute every Sort’s level by subst. This specializes a universe-POLYMORPHIC term (λA:Sort u. …) to a concrete level (u := Type 0), yielding an ordinary term the kernel checks as-is — so one definition is reused at every level instead of duplicated.
int_lit: The canonical Literal for an integer: Int(i64) when it fits (the fast, common path), otherwise the arbitrary-precision BigInt. This is the ONLY sanctioned way to build an integer literal from a BigInt result, guaranteeing the one-representation-per-value invariant on which definitional equality of literals rests.
is_subtype: Check if type a is a subtype of type b (cumulativity).
lit_bigint: The BigInt value of an integer literal, promoting a machine Int — for arithmetic that must run in arbitrary precision. None for non-integer literals.
normalize: Normalize a term to its normal form.

Type Aliases§

KernelResult: Result type for kernel operations.