Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Enable more passing proofs with RPC prover #2479

Closed
wants to merge 4 commits into from
Closed

Enable more passing proofs with RPC prover #2479

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
129c0c9
tests/specs/examples/sum-to-n-spec.k, tests/failing: changes for pass…
ehildenb Jun 11, 2024
23e905a
tests/specs/functional/merkle-spec: use appropriate klabel to avoid t…
ehildenb Jun 11, 2024
8b79ee1
evm-semantics/serialization, tests/storageRoot-spec, tests/failing: f…
ehildenb Jun 11, 2024
24b2589
tests/failing-symbolic: move storageRoot spec over to booster
ehildenb Jun 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -648,7 +648,7 @@ Tree Root Helper Functions

rule #intMap2StorageMapAux( SMAP, _, .List ) => SMAP
rule #intMap2StorageMapAux( SMAP, IMAP, ListItem(K) REST )
=> #intMap2StorageMapAux( #wordBytes(K) |-> #rlpEncodeInt({IMAP[K]}:>Int) SMAP, IMAP, REST )
=> #intMap2StorageMapAux( #wordBytes(K) |-> Bytes2String(#rlpEncodeInt({IMAP[K]}:>Int)) SMAP, IMAP, REST )
requires {IMAP[K]}:>Int =/=Int 0

rule #intMap2StorageMapAux( SMAP, IMAP, ListItem(K) REST )
Expand Down
1 change: 1 addition & 0 deletions tests/failing-symbolic.haskell
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ tests/specs/examples/erc20-spec.md
tests/specs/examples/erc721-spec.md
tests/specs/examples/solidity-code-spec.md
tests/specs/examples/storage-spec.md
tests/specs/examples/sum-to-n-spec.k
tests/specs/functional/evm-int-simplifications-spec.k
tests/specs/functional/infinite-gas-spec.k
tests/specs/functional/int-simplifications-spec.k
Expand Down
3 changes: 0 additions & 3 deletions tests/failing-symbolic.haskell-booster
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
tests/specs/examples/erc721-spec.md
tests/specs/examples/sum-to-n-foundry-spec.k
tests/specs/examples/sum-to-n-spec.k
tests/specs/functional/merkle-spec.k
tests/specs/functional/storageRoot-spec.k
tests/specs/mcd/vat-fold-pass-rough-spec.k
tests/specs/mcd/vat-fork-diff-pass-rough-spec.k
tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k
8 changes: 6 additions & 2 deletions tests/specs/examples/sum-to-n-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,8 @@ endmodule
module SUM-TO-N-SPEC
imports VERIFICATION

claim <k> #execute ... </k>
claim [main]:
<k> #execute => #halt ... </k>
<mode> NORMAL </mode>
<schedule> ISTANBUL </schedule>
<useGas> true </useGas>
Expand All @@ -49,8 +50,10 @@ module SUM-TO-N-SPEC
andBool N <=Int 340282366920938463463374607431768211455
andBool #sizeWordStack(WS) <Int 1021
andBool G >=Int 52 *Int N +Int 27
[depends(loop)]

claim <k> #execute ... </k>
claim [loop]:
<k> #execute => #halt ... </k>
<mode> NORMAL </mode>
<schedule> ISTANBUL </schedule>
<useGas> true </useGas>
Expand All @@ -69,5 +72,6 @@ module SUM-TO-N-SPEC
andBool S +Int I *Int (I +Int 1) /Int 2 <Int pow256
andBool #sizeWordStack(WS) <Int 1021
andBool G >=Int 52 *Int I +Int 21
[circularity]

endmodule
64 changes: 32 additions & 32 deletions tests/specs/functional/merkle-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@ module VERIFICATION
imports EVM

syntax StepSort ::= MerkleTree | String | Int
syntax KItem ::= runMerkle ( StepSort )
| doneMerkle( StepSort )
// ------------------------------------------
rule <k> runMerkle( T ) => doneMerkle( T ) ... </k>
syntax KItem ::= runLemma ( StepSort ) [symbol(runLemma)]
| doneLemma( StepSort )
// -----------------------------------------
rule <k> runLemma( T ) => doneLemma( T ) ... </k>

syntax MerkleTree ::= "#initTree" [macro]
// -----------------------------------------
Expand All @@ -25,61 +25,61 @@ module MERKLE-SPEC
////////////////////
// Symbolic Tests //
////////////////////
claim <k> runMerkle ( MerkleUpdate( .MerkleTree, .Bytes, V ) )
=> doneMerkle( MerkleLeaf( .Bytes, V ) ) </k>
claim <k> runLemma ( MerkleUpdate( .MerkleTree, .Bytes, V ) )
=> doneLemma( MerkleLeaf( .Bytes, V ) ) ... </k>
requires V =/=String ""

