diff --git a/assertions-book/assertions/ass12-erc4626-assets-to-shares.mdx b/assertions-book/assertions/ass12-erc4626-assets-to-shares.mdx
index f8878bb..09d970b 100644
--- a/assertions-book/assertions/ass12-erc4626-assets-to-shares.mdx
+++ b/assertions-book/assertions/ass12-erc4626-assets-to-shares.mdx
@@ -30,4 +30,5 @@ For more information about cheatcodes, see the [Cheatcodes Documentation](/credi
Full examples with tests available in the [Phylax Assertion Examples Repository](https://github.com/phylaxsystems/assertion-examples/blob/main/assertions/).
## Related Assertions
-- [ERC4626 Deposit and Withdrawal](/assertions-book/assertions/ass13-erc4626-deposit-withdraw)
\ No newline at end of file
+
+- [ERC4626 Vault Operations](/assertions-book/assertions/ass13-erc4626-deposit-withdraw) — deposit, withdraw, mint, redeem with batch handling
\ No newline at end of file
diff --git a/assertions-book/assertions/ass13-erc4626-deposit-withdraw.mdx b/assertions-book/assertions/ass13-erc4626-deposit-withdraw.mdx
index c57aa1d..00cd66b 100644
--- a/assertions-book/assertions/ass13-erc4626-deposit-withdraw.mdx
+++ b/assertions-book/assertions/ass13-erc4626-deposit-withdraw.mdx
@@ -1,45 +1,57 @@
---
-title: ERC4626 Vault Deposit and Withdrawal
-description: Assert that ERC4626 deposit and withdrawal operations maintain correct accounting
+title: ERC4626 Vault Operations
+description: Ensure that ERC4626 operations maintain correct accounting
---
import ass13Erc4626DepositWithdraw from "/snippets/ass13-erc4626-deposit-withdraw.a.mdx";
+import ass2Erc4626Operations from "/snippets/ass2-erc4626-operations.a.mdx";
## Use Case & Applications
-Ensures ERC4626 deposit and withdrawal operations maintain correct accounting for both assets and shares, preventing share calculation errors and fund loss. Critical for yield aggregators (Yearn, Aave, Compound), lending protocols with ERC4626 interest-bearing tokens, liquidity pools using ERC4626 for LP tokens, and staking protocols with ERC4626 staking tokens.
+Ensures ERC4626 operations maintain correct accounting for both assets and shares, preventing share calculation errors and fund loss. Critical for yield aggregators (Yearn, Aave, Compound), lending protocols with ERC4626 interest-bearing tokens, liquidity pools using ERC4626 for LP tokens, and staking protocols with ERC4626 staking tokens.
Any discrepancy between preview functions and actual operations could lead to users receiving incorrect amounts, potentially resulting in value loss.
-## Explanation
+## Focused Approach: Deposit & Withdraw
-Collection of five assertion functions providing comprehensive verification of deposit/withdrawal operations:
+Five assertion functions for deposit/withdrawal verification:
**Deposit Assertions:**
- **Asset Accounting**: Total vault assets increase by exact deposit amount
-- **Share Accounting**: Depositors receive correct shares (verified against `previewDeposit()`)
+- **Share Accounting**: Depositors receive correct shares
**Withdrawal Assertions:**
- **Asset Accounting**: Total vault assets decrease by exact withdrawal amount
-- **Share Accounting**: Correct shares burned (verified against `previewWithdraw()`)
+- **Share Accounting**: Correct shares burned
**Share Value Assertion:**
-- **Share Value Monotonicity**: Share value never decreases unexpectedly
+- **Share Value Monotonicity**: Share value never decreases unexpectedly (with precision tolerance for rounding)
-Uses these cheatcodes:
-- `ph.getCallInputs()`: Track deposit/withdraw call inputs
-- `ph.forkPreState()` / `ph.forkPostState()`: Compare balances before/after operations
-- `registerCallTrigger()`: Trigger on ERC4626 vault operations
+Uses `ph.getCallInputs()`, `ph.forkPreTx()` / `ph.forkPostTx()`, and `registerCallTrigger()`. See the [Cheatcodes Reference](/credible/cheatcodes-reference) for details.
-The assertions verify no discrepancy exists between preview function predictions and actual operation results.
+
-For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference).
+## Comprehensive Approach: All Operations + Batch Handling
-## Code Example
+Use this approach when your protocol:
+- Uses mint/redeem in addition to deposit/withdraw
+- Handles multiple operations in a single transaction
+- Needs validation against preview functions
-
+Four assertion functions covering all ERC4626 operations:
+
+- **Batch Operations Consistency**: Validates deposit, mint, withdraw, and redeem in a single transaction. Uses preview functions for expected value calculation.
+- **Deposit Balance Verification**: Confirms vault assets increase by exact deposit amount
+- **Depositor Shares Verification**: Confirms depositor receives shares matching `previewDeposit()`
+- **Base Invariant**: Ensures vault always has at least as many assets as shares
+
+Uses both `registerCallTrigger()` and `registerStorageChangeTrigger()`.
+
+
Full examples with tests available in the [Phylax Assertion Examples Repository](https://github.com/phylaxsystems/assertion-examples/blob/main/assertions/).
## Related Assertions
-- [ERC4626 Assets to Shares](/assertions-book/assertions/ass12-erc4626-assets-to-shares)
+
+- [ERC4626 Assets to Shares](/assertions-book/assertions/ass12-erc4626-assets-to-shares) — simple base invariant check
+- [Harvest Increases Balance](/assertions-book/assertions/ass18-harvest-increases-balance) — yield operation validation
diff --git a/assertions-book/assertions/ass22-farcaster-protocol-integrity.mdx b/assertions-book/assertions/ass22-farcaster-protocol-integrity.mdx
deleted file mode 100644
index f0e79b2..0000000
--- a/assertions-book/assertions/ass22-farcaster-protocol-integrity.mdx
+++ /dev/null
@@ -1,35 +0,0 @@
----
-title: 'Farcaster Protocol Integrity'
-description: 'Ensure message validity, unique usernames, and rate limits in Farcaster'
----
-
-import ass22FarcasterMessageValidity from "/snippets/ass22-farcaster-message-validity.a.mdx";
-
-## Use Case & Applications
-
-Ensures security and integrity of decentralized social media protocols by maintaining critical invariants: data integrity (proper message signatures), identity protection (preventing username spoofing), DoS prevention (rate limiting), and platform stability. Critical for social protocols (Farcaster, Lens Protocol), identity systems managing unique identifiers, content publishing platforms, and governance systems requiring message validity.
-
-Without proper validation, attackers could post messages as other users, register duplicate usernames, flood the network, or create invalid content that breaks client applications.
-
-## Explanation
-
-Provides comprehensive protection by monitoring three critical aspects:
-
-- **Message Validity**: Validates posted messages have proper signatures, meet content requirements, and pass protocol-specific checks
-- **Username Uniqueness**: Ensures usernames remain unique and ownership is properly tracked
-- **Rate Limiting**: Enforces posting rate limits to prevent network abuse
-
-Uses these cheatcodes:
-- `ph.forkPreState()` / `ph.forkPostState()`: Check system state before and after operations
-- `ph.getCallInputs()`: Retrieve and decode function call parameters
-- `registerCallTrigger()`: Trigger when specific functions are called
-
-The multi-layered approach checks basic invariants first, then performs deeper validation of protocol-specific rules for both performance efficiency and comprehensive coverage.
-
-For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference).
-
-## Code Example
-
-
-
-Full examples with tests available in the [Phylax Assertion Examples Repository](https://github.com/phylaxsystems/assertion-examples/blob/main/assertions/).
diff --git a/assertions-book/assertions/use-cases-index.mdx b/assertions-book/assertions/use-cases-index.mdx
index 2d42347..1e59700 100644
--- a/assertions-book/assertions/use-cases-index.mdx
+++ b/assertions-book/assertions/use-cases-index.mdx
@@ -45,7 +45,7 @@ This section contains assertion patterns organized by use case categories.
- [**ERC4626 Assets to Shares**](/assertions-book/assertions/ass12-erc4626-assets-to-shares): Verifies correct conversion between assets and shares in ERC4626 vaults, preventing accounting errors that could lead to fund loss.
-- [**ERC4626 Deposit and Withdraw**](/assertions-book/assertions/ass13-erc4626-deposit-withdraw): Ensures deposit and withdrawal operations maintain correct accounting in ERC4626 vaults, protecting user funds during transfers.
+- [**ERC4626 Vault Operations**](/assertions-book/assertions/ass13-erc4626-deposit-withdraw): Ensures all ERC4626 operations (deposit, withdraw, mint, redeem) maintain correct accounting, with support for batch transaction validation.
- [**Harvest Increases Balance**](/assertions-book/assertions/ass18-harvest-increases-balance): Verifies that yield-generating operations like harvests always increase the total balance of vaults, preventing value extraction attacks.
@@ -60,10 +60,6 @@ This section contains assertion patterns organized by use case categories.
- [**Ether Drain**](/assertions-book/assertions/ass21-ether-drain): Monitors and limits ETH outflows from contracts, protecting against unauthorized withdrawals that could deplete protocol reserves.
-## Data Integrity & Message Verification
-
-- [**Farcaster Protocol Integrity**](/assertions-book/assertions/ass22-farcaster-protocol-integrity): Ensures the integrity of cross-chain messages in the Farcaster protocol, preventing unauthorized or malformed message processing.
-
---
**Next:** Explore [previous hacks analysis](/assertions-book/previous-hacks/) to see how assertions could have prevented real-world exploits.
diff --git a/docs.json b/docs.json
index 65c19f2..0b6cd7a 100644
--- a/docs.json
+++ b/docs.json
@@ -191,12 +191,6 @@
"assertions-book/assertions/ass21-ether-drain"
]
},
- {
- "group": "Data Integrity & Message Verification",
- "pages": [
- "assertions-book/assertions/ass22-farcaster-protocol-integrity"
- ]
- },
{
"group": "Use Case Mapping",
"pages": [
diff --git a/snippets/ass22-farcaster-message-validity.a.mdx b/snippets/ass22-farcaster-message-validity.a.mdx
deleted file mode 100644
index c3a234a..0000000
--- a/snippets/ass22-farcaster-message-validity.a.mdx
+++ /dev/null
@@ -1,122 +0,0 @@
-```solidity
-// SPDX-License-Identifier: MIT
-pragma solidity ^0.8.13;
-
-import {Assertion} from "credible-std/Assertion.sol";
-import {PhEvm} from "credible-std/PhEvm.sol";
-
-contract FarcasterProtocolAssertion is Assertion {
- // Constants
- uint256 constant MAX_CONTENT_LENGTH = 320; // Farcaster's max message length
- uint256 constant POST_COOLDOWN = 1 minutes;
-
- function triggers() external view override {
- // Register trigger for message validity on postMessage calls
- registerCallTrigger(this.assertMessageValidity.selector, IFarcaster.postMessage.selector);
-
- // Register trigger for username uniqueness on register calls
- registerCallTrigger(this.assertUniqueUsername.selector, IFarcaster.register.selector);
-
- // Register trigger for rate limits on postMessage calls
- registerCallTrigger(this.assertRateLimit.selector, IFarcaster.postMessage.selector);
- }
-
- function assertMessageValidity() external {
- // Get the assertion adopter address
- IFarcaster adopter = IFarcaster(ph.getAssertionAdopter());
-
- // Get all calls to postMessage function
- PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(adopter), adopter.postMessage.selector);
-
- for (uint256 i = 0; i < callInputs.length; i++) {
- // Decode the message parameters from the call data
- IFarcaster.Message memory message = abi.decode(callInputs[i].input, (IFarcaster.Message));
-
- // Examine state after the message is posted to ensure all validations pass
- ph.forkPostTx();
-
- // Check basic message validity requirements
- require(message.author != address(0), "Invalid author: zero address");
- require(message.content.length > 0, "Invalid message: empty content");
- require(message.content.length <= MAX_CONTENT_LENGTH, "Invalid message: content exceeds max length");
- require(message.timestamp > 0, "Invalid message: missing timestamp");
- require(message.signature.length > 0, "Invalid message: missing signature");
-
- // Verify cryptographic signature is valid for the message
- require(adopter.verifySignature(message), "Security violation: invalid signature");
-
- // Check protocol-specific validation rules
- require(adopter.isValidMessage(message), "Message failed protocol validation");
- }
- }
-
- function assertUniqueUsername() external {
- // Get the assertion adopter address
- IFarcaster adopter = IFarcaster(ph.getAssertionAdopter());
-
- // Get all calls to register function
- PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(adopter), adopter.register.selector);
-
- for (uint256 i = 0; i < callInputs.length; i++) {
- // Decode registration parameters
- (string memory username, address owner) = abi.decode(callInputs[i].input, (string, address));
-
- // Check pre-registration state to ensure username isn't already taken
- ph.forkPreCall(callInputs[i].id);
- require(!adopter.isRegistered(username), "Security violation: username already registered");
-
- // Check post-registration state to ensure registration succeeded and owner is correct
- ph.forkPostCall(callInputs[i].id);
- require(adopter.isRegistered(username), "Registration failed to complete");
- require(
- adopter.getUsernameOwner(username) == owner, "Security violation: owner mismatch after registration"
- );
- }
- }
-
- function assertRateLimit() external {
- // Get the assertion adopter address
- IFarcaster adopter = IFarcaster(ph.getAssertionAdopter());
-
- // Get all calls to postMessage function
- PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(adopter), adopter.postMessage.selector);
-
- for (uint256 i = 0; i < callInputs.length; i++) {
- // Decode the message to get author
- IFarcaster.Message memory message = abi.decode(callInputs[i].input, (IFarcaster.Message));
-
- address user = message.author;
-
- // Check state before posting to validate rate limits
- ph.forkPreCall(callInputs[i].id);
-
- // Ensure cooldown between posts is respected
- uint256 lastPostTime = adopter.getLastPostTimestamp(user);
- require(block.timestamp >= lastPostTime + POST_COOLDOWN, "Rate limit violation: posting too frequently");
- }
- }
-}
-
-interface IFarcaster {
- // Message struct and functions
- struct Message {
- uint256 id;
- address author;
- bytes content;
- uint256 timestamp;
- bytes signature;
- }
-
- function isValidMessage(Message memory message) external view returns (bool);
- function verifySignature(Message memory message) external view returns (bool);
- function postMessage(Message memory message) external;
-
- // Username functions
- function register(string calldata username, address owner) external;
- function isRegistered(string calldata username) external view returns (bool);
- function getUsernameOwner(string calldata username) external view returns (address);
-
- // Rate limit functions
- function getLastPostTimestamp(address user) external view returns (uint256);
-}
-```
diff --git a/snippets/ass3-pending-balance-bedrock-staking.a.mdx b/snippets/ass3-pending-balance-bedrock-staking.a.mdx
deleted file mode 100644
index 6554643..0000000
--- a/snippets/ass3-pending-balance-bedrock-staking.a.mdx
+++ /dev/null
@@ -1,39 +0,0 @@
-```solidity
-// SPDX-License-Identifier: MIT
-pragma solidity ^0.8.13;
-
-import {Assertion} from "credible-std/Assertion.sol";
-import {Staking} from "src/ass3-pending-balance-bedrock-staking.sol";
-import {PhEvm} from "credible-std/PhEvm.sol";
-import {Test} from "forge-std/Test.sol";
-
-contract StakingAssertions is Assertion, Staking, Test {
- function triggers() public view override {
- triggerRecorder.registerCallTrigger(this.assertTotalPendingOnMint.selector, Staking.mint.selector);
- }
-
- // Assertion PostTotalPending = PreTotalPending + ethersToMint
- function assertTotalPendingOnMint() public {
- Staking staking = Staking(payable(ph.getAssertionAdopter()));
-
- PhEvm.CallInputs[] memory mintCalls = ph.getCallInputs(address(staking), Staking.mint.selector);
-
- ph.forkPreTx();
- uint256 preTotalPending = staking.getPendingEthers();
-
- uint256 expectedPostTotalPending = preTotalPending;
- for (uint256 i = 0; i < mintCalls.length; i++) {
- (uint256 minToMint,) = abi.decode(mintCalls[i].input, (uint256, uint256));
- expectedPostTotalPending += minToMint;
- }
-
- ph.forkPostTx();
-
- require(staking.getPendingEthers() == expectedPostTotalPending, "ExpectedTotalPendingInvalid");
- }
-
- function _load(bytes32 slot) internal view returns (bytes32 value) {
- value = ph.load(ph.getAssertionAdopter(), slot);
- }
-}
-```