Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion proposals/MIGRATION-PLAN.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,8 @@ Heuristic:
| C6+C8 (fan-out) | DONE | Parallel deep wave (2026-06-05): two Sonnet agents migrated clusters C6 (combat/enemy) + C8 (device/network); parent re-verified + consolidated. *16 kernels* staged under `proposals/idaptik/migrated/` — C6: CombatFx, Detection, DifficultyScale, Distraction, DualAlert, HitboxGeom, PlayerHp, SecurityAi; C8: GlobalNetworkData, NetworkManager, SecurityRank, DeviceCaps, LaptopState, NetworkTransfer, PowerManager, CovertLink. *Four gates green (re-run by parent, not just agent-reported):* 16/16 compile, *34280/34280 parity* (C6 8185 + C8 26095, independent oracles), 7 echo-boundary LOSSLESS proofs, 16/16 assail-clean. Re-verification CAUGHT 3 PA-AFF-001 findings the agent reports missed (SecurityAi, SecurityRank, NetworkManager) — fixed with the established guard-helper clamp declaration; NetworkManager parity held at 2645/2645 after dropping the dead `Cat` enum, confirming semantics preserved. *4th compiler finding:* Float→wasm codegen broadly incomplete (pub-fn exports always type i32; float-literal operands mis-emit; `trunc()`/`float()` absent) — drives the `*Int.affine` parity subsets, keeps floats host-side. Evidence: `migrated/EVIDENCE-C6.adoc` + `EVIDENCE-C8.adoc`. NEXT: complete C7, then C2 wave 2.
| C7 | DONE | Player cluster complete (2026-06-05): two scoped agents (5 verify + 3 float-re-decompose) + parent re-verification. *8 kernels* — CriticalRoll, PlayerAttributes, QCertifications, SkillRank, SkillAbilities, QPrograms, JessicaLoadout, JessicaBackground. *Four gates green (every gate re-run by parent):* 8/8 compile, *4348/4348 parity* (independent oracles), *6 echo-boundary LOSSLESS proofs* across 4 kernels (QCertifications, SkillRank, JessicaLoadout×3, JessicaBackground — agda re-typechecked by parent, exit 0); the other 4 transform/classifier kernels G3-n/a, 8/8 assail-clean. 3 kernels (CriticalRoll/PlayerAttributes/QPrograms) hit the Float→wasm wall (`min_float`/`max_float`/`trunc`) and were re-decomposed Int-native (milli-unit convention, floats host-side) per the C6 `*Int` pattern; parity caught + fixed an off-by-100 in PlayerAttributes. Evidence: `migrated/EVIDENCE-C7.adoc`. NEXT: C2 wave 2.
| C2 wave 2a | DONE | Scalar multiply/divide (2026-06-05, Opus). `Mul`/`Div` turned out to be pure *scalar* value-transforms (not memory ops), so they need *no* array ABI — split out of "wave 2" and landed now. *1 kernel* `VmMulDiv` (11 exports) under `proposals/idaptik/migrated/`. Brain = the reversible ancilla multiply (`c := c + a*b`, inverse `c := c - a*b`) + the quotient/remainder divide whose dividend is reconstructable (`q*b + r == a` for all b incl. 0); the intentional-flaw in-place/simple variants migrated as value transforms with no rt==id claim. *Four gates green:* 1/1 compile, *3322/3322 parity* (incl. mul reversibility roundtrip + div reconstruction), G3 n/a (numeric transform), 1/1 assail-clean. *2 new i32 ABI facts:* (a) JS `a*b` loses precision >2^53 → oracle must use `Math.imul` to match `i32.mul`; (b) `i32.div_s` TRAPS on `b==0` and `INT_MIN/-1` (ReScript wraps the latter) → brain guards both (nested-`if`, avoiding the unverified `&&` codegen path) so the wasm is total. Evidence: `migrated/EVIDENCE-C2-wave2a.adoc`. NEXT: C2 wave 2b.
| C2 wave 2b | TODO | The memory/control opcodes (Push/Pop/Load/Store, Call/Loop/IfPos/IfZero, Recv/Send/CoprocessorCall/InstructionCoprocessor) + structural VM files (State, VM, SubroutineRegistry, VmStateCoprocessor, bindings). *Genuinely needs an array/linear-memory ABI* (`[len:i32 LE][bytes]` + `__affine_alloc`) — the next real unblocker, also feeds the string wall. Opus-level ABI design. Then C3..C12. The unary-`~` codegen bug is a candidate Phase-F compiler fix.
| C2 wave 2b | DONE | Memory/stack/port/control opcodes (2026-06-05, Opus). *The "needs an array/linear-memory ABI" premise was WRONG and re-decomposition overturned it:* reading the sources, the VM's memory/stack/port buffers are not arrays in the brain — `VmState.res` stores every one as string-keyed dict slots (`_mem:N`, `_s:N`, `_pin:port`), i.e. host-side STATE (senses). The integer brains are all scalar. *4 kernels* `VmMemory` (LOAD/STORE), `VmStack` (PUSH/POP), `VmPort` (RECV/SEND), `VmControl` (IF_POS/IF_ZERO/LOOP) covering *9 opcodes*. *Four gates green:* 4/4 compile, *1568/1568 parity* (incl. load/store/sp/recv/send round-trips), G3 n/a (transforms/predicates), 4/4 assail-clean. No-kernel senses (classified, not migrated): Call (orchestration), CoprocessorCall (tombstone — never implemented), State/VmState/VM/SubroutineRegistry/VmStateCoprocessor/InstructionCoprocessor (state containers / bridges). Evidence: `migrated/EVIDENCE-C2-wave2b.adoc`. *No array ABI was required* (the blocker was a triage-bucket artefact). *Cluster C2 COMPLETE.* NEXT: C3.
| C3..C12 | TODO | Remaining MIGRATABLE-NOW clusters per `migration-map.json`: C3 (17), C5 (11), C9 (16), C10 (21), C11 (10), C12 (43). Established scalar/enum/predicate recipe. The unary-`~` codegen bug is a candidate Phase-F compiler fix; the string wall (52 non-test .res) + effect wall (110) remain the genuine compiler gates for the STRING-/EFFECT-GATED kernels.
| F+ | TODO | Compiler walls (string backend, then effects).
| Ω | TODO (access-gated) | Cutover + ReScript extinction.
|===
Expand Down
103 changes: 103 additions & 0 deletions proposals/idaptik/migrated/EVIDENCE-C2-wave2b.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,103 @@
// 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 2b (VM memory / stack / port / control) — four-gate evidence (captured 2026-06-05)
:toc: macro

