feat: consolidate per-protocol assertion examples under examples/

examples/README.md

@@ -0,0 +1,33 @@
+# Examples
+
+This folder contains assertion examples for credible-std across many protocols, consolidated from per-protocol git branches.
+
+Each subfolder is compiled standalone via a Foundry profile that reuses the root `src/` (credible-std) and `lib/` (forge submodules) — there are no nested Foundry projects, only profiles in the root `foundry.toml`.
+
+## Build a specific protocol
+
+```sh
+FOUNDRY_PROFILE=<protocol> forge build
+```
+
+## Protocols
+
+| Folder | Source branch | Highlights |
+|---|---|---|
+| `aave/` | `aave` | Aave V3 Horizon oracle & reserve-backing; Aave V4 hub/spoke |
+| `aerodrome/` | `aerodrome` | Aerodrome pool assertions |
+| `cap/` | `cap` | OFAC compliance + redemption-gate (ERC-4626) |
+| `curve/` | `curve` | crvUSD controller, LlamaLend, CurveLlamma, StableSwap-NG, TriCrypto-NG |
+| `denaria/` | `all-protection-suites` | Denaria perpetual operation safety |
+| `euler/` | `eulerv2` | EVault, circuit breaker, sandwich detection |
+| `nado/` | `ink/assertions` | Nado perpetual clearinghouse |
+| `royco/` | `royco-dawn` | Royco kernel accounting, cumulative flow, vault tranche |
+| `safe/` | `safe-protection-suite` | Safe config lock + tx-shape assertions |
+| `spark/` | `spark` | Spark vault + SparkLend oracle/SLL inflow |
+| `symbiotic/` | `symbiotic` | Symbiotic vault (flow, config, circuit breaker) + relay |
+| `tydro/` | `ink/assertions` | Tydro Aave-v3-like operation safety on Ink |
+| `uniswap/` | `0x` | Uniswap V3 pool assertions (V4 lives in root `src/`) |
+| `veda/` | `ink/assertions` | Veda BoringVault assertions |
+| `zeroex/` | `0x` | 0x Settler assertion |
+
+Existing example projects on master (`assertions-book/`, `micro-patterns/`, `vault_demo/`) are unchanged.

examples/aave/README.md

@@ -0,0 +1,20 @@
+# aave examples
+
+Assertion examples and supporting helpers extracted from the `aave` branch.
+
+## Build
+
+```sh
+FOUNDRY_PROFILE=aave forge build
+```
+
+## Files
+
+- AaveV3HorizonHelpers.sol
+- AaveV3HorizonInterfaces.sol
+- AaveV3HorizonOracleAssertion.sol
+- AaveV3HorizonReserveBackingAssertion.sol
+- AaveV4Helpers.sol
+- AaveV4HubAccountingAssertion.sol
+- AaveV4Interfaces.sol
+- AaveV4SpokeRiskAssertion.sol

examples/aave/src/AaveV3HorizonHelpers.sol