// Update on MerkleLeaf
claim <k> runMerkle ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x0607"), _ ), #parseByteStack("0x0607"), V ) )
=> doneMerkle( MerkleLeaf ( #parseByteStack("0x0607"), V ) ) </k>
claim <k> runLemma ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x0607"), _ ), #parseByteStack("0x0607"), V ) )
=> doneLemma( MerkleLeaf ( #parseByteStack("0x0607"), V ) ) ... </k>
requires V =/=String ""

claim <k> runMerkle ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x0607"), _ ), #parseByteStack("0x0608"), V ) )
=> doneMerkle( MerkleExtension( #parseByteStack("0x06"), ?_ ) ) </k>
claim <k> runLemma ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x0607"), _ ), #parseByteStack("0x0608"), V ) )
=> doneLemma( MerkleExtension( #parseByteStack("0x06"), ?_ ) ) ... </k>
requires V =/=String ""

claim <k> runMerkle ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x05"), _ ), #parseByteStack("0x06"), V ) )
=> doneMerkle( MerkleBranch( ?_, ?_ ) ) </k>
claim <k> runLemma ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x05"), _ ), #parseByteStack("0x06"), V ) )
=> doneLemma( MerkleBranch( ?_, ?_ ) ) ... </k>
requires V =/=String ""

// Update on MerkleExtension
claim <k> runMerkle ( MerkleUpdate( MerkleExtension( #parseByteStack("0x06"), .MerkleTree ), #parseByteStack("0x06"), V ) )
=> doneMerkle( MerkleExtension( #parseByteStack("0x06"), MerkleLeaf( .Bytes, V ) ) ) </k>
claim <k> runLemma ( MerkleUpdate( MerkleExtension( #parseByteStack("0x06"), .MerkleTree ), #parseByteStack("0x06"), V ) )
=> doneLemma( MerkleExtension( #parseByteStack("0x06"), MerkleLeaf( .Bytes, V ) ) ) ... </k>
requires V =/=String ""

claim <k> runMerkle ( MerkleUpdate( MerkleExtension( #parseByteStack("0x07"), _ ), #parseByteStack("0x06"), V ) )
=> doneMerkle( MerkleBranch( ?_, ?_ ) ) </k>
claim <k> runLemma ( MerkleUpdate( MerkleExtension( #parseByteStack("0x07"), _ ), #parseByteStack("0x06"), V ) )
=> doneLemma( MerkleBranch( ?_, ?_ ) ) ... </k>
requires V =/=String ""

claim <k> runMerkle ( MerkleUpdate( MerkleExtension( #parseByteStack("0x0708"), _ ), #parseByteStack("0x0709"), V ) )
=> doneMerkle( MerkleExtension( #parseByteStack("0x07"), MerkleBranch( ?_, ?_ ) ) ) </k>
claim <k> runLemma ( MerkleUpdate( MerkleExtension( #parseByteStack("0x0708"), _ ), #parseByteStack("0x0709"), V ) )
=> doneLemma( MerkleExtension( #parseByteStack("0x07"), MerkleBranch( ?_, ?_ ) ) ) ... </k>
requires V =/=String ""

// Update on MerkleBranch
claim <k> runMerkle ( MerkleUpdate( MerkleBranch( M, _ ), .Bytes, V ) )
=> doneMerkle( MerkleBranch( M, V ) ) </k>
claim <k> runLemma ( MerkleUpdate( MerkleBranch( M, _ ), .Bytes, V ) )
=> doneLemma( MerkleBranch( M, V ) ) ... </k>
requires V =/=String ""

claim <k> runMerkle ( #merkleExtensionBuilder ( #parseByteStack("0e") , #parseByteStack("") , "verb" , #parseByteStack("0f0e") , "coin" ) )
=> doneMerkle ( MerkleExtension ( #parseByteStack("0e") , MerkleBranch ( 15 |-> MerkleLeaf ( #parseByteStack("0e") , "coin" ) , "verb" ) ) ) </k>
claim <k> runLemma ( #merkleExtensionBuilder ( #parseByteStack("0e") , #parseByteStack("") , "verb" , #parseByteStack("0f0e") , "coin" ) )
=> doneLemma ( MerkleExtension ( #parseByteStack("0e") , MerkleBranch ( 15 |-> MerkleLeaf ( #parseByteStack("0e") , "coin" ) , "verb" ) ) ) ... </k>

////////////////////////
// MerkleDelete Tests //
////////////////////////

claim <k> runMerkle ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( #initTree, "de", "" ) ) ) )
=> doneMerkle( "4ba393b447e1c78b2f647e10ae687de132f01f49d67e396bcdea4da2de05370f" ) </k>
claim <k> runLemma ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( #initTree, "de", "" ) ) ) )
=> doneLemma( "4ba393b447e1c78b2f647e10ae687de132f01f49d67e396bcdea4da2de05370f" ) ... </k>

claim <k> runMerkle ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( #initTree, "becfe", "" ) ) ) )
=> doneMerkle( "4ba393b447e1c78b2f647e10ae687de132f01f49d67e396bcdea4da2de05370f" ) </k>
claim <k> runLemma ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( #initTree, "becfe", "" ) ) ) )
=> doneLemma( "4ba393b447e1c78b2f647e10ae687de132f01f49d67e396bcdea4da2de05370f" ) ... </k>

claim <k> runMerkle ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( #initTree, "def", "" ) ) ) )
=> doneMerkle( "4ba393b447e1c78b2f647e10ae687de132f01f49d67e396bcdea4da2de05370f" ) </k>
claim <k> runLemma ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( #initTree, "def", "" ) ) ) )
=> doneLemma( "4ba393b447e1c78b2f647e10ae687de132f01f49d67e396bcdea4da2de05370f" ) ... </k>

claim <k> runMerkle ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( #initTree, "defe", "" ) ) ) )
=> doneMerkle( "4ba393b447e1c78b2f647e10ae687de132f01f49d67e396bcdea4da2de05370f" ) </k>
claim <k> runLemma ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( #initTree, "defe", "" ) ) ) )
=> doneLemma( "4ba393b447e1c78b2f647e10ae687de132f01f49d67e396bcdea4da2de05370f" ) ... </k>

claim <k> runMerkle ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( MerkleUpdate( #initTree, "defe", "" ), "becfe", "" ) ) ) )
=> doneMerkle( "4ba393b447e1c78b2f647e10ae687de132f01f49d67e396bcdea4da2de05370f" ) </k>
claim <k> runLemma ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( MerkleUpdate( #initTree, "defe", "" ), "becfe", "" ) ) ) )
=> doneLemma( "4ba393b447e1c78b2f647e10ae687de132f01f49d67e396bcdea4da2de05370f" ) ... </k>

endmodule
28 changes: 18 additions & 10 deletions tests/specs/functional/storageRoot-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,32 +9,37 @@ module VERIFICATION
// -------------------------------------------------------
rule <k> runLemma(S) => doneLemma(S) ... </k>

syntax Step ::= String | MerkleTree
// -----------------------------------
syntax Step ::= String | MerkleTree | Bytes
// -------------------------------------------

endmodule

module STORAGEROOT-SPEC
imports VERIFICATION

claim <k> runLemma ( #storageRoot( .Map ) ) => doneLemma ( .MerkleTree ) </k>
claim [merkle.1]:
<k> runLemma ( #storageRoot( .Map ) ) => doneLemma ( .MerkleTree ) </k>

claim <k> runLemma ( #rlpEncodeString ( "" ) ) => doneLemma ( "\x80" ) </k>
claim [merkle.2]:
<k> runLemma ( #rlpEncodeString ( "" ) ) => doneLemma ( b"\x80" ) </k>

claim <k> runLemma ( #rlpEncodeString ( "\x82\x04\xd2" ) ) => doneLemma ( "\x83\x82\x04\xd2" ) </k>
claim [merkle.3]:
<k> runLemma ( #rlpEncodeString ( "\x82\x04\xd2" ) ) => doneLemma ( b"\x83\x82\x04\xd2" ) </k>

// uint pos0;
//
// pos0 = 1234;
claim <k> runLemma ( Keccak256( #rlpEncodeMerkleTree( #storageRoot( #hashedLocation( "Solidity", 0, .IntList ) |-> 1234 ) ) ) )
claim [merkle.4]:
<k> runLemma ( Keccak256( #rlpEncodeMerkleTree( #storageRoot( #hashedLocation( "Solidity", 0, .IntList ) |-> 1234 ) ) ) )
=> doneLemma ( "6ff6cfba457bc662332201b53a8bda503e307197962f2c51e5e2dcc3809e19be" )
</k>

// mapping (uint => uint) pos0;
//
// pos0[0] = 100;
// pos0[1] = 200;
claim <k> runLemma ( Keccak256( #rlpEncodeMerkleTree( #storageRoot( #hashedLocation( "Solidity", 0, 0 ) |-> 100 #hashedLocation( "Solidity", 0, 1 ) |-> 200 ) ) ) )
claim [merkle.5]:
<k> runLemma ( Keccak256( #rlpEncodeMerkleTree( #storageRoot( #hashedLocation( "Solidity", 0, 0 ) |-> 100 #hashedLocation( "Solidity", 0, 1 ) |-> 200 ) ) ) )
=> doneLemma ( "27093708a19995cf73ddd4b27049a7e33fb49e242bde6c1bffbb6596b67b8b3e" )
</k>

Expand All @@ -44,7 +49,8 @@ module STORAGEROOT-SPEC
// pos0 = 600;
// pos1[0] = 200;
// pos1[5] = 24;
claim <k> runLemma ( Keccak256( #rlpEncodeMerkleTree( #storageRoot( #hashedLocation( "Solidity", 0, .IntList ) |-> 600 #hashedLocation( "Solidity", 1, 0 ) |-> 200 #hashedLocation( "Solidity", 1, 5 ) |-> 24 ) ) ) )
claim [merkle.6]:
<k> runLemma ( Keccak256( #rlpEncodeMerkleTree( #storageRoot( #hashedLocation( "Solidity", 0, .IntList ) |-> 600 #hashedLocation( "Solidity", 1, 0 ) |-> 200 #hashedLocation( "Solidity", 1, 5 ) |-> 24 ) ) ) )
=> doneLemma ( "7df5d7b198240b49434b4e1dbff02fcb0649dd91650ae0fae191b2881cbb009e" )
</k>

Expand All @@ -55,7 +61,8 @@ module STORAGEROOT-SPEC
// pos0[1] = 456;
// pos1[6] = 56;
// pos1[9] = 333;
claim <k> runLemma ( Keccak256( #rlpEncodeMerkleTree( #storageRoot( #hashedLocation( "Solidity", 0, 0 ) |-> 123 #hashedLocation( "Solidity", 0, 1 ) |-> 456 #hashedLocation( "Solidity", 1, 6 ) |-> 56 #hashedLocation( "Solidity", 1, 9 ) |-> 333 ) ) ) )
claim [merkle.7]:
<k> runLemma ( Keccak256( #rlpEncodeMerkleTree( #storageRoot( #hashedLocation( "Solidity", 0, 0 ) |-> 123 #hashedLocation( "Solidity", 0, 1 ) |-> 456 #hashedLocation( "Solidity", 1, 6 ) |-> 56 #hashedLocation( "Solidity", 1, 9 ) |-> 333 ) ) ) )
=> doneLemma ( "e3d130ca69a8d33ad2058d86ba26ec414f6e5639930041d6a266ee88b25ea835" )
</k>

Expand All @@ -70,7 +77,8 @@ module STORAGEROOT-SPEC
// pos2 = 100;
// pos3[0][0] = 42;
// pos3[2][1] = 2019;
claim <k> runLemma ( Keccak256( #rlpEncodeMerkleTree( #storageRoot( #hashedLocation( "Solidity", 0, .IntList ) |-> 1234 #hashedLocation( "Solidity", 1, 0 ) |-> 0 #hashedLocation( "Solidity", 1, 1 ) |-> 1 #hashedLocation( "Solidity", 2, .IntList ) |-> 100 #hashedLocation( "Solidity", 3, 0 0 ) |-> 42 #hashedLocation( "Solidity", 3, 2 1 ) |-> 2019 ) ) ) )
claim [merkle.8]:
<k> runLemma ( Keccak256( #rlpEncodeMerkleTree( #storageRoot( #hashedLocation( "Solidity", 0, .IntList ) |-> 1234 #hashedLocation( "Solidity", 1, 0 ) |-> 0 #hashedLocation( "Solidity", 1, 1 ) |-> 1 #hashedLocation( "Solidity", 2, .IntList ) |-> 100 #hashedLocation( "Solidity", 3, 0 0 ) |-> 42 #hashedLocation( "Solidity", 3, 2 1 ) |-> 2019 ) ) ) )
=> doneLemma ( "1a40e309e184fb6483112c37def9ed52e5ee36aa4b570a234a962b3a8f186610" )
</k>
endmodule
Loading