Exemplary ERC4626 specs - #3

Open

johspaeth wants to merge 127 commits into

Certora:masterfrom

johspaeth:johannes/erc4626-specs

Commits on Sep 12, 2023

Exemplary ERC4626 specs
Johannes Spaeth
committed
720e5e0
Adding missing library
Johannes Spaeth
committed
2370cc3
Adding minimal OpenZeppelin code
Johannes Spaeth
committed
de8b419
Adding config and rules adopted for Open Zeppelin
Johannes Spaeth
committed
60763f7
Modular verification
Johannes Spaeth
committed
fcc611b
Adding spec for singleUserBalanceSmallerThanTotalSupply for ERC4626, adding run script
Johannes Spaeth
committed
cb0d39b

Commits on Sep 13, 2023

Merge branch 'johannes/erc4626-specs' into johannes/openzeppelin
Johannes Spaeth
committed
016054b
Fixes spec after merge
Johannes Spaeth
committed
8f3118c
Introducing inflation bug
Johannes Spaeth
committed
641f676
Add info to bash script
Johannes Spaeth
committed
4189a10
Reverting introduction of bug and removing invariant that doesn't hold.
Johannes Spaeth
committed
c811e4c
Adding mirrorBalance and adding assumptions
Johannes Spaeth
committed
896ee63
Manually assuming totalSupply == sumOfBalances as invariant isn't working
Johannes Spaeth
committed
12b2a2f
Merge branch 'johannes/erc4626-specs' into johannes/openzeppelin
Johannes Spaeth
committed
9e2836b

Commits on Sep 15, 2023

Commits on Sep 18, 2023

Results for run: https://prover.certora.com/output/53900/878ce98bfb704d4b9b58defa3c0ea7bb?anonymousKey=d815027bcf06818470c7480c4843680ffe0cd305 with arguments src/certora/conf-openzeppelin/certoraR…
Johannes Spaeth
committed
69da824
Adding github action
Johannes Spaeth
committed
87350c9
Results for run: https://prover.certora.com/output/53900/dc0a906fad22482a88ea5ee7402898a8?anonymousKey=667f5ae97b65a5500a562af9184cf808aeac0b67 with arguments src/certora/conf-openzeppelin/certoraR…
Johannes Spaeth
committed
cf15714
Fixing github action
Johannes Spaeth
committed
0679447
Concretizing values
Johannes Spaeth
committed
3f3e57a
Fixing github action
Johannes Spaeth
committed
4458df5
Fixing github action
Johannes Spaeth
committed
f56040f
Fix receivers
Johannes Spaeth
committed
6aeb035
Simplifying withdraw logic (munging)
Johannes Spaeth
committed
9c37d73
Using non beta version of certora
Johannes Spaeth
committed
6c6b949
Removing non-linear math in function summary
Johannes Spaeth
committed
4898296
Removing non-linear math in function summary
Johannes Spaeth
committed
5d63179
Making mulDiv summary more precise
Johannes Spaeth
committed
bc417c3
Adding upper bound on mulDiv summary
Johannes Spaeth
committed
a76fb56
Relaxing lower bound
Johannes Spaeth
committed
d84b2f9
concretizing input share values
Johannes Spaeth
committed
023634f
Shares in range of 1 to 10.000
Johannes Spaeth
committed
4c35407
Select 3 values for shares, allow allowance case
Johannes Spaeth
committed
d1e5dd9
Parrallel proving OpenZeppelin and base implementation // require shares to be larger than 0
Johannes Spaeth
committed
64ce5d8
Fixing spec for non open zeppelin
Johannes Spaeth
committed
6f67c56
Loading values to displaying them in Certora variable view.
Johannes Spaeth
committed
dd25af7
Loading variables for certora to display
Johannes Spaeth
committed
95ff65b
Refining rule to get better counter example
Johannes Spaeth
committed
f44ea66
Limiting search space to get plausible counter example
Johannes Spaeth
committed
23a24cc
Limiting search space
Johannes Spaeth
committed
eda4c65
Adding missing requires
Johannes Spaeth
committed
da34f00

Commits on Sep 19, 2023

Duplicate rules for OpenZeppelin and base implementation
Johannes Spaeth
committed
21d0676
Starting point of rule writing of Rounding Props
Johannes Spaeth
committed
b68fa0f
First summary of mulDiv
Johannes Spaeth
committed
711d927
Removing mulDivSummary from parent spec file
Johannes Spaeth
committed
e715153
Fix rule
Johannes Spaeth
committed
ce6ebc6
Use lower and upper bounds to express summary of mulDiv // remove unused code
Johannes Spaeth
committed
feee058
Relaxation of mulDivSummary
Johannes Spaeth
committed
fcf1aec
Adding requirements to rule to find interesting CEXs // removing unnecessary rules for documentation purpose
Johannes Spaeth
committed
8bb3b6c
Use lower and upper bounds to express summary of mulDiv
Johannes Spaeth
committed
358eff9
Full relaxation of mulDivSummary
Johannes Spaeth
committed
33c3f0d
Removing safeAssumption to see if we run into a timeout
Johannes Spaeth
committed
51741e8
No safeAssumptions & requireuint summary
Johannes Spaeth
committed
b196cc2
Using relaxed summary for update function
Johannes Spaeth
committed
2f6b66d
Using fully relaxed summary in combination with ghost to bound results of convertToAssets/convertToShares
Johannes Spaeth
committed
5339cbb
Fixing shares to 10000
Johannes Spaeth
committed
a7ca05e
Fixing addresses
Johannes Spaeth
committed
e807845
Using yices
Johannes Spaeth
committed
f62f9ad

Commits on Sep 21, 2023

Basic version of inflation attack working for OpenZeppelin and base implementation
Johannes Spaeth
committed
76f3c8c
Duplicating code to separate buggy and non buggy version
Johannes Spaeth
committed
abcc64b
Adding buggy version
Johannes Spaeth
committed
aec6d79
Applying fix patch
Johannes Spaeth
committed
a793750
Prooving fixed version of inflation attack
Johannes Spaeth
committed
089de79

Commits on Sep 22, 2023

current state
Johannes Spaeth
committed
ca54ce1
Removing zeppelin specs
Johannes Spaeth
committed
169add5
Removing unnecessary files
Johannes Spaeth
committed
8f49b1d
Adding remaining TODOs
Johannes Spaeth
committed
6625384
Enabling all specs rules in GitHub Action
Johannes Spaeth
committed
a5ce305

Commits on Sep 28, 2023

Delete lesson4_reading/erc4626/src/certora/specs/ERC20-OZ-Modular.spec
johspaeth
authored
909ec7a

Commits on Oct 6, 2023

Adding rule relating increase in underlying vault to redeem of assets
Johannes Spaeth
committed
58daf52
Adding missing requireInvariant
Johannes Spaeth
committed
2e4c5cb