migration D (C2 wave 1): reversible VM opcodes (4 kernels, 4-gate green)

proposals/MIGRATION-PLAN.adoc

@@ -189,7 +189,8 @@ Heuristic:
 | 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.
+| D (C2 wave 1) | DONE | Deep wave 2 (2026-06-05, Opus). Cluster C2 *wave 1* — the reversible VM value-transform opcodes — re-decomposed into *4 kernels* under `proposals/idaptik/migrated/` (VmArith, VmBitwise, VmAncilla, VmInstruction), covering 11 opcodes (Add/Sub/Negate/Noop/Swap/Flip/Xor/Rol/Ror/And/Or) + the 23-opcode taxonomy. Brain = the reversible scalar-int value transform per opcode; the register-name dict stays host-side. *Reversibility (`invert∘execute = id`) pinned as `*_roundtrip` exports.* *Four gates green:* 4/4 compile, 2100/2100 parity (incl. every round-trip, over i32 extremes), 1 echo-boundary LOSSLESS (23-opcode encoding, agda exit 0), 4/4 assail-clean. Evidence: `migrated/EVIDENCE-C2.adoc`. Surfaced 3 compiler facts: unary `~` codegen bug (workaround `-a-1`), arithmetic `>>` + no `>>>` (logical-shift-right emulated). NEXT: C2 wave 2.
+| C2b+ | TODO | C2 wave 2 (needs an array/linear-memory ABI): Mul/Div, the stack/memory opcodes (Push/Pop/Load/Store), control flow (Call/Loop/IfPos/IfZero), I/O (Send/Recv/CoprocessorCall), and the structural VM files (State, VM, SubroutineRegistry, *Coprocessor, bindings). Then C3..C12. The unary-`~` codegen bug is a candidate Phase-F compiler fix.
 | F+ | TODO | Compiler walls (string backend, then effects).
 | Ω | TODO (access-gated) | Cutover + ReScript extinction.
 |===

proposals/idaptik/migrated/EVIDENCE-C2.adoc

