System Invariants
Relevant source files
The following files were used as context for generating this wiki page:
System Invariants in Canon Guard represent the core security properties and logical constraints that must remain true throughout the execution of any transaction or state transition. These invariants are primarily validated through property-based fuzzing and symbolic execution to ensure the multisig solution's integrity, specifically focusing on its time-lock mechanisms and Action Builder patterns.
The invariant testing suite is designed to prevent "frozen" states and ensure that the security provided by the underlying Safe contracts is not bypassed. It covers accounting limits, state consistency, and the strict timing requirements of the queued transaction lifecycle.
Sources: test/invariants/PROPERTIES.md:13-15, CLAUDE.md:25-27
Core Invariant Categories
The system's correctness is categorized into several logical domains, each targeting specific components like CanonGuard, ActionHub, and various Action Builders.
Approval and Timing Constraints
The system relies on a rigorous timeline for transaction execution. Transactions must transition through specific states (Queued -> Executable -> Expired) within predefined time windows.
| Invariant | Description |
|---|---|
invariant_transactionTimingIsCorrect | Ensures expiresAt > executableAt and executableAt >= queuedAt. |
invariant_approvalExpiriesAreValid | Approval durations cannot exceed the defined MAX_APPROVAL_DURATION. |
invariant_preApprovedTransactionsUsedShortDelay | Verifies that pre-approved actions correctly utilize the SHORT_TX_EXECUTION_DELAY. |
| Sources: test/invariants/PROPERTIES.md:29-33 |
Accounting and Cap Invariants
Action Builders like CappedTokenTransfers enforce volume limits. The system must ensure that these limits are never bypassed regardless of transaction frequency or epoch boundaries.
- Cap Integrity:
invariant_capNeverExceededensures that the cumulative value of transfers within a hub stays within the allowed cap, accounting for epoch resets.
Sources: test/invariants/PROPERTIES.md:20-22
State Consistency
The relationship between the internal queue (array) and the transaction information (mapping) must be perfectly synchronized to prevent orphaned transactions or inaccessible actions.
The diagram above illustrates the synchronization requirements between the queue data structures.
Sources: test/invariants/PROPERTIES.md:41-43
Testing Infrastructure
The project utilizes a multi-layered verification approach to maintain these invariants, integrating Medusa for fuzzing and Halmos for symbolic execution.
Fuzzing Configuration
The Medusa fuzzer is configured to target the FuzzTest contract, using a corpus-driven approach to discover edge cases that might violate system properties.
- Runs: 1000 fuzz runs by default (5000 in deep mode).
- Timeouts: 1000 seconds for invariant testing.
- Failure Mode:
fail_on_revert = trueto catch unexpected execution paths.
Sources: foundry.toml:28-34, package.json:28
Symbolic Execution
While fuzzing explores random paths, symbolic execution via Halmos is used to mathematically prove that certain properties cannot be violated under any possible input set.
Sources: README.md:52-54, package.json:27
Action Builder Architecture
The system's modularity is built around "Action Builders," which define specific transaction patterns. Each builder must adhere to the global guardrails while maintaining its own internal logic.
The class hierarchy shows how the CanonGuard interacts with hubs and builders to enforce transaction patterns.
Sources: CLAUDE.md:12-16, test/invariants/PROPERTIES.md:6-11
Relevant Components for Invariants
| Component | Responsibility in Invariants |
|---|---|
SafeEntrypoint | Main entry point for time-delayed executions. |
OnlyEntrypointGuard | Ensures bypasses are impossible. |
AllowanceClaimor | Subject to cap and accounting invariants. |
EmergencyModeHook | Mechanism to pause operations, effectively freezing the state in a controlled manner. |
| Sources: CLAUDE.md:12-18, test/invariants/PROPERTIES.md:6-11 |
Conclusion
System Invariants in Canon Guard provide a formal framework for security beyond standard unit testing. By enforcing strict rules on transaction timing, cap limits, and state consistency, the project ensures that the dynamic timelocks and on-chain actions operate predictably even under adversarial conditions. The integration of Medusa and Halmos provides both probabilistic and deterministic assurances that these invariants hold true.
Sources: test/invariants/PROPERTIES.md:13-17, README.md:48-54