Phase 0 reference implementation status (OCaml compiler)

Context. Phase 0 Sections 1–5 describe the full calculus: SMT-backed obligations (Γ ⊨ φ), refinement sets, the complete operation admissibility tables, and reshape volume as an asserted axiom with a runtime backstop. The repository ships an OCaml compiler under src/compiler/ that implements a subset: structural shape reasoning, textual MLIR emission, a bootstrap .kina surface, and the older S-expression core. Visitor-facing snapshot: docs/00-foundation/03-current-status.md.

Decision. Treat this document as the non-normative bridge between the normative specs (phase-0/01–05) and the tree. The specs remain authoritative for intent; this ADR records what is wired today so checklist and exit-criteria rows stay honest. When implementation catches up, update this file (or supersede it with finer-grained ADRs).

Consequences. Reviewers use this mapping for gap analysis; phase-0/REVIEW-CHECKLIST.md §4 can cite it. Divergence here does not relax the formal spec until an explicit spec amendment or ADR says so.

Shape and SMT (Sections 1–2, Section 5 §4)

Topic	Normative spec	`compiler/` today
`Γ ⊨ φ` discharge	Z3 (`ocaml-z3`), 2s timeout policy (§02 §14)	Partial — dimension equality + root `requires`. `compiler/lib/smt/discharge.ml` builds one Z3 context per `check_program` session. Dimension equality (broadcast / concat / matmul): structural fast path, then Z3 with default `>= 1` axioms plus user equalities from `(requires (= d₁ d₂) … (body))` at program root. Reshape volume (`∏` axes): static product when fully static; otherwise Z3 on nonlinear products with the same axioms. SAT/UNKNOWN messages include counterexamples where applicable. Full refinements and non-equality `requires` remain future work.
Reshape volume	Asserted `volEq` axiom; refinements dropped per §02 §10	Typed: static-only product or Z3 when symbols appear (same context as dim checks). MLIR: `tensor.reshape` lowering still requires a fully static target shape list; symbolic targets fail at emit with an explicit error (typed programs may still be useful for API-only checks).
Refinements `R` on tensor types	Carried through rules; SMT for implication (§03)	Not represented in the typed IR used for MLIR emission beyond dtype + shape list.

Surface syntax

Two parsers share Ast_surface:

Bootstrap .kina (src/compiler/lib/parser/kina_parser.mly, selected when the file extension is .kina): the public examples and site. Grammar: docs/00-foundation/01-surface-kina.md. Also accepts fn / let / if / while, effect rows, perform / handle. Tensor { … } payloads are parsed and discarded.
S-expression core (src/compiler/lib/parser/sexpr_parser.ml): still accepted. Grammar: docs/00-foundation/02-surface-kina.md.

Phase 7 of the roadmap still owns a frozen grammar, inference, and tooling. The .kina surface is a bootstrap pulled forward, not that freeze. Example index: tests/compiler/examples/README.md. Pretty-print: Ast_surface.pp_expr (S-expression shaped).

Operation coverage vs §02 “included” lists

Elementwise binary (§06). Parser and IR: add, mul, sub, div, pow (all floats; float8 via f32 math.powf), max / min (f32/f16/bf16 via linalg; float8 via arith.maximumf / minimumf; signed int), comparisons eq–ge, bitwise_*, rem (signed int), frem (floats; float8 via f32). Reduce max / min on float8 uses ±∞ f32 constants truncated to the float8 element type as fill identities. The full §06 catalog may still list ops not wired here.

Elementwise unary (§04). Type admissibility (type_formation.ml unary_ok) lists many names aligned with the spec. MLIR lowering (emitter.ml) implements relu, neg, abs on floats (f32/f16/bf16 via linalg; float8 via extf → f32 scalar op → truncf in linalg.generic, including relu with arith.maximumf vs 0 f32), exp, log, sqrt, rsqrt, tanh (named linalg on f32/f16/bf16; float8 via math.* on f32 bridge), sigmoid, silu, gelu (f32/f16/bf16 linalg.generic; float8 runs the same f32 bodies after extf of %a0), and bitwise_not (int xor −1; bool xor true). Reduce mean on float8 uses the same arith.addf combine + linalg.mul scale path as wider floats once the tensor uses float8 element type.

Cast (§05). Formation is permissive (dtype change, shape preserved). Emitter supports a widened cast matrix: F32 hub for sub-f32 floats (extf / truncf), F32↔I64/I32/I16/I8/I4 float↔int (fptosi / sitofp), F32↔F8 (truncf / extf), int width (extsi / trunci), bool↔int (extui / trunci), bool→float via I32, float→bool via F32→I32→i1; uncommon pairs may still fail at emit until added. I64 is currently host-only: device-placement I64 is rejected until matching runtime wrappers and kernels exist.

Reduce (§08). Parser accepts arbitrary reduction op strings; type_formation.reduce_ok gates supported ops. Emitter lowers sum, mean (float), max, min (float via arith.maximumf / minimumf with IEEE ±∞ fills; signed int via arith.maxsi / minsi with extremal fills), and host argmax (result dtype I64; lowest-index tie-break via strict ogt / sgt and linalg.index; see Phase 1 Section 17). Other names (e.g. prod, argmin) fail at type-check or emit until added. Device argmax is rejected at type-check.

Matmul (§07). Rank-3 batched and rank-2; dtype must match. Higher-rank matmul remains deferred per spec.

Transpose, broadcast, slice, concat. Implemented end-to-end with the structural limitations noted in shape_ops.ml (e.g. slice/concat axes requiring static dimensions where checked). Host broadcast left-pads the source and maps each size-1 source axis to affine 0 (Phase 0 §11), including rank-changing [1, 1] → [1, 4, 8]. Host concat with static shapes lowers to tensor.empty plus two tensor.insert_slice ops (LLVM 18 one-shot-bufferize has no tensor.concat pattern). Host extract_slice .so lowering runs --lower-affine after --expand-strided-metadata.

Tests and goldens

src/compiler/test/expect/pipeline.ml — ppx_expect strings for representative programs (parse → type → emit).
tests/compiler/examples/*.kina plus tests/snapshots/mlir-golden/*.mlir — checked by scripts/mlir-golden-check.sh and just compile-examples.

These track regression coverage, not a complete enumeration of §02.

Runtime and verification (§05 §8.4–8.5)

Artifact	Status (high level)
`src/runtime/`	Past the Phase 0 heap stub: DLPack/tensor types, FFI dispatch, optional CUDA, experimental fibers, plus the original smoke `libloading` path. Not the completed Phase 1 runtime contract.
`src/verification/`	Lake project with `Spec/*.lean` statements. Subject reduction remains `sorry`.
CI	Deferred (hosted CI / org billing). No `.github/workflows` in-tree; use local `just test` and language-specific targets as the gate until CI is affordable or runs elsewhere (e.g. self-hosted).

Last updated: 2026-08-23 (align with repository state; see 03-current-status.md).