github/powdr
1
1
Fork 0
mirror of https://github.com/powdr-labs/powdr.git synced 2026-04-20 03:03:25 -04:00
Code Issues Packages Projects Releases Wiki Activity

Add SplitBN254 machine, use queries in SplitGL machine

Browse Source
This commit is contained in:
Georg Wiese
2023-10-27 10:05:25 +00:00
parent 88c578a22c
commit f26a161ae3
6 changed files with 186 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
compiler/tests/powdr_std.rs
View File

@@ -40,7 +40,7 @@ fn gen_halo2_proof(file_name: &str, inputs: Vec<Bn254Field>) {
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";

4
executor/src/witgen/query_processor.rs
View File

@@ -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(),
))
}
}

1
std/split/mod.asm
View File

@@ -1 +1,2 @@
mod split_bn254;
mod split_gl;

82
std/split/split_bn254.asm Normal file
View File

@@ -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;
}

12
std/split/split_gl.asm
View File

@@ -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]*;

88
test_data/std/split_bn254_test.asm Normal file
View File

@@ -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;
}
}