ADR: Toolchain pins (LLVM, Z3, Lean)

Context

Phase 0 Section 5 §11 requires pinning compiler, SMT, and proof-assistant stacks so CI and local builds are reproducible. Textual MLIR, ocaml-z3, and mathlib4 all move on independent schedules; unpinned versions break tutorials and bisection.

Decision

1. LLVM / MLIR: Baseline LLVM 18 (already cited in Section 5 §12). Upgrade on a deliberate cycle (suggest: review annually); document pass names and textual dialect changes in upgrade notes.

2. Z3 / ocaml-z3: Pin a known-good pair of Z3 and ocaml-z3 versions in the compiler’s dependency manifest (e.g. opam / dune lock). Verify the pair on CI. If upstream skew breaks the build, vendor a tested binding revision rather than floating on latest.

3. Lean 4 / mathlib4: Pin lean-toolchain and a specific mathlib4 commit (not master). Schedule maintenance bumps (e.g. every 1–2 months) as explicit tasks, not ad-hoc upgrades.

Exact version numbers and commit hashes are filled in when compiler/, verification/, and CI exist; this ADR records the policy.

Consequences

• Reproducible builds and teachable setup (scripts/setup.sh, docs).
• Occasional maintenance cost to bump pins and fix breakage.
• Trade-off accepted vs chasing latest features unsafely.