Liav/cert 7804 trusted methods #149
Conversation
Co-authored-by: yoav-el-certora <[email protected]>
liav-certora
requested review from
nd-certora,
shoham-certora and
yoav-el-certora
|
|
||
| Run this example using: | ||
| ```certoraRun Example.conf``` | ||
| [A report of this run](https://vaas-stg.certora.com/output/15800/7329f2dcf86c49f6b96891439eeaa467?anonymousKey=cde57e9e5f2ab7c5300399cdaa97585add830664) |
There was a problem hiding this comment.
give a link to prover.cerotra.com
| Foo bar = Foo(userTrustedContractAddress); | ||
| return bar.trusted(); | ||
| } | ||
| } |
There was a problem hiding this comment.
can we show more complicated examples? I'm not sure what will happen when the resolution is via spec/smt:
for example: 1. passing the target as a parameter and having a dispatcher:
2. an unresolved call the we have a in the spec "unresolved call"
There was a problem hiding this comment.
I'll try to play with this a bit.
There was a problem hiding this comment.
Ok, I tried some things but I probably didn't fully understand you.
I mainly tried to add an example for a function that will call an arbitrary function on Foo and then have a dispatch list such that any unresolved calls in that function will go to Foo.trusted() and this was the result.
If that's important it would be helpful if you could elaborate a little bit about what you meant please :)
There was a problem hiding this comment.
@johspaeth you might be able to help here 😬
There was a problem hiding this comment.
Using a dispatcher is currently not expected to work here, the check is implemented as a built-in rule and these don't apply the CVL summaries at all. (Exactly as use builtin rule sanity;)
The current use case we have is actually for byte code analysis to have a simple analysis that detects method calls that are to unknown target / unknown sighashes. If we have more use cases, we can change the logic and allow CVL summarization etc, for now I don't see this critical though.
There was a problem hiding this comment.
Thanks for the clarification @johspaeth 🙏
No description provided.