Phase 0 review checklist — coverage before freeze
Use this document to systematically close gaps in Phase 0 so the foundation does not need rework later. Work top-to-bottom; check boxes as items are resolved (spec text updated, ADR filed, or explicitly accepted as deferred with no ambiguity).
Normative spec remains the five section files 01–05 and README.md. This file is process only; if it disagrees with a section file, the section file wins—then update this checklist.
Last checklist pass: open issues triaged in spec + decisions/toolchain-pins.md added; §4 exit criteria refreshed against the repository (2026-05-09).
1. How to use
- Complete §2 Open issues register first: every row must end in one of: Resolved in spec, ADR + spec note, Deferred to Phase N (section cite), Implementation-only (Section 5).
- Run §3 Preview paragraphs: forward-looking text at the end of sections should not contradict later sections.
- Run §4 Exit criteria vs repository when you approach engineering “Phase 0 complete.”
- Optional: §5 Sign-off before treating Phase 0 as frozen for Phase 1.
2. Open issues register
| ID | Source | Topic | Status / next action |
|---|---|---|---|
| O-01-1 | §01 §9 #1 | Reshape variable-product | Resolved §02 §10. |
| O-01-2 | §01 §9 #2 | Default α ≥ 1 |
Resolved §02 §15–§16; §01 §6 cross-ref. |
| O-01-3 | §01 §9 #3 | Refinement canonicalization | Split: SMT (§03 §8.6) vs impl. total order (§05). |
| O-01-4 | §01 §9 #4 | requires vs inline |
Resolved §02 §15. |
| O-02-1 | §02 §16 #1 | Operation “overloading” | Resolved Phase 0: admissibility tables; traits later + ADR (§02 §16, decisions table 2.9). |
| O-02-2 | §02 §16 #2 | Value mul vs shape * |
Resolved §02 §2.1. |
| O-02-3 | §02 §16 #3 | Reduction axis literal-only | Accepted limitation §02 §16 #3 (macros / Phase 7 sugar). |
| O-02-4 | §02 §16 #4 | FP reduction order | Deferred §04 §6–§8. |
| O-02-5 | §02 §16 #5 | Empty tensors | Resolved §02 §16 #5 + §01 §6 paragraph on α ≥ 0 override. |
| O-03-1 | §03 §11 #1 | ∀ in subtyping / SMT | Implementation §05 §11 (item 4). |
| O-03-2 | §03 §11 #2 | Mutual recursion | Implementation §05 §11 (item 5). |
| O-03-3 | §03 §11 #3 | Effect rows | Deferred Phase 2 §03 §11 #3. |
| O-03-4 | §03 §11 #4 | Negative refinements | Implementation §05 §11 (item 6) + §03 §11. |
| O-04-1 | §04 §8 #1 | Heap deallocation | Deferred Phase 5+. |
| O-04-2 | §04 §8 #2 | Well-typed heap | Resolved §04 §3.3; §04 §8 item 2 updated. |
| O-04-3 | §04 §8 #3 | Termination / divergence | Process: revisit when Phase 2+ adds control flow. |
| O-04-4 | §04 §8 #4 | Bit reproducibility | Non-goal Phase 0; Phase 6+ policy. |
| O-05-1 | §05 §11 #1 | MLIR/LLVM pin | ADR decisions/toolchain-pins.md; CI when repo exists. |
| O-05-2 | §05 §11 #2 | ocaml-z3 / Z3 pin | ADR toolchain-pins.md; CI when repo exists. |
| O-05-3 | §05 §11 #3 | Lean / mathlib pin | ADR toolchain-pins.md; CI when repo exists. |
3. Preview paragraphs (forward references)
| Location | Check |
|---|---|
| §01 §10 | Ten ops + explicit broadcast — done (prior pass). |
| §02 §18 | Matches §03 — done (prior pass). |
| §03 §13 | Matches §04 incl. §3.3 heap + §7.0 — done (this pass). |
| §04 §10 | Matches §05 (OCaml/Rust/Lean, textual MLIR) — done (unchanged; still accurate). |
4. Exit criteria vs repository (05 §9)
| # | Criterion | Repo check |
|---|---|---|
| 1 | Five specs written & reviewed | Docs exist (phase-0/01–05); second-reader review is a process checkbox. |
| 2 | Repository skeleton + build orchestration | compiler/, runtime/, verification/, Justfile — present. |
| 3 | Compiler: parse, type-formation, MLIR emission | Present — S-expr pipeline, structural shape_ops, textual MLIR; examples + snapshots/mlir-golden/. Subset of §02 ops/casts vs normative tables — see decisions/phase-0-reference-implementation-status.md. |
| 4 | Runtime stub: handles, dlopen, smoke test | runtime/ — Heap + unit tests; libloading + integration test loading smoke_lib/kina_smoke.c built by build.rs (see runtime/README.md). |
| 5 | Lean spec compiles (sorry OK) |
verification/ Lake project present (Spec/*.lean). |
| 6 | CI green | Deferred — no in-repo workflow; hosted CI blocked by org/billing policy for now. Gate: local just test (or just test-compiler, just test-runtime, just test-verification). Revisit when billing allows. |
| 7 | Author judgment to proceed | Subjective. |
5. Cross-corpus consistency (non-normative)
| Artifact | Check |
|---|---|
../phase-1/ |
Ten core ops, reduce rules, decisions/ paths — aligned. |
../companions/ |
Examples use explicit broadcast in IR; surface sugar labeled — spot-check when editing. |
../decisions/ |
toolchain-pins.md records LLVM/Z3/Lean policy; further ADRs as needed. |
6. Recommended work order (minimize backtracking)
Spec ambiguities (overloading, heap, mul)Addressed in this checklist pass.Preview audit §01–§04Done.ADRs O-05-1–3 policydecisions/toolchain-pins.md.Implementation stubs for Phase 0 exit criteriaIn progress — compiler/runtime/verification trees exist; see §4 anddecisions/phase-0-reference-implementation-status.mdfor gaps (full §02 op surface, refinements, …). S-expression surface grammar:../docs/00-foundation/02-surface-sexpr.md. CI: consciously deferred (§4 #6).- Second-reader review of
01–05(process).
7. Sign-off (optional)
Before freezing Phase 0 for Phase 1:
- Every Open design / spec gap row in §2 closed or explicitly deferred with phase cite (as of last pass).
- §3 preview checks pass.
- Second reader has skimmed
01–05(or issues logged) — seesecond-reader-pass-2026-05-09.md(limits of this pass stated there). - Exit criteria §4 either satisfied or consciously deferred with written rationale — §4 table +
decisions/phase-0-reference-implementation-status.md; CI deferral in §4 #6.
Maintainers: update the Status column as items close; keep this file honest.