Skip to content

Commit 592ae79

Browse files
anvacaruanvacaru
committed
add fetch productions for access opcodes
1 parent aa7e727 commit 592ae79

File tree

3 files changed

+72
-21
lines changed

3 files changed

+72
-21
lines changed

‎src/kontrol/foundry.py

Lines changed: 34 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@
1717
from typing import TYPE_CHECKING
1818

1919
import tomlkit
20-
from kevm_pyk.kevm import KEVM, KEVMNodePrinter, KEVMSemantics
20+
from kevm_pyk.kevm import KEVM, CustomStep, KEVMNodePrinter, KEVMSemantics
2121
from kevm_pyk.utils import byte_offset_to_lines, legacy_explore, print_failure_info, print_model
2222
from pyk.cterm import CTerm
2323
from pyk.kast.inner import KApply, KInner, KSequence, KSort, KToken, KVariable, Subst, build_assoc
@@ -103,21 +103,26 @@ class KontrolSemantics(KEVMSemantics):
103103
def __init__(
104104
self, auto_abstract_gas: bool = False, allow_symbolic_program: bool = False, provider_url: str | None = None
105105
) -> None:
106-
super().__init__(auto_abstract_gas=auto_abstract_gas, allow_symbolic_program=allow_symbolic_program)
106+
107+
custom_steps = (
108+
CustomStep(self._rename_pattern, self._exec_rename_custom_step),
109+
CustomStep(self._forget_branch_pattern, self._exec_forget_custom_step),
110+
CustomStep(self._call_fork_pattern, self._exec_fork_call_custom_step),
111+
CustomStep(self._sload_fork_pattern, self._exec_fork_sload_custom_step),
112+
)
113+
114+
super().__init__(
115+
auto_abstract_gas=auto_abstract_gas,
116+
allow_symbolic_program=allow_symbolic_program,
117+
custom_step_definitions=custom_steps,
118+
)
107119

108120
self._external_accounts = set()
109121
if provider_url:
110122
self._provider = Web3Providers.get_provider(provider_url)
111123
else:
112124
self._provider = None
113125

