Fix exp circuit padding

[rrzhang139]

Need to enforce the soundness of the exp_circuit padding. Basically there is no selector that fixes the padding so padding constraints are not being checked.

[rrzhang139]

I'm having an issue with cells not being assigned. Specifically, when starting at the padding offset, I can enable selectors of 3 rows until the 4th row, in which it throws an error like so CellNotAssigned { gate: Gate { index: 2, name: "verify all but the last step" }, region: Region { index: 0, name: "exponentiation circuit" }, gate_offset: 11, column: Column { index: 3, column_type: Advice }, offset: 21 }

[ed255]

I'm having an issue with cells not being assigned. Specifically, when starting at the padding offset, I can enable selectors of 3 rows until the 4th row, in which it throws an error like so CellNotAssigned { gate: Gate { index: 2, name: "verify all but the last step" }, region: Region { index: 0, name: "exponentiation circuit" }, gate_offset: 11, column: Column { index: 3, column_type: Advice }, offset: 21 }

I think the issue is that what you call the 4th row is actually the 5th! You have this code:

        self.q_usable.enable(region, offset)?;
        dbg!(offset + 1);
        self.q_usable.enable(region, offset + 1)?;
        dbg!(offset + 2);
        self.q_usable.enable(region, offset + 2)?;
        dbg!(offset + 3);
        self.q_usable.enable(region, offset + 3)?;
        dbg!(offset + 4);
        self.q_usable.enable(region, offset + 4)?;

This is enabling the q_usable at rows [offset+0, offset+1, offset+2, offset+3, offset+4] = [7, 8, 9, 10, 11] (that's 5 rows).

• offset+4 = 11
• Then you assign the other columns from offset+0 = 7 to offset+2*OFFSET_INCREMENT-1 = offset+14-1 = 20
• The mul_gate does rotation(10) on exp_table.base_limb See

  zkevm-circuits/zkevm-circuits/src/exp_circuit.rs

  Line 73 in 6e3d9dc

  meta.query_advice(exp_table.base_limb, Rotation(i + 7)),

• And is enabled with q_usable. This means that at offset=11 q_usable selects the constraint which reads exp_table.base_limb at offset+10 = 21, which is not assigned.

I have some questions about the approach for the constant fixed columns. I see that the ExpCircuit can be divided into steps, where each step takes 7 rows. I think we should have a parameter called max_exp_steps for the ExpCircuit, to force that 7 * max_exp_steps rows are assigned with their corresponding selectors set. Then the assignment function should first assign each step from the input, and then assign padding data on the remaining steps.
I haven't looked into detail at the ExpCircuit, but maybe it can encode the simplest exponentiation (like 1^0 or 1^1) in a single step, and that can be used as padding (no need to add special padding constraints). This is the approach that the keccak circuit uses for example (it just fills the remaining rows of the circuit with assignments to empty inputs).

[roynalnaruto]

We can put this PR on hold until privacy-scaling-explorations/zkevm-specs#359 is reviewed and merged.

[ed255]

The approach followed in the last two commits seems to be working!

Regarding choosing the circuit length (currently you're doing k - self.minimum_rows + 1; I assume there's a typo there and should be 1 << k instead of k)., I want to ask you to follow the same approach as other circuits, where a circuit parameter defines the number of rows / operations / steps that we want to use to setup the circuit. For reference, you can check the copy circuit as an example https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/main/zkevm-circuits/src/copy_circuit.rs and see how it uses the parameter max_copy_rows, or the tx circuit https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/main/zkevm-circuits/src/tx_circuit.rs and see how it uses the max_txs parameter.

Also, could you add the following test (or a similar one) that verifies that the fixed columns stay constant no matter the input?

    #[test]
    fn variadic_size_check() {
        let k = 20;
        // Empty
        let block: GethData = TestContext::<0, 0>::new(None, |_| {}, |_, _| {}, |b, _| b)
            .unwrap()
            .into();
        let mut builder =
            BlockData::new_from_geth_data_with_params(block.clone(), CircuitsParams::default())
                .new_circuit_input_builder();
        builder
            .handle_block(&block.eth_block, &block.geth_traces)
            .unwrap();
        let block = block_convert::<Fr>(&builder.block, &builder.code_db).unwrap();
        let circuit = ExpCircuit::<Fr>::new(block);
        let prover1 = MockProver::<Fr>::run(k, &circuit, vec![]).unwrap();

        // Non-empty
        let code = bytecode! {
            PUSH32(8)
            PUSH32(10)
            EXP
            PUSH32(3)
            PUSH32(5)
            EXP
            STOP
        };
        let builder = gen_data(code);
        let block = block_convert::<Fr>(&builder.block, &builder.code_db).unwrap();
        let circuit = ExpCircuit::<Fr>::new(block);
        let prover2 = MockProver::<Fr>::run(k, &circuit, vec![]).unwrap();

        assert_eq!(prover1.fixed(), prover2.fixed());
        assert_eq!(prover1.permutation(), prover2.permutation());
    }

I tried this test on the current state of the PR and it passes :)

