Feat/sha3

src/zkevm_specs/evm/execution/__init__.py

@@ -33,6 +33,7 @@
 from .selfbalance import *
 from .extcodehash import *
 from .log import *
+from .sha3 import sha3
 from .shr import shr
 from .bitwise import not_opcode
 from .sdiv_smod import sdiv_smod
@@ -63,6 +64,7 @@
     ExecutionState.PUSH: push,
     ExecutionState.SCMP: scmp,
     ExecutionState.GAS: gas,
+    ExecutionState.SHA3: sha3,
     ExecutionState.SLOAD: sload,
     ExecutionState.SSTORE: sstore,
     ExecutionState.SELFBALANCE: selfbalance,

src/zkevm_specs/evm/execution/calldatacopy.py

@@ -39,7 +39,7 @@ def calldatacopy(instruction: Instruction):
         FQ(instruction.curr.is_root), FQ(CopyDataTypeTag.TxCalldata), FQ(CopyDataTypeTag.Memory)
     )
     if instruction.is_zero(length) == 0:
-        copy_rwc_inc = instruction.copy_lookup(
+        copy_rwc_inc, _ = instruction.copy_lookup(
             src_id,
             CopyDataTypeTag(src_type.n),
             instruction.curr.call_id,

src/zkevm_specs/evm/execution/codecopy.py

@@ -24,7 +24,7 @@ def codecopy(instruction: Instruction):
     gas_cost = instruction.memory_copier_gas_cost(size, memory_expansion_gas_cost)
 
     if instruction.is_zero(size) == FQ(0):
-        copy_rwc_inc = instruction.copy_lookup(
+        copy_rwc_inc, _ = instruction.copy_lookup(
             instruction.curr.code_hash,
             CopyDataTypeTag.Bytecode,
             instruction.curr.call_id,

src/zkevm_specs/evm/execution/log.py

@@ -63,7 +63,7 @@ def log(instruction: Instruction):
             instruction.constrain_bool(FQ(diff))
 
     if instruction.is_zero(msize) == 0 and is_persistent == 1:
-        copy_rwc_inc = instruction.copy_lookup(
+        copy_rwc_inc, _ = instruction.copy_lookup(
             instruction.curr.call_id,
             CopyDataTypeTag.Memory,
             tx_id,

src/zkevm_specs/evm/execution/return_.py

@@ -35,7 +35,7 @@ def return_(instruction: Instruction):
         # callee's memory to bytecode, using the copy circuit.
         code_hash = instruction.curr.aux_data  # Load code_hash witness value from aux_data
         copy_length = return_length
-        copy_rwc_inc = instruction.copy_lookup(
+        copy_rwc_inc, _ = instruction.copy_lookup(
             instruction.curr.call_id,  # src_id
             CopyDataTypeTag.Memory,  # src_type
             code_hash,  # dst_id
@@ -62,7 +62,7 @@ def return_(instruction: Instruction):
             CallContextFieldTag.ReturnDataLength
         )  # rwc += 1
         copy_length = instruction.min(return_length, caller_return_length, N_BYTES_MEMORY_ADDRESS)
-        copy_rwc_inc = instruction.copy_lookup(
+        copy_rwc_inc, _ = instruction.copy_lookup(
             instruction.curr.call_id,  # src_id
             CopyDataTypeTag.Memory,  # src_type
             instruction.next.call_id,  # dst_id

src/zkevm_specs/evm/execution/sha3.py

@@ -0,0 +1,52 @@
+from ..instruction import Instruction, Transition
+from ..table import CopyDataTypeTag
+from zkevm_specs.util import FQ, GAS_COST_COPY_SHA3, RLC
+
+
+def sha3(instruction: Instruction):
+    opcode = instruction.opcode_lookup(True)
+
+    # byte offset in memory.
+    offset = instruction.stack_pop()
+    # byte size to read in memory.
+    size = instruction.stack_pop()
+    # sha3 value pushed to stack.
+    sha3_value = instruction.stack_push()
+
+    # convert RLC encoded stack elements to FQ.
+    memory_offset, length = instruction.memory_offset_and_length(offset, size)
+
+    copy_rwc_inc, rlc_acc = instruction.copy_lookup(
+        instruction.curr.call_id,
+        CopyDataTypeTag.Memory,
+        instruction.curr.call_id,
+        CopyDataTypeTag.RlcAcc,
+        memory_offset,
+        memory_offset + length,
+        FQ.zero(),
+        length,
+        instruction.curr.rw_counter + instruction.rw_counter_offset,
+    )
+    keccak256_rlc_acc = instruction.keccak_lookup(length, rlc_acc)
+
+    instruction.constrain_equal(
+        keccak256_rlc_acc,
+        sha3_value.expr(),
+    )
+
+    # calculate memory expansion gas costs.
+    next_memory_size, memory_expansion_gas_cost = instruction.memory_expansion_dynamic_length(
+        memory_offset, length
+    )
+    gas_cost = instruction.memory_copier_gas_cost(
+        length, memory_expansion_gas_cost, GAS_COST_COPY_SHA3
+    )
+
+    instruction.step_state_transition_in_same_context(
+        opcode,
+        rw_counter=Transition.delta(instruction.rw_counter_offset + copy_rwc_inc),
+        program_counter=Transition.delta(1),
+        stack_pointer=Transition.delta(1),  # 2 stack reads and 1 stack write
+        memory_size=Transition.to(next_memory_size),
+        dynamic_gas_cost=gas_cost,
+    )

src/zkevm_specs/evm/instruction.py

@@ -999,10 +999,13 @@ def memory_expansion_dynamic_length(
         return cast_expr(next_memory_size, FQ), cast_expr(memory_expansion_gas_cost, FQ)
 
     def memory_copier_gas_cost(
-        self, length: Expression, memory_expansion_gas_cost: Expression
+        self,
+        length: Expression,
+        memory_expansion_gas_cost: Expression,
+        gas_cost_copy: int = GAS_COST_COPY,
     ) -> FQ:
         word_size, _ = self.constant_divmod(length + FQ(31), FQ(32), N_BYTES_MEMORY_SIZE)
-        gas_cost = word_size * GAS_COST_COPY + memory_expansion_gas_cost
+        gas_cost = word_size * gas_cost_copy + memory_expansion_gas_cost
         self.range_check(gas_cost, N_BYTES_GAS)
         return gas_cost
 
@@ -1021,8 +1024,8 @@ def copy_lookup(
         length: Expression,
         rw_counter: Expression,
         log_id: Expression = None,
-    ) -> FQ:
-        return self.tables.copy_lookup(
+    ) -> Tuple[FQ, FQ]:
+        copy_table_row = self.tables.copy_lookup(
             src_id,
             FQ(src_type),
             dst_id,
@@ -1033,4 +1036,8 @@ def copy_lookup(
             length,
             rw_counter,
             log_id,
-        ).rwc_inc
+        )
+        return copy_table_row.rwc_inc, copy_table_row.value_rlc
+
+    def keccak_lookup(self, length: Expression, value_rlc: Expression) -> FQ:
+        return self.tables.keccak_lookup(length, value_rlc).hash_rlc

src/zkevm_specs/evm/table.py

@@ -418,10 +418,18 @@ class CopyTableRow(TableRow):
     src_addr_end: FQ
     dst_addr: FQ
     length: FQ
+    value_rlc: FQ
     rw_counter: FQ
     rwc_inc: FQ
 
 
+@dataclass(frozen=True)
+class KeccakTableRow(TableRow):
+    idx: FQ
+    hash_rlc: FQ
+    value_rlc: FQ
+
+
 class Tables:
     """
     A collection of lookup tables used in EVM circuit.
@@ -433,6 +441,7 @@ class Tables:
     bytecode_table: Set[BytecodeTableRow]
     rw_table: Set[RWTableRow]
     copy_table: Set[CopyTableRow]
+    keccak_table: Set[KeccakTableRow]
 
     def __init__(
         self,
@@ -441,6 +450,7 @@ def __init__(
         bytecode_table: Set[BytecodeTableRow],
         rw_table: Union[Set[Sequence[Expression]], Set[RWTableRow]],
         copy_circuit: Sequence[CopyCircuitRow] = None,
+        keccak_table: Sequence[KeccakTableRow] = None,
     ) -> None:
         self.block_table = block_table
         self.tx_table = tx_table
@@ -451,29 +461,38 @@ def __init__(
         )
         if copy_circuit is not None:
             self.copy_table = self._convert_copy_circuit_to_table(copy_circuit)
+        if keccak_table is not None:
+            self.keccak_table = set(keccak_table)
 
     def _convert_copy_circuit_to_table(self, copy_circuit: Sequence[CopyCircuitRow]):
-        rows = []
+        rows: List[CopyTableRow] = []
         for i, row in enumerate(copy_circuit):
-            if row.is_first != 1:
-                continue
-            assert i + 1 < len(copy_circuit), "Not enough rows in copy circuit"
-            next_row = copy_circuit[i + 1]
-            assert next_row.q_step == 0, "Invalid copy circuit"
-            rows.append(
-                CopyTableRow(
-                    src_id=row.id,
-                    src_type=row.tag,
-                    dst_id=next_row.id,
-                    dst_type=next_row.tag,
-                    src_addr=row.addr,
-                    src_addr_end=row.src_addr_end,
-                    dst_addr=next_row.addr,
-                    length=row.bytes_left,
-                    rw_counter=row.rw_counter,
-                    rwc_inc=row.rwc_inc_left,
+            # the first row and the row next to it will be used for its fields.
+            if row.is_first == 1:
+                first_row = row
+                assert i + 1 < len(copy_circuit), "Not enough rows in copy circuit"
+                next_row = copy_circuit[i + 1]
+                assert next_row.q_step == 0, "Invalid copy circuit"
+
+            # update `value_rlc` when we encounter the copy event's last row.
+            if row.is_last == 1:
+                value_rlc = row.value
+                rows.append(
+                    CopyTableRow(
+                        src_id=first_row.id,
+                        src_type=first_row.tag,
+                        dst_id=next_row.id,
+                        dst_type=next_row.tag,
+                        src_addr=first_row.addr,
+                        src_addr_end=first_row.src_addr_end,
+                        dst_addr=next_row.addr,
+                        length=first_row.bytes_left,
+                        value_rlc=value_rlc,
+                        rw_counter=first_row.rw_counter,
+                        rwc_inc=first_row.rwc_inc_left,
+                    )
                 )
-            )
+
         return set(rows)
 
     def fixed_lookup(
@@ -581,6 +600,13 @@ def copy_lookup(
         }
         return lookup(CopyTableRow, self.copy_table, query)
 
+    def keccak_lookup(self, length: Expression, value_rlc: Expression):
+        query = {
+            "idx": length - FQ(1),
+            "value_rlc": value_rlc,
+        }
+        return lookup(KeccakTableRow, self.keccak_table, query)
+
 
 T = TypeVar("T", bound=TableRow)
 

src/zkevm_specs/evm/typing.py

@@ -45,6 +45,7 @@
     CopyDataTypeTag,
     CopyCircuitRow,
     CopyTableRow,
+    KeccakTableRow,
 )
 from .opcode import get_push_size, Opcode
 
@@ -666,6 +667,29 @@ def _append(
         return self
 
 
+class KeccakCircuit:
+    rows: List[KeccakTableRow]
+
+    def __init__(self) -> None:
+        self.rows = []
+
+    def add(self, data: bytes, r: FQ) -> KeccakCircuit:
+        rows: List[KeccakTableRow] = []
+        hash_rlc = RLC(keccak256(RLC(bytes(reversed(data)), r, len(data)).le_bytes), r)
+        value_rlc = FQ.zero()
+        for i in range(len(data)):
+            value_rlc = value_rlc * r + data[i]
+            rows.append(
+                KeccakTableRow(
+                    idx=FQ(i),
+                    hash_rlc=hash_rlc.expr(),
+                    value_rlc=value_rlc,
+                )
+            )
+        self.rows.extend(rows)
+        return self
+
+
 class CopyCircuit:
     rows: List[CopyCircuitRow]
     pad_rows: List[CopyCircuitRow]

src/zkevm_specs/util/param.py

@@ -41,6 +41,8 @@
 GAS_COST_SELF_DESTRUCT = 5000
 # Gas cost of copying every word
 GAS_COST_COPY = 3
+# Gas cost of copying every word, specifically in the case of SHA3 opcode
+GAS_COST_COPY_SHA3 = 6
 # Gas cost of non-creation transaction
 GAS_COST_TX = 21000
 # Constant gas cost of LOG
@@ -72,6 +74,8 @@
 MEMORY_EXPANSION_QUAD_DENOMINATOR = 512
 # Coefficient of linear part of memory expansion gas cost
 MEMORY_EXPANSION_LINEAR_COEFF = 3
+# Coefficient of linear part of memory expansion gas cost, specifically in the case of SHA3
+MEMORY_EXPANSION_LINEAR_COEFF_SHA3 = 6
 
 # Maximum number of bytes copied during one single iteration of CopyToMemory, i.e. the internal state used by the
 # CALLDATACOPY gadget

src/zkevm_specs/util/testing.py

@@ -21,6 +21,7 @@ def div(
 def memory_expansion(
     curr_memory_size: U64,
     address: U64,
+    mem_exp_linear: int = MEMORY_EXPANSION_LINEAR_COEFF,
 ) -> Tuple[U64, U128]:
     # The memory size required for the used address
     address_memory_size = memory_word_size(address)
@@ -34,7 +35,7 @@ def memory_expansion(
 
     # Calculate the gas cost for the memory expansion
     # This gas cost is the difference between the next and current memory costs
-    memory_gas_cost = (next_memory_size - curr_memory_size) * MEMORY_EXPANSION_LINEAR_COEFF + (
+    memory_gas_cost = (next_memory_size - curr_memory_size) * mem_exp_linear + (
         next_quad_memory_cost - curr_quad_memory_cost
     )
 

tests/evm/test_calldatacopy.py

@@ -104,13 +104,6 @@ def test_calldatacopy(
         )
     ]
 
-    rw_dictionary = (
-        RWDictionary(1)
-        .stack_read(CALL_ID, 1021, memory_offset_rlc)
-        .stack_read(CALL_ID, 1022, data_offset_rlc)
-        .stack_read(CALL_ID, 1023, length_rlc)
-        .call_context_read(CALL_ID, CallContextFieldTag.TxId, TX_ID)
-    )
     rw_dictionary = (
         RWDictionary(1)
         .stack_read(CALL_ID, 1021, memory_offset_rlc)