Skip to content
This repository has been archived by the owner on Jul 5, 2024. It is now read-only.

Commit

Permalink
Padding step in RwMap
Browse files Browse the repository at this point in the history
  • Loading branch information
hero78119 committed Oct 6, 2023
1 parent 69680b8 commit dd5c9bb
Show file tree
Hide file tree
Showing 17 changed files with 272 additions and 76 deletions.
70 changes: 45 additions & 25 deletions bus-mapping/src/circuit_input_builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ use self::access::gen_state_access_trace;
use crate::{
error::Error,
evm::opcodes::{gen_associated_ops, gen_associated_steps},
operation::{CallContextField, Operation, RWCounter, StartOp, RW},
operation::{CallContextField, Op, Operation, OperationContainer, RWCounter, RW},
rpc::GethClient,
state_db::{self, CodeDB, StateDB},
};
Expand Down Expand Up @@ -293,11 +293,6 @@ impl CircuitInputBuilder<FixedCParams> {
);
}

let mut push_op = |step: &mut ExecStep, rwc: RWCounter, rw: RW, op: StartOp| {
let op_ref = state.block.container.insert(Operation::new(rwc, rw, op));
step.bus_mapping_instance.push(op_ref);
};

// rwc index start from 1
let total_rws = state.block_ctx.rwc.0 - 1;
// We need at least 1 extra Start row
Expand All @@ -310,27 +305,51 @@ impl CircuitInputBuilder<FixedCParams> {
max_rws
);
}
let (padding_start, padding_end) = (1, max_rws - total_rws); // rw counter start from 1
push_op(
&mut end_block_last,
RWCounter(padding_start),
RW::READ,
StartOp {},
);
if padding_end != padding_start {
push_op(
&mut end_block_last,
RWCounter(padding_end),
RW::READ,
StartOp {},
);
}
// TODO only push StartOp in first chunk
// push_op(
// &mut state.block.container,
// &mut end_block_last,
// RWCounter(1),
// RW::READ,
// StartOp {},
// );
// if max_rws - total_rws > 1 {
// let (padding_start, padding_end) = (max_rws - total_rws, max_rws); // rw counter
// start from 1 push_op(
// &mut state.block.container,
// &mut end_block_last,
// RWCounter(padding_start),
// RW::READ,
// PaddingOp {},
// );
// if padding_end != padding_start {
// push_op(
// &mut state.block.container,
// &mut end_block_last,
// RWCounter(padding_end),
// RW::READ,
// PaddingOp {},
// );
// }
// }

self.block.block_steps.end_block_not_last = end_block_not_last;
self.block.block_steps.end_block_last = end_block_last;
}
}

#[allow(dead_code)]
fn push_op<T: Op>(
container: &mut OperationContainer,
step: &mut ExecStep,
rwc: RWCounter,
rw: RW,
op: T,
) {
let op_ref = container.insert(Operation::new(rwc, rw, op));
step.bus_mapping_instance.push(op_ref);
}