[rrzhang139]

Hi @ed255, I think the passed in parameter k is of the form 1 << k because I passed in self.size which is equal to 1 << k. The latest commit actually does not pass the unit tests. If you pull the latest commit from the branch, and run cargo test --package zkevm-circuits --lib -- exp_circuit::tests::exp_circuit_single --exact you will get this error:
panicked at 'called Result::unwrap() on an Err value: NotEnoughRowsAvailable { current_k: 18 }', zkevm-circuits/src/exp_circuit.rs:548:64
This test uses 2^2, so there are 7 rows used, 13 rows are reserved for blinding factors and others (minimum rows) and the rest is padded. I’m not sure why it’s complaining that there are not enough rows to be assigned. 2^18 seems like more than enough rows to include minimum_rows() + used_rows. Are you passing tests on your side?

[rrzhang139]

Also, what should the default max_exp_rows value be? I've been testing 1 << 18 most of the time.

[ed255]

Hi @ed255, I think the passed in parameter k is of the form 1 << k because I passed in self.size which is equal to 1 << k.

I see! In that case I suggest using the variable name k for degree and num_rows for number of rows which is 1 << k.

The latest commit actually does not pass the unit tests. If you pull the latest commit from the branch, and run cargo test --package zkevm-circuits --lib -- exp_circuit::tests::exp_circuit_single --exact you will get this error: panicked at 'called Result::unwrap() on an Err value: NotEnoughRowsAvailable { current_k: 18 }', zkevm-circuits/src/exp_circuit.rs:548:64 This test uses 2^2, so there are 7 rows used, 13 rows are reserved for blinding factors and others (minimum rows) and the rest is padded. I’m not sure why it’s complaining that there are not enough rows to be assigned. 2^18 seems like more than enough rows to include minimum_rows() + used_rows. Are you passing tests on your side?

I didn't check any unit tests, I only tried running the variadic_size_check test I added in my previous commit. I also expected the circuit to run with a much lower k value. I can take a look at this.

Also, what should the default max_exp_rows value be? I've been testing 1 << 18 most of the time.

