diff --git a/.gitignore b/.gitignore index 5302249431..a5a46ebb05 100644 --- a/.gitignore +++ b/.gitignore @@ -27,6 +27,7 @@ _build # If symlink created for kimchi-visu tools/srs +.ignore optimism/*op-program-data-log.sh optimism/cpu.pprof optimism/meta.json diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 2ac4a2d8bb..4abb936269 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -9,15 +9,15 @@ - [Rings](./fundamentals/zkbook_rings.md) - [Fields](./fundamentals/zkbook.md) - [Polynomials](./fundamentals/zkbook_polynomials.md) - - [Multiplying polynomials](./fundamentals/zkbook_multiplying_polynomials.md) - - [Fast Fourier transform](./fundamentals/zkbook_fft.md) + - [Multiplying Polynomials](./fundamentals/zkbook_multiplying_polynomials.md) + - [Fast Fourier Transform](./fundamentals/zkbook_fft.md) # Cryptographic Tools - [Commitments](./fundamentals/zkbook_commitment.md) -- [Polynomial commitments](./plonk/polynomial_commitments.md) - - [Inner product argument](./plonk/inner_product.md) - - [Different functionnalities](./plonk/inner_product_api.md) +- [Polynomial Commitments](./plonk/polynomial_commitments.md) + - [Inner Product Argument](./plonk/inner_product.md) + - [Different Functionnalities](./plonk/inner_product_api.md) - [Two Party Computation](./fundamentals/zkbook_2pc/overview.md) - [Garbled Circuits](./fundamentals/zkbook_2pc/gc.md) - [Basics](./fundamentals/zkbook_2pc/basics.md) @@ -70,8 +70,8 @@ # Technical Specifications - [Poseidon hash](./specs/poseidon.md) -- [Polynomial commitment](./specs/poly-commitment.md) -- [Pasta curves](./specs/pasta.md) +- [Polynomial Commitment](./specs/poly-commitment.md) +- [Pasta Curves](./specs/pasta.md) - [Kimchi](./specs/kimchi.md) - [Universal Reference String (URS)](./specs/urs.md) - [Pickles](./specs/pickles.md) diff --git a/book/src/specs/kimchi.md b/book/src/specs/kimchi.md index 6914feac74..dae3877e25 100644 --- a/book/src/specs/kimchi.md +++ b/book/src/specs/kimchi.md @@ -2208,7 +2208,7 @@ The prover then follows the following steps to create the proof: * $s_i$ * $w_i$ * $z$ - * lookup (TODO) + * lookup (TODO, see [this issue](https://github.com/MinaProtocol/mina/issues/13886)) * generic selector * poseidon selector diff --git a/kimchi/Cargo.toml b/kimchi/Cargo.toml index d9415dce18..f1c3042598 100644 --- a/kimchi/Cargo.toml +++ b/kimchi/Cargo.toml @@ -50,7 +50,7 @@ mina-poseidon = { path = "../poseidon", version = "0.1.0" } ocaml = { version = "0.22.2", optional = true } ocaml-gen = { version = "0.1.5", optional = true } -wasm-bindgen = { version = "0.2.81", optional = true } +wasm-bindgen = { version = "=0.2.87", optional = true } internal-tracing = { path = "../internal-tracing", version = "0.1.0" } diff --git a/kimchi/src/circuits/constraints.rs b/kimchi/src/circuits/constraints.rs index 78e1102ec1..83aeb30ffe 100644 --- a/kimchi/src/circuits/constraints.rs +++ b/kimchi/src/circuits/constraints.rs @@ -5,7 +5,11 @@ use crate::{ domain_constant_evaluation::DomainConstantEvaluations, domains::EvaluationDomains, gate::{CircuitGate, GateType}, - lookup::{index::LookupConstraintSystem, lookups::LookupFeatures, tables::LookupTable}, + lookup::{ + index::LookupConstraintSystem, + lookups::LookupFeatures, + tables::{GateLookupTables, LookupTable}, + }, polynomial::{WitnessEvals, WitnessOverDomains, WitnessShifts}, polynomials::permutation::Shifts, wires::*, @@ -32,6 +36,11 @@ use std::sync::Arc; // /// Flags for optional features in the constraint system +#[cfg_attr( + feature = "ocaml_types", + derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct) +)] +#[cfg_attr(feature = "wasm_types", wasm_bindgen::prelude::wasm_bindgen)] #[derive(Copy, Clone, Serialize, Deserialize, Debug)] pub struct FeatureFlags { /// RangeCheck0 gate @@ -614,6 +623,47 @@ pub fn zk_rows_strict_lower_bound(num_chunks: usize) -> usize { (2 * (PERMUTS + 1) * num_chunks - 2) / PERMUTS } +impl FeatureFlags { + pub fn from_gates_and_lookup_features( + gates: &[CircuitGate], + lookup_features: LookupFeatures, + ) -> FeatureFlags { + let mut feature_flags = FeatureFlags { + range_check0: false, + range_check1: false, + lookup_features, + foreign_field_add: false, + foreign_field_mul: false, + xor: false, + rot: false, + }; + + for gate in gates { + match gate.typ { + GateType::RangeCheck0 => feature_flags.range_check0 = true, + GateType::RangeCheck1 => feature_flags.range_check1 = true, + GateType::ForeignFieldAdd => feature_flags.foreign_field_add = true, + GateType::ForeignFieldMul => feature_flags.foreign_field_mul = true, + GateType::Xor16 => feature_flags.xor = true, + GateType::Rot64 => feature_flags.rot = true, + _ => (), + } + } + + feature_flags + } + + pub fn from_gates( + gates: &[CircuitGate], + uses_runtime_tables: bool, + ) -> FeatureFlags { + FeatureFlags::from_gates_and_lookup_features( + gates, + LookupFeatures::from_gates(gates, uses_runtime_tables), + ) + } +} + impl Builder { /// Set up the number of public inputs. /// If not invoked, it equals `0` by default. @@ -682,7 +732,7 @@ impl Builder { // for some reason we need more than 1 gate for the circuit to work, see TODO below assert!(gates.len() > 1); - let lookup_features = LookupFeatures::from_gates(&gates, runtime_tables.is_some()); + let feature_flags = FeatureFlags::from_gates(&gates, runtime_tables.is_some()); let lookup_domain_size = { // First we sum over the lookup table size @@ -705,12 +755,19 @@ impl Builder { } } // And we add the built-in tables, depending on the features. - let LookupFeatures { patterns, .. } = &lookup_features; + let LookupFeatures { patterns, .. } = &feature_flags.lookup_features; + let mut gate_lookup_tables = GateLookupTables { + xor: false, + range_check: false, + }; for pattern in patterns.into_iter() { if let Some(gate_table) = pattern.table() { - lookup_domain_size += gate_table.table_size(); + gate_lookup_tables[gate_table] = true } } + for gate_table in gate_lookup_tables.into_iter() { + lookup_domain_size += gate_table.table_size(); + } lookup_domain_size }; @@ -787,28 +844,6 @@ impl Builder { .collect(); gates.append(&mut padding); - let mut feature_flags = FeatureFlags { - range_check0: false, - range_check1: false, - lookup_features, - foreign_field_add: false, - foreign_field_mul: false, - xor: false, - rot: false, - }; - - for gate in &gates { - match gate.typ { - GateType::RangeCheck0 => feature_flags.range_check0 = true, - GateType::RangeCheck1 => feature_flags.range_check1 = true, - GateType::ForeignFieldAdd => feature_flags.foreign_field_add = true, - GateType::ForeignFieldMul => feature_flags.foreign_field_mul = true, - GateType::Xor16 => feature_flags.xor = true, - GateType::Rot64 => feature_flags.rot = true, - _ => (), - } - } - //~ 1. sample the `PERMUTS` shifts. let shifts = Shifts::new(&domain.d1); diff --git a/kimchi/src/circuits/gate.rs b/kimchi/src/circuits/gate.rs index ec5b2f9377..82e3c76031 100644 --- a/kimchi/src/circuits/gate.rs +++ b/kimchi/src/circuits/gate.rs @@ -209,6 +209,7 @@ impl CircuitGate { EndoMul => self.verify_endomul::(row, witness, &index.cs), EndoMulScalar => self.verify_endomul_scalar::(row, witness, &index.cs), // TODO: implement the verification for the lookup gate + // See https://github.com/MinaProtocol/mina/issues/14011 Lookup => Ok(()), CairoClaim | CairoInstruction | CairoFlags | CairoTransition => { self.verify_cairo_gate::(row, witness, &index.cs) @@ -303,6 +304,7 @@ impl CircuitGate { } GateType::Lookup => { // TODO: implement the verification for the lookup gate + // See https://github.com/MinaProtocol/mina/issues/14011 vec![] } GateType::CairoClaim => turshi::Claim::constraint_checks(&env, &mut cache), diff --git a/kimchi/src/circuits/lookup/constraints.rs b/kimchi/src/circuits/lookup/constraints.rs index 3cbf3f34ad..715b6f2c80 100644 --- a/kimchi/src/circuits/lookup/constraints.rs +++ b/kimchi/src/circuits/lookup/constraints.rs @@ -256,6 +256,8 @@ where .iter() .enumerate() .map(|(i, s)| { + // Snake pattern: even chunks of s are direct + // while the odd ones are reversed let (i1, i2) = if i % 2 == 0 { (row, row + 1) } else { diff --git a/kimchi/src/circuits/lookup/lookups.rs b/kimchi/src/circuits/lookup/lookups.rs index b126e1be00..002b040828 100644 --- a/kimchi/src/circuits/lookup/lookups.rs +++ b/kimchi/src/circuits/lookup/lookups.rs @@ -323,7 +323,6 @@ pub type JointLookupSpec = JointLookup, LookupTableID>; pub type JointLookupValue = JointLookup; impl + From> JointLookupValue { - // TODO: Support multiple tables /// Evaluate the combined value of a joint-lookup. pub fn evaluate(&self, joint_combiner: &F, table_id_combiner: &F) -> F { combine_table_entry( diff --git a/kimchi/src/circuits/lookup/tables/mod.rs b/kimchi/src/circuits/lookup/tables/mod.rs index 09ed562c91..dc5bf3febd 100644 --- a/kimchi/src/circuits/lookup/tables/mod.rs +++ b/kimchi/src/circuits/lookup/tables/mod.rs @@ -23,6 +23,53 @@ pub enum GateLookupTable { RangeCheck, } +/// Enumerates the different 'fixed' lookup tables used by individual gates +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)] +pub struct GateLookupTables { + pub xor: bool, + pub range_check: bool, +} + +impl std::ops::Index for GateLookupTables { + type Output = bool; + + fn index(&self, index: GateLookupTable) -> &Self::Output { + match index { + GateLookupTable::Xor => &self.xor, + GateLookupTable::RangeCheck => &self.range_check, + } + } +} + +impl std::ops::IndexMut for GateLookupTables { + fn index_mut(&mut self, index: GateLookupTable) -> &mut Self::Output { + match index { + GateLookupTable::Xor => &mut self.xor, + GateLookupTable::RangeCheck => &mut self.range_check, + } + } +} + +impl IntoIterator for GateLookupTables { + type Item = GateLookupTable; + type IntoIter = std::vec::IntoIter; + + fn into_iter(self) -> Self::IntoIter { + // Destructor pattern to make sure we add new lookup patterns. + let GateLookupTables { xor, range_check } = self; + + let mut patterns = Vec::with_capacity(2); + + if xor { + patterns.push(GateLookupTable::Xor) + } + if range_check { + patterns.push(GateLookupTable::RangeCheck) + } + patterns.into_iter() + } +} + /// A table of values that can be used for a lookup, along with the ID for the table. #[derive(Debug, Clone)] pub struct LookupTable { diff --git a/kimchi/src/prover.rs b/kimchi/src/prover.rs index 44c6571765..0f92745d7f 100644 --- a/kimchi/src/prover.rs +++ b/kimchi/src/prover.rs @@ -936,7 +936,7 @@ where //~~ * $s_i$ //~~ * $w_i$ //~~ * $z$ - //~~ * lookup (TODO) + //~~ * lookup (TODO, see [this issue](https://github.com/MinaProtocol/mina/issues/13886)) //~~ * generic selector //~~ * poseidon selector //~ diff --git a/optimism/src/main.rs b/optimism/src/main.rs index c8bb5e85af..7a202dc4cc 100644 --- a/optimism/src/main.rs +++ b/optimism/src/main.rs @@ -146,7 +146,7 @@ pub fn main() -> ExitCode { let mut env = witness::Env::::create(cannon::PAGE_SIZE as usize, state, po); while !env.halt { - env.step(configuration.clone(), &meta, &start); + env.step(&configuration, &meta, &start); } // TODO: Logic diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs index a22a5e6509..eec9f40d84 100644 --- a/optimism/src/mips/interpreter.rs +++ b/optimism/src/mips/interpreter.rs @@ -750,190 +750,3 @@ pub mod debugging { } } } - -#[cfg(test)] -mod tests { - - use super::{debugging::*, *}; - use crate::cannon::{HostProgram, PAGE_SIZE}; - use crate::mips::registers::Registers; - use crate::mips::witness::{Env, SyscallEnv, SCRATCH_SIZE}; - use crate::preimage_oracle::PreImageOracle; - use mina_curves::pasta::Fp; - use rand::Rng; - - fn dummy_env() -> Env { - let host_program = Some(HostProgram { - name: String::from("true"), - arguments: vec![], - }); - let mut rng = rand::thread_rng(); - let dummy_preimage_oracle = PreImageOracle::create(&host_program); - Env { - instruction_counter: 0, - // Only 8kb of memory (two PAGE_ADDRESS_SIZE) - memory: vec![ - // Read/write memory - (0, vec![rng.gen(); PAGE_SIZE as usize]), - // Executable memory - (1, vec![0; PAGE_SIZE as usize]), - ], - memory_write_index: vec![ - // Read/write memory - (0, vec![0; PAGE_SIZE as usize]), - // Executable memory - (1, vec![0; PAGE_SIZE as usize]), - ], - registers: Registers::default(), - registers_write_index: Registers::default(), - instruction_pointer: PAGE_SIZE, - next_instruction_pointer: PAGE_SIZE + 4, - scratch_state_idx: 0, - scratch_state: [Fp::from(0); SCRATCH_SIZE], - halt: true, - syscall_env: SyscallEnv::default(), - preimage_oracle: dummy_preimage_oracle, - } - } - - fn write_instruction(env: &mut Env, instruction_parts: InstructionParts) { - let instr = instruction_parts.encode(); - env.memory[1].1[0] = ((instr >> 24) & 0xFF) as u8; - env.memory[1].1[1] = ((instr >> 16) & 0xFF) as u8; - env.memory[1].1[2] = ((instr >> 8) & 0xFF) as u8; - env.memory[1].1[3] = (instr & 0xFF) as u8; - } - - #[test] - fn test_unit_jump_instruction() { - // We only care about instruction parts and instruction pointer - let mut dummy_env = dummy_env(); - // Instruction: 0b00001000000000101010011001100111 - // j 173671 - write_instruction( - &mut dummy_env, - InstructionParts { - op_code: 0b000010, - rs: 0b00000, - rt: 0b00010, - rd: 0b10100, - shamt: 0b11001, - funct: 0b100111, - }, - ); - interpret_jtype(&mut dummy_env, JTypeInstruction::Jump); - assert_eq!(dummy_env.instruction_pointer, 694684); - } - - #[test] - fn test_unit_load32_instruction() { - let mut rng = rand::thread_rng(); - // lw instruction - let mut dummy_env = dummy_env(); - // Instruction: 0b10001111101001000000000000000000 - // lw $a0, 0(29) - // a0 = 4 - // Random address in SP - // Address has only one index - let addr: u32 = rng.gen_range(0u32..100u32); - let aligned_addr: u32 = (addr / 4) * 4; - dummy_env.registers[REGISTER_SP as usize] = aligned_addr; - let mem = &dummy_env.memory[0]; - let mem = &mem.1; - let v0 = mem[aligned_addr as usize]; - let v1 = mem[(aligned_addr + 1) as usize]; - let v2 = mem[(aligned_addr + 2) as usize]; - let v3 = mem[(aligned_addr + 3) as usize]; - let exp_v = ((v0 as u32) << 24) + ((v1 as u32) << 16) + ((v2 as u32) << 8) + (v3 as u32); - // Set random alue into registers - write_instruction( - &mut dummy_env, - InstructionParts { - op_code: 0b000010, - rs: 0b11101, - rt: 0b00100, - rd: 0b00000, - shamt: 0b00000, - funct: 0b000000, - }, - ); - interpret_itype(&mut dummy_env, ITypeInstruction::Load32); - assert_eq!( - dummy_env.registers.general_purpose[REGISTER_A0 as usize], - exp_v - ); - } - - #[test] - fn test_unit_addi_instruction() { - // We only care about instruction parts and instruction pointer - let mut dummy_env = dummy_env(); - // Instruction: 0b10001111101001000000000000000000 - // addi a1,sp,4 - write_instruction( - &mut dummy_env, - InstructionParts { - op_code: 0b000010, - rs: 0b11101, - rt: 0b00101, - rd: 0b00000, - shamt: 0b00000, - funct: 0b000100, - }, - ); - interpret_itype(&mut dummy_env, ITypeInstruction::AddImmediate); - assert_eq!( - dummy_env.registers.general_purpose[REGISTER_A1 as usize], - dummy_env.registers.general_purpose[REGISTER_SP as usize] + 4 - ); - } - - #[test] - fn test_unit_lui_instruction() { - // We only care about instruction parts and instruction pointer - let mut dummy_env = dummy_env(); - // Instruction: 0b00111100000000010000000000001010 - // lui at, 0xa - write_instruction( - &mut dummy_env, - InstructionParts { - op_code: 0b000010, - rs: 0b00000, - rt: 0b00001, - rd: 0b00000, - shamt: 0b00000, - funct: 0b001010, - }, - ); - interpret_itype(&mut dummy_env, ITypeInstruction::LoadUpperImmediate); - assert_eq!( - dummy_env.registers.general_purpose[REGISTER_AT as usize], - 0xa0000 - ); - } - - #[test] - fn test_unit_addiu_instruction() { - // We only care about instruction parts and instruction pointer - let mut dummy_env = dummy_env(); - // Instruction: 0b00100100001000010110110011101000 - // lui at, 0xa - write_instruction( - &mut dummy_env, - InstructionParts { - op_code: 0b001001, - rs: 0b00001, - rt: 0b00001, - rd: 0b01101, - shamt: 0b10011, - funct: 0b101000, - }, - ); - let exp_res = dummy_env.registers[REGISTER_AT as usize] + 27880; - interpret_itype(&mut dummy_env, ITypeInstruction::AddImmediateUnsigned); - assert_eq!( - dummy_env.registers.general_purpose[REGISTER_AT as usize], - exp_res - ); - } -} diff --git a/optimism/src/mips/witness.rs b/optimism/src/mips/witness.rs index b8c0fed886..93833eec32 100644 --- a/optimism/src/mips/witness.rs +++ b/optimism/src/mips/witness.rs @@ -443,7 +443,7 @@ impl Env { (opcode, instruction) } - pub fn step(&mut self, config: VmConfiguration, metadata: &Meta, start: &Start) { + pub fn step(&mut self, config: &VmConfiguration, metadata: &Meta, start: &Start) { self.reset_scratch_state(); let (opcode, instruction) = self.decode_instruction(); let instruction_parts: InstructionParts = InstructionParts::decode(instruction); @@ -456,10 +456,10 @@ impl Env { debug!("Shamt: {:#07b}", instruction_parts.shamt); debug!("Funct: {:#08b}", instruction_parts.funct); - self.pp_info(config.info_at, metadata, start); + self.pp_info(&config.info_at, metadata, start); // Force stops at given iteration - if self.should_trigger_at(config.stop_at) { + if self.should_trigger_at(&config.stop_at) { self.halt = true; return; } @@ -469,13 +469,13 @@ impl Env { self.instruction_counter += 1; } - fn should_trigger_at(&self, at: StepFrequency) -> bool { + fn should_trigger_at(&self, at: &StepFrequency) -> bool { let m: u64 = self.instruction_counter as u64; match at { StepFrequency::Never => false, StepFrequency::Always => true, - StepFrequency::Exactly(n) => n == m, - StepFrequency::Every(n) => m % n == 0, + StepFrequency::Exactly(n) => *n == m, + StepFrequency::Every(n) => m % *n == 0, } } @@ -505,7 +505,7 @@ impl Env { None } - fn pp_info(&mut self, at: StepFrequency, meta: &Meta, start: &Start) { + fn pp_info(&mut self, at: &StepFrequency, meta: &Meta, start: &Start) { if self.should_trigger_at(at) { let elapsed = start.time.elapsed(); let step = self.instruction_counter;