Update specs for continuation #489

hratoanina · 2024-08-13T20:25:27Z

hratoanina · 2024-08-13T20:26:57Z

evm_arithmetization/src/cpu/kernel/asm/mpt/linked_list/linked_list.asm

@@ -24,8 +24,8 @@
 /// The values at the respective positions are:
 /// - 0: The account key
 /// - 1: The slot key
-/// - 2: A ptr to the payload (the stored value)
-/// - 3: A ptr to the initial payload.
+/// - 2: The slot value.


Unrelated to the PR, but it wasn't changed in #433.

docs/arithmetization/cpulogic.tex

Nashtare · 2024-08-13T23:06:20Z

docs/arithmetization/cpulogic.tex


-Since we process one transaction at a time, a few intermediary values need to be provided by the prover. Indeed, to prove that the registers in the EVM state are correctly updated, we need to have access to their initial values. When aggregating proofs, we can also constrain those values to match from one transaction to the next. Let us consider the example of the transaction number. Let $n$ be the number of transactions executed so far in the current block. If the current proof is not a dummy one (we are indeed executing a transaction), then the transaction number should be updated: $n := n+1$. Otherwise, the number remains unchanged. We can easily constrain this update. When aggregating the previous transaction proof ($lhs$) with the current one ($rhs$), we also need to check that the output transaction number of $lhs$ is the same as the input transaction number of $rhs$. 
+Since we process transactions and not full blocks, a few intermediary values need to be provided by the prover. Indeed, to prove that the registers in the EVM state are correctly updated, we need to have access to their initial values. When aggregating proofs, we can also constrain those values to match from one batch to the next. Let us consider the example of the transaction number. Let $n$ be the number of transactions executed so far in the current block. If the current proof is not a dummy one (we are indeed executing a transaction), then the transaction number should be updated: $n := n+k$ with $k$ the number of transactions in the batch. Otherwise, the number remains unchanged. We can easily constrain this update. When aggregating the previous transaction batch proof ($lhs$) with the current one ($rhs$), we also need to check that the output transaction number of $lhs$ is the same as the input transaction number of $rhs$. 


Suggested change

Since we process transactions and not full blocks, a few intermediary values need to be provided by the prover. Indeed, to prove that the registers in the EVM state are correctly updated, we need to have access to their initial values. When aggregating proofs, we can also constrain those values to match from one batch to the next. Let us consider the example of the transaction number. Let $n$ be the number of transactions executed so far in the current block. If the current proof is not a dummy one (we are indeed executing a transaction), then the transaction number should be updated: $n := n+k$ with $k$ the number of transactions in the batch. Otherwise, the number remains unchanged. We can easily constrain this update. When aggregating the previous transaction batch proof ($lhs$) with the current one ($rhs$), we also need to check that the output transaction number of $lhs$ is the same as the input transaction number of $rhs$.

Since we process transactions and not entire blocks, a few intermediary values need to be provided by the prover. Indeed, to prove that the registers in the EVM state are correctly updated, we need to have access to their initial values. When aggregating proofs, we can also constrain those values to match from one batch to the next. Let us consider the example of the transaction number. Let $n$ be the number of transactions executed so far in the current block. If the current proof is not a dummy one (we are indeed executing a batch of transactions), then the transaction number should be updated: $n := n+k$ with $k$ the number of transactions in the batch. Otherwise, the number remains unchanged. We can easily constrain this update. When aggregating the previous transaction batch proof ($lhs$) with the current one ($rhs$), we also need to check that the output transaction number of $lhs$ is the same as the input transaction number of $rhs$.

Orthogonal to the changes, but I find this paragraph and a few other extremely heavy / verbose.

docs/arithmetization/cpulogic.tex

docs/arithmetization/tables/cpu.tex

Nashtare · 2024-08-13T23:33:37Z

docs/arithmetization/tables/cpu.tex

+    \item  \texttt{Context pruning}: When \texttt{SET\_CONTEXT} is called to return to a parent context, this makes the current context stale. The kernel indicates it
+by setting one general column to 1. For more details about context pruning, see \ref{context-pruning}.


Don't know where to write the comment, but it's missing (if we want to keep writing them...) the new columns on the memory table side.

docs/arithmetization/tables/mem-before.tex

docs/arithmetization/tables/memory.tex

Update specs for continuation

2e8e1c4

hratoanina requested review from muursh and Nashtare as code owners August 13, 2024 20:25

github-actions bot added crate: evm_arithmetization Anything related to the evm_arithmetization crate. specs labels Aug 13, 2024

hratoanina commented Aug 13, 2024

View reviewed changes

Nashtare reviewed Aug 13, 2024

View reviewed changes

Nashtare requested a review from LindaGuiga as a code owner August 16, 2024 13:48

Nashtare added this to the continuations - Q3 2024 milestone Aug 17, 2024

Nashtare assigned hratoanina Aug 17, 2024

hratoanina added 2 commits August 19, 2024 10:08

Apply comments

371d9c7

Combine continuation tables

2bffe04

Nashtare approved these changes Aug 20, 2024

View reviewed changes

Nashtare merged commit 5cb6b5a into feat/continuations Aug 20, 2024
15 checks passed

Nashtare deleted the continuation_specs branch August 20, 2024 22:45

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Update specs for continuation #489

Update specs for continuation #489

hratoanina commented Aug 13, 2024

hratoanina Aug 13, 2024

Nashtare Aug 13, 2024

Nashtare Aug 13, 2024

Nashtare Aug 13, 2024


		Since we process one transaction at a time, a few intermediary values need to be provided by the prover. Indeed, to prove that the registers in the EVM state are correctly updated, we need to have access to their initial values. When aggregating proofs, we can also constrain those values to match from one transaction to the next. Let us consider the example of the transaction number. Let $n$ be the number of transactions executed so far in the current block. If the current proof is not a dummy one (we are indeed executing a transaction), then the transaction number should be updated: $n := n+1$. Otherwise, the number remains unchanged. We can easily constrain this update. When aggregating the previous transaction proof ($lhs$) with the current one ($rhs$), we also need to check that the output transaction number of $lhs$ is the same as the input transaction number of $rhs$.
		Since we process transactions and not full blocks, a few intermediary values need to be provided by the prover. Indeed, to prove that the registers in the EVM state are correctly updated, we need to have access to their initial values. When aggregating proofs, we can also constrain those values to match from one batch to the next. Let us consider the example of the transaction number. Let $n$ be the number of transactions executed so far in the current block. If the current proof is not a dummy one (we are indeed executing a transaction), then the transaction number should be updated: $n := n+k$ with $k$ the number of transactions in the batch. Otherwise, the number remains unchanged. We can easily constrain this update. When aggregating the previous transaction batch proof ($lhs$) with the current one ($rhs$), we also need to check that the output transaction number of $lhs$ is the same as the input transaction number of $rhs$.

		\item \texttt{Context pruning}: When \texttt{SET\_CONTEXT} is called to return to a parent context, this makes the current context stale. The kernel indicates it
		by setting one general column to 1. For more details about context pruning, see \ref{context-pruning}.

Update specs for continuation #489

Update specs for continuation #489

Conversation

hratoanina commented Aug 13, 2024

hratoanina Aug 13, 2024

Choose a reason for hiding this comment

Nashtare Aug 13, 2024

Choose a reason for hiding this comment

Nashtare Aug 13, 2024

Choose a reason for hiding this comment

Nashtare Aug 13, 2024

Choose a reason for hiding this comment