diff --git a/compiler/tests/powdr_std.rs b/compiler/tests/powdr_std.rs index b0b0fca10..43516b43f 100644 --- a/compiler/tests/powdr_std.rs +++ b/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::(f, Default::default()); gen_estark_proof(f, Default::default()); } diff --git a/std/mod.asm b/std/mod.asm index 4403092bc..000d5c115 100644 --- a/std/mod.asm +++ b/std/mod.asm @@ -1,4 +1,4 @@ mod binary; mod hash; mod shift; -mod wrap; \ No newline at end of file +mod split; \ No newline at end of file diff --git a/std/split/mod.asm b/std/split/mod.asm new file mode 100644 index 000000000..5e04b8d4c --- /dev/null +++ b/std/split/mod.asm @@ -0,0 +1 @@ +mod split_gl; \ No newline at end of file diff --git a/std/wrap/wrap_gl.asm b/std/split/split_gl.asm similarity index 84% rename from std/wrap/wrap_gl.asm rename to std/split/split_gl.asm index d02342d5b..5a51b1243 100644 --- a/std/wrap/wrap_gl.asm +++ b/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 // diff --git a/std/wrap/mod.asm b/std/wrap/mod.asm deleted file mode 100644 index e2cc6b577..000000000 --- a/std/wrap/mod.asm +++ /dev/null @@ -1 +0,0 @@ -mod wrap_gl; \ No newline at end of file diff --git a/test_data/std/split_gl_test.asm b/test_data/std/split_gl_test.asm new file mode 100644 index 000000000..239051b55 --- /dev/null +++ b/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; + } +} \ No newline at end of file diff --git a/test_data/std/wrap_gl_test.asm b/test_data/std/wrap_gl_test.asm deleted file mode 100644 index 67cfc1a12..000000000 --- a/test_data/std/wrap_gl_test.asm +++ /dev/null @@ -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; - } -} \ No newline at end of file