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	0	22.7 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: 1e70e61

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.

[ernestognw]

Attempted to retake this, and found a couple of issues. New errors appear in pretty much every spec, similar to the following:

EVM instruction at PC 2786 jumps to unknown destination 5140, from 2783#2705/16. Possible unresolved function pointer.

Also the CLI hangs up when I run node certora/run.js --all, and most importantly, the Certora Prover and the CLI report the jobs succeded even though the verification of multiple rules failed. My guess is that they might have changed the definition of what a successful verification is, possibly affecting our CI as well.

Here's how Certora is presenting the status as passed although rules didn't: