xWELL

.github/helper/get-env-var.sh

@@ -10,7 +10,7 @@ LATEST_MIP_DIR=$(ls -1v ${BASE_DIR}/ | grep '^mip-b' | tail -n 1)
 
 MIP_NUM=${LATEST_MIP_DIR:5:2}
 
-if [[ "$LATEST_MIP_DIR" == "mip-b07.sol" ]]; then
+if [[ "$LATEST_MIP_DIR" == "mip-b12-moonbeam.sol" ]]; then
     echo "PROPOSAL_ARTIFACT_PATH="
 else
     echo "PROPOSAL_ARTIFACT_PATH=${BASE_DIR}/${LATEST_MIP_DIR}/mipb${MIP_NUM}.json"

.github/workflows/invariant.yml

@@ -0,0 +1,20 @@
+name: Foundry invariant tests
+
+on: [pull_request]
+
+jobs:
+  invariant-tests:
+    name: invariant-tests
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v2
+        with:
+          submodules: recursive
+
+      - name: Setup Environment
+        uses: ./.github/actions
+
+      - name: Invariant Test Contracts
+        run: time forge test -vvv --match-contract InvariantTest

.github/workflows/moonbeam-integration.yml

@@ -4,7 +4,6 @@ on: [pull_request]
 
 env:
   MOONBEAM_API_KEY: ${{secrets.MOONBEAM_API_KEY}}
-  ETHERSCAN_API_KEY: ${{secrets.ETHERSCAN_API_KEY}}
 
 jobs:
   run-moonbeam-tests:

.gitignore

@@ -116,3 +116,7 @@ typescript/node_modules/
 typescript/package-lock.json
 
 typescript/yarn.lock
+
+.certora_internal/
+
+lcov.info

.gitmodules

@@ -7,3 +7,10 @@
 [submodule "lib/solmate"]
 	path = lib/solmate
 	url = https://github.com/transmissions11/solmate
+[submodule "lib/zelt"]
+	path = lib/zelt
+	url = https://github.com/solidity-labs-io/zelt
+	branch = main
+[submodule "lib/openzeppelin-contracts-upgradeable"]
+	path = lib/openzeppelin-contracts-upgradeable
+	url = https://github.com/OpenZeppelin/openzeppelin-contracts-upgradeable

certora/confs/ConfigurablePauseGuardian.conf

@@ -0,0 +1,23 @@
+{
+    "files": [
+        "src/xWELL/xWELL.sol"
+    ],
+    "verify": "xWELL:certora/specs/Pause.spec",
+    "send_only": true,
+    "optimistic_loop": true,
+    "solc": "solc",
+    "msg": "Verification of Configurable Pause Guardian",
+    "rule_sanity": "basic",
+    "packages": [
+        "@forge-std/=lib/forge-std/src/",
+        "@openzeppelin-contracts/=lib/openzeppelin-contracts/",
+        "@openzeppelin-contracts-upgradeable/=lib/openzeppelin-contracts-upgradeable/",
+        "@protocol=src/",
+        "@test=test/",
+        "@proposals=src/proposals/",
+        "@utils/=utils/",
+        "@zelt/=lib/zelt/",
+        "@zelt-src/=lib/zelt/src/",
+        "@zelt-test/=lib/zelt/test/"
+    ]
+}

certora/confs/ERC20.conf

@@ -0,0 +1,23 @@
+{
+    "files": [
+        "src/xWELL/xWELL.sol"
+    ],
+    "verify": "xWELL:certora/specs/ERC20.spec",
+    "send_only": true,
+    "optimistic_loop": true,
+    "solc": "solc",
+    "msg": "Verification of xWELL Token",
+    "rule_sanity": "basic",
+    "packages": [
+        "@forge-std/=lib/forge-std/src/",
+        "@openzeppelin-contracts/=lib/openzeppelin-contracts/",
+        "@openzeppelin-contracts-upgradeable/=lib/openzeppelin-contracts-upgradeable/",
+        "@protocol=src/",
+        "@test=test/",
+        "@proposals=src/proposals/",
+        "@utils/=utils/",
+        "@zelt/=lib/zelt/",
+        "@zelt-src/=lib/zelt/src/",
+        "@zelt-test/=lib/zelt/test/"
+    ]
+}

