word hi/lo utilities (initial version) #1394

hero78119 · 2023-05-08T04:29:26Z

Description

[PR description]

Issue Link

Type of change

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

Rationale

Defined WordN, where N represent number of limbs, where the word size is EVM word 256bits. For instance, Word4 means 4 limbs, each limb 64 bits. Giving 2 word word_n1, word_n2, and n1 % n2 = 0, There are util function to convert n1 to n2. Words related utility are defined in new file word.rc

constraint builder also introduce few util apis

util functions to support query WordN cells. For N=32, limb cell integrate with byte lookup. For N < 32, need caller to have range check carefully.
word equality check
separate read/write api to hint which need careful range check

Range check strategy

State circuit will assure read value match with last write. Therefore, for lookup table except stack.pop, such as txtable, blocktable, callcontext, we need to assure value write got proper range check carefully. For read part, range check can be skip by purpose.

Special note for stack.pop, since some arithmetcis operation might need special range for operand from stack, and stack can be any value. Therefore, some case read part also need range check carefully, unless it's just some equality check, like CmpGadget, where the value range is not matter, such kind of operation can skip range check.

TODO Any other case need range check during read?

Pending tasks

How Has This Been Tested?

compile pass first
all unittest pass

hero78119 · 2023-05-08T07:22:56Z

Hi @ed255 and @adria0

Tried to modify few places as examples to show what the utilities api looks like. Please kindly take a first look and review, see whether the api usage fulfill the expectation.

One thing I am not pretty sure is what the best practice to do range check. So far the design follows Word16 (means 16 limbs, each limbs 2 bytes) should be widely use, especially when get word from constriantbuilder we should use cb.query_word16() then do most of operation on word16 directly. In constriantbuilder, we can have a new enum Lookup2Bytes and cb.query_word16() will have range check naturally.

Notes, right now cb.query_word32 is used in most of place, because haven't introduce 16 bits lookup. Once introduce 16 bits range lookup, we can call cb.query_word16() instead.

In current design, to_word api by default convert to Word2. This design can help to minimize the cost in the future if we change to smaller field size, e.g. goldilock 64 bit, then we just need to modify to_word and default Word type with Word4, and all the codebase do not need to change.

Table field will always follow Word and during lookup, all the wordlimbs > 2 will call to_word to convert to Word type

ed255 · 2023-05-08T12:36:50Z

zkevm-circuits/src/evm_circuit/execution/add_sub.rs

+        cb.stack_pop(Word::select(
+            is_sub.expr().0,
+            c.expr().to_word(),
+            a.expr().to_word(),
+        ));
+        cb.stack_pop(b.expr().to_word());
+        cb.stack_push(Word::select(
+            is_sub.expr().0,
+            a.expr().to_word(),
+            c.expr().to_word(),
+        ));


This opcode does POP on a and b, and PUSH on c.
This means that a and b are read and c is written.
The StateCircuit guarantees that any read is consistent with the previous write. From this we can optimize out the range checks on the reads, and only leave the range checks on the writes!

So we can directly read a and b from the stack and assume their corresponding lo,hi are 128 bits each. From this we create c and prove that c.lo and c.hi are 128 bit each, and then write c to the stack.

In this case the native format for the AddWordsGadget is lo, hi so I think there's no need to express a and b as 8 bit limbs at any time. AddWordsGadget doesn't do any range check on sum.lo, sum.hi so those ones do need to be split into limbs to guarantee that sum.lo, sum.hi are 128 bit each.

Note that this is an optimization, so we may apply it in the future. I see that you also implemented cb.query_word so, so this is just a comment :)

Hi @ed255 This is a good consolidation for when should do range check! And it definitely can be applied on other lookup with tag, since all value should be checked during write.

Just have small add-on, this add-sub.rs is pretty typical that we can just assume value pop from stack it's low/hi is within 128 bits and fit optimisation! But there are some other edge cases, for example operand pop from stack must be an address, therefore range should be within 20 bytes. I applied partial optimisation on address type as well in latest commits. We can apply same tricks on other type, such as U64 range etc.

ed255 · 2023-05-08T12:44:19Z

zkevm-circuits/src/evm_circuit/table.rs

+            } => [
+                vec![id.clone(), field_tag.clone(), index.clone()],
+                value.limbs.to_vec().clone(),
+            ]
+            .concat(),


Another option for this would be:

vec![id.clone(), field_tag.clone(), index.clone(), value.lo().clone(), value.hi().clone()]

What do you think about this form?

I like value.lo().clone(), value.hi().clone() style, just I was thinking if using lo(), hi() here then once change to different field we need to modify this part. Although it just small change though.

@ed255 I realized there are table.annotations() which still hardcode column to annotation string. So my methodology doenst really help to generalized. I adapt your method 👍 and updated in latest commit

ed255 · 2023-05-08T12:48:51Z

zkevm-circuits/src/evm_circuit/util.rs

+        offset: usize,
+        bytes: Option<[u8; N1]>,
+    ) -> Result<Vec<AssignedCell<F, F>>, Error> {
+        assert_eq!(N1 % N, 0); // assure N|N1


Maybe we can use https://docs.rs/static_assertions/latest/static_assertions/ for these assertions that should be performed at compile time?

Yes I plan to use this. However, static_assertion this library do not work on const generic, see issue here
nvzqz/static-assertions#40
I will try the workaround later.

zkevm-circuits/src/evm_circuit/util/constraint_builder.rs

ed255 · 2023-05-08T12:52:01Z

zkevm-circuits/src/evm_circuit/util/constraint_builder.rs

+        )
+    }
+
+    pub(crate) fn query_word4<const N: usize>(&mut self) -> Word4<Cell<F>> {


Document that the resulting word is not range checked. (each limb is not guaranteed to be 64 bits)

ed255 · 2023-05-08T12:52:14Z

zkevm-circuits/src/evm_circuit/util/constraint_builder.rs

+        )
+    }
+
+    pub(crate) fn query_word16<const N: usize>(&mut self) -> Word16<Cell<F>> {


Document that the resulting word is not range checked yet. (each limb is not guaranteed to be 16 bits)

Add documentation with TODO to implement 16 bits range check soon

zkevm-circuits/src/evm_circuit/util/constraint_builder.rs

zkevm-circuits/src/evm_circuit/execution/logs.rs

ed255

Overall the abstractions look really good to me! I see that you focused a lot on the EVM Circuit.
For example, all the word types are in zkevm-circuits/src/evm_circuit/util.rs but they will also be useful outside of the evm_circuit. I think a next step will be to focus on how these types can be used in other circuits :)

The other part that needs to be explored is the tables and lookups. I see you changed zkevm-circuits/src/table.rs a bit. I'm looking forward to how these abstractions can be used on a circuit that contains a table that the evm circuit looks up to.

zkevm-circuits/src/evm_circuit/util/math_gadget/is_equal_word.rs

ed255 · 2023-05-08T13:01:54Z

zkevm-circuits/src/evm_circuit/util/math_gadget/mul_add_words.rs

-            let idx = (trunk * 8) as usize;
-            a_limbs.push(from_bytes::expr(&a.cells[idx..idx + 8]));
-            b_limbs.push(from_bytes::expr(&b.cells[idx..idx + 8]));
+        let word4_a: Word4<Expression<F>> = a.expr().to_wordlimbs();


This looks really nice! I think having these gadgets take Word32 and then converting to a different number of limbs as necessary makes the refactor look very clean!

ed255 · 2023-05-08T13:07:59Z

Also I think it's a very good idea for now to mechanically translate every WordRLC (from query_word_rlc) to Word32. That should work all the time, and we can focus on some optimizations like #1394 (comment) in the future. No need to worry about it now.

zkevm-circuits/src/evm_circuit/util/constraint_builder.rs

zkevm-circuits/src/evm_circuit/execution/logs.rs

KimiWu123 · 2023-05-09T05:43:41Z

zkevm-circuits/src/evm_circuit/util.rs

+    }
+}
+
+// `Word`, special alias for Word2.


I'm a little bit confused, I thought the number 2 stands for the number of byte. So, Word2 is a 2 bytes data structure, isn't it? And from my understanding, word hi/lo is to represent 32 bytes evm word. Could you please explain it more? thanks

I moved the new Word type to new file word.rs, and add simple comment.

WordN means splits 256 bit into N chunk. Each chunk is also called limb. (would chunk be better naming 😢 ?)

Therefore, Word2 means 2 limb, each with 128bit

haha, got it. I thought the other way around. I thought Word32 includes 32 limbs and each limb is 1 byte and Word2 is a 2 bytes data. But I get your idea.

What if we name these types like this,

Word and Word128 stands for 2 x 128 bits limbs

