Skip to content
This repository has been archived by the owner on Jul 5, 2024. It is now read-only.

word hi/lo utilities (initial version) #1394

Conversation

hero78119
Copy link
Member

@hero78119 hero78119 commented May 8, 2023

Description

[PR description]

Issue Link

#1388

Type of change

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

Contents

  • define general type Word and WordLimbs along with util function to replace RandomLinearCombination in word.rs
  • evm util function/common gadgets switch to new Word type
  • (Ongoing, partially done) EVM circuit switch to new Word type

Pending List

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

  • evm circuit switch to word type. It will be finished in another evm circuit pr. In this pr have incomplete evm circuit work, just to verify the usage of utility functions.
  • optimise cell comsumption, e.g. U64 type, such as gas type which just need 8 bytes cells range check. For example, refer CommonCallGadget gas type.
  • support byte16 range check
  • review common_gadget all range check.
  • review reversible info range check
  • review word::from_lo_uncheck range check
  • optimise range check for lookup read, see comment word hi/lo utilities (initial version) #1394 (comment)
  • replace Word<Expression<F>> with generic WordExpr<F> in lookup so can save to_word() conversion in most of gadget
  • static assertion on const generic check
  • review memory to assure if length is 0 then offset can be larger than u64

How Has This Been Tested?

  • compile pass first
  • all unittest pass

@github-actions github-actions bot added the crate-zkevm-circuits Issues related to the zkevm-circuits workspace member label May 8, 2023
@hero78119 hero78119 marked this pull request as draft May 8, 2023 04:29
@hero78119 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 hero78119 changed the title WIP word hi/lo utilization WIP word hi/lo utilities May 8, 2023
@hero78119
Copy link
Member Author

hero78119 commented May 8, 2023

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

Comment on lines 54 to 64
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(),
));
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 :)

Copy link
Member Author

@hero78119 hero78119 May 12, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Comment on lines 316 to 319
} => [
vec![id.clone(), field_tag.clone(), index.clone()],
value.limbs.to_vec().clone(),
]
.concat(),
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

@hero78119 hero78119 May 15, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 Outdated Show resolved Hide resolved
)
}

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

)
}

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add documentation with TODO to implement 16 bits range check soon

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

@ed255 ed255 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

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();
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Member

ed255 commented May 8, 2023

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.

}
}

// `Word`, special alias for Word2.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

@KimiWu123 KimiWu123 May 10, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 :)

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

ed255 commented May 9, 2023

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 hero78119 changed the base branch from main to word-lo-hi May 9, 2023 14:45
@hero78119
Copy link
Member Author

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
Copy link
Member

adria0 commented May 10, 2023

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

@hero78119
Copy link
Member Author

hero78119 commented May 10, 2023

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

WordLimbs::<Expression<F>, N2>::new(limbs)
}

pub fn to_word(&self) -> Word<Expression<F>> {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

And instead to_wordlimbs(), use limbs_expr()

Copy link
Member Author

@hero78119 hero78119 May 12, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@github-actions github-actions bot added the crate-keccak Issues related to the keccak workspace member label May 15, 2023
@hero78119 hero78119 marked this pull request as ready for review May 15, 2023 11:53
@hero78119
Copy link
Member Author

Excepted for documentation, other issues are addressed :P

@hero78119
Copy link
Member Author

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

@hero78119 hero78119 changed the title WIP word hi/lo utilities word hi/lo utilities (initial version) May 15, 2023
@hero78119
Copy link
Member Author

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

@hero78119
Copy link
Member Author

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

@hero78119 hero78119 mentioned this pull request May 16, 2023
8 tasks
@hero78119 hero78119 merged commit f749c6d into privacy-scaling-explorations:word-lo-hi May 17, 2023
@adria0 adria0 mentioned this pull request May 24, 2023
4 tasks
@ed255 ed255 linked an issue May 31, 2023 that may be closed by this pull request
hero78119 added a commit that referenced this pull request Jun 20, 2023
### 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 <[email protected]>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
crate-keccak Issues related to the keccak workspace member crate-zkevm-circuits Issues related to the zkevm-circuits workspace member
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Write Word utilities, types and abstractions for word lo/hi
4 participants