feat(panel-clades): graded clade contracts over typed-wasm's grade kernel (PWL-01)

.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

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 `+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
+(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

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
 

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]}")/.." || 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'
+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"
+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)"
+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)"

panel-clades/scripts/fetch-siblings.sh

@@ -0,0 +1,39 @@
+#!/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 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:-117bbf895b513673ba06eb6c4ebb0e26e276e295}"
+
+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"

panel-clades/src/abi/PanelClades/ABI/Grades.idr

@@ -0,0 +1,188 @@
+-- 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
+
+||| 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 (maxLub 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