From 80c15fa53dc635321ce95ff8ec2e88d53aa0b80d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A9lien=20Nicolas?= Date: Thu, 31 Oct 2024 15:36:10 +0100 Subject: [PATCH] rename-internal --- ceno_emul/src/rv32im.rs | 9 ++++---- ceno_zkvm/src/instructions/riscv/arith_imm.rs | 2 +- ceno_zkvm/src/instructions/riscv/b_insn.rs | 2 +- .../src/instructions/riscv/jump/auipc.rs | 2 +- ceno_zkvm/src/instructions/riscv/jump/jalr.rs | 4 ++-- .../riscv/logic_imm/logic_imm_circuit.rs | 4 ++-- .../src/instructions/riscv/memory/load.rs | 4 ++-- .../src/instructions/riscv/memory/store.rs | 4 ++-- ceno_zkvm/src/instructions/riscv/shift_imm.rs | 2 +- ceno_zkvm/src/instructions/riscv/slti.rs | 4 ++-- ceno_zkvm/src/tables/program.rs | 23 +++++++++---------- 11 files changed, 30 insertions(+), 30 deletions(-) diff --git a/ceno_emul/src/rv32im.rs b/ceno_emul/src/rv32im.rs index 490248436..41fdb7576 100644 --- a/ceno_emul/src/rv32im.rs +++ b/ceno_emul/src/rv32im.rs @@ -271,8 +271,8 @@ impl DecodedInstruction { } } - /// Get the decoded immediate, or 2^shift, or the funct7 field, depending on the instruction format. - pub fn imm_or_funct7(&self) -> u32 { + /// The internal view of the immediate, for use in circuits. + pub fn imm_internal(&self) -> u32 { match self.codes().format { R => self.func7, I => match self.codes().kind { @@ -287,12 +287,13 @@ impl DecodedInstruction { } } + /// The internal interpretation of the immediate sign, for use in circuits. /// Indicates if the immediate value, when signed, needs to be encoded as field negative. /// example: /// imm = ux::MAX - 1 implies /// imm_field = FIELD_MODULUS - 1 if imm_field_is_negative /// imm_field = ux::MAX - 1 otherwise - /// see InsnRecord::imm_or_funct7_field + /// see InsnRecord::imm_internal_field pub fn imm_field_is_negative(&self) -> bool { match self.codes() { InsnCodes { format: R | U, .. } => false, @@ -364,7 +365,7 @@ fn test_decode_imm() { 0x20, ), ] { - let imm = DecodedInstruction::new(i).imm_or_funct7(); + let imm = DecodedInstruction::new(i).imm_internal(); assert_eq!(imm, expected); } } diff --git a/ceno_zkvm/src/instructions/riscv/arith_imm.rs b/ceno_zkvm/src/instructions/riscv/arith_imm.rs index c8e464719..3831791f4 100644 --- a/ceno_zkvm/src/instructions/riscv/arith_imm.rs +++ b/ceno_zkvm/src/instructions/riscv/arith_imm.rs @@ -62,7 +62,7 @@ impl Instruction for AddiInstruction { step: &StepRecord, ) -> Result<(), ZKVMError> { let rs1_read = Value::new_unchecked(step.rs1().unwrap().value); - let imm = Value::new(step.insn().imm_or_funct7(), lk_multiplicity); + let imm = Value::new(step.insn().imm_internal(), lk_multiplicity); let result = rs1_read.add(&imm, lk_multiplicity, true); diff --git a/ceno_zkvm/src/instructions/riscv/b_insn.rs b/ceno_zkvm/src/instructions/riscv/b_insn.rs index 2edd1e5b6..e73ad0f4e 100644 --- a/ceno_zkvm/src/instructions/riscv/b_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/b_insn.rs @@ -100,7 +100,7 @@ impl BInstructionConfig { set_val!( instance, self.imm, - InsnRecord::imm_or_funct7_field::(&step.insn()) + InsnRecord::imm_internal_field::(&step.insn()) ); // Fetch the instruction. diff --git a/ceno_zkvm/src/instructions/riscv/jump/auipc.rs b/ceno_zkvm/src/instructions/riscv/jump/auipc.rs index 7d20430b7..67e123497 100644 --- a/ceno_zkvm/src/instructions/riscv/jump/auipc.rs +++ b/ceno_zkvm/src/instructions/riscv/jump/auipc.rs @@ -74,7 +74,7 @@ impl Instruction for AuipcInstruction { step: &ceno_emul::StepRecord, ) -> Result<(), ZKVMError> { let pc: u32 = step.pc().before.0; - let imm: u32 = step.insn().imm_or_funct7(); + let imm: u32 = step.insn().imm_internal(); let (sum, overflow) = pc.overflowing_add(imm); set_val!(instance, config.imm, imm as u64); diff --git a/ceno_zkvm/src/instructions/riscv/jump/jalr.rs b/ceno_zkvm/src/instructions/riscv/jump/jalr.rs index 39ee50458..425b334e3 100644 --- a/ceno_zkvm/src/instructions/riscv/jump/jalr.rs +++ b/ceno_zkvm/src/instructions/riscv/jump/jalr.rs @@ -116,7 +116,7 @@ impl Instruction for JalrInstruction { let insn = step.insn(); let rs1 = step.rs1().unwrap().value; - let imm: i32 = insn.imm_or_funct7() as i32; + let imm: i32 = insn.imm_internal() as i32; let rd = step.rd().unwrap().value.after; let (sum, overflowing) = rs1.overflowing_add_signed(imm); @@ -128,7 +128,7 @@ impl Instruction for JalrInstruction { .rd_written .assign_value(instance, Value::new(rd, lk_multiplicity)); - let imm_field = InsnRecord::imm_or_funct7_field::(&insn); + let imm_field = InsnRecord::imm_internal_field::(&insn); set_val!(instance, config.imm, imm_field); config diff --git a/ceno_zkvm/src/instructions/riscv/logic_imm/logic_imm_circuit.rs b/ceno_zkvm/src/instructions/riscv/logic_imm/logic_imm_circuit.rs index 7fb061b5c..c423bda0a 100644 --- a/ceno_zkvm/src/instructions/riscv/logic_imm/logic_imm_circuit.rs +++ b/ceno_zkvm/src/instructions/riscv/logic_imm/logic_imm_circuit.rs @@ -57,7 +57,7 @@ impl Instruction for LogicInstruction { UInt8::::logic_assign::( lkm, step.rs1().unwrap().value.into(), - step.insn().imm_or_funct7().into(), + step.insn().imm_internal().into(), ); config.assign_instance(instance, lkm, step) @@ -112,7 +112,7 @@ impl LogicConfig { let rs1_read = split_to_u8(step.rs1().unwrap().value); self.rs1_read.assign_limbs(instance, &rs1_read); - let imm = split_to_u8::(step.insn().imm_or_funct7()); + let imm = split_to_u8::(step.insn().imm_internal()); self.imm.assign_limbs(instance, &imm); let rd_written = split_to_u8(step.rd().unwrap().value.after); diff --git a/ceno_zkvm/src/instructions/riscv/memory/load.rs b/ceno_zkvm/src/instructions/riscv/memory/load.rs index 1bc76f311..36b8d33b2 100644 --- a/ceno_zkvm/src/instructions/riscv/memory/load.rs +++ b/ceno_zkvm/src/instructions/riscv/memory/load.rs @@ -205,12 +205,12 @@ impl Instruction for LoadInstruction> 1) & 0x01]; diff --git a/ceno_zkvm/src/instructions/riscv/memory/store.rs b/ceno_zkvm/src/instructions/riscv/memory/store.rs index 878777de6..c76be7362 100644 --- a/ceno_zkvm/src/instructions/riscv/memory/store.rs +++ b/ceno_zkvm/src/instructions/riscv/memory/store.rs @@ -142,14 +142,14 @@ impl Instruction let rs1 = Value::new_unchecked(step.rs1().unwrap().value); let rs2 = Value::new_unchecked(step.rs2().unwrap().value); let memory_op = step.memory_op().unwrap(); - let imm: E::BaseField = InsnRecord::imm_or_funct7_field(&step.insn()); + let imm: E::BaseField = InsnRecord::imm_internal_field(&step.insn()); let prev_mem_value = Value::new(memory_op.value.before, lk_multiplicity); let addr = ByteAddr::from( step.rs1() .unwrap() .value - .wrapping_add(step.insn().imm_or_funct7()), + .wrapping_add(step.insn().imm_internal()), ); config .s_insn diff --git a/ceno_zkvm/src/instructions/riscv/shift_imm.rs b/ceno_zkvm/src/instructions/riscv/shift_imm.rs index 1f43da85c..4a27d285b 100644 --- a/ceno_zkvm/src/instructions/riscv/shift_imm.rs +++ b/ceno_zkvm/src/instructions/riscv/shift_imm.rs @@ -136,7 +136,7 @@ impl Instruction for ShiftImmInstructio lk_multiplicity: &mut LkMultiplicity, step: &StepRecord, ) -> Result<(), ZKVMError> { - let imm = step.insn().imm_or_funct7(); + let imm = step.insn().imm_internal(); let rs1_read = Value::new_unchecked(step.rs1().unwrap().value); let rd_written = Value::new(step.rd().unwrap().value.after, lk_multiplicity); diff --git a/ceno_zkvm/src/instructions/riscv/slti.rs b/ceno_zkvm/src/instructions/riscv/slti.rs index cc80d629b..3e77fa9d0 100644 --- a/ceno_zkvm/src/instructions/riscv/slti.rs +++ b/ceno_zkvm/src/instructions/riscv/slti.rs @@ -114,8 +114,8 @@ impl Instruction for SetLessThanImmInst .rs1_read .assign_value(instance, Value::new_unchecked(rs1)); - let imm = step.insn().imm_or_funct7(); - let imm_field = InsnRecord::imm_or_funct7_field::(&step.insn()); + let imm = step.insn().imm_internal(); + let imm_field = InsnRecord::imm_internal_field::(&step.insn()); set_val!(instance, config.imm, imm_field); match I::INST_KIND { diff --git a/ceno_zkvm/src/tables/program.rs b/ceno_zkvm/src/tables/program.rs index 13291aa88..2df3ec66e 100644 --- a/ceno_zkvm/src/tables/program.rs +++ b/ceno_zkvm/src/tables/program.rs @@ -34,8 +34,8 @@ macro_rules! declare_program { pub struct InsnRecord([T; 7]); impl InsnRecord { - pub fn new(pc: T, opcode: T, rd: T, funct3: T, rs1: T, rs2: T, imm_or_funct7: T) -> Self { - InsnRecord([pc, opcode, rd, funct3, rs1, rs2, imm_or_funct7]) + pub fn new(pc: T, opcode: T, rd: T, funct3: T, rs1: T, rs2: T, imm_internal: T) -> Self { + InsnRecord([pc, opcode, rd, funct3, rs1, rs2, imm_internal]) } pub fn as_slice(&self) -> &[T] { @@ -71,9 +71,8 @@ impl InsnRecord { &self.0[0..6] } - /// The complete immediate value, for instruction types I/S/B/U/J. - /// Otherwise, the field funct7 of R-Type instructions. - pub fn imm_or_funct7(&self) -> &T { + /// The internal view of the immediate. See `DecodedInstruction::imm_internal`. + pub fn imm_internal(&self) -> &T { &self.0[6] } } @@ -87,17 +86,17 @@ impl InsnRecord { insn.funct3_or_zero(), insn.rs1_or_zero(), insn.rs2_or_zero(), - insn.imm_or_funct7(), + insn.imm_internal(), ) } /// Interpret the immediate or funct7 as unsigned or signed depending on the instruction. /// Convert negative values from two's complement to field. - pub fn imm_or_funct7_field(insn: &DecodedInstruction) -> F { + pub fn imm_internal_field(insn: &DecodedInstruction) -> F { if insn.imm_field_is_negative() { - -F::from(-(insn.imm_or_funct7() as i32) as u64) + -F::from(-(insn.imm_internal() as i32) as u64) } else { - F::from(insn.imm_or_funct7() as u64) + F::from(insn.imm_internal() as u64) } } } @@ -132,7 +131,7 @@ impl TableCircuit cb.create_fixed(|| "funct3")?, cb.create_fixed(|| "rs1")?, cb.create_fixed(|| "rs2")?, - cb.create_fixed(|| "imm_or_funct7")?, + cb.create_fixed(|| "imm_internal")?, ]); let mlt = cb.create_witin(|| "mlt"); @@ -179,8 +178,8 @@ impl TableCircuit set_fixed_val!( row, - config.record.imm_or_funct7(), - InsnRecord::imm_or_funct7_field(&insn) + config.record.imm_internal(), + InsnRecord::imm_internal_field(&insn) ); });