-
Notifications
You must be signed in to change notification settings - Fork 15
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
Certora #1
base: main
Are you sure you want to change the base?
Certora #1
Conversation
env e; | ||
calldataarg args; | ||
f(e, args); | ||
assert false; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Better to make this rule with the calls to setup function and the use callFunctionSetParams, then we check that we don't have sanity issues due to the setup
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So you mean check reachability of 'callFunctionSetParams' ?
I can write it as a rule, though I already did.
Unreachability is obtained for the withdraw and receiveRewards functions, but this is intended, as to not let the user call those functions from L1 - this is a result of the alwaysUnSent(e) entrancy guard.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
in general, instead of f(e,args) use the callFunctionSetParams, and call the setup functions. they way you are more certain that you setup is ok. this will be good for others that might add more require to the setup
certora/specs/bridge.spec
Outdated
(getUnderlyingAssetHelper(AToken) == asset | ||
<=> | ||
getUnderlyingAssetOfAToken(AToken) == asset) | ||
filtered{f-> excludeInitialize(f)} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
what are we checking here? that the linkage is correct? is there a bug that you can insert to the code and this rule will fail?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This invariant is part of the setup (not explicitly), so I just wanted to check that there is consistency between the AToken contract value and the one in the bridge.
If someone were to write a flawed code, this would have been broken.
/* | ||
The following functions are used as summarization (under-approximation) | ||
for the real functions in the code rayMul and rayDiv. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this is equivalent to assuming that the index is 2, right? you can explain this so it will give the incentive for this.
One can instead of this use constantL1Index for specific rules, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The summarization allows any constant value for the index, not just 2. But it is a global requirement, i.e. for every call to this function, for every asset.
The function constantL1Index is asset dependent (and can be triggered on/off).
Only with the summarization one can reduce the run times.
No description provided.