@@ -0,0 +1,94 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.13;
+
+import {Assertion} from "credible-std/Assertion.sol";
+import {PhEvm} from "credible-std/PhEvm.sol";
+import {AssertionSpec} from "credible-std/SpecRecorder.sol";
+
+import {AaveV3LikeTypes, IAaveV3LikeAddressesProvider, IAaveV3LikePool} from "credible-std/protection/lending/examples/AaveV3LikeInterfaces.sol";
+import {IAaveV3HorizonOracle} from "./AaveV3HorizonInterfaces.sol";
+
+/// @title AaveV3HorizonHelpers
+/// @author Phylax Systems
+/// @notice Shared fork-aware readers and decoders for Aave v3 Horizon examples.
+/// @dev Horizon assertions intentionally read through the Pool, AddressesProvider, AaveOracle,
+///      Chainlink-compatible sources, aTokens, and debt tokens rather than restating one local
+///      require branch. Constructor inputs are explicit so assertion deployment does not depend
+///      on target-state reads in an isolated runtime.
+abstract contract AaveV3HorizonHelpers is Assertion {
+    uint256 internal constant BPS = 10_000;
+
+    constructor() {
+        registerAssertionSpec(AssertionSpec.Reshiram);
+    }
+
+    function _viewFailureMessage() internal pure override returns (string memory) {
+        return "AaveV3Horizon: fork view failed";
+    }
+
+    function _oracleAt(address addressesProvider, PhEvm.ForkId memory fork) internal view returns (address) {
+        return _readAddressAt(addressesProvider, abi.encodeCall(IAaveV3LikeAddressesProvider.getPriceOracle, ()), fork);
+    }
+
+    function _reservesListAt(address pool, PhEvm.ForkId memory fork) internal view returns (address[] memory reserves) {
+        reserves = abi.decode(_viewAt(pool, abi.encodeCall(IAaveV3LikePool.getReservesList, ()), fork), (address[]));
+    }
+
+    function _reserveDataAt(address pool, address asset, PhEvm.ForkId memory fork)
+        internal
+        view
+        returns (AaveV3LikeTypes.ReserveData memory reserveData)
+    {
+        reserveData = abi.decode(
+            _viewAt(pool, abi.encodeCall(IAaveV3LikePool.getReserveData, (asset)), fork), (AaveV3LikeTypes.ReserveData)
+        );
+    }
+
+    function _userConfigDataAt(address pool, address account, PhEvm.ForkId memory fork)
+        internal
+        view
+        returns (uint256)
+    {
+        AaveV3LikeTypes.UserConfigurationMap memory userConfig = abi.decode(
+            _viewAt(pool, abi.encodeCall(IAaveV3LikePool.getUserConfiguration, (account)), fork),
+            (AaveV3LikeTypes.UserConfigurationMap)
+        );
+        return userConfig.data;
+    }
+
+    function _assetPriceAt(address oracle, address asset, PhEvm.ForkId memory fork) internal view returns (uint256) {
+        return _readUintAt(oracle, abi.encodeCall(IAaveV3HorizonOracle.getAssetPrice, (asset)), fork);
+    }
+
+    function _sourceOfAssetAt(address oracle, address asset, PhEvm.ForkId memory fork) internal view returns (address) {
+        return _readAddressAt(oracle, abi.encodeCall(IAaveV3HorizonOracle.getSourceOfAsset, (asset)), fork);
+    }
+
+    function _assertPriceBounded(
+        address oracle,
+        address asset,
+        PhEvm.ForkId memory pre,
+        PhEvm.ForkId memory post,
+        uint256 deviationBps
+    ) internal view {
+        uint256 prePrice = _assetPriceAt(oracle, asset, pre);
+        uint256 postPrice = _assetPriceAt(oracle, asset, post);
+        require(prePrice > 0 && postPrice > 0, "AaveV3Horizon: reserve oracle price invalid");
+        require(
+            ph.ratioGe(postPrice, 1, prePrice, 1, deviationBps) && ph.ratioGe(prePrice, 1, postPrice, 1, deviationBps),
+            "AaveV3Horizon: reserve oracle price drift"
+        );
+    }
+
+    function _requireAdopter(address expected, string memory message) internal view {
+        require(ph.getAssertionAdopter() == expected, message);
+    }
+
+    function _isBorrowing(uint256 userConfigData, uint256 reserveId) internal pure returns (bool) {
+        return ((userConfigData >> (reserveId * 2)) & 1) != 0;
+    }
+
+    function _isUsingAsCollateral(uint256 userConfigData, uint256 reserveId) internal pure returns (bool) {
+        return ((userConfigData >> (reserveId * 2 + 1)) & 1) != 0;
+    }
+}

examples/aave/src/AaveV3HorizonInterfaces.sol

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.13;
+
+/// @notice Minimal AaveOracle surface used by the Horizon-specific assertions.
+interface IAaveV3HorizonOracle {
+    function getAssetPrice(address asset) external view returns (uint256);
+    function getSourceOfAsset(address asset) external view returns (address);
+    function getFallbackOracle() external view returns (address);
+    function setAssetSources(address[] calldata assets, address[] calldata sources) external;
+    function setFallbackOracle(address fallbackOracle) external;
+}
+
+/// @notice Minimal ERC20/accounting-token surface used by Horizon reserve backing checks.
+interface IAaveV3HorizonToken {
+    function balanceOf(address account) external view returns (uint256);
+    function totalSupply() external view returns (uint256);
+}

examples/aave/src/AaveV3HorizonOracleAssertion.sol

