ethereum: Add property tests and instructions for running them with K…

…EVM (#2956) * ethereum: Add Foundry tests written by RV * ethereum: Add scripts and instructions to run proofs using KEVM * ethereum: Fix typo on testSetup_after_setup_revert_KEVM * ethereum: Edit Makefile to skip KEVM tests when running forge test * ethereum: Fix commented-out lines in Foundry tests * ethereum: Refactor GovernanceStructs invalid-size tests * ethereum: Replace assume with bound in Foundry tests Co-authored-by: Jeff Schroeder <jeffschroeder@computer.org> * ethereum: Apply review suggestions to run-kevm script Co-authored-by: Jeff Schroeder <jeffschroeder@computer.org> * ethereum: explicit cast to uint8 for some vars The bound() calls need to be explicitly cast to uint8 from the uint256 that forge-std's bound() returns. * ethereum: updating some of the RV tests The definitions don't compile with newer forge/solc. * ethereum: Add assumption to test that guardian count > 0 Prevents an arithmetic over/underflow error in testCannotVerifySignaturesWithOutOfBoundsSignature, in the expression bound(outOfBoundsGuardian, 0, params.guardianCount - 1) --------- Co-authored-by: Lucas MT <lucas.tabajara@runtimeverification.com> Co-authored-by: Jeff Schroeder <jeffschroeder@computer.org>
wormhole-foundation · Sep 6, 2023 · 406a43d · 406a43d
1 parent 5457e7f
commit 406a43d
Show file tree

Hide file tree

Showing 18 changed files with 3,445 additions and 2 deletions.
diff --git a/ethereum/Makefile b/ethereum/Makefile
@@ -83,7 +83,7 @@ test-identifiers: dependencies
 
 .PHONY:
 test-forge: dependencies
- forge test
+ forge test --no-match-test .*_KEVM # ignore KEVM tests (see PROOFS.md)
 
 clean:
  rm -rf ganache.log .env node_modules build flattened build-forge ethers-contracts lib/forge-std lib/openzeppelin-contracts
diff --git a/ethereum/PROOFS.md b/ethereum/PROOFS.md
@@ -0,0 +1,49 @@
+# Instructions to Reproduce the KEVM Proofs
+
+## Dependencies
+
+First, install [Forge](https://github.com/foundry-rs/foundry/tree/master/forge) and run
+
+```
+make dependencies
+```
+
+to install the `forge-std` library in the `lib` folder.
+
+Next, [follow the instructions here](https://github.com/runtimeverification/evm-semantics/) to install KEVM (we recommend the fast installation with kup). All proofs were originally run using the KEVM version corresponding to commit [f5c1795aea0c7d6781c94f0e6d4c434ad3ad1982](https://github.com/runtimeverification/evm-semantics/commit/f5c1795aea0c7d6781c94f0e6d4c434ad3ad1982). To update the installation to a specific KEVM version, run
+
+```
+kup update kevm --version <branch name or commit hash>
+```
+
+## Reproducing the Proofs
+
+Use the following command to run the proofs using KEVM:
+
+```
+./run-kevm.sh
+```
+
+The script first builds the tests with `forge build`, then kompiles them into a KEVM specification and runs the prover.
+
+The script symbolically executes all tests added to the `tests` variable. By default, it is set to run all of the tests that have been verified using KEVM. To run a single test at a time, comment out the lines with the other tests. Tests can also be run in parallel by changing the value of the `workers` variable.
+
+The script is set to resume proofs from where they left off. This means that if a proof is interrupted halfway, running the script again will continue from that point. Similarly, if a proof has already completed, running the script again will do nothing and just report the result. To instead restart from the beginning, turn on the `reinit` option in the script. Also note that if changes are made to the Solidity code, or if you switch to a different KEVM version, you should turn on the `regen` option the next time you run the script.
+
+**Note:** When building the tests, the `run-kevm.sh` script uses the command `forge build --skip Migrator.sol` to avoid building the `Migrator` contract. The reason is that this contract contains a function named `claim`, which currently causes problems because `claim` is a reserved keyword in KEVM (none of the proofs depend on this contract, but KEVM generates definitions for all contracts built by `forge build`). Until this issue is fixed, if `forge build` has previously been run without the `--skip Migrator.sol` option, it is necessary to delete the `out/Migrator.sol` directory before running `run-kevm.sh`. Otherwise, the script will produce the following error:
+```
+[Error] Inner Parser: Parse error: unexpected end of file following token '.'.
+ Source(/path/to/wormhole/ethereum/out/kompiled/foundry.k)
+ Location(7633,23,7633,23)
+ 7633 | rule ( Migrator . claim ( V0__amount : uint256 ) => #abiCallData (
+"claim" , #uint256 ( V0__amount ) , .TypedArgs ) )
+ . ^
+[Error] Inner Parser: Parse error: unexpected token 'uint256' following token
+':'.
+ Source(/path/to/wormhole/ethereum/out/kompiled/foundry.k)
+ Location(7633,45,7633,52)
+ 7633 | rule ( Migrator . claim ( V0__amount : uint256 ) => #abiCallData (
+"claim" , #uint256 ( V0__amount ) , .TypedArgs ) )
+ . ^~~~~~~
+[Error] Compiler: Had 2 parsing errors.
+```
diff --git a/ethereum/forge-test/Getters.t.sol b/ethereum/forge-test/Getters.t.sol
@@ -0,0 +1,220 @@
+// test/Messages.sol
+// SPDX-License-Identifier: Apache 2
+
+pragma solidity ^0.8.0;
+
+import "../contracts/Messages.sol";
+import "../contracts/Getters.sol";
+import "../contracts/Structs.sol";
+import "forge-test/rv-helpers/TestUtils.sol";
+
+contract TestGetters is TestUtils {
+ Getters getters;
+
+ function setUp() public {
+ getters = new Getters();
+ }
+
+ function testGetGuardianSetIndex(uint32 index, bytes32 storageSlot)
+ public
+ unchangedStorage(address(getters), storageSlot)
+ {
+ vm.assume(storageSlot != GUARDIANSETINDEX_STORAGE_INDEX);
+
+ bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000);
+ bytes32 updatedStorage = storeWithMask(address(getters), GUARDIANSETINDEX_STORAGE_INDEX, bytes32(uint256(index)), mask);
+
+ assertEq(index, getters.getCurrentGuardianSetIndex());
+ assertEq(updatedStorage, vm.load(address(getters), GUARDIANSETINDEX_STORAGE_INDEX));
+ }
+
+ function testGetGuardianSetIndex_KEVM(uint32 index, bytes32 storageSlot)
+ public
+ symbolic(address(getters))
+ {
+ testGetGuardianSetIndex(index, storageSlot);
+ }
+
+ function testGetExpireGuardianSet(uint32 timestamp, uint32 index, bytes32 storageSlot)
+ public
+ unchangedStorage(address(getters), storageSlot)
+ {
+ bytes32 storageLocation = hashedLocationOffset(index,GUARDIANSETS_STORAGE_INDEX,1);
+ vm.assume(storageSlot != storageLocation);
+
+ bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000);
+ bytes32 updatedStorage = storeWithMask(address(getters), storageLocation, bytes32(uint256(timestamp)), mask);
+
+ uint32 expirationTime = getters.getGuardianSet(index).expirationTime;
+
+ assertEq(expirationTime, timestamp);
+ assertEq(updatedStorage, vm.load(address(getters), storageLocation));
+ }
+
+ function testGetExpireGuardianSet_KEVM(uint32 timestamp, uint32 index, bytes32 storageSlot)
+ public
+ symbolic(address(getters))
+ {
+ testGetExpireGuardianSet(timestamp, index, storageSlot);
+ }
+
+ function testGetMessageFee(uint256 newFee, bytes32 storageSlot)
+ public
+ unchangedStorage(address(getters), storageSlot)
+ {
+ vm.assume(storageSlot != MESSAGEFEE_STORAGE_INDEX);
+
+ vm.store(address(getters), MESSAGEFEE_STORAGE_INDEX, bytes32(newFee));
+
+ assertEq(newFee, getters.messageFee());
+ assertEq(bytes32(newFee), vm.load(address(getters), MESSAGEFEE_STORAGE_INDEX));
+ }
+
+ function testGetMessageFee_KEVM(uint256 newFee, bytes32 storageSlot)
+ public
+ symbolic(address(getters))
+ {
+ testGetMessageFee(newFee, storageSlot);
+ }
+
+ function testGetGovernanceContract(bytes32 newGovernanceContract, bytes32 storageSlot)
+ public
+ unchangedStorage(address(getters), storageSlot)
+ {
+ vm.assume(storageSlot != GOVERNANCECONTRACT_STORAGE_INDEX);
+
+ vm.store(address(getters), GOVERNANCECONTRACT_STORAGE_INDEX, newGovernanceContract);
+
+ assertEq(newGovernanceContract, getters.governanceContract());
+ assertEq(newGovernanceContract, vm.load(address(getters), GOVERNANCECONTRACT_STORAGE_INDEX));
+ }
+
+ function testGetGovernanceContract_KEVM(bytes32 newGovernanceContract, bytes32 storageSlot)
+ public
+ symbolic(address(getters))
+ {
+ testGetGovernanceContract(newGovernanceContract, storageSlot);
+ }
+
+ function testIsInitialized(address newImplementation, uint8 initialized, bytes32 storageSlot)
+ public
+ unchangedStorage(address(getters), storageSlot)
+ {
+ bytes32 storageLocation = hashedLocation(newImplementation, INITIALIZEDIMPLEMENTATIONS_STORAGE_INDEX); 
+ vm.assume(storageSlot != storageLocation);
+
+ bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00);
+ bytes32 updatedStorage = storeWithMask(address(getters), storageLocation, bytes32(uint256(initialized)), mask);
+
+ assertEq(getters.isInitialized(newImplementation), initialized != 0);
+ assertEq(updatedStorage, vm.load(address(getters), storageLocation));
+ }
+
+ function testIsInitialized_KEVM(address newImplementation, uint8 initialized, bytes32 storageSlot)
+ public
+ symbolic(address(getters))
+ {
+ testIsInitialized(newImplementation, initialized, storageSlot);
+ }
+
+ function testGetGovernanceActionConsumed(bytes32 hash, uint8 initialized, bytes32 storageSlot)
+ public
+ unchangedStorage(address(getters), storageSlot)
+ {
+ bytes32 storageLocation = hashedLocation(hash, CONSUMEDGOVACTIONS_STORAGE_INDEX);
+ vm.assume(storageSlot != storageLocation);
+
+ bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00);
+ bytes32 updatedStorage = storeWithMask(address(getters), storageLocation, bytes32(uint256(initialized)), mask);
+
+ assertEq(getters.governanceActionIsConsumed(hash), initialized != 0);
+ assertEq(updatedStorage, vm.load(address(getters), storageLocation));
+ }
+
+ function testGetGovernanceActionConsumed_KEVM(bytes32 hash, uint8 initialized, bytes32 storageSlot)
+ public
+ symbolic(address(getters))
+ {
+ testGetGovernanceActionConsumed(hash, initialized, storageSlot);
+ }
+
+ function testChainId(uint16 newChainId, bytes32 storageSlot)
+ public
+ unchangedStorage(address(getters), storageSlot)
+ {
+ vm.assume(storageSlot != CHAINID_STORAGE_INDEX);
+
+ bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000);
+ bytes32 updatedStorage = storeWithMask(address(getters), CHAINID_STORAGE_INDEX, bytes32(uint256(newChainId)), mask);
+
+ assertEq(getters.chainId(), newChainId);
+ assertEq(updatedStorage, vm.load(address(getters), CHAINID_STORAGE_INDEX));
+ }
+
+ function testChainId_KEVM(uint16 newChainId, bytes32 storageSlot)
+ public
+ symbolic(address(getters))
+ {
+ testChainId(newChainId, storageSlot);
+ }
+
+ function testGovernanceChainId(uint16 newChainId, bytes32 storageSlot)
+ public
+ unchangedStorage(address(getters), storageSlot)
+ {
+ vm.assume(storageSlot != CHAINID_STORAGE_INDEX);
+
+ bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000ffff);
+ bytes32 updatedStorage = storeWithMask(address(getters), CHAINID_STORAGE_INDEX, bytes32(uint256(newChainId)) << 16, mask);
+
+ assertEq(getters.governanceChainId(), newChainId);
+ assertEq(updatedStorage, vm.load(address(getters), CHAINID_STORAGE_INDEX));
+ }
+
+ function testGovernanceChainId_KEVM(uint16 newChainId, bytes32 storageSlot)
+ public
+ symbolic(address(getters))
+ {
+ testGovernanceChainId(newChainId, storageSlot);
+ }
+
+ function testNextSequence(address emitter, uint64 sequence, bytes32 storageSlot)
+ public
+ unchangedStorage(address(getters), storageSlot)
+ {
+ bytes32 storageLocation = hashedLocation(emitter, SEQUENCES_STORAGE_INDEX); 
+ vm.assume(storageSlot != storageLocation);
+
+ bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000);
+ bytes32 updatedStorage = storeWithMask(address(getters), storageLocation, bytes32(uint256(sequence)), mask);
+
+ assertEq(getters.nextSequence(emitter), sequence);
+ assertEq(updatedStorage, vm.load(address(getters), storageLocation));
+ }
+
+ function testNextSequence_KEVM(address emitter, uint64 sequence, bytes32 storageSlot)
+ public
+ symbolic(address(getters))
+ {
+ testNextSequence(emitter, sequence, storageSlot);
+ }
+
+ function testEvmChainId(uint256 newEvmChainId, bytes32 storageSlot)
+ public
+ unchangedStorage(address(getters), storageSlot)
+ {
+ vm.assume(storageSlot != EVMCHAINID_STORAGE_INDEX);
+
+ vm.store(address(getters), EVMCHAINID_STORAGE_INDEX, bytes32(newEvmChainId));
+
+ assertEq(getters.evmChainId(), newEvmChainId);
+ assertEq(bytes32(newEvmChainId), vm.load(address(getters), EVMCHAINID_STORAGE_INDEX));
+ }
+
+ function testEvmChainId_KEVM(uint256 newEvmChainId, bytes32 storageSlot)
+ public
+ symbolic(address(getters))
+ {
+ testEvmChainId(newEvmChainId, storageSlot);
+ }
+}