WrapGL machine: return both high and low values

compiler/tests/powdr_std.rs

@@ -62,8 +62,8 @@ fn poseidon_gl_test() {
 }
 
 #[test]
-fn wrap_gl_test() {
-    let f = "wrap_gl_test.asm";
+fn split_gl_test() {
+    let f = "split_gl_test.asm";
     verify_asm::<GoldilocksField>(f, Default::default());
     gen_estark_proof(f, Default::default());
 }

std/mod.asm

@@ -1,4 +1,4 @@
 mod binary;
 mod hash;
 mod shift;
-mod wrap;
+mod split;

std/split/mod.asm

@@ -0,0 +1 @@
+mod split_gl;

std/split/split_gl.asm

@@ -1,7 +1,7 @@
-// Wraps an arbitrary field element into a u32, on the Goldilocks field.
-machine WrapGL(RESET, operation_id) {
+// Splits an arbitrary field element into two u32s, on the Goldilocks field.
+machine SplitGL(RESET, operation_id) {
 
-    operation wrap<0> in_acc -> output;
+    operation split<0> in_acc -> output_low, output_high;
 
     // Latch and operation ID
     col fixed RESET(i) { i % 8 == 7 };
@@ -22,9 +22,11 @@ machine WrapGL(RESET, operation_id) {
 
     // 2. Build the output, packing the least significant 4 byte into
     //    a field element
-    col witness output;
-    col fixed FACTOR_OUTPUT = [0x100, 0x10000, 0x1000000, 0, 0, 0, 0, 1]*;
-    output' = (1 - RESET) * output + bytes * FACTOR_OUTPUT;
+    col witness output_low, output_high;
+    col fixed FACTOR_OUTPUT_LOW = [0x100, 0x10000, 0x1000000, 0, 0, 0, 0, 1]*;
+    col fixed FACTOR_OUTPUT_HIGH = [0, 0, 0, 1, 0x100, 0x10000, 0x1000000, 0]*;
+    output_low' = (1 - RESET) * output_low + bytes * FACTOR_OUTPUT_LOW;
+    output_high' = (1 - RESET) * output_high + bytes * FACTOR_OUTPUT_HIGH;
 
     // 3. Check that the byte decomposition does not overflow
     //

std/wrap/mod.asm

@@ -1 +0,0 @@
-mod wrap_gl;

test_data/std/split_gl_test.asm

@@ -0,0 +1,52 @@
+use std::split::split_gl::SplitGL;
+
+
+machine Main {
+    reg pc[@pc];
+    reg X0[<=];
+    reg X1[<=];
+    reg X2[<=];
+    reg low;
+    reg high;
+
+    degree 65536;
+
+    SplitGL split_machine;
+
+    instr split X0 -> X1, X2 = split_machine.split
+
+    instr assert_eq X0, X1 {
+        X0 = X1
+    }
+
+    instr loop { pc' = pc }
+
+    function main {
+
+        // Min value
+        // Note that this has two byte decompositions, 0x and p = 0xffffffff00000001.
+        // The second would lead to a different split value, but should be ruled
+        // out by the overflow check.
+        low, high <== split(0);
+        assert_eq low, 0;
+        assert_eq high, 0;
+
+        // Max value
+        // On Goldilocks, this is 0xffffffff00000000.
+        low, high <== split(-1);
+        assert_eq low, 0;
+        assert_eq high, 0xffffffff;
+
+        // Max low value
+        low, high <== split(0xfffffffeffffffff);
+        assert_eq low, 0xffffffff;
+        assert_eq high, 0xfffffffe;
+
+        // Some other value
+        low, high <== split(0xabcdef0123456789);
+        assert_eq low, 0x23456789;
+        assert_eq high, 0xabcdef01;
+
+        return;
+    }
+}

test_data/std/wrap_gl_test.asm

@@ -1,46 +0,0 @@
-use std::wrap::wrap_gl::WrapGL;
-
-
-machine Main {
-    reg pc[@pc];
-    reg X0[<=];
-    reg X1[<=];
-    reg A;
-
-    degree 65536;
-
-    WrapGL wrap_machine;
-
-    instr wrap X0 -> X1 = wrap_machine.wrap
-
-    instr assert_eq X0, X1 {
-        X0 = X1
-    }
-
-    instr loop { pc' = pc }
-
-    function main {
-
-        // Min value
-        // Note that this has two byte decompositions, 0x and p = 0xffffffff00000001.
-        // The second would lead to a different wrapped value, but should be ruled
-        // out by the overflow check.
-        A <== wrap(0);
-        assert_eq A, 0;
-
-        // Max value
-        // On Goldilocks, this is 0xffffffff00000000, which wraps to 0.
-        A <== wrap(-1);
-        assert_eq A, 0;
-
-        // Max wrapped value
-        A <== wrap(0xfffffffeffffffff);
-        assert_eq A, 0xffffffff;
-
-        // Some other value
-        A <== wrap(0xabcdef0123456789);
-        assert_eq A, 0x23456789;
-
-        return;
-    }
-}