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

[proof chunk] introduce Padding virtual step #1718

Closed
wants to merge 1 commit into from
Closed

[proof chunk] introduce Padding virtual step #1718

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 24 additions & 17 deletions bus-mapping/src/circuit_input_builder.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -371,20 +371,27 @@ impl CircuitInputBuilder<FixedCParams> {
self.set_end_chunk(max_rws);
return;
}

// set end block
let mut end_block_not_last = self.block.block_steps.end_block_not_last.clone();
let mut end_block_last = self.block.block_steps.end_block_last.clone();
end_block_not_last.rwc = self.block_ctx.rwc;
end_block_last.rwc = self.block_ctx.rwc;
end_block_not_last.rwc_inner_chunk = self
.chunk_ctx
.as_ref()
.map_or_else(RWCounter::new, |chunk_ctx| chunk_ctx.rwc);
end_block_last.rwc_inner_chunk = self
// set padding
let last_step = self
.block
.txs()
.last()
.map(|tx| tx.last_step())
.unwrap_or_else(|| &self.block.block_steps.padding);
let mut padding = last_step.clone(); // padding step need to keep transition context
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Heads up: here use last_step because it's at the end of block.
In chunking, we should use next_tx.first_step instead

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just to make sure this_tx.last_step has the same transition witness as next_tx.first_step right?

Copy link
Member Author

@hero78119 hero78119 Jan 2, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No they are different. I thought we discussed this issue in Pr #1690 review section :)
Feel free to bring it up further if you thought it doenst make sense for why they different

padding.bus_mapping_instance = vec![]; // there is no rw in padding step
padding.exec_state = ExecState::Padding;
padding.rwc = self.block_ctx.rwc;
padding.rwc_inner_chunk = self
.chunk_ctx
.as_ref()
.map_or_else(RWCounter::new, |chunk_ctx| chunk_ctx.rwc);
// TODO automatially assign all field

// set end block
let mut end_block = padding.clone();
end_block.exec_state = ExecState::EndBlock;

