hyperpolymath · hyperpolymath · Jun 15, 2026 · Jun 15, 2026 · Jun 15, 2026
@@ -1,27 +1,41 @@
 ;; SPDX-License-Identifier: MPL-2.0
-;; Project state — update throughout each session
+;; Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+;; Project state — update throughout each session.
 (state
   (metadata
-    (version "1.0.1")
-    (project "rsr-template-repo")
-    (last-updated "2026-04-04"))
+    (version "2.0.0-dev")
+    (project "kitchenspeak")
+    (last-updated "2026-06-15"))
   (project-context
-    (description "RSR Standard Repository Template — baseline for all hyperpolymath projects")
-    (primary-language "Idris2 (ABI) + Zig (FFI)")
-    (status "testing-complete"))
+    (description
+      "KitchenSpeak — a formally-verified, hardware-agnostic orchestration DSL \
+for the domestic kitchen and consumer robotics. The v2.0 line elevates the \
+seven teaching types into a physically-grounded substructural type system: \
+materials carry thermal/mechanical/chemical envelopes and appliances carry \
+capability envelopes, so physical-safety violations (curdle, scorch, \
+over-torque, melt-the-tool) are compile errors, not firmware run-time faults.")
+    (primary-language "OCaml (front end + checker) + Agda/Lean (proofs) + Idris2/Zig (ABI/FFI)")
+    (status "v1.0 spec stable; v2.0 design + reference prototype in progress"))
   (current-position
-    (phase "testing")
-    (completion-percentage 100)
-    (milestone "CRG C - Testing & Benchmarking complete"))
-  (testing-summary
-    (validation-script "scripts/validate-template.sh: PASS (0 errors)")
-    (workflow-tests "tests/workflows/validate_workflows_test.sh: PASS (21/21 workflows)")
-    (integration-tests "test/integration_test.zig: PASS (placeholder template)")
-    (e2e-tests "tests/e2e/template_instantiation_test.sh: READY")
-    (benchmarks "benches/template_bench.sh: PASS (5 suites)")
-    (zig-build "Zig 0.15.2 compatible: PASS"))
+    (phase "v2.0 elevation: blueprint + reference prototype LANDED; PR #1 open")
+    (completion-percentage 60)
+    (milestone "Blueprint docs, OCaml reference checker (corpus 15/15), and the \
+machine-checked NoCurdle proof are committed (signed), pushed, and open as PR #1. \
+Remaining work is depth: session-typing/effects in the checker, more proofs, \
+real HAL adapters."))
+  (heritage
+    (note "This repo was instantiated from rsr-template-repo and previously \
+retained the template's STATE identity. Corrected 2026-06-15 to its true \
+identity. The design substance (proofs, ROADMAP, ADRs 0002-0004) was \
+re-homed from the nextgen-languages monorepo copy in the same session."))
+  (done-2026-06-15
+    ("docs/spec + docs/design blueprint landed (constitution, grammar, type system, semantics, HAL, ontology, index)."
+     "src/compiler/ OCaml checker built; corpus tests/run-corpus.sh 15/15 (5 accept, 10 reject-with-expected-code)."
+     "proofs/agda/NoCurdle.agda machine-checked (exit 0) + wired into proofs/Makefile."
+     "Committed (signed id_ed25519_signing), pushed, PR #1 open, GitHub Verified."))
   (critical-next-actions
-    ("Commit test suite"
-     "Push to GitHub"
-     "Verify CI workflows pass"
-     "Document test instantiation patterns")))
+    ("Implement choreographic deadlock-freedom + ceremony-commutation in src/compiler/check.ml (specified, not yet enforced)."
+     "Add Emulsion + Sear proofs (ROADMAP Phase 1c); then QTT-Agda linearity port; then Lean 4 port."
+     "Wire real HAL adapters (Matter/MQTT/ROS2) behind the trace IR the prototype already emits."
+     "Finish the adversarial completeness pass over the 6 blueprint docs (4 are workflow drafts; critic cut by spend cap)."
+     "Retire or repoint the old nextgen-languages/kitchenspeak copy now the standalone is canonical and ahead.")))
@@ -51,6 +51,16 @@ scripts/
 verification/
 container/                 # may host Containerfile if not at build/
 
