Crate oxilean_kernel

Expand description

§OxiLean Kernel — Trusted Computing Base

The minimal, auditable kernel implementing the Calculus of Inductive Constructions (CiC) with universe polymorphism. This crate is the trusted core of OxiLean.

§Philosophy

Minimal TCB: Only ~3,500 SLOC need to be trusted for soundness
Zero dependencies: Uses only std (and is no_std-compatible where feasible)
No unsafe: #![forbid(unsafe_code)] ensures memory safety via Rust’s guarantees
Layered trust: Bugs in the parser or elaborator cannot produce unsound proofs
Arena-based memory: All expressions allocated in typed arenas for O(1) equality
WASM-first: Compiles to wasm32-unknown-unknown with no system calls or FFI

§Quick Start

§Creating a Type

use oxilean_kernel::{Expr, Environment, Level};

let env = Environment::new();
// Nat : Type 0
let nat_type = Expr::Sort(Level::Zero);

§Type Checking

use oxilean_kernel::{TypeChecker, KernelError};

let mut checker = TypeChecker::new(&env);
// Type-check an expression
let result = checker.infer(expr)?;

§Architecture Overview

The kernel is organized into three layers:

§Layer 1: Core Data Structures

arena — Typed arena allocator (Arena<T>, Idx<T>)
name — Hierarchical identifiers (Nat.add.comm)
level — Universe levels (Zero, Succ, Max, IMax, Param)
expr — Core AST (11 node types: BVar, FVar, Sort, Const, App, Lam, Pi, Let, Lit, Proj, Rec)

§Layer 2: Environment & Declarations

env — Global environment holding axioms, definitions, inductives, etc.
declaration — Declaration types: Axiom, Def, Theorem, Inductive, Quotient, Recursor, Opaque, Constructor
context — Local variable contexts and context snapshots

§Layer 3: Type Theory Engine

infer — Type inference: infer_type(expr) → Type
def_eq — Definitional equality: is_def_eq(t1, t2) → bool
whnf — Weak head normal form: whnf(expr) → Expr
check — Declaration checking and environment validation

§Layer 4: Reduction & Normalization

beta — β-reduction (function application)
eta — η-reduction (function extensionality)
simp — Simplification using equations
reduce — Generic reducer trait with reducibility hints
normalize — Full normal form computation

§Layer 5: Inductive Types & Recursion

inductive — Inductive type validation and recursor synthesis
match_compile — Pattern matching compilation to decision trees
quotient — Quotient type operations
termination — Structural recursion validation

§Key Concepts & Terminology

§Calculus of Inductive Constructions (CiC)

OxiLean implements a variant of CiC featuring:

Dependent types: Π (x : A), B x (types can depend on values)
Universe polymorphism: Definitions can abstract over type universe levels
Inductive types: Type families with auto-generated recursion principles
Impredicativity: Prop : Prop (proofs of propositions are proof-irrelevant)
Quotient types: Extensional equality for abstract types\

§Trust Boundary

Only the kernel is trusted. External code paths:

Parser → produces AST (can contain errors/malice)
Elaborator → converts AST to kernel terms (can produce invalid proofs)
Kernel → validates every declaration independently (soundness gate)

If parser or elaborator is compromised, users get proof failures, never unsoundness.

§Soundness Properties

Every type-checkable declaration is sound by construction
No unsafe code means memory safety is Rust’s responsibility
Axiom tracking prevents unsound axioms from polluting proofs
Universe polymorphism respects level constraints

§Memory Layout

Expressions live in typed arenas:

Environment
  ├─ expr_arena: Arena<Expr>     // All Expr nodes
  ├─ level_arena: Arena<Level>   // All universe levels
  └─ name_arena: Arena<Name>     // All identifiers

Idx<Expr> = u32 (not a pointer, just an index)
→ O(1) equality via index comparison
→ Cache-friendly dense layout
→ Deterministic, no GC pauses

§Reduction Strategy

WHNF (Weak Head Normal Form): Reduces until top-level constructor
- λ x. t stays as lambda
- App (λ x. t) a reduces to t[a/x]
- Inductive pattern match reduces to branch
Full Normal Form: WHNF + reduce inside binders
Eta-expansion: Insert λ x. f x for functions

§Locally Nameless Representation

Bound variables (inside binders): de Bruijn indices (BVar(0) = innermost binder)
Free variables (global/local): unique IDs (FVar(id))
Converting between: abstract (close over binder), instantiate (substitute FVar)\

§Module Organization

§Foundational Modules\

Module	SLOC	Purpose
`arena`	~150	Typed arena allocator
`name`	~200	Hierarchical names
`level`	~300	Universe level computation
`expr`	~400	Expression AST definition
`subst`	~150	Substitution/instantiation
`context`	~100	Local context management

§Type Checking Core

