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 <jeffschroeder@computer.org>

* ethereum: Apply review suggestions to run-kevm script

Co-authored-by: Jeff Schroeder <jeffschroeder@computer.org>

* ethereum: explicit cast to uint8 for some vars

The bound() calls need to be explicitly cast to uint8 from the uint256
that forge-std's bound() returns.

* ethereum: updating some of the RV tests

The definitions don't compile with newer forge/solc.

* ethereum: Add assumption to test that guardian count > 0

Prevents an arithmetic over/underflow error in testCannotVerifySignaturesWithOutOfBoundsSignature, in the expression bound(outOfBoundsGuardian, 0, params.guardianCount - 1)

---------

Co-authored-by: Lucas MT <lucas.tabajara@runtimeverification.com>
Co-authored-by: Jeff Schroeder <jeffschroeder@computer.org>

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

ethereum/PROOFS.md

@@ -0,0 +1,49 @@
+# Instructions to Reproduce the KEVM Proofs
+
+## Dependencies
+
+First, install [Forge](https://github.com/foundry-rs/foundry/tree/master/forge) and run
+
+```
+make dependencies
+```
+
+to install the `forge-std` library in the `lib` folder.
+
+Next, [follow the instructions here](https://github.com/runtimeverification/evm-semantics/) to install KEVM (we recommend the fast installation with kup). All proofs were originally run using the KEVM version corresponding to commit [f5c1795aea0c7d6781c94f0e6d4c434ad3ad1982](https://github.com/runtimeverification/evm-semantics/commit/f5c1795aea0c7d6781c94f0e6d4c434ad3ad1982). To update the installation to a specific KEVM version, run
+
+```
+kup update kevm --version <branch name or commit hash>
+```
+
+## Reproducing the Proofs
+
+Use the following command to run the proofs using KEVM:
+
+```
+./run-kevm.sh
+```
+
+The script first builds the tests with `forge build`, then kompiles them into a KEVM specification and runs the prover.
+
+The script symbolically executes all tests added to the `tests` variable. By default, it is set to run all of the tests that have been verified using KEVM. To run a single test at a time, comment out the lines with the other tests. Tests can also be run in parallel by changing the value of the `workers` variable.
+
+The script is set to resume proofs from where they left off. This means that if a proof is interrupted halfway, running the script again will continue from that point. Similarly, if a proof has already completed, running the script again will do nothing and just report the result. To instead restart from the beginning, turn on the `reinit` option in the script. Also note that if changes are made to the Solidity code, or if you switch to a different KEVM version, you should turn on the `regen` option the next time you run the script.
+
+**Note:** When building the tests, the `run-kevm.sh` script uses the command `forge build --skip Migrator.sol` to avoid building the `Migrator` contract. The reason is that this contract contains a function named `claim`, which currently causes problems because `claim` is a reserved keyword in KEVM (none of the proofs depend on this contract, but KEVM generates definitions for all contracts built by `forge build`). Until this issue is fixed, if `forge build` has previously been run without the `--skip Migrator.sol` option, it is necessary to delete the `out/Migrator.sol` directory before running `run-kevm.sh`. Otherwise, the script will produce the following error:
+```
+[Error] Inner Parser: Parse error: unexpected end of file following token '.'.
+	Source(/path/to/wormhole/ethereum/out/kompiled/foundry.k)
+	Location(7633,23,7633,23)
+	7633 |	    rule  ( Migrator . claim ( V0__amount : uint256 ) => #abiCallData (
+"claim" , #uint256 ( V0__amount ) , .TypedArgs ) )
+	     .	                      ^
+[Error] Inner Parser: Parse error: unexpected token 'uint256' following token
+':'.
+	Source(/path/to/wormhole/ethereum/out/kompiled/foundry.k)
+	Location(7633,45,7633,52)
+	7633 |	    rule  ( Migrator . claim ( V0__amount : uint256 ) => #abiCallData (
+"claim" , #uint256 ( V0__amount ) , .TypedArgs ) )
+	     .	                                            ^~~~~~~
+[Error] Compiler: Had 2 parsing errors.
+```

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);
+    }
+}

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);
+    }
+}

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);
+    }
+}

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);
+    }
+}

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);
+    }
+}

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);
+    }
+}

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
+        );
+    }
+}

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);
+    }
+}

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);

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;
+}

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 <gas> 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));
+    }
+}

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);
+    }
+}

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);
+    }
+}

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));
+    }
+}

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

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 <k> runLemma(T) => doneLemma(T) ... </k>
+
+    rule notMaxUInt248 &Int ( X <<Int 248 ) => X <<Int 248
+        requires #rangeUInt ( 8 , X )
+        [simplification]
+
+    rule notMaxUInt240 &Int ( X <<Int 240 ) => X <<Int 240
+        requires #rangeUInt ( 16 , X )
+        [simplification]
+
+    rule 4294901760 &Int ( X <<Int 16 ) => X <<Int 16
+        requires #rangeUInt ( 16 , X )
+        [simplification]
+
+    rule maxUInt16 &Int ( ( ( X *Int pow16 ) |Int ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int _ ) ) >>Int 16 ) => X
+        requires #rangeUInt ( 16 , X )
+        [simplification]
+
+    rule maxUInt16 &Int ( ( ( X <<Int 16 ) |Int ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int _ ) ) /Int pow16 ) => 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 <<Int 248) <Int pow256 => true
+        requires #rangeUInt ( 8 , X )
+        [simplification]
+
+    rule (X <<Int 240) <Int pow256 => true
+        requires #rangeUInt ( 16 , X )
+        [simplification]
+
+    rule (X <<Int 16) <Int pow256 => true
+        requires #rangeUInt ( 240 , X )
+        [simplification]
+
+    rule 0 <=Int (X <<Int Y) => 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 <<Int 248 ) => #buf ( 1 , X ) +Bytes #buf ( 31 , 0 )
+        requires #rangeUInt ( 8 , X )
+        [simplification]
+
+    rule #buf ( 32 , X <<Int 240 ) => #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 <<Int 16 ) ==Int ( X *Int pow16 ) => true
+        requires 0 <=Int X
+        [simplification, smt-lemma]
+endmodule
+
+module WORMHOLE-LEMMAS-SPEC
+    imports WORMHOLE-LEMMAS
+
+    claim [lowest-32-bits]: <k> runLemma ( VV0_index_114b9705:Int ==Int ( maxUInt32 &Int ( VV0_index_114b9705:Int |Int ( notMaxUInt32 &Int #lookup ( _STORAGE:Map , 11 ) ) ) ) )
+           => doneLemma ( true ) ... </k>
+           requires #rangeUInt ( 32 , VV0_index_114b9705 )
+
+    claim [chop-successor-key]: <k> runLemma ( #lookup ( STORAGE [ chop ( KEY +Int 1 ) <- _ ] , KEY ) )
+           => doneLemma ( #lookup ( STORAGE , KEY ) ) ... </k>
+
+    claim [chop-successor]: <k> runLemma ( chop ( KEY +Int 1 ) =/=Int KEY )
+        => doneLemma ( true ) ... </k>
+
+    claim [bits-16-to-31]: <k> runLemma ( ( 65535 &Int ( ( ( ( ( VV0_newChainId_114b9705:Int <<Int 16 ) modInt 115792089237316195423570985008687907853269984665640564039457584007913129639936 ) &Int 4294901760 ) /Int 65536 ) &Int 65535 ) ) ==Int VV0_newChainId_114b9705:Int )
+        => doneLemma ( true ) ... </k>
+        requires #rangeUInt ( 16 , VV0_newChainId_114b9705 )
+
+    claim [bits-16-to-31-2]: <k> runLemma ( ( maxUInt16 &Int ( ( ( 4294901760 &Int ( VV0_newChainId_114b9705:Int <<Int 16 ) ) |Int ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int #lookup ( _STORAGE:Map , 8 ) ) ) /Int pow16 ) ) ==Int VV0_newChainId_114b9705:Int ) => doneLemma ( true ) ... </k>
+        requires #rangeUInt ( 16 , VV0_newChainId_114b9705 )
+
+    claim [bits-16-to-31-3]: <k> runLemma ( maxUInt16 &Int ( ( ( ( ( X <<Int 16 ) modInt pow256 ) &Int 4294901760 ) /Int pow16 ) &Int maxUInt16 ) ) => doneLemma ( X ) ... </k>
+        requires #rangeUInt ( 16 , X )
+
+    claim [bits-16-to-31-4]: <k> runLemma ( ( X *Int pow16 ) |Int Y ==Int ( ( ( ( X <<Int 16 ) modInt pow256 ) &Int 4294901760 ) |Int Y ) ) => doneLemma ( true ) ... </k>
+        requires #rangeUInt ( 16 , X )
+
+    claim [bits-16-to-31-5]: <k> runLemma ( ( ( X *Int pow16 ) |Int ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int Y ) ) ==Int ( ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int Y ) |Int ( 4294901760 &Int ( ( X <<Int 16 ) modInt pow256 ) ) ) ) => doneLemma ( true ) ... </k>
+        requires #rangeUInt ( 16 , X )
+         andBool #rangeUInt ( 256 , Y )
+
+    claim [shift-mask]: <k> runLemma ( ( ( VV0_newChainId_114b9705:Int *Int pow16 ) |Int Y ==Int ( ( ( ( VV0_newChainId_114b9705:Int <<Int 16 ) modInt pow256 ) &Int 4294901760 ) |Int Y ) ) )
+        => doneLemma ( true ) ... </k>
+        requires #rangeUInt ( 16 , VV0_newChainId_114b9705 )
+
+    claim [shift-range]: <k> runLemma ( #rangeUInt ( 256 , X <<Int 16 ) ) => doneLemma ( true ) ... </k>
+        requires #rangeUInt ( 16 , X )
+
+    claim [shift-mod]: <k> runLemma ( ( X <<Int 16 ) modInt pow256 ) => doneLemma ( X <<Int 16 ) ... </k>
+        requires #rangeUInt ( 16 , X )
+
+    claim [lowest-8-bits]: <k> 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 ) ... </k>
+        requires #rangeUInt ( 256 , X )
+         andBool #rangeUInt ( 256 , Y )
+         andBool #rangeUInt ( 256 , Z )
+
+    claim [highest-8-bits]: <k> runLemma ( maxUInt8 &Int #asWord ( #range ( #buf ( 32 , ( notMaxUInt248 &Int ( ( X <<Int 248 ) modInt pow256 ) ) ) , 0 , 1 ) ) )
+        => doneLemma ( X ) ... </k>
+        requires #rangeUInt ( 8 , X )
+
+    claim [highest-16-bits]: <k> runLemma ( maxUInt16 &Int #asWord ( #range ( #buf ( 32 , X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #range ( #buf ( 32 , ( notMaxUInt240 &Int ( ( Y <<Int 240 ) modInt pow256 ) ) ) , 0 , 2 ) ) )
+        => doneLemma ( Y ) ... </k>
+        requires #rangeUInt ( 256 , X )
+         andBool #rangeUInt ( 16 , Y )
+
+    claim [one-byte-range]: <k> runLemma ( #asWord ( #range ( #buf ( 32 , notMaxUInt248 &Int ( X <<Int 248 ) modInt pow256 ) , 0 , 1 ) ) <Int pow8 )
+        => doneLemma ( true ) ... </k>
+        requires #rangeUInt ( 8 , X )
+
+    claim [shift-248]: <k> runLemma ( ( X <<Int 248 ) <Int pow256 )
+        => doneLemma ( true ) ... </k>
+        requires #rangeUInt ( 8 , X )
+
+    claim [length-concat]: <k> runLemma ( lengthBytes ( #range ( #buf ( 32 , _X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #buf ( 2 , Y ) ) )
+        => doneLemma ( 32 ) ... </k>
+        requires #rangeUInt ( 16 , Y )
+
+    claim [concat-ranges]: <k> runLemma ( #asWord ( #range ( #buf ( 32 , X ) , 0 , 29 ) +Bytes #range ( #buf ( 32 , X ) , 29 , 3 ) ) )
+        => doneLemma ( X ) ... </k>
+        requires #rangeUInt ( 256 , X )
+
+endmodule