Specification

Codebase guide

This repository is mostly specification and design (docs/spec/, docs/design-memos/, …) plus three early implementation tracks: an OCaml compiler stub, a Rust runtime stub, and a Lean verification tree under src/. This document focuses on what lives where and how the runnable pieces fit together.

Top-level layout

Path	Role
`docs/10-spec/11-phase-0/`, `docs/10-spec/12-phase-1/`	Formal and implementation specs (source of truth for language semantics and build plan).
`docs/10-spec/10-implementation-roadmap.md`	Phased roadmap tracks.
`src/compiler/`	OCaml: parse S-expressions → type formation → emit textual MLIR (`linalg` / `tensor` / `arith`).
`src/runtime/`	Rust: placeholder / future execution and FFI (see `src/runtime/README.md`).
`src/verification/`	Lean 4: proofs and artifacts (see `src/verification/README.md`).
`scripts/`	Bash helpers: doc/code/MLIR snapshots, CI glue.
`tests/compiler/`	Compiler examples and error cases.
`tests/snapshots/`	Golden outputs: `mlir-golden/*.mlir`, `code-manifest.sha256`, etc.
`docs/decisions/`	ADRs and change logs when behavior or baselines shift intentionally.
`docs/00-foundation/02-surface-sexpr.md`	Phase 0 S-expression surface grammar (programs the compiler accepts today); `.kina` text syntax remains Phase 7.
`docs/architecture/`	Agent harness specifications and boundaries.
`Justfile`	Developer entry points: `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

End-to-end flow is a straight line (no separate driver library yet):

Sexpr_parser.parse_program — reads the whole file as a surface AST (Ast_surface).
Type_formation.check_program — structural typing + shape rules; produces typed IR (Ir_typed).
Emitter.emit_tensor_program — prints an MLIR module with func.func @main.

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

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`), `tensor_type`.
Surface	`ast/ast_surface.ml`	What the parser builds: tensors, ops, reshape, etc.
IR	`ir/ir_typed.ml`	Typed programs carrying result `tensor_type` on each node.
Parser	`parser/sexpr_parser.ml`	S-expression tokenizer + dispatch; `reduce_keep` vs `reduce` ordering matters.
Elab	`elab/shape_ops.ml`, `elab/type_formation.ml`	Broadcast/matmul/transpose/reduce/slice/concat/reshape rules; `check_expr` → `Ir_typed.program`.
MLIR	`mlir/emitter.ml`	Recursive lowering to `linalg.`, `tensor.`, `arith.*`.
Legacy / tests	`kina_core.ml`	Older tensor-literal-only parse/print path used by `compiler_tests.ml`; main binary uses the pipeline above.
SMT (stepping stone)	`smt/discharge.ml`, `smt/obligation.ml`	`Discharge.env` (shared Z3 context per program): `prove_dim_equal`, `prove_shape_volume_equal`, root `(requires (= …) …)` user axioms; richer obligations still in `obligation.ml`.

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 summary lives in src/compiler/README.md.

Tests

src/compiler/test/compiler_tests.ml — lightweight checks (e.g. Kina_core round-trip). Extend this as the pipeline gains coverage.

Runtime (`src/runtime/`)

The compiler lowers the typed AST directly to textual MLIR using the linalg, tensor, and arith dialects.

Execution occurs via an LLVM/MLIR lowering pipeline that converts textual MLIR to LLVM IR, compiles it into a shared object, and dynamically links against the Kina Rust Runtime (libkina_runtime.so).

The runtime utilizes the ctypes boundary to interact with Python test scripts, utilizing Unranked Memref Descriptors via the C-Interop Application Binary Interface (ABI). To inspect details on memory representations and runtime function mappings, consult docs/10-spec/13-abi.md.

Key files:

src/compiler/lib/mlir/emitter.ml: Emits textual MLIR for CPU tensors.
src/compiler/lib/mlir/emitter_gpu.ml: Emits textual MLIR for GPU-dispatched tensors, injecting _mlir_ciface_runtime_gpu_alloc_unranked allocator calls.
src/runtime/src/ffi/dispatch.rs: The Rust FFI boundary, exposing the GPU CUBLAS integration and allocators.

Verification (`src/verification/`)

Lake-based Lean 4 project; see src/verification/README.md. Toolchain via src/verification/lean-toolchain; just setup / PATH notes in root README.md.

OCaml and documentation (vs Rust’s `rustdoc`)

Rust’s rustdoc embeds API docs and doctest examples in /// comments and runs examples as tests. This repo uses in-house, Dune-driven odoc for the compiler library:

Mechanism	What it does here
`odoc` + `dune build @doc`	From `src/compiler/`, builds `_build/default/_doc/_html/`. Requires `odoc` on `PATH` (`opam install odoc`). No separate `(using odoc …)` stanza is needed on current Dune.
`src/compiler/dune`	`(documentation (package kina_compiler))` wires the package to odoc.
`src/compiler/index.mld`	Landing page (like a crate root): links into `{!modules: …}`.
`src/compiler/examples.mld`	Extra odoc page: copy-pastable S-expressions and OCaml snippets (parse → check → emit), plus pointers to `tests/compiler/examples/*.kina` and MLIR goldens.
Docstrings	`(** … *)` at the top of modules (and on values as you grow them); cross-refs with `{!Module}` / `{!type:…}` where useful.
`.mld` pages	Add more `.mld` files beside `index.mld` for tutorials; list them from the index when needed.
Runnable “examples”	*`tests/compiler/examples/.kina` + `scripts/mlir-golden-check.sh` (full MLIR goldens). `test/expect/pipeline.ml` uses `ppx_expect` (`dune runtest`) to pin the same strings as `src/compiler/examples.mld`—Rust-doctest-style for the API surface. `mdx`** remains optional for literate markdown.

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          # includes example compile + negative examples
just doc-compiler           # HTML API docs (needs: opam install odoc)
just snapshot-mlir-golden   # after intentional MLIR changes
just check-code-snapshot    # manifest drift

Where to read next

Specs: docs/10-spec/11-phase-0/README.md, docs/10-spec/12-phase-1/02-compiler-implementation.md (lowering story).
Compiler surface: src/compiler/README.md.
Intentional drift: docs/30-decisions/31-code-change-log.md.

If you later want generated API docs for src/compiler/lib, the next step is to add (documentation) fields and enable dune build @doc with odoc in the opam switch; this file can be linked from that index as the human overview.