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

Allow and use permutation in all std machines

Browse Source
This commit is contained in:
Georg Wiese
2024-03-21 17:20:18 +01:00
parent 4d95210091
commit 10aeae6cb5
14 changed files with 36 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
std/arith.asm
View File

@@ -14,7 +14,7 @@ use std::prover::Query;
// Currently only supports "Equation 0", i.e., 256-Bit addition and multiplication.
machine Arith(CLK32_31, operation_id){
// The operation ID will be bit-decomosed to yield selEq[], controlling which equations are activated.
// The operation ID will be bit-decomposed to yield selEq[], controlling which equations are activated.
col witness operation_id;
// Computes x1 * y1 + x2, where all inputs / outputs are 256-bit words (represented as 32-Bit limbs in little-endian order).
@@ -29,7 +29,10 @@ machine Arith(CLK32_31, operation_id){
// Performs elliptic curve doubling of point (x1, y2).
// Operation ID is 12 = 0b1100, i.e., we activate equations 2, 3, and 4.
operation ec_double<12> x1c[0], x1c[1], x1c[2], x1c[3], x1c[4], x1c[5], x1c[6], x1c[7], y1c[0], y1c[1], y1c[2], y1c[3], y1c[4], y1c[5], y1c[6], y1c[7] -> x3c[0], x3c[1], x3c[2], x3c[3], x3c[4], x3c[5], x3c[6], x3c[7], y3c[0], y3c[1], y3c[2], y3c[3], y3c[4], y3c[5], y3c[6], y3c[7];
// Allow this machine to be connected via a permutation
call_selectors sel;
let BYTE: col = |i| i & 0xff;
let BYTE2: col = |i| i & 0xffff;

5
std/binary.asm
View File

@@ -12,13 +12,16 @@ machine Binary(latch, operation_id) {
operation xor<2> A, B -> C;
// Allow this machine to be connected via a permutation
call_selectors sel;
col witness operation_id;
unchanged_until(operation_id, latch);
col fixed latch(i) { if (i % 4) == 3 { 1 } else { 0 } };
col fixed FACTOR(i) { 1 << (((i + 1) % 4) * 8) };
// TOOD would be nice with destructuring assignment for arrays.
// TODO would be nice with destructuring assignment for arrays.
let inputs: (int -> int)[] = cross_product([256, 256, 3]);
let a = inputs[0];
let b = inputs[1];

3
std/hash/poseidon_bn254.asm
View File

@@ -14,6 +14,9 @@ machine PoseidonBN254(FIRSTBLOCK, operation_id) {
// hash functions.
operation poseidon_permutation<0> state[0], state[1], state[2] -> output[0];
// Allow this machine to be connected via a permutation
call_selectors sel;
col witness operation_id;
// Using parameters from https://eprint.iacr.org/2019/458.pdf

3
std/hash/poseidon_gl.asm
View File

@@ -11,6 +11,9 @@ machine PoseidonGL(FIRSTBLOCK, operation_id) {
// hash functions.
operation poseidon_permutation<0> state[0], state[1], state[2], state[3], state[4], state[5], state[6], state[7], state[8], state[9], state[10], state[11] -> output[0], output[1], output[2], output[3];
// Allow this machine to be connected via a permutation
call_selectors sel;
col witness operation_id;
// Ported from:

3
std/shift.asm
View File

@@ -9,6 +9,9 @@ machine Shift(latch, operation_id) {
operation shr<1> A, B -> C;
// Allow this machine to be connected via a permutation
call_selectors sel;
col witness operation_id;
unchanged_until(operation_id, latch);

3
std/split/split_bn254.asm
View File

@@ -6,6 +6,9 @@ machine SplitBN254(RESET, _) {
operation split in_acc -> o1, o2, o3, o4, o5, o6, o7, o8;
// Allow this machine to be connected via a permutation
call_selectors sel;
// Latch and operation ID
col fixed RESET(i) { if i % 32 == 31 { 1 } else { 0 } };

3
std/split/split_gl.asm
View File

@@ -6,6 +6,9 @@ machine SplitGL(RESET, _) {
operation split in_acc -> output_low, output_high;
// Allow this machine to be connected via a permutation
call_selectors sel;
// Latch and operation ID
col fixed RESET(i) { if i % 8 == 7 { 1 } else { 0 } };

6
test_data/std/arith_test.asm
View File

@@ -72,9 +72,9 @@ machine Main{
Arith arith;
instr affine_256 A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, C0, C1, C2, C3, C4, C5, C6, C7 -> D0, D1, D2, D3, D4, D5, D6, D7, E0, E1, E2, E3, E4, E5, E6, E7 = arith.affine_256;
instr ec_add A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, C0, C1, C2, C3, C4, C5, C6, C7, D0, D1, D2, D3, D4, D5, D6, D7 -> E0, E1, E2, E3, E4, E5, E6, E7, F0, F1, F2, F3, F4, F5, F6, F7 = arith.ec_add;
instr ec_double A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7 -> E0, E1, E2, E3, E4, E5, E6, E7, F0, F1, F2, F3, F4, F5, F6, F7 = arith.ec_double;
instr affine_256 A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, C0, C1, C2, C3, C4, C5, C6, C7 -> D0, D1, D2, D3, D4, D5, D6, D7, E0, E1, E2, E3, E4, E5, E6, E7 ~ arith.affine_256;
instr ec_add A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, C0, C1, C2, C3, C4, C5, C6, C7, D0, D1, D2, D3, D4, D5, D6, D7 -> E0, E1, E2, E3, E4, E5, E6, E7, F0, F1, F2, F3, F4, F5, F6, F7 ~ arith.ec_add;
instr ec_double A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7 -> E0, E1, E2, E3, E4, E5, E6, E7, F0, F1, F2, F3, F4, F5, F6, F7 ~ arith.ec_double;
instr assert_eq A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7 {
A0 = B0,

6
test_data/std/binary_test.asm
View File

@@ -12,9 +12,9 @@ machine Main {
Binary binary;
instr and X0, X1 -> X2 = binary.and;
instr or X0, X1 -> X2 = binary.or;
instr xor X0, X1 -> X2 = binary.xor;
instr and X0, X1 -> X2 ~ binary.and;
instr or X0, X1 -> X2 ~ binary.or;
instr xor X0, X1 -> X2 ~ binary.xor;
instr assert_eq X0, X1 {
X0 = X1

2
test_data/std/poseidon_bn254_test.asm
View File

@@ -12,7 +12,7 @@ machine Main {
PoseidonBN254 poseidon;
instr poseidon X0, X1, X2 -> X3 = poseidon.poseidon_permutation;
instr poseidon X0, X1, X2 -> X3 ~ poseidon.poseidon_permutation;
instr assert_eq X0, X1 {
X0 = X1

2
test_data/std/poseidon_gl_test.asm
View File

@@ -27,7 +27,7 @@ machine Main {
PoseidonGL poseidon;
instr poseidon X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11 -> X12, X13, X14, X15 = poseidon.poseidon_permutation;
instr poseidon X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11 -> X12, X13, X14, X15 ~ poseidon.poseidon_permutation;
instr assert_eq X0, X1 {
X0 = X1

4
test_data/std/shift_test.asm
View File

@@ -12,8 +12,8 @@ machine Main {
Shift shift;
instr shl X0, X1 -> X2 = shift.shl;
instr shr X0, X1 -> X2 = shift.shr;
instr shl X0, X1 -> X2 ~ shift.shl;
instr shr X0, X1 -> X2 ~ shift.shr;
instr assert_eq X0, X1 {
X0 = X1

2
test_data/std/split_bn254_test.asm
View File

@@ -25,7 +25,7 @@ machine Main {
SplitBN254 split_machine;
instr split X0 -> X1, X2, X3, X4, X5, X6, X7, X8 = split_machine.split;
instr split X0 -> X1, X2, X3, X4, X5, X6, X7, X8 ~ split_machine.split;
instr assert_eq X0, X1 {
X0 = X1

2
test_data/std/split_gl_test.asm
View File

@@ -13,7 +13,7 @@ machine Main {
SplitGL split_machine;
instr split X0 -> X1, X2 = split_machine.split;
instr split X0 -> X1, X2 ~ split_machine.split;
instr assert_eq X0, X1 {
X0 = X1