Skip to content

Commit b37af77

Browse files
migrate(C2 wave 2b): VM memory/stack/port/control opcodes — cluster C2 complete (#540)
## C2 wave 2b — and the array-ABI blocker was never real The ledger scoped wave 2b as **"needs an array/linear-memory ABI."** Reading the actual opcode sources overturned that: the VM's memory, stack, and port buffers are **not arrays in the brain** — `VmState.res` stores every one as **string-keyed dict slots** (`_mem:N`, `_s:N`, `_pin:port`). That dict is host-side **state (the senses)**; the integer brains are all **scalar**. No array ABI was required — this is the established scalar recipe. ### 4 kernels, 9 opcodes (re-decomposed per brain/senses) | Kernel | Opcodes | Scalar brain | |---|---|---| | `VmMemory` | LOAD, STORE | additive `reg ± mem` / `mem ± reg` (host owns `memory[]`) | | `VmStack` | PUSH, POP | stack-pointer `sp ± 1` + register clear (host owns the slots) | | `VmPort` | RECV, SEND | port-pointer `ptr ± 1` + additive accumulate | | `VmControl` | IF_POS, IF_ZERO, LOOP | scalar branch/continuation predicates (bodies host-orchestrated) | Reversibility migrated as explicit round-trip exports: `load`/`store`/`sp`/`recv_acc`/`recv_ptr`/`send_ptr` all round-trip to identity. IF/LOOP carry no value round-trip — their Janus reversibility is host orchestration (reverse run applies the same predicate to the *exit* register, runs the chosen branch reversed). ### Four gates green | Gate | Result | |---|---| | G1 compile | 4/4 (WASM) | | G2 parity | **1568/1568** (independent oracles re-derive each `.res` transform) | | G3 boundary | n/a (transforms/predicates — no value↔integer encoding table) | | G4 assail | 4/4 clean | ### No-kernel senses (faithfully classified, not migrated) `Call` (orchestration) · `CoprocessorCall` (**tombstone** — never implemented, superseded by SEND/RECV) · `State`/`VmState`/`VM`/`SubroutineRegistry`/`VmStateCoprocessor`/`InstructionCoprocessor` (state containers / bridges). **Cluster C2 COMPLETE** — wave 1 (11 opcodes + taxonomy) + 2a (Mul/Div) + 2b (these 9) = every reversible-VM opcode with a separable integer brain. NEXT = C3. Staged-only under `proposals/idaptik/migrated/` — idaptik write-gate honoured. https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --- _Generated by [Claude Code](https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent de546e2 commit b37af77

11 files changed

Lines changed: 300 additions & 4 deletions

File tree

proposals/MIGRATION-PLAN.adoc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -193,7 +193,8 @@ Heuristic:
193193
| 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.
194194
| 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.
195195
| 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.
196-
| 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.
196+
| 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.
197+
| 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.
197198
| F+ | TODO | Compiler walls (string backend, then effects).
198199
| Ω | TODO (access-gated) | Cutover + ReScript extinction.
199200
|===
Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
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 2b (VM memory / stack / port / control) — four-gate evidence (captured 2026-06-05)
4+
:toc: macro
5+
6+
[IMPORTANT]
7+
====
8+
*The ledger's premise for this wave was wrong, and re-decomposition overturned
9+
it.* Wave 2b was scoped as "needs an array/linear-memory ABI." Reading the
10+
actual opcode sources shows the VM's memory, stack, and port buffers are NOT
11+
arrays in the brain — `VmState.res` stores every one of them as *string-keyed
12+
dict entries* (`_mem:0`, `_s:0`, `_pin:port`, ...). That dict is host-side STATE
13+
(the senses). The pure-integer brains are all SCALAR: additive value transforms,
14+
pointer arithmetic, and branch predicates. So wave 2b needs *no* array ABI —
15+
it is the established scalar recipe. Toolchain: AffineScript compiler
16+
`_build/default/bin/main.exe`, Deno 2.8.2.
17+
====
18+
19+
toc::[]
20+
21+
== Summary
22+
23+
[cols="2,2,1,1,2,1",options="header"]
24+
|===
25+
| Kernel | Opcodes | G1 | G2 parity | G3 | G4 assail
26+
| `VmMemory` | LOAD, STORE | OK | 486/486 | n/a (transform) | clean
27+
| `VmStack` | PUSH, POP | OK | 28/28 | n/a (transform) | clean
28+
| `VmPort` | RECV, SEND | OK | 298/298 | n/a (transform) | clean
29+
| `VmControl` | IF_POS, IF_ZERO, LOOP | OK | 756/756 | n/a (predicate) | clean
30+
| *Total* | *9 opcodes* | *4/4* | *1568/1568* | *n/a* | *4/4 clean*
31+
|===
32+
33+
== The re-decomposition that dissolved the array-ABI blocker
34+
35+
Each opcode manipulates host-side state, but the integer brain is scalar:
36+
37+
[cols="1,3,2",options="header"]
38+
|===
39+
| Opcode | Source semantics | Scalar brain (the wasm)
40+
| LOAD | `reg += memory[addr]` / `reg -= memory[addr]` | additive `reg ± mem` (host supplies `mem`)
41+
| STORE | `memory[addr] += reg` / `-= reg` | additive `mem ± reg`
42+
| PUSH | `stack[sp]:=reg; sp++; reg:=0` | pointer `sp+1`, register clear `0`
43+
| POP | `sp--; reg:=stack[sp]; stack[sp]:=0` | pointer `sp-1`
44+
| RECV | `reg += port_in[ptr]; ptr++` | additive `reg ± val`, pointer `ptr±1`
45+
| SEND | `port_out[ptr]:=reg; ptr++` (inv writes 0) | pointer `ptr±1`, slot clear `0`
46+
| IF_POS | run then/else by `testReg > 0` | predicate `v > 0 -> 1/0`
47+
| IF_ZERO| run then/else by `testReg == 0` | predicate `v == 0 -> 1/0`
48+
| LOOP | `while exitReg != 0 && iters < max` | continuation predicate + `iters+1`
49+
|===
50+
51+
The arrays (`stack`, `memory`, port buffers) and the register dict are the
52+
*senses* — host-owned `VmState` dict slots. The host performs every array
53+
get/set; the wasm computes only the next pointer, the accumulated value, or the
54+
branch decision. "The integer IS the register / pointer / predicate."
55+
56+
*Reversibility is migrated as explicit round-trip exports* (the headline gate):
57+
`load_roundtrip == reg`, `store_roundtrip == mem`, `sp_roundtrip == sp`,
58+
`recv_acc_roundtrip == reg`, `recv_ptr_roundtrip == ptr`,
59+
`send_ptr_roundtrip == ptr`. IF_POS/IF_ZERO/LOOP carry no value round-trip —
60+
their Janus reversibility is host orchestration (the reverse run applies the
61+
same predicate to the *exit* register and runs the chosen branch reversed); the
62+
brain is the shared predicate.
63+
64+
== No-kernel files (host-side senses, faithfully classified — not migrated)
65+
66+
[cols="2,3",options="header"]
67+
|===
68+
| File | Why no integer brain
69+
| `Call.res` | Pure orchestration: runs the body instructions forward / reversed-and-inverted. No value transform.
70+
| `CoprocessorCall.res` | *Tombstone* — never implemented; superseded by terminal SEND/RECV + VM Tier-4 Send/Recv (see the file's own header). Nothing to migrate.
71+
| `State.res`, `VmState.res` | The state container itself (the senses): `dict<int>` slot accessors + serialise (string-gated). No brain.
72+
| `SubroutineRegistry.res` | name -> `array<Instruction.t>` registry; orchestration container.
73+
| `VmStateCoprocessor.res`, `InstructionCoprocessor.res` | Coprocessor bridges — host-side dispatch; the integer cores they call are the already-migrated opcode brains.
74+
| `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.
75+
|===
76+
77+
== Gate detail
78+
79+
* *G1 compile* — `main.exe compile <k>.affine -o <k>.wasm` → WASM for all 4
80+
(VmMemory 346 B, VmStack 243 B, VmPort 508 B, VmControl 299 B).
81+
* *G2 parity* — `parity.mjs <k>.config.mjs` → 1568/1568 over the i32 domain
82+
`{INT_MIN, -1e6, -7, -1, 0, 1, 7, 1e6, INT_MAX}` (Cartesian per arity). Each
83+
oracle independently re-derives the original `.res` value transform.
84+
* *G3 boundary* — n/a for all 4. These are numeric transforms / branch
85+
predicates with no discrete value↔integer encoding table; the G2 round-trip
86+
against the independent oracle is the faithfulness check (same disposition as
87+
the wave-1/2a value-transform kernels).
88+
* *G4 assail* — 0 findings across all 4. Predicates use boolean fall-through
89+
(`if cond { 1 } else { 0 }`) and the LOOP guard uses an out-of-band `return 0`
90+
on the `exit_val == 0` early exit; there is no enum decoder, so PA-AFF-001
91+
does not apply.
92+
93+
== Cluster C2 — COMPLETE
94+
95+
With wave 1 (Add/Sub/Negate/Noop/Swap/Flip/Xor/Rol/Ror/And/Or + Instruction
96+
taxonomy), wave 2a (Mul/Div), and wave 2b (Load/Store/Push/Pop/Recv/Send/IfPos/
97+
IfZero/Loop), every reversible-VM opcode with a separable integer brain is
98+
migrated and four-gate verified. The remaining C2 files (Call, CoprocessorCall,
99+
State, VmState, VM, SubroutineRegistry, VmStateCoprocessor, InstructionCoprocessor)
100+
are host-side senses / orchestration with no integer brain, classified above.
101+
*No array/linear-memory ABI was required* — that blocker was an artefact of the
102+
coarse triage bucket, dissolved by reading the sources. (The string wall remains
103+
a separate, genuine compiler gate for the STRING-GATED clusters.)
Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
// SPDX-License-Identifier: AGPL-3.0-or-later
2+
//
3+
// VmControl -- the control-flow opcodes IF_POS/IF_ZERO/LOOP of the idaptik VM,
4+
// the pure-integer core from vm/lib/ocaml/{IfPos,IfZero,Loop}.res. The branch
5+
// bodies are arrays of sub-instructions run by the host orchestrator (the
6+
// senses); the brain is only the scalar BRANCH PREDICATE that selects a branch
7+
// (and, for LOOP, the iteration counter + bound check). Janus reversibility
8+
// lives in the host: the reverse run applies the SAME predicate to the exit
9+
// register instead of the test register, then runs the chosen branch reversed.
10+
//
11+
// IF_POS take then-branch iff testReg > 0 (reverse: iff exitReg > 0)
12+
// IF_ZERO take then-branch iff testReg == 0 (reverse: iff exitReg == 0)
13+
// LOOP continue iff exitReg != 0 and iterations < maxIterations
14+
// Predicates return 1 (take / continue) or 0 (skip / stop).
15+
16+
// --- IF_POS / IF_ZERO branch predicates (1 = then-branch, 0 = else-branch) ---
17+
pub fn if_pos(v: Int) -> Int { if v > 0 { 1 } else { 0 } }
18+
pub fn if_zero(v: Int) -> Int { if v == 0 { 1 } else { 0 } }
19+
20+
// --- LOOP continuation: 1 = run another iteration, 0 = stop ---
21+
// Continue while the exit register is non-zero AND the iteration cap is unhit.
22+
pub fn loop_continue(exit_val: Int, iters: Int, max_iters: Int) -> Int {
23+
if exit_val == 0 { return 0; }
24+
if iters < max_iters { 1 } else { 0 }
25+
}
26+
// Iteration counter advance (the maxIterations guard counts these).
27+
pub fn loop_iter_next(iters: Int) -> Int { iters + 1 }
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc)
3+
//
4+
// affine-parity config for VmControl.affine (IF_POS/IF_ZERO/LOOP branch
5+
// predicates; scalar i32 ABI). Oracles re-derive vm/lib/ocaml/{IfPos,IfZero,
6+
// Loop}.res predicates. The branch bodies are host-orchestrated; only the
7+
// scalar predicate (1 = take/continue, 0 = skip/stop) crosses the boundary.
8+
const I = { values: [-2147483648, -1000000, -7, -1, 0, 1, 7, 1000000, 2147483647] };
9+
const i32 = (x) => x | 0;
10+
11+
export default {
12+
affine: "VmControl.affine",
13+
cases: [
14+
{ name: "if_pos v>0 -> 1/0", export: "if_pos", args: [I], oracle: (v) => (v > 0 ? 1 : 0) },
15+
{ name: "if_zero v==0 -> 1/0", export: "if_zero", args: [I], oracle: (v) => (v === 0 ? 1 : 0) },
16+
{ 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)) },
17+
{ name: "loop_iter_next iters+1", export: "loop_iter_next", args: [I], oracle: (i) => i32(i + 1) },
18+
],
19+
};
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// SPDX-License-Identifier: AGPL-3.0-or-later
2+
//
3+
// VmMemory -- the additive memory opcodes LOAD/STORE of the idaptik VM, the
4+
// pure-integer core extracted from vm/lib/ocaml/{Load,Store}.res. The VM's
5+
// "memory" is NOT an array in the brain: VmState stores it as string-keyed dict
6+
// entries (`_mem:0`, `_mem:1`, ... 256 slots), so that dict is host-side STATE
7+
// (the senses). The host reads/writes memory[addr]; the brain is only the
8+
// reversible ADDITIVE value transform -- LOAD/STORE therefore need no array ABI.
9+
//
10+
// LOAD execute reg := reg + memory[addr] invert reg := reg - memory[addr]
11+
// STORE execute memory[addr] := memory[addr] + reg invert ... - reg
12+
// Both are additive (non-destructive): the inverse subtracts, so the round-trip
13+
// is exact over i32 wraparound -- the same reason ADD/SUB round-trip.
14+
15+
// --- LOAD: additive load (host supplies memory[addr] as `mem`) ---
16+
pub fn load_fwd(reg: Int, mem: Int) -> Int { reg + mem }
17+
pub fn load_inv(reg: Int, mem: Int) -> Int { reg - mem }
18+
pub fn load_roundtrip(reg: Int, mem: Int) -> Int { load_inv(load_fwd(reg, mem), mem) } // == reg
19+
20+
// --- STORE: additive store (host supplies memory[addr] as `mem`) ---
21+
pub fn store_fwd(mem: Int, reg: Int) -> Int { mem + reg }
22+
pub fn store_inv(mem: Int, reg: Int) -> Int { mem - reg }
23+
pub fn store_roundtrip(mem: Int, reg: Int) -> Int { store_inv(store_fwd(mem, reg), reg) } // == mem
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc)
3+
//
4+
// affine-parity config for VmMemory.affine (additive LOAD/STORE; scalar i32
5+
// ABI). Oracles re-derive vm/lib/ocaml/{Load,Store}.res value transforms
6+
// independently. The memory array is host-side; only the additive value
7+
// transform crosses the boundary. Both sides normalise to i32 (| 0).
8+
const I = { values: [-2147483648, -1000000, -7, -1, 0, 1, 7, 1000000, 2147483647] };
9+
const i32 = (x) => x | 0;
10+
11+
export default {
12+
affine: "VmMemory.affine",
13+
cases: [
14+
{ name: "load_fwd reg+mem", export: "load_fwd", args: [I, I], oracle: (reg, mem) => i32(reg + mem) },
15+
{ name: "load_inv reg-mem", export: "load_inv", args: [I, I], oracle: (reg, mem) => i32(reg - mem) },
16+
{ name: "load_roundtrip == reg", export: "load_roundtrip", args: [I, I], oracle: (reg, mem) => i32(reg) },
17+
{ name: "store_fwd mem+reg", export: "store_fwd", args: [I, I], oracle: (mem, reg) => i32(mem + reg) },
18+
{ name: "store_inv mem-reg", export: "store_inv", args: [I, I], oracle: (mem, reg) => i32(mem - reg) },
19+
{ name: "store_roundtrip == mem", export: "store_roundtrip", args: [I, I], oracle: (mem, reg) => i32(mem) },
20+
],
21+
};
Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
// SPDX-License-Identifier: AGPL-3.0-or-later
2+
//
3+
// VmPort -- the I/O port opcodes RECV/SEND of the idaptik VM, the pure-integer
4+
// core from vm/lib/ocaml/{Recv,Send}.res. The port buffers (`_pin:port`,
5+
// `_pout:port` slots + pointers) are host-side state (the senses); the host
6+
// reads/writes the buffer slot. The brain is the port-POINTER arithmetic plus,
7+
// for RECV, the additive accumulate of the received value -- no array ABI.
8+
//
9+
// RECV execute reg := reg + port_in[ptr]; ptr := ptr + 1
10+
// invert ptr := ptr - 1; reg := reg - port_in[ptr]
11+
// SEND execute port_out[ptr] := reg; ptr := ptr + 1
12+
// invert ptr := ptr - 1; port_out[ptr] := 0
13+
14+
// --- RECV: additive accumulate + input-pointer advance ---
15+
pub fn recv_acc_fwd(reg: Int, val: Int) -> Int { reg + val }
16+
pub fn recv_acc_inv(reg: Int, val: Int) -> Int { reg - val }
17+
pub fn recv_acc_roundtrip(reg: Int, val: Int) -> Int { recv_acc_inv(recv_acc_fwd(reg, val), val) } // == reg
18+
pub fn recv_ptr_fwd(ptr: Int) -> Int { ptr + 1 }
19+
pub fn recv_ptr_inv(ptr: Int) -> Int { ptr - 1 }
20+
pub fn recv_ptr_roundtrip(ptr: Int) -> Int { recv_ptr_inv(recv_ptr_fwd(ptr)) } // == ptr
21+
22+
// --- SEND: output-pointer advance; inverse clears the vacated slot to 0 ---
23+
pub fn send_ptr_fwd(ptr: Int) -> Int { ptr + 1 }
24+
pub fn send_ptr_inv(ptr: Int) -> Int { ptr - 1 }
25+
pub fn send_ptr_roundtrip(ptr: Int) -> Int { send_ptr_inv(send_ptr_fwd(ptr)) } // == ptr
26+
pub fn send_clears_slot() -> Int { 0 }
Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc)
3+
//
4+
// affine-parity config for VmPort.affine (RECV/SEND port pointer + additive
5+
// accumulate; scalar i32 ABI). Oracles re-derive vm/lib/ocaml/{Recv,Send}.res.
6+
// The port buffers + pointers are host-side state; only the pointer arithmetic
7+
// and the additive accumulate cross the boundary. Both sides normalise to i32.
8+
const I = { values: [-2147483648, -1000000, -7, -1, 0, 1, 7, 1000000, 2147483647] };
9+
const i32 = (x) => x | 0;
10+
11+
export default {
12+
affine: "VmPort.affine",
13+
cases: [
14+
{ name: "recv_acc_fwd reg+val", export: "recv_acc_fwd", args: [I, I], oracle: (reg, val) => i32(reg + val) },
15+
{ name: "recv_acc_inv reg-val", export: "recv_acc_inv", args: [I, I], oracle: (reg, val) => i32(reg - val) },
16+
{ name: "recv_acc_roundtrip == reg", export: "recv_acc_roundtrip", args: [I, I], oracle: (reg, val) => i32(reg) },
17+
{ name: "recv_ptr_fwd ptr+1", export: "recv_ptr_fwd", args: [I], oracle: (ptr) => i32(ptr + 1) },
18+
{ name: "recv_ptr_inv ptr-1", export: "recv_ptr_inv", args: [I], oracle: (ptr) => i32(ptr - 1) },
19+
{ name: "recv_ptr_roundtrip == ptr", export: "recv_ptr_roundtrip", args: [I], oracle: (ptr) => i32(ptr) },
20+
{ name: "send_ptr_fwd ptr+1", export: "send_ptr_fwd", args: [I], oracle: (ptr) => i32(ptr + 1) },
21+
{ name: "send_ptr_inv ptr-1", export: "send_ptr_inv", args: [I], oracle: (ptr) => i32(ptr - 1) },
22+
{ name: "send_ptr_roundtrip == ptr", export: "send_ptr_roundtrip", args: [I], oracle: (ptr) => i32(ptr) },
23+
{ name: "send_clears_slot == 0", export: "send_clears_slot", args: [], oracle: () => 0 },
24+
],
25+
};

0 commit comments

Comments
 (0)