Required invariant minimal example

CVLByExample/Invariant/RequireInvariant/DataInvariant.conf

@@ -0,0 +1,6 @@
+{
+  "files": ["DataInvariant.sol"],
+  "verify": "DataInvariant:DataInvariant.spec",
+  "solc": "solc8.25",
+  "msg": "Verifying data invariants"
+}

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
+    }
+}

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);
+}

CVLByExample/Invariant/RequireInvariant/README.md

@@ -0,0 +1,35 @@
+# 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.
+
+the invariant won't be enforced at the time the hook triggered
+
+## 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 new semantics but not under the old semantics.
+  - **Hook**: When the contract reads `accessInvariant[user]`, we call a CVL function `safeAssumptions(user)` which has a `requireInvariant alwaysPositive(user)`.
+## How to Run
+
+1. **Command** the Solidity file and run the Certora Prover using the provided config:
+   ```bash
+   certoraRun DataInvariant.conf
+   ```
+
+## Execution Under the Old Semantic
+See the Certora Prover output:
+https://vaas-stg.certora.com/output/1512/b774667137d348039ab86be0f3a1b8f8?anonymousKey=cbd717f02b7ea78a275518c7c4ae340282789318
+- Expected outcome: The invariant verified incorrectly, allowing negative balances as long as they occur in the transaction but not after the transaction. This leads to incorrect assumptions about the state of the contract.
+
+## Execution Under the New Semantic
+See the Certora Prover output:
+https://vaas-stg.certora.com/output/1512/09d15b32556c469f9173b33b41e01711?anonymousKey=c1369211cc8d991e1f345d9012ef655dfb495d05
+- Expected outcome: The invariant correctly violated when a negative balance arises. This leads to incorrect assumptions about the state of the contract.