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-09-05

• Scope (paths / examples): docs/10-spec/12-phase-1/27-storylm0-trained-fixture.md, tests/compiler/fixtures/storylm0/trained_checkpoint.npz, tests/compiler/fixtures/storylm0/trained_manifest.json, scripts/export_trained_checkpoint.py, scripts/validate_trained_rollout.py

• Reason for change: StoryLM-0 trained 32-token fixture. Persist Section 24 SGD weights as storylm0-checkpoint-v1 and lock a taught 32-token rollout. No new .kina program. No new compiler operator.

• Spec / docs linkage: docs/10-spec/12-phase-1/27-storylm0-trained-fixture.md, docs/30-decisions/56-storylm0-trained-fixture.md.

• Follow-up actions: AdamW-trained fixture optional; top-k / top-p; reduce_mean VJP.

• Date: 2026-08-24

• Scope (paths / examples): docs/10-spec/12-phase-1/26-storylm0-mean-nll.md, tests/compiler/examples/ad_reduce_sum.kina, tests/compiler/examples/storylm0_mean_nll_step.kina, tests/compiler/examples/invalid_reduce_mean_ad.kina, scripts/validate_mean_nll.py

• Reason for change: StoryLM-0 mean NLL. Keepdims reduce_sum VJP plus host 1/(B·T). No new compiler operator. No reduce_mean VJP.

• Spec / docs linkage: docs/10-spec/12-phase-1/26-storylm0-mean-nll.md, docs/30-decisions/55-storylm0-mean-nll.md.

• Follow-up actions: reduce_mean VJP, trained 32-token fixture.

• Date: 2026-08-24

• Scope (paths / examples): docs/10-spec/12-phase-1/25-storylm0-decoder-adamw.md, tests/compiler/examples/storylm0_adamw_step.kina, tests/compiler/fixtures/storylm0/adamw.json, scripts/validate_decoder_adamw.py

• Reason for change: StoryLM-0 decoder-wide AdamW. Section 15 reverseMode plus one Section 16 copy per trainable weight. Host loop over the Section 24 corpus. No new compiler operator.

• Spec / docs linkage: docs/10-spec/12-phase-1/25-storylm0-decoder-adamw.md, docs/30-decisions/54-storylm0-decoder-adamw.md.

• Follow-up actions: Mean NLL, trained 32-token fixture.

• Date: 2026-08-24

• Scope (paths / examples): docs/10-spec/12-phase-1/24-storylm0-host-train.md, tests/compiler/fixtures/storylm0/corpus.json, scripts/validate_train.py

• Reason for change: StoryLM-0 host train loop. 40 epochs of existing NLL ∘ SGD over a three-window toy corpus, then Section 23 greedy. No new .kina program. No new compiler operator.

• Spec / docs linkage: docs/10-spec/12-phase-1/24-storylm0-host-train.md, docs/30-decisions/53-storylm0-host-train.md.

• Follow-up actions: Mean NLL, decoder-wide AdamW, trained 32-token fixture.

• Date: 2026-08-24

• Scope (paths / examples): docs/10-spec/12-phase-1/23-storylm0-rollout.md, tests/compiler/examples/storylm0_rollout.kina, tests/compiler/fixtures/storylm0/, scripts/validate_rollout.py

• Reason for change: StoryLM-0 32-token checkpoint rollout. Host loop around a static T=36 forward plus argmax / Gumbel-max. Loads a versioned NPZ fixture. No compiler operator change. No in-place write.

• Spec / docs linkage: docs/10-spec/12-phase-1/23-storylm0-rollout.md, docs/30-decisions/52-storylm0-rollout.md.

• Follow-up actions: Prefill-T family, in-place write if ever specified, trained fixture.

• Date: 2026-08-24

• Scope (paths / examples): docs/10-spec/14-phase-3/07-storylm0-proj-shards.md, tests/compiler/examples/storylm0_tp_proj.kina, scripts/validate_tp_proj.py

• Reason for change: StoryLM-0 QKV projection shards. Slice Wq/Wk/Wv on the H·Dh axis, project each head, attend with H=1, concat the context. No compiler operator change. No @mesh.

