-
Notifications
You must be signed in to change notification settings - Fork 857
word hi/lo utilities (initial version) #1394
word hi/lo utilities (initial version) #1394
Conversation
91e8968
to
5cac031
Compare
5cac031
to
2ed021b
Compare
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
In current design, Table field will always follow |
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(), | ||
)); |
There was a problem hiding this comment.
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 :)
There was a problem hiding this comment.
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.
} => [ | ||
vec![id.clone(), field_tag.clone(), index.clone()], | ||
value.limbs.to_vec().clone(), | ||
] | ||
.concat(), |
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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 |
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.
) | ||
} | ||
|
||
pub(crate) fn query_word4<const N: usize>(&mut self) -> Word4<Cell<F>> { |
There was a problem hiding this comment.
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>> { |
There was a problem hiding this comment.
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)
There was a problem hiding this comment.
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
There was a problem hiding this 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.
zkevm-circuits/src/evm_circuit/util/math_gadget/is_equal_word.rs
Outdated
Show resolved
Hide resolved
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(); |
There was a problem hiding this comment.
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!
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. |
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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
andWord128
stands for 2 x 128 bits limbsWord64
stands for 4 x64
bits limbsWord16
stands for 16 x16
bits limbsWord8
stands for 32 x8
bits limbs
Just like uintN
in solidity, the following N
stands for bit numbers
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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 :)
3664c37
to
8585ee7
Compare
BTW, currently this PR targets the |
8585ee7
to
0e3e310
Compare
49d408c
to
34fae76
Compare
After consolidate concept for range check on |
Why not rename |
'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 |
zkevm-circuits/src/util/word.rs
Outdated
WordLimbs::<Expression<F>, N2>::new(limbs) | ||
} | ||
|
||
pub fn to_word(&self) -> Word<Expression<F>> { |
There was a problem hiding this comment.
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()
There was a problem hiding this comment.
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
e9faa3d
to
b189aad
Compare
Excepted for documentation, other issues are addressed :P |
Updated: just fix few obvious errors in common/math gadget 2a14cd3 |
f4bb10d
to
e4425eb
Compare
Plan to have detail documentation on separated PR, so it wont block other task to start |
Update: revamp few types and util, e.g. RwTable |
e4b9464
to
cca6728
Compare
### 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]>
Description
[PR description]
Issue Link
#1388
Type of change
Contents
Word
andWordLimbs
along with util function to replace RandomLinearCombination inword.rs
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 fileword.rc
constraint builder also introduce few util apis
WordN
cells. For N=32, limb cell integrate with byte lookup. For N < 32, need caller to have range check carefully.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 valuewrite
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, likeCmpGadget
, where the value range is not matter, such kind of operation can skip range check.Pending tasks
gas
type which just need 8 bytes cells range check. For example, referCommonCallGadget
gas type.Word<Expression<F>>
with genericWordExpr<F>
in lookup so can saveto_word()
conversion in most of gadgetHow Has This Been Tested?