d9f952fa6c
Standard convention: README.md at root, everything else in docs/. Engine docs/: FFI_DESIGN, FFI_COMPLETENESS, KERNEL_BOUNDARY, NUMERICAL, PHASE1_HISTORY, ZIGZAG_PORT. README.md links updated to docs/<name>. Cross-repo reference in NUMERICAL.md (to topolei's STATUS.md) now includes the relative path `../topolei/docs/STATUS.md`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
12 KiB
FFI_COMPLETENESS.md — Axiom Coverage Audit for the Rust Backend
Stage 4.7 deliverable (2026-04-23). Cross-checks that every
FFI-declared Rust entry point has a complete set of reduction axioms
covering all reachable input cases. Companion to FFI_DESIGN.md:
design describes the contract, completeness confirms the contract is
satisfiable.
Verdict key
- 🟢 Green — Axiom set covers every constructor case; face-disjoint hypotheses partition the precondition space without overlap. Rust can implement by structural pattern match on the input.
- 🟡 Yellow — Axiom set covers the "main" cases; some combinations fall through to marker neutrals (type-error placeholders). Rust mirrors the partial def fallback behaviour (see FFI_DESIGN.md §6).
- 🔴 Red — Genuine gap: some reachable well-typed input has no discharging axiom. Rust cannot satisfy. None present as of Stage 4.
1. eval (topolei_cubical_eval)
Signature: CEnv → CTerm → CVal
| CTerm constructor | Axiom | Notes |
|---|---|---|
.var x |
eval_var |
env lookup with fallback to .vneu (.nvar x) |
.lam x body |
eval_lam |
produces .vlam env x body |
.app f a |
eval_app |
calls vApp |
.plam i body |
eval_plam |
produces .vplam env i body |
.papp t r |
eval_papp |
calls vPApp |
.transp i A .top t |
eval_transp_top |
T1 at eval level |
.transp i A φ t (A dim-absent) |
eval_transp_const |
T2 at eval level |
.transp i (.path A a b) φ t |
eval_transp_path |
produces vPathTransp closure |
.transp i A φ t (non-path, non-glue) |
eval_transp_nonpath |
delegates to vTransp |
.transp i (.glue …) φ t — 9 face-disjoint forms |
eval_transp_glue_{const,varA}_{at_bot,at_top,stuck} + _{const,varA}_at_top_hcomp + _varEquiv |
9 axioms partition (const/varA/varEquiv × bot/top/stuck) |
.transp i A ψ t (T5 face normalisation) |
eval_transp_face_congr |
face substitution commutes with transp |
.comp i A .top u t |
eval_comp_top |
C1 at eval level |
.comp i A .bot u t |
eval_comp_bot |
C2 at eval level |
.comp i A φ u t (A dim-absent) |
eval_comp_const |
C3-like for constant line |
.comp i (.pi domA codA) φ u t |
eval_comp_pi |
CCHM Π hetero comp |
.comp i A φ u t (stuck) |
eval_comp_stuck |
structured neutral |
.compN i A clauses t |
eval_compN |
multi-clause dispatch |
.glueIn .top t a |
eval_glueIn_top |
T-side wins |
.glueIn .bot t a |
eval_glueIn_bot |
A-side wins |
.glueIn φ t a (stuck, not unglue φ _ _) |
eval_glueIn_stuck |
structured nglueIn |
.glueIn φ t (.unglue φ f g) (η-redex) |
eval_glueIn_of_unglue |
under h_overlap |
.unglue .top f g |
eval_unglue_top |
forward map applied |
.unglue .bot f g |
eval_unglue_bot |
identity |
.unglue φ f g (stuck, not glueIn φ _ _) |
eval_unglue_stuck |
structured nunglue |
.unglue φ f (.glueIn φ t a) (β-redex) |
eval_unglue_of_glueIn |
under h_overlap |
.pair a b |
eval_pair |
produces .vpair |
.fst t |
eval_fst |
calls vFst |
.snd t |
eval_snd |
calls vSnd |
Verdict: 🟢 Green. Every CTerm constructor has a discharging axiom family. Face-disjoint preconditions partition the dispatch space without overlap. The Glue-transport family (9 axioms) is the widest partition; all are pattern-disjoint.
2. vApp (topolei_cubical_vapp)
Signature: CVal → CVal → CVal
| First CVal | Axiom | Notes |
|---|---|---|
.vlam env x body |
vApp_vlam |
β-reduce closure |
.vneu n |
vApp_vneu |
push into .napp |
.vTranspFun i domA codA φ f |
vApp_vTranspFun |
CCHM Π transport rule |
.vHCompFun codA φ tube base |
vApp_vHCompFun |
CCHM Π hcomp rule |
.vCompFun env i domA codA φ u t |
vApp_vCompFun |
CCHM Π hetero comp |
.vplam _ _ _ |
(marker neutral) | type error; .nvar "<vApp: vplam applied as function>" |
.vTubeApp _ _ |
(marker neutral) | type error |
.vPathTransp _ _ _ _ _ _ _ |
(marker neutral) | type error |
.vpair _ _ |
(marker neutral) | type error |
Verdict: 🟡 Yellow. The five principal cases (vlam, vneu, vTranspFun, vHCompFun, vCompFun) have axioms. Four type-error cases produce marker neutrals without dedicated axioms — Rust mirrors the partial def's marker-neutral behaviour (FFI_DESIGN.md §6). This is by design; well-typed terms never reach these arms.
3. vPApp (topolei_cubical_vpapp)
Signature: CVal → DimExpr → CVal
| First CVal | Axiom | Notes |
|---|---|---|
.vplam env i body |
vPApp_vplam |
β-reduce dim-closure |
.vneu n |
vPApp_vneu |
push into .npapp |
.vTubeApp tube arg |
vPApp_vTubeApp |
reduce pointwise |
.vPathTransp _ _ _ a _ _ _ at .zero |
vPApp_vPathTransp_zero |
|
.vPathTransp _ _ _ _ b _ _ at .one |
vPApp_vPathTransp_one |
|
.vPathTransp env i A a b φ p at generic r |
vPApp_vPathTransp_general |
CCHM multi-clause |
| Other vCtors (vlam, vTranspFun, vHCompFun, vCompFun, vpair) | (marker neutral) | type errors |
Verdict: 🟡 Yellow — same reasoning as §2.
4. vTransp (topolei_cubical_vtransp)
Signature: DimVar → CType → FaceFormula → CVal → CVal
| Condition | Axiom |
|---|---|
φ = .top |
vTransp_top |
| A dim-absent from i | vTransp_const |
A = .pi domA codA, not dim-absent, φ ≠ .top |
vTransp_pi |
| Otherwise stuck | vTransp_stuck |
Verdict: 🟢 Green. Four priority-ordered cases with face-disjoint hypotheses.
5. vHCompValue (topolei_cubical_vhcomp)
Signature: CType → FaceFormula → CVal → CVal → CVal
| Condition | Axiom |
|---|---|
φ = .top |
vHCompValue_top |
A = .pi domA codA |
vHCompValue_pi |
| Otherwise | vHCompValue_stuck |
Verdict: 🟢 Green.
6. vCompAtTerm (topolei_cubical_vcomp_term)
Signature: CEnv → DimVar → CType → FaceFormula → CTerm → CTerm → CVal
Delegates to eval's .comp arm via the term-level substDim behaviour.
Covered by the 5 eval_comp_* axioms (§1).
Verdict: 🟢 Green.
7. vCompNAtTerm (topolei_cubical_vcompn_term)
Signature: CEnv → DimVar → CType → List (FaceFormula × CTerm) → CTerm → CVal
| Clause configuration | Axiom | Notes |
|---|---|---|
| any form | vCompNAtTerm_def |
scan-and-dispatch definitional equation |
Verdict: 🟢 Green. Single axiom describes the complete scan behaviour; Rust implements the scan-find-top / strip-bot / single-live / multi-live dispatch.
8. vFst / vSnd (topolei_cubical_vfst, topolei_cubical_vsnd)
Signature: CVal → CVal
| Input | vFst axiom | vSnd axiom |
|---|---|---|
.vpair a b |
vFst_vpair |
vSnd_vpair |
.vneu n |
vFst_vneu |
vSnd_vneu |
| Other vCtors | (marker neutral) | (marker neutral) |
Verdict: 🟢 Green (on principal cases). Marker neutrals for type-error cases follow §2 convention.
9. readback (topolei_cubical_readback)
Signature: CVal → CTerm
| CVal constructor | Axiom |
|---|---|
.vneu n |
readback_vneu (delegates to readbackNeu) |
.vlam env x body |
readback_vlam |
.vplam env i body |
readback_vplam |
.vTranspFun i domA codA φ f |
readback_vTranspFun |
.vCompFun env i domA codA φ u t |
readback_vCompFun |
.vHCompFun codA φ tube base |
readback_vHCompFun |
.vTubeApp tube arg |
readback_vTubeApp |
.vPathTransp _ _ _ _ _ _ (.plam j body) |
readback_vPathTransp_plam |
.vPathTransp _ _ _ _ _ _ p (non-plam p) |
readback_vPathTransp_other |
.vpair a b |
readback_vpair |
Verdict: 🟢 Green. Every CVal constructor handled; .vPathTransp
face-disjointly split on inner CTerm shape (Stream B #2c).
10. readbackNeu (topolei_cubical_readback_neu)
Signature: CNeu → CTerm
| CNeu constructor | Axiom |
|---|---|
.nvar x |
readbackNeu_nvar |
.napp n arg |
readbackNeu_napp |
.npapp n r |
readbackNeu_npapp |
.ntransp i A φ v |
readbackNeu_ntransp |
.ncomp i A φ u t |
readbackNeu_ncomp |
.nhcomp A φ tube base |
readbackNeu_nhcomp |
.ncompN env i A clauses t |
readbackNeu_ncompN |
.nglueIn φ t a |
readbackNeu_nglueIn |
.nunglue φ f g |
readbackNeu_nunglue |
.nfst n |
readbackNeu_nfst |
.nsnd n |
readbackNeu_nsnd |
Verdict: 🟢 Green. Every CNeu constructor has an axiom.
11. stepRust (topolei_cubical_step) — optional
Signature: CTerm → CTerm
Per FFI_DESIGN.md §8, the Rust backend may either implement step
natively (Option A) or derive it as readback ∘ eval .nil (Option B).
Both satisfy:
| Axiom | Content |
|---|---|
transp_plam_is_plam_path |
T4 path-restricted: step (transp i (.path A a b) φ (.plam j body)) = .plam j (.compN i A [(φ, body), (.eq0 j, a), (.eq1 j, b)] body) |
For arbitrary (non-T4) inputs, step has no reduction axiom; its
behaviour is determined by the CTerm.step_preserves_type axiom in
ValueTyping.lean (which is a typing-preservation claim, not a
reduction rule).
Verdict: 🟢 Green. One reduction axiom (T4 path-restricted).
Subject reduction handled at the ValueTyping layer. Option B (derived
step) automatically satisfies T4 via the .vPathTransp → .plam j (.compN …) readback arm.
12. DimExpr.normalize (topolei_cubical_dimexpr_normalize)
Signature: DimExpr → DimExpr
| Axiom / Theorem | Content |
|---|---|
DimExpr.normalize_preserves_eval |
semantic: (normalize r).eval env = r.eval env |
normalize_inv_zero |
.inv .zero → .one |
normalize_inv_one |
.inv .one → .zero |
normalize_inv_inv_eval |
double-negation preserves eval |
Verdict: 🟢 Green (for the implemented reductions). Unit /
absorption laws (.meet .zero _ → .zero etc.) are semantically valid
but deliberately not normalised — future normalize_full extension.
13. FaceFormula.normalize (topolei_cubical_face_normalize)
Signature: FaceFormula → FaceFormula
| Axiom / Theorem | Content |
|---|---|
FaceFormula.normalize_preserves_eval |
semantic: evaluation preserved |
| Recursive literal-identity / absorption reductions | covered by the definition |
Verdict: 🟢 Green. Covers meet/join with .top / .bot literals;
mutually-exclusive literal reductions (.meet (.eq0 i) (.eq1 i) → .bot)
are skipped and may be added later.
14. Cross-cutting audit — Lean-discharge remnants
These axioms are not Rust's responsibility — they're future Lean work:
| Axiom | File | Target |
|---|---|---|
HasVal, HasNeu, EnvHasType |
ValueTyping.lean | Inductive definition |
eval_preserves_type |
ValueTyping.lean | Structural induction on eval |
readback_preserves_type |
ValueTyping.lean | Structural induction on readback |
EnvHasType.nil |
ValueTyping.lean | Base case lemma |
CTerm.step_preserves_type |
ValueTyping.lean | Composition of above |
DimLine.inv_at0, inv_at1, inv_inv |
Line.lean | Pending CType-level normalisation |
transp_plam_is_plam_path |
TransportLaws.lean | (or Rust-discharged via Option B) |
Total Lean-discharge remaining: 8 axioms.
15. Overall verdict
🟢 Green across the FFI surface. Every Rust entry point has an axiom set covering all constructor cases and face dispatches. The yellow flags in §§2, 3, 8 are by-design marker-neutral behaviour for ill-typed inputs, not genuine gaps.
Rust is ready to start. The Lean spec side is complete for the cubical core + Line + Sigma + Glue (constant-equiv + hcomp-corrected + varying-equiv stuck) + β/η glue + subject reduction. Remaining Lean work (§14) is orthogonal to Rust and can proceed in parallel.
End of FFI_COMPLETENESS.md. Sibling: FFI_DESIGN.md (memory /
marshalling / build integration contract).