feat: Filtered micro pattern examples

README.md

@@ -8,27 +8,8 @@ Full API documentation is available at: https://phylaxsystems.github.io/credible
 
 ## 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.
+Assertion Book examples live in `examples/assertions-book`; micro-pattern examples
+live in `examples/micro-patterns`.
 
 ## Installation
 

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 |

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

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

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

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

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