From d00ddca1a578f36970d405a8a7c98a54cf0f0a9e Mon Sep 17 00:00:00 2001
From: "lukasz.rozmej" <lukasz.rozmej@gmail.com>
Date: Wed, 7 Oct 2026 14:37:50 +0200
Subject: [PATCH 1/3] test: execute the u256 intrinsics against vectors on the
 OpenVM runner

guest.cs only links the zkvm_u256_* shims. u256.cs runs each of the eleven
against precomputed results, out of place and with the result over the first
operand, and CI asserts zero mismatches over 296 checks on the pinned runner.
---
 .github/workflows/build-release.yml |  34 +-
 README.md                           |   4 +-
 tests/integration/u256.cs           | 564 ++++++++++++++++++++++++++++
 3 files changed, 600 insertions(+), 2 deletions(-)
 create mode 100644 tests/integration/u256.cs

diff --git a/.github/workflows/build-release.yml b/.github/workflows/build-release.yml
index 0be5991..34bce89 100644
--- a/.github/workflows/build-release.yml
+++ b/.github/workflows/build-release.yml
@@ -131,6 +131,7 @@ jobs:
             -o guest
           riscv64-linux-gnu-readelf -h guest | grep -E 'Class:|Machine:|Entry point'
           ls -la guest
+          bflat-riscv64/src/bflat/bin/Debug/net10.0/bflat build             bflat-openvm/tests/integration/u256.cs             --os linux --arch riscv64 --libc openvm --stdlib dotnet             --no-pie --no-pthread -Ot             --extlib "$PWD/bflat-openvm/output/libopenvm.bflat.manifest"             -o u256
 
       - name: Upload the linked guest
         # Keeping the image makes an "N instructions the VM cannot decode"
@@ -138,7 +139,9 @@ jobs:
         uses: actions/upload-artifact@v4
         with:
           name: integration-guest
-          path: guest
+          path: |
+            guest
+            u256
 
       - name: Check the linked image
         # --no-atomics is now enforced: bflat's nothread module displaces the
@@ -150,6 +153,35 @@ jobs:
         run: |
           python3 bflat-openvm/tests/integration/check_image.py guest --require-custom --no-atomics
 
+  run-u256-vectors:
+    # guest.cs only links the u256 shims; this executes them. A wrong funct7 or
+    # register order in openvm_intrinsics.S links fine and computes the wrong
+    # thing, so the vector guest runs on the OpenVM runner and must report zero
+    # mismatches over its 296 checks.
+    name: Run the u256 vectors on OpenVM
+    needs: link-guest
+    runs-on: ubuntu-latest
+    env:
+      OPENVM_IMAGE: nethermindeth/openvm-runner:v2.1.0-rv64@sha256:d8209a5db5d59df6d6f5899b2ce6866f81c30bdc3df952dc78243b8316706baa
+    steps:
+      - name: Check out repository
+        uses: actions/checkout@v7
+
+      - name: Download the linked guests
+        uses: actions/download-artifact@v4
+        with:
+          name: integration-guest
+          path: guests
+
+      - name: Execute the vector guest
+        run: |
+          cp runner/openvm.toml guests/
+          : > guests/empty.raw
+          out=$(docker run --rm -v "$PWD/guests:/n" "$OPENVM_IMAGE" /n/u256 /n/openvm.toml /n/empty.raw | tail -1)
+          echo "$out"
+          # Mismatches, then checks, as little-endian u64s.
+          [ "$out" = "public_values=0000000000000000280100000000000000000000000000000000000000000000" ]             || { echo "::error::u256 vectors failed: $out"; exit 1; }
+
   build-nupkg:
     name: Build NuGet package
     needs: build-libopenvm
diff --git a/README.md b/README.md
index b991459..1d5bf74 100644
--- a/README.md
+++ b/README.md
@@ -69,7 +69,9 @@ All 19 accelerators, plus both IO entry points:
 custom-0 and custom-1 instructions to catch a silent fallback to portable Rust.
 CI then links a real bflat guest that calls all 21 through direct P/Invoke
 (`tests/integration/guest.cs`) — which is what proves the symbols not only