impl<C: CircuitsParams> CircuitInputBuilder<C> {
/// First part of handle_block, common for dynamic and static circuit parameters.
pub fn begin_handle_block(
Expand Down Expand Up @@ -393,11 +412,12 @@ impl CircuitInputBuilder<DynamicCParams> {
* 2
+ 4; // disabled and unused rows.

let total_rws_before_padding: usize =
// TODO fix below logic for multiple rw_table chunks
let total_rws_before_end_block: usize =
<RWCounter as Into<usize>>::into(self.block_ctx.rwc) - 1; // -1 since rwc start from index `1`
let max_rws_after_padding = total_rws_before_padding
+ 1 // fill 1 to have exactly one StartOp padding in below `set_end_block`
+ if total_rws_before_padding > 0 { 1 /*end_block -> CallContextFieldTag::TxId lookup*/ } else { 0 };
let max_rws_after_padding = total_rws_before_end_block
+ 1 // +1 for RW::Start padding in offset 0
+ if total_rws_before_end_block > 0 { 1 /*end_block -> CallContextFieldTag::TxId lookup*/ } else { 0 };
// Computing the number of rows for the EVM circuit requires the size of ExecStep,
// which is determined in the code of zkevm-circuits and cannot be imported here.
// When the evm circuit receives a 0 value it dynamically computes the minimum
Expand Down
1 change: 1 addition & 0 deletions bus-mapping/src/exec_trace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ impl fmt::Debug for OperationRef {
"OperationRef{{ {}, {} }}",
match self.0 {
Target::Start => "Start",
Target::Padding => "Padding",
Target::Memory => "Memory",
Target::Stack => "Stack",
Target::Storage => "Storage",
Expand Down
32 changes: 31 additions & 1 deletion bus-mapping/src/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ impl RWCounter {
/// Enum used to differenciate between EVM Stack, Memory and Storage operations.
#[derive(Debug, Clone, PartialEq, Eq, Copy, EnumIter, Hash)]
pub enum Target {
/// Start is a padding operation.
/// Start operation in the first row
Start = 1,
/// Means the target of the operation is the Memory.
Memory,
Expand All @@ -115,6 +115,8 @@ pub enum Target {
TxReceipt,
/// Means the target of the operation is the TxLog.
TxLog,
/// padding operation.
Padding,
}

impl_expr!(Target);
Expand Down Expand Up @@ -885,6 +887,32 @@ impl Op for StartOp {
}
}

/// Represent a Padding padding operation
#[derive(Clone, PartialEq, Eq, Debug)]
pub struct PaddingOp {}

impl PartialOrd for PaddingOp {
fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
Some(self.cmp(other))
}
}

impl Ord for PaddingOp {
fn cmp(&self, _other: &Self) -> Ordering {
Ordering::Equal
}
}

impl Op for PaddingOp {
fn into_enum(self) -> OpEnum {
OpEnum::Padding(self)
}

fn reverse(&self) -> Self {
unreachable!("Padding can't be reverted")
}
}

/// Represents TxReceipt read/write operation.
#[derive(Clone, PartialEq, Eq)]
pub struct TxReceiptOp {
Expand Down Expand Up @@ -955,6 +983,8 @@ pub enum OpEnum {
TxLog(TxLogOp),
/// Start
Start(StartOp),
/// Start
Padding(PaddingOp),
}

/// Operation is a Wrapper over a type that implements Op with a RWCounter.
Expand Down
13 changes: 10 additions & 3 deletions bus-mapping/src/operation/container.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use super::{
AccountOp, CallContextOp, MemoryOp, Op, OpEnum, Operation, RWCounter, StackOp, StartOp,
StorageOp, Target, TxAccessListAccountOp, TxAccessListAccountStorageOp, TxLogOp, TxReceiptOp,
TxRefundOp, RW,
AccountOp, CallContextOp, MemoryOp, Op, OpEnum, Operation, PaddingOp, RWCounter, StackOp,
StartOp, StorageOp, Target, TxAccessListAccountOp, TxAccessListAccountStorageOp, TxLogOp,
TxReceiptOp, TxRefundOp, RW,
};
use crate::exec_trace::OperationRef;
use itertools::Itertools;
Expand Down Expand Up @@ -44,6 +44,8 @@ pub struct OperationContainer {
pub tx_log: Vec<Operation<TxLogOp>>,
/// Operations of Start
pub start: Vec<Operation<StartOp>>,
/// Operations of Padding
pub padding: Vec<Operation<PaddingOp>>,
}

impl Default for OperationContainer {
Expand All @@ -68,6 +70,7 @@ impl OperationContainer {
tx_receipt: Vec::new(),
tx_log: Vec::new(),
start: Vec::new(),
padding: Vec::new(),
}
}

Expand Down Expand Up @@ -164,6 +167,10 @@ impl OperationContainer {
self.start.push(Operation::new(rwc, rw, op));
OperationRef::from((Target::Start, self.start.len() - 1))
}
OpEnum::Padding(op) => {
self.padding.push(Operation::new(rwc, rw, op));
OperationRef::from((Target::Padding, self.padding.len() - 1))
}
}
}

Expand Down
1 change: 1 addition & 0 deletions circuit-benchmarks/src/state_circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ mod tests {
Fr::from(1),
Fr::from(1),
Fr::from(1),
0,
);

// Initialize the polynomial commitment parameters
Expand Down
1 change: 1 addition & 0 deletions zkevm-circuits/src/copy_circuit/dev.rs
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ impl<F: Field> Circuit<F> for CopyCircuit<F> {
&mut layouter,
&self.external_data.rws.table_assignments(true),
self.external_data.max_rws,
true,
)?;

config
Expand Down
8 changes: 6 additions & 2 deletions zkevm-circuits/src/evm_circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -303,9 +303,10 @@ impl<F: Field> SubCircuit<F> for EvmCircuit<F> {

config.execution.assign_block(layouter, block, challenges)?;

let (rw_rows_padding, _) = RwMap::table_assignments_prepad(
let (rw_rows_padding, _) = RwMap::table_assignments_padding(
&block.rws.table_assignments(true),
block.circuits_params.max_rws,
block.rw_table_chunked_index == 0,
);
let (
(rw_table_row_first, rw_table_row_last),
Expand All @@ -330,6 +331,7 @@ impl<F: Field> SubCircuit<F> for EvmCircuit<F> {
&block.rws.table_assignments(true),
// align with state circuit to padding to same max_rws
block.circuits_params.max_rws,
block.rw_table_chunked_index == 0,
)?;
let permutation_cells = config.rw_permutation_config.assign(
&mut region,
Expand Down Expand Up @@ -372,9 +374,11 @@ impl<F: Field> SubCircuit<F> for EvmCircuit<F> {
fn instance(&self) -> Vec<Vec<F>> {
let block = self.block.as_ref().unwrap();

let (rws_assignments_padding, _) = RwMap::table_assignments_prepad(
let (rws_assignments_padding, _) = RwMap::table_assignments_padding(
&block.rws.table_assignments(true),
block.circuits_params.max_rws,
// only padding first row
block.rw_table_chunked_index == 0,
);

assert!(!rws_assignments_padding.is_empty());
Expand Down
26 changes: 23 additions & 3 deletions zkevm-circuits/src/evm_circuit/execution/end_block.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ impl<F: Field> ExecutionGadget<F> for EndBlockGadget<F> {
let is_empty_block =
IsZeroGadget::construct(cb, cb.curr.state.rw_counter.clone().expr() - 1.expr());

let total_rws_before_padding = cb.curr.state.rw_counter.clone().expr() - 1.expr()
let _total_rws_before_padding = cb.curr.state.rw_counter.clone().expr() - 1.expr()
+ select::expr(
is_empty_block.expr(),
0.expr(),
Expand Down Expand Up @@ -83,11 +83,31 @@ impl<F: Field> ExecutionGadget<F> for EndBlockGadget<F> {
// meaningful txs in the tx_table is total_tx.
});

// TODO fix below logic checking logic
// - startop only exist in first chunk
// - total_rws_before_padding are across chunk. We need new way, maybe new
// `rw_counter_intra_chunk` to lookup padding logic

// 3. Verify rw_counter counts to the same number of meaningful rows in
// rw_table to ensure there is no malicious insertion.
// Verify that there are at most total_rws meaningful entries in the rw_table
cb.rw_table_start_lookup(1.expr());
cb.rw_table_start_lookup(max_rws.expr() - total_rws_before_padding.expr());
// TODO only lookup start on first rwtable chunk
// cb.rw_table_start_lookup(1.expr());
// current SRS size < 2^30 so use 4 bytes (2^32) in LtGadet should be enough
// TODO find better way other than hardcode
// let is_end_padding_exist = LtGadget::<_, 32>::construct(
// cb,
// 1.expr(),
// max_rws.expr() - total_rws_before_padding.expr(),
// );
// cb.debug_expression(
// "is_end_padding_exist",
// max_rws.expr() - total_rws_before_padding.expr(),
// );
// cb.condition(is_end_padding_exist.expr(), |cb| {
// cb.rw_table_padding_lookup(total_rws_before_padding.expr() + 1.expr());
// cb.rw_table_padding_lookup(max_rws.expr());
// });
// Since every lookup done in the EVM circuit must succeed and uses
// a unique rw_counter, we know that at least there are
// total_rws meaningful entries in the rw_table.
Expand Down
24 changes: 22 additions & 2 deletions zkevm-circuits/src/evm_circuit/util/constraint_builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1290,8 +1290,8 @@ impl<'a, F: Field> EVMConstraintBuilder<'a, F> {
);
}

// RwTable Padding (Start tag)

// RwTable Start (Start tag)
#[allow(dead_code)]
pub(crate) fn rw_table_start_lookup(&mut self, counter: Expression<F>) {
self.rw_lookup_with_counter(
"Start lookup",
Expand All @@ -1310,6 +1310,26 @@ impl<'a, F: Field> EVMConstraintBuilder<'a, F> {
);
}

// RwTable Padding (Padding tag)
#[allow(dead_code)]
pub(crate) fn rw_table_padding_lookup(&mut self, counter: Expression<F>) {
self.rw_lookup_with_counter(
"Padding lookup",
counter,
0.expr(),
Target::Padding,
RwValues::new(
0.expr(),
0.expr(),
0.expr(),
Word::zero(),
Word::zero(),
Word::zero(),
Word::zero(),
),
);
}

// Copy Table

#[allow(clippy::too_many_arguments)]
Expand Down
Loading

0 comments on commit dd5c9bb

Please sign in to comment.