Update FV specs and script #5786

Amxx · 2025-07-07T10:03:32Z

Fixes:

ERC20Wrapper
AccessManager
AccessManaged: https://discord.com/channels/795999272293236746/1391760909780914316

Todo:

CERTORAKEY
wait_for_results

changeset-bot · 2025-07-07T10:03:35Z

⚠️ No Changeset found

Latest commit: d9c9397

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

socket-security · 2025-07-07T14:13:53Z

Review the following changes in direct dependencies. Learn more about Socket for GitHub.

Diff	Package	Supply Chain Security	Vulnerability	Quality	Maintenance	License
	pypi/certora-cli@4.13.1 ⏵ 8.1.0	^-5				^-30

View full report

This reverts commit 1b324c7.

certora/specs/AccessControlDefaultAdminRules.spec

ernestognw · 2025-08-18T20:57:43Z

certora/specs/AccessManager.spec

+    } else if (
+        selector == to_bytes4(sig:labelRole(uint64,string).selector) ||
+        selector == to_bytes4(sig:setRoleAdmin(uint64,uint64).selector) ||
+        selector == to_bytes4(sig:setRoleGuardian(uint64,uint64).selector) ||
+        selector == to_bytes4(sig:setGrantDelay(uint64,uint32).selector) ||
+        selector == to_bytes4(sig:setTargetAdminDelay(address,uint32).selector)
+    ) {
+        assert restricted == true;
+        assert roleId     == ADMIN_ROLE();
+        assert delay      == 0;
+    } else if (
+        selector == to_bytes4(sig:updateAuthority(address,address).selector) ||
+        selector == to_bytes4(sig:setTargetClosed(address,bool).selector) ||
+        selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector)
+    ) {
+        assert restricted == true;
+        assert roleId     == ADMIN_ROLE();
+        assert delay      == getTargetAdminDelay(e, getFirstArgumentAsAddress(data));
+    } else if (
+        selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector) ||
+        selector == to_bytes4(sig:revokeRole(uint64,address).selector)
+    ) {
+        assert restricted == true;
+        assert roleId     == getRoleAdmin(getFirstArgumentAsUint64(data));
+        assert delay      == 0;
    } else {
-        assert restricted ==
-            isOnlyAuthorized(selector);
-
-        assert roleId == (
-            (restricted && selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector)) ||
-            (restricted && selector == to_bytes4(sig:revokeRole(uint64,address).selector      ))
-            ? getRoleAdmin(getFirstArgumentAsUint64(data))
-            : ADMIN_ROLE()
-        );
-
-        assert delay == (
-            (restricted && selector == to_bytes4(sig:updateAuthority(address,address).selector              )) ||
-            (restricted && selector == to_bytes4(sig:setTargetClosed(address,bool).selector                 )) ||
-            (restricted && selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector))
-            ? getTargetAdminDelay(e, getFirstArgumentAsAddress(data))
-            : 0
-        );
+        assert restricted == false;
+        assert roleId     == getTargetFunctionRole(currentContract, selector);
+        assert delay      == 0;


I think this version is clearer and more succinct

Suggested change

} else if (

selector == to_bytes4(sig:labelRole(uint64,string).selector) ||

selector == to_bytes4(sig:setRoleAdmin(uint64,uint64).selector) ||

selector == to_bytes4(sig:setRoleGuardian(uint64,uint64).selector) ||

selector == to_bytes4(sig:setGrantDelay(uint64,uint32).selector) ||

selector == to_bytes4(sig:setTargetAdminDelay(address,uint32).selector)

) {

assert restricted == true;

assert roleId == ADMIN_ROLE();

assert delay == 0;

} else if (

selector == to_bytes4(sig:updateAuthority(address,address).selector) ||

selector == to_bytes4(sig:setTargetClosed(address,bool).selector) ||

selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector)

) {

assert restricted == true;

assert roleId == ADMIN_ROLE();

assert delay == getTargetAdminDelay(e, getFirstArgumentAsAddress(data));

} else if (

selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector) ||

selector == to_bytes4(sig:revokeRole(uint64,address).selector)

) {

assert restricted == true;

assert roleId == getRoleAdmin(getFirstArgumentAsUint64(data));

assert delay == 0;

} else {

assert restricted ==

isOnlyAuthorized(selector);

assert roleId == (

(restricted && selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector)) ||

(restricted && selector == to_bytes4(sig:revokeRole(uint64,address).selector ))

? getRoleAdmin(getFirstArgumentAsUint64(data))

: ADMIN_ROLE()

);

assert delay == (

(restricted && selector == to_bytes4(sig:updateAuthority(address,address).selector )) ||

(restricted && selector == to_bytes4(sig:setTargetClosed(address,bool).selector )) ||

(restricted && selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector))

? getTargetAdminDelay(e, getFirstArgumentAsAddress(data))

: 0

);

assert restricted == false;

assert roleId == getTargetFunctionRole(currentContract, selector);

assert delay == 0;

assert restricted == isOnlyAuthorized(selector);

assert roleId == (

(restricted && selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector)) ||

(restricted && selector == to_bytes4(sig:revokeRole(uint64,address).selector ))

? getRoleAdmin(getFirstArgumentAsUint64(data))

: (restricted ? ADMIN_ROLE() : getTargetFunctionRole(currentContract, selector))

);

assert delay == (

(restricted && selector == to_bytes4(sig:updateAuthority(address,address).selector )) ||

(restricted && selector == to_bytes4(sig:setTargetClosed(address,bool).selector )) ||

(restricted && selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector))

? getTargetAdminDelay(e, getFirstArgumentAsAddress(data))

: 0

);

I think this is a matter of personal preference. They express the same thing in different ways.

