Merge remote-tracking branch 'origin/master' into release

Author: rv-auditor

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

@@ -1597,16 +1597,11 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
     syntax KItem ::= "#accessStorage" Account Int
  // ---------------------------------------------
     rule <k> #accessStorage ACCT INDEX => .K ... </k>
-         <accessedStorage> ... ACCT |-> (TS:Set => TS |Set SetItem(INDEX)) ... </accessedStorage>
+         <accessedStorage> TS => TS[ACCT <- {TS[ACCT] orDefault .Set}:>Set |Set SetItem(INDEX)] </accessedStorage>
          <schedule> SCHED </schedule>
          requires Ghasaccesslist << SCHED >>
          [preserves-definedness]
 
-    rule <k> #accessStorage ACCT INDEX => .K ... </k>
-         <accessedStorage> TS => TS[ACCT <- SetItem(INDEX)] </accessedStorage>
-         <schedule> SCHED </schedule>
-      requires Ghasaccesslist << SCHED >> andBool notBool ACCT in_keys(TS)
-
     rule <k> #accessStorage _ _ => .K ... </k>
          <schedule> SCHED </schedule>
       requires notBool Ghasaccesslist << SCHED >>
@@ -2310,7 +2305,8 @@ Access List Gas
          <schedule> SCHED </schedule>
       requires Ghasaccesslist << SCHED >> andBool #usesAccessList(OP)
 
-    rule <k> #access [ _ , _ ] => .K ... </k> <schedule> _ </schedule> [owise]
+    rule <k> #access [ OP , _ ] => .K ... </k> <schedule> SCHED </schedule>
+      requires notBool (Ghasaccesslist << SCHED >> andBool #usesAccessList(OP))
 
     syntax InternalOp ::= #gasAccess ( Schedule, OpCode ) [symbol(#gasAccess)]
  // --------------------------------------------------------------------------

kevm-pyk/src/kevm_pyk/summarizer.py

@@ -433,8 +433,7 @@ def _build_spec(
         # This is because #push doesn't handle `.Account`. And it's okay to be Int for other opcodes.
         _init_subst['CALLER_CELL'] = KVariable('CALLER_CELL', KSort('Int'))  # CALLER_CELL should be Int for CALLER.
         _init_subst['ORIGIN_CELL'] = KVariable('ORIGIN_CELL', KSort('Int'))  # ORIGIN_CELL should be Int for ORIGIN.
-        inf_gas_cell = KEVM.inf_gas(KVariable('GAS_CELL', KSort('Gas')))
-        _init_subst['GAS_CELL'] = inf_gas_cell  # inf_gas to reduce the computation cost.
+        _init_subst['GAS_CELL'] = KEVM.inf_gas(KVariable('GAS_CELL', 'Gas'))  # SLOAD & SSTORE must use infinite gas.
         _init_subst.update(init_map)
         init_subst = CSubst(Subst(_init_subst), init_constraints)
 
@@ -467,6 +466,9 @@ def _le(a: KInner, b: KInner) -> KInner:
         init_subst: dict[str, KInner] = {}
         final_subst: dict[str, KInner] = {}
 
+        if opcode_symbol == 'SSTORE':
+            init_subst['STATIC_CELL'] = KToken('false', KSort('Bool'))
+
         if opcode_symbol in NOT_USEGAS_OPCODES:
             # TODO: Should allow infGas to calculate gas. Skip for now.
             init_subst['USEGAS_CELL'] = KToken('false', KSort('Bool'))
@@ -572,7 +574,7 @@ def create_kcfg_explore() -> KCFGExplore:
                     proof,
                     create_kcfg_explore=create_kcfg_explore,
                     max_depth=1,
-                    max_iterations=None,
+                    max_iterations=300,
                     cut_point_rules=KEVMSemantics.cut_point_rules(
                         break_on_jumpi=False,
                         break_on_jump=False,