diff --git a/Cargo.toml b/Cargo.toml index da3c8d95..43a7ed2b 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -93,6 +93,7 @@ cloned_instead_of_copied = "warn" copy_iterator = "warn" default_trait_access = "warn" doc_link_with_quotes = "warn" +enum_glob_use = "warn" expl_impl_clone_on_copy = "warn" explicit_deref_methods = "warn" explicit_into_iter_loop = "warn" @@ -145,6 +146,7 @@ unnested_or_patterns = "warn" unused_async = "warn" used_underscore_binding = "warn" verbose_bit_mask = "warn" +wildcard_imports = "warn" [workspace.dependencies.cargo-husky] version = "1.5" diff --git a/triton-air/src/lib.rs b/triton-air/src/lib.rs index 7f4c3697..0e413fc1 100644 --- a/triton-air/src/lib.rs +++ b/triton-air/src/lib.rs @@ -25,7 +25,7 @@ pub mod table_column; /// - introduce new constraints `e = b²`, `f = c²`, and `g = e·f`, /// - replace the original constraint with `a = g·d`. /// -/// The degree lowering happens in the Triton VM's build script, `build.rs`. +/// The degree lowering happens in Triton VM's build script, `build.rs`. pub const TARGET_DEGREE: isize = 4; pub trait AIR { diff --git a/triton-air/src/table/processor.rs b/triton-air/src/table/processor.rs index e897297a..6c4b105e 100644 --- a/triton-air/src/table/processor.rs +++ b/triton-air/src/table/processor.rs @@ -25,56 +25,6 @@ use twenty_first::math::x_field_element::EXTENSION_DEGREE; use twenty_first::prelude::*; use crate::challenge_id::ChallengeId; -use crate::challenge_id::ChallengeId::ClockJumpDifferenceLookupIndeterminate; -use crate::challenge_id::ChallengeId::CompressProgramDigestIndeterminate; -use crate::challenge_id::ChallengeId::CompressedProgramDigest; -use crate::challenge_id::ChallengeId::HashCIWeight; -use crate::challenge_id::ChallengeId::HashDigestIndeterminate; -use crate::challenge_id::ChallengeId::HashInputIndeterminate; -use crate::challenge_id::ChallengeId::InstructionLookupIndeterminate; -use crate::challenge_id::ChallengeId::JumpStackCiWeight; -use crate::challenge_id::ChallengeId::JumpStackClkWeight; -use crate::challenge_id::ChallengeId::JumpStackIndeterminate; -use crate::challenge_id::ChallengeId::JumpStackJsdWeight; -use crate::challenge_id::ChallengeId::JumpStackJsoWeight; -use crate::challenge_id::ChallengeId::JumpStackJspWeight; -use crate::challenge_id::ChallengeId::OpStackClkWeight; -use crate::challenge_id::ChallengeId::OpStackFirstUnderflowElementWeight; -use crate::challenge_id::ChallengeId::OpStackIb1Weight; -use crate::challenge_id::ChallengeId::OpStackIndeterminate; -use crate::challenge_id::ChallengeId::OpStackPointerWeight; -use crate::challenge_id::ChallengeId::ProgramAddressWeight; -use crate::challenge_id::ChallengeId::ProgramInstructionWeight; -use crate::challenge_id::ChallengeId::ProgramNextInstructionWeight; -use crate::challenge_id::ChallengeId::RamClkWeight; -use crate::challenge_id::ChallengeId::RamIndeterminate; -use crate::challenge_id::ChallengeId::RamInstructionTypeWeight; -use crate::challenge_id::ChallengeId::RamPointerWeight; -use crate::challenge_id::ChallengeId::RamValueWeight; -use crate::challenge_id::ChallengeId::SpongeIndeterminate; -use crate::challenge_id::ChallengeId::StackWeight0; -use crate::challenge_id::ChallengeId::StackWeight1; -use crate::challenge_id::ChallengeId::StackWeight10; -use crate::challenge_id::ChallengeId::StackWeight11; -use crate::challenge_id::ChallengeId::StackWeight12; -use crate::challenge_id::ChallengeId::StackWeight13; -use crate::challenge_id::ChallengeId::StackWeight14; -use crate::challenge_id::ChallengeId::StackWeight15; -use crate::challenge_id::ChallengeId::StackWeight2; -use crate::challenge_id::ChallengeId::StackWeight3; -use crate::challenge_id::ChallengeId::StackWeight4; -use crate::challenge_id::ChallengeId::StackWeight5; -use crate::challenge_id::ChallengeId::StackWeight6; -use crate::challenge_id::ChallengeId::StackWeight7; -use crate::challenge_id::ChallengeId::StackWeight8; -use crate::challenge_id::ChallengeId::StackWeight9; -use crate::challenge_id::ChallengeId::StandardInputIndeterminate; -use crate::challenge_id::ChallengeId::StandardOutputIndeterminate; -use crate::challenge_id::ChallengeId::U32CiWeight; -use crate::challenge_id::ChallengeId::U32Indeterminate; -use crate::challenge_id::ChallengeId::U32LhsWeight; -use crate::challenge_id::ChallengeId::U32ResultWeight; -use crate::challenge_id::ChallengeId::U32RhsWeight; use crate::cross_table_argument::CrossTableArg; use crate::cross_table_argument::EvalArg; use crate::cross_table_argument::LookupArg; @@ -82,58 +32,6 @@ use crate::cross_table_argument::PermArg; use crate::table; use crate::table_column::MasterAuxColumn; use crate::table_column::MasterMainColumn; -use crate::table_column::ProcessorAuxColumn; -use crate::table_column::ProcessorAuxColumn::ClockJumpDifferenceLookupServerLogDerivative; -use crate::table_column::ProcessorAuxColumn::HashDigestEvalArg; -use crate::table_column::ProcessorAuxColumn::HashInputEvalArg; -use crate::table_column::ProcessorAuxColumn::InputTableEvalArg; -use crate::table_column::ProcessorAuxColumn::InstructionLookupClientLogDerivative; -use crate::table_column::ProcessorAuxColumn::JumpStackTablePermArg; -use crate::table_column::ProcessorAuxColumn::OpStackTablePermArg; -use crate::table_column::ProcessorAuxColumn::OutputTableEvalArg; -use crate::table_column::ProcessorAuxColumn::RamTablePermArg; -use crate::table_column::ProcessorAuxColumn::SpongeEvalArg; -use crate::table_column::ProcessorAuxColumn::U32LookupClientLogDerivative; -use crate::table_column::ProcessorMainColumn; -use crate::table_column::ProcessorMainColumn::ClockJumpDifferenceLookupMultiplicity; -use crate::table_column::ProcessorMainColumn::IsPadding; -use crate::table_column::ProcessorMainColumn::OpStackPointer; -use crate::table_column::ProcessorMainColumn::CI; -use crate::table_column::ProcessorMainColumn::CLK; -use crate::table_column::ProcessorMainColumn::HV0; -use crate::table_column::ProcessorMainColumn::HV1; -use crate::table_column::ProcessorMainColumn::HV2; -use crate::table_column::ProcessorMainColumn::HV3; -use crate::table_column::ProcessorMainColumn::HV4; -use crate::table_column::ProcessorMainColumn::HV5; -use crate::table_column::ProcessorMainColumn::IB0; -use crate::table_column::ProcessorMainColumn::IB1; -use crate::table_column::ProcessorMainColumn::IB2; -use crate::table_column::ProcessorMainColumn::IB3; -use crate::table_column::ProcessorMainColumn::IB4; -use crate::table_column::ProcessorMainColumn::IB5; -use crate::table_column::ProcessorMainColumn::IB6; -use crate::table_column::ProcessorMainColumn::IP; -use crate::table_column::ProcessorMainColumn::JSD; -use crate::table_column::ProcessorMainColumn::JSO; -use crate::table_column::ProcessorMainColumn::JSP; -use crate::table_column::ProcessorMainColumn::NIA; -use crate::table_column::ProcessorMainColumn::ST0; -use crate::table_column::ProcessorMainColumn::ST1; -use crate::table_column::ProcessorMainColumn::ST10; -use crate::table_column::ProcessorMainColumn::ST11; -use crate::table_column::ProcessorMainColumn::ST12; -use crate::table_column::ProcessorMainColumn::ST13; -use crate::table_column::ProcessorMainColumn::ST14; -use crate::table_column::ProcessorMainColumn::ST15; -use crate::table_column::ProcessorMainColumn::ST2; -use crate::table_column::ProcessorMainColumn::ST3; -use crate::table_column::ProcessorMainColumn::ST4; -use crate::table_column::ProcessorMainColumn::ST5; -use crate::table_column::ProcessorMainColumn::ST6; -use crate::table_column::ProcessorMainColumn::ST7; -use crate::table_column::ProcessorMainColumn::ST8; -use crate::table_column::ProcessorMainColumn::ST9; use crate::AIR; /// The number of helper variable registers @@ -142,33 +40,36 @@ pub const NUM_HELPER_VARIABLE_REGISTERS: usize = 6; #[derive(Debug, Copy, Clone, Eq, PartialEq)] pub struct ProcessorTable; +type MainColumn = ::MainColumn; +type AuxColumn = ::AuxColumn; + impl ProcessorTable { /// # Panics /// /// Panics if the index is out of bounds. - pub fn op_stack_column_by_index(index: usize) -> ProcessorMainColumn { + pub fn op_stack_column_by_index(index: usize) -> MainColumn { assert!( index < OpStackElement::COUNT, "Op Stack column index must be in [0, 15], not {index}" ); match index { - 0 => ST0, - 1 => ST1, - 2 => ST2, - 3 => ST3, - 4 => ST4, - 5 => ST5, - 6 => ST6, - 7 => ST7, - 8 => ST8, - 9 => ST9, - 10 => ST10, - 11 => ST11, - 12 => ST12, - 13 => ST13, - 14 => ST14, - 15 => ST15, + 0 => MainColumn::ST0, + 1 => MainColumn::ST1, + 2 => MainColumn::ST2, + 3 => MainColumn::ST3, + 4 => MainColumn::ST4, + 5 => MainColumn::ST5, + 6 => MainColumn::ST6, + 7 => MainColumn::ST7, + 8 => MainColumn::ST8, + 9 => MainColumn::ST9, + 10 => MainColumn::ST10, + 11 => MainColumn::ST11, + 12 => MainColumn::ST12, + 13 => MainColumn::ST13, + 14 => MainColumn::ST14, + 15 => MainColumn::ST15, _ => unreachable!(), } } @@ -184,82 +85,83 @@ impl AIR for ProcessorTable { let constant = |c: u32| circuit_builder.b_constant(c); let x_constant = |x| circuit_builder.x_constant(x); let challenge = |c| circuit_builder.challenge(c); - let main_row = - |col: ProcessorMainColumn| circuit_builder.input(Main(col.master_main_index())); - let aux_row = |col: ProcessorAuxColumn| circuit_builder.input(Aux(col.master_aux_index())); - - let clk_is_0 = main_row(CLK); - let ip_is_0 = main_row(IP); - let jsp_is_0 = main_row(JSP); - let jso_is_0 = main_row(JSO); - let jsd_is_0 = main_row(JSD); - let st0_is_0 = main_row(ST0); - let st1_is_0 = main_row(ST1); - let st2_is_0 = main_row(ST2); - let st3_is_0 = main_row(ST3); - let st4_is_0 = main_row(ST4); - let st5_is_0 = main_row(ST5); - let st6_is_0 = main_row(ST6); - let st7_is_0 = main_row(ST7); - let st8_is_0 = main_row(ST8); - let st9_is_0 = main_row(ST9); - let st10_is_0 = main_row(ST10); - let op_stack_pointer_is_16 = main_row(OpStackPointer) - constant(16); + let main_row = |col: MainColumn| circuit_builder.input(Main(col.master_main_index())); + let aux_row = |col: AuxColumn| circuit_builder.input(Aux(col.master_aux_index())); + + let clk_is_0 = main_row(MainColumn::CLK); + let ip_is_0 = main_row(MainColumn::IP); + let jsp_is_0 = main_row(MainColumn::JSP); + let jso_is_0 = main_row(MainColumn::JSO); + let jsd_is_0 = main_row(MainColumn::JSD); + let st0_is_0 = main_row(MainColumn::ST0); + let st1_is_0 = main_row(MainColumn::ST1); + let st2_is_0 = main_row(MainColumn::ST2); + let st3_is_0 = main_row(MainColumn::ST3); + let st4_is_0 = main_row(MainColumn::ST4); + let st5_is_0 = main_row(MainColumn::ST5); + let st6_is_0 = main_row(MainColumn::ST6); + let st7_is_0 = main_row(MainColumn::ST7); + let st8_is_0 = main_row(MainColumn::ST8); + let st9_is_0 = main_row(MainColumn::ST9); + let st10_is_0 = main_row(MainColumn::ST10); + let op_stack_pointer_is_16 = main_row(MainColumn::OpStackPointer) - constant(16); // Compress the program digest using an Evaluation Argument. // Lowest index in the digest corresponds to lowest index on the stack. let program_digest: [_; Digest::LEN] = [ - main_row(ST11), - main_row(ST12), - main_row(ST13), - main_row(ST14), - main_row(ST15), + main_row(MainColumn::ST11), + main_row(MainColumn::ST12), + main_row(MainColumn::ST13), + main_row(MainColumn::ST14), + main_row(MainColumn::ST15), ]; let compressed_program_digest = program_digest.into_iter().fold( circuit_builder.x_constant(EvalArg::default_initial()), |acc, digest_element| { - acc * challenge(CompressProgramDigestIndeterminate) + digest_element + acc * challenge(ChallengeId::CompressProgramDigestIndeterminate) + digest_element }, ); let compressed_program_digest_is_expected_program_digest = - compressed_program_digest - challenge(CompressedProgramDigest); + compressed_program_digest - challenge(ChallengeId::CompressedProgramDigest); // Permutation and Evaluation Arguments with all tables the Processor Table relates to // standard input let running_evaluation_for_standard_input_is_initialized_correctly = - aux_row(InputTableEvalArg) - x_constant(EvalArg::default_initial()); + aux_row(AuxColumn::InputTableEvalArg) - x_constant(EvalArg::default_initial()); // program table - let instruction_lookup_indeterminate = challenge(InstructionLookupIndeterminate); - let instruction_ci_weight = challenge(ProgramInstructionWeight); - let instruction_nia_weight = challenge(ProgramNextInstructionWeight); - let compressed_row_for_instruction_lookup = - instruction_ci_weight * main_row(CI) + instruction_nia_weight * main_row(NIA); + let instruction_lookup_indeterminate = + challenge(ChallengeId::InstructionLookupIndeterminate); + let instruction_ci_weight = challenge(ChallengeId::ProgramInstructionWeight); + let instruction_nia_weight = challenge(ChallengeId::ProgramNextInstructionWeight); + let compressed_row_for_instruction_lookup = instruction_ci_weight + * main_row(MainColumn::CI) + + instruction_nia_weight * main_row(MainColumn::NIA); let instruction_lookup_log_derivative_is_initialized_correctly = - (aux_row(InstructionLookupClientLogDerivative) + (aux_row(AuxColumn::InstructionLookupClientLogDerivative) - x_constant(LookupArg::default_initial())) * (instruction_lookup_indeterminate - compressed_row_for_instruction_lookup) - constant(1); // standard output let running_evaluation_for_standard_output_is_initialized_correctly = - aux_row(OutputTableEvalArg) - x_constant(EvalArg::default_initial()); + aux_row(AuxColumn::OutputTableEvalArg) - x_constant(EvalArg::default_initial()); let running_product_for_op_stack_table_is_initialized_correctly = - aux_row(OpStackTablePermArg) - x_constant(PermArg::default_initial()); + aux_row(AuxColumn::OpStackTablePermArg) - x_constant(PermArg::default_initial()); // ram table let running_product_for_ram_table_is_initialized_correctly = - aux_row(RamTablePermArg) - x_constant(PermArg::default_initial()); + aux_row(AuxColumn::RamTablePermArg) - x_constant(PermArg::default_initial()); // jump-stack table - let jump_stack_indeterminate = challenge(JumpStackIndeterminate); - let jump_stack_ci_weight = challenge(JumpStackCiWeight); + let jump_stack_indeterminate = challenge(ChallengeId::JumpStackIndeterminate); + let jump_stack_ci_weight = challenge(ChallengeId::JumpStackCiWeight); // note: `clk`, `jsp`, `jso`, and `jsd` are already constrained to be 0. - let compressed_row_for_jump_stack_table = jump_stack_ci_weight * main_row(CI); + let compressed_row_for_jump_stack_table = jump_stack_ci_weight * main_row(MainColumn::CI); let running_product_for_jump_stack_table_is_initialized_correctly = - aux_row(JumpStackTablePermArg) + aux_row(AuxColumn::JumpStackTablePermArg) - x_constant(PermArg::default_initial()) * (jump_stack_indeterminate - compressed_row_for_jump_stack_table); @@ -270,36 +172,38 @@ impl AIR for ProcessorTable { // collapses to challenge(ClockJumpDifferenceLookupIndeterminate) // because main_row(CLK) = 0 is already a constraint. let clock_jump_diff_lookup_log_derivative_is_initialized_correctly = - aux_row(ClockJumpDifferenceLookupServerLogDerivative) - * challenge(ClockJumpDifferenceLookupIndeterminate) - - main_row(ClockJumpDifferenceLookupMultiplicity); + aux_row(AuxColumn::ClockJumpDifferenceLookupServerLogDerivative) + * challenge(ChallengeId::ClockJumpDifferenceLookupIndeterminate) + - main_row(MainColumn::ClockJumpDifferenceLookupMultiplicity); // from processor to hash table - let hash_selector = main_row(CI) - constant(Instruction::Hash.opcode()); + let hash_selector = main_row(MainColumn::CI) - constant(Instruction::Hash.opcode()); let hash_deselector = instruction_deselector_single_row(circuit_builder, Instruction::Hash); - let hash_input_indeterminate = challenge(HashInputIndeterminate); + let hash_input_indeterminate = challenge(ChallengeId::HashInputIndeterminate); // the opStack is guaranteed to be initialized to 0 by virtue of other initial constraints let compressed_row = constant(0); - let running_evaluation_hash_input_has_absorbed_first_row = aux_row(HashInputEvalArg) - - hash_input_indeterminate * x_constant(EvalArg::default_initial()) - - compressed_row; + let running_evaluation_hash_input_has_absorbed_first_row = + aux_row(AuxColumn::HashInputEvalArg) + - hash_input_indeterminate * x_constant(EvalArg::default_initial()) + - compressed_row; let running_evaluation_hash_input_is_default_initial = - aux_row(HashInputEvalArg) - x_constant(EvalArg::default_initial()); + aux_row(AuxColumn::HashInputEvalArg) - x_constant(EvalArg::default_initial()); let running_evaluation_hash_input_is_initialized_correctly = hash_selector * running_evaluation_hash_input_is_default_initial + hash_deselector * running_evaluation_hash_input_has_absorbed_first_row; // from hash table to processor let running_evaluation_hash_digest_is_initialized_correctly = - aux_row(HashDigestEvalArg) - x_constant(EvalArg::default_initial()); + aux_row(AuxColumn::HashDigestEvalArg) - x_constant(EvalArg::default_initial()); // Hash Table – Sponge let running_evaluation_sponge_absorb_is_initialized_correctly = - aux_row(SpongeEvalArg) - x_constant(EvalArg::default_initial()); + aux_row(AuxColumn::SpongeEvalArg) - x_constant(EvalArg::default_initial()); // u32 table let running_sum_log_derivative_for_u32_table_is_initialized_correctly = - aux_row(U32LookupClientLogDerivative) - x_constant(LookupArg::default_initial()); + aux_row(AuxColumn::U32LookupClientLogDerivative) + - x_constant(LookupArg::default_initial()); vec![ clk_is_0, @@ -338,35 +242,36 @@ impl AIR for ProcessorTable { circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); - let main_row = - |col: ProcessorMainColumn| circuit_builder.input(Main(col.master_main_index())); + let main_row = |col: MainColumn| circuit_builder.input(Main(col.master_main_index())); // The composition of instruction bits ib0-ib7 corresponds the current instruction ci. - let ib_composition = main_row(IB0) - + constant(1 << 1) * main_row(IB1) - + constant(1 << 2) * main_row(IB2) - + constant(1 << 3) * main_row(IB3) - + constant(1 << 4) * main_row(IB4) - + constant(1 << 5) * main_row(IB5) - + constant(1 << 6) * main_row(IB6); - let ci_corresponds_to_ib0_thru_ib7 = main_row(CI) - ib_composition; - - let ib0_is_bit = main_row(IB0) * (main_row(IB0) - constant(1)); - let ib1_is_bit = main_row(IB1) * (main_row(IB1) - constant(1)); - let ib2_is_bit = main_row(IB2) * (main_row(IB2) - constant(1)); - let ib3_is_bit = main_row(IB3) * (main_row(IB3) - constant(1)); - let ib4_is_bit = main_row(IB4) * (main_row(IB4) - constant(1)); - let ib5_is_bit = main_row(IB5) * (main_row(IB5) - constant(1)); - let ib6_is_bit = main_row(IB6) * (main_row(IB6) - constant(1)); - let is_padding_is_bit = main_row(IsPadding) * (main_row(IsPadding) - constant(1)); + let ib_composition = main_row(MainColumn::IB0) + + constant(1 << 1) * main_row(MainColumn::IB1) + + constant(1 << 2) * main_row(MainColumn::IB2) + + constant(1 << 3) * main_row(MainColumn::IB3) + + constant(1 << 4) * main_row(MainColumn::IB4) + + constant(1 << 5) * main_row(MainColumn::IB5) + + constant(1 << 6) * main_row(MainColumn::IB6); + let ci_corresponds_to_ib0_thru_ib7 = main_row(MainColumn::CI) - ib_composition; + + let ib0_is_bit = main_row(MainColumn::IB0) * (main_row(MainColumn::IB0) - constant(1)); + let ib1_is_bit = main_row(MainColumn::IB1) * (main_row(MainColumn::IB1) - constant(1)); + let ib2_is_bit = main_row(MainColumn::IB2) * (main_row(MainColumn::IB2) - constant(1)); + let ib3_is_bit = main_row(MainColumn::IB3) * (main_row(MainColumn::IB3) - constant(1)); + let ib4_is_bit = main_row(MainColumn::IB4) * (main_row(MainColumn::IB4) - constant(1)); + let ib5_is_bit = main_row(MainColumn::IB5) * (main_row(MainColumn::IB5) - constant(1)); + let ib6_is_bit = main_row(MainColumn::IB6) * (main_row(MainColumn::IB6) - constant(1)); + let is_padding_is_bit = + main_row(MainColumn::IsPadding) * (main_row(MainColumn::IsPadding) - constant(1)); // In padding rows, the clock jump difference lookup multiplicity is 0. The one row // exempt from this rule is the row wth CLK == 1: since the memory-like tables don't have // an “awareness” of padding rows, they keep looking up clock jump differences of // magnitude 1. - let clock_jump_diff_lookup_multiplicity_is_0_in_padding_rows = main_row(IsPadding) - * (main_row(CLK) - constant(1)) - * main_row(ClockJumpDifferenceLookupMultiplicity); + let clock_jump_diff_lookup_multiplicity_is_0_in_padding_rows = + main_row(MainColumn::IsPadding) + * (main_row(MainColumn::CLK) - constant(1)) + * main_row(MainColumn::ClockJumpDifferenceLookupMultiplicity); vec![ ib0_is_bit, @@ -387,14 +292,15 @@ impl AIR for ProcessorTable { ) -> Vec> { let constant = |c: u64| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); // constraints common to all instructions - let clk_increases_by_1 = next_main_row(CLK) - curr_main_row(CLK) - constant(1); - let is_padding_is_0_or_does_not_change = - curr_main_row(IsPadding) * (next_main_row(IsPadding) - curr_main_row(IsPadding)); + let clk_increases_by_1 = + next_main_row(MainColumn::CLK) - curr_main_row(MainColumn::CLK) - constant(1); + let is_padding_is_0_or_does_not_change = curr_main_row(MainColumn::IsPadding) + * (next_main_row(MainColumn::IsPadding) - curr_main_row(MainColumn::IsPadding)); let instruction_independent_constraints = vec![clk_increases_by_1, is_padding_is_0_or_does_not_change]; @@ -510,15 +416,14 @@ fn combine_transition_constraints_with_padding_constraints( ) -> Vec> { let constant = |c: u64| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let padding_row_transition_constraints = [ vec![ - next_main_row(IP) - curr_main_row(IP), - next_main_row(CI) - curr_main_row(CI), - next_main_row(NIA) - curr_main_row(NIA), + next_main_row(MainColumn::IP) - curr_main_row(MainColumn::IP), + next_main_row(MainColumn::CI) - curr_main_row(MainColumn::CI), + next_main_row(MainColumn::NIA) - curr_main_row(MainColumn::NIA), ], instruction_group_keep_jump_stack(circuit_builder), instruction_group_keep_op_stack(circuit_builder), @@ -527,8 +432,8 @@ fn combine_transition_constraints_with_padding_constraints( ] .concat(); - let padding_row_deselector = constant(1) - next_main_row(IsPadding); - let padding_row_selector = next_main_row(IsPadding); + let padding_row_deselector = constant(1) - next_main_row(MainColumn::IsPadding); + let padding_row_selector = next_main_row(MainColumn::IsPadding); let max_number_of_constraints = max( instruction_transition_constraints.len(), @@ -557,18 +462,22 @@ fn instruction_group_decompose_arg( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - - let hv0_is_a_bit = curr_main_row(HV0) * (curr_main_row(HV0) - constant(1)); - let hv1_is_a_bit = curr_main_row(HV1) * (curr_main_row(HV1) - constant(1)); - let hv2_is_a_bit = curr_main_row(HV2) * (curr_main_row(HV2) - constant(1)); - let hv3_is_a_bit = curr_main_row(HV3) * (curr_main_row(HV3) - constant(1)); - - let helper_variables_are_binary_decomposition_of_nia = curr_main_row(NIA) - - constant(8) * curr_main_row(HV3) - - constant(4) * curr_main_row(HV2) - - constant(2) * curr_main_row(HV1) - - curr_main_row(HV0); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + + let hv0_is_a_bit = + curr_main_row(MainColumn::HV0) * (curr_main_row(MainColumn::HV0) - constant(1)); + let hv1_is_a_bit = + curr_main_row(MainColumn::HV1) * (curr_main_row(MainColumn::HV1) - constant(1)); + let hv2_is_a_bit = + curr_main_row(MainColumn::HV2) * (curr_main_row(MainColumn::HV2) - constant(1)); + let hv3_is_a_bit = + curr_main_row(MainColumn::HV3) * (curr_main_row(MainColumn::HV3) - constant(1)); + + let helper_variables_are_binary_decomposition_of_nia = curr_main_row(MainColumn::NIA) + - constant(8) * curr_main_row(MainColumn::HV3) + - constant(4) * curr_main_row(MainColumn::HV2) + - constant(2) * curr_main_row(MainColumn::HV1) + - curr_main_row(MainColumn::HV0); vec![ hv0_is_a_bit, @@ -584,12 +493,10 @@ fn instruction_group_decompose_arg( fn instruction_group_no_ram( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); - vec![next_aux_row(RamTablePermArg) - curr_aux_row(RamTablePermArg)] + vec![next_aux_row(AuxColumn::RamTablePermArg) - curr_aux_row(AuxColumn::RamTablePermArg)] } fn instruction_group_no_io( @@ -609,10 +516,8 @@ fn instruction_group_op_stack_remains_except_top_n( ) -> Vec> { assert!(n <= NUM_OP_STACK_REGISTERS); - let curr_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_row = |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let stack = (0..OpStackElement::COUNT) .map(ProcessorTable::op_stack_column_by_index) @@ -653,14 +558,16 @@ fn instruction_group_keep_op_stack_height( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let op_stack_pointer_curr = - circuit_builder.input(CurrentMain(OpStackPointer.master_main_index())); - let op_stack_pointer_next = circuit_builder.input(NextMain(OpStackPointer.master_main_index())); + circuit_builder.input(CurrentMain(MainColumn::OpStackPointer.master_main_index())); + let op_stack_pointer_next = + circuit_builder.input(NextMain(MainColumn::OpStackPointer.master_main_index())); let osp_remains_unchanged = op_stack_pointer_next - op_stack_pointer_curr; - let op_stack_table_perm_arg_curr = - circuit_builder.input(CurrentAux(OpStackTablePermArg.master_aux_index())); + let op_stack_table_perm_arg_curr = circuit_builder.input(CurrentAux( + AuxColumn::OpStackTablePermArg.master_aux_index(), + )); let op_stack_table_perm_arg_next = - circuit_builder.input(NextAux(OpStackTablePermArg.master_aux_index())); + circuit_builder.input(NextAux(AuxColumn::OpStackTablePermArg.master_aux_index())); let perm_arg_remains_unchanged = op_stack_table_perm_arg_next - op_stack_table_perm_arg_curr; vec![osp_remains_unchanged, perm_arg_remains_unchanged] @@ -671,26 +578,27 @@ fn instruction_group_grow_op_stack_and_top_two_elements_unconstrained( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); vec![ - next_main_row(ST2) - curr_main_row(ST1), - next_main_row(ST3) - curr_main_row(ST2), - next_main_row(ST4) - curr_main_row(ST3), - next_main_row(ST5) - curr_main_row(ST4), - next_main_row(ST6) - curr_main_row(ST5), - next_main_row(ST7) - curr_main_row(ST6), - next_main_row(ST8) - curr_main_row(ST7), - next_main_row(ST9) - curr_main_row(ST8), - next_main_row(ST10) - curr_main_row(ST9), - next_main_row(ST11) - curr_main_row(ST10), - next_main_row(ST12) - curr_main_row(ST11), - next_main_row(ST13) - curr_main_row(ST12), - next_main_row(ST14) - curr_main_row(ST13), - next_main_row(ST15) - curr_main_row(ST14), - next_main_row(OpStackPointer) - curr_main_row(OpStackPointer) - constant(1), + next_main_row(MainColumn::ST2) - curr_main_row(MainColumn::ST1), + next_main_row(MainColumn::ST3) - curr_main_row(MainColumn::ST2), + next_main_row(MainColumn::ST4) - curr_main_row(MainColumn::ST3), + next_main_row(MainColumn::ST5) - curr_main_row(MainColumn::ST4), + next_main_row(MainColumn::ST6) - curr_main_row(MainColumn::ST5), + next_main_row(MainColumn::ST7) - curr_main_row(MainColumn::ST6), + next_main_row(MainColumn::ST8) - curr_main_row(MainColumn::ST7), + next_main_row(MainColumn::ST9) - curr_main_row(MainColumn::ST8), + next_main_row(MainColumn::ST10) - curr_main_row(MainColumn::ST9), + next_main_row(MainColumn::ST11) - curr_main_row(MainColumn::ST10), + next_main_row(MainColumn::ST12) - curr_main_row(MainColumn::ST11), + next_main_row(MainColumn::ST13) - curr_main_row(MainColumn::ST12), + next_main_row(MainColumn::ST14) - curr_main_row(MainColumn::ST13), + next_main_row(MainColumn::ST15) - curr_main_row(MainColumn::ST14), + next_main_row(MainColumn::OpStackPointer) + - curr_main_row(MainColumn::OpStackPointer) + - constant(1), running_product_op_stack_accounts_for_growing_stack_by(circuit_builder, 1), ] } @@ -699,11 +607,11 @@ fn instruction_group_grow_op_stack( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let specific_constraints = vec![next_main_row(ST1) - curr_main_row(ST0)]; + let specific_constraints = + vec![next_main_row(MainColumn::ST1) - curr_main_row(MainColumn::ST0)]; let inherited_constraints = instruction_group_grow_op_stack_and_top_two_elements_unconstrained(circuit_builder); @@ -715,24 +623,24 @@ fn instruction_group_op_stack_shrinks_and_top_three_elements_unconstrained( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); vec![ - next_main_row(ST3) - curr_main_row(ST4), - next_main_row(ST4) - curr_main_row(ST5), - next_main_row(ST5) - curr_main_row(ST6), - next_main_row(ST6) - curr_main_row(ST7), - next_main_row(ST7) - curr_main_row(ST8), - next_main_row(ST8) - curr_main_row(ST9), - next_main_row(ST9) - curr_main_row(ST10), - next_main_row(ST10) - curr_main_row(ST11), - next_main_row(ST11) - curr_main_row(ST12), - next_main_row(ST12) - curr_main_row(ST13), - next_main_row(ST13) - curr_main_row(ST14), - next_main_row(ST14) - curr_main_row(ST15), - next_main_row(OpStackPointer) - curr_main_row(OpStackPointer) + constant(1), + next_main_row(MainColumn::ST3) - curr_main_row(MainColumn::ST4), + next_main_row(MainColumn::ST4) - curr_main_row(MainColumn::ST5), + next_main_row(MainColumn::ST5) - curr_main_row(MainColumn::ST6), + next_main_row(MainColumn::ST6) - curr_main_row(MainColumn::ST7), + next_main_row(MainColumn::ST7) - curr_main_row(MainColumn::ST8), + next_main_row(MainColumn::ST8) - curr_main_row(MainColumn::ST9), + next_main_row(MainColumn::ST9) - curr_main_row(MainColumn::ST10), + next_main_row(MainColumn::ST10) - curr_main_row(MainColumn::ST11), + next_main_row(MainColumn::ST11) - curr_main_row(MainColumn::ST12), + next_main_row(MainColumn::ST12) - curr_main_row(MainColumn::ST13), + next_main_row(MainColumn::ST13) - curr_main_row(MainColumn::ST14), + next_main_row(MainColumn::ST14) - curr_main_row(MainColumn::ST15), + next_main_row(MainColumn::OpStackPointer) - curr_main_row(MainColumn::OpStackPointer) + + constant(1), running_product_op_stack_accounts_for_shrinking_stack_by(circuit_builder, 1), ] } @@ -741,13 +649,12 @@ fn instruction_group_binop( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let specific_constraints = vec![ - next_main_row(ST1) - curr_main_row(ST2), - next_main_row(ST2) - curr_main_row(ST3), + next_main_row(MainColumn::ST1) - curr_main_row(MainColumn::ST2), + next_main_row(MainColumn::ST2) - curr_main_row(MainColumn::ST3), ]; let inherited_constraints = instruction_group_op_stack_shrinks_and_top_three_elements_unconstrained(circuit_builder); @@ -759,11 +666,11 @@ fn instruction_group_shrink_op_stack( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let specific_constraints = vec![next_main_row(ST0) - curr_main_row(ST1)]; + let specific_constraints = + vec![next_main_row(MainColumn::ST0) - curr_main_row(MainColumn::ST1)]; let inherited_constraints = instruction_group_binop(circuit_builder); [specific_constraints, inherited_constraints].concat() @@ -773,13 +680,12 @@ fn instruction_group_keep_jump_stack( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let jsp_does_not_change = next_main_row(JSP) - curr_main_row(JSP); - let jso_does_not_change = next_main_row(JSO) - curr_main_row(JSO); - let jsd_does_not_change = next_main_row(JSD) - curr_main_row(JSD); + let jsp_does_not_change = next_main_row(MainColumn::JSP) - curr_main_row(MainColumn::JSP); + let jso_does_not_change = next_main_row(MainColumn::JSO) - curr_main_row(MainColumn::JSO); + let jsd_does_not_change = next_main_row(MainColumn::JSD) - curr_main_row(MainColumn::JSD); vec![ jsp_does_not_change, @@ -794,11 +700,11 @@ fn instruction_group_step_1( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let instruction_pointer_increases_by_one = next_main_row(IP) - curr_main_row(IP) - constant(1); + let instruction_pointer_increases_by_one = + next_main_row(MainColumn::IP) - curr_main_row(MainColumn::IP) - constant(1); [ instruction_group_keep_jump_stack(circuit_builder), vec![instruction_pointer_increases_by_one], @@ -812,11 +718,11 @@ fn instruction_group_step_2( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let instruction_pointer_increases_by_two = next_main_row(IP) - curr_main_row(IP) - constant(2); + let instruction_pointer_increases_by_two = + next_main_row(MainColumn::IP) - curr_main_row(MainColumn::IP) - constant(2); [ instruction_group_keep_jump_stack(circuit_builder), vec![instruction_pointer_increases_by_two], @@ -858,16 +764,16 @@ fn instruction_deselector_current_row( instruction: Instruction, ) -> ConstraintCircuitMonad { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); let instruction_bit_polynomials = [ - curr_main_row(IB0), - curr_main_row(IB1), - curr_main_row(IB2), - curr_main_row(IB3), - curr_main_row(IB4), - curr_main_row(IB5), - curr_main_row(IB6), + curr_main_row(MainColumn::IB0), + curr_main_row(MainColumn::IB1), + curr_main_row(MainColumn::IB2), + curr_main_row(MainColumn::IB3), + curr_main_row(MainColumn::IB4), + curr_main_row(MainColumn::IB5), + curr_main_row(MainColumn::IB6), ]; instruction_deselector_common_functionality( @@ -883,17 +789,16 @@ fn instruction_deselector_next_row( circuit_builder: &ConstraintCircuitBuilder, instruction: Instruction, ) -> ConstraintCircuitMonad { - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let instruction_bit_polynomials = [ - next_main_row(IB0), - next_main_row(IB1), - next_main_row(IB2), - next_main_row(IB3), - next_main_row(IB4), - next_main_row(IB5), - next_main_row(IB6), + next_main_row(MainColumn::IB0), + next_main_row(MainColumn::IB1), + next_main_row(MainColumn::IB2), + next_main_row(MainColumn::IB3), + next_main_row(MainColumn::IB4), + next_main_row(MainColumn::IB5), + next_main_row(MainColumn::IB6), ]; instruction_deselector_common_functionality( @@ -909,16 +814,16 @@ fn instruction_deselector_single_row( circuit_builder: &ConstraintCircuitBuilder, instruction: Instruction, ) -> ConstraintCircuitMonad { - let main_row = |col: ProcessorMainColumn| circuit_builder.input(Main(col.master_main_index())); + let main_row = |col: MainColumn| circuit_builder.input(Main(col.master_main_index())); let instruction_bit_polynomials = [ - main_row(IB0), - main_row(IB1), - main_row(IB2), - main_row(IB3), - main_row(IB4), - main_row(IB5), - main_row(IB6), + main_row(MainColumn::IB0), + main_row(MainColumn::IB1), + main_row(MainColumn::IB2), + main_row(MainColumn::IB3), + main_row(MainColumn::IB4), + main_row(MainColumn::IB5), + main_row(MainColumn::IB6), ]; instruction_deselector_common_functionality( @@ -946,11 +851,11 @@ fn instruction_push( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let specific_constraints = vec![next_main_row(ST0) - curr_main_row(NIA)]; + let specific_constraints = + vec![next_main_row(MainColumn::ST0) - curr_main_row(MainColumn::NIA)]; [ specific_constraints, instruction_group_grow_op_stack(circuit_builder), @@ -979,13 +884,12 @@ fn instruction_dup( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let indicator_poly = |idx| indicator_polynomial(circuit_builder, idx); - let curr_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_row = |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let st_column = ProcessorTable::op_stack_column_by_index; - let duplicate_element = |i| indicator_poly(i) * (next_row(ST0) - curr_row(st_column(i))); + let duplicate_element = + |i| indicator_poly(i) * (next_row(MainColumn::ST0) - curr_row(st_column(i))); let duplicate_indicated_element = (0..OpStackElement::COUNT).map(duplicate_element).sum(); [ @@ -1002,10 +906,8 @@ fn instruction_dup( fn instruction_swap( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { - let curr_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_row = |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let stack = (0..OpStackElement::COUNT) .map(ProcessorTable::op_stack_column_by_index) @@ -1062,21 +964,22 @@ fn instruction_skiz( let constant = |c: u32| circuit_builder.b_constant(c); let one = || constant(1); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let hv0_is_inverse_of_st0 = curr_main_row(HV0) * curr_main_row(ST0) - one(); - let hv0_is_inverse_of_st0_or_hv0_is_0 = hv0_is_inverse_of_st0.clone() * curr_main_row(HV0); - let hv0_is_inverse_of_st0_or_st0_is_0 = hv0_is_inverse_of_st0 * curr_main_row(ST0); + let hv0_is_inverse_of_st0 = + curr_main_row(MainColumn::HV0) * curr_main_row(MainColumn::ST0) - one(); + let hv0_is_inverse_of_st0_or_hv0_is_0 = + hv0_is_inverse_of_st0.clone() * curr_main_row(MainColumn::HV0); + let hv0_is_inverse_of_st0_or_st0_is_0 = hv0_is_inverse_of_st0 * curr_main_row(MainColumn::ST0); // The next instruction nia is decomposed into helper variables hv. - let nia_decomposes_to_hvs = curr_main_row(NIA) - - curr_main_row(HV1) - - constant(1 << 1) * curr_main_row(HV2) - - constant(1 << 3) * curr_main_row(HV3) - - constant(1 << 5) * curr_main_row(HV4) - - constant(1 << 7) * curr_main_row(HV5); + let nia_decomposes_to_hvs = curr_main_row(MainColumn::NIA) + - curr_main_row(MainColumn::HV1) + - constant(1 << 1) * curr_main_row(MainColumn::HV2) + - constant(1 << 3) * curr_main_row(MainColumn::HV3) + - constant(1 << 5) * curr_main_row(MainColumn::HV4) + - constant(1 << 7) * curr_main_row(MainColumn::HV5); // If `st0` is non-zero, register `ip` is incremented by 1. // If `st0` is 0 and `nia` takes no argument, register `ip` is incremented by 2. @@ -1088,13 +991,14 @@ fn instruction_skiz( // (Register `st0` is 0 or `ip` is incremented by 1), and // (`st0` has a multiplicative inverse or `hv1` is 1 or `ip` is incremented by 2), and // (`st0` has a multiplicative inverse or `hv1` is 0 or `ip` is incremented by 3). - let ip_case_1 = (next_main_row(IP) - curr_main_row(IP) - constant(1)) * curr_main_row(ST0); - let ip_case_2 = (next_main_row(IP) - curr_main_row(IP) - constant(2)) - * (curr_main_row(ST0) * curr_main_row(HV0) - one()) - * (curr_main_row(HV1) - one()); - let ip_case_3 = (next_main_row(IP) - curr_main_row(IP) - constant(3)) - * (curr_main_row(ST0) * curr_main_row(HV0) - one()) - * curr_main_row(HV1); + let ip_case_1 = (next_main_row(MainColumn::IP) - curr_main_row(MainColumn::IP) - constant(1)) + * curr_main_row(MainColumn::ST0); + let ip_case_2 = (next_main_row(MainColumn::IP) - curr_main_row(MainColumn::IP) - constant(2)) + * (curr_main_row(MainColumn::ST0) * curr_main_row(MainColumn::HV0) - one()) + * (curr_main_row(MainColumn::HV1) - one()); + let ip_case_3 = (next_main_row(MainColumn::IP) - curr_main_row(MainColumn::IP) - constant(3)) + * (curr_main_row(MainColumn::ST0) * curr_main_row(MainColumn::HV0) - one()) + * curr_main_row(MainColumn::HV1); let ip_incr_by_1_or_2_or_3 = ip_case_1 + ip_case_2 + ip_case_3; let specific_constraints = vec![ @@ -1119,11 +1023,10 @@ fn next_instruction_range_check_constraints_for_instruction_skiz( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let is_0_or_1 = - |var: ProcessorMainColumn| curr_main_row(var) * (curr_main_row(var) - constant(1)); - let is_0_or_1_or_2_or_3 = |var: ProcessorMainColumn| { + let is_0_or_1 = |var: MainColumn| curr_main_row(var) * (curr_main_row(var) - constant(1)); + let is_0_or_1_or_2_or_3 = |var: MainColumn| { curr_main_row(var) * (curr_main_row(var) - constant(1)) * (curr_main_row(var) - constant(2)) @@ -1131,11 +1034,11 @@ fn next_instruction_range_check_constraints_for_instruction_skiz( }; vec![ - is_0_or_1(HV1), - is_0_or_1_or_2_or_3(HV2), - is_0_or_1_or_2_or_3(HV3), - is_0_or_1_or_2_or_3(HV4), - is_0_or_1_or_2_or_3(HV5), + is_0_or_1(MainColumn::HV1), + is_0_or_1_or_2_or_3(MainColumn::HV2), + is_0_or_1_or_2_or_3(MainColumn::HV3), + is_0_or_1_or_2_or_3(MainColumn::HV4), + is_0_or_1_or_2_or_3(MainColumn::HV5), ] } @@ -1144,21 +1047,21 @@ fn instruction_call( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); // The jump stack pointer jsp is incremented by 1. - let jsp_incr_1 = next_main_row(JSP) - curr_main_row(JSP) - constant(1); + let jsp_incr_1 = next_main_row(MainColumn::JSP) - curr_main_row(MainColumn::JSP) - constant(1); // The jump's origin jso is set to the current instruction pointer ip plus 2. - let jso_becomes_ip_plus_2 = next_main_row(JSO) - curr_main_row(IP) - constant(2); + let jso_becomes_ip_plus_2 = + next_main_row(MainColumn::JSO) - curr_main_row(MainColumn::IP) - constant(2); // The jump's destination jsd is set to the instruction's argument. - let jsd_becomes_nia = next_main_row(JSD) - curr_main_row(NIA); + let jsd_becomes_nia = next_main_row(MainColumn::JSD) - curr_main_row(MainColumn::NIA); // The instruction pointer ip is set to the instruction's argument. - let ip_becomes_nia = next_main_row(IP) - curr_main_row(NIA); + let ip_becomes_nia = next_main_row(MainColumn::IP) - curr_main_row(MainColumn::NIA); let specific_constraints = vec![ jsp_incr_1, @@ -1180,12 +1083,12 @@ fn instruction_return( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let jsp_decrements_by_1 = next_main_row(JSP) - curr_main_row(JSP) + constant(1); - let ip_is_set_to_jso = next_main_row(IP) - curr_main_row(JSO); + let jsp_decrements_by_1 = + next_main_row(MainColumn::JSP) - curr_main_row(MainColumn::JSP) + constant(1); + let ip_is_set_to_jso = next_main_row(MainColumn::IP) - curr_main_row(MainColumn::JSO); let specific_constraints = vec![jsp_decrements_by_1, ip_is_set_to_jso]; [ @@ -1201,12 +1104,11 @@ fn instruction_recurse( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); // The instruction pointer ip is set to the last jump's destination jsd. - let ip_becomes_jsd = next_main_row(IP) - curr_main_row(JSD); + let ip_becomes_jsd = next_main_row(MainColumn::IP) - curr_main_row(MainColumn::JSD); let specific_constraints = vec![ip_becomes_jsd]; [ specific_constraints, @@ -1222,28 +1124,27 @@ fn instruction_recurse_or_return( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let one = || circuit_builder.b_constant(1); - let curr_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_row = |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); // Zero if the ST5 equals ST6. One if they are not equal. - let st5_eq_st6 = || curr_row(HV0) * (curr_row(ST6) - curr_row(ST5)); + let st5_eq_st6 = + || curr_row(MainColumn::HV0) * (curr_row(MainColumn::ST6) - curr_row(MainColumn::ST5)); let st5_neq_st6 = || one() - st5_eq_st6(); let maybe_return = vec![ // hv0 is inverse-or-zero of the difference of ST6 and ST5. - st5_neq_st6() * curr_row(HV0), - st5_neq_st6() * (curr_row(ST6) - curr_row(ST5)), - st5_neq_st6() * (next_row(IP) - curr_row(JSO)), - st5_neq_st6() * (next_row(JSP) - curr_row(JSP) + one()), + st5_neq_st6() * curr_row(MainColumn::HV0), + st5_neq_st6() * (curr_row(MainColumn::ST6) - curr_row(MainColumn::ST5)), + st5_neq_st6() * (next_row(MainColumn::IP) - curr_row(MainColumn::JSO)), + st5_neq_st6() * (next_row(MainColumn::JSP) - curr_row(MainColumn::JSP) + one()), ]; let maybe_recurse = vec![ // constraints are ordered to line up nicely with group “maybe_return” - st5_eq_st6() * (next_row(JSO) - curr_row(JSO)), - st5_eq_st6() * (next_row(JSD) - curr_row(JSD)), - st5_eq_st6() * (next_row(IP) - curr_row(JSD)), - st5_eq_st6() * (next_row(JSP) - curr_row(JSP)), + st5_eq_st6() * (next_row(MainColumn::JSO) - curr_row(MainColumn::JSO)), + st5_eq_st6() * (next_row(MainColumn::JSD) - curr_row(MainColumn::JSD)), + st5_eq_st6() * (next_row(MainColumn::IP) - curr_row(MainColumn::JSD)), + st5_eq_st6() * (next_row(MainColumn::JSP) - curr_row(MainColumn::JSP)), ]; // The two constraint groups are mutually exclusive: the stack element is either @@ -1268,10 +1169,10 @@ fn instruction_assert( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); // The current top of the stack st0 is 1. - let st_0_is_1 = curr_main_row(ST0) - constant(1); + let st_0_is_1 = curr_main_row(MainColumn::ST0) - constant(1); let specific_constraints = vec![st_0_is_1]; [ @@ -1288,12 +1189,11 @@ fn instruction_halt( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); // The instruction executed in the following step is instruction halt. - let halt_is_followed_by_halt = next_main_row(CI) - curr_main_row(CI); + let halt_is_followed_by_halt = next_main_row(MainColumn::CI) - curr_main_row(MainColumn::CI); let specific_constraints = vec![halt_is_followed_by_halt]; [ @@ -1338,18 +1238,18 @@ fn instruction_hash( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let op_stack_shrinks_by_5_and_top_5_unconstrained = vec![ - next_main_row(ST5) - curr_main_row(ST10), - next_main_row(ST6) - curr_main_row(ST11), - next_main_row(ST7) - curr_main_row(ST12), - next_main_row(ST8) - curr_main_row(ST13), - next_main_row(ST9) - curr_main_row(ST14), - next_main_row(ST10) - curr_main_row(ST15), - next_main_row(OpStackPointer) - curr_main_row(OpStackPointer) + constant(5), + next_main_row(MainColumn::ST5) - curr_main_row(MainColumn::ST10), + next_main_row(MainColumn::ST6) - curr_main_row(MainColumn::ST11), + next_main_row(MainColumn::ST7) - curr_main_row(MainColumn::ST12), + next_main_row(MainColumn::ST8) - curr_main_row(MainColumn::ST13), + next_main_row(MainColumn::ST9) - curr_main_row(MainColumn::ST14), + next_main_row(MainColumn::ST10) - curr_main_row(MainColumn::ST15), + next_main_row(MainColumn::OpStackPointer) - curr_main_row(MainColumn::OpStackPointer) + + constant(5), running_product_op_stack_accounts_for_shrinking_stack_by(circuit_builder, 5), ]; @@ -1378,17 +1278,23 @@ fn instruction_merkle_step_mem( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let stack_weight = |i| circuit_builder.challenge(stack_weight_by_index(i)); - let curr = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next = |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - - let ram_pointers = [0, 1, 2, 3, 4].map(|i| curr(ST7) + constant(i)); - let ram_read_destinations = [HV0, HV1, HV2, HV3, HV4].map(curr); + let curr = |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + + let ram_pointers = [0, 1, 2, 3, 4].map(|i| curr(MainColumn::ST7) + constant(i)); + let ram_read_destinations = [ + MainColumn::HV0, + MainColumn::HV1, + MainColumn::HV2, + MainColumn::HV3, + MainColumn::HV4, + ] + .map(curr); let read_from_ram_to_hvs = read_from_ram_to(circuit_builder, ram_pointers, ram_read_destinations); - let st6_does_not_change = next(ST6) - curr(ST6); - let st7_increments_by_5 = next(ST7) - curr(ST7) - constant(5); + let st6_does_not_change = next(MainColumn::ST6) - curr(MainColumn::ST6); + let st7_increments_by_5 = next(MainColumn::ST7) - curr(MainColumn::ST7) - constant(5); let st6_and_st7_update_correctly = stack_weight(6) * st6_does_not_change + stack_weight(7) * st7_increments_by_5; @@ -1410,12 +1316,12 @@ fn instruction_merkle_step_shared_constraints( ) -> Vec> { let constant = |c: u32| circuit_builder.b_constant(c); let one = || constant(1); - let curr = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next = |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr = |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let hv5_is_0_or_1 = curr(HV5) * (curr(HV5) - one()); - let new_st5_is_previous_st5_div_2 = constant(2) * next(ST5) + curr(HV5) - curr(ST5); + let hv5_is_0_or_1 = curr(MainColumn::HV5) * (curr(MainColumn::HV5) - one()); + let new_st5_is_previous_st5_div_2 = + constant(2) * next(MainColumn::ST5) + curr(MainColumn::HV5) - curr(MainColumn::ST5); let update_merkle_tree_node_index = vec![hv5_is_0_or_1, new_st5_is_previous_st5_div_2]; [ @@ -1430,14 +1336,14 @@ fn instruction_assert_vector( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); let specific_constraints = vec![ - curr_main_row(ST5) - curr_main_row(ST0), - curr_main_row(ST6) - curr_main_row(ST1), - curr_main_row(ST7) - curr_main_row(ST2), - curr_main_row(ST8) - curr_main_row(ST3), - curr_main_row(ST9) - curr_main_row(ST4), + curr_main_row(MainColumn::ST5) - curr_main_row(MainColumn::ST0), + curr_main_row(MainColumn::ST6) - curr_main_row(MainColumn::ST1), + curr_main_row(MainColumn::ST7) - curr_main_row(MainColumn::ST2), + curr_main_row(MainColumn::ST8) - curr_main_row(MainColumn::ST3), + curr_main_row(MainColumn::ST9) - curr_main_row(MainColumn::ST4), ]; [ specific_constraints, @@ -1477,13 +1383,13 @@ fn instruction_sponge_absorb_mem( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let constant = |c| circuit_builder.b_constant(c); - let increment_ram_pointer = - next_main_row(ST0) - curr_main_row(ST0) - constant(tip5::RATE as u32); + let increment_ram_pointer = next_main_row(MainColumn::ST0) + - curr_main_row(MainColumn::ST0) + - constant(tip5::RATE as u32); [ vec![increment_ram_pointer], @@ -1510,11 +1416,14 @@ fn instruction_add( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let specific_constraints = vec![next_main_row(ST0) - curr_main_row(ST0) - curr_main_row(ST1)]; + let specific_constraints = vec![ + next_main_row(MainColumn::ST0) + - curr_main_row(MainColumn::ST0) + - curr_main_row(MainColumn::ST1), + ]; [ specific_constraints, instruction_group_step_1(circuit_builder), @@ -1529,11 +1438,14 @@ fn instruction_addi( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let specific_constraints = vec![next_main_row(ST0) - curr_main_row(ST0) - curr_main_row(NIA)]; + let specific_constraints = vec![ + next_main_row(MainColumn::ST0) + - curr_main_row(MainColumn::ST0) + - curr_main_row(MainColumn::NIA), + ]; [ specific_constraints, instruction_group_step_2(circuit_builder), @@ -1548,11 +1460,13 @@ fn instruction_mul( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let specific_constraints = vec![next_main_row(ST0) - curr_main_row(ST0) * curr_main_row(ST1)]; + let specific_constraints = vec![ + next_main_row(MainColumn::ST0) + - curr_main_row(MainColumn::ST0) * curr_main_row(MainColumn::ST1), + ]; [ specific_constraints, instruction_group_step_1(circuit_builder), @@ -1569,11 +1483,11 @@ fn instruction_invert( let constant = |c: u32| circuit_builder.b_constant(c); let one = || constant(1); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let specific_constraints = vec![next_main_row(ST0) * curr_main_row(ST0) - one()]; + let specific_constraints = + vec![next_main_row(MainColumn::ST0) * curr_main_row(MainColumn::ST0) - one()]; [ specific_constraints, instruction_group_step_1(circuit_builder), @@ -1590,24 +1504,27 @@ fn instruction_eq( let constant = |c: u32| circuit_builder.b_constant(c); let one = || constant(1); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let st0_eq_st1 = || one() - curr_main_row(HV0) * (curr_main_row(ST1) - curr_main_row(ST0)); + let st0_eq_st1 = || { + one() + - curr_main_row(MainColumn::HV0) + * (curr_main_row(MainColumn::ST1) - curr_main_row(MainColumn::ST0)) + }; // Helper variable hv0 is the inverse-or-zero of the difference of the stack's two top-most // elements: `hv0·(1 - hv0·(st1 - st0))` - let hv0_is_inverse_of_diff_or_hv0_is_0 = curr_main_row(HV0) * st0_eq_st1(); + let hv0_is_inverse_of_diff_or_hv0_is_0 = curr_main_row(MainColumn::HV0) * st0_eq_st1(); // Helper variable hv0 is the inverse-or-zero of the difference of the stack's two // top-most elements: `(st1 - st0)·(1 - hv0·(st1 - st0))` let hv0_is_inverse_of_diff_or_diff_is_0 = - (curr_main_row(ST1) - curr_main_row(ST0)) * st0_eq_st1(); + (curr_main_row(MainColumn::ST1) - curr_main_row(MainColumn::ST0)) * st0_eq_st1(); // The new top of the stack is 1 if the difference between the stack's two top-most // elements is not invertible, 0 otherwise: `st0' - (1 - hv0·(st1 - st0))` - let st0_becomes_1_if_diff_is_not_invertible = next_main_row(ST0) - st0_eq_st1(); + let st0_becomes_1_if_diff_is_not_invertible = next_main_row(MainColumn::ST0) - st0_eq_st1(); let specific_constraints = vec![ hv0_is_inverse_of_diff_or_hv0_is_0, @@ -1630,14 +1547,13 @@ fn instruction_split( let constant = |c: u64| circuit_builder.b_constant(c); let one = || constant(1); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); // The top of the stack is decomposed as 32-bit chunks into the stack's top-most elements: // st0 - (2^32·st0' + st1') = 0$ - let st0_decomposes_to_two_32_bit_chunks = - curr_main_row(ST0) - (constant(1 << 32) * next_main_row(ST1) + next_main_row(ST0)); + let st0_decomposes_to_two_32_bit_chunks = curr_main_row(MainColumn::ST0) + - (constant(1 << 32) * next_main_row(MainColumn::ST1) + next_main_row(MainColumn::ST0)); // Helper variable `hv0` = 0 if either // 1. `hv0` is the difference between (2^32 - 1) and the high 32 bits (`st0'`), or @@ -1646,9 +1562,9 @@ fn instruction_split( // st1'·(hv0·(st0' - (2^32 - 1)) - 1) // lo·(hv0·(hi - 0xffff_ffff)) - 1) let hv0_holds_inverse_of_chunk_difference_or_low_bits_are_0 = { - let hv0 = curr_main_row(HV0); - let hi = next_main_row(ST1); - let lo = next_main_row(ST0); + let hv0 = curr_main_row(MainColumn::HV0); + let hi = next_main_row(MainColumn::ST1); + let lo = next_main_row(MainColumn::ST0); let ffff_ffff = constant(0xffff_ffff); lo * (hv0 * (hi - ffff_ffff) - one()) @@ -1732,13 +1648,13 @@ fn instruction_div_mod( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); // `n == d·q + r` means `st0 - st1·st1' - st0'` - let numerator_is_quotient_times_denominator_plus_remainder = - curr_main_row(ST0) - curr_main_row(ST1) * next_main_row(ST1) - next_main_row(ST0); + let numerator_is_quotient_times_denominator_plus_remainder = curr_main_row(MainColumn::ST0) + - curr_main_row(MainColumn::ST1) * next_main_row(MainColumn::ST1) + - next_main_row(MainColumn::ST0); let specific_constraints = vec![numerator_is_quotient_times_denominator_plus_remainder]; [ @@ -1767,13 +1683,18 @@ fn instruction_xx_add( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - - let st0_becomes_st0_plus_st3 = next_main_row(ST0) - curr_main_row(ST0) - curr_main_row(ST3); - let st1_becomes_st1_plus_st4 = next_main_row(ST1) - curr_main_row(ST1) - curr_main_row(ST4); - let st2_becomes_st2_plus_st5 = next_main_row(ST2) - curr_main_row(ST2) - curr_main_row(ST5); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + + let st0_becomes_st0_plus_st3 = next_main_row(MainColumn::ST0) + - curr_main_row(MainColumn::ST0) + - curr_main_row(MainColumn::ST3); + let st1_becomes_st1_plus_st4 = next_main_row(MainColumn::ST1) + - curr_main_row(MainColumn::ST1) + - curr_main_row(MainColumn::ST4); + let st2_becomes_st2_plus_st5 = next_main_row(MainColumn::ST2) + - curr_main_row(MainColumn::ST2) + - curr_main_row(MainColumn::ST5); let specific_constraints = vec![ st0_becomes_st0_plus_st3, st1_becomes_st1_plus_st4, @@ -1794,17 +1715,24 @@ fn instruction_xx_mul( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - - let [x0, x1, x2, y0, y1, y2] = [ST0, ST1, ST2, ST3, ST4, ST5].map(curr_main_row); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + + let [x0, x1, x2, y0, y1, y2] = [ + MainColumn::ST0, + MainColumn::ST1, + MainColumn::ST2, + MainColumn::ST3, + MainColumn::ST4, + MainColumn::ST5, + ] + .map(curr_main_row); let [c0, c1, c2] = xx_product([x0, x1, x2], [y0, y1, y2]); let specific_constraints = vec![ - next_main_row(ST0) - c0, - next_main_row(ST1) - c1, - next_main_row(ST2) - c2, + next_main_row(MainColumn::ST0) - c0, + next_main_row(MainColumn::ST1) - c1, + next_main_row(MainColumn::ST2) - c2, ]; [ specific_constraints, @@ -1821,27 +1749,27 @@ fn instruction_xinv( ) -> Vec> { let constant = |c: u64| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - - let first_coefficient_of_product_of_element_and_inverse_is_1 = curr_main_row(ST0) - * next_main_row(ST0) - - curr_main_row(ST2) * next_main_row(ST1) - - curr_main_row(ST1) * next_main_row(ST2) + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + + let first_coefficient_of_product_of_element_and_inverse_is_1 = curr_main_row(MainColumn::ST0) + * next_main_row(MainColumn::ST0) + - curr_main_row(MainColumn::ST2) * next_main_row(MainColumn::ST1) + - curr_main_row(MainColumn::ST1) * next_main_row(MainColumn::ST2) - constant(1); - let second_coefficient_of_product_of_element_and_inverse_is_0 = - curr_main_row(ST1) * next_main_row(ST0) + curr_main_row(ST0) * next_main_row(ST1) - - curr_main_row(ST2) * next_main_row(ST2) - + curr_main_row(ST2) * next_main_row(ST1) - + curr_main_row(ST1) * next_main_row(ST2); + let second_coefficient_of_product_of_element_and_inverse_is_0 = curr_main_row(MainColumn::ST1) + * next_main_row(MainColumn::ST0) + + curr_main_row(MainColumn::ST0) * next_main_row(MainColumn::ST1) + - curr_main_row(MainColumn::ST2) * next_main_row(MainColumn::ST2) + + curr_main_row(MainColumn::ST2) * next_main_row(MainColumn::ST1) + + curr_main_row(MainColumn::ST1) * next_main_row(MainColumn::ST2); - let third_coefficient_of_product_of_element_and_inverse_is_0 = curr_main_row(ST2) - * next_main_row(ST0) - + curr_main_row(ST1) * next_main_row(ST1) - + curr_main_row(ST0) * next_main_row(ST2) - + curr_main_row(ST2) * next_main_row(ST2); + let third_coefficient_of_product_of_element_and_inverse_is_0 = curr_main_row(MainColumn::ST2) + * next_main_row(MainColumn::ST0) + + curr_main_row(MainColumn::ST1) * next_main_row(MainColumn::ST1) + + curr_main_row(MainColumn::ST0) * next_main_row(MainColumn::ST2) + + curr_main_row(MainColumn::ST2) * next_main_row(MainColumn::ST2); let specific_constraints = vec![ first_coefficient_of_product_of_element_and_inverse_is_1, @@ -1862,17 +1790,22 @@ fn instruction_xb_mul( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - - let [x, y0, y1, y2] = [ST0, ST1, ST2, ST3].map(curr_main_row); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + + let [x, y0, y1, y2] = [ + MainColumn::ST0, + MainColumn::ST1, + MainColumn::ST2, + MainColumn::ST3, + ] + .map(curr_main_row); let [c0, c1, c2] = xb_product([y0, y1, y2], x); let specific_constraints = vec![ - next_main_row(ST0) - c0, - next_main_row(ST1) - c1, - next_main_row(ST2) - c2, + next_main_row(MainColumn::ST0) - c0, + next_main_row(MainColumn::ST1) - c1, + next_main_row(MainColumn::ST2) - c2, ]; [ specific_constraints, @@ -1946,29 +1879,28 @@ fn read_from_ram_to( destinations: [ConstraintCircuitMonad; N], ) -> ConstraintCircuitMonad { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); let challenge = |c: ChallengeId| circuit_builder.challenge(c); let constant = |bfe| circuit_builder.b_constant(bfe); let compress_row = |(ram_pointer, destination)| { - curr_main_row(CLK) * challenge(RamClkWeight) - + constant(table::ram::INSTRUCTION_TYPE_READ) * challenge(RamInstructionTypeWeight) - + ram_pointer * challenge(RamPointerWeight) - + destination * challenge(RamValueWeight) + curr_main_row(MainColumn::CLK) * challenge(ChallengeId::RamClkWeight) + + constant(table::ram::INSTRUCTION_TYPE_READ) + * challenge(ChallengeId::RamInstructionTypeWeight) + + ram_pointer * challenge(ChallengeId::RamPointerWeight) + + destination * challenge(ChallengeId::RamValueWeight) }; let factor = ram_pointers .into_iter() .zip(destinations) .map(compress_row) - .map(|compressed_row| challenge(RamIndeterminate) - compressed_row) + .map(|compressed_row| challenge(ChallengeId::RamIndeterminate) - compressed_row) .reduce(|l, r| l * r) .unwrap_or_else(|| constant(bfe!(1))); - curr_aux_row(RamTablePermArg) * factor - next_aux_row(RamTablePermArg) + curr_aux_row(AuxColumn::RamTablePermArg) * factor - next_aux_row(AuxColumn::RamTablePermArg) } fn xx_product( @@ -1997,13 +1929,12 @@ fn xb_product( fn update_dotstep_accumulator( circuit_builder: &ConstraintCircuitBuilder, - accumulator_indices: [ProcessorMainColumn; EXTENSION_DEGREE], + accumulator_indices: [MainColumn; EXTENSION_DEGREE], difference: [ConstraintCircuitMonad; EXTENSION_DEGREE], ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let curr = accumulator_indices.map(curr_main_row); let next = accumulator_indices.map(next_main_row); izip!(curr, next, difference) @@ -2015,22 +1946,31 @@ fn instruction_xx_dot_step( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let constant = |c| circuit_builder.b_constant(c); - let increment_ram_pointer_st0 = next_main_row(ST0) - curr_main_row(ST0) - constant(3); - let increment_ram_pointer_st1 = next_main_row(ST1) - curr_main_row(ST1) - constant(3); + let increment_ram_pointer_st0 = + next_main_row(MainColumn::ST0) - curr_main_row(MainColumn::ST0) - constant(3); + let increment_ram_pointer_st1 = + next_main_row(MainColumn::ST1) - curr_main_row(MainColumn::ST1) - constant(3); - let rhs_ptr0 = curr_main_row(ST0); + let rhs_ptr0 = curr_main_row(MainColumn::ST0); let rhs_ptr1 = rhs_ptr0.clone() + constant(1); let rhs_ptr2 = rhs_ptr0.clone() + constant(2); - let lhs_ptr0 = curr_main_row(ST1); + let lhs_ptr0 = curr_main_row(MainColumn::ST1); let lhs_ptr1 = lhs_ptr0.clone() + constant(1); let lhs_ptr2 = lhs_ptr0.clone() + constant(2); let ram_read_sources = [rhs_ptr0, rhs_ptr1, rhs_ptr2, lhs_ptr0, lhs_ptr1, lhs_ptr2]; - let ram_read_destinations = [HV0, HV1, HV2, HV3, HV4, HV5].map(curr_main_row); + let ram_read_destinations = [ + MainColumn::HV0, + MainColumn::HV1, + MainColumn::HV2, + MainColumn::HV3, + MainColumn::HV4, + MainColumn::HV5, + ] + .map(curr_main_row); let read_two_xfes_from_ram = read_from_ram_to(circuit_builder, ram_read_sources, ram_read_destinations); @@ -2040,12 +1980,24 @@ fn instruction_xx_dot_step( read_two_xfes_from_ram, ]; - let [hv0, hv1, hv2, hv3, hv4, hv5] = [HV0, HV1, HV2, HV3, HV4, HV5].map(curr_main_row); + let [hv0, hv1, hv2, hv3, hv4, hv5] = [ + MainColumn::HV0, + MainColumn::HV1, + MainColumn::HV2, + MainColumn::HV3, + MainColumn::HV4, + MainColumn::HV5, + ] + .map(curr_main_row); let hv_product = xx_product([hv0, hv1, hv2], [hv3, hv4, hv5]); [ ram_pointer_constraints, - update_dotstep_accumulator(circuit_builder, [ST2, ST3, ST4], hv_product), + update_dotstep_accumulator( + circuit_builder, + [MainColumn::ST2, MainColumn::ST3, MainColumn::ST4], + hv_product, + ), instruction_group_step_1(circuit_builder), instruction_group_no_io(circuit_builder), instruction_group_op_stack_remains_except_top_n(circuit_builder, 5), @@ -2057,20 +2009,27 @@ fn instruction_xb_dot_step( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let constant = |c| circuit_builder.b_constant(c); - let increment_ram_pointer_st0 = next_main_row(ST0) - curr_main_row(ST0) - constant(1); - let increment_ram_pointer_st1 = next_main_row(ST1) - curr_main_row(ST1) - constant(3); + let increment_ram_pointer_st0 = + next_main_row(MainColumn::ST0) - curr_main_row(MainColumn::ST0) - constant(1); + let increment_ram_pointer_st1 = + next_main_row(MainColumn::ST1) - curr_main_row(MainColumn::ST1) - constant(3); - let rhs_ptr0 = curr_main_row(ST0); - let lhs_ptr0 = curr_main_row(ST1); + let rhs_ptr0 = curr_main_row(MainColumn::ST0); + let lhs_ptr0 = curr_main_row(MainColumn::ST1); let lhs_ptr1 = lhs_ptr0.clone() + constant(1); let lhs_ptr2 = lhs_ptr0.clone() + constant(2); let ram_read_sources = [rhs_ptr0, lhs_ptr0, lhs_ptr1, lhs_ptr2]; - let ram_read_destinations = [HV0, HV1, HV2, HV3].map(curr_main_row); + let ram_read_destinations = [ + MainColumn::HV0, + MainColumn::HV1, + MainColumn::HV2, + MainColumn::HV3, + ] + .map(curr_main_row); let read_bfe_and_xfe_from_ram = read_from_ram_to(circuit_builder, ram_read_sources, ram_read_destinations); @@ -2080,12 +2039,22 @@ fn instruction_xb_dot_step( read_bfe_and_xfe_from_ram, ]; - let [hv0, hv1, hv2, hv3] = [HV0, HV1, HV2, HV3].map(curr_main_row); + let [hv0, hv1, hv2, hv3] = [ + MainColumn::HV0, + MainColumn::HV1, + MainColumn::HV2, + MainColumn::HV3, + ] + .map(curr_main_row); let hv_product = xb_product([hv1, hv2, hv3], hv0); [ ram_pointer_constraints, - update_dotstep_accumulator(circuit_builder, [ST2, ST3, ST4], hv_product), + update_dotstep_accumulator( + circuit_builder, + [MainColumn::ST2, MainColumn::ST3, MainColumn::ST4], + hv_product, + ), instruction_group_step_1(circuit_builder), instruction_group_no_io(circuit_builder), instruction_group_op_stack_remains_except_top_n(circuit_builder, 5), @@ -2160,59 +2129,50 @@ fn log_derivative_accumulates_clk_next( circuit_builder: &ConstraintCircuitBuilder, ) -> ConstraintCircuitMonad { let challenge = |c: ChallengeId| circuit_builder.challenge(c); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); - (next_aux_row(ClockJumpDifferenceLookupServerLogDerivative) - - curr_aux_row(ClockJumpDifferenceLookupServerLogDerivative)) - * (challenge(ClockJumpDifferenceLookupIndeterminate) - next_main_row(CLK)) - - next_main_row(ClockJumpDifferenceLookupMultiplicity) + (next_aux_row(AuxColumn::ClockJumpDifferenceLookupServerLogDerivative) + - curr_aux_row(AuxColumn::ClockJumpDifferenceLookupServerLogDerivative)) + * (challenge(ChallengeId::ClockJumpDifferenceLookupIndeterminate) + - next_main_row(MainColumn::CLK)) + - next_main_row(MainColumn::ClockJumpDifferenceLookupMultiplicity) } fn running_evaluation_for_standard_input_remains_unchanged( circuit_builder: &ConstraintCircuitBuilder, ) -> ConstraintCircuitMonad { - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); - next_aux_row(InputTableEvalArg) - curr_aux_row(InputTableEvalArg) + next_aux_row(AuxColumn::InputTableEvalArg) - curr_aux_row(AuxColumn::InputTableEvalArg) } fn running_evaluation_for_standard_output_remains_unchanged( circuit_builder: &ConstraintCircuitBuilder, ) -> ConstraintCircuitMonad { - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); - next_aux_row(OutputTableEvalArg) - curr_aux_row(OutputTableEvalArg) + next_aux_row(AuxColumn::OutputTableEvalArg) - curr_aux_row(AuxColumn::OutputTableEvalArg) } fn grow_stack_by_n_and_read_n_symbols_from_input( circuit_builder: &ConstraintCircuitBuilder, n: usize, ) -> Vec> { - let indeterminate = || circuit_builder.challenge(StandardInputIndeterminate); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + let indeterminate = || circuit_builder.challenge(ChallengeId::StandardInputIndeterminate); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); - let mut running_evaluation = curr_aux_row(InputTableEvalArg); + let mut running_evaluation = curr_aux_row(AuxColumn::InputTableEvalArg); for i in (0..n).rev() { let stack_element = ProcessorTable::op_stack_column_by_index(i); running_evaluation = indeterminate() * running_evaluation + next_main_row(stack_element); } - let running_evaluation_update = next_aux_row(InputTableEvalArg) - running_evaluation; + let running_evaluation_update = next_aux_row(AuxColumn::InputTableEvalArg) - running_evaluation; let conditional_running_evaluation_update = indicator_polynomial(circuit_builder, n) * running_evaluation_update; @@ -2225,20 +2185,19 @@ fn shrink_stack_by_n_and_write_n_symbols_to_output( circuit_builder: &ConstraintCircuitBuilder, n: usize, ) -> Vec> { - let indeterminate = || circuit_builder.challenge(StandardOutputIndeterminate); + let indeterminate = || circuit_builder.challenge(ChallengeId::StandardOutputIndeterminate); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); - let mut running_evaluation = curr_aux_row(OutputTableEvalArg); + let mut running_evaluation = curr_aux_row(AuxColumn::OutputTableEvalArg); for i in 0..n { let stack_element = ProcessorTable::op_stack_column_by_index(i); running_evaluation = indeterminate() * running_evaluation + curr_main_row(stack_element); } - let running_evaluation_update = next_aux_row(OutputTableEvalArg) - running_evaluation; + let running_evaluation_update = + next_aux_row(AuxColumn::OutputTableEvalArg) - running_evaluation; let conditional_running_evaluation_update = indicator_polynomial(circuit_builder, n) * running_evaluation_update; @@ -2252,25 +2211,23 @@ fn log_derivative_for_instruction_lookup_updates_correctly( ) -> ConstraintCircuitMonad { let one = || circuit_builder.b_constant(1); let challenge = |c: ChallengeId| circuit_builder.challenge(c); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); - - let compressed_row = challenge(ProgramAddressWeight) * next_main_row(IP) - + challenge(ProgramInstructionWeight) * next_main_row(CI) - + challenge(ProgramNextInstructionWeight) * next_main_row(NIA); - let log_derivative_updates = (next_aux_row(InstructionLookupClientLogDerivative) - - curr_aux_row(InstructionLookupClientLogDerivative)) - * (challenge(InstructionLookupIndeterminate) - compressed_row) + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + + let compressed_row = challenge(ChallengeId::ProgramAddressWeight) + * next_main_row(MainColumn::IP) + + challenge(ChallengeId::ProgramInstructionWeight) * next_main_row(MainColumn::CI) + + challenge(ChallengeId::ProgramNextInstructionWeight) * next_main_row(MainColumn::NIA); + let log_derivative_updates = (next_aux_row(AuxColumn::InstructionLookupClientLogDerivative) + - curr_aux_row(AuxColumn::InstructionLookupClientLogDerivative)) + * (challenge(ChallengeId::InstructionLookupIndeterminate) - compressed_row) - one(); - let log_derivative_remains = next_aux_row(InstructionLookupClientLogDerivative) - - curr_aux_row(InstructionLookupClientLogDerivative); + let log_derivative_remains = next_aux_row(AuxColumn::InstructionLookupClientLogDerivative) + - curr_aux_row(AuxColumn::InstructionLookupClientLogDerivative); - (one() - next_main_row(IsPadding)) * log_derivative_updates - + next_main_row(IsPadding) * log_derivative_remains + (one() - next_main_row(MainColumn::IsPadding)) * log_derivative_updates + + next_main_row(MainColumn::IsPadding) * log_derivative_remains } fn constraints_for_shrinking_stack_by_3_and_top_3_unconstrained( @@ -2278,22 +2235,22 @@ fn constraints_for_shrinking_stack_by_3_and_top_3_unconstrained( ) -> Vec> { let constant = |c: u64| circuit_builder.b_constant(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); vec![ - next_main_row(ST3) - curr_main_row(ST6), - next_main_row(ST4) - curr_main_row(ST7), - next_main_row(ST5) - curr_main_row(ST8), - next_main_row(ST6) - curr_main_row(ST9), - next_main_row(ST7) - curr_main_row(ST10), - next_main_row(ST8) - curr_main_row(ST11), - next_main_row(ST9) - curr_main_row(ST12), - next_main_row(ST10) - curr_main_row(ST13), - next_main_row(ST11) - curr_main_row(ST14), - next_main_row(ST12) - curr_main_row(ST15), - next_main_row(OpStackPointer) - curr_main_row(OpStackPointer) + constant(3), + next_main_row(MainColumn::ST3) - curr_main_row(MainColumn::ST6), + next_main_row(MainColumn::ST4) - curr_main_row(MainColumn::ST7), + next_main_row(MainColumn::ST5) - curr_main_row(MainColumn::ST8), + next_main_row(MainColumn::ST6) - curr_main_row(MainColumn::ST9), + next_main_row(MainColumn::ST7) - curr_main_row(MainColumn::ST10), + next_main_row(MainColumn::ST8) - curr_main_row(MainColumn::ST11), + next_main_row(MainColumn::ST9) - curr_main_row(MainColumn::ST12), + next_main_row(MainColumn::ST10) - curr_main_row(MainColumn::ST13), + next_main_row(MainColumn::ST11) - curr_main_row(MainColumn::ST14), + next_main_row(MainColumn::ST12) - curr_main_row(MainColumn::ST15), + next_main_row(MainColumn::OpStackPointer) - curr_main_row(MainColumn::OpStackPointer) + + constant(3), running_product_op_stack_accounts_for_shrinking_stack_by(circuit_builder, 3), ] } @@ -2388,10 +2345,8 @@ fn constraints_for_shrinking_stack_by( n: usize, ) -> Vec> { let constant = |c: usize| circuit_builder.b_constant(u64::try_from(c).unwrap()); - let curr_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_row = |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let stack = || (0..OpStackElement::COUNT).map(ProcessorTable::op_stack_column_by_index); let new_stack = stack().dropping_back(n).map(next_row).collect_vec(); @@ -2407,7 +2362,7 @@ fn constraints_for_shrinking_stack_by( let compressed_old_stack = compress(old_stack_with_top_n_removed); let op_stack_pointer_shrinks_by_n = - next_row(OpStackPointer) - curr_row(OpStackPointer) + constant(n); + next_row(MainColumn::OpStackPointer) - curr_row(MainColumn::OpStackPointer) + constant(n); let new_stack_is_old_stack_with_top_n_removed = compressed_new_stack - compressed_old_stack; vec![ @@ -2422,10 +2377,8 @@ fn constraints_for_growing_stack_by( n: usize, ) -> Vec> { let constant = |c: usize| circuit_builder.b_constant(u32::try_from(c).unwrap()); - let curr_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_row = |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); let stack = || (0..OpStackElement::COUNT).map(ProcessorTable::op_stack_column_by_index); let new_stack = stack().skip(n).map(next_row).collect_vec(); @@ -2441,7 +2394,7 @@ fn constraints_for_growing_stack_by( let compressed_old_stack = compress(old_stack_with_top_n_added); let op_stack_pointer_grows_by_n = - next_row(OpStackPointer) - curr_row(OpStackPointer) - constant(n); + next_row(MainColumn::OpStackPointer) - curr_row(MainColumn::OpStackPointer) - constant(n); let new_stack_is_old_stack_with_top_n_added = compressed_new_stack - compressed_old_stack; vec![ @@ -2476,10 +2429,8 @@ fn running_product_op_stack_accounts_for_growing_stack_by( n: usize, ) -> ConstraintCircuitMonad { let constant = |c: u32| circuit_builder.b_constant(c); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); let single_grow_factor = |op_stack_pointer_offset| { single_factor_for_permutation_argument_with_op_stack_table( circuit_builder, @@ -2493,7 +2444,8 @@ fn running_product_op_stack_accounts_for_growing_stack_by( factor = factor * single_grow_factor(op_stack_pointer_offset); } - next_aux_row(OpStackTablePermArg) - curr_aux_row(OpStackTablePermArg) * factor + next_aux_row(AuxColumn::OpStackTablePermArg) + - curr_aux_row(AuxColumn::OpStackTablePermArg) * factor } fn running_product_op_stack_accounts_for_shrinking_stack_by( @@ -2501,10 +2453,8 @@ fn running_product_op_stack_accounts_for_shrinking_stack_by( n: usize, ) -> ConstraintCircuitMonad { let constant = |c: u32| circuit_builder.b_constant(c); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); let single_shrink_factor = |op_stack_pointer_offset| { single_factor_for_permutation_argument_with_op_stack_table( circuit_builder, @@ -2518,7 +2468,8 @@ fn running_product_op_stack_accounts_for_shrinking_stack_by( factor = factor * single_shrink_factor(op_stack_pointer_offset); } - next_aux_row(OpStackTablePermArg) - curr_aux_row(OpStackTablePermArg) * factor + next_aux_row(AuxColumn::OpStackTablePermArg) + - curr_aux_row(AuxColumn::OpStackTablePermArg) * factor } fn single_factor_for_permutation_argument_with_op_stack_table( @@ -2529,8 +2480,8 @@ fn single_factor_for_permutation_argument_with_op_stack_table( let constant = |c: u32| circuit_builder.b_constant(c); let challenge = |c: ChallengeId| circuit_builder.challenge(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let row_with_shorter_stack = |col: ProcessorMainColumn| { + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let row_with_shorter_stack = |col: MainColumn| { circuit_builder.input(row_with_shorter_stack_indicator(col.master_main_index())) }; @@ -2539,15 +2490,15 @@ fn single_factor_for_permutation_argument_with_op_stack_table( let stack_element = ProcessorTable::op_stack_column_by_index(stack_element_index); let underflow_element = row_with_shorter_stack(stack_element); - let op_stack_pointer = row_with_shorter_stack(OpStackPointer); + let op_stack_pointer = row_with_shorter_stack(MainColumn::OpStackPointer); let offset = constant(op_stack_pointer_offset as u32); let offset_op_stack_pointer = op_stack_pointer + offset; - let compressed_row = challenge(OpStackClkWeight) * curr_main_row(CLK) - + challenge(OpStackIb1Weight) * curr_main_row(IB1) - + challenge(OpStackPointerWeight) * offset_op_stack_pointer - + challenge(OpStackFirstUnderflowElementWeight) * underflow_element; - challenge(OpStackIndeterminate) - compressed_row + let compressed_row = challenge(ChallengeId::OpStackClkWeight) * curr_main_row(MainColumn::CLK) + + challenge(ChallengeId::OpStackIb1Weight) * curr_main_row(MainColumn::IB1) + + challenge(ChallengeId::OpStackPointerWeight) * offset_op_stack_pointer + + challenge(ChallengeId::OpStackFirstUnderflowElementWeight) * underflow_element; + challenge(ChallengeId::OpStackIndeterminate) - compressed_row } /// Build constraints for popping `n` elements from the top of the stack and @@ -2605,13 +2556,14 @@ fn shrink_stack_by_n_and_write_n_elements_to_ram( ) -> Vec> { let constant = |c: usize| circuit_builder.b_constant(u32::try_from(c).unwrap()); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let op_stack_pointer_shrinks_by_n = - next_main_row(OpStackPointer) - curr_main_row(OpStackPointer) + constant(n); - let ram_pointer_grows_by_n = next_main_row(ST0) - curr_main_row(ST0) - constant(n); + let op_stack_pointer_shrinks_by_n = next_main_row(MainColumn::OpStackPointer) + - curr_main_row(MainColumn::OpStackPointer) + + constant(n); + let ram_pointer_grows_by_n = + next_main_row(MainColumn::ST0) - curr_main_row(MainColumn::ST0) - constant(n); let mut constraints = vec![ op_stack_pointer_shrinks_by_n, @@ -2637,13 +2589,14 @@ fn grow_stack_by_n_and_read_n_elements_from_ram( ) -> Vec> { let constant = |c: usize| circuit_builder.b_constant(u64::try_from(c).unwrap()); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let op_stack_pointer_grows_by_n = - next_main_row(OpStackPointer) - curr_main_row(OpStackPointer) - constant(n); - let ram_pointer_shrinks_by_n = next_main_row(ST0) - curr_main_row(ST0) + constant(n); + let op_stack_pointer_grows_by_n = next_main_row(MainColumn::OpStackPointer) + - curr_main_row(MainColumn::OpStackPointer) + - constant(n); + let ram_pointer_shrinks_by_n = + next_main_row(MainColumn::ST0) - curr_main_row(MainColumn::ST0) + constant(n); let mut constraints = vec![ op_stack_pointer_grows_by_n, @@ -2668,10 +2621,8 @@ fn running_product_ram_accounts_for_writing_n_elements( n: usize, ) -> ConstraintCircuitMonad { let constant = |c: u32| circuit_builder.b_constant(c); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); let single_write_factor = |ram_pointer_offset| { single_factor_for_permutation_argument_with_ram_table( circuit_builder, @@ -2686,7 +2637,7 @@ fn running_product_ram_accounts_for_writing_n_elements( factor = factor * single_write_factor(ram_pointer_offset); } - next_aux_row(RamTablePermArg) - curr_aux_row(RamTablePermArg) * factor + next_aux_row(AuxColumn::RamTablePermArg) - curr_aux_row(AuxColumn::RamTablePermArg) * factor } fn running_product_ram_accounts_for_reading_n_elements( @@ -2694,10 +2645,8 @@ fn running_product_ram_accounts_for_reading_n_elements( n: usize, ) -> ConstraintCircuitMonad { let constant = |c: u32| circuit_builder.b_constant(c); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); let single_read_factor = |ram_pointer_offset| { single_factor_for_permutation_argument_with_ram_table( circuit_builder, @@ -2712,7 +2661,7 @@ fn running_product_ram_accounts_for_reading_n_elements( factor = factor * single_read_factor(ram_pointer_offset); } - next_aux_row(RamTablePermArg) - curr_aux_row(RamTablePermArg) * factor + next_aux_row(AuxColumn::RamTablePermArg) - curr_aux_row(AuxColumn::RamTablePermArg) * factor } fn single_factor_for_permutation_argument_with_ram_table( @@ -2725,8 +2674,8 @@ fn single_factor_for_permutation_argument_with_ram_table( let b_constant = |c| circuit_builder.b_constant(c); let challenge = |c: ChallengeId| circuit_builder.challenge(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let row_with_longer_stack = |col: ProcessorMainColumn| { + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let row_with_longer_stack = |col: MainColumn| { circuit_builder.input(row_with_longer_stack_indicator(col.master_main_index())) }; @@ -2741,36 +2690,35 @@ fn single_factor_for_permutation_argument_with_ram_table( _ => panic!("Invalid instruction type"), }; - let ram_pointer = row_with_longer_stack(ST0); + let ram_pointer = row_with_longer_stack(MainColumn::ST0); let offset = constant(additional_offset + ram_pointer_offset as u32); let offset_ram_pointer = ram_pointer + offset; - let compressed_row = curr_main_row(CLK) * challenge(RamClkWeight) - + b_constant(instruction_type) * challenge(RamInstructionTypeWeight) - + offset_ram_pointer * challenge(RamPointerWeight) - + ram_value * challenge(RamValueWeight); - challenge(RamIndeterminate) - compressed_row + let compressed_row = curr_main_row(MainColumn::CLK) * challenge(ChallengeId::RamClkWeight) + + b_constant(instruction_type) * challenge(ChallengeId::RamInstructionTypeWeight) + + offset_ram_pointer * challenge(ChallengeId::RamPointerWeight) + + ram_value * challenge(ChallengeId::RamValueWeight); + challenge(ChallengeId::RamIndeterminate) - compressed_row } fn running_product_for_jump_stack_table_updates_correctly( circuit_builder: &ConstraintCircuitBuilder, ) -> ConstraintCircuitMonad { let challenge = |c: ChallengeId| circuit_builder.challenge(c); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); - let compressed_row = challenge(JumpStackClkWeight) * next_main_row(CLK) - + challenge(JumpStackCiWeight) * next_main_row(CI) - + challenge(JumpStackJspWeight) * next_main_row(JSP) - + challenge(JumpStackJsoWeight) * next_main_row(JSO) - + challenge(JumpStackJsdWeight) * next_main_row(JSD); + let compressed_row = challenge(ChallengeId::JumpStackClkWeight) + * next_main_row(MainColumn::CLK) + + challenge(ChallengeId::JumpStackCiWeight) * next_main_row(MainColumn::CI) + + challenge(ChallengeId::JumpStackJspWeight) * next_main_row(MainColumn::JSP) + + challenge(ChallengeId::JumpStackJsoWeight) * next_main_row(MainColumn::JSO) + + challenge(ChallengeId::JumpStackJsdWeight) * next_main_row(MainColumn::JSD); - next_aux_row(JumpStackTablePermArg) - - curr_aux_row(JumpStackTablePermArg) * (challenge(JumpStackIndeterminate) - compressed_row) + next_aux_row(AuxColumn::JumpStackTablePermArg) + - curr_aux_row(AuxColumn::JumpStackTablePermArg) + * (challenge(ChallengeId::JumpStackIndeterminate) - compressed_row) } /// Deal with instructions `hash` and `merkle_step`. The registers from which @@ -2790,38 +2738,48 @@ fn running_evaluation_hash_input_updates_correctly( let constant = |c: u32| circuit_builder.b_constant(c); let one = || constant(1); let challenge = |c: ChallengeId| circuit_builder.challenge(c); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); let hash_deselector = instruction_deselector_next_row(circuit_builder, Instruction::Hash); let merkle_step_deselector = instruction_deselector_next_row(circuit_builder, Instruction::MerkleStep); let merkle_step_mem_deselector = instruction_deselector_next_row(circuit_builder, Instruction::MerkleStepMem); - let hash_and_merkle_step_selector = (next_main_row(CI) - constant(Instruction::Hash.opcode())) - * (next_main_row(CI) - constant(Instruction::MerkleStep.opcode())) - * (next_main_row(CI) - constant(Instruction::MerkleStepMem.opcode())); + let hash_and_merkle_step_selector = (next_main_row(MainColumn::CI) + - constant(Instruction::Hash.opcode())) + * (next_main_row(MainColumn::CI) - constant(Instruction::MerkleStep.opcode())) + * (next_main_row(MainColumn::CI) - constant(Instruction::MerkleStepMem.opcode())); let weights = [ - StackWeight0, - StackWeight1, - StackWeight2, - StackWeight3, - StackWeight4, - StackWeight5, - StackWeight6, - StackWeight7, - StackWeight8, - StackWeight9, + ChallengeId::StackWeight0, + ChallengeId::StackWeight1, + ChallengeId::StackWeight2, + ChallengeId::StackWeight3, + ChallengeId::StackWeight4, + ChallengeId::StackWeight5, + ChallengeId::StackWeight6, + ChallengeId::StackWeight7, + ChallengeId::StackWeight8, + ChallengeId::StackWeight9, ] .map(challenge); // hash - let state_for_hash = [ST0, ST1, ST2, ST3, ST4, ST5, ST6, ST7, ST8, ST9].map(next_main_row); + let state_for_hash = [ + MainColumn::ST0, + MainColumn::ST1, + MainColumn::ST2, + MainColumn::ST3, + MainColumn::ST4, + MainColumn::ST5, + MainColumn::ST6, + MainColumn::ST7, + MainColumn::ST8, + MainColumn::ST9, + ] + .map(next_main_row); let compressed_hash_row = weights .iter() .zip_eq(state_for_hash) @@ -2829,21 +2787,21 @@ fn running_evaluation_hash_input_updates_correctly( .sum(); // merkle step - let is_left_sibling = || next_main_row(HV5); - let is_right_sibling = || one() - next_main_row(HV5); + let is_left_sibling = || next_main_row(MainColumn::HV5); + let is_right_sibling = || one() - next_main_row(MainColumn::HV5); let merkle_step_state_element = |l, r| is_right_sibling() * next_main_row(l) + is_left_sibling() * next_main_row(r); let state_for_merkle_step = [ - merkle_step_state_element(ST0, HV0), - merkle_step_state_element(ST1, HV1), - merkle_step_state_element(ST2, HV2), - merkle_step_state_element(ST3, HV3), - merkle_step_state_element(ST4, HV4), - merkle_step_state_element(HV0, ST0), - merkle_step_state_element(HV1, ST1), - merkle_step_state_element(HV2, ST2), - merkle_step_state_element(HV3, ST3), - merkle_step_state_element(HV4, ST4), + merkle_step_state_element(MainColumn::ST0, MainColumn::HV0), + merkle_step_state_element(MainColumn::ST1, MainColumn::HV1), + merkle_step_state_element(MainColumn::ST2, MainColumn::HV2), + merkle_step_state_element(MainColumn::ST3, MainColumn::HV3), + merkle_step_state_element(MainColumn::ST4, MainColumn::HV4), + merkle_step_state_element(MainColumn::HV0, MainColumn::ST0), + merkle_step_state_element(MainColumn::HV1, MainColumn::ST1), + merkle_step_state_element(MainColumn::HV2, MainColumn::ST2), + merkle_step_state_element(MainColumn::HV3, MainColumn::ST3), + merkle_step_state_element(MainColumn::HV4, MainColumn::ST4), ]; let compressed_merkle_step_row = weights .into_iter() @@ -2852,12 +2810,13 @@ fn running_evaluation_hash_input_updates_correctly( .sum::>(); let running_evaluation_updates_with = |compressed_row| { - next_aux_row(HashInputEvalArg) - - challenge(HashInputIndeterminate) * curr_aux_row(HashInputEvalArg) + next_aux_row(AuxColumn::HashInputEvalArg) + - challenge(ChallengeId::HashInputIndeterminate) + * curr_aux_row(AuxColumn::HashInputEvalArg) - compressed_row }; let running_evaluation_remains = - next_aux_row(HashInputEvalArg) - curr_aux_row(HashInputEvalArg); + next_aux_row(AuxColumn::HashInputEvalArg) - curr_aux_row(AuxColumn::HashInputEvalArg); hash_and_merkle_step_selector * running_evaluation_remains + hash_deselector * running_evaluation_updates_with(compressed_hash_row) @@ -2872,43 +2831,49 @@ fn running_evaluation_hash_digest_updates_correctly( let constant = |c: u32| circuit_builder.b_constant(c); let challenge = |c: ChallengeId| circuit_builder.challenge(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); let hash_deselector = instruction_deselector_current_row(circuit_builder, Instruction::Hash); let merkle_step_deselector = instruction_deselector_current_row(circuit_builder, Instruction::MerkleStep); let merkle_step_mem_deselector = instruction_deselector_current_row(circuit_builder, Instruction::MerkleStepMem); - let hash_and_merkle_step_selector = (curr_main_row(CI) - constant(Instruction::Hash.opcode())) - * (curr_main_row(CI) - constant(Instruction::MerkleStep.opcode())) - * (curr_main_row(CI) - constant(Instruction::MerkleStepMem.opcode())); + let hash_and_merkle_step_selector = (curr_main_row(MainColumn::CI) + - constant(Instruction::Hash.opcode())) + * (curr_main_row(MainColumn::CI) - constant(Instruction::MerkleStep.opcode())) + * (curr_main_row(MainColumn::CI) - constant(Instruction::MerkleStepMem.opcode())); let weights = [ - StackWeight0, - StackWeight1, - StackWeight2, - StackWeight3, - StackWeight4, + ChallengeId::StackWeight0, + ChallengeId::StackWeight1, + ChallengeId::StackWeight2, + ChallengeId::StackWeight3, + ChallengeId::StackWeight4, ] .map(challenge); - let state = [ST0, ST1, ST2, ST3, ST4].map(next_main_row); + let state = [ + MainColumn::ST0, + MainColumn::ST1, + MainColumn::ST2, + MainColumn::ST3, + MainColumn::ST4, + ] + .map(next_main_row); let compressed_row = weights .into_iter() .zip_eq(state) .map(|(weight, state)| weight * state) .sum(); - let running_evaluation_updates = next_aux_row(HashDigestEvalArg) - - challenge(HashDigestIndeterminate) * curr_aux_row(HashDigestEvalArg) + let running_evaluation_updates = next_aux_row(AuxColumn::HashDigestEvalArg) + - challenge(ChallengeId::HashDigestIndeterminate) + * curr_aux_row(AuxColumn::HashDigestEvalArg) - compressed_row; let running_evaluation_remains = - next_aux_row(HashDigestEvalArg) - curr_aux_row(HashDigestEvalArg); + next_aux_row(AuxColumn::HashDigestEvalArg) - curr_aux_row(AuxColumn::HashDigestEvalArg); hash_and_merkle_step_selector * running_evaluation_remains + (hash_deselector + merkle_step_deselector + merkle_step_mem_deselector) @@ -2921,13 +2886,10 @@ fn running_evaluation_sponge_updates_correctly( let constant = |c: u32| circuit_builder.b_constant(c); let challenge = |c: ChallengeId| circuit_builder.challenge(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); let sponge_init_deselector = instruction_deselector_current_row(circuit_builder, Instruction::SpongeInit); @@ -2938,53 +2900,79 @@ fn running_evaluation_sponge_updates_correctly( let sponge_squeeze_deselector = instruction_deselector_current_row(circuit_builder, Instruction::SpongeSqueeze); - let sponge_instruction_selector = (curr_main_row(CI) + let sponge_instruction_selector = (curr_main_row(MainColumn::CI) - constant(Instruction::SpongeInit.opcode())) - * (curr_main_row(CI) - constant(Instruction::SpongeAbsorb.opcode())) - * (curr_main_row(CI) - constant(Instruction::SpongeAbsorbMem.opcode())) - * (curr_main_row(CI) - constant(Instruction::SpongeSqueeze.opcode())); + * (curr_main_row(MainColumn::CI) - constant(Instruction::SpongeAbsorb.opcode())) + * (curr_main_row(MainColumn::CI) - constant(Instruction::SpongeAbsorbMem.opcode())) + * (curr_main_row(MainColumn::CI) - constant(Instruction::SpongeSqueeze.opcode())); let weighted_sum = |state| { let weights = [ - StackWeight0, - StackWeight1, - StackWeight2, - StackWeight3, - StackWeight4, - StackWeight5, - StackWeight6, - StackWeight7, - StackWeight8, - StackWeight9, + ChallengeId::StackWeight0, + ChallengeId::StackWeight1, + ChallengeId::StackWeight2, + ChallengeId::StackWeight3, + ChallengeId::StackWeight4, + ChallengeId::StackWeight5, + ChallengeId::StackWeight6, + ChallengeId::StackWeight7, + ChallengeId::StackWeight8, + ChallengeId::StackWeight9, ]; let weights = weights.map(challenge).into_iter(); weights.zip_eq(state).map(|(w, st)| w * st).sum() }; - let state = [ST0, ST1, ST2, ST3, ST4, ST5, ST6, ST7, ST8, ST9]; + let state = [ + MainColumn::ST0, + MainColumn::ST1, + MainColumn::ST2, + MainColumn::ST3, + MainColumn::ST4, + MainColumn::ST5, + MainColumn::ST6, + MainColumn::ST7, + MainColumn::ST8, + MainColumn::ST9, + ]; let compressed_row_current = weighted_sum(state.map(curr_main_row)); let compressed_row_next = weighted_sum(state.map(next_main_row)); // Use domain-specific knowledge: the compressed row (i.e., random linear sum) // of the initial Sponge state is 0. - let running_evaluation_updates_for_sponge_init = next_aux_row(SpongeEvalArg) - - challenge(SpongeIndeterminate) * curr_aux_row(SpongeEvalArg) - - challenge(HashCIWeight) * curr_main_row(CI); + let running_evaluation_updates_for_sponge_init = next_aux_row(AuxColumn::SpongeEvalArg) + - challenge(ChallengeId::SpongeIndeterminate) * curr_aux_row(AuxColumn::SpongeEvalArg) + - challenge(ChallengeId::HashCIWeight) * curr_main_row(MainColumn::CI); let running_evaluation_updates_for_absorb = running_evaluation_updates_for_sponge_init.clone() - compressed_row_current; let running_evaluation_updates_for_squeeze = running_evaluation_updates_for_sponge_init.clone() - compressed_row_next; - let running_evaluation_remains = next_aux_row(SpongeEvalArg) - curr_aux_row(SpongeEvalArg); + let running_evaluation_remains = + next_aux_row(AuxColumn::SpongeEvalArg) - curr_aux_row(AuxColumn::SpongeEvalArg); // `sponge_absorb_mem` - let stack_elements = [ST1, ST2, ST3, ST4].map(next_main_row); - let hv_elements = [HV0, HV1, HV2, HV3, HV4, HV5].map(curr_main_row); + let stack_elements = [ + MainColumn::ST1, + MainColumn::ST2, + MainColumn::ST3, + MainColumn::ST4, + ] + .map(next_main_row); + let hv_elements = [ + MainColumn::HV0, + MainColumn::HV1, + MainColumn::HV2, + MainColumn::HV3, + MainColumn::HV4, + MainColumn::HV5, + ] + .map(curr_main_row); let absorb_mem_elements = stack_elements.into_iter().chain(hv_elements); let absorb_mem_elements = absorb_mem_elements.collect_vec().try_into().unwrap(); let compressed_row_absorb_mem = weighted_sum(absorb_mem_elements); - let running_evaluation_updates_for_absorb_mem = next_aux_row(SpongeEvalArg) - - challenge(SpongeIndeterminate) * curr_aux_row(SpongeEvalArg) - - challenge(HashCIWeight) * constant(Instruction::SpongeAbsorb.opcode()) + let running_evaluation_updates_for_absorb_mem = next_aux_row(AuxColumn::SpongeEvalArg) + - challenge(ChallengeId::SpongeIndeterminate) * curr_aux_row(AuxColumn::SpongeEvalArg) + - challenge(ChallengeId::HashCIWeight) * constant(Instruction::SpongeAbsorb.opcode()) - compressed_row_absorb_mem; sponge_instruction_selector * running_evaluation_remains @@ -3002,13 +2990,10 @@ fn log_derivative_with_u32_table_updates_correctly( let two_inverse = circuit_builder.b_constant(bfe!(2).inverse()); let challenge = |c: ChallengeId| circuit_builder.challenge(c); let curr_main_row = - |col: ProcessorMainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); - let next_main_row = - |col: ProcessorMainColumn| circuit_builder.input(NextMain(col.master_main_index())); - let curr_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); - let next_aux_row = - |col: ProcessorAuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); + |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_main_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + let curr_aux_row = |col: AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index())); + let next_aux_row = |col: AuxColumn| circuit_builder.input(NextAux(col.master_aux_index())); let split_deselector = instruction_deselector_current_row(circuit_builder, Instruction::Split); let lt_deselector = instruction_deselector_current_row(circuit_builder, Instruction::Lt); @@ -3026,42 +3011,43 @@ fn log_derivative_with_u32_table_updates_correctly( let merkle_step_mem_deselector = instruction_deselector_current_row(circuit_builder, Instruction::MerkleStepMem); - let running_sum = curr_aux_row(U32LookupClientLogDerivative); - let running_sum_next = next_aux_row(U32LookupClientLogDerivative); - - let split_factor = challenge(U32Indeterminate) - - challenge(U32LhsWeight) * next_main_row(ST0) - - challenge(U32RhsWeight) * next_main_row(ST1) - - challenge(U32CiWeight) * curr_main_row(CI); - let binop_factor = challenge(U32Indeterminate) - - challenge(U32LhsWeight) * curr_main_row(ST0) - - challenge(U32RhsWeight) * curr_main_row(ST1) - - challenge(U32CiWeight) * curr_main_row(CI) - - challenge(U32ResultWeight) * next_main_row(ST0); - let xor_factor = challenge(U32Indeterminate) - - challenge(U32LhsWeight) * curr_main_row(ST0) - - challenge(U32RhsWeight) * curr_main_row(ST1) - - challenge(U32CiWeight) * constant(Instruction::And.opcode()) - - challenge(U32ResultWeight) - * (curr_main_row(ST0) + curr_main_row(ST1) - next_main_row(ST0)) + let running_sum = curr_aux_row(AuxColumn::U32LookupClientLogDerivative); + let running_sum_next = next_aux_row(AuxColumn::U32LookupClientLogDerivative); + + let split_factor = challenge(ChallengeId::U32Indeterminate) + - challenge(ChallengeId::U32LhsWeight) * next_main_row(MainColumn::ST0) + - challenge(ChallengeId::U32RhsWeight) * next_main_row(MainColumn::ST1) + - challenge(ChallengeId::U32CiWeight) * curr_main_row(MainColumn::CI); + let binop_factor = challenge(ChallengeId::U32Indeterminate) + - challenge(ChallengeId::U32LhsWeight) * curr_main_row(MainColumn::ST0) + - challenge(ChallengeId::U32RhsWeight) * curr_main_row(MainColumn::ST1) + - challenge(ChallengeId::U32CiWeight) * curr_main_row(MainColumn::CI) + - challenge(ChallengeId::U32ResultWeight) * next_main_row(MainColumn::ST0); + let xor_factor = challenge(ChallengeId::U32Indeterminate) + - challenge(ChallengeId::U32LhsWeight) * curr_main_row(MainColumn::ST0) + - challenge(ChallengeId::U32RhsWeight) * curr_main_row(MainColumn::ST1) + - challenge(ChallengeId::U32CiWeight) * constant(Instruction::And.opcode()) + - challenge(ChallengeId::U32ResultWeight) + * (curr_main_row(MainColumn::ST0) + curr_main_row(MainColumn::ST1) + - next_main_row(MainColumn::ST0)) * two_inverse; - let unop_factor = challenge(U32Indeterminate) - - challenge(U32LhsWeight) * curr_main_row(ST0) - - challenge(U32CiWeight) * curr_main_row(CI) - - challenge(U32ResultWeight) * next_main_row(ST0); - let div_mod_factor_for_lt = challenge(U32Indeterminate) - - challenge(U32LhsWeight) * next_main_row(ST0) - - challenge(U32RhsWeight) * curr_main_row(ST1) - - challenge(U32CiWeight) * constant(Instruction::Lt.opcode()) - - challenge(U32ResultWeight); - let div_mod_factor_for_range_check = challenge(U32Indeterminate) - - challenge(U32LhsWeight) * curr_main_row(ST0) - - challenge(U32RhsWeight) * next_main_row(ST1) - - challenge(U32CiWeight) * constant(Instruction::Split.opcode()); - let merkle_step_range_check_factor = challenge(U32Indeterminate) - - challenge(U32LhsWeight) * curr_main_row(ST5) - - challenge(U32RhsWeight) * next_main_row(ST5) - - challenge(U32CiWeight) * constant(Instruction::Split.opcode()); + let unop_factor = challenge(ChallengeId::U32Indeterminate) + - challenge(ChallengeId::U32LhsWeight) * curr_main_row(MainColumn::ST0) + - challenge(ChallengeId::U32CiWeight) * curr_main_row(MainColumn::CI) + - challenge(ChallengeId::U32ResultWeight) * next_main_row(MainColumn::ST0); + let div_mod_factor_for_lt = challenge(ChallengeId::U32Indeterminate) + - challenge(ChallengeId::U32LhsWeight) * next_main_row(MainColumn::ST0) + - challenge(ChallengeId::U32RhsWeight) * curr_main_row(MainColumn::ST1) + - challenge(ChallengeId::U32CiWeight) * constant(Instruction::Lt.opcode()) + - challenge(ChallengeId::U32ResultWeight); + let div_mod_factor_for_range_check = challenge(ChallengeId::U32Indeterminate) + - challenge(ChallengeId::U32LhsWeight) * curr_main_row(MainColumn::ST0) + - challenge(ChallengeId::U32RhsWeight) * next_main_row(MainColumn::ST1) + - challenge(ChallengeId::U32CiWeight) * constant(Instruction::Split.opcode()); + let merkle_step_range_check_factor = challenge(ChallengeId::U32Indeterminate) + - challenge(ChallengeId::U32LhsWeight) * curr_main_row(MainColumn::ST5) + - challenge(ChallengeId::U32RhsWeight) * next_main_row(MainColumn::ST5) + - challenge(ChallengeId::U32CiWeight) * constant(Instruction::Split.opcode()); let running_sum_absorbs_split_factor = (running_sum_next.clone() - running_sum.clone()) * split_factor - one(); @@ -3091,7 +3077,8 @@ fn log_derivative_with_u32_table_updates_correctly( merkle_step_deselector * running_sum_absorbs_merkle_step_factor.clone(); let merkle_step_mem_summand = merkle_step_mem_deselector * running_sum_absorbs_merkle_step_factor; - let no_update_summand = (one() - curr_main_row(IB2)) * (running_sum_next - running_sum); + let no_update_summand = + (one() - curr_main_row(MainColumn::IB2)) * (running_sum_next - running_sum); split_summand + lt_summand @@ -3108,22 +3095,22 @@ fn log_derivative_with_u32_table_updates_correctly( fn stack_weight_by_index(i: usize) -> ChallengeId { match i { - 0 => StackWeight0, - 1 => StackWeight1, - 2 => StackWeight2, - 3 => StackWeight3, - 4 => StackWeight4, - 5 => StackWeight5, - 6 => StackWeight6, - 7 => StackWeight7, - 8 => StackWeight8, - 9 => StackWeight9, - 10 => StackWeight10, - 11 => StackWeight11, - 12 => StackWeight12, - 13 => StackWeight13, - 14 => StackWeight14, - 15 => StackWeight15, + 0 => ChallengeId::StackWeight0, + 1 => ChallengeId::StackWeight1, + 2 => ChallengeId::StackWeight2, + 3 => ChallengeId::StackWeight3, + 4 => ChallengeId::StackWeight4, + 5 => ChallengeId::StackWeight5, + 6 => ChallengeId::StackWeight6, + 7 => ChallengeId::StackWeight7, + 8 => ChallengeId::StackWeight8, + 9 => ChallengeId::StackWeight9, + 10 => ChallengeId::StackWeight10, + 11 => ChallengeId::StackWeight11, + 12 => ChallengeId::StackWeight12, + 13 => ChallengeId::StackWeight13, + 14 => ChallengeId::StackWeight14, + 15 => ChallengeId::StackWeight15, i => panic!("Op Stack weight index must be in [0, 15], not {i}."), } } @@ -3162,12 +3149,12 @@ fn helper_variable( index: usize, ) -> ConstraintCircuitMonad { match index { - 0 => circuit_builder.input(CurrentMain(HV0.master_main_index())), - 1 => circuit_builder.input(CurrentMain(HV1.master_main_index())), - 2 => circuit_builder.input(CurrentMain(HV2.master_main_index())), - 3 => circuit_builder.input(CurrentMain(HV3.master_main_index())), - 4 => circuit_builder.input(CurrentMain(HV4.master_main_index())), - 5 => circuit_builder.input(CurrentMain(HV5.master_main_index())), + 0 => circuit_builder.input(CurrentMain(MainColumn::HV0.master_main_index())), + 1 => circuit_builder.input(CurrentMain(MainColumn::HV1.master_main_index())), + 2 => circuit_builder.input(CurrentMain(MainColumn::HV2.master_main_index())), + 3 => circuit_builder.input(CurrentMain(MainColumn::HV3.master_main_index())), + 4 => circuit_builder.input(CurrentMain(MainColumn::HV4.master_main_index())), + 5 => circuit_builder.input(CurrentMain(MainColumn::HV5.master_main_index())), i => unimplemented!("Helper variable index {i} out of bounds."), } } @@ -3186,6 +3173,8 @@ mod tests { use super::*; + type MainColumn = ::MainColumn; + #[test] fn instruction_deselector_gives_0_for_all_other_instructions() { let circuit_builder = ConstraintCircuitBuilder::new(); @@ -3198,7 +3187,6 @@ mod tests { .map(|i| XFieldElement::from(i as u64)) .collect_vec(); for instruction in ALL_INSTRUCTIONS { - use ProcessorMainColumn::*; let deselector = instruction_deselector_current_row(&circuit_builder, instruction); println!("\n\nThe Deselector for instruction {instruction} is:\n{deselector}",); @@ -3209,13 +3197,20 @@ mod tests { .filter(|other_instruction| *other_instruction != instruction) { let mut curr_row = master_main_table.slice_mut(s![0, ..]); - curr_row[IB0.master_main_index()] = other_instruction.ib(InstructionBit::IB0); - curr_row[IB1.master_main_index()] = other_instruction.ib(InstructionBit::IB1); - curr_row[IB2.master_main_index()] = other_instruction.ib(InstructionBit::IB2); - curr_row[IB3.master_main_index()] = other_instruction.ib(InstructionBit::IB3); - curr_row[IB4.master_main_index()] = other_instruction.ib(InstructionBit::IB4); - curr_row[IB5.master_main_index()] = other_instruction.ib(InstructionBit::IB5); - curr_row[IB6.master_main_index()] = other_instruction.ib(InstructionBit::IB6); + curr_row[MainColumn::IB0.master_main_index()] = + other_instruction.ib(InstructionBit::IB0); + curr_row[MainColumn::IB1.master_main_index()] = + other_instruction.ib(InstructionBit::IB1); + curr_row[MainColumn::IB2.master_main_index()] = + other_instruction.ib(InstructionBit::IB2); + curr_row[MainColumn::IB3.master_main_index()] = + other_instruction.ib(InstructionBit::IB3); + curr_row[MainColumn::IB4.master_main_index()] = + other_instruction.ib(InstructionBit::IB4); + curr_row[MainColumn::IB5.master_main_index()] = + other_instruction.ib(InstructionBit::IB5); + curr_row[MainColumn::IB6.master_main_index()] = + other_instruction.ib(InstructionBit::IB6); let result = deselector.clone().consume().evaluate( master_main_table.view(), master_aux_table.view(), @@ -3232,13 +3227,13 @@ mod tests { // Positive tests let mut curr_row = master_main_table.slice_mut(s![0, ..]); - curr_row[IB0.master_main_index()] = instruction.ib(InstructionBit::IB0); - curr_row[IB1.master_main_index()] = instruction.ib(InstructionBit::IB1); - curr_row[IB2.master_main_index()] = instruction.ib(InstructionBit::IB2); - curr_row[IB3.master_main_index()] = instruction.ib(InstructionBit::IB3); - curr_row[IB4.master_main_index()] = instruction.ib(InstructionBit::IB4); - curr_row[IB5.master_main_index()] = instruction.ib(InstructionBit::IB5); - curr_row[IB6.master_main_index()] = instruction.ib(InstructionBit::IB6); + curr_row[MainColumn::IB0.master_main_index()] = instruction.ib(InstructionBit::IB0); + curr_row[MainColumn::IB1.master_main_index()] = instruction.ib(InstructionBit::IB1); + curr_row[MainColumn::IB2.master_main_index()] = instruction.ib(InstructionBit::IB2); + curr_row[MainColumn::IB3.master_main_index()] = instruction.ib(InstructionBit::IB3); + curr_row[MainColumn::IB4.master_main_index()] = instruction.ib(InstructionBit::IB4); + curr_row[MainColumn::IB5.master_main_index()] = instruction.ib(InstructionBit::IB5); + curr_row[MainColumn::IB6.master_main_index()] = instruction.ib(InstructionBit::IB6); let result = deselector.consume().evaluate( master_main_table.view(), master_aux_table.view(), @@ -3331,10 +3326,10 @@ mod tests { let mut main_table = Array2::ones([2, NUM_MAIN_COLUMNS]); let aux_table = Array2::ones([2, NUM_AUX_COLUMNS]); - main_table[[0, HV0.master_main_index()]] = bfe!(query_index % 2); - main_table[[0, HV1.master_main_index()]] = bfe!((query_index >> 1) % 2); - main_table[[0, HV2.master_main_index()]] = bfe!((query_index >> 2) % 2); - main_table[[0, HV3.master_main_index()]] = bfe!((query_index >> 3) % 2); + main_table[[0, MainColumn::HV0.master_main_index()]] = bfe!(query_index % 2); + main_table[[0, MainColumn::HV1.master_main_index()]] = bfe!((query_index >> 1) % 2); + main_table[[0, MainColumn::HV2.master_main_index()]] = bfe!((query_index >> 2) % 2); + main_table[[0, MainColumn::HV3.master_main_index()]] = bfe!((query_index >> 3) % 2); let builder = ConstraintCircuitBuilder::new(); let indicator_poly = indicator_polynomial(&builder, indicator_poly_index).consume(); @@ -3383,18 +3378,25 @@ mod tests { #[strategy(arb())] b: XFieldElement, ) { let circuit_builder = ConstraintCircuitBuilder::new(); - let main_row = - |col: ProcessorMainColumn| circuit_builder.input(Main(col.master_main_index())); - let [x0, x1, x2, y0, y1, y2] = [ST0, ST1, ST2, ST3, ST4, ST5].map(main_row); + let main_row = |col: MainColumn| circuit_builder.input(Main(col.master_main_index())); + let [x0, x1, x2, y0, y1, y2] = [ + MainColumn::ST0, + MainColumn::ST1, + MainColumn::ST2, + MainColumn::ST3, + MainColumn::ST4, + MainColumn::ST5, + ] + .map(main_row); let mut main_table = Array2::zeros([1, NUM_MAIN_COLUMNS]); let aux_table = Array2::zeros([1, NUM_AUX_COLUMNS]); - main_table[[0, ST0.master_main_index()]] = a.coefficients[0]; - main_table[[0, ST1.master_main_index()]] = a.coefficients[1]; - main_table[[0, ST2.master_main_index()]] = a.coefficients[2]; - main_table[[0, ST3.master_main_index()]] = b.coefficients[0]; - main_table[[0, ST4.master_main_index()]] = b.coefficients[1]; - main_table[[0, ST5.master_main_index()]] = b.coefficients[2]; + main_table[[0, MainColumn::ST0.master_main_index()]] = a.coefficients[0]; + main_table[[0, MainColumn::ST1.master_main_index()]] = a.coefficients[1]; + main_table[[0, MainColumn::ST2.master_main_index()]] = a.coefficients[2]; + main_table[[0, MainColumn::ST3.master_main_index()]] = b.coefficients[0]; + main_table[[0, MainColumn::ST4.master_main_index()]] = b.coefficients[1]; + main_table[[0, MainColumn::ST5.master_main_index()]] = b.coefficients[2]; let [c0, c1, c2] = xx_product([x0, x1, x2], [y0, y1, y2]) .map(|c| c.consume()) @@ -3413,16 +3415,21 @@ mod tests { #[strategy(arb())] b: BFieldElement, ) { let circuit_builder = ConstraintCircuitBuilder::new(); - let main_row = - |col: ProcessorMainColumn| circuit_builder.input(Main(col.master_main_index())); - let [x0, x1, x2, y] = [ST0, ST1, ST2, ST3].map(main_row); + let main_row = |col: MainColumn| circuit_builder.input(Main(col.master_main_index())); + let [x0, x1, x2, y] = [ + MainColumn::ST0, + MainColumn::ST1, + MainColumn::ST2, + MainColumn::ST3, + ] + .map(main_row); let mut main_table = Array2::zeros([1, NUM_MAIN_COLUMNS]); let aux_table = Array2::zeros([1, NUM_AUX_COLUMNS]); - main_table[[0, ST0.master_main_index()]] = a.coefficients[0]; - main_table[[0, ST1.master_main_index()]] = a.coefficients[1]; - main_table[[0, ST2.master_main_index()]] = a.coefficients[2]; - main_table[[0, ST3.master_main_index()]] = b; + main_table[[0, MainColumn::ST0.master_main_index()]] = a.coefficients[0]; + main_table[[0, MainColumn::ST1.master_main_index()]] = a.coefficients[1]; + main_table[[0, MainColumn::ST2.master_main_index()]] = a.coefficients[2]; + main_table[[0, MainColumn::ST3.master_main_index()]] = b; let [c0, c1, c2] = xb_product([x0, x1, x2], y) .map(|c| c.consume()) diff --git a/triton-isa/src/parser.rs b/triton-isa/src/parser.rs index 37f43153..df662652 100644 --- a/triton-isa/src/parser.rs +++ b/triton-isa/src/parser.rs @@ -7,11 +7,19 @@ use std::fmt::Formatter; use std::fmt::Result as FmtResult; use nom::branch::alt; -use nom::bytes::complete::*; +use nom::bytes::complete::tag; +use nom::bytes::complete::take_while; +use nom::bytes::complete::take_while1; use nom::character::complete::digit1; -use nom::combinator::*; -use nom::error::*; -use nom::multi::*; +use nom::combinator::cut; +use nom::combinator::eof; +use nom::combinator::fail; +use nom::combinator::opt; +use nom::error::ErrorKind; +use nom::error::VerboseError; +use nom::error::VerboseErrorKind; +use nom::multi::many0; +use nom::multi::many1; use nom::Finish; use nom::IResult; use twenty_first::bfe; @@ -60,12 +68,15 @@ impl<'a> InstructionToken<'a> { } pub fn to_labelled_instruction(&self) -> LabelledInstruction { - use InstructionToken::*; match self { - Instruction(instr, _) => LabelledInstruction::Instruction(instr.to_owned()), - Label(label, _) => LabelledInstruction::Label(label.to_owned()), - Breakpoint(_) => LabelledInstruction::Breakpoint, - TypeHint(type_hint, _) => LabelledInstruction::TypeHint(type_hint.to_owned()), + InstructionToken::Instruction(instr, _) => { + LabelledInstruction::Instruction(instr.to_owned()) + } + InstructionToken::Label(label, _) => LabelledInstruction::Label(label.to_owned()), + InstructionToken::Breakpoint(_) => LabelledInstruction::Breakpoint, + InstructionToken::TypeHint(type_hint, _) => { + LabelledInstruction::TypeHint(type_hint.to_owned()) + } } } } @@ -94,7 +105,7 @@ fn pretty_print_error(s: &str, mut e: VerboseError<&str>) -> String { ) { e.errors.remove(0); } - convert_error(s, e) + nom::error::convert_error(s, e) } /// Parse a program @@ -185,7 +196,7 @@ type ParseResult<'input, Out> = IResult<&'input str, Out, VerboseError<&'input s pub fn tokenize(s: &str) -> ParseResult> { let (s, _) = comment_or_whitespace0(s)?; let (s, instructions) = many0(alt((label, labelled_instruction, breakpoint, type_hint)))(s)?; - let (s, _) = context("expecting label, instruction or eof", eof)(s)?; + let (s, _) = nom::error::context("expecting label, instruction or eof", eof)(s)?; Ok((s, instructions)) } @@ -204,7 +215,10 @@ fn label(label_s: &str) -> ParseResult { // `cut` will reject the alternative parser of `label`, being `labelled_instruction`, which // *is* allowed to contain valid instruction names. if is_instruction_name(&addr) { - return cut(context("label cannot be named after instruction", fail))(label_s); + return cut(nom::error::context( + "label cannot be named after instruction", + fail, + ))(label_s); } Ok((s, InstructionToken::Label(addr, label_s))) @@ -411,7 +425,10 @@ fn call_instruction<'a>() -> impl Fn(&'a str) -> ParseResult:` and `call