# topolei-cubical — Rust backend

Rust implementation of the cubical-transport HoTT evaluator for
[topolei](../../README.md) — 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

```sh
# 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)

```sh
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)

```sh
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
    └── ...
```