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>
55 lines
1.6 KiB
C
55 lines
1.6 KiB
C
/* shim.c — expose Lean's static inline runtime helpers as real extern
|
|
* symbols for Rust to link against.
|
|
*
|
|
* Lean 4's `lean_obj_tag` / `lean_ctor_get` / `lean_ctor_set` /
|
|
* `lean_alloc_ctor` / `lean_inc` / `lean_dec` / `lean_string_eq` are
|
|
* all `static inline` in `<lean/lean.h>`. A Rust staticlib that calls
|
|
* them via `extern "C"` produces unresolved references at link time.
|
|
*
|
|
* This shim provides `topolei_shim_*` thin wrappers that invoke the
|
|
* inlines inside a regular C function; the wrappers have real ELF
|
|
* symbols and link cleanly. Zero overhead — the compiler should
|
|
* inline the calls.
|
|
*
|
|
* Compiled by `build.rs` via the `cc` crate. Native targets only;
|
|
* wasm builds don't link against Lean's runtime (Phase D concern).
|
|
*/
|
|
|
|
#include <lean/lean.h>
|
|
#include <stdint.h>
|
|
|
|
uint32_t topolei_shim_obj_tag(b_lean_obj_arg o) {
|
|
return lean_obj_tag(o);
|
|
}
|
|
|
|
lean_obj_res topolei_shim_ctor_get(b_lean_obj_arg o, unsigned i) {
|
|
return lean_ctor_get(o, i);
|
|
}
|
|
|
|
void topolei_shim_ctor_set(lean_object* o, unsigned i, lean_obj_arg v) {
|
|
lean_ctor_set(o, i, v);
|
|
}
|
|
|
|
lean_obj_res topolei_shim_alloc_ctor(unsigned tag, unsigned num_objs, unsigned scalar_sz) {
|
|
return lean_alloc_ctor(tag, num_objs, scalar_sz);
|
|
}
|
|
|
|
void topolei_shim_inc(b_lean_obj_arg o) {
|
|
lean_inc(o);
|
|
}
|
|
|
|
void topolei_shim_dec(b_lean_obj_arg o) {
|
|
lean_dec(o);
|
|
}
|
|
|
|
uint8_t topolei_shim_string_eq(b_lean_obj_arg a, b_lean_obj_arg b) {
|
|
return lean_string_eq(a, b);
|
|
}
|
|
|
|
const char* topolei_shim_string_cstr(b_lean_obj_arg s) {
|
|
return lean_string_cstr(s);
|
|
}
|
|
|
|
lean_obj_res topolei_shim_mk_string(const char* s) {
|
|
return lean_mk_string(s);
|
|
}
|