oxilean-kernel

The Trusted Computing Base (TCB) of OxiLean

The kernel is the core responsible for type checking in the Calculus of Inductive Constructions (CiC). Only code in this crate needs to be trusted for logical soundness.

Design Principles

Zero external dependencies -- only std is used
No unsafe code -- enforced by #![forbid(unsafe_code)]
113,179 SLOC -- comprehensive implementation
WASM-compatible -- no system calls

Module Overview

Module	Status	Description
`arena.rs`	Implemented	Typed arena allocator with `Idx<T>` index type
`name.rs`	Implemented	Hierarchical names (`Nat.add.comm`) with `name!` macro
`level.rs`	Implemented	Universe levels (`Zero`, `Succ`, `Max`, `IMax`, `Param`)
`expr.rs`	Implemented	Core expression type (11 variants)
`subst.rs`	Implemented	Substitution: `instantiate`, `abstract`, `lift_bvars`
`reduce.rs`	Implemented	WHNF reduction (beta, delta, zeta, iota, projection, quotient)
`infer.rs`	Implemented	Type inference for all `Expr` forms
`def_eq.rs`	Implemented	Definitional equality with proof irrelevance
`check.rs`	Implemented	Declaration checking (Axiom, Definition, Theorem)
`inductive.rs`	Implemented	Inductive types, positivity check, recursor generation
`env.rs`	Implemented	Global environment (declaration storage)
`whnf.rs`	Implemented	Weak head normal form evaluation
`quot.rs`	Implemented	Quotient type support
`builtin.rs`	Implemented	Built-in constant definitions and operations

Core Types

`Arena<T>` & `Idx<T>`

Typed arena allocator. All expression nodes are allocated contiguously for cache-friendly traversal. Idx<T> is a u32-based index with zero-cost PhantomData typing.

let mut arena = Arena::new();
let idx: Idx<MyType> = arena.alloc(value);
let val: &MyType = arena.get(idx);

`Name`

Hierarchical names representing identifiers like Nat.add.comm:

enum Name {
    Anonymous,
    Str(Box<Name>, String),
    Num(Box<Name>, u64),
}
// Convenience macro:
let n = name!("Nat", "add", "comm");  // -> Nat.add.comm

`Level`

Universe levels for the sort hierarchy Prop : Type 0 : Type 1 : ...:

enum Level {
    Zero,                          // 0 (Prop)
    Succ(Box<Level>),              // u + 1
    Max(Box<Level>, Box<Level>),   // max(u, v)
    IMax(Box<Level>, Box<Level>),  // imax(u, v) = 0 if v=0, else max(u,v)
    Param(Name),                   // universe parameter
}

`Expr`

The core expression type -- all terms in the type theory:

Variant	Description	Example
`BVar(u32)`	Bound variable (de Bruijn index)	`#0`, `#1`
`FVar(FVarId)`	Free variable (unique ID)	`x`, `alpha`
`Sort(Level)`	Universe sort	`Prop`, `Type u`
`Const(Name, Vec<Level>)`	Named constant	`Nat.add.{u}`
`App(Box<Expr>, Box<Expr>)`	Application	`f a`
`Lam(BinderInfo, Name, Box<Expr>, Box<Expr>)`	Lambda	`fun (x : T), body`
`Pi(BinderInfo, Name, Box<Expr>, Box<Expr>)`	Pi / forall	`Pi (x : T), body`
`Let(Name, Box<Expr>, Box<Expr>, Box<Expr>)`	Let binding	`let x : T := v in body`
`Lit(Literal)`	Literal	`42`, `"hello"`
`Proj(Name, u32, Box<Expr>)`	Projection	`s.1`

Usage

use oxilean_kernel::{Name, Level, Expr, BinderInfo, Arena, Idx, name};

// Create Prop (Sort 0)
let prop = Expr::Sort(Level::zero());

// Create Type 0 (Sort 1)
let type0 = Expr::Sort(Level::succ(Level::zero()));

// Create identity function type: Pi (alpha : Type 0), alpha -> alpha
let alpha = Name::str("alpha");
let id_type = Expr::Pi(
    BinderInfo::Implicit,
    alpha.clone(),
    Box::new(type0),
    Box::new(Expr::Pi(
        BinderInfo::Default,
        Name::Anonymous,
        Box::new(Expr::BVar(0)),
        Box::new(Expr::BVar(1)),
    )),
);

Testing

cargo test -p oxilean-kernel
cargo test -p oxilean-kernel -- --nocapture  # verbose

oxilean-kernel 0.1.0

oxilean-kernel

Design Principles

Module Overview

Core Types

`Arena<T>` & `Idx<T>`

`Name`

`Level`

`Expr`

Usage

Testing

License

oxilean-kernel 0.1.0

oxilean-kernel

Design Principles

Module Overview

Core Types

Arena<T> & Idx<T>

Name

Level

Expr

Usage

Testing

License

`Arena<T>` & `Idx<T>`

`Name`

`Level`

`Expr`