• Spec / docs linkage: docs/10-spec/14-phase-3/07-storylm0-proj-shards.md, docs/30-decisions/51-storylm0-proj-shards.md.

• Follow-up actions: Vocab+heads together, row-parallel Wo, mesh syntax.

• Date: 2026-08-24

• Scope (paths / examples): docs/10-spec/14-phase-3/06-storylm0-head-parallel.md, tests/compiler/examples/storylm0_tp_heads.kina, scripts/validate_tp_heads.py

• Reason for change: StoryLM-0 head-parallel attention. Slice Q/Kᵀ/V on the head axis, attend with H=1, concat the context. No compiler operator change. No @mesh.

• Spec / docs linkage: docs/10-spec/14-phase-3/06-storylm0-head-parallel.md, docs/30-decisions/50-storylm0-head-parallel.md.

• Follow-up actions: Projection-weight shards, vocab+heads together, mesh syntax.

• Date: 2026-08-24

• Scope (paths / examples): docs/10-spec/14-phase-3/05-storylm0-workload.md, tests/compiler/examples/storylm0_tp_vocab.kina, scripts/validate_tp_vocab.py

• Reason for change: StoryLM-0 vocab-parallel logits. Column-parallel lm_head as slice + matmul + concat. No compiler operator change. No @mesh.

• Spec / docs linkage: docs/10-spec/14-phase-3/05-storylm0-workload.md, docs/30-decisions/49-storylm0-sharding-workload.md.

• Follow-up actions: Mesh syntax, GSPMD, head-parallel attention, collective lowering.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/22-tmax-scratch.md, tests/compiler/examples/storylm0_tmax.kina, scripts/validate_tmax.py

• Reason for change: StoryLM-0 T_max padded scratch. Live cache padded to a static T_max with zeros, then sliced back. No compiler operator change. No in-place write.

• Spec / docs linkage: docs/10-spec/12-phase-1/22-tmax-scratch.md, docs/30-decisions/48-storylm0-tmax-scratch.md.

• Follow-up actions: Prefill-T family, sampled rollout, in-place write if ever specified.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/21-prefill-handoff.md, tests/compiler/examples/storylm0_prefill.kina, scripts/validate_prefill.py

• Reason for change: StoryLM-0 prefill → decode handoff. Forward graph returns Kᵀ/V; host slices last logits and calls one static-S decode. The .so pipeline now runs --lower-affine so host extract_slice converts.

• Spec / docs linkage: docs/10-spec/12-phase-1/21-prefill-handoff.md, docs/30-decisions/47-storylm0-prefill-handoff.md.

• Follow-up actions: T_max scratch, prefill-T family, sampled rollout.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/20-host-generation-loop.md, tests/compiler/examples/storylm0_generate.kina, scripts/validate_generate.py

• Reason for change: StoryLM-0 host generation loop. Static-S decode plus host argmax. No compiler operator change.

• Spec / docs linkage: docs/10-spec/12-phase-1/20-host-generation-loop.md, docs/30-decisions/46-storylm0-host-generation-loop.md.

• Follow-up actions: Prefill handoff, T_max scratch, sampled rollout.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/19-kv-cache.md, tests/compiler/examples/storylm0_kv_step.kina, scripts/validate_kv_cache.py

• Reason for change: StoryLM-0 functional KV-cache append. concat on the sequence axis plus one new-token attention. Host static concat now lowers to insert_slice so .so one-shot-bufferize can run. No new operator.

• Spec / docs linkage: docs/10-spec/12-phase-1/19-kv-cache.md, docs/30-decisions/45-storylm0-kv-cache.md.

• Follow-up actions: Host generation loop, prefill handoff, T_max scratch.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/18-seeded-sampling.md, tests/compiler/examples/storylm0_sample.kina, scripts/validate_sample.py

• Reason for change: StoryLM-0 seeded categorical sampling. Host Uniform(0, 1) + Gumbel-max + Section 17 argmax. Host padded broadcast now maps size-1 source dims to affine 0 so [1, 1] → [1, 4, 8] lowers.

