31d19f655e
Some checks are pending
Lean Action CI / build (push) Waiting to run
Restructure to engine-only contents. Application code (Topolei.*
namespace, canvas-rs / render Rust crates, Main / ProbeTest, naga IR
pipeline, Selection / Subobject / Trace / Obs.Ctx hypothesis stack,
cells-spec / HYPOTHESES / STATUS / NAGA_IR_PLAN docs) moves to the
sibling repo max/topolei.
What moved:
- `Topolei/Cubical/*.lean` (22 files) → `CubicalTransport/*.lean`
with namespace `Topolei.Cubical.*` renamed to `CubicalTransport.*`.
Fully-qualified test types `TopoleiCubical{FFI,Property}Test` →
`CubicalTransport{FFI,Property}Test` for consistency.
- New root file `CubicalTransport.lean` re-exporting all 22 modules.
- Lakefile: package `cubicalTransport`; lib `CubicalTransport`; only
`cubical-test` and `cubical-bench` exes (no GPU link path).
The split criterion: anything an AI shortcut could break that would
cascade-corrupt downstream proofs lives here. Anything that would
only break the application stays in the topolei interface repo.
cubical-test passes 62/62 (smoke + properties) on the renamed engine.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
63 lines
2.6 KiB
Text
63 lines
2.6 KiB
Text
/-
|
|
Topolei.Cubical.FFI
|
|
===================
|
|
Documentation + convenience re-exports for the Rust cubical-HoTT
|
|
backend (Phase C, 2026-04-24).
|
|
|
|
## Architecture after Phase C
|
|
|
|
The `@[extern "topolei_cubical_*"]` `opaque` declarations and their
|
|
`@[implemented_by]` attributes are **inlined directly in the files
|
|
that own the fallback `partial def`**:
|
|
|
|
| Function | File where extern + impl_by live |
|
|
|-----------------------|----------------------------------|
|
|
| `eval` | `Cubical/Eval.lean` |
|
|
| `vApp`, `vPApp` | `Cubical/Eval.lean` |
|
|
| `vHCompValue` | `Cubical/Eval.lean` |
|
|
| `vCompAtTerm` | `Cubical/Eval.lean` |
|
|
| `vCompNAtTerm` | `Cubical/Eval.lean` |
|
|
| `vFst`, `vSnd` | `Cubical/Eval.lean` |
|
|
| `vTransp` | `Cubical/Transport.lean` |
|
|
| `readback` | `Cubical/Readback.lean` |
|
|
| `readbackNeu` | `Cubical/Readback.lean` |
|
|
| `DimExpr.normalize` | `Cubical/Interval.lean` |
|
|
| `FaceFormula.normalize` | `Cubical/Face.lean` |
|
|
|
|
**Why inline.** Lean 4 requires `@[implemented_by]` to be attached
|
|
at the declaration site. A central FFI module that tries to
|
|
retroactively attach the attribute to imported declarations fails
|
|
with `Cannot add attribute [implemented_by] to declaration ... in
|
|
an imported module`. The extern declaration and the `partial def`
|
|
must therefore be co-located.
|
|
|
|
This file is kept as a documentation anchor + a place to add any
|
|
future shared FFI utilities that don't belong to a specific
|
|
cubical-core module.
|
|
|
|
## Runtime behaviour
|
|
|
|
When `libtopolei_cubical.a` is linked (default via `lakefile.toml`),
|
|
every runtime call to `eval` / `vApp` / `readback` / etc. routes
|
|
through Rust at native speed. Kernel-level proof reasoning
|
|
continues to go through the axioms in each module — unchanged.
|
|
|
|
Without the Rust library linked, compilation fails at link time
|
|
(every extern symbol is unresolved), so a built executable always
|
|
has Rust present.
|
|
|
|
## ABI version
|
|
|
|
`TOPOLEI_FFI_ABI_VERSION = 1`. Defined in
|
|
`native/cubical/include/topolei_cubical.h`. Any change to an
|
|
`@[extern]` signature (arity, argument types) requires incrementing
|
|
the version and updating the C header.
|
|
|
|
## Related documents
|
|
|
|
- `FFI_DESIGN.md` — C ABI contract (memory, marshalling, ownership).
|
|
- `FFI_COMPLETENESS.md` — per-function axiom-coverage audit.
|
|
- `KERNEL_BOUNDARY.md` — what this delivers vs. what requires kernel work.
|
|
-/
|
|
|
|
import CubicalTransport.Readback
|