// SPDX-License-Identifier: CC-BY-SA-4.0
// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
= idaptik migration — staged kernels (Phase C cluster C1, Phase D cluster C2)
:toc: macro

[IMPORTANT]
====
*Staged, four-gate-verified, applyable units — not yet applied.* Per the
migration plan's access gate, idaptik-bound work lands here under
`proposals/idaptik/migrated/<Name>/` until idaptik is opened for writes or the
owner accepts the staged patches. "Migrated" here means *re-decomposed +
compiled + parity-green + boundary-certified + assail-clean + staged*.

Each kernel is the pure-integer *brain* of an idaptik `shared/src/*.res`
module: the host (JS/Pixi/) keeps the strings, floats, DOM, network
and mutable service state (the *senses*); AffineScript owns the integer
arithmetic and crosses the wasm boundary in primitives. See
`../../nextgen-evangelist/affine-parity/README.adoc` for the scalar-i32 ABI.
====

toc::[]

== What landed

Cluster C1 = the eleven `shared/src/*.res` leaf files. Eight have a
pure-integer brain and are delivered here; three are host-side "senses" with no
brain to extract (see `EVIDENCE.adoc` § Host-side files).

[cols="2,3,2",options="header"]
|===
| Kernel | Brain (what crosses the boundary) | Source `shared/src/*.res`
| `DeviceType`     | 12-device taxonomy: count, validity, code-clamp (lossless, -1 sentinel) | `DeviceType.res`
| `PuzzleFormat`   | difficulty(4)/tier(5) encodings + DLCLoader's clamp-to-default | `PuzzleFormat.res` (+ `DLCLoader.res`)
| `PortNames`      | 10 coprocessor-domain port taxonomy = portnames.wasm | `PortNames.res` (bound by `PortNamesCoprocessor.res`)
| `GameEvent`      | alertLevel(4, ordered clamp) + direction(6, flat) | `GameEvent.res`
| `Kernel_Compute` | per-domain element caps + the 504/413/404/0 scheduler gate | `Kernel_Compute.res`
| `Kernel`         | the 503/404/0 pre-flight gate + domain→handler router | `Kernel.res`
| `RetryPolicy`    | the 503/504/429 transient classifier + 3-policy config table | `RetryPolicy.res`
| `Diagnostics`    | the <70/<90/≥90 health-band classifier + registry sanity check | `Diagnostics.res`
|===

Verification status: *all four gates green* — 8/8 compile, 1223/1223 parity,
6 echo-boundary proofs (agda exit 0), 8/8 assail-clean. Captured in
`EVIDENCE.adoc`.

== What landed (C2 wave 1 — the reversible VM)

Cluster C2 = the 31 `vm/lib/ocaml` instruction-set files. Wave 1 delivers the
*reversible value-transform opcodes* + the opcode taxonomy as four kernels. The
VM stores state in a `dict<int>` keyed by register NAME with each instruction a
pair of `execute`/`invert` closures; we keep the names + dict host-side and make
the brain the reversible scalar-int value transform per opcode. The defining
invariant — `invert` undoes `execute` — is pinned as `*_roundtrip` exports
(oracle = identity) and swept in Gate 2.

[cols="2,3,2",options="header"]
|===
| Kernel | Brain (reversible value transforms) | Source `vm/lib/ocaml/*.res`
| `VmArith`       | ADD/SUB (inverse pair), NEGATE/NOOP/SWAP (self-inverse) | `Add,Sub,Negate,Noop,Swap`
| `VmBitwise`     | FLIP/XOR (self-inverse), ROL/ROR (inverse pair, 32-bit) | `Flip,Xor,Rol,Ror`
| `VmAncilla`     | AND/OR via Bennett's ancilla (reversible iff c==0) | `And,Or`
| `VmInstruction` | 23-opcode instruction-set encoding + tier classifier | `Instruction`
|===

