diff --git a/Cargo.toml b/Cargo.toml index 82fb725e..357a6278 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,5 +1,5 @@ [workspace] -members = ["ecdsa", "evm", "field", "insertion", "maybe_rayon", "plonky2", "starky", "system_zero", "u32", "util", "waksman"] +members = ["ecdsa", "evm", "field", "insertion", "maybe_rayon", "plonky2", "starky", "u32", "util", "waksman"] [profile.release] opt-level = 3 diff --git a/system_zero/Cargo.toml b/system_zero/Cargo.toml deleted file mode 100644 index 2595eb03..00000000 --- a/system_zero/Cargo.toml +++ /dev/null @@ -1,26 +0,0 @@ -[package] -name = "system_zero" -description = "A VM whose execution can be verified with STARKs; designed for proving Ethereum transactions" -version = "0.1.0" -edition = "2021" - -[dependencies] -anyhow = "1.0.40" -itertools = "0.10.0" -log = "0.4.14" -plonky2 = { version = "0.1.2" } -plonky2_util = { version = "0.1.0" } -rand = "0.8.4" -rand_chacha = "0.3.1" -starky = { version = "0.1.1" } - -[dev-dependencies] -criterion = "0.4.0" -env_logger = "0.10.0" - -[[bench]] -name = "lookup_permuted_cols" -harness = false - -[target.'cfg(not(target_env = "msvc"))'.dev-dependencies] -jemallocator = "0.5.0" diff --git a/system_zero/benches/allocator/mod.rs b/system_zero/benches/allocator/mod.rs deleted file mode 100644 index 441e5dc5..00000000 --- a/system_zero/benches/allocator/mod.rs +++ /dev/null @@ -1,7 +0,0 @@ -// Set up Jemalloc -#[cfg(not(target_env = "msvc"))] -use jemallocator::Jemalloc; - -#[cfg(not(target_env = "msvc"))] -#[global_allocator] -static GLOBAL: Jemalloc = Jemalloc; diff --git a/system_zero/benches/lookup_permuted_cols.rs b/system_zero/benches/lookup_permuted_cols.rs deleted file mode 100644 index 0088f565..00000000 --- a/system_zero/benches/lookup_permuted_cols.rs +++ /dev/null @@ -1,32 +0,0 @@ -mod allocator; - -use criterion::{criterion_group, criterion_main, BenchmarkId, Criterion}; -use itertools::Itertools; -use plonky2::field::goldilocks_field::GoldilocksField; -use plonky2::field::types::Field; -use rand::{thread_rng, Rng}; -use system_zero::lookup::permuted_cols; - -type F = GoldilocksField; - -fn criterion_benchmark(c: &mut Criterion) { - let mut group = c.benchmark_group("lookup-permuted-cols"); - - for size_log in [16, 17, 18] { - let size = 1 << size_log; - group.bench_with_input(BenchmarkId::from_parameter(size), &size, |b, _| { - // We could benchmark a table of random values with - // let table = F::rand_vec(size); - // But in practice we currently use tables that are pre-sorted, which makes - // permuted_cols cheaper since it will sort the table. - let table = (0..size).map(F::from_canonical_usize).collect_vec(); - let input = (0..size) - .map(|_| table[thread_rng().gen_range(0..size)]) - .collect_vec(); - b.iter(|| permuted_cols(&input, &table)); - }); - } -} - -criterion_group!(benches, criterion_benchmark); -criterion_main!(benches); diff --git a/system_zero/src/alu/addition.rs b/system_zero/src/alu/addition.rs deleted file mode 100644 index 3810482c..00000000 --- a/system_zero/src/alu/addition.rs +++ /dev/null @@ -1,70 +0,0 @@ -use plonky2::field::extension::Extendable; -use plonky2::field::packed::PackedField; -use plonky2::field::types::{Field, PrimeField64}; -use plonky2::hash::hash_types::RichField; -use plonky2::iop::ext_target::ExtensionTarget; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use plonky2::plonk::plonk_common::reduce_with_powers_ext_circuit; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; - -use crate::registers::alu::*; -use crate::registers::NUM_COLUMNS; - -pub(crate) fn generate_addition(values: &mut [F; NUM_COLUMNS]) { - let in_1 = values[COL_ADD_INPUT_0].to_canonical_u64(); - let in_2 = values[COL_ADD_INPUT_1].to_canonical_u64(); - let in_3 = values[COL_ADD_INPUT_2].to_canonical_u64(); - let output = in_1 + in_2 + in_3; - - values[COL_ADD_OUTPUT_0] = F::from_canonical_u16(output as u16); - values[COL_ADD_OUTPUT_1] = F::from_canonical_u16((output >> 16) as u16); - values[COL_ADD_OUTPUT_2] = F::from_canonical_u16((output >> 32) as u16); -} - -pub(crate) fn eval_addition>( - local_values: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, -) { - let is_add = local_values[IS_ADD]; - let in_1 = local_values[COL_ADD_INPUT_0]; - let in_2 = local_values[COL_ADD_INPUT_1]; - let in_3 = local_values[COL_ADD_INPUT_2]; - let out_1 = local_values[COL_ADD_OUTPUT_0]; - let out_2 = local_values[COL_ADD_OUTPUT_1]; - let out_3 = local_values[COL_ADD_OUTPUT_2]; - - let weight_2 = F::from_canonical_u64(1 << 16); - let weight_3 = F::from_canonical_u64(1 << 32); - // Note that this can't overflow. Since each output limb has been range checked as 16-bits, - // this sum can be around 48 bits at most. - let out = out_1 + out_2 * weight_2 + out_3 * weight_3; - - let computed_out = in_1 + in_2 + in_3; - - yield_constr.constraint(is_add * (out - computed_out)); -} - -pub(crate) fn eval_addition_circuit, const D: usize>( - builder: &mut CircuitBuilder, - local_values: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, -) { - let is_add = local_values[IS_ADD]; - let in_1 = local_values[COL_ADD_INPUT_0]; - let in_2 = local_values[COL_ADD_INPUT_1]; - let in_3 = local_values[COL_ADD_INPUT_2]; - let out_1 = local_values[COL_ADD_OUTPUT_0]; - let out_2 = local_values[COL_ADD_OUTPUT_1]; - let out_3 = local_values[COL_ADD_OUTPUT_2]; - - let limb_base = builder.constant(F::from_canonical_u64(1 << 16)); - // Note that this can't overflow. Since each output limb has been range checked as 16-bits, - // this sum can be around 48 bits at most. - let out = reduce_with_powers_ext_circuit(builder, &[out_1, out_2, out_3], limb_base); - - let computed_out = builder.add_many_extension([in_1, in_2, in_3]); - - let diff = builder.sub_extension(out, computed_out); - let filtered_diff = builder.mul_extension(is_add, diff); - yield_constr.constraint(builder, filtered_diff); -} diff --git a/system_zero/src/alu/bitops.rs b/system_zero/src/alu/bitops.rs deleted file mode 100644 index aed63415..00000000 --- a/system_zero/src/alu/bitops.rs +++ /dev/null @@ -1,360 +0,0 @@ -use plonky2::field::extension::Extendable; -use plonky2::field::packed::PackedField; -use plonky2::field::types::{Field, PrimeField64}; -use plonky2::hash::hash_types::RichField; -use plonky2::iop::ext_target::ExtensionTarget; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use plonky2::plonk::plonk_common::reduce_with_powers_ext_circuit; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; - -use crate::registers::alu::*; -use crate::registers::NUM_COLUMNS; - -/// Interpret the N <= 32 elements of `bits` as bits from low to high of a -/// u32 and return \sum_i bits[i] 2^i as an element of P. -pub(crate) fn binary_to_u32(bits: [P; 32]) -> P -where - F: Field, - P: PackedField, -{ - bits.into_iter() - .enumerate() - .map(|(i, b)| b * F::from_canonical_u64(1u64 << i)) - .sum() -} - -fn generate_bitop_32( - values: &mut [F; NUM_COLUMNS], - bitop: usize, - input_a_regs: [usize; 32], - input_b_regs: [usize; 32], - output_reg: usize, -) { - let a_bits = input_a_regs.map(|r| values[r]); - let b_bits = input_b_regs.map(|r| values[r]); - - let a = binary_to_u32(a_bits).to_canonical_u64() as u32; - let b = binary_to_u32(b_bits).to_canonical_u64() as u32; - - let out = match bitop { - IS_AND => a & b, - IS_IOR => a | b, - IS_XOR => a ^ b, - IS_ANDNOT => a & !b, - _ => panic!("unrecognized bitop instruction code"), - }; - - values[output_reg] = F::from_canonical_u32(out); -} - -/// Use the `COL_BIT_DECOMP_INPUT_[AB]_{LO,HI}_*` registers to read -/// bits from `values`, apply `bitop` to the reconstructed u32's (both -/// lo and hi, for 64 bits total), and write the result to the -/// `COL_BITOP_OUTPUT_*` registers. -pub(crate) fn generate_bitop(values: &mut [F; NUM_COLUMNS], bitop: usize) { - // Generate lo half - generate_bitop_32( - values, - bitop, - COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS, - COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS, - COL_BITOP_OUTPUT_0, - ); - // Generate hi half - generate_bitop_32( - values, - bitop, - COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS, - COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS, - COL_BITOP_OUTPUT_1, - ); -} - -fn eval_bitop_32>( - lv: &[P; NUM_COLUMNS], - input_a_regs: [usize; 32], - input_b_regs: [usize; 32], - output_reg: usize, - yield_constr: &mut ConstraintConsumer

, -) { - // Filters - let is_and = lv[IS_AND]; - let is_ior = lv[IS_IOR]; - let is_xor = lv[IS_XOR]; - let is_andnot = lv[IS_ANDNOT]; - - // Inputs - let a_bits = input_a_regs.map(|r| lv[r]); - let b_bits = input_b_regs.map(|r| lv[r]); - - // Ensure that the inputs are bits - let inst_constr = is_and + is_ior + is_xor + is_andnot; - a_bits.map(|v| yield_constr.constraint(inst_constr * (v * v - v))); - b_bits.map(|v| yield_constr.constraint(inst_constr * (v * v - v))); - - // Output - let output = lv[output_reg]; - - let a = binary_to_u32(a_bits); - let b = binary_to_u32(b_bits); - let a_and_b = binary_to_u32(a_bits.zip(b_bits).map(|(b0, b1)| b0 * b1)); - - let constraint = is_and * (a_and_b - output) - + is_ior * (a + b - a_and_b - output) - + is_xor * (a + b - a_and_b * F::TWO - output) - + is_andnot * (a - a_and_b - output); - - yield_constr.constraint(constraint); -} - -/// Verify an AND, IOR, XOR, or ANDNOT instruction. -pub(crate) fn eval_bitop>( - lv: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, -) { - // Constraint for lo half - eval_bitop_32( - lv, - COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS, - COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS, - COL_BITOP_OUTPUT_0, - yield_constr, - ); - // Constraint for hi half - eval_bitop_32( - lv, - COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS, - COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS, - COL_BITOP_OUTPUT_1, - yield_constr, - ); -} - -pub(crate) fn constrain_all_to_bits_circuit, const D: usize>( - builder: &mut CircuitBuilder, - yield_constr: &mut RecursiveConstraintConsumer, - filter: ExtensionTarget, - vals: &[ExtensionTarget], -) { - for v in vals.iter() { - let t0 = builder.mul_sub_extension(*v, *v, *v); - let t1 = builder.mul_extension(filter, t0); - yield_constr.constraint(builder, t1) - } -} - -/// As for `eval_bitop`, but build with `builder`. -fn eval_bitop_32_circuit, const D: usize>( - builder: &mut CircuitBuilder, - lv: &[ExtensionTarget; NUM_COLUMNS], - input_a_regs: [usize; 32], - input_b_regs: [usize; 32], - output_reg: usize, - yield_constr: &mut RecursiveConstraintConsumer, -) { - // Filters - let is_and = lv[IS_AND]; - let is_ior = lv[IS_IOR]; - let is_xor = lv[IS_XOR]; - let is_andnot = lv[IS_ANDNOT]; - - // Inputs - let a_bits = input_a_regs.map(|r| lv[r]); - let b_bits = input_b_regs.map(|r| lv[r]); - - // Ensure that the inputs are bits - let inst_constr = builder.add_many_extension([is_and, is_ior, is_xor, is_andnot]); - constrain_all_to_bits_circuit(builder, yield_constr, inst_constr, &a_bits); - constrain_all_to_bits_circuit(builder, yield_constr, inst_constr, &b_bits); - - // Output - let output = lv[output_reg]; - - let limb_base = builder.constant(F::TWO); - let a = reduce_with_powers_ext_circuit(builder, &a_bits, limb_base); - let b = reduce_with_powers_ext_circuit(builder, &b_bits, limb_base); - let a_and_b_bits = a_bits - .zip(b_bits) - .map(|(b0, b1)| builder.mul_extension(b0, b1)); - let a_and_b = reduce_with_powers_ext_circuit(builder, &a_and_b_bits, limb_base); - - let and_constr = { - let t = builder.sub_extension(a_and_b, output); - builder.mul_extension(t, is_and) - }; - - let ior_constr = { - let t0 = builder.add_extension(a, b); - let t1 = builder.sub_extension(t0, a_and_b); - let t2 = builder.sub_extension(t1, output); - builder.mul_extension(t2, is_ior) - }; - - let xor_constr = { - let t0 = builder.add_extension(a, b); - let t1 = builder.mul_const_extension(F::TWO, a_and_b); - let t2 = builder.sub_extension(t0, t1); - let t3 = builder.sub_extension(t2, output); - builder.mul_extension(t3, is_xor) - }; - - let andnot_constr = { - let t0 = builder.sub_extension(a, a_and_b); - let t1 = builder.sub_extension(t0, output); - builder.mul_extension(t1, is_andnot) - }; - - let constr = builder.add_many_extension([and_constr, ior_constr, xor_constr, andnot_constr]); - yield_constr.constraint(builder, constr); -} - -/// As for `eval_bitop` but with a builder. -pub(crate) fn eval_bitop_circuit, const D: usize>( - builder: &mut CircuitBuilder, - lv: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, -) { - // Recursive constraint for lo half - eval_bitop_32_circuit( - builder, - lv, - COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS, - COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS, - COL_BITOP_OUTPUT_0, - yield_constr, - ); - // Recursive constraint for hi half - eval_bitop_32_circuit( - builder, - lv, - COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS, - COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS, - COL_BITOP_OUTPUT_1, - yield_constr, - ); -} - -#[cfg(test)] -mod tests { - use plonky2::field::goldilocks_field::GoldilocksField; - use plonky2::field::types::Sample; - use rand::{Rng, SeedableRng}; - use rand_chacha::ChaCha8Rng; - use starky::constraint_consumer::ConstraintConsumer; - - use super::*; - use crate::registers::NUM_COLUMNS; - - #[test] - fn generate_eval_consistency_not_bitop() { - type F = GoldilocksField; - - let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25); - let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng)); - - // if `IS_bitop == 0`, then the constraints should be met even - // if all values are garbage. - for bitop in [IS_AND, IS_IOR, IS_XOR, IS_ANDNOT] { - values[bitop] = F::ZERO; - } - - let mut constrant_consumer = ConstraintConsumer::new( - vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)], - GoldilocksField::ONE, - GoldilocksField::ONE, - GoldilocksField::ONE, - ); - eval_bitop(&values, &mut constrant_consumer); - for &acc in &constrant_consumer.constraint_accs { - assert_eq!(acc, GoldilocksField::ZERO); - } - } - - #[test] - fn generate_eval_consistency_bitop() { - type F = GoldilocksField; - - let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25); - let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng)); - - const BITOPS: [usize; 4] = [IS_AND, IS_IOR, IS_XOR, IS_ANDNOT]; - for bitop in BITOPS { - // Reset all the instruction registers - for op in BITOPS { - values[op] = F::ZERO; - } - // set `IS_bitop == 1` and ensure all constraints are satisfied. - values[bitop] = F::ONE; - - // Set inputs to random binary values - let all_bin_regs = COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS - .into_iter() - .chain(COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS) - .chain(COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS) - .chain(COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS); - - for reg in all_bin_regs { - values[reg] = F::from_canonical_u32(rng.gen::() & 1); - } - - generate_bitop(&mut values, bitop); - - let mut constrant_consumer = ConstraintConsumer::new( - vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)], - GoldilocksField::ONE, - GoldilocksField::ONE, - GoldilocksField::ONE, - ); - eval_bitop(&values, &mut constrant_consumer); - for &acc in &constrant_consumer.constraint_accs { - assert_eq!(acc, GoldilocksField::ZERO); - } - } - } - - #[test] - fn generate_eval_consistency_bit_inputs() { - type F = GoldilocksField; - - let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25); - let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng)); - - const BITOPS: [usize; 4] = [IS_AND, IS_IOR, IS_XOR, IS_ANDNOT]; - for bitop in BITOPS { - // Reset all the instruction registers - for op in BITOPS { - values[op] = F::ZERO; - } - // set `IS_bitop == 1` and ensure all constraints are satisfied. - values[bitop] = F::ONE; - - // Set inputs to random binary values - let all_bin_regs = COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS - .into_iter() - .chain(COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS) - .chain(COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS) - .chain(COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS); - - for reg in all_bin_regs { - values[reg] = F::from_canonical_u32(rng.gen::() & 1); - } - // Make first "bit" non-binary. - values[COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS[0]] = F::TWO; - - generate_bitop(&mut values, bitop); - - let mut constrant_consumer = ConstraintConsumer::new( - vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)], - GoldilocksField::ONE, - GoldilocksField::ONE, - GoldilocksField::ONE, - ); - eval_bitop(&values, &mut constrant_consumer); - for &acc in &constrant_consumer.constraint_accs { - assert_ne!(acc, GoldilocksField::ZERO); - } - } - } - - // TODO: test eval_division_recursively. -} diff --git a/system_zero/src/alu/canonical.rs b/system_zero/src/alu/canonical.rs deleted file mode 100644 index bbc9e1a0..00000000 --- a/system_zero/src/alu/canonical.rs +++ /dev/null @@ -1,109 +0,0 @@ -//! Helper methods for checking that a value is canonical, i.e. is less than `|F|`. -//! -//! See https://hackmd.io/NC-yRmmtRQSvToTHb96e8Q#Checking-element-validity - -use plonky2::field::extension::Extendable; -use plonky2::field::packed::PackedField; -use plonky2::field::types::Field; -use plonky2::hash::hash_types::RichField; -use plonky2::iop::ext_target::ExtensionTarget; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; - -/// Computes the helper value used in the is-canonical check. -pub(crate) fn compute_canonical_inv(value_to_check: u64) -> F { - let value_hi_32 = (value_to_check >> 32) as u32; - - if value_hi_32 == u32::MAX { - debug_assert_eq!(value_to_check as u32, 0, "Value was not canonical."); - // In this case it doesn't matter what we put for the purported inverse value. The - // constraint containing this value will get multiplied by the low u32 limb, which will be - // zero, satisfying the constraint regardless of what we put here. - F::ZERO - } else { - F::from_canonical_u32(u32::MAX - value_hi_32).inverse() - } -} - -/// Adds constraints to require that a list of four `u16`s, in little-endian order, represent a -/// canonical field element, i.e. that their combined value is less than `|F|`. Returns their -/// combined value. -pub(crate) fn combine_u16s_check_canonical>( - limb_0_u16: P, - limb_1_u16: P, - limb_2_u16: P, - limb_3_u16: P, - inverse: P, - yield_constr: &mut ConstraintConsumer

, -) -> P { - let base = F::from_canonical_u32(1 << 16); - let limb_0_u32 = limb_0_u16 + limb_1_u16 * base; - let limb_1_u32 = limb_2_u16 + limb_3_u16 * base; - combine_u32s_check_canonical(limb_0_u32, limb_1_u32, inverse, yield_constr) -} - -/// Adds constraints to require that a list of four `u16`s, in little-endian order, represent a -/// canonical field element, i.e. that their combined value is less than `|F|`. Returns their -/// combined value. -pub(crate) fn combine_u16s_check_canonical_circuit, const D: usize>( - builder: &mut CircuitBuilder, - limb_0_u16: ExtensionTarget, - limb_1_u16: ExtensionTarget, - limb_2_u16: ExtensionTarget, - limb_3_u16: ExtensionTarget, - inverse: ExtensionTarget, - yield_constr: &mut RecursiveConstraintConsumer, -) -> ExtensionTarget { - let base = F::from_canonical_u32(1 << 16); - let limb_0_u32 = builder.mul_const_add_extension(base, limb_1_u16, limb_0_u16); - let limb_1_u32 = builder.mul_const_add_extension(base, limb_3_u16, limb_2_u16); - combine_u32s_check_canonical_circuit(builder, limb_0_u32, limb_1_u32, inverse, yield_constr) -} - -/// Adds constraints to require that a pair of `u32`s, in little-endian order, represent a canonical -/// field element, i.e. that their combined value is less than `|F|`. Returns their combined value. -pub(crate) fn combine_u32s_check_canonical>( - limb_0_u32: P, - limb_1_u32: P, - inverse: P, - yield_constr: &mut ConstraintConsumer

