DOC-302 Eyal h/call resolution table #74
Conversation
sammy-1234
changed the title
There was a problem hiding this comment.
There are errors in the build; see the Details under "all checks have failed". Looks like you need to update the index.md to add a link to the new page, and maybe fix some references as well.
The spelling errors can be fixed by adding any necessary correctly spelled words to spelling_wordlist.txt
This reverts commit b79b898.
|
@mdgeorge4153 Can you approve this? |
There was a problem hiding this comment.
It looks like I had a review queued up, maybe I didn't finish or forgot to submit. I remember @nd-certora saying that we should maybe not finish this one until we have more documentation in place for the rest of the rule report.
| @@ -18,5 +18,6 @@ checking/index.md | |||
| cli/index.md | |||
| portal/using.md | |||
| changelog.md | |||
| portal/CallResolutionTable.md | |||
There was a problem hiding this comment.
Putting the file here makes it show up in the wrong place in the table of contents. Instead, add it to the TOC of portal/using.md. Probably makes sense to rename using.md to index.md for consistency.
| @@ -0,0 +1,61 @@ | |||
| CallResolutionTable | |||
There was a problem hiding this comment.
This should be the title of a section, rather than a variable name. "Call Resolution Table"
| CallResolutionTable | ||
| ================= | ||
|
|
||
| The code verified by the Prover consists of several modules. However, by default, the Prover is aware of just one module. When the module is calling other modules, the Prover does not know how to identify them, let alone seeing and analyzing their code. In this case, the user guides the Prover by configuring it to identify the different modules and connect them through linking. This can be done through two ways: |
There was a problem hiding this comment.
What's a module? I think maybe you mean contract...
| ================= | ||
|
|
||
| The code verified by the Prover consists of several modules. However, by default, the Prover is aware of just one module. When the module is calling other modules, the Prover does not know how to identify them, let alone seeing and analyzing their code. In this case, the user guides the Prover by configuring it to identify the different modules and connect them through linking. This can be done through two ways: | ||
| 1. Inlining- Taking the code of the two modules and building one big module with the code of both. |
There was a problem hiding this comment.
A lot of this information is already in the multicontract user guide. This page should be focused on reading the output, rather than the theory of how the prover works. Relevant concepts should be linked (or use the glossary.. e.g. {term}`summarize` - terms are defined in docs/user-guide/glossary.md)
| @@ -0,0 +1,61 @@ | |||
| CallResolutionTable | |||
| ================= | |||
There was a problem hiding this comment.
A screenshot would be very helpful
| 1. Inlining- Taking the code of the two modules and building one big module with the code of both. | ||
| 2. Summarization- This is a mathematical description of the behavior of the module. It is usually short though less precise. It exists in two forms which are either be over approximating (describing more behaviors than there are actually implemented in the module) or under approximating (limiting the scope of what the other module can do). | ||
|
|
||
| The `CallResolutionTable` shows information about all the summarized calls in the program. |
There was a problem hiding this comment.
| The `CallResolutionTable` shows information about all the summarized calls in the program. | |
| The call resolution table shows information about all the summarized calls in the program. |
|
It does seem out of place to document the call resolution table with no guide whatsoever on the rule report. As it is dynamic I suggest to postpone working on this for now |
CallResolutionTable documentation, also referenced in: https://certora.atlassian.net/wiki/spaces/DR/pages/467501088/CallResolutionTable
Generated docs: https://certora-certora-prover-documentation--74.com.readthedocs.build/en/74/docs/prover/portal/CallResolutionTable.html