Relevant source files

The following files were used as context for generating this wiki page: - [test/invariants/PROPERTIES.md](https://github.com/defi-wonderland/canon-guard/blob/main/test/invariants/PROPERTIES.md) - [CLAUDE.md](https://github.com/defi-wonderland/canon-guard/blob/main/CLAUDE.md) - [README.md](https://github.com/defi-wonderland/canon-guard/blob/main/README.md) - [package.json](https://github.com/defi-wonderland/canon-guard/blob/main/package.json) - [foundry.toml](https://github.com/defi-wonderland/canon-guard/blob/main/foundry.toml) - [medusa.json](https://github.com/defi-wonderland/canon-guard/blob/main/medusa.json)

# System Invariants 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_capNeverExceeded` ensures 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. ```mermaid flowchart TD A[Queue Array] <-->|Must be in sync| B[Transactions Mapping] B --> C{Non-zero Expiry?} C -- Yes --> D[Builder exists in Queue] C -- No --> E[Builder NOT in Queue] D --> F[invariant_queueMappingConsistency] ``` 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 = true` to 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. ```mermaid classDiagram class ActionHub { <> +manageBuilders() } class CanonGuard { +checkTransaction() +queueTransaction() } class ActionBuilder { <> +buildAction() } ActionHub <|-- SimpleActions ActionHub <|-- CappedTokenTransfers CanonGuard --> ActionHub : Validates ActionHub --> ActionBuilder : Uses ``` 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]()