diff --git a/Cargo.lock b/Cargo.lock index c2dc05cf2..547d2b9d3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -6136,7 +6136,7 @@ dependencies = [ [[package]] name = "test-artifacts" -version = "1.2.6" +version = "1.2.7" dependencies = [ "zkm-build", ] @@ -7718,7 +7718,7 @@ dependencies = [ [[package]] name = "zkm-build" -version = "1.2.6" +version = "1.2.7" dependencies = [ "anyhow", "cargo_metadata", @@ -7728,7 +7728,7 @@ dependencies = [ [[package]] name = "zkm-cli" -version = "1.2.6" +version = "1.2.7" dependencies = [ "anyhow", "cargo_metadata", @@ -7741,7 +7741,7 @@ dependencies = [ [[package]] name = "zkm-core-executor" -version = "1.2.6" +version = "1.2.7" dependencies = [ "anyhow", "bincode", @@ -7777,13 +7777,13 @@ dependencies = [ "vec_map", "zkm-curves", "zkm-instruction-test-defs", - "zkm-primitives 1.2.6", + "zkm-primitives 1.2.7", "zkm-stark", ] [[package]] name = "zkm-core-machine" -version = "1.2.6" +version = "1.2.7" dependencies = [ "bincode", "cbindgen", @@ -7834,13 +7834,13 @@ dependencies = [ "zkm-curves", "zkm-derive", "zkm-instruction-test-defs", - "zkm-primitives 1.2.6", + "zkm-primitives 1.2.7", "zkm-stark", ] [[package]] name = "zkm-cuda" -version = "1.2.6" +version = "1.2.7" dependencies = [ "bincode", "ctrlc", @@ -7857,7 +7857,7 @@ dependencies = [ [[package]] name = "zkm-curves" -version = "1.2.6" +version = "1.2.7" dependencies = [ "cfg-if", "curve25519-dalek", @@ -7876,13 +7876,13 @@ dependencies = [ "thiserror 1.0.69", "tracing", "typenum", - "zkm-primitives 1.2.6", + "zkm-primitives 1.2.7", "zkm-stark", ] [[package]] name = "zkm-derive" -version = "1.2.6" +version = "1.2.7" dependencies = [ "proc-macro2", "quote", @@ -7891,7 +7891,7 @@ dependencies = [ [[package]] name = "zkm-instruction-test-defs" -version = "1.2.6" +version = "1.2.7" dependencies = [ "zkm-core-executor", ] @@ -7911,19 +7911,19 @@ dependencies = [ [[package]] name = "zkm-lib" -version = "1.2.6" +version = "1.2.7" dependencies = [ "bincode", "cfg-if", "elliptic-curve", "serde", "sha2", - "zkm-primitives 1.2.6", + "zkm-primitives 1.2.7", ] [[package]] name = "zkm-picus" -version = "1.2.6" +version = "1.2.7" dependencies = [ "clap", "p3-air", @@ -7955,7 +7955,7 @@ dependencies = [ [[package]] name = "zkm-primitives" -version = "1.2.6" +version = "1.2.7" dependencies = [ "bincode", "hex", @@ -7972,7 +7972,7 @@ dependencies = [ [[package]] name = "zkm-prover" -version = "1.2.6" +version = "1.2.7" dependencies = [ "anyhow", "bincode", @@ -8000,7 +8000,7 @@ dependencies = [ "tracing-subscriber 0.3.23", "zkm-core-executor", "zkm-core-machine", - "zkm-primitives 1.2.6", + "zkm-primitives 1.2.7", "zkm-recursion-circuit", "zkm-recursion-compiler", "zkm-recursion-core", @@ -8010,7 +8010,7 @@ dependencies = [ [[package]] name = "zkm-recursion-circuit" -version = "1.2.6" +version = "1.2.7" dependencies = [ "ff 0.13.1", "hashbrown 0.14.5", @@ -8038,7 +8038,7 @@ dependencies = [ "zkm-core-executor", "zkm-core-machine", "zkm-derive", - "zkm-primitives 1.2.6", + "zkm-primitives 1.2.7", "zkm-recursion-compiler", "zkm-recursion-core", "zkm-recursion-gnark-ffi", @@ -8047,7 +8047,7 @@ dependencies = [ [[package]] name = "zkm-recursion-compiler" -version = "1.2.6" +version = "1.2.7" dependencies = [ "backtrace", "itertools 0.13.0", @@ -8063,7 +8063,7 @@ dependencies = [ "tracing", "vec_map", "zkm-core-machine", - "zkm-primitives 1.2.6", + "zkm-primitives 1.2.7", "zkm-recursion-core", "zkm-recursion-derive", "zkm-stark", @@ -8071,7 +8071,7 @@ dependencies = [ [[package]] name = "zkm-recursion-core" -version = "1.2.6" +version = "1.2.7" dependencies = [ "backtrace", "cbindgen", @@ -8107,13 +8107,13 @@ dependencies = [ "zkhash", "zkm-core-machine", "zkm-derive", - "zkm-primitives 1.2.6", + "zkm-primitives 1.2.7", "zkm-stark", ] [[package]] name = "zkm-recursion-derive" -version = "1.2.6" +version = "1.2.7" dependencies = [ "quote", "syn 1.0.109", @@ -8121,7 +8121,7 @@ dependencies = [ [[package]] name = "zkm-recursion-gnark-ffi" -version = "1.2.6" +version = "1.2.7" dependencies = [ "anyhow", "bincode", @@ -8144,7 +8144,7 @@ dependencies = [ [[package]] name = "zkm-sdk" -version = "1.2.6" +version = "1.2.7" dependencies = [ "alloy-primitives", "alloy-signer", @@ -8184,14 +8184,14 @@ dependencies = [ "zkm-core-executor", "zkm-core-machine", "zkm-cuda", - "zkm-primitives 1.2.6", + "zkm-primitives 1.2.7", "zkm-prover", "zkm-stark", ] [[package]] name = "zkm-stark" -version = "1.2.6" +version = "1.2.7" dependencies = [ "arrayref", "hashbrown 0.14.5", @@ -8226,13 +8226,13 @@ dependencies = [ "tracing-forest", "tracing-subscriber 0.3.23", "zkm-derive", - "zkm-primitives 1.2.6", + "zkm-primitives 1.2.7", "zkm-zkvm", ] [[package]] name = "zkm-verifier" -version = "1.2.6" +version = "1.2.7" dependencies = [ "anyhow", "ark-bn254", @@ -8262,7 +8262,7 @@ dependencies = [ "thiserror 2.0.18", "zkm-core-executor", "zkm-core-machine", - "zkm-primitives 1.2.6", + "zkm-primitives 1.2.7", "zkm-prover", "zkm-recursion-core", "zkm-sdk", @@ -8271,7 +8271,7 @@ dependencies = [ [[package]] name = "zkm-zkvm" -version = "1.2.6" +version = "1.2.7" dependencies = [ "bincode", "cfg-if", @@ -8285,8 +8285,8 @@ dependencies = [ "rand 0.8.5", "serde", "sha2", - "zkm-lib 1.2.6", - "zkm-primitives 1.2.6", + "zkm-lib 1.2.7", + "zkm-primitives 1.2.7", ] [[package]] diff --git a/Cargo.toml b/Cargo.toml index 38a4917fd..4cdb9955d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,5 +1,5 @@ [workspace.package] -version = "1.2.6" +version = "1.2.7" edition = "2021" license = "MIT OR Apache-2.0" rust-version = "1.80" diff --git a/crates/core/executor/src/air.rs b/crates/core/executor/src/air.rs index e16821bce..79153ba94 100644 --- a/crates/core/executor/src/air.rs +++ b/crates/core/executor/src/air.rs @@ -115,8 +115,6 @@ pub enum MipsAirId { SysLinux = 47, /// The MovCondChip. MovCond = 49, - // The BooleanCircuitGarble chip. - BooleanCircuitGarble = 50, } impl MipsAirId { @@ -197,7 +195,6 @@ impl MipsAirId { Self::Byte => "Byte", Self::SysLinux => "SysLinux", Self::MovCond => "MovCond", - Self::BooleanCircuitGarble => "BooleanCircuitGarble", } } } diff --git a/crates/core/executor/src/artifacts/mips_costs.json b/crates/core/executor/src/artifacts/mips_costs.json index 98aee564e..237243417 100644 --- a/crates/core/executor/src/artifacts/mips_costs.json +++ b/crates/core/executor/src/artifacts/mips_costs.json @@ -1,52 +1,51 @@ { - "U256XU2048Mul": 5849, - "Bn254Fp2MulAssign": 2885, + "U256XU2048Mul": 7045, + "Bn254Fp2MulAssign": 3141, "CloClz": 41, - "Bls12831Fp2AddSubAssign": 2070, + "Bls12831Fp2AddSubAssign": 2454, "SyscallInstrs": 97, - "DivRem": 170, + "DivRem": 178, "ShiftRight": 131, - "Secp256r1Decompress": 2686, - "Secp256k1Decompress": 2686, - "KeccakSponge": 112104, - "Bn254AddAssign": 4013, + "Secp256r1Decompress": 2814, + "Secp256k1Decompress": 2814, + "KeccakSponge": 122280, + "Bn254AddAssign": 4269, "Bitwise": 42, "ShiftLeft": 68, - "MemoryLocal": 100, + "MemoryLocal": 204, "Program": 31, "Global": 115, - "Secp256k1AddAssign": 4013, - "BooleanCircuitGarble": 456, + "Secp256k1AddAssign": 4269, "AddSub": 47, "Jump": 82, - "Bn254FpOpAssign": 704, - "Poseidon2Permute": 1245, - "Mul": 110, - "ShaExtend": 15936, - "Bls12381AddAssign": 6045, + "Bn254FpOpAssign": 832, + "Poseidon2Permute": 1373, + "Mul": 118, + "ShaExtend": 17856, + "Bls12381AddAssign": 6429, "MemoryGlobalFinalize": 127, "Byte": 54, - "EdDecompress": 3062, + "EdDecompress": 3190, "MemoryGlobalInit": 127, "SyscallPrecompile": 39, - "Secp256r1AddAssign": 4013, - "Bn254DoubleAssign": 4492, - "Uint256MulMod": 880, - "Bls12381DoubleAssign": 6772, - "Bls12831Fp2MulAssign": 4341, - "EdAddAssign": 3637, - "Bls12381Decompress": 4149, + "Secp256r1AddAssign": 4269, + "Bn254DoubleAssign": 4620, + "Uint256MulMod": 1072, + "Bls12381DoubleAssign": 6964, + "Bls12831Fp2MulAssign": 4725, + "EdAddAssign": 3893, + "Bls12381Decompress": 4341, "Lt": 52, - "Secp256r1DoubleAssign": 4492, + "Secp256r1DoubleAssign": 4620, "Branch": 90, "SyscallCore": 39, - "SysLinux": 187, - "Bn254Fp2AddSubAssign": 1382, + "SysLinux": 219, + "Bn254Fp2AddSubAssign": 1638, "MovCond": 48, - "Bls12381FpOpAssign": 1048, - "Cpu": 119, - "ShaCompress": 40480, - "MemoryInstrs": 115, - "MiscInstrs": 152, - "Secp256k1DoubleAssign": 4492 + "Bls12381FpOpAssign": 1240, + "Cpu": 143, + "ShaCompress": 41120, + "MemoryInstrs": 123, + "MiscInstrs": 160, + "Secp256k1DoubleAssign": 4620 } \ No newline at end of file diff --git a/crates/core/executor/src/dependencies.rs b/crates/core/executor/src/dependencies.rs index 7ded3d59e..2007c7934 100644 --- a/crates/core/executor/src/dependencies.rs +++ b/crates/core/executor/src/dependencies.rs @@ -288,6 +288,12 @@ pub fn emit_misc_dependencies(executor: &mut Executor, event: MiscEvent) { } else if matches!(event.opcode, Opcode::EXT) { let lsb = event.c & 0x1f; let msbd = event.c >> 5; + // `execute_ext` rejects encodings with `lsb + msbd >= 32`, so the `31 - lsb - msbd` + // shift amounts below cannot underflow. + debug_assert!( + lsb + msbd < 32, + "EXT with lsb + msbd >= 32 must be rejected during execution" + ); let sll_val = event.b << (31 - lsb - msbd); let sll_event = AluEvent { pc: UNUSED_PC, diff --git a/crates/core/executor/src/events/byte.rs b/crates/core/executor/src/events/byte.rs index aa6d1a3be..6a9b7cc04 100644 --- a/crates/core/executor/src/events/byte.rs +++ b/crates/core/executor/src/events/byte.rs @@ -121,9 +121,13 @@ impl ByteRecord for Vec { fn add_byte_lookup_events_from_maps( &mut self, - _new_events: Vec<&HashMap>, + new_events: Vec<&HashMap>, ) { - todo!() + for new_blu_map in new_events { + for (blu_event, count) in new_blu_map.iter() { + self.extend(std::iter::repeat_n(*blu_event, *count)); + } + } } } @@ -185,3 +189,21 @@ impl ByteOpcode { F::from_canonical_u8(self as u8) } } + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_vec_add_byte_lookup_events_from_maps_expands_counts() { + let event = ByteLookupEvent::new(ByteOpcode::U8Range, 0, 0, 1, 2); + let mut map = HashMap::new(); + map.insert(event, 3); + + let mut events = Vec::new(); + events.add_byte_lookup_events_from_maps(vec![&map]); + + assert_eq!(events.len(), 3); + assert!(events.iter().all(|e| *e == event)); + } +} diff --git a/crates/core/executor/src/events/precompiles/boolean_circuit_garble.rs b/crates/core/executor/src/events/precompiles/boolean_circuit_garble.rs deleted file mode 100644 index f0cd34ae0..000000000 --- a/crates/core/executor/src/events/precompiles/boolean_circuit_garble.rs +++ /dev/null @@ -1,45 +0,0 @@ -use serde::{Deserialize, Serialize}; - -use crate::events::{ - memory::{MemoryReadRecord, MemoryWriteRecord}, - MemoryLocalEvent, -}; - -/// Boolean Circuit Garble Event -/// -/// This event is emitted when a boolean circuit garble operation is performed. -#[derive(Default, Debug, Clone, Serialize, Deserialize)] -pub struct BooleanCircuitGarbleEvent { - /// The shard number. - pub shard: u32, - /// The clock cycle. - pub clk: u32, - /// The address of the input - pub input_addr: u32, - /// The address of the output - pub output_addr: u32, - /// The number of gates - pub num_gates: u32, - /// Delta: - pub delta: [u32; 4], - /// Gates info - pub gates_info: Vec, - /// The output - pub output: u32, - /// The memory record for the number of gates - pub num_gates_read_record: MemoryReadRecord, - /// The memory read record for delta - pub delta_read_records: [MemoryReadRecord; 4], - /// The memory records for the gates info - pub gates_read_records: Vec, - /// The memory records for the output - pub output_write_record: MemoryWriteRecord, - /// The local memory access records. - pub local_mem_access: Vec, -} - -impl BooleanCircuitGarbleEvent { - pub fn num_gates(&self) -> usize { - self.num_gates as usize - } -} diff --git a/crates/core/executor/src/events/precompiles/mod.rs b/crates/core/executor/src/events/precompiles/mod.rs index 54246eaae..d2cd0a94d 100644 --- a/crates/core/executor/src/events/precompiles/mod.rs +++ b/crates/core/executor/src/events/precompiles/mod.rs @@ -1,4 +1,3 @@ -mod boolean_circuit_garble; mod ec; mod edwards; mod fptower; @@ -11,7 +10,6 @@ mod u256x2048_mul; mod uint256; use super::{MemoryLocalEvent, SyscallEvent}; use crate::syscalls::SyscallCode; -pub use boolean_circuit_garble::*; pub use ec::*; pub use edwards::*; pub use fptower::*; @@ -83,7 +81,6 @@ pub enum PrecompileEvent { Poseidon2Permute(Poseidon2PermuteEvent), /// linux precompile event. Linux(LinuxEvent), - BooleanCircuitGarble(BooleanCircuitGarbleEvent), } /// Trait to retrieve all the local memory events from a vec of precompile events. @@ -150,9 +147,6 @@ impl PrecompileLocalMemory for Vec<(SyscallEvent, PrecompileEvent)> { PrecompileEvent::Linux(e) => { iterators.push(e.local_mem_access.iter()); } - PrecompileEvent::BooleanCircuitGarble(e) => { - iterators.push(e.local_mem_access.iter()); - } } } diff --git a/crates/core/executor/src/executor.rs b/crates/core/executor/src/executor.rs index 4a482d1ac..44c2fdc4d 100644 --- a/crates/core/executor/src/executor.rs +++ b/crates/core/executor/src/executor.rs @@ -250,6 +250,10 @@ pub enum ExecutionError { #[error("buffer length {1} must be greater than or equal to {0}")] BufferLengthTooSmall(usize, usize), + /// The execution failed because a hook received an unsupported elliptic curve identifier. + #[error("unsupported ecrecover curve id: {0}")] + UnsupportedEcrecoverCurveId(u8), + /// The execution failed while converting a slice to an array due to size mismatch. #[error("failed to convert slice {0} to array")] IntoArrayError(String), @@ -1545,11 +1549,11 @@ impl<'a> Executor<'a> { if instruction.opcode == Opcode::WSBH { (a, b, c) = self.execute_wsbh(instruction); } else if instruction.opcode == Opcode::EXT { - (a, b, c) = self.execute_ext(instruction); + (a, b, c) = self.execute_ext(instruction)?; } else if instruction.opcode == Opcode::MADDU { (hi_or_prev_a, a, b, c) = self.execute_maddu(instruction); } else if instruction.opcode == Opcode::INS { - (hi_or_prev_a, a, b, c) = self.execute_ins(instruction); + (hi_or_prev_a, a, b, c) = self.execute_ins(instruction)?; } else if instruction.opcode == Opcode::SEXT { (a, b, c) = self.execute_sext(instruction); } else if instruction.opcode == Opcode::TEQ { @@ -1784,20 +1788,32 @@ impl<'a> Executor<'a> { (a, b, 0) } - fn execute_ext(&mut self, instruction: &Instruction) -> (u32, u32, u32) { + fn execute_ext( + &mut self, + instruction: &Instruction, + ) -> Result<(u32, u32, u32), ExecutionError> { let (rd, rt, c) = (instruction.op_a.into(), (instruction.op_b as u8).into(), instruction.op_c); let b = self.rr_cpu(rt, MemoryAccessPosition::B); let msbd = c >> 5; let lsb = c & 0x1f; + // `lsb + msbd < 32` is architecturally required (and enforced by the EXT AIR + // constraint). Otherwise the `31 - lsb - msbd` shift amount used here and in trace + // generation underflows as a `u32`. Reject the undefined encoding instead of panicking. + if msbd + lsb >= 32 { + return Err(ExecutionError::ExceptionOrTrap()); + } let mask_msb = if msbd + lsb + 1 == 32 { 0xFFFFFFFF } else { (1u32 << (msbd + lsb + 1)) - 1 }; let a = (b & mask_msb) >> lsb; self.rw_cpu(rd, a, MemoryAccessPosition::A); - (a, b, c) + Ok((a, b, c)) } - fn execute_ins(&mut self, instruction: &Instruction) -> (Option, u32, u32, u32) { + fn execute_ins( + &mut self, + instruction: &Instruction, + ) -> Result<(Option, u32, u32, u32), ExecutionError> { let (rd, rt, c) = (instruction.op_a.into(), (instruction.op_b as u8).into(), instruction.op_c); let b = self.rr_cpu(rt, MemoryAccessPosition::B); @@ -1805,11 +1821,14 @@ impl<'a> Executor<'a> { let prev_a = a; let msb = c >> 5; let lsb = c & 0x1f; + if msb < lsb { + return Err(ExecutionError::ExceptionOrTrap()); + } let mask = if msb - lsb + 1 == 32 { 0xFFFFFFFF } else { (1u32 << (msb - lsb + 1)) - 1 }; let mask_field = mask << lsb; let a = (a & !mask_field) | ((b << lsb) & mask_field); self.rw_cpu(rd, a, MemoryAccessPosition::A); - (Some(prev_a), a, b, c) + Ok((Some(prev_a), a, b, c)) } fn execute_teq( @@ -2069,7 +2088,7 @@ impl<'a> Executor<'a> { rt } // Opcode::SDC1 => 0, - _ => todo!(), + _ => unreachable!("unexpected store opcode: {:?}", instruction.opcode), }; if aligned_addr + 3 > MAX_MEMORY as u32 { diff --git a/crates/core/executor/src/hook.rs b/crates/core/executor/src/hook.rs index 1af3d7f08..040d26235 100644 --- a/crates/core/executor/src/hook.rs +++ b/crates/core/executor/src/hook.rs @@ -130,7 +130,7 @@ pub fn hook_ecrecover(_: HookEnv, buf: &[u8]) -> Result>, ExecutionE match curve_id { 1 => Ok(ecrecover::handle_secp256k1(r_bytes, alpha_bytes, r_is_y_odd)), 2 => Ok(ecrecover::handle_secp256r1(r_bytes, alpha_bytes, r_is_y_odd)), - _ => unimplemented!("Unsupported curve id: {}", curve_id), + _ => Err(ExecutionError::UnsupportedEcrecoverCurveId(curve_id)), } } diff --git a/crates/core/executor/src/record.rs b/crates/core/executor/src/record.rs index b10c8f17d..636815211 100644 --- a/crates/core/executor/src/record.rs +++ b/crates/core/executor/src/record.rs @@ -142,7 +142,6 @@ impl ExecutionRecord { SyscallCode::KECCAK_SPONGE => opts.keccak, SyscallCode::SHA_EXTEND => opts.sha_extend, SyscallCode::SHA_COMPRESS => opts.sha_compress, - SyscallCode::BOOLEAN_CIRCUIT_GARBLE => opts.boolean_circuit_garble, _ => opts.deferred, }; @@ -170,28 +169,6 @@ impl ExecutionRecord { } current_shard } - SyscallCode::BOOLEAN_CIRCUIT_GARBLE => { - let mut current_shard = Vec::new(); - let mut current_len = 0; - - for (syscall_event, event) in events { - if let PrecompileEvent::BooleanCircuitGarble(event) = &event { - // Here, input_len_u32s must be a multiple of GENERAL_BLOCK_SIZE_U32S. - let input_len = event.num_gates() + 1; - - if current_len + input_len > threshold && !current_shard.is_empty() { - let mut record = ExecutionRecord::new(self.program.clone()); - record.precompile_events.insert(syscall_code, current_shard); - shards_input.push(record); - current_shard = Vec::new(); - current_len = 0; - } - current_len += input_len; - } - current_shard.push((syscall_event, event)); - } - current_shard - } _ => { let chunks = events.chunks_exact(threshold); let remainder = chunks.remainder().to_vec(); diff --git a/crates/core/executor/src/syscalls/code.rs b/crates/core/executor/src/syscalls/code.rs index 9d86b1cd6..90ed9eba7 100644 --- a/crates/core/executor/src/syscalls/code.rs +++ b/crates/core/executor/src/syscalls/code.rs @@ -181,9 +181,6 @@ pub enum SyscallCode { /// Executes the `POSEIDON2_PERMUTE` precompile. POSEIDON2_PERMUTE = 0x00_01_00_30, - /// Executes the `BOOLEAN_CIRCUIT_GARBLE` precompile. - BOOLEAN_CIRCUIT_GARBLE = 0x00_01_00_31, - SYS_LINUX = 4000, // not real syscall, used for represent all linux syscalls UNIMPLEMENTED = 0xFF_FF_FF_FF, @@ -236,7 +233,6 @@ impl SyscallCode { 0x00_01_00_2D => SyscallCode::SECP256R1_DOUBLE, 0x00_01_00_2E => SyscallCode::SECP256R1_DECOMPRESS, 0x01_01_00_2F => SyscallCode::U256XU2048_MUL, - 0x00_01_00_31 => SyscallCode::BOOLEAN_CIRCUIT_GARBLE, 4000 => SyscallCode::SYS_LINUX, 4003 => SyscallCode::SYS_READ, 4004 => SyscallCode::SYS_WRITE, diff --git a/crates/core/executor/src/syscalls/mod.rs b/crates/core/executor/src/syscalls/mod.rs index 6c1960220..c2d520256 100644 --- a/crates/core/executor/src/syscalls/mod.rs +++ b/crates/core/executor/src/syscalls/mod.rs @@ -22,7 +22,6 @@ pub use code::*; pub use context::*; use hint::{HintLenSyscall, HintReadSyscall}; use precompiles::{ - boolean_circuit::garble::BooleanCircuitGarbleSyscall, edwards::{add::EdwardsAddAssignSyscall, decompress::EdwardsDecompressSyscall}, fptower::{Fp2AddSubSyscall, Fp2MulSyscall, FpOpSyscall}, keccak::sponge::KeccakSpongeSyscall, @@ -105,8 +104,6 @@ pub fn default_syscall_map() -> HashMap> { syscall_map.insert(SyscallCode::KECCAK_SPONGE, Arc::new(KeccakSpongeSyscall)); - syscall_map.insert(SyscallCode::BOOLEAN_CIRCUIT_GARBLE, Arc::new(BooleanCircuitGarbleSyscall)); - syscall_map.insert( SyscallCode::SECP256K1_ADD, Arc::new(WeierstrassAddAssignSyscall::::new()), diff --git a/crates/core/executor/src/syscalls/precompiles/boolean_circuit/garble.rs b/crates/core/executor/src/syscalls/precompiles/boolean_circuit/garble.rs deleted file mode 100644 index 604cb4d7e..000000000 --- a/crates/core/executor/src/syscalls/precompiles/boolean_circuit/garble.rs +++ /dev/null @@ -1,96 +0,0 @@ -use crate::events::{BooleanCircuitGarbleEvent, PrecompileEvent}; -use crate::syscalls::{Syscall, SyscallCode, SyscallContext}; -use crate::ExecutionError; - -pub(crate) struct BooleanCircuitGarbleSyscall; - -// number of bytes for each gate input info. -pub const GATE_INFO_BYTES: usize = 17; - -impl Syscall for BooleanCircuitGarbleSyscall { - fn execute( - &self, - ctx: &mut SyscallContext, - syscall_code: SyscallCode, - arg1: u32, - arg2: u32, - ) -> Result, ExecutionError> { - let start_clk = ctx.clk; - let input_ptr = arg1; - let output_ptr = arg2; - - let mut result = true; - - // read number of gates - let (num_gates_read_record, num_gates_u32) = ctx.mr(input_ptr); - - let (delta_read_records, delta_u32s) = ctx.mr_slice(input_ptr + 4, 4); - let delta: [u32; 4] = delta_u32s.try_into().unwrap(); - - let gate_input_size = GATE_INFO_BYTES as u32 * num_gates_u32; - let gates_base_ptr = input_ptr + 20; - let (gate_read_records, gates_info) = - ctx.mr_slice(gates_base_ptr, gate_input_size as usize); - - // for each gate info - for i in 0..num_gates_u32 { - let base = i as usize * GATE_INFO_BYTES; - - let gate_type_u32 = gates_info[base]; - let h0 = &gates_info[base + 1..base + 5]; - let h1 = &gates_info[base + 5..base + 9]; - let label_b = &gates_info[base + 9..base + 13]; - let expected_ciphertext = &gates_info[base + 13..base + 17]; - - let computed_ciphertext = h0 - .iter() - .zip(h1.iter().zip(label_b.iter().zip(delta.iter()))) - .map(|(&h0_i, (&h1_i, (&label_b_i, &delta_i)))| { - if gate_type_u32 == 0 { - // AND gate - h0_i ^ h1_i ^ label_b_i - } else { - // OR gate - h0_i ^ h1_i ^ label_b_i ^ delta_i - } - }) - .collect::>(); - - let checked = computed_ciphertext.as_slice() == expected_ciphertext; - result = result && checked; - } - - // write result to output - let write_record = ctx.mw(output_ptr, result as u32); - let shard = ctx.current_shard(); - let event = BooleanCircuitGarbleEvent { - shard, - clk: start_clk, - input_addr: input_ptr, - output_addr: output_ptr, - num_gates: num_gates_u32, - delta, - gates_info: gates_info.clone(), - output: result as u32, - num_gates_read_record, - delta_read_records: delta_read_records.try_into().unwrap(), - gates_read_records: gate_read_records, - output_write_record: write_record, - local_mem_access: ctx.postprocess(), - }; - let syscall_event = ctx.rt.syscall_event( - start_clk, - None, - ctx.next_pc, - syscall_code.syscall_id(), - arg1, - arg2, - ); - ctx.add_precompile_event( - syscall_code, - syscall_event, - PrecompileEvent::BooleanCircuitGarble(event), - ); - Ok(None) - } -} diff --git a/crates/core/executor/src/syscalls/precompiles/boolean_circuit/mod.rs b/crates/core/executor/src/syscalls/precompiles/boolean_circuit/mod.rs deleted file mode 100644 index a6c2e0737..000000000 --- a/crates/core/executor/src/syscalls/precompiles/boolean_circuit/mod.rs +++ /dev/null @@ -1 +0,0 @@ -pub mod garble; diff --git a/crates/core/executor/src/syscalls/precompiles/mod.rs b/crates/core/executor/src/syscalls/precompiles/mod.rs index 4e7a22413..cc50a28f4 100644 --- a/crates/core/executor/src/syscalls/precompiles/mod.rs +++ b/crates/core/executor/src/syscalls/precompiles/mod.rs @@ -1,4 +1,3 @@ -pub mod boolean_circuit; pub mod edwards; pub mod fptower; pub mod keccak; diff --git a/crates/core/executor/src/syscalls/precompiles/sys_linux/sysbrk.rs b/crates/core/executor/src/syscalls/precompiles/sys_linux/sysbrk.rs index dff27983f..f710a4823 100644 --- a/crates/core/executor/src/syscalls/precompiles/sys_linux/sysbrk.rs +++ b/crates/core/executor/src/syscalls/precompiles/sys_linux/sysbrk.rs @@ -1,11 +1,37 @@ use crate::{ events::{LinuxEvent, PrecompileEvent}, + program::MAX_MEMORY, syscalls::{Syscall, SyscallCode, SyscallContext}, ExecutionError, Register, }; pub(crate) struct SysBrkSyscall; +/// Maximum amount of heap growth allowed from the program's initial BRK value. +/// +/// This is a prover-side safety bound to prevent guest-controlled `brk` values from +/// expanding memory usage without limit. +const MAX_HEAP_SIZE: u32 = 0x4000_0000; + +fn max_brk(initial_brk: u32) -> Result { + let limit = + initial_brk.checked_add(MAX_HEAP_SIZE).ok_or(ExecutionError::InvalidSyscallArgs())?; + Ok(limit.min(MAX_MEMORY as u32)) +} + +fn resolve_brk( + initial_brk: u32, + current_brk: u32, + requested_brk: u32, +) -> Result { + let limit = max_brk(initial_brk)?; + let v0 = requested_brk.max(current_brk); + if v0 > limit { + return Err(ExecutionError::InvalidSyscallArgs()); + } + Ok(v0) +} + impl Syscall for SysBrkSyscall { fn num_extra_cycles(&self) -> u32 { 0 @@ -20,7 +46,8 @@ impl Syscall for SysBrkSyscall { ) -> Result, ExecutionError> { let start_clk = rt.clk; let (record, brk) = rt.rr_traced(Register::BRK); - let v0 = if a0 > brk { a0 } else { brk }; + let initial_brk = rt.rt.program.image.get(&(Register::BRK as u32)).copied().unwrap_or(brk); + let v0 = resolve_brk(initial_brk, brk, a0)?; let a3_record = rt.rw_traced(Register::A3, 0); let shard = rt.current_shard(); let event = PrecompileEvent::Linux(LinuxEvent { @@ -40,3 +67,36 @@ impl Syscall for SysBrkSyscall { Ok(Some(v0)) } } + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn resolve_brk_keeps_current_value_when_request_is_lower() { + assert_eq!(resolve_brk(0x1000, 0x2000, 0x1800).unwrap(), 0x2000); + } + + #[test] + fn resolve_brk_allows_growth_within_limit() { + assert_eq!(resolve_brk(0x1000, 0x2000, 0x3000).unwrap(), 0x3000); + } + + #[test] + fn resolve_brk_rejects_growth_past_limit() { + let initial_brk = 0x1000; + let limit = max_brk(initial_brk).unwrap(); + assert!(matches!( + resolve_brk(initial_brk, 0x2000, limit + 4), + Err(ExecutionError::InvalidSyscallArgs()) + )); + } + + #[test] + fn max_brk_rejects_overflowing_initial_brk() { + assert!(matches!( + max_brk(u32::MAX - MAX_HEAP_SIZE + 1), + Err(ExecutionError::InvalidSyscallArgs()) + )); + } +} diff --git a/crates/core/executor/src/syscalls/precompiles/sys_linux/sysmmap.rs b/crates/core/executor/src/syscalls/precompiles/sys_linux/sysmmap.rs index ef59a554d..737b34105 100644 --- a/crates/core/executor/src/syscalls/precompiles/sys_linux/sysmmap.rs +++ b/crates/core/executor/src/syscalls/precompiles/sys_linux/sysmmap.rs @@ -10,6 +10,17 @@ pub const PAGE_ADDR_SIZE: usize = 12; pub const PAGE_ADDR_MASK: usize = (1 << PAGE_ADDR_SIZE) - 1; pub const PAGE_SIZE: usize = 1 << PAGE_ADDR_SIZE; +fn align_size(size: u32) -> Result { + if size & (PAGE_ADDR_MASK as u32) == 0 { + return Ok(size); + } + + let aligned = size + .checked_add(PAGE_SIZE as u32 - (size & (PAGE_ADDR_MASK as u32))) + .ok_or(ExecutionError::InvalidSyscallArgs())?; + Ok(aligned) +} + impl Syscall for SysMmapSyscall { fn num_extra_cycles(&self) -> u32 { 0 @@ -22,12 +33,8 @@ impl Syscall for SysMmapSyscall { a0: u32, a1: u32, ) -> Result, ExecutionError> { - let mut size = a1; let start_clk = rt.clk; - if size & (PAGE_ADDR_MASK as u32) != 0 { - // adjust size to align with page size - size = size.wrapping_add(PAGE_SIZE as u32 - (size & (PAGE_ADDR_MASK as u32))); - } + let size = align_size(a1)?; let a3_record = rt.rw_traced(Register::A3, 0); @@ -57,3 +64,23 @@ impl Syscall for SysMmapSyscall { Ok(Some(v0)) } } + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_align_size_preserves_aligned_values() { + assert_eq!(align_size(0x2000).unwrap(), 0x2000); + } + + #[test] + fn test_align_size_rounds_up_misaligned_values() { + assert_eq!(align_size(0x1001).unwrap(), 0x2000); + } + + #[test] + fn test_align_size_rejects_overflow() { + assert!(matches!(align_size(0xFFFF_F001), Err(ExecutionError::InvalidSyscallArgs()))); + } +} diff --git a/crates/core/executor/tests/ext_executor_edge_cases.rs b/crates/core/executor/tests/ext_executor_edge_cases.rs new file mode 100644 index 000000000..d02672111 --- /dev/null +++ b/crates/core/executor/tests/ext_executor_edge_cases.rs @@ -0,0 +1,36 @@ +use zkm_core_executor::{ExecutionError, Executor}; +use zkm_stark::ZKMCoreOpts; + +/// `EXT` with `lsb + msbd >= 32` is architecturally undefined. The executor must reject it +/// with a trap instead of underflowing the `31 - lsb - msbd` shift amount (which would panic +/// or produce an incorrect trace). Here `op_c = 0x28F` encodes `msbd = 20, lsb = 15`. +#[test] +fn n75_ext_oversized_field_traps() { + let mut runtime = Executor::new( + zkm_core_executor::Program::new( + vec![ + zkm_core_executor::Instruction::new( + zkm_core_executor::Opcode::ADD, + zkm_core_executor::Register::T0 as u8, + 0, + 0x1234_5678, + false, + true, + ), + zkm_core_executor::Instruction::new( + zkm_core_executor::Opcode::EXT, + zkm_core_executor::Register::T1 as u8, + zkm_core_executor::Register::T0 as u32, + 0x28F, + false, + true, + ), + ], + 0, + 0, + ), + ZKMCoreOpts::default(), + ); + let err = runtime.run_very_fast().unwrap_err(); + assert!(matches!(err, ExecutionError::ExceptionOrTrap())); +} diff --git a/crates/core/machine/include/memory_local.hpp b/crates/core/machine/include/memory_local.hpp index 0ac208c60..7dc9b9f82 100644 --- a/crates/core/machine/include/memory_local.hpp +++ b/crates/core/machine/include/memory_local.hpp @@ -8,15 +8,24 @@ namespace zkm_core_machine_sys::memory_local { template __ZKM_HOSTDEV__ void event_to_row(const MemoryLocalEvent* event, SingleMemoryLocal* cols) { cols->addr = F::from_canonical_u32(event->addr); - + + cols->initial_shard = F::from_canonical_u32(event->initial_mem_access.shard); cols->initial_clk = F::from_canonical_u32(event->initial_mem_access.timestamp); write_word_from_u32_v2(cols->initial_value, event->initial_mem_access.value); - + cols->final_shard = F::from_canonical_u32(event->final_mem_access.shard); cols->final_clk = F::from_canonical_u32(event->final_mem_access.timestamp); write_word_from_u32_v2(cols->final_value, event->final_mem_access.value); + // 16-bit limbs for shards and 16-bit + 8-bit limbs for the 24-bit clk range checks. + cols->initial_shard_16bit_limb = F::from_canonical_u32(event->initial_mem_access.shard & 0xffff); + cols->final_shard_16bit_limb = F::from_canonical_u32(event->final_mem_access.shard & 0xffff); + cols->initial_clk_16bit_limb = F::from_canonical_u32(event->initial_mem_access.timestamp & 0xffff); + cols->initial_clk_8bit_limb = F::from_canonical_u32((event->initial_mem_access.timestamp >> 16) & 0xff); + cols->final_clk_16bit_limb = F::from_canonical_u32(event->final_mem_access.timestamp & 0xffff); + cols->final_clk_8bit_limb = F::from_canonical_u32((event->final_mem_access.timestamp >> 16) & 0xff); + cols->is_real = F::one(); } } // namespace zkm::memory_local diff --git a/crates/core/machine/src/air/memory.rs b/crates/core/machine/src/air/memory.rs index 883d5423a..acf54c614 100644 --- a/crates/core/machine/src/air/memory.rs +++ b/crates/core/machine/src/air/memory.rs @@ -8,7 +8,10 @@ use zkm_stark::{ LookupKind, }; -use crate::memory::{MemoryAccessCols, MemoryCols}; +use crate::{ + air::WordAirBuilder, + memory::{MemoryAccessCols, MemoryCols}, +}; pub trait MemoryAirBuilder: BaseAirBuilder { /// Constrain a memory read or write. @@ -35,6 +38,11 @@ pub trait MemoryAirBuilder: BaseAirBuilder { // Verify that the current memory access time is greater than the previous's. self.eval_memory_access_timestamp(mem_access, do_check.clone(), shard.clone(), clk.clone()); + // Defense-in-depth: memory words entering the subsystem must remain byte-shaped even + // if an upstream chip forgot to range check them. + self.slice_range_check_u8(&memory_access.prev_value().0, do_check.clone()); + self.slice_range_check_u8(&memory_access.value().0, do_check.clone()); + // Add to the memory argument. let addr = addr.into(); let prev_shard = mem_access.prev_shard.clone().into(); diff --git a/crates/core/machine/src/alu/divrem/mod.rs b/crates/core/machine/src/alu/divrem/mod.rs index 22aedb94d..8948c0601 100644 --- a/crates/core/machine/src/alu/divrem/mod.rs +++ b/crates/core/machine/src/alu/divrem/mod.rs @@ -55,11 +55,10 @@ //! elif c > 0: //! assert 0 <= remainder < c //! -//! if is_c_0: -//! # if division by 0, then quotient is UNPREDICTABLE per MIPS spec. -//! We restrict the quotient = 0xffffffff and remainder = b. -//! This needs special care since # b = 0 * quotient + b is satisfied by any quotient. -//! assert quotient = 0xffffffff +//! # Division by zero is undefined per the MIPS spec and is rejected by the executor +//! # (it traps), so an honest trace never contains a div-by-zero event. The AIR enforces +//! # the same to stay in agreement with the executor. +//! assert not is_c_0 # i.e. c != 0 on every real row use core::{ borrow::{Borrow, BorrowMut}, @@ -568,7 +567,12 @@ where .assert_zero(local.b_neg); // b is not negative. } - // When division by 0, quotient is UNPREDICTABLE per MIPS spec. We restrict the quotient = 0xffffffff + // Division by zero is architecturally undefined: the executor traps on it + // (`ExecutionError::ExceptionOrTrap`, see `execute_alu`), so an honest trace never + // contains a divrem event with c == 0. Enforce the same here so the AIR rejects + // div-by-zero rows rather than accepting them with a forced quotient. This keeps the + // executor and AIR in agreement and removes a path for injecting controlled + // quotient/remainder values into the trace. { // Calculate whether c is 0. IsZeroWordOperation::::eval( @@ -578,12 +582,8 @@ where is_real.clone(), ); - // If is_c_0 is true, then quotient must be 0xffffffff = u32::MAX. - for i in 0..WORD_SIZE { - builder - .when(local.is_c_0.result) - .assert_eq(local.quotient[i], AB::F::from_canonical_u8(u8::MAX)); - } + // c must be non-zero on every real divrem row. + builder.when(is_real.clone()).assert_zero(local.is_c_0.result); } // Range check remainder. (i.e., |remainder| < |c| when not is_c_0) diff --git a/crates/core/machine/src/alu/mul/mod.rs b/crates/core/machine/src/alu/mul/mod.rs index af9c42dc6..baaeaad2b 100644 --- a/crates/core/machine/src/alu/mul/mod.rs +++ b/crates/core/machine/src/alu/mul/mod.rs @@ -42,7 +42,7 @@ use p3_matrix::{dense::RowMajorMatrix, Matrix}; use p3_maybe_rayon::prelude::{ParallelBridge, ParallelIterator, ParallelSlice}; use zkm_core_executor::{ events::{ByteLookupEvent, ByteRecord, CompAluEvent, MemoryAccessPosition, MemoryRecordEnum}, - ByteOpcode, ExecutionRecord, Opcode, Program, + ByteOpcode, ExecutionRecord, Opcode, Program, UNUSED_PC, }; use zkm_derive::AlignedBorrow; #[cfg(feature = "picus")] @@ -513,6 +513,12 @@ where // if hi_record_is_real = 0, both clk and shard should be zero. builder.when_not(local.is_real).assert_zero(local.hi_record_is_real); builder.when(local.hi_record_is_real).assert_one(local.is_mult + local.is_multu); + // Hardware MULT/MULTU rows must write HI. Dependency-only multiply + // rows use UNUSED_PC and keep hi_record_is_real = 0. + builder.when(local.is_mult + local.is_multu).assert_zero( + (local.pc - AB::Expr::from_canonical_u32(UNUSED_PC)) + * (AB::Expr::one() - local.hi_record_is_real), + ); builder.when(local.hi_record_is_real).assert_word_eq(local.hi, *local.op_hi_access.value()); builder.when_not(local.hi_record_is_real).assert_zero(local.clk); builder.when_not(local.hi_record_is_real).assert_zero(local.shard); diff --git a/crates/core/machine/src/cpu/air/mod.rs b/crates/core/machine/src/cpu/air/mod.rs index 02fa3557c..9df2883ed 100644 --- a/crates/core/machine/src/cpu/air/mod.rs +++ b/crates/core/machine/src/cpu/air/mod.rs @@ -208,6 +208,16 @@ impl CpuChip { // If the last real row is the last row, verify the public value's next pc. builder.when_last_row().when(local.is_real).assert_eq(public_values.next_pc, local.next_pc); + + // A branch or jump row carries its post-delay-slot target in `next_next_pc`. + // Since shard public values only export `next_pc`, such rows must not be + // the last real row of a shard; otherwise the target is dropped at the + // boundary and the next shard can rederive fall-through. + builder + .when_transition() + .when(local.is_real - next.is_real) + .assert_one(local.is_sequential + local.is_halt); + builder.when_last_row().when(local.is_real).assert_one(local.is_sequential + local.is_halt); } /// Constraints related to the is_real column. diff --git a/crates/core/machine/src/cpu/air/register.rs b/crates/core/machine/src/cpu/air/register.rs index b5dc36f7a..82321ef2a 100644 --- a/crates/core/machine/src/cpu/air/register.rs +++ b/crates/core/machine/src/cpu/air/register.rs @@ -49,6 +49,13 @@ impl CpuChip { .when_not(local.instruction.op_a_0) .assert_word_eq(local.op_a_value, *local.op_a_access.value()); + // If `op_a` is an immutable read from register 0, the logical operand + // sent to instruction chips must also be zero. Writes to register 0 + // are intentionally excluded because their computed result is discarded. + builder + .when(local.instruction.op_a_0 * local.op_a_immutable) + .assert_word_zero(local.op_a_value); + // If we are maddu，msubu，madd, msub, ins，mne, meq, syscall and memory instruction then the hi_or_prev_a should equal to op_a_access.prev_value. builder .when(local.is_rw_a) diff --git a/crates/core/machine/src/memory/consistency/trace.rs b/crates/core/machine/src/memory/consistency/trace.rs index f63ff2988..ba0864fb8 100644 --- a/crates/core/machine/src/memory/consistency/trace.rs +++ b/crates/core/machine/src/memory/consistency/trace.rs @@ -74,6 +74,11 @@ impl MemoryAccessCols { ) { self.value = current_record.value.into(); + // Match the byte range checks emitted by `eval_memory_access` for both the previous and + // current memory words. + output.add_u8_range_checks(&prev_record.value.to_le_bytes()); + output.add_u8_range_checks(¤t_record.value.to_le_bytes()); + self.prev_shard = F::from_canonical_u32(prev_record.shard); self.prev_clk = F::from_canonical_u32(prev_record.timestamp); diff --git a/crates/core/machine/src/memory/local.rs b/crates/core/machine/src/memory/local.rs index be0943f32..5d04c310d 100644 --- a/crates/core/machine/src/memory/local.rs +++ b/crates/core/machine/src/memory/local.rs @@ -3,14 +3,15 @@ use std::{ mem::size_of, }; -use p3_air::{Air, BaseAir}; +use hashbrown::HashMap; +use p3_air::{Air, AirBuilder, BaseAir}; use p3_field::FieldAlgebra; use p3_field::PrimeField32; use p3_matrix::{dense::RowMajorMatrix, Matrix}; use p3_maybe_rayon::prelude::{ IndexedParallelIterator, IntoParallelRefMutIterator, ParallelIterator, }; -use zkm_core_executor::events::{GlobalLookupEvent, MemoryLocalEvent}; +use zkm_core_executor::events::{ByteLookupEvent, ByteRecord, GlobalLookupEvent, MemoryLocalEvent}; use zkm_core_executor::{ExecutionRecord, Program}; use zkm_derive::AlignedBorrow; use zkm_stark::{ @@ -19,6 +20,7 @@ use zkm_stark::{ }; use crate::{ + air::{MemoryAirBuilder, WordAirBuilder}, utils::{next_power_of_two, zeroed_f_vec}, CoreChipError, }; @@ -44,6 +46,22 @@ pub struct SingleMemoryLocal { /// The final clk of the memory access. pub final_clk: T, + /// The 16-bit limb of `initial_shard`, used for its 16-bit range check. + pub initial_shard_16bit_limb: T, + + /// The 16-bit limb of `final_shard`, used for its 16-bit range check. + pub final_shard_16bit_limb: T, + + /// The 16-bit limb of `initial_clk`, used for its 24-bit range check. + pub initial_clk_16bit_limb: T, + /// The 8-bit limb of `initial_clk`, used for its 24-bit range check. + pub initial_clk_8bit_limb: T, + + /// The 16-bit limb of `final_clk`, used for its 24-bit range check. + pub final_clk_16bit_limb: T, + /// The 8-bit limb of `final_clk`, used for its 24-bit range check. + pub final_clk_8bit_limb: T, + /// The initial value of the memory access. pub initial_value: Word, @@ -100,6 +118,8 @@ impl MachineAir for MemoryLocalChip { output: &mut ExecutionRecord, ) -> Result<(), Self::Error> { let mut events = Vec::new(); + // Byte lookups required by the defense-in-depth range checks emitted in `eval`. + let mut blu: HashMap = HashMap::new(); input.get_local_mem_events().for_each(|mem_event| { events.push(GlobalLookupEvent { @@ -128,9 +148,27 @@ impl MachineAir for MemoryLocalChip { is_receive: false, kind: LookupKind::Memory as u8, }); + + // Byte range check the eight value limbs (initial and final). + blu.add_u8_range_checks(&mem_event.initial_mem_access.value.to_le_bytes()); + blu.add_u8_range_checks(&mem_event.final_mem_access.value.to_le_bytes()); + + // 16-bit range checks for shards. + for value in [mem_event.initial_mem_access.shard, mem_event.final_mem_access.shard] { + blu.add_u16_range_check(value as u16); + } + + // 24-bit range checks (16-bit + 8-bit limbs) for the clk fields. + for value in + [mem_event.initial_mem_access.timestamp, mem_event.final_mem_access.timestamp] + { + blu.add_u16_range_check((value & 0xffff) as u16); + blu.add_u8_range_check(0, ((value >> 16) & 0xff) as u8); + } }); output.global_lookup_events.extend(events); + output.add_byte_lookup_events_from_maps(vec![&blu]); Ok(()) } @@ -170,12 +208,36 @@ impl MachineAir for MemoryLocalChip { let cols = &mut cols.memory_local_entries[k]; if idx + k < events.len() { let event: &&MemoryLocalEvent = &events[idx + k]; + let initial_shard = event.initial_mem_access.shard; + let final_shard = event.final_mem_access.shard; + let initial_clk = event.initial_mem_access.timestamp; + let final_clk = event.final_mem_access.timestamp; + cols.addr = F::from_canonical_u32(event.addr); - cols.initial_shard = F::from_canonical_u32(event.initial_mem_access.shard); - cols.final_shard = F::from_canonical_u32(event.final_mem_access.shard); - cols.initial_clk = - F::from_canonical_u32(event.initial_mem_access.timestamp); - cols.final_clk = F::from_canonical_u32(event.final_mem_access.timestamp); + cols.initial_shard = F::from_canonical_u32(initial_shard); + cols.final_shard = F::from_canonical_u32(final_shard); + cols.initial_clk = F::from_canonical_u32(initial_clk); + cols.final_clk = F::from_canonical_u32(final_clk); + + // Populate the limbs backing the defense-in-depth range checks. + for (value, limb_16, limb_8) in [ + ( + initial_clk, + &mut cols.initial_clk_16bit_limb, + &mut cols.initial_clk_8bit_limb, + ), + ( + final_clk, + &mut cols.final_clk_16bit_limb, + &mut cols.final_clk_8bit_limb, + ), + ] { + *limb_16 = F::from_canonical_u32(value & 0xffff); + *limb_8 = F::from_canonical_u32((value >> 16) & 0xff); + } + cols.initial_shard_16bit_limb = F::from_canonical_u32(initial_shard); + cols.final_shard_16bit_limb = F::from_canonical_u32(final_shard); + cols.initial_value = event.initial_mem_access.value.into(); cols.final_value = event.final_mem_access.value.into(); cols.is_real = F::ONE; @@ -213,6 +275,32 @@ where for local in local.memory_local_entries.iter() { builder.assert_bool(local.is_real); + // Defense-in-depth: byte range check all eight value limbs via the byte lookup table. + builder.slice_range_check_u8(&local.initial_value.0, local.is_real); + builder.slice_range_check_u8(&local.final_value.0, local.is_real); + + // Defense-in-depth: range check shards to 16 bits and clocks to 24 bits. + builder + .when(local.is_real) + .assert_eq(local.initial_shard, local.initial_shard_16bit_limb); + builder.when(local.is_real).assert_eq(local.final_shard, local.final_shard_16bit_limb); + builder.slice_range_check_u16( + &[local.initial_shard_16bit_limb, local.final_shard_16bit_limb], + local.is_real, + ); + builder.eval_range_check_24bits( + local.initial_clk, + local.initial_clk_16bit_limb, + local.initial_clk_8bit_limb, + local.is_real, + ); + builder.eval_range_check_24bits( + local.final_clk, + local.final_clk_16bit_limb, + local.final_clk_8bit_limb, + local.is_real, + ); + let mut values = vec![local.initial_shard.into(), local.initial_clk.into(), local.addr.into()]; values.extend(local.initial_value.map(Into::into)); @@ -310,6 +398,49 @@ mod tests { } } + #[test] + fn test_memory_local_defense_in_depth_lookups() { + // Uses the inline `simple_program` (no guest ELF) so it can run without the zkVM + // toolchain. Verifies that the byte-lookup events recorded in `generate_dependencies` + // for the defense-in-depth range checks exactly balance the AIR `send_byte` calls, and + // that the memory lookups still balance. + setup_logger(); + let program = simple_program(); + let program_clone = program.clone(); + let mut runtime = Executor::new(program, ZKMCoreOpts::default()); + runtime.run().unwrap(); + + // Sanity check: the program must exercise the memory-local chip for the byte-lookup + // balance assertion below to be meaningful. + let n_local_events: usize = + runtime.records.iter().map(|r| r.get_local_mem_events().count()).sum(); + assert!(n_local_events > 0, "expected the test program to produce local memory events"); + + let machine: StarkMachine> = + MipsAir::machine(KoalaBearPoseidon2::new()); + let (pkey, _) = machine.setup(&program_clone); + let opts = ZKMCoreOpts::default(); + machine.generate_dependencies(&mut runtime.records, &opts, None).unwrap(); + + let shards = runtime.records; + for shard in shards.clone() { + debug_lookups_with_all_chips::>( + &machine, + &pkey, + &[shard], + vec![LookupKind::Memory], + LookupScope::Local, + ); + } + debug_lookups_with_all_chips::>( + &machine, + &pkey, + &shards, + vec![LookupKind::Byte], + LookupScope::Global, + ); + } + #[test] fn test_memory_lookup_lookups() { setup_logger(); diff --git a/crates/core/machine/src/mips/mod.rs b/crates/core/machine/src/mips/mod.rs index 03a9518cf..226d6b991 100644 --- a/crates/core/machine/src/mips/mod.rs +++ b/crates/core/machine/src/mips/mod.rs @@ -1,4 +1,3 @@ -use crate::syscall::precompiles::boolean_circuit_garble::BooleanCircuitGarbleChip; use crate::{ global::GlobalChip, memory::{MemoryChipType, MemoryLocalChip, NUM_LOCAL_MEMORY_ENTRIES_PER_ROW}, @@ -145,8 +144,6 @@ pub enum MipsAir { Secp256r1Double(WeierstrassDoubleAssignChip>), /// A precompile for the Poseidon2 permutation Poseidon2Permute(Poseidon2PermuteChip), - /// A precompile for the Boolean Circuit Garble - BooleanCircuitGarble(BooleanCircuitGarbleChip), /// A precompile for the Keccak Sponge KeccakSponge(KeccakSpongeChip), /// A precompile for addition on the Elliptic curve bn254. @@ -440,11 +437,6 @@ impl MipsAir { costs.insert(movcond_instrs.name(), movcond_instrs.cost()); chips.push(movcond_instrs); - let boolean_circuit_garble = - Chip::new(MipsAir::::BooleanCircuitGarble(BooleanCircuitGarbleChip::default())); - costs.insert(boolean_circuit_garble.name(), boolean_circuit_garble.cost()); - chips.push(boolean_circuit_garble); - (chips, costs) } @@ -498,7 +490,6 @@ impl MipsAir { .map(|events| { let events_len = match self { Self::KeccakSponge(_) => self.keccak_permutation_in_record(record), - Self::BooleanCircuitGarble(_) => self.boolean_circuit_garble_in_record(record), _ => events.len(), }; let num_rows = events_len * self.rows_per_event(); @@ -615,25 +606,6 @@ impl MipsAir { .unwrap_or(0) } - fn boolean_circuit_garble_in_record(&self, record: &ExecutionRecord) -> usize { - record - .precompile_events - .get_events(SyscallCode::BOOLEAN_CIRCUIT_GARBLE) - .map(|events| { - events - .iter() - .map(|(_, pre_e)| { - if let PrecompileEvent::BooleanCircuitGarble(event) = pre_e { - event.num_gates() + 1 - } else { - unreachable!() - } - }) - .sum::() - }) - .unwrap_or(0) - } - pub(crate) fn syscall_code(&self) -> SyscallCode { match self { Self::Bls12381Add(_) => SyscallCode::BLS12381_ADD, @@ -660,7 +632,6 @@ impl MipsAir { Self::Bls12381Fp2Mul(_) => SyscallCode::BLS12381_FP2_MUL, Self::Bls12381Fp2AddSub(_) => SyscallCode::BLS12381_FP2_ADD, Self::Poseidon2Permute(_) => SyscallCode::POSEIDON2_PERMUTE, - Self::BooleanCircuitGarble(_) => SyscallCode::BOOLEAN_CIRCUIT_GARBLE, Self::KeccakSponge(_) => SyscallCode::KECCAK_SPONGE, Self::SysLinux(_) => SyscallCode::SYS_LINUX, Self::Add(_) => unreachable!("Invalid for core chip"), @@ -784,6 +755,7 @@ pub mod tests { Instruction::new(Opcode::ADD, 29, 0, 1, false, true), Instruction::new(Opcode::ADD, 30, 0, 1, false, true), Instruction::new(Opcode::BEQ, 29, 30, 100, false, true), + Instruction::new(Opcode::ADD, 0, 0, 0, false, true), ]; let program = Program::new(instructions, 0, 0); run_test::>(program).unwrap(); @@ -796,6 +768,7 @@ pub mod tests { Instruction::new(Opcode::ADD, 29, 0, 1, false, true), Instruction::new(Opcode::ADD, 30, 0, 2, false, true), Instruction::new(Opcode::BEQ, 29, 30, 100, false, true), + Instruction::new(Opcode::ADD, 0, 0, 0, false, true), ]; let program = Program::new(instructions, 0, 0); run_test::>(program).unwrap(); @@ -808,6 +781,7 @@ pub mod tests { Instruction::new(Opcode::ADD, 29, 0, 1, false, true), Instruction::new(Opcode::ADD, 30, 0, 2, false, true), Instruction::new(Opcode::BNE, 29, 30, 100, false, true), + Instruction::new(Opcode::ADD, 0, 0, 0, false, true), ]; let program = Program::new(instructions, 0, 0); run_test::>(program).unwrap(); @@ -820,6 +794,7 @@ pub mod tests { Instruction::new(Opcode::ADD, 29, 0, 0, false, true), Instruction::new(Opcode::ADD, 30, 0, 0, false, true), Instruction::new(Opcode::BNE, 29, 30, 100, false, true), + Instruction::new(Opcode::ADD, 0, 0, 0, false, true), ]; let program = Program::new(instructions, 0, 0); run_test::>(program).unwrap(); @@ -835,6 +810,7 @@ pub mod tests { let instructions = vec![ Instruction::new(Opcode::ADD, 29, 0, *operand, false, true), Instruction::new(*branch_op, 29, 0, 100, true, true), + Instruction::new(Opcode::ADD, 0, 0, 0, false, true), ]; let program = Program::new(instructions, 0, 0); run_test::>(program).unwrap(); @@ -1018,6 +994,7 @@ pub mod tests { let instructions = vec![ Instruction::new(Opcode::ADD, 11, 0, 100, false, true), Instruction::new(Opcode::Jumpi, 0, 100, 0, true, true), + Instruction::new(Opcode::ADD, 0, 0, 0, false, true), ]; let program = Program::new(instructions, 0, 0); run_test::>(program).unwrap(); @@ -1033,6 +1010,7 @@ pub mod tests { let instructions = vec![ Instruction::new(Opcode::ADD, 11, 0, 100, false, true), Instruction::new(Opcode::Jump, 0, 11, 0, false, true), + Instruction::new(Opcode::ADD, 0, 0, 0, false, true), ]; let program = Program::new(instructions, 0, 0); run_test::>(program).unwrap(); @@ -1048,6 +1026,7 @@ pub mod tests { let instructions = vec![ Instruction::new(Opcode::ADD, 31, 0, 0, false, true), Instruction::new(Opcode::Jumpi, 31, 100, 0, true, true), + Instruction::new(Opcode::ADD, 0, 0, 0, false, true), ]; let program = Program::new(instructions, 0, 0); run_test::>(program).unwrap(); @@ -1064,6 +1043,7 @@ pub mod tests { Instruction::new(Opcode::ADD, 5, 0, 0, false, true), Instruction::new(Opcode::ADD, 11, 11, 100, false, true), Instruction::new(Opcode::Jump, 5, 11, 0, false, true), + Instruction::new(Opcode::ADD, 0, 0, 0, false, true), ]; let program = Program::new(instructions, 0, 0); run_test::>(program).unwrap(); diff --git a/crates/core/machine/src/operations/global_accumulation.rs b/crates/core/machine/src/operations/global_accumulation.rs index 40b45b4b9..ffff5db52 100644 --- a/crates/core/machine/src/operations/global_accumulation.rs +++ b/crates/core/machine/src/operations/global_accumulation.rs @@ -143,6 +143,13 @@ impl GlobalAccumulationOperation { }), }; + let assert_on_curve = |builder: &mut AB, point: SepticCurve| { + builder.assert_septic_ext_eq( + point.y.square(), + SepticCurve::::curve_formula(point.x), + ); + }; + let ith_cumulative_sum = |idx: usize| SepticCurve:: { x: SepticExtension::::from_base_fn(|i| { local_accumulation.cumulative_sum[idx][0].0[i].into() @@ -166,12 +173,17 @@ impl GlobalAccumulationOperation { builder.when_first_row().assert_septic_ext_eq(initial_digest.x.clone(), zero_digest.x); builder.when_first_row().assert_septic_ext_eq(initial_digest.y.clone(), zero_digest.y); + // Defense-in-depth: every witnessed running digest must stay on-curve even if the + // incomplete Weierstrass addition edge case is triggered. + assert_on_curve(builder, initial_digest.clone()); + // Constrain that when `is_real = 1`, addition is being carried out, and when `is_real = 0`, the sum remains the same. for i in 0..N { let current_sum = if i == 0 { initial_digest.clone() } else { ith_cumulative_sum(i - 1) }; let point_to_add = ith_point_to_add(i); let next_sum = ith_cumulative_sum(i); + assert_on_curve(builder, next_sum.clone()); // If `local_is_real[i] == 1`, current_sum + point_to_add == next_sum must hold. // To do this, constrain that `sum_checker_x` and `sum_checker_y` are both zero when `is_real == 1`. let sum_checker_x = SepticCurve::::sum_checker_x( diff --git a/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/air.rs b/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/air.rs deleted file mode 100644 index 1f9b0128a..000000000 --- a/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/air.rs +++ /dev/null @@ -1,285 +0,0 @@ -use crate::air::MemoryAirBuilder; -use crate::operations::{IsEqualWordOperation, XorOperation}; -use crate::syscall::precompiles::boolean_circuit_garble::columns::{ - BooleanCircuitGarbleCols, NUM_BOOLEAN_CIRCUIT_GARBLE_COLS, -}; -use crate::syscall::precompiles::boolean_circuit_garble::{ - BooleanCircuitGarbleChip, GATE_INFO_BYTES, OR_GATE_ID, -}; -use p3_air::{Air, AirBuilder, BaseAir}; -use p3_field::FieldAlgebra; -use p3_matrix::Matrix; -use std::borrow::Borrow; -use zkm_core_executor::syscalls::SyscallCode; -use zkm_stark::{LookupScope, ZKMAirBuilder}; - -impl BaseAir for BooleanCircuitGarbleChip { - fn width(&self) -> usize { - NUM_BOOLEAN_CIRCUIT_GARBLE_COLS - } -} - -impl Air for BooleanCircuitGarbleChip -where - AB: ZKMAirBuilder, -{ - fn eval(&self, builder: &mut AB) { - let main = builder.main(); - let (local, next) = (main.row_slice(0), main.row_slice(1)); - let local: &BooleanCircuitGarbleCols = (*local).borrow(); - let next: &BooleanCircuitGarbleCols = (*next).borrow(); - - builder.receive_syscall( - local.shard, - local.clk, - AB::F::from_canonical_u32(SyscallCode::BOOLEAN_CIRCUIT_GARBLE.syscall_id()), - local.input_address, // adjust for num_gates u32 - local.output_address, - local.is_first_row, - LookupScope::Local, - ); - - self.eval_flags(builder, local); - self.eval_memory_access(builder, local); - self.eval_logic_check(builder, local, next); - self.eval_transition(builder, local, next); - } -} - -impl BooleanCircuitGarbleChip { - fn eval_flags( - &self, - builder: &mut AB, - local: &BooleanCircuitGarbleCols, - ) { - // In a true single-row trace, this chip only has the prelude row - // (num_gates + delta read), never a gate row. - let single_row_phase = builder.is_first_row() * builder.is_last_row(); - builder.when(single_row_phase).assert_one(local.is_first_row); - - builder.assert_bool(local.is_real); - builder.assert_bool(local.is_first_row); - builder.assert_bool(local.is_first_gate); - builder.assert_bool(local.not_last_gate); - builder.assert_bool(local.is_gate); - builder.assert_bool(local.checks_acc); - builder.assert_eq(local.is_first_gate * local.is_gate, local.is_first_gate); - builder.assert_eq(local.is_last_gate * local.is_gate, local.is_last_gate); - builder.assert_eq(local.not_last_gate * local.is_gate, local.not_last_gate); - builder.assert_zero(local.is_last_gate * local.is_first_gate); - builder.when(local.is_gate).assert_one(local.is_last_gate + local.not_last_gate); - builder.assert_bool(local.gate_type[0]); - builder.assert_bool(local.gate_type[1]); - builder.assert_eq(local.gate_type[0] + local.gate_type[1], local.is_gate); - builder.when(local.is_real).assert_one(local.is_first_row + local.is_gate); - } - - fn eval_memory_access( - &self, - builder: &mut AB, - local: &BooleanCircuitGarbleCols, - ) { - // eval gate number read - builder.eval_memory_access( - local.shard, - local.clk, - local.input_address, // adjust for num_gates u32, - &local.gates_input_mem[0], - local.is_first_row, - ); - - // eval delta read - for i in 0..4 { - builder.eval_memory_access( - local.shard, - local.clk, - local.input_address + AB::F::from_canonical_u32(4 + (i as u32) * 4), - &local.gates_input_mem[i + 1], - local.is_first_row, - ); - } - - // eval gate info read - for i in 0..GATE_INFO_BYTES { - builder.eval_memory_access( - local.shard, - local.clk, - local.input_address + AB::F::from_canonical_u32((i as u32) * 4), - &local.gates_input_mem[i], - local.is_gate, - ); - } - // eval result write - builder.eval_memory_access( - local.shard, - local.clk, - local.output_address, - &local.result_mem, - local.is_last_gate, - ); - - // The syscall writes a boolean result (as u32) at the final gate. - builder - .when(local.is_last_gate) - .assert_eq(local.result_mem.access.value[0], local.checks_acc * local.checks[2]); - builder.when(local.is_last_gate).assert_zero(local.result_mem.access.value[1]); - builder.when(local.is_last_gate).assert_zero(local.result_mem.access.value[2]); - builder.when(local.is_last_gate).assert_zero(local.result_mem.access.value[3]); - builder.when(local.is_last_gate).assert_zero(local.result_mem.prev_value[0]); - builder.when(local.is_last_gate).assert_zero(local.result_mem.prev_value[1]); - builder.when(local.is_last_gate).assert_zero(local.result_mem.prev_value[2]); - builder.when(local.is_last_gate).assert_zero(local.result_mem.prev_value[3]); - } - - fn eval_logic_check( - &self, - builder: &mut AB, - local: &BooleanCircuitGarbleCols, - next: &BooleanCircuitGarbleCols, - ) { - let transition_continuation = local.not_last_gate * local.is_gate; - // eval XOR operations - for i in 0..4 { - let h0_id = 1 + i; - let h1_id = 5 + i; - let label_b_id = 9 + i; - - XorOperation::::eval( - builder, - local.gates_input_mem[h0_id].access.value, - local.gates_input_mem[h1_id].access.value, - local.aux1[i], - local.is_gate, - ); - - XorOperation::::eval( - builder, - local.aux1[i].value, - local.gates_input_mem[label_b_id].access.value, - local.aux2[i], - local.is_gate, - ); - - XorOperation::::eval( - builder, - local.aux2[i].value, - local.delta[i], - local.aux3[i], - local.is_gate, - ); - } - - // eval check - for i in 0..4 { - let expected_id = 13 + i; - IsEqualWordOperation::::eval( - builder, - local.aux2[i].value.map(|x| x.into()), - local.gates_input_mem[expected_id].access.value.map(|x| x.into()), - local.is_equal_words[i], - local.gate_type[0].into(), - ); - - IsEqualWordOperation::::eval( - builder, - local.aux3[i].value.map(|x| x.into()), - local.gates_input_mem[expected_id].access.value.map(|x| x.into()), - local.is_equal_words[i], - local.gate_type[1].into(), - ); - } - builder.when(local.is_gate).assert_eq( - local.checks[0], - local.is_equal_words[0].is_diff_zero.result - * local.is_equal_words[1].is_diff_zero.result, - ); - builder.when(local.is_gate).assert_eq( - local.checks[1], - local.is_equal_words[2].is_diff_zero.result * local.checks[0], - ); - builder.when(local.is_gate).assert_eq( - local.checks[2], - local.is_equal_words[3].is_diff_zero.result * local.checks[1], - ); - builder.when(local.is_first_row).assert_zero(local.checks[0]); - builder.when(local.is_first_row).assert_zero(local.checks[1]); - builder.when(local.is_first_row).assert_zero(local.checks[2]); - builder.when(local.is_first_row).assert_one(local.checks_acc); - builder - .when(transition_continuation) - .assert_eq(next.checks_acc, local.checks_acc * local.checks[2]); - } - - fn eval_transition( - &self, - builder: &mut AB, - local: &BooleanCircuitGarbleCols, - next: &BooleanCircuitGarbleCols, - ) { - let transition_continuation = local.not_last_gate * local.is_gate; - let bytes_shift = AB::F::from_canonical_u32(256); - let num_gates = local.gates_input_mem[0].access.value.0[0] - + local.gates_input_mem[0].access.value.0[1] * bytes_shift - + local.gates_input_mem[0].access.value.0[2] * bytes_shift * bytes_shift - + local.gates_input_mem[0].access.value.0[3] * bytes_shift * bytes_shift * bytes_shift; - builder.when(local.is_first_row).assert_eq(local.gates_num, num_gates.clone()); - - for i in 0..4 { - let delta_i = local.gates_input_mem[i + 1].access.value; - for j in 0..4 { - builder.when(local.is_first_row).assert_eq(local.delta[i][j], delta_i[j]); - } - } - - let gate_type_value = - local.gate_type[0] + local.gate_type[1] * AB::Expr::from_canonical_u32(OR_GATE_ID); - builder.when(local.is_gate).assert_eq(gate_type_value, num_gates); - - builder.when(local.is_first_gate).assert_zero(local.gate_id); - builder.when(local.is_last_gate).assert_eq(local.gates_num - AB::F::ONE, local.gate_id); - builder - .when(transition_continuation.clone()) - .assert_eq(local.gate_id + AB::F::ONE, next.gate_id); - - // Bridge the prelude row (num_gates + delta read) to the first gate row. - builder - .when(local.is_first_row) - .assert_eq(next.input_address, local.input_address + AB::F::from_canonical_u32(20)); - builder.when(local.is_first_row).assert_eq(next.output_address, local.output_address); - builder.when(local.is_first_row).assert_eq(next.shard, local.shard); - builder.when(local.is_first_row).assert_eq(next.clk, local.clk); - builder.when(local.is_first_row).assert_eq(next.gates_num, local.gates_num); - builder.when(local.is_first_row).assert_zero(next.is_first_row); - builder.when(local.is_first_row).assert_eq(next.is_gate, next.is_first_gate); - builder.when(local.is_first_row).assert_eq(next.checks_acc, next.is_gate); - // Continue with next gate row only when explicitly in same-event continuation. - builder.when(transition_continuation.clone()).assert_one(next.is_gate); - builder.when(transition_continuation.clone()).assert_zero(next.is_first_row); - builder.when(transition_continuation.clone()).assert_zero(next.is_first_gate); - builder - .when(transition_continuation.clone()) - .assert_eq(next.output_address, local.output_address); - builder.when(transition_continuation.clone()).assert_eq(next.shard, local.shard); - builder.when(transition_continuation.clone()).assert_eq(next.clk, local.clk); - for i in 0..4 { - for j in 0..4 { - builder.when(local.is_first_row).assert_eq(local.delta[i][j], next.delta[i][j]); - } - } - - builder.when(transition_continuation.clone()).assert_eq( - local.input_address + AB::F::from_canonical_usize(GATE_INFO_BYTES * 4), - next.input_address, - ); - - builder.when(transition_continuation.clone()).assert_eq(local.gates_num, next.gates_num); - - for i in 0..4 { - for j in 0..4 { - builder - .when(transition_continuation.clone()) - .assert_eq(local.delta[i][j], next.delta[i][j]); - } - } - } -} diff --git a/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/columns.rs b/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/columns.rs deleted file mode 100644 index 7c5711426..000000000 --- a/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/columns.rs +++ /dev/null @@ -1,52 +0,0 @@ -use crate::memory::{MemoryReadCols, MemoryWriteCols}; -use crate::operations::{IsEqualWordOperation, XorOperation}; -use zkm_derive::AlignedBorrow; -#[cfg(feature = "picus")] -use zkm_derive::PicusAnnotations; -use zkm_stark::Word; - -#[cfg(feature = "picus")] -use zkm_stark::PicusInfo; -/// BooleanCircuitGarbleCols is the column layout for the Boolean Circuit Garble. -/// The number of rows equal to the number of gates -#[derive(AlignedBorrow)] -#[cfg_attr(feature = "picus", derive(PicusAnnotations))] -#[repr(C)] -pub struct BooleanCircuitGarbleCols { - #[cfg_attr(feature = "picus", picus(transition_input))] - pub shard: T, - #[cfg_attr(feature = "picus", picus(transition_input))] - pub clk: T, - pub is_real: T, - #[cfg_attr(feature = "picus", picus(transition_input))] - pub input_address: T, - #[cfg_attr(feature = "picus", picus(transition_input))] - pub output_address: T, - pub is_first_row: T, // The first row contains gates_num and delt - #[cfg_attr(feature = "picus", picus(transition_input))] - pub is_gate: T, - #[cfg_attr(feature = "picus", picus(transition_input))] - pub is_first_gate: T, - #[cfg_attr(feature = "picus", picus(transition_input))] - pub is_last_gate: T, - #[cfg_attr(feature = "picus", picus(transition_input))] - pub not_last_gate: T, // from first gate -> (last - 1)-th gate - pub gate_type: [T; 2], - #[cfg_attr(feature = "picus", picus(transition_input))] - pub gate_id: T, - #[cfg_attr(feature = "picus", picus(transition_input))] - pub gates_num: T, - #[cfg_attr(feature = "picus", picus(transition_input))] - pub delta: [Word; 4], // [u8; 16] - pub gates_input_mem: [MemoryReadCols; 17], // gate_type, h0, h1, label_b, expected_ciphertext - pub result_mem: MemoryWriteCols, - pub aux1: [XorOperation; 4], // h1 ^ h0 - pub aux2: [XorOperation; 4], // h1 ^ h0 ^ label_b - pub aux3: [XorOperation; 4], // h1 ^ h0 ^ label_b ^ delta - pub is_equal_words: [IsEqualWordOperation; 4], // computed ciphertext == expected_ciphertext - pub checks: [T; 3], // row-local chaining result - #[cfg_attr(feature = "picus", picus(input, transition_input))] - pub checks_acc: T, // cross-row accumulated check state -} - -pub const NUM_BOOLEAN_CIRCUIT_GARBLE_COLS: usize = size_of::>(); diff --git a/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/mod.rs b/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/mod.rs deleted file mode 100644 index 4d265bc2e..000000000 --- a/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/mod.rs +++ /dev/null @@ -1,11 +0,0 @@ -mod air; -mod columns; -mod trace; - -// number of bytes for each gate input info. -pub const GATE_INFO_BYTES: usize = 17; -// OR gate id -pub const OR_GATE_ID: u32 = 7; -/// A chip that computes non-free-gate ciphertexts and verifies them against the received ones. -#[derive(Default)] -pub struct BooleanCircuitGarbleChip; diff --git a/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/trace.rs b/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/trace.rs deleted file mode 100644 index 7e558f626..000000000 --- a/crates/core/machine/src/syscall/precompiles/boolean_circuit_garble/trace.rs +++ /dev/null @@ -1,232 +0,0 @@ -use crate::syscall::precompiles::boolean_circuit_garble::columns::{ - BooleanCircuitGarbleCols, NUM_BOOLEAN_CIRCUIT_GARBLE_COLS, -}; -use crate::syscall::precompiles::boolean_circuit_garble::{ - BooleanCircuitGarbleChip, GATE_INFO_BYTES, OR_GATE_ID, -}; -use crate::CoreChipError; -use hashbrown::HashMap; -use itertools::Itertools; -use p3_field::PrimeField32; -use p3_matrix::dense::RowMajorMatrix; -use p3_maybe_rayon::prelude::ParallelIterator; -use rayon::iter::IntoParallelRefIterator; -use rayon::prelude::ParallelSlice; -use std::borrow::BorrowMut; -use zkm_core_executor::events::{ - BooleanCircuitGarbleEvent, ByteLookupEvent, ByteRecord, PrecompileEvent, -}; -use zkm_core_executor::syscalls::SyscallCode; -use zkm_core_executor::{ExecutionRecord, Program}; -#[cfg(feature = "picus")] -use zkm_stark::air::PicusInfo; -use zkm_stark::MachineAir; - -impl MachineAir for BooleanCircuitGarbleChip { - type Record = ExecutionRecord; - type Program = Program; - type Error = CoreChipError; - - fn name(&self) -> String { - "BooleanCircuitGarble".to_string() - } - - #[cfg(feature = "picus")] - fn picus_info(&self) -> PicusInfo { - BooleanCircuitGarbleCols::::picus_info() - } - - fn generate_dependencies( - &self, - input: &Self::Record, - output: &mut Self::Record, - ) -> Result<(), Self::Error> { - let events = input.get_precompile_events(SyscallCode::BOOLEAN_CIRCUIT_GARBLE); - let chunk_size = std::cmp::max(events.len() / num_cpus::get(), 1); - - let blu_batches = events - .par_chunks(chunk_size) - .map(|events| { - let mut blu: HashMap = HashMap::new(); - events.iter().for_each(|(_, event)| { - let event = if let PrecompileEvent::BooleanCircuitGarble(event) = event { - event - } else { - unreachable!(); - }; - - let _ = self.event_to_rows::(event, &mut blu); - }); - blu - }) - .collect::>(); - - output.add_byte_lookup_events_from_maps(blu_batches.iter().collect_vec()); - Ok(()) - } - - fn generate_trace( - &self, - input: &Self::Record, - _output: &mut Self::Record, - ) -> Result, Self::Error> { - let events = input.get_precompile_events(SyscallCode::BOOLEAN_CIRCUIT_GARBLE); - let mut rows: Vec<[F; NUM_BOOLEAN_CIRCUIT_GARBLE_COLS]> = events - .par_iter() - .flat_map(|(_, event)| { - let event = if let PrecompileEvent::BooleanCircuitGarble(event) = event { - event - } else { - unreachable!(); - }; - - self.event_to_rows(event, &mut Vec::new()) - }) - .collect(); - - let padded = if rows.is_empty() { 0 } else { rows.len().next_power_of_two() }; - rows.resize_with(padded, || [F::ZERO; NUM_BOOLEAN_CIRCUIT_GARBLE_COLS]); - Ok(RowMajorMatrix::new( - rows.into_iter().flatten().collect::>(), - NUM_BOOLEAN_CIRCUIT_GARBLE_COLS, - )) - } - - fn included(&self, shard: &Self::Record) -> bool { - if let Some(shape) = shard.shape.as_ref() { - shape.included::(self) - } else { - !shard.get_precompile_events(SyscallCode::BOOLEAN_CIRCUIT_GARBLE).is_empty() - } - } -} - -impl BooleanCircuitGarbleChip { - pub fn event_to_rows( - &self, - event: &BooleanCircuitGarbleEvent, - blu: &mut impl ByteRecord, - ) -> Vec<[F; NUM_BOOLEAN_CIRCUIT_GARBLE_COLS]> { - let gates_num = event.num_gates(); - let mut rows = Vec::new(); - - let mut input_address = event.input_addr; - let mut pre_check = true; - - // first row to read gates_num and delta - // gates_num: gate_input_mem[0] - // delta: gate_input_mem[1..5] - { - let mut row = [F::ZERO; NUM_BOOLEAN_CIRCUIT_GARBLE_COLS]; - let cols: &mut BooleanCircuitGarbleCols = row.as_mut_slice().borrow_mut(); - cols.shard = F::from_canonical_u32(event.shard); - cols.clk = F::from_canonical_u32(event.clk); - cols.is_real = F::ONE; - cols.is_gate = F::ZERO; - cols.is_first_row = F::ONE; - cols.input_address = F::from_canonical_u32(input_address); - cols.output_address = F::from_canonical_u32(event.output_addr); - cols.gates_num = F::from_canonical_u32(gates_num as u32); - cols.checks_acc = F::ONE; - for i in 0..4 { - let delta_i_bytes = event.delta[i].to_le_bytes(); - cols.delta[i] - .0 - .iter_mut() - .enumerate() - .for_each(|(id, x)| *x = F::from_canonical_u8(delta_i_bytes[id])); - } - // read number of gates - cols.gates_input_mem[0].populate(event.num_gates_read_record, blu); - // read delta - for i in 0..4 { - cols.gates_input_mem[1 + i].populate(event.delta_read_records[i], blu); - } - rows.push(row); - } - - input_address += 20; - for gate_id in 0..gates_num { - let mut row = [F::ZERO; NUM_BOOLEAN_CIRCUIT_GARBLE_COLS]; - let cols: &mut BooleanCircuitGarbleCols = row.as_mut_slice().borrow_mut(); - cols.shard = F::from_canonical_u32(event.shard); - cols.clk = F::from_canonical_u32(event.clk); - cols.is_real = F::ONE; - cols.is_gate = F::ONE; - cols.input_address = F::from_canonical_u32(input_address); - cols.output_address = F::from_canonical_u32(event.output_addr); - cols.is_first_gate = F::from_bool(gate_id == 0); - cols.is_last_gate = F::from_bool(gate_id == gates_num - 1); - cols.not_last_gate = F::from_bool(gate_id != gates_num - 1); - cols.gate_id = F::from_canonical_u32(gate_id as u32); - cols.gates_num = F::from_canonical_u32(gates_num as u32); - - for i in 0..4 { - let delta_i_bytes = event.delta[i].to_le_bytes(); - cols.delta[i] - .0 - .iter_mut() - .enumerate() - .for_each(|(id, x)| *x = F::from_canonical_u8(delta_i_bytes[id])); - } - - // read gate info - for i in 0..GATE_INFO_BYTES { - cols.gates_input_mem[i] - .populate(event.gates_read_records[gate_id * GATE_INFO_BYTES + i], blu); - } - - let gate_type = event.gates_info[gate_id * GATE_INFO_BYTES]; - assert!(gate_type == 0 || gate_type == OR_GATE_ID); - cols.gate_type[(gate_type == OR_GATE_ID) as usize] = F::ONE; - - // XOR computation - let mut check_u32s = [0u32; 4]; - for i in 0..4 { - let h0_id = gate_id * GATE_INFO_BYTES + 1 + i; - let h1_id = gate_id * GATE_INFO_BYTES + 5 + i; - let label_b_id = gate_id * GATE_INFO_BYTES + 9 + i; - let expected_id = gate_id * GATE_INFO_BYTES + 13 + i; - - let inter1 = - cols.aux1[i].populate(blu, event.gates_info[h0_id], event.gates_info[h1_id]); - let inter2 = cols.aux2[i].populate(blu, inter1, event.gates_info[label_b_id]); - let inter3 = cols.aux3[i].populate(blu, inter2, event.delta[i]); - if i == 0 { - if gate_type == 0 { - // AND gate - check_u32s[i] = - cols.is_equal_words[i].populate(inter2, event.gates_info[expected_id]); - } else { - // OR gate - check_u32s[i] = - cols.is_equal_words[i].populate(inter3, event.gates_info[expected_id]); - } - } else if gate_type == 0 { - // AND gate - check_u32s[i] = check_u32s[i - 1] - * cols.is_equal_words[i].populate(inter2, event.gates_info[expected_id]); - } else { - // OR gate - check_u32s[i] = check_u32s[i - 1] - * cols.is_equal_words[i].populate(inter3, event.gates_info[expected_id]); - } - } - // populate check results - cols.checks[0] = F::from_canonical_u32(check_u32s[1]); - cols.checks[1] = F::from_canonical_u32(check_u32s[2]); - cols.checks[2] = F::from_canonical_u32(check_u32s[3]); - cols.checks_acc = F::from_bool(pre_check); - pre_check = pre_check && (check_u32s[3] == 1); - - // if this is the last gate, write result - if gate_id == gates_num - 1 { - cols.result_mem.populate(event.output_write_record, blu); - } - - rows.push(row); - input_address += 68; - } - rows - } -} diff --git a/crates/core/machine/src/syscall/precompiles/keccak_sponge/air.rs b/crates/core/machine/src/syscall/precompiles/keccak_sponge/air.rs index b10cd32a5..f4292cd41 100644 --- a/crates/core/machine/src/syscall/precompiles/keccak_sponge/air.rs +++ b/crates/core/machine/src/syscall/precompiles/keccak_sponge/air.rs @@ -58,6 +58,26 @@ where LookupScope::Local, ); + // The first block flag is fixed on the first row and then held steady + // within the block. Once a non-final block ends, the next block must + // reset this flag to zero. + builder.when(local.receive_syscall).assert_one(first_block); + builder + .when_transition() + .when(not_final_step.clone()) + .assert_eq(next.is_first_input_block, first_block); + builder.when(local.is_absorbed).assert_zero(next.is_first_input_block); + + // The final block flag stays low on all non-final blocks and is fixed + // to one on the final block's write-output row. Within a block it stays + // constant across Keccak rounds. + builder.when(local.write_output).assert_one(final_block); + builder.when(local.is_absorbed).assert_zero(final_block); + builder + .when_transition() + .when(not_final_step.clone()) + .assert_eq(next.is_final_input_block, final_block); + // Constrain that the inputs stay the same throughout the rows of each cycle let mut transition_builder = builder.when_transition(); let mut transition_not_final_builder = transition_builder.when(not_final_sponge.clone()); @@ -142,6 +162,12 @@ where .assert_eq(local.input_address, next.input_address); // If this is the first block, absorbed bytes should be 0 builder.when(first_block).assert_eq(local.already_absorbed_u32s, AB::Expr::zero()); + // If this is the first block, the sponge state must start from the + // fixed all-zero Keccak IV. + let mut first_block_builder = builder.when(first_block); + for i in 0..KECCAK_STATE_U32S { + first_block_builder.assert_word_zero(local.original_state[i]); + } // If this is the final block, absorbed bytes should be equal to the input length - KECCAK_GENERAL_RATE_U32S builder.when(final_block).assert_eq( local.already_absorbed_u32s, @@ -269,6 +295,9 @@ impl KeccakSpongeChip { // enforce booleanity and mutual exclusion of first/final step flags. // This prevents degenerate witnesses where a single row is both // first-round and final-round when summary internals are hidden. + builder.assert_bool(first_block); + builder.assert_bool(final_block); + builder.assert_bool(local.read_block); builder.when(local.is_real).assert_bool(first_step); builder.when(local.is_real).assert_bool(final_step); builder.when(local.is_real).assert_zero(first_step * final_step); diff --git a/crates/core/machine/src/syscall/precompiles/keccak_sponge/trace.rs b/crates/core/machine/src/syscall/precompiles/keccak_sponge/trace.rs index 68fb182da..608082e49 100644 --- a/crates/core/machine/src/syscall/precompiles/keccak_sponge/trace.rs +++ b/crates/core/machine/src/syscall/precompiles/keccak_sponge/trace.rs @@ -228,3 +228,82 @@ impl KeccakSpongeChip { } } } + +#[cfg(test)] +mod tests { + use super::*; + use crate::syscall::precompiles::keccak_sponge::columns::KeccakSpongeCols; + use p3_field::FieldAlgebra; + use p3_koala_bear::KoalaBear; + use std::borrow::Borrow; + use zkm_core_executor::events::{ + ByteLookupEvent, KeccakSpongeEvent, MemoryReadRecord, MemoryWriteRecord, + }; + + fn make_event(blocks: usize) -> KeccakSpongeEvent { + let shard = 1; + let clk = 7; + let input_addr = 0x1000; + let output_addr = 0x2000; + let input_len_u32s = (blocks * KECCAK_GENERAL_RATE_U32S) as u32; + let input = vec![0u32; input_len_u32s as usize]; + let output = [0u32; KECCAK_GENERAL_OUTPUT_U32S]; + let input_length_record = MemoryReadRecord::new(input_len_u32s, shard, 1, 0, 0); + + let mut timestamp = 2u32; + let input_read_records = input + .iter() + .map(|&value| { + let record = MemoryReadRecord::new(value, shard, timestamp, 0, 0); + timestamp += 1; + record + }) + .collect::>(); + + let output_write_records = output + .iter() + .map(|&value| { + let record = MemoryWriteRecord::new(value, shard, timestamp, 0, 0, 0); + timestamp += 1; + record + }) + .collect::>(); + + KeccakSpongeEvent { + shard, + clk, + input, + output, + input_len_u32s, + input_read_records, + input_length_record, + output_write_records, + xored_state_list: vec![[0u64; 25]; blocks], + input_addr, + output_addr, + local_mem_access: vec![], + } + } + + #[test] + fn test_keccak_sponge_block_flags_follow_trace_positions() { + let chip = KeccakSpongeChip::new(); + let event = make_event(2); + let mut rows = Some(Vec::new()); + let mut blu = Vec::::new(); + chip.event_to_rows::(&event, &mut rows, &mut blu); + + let rows = rows.unwrap(); + assert_eq!(rows.len(), 2 * NUM_ROUNDS); + + for (index, row) in rows.iter().enumerate() { + let cols: &KeccakSpongeCols = row.as_slice().borrow(); + let block_index = index / NUM_ROUNDS; + let round_index = index % NUM_ROUNDS; + + assert_eq!(cols.is_first_input_block, KoalaBear::from_bool(block_index == 0)); + assert_eq!(cols.is_final_input_block, KoalaBear::from_bool(block_index == 1)); + assert_eq!(cols.read_block, KoalaBear::from_bool(round_index == 0)); + } + } +} diff --git a/crates/core/machine/src/syscall/precompiles/mod.rs b/crates/core/machine/src/syscall/precompiles/mod.rs index bc36f8a5b..6a5c37835 100644 --- a/crates/core/machine/src/syscall/precompiles/mod.rs +++ b/crates/core/machine/src/syscall/precompiles/mod.rs @@ -1,4 +1,3 @@ -pub mod boolean_circuit_garble; pub mod edwards; pub mod fptower; pub mod keccak_sponge; diff --git a/crates/core/machine/src/syscall/precompiles/u256x2048_mul/air.rs b/crates/core/machine/src/syscall/precompiles/u256x2048_mul/air.rs index 57033999d..731fd7bd7 100644 --- a/crates/core/machine/src/syscall/precompiles/u256x2048_mul/air.rs +++ b/crates/core/machine/src/syscall/precompiles/u256x2048_mul/air.rs @@ -1,7 +1,7 @@ use crate::{ air::MemoryAirBuilder, memory::{value_as_limbs, MemoryCols, MemoryReadCols, MemoryWriteCols}, - operations::field::field_op::FieldOpCols, + operations::{field::field_op::FieldOpCols, KoalaBearWordRangeChecker}, utils::{limbs_from_access, pad_rows_fixed, words_to_bytes_le}, CoreChipError, }; @@ -74,6 +74,9 @@ pub struct U256x2048MulCols { pub lo_ptr_memory: MemoryReadCols, pub hi_ptr_memory: MemoryReadCols, + pub lo_ptr_range_checker: KoalaBearWordRangeChecker, + pub hi_ptr_range_checker: KoalaBearWordRangeChecker, + // Memory columns. pub a_memory: [MemoryReadCols; WORDS_FIELD_ELEMENT], pub b_memory: [MemoryReadCols; WORDS_FIELD_ELEMENT * 8], @@ -144,6 +147,8 @@ impl MachineAir for U256x2048MulChip { .populate(event.lo_ptr_memory, &mut new_byte_lookup_events); cols.hi_ptr_memory .populate(event.hi_ptr_memory, &mut new_byte_lookup_events); + cols.lo_ptr_range_checker.populate(event.lo_ptr_memory.value); + cols.hi_ptr_range_checker.populate(event.hi_ptr_memory.value); // Populate memory columns. for i in 0..WORDS_FIELD_ELEMENT { @@ -400,6 +405,21 @@ where ); } + // Range-check the raw pointer words before reducing them to field + // addresses, so the reduction is injective for these memory values. + KoalaBearWordRangeChecker::::range_check( + builder, + *local.lo_ptr_memory.value(), + local.lo_ptr_range_checker, + local.is_real.into(), + ); + KoalaBearWordRangeChecker::::range_check( + builder, + *local.hi_ptr_memory.value(), + local.hi_ptr_range_checker, + local.is_real.into(), + ); + // Constrain that the lo_ptr is the value of lo_ptr_memory. builder .when(local.is_real) diff --git a/crates/core/machine/src/utils/mod.rs b/crates/core/machine/src/utils/mod.rs index c20c9a819..f4a44c938 100644 --- a/crates/core/machine/src/utils/mod.rs +++ b/crates/core/machine/src/utils/mod.rs @@ -179,8 +179,22 @@ pub fn zkm_debug_mode() -> bool { /// /// This function is safe to use only for fields that can be transmuted from 0u32. pub fn zeroed_f_vec(len: usize) -> Vec { - debug_assert!(std::mem::size_of::() == 4); + assert!(std::mem::size_of::() == 4, "zeroed_f_vec only supports 4-byte field elements"); let vec = vec![0u32; len]; unsafe { std::mem::transmute::, Vec>(vec) } } + +#[cfg(test)] +mod tests { + use super::*; + use p3_field::FieldAlgebra; + use p3_koala_bear::KoalaBear; + + #[test] + fn zeroed_f_vec_returns_zero_values_for_koalabear() { + let values = zeroed_f_vec::(4); + assert_eq!(values.len(), 4); + assert!(values.iter().all(|value| *value == KoalaBear::ZERO)); + } +} diff --git a/crates/go-runtime/zkvm_runtime/deserialize.go b/crates/go-runtime/zkvm_runtime/deserialize.go index c98b3fe54..61a6d03dd 100644 --- a/crates/go-runtime/zkvm_runtime/deserialize.go +++ b/crates/go-runtime/zkvm_runtime/deserialize.go @@ -34,70 +34,113 @@ func DeserializeData(data []byte, e any) { } } +func readBytes(data []byte, index, size int) ([]byte, error) { + if index < 0 || size < 0 || index > len(data) || size > len(data)-index { + return nil, fmt.Errorf("deserialize failed: need %d bytes at offset %d, have %d", size, index, len(data)-index) + } + return data[index : index+size], nil +} + +func maxInt() int { + return int(^uint(0) >> 1) +} + func deserializeData(data []byte, v reflect.Value, index int) (int, error) { switch v.Kind() { case reflect.Bool: - v.SetBool(data[index] == 1) + b, err := readBytes(data, index, 1) + if err != nil { + return index, err + } + v.SetBool(b[0] == 1) return index + 1, nil case reflect.Int8: - v.SetInt(int64(int8(data[index]))) + b, err := readBytes(data, index, 1) + if err != nil { + return index, err + } + v.SetInt(int64(int8(b[0]))) return index + 1, nil case reflect.Uint8: - v.SetUint(uint64(data[index])) + b, err := readBytes(data, index, 1) + if err != nil { + return index, err + } + v.SetUint(uint64(b[0])) return index + 1, nil case reflect.Int16: - b := []byte{data[index], data[index+1]} + b, err := readBytes(data, index, 2) + if err != nil { + return index, err + } a := binary.LittleEndian.Uint16(b) v.SetInt(int64(int16(a))) return index + 2, nil case reflect.Uint16: - b := []byte{data[index], data[index+1]} + b, err := readBytes(data, index, 2) + if err != nil { + return index, err + } a := binary.LittleEndian.Uint16(b) v.SetUint(uint64(a)) return index + 2, nil case reflect.Int32: - b := []byte{data[index], data[index+1], data[index+2], data[index+3]} + b, err := readBytes(data, index, 4) + if err != nil { + return index, err + } a := binary.LittleEndian.Uint32(b) v.SetInt(int64(int32(a))) return index + 4, nil case reflect.Uint32: - b := []byte{data[index], data[index+1], data[index+2], data[index+3]} + b, err := readBytes(data, index, 4) + if err != nil { + return index, err + } a := binary.LittleEndian.Uint32(b) v.SetUint(uint64(a)) return index + 4, nil case reflect.Int64: - b := []byte{data[index], data[index+1], data[index+2], data[index+3], - data[index+4], data[index+5], data[index+6], data[index+7]} + b, err := readBytes(data, index, 8) + if err != nil { + return index, err + } a := binary.LittleEndian.Uint64(b) v.SetInt(int64(a)) return index + 8, nil case reflect.Uint64: - b := []byte{data[index], data[index+1], data[index+2], data[index+3], - data[index+4], data[index+5], data[index+6], data[index+7]} + b, err := readBytes(data, index, 8) + if err != nil { + return index, err + } a := binary.LittleEndian.Uint64(b) v.SetUint(a) return index + 8, nil case reflect.Slice: const maxSliceLen = 1_000_000 - b := []byte{data[index], data[index+1], data[index+2], data[index+3], - data[index+4], data[index+5], data[index+6], data[index+7]} + b, err := readBytes(data, index, 8) + if err != nil { + return index, err + } length := binary.LittleEndian.Uint64(b) index += 8 elemKind := v.Type().Elem().Kind() + if length > uint64(maxInt()) { + return index, fmt.Errorf("deserialize failed: slice length %d exceeds int range", length) + } + l := int(length) if elemKind == reflect.Uint8 { - if length > uint64(len(data)-index) { - return index, fmt.Errorf("deserialize failed: []byte length %d exceeds remaining %d", length, len(data)-index) + if l > len(data)-index { + return index, fmt.Errorf("deserialize failed: []byte length %d exceeds remaining %d", l, len(data)-index) } - bytes := data[index : index+int(length)] - v.SetBytes(bytes) - return index + int(length), nil + v.SetBytes(data[index : index+l]) + return index + l, nil } - if length > maxSliceLen { - return index, fmt.Errorf("deserialize failed: slice length %d exceeds max %d", length, maxSliceLen) + if l > maxSliceLen { + return index, fmt.Errorf("deserialize failed: slice length %d exceeds max %d", l, maxSliceLen) } - l := int(length) slice := reflect.MakeSlice(v.Type(), l, l) for i := 0; i < l; i++ { var err error @@ -118,20 +161,35 @@ func deserializeData(data []byte, v reflect.Value, index int) (int, error) { } return index, nil case reflect.String: - b := []byte{data[index], data[index+1], data[index+2], data[index+3], - data[index+4], data[index+5], data[index+6], data[index+7]} + b, err := readBytes(data, index, 8) + if err != nil { + return index, err + } l := binary.LittleEndian.Uint64(b) index += 8 + if l > uint64(maxInt()) { + return index, fmt.Errorf("deserialize failed: string length %d exceeds int range", l) + } length := int(l) + if length > len(data)-index { + return index, fmt.Errorf("deserialize failed: string length %d exceeds remaining %d", length, len(data)-index) + } str := make([]byte, length) copy(str[:], data[index:index+length]) v.SetString(string(str)) return index + length, nil case reflect.Ptr: - if data[index] == 0 { + b, err := readBytes(data, index, 1) + if err != nil { + return index, err + } + if b[0] == 0 { v.SetZero() return index + 1, nil } + if v.IsNil() { + v.Set(reflect.New(v.Type().Elem())) + } return deserializeData(data, v.Elem(), index+1) case reflect.Struct: for i := 0; i < v.NumField(); i++ { diff --git a/crates/go-runtime/zkvm_runtime/deserialize_test.go b/crates/go-runtime/zkvm_runtime/deserialize_test.go new file mode 100644 index 000000000..6b0b05b53 --- /dev/null +++ b/crates/go-runtime/zkvm_runtime/deserialize_test.go @@ -0,0 +1,51 @@ +package zkvm_runtime + +import ( + "reflect" + "testing" +) + +type nestedPayload struct { + Value *uint32 +} + +func TestDeserializeDataRejectsTruncatedInput(t *testing.T) { + var out uint16 + _, err := deserializeData([]byte{0x01}, reflect.ValueOf(&out).Elem(), 0) + if err == nil { + t.Fatal("expected an error for truncated input") + } +} + +func TestDeserializeDataRejectsOversizedSliceLength(t *testing.T) { + var out []byte + data := []byte{ + 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, + } + _, err := deserializeData(data, reflect.ValueOf(&out).Elem(), 0) + if err == nil { + t.Fatal("expected an error for oversized slice length") + } +} + +func TestDeserializeDataAllocatesNilPointerField(t *testing.T) { + var out nestedPayload + data := []byte{ + 0x01, + 0x78, 0x56, 0x34, 0x12, + } + index, err := deserializeData(data, reflect.ValueOf(&out).Elem(), 0) + if err != nil { + t.Fatalf("unexpected error: %v", err) + } + if index != len(data) { + t.Fatalf("unexpected index: got %d want %d", index, len(data)) + } + if out.Value == nil { + t.Fatal("expected nil pointer field to be allocated") + } + if *out.Value != 0x12345678 { + t.Fatalf("unexpected pointer value: got %x want %x", *out.Value, 0x12345678) + } +} diff --git a/crates/go-runtime/zkvm_runtime/runtime.go b/crates/go-runtime/zkvm_runtime/runtime.go index 2ddb90778..4b2e52a94 100644 --- a/crates/go-runtime/zkvm_runtime/runtime.go +++ b/crates/go-runtime/zkvm_runtime/runtime.go @@ -103,12 +103,23 @@ const MAX_MEMORY int = 0x7f000000 var RESERVED_INPUT_PTR int = MAX_MEMORY - EMBEDDED_RESERVED_INPUT_REGION_SIZE +func readReservedInput(capacity int) int { + addr := RESERVED_INPUT_PTR + if capacity < 0 { + panic("input region overflowed") + } + if addr < 0 || addr > MAX_MEMORY-capacity { + panic("input region overflowed") + } + RESERVED_INPUT_PTR = addr + capacity + return addr +} + func Read[T any]() T { len := SyscallHintLen() var value []byte capacity := (len + 3) / 4 * 4 - addr := RESERVED_INPUT_PTR - RESERVED_INPUT_PTR += capacity + addr := readReservedInput(capacity) ptr := unsafe.Pointer(uintptr(addr)) value = unsafe.Slice((*byte)(ptr), capacity) var result T diff --git a/crates/go-runtime/zkvm_runtime/runtime_test.go b/crates/go-runtime/zkvm_runtime/runtime_test.go new file mode 100644 index 000000000..da798efdb --- /dev/null +++ b/crates/go-runtime/zkvm_runtime/runtime_test.go @@ -0,0 +1,33 @@ +//go:build mipsle +// +build mipsle + +package zkvm_runtime + +import "testing" + +func TestReadReservedInputAdvancesPointer(t *testing.T) { + oldPtr := RESERVED_INPUT_PTR + defer func() { RESERVED_INPUT_PTR = oldPtr }() + + RESERVED_INPUT_PTR = MAX_MEMORY - EMBEDDED_RESERVED_INPUT_REGION_SIZE + addr := readReservedInput(16) + if addr != MAX_MEMORY-EMBEDDED_RESERVED_INPUT_REGION_SIZE { + t.Fatalf("unexpected addr: got %x want %x", addr, MAX_MEMORY-EMBEDDED_RESERVED_INPUT_REGION_SIZE) + } + if RESERVED_INPUT_PTR != addr+16 { + t.Fatalf("unexpected ptr: got %x want %x", RESERVED_INPUT_PTR, addr+16) + } +} + +func TestReadReservedInputPanicsOnOverflow(t *testing.T) { + oldPtr := RESERVED_INPUT_PTR + defer func() { RESERVED_INPUT_PTR = oldPtr }() + + RESERVED_INPUT_PTR = MAX_MEMORY - 8 + defer func() { + if r := recover(); r == nil { + t.Fatal("expected panic on overflow") + } + }() + _ = readReservedInput(16) +} diff --git a/crates/picus/README.md b/crates/picus/README.md index 43cf57f37..706416678 100644 --- a/crates/picus/README.md +++ b/crates/picus/README.md @@ -85,14 +85,6 @@ Rule of thumb: check determinism of that successor state. If the next-row value is padding-only, phase-local, or intentionally existential, do not expose it. -Concrete example: - -- In `BooleanCircuitGarble`, `delta` and `checks` are carried across gate rows, so - they are marked with `#[picus(transition_input, transition_output)]`. -- That tells Picus to treat the current row's `delta` / `checks` as inputs and the - immediate next row's `delta` / `checks` as outputs in the phases where successor - state is part of the interface. - ## Picus Projections `PicusAnnotations` describe concrete trace storage fields on a chip row. diff --git a/crates/picus/src/main.rs b/crates/picus/src/main.rs index fa132e4c0..42748a223 100644 --- a/crates/picus/src/main.rs +++ b/crates/picus/src/main.rs @@ -813,7 +813,7 @@ fn normalize_constraint( } fn postprocess_module(chip_name: &str, module: &mut PicusModule) { - if matches!(chip_name, "BooleanCircuitGarble" | "SysLinux" | "MemoryInstrs") { + if matches!(chip_name, "SysLinux" | "MemoryInstrs") { let protected_vars = collect_interface_vars(module); loop { // The guarded-width simplifier is only sound when the target variable is diff --git a/crates/prover/vk_map.bin b/crates/prover/vk_map.bin index 12d52f3ea..e2ad9f658 100644 Binary files a/crates/prover/vk_map.bin and b/crates/prover/vk_map.bin differ diff --git a/crates/recursion/circuit/src/machine/compress.rs b/crates/recursion/circuit/src/machine/compress.rs index 5128eb2fc..b69e470a0 100644 --- a/crates/recursion/circuit/src/machine/compress.rs +++ b/crates/recursion/circuit/src/machine/compress.rs @@ -2,7 +2,6 @@ use std::{ array, borrow::{Borrow, BorrowMut}, marker::PhantomData, - mem::MaybeUninit, }; use itertools::{izip, Itertools}; @@ -103,9 +102,8 @@ where // Initialize the values for the aggregated public output. - let mut reduce_public_values_stream: Vec> = (0..RECURSIVE_PROOF_NUM_PV_ELTS) - .map(|_| unsafe { MaybeUninit::zeroed().assume_init() }) - .collect(); + let mut reduce_public_values_stream: Vec> = + (0..RECURSIVE_PROOF_NUM_PV_ELTS).map(|_| builder.uninit()).collect(); let compress_public_values: &mut RecursionPublicValues<_> = reduce_public_values_stream.as_mut_slice().borrow_mut(); @@ -115,27 +113,22 @@ where assert!(!vks_and_proofs.is_empty()); // Initialize the consistency check variables. - let mut zkm_vk_digest: [Felt<_>; DIGEST_SIZE] = - array::from_fn(|_| unsafe { MaybeUninit::zeroed().assume_init() }); - let mut pc: Felt<_> = unsafe { MaybeUninit::zeroed().assume_init() }; - let mut shard: Felt<_> = unsafe { MaybeUninit::zeroed().assume_init() }; + let mut zkm_vk_digest: [Felt<_>; DIGEST_SIZE] = array::from_fn(|_| builder.uninit()); + let mut pc: Felt<_> = builder.uninit(); + let mut shard: Felt<_> = builder.uninit(); let mut exit_code: Felt<_> = builder.uninit(); - let mut execution_shard: Felt<_> = unsafe { MaybeUninit::zeroed().assume_init() }; + let mut execution_shard: Felt<_> = builder.uninit(); let mut committed_value_digest: [Word>; PV_DIGEST_NUM_WORDS] = - array::from_fn(|_| { - Word(array::from_fn(|_| unsafe { MaybeUninit::zeroed().assume_init() })) - }); + array::from_fn(|_| Word(array::from_fn(|_| builder.uninit()))); let mut deferred_proofs_digest: [Felt<_>; POSEIDON_NUM_WORDS] = - array::from_fn(|_| unsafe { MaybeUninit::zeroed().assume_init() }); + array::from_fn(|_| builder.uninit()); let mut reconstruct_deferred_digest: [Felt<_>; POSEIDON_NUM_WORDS] = - core::array::from_fn(|_| unsafe { MaybeUninit::zeroed().assume_init() }); + core::array::from_fn(|_| builder.uninit()); let mut global_cumulative_sums = Vec::new(); - let mut init_addr_bits: [Felt<_>; 32] = - core::array::from_fn(|_| unsafe { MaybeUninit::zeroed().assume_init() }); - let mut finalize_addr_bits: [Felt<_>; 32] = - core::array::from_fn(|_| unsafe { MaybeUninit::zeroed().assume_init() }); + let mut init_addr_bits: [Felt<_>; 32] = core::array::from_fn(|_| builder.uninit()); + let mut finalize_addr_bits: [Felt<_>; 32] = core::array::from_fn(|_| builder.uninit()); // Initialize a flag to denote if any of the recursive proofs represents a shard range // where at least once of the shards is an execution shard (i.e. contains cpu). diff --git a/crates/recursion/circuit/src/machine/core.rs b/crates/recursion/circuit/src/machine/core.rs index b4d7617e7..c621e50bb 100644 --- a/crates/recursion/circuit/src/machine/core.rs +++ b/crates/recursion/circuit/src/machine/core.rs @@ -2,7 +2,6 @@ use std::{ array, borrow::{Borrow, BorrowMut}, marker::PhantomData, - mem::MaybeUninit, }; use itertools::Itertools; @@ -126,29 +125,27 @@ where input; // Initialize shard variables. - let mut initial_shard: Felt<_> = unsafe { MaybeUninit::zeroed().assume_init() }; - let mut current_shard: Felt<_> = unsafe { MaybeUninit::zeroed().assume_init() }; + let mut initial_shard: Felt<_> = builder.uninit(); + let mut current_shard: Felt<_> = builder.uninit(); // Initialize execution shard variables. - let mut initial_execution_shard: Felt<_> = unsafe { MaybeUninit::zeroed().assume_init() }; - let mut current_execution_shard: Felt<_> = unsafe { MaybeUninit::zeroed().assume_init() }; + let mut initial_execution_shard: Felt<_> = builder.uninit(); + let mut current_execution_shard: Felt<_> = builder.uninit(); // Initialize program counter variables. - let mut start_pc: Felt<_> = unsafe { MaybeUninit::zeroed().assume_init() }; - let mut current_pc: Felt<_> = unsafe { MaybeUninit::zeroed().assume_init() }; + let mut start_pc: Felt<_> = builder.uninit(); + let mut current_pc: Felt<_> = builder.uninit(); // Initialize memory initialization and finalization variables. let mut initial_previous_init_addr_bits: [Felt<_>; 32] = - unsafe { MaybeUninit::zeroed().assume_init() }; + array::from_fn(|_| builder.uninit()); let mut initial_previous_finalize_addr_bits: [Felt<_>; 32] = - unsafe { MaybeUninit::zeroed().assume_init() }; - let mut current_init_addr_bits: [Felt<_>; 32] = - unsafe { MaybeUninit::zeroed().assume_init() }; - let mut current_finalize_addr_bits: [Felt<_>; 32] = - unsafe { MaybeUninit::zeroed().assume_init() }; + array::from_fn(|_| builder.uninit()); + let mut current_init_addr_bits: [Felt<_>; 32] = array::from_fn(|_| builder.uninit()); + let mut current_finalize_addr_bits: [Felt<_>; 32] = array::from_fn(|_| builder.uninit()); // Initialize the exit code variable. - let mut exit_code: Felt<_> = unsafe { MaybeUninit::zeroed().assume_init() }; + let mut exit_code: Felt<_> = builder.uninit(); // Initialize the public values digest. let mut committed_value_digest: [Word>; PV_DIGEST_NUM_WORDS] = diff --git a/crates/recursion/circuit/src/machine/wrap.rs b/crates/recursion/circuit/src/machine/wrap.rs index 604669a13..b2586b85c 100644 --- a/crates/recursion/circuit/src/machine/wrap.rs +++ b/crates/recursion/circuit/src/machine/wrap.rs @@ -12,7 +12,7 @@ use zkm_stark::{air::MachineAir, StarkMachine}; use crate::{ challenger::CanObserveVariable, constraints::RecursiveVerifierConstraintFolder, - machine::{assert_root_public_values_valid, RootPublicValues}, + machine::{assert_complete, assert_root_public_values_valid, RootPublicValues}, stark::StarkVerifier, CircuitConfig, KoalaBearFriConfigVariable, }; @@ -78,6 +78,8 @@ where // Get the public values, and assert that they are valid. let public_values: &RootPublicValues> = proof.public_values.as_slice().borrow(); assert_root_public_values_valid::(builder, public_values); + builder.assert_felt_eq(public_values.inner.is_complete, C::F::ONE); + assert_complete(builder, &public_values.inner, public_values.inner.is_complete); // Reflect the public values to the next level. if zkm_imm_wrap_vk_mode() { diff --git a/crates/recursion/compiler/src/ir/collections.rs b/crates/recursion/compiler/src/ir/collections.rs index dca00fa37..ccad4cbd7 100644 --- a/crates/recursion/compiler/src/ir/collections.rs +++ b/crates/recursion/compiler/src/ir/collections.rs @@ -30,9 +30,7 @@ impl> Array { /// Shifts the array by `shift` elements. pub fn shift(&self, builder: &mut Builder, shift: Var) -> Array { match self { - Self::Fixed(_) => { - todo!() - } + Self::Fixed(_) => unreachable!("Array::Fixed does not support shift()"), Self::Dyn(ptr, len) => { assert!(V::size_of() == 1, "only support variables of size 1"); let new_address = builder.eval(ptr.address + shift); @@ -47,9 +45,7 @@ impl> Array { /// Truncates the array to `len` elements. pub fn truncate(&self, builder: &mut Builder, len: Usize) { match self { - Self::Fixed(_) => { - todo!() - } + Self::Fixed(_) => unreachable!("Array::Fixed does not support truncate()"), Self::Dyn(_, old_len) => { builder.assign(*old_len, len); } @@ -157,9 +153,7 @@ impl Builder { let index = index.into(); match slice { - Array::Fixed(_) => { - todo!() - } + Array::Fixed(_) => unreachable!("Array::Fixed does not support get_ptr()"), Array::Dyn(ptr, len) => { if self.debug { let index_v = index.materialize(self); @@ -184,8 +178,13 @@ impl Builder { let index = index.into(); match slice { - Array::Fixed(_) => { - todo!() + Array::Fixed(slice) => { + if let Usize::Const(idx) = index { + let value: V = self.eval(value); + slice[idx] = value; + } else { + unreachable!("Array::Fixed does not support symbolic indices in set()") + } } Array::Dyn(ptr, len) => { if self.debug { @@ -210,8 +209,12 @@ impl Builder { let index = index.into(); match slice { - Array::Fixed(_) => { - todo!() + Array::Fixed(slice) => { + if let Usize::Const(idx) = index { + slice[idx] = value; + } else { + unreachable!("Array::Fixed does not support symbolic indices in set_value()") + } } Array::Dyn(ptr, _) => { let index = MemIndex { index, offset: 0, size: V::size_of() }; @@ -364,3 +367,61 @@ impl + MemVariable, const N: usize> FromConstan value.map(|x| V::constant(x, builder)) } } + +#[cfg(test)] +mod tests { + use super::*; + use crate::config::OuterConfig; + use crate::ir::Felt; + use p3_field::FieldAlgebra; + + type C = OuterConfig; + type N = ::N; + type Ff = ::F; + + #[test] + fn fixed_array_set_and_set_value_update_elements() { + let mut builder = Builder::::default(); + let one: Felt = builder.eval(Ff::from_canonical_u32(1)); + let two: Felt = builder.eval(Ff::from_canonical_u32(2)); + let three: Felt = builder.eval(Ff::from_canonical_u32(3)); + let seven: Felt = builder.eval(Ff::from_canonical_u32(7)); + let nine: Felt = builder.eval(Ff::from_canonical_u32(9)); + let mut array = builder.vec::>(vec![one, two, three]); + + builder.set_value(&mut array, 1, seven); + builder.set(&mut array, 2, nine); + + let values = array.vec(); + assert_eq!(values.len(), 3); + assert_eq!(array.len(), Usize::Const(3)); + } + + #[test] + #[should_panic(expected = "Array::Fixed does not support shift()")] + fn fixed_array_shift_panics_with_clear_message() { + let mut builder = Builder::::default(); + let one: Felt = builder.eval(Ff::from_canonical_u32(1)); + let shift = builder.eval(N::from_canonical_u32(1)); + let array = builder.vec::>(vec![one]); + let _ = array.shift(&mut builder, shift); + } + + #[test] + #[should_panic(expected = "Array::Fixed does not support truncate()")] + fn fixed_array_truncate_panics_with_clear_message() { + let mut builder = Builder::::default(); + let one: Felt = builder.eval(Ff::from_canonical_u32(1)); + let array = builder.vec::>(vec![one]); + array.truncate(&mut builder, Usize::Const(0)); + } + + #[test] + #[should_panic(expected = "Array::Fixed does not support get_ptr()")] + fn fixed_array_get_ptr_panics_with_clear_message() { + let mut builder = Builder::::default(); + let one: Felt = builder.eval(Ff::from_canonical_u32(1)); + let array = builder.vec::>(vec![one]); + let _ = builder.get_ptr(&array, 0usize); + } +} diff --git a/crates/stark/src/machine.rs b/crates/stark/src/machine.rs index 32a96eb6f..c5ca72afd 100644 --- a/crates/stark/src/machine.rs +++ b/crates/stark/src/machine.rs @@ -10,7 +10,7 @@ use p3_uni_stark::{get_symbolic_constraints, SymbolicAirBuilder}; use serde::de::DeserializeOwned; use serde::{Deserialize, Serialize}; -use std::{cmp::Reverse, env, fmt::Debug, iter::once, time::Instant}; +use std::{cmp::Reverse, collections::HashSet, env, fmt::Debug, iter::once, time::Instant}; use tracing::instrument; use super::{debug_constraints, Dom}; @@ -177,6 +177,56 @@ impl>> StarkMachine { .sorted_by_key(|chip| chip_ordering.get(&chip.name())) } + fn validate_chip_ordering( + &self, + vk: &StarkVerifyingKey, + proof: &ShardProof, + ) -> Result<(), VerificationError> { + let n = proof.opened_values.chips.len(); + if proof.chip_ordering.len() != n { + return Err(VerificationError::InvalidChipOrdering( + "chip ordering length does not match opened values".to_string(), + )); + } + + let known_chips = self.chips.iter().map(|chip| chip.name()).collect::>(); + let mut seen_indices = vec![false; n]; + for (name, &index) in &proof.chip_ordering { + if !known_chips.contains(name) { + return Err(VerificationError::InvalidChipOrdering(format!( + "unknown chip in ordering: {name}" + ))); + } + if index >= n { + return Err(VerificationError::InvalidChipOrdering(format!( + "chip ordering index out of bounds for {name}: {index}" + ))); + } + if seen_indices[index] { + return Err(VerificationError::InvalidChipOrdering(format!( + "duplicate chip ordering index: {index}" + ))); + } + seen_indices[index] = true; + } + + if seen_indices.iter().any(|seen| !seen) { + return Err(VerificationError::InvalidChipOrdering( + "chip ordering indices are not contiguous".to_string(), + )); + } + + for (name, _, _) in &vk.chip_information { + if !proof.chip_ordering.contains_key(name) { + return Err(VerificationError::InvalidChipOrdering(format!( + "missing preprocessed chip in ordering: {name}" + ))); + } + } + + Ok(()) + } + /// Returns the config of the machine. pub const fn config(&self) -> &SC { &self.config @@ -637,6 +687,8 @@ impl> + Air>(); let mut shard_challenger = challenger.clone(); diff --git a/crates/stark/src/opts.rs b/crates/stark/src/opts.rs index 74f6d34a4..9a53d467a 100644 --- a/crates/stark/src/opts.rs +++ b/crates/stark/src/opts.rs @@ -68,7 +68,6 @@ impl ZKMProverOpts { opts.core_opts.split_opts.keccak /= divisor; opts.core_opts.split_opts.sha_extend /= divisor; opts.core_opts.split_opts.sha_compress /= divisor; - opts.core_opts.split_opts.boolean_circuit_garble /= divisor; opts.core_opts.split_opts.memory /= divisor; opts.recursion_opts.shard_batch_size = 2; @@ -176,7 +175,6 @@ impl Default for ZKMCoreOpts { opts.split_opts.keccak /= divisor; opts.split_opts.sha_extend /= divisor; opts.split_opts.sha_compress /= divisor; - opts.split_opts.boolean_circuit_garble /= divisor; opts.split_opts.memory /= divisor; opts @@ -243,8 +241,6 @@ pub struct SplitOpts { pub sha_extend: usize, /// The threshold for sha compress events. pub sha_compress: usize, - /// The threshold for Boolean Circuit Garble events - pub boolean_circuit_garble: usize, /// The threshold for memory events. pub memory: usize, /// The threshold for combining the memory init/finalize events in to the current shard in @@ -261,7 +257,6 @@ impl SplitOpts { keccak: 8 * deferred_split_threshold / 24, sha_extend: 32 * deferred_split_threshold / 48, sha_compress: 32 * deferred_split_threshold / 80, - boolean_circuit_garble: deferred_split_threshold / 8, memory: 64 * deferred_split_threshold, combine_memory_threshold: 1 << 17, } diff --git a/crates/stark/src/verifier.rs b/crates/stark/src/verifier.rs index 52dd7b81c..dcf174f22 100644 --- a/crates/stark/src/verifier.rs +++ b/crates/stark/src/verifier.rs @@ -1,9 +1,11 @@ use core::fmt::Display; use std::{ + collections::HashSet, fmt::{Debug, Formatter}, marker::PhantomData, }; +use hashbrown::HashMap; use itertools::Itertools; use num_traits::cast::ToPrimitive; use p3_air::{Air, BaseAir}; @@ -25,6 +27,58 @@ use crate::{ pub struct Verifier(PhantomData, PhantomData); impl>> Verifier { + fn validate_chip_ordering( + vk: &StarkVerifyingKey, + chips: &[&MachineChip], + opened_values_len: usize, + chip_ordering: &HashMap, + ) -> Result<(), VerificationError> { + if chip_ordering.len() != opened_values_len { + return Err(VerificationError::InvalidChipOrdering( + "chip ordering length does not match opened values".to_string(), + )); + } + if chips.len() != opened_values_len { + return Err(VerificationError::ChipOpeningLengthMismatch); + } + + let chip_names = chips.iter().map(|chip| chip.name()).collect::>(); + let mut seen_indices = vec![false; opened_values_len]; + for (name, &index) in chip_ordering { + if !chip_names.contains(name) { + return Err(VerificationError::InvalidChipOrdering(format!( + "unexpected chip in ordering: {name}" + ))); + } + if index >= opened_values_len { + return Err(VerificationError::InvalidChipOrdering(format!( + "chip ordering index out of bounds for {name}: {index}" + ))); + } + if seen_indices[index] { + return Err(VerificationError::InvalidChipOrdering(format!( + "duplicate chip ordering index: {index}" + ))); + } + seen_indices[index] = true; + } + if seen_indices.iter().any(|seen| !seen) { + return Err(VerificationError::InvalidChipOrdering( + "chip ordering indices are not contiguous".to_string(), + )); + } + + for (name, _, _) in &vk.chip_information { + if !chip_ordering.contains_key(name) { + return Err(VerificationError::InvalidChipOrdering(format!( + "missing preprocessed chip in ordering: {name}" + ))); + } + } + + Ok(()) + } + /// Verify a proof for a collection of air chips. #[allow(clippy::too_many_lines)] pub fn verify_shard( @@ -54,6 +108,8 @@ impl>> Verifier { return Err(VerificationError::ChipOpeningLengthMismatch); } + Self::validate_chip_ordering(vk, chips, opened_values.chips.len(), chip_ordering)?; + // Assert that the byte multiplicities don't overflow. let mut max_byte_lookup_mult = 0u64; chips.iter().zip(opened_values.chips.iter()).for_each(|(chip, val)| { @@ -466,6 +522,8 @@ pub enum VerificationError { MissingCpuChip, /// The length of the chip opening does not match the expected length. ChipOpeningLengthMismatch, + /// The prover-supplied chip ordering is malformed. + InvalidChipOrdering(String), /// Cumulative sums error CumulativeSumsError(&'static str), } @@ -518,6 +576,9 @@ impl Debug for VerificationError { VerificationError::ChipOpeningLengthMismatch => { write!(f, "Chip opening length mismatch") } + VerificationError::InvalidChipOrdering(s) => { + write!(f, "Invalid chip ordering: {}", s) + } VerificationError::CumulativeSumsError(s) => write!(f, "cumulative sums error: {}", s), } } @@ -542,6 +603,9 @@ impl Display for VerificationError { VerificationError::ChipOpeningLengthMismatch => { write!(f, "Chip opening length mismatch") } + VerificationError::InvalidChipOrdering(s) => { + write!(f, "Invalid chip ordering: {}", s) + } VerificationError::CumulativeSumsError(s) => write!(f, "cumulative sums error: {}", s), } } diff --git a/crates/verifier/bn254-vk/groth16_vk.bin b/crates/verifier/bn254-vk/groth16_vk.bin index 915287056..00091bc2d 100644 Binary files a/crates/verifier/bn254-vk/groth16_vk.bin and b/crates/verifier/bn254-vk/groth16_vk.bin differ diff --git a/crates/verifier/bn254-vk/history/v1.2.7_part_stark_vk.bin b/crates/verifier/bn254-vk/history/v1.2.7_part_stark_vk.bin new file mode 100644 index 000000000..cf9600ccc Binary files /dev/null and b/crates/verifier/bn254-vk/history/v1.2.7_part_stark_vk.bin differ diff --git a/crates/verifier/bn254-vk/part_stark_vk.bin b/crates/verifier/bn254-vk/part_stark_vk.bin index 4fed7470c..cf9600ccc 100644 Binary files a/crates/verifier/bn254-vk/part_stark_vk.bin and b/crates/verifier/bn254-vk/part_stark_vk.bin differ diff --git a/crates/verifier/bn254-vk/plonk_vk.bin b/crates/verifier/bn254-vk/plonk_vk.bin index 54306e283..5fce11a52 100644 Binary files a/crates/verifier/bn254-vk/plonk_vk.bin and b/crates/verifier/bn254-vk/plonk_vk.bin differ diff --git a/crates/zkvm/entrypoint/src/syscalls/boolean_circuit_garble.rs b/crates/zkvm/entrypoint/src/syscalls/boolean_circuit_garble.rs deleted file mode 100644 index c0a7f73c2..000000000 --- a/crates/zkvm/entrypoint/src/syscalls/boolean_circuit_garble.rs +++ /dev/null @@ -1,25 +0,0 @@ -#[cfg(target_os = "zkvm")] -use core::arch::asm; - -/// Executes the boolean circuit garble -/// -/// ### Safety -/// -/// The caller must ensure that `inputs` and `output` are valid pointers to data that are aligned along -/// a four byte boundary. -#[allow(unused_variables)] -#[no_mangle] -pub extern "C" fn syscall_boolean_circuit_garble(input: *const u8, output: *mut u32) { - #[cfg(target_os = "zkvm")] - unsafe { - asm!( - "syscall", - in("$2") crate::syscalls::BOOLEAN_CIRCUIT_GARBLE, - in("$4") input, - in("$5") output, - ); - } - - #[cfg(not(target_os = "zkvm"))] - unreachable!() -} diff --git a/crates/zkvm/entrypoint/src/syscalls/mod.rs b/crates/zkvm/entrypoint/src/syscalls/mod.rs index e9007bb9e..b07047bc2 100644 --- a/crates/zkvm/entrypoint/src/syscalls/mod.rs +++ b/crates/zkvm/entrypoint/src/syscalls/mod.rs @@ -1,8 +1,6 @@ mod bigint; mod bls12381; mod bn254; -mod boolean_circuit_garble; - mod ed25519; mod fptower; mod halt; @@ -23,7 +21,6 @@ mod verify; pub use bigint::*; pub use bls12381::*; pub use bn254::*; -pub use boolean_circuit_garble::*; pub use ed25519::*; pub use fptower::*; pub use halt::*; @@ -164,6 +161,3 @@ pub const BN254_FP2_MUL: u32 = 0x01_01_00_2B; /// Executes the `POSEIDON2_PERMUTE` precompile. pub const POSEIDON2_PERMUTE: u32 = 0x00_01_00_30; - -/// Executes the `BOOLEAN_CIRCUIT_GARBLE` precompile. -pub const BOOLEAN_CIRCUIT_GARBLE: u32 = 0x00_01_00_31; diff --git a/crates/zkvm/lib/src/boolean_circuit_garble.rs b/crates/zkvm/lib/src/boolean_circuit_garble.rs deleted file mode 100644 index a9c173711..000000000 --- a/crates/zkvm/lib/src/boolean_circuit_garble.rs +++ /dev/null @@ -1,49 +0,0 @@ -use crate::syscall_boolean_circuit_garble; -pub const GATE_INFO_BYTES: usize = 68; -pub const MAX_GATES_PER_SYSCALL: usize = 62500; -pub fn boolean_circuit_garble(gates_info: &[u8]) -> bool { - // Validate layout - assert_eq!(gates_info.len() % GATE_INFO_BYTES, 16); - - let num_gates = gates_info.len() / GATE_INFO_BYTES; - let syscall_num = (num_gates - 1) / MAX_GATES_PER_SYSCALL + 1; - let base = MAX_GATES_PER_SYSCALL; - let remainder = num_gates - base * (syscall_num - 1); - - let base_bytes = base.to_le_bytes(); - let remainder_bytes = remainder.to_le_bytes(); - - let delta = &gates_info[0..16]; - let mut output = 0_u32; - let mut start_offset = 16; - for _i in 0..syscall_num - 1 { - // Gate data slice for this chunk - let end_offset = start_offset + base * GATE_INFO_BYTES; - // Precompute final input length: 4 (count) + 16 (delta) + gate bytes - let input_len = 20 + base * GATE_INFO_BYTES; - let mut input = vec![0u8; input_len]; - input[0..4].copy_from_slice(&base_bytes); - input[4..20].copy_from_slice(delta); - input[20..].copy_from_slice(&gates_info[start_offset..end_offset]); - - unsafe { - syscall_boolean_circuit_garble(input.as_ptr(), &mut output); - } - assert!(output <= 1); - if output == 0 { - return false; - } - start_offset = end_offset; - } - - let input_len = 20 + remainder * GATE_INFO_BYTES; - let mut input = vec![0u8; input_len]; - input[0..4].copy_from_slice(&remainder_bytes); - input[4..20].copy_from_slice(delta); - input[20..].copy_from_slice(&gates_info[start_offset..]); - unsafe { - syscall_boolean_circuit_garble(input.as_ptr(), &mut output); - } - assert!(output <= 1); - output == 1 -} diff --git a/crates/zkvm/lib/src/lib.rs b/crates/zkvm/lib/src/lib.rs index 9b1f2b036..7dfeb1d3a 100644 --- a/crates/zkvm/lib/src/lib.rs +++ b/crates/zkvm/lib/src/lib.rs @@ -4,7 +4,6 @@ //! `zkm_zkvm::syscalls` module. pub mod bls12381; pub mod bn254; -pub mod boolean_circuit_garble; #[cfg(feature = "ecdsa")] pub mod ecdsa; @@ -78,9 +77,6 @@ extern "C" { /// Executes the Poseidon2 permutation pub fn syscall_poseidon2_permute(state: *mut [u32; 16]); - /// Executes a Boolean Circuit Garble operation. - pub fn syscall_boolean_circuit_garble(input: *const u8, output: *mut u32); - /// Executes an uint256 multiplication on the given inputs. pub fn syscall_uint256_mulmod(x: *mut [u32; 8], y: *const [u32; 8]); diff --git a/docs/src/design/chips/cpu.md b/docs/src/design/chips/cpu.md index 3c9e12574..12d2fe6ff 100644 --- a/docs/src/design/chips/cpu.md +++ b/docs/src/design/chips/cpu.md @@ -21,7 +21,10 @@ Ziren's CPU constraints ensure instruction integrity across four key dimensions: - Flow Constraints​​ - - Program counter continuity: Ensures sequential instruction flow continuity via program counter validation. + - Program counter continuity: Consecutive real rows satisfy `local.next_pc = next.pc`. + - Delay-slot carry: For non-halting successor rows, `local.next_next_pc = next.next_pc`, so branch/jump targets survive across the delay slot. + - Sequential rows: When `is_sequential = 1`, the CPU enforces `next_next_pc = next_pc + 4`. + - Shard boundary safety: The last real row of a shard must be sequential or halt. Branch/jump rows cannot end a shard because shard public values export only `next_pc`, not `next_next_pc`. - Clock synchronization: Synchronizes timing mechanisms for system operations. - ​​Operand Constraints​​ @@ -39,3 +42,11 @@ Ziren's CPU constraints ensure instruction integrity across four key dimensions: Real-row validation: Enforces operational validity flags for non-padded execution. These constraints are implemented through AIR polynomial identities, cross-table lookup arguments, boolean assertions, and multi-set hashing ensuring verifiable MIPS execution within Ziren's zkVM framework. + +## PC Boundary Rules + +The CPU chip carries both `next_pc` and `next_next_pc` in each row. + +- `next_pc` is the address of the delay-slot instruction and is always the next row's `pc` for real transitions. +- `next_next_pc` is the PC after the delay slot. For sequential rows it equals `next_pc + 4`; for branch and jump rows it carries the taken or fall-through post-delay-slot target. +- Shard public values expose only `start_pc` and `next_pc`. Because of that, a branch or jump row cannot be the last real row of a shard; otherwise its `next_next_pc` target would be lost at the boundary. diff --git a/docs/src/design/chips/flow-ctrl.md b/docs/src/design/chips/flow-ctrl.md index 257ae651a..adc058e39 100644 --- a/docs/src/design/chips/flow-ctrl.md +++ b/docs/src/design/chips/flow-ctrl.md @@ -26,10 +26,12 @@ We use the following key constraints to validate the branch chip: - Program Counter Validation - - Range check for all PC values (`pc`, `next_pc`, `target_pc`, `next_next_pc`, etc.). - - Branching case: `next_pc` must equal `target_pc`. - - Non-branching case: `next_next_pc` must equal `next_pc + 4`. + - `next_pc` is the delay-slot PC and must match the next CPU row's `pc`. + - `next_next_pc` is the post-delay-slot PC carried by the current row. + - Taken branch case: `next_next_pc = target_pc`. + - Not-taken branch case: `next_next_pc = next_pc + 4`. - `is_branching` and `not_branching` are mutually exclusive and exhaustive for real instructions. + - Branch rows cannot terminate a shard, because shard public values export only `next_pc` and not the post-delay-slot target in `next_next_pc`. - Instruction Validity - Exactly one branch instruction flag must be active per row (`1 = is_beq + ... + is_bgtz`). @@ -76,6 +78,10 @@ We use the following key constraints to validate the jump chip: op_a_value = next_pc + 4 ``` op_a_value is saved into op_a register only when 'op_a_0 = 0'(checked in CpuChip) +- Delay-slot / target handling + - `next_pc` is still the delay-slot PC. + - The actual jump destination is carried in `next_next_pc` and becomes the successor row's `next_pc` after the delay slot executes. + - Jump rows cannot be the last real row of a shard for the same reason as branches: only `next_pc` is exported through shard public values. - Range Checking - All critical values (`op_a_value, next_pc, target_pc`) are range-checked, ensuring values are valid 32-bit words. - PC Transition Logic @@ -88,4 +94,3 @@ We use the following key constraints to validate the jump chip: ) ``` - Direct jumps (`is_jumpdirect`) use immediate operand addition. - diff --git a/docs/src/dev/precompiles.md b/docs/src/dev/precompiles.md index cc7cf710d..677af2881 100644 --- a/docs/src/dev/precompiles.md +++ b/docs/src/dev/precompiles.md @@ -92,9 +92,6 @@ extern "C" { /// Executes the Poseidon2 permutation pub fn syscall_poseidon2_permute(state: *mut [u32; 16]); - /// Executes a Boolean Circuit Garble operation. - pub fn syscall_boolean_circuit_garble(input: *const u8, output: *mut u32); - /// Executes an uint256 multiplication on the given inputs. pub fn syscall_uint256_mulmod(x: *mut [u32; 8], y: *const [u32; 8]); diff --git a/docs/src/mips-vm/mips-isa.md b/docs/src/mips-vm/mips-isa.md index 35430d74a..48cadaaf5 100644 --- a/docs/src/mips-vm/mips-isa.md +++ b/docs/src/mips-vm/mips-isa.md @@ -218,7 +218,6 @@ The support instructions are as follows: | SECP256R1_DOUBLE = 0x00_01_002D, | Executes the `SECP256R1_DOUBLE` precompile. | | SECP256R1_DECOMPRESS = 0x00_01_002E, | Executes the `SECP256R1_DECOMPRESS` precompile. | | POSEIDON2_PERMUTE = 0x00_01_0030, | Executes the `POSEIDON2_PERMUTE` precompile. | -| BOOLEAN_CIRCUIT_GARBLE = 0x00_01_0031, | Executes the `BOOLEAN_CIRCUIT_GARBLE` precompile. | | SYS_MMAP = 4210, | Executes the `Linux MMAP API` precompile. | | SYS_MMAP2 = 4090, | Executes the `Linux MMAP2 API` precompile. | | SYS_BRK = 4045, | Executes the `Linux BRK API` precompile. | diff --git a/examples/Cargo.lock b/examples/Cargo.lock index bfa2b73df..886832859 100644 --- a/examples/Cargo.lock +++ b/examples/Cargo.lock @@ -7617,7 +7617,7 @@ dependencies = [ "crypto-bigint 0.6.1", "hex", "k256", - "zkm-lib 1.2.5", + "zkm-lib 1.2.7", "zkm-zkvm", ] @@ -8580,7 +8580,7 @@ dependencies = [ [[package]] name = "zkm-build" -version = "1.2.5" +version = "1.2.7" dependencies = [ "anyhow", "cargo_metadata", @@ -8590,7 +8590,7 @@ dependencies = [ [[package]] name = "zkm-core-executor" -version = "1.2.5" +version = "1.2.7" dependencies = [ "anyhow", "bincode", @@ -8624,13 +8624,13 @@ dependencies = [ "typenum", "vec_map", "zkm-curves", - "zkm-primitives 1.2.5", + "zkm-primitives 1.2.7", "zkm-stark", ] [[package]] name = "zkm-core-machine" -version = "1.2.5" +version = "1.2.7" dependencies = [ "bincode", "cfg-if", @@ -8675,13 +8675,13 @@ dependencies = [ "zkm-core-executor", "zkm-curves", "zkm-derive", - "zkm-primitives 1.2.5", + "zkm-primitives 1.2.7", "zkm-stark", ] [[package]] name = "zkm-cuda" -version = "1.2.5" +version = "1.2.7" dependencies = [ "bincode", "ctrlc", @@ -8698,7 +8698,7 @@ dependencies = [ [[package]] name = "zkm-curves" -version = "1.2.5" +version = "1.2.7" dependencies = [ "cfg-if", "curve25519-dalek", @@ -8715,13 +8715,13 @@ dependencies = [ "thiserror 1.0.69", "tracing", "typenum", - "zkm-primitives 1.2.5", + "zkm-primitives 1.2.7", "zkm-stark", ] [[package]] name = "zkm-derive" -version = "1.2.5" +version = "1.2.7" dependencies = [ "proc-macro2", "quote", @@ -8743,14 +8743,14 @@ dependencies = [ [[package]] name = "zkm-lib" -version = "1.2.5" +version = "1.2.7" dependencies = [ "bincode", "cfg-if", "elliptic-curve", "serde", "sha2 0.10.8", - "zkm-primitives 1.2.5", + "zkm-primitives 1.2.7", ] [[package]] @@ -8773,7 +8773,7 @@ dependencies = [ [[package]] name = "zkm-primitives" -version = "1.2.5" +version = "1.2.7" dependencies = [ "bincode", "hex", @@ -8790,7 +8790,7 @@ dependencies = [ [[package]] name = "zkm-prover" -version = "1.2.5" +version = "1.2.7" dependencies = [ "anyhow", "bincode", @@ -8816,7 +8816,7 @@ dependencies = [ "tracing-subscriber", "zkm-core-executor", "zkm-core-machine", - "zkm-primitives 1.2.5", + "zkm-primitives 1.2.7", "zkm-recursion-circuit", "zkm-recursion-compiler", "zkm-recursion-core", @@ -8826,7 +8826,7 @@ dependencies = [ [[package]] name = "zkm-recursion-circuit" -version = "1.2.5" +version = "1.2.7" dependencies = [ "hashbrown 0.14.5", "itertools 0.13.0", @@ -8849,7 +8849,7 @@ dependencies = [ "zkm-core-executor", "zkm-core-machine", "zkm-derive", - "zkm-primitives 1.2.5", + "zkm-primitives 1.2.7", "zkm-recursion-compiler", "zkm-recursion-core", "zkm-recursion-gnark-ffi", @@ -8858,7 +8858,7 @@ dependencies = [ [[package]] name = "zkm-recursion-compiler" -version = "1.2.5" +version = "1.2.7" dependencies = [ "backtrace", "itertools 0.13.0", @@ -8870,7 +8870,7 @@ dependencies = [ "tracing", "vec_map", "zkm-core-machine", - "zkm-primitives 1.2.5", + "zkm-primitives 1.2.7", "zkm-recursion-core", "zkm-recursion-derive", "zkm-stark", @@ -8878,7 +8878,7 @@ dependencies = [ [[package]] name = "zkm-recursion-core" -version = "1.2.5" +version = "1.2.7" dependencies = [ "backtrace", "ff 0.13.1", @@ -8908,13 +8908,13 @@ dependencies = [ "zkhash", "zkm-core-machine", "zkm-derive", - "zkm-primitives 1.2.5", + "zkm-primitives 1.2.7", "zkm-stark", ] [[package]] name = "zkm-recursion-derive" -version = "1.2.5" +version = "1.2.7" dependencies = [ "quote", "syn 1.0.109", @@ -8922,7 +8922,7 @@ dependencies = [ [[package]] name = "zkm-recursion-gnark-ffi" -version = "1.2.5" +version = "1.2.7" dependencies = [ "anyhow", "bincode", @@ -8945,7 +8945,7 @@ dependencies = [ [[package]] name = "zkm-sdk" -version = "1.2.5" +version = "1.2.7" dependencies = [ "alloy-primitives", "alloy-signer", @@ -8984,14 +8984,14 @@ dependencies = [ "zkm-core-executor", "zkm-core-machine", "zkm-cuda", - "zkm-primitives 1.2.5", + "zkm-primitives 1.2.7", "zkm-prover", "zkm-stark", ] [[package]] name = "zkm-stark" -version = "1.2.5" +version = "1.2.7" dependencies = [ "arrayref", "hashbrown 0.14.5", @@ -9026,13 +9026,13 @@ dependencies = [ "tracing-forest", "tracing-subscriber", "zkm-derive", - "zkm-primitives 1.2.5", + "zkm-primitives 1.2.7", "zkm-zkvm", ] [[package]] name = "zkm-verifier" -version = "1.2.5" +version = "1.2.7" dependencies = [ "anyhow", "bincode", @@ -9054,14 +9054,14 @@ dependencies = [ "thiserror 2.0.18", "zkm-core-executor", "zkm-core-machine", - "zkm-primitives 1.2.5", + "zkm-primitives 1.2.7", "zkm-recursion-core", "zkm-stark", ] [[package]] name = "zkm-zkvm" -version = "1.2.5" +version = "1.2.7" dependencies = [ "bincode", "cfg-if", @@ -9075,8 +9075,8 @@ dependencies = [ "rand 0.8.5", "serde", "sha2 0.10.8", - "zkm-lib 1.2.5", - "zkm-primitives 1.2.5", + "zkm-lib 1.2.7", + "zkm-primitives 1.2.7", ] [[package]]