@@ -0,0 +1,128 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Cluster C2 (wave 1) — reversible-VM four-gate evidence (captured 2026-06-05)
+:toc: macro
+
+[IMPORTANT]
+====
+*Captured run of the 4-gate recipe over the cluster-C2 wave-1 kernels — the
+unconditionally- and conditionally-reversible value-transform opcodes of the
+idaptik VM, plus the opcode taxonomy.* The defining C2 invariant is
+*reversibility*: every opcode's `invert` undoes its `execute`. This is pinned
+directly as `*_roundtrip` exports whose oracle is the identity. 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
+| `VmArith`       | OK | 846/846  | (transforms) | clean
+| `VmBitwise`     | OK | 572/572  | (transforms) | clean
+| `VmAncilla`     | OK | 401/401  | (transforms) | clean
+| `VmInstruction` | OK | 281/281  | LOSSLESS (23) | clean
+| *Total*         | *4/4* | *2100/2100* | *1 proof, agda exit 0* | *4/4 clean*
+|===
+
+Opcodes delivered this wave (11 + the taxonomy): ADD, SUB, NEGATE, NOOP, SWAP
+(`VmArith`); FLIP, XOR, ROL, ROR (`VmBitwise`); AND, OR (`VmAncilla`); the
+23-opcode instruction-set encoding + tier classifier (`VmInstruction`).
+
+== The reversibility gate (what makes C2 different from C1)
+
+Each opcode is migrated as the scalar-int *value transform* the ReScript
+`execute` / `invert` closures perform on a register; the register-name strings
+and the `dict<int>` stay host-side. The reversibility law is pinned as explicit
+round-trip exports and swept in Gate 2 with the identity (or 0) as oracle:
+
+[cols="2,3,1",options="header"]
+|===
+| Opcode(s) | Round-trip law (verified over i32 incl. extremes) | Kind
+| ADD / SUB | `inv(fwd(a,b),b) == a` (holds under two's-complement wrap) | inverse pair
+| NEGATE / NOOP / SWAP | `op(op(x)) == x` | self-inverse
+| FLIP / XOR | `op(op(x)) == x` | self-inverse
+| ROL / ROR | `ror(rol(a,bits),bits) == a` over full i32 | inverse pair
+| AND / OR | ancilla `0 -> a∘b -> 0` (Bennett, precondition c==0) | conditional
+|===
+
+AND/OR are the honest outlier: reversible *only* via Bennett's ancilla trick and
+*only* under the precondition that the ancilla register starts at 0 — a declared
+precondition, documented in `VmAncilla.affine`. Every other opcode here is
+unconditionally reversible.
+
+== Compiler facts this cluster is written around
+
+Migrating the bitwise opcodes surfaced three AffineScript backend facts. None
+blocked the migration — each has a sound in-language workaround — but they are
+recorded here as findings (the first is a genuine codegen bug worth a Phase-F
+fix).
+
+. *Unary `~` mis-compiles (BUG).* `pub fn f(a) { ~a }` compiles but the wasm
+  fails to instantiate: `i32.xor (need 2, got 1)` — the codegen emits an
+  `i32.xor` without pushing the second operand. Isolated to the unary `~`
+  operator only; binary `&` `|` `^` are all sound. *Workaround:* FLIP uses the
+  two's-complement identity `~a == -a - 1` (verified equal to JS `~a` over the
+  i32 sample, and self-inverse: `~(~a) = a`).
+. *`>>` is arithmetic; `>>>` does not exist.* `-1 >> 1 == -1` (sign-propagating),
+  and `a >>> n` is a parse error. The ReScript ROL/ROR use a *logical* shift
+  right, so a naive `(a<<b)|(a>>(32-b))` rotation fails to round-trip for
+  high-bit values. *Workaround:* emulate logical shift right as
+  `lsr(a,n) = (a >> n) & ((1 << (32 - n)) - 1)` (clears the n sign-extended
+  bits). With it, ROL/ROR match JS `((a<<n)|(a>>>(32-n)))|0` and round-trip over
+  the full i32 range (checked at `0x55555555` / `0xAAAAAAAA` and the extremes).
+. *`<<` and i32 wrap are correct.* `1 << 31 == -2147483648`; `&` `|` `^` `-a`
+  all behave as i32 two's-complement, which is exactly the VM's word model.
+
+== Gate 1 — compile
+
+----
+[OK] VmArith   [OK] VmBitwise   [OK] VmAncilla   [OK] VmInstruction
+----
+
+== Gate 2 — parity (oracle-vs-wasm, scalar i32 ABI)
+
+2100 inputs, 0 mismatches. Oracles re-derive every transform independently
+(JS native bitwise incl. the logical `>>>` the kernel emulates) plus the
+reversibility round-trips (oracle = identity, or 0 for the ancilla).
+
+----
+VmArith ......... 846/846     VmAncilla ....... 401/401
+VmBitwise ....... 572/572     VmInstruction ... 281/281
+----
+
+== Gate 3 — echo-boundary
+
+`VmInstructionBoundary` — the 23-opcode instruction-set encoding (NOOP=0 ..
+RECV=22) certified LOSSLESS (`agda exit 0`): 23 instructions → 23 distinct
+opcodes, so the host round-trips instruction ↔ opcode with no collision. The
+value-transform kernels (`VmArith`/`VmBitwise`/`VmAncilla`) are reversible
+*transforms*, not encodings, so echo-boundary's injectivity lens does not apply;
+their faithfulness is the Gate-2 round-trip.
+
+== Gate 4 — affine-assail
+
+----
+[CLEAN] VmArith   [CLEAN] VmBitwise   [CLEAN] VmAncilla   [CLEAN] VmInstruction
+----
+
+All clamps are guard-style sentinels (`-1` for out-of-band opcodes/tiers, which
+are outside the in-band range — not in-band collapses), so no `PA-AFF-001`.
+
+== Remaining in cluster C2 (wave 2)
+
+This wave migrated the value-transform opcodes (no stack/memory/control state
+crosses the boundary as a scalar). The rest of C2 needs an array/linear-memory
+ABI and a control-flow model, deferred to wave 2:
+
+* *Arithmetic with structure:* `Mul`, `Div` (reversibility needs the operand
+  kept + the remainder, respectively — richer than the inverse-pair shape here).
+* *Stack / memory:* `Push`, `Pop`, `Load`, `Store` (operate on `_sp` / `_mem:N`
+  dict keys — need the array/memory ABI).
+* *Control flow:* `Call`, `Loop`, `IfPos`, `IfZero` (sequences + branch state).
+* *I/O channels:* `Send`, `Recv`, `CoprocessorCall` (port buffers).
+* *Structural:* `State`, `VM`, `SubroutineRegistry`, the `*Coprocessor`
+  wrappers, and the `vm/wasm/src/bindings` shim (the host-side glue).

proposals/idaptik/migrated/README.adoc

@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: AGPL-3.0-or-later
 // SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= idaptik migration — staged kernels (Phase C, cluster C1)
+= idaptik migration — staged kernels (Phase C cluster C1, Phase D cluster C2)
 :toc: macro
 
 [IMPORTANT]
@@ -43,6 +43,33 @@ 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)
 
 ----

