Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Regenerate SMTChecker report #704

Open
PaulRBerg opened this issue Oct 12, 2023 · 7 comments
Open

Regenerate SMTChecker report #704

PaulRBerg opened this issue Oct 12, 2023 · 7 comments
Assignees
Labels
effort: high Large or difficult task. priority: 3 Nice-to-have. Willing to ship without this. type: test Adding, updating, or removing tests. work: complex Probe-sense-respond. The relationship between cause and effect can only be perceived in retrospect.

Comments

@PaulRBerg
Copy link
Member

Investigate why it is failing:

https://github.com/sablier-labs/v2-core/actions/runs/6213048327

@PaulRBerg
Copy link
Member Author

PaulRBerg commented Oct 19, 2023

@andreivladbrg I would really like to generate this SMTChecker report before the audits start in November. Can you please work on this task?

@andreivladbrg
Copy link
Member

yes, next on my list

@andreivladbrg
Copy link
Member

I've been attempting to compile this full report for a couple of days now, but it simply won't complete. I even left my laptop on overnight to run the full report, but it didn't work for the lockupDynamic contract.

I'll leave the report for the linear contract below:

smtchecker-report-linear.txt

The result is odd, especially given that we have this configuration:

v2-core/foundry.toml

Lines 55 to 57 in 91887da

show_proved_safe = true
show_unproved = true
show_unsupported = true

I suspect this issue is related to the new Solidity version 0.8.21 we are using, it might not be fully supported yet.

@PaulRBerg
Copy link
Member Author

PaulRBerg commented Oct 27, 2023

I was expecting the report generation to take a long time.

But yes, the report is strange.

Don't worry in this case, I will pick up this task later. Thanks for your help.

@PaulRBerg
Copy link
Member Author

We should upload the SMTChecker report in the docs.

@PaulRBerg PaulRBerg assigned PaulRBerg and unassigned andreivladbrg Dec 8, 2023
@PaulRBerg PaulRBerg added effort: high Large or difficult task. work: complex Probe-sense-respond. The relationship between cause and effect can only be perceived in retrospect. type: test Adding, updating, or removing tests. priority: 3 Nice-to-have. Willing to ship without this. and removed backlog labels Jan 1, 2024

This comment was marked as resolved.

@github-actions github-actions bot added the stale Inactive for a long time. label Jul 7, 2024
@PaulRBerg

This comment was marked as resolved.

@github-actions github-actions bot removed the stale Inactive for a long time. label Jul 14, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
effort: high Large or difficult task. priority: 3 Nice-to-have. Willing to ship without this. type: test Adding, updating, or removing tests. work: complex Probe-sense-respond. The relationship between cause and effect can only be perceived in retrospect.
Projects
None yet
Development

No branches or pull requests

2 participants