search

taikoxyz / zkevm-circuits

DEPRECATED in favor of https://github.com/taikoxyz/raiko! Taiko's fork of the PSE's ZK-EVM
Other
159 stars 125 forks source link

MPT review #39

Open Brechtpd opened 1 year ago

Brechtpd commented 1 year ago

First step is understanding the spec and making sure it does what it needs to do compared to e.g. geth. The second step is comparing the spec against the implementation.

References:

Brechtpd commented 1 year ago

TODO list:

CeciliaZ030 commented 1 year ago

Make the CellManager automatically aware of "contexts", instead of having to manually reset the state in each matchx!/ifx arm. If a match arm/if branch is take, the cell manager pushes a new context so that when the arm is left the state can be restored to how it was before it was taken, so that all cell positions used in that arm usable again (all arms in matchx!, if/else statements are mutually exclusive so a cell in e.g. the if statement can be used to store different data then in the else statement).

I'm working on this and It looks quite impossible to dynamically apply different contexts as the circuits branch out, because we don't know which branch it will actually takes until we have the witness. I can save all possible contexts like this, explicitly:

let x = meta.query_bool();
let cm_if = cm.clone();
let cm_else = cm.clone();
ifx! x {
    let cm_temp = cm_if;
    // assign some cells with cm
    cm_if = cm_temp;
} elsex {
    let cm_temp = cm_else;
    // assign some cells with cm
    cm_else = cm_temp;
}

// then if x is actually true in witness, we set cm = cm_if here, if not we set cm = cm_else
// but we don't know what x is ...

Not sure if you have other work-arounds or am I getting the right idea, but one things I can think of is to save all paths, namely [cm_if, cm_else] and maybe do apply_managed_cells() at the end, but even this function requires seeing the actual advice assignment. Perhaps we have to change Halo2 API?

Brechtpd commented 1 year ago

I think you got the right idea, but I think we can keep it very simply! Because the location of the cell is stored in the Cell, no need to actually keep these contexts around for the witness generation.

For example, and to keep things easy, let's say the cell manager has 10 columns it can use, so the only "context" state is just how many columns have already been used:

struct Context {
  num_used: usize;
}

Now we just have to keep track of these while building the circuit:

// We're in context[0] now
config.dummy1 = cb.query_cell(); // will use column[0]
config.dummy2 = cb.query_cell(); // will use column[1]
// context[0].num_used == 2
ifx! x {
    // New context is pushed, copied from the parent one so context[1].num_used == 2
    config.cell_true_1 = cb.query_cell(); // will use column[2]
    require!(config.cell_true_1 => 0);
    config.cell_true_2 = cb.query_cell(); // will use column[3]
    require!(config.cell_true_2 => 1);
    // context[1].num_used == 4
    // End of the arm, context[1] is popped
} elsex {
    // New context is pushed, copied from the parent one so context[1].num_used == 2
    config.cell_false_1 = cb.query_cell(); // will use column[2]
    require!(config.cell_false_1 => 1);
    // context[1].num_used == 3
    // End of the arm, context[1] is popped
}
// Back at context[0], but we needed max 2 cells per arm in the if/else statement above, 
// so context[0].num_used == 4 here
config.dummy3 = cb.query_cell(); // will use column[4]

In the example above, config.cell_true_1 and config.cell_false_1 will point to the same location! It's up to whoever writes the witness to make sure that the witness is only assigned to config.cell_true_1 OR config.cell_false_1 depending on the condition that will be triggered, but that's something that will be known.

// Witness generation
if x {
    self.cell_true_1.assign(...)?;
} else {
    self.cell_false_1.assign(...)?;
}

Still a good idea to add some checking on this to make sure a cell location is only assigned a single time because otherwise hard to track this down:

// Witness generation
self.cell_true_1.assign(...)?;
self.cell_false_1.assign(...)?; // ERROR: cell location assigned more than once!