+# ─── Language artefacts (this repo IS a language, not a bare template) ────────
+# KitchenSpeak's authoritative spec family lives at root by convention, mirroring
+# the nextgen-languages monorepo copy these were re-homed from (2026-06-15).
+SPEC.adoc                  # class v1.0 specification (authoritative requirements)
+COMMENTARY.adoc            # type-theoretic companion to SPEC.adoc
+grammar.ebnf               # class grammar (Section A) + marked patches (Section B)
+ROADMAP.adoc               # proofs-first plan to full-toolchain parity
+decisions/                 # Architecture Decision Records (ADRs 0001-0004)
+proofs/                    # Agda (now) / Lean (later) lowerings of the recipes
+
 # ─── Tolerated pending follow-up (re-evaluate when item lands) ───────────────
 .gitlab-ci.yml             # TODO: relocate to ci/.gitlab-ci.yml after GitLab project-setting update
 .pre-commit-config.yaml    # TODO: relocate to ci/.pre-commit-config.yaml after invocation pattern decided

@@ -9,3 +9,29 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 <!-- Run: just changelog -->
 
 ## [Unreleased]
+
+### Added — v2.0 elevation (2026-06-15)
+
+- **Physically-grounded type system design.** `docs/design/0001-v2-constitution.adoc`
+  (binding contract) plus the blueprint: `docs/spec/` (lexical grammar, concrete
+  grammar v2, normative type system) and `docs/design/` (semantics & safety
+  calculus, HAL & hardware, standard ontology, blueprint index). Materials carry
+  thermal/mechanical/chemical envelopes and appliances carry capability envelopes
+  so physical-safety violations are compile errors.
+- **Reference compiler** `src/compiler/` (`ksc`, dependency-free OCaml): lexer →
+  parser → typed AST → physical-safety checker → HAL lowering (Matter / MQTT /
+  ROS 2). `ksc check | lower | parse`.
+- **Example corpus** `examples/v2/` (5 well-typed recipes) + `examples/v2/negative/`
+  (9 must-reject recipes) and `tests/run-corpus.sh` (14/14 green).
+- **`proofs/agda/NoCurdle.agda`** — v2.0 flagship: machine-checked proof that a
+  bounded controller keeps milk below its curdle envelope and the milk phase never
+  becomes CURDLED. Wired into `proofs/Makefile`.
+
+### Fixed
+
+- **Re-homed the design substance** lost in the original excavation from the
+  nextgen-languages monorepo: `proofs/agda/{Dough,PoachedEgg,EchoBridge}`,
+  `proofs/Makefile`, ADRs 0002–0004, and `ROADMAP.adoc`.
+- Corrected `.machine_readable/STATE.a2ml` identity (was still
+  `project "rsr-template-repo"`) and added the language artefacts to
+  `.machine_readable/root-allow.txt`.
@@ -10,10 +10,43 @@ machine-executable actions for MQTT/Matter-class appliances, while
 maintaining physical and digital safety through a multi-layered type
 system.
 