Module	SLOC	Purpose
`infer`	~500	Type inference
`def_eq`	~400	Definitional equality
`whnf`	~300	Weak head normal form
`check`	~250	Declaration validation

§Reduction & Normalization

Module	SLOC	Purpose
`beta`	~200	Beta reduction
`eta`	~150	Eta reduction
`reduce`	~200	Generic reduction infrastructure
`simp`	~300	Simplification engine
`normalize`	~150	Full normalization

§Type Families

Module	SLOC	Purpose
`inductive`	~500	Inductive types and recursors
`quotient`	~300	Quotient types
`match_compile`	~400	Pattern match compilation
`termination`	~350	Recursion validation

§Utilities

Module	SLOC	Purpose
`alpha`	~200	Alpha equivalence
`axiom`	~250	Axiom tracking and safety
`congruence`	~300	Congruence closure
`export`	~400	Module serialization
`prettyprint`	~350	Expression printing
`trace`	~200	Debug tracing

§Usage Examples

§Example 1: Check if Two Terms Are Definitionally Equal

use oxilean_kernel::{DefEqChecker, Expr};

let checker = DefEqChecker::new(&env);
let eq = checker.is_def_eq(expr1, expr2)?;
assert!(eq);

§Example 2: Normalize an Expression

use oxilean_kernel::normalize;

let normal = normalize(&env, expr)?;
// normal is now in full normal form\

§Example 3: Work with Inductive Types

use oxilean_kernel::{InductiveType, check_inductive};

let nat_ind = InductiveType::new(/* ... */);
check_inductive(&env, &nat_ind)?;
// nat_ind is validated and recursors are synthesized

§Integration with Other Crates

§With `oxilean-meta`

The meta layer (oxilean-meta) extends the kernel with:

Metavariable support: Holes ?m for unification
Meta WHNF: WHNF aware of unsolved metavars
Meta DefEq: Unification that assigns metavars
App builder: Helpers for constructing proof terms

§With `oxilean-elab`

The elaborator (oxilean-elab) uses the kernel for:

Type checking: Validates elaborated proofs via TypeChecker
Definitional equality: Checks is_def_eq during elaboration
Declaration checking: Ensures all definitions are sound

§With `oxilean-parse`

The parser provides surface syntax (Expr types) that the elaborator converts to kernel Expr.

§Soundness Guarantees

OxiLean provides the following soundness invariants:

Type Safety: No expression can be assigned a type that doesn’t logically follow
Axiom Tracking: All uses of axioms are recorded; proofs can be reviewed for axiomatic assumptions
Termination: Recursive definitions are proven terminating before acceptance
Universe Consistency: No universe cycles or level violations
Proof Irrelevance: All proofs of the same Prop are definitionally equal

§Performance Characteristics

Expression comparison: O(1) via arena indexing
WHNF reduction: O(depth × reduction_steps) for typical programs
Environment lookup: O(log n) (indexed environment)
Memory: Dense arena layout, no pointer chasing
GC: None needed (Rust ownership handles deallocation)\

§Further Reading

ARCHITECTURE.md — System architecture
BLUEPRINT.md — Formal CiC specification
Module documentation for specific subcomponents

Re-exports§

