State circuit #23

miha-stopar · 2021-07-23T09:20:44Z

File memory.rs renamed into state.rs and made it flexible enough to cover the stack circuit too. Also, range value tables (global_counter and address) now load the maximum value too - consequently, for example, now you specify 1023 for max address in the stack circuit and not 1024.

src/gadget/is_zero.rs

src/state_circuit/state.rs

…it case too

therealyingtong · 2021-07-29T14:05:55Z

Force-pushed to rebase on main.

therealyingtong · 2021-07-29T14:12:05Z

src/state_circuit/state.rs

+
+/// In the state proof, memory operations are ordered first by address, and then by global_counter.
+/// Memory is initialised at 0 for each new address.
+/// Memory is a word-addressed byte array, i.e. a mapping from a 253-bit word -> u8.


I'm not sure if we're still doing 253-bit addresses, or using the full 256-bit instead. Let's add a TODO here.

Suggested change

/// Memory is a word-addressed byte array, i.e. a mapping from a 253-bit word -> u8.

/// Memory is a word-addressed byte array, i.e. a mapping from a 253-bit word -> u8.

/// TODO: Confirm if we are using 253- or 256-bit memory addresses.

I think that when you use the compressed form the address will be a253 number its just the random linear combination of the 8 bit words making up the 256 bit address.

If we can assume a circuit memory size hard bound (say 2**24), it would be easier to use actual value instead of random linear combination for memory index.

For example, when one is going to do like mload(250), we will need to do memory bus mapping lookup in range (250, 250 + 1, 250 + 2, ..., 281) from byte to byte. If we use random linear combination, then some of indexes would have the first byte which exceeds 256 and produces carry to the second byte, which makes the random linear combination harder to calculate (hard do that without requiring intermediate witness).

If we assume a hard bound, we just take first 3 bytes and recompose it to 2**24 value to lookup memory, which seems to be easier, but is incompatible with current evm which doesn't has any hard bound.

Yes this makes sense. Hard bound means we can't overflow 2**253 memory elements.

I was thinking if we used compressed form we would be able to avoid a decompression of the index when it comes from the stack. But you have to decompress to get the ordering right anyway so probably good to use the decompressed form.

253 bit width range come from Pasta Curves ?

It comes from the bn254 curve we are using. We replace Pasta curve with bn254 and halo2 polynomial commitment with kate polynomial commitment.

you mean code "pasta_curves::arithmetic::FieldExt;" has been with bn254 or happens on other branch ?

I think it happened on another branch but that is our plan.

The BN254 / KZG fork of halo2 is on @kilic's branch: https://github.com/kilic/halo2/tree/kzg

@therealyingtong I see & Thx

src/state_circuit/state.rs

src/state_circuit.rs

src/state_circuit/state.rs

therealyingtong · 2021-07-29T15:29:06Z

src/state_circuit/state.rs

+                // We pad all remaining memory rows to avoid the check at the first unused row.
+                // Without padding, (address_cur - address_prev) would not be zero at the first unused row
+                // and some checks would be triggered.


TODO: We eventually want to exclude the padding rows from the bus mapping lookup.

gaswhat · 2021-08-04T05:04:55Z

src/state_circuit/state.rs

+            // If address_cur != address_prev, this is an `init`. We must constrain:
+            //      - values[0] == [0]
+            //      - flags[0] == 1
+            //      - global_counters[0] == 0


Why does global_counter need to be 0 for a new address? Isn't global_counter supposed to keep increasing across all addresses?

For a new call context, the global_counter should be init with 0.

@spartucus This is not a new call context. It just moves to check the next memory/stack address.

The init at each new address is effectively a "dummy write" of value = 0. This handles the case where the first operation at an address is a read. Since this address has never been written to, the first read should return 0. (This "dummy write" isn't a real operation and doesn't affect the global_counter.)

In terms of circuit constraints: note that the q_read case involves querying the value on the previous row value_prev. Without a dummy init row, the first read would end up querying the last value from the previous address.

(Thanks @han0110 for explaining this to me.)

Thanks @therealyingtong!

I asked @han0110 a couple of related questions - global_counter can be set to 0 in the init operation as this is not put in the bus mapping. We don't check global_counter uniqueness in the state circuit - this will be done in the evm circuit. In the evm circuit, we will (1) lookup global_counter one by one and (2) check the degree of bus mapping is equal to the number of operations. If a malicious prover skips a write, (1) will fail. If a malicious prover inserts a non-existing write, (2) fails.

@gaswhat: I think global_counter doesn't need to be increasing across all addresses, it only needs to be ordered increasingly for each address.

Thanks for the explanation @therealyingtong @miha-stopar. I missed the init row at each new address previously.

I have a follow up question. Could we skip this init row for each new address to save some rows? It seems to me a bit redundant. I think we just need to prove the first row of a new address must be a write operation. Should be enough?

@gaswhat I removed stack init rows in #1bdbe5d. This requires some more code and some more gates, but indeed we save quite some rows. I left the memory init rows in there as they seem to be required. I will try to summarize @han0110 explanation below:

Memory init rows are needed to mimic the EVM interpreter's behaviour. For example, when memory is empty and mload(32) is executed (which returns memory[32..64]), EVM expands memory size to 64 and returns 0. Thus, in state circuit we allocate to 0 all addresses that are used to be compatible with EVM.

Indeed, we don't have to do such things for stack operations. Thanks for your comments!

barryWhiteHat · 2021-08-10T13:39:06Z

@miha-stopar to make memory byte addressable is all that we need to do is apply a range check on every element we write to memory being 1 byte ?

If we do this we know that each address maps to a single byte. We would also have to change mstore to access 32 bus mapping element in evm proof.

miha-stopar · 2021-08-10T16:39:25Z

@miha-stopar to make memory byte addressable is all that we need to do is apply a range check on every element we write to memory being 1 byte ?

If we do this we know that each address maps to a single byte. We would also have to change mstore to access 32 bus mapping element in evm proof.

@barryWhiteHat yes, I plan to add this constraint as it's in the specs. Was having some problems with switching between memory and stack operations - I still have a couple of things to add, but it works now.

therealyingtong

LGTM! some non-blocking nits and questions.

therealyingtong · 2021-09-21T07:22:59Z