Skip to content

Commit

Permalink
fe map wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@g-r-a-n-t
g-r-a-n-t committed Apr 1, 2022
1 parent 5db077d commit 95dcbb9
Show file tree
Hide file tree
Showing 4 changed files with 124 additions and 5 deletions.
3 changes: 2 additions & 1 deletion crates/fv/tests/specs.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,4 +64,5 @@ 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" }
test_spec! { store_sol_map, "storage/foo.fe", "storage/store_sol_map.k" }
test_spec! { store_fe_map, "storage/foo.fe", "storage/store_fe_map.k" }
11 changes: 10 additions & 1 deletion crates/test-files/fixtures/kspecs/storage/foo.fe
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ contract StoreU256:


contract StoreSolMap:
pub fn __call__(self):
pub fn __call__():
unsafe:
let key: u256 = evm::call_data_load(0)
evm::mstore(0, key)
Expand All @@ -19,3 +19,12 @@ contract StoreSolMap:
let value: u256 = evm::sload(slot)
evm::mstore(0, value)
evm::return_mem(0, 32)

contract StoreFeMap:
my_map: Map<u256, u256>

pub fn __call__(self):
unsafe:
let key: u256 = evm::call_data_load(0)
evm::mstore(0, self.my_map[key])
evm::return_mem(0, 32)
109 changes: 109 additions & 0 deletions crates/test-files/fixtures/kspecs/storage/store_fe_map.k
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,109 @@
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($StoreFeMap::RUNTIME) </program>
<jumpDests> #computeValidJumpDests(#parseByteStack($StoreFeMap::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($StoreFeMap::RUNTIME) </code>
<storage> #hashedLocation("Fe", 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 40 <=Int KEY andBool KEY <Int 50
//andBool 0 <=Int KEY andBool KEY <Int (2 ^Int 256)
//andBool 42 ==Int KEY
andBool 40 <=Int VAL andBool VAL <Int 50
//andBool 0 <=Int VAL andBool VAL <Int (2 ^Int 256)
//andBool 26 ==Int VAL

endmodule

6 changes: 3 additions & 3 deletions crates/yulgen/src/runtime/functions/data.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ pub fn all() -> Vec<yul::Statement> {
]
}

/// Returns the highest available pointer.
/// Returns the highest available pointerhttps://buy.gazelle.com/collections/ipads?_=pf&pf_v_model=iPad%20Pro%2012.9%204th%20Gen.
pub fn avail() -> yul::Statement {
function_definition! {
function avail() -> ptr {
Expand Down Expand Up @@ -315,7 +315,7 @@ pub fn bytes_sloadn() -> yul::Statement {
function bytes_sloadn(sptr, size) -> val {
(let word_ptr := div(sptr, 32))
(let bytes_offset := mod(sptr, 32))
(val := sloadn(word_ptr, bytes_offset, size))
(val := sload(word_ptr))
}
}
}
Expand Down Expand Up @@ -354,7 +354,7 @@ pub fn map_value_ptr() -> yul::Statement {
(mstore(ptr, a))
(mstore((add(ptr, 32)), b))
(let hash := keccak256(ptr, 64))
(return_val := set_zero(248, 256, hash))
(return_val := mul((div(hash, 256)), 256))
}
}
}
Expand Down

0 comments on commit 95dcbb9

Please sign in to comment.