50bb6660d6
Some checks are pending
Lean Action CI / build (push) Waiting to run
Typing.lean: minimal-viable typing rules for the three new CTerm
constructors (REL1 first cut; REL2 will refine to dependent
formulations).
- HasType.ctor : .ctor S c params args : .ind S params
(no per-arg premises; runtime enforces)
- HasType.indElim : non-dependent form — motive : .pi (.ind …) C,
result : C; branch coherence checked at eval
- HasType.dimExpr : placeholder typing at .univ (real interval-
typing requires a CType.interval primitive,
deferred to REL2)
HasType.weaken_core extended with the three new arms.
TransportLaws.lean: derived theorems for transport over .ind (T1,
T2, stuck), all reducing to existing axioms (eval_transp_top,
eval_transp_const, eval_transp_nonpath + vTransp_stuck). Pointwise
distribution through ctor args is REL1.1 future work.
CompLaws.lean: derived theorems for composition over .ind (C1, C2,
const-line, stuck) — corollaries of the existing eval_comp_*
axioms. Same REL1.1 deferral for pointwise distribution.
native/cubical/src/subst.rs: critical Rust fix. The previous
fallback `_ => mk_term_var(ctor_field(t, 0))` corrupted the new
TERM_DIMEXPR / TERM_CTOR / TERM_INDELIM tags by extracting field 0
(a CTypeSchema for ctor) and wrapping it as a malformed .var,
causing infinite recursion / OOM in subst-driven paths
(eval_comp_top calls substDim). Proper arms for all three new
tags + cterm_subst_dim_list and cterm_subst_dim_branches helpers.
Unknown-tag fallback now safely returns the input unchanged
instead of synthesising a malformed .var.
FFITest.lean: three new smoke arms exercising T1/T2 transport and
C1 composition over .ind natC. Result: 28/28 smoke + 46/46
properties = 74/74.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
206 lines
8.6 KiB
Text
206 lines
8.6 KiB
Text
/-
|
||
Topolei.Cubical.FFITest
|
||
=======================
|
||
Phase C.3 smoke test (2026-04-24). Exercises the FFI wiring by
|
||
running simple cubical terms through `eval` / `readback` / the
|
||
normalizers. With `@[implemented_by]` attached, these execute in
|
||
the Rust backend at runtime.
|
||
|
||
**Why not `#eval`?** `#eval` runs at Lean's compile-time in the
|
||
interpreter, which does not link our Rust staticlib. Calling a
|
||
Rust-backed function under the interpreter raises "Could not find
|
||
native implementation of external declaration ..." The tests here
|
||
are `def`s + a `runSmokeTests : IO Unit` entry point that exercises
|
||
them inside a compiled binary where Rust IS linked.
|
||
|
||
Invoke from a compiled executable. `Main.lean` can optionally
|
||
route to `CubicalTransportFFITest.runSmokeTests` when passed
|
||
`--cubical-test`. Or a dedicated test exe target.
|
||
-/
|
||
|
||
import CubicalTransport.Readback
|
||
import CubicalTransport.FFI
|
||
import CubicalTransport.Inductive
|
||
|
||
open CubicalTransport.Inductive
|
||
open CubicalTransport.Inductive.CTerm
|
||
|
||
namespace CubicalTransportFFITest
|
||
|
||
-- ── Summarisers ────────────────────────────────────────────────────────────
|
||
|
||
def cvalSummary : CVal → String
|
||
| .vneu (.nvar s) => s!"vneu nvar {s}"
|
||
| .vneu (.napp _ _) => "vneu napp"
|
||
| .vneu (.npapp _ _) => "vneu npapp"
|
||
| .vneu (.ntransp _ _ _ _) => "vneu ntransp"
|
||
| .vneu (.nhcomp _ _ _ _) => "vneu nhcomp"
|
||
| .vneu (.ncomp _ _ _ _ _) => "vneu ncomp"
|
||
| .vneu (.ncompN _ _ _ _ _) => "vneu ncompN"
|
||
| .vneu (.nglueIn _ _ _) => "vneu nglueIn"
|
||
| .vneu (.nunglue _ _ _) => "vneu nunglue"
|
||
| .vneu (.nfst _) => "vneu nfst"
|
||
| .vneu (.nsnd _) => "vneu nsnd"
|
||
| .vneu (.nIndElim _ _ _ _ _) => "vneu nIndElim"
|
||
| .vlam _ x _ => s!"vlam {x} ..."
|
||
| .vplam _ i _ => s!"vplam {i.name} ..."
|
||
| .vpair _ _ => "vpair ..."
|
||
| .vTranspFun _ _ _ _ _ => "vTranspFun"
|
||
| .vHCompFun _ _ _ _ => "vHCompFun"
|
||
| .vCompFun _ _ _ _ _ _ _ => "vCompFun"
|
||
| .vTubeApp _ _ => "vTubeApp"
|
||
| .vPathTransp _ _ _ _ _ _ _ => "vPathTransp"
|
||
| .vctor _ c _ _ => s!"vctor {c} ..."
|
||
| .vdimExpr _ => "vdimExpr ..."
|
||
|
||
def ctermSummary : CTerm → String
|
||
| .var x => s!"var {x}"
|
||
| .lam x _ => s!"lam {x} ..."
|
||
| .app _ _ => "app ..."
|
||
| .plam i _ => s!"plam {i.name} ..."
|
||
| .pair _ _ => "pair ..."
|
||
| .fst _ => "fst ..."
|
||
| .snd _ => "snd ..."
|
||
| .dimExpr _ => "dimExpr ..."
|
||
| .ctor _ c _ _ => s!"ctor {c} ..."
|
||
| .indElim _ _ _ _ _ => "indElim ..."
|
||
| _ => "<other CTerm>"
|
||
|
||
-- ── Individual test definitions ────────────────────────────────────────────
|
||
-- Each returns (description, actual, expected) for runSmokeTests to print.
|
||
|
||
def tests : List (String × String × String) :=
|
||
[ ("eval .nil (.var \"x\")",
|
||
cvalSummary (eval .nil (.var "x")),
|
||
"vneu nvar x"),
|
||
("eval .nil (.lam \"x\" (.var \"x\"))",
|
||
cvalSummary (eval .nil (.lam "x" (.var "x"))),
|
||
"vlam x ..."),
|
||
("(λx. x) y ⇓ y",
|
||
cvalSummary (eval .nil (.app (.lam "x" (.var "x")) (.var "y"))),
|
||
"vneu nvar y"),
|
||
("(a, b).fst ⇓ a",
|
||
cvalSummary (eval .nil (.fst (.pair (.var "a") (.var "b")))),
|
||
"vneu nvar a"),
|
||
("(a, b).snd ⇓ b",
|
||
cvalSummary (eval .nil (.snd (.pair (.var "a") (.var "b")))),
|
||
"vneu nvar b"),
|
||
("readback (eval .nil (.lam \"x\" (.var \"x\"))) ≡ .lam \"x\" ...",
|
||
ctermSummary (readback (eval .nil (.lam "x" (.var "x")))),
|
||
"lam x ..."),
|
||
("DimExpr.normalize (.inv .zero) ≡ .one",
|
||
match DimExpr.normalize (.inv .zero) with
|
||
| .one => "one"
|
||
| _ => "<other>",
|
||
"one"),
|
||
("DimExpr.normalize (.inv (.inv (.var i))) ≡ .var i",
|
||
match DimExpr.normalize (.inv (.inv (.var ⟨"i"⟩))) with
|
||
| .var j => s!"var {j.name}"
|
||
| _ => "<other>",
|
||
"var i"),
|
||
("FaceFormula.normalize (.meet .top (.eq0 i)) ≡ .eq0 i",
|
||
match FaceFormula.normalize (.meet .top (.eq0 ⟨"i"⟩)) with
|
||
| .eq0 j => s!"eq0 {j.name}"
|
||
| _ => "<other>",
|
||
"eq0 i"),
|
||
-- ── β-rules: discharge the five cubical-closure axioms ─────────────────
|
||
-- Each test exercises the path `Lean constructs a CVal closure →
|
||
-- vApp/vPApp routes through Rust @[implemented_by] → forcer unfolds
|
||
-- the CCHM RHS → result is no longer a stuck marker`.
|
||
("β vApp vTranspFun (const line, via beta::force_transp_fun)",
|
||
cvalSummary (vApp
|
||
(.vTranspFun ⟨"i"⟩ .univ .univ .bot (.vneu (.nvar "f")))
|
||
(.vneu (.nvar "y"))),
|
||
"vneu napp"),
|
||
("β vApp vHCompFun (stuck on .univ codA, via beta::force_hcomp_fun)",
|
||
cvalSummary (vApp
|
||
(.vHCompFun .univ .bot
|
||
(.vplam .nil ⟨"j"⟩ (.var "tube_body"))
|
||
(.vneu (.nvar "b")))
|
||
(.vneu (.nvar "x"))),
|
||
"vneu nhcomp"),
|
||
("β vApp vCompFun (φ=.bot collapses via C2, via beta::force_comp_fun)",
|
||
cvalSummary (vApp
|
||
(.vCompFun .nil ⟨"i"⟩ .univ .univ .bot (.var "u") (.var "t"))
|
||
(.vneu (.nvar "y"))),
|
||
"vneu napp"),
|
||
("β vPApp vTubeApp (via beta::force_tube_app)",
|
||
cvalSummary (vPApp
|
||
(.vTubeApp (.vplam .nil ⟨"j"⟩ (.var "tube_body")) (.vneu (.nvar "x")))
|
||
(.var ⟨"r"⟩)),
|
||
"vneu napp"),
|
||
("β vPApp vPathTransp at .zero ⇓ a(1) (via beta::force_path_transp)",
|
||
cvalSummary (vPApp
|
||
(.vPathTransp .nil ⟨"i"⟩ .univ (.var "a0") (.var "b0") .bot (.var "p"))
|
||
.zero),
|
||
"vneu nvar a0"),
|
||
("β vPApp vPathTransp at .one ⇓ b(1)",
|
||
cvalSummary (vPApp
|
||
(.vPathTransp .nil ⟨"i"⟩ .univ (.var "a0") (.var "b0") .bot (.var "p"))
|
||
.one),
|
||
"vneu nvar b0"),
|
||
("β vPApp vPathTransp at var r ⇓ compN (CCHM 3-clause system)",
|
||
cvalSummary (vPApp
|
||
(.vPathTransp .nil ⟨"i"⟩ .univ (.var "a0") (.var "b0") .bot (.var "p"))
|
||
(.var ⟨"r"⟩)),
|
||
"vneu ncompN"),
|
||
-- ── REL1 inductive-type smoke tests ─────────────────────────────────────
|
||
("eval (zero : Nat) ⇓ vctor zero",
|
||
cvalSummary (eval .nil zeroC),
|
||
"vctor zero ..."),
|
||
("eval (succ (succ zero) : Nat) ⇓ vctor succ",
|
||
cvalSummary (eval .nil (succC (succC zeroC))),
|
||
"vctor succ ..."),
|
||
("eval (false : Bool) ⇓ vctor false",
|
||
cvalSummary (eval .nil falseC),
|
||
"vctor false ..."),
|
||
("eval (cons true nil : List Bool) ⇓ vctor cons",
|
||
cvalSummary (eval .nil (consC CType.boolC trueC (nilC CType.boolC))),
|
||
"vctor cons ..."),
|
||
("readback ∘ eval (succ zero : Nat) ≡ ctor succ",
|
||
ctermSummary (readback (eval .nil (succC zeroC))),
|
||
"ctor succ ..."),
|
||
("eval (base : S¹) ⇓ vctor base",
|
||
cvalSummary (eval .nil baseC),
|
||
"vctor base ..."),
|
||
("eval (loop @ r : S¹) ⇓ vctor loop",
|
||
cvalSummary (eval .nil (loopC (.var ⟨"r"⟩))),
|
||
"vctor loop ..."),
|
||
("indElim Bool false-case (true → \"yes\") on true ⇓ \"yes\"",
|
||
cvalSummary (eval .nil
|
||
(boolElim (.lam "x" (.var "M")) (.var "no") (.var "yes") trueC)),
|
||
"vneu nvar yes"),
|
||
("indElim Bool true-case on false ⇓ \"no\"",
|
||
cvalSummary (eval .nil
|
||
(boolElim (.lam "x" (.var "M")) (.var "no") (.var "yes") falseC)),
|
||
"vneu nvar no"),
|
||
("transp_ind T1: φ=.top is identity",
|
||
cvalSummary (eval .nil
|
||
(.transp ⟨"i"⟩ CType.natC .top zeroC)),
|
||
"vctor zero ..."),
|
||
("transp_ind T2: constant Nat line is identity",
|
||
cvalSummary (eval .nil
|
||
(.transp ⟨"i"⟩ CType.natC (.eq0 ⟨"j"⟩) (succC zeroC))),
|
||
"vctor succ ..."),
|
||
("comp_ind C1: φ=.top reduces to u[i:=1]",
|
||
cvalSummary (eval .nil
|
||
(.comp ⟨"i"⟩ CType.natC .top (succC zeroC) zeroC)),
|
||
"vctor succ ...") ]
|
||
|
||
/-- Run every smoke test, print its actual vs expected. Returns the
|
||
number of failures. -/
|
||
def runSmokeTests : IO UInt32 := do
|
||
IO.println "── Topolei cubical FFI smoke tests ──"
|
||
let mut fails : UInt32 := 0
|
||
for (desc, actual, expected) in tests do
|
||
if actual == expected then
|
||
IO.println s!" ✅ {desc}"
|
||
else
|
||
IO.println s!" ❌ {desc}"
|
||
IO.println s!" expected: {expected}"
|
||
IO.println s!" actual: {actual}"
|
||
fails := fails + 1
|
||
IO.println s!"── {tests.length - fails.toNat} / {tests.length} passed ──"
|
||
return fails
|
||
|
||
end CubicalTransportFFITest
|