let is_first_chunk = self
.chunk_ctx
.as_ref()
Expand All @@ -395,7 +402,7 @@ impl CircuitInputBuilder<FixedCParams> {

if let Some(call_id) = state.block.txs.last().map(|tx| tx.calls[0].call_id) {
state.call_context_read(
&mut end_block_last,
&mut end_block,
call_id,
CallContextField::TxId,
Word::from(state.block.txs.len() as u64),
Expand All @@ -421,7 +428,7 @@ impl CircuitInputBuilder<FixedCParams> {
if is_first_chunk {
push_op(
&mut state.block.container,
&mut end_block_last,
&mut end_block,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why don't we just move StartOp and PaddingOp here in to the padding ExecStep?

RWCounter(1),
RWCounter(1),
RW::READ,
Expand All @@ -433,7 +440,7 @@ impl CircuitInputBuilder<FixedCParams> {
let (padding_start, padding_end) = (total_rws + 1, max_rws - 1);
push_op(
&mut state.block.container,
&mut end_block_last,
&mut end_block,
RWCounter(padding_start),
RWCounter(padding_start),
RW::READ,
Expand All @@ -442,7 +449,7 @@ impl CircuitInputBuilder<FixedCParams> {
if padding_end != padding_start {
push_op(
&mut state.block.container,
&mut end_block_last,
&mut end_block,
RWCounter(padding_end),
RWCounter(padding_end),
RW::READ,
Expand All @@ -451,8 +458,8 @@ impl CircuitInputBuilder<FixedCParams> {
}
}

self.block.block_steps.end_block_not_last = end_block_not_last;
self.block.block_steps.end_block_last = end_block_last;
self.block.block_steps.padding = padding;
self.block.block_steps.end_block = end_block;

// set final rwc value to chunkctx
if let Some(chunk_ctx) = self.chunk_ctx.as_mut() {
Expand Down
14 changes: 7 additions & 7 deletions bus-mapping/src/circuit_input_builder/block.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,11 +45,11 @@ impl BlockContext {
/// Block-wise execution steps that don't belong to any Transaction.
#[derive(Debug)]
pub struct BlockSteps {
/// EndBlock step that is repeated after the last transaction and before
/// Padding step that is repeated after the last transaction and before
/// reaching the last EVM row.
pub end_block_not_last: ExecStep,
/// Last EndBlock step that appears in the last EVM row.
pub end_block_last: ExecStep,
pub padding: ExecStep,
/// EndBlock step that appears in the last chunk last EVM row.
pub end_block: ExecStep,
/// TODO Define and move chunk related step to Chunk struct
/// Begin op of a chunk
pub begin_chunk: ExecStep,
Expand Down Expand Up @@ -136,11 +136,11 @@ impl Block {
exec_state: ExecState::BeginChunk,
..ExecStep::default()
},
end_block_not_last: ExecStep {
exec_state: ExecState::EndBlock,
padding: ExecStep {
exec_state: ExecState::Padding,
..ExecStep::default()
},
end_block_last: ExecStep {
end_block: ExecStep {
exec_state: ExecState::EndBlock,
..ExecStep::default()
},
Expand Down
2 changes: 2 additions & 0 deletions bus-mapping/src/circuit_input_builder/execution.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,8 @@ pub enum ExecState {
BeginTx,
/// Virtual step End Tx
EndTx,
/// Virtual step Padding
Padding,
/// Virtual step End Block
EndBlock,
/// Virtual step End Chunk
Expand Down
50 changes: 34 additions & 16 deletions zkevm-circuits/src/evm_circuit/execution.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,7 @@ mod mulmod;
#[path = "execution/not.rs"]
mod opcode_not;
mod origin;
mod padding;
mod pc;
mod pop;
mod push;
Expand Down Expand Up @@ -185,6 +186,7 @@ use mul_div_mod::MulDivModGadget;
use mulmod::MulModGadget;
use opcode_not::NotGadget;
use origin::OriginGadget;
use padding::PaddingGadget;
use pc::PcGadget;
use pop::PopGadget;
use push::PushGadget;
Expand Down Expand Up @@ -246,6 +248,7 @@ pub struct ExecutionConfig<F> {
// internal state gadgets
begin_tx_gadget: Box<BeginTxGadget<F>>,
end_block_gadget: Box<EndBlockGadget<F>>,
padding_gadget: Box<PaddingGadget<F>>,
end_tx_gadget: Box<EndTxGadget<F>>,
begin_chunk_gadget: Box<BeginChunkGadget<F>>,
end_chunk_gadget: Box<EndChunkGadget<F>>,
Expand Down Expand Up @@ -386,7 +389,7 @@ impl<F: Field> ExecutionConfig<F> {
let (execute_state_first_step_whitelist, execute_state_last_step_whitelist) = (
HashSet::from([
ExecutionState::BeginTx,
ExecutionState::EndBlock,
ExecutionState::Padding,
ExecutionState::BeginChunk,
]),
HashSet::from([ExecutionState::EndBlock, ExecutionState::EndChunk]),
Expand Down Expand Up @@ -553,6 +556,7 @@ impl<F: Field> ExecutionConfig<F> {
// internal states
begin_tx_gadget: configure_gadget!(),
end_block_gadget: configure_gadget!(),
padding_gadget: configure_gadget!(),
end_tx_gadget: configure_gadget!(),
begin_chunk_gadget: configure_gadget!(),
end_chunk_gadget: configure_gadget!(),
Expand Down Expand Up @@ -876,11 +880,12 @@ impl<F: Field> ExecutionConfig<F> {
.chain(
IntoIterator::into_iter([
(
"EndTx can only transit to BeginTx or EndBlock or EndChunk",
"EndTx can only transit to BeginTx or Padding or EndBlock or EndChunk",
ExecutionState::EndTx,
vec![
ExecutionState::BeginTx,
ExecutionState::EndBlock,
ExecutionState::Padding,
ExecutionState::EndChunk,
],
),
Expand All @@ -889,6 +894,15 @@ impl<F: Field> ExecutionConfig<F> {
ExecutionState::EndChunk,
vec![ExecutionState::EndChunk],
),
(
"Padding can only transit to Padding or EndBlock or EndChunk",
ExecutionState::Padding,
vec![
ExecutionState::Padding,
ExecutionState::EndBlock,
ExecutionState::EndChunk,
],
),
(
"EndBlock can only transit to EndBlock",
ExecutionState::EndBlock,
Expand All @@ -914,9 +928,13 @@ impl<F: Field> ExecutionConfig<F> {
.collect(),
),
(
"Only EndTx or EndBlock can transit to EndBlock",
"Only EndTx or EndBlock or Padding can transit to EndBlock",
ExecutionState::EndBlock,
vec![ExecutionState::EndTx, ExecutionState::EndBlock],
vec![
ExecutionState::EndTx,
ExecutionState::EndBlock,
ExecutionState::Padding,
],
),
(
"Only BeginChunk can transit to BeginChunk",
Expand Down Expand Up @@ -1063,8 +1081,8 @@ impl<F: Field> ExecutionConfig<F> {
let is_last_chunk =
block.chunk_context.chunk_index == block.chunk_context.total_chunks - 1;

let end_block_not_last = &block.end_block_not_last;
let end_block_last = &block.end_block_last;
let padding = &block.padding;
let end_block = &block.end_block;
let begin_chunk = &block.begin_chunk;
let end_chunk = &block.end_chunk;
// Collect all steps
Expand All @@ -1077,7 +1095,7 @@ impl<F: Field> ExecutionConfig<F> {
.map(move |step| (tx, &tx.calls()[step.call_index], step))
}))
// add last dummy step just to satisfy below logic, which will not be assigned and count as real step
.chain(std::iter::once((&dummy_tx, &last_call, end_block_not_last)))
.chain(std::iter::once((&dummy_tx, &last_call, padding)))
.peekable();

let evm_rows = block.circuits_params.max_evm_rows;
Expand Down Expand Up @@ -1112,7 +1130,7 @@ impl<F: Field> ExecutionConfig<F> {
offset += height;
}

// part2: assign non-last EndBlock steps when padding needed
// part2: assign Padding steps when padding needed
if !no_padding {
if offset >= evm_rows {
log::error!(
Expand All @@ -1122,11 +1140,11 @@ impl<F: Field> ExecutionConfig<F> {
);
return Err(Error::Synthesis);
}
let height = ExecutionState::EndBlock.get_step_height();
let height = ExecutionState::Padding.get_step_height();
debug_assert_eq!(height, 1);
let last_row = evm_rows - 1;
log::trace!(
"assign non-last EndBlock in range [{},{})",
"assign Padding in range [{},{})",
offset,
last_row
);
Expand All @@ -1137,7 +1155,7 @@ impl<F: Field> ExecutionConfig<F> {
block,
&dummy_tx,
&last_call,
end_block_not_last,
padding,
height,
challenges,
assign_pass,
Expand All @@ -1160,7 +1178,7 @@ impl<F: Field> ExecutionConfig<F> {
block,
&dummy_tx,
&last_call,
end_block_last,
end_block,
height,
None,
challenges,
Expand Down Expand Up @@ -1268,7 +1286,7 @@ impl<F: Field> ExecutionConfig<F> {
}
assert_eq!(height, 1);
assert!(step.rw_indices_len() == 0);
assert!(matches!(step.execution_state(), ExecutionState::EndBlock));
assert!(matches!(step.execution_state(), ExecutionState::Padding));

// Disable access to next step deliberately for "repeatable" step
let region = &mut CachedRegion::<'_, '_, F>::new(
Expand Down Expand Up @@ -1312,7 +1330,7 @@ impl<F: Field> ExecutionConfig<F> {
challenges: &Challenges<Value<F>>,
assign_pass: usize,
) -> Result<(), Error> {
if !matches!(step.execution_state(), ExecutionState::EndBlock) {
if !matches!(step.execution_state(), ExecutionState::Padding) {
log::trace!(
"assign_exec_step offset: {} state {:?} step: {:?} call: {:?}",
offset,
Expand Down Expand Up @@ -1390,6 +1408,7 @@ impl<F: Field> ExecutionConfig<F> {
// internal states
ExecutionState::BeginTx => assign_exec_step!(self.begin_tx_gadget),
ExecutionState::EndTx => assign_exec_step!(self.end_tx_gadget),
ExecutionState::Padding => assign_exec_step!(self.padding_gadget),
ExecutionState::EndBlock => assign_exec_step!(self.end_block_gadget),
ExecutionState::BeginChunk => assign_exec_step!(self.begin_chunk_gadget),
ExecutionState::EndChunk => assign_exec_step!(self.end_chunk_gadget),
Expand Down Expand Up @@ -1536,8 +1555,7 @@ impl<F: Field> ExecutionConfig<F> {

// enable with `RUST_LOG=debug`
if log::log_enabled!(log::Level::Debug) {
let is_padding_step = matches!(step.execution_state(), ExecutionState::EndBlock)
&& step.rw_indices_len() == 0;
let is_padding_step = matches!(step.execution_state(), ExecutionState::Padding);
if !is_padding_step {
// expensive function call
Self::check_rw_lookup(
Expand Down
12 changes: 2 additions & 10 deletions zkevm-circuits/src/evm_circuit/execution/end_block.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -176,17 +176,9 @@ mod test {
.run();
}

// Test where the EVM circuit contains an exact number of rows corresponding to
// the trace steps + 1 EndBlock
// Test steps + 1 EndBlock without padding
#[test]
fn end_block_exact() {
fn end_block_no_padding() {
test_circuit(0);
}

// Test where the EVM circuit has a fixed size and contains several padding
// EndBlocks at the end after the trace steps
#[test]
fn end_block_padding() {
test_circuit(50);
}
}
3 changes: 2 additions & 1 deletion zkevm-circuits/src/evm_circuit/execution/end_tx.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -180,7 +180,8 @@ impl<F: Field> ExecutionGadget<F> for EndTxGadget<F> {
);

cb.condition(
cb.next.execution_state_selector([ExecutionState::EndBlock]),
cb.next
.execution_state_selector([ExecutionState::EndBlock, ExecutionState::Padding]),
|cb| {
cb.require_step_state_transition(StepStateTransition {
rw_counter: Delta(9.expr() - is_first_tx.expr() + coinbase_reward.rw_delta()),
Expand Down
Loading
Loading