Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Future optimization for plonky3 keccak memory (16 bits limbs) #2146

Draft
wants to merge 1 commit into
base: plonky3-keccak-memory-new-new
Choose a base branch
from
+1,396 −5,288
Draft

Future optimization for plonky3 keccak memory (16 bits limbs) #2146

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6,547 changes: 1,327 additions & 5,220 deletions output.txt
View file

Large diffs are not rendered by default.

47 changes: 24 additions & 23 deletions std/machines/hash/keccakf16_memory.asm
View file
Original file line number Diff line number Diff line change
@@ -73,42 +73,42 @@ machine Keccakf16Memory(mem: Memory) with
// Helper column to reduce the degree from the inverse constraints to 3.
col witness helper[50];

// Address constraints for first step (input addresses)

// Helper column is set to equal (addr_l[i]' * (addr_l[i] - 0xfffc) - 1),
// i.e. inverse * expr_to_test_for_zero - 1, where (addr_l[i] - 0xfffc) is tested for zero
// and where inverse is stored as rotation of addr_l.
array::new(50, |i| {
first_step * (helper[i] - (addr_l[i]' * (addr_l[i] - 0xfffc) - 1)) = 0
});

// Inverse constraint that (inverse * expr_to_test_for_zero - 1) * expr_to_test_for_zero = 0.
array::new(50, |i| {
first_step * helper[i] * (addr_l[i] - 0xfffc) = 0
// First step
// Keep same value for addr_l
array::map(addr_l, |l| {
first_step * (l' - l) = 0
});

// Carry is stored as rotation of addr_h.
// Constrain that carry + inverse * expr_to_test_for_zero - 1 = 0,
// so that if addr_l = 0xfffc (addr_h will be incremented by 1),
// then carry must be 1, or carry must be 0 in all other cases.
array::zip(addr_h, addr_l, |h, l| {
first_step * (h' + l' * (l - 0xfffc) - 1) = 0
// Constrain carry (addr_h') and addr_h
array::new(49, |i| {
first_step * (addr_h[i + 1] - addr_h[i] - addr_h[i]') = 0
});

// Constrain that if carry = 0, then the next addr_l is reset to 0,
// else if carry = 1, then the next addr_l increments by 4.
// Constrain carry (addr_h') and addr_l
array::new(49, |i| {
first_step * (
addr_h[i]' * addr_l[i + 1] +
(1 - addr_h[i]') * (addr_l[i + 1] - addr_l[i] - 4)
) = 0
});

// Constrain that addr_h is always incremented by carry, whether carry is 0 or 1.
array::new(49, |i| {
first_step * (addr_h[i + 1] - addr_h[i] - addr_h[i]') = 0
// Second step
// Store addr_l * inverse (addr_h') to addr_l'
array::zip(addr_h, addr_l, |h, l| {
second_step * (l' - l * h') = 0
});

// Constrain carry (addr_h), inverse (addr_h'), and addr_l
array::zip(addr_h, addr_l, |h, l| {
second_step * (h + h' * (l - 0xfffc) - 1) = 0
});

// Constrain inverse (addr_h') and addr_l, using addr_l * inverse (addr_l')
array::zip(addr_h, addr_l, |h, l| {
second_step * (l' - 0xfffc * h' - 1) * (l - 0xfffc) = 0
});


// Address constraints for final step (output addresses)
// Same as constraints for first step (input addresses),
// except that carry is stored as prior row of addr_h
@@ -356,6 +356,7 @@ machine Keccakf16Memory(mem: Memory) with

let first_step: expr = step_flags[0]; // Aliasing instead of defining a new fixed column.
let final_step: expr = step_flags[NUM_ROUNDS - 1];
let second_step: expr = step_flags[1];
let penultimate_step: expr = step_flags[NUM_ROUNDS - 2];
col fixed is_last = [0]* + [1];

90 changes: 45 additions & 45 deletions test_data/std/keccakf16_memory_test.asm
View file
Original file line number Diff line number Diff line change
@@ -36,51 +36,51 @@ machine Main with degree: 65536 {
}

function main {
// Test 1: Input/output address computations have no carry.
// 0 for all 25 64-bit inputs except setting the second 64-bit input to 1. All 64-bit inputs in chunks of 4 16-bit big endian limbs.
mstore 0, 0, 0, 0;
mstore 0, 4, 0, 0;
mstore 0, 8, 0, 0;
mstore 0, 12, 0, 1;
mstore 0, 16, 0, 0;
mstore 0, 20, 0, 0;
mstore 0, 24, 0, 0;
mstore 0, 28, 0, 0;
mstore 0, 32, 0, 0;
mstore 0, 36, 0, 0;
mstore 0, 40, 0, 0;
mstore 0, 44, 0, 0;
mstore 0, 48, 0, 0;
mstore 0, 52, 0, 0;
mstore 0, 56, 0, 0;
mstore 0, 60, 0, 0;
mstore 0, 64, 0, 0;
mstore 0, 68, 0, 0;
mstore 0, 72, 0, 0;
mstore 0, 76, 0, 0;
mstore 0, 80, 0, 0;
mstore 0, 84, 0, 0;
mstore 0, 88, 0, 0;
mstore 0, 92, 0, 0;
mstore 0, 96, 0, 0;
// Input address 0. Output address 200.
keccakf16_memory 0, 0, 0, 200;
// Selectively checking a few registers only.
// Test vector generated from Tiny Keccak.
assert_eq 0, 200, 0xfdbb, 0xbbdf;
assert_eq 0, 204, 0x9001, 0x405f;
assert_eq 0, 392, 0xeac9, 0xf006;
assert_eq 0, 396, 0x664d, 0xeb35;

// Test 2: Same as Test 1 but sets input and output addresses to be the same.
// No need to rerun the mstores because input values from Test 1 should be intact.
keccakf16_memory 0, 0, 0, 0;
// Selectively checking a few registers only.
// Test vector generated from Tiny Keccak.
assert_eq 0, 0, 0xfdbb, 0xbbdf;
assert_eq 0, 4, 0x9001, 0x405f;
assert_eq 0, 192, 0xeac9, 0xf006;
assert_eq 0, 196, 0x664d, 0xeb35;
// // Test 1: Input/output address computations have no carry.
// // 0 for all 25 64-bit inputs except setting the second 64-bit input to 1. All 64-bit inputs in chunks of 4 16-bit big endian limbs.
// mstore 0, 0, 0, 0;
// mstore 0, 4, 0, 0;
// mstore 0, 8, 0, 0;
// mstore 0, 12, 0, 1;
// mstore 0, 16, 0, 0;
// mstore 0, 20, 0, 0;
// mstore 0, 24, 0, 0;
// mstore 0, 28, 0, 0;
// mstore 0, 32, 0, 0;
// mstore 0, 36, 0, 0;
// mstore 0, 40, 0, 0;
// mstore 0, 44, 0, 0;
// mstore 0, 48, 0, 0;
// mstore 0, 52, 0, 0;
// mstore 0, 56, 0, 0;
// mstore 0, 60, 0, 0;
// mstore 0, 64, 0, 0;
// mstore 0, 68, 0, 0;
// mstore 0, 72, 0, 0;
// mstore 0, 76, 0, 0;
// mstore 0, 80, 0, 0;
// mstore 0, 84, 0, 0;
// mstore 0, 88, 0, 0;
// mstore 0, 92, 0, 0;
// mstore 0, 96, 0, 0;
// // Input address 0. Output address 200.
// keccakf16_memory 0, 0, 0, 200;
// // Selectively checking a few registers only.
// // Test vector generated from Tiny Keccak.
// assert_eq 0, 200, 0xfdbb, 0xbbdf;
// assert_eq 0, 204, 0x9001, 0x405f;
// assert_eq 0, 392, 0xeac9, 0xf006;
// assert_eq 0, 396, 0x664d, 0xeb35;
//
// // Test 2: Same as Test 1 but sets input and output addresses to be the same.
// // No need to rerun the mstores because input values from Test 1 should be intact.
// keccakf16_memory 0, 0, 0, 0;
// // Selectively checking a few registers only.
// // Test vector generated from Tiny Keccak.
// assert_eq 0, 0, 0xfdbb, 0xbbdf;
// assert_eq 0, 4, 0x9001, 0x405f;
// assert_eq 0, 192, 0xeac9, 0xf006;
// assert_eq 0, 196, 0x664d, 0xeb35;

// Test 3: Input/output address computations have carry.
// 0 for all 25 64-bit inputs except setting the second 64-bit input to 1. All 64-bit inputs in chunks of 4 16-bit big endian limbs.