add/sub -> rtype gadget to build circuit #230
Conversation
hero78119
force-pushed
the
feat/r_type_gadget
branch
from
1c930da to
f90b039
Compare
ceno_emul/src/rv32im.rs
Outdated
| let isa_idx = self.table[Self::map10(decoded.opcode, decoded.func3, decoded.func7)]; | ||
| RV32IM_ISA[isa_idx as usize] | ||
| } | ||
|
|
||
| pub const fn lookup_raw(&self, opcode: u32, func3: u32, func7: u32) -> FastDecodeEntry { |
There was a problem hiding this comment.
I think we can leverage InsnKind directly and then we don't need to assign opcode, func3 and func7.
There was a problem hiding this comment.
you are right! I force-push to update it with more simplify design 👍
hero78119
force-pushed
the
feat/r_type_gadget
branch
from
f90b039 to
9544596
Compare
hero78119
force-pushed
the
feat/r_type_gadget
branch
from
9544596 to
0bba26f
Compare
|
I’ve doing something related over here: #231 |
| pub lt_rs1_cfg: ExprLtConfig, | ||
| pub lt_rs2_cfg: ExprLtConfig, | ||
| pub lt_prev_ts_cfg: ExprLtConfig, | ||
| phantom: PhantomData<E>, |
| @@ -282,7 +282,7 @@ const fn insn( | |||
| type InstructionTable = [FastDecodeEntry; 48]; | |||
| type FastInstructionTable = [u8; 1 << 10]; | |||
|
|
|||
| const RV32IM_ISA: InstructionTable = [ | |||
| pub const RV32IM_ISA: InstructionTable = [ | |||
There was a problem hiding this comment.
There could be a pub fn getter and keep details of the table private.
|
|
||
| #[derive(Debug)] | ||
| pub struct RTypeInstructionConfig<E: ExtensionField> { | ||
| pub pc: WitIn, |
There was a problem hiding this comment.
Such a complex type should have private fields. Only the 3 operands are needed outside, and they could be exposed by pub fn methods or passed as arguments to operands_fn.
| @@ -7,10 +7,12 @@ pub mod addsub; | |||
| pub mod blt; | |||
| pub mod config; | |||
| pub mod constants; | |||
| mod gadgets; | |||
There was a problem hiding this comment.
This could have a specific name such as r_insn.
| pub lt_rs2_cfg: ExprLtConfig, | ||
| pub lt_prev_ts_cfg: ExprLtConfig, | ||
| phantom: PhantomData<E>, | ||
| pub struct InstructionConfig<E: ExtensionField>(RTypeInstructionConfig<E>); |
There was a problem hiding this comment.
This type does not really bring anything, it could be type InstructionConfig = RTypeInstructionConfig directly.
| instance: &mut [MaybeUninit<E::BaseField>], | ||
| lk_multiplicity: &mut LkMultiplicity, | ||
| step: &StepRecord, | ||
| operands_fn: impl FnOnce( |
There was a problem hiding this comment.
I think this function should be symmetrical with the one in construct_circuit. Here it is strange that this function is given the whole config, and implicitly it must assign some fields and not some others from the config.
Instead, we say specifically that the inheriting circuit (e.g. Add) is responsible for the operands. In construct_circuit it allocates them, and in assign it assigns them. This responsibility can be made explicit by passing back the operands that it created and not the rest.
operands_fn: impl FnOnce(
&RegUInt<E>, // operand_1
&RegUInt<E>, // operand_2
&RegUInt<E>, // operand_out
&mut [MaybeUninit<E::BaseField>],
&mut LkMultiplicity,
&StepRecord,
) -> Result<(), ZKVMError>,There was a problem hiding this comment.
Alternatively, there is the composition style (see #231), where the operands stay in the specific type that owns them and not in the gadget.
| lk_multiplicity.fetch(step.pc().before.0); | ||
| set_val!(instance, config.pc, step.pc().before.0 as u64); | ||
| set_val!(instance, config.ts, step.cycle()); | ||
| let addend_1 = UIntValue::new_unchecked(step.rs2().unwrap().value); |
There was a problem hiding this comment.
Leave the operand responsibility to the caller (operand_fn).
This PR aiming for
ceno_emulrelated to #219 and #228