Add Halmos FV for Packing and NoncesKeyed (#5847)

scripts/generate/templates/Packing.t.js

@@ -11,14 +11,14 @@ import {Packing} from "@openzeppelin/contracts/utils/Packing.sol";
 `;
 
 const testPack = (left, right) => `\
-function testPack(bytes${left} left, bytes${right} right) external pure {
+function testSymbolicPack(bytes${left} left, bytes${right} right) external pure {
     assertEq(left, Packing.pack_${left}_${right}(left, right).extract_${left + right}_${left}(0));
     assertEq(right, Packing.pack_${left}_${right}(left, right).extract_${left + right}_${right}(${left}));
 }
 `;
 
 const testReplace = (outer, inner) => `\
-function testReplace(bytes${outer} container, bytes${inner} newValue, uint8 offset) external pure {
+function testSymbolicReplace(bytes${outer} container, bytes${inner} newValue, uint8 offset) external pure {
     offset = uint8(bound(offset, 0, ${outer - inner}));
 
     bytes${inner} oldValue = container.extract_${outer}_${inner}(offset);

scripts/generate/templates/SlotDerivation.t.js

@@ -62,7 +62,7 @@ function testSymbolicDeriveMapping${name}(${type} key) public view {
 `;
 
 const mappingDirty = ({ type, name }) => `\
-function testSymbolicDeriveMapping${name}Dirty(bytes32 dirtyKey) public {
+function testSymbolicDeriveMapping${name}Dirty(bytes32 dirtyKey) public view {
     ${type} key;
     assembly {
         key := dirtyKey

test/utils/NoncesKeyed.t.sol

@@ -0,0 +1,51 @@
+// SPDX-License-Identifier: MIT
+// This file was procedurally generated from scripts/generate/templates/Packing.t.js.
+
+pragma solidity ^0.8.20;
+
+import {Test} from "forge-std/Test.sol";
+import {NoncesKeyed} from "@openzeppelin/contracts/utils/NoncesKeyed.sol";
+import {Nonces} from "@openzeppelin/contracts/utils/Nonces.sol";
+
+// CAUTION: Unsafe mock for testing purposes.
+contract NoncesKeyedMock is NoncesKeyed {
+    function useNonce(address owner, uint192 key) public returns (uint256) {
+        return _useNonce(owner, key);
+    }
+
+    function useCheckedNonce(address owner, uint192 key, uint64 nonce) public {
+        _useCheckedNonce(owner, key, nonce);
+    }
+}
+
+contract NoncesKeyedTest is Test {
+    NoncesKeyedMock private _mock;
+
+    function setUp() public {
+        _mock = new NoncesKeyedMock();
+    }
+
+    function testSymbolicUseNonce(address owner, uint192 key) public {
+        uint256 prevNonce = _mock.useNonce(owner, key);
+        assertEq(prevNonce + 1, _mock.nonces(owner, key));
+    }
+
+    function testSymbolicUseCheckedNonceLiveness(address owner, uint192 key) public {
+        uint256 currNonce = _mock.nonces(owner, key);
+
+        // Does not revert
+        _mock.useCheckedNonce(owner, key, uint64(currNonce));
+        assertEq(currNonce + 1, _mock.nonces(owner, key));
+    }
+
+    function testUseCheckedNonce(address owner, uint192 key, uint64 nonce) public {
+        uint256 currNonce = _mock.nonces(owner, key);
+
+        if (uint64(currNonce) == nonce) {
+            _mock.useCheckedNonce(owner, key, nonce);
+        } else {
+            vm.expectRevert(abi.encodeWithSelector(Nonces.InvalidAccountNonce.selector, owner, currNonce));
+            _mock.useCheckedNonce(owner, key, nonce);
+        }
+    }
+}

test/utils/SlotDerivation.t.sol

@@ -226,7 +226,7 @@ contract SlotDerivationTest is Test, SymTest {
         assertEq(baseSlot.deriveMapping(key), derivedSlot);
     }
 
-    function testSymbolicDeriveMappingBooleanDirty(bytes32 dirtyKey) public {
+    function testSymbolicDeriveMappingBooleanDirty(bytes32 dirtyKey) public view {
         bool key;
         assembly {
             key := dirtyKey
@@ -236,7 +236,7 @@ contract SlotDerivationTest is Test, SymTest {
         testSymbolicDeriveMappingBoolean(key);
     }
 
-    function testSymbolicDeriveMappingAddressDirty(bytes32 dirtyKey) public {
+    function testSymbolicDeriveMappingAddressDirty(bytes32 dirtyKey) public view {
         address key;
         assembly {
             key := dirtyKey