max/cubical-transport-hott-lean4
1
0
Fork 0
Code Issues 1 Pull requests Projects Releases Packages Wiki Activity Actions
12 commits 3 branches 0 tags 2.1 MiB
Commit graph

2 commits

Author SHA1 Message Date
Maximus Gorog
4d6853a0ef REL1 Inductive.lean + Rust dispatch + 9 new smoke tests (25/25 + 46/46) 
Inductive.lean (new module): schema combinators (mkSchema, mkCtor,
mkPath) and canonical schema instances:
  - Plain inductives: natSchema, boolSchema, listSchema
  - HITs: s1Schema, intervalSchema, propTruncSchema
Plus type-level helpers (CType.natC, listC, s1C, …) and term-level
ergonomic builders (zeroC, succC, nilC, consC, baseC, loopC, …,
natLit, natElim, boolElim, listElim).

Rust kernel (native/cubical/src/):
  · tags.rs       — TY_IND, TERM_DIMEXPR/CTOR/INDELIM, VAL_VCTOR/VDIMEXPR,
                    NEU_NINDELIM tag constants per docs/INDUCTIVE_TYPES.md §6.
  · value.rs      — mk_vctor, mk_vdimexpr, mk_nindelim builders.
  · eval.rs       — TERM_DIMEXPR / TERM_CTOR / TERM_INDELIM dispatch
                    arms; full β-reduction on canonical vctor target
                    (find matching branch by name, vapp chain over
                    ctor args); stuck nIndElim build for vneu target;
                    eval_term_list / eval_branches / find_branch_body
                    helpers (recursive list walking).
  · readback.rs   — VAL_VCTOR / VAL_VDIMEXPR readback arms;
                    readback_val_list, map_readback_branches helpers;
                    NEU_NINDELIM neutral readback; mk_term_dimexpr,
                    mk_term_ctor, mk_term_indelim builders.

Tests (CubicalTransport/FFITest.lean): nine new smoke arms exercising
canonical-form eval (zero, succ-of-succ, false, cons-true-nil, base,
loop@r), readback round-trip on succ zero, and indElim β on Bool with
both branch directions.  Result: 25/25 smoke + 46/46 properties =
71/71 passing.

Existing tests untouched (constructor tags preserved per REL1 freeze).
Rust ABI version is now de facto v2 (new tags); update the
TOPOLEI_FFI_ABI_VERSION constant in a follow-up commit.

Remaining REL1 work (per task list):
  - #4  HasType arms for ctor / indElim
  - #8  transport over .ind axioms
  - #9  composition over .ind axioms
  - Path-ctor boundary firing (REL1.1)
  - Recursive-arg IH wiring in indElim β (REL1.1)
  - Topolei migration (sibling repo) per docs/INDUCTIVE_TYPES.md §9.1

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
 2026-04-30 15:15:50 -06:00
Maximus Gorog
31d19f655e Split: engine = cubical-transport HoTT only
Some checks are pending
Lean Action CI / build (push) Waiting to run
Details 
Restructure to engine-only contents.  Application code (Topolei.*
namespace, canvas-rs / render Rust crates, Main / ProbeTest, naga IR
pipeline, Selection / Subobject / Trace / Obs.Ctx hypothesis stack,
cells-spec / HYPOTHESES / STATUS / NAGA_IR_PLAN docs) moves to the
sibling repo max/topolei.

What moved:
- `Topolei/Cubical/*.lean` (22 files) → `CubicalTransport/*.lean`
  with namespace `Topolei.Cubical.*` renamed to `CubicalTransport.*`.
  Fully-qualified test types `TopoleiCubical{FFI,Property}Test` →
  `CubicalTransport{FFI,Property}Test` for consistency.
- New root file `CubicalTransport.lean` re-exporting all 22 modules.
- Lakefile: package `cubicalTransport`; lib `CubicalTransport`; only
  `cubical-test` and `cubical-bench` exes (no GPU link path).

The split criterion: anything an AI shortcut could break that would
cascade-corrupt downstream proofs lives here.  Anything that would
only break the application stays in the topolei interface repo.

cubical-test passes 62/62 (smoke + properties) on the renamed engine.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
 2026-04-27 21:35:01 -06:00