From 406a43d03ee2347b6ae4e3b57962e09138ee276a Mon Sep 17 00:00:00 2001 From: lucasmt <36549752+lucasmt@users.noreply.github.com> Date: Wed, 6 Sep 2023 10:24:00 -0500 Subject: [PATCH] ethereum: Add property tests and instructions for running them with KEVM (#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 * ethereum: Apply review suggestions to run-kevm script Co-authored-by: Jeff Schroeder * 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 Co-authored-by: Jeff Schroeder --- ethereum/Makefile | 2 +- ethereum/PROOFS.md | 49 + ethereum/forge-test/Getters.t.sol | 220 +++ ethereum/forge-test/Governance.t.sol | 1238 +++++++++++++++++ ethereum/forge-test/GovernanceStructs.t.sol | 440 ++++++ ethereum/forge-test/Implementation.t.sol | 155 +++ ethereum/forge-test/MessagesRV.t.sol | 214 +++ ethereum/forge-test/Setters.t.sol | 268 ++++ ethereum/forge-test/Setup.t.sol | 116 ++ ethereum/forge-test/Shutdown.t.sol | 86 ++ ethereum/forge-test/TokenImplementation.t.sol | 2 +- .../forge-test/rv-helpers/IMyWormhole.sol | 11 + ethereum/forge-test/rv-helpers/KEVMCheats.sol | 38 + .../rv-helpers/MyImplementation.sol | 21 + ethereum/forge-test/rv-helpers/MySetters.sol | 47 + ethereum/forge-test/rv-helpers/TestUtils.sol | 187 +++ ethereum/run-kevm.sh | 113 ++ ethereum/wormhole-lemmas.k | 240 ++++ 18 files changed, 3445 insertions(+), 2 deletions(-) create mode 100644 ethereum/PROOFS.md create mode 100644 ethereum/forge-test/Getters.t.sol create mode 100644 ethereum/forge-test/Governance.t.sol create mode 100644 ethereum/forge-test/GovernanceStructs.t.sol create mode 100644 ethereum/forge-test/Implementation.t.sol create mode 100644 ethereum/forge-test/MessagesRV.t.sol create mode 100644 ethereum/forge-test/Setters.t.sol create mode 100644 ethereum/forge-test/Setup.t.sol create mode 100644 ethereum/forge-test/Shutdown.t.sol create mode 100644 ethereum/forge-test/rv-helpers/IMyWormhole.sol create mode 100644 ethereum/forge-test/rv-helpers/KEVMCheats.sol create mode 100644 ethereum/forge-test/rv-helpers/MyImplementation.sol create mode 100644 ethereum/forge-test/rv-helpers/MySetters.sol create mode 100644 ethereum/forge-test/rv-helpers/TestUtils.sol create mode 100755 ethereum/run-kevm.sh create mode 100644 ethereum/wormhole-lemmas.k diff --git a/ethereum/Makefile b/ethereum/Makefile index a1502645e4..daa67bb1c1 100644 --- 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 new file mode 100644 index 0000000000..b72242ff5d --- /dev/null +++ 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 +``` + +## 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. +``` \ No newline at end of file diff --git a/ethereum/forge-test/Getters.t.sol b/ethereum/forge-test/Getters.t.sol new file mode 100644 index 0000000000..368150ec4e --- /dev/null +++ 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); + } +} diff --git a/ethereum/forge-test/Governance.t.sol b/ethereum/forge-test/Governance.t.sol new file mode 100644 index 0000000000..3615524a50 --- /dev/null +++ b/ethereum/forge-test/Governance.t.sol @@ -0,0 +1,1238 @@ +// test/Messages.sol +// SPDX-License-Identifier: Apache 2 + +pragma solidity ^0.8.0; + +import "../contracts/Implementation.sol"; +import "../contracts/Setup.sol"; +import "../contracts/Wormhole.sol"; +import "forge-std/Test.sol"; +import "forge-test/rv-helpers/TestUtils.sol"; +import "forge-test/rv-helpers/MyImplementation.sol"; +import "forge-test/rv-helpers/IMyWormhole.sol"; + +contract TestGovernance is TestUtils { + + uint16 constant CHAINID = 2; + uint256 constant EVMCHAINID = 1; + bytes32 constant MODULE = 0x00000000000000000000000000000000000000000000000000000000436f7265; + bytes32 constant governanceContract = 0x0000000000000000000000000000000000000000000000000000000000000004; + + bytes32 constant CHAINID_SLOT = bytes32(uint256(0)); + bytes32 constant GUARDIANSETS_SLOT = bytes32(uint256(2)); + bytes32 constant GUARDIANSETINDEX_SLOT = bytes32(uint256(3)); + bytes32 constant IMPLEMENTATION_SLOT = 0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc; + bytes32 constant CONSUMED_ACTIONS_SLOT = bytes32(uint256(5)); + bytes32 constant INIT_IMPLEMENTATION_SLOT = bytes32(uint256(6)); + bytes32 constant MESSAGEFEE_SLOT = bytes32(uint256(7)); + bytes32 constant EVMCHAINID_SLOT = bytes32(uint256(8)); + + Wormhole proxy; + Implementation impl; + Setup setup; + Setup proxiedSetup; + IMyWormhole proxied; + + uint256 constant testGuardian = 93941733246223705020089879371323733820373732307041878556247502674739205313440; + + event ContractUpgraded(address indexed oldContract, address indexed newContract); + + function setUp() public { + // Deploy setup + setup = new Setup(); + // Deploy implementation contract + impl = new Implementation(); + // Deploy proxy + proxy = new Wormhole(address(setup), bytes("")); + + address[] memory keys = new address[](1); + keys[0] = 0xbeFA429d57cD18b7F8A4d91A2da9AB4AF05d0FBe; // vm.addr(testGuardian) + + //proxied setup + proxiedSetup = Setup(address(proxy)); + + vm.chainId(1); + proxiedSetup.setup({ + implementation: address(impl), + initialGuardians: keys, + chainId: CHAINID, + governanceChainId: 1, + governanceContract: governanceContract, + evmChainId: EVMCHAINID + }); + + proxied = IMyWormhole(address(proxy)); + } + + function testSubmitContractUpgrade( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + MyImplementation newImpl = new MyImplementation(EVMCHAINID, CHAINID); + + vm.assume(storageSlot != IMPLEMENTATION_SLOT); + vm.assume(storageSlot != hashedLocation(address(newImpl), INIT_IMPLEMENTATION_SLOT)); + + bytes memory payload = payloadSubmitContract(MODULE, CHAINID, address(newImpl)); + (bytes memory _vm, bytes32 hash) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + proxied.submitContractUpgrade(_vm); + + assertEq(address(newImpl), address(proxied.getImplementation())); + assertEq(true, proxied.isInitialized(address(newImpl))); + assertEq(true, proxied.governanceActionIsConsumed(hash)); + } + + function testSubmitContractUpgrade_Emit( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + MyImplementation newImpl = new MyImplementation(EVMCHAINID, CHAINID); + + vm.assume(storageSlot != IMPLEMENTATION_SLOT); + vm.assume(storageSlot != hashedLocation(address(newImpl), INIT_IMPLEMENTATION_SLOT)); + + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitContract(MODULE, CHAINID, address(newImpl)); + (bytes memory _vm, bytes32 hash) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + vm.expectEmit(true,true,true,true); + emit ContractUpgraded(address(impl), address(newImpl)); + + proxied.submitContractUpgrade(_vm); + } + + function testInitialize_after_upgrade_revert(bytes32 storageSlot, address alice) + public + unchangedStorage(address(proxied), storageSlot) + { + Implementation newImpl = new Implementation(); + + vm.assume(storageSlot != IMPLEMENTATION_SLOT); + vm.assume(storageSlot != hashedLocation(address(newImpl), INIT_IMPLEMENTATION_SLOT)); + + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitContract(MODULE, 2, address(newImpl)); + (bytes memory _vm, bytes32 hash) = validVm(0, 0, 0, 1, governanceContract, 0, 0, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + proxied.submitContractUpgrade(_vm); + + vm.prank(alice); + vm.expectRevert("already initialized"); + proxied.initialize(); + } + + function testSubmitContractUpgrade_Revert_InvalidFork( + bytes32 storageSlot, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(evmChainId != EVMCHAINID); + vm.chainId(evmChainId); + + MyImplementation newImpl = new MyImplementation(evmChainId, CHAINID); + bytes memory payload = payloadSubmitContract(MODULE, CHAINID, address(newImpl)); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("invalid fork"); + proxied.submitContractUpgrade(_vm); + } + + function testSubmitContractUpgrade_Revert_InvalidModule( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + bytes32 module) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(module != MODULE); + vm.chainId(EVMCHAINID); + + MyImplementation newImpl = new MyImplementation(EVMCHAINID, CHAINID); + bytes memory payload = payloadSubmitContract(module, CHAINID, address(newImpl)); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("Invalid Module"); + proxied.submitContractUpgrade(_vm); + } + + function testSubmitContractUpgrade_Revert_InvalidChain( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(chainId != CHAINID); + vm.chainId(EVMCHAINID); + + MyImplementation newImpl = new MyImplementation(EVMCHAINID, CHAINID); + bytes memory payload = payloadSubmitContract(MODULE, chainId, address(newImpl)); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("Invalid Chain"); + proxied.submitContractUpgrade(_vm); + } + + function testSubmitContractUpgrade_Revert_InvalidGuardianSetIndex( + bytes32 storageSlot, + uint32 guardianSetIndex, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(guardianSetIndex != 0); + vm.chainId(EVMCHAINID); + + MyImplementation newImpl = new MyImplementation(EVMCHAINID, CHAINID); + bytes memory payload = payloadSubmitContract(MODULE, CHAINID, address(newImpl)); + (bytes memory _vm, ) = validVm( + guardianSetIndex, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + // Since the current version of the test uses only one guardian set, + // in practice only the 'else' branch will be taken + if (guardianSetIndex < proxied.getCurrentGuardianSetIndex()) { + vm.expectRevert("not signed by current guardian set"); + } else { + vm.expectRevert("invalid guardian set"); + } + + proxied.submitContractUpgrade(_vm); + } + + function testSubmitContractUpgrade_Revert_WrongGovernanceChain( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint16 emitterChainId, + uint64 sequence, + uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(emitterChainId != 1); + vm.chainId(EVMCHAINID); + + MyImplementation newImpl = new MyImplementation(EVMCHAINID, CHAINID); + bytes memory payload = payloadSubmitContract(MODULE, CHAINID, address(newImpl)); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, emitterChainId, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("wrong governance chain"); + proxied.submitContractUpgrade(_vm); + } + + function testSubmitContractUpgrade_Revert_WrongGovernanceContract( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + bytes32 emitterAddress, + uint64 sequence, + uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(emitterAddress != governanceContract); + vm.chainId(EVMCHAINID); + + MyImplementation newImpl = new MyImplementation(EVMCHAINID, CHAINID); + bytes memory payload = payloadSubmitContract(MODULE, CHAINID, address(newImpl)); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, emitterAddress, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("wrong governance contract"); + proxied.submitContractUpgrade(_vm); + } + + function testSubmitContractUpgrade_Revert_ReplayAttack( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.chainId(EVMCHAINID); + + MyImplementation newImpl = new MyImplementation(EVMCHAINID, CHAINID); + bytes memory payload = payloadSubmitContract(MODULE, CHAINID, address(newImpl)); + (bytes memory _vm, bytes32 hash) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + proxied.submitContractUpgrade(_vm); + + vm.expectRevert("governance action already consumed"); + proxied.submitContractUpgrade(_vm); + } + + function testSubmitSetMessageFee( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 newMessageFee) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(storageSlot != MESSAGEFEE_SLOT); + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitMessageFee(MODULE, CHAINID, newMessageFee); + (bytes memory _vm, bytes32 hash) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + proxied.submitSetMessageFee(_vm); + + assertEq(newMessageFee, proxied.messageFee()); + assertEq(true, proxied.governanceActionIsConsumed(hash)); + } + + function testSubmitSetMessageFee_Revert_InvalidModule( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + bytes32 module, + uint256 newMessageFee) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(module != MODULE); + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitMessageFee(module, CHAINID, newMessageFee); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("Invalid Module"); + proxied.submitSetMessageFee(_vm); + } + + function testSubmitSetMessageFee_Revert_InvalidChain( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId, + uint256 newMessageFee) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(chainId != CHAINID); + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitMessageFee(MODULE, chainId, newMessageFee); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("Invalid Chain"); + proxied.submitSetMessageFee(_vm); + } + + function testSubmitSetMessageFee_Revert_InvalidEvmChain( + bytes32 storageSlot, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 newMessageFee) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(evmChainId != EVMCHAINID); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitMessageFee(MODULE, CHAINID, newMessageFee); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("Invalid Chain"); + proxied.submitSetMessageFee(_vm); + } + + function testSubmitSetMessageFee_Revert_InvalidGuardianSetIndex( + bytes32 storageSlot, + uint32 guardianSetIndex, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 newMessageFee) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(guardianSetIndex != 0); + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitMessageFee(MODULE, CHAINID, newMessageFee); + (bytes memory _vm, ) = validVm( + guardianSetIndex, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + // Since the current version of the test uses only one guardian set, + // in practice only the 'else' branch will be taken + if (guardianSetIndex < proxied.getCurrentGuardianSetIndex()) { + vm.expectRevert("not signed by current guardian set"); + } else { + vm.expectRevert("invalid guardian set"); + } + + proxied.submitSetMessageFee(_vm); + } + + function testSubmitSetMessageFee_Revert_WrongGovernanceChain( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint16 emitterChainId, + uint64 sequence, + uint8 consistencyLevel, + uint256 newMessageFee) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(emitterChainId != 1); + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitMessageFee(MODULE, CHAINID, newMessageFee); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, emitterChainId, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("wrong governance chain"); + proxied.submitSetMessageFee(_vm); + } + + function testSubmitSetMessageFee_Revert_WrongGovernanceContract( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + bytes32 emitterAddress, + uint64 sequence, + uint8 consistencyLevel, + uint256 newMessageFee) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(emitterAddress != governanceContract); + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitMessageFee(MODULE, CHAINID, newMessageFee); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, emitterAddress, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("wrong governance contract"); + proxied.submitSetMessageFee(_vm); + } + + function testSubmitSetMessageFee_Revert_ReplayAttack( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 newMessageFee) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(storageSlot != MESSAGEFEE_SLOT); + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitMessageFee(MODULE, CHAINID, newMessageFee); + (bytes memory _vm, bytes32 hash) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + proxied.submitSetMessageFee(_vm); + + vm.expectRevert("governance action already consumed"); + proxied.submitSetMessageFee(_vm); + } + + //Make a similar test but with chainId = 0 + function testSubmitNewGuardianSet( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + address[] memory newGuardianSet) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(storageSlot != hashedLocationOffset(0, GUARDIANSETS_SLOT, 1)); + vm.assume(storageSlot != hashedLocationOffset(0, GUARDIANSETS_SLOT, 0)); + vm.assume(storageSlot != GUARDIANSETINDEX_SLOT); + vm.assume(0 < newGuardianSet.length); + vm.assume(newGuardianSet.length < 20); + for(uint8 i = 0; i < newGuardianSet.length; i++) + vm.assume(newGuardianSet[i] != address(0)); + + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitNewGuardianSet(MODULE, CHAINID, 1, newGuardianSet); + (bytes memory _vm, bytes32 hash) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + proxied.submitNewGuardianSet(_vm); + + assertEq(true, proxied.governanceActionIsConsumed(hash)); + assertEq(uint32(block.timestamp) + 86400, proxied.getGuardianSet(0).expirationTime); + assertEq(newGuardianSet, proxied.getGuardianSet(1).keys); + assertEq(1, proxied.getCurrentGuardianSetIndex()); + } + + function testSubmitNewGuardianSet_Revert_InvalidModule( + bytes32 storageSlot, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + bytes32 module, + uint16 chainId, + address[] memory newGuardianSet) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(module != MODULE); + vm.assume(chainId == 0 || (chainId == CHAINID && evmChainId == EVMCHAINID)); + vm.assume(newGuardianSet.length < 20); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitNewGuardianSet(module,chainId, 1, newGuardianSet); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("invalid Module"); + proxied.submitNewGuardianSet(_vm); + } + + function testSubmitNewGuardianSet_Revert_InvalidChain( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId, + address[] memory newGuardianSet) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(chainId != CHAINID && chainId != 0); + vm.assume(newGuardianSet.length < 20); + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitNewGuardianSet(MODULE, chainId, 1, newGuardianSet); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("invalid Chain"); + proxied.submitNewGuardianSet(_vm); + } + + function testSubmitNewGuardianSet_Revert_InvalidEvmChain( + bytes32 storageSlot, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + address[] memory newGuardianSet) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(evmChainId != EVMCHAINID); + vm.assume(newGuardianSet.length < 20); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitNewGuardianSet(MODULE, CHAINID, 1, newGuardianSet); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("invalid Chain"); + proxied.submitNewGuardianSet(_vm); + } + + function testSubmitNewGuardianSet_Revert_GuardianSetEmpty( + bytes32 storageSlot, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(chainId == 0 || (chainId == CHAINID && evmChainId == EVMCHAINID)); + vm.chainId(evmChainId); + + address[] memory newGuardianSet = new address[](0); // Empty guardian set + + bytes memory payload = payloadSubmitNewGuardianSet(MODULE, chainId, 1, newGuardianSet); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("new guardian set is empty"); + proxied.submitNewGuardianSet(_vm); + } + + function testSubmitNewGuardianSet_Revert_WrongIndex( + bytes32 storageSlot, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId, + uint32 newGuardianSetIndex, + address[] memory newGuardianSet) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(newGuardianSetIndex != 1); + vm.assume(chainId == 0 || (chainId == CHAINID && evmChainId == EVMCHAINID)); + vm.assume(0 < newGuardianSet.length); + vm.assume(newGuardianSet.length < 20); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitNewGuardianSet(MODULE, chainId, newGuardianSetIndex, newGuardianSet); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("index must increase in steps of 1"); + proxied.submitNewGuardianSet(_vm); + } + + function testSubmitNewGuardianSet_Revert_InvalidGuardianSetIndex( + bytes32 storageSlot, + uint32 guardianSetIndex, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId, + address[] memory newGuardianSet) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(guardianSetIndex != 0); + vm.assume(chainId == 0 || (chainId == CHAINID && evmChainId == EVMCHAINID)); + vm.assume(0 < newGuardianSet.length); + vm.assume(newGuardianSet.length < 20); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitNewGuardianSet(MODULE, chainId, 1, newGuardianSet); + (bytes memory _vm, ) = validVm( + guardianSetIndex, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + // Since the current version of the test uses only one guardian set, + // in practice only the 'else' branch will be taken + if (guardianSetIndex < proxied.getCurrentGuardianSetIndex()) { + vm.expectRevert("not signed by current guardian set"); + } else { + vm.expectRevert("invalid guardian set"); + } + + proxied.submitNewGuardianSet(_vm); + } + + function testSubmitNewGuardianSet_Revert_WrongGovernanceChain( + bytes32 storageSlot, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + uint16 emitterChainId, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId, + address[] memory newGuardianSet) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(emitterChainId != 1); + vm.assume(chainId == 0 || (chainId == CHAINID && evmChainId == EVMCHAINID)); + vm.assume(0 < newGuardianSet.length); + vm.assume(newGuardianSet.length < 20); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitNewGuardianSet(MODULE, chainId, 1, newGuardianSet); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, emitterChainId, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("wrong governance chain"); + proxied.submitNewGuardianSet(_vm); + } + + function testSubmitNewGuardianSet_Revert_WrongGovernanceContract( + bytes32 storageSlot, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + bytes32 emitterAddress, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId, + address[] memory newGuardianSet) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(emitterAddress != governanceContract); + vm.assume(chainId == 0 || (chainId == CHAINID && evmChainId == EVMCHAINID)); + vm.assume(0 < newGuardianSet.length); + vm.assume(newGuardianSet.length < 20); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitNewGuardianSet(MODULE, chainId, 1, newGuardianSet); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, emitterAddress, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("wrong governance contract"); + proxied.submitNewGuardianSet(_vm); + } + + function testSubmitNewGuardianSet_Revert_ReplayAttack( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + address[] memory newGuardianSet) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(storageSlot != hashedLocationOffset(0, GUARDIANSETS_SLOT, 1)); + vm.assume(storageSlot != hashedLocationOffset(0, GUARDIANSETS_SLOT, 0)); + vm.assume(storageSlot != GUARDIANSETINDEX_SLOT); + vm.assume(0 < newGuardianSet.length); + vm.assume(newGuardianSet.length < 20); + for(uint8 i = 0; i < newGuardianSet.length; i++) + vm.assume(newGuardianSet[i] != address(0)); + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitNewGuardianSet(MODULE, CHAINID, 1, newGuardianSet); + (bytes memory _vm, bytes32 hash) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + proxied.submitNewGuardianSet(_vm); + + // The error message is not "governance action already consumed" because the guardian set index is updated, + // and the check for the current guardian set index comes first than the check for action already consumed + vm.expectRevert("not signed by current guardian set"); + proxied.submitNewGuardianSet(_vm); + } + + function isReservedAddress(address addr) internal view returns (bool) { + return + // Avoid precompiled contracts + addr <= address(0x9) || + // Wormhole contract does not accept assets + addr == address(impl) || + // Setup contract + addr == address(setup) || + // Test contract + addr == address(this) || + // Cheatcode contract + addr == address(vm) || + // Create2Deployer address + addr == address(0x4e59b44847b379578588920cA78FbF26c0B4956C); + } + + function testSubmitTransferFees( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 amount, + bytes32 recipient) + public + unchangedStorage(address(proxied), storageSlot) + { + // Avoid reserved addresses (which will cause the transfer to revert) + vm.assume(!isReservedAddress(address(uint160(uint256(recipient))))); + + vm.chainId(EVMCHAINID); + vm.deal(address(proxied), amount); + + bytes memory payload = payloadSubmitTransferFees(MODULE, CHAINID, amount, recipient); + (bytes memory _vm, bytes32 hash) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + address payable receiver = payable(address(uint160(uint256(recipient)))); + uint256 previousBalance = receiver.balance; + + proxied.submitTransferFees(_vm); + + assertEq(receiver.balance, previousBalance + amount); + assertEq(address(proxied).balance, 0); + assertEq(true, proxied.governanceActionIsConsumed(hash)); + } + + function testSubmitTransferFees_Revert_InvalidModule( + bytes32 storageSlot, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + bytes32 module, + uint16 chainId, + uint256 amount, + bytes32 recipient) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(module != MODULE); + vm.assume(chainId == 0 || (chainId == CHAINID && evmChainId == EVMCHAINID)); + vm.chainId(evmChainId); + vm.deal(address(proxied), amount); + + bytes memory payload = payloadSubmitTransferFees(module, CHAINID, amount, recipient); + bytes memory body = abi.encodePacked( + timestamp, nonce, uint16(1), governanceContract, sequence, consistencyLevel, payload); + + bytes32 hash = keccak256(abi.encodePacked(keccak256(body))); + + bytes memory _vm = bytes.concat(validVmHeader(0), validSignature(testGuardian, hash), body); + + vm.expectRevert("invalid Module"); + proxied.submitTransferFees(_vm); + } + + function testSubmitTransferFees_Revert_InvalidChain( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId, + uint256 amount, + bytes32 recipient) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(chainId != CHAINID && chainId != 0); + vm.chainId(EVMCHAINID); + vm.deal(address(proxied), amount); + + bytes memory payload = payloadSubmitTransferFees(MODULE, chainId, amount, recipient); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("invalid Chain"); + proxied.submitTransferFees(_vm); + } + + function testSubmitTransferFees_Revert_InvalidEvmChain( + bytes32 storageSlot, + uint64 evmchainId, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 amount, + bytes32 recipient) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(evmchainId != EVMCHAINID); + vm.chainId(evmchainId); + vm.deal(address(proxied), amount); + + bytes memory payload = payloadSubmitTransferFees(MODULE, CHAINID, amount, recipient); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("invalid Chain"); + proxied.submitTransferFees(_vm); + } + + + function testSubmitTransferFees_Revert_InvalidGuardianSet( + bytes32 storageSlot, + uint64 evmChainId, + uint32 guardianSetIndex, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId, + uint256 amount, + bytes32 recipient) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(guardianSetIndex != 0); + vm.assume(chainId == 0 || (chainId == CHAINID && evmChainId == EVMCHAINID)); + vm.chainId(evmChainId); + vm.deal(address(proxied), amount); + + bytes memory payload = payloadSubmitTransferFees(MODULE, chainId, amount, recipient); + (bytes memory _vm, ) = validVm( + guardianSetIndex, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + // Since the current version of the test uses only one guardian set, + // in practice only the 'else' branch will be taken + if (guardianSetIndex < proxied.getCurrentGuardianSetIndex()) { + vm.expectRevert("not signed by current guardian set"); + } else { + vm.expectRevert("invalid guardian set"); + } + + proxied.submitTransferFees(_vm); + } + + function testSubmitTransferFees_Revert_WrongGovernanceChain( + bytes32 storageSlot, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + uint16 emitterChainId, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId, + uint256 amount, + bytes32 recipient) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(emitterChainId != 1); + vm.assume(chainId == 0 || (chainId == CHAINID && evmChainId == EVMCHAINID)); + vm.chainId(evmChainId); + vm.deal(address(proxied), amount); + + bytes memory payload = payloadSubmitTransferFees(MODULE, chainId, amount, recipient); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, emitterChainId, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("wrong governance chain"); + proxied.submitTransferFees(_vm); + } + + function testSubmitTransferFees_Revert_WrongGovernanceContract( + bytes32 storageSlot, + uint64 evmChainId, + uint32 timestamp, + uint32 nonce, + bytes32 emitterAddress, + uint64 sequence, + uint8 consistencyLevel, + uint16 chainId, + uint256 amount, + bytes32 recipient) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(emitterAddress != governanceContract); + vm.assume(chainId == 0 || (chainId == CHAINID && evmChainId == EVMCHAINID)); + vm.chainId(evmChainId); + vm.deal(address(proxied), amount); + + bytes memory payload = payloadSubmitTransferFees(MODULE, chainId, amount, recipient); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, emitterAddress, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("wrong governance contract"); + proxied.submitTransferFees(_vm); + } + + function testSubmitTransferFees_Revert_ReplayAttack( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 amount, + bytes32 recipient) + public + unchangedStorage(address(proxied), storageSlot) + { + // Avoid reserved addresses (which will cause the transfer to revert) + vm.assume(!isReservedAddress(address(uint160(uint256(recipient))))); + + vm.chainId(EVMCHAINID); + vm.deal(address(proxied), amount); + + bytes memory payload = payloadSubmitTransferFees(MODULE, CHAINID, amount, recipient); + (bytes memory _vm, bytes32 hash) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + proxied.submitTransferFees(_vm); + + vm.expectRevert("governance action already consumed"); + proxied.submitTransferFees(_vm); + } + + function testSubmitRecoverChainId( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 evmChainId, + uint16 newChainId) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(storageSlot != CHAINID_SLOT); + vm.assume(storageSlot != EVMCHAINID_SLOT); + vm.assume(evmChainId != EVMCHAINID); + vm.assume(evmChainId < 2 ** 64); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitRecoverChainId(MODULE, evmChainId, newChainId); + (bytes memory _vm, bytes32 hash) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + proxied.submitRecoverChainId(_vm); + + assertEq(true, proxied.governanceActionIsConsumed(hash)); + assertEq(evmChainId, proxied.evmChainId()); + assertEq(newChainId, proxied.chainId()); + } + + function testSubmitRecoverChainId_Revert_NotAFork( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 evmChainId, + uint16 newChainId) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(evmChainId != EVMCHAINID); + vm.chainId(EVMCHAINID); + + bytes memory payload = payloadSubmitRecoverChainId(MODULE, evmChainId, newChainId); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("not a fork"); + proxied.submitRecoverChainId(_vm); + } + + function testSubmitRecoverChainId_Revert_InvalidModule( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + bytes32 module, + uint256 evmChainId, + uint16 newChainId) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(module != MODULE); + vm.assume(evmChainId != EVMCHAINID); + vm.assume(evmChainId < 2 ** 64); + vm.chainId(evmChainId); + + vm.assume(module != MODULE); + bytes memory payload = payloadSubmitRecoverChainId(module, evmChainId, newChainId); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("invalid Module"); + proxied.submitRecoverChainId(_vm); + } + + function testSubmitRecoverChainId_Revert_InvalidEVMChain( + bytes32 storageSlot, + uint64 blockChainId, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 evmChainId, + uint16 newChainId) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(evmChainId != EVMCHAINID); + vm.assume(evmChainId < 2 ** 64); + vm.assume(blockChainId != evmChainId && blockChainId != EVMCHAINID); + vm.chainId(blockChainId); + + bytes memory payload = payloadSubmitRecoverChainId(MODULE, evmChainId, newChainId); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("invalid EVM Chain"); + proxied.submitRecoverChainId(_vm); + } + + + function testSubmitRecoverChainId_Revert_InvalidGuardianSetIndex( + bytes32 storageSlot, + uint32 guardianSetIndex, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 evmChainId, + uint16 newChainId) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(guardianSetIndex != 0); + vm.assume(evmChainId != EVMCHAINID); + vm.assume(evmChainId < 2 ** 64); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitRecoverChainId(MODULE, evmChainId, newChainId); + (bytes memory _vm, ) = validVm( + guardianSetIndex, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + // Since the current version of the test uses only one guardian set, + // in practice only the 'else' branch will be taken + if (guardianSetIndex < proxied.getCurrentGuardianSetIndex()) { + vm.expectRevert("not signed by current guardian set"); + } else { + vm.expectRevert("invalid guardian set"); + } + + proxied.submitRecoverChainId(_vm); + } + + function testSubmitRecoverChainId_Revert_WrongGovernanceChain( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint16 emitterChainId, + uint64 sequence, + uint8 consistencyLevel, + uint256 evmChainId, + uint16 newChainId) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(emitterChainId != 1); + vm.assume(evmChainId != EVMCHAINID); + vm.assume(evmChainId < 2 ** 64); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitRecoverChainId(MODULE, evmChainId, newChainId); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, emitterChainId, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("wrong governance chain"); + proxied.submitRecoverChainId(_vm); + } + + function testSubmitRecoverChainId_Revert_WrongGovernanceContract( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + bytes32 emitterAddress, + uint64 sequence, + uint8 consistencyLevel, + uint256 evmChainId, + uint16 newChainId) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(emitterAddress != governanceContract); + vm.assume(evmChainId != EVMCHAINID); + vm.assume(evmChainId < 2 ** 64); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitRecoverChainId(MODULE, evmChainId, newChainId); + (bytes memory _vm, ) = validVm( + 0, timestamp, nonce, 1, emitterAddress, sequence, consistencyLevel, payload, testGuardian); + + vm.expectRevert("wrong governance contract"); + proxied.submitRecoverChainId(_vm); + } + + function testSubmitRecoverChainId_Revert_ReplayAttack( + bytes32 storageSlot, + uint32 timestamp, + uint32 nonce, + uint64 sequence, + uint8 consistencyLevel, + uint256 evmChainId, + uint16 newChainId) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(storageSlot != CHAINID_SLOT); + vm.assume(storageSlot != EVMCHAINID_SLOT); + vm.assume(evmChainId != EVMCHAINID); + vm.assume(evmChainId < 2 ** 64); + vm.chainId(evmChainId); + + bytes memory payload = payloadSubmitRecoverChainId(MODULE, evmChainId, newChainId); + (bytes memory _vm, bytes32 hash) = validVm( + 0, timestamp, nonce, 1, governanceContract, sequence, consistencyLevel, payload, testGuardian); + + vm.assume(storageSlot != hashedLocation(hash, CONSUMED_ACTIONS_SLOT)); + + proxied.submitRecoverChainId(_vm); + + // The error message is not "governance action already consumed" because the evmChainId is updated, + // and the check for isFork() comes first than the check for action already consumed + vm.expectRevert("not a fork"); + proxied.submitRecoverChainId(_vm); + } +} diff --git a/ethereum/forge-test/GovernanceStructs.t.sol b/ethereum/forge-test/GovernanceStructs.t.sol new file mode 100644 index 0000000000..b1bc80f822 --- /dev/null +++ b/ethereum/forge-test/GovernanceStructs.t.sol @@ -0,0 +1,440 @@ +// test/Messages.sol +// SPDX-License-Identifier: Apache 2 + +pragma solidity ^0.8.0; + +import "../contracts/GovernanceStructs.sol"; +import "forge-test/rv-helpers/TestUtils.sol"; + +contract TestGovernanceStructs is TestUtils { + GovernanceStructs gs; + + function setUp() public { + gs = new GovernanceStructs(); + } + + function testParseContractUpgrade( + bytes32 module, + uint16 chain, + bytes32 newContract + ) public { + uint8 action = 1; + + bytes memory encodedUpgrade = abi.encodePacked( + module, + action, + chain, + newContract + ); + + assertEq(encodedUpgrade.length, 67); + + GovernanceStructs.ContractUpgrade memory cu = + gs.parseContractUpgrade(encodedUpgrade); + + assertEq(cu.module, module); + assertEq(cu.action, action); + assertEq(cu.chain, chain); + assertEq(cu.newContract, address(uint160(uint256(newContract)))); + } + + function testParseContractUpgrade_KEVM( + bytes32 module, + uint16 chain, + bytes32 newContract + ) public symbolic(address(gs)) { + testParseContractUpgrade(module, chain, newContract); + } + + function testParseContractUpgradeWrongAction( + bytes32 module, + uint8 action, + uint16 chain, + bytes32 newContract + ) public { + vm.assume(action != 1); + + bytes memory encodedUpgrade = abi.encodePacked( + module, + action, + chain, + newContract + ); + + assertEq(encodedUpgrade.length, 67); + + vm.expectRevert("invalid ContractUpgrade"); + + gs.parseContractUpgrade(encodedUpgrade); + } + + function testParseContractUpgradeWrongAction_KEVM( + bytes32 module, + uint8 action, + uint16 chain, + bytes32 newContract + ) public symbolic(address(gs)) { + testParseContractUpgradeWrongAction(module, action, chain, newContract); + } + + // Needs loop invariant for unbounded bytes type + function testParseContractUpgradeSizeTooSmall(bytes memory encodedUpgrade) + public + { + vm.assume(encodedUpgrade.length < 67); + + if (32 < encodedUpgrade.length) + encodedUpgrade[32] = bytes1(0x01); // ensure correct action + + vm.expectRevert(); + + gs.parseContractUpgrade(encodedUpgrade); + } + + // Needs loop invariant for unbounded bytes type + function testParseContractUpgradeSizeTooLarge( + bytes32 module, + uint16 chain, + bytes32 newContract, + bytes memory extraBytes + ) public { + vm.assume(0 < extraBytes.length); + + uint8 action = 1; + + bytes memory encodedUpgrade = abi.encodePacked( + module, + action, + chain, + newContract, + extraBytes + ); + + assertGt(encodedUpgrade.length, 67); + + vm.expectRevert("invalid ContractUpgrade"); + + gs.parseContractUpgrade(encodedUpgrade); + } + + function testParseSetMessageFee( + bytes32 module, + uint16 chain, + uint256 messageFee + ) public { + uint8 action = 3; + + bytes memory encodedSetMessageFee = abi.encodePacked( + module, + action, + chain, + messageFee + ); + + assertEq(encodedSetMessageFee.length, 67); + + GovernanceStructs.SetMessageFee memory smf = + gs.parseSetMessageFee(encodedSetMessageFee); + + assertEq(smf.module, module); + assertEq(smf.action, action); + assertEq(smf.chain, chain); + assertEq(smf.messageFee, messageFee); + } + + function testParseSetMessageFee_KEVM( + bytes32 module, + uint16 chain, + uint256 messageFee + ) public symbolic(address(gs)) { + testParseSetMessageFee(module, chain, messageFee); + } + + function testParseSetMessageFeeWrongAction( + bytes32 module, + uint8 action, + uint16 chain, + uint256 messageFee + ) public { + vm.assume(action != 3); + + bytes memory encodedSetMessageFee = abi.encodePacked( + module, + action, + chain, + messageFee + ); + + assertEq(encodedSetMessageFee.length, 67); + + vm.expectRevert("invalid SetMessageFee"); + + gs.parseSetMessageFee(encodedSetMessageFee); + } + + function testParseSetMessageFeeWrongAction_KEVM( + bytes32 module, + uint8 action, + uint16 chain, + uint256 messageFee + ) public symbolic(address(gs)) { + testParseSetMessageFeeWrongAction(module, action, chain, messageFee); + } + + // Needs loop invariant for unbounded bytes type + function testParseSetMessageFeeSizeTooSmall(bytes memory encodedSetMessageFee) + public + { + vm.assume(encodedSetMessageFee.length < 67); + + if (32 < encodedSetMessageFee.length) + encodedSetMessageFee[32] = bytes1(0x03); // ensure correct action + + vm.expectRevert(); + + gs.parseSetMessageFee(encodedSetMessageFee); + } + + // Needs loop invariant for unbounded bytes type + function testParseSetMessageFeeSizeTooLarge( + bytes32 module, + uint16 chain, + uint256 messageFee, + bytes memory extraBytes + ) public { + vm.assume(0 < extraBytes.length); + + uint8 action = 3; + + bytes memory encodedSetMessageFee = abi.encodePacked( + module, + action, + chain, + messageFee, + extraBytes + ); + + assertGt(encodedSetMessageFee.length, 67); + + vm.expectRevert("invalid SetMessageFee"); + + gs.parseSetMessageFee(encodedSetMessageFee); + } + + function testParseTransferFees( + bytes32 module, + uint16 chain, + uint256 amount, + bytes32 recipient + ) public { + uint8 action = 4; + + bytes memory encodedTransferFees = abi.encodePacked( + module, + action, + chain, + amount, + recipient + ); + + assertEq(encodedTransferFees.length, 99); + + GovernanceStructs.TransferFees memory tf = + gs.parseTransferFees(encodedTransferFees); + + assertEq(tf.module, module); + assertEq(tf.action, action); + assertEq(tf.chain, chain); + assertEq(tf.amount, amount); + assertEq(tf.recipient, recipient); + } + + function testParseTransferFees_KEVM( + bytes32 module, + uint16 chain, + uint256 amount, + bytes32 recipient + ) public symbolic(address(gs)) { + testParseTransferFees(module, chain, amount, recipient); + } + + function testParseTransferFeesWrongAction( + bytes32 module, + uint8 action, + uint16 chain, + uint256 amount, + bytes32 recipient + ) public { + vm.assume(action != 4); + + bytes memory encodedTransferFees = abi.encodePacked( + module, + action, + chain, + amount, + recipient + ); + + assertEq(encodedTransferFees.length, 99); + + vm.expectRevert("invalid TransferFees"); + + gs.parseTransferFees(encodedTransferFees); + } + + function testParseTransferFeesWrongAction_KEVM( + bytes32 module, + uint8 action, + uint16 chain, + uint256 amount, + bytes32 recipient + ) public symbolic(address(gs)) { + testParseTransferFeesWrongAction(module, action, chain, amount, recipient); + } + + // Needs loop invariant for unbounded bytes type + function testParseTransferFeesSizeTooSmall(bytes memory encodedTransferFees) + public + { + vm.assume(encodedTransferFees.length < 99); + + if (32 < encodedTransferFees.length) + encodedTransferFees[32] = bytes1(0x04); // ensure correct action + + vm.expectRevert(); + + gs.parseTransferFees(encodedTransferFees); + } + + // Needs loop invariant for unbounded bytes type + function testParseTransferFeesSizeTooLarge( + bytes32 module, + uint16 chain, + uint256 amount, + bytes32 recipient, + bytes memory extraBytes + ) public { + vm.assume(0 < extraBytes.length); + + uint8 action = 4; + + bytes memory encodedTransferFees = abi.encodePacked( + module, + action, + chain, + amount, + recipient, + extraBytes + ); + + assertGt(encodedTransferFees.length, 99); + + vm.expectRevert("invalid TransferFees"); + + gs.parseTransferFees(encodedTransferFees); + } + + function testParseRecoverChainId( + bytes32 module, + uint256 evmChainId, + uint16 newChainId + ) public { + uint8 action = 5; + + bytes memory encodedRecoverChainId = abi.encodePacked( + module, + action, + evmChainId, + newChainId + ); + + assertEq(encodedRecoverChainId.length, 67); + + GovernanceStructs.RecoverChainId memory rci = + gs.parseRecoverChainId(encodedRecoverChainId); + + assertEq(rci.module, module); + assertEq(rci.action, action); + assertEq(rci.evmChainId, evmChainId); + assertEq(rci.newChainId, newChainId); + } + + function testParseRecoverChainId_KEVM( + bytes32 module, + uint256 evmChainId, + uint16 newChainId + ) public symbolic(address(gs)) { + testParseRecoverChainId(module, evmChainId, newChainId); + } + + function testParseRecoverChainIdWrongAction( + bytes32 module, + uint8 action, + uint256 evmChainId, + uint16 newChainId + ) public { + vm.assume(action != 5); + + bytes memory encodedRecoverChainId = abi.encodePacked( + module, + action, + evmChainId, + newChainId + ); + + assertEq(encodedRecoverChainId.length, 67); + + vm.expectRevert("invalid RecoverChainId"); + + gs.parseRecoverChainId(encodedRecoverChainId); + } + + function testParseRecoverChainIdWrongAction_KEVM( + bytes32 module, + uint8 action, + uint256 evmChainId, + uint16 newChainId + ) public symbolic(address(gs)) { + testParseRecoverChainIdWrongAction(module, action, evmChainId, newChainId); + } + + // Needs loop invariant for unbounded bytes type + function testParseRecoverChainIdSizeTooSmall(bytes memory encodedRecoverChainId) + public + { + vm.assume(encodedRecoverChainId.length < 67); + + if (32 < encodedRecoverChainId.length) + encodedRecoverChainId[32] = bytes1(0x05); // ensure correct action + + vm.expectRevert(); + + gs.parseRecoverChainId(encodedRecoverChainId); + } + + // Needs loop invariant for unbounded bytes type + function testParseRecoverChainIdSizeTooLarge( + bytes32 module, + uint256 evmChainId, + uint16 newChainId, + bytes memory extraBytes + ) public { + vm.assume(0 < extraBytes.length); + + uint8 action = 5; + + bytes memory encodedRecoverChainId = abi.encodePacked( + module, + action, + evmChainId, + newChainId, + extraBytes + ); + + assertGt(encodedRecoverChainId.length, 67); + + vm.expectRevert("invalid RecoverChainId"); + + gs.parseRecoverChainId(encodedRecoverChainId); + } +} diff --git a/ethereum/forge-test/Implementation.t.sol b/ethereum/forge-test/Implementation.t.sol new file mode 100644 index 0000000000..e9b0c81583 --- /dev/null +++ b/ethereum/forge-test/Implementation.t.sol @@ -0,0 +1,155 @@ +// test/Messages.sol +// SPDX-License-Identifier: Apache 2 + +pragma solidity ^0.8.0; + +import "../contracts/Implementation.sol"; +import "../contracts/Setup.sol"; +import "../contracts/Wormhole.sol"; +import "../contracts/interfaces/IWormhole.sol"; +import "forge-std/Test.sol"; +import "forge-test/rv-helpers/TestUtils.sol"; + +contract TestImplementation is TestUtils { + event LogMessagePublished(address indexed sender, uint64 sequence, uint32 nonce, bytes payload, uint8 consistencyLevel); + + Wormhole proxy; + Implementation impl; + Setup setup; + Setup proxiedSetup; + IWormhole proxied; + + uint256 constant testGuardian = 93941733246223705020089879371323733820373732307041878556247502674739205313440; + bytes32 constant governanceContract = 0x0000000000000000000000000000000000000000000000000000000000000004; + bytes32 constant MESSAGEFEE_STORAGESLOT = bytes32(uint256(7)); + bytes32 constant SEQUENCES_SLOT = bytes32(uint256(4)); + + function setUp() public { + // Deploy setup + setup = new Setup(); + // Deploy implementation contract + impl = new Implementation(); + // Deploy proxy + proxy = new Wormhole(address(setup), bytes("")); + + address[] memory keys = new address[](1); + keys[0] = 0xbeFA429d57cD18b7F8A4d91A2da9AB4AF05d0FBe; + //keys[0] = vm.addr(testGuardian); + + //proxied setup + proxiedSetup = Setup(address(proxy)); + + vm.chainId(1); + proxiedSetup.setup({ + implementation: address(impl), + initialGuardians: keys, + chainId: 2, + governanceChainId: 1, + governanceContract: governanceContract, + evmChainId: 1 + }); + + proxied = IWormhole(address(proxy)); + } + + function testPublishMessage( + bytes32 storageSlot, + uint256 messageFee, + address alice, + uint256 aliceBalance, + uint32 nonce, + bytes memory payload, + uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + uint64 sequence = proxied.nextSequence(alice); + bytes32 storageLocation = hashedLocation(alice, SEQUENCES_SLOT); + + vm.assume(aliceBalance >= messageFee); + vm.assume(storageSlot != storageLocation); + vm.assume(storageSlot != MESSAGEFEE_STORAGESLOT); + + vm.store(address(proxied), MESSAGEFEE_STORAGESLOT, bytes32(messageFee)); + vm.deal(address(alice),aliceBalance); + + vm.prank(alice); + proxied.publishMessage{value: messageFee}(nonce, payload, consistencyLevel); + + assertEq(sequence + 1, proxied.nextSequence(alice)); + } + + function testPublishMessage_Emit( + bytes32 storageSlot, + uint256 messageFee, + address alice, + uint256 aliceBalance, + uint32 nonce, + bytes memory payload, + uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + uint64 sequence = proxied.nextSequence(alice); + bytes32 storageLocation = hashedLocation(alice, SEQUENCES_SLOT); + + vm.assume(aliceBalance >= messageFee); + vm.assume(storageSlot != storageLocation); + vm.assume(storageSlot != MESSAGEFEE_STORAGESLOT); + + vm.store(address(proxied), MESSAGEFEE_STORAGESLOT, bytes32(messageFee)); + vm.deal(address(alice),aliceBalance); + + vm.prank(alice); + vm.expectEmit(true, true, true, true); + emit LogMessagePublished(alice, sequence, nonce, payload, consistencyLevel); + + proxied.publishMessage{value: messageFee}(nonce, payload, consistencyLevel); + } + + function testPublishMessage_Revert_InvalidFee( + bytes32 storageSlot, + uint256 messageFee, + address alice, + uint256 aliceBalance, + uint256 aliceFee, + uint32 nonce, + bytes memory payload, + uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(aliceBalance >= aliceFee); + vm.assume(aliceFee != messageFee); + vm.assume(storageSlot != MESSAGEFEE_STORAGESLOT); + + vm.store(address(proxied), MESSAGEFEE_STORAGESLOT, bytes32(messageFee)); + vm.deal(address(alice),aliceBalance); + + vm.prank(alice); + vm.expectRevert("invalid fee"); + proxied.publishMessage{value: aliceFee}(nonce, payload, consistencyLevel); + } + + function testPublishMessage_Revert_OutOfFunds( + bytes32 storageSlot, + uint256 messageFee, + address alice, + uint256 aliceBalance, + uint32 nonce, + bytes memory payload, + uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.assume(aliceBalance < messageFee); + vm.assume(storageSlot != MESSAGEFEE_STORAGESLOT); + + vm.store(address(proxied), MESSAGEFEE_STORAGESLOT, bytes32(messageFee)); + vm.deal(address(alice),aliceBalance); + + vm.prank(alice); + vm.expectRevert(); + proxied.publishMessage{value: messageFee}(nonce, payload, consistencyLevel); + } +} diff --git a/ethereum/forge-test/MessagesRV.t.sol b/ethereum/forge-test/MessagesRV.t.sol new file mode 100644 index 0000000000..f74acc4e99 --- /dev/null +++ b/ethereum/forge-test/MessagesRV.t.sol @@ -0,0 +1,214 @@ +// test/Messages.sol +// SPDX-License-Identifier: Apache 2 + +pragma solidity ^0.8.0; + +import "../contracts/Messages.sol"; +import "../contracts/Setters.sol"; +import "../contracts/Structs.sol"; +import "forge-test/rv-helpers/TestUtils.sol"; + +contract TestMessagesRV is TestUtils { + using BytesLib for bytes; + + Messages messages; + + struct GuardianSetParams { + uint256[] privateKeys; + uint8 guardianCount; + uint32 expirationTime; + } + + function setUp() public { + messages = new Messages(); + } + + function paramsAreWellFormed(GuardianSetParams memory params) + internal + pure + returns (bool) + { + return params.guardianCount <= 19 && + params.guardianCount <= params.privateKeys.length; + } + + function generateGuardianSet(GuardianSetParams memory params) + internal + returns (Structs.GuardianSet memory) + { + for (uint8 i = 0; i < params.guardianCount; ++i) + vm.assume(0 < params.privateKeys[i] && + params.privateKeys[i] < SECP256K1_CURVE_ORDER); + + address[] memory guardians = new address[](params.guardianCount); + + for (uint8 i = 0; i < params.guardianCount; ++i) { + guardians[i] = vm.addr(params.privateKeys[i]); + } + + return Structs.GuardianSet(guardians, params.expirationTime); + } + + function generateSignature( + uint8 index, + uint256 privateKey, + address guardian, + bytes32 message + ) + internal + returns (Structs.Signature memory) + { + (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, message); + assertEq(ecrecover(message, v, r, s), guardian); + + return Structs.Signature(r, s, v, index); + } + + function generateSignatures( + uint256[] memory privateKeys, + address[] memory guardians, + bytes32 message + ) + internal + returns (Structs.Signature[] memory) + { + Structs.Signature[] memory sigs = + new Structs.Signature[](guardians.length); + + for (uint8 i = 0; i < guardians.length; ++i) { + sigs[i] = generateSignature( + i, + privateKeys[i], + guardians[i], + message + ); + } + + return sigs; + } + + function isProperSignature(Structs.Signature memory sig, bytes32 message) + internal + pure + returns (bool) + { + address signer = ecrecover(message, sig.v, sig.r, sig.s); + + return signer != address(0); + } + + function testCannotVerifySignaturesWithOutOfBoundsSignature( + bytes memory encoded, + GuardianSetParams memory params, + uint8 outOfBoundsGuardian, + uint8 outOfBoundsAmount + ) public { + vm.assume(encoded.length > 0); + vm.assume(paramsAreWellFormed(params)); + vm.assume(params.guardianCount > 0); + outOfBoundsGuardian = uint8(bound(outOfBoundsGuardian, 0, params.guardianCount - 1)); + outOfBoundsAmount = uint8(bound(outOfBoundsAmount, 0, MAX_UINT8 - params.guardianCount)); + + bytes32 message = keccak256(encoded); + Structs.GuardianSet memory guardianSet = generateGuardianSet(params); + Structs.Signature[] memory sigs = generateSignatures( + params.privateKeys, + guardianSet.keys, + keccak256(encoded) + ); + + sigs[outOfBoundsGuardian].guardianIndex = + params.guardianCount + outOfBoundsAmount; + + vm.expectRevert("guardian index out of bounds"); + messages.verifySignatures(message, sigs, guardianSet); + } + + function testCannotVerifySignaturesWithInvalidSignature1( + bytes memory encoded, + GuardianSetParams memory params, + Structs.Signature memory fakeSignature + ) public { + vm.assume(encoded.length > 0); + vm.assume(paramsAreWellFormed(params)); + vm.assume(fakeSignature.guardianIndex < params.guardianCount); + + bytes32 message = keccak256(encoded); + Structs.GuardianSet memory guardianSet = generateGuardianSet(params); + Structs.Signature[] memory sigs = generateSignatures( + params.privateKeys, + guardianSet.keys, + message + ); + + sigs[fakeSignature.guardianIndex] = fakeSignature; + + // It is very unlikely that the arbitrary fakeSignature will be the + // correct signature for the guardian at that index, so the below + // should be the only reasonable outcomes + if (isProperSignature(fakeSignature, message)) { + (bool valid, string memory reason) = + messages.verifySignatures(message, sigs, guardianSet); + + assertEq(valid, false); + assertEq(reason, "VM signature invalid"); + } else { + vm.expectRevert("ecrecover failed with signature"); + messages.verifySignatures(message, sigs, guardianSet); + } + } + + function testCannotVerifySignaturesWithInvalidSignature2( + bytes memory encoded, + GuardianSetParams memory params, + uint8 fakeGuardianIndex, + uint256 fakeGuardianPrivateKey + ) public { + vm.assume(encoded.length > 0); + vm.assume(paramsAreWellFormed(params)); + vm.assume(fakeGuardianIndex < params.guardianCount); + vm.assume(0 < fakeGuardianPrivateKey && + fakeGuardianPrivateKey < SECP256K1_CURVE_ORDER); + vm.assume(fakeGuardianPrivateKey != params.privateKeys[fakeGuardianIndex]); + + bytes32 message = keccak256(encoded); + Structs.GuardianSet memory guardianSet = generateGuardianSet(params); + Structs.Signature[] memory sigs = generateSignatures( + params.privateKeys, + guardianSet.keys, + message + ); + + address fakeGuardian = vm.addr(fakeGuardianPrivateKey); + sigs[fakeGuardianIndex] = generateSignature( + fakeGuardianIndex, + fakeGuardianPrivateKey, + fakeGuardian, + message + ); + + (bool valid, string memory reason) = messages.verifySignatures(message, sigs, guardianSet); + assertEq(valid, false); + assertEq(reason, "VM signature invalid"); + } + + function testVerifySignatures( + bytes memory encoded, + GuardianSetParams memory params + ) public { + vm.assume(encoded.length > 0); + vm.assume(paramsAreWellFormed(params)); + + bytes32 message = keccak256(encoded); + Structs.GuardianSet memory guardianSet = generateGuardianSet(params); + Structs.Signature[] memory sigs = generateSignatures( + params.privateKeys, + guardianSet.keys, + message + ); + + (bool valid, string memory reason) = messages.verifySignatures(message, sigs, guardianSet); + assertEq(valid, true); + assertEq(bytes(reason).length, 0); + } +} diff --git a/ethereum/forge-test/Setters.t.sol b/ethereum/forge-test/Setters.t.sol new file mode 100644 index 0000000000..e1649ec2b0 --- /dev/null +++ b/ethereum/forge-test/Setters.t.sol @@ -0,0 +1,268 @@ +// test/Messages.sol +// SPDX-License-Identifier: Apache 2 + +pragma solidity ^0.8.0; + +import "forge-test/rv-helpers/MySetters.sol"; +import "forge-test/rv-helpers/TestUtils.sol"; + +contract TestSetters is TestUtils { + MySetters setters; + + function setUp() public { + setters = new MySetters(); + } + + function testUpdateGuardianSetIndex(uint32 index, bytes32 storageSlot) + public + unchangedStorage(address(setters), storageSlot) + { + vm.assume(storageSlot != GUARDIANSETINDEX_STORAGE_INDEX); + + bytes32 originalSlot = vm.load(address(setters), GUARDIANSETINDEX_STORAGE_INDEX); + + setters.updateGuardianSetIndex_external(index); + + bytes32 updatedSlot = vm.load(address(setters), GUARDIANSETINDEX_STORAGE_INDEX); + bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000); + bytes32 expectedSlot = bytes32(uint256(index)) | (mask & originalSlot); + + assertEq(updatedSlot, expectedSlot); + } + + function testUpdateGuardianSetIndex_KEVM(uint32 index, bytes32 storageSlot) + public + symbolic(address(setters)) + { + testUpdateGuardianSetIndex(index, storageSlot); + } + + function testExpireGuardianSet(uint32 timestamp, uint32 index, bytes32 storageSlot) + public + unchangedStorage(address(setters), storageSlot) + { + bytes32 storageLocation = hashedLocationOffset(index,GUARDIANSETS_STORAGE_INDEX,1); + vm.assume(storageSlot != storageLocation); + vm.assume(timestamp <= MAX_UINT32 - 86400); + + bytes32 originalSlot = vm.load(address(setters), storageLocation); + + vm.warp(timestamp); + + setters.expireGuardianSet_external(index); + + bytes32 updatedSlot = vm.load(address(setters), storageLocation); + bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000); + bytes32 expectedSlot = bytes32(uint256(timestamp + 86400)) | (mask & originalSlot); + + assertEq(updatedSlot, expectedSlot); + } + + function testExpireGuardianSet_KEVM(uint32 timestamp, uint32 index, bytes32 storageSlot) + public + symbolic(address(setters)) + { + testExpireGuardianSet(timestamp, index, storageSlot); + } + + function testSetInitialized(address newImplementation, bytes32 storageSlot) + public + unchangedStorage(address(setters), storageSlot) + { + bytes32 storageLocation = hashedLocation(newImplementation, INITIALIZEDIMPLEMENTATIONS_STORAGE_INDEX); + vm.assume(storageSlot != storageLocation); + + bytes32 originalSlot = vm.load(address(setters), storageLocation); + + setters.setInitialized_external(newImplementation); + + bytes32 updatedSlot = vm.load(address(setters), storageLocation); + bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00); + bytes32 expectedSlot = bytes32(uint256(uint8(0x01))) | (mask & originalSlot); + + assertEq(updatedSlot, expectedSlot); + } + + function testSetInitialized_KEVM(address newImplementation, bytes32 storageSlot) + public + symbolic(address(setters)) + { + testSetInitialized(newImplementation, storageSlot); + } + + function testSetGovernanceActionConsumed(bytes32 hash, bytes32 storageSlot) + public + unchangedStorage(address(setters), storageSlot) + { + bytes32 storageLocation = hashedLocation(hash, CONSUMEDGOVACTIONS_STORAGE_INDEX); + vm.assume(storageSlot != storageLocation); + + bytes32 originalSlot = vm.load(address(setters), storageLocation); + + setters.setGovernanceActionConsumed_external(hash); + + bytes32 updatedSlot = vm.load(address(setters), storageLocation); + bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00); + bytes32 expectedSlot = bytes32(uint256(uint8(0x01))) | (mask & originalSlot); + + assertEq(updatedSlot, expectedSlot); + } + + function testSetGovernanceActionConsumed_KEVM(bytes32 hash, bytes32 storageSlot) + public + symbolic(address(setters)) + { + testSetGovernanceActionConsumed(hash, storageSlot); + } + + function testSetChainId(uint16 newChainId, bytes32 storageSlot) + public + unchangedStorage(address(setters), storageSlot) + { + vm.assume(storageSlot != CHAINID_STORAGE_INDEX); + + bytes32 originalSlot = vm.load(address(setters), CHAINID_STORAGE_INDEX); + + setters.setChainId_external(newChainId); + + bytes32 updatedSlot = vm.load(address(setters), CHAINID_STORAGE_INDEX); + bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000); + bytes32 expectedSlot = bytes32(uint256(newChainId)) | (mask & originalSlot); + + assertEq(updatedSlot, expectedSlot); + } + + function testSetChainId_KEVM(uint16 newChainId, bytes32 storageSlot) + public + symbolic(address(setters)) + { + testSetChainId(newChainId, storageSlot); + } + + function testSetGovernanceChainId(uint16 newChainId, bytes32 storageSlot) + public + unchangedStorage(address(setters), storageSlot) + { + vm.assume(storageSlot != CHAINID_STORAGE_INDEX); + + bytes32 originalSlot = vm.load(address(setters), CHAINID_STORAGE_INDEX); + + setters.setGovernanceChainId_external(newChainId); + + bytes32 updatedSlot = vm.load(address(setters), CHAINID_STORAGE_INDEX); + bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000ffff); + bytes32 expectedSlot = bytes32(uint256(newChainId) << 16) | (mask & originalSlot); + + assertEq(updatedSlot, expectedSlot); + } + + function testSetGovernanceChainId_KEVM(uint16 newChainId, bytes32 storageSlot) + public + symbolic(address(setters)) + { + testSetGovernanceChainId(newChainId, storageSlot); + } + + function testSetGovernanceContract(bytes32 newGovernanceContract, bytes32 storageSlot) + public + unchangedStorage(address(setters), storageSlot) + { + vm.assume(storageSlot != GOVERNANCECONTRACT_STORAGE_INDEX); + + setters.setGovernanceContract_external(newGovernanceContract); + + assertEq(newGovernanceContract, vm.load(address(setters), GOVERNANCECONTRACT_STORAGE_INDEX)); + } + + function testSetGovernanceContract_KEVM(bytes32 newGovernanceContract, bytes32 storageSlot) + public + symbolic(address(setters)) + { + testSetGovernanceContract(newGovernanceContract, storageSlot); + } + + function testSetMessageFee(uint256 newFee, bytes32 storageSlot) + public + unchangedStorage(address(setters), storageSlot) + { + vm.assume(storageSlot != MESSAGEFEE_STORAGE_INDEX); + + setters.setMessageFee_external(newFee); + + bytes32 updatedSlot = vm.load(address(setters), MESSAGEFEE_STORAGE_INDEX); + bytes32 expectedSlot = bytes32(newFee); + + assertEq(updatedSlot, expectedSlot); + } + + function testSetMessageFee_KEVM(uint256 newFee, bytes32 storageSlot) + public + symbolic(address(setters)) + { + testSetMessageFee(newFee, storageSlot); + } + + function testSetNextSequence(address emitter, uint64 sequence, bytes32 storageSlot) + public + unchangedStorage(address(setters), storageSlot) + { + bytes32 storageLocation = hashedLocation(emitter, SEQUENCES_STORAGE_INDEX); + vm.assume(storageSlot != storageLocation); + + bytes32 originalSlot = vm.load(address(setters), storageLocation); + + setters.setNextSequence_external(emitter, sequence); + + bytes32 updatedSlot = vm.load(address(setters), storageLocation); + bytes32 mask = bytes32(0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000); + bytes32 expectedSlot = bytes32(uint256(sequence)) | (mask & originalSlot); + + assertEq(updatedSlot, expectedSlot); + } + + function testSetNextSequence_KEVM(address emitter, uint64 sequence, bytes32 storageSlot) + public + symbolic(address(setters)) + { + testSetNextSequence(emitter, sequence, storageSlot); + } + + function testSetEvmChainId_Success(uint256 newEvmChainId, bytes32 storageSlot) + public + unchangedStorage(address(setters), storageSlot) + { + vm.assume(storageSlot != EVMCHAINID_STORAGE_INDEX); + vm.assume(newEvmChainId < 2 ** 64); + + vm.chainId(newEvmChainId); + + setters.setEvmChainId_external(newEvmChainId); + + assertEq(bytes32(newEvmChainId), vm.load(address(setters), EVMCHAINID_STORAGE_INDEX)); + } + + function testSetEvmChainId_Success_KEVM(uint256 newEvmChainId, bytes32 storageSlot) + public + symbolic(address(setters)) + { + testSetEvmChainId_Success(newEvmChainId, storageSlot); + } + + function testSetEvmChainId_Revert(uint256 newEvmChainId, bytes32 storageSlot) + public + unchangedStorage(address(setters), storageSlot) + { + vm.assume(newEvmChainId < 2 ** 64); + vm.assume(newEvmChainId != block.chainid); + + vm.expectRevert("invalid evmChainId"); + setters.setEvmChainId_external(newEvmChainId); + } + + function testSetEvmChainId_Revert_KEVM(uint256 newEvmChainId, bytes32 storageSlot) + public + symbolic(address(setters)) + { + testSetEvmChainId_Revert(newEvmChainId, storageSlot); + } +} diff --git a/ethereum/forge-test/Setup.t.sol b/ethereum/forge-test/Setup.t.sol new file mode 100644 index 0000000000..53278f7715 --- /dev/null +++ b/ethereum/forge-test/Setup.t.sol @@ -0,0 +1,116 @@ +// test/Messages.sol +// SPDX-License-Identifier: Apache 2 + +pragma solidity ^0.8.0; + +import "../contracts/Implementation.sol"; +import "../contracts/Setup.sol"; +import "../contracts/Wormhole.sol"; +import "../contracts/interfaces/IWormhole.sol"; +import "forge-test/rv-helpers/TestUtils.sol"; + +contract TestSetup is TestUtils { + + Wormhole proxy; + Implementation impl; + Setup setup; + Setup proxiedSetup; + IWormhole proxied; + + uint256 constant testGuardian = 93941733246223705020089879371323733820373732307041878556247502674739205313440; + bytes32 constant governanceContract = 0x0000000000000000000000000000000000000000000000000000000000000004; + + function setUp() public { + // Deploy setup + setup = new Setup(); + // Deploy implementation contract + impl = new Implementation(); + // Deploy proxy + proxy = new Wormhole(address(setup), bytes("")); + + address[] memory keys = new address[](1); + keys[0] = 0xbeFA429d57cD18b7F8A4d91A2da9AB4AF05d0FBe; // vm.addr(testGuardian) + + //proxied setup + proxiedSetup = Setup(address(proxy)); + + vm.chainId(1); + proxiedSetup.setup({ + implementation: address(impl), + initialGuardians: keys, + chainId: 2, + governanceChainId: 1, + governanceContract: governanceContract, + evmChainId: 1 + }); + + proxied = IWormhole(address(proxy)); + } + + function testInitialize_after_setup_revert(bytes32 storageSlot, address alice) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.prank(alice); + vm.expectRevert("already initialized"); + proxied.initialize(); + } + + function testInitialize_after_setup_revert_KEVM(bytes32 storageSlot, address alice) + public + { + kevm.infiniteGas(); + testInitialize_after_setup_revert(storageSlot, alice); + } + + function testSetup_after_setup_revert( + bytes32 storageSlot, + address alice, + address implementation, + address initialGuardian, + uint16 chainId, + uint16 governanceChainId, + bytes32 govContract, + uint256 evmChainId) + public + unchangedStorage(address(proxied), storageSlot) + { + address[] memory keys = new address[](1); + keys[0] = initialGuardian; + + vm.prank(alice); + vm.expectRevert("unsupported"); + proxiedSetup.setup({ + implementation: implementation, + initialGuardians: keys, + chainId: chainId, + governanceChainId: governanceChainId, + governanceContract: govContract, + evmChainId: evmChainId + }); + } + + function testSetup_after_setup_revert_KEVM( + bytes32 storageSlot, + address alice, + address implementation, + address initialGuardian, + uint16 chainId, + uint16 governanceChainId, + bytes32 govContract, + uint256 evmChainId) + public + { + kevm.infiniteGas(); + testSetup_after_setup_revert( + storageSlot, + alice, + implementation, + initialGuardian, + chainId, + governanceChainId, + govContract, + evmChainId + ); + } +} diff --git a/ethereum/forge-test/Shutdown.t.sol b/ethereum/forge-test/Shutdown.t.sol new file mode 100644 index 0000000000..ba039c2e70 --- /dev/null +++ b/ethereum/forge-test/Shutdown.t.sol @@ -0,0 +1,86 @@ +// SPDX-License-Identifier: Apache 2 + +pragma solidity ^0.8.0; + +import "../contracts/Implementation.sol"; +import "../contracts/Governance.sol"; +import "../contracts/Setup.sol"; +import "../contracts/Shutdown.sol"; +import "../contracts/Wormhole.sol"; +import "forge-test/rv-helpers/TestUtils.sol"; +import "forge-test/rv-helpers/MyImplementation.sol"; +import "forge-test/rv-helpers/IMyWormhole.sol"; + +contract TestShutdown is TestUtils { + + MyImplementation impl; + + Wormhole proxy; + Setup setup; + Setup proxiedSetup; + IMyWormhole proxied; + + uint256 constant testGuardian = 93941733246223705020089879371323733820373732307041878556247502674739205313440; + bytes32 constant governanceContract = 0x0000000000000000000000000000000000000000000000000000000000000004; + + function setUp() public { + vm.chainId(1); + // Deploy setup + setup = new Setup(); + // Deploy implementation contract + impl = new MyImplementation(1,2); + // Deploy proxy + proxy = new Wormhole(address(setup), bytes("")); + + address[] memory keys = new address[](1); + keys[0] = 0xbeFA429d57cD18b7F8A4d91A2da9AB4AF05d0FBe; + //keys[0] = vm.addr(testGuardian); + + //proxied setup + proxiedSetup = Setup(address(proxy)); + + proxiedSetup.setup({ + implementation: address(impl), + initialGuardians: keys, + chainId: 2, + governanceChainId: 1, + governanceContract: governanceContract, + evmChainId: 1 + }); + + proxied = IMyWormhole(address(proxy)); + upgradeImplementation(); + } + + function upgradeImplementation() internal { + vm.chainId(1); + + Shutdown shutdn = new Shutdown(); + bytes memory payload = payloadSubmitContract( + 0x00000000000000000000000000000000000000000000000000000000436f7265, + 2, + address(shutdn) + ); + (bytes memory _vm, ) = validVm( + 0, 0, 0, 1, governanceContract, 0, 0, payload, testGuardian); + + proxied.submitContractUpgrade(_vm); + } + + function testShutdownInit(address alice, bytes32 storageSlot) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.prank(alice); + proxied.initialize(); + } + + function testShutdown_publishMessage_revert(address alice, bytes32 storageSlot, uint32 nonce, bytes memory payload, uint8 consistencyLevel) + public + unchangedStorage(address(proxied), storageSlot) + { + vm.prank(alice); + vm.expectRevert(); + proxied.publishMessage(nonce,payload,consistencyLevel); + } +} diff --git a/ethereum/forge-test/TokenImplementation.t.sol b/ethereum/forge-test/TokenImplementation.t.sol index c553410359..fb089aafa1 100644 --- a/ethereum/forge-test/TokenImplementation.t.sol +++ b/ethereum/forge-test/TokenImplementation.t.sol @@ -78,7 +78,7 @@ contract TestTokenImplementation is TokenImplementation, Test { address spender, uint256 amount, uint256 deadline - ) public view returns (SignatureSetup memory output) { + ) public returns (SignatureSetup memory output) { // prepare signer allowing for tokens to be spent uint256 sk = uint256(walletPrivateKey); output.allower = vm.addr(sk); diff --git a/ethereum/forge-test/rv-helpers/IMyWormhole.sol b/ethereum/forge-test/rv-helpers/IMyWormhole.sol new file mode 100644 index 0000000000..a0e5716d19 --- /dev/null +++ b/ethereum/forge-test/rv-helpers/IMyWormhole.sol @@ -0,0 +1,11 @@ +// SPDX-License-Identifier: Apache 2 + +pragma solidity ^0.8.0; + +import "contracts/interfaces/IWormhole.sol"; + +interface IMyWormhole is IWormhole { + + function getImplementation() external returns (address); + function upgradeImpl(address newImplementation) external; +} diff --git a/ethereum/forge-test/rv-helpers/KEVMCheats.sol b/ethereum/forge-test/rv-helpers/KEVMCheats.sol new file mode 100644 index 0000000000..ce66cea129 --- /dev/null +++ b/ethereum/forge-test/rv-helpers/KEVMCheats.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: MIT +pragma solidity >=0.6.2 <0.9.0; +pragma experimental ABIEncoderV2; + +interface KEVMCheatsBase { + // Expects a call using the CALL opcode to an address with the specified calldata. + function expectRegularCall(address,bytes calldata) external; + // Expects a call using the CALL opcode to an address with the specified msg.value and calldata. + function expectRegularCall(address,uint256,bytes calldata) external; + // Expects a static call to an address with the specified calldata. + function expectStaticCall(address,bytes calldata) external; + // Expects a delegate call to an address with the specified calldata. + function expectDelegateCall(address,bytes calldata) external; + // Expects that no contract calls are made after invoking the cheatcode. + function expectNoCall() external; + // Expects the given address to deploy a new contract, using the CREATE opcode, with the specified value and bytecode. + function expectCreate(address,uint256,bytes calldata) external; + // Expects the given address to deploy a new contract, using the CREATE2 opcode, with the specified value and bytecode (appended with a bytes32 salt). + function expectCreate2(address,uint256,bytes calldata) external; + // Makes the storage of the given address completely symbolic. + function symbolicStorage(address) external; + // Adds an address to the whitelist. + function allowCallsToAddress(address) external; + // Adds an address and a storage slot to the whitelist. + function allowChangesToStorage(address,uint256) external; + // Set the current cell + function infiniteGas() external; +} + +abstract contract KEVMCheats { + KEVMCheatsBase public constant kevm = KEVMCheatsBase(address(uint160(uint256(keccak256("hevm cheat code"))))); + + // Checks if an address matches one of the built-in addresses. + function notBuiltinAddress(address addr) internal pure returns (bool) { + return (addr != address(645326474426547203313410069153905908525362434349) && + addr != address(1032069922050249630382865877677304880282300743300)); + } +} diff --git a/ethereum/forge-test/rv-helpers/MyImplementation.sol b/ethereum/forge-test/rv-helpers/MyImplementation.sol new file mode 100644 index 0000000000..f860701784 --- /dev/null +++ b/ethereum/forge-test/rv-helpers/MyImplementation.sol @@ -0,0 +1,21 @@ +// SPDX-License-Identifier: Apache 2 + +pragma solidity ^0.8.0; + +import "contracts/Implementation.sol"; + +contract MyImplementation is Implementation { + constructor(uint256 evmChain, uint16 chain) { + setEvmChainId(evmChain); + setChainId(chain); + } + + function getImplementation() public view returns (address impl) { + impl = _getImplementation(); + return impl; + } + + function upgradeImpl(address newImplementation) public { + upgradeImplementation(newImplementation); + } +} diff --git a/ethereum/forge-test/rv-helpers/MySetters.sol b/ethereum/forge-test/rv-helpers/MySetters.sol new file mode 100644 index 0000000000..d2e4388920 --- /dev/null +++ b/ethereum/forge-test/rv-helpers/MySetters.sol @@ -0,0 +1,47 @@ +// SPDX-License-Identifier: Apache 2 + +pragma solidity ^0.8.0; +import "contracts/Setters.sol"; + +contract MySetters is Setters { + + function updateGuardianSetIndex_external(uint32 newIndex) external { + updateGuardianSetIndex(newIndex); + } + + function expireGuardianSet_external(uint32 index) external { + expireGuardianSet(index); + } + + function setInitialized_external(address implementation) external { + setInitialized(implementation); + } + + function setGovernanceActionConsumed_external(bytes32 hash) external { + setGovernanceActionConsumed(hash); + } + + function setChainId_external(uint16 chainId) external { + setChainId(chainId); + } + + function setGovernanceChainId_external(uint16 chainId) external { + setGovernanceChainId(chainId); + } + + function setGovernanceContract_external(bytes32 governanceContract) external { + setGovernanceContract(governanceContract); + } + + function setMessageFee_external(uint256 newFee) external { + setMessageFee(newFee); + } + + function setNextSequence_external(address emitter, uint64 sequence) external { + setNextSequence(emitter, sequence); + } + + function setEvmChainId_external(uint256 evmChainId) external { + setEvmChainId(evmChainId); + } +} diff --git a/ethereum/forge-test/rv-helpers/TestUtils.sol b/ethereum/forge-test/rv-helpers/TestUtils.sol new file mode 100644 index 0000000000..84ae0261a2 --- /dev/null +++ b/ethereum/forge-test/rv-helpers/TestUtils.sol @@ -0,0 +1,187 @@ +// test/Messages.sol +// SPDX-License-Identifier: Apache 2 + +pragma solidity ^0.8.0; + +import "forge-std/Test.sol"; +import "forge-test/rv-helpers/KEVMCheats.sol"; + +uint32 constant MAX_UINT8 = 0xff; +uint32 constant MAX_UINT16 = 0xffff; +uint32 constant MAX_UINT32 = 0xffffffff; + +bytes32 constant CHAINID_STORAGE_INDEX = bytes32(uint256(0)); +bytes32 constant GOVERNANCECONTRACT_STORAGE_INDEX = bytes32(uint256(1)); +bytes32 constant GUARDIANSETS_STORAGE_INDEX = bytes32(uint256(2)); +bytes32 constant GUARDIANSETINDEX_STORAGE_INDEX = bytes32(uint256(3)); +bytes32 constant SEQUENCES_STORAGE_INDEX = bytes32(uint256(4)); +bytes32 constant CONSUMEDGOVACTIONS_STORAGE_INDEX = bytes32(uint256(5)); +bytes32 constant INITIALIZEDIMPLEMENTATIONS_STORAGE_INDEX = bytes32(uint256(6)); +bytes32 constant MESSAGEFEE_STORAGE_INDEX = bytes32(uint256(7)); +bytes32 constant EVMCHAINID_STORAGE_INDEX = bytes32(uint256(8)); + +uint256 constant SECP256K1_CURVE_ORDER = + 115792089237316195423570985008687907852837564279074904382605163141518161494337; + +contract TestUtils is Test, KEVMCheats { + + // Returns the index hash of the storage slot of a map at location `index` and the key `_key`. + function hashedLocation(address _key, bytes32 _index) public pure returns(bytes32) { + // returns `keccak(#buf(32,_key) +Bytes #buf(32, index)) + return keccak256(abi.encode(_key, _index)); + } + + // Returns the index hash of the storage slot of a map at location `index` and the key `_key`. + function hashedLocation(bytes32 _key, bytes32 _index) public pure returns(bytes32) { + // returns `keccak(#buf(32,_key) +Bytes #buf(32, index)) + return keccak256(abi.encode(_key, _index)); + } + + // Returns the index hash of the storage slot of a map at location `index` and the key `_key`. + function hashedLocationOffset(uint32 _key, bytes32 _index, uint256 offset) public pure returns(bytes32) { + // returns `keccak(#buf(32,_key) +Bytes #buf(32, index)) + return bytes32(uint256(keccak256(abi.encode(_key, _index))) + offset); + } + + // Updates an address's storage slot with the given content, using a bitmask. + // The bitmask should set to 0 those bits that will be updated with the new content. + // It is assumed that the new content fits in the 0 region of the bitmask. + function storeWithMask(address contractAddress, bytes32 storageSlot, bytes32 content, bytes32 mask) public returns (bytes32) { + bytes32 originalStorage = vm.load(contractAddress, storageSlot); + bytes32 updatedStorage = (mask & originalStorage) | content; + vm.store(contractAddress, storageSlot, updatedStorage); + return updatedStorage; + } + + // Uses KEVM cheatcodes to make the gas and contract storage symbolic. + modifier symbolic(address contractAddress){ + kevm.infiniteGas(); + kevm.symbolicStorage(contractAddress); + _; + } + + // Asserts that the given storage slot doesn't change in the given contract. + modifier unchangedStorage(address contractAddress, bytes32 storageSlot) { + bytes32 initialStorage = vm.load(contractAddress, storageSlot); + _; + bytes32 finalStorage = vm.load(contractAddress, storageSlot); + assertEq(initialStorage, finalStorage); + } + + function validVmHeader(uint32 guardianSetIndex) internal pure returns (bytes memory vmH) { + uint8 version = 1; + uint8 signersLen = 1; + uint8 guardianIndex = 0; + + vmH = abi.encodePacked( + version, + guardianSetIndex, + signersLen, + guardianIndex + ); + } + + function payloadSubmitContract(bytes32 module, uint16 chainId, address newImpl) internal pure returns (bytes memory payload) { + uint8 action = 1; + bytes32 newContract = bytes32(uint256(uint160(newImpl))); + + payload = abi.encodePacked( + module, + action, + chainId, + newContract + ); + } + + function payloadSubmitMessageFee(bytes32 module, uint16 chainId, uint256 newMessageFee) internal pure returns (bytes memory payload) { + uint8 action = 3; + + payload = abi.encodePacked( + module, + action, + chainId, + newMessageFee + ); + } + + function payloadSubmitNewGuardianSet(bytes32 module, uint16 chainId, uint32 newGuardianSetIndex, address[] memory keys) internal pure returns (bytes memory payload) { + uint8 action = 2; + uint8 keysLength = uint8(keys.length); + + payload = abi.encodePacked( + module, + action, + chainId, + newGuardianSetIndex, + keysLength + ); + + for(uint8 i = 0; i < keysLength; i++) + payload = abi.encodePacked(payload, keys[i]); + } + + function payloadSubmitTransferFees(bytes32 module, uint16 chainId, uint256 amount, bytes32 recipient) internal pure returns (bytes memory payload) { + uint8 action = 4; + + payload = abi.encodePacked( + module, + action, + chainId, + amount, + recipient + ); + } + + function payloadSubmitRecoverChainId(bytes32 module, uint256 evmChainId, uint16 newChainId) internal pure returns (bytes memory payload) { + uint8 action = 5; + + payload = abi.encodePacked( + module, + action, + evmChainId, + newChainId + ); + } + + + function validVm( + uint32 guardianSetIndex, + uint32 timestamp, + uint32 nonce, + uint16 emitterChainId, + bytes32 emitterAddress, + uint64 sequence, + uint8 consistencyLevel, + bytes memory payload, + uint256 pk) + internal + returns (bytes memory _vm, bytes32 hash) + { + bytes memory header = validVmHeader(guardianSetIndex); + + bytes memory body = abi.encodePacked( + timestamp, + nonce, + emitterChainId, + emitterAddress, + sequence, + consistencyLevel, + payload + ); + + hash = keccak256(abi.encodePacked(keccak256(body))); + + bytes memory signature = validSignature(pk, hash); + + _vm = bytes.concat(header, signature, body); + } + + function validSignature(uint256 pk, bytes32 hash) public returns (bytes memory signature) { + uint8 v; + bytes32 r; + bytes32 s; + (v, r, s) = vm.sign(pk, hash); + + signature = abi.encodePacked(r, s,(v - 27)); + } +} diff --git a/ethereum/run-kevm.sh b/ethereum/run-kevm.sh new file mode 100755 index 0000000000..b051b838af --- /dev/null +++ b/ethereum/run-kevm.sh @@ -0,0 +1,113 @@ +#!/usr/bin/env bash +set -euxo pipefail + +forge_build() { + # Avoid building Migrator contract (see PROOFS.md for explanation) + forge build --skip Migrator.sol +} + +foundry_kompile() { + kevm foundry-kompile --verbose \ + --require wormhole-lemmas.k \ + --module-import WORMHOLE-LEMMAS \ + ${rekompile} \ + ${regen} +} + +foundry_prove() { + kevm foundry-prove \ + --max-depth ${max_depth} \ + --max-iterations ${max_iterations} \ + --workers ${workers} \ + --verbose \ + ${reinit} \ + ${debug} \ + ${simplify_init} \ + ${implication_every_block} \ + ${break_every_step} \ + ${break_on_calls} \ + ${auto_abstract} \ + ${tests[*]} +} + +max_depth=5000 +max_iterations=5000 + +# Number of processes run by the prover in parallel +# Should be at most (M - 8) / 8 in a machine with M GB of RAM +workers=1 + +# Switch the options below to turn them on or off + +# Turn on to regenerate K definitions if Solidity code or KEVM version changes +regen=--regen +regen= + +# Turn on if new lemmas have been added to wormhole-lemmas.k (subsumed by --regen) +rekompile=--rekompile +rekompile= + +# Progress is saved automatically so an unfinished proof can be resumed from where it left off +# Turn on to restart proof from the beginning instead of resuming +reinit=--reinit +reinit= + +debug=--debug +debug= + +simplify_init=--no-simplify-init +simplify_init= + +implication_every_block=--implication-every-block +implication_every_block= + +break_every_step=--break-every-step +break_every_step= + +# Turn off to save the state before every call to the KCFG +break_on_calls= +break_on_calls=--no-break-on-calls + +auto_abstract=--auto-abstract +auto_abstract= + +# List of tests to symbolically execute + +tests=( + "--test TestSetters.testUpdateGuardianSetIndex_KEVM " + "--test TestSetters.testExpireGuardianSet_KEVM " + "--test TestSetters.testSetMessageFee_KEVM " + "--test TestSetters.testSetGovernanceContract_KEVM " + "--test TestSetters.testSetInitialized_KEVM " + "--test TestSetters.testSetGovernanceActionConsumed_KEVM " + "--test TestSetters.testSetChainId_KEVM " + "--test TestSetters.testSetGovernanceChainId_KEVM " + "--test TestSetters.testSetNextSequence_KEVM " + "--test TestSetters.testSetEvmChainId_Success_KEVM " + "--test TestSetters.testSetEvmChainId_Revert_KEVM " + "--test TestGetters.testGetGuardianSetIndex_KEVM " + "--test TestGetters.testGetMessageFee_KEVM " + "--test TestGetters.testGetGovernanceContract_KEVM " + "--test TestGetters.testIsInitialized_KEVM " + "--test TestGetters.testGetGovernanceActionConsumed_KEVM " + "--test TestGetters.testChainId_KEVM " + "--test TestGetters.testGovernanceChainId_KEVM " + "--test TestGetters.testNextSequence_KEVM " + "--test TestGetters.testEvmChainId_KEVM " + "--test TestGovernanceStructs.testParseContractUpgrade_KEVM " + "--test TestGovernanceStructs.testParseContractUpgradeWrongAction_KEVM " + "--test TestGovernanceStructs.testParseSetMessageFee_KEVM " + "--test TestGovernanceStructs.testParseSetMessageFeeWrongAction_KEVM " + "--test TestGovernanceStructs.testParseTransferFees_KEVM " + "--test TestGovernanceStructs.testParseTransferFeesWrongAction_KEVM " + "--test TestGovernanceStructs.testParseRecoverChainId_KEVM " + "--test TestGovernanceStructs.testParseRecoverChainIdWrongAction_KEVM " + "--test TestSetup.testInitialize_after_setup_revert_KEVM " + "--test TestSetup.testSetup_after_setup_revert_KEVM " +) + +# Comment these lines as needed +pkill kore-rpc || true +forge_build +foundry_kompile +foundry_prove diff --git a/ethereum/wormhole-lemmas.k b/ethereum/wormhole-lemmas.k new file mode 100644 index 0000000000..46914a3ed0 --- /dev/null +++ b/ethereum/wormhole-lemmas.k @@ -0,0 +1,240 @@ +requires "evm.md" +requires "foundry.md" + +module WORMHOLE-LEMMAS + imports FOUNDRY + imports INFINITE-GAS + imports SET-SYMBOLIC + + syntax StepSort ::= Int + | Bool + | Bytes + | Set + // ------------------------ + + syntax KItem ::= runLemma ( StepSort ) + | doneLemma( StepSort ) + // -------------------------------------- + + syntax Int ::= "notMaxUInt8" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00 */ + | "notMaxUInt16" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF0000 */ + | "notMaxUInt32" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00000000 */ + | "notMaxUInt64" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF0000000000000000 */ + | "notMaxUInt240" [alias] /* FFFF000000000000000000000000000000000000000000000000000000000000 */ + | "notMaxUInt248" [alias] /* FF00000000000000000000000000000000000000000000000000000000000000 */ + // ------------------------------------------------------------------------------------------------------------ + + rule notMaxUInt8 => 115792089237316195423570985008687907853269984665640564039457584007913129639680 + + rule notMaxUInt16 => 115792089237316195423570985008687907853269984665640564039457584007913129574400 + + rule notMaxUInt32 => 115792089237316195423570985008687907853269984665640564039457584007908834672640 + + rule notMaxUInt64 => 115792089237316195423570985008687907853269984665640564039439137263839420088320 + + rule notMaxUInt240 => 115790322390251417039241401711187164934754157181743688420499462401711837020160 + + rule notMaxUInt248 => 115339776388732929035197660848497720713218148788040405586178452820382218977280 + + rule runLemma(T) => doneLemma(T) ... + + rule notMaxUInt248 &Int ( X < X < X < X <>Int 16 ) => X + requires #rangeUInt ( 16 , X ) + [simplification] + + rule maxUInt16 &Int ( ( ( X < X + requires #rangeUInt ( 16 , X ) + [simplification] + + rule maxUInt8 &Int ( X |Int ( notMaxUInt8 &Int _ ) ) => X + requires #rangeUInt ( 8 , X ) + [simplification] + + rule maxUInt16 &Int ( X |Int ( notMaxUInt16 &Int _ ) ) => X + requires #rangeUInt ( 16 , X ) + [simplification] + + rule maxUInt32 &Int ( X |Int ( notMaxUInt32 &Int _ ) ) => X + requires #rangeUInt ( 32 , X ) + [simplification] + + rule maxUInt64 &Int ( X |Int ( notMaxUInt64 &Int _ ) ) => X + requires #rangeUInt ( 64 , X ) + [simplification] + + rule notMaxUInt16 &Int X => 0 + requires #rangeUInt ( 16 , X ) + [simplification] + + rule notMaxUInt32 &Int X => 0 + requires #rangeUInt ( 32 , X ) + [simplification] + + rule notMaxUInt64 &Int X => 0 + requires #rangeUInt ( 64 , X ) + [simplification] + + rule maxUInt32 &Int X => X + requires #rangeUInt ( 32 , X ) + [simplification] + + rule #lookup ( MAP [ KEY1 <- _ ] , KEY2 ) => #lookup ( MAP , KEY2 ) + requires KEY1 =/=Int KEY2 + [simplification] + + rule chop ( I:Int ) => I modInt pow256 [simplification, smt-lemma] + + rule A &Int B => B &Int A + [symbolic(A), concrete(B), simplification] + + // Not being able to generalize this for some reason + rule (X < true + requires #rangeUInt ( 8 , X ) + [simplification] + + rule (X < true + requires #rangeUInt ( 16 , X ) + [simplification] + + rule (X < true + requires #rangeUInt ( 240 , X ) + [simplification] + + rule 0 <=Int (X < true + requires 0 <=Int X andBool 0 <=Int Y + [simplification] + + rule ( ( X modInt N ) +Int Y ) modInt N => (X +Int Y) modInt N + [simplification] + + rule X xorInt maxUInt256 => maxUInt256 -Int X + requires #rangeUInt ( 256 , X ) + [simplification] + + rule X <=Int 115792089237316195423570985008687907853269984665640564039457584007913129639934 => X =/=Int maxUInt256 + requires #rangeUInt ( 256 , X ) + [simplification] + + rule keccak ( _ ) ==Int maxUInt256 => false + [simplification] + + rule 1 |Int _ ==Int 0 => false + [simplification] + + rule (A |Int B) ==Int (B |Int A) => true + [simplification, smt-lemma] + + rule maxUInt8 &Int #asWord ( X ) => #asWord ( #range ( X , 31 , 1 ) ) + requires lengthBytes ( X ) ==Int 32 + [simplification] + + rule maxUInt16 &Int #asWord ( X ) => #asWord ( #range ( X , 30 , 2 ) ) + requires lengthBytes ( X ) ==Int 32 + [simplification] + + rule #buf ( 32 , #asWord ( X ) ) => X + requires lengthBytes ( X ) ==Int 32 + [simplification] + + rule #buf ( 32 , X < #buf ( 1 , X ) +Bytes #buf ( 31 , 0 ) + requires #rangeUInt ( 8 , X ) + [simplification] + + rule #buf ( 32 , X < #buf ( 2 , X ) +Bytes #buf ( 30 , 0 ) + requires #rangeUInt ( 16 , X ) + [simplification] + + rule #range ( X , S1 , W1 ) +Bytes #range ( X , S2 , W2 ) => #range ( X , S1 , W1 +Int W2 ) + requires S1 +Int W1 ==Int S2 + andBool S2 +Int W2 <=Int lengthBytes ( X ) + [simplification] + + rule ( X < true + requires 0 <=Int X + [simplification, smt-lemma] +endmodule + +module WORMHOLE-LEMMAS-SPEC + imports WORMHOLE-LEMMAS + + claim [lowest-32-bits]: runLemma ( VV0_index_114b9705:Int ==Int ( maxUInt32 &Int ( VV0_index_114b9705:Int |Int ( notMaxUInt32 &Int #lookup ( _STORAGE:Map , 11 ) ) ) ) ) + => doneLemma ( true ) ... + requires #rangeUInt ( 32 , VV0_index_114b9705 ) + + claim [chop-successor-key]: runLemma ( #lookup ( STORAGE [ chop ( KEY +Int 1 ) <- _ ] , KEY ) ) + => doneLemma ( #lookup ( STORAGE , KEY ) ) ... + + claim [chop-successor]: runLemma ( chop ( KEY +Int 1 ) =/=Int KEY ) + => doneLemma ( true ) ... + + claim [bits-16-to-31]: runLemma ( ( 65535 &Int ( ( ( ( ( VV0_newChainId_114b9705:Int < doneLemma ( true ) ... + requires #rangeUInt ( 16 , VV0_newChainId_114b9705 ) + + claim [bits-16-to-31-2]: runLemma ( ( maxUInt16 &Int ( ( ( 4294901760 &Int ( VV0_newChainId_114b9705:Int < doneLemma ( true ) ... + requires #rangeUInt ( 16 , VV0_newChainId_114b9705 ) + + claim [bits-16-to-31-3]: runLemma ( maxUInt16 &Int ( ( ( ( ( X < doneLemma ( X ) ... + requires #rangeUInt ( 16 , X ) + + claim [bits-16-to-31-4]: runLemma ( ( X *Int pow16 ) |Int Y ==Int ( ( ( ( X < doneLemma ( true ) ... + requires #rangeUInt ( 16 , X ) + + claim [bits-16-to-31-5]: runLemma ( ( ( X *Int pow16 ) |Int ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int Y ) ) ==Int ( ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int Y ) |Int ( 4294901760 &Int ( ( X < doneLemma ( true ) ... + requires #rangeUInt ( 16 , X ) + andBool #rangeUInt ( 256 , Y ) + + claim [shift-mask]: runLemma ( ( ( VV0_newChainId_114b9705:Int *Int pow16 ) |Int Y ==Int ( ( ( ( VV0_newChainId_114b9705:Int < doneLemma ( true ) ... + requires #rangeUInt ( 16 , VV0_newChainId_114b9705 ) + + claim [shift-range]: runLemma ( #rangeUInt ( 256 , X < doneLemma ( true ) ... + requires #rangeUInt ( 16 , X ) + + claim [shift-mod]: runLemma ( ( X < doneLemma ( X < + requires #rangeUInt ( 16 , X ) + + claim [lowest-8-bits]: runLemma ( maxUInt8 &Int #asWord ( #range ( #buf ( 32 , X ) , 1 , 31 ) +Bytes #range ( #buf ( 32 , #asWord ( b"\x01" +Bytes #range ( #buf ( 32 , Y ) , 0 , 2 ) +Bytes #range ( #buf ( 32 , Z ) , 0 , 29 ) ) ) , 0 , 1 ) ) ) + => doneLemma ( 1 ) ... + requires #rangeUInt ( 256 , X ) + andBool #rangeUInt ( 256 , Y ) + andBool #rangeUInt ( 256 , Z ) + + claim [highest-8-bits]: runLemma ( maxUInt8 &Int #asWord ( #range ( #buf ( 32 , ( notMaxUInt248 &Int ( ( X < doneLemma ( X ) ... + requires #rangeUInt ( 8 , X ) + + claim [highest-16-bits]: runLemma ( maxUInt16 &Int #asWord ( #range ( #buf ( 32 , X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #range ( #buf ( 32 , ( notMaxUInt240 &Int ( ( Y < doneLemma ( Y ) ... + requires #rangeUInt ( 256 , X ) + andBool #rangeUInt ( 16 , Y ) + + claim [one-byte-range]: runLemma ( #asWord ( #range ( #buf ( 32 , notMaxUInt248 &Int ( X < doneLemma ( true ) ... + requires #rangeUInt ( 8 , X ) + + claim [shift-248]: runLemma ( ( X < doneLemma ( true ) ... + requires #rangeUInt ( 8 , X ) + + claim [length-concat]: runLemma ( lengthBytes ( #range ( #buf ( 32 , _X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #buf ( 2 , Y ) ) ) + => doneLemma ( 32 ) ... + requires #rangeUInt ( 16 , Y ) + + claim [concat-ranges]: runLemma ( #asWord ( #range ( #buf ( 32 , X ) , 0 , 29 ) +Bytes #range ( #buf ( 32 , X ) , 29 , 3 ) ) ) + => doneLemma ( X ) ... + requires #rangeUInt ( 256 , X ) + +endmodule