add testing vs production execution model documentation (GTM-2310)

assertions-book/assertions/aave-v3-suite.mdx

@@ -31,11 +31,9 @@ In order to showcase the real power of assertions, we have introduced a bug in t
 
 Anyone borrowing exactly `333e6` tokens will receive double the amount of tokens they would normally receive if they borrowed any other amount.
 
-The bug can be found in the [BorrowLogic.sol](https://github.com/phylaxsystems/aave-v3-origin/tree/main/src/protocol/libraries/logic/BorrowLogic.sol#L128-L144) file.
+The bug can be found in the [BorrowLogic.sol](https://github.com/phylaxsystems/aave-v3-origin/blob/main/src/contracts/protocol/libraries/logic/BorrowLogic.sol#L137-L141) file.
 
-<Warning>
-**DO NOT USE THIS VERSION OF AAVE V3 IN PRODUCTION!**
-</Warning>
+<Warning>**DO NOT USE THIS VERSION OF AAVE V3 IN PRODUCTION!**</Warning>
 
 ## Key Features
 
@@ -66,7 +64,7 @@ These demonstrate assertion capabilities but could be implemented in Solidity:
 
 ## Assertion Collections
 
-### Production Assertions (High Value)
+### Production Assertions
 
 #### Core Invariants
 
@@ -97,18 +95,12 @@ These demonstrate assertion capabilities but could be implemented in Solidity:
   - Balance change verification using event logs
   - Works with complex call patterns
 
-### Showcase Assertions (Demonstrative)
+### Showcase Assertions
 
 #### Operation Validation
 
-- **[BorrowingInvariantAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/showcase/BorrowingInvariantAssertions.a.sol)** - Standard borrow checks:
-  - Liability decrease verification
-  - Health factor maintenance
-  - Reserve state consistency
-  - Borrow cap enforcement
-  - Balance/debt tracking
-
 - **[LendingInvariantAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/showcase/LendingInvariantAssertions.a.sol)** - Standard supply/withdrawal checks:
+
   - Reserve state validation
   - Supply cap enforcement
   - Balance change verification
@@ -152,6 +144,7 @@ These demonstrate assertion capabilities but could be implemented in Solidity:
 ## Intentional Bugs
 
 1. **333e6 Borrow Bug**: Borrowing exactly 333e6 tokens returns double amount
+
    - Location: `BorrowLogic.sol` lines 128-144
    - Test: `test_BASE_INVARIANT_A_DebtTokenSupply_333e6Bug()`
 

credible/assertions-overview.mdx

@@ -61,14 +61,15 @@ Assertions run [off-chain](/credible/glossary#off-chain-execution) with higher g
 
 **Gas Limit**
 
-Assertion functions are limited to 300,000 gas per execution. If an assertion exceeds this limit, the transaction will be invalidated and dropped.
+Assertion functions are limited to 300,000 gas per execution. If an assertion exceeds this limit, the transaction is dropped.
+
+This is a security measure: assertion gas usage can vary depending on the transaction being validated. Without this limit, an attacker could craft a transaction that causes the assertion to exceed gas limits, bypassing the protection. By dropping transactions that cause assertions to run out of gas, the system remains secure.
 
 Stay mindful of gas consumption:
 - Use [triggers](/credible/triggers) to run assertions only when needed
 - Be aware that some cheatcodes like `getCallInputs()` have variable gas costs due to unknown input lengths
 - Optimize your assertion logic to stay within the gas limit
-
-For gas optimization strategies, see the [Triggers](/credible/triggers) documentation.
+- Test with realistic data volumes - see [Gas Limits in Testing](/credible/testing-assertions#gas-limits)
 
 ## Hacks Assertions Would Have Prevented
 

credible/execution-model.mdx

@@ -0,0 +1,175 @@
+---
+title: 'Testing vs. Production'
+description: 'How assertion execution differs between testing and on-chain environments'
+---
+
+In production, the Credible Layer **drops** transactions that fail assertions - they never enter the blockchain. This means there's no on-chain trace of what the attacker tried or which vulnerability was targeted.
+
+In testing, failed assertions cause **reverts**. This lets you use `vm.expectRevert()` to verify your assertion catches violations and returns the expected error message.
+
+Understanding this difference is important for writing effective tests and interpreting their results.
+
+## Quick Comparison
+
+| Aspect | Testing | Production |
+|--------|---------|------------|
+| **When assertion fails** | Transaction reverts | Transaction dropped (never enters block) |
+| **Which assertion runs** | Specified by `fnSelector` | All matching assertions |
+| **Scope** | Next external call only | All transactions to protected contracts |
+
+## Production: Transactions Are Dropped
+
+In production, the [Assertion Enforcer](/credible/assertion-enforcer) validates transactions during block building:
+
+```mermaid
+flowchart LR
+    TX[Transaction] --> AE[Assertion Enforcer]
+    AE --> |Identify triggers| MATCH{Triggers<br/>match?}
+    MATCH --> |Yes| RUN[Run assertions]
+    MATCH --> |No| INCLUDE[Include in block]
+    RUN --> |All pass| INCLUDE
+    RUN --> |Any fails| DROP[Drop transaction]
+
+    style DROP fill:#e74c3c,color:#fff
+    style INCLUDE fill:#27ae60,color:#fff
+```
+
+Key behaviors:
+- Triggers are evaluated to determine which assertions run
+- All matching assertions for all interacted contracts execute
+- Failed transactions are dropped - they never enter the blockchain
+- Users don't see reverts; the transaction simply doesn't get included
+
+## Testing: Transactions Revert
+
+In testing, `cl.assertion()` registers an assertion to run on the next external call:
+
+```mermaid
+flowchart LR
+    CL["cl.assertion()"] --> |Register| NEXT[Next external call]
+    NEXT --> RUN[Run specified<br/>assertion function]
+    RUN --> |Passes| PERSIST[State persisted]
+    RUN --> |Fails| REVERT[Transaction reverts]
+
+    style REVERT fill:#e74c3c,color:#fff
+    style PERSIST fill:#27ae60,color:#fff
+```
+
+Key behaviors:
+- You specify the assertion function via `fnSelector`, but triggers still determine if it runs
+- Only the specified assertion runs, not all assertions for the contract
+- Only the next external call is validated, then the registration is consumed
+- Reverts simulate drops - use `vm.expectRevert()` to test failure cases
+
+## The `cl.assertion()` Mental Model
+
+`cl.assertion()` works like `vm.prank()` - it only affects the immediately following external call.
+
+```solidity
+// ✅ CORRECT: cl.assertion() immediately before target call
+function testCorrectOrder() public {
+    // Setup first
+    token.mint(user, 1000);
+
+    // Register assertion
+    cl.assertion({
+        adopter: address(protocol),
+        createData: type(MyAssertion).creationCode,
+        fnSelector: MyAssertion.assertionFunction.selector
+    });
+
+    // Target call - assertion runs here
+    vm.prank(user);
+    protocol.deposit(100);
+}
+```
+
+```solidity
+// ❌ WRONG: External call between cl.assertion() and target
+function testWrongOrder() public {
+    cl.assertion({...});
+
+    // This call consumes the assertion registration!
+    token.mint(user, 1000);
+
+    // Assertion already consumed - won't run here
+    vm.prank(user);
+    protocol.deposit(100);
+}
+// Results in: "Expected 1 assertion to be executed, but 0 were executed"
+```
+
+### State Persistence
+
+When an assertion passes, state changes persist for the rest of the test. You can assert on updated values and register subsequent assertions.
+
+```solidity
+function testStatePersistence() public {
+    // First operation
+    cl.assertion({...});
+    protocol.deposit(100);
+
+    // State from deposit persists - we can check it
+    assertEq(protocol.balance(user), 100);
+
+    // Register new assertion for next operation
+    cl.assertion({...});
+    protocol.withdraw(50);
+
+    // Both operations' effects visible
+    assertEq(protocol.balance(user), 50);
+}
+```
+
+## Common Pitfalls
+
+### "Expected 1 assertion to be executed, but 0 were executed"
+
+This error means the assertion didn't run. Common causes:
+
+1. External call between `cl.assertion()` and target - the intervening call consumed the assertion registration
+2. Called function doesn't match a registered trigger - see below
+3. Target transaction reverts before assertion runs - the protocol function itself fails
+
+### Trigger Mismatch
+
+The `fnSelector` parameter specifies which assertion function to run, but triggers are still evaluated. The assertion only runs if the next external call matches a registered trigger for that assertion function.
+
+```solidity
+// In assertion contract
+function triggers() external view override {
+    registerCallTrigger(this.assertDeposit.selector, Protocol.deposit.selector);
+    registerCallTrigger(this.assertWithdraw.selector, Protocol.withdraw.selector);
+}
+```
+
+```solidity
+// ✅ CORRECT: deposit() matches the trigger for assertDeposit
+cl.assertion({fnSelector: MyAssertion.assertDeposit.selector});
+protocol.deposit(100);
+
+// ❌ WRONG: withdraw() has no trigger registered for assertDeposit
+cl.assertion({fnSelector: MyAssertion.assertDeposit.selector});
+protocol.withdraw(50);
+// Results in: "Expected 1 assertion to be executed, but 0 were executed"
+```
+
+To verify triggers work correctly with real transactions, use [backtesting](/credible/backtesting).
+
+## Related Documentation
+
+<CardGroup cols={2}>
+  <Card title="Testing Assertions" icon="flask" href="/credible/testing-assertions">
+    Testing patterns
+  </Card>
+  <Card title="Triggers" icon="bolt" href="/credible/triggers">
+    Production trigger behavior
+  </Card>
+  <Card title="Backtesting" icon="clock-rotate-left" href="/credible/backtesting">
+    Test with real transactions
+  </Card>
+  <Card title="Troubleshooting" icon="wrench" href="/credible/troubleshooting">
+    Common errors
+  </Card>
+</CardGroup>
+

credible/testing-assertions.mdx

@@ -75,6 +75,10 @@ contract TestOwnableAssertion is CredibleTest, Test {
 }
 ```
 
+<Note>
+Testing uses reverts to simulate production behavior where transactions are dropped. See [Testing vs. Production](/credible/execution-model) for details.
+</Note>
+
 Key concepts:
 - Use `cl.assertion()` to register assertions that will be run on the next transaction
 - Only one assertion function can be registered at a time, which allows you to test assertion functions in isolation
@@ -179,6 +183,30 @@ When testing assertions, it can be difficult to trigger the conditions that woul
 
 You can see examples of mock protocols in the [Assertion Examples](https://github.com/phylaxsystems/assertion-examples/tree/main/src) repository.
 
+## Gas Limits
+
+Assertion functions have a gas limit of 300k. This limit exists to ensure assertion validation doesn't slow down block production.
+
+If an assertion exceeds this limit, it reverts with `OutOfGas`. In production, this causes the transaction to be dropped - even if there's no actual violation. Since Assertion gas usage can fluctuate with the transaction they are validating, a sophisticated attacker could potentially craft a transaction that intentionally makes the Assertion execution to be over the gas limit. In that case, if we didn't drop the invalidating transaction, the attacker would be able to use the gas limit to get around the system and forcefully include an invalidating transaction.
+
+This makes gas limit issues critical to catch during testing.
+
+### The Happy Path Problem
+
+Counterintuitively, the happy path is usually the most expensive. When no violation is detected:
+- All checks run to completion
+- Loops iterate through all items
+- No early returns short-circuit execution
+
+Failure cases often exit early when a violation is found, using less gas.
+
+### Testing Recommendations
+
+- Test with realistic data volumes - if your assertion loops through items, test with the maximum expected count
+- Test batch operations at maximum expected size
+- Use `pcl test -vvv` to monitor gas usage
+- If approaching the limit, optimize or split the assertion
+
 ## What's Next?
 
 - If you encounter issues while testing, check the [Troubleshooting Guide](/credible/troubleshooting)

credible/triggers.mdx

@@ -9,6 +9,15 @@ Triggers determine when assertions should execute. Using the right triggers ensu
 
 It is important to use triggers to make sure that assertions are only called when they are needed in order to save gas and resources. For example, it is a waste to trigger an assertion on every call to a contract if the assertion is only checking a value that can only be changed by a specific function. In this case it would make sense to use a trigger that only triggers on calls to the specific function or updates to the specific storage slot of the value.
 
+## Trigger Behavior in Production
+
+When a transaction is validated, the Credible Layer identifies all assertions with triggers matching the transaction. All matching assertions execute - if any fails, the transaction is dropped.
+
+This means:
+- Multiple assertions can protect the same function
+- Each assertion with a matching trigger runs independently
+- A transaction must pass all matching assertions to be included in a block
+
 ## Trigger Types
 
 Different triggers provide different guarantees and should be chosen based on the specific invariant you're trying to enforce.

credible/troubleshooting.mdx

@@ -110,7 +110,7 @@ These errors occur when the assertion executes but fails due to issues in the as
 
 ### Gas Limit Exceeded
 
-Assertions have a **300k gas limit** per assertion function. If exceeded, you'll see an `OutOfGas` error.
+Assertions have a **300k gas limit** per assertion function. If exceeded, the assertion reverts with `OutOfGas` - causing the transaction to be dropped even if there's no actual violation.
 
 **Symptoms:**
 
@@ -124,15 +124,14 @@ Assertions have a **300k gas limit** per assertion function. If exceeded, you'll
 - Parsing too many events
 - Multiple storage reads without caching
 - Complex calculations without early returns
+- Happy path runs the most code - When no violation occurs, the assertion runs all checks and iterations without early exit
 
 **Solutions:**
 
-Optimize the assertion logic:
-
 1. **Fail fast** - Check simple conditions first before expensive operations
 2. **Optimize loops** - Limit iterations, cache values outside loops
-3. **Share storage reads** - Read once, extract multiple values
-4. **Split complex assertions** - Consider splitting into multiple assertion functions
+3. **Cache storage reads** - Read once, reuse the value
+4. **Split complex assertions** - Break into multiple assertion functions with specific triggers
 
 **Debugging:**
 

docs.json

@@ -47,6 +47,7 @@
                 "group": "Testing",
                 "pages": [
                   "credible/testing-assertions",
+                  "credible/execution-model",
                   "credible/fuzz-testing",
                   "credible/backtesting",
                   "credible/ci-cd-integration"