Dependency-ordered future kernel, bridge, extraction and Intent implementation work.
Core-3 Dependency-Ordered Implementation Roadmap
Status: planned follow-ups; no implementation or tracking-system mutation is implied by this document. The specification can be delivered and reviewed before any of these implementation projects starts.
| Order | Work | Depends on | Completion evidence |
|---|---|---|---|
| 1 | Foundation audit and proof-term/parser/elaborator inspection | Specification acceptance | Closed typed terms, adversarial universe/positivity cases, explicit metatheoretic assumptions; no runtime claims |
| 2 | Small independent-checkable kernel and minimal logical library | 1 | Checked propositions, inductives/recursors, exact challenge matching, derived axiom footprints, bounded failures |
| 3 | Logical proof/environment transport and identity validation | 1, 2 | Canonical vectors, reference closure, tamper rejection, independent rechecking and version isolation |
| 4 | Algorithm semantic bridge | 2, 3 | Checked operational model, partial/total distinction, numeric/ownership/error behavior, disclosed encoder trust |
| 5 | Compute, State, Flow, Optimize, Hardware, Physics bridges | 4 and each actual backend/model | Per-paradigm obligations from verification; physical fidelity and bounded evidence remain distinct |
| 6 | Computational extraction | 2, 3, 4 | Erasure and representation preservation; noncomputability rejection; host resource/error behavior |
| 7 | Intent declarations, policy/authority and formalization records | 1, 3 | Complete coverage, authenticated delegated approval, pinned challenges, protected context and independent-approval cases |
| 8 | Code/plan resolution, validation and admission | 4, 7 | Both product kinds satisfy one approved contract; no weakened-evidence fallback; pre/postcheck distinction |
| 9 | Capability-gated Intent runtime and provider boundary | 8 | Bounded resource reservations, cancellation/failure, scoped provider/context/execution grants, no implicit compiler model access |
| 10 | Durable Intent activities, replay and recovery | 9 and Flow/action journal | No model rerun on replay, immutable revisions, crash-gap and indeterminate-effect recovery |
| 11 | Canonical runtime snapshot and Proof/Intent ZDE views | Paired with 9 and 10 | Typed snapshot and user-visible ownership/evidence/budget/uncertainty tests, no UI-only state store |
| 12 | Physical ZLM4 transport, independent checker agreement and broader release evidence | 3, 6, 10, 11 | Frozen encoding, property/mutation tests, compatibility, provenance and activation review |
Each implementation step follows test-first ordering with public-interface assertions. Property tests cover serialization, canonical identities, alpha-renaming, exact dependency reuse, and replay invariants. Behavior-bearing mutants must be killed with new tests; equivalent mutants are documented.
Large theorem libraries, automatic Lean import, a tactics language, mutually recursive/nested inductives, higher-order extraction, implicit runtime model calls, and general natural-language equivalence are not promises of this preview. A future expansion needs explicit semantics and separately identified conformance, not permissive unknown-record handling.