|
| 1 | +// SPDX-License-Identifier: AGPL-3.0-or-later |
| 2 | +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | += Cluster C2 wave 2a (VM multiply/divide) — four-gate evidence (captured 2026-06-05) |
| 4 | +:toc: macro |
| 5 | + |
| 6 | +[IMPORTANT] |
| 7 | +==== |
| 8 | +*Captured run of the 4-gate recipe over the scalar multiply/divide opcodes.* |
| 9 | +Wave 1 (#537-era) covered the value-transform opcodes that need only `+`/`-`/ |
| 10 | +bitwise ops. This wave 2a covers `Mul` and `Div` — also pure scalar transforms, |
| 11 | +so they need *no* array/linear-memory ABI. (The memory opcodes — Push/Pop/Load/ |
| 12 | +Store/Call/Loop/IfPos/IfZero and the structural VM files — are wave 2b and *do* |
| 13 | +need the array ABI; they are deliberately not in this wave.) Toolchain: |
| 14 | +AffineScript compiler `_build/default/bin/main.exe`, Deno 2.8.2. |
| 15 | +==== |
| 16 | + |
| 17 | +toc::[] |
| 18 | + |
| 19 | +== Summary |
| 20 | + |
| 21 | +[cols="2,1,1,2,1",options="header"] |
| 22 | +|=== |
| 23 | +| Kernel | G1 compile | G2 parity | G3 boundary | G4 assail |
| 24 | +| `VmMulDiv` | OK | 3322/3322 | n/a (numeric transform) | clean |
| 25 | +| *Total* | *1/1* | *3322/3322* | *n/a* | *1/1 clean* |
| 26 | +|=== |
| 27 | + |
| 28 | +Source: `vm/lib/ocaml/Mul.res` + `vm/lib/ocaml/Div.res`. Eleven exports — |
| 29 | +`mul_fwd`, `mul_inv`, `mul_roundtrip`, `div_q`, `div_r`, `div_reconstruct`, |
| 30 | +`mul_inplace_fwd`, `mul_inplace_inv`, `div_simple_q`, `div_simple_invert`. |
| 31 | + |
| 32 | +== Re-decomposition (brain/senses) |
| 33 | + |
| 34 | +The ReScript VM stores state in a `dict<int>` keyed by register name; each |
| 35 | +opcode is an `execute`/`invert` closure pair over that dict. Per the brain/ |
| 36 | +senses split the register-name strings + dict stay host-side; the brain is the |
| 37 | +scalar-int value transform. "The integer IS the register." |
| 38 | + |
| 39 | +*Reversibility is migrated as explicit headline exports:* |
| 40 | + |
| 41 | +* `mul_roundtrip` — `mul_inv(a, b, mul_fwd(a,b,c)) == c` (Bennett ancilla: |
| 42 | + `c := c + a*b`, inverse `c := c - a*b`). 729/729. |
| 43 | +* `div_reconstruct` — `q*b + r == a` for *all* `b` including 0 (the source |
| 44 | + stashes the original `a` into `r` on the divide-by-zero branch, so the |
| 45 | + identity holds universally). 81/81. |
| 46 | + |
| 47 | +The intentional-flaw educational variants (`Mul.makeInPlace`, `Div.makeSimple`) |
| 48 | +are migrated faithfully as value transforms but carry *no* roundtrip==id claim |
| 49 | +(the source ships them precisely to demonstrate where in-place multiply / simple |
| 50 | +divide break reversibility). |
| 51 | + |
| 52 | +== Two real i32 ABI facts surfaced by this opcode pair |
| 53 | + |
| 54 | +. *JS multiplication is not i32-exact.* `a * b` in JS is exact only below 2^53; |
| 55 | + for two i32 operands the product can exceed that and lose precision before |
| 56 | + `| 0`. The parity oracle therefore uses `Math.imul`, which matches wasm |
| 57 | + `i32.mul` exactly (e.g. `2147483647 * 2147483647 -> 1`). A naive `(a*b)|0` |
| 58 | + oracle would have produced false mismatches at the domain extremes. This is a |
| 59 | + new fact beyond wave 1 (which used only `+`/`-`, exact in JS over the domain). |
| 60 | +. *`i32.div_s` / `i32.rem_s` trap where ReScript wraps/guards.* `i32.div_s` |
| 61 | + TRAPS on `b == 0` and on `INT_MIN / -1`; `i32.rem_s` TRAPS on `b == 0` |
| 62 | + (but `INT_MIN % -1 == 0`, no trap). ReScript's int `/` truncates through |
| 63 | + `| 0` so `INT_MIN / -1` wraps to `INT_MIN`, and the source guards `b == 0` |
| 64 | + explicitly. The `.affine` brain reproduces both guards (nested-`if` form, to |
| 65 | + stay clear of the unverified `&&` codegen path) so the wasm is a *total* |
| 66 | + function matching ReScript's observable output — never a trap. The oracle |
| 67 | + re-derives the original `.res` output independently and the two agree across |
| 68 | + the full sweep, including every `(x, 0)` and the `(INT_MIN, -1)` pair. |
| 69 | + |
| 70 | +== Gate detail |
| 71 | + |
| 72 | +* *G1 compile* — `main.exe compile VmMulDiv.affine -o VmMulDiv.wasm` → WASM, |
| 73 | + validates via `WebAssembly.compile`; 11 exports + `memory`. |
| 74 | +* *G2 parity* — `parity.mjs vmmuldiv.config.mjs` → 3322/3322 over the i32 |
| 75 | + domain `{INT_MIN, -1e6, -7, -1, 0, 1, 7, 1e6, INT_MAX}` (Cartesian per arity). |
| 76 | +* *G3 boundary* — n/a. `Mul`/`Div` are numeric transforms with no discrete |
| 77 | + value↔integer encoding table, so injectivity is not the relevant property; |
| 78 | + the G2 round-trip against the independent oracle is the faithfulness check |
| 79 | + (same disposition as wave-1 `VmArith`/`VmBitwise`/`VmAncilla`). |
| 80 | +* *G4 assail* — `assail.mjs VmMulDiv.affine` → 0 findings. The numeric guards |
| 81 | + return out-of-band-safe values (`0` on divide-by-zero per source; `INT_MIN` |
| 82 | + on the wrap); there is no enum decoder, so PA-AFF-001 does not apply. |
| 83 | + |
| 84 | +== Remaining in cluster C2 |
| 85 | + |
| 86 | +Wave 2b — the memory/control opcodes (Push, Pop, Load, Store, Call, Loop, |
| 87 | +IfPos, IfZero, Recv, Send, CoprocessorCall, InstructionCoprocessor) and the |
| 88 | +structural VM files (State, VM, SubroutineRegistry, VmStateCoprocessor, |
| 89 | +bindings). These need an *array / linear-memory ABI* (`[len:i32 LE][bytes]` + |
| 90 | +`__affine_alloc`), the next real unblocker — it also feeds the string wall. |
| 91 | +That is Opus-level ABI design and is the next C2 task. |
0 commit comments