Phase 1, Section 1: Scope, Milestones, and Exit Criteria

Phase 1: Implementation — the shape-typed core compiled end-to-end. Section 1 of 7: Scope, Milestones, and Exit Criteria.

1. What this section commits to

What Phase 1 actually delivers, broken into three internal milestones with clear acceptance criteria for each. What's deferred to later phases. The risks and abandonment criteria for Phase 1 specifically. The timeline.

This is not a project plan in the project-management sense — no dates, no Gantt charts. It is a commitment to what the shape of done looks like so that progress can be measured against something real and so that abandonment is a reachable decision rather than a slow drift.

2. Phase 1 scope (final, after CUDA + ecosystem additions)

The scope is larger than the original roadmap framing because three things accumulated during Phase 0:

1. CUDA-native commitment (CUDA-native walkthrough) added device placement to the type system and committed Phase 1 to GPU forward-pass execution via library kernels.
2. Ecosystem architecture (ecosystem architecture) added the memory manager, tensor ABI, and library author's guide as Phase 1 deliverables.
3. Real-world examples (real-world examples) surfaced four operation-set additions worth committing to in Phase 1: variadic-batch matmul, gather, softmax-as-primitive, and repeat_interleave.

The full Phase 1 deliverable is therefore:

The end-to-end demo is the load-bearing acceptance criterion. Everything else can be checked off, but if the forward pass of a small transformer block doesn't run on a GPU and produce numerically-correct results within FP tolerance against PyTorch, Phase 1 is not done.

3. Three internal milestones

Phase 1 breaks naturally into three checkpoints. Each is roughly two months of part-time work; together they fit the 4–6 month part-time / 2–3 month full-time envelope.

3.1 Milestone 1 — CPU-only working compiler

Target: months 1–2 (part-time).

The Phase 0 stubs grow into real implementations. The compiler can:

• Parse the S-expression IR for tensor expressions.
• Type-check programs using the Phase 0 rules, including SMT discharge for shape obligations.
• Emit MLIR text via the textual-emission strategy (Phase 0 §5.3).
• Drive mlir-opt | mlir-translate | llc as subprocesses to produce LLVM IR and a shared object.
• Surface meaningful error messages when type-checking fails (with SMT counterexamples for shape mismatches).

The runtime can:

• Allocate tensor handles in a heap.
• Load a compiled .so and invoke entry points via libloading.
• Run a forward pass of an MLP and compare results against a PyTorch reference within FP tolerance.

Acceptance: a small but realistic test program (e.g., a 2-layer MLP forward pass on a [B, S, D] input with B=4, S=128, D=256) compiles and produces results matching PyTorch within 1e-5 FP tolerance. CPU-only; no GPU work yet.

3.2 Milestone 2 — Memory manager, tensor ABI, GPU library dispatch

Target: months 3–4 (part-time).

The runtime grows in three ways:

• The MemoryResource trait is implemented with four backends: raw CUDA, async CUDA, pool-on-CUDA, logging-wrapper.
• The Tensor struct gets its DLPack-compatible #[repr(C)] prefix; round-trip interop with PyTorch via DLPack is demonstrable.
• The compiler's lowering pipeline learns to emit code that calls library kernels — cuBLAS for matmul, cuDNN for elementwise + reductions where they're faster, naive in-house kernels for the rest.

The compiler grows in two ways:

• Device placement is propagated through the IR. Operations between mismatched placements either type-check via copy_to_device / copy_to_host or fail with clear errors.
• The lowering pipeline picks library calls vs. in-house implementations based on operation, shape, and dtype.

Acceptance: the same MLP from Milestone 1 now runs on GPU, with both inputs and weights resident in cuda:global(0). Performance is within 3× of PyTorch on the same workload. The DLPack interop demo (export a tensor from our runtime, run a PyTorch operation on it, import the result back) works without copies.

3.3 Milestone 3 — Operation extensions, verification, ABI hardening

Target: months 5–6 (part-time).

The four operation extensions land:

• Variadic-batch matmul: Tensor[T, [..., M, K]] → Tensor[T, [..., K, N]] → Tensor[T, [..., M, N]]. Eliminates the flatten dance that real-world-examples §3.1 highlighted.
• Gather: Tensor[T, [V, D]] → Tensor[I64, [B, S]] → Tensor[T, [B, S, D]]. Unblocks embedding lookup, cross-entropy, MoE routing.
• Softmax as a primitive: lowering decomposes internally into the six-op composite; users see one operation with one type rule.
• repeat_interleave: handles GQA cleanly; eliminates a class of axiomatic assertions.

The verification track delivers:

• Lean 4 mechanization of Phase 0 sections 1–4 (statements only; type-checks but uses sorry for some proofs).
• One non-trivial proof: subject reduction for a fragment of the language. The "fragment" can be small — e.g., the elementwise unary and binary operations only — but the proof must actually go through.

The public ABI is documented:

• The library author's guide reaches a usable v0.1: enough that a hypothetical second user could understand how to build a small library on top of the runtime.
• The ABI stability policy is committed: which surfaces are #[unstable], which are #[stable], and the path between them.

Acceptance: a transformer-block forward pass (RMSNorm + multi-head attention with softmax + SwiGLU FFN + residual connections; ~50–100M params equivalent) runs end-to-end on GPU with results within 1e-3 FP tolerance against a PyTorch reference. The test suite covers all of Phase 0's operations plus the four extensions. Phase 1's Lean 4 work compiles cleanly with at least one real proof.

4. Exit criteria

Phase 1 is complete when all of the following are true:

1. All three milestones met with their acceptance criteria satisfied.
2. A demonstrable end-to-end forward pass of a small but realistic LLM building block runs on GPU and produces correct results.
3. Performance is within 3–5× of PyTorch on the benchmark workloads (acceptable for a research artifact; not production).
4. CI is green on every push, with unit / integration / golden-output / GPU tests all running.
5. The Lean 4 verification track has produced at least one non-trivial proof beyond the spec-mechanization stubs.
6. The public ABI is documented and stable enough that a hypothetical external library author could plausibly start building on it.
7. The author is willing to commit to Phase 2. This is judgment, not metric. The Phase 0 §9 framing applies here too: if at the end of Phase 1 the foundation feels wrong, the right move is to revise rather than continue.

The seventh criterion is the hardest. By Phase 1 end, the project has accumulated significant code (probably 10–15K LOC across OCaml, Rust, and Lean). Walking away from that is psychologically harder than walking away from Phase 0's paper-only spec. But the discipline is the same: gate continuation on whether the foundation feels sturdy enough to bear Phase 2's weight (effects, AD, control flow), not on sunk cost.

5. What is explicitly deferred to later phases

What Phase 1 does not deliver, by design:

The above is the contract for what Phase 2 onward will need to handle. Phase 1 must not accidentally implement any of it; doing so creates inconsistencies between phases and forces re-work.

The single most tempting thing to slip is rudimentary AD. PyTorch-style autograd via tape-building is implementable in a few hundred lines of OCaml and would make the Phase 1 demo more impressive. It is forbidden. Phase 2 commits to AD as algebraic effects (memo 2's framework); a tape-based shortcut in Phase 1 would either contradict Phase 2's design or get thrown away when Phase 2 lands. Either is bad. The discipline is to leave AD untouched until Phase 2 begins.

Similarly tempting and similarly forbidden: a tile-IR prototype, a sharding annotation system, a sparsity type. Each of these has a designated phase and a designed framework; Phase 1 implementations of any of them would short-circuit the design work that gives them shape.

6. Risks and abandonment criteria

Phase 1 is the project's first encounter with reality. Some failures are recoverable; some indicate the design is wrong. The criteria below are stated explicitly so that a wrong outcome triggers a decision, not a slow drift.

6.1 Recoverable risks (revise and continue)

• SMT timeouts on real programs. If Z3 is too slow to discharge typical type-checking obligations within the 2-second budget (Phase 0 §2.14), the response is heuristic shortcuts (drop irrelevant assumptions, retry with simpler constraints) and a bigger budget. Annoying but not fundamental.
• MLIR/LLVM version churn. If the pinned LLVM version (Phase 0 §5.7) becomes a liability, upgrade it. Cost is updating the textual-emission code; bounded.
• OCaml-Z3 binding bugs. Vendor a known-good fork; document the workaround.
• DLPack ABI versioning. Pin to a specific DLPack version; document the upgrade path.

6.2 Architectural risks (consider revising the framework)

• Compiler can't produce correct LLVM for basic operations within 2–3 months. Indicates the IR design is wrong or the lowering strategy is wrong. The textual-emission approach (Phase 0 §5.3) was chosen for simplicity; if it's actually a constraint, switch to direct C++ API access.
• Memory manager performance is below 10× of PyTorch's caching allocator even after a pool implementation. Indicates the trait design is wrong, or the layered approach is too costly. Worth measuring the gap and deciding whether to optimize or redesign.
• GPU dispatch latency is too high to be useful (e.g., > 100µs per kernel launch). Indicates the runtime API has too much overhead. Probably fixable; if not, the FFI strategy needs rethinking.

6.3 Foundational risks (consider abandonment)

• The unified type system can't express common ML programs even with the four Phase 1 operation extensions. Indicates the refinement-typed-tensor framework is wrong. Real-world-examples §6 already surfaced one issue (matmul-batched-with-one-dim) that the Phase 1 extensions address; if more such issues emerge in Phase 1 implementation, the framework may need fundamental revision.
• Lean 4 verification of a small fragment is intractable. Indicates the operational semantics is wrong, or the proof technique is wrong. Worth retreating to translation validation or to a different formal tool (Coq, F*).
• Real-world programs (the transformer-block demo) hit too many escape hatches (Phase 0's controlled unsoundness in reshape; the variable-product axioms in attention). Indicates the type system trades off the wrong ergonomic-vs-soundness balance. Phase 1 is the place to discover this; revise Phase 0 if needed.

The last category triggers the abandonment-or-revision conversation. The first two categories trigger fix-it-or-revise.

7. Timeline

Phase 1 is 4–6 months part-time (10–15 hours per week, sustainable) or 2–3 months full-time.

Adding collaborators is mostly irrelevant in Phase 1. The work is deep and bottlenecked on design coherence; a second engineer adds coordination overhead more than throughput. Phase 5 onward (where parallel hardware backends, surface syntax tooling, and library implementations all want to happen at once) is where additional people start to help.

The part-time framing is realistic for someone in Antonette's situation: full-time GDIT work, multiple parallel projects, this as a research-and-implementation track that runs alongside everything else. The timeline assumes some weeks lose work to other commitments and some weeks have more focused time available. The 4–6 month range is wide enough to absorb that variance.

8. Section preview

The remaining six sections cover specific implementation tracks. Each will commit to specific code, specific APIs, specific acceptance criteria — in the same spec-style discipline as Phase 0, but for engineering deliverables rather than formal rules.

After Section 7, Phase 1 specification is complete. Implementation work can begin (or be reconsidered) against a well-defined target.

End of Phase 1, Section 1.