-exist but survive a guest's link.
+exist but survive a guest's link. The 256-bit integer shims are also executed:
+`tests/integration/u256.cs` runs each against precomputed vectors on the
+OpenVM runner, in place and out of place.
 
 ## The output window is 32 bytes
 
diff --git a/tests/integration/u256.cs b/tests/integration/u256.cs
new file mode 100644
index 0000000..8af6226
--- /dev/null
+++ b/tests/integration/u256.cs
@@ -0,0 +1,564 @@
+// u256 vector guest: runs every zkvm_u256_* shim in openvm_intrinsics.S against
+// precomputed results, on the OpenVM runner rather than only linking.
+//
+// guest.cs proves the symbols link; it never executes them, so a wrong funct7,
+// a swapped register or a misread operand would still pass there. This guest
+// executes each shim and compares limb for limb. Every operation also runs once
+// more with the result written over its first operand, the in-place form a
+// caller uses on a stack slot, which only holds if the instruction reads both
+// operands before it writes.
+//
+// The public output is 32 bytes: the number of mismatches, then the number of
+// checks, each a little-endian u64, then zeros. CI asserts zero mismatches.
+//
+// Semantics, from OpenVM's bigint circuit on the rv64 line: add, sub and mul wrap
+// modulo 2^256; the shifts take their count from the low byte of the second
+// operand, so a count of 256 shifts by 0; slt and sltu write 1 or 0.
+
+using System.Runtime.InteropServices;
+
+internal static unsafe class U256
+{
+    [DllImport("__Internal")] private static extern void zkvm_u256_add(ulong* r, ulong* a, ulong* b);
+    [DllImport("__Internal")] private static extern void zkvm_u256_sub(ulong* r, ulong* a, ulong* b);
+    [DllImport("__Internal")] private static extern void zkvm_u256_xor(ulong* r, ulong* a, ulong* b);
+    [DllImport("__Internal")] private static extern void zkvm_u256_or(ulong* r, ulong* a, ulong* b);
+    [DllImport("__Internal")] private static extern void zkvm_u256_and(ulong* r, ulong* a, ulong* b);
+    [DllImport("__Internal")] private static extern void zkvm_u256_sll(ulong* r, ulong* a, ulong* b);
+    [DllImport("__Internal")] private static extern void zkvm_u256_srl(ulong* r, ulong* a, ulong* b);
+    [DllImport("__Internal")] private static extern void zkvm_u256_sra(ulong* r, ulong* a, ulong* b);
+    [DllImport("__Internal")] private static extern void zkvm_u256_slt(ulong* r, ulong* a, ulong* b);
+    [DllImport("__Internal")] private static extern void zkvm_u256_sltu(ulong* r, ulong* a, ulong* b);
+    [DllImport("__Internal")] private static extern void zkvm_u256_mul(ulong* r, ulong* a, ulong* b);
+    [DllImport("__Internal")] private static extern void write_output(ulong* output, nuint size);
+
+    internal static void Run(ulong op, ulong* r, ulong* a, ulong* b)
+    {
+        switch (op)
+        {
+            case 0: zkvm_u256_add(r, a, b); break;
+            case 1: zkvm_u256_sub(r, a, b); break;
+            case 2: zkvm_u256_xor(r, a, b); break;
+            case 3: zkvm_u256_or(r, a, b); break;
+            case 4: zkvm_u256_and(r, a, b); break;
+            case 5: zkvm_u256_sll(r, a, b); break;
+            case 6: zkvm_u256_srl(r, a, b); break;
+            case 7: zkvm_u256_sra(r, a, b); break;
+            case 8: zkvm_u256_slt(r, a, b); break;
+            case 9: zkvm_u256_sltu(r, a, b); break;
+            case 10: zkvm_u256_mul(r, a, b); break;
+        }
+    }
+
+    internal static void Publish(ulong mismatches, ulong checks)
+    {
+        // ulong locals keep the buffer 8-byte aligned, as the output window requires.
+        ulong* output = stackalloc ulong[4];
+        output[0] = mismatches;
+        output[1] = checks;
+        output[2] = 0;
+        output[3] = 0;
+        write_output(output, 32);
+    }
+}
+
+internal static unsafe class Program
+{
+    private const int Row = 13;
+
+    // Each row: the operation (index into U256.Run), a, b and the expected result,
+    // each operand four little-endian u64 limbs. Generated with Python's integers.
+    private static readonly ulong[] Vectors =
+    [
+        // add
+        0, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        0, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        0, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xfffffffffffffffe, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        0, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        0, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x88b9eb1c4d7eafdf, 0x8787878787878787, 0xefbe8d5c2af9c897, 0x0000000000000000,
+        0, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x88b9eb1c4d7eafdf, 0x8787878787878787, 0xefbe8d5c2af9c897, 0x0000000000000000,
+        0, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+        0, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000002, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        0, 0xffffffffffffffff, 0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000001, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000002, 0x0000000000000000,
+        0, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000007, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8796a5b4c3d2e1f7, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+        0, 0x0000000000000003, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000002, 0x0000000000000002, 0x0000000000000000, 0x0000000000000000,
+        // sub
+        1, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        1, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000002, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        1, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        1, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        1, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x8673604d3a271401, 0x96b4d2f10f2d4b69, 0x0dfae7d4c1ae9b88, 0x02468acf13579bdf,
+        1, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x798c9fb2c5d8ebff, 0x694b2d0ef0d2b496, 0xf205182b3e516477, 0xfdb97530eca86420,
+        1, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0x7fffffffffffffff,
+        1, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000002, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xfffffffffffffffd, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        1, 0xffffffffffffffff, 0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000001, 0x0000000000000000,
+            0xfffffffffffffffe, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        1, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000007, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8796a5b4c3d2e1e9, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+        1, 0x0000000000000003, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000004, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        // xor
+        2, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        2, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xfffffffffffffffe, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        2, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        2, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        2, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x86b5e0d34a792c1f, 0x7777777777777777, 0x0e3d685bc2f1a497, 0xffffffffffffffff,
+        2, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x86b5e0d34a792c1f, 0x7777777777777777, 0x0e3d685bc2f1a497, 0xffffffffffffffff,
+        2, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+        2, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000002, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xfffffffffffffffd, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        2, 0xffffffffffffffff, 0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000001, 0x0000000000000000,
+            0xfffffffffffffffe, 0xffffffffffffffff, 0x0000000000000001, 0x0000000000000000,
+        2, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000007, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8796a5b4c3d2e1f7, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+        2, 0x0000000000000003, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xfffffffffffffffc, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000,
+        // or
+        3, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        3, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        3, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        3, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+        3, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x87b7e5f7cbfbedff, 0x7f7f7f7f7f7f7f7f, 0xfefdfadbf6f5b697, 0xffffffffffffffff,
+        3, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x87b7e5f7cbfbedff, 0x7f7f7f7f7f7f7f7f, 0xfefdfadbf6f5b697, 0xffffffffffffffff,
+        3, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+        3, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000002, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        3, 0xffffffffffffffff, 0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000001, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0x0000000000000001, 0x0000000000000000,
+        3, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000007, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8796a5b4c3d2e1f7, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+        3, 0x0000000000000003, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000,
+        // and
+        4, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        4, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        4, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        4, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+        4, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x010205248182c1e0, 0x0808080808080808, 0xf0c0928034041200, 0x0000000000000000,
+        4, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x010205248182c1e0, 0x0808080808080808, 0xf0c0928034041200, 0x0000000000000000,
+        4, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        4, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000002, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000002, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        4, 0xffffffffffffffff, 0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000001, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        4, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000007, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        4, 0x0000000000000003, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000003, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        // sll
+        5, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+        5, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0f2d4b6987a5c3e0, 0x1e3c5a7896b4d2f1, 0xfdb97530eca86420, 0x02468acf13579bdf,
+        5, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x000000000000003f, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x43cb52da61e970f8, 0x078f169e25ad34bc, 0xff6e5d4c3b2a1908,
+        5, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000040, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210,
+        5, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000041, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0f2d4b6987a5c3e0, 0x1e3c5a7896b4d2f1, 0xfdb97530eca86420,
+        5, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000080, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978,
+        5, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x00000000000000ff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        5, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000100, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+        5, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x000000000000012c, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x2e1f000000000000, 0xa69788796a5b4c3d, 0x432100f1e2d3c4b5, 0xbcdeffedcba98765,
+        5, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        5, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+        5, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x02468acf13579bde, 0xf0d2b496785a3c1e, 0xe1c3a587694b2d0e, 0xfdb97530eca86421,
+        5, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x000000000000003f, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8000000000000000, 0x8091a2b3c4d5e6f7, 0xbc34ad259e168f07, 0x7870e961da52cb43,
+        5, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000040, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687,
+        5, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000041, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x02468acf13579bde, 0xf0d2b496785a3c1e, 0xe1c3a587694b2d0e,
+        5, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000080, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0123456789abcdef, 0x78695a4b3c2d1e0f,
+        5, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x00000000000000ff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+        5, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000100, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+        5, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x000000000000012c, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xbcdef00000000000, 0xd1e0f0123456789a, 0x5968778695a4b3c2, 0x43210f0e1d2c3b4a,
+        5, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+        // srl
+        6, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+        6, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x43cb52da61e970f8, 0x078f169e25ad34bc, 0xff6e5d4c3b2a1908, 0x0091a2b3c4d5e6f7,
+        6, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x000000000000003f, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x1e3c5a7896b4d2f1, 0xfdb97530eca86420, 0x02468acf13579bdf, 0x0000000000000000,
+        6, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000040, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef, 0x0000000000000000,
+        6, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000041, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x078f169e25ad34bc, 0xff6e5d4c3b2a1908, 0x0091a2b3c4d5e6f7, 0x0000000000000000,
+        6, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000080, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xfedcba9876543210, 0x0123456789abcdef, 0x0000000000000000, 0x0000000000000000,
+        6, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x00000000000000ff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        6, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000100, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+        6, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x000000000000012c, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xd3c4b5a69788796a, 0xa98765432100f1e2, 0x56789abcdeffedcb, 0x0000000000001234,
+        6, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        6, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+        6, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8091a2b3c4d5e6f7, 0xbc34ad259e168f07, 0x7870e961da52cb43, 0x7f6e5d4c3b2a1908,
+        6, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x000000000000003f, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xf0d2b496785a3c1e, 0xe1c3a587694b2d0e, 0xfdb97530eca86421, 0x0000000000000001,
+        6, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000040, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210, 0x0000000000000000,
+        6, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000041, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xbc34ad259e168f07, 0x7870e961da52cb43, 0x7f6e5d4c3b2a1908, 0x0000000000000000,
+        6, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000080, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xf0e1d2c3b4a59687, 0xfedcba9876543210, 0x0000000000000000, 0x0000000000000000,
+        6, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x00000000000000ff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        6, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000100, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+        6, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x000000000000012c, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xa4b3c2d1e0f01234, 0x2c3b4a5968778695, 0xa9876543210f0e1d, 0x00000000000fedcb,
+        6, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        // sra
+        7, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+        7, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x43cb52da61e970f8, 0x078f169e25ad34bc, 0xff6e5d4c3b2a1908, 0x0091a2b3c4d5e6f7,
+        7, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x000000000000003f, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x1e3c5a7896b4d2f1, 0xfdb97530eca86420, 0x02468acf13579bdf, 0x0000000000000000,
+        7, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000040, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef, 0x0000000000000000,
+        7, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000041, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x078f169e25ad34bc, 0xff6e5d4c3b2a1908, 0x0091a2b3c4d5e6f7, 0x0000000000000000,
+        7, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000080, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xfedcba9876543210, 0x0123456789abcdef, 0x0000000000000000, 0x0000000000000000,
+        7, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x00000000000000ff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        7, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000100, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+        7, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x000000000000012c, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xd3c4b5a69788796a, 0xa98765432100f1e2, 0x56789abcdeffedcb, 0x0000000000001234,
+        7, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        7, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+        7, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x8091a2b3c4d5e6f7, 0xbc34ad259e168f07, 0x7870e961da52cb43, 0xff6e5d4c3b2a1908,
+        7, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x000000000000003f, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xf0d2b496785a3c1e, 0xe1c3a587694b2d0e, 0xfdb97530eca86421, 0xffffffffffffffff,
+        7, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000040, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210, 0xffffffffffffffff,
+        7, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000041, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xbc34ad259e168f07, 0x7870e961da52cb43, 0xff6e5d4c3b2a1908, 0xffffffffffffffff,
+        7, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000080, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xf0e1d2c3b4a59687, 0xfedcba9876543210, 0xffffffffffffffff, 0xffffffffffffffff,
+        7, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x00000000000000ff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        7, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000100, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+        7, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x000000000000012c, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xa4b3c2d1e0f01234, 0x2c3b4a5968778695, 0xa9876543210f0e1d, 0xffffffffffffedcb,
+        7, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        // slt
+        8, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        8, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        8, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        8, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        8, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        8, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        8, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        8, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000002, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        8, 0xffffffffffffffff, 0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000001, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        8, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000007, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        8, 0x0000000000000003, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        // sltu
+        9, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        9, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        9, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        9, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        9, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        9, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        9, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        9, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000002, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        9, 0xffffffffffffffff, 0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000001, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        9, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000007, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        9, 0x0000000000000003, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        // mul
+        10, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        10, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        10, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        10, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+        10, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x196fb4e90c1e1f10, 0x1c6096a05fb686b2, 0xa9d0780af39c6fd8, 0x5cba6e860e13a3ca,
+        10, 0x0123456789abcdef, 0x78695a4b3c2d1e0f, 0xf0e1d2c3b4a59687, 0xfedcba9876543210,
+            0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x196fb4e90c1e1f10, 0x1c6096a05fb686b2, 0xa9d0780af39c6fd8, 0x5cba6e860e13a3ca,
+        10, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x8000000000000000,
+        10, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+            0x0000000000000002, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xfffffffffffffffe, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        10, 0xffffffffffffffff, 0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000,
+            0x0000000000000001, 0x0000000000000000, 0x0000000000000001, 0x0000000000000000,
+            0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff, 0xffffffffffffffff,
+        10, 0x8796a5b4c3d2e1f0, 0x0f1e2d3c4b5a6978, 0xfedcba9876543210, 0x0123456789abcdef,
+            0x0000000000000007, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xb51e87f15ac42d90, 0x69d33ca60f78e24b, 0xf8091a2b3c4d5e70, 0x07f6e5d4c3b2a18f,
+        10, 0x0000000000000003, 0x0000000000000001, 0x0000000000000000, 0x0000000000000000,
+            0xffffffffffffffff, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000,
+            0xfffffffffffffffd, 0x0000000000000001, 0x0000000000000001, 0x0000000000000000,
+    ];
+
+    private static int Main()
+    {
+        ulong mismatches = 0;
+        ulong checks = 0;
+        ulong* a = stackalloc ulong[4];
+        ulong* b = stackalloc ulong[4];
+        ulong* r = stackalloc ulong[4];
+        fixed (ulong* vectors = Vectors)
+        {
+            for (int row = 0; row < Vectors.Length; row += Row)
+            {
+                ulong* v = vectors + row;
+                ulong* expected = v + 9;
+                for (int i = 0; i < 4; i++)
+                {
+                    a[i] = v[1 + i];
+                    b[i] = v[5 + i];
+                    r[i] = 0xdeadbeefdeadbeefUL;
+                }
+
+                U256.Run(v[0], r, a, b);
+                mismatches += Differs(r, expected);
+                U256.Run(v[0], a, a, b);
+                mismatches += Differs(a, expected);
+                checks += 2;
+            }
+        }
+
+        U256.Publish(mismatches, checks);
+        return 0;
+    }
+
+    private static ulong Differs(ulong* actual, ulong* expected) =>
+        (actual[0] ^ expected[0] | actual[1] ^ expected[1] | actual[2] ^ expected[2] | actual[3] ^ expected[3]) == 0 ? 0UL : 1UL;
+}