I think we should consider a default value that is good for testing. Maybe 1000 or 2000. Setting a value too big in tests can cause the mock prover to take a longer time (because it's verifying thousands of "padding" rows with the 1^1 assignments)

[ed255]

I have debugged the NotEnoughRowsAvailable from the exp_circuit_single test and it comes from the fact that an advice assignment is being made in row 262133 but the range of usable rows is 0..262133.

[rrzhang139]

@ed255 whats the difference between the value k that is inputted into MockProver::run and max_rows? I am testing with k = 10 (1 << 10 = 1024) and max_rows = 1000. I'm getting a new error when trying this:

Err([Region 0 ('exponentiation circuit') uses Gate 2 ('verify all but the last step') at offset 978, which requires cell in column Column { index: 3, column_type: Advice } at offset 988 with annotation None to be assigned.

Does this mean there is a cell outside the usable rows range? But usable rows should be between 0..1000?

[ed255]

@ed255 whats the difference between the value k that is inputted into MockProver::run and max_rows? I am testing with k = 10 (1 << 10 = 1024) and max_rows = 1000. I'm getting a new error when trying this:

In MockProver::run you pass the value k which is the degree. max_rows is a value of how many rows should this circuit use. max_rows then should be less than 1 << k, and then a bit more (to account for unusable rows).
The reason to have a parameter max_rows instead of trying to use all available rows is twofold:

• 1. So that when running a test with the mock prover, there are less rows to verify, which speeds the unit tests
• 2. In theory halo2 should be able to stack regions one on top of the other. So we may combine the ExpCircuit with another circuit (for example in the SuperCircuit) and they could share columns. In that case the ExpCircuit shouldn't reach the end, because there should be rows for another circuit. Currently we're not doing this.

Err([Region 0 ('exponentiation circuit') uses Gate 2 ('verify all but the last step') at offset 978, which requires cell in column Column { index: 3, column_type: Advice } at offset 988 with annotation None to be assigned.

Does this mean there is a cell outside the usable rows range? But usable rows should be between 0..1000?

Ah, halo2 doesn't report too much details here... Actually the NotEnoughRowsAvailable can come from trying to assign an advice / selector to a non-usable row.

I've spent some time debugging and I made a branch with a commit that fixes the issues (and makes all the tests pass). Please take a look: 3e17bbf In particular the files:

• bus-mapping/src/circuit_input_builder.rs
• zkevm-circuits/src/exp_circuit.rs

I used a local version of halo2 to add debugging logs.

The approach I followed in the commit is:

1. Reduce the default max_exp_rows to 2000 (a value that should work in most of our unit tests)
2. Join the functions to assign the exp circuit gadgets and the exp table into one, which takes an Exp event
3. Use the same function to assign the useful exp events (passed by argument), as well as the remaining "padding" ones to fill the rest of the circuit up to max_exp_rows
4. Recover the function assign_padding_rows now renamed to assign_unused_rows from before this PR to assign some extra rows to avoid the access to unassigned cell error (this is due to the usage of rotation 10 enabled by the circuit selector)

Please review the changes and feel free to integrate them in this PR or discuss them here :)

[roynalnaruto]

@ed255 I spent some time updating this as well. I am in favour of max_exp_steps and making the is_step a fixed column (instead of advice). Since each step is represented by 7 rows, and only the first of those rows is a step (is_step == 1), we are able to convert the is_step column to fixed.

The minimum number of rows required would be calculated by the number of steps in the exponentiation trace times 7 (since each step uses 7 rows). We basically would require max_exp_steps * 7 to be more than minimum number of rows available so that there are sufficient rows to populate the witness data.

Wdyt?

@rrzhang139 Is the above explanation clear?

[roynalnaruto]

Looking good, added a few comments though!

[rrzhang139]

@ed255 @roynalnaruto If you can resolve my failing test cases that would be very much appreciated. Somehow failing on testtool even though I never touched it.

[ed255]

@ed255 @roynalnaruto If you can resolve my failing test cases that would be very much appreciated. Somehow failing on testtool even though I never touched it.

I can look into it tomorrow!

[ed255]

@ed255 @roynalnaruto If you can resolve my failing test cases that would be very much appreciated. Somehow failing on testtool even though I never touched it.

This should fix it, can you try this change?

--- a/zkevm-circuits/src/table.rs
+++ b/zkevm-circuits/src/table.rs
@@ -1297,7 +1297,7 @@ impl ExpTable {
                 }
 
                 // pad an empty row
-                let row = [F::from_u128(0); 6];
+                let row = [F::from_u128(0); 5];
                 for (column, value) in exp_table_columns.iter().zip_eq(row) {
                     region.assign_advice(
                         || format!("exponentiation table row {}", offset),

[roynalnaruto]

@rrzhang139 Could you resolve conflicts coming from the latest update to main? We're very close to getting this merged, and then we can move on to #1100

[roynalnaruto]

Looks good to me

[roynalnaruto]

• ExpTable::columns removed since its already handled in the LookupTable trait implementation
• Removed the name_column annotations because table annotations are supported Annotate LookupTable & EVM Circuit columns #1137 and circuit annotations are a separate issue Apply Column annotations for all of our circuits. #1106
• Refactored the min_rows to include the UNUSABLE rows

[ed255]

LGTM! Great job! 😀