cubical-transport-hott-lean4/native/cubical/README.md

topolei-cubical — Rust backend

Rust implementation of the cubical-transport HoTT evaluator for topolei — Lean 4's cubical-HoTT kernel extension.

See FFI_DESIGN.md and FFI_COMPLETENESS.md at the project root for the full C ABI contract and per-function axiom audit.

Build

# Native staticlib + cdylib (linux / macos / windows):
cargo build --release

# wasm32-unknown-unknown (for Lean-wasm composite artifacts):
cargo build --release --target wasm32-unknown-unknown

Artifacts:

Target	Path
Native staticlib	target/release/libtopolei_cubical.a
Native cdylib	target/release/libtopolei_cubical.so (linux), .dylib (macos), .dll (windows)
Wasm cdylib	target/wasm32-unknown-unknown/release/topolei_cubical.wasm
Wasm staticlib	target/wasm32-unknown-unknown/release/libtopolei_cubical.a

Discipline

• no_std throughout — wasm32-unknown-unknown has no std, and native uses the same source for ABI uniformity.
• Pure-functional evaluator — no IO, no threads, no allocator. All objects live in Lean's heap; Rust operates via lean_object* pointers.
• Hand-rolled lean_runtime.rs — ~12 extern "C" declarations for the Lean runtime primitives we need. No lean-sys dependency (that crate isn't wasm-ready).

Phase tracker

• Phase A ✅: crate skeleton + stubs.
• Phase B ✅: full evaluator implementation (14 FFI entries).
• Phase C ✅: @[implemented_by] wiring + native staticlib linkage
  • smoke tests (9/9 passing via lake build cubical-test).
• Phase D.wasm ✅: wasm32 target + JS test harness (10/10 passing via node test/wasm_harness.mjs). See WASM.md for integration with a Lean-wasm composite artifact.
• Phase D.properties ✅: 46 property-based tests in CubicalTransport/PropertyTest.lean covering λ β-rules, Σ β-rules, eval determinism, DimExpr idempotence + literals, FaceFormula absorption, readback roundtrip. 55/55 total (9 smoke + 46 property).
• Phase D.bench ✅: baseline perf benchmarks via cubical-bench exe: λ β & Σ projections 11 ns/iter, normalizers ~50 ns/op, readback 11 ns/iter (100k iters, accumulator prevents DCE).

Testing

Two test surfaces, both currently passing:

Native smoke tests (Lean-side)

lake build cubical-test
./.lake/build/bin/cubical-test

Expected output: ── 9 / 9 passed ──, covering λ-fragment eval, Σ β-rules, readback, and normalizer reductions. Source: CubicalTransport/FFITest.lean + CubicalTest.lean.

Wasm smoke tests (Node.js harness)

cargo build --release --target wasm32-unknown-unknown
node test/wasm_harness.mjs

Expected output: ── 10 / 10 tests passed ──. The harness implements a minimal JS version of Lean's runtime (bump allocator + object header helpers) to exercise both scalar and heap-allocating reductions. See WASM.md for the full ABI contract and integration with a Lean-wasm composite artifact.

Layout

native/cubical/
├── Cargo.toml
├── README.md              — this file
├── include/
│   └── topolei_cubical.h  — C declarations (ABI v1)
└── src/
    ├── lib.rs             — crate root; panic handler
    ├── lean_runtime.rs    — hand-rolled Lean C ABI
    └── ffi.rs             — #[no_mangle] exports (stubs in Phase A)

Future expansion (Phases B–C):

└── src/
    ├── cubical/
    │   ├── mod.rs
    │   ├── eval.rs
    │   ├── transport.rs
    │   ├── comp.rs
    │   ├── glue.rs
    │   └── readback.rs
    ├── subst/
    │   ├── mod.rs
    │   ├── dim_expr.rs
    │   └── face.rs
    └── ...