Skip to content

Feat: add Certora specs #7

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.

Sign up for GitHub

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

Jump to bottom
Open
wants to merge 99 commits into
base: master
Choose a base branch
from
Open

Feat: add Certora specs #7

wants to merge 99 commits into from

Conversation

amusingaxl
Copy link
Contributor

No description provided.

oddaf and others added 30 commits February 14, 2025 00:04
@oddaf
initial implementation
e62ac29
@oddaf @amusingaxl
Update script/input/1/README.md
13e9d95 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf @amusingaxl
Update src/DSPC.sol
2d4ff02 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf @amusingaxl
Update src/DSPC.sol
2bccdbe 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf @amusingaxl
Update src/DSPC.sol
2c3f886 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf @amusingaxl
Update src/DSPC.sol
3c60b1f 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf
refactor: rename function put to set
52a59f7
@oddaf
fix: add check if data can be safely cast to uint16 in file()
c04ef6c
@oddaf
refactor: remove step restriction
d6ff178
@oddaf
chore: forge fmt
b341255
@oddaf
refactor: Update Set event to be emitted for each rate update
917eb4d
@oddaf @amusingaxl
Update src/deployment/DSPCInstance.sol
def70fa 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf @amusingaxl
Update src/deployment/DSPCInit.sol
9c2898d 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf @amusingaxl
Update src/deployment/DSPCInit.sol
b6c57c0 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf @amusingaxl
Update src/deployment/DSPCDeploy.sol
253af36 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf @amusingaxl
Update src/deployment/DSPCDeploy.sol
45a1834 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf @amusingaxl
Update src/deployment/DSPCDeploy.sol
cec6dc4 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf @amusingaxl
Update src/deployment/DSPCInit.sol
48b668a 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf
refactor: use addresses instead of interfaces in DSPCInstance to ease…
b9482c3 
… casting
@oddaf
fix: enforce min < max and max > min on file()
2274abe
@oddaf
fix: typo in RelyLike
75211ed
@oddaf @amusingaxl
Update src/DSPC.sol
3d3a515 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf
feat: dspc cooldown + step
b7dadb5
@oddaf
remove unnecessary setup from dspcMom test
0582668
@oddaf
chore: forge fmt
e03048f
@oddaf @amusingaxl
Apply suggestions from code review
d685819 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
@oddaf
fix: revert message in test
9dcf622
@oddaf
chore: forge fmt
0a79139
@oddaf
feat: improvements to initialization script
a47d4ff
@oddaf @amusingaxl
Apply suggestions from code review
4077e06 
Co-authored-by: amusingaxl <[email protected]>
Signed-off-by: oddaf <[email protected]>
amusingaxl and others added 8 commits March 28, 2025 09:13
@amusingaxl
refactor: formatting and cleanup
b156c66
@amusingaxl
feat: add Certora CI action
57f95dc
@oddaf
Rename module (DSPC -> SPBEAM) (#9)
4e7a435 
* refactor: rename module (DSPC -> SPBEAM)

* chore: formatting
@oddaf @amusingaxl
Rename module (DSPC -> SPBEAM) (#9)
2d04d2e 
* refactor: rename module (DSPC -> SPBEAM)

* chore: formatting
@amusingaxl
refactor: rename DSPC to SPBEAM
fcb2478
@amusingaxl
fix: remove MockerBrokenConv override
4507d0f 
The override was failing due to `ConvMock.btor` not being virtual. When I added the `virtual` modifier, for some reason `forge build --sizes` fail because the MockConv contract becomes too big.
@amusingaxl
Merge branch 'initial-implementation' into feat/certora-spec
ab956ec 
Signed-off-by: amusingaxl <[email protected]>
@amusingaxl
refactor: revert mock implementation change
e6ff425
@amusingaxl amusingaxl marked this pull request as ready for review March 28, 2025 13:32
pedrobergamini
pedrobergamini previously approved these changes Mar 28, 2025
View reviewed changes
Copy link

@pedrobergamini pedrobergamini left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me! Just commented an idea on Certora's GH actions workflow

pedrobergamini
pedrobergamini previously approved these changes Apr 2, 2025
View reviewed changes
certora/SPBEAM.spec
revert7 || revert8 || revert9 ||
revert10,
"set revert rules failed";
revert7 || revert8,
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice work on this change

sunbreak1211
sunbreak1211 reviewed Apr 9, 2025
View reviewed changes
sunbreak1211
sunbreak1211 reviewed Apr 9, 2025
View reviewed changes
sunbreak1211
sunbreak1211 reviewed Apr 9, 2025
View reviewed changes
@sunbreak1211
Copy link
Collaborator

Maybe an interesting rule/invariant to do, if you end up having some extra time, would be to prove that after any call to set, the values updated can not end up being outside the min-max range and always respect be restricted by the step.
Then the fix ordering can be roll back and check that the rule would have caught that. In either case those things are also indirectly proved with the current rules so not really mandatory, but I guess it would be a more high level rule that helps guaranteeing those invariants.

@amusingaxl
Copy link
Contributor Author

Maybe an interesting rule/invariant to do, if you end up having some extra time, would be to prove that after any call to set, the values updated can not end up being outside the min-max range and always respect be restricted by the step.

This was added in 67d5fbc.

Then the fix ordering can be roll back and check that the rule would have caught that.

Not entirely sure if I get what you're suggesting here.

Base automatically changed from initial-implementation to master April 22, 2025 12:50
@amusingaxl amusingaxl dismissed pedrobergamini’s stale review April 22, 2025 12:50

The base branch was changed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sunbreak1211 sunbreak1211 sunbreak1211 left review comments

@pedrobergamini pedrobergamini Awaiting requested review from pedrobergamini

At least 2 approving reviews are required to merge this pull request.

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@amusingaxl @sunbreak1211 @pedrobergamini @oddaf