Optimizing storage requirement to create an existing acccount

runtimeverification · Jan 23, 2025 · 983a41a · 983a41a
1 parent 07578e9
commit 983a41a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -817,11 +817,11 @@ These are just used by the other operators for shuffling local execution state a
            <acctID>      ACCT      </acctID>
            <code>        CODE      </code>
            <nonce>       0         </nonce>
-           <storage>     STORAGE   </storage>
+           <storage>     .Map   </storage>
            <origStorage> _ => .Map </origStorage>
            ...
          </account>
-      requires lengthBytes(CODE) ==Int 0 andBool STORAGE ==K .Map
+      requires lengthBytes(CODE) ==Int 0
 ```
 
 -   `#transferFunds` moves money from one account into another, creating the destination account if it doesn't exist.