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 5, 2023
1 parent 69680b8 commit b97ba34
Show file tree
Hide file tree
Showing 16 changed files with 256 additions and 61 deletions.
45 changes: 34 additions & 11 deletions bus-mapping/src/circuit_input_builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,9 @@ 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, PaddingOp, RWCounter, StartOp, RW,
},
rpc::GethClient,
state_db::{self, CodeDB, StateDB},
};
Expand Down Expand Up @@ -293,11 +295,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 +307,52 @@ impl CircuitInputBuilder<FixedCParams> {
max_rws
);
}
let (padding_start, padding_end) = (1, max_rws - total_rws); // rw counter start from 1
// TODO only push StartOp in first chunk
push_op(
&mut state.block.container,
&mut end_block_last,
RWCounter(padding_start),
RWCounter(1),
RW::READ,
StartOp {},
);
if padding_end != padding_start {
println!("checking..");
if max_rws - total_rws > 1 {
println!("are u there?");
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_end),
RWCounter(padding_start),
RW::READ,
StartOp {},
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;
}
}

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 @@ -395,6 +417,7 @@ impl CircuitInputBuilder<DynamicCParams> {

let total_rws_before_padding: usize =
<RWCounter as Into<usize>>::into(self.block_ctx.rwc) - 1; // -1 since rwc start from index `1`
println!("total_rws_before_padding: {:?}", total_rws_before_padding);
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 };
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.stack.len() - 1))
}
}
}

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
19 changes: 17 additions & 2 deletions zkevm-circuits/src/evm_circuit/execution/end_block.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ use crate::{
constraint_builder::{
ConstrainBuilderCommon, EVMConstraintBuilder, StepStateTransition, Transition::Same,
},
math_gadget::{IsEqualGadget, IsZeroGadget},
math_gadget::{IsEqualGadget, IsZeroGadget, LtGadget},
not, CachedRegion, Cell,
},
witness::{Block, Call, ExecStep, Transaction},
Expand Down Expand Up @@ -86,8 +86,23 @@ impl<F: Field> ExecutionGadget<F> for EndBlockGadget<F> {
// 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
// TODO only lookup start on first rwtable chunk
cb.rw_table_start_lookup(1.expr());
cb.rw_table_start_lookup(max_rws.expr() - total_rws_before_padding.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
22 changes: 20 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,7 @@ impl<'a, F: Field> EVMConstraintBuilder<'a, F> {
);
}

// RwTable Padding (Start tag)

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

// RwTable Padding (Padding tag)
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 b97ba34

Please sign in to comment.