feat(v2): elevate KitchenSpeak to a physically-grounded DSL + reference toolchain

[hyperpolymath]

What & why

Elevates KitchenSpeak from a v1.0 teaching DSL into a production orchestration
language whose superpower is physics in the types: materials carry
thermal/mechanical/chemical safety envelopes, appliances carry capability
envelopes, and an action type-checks only inside their intersection — so a
program that could curdle the milk, scorch the egg, bake the silicone spatula,
or over-torque the robot arm fails to compile, never reaching the hardware. The
same types lower to machine-checked Agda proofs and to a HAL over Matter / MQTT
/ ROS 2.

Heals the two-copy split first

Re-homes the design substance lost in the original excavation from the
nextgen-languages monorepo: proofs/agda/{Dough,PoachedEgg,EchoBridge},
proofs/Makefile, ADRs 0002–0004, ROADMAP.adoc. Corrects STATE.a2ml (was
still project "rsr-template-repo") and the root allowlist.

What's included

• Design blueprint (docs/): design/0001-v2-constitution.adoc (binding
  contract) + spec/{lexical,concrete-grammar,type-system} (close grammar.ebnf
  O1/O2/O3) + design/{semantics,hal-and-hardware,stdlib-ontology,blueprint-index}.
• Reference compiler (src/compiler/, dependency-free OCaml ~1240 LOC):
  lexer → parser → typed AST → physical-safety checker → HAL lowering.
  ksc check | lower (matter|mqtt|ros2) | parse.
• Corpus (examples/v2/ + tests/run-corpus.sh): 15/15 — 5 accept,
  10 reject-with-expected-code (CURDLE, MELT_TOOL, OVER_TORQUE, OVER_REACH,
  DOUBLE_USE, UNWITNESSED_SYNC, DIM_MISMATCH, NO_CAPABILITY, MISSING_ONFAIL).
• Proof (proofs/agda/NoCurdle.agda): v2 flagship, machine-checked
  (exit 0, 0 unsolved goals) — milk never reaches its curdle envelope; phase
  never becomes CURDLED. Wired into proofs/Makefile.

Verified

• cd src/compiler && dune build — clean.
• bash tests/run-corpus.sh — 15/15.
• make -C proofs nocurdle (+ Dough/PoachedEgg) — machine-check, exit 0.

Deferred (tracked in ROADMAP.adoc)

• Choreographic deadlock-freedom + ceremony-commutation are specified but not
  yet enforced by the checker.
• Emulsion/Sear proofs; QTT-Agda linearity port; Lean 4 port.
• Real HAL adapters (the prototype emits trace JSON only).
• The blueprint's adversarial completeness pass was cut short by a spend cap;
  the 4 workflow-generated docs are drafts pending that review.

🤖 Generated with Claude Code