Verification status: *all four gates green* — 4/4 compile, 2100/2100 parity
(every reversibility round-trip included), 1 echo-boundary proof (LOSSLESS
23-opcode encoding, agda exit 0), 4/4 assail-clean. Captured in
`EVIDENCE-C2.adoc`, which also records three AffineScript backend facts this
cluster is written around (the unary-`~` codegen bug; arithmetic `>>` with no
`>>>`; correct i32 `<<`/wrap). Wave 2 (Mul/Div, stack/memory/control opcodes,
the structural VM files) needs an array/linear-memory ABI — deferred.

== Layout (per kernel)

----
<Name>/
  <Name>.affine            re-decomposed pure-integer kernel (the deliverable)
  <name>.config.mjs        affine-parity oracle config (gate 2)
  <Name>Boundary.agda      generated echo-boundary proof, where applicable (gate 3)
----

Compiled `*.wasm` is build output (regenerated by every parity run) and is
git-ignored; see `.gitignore`.

== Re-running the gates

From this directory, with the prebuilt compiler at
`/home/user/affinescript/_build/default/bin/main.exe`, Deno, and (for gate 3)
Agda + the echo mirror at `/tmp/mirror-boundary`:

[source,console]
----
# Gate 1 — compile
C=/home/user/affinescript/_build/default/bin/main.exe
$C compile DeviceType/DeviceType.affine -o DeviceType/DeviceType.wasm

# Gate 2 — parity (recompiles, then sweeps every export vs its oracle)
P=../../nextgen-evangelist/affine-parity/parity.mjs
deno run --allow-read --allow-run $P DeviceType/devicetype.config.mjs

# Gate 3 — echo-boundary (Agda-certify an encoding table)
B=../../nextgen-evangelist/echo-boundary/boundary.mjs
deno run --allow-read --allow-write --allow-run --allow-env $B \
  --name DeviceTypeBoundary --out DeviceType/DeviceTypeBoundary.agda \
  '{"Laptop":0,"Desktop":1,"Server":2,"Router":3,"Switch":4,"Firewall":5,"Camera":6,"AccessPoint":7,"PatchPanel":8,"PowerSupply":9,"PhoneSystem":10,"FibreHub":11}'

# Gate 4 — assail (weak-point scan; exit 1 on any undeclared clamp)
A=../../nextgen-evangelist/affine-assail/assail.mjs
deno run --allow-read $A DeviceType/DeviceType.affine
----

The per-kernel config names are `devicetype`, `puzzleformat`, `portnames`,
`gameevent`, `kernel_compute`, `kernel`, `retrypolicy`, `diagnostics`.

== The re-decomposition (not a transliteration)

Per the migration playbook these are re-decompositions, not 1:1 ports:

* *Promise/async collapsed.* `Kernel.execute` / `Kernel_Compute.handleCompute`
  return `promise<executionResult>`; the brain keeps only the synchronous status
  *decision*, leaving the await + dispatch host-side.
* *Service-locator state threaded as parameters.* `ResourceAccounting`
  device-state reads and the backend-registry lookup become explicit integer
  args (`active_calls`, `has_backend`, `has_capacity`) — no module-level mutable
  state crosses the boundary.
* *Variants re-encoded as closed integer bands.* device type, difficulty, tier,
  alert level, direction, domain — "the integer IS the X"; the strings stay in
  the host.
* *Floats kept in the senses.* `Diagnostics.healthOf` takes a floored integer
  percentage; `RetryPolicy`'s float backoff factor crosses as a percent (×100).
  Wall-clock timing (`setTimeout`) stays host-side — per the determinism model,
  timing is a sense, not a brain.

== Applying (later, gated)

When idaptik is opened for writes (Phase Ω), each `<Name>.affine` compiles to
`public/assets/wasm/<name>.wasm`, the host `*Coprocessor.res` bridge is wired to
it behind a `FeaturePacks` flag, and the corresponding `shared/src/*.res`
integer logic is retired. `PortNames` is the immediate candidate — its bridge
(`PortNamesCoprocessor.res`) already exists and references `portnames.wasm`.
