Plookups in ZKEVM

Halo2 technical questions

The memory circuit is being built here:
[1] https://github.com/appliedzkp/zkevm-circuits/blob/main/src/state_circuit/memory.rs.

Not sure if everything is doing in a correct way, but a slight extension of the memory circuit can be found here:
[2] https://github.com/miha-stopar/zkevm-circuits/blob/main/src/state_circuit/memory.rs.

Two checks have been added: to check whether the init state is properly set when the address changes, and whether the value read is the same as the value written in the last operation at this address. I will turn it in the pull request once the issues listed bellow and the remaining todos are resolved.

I had problems with the following:

1. The init function - in [1], there is init state for each memory address added automatically, wouldn't it be proper to be done this by additional MemoryOps added by a user (like in [2])?

2. In [2], I read the value in previous row by:

let value_prev = meta.query_advice(value, Rotation::prev());

This makes the verification in MockProver to fail due to a selector error - value not found for the -1 row. I did an ugly fix:

let value = ops[0].steps[0]
    .as_ref()
    .map(|read_write| read_write.value().0);
region.assign_advice(
    || "value",
    self.value,
    31,
    || value.ok_or(Error::SynthesisError),
)?;

What would be the proper way to solve this?

3. In [1], there is a call:

self.step(&mut region, offset + step_offset, address, step)?;

Probably not important, but is there any special reason why offset + step_offset is used? This makes this value to skip some numbers.

High-level questions

I still have troubles to understand the following code snippet in our main document https://hackmd.io/Hy_nqH4yTOmjjS9nbOArgw:

 if(global_counter!=0):
                # add to bus mapping 
                global_counter = plookup(global_counter, valid_glbal_counters)
                mapping = plookup(mapping, valid_mappings)
                memory = "memory"
                memory_flag = memory_flag
                index = index
                value = value
                # check the key-value mapping
                require(mapping == global_counter + rand[0]*memory
                                    + rand[1]*memory_flag + rand[2]* index)

It appears like plookup table is being built and immediately after it is verified whether something is in the table.

I understand that plookup table is being built on the fly, but doesn't the verification happen later in the EVM proof?

barryWhiteHat the plookup table is provided as a witness value and each element in it is checked on the fly. So its not being built by the ciruct we just need to check every element in it.

I checked Han's document https://hackmd.io/Nwd0e5AgTVSBWRQlp-Ving, which clarified many things to me, but I am still a bit at a loss regarding the issue above. There is the following call in the memory circuit:

bus_mapping_lookup(
⠀⠀compress(
⠀⠀⠀⠀"memory",
⠀⠀⠀⠀gc,
⠀⠀⠀⠀key,
⠀⠀⠀⠀val,
⠀⠀⠀⠀memory_op
⠀⠀)
)

Isn't everyting we need to do here just to build a table? I guess we don't need compress function (this is taken care of by Halo2)?