, -) -> P { - let u32_max = P::from(F::from_canonical_u32(u32::MAX)); - - // This is zero if and only if the high limb is `u32::MAX`. - let diff = u32_max - limb_1_u32; - // If this is zero, the diff is invertible, so the high limb is not `u32::MAX`. - let hi_not_max = inverse * diff - F::ONE; - // If this is zero, either the high limb is not `u32::MAX`, or the low limb is zero. - let hi_not_max_or_lo_zero = hi_not_max * limb_0_u32; - - yield_constr.constraint(hi_not_max_or_lo_zero); - - // Return the combined value. - limb_0_u32 + limb_1_u32 * F::from_canonical_u64(1 << 32) -} - -/// Adds constraints to require that a pair of `u32`s, in little-endian order, represent a canonical -/// field element, i.e. that their combined value is less than `|F|`. Returns their combined value. -pub(crate) fn combine_u32s_check_canonical_circuit, const D: usize>( - builder: &mut CircuitBuilder, - limb_0_u32: ExtensionTarget, - limb_1_u32: ExtensionTarget, - inverse: ExtensionTarget, - yield_constr: &mut RecursiveConstraintConsumer, -) -> ExtensionTarget { - let one = builder.one_extension(); - let u32_max = builder.constant_extension(F::Extension::from_canonical_u32(u32::MAX)); - - // This is zero if and only if the high limb is `u32::MAX`. - let diff = builder.sub_extension(u32_max, limb_1_u32); - // If this is zero, the diff is invertible, so the high limb is not `u32::MAX`. - let hi_not_max = builder.mul_sub_extension(inverse, diff, one); - // If this is zero, either the high limb is not `u32::MAX`, or the low limb is zero. - let hi_not_max_or_lo_zero = builder.mul_extension(hi_not_max, limb_0_u32); - - yield_constr.constraint(builder, hi_not_max_or_lo_zero); - - // Return the combined value. - builder.mul_const_add_extension(F::from_canonical_u64(1 << 32), limb_1_u32, limb_0_u32) -} diff --git a/system_zero/src/alu/div-constraints-proof.txt b/system_zero/src/alu/div-constraints-proof.txt deleted file mode 100644 index bd0b687c..00000000 --- a/system_zero/src/alu/div-constraints-proof.txt +++ /dev/null @@ -1,93 +0,0 @@ -Constraints A (implemented in code): -A1. dividend ∈ {0, …, u32::MAX} -A2. divisor ∈ {0, …, u32::MAX} -A3. quotient ∈ {0, …, u32::MAX} -A4. remainder ∈ {0, …, u32::MAX} -A5. divisor_rem_diff_m1 ∈ {0, …, u32::MAX} -A6. divisor * div_inverse = div_div_inverse -A7. (div_div_inverse - 1) * (remainder - quotient - u32::MAX) = 0 -A8. divisor * (div_div_inverse - 1) = 0 -A9. div_inverse * dividend = quotient + remainder * div_inverse -A10. divisor * (divisor - remainder - 1 - divisor_rem_diff_m1) = 0 - -Constraints B (intuitive division): -B1. dividend ∈ {0, …, u32::MAX} -B2. divisor ∈ {0, …, u32::MAX} -B3. divisor = 0 => quotient = 0 -B4. divisor = 0 => remainder = u32::MAX -B5. divisor ≠ 0 => dividend = quotient * divisor + remainder -B6. divisor ≠ 0 => quotient ∈ {0, …, u32::MAX} -B7. divisor ≠ 0 => remainder ∈ {0, …, divisor - 1} - - - -Assume we meet constraints A for some dividend, divisor, quotient, remainder, divisor_rem_diff_m1, div_inverse, and div_div_inverse. We want to show that constrants B are met. - -B1. Trivial by A1. - -B2. Trivial by A2. - -B3. Assume divisor = 0. Then div_div_inverse = 0 by A6. div_div_inverse - 1 ≠ 0, so remainder - quotient = u32::MAX by A7. -quotient ∈ {0, …, u32::MAX} by A3 and remainder ∈ {0, …, u32::MAX} by A4. Then remainder - quotient ∈ {-quotient, …, u32::MAX - quotient}. -If quotient ≠ 0, then quotient ∈ {1, …, u32::MAX} and remainder - quotient ∈ {-u32::MAX, …, u32::MAX - 1}, which does not include u32::MAX, contradicting A7. - -B4. Assume divisor = 0. Then div_div_inverse = 0 by A6. div_div_inverse - 1 ≠ 0, so remainder - quotient = u32::MAX by A7. -quotient ∈ {0, …, u32::MAX} by A3 and remainder ∈ {0, …, u32::MAX} by A4. Then remainder - quotient ∈ {remainder - u32::MAX, …, remainder}. -If remainder ≠ u32::MAX, then remainder ∈ {0, …, u32::MAX - 1} and remainder - quotient ∈ {-u32::MAX, …, u32::MAX - 1} which does not include u32::MAX, contradicting A7. - -B5. Assume divisor ≠ 0. By A8, div_div_inverse = 1. By A6, div_inverse = divisor^-1. Multiplying both sides of A9 by divisor, dividend = quotient * divisor + remainder. - -B6. Follows from A3. - -B7. remainder ∈ {0, …, u32::MAX} by A4. Assume divisor ≠ 0. Then divisor_rem_diff_m1 = divisor - remainder - 1 by A10. divisor ∈ {1, …, u32::MAX} by A2. If remainder ∈ {divisor, …, u32::MAX}, then divisor - remainder - 1 ∈ {-u32::MAX, …, u32::MAX - divisor} ⊆ {-u32::MAX, …, u32::MAX - 1}, contradicting A5. Hence, remainder ∈ {0, …, divisor - 1}. - - - -Assume we meet constraints B for some dividend, divisor, quotient, and remainder. We want to show -that there exist divisor_rem_diff_m1, div_inverse, div_div_inverse, such that constrants A are met. - -If divisor = 0, set divisor_rem_diff_m1 = 0, div_inverse = 0, div_div_inverse = 0. -Otherwise, set divisor_rem_diff_m1 = divisor - remainder - 1, div_inverse = divisor^-1, div_div_inverse = 1. - -A1. Trivial by B1. - -A2. Trivial by B2. - -The remainder is by cases: - -(divisor = 0) - - A3. Follows from B3. - - A4. Follows from B4. - - A5. Follows from our choice of divisor_rem_diff_m1 = 0. - - A6. Follows from our choice of div_div_inverse = 0. - - A7. quotient = 0 by B3. remainder = u32::MAX by B4. Then remainder - quotient = u32::MAX. - - A8. Trivial since divisor = 0. - - A9. By our choice, div_inverse = 0. quotient = 0 by B3. - - A10. Trivial since divisor = 0. - - -(divisor ≠ 0) - - A3. Follows from B6. - - A4. By B7, remainder ∈ {0, …, divisor - 1}, and by B2, divisor ∈ {0, …, u32::MAX}, implying that remainder ∈ {0, …, u32::MAX - 1}. - - A5. We've set divisor_rem_diff_m1 = divisor - remainder - 1. remainder ∈ {0, …, divisor - 1}, so divisor - remainder ∈ {1, …, divisor} and divisor - remainder - 1 = divisor_rem_diff_m1 ∈ {0, …, divisor - 1}. From B2, divisor ∈ {0, …, u32::MAX}, so divisor_rem_diff_m1 ∈ {0, …, u32::MAX - 1} as desired. - - A6. div_inverse = divisor^-1 by choice, so divisor * div_inverse = 1. div_div_inverse = 1 by choice. - - A7. div_div_inverse = 1 by choice, so div_div_inverse - 1 = 0. - - A8. div_div_inverse = 1 by choice, so div_div_inverse - 1 = 0. - - A9. From B5, dividend = quotient * divisor + remainder. Since divisor ≠ 0, div_inverse = divisor^-1 by choice. Multiplying both sides by div_inverse, dividend * div_inverse = quotient * divisor * div_inverse + remainder * div_inverse = quotient + remainder * div_inverse. - - A10. By our choice of divisor_rem_diff_m1 = divisor - remainder - 1. diff --git a/system_zero/src/alu/division.rs b/system_zero/src/alu/division.rs deleted file mode 100644 index 055aafd3..00000000 --- a/system_zero/src/alu/division.rs +++ /dev/null @@ -1,221 +0,0 @@ -use plonky2::field::extension::Extendable; -use plonky2::field::packed::PackedField; -use plonky2::field::types::{Field, PrimeField64}; -use plonky2::hash::hash_types::RichField; -use plonky2::iop::ext_target::ExtensionTarget; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; - -use crate::registers::alu::*; -use crate::registers::NUM_COLUMNS; - -/// Division instruction of a u32 divisor N into a u32 dividend D, -/// with u32 quotient Q and u32 remainder R. If D is not zero, then -/// the values will satisfy N = Q*D + R with 0 <= R < D. If D is -/// zero, then the remainder is set to the special value u32::MAX = -/// 2^32 - 1 (which is not a valid remainder for any nonzero D) and -/// the quotient is set to zero. In particular, no overflow is -/// possible. - -pub(crate) fn generate_division(values: &mut [F; NUM_COLUMNS]) { - let dividend = values[COL_DIV_INPUT_DIVIDEND].to_canonical_u64() as u32; - let divisor = values[COL_DIV_INPUT_DIVISOR].to_canonical_u64() as u32; - - // `COL_DIV_INVDIVISOR` is `divisor^-1` if `divisor != 0` and `0` otherwise. - // `COL_DIV_NONZERO_DIVISOR` is `1` if `divisor != 0` and `0` otherwise. - - // `COL_DIV_RANGE_CHECKED_TMP` is set to `divisor - rem - 1` if `divisor != 0` and `0` - // otherwise. This is used to ensure that `rem < divisor` when `divisor != 0`. - - if divisor == 0 { - // Outputs - values[COL_DIV_OUTPUT_QUOT_0] = F::ZERO; - values[COL_DIV_OUTPUT_QUOT_1] = F::ZERO; - values[COL_DIV_OUTPUT_REM_0] = F::from_canonical_u16(u16::MAX); - values[COL_DIV_OUTPUT_REM_1] = F::from_canonical_u16(u16::MAX); - - // Temporaries - values[COL_DIV_RANGE_CHECKED_TMP_0] = F::ZERO; - values[COL_DIV_RANGE_CHECKED_TMP_1] = F::ZERO; - values[COL_DIV_INVDIVISOR] = F::ZERO; - values[COL_DIV_NONZERO_DIVISOR] = F::ZERO; - } else { - let quo = dividend / divisor; - let rem = dividend % divisor; - - let div_rem_diff_m1 = divisor - rem - 1; - - // Outputs - values[COL_DIV_OUTPUT_QUOT_0] = F::from_canonical_u16(quo as u16); - values[COL_DIV_OUTPUT_QUOT_1] = F::from_canonical_u16((quo >> 16) as u16); - values[COL_DIV_OUTPUT_REM_0] = F::from_canonical_u16(rem as u16); - values[COL_DIV_OUTPUT_REM_1] = F::from_canonical_u16((rem >> 16) as u16); - - // Temporaries - values[COL_DIV_RANGE_CHECKED_TMP_0] = F::from_canonical_u16(div_rem_diff_m1 as u16); - values[COL_DIV_RANGE_CHECKED_TMP_1] = F::from_canonical_u16((div_rem_diff_m1 >> 16) as u16); - values[COL_DIV_INVDIVISOR] = F::from_canonical_u32(divisor).inverse(); - values[COL_DIV_NONZERO_DIVISOR] = F::ONE; - } -} - -pub(crate) fn eval_division>( - lv: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, -) { - let base = F::from_canonical_u64(1 << 16); - let u32_max = P::from(F::from_canonical_u32(u32::MAX)); - - // Filter - let is_div = lv[IS_DIV]; - - // Inputs - let dividend = lv[COL_DIV_INPUT_DIVIDEND]; - let divisor = lv[COL_DIV_INPUT_DIVISOR]; - - // Outputs - let quotient = lv[COL_DIV_OUTPUT_QUOT_0] + lv[COL_DIV_OUTPUT_QUOT_1] * base; - let remainder = lv[COL_DIV_OUTPUT_REM_0] + lv[COL_DIV_OUTPUT_REM_1] * base; - - // Temporaries - let divinv = lv[COL_DIV_INVDIVISOR]; - let div_divinv = lv[COL_DIV_NONZERO_DIVISOR]; - let div_rem_diff_m1 = lv[COL_DIV_RANGE_CHECKED_TMP_0] + lv[COL_DIV_RANGE_CHECKED_TMP_1] * base; - - // Constraints - yield_constr.constraint(is_div * (divisor * divinv - div_divinv)); - yield_constr.constraint(is_div * (div_divinv - F::ONE) * (remainder - quotient - u32_max)); - yield_constr.constraint(is_div * divisor * (div_divinv - F::ONE)); - yield_constr.constraint(is_div * (quotient + remainder * divinv - divinv * dividend)); - yield_constr.constraint(is_div * divisor * (divisor - remainder - F::ONE - div_rem_diff_m1)); -} - -pub(crate) fn eval_division_circuit, const D: usize>( - builder: &mut CircuitBuilder, - lv: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, -) { - let base = builder.constant_extension(F::Extension::from_canonical_u64(1 << 16)); - let u32_max = builder.constant_extension(F::Extension::from_canonical_u32(u32::MAX)); - let one = builder.constant_extension(F::Extension::ONE); - - // Filter - let is_div = lv[IS_DIV]; - - // Inputs - let dividend = lv[COL_DIV_INPUT_DIVIDEND]; - let divisor = lv[COL_DIV_INPUT_DIVISOR]; - - // Outputs - let quotient = - builder.mul_add_extension(lv[COL_DIV_OUTPUT_QUOT_1], base, lv[COL_DIV_OUTPUT_QUOT_0]); - let remainder = - builder.mul_add_extension(lv[COL_DIV_OUTPUT_REM_1], base, lv[COL_DIV_OUTPUT_REM_0]); - - // Temporaries - let divinv = lv[COL_DIV_INVDIVISOR]; - let div_divinv = lv[COL_DIV_NONZERO_DIVISOR]; - let div_rem_diff_m1 = builder.mul_add_extension( - lv[COL_DIV_RANGE_CHECKED_TMP_1], - base, - lv[COL_DIV_RANGE_CHECKED_TMP_0], - ); - - // Constraints - let constr6 = builder.mul_sub_extension(divisor, divinv, div_divinv); - let constr7 = { - let t = builder.sub_extension(div_divinv, one); - let u = builder.sub_extension(remainder, quotient); - let v = builder.sub_extension(u, u32_max); - builder.mul_extension(t, v) - }; - let constr8 = { - let t = builder.sub_extension(div_divinv, one); - builder.mul_extension(divisor, t) - }; - let constr9 = { - let t = builder.sub_extension(remainder, dividend); - builder.mul_add_extension(t, divinv, quotient) - }; - let constr10 = { - let t = builder.sub_extension(divisor, remainder); - let u = builder.add_extension(one, div_rem_diff_m1); - let v = builder.sub_extension(t, u); - builder.mul_extension(divisor, v) - }; - - let constr6 = builder.mul_extension(is_div, constr6); - let constr7 = builder.mul_extension(is_div, constr7); - let constr8 = builder.mul_extension(is_div, constr8); - let constr9 = builder.mul_extension(is_div, constr9); - let constr10 = builder.mul_extension(is_div, constr10); - - yield_constr.constraint(builder, constr6); - yield_constr.constraint(builder, constr7); - yield_constr.constraint(builder, constr8); - yield_constr.constraint(builder, constr9); - yield_constr.constraint(builder, constr10); -} - -#[cfg(test)] -mod tests { - use plonky2::field::goldilocks_field::GoldilocksField; - use plonky2::field::types::Sample; - use rand::{Rng, SeedableRng}; - use rand_chacha::ChaCha8Rng; - use starky::constraint_consumer::ConstraintConsumer; - - use super::*; - use crate::registers::NUM_COLUMNS; - - #[test] - fn generate_eval_consistency_not_div() { - type F = GoldilocksField; - - let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25); - let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng)); - - // if `IS_DIV == 0`, then the constraints should be met even if all values are garbage. - values[IS_DIV] = F::ZERO; - - let mut constrant_consumer = ConstraintConsumer::new( - vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)], - GoldilocksField::ONE, - GoldilocksField::ONE, - GoldilocksField::ONE, - ); - eval_division(&values, &mut constrant_consumer); - for &acc in &constrant_consumer.constraint_accs { - assert_eq!(acc, GoldilocksField::ZERO); - } - } - - #[test] - fn generate_eval_consistency_div() { - type F = GoldilocksField; - - let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25); - let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng)); - - // set `IS_DIV == 1` and ensure all constraints are satisfied. - values[IS_DIV] = F::ONE; - // set `DIVIDEND` and `DIVISOR` to `u32`s - values[COL_DIV_INPUT_DIVIDEND] = F::from_canonical_u32(rng.gen::()); - values[COL_DIV_INPUT_DIVISOR] = F::from_canonical_u32(rng.gen::()); - - generate_division(&mut values); - - let mut constrant_consumer = ConstraintConsumer::new( - vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)], - GoldilocksField::ONE, - GoldilocksField::ONE, - GoldilocksField::ONE, - ); - eval_division(&values, &mut constrant_consumer); - for &acc in &constrant_consumer.constraint_accs { - assert_eq!(acc, GoldilocksField::ZERO); - } - } - - // TODO: test eval_division_recursively. -} diff --git a/system_zero/src/alu/mod.rs b/system_zero/src/alu/mod.rs deleted file mode 100644 index a02a51e2..00000000 --- a/system_zero/src/alu/mod.rs +++ /dev/null @@ -1,107 +0,0 @@ -use plonky2::field::extension::Extendable; -use plonky2::field::packed::PackedField; -use plonky2::field::types::{Field, PrimeField64}; -use plonky2::hash::hash_types::RichField; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use starky::vars::{StarkEvaluationTargets, StarkEvaluationVars}; - -use crate::alu::addition::{eval_addition, eval_addition_circuit, generate_addition}; -use crate::alu::bitops::{eval_bitop, eval_bitop_circuit, generate_bitop}; -use crate::alu::division::{eval_division, eval_division_circuit, generate_division}; -use crate::alu::mul_add::{eval_mul_add, eval_mul_add_circuit, generate_mul_add}; -use crate::alu::rotate_shift::{ - eval_rotate_left, eval_rotate_left_circuit, eval_rotate_right, eval_rotate_right_circuit, - eval_shift_left, eval_shift_left_circuit, eval_shift_right, eval_shift_right_circuit, - generate_rotate_shift, -}; -use crate::alu::subtraction::{eval_subtraction, eval_subtraction_circuit, generate_subtraction}; -use crate::public_input_layout::NUM_PUBLIC_INPUTS; -use crate::registers::alu::*; -use crate::registers::NUM_COLUMNS; - -mod addition; -mod bitops; -mod canonical; -mod division; -mod mul_add; -mod rotate_shift; -mod subtraction; - -pub(crate) fn generate_alu(values: &mut [F; NUM_COLUMNS]) { - if values[IS_ADD].is_one() { - generate_addition(values); - } else if values[IS_SUB].is_one() { - generate_subtraction(values); - } else if values[IS_MUL_ADD].is_one() { - generate_mul_add(values); - } else if values[IS_DIV].is_one() { - generate_division(values); - } else if values[IS_AND].is_one() { - generate_bitop(values, IS_AND); - } else if values[IS_IOR].is_one() { - generate_bitop(values, IS_IOR); - } else if values[IS_XOR].is_one() { - generate_bitop(values, IS_XOR); - } else if values[IS_ANDNOT].is_one() { - generate_bitop(values, IS_ANDNOT); - } else if values[IS_ROTATE_LEFT].is_one() { - generate_rotate_shift(values, IS_ROTATE_LEFT); - } else if values[IS_ROTATE_RIGHT].is_one() { - generate_rotate_shift(values, IS_ROTATE_RIGHT); - } else if values[IS_SHIFT_LEFT].is_one() { - generate_rotate_shift(values, IS_SHIFT_LEFT); - } else if values[IS_SHIFT_RIGHT].is_one() { - generate_rotate_shift(values, IS_SHIFT_RIGHT); - } else { - //todo!("the requested operation has not yet been implemented"); - } -} - -pub(crate) fn eval_alu>( - vars: StarkEvaluationVars, - yield_constr: &mut ConstraintConsumer

, -) { - let local_values = &vars.local_values; - - // Check that the operation flag values are binary. - for col in ALL_OPERATIONS { - let val = local_values[col]; - yield_constr.constraint(val * val - val); - } - - eval_addition(local_values, yield_constr); - eval_subtraction(local_values, yield_constr); - eval_mul_add(local_values, yield_constr); - eval_division(local_values, yield_constr); - eval_bitop(local_values, yield_constr); - eval_rotate_left(local_values, yield_constr); - eval_rotate_right(local_values, yield_constr); - eval_shift_left(local_values, yield_constr); - eval_shift_right(local_values, yield_constr); -} - -pub(crate) fn eval_alu_circuit, const D: usize>( - builder: &mut CircuitBuilder, - vars: StarkEvaluationTargets, - yield_constr: &mut RecursiveConstraintConsumer, -) { - let local_values = &vars.local_values; - - // Check that the operation flag values are binary. - for col in ALL_OPERATIONS { - let val = local_values[col]; - let constraint = builder.mul_sub_extension(val, val, val); - yield_constr.constraint(builder, constraint); - } - - eval_addition_circuit(builder, local_values, yield_constr); - eval_subtraction_circuit(builder, local_values, yield_constr); - eval_mul_add_circuit(builder, local_values, yield_constr); - eval_division_circuit(builder, local_values, yield_constr); - eval_bitop_circuit(builder, local_values, yield_constr); - eval_rotate_left_circuit(builder, local_values, yield_constr); - eval_rotate_right_circuit(builder, local_values, yield_constr); - eval_shift_left_circuit(builder, local_values, yield_constr); - eval_shift_right_circuit(builder, local_values, yield_constr); -} diff --git a/system_zero/src/alu/mul_add.rs b/system_zero/src/alu/mul_add.rs deleted file mode 100644 index 39484bf8..00000000 --- a/system_zero/src/alu/mul_add.rs +++ /dev/null @@ -1,91 +0,0 @@ -use plonky2::field::extension::Extendable; -use plonky2::field::packed::PackedField; -use plonky2::field::types::{Field, PrimeField64}; -use plonky2::hash::hash_types::RichField; -use plonky2::iop::ext_target::ExtensionTarget; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use plonky2_util::assume; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; - -use crate::alu::canonical::*; -use crate::registers::alu::*; -use crate::registers::NUM_COLUMNS; - -pub(crate) fn generate_mul_add(values: &mut [F; NUM_COLUMNS]) { - let factor_0 = values[COL_MUL_ADD_FACTOR_0].to_canonical_u64(); - let factor_1 = values[COL_MUL_ADD_FACTOR_1].to_canonical_u64(); - let addend = values[COL_MUL_ADD_ADDEND].to_canonical_u64(); - - // Let the compiler know that each input must fit in 32 bits. - assume(factor_0 <= u32::MAX as u64); - assume(factor_1 <= u32::MAX as u64); - assume(addend <= u32::MAX as u64); - - let output = factor_0 * factor_1 + addend; - - // An advice value used to help verify that the limbs represent a canonical field element. - values[COL_MUL_ADD_RESULT_CANONICAL_INV] = compute_canonical_inv(output); - - values[COL_MUL_ADD_OUTPUT_0] = F::from_canonical_u16(output as u16); - values[COL_MUL_ADD_OUTPUT_1] = F::from_canonical_u16((output >> 16) as u16); - values[COL_MUL_ADD_OUTPUT_2] = F::from_canonical_u16((output >> 32) as u16); - values[COL_MUL_ADD_OUTPUT_3] = F::from_canonical_u16((output >> 48) as u16); -} - -pub(crate) fn eval_mul_add>( - local_values: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, -) { - let is_mul = local_values[IS_MUL_ADD]; - let factor_0 = local_values[COL_MUL_ADD_FACTOR_0]; - let factor_1 = local_values[COL_MUL_ADD_FACTOR_1]; - let addend = local_values[COL_MUL_ADD_ADDEND]; - let output_1 = local_values[COL_MUL_ADD_OUTPUT_0]; - let output_2 = local_values[COL_MUL_ADD_OUTPUT_1]; - let output_3 = local_values[COL_MUL_ADD_OUTPUT_2]; - let output_4 = local_values[COL_MUL_ADD_OUTPUT_3]; - let result_canonical_inv = local_values[COL_MUL_ADD_RESULT_CANONICAL_INV]; - - let computed_output = factor_0 * factor_1 + addend; - // TODO: Needs to be filtered by IS_MUL_ADD. - let output = combine_u16s_check_canonical( - output_1, - output_2, - output_3, - output_4, - result_canonical_inv, - yield_constr, - ); - yield_constr.constraint(is_mul * (computed_output - output)); -} - -pub(crate) fn eval_mul_add_circuit, const D: usize>( - builder: &mut CircuitBuilder, - local_values: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, -) { - let is_mul = local_values[IS_MUL_ADD]; - let factor_0 = local_values[COL_MUL_ADD_FACTOR_0]; - let factor_1 = local_values[COL_MUL_ADD_FACTOR_1]; - let addend = local_values[COL_MUL_ADD_ADDEND]; - let output_1 = local_values[COL_MUL_ADD_OUTPUT_0]; - let output_2 = local_values[COL_MUL_ADD_OUTPUT_1]; - let output_3 = local_values[COL_MUL_ADD_OUTPUT_2]; - let output_4 = local_values[COL_MUL_ADD_OUTPUT_3]; - let result_canonical_inv = local_values[COL_MUL_ADD_RESULT_CANONICAL_INV]; - - let computed_output = builder.mul_add_extension(factor_0, factor_1, addend); - // TODO: Needs to be filtered by IS_MUL_ADD. - let output = combine_u16s_check_canonical_circuit( - builder, - output_1, - output_2, - output_3, - output_4, - result_canonical_inv, - yield_constr, - ); - let diff = builder.sub_extension(computed_output, output); - let filtered_diff = builder.mul_extension(is_mul, diff); - yield_constr.constraint(builder, filtered_diff); -} diff --git a/system_zero/src/alu/rotate_shift.rs b/system_zero/src/alu/rotate_shift.rs deleted file mode 100644 index 87d54f0c..00000000 --- a/system_zero/src/alu/rotate_shift.rs +++ /dev/null @@ -1,645 +0,0 @@ -use plonky2::field::extension::Extendable; -use plonky2::field::packed::PackedField; -use plonky2::field::types::{Field, PrimeField64}; -use plonky2::hash::hash_types::RichField; -use plonky2::iop::ext_target::ExtensionTarget; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; - -use crate::alu::bitops::constrain_all_to_bits_circuit; -use crate::registers::alu::*; -use crate::registers::NUM_COLUMNS; - -/// ROTATE and SHIFT instructions -/// -/// To rotate a 64bit value by DELTA bit positions, the input is -/// -/// - a 64-bit integer X to be rotated/shifted, given as high and low 32-bit -/// words X_lo and X_hi. -/// - a 32-bit integer EXP (given as its 5 bits) which is either DELTA -/// mod 32, if the operation direction is left, or (32 - (DELTA mod 32)) -/// mod 32 if the operation direction is right. -/// - a single bit DELTA_DIV32 which is 1 if DELTA is >= 32 and 0 otherwise -/// - the value POW_EXP = 2^EXP, as well as three auxiliary values POW_EXP_AUX_[012] -/// to verify that POW_EXP == 2^EXP -/// - two 64-bit integers, INPUT_LO_DISPLACED and INPUT_HI_DISPLACED, -/// with INPUT_LO_DISPLACED being the high and low 32-bit words of -/// the value 2^EXP * X_lo; similarly for INPUT_HI_DISPLACED. -/// - two 64-bit auxiliary values DISPLACED_INPUT_{LO,HI}_AUX, one -/// each for INPUT_LO_DISPLACED and INPUT_HI_DISPLACED, used to prove -/// that INPUT_LO_DISPLACED and INPUT_HI_DISPLACED are valid -/// Goldilocks elements. - -pub(crate) fn generate_rotate_shift(values: &mut [F; NUM_COLUMNS], op: usize) { - // input_{lo,hi} are the 32-bit lo and hi words of the input - let input_lo = values[COL_ROTATE_SHIFT_INPUT_LO].to_canonical_u64(); - let input_hi = values[COL_ROTATE_SHIFT_INPUT_HI].to_canonical_u64(); - - // Given the 6 bits delta_bits[0..5], bits 0..4 represent - // delta_mod32 for left ops and (32 - delta_mod32) % 32 for right - // ops, and delta_bits[5] represents whether delta >= 32. - - // delta is the displacement amount. EXP_BITS holds the 5 bits of - // either delta mod 32 (for left ops) or (32 - (delta mod 32)) mod 32 - // for right ops. - let exp_bits = COL_ROTATE_SHIFT_EXP_BITS.map(|r| values[r].to_canonical_u64()); - - let is_right_op = op == IS_ROTATE_RIGHT || op == IS_SHIFT_RIGHT || op == IS_ARITH_SHIFT_RIGHT; - let exp: u64 = [0, 1, 2, 3, 4].map(|i| exp_bits[i] << i).into_iter().sum(); - let delta_mod32 = if is_right_op { (32u64 - exp) % 32 } else { exp }; - let exp_ge32_bit = values[COL_ROTATE_SHIFT_DELTA_DIV32].to_canonical_u64(); - let delta = (exp_ge32_bit << 5) + delta_mod32; - - // helper values - let pow_exp_aux_0 = (exp_bits[0] + 1) * (3 * exp_bits[1] + 1); - let pow_exp_aux_1 = (15 * exp_bits[2] + 1) * (255 * exp_bits[3] + 1); - let pow_exp_aux_2 = pow_exp_aux_0 * pow_exp_aux_1; - let pow_exp = pow_exp_aux_2 * (65535 * exp_bits[4] + 1); - values[COL_ROTATE_SHIFT_POW_EXP_AUX_0] = F::from_canonical_u64(pow_exp_aux_0); - values[COL_ROTATE_SHIFT_POW_EXP_AUX_1] = F::from_canonical_u64(pow_exp_aux_1); - values[COL_ROTATE_SHIFT_POW_EXP_AUX_2] = F::from_canonical_u64(pow_exp_aux_2); - values[COL_ROTATE_SHIFT_POW_EXP] = F::from_canonical_u64(pow_exp); - - let lo_shifted = input_lo << exp; - let lo_shifted_0 = lo_shifted as u32; - let lo_shifted_1 = (lo_shifted >> 32) as u32; - values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0] = F::from_canonical_u32(lo_shifted_0); - values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1] = F::from_canonical_u32(lo_shifted_1); - let hi_shifted = input_hi << exp; - let hi_shifted_0 = hi_shifted as u32; - let hi_shifted_1 = (hi_shifted >> 32) as u32; - values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0] = F::from_canonical_u32(hi_shifted_0); - values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1] = F::from_canonical_u32(hi_shifted_1); - - if lo_shifted_1 != u32::MAX { - let diff = F::from_canonical_u32(u32::MAX - lo_shifted_1); - let inv = diff.inverse(); - values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_0] = inv; - values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_1] = diff * inv; - } else { - // lo_shifted_0 must be zero, so this is unused. - values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_0] = F::ZERO; - values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_1] = F::ZERO; - } - if hi_shifted_1 != u32::MAX { - let diff = F::from_canonical_u32(u32::MAX - hi_shifted_1); - let inv = diff.inverse(); - values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_0] = inv; - values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_1] = diff * inv; - } else { - // hi_shifted_0 must be zero, so this is unused. - values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_0] = F::ZERO; - values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_1] = F::ZERO; - } - - // the input and output as u64s - let input = (input_hi << 32) | input_lo; - let delta = delta as u32; - let output = match op { - IS_ROTATE_LEFT => input.rotate_left(delta), - IS_ROTATE_RIGHT => input.rotate_right(delta), - IS_SHIFT_LEFT => input << delta, - IS_SHIFT_RIGHT => input >> delta, - IS_ARITH_SHIFT_RIGHT => (input as i64 >> delta) as u64, - _ => panic!("unrecognized rotate/shift instruction code"), - }; - - // Output in base 2^16. - values[COL_ROTATE_SHIFT_OUTPUT_0] = F::from_canonical_u32(output as u32); - values[COL_ROTATE_SHIFT_OUTPUT_1] = F::from_canonical_u32((output >> 32) as u32); -} - -/// Check that pow_exp = 2^exp, where exp is formed from the bits -/// exp_bits[0..4]. -/// -/// 2^exp = \prod_i=0^4 (2^(2^i) if exp_bits[i] = 1 else 1) -/// = \prod_i=0^4 ((2^(2^i) - 1) * exp_bits[i] + 1) -/// = pow_exp -/// -/// on the conditions that: -/// -/// pow_exp_aux_0 = \prod_i=0^1 ((2^i - 1) * exp_bits[i] + 1) -/// pow_exp_aux_1 = \prod_i=2^3 ((2^i - 1) * exp_bits[i] + 1) -/// pow_exp_aux_2 = pow_exp_aux_0 * pow_exp_aux_1 -/// pow_exp_mod32 = pow_exp_aux_2 * ((2^(2^4) - 1) * exp_bits[4] + 1) -/// -/// Also check that every "bit" of exp_bits and exp_ge32_bit is 0 or 1. -fn constrain_pow_exp>( - lv: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, - filter: P, -) { - let exp_bits = COL_ROTATE_SHIFT_EXP_BITS.map(|r| lv[r]); - let exp_ge32_bit = lv[COL_ROTATE_SHIFT_DELTA_DIV32]; - - let pow_exp_aux_0 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_0]; - let pow_exp_aux_1 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_1]; - let pow_exp_aux_2 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_2]; - let pow_exp = lv[COL_ROTATE_SHIFT_POW_EXP]; - - // Check that every "bit" of exp_bits and exp_ge32_bit is 0 or 1 - exp_bits.map(|b| yield_constr.constraint(filter * (b * b - b))); - yield_constr.constraint(filter * (exp_ge32_bit * exp_ge32_bit - exp_ge32_bit)); - - // c[i-1] = 2^(2^i) - 1 - let c = [1, 2, 3, 4].map(|i| P::from(F::from_canonical_u64(1u64 << (1u32 << i))) - P::ONES); - - let constr1 = (exp_bits[0] + P::ONES) * (c[0] * exp_bits[1] + P::ONES); - yield_constr.constraint(filter * (constr1 - pow_exp_aux_0)); - let constr2 = (c[1] * exp_bits[2] + P::ONES) * (c[2] * exp_bits[3] + P::ONES); - yield_constr.constraint(filter * (constr2 - pow_exp_aux_1)); - let constr3 = pow_exp_aux_0 * pow_exp_aux_1; - yield_constr.constraint(filter * (constr3 - pow_exp_aux_2)); - let constr4 = pow_exp_aux_2 * (c[3] * exp_bits[4] + P::ONES); - yield_constr.constraint(filter * (constr4 - pow_exp)); -} - -/// An invalid lo_shifted (or _hi) can be too big to fit in Goldilocks -/// field; e.g. if both _0 and _1 parts are 2^32-1, then lo_shifted = -/// 2^32 - 1 + 2^32 (2^32 - 1) = 2^64 - 1 which overflows in -/// GoldilocksField. Hence we check that {lo,hi}_shifted are valid -/// Goldilocks elements following -/// https:///hackmd.io/NC-yRmmtRQSvToTHb96e8Q#Checking-element-validity -/// -/// The idea is check that a value v = (v_lo, v_hi) (32-bit words) -/// satisfies the condition (v_lo == 0 OR v_hi != 2^32-1), which uses -/// the structure of Goldilocks to check that v has the right form. -/// The formula is: -/// v_lo * (one - aux * (u32_max - v_hi)) == 0 -/// where aux = (m32_max - v_hi)^-1 if it exists. -fn constrain_shifted_are_valid>( - lv: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, - filter: P, -) { - let lo_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0]; - let lo_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1]; - let hi_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0]; - let hi_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1]; - let lo_shifted_aux_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_0]; - let lo_shifted_aux_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_1]; - let hi_shifted_aux_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_0]; - let hi_shifted_aux_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_1]; - - // u32_max = 2^32 - 1 - let u32_max = P::from(F::from_canonical_u32(u32::MAX)); - - let constr1 = lo_shifted_aux_0 * (u32_max - lo_shifted_1); - yield_constr.constraint(filter * (constr1 - lo_shifted_aux_1)); - let constr2 = hi_shifted_aux_0 * (u32_max - hi_shifted_1); - yield_constr.constraint(filter * (constr2 - hi_shifted_aux_1)); - - let lo_shifted_is_valid = lo_shifted_0 * (P::ONES - lo_shifted_aux_1); - let hi_shifted_is_valid = hi_shifted_0 * (P::ONES - hi_shifted_aux_1); - - yield_constr.constraint(filter * lo_shifted_is_valid); - yield_constr.constraint(filter * hi_shifted_is_valid); -} - -fn eval_rotate_shift>( - lv: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, - filter: P, -) -> (P, P, P, P, P, P, P) { - // Input - let input_lo = lv[COL_ROTATE_SHIFT_INPUT_LO]; - let input_hi = lv[COL_ROTATE_SHIFT_INPUT_HI]; - - // Delta is the shift/rotate displacement; exp is delta mod 32 or - // (32 - (delta mod 32)) mod 32, depending on whether the operation - // direction is left or right. - let exp_ge32_bit = lv[COL_ROTATE_SHIFT_DELTA_DIV32]; - let pow_exp = lv[COL_ROTATE_SHIFT_POW_EXP]; - - let lo_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0]; - let lo_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1]; - let hi_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0]; - let hi_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1]; - - // Output - let output_lo = lv[COL_ROTATE_SHIFT_OUTPUT_0]; - let output_hi = lv[COL_ROTATE_SHIFT_OUTPUT_1]; - - constrain_pow_exp(lv, yield_constr, filter); - constrain_shifted_are_valid(lv, yield_constr, filter); - - // Check - // 2^exp * input_lo == lo_shifted_0 + 2^32 * lo_shifted_1 - // 2^exp * input_hi == hi_shifted_0 + 2^32 * hi_shifted_1 - - let base = F::from_canonical_u64(1u64 << 32); - let lo_shifted = lo_shifted_0 + lo_shifted_1 * base; - let hi_shifted = hi_shifted_0 + hi_shifted_1 * base; - - // exp must be <= 32 for this to never overflow in - // GoldilocksField: since 0 <= input_{lo,hi} <= 2^32 - 1, - // input_{lo,hi} * 2^32 <= 2^64 - 2^32 < 2^64 - 2^32 + 1 = Goldilocks. - let lo_shifted_expected = input_lo * pow_exp; - let hi_shifted_expected = input_hi * pow_exp; - - yield_constr.constraint(filter * (lo_shifted_expected - lo_shifted)); - yield_constr.constraint(filter * (hi_shifted_expected - hi_shifted)); - - ( - exp_ge32_bit, - lo_shifted_0, - lo_shifted_1, - hi_shifted_0, - hi_shifted_1, - output_lo, - output_hi, - ) -} - -pub(crate) fn eval_rotate_left>( - lv: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, -) { - let is_rol = lv[IS_ROTATE_LEFT]; - let one = P::ONES; - - let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) = - eval_rotate_shift(lv, yield_constr, is_rol); - - // Intuitively we want to do this (which works when delta <= 32): - //let lo_constr = hi_shifted_1 + lo_shifted_0 - output_lo; - //let hi_constr = lo_shifted_1 + hi_shifted_0 - output_hi; - - // If delta_bits[5] == 0, then delta < 32, so we use the bottom term. - // Otherwise delta_bits[5] == 1, so 32 <= delta < 64 and we need - // to swap the constraints for the hi and lo halves; hence we use - // the bottom term which is the top term from hi_constr. - let lo_constr = (one - delta_ge32) * (hi_shifted_1 + lo_shifted_0 - output_lo) - + delta_ge32 * (lo_shifted_1 + hi_shifted_0 - output_lo); - let hi_constr = (one - delta_ge32) * (lo_shifted_1 + hi_shifted_0 - output_hi) - + delta_ge32 * (hi_shifted_1 + lo_shifted_0 - output_hi); - yield_constr.constraint(is_rol * lo_constr); - yield_constr.constraint(is_rol * hi_constr); -} - -pub(crate) fn eval_rotate_right>( - lv: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, -) { - let is_ror = lv[IS_ROTATE_RIGHT]; - let one = P::ONES; - - let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) = - eval_rotate_shift(lv, yield_constr, is_ror); - - // Intuitively we want to do this (which works when delta <= 32): - // let lo_constr = lo_shifted_1 + hi_shifted_0 - output_lo; - // let hi_constr = hi_shifted_1 + lo_shifted_0 - output_hi; - - let lo_constr = (one - delta_ge32) * (lo_shifted_1 + hi_shifted_0 - output_lo) - + delta_ge32 * (hi_shifted_1 + lo_shifted_0 - output_lo); - let hi_constr = (one - delta_ge32) * (hi_shifted_1 + lo_shifted_0 - output_hi) - + delta_ge32 * (lo_shifted_1 + hi_shifted_0 - output_hi); - yield_constr.constraint(is_ror * lo_constr); - yield_constr.constraint(is_ror * hi_constr); -} - -pub(crate) fn eval_shift_left>( - lv: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, -) { - let is_shl = lv[IS_SHIFT_LEFT]; - let one = P::ONES; - - let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, _hi_shifted_1, output_lo, output_hi) = - eval_rotate_shift(lv, yield_constr, is_shl); - - // Intuitively we want to do this (which works when delta <= 32): - //let lo_constr = lo_shifted_0 - output_lo; - //let hi_constr = lo_shifted_1 + hi_shifted_0 - output_hi; - - let lo_constr = - (one - delta_ge32) * (lo_shifted_0 - output_lo) + delta_ge32 * (P::ZEROS - output_lo); - let hi_constr = (one - delta_ge32) * (lo_shifted_1 + hi_shifted_0 - output_hi) - + delta_ge32 * (lo_shifted_0 - output_hi); - yield_constr.constraint(is_shl * lo_constr); - yield_constr.constraint(is_shl * hi_constr); -} - -pub(crate) fn eval_shift_right>( - lv: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, -) { - let is_shl = lv[IS_SHIFT_LEFT]; - let one = P::ONES; - - let (delta_ge32, _lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) = - eval_rotate_shift(lv, yield_constr, is_shl); - - // Intuitively we want to do this (which works when delta <= 32): - //let lo_constr = lo_shifted_1 + hi_shifted_0 - output_hi; - //let hi_constr = hi_shifted_1 - output_lo; - - let lo_constr = (one - delta_ge32) * (lo_shifted_1 + hi_shifted_0 - output_lo) - + delta_ge32 * (hi_shifted_1 - output_lo); - let hi_constr = - (one - delta_ge32) * (hi_shifted_1 - output_hi) + delta_ge32 * (P::ZEROS - output_hi); - yield_constr.constraint(is_shl * lo_constr); - yield_constr.constraint(is_shl * hi_constr); -} - -fn constrain_pow_exp_circuit, const D: usize>( - builder: &mut CircuitBuilder, - lv: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, - filter: ExtensionTarget, -) { - let exp_bits = COL_ROTATE_SHIFT_EXP_BITS.map(|r| lv[r]); - let exp_ge32_bit = lv[COL_ROTATE_SHIFT_DELTA_DIV32]; - - let pow_exp_aux_0 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_0]; - let pow_exp_aux_1 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_1]; - let pow_exp_aux_2 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_2]; - let pow_exp = lv[COL_ROTATE_SHIFT_POW_EXP]; - - // Check that every "bit" of exp_bits and exp_ge32_bit is 0 or 1 - constrain_all_to_bits_circuit(builder, yield_constr, filter, &exp_bits); - constrain_all_to_bits_circuit(builder, yield_constr, filter, &[exp_ge32_bit]); - - let one = builder.one_extension(); - // c[i-1] = 2^(2^i) - 1 - let c = [1, 2, 3, 4].map(|i| F::from_canonical_u64(1u64 << (1u32 << i)) - F::ONE); - - let constr1 = { - let t0 = builder.add_extension(exp_bits[0], one); - let t1 = builder.mul_const_add_extension(c[0], exp_bits[1], one); - let t2 = builder.mul_sub_extension(t0, t1, pow_exp_aux_0); - builder.mul_extension(filter, t2) - }; - yield_constr.constraint(builder, constr1); - let constr2 = { - let t0 = builder.mul_const_add_extension(c[1], exp_bits[2], one); - let t1 = builder.mul_const_add_extension(c[2], exp_bits[3], one); - let t2 = builder.mul_sub_extension(t0, t1, pow_exp_aux_1); - builder.mul_extension(filter, t2) - }; - yield_constr.constraint(builder, constr2); - let constr3 = { - let t0 = builder.mul_sub_extension(pow_exp_aux_0, pow_exp_aux_1, pow_exp_aux_2); - builder.mul_extension(filter, t0) - }; - yield_constr.constraint(builder, constr3); - let constr4 = { - let t0 = builder.mul_const_add_extension(c[3], exp_bits[4], one); - let t1 = builder.mul_sub_extension(pow_exp_aux_2, t0, pow_exp); - builder.mul_extension(filter, t1) - }; - yield_constr.constraint(builder, constr4); -} - -fn constrain_shifted_are_valid_circuit, const D: usize>( - builder: &mut CircuitBuilder, - lv: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, - filter: ExtensionTarget, -) { - let lo_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0]; - let lo_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1]; - let hi_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0]; - let hi_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1]; - let lo_shifted_aux_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_0]; - let lo_shifted_aux_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_1]; - let hi_shifted_aux_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_0]; - let hi_shifted_aux_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_1]; - - let one = builder.one_extension(); - let u32_max = builder.constant_extension(F::Extension::from_canonical_u32(u32::MAX)); - - let constr1 = { - let t0 = builder.sub_extension(u32_max, lo_shifted_1); - let t1 = builder.mul_sub_extension(lo_shifted_aux_0, t0, lo_shifted_aux_1); - builder.mul_extension(filter, t1) - }; - yield_constr.constraint(builder, constr1); - - let constr2 = { - let t0 = builder.sub_extension(u32_max, hi_shifted_1); - let t1 = builder.mul_sub_extension(hi_shifted_aux_0, t0, hi_shifted_aux_1); - builder.mul_extension(filter, t1) - }; - yield_constr.constraint(builder, constr2); - - let lo_shifted_is_valid = { - let t0 = builder.sub_extension(one, lo_shifted_aux_1); - let t1 = builder.mul_extension(t0, lo_shifted_0); - builder.mul_extension(filter, t1) - }; - let hi_shifted_is_valid = { - let t0 = builder.sub_extension(one, hi_shifted_aux_1); - let t1 = builder.mul_extension(t0, hi_shifted_0); - builder.mul_extension(filter, t1) - }; - yield_constr.constraint(builder, lo_shifted_is_valid); - yield_constr.constraint(builder, hi_shifted_is_valid); -} - -fn eval_rotate_shift_circuit, const D: usize>( - builder: &mut CircuitBuilder, - lv: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, - filter: ExtensionTarget, -) -> ( - ExtensionTarget, - ExtensionTarget, - ExtensionTarget, - ExtensionTarget, - ExtensionTarget, - ExtensionTarget, - ExtensionTarget, -) { - // Input - let input_lo = lv[COL_ROTATE_SHIFT_INPUT_LO]; - let input_hi = lv[COL_ROTATE_SHIFT_INPUT_HI]; - - let exp_ge32_bit = lv[COL_ROTATE_SHIFT_DELTA_DIV32]; - let pow_exp = lv[COL_ROTATE_SHIFT_POW_EXP]; - - let lo_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0]; - let lo_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1]; - let hi_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0]; - let hi_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1]; - - // Output - let output_lo = lv[COL_ROTATE_SHIFT_OUTPUT_0]; - let output_hi = lv[COL_ROTATE_SHIFT_OUTPUT_1]; - - constrain_pow_exp_circuit(builder, lv, yield_constr, filter); - constrain_shifted_are_valid_circuit(builder, lv, yield_constr, filter); - - let base = builder.constant_extension(F::Extension::from_canonical_u64(1u64 << 32)); - let lo_shifted = builder.mul_add_extension(lo_shifted_1, base, lo_shifted_0); - let hi_shifted = builder.mul_add_extension(hi_shifted_1, base, hi_shifted_0); - - let lo_shifted_expected = builder.mul_extension(input_lo, pow_exp); - let hi_shifted_expected = builder.mul_extension(input_hi, pow_exp); - - let lo_shifted_valid = { - let t0 = builder.sub_extension(lo_shifted_expected, lo_shifted); - builder.mul_extension(filter, t0) - }; - yield_constr.constraint(builder, lo_shifted_valid); - let hi_shifted_valid = { - let t0 = builder.sub_extension(hi_shifted_expected, hi_shifted); - builder.mul_extension(filter, t0) - }; - yield_constr.constraint(builder, hi_shifted_valid); - - ( - exp_ge32_bit, - lo_shifted_0, - lo_shifted_1, - hi_shifted_0, - hi_shifted_1, - output_lo, - output_hi, - ) -} - -pub(crate) fn eval_rotate_left_circuit, const D: usize>( - builder: &mut CircuitBuilder, - lv: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, -) { - let is_rol = lv[IS_ROTATE_LEFT]; - - let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) = - eval_rotate_shift_circuit(builder, lv, yield_constr, is_rol); - - let one = builder.one_extension(); - let s0 = builder.add_extension(hi_shifted_1, lo_shifted_0); - let s1 = builder.add_extension(lo_shifted_1, hi_shifted_0); - let c = builder.sub_extension(one, delta_ge32); - - let lo_constr = { - let t0 = builder.sub_extension(s0, output_lo); - let t1 = builder.mul_extension(c, t0); - let t2 = builder.sub_extension(s1, output_lo); - let t3 = builder.mul_extension(delta_ge32, t2); - let t4 = builder.add_extension(t1, t3); - builder.mul_extension(is_rol, t4) - }; - - let hi_constr = { - let t0 = builder.sub_extension(s1, output_hi); - let t1 = builder.mul_extension(c, t0); - let t2 = builder.sub_extension(s0, output_hi); - let t3 = builder.mul_extension(delta_ge32, t2); - let t4 = builder.add_extension(t1, t3); - builder.mul_extension(is_rol, t4) - }; - - yield_constr.constraint(builder, lo_constr); - yield_constr.constraint(builder, hi_constr); -} - -pub(crate) fn eval_rotate_right_circuit, const D: usize>( - builder: &mut CircuitBuilder, - lv: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, -) { - let is_ror = lv[IS_ROTATE_RIGHT]; - - let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) = - eval_rotate_shift_circuit(builder, lv, yield_constr, is_ror); - - let one = builder.one_extension(); - let s0 = builder.add_extension(hi_shifted_1, lo_shifted_0); - let s1 = builder.add_extension(lo_shifted_1, hi_shifted_0); - let c = builder.sub_extension(one, delta_ge32); - - let lo_constr = { - let t0 = builder.sub_extension(s1, output_lo); - let t1 = builder.mul_extension(c, t0); - let t2 = builder.sub_extension(s0, output_lo); - let t3 = builder.mul_extension(delta_ge32, t2); - let t4 = builder.add_extension(t1, t3); - builder.mul_extension(is_ror, t4) - }; - - let hi_constr = { - let t0 = builder.sub_extension(s0, output_hi); - let t1 = builder.mul_extension(c, t0); - let t2 = builder.sub_extension(s1, output_hi); - let t3 = builder.mul_extension(delta_ge32, t2); - let t4 = builder.add_extension(t1, t3); - builder.mul_extension(is_ror, t4) - }; - - yield_constr.constraint(builder, lo_constr); - yield_constr.constraint(builder, hi_constr); -} - -pub(crate) fn eval_shift_left_circuit, const D: usize>( - builder: &mut CircuitBuilder, - lv: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, -) { - let is_shl = lv[IS_SHIFT_LEFT]; - - let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, _hi_shifted_1, output_lo, output_hi) = - eval_rotate_shift_circuit(builder, lv, yield_constr, is_shl); - - let one = builder.one_extension(); - let c = builder.sub_extension(one, delta_ge32); - - let lo_constr = { - let t0 = builder.sub_extension(lo_shifted_0, output_lo); - let t1 = builder.mul_extension(c, t0); - let t2 = builder.mul_extension(delta_ge32, output_lo); - let t3 = builder.add_extension(t1, t2); - builder.mul_extension(is_shl, t3) - }; - - let hi_constr = { - let t0 = builder.add_extension(lo_shifted_1, hi_shifted_0); - let t1 = builder.sub_extension(t0, output_hi); - let t2 = builder.mul_extension(c, t1); - let t3 = builder.sub_extension(lo_shifted_0, output_hi); - let t4 = builder.mul_extension(delta_ge32, t3); - let t5 = builder.add_extension(t2, t4); - builder.mul_extension(is_shl, t5) - }; - - yield_constr.constraint(builder, lo_constr); - yield_constr.constraint(builder, hi_constr); -} - -pub(crate) fn eval_shift_right_circuit, const D: usize>( - builder: &mut CircuitBuilder, - lv: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, -) { - let is_shr = lv[IS_SHIFT_RIGHT]; - - let (delta_ge32, _lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) = - eval_rotate_shift_circuit(builder, lv, yield_constr, is_shr); - - let one = builder.one_extension(); - let c = builder.sub_extension(one, delta_ge32); - - let lo_constr = { - let t0 = builder.add_extension(lo_shifted_1, hi_shifted_0); - let t1 = builder.sub_extension(t0, output_lo); - let t2 = builder.mul_extension(c, t1); - let t3 = builder.sub_extension(hi_shifted_1, output_lo); - let t4 = builder.mul_extension(delta_ge32, t3); - let t5 = builder.add_extension(t2, t4); - builder.mul_extension(is_shr, t5) - }; - - let hi_constr = { - let t0 = builder.sub_extension(hi_shifted_1, output_hi); - let t1 = builder.mul_extension(c, t0); - let t2 = builder.mul_extension(delta_ge32, output_hi); - let t3 = builder.add_extension(t1, t2); - builder.mul_extension(is_shr, t3) - }; - - yield_constr.constraint(builder, lo_constr); - yield_constr.constraint(builder, hi_constr); -} diff --git a/system_zero/src/alu/subtraction.rs b/system_zero/src/alu/subtraction.rs deleted file mode 100644 index dd83cbda..00000000 --- a/system_zero/src/alu/subtraction.rs +++ /dev/null @@ -1,76 +0,0 @@ -use plonky2::field::extension::Extendable; -use plonky2::field::packed::PackedField; -use plonky2::field::types::{Field, PrimeField64}; -use plonky2::hash::hash_types::RichField; -use plonky2::iop::ext_target::ExtensionTarget; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; - -use crate::registers::alu::*; -use crate::registers::NUM_COLUMNS; - -pub(crate) fn generate_subtraction(values: &mut [F; NUM_COLUMNS]) { - let in_1 = values[COL_SUB_INPUT_0].to_canonical_u64() as u32; - let in_2 = values[COL_SUB_INPUT_1].to_canonical_u64() as u32; - - // in_1 - in_2 == diff - br*2^32 - let (diff, br) = in_1.overflowing_sub(in_2); - - values[COL_SUB_OUTPUT_0] = F::from_canonical_u16(diff as u16); - values[COL_SUB_OUTPUT_1] = F::from_canonical_u16((diff >> 16) as u16); - values[COL_SUB_OUTPUT_BORROW] = F::from_bool(br); -} - -pub(crate) fn eval_subtraction>( - local_values: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, -) { - let is_sub = local_values[IS_SUB]; - let in_1 = local_values[COL_SUB_INPUT_0]; - let in_2 = local_values[COL_SUB_INPUT_1]; - let out_1 = local_values[COL_SUB_OUTPUT_0]; - let out_2 = local_values[COL_SUB_OUTPUT_1]; - let out_br = local_values[COL_SUB_OUTPUT_BORROW]; - - let base = F::from_canonical_u64(1 << 16); - let base_sqr = F::from_canonical_u64(1 << 32); - - let out_br = out_br * base_sqr; - let lhs = (out_br + in_1) - in_2; - let rhs = out_1 + out_2 * base; - - yield_constr.constraint(is_sub * (lhs - rhs)); - - // We don't need to check that out_br is in {0, 1} because it's - // checked by boolean::col_bit(0) in the ALU. -} - -pub(crate) fn eval_subtraction_circuit, const D: usize>( - builder: &mut CircuitBuilder, - local_values: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, -) { - let is_sub = local_values[IS_SUB]; - let in_1 = local_values[COL_SUB_INPUT_0]; - let in_2 = local_values[COL_SUB_INPUT_1]; - let out_1 = local_values[COL_SUB_OUTPUT_0]; - let out_2 = local_values[COL_SUB_OUTPUT_1]; - let out_br = local_values[COL_SUB_OUTPUT_BORROW]; - - let base = builder.constant_extension(F::Extension::from_canonical_u64(1 << 16)); - #[allow(unused)] // TODO - let base_sqr = builder.constant_extension(F::Extension::from_canonical_u64(1 << 32)); - - // lhs = (out_br + in_1) - in_2 - let lhs = builder.add_extension(out_br, in_1); - let lhs = builder.sub_extension(lhs, in_2); - - // rhs = out_1 + base * out_2 - let rhs = builder.mul_add_extension(out_2, base, out_1); - - // filtered_diff = is_sub * (lhs - rhs) - let diff = builder.sub_extension(lhs, rhs); - let filtered_diff = builder.mul_extension(is_sub, diff); - - yield_constr.constraint(builder, filtered_diff); -} diff --git a/system_zero/src/core_registers.rs b/system_zero/src/core_registers.rs deleted file mode 100644 index 210a9971..00000000 --- a/system_zero/src/core_registers.rs +++ /dev/null @@ -1,92 +0,0 @@ -use plonky2::field::extension::Extendable; -use plonky2::field::packed::PackedField; -use plonky2::field::types::{Field, PrimeField64}; -use plonky2::hash::hash_types::RichField; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use starky::vars::{StarkEvaluationTargets, StarkEvaluationVars}; - -use crate::public_input_layout::NUM_PUBLIC_INPUTS; -use crate::registers::core::*; -use crate::registers::NUM_COLUMNS; - -pub(crate) fn generate_first_row_core_registers(first_values: &mut [F; NUM_COLUMNS]) { - first_values[COL_CLOCK] = F::ZERO; - first_values[COL_RANGE_16] = F::ZERO; - first_values[COL_INSTRUCTION_PTR] = F::ZERO; - first_values[COL_FRAME_PTR] = F::ZERO; - first_values[COL_STACK_PTR] = F::ZERO; -} - -pub(crate) fn generate_next_row_core_registers( - local_values: &[F; NUM_COLUMNS], - next_values: &mut [F; NUM_COLUMNS], -) { - // We increment the clock by 1. - next_values[COL_CLOCK] = local_values[COL_CLOCK] + F::ONE; - - // We increment the 16-bit table by 1, unless we've reached the max value of 2^16 - 1, in - // which case we repeat that value. - let prev_range_16 = local_values[COL_RANGE_16].to_canonical_u64(); - let next_range_16 = (prev_range_16 + 1).min((1 << 16) - 1); - next_values[COL_RANGE_16] = F::from_canonical_u64(next_range_16); - - // next_values[COL_INSTRUCTION_PTR] = todo!(); - - // next_values[COL_FRAME_PTR] = todo!(); - - // next_values[COL_STACK_PTR] = todo!(); -} - -#[inline] -pub(crate) fn eval_core_registers>( - vars: StarkEvaluationVars, - yield_constr: &mut ConstraintConsumer

, -) { - // The clock must start with 0, and increment by 1. - let local_clock = vars.local_values[COL_CLOCK]; - let next_clock = vars.next_values[COL_CLOCK]; - let delta_clock = next_clock - local_clock; - yield_constr.constraint_first_row(local_clock); - yield_constr.constraint_transition(delta_clock - F::ONE); - - // The 16-bit table must start with 0, end with 2^16 - 1, and increment by 0 or 1. - let local_range_16 = vars.local_values[COL_RANGE_16]; - let next_range_16 = vars.next_values[COL_RANGE_16]; - let delta_range_16 = next_range_16 - local_range_16; - yield_constr.constraint_first_row(local_range_16); - yield_constr.constraint_last_row(local_range_16 - F::from_canonical_u64((1 << 16) - 1)); - yield_constr.constraint_transition(delta_range_16 * delta_range_16 - delta_range_16); - - // TODO constraints for stack etc. -} - -pub(crate) fn eval_core_registers_circuit, const D: usize>( - builder: &mut CircuitBuilder, - vars: StarkEvaluationTargets, - yield_constr: &mut RecursiveConstraintConsumer, -) { - let one_ext = builder.one_extension(); - let max_u16 = builder.constant(F::from_canonical_u64((1 << 16) - 1)); - let max_u16_ext = builder.convert_to_ext(max_u16); - - // The clock must start with 0, and increment by 1. - let local_clock = vars.local_values[COL_CLOCK]; - let next_clock = vars.next_values[COL_CLOCK]; - let delta_clock = builder.sub_extension(next_clock, local_clock); - yield_constr.constraint_first_row(builder, local_clock); - let constraint = builder.sub_extension(delta_clock, one_ext); - yield_constr.constraint_transition(builder, constraint); - - // The 16-bit table must start with 0, end with 2^16 - 1, and increment by 0 or 1. - let local_range_16 = vars.local_values[COL_RANGE_16]; - let next_range_16 = vars.next_values[COL_RANGE_16]; - let delta_range_16 = builder.sub_extension(next_range_16, local_range_16); - yield_constr.constraint_first_row(builder, local_range_16); - let constraint = builder.sub_extension(local_range_16, max_u16_ext); - yield_constr.constraint_last_row(builder, constraint); - let constraint = builder.mul_add_extension(delta_range_16, delta_range_16, delta_range_16); - yield_constr.constraint_transition(builder, constraint); - - // TODO constraints for stack etc. -} diff --git a/system_zero/src/lib.rs b/system_zero/src/lib.rs deleted file mode 100644 index 8681a97c..00000000 --- a/system_zero/src/lib.rs +++ /dev/null @@ -1,10 +0,0 @@ -#![feature(array_zip)] - -mod alu; -mod core_registers; -pub mod lookup; -mod memory; -mod permutation_unit; -mod public_input_layout; -mod registers; -pub mod system_zero; diff --git a/system_zero/src/lookup.rs b/system_zero/src/lookup.rs deleted file mode 100644 index d1d16223..00000000 --- a/system_zero/src/lookup.rs +++ /dev/null @@ -1,146 +0,0 @@ -//! Implementation of the Halo2 lookup argument. -//! -//! References: -//! - https://zcash.github.io/halo2/design/proving-system/lookup.html -//! - https://www.youtube.com/watch?v=YlTt12s7vGE&t=5237s - -use std::cmp::Ordering; - -use itertools::Itertools; -use plonky2::field::extension::Extendable; -use plonky2::field::packed::PackedField; -use plonky2::field::types::{Field, PrimeField64}; -use plonky2::hash::hash_types::RichField; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use starky::vars::{StarkEvaluationTargets, StarkEvaluationVars}; - -use crate::public_input_layout::NUM_PUBLIC_INPUTS; -use crate::registers::lookup::*; -use crate::registers::NUM_COLUMNS; - -pub(crate) fn generate_lookups(trace_cols: &mut [Vec]) { - for i in 0..NUM_LOOKUPS { - let inputs = &trace_cols[col_input(i)]; - let table = &trace_cols[col_table(i)]; - let (permuted_inputs, permuted_table) = permuted_cols(inputs, table); - trace_cols[col_permuted_input(i)] = permuted_inputs; - trace_cols[col_permuted_table(i)] = permuted_table; - } -} - -/// Given an input column and a table column, generate the permuted input and permuted table columns -/// used in the Halo2 permutation argument. -pub fn permuted_cols(inputs: &[F], table: &[F]) -> (Vec, Vec) { - let n = inputs.len(); - - // The permuted inputs do not have to be ordered, but we found that sorting was faster than - // hash-based grouping. We also sort the table, as this helps us identify "unused" table - // elements efficiently. - - // To compare elements, e.g. for sorting, we first need them in canonical form. It would be - // wasteful to canonicalize in each comparison, as a single element may be involved in many - // comparisons. So we will canonicalize once upfront, then use `to_noncanonical_u64` when - // comparing elements. - - let sorted_inputs = inputs - .iter() - .map(|x| x.to_canonical()) - .sorted_unstable_by_key(|x| x.to_noncanonical_u64()) - .collect_vec(); - let sorted_table = table - .iter() - .map(|x| x.to_canonical()) - .sorted_unstable_by_key(|x| x.to_noncanonical_u64()) - .collect_vec(); - - let mut unused_table_inds = Vec::with_capacity(n); - let mut unused_table_vals = Vec::with_capacity(n); - let mut permuted_table = vec![F::ZERO; n]; - let mut i = 0; - let mut j = 0; - while (j < n) && (i < n) { - let input_val = sorted_inputs[i].to_noncanonical_u64(); - let table_val = sorted_table[j].to_noncanonical_u64(); - match input_val.cmp(&table_val) { - Ordering::Greater => { - unused_table_vals.push(sorted_table[j]); - j += 1; - } - Ordering::Less => { - if let Some(x) = unused_table_vals.pop() { - permuted_table[i] = x; - } else { - unused_table_inds.push(i); - } - i += 1; - } - Ordering::Equal => { - permuted_table[i] = sorted_table[j]; - i += 1; - j += 1; - } - } - } - - #[allow(clippy::needless_range_loop)] // indexing is just more natural here - for jj in j..n { - unused_table_vals.push(sorted_table[jj]); - } - for ii in i..n { - unused_table_inds.push(ii); - } - for (ind, val) in unused_table_inds.into_iter().zip_eq(unused_table_vals) { - permuted_table[ind] = val; - } - - (sorted_inputs, permuted_table) -} - -pub(crate) fn eval_lookups>( - vars: StarkEvaluationVars, - yield_constr: &mut ConstraintConsumer

, -) { - for i in 0..NUM_LOOKUPS { - let local_perm_input = vars.local_values[col_permuted_input(i)]; - let next_perm_table = vars.next_values[col_permuted_table(i)]; - let next_perm_input = vars.next_values[col_permuted_input(i)]; - - // A "vertical" diff between the local and next permuted inputs. - let diff_input_prev = next_perm_input - local_perm_input; - // A "horizontal" diff between the next permuted input and permuted table value. - let diff_input_table = next_perm_input - next_perm_table; - - yield_constr.constraint(diff_input_prev * diff_input_table); - - // This is actually constraining the first row, as per the spec, since `diff_input_table` - // is a diff of the next row's values. In the context of `constraint_last_row`, the next - // row is the first row. - yield_constr.constraint_last_row(diff_input_table); - } -} - -pub(crate) fn eval_lookups_circuit, const D: usize>( - builder: &mut CircuitBuilder, - vars: StarkEvaluationTargets, - yield_constr: &mut RecursiveConstraintConsumer, -) { - for i in 0..NUM_LOOKUPS { - let local_perm_input = vars.local_values[col_permuted_input(i)]; - let next_perm_table = vars.next_values[col_permuted_table(i)]; - let next_perm_input = vars.next_values[col_permuted_input(i)]; - - // A "vertical" diff between the local and next permuted inputs. - let diff_input_prev = builder.sub_extension(next_perm_input, local_perm_input); - // A "horizontal" diff between the next permuted input and permuted table value. - let diff_input_table = builder.sub_extension(next_perm_input, next_perm_table); - - let diff_product = builder.mul_extension(diff_input_prev, diff_input_table); - yield_constr.constraint(builder, diff_product); - - // This is actually constraining the first row, as per the spec, since `diff_input_table` - // is a diff of the next row's values. In the context of `constraint_last_row`, the next - // row is the first row. - yield_constr.constraint_last_row(builder, diff_input_table); - } -} diff --git a/system_zero/src/memory.rs b/system_zero/src/memory.rs deleted file mode 100644 index 0cc42d30..00000000 --- a/system_zero/src/memory.rs +++ /dev/null @@ -1,16 +0,0 @@ -#[derive(Default)] -pub struct TransactionMemory { - pub calls: Vec, -} - -/// A virtual memory space specific to the current contract call. -pub struct ContractMemory { - pub code: MemorySegment, - pub main: MemorySegment, - pub calldata: MemorySegment, - pub returndata: MemorySegment, -} - -pub struct MemorySegment { - pub content: Vec, -} diff --git a/system_zero/src/permutation_unit.rs b/system_zero/src/permutation_unit.rs deleted file mode 100644 index 4ba469b4..00000000 --- a/system_zero/src/permutation_unit.rs +++ /dev/null @@ -1,321 +0,0 @@ -use plonky2::field::extension::{Extendable, FieldExtension}; -use plonky2::field::packed::PackedField; -use plonky2::hash::hash_types::RichField; -use plonky2::hash::hashing::SPONGE_WIDTH; -use plonky2::hash::poseidon::{Poseidon, HALF_N_FULL_ROUNDS, N_PARTIAL_ROUNDS}; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use starky::vars::{StarkEvaluationTargets, StarkEvaluationVars}; - -use crate::public_input_layout::NUM_PUBLIC_INPUTS; -use crate::registers::permutation::*; -use crate::registers::NUM_COLUMNS; - -fn constant_layer( - mut state: [P; SPONGE_WIDTH], - round: usize, -) -> [P; SPONGE_WIDTH] -where - F: Poseidon, - FE: FieldExtension, - P: PackedField, -{ - // One day I might actually vectorize this, but today is not that day. - for i in 0..P::WIDTH { - let mut unpacked_state = [P::Scalar::default(); SPONGE_WIDTH]; - for j in 0..SPONGE_WIDTH { - unpacked_state[j] = state[j].as_slice()[i]; - } - F::constant_layer_field(&mut unpacked_state, round); - for j in 0..SPONGE_WIDTH { - state[j].as_slice_mut()[i] = unpacked_state[j]; - } - } - state -} - -fn mds_layer(mut state: [P; SPONGE_WIDTH]) -> [P; SPONGE_WIDTH] -where - F: Poseidon, - FE: FieldExtension, - P: PackedField, -{ - for i in 0..P::WIDTH { - let mut unpacked_state = [P::Scalar::default(); SPONGE_WIDTH]; - for j in 0..SPONGE_WIDTH { - unpacked_state[j] = state[j].as_slice()[i]; - } - unpacked_state = F::mds_layer_field(&unpacked_state); - for j in 0..SPONGE_WIDTH { - state[j].as_slice_mut()[i] = unpacked_state[j]; - } - } - state -} - -pub(crate) fn generate_permutation_unit(values: &mut [F; NUM_COLUMNS]) { - // Load inputs. - let mut state = [F::ZERO; SPONGE_WIDTH]; - for i in 0..SPONGE_WIDTH { - state[i] = values[col_input(i)]; - } - - for r in 0..HALF_N_FULL_ROUNDS { - F::constant_layer(&mut state, r); - - for i in 0..SPONGE_WIDTH { - let state_cubed = state[i].cube(); - values[col_full_first_mid_sbox(r, i)] = state_cubed; - state[i] *= state_cubed.square(); // Form state ** 7. - } - - state = F::mds_layer(&state); - - for i in 0..SPONGE_WIDTH { - values[col_full_first_after_mds(r, i)] = state[i]; - } - } - - for r in 0..N_PARTIAL_ROUNDS { - F::constant_layer(&mut state, HALF_N_FULL_ROUNDS + r); - - let state0_cubed = state[0].cube(); - values[col_partial_mid_sbox(r)] = state0_cubed; - state[0] *= state0_cubed.square(); // Form state ** 7. - values[col_partial_after_sbox(r)] = state[0]; - - state = F::mds_layer(&state); - } - - for r in 0..HALF_N_FULL_ROUNDS { - F::constant_layer(&mut state, HALF_N_FULL_ROUNDS + N_PARTIAL_ROUNDS + r); - - for i in 0..SPONGE_WIDTH { - let state_cubed = state[i].cube(); - values[col_full_second_mid_sbox(r, i)] = state_cubed; - state[i] *= state_cubed.square(); // Form state ** 7. - } - - state = F::mds_layer(&state); - - for i in 0..SPONGE_WIDTH { - values[col_full_second_after_mds(r, i)] = state[i]; - } - } -} - -#[inline] -pub(crate) fn eval_permutation_unit( - vars: StarkEvaluationVars, - yield_constr: &mut ConstraintConsumer

, -) where - F: Poseidon, - FE: FieldExtension, - P: PackedField, -{ - let local_values = &vars.local_values; - - // Load inputs. - let mut state = [P::ZEROS; SPONGE_WIDTH]; - for i in 0..SPONGE_WIDTH { - state[i] = local_values[col_input(i)]; - } - - for r in 0..HALF_N_FULL_ROUNDS { - state = constant_layer(state, r); - - for i in 0..SPONGE_WIDTH { - let state_cubed = state[i] * state[i].square(); - yield_constr.constraint(state_cubed - local_values[col_full_first_mid_sbox(r, i)]); - let state_cubed = local_values[col_full_first_mid_sbox(r, i)]; - state[i] *= state_cubed.square(); // Form state ** 7. - } - - state = mds_layer(state); - - for i in 0..SPONGE_WIDTH { - yield_constr.constraint(state[i] - local_values[col_full_first_after_mds(r, i)]); - state[i] = local_values[col_full_first_after_mds(r, i)]; - } - } - - for r in 0..N_PARTIAL_ROUNDS { - state = constant_layer(state, HALF_N_FULL_ROUNDS + r); - - let state0_cubed = state[0] * state[0].square(); - yield_constr.constraint(state0_cubed - local_values[col_partial_mid_sbox(r)]); - let state0_cubed = local_values[col_partial_mid_sbox(r)]; - state[0] *= state0_cubed.square(); // Form state ** 7. - yield_constr.constraint(state[0] - local_values[col_partial_after_sbox(r)]); - state[0] = local_values[col_partial_after_sbox(r)]; - - state = mds_layer(state); - } - - for r in 0..HALF_N_FULL_ROUNDS { - state = constant_layer(state, HALF_N_FULL_ROUNDS + N_PARTIAL_ROUNDS + r); - - for i in 0..SPONGE_WIDTH { - let state_cubed = state[i] * state[i].square(); - yield_constr.constraint(state_cubed - local_values[col_full_second_mid_sbox(r, i)]); - let state_cubed = local_values[col_full_second_mid_sbox(r, i)]; - state[i] *= state_cubed.square(); // Form state ** 7. - } - - state = mds_layer(state); - - for i in 0..SPONGE_WIDTH { - yield_constr.constraint(state[i] - local_values[col_full_second_after_mds(r, i)]); - state[i] = local_values[col_full_second_after_mds(r, i)]; - } - } -} - -pub(crate) fn eval_permutation_unit_circuit, const D: usize>( - builder: &mut CircuitBuilder, - vars: StarkEvaluationTargets, - yield_constr: &mut RecursiveConstraintConsumer, -) { - let zero = builder.zero_extension(); - let local_values = &vars.local_values; - - // Load inputs. - let mut state = [zero; SPONGE_WIDTH]; - for i in 0..SPONGE_WIDTH { - state[i] = local_values[col_input(i)]; - } - - for r in 0..HALF_N_FULL_ROUNDS { - F::constant_layer_circuit(builder, &mut state, r); - - for i in 0..SPONGE_WIDTH { - let state_cubed = builder.cube_extension(state[i]); - let diff = - builder.sub_extension(state_cubed, local_values[col_full_first_mid_sbox(r, i)]); - yield_constr.constraint(builder, diff); - let state_cubed = local_values[col_full_first_mid_sbox(r, i)]; - state[i] = builder.mul_many_extension([state[i], state_cubed, state_cubed]); - // Form state ** 7. - } - - state = F::mds_layer_circuit(builder, &state); - - for i in 0..SPONGE_WIDTH { - let diff = - builder.sub_extension(state[i], local_values[col_full_first_after_mds(r, i)]); - yield_constr.constraint(builder, diff); - state[i] = local_values[col_full_first_after_mds(r, i)]; - } - } - - for r in 0..N_PARTIAL_ROUNDS { - F::constant_layer_circuit(builder, &mut state, HALF_N_FULL_ROUNDS + r); - - let state0_cubed = builder.cube_extension(state[0]); - let diff = builder.sub_extension(state0_cubed, local_values[col_partial_mid_sbox(r)]); - yield_constr.constraint(builder, diff); - let state0_cubed = local_values[col_partial_mid_sbox(r)]; - state[0] = builder.mul_many_extension([state[0], state0_cubed, state0_cubed]); // Form state ** 7. - let diff = builder.sub_extension(state[0], local_values[col_partial_after_sbox(r)]); - yield_constr.constraint(builder, diff); - state[0] = local_values[col_partial_after_sbox(r)]; - - state = F::mds_layer_circuit(builder, &state); - } - - for r in 0..HALF_N_FULL_ROUNDS { - F::constant_layer_circuit( - builder, - &mut state, - HALF_N_FULL_ROUNDS + N_PARTIAL_ROUNDS + r, - ); - - for i in 0..SPONGE_WIDTH { - let state_cubed = builder.cube_extension(state[i]); - let diff = - builder.sub_extension(state_cubed, local_values[col_full_second_mid_sbox(r, i)]); - yield_constr.constraint(builder, diff); - let state_cubed = local_values[col_full_second_mid_sbox(r, i)]; - state[i] = builder.mul_many_extension([state[i], state_cubed, state_cubed]); - // Form state ** 7. - } - - state = F::mds_layer_circuit(builder, &state); - - for i in 0..SPONGE_WIDTH { - let diff = - builder.sub_extension(state[i], local_values[col_full_second_after_mds(r, i)]); - yield_constr.constraint(builder, diff); - state[i] = local_values[col_full_second_after_mds(r, i)]; - } - } -} - -#[cfg(test)] -mod tests { - use plonky2::field::goldilocks_field::GoldilocksField; - use plonky2::field::types::{Field, Sample}; - use plonky2::hash::poseidon::Poseidon; - use rand::SeedableRng; - use rand_chacha::ChaCha8Rng; - use starky::constraint_consumer::ConstraintConsumer; - use starky::vars::StarkEvaluationVars; - - use crate::permutation_unit::{eval_permutation_unit, generate_permutation_unit, SPONGE_WIDTH}; - use crate::public_input_layout::NUM_PUBLIC_INPUTS; - use crate::registers::permutation::{col_input, col_output}; - use crate::registers::NUM_COLUMNS; - - #[test] - fn generate_eval_consistency() { - type F = GoldilocksField; - - let mut values = [F::default(); NUM_COLUMNS]; - generate_permutation_unit(&mut values); - - let vars = StarkEvaluationVars { - local_values: &values, - next_values: &[F::default(); NUM_COLUMNS], - public_inputs: &[F::default(); NUM_PUBLIC_INPUTS], - }; - - let mut constrant_consumer = ConstraintConsumer::new( - vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)], - GoldilocksField::ONE, - GoldilocksField::ONE, - GoldilocksField::ONE, - ); - eval_permutation_unit(vars, &mut constrant_consumer); - for &acc in &constrant_consumer.constraint_accs { - assert_eq!(acc, GoldilocksField::ZERO); - } - } - - #[test] - fn poseidon_result() { - type F = GoldilocksField; - - let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25); - let state = [F::default(); SPONGE_WIDTH].map(|_| F::sample(&mut rng)); - - // Get true Poseidon hash - let target = GoldilocksField::poseidon(state); - - // Get result from `generate_permutation_unit` - // Initialize `values` with randomness to test that the code doesn't rely on zero-filling. - let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng)); - for i in 0..SPONGE_WIDTH { - values[col_input(i)] = state[i]; - } - generate_permutation_unit(&mut values); - let mut result = [F::default(); SPONGE_WIDTH]; - for i in 0..SPONGE_WIDTH { - result[i] = values[col_output(i)]; - } - - assert_eq!(target, result); - } - - // TODO(JN): test degree - // TODO(JN): test `eval_permutation_unit_recursively` -} diff --git a/system_zero/src/public_input_layout.rs b/system_zero/src/public_input_layout.rs deleted file mode 100644 index 225b3814..00000000 --- a/system_zero/src/public_input_layout.rs +++ /dev/null @@ -1,7 +0,0 @@ -/// The previous state root, before these transactions were executed. -const PI_OLD_STATE_ROOT: usize = 0; - -/// The updated state root, after these transactions were executed. -const PI_NEW_STATE_ROOT: usize = PI_OLD_STATE_ROOT + 1; - -pub(crate) const NUM_PUBLIC_INPUTS: usize = PI_NEW_STATE_ROOT + 1; diff --git a/system_zero/src/registers/alu.rs b/system_zero/src/registers/alu.rs deleted file mode 100644 index a61df051..00000000 --- a/system_zero/src/registers/alu.rs +++ /dev/null @@ -1,185 +0,0 @@ -//! Arithmetic and logic unit. - -pub(crate) const IS_ADD: usize = super::START_ALU; -pub(crate) const IS_SUB: usize = IS_ADD + 1; -pub(crate) const IS_MUL_ADD: usize = IS_SUB + 1; -pub(crate) const IS_DIV: usize = IS_MUL_ADD + 1; -pub(crate) const IS_AND: usize = IS_DIV + 1; -pub(crate) const IS_IOR: usize = IS_AND + 1; -pub(crate) const IS_XOR: usize = IS_IOR + 1; -pub(crate) const IS_ANDNOT: usize = IS_XOR + 1; -pub(crate) const IS_NOT: usize = IS_ANDNOT + 1; -pub(crate) const IS_ROTATE_LEFT: usize = IS_NOT + 1; -pub(crate) const IS_ROTATE_RIGHT: usize = IS_ROTATE_LEFT + 1; -pub(crate) const IS_SHIFT_LEFT: usize = IS_ROTATE_RIGHT + 1; -pub(crate) const IS_SHIFT_RIGHT: usize = IS_SHIFT_LEFT + 1; -pub(crate) const IS_ARITH_SHIFT_RIGHT: usize = IS_SHIFT_RIGHT + 1; - -pub(crate) const ALL_OPERATIONS: [usize; 14] = [ - IS_ADD, - IS_SUB, - IS_MUL_ADD, - IS_DIV, - IS_AND, - IS_IOR, - IS_XOR, - IS_ANDNOT, - IS_NOT, - IS_ROTATE_LEFT, - IS_ROTATE_RIGHT, - IS_SHIFT_LEFT, - IS_SHIFT_RIGHT, - IS_ARITH_SHIFT_RIGHT, -]; - -const START_SHARED_COLS: usize = IS_ARITH_SHIFT_RIGHT + 1; - -/// Within the ALU, there are shared columns which can be used by any arithmetic/logic -/// circuit, depending on which one is active this cycle. -// Can be increased as needed as other operations are implemented. -const NUM_SHARED_COLS: usize = 130; - -const fn shared_col(i: usize) -> usize { - debug_assert!(i < NUM_SHARED_COLS); - START_SHARED_COLS + i -} - -/// The first value to be added; treated as an unsigned u32. -pub(crate) const COL_ADD_INPUT_0: usize = shared_col(0); -/// The second value to be added; treated as an unsigned u32. -pub(crate) const COL_ADD_INPUT_1: usize = shared_col(1); -/// The third value to be added; treated as an unsigned u32. -pub(crate) const COL_ADD_INPUT_2: usize = shared_col(2); - -// Note: Addition outputs three 16-bit chunks, and since these values need to be range-checked -// anyway, we might as well use the range check unit's columns as our addition outputs. So the -// three proceeding columns are basically aliases, not columns owned by the ALU. -/// The first 16-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_ADD_OUTPUT_0: usize = super::range_check_16::col_rc_16_input(0); -/// The second 16-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_ADD_OUTPUT_1: usize = super::range_check_16::col_rc_16_input(1); -/// The third 16-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_ADD_OUTPUT_2: usize = super::range_check_16::col_rc_16_input(2); - -/// Inputs for subtraction; the second value is subtracted from the -/// first; inputs treated as an unsigned u32. -pub(crate) const COL_SUB_INPUT_0: usize = shared_col(0); -pub(crate) const COL_SUB_INPUT_1: usize = shared_col(1); - -/// The first 16-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_SUB_OUTPUT_0: usize = super::range_check_16::col_rc_16_input(0); -/// The second 16-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_SUB_OUTPUT_1: usize = super::range_check_16::col_rc_16_input(1); -/// The borrow output -pub(crate) const COL_SUB_OUTPUT_BORROW: usize = super::boolean::col_bit(0); - -/// The first value to be multiplied; treated as an unsigned u32. -pub(crate) const COL_MUL_ADD_FACTOR_0: usize = shared_col(0); -/// The second value to be multiplied; treated as an unsigned u32. -pub(crate) const COL_MUL_ADD_FACTOR_1: usize = shared_col(1); -/// The value to be added to the product; treated as an unsigned u32. -pub(crate) const COL_MUL_ADD_ADDEND: usize = shared_col(2); - -/// The inverse of `u32::MAX - result_hi`, where `output_hi` is the high 32-bits of the result. -/// See https://hackmd.io/NC-yRmmtRQSvToTHb96e8Q#Checking-element-validity -pub(crate) const COL_MUL_ADD_RESULT_CANONICAL_INV: usize = shared_col(3); - -/// The first 16-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_MUL_ADD_OUTPUT_0: usize = super::range_check_16::col_rc_16_input(0); -/// The second 16-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_MUL_ADD_OUTPUT_1: usize = super::range_check_16::col_rc_16_input(1); -/// The third 16-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_MUL_ADD_OUTPUT_2: usize = super::range_check_16::col_rc_16_input(2); -/// The fourth 16-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_MUL_ADD_OUTPUT_3: usize = super::range_check_16::col_rc_16_input(3); - -/// Dividend for division, as an unsigned u32 -pub(crate) const COL_DIV_INPUT_DIVIDEND: usize = shared_col(0); -/// Divisor for division, as an unsigned u32 -pub(crate) const COL_DIV_INPUT_DIVISOR: usize = shared_col(1); -/// Inverse of divisor, if one exists, and 0 otherwise -pub(crate) const COL_DIV_INVDIVISOR: usize = shared_col(2); -/// 1 if divisor is nonzero and 0 otherwise -pub(crate) const COL_DIV_NONZERO_DIVISOR: usize = shared_col(3); - -/// The first 16-bit chunk of the quotient, based on little-endian ordering. -pub(crate) const COL_DIV_OUTPUT_QUOT_0: usize = super::range_check_16::col_rc_16_input(0); -/// The second 16-bit chunk of the quotient, based on little-endian ordering. -pub(crate) const COL_DIV_OUTPUT_QUOT_1: usize = super::range_check_16::col_rc_16_input(1); -/// The first 16-bit chunk of the remainder, based on little-endian ordering. -pub(crate) const COL_DIV_OUTPUT_REM_0: usize = super::range_check_16::col_rc_16_input(2); -/// The second 16-bit chunk of the remainder, based on little-endian ordering. -pub(crate) const COL_DIV_OUTPUT_REM_1: usize = super::range_check_16::col_rc_16_input(3); - -/// The first 16-bit chunk of a temporary value (divisor - remainder - 1). -pub(crate) const COL_DIV_RANGE_CHECKED_TMP_0: usize = super::range_check_16::col_rc_16_input(4); -/// The second 16-bit chunk of a temporary value (divisor - remainder - 1). -pub(crate) const COL_DIV_RANGE_CHECKED_TMP_1: usize = super::range_check_16::col_rc_16_input(5); - -/// -/// Bitwise logic operations -/// - -/// Bit decomposition of 64-bit values, as 32-bit low and high halves. - -const fn gen_bitop_nbit_input_regs(start: usize) -> [usize; N] { - let mut regs = [0usize; N]; - let mut i = 0; - while i < N { - regs[i] = shared_col(start + i); - i += 1; - } - regs -} - -pub(crate) const COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS: [usize; 32] = - gen_bitop_nbit_input_regs::<32>(0); -pub(crate) const COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS: [usize; 32] = - gen_bitop_nbit_input_regs::<32>(32); -pub(crate) const COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS: [usize; 32] = - gen_bitop_nbit_input_regs::<32>(64); -pub(crate) const COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS: [usize; 32] = - gen_bitop_nbit_input_regs::<32>(96); - -/// The first 32-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_BITOP_OUTPUT_0: usize = shared_col(128); -/// The second 32-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_BITOP_OUTPUT_1: usize = shared_col(129); - -/// Input value to be rotated or shifted, low 32 bits -pub(crate) const COL_ROTATE_SHIFT_INPUT_LO: usize = shared_col(0); -/// Input value to be rotated or shifted, high 32 bits -pub(crate) const COL_ROTATE_SHIFT_INPUT_HI: usize = shared_col(1); -/// Bit decomposition of EXP, which is DELTA mod 32 for left -/// rotate/shift; bit decomposition of (32 - DELTA mod 32) mod 32 for -/// right rotate/shift. -pub(crate) const COL_ROTATE_SHIFT_EXP_BITS: [usize; 5] = gen_bitop_nbit_input_regs::<5>(2); -/// Top bit of the 6-bit value DELTA; also interpreted as DELTA >= 32. -pub(crate) const COL_ROTATE_SHIFT_DELTA_DIV32: usize = shared_col(7); - -/// POW_EXP = 2^EXP, the AUX_i vars are helpers. -pub(crate) const COL_ROTATE_SHIFT_POW_EXP_AUX_0: usize = shared_col(8); -pub(crate) const COL_ROTATE_SHIFT_POW_EXP_AUX_1: usize = shared_col(9); -pub(crate) const COL_ROTATE_SHIFT_POW_EXP_AUX_2: usize = shared_col(10); -pub(crate) const COL_ROTATE_SHIFT_POW_EXP: usize = shared_col(11); - -/// low 32 bits of INPUT_LO * 2^EXP -pub(crate) const COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0: usize = shared_col(12); -/// high 32 bits of INPUT_LO * 2^EXP -pub(crate) const COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1: usize = shared_col(13); -/// low 32 bits of INPUT_HI * 2^EXP -pub(crate) const COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0: usize = shared_col(14); -/// high 32 bits of INPUT_HI * 2^EXP -pub(crate) const COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1: usize = shared_col(15); - -pub(crate) const COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_0: usize = shared_col(16); -pub(crate) const COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_1: usize = shared_col(17); -pub(crate) const COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_0: usize = shared_col(18); -pub(crate) const COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_1: usize = shared_col(19); - -/// The first 32-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_ROTATE_SHIFT_OUTPUT_0: usize = shared_col(20); -/// The second 32-bit chunk of the output, based on little-endian ordering. -pub(crate) const COL_ROTATE_SHIFT_OUTPUT_1: usize = shared_col(21); - -pub(super) const END: usize = START_SHARED_COLS + NUM_SHARED_COLS; diff --git a/system_zero/src/registers/boolean.rs b/system_zero/src/registers/boolean.rs deleted file mode 100644 index c59af8d4..00000000 --- a/system_zero/src/registers/boolean.rs +++ /dev/null @@ -1,10 +0,0 @@ -//! Boolean unit. Contains columns whose values must be 0 or 1. - -const NUM_BITS: usize = 128; - -pub const fn col_bit(index: usize) -> usize { - debug_assert!(index < NUM_BITS); - super::START_BOOLEAN + index -} - -pub(super) const END: usize = super::START_BOOLEAN + NUM_BITS; diff --git a/system_zero/src/registers/core.rs b/system_zero/src/registers/core.rs deleted file mode 100644 index 3fafab55..00000000 --- a/system_zero/src/registers/core.rs +++ /dev/null @@ -1,20 +0,0 @@ -//! Core registers. - -/// A cycle counter. Starts at 0; increments by 1. -pub(crate) const COL_CLOCK: usize = super::START_CORE; - -/// A column which contains the values `[0, ... 2^16 - 1]`, potentially with duplicates. Used for -/// 16-bit range checks. -/// -/// For ease of verification, we enforce that it must begin with 0 and end with `2^16 - 1`, and each -/// delta must be either 0 or 1. -pub(crate) const COL_RANGE_16: usize = COL_CLOCK + 1; - -/// Pointer to the current instruction. -pub(crate) const COL_INSTRUCTION_PTR: usize = COL_RANGE_16 + 1; -/// Pointer to the base of the current call's stack frame. -pub(crate) const COL_FRAME_PTR: usize = COL_INSTRUCTION_PTR + 1; -/// Pointer to the tip of the current call's stack frame. -pub(crate) const COL_STACK_PTR: usize = COL_FRAME_PTR + 1; - -pub(super) const END: usize = COL_STACK_PTR + 1; diff --git a/system_zero/src/registers/logic.rs b/system_zero/src/registers/logic.rs deleted file mode 100644 index 07f3f0e0..00000000 --- a/system_zero/src/registers/logic.rs +++ /dev/null @@ -1,3 +0,0 @@ -//! Logic unit. - -pub(super) const END: usize = super::START_LOGIC; diff --git a/system_zero/src/registers/lookup.rs b/system_zero/src/registers/lookup.rs deleted file mode 100644 index fd0abd43..00000000 --- a/system_zero/src/registers/lookup.rs +++ /dev/null @@ -1,37 +0,0 @@ -//! Lookup unit. -//! See https://zcash.github.io/halo2/design/proving-system/lookup.html - -const START_UNIT: usize = super::START_LOOKUP; - -pub(crate) const NUM_LOOKUPS: usize = - super::range_check_16::NUM_RANGE_CHECKS + super::range_check_degree::NUM_RANGE_CHECKS; - -pub(crate) const fn col_input(i: usize) -> usize { - if i < super::range_check_16::NUM_RANGE_CHECKS { - super::range_check_16::col_rc_16_input(i) - } else { - super::range_check_degree::col_rc_degree_input(i - super::range_check_16::NUM_RANGE_CHECKS) - } -} - -/// This column contains a permutation of the input values. -pub(crate) const fn col_permuted_input(i: usize) -> usize { - debug_assert!(i < NUM_LOOKUPS); - START_UNIT + 2 * i -} - -pub(crate) const fn col_table(i: usize) -> usize { - if i < super::range_check_16::NUM_RANGE_CHECKS { - super::core::COL_RANGE_16 - } else { - super::core::COL_CLOCK - } -} - -/// This column contains a permutation of the table values. -pub(crate) const fn col_permuted_table(i: usize) -> usize { - debug_assert!(i < NUM_LOOKUPS); - START_UNIT + 2 * i + 1 -} - -pub(super) const END: usize = START_UNIT + NUM_LOOKUPS * 2; diff --git a/system_zero/src/registers/memory.rs b/system_zero/src/registers/memory.rs deleted file mode 100644 index 1373d0d8..00000000 --- a/system_zero/src/registers/memory.rs +++ /dev/null @@ -1,3 +0,0 @@ -//! Memory unit. - -pub(super) const END: usize = super::START_MEMORY; diff --git a/system_zero/src/registers/mod.rs b/system_zero/src/registers/mod.rs deleted file mode 100644 index 12688b1c..00000000 --- a/system_zero/src/registers/mod.rs +++ /dev/null @@ -1,20 +0,0 @@ -pub(crate) mod alu; -pub(crate) mod boolean; -pub(crate) mod core; -pub(crate) mod logic; -pub(crate) mod lookup; -pub(crate) mod memory; -pub(crate) mod permutation; -pub(crate) mod range_check_16; -pub(crate) mod range_check_degree; - -const START_ALU: usize = 0; -const START_BOOLEAN: usize = alu::END; -const START_CORE: usize = boolean::END; -const START_LOGIC: usize = core::END; -const START_LOOKUP: usize = logic::END; -const START_MEMORY: usize = lookup::END; -const START_PERMUTATION: usize = memory::END; -const START_RANGE_CHECK_16: usize = permutation::END; -const START_RANGE_CHECK_DEGREE: usize = range_check_16::END; -pub(crate) const NUM_COLUMNS: usize = range_check_degree::END; diff --git a/system_zero/src/registers/permutation.rs b/system_zero/src/registers/permutation.rs deleted file mode 100644 index cde76af2..00000000 --- a/system_zero/src/registers/permutation.rs +++ /dev/null @@ -1,57 +0,0 @@ -//! Permutation unit. - -use plonky2::hash::hashing::SPONGE_WIDTH; -use plonky2::hash::poseidon; - -const START_FULL_FIRST: usize = super::START_PERMUTATION + SPONGE_WIDTH; - -pub const fn col_full_first_mid_sbox(round: usize, i: usize) -> usize { - debug_assert!(round < poseidon::HALF_N_FULL_ROUNDS); - debug_assert!(i < SPONGE_WIDTH); - START_FULL_FIRST + 2 * round * SPONGE_WIDTH + i -} - -pub const fn col_full_first_after_mds(round: usize, i: usize) -> usize { - debug_assert!(round < poseidon::HALF_N_FULL_ROUNDS); - debug_assert!(i < SPONGE_WIDTH); - START_FULL_FIRST + (2 * round + 1) * SPONGE_WIDTH + i -} - -const START_PARTIAL: usize = - col_full_first_after_mds(poseidon::HALF_N_FULL_ROUNDS - 1, SPONGE_WIDTH - 1) + 1; - -pub const fn col_partial_mid_sbox(round: usize) -> usize { - debug_assert!(round < poseidon::N_PARTIAL_ROUNDS); - START_PARTIAL + 2 * round -} - -pub const fn col_partial_after_sbox(round: usize) -> usize { - debug_assert!(round < poseidon::N_PARTIAL_ROUNDS); - START_PARTIAL + 2 * round + 1 -} - -const START_FULL_SECOND: usize = col_partial_after_sbox(poseidon::N_PARTIAL_ROUNDS - 1) + 1; - -pub const fn col_full_second_mid_sbox(round: usize, i: usize) -> usize { - debug_assert!(round <= poseidon::HALF_N_FULL_ROUNDS); - debug_assert!(i < SPONGE_WIDTH); - START_FULL_SECOND + 2 * round * SPONGE_WIDTH + i -} - -pub const fn col_full_second_after_mds(round: usize, i: usize) -> usize { - debug_assert!(round <= poseidon::HALF_N_FULL_ROUNDS); - debug_assert!(i < SPONGE_WIDTH); - START_FULL_SECOND + (2 * round + 1) * SPONGE_WIDTH + i -} - -pub const fn col_input(i: usize) -> usize { - debug_assert!(i < SPONGE_WIDTH); - super::START_PERMUTATION + i -} - -pub const fn col_output(i: usize) -> usize { - debug_assert!(i < SPONGE_WIDTH); - col_full_second_after_mds(poseidon::HALF_N_FULL_ROUNDS - 1, i) -} - -pub(super) const END: usize = col_output(SPONGE_WIDTH - 1) + 1; diff --git a/system_zero/src/registers/range_check_16.rs b/system_zero/src/registers/range_check_16.rs deleted file mode 100644 index cdb11065..00000000 --- a/system_zero/src/registers/range_check_16.rs +++ /dev/null @@ -1,11 +0,0 @@ -//! Range check unit which checks that values are in `[0, 2^16)`. - -pub(super) const NUM_RANGE_CHECKS: usize = 6; - -/// The input of the `i`th range check, i.e. the value being range checked. -pub(crate) const fn col_rc_16_input(i: usize) -> usize { - debug_assert!(i < NUM_RANGE_CHECKS); - super::START_RANGE_CHECK_16 + i -} - -pub(super) const END: usize = super::START_RANGE_CHECK_16 + NUM_RANGE_CHECKS; diff --git a/system_zero/src/registers/range_check_degree.rs b/system_zero/src/registers/range_check_degree.rs deleted file mode 100644 index caad705d..00000000 --- a/system_zero/src/registers/range_check_degree.rs +++ /dev/null @@ -1,11 +0,0 @@ -//! Range check unit which checks that values are in `[0, degree)`. - -pub(crate) const NUM_RANGE_CHECKS: usize = 5; - -/// The input of the `i`th range check, i.e. the value being range checked. -pub(crate) const fn col_rc_degree_input(i: usize) -> usize { - debug_assert!(i < NUM_RANGE_CHECKS); - super::START_RANGE_CHECK_DEGREE + i -} - -pub(super) const END: usize = super::START_RANGE_CHECK_DEGREE + NUM_RANGE_CHECKS; diff --git a/system_zero/src/system_zero.rs b/system_zero/src/system_zero.rs deleted file mode 100644 index 00673c7e..00000000 --- a/system_zero/src/system_zero.rs +++ /dev/null @@ -1,222 +0,0 @@ -use std::marker::PhantomData; - -use plonky2::field::extension::{Extendable, FieldExtension}; -use plonky2::field::packed::PackedField; -use plonky2::field::polynomial::PolynomialValues; -use plonky2::hash::hash_types::RichField; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use plonky2::timed; -use plonky2::util::timing::TimingTree; -use plonky2::util::transpose; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use starky::permutation::PermutationPair; -use starky::stark::Stark; -use starky::vars::{StarkEvaluationTargets, StarkEvaluationVars}; - -use crate::alu::{eval_alu, eval_alu_circuit, generate_alu}; -use crate::core_registers::{ - eval_core_registers, eval_core_registers_circuit, generate_first_row_core_registers, - generate_next_row_core_registers, -}; -use crate::lookup::{eval_lookups, eval_lookups_circuit, generate_lookups}; -use crate::memory::TransactionMemory; -use crate::permutation_unit::{ - eval_permutation_unit, eval_permutation_unit_circuit, generate_permutation_unit, -}; -use crate::public_input_layout::NUM_PUBLIC_INPUTS; -use crate::registers::{lookup, NUM_COLUMNS}; - -/// We require at least 2^16 rows as it helps support efficient 16-bit range checks. -const MIN_TRACE_ROWS: usize = 1 << 16; - -#[derive(Copy, Clone)] -pub struct SystemZero, const D: usize> { - _phantom: PhantomData, -} - -impl, const D: usize> SystemZero { - /// Generate the rows of the trace. Note that this does not generate the permuted columns used - /// in our lookup arguments, as those are computed after transposing to column-wise form. - fn generate_trace_rows(&self) -> Vec<[F; NUM_COLUMNS]> { - #[allow(unused)] // TODO - let memory = TransactionMemory::default(); - - let mut row = [F::ZERO; NUM_COLUMNS]; - generate_first_row_core_registers(&mut row); - generate_alu(&mut row); - generate_permutation_unit(&mut row); - - let mut trace = Vec::with_capacity(MIN_TRACE_ROWS); - - loop { - let mut next_row = [F::ZERO; NUM_COLUMNS]; - generate_next_row_core_registers(&row, &mut next_row); - generate_alu(&mut next_row); - generate_permutation_unit(&mut next_row); - - trace.push(row); - row = next_row; - - // TODO: Replace with proper termination condition. - if trace.len() == (1 << 16) - 1 { - break; - } - } - - trace.push(row); - trace - } - - pub fn generate_trace(&self) -> Vec> { - let mut timing = TimingTree::new("generate trace", log::Level::Debug); - - // Generate the witness, except for permuted columns in the lookup argument. - let trace_rows = timed!( - &mut timing, - "generate trace rows", - self.generate_trace_rows() - ); - - // Transpose from row-wise to column-wise. - let trace_row_vecs: Vec<_> = timed!( - &mut timing, - "convert to Vecs", - trace_rows.into_iter().map(|row| row.to_vec()).collect() - ); - let mut trace_col_vecs: Vec> = - timed!(&mut timing, "transpose", transpose(&trace_row_vecs)); - - // Generate permuted columns in the lookup argument. - timed!( - &mut timing, - "generate lookup columns", - generate_lookups(&mut trace_col_vecs) - ); - - let trace_polys = timed!( - &mut timing, - "convert to PolynomialValues", - trace_col_vecs - .into_iter() - .map(|column| PolynomialValues::new(column)) - .collect() - ); - - timing.print(); - trace_polys - } -} - -impl, const D: usize> Default for SystemZero { - fn default() -> Self { - Self { - _phantom: PhantomData, - } - } -} - -impl, const D: usize> Stark for SystemZero { - const COLUMNS: usize = NUM_COLUMNS; - const PUBLIC_INPUTS: usize = NUM_PUBLIC_INPUTS; - - fn eval_packed_generic( - &self, - vars: StarkEvaluationVars, - yield_constr: &mut ConstraintConsumer

, - ) where - FE: FieldExtension, - P: PackedField, - { - eval_core_registers(vars, yield_constr); - eval_alu(vars, yield_constr); - eval_permutation_unit::(vars, yield_constr); - eval_lookups(vars, yield_constr); - // TODO: Other units - } - - fn eval_ext_circuit( - &self, - builder: &mut CircuitBuilder, - vars: StarkEvaluationTargets, - yield_constr: &mut RecursiveConstraintConsumer, - ) { - eval_core_registers_circuit(builder, vars, yield_constr); - eval_alu_circuit(builder, vars, yield_constr); - eval_permutation_unit_circuit(builder, vars, yield_constr); - eval_lookups_circuit(builder, vars, yield_constr); - // TODO: Other units - } - - fn constraint_degree(&self) -> usize { - 3 - } - - fn permutation_pairs(&self) -> Vec { - let mut pairs = Vec::new(); - - for i in 0..lookup::NUM_LOOKUPS { - pairs.push(PermutationPair::singletons( - lookup::col_input(i), - lookup::col_permuted_input(i), - )); - pairs.push(PermutationPair::singletons( - lookup::col_table(i), - lookup::col_permuted_table(i), - )); - } - - // TODO: Add permutation pairs for memory. - - pairs - } -} - -#[cfg(test)] -mod tests { - use anyhow::Result; - use log::Level; - use plonky2::field::goldilocks_field::GoldilocksField; - use plonky2::field::types::Field; - use plonky2::plonk::config::PoseidonGoldilocksConfig; - use plonky2::util::timing::TimingTree; - use starky::config::StarkConfig; - use starky::prover::prove; - use starky::stark::Stark; - use starky::stark_testing::test_stark_low_degree; - use starky::verifier::verify_stark_proof; - - use crate::system_zero::SystemZero; - - #[test] - fn run() -> Result<()> { - init_logger(); - - type F = GoldilocksField; - type C = PoseidonGoldilocksConfig; - const D: usize = 2; - - type S = SystemZero; - let system = S::default(); - let public_inputs = [F::ZERO; S::PUBLIC_INPUTS]; - let config = StarkConfig::standard_fast_config(); - let mut timing = TimingTree::new("prove", Level::Debug); - let trace = system.generate_trace(); - let proof = prove::(system, &config, trace, public_inputs, &mut timing)?; - - verify_stark_proof(system, proof, &config) - } - - #[test] - fn degree() -> Result<()> { - type F = GoldilocksField; - const D: usize = 2; - - type S = SystemZero; - let system = S::default(); - test_stark_low_degree(system) - } - - fn init_logger() { - let _ = env_logger::builder().format_timestamp(None).try_init(); - } -}