[IMPORTANT]
====
*The ledger's premise for this wave was wrong, and re-decomposition overturned
it.* Wave 2b was scoped as "needs an array/linear-memory ABI." Reading the
actual opcode sources shows the VM's memory, stack, and port buffers are NOT
arrays in the brain — `VmState.res` stores every one of them as *string-keyed
dict entries* (`_mem:0`, `_s:0`, `_pin:port`, ...). That dict is host-side STATE
(the senses). The pure-integer brains are all SCALAR: additive value transforms,
pointer arithmetic, and branch predicates. So wave 2b needs *no* array ABI —
it is the established scalar recipe. Toolchain: AffineScript compiler
`_build/default/bin/main.exe`, Deno 2.8.2.
====

toc::[]

== Summary

[cols="2,2,1,1,2,1",options="header"]
|===
| Kernel | Opcodes | G1 | G2 parity | G3 | G4 assail
| `VmMemory` | LOAD, STORE | OK | 486/486 | n/a (transform) | clean
| `VmStack` | PUSH, POP | OK | 28/28 | n/a (transform) | clean
| `VmPort` | RECV, SEND | OK | 298/298 | n/a (transform) | clean
| `VmControl` | IF_POS, IF_ZERO, LOOP | OK | 756/756 | n/a (predicate) | clean
| *Total* | *9 opcodes* | *4/4* | *1568/1568* | *n/a* | *4/4 clean*
|===