From 26e16d42da7a8d3c3e387cedb654ba2c0f68a200 Mon Sep 17 00:00:00 2001
From: "lukasz.rozmej" <lukasz.rozmej@gmail.com>
Date: Wed, 7 Oct 2026 14:45:20 +0200
Subject: [PATCH 2/3] test: check the u256 shims with the result over either
 operand

Also restores the line continuations in the workflow step.
---
 .github/workflows/build-release.yml | 12 ++++++++---
 README.md                           |  2 +-
 tests/integration/u256.cs           | 31 ++++++++++++++++++-----------
 3 files changed, 29 insertions(+), 16 deletions(-)

diff --git a/.github/workflows/build-release.yml b/.github/workflows/build-release.yml
index 34bce89..a212f81 100644
--- a/.github/workflows/build-release.yml
+++ b/.github/workflows/build-release.yml
@@ -131,7 +131,12 @@ jobs:
             -o guest
           riscv64-linux-gnu-readelf -h guest | grep -E 'Class:|Machine:|Entry point'
           ls -la guest
-          bflat-riscv64/src/bflat/bin/Debug/net10.0/bflat build             bflat-openvm/tests/integration/u256.cs             --os linux --arch riscv64 --libc openvm --stdlib dotnet             --no-pie --no-pthread -Ot             --extlib "$PWD/bflat-openvm/output/libopenvm.bflat.manifest"             -o u256
+          bflat-riscv64/src/bflat/bin/Debug/net10.0/bflat build \
+            bflat-openvm/tests/integration/u256.cs \
+            --os linux --arch riscv64 --libc openvm --stdlib dotnet \
+            --no-pie --no-pthread -Ot \
+            --extlib "$PWD/bflat-openvm/output/libopenvm.bflat.manifest" \
+            -o u256
 
       - name: Upload the linked guest
         # Keeping the image makes an "N instructions the VM cannot decode"
