Update certora-cli to 7.3.0

[ernestognw]

Replaces #4957 and #5019

PR Checklist

• Tests
• Documentation
• Changeset entry (run npx changeset add)

[socket-security]

New and removed dependencies detected. Learn more about Socket for GitHub ↗︎

Package	New capabilities	Transitives	Size	Publisher
pypi/certora-cli@7.3.0	environment, eval, filesystem, network, shell Transitive: unsafe	+35	181 MB	certora, shellyg

View full report↗︎

[ernestognw]

The CI uses 0.8.24. When I compile locally with 0.8.25 everything works fine but switching to 0.8.24 produce the same results as the CI.

I'll keep investigating

[changeset-bot]

⚠️ No Changeset found

Latest commit: 42bf8c3

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

[Amxx]

Note: ERC721 safeMint and safeTransferFrom rules fail because failure of the underlying checkOnERC721Received is not modeled in the assert success <=> (...); description on liveness.

AFAIK, we a few options (in order of difficulty):

• require that to has no code in the rule
• require that to has no code, or that the check passes in the helper
• "leak" the data for the helper (return value) to verify the check in the liveness assert

[ernestognw]

Note: ERC721 safeMint and safeTransferFrom rules fail because failure of the underlying checkOnERC721Received is not modeled in the assert success <=> (...); description on liveness.

I am not sure of that since we're summarizing the result of an onERC721Received call so the checkOnERC721Received should not fail. The summarization is in certora/specs/methods/IERC721Receiver.spec.

Am I missing something?

[Amxx]

I'm not sure why that happens, but clearly there is an issue here

See this.