Skip to content

Commit c75ac23

Browse files
g-r-a-n-tg-r-a-n-t
committed
more specs
1 parent 1ae0965 commit c75ac23

22 files changed

+918
-13
lines changed

‎crates/fv/src/lib.rs‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,10 @@ pub fn run_spec(name: &str, src_path: &str, src: &str, spec: &str) -> Result<(),
2525
let out = Command::new("kevm")
2626
.arg("prove")
2727
.arg(spec_path.to_str().unwrap())
28-
.arg("--backend haskell")
28+
.arg("--backend")
29+
.arg("haskell")
2930
.arg("--format-failures")
31+
// we should define out own verification module
3032
.arg("--directory")
3133
.arg("tests/specs/erc20/verification/haskell")
3234
.env("PATH", format!(".build/usr/bin:{}", path))

‎crates/fv/tests/specs.rs‎

Lines changed: 22 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,14 @@ macro_rules! test_spec {
88
let src = fe_test_files::fixture(concat!("kspecs/", $src_path));
99
let spec = fe_test_files::fixture(concat!("kspecs/", $spec_path));
1010

11-
fv::run_spec(&stringify!($name).replace("_", "-"), $src_path, &src, &spec)
12-
.expect("spec failed");
11+
if let Err(output) = fv::run_spec(
12+
&stringify!($name).replace("_", "-"),
13+
$src_path,
14+
&src,
15+
&spec
16+
) {
17+
panic!("{}", output)
18+
}
1319
}
1420
};
1521
}
@@ -44,3 +50,17 @@ test_spec! { sanity_returns_in_cond2, "sanity/foo.fe", "sanity/returns_in_cond2.
4450
test_spec_invalid! { sanity_returns_42_invalid, "sanity/foo.fe", "sanity/returns_42_invalid.k" }
4551
test_spec_invalid! { sanity_returns_in_invalid, "sanity/foo.fe", "sanity/returns_in_invalid.k" }
4652
test_spec_invalid! { sanity_returns_in_cond2_invalid, "sanity/foo.fe", "sanity/returns_in_cond2_invalid.k" }
53+
54+
// encode/decode success
55+
test_spec! { abi_u256, "abi/foo.fe", "abi/u256.k" }
56+
test_spec! { abi_u8, "abi/foo.fe", "abi/u8.k" }
57+
test_spec! { abi_address, "abi/foo.fe", "abi/address.k" }
58+
test_spec! { abi_address_u16, "abi/foo.fe", "abi/address_u16.k" }
59+
60+
// decode revert
61+
test_spec! { abi_address_revert, "abi/foo.fe", "abi/address_revert.k" }
62+
test_spec! { abi_address_u16_revert_0, "abi/foo.fe", "abi/address_u16_revert_0.k" }
63+
test_spec! { abi_address_u16_revert_1, "abi/foo.fe", "abi/address_u16_revert_1.k" }
64+
65+
// storage
66+
test_spec! { store_u256, "storage/foo.fe", "storage/store_u256.k" }

‎crates/test-files/fixtures/kspecs/abi/address.k‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
module $TEST_NAME
2+
imports VERIFICATION
3+
4+
claim
5+
6+
<kevm>
7+
<k> #execute => #halt </k>
8+
<exit-code> 1 </exit-code>
9+
<mode> NORMAL </mode>
10+
<schedule> ISTANBUL </schedule>
11+
12+
<ethereum>
13+
<evm>
14+
<output> _ => #buf(32, OUT) </output>
15+
<statusCode> _ => EVMC_SUCCESS </statusCode>
16+
<endPC> _ => ?_ </endPC>
17+
<callStack> _ </callStack>
18+
<interimStates> _ </interimStates>
19+
<touchedAccounts> _ => ?_ </touchedAccounts>
20+
21+
<callState>
22+
<program> #parseByteStack($Foo::RUNTIME) </program>
23+
<jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>
24+
25+
<id> ACCT_ID </id> // contract owner
26+
<caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
27+
28+
<callData> #abiCallData("_address", #address(IN)) </callData>
29+
30+
<callValue> 0 </callValue>
31+
<wordStack> .WordStack => ?_ </wordStack>
32+
<localMem> .Memory => ?_ </localMem>
33+
<pc> 0 => ?_ </pc>
34+
<gas> #gas(_VGAS) => ?_ </gas>
35+
<memoryUsed> 0 => ?_ </memoryUsed>
36+
<callGas> _ => ?_ </callGas>
37+
38+
<static> false </static> // NOTE: non-static call
39+
<callDepth> CALL_DEPTH </callDepth>
40+
</callState>
41+
42+
<substate>
43+
<selfDestruct> _ </selfDestruct>
44+
<log> _ </log>
45+
<refund> _ </refund> // TODO: more detail
46+
<accessedAccounts> _ => ?_ </accessedAccounts>
47+
<accessedStorage> _ => ?_ </accessedStorage>
48+
</substate>
49+
50+
<gasPrice> _ </gasPrice>
51+
<origin> ORIGIN_ID </origin> // who fires tx
52+
53+
<blockhashes> _ </blockhashes>
54+
<block>
55+
<previousHash> _ </previousHash>
56+
<ommersHash> _ </ommersHash>
57+
<coinbase> _ </coinbase>
58+
<stateRoot> _ </stateRoot>
59+
<transactionsRoot> _ </transactionsRoot>
60+
<receiptsRoot> _ </receiptsRoot>
61+
<logsBloom> _ </logsBloom>
62+
<difficulty> _ </difficulty>
63+
<number> _ </number>
64+
<gasLimit> _ </gasLimit>
65+
<gasUsed> _ </gasUsed>
66+
<timestamp> _ </timestamp>
67+
<extraData> _ </extraData>
68+
<mixHash> _ </mixHash>
69+
<blockNonce> _ </blockNonce>
70+
<ommerBlockHeaders> _ </ommerBlockHeaders>
71+
</block>
72+
</evm>
73+
74+
<network>
75+
<chainID> _ </chainID>
76+
77+
<activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
78+
79+
<accounts>
80+
<account>
81+
<acctID> ACCT_ID </acctID>
82+
<balance> _ </balance>
83+
<code> #parseByteStack($Foo::RUNTIME) </code>
84+
<storage> _ </storage>
85+
<origStorage> _ </origStorage>
86+
<nonce> _ </nonce>
87+
</account>
88+
</accounts>
89+
90+
<txOrder> _ </txOrder>
91+
<txPending> _ </txPending>
92+
<messages> _ </messages>
93+
</network>
94+
</ethereum>
95+
</kevm>
96+
97+
requires 0 <=Int ACCT_ID andBool ACCT_ID <Int (2 ^Int 160)
98+
andBool 0 <=Int CALLER_ID andBool CALLER_ID <Int (2 ^Int 160)
99+
andBool 0 <=Int ORIGIN_ID andBool ORIGIN_ID <Int (2 ^Int 160)
100+
andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
101+
andBool 0 <=Int IN andBool IN <Int (2 ^Int 160)
102+
andBool IN ==Int OUT
103+
104+
endmodule
105+

‎crates/test-files/fixtures/kspecs/abi/address_revert.k‎

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
module $TEST_NAME
2+
imports VERIFICATION
3+
4+
claim
5+
6+
<kevm>
7+
<k> #execute => #halt </k>
8+
<exit-code> 1 </exit-code>
9+
<mode> NORMAL </mode>
10+
<schedule> ISTANBUL </schedule>
11+
12+
<ethereum>
13+
<evm>
14+
// todo: check code
15+
<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>
16+
<statusCode> _ => EVMC_REVERT </statusCode>
17+
<endPC> _ => ?_ </endPC>
18+
<callStack> _ </callStack>
19+
<interimStates> _ </interimStates>
20+
<touchedAccounts> _ => ?_ </touchedAccounts>
21+
22+
<callState>
23+
<program> #parseByteStack($Foo::RUNTIME) </program>
24+
<jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>
25+
26+
<id> ACCT_ID </id> // contract owner
27+
<caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
28+
29+
// address sig ++ input
30+
<callData> #buf(4, 652482574) ++ #buf(32, IN) </callData>
31+
32+
<callValue> 0 </callValue>
33+
<wordStack> .WordStack => ?_ </wordStack>
34+
<localMem> .Memory => ?_ </localMem>
35+
<pc> 0 => ?_ </pc>
36+
<gas> #gas(_VGAS) => ?_ </gas>
37+
<memoryUsed> 0 => ?_ </memoryUsed>
38+
<callGas> _ => ?_ </callGas>
39+
40+
<static> false </static> // NOTE: non-static call
41+
<callDepth> CALL_DEPTH </callDepth>
42+
</callState>
43+
44+
<substate>
45+
<selfDestruct> _ </selfDestruct>
46+
<log> _ </log>
47+
<refund> _ </refund> // TODO: more detail
48+
<accessedAccounts> _ => ?_ </accessedAccounts>
49+
<accessedStorage> _ => ?_ </accessedStorage>
50+
</substate>
51+
52+
<gasPrice> _ </gasPrice>
53+
<origin> ORIGIN_ID </origin> // who fires tx
54+
55+
<blockhashes> _ </blockhashes>
56+
<block>
57+
<previousHash> _ </previousHash>
58+
<ommersHash> _ </ommersHash>
59+
<coinbase> _ </coinbase>
60+
<stateRoot> _ </stateRoot>
61+
<transactionsRoot> _ </transactionsRoot>
62+
<receiptsRoot> _ </receiptsRoot>
63+
<logsBloom> _ </logsBloom>
64+
<difficulty> _ </difficulty>
65+
<number> _ </number>
66+
<gasLimit> _ </gasLimit>
67+
<gasUsed> _ </gasUsed>
68+
<timestamp> _ </timestamp>
69+
<extraData> _ </extraData>
70+
<mixHash> _ </mixHash>
71+
<blockNonce> _ </blockNonce>
72+
<ommerBlockHeaders> _ </ommerBlockHeaders>
73+
</block>
74+
</evm>
75+
76+
<network>
77+
<chainID> _ </chainID>
78+
79+
<activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
80+
81+
<accounts>
82+
<account>
83+
<acctID> ACCT_ID </acctID>
84+
<balance> _ </balance>
85+
<code> #parseByteStack($Foo::RUNTIME) </code>
86+
<storage> _ </storage>
87+
<origStorage> _ </origStorage>
88+
<nonce> _ </nonce>
89+
</account>
90+
</accounts>
91+
92+
<txOrder> _ </txOrder>
93+
<txPending> _ </txPending>
94+
<messages> _ </messages>
95+
</network>
96+
</ethereum>
97+
</kevm>
98+
99+
requires 0 <=Int ACCT_ID andBool ACCT_ID <Int (2 ^Int 160)
100+
andBool 0 <=Int CALLER_ID andBool CALLER_ID <Int (2 ^Int 160)
101+
andBool 0 <=Int ORIGIN_ID andBool ORIGIN_ID <Int (2 ^Int 160)
102+
andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
103+
andBool (2 ^Int 160) <=Int IN andBool IN <Int (2 ^Int 256)
104+
105+
endmodule
106+

‎crates/test-files/fixtures/kspecs/abi/address_u16.k‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
module $TEST_NAME
2+
imports VERIFICATION
3+
4+
claim
5+
6+
<kevm>
7+
<k> #execute => #halt </k>
8+
<exit-code> 1 </exit-code>
9+
<mode> NORMAL </mode>
10+
<schedule> ISTANBUL </schedule>
11+
12+
<ethereum>
13+
<evm>
14+
<output> _ => #buf(32, OUT_ADDR) ++ #buf(32, OUT_U16) </output>
15+
<statusCode> _ => EVMC_SUCCESS </statusCode>
16+
<endPC> _ => ?_ </endPC>
17+
<callStack> _ </callStack>
18+
<interimStates> _ </interimStates>
19+
<touchedAccounts> _ => ?_ </touchedAccounts>
20+
21+
<callState>
22+
<program> #parseByteStack($Foo::RUNTIME) </program>
23+
<jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>
24+
25+
<id> ACCT_ID </id> // contract owner
26+
<caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
27+
28+
<callData> #abiCallData("_address_u16", #address(IN_ADDR), #uint16(IN_U16)) </callData>
29+
30+
<callValue> 0 </callValue>
31+
<wordStack> .WordStack => ?_ </wordStack>
32+
<localMem> .Memory => ?_ </localMem>
33+
<pc> 0 => ?_ </pc>
34+
<gas> #gas(_VGAS) => ?_ </gas>
35+
<memoryUsed> 0 => ?_ </memoryUsed>
36+
<callGas> _ => ?_ </callGas>
37+
38+
<static> false </static> // NOTE: non-static call
39+
<callDepth> CALL_DEPTH </callDepth>
40+
</callState>
41+
42+
<substate>
43+
<selfDestruct> _ </selfDestruct>
44+
<log> _ </log>
45+
<refund> _ </refund> // TODO: more detail
46+
<accessedAccounts> _ => ?_ </accessedAccounts>
47+
<accessedStorage> _ => ?_ </accessedStorage>
48+
</substate>
49+
50+
<gasPrice> _ </gasPrice>
51+
<origin> ORIGIN_ID </origin> // who fires tx
52+
53+
<blockhashes> _ </blockhashes>
54+
<block>
55+
<previousHash> _ </previousHash>
56+
<ommersHash> _ </ommersHash>
57+
<coinbase> _ </coinbase>
58+
<stateRoot> _ </stateRoot>
59+
<transactionsRoot> _ </transactionsRoot>
60+
<receiptsRoot> _ </receiptsRoot>
61+
<logsBloom> _ </logsBloom>
62+
<difficulty> _ </difficulty>
63+
<number> _ </number>
64+
<gasLimit> _ </gasLimit>
65+
<gasUsed> _ </gasUsed>
66+
<timestamp> _ </timestamp>
67+
<extraData> _ </extraData>
68+
<mixHash> _ </mixHash>
69+
<blockNonce> _ </blockNonce>
70+
<ommerBlockHeaders> _ </ommerBlockHeaders>
71+
</block>
72+
</evm>
73+
74+
<network>
75+
<chainID> _ </chainID>
76+
77+
<activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
78+
79+
<accounts>
80+
<account>
81+
<acctID> ACCT_ID </acctID>
82+
<balance> _ </balance>
83+
<code> #parseByteStack($Foo::RUNTIME) </code>
84+
<storage> _ </storage>
85+
<origStorage> _ </origStorage>
86+
<nonce> _ </nonce>
87+
</account>
88+
</accounts>
89+
90+
<txOrder> _ </txOrder>
91+
<txPending> _ </txPending>
92+
<messages> _ </messages>
93+
</network>
94+
</ethereum>
95+
</kevm>
96+
97+
requires 0 <=Int ACCT_ID andBool ACCT_ID <Int (2 ^Int 160)
98+
andBool 0 <=Int CALLER_ID andBool CALLER_ID <Int (2 ^Int 160)
99+
andBool 0 <=Int ORIGIN_ID andBool ORIGIN_ID <Int (2 ^Int 160)
100+
andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
101+
andBool 0 <=Int IN_ADDR andBool IN_ADDR <Int (2 ^Int 160)
102+
andBool 0 <=Int IN_U16 andBool IN_U16 <Int (2 ^Int 16)
103+
andBool IN_ADDR ==Int OUT_ADDR
104+
andBool IN_U16 ==Int OUT_U16
105+
106+
endmodule
107+

0 commit comments

Comments
 (0)