Specification

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 compiler/ that intentionally implements a strict subset first: structural shape reasoning, textual MLIR emission, and S-expression surface syntax.

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

S-expression programs (compiler/lib/parser/sexpr_parser.ml): tensor literals, add / mul / sub / div, matmul, cast, unary, transpose, reduce / reduce_keep, broadcast, slice, concat, reshape, root (requires (= …) …). Normative grammar and examples: docs/00-foundation/02-surface-sexpr.md; example index: compiler/examples/README.md; pretty-print: Ast_surface.pp_expr. No separate user-facing .kina surface (still Phase 7 per §05).

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, and min (float via arith.maximumf / minimumf with IEEE ±∞ fills; signed int via arith.maxsi / minsi with extremal fills). Other names (e.g. prod, argmax) fail at type-check or emit until added.

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

Tests and goldens

compiler/test/expect/pipeline.ml — ppx_expect strings for representative programs (parse → type → emit).
compiler/examples/*.kina plus 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)
`runtime/`	`Heap` + `TensorHandle`; `libloading` helper `dynamic::call_nullary_i32`; integration test loads `smoke_lib/kina_smoke.c` built by `runtime/build.rs` (Phase 0 §8.4 smoke).
`verification/`	Lake project with `Spec/*.lean`; aligns with “Lean spec compiles” direction — detail in exit criteria checklist.
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-07-17 (align with repository state).