Implementation / code snapshot change log

Use this file when intentional changes alter tracked source files or golden compiler output captured under snapshots/.

Entry template

• Date:
• Scope (paths / examples):
• Reason for change:
• Spec / docs linkage (if any):
• Follow-up actions:

Entries

• Date: 2026-06-06

• Scope (paths / examples): docs/10-spec/13-phase-2/README.md, docs/10-spec/13-phase-2/02-effect-handler-infrastructure.md, docs/10-spec/13-phase-2/03-automatic-differentiation.md, docs/10-spec/13-phase-2/04-control-flow-and-iteration.md.

• Reason for change: Draft Phase 2 Specifications in Kina Syntax:

  1. Draft 02-effect-handler-infrastructure.md defining algebraic effect declarations, rows, and runtime fiber model using Kina syntax.
  2. Draft 03-automatic-differentiation.md specifying reverse-mode AD as a handler, pullback propagation, custom gradients, and IFT solver loops.
  3. Draft 04-control-flow-and-iteration.md detailing if conditionals, while loops with linear loop-carried variables, dynamic branching tape, and checkpointing optimizations.
  4. Link the drafted files in README.md.

• Spec / docs linkage (if any): Phase 2 milestones.

• Follow-up actions: None.

• Date: 2026-06-06

• Scope (paths / examples): src/compiler/dune-project, src/compiler/lib/dune, src/compiler/lib/parser/dune, src/compiler/lib/parser/kina_lexer.mll, src/compiler/lib/parser/kina_parser.mly, src/compiler/lib/parser/kina_parser_wrapper.ml, src/compiler/bin/main.ml, Justfile, tests/compiler/examples/*.kina, docs/00-foundation/01-surface-kina.md, tests/snapshots/code-manifest.sha256.

• Reason for change: Implement .kina Surface Language parser & Port examples:

  1. Add Menhir and ocamllex support to dune configurations.
  2. Implement lexical and parser grammar mapping .kina syntax to AST nodes (Ast_surface.expr).
  3. Integrate the .kina parser into the compiler CLI binary, supporting both .kina and .kina file extensions.
  4. Port 25+ representative S-expression examples to .kina format to achieve 100% feature coverage of the new parser, and verify MLIR compilation matches.

• Spec / docs linkage (if any): Phase 7 surface language goals.

• Follow-up actions: None.

• Date: 2026-05-30

• Scope: compiler/lib/dune, compiler/lib/parser/parser_utils.ml, compiler/lib/parser/parser_types.ml, compiler/lib/parser/sexpr_parser.ml, compiler/lib/mlir/emitter_utils.ml, compiler/lib/mlir/emitter_affine.ml, compiler/lib/mlir/emitter_math.ml, compiler/lib/mlir/emitter.ml, compiler/test/compiler_tests.ml, compiler/test/expect/pipeline.ml, Justfile, scripts/ci.sh, scripts/install-lean.sh, runtime/Cargo.toml, runtime/build.rs, runtime/src/lib.rs, runtime/src/error.rs, runtime/tests/smoke_dlopen.rs, runtime/tests/dlpack_roundtrip.rs, runtime/tests/tensor_lifecycle.rs, snapshots/code-manifest.sha256.

• Reason: Modularization & Static Analysis:

  1. Split sexpr_parser.ml and emitter.ml into sub-modules for parser utils/types and emitter utils/affine/math.
  2. Configure strict compiler warnings-as-errors in src/compiler/dune.
  3. Enforce strict cargo clippy --all-targets -- -D warnings on the Rust runtime.
  4. Fix FFI safety documentation clippy warnings, C-string literals, needless range loops, and cell allocations.
  5. Add lint targets to root Justfile and integrate static analysis into scripts/ci.sh.
  6. Correct setup paths in scripts/install-lean.sh for lean-toolchain.

• Spec / docs linkage: Phase 2 modularization and quality controls.

• Follow-up actions: None.

• Date: 2026-05-09

• Scope: compiler/lib/mlir/emitter.ml (float8 unary bridges: relu/neg/abs, exp/log/sqrt/rsqrt/tanh, sigmoid/silu/gelu), compiler/examples/unary_*_f8e4m3.kina, reduce_mean_f8_axis0.kina, snapshots/mlir-golden/*.mlir, scripts/mlir-golden-*.sh, Justfile, compiler/test/expect/pipeline.ml, docs/00-foundation/02-surface-sexpr.md, decisions/phase-0-reference-implementation-status.md, compiler/examples/README.md, decisions/code-change-log.md, snapshots/code-manifest.sha256.

• Reason: Float8 elementwise unaries lowered via f32 (extf / truncf); nonlinear ops use math.* or duplicated f32 arith bodies; document reduce mean on float8.

• Spec / docs linkage: Phase 0 §04 unary table.

• Follow-up actions: native float8 linalg where profitable; verify numeric accuracy vs hardware float8 kernels.

• Date: 2026-05-09

• Scope: compiler/lib/ast/ast_surface.ml, compiler/lib/ir/ir_typed.ml, compiler/lib/parser/sexpr_parser.ml, compiler/lib/elab/type_formation.ml, compiler/lib/mlir/emitter.ml, new compiler/examples/*.{sexpr} (float8 max/pow/reduce, rem, frem), snapshots/mlir-golden/*.mlir, scripts/mlir-golden-*.sh, Justfile, compiler/test/expect/pipeline.ml, docs/00-foundation/02-surface-sexpr.md, decisions/phase-0-reference-implementation-status.md, compiler/examples/README.md, decisions/code-change-log.md, snapshots/code-manifest.sha256.

• Reason: Float8 elementwise max/min (arith.maximumf/minimumf), pow/frem via f32 bridge; reduce max/min float8 fill from ±∞ f32 truncated to element type; surface rem / frem (remsi / remf).

• Spec / docs linkage: Phase 0 §06 remainder-style ops; float8 lowering notes in ADR.

• Follow-up actions: reduce mean/sum on f8 if needed; fmod naming vs spec.

• Date: 2026-05-09

• Scope: compiler/lib/ast/ast_surface.ml, compiler/lib/ir/ir_typed.ml, compiler/lib/parser/sexpr_parser.ml, compiler/lib/elab/type_formation.ml, compiler/lib/mlir/emitter.ml, compiler/examples/{pow_f32,max_i32,min_f32,eq_f32,bitwise_and_i32,cast_f16_bf16,cast_i8_i32,cast_bool_i32}.kina, snapshots/mlir-golden/*.mlir, scripts/mlir-golden-*.sh, Justfile, compiler/test/expect/pipeline.ml, compiler/examples/README.md, docs/00-foundation/02-surface-sexpr.md, decisions/phase-0-reference-implementation-status.md, decisions/code-change-log.md, snapshots/code-manifest.sha256.

• Reason: More elementwise binary ops (pow, max/min, compares eq–ge, bitwise and/or/xor) end-to-end; widen cast lowering (float/int/bool bridges and F32 hub for sub-f32).

• Spec / docs linkage: Phase 0 §05 cast, §06 elementwise binary.

• Follow-up actions: float8 max/min/pow; remainder/mod-style ops if added to surface.

• Date: 2026-05-09

• Scope: compiler/lib/mlir/emitter.ml, compiler/examples/unary_*.{sexpr}, snapshots/mlir-golden/unary_*.mlir, scripts/mlir-golden-*.sh, Justfile, compiler/test/expect/pipeline.ml, compiler/examples/README.md, decisions/phase-0-reference-implementation-status.md, docs/00-foundation/02-surface-sexpr.md, decisions/code-change-log.md, snapshots/code-manifest.sha256.

• Reason: Lower additional unary ops to MLIR: linalg.log/sqrt/rsqrt/tanh; sigmoid/silu/gelu via linalg.generic + math; int bitwise_not; examples + goldens + pipeline test.

• Spec / docs linkage: Phase 0 §04 unary table; float8 still deferred at emit.

• Follow-up actions: float8 elementwise; optional linalg/math version gates in CI with mlir-opt.

• Date: 2026-05-09

• Scope: docs/00-foundation/02-surface-sexpr.md, compiler/examples/README.md, compiler/lib/ast/ast_surface.ml (pp_dim, pp_shape, pp_expr), compiler/test/expect/pipeline.ml, compiler/README.md, docs/00-foundation/00-CODEBASE.md, decisions/phase-0-reference-implementation-status.md, decisions/code-change-log.md.

• Reason: Surface-first documentation for the Phase 0 S-expression IR plus canonical pretty-printing; explicit backlog pointer for subsequent compiler work.

• Spec / docs linkage: Phase 7 vs Phase 0 surface (phase-0/README.md, 05-implementation-infrastructure.md).

• Follow-up actions: execute “Compiler next” list in docs/00-foundation/02-surface-sexpr.md (unary/cast/reduce/…).

• Date: 2026-05-09

• Scope: compiler/lib/smt/discharge.ml, compiler/lib/elab/shape_ops.ml, compiler/lib/elab/type_formation.ml, compiler/lib/ast/ast_surface.ml, compiler/lib/parser/sexpr_parser.ml, compiler/lib/mlir/emitter.ml, compiler/test/expect/pipeline.ml, compiler/README.md, decisions/phase-0-reference-implementation-status.md, snapshots/code-manifest.sha256.

• Reason: Root (requires (= …) …) user equalities into a shared Z3 context; thread Discharge.env through shape rules; reshape volume via Z3 when shapes are not all-static; reject symbolic reshape targets at MLIR emit.

• Spec / docs linkage: Phase 0 §02 §14–§15, reshape volEq.

• Follow-up actions: nested or non-equality requires; dynamic reshape lowering when target dims are symbolic.

• Date: 2026-05-09

• Scope: compiler/dune-project, compiler/lib/dune, compiler/lib/smt/discharge.ml, compiler/lib/elab/shape_ops.ml (comment), compiler/lib/smt/obligation.ml, compiler/test/expect/pipeline.ml, decisions/phase-0-reference-implementation-status.md, decisions/code-change-log.md, docs/00-foundation/00-CODEBASE.md, compiler/README.md, phase-0/02-core-operations-and-typing.md (§19), snapshots/code-manifest.sha256.

• Reason: Link ocaml-z3 (z3 opam) and discharge non-structural dimension equalities with a fresh solver context (2s timeout, default >= 1 symbolic axioms, SAT counterexamples); refresh expect + code manifest.

• Spec / docs linkage: Phase 0 §02 §14–§15.

• Follow-up actions: reuse one Z3 context per type-check session where appropriate; extend discharge for user requires and full Γ ⊨ φ.

• Date: 2026-05-09

• Scope: compiler/lib/smt/discharge.ml, compiler/lib/elab/shape_ops.ml, compiler/lib/elab/type_formation.ml (reduce_ok), compiler/lib/mlir/emitter.ml (reduce max/min), compiler/examples/reduce_max_axis1.kina, reduce_min_axis0.kina, compiler/test/expect/pipeline.ml, snapshots/mlir-golden/reduce_*.mlir, scripts/mlir-golden-*.sh, Justfile, compiler/lib/smt/obligation.ml, docs/00-foundation/00-CODEBASE.md, compiler/README.md, decisions/phase-0-reference-implementation-status.md, snapshots/code-manifest.sha256.

• Reason: Dimension discharge API (Z3 stepping stone; pure symbolic messages today); reduce [max]/[min] lowering and tests; clearer broadcast/matmul type errors.

• Spec / docs linkage: Phase 0 §02 §11–§14, §08 reduce ops.

• Follow-up actions: extend [reduce_ok] for [prod] etc.; reuse a shared Z3 context for dimension checks where appropriate.

• Date: 2026-05-09

• Scope: phase-0/second-reader-pass-2026-05-09.md, phase-0/README.md (exit criteria + reference-impl pointer), phase-0/REVIEW-CHECKLIST.md (§7 sign-off).

• Reason: Close second-reader and §4 exit-criteria checklist items with a dated audit log; align README with deferred CI and partial compiler/ reality.

• Spec / docs linkage: phase-0/REVIEW-CHECKLIST.md §7.

• Follow-up actions: optional named human reviewer appendix to the second-reader log if governance requires it.

• Date: 2026-05-09

• Scope: phase-0/REVIEW-CHECKLIST.md (§4 #6, §6), decisions/phase-0-reference-implementation-status.md (CI row).

• Reason: Record that hosted CI is consciously deferred (org/billing); Phase 0 §9 #6 satisfied in spirit via documented local gates until CI is unblocked.

• Spec / docs linkage: phase-0/05-implementation-infrastructure.md §8.6 / §9 #6.

• Follow-up actions: add .github/workflows (or other CI) when billing/policy allows; optional self-hosted runner with zero SaaS cost.

• Date: 2026-05-09

• Scope: runtime/build.rs, runtime/smoke_lib/kina_smoke.c, runtime/src/dynamic.rs, runtime/tests/smoke_dlopen.rs, runtime/Cargo.toml (libloading), runtime/README.md, runtime/Cargo.lock, phase-0/REVIEW-CHECKLIST.md (§4 runtime row).

• Reason: Phase 0 §8.4 — tensor heap plus libloading smoke path calling a C entry point from a built shared library.

• Spec / docs linkage: phase-0/05-implementation-infrastructure.md §8.4; REVIEW-CHECKLIST.md §4.

• Follow-up actions: when the compiler emits .so artifacts, add an integration test that loads that output instead of (or in addition to) the C smoke stub.

• Date: 2026-05-09

• Scope: decisions/phase-0-reference-implementation-status.md, decisions/README.md, phase-0/02-core-operations-and-typing.md (§19 non-normative pointer), phase-0/05-implementation-infrastructure.md (§8.3 status note), phase-0/REVIEW-CHECKLIST.md (§4 exit criteria vs repo, §6–§7 cross-refs).

• Reason: Align review checklist and specs with the real tree; record compiler subset vs normative §02 without changing formal rules.

• Spec / docs linkage: Phase 0 §02 §19; §05 §8.3; REVIEW-CHECKLIST.md §4.

• Follow-up actions: add CI workflow when ready; narrow or extend §02 “included” lists only via explicit spec edits if desired.

• Date: 2026-05-09

• Scope: compiler/lib/mlir/emitter.ml (integer [neg] via [linalg.sub] and zero tensor; boolean [neg] via [linalg.generic] + [arith.xori]), compiler/examples/unary_neg_i32.kina, compiler/examples/unary_neg_bool.kina, snapshots/mlir-golden/unary_neg_*.mlir, Justfile, scripts/mlir-golden-*.sh, compiler/test/expect/pipeline.ml (parse failures + unary neg expects), snapshots/code-manifest.sha256.

• Reason: Lower signed integer and logical negation for unary [neg]; extend pipeline and golden coverage.

• Spec / docs linkage: phase-0/02-core-operations-and-typing.md (unary ops).

• Follow-up actions: optional [neg] on other integer widths in end-to-end tests if literals differ.

• Date: 2026-05-09

• Scope: compiler/lib/elab/shape_ops.ml ([matmul] rank guard + clearer mixed-rank error), compiler/test/expect/pipeline.ml (contraction + mixed-rank expect tests), snapshots/code-manifest.sha256.

• Reason: Explicit errors and tests for invalid 2D contraction and rank-3×rank-2 matmul.

• Spec / docs linkage: phase-0/02-core-operations-and-typing.md.

• Follow-up actions: optional numpy-style broadcast matmul (out of scope for current structural checker).

• Date: 2026-05-09

• Scope: compiler/lib/elab/shape_ops.ml (rank-2 [matmul] shapes), compiler/lib/mlir/emitter.ml (linalg.matmul vs batch_matmul), compiler/examples/matmul_2d.kina, snapshots/mlir-golden/matmul_2d.mlir, Justfile, scripts/mlir-golden-*.sh, compiler/README.md, compiler/test/expect/pipeline.ml, compiler/examples.mld, snapshots/code-manifest.sha256.

• Reason: Support 2D matrix multiply in type checker and MLIR; extend expect tests for literals and new example.

• Spec / docs linkage: phase-0/02-core-operations-and-typing.md.

• Follow-up actions: invalid rank mixes (2×3 matmul) as explicit error tests if desired.

• Date: 2026-05-09

• Scope: compiler/test/expect/pipeline.ml, compiler/examples.mld.

• Reason: Grow ppx_expect pipeline tests to cover Section 2 example programs (mul through reshape) plus matmul dtype mismatch.

• Spec / docs linkage: snapshots/mlir-golden/*.mlir, compiler/examples/*.kina.

• Follow-up actions: add neg/exp unary or parse-failure cases if desired.

• Date: 2026-05-09

• Scope: compiler/test/expect/ (ppx_expect inline tests), compiler/dune-project (ppx_expect :with-test), compiler/examples.mld, compiler/README.md, docs/00-foundation/00-CODEBASE.md, snapshots/code-manifest.sha256.

• Reason: Executable “doctest-style” checks for the same S-expressions as the odoc examples page; dune runtest enforces drift.

• Spec / docs linkage: compiler/examples.mld § ppx_expect; compiler/README.md.

• Follow-up actions: optional mdx for markdown; expand pipeline.ml with more ops.

• Date: 2026-05-09

• Scope: compiler/examples.mld, compiler/index.mld; compiler/README.md, docs/00-foundation/00-CODEBASE.md.

• Reason: Add odoc “Worked examples” page with real surface syntax and in-process API snippets; link from package index.

• Spec / docs linkage: compiler/examples/*.kina, snapshots/mlir-golden/.

• Follow-up actions: optional mdx to execute snippets in CI; small doc/ executable that asserts snippet output.

• Date: 2026-05-09

• Scope: compiler/dune-project (package kina_compiler), compiler/dune, compiler/index.mld, compiler/lib/dune (public_name), compiler/bin/dune (public_name kina-compile, package), compiler/test/dune, scripts/compiler-doc.sh, Justfile (doc-compiler), compiler/README.md, docs/00-foundation/00-CODEBASE.md; module docstrings across compiler/lib/**/*.ml.

