Theorem Compiler

theoremc is a Rust workspace for compile-time theorem validation via Kani.

Crate layout

Crate	Purpose
theoremc	Root facade — re-exports theoremc-core modules and the theorem_file! proc-macro
theoremc-core	Schema parsing, name mangling, collision detection, and the crate-relative theorem loader
theoremc-macros	The theorem_file! proc-macro implementation

theorem_file! proc-macro

The theorem_file! macro expands a crate-relative .theorem file into a deterministic private module at compile time:

theorem_file!("theorems/my_theorem.theorem");

Invalid theorem files cause the build to fail with an actionable schema diagnostic pointing to the source location of the error.

Programmatic theorem loading

theoremc-core exports load_theorem_file_from_manifest_dir for loading and validating .theorem files outside the proc-macro context:

use camino::Utf8Path;
use theoremc_core::load_theorem_file_from_manifest_dir;

let docs = load_theorem_file_from_manifest_dir(
    Utf8Path::new(env!("CARGO_MANIFEST_DIR")),
    Utf8Path::new("tests/fixtures/my_theorem.theorem"),
)?;

Documentation map

• docs/contents.md indexes the full documentation set.
• docs/users-guide.md covers public API and theorem-file behaviour.
• docs/repository-layout.md explains where code, tests, and durable documentation live.
• docs/developers-guide.md covers maintainer workflows and internal conventions.
• docs/theoremc-design.md records architecture rationale and planned evolution.

Workspace split (since Step 3.2.1)

Before Step 3.2.1, theorem_file! was a macro_rules! bridge in src/lib.rs. The real proc-macro now lives in crates/theoremc-macros, and schema, mangling, and IO logic live in crates/theoremc-core. The root theoremc crate re-exports both. Import paths from theoremc are unchanged.