certora/specs/IERC20.spec

@@ -0,0 +1,23 @@
+methods {
+    function name()                                external returns (string)  envfree;
+    function symbol()                              external returns (string)  envfree;
+    function decimals()                            external returns (uint8)   envfree;
+    function totalSupply()                         external returns (uint256) envfree;
+    function maxSupply()                           external returns (uint256) envfree;
+    function MAX_SUPPLY()                          external returns (uint256) envfree;
+    function balanceOf(address)                    external returns (uint256) envfree;
+    function allowance(address,address)            external returns (uint256) envfree;
+    function approve(address,uint256)              external returns (bool)           ;
+    function transfer(address,uint256)             external returns (bool)           ;
+    function transferFrom(address,address,uint256) external returns (bool)           ;
+    function paused()                              external returns (bool)           ;
+    function buffer(address)                       external returns (uint256)        ;
+    function getPastTotalSupply(uint256)           external returns (uint256)        ;
+    function numCheckpoints(address)               external returns (uint32)  envfree;
+    function delegates(address)                    external returns (address) envfree;
+    function bufferCap(address)                    external returns (uint256) envfree;
+    function getVotes(address)                     external returns (uint256) envfree;
+    function rateLimitPerSecond(address)           external returns (uint256) envfree;
+    function minBufferCap()                        external returns (uint112) envfree;
+    function maxRateLimitPerSecond()               external returns (uint128) envfree;
+}

certora/specs/IERC2612.spec

@@ -0,0 +1,5 @@
+methods {
+    function permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external;
+    function nonces(address)    external returns (uint256)                  envfree;
+    function DOMAIN_SEPARATOR() external returns (bytes32)                  envfree;
+}

certora/specs/IPauseable.spec

@@ -0,0 +1,7 @@
+methods {
+    function pauseStartTime()                      external returns (uint128) envfree;
+    function maxPauseDuration()                    external returns (uint256) envfree;
+    function pauseDuration()                       external returns (uint128) envfree;
+    function pauseGuardian()                       external returns (address) envfree;
+    function paused()                              external returns (bool)           ;
+}

certora/specs/Pause.spec