Word64 stands for 4 x 64 bits limbs

Word16 stands for 16 x 16 bits limbs

Word8 stands for 32 x 8 bits limbs

Just like uintN in solidity, the following N stands for bit numbers

I want to say that I like the original nomenclature that @hero78119 proposed (where N is the number of limbs).
If N means number of bits, I find it easier to mistake it for the word size, like the uintN example; but that's not the case: all Words are 32 bytes in Ethereum.
Also I think it's more direct to see WordN and then inspect the type and see an array of length N.
The other way would be inspecting the type and seeing an array of length 256 / N

I'm in the side of @KimiWu123, I think is more understandable (at least, for me).
Anyway, the other option also works for me, of course :)

zkevm-circuits/src/evm_circuit/util.rs

zkevm-circuits/src/evm_circuit/util/common_gadget.rs

ed255 · 2023-05-09T14:42:30Z

BTW, currently this PR targets the main branch. Merging this to main will probably not be possible due to many tests not passing (or even the code not compiling). I created a word-lo-hi branch that we can use to keep the development of the word lo/hi refactor, so this PR could be updated to target that branch; and once people start working on refactoring the circuits, they can also target that branch. This way we can still review everything via PRs, while the CI is not passing, without breaking main.

hero78119 · 2023-05-10T02:31:48Z

Also I think it's a very good idea for now to mechanically translate every WordRLC (from query_word_rlc) to Word32. That should work all the time, and we can focus on some optimizations like #1394 (comment) in the future. No need to worry about it now.

After consolidate concept for range check on write timing only, everything become more clear. We can apply optimisation for read part soon 👍

adria0 · 2023-05-10T11:31:06Z

Why not rename Word to Word2? I think that is more consistent with Word4, Word32, etc..

hero78119 · 2023-05-10T11:56:50Z

Why not rename Word to Word2? I think that is more consistent with Word4, Word32, etc..

'Word' is like default

later we can apply dereference if change to smaller fields , for example goldilocks, which is word4 will be default. Have default word make it happend without need to change most of the codebaae

adria0 · 2023-05-10T17:04:53Z

zkevm-circuits/src/util/word.rs