@@ -157,7 +162,7 @@ jobs:
     # guest.cs only links the u256 shims; this executes them. A wrong funct7 or
     # register order in openvm_intrinsics.S links fine and computes the wrong
     # thing, so the vector guest runs on the OpenVM runner and must report zero
-    # mismatches over its 296 checks.
+    # mismatches over its 444 checks.
     name: Run the u256 vectors on OpenVM
     needs: link-guest
     runs-on: ubuntu-latest
@@ -180,7 +185,8 @@ jobs:
           out=$(docker run --rm -v "$PWD/guests:/n" "$OPENVM_IMAGE" /n/u256 /n/openvm.toml /n/empty.raw | tail -1)
           echo "$out"
           # Mismatches, then checks, as little-endian u64s.
-          [ "$out" = "public_values=0000000000000000280100000000000000000000000000000000000000000000" ]             || { echo "::error::u256 vectors failed: $out"; exit 1; }
+          [ "$out" = "public_values=0000000000000000bc0100000000000000000000000000000000000000000000" ] \
+            || { echo "::error::u256 vectors failed: $out"; exit 1; }
 
   build-nupkg:
     name: Build NuGet package
diff --git a/README.md b/README.md
index 1d5bf74..6aab325 100644
--- a/README.md
+++ b/README.md
@@ -71,7 +71,7 @@ CI then links a real bflat guest that calls all 21 through direct P/Invoke
 (`tests/integration/guest.cs`) — which is what proves the symbols not only
 exist but survive a guest's link. The 256-bit integer shims are also executed:
 `tests/integration/u256.cs` runs each against precomputed vectors on the
