From f26a161ae3655caffd9c5f972783deecf68bf00f Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Fri, 27 Oct 2023 10:05:25 +0000 Subject: [PATCH] Add SplitBN254 machine, use queries in SplitGL machine --- compiler/tests/powdr_std.rs | 8 ++- executor/src/witgen/query_processor.rs | 4 +- std/split/mod.asm | 1 + std/split/split_bn254.asm | 82 ++++++++++++++++++++++++ std/split/split_gl.asm | 12 ++-- test_data/std/split_bn254_test.asm | 88 ++++++++++++++++++++++++++ 6 files changed, 186 insertions(+), 9 deletions(-) create mode 100644 std/split/split_bn254.asm create mode 100644 test_data/std/split_bn254_test.asm diff --git a/compiler/tests/powdr_std.rs b/compiler/tests/powdr_std.rs index 43516b43f..1270f5e37 100644 --- a/compiler/tests/powdr_std.rs +++ b/compiler/tests/powdr_std.rs @@ -40,7 +40,7 @@ fn gen_halo2_proof(file_name: &str, inputs: Vec) { inputs, &mktemp::Temp::new_dir().unwrap(), true, - Some(backend::BackendType::Halo2), + Some(backend::BackendType::Halo2Mock), ) .unwrap(); } @@ -61,6 +61,12 @@ fn poseidon_gl_test() { gen_estark_proof(f, Default::default()); } +#[test] +fn split_bn254_test() { + let f = "split_bn254_test.asm"; + gen_halo2_proof(f, Default::default()); +} + #[test] fn split_gl_test() { let f = "split_gl_test.asm"; diff --git a/executor/src/witgen/query_processor.rs b/executor/src/witgen/query_processor.rs index 250f41e48..9fd97af1c 100644 --- a/executor/src/witgen/query_processor.rs +++ b/executor/src/witgen/query_processor.rs @@ -116,7 +116,7 @@ where Ok(rows.current_row_index.into()) } Expression::Reference(Reference::Poly(poly)) => { - if !poly.next && poly.index.is_none() { + if poly.index.is_none() { let poly_id = poly.poly_id.unwrap(); match poly_id.ptype { PolynomialType::Committed | PolynomialType::Intermediate => { @@ -135,7 +135,7 @@ where } } else { Err(IncompleteCause::ExpressionEvaluationUnimplemented( - "Cannot evaluate arrays or next references.".to_string(), + "Cannot evaluate arrays.".to_string(), )) } } diff --git a/std/split/mod.asm b/std/split/mod.asm index 5e04b8d4c..c08ecdf61 100644 --- a/std/split/mod.asm +++ b/std/split/mod.asm @@ -1 +1,2 @@ +mod split_bn254; mod split_gl; \ No newline at end of file diff --git a/std/split/split_bn254.asm b/std/split/split_bn254.asm new file mode 100644 index 000000000..b9166a740 --- /dev/null +++ b/std/split/split_bn254.asm @@ -0,0 +1,82 @@ +// Splits an arbitrary field element into 8 u32s (in little endian order), on the BN254 field. +machine SplitBN254(RESET, _) { + + operation split in_acc -> o1, o2, o3, o4, o5, o6, o7, o8; + + // Latch and operation ID + col fixed RESET(i) { i % 32 == 31 }; + + // 1. Decompose the input into bytes + + // The byte decomposition of the input, in little-endian order + // and shifted forward by one (to use the last row of the + // previous block) + // A hint is provided because automatic witness generation does not + // understand step 3 to figure out that the byte decomposition is unique. + col witness bytes(i) query ("hint", (in_acc' >> (((i + 1) % 32) * 8)) % 0xff); + // Puts the bytes together to form the input + col witness in_acc; + // Factors to multiply the bytes by + col fixed FACTOR(i) { 1 << (((i + 1) % 32) * 8) }; + + in_acc' = (1 - RESET) * in_acc + bytes * FACTOR; + + // 2. Build the output, packing chunks of 4 bytes (i.e., 32 bit) into a field element + col witness o1, o2, o3, o4, o5, o6, o7, o8; + col fixed FACTOR_OUTPUT1 = [0x100, 0x10000, 0x1000000, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]*; + col fixed FACTOR_OUTPUT2 = [0, 0, 0, 1, 0x100, 0x10000, 0x1000000, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]*; + col fixed FACTOR_OUTPUT3 = [0, 0, 0, 0, 0, 0, 0, 1, 0x100, 0x10000, 0x1000000, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]*; + col fixed FACTOR_OUTPUT4 = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0x100, 0x10000, 0x1000000, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]*; + col fixed FACTOR_OUTPUT5 = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0x100, 0x10000, 0x1000000, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]*; + col fixed FACTOR_OUTPUT6 = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0x100, 0x10000, 0x1000000, 0, 0, 0, 0, 0, 0, 0, 0, 0]*; + col fixed FACTOR_OUTPUT7 = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0x100, 0x10000, 0x1000000, 0, 0, 0, 0, 0]*; + col fixed FACTOR_OUTPUT8 = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0x100, 0x10000, 0x1000000, 0]*; + + o1' = (1 - RESET) * o1 + bytes * FACTOR_OUTPUT1; + o2' = (1 - RESET) * o2 + bytes * FACTOR_OUTPUT2; + o3' = (1 - RESET) * o3 + bytes * FACTOR_OUTPUT3; + o4' = (1 - RESET) * o4 + bytes * FACTOR_OUTPUT4; + o5' = (1 - RESET) * o5 + bytes * FACTOR_OUTPUT5; + o6' = (1 - RESET) * o6 + bytes * FACTOR_OUTPUT6; + o7' = (1 - RESET) * o7 + bytes * FACTOR_OUTPUT7; + o8' = (1 - RESET) * o8 + bytes * FACTOR_OUTPUT8; + + // 3. Check that the byte decomposition does not overflow + // + // Skipping this step would work but it wouldn't be sound, because + // the 32-byte decomposition could overflow, since the BN254 scalar field + // prime is smaller than 2^256. + // + // The approach is to compare the byte decomposition with that of + // the maximum possible value (p - 1) byte by byte, + // from most significant to least significant (i.e., going backwards). + // A byte can only be larger than that of the max value if any previous + // byte has been smaller. + // See wrap_gl.asm for an example. + + // Bytes of the maximum value, in little endian order, rotated by one + // For BN254, p = 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001, + // so the maximum value is 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000000. + col fixed BYTES_MAX = [0x00, 0x00, 0xf0, 0x93, 0xf5, 0xe1, 0x43, 0x91, 0x70, 0xb9, 0x79, 0x48, 0xe8, 0x33, 0x28, 0x5d, 0x58, 0x81, 0x81, 0xb6, 0x45, 0x50, 0xb8, 0x29, 0xa0, 0x31, 0xe1, 0x72, 0x4e, 0x64, 0x30, 0x00]*; + + // Byte comparison block machine + col fixed P_A(i) { i % 256 }; + col fixed P_B(i) { (i >> 8) % 256 }; + col fixed P_LT(i) { (P_A(i) < P_B(i)) }; + col fixed P_GT(i) { (P_A(i) > P_B(i)) }; + + // Compare the current byte with the corresponding byte of the maximum value. + col witness lt; + col witness gt; + { bytes, BYTES_MAX, lt, gt } in { P_A, P_B, P_LT, P_GT }; + + // Compute whether the current or any previous byte has been less than + // the corresponding byte of the maximum value. + // This moves *backward* from the second to last row. + col witness was_lt; + was_lt = RESET' * lt + (1 - RESET') * (was_lt' + lt - was_lt' * lt); + + // If any byte is larger, but no previous byte was smaller, the byte + // decomposition has overflowed and should be rejected. + gt * (1 - was_lt) = 0; +} diff --git a/std/split/split_gl.asm b/std/split/split_gl.asm index 5a51b1243..4478fc3ca 100644 --- a/std/split/split_gl.asm +++ b/std/split/split_gl.asm @@ -1,18 +1,19 @@ // Splits an arbitrary field element into two u32s, on the Goldilocks field. -machine SplitGL(RESET, operation_id) { +machine SplitGL(RESET, _) { - operation split<0> in_acc -> output_low, output_high; + operation split in_acc -> output_low, output_high; // Latch and operation ID col fixed RESET(i) { i % 8 == 7 }; - col witness operation_id; // 1. Decompose the input into bytes // The byte decomposition of the input, in little-endian order // and shifted forward by one (to use the last row of the // previous block) - col witness bytes; + // A hint is provided because automatic witness generation does not + // understand step 3 to figure out that the byte decomposition is unique. + col witness bytes(i) query ("hint", (in_acc' >> (((i + 1) % 8) * 8)) % 0xff); // Puts the bytes together to form the input col witness in_acc; // Factors to multiply the bytes by @@ -20,8 +21,7 @@ machine SplitGL(RESET, operation_id) { in_acc' = (1 - RESET) * in_acc + bytes * FACTOR; - // 2. Build the output, packing the least significant 4 byte into - // a field element + // 2. Build the output, packing chunks of 4 bytes (i.e., 32 bit) into a field element 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]*; diff --git a/test_data/std/split_bn254_test.asm b/test_data/std/split_bn254_test.asm new file mode 100644 index 000000000..3bff0805c --- /dev/null +++ b/test_data/std/split_bn254_test.asm @@ -0,0 +1,88 @@ +use std::split::split_bn254::SplitBN254; + + +machine Main { + reg pc[@pc]; + reg X0[<=]; + reg X1[<=]; + reg X2[<=]; + reg X3[<=]; + reg X4[<=]; + reg X5[<=]; + reg X6[<=]; + reg X7[<=]; + reg X8[<=]; + reg A1; + reg A2; + reg A3; + reg A4; + reg A5; + reg A6; + reg A7; + reg A8; + + degree 65536; + + SplitBN254 split_machine; + + instr split X0 -> X1, X2, X3, X4, X5, X6, X7, X8 = 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, 0 and p. + // The second would lead to a different split value, but should be ruled + // out by the overflow check. + A1, A2, A3, A4, A5, A6, A7, A8 <== split(0); + assert_eq A1, 0; + assert_eq A2, 0; + assert_eq A3, 0; + assert_eq A4, 0; + assert_eq A5, 0; + assert_eq A6, 0; + assert_eq A7, 0; + assert_eq A8, 0; + + // Max value + // On BN254, this is 0x30644e72 e131a029 b85045b6 8181585d 2833e848 79b97091 43e1f593 f0000000 + A1, A2, A3, A4, A5, A6, A7, A8 <== split(-1); + assert_eq A1, 0xf0000000; + assert_eq A2, 0x43e1f593; + assert_eq A3, 0x79b97091; + assert_eq A4, 0x2833e848; + assert_eq A5, 0x8181585d; + assert_eq A6, 0xb85045b6; + assert_eq A7, 0xe131a029; + assert_eq A8, 0x30644e72; + + // Max low values + A1, A2, A3, A4, A5, A6, A7, A8 <== split(0x2fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff); + assert_eq A1, 0xffffffff; + assert_eq A2, 0xffffffff; + assert_eq A3, 0xffffffff; + assert_eq A4, 0xffffffff; + assert_eq A5, 0xffffffff; + assert_eq A6, 0xffffffff; + assert_eq A7, 0xffffffff; + assert_eq A8, 0x2fffffff; + + // Some other value + A1, A2, A3, A4, A5, A6, A7, A8 <== split(0xabcdef0123456789); + assert_eq A1, 0x23456789; + assert_eq A2, 0xabcdef01; + assert_eq A3, 0; + assert_eq A4, 0; + assert_eq A5, 0; + assert_eq A6, 0; + assert_eq A7, 0; + assert_eq A8, 0; + + return; + } +} \ No newline at end of file