Architecture decision records (ADRs)

This directory holds ADRs at the repository root, alongside the specification tree (phase-0/, phase-1/, …). That layout is committed in Phase 0 Section 5 (Implementation Infrastructure); see phase-0/05-implementation-infrastructure.md (repo layout and the decisions/ bullet in the notes).

Conventions

• One ADR per major, durable commitment (not every PR).
• Use the usual structure: Context, Decision, Consequences.
• Filenames: short kebab-case.md (for example bootstrap-stance.md, abi-stability.md).

Recorded decisions

• toolchain-pins.md — LLVM/MLIR, Z3/ocaml-z3, Lean/mathlib pinning policy (Phase 0 §05 §11).
• phase-0-reference-implementation-status.md — what the OCaml compiler implements today vs Phase 0 §02 (structural shapes, partial op/cast/reduce lowering); companion to phase-0/REVIEW-CHECKLIST.md §4.
• 35-storylm0-loss-ops.md — log_softmax and take_along_axis for StoryLM-0 NLL; not an AD or Phase 1 exit decision.
• 36-storylm0-loss-ad.md — restricted compiler VJPs for those ops; IR-internal scatter; not Phase 2 handler AD.
• 37-storylm0-functional-sgd.md — SGD as existing arithmetic; not a primitive and not AdamW.
• 38-reversemode-result-abi.md — Flat (primal, g…) reverseMode type; MLIR multi-result ABI; no tuple projection.
• 39-tuple-projection.md — Destructuring let to name reverseMode results; not AD-through-projection.
• 40-storylm0-decoder-ad.md — Restricted reshape / rank-4 matmul / 2D gather VJPs; IR-internal ScatterAdd; discrete parameters omitted from the result tuple.
• 41-storylm0-nll-decoder-train.md — NLL ∘ decoder and multi-weight SGD as composition; sum-NLL seed ones; no new operator.
• 42-storylm0-functional-adamw.md — AdamW as existing arithmetic (PyTorch algebra); host scalars; no new operator.
• 43-storylm0-argmax.md — Host argmax reduce; I64 result; lowest-index tie-break; no VJP.
• 44-storylm0-seeded-sampling.md — Categorical sample as host Uniform + Gumbel-max; no RNG primitive.
• 45-storylm0-kv-cache.md — One-step KV append as concat; host holds the cache; no while growth.
• 46-storylm0-host-generation-loop.md — Host greedy loop around static-S decode; no while growth.
• 47-storylm0-prefill-handoff.md — Prefill returns the cache; host slices last logits; one static-S decode.
• 48-storylm0-tmax-scratch.md — T_max as pad-with-zeros + slice-prefix; not an in-place write.
• 49-storylm0-sharding-workload.md — StoryLM-0 as the first Phase 3 workload; 2-way vocab-parallel lm_head; no @mesh.
• 50-storylm0-head-parallel.md — 2-way head-parallel attention as slice + rank-4 matmul + concat; no @mesh.
• 51-storylm0-proj-shards.md — 2-way column-parallel QKV as slice + rank-3 matmul + per-head attention + concat; no @mesh.
• 52-storylm0-rollout.md — 32-token host rollout around a static T=36 forward plus a versioned NPZ fixture; no new operator.
• 53-storylm0-host-train.md — Host loop of Section 15 SGD over a toy corpus, then Section 23 greedy; no new operator.
• 54-storylm0-decoder-adamw.md — Section 16 AdamW on every trainable decoder weight after Section 15 reverseMode; no new operator.
• 55-storylm0-mean-nll.md — Mean NLL as keepdims reduce_sum times host 1/(B·T); no reduce_mean VJP.
• 56-storylm0-trained-fixture.md — Persist Section 24 SGD weights as storylm0-checkpoint-v1; lock 32-token taught rollout.

Planned / cited elsewhere

Forward tracks and Phase 1 name additional ADRs as they appear. Examples: bootstrap stance, ABI stability policy, Arrow as canonical tabular format.