From 2d58f4ef890887062b6240caefd72d0b3db47f59 Mon Sep 17 00:00:00 2001 From: makemake Date: Thu, 14 May 2026 16:39:04 +0200 Subject: [PATCH 1/2] Add filtered assertion pattern examples --- README.md | 24 -- examples/assertions-book/README.md | 19 -- .../src/ass1-implementation-change.a.sol | 34 --- .../src/ass10-oracle-liveness.a.sol | 46 ---- .../assertions/src/ass11-twap-deviation.a.sol | 62 ----- .../src/ass12-erc4626-assets-shares.a.sol | 30 --- .../src/ass13-erc4626-deposit-withdraw.a.sol | 54 ---- .../src/ass14-fee-verification.a.sol | 38 --- .../src/ass15-price-within-ticks.a.sol | 56 ----- .../src/ass16-liquidation-health-factor.a.sol | 69 ----- .../src/ass17-panic-state-verificatoin.a.sol | 36 --- .../src/ass18-harvest-increases-balance.a.sol | 39 --- .../src/ass19-tokens-borrowed-invariant.a.sol | 33 --- .../src/ass2-erc4626-operations.a.sol | 209 ---------------- .../assertions/src/ass20-erc20-drain.a.sol | 38 --- .../assertions/src/ass21-ether-drain.a.sol | 54 ---- .../src/ass22-erc20-inflow-breaker.a.sol | 38 --- .../src/ass28-intra-tx-oracle-deviation.a.sol | 68 ----- .../assertions/src/ass4-kyc-whitelist.a.sol | 44 ---- .../assertions/src/ass5-owner-change.a.sol | 48 ---- .../src/ass6-constant-product.a.sol | 33 --- .../src/ass7-lending-health-factor.a.sol | 64 ----- .../assertions/src/ass8-positions-sum.a.sol | 44 ---- .../src/ass9-timelock-verification.a.sol | 38 --- .../src/AccreditedInvestorRegistry.sol | 10 - examples/assertions-book/src/MockToken.sol | 39 --- .../src/ass1-implementation-change.sol | 36 --- .../src/ass10-oracle-liveness.sol | 66 ----- .../src/ass11-twap-deviation.sol | 47 ---- .../src/ass12-erc4626-assets-shares.sol | 70 ------ .../src/ass13-erc4626-deposit-withdraw.sol | 233 ----------------- .../src/ass14-fee-verification.sol | 49 ---- .../src/ass15-price-within-ticks.sol | 100 -------- .../src/ass16-liquidation-health-factor.sol | 100 -------- .../src/ass17-panic-state-verificatoin.sol | 64 ----- .../src/ass18-harvest-increases-balance.sol | 68 ----- .../src/ass19-tokens-borrowed-invariant.sol | 89 ------- .../src/ass2-erc4626-operations.sol | 235 ------------------ .../assertions-book/src/ass20-erc20-drain.sol | 131 ---------- .../assertions-book/src/ass21-ether-drain.sol | 115 --------- .../src/ass22-farcaster-message-validity.sol | 115 --------- .../src/ass28-intra-tx-oracle-deviation.sol | 37 --- .../src/ass4-only-accredited-can-mint.sol | 17 -- .../assertions-book/src/ass5-owner-change.sol | 57 ----- .../src/ass6-constant-product.sol | 43 ---- .../src/ass7-lending-health-factor.sol | 68 ----- .../src/ass8-positions-sum.sol | 49 ---- .../src/ass9-timelock-verification.sol | 32 --- examples/micro-patterns/README.md | 19 ++ .../src/AccountingConservation.a.sol | 47 ++++ .../src/CallSandwichHonesty.a.sol | 57 +++++ .../src/ConfigurationGuard.a.sol | 52 ++++ .../src/OracleReduceOnlyGate.a.sol | 75 ++++++ .../micro-patterns/src/ParticipantGate.a.sol | 86 +++++++ .../src/PostOperationSolvency.a.sol | 81 ++++++ .../src/TieredCircuitBreaker.a.sol | 85 +++++++ .../test/.gitkeep | 0 foundry.toml | 15 +- 58 files changed, 508 insertions(+), 3097 deletions(-) delete mode 100644 examples/assertions-book/README.md delete mode 100644 examples/assertions-book/assertions/src/ass1-implementation-change.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass10-oracle-liveness.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass11-twap-deviation.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass12-erc4626-assets-shares.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass13-erc4626-deposit-withdraw.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass14-fee-verification.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass15-price-within-ticks.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass16-liquidation-health-factor.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass17-panic-state-verificatoin.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass18-harvest-increases-balance.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass19-tokens-borrowed-invariant.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass2-erc4626-operations.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass20-erc20-drain.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass21-ether-drain.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass22-erc20-inflow-breaker.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass28-intra-tx-oracle-deviation.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass4-kyc-whitelist.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass5-owner-change.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass6-constant-product.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass7-lending-health-factor.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass8-positions-sum.a.sol delete mode 100644 examples/assertions-book/assertions/src/ass9-timelock-verification.a.sol delete mode 100644 examples/assertions-book/src/AccreditedInvestorRegistry.sol delete mode 100644 examples/assertions-book/src/MockToken.sol delete mode 100644 examples/assertions-book/src/ass1-implementation-change.sol delete mode 100644 examples/assertions-book/src/ass10-oracle-liveness.sol delete mode 100644 examples/assertions-book/src/ass11-twap-deviation.sol delete mode 100644 examples/assertions-book/src/ass12-erc4626-assets-shares.sol delete mode 100644 examples/assertions-book/src/ass13-erc4626-deposit-withdraw.sol delete mode 100644 examples/assertions-book/src/ass14-fee-verification.sol delete mode 100644 examples/assertions-book/src/ass15-price-within-ticks.sol delete mode 100644 examples/assertions-book/src/ass16-liquidation-health-factor.sol delete mode 100644 examples/assertions-book/src/ass17-panic-state-verificatoin.sol delete mode 100644 examples/assertions-book/src/ass18-harvest-increases-balance.sol delete mode 100644 examples/assertions-book/src/ass19-tokens-borrowed-invariant.sol delete mode 100644 examples/assertions-book/src/ass2-erc4626-operations.sol delete mode 100644 examples/assertions-book/src/ass20-erc20-drain.sol delete mode 100644 examples/assertions-book/src/ass21-ether-drain.sol delete mode 100644 examples/assertions-book/src/ass22-farcaster-message-validity.sol delete mode 100644 examples/assertions-book/src/ass28-intra-tx-oracle-deviation.sol delete mode 100644 examples/assertions-book/src/ass4-only-accredited-can-mint.sol delete mode 100644 examples/assertions-book/src/ass5-owner-change.sol delete mode 100644 examples/assertions-book/src/ass6-constant-product.sol delete mode 100644 examples/assertions-book/src/ass7-lending-health-factor.sol delete mode 100644 examples/assertions-book/src/ass8-positions-sum.sol delete mode 100644 examples/assertions-book/src/ass9-timelock-verification.sol create mode 100644 examples/micro-patterns/README.md create mode 100644 examples/micro-patterns/src/AccountingConservation.a.sol create mode 100644 examples/micro-patterns/src/CallSandwichHonesty.a.sol create mode 100644 examples/micro-patterns/src/ConfigurationGuard.a.sol create mode 100644 examples/micro-patterns/src/OracleReduceOnlyGate.a.sol create mode 100644 examples/micro-patterns/src/ParticipantGate.a.sol create mode 100644 examples/micro-patterns/src/PostOperationSolvency.a.sol create mode 100644 examples/micro-patterns/src/TieredCircuitBreaker.a.sol rename examples/{assertions-book => micro-patterns}/test/.gitkeep (100%) diff --git a/README.md b/README.md index 496377d..b284d9d 100644 --- a/README.md +++ b/README.md @@ -6,30 +6,6 @@ Standard library for implementing assertions in the Phylax Credible Layer (PCL). Full API documentation is available at: https://phylaxsystems.github.io/credible-std -## Examples - -The Assertions Book examples live in `examples/assertions-book`. This directory -is the canonical source for the code snippets imported by -`phylaxsystems/phylax-docs`. - -| Directory | Purpose | -|----------|---------| -| `examples/assertions-book/assertions/src` | Assertion contracts used by the Assertions Book | -| `examples/assertions-book/src` | Mock protocols and helper contracts imported by assertion examples | - -Compile the Assertions Book example sources with: - -```bash -FOUNDRY_PROFILE=assertions-book forge build -``` - -Docs automation imports snippets from -`examples/assertions-book/assertions/src`; update examples here before updating -the docs pages that reference them. - -After example changes merge, run the `Import Credible Std Assertion Examples` -workflow in `phylaxsystems/phylax-docs` to refresh the rendered snippets. - ## Installation ### Using Foundry (Recommended) diff --git a/examples/assertions-book/README.md b/examples/assertions-book/README.md deleted file mode 100644 index c7792d8..0000000 --- a/examples/assertions-book/README.md +++ /dev/null @@ -1,19 +0,0 @@ -# Assertions Book Examples - -This directory is the canonical source for Assertions Book code examples. - -| Directory | Contents | -| --------- | -------- | -| `assertions/src` | Assertion contracts imported into `phylax-docs/snippets` | -| `src` | Mock protocols and helper contracts used by those assertions | -| `test` | Reserved for focused example tests | - -Before changing the docs snippets directly, update the matching Solidity file in -`assertions/src` and confirm the example profile still builds: - -```bash -FOUNDRY_PROFILE=assertions-book forge build -``` - -After the change lands, run the `Import Credible Std Assertion Examples` -workflow in `phylaxsystems/phylax-docs` to refresh the docs snippets. diff --git a/examples/assertions-book/assertions/src/ass1-implementation-change.a.sol b/examples/assertions-book/assertions/src/ass1-implementation-change.a.sol deleted file mode 100644 index 862c934..0000000 --- a/examples/assertions-book/assertions/src/ass1-implementation-change.a.sol +++ /dev/null @@ -1,34 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract ImplementationChangeAssertion is Assertion { - bytes32 internal constant IMPLEMENTATION_SLOT = bytes32(uint256(0)); - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerTxEndTrigger(this.implementationChange.selector); - } - - /// @notice Checks that the implementation slot is unchanged across the transaction. - function implementationChange() external view { - address adopter = ph.getAssertionAdopter(); - PhEvm.ForkId memory preFork = _preTx(); - PhEvm.ForkId memory postFork = _postTx(); - - address preImpl = _loadAddressAt(adopter, IMPLEMENTATION_SLOT, preFork); - address postImpl = _loadAddressAt(adopter, IMPLEMENTATION_SLOT, postFork); - - require(preImpl == postImpl, "Implementation changed"); - } - - function _loadAddressAt(address target, bytes32 slot, PhEvm.ForkId memory fork) internal view returns (address) { - return address(uint160(uint256(ph.loadStateAt(target, slot, fork)))); - } -} diff --git a/examples/assertions-book/assertions/src/ass10-oracle-liveness.a.sol b/examples/assertions-book/assertions/src/ass10-oracle-liveness.a.sol deleted file mode 100644 index 430e65f..0000000 --- a/examples/assertions-book/assertions/src/ass10-oracle-liveness.a.sol +++ /dev/null @@ -1,46 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract OracleLivenessAssertion is Assertion { - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - // Maximum time window (in seconds) that oracle data can be considered fresh - // This is a constant that should be adjusted based on the protocol's requirements - uint256 public constant MAX_UPDATE_WINDOW = 10 minutes; - - function triggers() external view override { - // Register trigger for the swap function which relies on oracle data - registerFnCallTrigger(this.assertionOracleLiveness.selector, IDex.swap.selector); - } - - // Assert that the oracle has been updated within the specified time window - function assertionOracleLiveness() external { - // Get the assertion adopter address - IDex adopter = IDex(ph.getAssertionAdopter()); - - // Get the current state to check the oracle's last update time - PhEvm.ForkId memory postFork = _postTx(); - - // Check if the oracle has been updated within the maximum allowed window - uint256 lastUpdateTime = IOracle(adopter.oracle()).lastUpdated(); - uint256 currentTime = block.timestamp; - - // Verify the oracle data is fresh (updated within the time window) - require(currentTime - lastUpdateTime <= MAX_UPDATE_WINDOW, "Oracle not updated within the allowed time window"); - } -} - -interface IOracle { - function lastUpdated() external view returns (uint256); -} - -interface IDex { - function swap(address tokenIn, address tokenOut, uint256 amountIn) external returns (uint256); - function oracle() external view returns (IOracle); -} diff --git a/examples/assertions-book/assertions/src/ass11-twap-deviation.a.sol b/examples/assertions-book/assertions/src/ass11-twap-deviation.a.sol deleted file mode 100644 index 264b742..0000000 --- a/examples/assertions-book/assertions/src/ass11-twap-deviation.a.sol +++ /dev/null @@ -1,62 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract TwapDeviationAssertion is Assertion { - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - // Register trigger for changes to the current price - // We assume that the price is stored in storage slot 0 - registerTxEndTrigger(this.assertionTwapDeviation.selector); - } - - // Assert that the current price doesn't deviate more than 5% from the TWAP price - function assertionTwapDeviation() external { - // Get the assertion adopter address - IPool adopter = IPool(ph.getAssertionAdopter()); - - // Get TWAP price before the transaction (our reference point) - PhEvm.ForkId memory preFork = _preTx(); - uint256 preTwapPrice = adopter.twap(); - - // Get price after the transaction - PhEvm.ForkId memory postFork = _postTx(); - uint256 postPrice = adopter.price(); - - uint256 maxDeviation = 5; - - // First check: Compare post-transaction price against pre-transaction TWAP - uint256 deviation = calculateDeviation(preTwapPrice, postPrice); - require(deviation <= maxDeviation, "Price deviation from TWAP exceeds maximum allowed"); - - // Second check: If the simple check passes, inspect all price changes in the callstack - // This is more expensive but catches manipulation attempts within the transaction - uint256[] memory priceChanges = getStateChangesUint( - address(adopter), - bytes32(uint256(0)) // Current price storage slot - ); - - // Check each price change against the pre-transaction TWAP - for (uint256 i = 0; i < priceChanges.length; i++) { - deviation = calculateDeviation(preTwapPrice, priceChanges[i]); - require(deviation <= maxDeviation, "Price deviation from TWAP exceeds maximum allowed"); - } - } - - // Helper function to calculate percentage deviation - function calculateDeviation(uint256 referencePrice, uint256 currentPrice) internal pure returns (uint256) { - return (((currentPrice > referencePrice) ? currentPrice - referencePrice : referencePrice - currentPrice) * 100) - / referencePrice; - } -} - -interface IPool { - function price() external view returns (uint256); - function twap() external view returns (uint256); -} diff --git a/examples/assertions-book/assertions/src/ass12-erc4626-assets-shares.a.sol b/examples/assertions-book/assertions/src/ass12-erc4626-assets-shares.a.sol deleted file mode 100644 index d15c3fc..0000000 --- a/examples/assertions-book/assertions/src/ass12-erc4626-assets-shares.a.sol +++ /dev/null @@ -1,30 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract ERC4626AssetsSharesAssertion is Assertion { - bytes32 internal constant TOTAL_ASSETS_SLOT = bytes32(uint256(0)); - bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(1)); - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerTxEndTrigger(this.assertionAssetsShares.selector); - } - - /// @notice Checks that stored total assets are sufficient to back stored total shares. - function assertionAssetsShares() external view { - address vault = ph.getAssertionAdopter(); - PhEvm.ForkId memory postFork = _postTx(); - - uint256 totalAssets = uint256(ph.loadStateAt(vault, TOTAL_ASSETS_SLOT, postFork)); - uint256 totalSupply = uint256(ph.loadStateAt(vault, TOTAL_SUPPLY_SLOT, postFork)); - - require(totalAssets >= totalSupply, "Not enough assets to back all shares"); - } -} diff --git a/examples/assertions-book/assertions/src/ass13-erc4626-deposit-withdraw.a.sol b/examples/assertions-book/assertions/src/ass13-erc4626-deposit-withdraw.a.sol deleted file mode 100644 index eb9fdb7..0000000 --- a/examples/assertions-book/assertions/src/ass13-erc4626-deposit-withdraw.a.sol +++ /dev/null @@ -1,54 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract ERC4626DepositWithdrawAssertion is Assertion { - bytes32 internal constant TOTAL_ASSETS_SLOT = bytes32(uint256(0)); - bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(1)); - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerFnCallTrigger(this.assertDepositPreservesSharePrice.selector, IERC4626.deposit.selector); - registerFnCallTrigger(this.assertWithdrawPreservesSharePrice.selector, IERC4626.withdraw.selector); - } - - /// @notice Checks that a deposit does not dilute existing shares. - function assertDepositPreservesSharePrice() external view { - PhEvm.TriggerContext memory ctx = ph.context(); - _assertSharePriceNotReduced(ctx.callStart, ctx.callEnd, "ERC4626: deposit diluted shares"); - } - - /// @notice Checks that a withdrawal does not dilute remaining shares. - function assertWithdrawPreservesSharePrice() external view { - PhEvm.TriggerContext memory ctx = ph.context(); - _assertSharePriceNotReduced(ctx.callStart, ctx.callEnd, "ERC4626: withdrawal diluted shares"); - } - - function _assertSharePriceNotReduced(uint256 callStart, uint256 callEnd, string memory reason) internal view { - address vault = ph.getAssertionAdopter(); - PhEvm.ForkId memory preCall = PhEvm.ForkId({forkType: 2, callIndex: callStart}); - PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: callEnd}); - - uint256 preAssets = uint256(ph.loadStateAt(vault, TOTAL_ASSETS_SLOT, preCall)); - uint256 preSupply = uint256(ph.loadStateAt(vault, TOTAL_SUPPLY_SLOT, preCall)); - uint256 postAssets = uint256(ph.loadStateAt(vault, TOTAL_ASSETS_SLOT, postCall)); - uint256 postSupply = uint256(ph.loadStateAt(vault, TOTAL_SUPPLY_SLOT, postCall)); - - if (preSupply == 0 || postSupply == 0) { - return; - } - - require(postAssets * preSupply >= preAssets * postSupply, reason); - } -} - -interface IERC4626 { - function deposit(uint256 assets, address receiver) external returns (uint256 shares); - function withdraw(uint256 assets, address receiver, address owner) external returns (uint256 shares); -} diff --git a/examples/assertions-book/assertions/src/ass14-fee-verification.a.sol b/examples/assertions-book/assertions/src/ass14-fee-verification.a.sol deleted file mode 100644 index 019dc44..0000000 --- a/examples/assertions-book/assertions/src/ass14-fee-verification.a.sol +++ /dev/null @@ -1,38 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract AmmFeeVerificationAssertion is Assertion { - bytes32 internal constant FEE_SLOT = bytes32(uint256(1)); - bytes32 internal constant STABLE_SLOT = bytes32(uint256(2)); - - uint256 private constant STABLE_POOL_FEE_1 = 1; - uint256 private constant STABLE_POOL_FEE_2 = 15; - uint256 private constant NON_STABLE_POOL_FEE_1 = 25; - uint256 private constant NON_STABLE_POOL_FEE_2 = 30; - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerTxEndTrigger(this.assertFeeVerification.selector); - } - - /// @notice Checks that the post-transaction fee is one of the allowed values. - function assertFeeVerification() external view { - address pool = ph.getAssertionAdopter(); - PhEvm.ForkId memory postFork = _postTx(); - - bool isStable = uint256(ph.loadStateAt(pool, STABLE_SLOT, postFork)) != 0; - uint256 newFee = uint256(ph.loadStateAt(pool, FEE_SLOT, postFork)); - bool isAllowed = isStable - ? (newFee == STABLE_POOL_FEE_1 || newFee == STABLE_POOL_FEE_2) - : (newFee == NON_STABLE_POOL_FEE_1 || newFee == NON_STABLE_POOL_FEE_2); - - require(isAllowed, "Fee change to unauthorized value"); - } -} diff --git a/examples/assertions-book/assertions/src/ass15-price-within-ticks.a.sol b/examples/assertions-book/assertions/src/ass15-price-within-ticks.a.sol deleted file mode 100644 index b508834..0000000 --- a/examples/assertions-book/assertions/src/ass15-price-within-ticks.a.sol +++ /dev/null @@ -1,56 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract PriceWithinTicksAssertion is Assertion { - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - // Uniswap V3 tick bounds - int24 constant MIN_TICK = -887272; - int24 constant MAX_TICK = 887272; - - function triggers() external view override { - // Register trigger for changes to the tick storage slot - // Assumes tick is stored in slot0 of the pool contract - registerTxEndTrigger(this.priceWithinTicks.selector); - } - - // Check that the price is within the tick bounds and that the tick is divisible by the tick spacing - function priceWithinTicks() external { - // Get the assertion adopter address - IUniswapV3Pool adopter = IUniswapV3Pool(ph.getAssertionAdopter()); - - // Get post-swap state - PhEvm.ForkId memory postFork = _postTx(); - (, int24 postTick,,,,,) = adopter.slot0(); - int24 spacing = adopter.tickSpacing(); - - // Check 1: Tick must be within global bounds - require(postTick >= MIN_TICK && postTick <= MAX_TICK, "Tick outside global bounds"); - - // Check 2: Tick must be divisible by tickSpacing - require(postTick % spacing == 0, "Tick not aligned with spacing"); - } -} - -// Uniswap v3 pool style interface -interface IUniswapV3Pool { - function slot0() - external - view - returns ( - uint160 sqrtPriceX96, - int24 tick, - uint16 observationIndex, - uint16 observationCardinality, - uint16 observationCardinalityNext, - uint8 feeProtocol, - bool unlocked - ); - function tickSpacing() external view returns (int24); -} diff --git a/examples/assertions-book/assertions/src/ass16-liquidation-health-factor.a.sol b/examples/assertions-book/assertions/src/ass16-liquidation-health-factor.a.sol deleted file mode 100644 index 8a7591d..0000000 --- a/examples/assertions-book/assertions/src/ass16-liquidation-health-factor.a.sol +++ /dev/null @@ -1,69 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract LiquidationHealthFactorAssertion is Assertion { - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - // Simple health factor constants (no scaling) - uint256 constant LIQUIDATION_THRESHOLD = 100; // Below this = liquidatable - uint256 constant MIN_HEALTH_FACTOR = 120; // Minimum safe health factor after liquidation - - function triggers() external view override { - // Register trigger for liquidation function calls - registerFnCallTrigger(this.assertHealthFactor.selector, ILendingProtocol.liquidate.selector); - } - - // Check that liquidation can't happen if the position is healthy - // Check that the health factor is improved after liquidation - function assertHealthFactor() external { - // Get the assertion adopter address - ILendingProtocol adopter = ILendingProtocol(ph.getAssertionAdopter()); - - // Get all liquidation calls in the transaction - PhEvm.CallInputs[] memory callInputs = ph.getAllCallInputs(address(adopter), adopter.liquidate.selector); - - for (uint256 i = 0; i < callInputs.length; i++) { - address borrower; - uint256 seizedAssets; - uint256 repaidDebt; - - // Decode liquidation parameters - (borrower, seizedAssets, repaidDebt) = abi.decode(callInputs[i].input, (address, uint256, uint256)); - - // Validate liquidation amounts - require(seizedAssets > 0, "Zero assets seized"); - require(repaidDebt > 0, "Zero debt repaid"); - - // Check health factor before liquidation - PhEvm.ForkId memory preCallFork = PhEvm.ForkId({forkType: 2, callIndex: callInputs[i].id}); - uint256 preHealthFactor = adopter.healthFactor(borrower); - require(preHealthFactor <= LIQUIDATION_THRESHOLD, "Account not eligible for liquidation"); - - // Check health factor after liquidation - PhEvm.ForkId memory postCallFork = PhEvm.ForkId({forkType: 3, callIndex: callInputs[i].id}); - uint256 postHealthFactor = adopter.healthFactor(borrower); - - // Verify the liquidation actually improved the position's health - require(postHealthFactor > preHealthFactor, "Health factor did not improve after liquidation"); - - // Ensure the position is now in a safe state above the minimum required health factor - require(postHealthFactor >= MIN_HEALTH_FACTOR, "Position still unhealthy after liquidation"); - } - } -} - -// Simplified lending protocol interface -interface ILendingProtocol { - function liquidate(address borrower, uint256 seizedAssets, uint256 repaidDebt) - external - returns (uint256, uint256); - - function isHealthy(address user) external view returns (bool); - function healthFactor(address user) external view returns (uint256); -} diff --git a/examples/assertions-book/assertions/src/ass17-panic-state-verificatoin.a.sol b/examples/assertions-book/assertions/src/ass17-panic-state-verificatoin.a.sol deleted file mode 100644 index f63174b..0000000 --- a/examples/assertions-book/assertions/src/ass17-panic-state-verificatoin.a.sol +++ /dev/null @@ -1,36 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract EmergencyStateAssertion is Assertion { - bytes32 internal constant PAUSED_SLOT = bytes32(uint256(0)); - bytes32 internal constant BALANCE_SLOT = bytes32(uint256(1)); - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerTxEndTrigger(this.assertionPanickedCanOnlyDecreaseBalance.selector); - } - - /// @notice Checks that a paused protocol cannot increase its stored balance. - function assertionPanickedCanOnlyDecreaseBalance() external view { - address adopter = ph.getAssertionAdopter(); - PhEvm.ForkId memory preFork = _preTx(); - PhEvm.ForkId memory postFork = _postTx(); - - bool wasPaused = uint256(ph.loadStateAt(adopter, PAUSED_SLOT, preFork)) != 0; - if (!wasPaused) { - return; - } - - uint256 preBalance = uint256(ph.loadStateAt(adopter, BALANCE_SLOT, preFork)); - uint256 postBalance = uint256(ph.loadStateAt(adopter, BALANCE_SLOT, postFork)); - - require(postBalance <= preBalance, "Balance can only decrease when panicked"); - } -} diff --git a/examples/assertions-book/assertions/src/ass18-harvest-increases-balance.a.sol b/examples/assertions-book/assertions/src/ass18-harvest-increases-balance.a.sol deleted file mode 100644 index fc3ddbf..0000000 --- a/examples/assertions-book/assertions/src/ass18-harvest-increases-balance.a.sol +++ /dev/null @@ -1,39 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract BeefyHarvestAssertion is Assertion { - bytes32 internal constant BALANCE_SLOT = bytes32(uint256(0)); - bytes32 internal constant PRICE_PER_SHARE_SLOT = bytes32(uint256(1)); - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerFnCallTrigger(this.assertionHarvestIncreasesBalance.selector, IBeefyVault.harvest.selector); - } - - /// @notice Checks that a harvest does not reduce vault balance or price per share. - function assertionHarvestIncreasesBalance() external view { - address vault = ph.getAssertionAdopter(); - PhEvm.TriggerContext memory ctx = ph.context(); - PhEvm.ForkId memory preCall = PhEvm.ForkId({forkType: 2, callIndex: ctx.callStart}); - PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd}); - - uint256 preBalance = uint256(ph.loadStateAt(vault, BALANCE_SLOT, preCall)); - uint256 postBalance = uint256(ph.loadStateAt(vault, BALANCE_SLOT, postCall)); - uint256 prePricePerShare = uint256(ph.loadStateAt(vault, PRICE_PER_SHARE_SLOT, preCall)); - uint256 postPricePerShare = uint256(ph.loadStateAt(vault, PRICE_PER_SHARE_SLOT, postCall)); - - require(postBalance >= preBalance, "Harvest decreased balance"); - require(postPricePerShare >= prePricePerShare, "Price per share decreased after harvest"); - } -} - -interface IBeefyVault { - function harvest(bool badHarvest) external; -} diff --git a/examples/assertions-book/assertions/src/ass19-tokens-borrowed-invariant.a.sol b/examples/assertions-book/assertions/src/ass19-tokens-borrowed-invariant.a.sol deleted file mode 100644 index f28f497..0000000 --- a/examples/assertions-book/assertions/src/ass19-tokens-borrowed-invariant.a.sol +++ /dev/null @@ -1,33 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract TokensBorrowedInvariant is Assertion { - bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(0)); - bytes32 internal constant TOTAL_BORROW_SLOT = bytes32(uint256(1)); - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerTxEndTrigger(this.assertBorrowedInvariant.selector); - } - - /// @notice Checks that total supplied assets cover total borrowed assets after the transaction. - function assertBorrowedInvariant() external view { - address market = ph.getAssertionAdopter(); - PhEvm.ForkId memory postFork = _postTx(); - - uint256 totalSupplyAsset = uint256(ph.loadStateAt(market, TOTAL_SUPPLY_SLOT, postFork)); - uint256 totalBorrowedAsset = uint256(ph.loadStateAt(market, TOTAL_BORROW_SLOT, postFork)); - - require( - totalSupplyAsset >= totalBorrowedAsset, - "INVARIANT VIOLATION: Total supply of assets is less than total borrowed assets" - ); - } -} diff --git a/examples/assertions-book/assertions/src/ass2-erc4626-operations.a.sol b/examples/assertions-book/assertions/src/ass2-erc4626-operations.a.sol deleted file mode 100644 index f9934fa..0000000 --- a/examples/assertions-book/assertions/src/ass2-erc4626-operations.a.sol +++ /dev/null @@ -1,209 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title ERC4626OperationsAssertion - * @notice This assertion contract validates the correctness of ERC4626 vault operations by checking: - * - * 1. Batch Operations Consistency: - * - Validates that all ERC4626 operations (deposit, mint, withdraw, redeem) maintain correct - * accounting of total assets and total supply - * - Ensures that the net changes in assets and shares match the expected changes - * - Handles multiple operations in a single transaction - * - * 2. Deposit Operation Validation: - * - Verifies that deposit operations correctly increase the vault's asset balance - * - Ensures depositors receive the correct number of shares based on previewDeposit - * - Validates that the vault's total assets increase by exactly the deposited amount - * - * 3. Base Invariants: - * - Ensures the vault always has at least as many assets as shares - * - Validates this invariant after any storage changes - * - * The contract uses the Credible Layer's fork mechanism to compare pre and post-state - * changes, ensuring that all operations maintain the vault's accounting integrity. - */ -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {CoolVault} from "../../src/ass2-erc4626-operations.sol"; -import {IERC4626} from "openzeppelin-contracts/interfaces/IERC4626.sol"; -import {IERC20} from "openzeppelin-contracts/token/ERC20/IERC20.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract ERC4626OperationsAssertion is Assertion { - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - // The triggers function tells the Credible Layer which assertion functions to run - function triggers() external view override { - // Batch operations assertion - triggers on any of the four functions - registerFnCallTrigger(this.assertionBatchOperationsConsistency.selector, CoolVault.deposit.selector); - registerFnCallTrigger(this.assertionBatchOperationsConsistency.selector, CoolVault.mint.selector); - registerFnCallTrigger(this.assertionBatchOperationsConsistency.selector, CoolVault.withdraw.selector); - registerFnCallTrigger(this.assertionBatchOperationsConsistency.selector, CoolVault.redeem.selector); - - // Deposit-specific assertions - registerFnCallTrigger(this.assertionDepositIncreasesBalance.selector, CoolVault.deposit.selector); - registerFnCallTrigger(this.assertionDepositerSharesIncreases.selector, CoolVault.deposit.selector); - - // Base invariant assertion - triggers on storage changes - registerTxEndTrigger(this.assertionVaultAlwaysAccumulatesAssets.selector); - } - - /** - * @dev Comprehensive assertion for batch operations: validates that all ERC4626 operations - * in a single transaction maintain consistency across total supply and total assets - * This function checks all four operations (deposit, mint, withdraw, redeem) that may occur - * within the same transaction and ensures the final state is mathematically correct - */ - function assertionBatchOperationsConsistency() external { - // Get the assertion adopter address - CoolVault adopter = CoolVault(ph.getAssertionAdopter()); - - // Get call inputs for all four functions - PhEvm.CallInputs[] memory depositInputs = ph.getCallInputs(address(adopter), adopter.deposit.selector); - PhEvm.CallInputs[] memory mintInputs = ph.getCallInputs(address(adopter), adopter.mint.selector); - PhEvm.CallInputs[] memory withdrawInputs = ph.getCallInputs(address(adopter), adopter.withdraw.selector); - PhEvm.CallInputs[] memory redeemInputs = ph.getCallInputs(address(adopter), adopter.redeem.selector); - - // Calculate net changes from all operations - uint256 totalAssetsAdded = 0; - uint256 totalAssetsRemoved = 0; - uint256 totalSharesAdded = 0; - uint256 totalSharesRemoved = 0; - - // Process deposit operations (increase assets and supply) - for (uint256 i = 0; i < depositInputs.length; i++) { - (uint256 assets,) = abi.decode(depositInputs[i].input, (uint256, address)); - totalAssetsAdded += assets; - totalSharesAdded += adopter.previewDeposit(assets); - } - - // Process mint operations (increase assets and supply) - for (uint256 i = 0; i < mintInputs.length; i++) { - (uint256 shares,) = abi.decode(mintInputs[i].input, (uint256, address)); - totalSharesAdded += shares; - totalAssetsAdded += adopter.previewMint(shares); - } - - // Process withdraw operations (decrease assets and supply) - for (uint256 i = 0; i < withdrawInputs.length; i++) { - (uint256 assets,,) = abi.decode(withdrawInputs[i].input, (uint256, address, address)); - totalAssetsRemoved += assets; - totalSharesRemoved += adopter.previewWithdraw(assets); - } - - // Process redeem operations (decrease assets and supply) - for (uint256 i = 0; i < redeemInputs.length; i++) { - (uint256 shares,,) = abi.decode(redeemInputs[i].input, (uint256, address, address)); - totalSharesRemoved += shares; - totalAssetsRemoved += adopter.previewRedeem(shares); - } - - PhEvm.ForkId memory preFork = _preTx(); - uint256 preVaultAssets = adopter.totalAssets(); - uint256 preVaultSupply = adopter.totalSupply(); - - PhEvm.ForkId memory postFork = _postTx(); - uint256 postVaultAssets = adopter.totalAssets(); - uint256 postVaultSupply = adopter.totalSupply(); - - // Calculate expected changes - uint256 expectedAssetsAdded = postVaultAssets > preVaultAssets ? postVaultAssets - preVaultAssets : 0; - uint256 expectedAssetsRemoved = preVaultAssets > postVaultAssets ? preVaultAssets - postVaultAssets : 0; - uint256 expectedSharesAdded = postVaultSupply > preVaultSupply ? postVaultSupply - preVaultSupply : 0; - uint256 expectedSharesRemoved = preVaultSupply > postVaultSupply ? preVaultSupply - postVaultSupply : 0; - - // Ensure operations had some effect if there were calls - require(totalAssetsAdded == expectedAssetsAdded, "Batch Operations: Assets added mismatch"); - require(totalAssetsRemoved == expectedAssetsRemoved, "Batch Operations: Assets removed mismatch"); - require(totalSharesAdded == expectedSharesAdded, "Batch Operations: Shares added mismatch"); - require(totalSharesRemoved == expectedSharesRemoved, "Batch Operations: Shares removed mismatch"); - } - - /** - * @dev Assertion to verify that deposit operations correctly increase the vault's asset balance - * This ensures that when users deposit assets, the vault's total assets increase by exactly the deposited amount - */ - function assertionDepositIncreasesBalance() external { - // Get the assertion adopter address - CoolVault adopter = CoolVault(ph.getAssertionAdopter()); - - // Get all deposit calls to the vault - PhEvm.CallInputs[] memory inputs = ph.getCallInputs(address(adopter), adopter.deposit.selector); - - for (uint256 i = 0; i < inputs.length; i++) { - (uint256 assets, address receiver) = abi.decode(inputs[i].input, (uint256, address)); - - // Check pre-state - PhEvm.ForkId memory preFork = _preTx(); - uint256 vaultAssetPreBalance = adopter.totalAssets(); - uint256 userSharesPreBalance = adopter.balanceOf(receiver); - uint256 expectedShares = adopter.previewDeposit(assets); - - // Check post-state - PhEvm.ForkId memory postFork = _postTx(); - uint256 vaultAssetPostBalance = adopter.totalAssets(); - uint256 userSharesPostBalance = adopter.balanceOf(receiver); - - // Verify vault assets increased by exactly the deposited amount - require( - vaultAssetPostBalance == vaultAssetPreBalance + assets, - "Deposit assertion failed: Vault assets did not increase by the correct amount" - ); - - // Verify user received exactly the expected number of shares - require( - userSharesPostBalance == userSharesPreBalance + expectedShares, - "Deposit assertion failed: User did not receive the correct number of shares" - ); - } - } - - /** - * @dev Assertion to verify that deposit operations correctly increase the depositor's share balance - * This ensures that when users deposit assets, they receive the correct number of shares - */ - function assertionDepositerSharesIncreases() external { - // Get the assertion adopter address - CoolVault adopter = CoolVault(ph.getAssertionAdopter()); - - PhEvm.CallInputs[] memory inputs = ph.getCallInputs(address(adopter), adopter.deposit.selector); - - for (uint256 i = 0; i < inputs.length; i++) { - PhEvm.ForkId memory preFork = _preTx(); - (uint256 assets,) = abi.decode(inputs[i].input, (uint256, address)); - uint256 previewPreAssets = adopter.previewDeposit(assets); - address depositer = inputs[0].caller; - uint256 preShares = adopter.balanceOf(depositer); - - PhEvm.ForkId memory postFork = _postTx(); - - uint256 postShares = adopter.balanceOf(depositer); - - require( - postShares == preShares + previewPreAssets, - "Depositer shares assertion failed: Share balance did not increase correctly" - ); - } - } - - /** - * @dev Base invariant assertion to verify that the vault always has at least as many assets as shares - * This is a fundamental invariant of ERC4626 vaults - they should never have more shares than assets - */ - function assertionVaultAlwaysAccumulatesAssets() external { - // Get the assertion adopter address - CoolVault adopter = CoolVault(ph.getAssertionAdopter()); - - PhEvm.ForkId memory postFork = _postTx(); - - uint256 vaultAssetPostBalance = adopter.totalAssets(); - uint256 vaultSharesPostBalance = adopter.balanceOf(address(adopter)); - - require( - vaultAssetPostBalance >= vaultSharesPostBalance, "Base invariant failed: Vault has more shares than assets" - ); - } -} diff --git a/examples/assertions-book/assertions/src/ass20-erc20-drain.a.sol b/examples/assertions-book/assertions/src/ass20-erc20-drain.a.sol deleted file mode 100644 index 98c9a38..0000000 --- a/examples/assertions-book/assertions/src/ass20-erc20-drain.a.sol +++ /dev/null @@ -1,38 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract ERC20CumulativeOutflowBreakerAssertion is Assertion { - address public immutable monitoredToken; - uint256 public immutable outflowThresholdBps; - uint256 public immutable outflowWindowDuration; - - constructor(address monitoredToken_, uint256 outflowThresholdBps_, uint256 outflowWindowDuration_) { - registerAssertionSpec(AssertionSpec.Reshiram); - - monitoredToken = monitoredToken_; - outflowThresholdBps = outflowThresholdBps_; - outflowWindowDuration = outflowWindowDuration_; - } - - function triggers() external view override { - watchCumulativeOutflow( - monitoredToken, - outflowThresholdBps, - outflowWindowDuration, - this.assertCumulativeOutflow.selector - ); - } - - /// @notice Reverts when cumulative token outflow breaches the rolling-window limit. - /// @dev The Reshiram trigger tracks the window and calls this function only after breach. - function assertCumulativeOutflow() external view { - PhEvm.OutflowContext memory ctx = ph.outflowContext(); - require(ctx.token == monitoredToken, "ERC20Outflow: wrong token context"); - - revert("ERC20Outflow: cumulative outflow breaker tripped"); - } -} diff --git a/examples/assertions-book/assertions/src/ass21-ether-drain.a.sol b/examples/assertions-book/assertions/src/ass21-ether-drain.a.sol deleted file mode 100644 index fe0015f..0000000 --- a/examples/assertions-book/assertions/src/ass21-ether-drain.a.sol +++ /dev/null @@ -1,54 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract EtherDrainAssertion is Assertion { - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - // Maximum percentage of ETH that can be drained in a single transaction (10% by default) - uint256 public constant MAX_DRAIN_PERCENTAGE = 10; - - function triggers() external view override { - // Register a trigger that activates when the ETH balance of the monitored contract changes - registerTxEndTrigger(this.assertionEtherDrain.selector); - } - - // Combined assertion for ETH drain with whitelist logic - function assertionEtherDrain() external { - // Get the assertion adopter address (this is the contract we're monitoring) - address exampleContract = ph.getAssertionAdopter(); - - // Capture the ETH balance before transaction execution - PhEvm.ForkId memory preFork = _preTx(); - uint256 preBalance = address(exampleContract).balance; - - // Capture the ETH balance after transaction execution - PhEvm.ForkId memory postFork = _postTx(); - uint256 postBalance = address(exampleContract).balance; - - // Only check for drainage (we don't care about ETH being added) - if (preBalance > postBalance) { - // Calculate the amount drained and the maximum allowed drain - uint256 drainAmount = preBalance - postBalance; - uint256 maxAllowedDrain = (preBalance * MAX_DRAIN_PERCENTAGE) / 100; - - // If drain amount is within allowed limit, allow the transaction - if (drainAmount <= maxAllowedDrain) { - return; // Small drain, no need to check whitelist - } - - // For large drains, we would need to check whitelist - // Since we can't easily access constructor parameters in the new interface, - // we'll use a simplified approach that just checks the drain percentage - // In a real implementation, this would be more sophisticated - revert("Large ETH drain detected - exceeds allowed percentage"); - } - } -} - -interface IExampleContract {} diff --git a/examples/assertions-book/assertions/src/ass22-erc20-inflow-breaker.a.sol b/examples/assertions-book/assertions/src/ass22-erc20-inflow-breaker.a.sol deleted file mode 100644 index a8a4b30..0000000 --- a/examples/assertions-book/assertions/src/ass22-erc20-inflow-breaker.a.sol +++ /dev/null @@ -1,38 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract ERC20CumulativeInflowBreakerAssertion is Assertion { - address public immutable monitoredToken; - uint256 public immutable inflowThresholdBps; - uint256 public immutable inflowWindowDuration; - - constructor(address monitoredToken_, uint256 inflowThresholdBps_, uint256 inflowWindowDuration_) { - registerAssertionSpec(AssertionSpec.Reshiram); - - monitoredToken = monitoredToken_; - inflowThresholdBps = inflowThresholdBps_; - inflowWindowDuration = inflowWindowDuration_; - } - - function triggers() external view override { - watchCumulativeInflow( - monitoredToken, - inflowThresholdBps, - inflowWindowDuration, - this.assertCumulativeInflow.selector - ); - } - - /// @notice Reverts when cumulative token inflow breaches the rolling-window limit. - /// @dev The Reshiram trigger tracks the window and calls this function only after breach. - function assertCumulativeInflow() external view { - PhEvm.InflowContext memory ctx = ph.inflowContext(); - require(ctx.token == monitoredToken, "ERC20Inflow: wrong token context"); - - revert("ERC20Inflow: cumulative inflow breaker tripped"); - } -} diff --git a/examples/assertions-book/assertions/src/ass28-intra-tx-oracle-deviation.a.sol b/examples/assertions-book/assertions/src/ass28-intra-tx-oracle-deviation.a.sol deleted file mode 100644 index 3bc0545..0000000 --- a/examples/assertions-book/assertions/src/ass28-intra-tx-oracle-deviation.a.sol +++ /dev/null @@ -1,68 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract IntraTxOracleDeviationAssertion is Assertion { - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - // Maximum allowed price deviation (10% by default) - uint256 public constant MAX_DEVIATION_PERCENTAGE = 10; - - function triggers() external view override { - // Register trigger for oracle price update calls - registerFnCallTrigger(this.assertOracleDeviation.selector, IOracle.updatePrice.selector); - } - - // Check that price updates don't deviate more than the allowed percentage - // from the initial price at any point during the transaction - function assertOracleDeviation() external { - // Get the assertion adopter address - IOracle adopter = IOracle(ph.getAssertionAdopter()); - - // Start with a simple check comparing pre and post state - PhEvm.ForkId memory preFork = _preTx(); - uint256 prePrice = adopter.price(); - - // Calculate allowed deviation thresholds (10% by default) - uint256 maxAllowedPrice = (prePrice * (100 + MAX_DEVIATION_PERCENTAGE)) / 100; - uint256 minAllowedPrice = (prePrice * (100 - MAX_DEVIATION_PERCENTAGE)) / 100; - - // First check post-state price - PhEvm.ForkId memory postFork = _postTx(); - uint256 postPrice = adopter.price(); - - // Verify post-state price is within allowed deviation from initial price - require( - postPrice >= minAllowedPrice && postPrice <= maxAllowedPrice, - "Oracle post-state price deviation exceeds threshold" - ); - - // Get all price update calls in this transaction - // Since this assertion is triggered by updatePrice calls, we know there's at least one - PhEvm.CallInputs[] memory priceUpdates = ph.getCallInputs(address(adopter), adopter.updatePrice.selector); - - // Check each price update to ensure none deviate more than allowed from initial price - for (uint256 i = 0; i < priceUpdates.length; i++) { - PhEvm.ForkId memory postCallFork = PhEvm.ForkId({forkType: 3, callIndex: priceUpdates[i].id}); - - // Call the price function at the given frame in the call stack - uint256 updatedPrice = adopter.price(); - - // Verify each update is within allowed deviation from initial pre-state price - require( - updatedPrice >= minAllowedPrice && updatedPrice <= maxAllowedPrice, - "Oracle intra-tx price deviation exceeds threshold" - ); - } - } -} - -interface IOracle { - function updatePrice(uint256 price) external; - function price() external view returns (uint256); -} diff --git a/examples/assertions-book/assertions/src/ass4-kyc-whitelist.a.sol b/examples/assertions-book/assertions/src/ass4-kyc-whitelist.a.sol deleted file mode 100644 index f0ce918..0000000 --- a/examples/assertions-book/assertions/src/ass4-kyc-whitelist.a.sol +++ /dev/null @@ -1,44 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; -import {OnlyAccreditedCanMint} from "../../src/ass4-only-accredited-can-mint.sol"; -import {AccreditedInvestorRegistry} from "../../src/AccreditedInvestorRegistry.sol"; - -contract OnlyAccreditedCanMintAssertion is Assertion { - AccreditedInvestorRegistry public immutable registry; - - constructor(address registry_) { - registerAssertionSpec(AssertionSpec.Reshiram); - registry = AccreditedInvestorRegistry(registry_); - } - - function triggers() external view override { - registerFnCallTrigger(this.assertOnlyAccreditedMint.selector, OnlyAccreditedCanMint.mint.selector); - registerFnCallTrigger(this.assertOnlyAccreditedTransfer.selector, OnlyAccreditedCanMint.transfer.selector); - } - - /// @notice Checks that the caller of `mint` is accredited. - function assertOnlyAccreditedMint() external view { - _assertMatchingCallersAccredited(OnlyAccreditedCanMint.mint.selector); - } - - /// @notice Checks that the caller of `transfer` is accredited. - function assertOnlyAccreditedTransfer() external view { - _assertMatchingCallersAccredited(OnlyAccreditedCanMint.transfer.selector); - } - - function _assertMatchingCallersAccredited(bytes4 selector) internal view { - PhEvm.TriggerCall[] memory calls = ph.matchingCalls(ph.getAssertionAdopter(), selector, _successfulCalls(), 32); - for (uint256 i = 0; i < calls.length; i++) { - require(registry.isAccredited(calls[i].caller), "caller is not accredited"); - } - } - - function _successfulCalls() internal pure returns (PhEvm.CallFilter memory filter) { - filter.callType = 1; - filter.successOnly = true; - } -} diff --git a/examples/assertions-book/assertions/src/ass5-owner-change.a.sol b/examples/assertions-book/assertions/src/ass5-owner-change.a.sol deleted file mode 100644 index a7d92b2..0000000 --- a/examples/assertions-book/assertions/src/ass5-owner-change.a.sol +++ /dev/null @@ -1,48 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract OwnerChangeAssertion is Assertion { - bytes32 internal constant OWNER_SLOT = bytes32(uint256(0)); - bytes32 internal constant ADMIN_SLOT = bytes32(uint256(1)); - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerTxEndTrigger(this.assertionOwnerChange.selector); - registerTxEndTrigger(this.assertionAdminChange.selector); - } - - /// @notice Checks that the owner slot is unchanged across the transaction. - function assertionOwnerChange() external view { - address adopter = ph.getAssertionAdopter(); - PhEvm.ForkId memory preFork = _preTx(); - PhEvm.ForkId memory postFork = _postTx(); - - address preOwner = _loadAddressAt(adopter, OWNER_SLOT, preFork); - address postOwner = _loadAddressAt(adopter, OWNER_SLOT, postFork); - - require(preOwner == postOwner, "Owner changed"); - } - - /// @notice Checks that the admin slot is unchanged across the transaction. - function assertionAdminChange() external view { - address adopter = ph.getAssertionAdopter(); - PhEvm.ForkId memory preFork = _preTx(); - PhEvm.ForkId memory postFork = _postTx(); - - address preAdmin = _loadAddressAt(adopter, ADMIN_SLOT, preFork); - address postAdmin = _loadAddressAt(adopter, ADMIN_SLOT, postFork); - - require(preAdmin == postAdmin, "Admin changed"); - } - - function _loadAddressAt(address target, bytes32 slot, PhEvm.ForkId memory fork) internal view returns (address) { - return address(uint160(uint256(ph.loadStateAt(target, slot, fork)))); - } -} diff --git a/examples/assertions-book/assertions/src/ass6-constant-product.a.sol b/examples/assertions-book/assertions/src/ass6-constant-product.a.sol deleted file mode 100644 index 973a667..0000000 --- a/examples/assertions-book/assertions/src/ass6-constant-product.a.sol +++ /dev/null @@ -1,33 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract ConstantProductAssertion is Assertion { - bytes32 internal constant RESERVE0_SLOT = bytes32(uint256(0)); - bytes32 internal constant RESERVE1_SLOT = bytes32(uint256(1)); - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerTxEndTrigger(this.assertionConstantProduct.selector); - } - - /// @notice Checks that the pool's stored reserve product is not reduced by the transaction. - function assertionConstantProduct() external view { - address pool = ph.getAssertionAdopter(); - PhEvm.ForkId memory preFork = _preTx(); - PhEvm.ForkId memory postFork = _postTx(); - - uint256 reserve0Pre = uint256(ph.loadStateAt(pool, RESERVE0_SLOT, preFork)); - uint256 reserve1Pre = uint256(ph.loadStateAt(pool, RESERVE1_SLOT, preFork)); - uint256 reserve0Post = uint256(ph.loadStateAt(pool, RESERVE0_SLOT, postFork)); - uint256 reserve1Post = uint256(ph.loadStateAt(pool, RESERVE1_SLOT, postFork)); - - require(reserve0Post * reserve1Post >= reserve0Pre * reserve1Pre, "Constant product invariant reduced"); - } -} diff --git a/examples/assertions-book/assertions/src/ass7-lending-health-factor.a.sol b/examples/assertions-book/assertions/src/ass7-lending-health-factor.a.sol deleted file mode 100644 index 0bd24b1..0000000 --- a/examples/assertions-book/assertions/src/ass7-lending-health-factor.a.sol +++ /dev/null @@ -1,64 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract LendingHealthFactorAssertion is Assertion { - bytes32 internal constant HEALTH_FACTOR_SLOT = bytes32(uint256(0)); - uint256 internal constant MIN_HEALTH_FACTOR = 1e18; - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.supply.selector); - registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.borrow.selector); - registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.withdraw.selector); - registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.repay.selector); - } - - /// @notice Checks that the touched account remains healthy after a lending operation. - function assertionOperationSafety() external view { - PhEvm.TriggerContext memory ctx = ph.context(); - PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd}); - (uint256 marketId,) = abi.decode(_stripSelector(ph.callinputAt(ctx.callStart)), (uint256, uint256)); - address account = _matchingCaller(ctx.selector); - bytes32 healthSlot = _healthFactorSlot(marketId, account); - uint256 healthFactor = uint256(ph.loadStateAt(ph.getAssertionAdopter(), healthSlot, postCall)); - - require(healthFactor >= MIN_HEALTH_FACTOR, "Operation resulted in unhealthy position"); - } - - function _matchingCaller(bytes4 selector) internal view returns (address) { - PhEvm.TriggerCall[] memory calls = ph.matchingCalls(ph.getAssertionAdopter(), selector, _successfulCalls(), 1); - require(calls.length == 1, "missing triggered call"); - return calls[0].caller; - } - - function _successfulCalls() internal pure returns (PhEvm.CallFilter memory filter) { - filter.callType = 1; - filter.successOnly = true; - } - - function _healthFactorSlot(uint256 marketId, address account) internal pure returns (bytes32) { - return keccak256(abi.encode(account, keccak256(abi.encode(marketId, HEALTH_FACTOR_SLOT)))); - } - - function _stripSelector(bytes memory data) internal pure returns (bytes memory) { - bytes memory stripped = new bytes(data.length - 4); - for (uint256 i = 4; i < data.length; i++) { - stripped[i - 4] = data[i]; - } - return stripped; - } -} - -interface IMorpho { - function supply(uint256 marketId, uint256 amount) external; - function borrow(uint256 marketId, uint256 amount) external; - function withdraw(uint256 marketId, uint256 amount) external; - function repay(uint256 marketId, uint256 amount) external; -} diff --git a/examples/assertions-book/assertions/src/ass8-positions-sum.a.sol b/examples/assertions-book/assertions/src/ass8-positions-sum.a.sol deleted file mode 100644 index ab6f01c..0000000 --- a/examples/assertions-book/assertions/src/ass8-positions-sum.a.sol +++ /dev/null @@ -1,44 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract PositionSumAssertion is Assertion { - bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(0)); - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerFnCallTrigger(this.assertionPositionsSum.selector, ILending.deposit.selector); - } - - /// @notice Checks that a deposit call increases stored total supply by the deposited amount. - function assertionPositionsSum() external view { - address adopter = ph.getAssertionAdopter(); - PhEvm.TriggerContext memory ctx = ph.context(); - PhEvm.ForkId memory preCall = PhEvm.ForkId({forkType: 2, callIndex: ctx.callStart}); - PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd}); - - uint256 preTotalSupply = uint256(ph.loadStateAt(adopter, TOTAL_SUPPLY_SLOT, preCall)); - uint256 postTotalSupply = uint256(ph.loadStateAt(adopter, TOTAL_SUPPLY_SLOT, postCall)); - (, uint256 amount) = abi.decode(_stripSelector(ph.callinputAt(ctx.callStart)), (address, uint256)); - - require(postTotalSupply == preTotalSupply + amount, "Positions sum does not match total supply"); - } - - function _stripSelector(bytes memory data) internal pure returns (bytes memory) { - bytes memory stripped = new bytes(data.length - 4); - for (uint256 i = 4; i < data.length; i++) { - stripped[i - 4] = data[i]; - } - return stripped; - } -} - -interface ILending { - function deposit(address user, uint256 amount) external; -} diff --git a/examples/assertions-book/assertions/src/ass9-timelock-verification.a.sol b/examples/assertions-book/assertions/src/ass9-timelock-verification.a.sol deleted file mode 100644 index 2c0c9dd..0000000 --- a/examples/assertions-book/assertions/src/ass9-timelock-verification.a.sol +++ /dev/null @@ -1,38 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -import {Assertion} from "credible-std/Assertion.sol"; -import {AssertionSpec} from "credible-std/SpecRecorder.sol"; -import {PhEvm} from "credible-std/PhEvm.sol"; - -contract TimelockVerificationAssertion is Assertion { - bytes32 internal constant TIMELOCK_DELAY_SLOT = bytes32(uint256(0)); - bytes32 internal constant TIMELOCK_ACTIVE_SLOT = bytes32(uint256(1)); - - constructor() { - registerAssertionSpec(AssertionSpec.Reshiram); - } - - function triggers() external view override { - registerTxEndTrigger(this.assertionTimelock.selector); - } - - /// @notice Checks that an activated timelock uses a bounded delay. - function assertionTimelock() external view { - address adopter = ph.getAssertionAdopter(); - PhEvm.ForkId memory preFork = _preTx(); - PhEvm.ForkId memory postFork = _postTx(); - - bool preActive = uint256(ph.loadStateAt(adopter, TIMELOCK_ACTIVE_SLOT, preFork)) != 0; - if (preActive) { - return; - } - - bool postActive = uint256(ph.loadStateAt(adopter, TIMELOCK_ACTIVE_SLOT, postFork)) != 0; - if (postActive) { - uint256 delay = uint256(ph.loadStateAt(adopter, TIMELOCK_DELAY_SLOT, postFork)); - - require(delay >= 1 days && delay <= 2 weeks, "Timelock parameters invalid"); - } - } -} diff --git a/examples/assertions-book/src/AccreditedInvestorRegistry.sol b/examples/assertions-book/src/AccreditedInvestorRegistry.sol deleted file mode 100644 index e28060e..0000000 --- a/examples/assertions-book/src/AccreditedInvestorRegistry.sol +++ /dev/null @@ -1,10 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -contract AccreditedInvestorRegistry { - mapping(address => bool) public isAccredited; - - function setAccredited(address account, bool accredited) external { - isAccredited[account] = accredited; - } -} diff --git a/examples/assertions-book/src/MockToken.sol b/examples/assertions-book/src/MockToken.sol deleted file mode 100644 index 2aa74c8..0000000 --- a/examples/assertions-book/src/MockToken.sol +++ /dev/null @@ -1,39 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.0; - -import "@openzeppelin/contracts/token/ERC20/ERC20.sol"; - -/** - * @title MockToken - * @dev A simple ERC20 token for testing the vault functionality - */ -contract MockToken is ERC20 { - /** - * @dev Constructor that mints initial supply to the deployer - * @param _name The name of the token - * @param _symbol The symbol of the token - * @param _initialSupply The initial supply of tokens to mint - */ - constructor( - string memory _name, - string memory _symbol, - uint256 _initialSupply - ) ERC20(_name, _symbol) { - _mint(msg.sender, _initialSupply * 10 ** decimals()); - } - - /** - * @dev Public mint function for testing purposes - * In a real token, this would have access controls - */ - function mint(address to, uint256 amount) external { - _mint(to, amount); - } - - /** - * @dev Public burn function for testing purposes - */ - function burn(uint256 amount) external { - _burn(msg.sender, amount); - } -} diff --git a/examples/assertions-book/src/ass1-implementation-change.sol b/examples/assertions-book/src/ass1-implementation-change.sol deleted file mode 100644 index 5d2b581..0000000 --- a/examples/assertions-book/src/ass1-implementation-change.sol +++ /dev/null @@ -1,36 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Implementation Contract - * @notice This contract serves as an example implementation for testing the ImplementationChange assertion - * @dev Contains a storage variable for the implementation address and methods to get/set it - */ -contract Implementation { - // Storage slot 0: implementation address - address private _implementation; - - /** - * @notice Constructor that sets the initial implementation address - * @param initialImpl The initial implementation address - */ - constructor(address initialImpl) { - _implementation = initialImpl; - } - - /** - * @notice Returns the current implementation address - * @return The current implementation address - */ - function implementation() external view returns (address) { - return _implementation; - } - - /** - * @notice Updates the implementation address - * @param newImplementation The new implementation address - */ - function setImplementation(address newImplementation) external { - _implementation = newImplementation; - } -} diff --git a/examples/assertions-book/src/ass10-oracle-liveness.sol b/examples/assertions-book/src/ass10-oracle-liveness.sol deleted file mode 100644 index a6af5de..0000000 --- a/examples/assertions-book/src/ass10-oracle-liveness.sol +++ /dev/null @@ -1,66 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Oracle Contract - * @notice This contract tracks the last update time of oracle data - * @dev Implements the IOracle interface for testing the OracleLivenessAssertion - */ -contract Oracle { - // Storage slot 0: last update timestamp - uint256 private _lastUpdated; - - /** - * @notice Constructor that sets the initial last update time - * @param initialLastUpdated The initial last update timestamp - */ - constructor(uint256 initialLastUpdated) { - _lastUpdated = initialLastUpdated; - } - - /** - * @notice Returns the last update timestamp - * @return The last update timestamp - */ - function lastUpdated() external view returns (uint256) { - return _lastUpdated; - } - - /** - * @notice Sets the last update timestamp - * @param newLastUpdated The new last update timestamp - */ - function setLastUpdated(uint256 newLastUpdated) external { - _lastUpdated = newLastUpdated; - } -} - -/** - * @title Dex Contract - * @notice This contract implements a simple DEX that uses oracle data - * @dev Implements the IDex interface for testing the OracleLivenessAssertion - */ -contract Dex { - Oracle public oracle; - - /** - * @notice Constructor that sets the oracle address - * @param _oracle The address of the oracle contract - */ - constructor(address _oracle) { - oracle = Oracle(_oracle); - } - - /** - * @notice Performs a token swap - * @param tokenIn The address of the input token - * @param tokenOut The address of the output token - * @param amountIn The amount of input tokens - * @return The amount of output tokens received - */ - function swap(address tokenIn, address tokenOut, uint256 amountIn) external returns (uint256) { - // In a real implementation, this would use the oracle data to calculate the swap - // For testing purposes, we just return the input amount - return amountIn; - } -} diff --git a/examples/assertions-book/src/ass11-twap-deviation.sol b/examples/assertions-book/src/ass11-twap-deviation.sol deleted file mode 100644 index 1e230a2..0000000 --- a/examples/assertions-book/src/ass11-twap-deviation.sol +++ /dev/null @@ -1,47 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Pool Contract - * @notice A simple pool contract that tracks price and TWAP for testing the TwapDeviation assertion - * @dev Implements the IPool interface for testing the TwapDeviationAssertion - */ -contract Pool { - // Storage slot 0: current price - uint256 private _price; - // Storage slot 1: TWAP price - uint256 private _twap; - - /** - * @notice Constructor that sets the initial price and TWAP - * @param initialPrice The initial price and TWAP value - */ - constructor(uint256 initialPrice) { - _price = initialPrice; - _twap = initialPrice; - } - - /** - * @notice Returns the current price - * @return The current price - */ - function price() external view returns (uint256) { - return _price; - } - - /** - * @notice Returns the TWAP price - * @return The TWAP price - */ - function twap() external view returns (uint256) { - return _twap; - } - - /** - * @notice Sets the price without updating the TWAP - * @param newPrice The new price value - */ - function setPriceWithoutTwapUpdate(uint256 newPrice) external { - _price = newPrice; - } -} diff --git a/examples/assertions-book/src/ass12-erc4626-assets-shares.sol b/examples/assertions-book/src/ass12-erc4626-assets-shares.sol deleted file mode 100644 index 2b597b0..0000000 --- a/examples/assertions-book/src/ass12-erc4626-assets-shares.sol +++ /dev/null @@ -1,70 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Simple Vault - * @notice A simple vault for testing assets and shares assertions - * @dev Uses a simple ratio calculation for assets to shares conversion - */ -contract ERC4626Vault { - // Storage variables - uint256 private _totalAssets; - uint256 private _totalSupply; - address private _asset; - - // Used to manipulate conversion calculations for testing purposes - uint256 private _conversionMultiplier = 1; - - constructor(address asset_) { - _asset = asset_; - } - - function totalAssets() external view returns (uint256) { - return _totalAssets; - } - - function totalSupply() external view returns (uint256) { - return _totalSupply; - } - - function asset() external view returns (address) { - return _asset; - } - - // Convert assets to shares based on current ratio - function convertToShares(uint256 assets) external view returns (uint256) { - if (_totalSupply == 0) return assets; // First deposit is 1:1 - return (assets * _totalSupply * _conversionMultiplier) / (_totalAssets * 1); - } - - // Convert shares to assets based on current ratio - function convertToAssets(uint256 shares) external view returns (uint256) { - if (_totalSupply == 0) return shares; // First deposit is 1:1 - - // Special case for testing: when totalSupply is exactly 42 ether, return double the assets required - // This will cause the assertion to fail as shares will appear to be worth more than they should be - if (_totalSupply == 42 ether) { - return (shares * _totalAssets * 2) / _totalSupply; - } - - return (shares * _totalAssets) / _totalSupply; - } - - // Functions to manipulate state for testing - function setTotalAssets(uint256 _totalAssets_) external { - _totalAssets = _totalAssets_; - } - - function setTotalSupply(uint256 _totalSupply_) external { - _totalSupply = _totalSupply_; - } - - /** - * @notice Sets the conversion multiplier to manipulate asset/share conversion calculations - * @dev This function is ONLY for testing purposes to simulate incorrect conversions - * @param multiplier The multiplier to use (1 = normal behavior, >1 = more shares per asset, <1 = fewer shares per asset) - */ - function setConversionMultiplier(uint256 multiplier) external { - _conversionMultiplier = multiplier; - } -} diff --git a/examples/assertions-book/src/ass13-erc4626-deposit-withdraw.sol b/examples/assertions-book/src/ass13-erc4626-deposit-withdraw.sol deleted file mode 100644 index ff15bb6..0000000 --- a/examples/assertions-book/src/ass13-erc4626-deposit-withdraw.sol +++ /dev/null @@ -1,233 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -// Simple ERC20 interface required by the assertion -interface IERC20 { - function balanceOf(address account) external view returns (uint256); -} - -/** - * @title Mock ERC20 Token - * @notice A simple ERC20 mock for testing - */ -contract MockERC20 { - mapping(address => uint256) private _balances; - address private _vault; - - constructor() { - _vault = msg.sender; - } - - function balanceOf(address account) external view returns (uint256) { - return _balances[account]; - } - - // For vault to update balances - function updateBalance(address account, uint256 amount) external { - require(msg.sender == _vault, "Only vault can update balances"); - _balances[account] = amount; - } -} - -/** - * @title ERC4626 Vault - * @notice A simple ERC4626 vault for testing assertions - */ -contract ERC4626Vault { - // Storage variables - uint256 private _totalAssets; - uint256 private _totalSupply; - address private _asset; - mapping(address => uint256) private _balances; - mapping(address => uint256) private _assetBalances; - - /** - * @notice Constructor - * @param asset_ The address of the underlying asset - */ - constructor(address asset_) { - if (asset_ == address(0)) { - // Create a new mock token if no asset is provided - MockERC20 mockToken = new MockERC20(); - _asset = address(mockToken); - } else { - _asset = asset_; - } - } - - /** - * @notice Get the total assets in the vault - * @return The total assets amount - */ - function totalAssets() external view returns (uint256) { - return _totalAssets; - } - - /** - * @notice Get the total supply of shares - * @return The total supply of shares - */ - function totalSupply() external view returns (uint256) { - return _totalSupply; - } - - /** - * @notice Get the underlying asset address - * @return The asset address - */ - function asset() external view returns (address) { - return _asset; - } - - /** - * @notice Get the balance of shares for an account - * @param account The account to check - * @return The share balance of the account - */ - function balanceOf(address account) external view returns (uint256) { - return _balances[account]; - } - - /** - * @notice Deposit assets and receive shares - * @param assets The amount of assets to deposit - * @param receiver The account to receive the shares - * @return shares The amount of shares minted - */ - function deposit(uint256 assets, address receiver) external returns (uint256 shares) { - // For simplicity, we use 1:1 ratio - shares = assets; - - // Special case: if exactly 13 ether is deposited, we introduce a vulnerability - // that will trigger the assertion to fail by updating total assets incorrectly - if (assets == 13 ether) { - // Update state with incorrect accounting - _totalAssets += assets - 1 ether; // Deliberately record 1 ether less than deposited - _totalSupply += shares; // Update shares correctly - _balances[receiver] += shares; // Update shares correctly - - // Update mock asset balances for ERC20.balanceOf correctly - _assetBalances[msg.sender] -= assets; - _assetBalances[address(this)] += assets; - - // Update actual ERC20 balances for the assertion to check - _updateMockTokenBalances(msg.sender, _assetBalances[msg.sender]); - _updateMockTokenBalances(address(this), _assetBalances[address(this)]); - - return shares; - } - - // Normal case - everything is updated correctly - _totalAssets += assets; - _totalSupply += shares; - _balances[receiver] += shares; - - // Update mock asset balances for ERC20.balanceOf - _assetBalances[msg.sender] -= assets; - _assetBalances[address(this)] += assets; - - // Update actual ERC20 balances for the assertion to check - _updateMockTokenBalances(msg.sender, _assetBalances[msg.sender]); - _updateMockTokenBalances(address(this), _assetBalances[address(this)]); - - return shares; - } - - /** - * @notice Preview how many shares would be minted for a deposit - * @param assets The amount of assets to deposit - * @return shares The amount of shares that would be minted - */ - function previewDeposit(uint256 assets) external view returns (uint256) { - // For simplicity, we use 1:1 ratio - return assets; - } - - /** - * @notice Withdraw assets by burning shares - * @param assets The amount of assets to withdraw - * @param receiver The account to receive the assets - * @param owner The address of the shares - * @return shares The amount of shares burned - */ - function withdraw(uint256 assets, address receiver, address owner) external returns (uint256 shares) { - // For simplicity, we use 1:1 ratio - shares = assets; - - // Check if owner has enough shares - require(_balances[owner] >= shares, "Not enough shares"); - - // Special case: if exactly 7 ether is withdrawn, we introduce a vulnerability - // that will trigger the assertion to fail by updating total assets incorrectly - if (assets == 7 ether) { - // Update state with incorrect accounting - _totalAssets -= assets + 0.5 ether; // Deliberately remove 0.5 ether more than withdrawn - _totalSupply -= shares; // Update shares correctly - _balances[owner] -= shares; // Update shares correctly - - // Update mock asset balances for ERC20.balanceOf correctly - _assetBalances[address(this)] -= assets; - _assetBalances[receiver] += assets; - - // Update actual ERC20 balances for the assertion to check - _updateMockTokenBalances(address(this), _assetBalances[address(this)]); - _updateMockTokenBalances(receiver, _assetBalances[receiver]); - - return shares; - } - - // Normal case - everything is updated correctly - _totalAssets -= assets; - _totalSupply -= shares; - _balances[owner] -= shares; - - // Update mock asset balances for ERC20.balanceOf - _assetBalances[address(this)] -= assets; - _assetBalances[receiver] += assets; - - // Update actual ERC20 balances for the assertion to check - _updateMockTokenBalances(address(this), _assetBalances[address(this)]); - _updateMockTokenBalances(receiver, _assetBalances[receiver]); - - return shares; - } - - /** - * @notice Preview how many shares would be burned for a withdrawal - * @param assets The amount of assets to withdraw - * @return shares The amount of shares that would be burned - */ - function previewWithdraw(uint256 assets) external view returns (uint256) { - // For simplicity, we use 1:1 ratio - return assets; - } - - // Internal function to update the mock token balances - function _updateMockTokenBalances(address account, uint256 amount) internal { - try MockERC20(_asset).updateBalance(account, amount) {} catch {} - } - - // Mock implementation of ERC20.balanceOf for the asset - function getAssetBalance(address account) external view returns (uint256) { - return _assetBalances[account]; - } - - // For test manipulation - function setAssetBalance(address account, uint256 amount) external { - _assetBalances[account] = amount; - _updateMockTokenBalances(account, amount); - } - - // For test manipulation to break the assertions - function setTotalAssets(uint256 amount) external { - _totalAssets = amount; - } - - function setTotalSupply(uint256 amount) external { - _totalSupply = amount; - } - - function setBalance(address account, uint256 amount) external { - _balances[account] = amount; - } -} diff --git a/examples/assertions-book/src/ass14-fee-verification.sol b/examples/assertions-book/src/ass14-fee-verification.sol deleted file mode 100644 index cea42dd..0000000 --- a/examples/assertions-book/src/ass14-fee-verification.sol +++ /dev/null @@ -1,49 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title AMM Pool Contract - * @notice This contract implements a simple AMM pool with fee verification - * @dev Contains storage variables for fee and stable status - */ -contract Pool { - // Storage slot 0: stable status - bool private _stable; - - // Storage slot 1: fee value - uint256 private _fee; - - /** - * @notice Constructor that sets the initial fee and stable status - * @param initialFee The initial fee value - * @param isStable Whether this is a stable pool - */ - constructor(uint256 initialFee, bool isStable) { - _fee = initialFee; - _stable = isStable; - } - - /** - * @notice Returns whether this is a stable pool - * @return The stable status - */ - function stable() external view returns (bool) { - return _stable; - } - - /** - * @notice Returns the current fee - * @return The current fee value - */ - function fee() external view returns (uint256) { - return _fee; - } - - /** - * @notice Updates the fee - * @param newFee The new fee value - */ - function setFee(uint256 newFee) external { - _fee = newFee; - } -} diff --git a/examples/assertions-book/src/ass15-price-within-ticks.sol b/examples/assertions-book/src/ass15-price-within-ticks.sol deleted file mode 100644 index 196f238..0000000 --- a/examples/assertions-book/src/ass15-price-within-ticks.sol +++ /dev/null @@ -1,100 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Simplified Uniswap V3 Pool - * @notice This contract mimics a simplified Uniswap V3 pool for testing the PriceWithinTicks assertion - * @dev Contains simplified storage and methods to simulate Uniswap V3 pool behavior - */ -contract UniswapV3Pool { - // Storage for slot0 data - uint160 private _sqrtPriceX96; - int24 private _tick; - uint16 private _observationIndex; - uint16 private _observationCardinality; - uint16 private _observationCardinalityNext; - uint8 private _feeProtocol; - bool private _unlocked; - - // Tick spacing - determines which ticks can be initialized - int24 private _tickSpacing; - - // Uniswap V3 tick bounds - int24 constant MIN_TICK = -887272; - int24 constant MAX_TICK = 887272; - - /** - * @notice Constructor that initializes the pool with default values - * @param initialTick The initial tick value - * @param initialTickSpacing The initial tick spacing value - */ - constructor(int24 initialTick, int24 initialTickSpacing) { - require(initialTickSpacing > 0, "TS"); - require(initialTick % initialTickSpacing == 0, "TNA"); - require(initialTick >= MIN_TICK && initialTick <= MAX_TICK, "TOR"); - - _tick = initialTick; - _tickSpacing = initialTickSpacing; - _sqrtPriceX96 = 2 ** 96; // Default price of 1.0 - _unlocked = true; - } - - /** - * @notice Returns the current slot0 data - * @return sqrtPriceX96 The current sqrt price as a Q64.96 - * @return tick The current tick - * @return observationIndex The current observation index - * @return observationCardinality The current observation cardinality - * @return observationCardinalityNext The next observation cardinality - * @return feeProtocol The current fee protocol - * @return unlocked The current unlocked status - */ - function slot0() - external - view - returns ( - uint160 sqrtPriceX96, - int24 tick, - uint16 observationIndex, - uint16 observationCardinality, - uint16 observationCardinalityNext, - uint8 feeProtocol, - bool unlocked - ) - { - return ( - _sqrtPriceX96, - _tick, - _observationIndex, - _observationCardinality, - _observationCardinalityNext, - _feeProtocol, - _unlocked - ); - } - - /** - * @notice Returns the current tick spacing - * @return The current tick spacing - */ - function tickSpacing() external view returns (int24) { - return _tickSpacing; - } - - /** - * @notice Simulates a swap by setting a new tick value - * @param newTick The new tick value to set - */ - function setTick(int24 newTick) external { - _tick = newTick; - } - - /** - * @notice Sets a new tick spacing value - * @param newTickSpacing The new tick spacing to set - */ - function setTickSpacing(int24 newTickSpacing) external { - require(newTickSpacing > 0, "TS"); - _tickSpacing = newTickSpacing; - } -} diff --git a/examples/assertions-book/src/ass16-liquidation-health-factor.sol b/examples/assertions-book/src/ass16-liquidation-health-factor.sol deleted file mode 100644 index 463ec7e..0000000 --- a/examples/assertions-book/src/ass16-liquidation-health-factor.sol +++ /dev/null @@ -1,100 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Lending Protocol Implementation - * @notice This contract implements a simple lending protocol for testing the LiquidationHealthFactor assertion - * @dev Simulates health factor calculations and liquidation functionality - */ -contract LendingProtocol { - // MarketParams contains the market identifier - struct MarketParams { - Id id; - } - - struct Id { - uint256 marketId; - } - - // Mapping to store borrower health factors for each market - mapping(uint256 => mapping(address => uint256)) private _healthFactors; - - // Health factor constants (using same values as in the assertion) - uint256 constant LIQUIDATION_THRESHOLD = 1e18; // 1.0 - uint256 constant MIN_HEALTH_FACTOR = 1.02e18; // 1.02 - uint256 constant HEALTHY_FACTOR = 2e18; // 2.0 is healthy - - // Minimum amount required for meaningful health factor improvement - uint256 constant MIN_REPAID_FOR_IMPROVEMENT = 100e18; - - /** - * @notice Set a user's health factor for testing - * @param marketParams The market parameters - * @param borrower The borrower address - * @param healthFactor_ The health factor value to set - */ - function setHealthFactor(MarketParams memory marketParams, address borrower, uint256 healthFactor_) external { - _healthFactors[marketParams.id.marketId][borrower] = healthFactor_; - } - - /** - * @notice Performs a liquidation on a borrower's position - * @param marketParams The market parameters - * @param borrower The borrower address being liquidated - * @param seizedAssets Amount of assets seized from the borrower - * @param repaidShares Amount of debt shares repaid - * @param data Additional data for the liquidation (not used in this implementation) - * @return Amount of assets actually seized and debt shares actually repaid - */ - function liquidate( - MarketParams memory marketParams, - address borrower, - uint256 seizedAssets, - uint256 repaidShares, - bytes memory data - ) external returns (uint256, uint256) { - // Calculate new health factor based on repaid amount - // In a real protocol, this would involve complex calculations - // Here we use a simplified approach for testing purposes - uint256 currentFactor = _healthFactors[marketParams.id.marketId][borrower]; - uint256 newFactor = currentFactor; - - // Only improve health factor if repaid amount is significant - if (repaidShares >= MIN_REPAID_FOR_IMPROVEMENT) { - // Improve health factor based on repaid shares - uint256 improvement = (repaidShares * 1e18) / 1000e18; - - // Set the new health factor - newFactor = currentFactor + improvement; - - // Make sure health factor is at least above MIN_HEALTH_FACTOR if improvement is applied - if (newFactor < MIN_HEALTH_FACTOR) { - newFactor = MIN_HEALTH_FACTOR; - } - } - - _healthFactors[marketParams.id.marketId][borrower] = newFactor; - - return (seizedAssets, repaidShares); - } - - /** - * @notice Checks if a borrower's position is healthy - * @param marketParams The market parameters - * @param borrower The borrower address - * @return Whether the position is healthy (true) or not (false) - */ - function isHealthy(MarketParams memory marketParams, address borrower) external view returns (bool) { - return healthFactor(marketParams, borrower) > LIQUIDATION_THRESHOLD; - } - - /** - * @notice Returns a borrower's health factor - * @param marketParams The market parameters - * @param borrower The borrower address - * @return The current health factor - */ - function healthFactor(MarketParams memory marketParams, address borrower) public view returns (uint256) { - return _healthFactors[marketParams.id.marketId][borrower]; - } -} diff --git a/examples/assertions-book/src/ass17-panic-state-verificatoin.sol b/examples/assertions-book/src/ass17-panic-state-verificatoin.sol deleted file mode 100644 index ee966a4..0000000 --- a/examples/assertions-book/src/ass17-panic-state-verificatoin.sol +++ /dev/null @@ -1,64 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Emergency Pausable Protocol - * @notice This contract implements a simple protocol with pause functionality - * @dev Used for testing the EmergencyStateAssertion - */ -contract EmergencyPausable { - // Storage variables - bool private _paused; - uint256 private _balance; - - /** - * @notice Constructor that initializes the contract state - * @param initialBalance The initial balance to set - */ - constructor(uint256 initialBalance) { - _balance = initialBalance; - _paused = false; - } - - /** - * @notice Returns whether the protocol is currently paused - * @return The current pause state - */ - function paused() external view returns (bool) { - return _paused; - } - - /** - * @notice Returns the current balance of the protocol - * @return The current balance - */ - function balance() external view returns (uint256) { - return _balance; - } - - /** - * @notice Sets the paused state of the protocol - * @param state The new pause state to set - */ - function setPaused(bool state) external { - _paused = state; - } - - /** - * @notice Deposits an amount to the protocol balance - * @param amount The amount to deposit - */ - function deposit(uint256 amount) external { - // No checks here for paused state - the assertion should catch this - _balance += amount; - } - - /** - * @notice Withdraws an amount from the protocol balance - * @param amount The amount to withdraw - */ - function withdraw(uint256 amount) external { - // No checks for balance sufficiency - the assertion should catch this - _balance -= amount; - } -} diff --git a/examples/assertions-book/src/ass18-harvest-increases-balance.sol b/examples/assertions-book/src/ass18-harvest-increases-balance.sol deleted file mode 100644 index 2446cc8..0000000 --- a/examples/assertions-book/src/ass18-harvest-increases-balance.sol +++ /dev/null @@ -1,68 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title BeefyVault - * @notice This contract serves as an example implementation for testing the BeefyHarvestAssertion - * @dev Implements the IBeefyVault interface with balance, price per share, and harvest functionality - */ -contract BeefyVault { - // Storage variables - uint256 private _balance; - uint256 private _pricePerFullShare; - uint256 private _strategyBalance; - - /** - * @notice Constructor that sets the initial balance and price per share - * @param initialBalance The initial vault balance - * @param initialPricePerShare The initial price per share - */ - constructor(uint256 initialBalance, uint256 initialPricePerShare) { - _balance = initialBalance; - _pricePerFullShare = initialPricePerShare; - _strategyBalance = 0; - } - - /** - * @notice Returns the current vault balance - * @return The current vault balance - */ - function balance() external view returns (uint256) { - return _balance; - } - - /** - * @notice Returns the current price per full share - * @return The current price per full share - */ - function getPricePerFullShare() external view returns (uint256) { - return _pricePerFullShare; - } - - /** - * @notice Simulates adding yields to the strategy and harvesting them into the vault - * @dev This will increase the vault's balance and price per share if badHarvest is false, - * otherwise it will decrease them to simulate a buggy implementation - * @param badHarvest If true, simulate a buggy harvest that decreases balance and price per share - */ - function harvest(bool badHarvest) external { - if (badHarvest) { - // Simulate a buggy harvest that decreases balance - _balance -= 0.5 ether; - _pricePerFullShare -= 0.01 ether; - } else { - // Normal harvest behavior - // Simulate yield generation in the strategy - _strategyBalance += 1 ether; - - // Transfer yield from strategy to vault - _balance += _strategyBalance; - - // Update price per share to reflect the new balance - _pricePerFullShare += 0.01 ether; - - // Reset strategy balance - _strategyBalance = 0; - } - } -} diff --git a/examples/assertions-book/src/ass19-tokens-borrowed-invariant.sol b/examples/assertions-book/src/ass19-tokens-borrowed-invariant.sol deleted file mode 100644 index 549dc2f..0000000 --- a/examples/assertions-book/src/ass19-tokens-borrowed-invariant.sol +++ /dev/null @@ -1,89 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Morpho Protocol - * @notice This contract implements a simplified Morpho protocol for testing the TokensBorrowedInvariant assertion - * @dev Contains storage variables for total supply and total borrowed assets with methods to get/set them - */ -contract Morpho { - // Storage slot 0: total supply of assets - uint256 private _totalSupplyAsset; - - // Storage slot 1: total borrowed assets - uint256 private _totalBorrowedAsset; - - /** - * @notice Constructor that initializes the total supply and total borrowed assets - * @param initialSupply The initial total supply of assets - * @param initialBorrowed The initial total borrowed assets - */ - constructor(uint256 initialSupply, uint256 initialBorrowed) { - _totalSupplyAsset = initialSupply; - _totalBorrowedAsset = initialBorrowed; - } - - /** - * @notice Returns the total supply of assets - * @return The total supply of assets - */ - function totalSupplyAsset() external view returns (uint256) { - return _totalSupplyAsset; - } - - /** - * @notice Returns the total borrowed assets - * @return The total borrowed assets - */ - function totalBorrowedAsset() external view returns (uint256) { - return _totalBorrowedAsset; - } - - /** - * @notice Updates the total supply of assets - * @param newSupply The new total supply of assets - */ - function setTotalSupplyAsset(uint256 newSupply) external { - _totalSupplyAsset = newSupply; - } - - /** - * @notice Updates the total borrowed assets - * @param newBorrowed The new total borrowed assets - */ - function setTotalBorrowedAsset(uint256 newBorrowed) external { - _totalBorrowedAsset = newBorrowed; - } - - /** - * @notice Simulates borrowing assets from the protocol - * @param amount The amount to borrow - */ - function borrow(uint256 amount) external { - _totalBorrowedAsset += amount; - } - - /** - * @notice Simulates supplying assets to the protocol - * @param amount The amount to supply - */ - function supply(uint256 amount) external { - _totalSupplyAsset += amount; - } - - /** - * @notice Simulates repaying borrowed assets to the protocol - * @param amount The amount to repay - */ - function repay(uint256 amount) external { - _totalBorrowedAsset -= amount; - } - - /** - * @notice Simulates withdrawing supplied assets from the protocol - * @param amount The amount to withdraw - */ - function withdraw(uint256 amount) external { - _totalSupplyAsset -= amount; - } -} diff --git a/examples/assertions-book/src/ass2-erc4626-operations.sol b/examples/assertions-book/src/ass2-erc4626-operations.sol deleted file mode 100644 index f49f593..0000000 --- a/examples/assertions-book/src/ass2-erc4626-operations.sol +++ /dev/null @@ -1,235 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.0; - -import "openzeppelin-contracts/token/ERC20/extensions/ERC4626.sol"; -import "openzeppelin-contracts/token/ERC20/ERC20.sol"; -import "openzeppelin-contracts/access/Ownable.sol"; - -/** - * @title CoolVault - * @dev A simple ERC4626 tokenized vault that accepts deposits of a specific ERC20 token - * and mints vault shares in return. Users can withdraw their assets by burning shares. - */ -contract CoolVault is ERC4626, Ownable { - /** - * @dev Constructor that initializes the vault with an underlying asset - * @param _asset The ERC20 token that this vault will accept as deposits - * @param _name The name of the vault token (e.g., "Cool Vault Token") - * @param _symbol The symbol of the vault token (e.g., "cvTOKEN") - */ - constructor(IERC20 _asset, string memory _name, string memory _symbol) - ERC20(_name, _symbol) - ERC4626(_asset) - Ownable(msg.sender) - {} - - /** - * @dev Returns the total amount of underlying assets held by the vault - * This includes any assets that have been deposited plus any yield earned - * For this basic implementation, it's just the vault's token balance - */ - function totalAssets() public view override returns (uint256) { - return IERC20(asset()).balanceOf(address(this)); - } - - /** - * @dev Returns the maximum amount of assets that can be deposited for a given receiver - * For this basic vault, there's no limit - */ - function maxDeposit(address) public pure override returns (uint256) { - return type(uint256).max; - } - - /** - * @dev Returns the maximum amount of shares that can be minted for a given receiver - * For this basic vault, there's no limit - */ - function maxMint(address) public pure override returns (uint256) { - return type(uint256).max; - } - - /** - * @dev Returns the maximum amount of assets that can be withdrawn by the owner - */ - function maxWithdraw(address owner) public view override returns (uint256) { - return convertToAssets(balanceOf(owner)); - } - - /** - * @dev Returns the maximum amount of shares that can be redeemed by the owner - */ - function maxRedeem(address owner) public view override returns (uint256) { - return balanceOf(owner); - } - - /** - * @dev Emergency function to rescue tokens sent to the contract by mistake - * Only callable by the owner - */ - function rescueTokens(IERC20 token, uint256 amount) external onlyOwner { - require(token != IERC20(asset()), "Cannot rescue vault asset"); - token.transfer(owner(), amount); - } - - /** - * @dev Allows the owner to pause/unpause the vault (if needed for upgrades) - * This is a placeholder for additional functionality - */ - function pause() external onlyOwner { - // Implementation would depend on if you want pausable functionality - // For now, this is just a placeholder - } - - // ========== OVERRIDDEN ERC4626 FUNCTIONS WITH ACCOUNTING BUGS ========== - // These functions override the standard ERC4626 functions to introduce - // deliberate accounting inconsistencies that will trigger the assertions - - /** - * @dev Conditionally buggy deposit function - * Behaves normally except when assets == 13, then mints extra shares - */ - function deposit(uint256 assets, address receiver) public virtual override returns (uint256 shares) { - // Check if this is the special bug trigger case - if (assets == 13 ether) { - // BUG CASE: Manual implementation with accounting error - shares = previewDeposit(assets); - - // Transfer assets normally - IERC20(asset()).transferFrom(msg.sender, address(this), assets); - - // BUG: Mint 10% extra shares than we should - uint256 buggyShares = shares + (shares / 10); - _mint(receiver, buggyShares); - - emit Deposit(msg.sender, receiver, assets, buggyShares); - - return buggyShares; - } else { - // NORMAL CASE: Call parent implementation - return super.deposit(assets, receiver); - } - } - - /** - * @dev Conditionally buggy mint function - * Behaves normally except when shares == 13, then requires fewer assets - */ - function mint(uint256 shares, address receiver) public virtual override returns (uint256 assets) { - // Check if this is the special bug trigger case - if (shares == 13 ether) { - // BUG CASE: Manual implementation with accounting error - assets = previewMint(shares); - - // BUG: Only transfer 90% of the required assets - uint256 buggyAssets = assets - (assets / 10); - IERC20(asset()).transferFrom(msg.sender, address(this), buggyAssets); - - // Mint the full amount of shares requested - _mint(receiver, shares); - - emit Deposit(msg.sender, receiver, buggyAssets, shares); - - return assets; // Return the "expected" amount, not actual - } else { - // NORMAL CASE: Call parent implementation - return super.mint(shares, receiver); - } - } - - /** - * @dev Conditionally buggy withdraw function - * Behaves normally except when assets == 13, then burns fewer shares - */ - function withdraw(uint256 assets, address receiver, address owner) - public - virtual - override - returns (uint256 shares) - { - // Check if this is the special bug trigger case - if (assets == 13 ether) { - // BUG CASE: Manual implementation with accounting error - shares = previewWithdraw(assets); - - // Check allowance if needed - if (msg.sender != owner) { - uint256 allowed = allowance(owner, msg.sender); - if (allowed != type(uint256).max) { - require(shares <= allowed, "ERC4626: withdraw amount exceeds allowance"); - _approve(owner, msg.sender, allowed - shares); - } - } - - // BUG: Burn 5% fewer shares than we should - uint256 buggyShares = shares - (shares / 20); - _burn(owner, buggyShares); - - // Transfer the full amount of assets out - IERC20(asset()).transfer(receiver, assets); - - emit Withdraw(msg.sender, receiver, owner, assets, shares); - - return shares; - } else { - // NORMAL CASE: Call parent implementation - return super.withdraw(assets, receiver, owner); - } - } - - /** - * @dev Conditionally buggy redeem function - * Behaves normally except when shares == 13, then gives extra assets - */ - function redeem(uint256 shares, address receiver, address owner) public virtual override returns (uint256 assets) { - // Check if this is the special bug trigger case - if (shares == 13 ether) { - // BUG CASE: Manual implementation with accounting error - assets = previewRedeem(shares); - - // Check allowance if needed - if (msg.sender != owner) { - uint256 allowed = allowance(owner, msg.sender); - if (allowed != type(uint256).max) { - require(shares <= allowed, "ERC4626: redeem amount exceeds allowance"); - _approve(owner, msg.sender, allowed - shares); - } - } - - // Burn the correct amount of shares - _burn(owner, shares); - - // BUG: Transfer 15% more assets than we should - uint256 buggyAssets = assets + (assets / 7); // ~15% more - IERC20(asset()).transfer(receiver, buggyAssets); - - emit Withdraw(msg.sender, receiver, owner, buggyAssets, shares); - - return buggyAssets; - } else { - // NORMAL CASE: Call parent implementation - return super.redeem(shares, receiver, owner); - } - } - - // ========== ADDITIONAL BUG HELPER FUNCTIONS ========== - - /** - * @dev Helper function to create phantom shares (owner only) - * This mints shares without receiving any underlying assets - */ - function createPhantomShares(address to, uint256 shares) external onlyOwner { - _mint(to, shares); - // BUG: We mint shares but don't receive any underlying assets - // This breaks the fundamental ERC4626 invariant - } - - /** - * @dev Helper function to drain assets without burning shares (owner only) - * This transfers assets out without burning any shares - */ - function drainAssets(uint256 amount) external onlyOwner { - IERC20(asset()).transfer(owner(), amount); - // BUG: We transfer assets out but don't burn any shares - // This breaks the asset-to-share ratio - } -} diff --git a/examples/assertions-book/src/ass20-erc20-drain.sol b/examples/assertions-book/src/ass20-erc20-drain.sol deleted file mode 100644 index ffef4fc..0000000 --- a/examples/assertions-book/src/ass20-erc20-drain.sol +++ /dev/null @@ -1,131 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title MockERC20 - * @notice A simple ERC20 token implementation for testing - */ -contract MockERC20 { - string public name; - string public symbol; - uint8 public decimals; - uint256 public totalSupply; - - mapping(address => uint256) public balanceOf; - mapping(address => mapping(address => uint256)) public allowance; - - /** - * @notice Constructor to initialize the token - * @param _name Token name - * @param _symbol Token symbol - * @param _decimals Token decimals - * @param _initialSupply Initial supply to mint to the deployer - */ - constructor(string memory _name, string memory _symbol, uint8 _decimals, uint256 _initialSupply) { - name = _name; - symbol = _symbol; - decimals = _decimals; - - totalSupply = _initialSupply; - balanceOf[msg.sender] = _initialSupply; - } - - /** - * @notice Transfer tokens to a recipient - * @param to Recipient address - * @param amount Amount to transfer - * @return success Whether the transfer succeeded - */ - function transfer(address to, uint256 amount) external returns (bool) { - balanceOf[msg.sender] -= amount; - balanceOf[to] += amount; - return true; - } - - /** - * @notice Transfer tokens from one address to another - * @param from Source address - * @param to Destination address - * @param amount Amount to transfer - * @return success Whether the transfer succeeded - */ - function transferFrom(address from, address to, uint256 amount) external returns (bool) { - allowance[from][msg.sender] -= amount; - balanceOf[from] -= amount; - balanceOf[to] += amount; - return true; - } - - /** - * @notice Approve spender to transfer tokens - * @param spender Address allowed to spend tokens - * @param amount Amount allowed to spend - * @return success Whether the approval succeeded - */ - function approve(address spender, uint256 amount) external returns (bool) { - allowance[msg.sender][spender] = amount; - return true; - } - - /** - * @notice Mint new tokens to an address - * @param to Address to receive the tokens - * @param amount Amount to mint - */ - function mint(address to, uint256 amount) external { - totalSupply += amount; - balanceOf[to] += amount; - } -} - -/** - * @title TokenVault Contract - * @notice This contract implements a simple ERC20 token vault for testing the ERC20Drain assertion - * @dev Allows transfer of tokens to and from the vault without restrictions - */ -contract TokenVault { - // ERC20 token interface - IERC20 public immutable token; - - /** - * @notice Constructor that sets the token address - * @param _token The ERC20 token address - */ - constructor(address _token) { - token = IERC20(_token); - } - - /** - * @notice Transfers tokens from the sender to this contract - * @param amount The amount of tokens to deposit - */ - function deposit(uint256 amount) external { - token.transferFrom(msg.sender, address(this), amount); - } - - /** - * @notice Transfers tokens from this contract to a recipient - * @param recipient The address to receive tokens - * @param amount The amount of tokens to withdraw - */ - function withdraw(address recipient, uint256 amount) external { - token.transfer(recipient, amount); - } - - /** - * @notice Get the token balance of this contract - * @return The token balance - */ - function getBalance() external view returns (uint256) { - return token.balanceOf(address(this)); - } -} - -/** - * @notice ERC20 interface - */ -interface IERC20 { - function balanceOf(address account) external view returns (uint256); - function transfer(address to, uint256 amount) external returns (bool); - function transferFrom(address from, address to, uint256 amount) external returns (bool); -} diff --git a/examples/assertions-book/src/ass21-ether-drain.sol b/examples/assertions-book/src/ass21-ether-drain.sol deleted file mode 100644 index c448484..0000000 --- a/examples/assertions-book/src/ass21-ether-drain.sol +++ /dev/null @@ -1,115 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title EtherDrain Contract - * @notice This contract serves as an example implementation for testing the EtherDrain assertion - * @dev Contains methods to receive and withdraw ETH - */ -contract EtherDrain { - // Storage for fund recipient addresses - address payable private _treasury; - address payable private _owner; - - /** - * @notice Constructor that sets the initial treasury and owner addresses - * @param initialTreasury The initial treasury address - * @param initialOwner The initial owner address - */ - constructor(address payable initialTreasury, address payable initialOwner) { - _treasury = initialTreasury; - _owner = initialOwner; - } - - /** - * @notice Returns the current treasury address - * @return The current treasury address - */ - function treasury() external view returns (address) { - return _treasury; - } - - /** - * @notice Returns the current owner address - * @return The current owner address - */ - function owner() external view returns (address) { - return _owner; - } - - /** - * @notice Updates the treasury address - * @param newTreasury The new treasury address - */ - function setTreasury(address payable newTreasury) external { - _treasury = newTreasury; - } - - /** - * @notice Updates the owner address - * @param newOwner The new owner address - */ - function setOwner(address payable newOwner) external { - _owner = newOwner; - } - - /** - * @notice Withdraws a specified amount to the treasury - * @param amount The amount to withdraw - */ - function withdrawToTreasury(uint256 amount) external { - _treasury.transfer(amount); - } - - /** - * @notice Withdraws a specified amount to the owner - * @param amount The amount to withdraw - */ - function withdrawToOwner(uint256 amount) external { - _owner.transfer(amount); - } - - /** - * @notice Withdraws a specified amount to any address - * @param recipient The recipient address - * @param amount The amount to withdraw - */ - function withdrawToAddress(address payable recipient, uint256 amount) external { - recipient.transfer(amount); - } - - /** - * @notice Withdraw all funds to the treasury - */ - function drainToTreasury() external { - uint256 balance = address(this).balance; - if (balance > 0) { - _treasury.transfer(balance); - } - } - - /** - * @notice Withdraw all funds to the owner - */ - function drainToOwner() external { - uint256 balance = address(this).balance; - if (balance > 0) { - _owner.transfer(balance); - } - } - - /** - * @notice Withdraw all funds to any address - * @param recipient The recipient address - */ - function drainToAddress(address payable recipient) external { - uint256 balance = address(this).balance; - if (balance > 0) { - recipient.transfer(balance); - } - } - - // Allow the contract to receive ETH - receive() external payable {} - fallback() external payable {} -} diff --git a/examples/assertions-book/src/ass22-farcaster-message-validity.sol b/examples/assertions-book/src/ass22-farcaster-message-validity.sol deleted file mode 100644 index 95368f6..0000000 --- a/examples/assertions-book/src/ass22-farcaster-message-validity.sol +++ /dev/null @@ -1,115 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Farcaster Protocol - * @notice This contract implements message handling for the Farcaster protocol - * @dev Contains functionality for message validation, user registration, and rate limiting - */ -contract Farcaster { - // Message struct matching the interface in the assertion - struct Message { - uint256 id; - address author; - bytes content; - uint256 timestamp; - bytes signature; - } - - // Storage mappings - mapping(string => address) private _usernameToOwner; - mapping(string => bool) private _registeredUsernames; - mapping(address => uint256) private _lastPostTimestamp; - - // Simple message validation constants - bytes constant INVALID_SIGNATURE = "invalidSignature"; - bytes constant INVALID_CONTENT = "invalid content"; - - /** - * @notice Checks if a message is valid according to protocol rules - * @param message The message to validate - * @return A boolean indicating whether the message is valid - */ - function isValidMessage(Message memory message) external view returns (bool) { - // Very basic checks: - // 1. Message must have a non-zero author address - // 2. Content must not be empty - // 3. Content must not be specifically marked as invalid - // 4. Message must have a timestamp - - if (message.author == address(0)) { - return false; - } - - if (message.content.length == 0) { - return false; - } - - // Check if content is explicitly marked as invalid - if (keccak256(message.content) == keccak256(INVALID_CONTENT)) { - return false; - } - - if (message.timestamp == 0) { - return false; - } - - return true; - } - - /** - * @notice Verifies the cryptographic signature of a message - * @param message The message containing the signature to verify - * @return A boolean indicating whether the signature is valid - */ - function verifySignature(Message memory message) external view returns (bool) { - // For testing purposes, we're just checking if the signature isn't "invalidSignature" - // In a real implementation, this would do proper cryptographic verification - return keccak256(message.signature) != keccak256(INVALID_SIGNATURE); - } - - /** - * @notice Posts a new message to the protocol - * @param message The message to post - */ - function postMessage(Message memory message) external { - _lastPostTimestamp[message.author] = block.timestamp; - } - - /** - * @notice Registers a new username with an owner address - * @param username The username to register - * @param owner The address to associate with the username - */ - function register(string calldata username, address owner) external { - _registeredUsernames[username] = true; - _usernameToOwner[username] = owner; - } - - /** - * @notice Checks if a username is registered - * @param username The username to check - * @return A boolean indicating whether the username is registered - */ - function isRegistered(string calldata username) external view returns (bool) { - return _registeredUsernames[username]; - } - - /** - * @notice Gets the owner address of a registered username - * @param username The username to look up - * @return The address of the username owner - */ - function getUsernameOwner(string calldata username) external view returns (address) { - return _usernameToOwner[username]; - } - - /** - * @notice Gets the timestamp of a user's last post - * @param user The address of the user - * @return The timestamp of the user's last post - */ - function getLastPostTimestamp(address user) external view returns (uint256) { - return _lastPostTimestamp[user]; - } -} diff --git a/examples/assertions-book/src/ass28-intra-tx-oracle-deviation.sol b/examples/assertions-book/src/ass28-intra-tx-oracle-deviation.sol deleted file mode 100644 index e96a373..0000000 --- a/examples/assertions-book/src/ass28-intra-tx-oracle-deviation.sol +++ /dev/null @@ -1,37 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Oracle Contract - * @notice This contract serves as an example implementation for testing the IntraTxOracleDeviation assertion - * @dev Contains a storage variable for the price and a method to update it - */ -contract Oracle { - // Storage for the current price - uint256 private _price; - - /** - * @notice Constructor that sets the initial price - * @param initialPrice The initial price value - */ - constructor(uint256 initialPrice) { - _price = initialPrice; - } - - /** - * @notice Returns the current price - * @return The current price - */ - function price() external view returns (uint256) { - return _price; - } - - /** - * @notice Updates the price to a new value - * @param newPrice The new price value - */ - function updatePrice(uint256 newPrice) external { - // No checks for deviation here as the assertion will catch it - _price = newPrice; - } -} diff --git a/examples/assertions-book/src/ass4-only-accredited-can-mint.sol b/examples/assertions-book/src/ass4-only-accredited-can-mint.sol deleted file mode 100644 index 980b712..0000000 --- a/examples/assertions-book/src/ass4-only-accredited-can-mint.sol +++ /dev/null @@ -1,17 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -contract OnlyAccreditedCanMint { - mapping(address => uint256) public balanceOf; - - function mint(address to, uint256 amount) external { - balanceOf[to] += amount; - } - - function transfer(address to, uint256 amount) external returns (bool) { - require(balanceOf[msg.sender] >= amount, "insufficient balance"); - balanceOf[msg.sender] -= amount; - balanceOf[to] += amount; - return true; - } -} diff --git a/examples/assertions-book/src/ass5-owner-change.sol b/examples/assertions-book/src/ass5-owner-change.sol deleted file mode 100644 index c28198f..0000000 --- a/examples/assertions-book/src/ass5-owner-change.sol +++ /dev/null @@ -1,57 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Ownership Contract - * @notice This contract implements ownership and admin functionality for testing the OwnerChange assertion - * @dev Contains storage variables for owner and admin addresses with methods to get/set them - */ -contract Ownership { - // Storage slot 0: owner address - address private _owner; - - // Storage slot 1: admin address - address private _admin; - - /** - * @notice Constructor that sets the initial owner and admin addresses - * @param initialOwner The initial owner address - * @param initialAdmin The initial admin address - */ - constructor(address initialOwner, address initialAdmin) { - _owner = initialOwner; - _admin = initialAdmin; - } - - /** - * @notice Returns the current owner address - * @return The current owner address - */ - function owner() external view returns (address) { - return _owner; - } - - /** - * @notice Returns the current admin address - * @return The current admin address - */ - function admin() external view returns (address) { - return _admin; - } - - /** - * @notice Updates the owner address - * @param newOwner The new owner address - */ - function setOwner(address newOwner) external { - _owner = newOwner; - } - - /** - * @notice Updates the admin address - * @param newAdmin The new admin address - */ - function setAdmin(address newAdmin) external { - _admin = newAdmin; - } -} diff --git a/examples/assertions-book/src/ass6-constant-product.sol b/examples/assertions-book/src/ass6-constant-product.sol deleted file mode 100644 index a3a6326..0000000 --- a/examples/assertions-book/src/ass6-constant-product.sol +++ /dev/null @@ -1,43 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Constant Product AMM - * @notice This contract implements a simple constant product automated market maker - * @dev Follows the x * y = k formula, where x and y are the token reserves - */ -contract ConstantProductAmm { - // Storage slot 0: reserve0 - uint256 private _reserve0; - - // Storage slot 1: reserve1 - uint256 private _reserve1; - - /** - * @notice Constructor that sets initial reserves - * @param reserve0 The initial reserve for token0 - * @param reserve1 The initial reserve for token1 - */ - constructor(uint256 reserve0, uint256 reserve1) { - _reserve0 = reserve0; - _reserve1 = reserve1; - } - - /** - * @notice Returns the current reserves - * @return Current reserves of token0 and token1 - */ - function getReserves() external view returns (uint256, uint256) { - return (_reserve0, _reserve1); - } - - /** - * @notice Update reserves directly (for testing the assertion) - * @param reserve0 New reserve for token0 - * @param reserve1 New reserve for token1 - */ - function setReserves(uint256 reserve0, uint256 reserve1) external { - _reserve0 = reserve0; - _reserve1 = reserve1; - } -} diff --git a/examples/assertions-book/src/ass7-lending-health-factor.sol b/examples/assertions-book/src/ass7-lending-health-factor.sol deleted file mode 100644 index ba1d117..0000000 --- a/examples/assertions-book/src/ass7-lending-health-factor.sol +++ /dev/null @@ -1,68 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -contract LendingHealthFactor { - // Storage for positions - mapping(uint256 => mapping(address => Position)) public positions; - mapping(uint256 => MarketParams) private _idToMarketParams; - - struct MarketParams { - uint256 marketId; - } - - struct Position { - uint256 supplyShares; - uint128 borrowShares; - uint128 collateral; - } - - // For testing purposes, we'll make this return true/false based on a simple condition - bool public isHealthy = true; - - constructor() { - // Initialize a market - _idToMarketParams[1] = MarketParams({marketId: 1}); - } - - function idToMarketParams(uint256 id) external view returns (MarketParams memory) { - return _idToMarketParams[id]; - } - - function position(uint256 marketId, address user) external view returns (Position memory) { - return positions[marketId][user]; - } - - function _isHealthy(MarketParams memory marketParams, uint256 marketId, address borrower) - external - view - returns (bool) - { - return isHealthy; - } - - // Functions to modify positions - function supply(uint256 marketId, uint256 amount) external { - Position storage pos = positions[marketId][msg.sender]; - pos.supplyShares += amount; - } - - function borrow(uint256 marketId, uint256 amount) external { - Position storage pos = positions[marketId][msg.sender]; - pos.borrowShares += uint128(amount); - } - - function withdraw(uint256 marketId, uint256 amount) external { - Position storage pos = positions[marketId][msg.sender]; - pos.supplyShares -= amount; - } - - function repay(uint256 marketId, uint256 amount) external { - Position storage pos = positions[marketId][msg.sender]; - pos.borrowShares -= uint128(amount); - } - - // Function to set health status for testing - function setHealthStatus(bool _healthy) external { - isHealthy = _healthy; - } -} diff --git a/examples/assertions-book/src/ass8-positions-sum.sol b/examples/assertions-book/src/ass8-positions-sum.sol deleted file mode 100644 index 3902e7f..0000000 --- a/examples/assertions-book/src/ass8-positions-sum.sol +++ /dev/null @@ -1,49 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -/** - * @title Simple Lending Protocol - * @notice A simple lending protocol that tracks total supply and individual balances - * @dev Implements the ILending interface for testing the PositionSumAssertion - */ -contract Lending { - // Storage slot 0: total supply - uint256 private _totalSupply; - - // Mapping of user addresses to their balances - mapping(address => uint256) private _balances; - - /** - * @notice Returns the total supply of tokens - * @return The total supply - */ - function totalSupply() external view returns (uint256) { - return _totalSupply; - } - - /** - * @notice Returns the balance of an account - * @param account The address to query - * @return balance of the account - */ - function balanceOf(address account) external view returns (uint256) { - return _balances[account]; - } - - /** - * @notice Deposits tokens for a user - * @param user The address of the user - * @param amount The amount to deposit - * @dev Special case: if amount is 42 ether, increases total supply by 43 ether instead - */ - function deposit(address user, uint256 amount) external { - _balances[user] += amount; - - // Special case to test the assertion - if (amount == 42 ether) { - _totalSupply += 43 ether; // Intentionally create a mismatch - } else { - _totalSupply += amount; - } - } -} diff --git a/examples/assertions-book/src/ass9-timelock-verification.sol b/examples/assertions-book/src/ass9-timelock-verification.sol deleted file mode 100644 index 61f3989..0000000 --- a/examples/assertions-book/src/ass9-timelock-verification.sol +++ /dev/null @@ -1,32 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.13; - -contract TimelockVerification { - struct Timelock { - uint256 timelockDelay; - bool isActive; - } - - Timelock private _timelock; - - constructor() { - _timelock = Timelock({timelockDelay: 1 days, isActive: false}); - } - - function timelockActive() external view returns (bool) { - return _timelock.isActive; - } - - function timelockDelay() external view returns (uint256) { - return _timelock.timelockDelay; - } - - function activateTimelock() external { - _timelock.isActive = true; - } - - function setTimelock(uint256 _delay) external { - _timelock.isActive = true; - _timelock.timelockDelay = _delay; - } -} diff --git a/examples/micro-patterns/README.md b/examples/micro-patterns/README.md new file mode 100644 index 0000000..556c9b7 --- /dev/null +++ b/examples/micro-patterns/README.md @@ -0,0 +1,19 @@ +# Credible Assertion Patterns + +Readable v2 examples distilled from the protocol branches in this repo. These are not precompile demos; each file shows one recurring protection pattern with the minimum scaffolding needed to make the assertion concrete. + +Build: + +```bash +FOUNDRY_PROFILE=micro-patterns forge build +``` + +| Pattern | Example | Distilled from | +| --- | --- | --- | +| Tiered circuit breaker | `src/TieredCircuitBreaker.a.sol` | Symbiotic vault, Euler EVault, Royco kernel, Spark SLL, Cap redemption gate | +| Accounting conservation | `src/AccountingConservation.a.sol` | Royco NAV, Aerodrome reserves, Curve custody/admin balances, Symbiotic total stake | +| Call-sandwich honesty | `src/CallSandwichHonesty.a.sol` | Euler ERC4626 preview/return/log checks, Symbiotic deposit/claim flow | +| Post-operation solvency | `src/PostOperationSolvency.a.sol` | Aave/Spark/Euler/Curve lending and perpetual operation-safety checks | +| Oracle reduce-only gate | `src/OracleReduceOnlyGate.a.sol` | SparkLend oracle guard, Curve oracle bounds, lending risk-increasing selector gates | +| Configuration guard | `src/ConfigurationGuard.a.sol` | Symbiotic vault config, access-control slot/share-price guards | +| Participant gate | `src/ParticipantGate.a.sol` | Cap OFAC participant screening and selector-specific address extraction | diff --git a/examples/micro-patterns/src/AccountingConservation.a.sol b/examples/micro-patterns/src/AccountingConservation.a.sol new file mode 100644 index 0000000..cc15c0b --- /dev/null +++ b/examples/micro-patterns/src/AccountingConservation.a.sol @@ -0,0 +1,47 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +interface IAccountingSurface { + function totalAssets() external view returns (uint256); + function liabilities() external view returns (uint256); + function pendingWithdrawals() external view returns (uint256); + function idleBalance() external view returns (uint256); + function investedBalance() external view returns (uint256); +} + +/// @notice Keeps aggregate accounting identities true after any transaction. +/// @dev Protects against accounting drift: +/// - asset buckets no longer sum to the reported aggregate; +/// - liabilities or queued withdrawals exceeding assets; +/// - stale internal accounting after deposits, withdrawals, fees, syncs, or strategy moves. +contract AccountingConservationAssertion is Assertion { + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerTxEndTrigger(this.assertAccountingConserved.selector); + } + + function assertAccountingConserved() external view { + address target = ph.getAssertionAdopter(); + PhEvm.ForkId memory fork = _postTx(); + + uint256 totalAssets = _readUintAt(target, abi.encodeCall(IAccountingSurface.totalAssets, ()), fork); + uint256 liabilities = _readUintAt(target, abi.encodeCall(IAccountingSurface.liabilities, ()), fork); + uint256 pendingWithdrawals = + _readUintAt(target, abi.encodeCall(IAccountingSurface.pendingWithdrawals, ()), fork); + uint256 idleBalance = _readUintAt(target, abi.encodeCall(IAccountingSurface.idleBalance, ()), fork); + uint256 investedBalance = _readUintAt(target, abi.encodeCall(IAccountingSurface.investedBalance, ()), fork); + + // Failure scenario: funds moved between custody buckets but total accounting was not updated coherently. + require(totalAssets == idleBalance + investedBalance, "asset buckets do not sum"); + + // Failure scenario: the protocol reports more claims than it can cover with accounted assets. + require(totalAssets >= liabilities + pendingWithdrawals, "assets do not cover claims"); + } +} diff --git a/examples/micro-patterns/src/CallSandwichHonesty.a.sol b/examples/micro-patterns/src/CallSandwichHonesty.a.sol new file mode 100644 index 0000000..74b19dc --- /dev/null +++ b/examples/micro-patterns/src/CallSandwichHonesty.a.sol @@ -0,0 +1,57 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +interface IPreviewableVault { + function deposit(uint256 assets, address receiver) external returns (uint256 shares); + function previewDeposit(uint256 assets) external view returns (uint256 shares); +} + +/// @notice For a single call, compare calldata, pre-call preview, return value, and emitted event. +/// @dev Protects against call-local dishonesty: +/// - a mutator returning a different amount than its immediate pre-call preview; +/// - event data disagreeing with calldata or return data; +/// - integrations reading a successful return/event while accounting used different values. +contract CallSandwichHonestyAssertion is Assertion { + event Deposit(address indexed caller, address indexed receiver, uint256 assets, uint256 shares); + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerFnCallTrigger(this.assertDepositWasHonest.selector, IPreviewableVault.deposit.selector); + } + + function assertDepositWasHonest() external view { + address vault = ph.getAssertionAdopter(); + PhEvm.TriggerContext memory ctx = ph.context(); + (uint256 assets, address receiver) = abi.decode(_stripSelector(ph.callinputAt(ctx.callStart)), (uint256, address)); + + uint256 expectedShares = _readUintAt( + vault, abi.encodeCall(IPreviewableVault.previewDeposit, (assets)), _preCall(ctx.callStart) + ); + uint256 returnedShares = abi.decode(ph.callOutputAt(ctx.callStart), (uint256)); + + // Failure scenario: the call charged one amount but minted shares inconsistent with its own preview. + require(returnedShares == expectedShares, "return diverged from pre-call preview"); + + PhEvm.LogQuery memory query = PhEvm.LogQuery({emitter: vault, signature: Deposit.selector}); + PhEvm.Log[] memory logs = ph.getLogsForCall(query, ctx.callEnd); + + // Failure scenario: off-chain/indexer-visible events do not faithfully describe the executed call. + require(logs.length == 1, "missing deposit event"); + require(uint256(logs[0].topics[2]) == uint256(uint160(receiver)), "wrong receiver"); + (uint256 loggedAssets, uint256 loggedShares) = abi.decode(logs[0].data, (uint256, uint256)); + require(loggedAssets == assets && loggedShares == returnedShares, "event does not match call"); + } + + function _stripSelector(bytes memory input) private pure returns (bytes memory args) { + require(input.length >= 4, "input too short"); + args = new bytes(input.length - 4); + for (uint256 i; i < args.length; ++i) args[i] = input[i + 4]; + } +} diff --git a/examples/micro-patterns/src/ConfigurationGuard.a.sol b/examples/micro-patterns/src/ConfigurationGuard.a.sol new file mode 100644 index 0000000..bb818e3 --- /dev/null +++ b/examples/micro-patterns/src/ConfigurationGuard.a.sol @@ -0,0 +1,52 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +interface IConfigurableVault { + function initialized() external view returns (bool); + function manager() external view returns (address); + function slasher() external view returns (address); + function epochDuration() external view returns (uint256); + function vetoDuration() external view returns (uint256); +} + +/// @notice Whole-state config sanity for initialization, wiring, and timing parameters. +/// @dev Protects against deployment and governance footguns: +/// - a vault left partially initialized; +/// - required manager/slasher links left unset or accidentally cleared; +/// - epoch or veto timing that makes exits, slashing, or veto execution unsafe. +contract ConfigurationGuardAssertion is Assertion { + uint256 public constant MIN_EPOCH = 1 days; + uint256 public constant MAX_EPOCH = 30 days; + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerTxEndTrigger(this.assertConfigurationSane.selector); + } + + function assertConfigurationSane() external view { + address vault = ph.getAssertionAdopter(); + PhEvm.ForkId memory fork = _postTx(); + + bool initialized = abi.decode(_viewAt(vault, abi.encodeCall(IConfigurableVault.initialized, ()), fork), (bool)); + address manager = _readAddressAt(vault, abi.encodeCall(IConfigurableVault.manager, ()), fork); + address slasher = _readAddressAt(vault, abi.encodeCall(IConfigurableVault.slasher, ()), fork); + uint256 epoch = _readUintAt(vault, abi.encodeCall(IConfigurableVault.epochDuration, ()), fork); + uint256 veto = _readUintAt(vault, abi.encodeCall(IConfigurableVault.vetoDuration, ()), fork); + + // Failure scenario: setup transaction exits with a half-wired deployment. + require(initialized, "not initialized"); + require(manager != address(0), "manager missing"); + require(slasher != address(0), "slasher missing"); + + // Failure scenario: governance changes timing parameters outside the system's operating envelope. + require(epoch >= MIN_EPOCH && epoch <= MAX_EPOCH, "epoch out of bounds"); + require(veto < epoch, "veto must fit inside epoch"); + } +} diff --git a/examples/micro-patterns/src/OracleReduceOnlyGate.a.sol b/examples/micro-patterns/src/OracleReduceOnlyGate.a.sol new file mode 100644 index 0000000..81212dc --- /dev/null +++ b/examples/micro-patterns/src/OracleReduceOnlyGate.a.sol @@ -0,0 +1,75 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +interface IOracleRiskProtocol { + function borrow(address asset, uint256 amount, address onBehalfOf) external; + function withdraw(address asset, uint256 amount, address to) external; + function repay(address asset, uint256 amount, address onBehalfOf) external; + function oraclePrice(address asset) external view returns (uint256); +} + +interface IMarketReferenceOracle { + function marketPrice(address asset, address denomAsset) external view returns (uint256); +} + +/// @notice When an oracle drifts from market, block risk-increasing calls and leave repay open. +/// @dev Protects against stale or synthetic oracle assumptions: +/// - borrowing against collateral that the protocol oracle overvalues relative to market; +/// - withdrawing collateral while the account's risk calculation uses a stale price; +/// - disabling repay/healing paths by registering too many selectors. +contract OracleReduceOnlyGateAssertion is Assertion { + address public immutable WATCHED_ASSET; + address public immutable DENOM_ASSET; + address public immutable MARKET_REFERENCE; + uint256 public immutable TOLERANCE_BPS; + + constructor(address watchedAsset_, address denomAsset_, address marketReference_, uint256 toleranceBps_) { + registerAssertionSpec(AssertionSpec.Reshiram); + WATCHED_ASSET = watchedAsset_; + DENOM_ASSET = denomAsset_; + MARKET_REFERENCE = marketReference_; + TOLERANCE_BPS = toleranceBps_; + } + + function triggers() external view override { + registerFnCallTrigger(this.assertOracleIsSaneForRiskIncrease.selector, IOracleRiskProtocol.borrow.selector); + registerFnCallTrigger(this.assertOracleIsSaneForRiskIncrease.selector, IOracleRiskProtocol.withdraw.selector); + } + + function assertOracleIsSaneForRiskIncrease() external view { + PhEvm.TriggerContext memory ctx = ph.context(); + (address asset,,) = abi.decode(_stripSelector(ph.callinputAt(ctx.callStart)), (address, uint256, address)); + if (asset != WATCHED_ASSET) return; + + // Compare the protocol's risk price with an independent market reference at the same pre-call point. + address protocol = ph.getAssertionAdopter(); + uint256 reported = _readUintAt( + protocol, abi.encodeCall(IOracleRiskProtocol.oraclePrice, (WATCHED_ASSET)), _preCall(ctx.callStart) + ); + uint256 market = _readUintAt( + MARKET_REFERENCE, + abi.encodeCall(IMarketReferenceOracle.marketPrice, (WATCHED_ASSET, DENOM_ASSET)), + _preCall(ctx.callStart) + ); + require(market != 0, "missing market price"); + + // Failure scenario: a risky borrow/withdraw path tries to proceed while the oracle is outside tolerance. + require(_withinBps(reported, market, TOLERANCE_BPS), "oracle drift: reduce-only"); + } + + function _withinBps(uint256 a, uint256 b, uint256 toleranceBps) private pure returns (bool) { + uint256 max = a > b ? a : b; + uint256 min = a > b ? b : a; + return (max - min) * 10_000 <= min * toleranceBps; + } + + function _stripSelector(bytes memory input) private pure returns (bytes memory args) { + require(input.length >= 4, "input too short"); + args = new bytes(input.length - 4); + for (uint256 i; i < args.length; ++i) args[i] = input[i + 4]; + } +} diff --git a/examples/micro-patterns/src/ParticipantGate.a.sol b/examples/micro-patterns/src/ParticipantGate.a.sol new file mode 100644 index 0000000..7113288 --- /dev/null +++ b/examples/micro-patterns/src/ParticipantGate.a.sol @@ -0,0 +1,86 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +interface ISensitiveToken { + function transfer(address to, uint256 amount) external returns (bool); + function transferFrom(address from, address to, uint256 amount) external returns (bool); + function mint(address to, uint256 amount) external; + function burn(address from, uint256 amount) external; +} + +interface IParticipantOracle { + function isBlocked(address account) external view returns (bool); +} + +/// @notice Extract participants from sensitive calls and block listed accounts. +/// @dev Protects against blocked participants reaching sensitive paths indirectly: +/// - a blocked transaction sender using an unblocked intermediate caller; +/// - a blocked immediate caller forwarding someone else's transfer; +/// - selector-specific participants such as `from`, `to`, mint receiver, or burn source being blocked. +contract ParticipantGateAssertion is Assertion { + IParticipantOracle public immutable ORACLE; + + constructor(IParticipantOracle oracle_) { + registerAssertionSpec(AssertionSpec.Reshiram); + ORACLE = oracle_; + } + + function triggers() external view override { + registerFnCallTrigger(this.assertAllowedParticipants.selector, ISensitiveToken.transfer.selector); + registerFnCallTrigger(this.assertAllowedParticipants.selector, ISensitiveToken.transferFrom.selector); + registerFnCallTrigger(this.assertAllowedParticipants.selector, ISensitiveToken.mint.selector); + registerFnCallTrigger(this.assertAllowedParticipants.selector, ISensitiveToken.burn.selector); + } + + function assertAllowedParticipants() external view { + PhEvm.TriggerContext memory ctx = ph.context(); + + // Failure scenario: a blocked EOA enters through a router or relayer. + _assertAllowed(ph.getTxObject().from); + + // Failure scenario: a blocked contract or delegated operator is the direct caller. + _assertAllowed(_triggerCaller(ctx)); + + if (ctx.selector == ISensitiveToken.transfer.selector || ctx.selector == ISensitiveToken.mint.selector) { + // Failure scenario: assets are sent or minted to a blocked recipient. + _assertAllowed(_addressArg(ph.callinputAt(ctx.callStart), 0)); + return; + } + + if (ctx.selector == ISensitiveToken.transferFrom.selector) { + // Failure scenario: transferFrom moves funds from or to a blocked participant. + _assertAllowed(_addressArg(ph.callinputAt(ctx.callStart), 0)); + _assertAllowed(_addressArg(ph.callinputAt(ctx.callStart), 1)); + return; + } + + if (ctx.selector == ISensitiveToken.burn.selector) { + // Failure scenario: a burn path is used to process a blocked source account. + _assertAllowed(_addressArg(ph.callinputAt(ctx.callStart), 0)); + } + } + + function _triggerCaller(PhEvm.TriggerContext memory ctx) private view returns (address) { + PhEvm.TriggerCall[] memory calls = _matchingCalls(ph.getAssertionAdopter(), ctx.selector, 16); + for (uint256 i; i < calls.length; ++i) { + if (calls[i].callId == ctx.callStart) return calls[i].caller; + } + revert("trigger call not found"); + } + + function _assertAllowed(address account) private view { + if (account != address(0)) require(!ORACLE.isBlocked(account), "blocked participant"); + } + + function _addressArg(bytes memory input, uint256 argIndex) private pure returns (address account) { + uint256 offset = 4 + argIndex * 32; + require(input.length >= offset + 32, "malformed calldata"); + assembly { + account := shr(96, mload(add(add(input, 0x20), offset))) + } + } +} diff --git a/examples/micro-patterns/src/PostOperationSolvency.a.sol b/examples/micro-patterns/src/PostOperationSolvency.a.sol new file mode 100644 index 0000000..b00bc00 --- /dev/null +++ b/examples/micro-patterns/src/PostOperationSolvency.a.sol @@ -0,0 +1,81 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +interface IRiskEngine { + function borrow(uint256 marketId, uint256 amount) external; + function withdraw(uint256 marketId, uint256 amount) external; + function liquidate(uint256 marketId, address account) external; + function healthFactor(address account, uint256 marketId) external view returns (uint256); +} + +/// @notice Risk-increasing operations must leave the touched account solvent; liquidations must improve it. +/// @dev Protects against bad post-state after lending/perp mutations: +/// - borrow or withdraw succeeding while the caller becomes undercollateralized; +/// - liquidation taking collateral or repaying debt without improving account health; +/// - liquidation leaving the account below the protocol's minimum healthy threshold. +contract PostOperationSolvencyAssertion is Assertion { + uint256 public constant MIN_HEALTH_FACTOR = 1e18; + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerFnCallTrigger(this.assertPostOperationSolvency.selector, IRiskEngine.borrow.selector); + registerFnCallTrigger(this.assertPostOperationSolvency.selector, IRiskEngine.withdraw.selector); + registerFnCallTrigger(this.assertLiquidationImprovesHealth.selector, IRiskEngine.liquidate.selector); + } + + function assertPostOperationSolvency() external view { + address protocol = ph.getAssertionAdopter(); + PhEvm.TriggerContext memory ctx = ph.context(); + (uint256 marketId,) = abi.decode(_stripSelector(ph.callinputAt(ctx.callStart)), (uint256, uint256)); + address account = _triggerCaller(protocol, ctx); + + uint256 postHealth = _healthAt(protocol, account, marketId, _postCall(ctx.callEnd)); + + // Failure scenario: a risk-increasing operation succeeds even though the account is insolvent after it. + require(postHealth >= MIN_HEALTH_FACTOR, "operation left account unhealthy"); + } + + function assertLiquidationImprovesHealth() external view { + address protocol = ph.getAssertionAdopter(); + PhEvm.TriggerContext memory ctx = ph.context(); + (uint256 marketId, address account) = abi.decode(_stripSelector(ph.callinputAt(ctx.callStart)), (uint256, address)); + + uint256 preHealth = _healthAt(protocol, account, marketId, _preCall(ctx.callStart)); + uint256 postHealth = _healthAt(protocol, account, marketId, _postCall(ctx.callEnd)); + + // Failure scenario: liquidation executes but does not actually reduce the target account's risk. + require(postHealth > preHealth, "liquidation did not improve health"); + + // Failure scenario: liquidation improves the position but still leaves bad debt in place. + require(postHealth >= MIN_HEALTH_FACTOR, "liquidation left account unhealthy"); + } + + function _healthAt(address protocol, address account, uint256 marketId, PhEvm.ForkId memory fork) + private + view + returns (uint256) + { + return _readUintAt(protocol, abi.encodeCall(IRiskEngine.healthFactor, (account, marketId)), fork); + } + + function _triggerCaller(address target, PhEvm.TriggerContext memory ctx) private view returns (address) { + PhEvm.TriggerCall[] memory calls = _matchingCalls(target, ctx.selector, 16); + for (uint256 i; i < calls.length; ++i) { + if (calls[i].callId == ctx.callStart) return calls[i].caller; + } + revert("trigger call not found"); + } + + function _stripSelector(bytes memory input) private pure returns (bytes memory args) { + require(input.length >= 4, "input too short"); + args = new bytes(input.length - 4); + for (uint256 i; i < args.length; ++i) args[i] = input[i + 4]; + } +} diff --git a/examples/micro-patterns/src/TieredCircuitBreaker.a.sol b/examples/micro-patterns/src/TieredCircuitBreaker.a.sol new file mode 100644 index 0000000..e3171db --- /dev/null +++ b/examples/micro-patterns/src/TieredCircuitBreaker.a.sol @@ -0,0 +1,85 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +interface ILiquidationPath { + function liquidate(address account) external; +} + +interface IUserExitPath { + function withdraw(uint256 amount) external; + function redeem(uint256 shares) external; +} + +/// @notice A two-tier outflow breaker: soft breach becomes liquidation-only, hard breach stops everything. +/// @dev Protects against bank-run or exploit-style asset flight: +/// - ordinary withdrawals/redeems continuing after a rolling outflow breach; +/// - new net outflow that is not part of a configured liquidation path; +/// - catastrophic outflow that should halt all touching transactions until the window recovers. +contract TieredCircuitBreakerAssertion is Assertion { + address public immutable ASSET; + address public immutable LIQUIDATION_TARGET; + + uint256 public constant SOFT_THRESHOLD_BPS = 1_000; + uint256 public constant HARD_THRESHOLD_BPS = 3_000; + uint256 public constant WINDOW = 24 hours; + + constructor(address asset_, address liquidationTarget_) { + registerAssertionSpec(AssertionSpec.Reshiram); + ASSET = asset_; + LIQUIDATION_TARGET = liquidationTarget_; + } + + function triggers() external view override { + watchCumulativeOutflow(ASSET, SOFT_THRESHOLD_BPS, WINDOW, this.assertSoftBreaker.selector); + watchCumulativeOutflow(ASSET, HARD_THRESHOLD_BPS, WINDOW, this.assertHardBreaker.selector); + } + + function assertSoftBreaker() external view { + PhEvm.OutflowContext memory ctx = ph.outflowContext(); + require(ctx.token == ASSET, "wrong asset"); + + // Failure scenario: the vault is already in stress and a user exit would deepen the run. + require(!_hasUserExit(), "user exits blocked during outflow breach"); + + // Healing transactions such as deposits or neutral accounting updates should remain live. + if (_currentTxNetOutflow() == 0) { + return; + } + + // Failure scenario: more assets leave custody without an approved liquidation reason. + require(_hasLiquidation(), "new outflow requires liquidation"); + } + + function assertHardBreaker() external pure { + // Failure scenario: the larger outflow tier is breached, so reduce-only is no longer enough. + revert("hard outflow breaker tripped"); + } + + function _hasLiquidation() internal view returns (bool) { + return _matchingCalls(LIQUIDATION_TARGET, ILiquidationPath.liquidate.selector, 1).length != 0; + } + + function _hasUserExit() internal view returns (bool) { + address vault = ph.getAssertionAdopter(); + return _matchingCalls(vault, IUserExitPath.withdraw.selector, 1).length != 0 + || _matchingCalls(vault, IUserExitPath.redeem.selector, 1).length != 0; + } + + function _currentTxNetOutflow() internal view returns (uint256 netOutflow) { + address vault = ph.getAssertionAdopter(); + PhEvm.Erc20TransferData[] memory deltas = ph.reduceErc20BalanceDeltas(ASSET, _postTx()); + uint256 outflow; + uint256 inflow; + + for (uint256 i; i < deltas.length; ++i) { + if (deltas[i].from == vault) outflow += deltas[i].value; + if (deltas[i].to == vault) inflow += deltas[i].value; + } + + return outflow > inflow ? outflow - inflow : 0; + } +} diff --git a/examples/assertions-book/test/.gitkeep b/examples/micro-patterns/test/.gitkeep similarity index 100% rename from examples/assertions-book/test/.gitkeep rename to examples/micro-patterns/test/.gitkeep diff --git a/foundry.toml b/foundry.toml index 0c85014..ed64fbb 100644 --- a/foundry.toml +++ b/foundry.toml @@ -14,16 +14,13 @@ gas_limit = 100000000 # Include test directory test = "test" -[profile.assertions-book] -src = "examples/assertions-book/assertions/src" -test = "examples/assertions-book/test" -out = "examples/assertions-book/out" -cache_path = "examples/assertions-book/cache" -libs = ["lib"] +[profile.micro-patterns] +src = "examples/micro-patterns/src" +test = "examples/micro-patterns/test" +out = "examples/micro-patterns/out" +cache_path = "examples/micro-patterns/cache" remappings = [ - "credible-std/=src/", - "forge-std/=lib/forge-std/src/", - "openzeppelin-contracts/=lib/openzeppelin-contracts/contracts/" + "credible-std/=src/" ] [doc] From c0b933b3e51445f442cd4725da11ca20d224e65e Mon Sep 17 00:00:00 2001 From: makemake Date: Mon, 18 May 2026 13:05:36 +0200 Subject: [PATCH 2/2] Restore assertion book examples --- README.md | 5 + examples/assertions-book/README.md | 19 ++ .../src/ass1-implementation-change.a.sol | 34 +++ .../src/ass10-oracle-liveness.a.sol | 46 ++++ .../assertions/src/ass11-twap-deviation.a.sol | 62 +++++ .../src/ass12-erc4626-assets-shares.a.sol | 30 +++ .../src/ass13-erc4626-deposit-withdraw.a.sol | 54 ++++ .../src/ass14-fee-verification.a.sol | 38 +++ .../src/ass15-price-within-ticks.a.sol | 56 +++++ .../src/ass16-liquidation-health-factor.a.sol | 69 +++++ .../src/ass17-panic-state-verificatoin.a.sol | 36 +++ .../src/ass18-harvest-increases-balance.a.sol | 39 +++ .../src/ass19-tokens-borrowed-invariant.a.sol | 33 +++ .../src/ass2-erc4626-operations.a.sol | 209 ++++++++++++++++ .../assertions/src/ass20-erc20-drain.a.sol | 38 +++ .../assertions/src/ass21-ether-drain.a.sol | 54 ++++ .../src/ass22-erc20-inflow-breaker.a.sol | 38 +++ .../src/ass28-intra-tx-oracle-deviation.a.sol | 68 +++++ .../assertions/src/ass4-kyc-whitelist.a.sol | 44 ++++ .../assertions/src/ass5-owner-change.a.sol | 48 ++++ .../src/ass6-constant-product.a.sol | 33 +++ .../src/ass7-lending-health-factor.a.sol | 64 +++++ .../assertions/src/ass8-positions-sum.a.sol | 44 ++++ .../src/ass9-timelock-verification.a.sol | 38 +++ .../src/AccreditedInvestorRegistry.sol | 10 + examples/assertions-book/src/MockToken.sol | 39 +++ .../src/ass1-implementation-change.sol | 36 +++ .../src/ass10-oracle-liveness.sol | 66 +++++ .../src/ass11-twap-deviation.sol | 47 ++++ .../src/ass12-erc4626-assets-shares.sol | 70 ++++++ .../src/ass13-erc4626-deposit-withdraw.sol | 233 +++++++++++++++++ .../src/ass14-fee-verification.sol | 49 ++++ .../src/ass15-price-within-ticks.sol | 100 ++++++++ .../src/ass16-liquidation-health-factor.sol | 100 ++++++++ .../src/ass17-panic-state-verificatoin.sol | 64 +++++ .../src/ass18-harvest-increases-balance.sol | 68 +++++ .../src/ass19-tokens-borrowed-invariant.sol | 89 +++++++ .../src/ass2-erc4626-operations.sol | 235 ++++++++++++++++++ .../assertions-book/src/ass20-erc20-drain.sol | 131 ++++++++++ .../assertions-book/src/ass21-ether-drain.sol | 115 +++++++++ .../src/ass22-farcaster-message-validity.sol | 115 +++++++++ .../src/ass28-intra-tx-oracle-deviation.sol | 37 +++ .../src/ass4-only-accredited-can-mint.sol | 17 ++ .../assertions-book/src/ass5-owner-change.sol | 57 +++++ .../src/ass6-constant-product.sol | 43 ++++ .../src/ass7-lending-health-factor.sol | 68 +++++ .../src/ass8-positions-sum.sol | 49 ++++ .../src/ass9-timelock-verification.sol | 32 +++ examples/assertions-book/test/.gitkeep | 1 + foundry.toml | 12 + 50 files changed, 3082 insertions(+) create mode 100644 examples/assertions-book/README.md create mode 100644 examples/assertions-book/assertions/src/ass1-implementation-change.a.sol create mode 100644 examples/assertions-book/assertions/src/ass10-oracle-liveness.a.sol create mode 100644 examples/assertions-book/assertions/src/ass11-twap-deviation.a.sol create mode 100644 examples/assertions-book/assertions/src/ass12-erc4626-assets-shares.a.sol create mode 100644 examples/assertions-book/assertions/src/ass13-erc4626-deposit-withdraw.a.sol create mode 100644 examples/assertions-book/assertions/src/ass14-fee-verification.a.sol create mode 100644 examples/assertions-book/assertions/src/ass15-price-within-ticks.a.sol create mode 100644 examples/assertions-book/assertions/src/ass16-liquidation-health-factor.a.sol create mode 100644 examples/assertions-book/assertions/src/ass17-panic-state-verificatoin.a.sol create mode 100644 examples/assertions-book/assertions/src/ass18-harvest-increases-balance.a.sol create mode 100644 examples/assertions-book/assertions/src/ass19-tokens-borrowed-invariant.a.sol create mode 100644 examples/assertions-book/assertions/src/ass2-erc4626-operations.a.sol create mode 100644 examples/assertions-book/assertions/src/ass20-erc20-drain.a.sol create mode 100644 examples/assertions-book/assertions/src/ass21-ether-drain.a.sol create mode 100644 examples/assertions-book/assertions/src/ass22-erc20-inflow-breaker.a.sol create mode 100644 examples/assertions-book/assertions/src/ass28-intra-tx-oracle-deviation.a.sol create mode 100644 examples/assertions-book/assertions/src/ass4-kyc-whitelist.a.sol create mode 100644 examples/assertions-book/assertions/src/ass5-owner-change.a.sol create mode 100644 examples/assertions-book/assertions/src/ass6-constant-product.a.sol create mode 100644 examples/assertions-book/assertions/src/ass7-lending-health-factor.a.sol create mode 100644 examples/assertions-book/assertions/src/ass8-positions-sum.a.sol create mode 100644 examples/assertions-book/assertions/src/ass9-timelock-verification.a.sol create mode 100644 examples/assertions-book/src/AccreditedInvestorRegistry.sol create mode 100644 examples/assertions-book/src/MockToken.sol create mode 100644 examples/assertions-book/src/ass1-implementation-change.sol create mode 100644 examples/assertions-book/src/ass10-oracle-liveness.sol create mode 100644 examples/assertions-book/src/ass11-twap-deviation.sol create mode 100644 examples/assertions-book/src/ass12-erc4626-assets-shares.sol create mode 100644 examples/assertions-book/src/ass13-erc4626-deposit-withdraw.sol create mode 100644 examples/assertions-book/src/ass14-fee-verification.sol create mode 100644 examples/assertions-book/src/ass15-price-within-ticks.sol create mode 100644 examples/assertions-book/src/ass16-liquidation-health-factor.sol create mode 100644 examples/assertions-book/src/ass17-panic-state-verificatoin.sol create mode 100644 examples/assertions-book/src/ass18-harvest-increases-balance.sol create mode 100644 examples/assertions-book/src/ass19-tokens-borrowed-invariant.sol create mode 100644 examples/assertions-book/src/ass2-erc4626-operations.sol create mode 100644 examples/assertions-book/src/ass20-erc20-drain.sol create mode 100644 examples/assertions-book/src/ass21-ether-drain.sol create mode 100644 examples/assertions-book/src/ass22-farcaster-message-validity.sol create mode 100644 examples/assertions-book/src/ass28-intra-tx-oracle-deviation.sol create mode 100644 examples/assertions-book/src/ass4-only-accredited-can-mint.sol create mode 100644 examples/assertions-book/src/ass5-owner-change.sol create mode 100644 examples/assertions-book/src/ass6-constant-product.sol create mode 100644 examples/assertions-book/src/ass7-lending-health-factor.sol create mode 100644 examples/assertions-book/src/ass8-positions-sum.sol create mode 100644 examples/assertions-book/src/ass9-timelock-verification.sol create mode 100644 examples/assertions-book/test/.gitkeep diff --git a/README.md b/README.md index b284d9d..3d38efd 100644 --- a/README.md +++ b/README.md @@ -6,6 +6,11 @@ Standard library for implementing assertions in the Phylax Credible Layer (PCL). Full API documentation is available at: https://phylaxsystems.github.io/credible-std +## Examples + +Assertion Book examples live in `examples/assertions-book`; micro-pattern examples +live in `examples/micro-patterns`. + ## Installation ### Using Foundry (Recommended) diff --git a/examples/assertions-book/README.md b/examples/assertions-book/README.md new file mode 100644 index 0000000..c7792d8 --- /dev/null +++ b/examples/assertions-book/README.md @@ -0,0 +1,19 @@ +# Assertions Book Examples + +This directory is the canonical source for Assertions Book code examples. + +| Directory | Contents | +| --------- | -------- | +| `assertions/src` | Assertion contracts imported into `phylax-docs/snippets` | +| `src` | Mock protocols and helper contracts used by those assertions | +| `test` | Reserved for focused example tests | + +Before changing the docs snippets directly, update the matching Solidity file in +`assertions/src` and confirm the example profile still builds: + +```bash +FOUNDRY_PROFILE=assertions-book forge build +``` + +After the change lands, run the `Import Credible Std Assertion Examples` +workflow in `phylaxsystems/phylax-docs` to refresh the docs snippets. diff --git a/examples/assertions-book/assertions/src/ass1-implementation-change.a.sol b/examples/assertions-book/assertions/src/ass1-implementation-change.a.sol new file mode 100644 index 0000000..862c934 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass1-implementation-change.a.sol @@ -0,0 +1,34 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract ImplementationChangeAssertion is Assertion { + bytes32 internal constant IMPLEMENTATION_SLOT = bytes32(uint256(0)); + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerTxEndTrigger(this.implementationChange.selector); + } + + /// @notice Checks that the implementation slot is unchanged across the transaction. + function implementationChange() external view { + address adopter = ph.getAssertionAdopter(); + PhEvm.ForkId memory preFork = _preTx(); + PhEvm.ForkId memory postFork = _postTx(); + + address preImpl = _loadAddressAt(adopter, IMPLEMENTATION_SLOT, preFork); + address postImpl = _loadAddressAt(adopter, IMPLEMENTATION_SLOT, postFork); + + require(preImpl == postImpl, "Implementation changed"); + } + + function _loadAddressAt(address target, bytes32 slot, PhEvm.ForkId memory fork) internal view returns (address) { + return address(uint160(uint256(ph.loadStateAt(target, slot, fork)))); + } +} diff --git a/examples/assertions-book/assertions/src/ass10-oracle-liveness.a.sol b/examples/assertions-book/assertions/src/ass10-oracle-liveness.a.sol new file mode 100644 index 0000000..430e65f --- /dev/null +++ b/examples/assertions-book/assertions/src/ass10-oracle-liveness.a.sol @@ -0,0 +1,46 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract OracleLivenessAssertion is Assertion { + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + // Maximum time window (in seconds) that oracle data can be considered fresh + // This is a constant that should be adjusted based on the protocol's requirements + uint256 public constant MAX_UPDATE_WINDOW = 10 minutes; + + function triggers() external view override { + // Register trigger for the swap function which relies on oracle data + registerFnCallTrigger(this.assertionOracleLiveness.selector, IDex.swap.selector); + } + + // Assert that the oracle has been updated within the specified time window + function assertionOracleLiveness() external { + // Get the assertion adopter address + IDex adopter = IDex(ph.getAssertionAdopter()); + + // Get the current state to check the oracle's last update time + PhEvm.ForkId memory postFork = _postTx(); + + // Check if the oracle has been updated within the maximum allowed window + uint256 lastUpdateTime = IOracle(adopter.oracle()).lastUpdated(); + uint256 currentTime = block.timestamp; + + // Verify the oracle data is fresh (updated within the time window) + require(currentTime - lastUpdateTime <= MAX_UPDATE_WINDOW, "Oracle not updated within the allowed time window"); + } +} + +interface IOracle { + function lastUpdated() external view returns (uint256); +} + +interface IDex { + function swap(address tokenIn, address tokenOut, uint256 amountIn) external returns (uint256); + function oracle() external view returns (IOracle); +} diff --git a/examples/assertions-book/assertions/src/ass11-twap-deviation.a.sol b/examples/assertions-book/assertions/src/ass11-twap-deviation.a.sol new file mode 100644 index 0000000..264b742 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass11-twap-deviation.a.sol @@ -0,0 +1,62 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract TwapDeviationAssertion is Assertion { + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + // Register trigger for changes to the current price + // We assume that the price is stored in storage slot 0 + registerTxEndTrigger(this.assertionTwapDeviation.selector); + } + + // Assert that the current price doesn't deviate more than 5% from the TWAP price + function assertionTwapDeviation() external { + // Get the assertion adopter address + IPool adopter = IPool(ph.getAssertionAdopter()); + + // Get TWAP price before the transaction (our reference point) + PhEvm.ForkId memory preFork = _preTx(); + uint256 preTwapPrice = adopter.twap(); + + // Get price after the transaction + PhEvm.ForkId memory postFork = _postTx(); + uint256 postPrice = adopter.price(); + + uint256 maxDeviation = 5; + + // First check: Compare post-transaction price against pre-transaction TWAP + uint256 deviation = calculateDeviation(preTwapPrice, postPrice); + require(deviation <= maxDeviation, "Price deviation from TWAP exceeds maximum allowed"); + + // Second check: If the simple check passes, inspect all price changes in the callstack + // This is more expensive but catches manipulation attempts within the transaction + uint256[] memory priceChanges = getStateChangesUint( + address(adopter), + bytes32(uint256(0)) // Current price storage slot + ); + + // Check each price change against the pre-transaction TWAP + for (uint256 i = 0; i < priceChanges.length; i++) { + deviation = calculateDeviation(preTwapPrice, priceChanges[i]); + require(deviation <= maxDeviation, "Price deviation from TWAP exceeds maximum allowed"); + } + } + + // Helper function to calculate percentage deviation + function calculateDeviation(uint256 referencePrice, uint256 currentPrice) internal pure returns (uint256) { + return (((currentPrice > referencePrice) ? currentPrice - referencePrice : referencePrice - currentPrice) * 100) + / referencePrice; + } +} + +interface IPool { + function price() external view returns (uint256); + function twap() external view returns (uint256); +} diff --git a/examples/assertions-book/assertions/src/ass12-erc4626-assets-shares.a.sol b/examples/assertions-book/assertions/src/ass12-erc4626-assets-shares.a.sol new file mode 100644 index 0000000..d15c3fc --- /dev/null +++ b/examples/assertions-book/assertions/src/ass12-erc4626-assets-shares.a.sol @@ -0,0 +1,30 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract ERC4626AssetsSharesAssertion is Assertion { + bytes32 internal constant TOTAL_ASSETS_SLOT = bytes32(uint256(0)); + bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(1)); + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerTxEndTrigger(this.assertionAssetsShares.selector); + } + + /// @notice Checks that stored total assets are sufficient to back stored total shares. + function assertionAssetsShares() external view { + address vault = ph.getAssertionAdopter(); + PhEvm.ForkId memory postFork = _postTx(); + + uint256 totalAssets = uint256(ph.loadStateAt(vault, TOTAL_ASSETS_SLOT, postFork)); + uint256 totalSupply = uint256(ph.loadStateAt(vault, TOTAL_SUPPLY_SLOT, postFork)); + + require(totalAssets >= totalSupply, "Not enough assets to back all shares"); + } +} diff --git a/examples/assertions-book/assertions/src/ass13-erc4626-deposit-withdraw.a.sol b/examples/assertions-book/assertions/src/ass13-erc4626-deposit-withdraw.a.sol new file mode 100644 index 0000000..eb9fdb7 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass13-erc4626-deposit-withdraw.a.sol @@ -0,0 +1,54 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract ERC4626DepositWithdrawAssertion is Assertion { + bytes32 internal constant TOTAL_ASSETS_SLOT = bytes32(uint256(0)); + bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(1)); + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerFnCallTrigger(this.assertDepositPreservesSharePrice.selector, IERC4626.deposit.selector); + registerFnCallTrigger(this.assertWithdrawPreservesSharePrice.selector, IERC4626.withdraw.selector); + } + + /// @notice Checks that a deposit does not dilute existing shares. + function assertDepositPreservesSharePrice() external view { + PhEvm.TriggerContext memory ctx = ph.context(); + _assertSharePriceNotReduced(ctx.callStart, ctx.callEnd, "ERC4626: deposit diluted shares"); + } + + /// @notice Checks that a withdrawal does not dilute remaining shares. + function assertWithdrawPreservesSharePrice() external view { + PhEvm.TriggerContext memory ctx = ph.context(); + _assertSharePriceNotReduced(ctx.callStart, ctx.callEnd, "ERC4626: withdrawal diluted shares"); + } + + function _assertSharePriceNotReduced(uint256 callStart, uint256 callEnd, string memory reason) internal view { + address vault = ph.getAssertionAdopter(); + PhEvm.ForkId memory preCall = PhEvm.ForkId({forkType: 2, callIndex: callStart}); + PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: callEnd}); + + uint256 preAssets = uint256(ph.loadStateAt(vault, TOTAL_ASSETS_SLOT, preCall)); + uint256 preSupply = uint256(ph.loadStateAt(vault, TOTAL_SUPPLY_SLOT, preCall)); + uint256 postAssets = uint256(ph.loadStateAt(vault, TOTAL_ASSETS_SLOT, postCall)); + uint256 postSupply = uint256(ph.loadStateAt(vault, TOTAL_SUPPLY_SLOT, postCall)); + + if (preSupply == 0 || postSupply == 0) { + return; + } + + require(postAssets * preSupply >= preAssets * postSupply, reason); + } +} + +interface IERC4626 { + function deposit(uint256 assets, address receiver) external returns (uint256 shares); + function withdraw(uint256 assets, address receiver, address owner) external returns (uint256 shares); +} diff --git a/examples/assertions-book/assertions/src/ass14-fee-verification.a.sol b/examples/assertions-book/assertions/src/ass14-fee-verification.a.sol new file mode 100644 index 0000000..019dc44 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass14-fee-verification.a.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract AmmFeeVerificationAssertion is Assertion { + bytes32 internal constant FEE_SLOT = bytes32(uint256(1)); + bytes32 internal constant STABLE_SLOT = bytes32(uint256(2)); + + uint256 private constant STABLE_POOL_FEE_1 = 1; + uint256 private constant STABLE_POOL_FEE_2 = 15; + uint256 private constant NON_STABLE_POOL_FEE_1 = 25; + uint256 private constant NON_STABLE_POOL_FEE_2 = 30; + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerTxEndTrigger(this.assertFeeVerification.selector); + } + + /// @notice Checks that the post-transaction fee is one of the allowed values. + function assertFeeVerification() external view { + address pool = ph.getAssertionAdopter(); + PhEvm.ForkId memory postFork = _postTx(); + + bool isStable = uint256(ph.loadStateAt(pool, STABLE_SLOT, postFork)) != 0; + uint256 newFee = uint256(ph.loadStateAt(pool, FEE_SLOT, postFork)); + bool isAllowed = isStable + ? (newFee == STABLE_POOL_FEE_1 || newFee == STABLE_POOL_FEE_2) + : (newFee == NON_STABLE_POOL_FEE_1 || newFee == NON_STABLE_POOL_FEE_2); + + require(isAllowed, "Fee change to unauthorized value"); + } +} diff --git a/examples/assertions-book/assertions/src/ass15-price-within-ticks.a.sol b/examples/assertions-book/assertions/src/ass15-price-within-ticks.a.sol new file mode 100644 index 0000000..b508834 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass15-price-within-ticks.a.sol @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract PriceWithinTicksAssertion is Assertion { + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + // Uniswap V3 tick bounds + int24 constant MIN_TICK = -887272; + int24 constant MAX_TICK = 887272; + + function triggers() external view override { + // Register trigger for changes to the tick storage slot + // Assumes tick is stored in slot0 of the pool contract + registerTxEndTrigger(this.priceWithinTicks.selector); + } + + // Check that the price is within the tick bounds and that the tick is divisible by the tick spacing + function priceWithinTicks() external { + // Get the assertion adopter address + IUniswapV3Pool adopter = IUniswapV3Pool(ph.getAssertionAdopter()); + + // Get post-swap state + PhEvm.ForkId memory postFork = _postTx(); + (, int24 postTick,,,,,) = adopter.slot0(); + int24 spacing = adopter.tickSpacing(); + + // Check 1: Tick must be within global bounds + require(postTick >= MIN_TICK && postTick <= MAX_TICK, "Tick outside global bounds"); + + // Check 2: Tick must be divisible by tickSpacing + require(postTick % spacing == 0, "Tick not aligned with spacing"); + } +} + +// Uniswap v3 pool style interface +interface IUniswapV3Pool { + function slot0() + external + view + returns ( + uint160 sqrtPriceX96, + int24 tick, + uint16 observationIndex, + uint16 observationCardinality, + uint16 observationCardinalityNext, + uint8 feeProtocol, + bool unlocked + ); + function tickSpacing() external view returns (int24); +} diff --git a/examples/assertions-book/assertions/src/ass16-liquidation-health-factor.a.sol b/examples/assertions-book/assertions/src/ass16-liquidation-health-factor.a.sol new file mode 100644 index 0000000..8a7591d --- /dev/null +++ b/examples/assertions-book/assertions/src/ass16-liquidation-health-factor.a.sol @@ -0,0 +1,69 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract LiquidationHealthFactorAssertion is Assertion { + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + // Simple health factor constants (no scaling) + uint256 constant LIQUIDATION_THRESHOLD = 100; // Below this = liquidatable + uint256 constant MIN_HEALTH_FACTOR = 120; // Minimum safe health factor after liquidation + + function triggers() external view override { + // Register trigger for liquidation function calls + registerFnCallTrigger(this.assertHealthFactor.selector, ILendingProtocol.liquidate.selector); + } + + // Check that liquidation can't happen if the position is healthy + // Check that the health factor is improved after liquidation + function assertHealthFactor() external { + // Get the assertion adopter address + ILendingProtocol adopter = ILendingProtocol(ph.getAssertionAdopter()); + + // Get all liquidation calls in the transaction + PhEvm.CallInputs[] memory callInputs = ph.getAllCallInputs(address(adopter), adopter.liquidate.selector); + + for (uint256 i = 0; i < callInputs.length; i++) { + address borrower; + uint256 seizedAssets; + uint256 repaidDebt; + + // Decode liquidation parameters + (borrower, seizedAssets, repaidDebt) = abi.decode(callInputs[i].input, (address, uint256, uint256)); + + // Validate liquidation amounts + require(seizedAssets > 0, "Zero assets seized"); + require(repaidDebt > 0, "Zero debt repaid"); + + // Check health factor before liquidation + PhEvm.ForkId memory preCallFork = PhEvm.ForkId({forkType: 2, callIndex: callInputs[i].id}); + uint256 preHealthFactor = adopter.healthFactor(borrower); + require(preHealthFactor <= LIQUIDATION_THRESHOLD, "Account not eligible for liquidation"); + + // Check health factor after liquidation + PhEvm.ForkId memory postCallFork = PhEvm.ForkId({forkType: 3, callIndex: callInputs[i].id}); + uint256 postHealthFactor = adopter.healthFactor(borrower); + + // Verify the liquidation actually improved the position's health + require(postHealthFactor > preHealthFactor, "Health factor did not improve after liquidation"); + + // Ensure the position is now in a safe state above the minimum required health factor + require(postHealthFactor >= MIN_HEALTH_FACTOR, "Position still unhealthy after liquidation"); + } + } +} + +// Simplified lending protocol interface +interface ILendingProtocol { + function liquidate(address borrower, uint256 seizedAssets, uint256 repaidDebt) + external + returns (uint256, uint256); + + function isHealthy(address user) external view returns (bool); + function healthFactor(address user) external view returns (uint256); +} diff --git a/examples/assertions-book/assertions/src/ass17-panic-state-verificatoin.a.sol b/examples/assertions-book/assertions/src/ass17-panic-state-verificatoin.a.sol new file mode 100644 index 0000000..f63174b --- /dev/null +++ b/examples/assertions-book/assertions/src/ass17-panic-state-verificatoin.a.sol @@ -0,0 +1,36 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract EmergencyStateAssertion is Assertion { + bytes32 internal constant PAUSED_SLOT = bytes32(uint256(0)); + bytes32 internal constant BALANCE_SLOT = bytes32(uint256(1)); + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerTxEndTrigger(this.assertionPanickedCanOnlyDecreaseBalance.selector); + } + + /// @notice Checks that a paused protocol cannot increase its stored balance. + function assertionPanickedCanOnlyDecreaseBalance() external view { + address adopter = ph.getAssertionAdopter(); + PhEvm.ForkId memory preFork = _preTx(); + PhEvm.ForkId memory postFork = _postTx(); + + bool wasPaused = uint256(ph.loadStateAt(adopter, PAUSED_SLOT, preFork)) != 0; + if (!wasPaused) { + return; + } + + uint256 preBalance = uint256(ph.loadStateAt(adopter, BALANCE_SLOT, preFork)); + uint256 postBalance = uint256(ph.loadStateAt(adopter, BALANCE_SLOT, postFork)); + + require(postBalance <= preBalance, "Balance can only decrease when panicked"); + } +} diff --git a/examples/assertions-book/assertions/src/ass18-harvest-increases-balance.a.sol b/examples/assertions-book/assertions/src/ass18-harvest-increases-balance.a.sol new file mode 100644 index 0000000..fc3ddbf --- /dev/null +++ b/examples/assertions-book/assertions/src/ass18-harvest-increases-balance.a.sol @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract BeefyHarvestAssertion is Assertion { + bytes32 internal constant BALANCE_SLOT = bytes32(uint256(0)); + bytes32 internal constant PRICE_PER_SHARE_SLOT = bytes32(uint256(1)); + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerFnCallTrigger(this.assertionHarvestIncreasesBalance.selector, IBeefyVault.harvest.selector); + } + + /// @notice Checks that a harvest does not reduce vault balance or price per share. + function assertionHarvestIncreasesBalance() external view { + address vault = ph.getAssertionAdopter(); + PhEvm.TriggerContext memory ctx = ph.context(); + PhEvm.ForkId memory preCall = PhEvm.ForkId({forkType: 2, callIndex: ctx.callStart}); + PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd}); + + uint256 preBalance = uint256(ph.loadStateAt(vault, BALANCE_SLOT, preCall)); + uint256 postBalance = uint256(ph.loadStateAt(vault, BALANCE_SLOT, postCall)); + uint256 prePricePerShare = uint256(ph.loadStateAt(vault, PRICE_PER_SHARE_SLOT, preCall)); + uint256 postPricePerShare = uint256(ph.loadStateAt(vault, PRICE_PER_SHARE_SLOT, postCall)); + + require(postBalance >= preBalance, "Harvest decreased balance"); + require(postPricePerShare >= prePricePerShare, "Price per share decreased after harvest"); + } +} + +interface IBeefyVault { + function harvest(bool badHarvest) external; +} diff --git a/examples/assertions-book/assertions/src/ass19-tokens-borrowed-invariant.a.sol b/examples/assertions-book/assertions/src/ass19-tokens-borrowed-invariant.a.sol new file mode 100644 index 0000000..f28f497 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass19-tokens-borrowed-invariant.a.sol @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract TokensBorrowedInvariant is Assertion { + bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(0)); + bytes32 internal constant TOTAL_BORROW_SLOT = bytes32(uint256(1)); + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerTxEndTrigger(this.assertBorrowedInvariant.selector); + } + + /// @notice Checks that total supplied assets cover total borrowed assets after the transaction. + function assertBorrowedInvariant() external view { + address market = ph.getAssertionAdopter(); + PhEvm.ForkId memory postFork = _postTx(); + + uint256 totalSupplyAsset = uint256(ph.loadStateAt(market, TOTAL_SUPPLY_SLOT, postFork)); + uint256 totalBorrowedAsset = uint256(ph.loadStateAt(market, TOTAL_BORROW_SLOT, postFork)); + + require( + totalSupplyAsset >= totalBorrowedAsset, + "INVARIANT VIOLATION: Total supply of assets is less than total borrowed assets" + ); + } +} diff --git a/examples/assertions-book/assertions/src/ass2-erc4626-operations.a.sol b/examples/assertions-book/assertions/src/ass2-erc4626-operations.a.sol new file mode 100644 index 0000000..f9934fa --- /dev/null +++ b/examples/assertions-book/assertions/src/ass2-erc4626-operations.a.sol @@ -0,0 +1,209 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title ERC4626OperationsAssertion + * @notice This assertion contract validates the correctness of ERC4626 vault operations by checking: + * + * 1. Batch Operations Consistency: + * - Validates that all ERC4626 operations (deposit, mint, withdraw, redeem) maintain correct + * accounting of total assets and total supply + * - Ensures that the net changes in assets and shares match the expected changes + * - Handles multiple operations in a single transaction + * + * 2. Deposit Operation Validation: + * - Verifies that deposit operations correctly increase the vault's asset balance + * - Ensures depositors receive the correct number of shares based on previewDeposit + * - Validates that the vault's total assets increase by exactly the deposited amount + * + * 3. Base Invariants: + * - Ensures the vault always has at least as many assets as shares + * - Validates this invariant after any storage changes + * + * The contract uses the Credible Layer's fork mechanism to compare pre and post-state + * changes, ensuring that all operations maintain the vault's accounting integrity. + */ +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {CoolVault} from "../../src/ass2-erc4626-operations.sol"; +import {IERC4626} from "openzeppelin-contracts/interfaces/IERC4626.sol"; +import {IERC20} from "openzeppelin-contracts/token/ERC20/IERC20.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract ERC4626OperationsAssertion is Assertion { + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + // The triggers function tells the Credible Layer which assertion functions to run + function triggers() external view override { + // Batch operations assertion - triggers on any of the four functions + registerFnCallTrigger(this.assertionBatchOperationsConsistency.selector, CoolVault.deposit.selector); + registerFnCallTrigger(this.assertionBatchOperationsConsistency.selector, CoolVault.mint.selector); + registerFnCallTrigger(this.assertionBatchOperationsConsistency.selector, CoolVault.withdraw.selector); + registerFnCallTrigger(this.assertionBatchOperationsConsistency.selector, CoolVault.redeem.selector); + + // Deposit-specific assertions + registerFnCallTrigger(this.assertionDepositIncreasesBalance.selector, CoolVault.deposit.selector); + registerFnCallTrigger(this.assertionDepositerSharesIncreases.selector, CoolVault.deposit.selector); + + // Base invariant assertion - triggers on storage changes + registerTxEndTrigger(this.assertionVaultAlwaysAccumulatesAssets.selector); + } + + /** + * @dev Comprehensive assertion for batch operations: validates that all ERC4626 operations + * in a single transaction maintain consistency across total supply and total assets + * This function checks all four operations (deposit, mint, withdraw, redeem) that may occur + * within the same transaction and ensures the final state is mathematically correct + */ + function assertionBatchOperationsConsistency() external { + // Get the assertion adopter address + CoolVault adopter = CoolVault(ph.getAssertionAdopter()); + + // Get call inputs for all four functions + PhEvm.CallInputs[] memory depositInputs = ph.getCallInputs(address(adopter), adopter.deposit.selector); + PhEvm.CallInputs[] memory mintInputs = ph.getCallInputs(address(adopter), adopter.mint.selector); + PhEvm.CallInputs[] memory withdrawInputs = ph.getCallInputs(address(adopter), adopter.withdraw.selector); + PhEvm.CallInputs[] memory redeemInputs = ph.getCallInputs(address(adopter), adopter.redeem.selector); + + // Calculate net changes from all operations + uint256 totalAssetsAdded = 0; + uint256 totalAssetsRemoved = 0; + uint256 totalSharesAdded = 0; + uint256 totalSharesRemoved = 0; + + // Process deposit operations (increase assets and supply) + for (uint256 i = 0; i < depositInputs.length; i++) { + (uint256 assets,) = abi.decode(depositInputs[i].input, (uint256, address)); + totalAssetsAdded += assets; + totalSharesAdded += adopter.previewDeposit(assets); + } + + // Process mint operations (increase assets and supply) + for (uint256 i = 0; i < mintInputs.length; i++) { + (uint256 shares,) = abi.decode(mintInputs[i].input, (uint256, address)); + totalSharesAdded += shares; + totalAssetsAdded += adopter.previewMint(shares); + } + + // Process withdraw operations (decrease assets and supply) + for (uint256 i = 0; i < withdrawInputs.length; i++) { + (uint256 assets,,) = abi.decode(withdrawInputs[i].input, (uint256, address, address)); + totalAssetsRemoved += assets; + totalSharesRemoved += adopter.previewWithdraw(assets); + } + + // Process redeem operations (decrease assets and supply) + for (uint256 i = 0; i < redeemInputs.length; i++) { + (uint256 shares,,) = abi.decode(redeemInputs[i].input, (uint256, address, address)); + totalSharesRemoved += shares; + totalAssetsRemoved += adopter.previewRedeem(shares); + } + + PhEvm.ForkId memory preFork = _preTx(); + uint256 preVaultAssets = adopter.totalAssets(); + uint256 preVaultSupply = adopter.totalSupply(); + + PhEvm.ForkId memory postFork = _postTx(); + uint256 postVaultAssets = adopter.totalAssets(); + uint256 postVaultSupply = adopter.totalSupply(); + + // Calculate expected changes + uint256 expectedAssetsAdded = postVaultAssets > preVaultAssets ? postVaultAssets - preVaultAssets : 0; + uint256 expectedAssetsRemoved = preVaultAssets > postVaultAssets ? preVaultAssets - postVaultAssets : 0; + uint256 expectedSharesAdded = postVaultSupply > preVaultSupply ? postVaultSupply - preVaultSupply : 0; + uint256 expectedSharesRemoved = preVaultSupply > postVaultSupply ? preVaultSupply - postVaultSupply : 0; + + // Ensure operations had some effect if there were calls + require(totalAssetsAdded == expectedAssetsAdded, "Batch Operations: Assets added mismatch"); + require(totalAssetsRemoved == expectedAssetsRemoved, "Batch Operations: Assets removed mismatch"); + require(totalSharesAdded == expectedSharesAdded, "Batch Operations: Shares added mismatch"); + require(totalSharesRemoved == expectedSharesRemoved, "Batch Operations: Shares removed mismatch"); + } + + /** + * @dev Assertion to verify that deposit operations correctly increase the vault's asset balance + * This ensures that when users deposit assets, the vault's total assets increase by exactly the deposited amount + */ + function assertionDepositIncreasesBalance() external { + // Get the assertion adopter address + CoolVault adopter = CoolVault(ph.getAssertionAdopter()); + + // Get all deposit calls to the vault + PhEvm.CallInputs[] memory inputs = ph.getCallInputs(address(adopter), adopter.deposit.selector); + + for (uint256 i = 0; i < inputs.length; i++) { + (uint256 assets, address receiver) = abi.decode(inputs[i].input, (uint256, address)); + + // Check pre-state + PhEvm.ForkId memory preFork = _preTx(); + uint256 vaultAssetPreBalance = adopter.totalAssets(); + uint256 userSharesPreBalance = adopter.balanceOf(receiver); + uint256 expectedShares = adopter.previewDeposit(assets); + + // Check post-state + PhEvm.ForkId memory postFork = _postTx(); + uint256 vaultAssetPostBalance = adopter.totalAssets(); + uint256 userSharesPostBalance = adopter.balanceOf(receiver); + + // Verify vault assets increased by exactly the deposited amount + require( + vaultAssetPostBalance == vaultAssetPreBalance + assets, + "Deposit assertion failed: Vault assets did not increase by the correct amount" + ); + + // Verify user received exactly the expected number of shares + require( + userSharesPostBalance == userSharesPreBalance + expectedShares, + "Deposit assertion failed: User did not receive the correct number of shares" + ); + } + } + + /** + * @dev Assertion to verify that deposit operations correctly increase the depositor's share balance + * This ensures that when users deposit assets, they receive the correct number of shares + */ + function assertionDepositerSharesIncreases() external { + // Get the assertion adopter address + CoolVault adopter = CoolVault(ph.getAssertionAdopter()); + + PhEvm.CallInputs[] memory inputs = ph.getCallInputs(address(adopter), adopter.deposit.selector); + + for (uint256 i = 0; i < inputs.length; i++) { + PhEvm.ForkId memory preFork = _preTx(); + (uint256 assets,) = abi.decode(inputs[i].input, (uint256, address)); + uint256 previewPreAssets = adopter.previewDeposit(assets); + address depositer = inputs[0].caller; + uint256 preShares = adopter.balanceOf(depositer); + + PhEvm.ForkId memory postFork = _postTx(); + + uint256 postShares = adopter.balanceOf(depositer); + + require( + postShares == preShares + previewPreAssets, + "Depositer shares assertion failed: Share balance did not increase correctly" + ); + } + } + + /** + * @dev Base invariant assertion to verify that the vault always has at least as many assets as shares + * This is a fundamental invariant of ERC4626 vaults - they should never have more shares than assets + */ + function assertionVaultAlwaysAccumulatesAssets() external { + // Get the assertion adopter address + CoolVault adopter = CoolVault(ph.getAssertionAdopter()); + + PhEvm.ForkId memory postFork = _postTx(); + + uint256 vaultAssetPostBalance = adopter.totalAssets(); + uint256 vaultSharesPostBalance = adopter.balanceOf(address(adopter)); + + require( + vaultAssetPostBalance >= vaultSharesPostBalance, "Base invariant failed: Vault has more shares than assets" + ); + } +} diff --git a/examples/assertions-book/assertions/src/ass20-erc20-drain.a.sol b/examples/assertions-book/assertions/src/ass20-erc20-drain.a.sol new file mode 100644 index 0000000..98c9a38 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass20-erc20-drain.a.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract ERC20CumulativeOutflowBreakerAssertion is Assertion { + address public immutable monitoredToken; + uint256 public immutable outflowThresholdBps; + uint256 public immutable outflowWindowDuration; + + constructor(address monitoredToken_, uint256 outflowThresholdBps_, uint256 outflowWindowDuration_) { + registerAssertionSpec(AssertionSpec.Reshiram); + + monitoredToken = monitoredToken_; + outflowThresholdBps = outflowThresholdBps_; + outflowWindowDuration = outflowWindowDuration_; + } + + function triggers() external view override { + watchCumulativeOutflow( + monitoredToken, + outflowThresholdBps, + outflowWindowDuration, + this.assertCumulativeOutflow.selector + ); + } + + /// @notice Reverts when cumulative token outflow breaches the rolling-window limit. + /// @dev The Reshiram trigger tracks the window and calls this function only after breach. + function assertCumulativeOutflow() external view { + PhEvm.OutflowContext memory ctx = ph.outflowContext(); + require(ctx.token == monitoredToken, "ERC20Outflow: wrong token context"); + + revert("ERC20Outflow: cumulative outflow breaker tripped"); + } +} diff --git a/examples/assertions-book/assertions/src/ass21-ether-drain.a.sol b/examples/assertions-book/assertions/src/ass21-ether-drain.a.sol new file mode 100644 index 0000000..fe0015f --- /dev/null +++ b/examples/assertions-book/assertions/src/ass21-ether-drain.a.sol @@ -0,0 +1,54 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract EtherDrainAssertion is Assertion { + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + // Maximum percentage of ETH that can be drained in a single transaction (10% by default) + uint256 public constant MAX_DRAIN_PERCENTAGE = 10; + + function triggers() external view override { + // Register a trigger that activates when the ETH balance of the monitored contract changes + registerTxEndTrigger(this.assertionEtherDrain.selector); + } + + // Combined assertion for ETH drain with whitelist logic + function assertionEtherDrain() external { + // Get the assertion adopter address (this is the contract we're monitoring) + address exampleContract = ph.getAssertionAdopter(); + + // Capture the ETH balance before transaction execution + PhEvm.ForkId memory preFork = _preTx(); + uint256 preBalance = address(exampleContract).balance; + + // Capture the ETH balance after transaction execution + PhEvm.ForkId memory postFork = _postTx(); + uint256 postBalance = address(exampleContract).balance; + + // Only check for drainage (we don't care about ETH being added) + if (preBalance > postBalance) { + // Calculate the amount drained and the maximum allowed drain + uint256 drainAmount = preBalance - postBalance; + uint256 maxAllowedDrain = (preBalance * MAX_DRAIN_PERCENTAGE) / 100; + + // If drain amount is within allowed limit, allow the transaction + if (drainAmount <= maxAllowedDrain) { + return; // Small drain, no need to check whitelist + } + + // For large drains, we would need to check whitelist + // Since we can't easily access constructor parameters in the new interface, + // we'll use a simplified approach that just checks the drain percentage + // In a real implementation, this would be more sophisticated + revert("Large ETH drain detected - exceeds allowed percentage"); + } + } +} + +interface IExampleContract {} diff --git a/examples/assertions-book/assertions/src/ass22-erc20-inflow-breaker.a.sol b/examples/assertions-book/assertions/src/ass22-erc20-inflow-breaker.a.sol new file mode 100644 index 0000000..a8a4b30 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass22-erc20-inflow-breaker.a.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract ERC20CumulativeInflowBreakerAssertion is Assertion { + address public immutable monitoredToken; + uint256 public immutable inflowThresholdBps; + uint256 public immutable inflowWindowDuration; + + constructor(address monitoredToken_, uint256 inflowThresholdBps_, uint256 inflowWindowDuration_) { + registerAssertionSpec(AssertionSpec.Reshiram); + + monitoredToken = monitoredToken_; + inflowThresholdBps = inflowThresholdBps_; + inflowWindowDuration = inflowWindowDuration_; + } + + function triggers() external view override { + watchCumulativeInflow( + monitoredToken, + inflowThresholdBps, + inflowWindowDuration, + this.assertCumulativeInflow.selector + ); + } + + /// @notice Reverts when cumulative token inflow breaches the rolling-window limit. + /// @dev The Reshiram trigger tracks the window and calls this function only after breach. + function assertCumulativeInflow() external view { + PhEvm.InflowContext memory ctx = ph.inflowContext(); + require(ctx.token == monitoredToken, "ERC20Inflow: wrong token context"); + + revert("ERC20Inflow: cumulative inflow breaker tripped"); + } +} diff --git a/examples/assertions-book/assertions/src/ass28-intra-tx-oracle-deviation.a.sol b/examples/assertions-book/assertions/src/ass28-intra-tx-oracle-deviation.a.sol new file mode 100644 index 0000000..3bc0545 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass28-intra-tx-oracle-deviation.a.sol @@ -0,0 +1,68 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract IntraTxOracleDeviationAssertion is Assertion { + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + // Maximum allowed price deviation (10% by default) + uint256 public constant MAX_DEVIATION_PERCENTAGE = 10; + + function triggers() external view override { + // Register trigger for oracle price update calls + registerFnCallTrigger(this.assertOracleDeviation.selector, IOracle.updatePrice.selector); + } + + // Check that price updates don't deviate more than the allowed percentage + // from the initial price at any point during the transaction + function assertOracleDeviation() external { + // Get the assertion adopter address + IOracle adopter = IOracle(ph.getAssertionAdopter()); + + // Start with a simple check comparing pre and post state + PhEvm.ForkId memory preFork = _preTx(); + uint256 prePrice = adopter.price(); + + // Calculate allowed deviation thresholds (10% by default) + uint256 maxAllowedPrice = (prePrice * (100 + MAX_DEVIATION_PERCENTAGE)) / 100; + uint256 minAllowedPrice = (prePrice * (100 - MAX_DEVIATION_PERCENTAGE)) / 100; + + // First check post-state price + PhEvm.ForkId memory postFork = _postTx(); + uint256 postPrice = adopter.price(); + + // Verify post-state price is within allowed deviation from initial price + require( + postPrice >= minAllowedPrice && postPrice <= maxAllowedPrice, + "Oracle post-state price deviation exceeds threshold" + ); + + // Get all price update calls in this transaction + // Since this assertion is triggered by updatePrice calls, we know there's at least one + PhEvm.CallInputs[] memory priceUpdates = ph.getCallInputs(address(adopter), adopter.updatePrice.selector); + + // Check each price update to ensure none deviate more than allowed from initial price + for (uint256 i = 0; i < priceUpdates.length; i++) { + PhEvm.ForkId memory postCallFork = PhEvm.ForkId({forkType: 3, callIndex: priceUpdates[i].id}); + + // Call the price function at the given frame in the call stack + uint256 updatedPrice = adopter.price(); + + // Verify each update is within allowed deviation from initial pre-state price + require( + updatedPrice >= minAllowedPrice && updatedPrice <= maxAllowedPrice, + "Oracle intra-tx price deviation exceeds threshold" + ); + } + } +} + +interface IOracle { + function updatePrice(uint256 price) external; + function price() external view returns (uint256); +} diff --git a/examples/assertions-book/assertions/src/ass4-kyc-whitelist.a.sol b/examples/assertions-book/assertions/src/ass4-kyc-whitelist.a.sol new file mode 100644 index 0000000..f0ce918 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass4-kyc-whitelist.a.sol @@ -0,0 +1,44 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; +import {OnlyAccreditedCanMint} from "../../src/ass4-only-accredited-can-mint.sol"; +import {AccreditedInvestorRegistry} from "../../src/AccreditedInvestorRegistry.sol"; + +contract OnlyAccreditedCanMintAssertion is Assertion { + AccreditedInvestorRegistry public immutable registry; + + constructor(address registry_) { + registerAssertionSpec(AssertionSpec.Reshiram); + registry = AccreditedInvestorRegistry(registry_); + } + + function triggers() external view override { + registerFnCallTrigger(this.assertOnlyAccreditedMint.selector, OnlyAccreditedCanMint.mint.selector); + registerFnCallTrigger(this.assertOnlyAccreditedTransfer.selector, OnlyAccreditedCanMint.transfer.selector); + } + + /// @notice Checks that the caller of `mint` is accredited. + function assertOnlyAccreditedMint() external view { + _assertMatchingCallersAccredited(OnlyAccreditedCanMint.mint.selector); + } + + /// @notice Checks that the caller of `transfer` is accredited. + function assertOnlyAccreditedTransfer() external view { + _assertMatchingCallersAccredited(OnlyAccreditedCanMint.transfer.selector); + } + + function _assertMatchingCallersAccredited(bytes4 selector) internal view { + PhEvm.TriggerCall[] memory calls = ph.matchingCalls(ph.getAssertionAdopter(), selector, _successfulCalls(), 32); + for (uint256 i = 0; i < calls.length; i++) { + require(registry.isAccredited(calls[i].caller), "caller is not accredited"); + } + } + + function _successfulCalls() internal pure returns (PhEvm.CallFilter memory filter) { + filter.callType = 1; + filter.successOnly = true; + } +} diff --git a/examples/assertions-book/assertions/src/ass5-owner-change.a.sol b/examples/assertions-book/assertions/src/ass5-owner-change.a.sol new file mode 100644 index 0000000..a7d92b2 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass5-owner-change.a.sol @@ -0,0 +1,48 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract OwnerChangeAssertion is Assertion { + bytes32 internal constant OWNER_SLOT = bytes32(uint256(0)); + bytes32 internal constant ADMIN_SLOT = bytes32(uint256(1)); + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerTxEndTrigger(this.assertionOwnerChange.selector); + registerTxEndTrigger(this.assertionAdminChange.selector); + } + + /// @notice Checks that the owner slot is unchanged across the transaction. + function assertionOwnerChange() external view { + address adopter = ph.getAssertionAdopter(); + PhEvm.ForkId memory preFork = _preTx(); + PhEvm.ForkId memory postFork = _postTx(); + + address preOwner = _loadAddressAt(adopter, OWNER_SLOT, preFork); + address postOwner = _loadAddressAt(adopter, OWNER_SLOT, postFork); + + require(preOwner == postOwner, "Owner changed"); + } + + /// @notice Checks that the admin slot is unchanged across the transaction. + function assertionAdminChange() external view { + address adopter = ph.getAssertionAdopter(); + PhEvm.ForkId memory preFork = _preTx(); + PhEvm.ForkId memory postFork = _postTx(); + + address preAdmin = _loadAddressAt(adopter, ADMIN_SLOT, preFork); + address postAdmin = _loadAddressAt(adopter, ADMIN_SLOT, postFork); + + require(preAdmin == postAdmin, "Admin changed"); + } + + function _loadAddressAt(address target, bytes32 slot, PhEvm.ForkId memory fork) internal view returns (address) { + return address(uint160(uint256(ph.loadStateAt(target, slot, fork)))); + } +} diff --git a/examples/assertions-book/assertions/src/ass6-constant-product.a.sol b/examples/assertions-book/assertions/src/ass6-constant-product.a.sol new file mode 100644 index 0000000..973a667 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass6-constant-product.a.sol @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract ConstantProductAssertion is Assertion { + bytes32 internal constant RESERVE0_SLOT = bytes32(uint256(0)); + bytes32 internal constant RESERVE1_SLOT = bytes32(uint256(1)); + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerTxEndTrigger(this.assertionConstantProduct.selector); + } + + /// @notice Checks that the pool's stored reserve product is not reduced by the transaction. + function assertionConstantProduct() external view { + address pool = ph.getAssertionAdopter(); + PhEvm.ForkId memory preFork = _preTx(); + PhEvm.ForkId memory postFork = _postTx(); + + uint256 reserve0Pre = uint256(ph.loadStateAt(pool, RESERVE0_SLOT, preFork)); + uint256 reserve1Pre = uint256(ph.loadStateAt(pool, RESERVE1_SLOT, preFork)); + uint256 reserve0Post = uint256(ph.loadStateAt(pool, RESERVE0_SLOT, postFork)); + uint256 reserve1Post = uint256(ph.loadStateAt(pool, RESERVE1_SLOT, postFork)); + + require(reserve0Post * reserve1Post >= reserve0Pre * reserve1Pre, "Constant product invariant reduced"); + } +} diff --git a/examples/assertions-book/assertions/src/ass7-lending-health-factor.a.sol b/examples/assertions-book/assertions/src/ass7-lending-health-factor.a.sol new file mode 100644 index 0000000..0bd24b1 --- /dev/null +++ b/examples/assertions-book/assertions/src/ass7-lending-health-factor.a.sol @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract LendingHealthFactorAssertion is Assertion { + bytes32 internal constant HEALTH_FACTOR_SLOT = bytes32(uint256(0)); + uint256 internal constant MIN_HEALTH_FACTOR = 1e18; + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.supply.selector); + registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.borrow.selector); + registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.withdraw.selector); + registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.repay.selector); + } + + /// @notice Checks that the touched account remains healthy after a lending operation. + function assertionOperationSafety() external view { + PhEvm.TriggerContext memory ctx = ph.context(); + PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd}); + (uint256 marketId,) = abi.decode(_stripSelector(ph.callinputAt(ctx.callStart)), (uint256, uint256)); + address account = _matchingCaller(ctx.selector); + bytes32 healthSlot = _healthFactorSlot(marketId, account); + uint256 healthFactor = uint256(ph.loadStateAt(ph.getAssertionAdopter(), healthSlot, postCall)); + + require(healthFactor >= MIN_HEALTH_FACTOR, "Operation resulted in unhealthy position"); + } + + function _matchingCaller(bytes4 selector) internal view returns (address) { + PhEvm.TriggerCall[] memory calls = ph.matchingCalls(ph.getAssertionAdopter(), selector, _successfulCalls(), 1); + require(calls.length == 1, "missing triggered call"); + return calls[0].caller; + } + + function _successfulCalls() internal pure returns (PhEvm.CallFilter memory filter) { + filter.callType = 1; + filter.successOnly = true; + } + + function _healthFactorSlot(uint256 marketId, address account) internal pure returns (bytes32) { + return keccak256(abi.encode(account, keccak256(abi.encode(marketId, HEALTH_FACTOR_SLOT)))); + } + + function _stripSelector(bytes memory data) internal pure returns (bytes memory) { + bytes memory stripped = new bytes(data.length - 4); + for (uint256 i = 4; i < data.length; i++) { + stripped[i - 4] = data[i]; + } + return stripped; + } +} + +interface IMorpho { + function supply(uint256 marketId, uint256 amount) external; + function borrow(uint256 marketId, uint256 amount) external; + function withdraw(uint256 marketId, uint256 amount) external; + function repay(uint256 marketId, uint256 amount) external; +} diff --git a/examples/assertions-book/assertions/src/ass8-positions-sum.a.sol b/examples/assertions-book/assertions/src/ass8-positions-sum.a.sol new file mode 100644 index 0000000..ab6f01c --- /dev/null +++ b/examples/assertions-book/assertions/src/ass8-positions-sum.a.sol @@ -0,0 +1,44 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract PositionSumAssertion is Assertion { + bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(0)); + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerFnCallTrigger(this.assertionPositionsSum.selector, ILending.deposit.selector); + } + + /// @notice Checks that a deposit call increases stored total supply by the deposited amount. + function assertionPositionsSum() external view { + address adopter = ph.getAssertionAdopter(); + PhEvm.TriggerContext memory ctx = ph.context(); + PhEvm.ForkId memory preCall = PhEvm.ForkId({forkType: 2, callIndex: ctx.callStart}); + PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd}); + + uint256 preTotalSupply = uint256(ph.loadStateAt(adopter, TOTAL_SUPPLY_SLOT, preCall)); + uint256 postTotalSupply = uint256(ph.loadStateAt(adopter, TOTAL_SUPPLY_SLOT, postCall)); + (, uint256 amount) = abi.decode(_stripSelector(ph.callinputAt(ctx.callStart)), (address, uint256)); + + require(postTotalSupply == preTotalSupply + amount, "Positions sum does not match total supply"); + } + + function _stripSelector(bytes memory data) internal pure returns (bytes memory) { + bytes memory stripped = new bytes(data.length - 4); + for (uint256 i = 4; i < data.length; i++) { + stripped[i - 4] = data[i]; + } + return stripped; + } +} + +interface ILending { + function deposit(address user, uint256 amount) external; +} diff --git a/examples/assertions-book/assertions/src/ass9-timelock-verification.a.sol b/examples/assertions-book/assertions/src/ass9-timelock-verification.a.sol new file mode 100644 index 0000000..2c0c9dd --- /dev/null +++ b/examples/assertions-book/assertions/src/ass9-timelock-verification.a.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "credible-std/Assertion.sol"; +import {AssertionSpec} from "credible-std/SpecRecorder.sol"; +import {PhEvm} from "credible-std/PhEvm.sol"; + +contract TimelockVerificationAssertion is Assertion { + bytes32 internal constant TIMELOCK_DELAY_SLOT = bytes32(uint256(0)); + bytes32 internal constant TIMELOCK_ACTIVE_SLOT = bytes32(uint256(1)); + + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + function triggers() external view override { + registerTxEndTrigger(this.assertionTimelock.selector); + } + + /// @notice Checks that an activated timelock uses a bounded delay. + function assertionTimelock() external view { + address adopter = ph.getAssertionAdopter(); + PhEvm.ForkId memory preFork = _preTx(); + PhEvm.ForkId memory postFork = _postTx(); + + bool preActive = uint256(ph.loadStateAt(adopter, TIMELOCK_ACTIVE_SLOT, preFork)) != 0; + if (preActive) { + return; + } + + bool postActive = uint256(ph.loadStateAt(adopter, TIMELOCK_ACTIVE_SLOT, postFork)) != 0; + if (postActive) { + uint256 delay = uint256(ph.loadStateAt(adopter, TIMELOCK_DELAY_SLOT, postFork)); + + require(delay >= 1 days && delay <= 2 weeks, "Timelock parameters invalid"); + } + } +} diff --git a/examples/assertions-book/src/AccreditedInvestorRegistry.sol b/examples/assertions-book/src/AccreditedInvestorRegistry.sol new file mode 100644 index 0000000..e28060e --- /dev/null +++ b/examples/assertions-book/src/AccreditedInvestorRegistry.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +contract AccreditedInvestorRegistry { + mapping(address => bool) public isAccredited; + + function setAccredited(address account, bool accredited) external { + isAccredited[account] = accredited; + } +} diff --git a/examples/assertions-book/src/MockToken.sol b/examples/assertions-book/src/MockToken.sol new file mode 100644 index 0000000..2aa74c8 --- /dev/null +++ b/examples/assertions-book/src/MockToken.sol @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import "@openzeppelin/contracts/token/ERC20/ERC20.sol"; + +/** + * @title MockToken + * @dev A simple ERC20 token for testing the vault functionality + */ +contract MockToken is ERC20 { + /** + * @dev Constructor that mints initial supply to the deployer + * @param _name The name of the token + * @param _symbol The symbol of the token + * @param _initialSupply The initial supply of tokens to mint + */ + constructor( + string memory _name, + string memory _symbol, + uint256 _initialSupply + ) ERC20(_name, _symbol) { + _mint(msg.sender, _initialSupply * 10 ** decimals()); + } + + /** + * @dev Public mint function for testing purposes + * In a real token, this would have access controls + */ + function mint(address to, uint256 amount) external { + _mint(to, amount); + } + + /** + * @dev Public burn function for testing purposes + */ + function burn(uint256 amount) external { + _burn(msg.sender, amount); + } +} diff --git a/examples/assertions-book/src/ass1-implementation-change.sol b/examples/assertions-book/src/ass1-implementation-change.sol new file mode 100644 index 0000000..5d2b581 --- /dev/null +++ b/examples/assertions-book/src/ass1-implementation-change.sol @@ -0,0 +1,36 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Implementation Contract + * @notice This contract serves as an example implementation for testing the ImplementationChange assertion + * @dev Contains a storage variable for the implementation address and methods to get/set it + */ +contract Implementation { + // Storage slot 0: implementation address + address private _implementation; + + /** + * @notice Constructor that sets the initial implementation address + * @param initialImpl The initial implementation address + */ + constructor(address initialImpl) { + _implementation = initialImpl; + } + + /** + * @notice Returns the current implementation address + * @return The current implementation address + */ + function implementation() external view returns (address) { + return _implementation; + } + + /** + * @notice Updates the implementation address + * @param newImplementation The new implementation address + */ + function setImplementation(address newImplementation) external { + _implementation = newImplementation; + } +} diff --git a/examples/assertions-book/src/ass10-oracle-liveness.sol b/examples/assertions-book/src/ass10-oracle-liveness.sol new file mode 100644 index 0000000..a6af5de --- /dev/null +++ b/examples/assertions-book/src/ass10-oracle-liveness.sol @@ -0,0 +1,66 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Oracle Contract + * @notice This contract tracks the last update time of oracle data + * @dev Implements the IOracle interface for testing the OracleLivenessAssertion + */ +contract Oracle { + // Storage slot 0: last update timestamp + uint256 private _lastUpdated; + + /** + * @notice Constructor that sets the initial last update time + * @param initialLastUpdated The initial last update timestamp + */ + constructor(uint256 initialLastUpdated) { + _lastUpdated = initialLastUpdated; + } + + /** + * @notice Returns the last update timestamp + * @return The last update timestamp + */ + function lastUpdated() external view returns (uint256) { + return _lastUpdated; + } + + /** + * @notice Sets the last update timestamp + * @param newLastUpdated The new last update timestamp + */ + function setLastUpdated(uint256 newLastUpdated) external { + _lastUpdated = newLastUpdated; + } +} + +/** + * @title Dex Contract + * @notice This contract implements a simple DEX that uses oracle data + * @dev Implements the IDex interface for testing the OracleLivenessAssertion + */ +contract Dex { + Oracle public oracle; + + /** + * @notice Constructor that sets the oracle address + * @param _oracle The address of the oracle contract + */ + constructor(address _oracle) { + oracle = Oracle(_oracle); + } + + /** + * @notice Performs a token swap + * @param tokenIn The address of the input token + * @param tokenOut The address of the output token + * @param amountIn The amount of input tokens + * @return The amount of output tokens received + */ + function swap(address tokenIn, address tokenOut, uint256 amountIn) external returns (uint256) { + // In a real implementation, this would use the oracle data to calculate the swap + // For testing purposes, we just return the input amount + return amountIn; + } +} diff --git a/examples/assertions-book/src/ass11-twap-deviation.sol b/examples/assertions-book/src/ass11-twap-deviation.sol new file mode 100644 index 0000000..1e230a2 --- /dev/null +++ b/examples/assertions-book/src/ass11-twap-deviation.sol @@ -0,0 +1,47 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Pool Contract + * @notice A simple pool contract that tracks price and TWAP for testing the TwapDeviation assertion + * @dev Implements the IPool interface for testing the TwapDeviationAssertion + */ +contract Pool { + // Storage slot 0: current price + uint256 private _price; + // Storage slot 1: TWAP price + uint256 private _twap; + + /** + * @notice Constructor that sets the initial price and TWAP + * @param initialPrice The initial price and TWAP value + */ + constructor(uint256 initialPrice) { + _price = initialPrice; + _twap = initialPrice; + } + + /** + * @notice Returns the current price + * @return The current price + */ + function price() external view returns (uint256) { + return _price; + } + + /** + * @notice Returns the TWAP price + * @return The TWAP price + */ + function twap() external view returns (uint256) { + return _twap; + } + + /** + * @notice Sets the price without updating the TWAP + * @param newPrice The new price value + */ + function setPriceWithoutTwapUpdate(uint256 newPrice) external { + _price = newPrice; + } +} diff --git a/examples/assertions-book/src/ass12-erc4626-assets-shares.sol b/examples/assertions-book/src/ass12-erc4626-assets-shares.sol new file mode 100644 index 0000000..2b597b0 --- /dev/null +++ b/examples/assertions-book/src/ass12-erc4626-assets-shares.sol @@ -0,0 +1,70 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Simple Vault + * @notice A simple vault for testing assets and shares assertions + * @dev Uses a simple ratio calculation for assets to shares conversion + */ +contract ERC4626Vault { + // Storage variables + uint256 private _totalAssets; + uint256 private _totalSupply; + address private _asset; + + // Used to manipulate conversion calculations for testing purposes + uint256 private _conversionMultiplier = 1; + + constructor(address asset_) { + _asset = asset_; + } + + function totalAssets() external view returns (uint256) { + return _totalAssets; + } + + function totalSupply() external view returns (uint256) { + return _totalSupply; + } + + function asset() external view returns (address) { + return _asset; + } + + // Convert assets to shares based on current ratio + function convertToShares(uint256 assets) external view returns (uint256) { + if (_totalSupply == 0) return assets; // First deposit is 1:1 + return (assets * _totalSupply * _conversionMultiplier) / (_totalAssets * 1); + } + + // Convert shares to assets based on current ratio + function convertToAssets(uint256 shares) external view returns (uint256) { + if (_totalSupply == 0) return shares; // First deposit is 1:1 + + // Special case for testing: when totalSupply is exactly 42 ether, return double the assets required + // This will cause the assertion to fail as shares will appear to be worth more than they should be + if (_totalSupply == 42 ether) { + return (shares * _totalAssets * 2) / _totalSupply; + } + + return (shares * _totalAssets) / _totalSupply; + } + + // Functions to manipulate state for testing + function setTotalAssets(uint256 _totalAssets_) external { + _totalAssets = _totalAssets_; + } + + function setTotalSupply(uint256 _totalSupply_) external { + _totalSupply = _totalSupply_; + } + + /** + * @notice Sets the conversion multiplier to manipulate asset/share conversion calculations + * @dev This function is ONLY for testing purposes to simulate incorrect conversions + * @param multiplier The multiplier to use (1 = normal behavior, >1 = more shares per asset, <1 = fewer shares per asset) + */ + function setConversionMultiplier(uint256 multiplier) external { + _conversionMultiplier = multiplier; + } +} diff --git a/examples/assertions-book/src/ass13-erc4626-deposit-withdraw.sol b/examples/assertions-book/src/ass13-erc4626-deposit-withdraw.sol new file mode 100644 index 0000000..ff15bb6 --- /dev/null +++ b/examples/assertions-book/src/ass13-erc4626-deposit-withdraw.sol @@ -0,0 +1,233 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +// Simple ERC20 interface required by the assertion +interface IERC20 { + function balanceOf(address account) external view returns (uint256); +} + +/** + * @title Mock ERC20 Token + * @notice A simple ERC20 mock for testing + */ +contract MockERC20 { + mapping(address => uint256) private _balances; + address private _vault; + + constructor() { + _vault = msg.sender; + } + + function balanceOf(address account) external view returns (uint256) { + return _balances[account]; + } + + // For vault to update balances + function updateBalance(address account, uint256 amount) external { + require(msg.sender == _vault, "Only vault can update balances"); + _balances[account] = amount; + } +} + +/** + * @title ERC4626 Vault + * @notice A simple ERC4626 vault for testing assertions + */ +contract ERC4626Vault { + // Storage variables + uint256 private _totalAssets; + uint256 private _totalSupply; + address private _asset; + mapping(address => uint256) private _balances; + mapping(address => uint256) private _assetBalances; + + /** + * @notice Constructor + * @param asset_ The address of the underlying asset + */ + constructor(address asset_) { + if (asset_ == address(0)) { + // Create a new mock token if no asset is provided + MockERC20 mockToken = new MockERC20(); + _asset = address(mockToken); + } else { + _asset = asset_; + } + } + + /** + * @notice Get the total assets in the vault + * @return The total assets amount + */ + function totalAssets() external view returns (uint256) { + return _totalAssets; + } + + /** + * @notice Get the total supply of shares + * @return The total supply of shares + */ + function totalSupply() external view returns (uint256) { + return _totalSupply; + } + + /** + * @notice Get the underlying asset address + * @return The asset address + */ + function asset() external view returns (address) { + return _asset; + } + + /** + * @notice Get the balance of shares for an account + * @param account The account to check + * @return The share balance of the account + */ + function balanceOf(address account) external view returns (uint256) { + return _balances[account]; + } + + /** + * @notice Deposit assets and receive shares + * @param assets The amount of assets to deposit + * @param receiver The account to receive the shares + * @return shares The amount of shares minted + */ + function deposit(uint256 assets, address receiver) external returns (uint256 shares) { + // For simplicity, we use 1:1 ratio + shares = assets; + + // Special case: if exactly 13 ether is deposited, we introduce a vulnerability + // that will trigger the assertion to fail by updating total assets incorrectly + if (assets == 13 ether) { + // Update state with incorrect accounting + _totalAssets += assets - 1 ether; // Deliberately record 1 ether less than deposited + _totalSupply += shares; // Update shares correctly + _balances[receiver] += shares; // Update shares correctly + + // Update mock asset balances for ERC20.balanceOf correctly + _assetBalances[msg.sender] -= assets; + _assetBalances[address(this)] += assets; + + // Update actual ERC20 balances for the assertion to check + _updateMockTokenBalances(msg.sender, _assetBalances[msg.sender]); + _updateMockTokenBalances(address(this), _assetBalances[address(this)]); + + return shares; + } + + // Normal case - everything is updated correctly + _totalAssets += assets; + _totalSupply += shares; + _balances[receiver] += shares; + + // Update mock asset balances for ERC20.balanceOf + _assetBalances[msg.sender] -= assets; + _assetBalances[address(this)] += assets; + + // Update actual ERC20 balances for the assertion to check + _updateMockTokenBalances(msg.sender, _assetBalances[msg.sender]); + _updateMockTokenBalances(address(this), _assetBalances[address(this)]); + + return shares; + } + + /** + * @notice Preview how many shares would be minted for a deposit + * @param assets The amount of assets to deposit + * @return shares The amount of shares that would be minted + */ + function previewDeposit(uint256 assets) external view returns (uint256) { + // For simplicity, we use 1:1 ratio + return assets; + } + + /** + * @notice Withdraw assets by burning shares + * @param assets The amount of assets to withdraw + * @param receiver The account to receive the assets + * @param owner The address of the shares + * @return shares The amount of shares burned + */ + function withdraw(uint256 assets, address receiver, address owner) external returns (uint256 shares) { + // For simplicity, we use 1:1 ratio + shares = assets; + + // Check if owner has enough shares + require(_balances[owner] >= shares, "Not enough shares"); + + // Special case: if exactly 7 ether is withdrawn, we introduce a vulnerability + // that will trigger the assertion to fail by updating total assets incorrectly + if (assets == 7 ether) { + // Update state with incorrect accounting + _totalAssets -= assets + 0.5 ether; // Deliberately remove 0.5 ether more than withdrawn + _totalSupply -= shares; // Update shares correctly + _balances[owner] -= shares; // Update shares correctly + + // Update mock asset balances for ERC20.balanceOf correctly + _assetBalances[address(this)] -= assets; + _assetBalances[receiver] += assets; + + // Update actual ERC20 balances for the assertion to check + _updateMockTokenBalances(address(this), _assetBalances[address(this)]); + _updateMockTokenBalances(receiver, _assetBalances[receiver]); + + return shares; + } + + // Normal case - everything is updated correctly + _totalAssets -= assets; + _totalSupply -= shares; + _balances[owner] -= shares; + + // Update mock asset balances for ERC20.balanceOf + _assetBalances[address(this)] -= assets; + _assetBalances[receiver] += assets; + + // Update actual ERC20 balances for the assertion to check + _updateMockTokenBalances(address(this), _assetBalances[address(this)]); + _updateMockTokenBalances(receiver, _assetBalances[receiver]); + + return shares; + } + + /** + * @notice Preview how many shares would be burned for a withdrawal + * @param assets The amount of assets to withdraw + * @return shares The amount of shares that would be burned + */ + function previewWithdraw(uint256 assets) external view returns (uint256) { + // For simplicity, we use 1:1 ratio + return assets; + } + + // Internal function to update the mock token balances + function _updateMockTokenBalances(address account, uint256 amount) internal { + try MockERC20(_asset).updateBalance(account, amount) {} catch {} + } + + // Mock implementation of ERC20.balanceOf for the asset + function getAssetBalance(address account) external view returns (uint256) { + return _assetBalances[account]; + } + + // For test manipulation + function setAssetBalance(address account, uint256 amount) external { + _assetBalances[account] = amount; + _updateMockTokenBalances(account, amount); + } + + // For test manipulation to break the assertions + function setTotalAssets(uint256 amount) external { + _totalAssets = amount; + } + + function setTotalSupply(uint256 amount) external { + _totalSupply = amount; + } + + function setBalance(address account, uint256 amount) external { + _balances[account] = amount; + } +} diff --git a/examples/assertions-book/src/ass14-fee-verification.sol b/examples/assertions-book/src/ass14-fee-verification.sol new file mode 100644 index 0000000..cea42dd --- /dev/null +++ b/examples/assertions-book/src/ass14-fee-verification.sol @@ -0,0 +1,49 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title AMM Pool Contract + * @notice This contract implements a simple AMM pool with fee verification + * @dev Contains storage variables for fee and stable status + */ +contract Pool { + // Storage slot 0: stable status + bool private _stable; + + // Storage slot 1: fee value + uint256 private _fee; + + /** + * @notice Constructor that sets the initial fee and stable status + * @param initialFee The initial fee value + * @param isStable Whether this is a stable pool + */ + constructor(uint256 initialFee, bool isStable) { + _fee = initialFee; + _stable = isStable; + } + + /** + * @notice Returns whether this is a stable pool + * @return The stable status + */ + function stable() external view returns (bool) { + return _stable; + } + + /** + * @notice Returns the current fee + * @return The current fee value + */ + function fee() external view returns (uint256) { + return _fee; + } + + /** + * @notice Updates the fee + * @param newFee The new fee value + */ + function setFee(uint256 newFee) external { + _fee = newFee; + } +} diff --git a/examples/assertions-book/src/ass15-price-within-ticks.sol b/examples/assertions-book/src/ass15-price-within-ticks.sol new file mode 100644 index 0000000..196f238 --- /dev/null +++ b/examples/assertions-book/src/ass15-price-within-ticks.sol @@ -0,0 +1,100 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Simplified Uniswap V3 Pool + * @notice This contract mimics a simplified Uniswap V3 pool for testing the PriceWithinTicks assertion + * @dev Contains simplified storage and methods to simulate Uniswap V3 pool behavior + */ +contract UniswapV3Pool { + // Storage for slot0 data + uint160 private _sqrtPriceX96; + int24 private _tick; + uint16 private _observationIndex; + uint16 private _observationCardinality; + uint16 private _observationCardinalityNext; + uint8 private _feeProtocol; + bool private _unlocked; + + // Tick spacing - determines which ticks can be initialized + int24 private _tickSpacing; + + // Uniswap V3 tick bounds + int24 constant MIN_TICK = -887272; + int24 constant MAX_TICK = 887272; + + /** + * @notice Constructor that initializes the pool with default values + * @param initialTick The initial tick value + * @param initialTickSpacing The initial tick spacing value + */ + constructor(int24 initialTick, int24 initialTickSpacing) { + require(initialTickSpacing > 0, "TS"); + require(initialTick % initialTickSpacing == 0, "TNA"); + require(initialTick >= MIN_TICK && initialTick <= MAX_TICK, "TOR"); + + _tick = initialTick; + _tickSpacing = initialTickSpacing; + _sqrtPriceX96 = 2 ** 96; // Default price of 1.0 + _unlocked = true; + } + + /** + * @notice Returns the current slot0 data + * @return sqrtPriceX96 The current sqrt price as a Q64.96 + * @return tick The current tick + * @return observationIndex The current observation index + * @return observationCardinality The current observation cardinality + * @return observationCardinalityNext The next observation cardinality + * @return feeProtocol The current fee protocol + * @return unlocked The current unlocked status + */ + function slot0() + external + view + returns ( + uint160 sqrtPriceX96, + int24 tick, + uint16 observationIndex, + uint16 observationCardinality, + uint16 observationCardinalityNext, + uint8 feeProtocol, + bool unlocked + ) + { + return ( + _sqrtPriceX96, + _tick, + _observationIndex, + _observationCardinality, + _observationCardinalityNext, + _feeProtocol, + _unlocked + ); + } + + /** + * @notice Returns the current tick spacing + * @return The current tick spacing + */ + function tickSpacing() external view returns (int24) { + return _tickSpacing; + } + + /** + * @notice Simulates a swap by setting a new tick value + * @param newTick The new tick value to set + */ + function setTick(int24 newTick) external { + _tick = newTick; + } + + /** + * @notice Sets a new tick spacing value + * @param newTickSpacing The new tick spacing to set + */ + function setTickSpacing(int24 newTickSpacing) external { + require(newTickSpacing > 0, "TS"); + _tickSpacing = newTickSpacing; + } +} diff --git a/examples/assertions-book/src/ass16-liquidation-health-factor.sol b/examples/assertions-book/src/ass16-liquidation-health-factor.sol new file mode 100644 index 0000000..463ec7e --- /dev/null +++ b/examples/assertions-book/src/ass16-liquidation-health-factor.sol @@ -0,0 +1,100 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Lending Protocol Implementation + * @notice This contract implements a simple lending protocol for testing the LiquidationHealthFactor assertion + * @dev Simulates health factor calculations and liquidation functionality + */ +contract LendingProtocol { + // MarketParams contains the market identifier + struct MarketParams { + Id id; + } + + struct Id { + uint256 marketId; + } + + // Mapping to store borrower health factors for each market + mapping(uint256 => mapping(address => uint256)) private _healthFactors; + + // Health factor constants (using same values as in the assertion) + uint256 constant LIQUIDATION_THRESHOLD = 1e18; // 1.0 + uint256 constant MIN_HEALTH_FACTOR = 1.02e18; // 1.02 + uint256 constant HEALTHY_FACTOR = 2e18; // 2.0 is healthy + + // Minimum amount required for meaningful health factor improvement + uint256 constant MIN_REPAID_FOR_IMPROVEMENT = 100e18; + + /** + * @notice Set a user's health factor for testing + * @param marketParams The market parameters + * @param borrower The borrower address + * @param healthFactor_ The health factor value to set + */ + function setHealthFactor(MarketParams memory marketParams, address borrower, uint256 healthFactor_) external { + _healthFactors[marketParams.id.marketId][borrower] = healthFactor_; + } + + /** + * @notice Performs a liquidation on a borrower's position + * @param marketParams The market parameters + * @param borrower The borrower address being liquidated + * @param seizedAssets Amount of assets seized from the borrower + * @param repaidShares Amount of debt shares repaid + * @param data Additional data for the liquidation (not used in this implementation) + * @return Amount of assets actually seized and debt shares actually repaid + */ + function liquidate( + MarketParams memory marketParams, + address borrower, + uint256 seizedAssets, + uint256 repaidShares, + bytes memory data + ) external returns (uint256, uint256) { + // Calculate new health factor based on repaid amount + // In a real protocol, this would involve complex calculations + // Here we use a simplified approach for testing purposes + uint256 currentFactor = _healthFactors[marketParams.id.marketId][borrower]; + uint256 newFactor = currentFactor; + + // Only improve health factor if repaid amount is significant + if (repaidShares >= MIN_REPAID_FOR_IMPROVEMENT) { + // Improve health factor based on repaid shares + uint256 improvement = (repaidShares * 1e18) / 1000e18; + + // Set the new health factor + newFactor = currentFactor + improvement; + + // Make sure health factor is at least above MIN_HEALTH_FACTOR if improvement is applied + if (newFactor < MIN_HEALTH_FACTOR) { + newFactor = MIN_HEALTH_FACTOR; + } + } + + _healthFactors[marketParams.id.marketId][borrower] = newFactor; + + return (seizedAssets, repaidShares); + } + + /** + * @notice Checks if a borrower's position is healthy + * @param marketParams The market parameters + * @param borrower The borrower address + * @return Whether the position is healthy (true) or not (false) + */ + function isHealthy(MarketParams memory marketParams, address borrower) external view returns (bool) { + return healthFactor(marketParams, borrower) > LIQUIDATION_THRESHOLD; + } + + /** + * @notice Returns a borrower's health factor + * @param marketParams The market parameters + * @param borrower The borrower address + * @return The current health factor + */ + function healthFactor(MarketParams memory marketParams, address borrower) public view returns (uint256) { + return _healthFactors[marketParams.id.marketId][borrower]; + } +} diff --git a/examples/assertions-book/src/ass17-panic-state-verificatoin.sol b/examples/assertions-book/src/ass17-panic-state-verificatoin.sol new file mode 100644 index 0000000..ee966a4 --- /dev/null +++ b/examples/assertions-book/src/ass17-panic-state-verificatoin.sol @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Emergency Pausable Protocol + * @notice This contract implements a simple protocol with pause functionality + * @dev Used for testing the EmergencyStateAssertion + */ +contract EmergencyPausable { + // Storage variables + bool private _paused; + uint256 private _balance; + + /** + * @notice Constructor that initializes the contract state + * @param initialBalance The initial balance to set + */ + constructor(uint256 initialBalance) { + _balance = initialBalance; + _paused = false; + } + + /** + * @notice Returns whether the protocol is currently paused + * @return The current pause state + */ + function paused() external view returns (bool) { + return _paused; + } + + /** + * @notice Returns the current balance of the protocol + * @return The current balance + */ + function balance() external view returns (uint256) { + return _balance; + } + + /** + * @notice Sets the paused state of the protocol + * @param state The new pause state to set + */ + function setPaused(bool state) external { + _paused = state; + } + + /** + * @notice Deposits an amount to the protocol balance + * @param amount The amount to deposit + */ + function deposit(uint256 amount) external { + // No checks here for paused state - the assertion should catch this + _balance += amount; + } + + /** + * @notice Withdraws an amount from the protocol balance + * @param amount The amount to withdraw + */ + function withdraw(uint256 amount) external { + // No checks for balance sufficiency - the assertion should catch this + _balance -= amount; + } +} diff --git a/examples/assertions-book/src/ass18-harvest-increases-balance.sol b/examples/assertions-book/src/ass18-harvest-increases-balance.sol new file mode 100644 index 0000000..2446cc8 --- /dev/null +++ b/examples/assertions-book/src/ass18-harvest-increases-balance.sol @@ -0,0 +1,68 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title BeefyVault + * @notice This contract serves as an example implementation for testing the BeefyHarvestAssertion + * @dev Implements the IBeefyVault interface with balance, price per share, and harvest functionality + */ +contract BeefyVault { + // Storage variables + uint256 private _balance; + uint256 private _pricePerFullShare; + uint256 private _strategyBalance; + + /** + * @notice Constructor that sets the initial balance and price per share + * @param initialBalance The initial vault balance + * @param initialPricePerShare The initial price per share + */ + constructor(uint256 initialBalance, uint256 initialPricePerShare) { + _balance = initialBalance; + _pricePerFullShare = initialPricePerShare; + _strategyBalance = 0; + } + + /** + * @notice Returns the current vault balance + * @return The current vault balance + */ + function balance() external view returns (uint256) { + return _balance; + } + + /** + * @notice Returns the current price per full share + * @return The current price per full share + */ + function getPricePerFullShare() external view returns (uint256) { + return _pricePerFullShare; + } + + /** + * @notice Simulates adding yields to the strategy and harvesting them into the vault + * @dev This will increase the vault's balance and price per share if badHarvest is false, + * otherwise it will decrease them to simulate a buggy implementation + * @param badHarvest If true, simulate a buggy harvest that decreases balance and price per share + */ + function harvest(bool badHarvest) external { + if (badHarvest) { + // Simulate a buggy harvest that decreases balance + _balance -= 0.5 ether; + _pricePerFullShare -= 0.01 ether; + } else { + // Normal harvest behavior + // Simulate yield generation in the strategy + _strategyBalance += 1 ether; + + // Transfer yield from strategy to vault + _balance += _strategyBalance; + + // Update price per share to reflect the new balance + _pricePerFullShare += 0.01 ether; + + // Reset strategy balance + _strategyBalance = 0; + } + } +} diff --git a/examples/assertions-book/src/ass19-tokens-borrowed-invariant.sol b/examples/assertions-book/src/ass19-tokens-borrowed-invariant.sol new file mode 100644 index 0000000..549dc2f --- /dev/null +++ b/examples/assertions-book/src/ass19-tokens-borrowed-invariant.sol @@ -0,0 +1,89 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Morpho Protocol + * @notice This contract implements a simplified Morpho protocol for testing the TokensBorrowedInvariant assertion + * @dev Contains storage variables for total supply and total borrowed assets with methods to get/set them + */ +contract Morpho { + // Storage slot 0: total supply of assets + uint256 private _totalSupplyAsset; + + // Storage slot 1: total borrowed assets + uint256 private _totalBorrowedAsset; + + /** + * @notice Constructor that initializes the total supply and total borrowed assets + * @param initialSupply The initial total supply of assets + * @param initialBorrowed The initial total borrowed assets + */ + constructor(uint256 initialSupply, uint256 initialBorrowed) { + _totalSupplyAsset = initialSupply; + _totalBorrowedAsset = initialBorrowed; + } + + /** + * @notice Returns the total supply of assets + * @return The total supply of assets + */ + function totalSupplyAsset() external view returns (uint256) { + return _totalSupplyAsset; + } + + /** + * @notice Returns the total borrowed assets + * @return The total borrowed assets + */ + function totalBorrowedAsset() external view returns (uint256) { + return _totalBorrowedAsset; + } + + /** + * @notice Updates the total supply of assets + * @param newSupply The new total supply of assets + */ + function setTotalSupplyAsset(uint256 newSupply) external { + _totalSupplyAsset = newSupply; + } + + /** + * @notice Updates the total borrowed assets + * @param newBorrowed The new total borrowed assets + */ + function setTotalBorrowedAsset(uint256 newBorrowed) external { + _totalBorrowedAsset = newBorrowed; + } + + /** + * @notice Simulates borrowing assets from the protocol + * @param amount The amount to borrow + */ + function borrow(uint256 amount) external { + _totalBorrowedAsset += amount; + } + + /** + * @notice Simulates supplying assets to the protocol + * @param amount The amount to supply + */ + function supply(uint256 amount) external { + _totalSupplyAsset += amount; + } + + /** + * @notice Simulates repaying borrowed assets to the protocol + * @param amount The amount to repay + */ + function repay(uint256 amount) external { + _totalBorrowedAsset -= amount; + } + + /** + * @notice Simulates withdrawing supplied assets from the protocol + * @param amount The amount to withdraw + */ + function withdraw(uint256 amount) external { + _totalSupplyAsset -= amount; + } +} diff --git a/examples/assertions-book/src/ass2-erc4626-operations.sol b/examples/assertions-book/src/ass2-erc4626-operations.sol new file mode 100644 index 0000000..f49f593 --- /dev/null +++ b/examples/assertions-book/src/ass2-erc4626-operations.sol @@ -0,0 +1,235 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import "openzeppelin-contracts/token/ERC20/extensions/ERC4626.sol"; +import "openzeppelin-contracts/token/ERC20/ERC20.sol"; +import "openzeppelin-contracts/access/Ownable.sol"; + +/** + * @title CoolVault + * @dev A simple ERC4626 tokenized vault that accepts deposits of a specific ERC20 token + * and mints vault shares in return. Users can withdraw their assets by burning shares. + */ +contract CoolVault is ERC4626, Ownable { + /** + * @dev Constructor that initializes the vault with an underlying asset + * @param _asset The ERC20 token that this vault will accept as deposits + * @param _name The name of the vault token (e.g., "Cool Vault Token") + * @param _symbol The symbol of the vault token (e.g., "cvTOKEN") + */ + constructor(IERC20 _asset, string memory _name, string memory _symbol) + ERC20(_name, _symbol) + ERC4626(_asset) + Ownable(msg.sender) + {} + + /** + * @dev Returns the total amount of underlying assets held by the vault + * This includes any assets that have been deposited plus any yield earned + * For this basic implementation, it's just the vault's token balance + */ + function totalAssets() public view override returns (uint256) { + return IERC20(asset()).balanceOf(address(this)); + } + + /** + * @dev Returns the maximum amount of assets that can be deposited for a given receiver + * For this basic vault, there's no limit + */ + function maxDeposit(address) public pure override returns (uint256) { + return type(uint256).max; + } + + /** + * @dev Returns the maximum amount of shares that can be minted for a given receiver + * For this basic vault, there's no limit + */ + function maxMint(address) public pure override returns (uint256) { + return type(uint256).max; + } + + /** + * @dev Returns the maximum amount of assets that can be withdrawn by the owner + */ + function maxWithdraw(address owner) public view override returns (uint256) { + return convertToAssets(balanceOf(owner)); + } + + /** + * @dev Returns the maximum amount of shares that can be redeemed by the owner + */ + function maxRedeem(address owner) public view override returns (uint256) { + return balanceOf(owner); + } + + /** + * @dev Emergency function to rescue tokens sent to the contract by mistake + * Only callable by the owner + */ + function rescueTokens(IERC20 token, uint256 amount) external onlyOwner { + require(token != IERC20(asset()), "Cannot rescue vault asset"); + token.transfer(owner(), amount); + } + + /** + * @dev Allows the owner to pause/unpause the vault (if needed for upgrades) + * This is a placeholder for additional functionality + */ + function pause() external onlyOwner { + // Implementation would depend on if you want pausable functionality + // For now, this is just a placeholder + } + + // ========== OVERRIDDEN ERC4626 FUNCTIONS WITH ACCOUNTING BUGS ========== + // These functions override the standard ERC4626 functions to introduce + // deliberate accounting inconsistencies that will trigger the assertions + + /** + * @dev Conditionally buggy deposit function + * Behaves normally except when assets == 13, then mints extra shares + */ + function deposit(uint256 assets, address receiver) public virtual override returns (uint256 shares) { + // Check if this is the special bug trigger case + if (assets == 13 ether) { + // BUG CASE: Manual implementation with accounting error + shares = previewDeposit(assets); + + // Transfer assets normally + IERC20(asset()).transferFrom(msg.sender, address(this), assets); + + // BUG: Mint 10% extra shares than we should + uint256 buggyShares = shares + (shares / 10); + _mint(receiver, buggyShares); + + emit Deposit(msg.sender, receiver, assets, buggyShares); + + return buggyShares; + } else { + // NORMAL CASE: Call parent implementation + return super.deposit(assets, receiver); + } + } + + /** + * @dev Conditionally buggy mint function + * Behaves normally except when shares == 13, then requires fewer assets + */ + function mint(uint256 shares, address receiver) public virtual override returns (uint256 assets) { + // Check if this is the special bug trigger case + if (shares == 13 ether) { + // BUG CASE: Manual implementation with accounting error + assets = previewMint(shares); + + // BUG: Only transfer 90% of the required assets + uint256 buggyAssets = assets - (assets / 10); + IERC20(asset()).transferFrom(msg.sender, address(this), buggyAssets); + + // Mint the full amount of shares requested + _mint(receiver, shares); + + emit Deposit(msg.sender, receiver, buggyAssets, shares); + + return assets; // Return the "expected" amount, not actual + } else { + // NORMAL CASE: Call parent implementation + return super.mint(shares, receiver); + } + } + + /** + * @dev Conditionally buggy withdraw function + * Behaves normally except when assets == 13, then burns fewer shares + */ + function withdraw(uint256 assets, address receiver, address owner) + public + virtual + override + returns (uint256 shares) + { + // Check if this is the special bug trigger case + if (assets == 13 ether) { + // BUG CASE: Manual implementation with accounting error + shares = previewWithdraw(assets); + + // Check allowance if needed + if (msg.sender != owner) { + uint256 allowed = allowance(owner, msg.sender); + if (allowed != type(uint256).max) { + require(shares <= allowed, "ERC4626: withdraw amount exceeds allowance"); + _approve(owner, msg.sender, allowed - shares); + } + } + + // BUG: Burn 5% fewer shares than we should + uint256 buggyShares = shares - (shares / 20); + _burn(owner, buggyShares); + + // Transfer the full amount of assets out + IERC20(asset()).transfer(receiver, assets); + + emit Withdraw(msg.sender, receiver, owner, assets, shares); + + return shares; + } else { + // NORMAL CASE: Call parent implementation + return super.withdraw(assets, receiver, owner); + } + } + + /** + * @dev Conditionally buggy redeem function + * Behaves normally except when shares == 13, then gives extra assets + */ + function redeem(uint256 shares, address receiver, address owner) public virtual override returns (uint256 assets) { + // Check if this is the special bug trigger case + if (shares == 13 ether) { + // BUG CASE: Manual implementation with accounting error + assets = previewRedeem(shares); + + // Check allowance if needed + if (msg.sender != owner) { + uint256 allowed = allowance(owner, msg.sender); + if (allowed != type(uint256).max) { + require(shares <= allowed, "ERC4626: redeem amount exceeds allowance"); + _approve(owner, msg.sender, allowed - shares); + } + } + + // Burn the correct amount of shares + _burn(owner, shares); + + // BUG: Transfer 15% more assets than we should + uint256 buggyAssets = assets + (assets / 7); // ~15% more + IERC20(asset()).transfer(receiver, buggyAssets); + + emit Withdraw(msg.sender, receiver, owner, buggyAssets, shares); + + return buggyAssets; + } else { + // NORMAL CASE: Call parent implementation + return super.redeem(shares, receiver, owner); + } + } + + // ========== ADDITIONAL BUG HELPER FUNCTIONS ========== + + /** + * @dev Helper function to create phantom shares (owner only) + * This mints shares without receiving any underlying assets + */ + function createPhantomShares(address to, uint256 shares) external onlyOwner { + _mint(to, shares); + // BUG: We mint shares but don't receive any underlying assets + // This breaks the fundamental ERC4626 invariant + } + + /** + * @dev Helper function to drain assets without burning shares (owner only) + * This transfers assets out without burning any shares + */ + function drainAssets(uint256 amount) external onlyOwner { + IERC20(asset()).transfer(owner(), amount); + // BUG: We transfer assets out but don't burn any shares + // This breaks the asset-to-share ratio + } +} diff --git a/examples/assertions-book/src/ass20-erc20-drain.sol b/examples/assertions-book/src/ass20-erc20-drain.sol new file mode 100644 index 0000000..ffef4fc --- /dev/null +++ b/examples/assertions-book/src/ass20-erc20-drain.sol @@ -0,0 +1,131 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title MockERC20 + * @notice A simple ERC20 token implementation for testing + */ +contract MockERC20 { + string public name; + string public symbol; + uint8 public decimals; + uint256 public totalSupply; + + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowance; + + /** + * @notice Constructor to initialize the token + * @param _name Token name + * @param _symbol Token symbol + * @param _decimals Token decimals + * @param _initialSupply Initial supply to mint to the deployer + */ + constructor(string memory _name, string memory _symbol, uint8 _decimals, uint256 _initialSupply) { + name = _name; + symbol = _symbol; + decimals = _decimals; + + totalSupply = _initialSupply; + balanceOf[msg.sender] = _initialSupply; + } + + /** + * @notice Transfer tokens to a recipient + * @param to Recipient address + * @param amount Amount to transfer + * @return success Whether the transfer succeeded + */ + function transfer(address to, uint256 amount) external returns (bool) { + balanceOf[msg.sender] -= amount; + balanceOf[to] += amount; + return true; + } + + /** + * @notice Transfer tokens from one address to another + * @param from Source address + * @param to Destination address + * @param amount Amount to transfer + * @return success Whether the transfer succeeded + */ + function transferFrom(address from, address to, uint256 amount) external returns (bool) { + allowance[from][msg.sender] -= amount; + balanceOf[from] -= amount; + balanceOf[to] += amount; + return true; + } + + /** + * @notice Approve spender to transfer tokens + * @param spender Address allowed to spend tokens + * @param amount Amount allowed to spend + * @return success Whether the approval succeeded + */ + function approve(address spender, uint256 amount) external returns (bool) { + allowance[msg.sender][spender] = amount; + return true; + } + + /** + * @notice Mint new tokens to an address + * @param to Address to receive the tokens + * @param amount Amount to mint + */ + function mint(address to, uint256 amount) external { + totalSupply += amount; + balanceOf[to] += amount; + } +} + +/** + * @title TokenVault Contract + * @notice This contract implements a simple ERC20 token vault for testing the ERC20Drain assertion + * @dev Allows transfer of tokens to and from the vault without restrictions + */ +contract TokenVault { + // ERC20 token interface + IERC20 public immutable token; + + /** + * @notice Constructor that sets the token address + * @param _token The ERC20 token address + */ + constructor(address _token) { + token = IERC20(_token); + } + + /** + * @notice Transfers tokens from the sender to this contract + * @param amount The amount of tokens to deposit + */ + function deposit(uint256 amount) external { + token.transferFrom(msg.sender, address(this), amount); + } + + /** + * @notice Transfers tokens from this contract to a recipient + * @param recipient The address to receive tokens + * @param amount The amount of tokens to withdraw + */ + function withdraw(address recipient, uint256 amount) external { + token.transfer(recipient, amount); + } + + /** + * @notice Get the token balance of this contract + * @return The token balance + */ + function getBalance() external view returns (uint256) { + return token.balanceOf(address(this)); + } +} + +/** + * @notice ERC20 interface + */ +interface IERC20 { + function balanceOf(address account) external view returns (uint256); + function transfer(address to, uint256 amount) external returns (bool); + function transferFrom(address from, address to, uint256 amount) external returns (bool); +} diff --git a/examples/assertions-book/src/ass21-ether-drain.sol b/examples/assertions-book/src/ass21-ether-drain.sol new file mode 100644 index 0000000..c448484 --- /dev/null +++ b/examples/assertions-book/src/ass21-ether-drain.sol @@ -0,0 +1,115 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title EtherDrain Contract + * @notice This contract serves as an example implementation for testing the EtherDrain assertion + * @dev Contains methods to receive and withdraw ETH + */ +contract EtherDrain { + // Storage for fund recipient addresses + address payable private _treasury; + address payable private _owner; + + /** + * @notice Constructor that sets the initial treasury and owner addresses + * @param initialTreasury The initial treasury address + * @param initialOwner The initial owner address + */ + constructor(address payable initialTreasury, address payable initialOwner) { + _treasury = initialTreasury; + _owner = initialOwner; + } + + /** + * @notice Returns the current treasury address + * @return The current treasury address + */ + function treasury() external view returns (address) { + return _treasury; + } + + /** + * @notice Returns the current owner address + * @return The current owner address + */ + function owner() external view returns (address) { + return _owner; + } + + /** + * @notice Updates the treasury address + * @param newTreasury The new treasury address + */ + function setTreasury(address payable newTreasury) external { + _treasury = newTreasury; + } + + /** + * @notice Updates the owner address + * @param newOwner The new owner address + */ + function setOwner(address payable newOwner) external { + _owner = newOwner; + } + + /** + * @notice Withdraws a specified amount to the treasury + * @param amount The amount to withdraw + */ + function withdrawToTreasury(uint256 amount) external { + _treasury.transfer(amount); + } + + /** + * @notice Withdraws a specified amount to the owner + * @param amount The amount to withdraw + */ + function withdrawToOwner(uint256 amount) external { + _owner.transfer(amount); + } + + /** + * @notice Withdraws a specified amount to any address + * @param recipient The recipient address + * @param amount The amount to withdraw + */ + function withdrawToAddress(address payable recipient, uint256 amount) external { + recipient.transfer(amount); + } + + /** + * @notice Withdraw all funds to the treasury + */ + function drainToTreasury() external { + uint256 balance = address(this).balance; + if (balance > 0) { + _treasury.transfer(balance); + } + } + + /** + * @notice Withdraw all funds to the owner + */ + function drainToOwner() external { + uint256 balance = address(this).balance; + if (balance > 0) { + _owner.transfer(balance); + } + } + + /** + * @notice Withdraw all funds to any address + * @param recipient The recipient address + */ + function drainToAddress(address payable recipient) external { + uint256 balance = address(this).balance; + if (balance > 0) { + recipient.transfer(balance); + } + } + + // Allow the contract to receive ETH + receive() external payable {} + fallback() external payable {} +} diff --git a/examples/assertions-book/src/ass22-farcaster-message-validity.sol b/examples/assertions-book/src/ass22-farcaster-message-validity.sol new file mode 100644 index 0000000..95368f6 --- /dev/null +++ b/examples/assertions-book/src/ass22-farcaster-message-validity.sol @@ -0,0 +1,115 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Farcaster Protocol + * @notice This contract implements message handling for the Farcaster protocol + * @dev Contains functionality for message validation, user registration, and rate limiting + */ +contract Farcaster { + // Message struct matching the interface in the assertion + struct Message { + uint256 id; + address author; + bytes content; + uint256 timestamp; + bytes signature; + } + + // Storage mappings + mapping(string => address) private _usernameToOwner; + mapping(string => bool) private _registeredUsernames; + mapping(address => uint256) private _lastPostTimestamp; + + // Simple message validation constants + bytes constant INVALID_SIGNATURE = "invalidSignature"; + bytes constant INVALID_CONTENT = "invalid content"; + + /** + * @notice Checks if a message is valid according to protocol rules + * @param message The message to validate + * @return A boolean indicating whether the message is valid + */ + function isValidMessage(Message memory message) external view returns (bool) { + // Very basic checks: + // 1. Message must have a non-zero author address + // 2. Content must not be empty + // 3. Content must not be specifically marked as invalid + // 4. Message must have a timestamp + + if (message.author == address(0)) { + return false; + } + + if (message.content.length == 0) { + return false; + } + + // Check if content is explicitly marked as invalid + if (keccak256(message.content) == keccak256(INVALID_CONTENT)) { + return false; + } + + if (message.timestamp == 0) { + return false; + } + + return true; + } + + /** + * @notice Verifies the cryptographic signature of a message + * @param message The message containing the signature to verify + * @return A boolean indicating whether the signature is valid + */ + function verifySignature(Message memory message) external view returns (bool) { + // For testing purposes, we're just checking if the signature isn't "invalidSignature" + // In a real implementation, this would do proper cryptographic verification + return keccak256(message.signature) != keccak256(INVALID_SIGNATURE); + } + + /** + * @notice Posts a new message to the protocol + * @param message The message to post + */ + function postMessage(Message memory message) external { + _lastPostTimestamp[message.author] = block.timestamp; + } + + /** + * @notice Registers a new username with an owner address + * @param username The username to register + * @param owner The address to associate with the username + */ + function register(string calldata username, address owner) external { + _registeredUsernames[username] = true; + _usernameToOwner[username] = owner; + } + + /** + * @notice Checks if a username is registered + * @param username The username to check + * @return A boolean indicating whether the username is registered + */ + function isRegistered(string calldata username) external view returns (bool) { + return _registeredUsernames[username]; + } + + /** + * @notice Gets the owner address of a registered username + * @param username The username to look up + * @return The address of the username owner + */ + function getUsernameOwner(string calldata username) external view returns (address) { + return _usernameToOwner[username]; + } + + /** + * @notice Gets the timestamp of a user's last post + * @param user The address of the user + * @return The timestamp of the user's last post + */ + function getLastPostTimestamp(address user) external view returns (uint256) { + return _lastPostTimestamp[user]; + } +} diff --git a/examples/assertions-book/src/ass28-intra-tx-oracle-deviation.sol b/examples/assertions-book/src/ass28-intra-tx-oracle-deviation.sol new file mode 100644 index 0000000..e96a373 --- /dev/null +++ b/examples/assertions-book/src/ass28-intra-tx-oracle-deviation.sol @@ -0,0 +1,37 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Oracle Contract + * @notice This contract serves as an example implementation for testing the IntraTxOracleDeviation assertion + * @dev Contains a storage variable for the price and a method to update it + */ +contract Oracle { + // Storage for the current price + uint256 private _price; + + /** + * @notice Constructor that sets the initial price + * @param initialPrice The initial price value + */ + constructor(uint256 initialPrice) { + _price = initialPrice; + } + + /** + * @notice Returns the current price + * @return The current price + */ + function price() external view returns (uint256) { + return _price; + } + + /** + * @notice Updates the price to a new value + * @param newPrice The new price value + */ + function updatePrice(uint256 newPrice) external { + // No checks for deviation here as the assertion will catch it + _price = newPrice; + } +} diff --git a/examples/assertions-book/src/ass4-only-accredited-can-mint.sol b/examples/assertions-book/src/ass4-only-accredited-can-mint.sol new file mode 100644 index 0000000..980b712 --- /dev/null +++ b/examples/assertions-book/src/ass4-only-accredited-can-mint.sol @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +contract OnlyAccreditedCanMint { + mapping(address => uint256) public balanceOf; + + function mint(address to, uint256 amount) external { + balanceOf[to] += amount; + } + + function transfer(address to, uint256 amount) external returns (bool) { + require(balanceOf[msg.sender] >= amount, "insufficient balance"); + balanceOf[msg.sender] -= amount; + balanceOf[to] += amount; + return true; + } +} diff --git a/examples/assertions-book/src/ass5-owner-change.sol b/examples/assertions-book/src/ass5-owner-change.sol new file mode 100644 index 0000000..c28198f --- /dev/null +++ b/examples/assertions-book/src/ass5-owner-change.sol @@ -0,0 +1,57 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Ownership Contract + * @notice This contract implements ownership and admin functionality for testing the OwnerChange assertion + * @dev Contains storage variables for owner and admin addresses with methods to get/set them + */ +contract Ownership { + // Storage slot 0: owner address + address private _owner; + + // Storage slot 1: admin address + address private _admin; + + /** + * @notice Constructor that sets the initial owner and admin addresses + * @param initialOwner The initial owner address + * @param initialAdmin The initial admin address + */ + constructor(address initialOwner, address initialAdmin) { + _owner = initialOwner; + _admin = initialAdmin; + } + + /** + * @notice Returns the current owner address + * @return The current owner address + */ + function owner() external view returns (address) { + return _owner; + } + + /** + * @notice Returns the current admin address + * @return The current admin address + */ + function admin() external view returns (address) { + return _admin; + } + + /** + * @notice Updates the owner address + * @param newOwner The new owner address + */ + function setOwner(address newOwner) external { + _owner = newOwner; + } + + /** + * @notice Updates the admin address + * @param newAdmin The new admin address + */ + function setAdmin(address newAdmin) external { + _admin = newAdmin; + } +} diff --git a/examples/assertions-book/src/ass6-constant-product.sol b/examples/assertions-book/src/ass6-constant-product.sol new file mode 100644 index 0000000..a3a6326 --- /dev/null +++ b/examples/assertions-book/src/ass6-constant-product.sol @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Constant Product AMM + * @notice This contract implements a simple constant product automated market maker + * @dev Follows the x * y = k formula, where x and y are the token reserves + */ +contract ConstantProductAmm { + // Storage slot 0: reserve0 + uint256 private _reserve0; + + // Storage slot 1: reserve1 + uint256 private _reserve1; + + /** + * @notice Constructor that sets initial reserves + * @param reserve0 The initial reserve for token0 + * @param reserve1 The initial reserve for token1 + */ + constructor(uint256 reserve0, uint256 reserve1) { + _reserve0 = reserve0; + _reserve1 = reserve1; + } + + /** + * @notice Returns the current reserves + * @return Current reserves of token0 and token1 + */ + function getReserves() external view returns (uint256, uint256) { + return (_reserve0, _reserve1); + } + + /** + * @notice Update reserves directly (for testing the assertion) + * @param reserve0 New reserve for token0 + * @param reserve1 New reserve for token1 + */ + function setReserves(uint256 reserve0, uint256 reserve1) external { + _reserve0 = reserve0; + _reserve1 = reserve1; + } +} diff --git a/examples/assertions-book/src/ass7-lending-health-factor.sol b/examples/assertions-book/src/ass7-lending-health-factor.sol new file mode 100644 index 0000000..ba1d117 --- /dev/null +++ b/examples/assertions-book/src/ass7-lending-health-factor.sol @@ -0,0 +1,68 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +contract LendingHealthFactor { + // Storage for positions + mapping(uint256 => mapping(address => Position)) public positions; + mapping(uint256 => MarketParams) private _idToMarketParams; + + struct MarketParams { + uint256 marketId; + } + + struct Position { + uint256 supplyShares; + uint128 borrowShares; + uint128 collateral; + } + + // For testing purposes, we'll make this return true/false based on a simple condition + bool public isHealthy = true; + + constructor() { + // Initialize a market + _idToMarketParams[1] = MarketParams({marketId: 1}); + } + + function idToMarketParams(uint256 id) external view returns (MarketParams memory) { + return _idToMarketParams[id]; + } + + function position(uint256 marketId, address user) external view returns (Position memory) { + return positions[marketId][user]; + } + + function _isHealthy(MarketParams memory marketParams, uint256 marketId, address borrower) + external + view + returns (bool) + { + return isHealthy; + } + + // Functions to modify positions + function supply(uint256 marketId, uint256 amount) external { + Position storage pos = positions[marketId][msg.sender]; + pos.supplyShares += amount; + } + + function borrow(uint256 marketId, uint256 amount) external { + Position storage pos = positions[marketId][msg.sender]; + pos.borrowShares += uint128(amount); + } + + function withdraw(uint256 marketId, uint256 amount) external { + Position storage pos = positions[marketId][msg.sender]; + pos.supplyShares -= amount; + } + + function repay(uint256 marketId, uint256 amount) external { + Position storage pos = positions[marketId][msg.sender]; + pos.borrowShares -= uint128(amount); + } + + // Function to set health status for testing + function setHealthStatus(bool _healthy) external { + isHealthy = _healthy; + } +} diff --git a/examples/assertions-book/src/ass8-positions-sum.sol b/examples/assertions-book/src/ass8-positions-sum.sol new file mode 100644 index 0000000..3902e7f --- /dev/null +++ b/examples/assertions-book/src/ass8-positions-sum.sol @@ -0,0 +1,49 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/** + * @title Simple Lending Protocol + * @notice A simple lending protocol that tracks total supply and individual balances + * @dev Implements the ILending interface for testing the PositionSumAssertion + */ +contract Lending { + // Storage slot 0: total supply + uint256 private _totalSupply; + + // Mapping of user addresses to their balances + mapping(address => uint256) private _balances; + + /** + * @notice Returns the total supply of tokens + * @return The total supply + */ + function totalSupply() external view returns (uint256) { + return _totalSupply; + } + + /** + * @notice Returns the balance of an account + * @param account The address to query + * @return balance of the account + */ + function balanceOf(address account) external view returns (uint256) { + return _balances[account]; + } + + /** + * @notice Deposits tokens for a user + * @param user The address of the user + * @param amount The amount to deposit + * @dev Special case: if amount is 42 ether, increases total supply by 43 ether instead + */ + function deposit(address user, uint256 amount) external { + _balances[user] += amount; + + // Special case to test the assertion + if (amount == 42 ether) { + _totalSupply += 43 ether; // Intentionally create a mismatch + } else { + _totalSupply += amount; + } + } +} diff --git a/examples/assertions-book/src/ass9-timelock-verification.sol b/examples/assertions-book/src/ass9-timelock-verification.sol new file mode 100644 index 0000000..61f3989 --- /dev/null +++ b/examples/assertions-book/src/ass9-timelock-verification.sol @@ -0,0 +1,32 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +contract TimelockVerification { + struct Timelock { + uint256 timelockDelay; + bool isActive; + } + + Timelock private _timelock; + + constructor() { + _timelock = Timelock({timelockDelay: 1 days, isActive: false}); + } + + function timelockActive() external view returns (bool) { + return _timelock.isActive; + } + + function timelockDelay() external view returns (uint256) { + return _timelock.timelockDelay; + } + + function activateTimelock() external { + _timelock.isActive = true; + } + + function setTimelock(uint256 _delay) external { + _timelock.isActive = true; + _timelock.timelockDelay = _delay; + } +} diff --git a/examples/assertions-book/test/.gitkeep b/examples/assertions-book/test/.gitkeep new file mode 100644 index 0000000..8b13789 --- /dev/null +++ b/examples/assertions-book/test/.gitkeep @@ -0,0 +1 @@ + diff --git a/foundry.toml b/foundry.toml index ed64fbb..13a95fd 100644 --- a/foundry.toml +++ b/foundry.toml @@ -14,6 +14,18 @@ gas_limit = 100000000 # Include test directory test = "test" +[profile.assertions-book] +src = "examples/assertions-book/assertions/src" +test = "examples/assertions-book/test" +out = "examples/assertions-book/out" +cache_path = "examples/assertions-book/cache" +libs = ["lib"] +remappings = [ + "credible-std/=src/", + "forge-std/=lib/forge-std/src/", + "openzeppelin-contracts/=lib/openzeppelin-contracts/contracts/" +] + [profile.micro-patterns] src = "examples/micro-patterns/src" test = "examples/micro-patterns/test"