sol map

ethereum · Mar 29, 2022 · 5db077d · 5db077d
1 parent 8dcf631
commit 5db077d
Show file tree

Hide file tree

Showing 4 changed files with 119 additions and 1 deletion.
diff --git a/crates/fv/tests/specs.rs b/crates/fv/tests/specs.rs
@@ -64,3 +64,4 @@ test_spec! { abi_address_u16_revert_1, "abi/foo.fe", "abi/address_u16_revert_1.k
 
 // storage
 test_spec! { store_u256, "storage/foo.fe", "storage/store_u256.k" }
+test_spec! { store_map, "storage/foo.fe", "storage/store_sol_map.k" }
diff --git a/crates/test-files/fixtures/kspecs/storage/foo.fe b/crates/test-files/fixtures/kspecs/storage/foo.fe
@@ -7,3 +7,15 @@ contract StoreU256:
         unsafe:
             evm::mstore(0, self.my_u256)
             evm::return_mem(0, 32)
+
+
+contract StoreSolMap:
+    pub fn __call__(self):
+        unsafe:
+            let key: u256 = evm::call_data_load(0)
+            evm::mstore(0, key)
+            evm::mstore(32, 0)
+            let slot: u256 = evm::keccak256_mem(0, 64)
+            let value: u256 = evm::sload(slot)
+            evm::mstore(0, value)
+            evm::return_mem(0, 32)
diff --git a/crates/test-files/fixtures/kspecs/storage/store_sol_map.k b/crates/test-files/fixtures/kspecs/storage/store_sol_map.k
@@ -0,0 +1,105 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> #buf(32, VAL) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($StoreSolMap::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($StoreSolMap::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #buf(32, KEY) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($StoreSolMap::RUNTIME) </code>
+                        <storage> #hashedLocation("Solidity", 0, KEY) |-> VAL _:Map </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0 <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 0 <=Int KEY   andBool KEY    <Int (2 ^Int 256)
+        andBool 0 <=Int VAL   andBool VAL    <Int (2 ^Int 256)
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/storage/store_u256.k b/crates/test-files/fixtures/kspecs/storage/store_u256.k
@@ -98,7 +98,7 @@ module $TEST_NAME
         andBool 0 <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
         andBool 0 <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
         andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
-        andBool 0 <=Int MY_U256  andBool MY_U256  <Int (2 ^Int 256)
+        andBool 0 <=Int MY_U256    andBool MY_U256    <Int (2 ^Int 256)
         andBool MY_U256 ==Int OUT
 
 endmodule