test with 16 bit limbs

powdr-labs · Aug 12, 2024 · 1e834a2 · 1e834a2
1 parent fae5bc1
commit 1e834a2
Show file tree

Hide file tree

Showing 3 changed files with 110 additions and 15 deletions.
diff --git a/std/machines/binary_bb.asm b/std/machines/binary_bb.asm
@@ -32,7 +32,7 @@ machine ByteBinary with
     };
 }
 
-machine Binary(byte_binary: ByteBinary) with
+machine Binary8(byte_binary: ByteBinary) with
     latch: latch,
     operation_id: operation_id,
     // Allow this machine to be connected via a permutation
@@ -48,18 +48,40 @@ machine Binary(byte_binary: ByteBinary) with
 
     col fixed latch(i) { 1 };
 
-    col witness A1;
-    col witness A2;
-    col witness A3;
-    col witness A4;
-    col witness B1;
-    col witness B2;
-    col witness B3;
-    col witness B4;
-    col witness C1;
-    col witness C2;
-    col witness C3;
-    col witness C4;
+    col witness A1, A2, A3, A4;
+    col witness B1, B2, B3, B4;
+    col witness C1, C2, C3, C4;
+
+    link => C1 = byte_binary.run(operation_id, A1, B1);
+    link => C2 = byte_binary.run(operation_id, A2, B2);
+    link => C3 = byte_binary.run(operation_id, A3, B3);
+    link => C4 = byte_binary.run(operation_id, A4, B4);
+}
+
+machine Binary16(byte_binary: ByteBinary) with
+    latch: latch,
+    operation_id: operation_id,
+    // Allow this machine to be connected via a permutation
+    call_selectors: sel,
+{
+    operation and<0> I1, I2, I3, I4 -> O1, O2;
+    operation or<1> I1, I2, I3, I4 -> O1, O2;
+    operation xor<2> I1, I2, I3, I4 -> O1, O2;
+
+    col witness operation_id;
+
+    col fixed latch(i) { 1 };
+
+    let I1: inter = A1 + 256 * A2;
+    let I2: inter = A3 + 256 * A4;
+    let I3: inter = B1 + 256 * B2;
+    let I4: inter = B3 + 256 * B4;
+    let O1: inter = C1 + 256 * C2;
+    let O2: inter = C3 + 256 * C4;
+
+    col witness A1, A2, A3, A4;
+    col witness B1, B2, B3, B4;
+    col witness C1, C2, C3, C4;
 
     link => C1 = byte_binary.run(operation_id, A1, B1);
     link => C2 = byte_binary.run(operation_id, A2, B2);

diff --git a/test_data/std/binary_bb_test_16.asm b/test_data/std/binary_bb_test_16.asm
@@ -0,0 +1,73 @@
+use std::machines::binary_bb::ByteBinary;
+use std::machines::binary_bb::Binary16;
+
+machine Main with degree: 196608 {
+    reg pc[@pc];
+    reg X0_1[<=];
+    reg X0_2[<=];
+    reg X1_1[<=];
+    reg X1_2[<=];
+    reg X2_1[<=];
+    reg X2_2[<=];
+    reg A1;
+    reg A2;
+
+    ByteBinary byte_binary;
+    Binary16 binary(byte_binary);
+
+    instr and X0_1, X0_2, X1_1, X1_2 -> X2_1, X2_2 link ~> (X2_1, X2_2) = binary.and(X0_1, X0_2, X1_1, X1_2);
+    instr or X0_1, X0_2, X1_1, X1_2 -> X2_1, X2_2 link ~> (X2_1, X2_2) = binary.or(X0_1, X0_2, X1_1, X1_2);
+    instr xor X0_1, X0_2, X1_1, X1_2 -> X2_1, X2_2 link ~> (X2_1, X2_2) = binary.xor(X0_1, X0_2, X1_1, X1_2);
+
+    instr assert_eq X0_1, X0_2, X1_1, X1_2 {
+        X0_1 = X1_1,
+        X0_2 = X1_2
+    }
+
+    function main {
+
+        // AND
+        A1, A2 <== and(0, 0, 0, 0);
+        assert_eq A1, A2, 0, 0;
+        A1, A2 <== and(0xffff, 0xffff, 0xffff, 0xffff);
+        assert_eq A1, A2, 0xffff, 0xffff;
+        A1, A2 <== and(0xffff, 0xffff, 0xabcd, 0xef01);
+        assert_eq A1, A2, 0xabcd, 0xef01;
+        A1, A2 <== and(0xabcd, 0xef01, 0xffff, 0xffff);
+        assert_eq A1, A2, 0xabcd, 0xef01;
+        A1, A2 <== and(0, 0, 0xabcd, 0xef01);
+        assert_eq A1, A2, 0, 0;
+        A1, A2 <== and(0xabcd, 0xef01, 0, 0);
+        assert_eq A1, A2, 0, 0;
+
+        // OR
+        A1, A2 <== or(0, 0, 0, 0);
+        assert_eq A1, A2, 0, 0;
+        A1, A2 <== or(0xffff, 0xffff, 0xffff, 0xffff);
+        assert_eq A1, A2, 0xffff, 0xffff;
+        A1, A2 <== or(0xffff, 0xffff, 0xabcd, 0xef01);
+        assert_eq A1, A2, 0xffff, 0xffff;
+        A1, A2 <== or(0xabcd, 0xef01, 0xffff, 0xffff);
+        assert_eq A1, A2, 0xffff, 0xffff;
+        A1, A2 <== or(0, 0, 0xabcd, 0xef01);
+        assert_eq A1, A2, 0xabcd, 0xef01;
+        A1, A2 <== or(0xabcd, 0xef01, 0, 0);
+        assert_eq A1, A2, 0xabcd, 0xef01;
+
+        // XOR
+        A1, A2 <== xor(0, 0, 0, 0);
+        assert_eq A1, A2, 0, 0;
+        A1, A2 <== xor(0xffff, 0xffff, 0xffff, 0xffff);
+        assert_eq A1, A2, 0, 0;
+        A1, A2 <== xor(0xffff, 0xffff, 0xabcd, 0xef01);
+        assert_eq A1, A2, 0x5432, 0x10fe;
+        A1, A2 <== xor(0xabcd, 0xef01, 0xffff, 0xffff);
+        assert_eq A1, A2, 0x5432, 0x10fe;
+        A1, A2 <== xor(0, 0, 0xabcd, 0xef01);
+        assert_eq A1, A2, 0xabcd, 0xef01;
+        A1, A2 <== xor(0xabcd, 0xef01, 0, 0);
+        assert_eq A1, A2, 0xabcd, 0xef01;
+
+        return;
+    }
+}
diff --git a/test_data/std/binary_bb_test.asm → test_data/std/binary_bb_test_8.asm b/test_data/std/binary_bb_test.asm → test_data/std/binary_bb_test_8.asm
@@ -1,5 +1,5 @@
 use std::machines::binary_bb::ByteBinary;
-use std::machines::binary_bb::Binary;
+use std::machines::binary_bb::Binary8;
 
 machine Main with degree: 196608 {
     reg pc[@pc];
@@ -21,7 +21,7 @@ machine Main with degree: 196608 {
     reg A4;
 
     ByteBinary byte_binary;
-    Binary binary(byte_binary);
+    Binary8 binary(byte_binary);
 
     instr and X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4 -> X2_1, X2_2, X2_3, X2_4 link ~> (X2_1, X2_2, X2_3, X2_4) = binary.and(X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4);
     instr or X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4 -> X2_1, X2_2, X2_3, X2_4 link ~> (X2_1, X2_2, X2_3, X2_4) = binary.or(X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4);