From b02779c853e5733bf92d772ef91f34567388ade2 Mon Sep 17 00:00:00 2001 From: Jan Ferdinand Sauer Date: Thu, 9 Feb 2023 02:29:35 +0100 Subject: [PATCH] simplify handling of challenges Fix #90. --- constraint-evaluation-generator/src/main.rs | 57 +- triton-vm/src/stark.rs | 42 +- triton-vm/src/table/challenges.rs | 413 ++--- triton-vm/src/table/constraint_circuit.rs | 193 +- triton-vm/src/table/cross_table_argument.rs | 101 +- triton-vm/src/table/extension_table.rs | 18 +- triton-vm/src/table/hash_table.rs | 198 +- triton-vm/src/table/jump_stack_table.rs | 151 +- triton-vm/src/table/master_table.rs | 38 +- triton-vm/src/table/op_stack_table.rs | 144 +- triton-vm/src/table/processor_table.rs | 1821 ++++--------------- triton-vm/src/table/program_table.rs | 108 +- triton-vm/src/table/ram_table.rs | 166 +- triton-vm/src/table/u32_table.rs | 124 +- 14 files changed, 964 insertions(+), 2610 deletions(-) diff --git a/constraint-evaluation-generator/src/main.rs b/constraint-evaluation-generator/src/main.rs index 1caffb85a..134120d38 100644 --- a/constraint-evaluation-generator/src/main.rs +++ b/constraint-evaluation-generator/src/main.rs @@ -5,7 +5,6 @@ use itertools::Itertools; use twenty_first::shared_math::b_field_element::BFieldElement; use twenty_first::shared_math::x_field_element::XFieldElement; -use triton_vm::table::challenges::TableChallenges; use triton_vm::table::constraint_circuit::CircuitExpression; use triton_vm::table::constraint_circuit::ConstraintCircuit; use triton_vm::table::constraint_circuit::InputIndicator; @@ -124,15 +123,14 @@ fn write(table_name_snake: &str, rust_source_code: String) { std::fs::write(output_filename, rust_source_code).expect("Write Rust source code"); } -fn gen( +fn gen( table_name_snake: &str, table_id_name: &str, - initial_constraint_circuits: &mut [ConstraintCircuit], - consistency_constraint_circuits: &mut [ConstraintCircuit], - transition_constraint_circuits: &mut [ConstraintCircuit], - terminal_constraint_circuits: &mut [ConstraintCircuit], + initial_constraint_circuits: &mut [ConstraintCircuit], + consistency_constraint_circuits: &mut [ConstraintCircuit], + transition_constraint_circuits: &mut [ConstraintCircuit], + terminal_constraint_circuits: &mut [ConstraintCircuit], ) -> String { - let challenge_enum_name = format!("{table_id_name}ChallengeId"); let table_mod_name = format!("Ext{table_id_name}"); let num_initial_constraints = initial_constraint_circuits.len(); @@ -161,12 +159,11 @@ use twenty_first::shared_math::b_field_element::BFieldElement; use twenty_first::shared_math::mpolynomial::Degree; use twenty_first::shared_math::x_field_element::XFieldElement; -use crate::table::challenges::AllChallenges; -use crate::table::challenges::TableChallenges; +use crate::table::challenges::Challenges; +use crate::table::challenges::ChallengeId::*; use crate::table::extension_table::Evaluable; use crate::table::extension_table::Quotientable; use crate::table::{table_name_snake}::{table_mod_name}; -use crate::table::{table_name_snake}::{challenge_enum_name}::*; // This file has been auto-generated. Any modifications _will_ be lost. // To re-generate, execute: @@ -177,9 +174,8 @@ impl Evaluable for {table_mod_name} {{ fn evaluate_initial_constraints( base_row: ArrayView1, ext_row: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) -> Vec {{ - let challenges = &challenges.{table_name_snake}_challenges; {initial_constraint_strings} }} @@ -188,9 +184,8 @@ impl Evaluable for {table_mod_name} {{ fn evaluate_consistency_constraints( base_row: ArrayView1, ext_row: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) -> Vec {{ - let challenges = &challenges.{table_name_snake}_challenges; {consistency_constraint_strings} }} @@ -201,9 +196,8 @@ impl Evaluable for {table_mod_name} {{ current_ext_row: ArrayView1, next_base_row: ArrayView1, next_ext_row: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) -> Vec {{ - let challenges = &challenges.{table_name_snake}_challenges; {transition_constraint_strings} }} @@ -212,9 +206,8 @@ impl Evaluable for {table_mod_name} {{ fn evaluate_terminal_constraints( base_row: ArrayView1, ext_row: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) -> Vec {{ - let challenges = &challenges.{table_name_snake}_challenges; {terminal_constraint_strings} }} }} @@ -274,8 +267,8 @@ impl Quotientable for {table_mod_name} {{ ) } -fn turn_circuits_into_degree_bounds_string( - constraint_circuits: &[ConstraintCircuit], +fn turn_circuits_into_degree_bounds_string( + constraint_circuits: &[ConstraintCircuit], ) -> String { constraint_circuits .iter() @@ -284,8 +277,8 @@ fn turn_circuits_into_degree_bounds_string( - constraint_circuits: &mut [ConstraintCircuit], +fn turn_circuits_into_string( + constraint_circuits: &mut [ConstraintCircuit], ) -> String { // Delete redundant nodes ConstraintCircuit::constant_folding(&mut constraint_circuits.iter_mut().collect_vec()); @@ -356,9 +349,9 @@ fn turn_circuits_into_string( /// Produce the code to evaluate code for all nodes that share a value number of /// times visited. A value for all nodes with a higher count than the provided are assumed /// to be in scope. -fn declare_nodes_with_visit_count( +fn declare_nodes_with_visit_count( requested_visited_count: usize, - circuits: &[ConstraintCircuit], + circuits: &[ConstraintCircuit], ) -> String { let mut in_scope: HashSet = HashSet::new(); let mut output = String::default(); @@ -375,9 +368,9 @@ fn declare_nodes_with_visit_count( output } -fn declare_single_node_with_visit_count( +fn declare_single_node_with_visit_count( requested_visited_count: usize, - circuit: &ConstraintCircuit, + circuit: &ConstraintCircuit, in_scope: &mut HashSet, output: &mut String, ) { @@ -433,9 +426,7 @@ fn declare_single_node_with_visit_count( /// Return a variable name for the node. Returns `point[n]` if node is just /// a value from the codewords. Otherwise returns the ID of the circuit. -fn get_binding_name( - circuit: &ConstraintCircuit, -) -> String { +fn get_binding_name(circuit: &ConstraintCircuit) -> String { match &circuit.expression { CircuitExpression::XConstant(xfe) => print_xfe(xfe), CircuitExpression::BConstant(bfe) => print_bfe(bfe), @@ -450,9 +441,7 @@ fn get_binding_name( /// Recursively check whether a node is composed of only BFieldElements, i.e., only uses /// (1) inputs from base rows, (2) constants from the B-field, and (3) binary operations on /// BFieldElements. -fn is_bfield_element( - circuit: &ConstraintCircuit, -) -> bool { +fn is_bfield_element(circuit: &ConstraintCircuit) -> bool { match &circuit.expression { CircuitExpression::XConstant(_) => false, CircuitExpression::BConstant(_) => true, @@ -466,9 +455,9 @@ fn is_bfield_element( /// Return (1) the code for evaluating a single node and (2) a list of symbols that this evaluation /// depends on. -fn evaluate_single_node( +fn evaluate_single_node( requested_visited_count: usize, - circuit: &ConstraintCircuit, + circuit: &ConstraintCircuit, in_scope: &HashSet, ) -> (String, Vec) { let mut output = String::default(); diff --git a/triton-vm/src/stark.rs b/triton-vm/src/stark.rs index 84bdf37ad..04548e8cb 100644 --- a/triton-vm/src/stark.rs +++ b/triton-vm/src/stark.rs @@ -41,7 +41,7 @@ use crate::proof::Claim; use crate::proof::Proof; use crate::proof_item::ProofItem; use crate::proof_stream::ProofStream; -use crate::table::challenges::AllChallenges; +use crate::table::challenges::Challenges; use crate::table::master_table::*; use crate::vm::AlgebraicExecutionTrace; @@ -180,13 +180,10 @@ impl Stark { proof_stream.enqueue(&ProofItem::MerkleRoot(base_merkle_tree_root)); let extension_weights = Self::sample_weights( proof_stream.prover_fiat_shamir(), - AllChallenges::TOTAL_CHALLENGES, - ); - let extension_challenges = AllChallenges::create_challenges( - extension_weights, - &self.claim.input, - &self.claim.output, + Challenges::num_challenges_to_sample(), ); + let extension_challenges = + Challenges::new(extension_weights, &self.claim.input, &self.claim.output); prof_stop!(maybe_profiler, "Fiat-Shamir"); prof_start!(maybe_profiler, "extend"); @@ -537,9 +534,11 @@ impl Stark { let base_merkle_tree_root = proof_stream.dequeue()?.as_merkle_root()?; let extension_challenge_seed = proof_stream.verifier_fiat_shamir(); - let extension_challenge_weights = - Self::sample_weights(extension_challenge_seed, AllChallenges::TOTAL_CHALLENGES); - let challenges = AllChallenges::create_challenges( + let extension_challenge_weights = Self::sample_weights( + extension_challenge_seed, + Challenges::num_challenges_to_sample(), + ); + let challenges = Challenges::new( extension_challenge_weights, &self.claim.input, &self.claim.output, @@ -872,11 +871,14 @@ pub(crate) mod triton_stark_tests { use num_traits::Zero; use rand::prelude::ThreadRng; use rand_core::RngCore; - use triton_opcodes::instruction::AnInstruction; use triton_opcodes::program::Program; use crate::shared_tests::*; + use crate::table::challenges::ChallengeId::StandardInputIndeterminate; + use crate::table::challenges::ChallengeId::StandardInputTerminal; + use crate::table::challenges::ChallengeId::StandardOutputIndeterminate; + use crate::table::challenges::ChallengeId::StandardOutputTerminal; use crate::table::cross_table_argument::CrossTableArg; use crate::table::cross_table_argument::EvalArg; use crate::table::cross_table_argument::GrandCrossTableArg; @@ -964,12 +966,12 @@ pub(crate) mod triton_stark_tests { MasterBaseTable, MasterBaseTable, MasterExtTable, - AllChallenges, + Challenges, ) { let (stark, unpadded_master_base_table, master_base_table) = parse_simulate_pad(code, stdin, secret_in); - let dummy_challenges = AllChallenges::placeholder(&stark.claim.input, &stark.claim.output); + let dummy_challenges = Challenges::placeholder(&stark.claim.input, &stark.claim.output); let master_ext_table = master_base_table.extend( &dummy_challenges, stark.parameters.num_randomizer_polynomials, @@ -1106,7 +1108,7 @@ pub(crate) mod triton_stark_tests { let ine = EvalArg::compute_terminal( &stark.claim.input, EvalArg::default_initial(), - all_challenges.input_challenges.processor_eval_indeterminate, + all_challenges.get_challenge(StandardInputIndeterminate), ); assert_eq!(ptie, ine, "The input evaluation arguments do not match."); @@ -1114,9 +1116,7 @@ pub(crate) mod triton_stark_tests { let oute = EvalArg::compute_terminal( &stark.claim.output, EvalArg::default_initial(), - all_challenges - .output_challenges - .processor_eval_indeterminate, + all_challenges.get_challenge(StandardOutputIndeterminate), ); assert_eq!(ptoe, oute, "The output evaluation arguments do not match."); } @@ -1137,12 +1137,12 @@ pub(crate) mod triton_stark_tests { let processor_table = master_ext_table.table(ProcessorTable); let processor_table_last_row = processor_table.slice(s![-1, ..]); assert_eq!( - all_challenges.cross_table_challenges.input_terminal, + all_challenges.get_challenge(StandardInputTerminal), processor_table_last_row[InputTableEvalArg.ext_table_index()], "The input terminal must match for TASM snippet #{code_idx}." ); assert_eq!( - all_challenges.cross_table_challenges.output_terminal, + all_challenges.get_challenge(StandardOutputTerminal), processor_table_last_row[OutputTableEvalArg.ext_table_index()], "The output terminal must match for TASM snippet #{code_idx}." ); @@ -1170,7 +1170,7 @@ pub(crate) mod triton_stark_tests { #[test] fn constraint_polynomials_use_right_variable_count_test() { - let challenges = AllChallenges::placeholder(&[], &[]); + let challenges = Challenges::placeholder(&[], &[]); let base_row = Array1::zeros(NUM_BASE_COLUMNS); let ext_row = Array1::zeros(NUM_EXT_COLUMNS); @@ -1294,7 +1294,7 @@ pub(crate) mod triton_stark_tests { fn number_of_quotient_degree_bounds_match_number_of_constraints_test() { let base_row = Array1::zeros(NUM_BASE_COLUMNS); let ext_row = Array1::zeros(NUM_EXT_COLUMNS); - let challenges = AllChallenges::placeholder(&[], &[]); + let challenges = Challenges::placeholder(&[], &[]); let padded_height = 2; let num_trace_randomizers = 2; let interpolant_degree = interpolant_degree(padded_height, num_trace_randomizers); diff --git a/triton-vm/src/table/challenges.rs b/triton-vm/src/table/challenges.rs index 96e6f6378..62187153d 100644 --- a/triton-vm/src/table/challenges.rs +++ b/triton-vm/src/table/challenges.rs @@ -1,257 +1,218 @@ +//! Challenges are needed for the cross-table arguments, _i.e._, Permutation Arguments, Evaluation +//! Arguments, and Lookup Arguments, as well as for the RAM Table's Contiguity Argument. +//! +//! There are three types of challenges: +//! - **Weights**. Weights are used to non-linearly combine multiple elements into one element. The +//! resulting single element can then be used in a cross-table argument. +//! - **Indeterminates**. All cross-table arguments work by checking the equality of polynomials (or +//! rational functions). Through the Schwartz-Zippel lemma, this equality check can be performed +//! by evaluating the polynomials (or rational functions) in a single point. The challenges that +//! are indeterminates are exactly this evaluation point. The polynomials (or rational functions) +//! are never stored explicitly. Instead, they are directly evaluated at the point indicated by a +//! challenge of “type” `Indeterminate`, giving rise to “running products”, “running +//! evaluations”, _et cetera_. +//! - **Terminals**. The public input (respectively output) of the program is not stored in any +//! table. Instead, the terminal of the Evaluation Argument is computed directly from the +//! public input (respectively output) and the indeterminate. + use std::fmt::Debug; -use std::fmt::Display; use std::hash::Hash; use strum::EnumCount; -use strum::IntoEnumIterator; +use strum_macros::Display; +use strum_macros::EnumCount as EnumCountMacro; +use strum_macros::EnumIter; use twenty_first::shared_math::b_field_element::BFieldElement; use twenty_first::shared_math::other::random_elements; use twenty_first::shared_math::x_field_element::XFieldElement; +use crate::table::challenges::ChallengeId::*; use crate::table::cross_table_argument::CrossTableArg; -use crate::table::cross_table_argument::CrossTableChallenges; use crate::table::cross_table_argument::EvalArg; -use crate::table::cross_table_argument::NUM_CROSS_TABLE_WEIGHTS; -use crate::table::hash_table::HashTableChallenges; -use crate::table::jump_stack_table::JumpStackTableChallenges; -use crate::table::op_stack_table::OpStackTableChallenges; -use crate::table::processor_table::IOChallenges; -use crate::table::processor_table::ProcessorTableChallenges; -use crate::table::program_table::ProgramTableChallenges; -use crate::table::ram_table::RamTableChallenges; -use crate::table::u32_table::U32TableChallenges; - -pub trait TableChallenges: Clone + Debug { - type Id: Display - + Clone - + Copy - + Debug - + EnumCount - + IntoEnumIterator - + Into - + PartialEq - + Hash; - - fn count() -> usize { - Self::Id::COUNT - } - fn get_challenge(&self, id: Self::Id) -> XFieldElement; +/// A `ChallengeId` is a unique, symbolic identifier for a challenge used in Triton VM. The +/// `ChallengeId` enum works in tandem with the struct `Challenges`, which can be +/// instantiated to hold actual challenges that can be indexed by some `ChallengeId`. +/// +/// Since almost all challenges relate to the Processor Table in some form, the words “Processor +/// Table” are usually omitted from the `ChallengeId`'s name. +#[repr(usize)] +#[derive(Display, Debug, Clone, Copy, PartialEq, Eq, EnumIter, EnumCountMacro, Hash)] +pub enum ChallengeId { + /// The indeterminate for the Evaluation Argument with standard input. + StandardInputIndeterminate, + + /// The indeterminate for the Evaluation Argument with standard output. + StandardOutputIndeterminate, + + /// The indeterminate for the instruction Lookup Argument between the Processor Table and the + /// Program Table guaranteeing that the instructions and their arguments are copied + /// correctly. + InstructionLookupIndeterminate, + + HashInputIndeterminate, + HashDigestIndeterminate, + SpongeIndeterminate, + + OpStackIndeterminate, + RamIndeterminate, + JumpStackIndeterminate, + + U32Indeterminate, + + /// The indeterminate for the Lookup Argument between the Processor Table and all memory-like + /// tables, _i.e._, the OpStack Table, the Ram Table, and the JumpStack Table, guaranteeing + /// that all clock jump differences are directed forward. + ClockJumpDifferenceLookupIndeterminate, + + /// The indeterminate for the Contiguity Argument within the Ram Table. + RamTableBezoutRelationIndeterminate, + + /// A weight for non-linearly combining multiple elements. Applies to + /// - `Address` in the Program Table + /// - `IP` in the Processor Table + ProgramAddressWeight, + + /// A weight for non-linearly combining multiple elements. Applies to + /// - `Instruction` in the Program Table + /// - `CI` in the Processor Table + ProgramInstructionWeight, + + /// A weight for non-linearly combining multiple elements. Applies to + /// - `Instruction'` (_i.e._, in the next row) in the Program Table + /// - `NIA` in the Processor Table + ProgramNextInstructionWeight, + + OpStackClkWeight, + OpStackIb1Weight, + OpStackOspWeight, + OpStackOsvWeight, + + RamClkWeight, + RamRampWeight, + RamRamvWeight, + RamPreviousInstructionWeight, + + JumpStackClkWeight, + JumpStackCiWeight, + JumpStackJspWeight, + JumpStackJsoWeight, + JumpStackJsdWeight, + + HashCIWeight, + HashStateWeight0, + HashStateWeight1, + HashStateWeight2, + HashStateWeight3, + HashStateWeight4, + HashStateWeight5, + HashStateWeight6, + HashStateWeight7, + HashStateWeight8, + HashStateWeight9, + HashStateWeight10, + HashStateWeight11, + HashStateWeight12, + HashStateWeight13, + HashStateWeight14, + HashStateWeight15, + + U32LhsWeight, + U32RhsWeight, + U32CiWeight, + U32ResultWeight, + + ProcessorToProgramWeight, + InputToProcessorWeight, + ProcessorToOutputWeight, + ProcessorToOpStackWeight, + ProcessorToRamWeight, + ProcessorToJumpStackWeight, + HashInputWeight, + HashDigestWeight, + SpongeWeight, + ProcessorToU32Weight, + ClockJumpDifferenceLookupWeight, + + /// The terminal for the Evaluation Argument with standard input. + StandardInputTerminal, + + /// The terminal for the Evaluation Argument with standard output. + StandardOutputTerminal, +} - fn to_vec(&self) -> Vec { - Self::Id::iter().map(|id| self.get_challenge(id)).collect() +impl ChallengeId { + pub fn index(&self) -> usize { + *self as usize } } -#[derive(Debug, Clone)] -pub struct AllChallenges { - pub program_table_challenges: ProgramTableChallenges, - pub input_challenges: IOChallenges, - pub output_challenges: IOChallenges, - pub processor_table_challenges: ProcessorTableChallenges, - pub op_stack_table_challenges: OpStackTableChallenges, - pub ram_table_challenges: RamTableChallenges, - pub jump_stack_table_challenges: JumpStackTableChallenges, - pub hash_table_challenges: HashTableChallenges, - pub u32_table_challenges: U32TableChallenges, - pub cross_table_challenges: CrossTableChallenges, +/// The `Challenges` struct holds the challenges used in Triton VM. The concrete challenges are +/// known only at runtime. The challenges are indexed using enum `ChallengeId`. The `Challenges` +/// struct is essentially a thin wrapper around an array of `XFieldElement`s, providing +/// convenience methods. +pub struct Challenges { + pub challenges: [XFieldElement; Self::count()], } -impl AllChallenges { - pub const TOTAL_CHALLENGES: usize = 45 + NUM_CROSS_TABLE_WEIGHTS; +impl Challenges { + pub const fn count() -> usize { + ChallengeId::COUNT + } + + /// The number of weights to sample using the Fiat-Shamir heuristic. This number is lower + /// than the number of challenges: the input terminal and output terminal are not sampled but + /// computed from the public input and output. + pub const fn num_challenges_to_sample() -> usize { + Self::count() - 2 + } - pub fn create_challenges( - mut weights: Vec, - claimed_input: &[BFieldElement], - claimed_output: &[BFieldElement], + pub fn new( + mut challenges: Vec, + public_input: &[BFieldElement], + public_output: &[BFieldElement], ) -> Self { - let processor_table_challenges = ProcessorTableChallenges { - standard_input_eval_indeterminate: weights.pop().unwrap(), - standard_output_eval_indeterminate: weights.pop().unwrap(), - hash_input_eval_indeterminate: weights.pop().unwrap(), - hash_digest_eval_indeterminate: weights.pop().unwrap(), - sponge_eval_indeterminate: weights.pop().unwrap(), - instruction_lookup_indeterminate: weights.pop().unwrap(), - op_stack_perm_indeterminate: weights.pop().unwrap(), - ram_perm_indeterminate: weights.pop().unwrap(), - jump_stack_perm_indeterminate: weights.pop().unwrap(), - - program_table_ip_weight: weights.pop().unwrap(), - program_table_ci_processor_weight: weights.pop().unwrap(), - program_table_nia_weight: weights.pop().unwrap(), - - op_stack_table_clk_weight: weights.pop().unwrap(), - op_stack_table_ib1_weight: weights.pop().unwrap(), - op_stack_table_osp_weight: weights.pop().unwrap(), - op_stack_table_osv_weight: weights.pop().unwrap(), - - ram_table_clk_weight: weights.pop().unwrap(), - ram_table_ramp_weight: weights.pop().unwrap(), - ram_table_ramv_weight: weights.pop().unwrap(), - ram_table_previous_instruction_weight: weights.pop().unwrap(), - - jump_stack_table_clk_weight: weights.pop().unwrap(), - jump_stack_table_ci_weight: weights.pop().unwrap(), - jump_stack_table_jsp_weight: weights.pop().unwrap(), - jump_stack_table_jso_weight: weights.pop().unwrap(), - jump_stack_table_jsd_weight: weights.pop().unwrap(), - - clock_jump_difference_lookup_indeterminate: weights.pop().unwrap(), - - hash_table_ci_weight: weights.pop().unwrap(), - hash_state_weight0: weights.pop().unwrap(), - hash_state_weight1: weights.pop().unwrap(), - hash_state_weight2: weights.pop().unwrap(), - hash_state_weight3: weights.pop().unwrap(), - hash_state_weight4: weights.pop().unwrap(), - hash_state_weight5: weights.pop().unwrap(), - hash_state_weight6: weights.pop().unwrap(), - hash_state_weight7: weights.pop().unwrap(), - hash_state_weight8: weights.pop().unwrap(), - hash_state_weight9: weights.pop().unwrap(), - - u32_table_lhs_weight: weights.pop().unwrap(), - u32_table_rhs_weight: weights.pop().unwrap(), - u32_table_ci_weight: weights.pop().unwrap(), - u32_table_result_weight: weights.pop().unwrap(), - - u32_table_perm_indeterminate: weights.pop().unwrap(), - }; - - let program_table_challenges = ProgramTableChallenges { - instruction_lookup_indeterminate: processor_table_challenges - .instruction_lookup_indeterminate, - address_weight: processor_table_challenges.program_table_ip_weight, - instruction_weight: processor_table_challenges.program_table_ci_processor_weight, - next_instruction_weight: processor_table_challenges.program_table_nia_weight, - }; - - let input_challenges = IOChallenges { - processor_eval_indeterminate: processor_table_challenges - .standard_input_eval_indeterminate, - }; - - let output_challenges = IOChallenges { - processor_eval_indeterminate: processor_table_challenges - .standard_output_eval_indeterminate, - }; - - let op_stack_table_challenges = OpStackTableChallenges { - processor_perm_indeterminate: processor_table_challenges.op_stack_perm_indeterminate, - clk_weight: processor_table_challenges.op_stack_table_clk_weight, - ib1_weight: processor_table_challenges.op_stack_table_ib1_weight, - osv_weight: processor_table_challenges.op_stack_table_osv_weight, - osp_weight: processor_table_challenges.op_stack_table_osp_weight, - clock_jump_difference_lookup_indeterminate: processor_table_challenges - .clock_jump_difference_lookup_indeterminate, - }; - - let ram_table_challenges = RamTableChallenges { - bezout_relation_indeterminate: weights.pop().unwrap(), - processor_perm_indeterminate: processor_table_challenges.ram_perm_indeterminate, - clk_weight: processor_table_challenges.ram_table_clk_weight, - ramp_weight: processor_table_challenges.ram_table_ramp_weight, - ramv_weight: processor_table_challenges.ram_table_ramv_weight, - previous_instruction_weight: processor_table_challenges - .ram_table_previous_instruction_weight, - clock_jump_difference_lookup_indeterminate: processor_table_challenges - .clock_jump_difference_lookup_indeterminate, - }; - - let jump_stack_table_challenges = JumpStackTableChallenges { - processor_perm_indeterminate: processor_table_challenges.jump_stack_perm_indeterminate, - clk_weight: processor_table_challenges.jump_stack_table_clk_weight, - ci_weight: processor_table_challenges.jump_stack_table_ci_weight, - jsp_weight: processor_table_challenges.jump_stack_table_jsp_weight, - jso_weight: processor_table_challenges.jump_stack_table_jso_weight, - jsd_weight: processor_table_challenges.jump_stack_table_jsd_weight, - clock_jump_difference_lookup_indeterminate: processor_table_challenges - .clock_jump_difference_lookup_indeterminate, - }; - - let hash_table_challenges = HashTableChallenges { - hash_input_eval_indeterminate: processor_table_challenges.hash_input_eval_indeterminate, - hash_digest_eval_indeterminate: processor_table_challenges - .hash_digest_eval_indeterminate, - sponge_eval_indeterminate: processor_table_challenges.sponge_eval_indeterminate, - - ci_weight: processor_table_challenges.hash_table_ci_weight, - hash_state_weight0: processor_table_challenges.hash_state_weight0, - hash_state_weight1: processor_table_challenges.hash_state_weight1, - hash_state_weight2: processor_table_challenges.hash_state_weight2, - hash_state_weight3: processor_table_challenges.hash_state_weight3, - hash_state_weight4: processor_table_challenges.hash_state_weight4, - hash_state_weight5: processor_table_challenges.hash_state_weight5, - hash_state_weight6: processor_table_challenges.hash_state_weight6, - hash_state_weight7: processor_table_challenges.hash_state_weight7, - hash_state_weight8: processor_table_challenges.hash_state_weight8, - hash_state_weight9: processor_table_challenges.hash_state_weight9, - hash_state_weight10: weights.pop().unwrap(), - hash_state_weight11: weights.pop().unwrap(), - hash_state_weight12: weights.pop().unwrap(), - hash_state_weight13: weights.pop().unwrap(), - hash_state_weight14: weights.pop().unwrap(), - hash_state_weight15: weights.pop().unwrap(), - }; - - let u32_table_challenges = U32TableChallenges { - lhs_weight: processor_table_challenges.u32_table_lhs_weight, - rhs_weight: processor_table_challenges.u32_table_rhs_weight, - ci_weight: processor_table_challenges.u32_table_ci_weight, - result_weight: processor_table_challenges.u32_table_result_weight, - processor_perm_indeterminate: processor_table_challenges.u32_table_perm_indeterminate, - }; + assert_eq!(challenges.len(), Self::num_challenges_to_sample()); + + // The terminals are computed from the public input and output, and the indeterminates. + // Then, the terminals are inserted into the challenges vector. + // The indeterminates' positions must not change after they have been used for the first + // time. Therefore, the insertion index of the terminals must be greater than the index of + // the indeterminates. + assert!(StandardInputIndeterminate.index() < StandardInputTerminal.index()); + assert!(StandardInputIndeterminate.index() < StandardOutputTerminal.index()); + + assert!(StandardOutputIndeterminate.index() < StandardInputTerminal.index()); + assert!(StandardOutputIndeterminate.index() < StandardOutputTerminal.index()); let input_terminal = EvalArg::compute_terminal( - claimed_input, + public_input, EvalArg::default_initial(), - processor_table_challenges.standard_input_eval_indeterminate, + challenges[StandardInputIndeterminate.index()], ); let output_terminal = EvalArg::compute_terminal( - claimed_output, + public_output, EvalArg::default_initial(), - processor_table_challenges.standard_output_eval_indeterminate, + challenges[StandardOutputIndeterminate.index()], ); - let cross_table_challenges = CrossTableChallenges { - input_terminal, - output_terminal, - processor_to_program_weight: weights.pop().unwrap(), - processor_to_op_stack_weight: weights.pop().unwrap(), - processor_to_ram_weight: weights.pop().unwrap(), - processor_to_jump_stack_weight: weights.pop().unwrap(), - hash_input_weight: weights.pop().unwrap(), - hash_digest_weight: weights.pop().unwrap(), - sponge_weight: weights.pop().unwrap(), - processor_to_u32_weight: weights.pop().unwrap(), - clock_jump_difference_lookup_weight: weights.pop().unwrap(), - input_to_processor_weight: weights.pop().unwrap(), - processor_to_output_weight: weights.pop().unwrap(), - }; - - assert!(weights.is_empty(), "{} weights left unused.", weights.len()); - - AllChallenges { - program_table_challenges, - input_challenges, - output_challenges, - processor_table_challenges, - op_stack_table_challenges, - ram_table_challenges, - jump_stack_table_challenges, - hash_table_challenges, - u32_table_challenges, - cross_table_challenges, - } + challenges.insert(StandardInputTerminal.index(), input_terminal); + challenges.insert(StandardOutputTerminal.index(), output_terminal); + assert_eq!(challenges.len(), Self::count()); + let challenges = challenges.try_into().unwrap(); + + Self { challenges } + } + + /// Stand-in challenges. Can be used in tests. For non-interactive STARKs, use the + /// Fiat-Shamir heuristic to derive the actual challenges. + pub fn placeholder(public_input: &[BFieldElement], public_output: &[BFieldElement]) -> Self { + let stand_in_challenges = random_elements(Self::num_challenges_to_sample()); + Self::new(stand_in_challenges, public_input, public_output) } - /// Stand-in challenges. Can be used in tests. For non-interactive STARKs, use Fiat-Shamir to - /// derive the actual challenges. - pub fn placeholder(claimed_input: &[BFieldElement], claimed_output: &[BFieldElement]) -> Self { - Self::create_challenges( - random_elements(Self::TOTAL_CHALLENGES), - claimed_input, - claimed_output, - ) + #[inline(always)] + pub fn get_challenge(&self, id: ChallengeId) -> XFieldElement { + self.challenges[id.index()] } } diff --git a/triton-vm/src/table/constraint_circuit.rs b/triton-vm/src/table/constraint_circuit.rs index ef24482e6..5874e3e14 100644 --- a/triton-vm/src/table/constraint_circuit.rs +++ b/triton-vm/src/table/constraint_circuit.rs @@ -1,4 +1,3 @@ -use ndarray::ArrayView2; use std::borrow::BorrowMut; use std::cell::RefCell; use std::cmp; @@ -7,12 +6,12 @@ use std::fmt::Debug; use std::fmt::Display; use std::hash::Hash; use std::iter::Sum; -use std::marker::PhantomData; use std::ops::Add; use std::ops::Mul; use std::ops::Sub; use std::rc::Rc; +use ndarray::ArrayView2; use num_traits::One; use num_traits::Zero; use twenty_first::shared_math::b_field_element::BFieldElement; @@ -21,7 +20,8 @@ use twenty_first::shared_math::x_field_element::XFieldElement; use CircuitExpression::*; -use super::challenges::TableChallenges; +use crate::table::challenges::ChallengeId; +use crate::table::challenges::Challenges; #[derive(Debug, Clone, Copy, PartialEq, Hash)] pub enum BinOp { @@ -197,19 +197,19 @@ impl InputIndicat } #[derive(Debug, Clone)] -pub enum CircuitExpression { +pub enum CircuitExpression { XConstant(XFieldElement), BConstant(BFieldElement), Input(II), - Challenge(T::Id), + Challenge(ChallengeId), BinaryOperation( BinOp, - Rc>>, - Rc>>, + Rc>>, + Rc>>, ), } -impl Hash for CircuitExpression { +impl Hash for CircuitExpression { fn hash(&self, state: &mut H) { match self { BConstant(bfe) => bfe.hash(state), @@ -227,28 +227,28 @@ impl Hash for CircuitExpression { } } -impl Hash for ConstraintCircuit { +impl Hash for ConstraintCircuit { fn hash(&self, state: &mut H) { self.expression.hash(state) } } -impl Hash for ConstraintCircuitMonad { +impl Hash for ConstraintCircuitMonad { fn hash(&self, state: &mut H) { self.circuit.as_ref().borrow().expression.hash(state) } } #[derive(Clone, Debug)] -pub struct ConstraintCircuit { +pub struct ConstraintCircuit { pub id: usize, pub visited_counter: usize, - pub expression: CircuitExpression, + pub expression: CircuitExpression, } -impl Eq for ConstraintCircuit {} +impl Eq for ConstraintCircuit {} -impl PartialEq for ConstraintCircuit { +impl PartialEq for ConstraintCircuit { /// Calculate equality of circuits. /// In particular, this function does *not* attempt to simplify /// or reduce neutral terms or products. So this comparison will @@ -288,7 +288,7 @@ impl PartialEq for ConstraintCircuit Display for ConstraintCircuit { +impl Display for ConstraintCircuit { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match &self.expression { XConstant(xfe) => { @@ -314,7 +314,7 @@ impl Display for ConstraintCircuit ConstraintCircuit { +impl ConstraintCircuit { /// Increment `visited_counter` by one for each reachable node fn traverse_single(&mut self) { self.visited_counter += 1; @@ -327,7 +327,7 @@ impl ConstraintCircuit { /// Count how many times each reachable node is reached when traversing from /// the starting points that are given as input. The result is stored in the /// `visited_counter` field in each node. - pub fn traverse_multiple(ccs: &mut [ConstraintCircuit]) { + pub fn traverse_multiple(ccs: &mut [ConstraintCircuit]) { for cc in ccs.iter_mut() { assert!( cc.visited_counter.is_zero(), @@ -363,7 +363,7 @@ impl ConstraintCircuit { } /// Verify that a multitree has unique IDs. Panics otherwise. - pub fn assert_has_unique_ids(constraints: &mut [ConstraintCircuit]) { + pub fn assert_has_unique_ids(constraints: &mut [ConstraintCircuit]) { let mut ids: HashSet = HashSet::new(); for circuit in constraints.iter_mut() { @@ -475,7 +475,7 @@ impl ConstraintCircuit { } /// Reduce size of multitree by simplifying constant expressions such as `1·X` to `X`. - pub fn constant_folding(circuits: &mut [&mut ConstraintCircuit]) { + pub fn constant_folding(circuits: &mut [&mut ConstraintCircuit]) { for circuit in circuits.iter_mut() { let mut mutated = circuit.constant_fold_inner(); while mutated { @@ -627,7 +627,7 @@ impl ConstraintCircuit { } /// Replace all challenges with constants in subtree - fn apply_challenges_to_one_root(&mut self, challenges: &T) { + fn apply_challenges_to_one_root(&mut self, challenges: &Challenges) { match &self.expression { Challenge(challenge_id) => { *self.expression.borrow_mut() = XConstant(challenges.get_challenge(*challenge_id)) @@ -645,7 +645,7 @@ impl ConstraintCircuit { } /// Simplify the circuit constraints by replacing the known challenges with roots - pub fn apply_challenges(constraints: &mut [ConstraintCircuit], challenges: &T) { + pub fn apply_challenges(constraints: &mut [ConstraintCircuit], challenges: &Challenges) { for circuit in constraints.iter_mut() { circuit.apply_challenges_to_one_root(challenges); } @@ -677,7 +677,7 @@ impl ConstraintCircuit { &self, base_table: ArrayView2, ext_table: ArrayView2, - challenges: &T, + challenges: &Challenges, ) -> XFieldElement { let mut self_to_evaluate = self.clone(); self_to_evaluate.apply_challenges_to_one_root(challenges); @@ -686,13 +686,13 @@ impl ConstraintCircuit { } #[derive(Clone)] -pub struct ConstraintCircuitMonad { - pub circuit: Rc>>, - pub all_nodes: Rc>>>, +pub struct ConstraintCircuitMonad { + pub circuit: Rc>>, + pub all_nodes: Rc>>>, pub id_counter_ref: Rc>, } -impl Debug for ConstraintCircuitMonad { +impl Debug for ConstraintCircuitMonad { // We cannot derive `Debug` as `all_nodes` contains itself which a derived `Debug` will // attempt to print as well, thus leading to infinite recursion. fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { @@ -710,13 +710,13 @@ impl Debug for ConstraintCircuitMonad Display for ConstraintCircuitMonad { +impl Display for ConstraintCircuitMonad { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!(f, "{}", self.circuit.as_ref().borrow()) } } -impl PartialEq for ConstraintCircuitMonad { +impl PartialEq for ConstraintCircuitMonad { // Equality for the ConstraintCircuitMonad is defined by the circuit, not the // other metadata (e.g. ID) that it carries around. fn eq(&self, other: &Self) -> bool { @@ -724,16 +724,16 @@ impl PartialEq for ConstraintCircuitMona } } -impl Eq for ConstraintCircuitMonad {} +impl Eq for ConstraintCircuitMonad {} /// Helper function for binary operations that are used to generate new parent /// nodes in the multitree that represents the algebraic circuit. Ensures that /// each newly created node has a unique ID. -fn binop( +fn binop( binop: BinOp, - lhs: ConstraintCircuitMonad, - rhs: ConstraintCircuitMonad, -) -> ConstraintCircuitMonad { + lhs: ConstraintCircuitMonad, + rhs: ConstraintCircuitMonad, +) -> ConstraintCircuitMonad { // Get ID for the new node let new_index = lhs.id_counter_ref.as_ref().borrow().to_owned(); @@ -795,24 +795,24 @@ fn binop( new_node } -impl Add for ConstraintCircuitMonad { - type Output = ConstraintCircuitMonad; +impl Add for ConstraintCircuitMonad { + type Output = ConstraintCircuitMonad; fn add(self, rhs: Self) -> Self::Output { binop(BinOp::Add, self, rhs) } } -impl Sub for ConstraintCircuitMonad { - type Output = ConstraintCircuitMonad; +impl Sub for ConstraintCircuitMonad { + type Output = ConstraintCircuitMonad; fn sub(self, rhs: Self) -> Self::Output { binop(BinOp::Sub, self, rhs) } } -impl Mul for ConstraintCircuitMonad { - type Output = ConstraintCircuitMonad; +impl Mul for ConstraintCircuitMonad { + type Output = ConstraintCircuitMonad; fn mul(self, rhs: Self) -> Self::Output { binop(BinOp::Mul, self, rhs) @@ -822,16 +822,16 @@ impl Mul for ConstraintCircuitMonad Sum for ConstraintCircuitMonad { +impl Sum for ConstraintCircuitMonad { fn sum>(iter: I) -> Self { iter.reduce(|accum, item| accum + item) .expect("ConstraintCircuitMonad Iterator was empty") } } -impl ConstraintCircuitMonad { +impl ConstraintCircuitMonad { /// Unwrap a ConstraintCircuitMonad to reveal its inner ConstraintCircuit - pub fn consume(self) -> ConstraintCircuit { + pub fn consume(self) -> ConstraintCircuit { self.circuit.try_borrow().unwrap().to_owned() } } @@ -839,52 +839,50 @@ impl ConstraintCircuitMonad { #[derive(Debug, Clone)] /// Helper struct to construct new leaf nodes in the circuit multitree. Ensures that each newly /// created node gets a unique ID. -pub struct ConstraintCircuitBuilder { +pub struct ConstraintCircuitBuilder { id_counter: Rc>, - all_nodes: Rc>>>, - _table_type: PhantomData, + all_nodes: Rc>>>, } -impl Default for ConstraintCircuitBuilder { +impl Default for ConstraintCircuitBuilder { fn default() -> Self { Self::new() } } -impl ConstraintCircuitBuilder { +impl ConstraintCircuitBuilder { pub fn new() -> Self { Self { id_counter: Rc::new(RefCell::new(0)), all_nodes: Rc::new(RefCell::new(HashSet::default())), - _table_type: PhantomData, } } /// Create constant leaf node - pub fn x_constant(&self, xfe: XFieldElement) -> ConstraintCircuitMonad { + pub fn x_constant(&self, xfe: XFieldElement) -> ConstraintCircuitMonad { let expression = XConstant(xfe); self.make_leaf(expression) } /// Create constant leaf node - pub fn b_constant(&self, bfe: BFieldElement) -> ConstraintCircuitMonad { + pub fn b_constant(&self, bfe: BFieldElement) -> ConstraintCircuitMonad { let expression = BConstant(bfe); self.make_leaf(expression) } /// Create deterministic input leaf node - pub fn input(&self, input: II) -> ConstraintCircuitMonad { + pub fn input(&self, input: II) -> ConstraintCircuitMonad { let expression = Input(input); self.make_leaf(expression) } /// Create challenge leaf node - pub fn challenge(&self, challenge_id: T::Id) -> ConstraintCircuitMonad { + pub fn challenge(&self, challenge_id: ChallengeId) -> ConstraintCircuitMonad { let expression = Challenge(challenge_id); self.make_leaf(expression) } - fn make_leaf(&self, expression: CircuitExpression) -> ConstraintCircuitMonad { + fn make_leaf(&self, expression: CircuitExpression) -> ConstraintCircuitMonad { let new_id = self.id_counter.as_ref().borrow().to_owned(); let new_node = ConstraintCircuitMonad { circuit: Rc::new(RefCell::new(ConstraintCircuit { @@ -925,19 +923,18 @@ mod constraint_circuit_tests { use rand::RngCore; use twenty_first::shared_math::other::random_elements; - use crate::table::challenges::AllChallenges; + use crate::table::challenges::ChallengeId::U32Indeterminate; + use crate::table::challenges::Challenges; use crate::table::jump_stack_table::ExtJumpStackTable; use crate::table::op_stack_table::ExtOpStackTable; use crate::table::processor_table::ExtProcessorTable; - use crate::table::processor_table::ProcessorTableChallengeId; - use crate::table::processor_table::ProcessorTableChallenges; use crate::table::program_table::ExtProgramTable; use crate::table::ram_table::ExtRamTable; use super::*; - fn node_counter_inner( - constraint: &mut ConstraintCircuit, + fn node_counter_inner( + constraint: &mut ConstraintCircuit, counter: &mut usize, ) { if constraint.visited_counter == 0 { @@ -952,9 +949,7 @@ mod constraint_circuit_tests { } /// Count the total number of nodes in call constraints - fn node_counter( - constraints: &mut [ConstraintCircuit], - ) -> usize { + fn node_counter(constraints: &mut [ConstraintCircuit]) -> usize { let mut counter = 0; for constraint in constraints.iter_mut() { @@ -969,8 +964,8 @@ mod constraint_circuit_tests { } fn random_circuit_builder() -> ( - ConstraintCircuitMonad>, - ConstraintCircuitBuilder>, + ConstraintCircuitMonad>, + ConstraintCircuitBuilder>, ) { let mut rng = thread_rng(); let num_base_columns = 50; @@ -996,7 +991,7 @@ mod constraint_circuit_tests { } 2 => { // p(x, y, z) = rand_i - circuit_builder.challenge(ProcessorTableChallengeId::U32PermIndeterminate) + circuit_builder.challenge(U32Indeterminate) } 3 => { // p(x, y, z) = 0 @@ -1010,8 +1005,8 @@ mod constraint_circuit_tests { // p(x, y, z) = rand_i * x let input_value = DualRowIndicator::CurrentExtRow(rng.next_u64() as usize % num_ext_columns); - let challenge = ProcessorTableChallengeId::U32PermIndeterminate; - circuit_builder.input(input_value) * circuit_builder.challenge(challenge) + let challenge_id = U32Indeterminate; + circuit_builder.input(input_value) * circuit_builder.challenge(challenge_id) } _ => unreachable!(), }; @@ -1027,10 +1022,10 @@ mod constraint_circuit_tests { } // Make a deep copy of a Multicircuit and return it as a ConstraintCircuitMonad - fn deep_copy_inner( - val: &ConstraintCircuit, - builder: &mut ConstraintCircuitBuilder, - ) -> ConstraintCircuitMonad { + fn deep_copy_inner( + val: &ConstraintCircuit, + builder: &mut ConstraintCircuitBuilder, + ) -> ConstraintCircuitMonad { match &val.expression { BinaryOperation(op, lhs, rhs) => { let lhs_ref = deep_copy_inner(&lhs.as_ref().borrow(), builder); @@ -1044,9 +1039,7 @@ mod constraint_circuit_tests { } } - fn deep_copy( - val: &ConstraintCircuit, - ) -> ConstraintCircuitMonad { + fn deep_copy(val: &ConstraintCircuit) -> ConstraintCircuitMonad { let mut builder = ConstraintCircuitBuilder::new(); deep_copy_inner(val, &mut builder) } @@ -1115,10 +1108,8 @@ mod constraint_circuit_tests { #[test] fn circuit_equality_check_and_constant_folding_test() { - let circuit_builder: ConstraintCircuitBuilder< - ProcessorTableChallenges, - DualRowIndicator<5, 3>, - > = ConstraintCircuitBuilder::new(); + let circuit_builder: ConstraintCircuitBuilder> = + ConstraintCircuitBuilder::new(); let var_0 = circuit_builder.input(DualRowIndicator::CurrentBaseRow(0)); let var_4 = circuit_builder.input(DualRowIndicator::NextBaseRow(4)); let four = circuit_builder.x_constant(4.into()); @@ -1306,9 +1297,9 @@ mod constraint_circuit_tests { } } - fn constant_folding_of_table_constraints_test( - mut constraints: Vec>, - challenges: T, + fn constant_folding_of_table_constraints_test( + mut constraints: Vec>, + challenges: &Challenges, table_name: &str, ) { ConstraintCircuit::assert_has_unique_ids(&mut constraints); @@ -1332,7 +1323,7 @@ mod constraint_circuit_tests { ); // apply challenges and verify that subtree no longer contains randomness - ConstraintCircuit::apply_challenges(&mut constraints, &challenges); + ConstraintCircuit::apply_challenges(&mut constraints, challenges); assert!( constraints .iter() @@ -1354,56 +1345,36 @@ mod constraint_circuit_tests { #[test] fn constant_folding_processor_table_test() { - let challenges = AllChallenges::placeholder(&[], &[]); + let challenges = Challenges::placeholder(&[], &[]); let constraint_circuits = ExtProcessorTable::ext_transition_constraints_as_circuits(); - constant_folding_of_table_constraints_test( - constraint_circuits, - challenges.processor_table_challenges, - "processor", - ); + constant_folding_of_table_constraints_test(constraint_circuits, &challenges, "processor"); } #[test] fn constant_folding_program_table_test() { - let challenges = AllChallenges::placeholder(&[], &[]); + let challenges = Challenges::placeholder(&[], &[]); let constraint_circuits = ExtProgramTable::ext_transition_constraints_as_circuits(); - constant_folding_of_table_constraints_test( - constraint_circuits, - challenges.program_table_challenges, - "program", - ); + constant_folding_of_table_constraints_test(constraint_circuits, &challenges, "program"); } #[test] fn constant_folding_jump_stack_table_test() { - let challenges = AllChallenges::placeholder(&[], &[]); + let challenges = Challenges::placeholder(&[], &[]); let constraint_circuits = ExtJumpStackTable::ext_transition_constraints_as_circuits(); - constant_folding_of_table_constraints_test( - constraint_circuits, - challenges.jump_stack_table_challenges, - "jump stack", - ); + constant_folding_of_table_constraints_test(constraint_circuits, &challenges, "jump stack"); } #[test] fn constant_folding_op_stack_table_test() { - let challenges = AllChallenges::placeholder(&[], &[]); + let challenges = Challenges::placeholder(&[], &[]); let constraint_circuits = ExtOpStackTable::ext_transition_constraints_as_circuits(); - constant_folding_of_table_constraints_test( - constraint_circuits, - challenges.op_stack_table_challenges, - "op stack", - ); + constant_folding_of_table_constraints_test(constraint_circuits, &challenges, "op stack"); } #[test] fn constant_folding_ram_stack_table_test() { - let challenges = AllChallenges::placeholder(&[], &[]); + let challenges = Challenges::placeholder(&[], &[]); let constraint_circuits = ExtRamTable::ext_transition_constraints_as_circuits(); - constant_folding_of_table_constraints_test( - constraint_circuits, - challenges.ram_table_challenges, - "ram", - ); + constant_folding_of_table_constraints_test(constraint_circuits, &challenges, "ram"); } } diff --git a/triton-vm/src/table/cross_table_argument.rs b/triton-vm/src/table/cross_table_argument.rs index 9acc54df3..b5eb29b21 100644 --- a/triton-vm/src/table/cross_table_argument.rs +++ b/triton-vm/src/table/cross_table_argument.rs @@ -1,26 +1,19 @@ -use itertools::Itertools; use std::ops::Add; use std::ops::Mul; +use itertools::Itertools; use ndarray::ArrayView1; use num_traits::One; use num_traits::Zero; -use strum_macros::Display; -use strum_macros::EnumCount as EnumCountMacro; -use strum_macros::EnumIter; use twenty_first::shared_math::b_field_element::BFieldElement; use twenty_first::shared_math::mpolynomial::Degree; use twenty_first::shared_math::traits::Inverse; use twenty_first::shared_math::x_field_element::XFieldElement; -use CrossTableChallengeId::*; - -use crate::table::challenges::AllChallenges; -use crate::table::challenges::TableChallenges; +use crate::table::challenges::ChallengeId::*; +use crate::table::challenges::Challenges; use crate::table::extension_table::Evaluable; use crate::table::extension_table::Quotientable; -use crate::table::processor_table::PROCESSOR_TABLE_NUM_EVALUATION_ARGUMENTS; -use crate::table::processor_table::PROCESSOR_TABLE_NUM_PERMUTATION_ARGUMENTS; use crate::table::table_column::HashExtTableColumn; use crate::table::table_column::JumpStackExtTableColumn; use crate::table::table_column::MasterExtTableColumn; @@ -30,15 +23,6 @@ use crate::table::table_column::ProgramExtTableColumn; use crate::table::table_column::RamExtTableColumn; use crate::table::table_column::U32ExtTableColumn; -pub const NUM_PUBLIC_EVAL_ARGS: usize = 2; // for public input and output -pub const NUM_PRIVATE_EVAL_ARGS: usize = - PROCESSOR_TABLE_NUM_EVALUATION_ARGUMENTS - NUM_PUBLIC_EVAL_ARGS; -pub const NUM_PRIVATE_PERM_ARGS: usize = PROCESSOR_TABLE_NUM_PERMUTATION_ARGUMENTS; -pub const NUM_LOOKUP_ARGS: usize = 2; -pub const NUM_CROSS_TABLE_ARGS: usize = - NUM_PRIVATE_PERM_ARGS + NUM_PRIVATE_EVAL_ARGS + NUM_LOOKUP_ARGS; -pub const NUM_CROSS_TABLE_WEIGHTS: usize = NUM_CROSS_TABLE_ARGS + NUM_PUBLIC_EVAL_ARGS; - pub trait CrossTableArg { fn default_initial() -> XFieldElement where @@ -140,76 +124,11 @@ impl LookupArg { #[derive(Debug, Clone, Copy, Eq, PartialEq)] pub struct GrandCrossTableArg {} -#[derive(Clone, Debug)] -pub struct CrossTableChallenges { - pub input_terminal: XFieldElement, - pub output_terminal: XFieldElement, - - pub processor_to_program_weight: XFieldElement, - pub processor_to_op_stack_weight: XFieldElement, - pub processor_to_ram_weight: XFieldElement, - pub processor_to_jump_stack_weight: XFieldElement, - pub hash_input_weight: XFieldElement, - pub hash_digest_weight: XFieldElement, - pub sponge_weight: XFieldElement, - pub processor_to_u32_weight: XFieldElement, - pub clock_jump_difference_lookup_weight: XFieldElement, - pub input_to_processor_weight: XFieldElement, - pub processor_to_output_weight: XFieldElement, -} - -#[derive(Debug, Copy, Clone, Display, EnumCountMacro, EnumIter, PartialEq, Eq, Hash)] -pub enum CrossTableChallengeId { - InputTerminal, - OutputTerminal, - - ProcessorToProgramWeight, - ProcessorToOpStackWeight, - ProcessorToRamWeight, - ProcessorToJumpStackWeight, - HashInputWeight, - HashDigestWeight, - SpongeWeight, - ProcessorToU32Weight, - ClockJumpDifferenceLookupWeight, - InputToProcessorWeight, - ProcessorToOutputWeight, -} - -impl From for usize { - fn from(val: CrossTableChallengeId) -> Self { - val as usize - } -} - -impl TableChallenges for CrossTableChallenges { - type Id = CrossTableChallengeId; - - #[inline] - fn get_challenge(&self, id: Self::Id) -> XFieldElement { - match id { - InputTerminal => self.input_terminal, - OutputTerminal => self.output_terminal, - ProcessorToProgramWeight => self.processor_to_program_weight, - ProcessorToOpStackWeight => self.processor_to_op_stack_weight, - ProcessorToRamWeight => self.processor_to_ram_weight, - ProcessorToJumpStackWeight => self.processor_to_jump_stack_weight, - HashInputWeight => self.hash_input_weight, - HashDigestWeight => self.hash_digest_weight, - SpongeWeight => self.sponge_weight, - ProcessorToU32Weight => self.processor_to_u32_weight, - ClockJumpDifferenceLookupWeight => self.clock_jump_difference_lookup_weight, - InputToProcessorWeight => self.input_to_processor_weight, - ProcessorToOutputWeight => self.processor_to_output_weight, - } - } -} - impl Evaluable for GrandCrossTableArg { fn evaluate_initial_constraints( _base_row: ArrayView1, _ext_row: ArrayView1, - _challenges: &AllChallenges, + _challenges: &Challenges, ) -> Vec { vec![] } @@ -217,7 +136,7 @@ impl Evaluable for GrandCrossTableArg { fn evaluate_consistency_constraints( _base_row: ArrayView1, _ext_row: ArrayView1, - _challenges: &AllChallenges, + _challenges: &Challenges, ) -> Vec { vec![] } @@ -227,7 +146,7 @@ impl Evaluable for GrandCrossTableArg { _current_ext_row: ArrayView1, _next_base_row: ArrayView1, _next_ext_row: ArrayView1, - _challenges: &AllChallenges, + _challenges: &Challenges, ) -> Vec { vec![] } @@ -235,15 +154,13 @@ impl Evaluable for GrandCrossTableArg { fn evaluate_terminal_constraints( _base_row: ArrayView1, ext_row: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) -> Vec { - let challenges = &challenges.cross_table_challenges; - - let input_to_processor = challenges.get_challenge(InputTerminal) + let input_to_processor = challenges.get_challenge(StandardInputTerminal) - ext_row[ProcessorExtTableColumn::InputTableEvalArg.master_ext_table_index()]; let processor_to_output = ext_row [ProcessorExtTableColumn::OutputTableEvalArg.master_ext_table_index()] - - challenges.get_challenge(OutputTerminal); + - challenges.get_challenge(StandardOutputTerminal); let instruction_lookup = ext_row [ProcessorExtTableColumn::InstructionLookupClientLogDerivative diff --git a/triton-vm/src/table/extension_table.rs b/triton-vm/src/table/extension_table.rs index b3f9872ab..4f778a08b 100644 --- a/triton-vm/src/table/extension_table.rs +++ b/triton-vm/src/table/extension_table.rs @@ -12,7 +12,7 @@ use twenty_first::shared_math::mpolynomial::Degree; use twenty_first::shared_math::x_field_element::XFieldElement; use crate::arithmetic_domain::ArithmeticDomain; -use crate::table::challenges::AllChallenges; +use crate::table::challenges::Challenges; const ERROR_MESSAGE_GENERATE_CONSTRAINTS: &str = "Constraints must be in place. Run: `cargo run --bin constraint-evaluation-generator`"; @@ -25,7 +25,7 @@ pub trait Evaluable { fn evaluate_initial_constraints( _base_row: ArrayView1, _ext_row: ArrayView1, - _challenges: &AllChallenges, + _challenges: &Challenges, ) -> Vec { panic!("{ERROR_MESSAGE_GENERATE_CONSTRAINTS}") } @@ -35,7 +35,7 @@ pub trait Evaluable { fn evaluate_consistency_constraints( _base_row: ArrayView1, _ext_row: ArrayView1, - _challenges: &AllChallenges, + _challenges: &Challenges, ) -> Vec { panic!("{ERROR_MESSAGE_GENERATE_CONSTRAINTS}") } @@ -47,7 +47,7 @@ pub trait Evaluable { _current_ext_row: ArrayView1, _next_base_row: ArrayView1, _next_ext_row: ArrayView1, - _challenges: &AllChallenges, + _challenges: &Challenges, ) -> Vec { panic!("{ERROR_MESSAGE_GENERATE_CONSTRAINTS}") } @@ -57,7 +57,7 @@ pub trait Evaluable { fn evaluate_terminal_constraints( _base_row: ArrayView1, _ext_row: ArrayView1, - _challenges: &AllChallenges, + _challenges: &Challenges, ) -> Vec { panic!("{ERROR_MESSAGE_GENERATE_CONSTRAINTS}") } @@ -143,7 +143,7 @@ pub trait Quotientable: Evaluable { master_ext_table: ArrayView2, quot_table: &mut ArrayViewMut2, zerofier_inverse: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) { debug_assert_eq!(zerofier_inverse.len(), master_base_table.nrows()); debug_assert_eq!(zerofier_inverse.len(), master_ext_table.nrows()); @@ -169,7 +169,7 @@ pub trait Quotientable: Evaluable { master_ext_table: ArrayView2, quot_table: &mut ArrayViewMut2, zerofier_inverse: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) { debug_assert_eq!(zerofier_inverse.len(), master_base_table.nrows()); debug_assert_eq!(zerofier_inverse.len(), master_ext_table.nrows()); @@ -195,7 +195,7 @@ pub trait Quotientable: Evaluable { master_ext_table: ArrayView2, quot_table: &mut ArrayViewMut2, zerofier_inverse: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, trace_domain: ArithmeticDomain, quotient_domain: ArithmeticDomain, ) { @@ -234,7 +234,7 @@ pub trait Quotientable: Evaluable { master_ext_table: ArrayView2, quot_table: &mut ArrayViewMut2, zerofier_inverse: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) { debug_assert_eq!(zerofier_inverse.len(), master_base_table.nrows()); debug_assert_eq!(zerofier_inverse.len(), master_ext_table.nrows()); diff --git a/triton-vm/src/table/hash_table.rs b/triton-vm/src/table/hash_table.rs index 36a409935..43c531fe7 100644 --- a/triton-vm/src/table/hash_table.rs +++ b/triton-vm/src/table/hash_table.rs @@ -6,9 +6,7 @@ use ndarray::ArrayView2; use ndarray::ArrayViewMut2; use num_traits::One; use strum::EnumCount; -use strum_macros::Display; -use strum_macros::EnumCount as EnumCountMacro; -use strum_macros::EnumIter; +use triton_opcodes::instruction::Instruction; use twenty_first::shared_math::b_field_element::BFieldElement; use twenty_first::shared_math::b_field_element::BFIELD_ONE; use twenty_first::shared_math::rescue_prime_digest::DIGEST_LENGTH; @@ -21,9 +19,8 @@ use twenty_first::shared_math::rescue_prime_regular::ROUND_CONSTANTS; use twenty_first::shared_math::rescue_prime_regular::STATE_SIZE; use twenty_first::shared_math::x_field_element::XFieldElement; -use triton_opcodes::instruction::Instruction; - -use crate::table::challenges::TableChallenges; +use crate::table::challenges::ChallengeId::*; +use crate::table::challenges::Challenges; use crate::table::constraint_circuit::ConstraintCircuit; use crate::table::constraint_circuit::ConstraintCircuitBuilder; use crate::table::constraint_circuit::ConstraintCircuitMonad; @@ -34,7 +31,6 @@ use crate::table::constraint_circuit::SingleRowIndicator; use crate::table::constraint_circuit::SingleRowIndicator::*; use crate::table::cross_table_argument::CrossTableArg; use crate::table::cross_table_argument::EvalArg; -use crate::table::hash_table::HashTableChallengeId::*; use crate::table::master_table::NUM_BASE_COLUMNS; use crate::table::master_table::NUM_EXT_COLUMNS; use crate::table::table_column::BaseTableColumn; @@ -47,10 +43,6 @@ use crate::table::table_column::MasterBaseTableColumn; use crate::table::table_column::MasterExtTableColumn; use crate::vm::AlgebraicExecutionTrace; -pub const HASH_TABLE_NUM_PERMUTATION_ARGUMENTS: usize = 0; -pub const HASH_TABLE_NUM_EVALUATION_ARGUMENTS: usize = 2; -pub const HASH_TABLE_NUM_EXTENSION_CHALLENGES: usize = HashTableChallengeId::COUNT; - pub const BASE_WIDTH: usize = HashBaseTableColumn::COUNT; pub const EXT_WIDTH: usize = HashExtTableColumn::COUNT; pub const FULL_WIDTH: usize = BASE_WIDTH + EXT_WIDTH; @@ -65,12 +57,8 @@ pub struct HashTable {} pub struct ExtHashTable {} impl ExtHashTable { - pub fn ext_initial_constraints_as_circuits() -> Vec< - ConstraintCircuit< - HashTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_initial_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let challenge = |c| circuit_builder.challenge(c); let constant = |c| circuit_builder.b_constant(c); @@ -108,7 +96,7 @@ impl ExtHashTable { HashStateWeight8, HashStateWeight9, ]; - let compressed_row: ConstraintCircuitMonad<_, _> = state_weights + let compressed_row: ConstraintCircuitMonad<_> = state_weights .into_iter() .zip_eq(state.into_iter()) .map(|(weight, state)| challenge(weight) * base_row(state)) @@ -123,7 +111,7 @@ impl ExtHashTable { // If the round number is 0, the running evaluation is the default initial. // If the current instruction is AbsorbInit, the running evaluation is the default initial. // Else, the first update has been applied to the running evaluation. - let from_processor_indeterminate = challenge(HashInputEvalIndeterminate); + let from_processor_indeterminate = challenge(HashInputIndeterminate); let running_evaluation_hash_input_is_default_initial = running_evaluation_hash_input.clone() - running_evaluation_initial.clone(); let running_evaluation_hash_input_has_accumulated_first_row = running_evaluation_hash_input @@ -140,12 +128,12 @@ impl ExtHashTable { running_evaluation_hash_digest - running_evaluation_initial.clone(); // Evaluation Argument “Sponge” - let sponge_indeterminate = challenge(SpongeEvalIndeterminate); + let sponge_indeterminate = challenge(SpongeIndeterminate); let running_evaluation_sponge_is_default_initial = running_evaluation_sponge.clone() - running_evaluation_initial.clone(); let running_evaluation_sponge_has_accumulated_first_row = running_evaluation_sponge - running_evaluation_initial * sponge_indeterminate - - challenge(CIWeight) * constant(Instruction::AbsorbInit.opcode_b()) + - challenge(HashCIWeight) * constant(Instruction::AbsorbInit.opcode_b()) - compressed_row; let running_evaluation_sponge_absorb_is_initialized_correctly = ci_is_hash * running_evaluation_sponge_has_accumulated_first_row @@ -163,10 +151,10 @@ impl ExtHashTable { } fn round_number_deselector( - circuit_builder: &ConstraintCircuitBuilder, - round_number_circuit_node: &ConstraintCircuitMonad, + circuit_builder: &ConstraintCircuitBuilder, + round_number_circuit_node: &ConstraintCircuitMonad, round_number_to_deselect: usize, - ) -> ConstraintCircuitMonad { + ) -> ConstraintCircuitMonad { let constant = |c: u64| circuit_builder.b_constant(c.into()); (0..=NUM_ROUNDS + 1) .filter(|&r| r != round_number_to_deselect) @@ -174,12 +162,8 @@ impl ExtHashTable { .fold(constant(1), |a, b| a * b) } - pub fn ext_consistency_constraints_as_circuits() -> Vec< - ConstraintCircuit< - HashTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_consistency_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let constant = |c: u64| circuit_builder.b_constant(c.into()); @@ -242,9 +226,8 @@ impl ExtHashTable { .collect() } - pub fn ext_transition_constraints_as_circuits() -> Vec< - ConstraintCircuit>, - > { + pub fn ext_transition_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let challenge = |c| circuit_builder.challenge(c); let constant = |c: u64| circuit_builder.b_constant(c.into()); @@ -268,9 +251,9 @@ impl ExtHashTable { circuit_builder.input(NextExtRow(column_idx.master_ext_table_index())) }; - let hash_input_eval_indeterminate = challenge(HashInputEvalIndeterminate); - let hash_digest_eval_indeterminate = challenge(HashDigestEvalIndeterminate); - let sponge_indeterminate = challenge(SpongeEvalIndeterminate); + let hash_input_eval_indeterminate = challenge(HashInputIndeterminate); + let hash_digest_eval_indeterminate = challenge(HashDigestIndeterminate); + let sponge_indeterminate = challenge(SpongeIndeterminate); let round_number = current_base_row(ROUNDNUMBER); let ci = current_base_row(CI); @@ -404,7 +387,7 @@ impl ExtHashTable { .map(|i| { (0..STATE_SIZE) .map(|j| b_constant(MDS[i * STATE_SIZE + j]) * after_sbox[j].clone()) - .sum::>() + .sum::>() }) .collect_vec(); @@ -425,7 +408,7 @@ impl ExtHashTable { .map(|i| { (0..STATE_SIZE) .map(|j| b_constant(MDS_INV[i * STATE_SIZE + j]) * before_constants[j].clone()) - .sum::>() + .sum::>() }) .collect_vec(); @@ -546,7 +529,7 @@ impl ExtHashTable { let running_evaluation_sponge_has_accumulated_next_row = running_evaluation_sponge_next .clone() - sponge_indeterminate.clone() * running_evaluation_sponge.clone() - - challenge(CIWeight) * ci_next.clone() + - challenge(HashCIWeight) * ci_next.clone() - compressed_row_next; let if_round_no_next_1_and_ci_next_absorb_init_or_squeeze_then_running_eval_sponge_updates = round_number_next_is_not_1.clone() @@ -554,7 +537,7 @@ impl ExtHashTable { * (ci_next.clone() - opcode_absorb.clone()) * running_evaluation_sponge_has_accumulated_next_row; - let compressed_difference_of_rows: ConstraintCircuitMonad<_, _> = state_weights[..RATE] + let compressed_difference_of_rows: ConstraintCircuitMonad<_> = state_weights[..RATE] .iter() .zip_eq(difference_of_state_registers[..RATE].iter()) .map(|(weight, state_difference)| weight.clone() * state_difference.clone()) @@ -562,7 +545,7 @@ impl ExtHashTable { let running_evaluation_sponge_absorb_has_accumulated_difference_of_rows = running_evaluation_sponge_next.clone() - sponge_indeterminate * running_evaluation_sponge.clone() - - challenge(CIWeight) * ci_next.clone() + - challenge(HashCIWeight) * ci_next.clone() - compressed_difference_of_rows; let if_round_no_next_is_1_and_ci_next_is_absorb_then_sponge_absorb_eval_is_updated = round_number_next_is_not_1 @@ -609,12 +592,8 @@ impl ExtHashTable { .collect() } - pub fn ext_terminal_constraints_as_circuits() -> Vec< - ConstraintCircuit< - HashTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_terminal_constraints_as_circuits( + ) -> Vec>> { // no more constraints vec![] } @@ -645,11 +624,17 @@ impl HashTable { pub fn extend( base_table: ArrayView2, mut ext_table: ArrayViewMut2, - challenges: &HashTableChallenges, + challenges: &Challenges, ) { assert_eq!(BASE_WIDTH, base_table.ncols()); assert_eq!(EXT_WIDTH, ext_table.ncols()); assert_eq!(base_table.nrows(), ext_table.nrows()); + + let ci_weight = challenges.get_challenge(HashCIWeight); + let hash_digest_eval_indeterminate = challenges.get_challenge(HashDigestIndeterminate); + let hash_input_eval_indeterminate = challenges.get_challenge(HashInputIndeterminate); + let sponge_eval_indeterminate = challenges.get_challenge(SpongeIndeterminate); + let mut hash_input_running_evaluation = EvalArg::default_initial(); let mut hash_digest_running_evaluation = EvalArg::default_initial(); let mut sponge_running_evaluation = EvalArg::default_initial(); @@ -669,16 +654,16 @@ impl HashTable { ] }; let state_weights = [ - challenges.hash_state_weight0, - challenges.hash_state_weight1, - challenges.hash_state_weight2, - challenges.hash_state_weight3, - challenges.hash_state_weight4, - challenges.hash_state_weight5, - challenges.hash_state_weight6, - challenges.hash_state_weight7, - challenges.hash_state_weight8, - challenges.hash_state_weight9, + challenges.get_challenge(HashStateWeight0), + challenges.get_challenge(HashStateWeight1), + challenges.get_challenge(HashStateWeight2), + challenges.get_challenge(HashStateWeight3), + challenges.get_challenge(HashStateWeight4), + challenges.get_challenge(HashStateWeight5), + challenges.get_challenge(HashStateWeight6), + challenges.get_challenge(HashStateWeight7), + challenges.get_challenge(HashStateWeight8), + challenges.get_challenge(HashStateWeight9), ]; let opcode_hash = Instruction::Hash.opcode_b(); @@ -703,7 +688,7 @@ impl HashTable { .map(|(&state, &weight)| weight * state) .sum(); hash_digest_running_evaluation = hash_digest_running_evaluation - * challenges.hash_digest_eval_indeterminate + * hash_digest_eval_indeterminate + compressed_hash_digest; } @@ -735,7 +720,7 @@ impl HashTable { match current_instruction { ci if ci == opcode_hash => { hash_input_running_evaluation = hash_input_running_evaluation - * challenges.hash_input_eval_indeterminate + * hash_input_eval_indeterminate + compressed_row_hash_input_and_sponge_operations; } ci if ci == opcode_absorb_init @@ -743,8 +728,8 @@ impl HashTable { || ci == opcode_squeeze => { sponge_running_evaluation = sponge_running_evaluation - * challenges.sponge_eval_indeterminate - + challenges.ci_weight * ci + * sponge_eval_indeterminate + + ci_weight * ci + compressed_row_hash_input_and_sponge_operations; } _ => panic!("Opcode must be of `hash`, `absorb_init`, `absorb`, or `squeeze`."), @@ -763,95 +748,6 @@ impl HashTable { } } -#[derive(Debug, Copy, Clone, Display, EnumCountMacro, EnumIter, PartialEq, Eq, Hash)] -pub enum HashTableChallengeId { - HashInputEvalIndeterminate, - HashDigestEvalIndeterminate, - SpongeEvalIndeterminate, - - CIWeight, - HashStateWeight0, - HashStateWeight1, - HashStateWeight2, - HashStateWeight3, - HashStateWeight4, - HashStateWeight5, - HashStateWeight6, - HashStateWeight7, - HashStateWeight8, - HashStateWeight9, - HashStateWeight10, - HashStateWeight11, - HashStateWeight12, - HashStateWeight13, - HashStateWeight14, - HashStateWeight15, -} - -impl From for usize { - fn from(val: HashTableChallengeId) -> Self { - val as usize - } -} - -#[derive(Debug, Clone)] -pub struct HashTableChallenges { - /// The weight that combines two consecutive rows in the - /// permutation/evaluation column of the hash table. - pub hash_input_eval_indeterminate: XFieldElement, - pub hash_digest_eval_indeterminate: XFieldElement, - pub sponge_eval_indeterminate: XFieldElement, - - /// Weights for condensing part of a row into a single column. (Related to processor table.) - pub ci_weight: XFieldElement, - pub hash_state_weight0: XFieldElement, - pub hash_state_weight1: XFieldElement, - pub hash_state_weight2: XFieldElement, - pub hash_state_weight3: XFieldElement, - pub hash_state_weight4: XFieldElement, - pub hash_state_weight5: XFieldElement, - pub hash_state_weight6: XFieldElement, - pub hash_state_weight7: XFieldElement, - pub hash_state_weight8: XFieldElement, - pub hash_state_weight9: XFieldElement, - pub hash_state_weight10: XFieldElement, - pub hash_state_weight11: XFieldElement, - pub hash_state_weight12: XFieldElement, - pub hash_state_weight13: XFieldElement, - pub hash_state_weight14: XFieldElement, - pub hash_state_weight15: XFieldElement, -} - -impl TableChallenges for HashTableChallenges { - type Id = HashTableChallengeId; - - #[inline] - fn get_challenge(&self, id: Self::Id) -> XFieldElement { - match id { - HashInputEvalIndeterminate => self.hash_input_eval_indeterminate, - HashDigestEvalIndeterminate => self.hash_digest_eval_indeterminate, - SpongeEvalIndeterminate => self.sponge_eval_indeterminate, - CIWeight => self.ci_weight, - HashStateWeight0 => self.hash_state_weight0, - HashStateWeight1 => self.hash_state_weight1, - HashStateWeight2 => self.hash_state_weight2, - HashStateWeight3 => self.hash_state_weight3, - HashStateWeight4 => self.hash_state_weight4, - HashStateWeight5 => self.hash_state_weight5, - HashStateWeight6 => self.hash_state_weight6, - HashStateWeight7 => self.hash_state_weight7, - HashStateWeight8 => self.hash_state_weight8, - HashStateWeight9 => self.hash_state_weight9, - HashStateWeight10 => self.hash_state_weight10, - HashStateWeight11 => self.hash_state_weight11, - HashStateWeight12 => self.hash_state_weight12, - HashStateWeight13 => self.hash_state_weight13, - HashStateWeight14 => self.hash_state_weight14, - HashStateWeight15 => self.hash_state_weight15, - } - } -} - #[cfg(test)] mod constraint_tests { use num_traits::Zero; diff --git a/triton-vm/src/table/jump_stack_table.rs b/triton-vm/src/table/jump_stack_table.rs index 7f59155e7..882514f44 100644 --- a/triton-vm/src/table/jump_stack_table.rs +++ b/triton-vm/src/table/jump_stack_table.rs @@ -1,4 +1,6 @@ use std::cmp::Ordering; +use std::fmt::Display; +use std::fmt::Formatter; use ndarray::parallel::prelude::*; use ndarray::s; @@ -8,19 +10,13 @@ use ndarray::ArrayView2; use ndarray::ArrayViewMut2; use ndarray::Axis; use strum::EnumCount; -use strum_macros::Display; -use strum_macros::EnumCount as EnumCountMacro; -use strum_macros::EnumIter; use triton_opcodes::instruction::Instruction; use twenty_first::shared_math::b_field_element::BFieldElement; use twenty_first::shared_math::traits::Inverse; use twenty_first::shared_math::x_field_element::XFieldElement; -use std::fmt::Display; -use std::fmt::Formatter; -use JumpStackTableChallengeId::*; - -use crate::table::challenges::TableChallenges; +use crate::table::challenges::ChallengeId::*; +use crate::table::challenges::Challenges; use crate::table::constraint_circuit::ConstraintCircuit; use crate::table::constraint_circuit::ConstraintCircuitBuilder; use crate::table::constraint_circuit::DualRowIndicator; @@ -43,10 +39,6 @@ use crate::table::table_column::MasterExtTableColumn; use crate::table::table_column::ProcessorBaseTableColumn; use crate::vm::AlgebraicExecutionTrace; -pub const JUMP_STACK_TABLE_NUM_PERMUTATION_ARGUMENTS: usize = 1; -pub const JUMP_STACK_TABLE_NUM_EVALUATION_ARGUMENTS: usize = 0; -pub const JUMP_STACK_TABLE_NUM_EXTENSION_CHALLENGES: usize = JumpStackTableChallengeId::COUNT; - pub const BASE_WIDTH: usize = JumpStackBaseTableColumn::COUNT; pub const EXT_WIDTH: usize = JumpStackExtTableColumn::COUNT; pub const FULL_WIDTH: usize = BASE_WIDTH + EXT_WIDTH; @@ -58,12 +50,8 @@ pub struct JumpStackTable {} pub struct ExtJumpStackTable {} impl ExtJumpStackTable { - pub fn ext_initial_constraints_as_circuits() -> Vec< - ConstraintCircuit< - JumpStackTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_initial_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let clk = circuit_builder.input(BaseRow(CLK.master_base_table_index())); @@ -76,9 +64,9 @@ impl ExtJumpStackTable { ClockJumpDifferenceLookupClientLogDerivative.master_ext_table_index(), )); - let processor_perm_indeterminate = circuit_builder.challenge(ProcessorPermRowIndeterminate); + let processor_perm_indeterminate = circuit_builder.challenge(JumpStackIndeterminate); // note: `clk`, `jsp`, `jso`, and `jsd` are all constrained to be 0 and can thus be omitted. - let compressed_row = circuit_builder.challenge(CiWeight) * ci; + let compressed_row = circuit_builder.challenge(JumpStackCiWeight) * ci; let rppa_starts_correctly = rppa - (processor_perm_indeterminate - compressed_row); // A clock jump difference of 0 is not allowed. Hence, the initial is recorded. @@ -97,22 +85,14 @@ impl ExtJumpStackTable { .to_vec() } - pub fn ext_consistency_constraints_as_circuits() -> Vec< - ConstraintCircuit< - JumpStackTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_consistency_constraints_as_circuits( + ) -> Vec>> { // no further constraints vec![] } - pub fn ext_transition_constraints_as_circuits() -> Vec< - ConstraintCircuit< - JumpStackTableChallenges, - DualRowIndicator, - >, - > { + pub fn ext_transition_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let one = circuit_builder.b_constant(1u32.into()); let call_opcode = @@ -173,14 +153,14 @@ impl ExtJumpStackTable { // The running product for the permutation argument `rppa` accumulates one row in each // row, relative to weights `a`, `b`, `c`, `d`, `e`, and indeterminate `α`. - let compressed_row = circuit_builder.challenge(ClkWeight) * clk_next.clone() - + circuit_builder.challenge(CiWeight) * ci_next - + circuit_builder.challenge(JspWeight) * jsp_next.clone() - + circuit_builder.challenge(JsoWeight) * jso_next - + circuit_builder.challenge(JsdWeight) * jsd_next; + let compressed_row = circuit_builder.challenge(JumpStackClkWeight) * clk_next.clone() + + circuit_builder.challenge(JumpStackCiWeight) * ci_next + + circuit_builder.challenge(JumpStackJspWeight) * jsp_next.clone() + + circuit_builder.challenge(JumpStackJsoWeight) * jso_next + + circuit_builder.challenge(JumpStackJsdWeight) * jsd_next; - let rppa_updates_correctly = rppa_next - - rppa * (circuit_builder.challenge(ProcessorPermRowIndeterminate) - compressed_row); + let rppa_updates_correctly = + rppa_next - rppa * (circuit_builder.challenge(JumpStackIndeterminate) - compressed_row); // The running sum of the logarithmic derivative for the clock jump difference Lookup // Argument accumulates a summand of `clk_diff` if and only if the `jsp` does not change. @@ -210,12 +190,8 @@ impl ExtJumpStackTable { .to_vec() } - pub fn ext_terminal_constraints_as_circuits() -> Vec< - ConstraintCircuit< - JumpStackTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_terminal_constraints_as_circuits( + ) -> Vec>> { vec![] } } @@ -341,11 +317,21 @@ impl JumpStackTable { pub fn extend( base_table: ArrayView2, mut ext_table: ArrayViewMut2, - challenges: &JumpStackTableChallenges, + challenges: &Challenges, ) { assert_eq!(BASE_WIDTH, base_table.ncols()); assert_eq!(EXT_WIDTH, ext_table.ncols()); assert_eq!(base_table.nrows(), ext_table.nrows()); + + let clk_weight = challenges.get_challenge(JumpStackClkWeight); + let ci_weight = challenges.get_challenge(JumpStackCiWeight); + let jsp_weight = challenges.get_challenge(JumpStackJspWeight); + let jso_weight = challenges.get_challenge(JumpStackJsoWeight); + let jsd_weight = challenges.get_challenge(JumpStackJsdWeight); + let perm_arg_indeterminate = challenges.get_challenge(JumpStackIndeterminate); + let clock_jump_difference_lookup_indeterminate = + challenges.get_challenge(ClockJumpDifferenceLookupIndeterminate); + let mut running_product = PermArg::default_initial(); let mut clock_jump_diff_lookup_log_derivative = LookupArg::default_initial(); let mut previous_row: Option> = None; @@ -358,23 +344,21 @@ impl JumpStackTable { let jso = current_row[JSO.base_table_index()]; let jsd = current_row[JSD.base_table_index()]; - let compressed_row_for_permutation_argument = clk * challenges.clk_weight - + ci * challenges.ci_weight - + jsp * challenges.jsp_weight - + jso * challenges.jso_weight - + jsd * challenges.jsd_weight; - running_product *= - challenges.processor_perm_indeterminate - compressed_row_for_permutation_argument; + let compressed_row_for_permutation_argument = clk * clk_weight + + ci * ci_weight + + jsp * jsp_weight + + jso * jso_weight + + jsd * jsd_weight; + running_product *= perm_arg_indeterminate - compressed_row_for_permutation_argument; // clock jump difference if let Some(prev_row) = previous_row { if prev_row[JSP.base_table_index()] == current_row[JSP.base_table_index()] { let clock_jump_difference = current_row[CLK.base_table_index()] - prev_row[CLK.base_table_index()]; - clock_jump_diff_lookup_log_derivative += (challenges - .clock_jump_difference_lookup_indeterminate - - clock_jump_difference) - .inverse(); + clock_jump_diff_lookup_log_derivative += + (clock_jump_difference_lookup_indeterminate - clock_jump_difference) + .inverse(); } } @@ -387,59 +371,6 @@ impl JumpStackTable { } } -#[derive(Debug, Copy, Clone, Display, EnumCountMacro, EnumIter, PartialEq, Eq, Hash)] -pub enum JumpStackTableChallengeId { - ProcessorPermRowIndeterminate, - ClkWeight, - CiWeight, - JspWeight, - JsoWeight, - JsdWeight, - ClockJumpDifferenceLookupIndeterminate, -} - -impl From for usize { - fn from(val: JumpStackTableChallengeId) -> Self { - val as usize - } -} - -#[derive(Debug, Clone)] -pub struct JumpStackTableChallenges { - /// The weight that combines two consecutive rows in the - /// permutation/evaluation column of the jump-stack table. - pub processor_perm_indeterminate: XFieldElement, - - /// Weights for condensing part of a row into a single column. (Related to processor table.) - pub clk_weight: XFieldElement, - pub ci_weight: XFieldElement, - pub jsp_weight: XFieldElement, - pub jso_weight: XFieldElement, - pub jsd_weight: XFieldElement, - - /// Indeterminate for the logarithmic derivative of the clock jump difference's Lookup Argument. - pub clock_jump_difference_lookup_indeterminate: XFieldElement, -} - -impl TableChallenges for JumpStackTableChallenges { - type Id = JumpStackTableChallengeId; - - #[inline] - fn get_challenge(&self, id: Self::Id) -> XFieldElement { - match id { - ProcessorPermRowIndeterminate => self.processor_perm_indeterminate, - ClkWeight => self.clk_weight, - CiWeight => self.ci_weight, - JspWeight => self.jsp_weight, - JsoWeight => self.jso_weight, - JsdWeight => self.jsd_weight, - ClockJumpDifferenceLookupIndeterminate => { - self.clock_jump_difference_lookup_indeterminate - } - } - } -} - pub struct JumpStackTraceRow { pub row: [BFieldElement; BASE_WIDTH], } diff --git a/triton-vm/src/table/master_table.rs b/triton-vm/src/table/master_table.rs index 5106af0e6..87d6345be 100644 --- a/triton-vm/src/table/master_table.rs +++ b/triton-vm/src/table/master_table.rs @@ -37,7 +37,7 @@ use twenty_first::util_types::merkle_tree_maker::MerkleTreeMaker; use crate::arithmetic_domain::ArithmeticDomain; use crate::stark::StarkHasher; -use crate::table::challenges::AllChallenges; +use crate::table::challenges::Challenges; use crate::table::cross_table_argument::GrandCrossTableArg; use crate::table::extension_table::DegreeWithOrigin; use crate::table::extension_table::Evaluable; @@ -450,7 +450,7 @@ impl MasterBaseTable { /// adding some number of columns. pub fn extend( &self, - challenges: &AllChallenges, + challenges: &Challenges, num_randomizer_polynomials: usize, ) -> MasterExtTable { // randomizer polynomials @@ -474,37 +474,37 @@ impl MasterBaseTable { ProgramTable::extend( self.table(TableId::ProgramTable), master_ext_table.table_mut(TableId::ProgramTable), - &challenges.program_table_challenges, + challenges, ); ProcessorTable::extend( self.table(TableId::ProcessorTable), master_ext_table.table_mut(TableId::ProcessorTable), - &challenges.processor_table_challenges, + challenges, ); OpStackTable::extend( self.table(TableId::OpStackTable), master_ext_table.table_mut(TableId::OpStackTable), - &challenges.op_stack_table_challenges, + challenges, ); RamTable::extend( self.table(TableId::RamTable), master_ext_table.table_mut(TableId::RamTable), - &challenges.ram_table_challenges, + challenges, ); JumpStackTable::extend( self.table(TableId::JumpStackTable), master_ext_table.table_mut(TableId::JumpStackTable), - &challenges.jump_stack_table_challenges, + challenges, ); HashTable::extend( self.table(TableId::HashTable), master_ext_table.table_mut(TableId::HashTable), - &challenges.hash_table_challenges, + challenges, ); U32Table::extend( self.table(TableId::U32Table), master_ext_table.table_mut(TableId::U32Table), - &challenges.u32_table_challenges, + challenges, ); master_ext_table @@ -820,7 +820,7 @@ pub fn fill_all_initial_quotients( master_ext_table: ArrayView2, quot_table: &mut ArrayViewMut2, zerofier_inverse: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) { // The order of the quotient tables is not actually important. However, it must be consistent // between prover and verifier, and the shapes must check out. @@ -908,7 +908,7 @@ pub fn fill_all_consistency_quotients( master_ext_table: ArrayView2, quot_table: &mut ArrayViewMut2, zerofier_inverse: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) { // The order of the quotient tables is not actually important. However, it must be consistent // between prover and verifier, and the shapes must check out. @@ -997,7 +997,7 @@ pub fn fill_all_transition_quotients( master_ext_table: ArrayView2, quot_table: &mut ArrayViewMut2, zerofier_inverse: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, trace_domain: ArithmeticDomain, quotient_domain: ArithmeticDomain, ) { @@ -1101,7 +1101,7 @@ pub fn fill_all_terminal_quotients( master_ext_table: ArrayView2, quot_table: &mut ArrayViewMut2, zerofier_inverse: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) { // The order of the quotient tables is not actually important. However, it must be consistent // between prover and verifier, and the shapes must check out. @@ -1210,7 +1210,7 @@ pub fn all_quotients( quotient_domain_master_ext_table: ArrayView2, trace_domain: ArithmeticDomain, quotient_domain: ArithmeticDomain, - challenges: &AllChallenges, + challenges: &Challenges, maybe_profiler: &mut Option, ) -> Array2 { assert_eq!( @@ -1310,7 +1310,7 @@ pub fn all_quotients( pub fn evaluate_all_initial_constraints( base_row: ArrayView1, ext_row: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) -> Vec { [ ExtProgramTable::evaluate_initial_constraints(base_row, ext_row, challenges), @@ -1327,7 +1327,7 @@ pub fn evaluate_all_initial_constraints( pub fn evaluate_all_consistency_constraints( base_row: ArrayView1, ext_row: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) -> Vec { [ ExtProgramTable::evaluate_consistency_constraints(base_row, ext_row, challenges), @@ -1346,7 +1346,7 @@ pub fn evaluate_all_transition_constraints( current_ext_row: ArrayView1, next_base_row: ArrayView1, next_ext_row: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) -> Vec { let cbr = current_base_row; let cer = current_ext_row; @@ -1367,7 +1367,7 @@ pub fn evaluate_all_transition_constraints( pub fn evaluate_all_terminal_constraints( base_row: ArrayView1, ext_row: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) -> Vec { [ ExtProgramTable::evaluate_terminal_constraints(base_row, ext_row, challenges), @@ -1387,7 +1387,7 @@ pub fn evaluate_all_constraints( current_ext_row: ArrayView1, next_base_row: ArrayView1, next_ext_row: ArrayView1, - challenges: &AllChallenges, + challenges: &Challenges, ) -> Vec { [ evaluate_all_initial_constraints(current_base_row, current_ext_row, challenges), diff --git a/triton-vm/src/table/op_stack_table.rs b/triton-vm/src/table/op_stack_table.rs index 19c308242..493b15749 100644 --- a/triton-vm/src/table/op_stack_table.rs +++ b/triton-vm/src/table/op_stack_table.rs @@ -8,17 +8,13 @@ use ndarray::ArrayView2; use ndarray::ArrayViewMut2; use ndarray::Axis; use strum::EnumCount; -use strum_macros::Display; -use strum_macros::EnumCount as EnumCountMacro; -use strum_macros::EnumIter; use twenty_first::shared_math::b_field_element::BFieldElement; use twenty_first::shared_math::traits::Inverse; use twenty_first::shared_math::x_field_element::XFieldElement; -use OpStackTableChallengeId::*; - use crate::op_stack::OP_STACK_REG_COUNT; -use crate::table::challenges::TableChallenges; +use crate::table::challenges::ChallengeId::*; +use crate::table::challenges::Challenges; use crate::table::constraint_circuit::ConstraintCircuit; use crate::table::constraint_circuit::ConstraintCircuitBuilder; use crate::table::constraint_circuit::DualRowIndicator; @@ -41,10 +37,6 @@ use crate::table::table_column::OpStackExtTableColumn::*; use crate::table::table_column::ProcessorBaseTableColumn; use crate::vm::AlgebraicExecutionTrace; -pub const OP_STACK_TABLE_NUM_PERMUTATION_ARGUMENTS: usize = 1; -pub const OP_STACK_TABLE_NUM_EVALUATION_ARGUMENTS: usize = 0; -pub const OP_STACK_TABLE_NUM_EXTENSION_CHALLENGES: usize = OpStackTableChallengeId::COUNT; - pub const BASE_WIDTH: usize = OpStackBaseTableColumn::COUNT; pub const EXT_WIDTH: usize = OpStackExtTableColumn::COUNT; pub const FULL_WIDTH: usize = BASE_WIDTH + EXT_WIDTH; @@ -56,12 +48,8 @@ pub struct OpStackTable {} pub struct ExtOpStackTable {} impl ExtOpStackTable { - pub fn ext_initial_constraints_as_circuits() -> Vec< - ConstraintCircuit< - OpStackTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_initial_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let clk = circuit_builder.input(BaseRow(CLK.master_base_table_index())); @@ -79,9 +67,10 @@ impl ExtOpStackTable { // The running product for the permutation argument `rppa` starts off having accumulated the // first row. Note that `clk` and `osv` are constrained to be 0, and `osp` to be 16. - let compressed_row = circuit_builder.challenge(Ib1Weight) * ib1 - + circuit_builder.challenge(OspWeight) * circuit_builder.b_constant(16_u32.into()); - let processor_perm_indeterminate = circuit_builder.challenge(ProcessorPermIndeterminate); + let compressed_row = circuit_builder.challenge(OpStackIb1Weight) * ib1 + + circuit_builder.challenge(OpStackOspWeight) + * circuit_builder.b_constant(16_u32.into()); + let processor_perm_indeterminate = circuit_builder.challenge(OpStackIndeterminate); let rppa_initial = processor_perm_indeterminate - compressed_row; let rppa_starts_correctly = rppa - rppa_initial; @@ -99,26 +88,16 @@ impl ExtOpStackTable { .to_vec() } - pub fn ext_consistency_constraints_as_circuits() -> Vec< - ConstraintCircuit< - OpStackTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_consistency_constraints_as_circuits( + ) -> Vec>> { // no further constraints vec![] } - pub fn ext_transition_constraints_as_circuits() -> Vec< - ConstraintCircuit< - OpStackTableChallenges, - DualRowIndicator, - >, - > { - let circuit_builder = ConstraintCircuitBuilder::< - OpStackTableChallenges, - DualRowIndicator, - >::new(); + pub fn ext_transition_constraints_as_circuits( + ) -> Vec>> { + let circuit_builder = + ConstraintCircuitBuilder::>::new(); let one = circuit_builder.b_constant(1u32.into()); let clk = circuit_builder.input(CurrentBaseRow(CLK.master_base_table_index())); @@ -159,11 +138,11 @@ impl ExtOpStackTable { * (one.clone() - ib1_shrink_stack); // The running product for the permutation argument `rppa` is updated correctly. - let alpha = circuit_builder.challenge(ProcessorPermIndeterminate); - let compressed_row = circuit_builder.challenge(ClkWeight) * clk_next.clone() - + circuit_builder.challenge(Ib1Weight) * ib1_shrink_stack_next - + circuit_builder.challenge(OspWeight) * osp_next.clone() - + circuit_builder.challenge(OsvWeight) * osv_next; + let alpha = circuit_builder.challenge(OpStackIndeterminate); + let compressed_row = circuit_builder.challenge(OpStackClkWeight) * clk_next.clone() + + circuit_builder.challenge(OpStackIb1Weight) * ib1_shrink_stack_next + + circuit_builder.challenge(OpStackOspWeight) * osp_next.clone() + + circuit_builder.challenge(OpStackOsvWeight) * osv_next; let rppa_updates_correctly = rppa_next - rppa * (alpha - compressed_row); @@ -193,12 +172,8 @@ impl ExtOpStackTable { .to_vec() } - pub fn ext_terminal_constraints_as_circuits() -> Vec< - ConstraintCircuit< - OpStackTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_terminal_constraints_as_circuits( + ) -> Vec>> { // no further constraints vec![] } @@ -323,11 +298,20 @@ impl OpStackTable { pub fn extend( base_table: ArrayView2, mut ext_table: ArrayViewMut2, - challenges: &OpStackTableChallenges, + challenges: &Challenges, ) { assert_eq!(BASE_WIDTH, base_table.ncols()); assert_eq!(EXT_WIDTH, ext_table.ncols()); assert_eq!(base_table.nrows(), ext_table.nrows()); + + let clk_weight = challenges.get_challenge(OpStackClkWeight); + let ib1_weight = challenges.get_challenge(OpStackIb1Weight); + let osp_weight = challenges.get_challenge(OpStackOspWeight); + let osv_weight = challenges.get_challenge(OpStackOsvWeight); + let perm_arg_indeterminate = challenges.get_challenge(OpStackIndeterminate); + let clock_jump_difference_lookup_indeterminate = + challenges.get_challenge(ClockJumpDifferenceLookupIndeterminate); + let mut running_product = PermArg::default_initial(); let mut clock_jump_diff_lookup_log_derivative = LookupArg::default_initial(); let mut previous_row: Option> = None; @@ -339,22 +323,18 @@ impl OpStackTable { let osp = current_row[OSP.base_table_index()]; let osv = current_row[OSV.base_table_index()]; - let compressed_row_for_permutation_argument = clk * challenges.clk_weight - + ib1 * challenges.ib1_weight - + osp * challenges.osp_weight - + osv * challenges.osv_weight; - running_product *= - challenges.processor_perm_indeterminate - compressed_row_for_permutation_argument; + let compressed_row_for_permutation_argument = + clk * clk_weight + ib1 * ib1_weight + osp * osp_weight + osv * osv_weight; + running_product *= perm_arg_indeterminate - compressed_row_for_permutation_argument; // clock jump difference if let Some(prev_row) = previous_row { if prev_row[OSP.base_table_index()] == current_row[OSP.base_table_index()] { let clock_jump_difference = current_row[CLK.base_table_index()] - prev_row[CLK.base_table_index()]; - clock_jump_diff_lookup_log_derivative += (challenges - .clock_jump_difference_lookup_indeterminate - - clock_jump_difference) - .inverse(); + clock_jump_diff_lookup_log_derivative += + (clock_jump_difference_lookup_indeterminate - clock_jump_difference) + .inverse(); } } @@ -366,53 +346,3 @@ impl OpStackTable { } } } - -#[derive(Debug, Copy, Clone, Display, EnumCountMacro, EnumIter, PartialEq, Eq, Hash)] -pub enum OpStackTableChallengeId { - ProcessorPermIndeterminate, - ClkWeight, - Ib1Weight, - OsvWeight, - OspWeight, - ClockJumpDifferenceLookupIndeterminate, -} - -impl From for usize { - fn from(val: OpStackTableChallengeId) -> Self { - val as usize - } -} - -impl TableChallenges for OpStackTableChallenges { - type Id = OpStackTableChallengeId; - - #[inline] - fn get_challenge(&self, id: Self::Id) -> XFieldElement { - match id { - ProcessorPermIndeterminate => self.processor_perm_indeterminate, - ClkWeight => self.clk_weight, - Ib1Weight => self.ib1_weight, - OsvWeight => self.osv_weight, - OspWeight => self.osp_weight, - ClockJumpDifferenceLookupIndeterminate => { - self.clock_jump_difference_lookup_indeterminate - } - } - } -} - -#[derive(Debug, Clone)] -pub struct OpStackTableChallenges { - /// The weight that combines two consecutive rows in the - /// permutation/evaluation column of the op-stack table. - pub processor_perm_indeterminate: XFieldElement, - - /// Weights for condensing part of a row into a single column. (Related to processor table.) - pub clk_weight: XFieldElement, - pub ib1_weight: XFieldElement, - pub osv_weight: XFieldElement, - pub osp_weight: XFieldElement, - - /// Indeterminate for the logarithmic derivative of the clock jump difference's Lookup Argument. - pub clock_jump_difference_lookup_indeterminate: XFieldElement, -} diff --git a/triton-vm/src/table/processor_table.rs b/triton-vm/src/table/processor_table.rs index 7b449e235..457e3e025 100644 --- a/triton-vm/src/table/processor_table.rs +++ b/triton-vm/src/table/processor_table.rs @@ -1,5 +1,4 @@ use std::cmp::max; -use std::cmp::Eq; use std::collections::HashMap; use std::fmt::Display; use std::ops::Mul; @@ -15,9 +14,6 @@ use ndarray::Axis; use num_traits::One; use num_traits::Zero; use strum::EnumCount; -use strum_macros::Display; -use strum_macros::EnumCount as EnumCountMacro; -use strum_macros::EnumIter; use triton_opcodes::instruction::all_instructions_without_args; use triton_opcodes::instruction::AnInstruction::*; use triton_opcodes::instruction::Instruction; @@ -27,9 +23,8 @@ use twenty_first::shared_math::b_field_element::BFIELD_ONE; use twenty_first::shared_math::traits::Inverse; use twenty_first::shared_math::x_field_element::XFieldElement; -use ProcessorTableChallengeId::*; - -use crate::table::challenges::TableChallenges; +use crate::table::challenges::ChallengeId::*; +use crate::table::challenges::Challenges; use crate::table::constraint_circuit::ConstraintCircuit; use crate::table::constraint_circuit::ConstraintCircuitBuilder; use crate::table::constraint_circuit::ConstraintCircuitMonad; @@ -52,10 +47,6 @@ use crate::table::table_column::ProcessorExtTableColumn; use crate::table::table_column::ProcessorExtTableColumn::*; use crate::vm::AlgebraicExecutionTrace; -pub const PROCESSOR_TABLE_NUM_PERMUTATION_ARGUMENTS: usize = 5; -pub const PROCESSOR_TABLE_NUM_EVALUATION_ARGUMENTS: usize = 8; -pub const PROCESSOR_TABLE_NUM_EXTENSION_CHALLENGES: usize = ProcessorTableChallengeId::COUNT; - pub const BASE_WIDTH: usize = ProcessorBaseTableColumn::COUNT; pub const EXT_WIDTH: usize = ProcessorExtTableColumn::COUNT; pub const FULL_WIDTH: usize = BASE_WIDTH + EXT_WIDTH; @@ -150,12 +141,11 @@ impl ProcessorTable { pub fn extend( base_table: ArrayView2, mut ext_table: ArrayViewMut2, - challenges: &ProcessorTableChallenges, + challenges: &Challenges, ) { assert_eq!(BASE_WIDTH, base_table.ncols()); assert_eq!(EXT_WIDTH, ext_table.ncols()); assert_eq!(base_table.nrows(), ext_table.nrows()); - let mut input_table_running_evaluation = EvalArg::default_initial(); let mut output_table_running_evaluation = EvalArg::default_initial(); let mut instruction_lookup_log_derivative = LookupArg::default_initial(); @@ -177,7 +167,7 @@ impl ProcessorTable { if prev_row[CI.base_table_index()] == Instruction::ReadIo.opcode_b() { let input_symbol = current_row[ST0.base_table_index()]; input_table_running_evaluation = input_table_running_evaluation - * challenges.standard_input_eval_indeterminate + * challenges.get_challenge(StandardInputIndeterminate) + input_symbol; } } @@ -186,7 +176,7 @@ impl ProcessorTable { if current_row[CI.base_table_index()] == Instruction::WriteIo.opcode_b() { let output_symbol = current_row[ST0.base_table_index()]; output_table_running_evaluation = output_table_running_evaluation - * challenges.standard_output_eval_indeterminate + * challenges.get_challenge(StandardOutputIndeterminate) + output_symbol; } @@ -195,10 +185,12 @@ impl ProcessorTable { let ip = current_row[IP.base_table_index()]; let ci = current_row[CI.base_table_index()]; let nia = current_row[NIA.base_table_index()]; - let compressed_row_for_instruction_lookup = ip * challenges.program_table_ip_weight - + ci * challenges.program_table_ci_processor_weight - + nia * challenges.program_table_nia_weight; - instruction_lookup_log_derivative += (challenges.instruction_lookup_indeterminate + let compressed_row_for_instruction_lookup = ip + * challenges.get_challenge(ProgramAddressWeight) + + ci * challenges.get_challenge(ProgramInstructionWeight) + + nia * challenges.get_challenge(ProgramNextInstructionWeight); + instruction_lookup_log_derivative += (challenges + .get_challenge(InstructionLookupIndeterminate) - compressed_row_for_instruction_lookup) .inverse(); } @@ -209,11 +201,11 @@ impl ProcessorTable { let osp = current_row[OSP.base_table_index()]; let osv = current_row[OSV.base_table_index()]; let compressed_row_for_op_stack_table_permutation_argument = clk - * challenges.op_stack_table_clk_weight - + ib1 * challenges.op_stack_table_ib1_weight - + osp * challenges.op_stack_table_osp_weight - + osv * challenges.op_stack_table_osv_weight; - op_stack_table_running_product *= challenges.op_stack_perm_indeterminate + * challenges.get_challenge(OpStackClkWeight) + + ib1 * challenges.get_challenge(OpStackIb1Weight) + + osp * challenges.get_challenge(OpStackOspWeight) + + osv * challenges.get_challenge(OpStackOsvWeight); + op_stack_table_running_product *= challenges.get_challenge(OpStackIndeterminate) - compressed_row_for_op_stack_table_permutation_argument; // RAM Table @@ -221,11 +213,11 @@ impl ProcessorTable { let ramp = current_row[RAMP.base_table_index()]; let previous_instruction = current_row[PreviousInstruction.base_table_index()]; let compressed_row_for_ram_table_permutation_argument = clk - * challenges.ram_table_clk_weight - + ramv * challenges.ram_table_ramv_weight - + ramp * challenges.ram_table_ramp_weight - + previous_instruction * challenges.ram_table_previous_instruction_weight; - ram_table_running_product *= challenges.ram_perm_indeterminate + * challenges.get_challenge(RamClkWeight) + + ramp * challenges.get_challenge(RamRampWeight) + + ramv * challenges.get_challenge(RamRamvWeight) + + previous_instruction * challenges.get_challenge(RamPreviousInstructionWeight); + ram_table_running_product *= challenges.get_challenge(RamIndeterminate) - compressed_row_for_ram_table_permutation_argument; // JumpStack Table @@ -233,29 +225,31 @@ impl ProcessorTable { let jsp = current_row[JSP.base_table_index()]; let jso = current_row[JSO.base_table_index()]; let jsd = current_row[JSD.base_table_index()]; - let compressed_row_for_jump_stack_table = clk * challenges.jump_stack_table_clk_weight - + ci * challenges.jump_stack_table_ci_weight - + jsp * challenges.jump_stack_table_jsp_weight - + jso * challenges.jump_stack_table_jso_weight - + jsd * challenges.jump_stack_table_jsd_weight; - jump_stack_running_product *= - challenges.jump_stack_perm_indeterminate - compressed_row_for_jump_stack_table; + let compressed_row_for_jump_stack_table = clk + * challenges.get_challenge(JumpStackClkWeight) + + ci * challenges.get_challenge(JumpStackCiWeight) + + jsp * challenges.get_challenge(JumpStackJspWeight) + + jso * challenges.get_challenge(JumpStackJsoWeight) + + jsd * challenges.get_challenge(JumpStackJsdWeight); + jump_stack_running_product *= challenges.get_challenge(JumpStackIndeterminate) + - compressed_row_for_jump_stack_table; // Hash Table – Hash's input from Processor to Hash Coprocessor let st_0_through_9 = [ST0, ST1, ST2, ST3, ST4, ST5, ST6, ST7, ST8, ST9] .map(|st| current_row[st.base_table_index()]); let hash_state_weights = [ - challenges.hash_state_weight0, - challenges.hash_state_weight1, - challenges.hash_state_weight2, - challenges.hash_state_weight3, - challenges.hash_state_weight4, - challenges.hash_state_weight5, - challenges.hash_state_weight6, - challenges.hash_state_weight7, - challenges.hash_state_weight8, - challenges.hash_state_weight9, - ]; + HashStateWeight0, + HashStateWeight1, + HashStateWeight2, + HashStateWeight3, + HashStateWeight4, + HashStateWeight5, + HashStateWeight6, + HashStateWeight7, + HashStateWeight8, + HashStateWeight9, + ] + .map(|id| challenges.get_challenge(id)); let compressed_row_for_hash_input_and_sponge: XFieldElement = st_0_through_9 .into_iter() .zip_eq(hash_state_weights.into_iter()) @@ -269,7 +263,7 @@ impl ProcessorTable { if current_row[CI.base_table_index()] == Instruction::Hash.opcode_b() { hash_input_running_evaluation = hash_input_running_evaluation - * challenges.hash_input_eval_indeterminate + * challenges.get_challenge(HashInputIndeterminate) + compressed_row_for_hash_input_and_sponge; } @@ -277,7 +271,7 @@ impl ProcessorTable { if let Some(prev_row) = previous_row { if prev_row[CI.base_table_index()] == Instruction::Hash.opcode_b() { hash_digest_running_evaluation = hash_digest_running_evaluation - * challenges.hash_digest_eval_indeterminate + * challenges.get_challenge(HashDigestIndeterminate) + compressed_row_for_hash_digest; } } @@ -289,8 +283,8 @@ impl ProcessorTable { || prev_row[CI.base_table_index()] == Instruction::Squeeze.opcode_b() { sponge_running_evaluation = sponge_running_evaluation - * challenges.sponge_eval_indeterminate - + challenges.hash_table_ci_weight * prev_row[CI.base_table_index()] + * challenges.get_challenge(SpongeIndeterminate) + + challenges.get_challenge(HashCIWeight) * prev_row[CI.base_table_index()] + compressed_row_for_hash_input_and_sponge; } } @@ -299,38 +293,44 @@ impl ProcessorTable { if let Some(prev_row) = previous_row { let previously_current_instruction = prev_row[CI.base_table_index()]; if previously_current_instruction == Instruction::Split.opcode_b() { - u32_table_running_product *= challenges.u32_table_perm_indeterminate - - current_row[ST0.base_table_index()] * challenges.u32_table_lhs_weight - - current_row[ST1.base_table_index()] * challenges.u32_table_rhs_weight - - prev_row[CI.base_table_index()] * challenges.u32_table_ci_weight; + u32_table_running_product *= challenges.get_challenge(U32Indeterminate) + - current_row[ST0.base_table_index()] + * challenges.get_challenge(U32LhsWeight) + - current_row[ST1.base_table_index()] + * challenges.get_challenge(U32RhsWeight) + - prev_row[CI.base_table_index()] * challenges.get_challenge(U32CiWeight); } if previously_current_instruction == Instruction::Lt.opcode_b() || previously_current_instruction == Instruction::And.opcode_b() || previously_current_instruction == Instruction::Xor.opcode_b() || previously_current_instruction == Instruction::Pow.opcode_b() { - u32_table_running_product *= challenges.u32_table_perm_indeterminate - - prev_row[ST0.base_table_index()] * challenges.u32_table_lhs_weight - - prev_row[ST1.base_table_index()] * challenges.u32_table_rhs_weight - - prev_row[CI.base_table_index()] * challenges.u32_table_ci_weight - - current_row[ST0.base_table_index()] * challenges.u32_table_result_weight; + u32_table_running_product *= challenges.get_challenge(U32Indeterminate) + - prev_row[ST0.base_table_index()] * challenges.get_challenge(U32LhsWeight) + - prev_row[ST1.base_table_index()] * challenges.get_challenge(U32RhsWeight) + - prev_row[CI.base_table_index()] * challenges.get_challenge(U32CiWeight) + - current_row[ST0.base_table_index()] + * challenges.get_challenge(U32ResultWeight); } if previously_current_instruction == Instruction::Log2Floor.opcode_b() { - u32_table_running_product *= challenges.u32_table_perm_indeterminate - - prev_row[ST0.base_table_index()] * challenges.u32_table_lhs_weight - - prev_row[CI.base_table_index()] * challenges.u32_table_ci_weight - - current_row[ST0.base_table_index()] * challenges.u32_table_result_weight; + u32_table_running_product *= challenges.get_challenge(U32Indeterminate) + - prev_row[ST0.base_table_index()] * challenges.get_challenge(U32LhsWeight) + - prev_row[CI.base_table_index()] * challenges.get_challenge(U32CiWeight) + - current_row[ST0.base_table_index()] + * challenges.get_challenge(U32ResultWeight); } if previously_current_instruction == Instruction::Div.opcode_b() { - u32_table_running_product *= challenges.u32_table_perm_indeterminate - - current_row[ST0.base_table_index()] * challenges.u32_table_lhs_weight - - prev_row[ST1.base_table_index()] * challenges.u32_table_rhs_weight - - Instruction::Lt.opcode_b() * challenges.u32_table_ci_weight - - BFieldElement::one() * challenges.u32_table_result_weight; - u32_table_running_product *= challenges.u32_table_perm_indeterminate - - prev_row[ST0.base_table_index()] * challenges.u32_table_lhs_weight - - current_row[ST1.base_table_index()] * challenges.u32_table_rhs_weight - - Instruction::Split.opcode_b() * challenges.u32_table_ci_weight; + u32_table_running_product *= challenges.get_challenge(U32Indeterminate) + - current_row[ST0.base_table_index()] + * challenges.get_challenge(U32LhsWeight) + - prev_row[ST1.base_table_index()] * challenges.get_challenge(U32RhsWeight) + - Instruction::Lt.opcode_b() * challenges.get_challenge(U32CiWeight) + - BFieldElement::one() * challenges.get_challenge(U32ResultWeight); + u32_table_running_product *= challenges.get_challenge(U32Indeterminate) + - prev_row[ST0.base_table_index()] * challenges.get_challenge(U32LhsWeight) + - current_row[ST1.base_table_index()] + * challenges.get_challenge(U32RhsWeight) + - Instruction::Split.opcode_b() * challenges.get_challenge(U32CiWeight); } } @@ -338,7 +338,7 @@ impl ProcessorTable { let lookup_multiplicity = current_row[ClockJumpDifferenceLookupMultiplicity.base_table_index()]; clock_jump_diff_lookup_op_stack_log_derivative += - (challenges.clock_jump_difference_lookup_indeterminate - clk).inverse() + (challenges.get_challenge(ClockJumpDifferenceLookupIndeterminate) - clk).inverse() * lookup_multiplicity; let mut extension_row = ext_table.row_mut(row_idx); @@ -380,19 +380,9 @@ impl ExtProcessorTable { factory: &mut DualRowConstraints, instr_tc_polys_tuples: [( Instruction, - Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - >, + Vec>>, ); Instruction::COUNT], - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let (all_instructions, all_tc_polys_for_all_instructions): (Vec<_>, Vec>) = instr_tc_polys_tuples.into_iter().unzip(); @@ -435,17 +425,9 @@ impl ExtProcessorTable { fn combine_transition_constraints_with_padding_constraints( factory: &DualRowConstraints, instruction_transition_constraints: Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - >, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, + ConstraintCircuitMonad>, >, - > { + ) -> Vec>> { let ip_remains = factory.ip_next() - factory.ip(); let ci_remains = factory.ci_next() - factory.ci(); let nia_remains = factory.nia_next() - factory.nia(); @@ -483,198 +465,12 @@ impl ExtProcessorTable { } } -#[derive(Debug, Copy, Clone, Display, EnumCountMacro, EnumIter, PartialEq, Eq, Hash)] -pub enum ProcessorTableChallengeId { - /// The weight that combines two consecutive rows in the - /// permutation/evaluation column of the processor table. - StandardInputEvalIndeterminate, - StandardOutputEvalIndeterminate, - HashInputEvalIndeterminate, - HashDigestEvalIndeterminate, - SpongeEvalIndeterminate, - - InstructionLookupIndeterminate, - OpStackPermIndeterminate, - RamPermIndeterminate, - JumpStackPermIndeterminate, - U32PermIndeterminate, - - /// Weights for condensing part of a row into a single column. (Related to processor table.) - ProgramTableIpWeight, - ProgramTableCiProcessorWeight, - ProgramTableNiaWeight, - - OpStackTableClkWeight, - OpStackTableIb1Weight, - OpStackTableOspWeight, - OpStackTableOsvWeight, - - RamTableClkWeight, - RamTableRamvWeight, - RamTableRampWeight, - RamTablePreviousInstructionWeight, - - JumpStackTableClkWeight, - JumpStackTableCiWeight, - JumpStackTableJspWeight, - JumpStackTableJsoWeight, - JumpStackTableJsdWeight, - - ClockJumpDifferenceLookupIndeterminate, - - HashTableCIWeight, - HashStateWeight0, - HashStateWeight1, - HashStateWeight2, - HashStateWeight3, - HashStateWeight4, - HashStateWeight5, - HashStateWeight6, - HashStateWeight7, - HashStateWeight8, - HashStateWeight9, - - U32TableLhsWeight, - U32TableRhsWeight, - U32TableCiWeight, - U32TableResultWeight, -} - -impl From for usize { - fn from(val: ProcessorTableChallengeId) -> Self { - val as usize - } -} - -#[derive(Debug, Clone)] -pub struct ProcessorTableChallenges { - /// The weight that combines two consecutive rows in the - /// permutation/evaluation column of the processor table. - pub standard_input_eval_indeterminate: XFieldElement, - pub standard_output_eval_indeterminate: XFieldElement, - pub hash_input_eval_indeterminate: XFieldElement, - pub hash_digest_eval_indeterminate: XFieldElement, - pub sponge_eval_indeterminate: XFieldElement, - - pub instruction_lookup_indeterminate: XFieldElement, - pub op_stack_perm_indeterminate: XFieldElement, - pub ram_perm_indeterminate: XFieldElement, - pub jump_stack_perm_indeterminate: XFieldElement, - pub u32_table_perm_indeterminate: XFieldElement, - - /// Weights for condensing part of a row into a single column. (Related to processor table.) - pub program_table_ip_weight: XFieldElement, - pub program_table_ci_processor_weight: XFieldElement, - pub program_table_nia_weight: XFieldElement, - - pub op_stack_table_clk_weight: XFieldElement, - pub op_stack_table_ib1_weight: XFieldElement, - pub op_stack_table_osp_weight: XFieldElement, - pub op_stack_table_osv_weight: XFieldElement, - - pub ram_table_clk_weight: XFieldElement, - pub ram_table_ramp_weight: XFieldElement, - pub ram_table_ramv_weight: XFieldElement, - pub ram_table_previous_instruction_weight: XFieldElement, - - pub jump_stack_table_clk_weight: XFieldElement, - pub jump_stack_table_ci_weight: XFieldElement, - pub jump_stack_table_jsp_weight: XFieldElement, - pub jump_stack_table_jso_weight: XFieldElement, - pub jump_stack_table_jsd_weight: XFieldElement, - - pub clock_jump_difference_lookup_indeterminate: XFieldElement, - - pub hash_table_ci_weight: XFieldElement, - pub hash_state_weight0: XFieldElement, - pub hash_state_weight1: XFieldElement, - pub hash_state_weight2: XFieldElement, - pub hash_state_weight3: XFieldElement, - pub hash_state_weight4: XFieldElement, - pub hash_state_weight5: XFieldElement, - pub hash_state_weight6: XFieldElement, - pub hash_state_weight7: XFieldElement, - pub hash_state_weight8: XFieldElement, - pub hash_state_weight9: XFieldElement, - - pub u32_table_lhs_weight: XFieldElement, - pub u32_table_rhs_weight: XFieldElement, - pub u32_table_ci_weight: XFieldElement, - pub u32_table_result_weight: XFieldElement, -} - -impl TableChallenges for ProcessorTableChallenges { - type Id = ProcessorTableChallengeId; - - #[inline] - fn get_challenge(&self, id: Self::Id) -> XFieldElement { - match id { - StandardInputEvalIndeterminate => self.standard_input_eval_indeterminate, - StandardOutputEvalIndeterminate => self.standard_output_eval_indeterminate, - HashInputEvalIndeterminate => self.hash_input_eval_indeterminate, - HashDigestEvalIndeterminate => self.hash_digest_eval_indeterminate, - SpongeEvalIndeterminate => self.sponge_eval_indeterminate, - InstructionLookupIndeterminate => self.instruction_lookup_indeterminate, - OpStackPermIndeterminate => self.op_stack_perm_indeterminate, - RamPermIndeterminate => self.ram_perm_indeterminate, - JumpStackPermIndeterminate => self.jump_stack_perm_indeterminate, - U32PermIndeterminate => self.u32_table_perm_indeterminate, - ProgramTableIpWeight => self.program_table_ip_weight, - ProgramTableCiProcessorWeight => self.program_table_ci_processor_weight, - ProgramTableNiaWeight => self.program_table_nia_weight, - OpStackTableClkWeight => self.op_stack_table_clk_weight, - OpStackTableIb1Weight => self.op_stack_table_ib1_weight, - OpStackTableOspWeight => self.op_stack_table_osp_weight, - OpStackTableOsvWeight => self.op_stack_table_osv_weight, - RamTableClkWeight => self.ram_table_clk_weight, - RamTableRamvWeight => self.ram_table_ramv_weight, - RamTableRampWeight => self.ram_table_ramp_weight, - RamTablePreviousInstructionWeight => self.ram_table_previous_instruction_weight, - JumpStackTableClkWeight => self.jump_stack_table_clk_weight, - JumpStackTableCiWeight => self.jump_stack_table_ci_weight, - JumpStackTableJspWeight => self.jump_stack_table_jsp_weight, - JumpStackTableJsoWeight => self.jump_stack_table_jso_weight, - JumpStackTableJsdWeight => self.jump_stack_table_jsd_weight, - ClockJumpDifferenceLookupIndeterminate => { - self.clock_jump_difference_lookup_indeterminate - } - HashTableCIWeight => self.hash_table_ci_weight, - HashStateWeight0 => self.hash_state_weight0, - HashStateWeight1 => self.hash_state_weight1, - HashStateWeight2 => self.hash_state_weight2, - HashStateWeight3 => self.hash_state_weight3, - HashStateWeight4 => self.hash_state_weight4, - HashStateWeight5 => self.hash_state_weight5, - HashStateWeight6 => self.hash_state_weight6, - HashStateWeight7 => self.hash_state_weight7, - HashStateWeight8 => self.hash_state_weight8, - HashStateWeight9 => self.hash_state_weight9, - U32TableLhsWeight => self.u32_table_lhs_weight, - U32TableRhsWeight => self.u32_table_rhs_weight, - U32TableCiWeight => self.u32_table_ci_weight, - U32TableResultWeight => self.u32_table_result_weight, - } - } -} - -#[derive(Debug, Clone)] -pub struct IOChallenges { - /// weight for updating the running evaluation with the next i/o symbol in the i/o list - pub processor_eval_indeterminate: XFieldElement, -} - #[derive(Debug, Clone)] pub struct ExtProcessorTable {} impl ExtProcessorTable { - pub fn ext_initial_constraints_as_circuits() -> Vec< - ConstraintCircuit< - ProcessorTableChallenges, - SingleRowIndicator, - >, - > { - use ProcessorTableChallengeId::*; - + pub fn ext_initial_constraints_as_circuits( + ) -> Vec>> { let factory = SingleRowConstraints::default(); let constant = |c| factory.constant_from_i32(c); let constant_x = |x| factory.constant_from_xfe(x); @@ -715,8 +511,8 @@ impl ExtProcessorTable { // program table let instruction_lookup_indeterminate = challenge(InstructionLookupIndeterminate); - let instruction_ci_weight = challenge(ProgramTableCiProcessorWeight); - let instruction_nia_weight = challenge(ProgramTableNiaWeight); + let instruction_ci_weight = challenge(ProgramInstructionWeight); + let instruction_nia_weight = challenge(ProgramNextInstructionWeight); let compressed_row_for_instruction_lookup = instruction_ci_weight * factory.ci() + instruction_nia_weight * factory.nia(); let instruction_lookup_log_derivative_is_initialized_correctly = (factory @@ -730,9 +526,9 @@ impl ExtProcessorTable { factory.running_evaluation_standard_output() - constant_x(EvalArg::default_initial()); // op-stack table - let op_stack_indeterminate = challenge(OpStackPermIndeterminate); - let op_stack_ib1_weight = challenge(OpStackTableIb1Weight); - let op_stack_osp_weight = challenge(OpStackTableOspWeight); + let op_stack_indeterminate = challenge(OpStackIndeterminate); + let op_stack_ib1_weight = challenge(OpStackIb1Weight); + let op_stack_osp_weight = challenge(OpStackOspWeight); // note: `clk` and `osv` are already constrained to be 0, `osp` to be 16 let compressed_row_for_op_stack_table = op_stack_ib1_weight * factory.ib1() + op_stack_osp_weight * constant(16); @@ -742,7 +538,7 @@ impl ExtProcessorTable { * (op_stack_indeterminate - compressed_row_for_op_stack_table); // ram table - let ram_indeterminate = challenge(RamPermIndeterminate); + let ram_indeterminate = challenge(RamIndeterminate); // note: `clk`, `ramp`, and `ramv` are already constrained to be 0. let compressed_row_for_ram_table = constant(0); let running_product_for_ram_table_is_initialized_correctly = factory @@ -751,8 +547,8 @@ impl ExtProcessorTable { * (ram_indeterminate - compressed_row_for_ram_table); // jump-stack table - let jump_stack_indeterminate = challenge(JumpStackPermIndeterminate); - let jump_stack_ci_weight = challenge(JumpStackTableCiWeight); + let jump_stack_indeterminate = challenge(JumpStackIndeterminate); + let jump_stack_ci_weight = challenge(JumpStackCiWeight); // note: `clk`, `jsp`, `jso`, and `jsd` are already constrained to be 0. let compressed_row_for_jump_stack_table = jump_stack_ci_weight * factory.ci(); let running_product_for_jump_stack_table_is_initialized_correctly = factory @@ -770,7 +566,7 @@ impl ExtProcessorTable { let hash_selector = factory.ci() - constant(Instruction::Hash.opcode() as i32); let hash_deselector = InstructionDeselectors::instruction_deselector_single_row(&factory, Instruction::Hash); - let hash_input_indeterminate = challenge(HashInputEvalIndeterminate); + let hash_input_indeterminate = challenge(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 = factory @@ -838,12 +634,8 @@ impl ExtProcessorTable { .to_vec() } - pub fn ext_consistency_constraints_as_circuits() -> Vec< - ConstraintCircuit< - ProcessorTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_consistency_constraints_as_circuits( + ) -> Vec>> { let factory = SingleRowConstraints::default(); let one = factory.one(); let constant = |c| factory.constant_from_i32(c); @@ -894,12 +686,8 @@ impl ExtProcessorTable { .to_vec() } - pub fn ext_transition_constraints_as_circuits() -> Vec< - ConstraintCircuit< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + pub fn ext_transition_constraints_as_circuits( + ) -> Vec>> { let mut factory = DualRowConstraints::default(); // instruction-specific constraints @@ -998,12 +786,8 @@ impl ExtProcessorTable { built_transition_constraints } - pub fn ext_terminal_constraints_as_circuits() -> Vec< - ConstraintCircuit< - ProcessorTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_terminal_constraints_as_circuits( + ) -> Vec>> { let factory = SingleRowConstraints::default(); // In the last row, current instruction register ci is 0, corresponding to instruction halt. @@ -1016,25 +800,15 @@ impl ExtProcessorTable { #[derive(Debug, Clone)] pub struct SingleRowConstraints { base_row_variables: [ConstraintCircuitMonad< - ProcessorTableChallenges, SingleRowIndicator, >; NUM_BASE_COLUMNS], ext_row_variables: [ConstraintCircuitMonad< - ProcessorTableChallenges, SingleRowIndicator, >; NUM_EXT_COLUMNS], - circuit_builder: ConstraintCircuitBuilder< - ProcessorTableChallenges, - SingleRowIndicator, - >, - one: ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - >, - two: ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - >, + circuit_builder: + ConstraintCircuitBuilder>, + one: ConstraintCircuitMonad>, + two: ConstraintCircuitMonad>, } impl Default for SingleRowConstraints { @@ -1068,19 +842,13 @@ impl SingleRowConstraints { pub fn constant_from_xfe( &self, constant: XFieldElement, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.circuit_builder.x_constant(constant) } pub fn constant_from_i32( &self, constant: i32, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { let bfe = if constant < 0 { BFieldElement::new(BFieldElement::P - ((-constant) as u64)) } else { @@ -1091,447 +859,282 @@ impl SingleRowConstraints { pub fn one( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.one.clone() } pub fn two( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.two.clone() } pub fn clk( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[CLK.master_base_table_index()].clone() } pub fn is_padding( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[IsPadding.master_base_table_index()].clone() } pub fn ip( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[IP.master_base_table_index()].clone() } pub fn ci( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[CI.master_base_table_index()].clone() } pub fn nia( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[NIA.master_base_table_index()].clone() } pub fn ib0( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[IB0.master_base_table_index()].clone() } pub fn ib1( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[IB1.master_base_table_index()].clone() } pub fn ib2( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[IB2.master_base_table_index()].clone() } pub fn ib3( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[IB3.master_base_table_index()].clone() } pub fn ib4( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[IB4.master_base_table_index()].clone() } pub fn ib5( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[IB5.master_base_table_index()].clone() } pub fn ib6( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[IB6.master_base_table_index()].clone() } pub fn ib7( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[IB7.master_base_table_index()].clone() } pub fn jsp( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[JSP.master_base_table_index()].clone() } pub fn jsd( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[JSD.master_base_table_index()].clone() } pub fn jso( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[JSO.master_base_table_index()].clone() } pub fn st0( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST0.master_base_table_index()].clone() } pub fn st1( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST1.master_base_table_index()].clone() } pub fn st2( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST2.master_base_table_index()].clone() } pub fn st3( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST3.master_base_table_index()].clone() } pub fn st4( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST4.master_base_table_index()].clone() } pub fn st5( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST5.master_base_table_index()].clone() } pub fn st6( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST6.master_base_table_index()].clone() } pub fn st7( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST7.master_base_table_index()].clone() } pub fn st8( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST8.master_base_table_index()].clone() } pub fn st9( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST9.master_base_table_index()].clone() } pub fn st10( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST10.master_base_table_index()].clone() } pub fn st11( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST11.master_base_table_index()].clone() } pub fn st12( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST12.master_base_table_index()].clone() } pub fn st13( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST13.master_base_table_index()].clone() } pub fn st14( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST14.master_base_table_index()].clone() } pub fn st15( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ST15.master_base_table_index()].clone() } pub fn osp( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[OSP.master_base_table_index()].clone() } pub fn osv( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[OSV.master_base_table_index()].clone() } pub fn hv0( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[HV0.master_base_table_index()].clone() } pub fn hv1( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[HV1.master_base_table_index()].clone() } pub fn hv2( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[HV2.master_base_table_index()].clone() } pub fn hv3( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[HV3.master_base_table_index()].clone() } pub fn ramv( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[RAMV.master_base_table_index()].clone() } pub fn ramp( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[RAMP.master_base_table_index()].clone() } pub fn clock_jump_difference_lookup_multiplicity( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[ClockJumpDifferenceLookupMultiplicity.master_base_table_index()] .clone() } pub fn previous_instruction( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.base_row_variables[PreviousInstruction.master_base_table_index()].clone() } pub fn running_evaluation_standard_input( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.ext_row_variables[InputTableEvalArg.master_ext_table_index()].clone() } pub fn running_evaluation_standard_output( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.ext_row_variables[OutputTableEvalArg.master_ext_table_index()].clone() } pub fn instruction_lookup_log_derivative( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.ext_row_variables[InstructionLookupClientLogDerivative.master_ext_table_index()] .clone() } pub fn running_product_op_stack_table( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.ext_row_variables[OpStackTablePermArg.master_ext_table_index()].clone() } pub fn running_product_ram_table( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.ext_row_variables[RamTablePermArg.master_ext_table_index()].clone() } pub fn running_product_jump_stack_table( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.ext_row_variables[JumpStackTablePermArg.master_ext_table_index()].clone() } pub fn clock_jump_difference_lookup_server_log_derivative( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.ext_row_variables [ClockJumpDifferenceLookupServerLogDerivative.master_ext_table_index()] .clone() } pub fn running_evaluation_hash_input( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.ext_row_variables[HashInputEvalArg.master_ext_table_index()].clone() } pub fn running_evaluation_hash_digest( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.ext_row_variables[HashDigestEvalArg.master_ext_table_index()].clone() } pub fn running_evaluation_sponge( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.ext_row_variables[SpongeEvalArg.master_ext_table_index()].clone() } pub fn running_product_u32_table( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.ext_row_variables[U32TablePermArg.master_ext_table_index()].clone() } } @@ -1539,37 +1142,21 @@ impl SingleRowConstraints { #[derive(Debug, Clone)] pub struct DualRowConstraints { current_base_row_variables: [ConstraintCircuitMonad< - ProcessorTableChallenges, DualRowIndicator, >; NUM_BASE_COLUMNS], current_ext_row_variables: [ConstraintCircuitMonad< - ProcessorTableChallenges, DualRowIndicator, >; NUM_EXT_COLUMNS], next_base_row_variables: [ConstraintCircuitMonad< - ProcessorTableChallenges, DualRowIndicator, >; NUM_BASE_COLUMNS], next_ext_row_variables: [ConstraintCircuitMonad< - ProcessorTableChallenges, DualRowIndicator, >; NUM_EXT_COLUMNS], - circuit_builder: ConstraintCircuitBuilder< - ProcessorTableChallenges, - DualRowIndicator, - >, - zero: ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - one: ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - two: ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, + circuit_builder: ConstraintCircuitBuilder>, + zero: ConstraintCircuitMonad>, + one: ConstraintCircuitMonad>, + two: ConstraintCircuitMonad>, } impl Default for DualRowConstraints { @@ -1630,10 +1217,7 @@ impl DualRowConstraints { /// when every `clk` register $a$ is one less than `clk` register $a + 1$. pub fn clk_always_increases_by_one( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { let one = self.one(); let clk = self.clk(); let clk_next = self.clk_next(); @@ -1643,29 +1227,20 @@ impl DualRowConstraints { pub fn is_padding_is_zero_or_does_not_change( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.is_padding() * (self.is_padding_next() - self.is_padding()) } pub fn previous_instruction_is_copied_correctly( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { (self.previous_instruction_next() - self.ci()) * (self.one() - self.is_padding_next()) } pub fn indicator_polynomial( &self, i: usize, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { let hv0 = self.hv0(); let hv1 = self.hv1(); let hv2 = self.hv2(); @@ -1694,12 +1269,7 @@ impl DualRowConstraints { pub fn instruction_pop( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { [self.step_1(), self.shrink_stack(), self.keep_ram()].concat() } @@ -1707,12 +1277,7 @@ impl DualRowConstraints { /// $st0_next == nia => st0_next - nia == 0$ pub fn instruction_push( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![self.st0_next() - self.nia()]; [ specific_constraints, @@ -1725,23 +1290,13 @@ impl DualRowConstraints { pub fn instruction_divine( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { [self.step_1(), self.grow_stack(), self.keep_ram()].concat() } pub fn instruction_dup( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![ self.indicator_polynomial(0) * (self.st0_next() - self.st0()), self.indicator_polynomial(1) * (self.st0_next() - self.st1()), @@ -1772,12 +1327,7 @@ impl DualRowConstraints { pub fn instruction_swap( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![ self.indicator_polynomial(0), self.indicator_polynomial(1) * (self.st1_next() - self.st0()), @@ -1839,23 +1389,13 @@ impl DualRowConstraints { pub fn instruction_nop( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { [self.step_1(), self.keep_stack(), self.keep_ram()].concat() } pub fn instruction_skiz( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // The next instruction nia is decomposed into helper variables hv. let nia_decomposes_to_hvs = self.nia() - (self.hv0() + self.two() * self.hv1()); @@ -1893,12 +1433,7 @@ impl DualRowConstraints { pub fn instruction_call( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // The jump stack pointer jsp is incremented by 1. let jsp_incr_1 = self.jsp_next() - (self.jsp() + self.one()); @@ -1922,12 +1457,7 @@ impl DualRowConstraints { pub fn instruction_return( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // The jump stack pointer jsp is decremented by 1. let jsp_incr_1 = self.jsp_next() - (self.jsp() - self.one()); @@ -1940,12 +1470,7 @@ impl DualRowConstraints { pub fn instruction_recurse( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // The instruction pointer ip is set to the last jump's destination jsd. let ip_becomes_jsd = self.ip_next() - self.jsd(); let specific_constraints = vec![ip_becomes_jsd]; @@ -1960,12 +1485,7 @@ impl DualRowConstraints { pub fn instruction_assert( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // The current top of the stack st0 is 1. let st_0_is_1 = self.st0() - self.one(); @@ -1981,12 +1501,7 @@ impl DualRowConstraints { pub fn instruction_halt( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // The instruction executed in the following step is instruction halt. let halt_is_followed_by_halt = self.ci_next() - self.ci(); @@ -2002,12 +1517,7 @@ impl DualRowConstraints { pub fn instruction_read_mem( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // the RAM pointer is overwritten with st0 let update_ramp = self.ramp_next() - self.st0(); @@ -2020,12 +1530,7 @@ impl DualRowConstraints { pub fn instruction_write_mem( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // the RAM pointer is overwritten with st1 let update_ramp = self.ramp_next() - self.st1(); @@ -2039,12 +1544,7 @@ impl DualRowConstraints { /// Two Evaluation Arguments with the Hash Table guarantee correct transition. pub fn instruction_hash( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { [ self.step_1(), self.stack_remains_and_top_ten_elements_unconstrained(), @@ -2059,12 +1559,7 @@ impl DualRowConstraints { /// st10 mod 2. The second polynomial sets the new value of st10 to st10 div 2. pub fn instruction_divine_sibling( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // Helper variable hv0 is either 0 or 1. let hv0_is_0_or_1 = self.hv0() * (self.hv0() - self.one()); @@ -2103,12 +1598,7 @@ impl DualRowConstraints { pub fn instruction_assert_vector( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![ // Register st0 is equal to st5. self.st5() - self.st0(), @@ -2130,12 +1620,7 @@ impl DualRowConstraints { pub fn instruction_absorb_init( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // no further constraints let specific_constraints = vec![]; [ @@ -2149,12 +1634,7 @@ impl DualRowConstraints { pub fn instruction_absorb( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // no further constraints let specific_constraints = vec![]; [ @@ -2168,12 +1648,7 @@ impl DualRowConstraints { pub fn instruction_squeeze( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // no further constraints let specific_constraints = vec![]; [ @@ -2190,12 +1665,7 @@ impl DualRowConstraints { /// $st0' - (st0 + st1) = 0$ pub fn instruction_add( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![self.st0_next() - (self.st0() + self.st1())]; [ specific_constraints, @@ -2211,12 +1681,7 @@ impl DualRowConstraints { /// $st0' - (st0 * st1) = 0$ pub fn instruction_mul( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![self.st0_next() - (self.st0() * self.st1())]; [ specific_constraints, @@ -2232,12 +1697,7 @@ impl DualRowConstraints { /// $st0'·st0 - 1 = 0$ pub fn instruction_invert( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![self.st0_next() * self.st0() - self.one()]; [ specific_constraints, @@ -2250,12 +1710,7 @@ impl DualRowConstraints { pub fn instruction_eq( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // Helper variable hv0 is the inverse of the difference of the stack's two top-most elements or 0. // // $ hv0·(hv0·(st1 - st0) - 1) = 0 $ @@ -2290,12 +1745,7 @@ impl DualRowConstraints { pub fn instruction_split( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let two_pow_32 = self.constant_b(BFieldElement::new(1_u64 << 32)); // The top of the stack is decomposed as 32-bit chunks into the stack's top-most elements. @@ -2334,12 +1784,7 @@ impl DualRowConstraints { pub fn instruction_lt( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // no further constraints let specific_constraints = vec![]; [ @@ -2353,12 +1798,7 @@ impl DualRowConstraints { pub fn instruction_and( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // no further constraints let specific_constraints = vec![]; [ @@ -2372,12 +1812,7 @@ impl DualRowConstraints { pub fn instruction_xor( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // no further constraints let specific_constraints = vec![]; [ @@ -2391,12 +1826,7 @@ impl DualRowConstraints { pub fn instruction_log_2_floor( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // no further constraints let specific_constraints = vec![]; [ @@ -2410,12 +1840,7 @@ impl DualRowConstraints { pub fn instruction_pow( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // no further constraints let specific_constraints = vec![]; [ @@ -2429,12 +1854,7 @@ impl DualRowConstraints { pub fn instruction_div( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // `n == d·q + r` means `st0 - st1·st1' - st0'` let numerator_is_quotient_times_denominator_plus_remainder = self.st0() - self.st1() * self.st1_next() - self.st0_next(); @@ -2456,12 +1876,7 @@ impl DualRowConstraints { pub fn instruction_xxadd( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // The result of adding st0 to st3 is moved into st0. let st0_becomes_st0_plus_st3 = self.st0_next() - (self.st0() + self.st3()); @@ -2487,12 +1902,7 @@ impl DualRowConstraints { pub fn instruction_xxmul( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // The coefficient of x^0 of multiplying the two X-Field elements on the stack is moved into st0. // // $st0' - (st0·st3 - st2·st4 - st1·st5)$ @@ -2532,12 +1942,7 @@ impl DualRowConstraints { pub fn instruction_xinv( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // The coefficient of x^0 of multiplying X-Field element on top of the current stack and on top of the next stack is 1. // // $st0·st0' - st2·st1' - st1·st2' - 1 = 0$ @@ -2579,12 +1984,7 @@ impl DualRowConstraints { pub fn instruction_xbmul( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { // The result of multiplying the top of the stack with the X-Field element's coefficient for x^0 is moved into st0. // // st0' - st0·st1 @@ -2619,12 +2019,7 @@ impl DualRowConstraints { /// An Evaluation Argument with the list of input symbols guarantees correct transition. pub fn instruction_read_io( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { [self.step_1(), self.grow_stack(), self.keep_ram()].concat() } @@ -2633,521 +2028,345 @@ impl DualRowConstraints { /// An Evaluation Argument with the list of output symbols guarantees correct transition. pub fn instruction_write_io( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { [self.step_1(), self.shrink_stack(), self.keep_ram()].concat() } pub fn zero( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.zero.to_owned() } pub fn one( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.one.to_owned() } pub fn two( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.two.to_owned() } pub fn constant( &self, constant: u32, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.circuit_builder.b_constant(constant.into()) } pub fn constant_b( &self, constant: BFieldElement, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.circuit_builder.b_constant(constant) } pub fn clk( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[CLK.master_base_table_index()].clone() } pub fn ip( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[IP.master_base_table_index()].clone() } pub fn ci( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[CI.master_base_table_index()].clone() } pub fn nia( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[NIA.master_base_table_index()].clone() } pub fn ib0( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[IB0.master_base_table_index()].clone() } pub fn ib1( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[IB1.master_base_table_index()].clone() } pub fn ib2( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[IB2.master_base_table_index()].clone() } pub fn ib3( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[IB3.master_base_table_index()].clone() } pub fn ib4( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[IB4.master_base_table_index()].clone() } pub fn ib5( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[IB5.master_base_table_index()].clone() } pub fn ib6( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[IB6.master_base_table_index()].clone() } pub fn ib7( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[IB7.master_base_table_index()].clone() } pub fn jsp( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[JSP.master_base_table_index()].clone() } pub fn jsd( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[JSD.master_base_table_index()].clone() } pub fn jso( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[JSO.master_base_table_index()].clone() } pub fn st0( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST0.master_base_table_index()].clone() } pub fn st1( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST1.master_base_table_index()].clone() } pub fn st2( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST2.master_base_table_index()].clone() } pub fn st3( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST3.master_base_table_index()].clone() } pub fn st4( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST4.master_base_table_index()].clone() } pub fn st5( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST5.master_base_table_index()].clone() } pub fn st6( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST6.master_base_table_index()].clone() } pub fn st7( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST7.master_base_table_index()].clone() } pub fn st8( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST8.master_base_table_index()].clone() } pub fn st9( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST9.master_base_table_index()].clone() } pub fn st10( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST10.master_base_table_index()].clone() } pub fn st11( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST11.master_base_table_index()].clone() } pub fn st12( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST12.master_base_table_index()].clone() } pub fn st13( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST13.master_base_table_index()].clone() } pub fn st14( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST14.master_base_table_index()].clone() } pub fn st15( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[ST15.master_base_table_index()].clone() } pub fn osp( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[OSP.master_base_table_index()].clone() } pub fn osv( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[OSV.master_base_table_index()].clone() } pub fn hv0( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[HV0.master_base_table_index()].clone() } pub fn hv1( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[HV1.master_base_table_index()].clone() } pub fn hv2( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[HV2.master_base_table_index()].clone() } pub fn hv3( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[HV3.master_base_table_index()].clone() } pub fn ramp( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[RAMP.master_base_table_index()].clone() } pub fn previous_instruction( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[PreviousInstruction.master_base_table_index()].clone() } pub fn ramv( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[RAMV.master_base_table_index()].clone() } pub fn is_padding( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_base_row_variables[IsPadding.master_base_table_index()].clone() } pub fn running_evaluation_standard_input( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_ext_row_variables[InputTableEvalArg.master_ext_table_index()].clone() } pub fn running_evaluation_standard_output( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_ext_row_variables[OutputTableEvalArg.master_ext_table_index()].clone() } pub fn instruction_lookup_log_derivative( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_ext_row_variables [InstructionLookupClientLogDerivative.master_ext_table_index()] .clone() } pub fn running_product_op_stack_table( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_ext_row_variables[OpStackTablePermArg.master_ext_table_index()].clone() } pub fn running_product_ram_table( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_ext_row_variables[RamTablePermArg.master_ext_table_index()].clone() } pub fn running_product_jump_stack_table( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_ext_row_variables[JumpStackTablePermArg.master_ext_table_index()].clone() } pub fn clock_jump_difference_lookup_server_log_derivative( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_ext_row_variables [ClockJumpDifferenceLookupServerLogDerivative.master_ext_table_index()] .clone() } pub fn running_evaluation_hash_input( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_ext_row_variables[HashInputEvalArg.master_ext_table_index()].clone() } pub fn running_evaluation_hash_digest( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_ext_row_variables[HashDigestEvalArg.master_ext_table_index()].clone() } pub fn running_evaluation_sponge( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_ext_row_variables[SpongeEvalArg.master_ext_table_index()].clone() } pub fn running_product_u32_table( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.current_ext_row_variables[U32TablePermArg.master_ext_table_index()].clone() } @@ -3155,327 +2374,216 @@ impl DualRowConstraints { // variable position / value as the one without '_next', +/- NUM_COLUMNS. pub fn clk_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[CLK.master_base_table_index()].clone() } pub fn ip_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[IP.master_base_table_index()].clone() } pub fn ci_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[CI.master_base_table_index()].clone() } pub fn nia_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[NIA.master_base_table_index()].clone() } pub fn ib0_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[IB0.master_base_table_index()].clone() } pub fn ib1_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[IB1.master_base_table_index()].clone() } pub fn ib2_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[IB2.master_base_table_index()].clone() } pub fn ib3_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[IB3.master_base_table_index()].clone() } pub fn ib4_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[IB4.master_base_table_index()].clone() } pub fn ib5_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[IB5.master_base_table_index()].clone() } pub fn ib6_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[IB6.master_base_table_index()].clone() } pub fn ib7_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[IB7.master_base_table_index()].clone() } pub fn jsp_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[JSP.master_base_table_index()].clone() } pub fn jsd_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[JSD.master_base_table_index()].clone() } pub fn jso_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[JSO.master_base_table_index()].clone() } pub fn st0_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST0.master_base_table_index()].clone() } pub fn st1_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST1.master_base_table_index()].clone() } pub fn st2_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST2.master_base_table_index()].clone() } pub fn st3_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST3.master_base_table_index()].clone() } pub fn st4_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST4.master_base_table_index()].clone() } pub fn st5_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST5.master_base_table_index()].clone() } pub fn st6_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST6.master_base_table_index()].clone() } pub fn st7_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST7.master_base_table_index()].clone() } pub fn st8_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST8.master_base_table_index()].clone() } pub fn st9_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST9.master_base_table_index()].clone() } pub fn st10_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST10.master_base_table_index()].clone() } pub fn st11_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST11.master_base_table_index()].clone() } pub fn st12_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST12.master_base_table_index()].clone() } pub fn st13_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST13.master_base_table_index()].clone() } pub fn st14_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST14.master_base_table_index()].clone() } pub fn st15_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[ST15.master_base_table_index()].clone() } pub fn osp_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[OSP.master_base_table_index()].clone() } pub fn osv_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[OSV.master_base_table_index()].clone() } pub fn ramp_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[RAMP.master_base_table_index()].clone() } pub fn previous_instruction_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[PreviousInstruction.master_base_table_index()].clone() } pub fn ramv_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[RAMV.master_base_table_index()].clone() } pub fn clock_jump_difference_lookup_multiplicity_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables [ClockJumpDifferenceLookupMultiplicity.master_base_table_index()] .clone() @@ -3483,113 +2591,72 @@ impl DualRowConstraints { pub fn is_padding_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_base_row_variables[IsPadding.master_base_table_index()].clone() } pub fn running_evaluation_standard_input_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_ext_row_variables[InputTableEvalArg.master_ext_table_index()].clone() } pub fn running_evaluation_standard_output_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_ext_row_variables[OutputTableEvalArg.master_ext_table_index()].clone() } pub fn instruction_lookup_log_derivative_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_ext_row_variables[InstructionLookupClientLogDerivative.master_ext_table_index()] .clone() } pub fn running_product_op_stack_table_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_ext_row_variables[OpStackTablePermArg.master_ext_table_index()].clone() } pub fn running_product_ram_table_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_ext_row_variables[RamTablePermArg.master_ext_table_index()].clone() } pub fn running_product_jump_stack_table_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_ext_row_variables[JumpStackTablePermArg.master_ext_table_index()].clone() } pub fn clock_jump_difference_lookup_server_log_derivative_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_ext_row_variables [ClockJumpDifferenceLookupServerLogDerivative.master_ext_table_index()] .clone() } pub fn running_evaluation_hash_input_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_ext_row_variables[HashInputEvalArg.master_ext_table_index()].clone() } pub fn running_evaluation_hash_digest_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_ext_row_variables[HashDigestEvalArg.master_ext_table_index()].clone() } pub fn running_evaluation_sponge_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_ext_row_variables[SpongeEvalArg.master_ext_table_index()].clone() } pub fn running_product_u32_table_next( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.next_ext_row_variables[U32TablePermArg.master_ext_table_index()].clone() } pub fn decompose_arg( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let hv0_is_a_bit = self.hv0() * (self.hv0() - self.one()); let hv1_is_a_bit = self.hv1() * (self.hv1() - self.one()); let hv2_is_a_bit = self.hv2() * (self.hv2() - self.one()); @@ -3610,12 +2677,7 @@ impl DualRowConstraints { pub fn keep_jump_stack( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let jsp_does_not_change = self.jsp_next() - self.jsp(); let jso_does_not_change = self.jso_next() - self.jso(); let jsd_does_not_change = self.jsd_next() - self.jsd(); @@ -3628,12 +2690,7 @@ impl DualRowConstraints { pub fn step_1( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let instruction_pointer_increases_by_one = self.ip_next() - self.ip() - self.one(); let specific_constraints = vec![instruction_pointer_increases_by_one]; [specific_constraints, self.keep_jump_stack()].concat() @@ -3641,12 +2698,7 @@ impl DualRowConstraints { pub fn step_2( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let instruction_pointer_increases_by_two = self.ip_next() - self.ip() - self.two(); let specific_constraints = vec![instruction_pointer_increases_by_two]; [specific_constraints, self.keep_jump_stack()].concat() @@ -3654,12 +2706,7 @@ impl DualRowConstraints { pub fn grow_stack_and_top_two_elements_unconstrained( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { vec![ // The stack element in st1 is moved into st2. self.st2_next() - self.st1(), @@ -3686,12 +2733,7 @@ impl DualRowConstraints { pub fn grow_stack( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![ // The stack element in st0 is moved into st1. self.st1_next() - self.st0(), @@ -3705,12 +2747,7 @@ impl DualRowConstraints { pub fn stack_shrinks_and_top_three_elements_unconstrained( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { vec![ // The stack element in st4 is moved into st3. self.st3_next() - self.st4(), @@ -3738,12 +2775,7 @@ impl DualRowConstraints { pub fn binop( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![ // The stack element in st2 is moved into st1. self.st1_next() - self.st2(), @@ -3759,24 +2791,14 @@ impl DualRowConstraints { pub fn shrink_stack( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constrants = vec![self.st0_next() - self.st1()]; [specific_constrants, self.binop()].concat() } pub fn stack_remains_and_top_eleven_elements_unconstrained( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { vec![ self.st11_next() - self.st11(), self.st12_next() - self.st12(), @@ -3792,12 +2814,7 @@ impl DualRowConstraints { pub fn stack_remains_and_top_ten_elements_unconstrained( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![self.st10_next() - self.st10()]; [ specific_constraints, @@ -3808,12 +2825,7 @@ impl DualRowConstraints { pub fn stack_remains_and_top_three_elements_unconstrained( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![ self.st3_next() - self.st3(), self.st4_next() - self.st4(), @@ -3832,12 +2844,7 @@ impl DualRowConstraints { pub fn unop( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![ // The stack element in st1 does not change. self.st1_next() - self.st1(), @@ -3853,24 +2860,14 @@ impl DualRowConstraints { pub fn keep_stack( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let specific_constraints = vec![self.st0_next() - self.st0()]; [specific_constraints, self.unop()].concat() } pub fn keep_ram( &self, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { vec![ self.ramv_next() - self.ramv(), self.ramp_next() - self.ramp(), @@ -3879,13 +2876,8 @@ impl DualRowConstraints { pub fn running_evaluation_for_standard_input_updates_correctly( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { - let indeterminate = self - .circuit_builder - .challenge(StandardInputEvalIndeterminate); + ) -> ConstraintCircuitMonad> { + let indeterminate = self.circuit_builder.challenge(StandardInputIndeterminate); let read_io_deselector = InstructionDeselectors::instruction_deselector(self, Instruction::ReadIo); let read_io_selector = self.ci() - self.constant_b(Instruction::ReadIo.opcode_b()); @@ -3902,18 +2894,13 @@ impl DualRowConstraints { pub fn log_derivative_for_instruction_lookup_updates_correctly( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { let indeterminate = self .circuit_builder .challenge(InstructionLookupIndeterminate); - let ip_weight = self.circuit_builder.challenge(ProgramTableIpWeight); - let ci_weight = self - .circuit_builder - .challenge(ProgramTableCiProcessorWeight); - let nia_weight = self.circuit_builder.challenge(ProgramTableNiaWeight); + let ip_weight = self.circuit_builder.challenge(ProgramAddressWeight); + let ci_weight = self.circuit_builder.challenge(ProgramInstructionWeight); + let nia_weight = self.circuit_builder.challenge(ProgramNextInstructionWeight); let compressed_row = ip_weight * self.ip_next() + ci_weight * self.ci_next() + nia_weight * self.nia_next(); let log_derivative_updates = (self.instruction_lookup_log_derivative_next() @@ -3929,13 +2916,8 @@ impl DualRowConstraints { pub fn running_evaluation_for_standard_output_updates_correctly( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { - let indeterminate = self - .circuit_builder - .challenge(StandardOutputEvalIndeterminate); + ) -> ConstraintCircuitMonad> { + let indeterminate = self.circuit_builder.challenge(StandardOutputIndeterminate); let write_io_deselector = InstructionDeselectors::instruction_deselector_next(self, Instruction::WriteIo); let write_io_selector = self.ci_next() - self.constant_b(Instruction::WriteIo.opcode_b()); @@ -3952,15 +2934,12 @@ impl DualRowConstraints { pub fn running_product_for_op_stack_table_updates_correctly( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { - let indeterminate = self.circuit_builder.challenge(OpStackPermIndeterminate); - let clk_weight = self.circuit_builder.challenge(OpStackTableClkWeight); - let ib1_weight = self.circuit_builder.challenge(OpStackTableIb1Weight); - let osp_weight = self.circuit_builder.challenge(OpStackTableOspWeight); - let osv_weight = self.circuit_builder.challenge(OpStackTableOsvWeight); + ) -> ConstraintCircuitMonad> { + let indeterminate = self.circuit_builder.challenge(OpStackIndeterminate); + let clk_weight = self.circuit_builder.challenge(OpStackClkWeight); + let ib1_weight = self.circuit_builder.challenge(OpStackIb1Weight); + let osp_weight = self.circuit_builder.challenge(OpStackOspWeight); + let osv_weight = self.circuit_builder.challenge(OpStackOsvWeight); let compressed_row = clk_weight * self.clk_next() + ib1_weight * self.ib1_next() + osp_weight * self.osp_next() @@ -3972,17 +2951,13 @@ impl DualRowConstraints { pub fn running_product_for_ram_table_updates_correctly( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { - let indeterminate = self.circuit_builder.challenge(RamPermIndeterminate); - let clk_weight = self.circuit_builder.challenge(RamTableClkWeight); - let ramp_weight = self.circuit_builder.challenge(RamTableRampWeight); - let ramv_weight = self.circuit_builder.challenge(RamTableRamvWeight); - let previous_instruction_weight = self - .circuit_builder - .challenge(RamTablePreviousInstructionWeight); + ) -> ConstraintCircuitMonad> { + let indeterminate = self.circuit_builder.challenge(RamIndeterminate); + let clk_weight = self.circuit_builder.challenge(RamClkWeight); + let ramp_weight = self.circuit_builder.challenge(RamRampWeight); + let ramv_weight = self.circuit_builder.challenge(RamRamvWeight); + let previous_instruction_weight = + self.circuit_builder.challenge(RamPreviousInstructionWeight); let compressed_row = clk_weight * self.clk_next() + ramp_weight * self.ramp_next() + ramv_weight * self.ramv_next() @@ -3994,16 +2969,13 @@ impl DualRowConstraints { pub fn running_product_for_jump_stack_table_updates_correctly( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { - let indeterminate = self.circuit_builder.challenge(JumpStackPermIndeterminate); - let clk_weight = self.circuit_builder.challenge(JumpStackTableClkWeight); - let ci_weight = self.circuit_builder.challenge(JumpStackTableCiWeight); - let jsp_weight = self.circuit_builder.challenge(JumpStackTableJspWeight); - let jso_weight = self.circuit_builder.challenge(JumpStackTableJsoWeight); - let jsd_weight = self.circuit_builder.challenge(JumpStackTableJsdWeight); + ) -> ConstraintCircuitMonad> { + let indeterminate = self.circuit_builder.challenge(JumpStackIndeterminate); + let clk_weight = self.circuit_builder.challenge(JumpStackClkWeight); + let ci_weight = self.circuit_builder.challenge(JumpStackCiWeight); + let jsp_weight = self.circuit_builder.challenge(JumpStackJspWeight); + let jso_weight = self.circuit_builder.challenge(JumpStackJsoWeight); + let jsd_weight = self.circuit_builder.challenge(JumpStackJsdWeight); let compressed_row = clk_weight * self.clk_next() + ci_weight * self.ci_next() + jsp_weight * self.jsp_next() @@ -4016,15 +2988,12 @@ impl DualRowConstraints { pub fn running_evaluation_hash_input_updates_correctly( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { let hash_deselector = InstructionDeselectors::instruction_deselector_next(self, Instruction::Hash); let hash_selector = self.ci_next() - self.constant_b(Instruction::Hash.opcode_b()); - let indeterminate = self.circuit_builder.challenge(HashInputEvalIndeterminate); + let indeterminate = self.circuit_builder.challenge(HashInputIndeterminate); let weights = [ HashStateWeight0, @@ -4067,15 +3036,12 @@ impl DualRowConstraints { pub fn running_evaluation_hash_digest_updates_correctly( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { let hash_deselector = InstructionDeselectors::instruction_deselector(self, Instruction::Hash); let hash_selector = self.ci() - self.constant_b(Instruction::Hash.opcode_b()); - let indeterminate = self.circuit_builder.challenge(HashDigestEvalIndeterminate); + let indeterminate = self.circuit_builder.challenge(HashDigestIndeterminate); let weights = [ HashStateWeight0, @@ -4108,10 +3074,7 @@ impl DualRowConstraints { pub fn running_evaluation_sponge_updates_correctly( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { let absorb_init_deselector = InstructionDeselectors::instruction_deselector(self, Instruction::AbsorbInit); let absorb_deselector = @@ -4157,8 +3120,8 @@ impl DualRowConstraints { .map(|(weight, st_next)| weight * st_next) .sum(); - let indeterminate = self.circuit_builder.challenge(SpongeEvalIndeterminate); - let ci_weight = self.circuit_builder.challenge(HashTableCIWeight); + let indeterminate = self.circuit_builder.challenge(SpongeIndeterminate); + let ci_weight = self.circuit_builder.challenge(HashCIWeight); let running_evaluation_updates = self.running_evaluation_sponge_next() - indeterminate * self.running_evaluation_sponge() - ci_weight * self.ci() @@ -4174,15 +3137,12 @@ impl DualRowConstraints { pub fn running_product_to_u32_table_updates_correctly( &self, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { - let indeterminate = self.circuit_builder.challenge(U32PermIndeterminate); - let lhs_weight = self.circuit_builder.challenge(U32TableLhsWeight); - let rhs_weight = self.circuit_builder.challenge(U32TableRhsWeight); - let ci_weight = self.circuit_builder.challenge(U32TableCiWeight); - let result_weight = self.circuit_builder.challenge(U32TableResultWeight); + ) -> ConstraintCircuitMonad> { + let indeterminate = self.circuit_builder.challenge(U32Indeterminate); + let lhs_weight = self.circuit_builder.challenge(U32LhsWeight); + let rhs_weight = self.circuit_builder.challenge(U32RhsWeight); + let ci_weight = self.circuit_builder.challenge(U32CiWeight); + let result_weight = self.circuit_builder.challenge(U32ResultWeight); let split_deselector = InstructionDeselectors::instruction_deselector(self, Instruction::Split); @@ -4246,10 +3206,7 @@ impl DualRowConstraints { pub struct InstructionDeselectors { deselectors: HashMap< Instruction, - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, + ConstraintCircuitMonad>, >, } @@ -4268,10 +3225,7 @@ impl InstructionDeselectors { pub fn get( &self, instruction: Instruction, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { self.deselectors .get(&instruction) .unwrap_or_else(|| panic!("The instruction {instruction} does not exist!")) @@ -4281,11 +3235,10 @@ impl InstructionDeselectors { /// internal helper function to de-duplicate functionality common between the similar (but /// different on a type level) functions for construction deselectors fn instruction_deselector_common_functionality( - circuit_builder: &ConstraintCircuitBuilder, + circuit_builder: &ConstraintCircuitBuilder, instruction: Instruction, - instruction_bucket_polynomials: [ConstraintCircuitMonad; - Ord8::COUNT], - ) -> ConstraintCircuitMonad { + instruction_bucket_polynomials: [ConstraintCircuitMonad; Ord8::COUNT], + ) -> ConstraintCircuitMonad { let one = circuit_builder.b_constant(1u32.into()); let selector_bits: [_; Ord8::COUNT] = [ @@ -4312,10 +3265,7 @@ impl InstructionDeselectors { pub fn instruction_deselector( factory: &DualRowConstraints, instruction: Instruction, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { let instruction_bucket_polynomials = [ factory.ib0(), factory.ib1(), @@ -4338,10 +3288,7 @@ impl InstructionDeselectors { pub fn instruction_deselector_single_row( factory: &SingleRowConstraints, instruction: Instruction, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - SingleRowIndicator, - > { + ) -> ConstraintCircuitMonad> { let instruction_bucket_polynomials = [ factory.ib0(), factory.ib1(), @@ -4364,10 +3311,7 @@ impl InstructionDeselectors { pub fn instruction_deselector_next( factory: &DualRowConstraints, instruction: Instruction, - ) -> ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - > { + ) -> ConstraintCircuitMonad> { let instruction_bucket_polynomials = [ factory.ib0_next(), factory.ib1_next(), @@ -4390,10 +3334,7 @@ impl InstructionDeselectors { factory: &mut DualRowConstraints, ) -> HashMap< Instruction, - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, + ConstraintCircuitMonad>, > { all_instructions_without_args() .into_iter() @@ -4599,7 +3540,6 @@ mod constraint_polynomial_tests { use crate::shared_tests::SourceCodeAndInput; use crate::stark::triton_stark_tests::parse_simulate_pad; - use crate::table::challenges::AllChallenges; use crate::table::master_table::MasterTable; use crate::table::processor_table::ProcessorTraceRow; use crate::vm::simulate_no_input; @@ -4627,12 +3567,7 @@ mod constraint_polynomial_tests { fn get_transition_constraints_for_instruction( instruction: Instruction, - ) -> Vec< - ConstraintCircuitMonad< - ProcessorTableChallenges, - DualRowIndicator, - >, - > { + ) -> Vec>> { let tc = DualRowConstraints::default(); match instruction { Pop => tc.instruction_pop(), @@ -4681,7 +3616,7 @@ mod constraint_polynomial_tests { debug_cols_curr_row: &[ProcessorBaseTableColumn], debug_cols_next_row: &[ProcessorBaseTableColumn], ) { - let challenges = AllChallenges::placeholder(&[], &[]); + let challenges = Challenges::placeholder(&[], &[]); let fake_ext_table = Array2::zeros([2, NUM_EXT_COLUMNS]); for (case_idx, test_rows) in master_base_tables.iter().enumerate() { let curr_row = test_rows.slice(s![0, ..]); @@ -4712,7 +3647,7 @@ mod constraint_polynomial_tests { let evaluation_result = constraint_circuit.consume().evaluate( test_rows.view(), fake_ext_table.view(), - &challenges.processor_table_challenges, + &challenges, ); assert_eq!( XFieldElement::zero(), @@ -5060,7 +3995,7 @@ mod constraint_polynomial_tests { let master_ext_table = Array2::zeros([2, NUM_EXT_COLUMNS]); // We need dummy challenges to evaluate. - let dummy_challenges = AllChallenges::placeholder(&[], &[]); + let dummy_challenges = Challenges::placeholder(&[], &[]); for instruction in all_instructions_without_args() { use ProcessorBaseTableColumn::*; let deselector = deselectors.get(instruction); @@ -5084,7 +4019,7 @@ mod constraint_polynomial_tests { let result = deselector.clone().consume().evaluate( master_base_table.view(), master_ext_table.view(), - &dummy_challenges.processor_table_challenges, + &dummy_challenges, ); assert!( @@ -5108,7 +4043,7 @@ mod constraint_polynomial_tests { let result = deselector.consume().evaluate( master_base_table.view(), master_ext_table.view(), - &dummy_challenges.processor_table_challenges, + &dummy_challenges, ); assert!( !result.is_zero(), diff --git a/triton-vm/src/table/program_table.rs b/triton-vm/src/table/program_table.rs index 178bdd140..6ea8157ba 100644 --- a/triton-vm/src/table/program_table.rs +++ b/triton-vm/src/table/program_table.rs @@ -5,16 +5,12 @@ use ndarray::ArrayViewMut2; use num_traits::One; use num_traits::Zero; use strum::EnumCount; -use strum_macros::Display; -use strum_macros::EnumCount as EnumCountMacro; -use strum_macros::EnumIter; use twenty_first::shared_math::b_field_element::BFieldElement; use twenty_first::shared_math::traits::Inverse; use twenty_first::shared_math::x_field_element::XFieldElement; -use ProgramTableChallengeId::*; - -use crate::table::challenges::TableChallenges; +use crate::table::challenges::ChallengeId::*; +use crate::table::challenges::Challenges; use crate::table::constraint_circuit::ConstraintCircuit; use crate::table::constraint_circuit::ConstraintCircuitBuilder; use crate::table::constraint_circuit::DualRowIndicator; @@ -35,10 +31,6 @@ use crate::table::table_column::ProgramExtTableColumn; use crate::table::table_column::ProgramExtTableColumn::*; use crate::vm::AlgebraicExecutionTrace; -pub const PROGRAM_TABLE_NUM_PERMUTATION_ARGUMENTS: usize = 0; -pub const PROGRAM_TABLE_NUM_EVALUATION_ARGUMENTS: usize = 1; -pub const PROGRAM_TABLE_NUM_EXTENSION_CHALLENGES: usize = ProgramTableChallengeId::COUNT; - pub const BASE_WIDTH: usize = ProgramBaseTableColumn::COUNT; pub const EXT_WIDTH: usize = ProgramExtTableColumn::COUNT; pub const FULL_WIDTH: usize = BASE_WIDTH + EXT_WIDTH; @@ -50,12 +42,8 @@ pub struct ProgramTable {} pub struct ExtProgramTable {} impl ExtProgramTable { - pub fn ext_initial_constraints_as_circuits() -> Vec< - ConstraintCircuit< - ProgramTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_initial_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let address = circuit_builder.input(BaseRow(Address.master_base_table_index())); @@ -75,12 +63,8 @@ impl ExtProgramTable { ] } - pub fn ext_consistency_constraints_as_circuits() -> Vec< - ConstraintCircuit< - ProgramTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_consistency_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let one = circuit_builder.b_constant(1_u32.into()); @@ -90,12 +74,8 @@ impl ExtProgramTable { vec![is_padding_is_bit.consume()] } - pub fn ext_transition_constraints_as_circuits() -> Vec< - ConstraintCircuit< - ProgramTableChallenges, - DualRowIndicator, - >, - > { + pub fn ext_transition_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let one = circuit_builder.b_constant(1u32.into()); let address = circuit_builder.input(CurrentBaseRow(Address.master_base_table_index())); @@ -121,9 +101,9 @@ impl ExtProgramTable { is_padding.clone() * (is_padding_next - is_padding.clone()); let log_derivative_remains = log_derivative_next.clone() - log_derivative.clone(); - let compressed_row = circuit_builder.challenge(AddressWeight) * address - + circuit_builder.challenge(InstructionWeight) * instruction - + circuit_builder.challenge(NextInstructionWeight) * instruction_next; + let compressed_row = circuit_builder.challenge(ProgramAddressWeight) * address + + circuit_builder.challenge(ProgramInstructionWeight) * instruction + + circuit_builder.challenge(ProgramNextInstructionWeight) * instruction_next; let indeterminate = circuit_builder.challenge(InstructionLookupIndeterminate); @@ -143,12 +123,8 @@ impl ExtProgramTable { .to_vec() } - pub fn ext_terminal_constraints_as_circuits() -> Vec< - ConstraintCircuit< - ProgramTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_terminal_constraints_as_circuits( + ) -> Vec>> { // no further constraints vec![] } @@ -193,11 +169,18 @@ impl ProgramTable { pub fn extend( base_table: ArrayView2, mut ext_table: ArrayViewMut2, - challenges: &ProgramTableChallenges, + challenges: &Challenges, ) { assert_eq!(BASE_WIDTH, base_table.ncols()); assert_eq!(EXT_WIDTH, ext_table.ncols()); assert_eq!(base_table.nrows(), ext_table.nrows()); + + let address_weight = challenges.get_challenge(ProgramAddressWeight); + let instruction_weight = challenges.get_challenge(ProgramInstructionWeight); + let next_instruction_weight = challenges.get_challenge(ProgramNextInstructionWeight); + let instruction_lookup_indeterminate = + challenges.get_challenge(InstructionLookupIndeterminate); + let mut instruction_lookup_log_derivative = LookupArg::default_initial(); for (idx, window) in base_table.windows([2, BASE_WIDTH]).into_iter().enumerate() { @@ -218,10 +201,11 @@ impl ProgramTable { let address = row[Address.base_table_index()]; let instruction = row[Instruction.base_table_index()]; let next_instruction = next_row[Instruction.base_table_index()]; - let compressed_row_for_instruction_lookup = address * challenges.address_weight - + instruction * challenges.instruction_weight - + next_instruction * challenges.next_instruction_weight; - instruction_lookup_log_derivative += (challenges.instruction_lookup_indeterminate + + let compressed_row_for_instruction_lookup = address * address_weight + + instruction * instruction_weight + + next_instruction * next_instruction_weight; + instruction_lookup_log_derivative += (instruction_lookup_indeterminate - compressed_row_for_instruction_lookup) .inverse() * lookup_multiplicity; @@ -237,43 +221,3 @@ impl ProgramTable { instruction_lookup_log_derivative; } } - -#[derive(Debug, Copy, Clone, Display, EnumCountMacro, EnumIter, PartialEq, Eq, Hash)] -pub enum ProgramTableChallengeId { - InstructionLookupIndeterminate, - AddressWeight, - InstructionWeight, - NextInstructionWeight, -} - -impl From for usize { - fn from(val: ProgramTableChallengeId) -> Self { - val as usize - } -} - -impl TableChallenges for ProgramTableChallenges { - type Id = ProgramTableChallengeId; - - #[inline] - fn get_challenge(&self, id: Self::Id) -> XFieldElement { - match id { - InstructionLookupIndeterminate => self.instruction_lookup_indeterminate, - AddressWeight => self.address_weight, - InstructionWeight => self.instruction_weight, - NextInstructionWeight => self.next_instruction_weight, - } - } -} - -#[derive(Debug, Clone)] -pub struct ProgramTableChallenges { - /// The weight that combines two consecutive rows in the - /// permutation/evaluation column of the program table. - pub instruction_lookup_indeterminate: XFieldElement, - - /// Weights for condensing part of a row into a single column. (Related to program table.) - pub address_weight: XFieldElement, - pub instruction_weight: XFieldElement, - pub next_instruction_weight: XFieldElement, -} diff --git a/triton-vm/src/table/ram_table.rs b/triton-vm/src/table/ram_table.rs index 9363a016c..90efbfdc9 100644 --- a/triton-vm/src/table/ram_table.rs +++ b/triton-vm/src/table/ram_table.rs @@ -10,18 +10,14 @@ use ndarray::Axis; use num_traits::One; use num_traits::Zero; use strum::EnumCount; -use strum_macros::Display; -use strum_macros::EnumCount as EnumCountMacro; -use strum_macros::EnumIter; use triton_opcodes::instruction::Instruction; use twenty_first::shared_math::b_field_element::BFieldElement; use twenty_first::shared_math::polynomial::Polynomial; use twenty_first::shared_math::traits::Inverse; use twenty_first::shared_math::x_field_element::XFieldElement; -use RamTableChallengeId::*; - -use crate::table::challenges::TableChallenges; +use crate::table::challenges::ChallengeId::*; +use crate::table::challenges::Challenges; use crate::table::constraint_circuit::ConstraintCircuit; use crate::table::constraint_circuit::ConstraintCircuitBuilder; use crate::table::constraint_circuit::DualRowIndicator; @@ -44,10 +40,6 @@ use crate::table::table_column::RamExtTableColumn; use crate::table::table_column::RamExtTableColumn::*; use crate::vm::AlgebraicExecutionTrace; -pub const RAM_TABLE_NUM_PERMUTATION_ARGUMENTS: usize = 1; -pub const RAM_TABLE_NUM_EVALUATION_ARGUMENTS: usize = 0; -pub const RAM_TABLE_NUM_EXTENSION_CHALLENGES: usize = RamTableChallengeId::COUNT; - pub const BASE_WIDTH: usize = RamBaseTableColumn::COUNT; pub const EXT_WIDTH: usize = RamExtTableColumn::COUNT; pub const FULL_WIDTH: usize = BASE_WIDTH + EXT_WIDTH; @@ -240,17 +232,28 @@ impl RamTable { pub fn extend( base_table: ArrayView2, mut ext_table: ArrayViewMut2, - challenges: &RamTableChallenges, + challenges: &Challenges, ) { assert_eq!(BASE_WIDTH, base_table.ncols()); assert_eq!(EXT_WIDTH, ext_table.ncols()); assert_eq!(base_table.nrows(), ext_table.nrows()); + + let clk_weight = challenges.get_challenge(RamClkWeight); + let ramp_weight = challenges.get_challenge(RamRampWeight); + let ramv_weight = challenges.get_challenge(RamRamvWeight); + let previous_instruction_weight = challenges.get_challenge(RamPreviousInstructionWeight); + let processor_perm_indeterminate = challenges.get_challenge(RamIndeterminate); + let bezout_relation_indeterminate = + challenges.get_challenge(RamTableBezoutRelationIndeterminate); + let clock_jump_difference_lookup_indeterminate = + challenges.get_challenge(ClockJumpDifferenceLookupIndeterminate); + let mut running_product_for_perm_arg = PermArg::default_initial(); let mut clock_jump_diff_lookup_log_derivative = LookupArg::default_initial(); // initialize columns establishing Bézout relation let mut running_product_of_ramp = - challenges.bezout_relation_indeterminate - base_table.row(0)[RAMP.base_table_index()]; + bezout_relation_indeterminate - base_table.row(0)[RAMP.base_table_index()]; let mut formal_derivative = XFieldElement::one(); let mut bezout_coefficient_0 = base_table.row(0)[BezoutCoefficientPolynomialCoefficient0.base_table_index()].lift(); @@ -272,31 +275,31 @@ impl RamTable { current_row[BezoutCoefficientPolynomialCoefficient0.base_table_index()]; let bcpc1 = current_row[BezoutCoefficientPolynomialCoefficient1.base_table_index()]; - let bezout_challenge = challenges.bezout_relation_indeterminate; - formal_derivative = - (bezout_challenge - ramp) * formal_derivative + running_product_of_ramp; - running_product_of_ramp *= bezout_challenge - ramp; - bezout_coefficient_0 = bezout_coefficient_0 * bezout_challenge + bcpc0; - bezout_coefficient_1 = bezout_coefficient_1 * bezout_challenge + bcpc1; + formal_derivative = (bezout_relation_indeterminate - ramp) * formal_derivative + + running_product_of_ramp; + running_product_of_ramp *= bezout_relation_indeterminate - ramp; + bezout_coefficient_0 = + bezout_coefficient_0 * bezout_relation_indeterminate + bcpc0; + bezout_coefficient_1 = + bezout_coefficient_1 * bezout_relation_indeterminate + bcpc1; } else { // prove that clock jump is directed forward let clock_jump_difference = current_row[CLK.base_table_index()] - prev_row[CLK.base_table_index()]; - clock_jump_diff_lookup_log_derivative += (challenges - .clock_jump_difference_lookup_indeterminate - - clock_jump_difference) - .inverse(); + clock_jump_diff_lookup_log_derivative += + (clock_jump_difference_lookup_indeterminate - clock_jump_difference) + .inverse(); } } // permutation argument to Processor Table - let compressed_row_for_permutation_argument = clk * challenges.clk_weight - + ramp * challenges.ramp_weight - + ramv * challenges.ramv_weight - + previous_instruction * challenges.previous_instruction_weight; + let compressed_row_for_permutation_argument = clk * clk_weight + + ramp * ramp_weight + + ramv * ramv_weight + + previous_instruction * previous_instruction_weight; running_product_for_perm_arg *= - challenges.processor_perm_indeterminate - compressed_row_for_permutation_argument; + processor_perm_indeterminate - compressed_row_for_permutation_argument; let mut extension_row = ext_table.row_mut(row_idx); extension_row[RunningProductPermArg.ext_table_index()] = running_product_for_perm_arg; @@ -312,19 +315,13 @@ impl RamTable { } impl ExtRamTable { - pub fn ext_initial_constraints_as_circuits() -> Vec< - ConstraintCircuit< - RamTableChallenges, - SingleRowIndicator, - >, - > { - use RamTableChallengeId::*; - + pub fn ext_initial_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let one = circuit_builder.b_constant(1_u32.into()); - let bezout_challenge = circuit_builder.challenge(BezoutRelationIndeterminate); - let rppa_challenge = circuit_builder.challenge(ProcessorPermIndeterminate); + let bezout_challenge = circuit_builder.challenge(RamTableBezoutRelationIndeterminate); + let rppa_challenge = circuit_builder.challenge(RamIndeterminate); let clk = circuit_builder.input(BaseRow(CLK.master_base_table_index())); let ramp = circuit_builder.input(BaseRow(RAMP.master_base_table_index())); @@ -359,10 +356,10 @@ impl ExtRamTable { let clock_jump_diff_log_derivative_is_initialized_correctly = clock_jump_diff_log_derivative - circuit_builder.x_constant(LookupArg::default_initial()); - let clk_weight = circuit_builder.challenge(ClkWeight); - let ramp_weight = circuit_builder.challenge(RampWeight); - let ramv_weight = circuit_builder.challenge(RamvWeight); - let previous_instruction_weight = circuit_builder.challenge(PreviousInstructionWeight); + let clk_weight = circuit_builder.challenge(RamClkWeight); + let ramp_weight = circuit_builder.challenge(RamRampWeight); + let ramv_weight = circuit_builder.challenge(RamRamvWeight); + let previous_instruction_weight = circuit_builder.challenge(RamPreviousInstructionWeight); let compressed_row_for_permutation_argument = clk * clk_weight + ramp * ramp_weight + ramv * ramv_weight @@ -384,28 +381,23 @@ impl ExtRamTable { .to_vec() } - pub fn ext_consistency_constraints_as_circuits() -> Vec< - ConstraintCircuit< - RamTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_consistency_constraints_as_circuits( + ) -> Vec>> { // no further constraints vec![] } - pub fn ext_transition_constraints_as_circuits() -> Vec< - ConstraintCircuit>, - > { + pub fn ext_transition_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let one = circuit_builder.b_constant(1u32.into()); - let bezout_challenge = circuit_builder.challenge(BezoutRelationIndeterminate); - let rppa_challenge = circuit_builder.challenge(ProcessorPermIndeterminate); - let clk_weight = circuit_builder.challenge(ClkWeight); - let ramp_weight = circuit_builder.challenge(RampWeight); - let ramv_weight = circuit_builder.challenge(RamvWeight); - let previous_instruction_weight = circuit_builder.challenge(PreviousInstructionWeight); + let bezout_challenge = circuit_builder.challenge(RamTableBezoutRelationIndeterminate); + let rppa_challenge = circuit_builder.challenge(RamIndeterminate); + let clk_weight = circuit_builder.challenge(RamClkWeight); + let ramp_weight = circuit_builder.challenge(RamRampWeight); + let ramv_weight = circuit_builder.challenge(RamRamvWeight); + let previous_instruction_weight = circuit_builder.challenge(RamPreviousInstructionWeight); let clk = circuit_builder.input(CurrentBaseRow(CLK.master_base_table_index())); let ramp = circuit_builder.input(CurrentBaseRow(RAMP.master_base_table_index())); @@ -540,12 +532,8 @@ impl ExtRamTable { .to_vec() } - pub fn ext_terminal_constraints_as_circuits() -> Vec< - ConstraintCircuit< - RamTableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_terminal_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let one = circuit_builder.b_constant(1_u32.into()); @@ -559,57 +547,3 @@ impl ExtRamTable { vec![bezout_relation_holds.consume()] } } - -#[derive(Debug, Copy, Clone, Display, EnumCountMacro, EnumIter, PartialEq, Eq, Hash)] -pub enum RamTableChallengeId { - BezoutRelationIndeterminate, - ProcessorPermIndeterminate, - ClkWeight, - RamvWeight, - RampWeight, - PreviousInstructionWeight, - ClockJumpDifferenceLookupIndeterminate, -} - -impl From for usize { - fn from(val: RamTableChallengeId) -> Self { - val as usize - } -} - -#[derive(Debug, Clone)] -pub struct RamTableChallenges { - /// The point in which the Bézout relation establishing contiguous memory regions is queried. - pub bezout_relation_indeterminate: XFieldElement, - - /// Point of evaluation for the row set equality argument between RAM and Processor Tables - pub processor_perm_indeterminate: XFieldElement, - - /// Weights for condensing part of a row into a single column. (Related to processor table.) - pub clk_weight: XFieldElement, - pub ramp_weight: XFieldElement, - pub ramv_weight: XFieldElement, - pub previous_instruction_weight: XFieldElement, - - /// Indeterminate for the logarithmic derivative of the clock jump difference's Lookup Argument. - pub clock_jump_difference_lookup_indeterminate: XFieldElement, -} - -impl TableChallenges for RamTableChallenges { - type Id = RamTableChallengeId; - - #[inline] - fn get_challenge(&self, id: Self::Id) -> XFieldElement { - match id { - BezoutRelationIndeterminate => self.bezout_relation_indeterminate, - ProcessorPermIndeterminate => self.processor_perm_indeterminate, - ClkWeight => self.clk_weight, - RamvWeight => self.ramv_weight, - RampWeight => self.ramp_weight, - PreviousInstructionWeight => self.previous_instruction_weight, - ClockJumpDifferenceLookupIndeterminate => { - self.clock_jump_difference_lookup_indeterminate - } - } - } -} diff --git a/triton-vm/src/table/u32_table.rs b/triton-vm/src/table/u32_table.rs index 7bb023b08..48e656cdd 100644 --- a/triton-vm/src/table/u32_table.rs +++ b/triton-vm/src/table/u32_table.rs @@ -1,6 +1,6 @@ -use itertools::Itertools; use std::ops::Mul; +use itertools::Itertools; use ndarray::parallel::prelude::*; use ndarray::s; use ndarray::Array1; @@ -11,17 +11,13 @@ use ndarray::Axis; use num_traits::One; use num_traits::Zero; use strum::EnumCount; -use strum_macros::Display; -use strum_macros::EnumCount as EnumCountMacro; -use strum_macros::EnumIter; +use triton_opcodes::instruction::Instruction; use twenty_first::shared_math::b_field_element::BFieldElement; use twenty_first::shared_math::traits::Inverse; use twenty_first::shared_math::x_field_element::XFieldElement; -use triton_opcodes::instruction::Instruction; -use U32TableChallengeId::*; - -use crate::table::challenges::TableChallenges; +use crate::table::challenges::ChallengeId::*; +use crate::table::challenges::Challenges; use crate::table::constraint_circuit::ConstraintCircuit; use crate::table::constraint_circuit::ConstraintCircuitBuilder; use crate::table::constraint_circuit::ConstraintCircuitMonad; @@ -43,10 +39,6 @@ use crate::table::table_column::U32ExtTableColumn; use crate::table::table_column::U32ExtTableColumn::*; use crate::vm::AlgebraicExecutionTrace; -pub const U32_TABLE_NUM_PERMUTATION_ARGUMENTS: usize = 2; -pub const U32_TABLE_NUM_EVALUATION_ARGUMENTS: usize = 0; -pub const U32_TABLE_NUM_EXTENSION_CHALLENGES: usize = U32TableChallengeId::COUNT; - pub const BASE_WIDTH: usize = U32BaseTableColumn::COUNT; pub const EXT_WIDTH: usize = U32ExtTableColumn::COUNT; pub const FULL_WIDTH: usize = BASE_WIDTH + EXT_WIDTH; @@ -56,12 +48,8 @@ pub struct U32Table {} pub struct ExtU32Table {} impl ExtU32Table { - pub fn ext_initial_constraints_as_circuits() -> Vec< - ConstraintCircuit< - U32TableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_initial_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let challenge = |c| circuit_builder.challenge(c); let one = circuit_builder.b_constant(1_u32.into()); @@ -111,11 +99,11 @@ impl ExtU32Table { * circuit_builder.input(BaseRow(Pow.master_base_table_index())); // + normalized_instruction_deselector(Instruction::Split) * 0, which is superfluous - let initial_factor = challenge(ProcessorPermIndeterminate) - - challenge(LhsWeight) * lhs - - challenge(RhsWeight) * rhs - - challenge(CIWeight) * ci - - challenge(ResultWeight) * result; + let initial_factor = challenge(U32Indeterminate) + - challenge(U32LhsWeight) * lhs + - challenge(U32RhsWeight) * rhs + - challenge(U32CiWeight) * ci + - challenge(U32ResultWeight) * result; let if_copy_flag_is_1_then_rp_has_accumulated_first_row = copy_flag.clone() * (rp.clone() - initial_factor); @@ -131,12 +119,8 @@ impl ExtU32Table { .to_vec() } - pub fn ext_consistency_constraints_as_circuits() -> Vec< - ConstraintCircuit< - U32TableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_consistency_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let one = circuit_builder.b_constant(1_u32.into()); @@ -207,9 +191,8 @@ impl ExtU32Table { .to_vec() } - pub fn ext_transition_constraints_as_circuits() -> Vec< - ConstraintCircuit>, - > { + pub fn ext_transition_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let challenge = |c| circuit_builder.challenge(c); let one = circuit_builder.b_constant(1_u32.into()); @@ -370,12 +353,12 @@ impl ExtU32Table { let if_copy_flag_next_is_0_then_running_product_stays = (copy_flag_next.clone() - one) * (rp_next.clone() - rp.clone()); - let compressed_row_next = challenge(CIWeight) * ci_next - + challenge(LhsWeight) * lhs_next - + challenge(RhsWeight) * rhs_next - + challenge(ResultWeight) * result_next; - let if_copy_flag_next_is_1_then_running_product_absorbs_next_row = copy_flag_next - * (rp_next - rp * (challenge(ProcessorPermIndeterminate) - compressed_row_next)); + let compressed_row_next = challenge(U32CiWeight) * ci_next + + challenge(U32LhsWeight) * lhs_next + + challenge(U32RhsWeight) * rhs_next + + challenge(U32ResultWeight) * result_next; + let if_copy_flag_next_is_1_then_running_product_absorbs_next_row = + copy_flag_next * (rp_next - rp * (challenge(U32Indeterminate) - compressed_row_next)); [ if_copy_flag_next_is_1_then_lhs_is_0, @@ -405,12 +388,8 @@ impl ExtU32Table { .to_vec() } - pub fn ext_terminal_constraints_as_circuits() -> Vec< - ConstraintCircuit< - U32TableChallenges, - SingleRowIndicator, - >, - > { + pub fn ext_terminal_constraints_as_circuits( + ) -> Vec>> { let circuit_builder = ConstraintCircuitBuilder::new(); let lhs = circuit_builder.input(BaseRow(LHS.master_base_table_index())); @@ -546,12 +525,18 @@ impl U32Table { pub fn extend( base_table: ArrayView2, mut ext_table: ArrayViewMut2, - challenges: &U32TableChallenges, + challenges: &Challenges, ) { assert_eq!(BASE_WIDTH, base_table.ncols()); assert_eq!(EXT_WIDTH, ext_table.ncols()); assert_eq!(base_table.nrows(), ext_table.nrows()); + let ci_weight = challenges.get_challenge(U32CiWeight); + let lhs_weight = challenges.get_challenge(U32LhsWeight); + let rhs_weight = challenges.get_challenge(U32RhsWeight); + let result_weight = challenges.get_challenge(U32ResultWeight); + let processor_perm_indeterminate = challenges.get_challenge(U32Indeterminate); + let mut running_product = PermArg::default_initial(); for row_idx in 0..base_table.nrows() { let current_row = base_table.row(row_idx); @@ -570,11 +555,11 @@ impl U32Table { ci => panic!("Instruction in U32 Table must be a u32 instruction. Got {ci}"), }; - let compressed_row = challenges.ci_weight * current_row[CI.base_table_index()] - + challenges.lhs_weight * current_row[LHS.base_table_index()] - + challenges.rhs_weight * current_row[RHS.base_table_index()] - + challenges.result_weight * result; - running_product *= challenges.processor_perm_indeterminate - compressed_row; + let compressed_row = ci_weight * current_row[CI.base_table_index()] + + lhs_weight * current_row[LHS.base_table_index()] + + rhs_weight * current_row[RHS.base_table_index()] + + result_weight * result; + running_product *= processor_perm_indeterminate - compressed_row; } let mut extension_row = ext_table.row_mut(row_idx); @@ -582,42 +567,3 @@ impl U32Table { } } } - -#[repr(usize)] -#[derive(Debug, Copy, Clone, Display, EnumCountMacro, EnumIter, PartialEq, Eq, Hash)] -pub enum U32TableChallengeId { - LhsWeight, - RhsWeight, - CIWeight, - ResultWeight, - ProcessorPermIndeterminate, -} - -impl From for usize { - fn from(val: U32TableChallengeId) -> Self { - val as usize - } -} - -impl TableChallenges for U32TableChallenges { - type Id = U32TableChallengeId; - - fn get_challenge(&self, id: Self::Id) -> XFieldElement { - match id { - LhsWeight => self.lhs_weight, - RhsWeight => self.rhs_weight, - CIWeight => self.ci_weight, - ResultWeight => self.result_weight, - ProcessorPermIndeterminate => self.processor_perm_indeterminate, - } - } -} - -#[derive(Debug, Clone)] -pub struct U32TableChallenges { - pub lhs_weight: XFieldElement, - pub rhs_weight: XFieldElement, - pub ci_weight: XFieldElement, - pub result_weight: XFieldElement, - pub processor_perm_indeterminate: XFieldElement, -}