c2e3ecb3e3
Some checks are pending
Lean Action CI / build (push) Waiting to run
Implements the cells-spec vision: a computation space that preserves auditability, correctness, interactivity. Phase 1 (Lean kernel + naga-IR Rust backend) is closed; foundation hypothesis stack (Selection H1+H2, Subobject H3, Trace H5, Obs.Ctx C2, Cubical.Trace) landed. Highlights: - Cubical-HoTT syntax + value/eval/readback in Lean - naga-IR pipeline (no GLSL string crosses FFI; 17/17 probes pass) - Honesty audit: every non-transport (sealed cells, vertex shader, Y-flip, presentation conventions) is documented as such - Polymorphic Trace α as free monoid; Cubical.Trace gives CTerm → Trace CTerm by structural fold (homomorphism = definition) - Selection as Huet zipper; Subobject as Boolean algebra over WCell - All theorems proven; the proof IS the implementation See STATUS.md for the resume guide. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
59 lines
2.4 KiB
C
59 lines
2.4 KiB
C
// topolei_cubical.h — C ABI contract for the Rust cubical-HoTT backend.
|
|
//
|
|
// Companion to Topolei/Cubical/FFI.lean (Lean-side extern declarations)
|
|
// and FFI_DESIGN.md (design rationale). Every function below is
|
|
// implemented in native/cubical/src/ffi.rs.
|
|
//
|
|
// ABI version: 1 (increment on any signature change).
|
|
|
|
#pragma once
|
|
#include <lean/lean.h>
|
|
|
|
#define TOPOLEI_FFI_ABI_VERSION 1
|
|
|
|
#ifdef __cplusplus
|
|
extern "C" {
|
|
#endif
|
|
|
|
// ── Evaluator entry points ────────────────────────────────────────────────
|
|
|
|
lean_obj_res topolei_cubical_eval(b_lean_obj_arg env, b_lean_obj_arg t);
|
|
lean_obj_res topolei_cubical_vapp(b_lean_obj_arg f, b_lean_obj_arg a);
|
|
lean_obj_res topolei_cubical_vpapp(b_lean_obj_arg v, b_lean_obj_arg r);
|
|
|
|
lean_obj_res topolei_cubical_vtransp(
|
|
b_lean_obj_arg i, b_lean_obj_arg A,
|
|
b_lean_obj_arg phi, b_lean_obj_arg v);
|
|
|
|
lean_obj_res topolei_cubical_vhcomp(
|
|
b_lean_obj_arg A, b_lean_obj_arg phi,
|
|
b_lean_obj_arg tube, b_lean_obj_arg base);
|
|
|
|
lean_obj_res topolei_cubical_vcomp_term(
|
|
b_lean_obj_arg env, b_lean_obj_arg i, b_lean_obj_arg A,
|
|
b_lean_obj_arg phi, b_lean_obj_arg u, b_lean_obj_arg t);
|
|
|
|
lean_obj_res topolei_cubical_vcompn_term(
|
|
b_lean_obj_arg env, b_lean_obj_arg i, b_lean_obj_arg A,
|
|
b_lean_obj_arg clauses, b_lean_obj_arg t);
|
|
|
|
lean_obj_res topolei_cubical_vfst(b_lean_obj_arg v);
|
|
lean_obj_res topolei_cubical_vsnd(b_lean_obj_arg v);
|
|
|
|
// ── Readback ──────────────────────────────────────────────────────────────
|
|
|
|
lean_obj_res topolei_cubical_readback(b_lean_obj_arg v);
|
|
lean_obj_res topolei_cubical_readback_neu(b_lean_obj_arg n);
|
|
|
|
// ── Step ──────────────────────────────────────────────────────────────────
|
|
|
|
lean_obj_res topolei_cubical_step(b_lean_obj_arg t);
|
|
|
|
// ── Normalisers ───────────────────────────────────────────────────────────
|
|
|
|
lean_obj_res topolei_cubical_dimexpr_normalize(b_lean_obj_arg r);
|
|
lean_obj_res topolei_cubical_face_normalize(b_lean_obj_arg phi);
|
|
|
|
#ifdef __cplusplus
|
|
} // extern "C"
|
|
#endif
|