feat: add protocol based examples, protection suites

src/protection/lending/ILendingProtectionSuite.sol

@@ -8,8 +8,8 @@ import {PhEvm} from "../../PhEvm.sol";
 /// @notice Step-oriented interface for protocol-specific lending protection suites.
 /// @dev Implementations expose the protocol-specific plumbing needed to assert a shared family of
 ///      lending-protocol invariants:
-///      - any successful action that increases debt or reduces effective collateral must leave the
-///        affected account solvent under the protocol's own risk metric
+///      - any successful action that increases debt or reduces effective collateral must not move a
+///        solvent account into insolvency under the protocol's own risk metric
 ///      - successful withdrawals must not consume more claim than the account had before the call
 ///      - successful liquidations must not consume more debt or collateral than existed before the call
 ///      The bounded-consumption portion should be measured from the successful call's actual effect,
@@ -24,7 +24,7 @@ import {PhEvm} from "../../PhEvm.sol";
 ///         `consumed <= availableBefore` for each returned check.
 ///      5. Filter to solvency-relevant operations with `shouldCheckPostOperationSolvency(...)`.
 ///      6. Read the account snapshot with `getAccountSnapshot(...)`.
-///      7. Require `snapshot.solvency.isSolvent == true`.
+///      7. Require that a solvent pre-call account remains solvent after the call.
 ///
 ///      Different protocols can encode different solvency metrics while preserving the same invariant:
 ///      - Aave-like systems can expose `metric = healthFactor`, `threshold = 1e18`, `comparison = Gte`.
@@ -54,7 +54,8 @@ interface ILendingProtectionSuite {
         WithdrawCollateral,
         DisableCollateral,
         TransferCollateral,
-        Liquidation
+        Liquidation,
+        SetEMode
     }
 
     /// @notice Comparison rule for the protocol-defined solvency metric.

src/protection/lending/LendingBaseAssertion.sol

@@ -3,6 +3,7 @@ pragma solidity ^0.8.13;
 
 import {Assertion} from "../../Assertion.sol";
 import {PhEvm} from "../../PhEvm.sol";
+import {AssertionSpec} from "../../SpecRecorder.sol";
 import {ForkUtils} from "../../utils/ForkUtils.sol";
 import {ILendingProtectionSuite} from "./ILendingProtectionSuite.sol";
 
@@ -64,7 +65,7 @@ abstract contract LendingProtectionSuiteBase is ForkUtils, ILendingProtectionSui
 /// @dev Inherit this together with a concrete `ILendingProtectionSuite` implementation. The base
 ///      contract handles one decode pass per triggered call, then enforces both:
 ///      - any bounded-consumption checks returned by the suite
-///      - post-operation solvency for risk-increasing operations
+///      - healthy accounts are not made insolvent by risk-increasing operations
 abstract contract LendingBaseAssertion is Assertion {
     error LendingTriggeredCallNotFound(bytes4 selector, uint256 callStart);
     error LendingOperationAccountMissing(bytes4 selector);
@@ -93,6 +94,10 @@ abstract contract LendingBaseAssertion is Assertion {
     /// @return suite The suite used to decode operations and evaluate solvency.
     function _suite() internal view virtual returns (ILendingProtectionSuite);
 
+    constructor() {
+        registerAssertionSpec(AssertionSpec.Reshiram);
+    }
+
     /// @notice Registers one generic lending operation-safety check for every monitored selector.
     /// @dev This is the only trigger wiring most lending assertions need to implement. The suite
     ///      decides which selectors matter through `getMonitoredSelectors()`, and this base maps all
@@ -130,7 +135,7 @@ abstract contract LendingBaseAssertion is Assertion {
         PhEvm.ForkId memory afterFork = _postCall(triggered.callEnd);
 
         _assertConsumptionChecks(suite, triggered, operation, beforeFork, afterFork);
-        _assertPostOperationSolvency(suite, triggered, operation, afterFork);
+        _assertPostOperationSolvency(suite, triggered, operation, beforeFork, afterFork);
     }
 
     /// @notice Enforces the suite-provided bounded-consumption checks for the triggered operation.
@@ -167,10 +172,10 @@ abstract contract LendingBaseAssertion is Assertion {
         }
     }
 
-    /// @notice Enforces post-operation solvency for risk-increasing operations.
-    /// @dev Operations that do not increase debt or reduce effective collateral are skipped. This is
-    ///      the original shared lending invariant, now run as one stage of the broader
-    ///      operation-safety pipeline.
+    /// @notice Enforces that risk-increasing operations do not newly make an account insolvent.
+    /// @dev Operations that do not increase debt or reduce effective collateral are skipped. Accounts
+    ///      already insolvent before the call are also skipped so existing bad debt or liquidatable
+    ///      positions do not cause false positives on unrelated account-management actions.
     /// @param suite The protocol-specific lending suite.
     /// @param triggered The exact adopter frame that caused the assertion to run.
     /// @param operation The decoded lending operation.
@@ -179,6 +184,7 @@ abstract contract LendingBaseAssertion is Assertion {
         ILendingProtectionSuite suite,
         ILendingProtectionSuite.TriggeredCall memory triggered,
         ILendingProtectionSuite.OperationContext memory operation,
+        PhEvm.ForkId memory beforeFork,
         PhEvm.ForkId memory afterFork
     ) internal view {
         if (!suite.shouldCheckPostOperationSolvency(operation)) {
@@ -189,6 +195,12 @@ abstract contract LendingBaseAssertion is Assertion {
             revert LendingOperationAccountMissing(triggered.selector);
         }
 
+        ILendingProtectionSuite.AccountSnapshot memory beforeSnapshot =
+            suite.getAccountSnapshot(operation.account, beforeFork);
+        if (!beforeSnapshot.solvency.isSolvent) {
+            return;
+        }
+
         ILendingProtectionSuite.AccountSnapshot memory snapshot = suite.getAccountSnapshot(operation.account, afterFork);
 
         if (!snapshot.solvency.isSolvent) {