Formal Verification

// spec/Vault.spec

using ERC20 as token;

methods {
    function deposit(uint256) external returns (uint256);
    function withdraw(uint256, address, address) external returns (uint256);
    function totalAssets() external returns (uint256) envfree;
    function totalSupply() external returns (uint256) envfree;
    function balanceOf(address) external returns (uint256) envfree;
    function asset() external returns (address) envfree;

    // Summarize external calls
    function _.transfer(address, uint256) external => DISPATCHER(true);
    function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
    function _.balanceOf(address) external => DISPATCHER(true);
}

// Depositing should increase total supply
rule depositIncreasesSupply(uint256 assets) {
    env e;
    uint256 supplyBefore = totalSupply();

    deposit(e, assets);

    uint256 supplyAfter = totalSupply();
    assert supplyAfter >= supplyBefore, "supply must not decrease on deposit";
}

// Solvency: vault always has enough assets to back shares
invariant solvency()
    totalSupply() == 0 || totalAssets() > 0
    {
        preserved deposit(uint256 assets) with (env e) {
            require assets > 0;
        }
    }

// Monotonicity: depositing more gives more shares
rule depositMonotonicity(uint256 assets1, uint256 assets2) {
    env e;
    require assets1 < assets2;

    storage init = lastStorage;

    uint256 shares1 = deposit(e, assets1);

    uint256 shares2 = deposit(e, assets2) at init;

    assert shares2 >= shares1, "more assets should give more shares";
}

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address user] uint256 newBalance (uint256 oldBalance) {
    sumOfBalances = sumOfBalances + newBalance - oldBalance;
}

invariant totalSupplyIsSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

import {Test} from "forge-std/Test.sol";
import {Vault} from "../src/Vault.sol";
import {SymTest} from "halmos-cheatcodes/SymTest.sol";

contract VaultSymbolicTest is Test, SymTest {
    Vault vault;

    function setUp() public {
        vault = new Vault(address(token));
    }

    /// @notice Verify deposit then withdraw returns at least original amount
    function check_depositWithdrawRoundTrip(uint256 assets) public {
        vm.assume(assets > 0 && assets < type(uint128).max);

        deal(address(token), address(this), assets);
        token.approve(address(vault), assets);

        uint256 shares = vault.deposit(assets, address(this));
        uint256 received = vault.redeem(shares, address(this), address(this));

        // Due to rounding, received should be <= assets
        assert(received <= assets);
    }

    /// @notice No share inflation from direct transfer
    function check_noShareInflation(uint256 donation) public {
        vm.assume(donation > 0 && donation < type(uint128).max);

        uint256 sharesBefore = vault.totalSupply();

        // Direct transfer (donation attack)
        deal(address(token), address(vault), donation);

        uint256 sharesAfter = vault.totalSupply();
        assert(sharesAfter == sharesBefore);
    }
}

rule transferIntegrity(address to, uint256 amount) {
    env e;
    address from = e.msg.sender;
    uint256 fromBefore = balanceOf(from);
    uint256 toBefore = balanceOf(to);

    transfer(e, to, amount);

    assert balanceOf(from) == fromBefore - amount;
    assert balanceOf(to) == toBefore + amount;
}

rule onlyOwnerCanPause() {
    env e;
    require e.msg.sender != owner();

    pause@withrevert(e);

    assert lastReverted, "non-owner should not be able to pause";
}

invariant noEtherLeak()
    nativeBalances[currentContract] == 0;

# Install
pip install certora-cli

# Run verification
certoraRun src/Vault.sol \
    --verify Vault:spec/Vault.spec \
    --solc solc8.20 \
    --optimistic_loop \
    --loop_iter 3 \
    --msg "Vault verification"