proposals/idaptik/migrated/VmAncilla/VmAncilla.affine

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+//
+// VmAncilla -- the CONDITIONALLY-reversible bitwise opcodes of the idaptik VM,
+// the pure-integer core extracted from vm/lib/ocaml/{And,Or}.res. Unlike the
+// VmArith / VmBitwise opcodes (unconditionally reversible), AND and OR are
+// reversible only via Bennett's ancilla trick, and only under a PRECONDITION.
+// This distinction is the interesting semantic content of this kernel.
+//
+//## The Bennett ancilla protocol (registers a, b, ancilla c)
+//   execute  c := a & b   (resp. a | b)      -- write the result into c
+//   invert   c := 0                          -- clear c back to zero
+// This is reversible ONLY when c == 0 before execute: then the pair restores c
+// to its original value (0). If c != 0 beforehand, invert does NOT restore it --
+// the trick has a declared precondition, exactly like a declared clamp. The
+// reversibility is on the ANCILLA round-trip:  0 --execute--> a∘b --invert--> 0.
+//
+// a & b and a | b are themselves many-to-one (lossy as maps from (a,b)); they
+// are made reversible only by keeping a and b live and storing the result in a
+// fresh zeroed ancilla. We expose the forward computation and the inverse clear
+// separately, and pin the ancilla round-trip (oracle = 0).
+
+// --- forward: the value written into the zeroed ancilla c ---
+pub fn and_compute(a: Int, b: Int) -> Int { a & b }
+pub fn or_compute(a: Int, b: Int) -> Int { a | b }
+
+// --- invert: clear the ancilla back to zero (independent of a, b) ---
+pub fn ancilla_clear() -> Int { 0 }
+
+// --- ancilla round-trip under the precondition c0 == 0:
+//     start at 0, execute writes a∘b, invert clears to 0. Result == 0. ---
+pub fn and_ancilla_roundtrip(a: Int, b: Int) -> Int {
+  let _written = and_compute(a, b);
+  ancilla_clear()
+}                                                                   // == 0
+pub fn or_ancilla_roundtrip(a: Int, b: Int) -> Int {
+  let _written = or_compute(a, b);
+  ancilla_clear()
+}                                                                   // == 0

proposals/idaptik/migrated/VmAncilla/vmancilla.config.mjs

@@ -0,0 +1,18 @@
+// 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 VmAncilla.affine (Bennett-ancilla AND/OR; scalar i32
+// ABI). Oracles re-derive the forward computations and the ancilla round-trip
+// (which, starting from a zeroed ancilla, returns 0 regardless of a,b).
+const I = { values: [-2147483648, -1000000, -1, 0, 1, 7, 12, 10, 1000000, 2147483647] };
+export default {
+  affine: "VmAncilla.affine",
+  cases: [
+    { name: "and_compute a&b", export: "and_compute", args: [I, I], oracle: (a, b) => (a & b) | 0 },
+    { name: "or_compute a|b", export: "or_compute", args: [I, I], oracle: (a, b) => (a | b) | 0 },
+    { name: "ancilla_clear == 0", export: "ancilla_clear", args: [], oracle: () => 0 },
+    // --- ancilla round-trip (precondition c0==0): 0 -> a∘b -> 0 ---
+    { name: "and_ancilla_roundtrip == 0", export: "and_ancilla_roundtrip", args: [I, I], oracle: (a, b) => 0 },
+    { name: "or_ancilla_roundtrip == 0", export: "or_ancilla_roundtrip", args: [I, I], oracle: (a, b) => 0 },
+  ],
+};

proposals/idaptik/migrated/VmArith/VmArith.affine

