From 18a22e359afbe2b164039d60894f33dab26d7bcc Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 14 Oct 2026 01:38:50 +0000
Subject: [PATCH 1/5] feat(panel-clades): graded clade contracts over
 typed-wasm's grade kernel

PanelClades.ABI.Grades grades a clade's resource contract in typed-wasm's
Idris2 grade kernel (TypedWasm.ABI.ResourceAlgebra, transcribed from
hyperpolymath/resource-algebra), imported at a pin, not re-declared:

  - panel state by OCCUPANCY (HWM): StateWithin, and phasesWithin, the
    reclamation law at the panel (a second phase fits in what the first
    left);
  - the Panel-N -> Panel-W crossing by LOSS: LossWithin (total collapse is
    never within tolerance), crossTwice (losses add, lossSeq), betterOfTwo
    (the less lossy translation, lossAlt);
  - CladeResourceContract, its {grade, algebra} pairs (TaggedGrade), and the
    neurosym-bridge contract: state peak 48 / drift 16 within 64, crossing
    loss 2 within 3.  DESIGNED: declared values for the owner to confirm,
    not measurements;
  - the computed separation at the panel: two phases occupy 64 but cost 96.

panel-clades/scripts/fetch-siblings.sh pins typed-wasm at main 9403258
(the kernel's landing, typed-wasm#271).  panel-clades/scripts/check-abi.sh
builds the kernel there, builds panel-clades-grades.ipkg against it (exit 0
and no Error line), and requires tests/reject/{OverBudget,
CollapseWithinTolerance}.idr to be refused at their invalid declarations
for the intended reason.  It runs as job panel-clades-abi in
build-validation.yml (Idris2 0.8.0 built from its tag; no binaries exist).

schema/typell-grade.schema.json is the {grade, algebra} wire payload for
TypeLL (DESIGNED: the Panel-L JSON-RPC wiring is not built).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
---
 .github/workflows/build-validation.yml        |  29 +++
 panel-clades/scripts/check-abi.sh             |  72 +++++++
 panel-clades/scripts/fetch-siblings.sh        |  38 ++++
 .../src/abi/PanelClades/ABI/Grades.idr        | 195 ++++++++++++++++++
 panel-clades/src/abi/panel-clades-grades.ipkg |  16 ++
 .../tests/reject/CollapseWithinTolerance.idr  |  17 ++
 panel-clades/tests/reject/OverBudget.idr      |  17 ++
 schema/typell-grade.schema.json               |  71 +++++++
 8 files changed, 455 insertions(+)
 create mode 100755 panel-clades/scripts/check-abi.sh
 create mode 100755 panel-clades/scripts/fetch-siblings.sh
 create mode 100644 panel-clades/src/abi/PanelClades/ABI/Grades.idr
 create mode 100644 panel-clades/src/abi/panel-clades-grades.ipkg
 create mode 100644 panel-clades/tests/reject/CollapseWithinTolerance.idr
 create mode 100644 panel-clades/tests/reject/OverBudget.idr
 create mode 100644 schema/typell-grade.schema.json

diff --git a/.github/workflows/build-validation.yml b/.github/workflows/build-validation.yml
index 6511a2e6..2c42e863 100644
--- a/.github/workflows/build-validation.yml
+++ b/.github/workflows/build-validation.yml
@@ -61,3 +61,32 @@ jobs:
 
       - name: Panel wiring verification gate
         run: ./tools/pcc/target/release/panll panel verify --repo-root .
+
+  # panel-clades grades ABI: PanelClades.ABI.Grades typechecks against
+  # typed-wasm's grade kernel at its pin, and the expected rejections are
+  # refused.  Idris2 publishes no binaries, so 0.8.0 is built from its tag.
+  panel-clades-abi:
+    runs-on: ubuntu-latest
+    timeout-minutes: 40
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+
+      - name: Install Chez Scheme and GMP
+        run: |
+          sudo apt-get update -qq
+          sudo apt-get install -y -qq chezscheme libgmp-dev
+
+      - name: Build Idris2 0.8.0 from source
+        run: |
+          git clone --quiet --depth 1 --branch v0.8.0 https://github.com/idris-lang/Idris2 "$RUNNER_TEMP/idris2-src"
+          make -C "$RUNNER_TEMP/idris2-src" bootstrap SCHEME=scheme -j"$(nproc)" > "$RUNNER_TEMP/idris2-build.log" 2>&1 \
+            || { tail -60 "$RUNNER_TEMP/idris2-build.log"; exit 1; }
+          make -C "$RUNNER_TEMP/idris2-src" install > "$RUNNER_TEMP/idris2-install.log" 2>&1 \
+            || { tail -60 "$RUNNER_TEMP/idris2-install.log"; exit 1; }
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+
+      - name: panel-clades grades ABI
+        run: bash panel-clades/scripts/check-abi.sh
diff --git a/panel-clades/scripts/check-abi.sh b/panel-clades/scripts/check-abi.sh
new file mode 100755
index 00000000..1caf8448
--- /dev/null
+++ b/panel-clades/scripts/check-abi.sh
@@ -0,0 +1,72 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# check-abi.sh — typecheck the panel-clades grades ABI against typed-wasm's
+# grade kernel at its pin, and run the expected rejections.
+#
+#   1. fetch typed-wasm at the pin (scripts/fetch-siblings.sh) and build its
+#      ABI package (the kernel's TTCs);
+#   2. build src/abi/panel-clades-grades.ipkg against them: exit 0 AND no
+#      `Error:` line (idris2 can exit 0 while printing an error);
+#   3. every tests/reject/*.idr must FAIL at its `invalid` declaration with
+#      the message in its `-- EXPECT:` line, and not for a scope/parse/path
+#      reason.
+#
+# A missing toolchain is a failure, never a skip.  Types.idr / Layout.idr /
+# Foreign.idr are NOT checked: they do not typecheck (src/abi/README.adoc).
+set -uo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+ROOT="$(pwd)"
+OUT="_build/check-abi"
+WRONG_REASON='Undefined name|Couldn.t parse|Parse error|not in the source directory|Can.t find import|Module .* not found|INTERNAL ERROR|does not match file name'
+fail=0
+pass() { printf 'PASS: %s\n' "$1"; }
+err()  { printf 'FAIL: %s\n' "$1"; fail=1; }
+die()  { printf 'FAIL: %s\n' "$1"; exit 1; }
+
+command -v idris2 >/dev/null || die "idris2 not on PATH (a gate that cannot run must not report OK)"
+iv="$(idris2 --version)"; echo "$iv"
+case "$iv" in *"version 0.8.0"*) ;; *) [ -n "${ALLOW_ANY_IDRIS2:-}" ] || die "Idris2 0.8.0 required (set ALLOW_ANY_IDRIS2=1 to try another)" ;; esac
+rm -rf "$OUT"; mkdir -p "$OUT"
+
+bash scripts/fetch-siblings.sh || die "could not fetch typed-wasm at its pin"
+TW="_build/dependencies/typed-wasm/src/abi"
+rm -rf "$TW/build"
+(cd "$TW" && idris2 --build typed-wasm.ipkg) > "$OUT/kernel.log" 2>&1
+if [ $? -ne 0 ] || grep -q '^Error' "$OUT/kernel.log"; then
+  grep -A10 '^Error' "$OUT/kernel.log" | head -30; die "typed-wasm's ABI package does not build at the pin"
+fi
+pass "typed-wasm grade kernel built at $(git -C _build/dependencies/typed-wasm rev-parse --short HEAD)"
+KTTC="$ROOT/$TW/build/ttc"
+
+rm -rf src/abi/build
+(cd src/abi && IDRIS2_PATH="$KTTC" idris2 --build panel-clades-grades.ipkg) > "$OUT/grades.log" 2>&1
+st=$?
+if [ "$st" -eq 0 ] && ! grep -q '^Error' "$OUT/grades.log"; then
+  pass "panel-clades-grades.ipkg builds against the kernel ($(grep -c ': Building ' "$OUT/grades.log") module(s), 0 errors)"
+else
+  grep -A12 '^Error' "$OUT/grades.log" | head -40; err "panel-clades-grades.ipkg (exit $st)"
+fi
+PTTC="$ROOT/src/abi/build/ttc"
+
+n=0
+for f in tests/reject/*.idr; do
+  [ -e "$f" ] || { err "no tests/reject/*.idr fixtures"; break; }
+  n=$((n + 1)); name="$(basename "$f" .idr)"
+  expect="$(sed -n 's/^-- EXPECT: //p' "$f" | head -1)"
+  decl="$(grep -nE '^invalid[[:space:]]*:' "$f" | head -1 | cut -d: -f1)"
+  log="$OUT/reject-$name.log"
+  (cd tests/reject && IDRIS2_PATH="$KTTC:$PTTC" idris2 --build-dir "$ROOT/$OUT/reject-build" --check "$name.idr") > "$log" 2>&1
+  loc="$(grep -oE "^${name}:[0-9]+:" "$log" | head -1 | cut -d: -f2)"
+  if [ -z "$expect" ] || [ -z "$decl" ]; then err "reject $name: no '-- EXPECT:' line or 'invalid :' declaration"
+  elif ! grep -q '^Error' "$log"; then cat "$log"; err "reject $name: ACCEPTED"
+  elif grep -qE "$WRONG_REASON" "$log"; then cat "$log"; err "reject $name: refused for the WRONG reason"
+  elif [ -z "$loc" ] || [ "$loc" -lt "$decl" ]; then cat "$log"; err "reject $name: error not at its invalid declaration"
+  elif ! grep -qE -- "$expect" "$log"; then cat "$log"; err "reject $name: not refused with: $expect"
+  else pass "rejected $name at line $loc ($expect)"; fi
+done
+
+echo
+[ "$fail" -eq 0 ] || { echo "PANEL-CLADES ABI CHECK FAILED"; exit 1; }
+echo "OK: panel-clades grades ABI — builds against the kernel, ${n} rejection(s)"
diff --git a/panel-clades/scripts/fetch-siblings.sh b/panel-clades/scripts/fetch-siblings.sh
new file mode 100755
index 00000000..45e2cce0
--- /dev/null
+++ b/panel-clades/scripts/fetch-siblings.sh
@@ -0,0 +1,38 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Fetch the sibling repositories the panel-clades ABI consumes, at pinned
+# commits (pattern: residual-evidence-types / choreographic-types).
+#
+#   typed-wasm — its Idris2 grade kernel (src/abi/TypedWasm/ABI/ResourceAlgebra*,
+#                transcribed from hyperpolymath/resource-algebra @ cf9235c) is
+#                imported by PanelClades.ABI.Grades, never re-declared.
+#
+# Pinned at typed-wasm main 9403258 (#271, the kernel's landing).  Re-pin
+# deliberately, one commit per pin.  Override for an experiment with
+#   TYPED_WASM_COMMIT=<sha> panel-clades/scripts/fetch-siblings.sh
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+
+TYPED_WASM_COMMIT="${TYPED_WASM_COMMIT:-940325876dcc3e768e853dec2bb9b290200cb16a}"
+
+fetch() { # fetch <name> <commit>
+  local name="$1" commit="$2" dir="_build/dependencies/$1"
+  mkdir -p _build/dependencies
+  if [ ! -d "$dir/.git" ]; then
+    git clone --quiet "https://github.com/hyperpolymath/${name}.git" "$dir"
+  fi
+  if ! git -C "$dir" cat-file -e "${commit}^{commit}" 2>/dev/null; then
+    git -C "$dir" fetch --quiet origin
+  fi
+  git -C "$dir" checkout --quiet --detach "$commit"
+  local got
+  got="$(git -C "$dir" rev-parse HEAD)"
+  case "$got" in
+    "$commit"*) echo "${name} at ${got}" ;;
+    *) echo "ERROR: ${name} resolved to ${got}, expected ${commit}" >&2; exit 1 ;;
+  esac
+}
+
+fetch typed-wasm "$TYPED_WASM_COMMIT"
diff --git a/panel-clades/src/abi/PanelClades/ABI/Grades.idr b/panel-clades/src/abi/PanelClades/ABI/Grades.idr
new file mode 100644
index 00000000..0ee8ba32
--- /dev/null
+++ b/panel-clades/src/abi/PanelClades/ABI/Grades.idr
@@ -0,0 +1,195 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Graded clade resource contracts for PanLL panel-clades.
+|||
+||| A clade's resource contract is graded in typed-wasm's grade kernel
+||| (TypedWasm.ABI.ResourceAlgebra, transcribed from hyperpolymath/
+||| resource-algebra), imported at the pin in
+||| panel-clades/scripts/fetch-siblings.sh — not re-declared here:
+|||
+|||   * panel state is graded by OCCUPANCY (the kernel's HWM instance): the
+|||     high-water mark of the panel's live state, and what it still holds
+|||     at the end of a phase;
+|||   * the Panel-N → Panel-W crossing is graded by LOSS (the kernel's Loss
+|||     instance, min-plus): how much a neural result loses on its way to
+|||     the world panel (translation, confidence gating), with total
+|||     collapse (Infinity) never within tolerance.
+|||
+||| The two must stay apart: an occupancy bound is not a cost bound
+||| (resource-algebra S-1; `panelPhasesOccupancy` vs `panelPhasesCost`
+||| below), and loss alternatives keep the LESS lossy branch.
+|||
+||| Status: the lemmas below are PROVEN (idris2 --build against the pinned
+||| kernel).  The contract for `neurosym-bridge` at the end is DESIGNED: its
+||| budgets are declared values for the owner to confirm, not measurements,
+||| and nothing in the panel runtime yet emits or checks these grades.
+|||
+||| No unsafe casts, postulates or totality escapes.  %default total.
+
+module PanelClades.ABI.Grades
+
+import Data.Nat
+import TypedWasm.ABI.ResourceAlgebra
+import TypedWasm.ABI.ResourceAlgebra.Nat
+import TypedWasm.ABI.ResourceAlgebra.Loss
+import TypedWasm.ABI.ResourceAlgebra.MaxPlus
+import TypedWasm.ABI.ResourceAlgebra.HWM
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Which algebra a grade comes from (the `algebra` field on the TypeLL wire)
+--------------------------------------------------------------------------------
+
+||| The kernel algebra a grade is drawn from.  Mirrors the `algebra` field of
+||| schema/typell-grade.schema.json.
+public export
+data GradeAlgebra = AlgLoss | AlgMaxPlus | AlgHWM
+
+||| The carrier of each algebra.
+public export
+GradeOf : GradeAlgebra -> Type
+GradeOf AlgLoss    = LossGrade
+GradeOf AlgMaxPlus = MaxPlusGrade
+GradeOf AlgHWM     = HWMGrade
+
+||| A grade tagged with its algebra: the `{grade, algebra}` pair.
+public export
+record TaggedGrade where
+  constructor MkTaggedGrade
+  algebra : GradeAlgebra
+  grade   : GradeOf algebra
+
+--------------------------------------------------------------------------------
+-- Panel state: occupancy (HWM)
+--------------------------------------------------------------------------------
+
+||| The panel's live state stays within its budget: peak ≤ budget.
+public export
+data StateWithin : HWMGrade -> Nat -> Type where
+  MkStateWithin : {g : HWMGrade} -> {budget : Nat} ->
+                  LTE (peak g) budget -> StateWithin g budget
+
+||| max is the least upper bound (local: the pinned kernel predates
+||| typed-wasm's `maxLub`; drop this when re-pinned past it).
+maxLeast : {a, b, c : Nat} -> LTE a c -> LTE b c -> LTE (maximum a b) c
+maxLeast LTEZero     q           = q
+maxLeast (LTESucc p) LTEZero     = LTESucc p
+maxLeast (LTESucc p) (LTESucc q) = LTESucc (maxLeast p q)
+
+||| Two phases of a panel's life (e.g. before and after it transmutes): the
+||| second starts from what the first still holds, so the run fits the
+||| budget if the first phase does and the second fits in what the first
+||| left.  This is the reclamation law (occupancy-types R-2) at the panel.
+public export
+phasesWithin : {a, b : HWMGrade} -> {m : Nat} ->
+               StateWithin a m -> LTE (drift a + peak b) m ->
+               StateWithin (hwmSeq a b) m
+phasesWithin {a = MkHWM p1 n1 _} {b = MkHWM p2 n2 _} (MkStateWithin fits) after =
+  MkStateWithin (maxLeast fits after)
+
+--------------------------------------------------------------------------------
+-- The Panel-N → Panel-W crossing: loss
+--------------------------------------------------------------------------------
+
+||| The crossing loses no more than `tolerance`.  Total collapse (Infinity)
+||| has no constructor: it is never within tolerance.
+public export
+data LossWithin : LossGrade -> Nat -> Type where
+  MkLossWithin : {k, tolerance : Nat} -> LTE k tolerance -> LossWithin (Finite k) tolerance
+
+||| Two crossings in sequence (Panel-N → bridge → Panel-W): losses add, and
+||| so do the tolerances.  The kernel's sequence (lossSeq).
+public export
+crossTwice : {a, b : LossGrade} -> {n, m : Nat} ->
+             LossWithin a n -> LossWithin b m -> LossWithin (lossSeq a b) (n + m)
+crossTwice (MkLossWithin p) (MkLossWithin q) = MkLossWithin (plusLteMonotone p q)
+
+||| min is below its left argument.
+minLeLeft : (a, b : Nat) -> LTE (minimum a b) a
+minLeLeft Z     _     = LTEZero
+minLeLeft (S a) Z     = LTEZero
+minLeLeft (S a) (S b) = LTESucc (minLeLeft a b)
+
+||| Keeping the less lossy of two translations stays within tolerance.  The
+||| kernel's alternatives (lossAlt = min).
+public export
+betterOfTwo : {a, b : LossGrade} -> {n : Nat} ->
+              LossWithin a n -> LossWithin b n -> LossWithin (lossAlt a b) n
+betterOfTwo {a = Finite x} {b = Finite y} (MkLossWithin p) (MkLossWithin _) =
+  MkLossWithin (lteTrans (minLeLeft x y) p)
+
+--------------------------------------------------------------------------------
+-- The contract
+--------------------------------------------------------------------------------
+
+||| A clade's resource contract, graded in the kernel.
+public export
+record CladeResourceContract where
+  constructor MkCladeResourceContract
+  ||| The clade's id (its A2ML `clade-metadata.id`).
+  cladeId       : String
+  ||| Panel state over a run, as an occupancy grade (HWM).
+  stateGrade    : HWMGrade
+  ||| Declared state budget, in the panel's state units.
+  stateBudget   : Nat
+  ||| The state fits the budget.
+  stateFits     : StateWithin stateGrade stateBudget
+  ||| Loss on the Panel-N → Panel-W crossing (Loss).
+  crossingLoss  : LossGrade
+  ||| Declared loss tolerance for the crossing.
+  lossTolerance : Nat
+  ||| The crossing stays within tolerance.
+  crossingFits  : LossWithin crossingLoss lossTolerance
+
+||| The contract's two grades on the wire, each tagged with its algebra.
+public export
+contractGrades : CladeResourceContract -> List TaggedGrade
+contractGrades c =
+  [ MkTaggedGrade AlgHWM  c.stateGrade
+  , MkTaggedGrade AlgLoss c.crossingLoss ]
+
+--------------------------------------------------------------------------------
+-- One graded clade contract: neurosym-bridge (DESIGNED; values to confirm)
+--------------------------------------------------------------------------------
+--
+-- neurosym-bridge (kind `bridge`, clades/neurosym-bridge/NeurosymBridge.a2ml)
+-- translates neural results (Panel-N) into symbolic / world terms with
+-- confidence gating.  Declared, not measured: its panel state peaks at 48
+-- units and holds 16 between inferences, within a budget of 64; the
+-- crossing loses 2 (two gating stages may each drop a candidate), within a
+-- tolerance of 3.
+
+||| neurosym-bridge's panel state over one inference.
+public export
+neurosymState : HWMGrade
+neurosymState = MkHWM 48 16 (lteAddRight 16)
+
+||| The graded contract.
+public export
+neurosymBridgeContract : CladeResourceContract
+neurosymBridgeContract = MkCladeResourceContract
+  "neurosym-bridge"
+  neurosymState 64 (MkStateWithin (lteAddRight 48))
+  (Finite 2) 3 (MkLossWithin (lteAddRight 2))
+
+||| Two inferences back to back stay within budget: the second starts from
+||| the 16 units the first still holds (16 + 48 = 64 ≤ 64).
+public export
+neurosymTwoInferences : StateWithin (hwmSeq Grades.neurosymState Grades.neurosymState) 64
+neurosymTwoInferences =
+  phasesWithin {a = neurosymState} {b = neurosymState}
+    (MkStateWithin (lteAddRight 48)) (lteRefl 64)
+
+||| Occupancy of those two inferences: 64 (the 32 freed between them are
+||| not charged again)...
+public export
+panelPhasesOccupancy : peak (hwmSeq Grades.neurosymState Grades.neurosymState) = 64
+panelPhasesOccupancy = Refl
+
+||| ...whereas reading the same two phases as COST (max-plus) charges 96:
+||| an occupancy budget must not be checked with a cost grade.
+public export
+panelPhasesCost : maxPlusSeq (Val 48) (Val 48) = Val 96
+panelPhasesCost = Refl
diff --git a/panel-clades/src/abi/panel-clades-grades.ipkg b/panel-clades/src/abi/panel-clades-grades.ipkg
new file mode 100644
index 00000000..64e13778
--- /dev/null
+++ b/panel-clades/src/abi/panel-clades-grades.ipkg
@@ -0,0 +1,16 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- The panel-clades modules that typecheck under Idris2 0.8.0, against
+-- typed-wasm's grade kernel at the pin in scripts/fetch-siblings.sh.
+-- Check with panel-clades/scripts/check-abi.sh.
+--
+-- Types.idr / Layout.idr / Foreign.idr are NOT listed: they do not
+-- typecheck (module names do not match their paths, and Types.idr has 11
+-- type errors at 787ac2e; see README.adoc in this directory).
+
+package panelcladesgrades
+
+sourcedir = "."
+
+modules = PanelClades.ABI.Grades
diff --git a/panel-clades/tests/reject/CollapseWithinTolerance.idr b/panel-clades/tests/reject/CollapseWithinTolerance.idr
new file mode 100644
index 00000000..6cc48d3c
--- /dev/null
+++ b/panel-clades/tests/reject/CollapseWithinTolerance.idr
@@ -0,0 +1,17 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- MUST FAIL (panel-clades/scripts/check-abi.sh).
+--
+-- A Panel-N → Panel-W crossing that collapses totally (loss = Infinity, the
+-- kernel's 𝟘) is never within any tolerance.
+-- EXPECT: Mismatch between: Finite .* and Infinity
+module CollapseWithinTolerance
+
+import TypedWasm.ABI.ResourceAlgebra.Loss
+import PanelClades.ABI.Grades
+
+%default total
+
+invalid : LossWithin Infinity 1000
+invalid = MkLossWithin LTEZero
diff --git a/panel-clades/tests/reject/OverBudget.idr b/panel-clades/tests/reject/OverBudget.idr
new file mode 100644
index 00000000..57b40b1e
--- /dev/null
+++ b/panel-clades/tests/reject/OverBudget.idr
@@ -0,0 +1,17 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- MUST FAIL (panel-clades/scripts/check-abi.sh).
+--
+-- A panel whose state peaks at 80 does not fit a budget of 64; no proof of
+-- StateWithin can be written.
+-- EXPECT: Mismatch between: 0 and 16
+module OverBudget
+
+import TypedWasm.ABI.ResourceAlgebra.HWM
+import PanelClades.ABI.Grades
+
+%default total
+
+invalid : StateWithin (MkHWM 80 0 LTEZero) 64
+invalid = MkStateWithin (lteAddRight 64)
diff --git a/schema/typell-grade.schema.json b/schema/typell-grade.schema.json
new file mode 100644
index 00000000..60ae8124
--- /dev/null
+++ b/schema/typell-grade.schema.json
@@ -0,0 +1,71 @@
+{
+  "$schema": "https://json-schema.org/draft/2020-12/schema",
+  "$id": "https://panll.dev/schemas/typell/grade/v1.json",
+  "$comment": "SPDX-License-Identifier: MPL-2.0. STATUS: DESIGNED. The {grade, algebra} payload for grades on the TypeLL JSON-RPC wire (Panel-L <-> TypeLL, planned, not yet wired). Mirrors PanelClades.ABI.Grades.TaggedGrade, whose carriers are typed-wasm's grade kernel (src/abi/TypedWasm/ABI/ResourceAlgebra*, transcribed from hyperpolymath/resource-algebra) at the pin in panel-clades/scripts/fetch-siblings.sh. The algebra tag is required because the three grades are not interchangeable (resource-algebra Separation S-1..S-3): a loss of 2 is not a cost of 2 and not an occupancy of 2.",
+  "title": "TypeLL graded value",
+  "description": "A grade together with the kernel algebra it is drawn from.",
+  "type": "object",
+  "required": ["algebra", "grade"],
+  "additionalProperties": false,
+  "properties": {
+    "algebra": {
+      "description": "loss = min-plus on N u {inf} (echo loss; Panel-N -> Panel-W crossing). maxplus = max-plus on N u {-inf} (worst-case cost). hwm = high-water mark (panel-state occupancy).",
+      "enum": ["loss", "maxplus", "hwm"]
+    },
+    "grade": {
+      "description": "The grade, in the encoding of its algebra."
+    }
+  },
+  "allOf": [
+    {
+      "if": { "properties": { "algebra": { "const": "loss" } } },
+      "then": {
+        "properties": {
+          "grade": {
+            "description": "Finite n, or total collapse.",
+            "oneOf": [
+              { "type": "integer", "minimum": 0 },
+              { "const": "infinity" }
+            ]
+          }
+        }
+      }
+    },
+    {
+      "if": { "properties": { "algebra": { "const": "maxplus" } } },
+      "then": {
+        "properties": {
+          "grade": {
+            "description": "Val n, or no run (-inf).",
+            "oneOf": [
+              { "type": "integer", "minimum": 0 },
+              { "const": "bot" }
+            ]
+          }
+        }
+      }
+    },
+    {
+      "if": { "properties": { "algebra": { "const": "hwm" } } },
+      "then": {
+        "properties": {
+          "grade": {
+            "description": "Peak live state and drift (still held at the end). drift <= peak is an invariant of the kernel type that JSON Schema cannot express; a receiver must check it.",
+            "type": "object",
+            "required": ["peak", "drift"],
+            "additionalProperties": false,
+            "properties": {
+              "peak": { "type": "integer", "minimum": 0 },
+              "drift": { "type": "integer", "minimum": 0 }
+            }
+          }
+        }
+      }
+    }
+  ],
+  "examples": [
+    { "algebra": "hwm", "grade": { "peak": 48, "drift": 16 } },
+    { "algebra": "loss", "grade": 2 },
+    { "algebra": "loss", "grade": "infinity" }
+  ]
+}

From 766e67d5167a3ad80a1a7fa917f74805b488aa9f Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 14 Oct 2026 01:38:50 +0000
Subject: [PATCH 2/5] docs(panel-clades): the ABI's check status, honestly

The ABI README said "Verified by: Idris2 0.8.0 type checker" with every
proof CLOSED.  Checked today: Types.idr / Layout.idr / Foreign.idr do not
typecheck.  Their module names (PanelClades.ABI.*) do not match their
paths, so Idris2 refuses them outright, and laid out at matching paths
Types.idr still has 11 errors (ElabReflection not enabled, DecEq without
Decidable.Equality, unprovable So auto-proofs, Bits used as a type,
pattern matching on types, an auto-bound cladeKindCount).  The README now
says which module does typecheck (Grades.idr, via scripts/check-abi.sh) and
lists those errors; fixing them is left to the owner, as some need
redesign.  Also: SPDX header on that README, a pointer from the TypeLL
clade README to the grade schema, and a CHANGELOG entry.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
---
 CHANGELOG.adoc                         | 18 +++++++++++++++
 panel-clades/clades/typell/README.adoc |  3 +++
 panel-clades/src/abi/README.adoc       | 31 +++++++++++++++++++++++++-
 3 files changed, 51 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 3ff9df14..bfe9e565 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -9,6 +9,24 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === https://github.com/hyperpolymath/panll/compare/v0.1.0...HEAD[Unreleased]
 
+==== Added (2026-10-14 — graded clade contracts over typed-wasm's grade kernel, PWL-01)
+
+* `+panel-clades/src/abi/PanelClades/ABI/Grades.idr+` grades a clade's
+resource contract in typed-wasm's grade kernel, pinned by
+`+panel-clades/scripts/fetch-siblings.sh+` at typed-wasm `+9403258+`. Panel
+state is graded by occupancy (HWM) and the Panel-N → Panel-W crossing by
+loss (Loss). It includes the `+neurosym-bridge+` contract (DESIGNED: the
+budgets are declared values) and the computed occupancy-vs-cost witness
+(64 vs 96).
+* `+panel-clades/scripts/check-abi.sh+` builds it against the kernel and runs
+two expected rejections (`+panel-clades/tests/reject/+`). It runs in CI
+(`+build-validation.yml+`, job `+panel-clades-abi+`).
+* `+schema/typell-grade.schema.json+` defines the `+{grade, algebra}+` wire
+payload for TypeLL (DESIGNED).
+* *Finding:* `+panel-clades/src/abi/{Types,Layout,Foreign}.idr+` do not
+typecheck, because of module/path mismatch and 11 errors in `+Types.idr+`. The
+ABI README now says so.
+
 ==== Changed (2026-05-30 — npm → Deno migration)
 
 * *`+package.json+` + `+package-lock.json+` deleted.* ReScript and
diff --git a/panel-clades/clades/typell/README.adoc b/panel-clades/clades/typell/README.adoc
index 0c214662..15ba21fb 100644
--- a/panel-clades/clades/typell/README.adoc
+++ b/panel-clades/clades/typell/README.adoc
@@ -19,6 +19,9 @@ and universes. All panels MUST degrade gracefully when TypeLL is unavailable.
 * Proof obligation generation
 * Cross-panel dispatch via TypeLLService helpers
 * Backend on port 7800
+* Grades on the wire carry their algebra: `schema/typell-grade.schema.json`
+  (`{grade, algebra}`, algebra ∈ loss / maxplus / hwm, from typed-wasm's grade
+  kernel). DESIGNED — the JSON-RPC wiring to Panel-L is not built yet.
 
 == Integration Points
 
diff --git a/panel-clades/src/abi/README.adoc b/panel-clades/src/abi/README.adoc
index da8cce1a..55b34dee 100644
--- a/panel-clades/src/abi/README.adoc
+++ b/panel-clades/src/abi/README.adoc
@@ -1,3 +1,4 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
 == panel-clades/src/abi/ — Idris2 ABI Formal Proofs
 
 === Purpose
@@ -8,7 +9,8 @@ safety for the Zig FFI layer.
 
 === Boundary
 
-* *Verified by*: Idris2 0.8.0 type checker
+* *Verified by*: Idris2 0.8.0 type checker — today only
+`+PanelClades/ABI/Grades.idr+` (`+scripts/check-abi.sh+`); see Check status
 * *Implemented by*: `+panel-clades/ffi/zig/+` (Zig FFI matching these
 proofs)
 * *Generated output*: `+generated/abi/*.h+` (C headers from ABI
@@ -26,8 +28,35 @@ proofs
 compliance
 
 |`+Foreign.idr+` |FFI function declarations with type signatures
+
+|`+PanelClades/ABI/Grades.idr+` |Graded clade resource contracts over
+typed-wasm's grade kernel: panel state by occupancy (HWM), the Panel-N →
+Panel-W crossing by loss (Loss); the `+neurosym-bridge+` contract
+
+|`+panel-clades-grades.ipkg+` |The package `+scripts/check-abi.sh+` builds
 |===
 
+=== Check status (2026-10-14)
+
+* `+PanelClades/ABI/Grades.idr+` *typechecks* under Idris2 0.8.0 against
+typed-wasm's grade kernel at the pin in `+scripts/fetch-siblings.sh+`
+(`+bash panel-clades/scripts/check-abi.sh+`), with two expected rejections
+(`+tests/reject/+`). Its lemmas are PROVEN; the `+neurosym-bridge+` budgets
+are declared values (DESIGNED), not measurements.
+* `+Types.idr+`, `+Layout.idr+`, `+Foreign.idr+` *do not typecheck* as of
+`+787ac2e+`. Their module names (`+PanelClades.ABI.*+`) do not match their
+paths, so Idris2 refuses them before checking anything. Laid out at
+matching paths, `+Types.idr+` still has 11 errors: `+%runElab+` without
+`+%language ElabReflection+`; `+DecEq+` used without
+`+import Decidable.Equality+` (twice); `+So+` auto-proofs that cannot be
+found for runtime values (`+createHandle+`, `+mkCladeId+`);
+`+Bits (ptrSize p)+` where a type is expected (`+CPtr+`); pattern
+matching on types (`+cSizeOf+`, `+cAlignOf+`); and `+allCladeKinds+` /
+`+cladeKindExhaustive+`, where `+cladeKindCount+` is auto-bound as a
+variable. The proof statuses below were therefore never machine-checked.
+Fixing them is open (owner decision: some need redesign, e.g. sizes by
+type).
+
 === Invariants
 
 * `+%default total+` — all functions must be provably total

From 9530dded0efee0e6cb68cc732e85e8d102911b1d Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 14 Oct 2026 01:47:14 +0000
Subject: [PATCH 3/5] feat(panel-clades): re-pin typed-wasm at 117bbf8; use the
 kernel's maxLub

typed-wasm #273 and #274 have merged, so the pin moves from 9403258 (the
kernel's landing, #271) to main 117bbf8.  #273 added maxLub to the
kernel's Nat lemmas, so Grades.idr's local copy (maxLeast) goes and
phasesWithin uses the kernel's.  check-abi.sh passes at the new pin
(1 module, 0 errors, 2 rejections).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
---
 CHANGELOG.adoc                                  | 2 +-
 panel-clades/scripts/fetch-siblings.sh          | 7 ++++---
 panel-clades/src/abi/PanelClades/ABI/Grades.idr | 9 +--------
 3 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index bfe9e565..9f2bcb26 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -13,7 +13,7 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 * `+panel-clades/src/abi/PanelClades/ABI/Grades.idr+` grades a clade's
 resource contract in typed-wasm's grade kernel, pinned by
-`+panel-clades/scripts/fetch-siblings.sh+` at typed-wasm `+9403258+`. Panel
+`+panel-clades/scripts/fetch-siblings.sh+` at typed-wasm `+117bbf8+`. Panel
 state is graded by occupancy (HWM) and the Panel-N → Panel-W crossing by
 loss (Loss). It includes the `+neurosym-bridge+` contract (DESIGNED: the
 budgets are declared values) and the computed occupancy-vs-cost witness
diff --git a/panel-clades/scripts/fetch-siblings.sh b/panel-clades/scripts/fetch-siblings.sh
index 45e2cce0..5d25ee0d 100755
--- a/panel-clades/scripts/fetch-siblings.sh
+++ b/panel-clades/scripts/fetch-siblings.sh
@@ -9,13 +9,14 @@
 #                transcribed from hyperpolymath/resource-algebra @ cf9235c) is
 #                imported by PanelClades.ABI.Grades, never re-declared.
 #
-# Pinned at typed-wasm main 9403258 (#271, the kernel's landing).  Re-pin
-# deliberately, one commit per pin.  Override for an experiment with
+# Pinned at typed-wasm main 117bbf8 (#274; the kernel landed in #271, its
+# Nat lemmas such as maxLub in #273).  Re-pin deliberately, one commit per
+# pin.  Override for an experiment with
 #   TYPED_WASM_COMMIT=<sha> panel-clades/scripts/fetch-siblings.sh
 set -euo pipefail
 cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 
-TYPED_WASM_COMMIT="${TYPED_WASM_COMMIT:-940325876dcc3e768e853dec2bb9b290200cb16a}"
+TYPED_WASM_COMMIT="${TYPED_WASM_COMMIT:-117bbf895b513673ba06eb6c4ebb0e26e276e295}"
 
 fetch() { # fetch <name> <commit>
   local name="$1" commit="$2" dir="_build/dependencies/$1"
diff --git a/panel-clades/src/abi/PanelClades/ABI/Grades.idr b/panel-clades/src/abi/PanelClades/ABI/Grades.idr
index 0ee8ba32..9b8b9183 100644
--- a/panel-clades/src/abi/PanelClades/ABI/Grades.idr
+++ b/panel-clades/src/abi/PanelClades/ABI/Grades.idr
@@ -71,13 +71,6 @@ data StateWithin : HWMGrade -> Nat -> Type where
   MkStateWithin : {g : HWMGrade} -> {budget : Nat} ->
                   LTE (peak g) budget -> StateWithin g budget
 
-||| max is the least upper bound (local: the pinned kernel predates
-||| typed-wasm's `maxLub`; drop this when re-pinned past it).
-maxLeast : {a, b, c : Nat} -> LTE a c -> LTE b c -> LTE (maximum a b) c
-maxLeast LTEZero     q           = q
-maxLeast (LTESucc p) LTEZero     = LTESucc p
-maxLeast (LTESucc p) (LTESucc q) = LTESucc (maxLeast p q)
-
 ||| Two phases of a panel's life (e.g. before and after it transmutes): the
 ||| second starts from what the first still holds, so the run fits the
 ||| budget if the first phase does and the second fits in what the first
@@ -87,7 +80,7 @@ phasesWithin : {a, b : HWMGrade} -> {m : Nat} ->
                StateWithin a m -> LTE (drift a + peak b) m ->
                StateWithin (hwmSeq a b) m
 phasesWithin {a = MkHWM p1 n1 _} {b = MkHWM p2 n2 _} (MkStateWithin fits) after =
-  MkStateWithin (maxLeast fits after)
+  MkStateWithin (maxLub fits after)
 
 --------------------------------------------------------------------------------
 -- The Panel-N → Panel-W crossing: loss

From a1886754808b4d4c88c81a9dd2779ed00e5e785a Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 14 Oct 2026 01:47:14 +0000
Subject: [PATCH 4/5] fix(panel-clades): check-abi.sh exits if cd fails; test
 the kernel build directly

shellcheck SC2164 and SC2181, the likely source of CodeFactor's one
finding on #145.  The script runs without `set -e` (it collects
failures), so a failed cd would have carried on in the wrong directory.
The kernel-build test now checks the subshell's status directly.  Both
failure branches still fail the gate (checked with an idris2 shim that
refuses the build, and one that prints Error: but exits 0).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
---
 panel-clades/scripts/check-abi.sh | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/panel-clades/scripts/check-abi.sh b/panel-clades/scripts/check-abi.sh
index 1caf8448..3760cee6 100755
--- a/panel-clades/scripts/check-abi.sh
+++ b/panel-clades/scripts/check-abi.sh
@@ -16,7 +16,7 @@
 # A missing toolchain is a failure, never a skip.  Types.idr / Layout.idr /
 # Foreign.idr are NOT checked: they do not typecheck (src/abi/README.adoc).
 set -uo pipefail
-cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." || exit 1
 ROOT="$(pwd)"
 OUT="_build/check-abi"
 WRONG_REASON='Undefined name|Couldn.t parse|Parse error|not in the source directory|Can.t find import|Module .* not found|INTERNAL ERROR|does not match file name'
@@ -33,8 +33,8 @@ rm -rf "$OUT"; mkdir -p "$OUT"
 bash scripts/fetch-siblings.sh || die "could not fetch typed-wasm at its pin"
 TW="_build/dependencies/typed-wasm/src/abi"
 rm -rf "$TW/build"
-(cd "$TW" && idris2 --build typed-wasm.ipkg) > "$OUT/kernel.log" 2>&1
-if [ $? -ne 0 ] || grep -q '^Error' "$OUT/kernel.log"; then
+if ! (cd "$TW" && idris2 --build typed-wasm.ipkg) > "$OUT/kernel.log" 2>&1 \
+   || grep -q '^Error' "$OUT/kernel.log"; then
   grep -A10 '^Error' "$OUT/kernel.log" | head -30; die "typed-wasm's ABI package does not build at the pin"
 fi
 pass "typed-wasm grade kernel built at $(git -C _build/dependencies/typed-wasm rev-parse --short HEAD)"

From 42dbbbe76ffbc15170a2c884e7225916891466da Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 14 Oct 2026 01:59:09 +0000
Subject: [PATCH 5/5] fix(ci): pin Idris2 by commit, drop the checkout token,
 show the log tail

CodeRabbit on #145:
- build-validation.yml fetched Idris2 by its v0.8.0 tag, which can move
  (CWE-494).  It now fetches 15a3e4e70843f7a34100f6470c04b791330788df,
  the commit that tag names, checks HEAD against it, and tags it v0.8.0
  locally so the Makefile still reports 0.8.0 (without a tag it appends
  the short SHA).
- The panel-clades-abi checkout sets persist-credentials: false; the job
  needs no token after checkout (the sibling fetch is anonymous https).
- check-abi.sh printed nothing when idris2 failed without an `Error`
  line (an INTERNAL ERROR, say).  Both build branches now fall back to the
  log tail; checked with an idris2 shim that fails with no Error line.

shellcheck clean; check-abi.sh passes (1 module, 0 errors, 2 rejections).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
---
 .github/workflows/build-validation.yml | 16 ++++++++++++++--
 panel-clades/scripts/check-abi.sh      |  6 ++++--
 2 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/build-validation.yml b/.github/workflows/build-validation.yml
index 2c42e863..a9fae686 100644
--- a/.github/workflows/build-validation.yml
+++ b/.github/workflows/build-validation.yml
@@ -64,15 +64,21 @@ jobs:
 
   # panel-clades grades ABI: PanelClades.ABI.Grades typechecks against
   # typed-wasm's grade kernel at its pin, and the expected rejections are
-  # refused.  Idris2 publishes no binaries, so 0.8.0 is built from its tag.
+  # refused.  Idris2 publishes no binaries, so 0.8.0 is built from source,
+  # fetched by the commit its v0.8.0 tag names (a tag can move; the SHA
+  # cannot).
   panel-clades-abi:
     runs-on: ubuntu-latest
     timeout-minutes: 40
     permissions:
       contents: read
+    env:
+      IDRIS2_COMMIT: 15a3e4e70843f7a34100f6470c04b791330788df  # v0.8.0
     steps:
       - name: Checkout
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Install Chez Scheme and GMP
         run: |
@@ -81,7 +87,13 @@ jobs:
 
       - name: Build Idris2 0.8.0 from source
         run: |
-          git clone --quiet --depth 1 --branch v0.8.0 https://github.com/idris-lang/Idris2 "$RUNNER_TEMP/idris2-src"
+          git init --quiet "$RUNNER_TEMP/idris2-src"
+          git -C "$RUNNER_TEMP/idris2-src" fetch --quiet --depth 1 https://github.com/idris-lang/Idris2 "$IDRIS2_COMMIT"
+          git -C "$RUNNER_TEMP/idris2-src" checkout --quiet --detach FETCH_HEAD
+          test "$(git -C "$RUNNER_TEMP/idris2-src" rev-parse HEAD)" = "$IDRIS2_COMMIT"
+          # Local tag on the verified commit, so the Makefile reports the
+          # release version (0.8.0) rather than 0.8.0-<sha>.
+          git -C "$RUNNER_TEMP/idris2-src" tag v0.8.0
           make -C "$RUNNER_TEMP/idris2-src" bootstrap SCHEME=scheme -j"$(nproc)" > "$RUNNER_TEMP/idris2-build.log" 2>&1 \
             || { tail -60 "$RUNNER_TEMP/idris2-build.log"; exit 1; }
           make -C "$RUNNER_TEMP/idris2-src" install > "$RUNNER_TEMP/idris2-install.log" 2>&1 \
diff --git a/panel-clades/scripts/check-abi.sh b/panel-clades/scripts/check-abi.sh
index 3760cee6..7400dd18 100755
--- a/panel-clades/scripts/check-abi.sh
+++ b/panel-clades/scripts/check-abi.sh
@@ -35,7 +35,8 @@ TW="_build/dependencies/typed-wasm/src/abi"
 rm -rf "$TW/build"
 if ! (cd "$TW" && idris2 --build typed-wasm.ipkg) > "$OUT/kernel.log" 2>&1 \
    || grep -q '^Error' "$OUT/kernel.log"; then
-  grep -A10 '^Error' "$OUT/kernel.log" | head -30; die "typed-wasm's ABI package does not build at the pin"
+  { grep -A10 '^Error' "$OUT/kernel.log" || tail -30 "$OUT/kernel.log"; } | head -30
+  die "typed-wasm's ABI package does not build at the pin"
 fi
 pass "typed-wasm grade kernel built at $(git -C _build/dependencies/typed-wasm rev-parse --short HEAD)"
 KTTC="$ROOT/$TW/build/ttc"
@@ -46,7 +47,8 @@ st=$?
 if [ "$st" -eq 0 ] && ! grep -q '^Error' "$OUT/grades.log"; then
   pass "panel-clades-grades.ipkg builds against the kernel ($(grep -c ': Building ' "$OUT/grades.log") module(s), 0 errors)"
 else
-  grep -A12 '^Error' "$OUT/grades.log" | head -40; err "panel-clades-grades.ipkg (exit $st)"
+  { grep -A12 '^Error' "$OUT/grades.log" || tail -40 "$OUT/grades.log"; } | head -40
+  err "panel-clades-grades.ipkg (exit $st)"
 fi
 PTTC="$ROOT/src/abi/build/ttc"