== The re-decomposition that dissolved the array-ABI blocker

Each opcode manipulates host-side state, but the integer brain is scalar:

[cols="1,3,2",options="header"]
|===
| Opcode | Source semantics | Scalar brain (the wasm)
| LOAD | `reg += memory[addr]` / `reg -= memory[addr]` | additive `reg ± mem` (host supplies `mem`)
| STORE | `memory[addr] += reg` / `-= reg` | additive `mem ± reg`
| PUSH | `stack[sp]:=reg; sp++; reg:=0` | pointer `sp+1`, register clear `0`
| POP | `sp--; reg:=stack[sp]; stack[sp]:=0` | pointer `sp-1`
| RECV | `reg += port_in[ptr]; ptr++` | additive `reg ± val`, pointer `ptr±1`
| SEND | `port_out[ptr]:=reg; ptr++` (inv writes 0) | pointer `ptr±1`, slot clear `0`
| IF_POS | run then/else by `testReg > 0` | predicate `v > 0 -> 1/0`
| IF_ZERO| run then/else by `testReg == 0` | predicate `v == 0 -> 1/0`
| LOOP | `while exitReg != 0 && iters < max` | continuation predicate + `iters+1`
|===

The arrays (`stack`, `memory`, port buffers) and the register dict are the
*senses* — host-owned `VmState` dict slots. The host performs every array
get/set; the wasm computes only the next pointer, the accumulated value, or the
branch decision. "The integer IS the register / pointer / predicate."

*Reversibility is migrated as explicit round-trip exports* (the headline gate):
`load_roundtrip == reg`, `store_roundtrip == mem`, `sp_roundtrip == sp`,
`recv_acc_roundtrip == reg`, `recv_ptr_roundtrip == ptr`,
`send_ptr_roundtrip == ptr`. IF_POS/IF_ZERO/LOOP carry no value round-trip —
their Janus reversibility is host orchestration (the reverse run applies the
same predicate to the *exit* register and runs the chosen branch reversed); the
brain is the shared predicate.

== No-kernel files (host-side senses, faithfully classified — not migrated)

