Implementing Assertions

Implementing Assertions

Turn a written invariant spec into a correct, gas-safe assertion contract.

Meta-Cognitive Protocol

Adopt the role of a Meta-Cognitive Reasoning Expert.

For every complex problem: 1.DECOMPOSE: Break into sub-problems 2.SOLVE: Address each with explicit confidence (0.0-1.0) 3.VERIFY: Check logic, facts, completeness, bias 4.SYNTHESIZE: Combine using weighted confidence 5.REFLECT: If confidence <0.8, identify weakness and retry For simple questions, skip to direct answer.

Always output: ∙Clear answer ∙Confidence level ∙Key caveats

When to Use

• Writing a new assertion contract from a defined invariant.
• Refactoring or optimizing existing assertions.
• Adding trigger logic, call input parsing, or event/state checks.

When NOT to Use

• You only need invariant ideation or trigger selection. Use designing-assertions.
• You only need testing patterns. Use testing-assertions.

Quick Start

Setup:

• Install the standard library: forge install phylaxsystems/credible-std (https://github.com/phylaxsystems/credible-std).
• Update remappings.txt with:
  • credible-std/=lib/credible-std/src/ (https://github.com/phylaxsystems/credible-std)
  • forge-std/=lib/forge-std/src/ (https://github.com/foundry-rs/forge-std)
• Credible cheatcodes (ph.*) are documented at https://docs.phylax.systems/credible/cheatcodes-overview and https://docs.phylax.systems/credible/cheatcodes-reference; use credible-std/src/PhEvm.sol in https://github.com/phylaxsystems/credible-std for the exact interface.
• Credible Layer overview: https://docs.phylax.systems/credible/credible-introduction.

File and Naming Conventions

• Assertion files: {ContractOrFeature}Assertion.a.sol (e.g., VaultOwnerAssertion.a.sol)
• Test files: {ContractOrFeature}Assertion.t.sol (e.g., VaultOwnerAssertion.t.sol)
• Assertion functions: must start with assertion followed by the property name (e.g., assertionOwnershipChange, assertionHealthFactor, assertionSupplyCap)
• Directory structure: assertions/src/ for assertion contracts, assertions/test/ for tests

contract MyAssertion is Assertion {
    function triggers() external view override {
        registerCallTrigger(this.assertionMonotonic.selector, ITarget.doThing.selector);
    }

    function assertionMonotonic() external {
        ITarget target = ITarget(ph.getAssertionAdopter());
        ph.forkPreTx();
        uint256 pre = target.totalAssets();
        ph.forkPostTx();
        uint256 post = target.totalAssets();
        require(post >= pre, "Invariant violated");
    }
}

Implementation Checklist

• Triggers: use the narrowest possible trigger; avoid global triggers (registerCallTrigger(fn) or registerStorageChangeTrigger(fn) without a selector/slot).
• One Trigger, One Assertion: avoid multi-selector dispatchers; register each selector to its own assertion function and reuse shared helpers.
• Interface Clarity: use selectors from the interface that declares the function; if the adopter inherits it (e.g., ERC20/4626), call that out so the trigger source is obvious.
• Pre/Post: call forkPreTx() only when needed; default is post-state.
• Call-Scoped Checks: use getCallInputs + forkPreCall/forkPostCall for per-call invariants.
• Call Input Shape: CallInputs.input contains args only (selector is stripped). Decode args directly; if you need msg.data (e.g., timelock keys), rebuild with abi.encodePacked(selector, input).
• Preconditions: use before* hook triggers or forkPreCall to assert pre-state requirements.
• Baselines: for intra-tx stability, read forkPreTx() once and compare per-call post snapshots.
• Event Parsing: filter by emitter and topics[0]; decode indexed vs data fields correctly.
• Storage Slots: use ph.load (not vm.load) for EIP-1967 slots, packed fields, and mappings; derive slots via forge inspect <Contract> storage-layout.
• State Changes: getStateChanges* includes the initial value at index 0; length 0 means no changes.
• Constructors: cheatcodes are unavailable; prefer ph.getAssertionAdopter() inside assertion functions and pass only constants via constructor args if needed.
• Nested Calls: avoid double counting; prefer getCallInputs to avoid proxy duplicates.
• Internal Calls: internal Solidity calls are not traced; register on external entrypoints (or this. calls) when you need call inputs.
• Batch Dedupe: deduplicate targets/accounts when a batch can repeat entries.
• Tolerances: use minimal, documented tolerances for price/decimals rounding.
• Optional Interfaces: use staticcall probing and skip when unsupported.
• Token Quirks: validate using balance deltas; handle fee-on-transfer and rebasing tokens.
• Packed Calldata: decode using protocol packing logic (assetId, amount, mode) and map ids via helpers.
• Delta-Based Supply Checks: compare totalSupply delta to sum of per-call amounts instead of enumerating users.
• Id Mapping Guards: if a packed id maps to address(0), skip or fail early to avoid false positives.
• Sentinel Amounts: normalize max/sentinel values (e.g., full repay/withdraw) using pre-state.
• Gas: assertion gas cap is 300k; happy path is often most expensive; early return, cache reads, and limit loops.
• Size Limit: organize assertions by domain (e.g., access control, timelock, accounting) and split if you hit CreateContractSizeLimit.

Anti-Patterns

❌ Dispatcher Pattern (Avoid)

Do not route multiple triggers through one assertion function that dispatches to helpers:

// ❌ WRONG: Many triggers → one dispatcher → helpers
function triggers() external view override {
    registerCallTrigger(this.assertionOwnership.selector, IVault.setFee.selector);
    registerCallTrigger(this.assertionOwnership.selector, IVault.setGuardian.selector);
    registerCallTrigger(this.assertionOwnership.selector, IVault.submitCap.selector);
}

function assertionOwnership() external {
    // Dispatches internally based on what was called - hard to debug, wastes gas
}

✅ One Trigger, One Assertion (Preferred)

Register each trigger to its own assertion function. Share logic via internal helpers:

// ✅ CORRECT: Each trigger has its own assertion function
function triggers() external view override {
    registerCallTrigger(this.assertionSetFee.selector, IVault.setFee.selector);
    registerCallTrigger(this.assertionSetGuardian.selector, IVault.setGuardian.selector);
    registerCallTrigger(this.assertionSubmitCap.selector, IVault.submitCap.selector);
}

function assertionSetFee() external {
    _checkOnlyOwner(); // Reuse helper
}

function assertionSetGuardian() external {
    _checkOnlyOwner(); // Reuse helper
}

❌ Mixed Interfaces (Avoid)

Do not mix selectors from parent and child interfaces:

// ❌ CONFUSING: Mixing IERC4626 and IVault when IVault extends IERC4626
registerCallTrigger(this.assertionDeposit.selector, IERC4626.deposit.selector);
registerCallTrigger(this.assertionSubmitCap.selector, IVault.submitCap.selector);

✅ Consistent Interface (Preferred)

Use the adopter's interface consistently:

// ✅ CLEAR: Use IVault for everything since it extends IERC4626
registerCallTrigger(this.assertionDeposit.selector, IVault.deposit.selector);
registerCallTrigger(this.assertionSubmitCap.selector, IVault.submitCap.selector);

Rationalizations to Reject

• "Use getAllCallInputs everywhere." It can double-count proxy calls.
• "Many selectors can share one assertion dispatcher." It hurts gas and makes debugging harder.
• "I can ignore nested calls." Batched flows are common and must be handled.
• "Events are enough." If events can be skipped, back them with state checks.
• "We can rely on storage layout guesses." Always derive slots from layout.

References

• Cheatcodes and Traces
• Storage Layouts and Slots
• Event Parsing
• Tolerance and Rounding
• Token Integration Safety