diff --git a/proposals/MIGRATION-PLAN.adoc b/proposals/MIGRATION-PLAN.adoc index 920d319..e933bd7 100644 --- a/proposals/MIGRATION-PLAN.adoc +++ b/proposals/MIGRATION-PLAN.adoc @@ -192,7 +192,8 @@ Heuristic: | 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. | 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. -| 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. +| 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. | F+ | TODO | Compiler walls (string backend, then effects). | Ω | TODO (access-gated) | Cutover + ReScript extinction. |=== diff --git a/proposals/idaptik/migrated/EVIDENCE-C2-wave2a.adoc b/proposals/idaptik/migrated/EVIDENCE-C2-wave2a.adoc new file mode 100644 index 0000000..2987939 --- /dev/null +++ b/proposals/idaptik/migrated/EVIDENCE-C2-wave2a.adoc @@ -0,0 +1,91 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += Cluster C2 wave 2a (VM multiply/divide) — four-gate evidence (captured 2026-06-05) +:toc: macro + +[IMPORTANT] +==== +*Captured run of the 4-gate recipe over the scalar multiply/divide opcodes.* +Wave 1 (#537-era) covered the value-transform opcodes that need only `+`/`-`/ +bitwise ops. This wave 2a covers `Mul` and `Div` — also pure scalar transforms, +so they need *no* array/linear-memory ABI. (The memory opcodes — Push/Pop/Load/ +Store/Call/Loop/IfPos/IfZero and the structural VM files — are wave 2b and *do* +need the array ABI; they are deliberately not in this wave.) Toolchain: +AffineScript compiler `_build/default/bin/main.exe`, Deno 2.8.2. +==== + +toc::[] + +== Summary + +[cols="2,1,1,2,1",options="header"] +|=== +| Kernel | G1 compile | G2 parity | G3 boundary | G4 assail +| `VmMulDiv` | OK | 3322/3322 | n/a (numeric transform) | clean +| *Total* | *1/1* | *3322/3322* | *n/a* | *1/1 clean* +|=== + +Source: `vm/lib/ocaml/Mul.res` + `vm/lib/ocaml/Div.res`. Eleven exports — +`mul_fwd`, `mul_inv`, `mul_roundtrip`, `div_q`, `div_r`, `div_reconstruct`, +`mul_inplace_fwd`, `mul_inplace_inv`, `div_simple_q`, `div_simple_invert`. + +== Re-decomposition (brain/senses) + +The ReScript VM stores state in a `dict` keyed by register name; each +opcode is an `execute`/`invert` closure pair over that dict. Per the brain/ +senses split the register-name strings + dict stay host-side; the brain is the +scalar-int value transform. "The integer IS the register." + +*Reversibility is migrated as explicit headline exports:* + +* `mul_roundtrip` — `mul_inv(a, b, mul_fwd(a,b,c)) == c` (Bennett ancilla: + `c := c + a*b`, inverse `c := c - a*b`). 729/729. +* `div_reconstruct` — `q*b + r == a` for *all* `b` including 0 (the source + stashes the original `a` into `r` on the divide-by-zero branch, so the + identity holds universally). 81/81. + +The intentional-flaw educational variants (`Mul.makeInPlace`, `Div.makeSimple`) +are migrated faithfully as value transforms but carry *no* roundtrip==id claim +(the source ships them precisely to demonstrate where in-place multiply / simple +divide break reversibility). + +== Two real i32 ABI facts surfaced by this opcode pair + +. *JS multiplication is not i32-exact.* `a * b` in JS is exact only below 2^53; + for two i32 operands the product can exceed that and lose precision before + `| 0`. The parity oracle therefore uses `Math.imul`, which matches wasm + `i32.mul` exactly (e.g. `2147483647 * 2147483647 -> 1`). A naive `(a*b)|0` + oracle would have produced false mismatches at the domain extremes. This is a + new fact beyond wave 1 (which used only `+`/`-`, exact in JS over the domain). +. *`i32.div_s` / `i32.rem_s` trap where ReScript wraps/guards.* `i32.div_s` + TRAPS on `b == 0` and on `INT_MIN / -1`; `i32.rem_s` TRAPS on `b == 0` + (but `INT_MIN % -1 == 0`, no trap). ReScript's int `/` truncates through + `| 0` so `INT_MIN / -1` wraps to `INT_MIN`, and the source guards `b == 0` + explicitly. The `.affine` brain reproduces both guards (nested-`if` form, to + stay clear of the unverified `&&` codegen path) so the wasm is a *total* + function matching ReScript's observable output — never a trap. The oracle + re-derives the original `.res` output independently and the two agree across + the full sweep, including every `(x, 0)` and the `(INT_MIN, -1)` pair. + +== Gate detail + +* *G1 compile* — `main.exe compile VmMulDiv.affine -o VmMulDiv.wasm` → WASM, + validates via `WebAssembly.compile`; 11 exports + `memory`. +* *G2 parity* — `parity.mjs vmmuldiv.config.mjs` → 3322/3322 over the i32 + domain `{INT_MIN, -1e6, -7, -1, 0, 1, 7, 1e6, INT_MAX}` (Cartesian per arity). +* *G3 boundary* — n/a. `Mul`/`Div` are numeric transforms with no discrete + value↔integer encoding table, so injectivity is not the relevant property; + the G2 round-trip against the independent oracle is the faithfulness check + (same disposition as wave-1 `VmArith`/`VmBitwise`/`VmAncilla`). +* *G4 assail* — `assail.mjs VmMulDiv.affine` → 0 findings. The numeric guards + return out-of-band-safe values (`0` on divide-by-zero per source; `INT_MIN` + on the wrap); there is no enum decoder, so PA-AFF-001 does not apply. + +== Remaining in cluster C2 + +Wave 2b — the memory/control opcodes (Push, Pop, Load, Store, Call, Loop, +IfPos, IfZero, Recv, Send, CoprocessorCall, InstructionCoprocessor) and the +structural VM files (State, VM, SubroutineRegistry, VmStateCoprocessor, +bindings). These need an *array / linear-memory ABI* (`[len:i32 LE][bytes]` + +`__affine_alloc`), the next real unblocker — it also feeds the string wall. +That is Opus-level ABI design and is the next C2 task. diff --git a/proposals/idaptik/migrated/VmMulDiv/VmMulDiv.affine b/proposals/idaptik/migrated/VmMulDiv/VmMulDiv.affine new file mode 100644 index 0000000..4a1a06f --- /dev/null +++ b/proposals/idaptik/migrated/VmMulDiv/VmMulDiv.affine @@ -0,0 +1,81 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// VmMulDiv -- the reversible integer multiply/divide opcodes of the idaptik VM, +// the pure-integer core extracted from vm/lib/ocaml/{Mul,Div}.res. Per the +// brain/senses split (DESIGN-VISION), the register-name strings and the state +// dict live host-side; the brain is the reversible VALUE transform each opcode +// performs, as scalar-int functions. "The integer IS the register." +// +// Reversibility is the defining invariant of this VM, but MUL and DIV are NOT +// reversible in place -- multiply-by-zero and integer division both erase +// information (Landauer). The source therefore uses Bennett's ancilla trick: +// * MUL.make accumulates the product into a THIRD register: c := c + a*b, +// inverse c := c - a*b -- reversible as long as a,b are untouched. +// * DIV.make keeps BOTH quotient and remainder (q = a/b, r = a mod b), so the +// dividend is reconstructable: a == q*b + r (true even for b == 0, since the +// source stashes the original a into r on the divide-by-zero branch). +// The educational in-place / simple variants (intentionally NOT reversible) are +// migrated faithfully as value transforms, but carry no roundtrip==id claim. +// +//## Two wasm i32 hazards the ReScript source does not share (guarded here) +// i32.div_s TRAPS on b == 0 and on INT_MIN / -1; i32.rem_s TRAPS on b == 0. +// ReScript wraps INT_MIN / -1 to INT_MIN (its `/` truncates through `| 0`) and +// the source guards b == 0 explicitly. We reproduce both guards so the wasm is +// a TOTAL function matching ReScript's observable output -- never a trap. +// (Separately, JS `a*b` loses precision above 2^53, so the parity oracle uses +// Math.imul to stay i32-exact against i32.mul -- see vmmuldiv.config.mjs.) + +// --- MUL.make: ancilla multiply, a reversible inverse-pair on the c register --- +// execute c := c + a*b invert c := c - a*b +pub fn mul_fwd(a: Int, b: Int, c: Int) -> Int { c + a * b } +pub fn mul_inv(a: Int, b: Int, c: Int) -> Int { c - a * b } +// reversibility headline: invert undoes execute (oracle = identity on c). +// Holds over i32 wraparound: (c + a*b) - a*b == c even when a*b overflows. +pub fn mul_roundtrip(a: Int, b: Int, c: Int) -> Int { mul_inv(a, b, mul_fwd(a, b, c)) } // == c + +// --- DIV.make: quotient + remainder, reconstructable dividend --- +// Quotient. b == 0 guard mirrors the source (q := 0). The INT_MIN/-1 guard +// returns ReScript's wrapped value and avoids the i32.div_s trap. +fn div_q_guarded(a: Int, b: Int) -> Int { + if b == 0 { return 0; } + if a == -2147483648 { + if b == -1 { return -2147483648; } + } + a / b +} +pub fn div_q(a: Int, b: Int) -> Int { div_q_guarded(a, b) } +// Remainder. b == 0 stores the original a (the source's divide-by-zero branch). +// i32.rem_s(INT_MIN, -1) == 0 in wasm, matching ReScript's 0 -- no guard needed. +pub fn div_r(a: Int, b: Int) -> Int { + if b == 0 { return a; } + a % b +} +// reversibility headline: a == q*b + r -- the whole reason DIV keeps r. +// Holds for ALL b (b == 0: q=0, r=a, so 0*0 + a == a). +pub fn div_reconstruct(a: Int, b: Int) -> Int { div_q(a, b) * b + div_r(a, b) } // == a + +// --- MUL.makeInPlace: a := a*b (execute), a := a/b (invert) -- INTENTIONAL FLAW +// The source ships this to demonstrate why in-place multiply breaks +// reversibility (b == 0 erases the product; a*b can overflow). We migrate the +// value transforms faithfully; NO roundtrip == id is claimed for them. +pub fn mul_inplace_fwd(a: Int, b: Int) -> Int { a * b } +pub fn mul_inplace_inv(a: Int, b: Int) -> Int { + if b == 0 { return a; } // source leaves a unchanged when b == 0 + if a == -2147483648 { + if b == -1 { return -2147483648; } + } + a / b +} + +// --- DIV.makeSimple: q := a/b (execute; q unchanged if b == 0), q := 0 (invert) +// execute reads the prior quotient register so the b == 0 no-write branch is a +// faithful identity on it. +pub fn div_simple_q(a: Int, b: Int, q_prev: Int) -> Int { + if b == 0 { return q_prev; } // source performs no write when b == 0 + if a == -2147483648 { + if b == -1 { return -2147483648; } + } + a / b +} +// invert clears the quotient ancilla unconditionally. +pub fn div_simple_invert() -> Int { 0 } diff --git a/proposals/idaptik/migrated/VmMulDiv/vmmuldiv.config.mjs b/proposals/idaptik/migrated/VmMulDiv/vmmuldiv.config.mjs new file mode 100644 index 0000000..1da83fa --- /dev/null +++ b/proposals/idaptik/migrated/VmMulDiv/vmmuldiv.config.mjs @@ -0,0 +1,44 @@ +// 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 VmMulDiv.affine (reversible VM multiply/divide +// opcodes; scalar i32 ABI). Each oracle independently re-derives the ORIGINAL +// vm/lib/ocaml/{Mul,Div}.res value transform in JS -- it is NOT read off the +// .affine. Both sides normalise to i32 (| 0), so two's-complement wraparound is +// covered. +// +// Two correctness points, both real ABI facts surfaced by this opcode pair: +// 1. JS `a * b` is exact only below 2^53; for i32 products it must use +// Math.imul to match wasm i32.mul (e.g. 2147483647*2147483647 -> 1). +// 2. ReScript int `/` truncates through `| 0`, so INT_MIN / -1 wraps to +// INT_MIN; `b == 0` is guarded by the source (q := 0, r := a). The oracle +// reproduces the source's observable output; the .affine reproduces it +// with explicit guards because i32.div_s would otherwise TRAP. +const I = { values: [-2147483648, -1000000, -7, -1, 0, 1, 7, 1000000, 2147483647] }; +const i32 = (x) => x | 0; +const imul = (a, b) => Math.imul(a, b); // i32-exact product +const sdiv = (a, b) => (b === 0 ? 0 : i32(a / b)); // Div.res quotient branch +const srem = (a, b) => (b === 0 ? a : i32(a % b)); // Div.res remainder branch + +export default { + affine: "VmMulDiv.affine", + cases: [ + // --- MUL.make ancilla pair + reversibility --- + { name: "mul_fwd c+a*b", export: "mul_fwd", args: [I, I, I], oracle: (a, b, c) => i32(c + imul(a, b)) }, + { name: "mul_inv c-a*b", export: "mul_inv", args: [I, I, I], oracle: (a, b, c) => i32(c - imul(a, b)) }, + { name: "mul_roundtrip == c", export: "mul_roundtrip", args: [I, I, I], oracle: (a, b, c) => i32(c) }, + + // --- DIV.make quotient/remainder + reconstruction (reversibility) --- + { name: "div_q a/b (guarded)", export: "div_q", args: [I, I], oracle: (a, b) => sdiv(a, b) }, + { name: "div_r a mod b (guarded)", export: "div_r", args: [I, I], oracle: (a, b) => srem(a, b) }, + { name: "div_reconstruct == a", export: "div_reconstruct", args: [I, I], oracle: (a, b) => i32(a) }, + + // --- MUL.makeInPlace value transforms (intentional-flaw variant; no rt==id) --- + { name: "mul_inplace_fwd a*b", export: "mul_inplace_fwd", args: [I, I], oracle: (a, b) => imul(a, b) }, + { name: "mul_inplace_inv a/b (b==0 -> a)", export: "mul_inplace_inv", args: [I, I], oracle: (a, b) => (b === 0 ? i32(a) : i32(a / b)) }, + + // --- DIV.makeSimple quotient (b==0 keeps prior q) + invert clears --- + { name: "div_simple_q (b==0 -> q_prev)", export: "div_simple_q", args: [I, I, I], oracle: (a, b, q) => (b === 0 ? i32(q) : i32(a / b)) }, + { name: "div_simple_invert == 0", export: "div_simple_invert", args: [], oracle: () => 0 }, + ], +}; diff --git a/proposals/idaptik/migration-map.json b/proposals/idaptik/migration-map.json index 4cc31ca..7b77694 100644 --- a/proposals/idaptik/migration-map.json +++ b/proposals/idaptik/migration-map.json @@ -91,7 +91,19 @@ "evidence": "proposals/idaptik/migrated/EVIDENCE-C2.adoc", "compiler_findings": "unary ~ codegen bug (i32.xor missing operand; workaround -a-1); >> is arithmetic + no >>> (logical shift-right emulated for ROL/ROR)" }, - "remaining_wave2": ["Mul", "Div", "Push", "Pop", "Load", "Store", "Call", "Loop", "IfPos", "IfZero", "Recv", "Send", "CoprocessorCall", "InstructionCoprocessor", "State", "VM", "SubroutineRegistry", "VmStateCoprocessor", "bindings"], + "done_wave2a": { + "date": "2026-06-05", + "phase": "G", + "staged_at": "proposals/idaptik/migrated/", + "kernels": ["VmMulDiv"], + "opcodes": ["Mul", "Div"], + "note": "Mul/Div are pure SCALAR transforms, not memory ops; need no array ABI, so split out of wave 2 and landed ahead of 2b. Reversibility via Bennett ancilla (mul c:=c+a*b) and quotient+remainder (div q*b+r==a for all b).", + "gates": "1/1 compile; 3322/3322 parity (incl. mul_roundtrip + div_reconstruct); G3 n/a (numeric transform); 1/1 assail-clean", + "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", "files": [ "vm/lib/ocaml/Add.res", "vm/lib/ocaml/And.res",