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

Feat/#498 integrate precompiles into callop #508

Merged
merged 13 commits into from
Feb 21, 2024
Merged
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
- `DELEGATECALL` creates a new sub context as setting caller address to parent caller's and callee address to current caller's, but with the code of the given account (callee). In particular the current `sender` (parent caller) and `value` remain the same.
- `STATICCALL` does not allow any state modifying instructions (is_static == 1) or sending ether to callee in the sub context.

These are done by popping serveral words from stack:
These are done by popping several words from stack:

1. `gas` - The amount of gas caller want to give to callee (capped by rule in EIP150)
2. `callee_address` - The ether recipient whose code is to be executed (by taking the 20 LSB of popped word)
Expand Down
3 changes: 3 additions & 0 deletions src/zkevm_specs/evm_circuit/execution/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,7 @@
from .precompiles.ecadd import *
from .precompiles.ecpairing import *
from .precompiles.ecmul import *
from .precompiles.error_oog_precompile import *


EXECUTION_STATE_IMPL: Dict[ExecutionState, Callable] = {
Expand Down Expand Up @@ -156,6 +157,8 @@
ExecutionState.ErrorOutOfGasSloadSstore: error_oog_sload_sstore,
ExecutionState.ErrorReturnDataOutOfBound: error_return_data_out_of_bound,
ExecutionState.ErrorOutOfGasCREATE: error_oog_create,
ExecutionState.ErrorOutOfGasPrecompile: error_oog_precompile,
# Precompiles
ExecutionState.ECRECOVER: ecRecover,
# ExecutionState.SHA256: ,
# ExecutionState.RIPEMD160: ,
Expand Down
134 changes: 130 additions & 4 deletions src/zkevm_specs/evm_circuit/execution/callop.py
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
from zkevm_specs.evm_circuit.util.call_gadget import CallGadget
from zkevm_specs.util.param import N_BYTES_GAS, N_BYTES_STACK
from zkevm_specs.evm_circuit.util.precompile_gadget import PrecompileGadget
from zkevm_specs.util.hash import EMPTY_CODE_HASH
from zkevm_specs.util.param import N_BYTES_GAS, N_BYTES_MEMORY_WORD_SIZE, N_BYTES_STACK
from ...util import FQ, GAS_STIPEND_CALL_WITH_VALUE, Word, WordOrValue
from ..instruction import Instruction, Transition
from ..opcode import Opcode
from ..table import RW, CallContextFieldTag, AccountFieldTag
from ..table import RW, CallContextFieldTag, AccountFieldTag, CopyDataTypeTag
from ..execution_state import precompile_execution_states


Expand Down Expand Up @@ -115,13 +117,14 @@ def callop(instruction: Instruction):

# Make sure the state transition to ExecutionState for precompile if and
# only if the callee address is one of precompile
is_precompile = instruction.precompile(callee_address)
is_precompile = instruction.precompile(call.callee_address)
instruction.constrain_equal(
is_precompile, FQ(instruction.next.execution_state in precompile_execution_states())
)

stack_pointer_delta = 5 + is_call + is_callcode
no_callee_code = call.is_empty_code_hash + call.callee_not_exists
# precheck fails or callee has no code
if is_precheck_ok is False or (no_callee_code == FQ(1) and is_precompile == FQ(0)):
# Empty return_data
for field_tag, expected_value in [
Expand All @@ -147,7 +150,130 @@ def callop(instruction: Instruction):
is_create=Transition.same(),
code_hash=Transition.same_word(),
)
else:
# precompiles call
elif is_precheck_ok and is_precompile == FQ.one():
precompile_input_len: FQ = instruction.curr.aux_data[0]
precompile_return_length: FQ = instruction.curr.aux_data[1]
min_rd_copy_size = min(precompile_return_length, call.rd_length.n)

# precompiles have no code
instruction.constrain_equal(no_callee_code, FQ.one())
# precompiles address must be warm
instruction.constrain_equal(is_warm_access, FQ.one())

# Setup next call's context.
for field_tag, expected_value in [
(CallContextFieldTag.IsSuccess, call.is_success),
(CallContextFieldTag.CalleeAddress, callee_address_word),
(CallContextFieldTag.CallerId, instruction.curr.call_id),
(CallContextFieldTag.CallDataOffset, call.cd_offset),
(CallContextFieldTag.CallDataLength, call.cd_length),
(CallContextFieldTag.ReturnDataOffset, call.rd_offset),
(CallContextFieldTag.ReturnDataLength, call.rd_length),
]:
instruction.constrain_equal_word(
instruction.call_context_lookup_word(field_tag, RW.Write, callee_call_id),
WordOrValue(expected_value),
)

# Save caller's call state
for field_tag, expected_value in [
(CallContextFieldTag.ProgramCounter, instruction.curr.program_counter + 1),
(
CallContextFieldTag.StackPointer,
instruction.curr.stack_pointer + stack_pointer_delta,
),
(CallContextFieldTag.GasLeft, instruction.curr.gas_left - gas_cost - callee_gas_left),
(CallContextFieldTag.MemorySize, call.next_memory_size),
(
CallContextFieldTag.ReversibleWriteCounter,
instruction.curr.reversible_write_counter + 1,
),
(CallContextFieldTag.LastCalleeId, callee_call_id),
(CallContextFieldTag.LastCalleeReturnDataOffset, FQ.zero()),
(CallContextFieldTag.LastCalleeReturnDataLength, FQ(precompile_return_length)),
]:
instruction.constrain_equal(
instruction.call_context_lookup(field_tag, RW.Write),
expected_value,
)

### copy table lookup here
### is to rlc input and output to have an easy way to verify data

# RLC precompile input from memory
rw_counter_inc = instruction.rw_counter_offset
input_copy_rwc_inc = FQ.zero()
if precompile_input_len != FQ(0):
input_copy_rwc_inc, _ = instruction.copy_lookup(
instruction.curr.call_id,
CopyDataTypeTag.Memory,
callee_call_id,
CopyDataTypeTag.RlcAcc,
call.cd_offset,
FQ(call.cd_offset + precompile_input_len),
FQ.zero(),
FQ(precompile_input_len),
instruction.curr.rw_counter + rw_counter_inc,
)
rw_counter_inc += input_copy_rwc_inc

# RLC precompile output from memory
output_copy_rwc_inc = FQ.zero()
if call.is_success == FQ.one() and precompile_return_length != FQ.zero():
output_copy_rwc_inc, _ = instruction.copy_lookup(
callee_call_id,
CopyDataTypeTag.Memory,
callee_call_id,
CopyDataTypeTag.RlcAcc,
FQ.zero(),
FQ(precompile_return_length),
FQ.zero(),
FQ(precompile_return_length),
instruction.curr.rw_counter + rw_counter_inc,
)
rw_counter_inc += output_copy_rwc_inc

# Verify data copy from precompiles
return_copy_rwc_inc = FQ.zero()
ChihChengLiang marked this conversation as resolved.
Show resolved Hide resolved
if call.is_success == FQ.one() and precompile_return_length != FQ.zero():
return_copy_rwc_inc, _ = instruction.copy_lookup(
callee_call_id,
CopyDataTypeTag.Memory,
instruction.curr.call_id,
CopyDataTypeTag.Memory,
FQ.zero(),
FQ(min_rd_copy_size),
call.rd_offset,
FQ(min_rd_copy_size),
instruction.curr.rw_counter + rw_counter_inc,
)
rw_counter_inc += return_copy_rwc_inc

precompile_memory_word_size, _ = instruction.constant_divmod(
FQ(min_rd_copy_size + 31), FQ(32), N_BYTES_MEMORY_WORD_SIZE
)

# Give gas stipend if value is not zero
callee_gas_left += has_value * GAS_STIPEND_CALL_WITH_VALUE

instruction.constrain_step_state_transition(
rw_counter=Transition.delta(rw_counter_inc),
call_id=Transition.to(callee_call_id),
is_root=Transition.to(False),
is_create=Transition.to(False),
code_hash=Transition.to_word(Word(EMPTY_CODE_HASH)),
gas_left=Transition.to(callee_gas_left),
reversible_write_counter=Transition.to(2),
program_counter=Transition.delta(1),
stack_pointer=Transition.same(),
memory_word_size=Transition.to(precompile_memory_word_size),
)

PrecompileGadget(
instruction, call.callee_address, FQ(precompile_return_length), call.cd_length
)
else: # precheck is ok and callee has code
# Save caller's call state
for field_tag, expected_value in [
(CallContextFieldTag.ProgramCounter, instruction.curr.program_counter + 1),
Expand Down
24 changes: 24 additions & 0 deletions src/zkevm_specs/evm_circuit/execution/precompiles/ecrecover.py
Original file line number Diff line number Diff line change
@@ -1,14 +1,22 @@
from dataclasses import dataclass
from zkevm_specs.evm_circuit.instruction import Instruction
from zkevm_specs.evm_circuit.table import (
CallContextFieldTag,
FixedTableTag,
RW,
)
from zkevm_specs.util import FQ, Word, EcrecoverGas
from zkevm_specs.util.arithmetic import RLC

SECP256K1N = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEBAAEDCE6AF48A03BBFD25E8CD0364141


@dataclass(frozen=True)
class PrecompileRlcData:
input_rlc: FQ
output_rlc: FQ


def ecRecover(instruction: Instruction):
is_success = instruction.call_context_lookup(CallContextFieldTag.IsSuccess, RW.Read)
address_word = instruction.call_context_lookup_word(CallContextFieldTag.CalleeAddress)
Expand All @@ -26,9 +34,25 @@ def ecRecover(instruction: Instruction):
sig_r: Word = instruction.curr.aux_data[2]
sig_s: Word = instruction.curr.aux_data[3]
recovered_addr: FQ = instruction.curr.aux_data[4]
rlc_data: PrecompileRlcData = instruction.curr.aux_data[5]
keccak_randomness: FQ = instruction.curr.aux_data[6]

is_recovered = FQ(instruction.is_zero(recovered_addr) != FQ(1))

# Verify input and output
input_bytes = bytearray(b"")
input_bytes.extend(msg_hash.int_value().to_bytes(32, "little"))
input_bytes.extend(sig_v.int_value().to_bytes(32, "little"))
input_bytes.extend(sig_r.int_value().to_bytes(32, "little"))
input_bytes.extend(sig_s.int_value().to_bytes(32, "little"))
input_rlc = RLC(bytes(reversed(input_bytes)), keccak_randomness, n_bytes=128).expr()
instruction.constrain_equal(rlc_data.input_rlc, input_rlc)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Aren't these two values actually the same (I mean not equal, but the same)? Because rlc_data.input_rlc is computed when instantiating the auxiliary data and input_rlc is computed accessing the same values in aux_data?

Copy link
Contributor Author

@KimiWu123 KimiWu123 Feb 20, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For me, data assignment in testing is like what assign_exec_step does at proving time in our circuit. So, yes, it looks the same (but not always the same).
At proving time, a prover assigns

  • msg_hash
  • sig_v, sig_r, sig_s
  • RLC(msg_hash, sig_v, sig_r, sig_s) (a.k.a input_rlc here, this field is to verify data consistency between calls)

In verification logic here, we have to gaurantee msg_hash, sig_v, sig_r and sig_s are the same pairs (sig_v, sig_r and sig_s are coming from the signature of msg_hash). However, a malious signer could sign msg_hash2 and have sig_v2, sig_r2 and sig_s2. It still can pass all the constraints if we don't have calculate input_rlc here. I'm assuming rlc_data.input_rlc is coming from previous step (we can pass data around between previous step and next step in our circuit, but it seems not doable in our spec), so that's why rlc_data.input_rlc and input_rlc look "the same".

Does it make sense to you? Or do you think we need to copy rlc_data.input_rlc from copy_table?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I am missing something and would like to fix my understanding :). My understanding was that we need to ensure that instruction.curr.aux_data is the same as used in callop.py and that this should be done by checking the RLC, so to have a lookup call into copy_table (RLC field) here in ecrecover.py. Maybe this is not the case?

I agree on the assignment part, putting a link to the assignment was probably misleading from my side. What it seems to me here is that we have aux_data: PrecompileAuxData = instruction.curr.aux_data[0] and then both values, aux_data.input_rlc and input_rlc, are computed using aux_data. Or is it aux_data.input_rlc checked somewhere else?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My understanding was that we need to ensure that instruction.curr.aux_data is the same as used in callop.py and that this should be done by checking the RLC, so to have a lookup call into copy_table (RLC field) here in ecrecover.py. Maybe this is not the case?

Yes, that's exactly what I want to do.

I agree on the assignment part, putting a link to the assignment was probably misleading from my side. What it seems to me here is that we have aux_data: PrecompileAuxData = instruction.curr.aux_data[0] and then both values, aux_data.input_rlc and input_rlc, are computed using aux_data. Or is it aux_data.input_rlc checked somewhere else?

No, aux_data.input_rlc was not check in other place.

In my implementation, I treated aux_data as witness inputs, a place I can assign my witnesses. Those data (e.g. sig_r, sig_v...etc) can't be retrieved from stack or memory like what other opcode gagdets implemented.

I might not explain it very well, but you can check Scroll's impl. The msg_hash_raw was converted into rlc formate and compared with msg_hash_keccak_rlc. In the assignment, you can see both of them come from the same source, here and here.


output_rlc = RLC(
bytes(reversed(recovered_addr.n.to_bytes(32, "little"))), keccak_randomness, n_bytes=32
).expr()
instruction.constrain_equal(rlc_data.output_rlc, output_rlc)

# is_success is always true
# ref: https://github.com/ethereum/execution-specs/blob/master/src/ethereum/shanghai/vm/precompiled_contracts/ecrecover.py
instruction.constrain_equal(is_success, FQ(1))
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
from zkevm_specs.evm_circuit.execution.precompiles.ecpairing import BYTES_PER_PAIRING
from zkevm_specs.evm_circuit.instruction import Instruction
from zkevm_specs.evm_circuit.precompile import Precompile
from zkevm_specs.evm_circuit.table import CallContextFieldTag
from zkevm_specs.util import FQ
from zkevm_specs.util.param import N_BYTES_GAS, Bn254PairingPerPointGas, IdentityPerWordGas


def error_oog_precompile(instruction: Instruction):
address_word = instruction.call_context_lookup_word(CallContextFieldTag.CalleeAddress)
address = instruction.word_to_address(address_word)
calldata_len = instruction.call_context_lookup(CallContextFieldTag.CallDataLength)

# the address must be one of precompiles
instruction.constrain_equal(instruction.precompile(address), FQ.one())

# TODO: Handle OOG of SHA256, RIPEMD160, BIGMODEXP and BLAKE2F.
### total gas cost
# constant gas cost
precompile = Precompile(address)
gas_cost = precompile.base_gas_cost()
# dynamic gas cost
if precompile == Precompile.BN254PAIRING:
pairs = calldata_len / BYTES_PER_PAIRING
gas_cost += Bn254PairingPerPointGas * pairs
elif precompile == Precompile.DATACOPY:
gas_cost += instruction.memory_copier_gas_cost(calldata_len, FQ(0), IdentityPerWordGas)

# check gas left is less than total gas required
insufficient_gas, _ = instruction.compare(instruction.curr.gas_left, gas_cost, N_BYTES_GAS)
instruction.constrain_equal(insufficient_gas, FQ(1))

instruction.constrain_error_state(
instruction.rw_counter_offset + instruction.curr.reversible_write_counter
)
2 changes: 2 additions & 0 deletions src/zkevm_specs/evm_circuit/execution_state.py
Original file line number Diff line number Diff line change
Expand Up @@ -123,6 +123,8 @@ class ExecutionState(IntEnum):
# For CREATE and CREATE2 opcodes which may run out of gas.
ErrorOutOfGasCREATE = auto()
ErrorOutOfGasSELFDESTRUCT = auto()
# OOG case of precompiles
ErrorOutOfGasPrecompile = auto()

# Precompile's successful cases
ECRECOVER = auto()
Expand Down
4 changes: 4 additions & 0 deletions src/zkevm_specs/evm_circuit/precompile.py
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,10 @@ def execution_state(self) -> ExecutionState:
def base_gas_cost(self) -> int:
return PRECOMPILE_INFO_MAP[self].base_gas

@classmethod
def len(cls) -> int:
return len(cls)


class PrecompileInfo:
"""
Expand Down
38 changes: 38 additions & 0 deletions src/zkevm_specs/evm_circuit/util/precompile_gadget.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
from zkevm_specs.evm_circuit.precompile import Precompile
from ...util import FQ
from ..instruction import Instruction


class PrecompileGadget:
address: FQ

def __init__(
self,
instruction: Instruction,
callee_addr: FQ,
precompile_return_len: FQ,
calldata_len: FQ,
):
# next execution state must be one of precompiles
instruction.constrain_equal(instruction.precompile(callee_addr), FQ.one())

### precompiles' specific constraints
precompile = Precompile(callee_addr)
if precompile == Precompile.DATACOPY:
# input length is the same as return data length
instruction.constrain_equal(precompile_return_len, calldata_len)
elif precompile == Precompile.ECRECOVER:
# The input different from 128 is allowed and is then right padded with zeros
# We only ensure hat the return length is either 32 or 0.
is_128 = instruction.is_equal(precompile_return_len, FQ(32))
is_zero = instruction.is_equal(precompile_return_len, FQ.zero())
instruction.constrain_equal(is_128 + is_zero, FQ.one())
elif precompile == Precompile.BN254ADD:
# input length is 128 bytes
instruction.constrain_equal(calldata_len, FQ(128))
elif precompile == Precompile.BN254SCALARMUL:
# input length is 96 bytes
instruction.constrain_equal(calldata_len, FQ(96))
elif precompile == Precompile.BN254PAIRING:
# input length is 192 * n bytes
instruction.constrain_equal(FQ(calldata_len.n % 192), FQ.zero())
17 changes: 16 additions & 1 deletion tests/evm/precompiles/test_ecRecover.py
Original file line number Diff line number Diff line change
Expand Up @@ -14,12 +14,13 @@
Tables,
verify_steps,
)
from zkevm_specs.evm_circuit.execution.precompiles.ecrecover import SECP256K1N
from zkevm_specs.evm_circuit.execution.precompiles.ecrecover import PrecompileRlcData, SECP256K1N
from zkevm_specs.util import (
Word,
FQ,
)
from zkevm_specs.evm_circuit.table import SigTableRow
from zkevm_specs.util.arithmetic import RLC


def gen_testing_data():
Expand Down Expand Up @@ -49,6 +50,8 @@ def gen_testing_data():

TESTING_DATA = gen_testing_data()

randomness_keccak = rand_fq()


@pytest.mark.parametrize(
"caller_ctx, msg_hash, v, r, s, address",
Expand All @@ -72,12 +75,24 @@ def test_ecRecover(
return_data_offset = 0
return_data_length = 0x20 if recovered else 0

input_bytes = bytearray(b"")
input_bytes.extend(msg_hash)
input_bytes.extend((v + 27).to_bytes(32, "little"))
input_bytes.extend(r.to_bytes(32, "little"))
input_bytes.extend(s.to_bytes(32, "little"))
input_rlc = RLC(bytes(reversed(input_bytes)), randomness_keccak, n_bytes=128).expr()
output_bytes = int.from_bytes(address, "big").to_bytes(32, "little")
output_rlc = RLC(bytes(reversed(output_bytes)), randomness_keccak, n_bytes=32).expr()
rlc_data = PrecompileRlcData(input_rlc, output_rlc)

aux_data = [
Word(msg_hash),
Word(v + 27),
Word(r),
Word(s),
FQ(int.from_bytes(address, "big")),
rlc_data,
randomness_keccak,
]

# assign sig_table
Expand Down
Loading
Loading