• Spec / docs linkage: docs/10-spec/12-phase-1/18-seeded-sampling.md, docs/30-decisions/44-storylm0-seeded-sampling.md.

• Follow-up actions: Top-k / top-p, KV-cache, Phase 2 Random.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/17-argmax.md, src/compiler/lib/elab/type_formation.ml, src/compiler/lib/mlir/emitter_tensor_ops.ml, src/compiler/lib/mlir/emitter.ml, src/compiler/lib/elab/ad_pass.ml, tests/compiler/examples/argmax_axis1.kina, tests/compiler/examples/argmax_keep_axis1.kina, tests/compiler/examples/storylm0_greedy.kina, scripts/validate_argmax.py

• Reason for change: StoryLM-0 deterministic argmax. Host reduce argmax with I64 result and lowest-index tie-break. No new surface token. No VJP.

• Spec / docs linkage: docs/10-spec/12-phase-1/17-argmax.md, docs/30-decisions/43-storylm0-argmax.md.

• Follow-up actions: Seeded sampling, KV-cache, device argmax, argmin.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/16-functional-adamw.md, tests/compiler/examples/adamw_step.kina, scripts/validate_adamw.py

• Reason for change: StoryLM-0 functional AdamW. Moments, bias correction, and decoupled weight decay as existing ops. No compiler operator change.

• Spec / docs linkage: docs/10-spec/12-phase-1/16-functional-adamw.md, docs/30-decisions/42-storylm0-functional-adamw.md.

• Follow-up actions: Decoder-wide AdamW, argmax / sampling / KV-cache.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/15-nll-decoder-train.md, tests/compiler/examples/storylm0_nll_step.kina, scripts/validate_nll_decoder_train.py

• Reason for change: StoryLM-0 NLL ∘ decoder train step. Compose existing NLL and decoder VJPs; apply functional SGD to every trainable weight. No compiler operator change.

• Spec / docs linkage: docs/10-spec/12-phase-1/15-nll-decoder-train.md, docs/30-decisions/41-storylm0-nll-decoder-train.md.

• Follow-up actions: AdamW, mean NLL, argmax / sampling / KV-cache.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/14-decoder-ad.md, src/compiler/lib/ir/ir_typed.ml, src/compiler/lib/elab/ad_pass.ml, src/compiler/lib/mlir/emitter.ml, src/compiler/lib/mlir/pipeline.ml, tests/compiler/examples/ad_gather.kina, tests/compiler/examples/ad_reshape.kina, tests/compiler/examples/ad_matmul4.kina, tests/compiler/examples/storylm0_ad_step.kina, scripts/validate_decoder_ad.py, tests/snapshots/mlir-golden/ (matmul dest zero-init in inlined stdlib plus new ad_gather / ad_reshape / ad_matmul4 / storylm0_ad_step goldens)

• Reason for change: StoryLM-0 decoder AD. Restricted VJPs for reshape, variadic-batch matmul (rank ≥ 2), and 2D gather. Gather cotangent is IR-internal ScatterAdd. Discrete I64 parameters are omitted from the reverseMode tuple. Embedding SGD train step on the decoder graph. linalg.matmul / batch_matmul dests are zero-initialized (arith.constant dense<0>) because those ops accumulate; tensor.empty() dests produced garbage in the AD backward graph. Host .so links -lmlir_c_runner_utils for memrefCopy after tensor.reshape / collapse / expand. Isolated ad_reshape.so dest-passing still crashes; reshape VJP is checked inside storylm0_ad_step.

• Spec / docs linkage: docs/10-spec/12-phase-1/14-decoder-ad.md, docs/30-decisions/40-storylm0-decoder-ad.md.

• Follow-up actions: Isolated reshape .so dest-passing, device ScatterAdd, multi-weight SGD, NLL∘decoder, AdamW / sampling / KV-cache, rank-changing broadcast VJP.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/13-tuple-projection.md, src/compiler/lib/ast/ast_surface.ml, src/compiler/lib/ir/ir_typed.ml, src/compiler/lib/parser/kina_parser.mly, src/compiler/lib/elab/type_formation.ml, src/compiler/lib/mlir/emitter_control_flow.ml, tests/compiler/examples/ad_sgd_step.kina, scripts/validate_ad_sgd.py

