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

[proof-chunk] merge to main branch #1785

Merged
merged 16 commits into from
Mar 21, 2024
Merged

[proof-chunk] merge to main branch #1785

merged 16 commits into from
Mar 21, 2024

Conversation

hero78119
Copy link
Member

@hero78119 hero78119 commented Mar 1, 2024

Description

This PR makes the first move toward single block chunking into multiple proof & aggregation

Issue Link

#1498

Type of change

  • Breaking change (fix or feature that would cause existing functionality to not work as expected)

Rationale

design rationale are list below as separated section

hero78119 and others added 7 commits October 30, 2023 20:11
…nk (#1641)

### Description

[_PR description_]

### Issue Link

#1601 

### Type of change

- [ ] Bug fix (non-breaking change which fixes an issue)
- [ ] New feature (non-breaking change which adds functionality)
- [x] Breaking change (fix or feature that would cause existing
functionality to not work as expected)
- [ ] This change requires a documentation update

### Highlights
- separate rw_table in evm_circuit/state_circuit and each have its own
permutationchip. fingerprints checking will be deferred to root circuit.
- disable rwtable first row check (by disable selector offset=0 in
state_circuit, other offset toggle on as usual), since it will be copy
constraints via public input.
- keep `Rw::Start` and introduce `Rw::Padding` to support post-padding
in address-sorted rwtable in last_chunk.
- instance (new public input) column are design into two, one for
prev_chunk context, another for current_chunk context to be used for
next chunk. So in root circuit commitment of instance column can be used
in snark-verifier without need to unwrap it.

> Update on 18 Oct 2023: beginchunk/endchunk virtual step,
inner_rw_counter, chunkctx

- add Begin/EndChunk virtual step. BeginChunk is not mandatory in first
chunk first step. while EndChunk is not mandatory in last chunk last
step.
- add `inner_rw_counter` which is local rw_counter within each chunk.
This is used to count valid rw_row and assure Rw::Padding are append
consecutively in `end_block.rs` logic => EndChunk should apply similar
check later on
- introduce chunkctx->{chunk_index, total_chunks} to tell first chunk
(chunk_index==0) and last chunk (chunk_index + 1 == total_chunks) during
witness generation/constraints assignment
- add chunkctx_table to able to lookup chunk context (chunk_index,
next_chunk_index, total_chunk, initial_rwc, end_rwc..etc) in exec step
to allow various conditional check based on current chunk context

### How Has This Been Tested?

[_explanation_]

### More context on Rw::Padding (Not cover in current PR, will be
handled in later multiple chunk PR to make scope smaller)

In new logic, `Rw::Start` will be insert in first chunk offset 0, while
other holes are filled by `Rw::Padding` in last chunk(s). The
address-sorted rwtable layout will be
```
address-sorted rwtable
## first chunk
[
      Rw::start,  // offset 0, Rw::Start is only in first chunk, and only in offset 0, constrainted by public input
      ....(normal Rw), 
       ...(Rw::Padding),  // padding if there are only one chunk
]

## end chunk (if there are > 1 chunk)
[
      ....(normal Rw),  // offset 0 are carry over from previous chunk, other are address sorted
       ...(Rw::Padding) // padding in end chunk
]
```

For chronologically rwtable, since there is no in-row constraints to
check each Rw operation, so theoretically Rw::Padding rows can be filled
in any offset. However, we also need to assure there is no malicious
insertion other than Rw::Padding. To do that, we will rewrite this logic
in later PR
https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/main/zkevm-circuits/src/evm_circuit/execution/end_block.rs#L86-L90
to lookup consecutive `Rw::Padding` at **chronologically** sorted table,
at the END of EACH chunk.

> A tricks: first Rw::Padding rw_counter need to be set as last
(globally) valid row rw_counter + 1. This is to make sure in both
chronologically rw_table or address-sorted rw_table it's always append
in the end of rw_table.

```
chronologically rwtable, ascending sorted by `rw_counter`.
## first chunk
[
      Rw::start,  // offset 0, Rw::Start is only in first chunk, constrainted by public input
      ...(normal Rw),
      ...(Rw::Padding),   // first Rw::Padding rw_counter need to be set as last (globally) valid row rw_counter + 1, last means from last !!chunk!!. It assures Rw::Padding always append at the end of each chunk
]

## end chunk (if there are > 1 chunk)
[
      ....(normal Rw),  // offset 0 are carry over from previous chunk, other are rw_counter sorted
       ...(Rw::Padding) // padding, also rw_counter sorted
]
```
### Description

Depends on #1641 with extra commit: adding fingerprint equality check on
chronological/by address rw_table
Fingerprint check gate will be enable in last chunk last row