@@ -0,0 +1,131 @@
+import "helpers.spec";
+import "IERC20.spec";
+import "IERC2612.spec";
+import "IPauseable.spec";
+
+function timestampMax() returns uint256 {
+    return 2 ^ 128 - 1;
+}
+
+function uintMax() returns uint256 {
+    return 2 ^ 256 - 1;
+}
+
+/// Preconditions:
+///    - block timestamp is under or equal uint32 max and gt 0
+
+/// Invariants:
+///     1. paused, pauseStartTime != 0, guardian != address(0)
+///     2. unpaused, pauseStartTime == 0, guardian == address(0)
+///     3. unpaused, pauseStartTime <= block.timestamp - pauseDuration, guardian != address(0)
+///     4. unpaused after kick, pauseStartTime == 0, guardian == address(0)
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Ghost: all state variables                                                                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+ghost address pauseGuardian {
+    init_state axiom pauseGuardian == 0;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Hooks: all state variables                                                                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+/// @title The hook for writing to pause guardian
+hook Sstore pauseGuardian address newPauseGuardian (address oldPauseGuardian) STORAGE
+{
+    pauseGuardian = newPauseGuardian;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariants                                                                                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+invariant pauseGuardianMirrorCorrect()
+    pauseGuardian == pauseGuardian();
+
+invariant pauseDurationLteMax()
+    assert_uint256(pauseDuration()) <= maxPauseDuration();
+
+invariant pausedCorrect(env e)
+    paused(e) => (
+        to_mathint(e.block.timestamp) >= to_mathint(pauseStartTime()) &&
+        to_mathint(e.block.timestamp) <= pauseStartTime() + pauseDuration()
+    ) {
+        preserved {
+            require timestampMax() >= e.block.timestamp;
+            requireInvariant pauseDurationLteMax();
+            requireInvariant pauseGuardianMirrorCorrect();
+        } preserved pause() with (env e1) {
+            require e1.block.timestamp == e.block.timestamp;
+            require timestampMax() >= e1.block.timestamp;
+            requireInvariant pausedCorrect(e1);
+            requireInvariant pauseDurationLteMax();
+            requireInvariant pauseGuardianMirrorCorrect();
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: kick behavior and side effects                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule kickSucceeds(env e) {
+   require pauseUsed(e);
+   require !paused(e);
+   require pauseGuardian != 0;
+
+   address guardianStartingAddress = pauseGuardian;
+
+   kickGuardian(e);
+
+   assert !paused(e), "not unpaused";
+   assert pauseGuardian == 0, "pause guardian address 0";
+   assert pauseStartTime() == 0, "pause start time not reset";
+   assert guardianStartingAddress != 0, "guardianStartingAddress eq 0 address";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pause/unpause behavior and side effects                                                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pauseSucceeds(env e) {
+   /// constrain the prover to a sane block timestamp we will see in this lifetime
+   require e.block.timestamp > 0 && e.block.timestamp <= timestampMax();
+   require !pauseUsed(e);
+   require !paused(e);
+   require pauseGuardian != 0;
+
+   address guardianStartingAddress = pauseGuardian;
+
+   pause(e);
+
+   assert paused(e), "not paused";
+   assert pauseUsed(e) == true, "pause used";
+   assert pauseGuardian == guardianStartingAddress, "pause guardian address 0";
+   assert to_mathint(pauseStartTime()) == to_mathint(e.block.timestamp), "pause start time not set";
+}
+
+rule unpauseSucceeds(env e) {
+   /// constrain the prover to a sane block timestamp we will see in this lifetime
+   require e.block.timestamp > 0 && e.block.timestamp <= timestampMax();
+   require pauseUsed(e);
+   require paused(e);
+   require pauseGuardian != 0;
+
+   address guardianStartingAddress = pauseGuardian;
+
+   unpause(e);
+
+   assert !paused(e), "not paused";
+   assert !pauseUsed(e) == true, "pause should not be used";
+   assert pauseStartTime() == 0, "pause start time not reset";
+   assert pauseGuardian == 0, "pause guardian not kicked";
+   assert guardianStartingAddress != 0, "pause start time not reset";
+}

certora/specs/helpers.spec

@@ -0,0 +1 @@
+definition nonpayable(env e) returns bool = e.msg.value == 0;

docs/xWELL.md

@@ -0,0 +1,60 @@
+# Overview
+
+The xWELL token is an xERC20 compatible token that is meant to be used as a cross chain fungible token. It relies on trusted bridge contracts that are given a rate limit in the MintLimits class. Each bridge has a different rate limit to prevent infinite mints when a single bridge is compromised. A lockbox contract is used on the source chain to allow migration of existing WELL holders over to the new WELL token.
+
+## Frontend Integration
+
+In order to allow token holders to seamlessly use the bridge, the frontend will need to understand the following flows for end users when moving between chains. To go from chain A to chain B, a user must first approve the wormhole or relevant bridge adapter contract the ability to spend their xWELL. Once approved, the user can then call the bridge adapter's `bridge(uint256 dstChainId,uint256 amount,address to)` function. The destination chain id should be the wormhole chainId of the destination chain. The amount should be the amount of xWELL the user wants to bridge. The to address should be the address of the receiving user on the destination chain. The bridge adapter will then transfer the xWELL from the user to the bridge contract, and then the bridge contract will mint the same amount of xWELL on the destination chain. The user will then be able to use the xWELL on the destination chain.
+
+To find out the required amount of gas to be spent to ensure a transaction is successful, the frontend can call the `bridgeCost(uint16 dstChainId)` function on the bridge adapter. This function takes only the destination wormhole chain id the parameter, and returns the maximum amount of gas that should be spent to ensure the transaction is successful. The frontend can then use this value to set the amount native asset to pay for the transaction. This amount of native tokens should be sent in the call to bridge.
+
+### Router Contract
+
+In order to use the router to simplify users migrating from WELL to xWELL, the frontend will need to talk to the router contract. Users will approve the router to spend their WELL and then call `bridgeToBase(address to, uint256 amount)` if to is different from sender, or `bridgeToBase(uint256 amount)` if to is the same as sender. The router will then transfer the WELL from the user to the lockbox contract, and then the lockbox contract will mint the same amount of xWELL to the router, which will then migrate those tokens to xWELL the base chain through the WormholeAdapter. The user must pass the correct amount of GLMR to the router to cover the gas costs of the transaction. The amount can be found by calling the `bridgeCost()` function on the router contract which returns a uint256.
+
+### Events
+
+When a user uses the WormholeBridgeAdapter contract to move tokens from one chain to another, the following events will be emitted
+
+from the xWELL token:
+
+On Mint:
+```Transfer(address(0), to, amount);```
+```BufferUsed(amount, newBufferStored);```
+
+On Burn:
+```Transfer(from, address(0), amount);```
+```BufferReplenished(amount, newBufferStored);```
+
+from the WormholeBridgeAdapter:
+
+on Mint:
+```BridgedIn(chainId, user, amount)```
+```BridgedIn(uint256 indexed srcChainId, address indexed tokenReceiver, uint256 amount);```
+
+on Burn:
+```TokensSent(targetChainId, to, amount);```
+```BridgedOut(uint256 indexed dstChainId, address indexed bridgeUser, address indexed tokenReceiver, uint256 amount);```
+
+## xWELL Token xERC20 Differences
+
+xERC20 enforces a global rate limit per second on each bridge, meaning all bridge's buffers refill at the same speed once depleted. The xWELL implementation allows each bridge to have a different rate limit, allowing for more flexibility in the bridge setup. The xWELL implementation also allows for a bridge to be disabled, preventing any further minting from that bridge. This is useful if a bridge is compromised and needs to be disabled.
+
+### Guardians
+
+The xWELL token has a guardian system that allows for the token to be paused, which disables all bridging functionality. The guardian address is meant to be a multisig contract that requires a quorum of guardians to approve a transaction before it can be executed. The guardian system is meant to be used as a failsafe in case of a bridge compromise or other emergency. Once the guardian pauses the contract, then the pause timer starts. The pause duration is specified in the initializer of the xWELL token, and once the pause duration has passed, the contract automatically unpauses itself. Only the mint and burn functions of the token are disabled while the contract is paused.
+
+The owner can change the pause duration, even while the contract is paused. This allows the owner to extend the pause duration if needed during an emergency situation.
+
+The owner can only grant a new pause guardian if the contract is not paused, and the owner can unpause the contract, which enables them to assign a new pause guardian.
+
+### Ownership
+
+The contract is owned by the Temporal Governor on Base, and by the Moonwell Artemis Timelock on Moonwell. The owner can change the guardian address, and add, remove and change the rate limits on the bridges. The owner can also change the pause duration, even while the contract is paused.
+
+
+### Constants
+
+The xWELL token has a few constants that are used to configure the contract. These constants are:
+- max rate limit per second: The maximum rate limit that a bridge can have is 10k tokens per second. This is used to prevent a bridge from having an unlimited rate limit.
+- max pause duration: The maximum pause duration is 30 days. This is used to prevent the contract from being paused indefinitely.

remappings.txt

@@ -1,6 +1,9 @@
 @forge-std/=lib/forge-std/src/
+@openzeppelin-contracts/=lib/openzeppelin-contracts/
 @openzeppelin/=lib/openzeppelin-contracts/
+@openzeppelin-contracts-upgradeable/=lib/openzeppelin-contracts-upgradeable/
 @protocol=src/
 @test=test/
 @proposals=src/proposals/
-@utils/=utils/
+@utils/=utils/
+@zelt/=lib/zelt/