diff --git a/.github/workflows/build-release.yml b/.github/workflows/build-release.yml
index 1e3ba4c..a7e1176 100644
--- a/.github/workflows/build-release.yml
+++ b/.github/workflows/build-release.yml
@@ -139,6 +139,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/secp256k1/guest.cs             --os linux --arch riscv64 --libc openvm --stdlib dotnet             --no-pie --no-pthread -Ot             --extlib "$PWD/bflat-openvm/output/libopenvm.bflat.manifest"             -o secp256k1-guest
 
       - name: Upload the linked guests
@@ -149,6 +155,7 @@ jobs:
           name: integration-guest
           path: |
             guest
+            u256
             secp256k1-guest
 
       - name: Check the linked image
@@ -161,6 +168,36 @@ 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 444 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=0000000000000000bc0100000000000000000000000000000000000000000000" ] \
+            || { echo "::error::u256 vectors failed: $out"; exit 1; }
+
   run-secp256k1-guest:
     # The host test emulates the chips' preconditions; this runs the recovery
     # on OpenVM itself, against the same reference, adversarial vectors
@@ -208,7 +245,7 @@ jobs:
 
   build-nupkg:
     name: Build NuGet package
-    needs: [build-libopenvm, run-divrem-vectors, run-secp256k1-guest]
+    needs: [build-libopenvm, run-divrem-vectors, run-secp256k1-guest, run-u256-vectors]
     runs-on: ubuntu-latest
     permissions:
       contents: read
diff --git a/README.md b/README.md
index dc6b57e..2b30b5b 100644
--- a/README.md
+++ b/README.md
@@ -70,7 +70,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, out of place and over either operand.
 
 `zkvm_secp256k1_ecrecover` is ours rather than openvm-eth's, so it is also
 tested for results: `tests/secp256k1/test_ecrecover.py` diffs a host build of
diff --git a/tests/integration/u256.cs b/tests/integration/u256.cs
new file mode 100644
index 0000000..5da974b
--- /dev/null
+++ b/tests/integration/u256.cs
@@ -0,0 +1,571 @@
+// 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 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.
+//
+// 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;
+                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);
+                Load(v, a, b, r);
+                U256.Run(v[0], b, a, b);
+                mismatches += Differs(b, expected);
+                checks += 3;
+            }
+        }
+
+        U256.Publish(mismatches, checks);
+        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;
+}