Skip to main content

Crate oxilean_kernel

Crate oxilean_kernel 

Source
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:

  1. Parser → produces AST (can contain errors/malice)
  2. Elaborator → converts AST to kernel terms (can produce invalid proofs)
  3. 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\

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

§Type Checking Core

ModuleSLOCPurpose
infer~500Type inference
def_eq~400Definitional equality
whnf~300Weak head normal form
check~250Declaration validation

§Reduction & Normalization

ModuleSLOCPurpose
beta~200Beta reduction
eta~150Eta reduction
reduce~200Generic reduction infrastructure
simp~300Simplification engine
normalize~150Full normalization

§Type Families

ModuleSLOCPurpose
inductive~500Inductive types and recursors
quotient~300Quotient types
match_compile~400Pattern match compilation
termination~350Recursion validation

§Utilities

ModuleSLOCPurpose
alpha~200Alpha equivalence
axiom~250Axiom tracking and safety
congruence~300Congruence closure
export~400Module serialization
prettyprint~350Expression printing
trace~200Debug 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:

  1. Type Safety: No expression can be assigned a type that doesn’t logically follow
  2. Axiom Tracking: All uses of axioms are recorded; proofs can be reviewed for axiomatic assumptions
  3. Termination: Recursive definitions are proven terminating before acceptance
  4. Universe Consistency: No universe cycles or level violations
  5. 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

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;
pub use proof_cert::create_certificate;
pub use proof_cert::deserialize_cert;
pub use proof_cert::hash_declaration;
pub use proof_cert::hash_expr;
pub use proof_cert::serialize_cert;
pub use proof_cert::verify_certificate;
pub use proof_cert::CertCheckResult;
pub use proof_cert::CertificateStore;
pub use proof_cert::ProofCertId;
pub use proof_cert::ProofCertificate;
pub use proof_cert::ProofStep;
pub use def_eq_cache::with_cache;
pub use def_eq_cache::CacheEviction;
pub use def_eq_cache::DefEqCache;
pub use def_eq_cache::DefEqCacheStats;
pub use def_eq_cache::DefEqEntry;
pub use def_eq_cache::DefEqKey;
pub use env_index::is_in_namespace;
pub use env_index::namespace_of;
pub use env_index::EnvIndex;
pub use env_index::IndexStats;
pub use env_index::LookupResult;
pub use env_index::ModuleIndex;
pub use env_index::NameIndex;
pub use env_index::TypeIndex;
pub use whnf_memo::hash_bytes;
pub use whnf_memo::with_memo;
pub use whnf_memo::MemoConfig;
pub use whnf_memo::MemoStats;
pub use whnf_memo::WhnfEntry;
pub use whnf_memo::WhnfKey;
pub use whnf_memo::WhnfMemo;
pub use core_types::*;

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
core_types
Auto-generated module structure
declaration
Auto-generated module structure
def_eq
Auto-generated module structure
def_eq_cache
Definitional Equality Cache — memoised results for is_def_eq queries. Definitional Equality Cache for OxiLean Kernel.
env
Auto-generated module structure
env_index
Indexed environment for fast declaration lookup. Indexed environment for fast declaration lookup.
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
hash_cons
Structural sharing (hash-consing) for Expr values. Structural sharing (hash-consing) for Expr values.
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
proof_cert
Proof Certificate System — compact, verifiable records of kernel-checked proofs. Proof Certificate System for OxiLean Kernel.
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
string_intern
Thread-safe string interning pool for Name construction. Thread-safe string interning pool for Name construction.
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
whnf_memo
Memoized WHNF reduction with environment-version-aware cache invalidation. Memoized WHNF reduction with environment-version-aware correctness.

Macros§

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