Below is a Lean 4 FFI spec you can drop into a new repo. It defines a stable C ABI that higher-level runtimes (Go/Rust/Node) can call, and wires it to the Prime Structure/Φ‑Atlas‑12288 core. It also includes a repo layout you can paste into a README.md.
uor-ffi/
├─ README.md
├─ lean-toolchain
├─ lakefile.lean
├─ lean/
│ └─ UOR/
│ ├─ Prime/
│ │ └─ Structure.lean # 48×256 boundary + R96 (core math)
│ ├─ Atlas/
│ │ └─ Core.lean # Φ-Atlas-12288 record instance
│ ├─ FFI/
│ │ └─ CAPI.lean # **Exported** C ABI (this is the spec)
│ └─ Verify/
│ └─ CLI.lean # tiny CLI for local testing
├─ ffi/
│ └─ c/
│ ├─ uor_ffi.h # C header: stable ABI
│ └─ uor_init.c # init shim: Lean runtime + module init
├─ runtime/
│ ├─ go/uorffi/uorffi.go # cgo wrapper (example)
│ ├─ rust/src/lib.rs # Rust FFI wrapper (example)
│ └─ node/
│ ├─ package.json
│ └─ index.ts # Node loader using ffi-napi (example)
├─ pkg/
│ └─ uor-ffi.pc # pkg-config file for link flags (optional)
├─ tests/
│ ├─ ffi/ffi_spec.lean # Lean-side smoke tests
│ └─ c/test_ffi.c # C-side smoke test
└─ .github/
└─ workflows/ci.yml # CI: lake build + smoke tests per runtimeimport Lake
open Lake DSL
package «uor-ffi» where
-- Build as a library that other languages link against.
-- Add more options as needed (optimization, release profile, etc.)
@[default_target]
lean_lib UOR where
-- Root namespace for the Lean library
-- If you split files further, add `globs := #["UOR/*"]`
-- or rely on automatic module discovery.
lean_exe «uor-verify» where
root := `UOR.Verify.CLIIf you already have these modules, keep them; otherwise, this is a self-contained minimal core used by the FFI.
lean/UOR/Prime/Structure.lean
namespace UOR.Prime
/-- Boundary sizes (Prime Structure). -/
def Pages : Nat := 48
def Bytes : Nat := 256
def R96 : Nat := 96
/-- R96 classifier on a raw byte. Returns a number in [0,95]. -/
def classifyByte (b : UInt8) : UInt8 :=
UInt8.ofNat (b.toNat % R96)
end UOR.Primelean/UOR/Atlas/Core.lean
import UOR.Prime.Structure
namespace UOR.Atlas
open UOR.Prime
/-- Φ-Atlas-12288 surface: boundary indices + a trivial Φ. -/
structure Core where
pages : Nat := Pages
bytes : Nat := Bytes
rclasses : Nat := R96
/-- The canonical instance. -/
def phiAtlas12288 : Core := {}
end UOR.AtlasThese are Lean definitions exported as C functions with stable names. Runtimes link against the compiled Lean library and call these functions.
import UOR.Prime.Structure
import UOR.Atlas.Core
namespace UOR.FFI
open UOR.Prime
open UOR.Atlas
/-- ABI version to help gate breaking changes. -/
def abiVersion : UInt32 := 1
/-- Pack (page, byte) as a 32-bit code: (page << 8) | byte. -/
@[inline] def phiEncode (page : UInt8) (byte : UInt8) : UInt32 :=
UInt32.ofNat ((page.toNat <<< 8) + byte.toNat)
/-- Extract page from a 32-bit code, reduced mod 48 for safety. -/
@[inline] def phiPage (code : UInt32) : UInt8 :=
UInt8.ofNat ((code.toNat >>> 8) % Pages)
/-- Extract byte from a 32-bit code (lowest 8 bits). -/
@[inline] def phiByte (code : UInt32) : UInt8 :=
UInt8.ofNat (code.toNat % Bytes)
/-- Truth ≙ conservation: true iff budget is 0. -/
@[inline] def truth (β : UInt32) : Bool := β == 0
/-- Truth addition law: Truth(a + b) ↔ (Truth a ∧ Truth b) — exposed as a predicate. -/
@[inline] def truthAdd (a b : UInt32) : Bool := (a + b == 0)
/-! ### EXPORTS (C ABI)
All exported symbols are prefixed `lean_` to align with Lean's default toolchain conventions.
-/
/-- ABI version. -/
@[export lean_uor_abi_version]
def c_abiVersion : UInt32 := abiVersion
/-- Constants (Pages, Bytes, R96). -/
@[export lean_uor_pages] def c_pages : UInt32 := UInt32.ofNat Pages
@[export lean_uor_bytes] def c_bytes : UInt32 := UInt32.ofNat Bytes
@[export lean_uor_rclasses] def c_rclasses : UInt32 := UInt32.ofNat R96
/-- R96 classifier: byte → class in [0,95]. -/
@[export lean_uor_r96_classify]
def c_r96 (b : @& UInt8) : UInt8 := classifyByte b
/-- Pack/unpack boundary codes. -/
@[export lean_uor_phi_encode]
def c_phiEncode (page : @& UInt8) (byte : @& UInt8) : UInt32 := phiEncode page byte
@[export lean_uor_phi_page]
def c_phiPage (code : @& UInt32) : UInt8 := phiPage code
@[export lean_uor_phi_byte]
def c_phiByte (code : @& UInt32) : UInt8 := phiByte code
/-- Truth & budget helpers. -/
@[export lean_uor_truth_zero]
def c_truthZero (β : @& UInt32) : UInt8 := if truth β then (1 : UInt8) else 0
@[export lean_uor_truth_add]
def c_truthAdd (a : @& UInt32) (b : @& UInt32) : UInt8 :=
if truthAdd a b then (1 : UInt8) else 0
end UOR.FFI#ifndef UOR_FFI_H
#define UOR_FFI_H
#include <stdint.h>
#include <stddef.h>
#ifdef __cplusplus
extern "C" {
#endif
/* ABI version: bump on breaking changes to signatures/semantics */
#define UOR_FFI_ABI_VERSION 1
/* Initialization helpers
Call `lean_initialize_uor` once before using any other symbol.
Call `lean_finalize_uor` at process shutdown (optional but recommended).
*/
void lean_initialize_uor(uintptr_t resv);
void lean_finalize_uor(void);
/* Constants: Prime Structure dimensions */
uint32_t lean_uor_abi_version(void); /* == UOR_FFI_ABI_VERSION */
uint32_t lean_uor_pages(void); /* 48 */
uint32_t lean_uor_bytes(void); /* 256 */
uint32_t lean_uor_rclasses(void); /* 96 */
/* R96 classifier: returns a value in [0,95] */
uint8_t lean_uor_r96_classify(uint8_t b);
/* Φ boundary pack/unpack */
uint32_t lean_uor_phi_encode(uint8_t page, uint8_t byte);
uint8_t lean_uor_phi_page(uint32_t code); /* modulo 48 */
uint8_t lean_uor_phi_byte(uint32_t code); /* low 8 bits */
/* Truth ≙ conservation helpers (boolean results returned as 0/1) */
uint8_t lean_uor_truth_zero(uint32_t budget);
uint8_t lean_uor_truth_add(uint32_t a, uint32_t b);
#ifdef __cplusplus
}
#endif
#endif /* UOR_FFI_H */This bridges the Lean runtime and the module initializer generated for UOR when you compile with Lake.
#include <stdint.h>
#include <lean/lean.h>
/* These are generated by Lean for each module you build. */
extern void initialize_UOR_Prime_Structure(uintptr_t);
extern void initialize_UOR_Atlas_Core(uintptr_t);
extern void initialize_UOR_FFI_CAPI(uintptr_t);
void lean_initialize_uor(uintptr_t resv) {
lean_initialize_runtime_module();
initialize_UOR_Prime_Structure(resv);
initialize_UOR_Atlas_Core(resv);
initialize_UOR_FFI_CAPI(resv);
}
void lean_finalize_uor(void) {
lean_finalize_runtime_module();
}package uorffi
/*
#cgo CFLAGS: -I../../ffi/c
#cgo LDFLAGS: -L${SRCDIR}/../../../.lake/build/lib -lUOR -lLean
#include "uor_ffi.h"
*/
import "C"
import "sync"
var initOnce sync.Once
func Init() { initOnce.Do(func() { C.lean_initialize_uor(0) }) }
func AbiVersion() uint32 { Init(); return uint32(C.lean_uor_abi_version()) }
func Pages() uint32 { Init(); return uint32(C.lean_uor_pages()) }
func Bytes() uint32 { Init(); return uint32(C.lean_uor_bytes()) }
func RClasses() uint32 { Init(); return uint32(C.lean_uor_rclasses()) }
func R96(b byte) byte { Init(); return byte(C.lean_uor_r96_classify(C.uchar(b))) }
func PhiEncode(page, by byte) uint32 { Init(); return uint32(C.lean_uor_phi_encode(C.uchar(page), C.uchar(by))) }
func PhiPage(code uint32) byte { Init(); return byte(C.lean_uor_phi_page(C.uint(code))) }
func PhiByte(code uint32) byte { Init(); return byte(C.lean_uor_phi_byte(C.uint(code))) }
func TruthZero(budget uint32) bool { Init(); return C.lean_uor_truth_zero(C.uint(budget)) == 1 }
func TruthAdd(a, b uint32) bool { Init(); return C.lean_uor_truth_add(C.uint(a), C.uint(b)) == 1 }#[link(name = "UOR")] // produced by Lake under .lake/build/lib
extern "C" {
fn lean_initialize_uor(resv: usize);
fn lean_uor_abi_version() -> u32;
fn lean_uor_pages() -> u32;
fn lean_uor_bytes() -> u32;
fn lean_uor_rclasses() -> u32;
fn lean_uor_r96_classify(b: u8) -> u8;
fn lean_uor_phi_encode(page: u8, byte: u8) -> u32;
fn lean_uor_phi_page(code: u32) -> u8;
fn lean_uor_phi_byte(code: u32) -> u8;
fn lean_uor_truth_zero(budget: u32) -> u8;
fn lean_uor_truth_add(a: u32, b: u32) -> u8;
}
static INIT: std::sync::Once = std::sync::Once::new();
fn init() { INIT.call_once(|| unsafe { lean_initialize_uor(0) }); }
pub fn abi_version() -> u32 { init(); unsafe { lean_uor_abi_version() } }
pub fn pages() -> u32 { init(); unsafe { lean_uor_pages() } }
pub fn bytes() -> u32 { init(); unsafe { lean_uor_bytes() } }
pub fn rclasses() -> u32 { init(); unsafe { lean_uor_rclasses() } }
pub fn r96(b: u8) -> u8 { init(); unsafe { lean_uor_r96_classify(b) } }
pub fn phi_encode(p: u8, b: u8) -> u32 { init(); unsafe { lean_uor_phi_encode(p, b) } }
pub fn phi_page(code: u32) -> u8 { init(); unsafe { lean_uor_phi_page(code) } }
pub fn phi_byte(code: u32) -> u8 { init(); unsafe { lean_uor_phi_byte(code) } }
pub fn truth_zero(budget: u32) -> bool { init(); unsafe { lean_uor_truth_zero(budget) == 1 } }
pub fn truth_add(a: u32, b: u32) -> bool { init(); unsafe { lean_uor_truth_add(a, b) == 1 } }Uses
ffi-napi(ornode-ffi) to call into the shared library produced by Lake.
import ffi from 'ffi-napi';
import path from 'path';
const libPath = path.resolve(__dirname, '../../.lake/build/lib'); // adjust
const uor = ffi.Library(path.join(libPath, process.platform === 'win32' ? 'UOR.dll' : 'libUOR'), {
'lean_initialize_uor': [ 'void', ['ulong'] ],
'lean_uor_abi_version': [ 'uint', [] ],
'lean_uor_pages': [ 'uint', [] ],
'lean_uor_bytes': [ 'uint', [] ],
'lean_uor_rclasses': [ 'uint', [] ],
'lean_uor_r96_classify': [ 'uchar', ['uchar'] ],
'lean_uor_phi_encode': [ 'uint', ['uchar', 'uchar'] ],
'lean_uor_phi_page': [ 'uchar', ['uint'] ],
'lean_uor_phi_byte': [ 'uchar', ['uint'] ],
'lean_uor_truth_zero': [ 'uchar', ['uint'] ],
'lean_uor_truth_add': [ 'uchar', ['uint', 'uint'] ],
});
uor.lean_initialize_uor(0);
export const AbiVersion = () => uor.lean_uor_abi_version();
export const Pages = () => uor.lean_uor_pages();
export const Bytes = () => uor.lean_uor_bytes();
export const RClasses = () => uor.lean_uor_rclasses();
export const R96 = (b: number) => uor.lean_uor_r96_classify(b);
export const PhiEncode = (p: number, b: number) => uor.lean_uor_phi_encode(p, b);
export const PhiPage = (code: number) => uor.lean_uor_phi_page(code);
export const PhiByte = (code: number) => uor.lean_uor_phi_byte(code);
export const TruthZero = (budget: number) => uor.lean_uor_truth_zero(budget) === 1;
export const TruthAdd = (a: number, b: number) => uor.lean_uor_truth_add(a, b) === 1;import UOR.FFI.CAPI
open UOR.FFI
def main (_args : List String) : IO UInt32 := do
-- Smoke-test the exported functions without leaving Lean.
let ok1 := (c_pages == 48) && (c_bytes == 256) && (c_rclasses == 96)
let ok2 := (c_r96 0xFF) ≤ 95
let code := c_phiEncode 3 0x10
let pg := c_phiPage code
let by := c_phiByte code
let ok3 := (pg == 3) && (by == 0x10)
let ok4 := (c_truthZero 0 == 1) && (c_truthAdd 0 0 == 1) && (c_truthAdd 1 0 == 0)
pure (if ok1 && ok2 && ok3 && ok4 then 0 else 1)#include <stdio.h>
#include <assert.h>
#include "ffi/c/uor_ffi.h"
int main(void) {
lean_initialize_uor(0);
assert(lean_uor_abi_version() == UOR_FFI_ABI_VERSION);
assert(lean_uor_pages() == 48);
assert(lean_uor_bytes() == 256);
assert(lean_uor_rclasses() == 96);
assert(lean_uor_r96_classify(255) < 96);
uint32_t code = lean_uor_phi_encode(3, 0x10);
assert(lean_uor_phi_page(code) == 3);
assert(lean_uor_phi_byte(code) == 0x10);
assert(lean_uor_truth_zero(0) == 1);
assert(lean_uor_truth_add(0, 0) == 1);
puts("OK");
return 0;
}# 1) Build Lean library + CLI
lake build
# Artifacts usually land under: .lake/build/lib (libUOR.{a,so,dylib})
# 2) C smoke test build (example)
cc -Iffi/c -L.lake/build/lib tests/c/test_ffi.c -o tests/c/test_ffi \
-lUOR -lLean -lpthread -ldl
# 3) Run CLI (exit code 0 ⇒ success)
.lake/build/bin/uor-verify ; echo $?
# 4) Run C smoke test
./tests/c/test_ffilean_uor_pages/bytes/rclasses: authoritative constants from the Prime Structure (48/256/96).lean_uor_r96_classify(b): canonical R96 class of a byteb(resonance class in[0,95]).lean_uor_phi_encode(p, b): packs boundary address (page, byte) into a 32‑bit code(p << 8) | b.lean_uor_phi_page/phi_byte(code): inverse projections; page is returned mod 48.lean_uor_truth_zero(budget): 1 iff budget is 0.lean_uor_truth_add(a, b): 1 iffa + b == 0(the “truth ≙ conservation” check at the boundary).
This gives you a stable, language‑neutral surface to integrate PrimeOS/Hologram invariants while keeping the math authoritative in Lean. If you want to add more invariants later (e.g., window admission or conformance checks), bump UOR_FFI_ABI_VERSION and extend CAPI.lean with new @[export] functions.