114-
self._custom_step_definitions = self._custom_step_definitions + (
115-
(self._rename_pattern, self._exec_rename_custom_step),
116-
(self._forget_branch_pattern, self._exec_forget_custom_step),
117-
(self._call_fork_pattern, self._exec_fork_call_custom_step),
118-
(self._sload_fork_pattern, self._exec_fork_sload_custom_step),
119-
)
120-
121126
@staticmethod
122127
def cut_point_rules(
123128
break_on_jumpi: bool,
@@ -133,7 +138,11 @@ def cut_point_rules(
133138
cut_point_rules.extend(
134139
[
135140
'EVM.call.false',
136-
'FOUNDRY.sload.false',
141+
'FOUNDRY.sload.w3provider',
142+
'FOUNDRY.balance.w3provider',
143+
'FOUNDRY.extcodesize.w3provider',
144+
'FOUNDRY.extcodehash.w3provider',
145+
'FOUNDRY.extcodecopy.w3provider',
137146
]
138147
)
139148
return cut_point_rules + KEVMSemantics.cut_point_rules(
@@ -201,6 +210,16 @@ def _sload_fork_pattern(self) -> KSequence:
201210
]
202211
)
203212

213+
@property
214+
def _balance_fork_pattern(self) -> KSequence:
215+
return KSequence(
216+
[
217+
KApply('FETCH_ACCOUNT_BALANCE', KVariable('###ACCTID')),
218+
KApply('#push_EVM_InternalOp'),
219+
KVariable('###CONTINUATION'),
220+
]
221+
)
222+
204223
def _exec_rename_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -> KCFGExtendResult | None:
205224
# Extract the target var and new name from the substitution
206225
target_var = subst['###RENAME_TARGET']
@@ -357,6 +376,10 @@ def _exec_fork_call_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbo
357376
all_accounts.append(account)
358377
new_accounts_cell = KEVM.accounts(all_accounts)
359378

379+
if account_code is KToken('b""', sort='Bytes'):
380+
_LOGGER.warning(f'Account {target_address.token} has no code available. Continuing execution.')
381+
return None
382+
360383
# Build a new continuation, replacing the account code placeholder with the fetched code.
361384
continuation = KSequence(
362385
[
@@ -390,7 +413,7 @@ def _exec_fork_call_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbo
390413
new_cterm = CTerm.from_kast(set_cell(new_cterm.kast, 'K_CELL', continuation))
391414

392415
_LOGGER.info(f'Successfully read account {address_value} from provider and added it to the state')
393-
return Step(CTerm(new_cterm.config, cterm.constraints), 1, (), ['call.false'], cut=True)
416+
return Step(CTerm(new_cterm.config, cterm.constraints), 1, (), ['call.true'], cut=True)
394417

395418
def _exec_fork_sload_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -> KCFGExtendResult | None:
396419
if self._provider is None:

‎src/kontrol/kdist/foundry.md

Lines changed: 33 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ module FOUNDRY
3131
<foundry>
3232
<kevm/>
3333
<forkedAccounts> .Set </forkedAccounts>
34+
<allowWeb3Connection> false </allowWeb3Connection>
3435
<stackChecks> true </stackChecks>
3536
<cheatcodes/>
3637
<KEVMTracing/>
@@ -57,20 +58,45 @@ module FOUNDRY
5758
rule #accountHasStorageSlot (_,_) => false [owise]
5859
5960
// Comment: Ideally, rules below would be available only when --fork-url is provided.
60-
syntax KItem ::= "FETCH_ACCOUNT_STORAGE" Int Int [symbol(FETCH_ACCOUNT_STORAGE)]
61-
// | "FETCH_ACCOUNT_BALANCE" Int [symbol(FETCH_ACCOUNT_BALANCE)]
62-
// | "FETCH_ACCOUNT_CODE" Int [symbol(FETCH_ACCOUNT_CODE)]
63-
// | "FETCH_ACCOUNT_CODE_SIZE" Int [symbol(FETCH_ACCOUNT_CODE_SIZE)]
64-
// | "FETCH_ACCOUNT_CODE_HASH" Int [symbol(FETCH_ACCOUNT_CODE_HASH)]
65-
// --------------------------------------------------------------------------------
66-
rule [sload.false]:
61+
// For this I'm using the <allowWeb3Connection> cell
62+
syntax KItem ::= "FETCH_ACCOUNT_STORAGE" Int Int [symbol(FETCH_ACCOUNT_STORAGE) ]
63+
| "FETCH_ACCOUNT_BALANCE" Int [symbol(FETCH_ACCOUNT_BALANCE) ]
64+
| "FETCH_ACCOUNT_CODE_SIZE" Int [symbol(FETCH_ACCOUNT_CODE_SIZE)]
65+
| "FETCH_ACCOUNT_CODE_HASH" Int [symbol(FETCH_ACCOUNT_CODE_HASH)]
66+
| "FETCH_ACCOUNT_CODE" Int Int Int Int [symbol(FETCH_ACCOUNT_CODE)]
67+
// ----------------------------------------------------------------------------------
68+
rule [sload.w3provider]:
6769
<k> SLOAD INDEX => FETCH_ACCOUNT_STORAGE ACCT INDEX ~> #push ... </k>
6870
<id> ACCT </id>
71+
<allowWeb3Connection> true </allowWeb3Connection>
6972
<forkedAccounts> FA </forkedAccounts>
7073
requires notBool #accountInState(ACCT)
7174
orBool (ACCT in FA andBool notBool #accountHasStorageSlot(ACCT, INDEX))
7275
[priority(30)]
7376
77+
rule [balance.w3provider]:
78+
<k> BALANCE ACCT => #accessAccounts ACCT ~> FETCH_ACCOUNT_BALANCE ACCT ~> #push ... </k>
79+
<allowWeb3Connection> true </allowWeb3Connection>
80+
requires notBool #accountInState(ACCT)
81+
[priority(30)]
82+
83+
rule [extcodesize.w3provider]:
84+
<k> EXTCODESIZE ACCT => #accessAccounts ACCT ~> FETCH_ACCOUNT_CODE_SIZE ACCT ~> #push ... </k>
85+
<allowWeb3Connection> true </allowWeb3Connection>
86+
requires notBool #accountInState(ACCT)
87+
[priority(30)]
88+
89+
rule [extcodecopy.w3provider]:
90+
<k> EXTCODECOPY ACCT MEMSTART PGMSTART WIDTH => #accessAccounts ACCT ~> FETCH_ACCOUNT_CODE ACCT MEMSTART PGMSTART WIDTH ... </k>
91+
<allowWeb3Connection> true </allowWeb3Connection>
92+
requires notBool #accountInState(ACCT)
93+
[priority(30)]
94+
95+
rule [extcodehash.w3provider]:
96+
<k> EXTCODEHASH ACCT => #accessAccounts ACCT ~> FETCH_ACCOUNT_CODE_HASH ACCT ~> #push ... </k>
97+
<allowWeb3Connection> true </allowWeb3Connection>
98+
requires notBool #accountInState(ACCT)
99+
[priority(30)]
74100
endmodule
75101
```
76102

‎src/kontrol/prove.py

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -399,11 +399,11 @@ def create_kcfg_explore() -> KCFGExplore:
399399
):
400400
options.config_type = ConfigType.SUMMARY_CONFIG
401401

402-
w3 = None
402+
provider = None
403403
block_metadata = None
404404
if options.fork_url:
405-
w3 = Web3Providers.get_provider(options.fork_url)
406-
block_metadata = get_block_metadata(w3)
405+
provider = Web3Providers.get_provider(options.fork_url)
406+
block_metadata = get_block_metadata(provider)
407407

408408
proof = method_to_apr_proof(
409409
test=test,
@@ -1067,6 +1067,7 @@ def _init_cterm(
10671067
'RECORDEDTRACE_CELL': FALSE,
10681068
'TRACEDATA_CELL': KApply('.List'),
10691069
'FORKEDACCOUNTS_CELL': set_empty(),
1070+
'ALLOWWEB3CONNECTION_CELL': FALSE,
10701071
}
10711072

10721073
storage_constraints: list[KApply] = []
@@ -1090,6 +1091,7 @@ def _init_cterm(
10901091
init_subst.update(init_subst_test)
10911092
if block_metadata:
10921093
init_subst_fork_data = {
1094+
'ALLOWWEB3CONNECTION_CELL': TRUE,
10931095
'NUMBER_CELL': token(block_metadata['block_number']),
10941096
'CHAINID_CELL': token(block_metadata['chain_id']),
10951097
'GASLIMIT_CELL': token(block_metadata['gas_limit']),

0 commit comments

Comments
 (0)