+        WordLimbs::<Expression<F>, N2>::new(limbs)
+    }
+
+    pub fn to_word(&self) -> Word<Expression<F>> {


What about .expr() instead to_word() ? It's how now works with stack_push/stack_pop

And instead to_wordlimbs(), use limbs_expr()

to_word is a special alias for to_word2. Here source and destination already be expression.

We have word_expr() which is implemented on Word<Cell> type already.

But thanks for the nice calls, I think to_wordN is better than to_wordlimbs. Will try to rename it

hero78119 · 2023-05-15T11:54:27Z

Excepted for documentation, other issues are addressed :P

hero78119 · 2023-05-15T15:32:09Z

Updated: just fix few obvious errors in common/math gadget 2a14cd3

hero78119 · 2023-05-15T16:09:06Z

Plan to have detail documentation on separated PR, so it wont block other task to start

hero78119 · 2023-05-16T04:53:22Z

Update: revamp few types and util, e.g. RwTable storage_key type to Word

### Description This PR is based on #1394 Need to merge #1394 first before review this. ### Issue Link #1379 ### Type of change - [x] Breaking change (fix or feature that would cause existing functionality to not work as expected) ### Contents - [x] fixed most of op compiling errors other than `callop.rs` and `begin_tx.rs`. - [x] fixed `callop.rs` and `begin_tx.rs` - [x] remove all compatible workaround `construct_new` under evm circuit - [x] unittest under evm circuit all pass `cargo test --features warn-unimplemented --features test --package zkevm-circuits --lib -- evm_circuit::execution::` - [x] fix few `word` gadgets generics to take `Word<T>` instead of `T` to restrict it flexibility, since it's non sense to put type not related to word - [x] remove most of `deprecated` api under evm circuits - [x] add IntDecomposition type as an alternative to RandomLinearComposition, with base 256 ### Cell utilization on main branch vs on word-lo-hi branch #### Storage_1 ``` Main: +-----------------------------------+------------------------------+-------------------------+ | "storage_1" total_available_cells | "storage_1" total_used_cells | "storage_1" Utilization (%) | +-----------------------------------+------------------------------+-------------------------+ | 25480 | 6482 | 25.4 | +-----------------------------------+------------------------------+-------------------------+ Word-lo-hi +-----------------------------------+------------------------------+-----------------------------+ | "storage_1" total_available_cells | "storage_1" total_used_cells | "storage_1" Utilization (%) | +-----------------------------------+------------------------------+-----------------------------+ | 24080 | 7078 | 29.4 | +-----------------------------------+------------------------------+-----------------------------+ ``` #### Storage_2 ``` Main +-----------------------------------+------------------------------+-------------------------+ | "storage_2" total_available_cells | "storage_2" total_used_cells | "storage_2" Utilization | +-----------------------------------+------------------------------+-------------------------+ | 1456 | 467 | 32.1 | +-----------------------------------+------------------------------+-------------------------+ Word-lo-hi +-----------------------------------+------------------------------+-----------------------------+ | "storage_2" total_available_cells | "storage_2" total_used_cells | "storage_2" Utilization (%) | +-----------------------------------+------------------------------+-----------------------------+ | 1376 | 14 | 1.0 | +-----------------------------------+------------------------------+-----------------------------+ ``` #### Byte_lookup ``` Main  +-------------------------------------+--------------------------------+---------------------------+ | "byte_lookup" total_available_cells | "byte_lookup" total_used_cells | "byte_lookup" Utilization | +-------------------------------------+--------------------------------+---------------------------+ | 8736 | 6786 | 77.7 | +-------------------------------------+--------------------------------+---------------------------+ Word-lo-hi +-------------------------------------+--------------------------------+-------------------------------+ | "byte_lookup" total_available_cells | "byte_lookup" total_used_cells | "byte_lookup" Utilization (%) | +-------------------------------------+--------------------------------+-------------------------------+ | 8256 | 6566 | 79.5 | +-------------------------------------+--------------------------------+-------------------------------+ ``` --------- Co-authored-by: Wu Sung-Ming <wusm@sea.com>

github-actions bot added the crate-zkevm-circuits Issues related to the zkevm-circuits workspace member label May 8, 2023

hero78119 marked this pull request as draft May 8, 2023 04:29

hero78119 force-pushed the feat/word_hi_lo_utilities branch 3 times, most recently from 91e8968 to 5cac031 Compare May 8, 2023 05:11

hero78119 changed the title ~~WIP word hi/lo utilization~~ WIP word hi/lo utilities May 8, 2023

hero78119 force-pushed the feat/word_hi_lo_utilities branch from 5cac031 to 2ed021b Compare May 8, 2023 07:00

ed255 reviewed May 8, 2023

View reviewed changes

hero78119 commented May 8, 2023

View reviewed changes

zkevm-circuits/src/evm_circuit/execution/logs.rs Outdated Show resolved Hide resolved

ed255 reviewed May 8, 2023

View reviewed changes

zkevm-circuits/src/evm_circuit/util/constraint_builder.rs Outdated Show resolved Hide resolved

zkevm-circuits/src/evm_circuit/util/constraint_builder.rs Outdated Show resolved Hide resolved

KimiWu123 reviewed May 9, 2023

View reviewed changes

zkevm-circuits/src/evm_circuit/execution/logs.rs Outdated Show resolved Hide resolved

KimiWu123 reviewed May 9, 2023

View reviewed changes

zkevm-circuits/src/evm_circuit/util.rs Outdated Show resolved Hide resolved

KimiWu123 reviewed May 9, 2023

View reviewed changes

zkevm-circuits/src/evm_circuit/util/common_gadget.rs Outdated Show resolved Hide resolved

hero78119 force-pushed the feat/word_hi_lo_utilities branch 5 times, most recently from 3664c37 to 8585ee7 Compare May 9, 2023 14:40

hero78119 force-pushed the feat/word_hi_lo_utilities branch from 8585ee7 to 0e3e310 Compare May 9, 2023 14:44

hero78119 changed the base branch from main to word-lo-hi May 9, 2023 14:45

hero78119 force-pushed the feat/word_hi_lo_utilities branch from 49d408c to 34fae76 Compare May 10, 2023 02:11

adria0 reviewed May 10, 2023

View reviewed changes

Wu Sung-Ming added 5 commits May 15, 2023 18:01

constraint builder support query memory address

100b262

codehash to word expr

3b10282

Word support add_uncheck

21686d9

clean up necessary generic and refine utility function

5bcf925

better generic design

b189aad

hero78119 force-pushed the feat/word_hi_lo_utilities branch from e9faa3d to b189aad Compare May 15, 2023 11:49

github-actions bot added the crate-keccak Issues related to the keccak workspace member label May 15, 2023

renaming

9b451b6

hero78119 marked this pull request as ready for review May 15, 2023 11:53

tuning util function

2a14cd3

revamp table column to lo/hi

e4425eb

hero78119 force-pushed the feat/word_hi_lo_utilities branch from f4bb10d to e4425eb Compare May 15, 2023 16:05

hero78119 changed the title ~~WIP word hi/lo utilities~~ word hi/lo utilities (initial version) May 15, 2023

revamp types and utilities

4ce6c76

Wu Sung-Ming added 2 commits May 16, 2023 14:55

storage_key type to word

92849db

fix common_gadget

cca6728

hero78119 force-pushed the feat/word_hi_lo_utilities branch from e4b9464 to cca6728 Compare May 16, 2023 06:56

hero78119 mentioned this pull request May 16, 2023

[word-lo-hi] evm circuit #1411

Merged

8 tasks

Wu Sung-Ming added 2 commits May 16, 2023 18:38

memory_word_size to Word

bd5d09d

LtWordGadget generic

d17fd55

hero78119 mentioned this pull request May 17, 2023

Write Word utilities, types and abstractions for word lo/hi #1388

Closed

add min_max_word gadget

f850396

hero78119 merged commit f749c6d into privacy-scaling-explorations:word-lo-hi May 17, 2023

adria0 mentioned this pull request May 24, 2023

Statecircuit lo hi #1431

Closed

4 tasks

ed255 linked an issue May 31, 2023 that may be closed by this pull request

Write Word utilities, types and abstractions for word lo/hi #1388

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

word hi/lo utilities (initial version) #1394

word hi/lo utilities (initial version) #1394

hero78119 commented May 8, 2023 •

edited

Loading

hero78119 commented May 8, 2023 •

edited

Loading

ed255 May 8, 2023

hero78119 May 12, 2023 •

edited

Loading

ed255 May 8, 2023

hero78119 May 8, 2023

hero78119 May 15, 2023 •

edited

Loading

ed255 May 8, 2023

hero78119 May 8, 2023

ed255 May 8, 2023

ed255 May 8, 2023

hero78119 May 9, 2023

ed255 left a comment

ed255 May 8, 2023

ed255 commented May 8, 2023 •

edited

Loading

KimiWu123 May 9, 2023

hero78119 May 9, 2023

KimiWu123 May 10, 2023 •

edited

Loading

KimiWu123 May 10, 2023

ed255 May 10, 2023

adria0 May 10, 2023

ed255 commented May 9, 2023

hero78119 commented May 10, 2023

adria0 commented May 10, 2023

hero78119 commented May 10, 2023 •

edited

Loading

adria0 May 10, 2023

hero78119 May 12, 2023 •

edited

Loading

hero78119 commented May 15, 2023

hero78119 commented May 15, 2023

hero78119 commented May 15, 2023

hero78119 commented May 16, 2023

word hi/lo utilities (initial version) #1394

word hi/lo utilities (initial version) #1394

Conversation

hero78119 commented May 8, 2023 • edited Loading

Description

Issue Link

Type of change

Contents

Rationale

Range check strategy

Pending tasks

How Has This Been Tested?

hero78119 commented May 8, 2023 • edited Loading

Choose a reason for hiding this comment

hero78119 May 12, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hero78119 May 15, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ed255 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ed255 commented May 8, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

KimiWu123 May 10, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ed255 commented May 9, 2023

hero78119 commented May 10, 2023

adria0 commented May 10, 2023

hero78119 commented May 10, 2023 • edited Loading

Choose a reason for hiding this comment

hero78119 May 12, 2023 • edited Loading

Choose a reason for hiding this comment

hero78119 commented May 15, 2023

hero78119 commented May 15, 2023

hero78119 commented May 15, 2023

hero78119 commented May 16, 2023

hero78119 commented May 8, 2023 •

edited

Loading

hero78119 commented May 8, 2023 •

edited

Loading

hero78119 May 12, 2023 •

edited

Loading

hero78119 May 15, 2023 •

edited

Loading

ed255 commented May 8, 2023 •

edited

Loading

KimiWu123 May 10, 2023 •

edited

Loading

hero78119 commented May 10, 2023 •

edited

Loading

hero78119 May 12, 2023 •

edited

Loading