Skip to content

Commit

Permalink
more specs
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 Mar 18, 2022
1 parent 1ae0965 commit c75ac23
Show file tree
Hide file tree
Showing 22 changed files with 918 additions and 13 deletions.
4 changes: 3 additions & 1 deletion crates/fv/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,10 @@ pub fn run_spec(name: &str, src_path: &str, src: &str, spec: &str) -> Result<(),
let out = Command::new("kevm")
.arg("prove")
.arg(spec_path.to_str().unwrap())
.arg("--backend haskell")
.arg("--backend")
.arg("haskell")
.arg("--format-failures")
// we should define out own verification module
.arg("--directory")
.arg("tests/specs/erc20/verification/haskell")
.env("PATH", format!(".build/usr/bin:{}", path))
Expand Down
24 changes: 22 additions & 2 deletions crates/fv/tests/specs.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,14 @@ macro_rules! test_spec {
let src = fe_test_files::fixture(concat!("kspecs/", $src_path));
let spec = fe_test_files::fixture(concat!("kspecs/", $spec_path));

fv::run_spec(&stringify!($name).replace("_", "-"), $src_path, &src, &spec)
.expect("spec failed");
if let Err(output) = fv::run_spec(
&stringify!($name).replace("_", "-"),
$src_path,
&src,
&spec
) {
panic!("{}", output)
}
}
};
}
Expand Down Expand Up @@ -44,3 +50,17 @@ test_spec! { sanity_returns_in_cond2, "sanity/foo.fe", "sanity/returns_in_cond2.
test_spec_invalid! { sanity_returns_42_invalid, "sanity/foo.fe", "sanity/returns_42_invalid.k" }
test_spec_invalid! { sanity_returns_in_invalid, "sanity/foo.fe", "sanity/returns_in_invalid.k" }
test_spec_invalid! { sanity_returns_in_cond2_invalid, "sanity/foo.fe", "sanity/returns_in_cond2_invalid.k" }

// encode/decode success
test_spec! { abi_u256, "abi/foo.fe", "abi/u256.k" }
test_spec! { abi_u8, "abi/foo.fe", "abi/u8.k" }
test_spec! { abi_address, "abi/foo.fe", "abi/address.k" }
test_spec! { abi_address_u16, "abi/foo.fe", "abi/address_u16.k" }

// decode revert
test_spec! { abi_address_revert, "abi/foo.fe", "abi/address_revert.k" }
test_spec! { abi_address_u16_revert_0, "abi/foo.fe", "abi/address_u16_revert_0.k" }
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" }
105 changes: 105 additions & 0 deletions crates/test-files/fixtures/kspecs/abi/address.k
View file
Original file line number Diff line number Diff line change
@@ -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, OUT) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => ?_ </touchedAccounts>

<callState>
<program> #parseByteStack($Foo::RUNTIME) </program>
<jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>

<id> ACCT_ID </id> // contract owner
<caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender

<callData> #abiCallData("_address", #address(IN)) </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($Foo::RUNTIME) </code>
<storage> _ </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 IN andBool IN <Int (2 ^Int 160)
andBool IN ==Int OUT

endmodule

106 changes: 106 additions & 0 deletions crates/test-files/fixtures/kspecs/abi/address_revert.k
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,106 @@
module $TEST_NAME
imports VERIFICATION

claim

<kevm>
<k> #execute => #halt </k>
<exit-code> 1 </exit-code>
<mode> NORMAL </mode>
<schedule> ISTANBUL </schedule>

<ethereum>
<evm>
// todo: check code
<output> _ => b".6\xa7\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x03" </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => ?_ </touchedAccounts>

<callState>
<program> #parseByteStack($Foo::RUNTIME) </program>
<jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>

<id> ACCT_ID </id> // contract owner
<caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender

// address sig ++ input
<callData> #buf(4, 652482574) ++ #buf(32, IN) </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($Foo::RUNTIME) </code>
<storage> _ </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 (2 ^Int 160) <=Int IN andBool IN <Int (2 ^Int 256)

endmodule

107 changes: 107 additions & 0 deletions crates/test-files/fixtures/kspecs/abi/address_u16.k
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,107 @@
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, OUT_ADDR) ++ #buf(32, OUT_U16) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => ?_ </touchedAccounts>

<callState>
<program> #parseByteStack($Foo::RUNTIME) </program>
<jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>

<id> ACCT_ID </id> // contract owner
<caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender

<callData> #abiCallData("_address_u16", #address(IN_ADDR), #uint16(IN_U16)) </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($Foo::RUNTIME) </code>
<storage> _ </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 IN_ADDR andBool IN_ADDR <Int (2 ^Int 160)
andBool 0 <=Int IN_U16 andBool IN_U16 <Int (2 ^Int 16)
andBool IN_ADDR ==Int OUT_ADDR
andBool IN_U16 ==Int OUT_U16

endmodule

Loading

0 comments on commit c75ac23

Please sign in to comment.