Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

docs: clean up documents #3

Open
wants to merge 9 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions module_classification.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@

Could be tackled in any order (modulo computational endpoints)

- SHAKIRA: trivial data storey to send data to some (gnark) circuit;
- BLAKEMODEXP: trivial data store to send data to some (gnark) ciruict;
- SHAKIRA: trivial data store to send data to some (gnark) circuit;
- BLAKEMODEXP: trivial data store to send data to some (gnark) circuit;
- LOG_DATA / LOG_INFO: trivial data stores to prepare data to send to RLP_TXN_RCPT (the transaction receipt module);
- ROM_LEX: nearly trivial internal logic; associates every nonempty bytecode with a unique identifier (CODE_FRAGMENT_INDEX); complex relationship with the HUB;
- ROM: somewhat complex internal logic; parses bytecode / initialization code; performs jumpdestination analysis; constructs push values;
Expand Down Expand Up @@ -44,7 +44,7 @@ Could be tackled in any order:
# Memory

- MXP: detects wildly out of bounds arguments for instructions that may trigger memory expansion; STATEFUL module (it provides e.g. the number of active words in memory for MSIZE);
- MMU: breaks complext memory instructions (MSTORE, MLOAD, MSTORE8, SHA3, RETURN, REVERT, CREATE's, COPY-instructions, ...) down into simpler custom ones;
- MMU: breaks complex memory instructions (MSTORE, MLOAD, MSTORE8, SHA3, RETURN, REVERT, CREATE's, COPY-instructions, ...) down into simpler custom ones;
- MMIO: executes the custom instructions prepared by the MMU; STATEFUL module;

# Hub
Expand Down
8 changes: 4 additions & 4 deletions notes/constraints.md
Original file line number Diff line number Diff line change
Expand Up @@ -33,15 +33,15 @@ Prefer looking ahead from the vantage point of CT_i = 0

And how do we verify a constraint ? (in the prover)

Data you want to constrain is commited to as the evaluations of polynomials over a certain FFT friendly subset of a field. Some coset of a multiplicative subgroup of the units of a field.
Data you want to constrain is committed to as the evaluations of polynomials over a certain FFT friendly subset of a field. Some coset of a multiplicative subgroup of the units of a field.

We have some fixed size rquirements, e.G. the cosets all have size 2^22. This is realistic for say HUB and RAM.
We have some fixed size requirements, e.G. the cosets all have size 2^22. This is realistic for say HUB and RAM.

What we prove on chain is the satisfaction of a SNARK circuit (of Plonk type) with fixed sizes that verifies a proof of our type (general huge constraint system.) It's a proof of a proof of a proof of a... (maybe 3 or 4 times). With every recursion step reduce size by a factor of sqrt(n). Vortex.

Not everything is of that circuit size.

When we verify an equatoin of the form
When we verify an equation of the form

A * B + C - D * E * F * G * H + 1 = 0 (must be true on the coset, call it Dom)

Expand All @@ -59,7 +59,7 @@ Note: Q has degree 4 * |Dom|
FFT is needed for 2 things:
- going from the evaluations to the coefficients
- what we commit to is the polynomial given by its coefficients
- to compute quotients effciently.
- to compute quotients efficiently.
- we first do FFTs on a larger domain of size 4 * |Dom|
- we deduce the evaluations of Q on that larger domain
- we do inverse FFT using these evaluations to get the coefficients Q so we can commit to it.
Expand Down
2 changes: 1 addition & 1 deletion notes/contexts.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@
- if transaction ≡ contract creation then during the TX_INIT phase there is 1 context row; that row initializes the deployment context; it is given as context number CN = 1 + h;
- if transaction ≡ message call then during the TX_INIT phase:
- if transaction call data = ∅ we do as with creation: there is 1 context row; that row initializes the deployment context ("root"); it is given as context number CN = 1 + h;
- if transaction call data ≠ ∅ then we define a fictitious parent context with CN = h (which will be nonzero) which is used solely to hold the transaction call data; we also initialization as above the execution context that will be the "root context" with CN = 1 + h;
- if transaction call data ≠ ∅ then we define a fictitious parent context with CN = h (which will be nonzero) which is used solely to hold the transaction call data; we also initialize as above the execution context that will be the "root context" with CN = 1 + h;
2 changes: 1 addition & 1 deletion notes/exception_profiles.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Our zk-evm knows the following exceptions with associated stack columns:
- OPCX: invalidOpCodeException:
- SUX: stack underflow exception: stack underflow exception
- SOX: stack overflow exception
- MXPX: memory expansion exeption (a subcase of the out of gas exception)
- MXPX: memory expansion exception (a subcase of the out of gas exception)
- OOGX: out of gas exception
- RDCX: RETURNDATACOPY exception
- JUMPX: invalid JUMP exception
Expand Down
14 changes: 7 additions & 7 deletions notes/hub tests.md
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
## CN_NEW purpose

CN_NEW: represents the context number of the context wherein the next instruction of the will be executed. Wether the execution context changes or remains the same ... depends on the CONTEXT_MAY_CHANGE flag i.e. CMC.
CN_NEW: represents the context number of the context wherein the next instruction of the will be executed. Whether the execution context changes or remains the same ... depends on the CONTEXT_MAY_CHANGE flag i.e. CMC.

Recall that
Recall that

```rust
XAHOY == true <=> [any exception occurs]
```
Expand All @@ -29,26 +29,26 @@ The idea is simple

### Back to CALLER

Under any of the following scenarios one shoud have CN_NEW == CALLER_CN:
Under any of the following scenarios one should have CN_NEW == CALLER_CN:
- [ ] if `InstructionFamily.HALTING`
- [ ] if `InstructionFamily.INVALID` Then CN_NEW == CALLER_CN
- [ ] if $\textsf{XAHOY}_{i} = 1$ Then CN_NEW == CALLER_CN

### Back to SELF

Under any of the following scenarios one shoud have CN_NEW == CN:
Under any of the following scenarios one should have CN_NEW == CN:
- [ ] If $\textsf{CMC}_{i} = 0$ Then must equal CN
- [ ] CREATE's
- [ ] no exception but abort
- [ ] no exception, no abort but $\textsf{FCOND}_{i} = 1$ (deployment address already has nonzero nonce or nonempty code)
- [ ] no exception, no abort but empty init code
- [ ] CALL's
- [ ] no exception but abort
- [ ] no exceptoin, no abort but call to precompile
- [ ] no exception, no abort but call to precompile

### Entering new context

Under any of the following scenarios one shoud have CN_NEW == HUB_STAMP + 1:
Under any of the following scenarios one should have CN_NEW == HUB_STAMP + 1:
- CALL: no exception, no abort, to != precompile
- CREATE: no exception, no abort and non empty init code

Expand All @@ -67,4 +67,4 @@ These tests pertain to $\texttt{EXTCODECOPY}$, $\texttt{EXTCODEHASH}$, $\texttt{
- [ ] $\texttt{EXTCODESIZE}$ returns 0
- [ ] This must be true even if there are several successive (failed) deployments at a given address.

**Note.** If an address is
**Note.** If an address is
4 changes: 2 additions & 2 deletions notes/prover_notes_account.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Account and storage management in the zkevm from the prover POV

The zkevm is able to prove internal consistency for account fields and storage values touched / read in a batch of transactions. In so doing it is able to identify when an account (or a storage key/value pair) is touched for the **first time** and when an account (or a storage value/key pair) is touched for the **last time** in the execution of said batch of transactions. Identifying these special "first" and "final" interactions with Linea state allows us extract the required state data and to update it accordingly. This identification happens in the "permuted domain" where access to the same account or storage key are listed contiguously and in chronological order.
The zkevm is able to prove internal consistency for account fields and storage values touched / read in a batch of transactions. In so doing it is able to identify when an account (or a storage key/value pair) is touched for the **first time** and when an account (or a storage value/key pair) is touched for the **last time** in the execution of said batch of transactions. Identifying these special "first" and "final" interactions with Linea state allows us extract the required state data and update it accordingly. This identification happens in the "permuted domain" where access to the same account or storage key are listed contiguously and in chronological order.

- [Account and storage management in the zkevm from the prover POV](#account-and-storage-management-in-the-zkevm-from-the-prover-pov)
- [Account Data](#account-data)
Expand Down Expand Up @@ -84,7 +84,7 @@ The rows of interest can be filtered out by means of FIRST_AOC[i] + FINAL_AOC[i]
- account/EXISTS
- account/EXISTS_NEW

These are bits that equal 1 if the account **exists**. Recall that the account associated with a particular address $a$ is said to not exist in the state $\sigma$ (and $\sigma[a] = \varnothing$) if
These are bits that equal 1 if the account **exists**. Recall that the account associated with a particular address $a$ is said not to exist in the state $\sigma$ (and $\sigma[a] = \varnothing$) if
- it has zero nonce i.e. $\sigma[a]_\text{n} = 0$
- it has zero balance i.e. $\sigma[a]_\text{b} = 0$
- it has empty code i.e. $\sigma[a]_\text{c} = \texttt{KECCAK}\big((\\;)\big)$
Expand Down
4 changes: 2 additions & 2 deletions notes/prover_notes_bytecode.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@

## Accessing byte code from Linea state

The byte code of an account **which exists in the Linea state** may be required to be loded if
The byte code of an account **which exists in the Linea state** may be required to be loaded if
- the address pointing to the account can be found among account rows of the HUB
- the underlying account **exists** and has **nonempty bytecode**
- the byte code is actually accessed either through
Expand Down Expand Up @@ -43,4 +43,4 @@ Byte code of an account with address _a_ may either

## Notes on addressing columns from different modules

To disambiguate column names that may occurr in several modules we use the following notation `module.COLUMN` to talk unambiguously about column `COLUMN` in the module called `module`. We remind the reader that we also have special notation for multiplexing columns whereby (e.g. in the HUB) we may speak of a column belonging to the perspective e.g. account with name e.g. BALANCE and address it as `account/BALANCE`. If this column interacts with columns from other modules we may apply both conventions and speak say of column `hub.stack/STACK_ITEM_VALUE_HI_4` to speak of the column `STACK_ITEM_VALUE_HI_4` belonging to the `stack` perspective of the `hub` module.
To disambiguate column names that may occur in several modules we use the following notation `module.COLUMN` to talk unambiguously about column `COLUMN` in the module called `module`. We remind the reader that we also have special notation for multiplexing columns whereby (e.g. in the HUB) we may speak of a column belonging to the perspective e.g. account with name e.g. BALANCE and address it as `account/BALANCE`. If this column interacts with columns from other modules we may apply both conventions and speak say of column `hub.stack/STACK_ITEM_VALUE_HI_4` to speak of the column `STACK_ITEM_VALUE_HI_4` belonging to the `stack` perspective of the `hub` module.
6 changes: 3 additions & 3 deletions notes/prover_notes_storage.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ Like for account data we use an acronym **scp** for "storage consistency permuta
3. within (reordered) storage-rows, rows are ordered as follows
- account addresses are listed in ascending order
- among (reordered) storage-rows with the same address storage keys are listed in ascending order
- amont (reordered) storage-rows with the same address and storage key, rows are listed in "chronological" order
- among (reordered) storage-rows with the same address and storage key, rows are listed in "chronological" order

**Note.** We refer the reader to the note on account consistency from the prover POV for the explanation of what constitutes a (reordered) storage-row.

Expand All @@ -25,7 +25,7 @@ The Arithmetization will provide the following columns
- `false` on all other (reordered) rows
- binary columns FIRST_KOC, FINAL_KOC
- The acronym `KOC` stands for "(storage) key occurrence."
- both are false on (reordred) rows that aren't (reordered) storage-rows
- both are false on (reordered) rows that aren't (reordered) storage-rows
- FIRST_AOC lights up on the first (reordered) storage-row featuring some given address and some given storage key
- FINAL_AOC lights up on the final (reordered) storage-row featuring some given address and some given storage key
- both may be on the same row if a particular storage slot is only viewed once (e.g. a single (unreverted) SLOAD or a single (unreverted) SSTORE)
Expand Down Expand Up @@ -77,4 +77,4 @@ The above can happen with a SELFDESTRUCT (it's the only way.)
**Account redeployment**
- if an account originally existed in state and ends up after the batch of transaction with acp_account/DEPLOYMENT_NUMBER_INFTY ≠ 0 then all original values in storage must be discarded, regardless of whether any storage values were required during execution.

The above can happen for instance if an account was SELFDESTRUCT'ed in some transaction T and in a later transction T' (same batch of tx's) redeployed (the original account was created with a CREATE2 so redeployments at the same address are possible.
The above can happen for instance if an account was SELFDESTRUCT'ed in some transaction T and in a later transaction T' (same batch of tx's) redeployed (the original account was created with a CREATE2 so redeployments at the same address are possible.
6 changes: 3 additions & 3 deletions notes/stipend.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@

The purpose of the present `STI` module is to carry out the computation producing the gas stipend provided to any context spawned through a CALL-type instruction or a CREATE-type instruction.

**Note.** The stipend itself is already claimed (without proof) in the `hub` (or will be, once the update to the `hub` is implemented.) For justficiation the `hub` will lookup the computaiton in the STI module, thereby justify the associated values which the `hub` merely claims. Note furthermore that the present module is stateless.
**Note.** The stipend itself is already claimed (without proof) in the `hub` (or will be, once the update to the `hub` is implemented.) For justification the `hub` will lookup the computation in the STI module, thereby justify the associated values which the `hub` merely claims. Note furthermore that the present module is stateless.

## High level specification

Expand All @@ -31,7 +31,7 @@ The following are columns that will be imported from the HUB. All of them are tr
- GAS_UPDT: gas amount available to the execution context just prior to dealing with the current CALL-type or CREATE-type instruction
- GAS_COST: sum of all upfront gas costs associated with the instruction (e.g. static cost, memory expansion cost, hashing cost for CREATE2, account creation cost for CALL-type instruction whose recipient account doesn't exist in the state, warmth cost, value transfer cost ...)
- GAS_HI, GAS_LO: required only for CALL-type instructions, 256 bit stack argument containing the 'max gas stipend' parameter $\mu{s}\big[0\big]$ of the instruction
- VALUE_HI, VALUE_LO: required for CALL-type isntructions that take a value parameter (i.e. CALL and CALLCODE)
- VALUE_HI, VALUE_LO: required for CALL-type instructions that take a value parameter (i.e. CALL and CALLCODE)
- GAS_STIPEND: the value which ought to be justified


Expand Down Expand Up @@ -69,7 +69,7 @@ This case starts with the same computation of

$$\lambda := L(\textsf{GAS\\_UPDT} - \textsf{GAS\\_COST})$$

Next one must compare compare $\lambda$ and the 256-bit integer $\mu{s}\big[0\big]$. This can be done via a lookup to the WCP module. Using the outcome of that comparison one can impose that
Next one must compare $\lambda$ and the 256-bit integer $\mu{s}\big[0\big]$. This can be done via a lookup to the WCP module. Using the outcome of that comparison one can impose that

$$\textsf{GAS-STIPEND} == \min \big\lbrace \lambda, \mu_{\textbf{s}} \big[ 0 \big] \big\rbrace + 2300 \cdot \textsf{VALUE-TRANSFER} \cdot \big[ \mu_{\textbf{s}} \big[ 2 \big] \neq 0 \big]$$

Expand Down