@@ -0,0 +1,191 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.13;
+
+import {PhEvm} from "credible-std/PhEvm.sol";
+
+import {AaveV3LikeTypes, IAaveV3LikePool} from "credible-std/protection/lending/examples/AaveV3LikeInterfaces.sol";
+import {AaveV3HorizonHelpers} from "./AaveV3HorizonHelpers.sol";
+
+/// @title AaveV3HorizonOracleAssertion
+/// @author Phylax Systems
+/// @notice Protects Horizon's oracle-backed lending risk state.
+/// @dev This assertion targets properties that are not local `require` checks:
+///      - Risk-changing Pool operations must not share a transaction envelope with material
+///        PreTx/PostTx oracle drift for active collateral, debt reserves, or touched assets.
+///      - The active oracle source for those reserves must not be swapped earlier or later in the
+///        same transaction while the Pool consumes the resulting risk state.
+///      - The checks span Pool reserve/user bitmaps, the AddressesProvider, AaveOracle, and
+///        Chainlink-compatible source contracts across the whole transaction, not one call frame.
+contract AaveV3HorizonOracleAssertion is AaveV3HorizonHelpers {
+    address internal immutable POOL;
+    address internal immutable ADDRESSES_PROVIDER;
+    uint256 internal immutable MAX_RESERVES_TO_SCAN;
+    uint256 internal immutable ORACLE_DEVIATION_BPS;
+
+    constructor(address pool_, address addressesProvider_, uint256 maxReservesToScan_, uint256 oracleDeviationBps_) {
+        require(pool_ != address(0), "AaveV3Horizon: pool zero");
+        require(addressesProvider_ != address(0), "AaveV3Horizon: provider zero");
+        require(maxReservesToScan_ != 0, "AaveV3Horizon: max reserves zero");
+        require(oracleDeviationBps_ <= BPS, "AaveV3Horizon: bad oracle tolerance");
+
+        POOL = pool_;
+        ADDRESSES_PROVIDER = addressesProvider_;
+        MAX_RESERVES_TO_SCAN = maxReservesToScan_;
+        ORACLE_DEVIATION_BPS = oracleDeviationBps_;
+    }
+
+    /// @notice Registers one transaction-end check for Horizon oracle/risk coupling.
+    /// @dev This intentionally runs after the whole transaction, so it catches bundled oracle
+    ///      changes that happened before or after a Pool risk operation. The Pool function itself
+    ///      cannot reproduce the PreTx oracle/source baseline with a local require.
+    function triggers() external view override {
+        registerTxEndTrigger(this.assertRiskOperationOracleEnvelope.selector);
+    }
+
+    /// @notice Bounds oracle/source movement across any transaction that includes Pool risk operations.
+    /// @dev Scans successful Horizon Pool calls in the transaction, resolves affected users/assets,
+    ///      and compares oracle prices and source addresses between PreTx and PostTx. A failure
+    ///      means the transaction consumed lending risk state while also changing the oracle basis
+    ///      used to value that risk.
+    function assertRiskOperationOracleEnvelope() external view {
+        _requireAdopter(POOL, "AaveV3Horizon: configured pool is not adopter");
+
+        PhEvm.ForkId memory pre = _preTx();
+        PhEvm.ForkId memory post = _postTx();
+        address oracle = _oracleAt(ADDRESSES_PROVIDER, post);
+
+        _assertCallGroupOracleEnvelope(oracle, IAaveV3LikePool.borrow.selector, pre, post);
+        _assertCallGroupOracleEnvelope(oracle, IAaveV3LikePool.withdraw.selector, pre, post);
+        _assertCallGroupOracleEnvelope(oracle, IAaveV3LikePool.setUserUseReserveAsCollateral.selector, pre, post);
+        _assertCallGroupOracleEnvelope(oracle, IAaveV3LikePool.finalizeTransfer.selector, pre, post);
+        _assertCallGroupOracleEnvelope(oracle, IAaveV3LikePool.setUserEMode.selector, pre, post);
+        _assertCallGroupOracleEnvelope(oracle, IAaveV3LikePool.liquidationCall.selector, pre, post);
+    }
+
+    function _assertCallGroupOracleEnvelope(
+        address oracle,
+        bytes4 selector,
+        PhEvm.ForkId memory pre,
+        PhEvm.ForkId memory post
+    ) internal view {
+        PhEvm.CallInputs[] memory calls = ph.getAllCallInputs(POOL, selector);
+
+        for (uint256 i; i < calls.length; ++i) {
+            address account = _operationAccount(selector, calls[i].input, calls[i].caller);
+            if (account != address(0)) {
+                _assertAccountReservePricesBounded(account, oracle, pre, post);
+            }
+
+            _assertTouchedAssetPricesBounded(selector, calls[i].input, oracle, pre, post);
+        }
+    }
+
+    function _assertAccountReservePricesBounded(
+        address account,
+        address oracle,
+        PhEvm.ForkId memory pre,
+        PhEvm.ForkId memory post
+    ) internal view {
+        address[] memory reserves = _reservesListAt(POOL, post);
+        require(reserves.length <= MAX_RESERVES_TO_SCAN, "AaveV3Horizon: too many reserves");
+
+        uint256 preConfig = _userConfigDataAt(POOL, account, pre);
+        uint256 postConfig = _userConfigDataAt(POOL, account, post);
+
+        for (uint256 i; i < reserves.length; ++i) {
+            AaveV3LikeTypes.ReserveData memory reserveData = _reserveDataAt(POOL, reserves[i], post);
+            bool activeBefore =
+                _isBorrowing(preConfig, reserveData.id) || _isUsingAsCollateral(preConfig, reserveData.id);
+            bool activeAfter =
+                _isBorrowing(postConfig, reserveData.id) || _isUsingAsCollateral(postConfig, reserveData.id);
+
+            if (!activeBefore && !activeAfter) {
+                continue;
+            }
+
+            _assertSourceStable(oracle, reserves[i], pre, post);
+            _assertPriceBounded(oracle, reserves[i], pre, post, ORACLE_DEVIATION_BPS);
+        }
+    }
+
+    function _assertTouchedAssetPricesBounded(
+        bytes4 selector,
+        bytes memory input,
+        address oracle,
+        PhEvm.ForkId memory pre,
+        PhEvm.ForkId memory post
+    ) internal view {
+        if (selector == IAaveV3LikePool.borrow.selector) {
+            (address asset,,,,) = abi.decode(input, (address, uint256, uint256, uint16, address));
+            _assertSourceStable(oracle, asset, pre, post);
+            _assertPriceBounded(oracle, asset, pre, post, ORACLE_DEVIATION_BPS);
+            return;
+        }
+
+        if (selector == IAaveV3LikePool.withdraw.selector) {
+            (address asset,,) = abi.decode(input, (address, uint256, address));
+            _assertSourceStable(oracle, asset, pre, post);
+            _assertPriceBounded(oracle, asset, pre, post, ORACLE_DEVIATION_BPS);
+            return;
+        }
+
+        if (selector == IAaveV3LikePool.setUserUseReserveAsCollateral.selector) {
+            (address asset,) = abi.decode(input, (address, bool));
+            _assertSourceStable(oracle, asset, pre, post);
+            _assertPriceBounded(oracle, asset, pre, post, ORACLE_DEVIATION_BPS);
+            return;
+        }
+
+        if (selector == IAaveV3LikePool.finalizeTransfer.selector) {
+            (address asset,,,,,) = abi.decode(input, (address, address, address, uint256, uint256, uint256));
+            _assertSourceStable(oracle, asset, pre, post);
+            _assertPriceBounded(oracle, asset, pre, post, ORACLE_DEVIATION_BPS);
+            return;
+        }
+
+        if (selector == IAaveV3LikePool.liquidationCall.selector) {
+            (address collateralAsset, address debtAsset,,,) =
+                abi.decode(input, (address, address, address, uint256, bool));
+            _assertSourceStable(oracle, collateralAsset, pre, post);
+            _assertSourceStable(oracle, debtAsset, pre, post);
+            _assertPriceBounded(oracle, collateralAsset, pre, post, ORACLE_DEVIATION_BPS);
+            _assertPriceBounded(oracle, debtAsset, pre, post, ORACLE_DEVIATION_BPS);
+        }
+    }
+
+    function _assertSourceStable(address oracle, address asset, PhEvm.ForkId memory pre, PhEvm.ForkId memory post)
+        internal
+        view
+    {
+        address preSource = _sourceOfAssetAt(oracle, asset, pre);
+        address postSource = _sourceOfAssetAt(oracle, asset, post);
+        require(preSource == postSource, "AaveV3Horizon: reserve oracle source changed");
+    }
+
+    function _operationAccount(bytes4 selector, bytes memory input, address caller) internal pure returns (address) {
+        if (selector == IAaveV3LikePool.borrow.selector) {
+            (,,,, address onBehalfOf) = abi.decode(input, (address, uint256, uint256, uint16, address));
+            return onBehalfOf;
+        }
+
+        if (
+            selector == IAaveV3LikePool.withdraw.selector
+                || selector == IAaveV3LikePool.setUserUseReserveAsCollateral.selector
+                || selector == IAaveV3LikePool.setUserEMode.selector
+        ) {
+            return caller;
+        }
+
+        if (selector == IAaveV3LikePool.finalizeTransfer.selector) {
+            (, address from,,,,) = abi.decode(input, (address, address, address, uint256, uint256, uint256));
+            return from;
+        }
+
+        if (selector == IAaveV3LikePool.liquidationCall.selector) {
+            (,, address user,,) = abi.decode(input, (address, address, address, uint256, bool));
+            return user;
+        }
+
+        return address(0);
+    }
+}