From bedd2aa711c2628c050a0ec86d9f4f0cbcf71a52 Mon Sep 17 00:00:00 2001 From: Daniel Lubarov Date: Sat, 19 Feb 2022 18:32:11 -0700 Subject: [PATCH 1/3] Rename arithmetic unit to ALU (#496) --- system_zero/src/{arithmetic => alu}/addition.rs | 2 +- system_zero/src/{arithmetic => alu}/division.rs | 2 +- system_zero/src/{arithmetic => alu}/mod.rs | 16 ++++++++-------- .../src/{arithmetic => alu}/multiplication.rs | 2 +- .../src/{arithmetic => alu}/subtraction.rs | 2 +- system_zero/src/lib.rs | 2 +- .../src/registers/{arithmetic.rs => alu.rs} | 10 +++++----- system_zero/src/registers/mod.rs | 6 +++--- system_zero/src/system_zero.rs | 12 +++++------- 9 files changed, 26 insertions(+), 28 deletions(-) rename system_zero/src/{arithmetic => alu}/addition.rs (98%) rename system_zero/src/{arithmetic => alu}/division.rs (96%) rename system_zero/src/{arithmetic => alu}/mod.rs (80%) rename system_zero/src/{arithmetic => alu}/multiplication.rs (96%) rename system_zero/src/{arithmetic => alu}/subtraction.rs (96%) rename system_zero/src/registers/{arithmetic.rs => alu.rs} (84%) diff --git a/system_zero/src/arithmetic/addition.rs b/system_zero/src/alu/addition.rs similarity index 98% rename from system_zero/src/arithmetic/addition.rs rename to system_zero/src/alu/addition.rs index 7aa0d81a..068092e8 100644 --- a/system_zero/src/arithmetic/addition.rs +++ b/system_zero/src/alu/addition.rs @@ -7,7 +7,7 @@ use plonky2::plonk::circuit_builder::CircuitBuilder; use plonky2::plonk::plonk_common::reduce_with_powers_ext_recursive; use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use crate::registers::arithmetic::*; +use crate::registers::alu::*; use crate::registers::NUM_COLUMNS; pub(crate) fn generate_addition(values: &mut [F; NUM_COLUMNS]) { diff --git a/system_zero/src/arithmetic/division.rs b/system_zero/src/alu/division.rs similarity index 96% rename from system_zero/src/arithmetic/division.rs rename to system_zero/src/alu/division.rs index e91288b9..f0d645f1 100644 --- a/system_zero/src/arithmetic/division.rs +++ b/system_zero/src/alu/division.rs @@ -6,7 +6,7 @@ use plonky2::iop::ext_target::ExtensionTarget; use plonky2::plonk::circuit_builder::CircuitBuilder; use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use crate::registers::arithmetic::*; +use crate::registers::alu::*; use crate::registers::NUM_COLUMNS; pub(crate) fn generate_division(values: &mut [F; NUM_COLUMNS]) { diff --git a/system_zero/src/arithmetic/mod.rs b/system_zero/src/alu/mod.rs similarity index 80% rename from system_zero/src/arithmetic/mod.rs rename to system_zero/src/alu/mod.rs index a2b3a4f8..17a12df1 100644 --- a/system_zero/src/arithmetic/mod.rs +++ b/system_zero/src/alu/mod.rs @@ -7,16 +7,16 @@ use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsume use starky::vars::StarkEvaluationTargets; use starky::vars::StarkEvaluationVars; -use crate::arithmetic::addition::{eval_addition, eval_addition_recursively, generate_addition}; -use crate::arithmetic::division::{eval_division, eval_division_recursively, generate_division}; -use crate::arithmetic::multiplication::{ +use crate::alu::addition::{eval_addition, eval_addition_recursively, generate_addition}; +use crate::alu::division::{eval_division, eval_division_recursively, generate_division}; +use crate::alu::multiplication::{ eval_multiplication, eval_multiplication_recursively, generate_multiplication, }; -use crate::arithmetic::subtraction::{ +use crate::alu::subtraction::{ eval_subtraction, eval_subtraction_recursively, generate_subtraction, }; use crate::public_input_layout::NUM_PUBLIC_INPUTS; -use crate::registers::arithmetic::*; +use crate::registers::alu::*; use crate::registers::NUM_COLUMNS; mod addition; @@ -24,7 +24,7 @@ mod division; mod multiplication; mod subtraction; -pub(crate) fn generate_arithmetic_unit(values: &mut [F; NUM_COLUMNS]) { +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() { @@ -36,7 +36,7 @@ pub(crate) fn generate_arithmetic_unit(values: &mut [F; NUM_COL } } -pub(crate) fn eval_arithmetic_unit>( +pub(crate) fn eval_alu>( vars: StarkEvaluationVars, yield_constr: &mut ConstraintConsumer

, ) { @@ -54,7 +54,7 @@ pub(crate) fn eval_arithmetic_unit>( eval_division(local_values, yield_constr); } -pub(crate) fn eval_arithmetic_unit_recursively, const D: usize>( +pub(crate) fn eval_alu_recursively, const D: usize>( builder: &mut CircuitBuilder, vars: StarkEvaluationTargets, yield_constr: &mut RecursiveConstraintConsumer, diff --git a/system_zero/src/arithmetic/multiplication.rs b/system_zero/src/alu/multiplication.rs similarity index 96% rename from system_zero/src/arithmetic/multiplication.rs rename to system_zero/src/alu/multiplication.rs index 70c181d8..a88b42f6 100644 --- a/system_zero/src/arithmetic/multiplication.rs +++ b/system_zero/src/alu/multiplication.rs @@ -6,7 +6,7 @@ use plonky2::iop::ext_target::ExtensionTarget; use plonky2::plonk::circuit_builder::CircuitBuilder; use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use crate::registers::arithmetic::*; +use crate::registers::alu::*; use crate::registers::NUM_COLUMNS; pub(crate) fn generate_multiplication(values: &mut [F; NUM_COLUMNS]) { diff --git a/system_zero/src/arithmetic/subtraction.rs b/system_zero/src/alu/subtraction.rs similarity index 96% rename from system_zero/src/arithmetic/subtraction.rs rename to system_zero/src/alu/subtraction.rs index 267bac72..8f8bb810 100644 --- a/system_zero/src/arithmetic/subtraction.rs +++ b/system_zero/src/alu/subtraction.rs @@ -6,7 +6,7 @@ use plonky2::iop::ext_target::ExtensionTarget; use plonky2::plonk::circuit_builder::CircuitBuilder; use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use crate::registers::arithmetic::*; +use crate::registers::alu::*; use crate::registers::NUM_COLUMNS; pub(crate) fn generate_subtraction(values: &mut [F; NUM_COLUMNS]) { diff --git a/system_zero/src/lib.rs b/system_zero/src/lib.rs index 1c097573..35576cd3 100644 --- a/system_zero/src/lib.rs +++ b/system_zero/src/lib.rs @@ -2,7 +2,7 @@ #![allow(dead_code)] #![allow(unused_variables)] -mod arithmetic; +mod alu; mod core_registers; mod memory; mod permutation_unit; diff --git a/system_zero/src/registers/arithmetic.rs b/system_zero/src/registers/alu.rs similarity index 84% rename from system_zero/src/registers/arithmetic.rs rename to system_zero/src/registers/alu.rs index 92c0d2c3..b4f82dff 100644 --- a/system_zero/src/registers/arithmetic.rs +++ b/system_zero/src/registers/alu.rs @@ -1,13 +1,13 @@ -//! Arithmetic unit. +//! Arithmetic and logic unit. -pub(crate) const IS_ADD: usize = super::START_ARITHMETIC; +pub(crate) const IS_ADD: usize = super::START_ALU; pub(crate) const IS_SUB: usize = IS_ADD + 1; pub(crate) const IS_MUL: usize = IS_SUB + 1; pub(crate) const IS_DIV: usize = IS_MUL + 1; const START_SHARED_COLS: usize = IS_DIV + 1; -/// Within the arithmetic unit, there are shared columns which can be used by any arithmetic +/// 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 = 3; @@ -26,7 +26,7 @@ pub(crate) const COL_ADD_INPUT_3: 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 arithmetic unit. +// 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_1: usize = super::range_check_16::col_rc_16_input(0); /// The second 16-bit chunk of the output, based on little-endian ordering. @@ -34,4 +34,4 @@ pub(crate) const COL_ADD_OUTPUT_2: usize = super::range_check_16::col_rc_16_inpu /// The third 16-bit chunk of the output, based on little-endian ordering. pub(crate) const COL_ADD_OUTPUT_3: usize = super::range_check_16::col_rc_16_input(2); -pub(super) const END: usize = super::START_ARITHMETIC + NUM_SHARED_COLS; +pub(super) const END: usize = super::START_ALU + NUM_SHARED_COLS; diff --git a/system_zero/src/registers/mod.rs b/system_zero/src/registers/mod.rs index 134a28bf..12688b1c 100644 --- a/system_zero/src/registers/mod.rs +++ b/system_zero/src/registers/mod.rs @@ -1,4 +1,4 @@ -pub(crate) mod arithmetic; +pub(crate) mod alu; pub(crate) mod boolean; pub(crate) mod core; pub(crate) mod logic; @@ -8,8 +8,8 @@ pub(crate) mod permutation; pub(crate) mod range_check_16; pub(crate) mod range_check_degree; -const START_ARITHMETIC: usize = 0; -const START_BOOLEAN: usize = arithmetic::END; +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; diff --git a/system_zero/src/system_zero.rs b/system_zero/src/system_zero.rs index cd7796d7..c42a04a8 100644 --- a/system_zero/src/system_zero.rs +++ b/system_zero/src/system_zero.rs @@ -10,9 +10,7 @@ use starky::stark::Stark; use starky::vars::StarkEvaluationTargets; use starky::vars::StarkEvaluationVars; -use crate::arithmetic::{ - eval_arithmetic_unit, eval_arithmetic_unit_recursively, generate_arithmetic_unit, -}; +use crate::alu::{eval_alu, eval_alu_recursively, generate_alu}; use crate::core_registers::{ eval_core_registers, eval_core_registers_recursively, generate_first_row_core_registers, generate_next_row_core_registers, @@ -38,7 +36,7 @@ impl, const D: usize> SystemZero { let mut row = [F::ZERO; NUM_COLUMNS]; generate_first_row_core_registers(&mut row); - generate_arithmetic_unit(&mut row); + generate_alu(&mut row); generate_permutation_unit(&mut row); let mut trace = Vec::with_capacity(MIN_TRACE_ROWS); @@ -46,7 +44,7 @@ impl, const D: usize> SystemZero { loop { let mut next_row = [F::ZERO; NUM_COLUMNS]; generate_next_row_core_registers(&row, &mut next_row); - generate_arithmetic_unit(&mut next_row); + generate_alu(&mut next_row); generate_permutation_unit(&mut next_row); trace.push(row); @@ -84,7 +82,7 @@ impl, const D: usize> Stark for SystemZero, { eval_core_registers(vars, yield_constr); - eval_arithmetic_unit(vars, yield_constr); + eval_alu(vars, yield_constr); eval_permutation_unit::(vars, yield_constr); // TODO: Other units } @@ -96,7 +94,7 @@ impl, const D: usize> Stark for SystemZero, ) { eval_core_registers_recursively(builder, vars, yield_constr); - eval_arithmetic_unit_recursively(builder, vars, yield_constr); + eval_alu_recursively(builder, vars, yield_constr); eval_permutation_unit_recursively(builder, vars, yield_constr); // TODO: Other units } From bc3685587cc371f96eabd7d169498251e1db55b1 Mon Sep 17 00:00:00 2001 From: Daniel Lubarov Date: Sun, 20 Feb 2022 17:48:31 -0700 Subject: [PATCH 2/3] Rename constraint methods (#497) Most of our constraints apply to all rows, and it seems safest to make that the "default". --- starky/src/constraint_consumer.rs | 20 ++++++++++---------- starky/src/fibonacci_stark.rs | 10 ++++++---- system_zero/src/alu/addition.rs | 4 ++-- system_zero/src/alu/mod.rs | 4 ++-- system_zero/src/core_registers.rs | 8 ++++---- system_zero/src/permutation_unit.rs | 28 ++++++++++++---------------- 6 files changed, 36 insertions(+), 38 deletions(-) diff --git a/starky/src/constraint_consumer.rs b/starky/src/constraint_consumer.rs index 88f66118..ada28730 100644 --- a/starky/src/constraint_consumer.rs +++ b/starky/src/constraint_consumer.rs @@ -53,12 +53,12 @@ impl ConstraintConsumer

{ } /// Add one constraint valid on all rows except the last. - pub fn constraint(&mut self, constraint: P) { - self.constraint_wrapping(constraint * self.z_last); + pub fn constraint_transition(&mut self, constraint: P) { + self.constraint(constraint * self.z_last); } /// Add one constraint on all rows. - pub fn constraint_wrapping(&mut self, constraint: P) { + pub fn constraint(&mut self, constraint: P) { for (&alpha, acc) in self.alphas.iter().zip(&mut self.constraint_accs) { *acc *= alpha; *acc += constraint; @@ -68,13 +68,13 @@ impl ConstraintConsumer

{ /// Add one constraint, but first multiply it by a filter such that it will only apply to the /// first row of the trace. pub fn constraint_first_row(&mut self, constraint: P) { - self.constraint_wrapping(constraint * self.lagrange_basis_first); + self.constraint(constraint * self.lagrange_basis_first); } /// Add one constraint, but first multiply it by a filter such that it will only apply to the /// last row of the trace. pub fn constraint_last_row(&mut self, constraint: P) { - self.constraint_wrapping(constraint * self.lagrange_basis_last); + self.constraint(constraint * self.lagrange_basis_last); } } @@ -122,17 +122,17 @@ impl, const D: usize> RecursiveConstraintConsumer, constraint: ExtensionTarget, ) { let filtered_constraint = builder.mul_extension(constraint, self.z_last); - self.constraint_wrapping(builder, filtered_constraint); + self.constraint(builder, filtered_constraint); } /// Add one constraint valid on all rows. - pub fn constraint_wrapping( + pub fn constraint( &mut self, builder: &mut CircuitBuilder, constraint: ExtensionTarget, @@ -150,7 +150,7 @@ impl, const D: usize> RecursiveConstraintConsumer, ) { let filtered_constraint = builder.mul_extension(constraint, self.lagrange_basis_first); - self.constraint_wrapping(builder, filtered_constraint); + self.constraint(builder, filtered_constraint); } /// Add one constraint, but first multiply it by a filter such that it will only apply to the @@ -161,6 +161,6 @@ impl, const D: usize> RecursiveConstraintConsumer, ) { let filtered_constraint = builder.mul_extension(constraint, self.lagrange_basis_last); - self.constraint_wrapping(builder, filtered_constraint); + self.constraint(builder, filtered_constraint); } } diff --git a/starky/src/fibonacci_stark.rs b/starky/src/fibonacci_stark.rs index bd1775e1..a0204359 100644 --- a/starky/src/fibonacci_stark.rs +++ b/starky/src/fibonacci_stark.rs @@ -68,9 +68,11 @@ impl, const D: usize> Stark for FibonacciStar .constraint_last_row(vars.local_values[1] - vars.public_inputs[Self::PI_INDEX_RES]); // x0' <- x1 - yield_constr.constraint(vars.next_values[0] - vars.local_values[1]); + yield_constr.constraint_transition(vars.next_values[0] - vars.local_values[1]); // x1' <- x0 + x1 - yield_constr.constraint(vars.next_values[1] - vars.local_values[0] - vars.local_values[1]); + yield_constr.constraint_transition( + vars.next_values[1] - vars.local_values[0] - vars.local_values[1], + ); } fn eval_ext_recursively( @@ -91,13 +93,13 @@ impl, const D: usize> Stark for FibonacciStar // x0' <- x1 let first_col_constraint = builder.sub_extension(vars.next_values[0], vars.local_values[1]); - yield_constr.constraint(builder, first_col_constraint); + yield_constr.constraint_transition(builder, first_col_constraint); // x1' <- x0 + x1 let second_col_constraint = { let tmp = builder.sub_extension(vars.next_values[1], vars.local_values[0]); builder.sub_extension(tmp, vars.local_values[1]) }; - yield_constr.constraint(builder, second_col_constraint); + yield_constr.constraint_transition(builder, second_col_constraint); } fn constraint_degree(&self) -> usize { diff --git a/system_zero/src/alu/addition.rs b/system_zero/src/alu/addition.rs index 068092e8..dc83ecb8 100644 --- a/system_zero/src/alu/addition.rs +++ b/system_zero/src/alu/addition.rs @@ -41,7 +41,7 @@ pub(crate) fn eval_addition>( let computed_out = in_1 + in_2 + in_3; - yield_constr.constraint_wrapping(is_add * (out - computed_out)); + yield_constr.constraint(is_add * (out - computed_out)); } pub(crate) fn eval_addition_recursively, const D: usize>( @@ -66,5 +66,5 @@ pub(crate) fn eval_addition_recursively, const D: u let diff = builder.sub_extension(out, computed_out); let filtered_diff = builder.mul_extension(is_add, diff); - yield_constr.constraint_wrapping(builder, filtered_diff); + yield_constr.constraint(builder, filtered_diff); } diff --git a/system_zero/src/alu/mod.rs b/system_zero/src/alu/mod.rs index 17a12df1..4e7e09fa 100644 --- a/system_zero/src/alu/mod.rs +++ b/system_zero/src/alu/mod.rs @@ -45,7 +45,7 @@ pub(crate) fn eval_alu>( // Check that the operation flag values are binary. for col in [IS_ADD, IS_SUB, IS_MUL, IS_DIV] { let val = local_values[col]; - yield_constr.constraint_wrapping(val * val - val); + yield_constr.constraint(val * val - val); } eval_addition(local_values, yield_constr); @@ -65,7 +65,7 @@ pub(crate) fn eval_alu_recursively, const D: usize> for col in [IS_ADD, IS_SUB, IS_MUL, IS_DIV] { let val = local_values[col]; let constraint = builder.mul_sub_extension(val, val, val); - yield_constr.constraint_wrapping(builder, constraint); + yield_constr.constraint(builder, constraint); } eval_addition_recursively(builder, local_values, yield_constr); diff --git a/system_zero/src/core_registers.rs b/system_zero/src/core_registers.rs index c8c6533b..1f33611a 100644 --- a/system_zero/src/core_registers.rs +++ b/system_zero/src/core_registers.rs @@ -49,7 +49,7 @@ pub(crate) fn eval_core_registers>( 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(delta_clock - F::ONE); + 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]; @@ -57,7 +57,7 @@ pub(crate) fn eval_core_registers>( 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(delta_range_16 * delta_range_16 - delta_range_16); + yield_constr.constraint_transition(delta_range_16 * delta_range_16 - delta_range_16); // TODO constraints for stack etc. } @@ -77,7 +77,7 @@ pub(crate) fn eval_core_registers_recursively, cons 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(builder, constraint); + 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]; @@ -87,7 +87,7 @@ pub(crate) fn eval_core_registers_recursively, cons 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(builder, constraint); + yield_constr.constraint_transition(builder, constraint); // TODO constraints for stack etc. } diff --git a/system_zero/src/permutation_unit.rs b/system_zero/src/permutation_unit.rs index 366cff65..079ab14a 100644 --- a/system_zero/src/permutation_unit.rs +++ b/system_zero/src/permutation_unit.rs @@ -127,8 +127,7 @@ pub(crate) fn eval_permutation_unit( for i in 0..SPONGE_WIDTH { let state_cubed = state[i] * state[i].square(); - yield_constr - .constraint_wrapping(state_cubed - local_values[col_full_first_mid_sbox(r, i)]); + 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. } @@ -136,8 +135,7 @@ pub(crate) fn eval_permutation_unit( state = mds_layer(state); for i in 0..SPONGE_WIDTH { - yield_constr - .constraint_wrapping(state[i] - local_values[col_full_first_after_mds(r, i)]); + 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)]; } } @@ -146,10 +144,10 @@ pub(crate) fn eval_permutation_unit( state = constant_layer(state, HALF_N_FULL_ROUNDS + r); let state0_cubed = state[0] * state[0].square(); - yield_constr.constraint_wrapping(state0_cubed - local_values[col_partial_mid_sbox(r)]); + 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_wrapping(state[0] - local_values[col_partial_after_sbox(r)]); + 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); @@ -160,8 +158,7 @@ pub(crate) fn eval_permutation_unit( for i in 0..SPONGE_WIDTH { let state_cubed = state[i] * state[i].square(); - yield_constr - .constraint_wrapping(state_cubed - local_values[col_full_second_mid_sbox(r, i)]); + 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. } @@ -169,8 +166,7 @@ pub(crate) fn eval_permutation_unit( state = mds_layer(state); for i in 0..SPONGE_WIDTH { - yield_constr - .constraint_wrapping(state[i] - local_values[col_full_second_after_mds(r, i)]); + 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)]; } } @@ -197,7 +193,7 @@ pub(crate) fn eval_permutation_unit_recursively, co 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_wrapping(builder, diff); + 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. @@ -208,7 +204,7 @@ pub(crate) fn eval_permutation_unit_recursively, co 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_wrapping(builder, diff); + yield_constr.constraint(builder, diff); state[i] = local_values[col_full_first_after_mds(r, i)]; } } @@ -218,11 +214,11 @@ pub(crate) fn eval_permutation_unit_recursively, co 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_wrapping(builder, diff); + 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_wrapping(builder, diff); + yield_constr.constraint(builder, diff); state[0] = local_values[col_partial_after_sbox(r)]; state = F::mds_layer_recursive(builder, &state); @@ -239,7 +235,7 @@ pub(crate) fn eval_permutation_unit_recursively, co 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_wrapping(builder, diff); + 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. @@ -250,7 +246,7 @@ pub(crate) fn eval_permutation_unit_recursively, co 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_wrapping(builder, diff); + yield_constr.constraint(builder, diff); state[i] = local_values[col_full_second_after_mds(r, i)]; } } From 6072fab0770eb2f9797bdc09997e72b85282e77f Mon Sep 17 00:00:00 2001 From: Daniel Lubarov Date: Mon, 21 Feb 2022 00:39:04 -0800 Subject: [PATCH 3/3] Implement a mul-add circuit in the ALU (#495) * Implement a mul-add circuit in the ALU The inputs are assumed to be `u32`s, while the output is encoded as four `u16 limbs`. Each output limb is range-checked. So, our basic mul-add constraint looks like out_0 + 2^16 out_1 + 2^32 out_2 + 2^48 out_3 = in_1 * in_2 + in_3 The right hand side will never overflow, since `u32::MAX * u32::MAX + u32::MAX < |F|`. However, the left hand side could overflow, even though we know each limb is less than `2^16`. For example, an operation like `0 * 0 + 0` could have two possible outputs, 0 and `|F|`, both of which would satisfy the constraint above. To prevent these non-canonical outputs, we need a comparison to enforce that `out < |F|`. Thankfully, `F::MAX` has all zeros in its low 32 bits, so `x <= F::MAX` is equivalent to `x_lo == 0 || x_hi != u32::MAX`. `x_hi != u32::MAX` can be checked by showing that `u32::MAX - x_hi` has an inverse. If `x_hi != u32::MAX`, the prover provides this (purported) inverse in an advice column. See @bobbinth's [post](https://hackmd.io/NC-yRmmtRQSvToTHb96e8Q#Checking-element-validity) for details. That post calls the purported inverse column `m`; I named it `canonical_inv` in this code. * fix * PR feedback * naming --- system_zero/Cargo.toml | 1 + system_zero/src/alu/addition.rs | 36 ++++----- system_zero/src/alu/canonical.rs | 109 ++++++++++++++++++++++++++ system_zero/src/alu/mod.rs | 13 ++- system_zero/src/alu/mul_add.rs | 88 +++++++++++++++++++++ system_zero/src/alu/multiplication.rs | 31 -------- system_zero/src/registers/alu.rs | 34 ++++++-- 7 files changed, 249 insertions(+), 63 deletions(-) create mode 100644 system_zero/src/alu/canonical.rs create mode 100644 system_zero/src/alu/mul_add.rs delete mode 100644 system_zero/src/alu/multiplication.rs diff --git a/system_zero/Cargo.toml b/system_zero/Cargo.toml index e5b617c9..032bfb53 100644 --- a/system_zero/Cargo.toml +++ b/system_zero/Cargo.toml @@ -6,6 +6,7 @@ edition = "2021" [dependencies] plonky2 = { path = "../plonky2" } +plonky2_util = { path = "../util" } starky = { path = "../starky" } anyhow = "1.0.40" env_logger = "0.9.0" diff --git a/system_zero/src/alu/addition.rs b/system_zero/src/alu/addition.rs index dc83ecb8..c2293b4a 100644 --- a/system_zero/src/alu/addition.rs +++ b/system_zero/src/alu/addition.rs @@ -11,14 +11,14 @@ 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_1].to_canonical_u64(); - let in_2 = values[COL_ADD_INPUT_2].to_canonical_u64(); - let in_3 = values[COL_ADD_INPUT_3].to_canonical_u64(); + 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_1] = F::from_canonical_u16(output as u16); - values[COL_ADD_OUTPUT_2] = F::from_canonical_u16((output >> 16) as u16); - values[COL_ADD_OUTPUT_3] = F::from_canonical_u16((output >> 32) as u16); + 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>( @@ -26,12 +26,12 @@ pub(crate) fn eval_addition>( yield_constr: &mut ConstraintConsumer

, ) { let is_add = local_values[IS_ADD]; - let in_1 = local_values[COL_ADD_INPUT_1]; - let in_2 = local_values[COL_ADD_INPUT_2]; - let in_3 = local_values[COL_ADD_INPUT_3]; - let out_1 = local_values[COL_ADD_OUTPUT_1]; - let out_2 = local_values[COL_ADD_OUTPUT_2]; - let out_3 = local_values[COL_ADD_OUTPUT_3]; + 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); @@ -50,12 +50,12 @@ pub(crate) fn eval_addition_recursively, const D: u yield_constr: &mut RecursiveConstraintConsumer, ) { let is_add = local_values[IS_ADD]; - let in_1 = local_values[COL_ADD_INPUT_1]; - let in_2 = local_values[COL_ADD_INPUT_2]; - let in_3 = local_values[COL_ADD_INPUT_3]; - let out_1 = local_values[COL_ADD_OUTPUT_1]; - let out_2 = local_values[COL_ADD_OUTPUT_2]; - let out_3 = local_values[COL_ADD_OUTPUT_3]; + 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, diff --git a/system_zero/src/alu/canonical.rs b/system_zero/src/alu/canonical.rs new file mode 100644 index 00000000..fb90eb0d --- /dev/null +++ b/system_zero/src/alu/canonical.rs @@ -0,0 +1,109 @@ +//! 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_field::Extendable; +use plonky2::field::field_types::Field; +use plonky2::field::packed_field::PackedField; +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/mod.rs b/system_zero/src/alu/mod.rs index 4e7e09fa..730ca302 100644 --- a/system_zero/src/alu/mod.rs +++ b/system_zero/src/alu/mod.rs @@ -9,9 +9,7 @@ use starky::vars::StarkEvaluationVars; use crate::alu::addition::{eval_addition, eval_addition_recursively, generate_addition}; use crate::alu::division::{eval_division, eval_division_recursively, generate_division}; -use crate::alu::multiplication::{ - eval_multiplication, eval_multiplication_recursively, generate_multiplication, -}; +use crate::alu::mul_add::{eval_mul_add, eval_mul_add_recursively, generate_mul_add}; use crate::alu::subtraction::{ eval_subtraction, eval_subtraction_recursively, generate_subtraction, }; @@ -20,8 +18,9 @@ use crate::registers::alu::*; use crate::registers::NUM_COLUMNS; mod addition; +mod canonical; mod division; -mod multiplication; +mod mul_add; mod subtraction; pub(crate) fn generate_alu(values: &mut [F; NUM_COLUMNS]) { @@ -30,7 +29,7 @@ pub(crate) fn generate_alu(values: &mut [F; NUM_COLUMNS]) { } else if values[IS_SUB].is_one() { generate_subtraction(values); } else if values[IS_MUL].is_one() { - generate_multiplication(values); + generate_mul_add(values); } else if values[IS_DIV].is_one() { generate_division(values); } @@ -50,7 +49,7 @@ pub(crate) fn eval_alu>( eval_addition(local_values, yield_constr); eval_subtraction(local_values, yield_constr); - eval_multiplication(local_values, yield_constr); + eval_mul_add(local_values, yield_constr); eval_division(local_values, yield_constr); } @@ -70,6 +69,6 @@ pub(crate) fn eval_alu_recursively, const D: usize> eval_addition_recursively(builder, local_values, yield_constr); eval_subtraction_recursively(builder, local_values, yield_constr); - eval_multiplication_recursively(builder, local_values, yield_constr); + eval_mul_add_recursively(builder, local_values, yield_constr); eval_division_recursively(builder, local_values, yield_constr); } diff --git a/system_zero/src/alu/mul_add.rs b/system_zero/src/alu/mul_add.rs new file mode 100644 index 00000000..53ba34a2 --- /dev/null +++ b/system_zero/src/alu/mul_add.rs @@ -0,0 +1,88 @@ +use plonky2::field::extension_field::Extendable; +use plonky2::field::field_types::{Field, PrimeField64}; +use plonky2::field::packed_field::PackedField; +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]; + 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; + let output = combine_u16s_check_canonical( + output_1, + output_2, + output_3, + output_4, + result_canonical_inv, + yield_constr, + ); + yield_constr.constraint(computed_output - output); +} + +pub(crate) fn eval_mul_add_recursively, const D: usize>( + builder: &mut CircuitBuilder, + local_values: &[ExtensionTarget; NUM_COLUMNS], + yield_constr: &mut RecursiveConstraintConsumer, +) { + let is_mul = local_values[IS_MUL]; + 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); + 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); + yield_constr.constraint(builder, diff); +} diff --git a/system_zero/src/alu/multiplication.rs b/system_zero/src/alu/multiplication.rs deleted file mode 100644 index a88b42f6..00000000 --- a/system_zero/src/alu/multiplication.rs +++ /dev/null @@ -1,31 +0,0 @@ -use plonky2::field::extension_field::Extendable; -use plonky2::field::field_types::{Field, PrimeField64}; -use plonky2::field::packed_field::PackedField; -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_multiplication(values: &mut [F; NUM_COLUMNS]) { - // TODO -} - -pub(crate) fn eval_multiplication>( - local_values: &[P; NUM_COLUMNS], - yield_constr: &mut ConstraintConsumer

, -) { - let is_mul = local_values[IS_MUL]; - // TODO -} - -pub(crate) fn eval_multiplication_recursively, const D: usize>( - builder: &mut CircuitBuilder, - local_values: &[ExtensionTarget; NUM_COLUMNS], - yield_constr: &mut RecursiveConstraintConsumer, -) { - let is_mul = local_values[IS_MUL]; - // TODO -} diff --git a/system_zero/src/registers/alu.rs b/system_zero/src/registers/alu.rs index b4f82dff..e678d8e4 100644 --- a/system_zero/src/registers/alu.rs +++ b/system_zero/src/registers/alu.rs @@ -10,7 +10,7 @@ const START_SHARED_COLS: usize = IS_DIV + 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 = 3; +const NUM_SHARED_COLS: usize = 4; const fn shared_col(i: usize) -> usize { debug_assert!(i < NUM_SHARED_COLS); @@ -18,20 +18,40 @@ const fn shared_col(i: usize) -> usize { } /// The first value to be added; treated as an unsigned u32. -pub(crate) const COL_ADD_INPUT_1: usize = shared_col(0); +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_2: usize = shared_col(1); +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_3: usize = shared_col(2); +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_1: usize = super::range_check_16::col_rc_16_input(0); +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_2: usize = super::range_check_16::col_rc_16_input(1); +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_3: usize = super::range_check_16::col_rc_16_input(2); +pub(crate) const COL_ADD_OUTPUT_2: usize = super::range_check_16::col_rc_16_input(2); + +/// 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); pub(super) const END: usize = super::START_ALU + NUM_SHARED_COLS;