Phase 1: Implementation — Index

The shape-typed core compiled end-to-end. Eight sections that take Phase 0's spec from paper to working language: a compiler in OCaml, a runtime in Rust, a parallel verification track in Lean 4, comprehensive testing, observability built in from day one, and the first version of the public API for external library authors.

Phase 1 is implementation work, not specification. Where Phase 0 committed to what the language is, Phase 1 commits to what gets built and how. The discipline is the same as Phase 0's — concrete decisions with rationale, tracked open issues, abandonment triggers stated explicitly — but the substance is engineering rather than formal rules.

The eight sections

1. Scope, Milestones, and Exit Criteria — What Phase 1 delivers, broken into three internal milestones. The end-to-end transformer block forward pass on GPU as the load-bearing acceptance criterion. Risks and abandonment criteria stated explicitly.

2. Compiler Implementation — OCaml end-to-end: parser, elaborator, type-checker, lowering pipeline, LLVM driver. The bidirectional type-checking discipline. Plain ADTs for the typed IR (not GADTs). The dramatic simplification of the GPU path: dispatch to library kernels rather than custom kernel generation.

3. Runtime Implementation — Rust end-to-end: MemoryResource trait + four implementations, Tensor struct with DLPack-compatible #[repr(C)] prefix, ~17 FFI entry points the compiler emits calls to, CUDA toolchain integration, the DLPack interop demo as the runtime's flagship validation.

4. Observability — Tracing, Logging, Diagnostics — The instrumentation infrastructure that makes Phase 1 debuggable from day one. Three pillars (tracing, logging, diagnostics). Logs for OCaml, tracing + nvtx-rs for Rust. Cross-system correlation via module IDs. Performance discipline: < 5% overhead in default mode, < 1% disabled.

5. Operation Set Extensions — Four new primitives that close the Phase 0 expressibility gap: variadic-batch matmul, gather, softmax-as-primitive, repeat_interleave. Each with typing rules, CPU lowering through MLIR linalg, GPU lowering through the runtime FFI, and tests. The "idiomatic transformer block in <200 lines" acceptance criterion.

6. Verification Track — Lean 4 mechanization running parallel to implementation. Phase 0 §1–§4 stated; basic proofs for §1 and §3; one non-trivial proof — subject reduction for the elementwise fragment — fully proven. Translation validation infrastructure committed; trusted-mode discharge for Phase 1, full discharge in Phase 6.

7. Testing, Quality, and Public ABI — The cross-cutting quality concerns. The testing pyramid (unit, integration, golden vs. PyTorch, GPU end-to-end). Two-tier CI (standard always; GPU on PRs touching GPU paths). Performance regression infrastructure consuming observability traces. Three ABI categories with snapshot tests. Library author's guide v0.1 with worked example as the load-bearing acceptance criterion.

8. Exit Criteria and Phase 2 Entry — Consolidated acceptance criteria from all seven preceding sections. The judgment-call exit criterion in operational terms (five questions). Risks revisited with implementation context. Phase 2 entry conditions and the handoff manifest. The arc forward — what Phase 2 starts with and where the project goes after.

Key commitments

The decisions that shape everything Phase 1 builds:

Cross-cutting commitments worth elevating

A few patterns recur across multiple sections and deserve specific attention:

The forbidden temptations in Phase 1. Section 1 §5 forbids tape-based AD, sharding type prototypes, sparsity primitives, tile-IR work — each has a designated framework in a designated phase. Cutting corners in Phase 1 short-circuits the design work that gives them shape. This discipline is hard to maintain in solo projects.

Cheap-now, expensive-later commitments. The DLPack ABI prefix (Section 3 §5), the runtime FFI design discipline (Section 3 §6), the translation-validation obligation format (Section 6 §6), the ABI snapshot tests (Section 7 §8.3). Each costs little to commit to during Phase 1; each is expensive or impossible to retrofit.

Load-bearing acceptance criteria. Three single-criterion tests that operationalize the rest: the transformer block forward pass on GPU (§1), the DLPack interop demo (§3), the library author's guide worked example (§7). Each can be verified independently; each fails if the corresponding architectural commitment was wrong.

What Phase 1 does not include

Phase 1's scope is bounded. The following are deliberately deferred:

• Effects (mutation, randomness, async memory). Phase 2.
• Reverse-mode AD. Phase 2.
• Control flow (if, while). Phase 2.
• Sharding / distribution. Phase 3.
• Sparsity / structured tensors. Phase 4.
• Custom kernel authoring (tile IR). Phase 5.
• Verified compilation passes (full proofs). Phase 6.
• Surface syntax. Phase 7.
• Mixed-precision matmul. Phase 2.
• Multi-GPU support. Phase 3.
• Compiler self-hosting. Phase 8+, possibly never.

This 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.

Suggested reading order

For a first pass: read in numerical order, 1 → 8. Sections 2 and 3 are the longest; allocate accordingly.

For someone implementing Phase 1: Section 1 first to internalize the milestones; then Sections 2 and 3 in detail; then Section 4 (observability is cross-cutting); then Sections 5–7 as the work in each domain begins; Section 8 for the exit decision.

For someone evaluating whether to commit to Phase 1 implementation: Section 1 (scope and exit criteria), Section 8 (the consolidated acceptance criteria), then a quick pass through the open issues sections of 2–7 (the §13–§14 of each) to surface the cumulative engineering risk.

For someone reviewing the design without intent to implement: Section 1 for framing; Section 8 for synthesis; then drill into whichever section's domain interests them.

Phase 1 exit criteria

Section 8 §2 consolidates the criteria. Briefly:

• All technical criteria from Sections 2–7 met.
• The end-to-end transformer block forward pass on GPU produces correct results within FP tolerance.
• The idiomatic transformer block expressible in under 200 lines of language code.
• Performance within 3–5× of PyTorch.
• The judgment-call exit criterion (Section 8 §3) answered "yes" — the foundation feels sturdy enough to bear Phase 2's weight.

Phase 1 is the gateway phase. Phase 0 was paper, cheap to walk away from. Phases 2–7 build on Phase 1 in compounding ways. Phase 1's exit decision is the moment the project commits to the framework as built; after Phase 1, revision becomes more expensive every phase.

Related documents

• ../phase-0/ — the strict spec Phase 1 implements.
• ../forward-tracks/ — architectural commitments that extend Phase 0 without modifying it (CUDA-native, ecosystem architecture, Arrow + typed dataframes, bootstrap and self-modeling, surface design and personas). Phase 1 is most constrained by the first four; the surface track mainly informs Phase 7.
• ../companions/ — examples and walkthroughs that ground the Phase 0 spec in real programs. Many of Phase 1's acceptance criteria refer back to these.
• ../implementation-roadmap.md — the original phased plan that Phase 1 inherits and refines.

What's next

If Phase 1 is accepted: Phase 2 begins with the AD-as-handler proof of concept (per the bootstrap-and-self-modeling forward track §6). The full Phase 2 plan is written when Phase 2 is nearing.

If Phase 1 surfaces design issues: revise the affected Phase 0 or Phase 1 sections; re-evaluate; restart Phase 1 implementation. The cost of revision is large but bounded; the cost of building Phase 2+ on patched foundations is much larger.

If the project is paused or abandoned: the Phase 0 spec, the Phase 1 implementation work to that point, and the forward-track documents stand as a research artifact regardless. The thesis was tested honestly; whatever the answer, the path forward is clear.