migrate(phase-c/C1): re-decompose 8 shared/src kernels, 4-gate green

Deep wave 1 of the ReScript -> AffineScript -> wasm migration. Cluster C1
(shared/src leaf modules) re-decomposed into eight pure-integer co-processor
kernels staged under proposals/idaptik/migrated/, each verified end-to-end by
the 4-gate recipe.

Kernels (brain = the integers that cross the wasm boundary; host keeps the
strings/floats/DOM/state — the senses):

  DeviceType      12-device taxonomy: count, validity, code-clamp (lossless)
  PuzzleFormat    difficulty(4)/tier(5) encodings + DLCLoader clamp-to-default
  PortNames       10 coprocessor-domain port taxonomy (= portnames.wasm, the
                  kernel PortNamesCoprocessor.res's JS bridge already targets)
  GameEvent       alertLevel(4, ordered clamp) + direction(6, flat)
  Kernel_Compute  per-domain element caps + the 504/413/404/0 scheduler gate
  Kernel          the 503/404/0 pre-flight gate + domain -> handler router
  RetryPolicy     the 503/504/429 transient classifier + 3-policy config table
  Diagnostics     the <70/<90/>=90 health-band classifier + registry check

Re-decomposed, not transliterated: Promise/async collapsed to the synchronous
status decision; service-locator reads (ResourceAccounting, backend registry)
threaded as explicit integer params; variants re-encoded as closed integer
bands; floats + wall-clock timing kept host-side (timing is a sense).

Four gates green (captured in migrated/EVIDENCE.adoc):
  G1 compile        8/8 -> wasm
  G2 parity         1223/1223 oracle-vs-wasm inputs (independent JS oracles)
  G3 echo-boundary  6 Agda proofs, agda exit 0: 3 LOSSLESS (DeviceType,
                    PortNames, GameEvent direction) + 3 CONTROLLED-LOSS
                    (PuzzleFormat tier clamp, GameEvent alert clamp, Kernel
                    route fan-in) — each collision named and certified
  G4 assail         8/8 clean (no undeclared clamp / unguarded decoder)

Three C1 files are host-side "senses" with no extractable brain and stay in
the host: Coprocessor_Backends.res (registration wiring), PortNamesCoprocessor
.res (JS bridge shim, consumes PortNames.affine), DLCLoader.res (JSON parser;
its one integer fragment is delivered as PuzzleFormat.clamp_tier).

Staged, not applied — per the plan's access gate, the apply + cutover wait on
idaptik write-access (Phase Omega). Ledger: Phase B + Phase C wave 1 DONE;
next = C2 (vm/lib/ocaml instruction set). migration-map.json C1 -> DONE.

https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s

Author: claude

proposals/MIGRATION-PLAN.adoc

@@ -185,10 +185,11 @@ Heuristic:
 [cols="1,1,3",options="header"]
 |===
 | Phase | State | Notes
-| Pre | DONE | #531 echo proof (merged); #532 migration practice + guide + proposals (merged); #533 evangelist toolkit (draft, CI green).
-| A | DONE | Plan + model-per-phase guidance written; determinism doc gained a latency-regimes appendix (verify-don't-transfer + game-vs-deep-space + the 2 SVGs); #533 green (draft, owner to merge). NEXT: PHASE B.
-| B | TODO | Full-corpus triage -> migration-map.{adoc,json}.
-| C+ | TODO | Deep waves via the 4-gate recipe.
+| Pre | DONE | #531 echo proof (merged); #532 migration practice + guide + proposals (merged); #533 evangelist toolkit (*merged* 2026-06-05).
+| A | DONE | Plan + model-per-phase guidance written; determinism doc gained a latency-regimes appendix (verify-don't-transfer + game-vs-deep-space + the 2 SVGs); #533 merged. NEXT: PHASE B.
+| B | DONE | Full-corpus triage complete (2026-06-05). 571 files: *389 MIGRATABLE NOW (68%)*, 71 STRING-GATED (12%), 111 EFFECT-GATED (19%). Non-test: 358 files, 196 migratable (55%). Clusters C1–C12 ordered, leaf-first. Worklist: `proposals/idaptik/migration-map.json`. NEXT: PHASE C — cluster 1 = C1 (shared/src, 11 files) + C2 (vm instructions, 31 files). Switch to *Opus* for re-decomposition.
+| C (C1) | DONE | Deep wave 1 complete (2026-06-05, Opus). Cluster C1 re-decomposed: *8 pure-integer kernels* staged under `proposals/idaptik/migrated/` (DeviceType, PuzzleFormat, PortNames, GameEvent, Kernel_Compute, Kernel, RetryPolicy, Diagnostics); 3 C1 files are host-side "senses" with no brain (Coprocessor_Backends, PortNamesCoprocessor, DLCLoader). *Four gates green:* 8/8 compile, 1223/1223 parity, 6 echo-boundary proofs (agda exit 0; 3 LOSSLESS + 3 CONTROLLED-LOSS), 8/8 assail-clean. Evidence: `migrated/EVIDENCE.adoc`. The per-shape recipe is now established (enum-taxonomy / status-gate / classifier / predicate). NEXT: wave 2 = C2.
+| C2+ | TODO | Remaining deep waves via the 4-gate recipe; next = *C2* (vm/lib/ocaml instruction set, 31 files — the pure-integer reversible VM opcodes). Opus for any novel re-decomposition; Sonnet for the now-rote gate passes (C1 set the pattern). Then C3..C12.
 | F+ | TODO | Compiler walls (string backend, then effects).
 | Ω | TODO (access-gated) | Cutover + ReScript extinction.
 |===

proposals/idaptik/migrated/.gitignore

@@ -0,0 +1,3 @@
+# Compiled wasm is build output, regenerated by every affine-parity run
+# (compile:true) from the staged .affine + config. Not committed.
+*.wasm

proposals/idaptik/migrated/DeviceType/DeviceType.affine

@@ -0,0 +1,47 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+//
+// DeviceType -- the device-type taxonomy co-processor, the pure-integer core
+// extracted from idaptik shared/src/DeviceType.res. Per the DESIGN-VISION
+// ("AffineScript is the brain, JS/Pixi the senses; they pass primitives across
+// the wasm boundary"), the JS host keeps every device-type STRING (portName,
+// fromString) and the per-device mutable defenceFlags record; AffineScript owns
+// only the canonical integer encoding of the twelve device kinds and its
+// validity.
+//
+// The ReScript original is a 12-constructor variant `t` plus a `portName`
+// switch and a `fromString` parser. We re-decompose the variant as the
+// canonical 0..11 integer the constructor order already implies, so the
+// taxonomy is a closed band and validity is one range test. The variant IS the
+// integer; no strings cross the boundary. (We use range guards rather than an
+// enum round-trip because, the band being contiguous, the round-trip would be
+// the identity -- the same flat shape PortNames.affine uses for its 0..9 band.)
+//
+//## Device-type encoding (the header contract for the JS host)
+//   code  device          code  device
+//     0   Laptop            6   Camera
+//     1   Desktop           7   AccessPoint
+//     2   Server            8   PatchPanel
+//     3   Router            9   PowerSupply
+//     4   Switch           10   PhoneSystem (PBX)
+//     5   Firewall         11   FibreHub
+// The encoding is LOSSLESS: twelve distinct kinds map to twelve distinct codes,
+// so the host round-trips device-type <-> code with no collision (certified by
+// echo-boundary, DeviceTypeBoundary.agda). A code outside 0..11 is not a device
+// type: is_valid_device_type reports 0 and clamp_device_type returns the
+// out-of-band sentinel -1 -- never an in-band code, so no in-band collision is
+// introduced (this is a sentinel, not a clamp; assail stays clean).
+
+// The number of canonical device kinds in the taxonomy.
+pub fn device_type_count() -> Int { 12 }
+
+// Whether a host integer names a defined device type. 1 = valid, 0 = out of band.
+pub fn is_valid_device_type(code: Int) -> Int {
+  if code < 0 { 0 } else { if code > 11 { 0 } else { 1 } }
+}
+
+// Canonicalise a host integer: identity on a valid 0..11 code, the out-of-band
+// sentinel -1 otherwise. -1 is not an in-band code, so out-of-band input can
+// never be confused with a real device type (this is a sentinel, not a clamp).
+pub fn clamp_device_type(code: Int) -> Int {
+  if is_valid_device_type(code) == 1 { code } else { -1 }
+}

proposals/idaptik/migrated/DeviceType/DeviceTypeBoundary.agda

@@ -0,0 +1,104 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+--
+-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand.
+--
+-- This module certifies an @boundary encoding-faithfulness verdict for a
+-- concrete host-value -> integer-code table, by reusing the
+-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's
+-- worked Rank / rankCode / rankCode-injective instance.
+--
+-- Source table (host name -> code):
+--   {
+--     "Laptop": 0,
+--     "Desktop": 1,
+--     "Server": 2,
+--     "Router": 3,
+--     "Switch": 4,
+--     "Firewall": 5,
+--     "Camera": 6,
+--     "AccessPoint": 7,
+--     "PatchPanel": 8,
+--     "PowerSupply": 9,
+--     "PhoneSystem": 10,
+--     "FibreHub": 11
+--   }
+
+module DeviceTypeBoundary where
+
+open import Echo                   using (Echo)
+open import EchoImageFactorization using (Injective)
+open import EchoEncodingFaithfulness using (Encoding; module EncodingTheorems)
+
+open import Data.Nat.Base         using (ℕ)
+open import Data.Product.Base     using (Σ; _,_; _×_; proj₁)
+open import Relation.Binary.PropositionalEquality
+                                  using (_≡_; _≢_; refl)
+open import Relation.Nullary      using (¬_)
+
+
+-- The host-side enumerated value (one constructor per table name).
+--   c0 = Laptop
+--   c1 = Desktop
+--   c2 = Server
+--   c3 = Router
+--   c4 = Switch
+--   c5 = Firewall
+--   c6 = Camera
+--   c7 = AccessPoint
+--   c8 = PatchPanel
+--   c9 = PowerSupply
+--   c10 = PhoneSystem
+--   c11 = FibreHub
+data Host : Set where
+  c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 : Host
+
+-- The integer code the pure kernel computes on.
+code : Host → ℕ
+code c0  = 0
+code c1  = 1
+code c2  = 2
+code c3  = 3
+code c4  = 4
+code c5  = 5
+code c6  = 6
+code c7  = 7
+code c8  = 8
+code c9  = 9
+code c10 = 10
+code c11 = 11
+
+-- Injectivity by exhaustive case analysis. The codes are literal
+-- numerals, so listing the diagonal refl clauses is enough: Agda's
+-- coverage checker discharges the off-diagonal pairs as absurd
+-- numeral equalities (mirrors rankCode-injective).
+code-injective : Injective code
+code-injective {c0}  {c0}  _ = refl
+code-injective {c1}  {c1}  _ = refl
+code-injective {c2}  {c2}  _ = refl
+code-injective {c3}  {c3}  _ = refl
+code-injective {c4}  {c4}  _ = refl
+code-injective {c5}  {c5}  _ = refl
+code-injective {c6}  {c6}  _ = refl
+code-injective {c7}  {c7}  _ = refl
+code-injective {c8}  {c8}  _ = refl
+code-injective {c9}  {c9}  _ = refl
+code-injective {c10} {c10} _ = refl
+code-injective {c11} {c11} _ = refl
+
+encoding : Encoding
+encoding = record
+  { Source = Host
+  ; Code   = ℕ
+  ; enc    = code
+  }
+
+-- Re-export the lossless-half headline, instantiated and proved:
+-- every integer code determines its host value uniquely.
+module Theorems = EncodingTheorems encoding
+
+boundary-lossless :
+  (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂
+boundary-lossless = Theorems.encoding-lossless code-injective
+

proposals/idaptik/migrated/DeviceType/devicetype.config.mjs

@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: MPL-2.0
+// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc)
+//
+// affine-parity config for DeviceType.affine (idaptik device-type taxonomy;
+// scalar i32 ABI). The oracle re-derives the 0..11 closed band in plain JS so a
+// codegen regression surfaces as a differential mismatch.
+const valid = (c) => c >= 0 && c <= 11;
+export default {
+  affine: "DeviceType.affine",
+  cases: [
+    { name: "device_type_count()", export: "device_type_count", args: [], oracle: () => 12 },
+    {
+      name: "is_valid_device_type over [-3..15]",
+      export: "is_valid_device_type",
+      args: [[-3, 15]],
+      oracle: (c) => (valid(c) ? 1 : 0),
+    },
+    {
+      name: "clamp_device_type over [-3..15]",
+      export: "clamp_device_type",
+      args: [[-3, 15]],
+      oracle: (c) => (valid(c) ? c : -1),
+    },
+  ],
+};

proposals/idaptik/migrated/Diagnostics/Diagnostics.affine

@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+//
+// Diagnostics -- the device-health band classifier + registry sanity check, the
+// pure-integer core extracted from idaptik shared/src/Diagnostics.res. The
+// ReScript original wraps raw float utilisation percentages and per-backend
+// stats into typed report structures and formatted strings; those reports and
+// strings are host-side (the senses). What IS pure integer is the threshold
+// classification `healthOf` and the `allDomainsRegistered` count check.
+//
+// We re-decompose `healthOf : float -> healthLevel` onto an integer utilisation
+// percentage 0..100 (the host floors the float before crossing the boundary --
+// Math.floor is a sense). The three bands and their cutoffs are unchanged.
+//
+//## Health band encoding (Diagnostics.healthLevel)
+//   band  level     range
+//     0   Healthy   pct < 70
+//     1   Warning   70 <= pct < 90
+//     2   Critical  pct >= 90      (>= 95 is the hard 503 cutoff)
+// health_of is deliberately many-to-one (a whole range folds onto one band);
+// that is the intended classification, not an encoding, so no injectivity is
+// claimed for it. The expected full registry is exactly ten domain backends.
+
+pub fn health_band_count() -> Int { 3 }
+pub fn expected_domain_count() -> Int { 10 }
+
+// Classify an integer utilisation percentage into a health band. Negative input
+// (impossible from a real percentage, but total here) lands in Healthy; >=90
+// in Critical, mirroring the ReScript `< 70 / < 90 / else` ladder.
+pub fn health_of(pct: Int) -> Int {
+  if pct < 70 { return 0; }
+  if pct < 90 { return 1; }
+  2
+}
+
+// 1 iff all ten expected domain backends are registered (Diagnostics
+// .allDomainsRegistered: registeredBackendCount() == 10).
+pub fn all_domains_registered(count: Int) -> Int {
+  if count == expected_domain_count() { 1 } else { 0 }
+}

proposals/idaptik/migrated/Diagnostics/diagnostics.config.mjs

@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: MPL-2.0
+// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc)
+//
+// affine-parity config for Diagnostics.affine (idaptik health-band classifier +
+// registry sanity check; scalar i32 ABI). Oracle re-derives the <70 / <90 / else
+// ladder and the ==10 registry check.
+export default {
+  affine: "Diagnostics.affine",
+  cases: [
+    { name: "health_band_count()", export: "health_band_count", args: [], oracle: () => 3 },
+    { name: "expected_domain_count()", export: "expected_domain_count", args: [], oracle: () => 10 },
+    {
+      name: "health_of over [-5..105]",
+      export: "health_of",
+      args: [[-5, 105]],
+      oracle: (pct) => (pct < 70 ? 0 : pct < 90 ? 1 : 2),
+    },
+    {
+      name: "all_domains_registered over [0..15]",
+      export: "all_domains_registered",
+      args: [[0, 15]],
+      oracle: (count) => (count === 10 ? 1 : 0),
+    },
+  ],
+};

proposals/idaptik/migrated/EVIDENCE.adoc

@@ -0,0 +1,125 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Cluster C1 — four-gate evidence (captured 2026-06-05)
+:toc: macro
+
+[IMPORTANT]
+====
+*Captured run of the 4-gate recipe over the eight cluster-C1 pure-integer
+kernels.* Every number here is reproducible from this directory; the
+re-run commands are in `README.adoc`. Toolchain: AffineScript compiler
+`_build/default/bin/main.exe`, Deno 2.8.2, Agda 2.6.3, echo mirror at
+`/tmp/mirror-boundary`.
+====
+
+toc::[]
+
+== Summary
+
+[cols="2,1,1,1,1",options="header"]
+|===
+| Kernel | G1 compile | G2 parity | G3 boundary | G4 assail
+| `DeviceType`      | OK | 39/39   | LOSSLESS (12)        | clean
+| `PuzzleFormat`    | OK | 74/74   | CONTROLLED-LOSS @0   | clean
+| `PortNames`       | OK | 52/52   | LOSSLESS (10)        | clean
+| `GameEvent`       | OK | 50/50   | LOSSLESS (6) + CL @0 | clean
+| `Kernel_Compute`  | OK | 736/736 | (decision; see note) | clean
+| `Kernel`          | OK | 19/19   | CONTROLLED-LOSS @4   | clean
+| `RetryPolicy`     | OK | 124/124 | (decision; see note) | clean
+| `Diagnostics`     | OK | 129/129 | (decision; see note) | clean
+| *Total*           | *8/8* | *1223/1223* | *6 proofs, agda exit 0* | *8/8 clean*
+|===
+
+== Gate 1 — compile (`main.exe compile … -o …`)
+
+All eight `.affine` sources lower to wasm, exit 0:
+
+----
+[OK]   DeviceType      [OK]   GameEvent       [OK]   RetryPolicy
+[OK]   PuzzleFormat    [OK]   Kernel_Compute  [OK]   Diagnostics
+[OK]   PortNames       [OK]   Kernel
+----
+
+== Gate 2 — parity (oracle-vs-wasm, scalar i32 ABI)
+
+Each kernel swept against an *independent* JS oracle (re-derived in the
+`*.config.mjs`, never reusing AffineScript code) so a codegen regression
+surfaces as a differential mismatch. 1223 inputs, 0 mismatches.
+
+----
+DeviceType ........ 39/39    Kernel_Compute ... 736/736
+PuzzleFormat ...... 74/74    Kernel ........... 19/19
+PortNames ......... 52/52    RetryPolicy ...... 124/124
+GameEvent ......... 50/50    Diagnostics ...... 129/129
+----
+
+`Kernel_Compute.compute_gate` is the widest sweep: the full
+domain × active_calls × data_len × has_backend grid (10 × 4 × 9 × 2 = 720),
+exercising the 504 > 413 > 404 > 0 precedence at every boundary.
+
+== Gate 3 — echo-boundary (Agda-certified encoding faithfulness)
+
+Six host-value→code tables certified against the `EchoEncodingFaithfulness`
+framework; every generated module typechecks (`agda exit 0`). The generated
+proofs are staged next to each kernel (`*Boundary.agda`).
+
+[cols="2,1,3",options="header"]
+|===
+| Module | Verdict | What it certifies
+| `DeviceTypeBoundary`          | LOSSLESS | 12 device kinds → 12 distinct codes; host round-trips device ↔ code.
+| `PortNamesBoundary`           | LOSSLESS | 10 coprocessor domains → ids 0..9; the portnames.wasm bridge contract.
+| `GameEventDirectionBoundary`  | LOSSLESS | 6 directions → codes 0..5.
+| `PuzzleFormatTierBoundary`    | CONTROLLED LOSS | DLCLoader's `parseTier` clamp: unknown numeral collapses to `Tier0` (code 0). Collision certified → no section.
+| `GameEventAlertBoundary`      | CONTROLLED LOSS | ordered alert clamp: below-Green collapses to Green (code 0). Collision certified → no section.
+| `KernelRouteBoundary`         | CONTROLLED LOSS | the router's compute fan-in: six domains share handler class 4. Deliberate forgetting, certified → no section.
+|===
+
+*Note (decision kernels).* `Kernel_Compute.compute_gate`,
+`RetryPolicy.is_transient` and `Diagnostics.health_of` are intentionally
+many-to-one *decisions*, not encodings — they classify rather than name, so no
+injectivity is claimed for them and echo-boundary's encoding lens does not
+apply. Their faithfulness is established by Gate 2 (full-grid parity against an
+independent oracle). Where one of these kernels *does* carry an encoding (the
+shared domain code, the alert/tier taxonomies), that encoding is certified
+above.
+
+== Gate 4 — affine-assail (no undeclared clamp / unguarded decoder)
+
+All eight kernels scan clean (exit 0):
+
+----
+[CLEAN] DeviceType      [CLEAN] Kernel_Compute
+[CLEAN] PuzzleFormat    [CLEAN] Kernel
+[CLEAN] PortNames       [CLEAN] RetryPolicy
+[CLEAN] GameEvent       [CLEAN] Diagnostics
+----
+
+*On clamps and the gate-4 signal.* The in-band clamps in this cluster
+(`PuzzleFormat.clamp_tier`/`clamp_difficulty` → 0, `GameEvent.clamp_alert_level`
+→ 0/3) are written *guard-style* — an explicit validity test then the default —
+rather than as a catch-all `match` arm. assail's `PA-AFF-001` heuristic targets
+the match-arm shape (e.g. SecurityRank's `Invalid(v) => …`, which it correctly
+flags as a declared clamp); guard-style clamps present no catch-all arm and so
+scan clean. This is sound here because the controlled-loss of every one of these
+clamps is *independently certified by Gate 3* (the `…Boundary.agda` proofs
+above). Gate 3 (the clamp is controlled-loss-certified) and Gate 4 (no
+*undeclared* match-arm clamp) together account for every boundary in the
+cluster. The out-of-band *sentinels* (`-1` in DeviceType/PortNames/GameEvent/
+PuzzleFormat) are not clamps — they map outside the in-band range, so no in-band
+collision is introduced and nothing is lost.
+
+== Host-side files (no pure-integer brain — the "senses")
+
+Three C1 files carry no extractable integer core and stay host-side:
+
+* `Coprocessor_Backends.res` — backend-registration wiring (ten `register()`
+  side-effects; the order is the only datum, and it is fixed).
+* `PortNamesCoprocessor.res` — the JS-bridge binding shim that *consumes*
+  `PortNames.affine` (→ portnames.wasm). The shim stays; the kernel it binds is
+  delivered here.
+* `DLCLoader.res` — a JSON parser/serialiser (`Js.String2.*` / `Js.Json.*`
+  throughout). Its one integer fragment, `parseTier`'s numeral clamp, is
+  delivered as `PuzzleFormat.clamp_tier` (certified controlled-loss above); the
+  rest is irreducibly string/JSON host work. (The Phase-B migratability tool
+  bucketed this MIGRATABLE-NOW because it scans the modern `String.*` API, not
+  the legacy `Js.String2.*` this file uses — recorded here as a triage erratum.)