-*Status:* CLASS PROJECT. Specification stable at v1.0; grammar and worked
-examples are in active development. Not intended for deployment on actual
-kitchen hardware. Experimental companion to the other languages in this
-repository.
+*Status:* v1.0 specification stable (the original class teaching artefact).
+*v2.0 elevation in progress* — a physically-grounded type system, a reference
+compiler, and a machine-checked material-safety proof. Not intended for
+deployment on actual kitchen hardware yet.
+
+== KitchenSpeak v2.0 — the production elevation
+
+v2.0 turns typing into the *superpower*: physical safety lives in the type
+system, so a program that could *curdle the milk*, *scorch the egg*, *bake the
+silicone spatula*, or *over-torque the robot arm* **fails to compile**. Materials
+carry thermal/mechanical/chemical safety envelopes; appliances carry capability
+envelopes; an action type-checks only inside the intersection of the two. The same
+types lower to machine-checked Agda proofs *and* to a HAL over Matter / MQTT /
+ROS 2.
+
+Start at `docs/design/0000-blueprint-index.adoc` (the document map and the
+"golden thread" tracing no-curdle from syntax → type rule → proof → HAL).
+
+[source,bash]
+----
+# Build and run the reference compiler (dependency-free OCaml; needs dune).
+cd src/compiler && dune build
+KSC=_build/default/main.exe
+
+$KSC check ../../examples/v2/poached-egg.ks          # => OK
+$KSC check ../../examples/v2/negative/curdle-milk.ks # => error [CURDLE] ... (exit 1)
+$KSC lower --target matter ../../examples/v2/poached-egg.ks   # => Matter trace JSON
+
+# Run the full accept/reject corpus (14 cases):
+bash tests/run-corpus.sh
+
+# Machine-check the v2.0 flagship safety proof:
+make -C proofs nocurdle    # (or: agda proofs/agda/NoCurdle.agda)
+----
+
+Not intended for deployment on actual kitchen hardware. Experimental companion to
+the other languages in this repository.
 
 == Origin
 

