Module extraction 

Program extraction from kernel terms to Rust.

This module compiles verified kernel terms into executable Rust source code.

Extraction Rules

Kernel Term	Rust Output
Inductive	enum Name { Ctor(Args...) }
Fix + Lambdas	fn name(args) -> Ret { body }
Match	match disc { Name::Ctor(vars) => body }
App	func(arg)

Structural Honesty

We extract types exactly as defined, with no optimization. For example, Nat becomes enum Nat { Zero, Succ(Box<Nat>) }. This guarantees that the extracted code is isomorphic to the verified logic.

Modules

fol_model

FOL → runnable Rust model-checker / temporal monitor.

verilog

Verilog Extraction: Kernel Term → SystemVerilog

Enums

ExtractError

Errors that can occur during extraction.

Functions

emit_property_check

Emit a runnable property check fn check_<name>(params) -> bool { … } from a theorem’s PROPOSITION (its kernel type), or None if the statement isn’t a finite, executable property over extractable functions. A proven theorem like ∀n. Eq Nat (add Zero n) n becomes fn check_…(n: Nat) -> bool { add(Nat::Zero, n) == n }.

emit_value

Emit a (normalized) data-value Term as a Rust expression — used by the self-verifying demo main to write the kernel-computed expected result.

extract_program

Extract a program rooted at the given entry point.

extract_programs

Extract a program rooted at several entry points into one Rust module.

is_extractable

Whether name extracts to self-contained Rust: a constructor of an emittable inductive, an emittable inductive (has constructors) or mapped primitive, or a definition whose body only references extractable things. Axioms / declarations / tactics (no extractable body, e.g. syn_diag, try_auto) are NOT extractable — extracting them would emit Rust referencing undefined symbols.

is_logical_type

StandardLibrary types that encode logic/proof/reflection rather than user data (Syntax ASTs, Eq/And/Ex propositions, Derivation proofs, …). Values of these are not the “compile my data to Rust” use case and don’t extract cleanly, so definitions over them are left as a note instead of emitting broken Rust.

primitive_rust_type

The canonical kernel-primitive → Rust-type bridge: the SINGLE source of truth for how the seven opaque kernel primitives lower to Rust. Both the extractor and any caller that reasons about extractable types consult this, so they can never disagree on a primitive’s Rust type — the soundness contract that lets imperative code call a bundled proven function over primitives. None means the name is not a primitive (it may still be a user inductive or a generic type variable). These are registered in the StandardLibrary as constructorless inductives, so they have no enum form and are represented directly by their Rust counterpart.