From c3801b05267c1e22c32cc2c781ce8f6f2f5edb5b Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 5 Jun 2026 12:02:06 +0000 Subject: [PATCH] migrate(phase-d/C2 wave 1): reversible VM opcodes, 4-gate green MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Deep wave 2 of the ReScript -> AffineScript -> wasm migration. Cluster C2 (the vm/lib/ocaml reversible instruction set) wave 1: the value-transform opcodes re-decomposed into four pure-integer kernels staged under proposals/idaptik/migrated/, each verified by the 4-gate recipe. The VM stores state in a dict keyed by register NAME, with each instruction a pair of execute/invert closures. Re-decomposition: the register names + dict stay host-side (the senses); the brain is the reversible scalar-int VALUE transform per opcode. "The integer IS the register." The defining VM invariant is reversibility (invert undoes execute). It is pinned directly as *_roundtrip exports whose oracle is the identity, and swept in Gate 2 over i32 extremes. VmArith ADD/SUB (inverse pair), NEGATE/NOOP/SWAP (self-inverse) VmBitwise FLIP/XOR (self-inverse), ROL/ROR (inverse pair, 32-bit) VmAncilla AND/OR via Bennett's ancilla (reversible iff ancilla c == 0) VmInstruction 23-opcode instruction-set encoding + tier classifier Four gates green (captured in migrated/EVIDENCE-C2.adoc): G1 compile 4/4 -> wasm G2 parity 2100/2100 oracle-vs-wasm inputs, incl. every reversibility round-trip (inverse undoes execute) over i32 extremes G3 echo-boundary VmInstruction 23-opcode encoding LOSSLESS (agda exit 0) G4 assail 4/4 clean Three AffineScript backend facts surfaced and worked around (recorded in EVIDENCE-C2.adoc as findings): * unary ~ mis-compiles (i32.xor missing an operand) -> FLIP uses the two's-complement identity ~a == -a - 1 (verified equal, self-inverse); * >> is arithmetic and >>> does not exist, but ROL/ROR need a logical shift right -> emulated as (a >> n) & ((1 << (32 - n)) - 1); rotations then match JS ((a<>>(32-n)))|0 and round-trip over the full i32 range; * << and i32 wrap are correct (the VM's word model). The unary-~ bug is a candidate Phase-F compiler fix. AND/OR are the honest outlier: reversible only via Bennett's ancilla trick and only under the declared precondition that the ancilla starts at 0; every other opcode here is unconditionally reversible. Wave 2 (deferred — needs an array/linear-memory ABI + control-flow model): Mul/Div, stack/memory (Push/Pop/Load/Store), control (Call/Loop/IfPos/IfZero), I/O (Send/Recv/CoprocessorCall), and the structural VM files (State, VM, SubroutineRegistry, *Coprocessor, bindings). Ledger: Phase D (C2 wave 1) DONE; migration-map.json C2 -> IN_PROGRESS with the wave-1 detail. Staged, not applied (idaptik write-access gate, Phase Omega). https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --- proposals/MIGRATION-PLAN.adoc | 3 +- proposals/idaptik/migrated/EVIDENCE-C2.adoc | 128 +++++++++++++++ proposals/idaptik/migrated/README.adoc | 29 +++- .../migrated/VmAncilla/VmAncilla.affine | 38 +++++ .../migrated/VmAncilla/vmancilla.config.mjs | 18 +++ .../idaptik/migrated/VmArith/VmArith.affine | 53 +++++++ .../migrated/VmArith/vmarith.config.mjs | 28 ++++ .../migrated/VmBitwise/VmBitwise.affine | 41 +++++ .../migrated/VmBitwise/vmbitwise.config.mjs | 25 +++ .../VmInstruction/VmInstruction.affine | 55 +++++++ .../VmInstruction/VmInstructionBoundary.agda | 148 ++++++++++++++++++ .../VmInstruction/vminstruction.config.mjs | 29 ++++ proposals/idaptik/migration-map.json | 13 +- 13 files changed, 605 insertions(+), 3 deletions(-) create mode 100644 proposals/idaptik/migrated/EVIDENCE-C2.adoc create mode 100644 proposals/idaptik/migrated/VmAncilla/VmAncilla.affine create mode 100644 proposals/idaptik/migrated/VmAncilla/vmancilla.config.mjs create mode 100644 proposals/idaptik/migrated/VmArith/VmArith.affine create mode 100644 proposals/idaptik/migrated/VmArith/vmarith.config.mjs create mode 100644 proposals/idaptik/migrated/VmBitwise/VmBitwise.affine create mode 100644 proposals/idaptik/migrated/VmBitwise/vmbitwise.config.mjs create mode 100644 proposals/idaptik/migrated/VmInstruction/VmInstruction.affine create mode 100644 proposals/idaptik/migrated/VmInstruction/VmInstructionBoundary.agda create mode 100644 proposals/idaptik/migrated/VmInstruction/vminstruction.config.mjs diff --git a/proposals/MIGRATION-PLAN.adoc b/proposals/MIGRATION-PLAN.adoc index 0ca401b..a8acb56 100644 --- a/proposals/MIGRATION-PLAN.adoc +++ b/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. |=== diff --git a/proposals/idaptik/migrated/EVIDENCE-C2.adoc b/proposals/idaptik/migrated/EVIDENCE-C2.adoc new file mode 100644 index 0000000..a729791 --- /dev/null +++ b/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 += 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` 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<>(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<>>(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). diff --git a/proposals/idaptik/migrated/README.adoc b/proposals/idaptik/migrated/README.adoc index ce7fe50..e58e7c7 100644 --- a/proposals/idaptik/migrated/README.adoc +++ b/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 -= 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` 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) ---- diff --git a/proposals/idaptik/migrated/VmAncilla/VmAncilla.affine b/proposals/idaptik/migrated/VmAncilla/VmAncilla.affine new file mode 100644 index 0000000..5649422 --- /dev/null +++ b/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 diff --git a/proposals/idaptik/migrated/VmAncilla/vmancilla.config.mjs b/proposals/idaptik/migrated/VmAncilla/vmancilla.config.mjs new file mode 100644 index 0000000..0c84e9f --- /dev/null +++ b/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 }, + ], +}; diff --git a/proposals/idaptik/migrated/VmArith/VmArith.affine b/proposals/idaptik/migrated/VmArith/VmArith.affine new file mode 100644 index 0000000..f342452 --- /dev/null +++ b/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 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 diff --git a/proposals/idaptik/migrated/VmArith/vmarith.config.mjs b/proposals/idaptik/migrated/VmArith/vmarith.config.mjs new file mode 100644 index 0000000..155e8df --- /dev/null +++ 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 }, + ], +}; diff --git a/proposals/idaptik/migrated/VmBitwise/VmBitwise.affine b/proposals/idaptik/migrated/VmBitwise/VmBitwise.affine new file mode 100644 index 0000000..e9661c6 --- /dev/null +++ b/proposals/idaptik/migrated/VmBitwise/VmBitwise.affine @@ -0,0 +1,41 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// VmBitwise -- the reversible bitwise opcodes of the idaptik VM, the +// pure-integer core extracted from vm/lib/ocaml/{Flip,Xor,Rol,Ror}.res. Same +// brain/senses split as VmArith: register names + dict are host-side; the brain +// is the reversible bit-level value transform. Every export's reversibility is +// pinned as a *_roundtrip whose oracle is the identity. +// +//## Opcode value semantics +// FLIP execute a := ~a invert a := ~a (self-inverse) +// XOR execute a := a ^ b invert a := a ^ b (self-inverse in a) +// ROL execute a := rotl(a,bits) invert a := rotr(a,bits) (inverse pair) +// ROR execute a := rotr(a,bits) invert a := rotl(a,bits) (inverse pair) +// +//## Two compiler facts this kernel is written around (see EVIDENCE.adoc) +// * Unary `~` mis-compiles (emits i32.xor missing an operand), so FLIP uses +// the two's-complement identity ~a == -a - 1. Self-inverse is preserved: +// ~(~a) = a, and (-(-a-1))-1 = a. +// * `>>` is ARITHMETIC (sign-propagating) and `>>>` does not exist, but the +// ReScript ROL/ROR use a LOGICAL shift-right (lsr). We emulate it: +// lsr(a,n) = (a >> n) & ((1 << (32 - n)) - 1) for 1 <= n <= 31 +// which clears the n sign-extended high bits. The mask (1<<(32-n))-1 wraps +// correctly at i32 (e.g. n=1 -> (1<<31)-1 = 0x7FFFFFFF). +// bits is the rotation amount, valid for 1 <= bits <= 31. + +// --- FLIP: self-inverse (~a via the two's-complement identity) --- +pub fn flip(a: Int) -> Int { -a - 1 } +pub fn flip_roundtrip(a: Int) -> Int { flip(flip(a)) } // == a + +// --- XOR: self-inverse in a --- +pub fn xor(a: Int, b: Int) -> Int { a ^ b } +pub fn xor_roundtrip(a: Int, b: Int) -> Int { xor(xor(a, b), b) } // == a + +// --- logical shift right (32-bit), emulated; private helper --- +fn lsr(a: Int, n: Int) -> Int { (a >> n) & ((1 << (32 - n)) - 1) } + +// --- ROL / ROR: inverse pair (rotate left/right by `bits`, 1..31) --- +pub fn rol(a: Int, bits: Int) -> Int { (a << bits) | lsr(a, 32 - bits) } +pub fn ror(a: Int, bits: Int) -> Int { lsr(a, bits) | (a << (32 - bits)) } +pub fn rol_roundtrip(a: Int, bits: Int) -> Int { ror(rol(a, bits), bits) } // == a +pub fn ror_roundtrip(a: Int, bits: Int) -> Int { rol(ror(a, bits), bits) } // == a diff --git a/proposals/idaptik/migrated/VmBitwise/vmbitwise.config.mjs b/proposals/idaptik/migrated/VmBitwise/vmbitwise.config.mjs new file mode 100644 index 0000000..7cfb363 --- /dev/null +++ b/proposals/idaptik/migrated/VmBitwise/vmbitwise.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 VmBitwise.affine (reversible VM bitwise opcodes; +// scalar i32 ABI). Oracles re-derive FLIP/XOR/ROL/ROR independently using JS's +// native 32-bit bitwise ops (including the logical >>> the kernel has to emulate) +// plus the reversibility round-trips (oracle = identity). +const I = { values: [-2147483648, -1000000, -2, -1, 0, 1, 7, 1000000, 1431655765, -1431655766, 2147483647] }; +const BITS = { values: [1, 2, 7, 8, 16, 24, 31] }; +const rol = (a, n) => ((a << n) | (a >>> (32 - n))) | 0; +const ror = (a, n) => ((a >>> n) | (a << (32 - n))) | 0; +export default { + affine: "VmBitwise.affine", + cases: [ + { name: "flip ~a", export: "flip", args: [I], oracle: (a) => ~a | 0 }, + { name: "flip_roundtrip == a", export: "flip_roundtrip", args: [I], oracle: (a) => a | 0 }, + { name: "xor a^b", export: "xor", args: [I, I], oracle: (a, b) => (a ^ b) | 0 }, + { name: "xor_roundtrip == a", export: "xor_roundtrip", args: [I, I], oracle: (a, b) => a | 0 }, + { name: "rol == js rotl", export: "rol", args: [I, BITS], oracle: (a, n) => rol(a, n) }, + { name: "ror == js rotr", export: "ror", args: [I, BITS], oracle: (a, n) => ror(a, n) }, + // --- reversibility: ROR undoes ROL and vice versa (oracle = identity) --- + { name: "rol_roundtrip == a", export: "rol_roundtrip", args: [I, BITS], oracle: (a, n) => a | 0 }, + { name: "ror_roundtrip == a", export: "ror_roundtrip", args: [I, BITS], oracle: (a, n) => a | 0 }, + ], +}; diff --git a/proposals/idaptik/migrated/VmInstruction/VmInstruction.affine b/proposals/idaptik/migrated/VmInstruction/VmInstruction.affine new file mode 100644 index 0000000..3efd849 --- /dev/null +++ b/proposals/idaptik/migrated/VmInstruction/VmInstruction.affine @@ -0,0 +1,55 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// VmInstruction -- the instruction-set taxonomy of the idaptik reversible VM, +// the pure-integer core behind vm/lib/ocaml/Instruction.res. The ReScript +// `Instruction.t` carries an `instructionType` STRING and `execute`/`invert` +// closures; the string is host-side (the senses). The brain is the canonical +// integer OPCODE for each of the 23 instructions, plus the tier each belongs to +// (the tier gates which opcodes a puzzle admits -- see PuzzleFormat.affine). +// +//## Opcode encoding (the header contract for the JS host) -- tier order +// tier 0 (register arithmetic) tier 2 (stack / memory) +// 0 NOOP 5 FLIP 10 XOR 16 PUSH 18 LOAD +// 1 ADD 6 ROL 11 MUL 17 POP 19 STORE +// 2 SUB 7 ROR 12 DIV tier 3 (subroutines) +// 3 NEGATE 8 AND 20 CALL +// 4 SWAP 9 OR tier 4 (I/O channels) +// tier 1 (conditionals) 21 SEND 22 RECV +// 13 IFZERO 14 IFPOS 15 LOOP +// The encoding is LOSSLESS: 23 instructions map to 23 distinct opcodes, so the +// host round-trips instruction <-> opcode with no collision (certified by +// echo-boundary, VmInstructionBoundary.agda). An opcode outside 0..22 is not an +// instruction: clamp returns the out-of-band sentinel -1. + +pub fn opcode_count() -> Int { 23 } +pub fn tier_count() -> Int { 5 } + +// Whether an integer names a defined opcode. 1 = valid, 0 = out of band. +pub fn is_valid_opcode(op: Int) -> Int { + if op < 0 { 0 } else { if op > 22 { 0 } else { 1 } } +} + +// Canonicalise: identity on a valid 0..22 opcode, the sentinel -1 otherwise. +pub fn clamp_opcode(op: Int) -> Int { + if is_valid_opcode(op) == 1 { op } else { -1 } +} + +// The tier (0..4) an opcode belongs to, or -1 if the opcode is out of band. +// A puzzle of tier T admits exactly the opcodes with tier_of_opcode <= T. +pub fn tier_of_opcode(op: Int) -> Int { + if is_valid_opcode(op) == 0 { return -1; } + if op <= 12 { return 0; } // NOOP..DIV -- register arithmetic + if op <= 15 { return 1; } // IFZERO..LOOP-- conditionals + if op <= 19 { return 2; } // PUSH..STORE -- stack / memory + if op == 20 { return 3; } // CALL -- subroutines + 4 // SEND, RECV -- I/O channels +} + +// Whether an opcode is admitted by a puzzle of the given tier (opcode tier <= +// puzzle tier). Out-of-band opcode or tier -> 0. +pub fn opcode_in_tier(op: Int, puzzle_tier: Int) -> Int { + let ot = tier_of_opcode(op); + if ot < 0 { return 0; } + if puzzle_tier < 0 { return 0; } + if ot <= puzzle_tier { 1 } else { 0 } +} diff --git a/proposals/idaptik/migrated/VmInstruction/VmInstructionBoundary.agda b/proposals/idaptik/migrated/VmInstruction/VmInstructionBoundary.agda new file mode 100644 index 0000000..e482ec0 --- /dev/null +++ b/proposals/idaptik/migrated/VmInstruction/VmInstructionBoundary.agda @@ -0,0 +1,148 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "NOOP": 0, +-- "ADD": 1, +-- "SUB": 2, +-- "NEGATE": 3, +-- "SWAP": 4, +-- "FLIP": 5, +-- "ROL": 6, +-- "ROR": 7, +-- "AND": 8, +-- "OR": 9, +-- "XOR": 10, +-- "MUL": 11, +-- "DIV": 12, +-- "IFZERO": 13, +-- "IFPOS": 14, +-- "LOOP": 15, +-- "PUSH": 16, +-- "POP": 17, +-- "LOAD": 18, +-- "STORE": 19, +-- "CALL": 20, +-- "SEND": 21, +-- "RECV": 22 +-- } + +module VmInstructionBoundary where + +open import Echo using (Echo) +open import EchoImageFactorization using (Injective) +open import EchoEncodingFaithfulness using (Encoding; module EncodingTheorems) + +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl) +open import Relation.Nullary using (¬_) + + +-- The host-side enumerated value (one constructor per table name). +-- c0 = NOOP +-- c1 = ADD +-- c2 = SUB +-- c3 = NEGATE +-- c4 = SWAP +-- c5 = FLIP +-- c6 = ROL +-- c7 = ROR +-- c8 = AND +-- c9 = OR +-- c10 = XOR +-- c11 = MUL +-- c12 = DIV +-- c13 = IFZERO +-- c14 = IFPOS +-- c15 = LOOP +-- c16 = PUSH +-- c17 = POP +-- c18 = LOAD +-- c19 = STORE +-- c20 = CALL +-- c21 = SEND +-- c22 = RECV +data Host : Set where + c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 +code c4 = 4 +code c5 = 5 +code c6 = 6 +code c7 = 7 +code c8 = 8 +code c9 = 9 +code c10 = 10 +code c11 = 11 +code c12 = 12 +code c13 = 13 +code c14 = 14 +code c15 = 15 +code c16 = 16 +code c17 = 17 +code c18 = 18 +code c19 = 19 +code c20 = 20 +code c21 = 21 +code c22 = 22 + +-- Injectivity by exhaustive case analysis. The codes are literal +-- numerals, so listing the diagonal refl clauses is enough: Agda's +-- coverage checker discharges the off-diagonal pairs as absurd +-- numeral equalities (mirrors rankCode-injective). +code-injective : Injective code +code-injective {c0} {c0} _ = refl +code-injective {c1} {c1} _ = refl +code-injective {c2} {c2} _ = refl +code-injective {c3} {c3} _ = refl +code-injective {c4} {c4} _ = refl +code-injective {c5} {c5} _ = refl +code-injective {c6} {c6} _ = refl +code-injective {c7} {c7} _ = refl +code-injective {c8} {c8} _ = refl +code-injective {c9} {c9} _ = refl +code-injective {c10} {c10} _ = refl +code-injective {c11} {c11} _ = refl +code-injective {c12} {c12} _ = refl +code-injective {c13} {c13} _ = refl +code-injective {c14} {c14} _ = refl +code-injective {c15} {c15} _ = refl +code-injective {c16} {c16} _ = refl +code-injective {c17} {c17} _ = refl +code-injective {c18} {c18} _ = refl +code-injective {c19} {c19} _ = refl +code-injective {c20} {c20} _ = refl +code-injective {c21} {c21} _ = refl +code-injective {c22} {c22} _ = refl + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +-- Re-export the lossless-half headline, instantiated and proved: +-- every integer code determines its host value uniquely. +module Theorems = EncodingTheorems encoding + +boundary-lossless : + (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂ +boundary-lossless = Theorems.encoding-lossless code-injective + diff --git a/proposals/idaptik/migrated/VmInstruction/vminstruction.config.mjs b/proposals/idaptik/migrated/VmInstruction/vminstruction.config.mjs new file mode 100644 index 0000000..4f984e2 --- /dev/null +++ b/proposals/idaptik/migrated/VmInstruction/vminstruction.config.mjs @@ -0,0 +1,29 @@ +// 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 VmInstruction.affine (VM opcode taxonomy; scalar i32 +// ABI). Oracle re-derives the 0..22 opcode band, the tier classifier, and the +// tier-admission predicate. +const validOp = (op) => op >= 0 && op <= 22; +const tierOf = (op) => !validOp(op) ? -1 : op <= 12 ? 0 : op <= 15 ? 1 : op <= 19 ? 2 : op === 20 ? 3 : 4; +export default { + affine: "VmInstruction.affine", + cases: [ + { name: "opcode_count()", export: "opcode_count", args: [], oracle: () => 23 }, + { name: "tier_count()", export: "tier_count", args: [], oracle: () => 5 }, + { name: "is_valid_opcode over [-3..26]", export: "is_valid_opcode", args: [[-3, 26]], oracle: (op) => (validOp(op) ? 1 : 0) }, + { name: "clamp_opcode over [-3..26]", export: "clamp_opcode", args: [[-3, 26]], oracle: (op) => (validOp(op) ? op : -1) }, + { name: "tier_of_opcode over [-3..26]", export: "tier_of_opcode", args: [[-3, 26]], oracle: (op) => tierOf(op) }, + { + name: "opcode_in_tier over [-2..24] x [-1..5]", + export: "opcode_in_tier", + args: [[-2, 24], [-1, 5]], + oracle: (op, pt) => { + const ot = tierOf(op); + if (ot < 0) return 0; + if (pt < 0) return 0; + return ot <= pt ? 1 : 0; + }, + }, + ], +}; diff --git a/proposals/idaptik/migration-map.json b/proposals/idaptik/migration-map.json index 3476b5a..5f7f84a 100644 --- a/proposals/idaptik/migration-map.json +++ b/proposals/idaptik/migration-map.json @@ -80,7 +80,18 @@ "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": "TODO", + "status": "IN_PROGRESS", + "done_wave1": { + "date": "2026-06-05", + "phase": "D", + "staged_at": "proposals/idaptik/migrated/", + "kernels": ["VmArith", "VmBitwise", "VmAncilla", "VmInstruction"], + "opcodes": ["Add", "Sub", "Negate", "Noop", "Swap", "Flip", "Xor", "Rol", "Ror", "And", "Or", "Instruction"], + "gates": "4/4 compile; 2100/2100 parity (incl. all reversibility round-trips); 1 echo-boundary LOSSLESS (23-opcode encoding, agda exit 0); 4/4 assail-clean", + "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"], "files": [ "vm/lib/ocaml/Add.res", "vm/lib/ocaml/And.res",