Solve conflicts with halmos

.changeset/chilly-humans-warn.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`ProxyAdmin`: Fixed documentation for `UPGRADE_INTERFACE_VERSION` getter.

.changeset/cold-cheetahs-check.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`CircularBuffer`: Add a data structure that stores the last `N` values pushed to it.

.changeset/spotty-falcons-explain.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`Math`, `SignedMath`: Add a branchless `ternary` function that computes`cond ? a : b` in constant gas cost.

.github/actions/gas-compare/action.yml

@@ -1,4 +1,5 @@
 name: Compare gas costs
+description: Compare gas costs between branches
 inputs:
   token:
     description: github token

.github/actions/setup/action.yml

@@ -1,4 +1,5 @@
 name: Setup
+description: Common environment setup
 
 runs:
   using: composite

.github/actions/storage-layout/action.yml

@@ -1,4 +1,5 @@
 name: Compare storage layouts
+description: Compare storage layouts between branches
 inputs:
   token:
     description: github token

.github/workflows/checks.yml

@@ -93,9 +93,9 @@ jobs:
         uses: ./.github/actions/setup
       - name: Run coverage
         run: npm run coverage
-      - uses: codecov/codecov-action@v3
-        with:
-          token: ${{ secrets.CODECOV_TOKEN }}
+      - uses: codecov/codecov-action@v4
+        env:
+          CODECOV_TOKEN: ${{ secrets.CODECOV_TOKEN }}
 
   harnesses:
     runs-on: ubuntu-latest
@@ -115,7 +115,7 @@ jobs:
       - name: Set up environment
         uses: ./.github/actions/setup
       - run: rm foundry.toml
-      - uses: crytic/slither-action@v0.3.2
+      - uses: crytic/slither-action@v0.4.0
         with:
           node-version: 18.15
           slither-version: 0.10.1

.github/workflows/formal-verification.yml

@@ -44,12 +44,13 @@ jobs:
           fi
           echo "result=$RESULT" >> "$GITHUB_OUTPUT"
       - name: Install python
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: ${{ env.PIP_VERSION }}
           cache: 'pip'
+          cache-dependency-path: 'fv-requirements.txt'
       - name: Install python packages
-        run: pip install -r requirements.txt
+        run: pip install -r fv-requirements.txt
       - name: Install java
         uses: actions/setup-java@v3
         with:
@@ -66,3 +67,20 @@ jobs:
           node certora/run.js ${{ steps.arguments.outputs.result }} >> "$GITHUB_STEP_SUMMARY"
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+  halmos:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Set up environment
+        uses: ./.github/actions/setup
+      - name: Install python
+        uses: actions/setup-python@v5
+        with:
+          python-version: ${{ env.PIP_VERSION }}
+          cache: 'pip'
+          cache-dependency-path: 'fv-requirements.txt'
+      - name: Install python packages
+        run: pip install -r fv-requirements.txt
+      - name: Run Halmos
+        run: halmos --match-test '^symbolic|^testSymbolic' -vv

.gitmodules

@@ -5,3 +5,6 @@
 [submodule "lib/erc4626-tests"]
 	path = lib/erc4626-tests
 	url = https://github.com/a16z/erc4626-tests.git
+[submodule "lib/halmos-cheatcodes"]
+	path = lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes

contracts/governance/IGovernor.sol

