diff --git a/proposals/MIGRATION-PLAN.adoc b/proposals/MIGRATION-PLAN.adoc index e933bd7..5d204de 100644 --- a/proposals/MIGRATION-PLAN.adoc +++ b/proposals/MIGRATION-PLAN.adoc @@ -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. |=== diff --git a/proposals/idaptik/migrated/EVIDENCE-C2-wave2b.adoc b/proposals/idaptik/migrated/EVIDENCE-C2-wave2b.adoc new file mode 100644 index 0000000..67b842d --- /dev/null +++ b/proposals/idaptik/migrated/EVIDENCE-C2-wave2b.adoc @@ -0,0 +1,103 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += 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` slot accessors + serialise (string-gated). No brain. +| `SubroutineRegistry.res` | name -> `array` 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 .affine -o .wasm` → WASM for all 4 + (VmMemory 346 B, VmStack 243 B, VmPort 508 B, VmControl 299 B). +* *G2 parity* — `parity.mjs .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.) diff --git a/proposals/idaptik/migrated/VmControl/VmControl.affine b/proposals/idaptik/migrated/VmControl/VmControl.affine new file mode 100644 index 0000000..ba8a21c --- /dev/null +++ b/proposals/idaptik/migrated/VmControl/VmControl.affine @@ -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 } diff --git a/proposals/idaptik/migrated/VmControl/vmcontrol.config.mjs b/proposals/idaptik/migrated/VmControl/vmcontrol.config.mjs new file mode 100644 index 0000000..e085de7 --- /dev/null +++ b/proposals/idaptik/migrated/VmControl/vmcontrol.config.mjs @@ -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 (e === 0 ? 0 : (i < m ? 1 : 0)) }, + { name: "loop_iter_next iters+1", export: "loop_iter_next", args: [I], oracle: (i) => i32(i + 1) }, + ], +}; diff --git a/proposals/idaptik/migrated/VmMemory/VmMemory.affine b/proposals/idaptik/migrated/VmMemory/VmMemory.affine new file mode 100644 index 0000000..91c3000 --- /dev/null +++ b/proposals/idaptik/migrated/VmMemory/VmMemory.affine @@ -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 diff --git a/proposals/idaptik/migrated/VmMemory/vmmemory.config.mjs b/proposals/idaptik/migrated/VmMemory/vmmemory.config.mjs new file mode 100644 index 0000000..c639687 --- /dev/null +++ b/proposals/idaptik/migrated/VmMemory/vmmemory.config.mjs @@ -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) }, + ], +}; diff --git a/proposals/idaptik/migrated/VmPort/VmPort.affine b/proposals/idaptik/migrated/VmPort/VmPort.affine new file mode 100644 index 0000000..4282107 --- /dev/null +++ b/proposals/idaptik/migrated/VmPort/VmPort.affine @@ -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 } diff --git a/proposals/idaptik/migrated/VmPort/vmport.config.mjs b/proposals/idaptik/migrated/VmPort/vmport.config.mjs new file mode 100644 index 0000000..900b004 --- /dev/null +++ b/proposals/idaptik/migrated/VmPort/vmport.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 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 }, + ], +}; diff --git a/proposals/idaptik/migrated/VmStack/VmStack.affine b/proposals/idaptik/migrated/VmStack/VmStack.affine new file mode 100644 index 0000000..49080c9 --- /dev/null +++ b/proposals/idaptik/migrated/VmStack/VmStack.affine @@ -0,0 +1,22 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// VmStack -- the stack opcodes PUSH/POP of the idaptik VM, the pure-integer core +// from vm/lib/ocaml/{Push,Pop}.res. The stack (slots `_s:N`, pointer `_sp`) +// lives in the host-side state dict (the senses); the host moves the value +// between register and stack slot. The brain is only the stack-POINTER +// arithmetic plus the register-clear constant -- no array ABI. +// +// PUSH execute stack[sp]:=reg; sp:=sp+1; reg:=0 +// invert sp:=sp-1; reg:=stack[sp]; stack[sp]:=0 +// POP execute sp:=sp-1; reg:=stack[sp]; stack[sp]:=0 +// invert stack[sp]:=reg; sp:=sp+1; reg:=0 +// PUSH and POP are mutual inverses; the shared brain is sp+1 / sp-1 with the +// register cleared to 0. + +// PUSH advances the stack pointer; POP retreats it. +pub fn push_sp(sp: Int) -> Int { sp + 1 } +pub fn pop_sp(sp: Int) -> Int { sp - 1 } +// reversibility: POP undoes PUSH on the pointer (and vice versa). +pub fn sp_roundtrip(sp: Int) -> Int { pop_sp(push_sp(sp)) } // == sp +// PUSH (forward) and POP (inverse) clear the register to 0. +pub fn reg_clear() -> Int { 0 } diff --git a/proposals/idaptik/migrated/VmStack/vmstack.config.mjs b/proposals/idaptik/migrated/VmStack/vmstack.config.mjs new file mode 100644 index 0000000..d6d47a3 --- /dev/null +++ b/proposals/idaptik/migrated/VmStack/vmstack.config.mjs @@ -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 VmStack.affine (PUSH/POP stack-pointer arithmetic; +// scalar i32 ABI). Oracles re-derive vm/lib/ocaml/{Push,Pop}.res. The stack +// slots + pointer are host-side state; only the pointer arithmetic + register +// clear cross 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: "VmStack.affine", + cases: [ + { name: "push_sp sp+1", export: "push_sp", args: [I], oracle: (sp) => i32(sp + 1) }, + { name: "pop_sp sp-1", export: "pop_sp", args: [I], oracle: (sp) => i32(sp - 1) }, + { name: "sp_roundtrip == sp", export: "sp_roundtrip", args: [I], oracle: (sp) => i32(sp) }, + { name: "reg_clear == 0", export: "reg_clear", args: [], oracle: () => 0 }, + ], +}; diff --git a/proposals/idaptik/migration-map.json b/proposals/idaptik/migration-map.json index 7b77694..b0427d0 100644 --- a/proposals/idaptik/migration-map.json +++ b/proposals/idaptik/migration-map.json @@ -80,7 +80,7 @@ "id": "C2", "name": "VM instruction set", "description": "VM instruction modules in vm/lib/ocaml \u2014 one file per opcode, pure-integer reversible VM. Also the wasm binding shim.", - "status": "IN_PROGRESS", + "status": "DONE", "done_wave1": { "date": "2026-06-05", "phase": "D", @@ -102,8 +102,18 @@ "evidence": "proposals/idaptik/migrated/EVIDENCE-C2-wave2a.adoc", "compiler_findings": "JS a*b loses precision >2^53 -> oracle must use Math.imul to match i32.mul; i32.div_s TRAPS on b==0 and INT_MIN/-1 (ReScript wraps) and i32.rem_s TRAPS on b==0 -> brain guards both (nested-if, avoiding unverified && codegen) for a total wasm" }, - "remaining_wave2b": ["Push", "Pop", "Load", "Store", "Call", "Loop", "IfPos", "IfZero", "Recv", "Send", "CoprocessorCall", "InstructionCoprocessor", "State", "VM", "SubroutineRegistry", "VmStateCoprocessor", "bindings"], - "remaining_wave2b_blocker": "needs array/linear-memory ABI ([len:i32 LE][bytes] + __affine_alloc); Opus-level design; also unblocks the string wall", + "done_wave2b": { + "date": "2026-06-05", + "phase": "G", + "staged_at": "proposals/idaptik/migrated/", + "kernels": ["VmMemory", "VmStack", "VmPort", "VmControl"], + "opcodes": ["Load", "Store", "Push", "Pop", "Recv", "Send", "IfPos", "IfZero", "Loop"], + "note": "The 'needs array/linear-memory ABI' premise was WRONG. VmState stores memory/stack/port buffers as string-keyed dict slots (_mem:N, _s:N, _pin:port) = host-side senses; the integer brains are all scalar (additive transforms, pointer arithmetic, branch predicates). No array ABI required.", + "gates": "4/4 compile; 1568/1568 parity (incl. load/store/sp/recv/send round-trips); G3 n/a (transforms/predicates); 4/4 assail-clean", + "evidence": "proposals/idaptik/migrated/EVIDENCE-C2-wave2b.adoc", + "no_kernel_senses": ["Call (orchestration)", "CoprocessorCall (tombstone, never implemented)", "State", "VmState", "VM", "SubroutineRegistry", "VmStateCoprocessor", "InstructionCoprocessor"], + "cluster_complete": true + }, "files": [ "vm/lib/ocaml/Add.res", "vm/lib/ocaml/And.res",