@@ -0,0 +1,53 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+//
+// VmArith -- the reversible integer-arithmetic opcodes of the idaptik VM, the
+// pure-integer core extracted from vm/lib/ocaml/{Add,Sub,Negate,Noop,Swap}.res.
+// The ReScript VM stores state in a dict<int> keyed by register NAME and each
+// instruction is a pair of `execute` / `invert` closures over that dict. We
+// re-decompose per the brain/senses split: the register-name strings and the
+// dict live host-side (the senses); the brain is the reversible VALUE transform
+// each opcode performs, as scalar-int functions. "The integer IS the register."
+//
+// The defining invariant of the reversible VM is that every opcode's `invert`
+// undoes its `execute`. We pin that here as explicit *_roundtrip exports whose
+// oracle is the identity -- the headline gate for this cluster.
+//
+//## Opcode value semantics (register a, register b; result is the new a)
+//   ADD     execute a := a + b      invert a := a - b      (inverse pair)
+//   SUB     execute a := a - b      invert a := a + b      (inverse pair)
+//   NEGATE  execute a := -a         invert a := -a         (self-inverse)
+//   NOOP    execute a := a          invert a := a          (identity)
+//   SWAP    execute (a,b):=(b,a)    invert (a,b):=(b,a)    (self-inverse)
+// All identities hold over i32 two's-complement wraparound: (a+b)-b == a even
+// when a+b overflows, because the wrap is consistent in both directions.
+
+// --- ADD: inverse pair ---
+pub fn add_fwd(a: Int, b: Int) -> Int { a + b }
+pub fn add_inv(a: Int, b: Int) -> Int { a - b }
+
+// --- SUB: inverse pair ---
+pub fn sub_fwd(a: Int, b: Int) -> Int { a - b }
+pub fn sub_inv(a: Int, b: Int) -> Int { a + b }
+
+// --- NEGATE: self-inverse ---
+pub fn negate(a: Int) -> Int { -a }
+
+// --- NOOP: identity ---
+pub fn noop(a: Int) -> Int { a }
+
+// --- SWAP: self-inverse; two projections of the (a,b) -> (b,a) transform ---
+pub fn swap_first(a: Int, b: Int) -> Int { b }
+pub fn swap_second(a: Int, b: Int) -> Int { a }
+
+// --- Reversibility round-trips (oracle = identity): invert undoes execute ---
+pub fn add_roundtrip(a: Int, b: Int) -> Int { add_inv(add_fwd(a, b), b) }       // == a
+pub fn sub_roundtrip(a: Int, b: Int) -> Int { sub_inv(sub_fwd(a, b), b) }       // == a
+pub fn negate_roundtrip(a: Int) -> Int { negate(negate(a)) }                    // == a
+pub fn noop_roundtrip(a: Int) -> Int { noop(noop(a)) }                          // == a
+// SWAP twice is identity: re-applying the (b,a) transform to (b,a) gives (a,b).
+pub fn swap_roundtrip_first(a: Int, b: Int) -> Int {
+  swap_first(swap_first(a, b), swap_second(a, b))
+}                                                                                // == a
+pub fn swap_roundtrip_second(a: Int, b: Int) -> Int {
+  swap_second(swap_first(a, b), swap_second(a, b))
+}                                                                                // == b

proposals/idaptik/migrated/VmArith/vmarith.config.mjs

@@ -0,0 +1,28 @@
+// 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 VmArith.affine (reversible VM arithmetic opcodes;
+// scalar i32 ABI). Oracles re-derive each opcode value transform AND the
+// reversibility round-trips (oracle = identity) independently in JS. Results are
+// normalised to i32 (| 0) on both sides, so two's-complement overflow is covered.
+const I = { values: [-2147483648, -1000000, -7, -1, 0, 1, 7, 1000000, 2147483647] };
+export default {
+  affine: "VmArith.affine",
+  cases: [
+    { name: "add_fwd a+b", export: "add_fwd", args: [I, I], oracle: (a, b) => (a + b) | 0 },
+    { name: "add_inv a-b", export: "add_inv", args: [I, I], oracle: (a, b) => (a - b) | 0 },
+    { name: "sub_fwd a-b", export: "sub_fwd", args: [I, I], oracle: (a, b) => (a - b) | 0 },
+    { name: "sub_inv a+b", export: "sub_inv", args: [I, I], oracle: (a, b) => (a + b) | 0 },
+    { name: "negate -a", export: "negate", args: [I], oracle: (a) => (-a) | 0 },
+    { name: "noop a", export: "noop", args: [I], oracle: (a) => a | 0 },
+    { name: "swap_first -> b", export: "swap_first", args: [I, I], oracle: (a, b) => b | 0 },
+    { name: "swap_second -> a", export: "swap_second", args: [I, I], oracle: (a, b) => a | 0 },
+    // --- reversibility: invert undoes execute (oracle = identity) ---
+    { name: "add_roundtrip == a", export: "add_roundtrip", args: [I, I], oracle: (a, b) => a | 0 },
+    { name: "sub_roundtrip == a", export: "sub_roundtrip", args: [I, I], oracle: (a, b) => a | 0 },
+    { name: "negate_roundtrip == a", export: "negate_roundtrip", args: [I], oracle: (a) => a | 0 },
+    { name: "noop_roundtrip == a", export: "noop_roundtrip", args: [I], oracle: (a) => a | 0 },
+    { name: "swap_roundtrip_first == a", export: "swap_roundtrip_first", args: [I, I], oracle: (a, b) => a | 0 },
+    { name: "swap_roundtrip_second == b", export: "swap_roundtrip_second", args: [I, I], oracle: (a, b) => b | 0 },
+  ],
+};