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

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

Closed
ed255 opened this issue May 3, 2023 · 4 comments · Fixed by #1394 or #1441
Closed

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

ed255 opened this issue May 3, 2023 · 4 comments · Fixed by #1394 or #1441
Assignees
Milestone

Comments

@ed255
Copy link
Member

ed255 commented May 3, 2023

Before refactoring all circuits to work with word lo/hi we need to create new utilities, types and abstractions for all circuits to deal with Words in a clean way.

This is a non-exhaustive list of topics to cover:

  • A type to encapsulate 2 columns that represent the word_lo and word_hi
  • A type to encapsulate 2 Cells that represent the word_lo and word_hi
  • ConstraintBuilder functions / Gadget to generate constraints like
    • constraint two words are equal
    • test if two words are equal
    • constraint a word is zero
    • test if a word is zero
    • test if a word is not zero
    • test if a word is smaller than another one
    • etc.
  • Helper utilities to go from:
    • word to bytes
    • bytes to word
    • word to limbs
    • limbs to word

Some months ago Haichen started looking into this, we can use his previous unfinished work as inspiration:

@hero78119
Copy link
Member

hero78119 commented May 17, 2023

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

  • initial version of util function
  • detail documentation + unittest to cover
  • compile pass first
  • all unittest pass
  • 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

hero78119 added a commit that referenced this issue May 17, 2023
### Description

[_PR description_]

### Issue Link


#1388

### Type of change

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

### Contents
- [x] define general type `Word` and `WordLimbs` along with util
function to replace RandomLinearCombination in `word.rs`
- [x] 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
#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
<hr>

---------
@hero78119
Copy link
Member

Closed and marked as done, optimisation will be raised in another ticket

@ChihChengLiang
Copy link
Collaborator

@hero78119 I see #1427 is still linked to this PR. Would you like us to link #1427 to other tickets?

@hero78119
Copy link
Member

@hero78119 I see #1427 is still linked to this PR. Would you like us to link #1427 to other tickets?

thanks for reminding, linked to #1487 instead

@ChihChengLiang ChihChengLiang removed a link to a pull request Jun 21, 2023
4 tasks
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.