Skip to main content

Documentation Index

Fetch the complete documentation index at: https://docs.phylax.systems/llms.txt

Use this file to discover all available pages before exploring further.

Call frame context mappings describe how assertions can use matched call context and call-scoped snapshots to validate state around a specific function call.

​
Status

  • Supported
  • Partially Supported
  • Not Supported Yet

​
Implementation Details

​
Required Cheatcodes

  • getCallInputs(address aa, bytes4 signature) - Gets call inputs with unique IDs
  • context() - Gets the currently matched onFnCall trigger context
  • loadStateAt(address target, bytes32 slot, ForkId fork) - Reads storage at a call-scoped snapshot

​
Example Implementation

Protocol: 
import {AssertionSpec} from "credible-std/SpecRecorder.sol";

contract Protocol {
    mapping(address => uint256) public balances;
    uint256 public totalSupply;

    function transfer(address to, uint256 amount) public {
        balances[msg.sender] -= amount;
        balances[to] += amount;
    }

    function batchTransfer(address[] calldata recipients, uint256[] calldata amounts) public {
        for (uint256 i = 0; i < recipients.length; i++) {
            transfer(recipients[i], amounts[i]);
        }
    }
}
Assertion: 
contract CallFrameContextAssertion is Assertion {
    constructor() {
        registerAssertionSpec(AssertionSpec.Reshiram);
    }

    function triggers() public view override {
        registerFnCallTrigger(this.assertCallFrameContext.selector, Protocol.transfer.selector);
    }

    function assertCallFrameContext() public view {
        Protocol protocol = Protocol(ph.getAssertionAdopter());
        PhEvm.TriggerContext memory ctx = ph.context();
        PhEvm.CallInputs[] memory transferCalls = ph.getCallInputs(
            address(protocol),
            protocol.transfer.selector
        );
        PhEvm.CallInputs memory transferCall;
        for (uint256 i = 0; i < transferCalls.length; i++) {
            if (transferCalls[i].id == ctx.callStart) {
                transferCall = transferCalls[i];
                break;
            }
        }

        address from = transferCall.caller;
        (address to, uint256 amount) = abi.decode(transferCall.input, (address, uint256));
        bytes32 fromBalanceSlot = keccak256(abi.encode(from, uint256(0)));
        bytes32 toBalanceSlot = keccak256(abi.encode(to, uint256(0)));
        PhEvm.ForkId memory preCall = PhEvm.ForkId({forkType: 2, callIndex: ctx.callStart});
        PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd});

        uint256 preFromBalance = uint256(ph.loadStateAt(address(protocol), fromBalanceSlot, preCall));
        uint256 preToBalance = uint256(ph.loadStateAt(address(protocol), toBalanceSlot, preCall));
        uint256 postFromBalance = uint256(ph.loadStateAt(address(protocol), fromBalanceSlot, postCall));
        uint256 postToBalance = uint256(ph.loadStateAt(address(protocol), toBalanceSlot, postCall));

        require(postFromBalance == preFromBalance - amount, "From balance mismatch in call frame");
        require(postToBalance == preToBalance + amount, "To balance mismatch in call frame");
    }
}

​
Implementation Notes

  • Call frame isolation:
    • Use registerFnCallTrigger() to execute once for each matched call
    • Use ph.context() to read the matched call’s callStart and callEnd
    • Construct PhEvm.ForkId({forkType: 2, callIndex: ctx.callStart}) and PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd}) for call-scoped snapshots
    • This allows validation at the individual function call level, not just transaction level
  • Benefits over transaction-level assertions:
    • Provides more precise state validation at the individual function call level
    • Allows validation of intermediate states within a transaction
    • Makes complex, multi-function transactions easier to validate
    • Can catch issues that would be masked by transaction-level checks
  • When to use call frame context vs transaction context:
    • Use call-scoped ForkId values when you need to validate individual calls within a transaction
    • Use transaction-scoped ForkId values when you only need to compare overall transaction state
    • Call frame context is especially useful for batch operations, multi-step protocols, or when validating intermediate states

​
Example Use Cases

  • Batch operations: Validate each individual operation within a batch transaction
  • Multi-step protocols: Check state at each step of a complex transaction
  • Oracle price updates: Verify each price update doesn’t exceed deviation limits (see Intra-TX Oracle Deviation)
  • Rate provider validation: Check rate changes before and after swaps (see Balancer V2 Stable Rate Exploit)

​
Implementation Considerations

  • Recursive function calls: Recursive calls compound state changes similar to transaction-level execution. Account for recursive call paths when precise call frame tracking is required.