diff --git a/CVLByExample/Invariant/RequireInvariant/DataInvariant.conf b/CVLByExample/Invariant/RequireInvariant/DataInvariant.conf new file mode 100644 index 00000000..89d970e0 --- /dev/null +++ b/CVLByExample/Invariant/RequireInvariant/DataInvariant.conf @@ -0,0 +1,6 @@ +{ + "files": ["DataInvariant.sol"], + "verify": "DataInvariant:DataInvariant.spec", + "solc": "solc8.25", + "msg": "Verifying data invariants" +} diff --git a/CVLByExample/Invariant/RequireInvariant/DataInvariant.sol b/CVLByExample/Invariant/RequireInvariant/DataInvariant.sol new file mode 100644 index 00000000..7fb153f8 --- /dev/null +++ b/CVLByExample/Invariant/RequireInvariant/DataInvariant.sol @@ -0,0 +1,23 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +/** + * @title DataInvariant + * @dev A contract with a per-address balance array and a function that can break an intended invariant. + */ +contract DataInvariant { + + mapping(address => int256) public balance; + mapping(address => bool) public accessInvariant; + + /** + * @notice Decreases the address's balance by 2*value and then partially restores it, + * potentially leaving it negative if `balance[a]` wasn't large enough. + */ + function breakInvariant(address a, int256 value) external returns (bool accessInv) { + require(value >= 0, "Value must be nonnegative"); + balance[a] -= 2 * value; // Force a large negative change + accessInv = accessInvariant[a]; // Read from the 'accessInvariant' mapping + balance[a] += value; // Restore half, potentially leaving negative + } +} diff --git a/CVLByExample/Invariant/RequireInvariant/DataInvariant.spec b/CVLByExample/Invariant/RequireInvariant/DataInvariant.spec new file mode 100644 index 00000000..6274c740 --- /dev/null +++ b/CVLByExample/Invariant/RequireInvariant/DataInvariant.spec @@ -0,0 +1,27 @@ +// -------------------------------------------------------- +// 1. Declare the methods we want to call or inspect +// -------------------------------------------------------- +methods { + function breakInvariant(address, int256) external returns bool envfree; + function accessInvariant(address) external returns bool envfree; +} + +// -------------------------------------------------------- +// 2. Define the invariant: alwaysPositive **should be violated** with the new semantics but should be verified with the old semantics +// -------------------------------------------------------- +invariant alwaysPositive(address a) + currentContract.balance[a] >= 0; + +// -------------------------------------------------------- +// 3. A helper function that enforces the invariant +// -------------------------------------------------------- +function safeAssumptions(address user) { + requireInvariant alwaysPositive(user); +} + +// -------------------------------------------------------- +// 4. Hook: whenever we read `accessInvariant[user]`, call `safeAssumptions(user)` +// -------------------------------------------------------- +hook Sload bool b currentContract.accessInvariant[KEY address user] { + safeAssumptions(user); +} diff --git a/CVLByExample/Invariant/RequireInvariant/README.md b/CVLByExample/Invariant/RequireInvariant/README.md new file mode 100644 index 00000000..c41bb780 --- /dev/null +++ b/CVLByExample/Invariant/RequireInvariant/README.md @@ -0,0 +1,42 @@ +# Data Invariant Example + +This folder shows a **simplified** demonstration of the new `requireInvariant` semantics in Certora’s CVL. We have: + +1. A **Solidity contract** (`DataInvariant.sol`) that allows negative balances to appear. +2. A **CVL specification** (`DataInvariant.spec`) that declares an invariant requiring **nonnegative** balances. +3. A **configuration file** (`DataInvariant.conf`) used to run the Certora Prover with our spec. + +> **Note:** The invariant is not enforced at the time the hook is triggered in versions **before 8**, but it is enforced globally in versions **from 8 on**. + +## Overview + +- **`DataInvariant.sol`** + A contract that tracks `balance[a]` for each address and includes the `breakInvariant` function. + +- **`DataInvariant.spec`** + - **Invariant**: `alwaysPositive(address a)` states `currentContract.balance[a] >= 0`. + The invariant is violated when `breakInvariant` is called under the semantics from version 8 on but not under the semantics before version 8. + - **Hook**: Whenever the contract reads `accessInvariant[user]` (i.e., an SLOAD on `accessInvariant[user]`), we call a CVL function `safeAssumptions(user)` which has a `requireInvariant alwaysPositive(user)`. + +**Explanation of `requireInvariant` semantics:** +- In versions **before 8**, `requireInvariant` was only enforced at the specific location where it was used (inside the hook, when `accessInvariant[user]` is read). This means the invariant is not guaranteed to hold globally—only at the hook point. + - a) Negative balances can exist during a transaction, as long as the invariant holds at the hook location. +- In versions **from 8 on**, the `requireInvariant` command is enforced globally—meaning the invariant must hold before any code of a rule or invariant is executed, not just at the hook. + - b) Negative balances are never allowed at any point where the invariant is expected to hold, so the violation is detected. + +## How to Run + +1. **Command** the Solidity file and run the Certora Prover using the provided config: + ```bash + certoraRun DataInvariant.conf + ``` + +## Execution Before Version 8 +See the Certora Prover output: +https://vaas-stg.certora.com/output/1512/b774667137d348039ab86be0f3a1b8f8?anonymousKey=cbd717f02b7ea78a275518c7c4ae340282789318 +- Expected outcome: The invariant is only checked at the hook, so negative balances can exist temporarily during a transaction, leading to incorrect assumptions about the state of the contract. + +## Execution From Version 8 On +See the Certora Prover output: +https://vaas-stg.certora.com/output/1512/09d15b32556c469f9173b33b41e01711?anonymousKey=c1369211cc8d991e1f345d9012ef655dfb495d05 +- Expected outcome: The invariant is enforced globally, so any negative balance is detected as a violation, ensuring the contract state always satisfies the invariant.