[cols="2,3",options="header"]
|===
| File | Why no integer brain
| `Call.res` | Pure orchestration: runs the body instructions forward / reversed-and-inverted. No value transform.
| `CoprocessorCall.res` | *Tombstone* — never implemented; superseded by terminal SEND/RECV + VM Tier-4 Send/Recv (see the file's own header). Nothing to migrate.
| `State.res`, `VmState.res` | The state container itself (the senses): `dict<int>` slot accessors + serialise (string-gated). No brain.
| `SubroutineRegistry.res` | name -> `array<Instruction.t>` registry; orchestration container.
| `VmStateCoprocessor.res`, `InstructionCoprocessor.res` | Coprocessor bridges — host-side dispatch; the integer cores they call are the already-migrated opcode brains.
| `VM.res` | Top-level interpreter loop: sequences opcode execute/invert over the state dict. Orchestration; the per-opcode brains are migrated here + in waves 1/2a.
|===

== Gate detail

* *G1 compile* — `main.exe compile <k>.affine -o <k>.wasm` → WASM for all 4
(VmMemory 346 B, VmStack 243 B, VmPort 508 B, VmControl 299 B).
* *G2 parity* — `parity.mjs <k>.config.mjs` → 1568/1568 over the i32 domain
`{INT_MIN, -1e6, -7, -1, 0, 1, 7, 1e6, INT_MAX}` (Cartesian per arity). Each
oracle independently re-derives the original `.res` value transform.
* *G3 boundary* — n/a for all 4. These are numeric transforms / branch
predicates with no discrete value↔integer encoding table; the G2 round-trip
against the independent oracle is the faithfulness check (same disposition as
the wave-1/2a value-transform kernels).
* *G4 assail* — 0 findings across all 4. Predicates use boolean fall-through
(`if cond { 1 } else { 0 }`) and the LOOP guard uses an out-of-band `return 0`
on the `exit_val == 0` early exit; there is no enum decoder, so PA-AFF-001
does not apply.

== Cluster C2 — COMPLETE

With wave 1 (Add/Sub/Negate/Noop/Swap/Flip/Xor/Rol/Ror/And/Or + Instruction
taxonomy), wave 2a (Mul/Div), and wave 2b (Load/Store/Push/Pop/Recv/Send/IfPos/
IfZero/Loop), every reversible-VM opcode with a separable integer brain is
migrated and four-gate verified. The remaining C2 files (Call, CoprocessorCall,
State, VmState, VM, SubroutineRegistry, VmStateCoprocessor, InstructionCoprocessor)
are host-side senses / orchestration with no integer brain, classified above.
*No array/linear-memory ABI was required* — that blocker was an artefact of the
coarse triage bucket, dissolved by reading the sources. (The string wall remains
a separate, genuine compiler gate for the STRING-GATED clusters.)
27 changes: 27 additions & 0 deletions proposals/idaptik/migrated/VmControl/VmControl.affine
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
// SPDX-License-Identifier: AGPL-3.0-or-later
//
// VmControl -- the control-flow opcodes IF_POS/IF_ZERO/LOOP of the idaptik VM,
// the pure-integer core from vm/lib/ocaml/{IfPos,IfZero,Loop}.res. The branch
// bodies are arrays of sub-instructions run by the host orchestrator (the
// senses); the brain is only the scalar BRANCH PREDICATE that selects a branch
// (and, for LOOP, the iteration counter + bound check). Janus reversibility
// lives in the host: the reverse run applies the SAME predicate to the exit
// register instead of the test register, then runs the chosen branch reversed.
//
// IF_POS take then-branch iff testReg > 0 (reverse: iff exitReg > 0)
// IF_ZERO take then-branch iff testReg == 0 (reverse: iff exitReg == 0)
// LOOP continue iff exitReg != 0 and iterations < maxIterations
// Predicates return 1 (take / continue) or 0 (skip / stop).

// --- IF_POS / IF_ZERO branch predicates (1 = then-branch, 0 = else-branch) ---
pub fn if_pos(v: Int) -> Int { if v > 0 { 1 } else { 0 } }
pub fn if_zero(v: Int) -> Int { if v == 0 { 1 } else { 0 } }

// --- LOOP continuation: 1 = run another iteration, 0 = stop ---
// Continue while the exit register is non-zero AND the iteration cap is unhit.
pub fn loop_continue(exit_val: Int, iters: Int, max_iters: Int) -> Int {
if exit_val == 0 { return 0; }
if iters < max_iters { 1 } else { 0 }
}
// Iteration counter advance (the maxIterations guard counts these).
pub fn loop_iter_next(iters: Int) -> Int { iters + 1 }
19 changes: 19 additions & 0 deletions proposals/idaptik/migrated/VmControl/vmcontrol.config.mjs
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// 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 VmControl.affine (IF_POS/IF_ZERO/LOOP branch
// predicates; scalar i32 ABI). Oracles re-derive vm/lib/ocaml/{IfPos,IfZero,
// Loop}.res predicates. The branch bodies are host-orchestrated; only the
// scalar predicate (1 = take/continue, 0 = skip/stop) crosses the boundary.
const I = { values: [-2147483648, -1000000, -7, -1, 0, 1, 7, 1000000, 2147483647] };
const i32 = (x) => x | 0;

export default {
affine: "VmControl.affine",
cases: [
{ name: "if_pos v>0 -> 1/0", export: "if_pos", args: [I], oracle: (v) => (v > 0 ? 1 : 0) },
{ name: "if_zero v==0 -> 1/0", export: "if_zero", args: [I], oracle: (v) => (v === 0 ? 1 : 0) },
{ name: "loop_continue exit!=0 && iters<max", export: "loop_continue", args: [I, I, I], oracle: (e, i, m) => (e === 0 ? 0 : (i < m ? 1 : 0)) },
{ name: "loop_iter_next iters+1", export: "loop_iter_next", args: [I], oracle: (i) => i32(i + 1) },
],
};
23 changes: 23 additions & 0 deletions proposals/idaptik/migrated/VmMemory/VmMemory.affine
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
// SPDX-License-Identifier: AGPL-3.0-or-later
//
// VmMemory -- the additive memory opcodes LOAD/STORE of the idaptik VM, the
// pure-integer core extracted from vm/lib/ocaml/{Load,Store}.res. The VM's
// "memory" is NOT an array in the brain: VmState stores it as string-keyed dict
// entries (`_mem:0`, `_mem:1`, ... 256 slots), so that dict is host-side STATE
// (the senses). The host reads/writes memory[addr]; the brain is only the
// reversible ADDITIVE value transform -- LOAD/STORE therefore need no array ABI.
//
// LOAD execute reg := reg + memory[addr] invert reg := reg - memory[addr]
// STORE execute memory[addr] := memory[addr] + reg invert ... - reg
// Both are additive (non-destructive): the inverse subtracts, so the round-trip
// is exact over i32 wraparound -- the same reason ADD/SUB round-trip.

// --- LOAD: additive load (host supplies memory[addr] as `mem`) ---
pub fn load_fwd(reg: Int, mem: Int) -> Int { reg + mem }
pub fn load_inv(reg: Int, mem: Int) -> Int { reg - mem }
pub fn load_roundtrip(reg: Int, mem: Int) -> Int { load_inv(load_fwd(reg, mem), mem) } // == reg

// --- STORE: additive store (host supplies memory[addr] as `mem`) ---
pub fn store_fwd(mem: Int, reg: Int) -> Int { mem + reg }
pub fn store_inv(mem: Int, reg: Int) -> Int { mem - reg }
pub fn store_roundtrip(mem: Int, reg: Int) -> Int { store_inv(store_fwd(mem, reg), reg) } // == mem
21 changes: 21 additions & 0 deletions proposals/idaptik/migrated/VmMemory/vmmemory.config.mjs
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
// 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 VmMemory.affine (additive LOAD/STORE; scalar i32
// ABI). Oracles re-derive vm/lib/ocaml/{Load,Store}.res value transforms
// independently. The memory array is host-side; only the additive value
// transform crosses the boundary. Both sides normalise to i32 (| 0).
const I = { values: [-2147483648, -1000000, -7, -1, 0, 1, 7, 1000000, 2147483647] };
const i32 = (x) => x | 0;

export default {
affine: "VmMemory.affine",
cases: [
{ name: "load_fwd reg+mem", export: "load_fwd", args: [I, I], oracle: (reg, mem) => i32(reg + mem) },
{ name: "load_inv reg-mem", export: "load_inv", args: [I, I], oracle: (reg, mem) => i32(reg - mem) },
{ name: "load_roundtrip == reg", export: "load_roundtrip", args: [I, I], oracle: (reg, mem) => i32(reg) },
{ name: "store_fwd mem+reg", export: "store_fwd", args: [I, I], oracle: (mem, reg) => i32(mem + reg) },
{ name: "store_inv mem-reg", export: "store_inv", args: [I, I], oracle: (mem, reg) => i32(mem - reg) },
{ name: "store_roundtrip == mem", export: "store_roundtrip", args: [I, I], oracle: (mem, reg) => i32(mem) },
],
};
26 changes: 26 additions & 0 deletions proposals/idaptik/migrated/VmPort/VmPort.affine
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
// SPDX-License-Identifier: AGPL-3.0-or-later
//
// VmPort -- the I/O port opcodes RECV/SEND of the idaptik VM, the pure-integer
// core from vm/lib/ocaml/{Recv,Send}.res. The port buffers (`_pin:port`,
// `_pout:port` slots + pointers) are host-side state (the senses); the host
// reads/writes the buffer slot. The brain is the port-POINTER arithmetic plus,
// for RECV, the additive accumulate of the received value -- no array ABI.
//
// RECV execute reg := reg + port_in[ptr]; ptr := ptr + 1
// invert ptr := ptr - 1; reg := reg - port_in[ptr]
// SEND execute port_out[ptr] := reg; ptr := ptr + 1
// invert ptr := ptr - 1; port_out[ptr] := 0

// --- RECV: additive accumulate + input-pointer advance ---
pub fn recv_acc_fwd(reg: Int, val: Int) -> Int { reg + val }
pub fn recv_acc_inv(reg: Int, val: Int) -> Int { reg - val }
pub fn recv_acc_roundtrip(reg: Int, val: Int) -> Int { recv_acc_inv(recv_acc_fwd(reg, val), val) } // == reg
pub fn recv_ptr_fwd(ptr: Int) -> Int { ptr + 1 }
pub fn recv_ptr_inv(ptr: Int) -> Int { ptr - 1 }
pub fn recv_ptr_roundtrip(ptr: Int) -> Int { recv_ptr_inv(recv_ptr_fwd(ptr)) } // == ptr

// --- SEND: output-pointer advance; inverse clears the vacated slot to 0 ---
pub fn send_ptr_fwd(ptr: Int) -> Int { ptr + 1 }
pub fn send_ptr_inv(ptr: Int) -> Int { ptr - 1 }
pub fn send_ptr_roundtrip(ptr: Int) -> Int { send_ptr_inv(send_ptr_fwd(ptr)) } // == ptr
pub fn send_clears_slot() -> Int { 0 }
25 changes: 25 additions & 0 deletions proposals/idaptik/migrated/VmPort/vmport.config.mjs
Original file line number Diff line number Diff line change
@@ -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 VmPort.affine (RECV/SEND port pointer + additive
// accumulate; scalar i32 ABI). Oracles re-derive vm/lib/ocaml/{Recv,Send}.res.
// The port buffers + pointers are host-side state; only the pointer arithmetic
// and the additive accumulate cross the boundary. Both sides normalise to i32.
const I = { values: [-2147483648, -1000000, -7, -1, 0, 1, 7, 1000000, 2147483647] };
const i32 = (x) => x | 0;

export default {
affine: "VmPort.affine",
cases: [
{ name: "recv_acc_fwd reg+val", export: "recv_acc_fwd", args: [I, I], oracle: (reg, val) => i32(reg + val) },
{ name: "recv_acc_inv reg-val", export: "recv_acc_inv", args: [I, I], oracle: (reg, val) => i32(reg - val) },
{ name: "recv_acc_roundtrip == reg", export: "recv_acc_roundtrip", args: [I, I], oracle: (reg, val) => i32(reg) },
{ name: "recv_ptr_fwd ptr+1", export: "recv_ptr_fwd", args: [I], oracle: (ptr) => i32(ptr + 1) },
{ name: "recv_ptr_inv ptr-1", export: "recv_ptr_inv", args: [I], oracle: (ptr) => i32(ptr - 1) },
{ name: "recv_ptr_roundtrip == ptr", export: "recv_ptr_roundtrip", args: [I], oracle: (ptr) => i32(ptr) },
{ name: "send_ptr_fwd ptr+1", export: "send_ptr_fwd", args: [I], oracle: (ptr) => i32(ptr + 1) },
{ name: "send_ptr_inv ptr-1", export: "send_ptr_inv", args: [I], oracle: (ptr) => i32(ptr - 1) },
{ name: "send_ptr_roundtrip == ptr", export: "send_ptr_roundtrip", args: [I], oracle: (ptr) => i32(ptr) },
{ name: "send_clears_slot == 0", export: "send_clears_slot", args: [], oracle: () => 0 },
],
};
Loading
Loading