• Reason for change: Tuple projection. Destructuring let (y, g) = handle f(w) with reverseMode so one program can apply Section 11 SGD to Section 12 grads.

• Spec / docs linkage: docs/10-spec/12-phase-1/13-tuple-projection.md, docs/30-decisions/39-tuple-projection.md.

• Follow-up actions: AdamW, sampling/KV-cache, AD through projection.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/12-reversemode-result-abi.md, src/compiler/lib/elab/type_formation.ml, src/compiler/lib/elab/ad_pass.ml, src/compiler/lib/mlir/emitter.ml, tests/compiler/examples/ad_neg_grad.kina, scripts/validate_reverse_mode_abi.py

• Reason for change: reverseMode result ABI. Flat (primal, g…) type; MLIR multi-result @main / fn; Kina-executed .so grads for neg.

• Spec / docs linkage: docs/10-spec/12-phase-1/12-reversemode-result-abi.md, docs/30-decisions/38-reversemode-result-abi.md.

• Follow-up actions: Tuple projection (loss → VJP → SGD in one program), AdamW, sampling/KV-cache.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/11-functional-sgd.md, tests/compiler/examples/sgd_step.kina, tests/compiler/examples/invalid_sgd_shape.kina, scripts/validate_sgd.py

• Reason for change: StoryLM-0 functional SGD. w' = w - lr.broadcast(σ) * g as existing ops. No new primitive. Numeric .so check.

• Spec / docs linkage: docs/10-spec/12-phase-1/11-functional-sgd.md, docs/30-decisions/37-storylm0-functional-sgd.md.

• Follow-up actions: reverseMode result ABI, AdamW, sampling/KV-cache.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/10-log-softmax-and-take-along-axis-ad.md, src/compiler/lib/ir/ir_typed.ml, src/compiler/lib/elab/ad_pass.ml, src/compiler/lib/mlir/emitter.ml, tests/compiler/examples/ad_neg.kina, tests/compiler/examples/ad_log_softmax.kina, tests/compiler/examples/ad_nll.kina, scripts/validate_loss_ad.py

• Reason for change: StoryLM-0 loss AD. Restricted reverse-mode VJPs for neg, log_softmax, and take_along_axis. Scatter is IR-internal. No @main tuple-return ABI.

• Spec / docs linkage: docs/10-spec/12-phase-1/10-log-softmax-and-take-along-axis-ad.md, docs/30-decisions/36-storylm0-loss-ad.md.

• Follow-up actions: Device take_along_axis, reverseMode result ABI / Kina-executed grads, SGD/sampling/KV-cache.

• Date: 2026-08-23

• Scope (paths / examples): docs/10-spec/12-phase-1/09-log-softmax-and-take-along-axis.md, src/compiler/, tests/compiler/examples/log_softmax_*.kina, tests/compiler/examples/take_along_axis_*.kina, tests/compiler/examples/storylm0_nll.kina, tests/compiler/examples/invalid_log_softmax_*.kina, tests/compiler/examples/invalid_take_along_axis_*.kina

• Reason for change: StoryLM-0 loss ops. Host log_softmax and take_along_axis with typing, MLIR lowering, negative tests, and goldens. NLL is composed, not a primitive. No AD VJP.

• Spec / docs linkage: docs/10-spec/12-phase-1/09-log-softmax-and-take-along-axis.md, docs/30-decisions/35-storylm0-loss-ops.md.

• Follow-up actions: AD parity, device take_along_axis, SGD/sampling/KV-cache.

• Date: 2026-08-23

• Scope (paths / examples): website/app/styles/site.css, website/app/examples/page.tsx.

• Reason for change: Examples masonry actually packs. @supports (grid-template-rows: masonry) and display: masonry were matching in Chromium and then being ignored, which left a regular equal-track grid. Use CSS columns as the layout, display: grid-lanes only where that value exists, and vary card height with a source preview.

