From 75476fbc7ba730c767c585c217ecb4261efa806a Mon Sep 17 00:00:00 2001 From: Zhang Junyu Date: Mon, 1 Jul 2024 09:52:32 +0000 Subject: [PATCH 1/2] mtable: fix constraint of termination --- crates/zkwasm/src/circuits/mtable/assign.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/crates/zkwasm/src/circuits/mtable/assign.rs b/crates/zkwasm/src/circuits/mtable/assign.rs index 227762b10..a20f70ef1 100644 --- a/crates/zkwasm/src/circuits/mtable/assign.rs +++ b/crates/zkwasm/src/circuits/mtable/assign.rs @@ -31,7 +31,7 @@ impl MemoryTableChip { fn assign_fixed(&self, ctx: &mut Context<'_, F>) -> Result<(), Error> { let capability = self.maximal_available_rows / MEMORY_TABLE_ENTRY_ROWS as usize; - for _ in 0..capability { + for i in 0..capability { ctx.region.assign_fixed( || "mtable: sel", self.config.entry_sel, @@ -39,6 +39,15 @@ impl MemoryTableChip { || Ok(F::one()), )?; + if i == capability - 1 { + ctx.region.assign_advice_from_constant( + || "rest_mops terminate", + self.config.rest_mops_cell.cell.col, + ctx.offset + self.config.rest_mops_cell.cell.rot as usize, + F::zero(), + )?; + } + ctx.step(MEMORY_TABLE_ENTRY_ROWS as usize); } From ad008ea20b73ba7a1d85fb4962c7e3ad54aa69c3 Mon Sep 17 00:00:00 2001 From: Zhang Junyu Date: Tue, 2 Jul 2024 05:51:20 +0000 Subject: [PATCH 2/2] rename frame table lookup api --- crates/zkwasm/src/circuits/bit_table/mod.rs | 2 +- crates/zkwasm/src/circuits/etable/mod.rs | 48 +++++++------------ .../zkwasm/src/circuits/jtable/configure.rs | 2 +- .../circuits/post_image_table/continuation.rs | 2 +- 4 files changed, 19 insertions(+), 35 deletions(-) diff --git a/crates/zkwasm/src/circuits/bit_table/mod.rs b/crates/zkwasm/src/circuits/bit_table/mod.rs index fc27abbfe..fe0769765 100644 --- a/crates/zkwasm/src/circuits/bit_table/mod.rs +++ b/crates/zkwasm/src/circuits/bit_table/mod.rs @@ -56,7 +56,7 @@ pub struct BitTableConfig { _mark: PhantomData, } -pub(in crate::circuits) const STEP_SIZE: usize = 11; +pub(self) const STEP_SIZE: usize = 11; pub(self) const BLOCK_SEL_OFFSET: usize = 1; pub(self) const U32_OFFSET: [usize; 2] = [1, 6]; pub(self) const U8_OFFSET: [usize; 8] = [2, 3, 4, 5, 7, 8, 9, 10]; diff --git a/crates/zkwasm/src/circuits/etable/mod.rs b/crates/zkwasm/src/circuits/etable/mod.rs index 1ce6ccccc..9da93b9fa 100644 --- a/crates/zkwasm/src/circuits/etable/mod.rs +++ b/crates/zkwasm/src/circuits/etable/mod.rs @@ -444,25 +444,21 @@ impl EventTableConfig { * 1. constrains the relation between the last step and termination. * 2. ignores rows following the termination step. */ - let sum_ops_expr_with_init = - |init: Expression, - meta: &mut VirtualCells<'_, F>, - get_expr: &dyn Fn( - &mut VirtualCells<'_, F>, - &OpcodeConfig, - ) -> Option>, - enable: Option<&dyn Fn(&mut VirtualCells<'_, F>) -> Expression>| { - let expr = op_bitmaps - .iter() - .filter_map(|(op, op_index)| { - get_expr(meta, op_configs.get(op).unwrap()) - .map(|expr| expr * ops[*op_index].curr_expr(meta)) - }) - .fold(init, |acc, x| acc + x) - * fixed_curr!(meta, step_sel); - - enable.map_or(expr.clone(), |enable_expr| expr * enable_expr(meta)) - }; + let sum_ops_expr_with_init = |init: Expression, + meta: &mut VirtualCells<'_, F>, + get_expr: &dyn Fn( + &mut VirtualCells<'_, F>, + &OpcodeConfig, + ) -> Option>| { + op_bitmaps + .iter() + .filter_map(|(op, op_index)| { + get_expr(meta, op_configs.get(op).unwrap()) + .map(|expr| expr * ops[*op_index].curr_expr(meta)) + }) + .fold(init, |acc, x| acc + x) + * fixed_curr!(meta, step_sel) + }; let sum_ops_expr = |meta: &mut VirtualCells<'_, F>, get_expr: &dyn Fn( @@ -484,7 +480,6 @@ impl EventTableConfig { rest_mops_cell.next_expr(meta) - rest_mops_cell.curr_expr(meta), meta, &|meta, config: &OpcodeConfig| config.0.mops(meta), - None, )] }); @@ -494,13 +489,11 @@ impl EventTableConfig { rest_call_ops_cell.next_expr(meta) - rest_call_ops_cell.curr_expr(meta), meta, &|meta, config: &OpcodeConfig| config.0.call_ops_expr(meta), - None, ), sum_ops_expr_with_init( rest_return_ops_cell.next_expr(meta) - rest_return_ops_cell.curr_expr(meta), meta, &|meta, config: &OpcodeConfig| config.0.return_ops_expr(meta), - None, ), ] }); @@ -512,7 +505,6 @@ impl EventTableConfig { &|meta, config: &OpcodeConfig| { config.0.input_index_increase(meta, &common_config) }, - None, )] }); @@ -526,7 +518,6 @@ impl EventTableConfig { .0 .external_host_call_index_increase(meta, &common_config) }, - None, )] }); @@ -535,7 +526,6 @@ impl EventTableConfig { sp_cell.curr_expr(meta) - sp_cell.next_expr(meta), meta, &|meta, config: &OpcodeConfig| config.0.sp_diff(meta), - None, )] }); @@ -544,7 +534,6 @@ impl EventTableConfig { mpages_cell.curr_expr(meta) - mpages_cell.next_expr(meta), meta, &|meta, config: &OpcodeConfig| config.0.allocated_memory_pages_diff(meta), - None, )] }); @@ -555,7 +544,6 @@ impl EventTableConfig { &|meta, config: &OpcodeConfig| { config.0.context_input_index_increase(meta, &common_config) }, - None, )] }); @@ -567,7 +555,6 @@ impl EventTableConfig { &|meta, config: &OpcodeConfig| { config.0.context_output_index_increase(meta, &common_config) }, - None, )] }); @@ -590,7 +577,6 @@ impl EventTableConfig { .next_fid(meta, &common_config) .map(|x| x - fid_cell.curr_expr(meta)) }, - None, )] }); @@ -604,7 +590,6 @@ impl EventTableConfig { .next_iid(meta, &common_config) .map(|x| iid_cell.curr_expr(meta) + enabled_cell.curr_expr(meta) - x) }, - None, )] }); @@ -618,7 +603,6 @@ impl EventTableConfig { .next_frame_id(meta, &common_config) .map(|x| x - frame_id_cell.curr_expr(meta)) }, - None, )] }); @@ -641,7 +625,7 @@ impl EventTableConfig { brtable_lookup_cell.curr_expr(meta) * fixed_curr!(meta, step_sel) }); - jtable.configure_in_event_table(meta, "c8c. jtable_lookup in jtable", |meta| { + jtable.configure_lookup_in_frame_table(meta, "c8c. jtable_lookup in jtable", |meta| { ( fixed_curr!(meta, step_sel), common_config.is_returned_cell.curr_expr(meta) * fixed_curr!(meta, step_sel), diff --git a/crates/zkwasm/src/circuits/jtable/configure.rs b/crates/zkwasm/src/circuits/jtable/configure.rs index 89ed1e882..fb7d463b7 100644 --- a/crates/zkwasm/src/circuits/jtable/configure.rs +++ b/crates/zkwasm/src/circuits/jtable/configure.rs @@ -89,7 +89,7 @@ impl JTableConstraint for JumpTableConfig { impl JumpTableConfig { /// Frame Table Constraint 4. Etable step's call/return record can be found on jtable_entry - pub(in crate::circuits) fn configure_in_event_table( + pub(in crate::circuits) fn configure_lookup_in_frame_table( &self, meta: &mut ConstraintSystem, key: &'static str, diff --git a/crates/zkwasm/src/circuits/post_image_table/continuation.rs b/crates/zkwasm/src/circuits/post_image_table/continuation.rs index a8c139677..f2a4177dc 100644 --- a/crates/zkwasm/src/circuits/post_image_table/continuation.rs +++ b/crates/zkwasm/src/circuits/post_image_table/continuation.rs @@ -152,7 +152,7 @@ impl PostImageTableConfig { |meta| curr!(meta, memory_finalized_lookup_encode), ); - frame_table.configure_in_event_table( + frame_table.configure_lookup_in_frame_table( meta, "post image table: extract unreturned frame table entries", |meta| {