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.

9. log_softmax and take_along_axis — StoryLM-0 loss slice. Stable log-softmax and axis-aware class selection from [B, T, V] logits. NLL is a composition, not a third primitive. Does not close Phase 1 exit criteria.

10. Restricted reverse-mode VJPs for StoryLM-0 loss — neg, log_softmax, and take_along_axis VJPs for the compiler AD pass. Scatter is IR-internal. Not Phase 2 handler AD. Does not close Phase 1 exit criteria.

11. Functional SGD — w' = w - broadcast(lr) * g. Not a primitive. Not AdamW. Does not close Phase 1 exit criteria.

12. reverseMode result ABI — Flat (primal, g…) tuple as MLIR multi-result func.func. Host .so grads via a wrapper fn. Does not close Phase 1 exit criteria.

13. Tuple projection — let (y, g) = … names reverseMode results so one program can be loss → VJP → SGD. No nested patterns. Does not close Phase 1 exit criteria.

14. Decoder-graph VJPs — Restricted reshape, variadic-batch matmul (including rank 4), and 2D gather VJPs. Gather cotangent is IR-internal ScatterAdd. Discrete I64 parameters are omitted from the result tuple. Does not close Phase 1 exit criteria.

15. NLL ∘ decoder train step — Compose Section 9 NLL with the Section 14 decoder graph; apply Section 11 SGD to every trainable weight. Seed ones on [B, T] NLL is sum, not mean. Does not close Phase 1 exit criteria.

16. Functional AdamW — Moments, bias correction, and decoupled weight decay as existing arithmetic. Not a primitive. Does not close Phase 1 exit criteria.

17. Deterministic argmax — Host reduce argmax with I64 result and lowest-index tie-break. No new token. Does not close Phase 1 exit criteria.

18. Seeded categorical sampling — Host Uniform(0, 1) + Gumbel-max + Section 17 argmax. Not a primitive and not a Random effect. Does not close Phase 1 exit criteria.

19. Functional KV-cache append — concat on the sequence axis plus one new-token attention. Not a primitive. Does not close Phase 1 exit criteria.

20. Host generation loop — Static-S decode plus host argmax. Not a primitive. Does not close Phase 1 exit criteria.

21. Prefill → decode handoff — Forward returns Kᵀ/V; host slices last logits and decodes one token. Not a primitive. Does not close Phase 1 exit criteria.

22. T_max padded scratch — Live cache padded to a static T_max with zeros, then sliced back. Not a primitive and not an in-place write. Does not close Phase 1 exit criteria.

23. 32-token checkpoint rollout — Host loop around a static T=36 forward plus argmax / Gumbel-max. Loads a versioned NPZ fixture. Does not close Phase 1 exit criteria.

24. Host train loop — 40 epochs of Section 15 SGD on a three-window toy corpus, then Section 23 greedy. Does not close Phase 1 exit criteria.

25. Decoder-wide AdamW — Section 16 applied independently to every trainable decoder weight after the Section 15 projection. Does not close Phase 1 exit criteria.

26. Mean NLL — Keepdims reduce_sum VJP plus host 1/(B·T). Not a reduce_mean VJP. Does not close Phase 1 exit criteria.

27. Trained 32-token fixture — Persist Section 24 SGD weights as storylm0-checkpoint-v1 and lock a 32-token taught rollout. Does not close Phase 1 exit criteria.

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 Phase 1, not a completion claim. The tree already has early Phase 2 syntax (if / while, handle) and a restricted compiler AD pass; Phase 1 exit criteria (GPU transformer vs PyTorch, performance band, Lean proof, runtime gates) remain open. Snapshot: docs/00-foundation/03-current-status.md.

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.