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.

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

Add FV specification for ERC20Wrapper #4100

Merged
merged 15 commits into from
Mar 8, 2023
Merged

Add FV specification for ERC20Wrapper #4100

Changes from 1 commit
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
099bf14
Add FV specification for ERC20Wrapper
Amxx Mar 8, 2023
03c35b0
update run.js
Amxx Mar 8, 2023
2a74f88
lint
Amxx Mar 8, 2023
4a9b4d2
rewrite the rules as liveness/effect/no side effect
Amxx Mar 8, 2023
056cc3f
simplification
Amxx Mar 8, 2023
55aa62a
spacing
Amxx Mar 8, 2023
9f73887
spacing
Amxx Mar 8, 2023
ebf8df6
spacing
Amxx Mar 8, 2023
3e14352
refactor of helpers
Amxx Mar 8, 2023
1b621ad
make some assumptions explicit
Amxx Mar 8, 2023
df17e38
Update ERC20Wrapper.sol
frangio Mar 8, 2023
8c7ce2b
fix comment
frangio Mar 8, 2023
fbdbddd
Merge branch 'master' into fv/ERC20Wrapper
Amxx Mar 8, 2023
3800164
fix
Amxx Mar 8, 2023
0c57f1b
Update ERC20Wrapper.spec
Amxx Mar 8, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
spacing
  • Loading branch information
@Amxx
Amxx committed Mar 8, 2023
commit 55aa62a95eb6345837ab3f722431f143aa44984d
26 changes: 13 additions & 13 deletions certora/specs/ERC20Wrapper.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,17 +82,17 @@ rule depositFor(env e) {

// liveness
assert success <=> (
sender != 0 && // invalid sender
receiver != 0 && // invalid receiver
amount <= senderUnderlyingBalanceBefore && // deposit doesn't exceed balance
amount <= senderUnderlyingAllowanceBefore // deposit doesn't exceed allowance
sender != 0 && // invalid sender
receiver != 0 && // invalid receiver
amount <= senderUnderlyingBalanceBefore && // deposit doesn't exceed balance
amount <= senderUnderlyingAllowanceBefore // deposit doesn't exceed allowance
);

// effects
assert success => balanceOf(receiver) == balanceBefore + amount;
assert success => totalSupply() == supplyBefore + amount;
assert success => underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount;
assert success => underlyingBalanceOf(sender) == senderUnderlyingBalanceBefore - amount;
assert success => balanceOf(receiver) == balanceBefore + amount;
assert success => totalSupply() == supplyBefore + amount;
assert success => underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount;
assert success => underlyingBalanceOf(sender) == senderUnderlyingBalanceBefore - amount;
frangio marked this conversation as resolved.
Show resolved Hide resolved
frangio marked this conversation as resolved.
Show resolved Hide resolved

// no side effect
assert underlyingTotalSupply() == underlyingSupplyBefore;
Expand Down Expand Up @@ -133,14 +133,14 @@ rule withdrawTo(env e) {

// liveness
assert success <=> (
sender != 0 && // invalid sender
receiver != 0 && // invalid receiver
amount <= balanceBefore // withdraw doesn't exceed balance
sender != 0 && // invalid sender
receiver != 0 && // invalid receiver
amount <= balanceBefore // withdraw doesn't exceed balance
);

// effects
assert success => balanceOf(sender) == balanceBefore - amount;
assert success => totalSupply() == supplyBefore - amount;
assert success => balanceOf(sender) == balanceBefore - amount;
assert success => totalSupply() == supplyBefore - amount;
assert success => underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0);
assert success => underlyingBalanceOf(receiver) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0);

Expand Down