@@ -0,0 +1,227 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= KitchenSpeak Roadmap — From Specification to AffineScript Parity
+:toc:
+:toclevels: 3
+:icons: font
+
+== Purpose
+
+KitchenSpeak has been elevated from an in-tree directory of the
+`nextgen-languages` monorepo to a standalone canonical repository, on a
+par with its sibling languages (`affinescript`, `ephapax`, `betlang`, …).
+This roadmap defines the path that takes KitchenSpeak from its current
+position — *a stable v1.0 specification plus a single hand-verified Agda
+proof* — to the position **AffineScript** currently occupies: a full
+language toolchain with an in-progress ABI and `RSR FULL` repository
+hygiene.
+
+The ordering principle is **proofs first**. KitchenSpeak's defining
+invariant (SPEC.adoc §6, "Agda-Proven") is that the core recipe library
+type-checks with zero unsolved goals. Unlike a conventional language,
+where proofs trail the compiler, KitchenSpeak's proofs *are* the
+specification's acceptance test and must lead. This also happens to be
+precisely where AffineScript is weakest — its own foundations grade is
+`FRG-E` with no `formal/` directory and an open type-soundness
+obligation (see the monorepo's `PROOF-NEEDS.md`) — so leading with
+proofs both honours KitchenSpeak's identity and lets it overtake its
+target on the one axis that matters most for a safety DSL.
+
+== Where AffineScript is (the target position)
+
+Recorded from the monorepo's own authoritative documents
+(`EXPLAINME.adoc` §Claim 1, `TOOLING-STATUS.adoc`, `PROOF-NEEDS.md`),
+since the standalone `hyperpolymath/affinescript` repo sits outside this
+work's scope:
+
+[cols="1,3"]
+|===
+| Axis | AffineScript's position
+
+| Front end
+| OCaml compiler (lexer → parser → checker). Tree-sitter grammar.
+
+| Toolchain
+| `affine-lsp` (Rust), `affine-dap` (Rust), `linter.ml`, formatter
+  (stub), `affine-doc`, `affine-pkg`. Conformance suite ✓.
+
+| ABI / FFI
+| `src/abi/` Idris2 (`Types`, `Layout`, `Foreign`); Zig FFI planned.
+  Status: *in progress*.
+
+| Target
+| typed WebAssembly (WasmGC) via the shared `typed-wasm` aggregate.
+
+| Grades
+| `ARG-D`, `FRG-E`, `RSR FULL`. Registered in BoJ `lang-mcp` (id 2).
+
+| Formal verification
+| *Known gap.* Claims affine types but the OCaml type checker is
+  unproven and the Rust runtime (GC, allocator) is unverified
+  (`PROOF-NEEDS.md`). No `formal/` directory.
+|===
+
+== Where KitchenSpeak is (the starting position)
+
+[cols="1,3"]
+|===
+| Artefact | Status
+
+| `SPEC.adoc`
+| Class v1.0 specification, stable. Authoritative requirements artefact.
+
+| `grammar.ebnf`
+| Class grammar (Section A) + three marked additive patches (Section B).
+  Lexical sub-grammar still placeholder (open item O3).
+
+| `COMMENTARY.adoc`
+| Type-theoretic companion: each of the seven types mapped to standard
+  foundations; proof obligations named.
+
+| `examples/poached-egg.ks`
+| One worked example (Linear + Tropical + Echo + Ceremonial).
+
+| `decisions/0001-proof-assistant.adoc`
+| ADR: Agda chosen for v1.0, Lean 4 reserved as successor.
+
+| `proofs/agda/Dough.agda`
+| One proof (Linear + Dyadic + Choreographic + Echo). Hand-verified,
+  not yet machine-checked (no Agda in CI yet).
+
+| Toolchain
+| None. No lexer, parser, type checker, LSP, DAP, formatter, package
+  manager, doc generator, ABI, or conformance suite.
+
+| Grades
+| All `TBD` (`TOOLING-STATUS.adoc`). No `spec/{ARG,FRG,TRG}-PROFILE`.
+|===
+
+== Phased plan
+
+=== Phase 0 — Repository elevation & hygiene *(this PR)*
+
+* Standalone repo created with `README.adoc`, `LICENSE` (Palimpsest /
+  MPL-2.0), `.gitignore`, `CHANGELOG.adoc`, this `ROADMAP.adoc`.
+* `ADR 0002` records the elevation and this roadmap's rationale.
+* Wired back into `nextgen-languages` as a submodule, matching every
+  other language.
+* *Exit criteria:* repo builds its proofs locally (`make -C proofs`);
+  listed as a DSL in the monorepo `README.adoc` and `EXPLAINME.adoc`.
+
+=== Phase 1 — Proofs first *(the core deliverable)*
+
+The `proving @witness` clause and the `Agda-Proven` mission criterion
+mean the proof library is the language's acceptance test. This phase is
+deliberately ahead of any compiler work.
+
+* *1a. Machine-check the existing library.* Add Agda 2.6.4+ / stdlib
+  2.0+ to CI (`proofs/Makefile`, `kitchenspeak.agda-lib` landed in this
+  PR). Bring `Dough.agda` from *hand-verified* to *machine-checked*,
+  zero unsolved goals.
+* *1b. PoachedEgg.agda* — landed in this PR. Lowers
+  `examples/poached-egg.ks`; first proof to discharge a *Tropical*
+  refinement (no-binary-overheat envelope) alongside Linear + Echo.
+* *1c. Complete the SPEC §6 core library.* Add `Emulsion.agda`
+  (Tropical + Linear) and `Sear.agda` (Tropical + Echo + Primitive) so
+  the three canonically-named recipes — Dough, Emulsion, Sear — all
+  type-check.
+* *1d. Linearity.* Move from the by-inspection discipline (Dough/Poached
+  Egg §Linearity notes) to a machine-checked QTT-Agda port, resolving
+  ADR 0001 open question 1.
+* *1e. Foundations grade.* Author `spec/FRG-PROFILE.adoc`. Target
+  `FRG ≥ E` immediately (a real `proofs/` tree exists, which AffineScript
+  lacks), climbing toward `FRG-D` as the library closes.
+* *Exit criteria:* `make -C proofs` green in CI for the whole core
+  library; FRG profile authored.
+
+=== Phase 2 — Front end (lexer + parser)
+
+* Formal lexer specification, closing `grammar.ebnf` open item O3
+  (the placeholder lexical nonterminals).
+* Parser to a typed AST. Implementation language **OCaml**, matching
+  AffineScript and the monorepo's compiler-front-end convention.
+* Resolve the remaining grammar open items O1 (nested blocks) and O2
+  (`resource_decl` / `chef_decl` / `echo_decl` definitions).
+* *Exit criteria:* `examples/poached-egg.ks` and the Dough/Emulsion/Sear
+  programs parse to AST; round-trips through a pretty-printer.
+
+=== Phase 3 — Type checker (static semantics)
+
+Implement the seven types as a checker, cross-validated against the Agda
+proofs from Phase 1 (the proofs are the oracle for the checker's
+soundness):
+
+* Tropical — bounded-derivative refinement over dimensioned quantities.
+* Linear — single-use resource discipline (QTT-style).
+* Choreographic — session-typed multiparty barriers; deadlock-freedom.
+* Echo — postulated-oracle witnesses bound by `proving`.
+* Dyadic — tensor product for `<~>` binds.
+* Ceremonial — ambient reader-effect, proven to commute with linearity.
+* Primitive — SI units-of-measure.
+* Enforce the three production-mandatory constructs (`max_duration`,
+  `on_fail`, `proving`) as typing rules.
+* *Exit criteria:* checker rejects the negative test corpus (double-used
+  egg, missing `on_fail`, unwitnessed `sync`); `ARG ≥ D` plausible.
+
+=== Phase 4 — Lowering & Hardware Abstraction Layer
+
+* Lower well-typed programs to the device-command JSON of SPEC §5
+  (HomeConnect / SmartThings / Tuya); Matter + MQTT as a later HAL
+  revision.
+* Echo postulates become HAL sensor bindings; the proven/postulated
+  boundary becomes a runtime trust boundary.
+* *Exit criteria:* the Poached Egg lowers to a HAL trace for at least
+  one simulated target.
+
+=== Phase 5 — Toolchain parity with AffineScript
+
+Build out, one-for-one against AffineScript's `TOOLING-STATUS` row:
+
+* `ks-lsp` (LSP), `ks-dap` (DAP) — Rust, per convention.
+* Linter, formatter, tree-sitter grammar, doc generator, package
+  manager.
+* Conformance suite + fuzzing.
+* *Exit criteria:* the AffineScript tooling row is matched cell-for-cell.
+
+=== Phase 6 — ABI / FFI
+
+* `src/abi/` in Idris2 (`Types`, `Layout`, `Foreign`); Zig FFI — exactly
+  mirroring AffineScript's in-progress ABI.
+* *Exit criteria:* ABI status reaches *in progress* parity.
+
+=== Phase 7 — Grades, registry, RSR FULL
+
+* Author `spec/{ARG,FRG,TRG}-PROFILE.adoc`; honour the cross-axis
+  invariants (`ARG ≤ TRG`; `ARG-A` requires `FRG ≥ B`).
+* Reach `RSR FULL` repository hygiene.
+* Register in the BoJ `lang-mcp` cartridge; add a row to
+  `language-status-tracker.jl`.
+* *Exit criteria:* `TOOLING-STATUS.adoc` shows KitchenSpeak at
+  AffineScript's grade row or better, with `FRG` strictly ahead.
+
+== Parity scorecard
+
+The single-glance "are we there yet" against the target. Updated as
+phases close.
+
+[cols="2,1,1,1", options="header"]
+|===
+| Axis | AffineScript | KitchenSpeak (now) | KitchenSpeak (target)
+
+| Proofs / `formal`   | none (gap)        | Dough + PoachedEgg (hand-verified) | core library machine-checked
+| Front end           | OCaml + parser    | grammar.ebnf only | OCaml lexer + parser
+| Type checker        | OCaml             | —                 | seven-type checker
+| LSP / DAP           | Rust ✓            | —                 | ks-lsp / ks-dap
+| Linter / formatter  | ✓ / stub          | —                 | ✓ / ✓
+| Tree-sitter         | ✓                 | —                 | ✓
+| Doc gen / pkg mgr   | ✓ / ✓             | —                 | ✓ / ✓
+| ABI (Idris2 + Zig)  | in progress       | —                 | in progress
+| FRG                 | E                 | TBD               | ≥ E, climbing to D
+| RSR                 | FULL              | TBD               | FULL
+|===
+
+== Status
+
+Phase 0 complete; Phase 1 commenced (1a harness + 1b PoachedEgg landed).
+Remaining work tracked per-phase above and mirrored in the monorepo's
+`TOOLING-STATUS.adoc` KitchenSpeak row.