### instance columns, top down order match instance array order

chunk ctx
- [current chunk index, total chunk, initial rwc] // equal with
chunk_{i-1}
- [next chunk index, total chunk, next rwc] equal with chunk_{i+1}

pi circuit
- [pi digest lo, pi digest hi] // same across all chunks

state circuit
- [prev permutation fingerprint] // equal with chunk_{i-1}
- [next permutation fingerprint] // equal with chunk_{i+1}
- [alpha, gamma] // same across all chunks

evm circuit
- [prev permutation fingerprint] // equal with chunk_{i-1}
- [next permutation fingerprint] // equal with chunk_{i+1}
- [alpha, gamma] // same across all chunks

### Type of change

- [ ] Bug fix (non-breaking change which fixes an issue)
- [x] New feature (non-breaking change which adds functionality)
- [ ] Breaking change (fix or feature that would cause existing
functionality to not work as expected)
- [ ] This change requires a documentation update
### Description

covered item
- [x] supercircuit simplify instance columns related to chunkctx to just
one column
- [x] first chunk instance: chunk continuity related fields should be
constraints as constant.
- [x] aggregate multiple super circuit proof chunk with chunk
consistency check .
- [x] compute permutation fingerprint challenges `alpha,gamma` from
rw_table advices commitments and assert its equality
- [x] generalized `challenge([column_indexs], challenge_column_index)`
to a new protocol structure so more challenges in the future can be
added.

TODO
- [ ] verify multiple chunk from bus_mapping => rely on
#1690
 
### Issue Link


#1603

### Type of change

- [ ] Bug fix (non-breaking change which fixes an issue)
- [ ] New feature (non-breaking change which adds functionality)
- [x] Breaking change (fix or feature that would cause existing
functionality to not work as expected)
- [ ] This change requires a documentation update

### Tests

Light tests pass.
integration test failed due to challenge computation in witness not
implemented yet, which will be done in bus mapping chunk PR.
### Description
Instantiate circuits with `Block` and specified `Chunk` from
bus-mapping. Refactor `CircuitInputBuilder` to generate given number of
`Chunk`s with fixed or dynamic params. Note that one instance of the
circuit corresponds to one chunk instead of one block.
<img width="606" alt="Screen Shot 2023-12-08 at 11 37 30 PM"
src="https://github.com/privacy-scaling-explorations/zkevm-circuits/assets/45245961/84eac662-5adf-49d6-99bf-eefc295cf5aa">
### Issue Link


#1696

### Type of change

- [ ] Bug fix (non-breaking change which fixes an issue)
- [ ] New feature (non-breaking change which adds functionality)
- [x] Breaking change (fix or feature that would cause existing
functionality to not work as expected)
- [ ] This change requires a documentation update

### Contents

- Initialize the `CircuitInputBuilder` with either `FixedCParam` or just
specify the total number of chunk and dynamically derive parameter after
a dry run.
- In `handle_tx` split the chunk whenever the local `rwc` exceeds the
target amount, specifically by setting the `EndChunk` and proceed to the
next `BeginChunk` if needed.
- Commit the `ChunkCtx` for each chunk at the end, which tracks the
global `Rw` range & local `rwc` later used in the State circuits.
- After the block is handled, generate witness for a specific chunk with
`builder.chunk_convert(idx)`, analogous to `builder.block_convert()`.
- Config the circuit with both block and chunk, which leads to API
changes in `SubCircuit<F: Field>` trait including
`new_from_block(&block, &chunk)` and `min_num_rows_block(&block,
&chunk)`.

### Workflow
For `CircuitInputBuilder` chunk is needed to build **all** circuits:
```
let builder = BlockData::new_from_geth_data(geth_data.clone())
        .new_circuit_input_builder()
        .handle_block(&eth_block, &geth_traces)
        .expect("handle_block");
    
let block = block_convert(&builder);   
let chunk = chunk_convert(&builder, 0);
   
let circuit = SuperCircuit::new_from_block(&block, &chunk);
```
For `CircuitTestBuilder` **modifier** is applied to both block and
chunk, and you can run with fixed or dynamic params:
```
CircuitTestBuilder::new_from_test_ctx(
        TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap(),
    )
    .modifier(Box::new(move |block, chunk| {
        // do something..
    }))
    .run_dynamic_chunk(4, 2);
```
```
CircuitTestBuilder::new_from_block(block)
    .params(FixedCParams {
        total_chunks: 2,
        max_rws: 60,
        ..Default::default()
    })
    .run_chunk(1);
```
Default `run()` still works since it runs one chunk internally.
```
CircuitTestBuilder::new_from_block(block).run()
```

