CERT 8687 Realistic example

CVLByExample/Invariant/RequireInvariantArray/README.md

@@ -0,0 +1,45 @@
+# Sorted Array Invariant Example
+
+This folder illustrates how the **new** `requireInvariant` semantics handle a **sorted array** property more accurately than the old semantics. We have:
+
+1. A **Solidity contract** (`SortedArray.sol`) that maintains an ascending-ordered array.
+2. A **CVL specification** that enforces a **“isSorted”** invariant using a **read hook**.
+
+Under the **old semantics**, the solver might incorrectly treat the invariant as satisfied inline, potentially missing real violations. Under the **new semantics**, the invariant is enforced at valid rule boundaries, catching unsorted states properly.
+
+---
+
+## Overview
+
+### `SortedArray.sol`
+- **`arr`**: A public array to remain sorted.
+- **`insert(uint256 val)`**: Inserts `val` into the correct position in ascending order.
+- **`remove(uint256 index)`**: Removes the element at `index`, shifting subsequent elements.
+- **`readAt(uint256 index)`**: Returns `arr[index]`, triggering our CVL read hook.
+
+### Specification Highlights
+- **`invariant isSorted(uint256 i)`**  
+  Requires that for each valid `i`, `arr[i] <= arr[i+1]`.  
+- **`hook Sload ... arr[INDEX uint256 index]`**  
+  Whenever `readAt(index)` is called, a CVL function `safeSortedAssumption(index)` invokes `requireInvariant isSorted(index)`.
+
+In **old semantics**, the check might be **inline**, potentially passing even if the array is temporarily unsorted. In **new semantics**, the captured indices are enforced at rule boundaries or after subcalls/havocs if `strong`, ensuring violations are caught.
+
+---
+
+## Comparing Execution Outputs
+
+- **Old Semantics**  
+  [View Output](https://vaas-stg.certora.com/output/1512/784d8a16d9c748ad980619483fe391b0?anonymousKey=4754ecd79909b410927a0af9c3d77afda15d6534)  
+  Result: The invariant may appear verified even in scenarios where the array is in fact unsorted (inside the transaction context).
+
+- **New Semantics**  
+  [View Output](https://vaas-stg.certora.com/output/1512/7cfd8d2823634113b906b60cba100e30?anonymousKey=176275751817ac50ed1647bc9bed70b700680b42)  
+  Result: Any genuine violation of sortedness is caught at rule boundaries, causing the verification to fail correctly.
+
+---
+
+## How to Run
+1. Use the Certora CLI:
+   ```bash
+   certoraRun SortedArray.conf

CVLByExample/Invariant/RequireInvariantArray/SortedArray.conf

@@ -0,0 +1,8 @@
+{
+  "files": ["SortedArray.sol"],
+  "verify": "SortedArray:SortedArray.spec",
+  "solc": "solc8.25",
+  "msg": "Verifying sorted array invariant",
+  "loop_iter": "5",
+  "optimistic_loop": true,
+}

CVLByExample/Invariant/RequireInvariantArray/SortedArray.sol

@@ -0,0 +1,51 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+/**
+ * @title SortedArray
+ * @notice A simple contract maintaining a sorted array of uint256
+ */
+contract SortedArray {
+    uint256[] public arr;
+
+    /**
+     * @notice Inserts a new value into the array, keeping it sorted in ascending order.
+     * @param val The value to insert
+     */
+    function insert(uint256 val) external {
+        // Simple linear approach:
+        // 1. Find the position where 'val' should go.
+        // 2. Insert it there, shifting subsequent elements.
+        uint256 pos = 0;
+        while (pos < arr.length && arr[pos] <= val) {
+            pos++;
+        }
+
+        // Insert by pushing a dummy at the end, then shifting
+        arr.push(val); // extends array by 1
+        for (uint256 i = arr.length - 1; i > pos; i--) {
+            arr[i] = arr[i - 1];
+        }
+        arr[pos] = val;
+    }
+
+    /**
+     * @notice Removes the element at index `index`. 
+     * @dev For simplicity, just shift down from 'index' onward; last element is pop'd.
+     */
+    function remove(uint256 index) external {
+        require(index < arr.length, "Index out of range");
+        for (uint256 i = index; i < arr.length - 1; i++) {
+            arr[i] = arr[i + 1];
+        }
+        arr.pop(); // remove the last element
+    }
+
+    /**
+     * @notice Returns the element at index `index`. 
+     * @dev Exposes array reads to demonstrate the read hook in CVL.
+     */
+    function readAt(uint256 index) external view returns (uint256) {
+        return arr[index];
+    }
+}

CVLByExample/Invariant/RequireInvariantArray/SortedArray.spec

@@ -0,0 +1,31 @@
+// ---------------------------------------------------------
+// 1. Declare the contract methods we want to call or inspect
+// ---------------------------------------------------------
+methods {
+    function insert(uint256) external envfree;
+    function remove(uint256) external envfree;
+    function readAt(uint256) external returns (uint256) envfree;
+}
+
+// ---------------------------------------------------------
+// 2. Define the sorted invariant: arr[i] <= arr[i+1] for all valid i, **Violated** under the new semantics and **Verified** under the old semantics.
+// ---------------------------------------------------------
+// Check array bounds carefully to avoid out-of-range checks
+// We only enforce i < arr.length - 1 => arr[i] <= arr[i+1]
+invariant isSorted(uint256 i) 
+    i < currentContract.arr.length - 1 => currentContract.arr[i] <= currentContract.arr[require_uint256(i + 1)];
+
+
+// ---------------------------------------------------------
+// 3. A function that calls 'requireInvariant' with the isSorted(i) invariant
+// ---------------------------------------------------------
+function safeSortedAssumption(uint256 i) {
+    requireInvariant isSorted(i);
+}
+
+// ---------------------------------------------------------
+// 4. Read Hook: whenever 'arr[i]' is accessed via 'readAt(i)', call 'safeSortedAssumption(i)'
+// ---------------------------------------------------------
+hook Sload uint256 ret currentContract.arr[INDEX uint256 index] {
+    safeSortedAssumption(index);
+}