Phase 1, Section 8: Exit Criteria and Phase 2 Entry
Phase 1: Implementation — the shape-typed core compiled end-to-end. Section 8 of 8: Exit Criteria and Phase 2 Entry.
1. What this section commits to
The closing section of Phase 1. Specifically:
- The consolidated acceptance criteria from all seven preceding sections, organized for a single decision moment.
- The judgment-call exit criterion in operational terms — what "the foundation feels sturdy enough" actually means.
- The risk-and-abandonment criteria from Section 1 §6, revisited with implementation context now visible.
- Phase 2 entry conditions: what Phase 1 must hand off to Phase 2 for that work to be tractable.
- The handoff manifest: the specific artifacts Phase 1 produces for Phase 2 to consume.
- Closing notes on the project's overall arc and what the Phase 1 commitment means in context.
After this section, Phase 1 specification is complete. Implementation work can begin (or be reconsidered) against a fully-defined target.
2. Consolidated acceptance criteria
The full picture, organized by category rather than by section. A Phase 1 release candidate must satisfy every item below.
2.1 Compiler (from Sections 2 and 5)
| Criterion | Source |
|---|---|
| All ten Phase 0 operations compile correctly for CPU and GPU placements | §2.12, §5.8 |
| Four operation extensions (variadic matmul, gather, softmax, repeat_interleave) work end-to-end | §5.8 |
| Type errors include source locations and SMT counterexamples where applicable | §2.10 |
| Compiler produces valid LLVM IR linkable into a shared object | §2.12 |
| Compiler is under 15K lines of OCaml | §2.12 |
| Compile time for transformer block under 2 seconds | §2.12 |
All compiler tests pass; no --ignore-test flags in main |
§2.12 |
| Bidirectional type-checking with batched SMT discharge | §2.5, §2.6 |
2.2 Runtime (from Section 3)
| Criterion | Source |
|---|---|
| All ~17 FFI entry points implemented and tested | §3.10 |
| Tensor lifecycle correct under stress (1M alloc/dealloc cycles, no leaks) | §3.10 |
| DLPack roundtrip with PyTorch passes in CI | §3.5.4 |
Pool allocator ≥5× speedup over CudaMemoryResource on stress workload |
§3.4.4 |
| Stream ordering correct under stress | §3.10 |
| No panics escape the FFI boundary (verified by random-input testing) | §3.10 |
Send + Sync correctness verified by Clippy + Miri |
§3.10 |
| Error messages preserve information through FFI translation | §3.10 |
Generated header kina_runtime.h matches Rust source in CI |
§3.10 |
| Compiles cleanly on Linux and macOS | §3.10 |
| Runtime is under 8K lines of Rust | §3.10 |
2.3 Observability (from Section 4)
| Criterion | Source |
|---|---|
| Every compiler phase emits a span (parse, elaborate, typecheck, lower, emit) | §4.11 |
Every public FFI function carries tracing::instrument |
§4.11 |
Module ID propagates from --module-id through every runtime span |
§4.6, §4.11 |
Nsight Systems shows our kernels with meaningful names; no unknown ranges |
§4.7, §4.11 |
| Default-mode trace overhead < 5% on transformer-block benchmark | §4.9, §4.11 |
| Disabled-mode trace overhead < 1% | §4.9, §4.11 |
| Errors include trace context | §4.4, §4.11 |
| Debugging guide documented with worked example | §4.11 |
| JSON-lines output follows OpenTelemetry semantic conventions | §4.11 |
2.4 Verification (from Section 6)
| Criterion | Source |
|---|---|
| Lean 4 project builds in CI; failures block PRs | §6.9 |
| Phase 0 §1 (types, refinements) mechanized with basic proofs | §6.9 |
| Phase 0 §2 typing rules mechanized as inductive cases (statements) | §6.9 |
| Phase 0 §3 subtyping mechanized; reflexivity and transitivity proven | §6.9 |
| Phase 0 §4 reduction relation mechanized (statements) | §6.9 |
Subject reduction for elementwise fragment fully proven (no sorry) |
§6.5, §6.9 |
| Translation validation obligation format committed; trusted-mode example working | §6.6, §6.9 |
Every sorry has a comment explaining what fills it (Phase 6 work) |
§6.9 |
| Verification project under 5K lines of Lean | §6.9 |
2.5 Testing and Quality (from Section 7)
| Criterion | Source |
|---|---|
| Unit test coverage > 85% (OCaml and Rust) | §7.12 |
| Integration tests pass in under 10 minutes total | §7.12 |
| Golden tests vs. PyTorch pass within FP tolerance per dtype | §7.5, §7.12 |
| Standard CI completes in under 10 minutes per push | §7.12 |
| GPU CI completes in under 30 minutes for relevant PRs | §7.12 |
| Performance regression thresholds enforced | §7.6, §7.12 |
| ABI snapshot tests in place; one per stable surface | §7.8.3 |
| Library author's guide v0.1 worked example builds from documentation alone | §7.9.3 |
| Documentation site live; updated on every push to main | §7.10, §7.12 |
| Doctests pass in CI | §7.10.3 |
| GPU determinism tests pass (bitwise-identical outputs) | §7.7.3 |
2.6 The end-to-end demonstration (from Section 1)
The single load-bearing acceptance criterion that integrates everything else:
| Criterion | Source |
|---|---|
Transformer block forward pass runs end-to-end on GPU, with results within 1e-3 FP tolerance against a PyTorch reference. The block includes RMSNorm + multi-head attention with grouped-query (GQA) heads + softmax + SwiGLU FFN + residual connections. ~50–100M-parameter equivalent. |
§1.3.3, §1.4 |
| Idiomatic transformer block expressible in under 200 lines of language code | §5.8 |
| Performance within 3–5× of PyTorch on the same workload | §1.4 |
If any one of these three fails, Phase 1 is not done — every other criterion can pass and Phase 1 still isn't complete. These three are the operational test that the system actually does what the spec promises.
3. The judgment-call exit criterion
Section 1 §4 #7 was: "the author is willing to commit to Phase 2." This is judgment, not metric. With Phase 1's full spec now visible, here is what the judgment is actually evaluating.
3.1 Five questions the judgment should answer
1. Does the type system feel expressive enough? Concretely: do the proto-stdlib functions and the transformer-block test program use escape hatches (axiomatic shape assertions, controlled-unsoundness reshape) only where genuinely necessary, or do they rely on them frequently? A handful of axioms in well-isolated places is fine. A program that's mostly axioms is a sign the type system isn't doing its job.
2. Did the verification track produce a real proof? The elementwise subject reduction proof either went through cleanly or struggled. If it struggled — if it required ad-hoc lemmas, contortion of the encoding, or weakening of the theorem statement — that's a signal the framework needs revision before Phase 6 invests more in it.
3. Is the DLPack interop demo solid? Not just "does it pass once" — does it pass under stress, with various dtypes, with non-contiguous tensors, with multi-stream workloads? Phase 5+ ecosystem work depends on this; if Phase 1's demo is fragile, Phase 5 is shaky.
4. Are the abandonment-trigger conditions absent? Section 1 §6.3 listed three foundational risks (type system inexpressive, verification intractable, real-world programs hit too many escape hatches). None should have triggered. If one did and was patched rather than addressed, the patch may be shallow.
5. Does Phase 2's design still feel right? Phase 1 produces artifacts on which Phase 2 builds. The bootstrap-and-self-modeling track committed Phase 2 to AD-as-handler. Does the runtime FFI surface (now built and battle-tested) actually look amenable to handler-based interception? Are there hidden state pockets the handler design didn't anticipate?
3.2 What "yes" looks like
For each of the five questions, the answer needed to commit to Phase 2 is not "perfect" but "no smoking guns."
- The type system: a few documented escape hatches, each with a clear path to fix in later phases.
- The verification track: a working proof and a coherent infrastructure, with the Phase 6 path visible.
- The runtime: an interop demo that's been stressed and survived.
- The risks: nothing fundamental triggered; the patches that did happen are sound.
- Phase 2 design: still coherent; the handler-friendly FFI is genuinely friendly.
This is the kind of judgment that's clearer in the moment than in the abstract. Phase 1's exit decision involves looking at the whole and asking does this feel like a foundation, or like a stack of patches?
3.3 What "no" looks like
If the answer is no — if the foundation feels patched or shaky — the response is the same as Phase 0's: revise rather than continue. Specifically:
- Type-system inexpressiveness: revise Phase 0 §1 or §2; reissue the spec; rebuild the affected compiler stages.
- Verification intractability: revisit Phase 0 §4's operational semantics; possibly reformulate the proof framework.
- Runtime fragility: identify the specific failure modes; revise the FFI design or the memory manager; rebuild.
- Phase 2 design concerns: write a Phase 2 design memo before starting Phase 2; possibly delay Phase 2 by 3–6 months for redesign.
The cost of revising Phase 1 is large — 6–12 months of additional work — but the cost of building Phase 2+ on a patched Phase 1 is much larger. Phase 1 is the foundation; foundations are where revision is cheapest relative to the long-term cost of getting them wrong.
4. Risks revisited
Section 1 §6 articulated three risk categories before implementation specifics were committed. With the full spec now in place, the picture is more concrete.
4.1 Recoverable risks (revise and continue)
These remain manageable; nothing in Sections 2–7 changed the analysis.
- SMT timeouts on real programs → heuristics + bigger budget (Section 2 §6).
- MLIR/LLVM version churn → deliberate-cycle upgrades (Section 2 §7.3, Phase 0 §5.7).
- Z3 binding bugs → vendor a known-good fork.
- DLPack ABI versioning → pin a specific version (Section 3 §5.3).
4.2 Architectural risks (consider revising the framework)
The implementation specs added two architectural concerns worth tracking:
The omega tactic might not be enough for verification. Section 6 §10.1.1 committed to Lean's omega tactic for Presburger arithmetic. If omega proves insufficient — particularly for modular-arithmetic refinements that gather and softmax depend on — the fallback is a custom Presburger DSL inside Lean. This is real engineering work (~1000 lines of Lean) and pushes onto Phase 6 territory. Manageable but flagged.
Compiler/runtime size budgets may be optimistic. Section 2 committed to 15K LoC OCaml; Section 3 committed to 8K LoC Rust. Section 4 added 500–800 LoC compiler and 300–500 LoC runtime for observability. The total budget is around 24K LoC of implementation code. If the codebase grows beyond, the discipline says refactor before continuing. If refactoring doesn't recover the budget, the design may be more complex than expected — worth flagging in the exit decision.
4.3 Foundational risks (consider abandonment)
These are unchanged from Section 1 §6.3 in shape but more concrete in trigger:
The unified type system can't express common ML programs. Trigger: the proto-stdlib (per the bootstrap track) requires axiomatic assertions in more than ~20% of functions. Or: the transformer-block demo's 200-line budget grows past 400 lines. Either signals expressiveness gaps that need foundational revision.
Lean 4 verification of a small fragment is intractable. Trigger: the elementwise subject reduction proof exceeds 1000 lines or requires axioms beyond Lean's standard library. Either signals the framework is harder to verify than the design assumed.
Real-world programs hit too many escape hatches. Trigger: the transformer-block demo uses controlled-unsoundness reshape in more than ~3 places, or uses axiomatic shape assertions in more than ~5 places. Either signals the type system is in tension with practical ML programs.
The numerical thresholds (20%, 200 lines, 1000 lines, etc.) are deliberate. They make abandonment a reachable decision rather than a vague feeling. If the project hits them, the exit decision is clear.
5. Phase 2 entry conditions
What must be true at Phase 1's end for Phase 2 to start.
5.1 Hard prerequisites
- All Phase 1 acceptance criteria from §2 satisfied.
- The judgment-call exit criterion from §3 answered "yes."
- The bootstrap-and-self-modeling track's Phase 1 commitments delivered:
- Proto-stdlib in test fixtures (per §7.1 of that document).
- ADR on bootstrap stance (per §7.2).
- Runtime FFI design discipline verified (per §7.3).
5.2 Soft prerequisites
These aren't strictly required but make Phase 2 dramatically easier:
- A clear list of escape hatches used by the proto-stdlib, with notes on what would fix each.
- A clear list of operation-set gaps that emerged during Phase 1, with priorities for Phase 2.
- A draft Phase 2 design document that specifies the AD-as-handler PoC's structure (per the bootstrap track §6).
- Performance baselines for the transformer block, by operation, recorded so Phase 2 changes can be compared.
5.3 Phase 2's first deliverable
Phase 2 starts with the AD-as-handler PoC (per the bootstrap track §6). This is:
- A small program (
linear → mse_loss). - A reverse-mode AD handler in the language.
- Gradients computed via
with reverseMode handle (f W b x target). - Gradients verified against PyTorch within FP tolerance.
- Handler implementation under a few hundred lines of language code.
If this PoC works, Phase 2 is on track. If not, Phase 2 is in revision mode and the rest of Phase 2's plan needs reconsidering.
This is the same discipline as Phase 1 had — the load-bearing milestone is at the start, not at the end. Failure surfaces early; success enables the rest.
6. The handoff manifest
Specific artifacts Phase 1 produces that Phase 2 consumes.
6.1 Code artifacts
compiler/— the OCaml compiler with the typed-IR data model, bidirectional type-checker, MLIR lowering, LLVM driver. ~12–15K LoC.runtime/— the Rust runtime withMemoryResourcetrait, DLPack-compatible Tensor, kernel dispatch FFI. ~7–9K LoC.verify/— the Lean 4 mechanization with Phase 0 §1–§4 stated and the elementwise subject reduction proven. ~4–5K LoC.
6.2 Documentation artifacts
docs/library-authors-guide.mdv0.1 (per §7.9). The first stable interface for external users.docs/architecture/— per-component overviews.decisions/— ADRs at repo root (Phase 0 Section 5); material decisions, including the bootstrap-stance ADR.docs/migrations/— empty for now; placeholder for future stable-API changes.docs/tutorials/— minimal Phase 1 set; expanded by later phases.
6.3 Test artifacts
compiler/test/— unit, integration, golden, error-path tests.runtime/tests/— runtime tests including the DLPack roundtrip.runtime/benches/— performance baselines using the observability infrastructure.verify/test/— Lean typing examples shared with the compiler test fixtures.- Golden references against PyTorch for every operation.
6.4 Infrastructure artifacts
- The CI pipeline (standard + GPU tiers).
- The performance regression infrastructure with baseline tracking.
- The ABI snapshot tests.
- The doc-build pipeline with doctests.
- Self-hosted GPU runners (operational, documented).
6.5 Specification artifacts
phase-0/— unchanged from Phase 0; possibly with Section 4 (observability) addenda absorbed into earlier sections.phase-1/— this entire directory of eight section documents.forward-tracks/— five forward-track documents (CUDA-native, ecosystem, Arrow, bootstrap/self-modeling, surface and personas).companions/— the walkthroughs and real-world examples, possibly updated based on Phase 1 implementation experience.
6.6 What Phase 2 starts with
Phase 2 doesn't start from zero. It starts from a working language with:
- A type system validated on real programs.
- A runtime with proven interop.
- A verification track with a working proof and infrastructure for more.
- A library author's guide that establishes what's stable.
- Performance baselines and regression detection.
- A complete spec for what's been built.
Phase 2's first design document describes how to extend this with effects (mutation, AD, control flow). The AD-as-handler PoC is the first concrete deliverable. Everything else Phase 2 commits to grows from there.
7. The arc forward
Phase 1 is not the destination. Worth ending the spec by placing it in context.
7.1 The shape of Phases 2–7
| Phase | Focus | Load-bearing deliverable |
|---|---|---|
| Phase 2 | Effects, AD, control flow | AD-as-handler PoC (per bootstrap track) |
| Phase 3 | Sharding, distribution | GSPMD-style sharding propagation as type inference |
| Phase 4 | Sparsity, structured tensors | TACO-style format generation; MoE routing |
| Phase 5 | Hardware capabilities, tile IR | Capability-typed tile programming; first AMD/TPU target |
| Phase 6 | Verification (parallel; becomes focus) | Verified subject reduction for full operation set |
| Phase 7 | Surface syntax | A real Pythonic or ML-flavored surface language |
Each phase has its own scope, milestones, exit criteria, abandonment triggers. Each phase's design memo is written when that phase is nearing.
7.2 What Phase 1 means in this context
Phase 1 is the gateway phase. Phase 0 was paper; walking away from Phase 0 cost essentially nothing. Phases 2–7 build on Phase 1 in compounding ways — Phase 2's AD handler depends on Phase 1's FFI; Phase 3's sharding depends on Phase 1's type system; Phase 5's tile IR depends on Phase 1's runtime architecture.
This is why Phase 1's exit criteria are stricter than Phase 0's, and why the judgment-call criterion is harder. Phase 1 is the moment the project commits to the framework as built. After Phase 1, revision becomes more expensive every phase.
7.3 Honest assessment
The Phase 1 plan is ambitious for a part-time effort. 4–6 months of part-time work to deliver a working compiler + runtime + verification track + observability + library-author's guide + comprehensive testing. ~24K lines of code across three languages. A full mechanization (statements at least) of the spec. A working non-trivial proof.
The plan is achievable for someone with the relevant background — compiler engineering, OCaml, Rust, CUDA, formal methods — and with realistic time allocation. It is not achievable as a casual side project; the discipline requirements alone (testing, ABI, documentation, observability) consume significant effort.
The plan will probably overrun on time. Plans of this size do. The discipline is to prefer extending the timeline over cutting scope — the scope is what makes Phase 1 a real foundation rather than a prototype, and cutting it accumulates technical debt that Phase 2 inherits.
7.4 The thesis
The thesis the project rests on, from the design memos: refinement-typed tensors with five orthogonal axes (shape, effects, structure, sharding, hardware capability), a multi-tier compilation pipeline, verified compilation passes for high-stakes transformations, RAPIDS-style ecosystem architecture. None of the pieces are new; the integration is the contribution.
Phase 1 validates the first axis (shape) end-to-end. Phases 2–5 add the other four axes. Phase 6 verifies them. Phase 7 packages them for human users.
If the thesis is right, this becomes a real language. If the thesis is wrong, Phase 1 is where it becomes wrong-in-an-obvious-way — and the project gets to walk away with the artifacts intact and the lessons learned. Either outcome is fine. The discipline is to make the test of the thesis cheap, fair, and falsifiable.
8. Closing
Phase 0 produced a spec. Phase 1 produces a working language that implements that spec on one of the five axes, with the infrastructure for the rest to follow.
If Phase 1 ships and the exit decision says "continue," Phases 2–7 become real plans rather than design memos, and the language project moves from a research artifact toward something usable. If Phase 1 ships and the exit decision says "wait" or "revise," Phase 0 gets revised, Phase 1 gets restarted, and the cost of having built it the first time is measured against the cost of getting the foundation wrong forever.
If Phase 1 doesn't ship — if the abandonment triggers fire and the project pauses — Phase 0's spec, Phase 1's implementation work to that point, and the forward-track documents stand as a research artifact. The thesis was tested honestly; the answer was negative; the path forward is clear (refine the framework, try again, or apply the lessons to a different project).
All three outcomes are acceptable. The discipline is to make the choice deliberately, with full information, against well-defined criteria. Phases 0 and 1 between them produce the criteria; the exit decision applies them.
Phase 1 is where the project becomes real. The Phase 1 spec is now complete.
End of Phase 1, Section 8. End of Phase 1 specification.