• Spec / docs linkage: docs/70-site/70-public-site.md.

• Follow-up actions: none for the compiler; visual only.

• Date: 2026-08-23

• Scope (paths / examples): website/app/styles/site.css, website/app/examples/page.tsx, website/app/page.tsx.

• Reason for change: Examples masonry. Long unspaced filenames overflowed equal-height tiles and overlapped on hover translate. Native masonry with a column fallback; tiles size to their copy.

• Spec / docs linkage: docs/70-site/70-public-site.md.

• Follow-up actions: none for the compiler; visual only.

• Date: 2026-08-23

• Scope (paths / examples): website/app/styles/site.css, website/app/ui/*, website/app/*.tsx, docs/70-site/70-public-site.md.

• Reason for change: Replace the site sheet and chrome. The previous layered stylesheet lost to the unlayered Tailwind reset, so headings, lists, and links looked unstyled. New unlayered site.css, new masthead / page-mast components, and a complete prose set.

• Spec / docs linkage: docs/70-site/70-public-site.md.

• Follow-up actions: none for the compiler; visual only.

• Date: 2026-08-23

• Scope (paths / examples): website/app/globals.css, website/app/*.tsx, website/lib/markdown.ts, docs/70-site/70-public-site.md.

• Reason for change: Site type and flow audit. Container-query type ramp, staggered mono/display/sans roles, region headers on every page, drop Daisy layout skins (navbar / footer / card) and leftover layout class names.

• Spec / docs linkage: docs/70-site/70-public-site.md.

• Follow-up actions: none for the compiler; visual only.

• Date: 2026-08-23

• Scope (paths / examples): website/app/globals.css, website/uno.config.ts, website/postcss.config.mjs, website/app/*, root Uno/PostCSS re-exports, docs/70-site/70-public-site.md.

• Reason for change: Site theme revamp. Light-first Stratos-style token cascade (OKLCH / OKLAB / P3 / Rec.2020) with DaisyUI + UnoCSS. Replace unreadable dark-mode gold with Pelorous (hue 205).

• Spec / docs linkage: docs/70-site/70-public-site.md.

• Follow-up actions: none for the compiler; visual only.

• Date: 2026-08-23

• Scope (paths / examples): root package.json, next.config.mjs, vercel.json, app → website/app, lib → website/lib.

• Reason for change: Fix Vercel preview with rootDirectory: null. The GitHub Vercel project builds from the repo root. Add a root Next.js entry that reuses the website/ app.

• Spec / docs linkage: website/DEPLOY.md.

• Follow-up actions: set the production project's Root Directory to website in the Vercel dashboard when possible.

• Date: 2026-08-23

• Scope (paths / examples): website/content/, website/.gitignore, website/scripts/collect-content.mjs, website/DEPLOY.md.

• Reason for change: Fix Vercel build. Root Directory website/ cannot read ../docs. Commit the collected corpus and fall back to that snapshot when the parent tree is invisible.

• Spec / docs linkage: docs/70-site/70-public-site.md.

• Follow-up actions: refresh website/content when docs or examples change (node website/scripts/collect-content.mjs).

• Date: 2026-08-23

• Scope (paths / examples): docs/00-foundation/03-current-status.md, docs/00-foundation/00-CODEBASE.md, docs/00-foundation/01-surface-kina.md, docs/00-foundation/02-surface-kina.md, docs/30-decisions/32-phase-0-reference-implementation-status.md, website/, README.md, src/compiler/README.md, src/runtime/README.md, tests/compiler/examples/README.md.

• Reason for change: Close the public-site / docs honesty gap. The live site and several READMEs described a finished .kina language and a StoryLM-0 vertical slice; the compiler is a bootstrap that emits MLIR, and StoryLM-0 is a compile-and-check forward graph. Publish /status, correct module names, and stop calling the S-expression core “the user-facing surface.”

• Spec / docs linkage: non-normative status page; Phase 0/1 specs unchanged as contracts.

• Follow-up actions: StoryLM-0 compiler slice (log_softmax / NLL) remains implementation work, not this docs pass.

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