add opcodes for evm circuit doc (#891)

Author: DreamWuGit

docs/EVM_Circuit.md

@@ -235,7 +235,7 @@ For the EVM Circuit, there are internal and external lookup tables. We summarize
 |BlockTable|tag, index, value|
 |CopyTable|is_first, src_id, src_tag, dst_id, dst_tag, src_addr, src_addr_end, dst_addr, length, rlc_acc, rw_counter, rw_inc|
 |KeccakTable|is_enabled (=1), input_rlc, input_len, output_rlc|
-|ExpTable|q_enable (=1), is_step (=1), base_limbs[0], base_limbs[1], base_limbs[2], base_limbs[3], exponent_lo_hi[0], exponent_lo_hi[1], exponentiation_lo_hi[0],  exponentiation_lo_hi[1]|
+|ExpTable|is_step (=1), identifier, is_last, base_limbs[0], base_limbs[1], base_limbs[2], base_limbs[3], exp_lo_hi[0], exp_lo_hi[1], exponentiation_lo_hi[0],  exponentiation_lo_hi[1]|
 |SigTable|msg_hash_rlc, sig_v, sig_r_rlc, sig_s_rlc, recovered_addr, is_valid|
 
 
@@ -261,10 +261,99 @@ The random challenge used to obtain the RLC result of lookup's input expressions
 
 ## Constraints 
 
+Due to page limit we only discuss some examples here.
+
 ### General Constraints
 
-<i>TODO: explain general step-transition constraints, such as `SameContextGadget` etc...</i>
+#### `SameContextGadget`
+
+This gadget is applied to every execution step in order to check the correct transition from current state to next state. The constraints include
+- lookup to Bytecode Table and Fixed Table (with `tag=FixedTableTag::ResponsibleOpcode`) for the correctness of the current opcode;
+- check remaining gas is sufficient;
+- check correct step state transition, such as change of `rw_counter`, `program_counter`, `stack_pointer` etc.
 
 ### Opcode Constraints 
 
-<i>TODO: maybe better idea is to mimic ConsenSys spec, that has a classification of opcodes based on stack behavior...</i>
+[ETH Yellow Paper]: https://ethereum.github.io/yellowpaper/paper.pdf
+
+#### `mulmod`
+
+According to the [ETH Yellow Paper], the MULMOD opcode (modulo addition operation) pops $3$ EVM words $\boldsymbol{\mu}_{\textbf{s}}[0], \boldsymbol{\mu}_{\textbf{s}}[1], \boldsymbol{\mu}_{\textbf{s}}[2]$ each with 256-bit (32 byte) size from the stack and push back one EVM word $\boldsymbol{\mu}_{\textbf{s}}'[0]$. 
+
+To make our notations simpler, we denote $a=\boldsymbol{\mu}_{\textbf{s}}[0]$, $b=\boldsymbol{\mu}_{\textbf{s}}[1]$ and $n=\boldsymbol{\mu}_{\textbf{s}}[2]$ and $r=\boldsymbol{\mu}_{\textbf{s}}'[0]$, then the EVM behavior of MULMOD opcode can be viewed as a mapping 
+$$(a, b, n)\stackrel{\text{MULMOD}}{\rightarrow}  
+r=\left\{\begin{array}{ll} 
+0 & \text{ if } n=0 \ ,
+\\
+a\cdot b \mod n & \text{ if } n\neq 0 \ .
+\end{array}\right.
+$$ 
+The intermediate calculation is the multiplication of two $32$-byte words $a$ and $b$, and this operation is supposed to be <i>not</i> subject to $2^{256}$ modulo. 
+
+Of course, a full characterization of the EVM behavior under MULMOD also involves the correct stack push-pop: $3$ stack pops and $1$ stack push, and together with a gas cost of $8$.
+
+For the MULMOD opcode, EVM Circuit assigns $(a, b, n, r, k, a_{\text{reduced}}, d, e)$, each of which is 32-byte word:
+
+$$\begin{array}{rl}
+a & =\overline{a_0a_1...a_{31}}=\sum\limits_{i=0}^{31} a_i \cdot 256^i \ ,
+\\
+b & =\overline{b_0b_1...b_{31}}=\sum\limits_{i=0}^{31} b_i\cdot 256^i \ , 
+\\
+n & =\overline{n_0n_1...n_{31}}=\sum\limits_{i=0}^{31} n_i\cdot 256^i \ , 
+\\
+r & =\overline{r_0r_1...r_{31}}=\sum\limits_{i=0}^{31} r_i\cdot 256^i \ ,
+\\
+a_\text{reduced} & =\overline{a_{r0}...a_{r31}}=\sum\limits_{i=0}^{31}a_{ri}\cdot 256^i \ ,
+\\
+d & =\overline{p_0p_1...p_{31}}=\sum\limits_{i=0}^{31} p_i\cdot 256^i \ ,
+\\
+e & =\overline{p_{32}p_{33}...p_{63}}=\sum\limits_{i=0}^{31} p_{32+i} \cdot 256^i \ ,
+\\
+k & =\overline{k_0k_1...k_{31}}=\sum\limits_{i=0}^{31} k_i \cdot 256^i \ .
+\end{array}$$
+
+It also assigns $\verb#n_sum#=n_0+...+n_{31}$.
+
+Then the constraints are
+
+- $a_{\text{reduced}} 
+== a\mod n \ \text{ if } n\neq 0
+\text{ and } a_{\text{reduced}} == 0 \text{ if } n=0$ (ModGadget); 
+- $a_{\text{reduced}}\cdot b + 0  
+== d\cdot 2^{256} + e$ (MulAddWords512Gadget);
+- $k\cdot n + r == d\cdot 2^{256} + e$ (MulAddWords512Gadget);
+- $1-\mathbf{1}_{\{r<n\}}-\mathbf{1}_{\{\verb#n_sum#=0\}}==0$ (IsZeroGadget, LtWordGadget);
+- `SameContextGadget`
+    - opcodeID checks: opId $==$ OpcodeId(0x09);
+    - state transition: rw_counter +4; stack\_pointer +2; pc +1; gas - op_cost;
+    - Lookups: $4$ busmapping lookups: $a=\boldsymbol{\mu}_{\textbf{s}}[0]$, 
+$b=\boldsymbol{\mu}_{\textbf{s}}[1]$, $n=\boldsymbol{\mu}_{\textbf{s}}[2]$, 
+$r=\boldsymbol{\mu}_{\textbf{s}}'[0]$;
+    - Exceptions: 
+        - 1. stack undeflow: $1022 \leq$ stack\_pointer $\leq 1024$; 
+        - 2. out of gas: Remaining gas is not enough.
+
+
+#### `returndatacopy`
+
+According to the [ETH Yellow Paper], the RETURNDATACOPY opcode pops 3 stack elements $\boldsymbol{\mu}_{\textbf{s}}[0]$=`dest_offset`, $\boldsymbol{\mu}_{\textbf{s}}[1]$=`data_offset` and $\boldsymbol{\mu}_{\textbf{s}}[2]$=`size`. It copies output data from the previous call to memory. The copied output data starts from `data_offset` within return data from last call and memory copy starts from `dest_offset`, with copy data size equal to `size`. Denote by $\boldsymbol{\mu}'_{\textbf{m}}$ the updated memory state and $\boldsymbol{\mu}_{\textbf{o}}$ the return data from last call, then the rule is given by the following formula
+$$\forall i\in \{0... \boldsymbol{\mu}_{\textbf{s}}[2]-1\}: \boldsymbol{\mu}_{\textbf{m}}'[\boldsymbol{\mu}_{\textbf{s}}[0]+i]=\left\{
+\begin{array}{ll}
+\boldsymbol{\mu}_{\textbf{o}}[\boldsymbol{\mu}_{\textbf{s}}[1]+i] & \text{ if } \boldsymbol{\mu}_{\textbf{s}}[1]+i<\|\boldsymbol{\mu}_{\textbf{o}}\|
+\\
+0 & \text{ otherwise .}
+\end{array}
+\right.$$
+Note that the data to be copied to memory that exceeds return data size ($\|\boldsymbol{\mu}_{\textbf{o}}\|$) will be padded by 0.
+
+For RETURNDATACOPY opcode, EVM Circuit does the following type of constraint checks together with witness assignments:
+
+- Constraints for stack pop of `dest_offset`, `data_offset` and `size`. This means they are assigned from the step's rw data (via bus mapping) and then they are checked by doing RwTable lookups with `tag=RwTableTag::Stack`, as well as verifying correct stack pointer update;
+- Constraints for call context related data including `last_callee_id`, `return_data_offset` (offset for $\boldsymbol{\mu}_{\textbf{o}}$) and `return_data_size` ($\|\boldsymbol{\mu}_{\textbf{o}}\|$). These are assigned and then checked by RwTable lookups with `tag=RwTableTag::CallContext`. Here return data means the output data from last call, from which we fetch data that is to be copied into memory;
+- Constraints for ensuring no out-of-bound errors happen with `return_data_size`;
+- Constraints for memory related behavior. This includes memory address and expansion via `dest_offset` and `size`, as well as gas cost for memory expansion;
+- Constraints for copy behavior. This is done by lookup to CopyTable with `src_id=last_callee_id` (source call id) and `dst_id=` current step call id (destination call id), and corresponding source and destination addresses determined by `return_data_offset`, `return_data_size`, `data_offset`, `dest_offset` and `size` (that computes destination memory address);
+- `SameContextGadget`
+    - opcodeID checks: opId $==$ OpcodeId(0x3e);
+    - state transition: rw_counter+, stack\_pointer+3, pc+1, gas -(op_cost+memory expansion cost), memory expand to next memory word size.
+