migration B+C: full-corpus triage + C1 deep wave (8 kernels, 4-gate green)

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),
+    },
+  ],
+};