• Reason: In-repo API docs via Dune’s dune build @doc / odoc (Rustdoc-like HTML from sources), plus a small script and just entry point.

• Spec / docs linkage: docs/00-foundation/00-CODEBASE.md (OCaml doc tooling section).

• Follow-up actions: optional mdx/expect for literate OCaml; publish _doc to static hosting in CI when enabled.

• Date: 2026-05-09

• Scope: compiler/lib/mlir/emitter.ml — real linalg/tensor/arith lowering for Section 2 ops; compiler/lib/parser/sexpr_parser.ml — fix reduce_keep slice prefix so the reduction op name is parsed correctly; refreshed snapshots/mlir-golden/*.mlir and snapshots/code-manifest.sha256.

• Reason: Replace the typed-zero stub with executable-shaped IR aligned to Phase 0 “through linalg” wording; correct mean/sum parsing for reduce_keep.

• Spec / docs linkage: phase-0/02-core-operations-and-typing.md, phase-1/02-compiler-implementation.md (linalg-on-tensors).

• Follow-up actions: extend unary/cast coverage; add linalg.matmul for rank-2 matmul; run mlir-opt in CI when available; validate emitted modules with upstream MLIR.

• Date: 2026-05-09

• Scope: Phase 0 Section 2 core ops in compiler (unary, cast, sub/div, matmul, transpose, reduce/reduce_keep, broadcast, slice, concat) plus examples and MLIR goldens.

• Reason: Align the executable stub with the Section 2 operation set ahead of real MLIR lowering and Z3 discharge.

• Spec / docs linkage: phase-0/02-core-operations-and-typing.md; SMT premises (Γ ⊨ φ) are still structural only (no Z3).

• Follow-up actions: add linalg emission for typed ops; wire Z3 for matmul/broadcast/slice obligations; extend compiler_tests.ml beyond Kina_core round-trip.

• Date: 2026-05-09

• Scope: Bootstrap snapshots/code-manifest.sha256 and snapshots/mlir-golden/*.mlir with just snapshot-code / just snapshot-mlir-golden.

• Reason: Establish baselines so compiler and runtime drift are visible in review and CI.

• Spec / docs linkage: Compiler behavior should remain aligned with phase-0/; update decisions/spec-change-log.md when docs and code diverge by design.

• Follow-up actions: Run just check-code-snapshot before merge when touching compiler, examples, runtime, or verification sources.