-OpenVM runner, in place and out of place.
+OpenVM runner, out of place and over either operand.
 
 ## The output window is 32 bytes
 
diff --git a/tests/integration/u256.cs b/tests/integration/u256.cs
index 8af6226..5da974b 100644
--- a/tests/integration/u256.cs
+++ b/tests/integration/u256.cs
@@ -3,10 +3,10 @@
 //
 // guest.cs proves the symbols link; it never executes them, so a wrong funct7,
 // a swapped register or a misread operand would still pass there. This guest
-// executes each shim and compares limb for limb. Every operation also runs once
-// more with the result written over its first operand, the in-place form a
-// caller uses on a stack slot, which only holds if the instruction reads both
-// operands before it writes.
+// executes each shim and compares limb for limb. Every operation also runs with
+// the result written over its first operand and over its second, the in-place
+// forms a caller uses on a stack slot, which only hold if the instruction reads
+// both operands before it writes.
 //
 // The public output is 32 bytes: the number of mismatches, then the number of
 // checks, each a little-endian u64, then zeros. CI asserts zero mismatches.
@@ -540,18 +540,15 @@ private static int Main()
             {
                 ulong* v = vectors + row;
                 ulong* expected = v + 9;
-                for (int i = 0; i < 4; i++)
-                {
-                    a[i] = v[1 + i];
-                    b[i] = v[5 + i];
-                    r[i] = 0xdeadbeefdeadbeefUL;
-                }
-
+                Load(v, a, b, r);
                 U256.Run(v[0], r, a, b);
                 mismatches += Differs(r, expected);
                 U256.Run(v[0], a, a, b);
                 mismatches += Differs(a, expected);
-                checks += 2;
+                Load(v, a, b, r);
+                U256.Run(v[0], b, a, b);
+                mismatches += Differs(b, expected);
+                checks += 3;
             }
         }
 