One is saying:

Let take all the possible function selector and group them in categories. For each category we verify that the output (restricted, roleId, delay) is what we expect.

The other is saying "here is a rule for what the roleId should be, depending on a combination of factor (including but not limited to the function selector).

The second option is indeed shorter, but I don't think its clearer or more readable. There is more intricated logic, with nested ternary operators. Option one is longer, but IMO the logic is more clearly segmented.

@james-toussaint How do you feel, given that you are "new" to FV with certora, is there one syntax you find clearer / more readable ?

certora/specs/EnumerableMap.spec

ernestognw · 2025-08-18T21:57:02Z

certora/specs/EnumerableMap.spec

-        _positionOf(key) <= length() &&
-        key_at(require_uint256(_positionOf(key) - 1)) == key
-    )
+    (contains(key) <=> key_at(require_uint256(_positionOf(key) - 1)) == key) && _positionOf(key) <= length()
    {
        preserved remove(bytes32 otherKey) {


This is vacuous too for key arguments out of bounds, so we need the following:

Suggested change

preserved remove(bytes32 otherKey) {

preserved {

require lengthSanity();

}

preserved remove(bytes32 key) {

I don't observe that. I've been running without that preserve and the prover did not find any issue with this property

certora/specs/EnumerableMap.spec

certora/specs/EnumerableSet.spec

ernestognw · 2025-08-19T00:28:05Z

Merged this PR into #5844. We need the branch of the changes to belong to the repository in order to run the Formal Verification CI properly with access to the CERTORAKEY in secrets

Co-authored-by: Ernesto García <[email protected]>

…racts into FV/update

Amxx · 2025-08-19T16:10:37Z

Closed in favor of #5844

Update FV specs and run script

fe21b69

Amxx requested a review from a team as a code owner July 7, 2025 10:03

Amxx added ignore-changeset formal-verification Enable FV run in a PR. labels Jul 7, 2025

Amxx added 5 commits July 7, 2025 12:07

lint

1c59740

compiler version

bc75b11

Fix AccessManager rules following OpenZeppelin#5014

c8d3e0f

fix ERC20Wrapper specs

a3f9730

limit parallelism

7c05496

Amxx force-pushed the FV/update branch from 36c0883 to 7c05496 Compare July 7, 2025 14:07

Amxx added 2 commits July 7, 2025 16:11

stdout on error

b6fdd84

update certora version

d3fc14d

Amxx added 3 commits July 7, 2025 16:21

remove env key

1b324c7

Revert "remove env key"

ded2966

This reverts commit 1b324c7.

update

4ebeda4

Amxx mentioned this pull request Jul 9, 2025

Update dependency certora-cli to v7 #4957

Closed

1 task

Amxx added 3 commits August 18, 2025 14:00

8.1.0

08d2b6c

Merge branch 'master' into FV/update

e5c5812

some fixes

231e5d8

Amxx commented Aug 18, 2025

View reviewed changes

certora/specs/AccessControlDefaultAdminRules.spec Outdated Show resolved Hide resolved

Apply suggestions from code review

901f37b

Amxx mentioned this pull request Aug 18, 2025

Update dependency certora-cli to v8 #5844

Merged

1 task

fix AccessManaged

1f45198

Amxx mentioned this pull request Aug 18, 2025

Add Certora syntax highlighting #5861

Merged

ernestognw reviewed Aug 18, 2025

View reviewed changes

ernestognw force-pushed the FV/update branch from 3196c86 to 901f37b Compare August 19, 2025 00:31

Amxx mentioned this pull request Aug 19, 2025

Update FV specs and script #5863

Closed

Amxx and others added 3 commits August 19, 2025 10:46

Update certora/specs/EnumerableMap.spec

661fac9

Co-authored-by: Ernesto García <[email protected]>

Apply suggestions from code review

1c750fc

Co-authored-by: Ernesto García <[email protected]>

Merge branch 'FV/update' of https://github.com/Amxx/openzeppelin-cont…

d9c9397

…racts into FV/update

Amxx closed this Aug 19, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Update FV specs and script #5786

Update FV specs and script #5786

Uh oh!

Amxx commented Jul 7, 2025 •

edited

Loading

Uh oh!

changeset-bot bot commented Jul 7, 2025 •

edited

Loading

Uh oh!

socket-security bot commented Jul 7, 2025 •

edited

Loading

Uh oh!

Uh oh!

ernestognw Aug 18, 2025

Uh oh!

Amxx Aug 19, 2025

Uh oh!

Uh oh!

ernestognw Aug 18, 2025

Uh oh!

Amxx Aug 19, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ernestognw commented Aug 19, 2025

Uh oh!

Amxx commented Aug 19, 2025 •

edited

Loading

Uh oh!

Uh oh!

-        preserved remove(bytes32 otherKey) {
+        preserved {
+            require lengthSanity();
+        }
+        preserved remove(bytes32 key) {

Update FV specs and script #5786

Update FV specs and script #5786

Uh oh!

Conversation

Amxx commented Jul 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

changeset-bot bot commented Jul 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

⚠️ No Changeset found

Uh oh!

socket-security bot commented Jul 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

ernestognw Aug 18, 2025

Choose a reason for hiding this comment

Uh oh!

Amxx Aug 19, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

ernestognw Aug 18, 2025

Choose a reason for hiding this comment

Uh oh!

Amxx Aug 19, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ernestognw commented Aug 19, 2025

Uh oh!

Amxx commented Aug 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Amxx commented Jul 7, 2025 •

edited

Loading

changeset-bot bot commented Jul 7, 2025 •

edited

Loading

socket-security bot commented Jul 7, 2025 •

edited

Loading

Amxx commented Aug 19, 2025 •

edited

Loading