CERT 8687 Realistic example

CVLByExample/Invariant/RequireInvariantArray/README.md

@@ -0,0 +1,60 @@
+# Sorted Array Invariant Example
+
+This folder illustrates how the `requireInvariant` semantics in Prover version >= 8 handle a **sorted array** property more accurately than the semantics in version below 8. We have:
+
+## Key Points
+
+- **Version < 8 semantics**: Using `requireInvariant` in non-boundary contexts (e.g., hooks, summaries) could lead to false verification results. The invariant might be incorrectly considered satisfied inline, missing real violations.
+- **Version >= 8 semantics**: `requireInvariant` is enforced only at valid rule boundaries (e.g., after function calls, subcalls, or havocs if `strong`). This ensures that violations are properly detected.
+
+---
+
+## Example Overview
+
+### Solidity Contract: `SortedArray.sol`
+- **`arr`**: Public array, intended 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]`, used to trigger CVL read hooks.
+
+### CVL Specification
+- **Invariant**:  
+  `isSorted(uint256 i)` requires that for each valid `i`, `arr[i] <= arr[i+1]`.
+- **Hooks**:  
+  On every read or write to `arr[index]`, `requireInvariant isSorted(index)` is invoked.
+
+---
+
+## Demonstration: Correctness and Bug Detection
+
+### Correct Implementation
+
+- **Below version 8 semantics**:  
+  [View Output](https://prover.certora.com/output/40726/1636fb234bc74a1bba7f7ee9678b9c4f/?anonymousKey=ff15dfcf8a4da66107d4d7c7f04a49416e992b4d)  
+  *May incorrectly verify even if the array is temporarily unsorted.*
+
+- **Version >= 8 semantics**:  
+  [View Output](https://prover.certora.com/output/40726/5811d2a30ded4dcea82460a2d1d080ac/?anonymousKey=f296e69f8f0ea379cfba6801f1e4fee8f4d39c91)  
+  *Correctly enforces the invariant at rule boundaries.*
+
+### Buggy Implementation
+
+- **Below version 8 semantics**:  
+  [View Output](https://prover.certora.com/output/40726/ca7307d763104f8abdc1dc900d1c4e5e/?anonymousKey=2b6d5374b36f9e4990c7d825e6c9bb8a292db9d8)  
+  *Fails to catch the violation.*
+
+- **Version >= 8 semantics**:  
+  [View Output](https://prover.certora.com/output/40726/006db65557f94285af8bdbe0b8d1408f/?anonymousKey=abefdb1b51401cc4ed93ef57e70f4ed5b43bf579)  
+  *Correctly detects the violation.*
+
+---
+
+## How to Run
+
+1. Make sure you have the Certora CLI installed.
+2. Run the specification:
+   ```bash
+   certoraRun SortedArray.conf
+   ```
+
+---

CVLByExample/Invariant/RequireInvariantArray/SortedArray.conf

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

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,29 @@
+
+
+// ---------------------------------------------------------------
+// Define the sorted invariant: arr[i] <= arr[i+1] for all valid i
+// ---------------------------------------------------------------
+// Check array bounds carefully to avoid out-of-range checks
+invariant isSorted(uint256 i) 
+    i < currentContract.arr.length - 1 => currentContract.arr[i] <= currentContract.arr[require_uint256(i + 1)] ;
+
+
+// ----------------------------------------------------------------
+// An incorrect invariant that is not violated in the old semantics 
+// ----------------------------------------------------------------
+invariant incorrect(uint256 i) 
+    i < currentContract.arr.length => currentContract.arr[i] == 71;
+
+
+// ----------------------------------------------------------------------------
+// Load and Store Hooks: whenever 'arr[i]' is accessed assume the invariants 
+// ----------------------------------------------------------------------------
+hook Sload uint256 ret currentContract.arr[INDEX uint256 index] {
+        requireInvariant isSorted(index);
+        requireInvariant incorrect(index);
+}
+
+hook Sstore currentContract.arr[INDEX uint256 index]  uint256 val {
+        requireInvariant isSorted(index);
+        requireInvariant incorrect(index);
+}

CVLByExample/Invariant/RequireInvariantArray/SortedArrayBug.sol

@@ -0,0 +1,52 @@
+// 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];
+        }
+        // push to the wrongs place
+        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];
+    }
+}