@@ -559,6 +556,16 @@ private static int Main()
         return 0;
     }
 
+    private static void Load(ulong* row, ulong* a, ulong* b, ulong* r)
+    {
+        for (int i = 0; i < 4; i++)
+        {
+            a[i] = row[1 + i];
+            b[i] = row[5 + i];
+            r[i] = 0xdeadbeefdeadbeefUL;
+        }
+    }
+
     private static ulong Differs(ulong* actual, ulong* expected) =>
         (actual[0] ^ expected[0] | actual[1] ^ expected[1] | actual[2] ^ expected[2] | actual[3] ^ expected[3]) == 0 ? 0UL : 1UL;
 }

From 628fbc7b8f435a93bb2b734540184e0f43c29363 Mon Sep 17 00:00:00 2001
From: "lukasz.rozmej" <lukasz.rozmej@gmail.com>
Date: Mon, 12 Oct 2026 18:54:41 +0200
Subject: [PATCH 3/3] ci: gate package publication on u256 execution tests

---
 .github/workflows/build-release.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build-release.yml b/.github/workflows/build-release.yml
index a212f81..984be48 100644
--- a/.github/workflows/build-release.yml
+++ b/.github/workflows/build-release.yml
@@ -190,7 +190,7 @@ jobs:
 
   build-nupkg:
     name: Build NuGet package
-    needs: build-libopenvm
+    needs: run-u256-vectors
     runs-on: ubuntu-latest
     permissions:
       contents: read