8561e19467
Some checks are pending
Lean Action CI / build (push) Waiting to run
- TRANSPORT_PLAN.md → PHASE1_HISTORY.md with archival header. Path references updated from `Topolei/Cubical/*` to `CubicalTransport/*` to match the post-split namespace. Methodology preserved as a template for future formalisation phases. - ZIGZAG_PORT.md moved here from topolei. This is engine code: the port lands in `CubicalTransport/Zigzag/`, and an AI shortcut on normalisation, degeneracy, or signature-typechecking would cascade-corrupt every higher-cell proof in topolei. Added a cascade caveat header explaining how engine-level zigzag changes ripple back into the topolei interface repo. Body updated for split context. - KERNEL_BOUNDARY.md: clarified that the planned `Eq ↔ Path` bridge module is distinct from the existing trace bridge (`Topolei/Cubical/Trace.lean` in topolei). - README.md: refreshed Reference section with renames + new docs. - native/cubical/README.md: path refs updated. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
114 lines
3.7 KiB
Markdown
114 lines
3.7 KiB
Markdown
# 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
|
||
└── ...
|
||
```
|