@@ -145,7 +145,7 @@ interface IGovernor is IERC165, IERC6372 {
      * @dev Emitted when a vote is cast with params.
      *
      * Note: `support` values should be seen as buckets. Their interpretation depends on the voting module used.
-     * `params` are additional encoded parameters. Their interpepretation also depends on the voting module used.
+     * `params` are additional encoded parameters. Their interpretation  also depends on the voting module used.
      */
     event VoteCastWithParams(
         address indexed voter,

contracts/mocks/Stateless.sol

@@ -10,6 +10,7 @@ import {AuthorityUtils} from "../access/manager/AuthorityUtils.sol";
 import {Base64} from "../utils/Base64.sol";
 import {BitMaps} from "../utils/structs/BitMaps.sol";
 import {Checkpoints} from "../utils/structs/Checkpoints.sol";
+import {CircularBuffer} from "../utils/structs/CircularBuffer.sol";
 import {Clones} from "../proxy/Clones.sol";
 import {Create2} from "../utils/Create2.sol";
 import {DoubleEndedQueue} from "../utils/structs/DoubleEndedQueue.sol";
@@ -24,6 +25,7 @@ import {ERC721Holder} from "../token/ERC721/utils/ERC721Holder.sol";
 import {Math} from "../utils/math/Math.sol";
 import {MerkleProof} from "../utils/cryptography/MerkleProof.sol";
 import {MessageHashUtils} from "../utils/cryptography/MessageHashUtils.sol";
+import {Panic} from "../utils/Panic.sol";
 import {Packing} from "../utils/Packing.sol";
 import {SafeCast} from "../utils/math/SafeCast.sol";
 import {SafeERC20} from "../token/ERC20/utils/SafeERC20.sol";

contracts/proxy/transparent/ProxyAdmin.sol

@@ -12,10 +12,10 @@ import {Ownable} from "../../access/Ownable.sol";
  */
 contract ProxyAdmin is Ownable {
     /**
-     * @dev The version of the upgrade interface of the contract. If this getter is missing, both `upgrade(address)`
-     * and `upgradeAndCall(address,bytes)` are present, and `upgradeTo` must be used if no function should be called,
-     * while `upgradeAndCall` will invoke the `receive` function if the second argument is the empty byte string.
-     * If the getter returns `"5.0.0"`, only `upgradeAndCall(address,bytes)` is present, and the second argument must
+     * @dev The version of the upgrade interface of the contract. If this getter is missing, both `upgrade(address,address)`
+     * and `upgradeAndCall(address,address,bytes)` are present, and `upgrade` must be used if no function should be called,
+     * while `upgradeAndCall` will invoke the `receive` function if the third argument is the empty byte string.
+     * If the getter returns `"5.0.0"`, only `upgradeAndCall(address,address,bytes)` is present, and the third argument must
      * be the empty byte string if no function should be called, making it impossible to invoke the `receive` function
      * during an upgrade.
      */

contracts/utils/Arrays.sol

@@ -455,6 +455,7 @@ library Arrays {
      * WARNING: this does not clear elements if length is reduced, of initialize elements if length is increased.
      */
     function unsafeSetLength(address[] storage array, uint256 len) internal {
+        /// @solidity memory-safe-assembly
         assembly {
             sstore(array.slot, len)
         }
@@ -466,6 +467,7 @@ library Arrays {
      * WARNING: this does not clear elements if length is reduced, of initialize elements if length is increased.
      */
     function unsafeSetLength(bytes32[] storage array, uint256 len) internal {
+        /// @solidity memory-safe-assembly
         assembly {
             sstore(array.slot, len)
         }
@@ -477,6 +479,7 @@ library Arrays {
      * WARNING: this does not clear elements if length is reduced, of initialize elements if length is increased.
      */
     function unsafeSetLength(uint256[] storage array, uint256 len) internal {
+        /// @solidity memory-safe-assembly
         assembly {
             sstore(array.slot, len)
         }

contracts/utils/README.adoc

@@ -21,6 +21,7 @@ Miscellaneous contracts and libraries containing utility functions you can use t
  * {EnumerableMap}: A type like Solidity's https://solidity.readthedocs.io/en/latest/types.html#mapping-types[`mapping`], but with key-value _enumeration_: this will let you know how many entries a mapping has, and iterate over them (which is not possible with `mapping`).
  * {EnumerableSet}: Like {EnumerableMap}, but for https://en.wikipedia.org/wiki/Set_(abstract_data_type)[sets]. Can be used to store privileged accounts, issued IDs, etc.
  * {DoubleEndedQueue}: An implementation of a https://en.wikipedia.org/wiki/Double-ended_queue[double ended queue] whose values can be removed added or remove from both sides. Useful for FIFO and LIFO structures.
+ * {CircularBuffer}: A data structure to store the last N values pushed to it.
  * {Checkpoints}: A data structure to store values mapped to an strictly increasing key. Can be used for storing and accessing values over time.
  * {MerkleTree}: A library with https://wikipedia.org/wiki/Merkle_Tree[Merkle Tree] data structures and helper functions.
  * {Create2}: Wrapper around the https://blog.openzeppelin.com/getting-the-most-out-of-create2/[`CREATE2` EVM opcode] for safe use without having to deal with low-level assembly.
@@ -95,6 +96,8 @@ Ethereum contracts have no native concept of an interface, so applications must
 
 {{DoubleEndedQueue}}
 
+{{CircularBuffer}}
+
 {{Checkpoints}}
 
 {{MerkleTree}}

contracts/utils/math/Math.sol

@@ -73,18 +73,34 @@ library Math {
         }
     }
 
+    /**
+     * @dev Branchless ternary evaluation for `a ? b : c`. Gas costs are constant.
+     *
+     * IMPORTANT: This function may reduce bytecode size and consume less gas when used standalone.
+     * However, the compiler may optimize Solidity ternary operations (i.e. `a ? b : c`) to only compute
+     * one branch when needed, making this function more expensive.
+     */
+    function ternary(bool condition, uint256 a, uint256 b) internal pure returns (uint256) {
+        unchecked {
+            // branchless ternary works because:
+            // b ^ (a ^ b) == a
+            // b ^ 0 == b
+            return b ^ ((a ^ b) * SafeCast.toUint(condition));
+        }
+    }
+
     /**
      * @dev Returns the largest of two numbers.
      */
     function max(uint256 a, uint256 b) internal pure returns (uint256) {
-        return a > b ? a : b;
+        return ternary(a > b, a, b);
     }
 
     /**
      * @dev Returns the smallest of two numbers.
      */
     function min(uint256 a, uint256 b) internal pure returns (uint256) {
-        return a < b ? a : b;
+        return ternary(a < b, a, b);
     }
 
     /**
@@ -114,7 +130,7 @@ library Math {
         // but the largest value we can obtain is type(uint256).max - 1, which happens
         // when a = type(uint256).max and b = 1.
         unchecked {
-            return a == 0 ? 0 : (a - 1) / b + 1;
+            return SafeCast.toUint(a > 0) * ((a - 1) / b + 1);
         }
     }
 
@@ -147,7 +163,7 @@ library Math {
 
             // Make sure the result is less than 2²⁵⁶. Also prevents denominator == 0.
             if (denominator <= prod1) {
-                Panic.panic(denominator == 0 ? Panic.DIVISION_BY_ZERO : Panic.UNDER_OVERFLOW);
+                Panic.panic(ternary(denominator == 0, Panic.DIVISION_BY_ZERO, Panic.UNDER_OVERFLOW));
             }
 
             ///////////////////////////////////////////////
@@ -268,7 +284,7 @@ library Math {
             }
 
             if (gcd != 1) return 0; // No inverse exists.
-            return x < 0 ? (n - uint256(-x)) : uint256(x); // Wrap the result if it's negative.
+            return ternary(x < 0, n - uint256(-x), uint256(x)); // Wrap the result if it's negative.
         }
     }
 
@@ -295,7 +311,7 @@ library Math {
 
     /**
      * @dev Returns the modular exponentiation of the specified base, exponent and modulus (b ** e % m).
-     * It includes a success flag indicating if the operation succeeded. Operation will be marked has failed if trying
+     * It includes a success flag indicating if the operation succeeded. Operation will be marked as failed if trying
      * to operate modulo 0 or if the underlying precompile reverted.
      *
      * IMPORTANT: The result is only valid if the success flag is true. When using this function, make sure the chain

contracts/utils/math/SignedMath.sol

@@ -3,22 +3,40 @@
 
 pragma solidity ^0.8.20;
 
+import {SafeCast} from "./SafeCast.sol";
+
 /**
  * @dev Standard signed math utilities missing in the Solidity language.
  */
 library SignedMath {
+    /**
+     * @dev Branchless ternary evaluation for `a ? b : c`. Gas costs are constant.
+     *
+     * IMPORTANT: This function may reduce bytecode size and consume less gas when used standalone.
+     * However, the compiler may optimize Solidity ternary operations (i.e. `a ? b : c`) to only compute
+     * one branch when needed, making this function more expensive.
+     */
+    function ternary(bool condition, int256 a, int256 b) internal pure returns (int256) {
+        unchecked {
+            // branchless ternary works because:
+            // b ^ (a ^ b) == a
+            // b ^ 0 == b
+            return b ^ ((a ^ b) * int256(SafeCast.toUint(condition)));
+        }
+    }
+
     /**
      * @dev Returns the largest of two signed numbers.
      */
     function max(int256 a, int256 b) internal pure returns (int256) {
-        return a > b ? a : b;
+        return ternary(a > b, a, b);
     }
 
     /**
      * @dev Returns the smallest of two signed numbers.
      */
     function min(int256 a, int256 b) internal pure returns (int256) {
-        return a < b ? a : b;
+        return ternary(a < b, a, b);
     }
 
     /**