Codebase guide

This repository is specification plus an in-progress implementation: an OCaml compiler that already emits MLIR, a Rust runtime that is past a heap stub but not Phase-1-complete, and a Lean verification tree of theorem statements. For a visitor-facing snapshot, read 03-current-status.md first.

Top-level layout

Path	Role
`docs/10-spec/11-phase-0/` … `14-phase-3/`	Formal and implementation specs (source of truth for intended semantics).
`docs/10-spec/10-implementation-roadmap.md`	Phased roadmap.
`docs/00-foundation/03-current-status.md`	What is actually wired.
`docs/00-foundation/01-surface-kina.md`	Implemented bootstrap `.kina` surface.
`docs/00-foundation/02-surface-kina.md`	Older S-expression core still accepted by `Sexpr_parser`.
`src/compiler/`	OCaml: parse `.kina` or S-expressions → type formation → optional AD pass → textual MLIR.
`src/runtime/`	Rust: tensor/DLPack types, FFI dispatch, optional CUDA, experimental fibers.
`src/verification/`	Lean 4: statements; subject reduction is still `sorry`.
`scripts/`	Bash helpers: doc/code/MLIR snapshots, StoryLM-0 numeric checks.
`tests/compiler/fixtures/storylm0/`	Host-owned StoryLM-0 NPZ / vocab fixture for the 32-token rollout.
`tests/compiler/examples/`	`.kina` compile examples (not a stdlib).
`tests/snapshots/`	Golden MLIR and code-manifest hashes.
`docs/30-decisions/`	ADRs and change logs.
`website/`	Public site (`kina.acaldwell.dev`): docs, examples, status.
`experiments/storylm/`	Python / Hugging Face writing lab; not the Kina compiler.
`Justfile`	`just build-compiler`, `just test-compiler`, `just snapshot-mlir-golden`, …

The root README.md is the map for reading specs vs. implementation.

Compiler (`src/compiler/`)

Pipeline

Kina_parser_wrapper.parse_kina_program when the input ends in .kina; otherwise Sexpr_parser.parse_program.
Type_formation.check_program — structural typing + shape rules; produces typed IR (Ir_typed).
Ad_pass.transform_ad — restricted reverse-mode rewrite when a handle … with reverseMode form is present. The result type is the flat tuple (primal, g…).
Emitter.emit_tensor_program — prints an MLIR module. Tensor tuples become multi-result func.func (not MLIR tuple<>). A destructuring let (y, g) = … (LetTuple) names those SSA values.
Optional Pipeline.compile_mlir_to_so when the output path ends in .so.

The CLI is bin/main.exe: dune exec bin/main.exe -- <input.kina> <output.mlir|output.so>.

Library layout (`src/compiler/lib/`)

Dune uses (include_subdirs unqualified) so subdirectories contribute modules without extra prefixes in code.

Area	Modules (representative)	Responsibility
Types	`common/tensor_types.ml`	Shared `dtype`, `dim` (`Static` / `Symbolic`), `placement`, `tensor_type`.
Surface	`ast/ast_surface.ml`	Parser output: tensors, ops, `fn`/`let`/`if`/`while`, handlers.
IR	`ir/ir_typed.ml`	Typed programs carrying result types on each node.
Parser	`parser/kina_parser_wrapper.ml`, `kina_parser.mly`, `sexpr_parser.ml`	Bootstrap `.kina` (Menhir) and older S-expression core.
Elab	`elab/shape_ops.ml`, `elab/type_formation.ml`, `elab/ad_pass.ml`	Shape rules, checking, restricted AD.
MLIR	`mlir/emitter.ml`, `emitter_gpu.ml`, `pipeline.ml`	Textual lowering; optional LLVM `.so` driver.
Legacy / tests	`kina_core.ml`	Older tensor-literal-only path used by some unit tests.
SMT	`smt/discharge.ml`, `smt/obligation.ml`	Per-program Z3 context: dim equality, reshape volume, root `requires`.

Examples and goldens

tests/compiler/examples/*.kina — small programs exercised by just compile-examples and scripts/mlir-golden-check.sh.
tests/snapshots/mlir-golden/*.mlir — expected compiler output; refresh with just snapshot-mlir-golden when emission is intentionally changed.
tests/snapshots/code-manifest.sha256 — hashes of tracked compiler sources; refresh with just snapshot-code when those files change.

Grammar: docs/00-foundation/01-surface-kina.md. Example index: tests/compiler/examples/README.md.

Tests

src/compiler/test/compiler_tests.ml — smoke checks (legacy Kina_core, gather / take_along_axis / argmax lowering, I64).
src/compiler/test/expect/pipeline.ml — ppx_expect parse → check → emit pins.

Runtime (`src/runtime/`)

The compiler lowers the typed AST to textual MLIR (linalg, tensor, arith). When a .so is requested, Pipeline drives MLIR/LLVM tools. The Rust crate exposes tensor/DLPack types, FFI entry points (including GPU allocator hooks), and an experimental fiber module. See src/runtime/README.md and 03-current-status.md. This is not a completed Phase 1 runtime.

Verification (`src/verification/`)

Lake-based Lean 4 project; see src/verification/README.md. Toolchain via src/verification/lean-toolchain. Statements exist; the Phase 1 subject-reduction proof is still sorry.

OCaml documentation vs the public site

Mechanism	What it does here
`website/`	Public language site: status, learn, examples, syntax, spec.
`odoc` + `dune build @doc`	Local compiler-library HTML under `src/compiler/_build/default/_doc/_html/`.
`src/compiler/index.mld` / `examples.mld`	odoc landing pages.
Goldens	`tests/compiler/examples/*.kina` + `scripts/mlir-golden-check.sh`.

Commands: just doc-compiler or ./scripts/compiler-doc.sh (see src/compiler/README.md).

Quick commands

# Compiler
cd src/compiler && dune build && dune runtest
dune exec bin/main.exe -- ../../tests/compiler/examples/add_2d.kina /tmp/out.mlir

# From repo root
just build-compiler
just test-compiler
just validate-storylm0-forward
just validate-loss-ad
just validate-sgd
just validate-decoder-ad
just validate-nll-decoder-train
just validate-adamw
just validate-argmax
just validate-sample
just validate-kv-cache
just validate-generate
just validate-prefill
just validate-tmax
just validate-tp-vocab
just validate-tp-heads
just validate-tp-proj
just validate-rollout
just validate-train
just validate-decoder-adamw
just validate-mean-nll
just validate-trained-rollout
just doc-compiler
just snapshot-mlir-golden
just check-code-snapshot

Where to read next

Honest snapshot: 03-current-status.md
Specs: docs/10-spec/11-phase-0/README.md, docs/10-spec/12-phase-1/02-compiler-implementation.md
Compiler surface: src/compiler/README.md
Intentional drift: docs/30-decisions/31-code-change-log.md