pub use arena::Arena;
pub use arena::Idx;
pub use expr::BinderInfo;
pub use expr::Expr;
pub use expr::FVarId;
pub use expr::Literal;
pub use level::Level;
pub use level::LevelMVarId;
pub use name::Name;
pub use subst::abstract_expr;
pub use subst::instantiate;
pub use env::Declaration;
pub use env::EnvError;
pub use env::Environment;
pub use reduce::reduce_nat_op;
pub use reduce::Reducer;
pub use reduce::ReducibilityHint;
pub use declaration::instantiate_level_params;
pub use declaration::AxiomVal;
pub use declaration::ConstantInfo;
pub use declaration::ConstantVal;
pub use declaration::ConstructorVal;
pub use declaration::DefinitionSafety;
pub use declaration::DefinitionVal;
pub use declaration::InductiveVal;
pub use declaration::OpaqueVal;
pub use declaration::QuotKind;
pub use declaration::QuotVal;
pub use declaration::RecursorRule;
pub use declaration::RecursorVal;
pub use declaration::TheoremVal;
pub use equiv_manager::EquivManager;
pub use error::KernelError;
pub use infer::LocalDecl;
pub use infer::TypeChecker;
pub use alpha::alpha_equiv;
pub use alpha::canonicalize;
pub use axiom::classify_axiom;
pub use axiom::extract_axioms;
pub use axiom::has_unsafe_dependencies;
pub use axiom::transitive_axiom_deps;
pub use axiom::AxiomSafety;
pub use axiom::AxiomValidator;
pub use beta::beta_normalize;
pub use beta::beta_step;
pub use beta::beta_under_binder;
pub use beta::is_beta_normal;
pub use beta::mk_beta_redex;
pub use builtin::init_builtin_env;
pub use builtin::is_nat_op;
pub use builtin::is_string_op;
pub use check::check_constant_info;
pub use check::check_constant_infos;
pub use check::check_declaration;
pub use check::check_declarations;
pub use congruence::mk_congr_theorem;
pub use congruence::mk_congr_theorem_with_fixed;
pub use congruence::CongrArgKind;
pub use congruence::CongruenceClosure;
pub use congruence::CongruenceTheorem;
pub use context::ContextSnapshot;
pub use context::NameGenerator;
pub use conversion::ConversionChecker;
pub use def_eq::is_def_eq_simple;
pub use def_eq::DefEqChecker;
pub use eta::eta_contract;
pub use eta::eta_expand;
pub use eta::is_eta_expandable;
pub use export::deserialize_module_header;
pub use export::export_environment;
pub use export::import_module;
pub use export::serialize_module;
pub use export::ExportedModule;
pub use export::ModuleCache;
pub use inductive::check_inductive;
pub use inductive::reduce_recursor;
pub use inductive::InductiveEnv;
pub use inductive::InductiveType;
pub use inductive::IntroRule;
pub use match_compile::CompileResult;
pub use match_compile::ConstructorInfo as MatchConstructorInfo;
pub use match_compile::DecisionTree;
pub use match_compile::MatchArm;
pub use match_compile::MatchCompiler;
pub use match_compile::Pattern;
pub use normalize::alpha_eq_env;
pub use normalize::evaluate;
pub use normalize::is_normal_form;
pub use normalize::normalize_env;
pub use normalize::normalize_whnf;
pub use prettyprint::print_expr;
pub use prettyprint::print_expr_ascii;
pub use prettyprint::ExprPrinter;
pub use proof::ProofTerm;
pub use quotient::check_equivalence_relation;
pub use quotient::check_quot_usage;
pub use quotient::is_quot_type_expr;
pub use quotient::quot_eq;
pub use quotient::reduce_quot_lift;
pub use quotient::QuotUsageKind;
pub use quotient::QuotientType;
pub use simp::alpha_eq;
pub use simp::normalize;
pub use simp::simplify;
pub use termination::ParamInfo;
pub use termination::RecCallInfo;
pub use termination::TerminationChecker;
pub use termination::TerminationResult;
pub use trace::TraceEvent;
pub use trace::TraceLevel;
pub use trace::Tracer;
pub use typeclasses::is_class_constraint;
pub use typeclasses::Instance as KernelInstance;
pub use typeclasses::Method as KernelMethod;
pub use typeclasses::TypeClass as KernelTypeClass;
pub use typeclasses::TypeClassRegistry as KernelTypeClassRegistry;
pub use universe::UnivChecker;
pub use universe::UnivConstraint;
pub use whnf::is_whnf;
pub use whnf::whnf;
pub use whnf::whnf_is_lambda;
pub use whnf::whnf_is_pi;
pub use whnf::whnf_is_sort;

Modules§

abstract: Auto-generated module structure
abstract_interp: Auto-generated module structure
alpha: Auto-generated module structure
arena: Auto-generated module structure
axiom: Auto-generated module structure
bench_support: Benchmarking support utilities for the OxiLean kernel. Auto-generated module structure
beta: Auto-generated module structure
builtin: Auto-generated module structure
cache: Caching infrastructure for performance optimization. Auto-generated module structure
check: Auto-generated module structure
congruence: Auto-generated module structure
context: Auto-generated module structure
conversion: Auto-generated module structure
declaration: Auto-generated module structure
def_eq: Auto-generated module structure
env: Auto-generated module structure
equiv_manager: Auto-generated module structure
error: Auto-generated module structure
eta: Auto-generated module structure
export: Auto-generated module structure
expr: Auto-generated module structure
expr_cache: Auto-generated module structure
expr_util: Auto-generated module structure
ffi: Foreign function interface support. Auto-generated module structure
inductive: Auto-generated module structure
infer: Auto-generated module structure
instantiate: Auto-generated module structure
level: Auto-generated module structure
match_compile: Auto-generated module structure
name: Auto-generated module structure
no_std_compat: No-std compatibility layer for constrained and WASM environments. Auto-generated module structure
normalize: Auto-generated module structure
prettyprint: Auto-generated module structure
proof: Auto-generated module structure
quotient: Auto-generated module structure
reduce: Auto-generated module structure
reduction: Auto-generated module structure
serial: Auto-generated module structure
simp: Auto-generated module structure
struct_eta: Auto-generated module structure
subst: Auto-generated module structure
substitution: Auto-generated module structure
termination: Auto-generated module structure
trace: Auto-generated module structure
type_erasure: Auto-generated module structure
typeclasses: Auto-generated module structure
universe: Auto-generated module structure
whnf: Auto-generated module structure

