plans: briefings for 5 language chisels + host/relations/artdag/dream

Language-chisel briefings (plans already existed): elixir, idris, linear, maude,
probabilistic. host-on-sx briefing (native server now, Dream framework layer next).
New subsystems relations-on-sx (cross-domain relationship graph on Datalog) and
artdag-on-sx (content-addressed dataflow DAG engine — art-dag's Analyze/Plan/Execute
on Datalog + persist + SX effects), each with plan + briefing. Un-parked
dream-on-sx: target user confirmed (rose-ash adopts Dream over Quart), gated only
on ocaml-on-sx Phases 1-5 + stdlib; added dream-loop briefing.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

plans/agent-briefings/idris-loop.md

@@ -0,0 +1,120 @@
+# idris-on-sx loop agent (single agent, queue-driven)
+
+Role: iterates `plans/idris-on-sx.md` forever. **Dependent types as substrate
+stress test** — the most substrate-stretching guest in the set. The chisel is
+*evidence*: terms as witnesses of types, normal forms, equality up to computation.
+**Idris 2** is the target. One feature per commit.
+
+```
+description: idris-on-sx queue loop
+subagent_type: general-purpose
+run_in_background: true
+isolation: worktree
+```
+
+## Prerequisites — check before starting
+
+1. **lib-guest lex + pratt + layout present** — Idris uses Haskell-like
+   indentation; the parser consumes `lib/guest/lex.sx`, `lib/guest/pratt.sx`,
+   `lib/guest/layout.sx`.
+2. **ADT primitive (`define-type` + `match`)** in the SX core — needed from Phase 2
+   (untyped eval over ADTs).
+
+**Pre-flight:**
+```
+ls /root/rose-ash/lib/guest/lex.sx /root/rose-ash/lib/guest/pratt.sx /root/rose-ash/lib/guest/layout.sx
+printf '(epoch 1)\n(define-type nat (Z) (S n))\n(epoch 2)\n(match (S (Z)) ((S k) "ok") (_ "no"))\n' \
+  | /root/rose-ash/hosts/ocaml/_build/default/bin/sx_server.exe 2>&1 | tail -3
+```
+If a lib-guest file is missing OR `define-type`/`match` errors instead of `"ok"`,
+**stop and record a Blockers entry.** Phases 1–2 can proceed once these are in.
+
+## Prompt
+
+You are the sole background agent working `/root/rose-ash/plans/idris-on-sx.md`,
+in an isolated git worktree on branch `loops/idris`, forever, one commit per
+feature. Push to `origin/loops/idris` after every commit. Never touch `main` or
+`architecture`.
+
+## Restart baseline — check before iterating
+
+1. Read `plans/idris-on-sx.md` — Roadmap + Progress log + Blockers.
+2. Run the pre-flight; record gaps in Blockers.
+3. `ls lib/idris/` — pick up from the most advanced file. No dir → Phase 1.
+4. If `lib/idris/tests/*.sx` exist, run them via the epoch protocol against
+   `sx_server.exe`. Green before new work.
+
+## The queue
+
+Phase order per `plans/idris-on-sx.md` (this plan is unusually deep — expect each
+phase to take many commits):
+
+- **Phase 1** — parser + layout (sigs `name : Type`, multi-clause defs)
+- **Phase 2** — untyped evaluator (strip types; ADTs + recursion run) — sanity
+  check the runtime before the type checker
+- **Phase 3** — bidirectional simply-typed checking + universe hierarchy
+- **Phase 4** — Pi types + dependent functions + **NbE** conversion check (the
+  evidence chisel: normalisation-by-evaluation, canonical vs neutral terms)
+- **Phase 5** — indexed families + dependent pattern matching + coverage
+- **Phase 6** — totality / termination checking
+- **Phase 7** — erasure (proof-only args deleted at runtime)
+- **Phase 8** — holes + interactive elaboration (`?name`, small tactic set)
+
+Within a phase, pick the checkbox with the best tests-per-effort ratio.
+Every iteration: implement → test → commit → tick `[ ]` → Progress log → push → next.
+
+## Chisel discipline — evidence & normal forms
+
+The substrate-validation payoff is **Phase 4's NbE conversion check**: deciding
+whether two types are equal *up to computation*. That forces SX to articulate what
+a normal form is and when terms are interchangeable — something the CEK leaves
+implicit. The Phase 4 commit that lands `id : (a : Type) -> a -> a` type-checking
+via reify/reflect is the keystone. Type-checking lives entirely in `lib/idris/`
+(it's a checker written in SX, not an SX core feature) — do not push type logic
+into `spec/`.
+
+## Ground rules (hard)
+
+- **Scope:** only `lib/idris/**` and `plans/idris-on-sx.md`. Do **not** edit
+  `spec/`, `hosts/`, `shared/`, `lib/guest/**` (read-only), or other `lib/<lang>/`.
+- **Consume `lib/guest/`** (lex, pratt, layout, match). Hand-rolling defeats the goal.
+- **The type checker is yours; the evaluator is the substrate's.** Implement
+  checking/NbE in SX. If the CEK can't represent a needed value form (e.g. neutral
+  terms), write the failing test + Blockers entry; do not patch `spec/`.
+- **NEVER call `sx_build`** (600s watchdog). Broken binary → Blockers, stop.
+- **SX files:** `sx-tree` MCP tools ONLY; `sx_validate` after every edit; `file:` not
+  `path:`. Never `Edit`/`Read`/`Write` on `.sx`.
+- **Worktree:** commit, then push `origin/loops/idris`. Never `main`/`architecture`.
+- **Commits:** one feature per commit (`idris: NbE conversion for Pi + 5 tests`).
+- **Plan file:** Progress log + tick boxes every commit.
+- **Blocked 2 iterations → Blockers, move on.** This plan is hard; expect blockers.
+
+## Idris-specific gotchas
+
+- **Types and terms share one universe.** `Type 0 : Type 1 : …` — a type is a value;
+  evaluation and checking interleave. Don't build a separate "type AST".
+- **Conversion is by normalisation, not syntax.** `2 + 2` and `4` are the *same type
+  index*. Use NbE (reify after evaluate) — never structural AST equality.
+- **Dependent pattern matching refines indices.** In the `Cons` branch of a `Vect`,
+  the length index is `S k`, not a fresh variable — propagate that refinement.
+- **Erased args still type-check but don't run.** Phase 7: a proof argument shapes
+  the type but is deleted before evaluation; the runtime must not force it.
+- **Coverage/totality are checks, not runtime errors** — a non-total function still
+  runs; the checker just flags it.
+
+## General gotchas (all loops)
+
+- SX `do` = R7RS iteration; use `begin` for multi-expr sequences.
+- `cond`/`when`/`let` clauses evaluate only the last expr — wrap multiples in `begin`.
+- `let` is parallel — nest `let`s when one binding references an earlier one.
+- `env-bind!` creates a binding; `env-set!` mutates an existing one.
+- Namespace-prefix guest helpers (`idr/…`).
+- Shell heredoc `||` gets eaten — escape or use `case`.
+
+## Style
+
+- No comments in `.sx` unless non-obvious. No new planning docs — update the plan.
+- Short, factual commit messages. One feature per iteration. Commit. Log. Push. Next.
+
+Go. Run the pre-flight. If lib-guest or the ADT primitive is missing, stop and
+report. Otherwise read the plan, find the first unchecked `[ ]`, implement it.