/-
  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