Macros§

cfg_if_std: Macro that documents what would change in a no_std build.
name: Macro for creating simple string names.

Structs§

ConfigNode: A hierarchical configuration tree.
FlatSubstitution: A flat list of substitution pairs (from, to).
FocusStack: A mutable reference stack for tracking the current “focus” in a tree traversal.
LabelSet: A label set for a graph node.
NonEmptyVec: A non-empty list (at least one element guaranteed).
PathBuf: A reusable scratch buffer for path computations.
RawFnPtr: A type-erased function pointer with arity tracking.
RewriteRule: Represents a rewrite rule lhs → rhs.
RewriteRuleSet: A set of rewrite rules.
SimpleDag: A simple directed acyclic graph.
SlidingSum: A fixed-size sliding window that computes a running sum.
SmallMap: A simple key-value store backed by a sorted Vec for small maps.
SparseVec: A sparse vector: stores only non-default elements.
StackCalc: A simple stack-based calculator for arithmetic expressions.
StatSummary: A generic counter that tracks min/max/sum for statistical summaries.
Stopwatch: A counter that can measure elapsed time between snapshots.
StringPool: A pool of reusable string buffers.
TokenBucket: A token bucket rate limiter.
TransformStat: A pair of StatSummary values tracking before/after a transformation.
TransitiveClosure: A dependency closure builder (transitive closure via BFS).
VersionedRecord: A versioned record that stores a history of values.
WindowIterator: A window iterator that yields overlapping windows of size n.
WriteOnce: A write-once cell.

Enums§

DecisionNode: A simple decision tree node for rule dispatching.
Either2: A tagged union for representing a simple two-case discriminated union.

Constants§

KERNEL_VERSION: Version string for the OxiLean kernel.

Functions§

app_arity: Count the number of arguments an expression is applied to.
build_lam_from_binders: Build a lambda from a list of binders and a body.
build_pi_from_binders: Build a Pi type from a list of binders and an inner type.
collect_const_names: Collect all Const names referenced in an expression.
collect_fvars: Collect all FVar ids referenced in an expression.
collect_literals: Collect all literals occurring in an expression.
const_name: Get the name of a constant, or None if not a constant.
contains_bvar: Check if BVar(idx + depth) occurs in expr at the given depth.
count_apps: Count the number of App nodes in an expression.
count_lam_binders: Count Lam binders in a Lambda-chain.
count_pi_binders: Count Pi binders in a Pi-chain.
count_sorts: Count all sort occurrences in an expression.
expr_head: Return the “head” of an expression (strip App arguments).
expr_size: Compute an approximate “size” of an expression (node count).
has_let_binders: Returns true if an expression contains any Let binders.
has_metavars: Check whether an expression contains any metavariable (MVar).
has_projections: Returns true if an expression contains any projections.
is_app: Check whether an expression is an application.
is_app_of: Check whether an expression is an App whose head is Const(name).
is_closed: Check whether an expression is closed (contains no BVar with index ≥ depth).
is_const: Check whether an expression is a constant.
is_eta_reducible: Check if an expression is eta-reducible at the top level.
is_ground: Check whether an expression contains no FVar, MVar, or BVar nodes.
is_lam: Check whether an expression is a lambda.
is_literal: Check whether an expression is a literal.
is_pi: Check whether an expression is a Pi-type (possibly nested).
is_sort: Check whether an expression is a sort.
kernel_version: Return the kernel version as a (major, minor, patch) tuple.
max_binder_depth: Return the depth of the deepest nested binder.
max_bvar_index: Return the maximum de Bruijn index that appears free (not under enough binders).
mk_app: Convenience: make App(f, a).
mk_app_spine: Build f a1 a2 ... an from a head f and argument list.
mk_lam: Convenience: make a lambda fun x : dom => body.
mk_lam_chain: Build a chain of lambdas from a list of (name, type) binders and a body.
mk_nat_lit: Convenience: make a Nat literal expression.
mk_pi: Convenience: make a Pi-type (x : dom) -> cod.
mk_pi_chain: Build a chain of Pi-types from a list of (name, type) binders and a result type.
mk_prop: Convenience: make a Prop expression (Sort 0).
mk_sort: Convenience: make Sort u for an arbitrary level.
mk_string_lit: Convenience: make a String literal expression.
mk_type0: Convenience: make Type 0 (Sort 1).
mk_type1: Convenience: make Type 1 (Sort 2).
replace_const: Replace all occurrences of a constant by another expression.
strip_lam_binders: Strip outer lambda binders, collecting binder info.
strip_pi_binders: Strip outer Pi binders, collecting binder info.
syntactically_equal: Check if two expressions are syntactically equal (no alpha equivalence, just ==).
unfold_app: Unfold the head and arguments of an App spine.