---------

Co-authored-by: sm.wu <hero78119@gmail.com>
…test (#1773)

### Content
Reported issues found on multi-chunk testing

- [x] refactor 1: simply chunking boundary judgement logic in
bus-mapping to ready for finish other incompleted features + avoid tech
dept in the future
- [x] add uncompleted logic in bus-mapping: chronological and by-address
rwtable not propagate pre-chunk last rw correctly.
- [x] edge case: deal with dummy chunk for real chunk less than desired
chunk in circuit params
- [x] allow zero limb diff in state_circuit lexicoordering => we allow
duplicated `rw_counter` in `padding`, and rely on permutation
constraints on by-address/chronological rw_table to avoid malicious
padding insert.
- [x] super_circuit/root_circuit tests adopt multiple chunk  

### Related Issue
To close
#1778
@hero78119 hero78119 marked this pull request as draft March 1, 2024 03:20
@github-actions github-actions bot added crate-bus-mapping Issues related to the bus-mapping workspace member crate-zkevm-circuits Issues related to the zkevm-circuits workspace member T-bench Type: benchmark improvements crate-circuit-benchmarks Issues related to the circuit-benchmarks workspace member crate-integration-tests Issues related to the integration-tests workspace member crate-gadgets Issues related to the gadgets workspace member labels Mar 1, 2024
@hero78119 hero78119 mentioned this pull request Mar 1, 2024
@hero78119
Copy link
Member Author

Docs & materials

@hero78119
Copy link
Member Author

hero78119 commented Mar 1, 2024

Permutation Fingerprints

To constrain 2 rw_table

  • chronological rw_table: sorted by rw counter
  • by-address rw table: sorted by address

are equals across multiple chunks, we constrain Permutation(chronological_rw_table) == Permutation(by_address_rw_table) via circuit constrains. Permutation fingerprints, in shorts, are via RLC columns of each row into one and accumulated into a single field value, passing them via public input across different chunk, and reach to end last chunk last row.

In the end, equality are constraints by gate in super_circuit

meta.create_gate(
"chronological rwtable fingerprint == by address rwtable fingerprint",
|meta| {
let is_last_chunk = chunk_ctx_config.is_last_chunk.expr();
let chronological_rwtable_acc_fingerprint = evm_circuit
.rw_permutation_config
.acc_fingerprints_cur_expr();
let by_address_rwtable_acc_fingerprint = state_circuit
.rw_permutation_config
.acc_fingerprints_cur_expr();
let q_row_last = meta.query_selector(evm_circuit.rw_permutation_config.q_row_last);
vec![
is_last_chunk
* q_row_last
* (chronological_rwtable_acc_fingerprint
- by_address_rwtable_acc_fingerprint),
]
},
);

@hero78119
Copy link
Member Author

hero78119 commented Mar 1, 2024

Continuity constraint on evm_circuit execution state

We introduce new virtual steps

  • EndChunk: write execution state back to rw_table
  • BeginChunk: read execution state from rw_table

to carry on the execution state begin chunk. BeginChunk will be append ahead of chunks execution steps except for the 1st chunk, while EndChunk will be added append to end of chunks except for the last chunk (EndBlock instead)

For rw_table we already able to carry on it continuity via public input, we dont implement extra public input to carry execution state. Instead we just write execution state from/to rw_table to get a free-ride.

An exception: begin_chunk/end_chunkwe can NOT read/write exec state rwc field

to rw_table because we rely rwc to assure rw lookup correctness. Therefore initial_rwc/end_rwc are exposed as evm circuit public input via chunk_ctx_table

F::from(chunk.chunk_context.initial_rwc as u64),
F::from(chunk.chunk_context.end_rwc as u64),

and in execution.rs circuit first/last row we lookup rwc from chunk context table

There is one interesting property of BeginChunk: it will constraint next execution state, so it can NOT be ahead of BeginTx, because BeginTx is the one define new transaction execution state. This was implemented in naive way: checking and chunk ahead before max_rws to assure there is space for end_tx -> begin_tx

self.check_and_chunk(
geth_trace,
tx.clone(),
tx_ctx.clone(),
None,
last_call.clone(),
)?;

@hero78119
Copy link
Member Author

hero78119 commented Mar 1, 2024

Bus-mapping witness chunking

Overall it follows the original design of circuit_input_buider to leverage mutable context when processing steps. In proof chunking, we introduce new chunk_ctx which is basically recording context information related to chunk, such as current chunk index…

With check_and_chunk condition match

self.set_end_chunk(&next_ops, Some(&tx));
// need to update next_ops.rwc to catch block_ctx.rwc in `set_end_chunk`
next_ops.rwc = self.block_ctx.rwc;
// tx.id start from 1, so it's equivalent to `next_tx_index`
self.commit_chunk_ctx(true, tx.id as usize, last_copy, last_call);
self.set_begin_chunk(&next_ops, Some(&tx));

we finalize current chunk and bump chunk_ctx to the next, until we reach the end of desired number of total_chunks. To support dynamic max_rws/max_evms calculation in unittest, there will be 2 pass going over whole block. First pass is for estimated max_rws/max_evms needed per chunk, and then second pass go over block again and finalized circuit_input_builder<FixedParams>.

New Chunk witness. While Block witness deal with block level data, Chunk as its name, is for chunk level data. chunk_convert which output all the chunks to be filled into individual super circuit as witness.

@hero78119
Copy link
Member Author

permutation fingerprint challenges

Permutation challenge is specially designed as an application-level challenge out of native halo2. The reason is because permutation challenge are cross different ConstrainSystem which halo2 yet support. The challenge are computed in bus-mapping via get_rwtable_cols_commitment Giving rw_table column vector from multiple chunk, this function will derive respective KZG commitments for each column and then poseidon hash all of them for challenge. challenge will be feed to super circuit as public input.

In aggregation circuit, user challenge value will be verified via poseidon circuit.

@hero78119
Copy link
Member Author

hero78119 commented Mar 1, 2024

chunk consistency check on aggregation circuit

Each chunk will derive respective super circuit proof and in final aggregation circuit we layout all of them to prove

  1. validity of each proof
  2. consistency check between ith, {i+1}th chunk via public input

Above verifier logic are arithmetization into circuit constrain in root_circuit With those magic to hide all the detail from final decider, final snark public_input is just lo-hi hash without leak any chunking context and complexity.

@hero78119
Copy link
Member Author

hero78119 commented Mar 1, 2024

rw_table padding logic

rw table will be padding to max_rws and previously we are padding via Rw::Start ahead.
With reasoning here we introduce new padding Rw::Padding. To relief the complex padding rwc calculation across chunk, right now we adapt simply design by incremental rwc just within each chunk. It will make Padding in by-address sorted might got rwc different by 0, 1. This relaxation reflect in build_padding_constraints constrain.

We will lookup consecutive padding in end_chunk/end_block via RwTablePaddingGadget to avoid malicious insertion.

Actually the rw lookup targeting table is chronological_rw_table and the table constraint on incremental rwc is not implemented yet. Means right we can randomly sorted chronological_rw_table within single chunk while still keep lookup correctly. This mechanism can be implemented later

@hero78119
Copy link
Member Author

What can be done after next

With first move of proof chunk we achieve the milestone to be able to deal with proof parallism on block data level by concurrent provers, each deal with smaller k to get final chunk, and then aggregate all proof.

An known limitation on root circuit, with current complex linearization(gate) functions, under k=26 in root circuit we can only verify 2 super circuit prove. To fully relax the power, we can design root circuit as recursive proof (issue #1631) so this part can be slightly eliminated.

with recursive proof, root circuit part still be limited as sequential execution.

@hero78119 hero78119 marked this pull request as ready for review March 1, 2024 08:50
@hero78119
Copy link
Member Author

hero78119 commented Mar 1, 2024

relevant tests

@hero78119
Copy link
Member Author

circuit stats (before & after)

chunkctx_table

new added table

+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+
| circuit        | constraints | rots | min/max(rots) | fix_cols | selectors | adv_cols | perm_cols | lookups | degree | mem_gb |
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+
| chunkctx_table | 1           | 2    | 0/1           | 1        | 1         | 1        | 1         | 0       | 3      | 54     |
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+

state circuit

new padding step logic increase number of constraints

+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+
| circuit        | constraints | rots | min/max(rots) | fix_cols | selectors | adv_cols | perm_cols | lookups | degree | mem_gb |
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+
| state          | 203         | 3    | -1/1          | 3        | 0         | 49       | 0         | 36      | 10     | 2224   |
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+
| state          | 242         | 3    | -1/1          | 3        | 3         | 64       | 5         | 36      | 10     | 2984   |
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+

evm circuit

constraints increase due to

  • new virtual step state transition
  • permutation fingerprint gadget
  • chunk context lookup
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+
| circuit        | constraints | rots | min/max(rots) | fix_cols | selectors | adv_cols | perm_cols | lookups | degree | mem_gb |
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+
| evm            | 42318       | 21   | 0/20          | 5        | 3         | 131      | 3         | 53      | 7      | 2976   |
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+
| evm            | 43624       | 22   | -1/20         | 8        | 8         | 175      | 10        | 68      | 9      | 4116   |
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+

super circuit

+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+
| circuit        | constraints | rots | min/max(rots) | fix_cols | selectors | adv_cols | perm_cols | lookups | degree | mem_gb |
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+
| super          | 45168       | 106  | -89/207       | 57       | 16        | 498      | 25        | 235     | 10     | 21736  |
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+
| super          | 46514       | 106  | -89/207       | 61       | 25        | 558      | 38        | 250     | 10     | 24620  |
+----------------+-------------+------+---------------+----------+-----------+----------+-----------+---------+--------+--------+

@ed255 ed255 linked an issue Mar 7, 2024 that may be closed by this pull request
8 tasks
@ed255 ed255 linked an issue Mar 7, 2024 that may be closed by this pull request
Copy link
Collaborator

@miha-stopar miha-stopar left a comment

Choose a reason for hiding this comment

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

Just some initial questions and nitpicks

zkevm-circuits/src/witness/chunk.rs Outdated Show resolved Hide resolved
zkevm-circuits/src/root_circuit.rs Outdated Show resolved Hide resolved
instance_i.sc_rwtable_row_next_fingerprint.assigned(),
instance_i_plus_one
.sc_rwtable_row_prev_fingerprint
.assigned(),
Copy link
Collaborator

Choose a reason for hiding this comment

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

I am wondering whether it's meant instance_i.sc_rwtable_row_next_fingerprint = instance_i_plus_one.sc_rwtable_row_curr_fingerprint.assigned, so curr instead of prev in i_plus_one?

Copy link
Member Author

Choose a reason for hiding this comment

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

Thanks for catch up this!
instance_i latest accumuated value will propagate to instance_i+1
Fix by renamed it to i.curr = {i+1}.prev semantically and erase next term to avoid confused

zkevm-circuits/src/witness/chunk.rs Outdated Show resolved Hide resolved
zkevm-circuits/src/super_circuit.rs Outdated Show resolved Hide resolved
zkevm-circuits/src/super_circuit.rs Show resolved Hide resolved
Copy link
Collaborator

@ChihChengLiang ChihChengLiang left a comment

Choose a reason for hiding this comment

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

First round

tx_ctx: TransactionContext,
next_geth_step: Option<(usize, &GethExecStep)>,
last_call: Option<Call>,
) -> Result<bool, Error> {
Copy link
Collaborator

Choose a reason for hiding this comment

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

We should comment on what this bool mean.
It seems to me true means we have the next chunk and false means we are at the last chunk.

Copy link
Member Author

Choose a reason for hiding this comment

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

good idea, explanation was added in latest commit

bus-mapping/src/circuit_input_builder.rs Outdated Show resolved Hide resolved
bus-mapping/src/circuit_input_builder.rs Outdated Show resolved Hide resolved
bus-mapping/src/operation.rs Outdated Show resolved Hide resolved
bus-mapping/src/operation.rs Outdated Show resolved Hide resolved
Copy link
Collaborator

@ChihChengLiang ChihChengLiang left a comment

Choose a reason for hiding this comment

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

LGTM modulo Miha's feedback.
Epic work on completing the proof chunking!

Copy link
Collaborator

@miha-stopar miha-stopar left a comment

Choose a reason for hiding this comment

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

Tremendous work! I added just some nitpicks.

gadgets/src/permutation.rs Outdated Show resolved Hide resolved
zkevm-circuits/src/evm_circuit/execution.rs Outdated Show resolved Hide resolved
zkevm-circuits/src/state_circuit.rs Outdated Show resolved Hide resolved
zkevm-circuits/src/witness/chunk.rs Outdated Show resolved Hide resolved
zkevm-circuits/src/table/chunk_ctx_table.rs Outdated Show resolved Hide resolved
@hero78119 hero78119 added this pull request to the merge queue Mar 21, 2024
Merged via the queue into main with commit 443da4b Mar 21, 2024
15 checks passed
@hero78119 hero78119 deleted the proof-chunk branch March 21, 2024 06:10
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
crate-bus-mapping Issues related to the bus-mapping workspace member crate-circuit-benchmarks Issues related to the circuit-benchmarks workspace member crate-gadgets Issues related to the gadgets workspace member crate-integration-tests Issues related to the integration-tests workspace member crate-zkevm-circuits Issues related to the zkevm-circuits workspace member T-bench Type: benchmark improvements
Projects
Status: Done
Development

Successfully merging this pull request may close these issues.

[proof-chunk] implement uncompleted features in bus-mapping and refactor Proof chunking exploration
4 participants