diff --git a/ceno_zkvm/src/instructions/riscv/insn_base.rs b/ceno_zkvm/src/instructions/riscv/insn_base.rs index bca216b66..0412dfb09 100644 --- a/ceno_zkvm/src/instructions/riscv/insn_base.rs +++ b/ceno_zkvm/src/instructions/riscv/insn_base.rs @@ -3,7 +3,7 @@ use ff_ext::{ExtensionField, FieldInto, SmallField}; use itertools::Itertools; use p3::field::{Field, FieldAlgebra}; -use super::constants::{PC_STEP_SIZE, UINT_LIMBS, UInt}; +use super::constants::{BIT_WIDTH, PC_STEP_SIZE, UINT_LIMBS, UInt}; use crate::{ chip_handler::{ AddressExpr, GlobalStateRegisterMachineChipOperations, MemoryChipOperations, MemoryExpr, @@ -368,6 +368,7 @@ impl WriteMEM { pub struct MemAddr { addr: UInt, low_bits: Vec, + max_bits: usize, } impl MemAddr { @@ -393,6 +394,17 @@ impl MemAddr { self.addr.address_expr() } + pub fn uint_unaligned(&self) -> UInt { + UInt::from_exprs_unchecked(self.addr.expr()) + } + + pub fn uint_align2(&self) -> UInt { + UInt::from_exprs_unchecked(vec![ + self.addr.limbs[0].expr() - &self.low_bit_exprs()[0], + self.addr.limbs[1].expr(), + ]) + } + /// Represent the address aligned to 2 bytes. pub fn expr_align2(&self) -> AddressExpr { self.addr.address_expr() - &self.low_bit_exprs()[0] @@ -404,6 +416,14 @@ impl MemAddr { self.addr.address_expr() - &low_bits[1] * 2 - &low_bits[0] } + pub fn uint_align4(&self) -> UInt { + let low_bits = self.low_bit_exprs(); + UInt::from_exprs_unchecked(vec![ + self.addr.limbs[0].expr() - &low_bits[1] * 2 - &low_bits[0], + self.addr.limbs[1].expr(), + ]) + } + /// Expressions of the low bits of the address, LSB-first: [bit_0, bit_1]. pub fn low_bit_exprs(&self) -> Vec> { iter::repeat_n(Expression::ZERO, self.n_zeros()) @@ -412,6 +432,14 @@ impl MemAddr { } fn construct(cb: &mut CircuitBuilder, n_zeros: usize) -> Result { + Self::construct_with_max_bits(cb, n_zeros, BIT_WIDTH) + } + + pub fn construct_with_max_bits( + cb: &mut CircuitBuilder, + n_zeros: usize, + max_bits: usize, + ) -> Result { assert!(n_zeros <= Self::N_LOW_BITS); // The address as two u16 limbs. @@ -442,11 +470,19 @@ impl MemAddr { cb.assert_ux::<_, _, 14>(|| "mid_u14", mid_u14)?; // Range check the high limb. - for high_u16 in limbs.iter().skip(1) { - cb.assert_ux::<_, _, 16>(|| "high_u16", high_u16.clone())?; + for (i, high_limb) in limbs.iter().enumerate().skip(1) { + cb.assert_ux_v2( + || "high_limb", + high_limb.clone(), + (max_bits - i * 16).min(16), + )?; } - Ok(MemAddr { addr, low_bits }) + Ok(MemAddr { + addr, + low_bits, + max_bits, + }) } pub fn assign_instance( @@ -470,7 +506,8 @@ impl MemAddr { // Range check the high limb. for i in 1..UINT_LIMBS { let high_u16 = (addr >> (i * 16)) & 0xffff; - lkm.assert_ux::<16>(high_u16 as u64); + println!("assignment max bit {}", (self.max_bits - i * 16).min(16)); + lkm.assert_ux_v2(high_u16 as u64, (self.max_bits - i * 16).min(16)); } Ok(()) diff --git a/ceno_zkvm/src/instructions/riscv/jump.rs b/ceno_zkvm/src/instructions/riscv/jump.rs index b57aadbbb..7bf1a41f6 100644 --- a/ceno_zkvm/src/instructions/riscv/jump.rs +++ b/ceno_zkvm/src/instructions/riscv/jump.rs @@ -1,8 +1,22 @@ +#[cfg(not(feature = "u16limb_circuit"))] mod jal; +#[cfg(feature = "u16limb_circuit")] +mod jal_v2; + +#[cfg(not(feature = "u16limb_circuit"))] mod jalr; +#[cfg(feature = "u16limb_circuit")] +mod jalr_v2; +#[cfg(not(feature = "u16limb_circuit"))] pub use jal::JalInstruction; +#[cfg(feature = "u16limb_circuit")] +pub use jal_v2::JalInstruction; + +#[cfg(not(feature = "u16limb_circuit"))] pub use jalr::JalrInstruction; +#[cfg(feature = "u16limb_circuit")] +pub use jalr_v2::JalrInstruction; #[cfg(test)] mod test; diff --git a/ceno_zkvm/src/instructions/riscv/jump/jal_v2.rs b/ceno_zkvm/src/instructions/riscv/jump/jal_v2.rs new file mode 100644 index 000000000..cd6ad194b --- /dev/null +++ b/ceno_zkvm/src/instructions/riscv/jump/jal_v2.rs @@ -0,0 +1,113 @@ +use std::marker::PhantomData; + +use ff_ext::ExtensionField; + +use crate::{ + circuit_builder::CircuitBuilder, + error::ZKVMError, + instructions::{ + Instruction, + riscv::{ + constants::{PC_BITS, UINT_BYTE_LIMBS, UInt8}, + j_insn::JInstructionConfig, + }, + }, + structs::ProgramParams, + utils::split_to_u8, + witness::LkMultiplicity, +}; +use ceno_emul::{InsnKind, PC_STEP_SIZE}; +use gkr_iop::tables::{LookupTable, ops::XorTable}; +use multilinear_extensions::{Expression, ToExpr}; +use p3::field::FieldAlgebra; + +pub struct JalConfig { + pub j_insn: JInstructionConfig, + pub rd_written: UInt8, +} + +pub struct JalInstruction(PhantomData); + +/// JAL instruction circuit +/// +/// Note: does not validate that next_pc is aligned by 4-byte increments, which +/// should be verified by lookup argument of the next execution step against +/// the program table +/// +/// Assumption: values for valid initial program counter must lie between +/// 2^20 and 2^32 - 2^20 + 2 inclusive, probably enforced by the static +/// program lookup table. If this assumption does not hold, then resulting +/// value for next_pc may not correctly wrap mod 2^32 because of the use +/// of native WitIn values for address space arithmetic. +impl Instruction for JalInstruction { + type InstructionConfig = JalConfig; + + fn name() -> String { + format!("{:?}", InsnKind::JAL) + } + + fn construct_circuit( + circuit_builder: &mut CircuitBuilder, + _params: &ProgramParams, + ) -> Result, ZKVMError> { + let rd_written = UInt8::new(|| "rd_written", circuit_builder)?; + let rd_exprs = rd_written.expr(); + + let j_insn = JInstructionConfig::construct_circuit( + circuit_builder, + InsnKind::JAL, + rd_written.register_expr(), + )?; + + // constrain rd_exprs [PC_BITS .. u32::BITS] are all 0 via xor + let last_limb_bits = PC_BITS - UInt8::::LIMB_BITS * (UInt8::::NUM_LIMBS - 1); + let additional_bits = + (last_limb_bits..UInt8::::LIMB_BITS).fold(0, |acc, x| acc + (1 << x)); + let additional_bits = E::BaseField::from_canonical_u32(additional_bits); + circuit_builder.logic_u8( + LookupTable::Xor, + rd_exprs[3].expr(), + additional_bits.expr(), + rd_exprs[3].expr() + additional_bits.expr(), + )?; + + circuit_builder.require_equal( + || "jal rd_written", + rd_exprs + .iter() + .enumerate() + .fold(Expression::ZERO, |acc, (i, val)| { + acc + val.expr() + * E::BaseField::from_canonical_u32(1 << (i * UInt8::::LIMB_BITS)).expr() + }), + j_insn.vm_state.pc.expr() + PC_STEP_SIZE, + )?; + + Ok(JalConfig { j_insn, rd_written }) + } + + fn assign_instance( + config: &Self::InstructionConfig, + instance: &mut [E::BaseField], + lk_multiplicity: &mut LkMultiplicity, + step: &ceno_emul::StepRecord, + ) -> Result<(), ZKVMError> { + config + .j_insn + .assign_instance(instance, lk_multiplicity, step)?; + + let rd_written = split_to_u8(step.rd().unwrap().value.after); + config.rd_written.assign_limbs(instance, &rd_written); + for val in &rd_written { + lk_multiplicity.assert_ux::<8>(*val as u64); + } + + // constrain pc msb limb range via xor + let last_limb_bits = PC_BITS - UInt8::::LIMB_BITS * (UINT_BYTE_LIMBS - 1); + let additional_bits = + (last_limb_bits..UInt8::::LIMB_BITS).fold(0, |acc, x| acc + (1 << x)); + lk_multiplicity.logic_u8::(rd_written[3] as u64, additional_bits as u64); + + Ok(()) + } +} diff --git a/ceno_zkvm/src/instructions/riscv/jump/jalr.rs b/ceno_zkvm/src/instructions/riscv/jump/jalr.rs index fe077d464..f1ba94aa7 100644 --- a/ceno_zkvm/src/instructions/riscv/jump/jalr.rs +++ b/ceno_zkvm/src/instructions/riscv/jump/jalr.rs @@ -53,8 +53,6 @@ impl Instruction for JalrInstruction { circuit_builder, InsnKind::JALR, imm.expr(), - #[cfg(feature = "u16limb_circuit")] - 0.into(), rs1_read.register_expr(), rd_written.register_expr(), true, diff --git a/ceno_zkvm/src/instructions/riscv/jump/jalr_v2.rs b/ceno_zkvm/src/instructions/riscv/jump/jalr_v2.rs new file mode 100644 index 000000000..66bb06c26 --- /dev/null +++ b/ceno_zkvm/src/instructions/riscv/jump/jalr_v2.rs @@ -0,0 +1,184 @@ +use ff_ext::ExtensionField; +use std::marker::PhantomData; + +use crate::{ + Value, + chip_handler::general::InstFetch, + circuit_builder::CircuitBuilder, + error::ZKVMError, + instructions::{ + Instruction, + riscv::{ + constants::{PC_BITS, UINT_LIMBS, UInt}, + i_insn::IInstructionConfig, + insn_base::{MemAddr, ReadRS1, StateInOut, WriteRD}, + }, + }, + structs::ProgramParams, + tables::InsnRecord, + utils::imm_sign_extend, + witness::{LkMultiplicity, set_val}, +}; +use ceno_emul::{InsnKind, PC_STEP_SIZE}; +use ff_ext::FieldInto; +use multilinear_extensions::{Expression, ToExpr, WitIn}; +use p3::field::{Field, FieldAlgebra}; + +pub struct JalrConfig { + pub i_insn: IInstructionConfig, + pub rs1_read: UInt, + pub imm: WitIn, + pub imm_sign: WitIn, + pub jump_pc_addr: MemAddr, + pub rd_high: WitIn, +} + +pub struct JalrInstruction(PhantomData); + +/// JALR instruction circuit +/// NOTE: does not validate that next_pc is aligned by 4-byte increments, which +/// should be verified by lookup argument of the next execution step against +/// the program table +impl Instruction for JalrInstruction { + type InstructionConfig = JalrConfig; + + fn name() -> String { + format!("{:?}", InsnKind::JALR) + } + + fn construct_circuit( + circuit_builder: &mut CircuitBuilder, + _params: &ProgramParams, + ) -> Result, ZKVMError> { + assert_eq!(UINT_LIMBS, 2); + let rs1_read = UInt::new_unchecked(|| "rs1_read", circuit_builder)?; // unsigned 32-bit value + let imm = circuit_builder.create_witin(|| "imm"); // signed 12-bit value + let imm_sign = circuit_builder.create_witin(|| "imm_sign"); + // State in and out + let vm_state = StateInOut::construct_circuit(circuit_builder, true)?; + let rd_high = circuit_builder.create_witin(|| "rd_high"); + let rd_low: Expression<_> = vm_state.pc.expr() + + E::BaseField::from_canonical_usize(PC_STEP_SIZE).expr() + - rd_high.expr() * E::BaseField::from_canonical_u32(1 << UInt::::LIMB_BITS).expr(); + // rd range check + // rd_low + circuit_builder.assert_ux_v2(|| "rd_low_u16", rd_low.expr(), UInt::::LIMB_BITS)?; + // rd_high + circuit_builder.assert_ux_v2( + || "rd_high_range", + rd_high.expr(), + PC_BITS - UInt::::LIMB_BITS, + )?; + let rd_uint = UInt::from_exprs_unchecked(vec![rd_low.expr(), rd_high.expr()]); + + let jump_pc_addr = MemAddr::construct_with_max_bits(circuit_builder, 0, PC_BITS)?; + + // Registers + let rs1 = + ReadRS1::construct_circuit(circuit_builder, rs1_read.register_expr(), vm_state.ts)?; + let rd = WriteRD::construct_circuit(circuit_builder, rd_uint.register_expr(), vm_state.ts)?; + + // Fetch the instruction. + circuit_builder.lk_fetch(&InsnRecord::new( + vm_state.pc.expr(), + InsnKind::JALR.into(), + Some(rd.id.expr()), + rs1.id.expr(), + 0.into(), + imm.expr(), + imm_sign.expr(), + ))?; + + let i_insn = IInstructionConfig { vm_state, rs1, rd }; + + // Next pc is obtained by rounding rs1+imm down to an even value. + // To implement this, check three conditions: + // 1. rs1 + imm = jump_pc_addr + overflow*2^32 + // 3. next_pc = jump_pc_addr aligned to even value (round down) + + let inv = E::BaseField::from_canonical_u32(1 << UInt::::LIMB_BITS).inverse(); + + let carry = (rs1_read.expr()[0].expr() + imm.expr() + - jump_pc_addr.uint_unaligned().expr()[0].expr()) + * inv.expr(); + circuit_builder.assert_bit(|| "carry_lo_bit", carry.expr())?; + + let imm_extend_limb = imm_sign.expr() + * E::BaseField::from_canonical_u32((1 << UInt::::LIMB_BITS) - 1).expr(); + let carry = (rs1_read.expr()[1].expr() + imm_extend_limb.expr() + carry + - jump_pc_addr.uint_unaligned().expr()[1].expr()) + * inv.expr(); + circuit_builder.assert_bit(|| "overflow_bit", carry)?; + + circuit_builder.require_equal( + || "jump_pc_addr = next_pc", + jump_pc_addr.expr_align2(), + i_insn.vm_state.next_pc.unwrap().expr(), + )?; + + // write pc+4 to rd + circuit_builder.require_equal( + || "rd_written = pc+4", + rd_uint.value(), // this operation is safe + i_insn.vm_state.pc.expr() + PC_STEP_SIZE, + )?; + + Ok(JalrConfig { + i_insn, + rs1_read, + imm, + imm_sign, + jump_pc_addr, + rd_high, + }) + } + + fn assign_instance( + config: &Self::InstructionConfig, + instance: &mut [E::BaseField], + lk_multiplicity: &mut LkMultiplicity, + step: &ceno_emul::StepRecord, + ) -> Result<(), ZKVMError> { + let insn = step.insn(); + + let rs1 = step.rs1().unwrap().value; + let imm = InsnRecord::::imm_internal(&insn); + set_val!(instance, config.imm, imm.1); + // according to riscvim32 spec, imm always do signed extension + let imm_sign_extend = imm_sign_extend(true, step.insn().imm as i16); + set_val!( + instance, + config.imm_sign, + E::BaseField::from_bool(imm_sign_extend[1] > 0) + ); + let rd = Value::new_unchecked(step.rd().unwrap().value.after); + let rd_limb = rd.as_u16_limbs(); + lk_multiplicity.assert_ux_v2(rd_limb[0] as u64, 16); + lk_multiplicity.assert_ux_v2(rd_limb[1] as u64, PC_BITS - 16); + + config + .rs1_read + .assign_value(instance, Value::new_unchecked(rs1)); + set_val!( + instance, + config.rd_high, + E::BaseField::from_canonical_u16(rd_limb[1]) + ); + + let (sum, _) = rs1.overflowing_add_signed(i32::from_ne_bytes([ + imm_sign_extend[0] as u8, + (imm_sign_extend[0] >> 8) as u8, + imm_sign_extend[1] as u8, + (imm_sign_extend[1] >> 8) as u8, + ])); + config + .jump_pc_addr + .assign_instance(instance, lk_multiplicity, sum)?; + + config + .i_insn + .assign_instance(instance, lk_multiplicity, step)?; + + Ok(()) + } +} diff --git a/ceno_zkvm/src/instructions/riscv/jump/test.rs b/ceno_zkvm/src/instructions/riscv/jump/test.rs index 5a7036ab7..0b379f250 100644 --- a/ceno_zkvm/src/instructions/riscv/jump/test.rs +++ b/ceno_zkvm/src/instructions/riscv/jump/test.rs @@ -1,37 +1,46 @@ -use ceno_emul::{ByteAddr, Change, InsnKind, PC_STEP_SIZE, StepRecord, Word, encode_rv32}; -use ff_ext::GoldilocksExt2; - +use super::{JalInstruction, JalrInstruction}; use crate::{ + Value, circuit_builder::{CircuitBuilder, ConstraintSystem}, - instructions::Instruction, + instructions::{Instruction, riscv::constants::UInt}, scheme::mock_prover::{MOCK_PC_START, MockProver}, structs::ProgramParams, }; - -use super::{JalInstruction, JalrInstruction}; +use ceno_emul::{ByteAddr, Change, InsnKind, PC_STEP_SIZE, StepRecord, Word, encode_rv32}; +#[cfg(feature = "u16limb_circuit")] +use ff_ext::BabyBearExt4; +use ff_ext::{ExtensionField, GoldilocksExt2}; +use gkr_iop::circuit_builder::DebugIndex; #[test] fn test_opcode_jal() { - let mut cs = ConstraintSystem::::new(|| "riscv"); + verify_test_opcode_jal::(-8); + verify_test_opcode_jal::(8); + + #[cfg(feature = "u16limb_circuit")] + { + verify_test_opcode_jal::(-8); + verify_test_opcode_jal::(8); + } +} + +fn verify_test_opcode_jal(pc_offset: i32) { + let mut cs = ConstraintSystem::::new(|| "riscv"); let mut cb = CircuitBuilder::new(&mut cs); let config = cb .namespace( || "jal", |cb| { - let config = JalInstruction::::construct_circuit( - cb, - &ProgramParams::default(), - ); + let config = JalInstruction::::construct_circuit(cb, &ProgramParams::default()); Ok(config) }, ) .unwrap() .unwrap(); - let pc_offset: i32 = -8i32; let new_pc: ByteAddr = ByteAddr(MOCK_PC_START.0.wrapping_add_signed(pc_offset)); let insn_code = encode_rv32(InsnKind::JAL, 0, 0, 4, pc_offset); - let (raw_witin, lkm) = JalInstruction::::assign_instances( + let (raw_witin, lkm) = JalInstruction::::assign_instances( &config, cb.cs.num_witin as usize, cb.cs.num_structural_witin as usize, @@ -45,33 +54,68 @@ fn test_opcode_jal() { ) .unwrap(); + // verify rd_written + let expected_rd_written = UInt::from_const_unchecked( + Value::new_unchecked(MOCK_PC_START.0 + PC_STEP_SIZE as u32) + .as_u16_limbs() + .to_vec(), + ); + let rd_written_expr = cb.get_debug_expr(DebugIndex::RdWrite as usize)[0].clone(); + cb.require_equal( + || "assert_rd_written", + rd_written_expr, + expected_rd_written.value(), + ) + .unwrap(); + MockProver::assert_satisfied_raw(&cb, raw_witin, &[insn_code], None, Some(lkm)); } #[test] fn test_opcode_jalr() { - let mut cs = ConstraintSystem::::new(|| "riscv"); + verify_test_opcode_jalr::(100, 3); + verify_test_opcode_jalr::(100, -3); + + #[cfg(feature = "u16limb_circuit")] + { + verify_test_opcode_jalr::(100, 3); + verify_test_opcode_jalr::(100, -3); + } +} + +fn verify_test_opcode_jalr(rs1_read: Word, imm: i32) { + let mut cs = ConstraintSystem::::new(|| "riscv"); let mut cb = CircuitBuilder::new(&mut cs); let config = cb .namespace( || "jalr", |cb| { - let config = JalrInstruction::::construct_circuit( - cb, - &ProgramParams::default(), - ); + let config = JalrInstruction::::construct_circuit(cb, &ProgramParams::default()); Ok(config) }, ) .unwrap() .unwrap(); - let imm = -15i32; - let rs1_read: Word = 100u32; + // trim lower bit to 0 let new_pc: ByteAddr = ByteAddr(rs1_read.wrapping_add_signed(imm) & (!1)); let insn_code = encode_rv32(InsnKind::JALR, 2, 0, 4, imm); - let (raw_witin, lkm) = JalrInstruction::::assign_instances( + // verify rd_written + let expected_rd_written = UInt::from_const_unchecked( + Value::new_unchecked(MOCK_PC_START.0 + PC_STEP_SIZE as u32) + .as_u16_limbs() + .to_vec(), + ); + let rd_written_expr = cb.get_debug_expr(DebugIndex::RdWrite as usize)[0].clone(); + cb.require_equal( + || "assert_rd_written", + rd_written_expr, + expected_rd_written.value(), + ) + .unwrap(); + + let (raw_witin, lkm) = JalrInstruction::::assign_instances( &config, cb.cs.num_witin as usize, cb.cs.num_structural_witin as usize, diff --git a/ceno_zkvm/src/tables/program.rs b/ceno_zkvm/src/tables/program.rs index 305ec9765..092c4b560 100644 --- a/ceno_zkvm/src/tables/program.rs +++ b/ceno_zkvm/src/tables/program.rs @@ -133,8 +133,10 @@ impl InsnRecord { (insn.imm as u32 >> 12) as i64, F::from_wrapped_u32(insn.imm as u32 >> 12), ), - // TODO JALR need to connecting register (2 limb) with pc (1 limb) - (JALR, _) => (insn.imm as i64, i64_to_base(insn.imm as i64)), + (JALR, _) => ( + insn.imm as i16 as i64, + F::from_canonical_u16(insn.imm as i16 as u16), + ), // for default imm to operate with register value _ => ( insn.imm as i16 as i64, @@ -158,8 +160,6 @@ impl InsnRecord { // in particular imm operated with program counter // encode as field element, which do not need extra sign extension of imm (_, B | J) => (false as i64, F::from_bool(false)), - // TODO JALR need to connecting register (2 limb) with pc (1 limb) - (JALR, _) => (false as i64, F::from_bool(false)), // Signed views _ => ((insn.imm < 0) as i64, F::from_bool(insn.imm < 0)), } diff --git a/gkr_iop/src/circuit_builder.rs b/gkr_iop/src/circuit_builder.rs index 7fd7cf1b9..8ce6f9b7c 100644 --- a/gkr_iop/src/circuit_builder.rs +++ b/gkr_iop/src/circuit_builder.rs @@ -786,6 +786,26 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> { } } + /// to replace `assert_ux` + pub fn assert_ux_v2( + &mut self, + name_fn: N, + expr: Expression, + max_bits: usize, + ) -> Result<(), CircuitBuilderError> + where + NR: Into, + N: FnOnce() -> NR, + { + match max_bits { + 16 => self.assert_u16(name_fn, expr), + 14 => self.assert_u14(name_fn, expr), + 8 => self.assert_byte(name_fn, expr), + 5 => self.assert_u5(name_fn, expr), + c => panic!("Unsupported bit range {c}"), + } + } + /// Generates U16 lookups to prove that `value` fits on `size < 16` bits. /// In general it can be done by two U16 checks: one for `value` and one for /// `value << (16 - size)`. diff --git a/gkr_iop/src/utils/lk_multiplicity.rs b/gkr_iop/src/utils/lk_multiplicity.rs index ccbe5246f..091e857b6 100644 --- a/gkr_iop/src/utils/lk_multiplicity.rs +++ b/gkr_iop/src/utils/lk_multiplicity.rs @@ -202,6 +202,20 @@ impl LkMultiplicity { } } + #[inline(always)] + pub fn assert_ux_v2(&mut self, v: u64, max_bits: usize) { + self.increment( + match max_bits { + 16 => LookupTable::U16, + 14 => LookupTable::U14, + 8 => LookupTable::U8, + 5 => LookupTable::U5, + _ => panic!("Unsupported bit range"), + }, + v, + ); + } + /// Track a lookup into a logic table (AndTable, etc). pub fn logic_u8(&mut self, a: u64, b: u64) { self.increment(OP::ROM_TYPE, OP::pack(a, b));