From 3ab0e91ceac0eaf8385319af045e4bad52f7b6c6 Mon Sep 17 00:00:00 2001 From: EyalHochCertora Date: Wed, 19 Apr 2023 12:21:04 +0300 Subject: [PATCH 01/11] CallResTable --- docs/prover/Report/CallResolutionTable.md | 56 +++++++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 docs/prover/Report/CallResolutionTable.md diff --git a/docs/prover/Report/CallResolutionTable.md b/docs/prover/Report/CallResolutionTable.md new file mode 100644 index 00000000..e15e3675 --- /dev/null +++ b/docs/prover/Report/CallResolutionTable.md @@ -0,0 +1,56 @@ +CallResolutionTable +================= + +The `CallResolutionTable` shows information about all the summarized calls in the program. +It helps the user to better understand decisions made by the Prover- which calls in the rule code got inlined, which were replaced by summaries, and why. + +Attributes +------ + + * **Caller**- The caller of the call. Always resolved by the Prover. + + * **Callee**- The callee of the call. For internal calls, always resolved. For external calls, might be unresolved, depending on linking, summarization, and more. +See below. + + * **Call Site**- source information of the call itself. Shows the location of the call (which file, which line), and a snippet from the source code (the invocation itself). + + * **Summary**- what summary got applied for the call. + + * **Comments**- a list of comments about the resolution of the callee (which as mentioned above, might be unresolved), the applied summarization. +See below. + + +The Callee +------ + +The callee is composed of two elements which should be taken into account: 1. Callee contract 2. Callee sighash. +The callee contract is the target contract of the call, the callee sighash is the sighash of the invoked function. +As mentioned above, for internal calls, the callee will always be resolved by the tool, while for external calls, it’s not always the case. +Here all the cases for unresolved callees are introduced: + + * Fully resolved callee: In such a case, the summary will be applied iff the application policy of the summary is `ALL` +(see {doc}`The Methods Block — Certora Prover Documentation 0.0 documentation `). +Notice, this does not mean that the call itself is resolved- it might happen, that both the callee contract and the callee sighash are resolved, but the sighash is not found in the contract. +This might happen, for example, due to a wrong linking in the configuration, or, due to a wrong low level call (`abi.encodeWithSignature("fdgf()")`), which is resolved in the bytecode level, even though it’s not an existing function signature. + + * Both callee contract, callee sighash are unresolved. + + * Callee contract unresolved, callee sighash resolved. + + * Callee Contract resolved, callee sighash unresolved. + + + Comments +------ + +In the comments, it is specified what is the resolution status of the callee. +In addition, they give more insights about why the prover failed to resolve the callee. +For example, if the callee contract is unresolved due to a wrong linking, a hint is given to the user, which specifies the slot that should be linked, and what are the possible contracts that should be considered to be linked (those that contain a function with the resolved sighash, if it is indeed resolved). +Moreover, the comments specify the summary application reason, which may be due to the configuration in the CLI, a summarization written in the spec, or a decision made by the Prover. +For example, if the Prover fails to resolve the callee, it decides to havoc the call. + + +Run Example with all the cases (rule per a case): +[Verification Report][report] + +[report]: https://vaas-stg.certora.com/output/20941/5deeb346152849f3976f4a68a30c8822?anonymousKey=1bf252ca0e1aae98e20d2daac6c0e6b3a03a0819 \ No newline at end of file From c921b5f0f0b774ae4071e42d9b02908114cdd9b5 Mon Sep 17 00:00:00 2001 From: EyalHochCertora Date: Tue, 25 Apr 2023 13:12:44 +0300 Subject: [PATCH 02/11] address review comments --- docs/prover/Report/CallResolutionTable.md | 37 +++++++++++++---------- 1 file changed, 21 insertions(+), 16 deletions(-) diff --git a/docs/prover/Report/CallResolutionTable.md b/docs/prover/Report/CallResolutionTable.md index e15e3675..9d4a25c7 100644 --- a/docs/prover/Report/CallResolutionTable.md +++ b/docs/prover/Report/CallResolutionTable.md @@ -1,37 +1,42 @@ 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: +1. Inlining- Taking the code of the two modules and building one big module with the code of both. +2. Summaries- 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. It helps the user to better understand decisions made by the Prover- which calls in the rule code got inlined, which were replaced by summaries, and why. Attributes ------ - * **Caller**- The caller of the call. Always resolved by the Prover. + * **Caller**- The maker of the call. Always resolved by the Prover. - * **Callee**- The callee of the call. For internal calls, always resolved. For external calls, might be unresolved, depending on linking, summarization, and more. + * **Callee**- The receiver of the call. For internal calls, always resolved. For external calls, might be unresolved, depending on linking, summarization, and more. See below. - * **Call Site**- source information of the call itself. Shows the location of the call (which file, which line), and a snippet from the source code (the invocation itself). + * **Call Site**- Source information of the call itself. This shows the location of the call file and also a snippet from the source code (the invocation). - * **Summary**- what summary got applied for the call. + * **Summary**- A brief summary of the call. - * **Comments**- a list of comments about the resolution of the callee (which as mentioned above, might be unresolved), the applied summarization. -See below. + * **Comments**- a list of comments about the resolution of the callee (as mentioned above, this might be unresolved). The Callee ------ -The callee is composed of two elements which should be taken into account: 1. Callee contract 2. Callee sighash. -The callee contract is the target contract of the call, the callee sighash is the sighash of the invoked function. -As mentioned above, for internal calls, the callee will always be resolved by the tool, while for external calls, it’s not always the case. +The callee is composed of two elements which should be taken into account: +1. Callee contract- This is the target contract of the call. +2. Callee sighash- This is the sighash of the invoked function. + +For internal calls, the callee will always be resolved by the Prover, while for external calls, this is not always the case. Here all the cases for unresolved callees are introduced: - * Fully resolved callee: In such a case, the summary will be applied iff the application policy of the summary is `ALL` + * Fully resolved callee: In such a case, the summary will be applied if the application policy of the summary is set to `ALL` (see {doc}`The Methods Block — Certora Prover Documentation 0.0 documentation `). -Notice, this does not mean that the call itself is resolved- it might happen, that both the callee contract and the callee sighash are resolved, but the sighash is not found in the contract. -This might happen, for example, due to a wrong linking in the configuration, or, due to a wrong low level call (`abi.encodeWithSignature("fdgf()")`), which is resolved in the bytecode level, even though it’s not an existing function signature. +Note, this does not mean that the call itself is resolved. There could be a case where both the callee contract and the callee sighash are resolved, but the sighash is not found in the contract. +This might happen, due to a wrong linking in the configuration, or, due to a wrong low level call (`abi.encodeWithSignature("fdgf()")`), which is resolved in the bytecode level, even though it’s not an existing function signature. * Both callee contract, callee sighash are unresolved. @@ -43,11 +48,11 @@ This might happen, for example, due to a wrong linking in the configuration, or, Comments ------ -In the comments, it is specified what is the resolution status of the callee. -In addition, they give more insights about why the prover failed to resolve the callee. -For example, if the callee contract is unresolved due to a wrong linking, a hint is given to the user, which specifies the slot that should be linked, and what are the possible contracts that should be considered to be linked (those that contain a function with the resolved sighash, if it is indeed resolved). +The comments, specify the resolution status of the callee. +In addition, they give more insights about why the Prover failed to resolve the callee. +For example, if the callee contract is unresolved due to wrong linking, a hint is given to the user. This hint specifies the slot that should be linked, and what are the possible contracts that should be considered when linking (those that contain a function with the resolved sighash, if it is indeed resolved). Moreover, the comments specify the summary application reason, which may be due to the configuration in the CLI, a summarization written in the spec, or a decision made by the Prover. -For example, if the Prover fails to resolve the callee, it decides to havoc the call. +For example, if the Prover fails to resolve the callee, it then decides to havoc the call. Run Example with all the cases (rule per a case): From 7237760056673f71ec6c4cc21e9c6271ed50da8d Mon Sep 17 00:00:00 2001 From: EyalHochCertora Date: Wed, 26 Apr 2023 19:52:06 +0300 Subject: [PATCH 03/11] a -> A --- docs/prover/Report/CallResolutionTable.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/Report/CallResolutionTable.md b/docs/prover/Report/CallResolutionTable.md index 9d4a25c7..e9f3a355 100644 --- a/docs/prover/Report/CallResolutionTable.md +++ b/docs/prover/Report/CallResolutionTable.md @@ -20,7 +20,7 @@ See below. * **Summary**- A brief summary of the call. - * **Comments**- a list of comments about the resolution of the callee (as mentioned above, this might be unresolved). + * **Comments**- A list of comments about the resolution of the callee (as mentioned above, this might be unresolved). The Callee From ce7217671ae89a0d43c08d99c79f23b83788f729 Mon Sep 17 00:00:00 2001 From: EyalHochCertora Date: Sat, 24 Jun 2023 19:02:49 +0300 Subject: [PATCH 04/11] summary types ref --- docs/prover/Report/CallResolutionTable.md | 9 ++++++--- spelling_wordlist.txt | 2 ++ 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/docs/prover/Report/CallResolutionTable.md b/docs/prover/Report/CallResolutionTable.md index e9f3a355..c6050472 100644 --- a/docs/prover/Report/CallResolutionTable.md +++ b/docs/prover/Report/CallResolutionTable.md @@ -3,7 +3,7 @@ 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: 1. Inlining- Taking the code of the two modules and building one big module with the code of both. -2. Summaries- 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). +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. It helps the user to better understand decisions made by the Prover- which calls in the rule code got inlined, which were replaced by summaries, and why. @@ -34,7 +34,7 @@ For internal calls, the callee will always be resolved by the Prover, while for Here all the cases for unresolved callees are introduced: * Fully resolved callee: In such a case, the summary will be applied if the application policy of the summary is set to `ALL` -(see {doc}`The Methods Block — Certora Prover Documentation 0.0 documentation `). +(see {ref}`summary types `). Note, this does not mean that the call itself is resolved. There could be a case where both the callee contract and the callee sighash are resolved, but the sighash is not found in the contract. This might happen, due to a wrong linking in the configuration, or, due to a wrong low level call (`abi.encodeWithSignature("fdgf()")`), which is resolved in the bytecode level, even though it’s not an existing function signature. @@ -58,4 +58,7 @@ For example, if the Prover fails to resolve the callee, it then decides to havoc Run Example with all the cases (rule per a case): [Verification Report][report] -[report]: https://vaas-stg.certora.com/output/20941/5deeb346152849f3976f4a68a30c8822?anonymousKey=1bf252ca0e1aae98e20d2daac6c0e6b3a03a0819 \ No newline at end of file +[report]: https://vaas-stg.certora.com/output/20941/5deeb346152849f3976f4a68a30c8822?anonymousKey=1bf252ca0e1aae98e20d2daac6c0e6b3a03a0819 + +(summary types)= +## Summary types \ No newline at end of file diff --git a/spelling_wordlist.txt b/spelling_wordlist.txt index c808884c..377945b3 100644 --- a/spelling_wordlist.txt +++ b/spelling_wordlist.txt @@ -142,3 +142,5 @@ verifier verifiers walkthrough whitespace +Inlining +callees From 01874cd27ff172f88092513e98db837b353386bc Mon Sep 17 00:00:00 2001 From: EyalHochCertora Date: Tue, 27 Jun 2023 18:14:31 +0300 Subject: [PATCH 05/11] add to doctree --- docs/prover/index.md | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/prover/index.md b/docs/prover/index.md index bdadcf99..07bc80cc 100644 --- a/docs/prover/index.md +++ b/docs/prover/index.md @@ -18,5 +18,6 @@ checking/index.md cli/index.md portal/using.md changelog.md +Report/CallResolutionTable.md ``` From 145ec6230489f4e090abcea86758a5f5e5476417 Mon Sep 17 00:00:00 2001 From: EyalHochCertora Date: Wed, 28 Jun 2023 16:47:34 +0300 Subject: [PATCH 06/11] link ref --- docs/cvl/methods.md | 1 + docs/prover/Report/CallResolutionTable.md | 64 ----------------------- docs/prover/index.md | 2 +- 3 files changed, 2 insertions(+), 65 deletions(-) delete mode 100644 docs/prover/Report/CallResolutionTable.md diff --git a/docs/cvl/methods.md b/docs/cvl/methods.md index 9d92c7e9..55f808a9 100644 --- a/docs/cvl/methods.md +++ b/docs/cvl/methods.md @@ -182,6 +182,7 @@ The `@dontsummarize` tag on method calls is currently undocumented but likely affects the summarization behavior. See {ref}`call-expr`. ``` +(summary-types)= Summary types ------------- diff --git a/docs/prover/Report/CallResolutionTable.md b/docs/prover/Report/CallResolutionTable.md deleted file mode 100644 index c6050472..00000000 --- a/docs/prover/Report/CallResolutionTable.md +++ /dev/null @@ -1,64 +0,0 @@ -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: -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. -It helps the user to better understand decisions made by the Prover- which calls in the rule code got inlined, which were replaced by summaries, and why. - -Attributes ------- - - * **Caller**- The maker of the call. Always resolved by the Prover. - - * **Callee**- The receiver of the call. For internal calls, always resolved. For external calls, might be unresolved, depending on linking, summarization, and more. -See below. - - * **Call Site**- Source information of the call itself. This shows the location of the call file and also a snippet from the source code (the invocation). - - * **Summary**- A brief summary of the call. - - * **Comments**- A list of comments about the resolution of the callee (as mentioned above, this might be unresolved). - - -The Callee ------- - -The callee is composed of two elements which should be taken into account: -1. Callee contract- This is the target contract of the call. -2. Callee sighash- This is the sighash of the invoked function. - -For internal calls, the callee will always be resolved by the Prover, while for external calls, this is not always the case. -Here all the cases for unresolved callees are introduced: - - * Fully resolved callee: In such a case, the summary will be applied if the application policy of the summary is set to `ALL` -(see {ref}`summary types `). -Note, this does not mean that the call itself is resolved. There could be a case where both the callee contract and the callee sighash are resolved, but the sighash is not found in the contract. -This might happen, due to a wrong linking in the configuration, or, due to a wrong low level call (`abi.encodeWithSignature("fdgf()")`), which is resolved in the bytecode level, even though it’s not an existing function signature. - - * Both callee contract, callee sighash are unresolved. - - * Callee contract unresolved, callee sighash resolved. - - * Callee Contract resolved, callee sighash unresolved. - - - Comments ------- - -The comments, specify the resolution status of the callee. -In addition, they give more insights about why the Prover failed to resolve the callee. -For example, if the callee contract is unresolved due to wrong linking, a hint is given to the user. This hint specifies the slot that should be linked, and what are the possible contracts that should be considered when linking (those that contain a function with the resolved sighash, if it is indeed resolved). -Moreover, the comments specify the summary application reason, which may be due to the configuration in the CLI, a summarization written in the spec, or a decision made by the Prover. -For example, if the Prover fails to resolve the callee, it then decides to havoc the call. - - -Run Example with all the cases (rule per a case): -[Verification Report][report] - -[report]: https://vaas-stg.certora.com/output/20941/5deeb346152849f3976f4a68a30c8822?anonymousKey=1bf252ca0e1aae98e20d2daac6c0e6b3a03a0819 - -(summary types)= -## Summary types \ No newline at end of file diff --git a/docs/prover/index.md b/docs/prover/index.md index 07bc80cc..0c6b334e 100644 --- a/docs/prover/index.md +++ b/docs/prover/index.md @@ -18,6 +18,6 @@ checking/index.md cli/index.md portal/using.md changelog.md -Report/CallResolutionTable.md +portal/CallResolutionTable.md ``` From a09da493031ef0efee7c33bc3fc0db3a333c1432 Mon Sep 17 00:00:00 2001 From: EyalHochCertora Date: Wed, 28 Jun 2023 17:42:01 +0300 Subject: [PATCH 07/11] CallResolutionTable.md inside portal dir --- docs/prover/portal/CallResolutionTable.md | 61 +++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 docs/prover/portal/CallResolutionTable.md diff --git a/docs/prover/portal/CallResolutionTable.md b/docs/prover/portal/CallResolutionTable.md new file mode 100644 index 00000000..ae7412be --- /dev/null +++ b/docs/prover/portal/CallResolutionTable.md @@ -0,0 +1,61 @@ +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: +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. +It helps the user to better understand decisions made by the Prover- which calls in the rule code got inlined, which were replaced by summaries, and why. + +Attributes +------ + + * **Caller**- The maker of the call. Always resolved by the Prover. + + * **Callee**- The receiver of the call. For internal calls, always resolved. For external calls, might be unresolved, depending on linking, summarization, and more. +See below. + + * **Call Site**- Source information of the call itself. This shows the location of the call file and also a snippet from the source code (the invocation). + + * **Summary**- A brief summary of the call. + + * **Comments**- A list of comments about the resolution of the callee (as mentioned above, this might be unresolved). + + +The Callee +------ + +The callee is composed of two elements which should be taken into account: +1. Callee contract- This is the target contract of the call. +2. Callee sighash- This is the sighash of the invoked function. + +For internal calls, the callee will always be resolved by the Prover, while for external calls, this is not always the case. +Here all the cases for unresolved callees are introduced: + + * Fully resolved callee: In such a case, the summary will be applied if the application policy of the summary is set to `ALL` +(see {ref}`summary-types`). +Note, this does not mean that the call itself is resolved. There could be a case where both the callee contract and the callee sighash are resolved, but the sighash is not found in the contract. +This might happen, due to a wrong linking in the configuration, or, due to a wrong low level call (`abi.encodeWithSignature("fdgf()")`), which is resolved in the bytecode level, even though it’s not an existing function signature. + + * Both callee contract, callee sighash are unresolved. + + * Callee contract unresolved, callee sighash resolved. + + * Callee Contract resolved, callee sighash unresolved. + + + Comments +------ + +The comments, specify the resolution status of the callee. +In addition, they give more insights about why the Prover failed to resolve the callee. +For example, if the callee contract is unresolved due to wrong linking, a hint is given to the user. This hint specifies the slot that should be linked, and what are the possible contracts that should be considered when linking (those that contain a function with the resolved sighash, if it is indeed resolved). +Moreover, the comments specify the summary application reason, which may be due to the configuration in the CLI, a summarization written in the spec, or a decision made by the Prover. +For example, if the Prover fails to resolve the callee, it then decides to havoc the call. + + +Run Example with all the cases (rule per a case): +[Verification Report][report] + +[report]: https://vaas-stg.certora.com/output/20941/5deeb346152849f3976f4a68a30c8822?anonymousKey=1bf252ca0e1aae98e20d2daac6c0e6b3a03a0819 \ No newline at end of file From b79b89804e0c4bf639871e97ca987e954144b78f Mon Sep 17 00:00:00 2001 From: EyalHochCertora Date: Wed, 28 Jun 2023 19:41:18 +0300 Subject: [PATCH 08/11] change ref --- docs/prover/portal/CallResolutionTable.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/prover/portal/CallResolutionTable.md b/docs/prover/portal/CallResolutionTable.md index ae7412be..16e0cf71 100644 --- a/docs/prover/portal/CallResolutionTable.md +++ b/docs/prover/portal/CallResolutionTable.md @@ -34,7 +34,7 @@ For internal calls, the callee will always be resolved by the Prover, while for Here all the cases for unresolved callees are introduced: * Fully resolved callee: In such a case, the summary will be applied if the application policy of the summary is set to `ALL` -(see {ref}`summary-types`). +(see {ref}`summaries`). Note, this does not mean that the call itself is resolved. There could be a case where both the callee contract and the callee sighash are resolved, but the sighash is not found in the contract. This might happen, due to a wrong linking in the configuration, or, due to a wrong low level call (`abi.encodeWithSignature("fdgf()")`), which is resolved in the bytecode level, even though it’s not an existing function signature. @@ -48,7 +48,7 @@ This might happen, due to a wrong linking in the configuration, or, due to a wro Comments ------ -The comments, specify the resolution status of the callee. +The comments specify the resolution status of the callee. In addition, they give more insights about why the Prover failed to resolve the callee. For example, if the callee contract is unresolved due to wrong linking, a hint is given to the user. This hint specifies the slot that should be linked, and what are the possible contracts that should be considered when linking (those that contain a function with the resolved sighash, if it is indeed resolved). Moreover, the comments specify the summary application reason, which may be due to the configuration in the CLI, a summarization written in the spec, or a decision made by the Prover. @@ -58,4 +58,4 @@ For example, if the Prover fails to resolve the callee, it then decides to havoc Run Example with all the cases (rule per a case): [Verification Report][report] -[report]: https://vaas-stg.certora.com/output/20941/5deeb346152849f3976f4a68a30c8822?anonymousKey=1bf252ca0e1aae98e20d2daac6c0e6b3a03a0819 \ No newline at end of file +[report]: https://vaas-stg.certora.com/output/20941/913f4cce938641a38c8fe1d37500d6e5?anonymousKey=d6d1bbd7bb0290b863ccd9b33905b96e91ad5373 \ No newline at end of file From d0b26012dedeb5256a17e3fe0767820a30620bcd Mon Sep 17 00:00:00 2001 From: EyalHochCertora Date: Wed, 28 Jun 2023 19:53:38 +0300 Subject: [PATCH 09/11] Revert "change ref" This reverts commit b79b89804e0c4bf639871e97ca987e954144b78f. --- docs/prover/portal/CallResolutionTable.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/prover/portal/CallResolutionTable.md b/docs/prover/portal/CallResolutionTable.md index 16e0cf71..ae7412be 100644 --- a/docs/prover/portal/CallResolutionTable.md +++ b/docs/prover/portal/CallResolutionTable.md @@ -34,7 +34,7 @@ For internal calls, the callee will always be resolved by the Prover, while for Here all the cases for unresolved callees are introduced: * Fully resolved callee: In such a case, the summary will be applied if the application policy of the summary is set to `ALL` -(see {ref}`summaries`). +(see {ref}`summary-types`). Note, this does not mean that the call itself is resolved. There could be a case where both the callee contract and the callee sighash are resolved, but the sighash is not found in the contract. This might happen, due to a wrong linking in the configuration, or, due to a wrong low level call (`abi.encodeWithSignature("fdgf()")`), which is resolved in the bytecode level, even though it’s not an existing function signature. @@ -48,7 +48,7 @@ This might happen, due to a wrong linking in the configuration, or, due to a wro Comments ------ -The comments specify the resolution status of the callee. +The comments, specify the resolution status of the callee. In addition, they give more insights about why the Prover failed to resolve the callee. For example, if the callee contract is unresolved due to wrong linking, a hint is given to the user. This hint specifies the slot that should be linked, and what are the possible contracts that should be considered when linking (those that contain a function with the resolved sighash, if it is indeed resolved). Moreover, the comments specify the summary application reason, which may be due to the configuration in the CLI, a summarization written in the spec, or a decision made by the Prover. @@ -58,4 +58,4 @@ For example, if the Prover fails to resolve the callee, it then decides to havoc Run Example with all the cases (rule per a case): [Verification Report][report] -[report]: https://vaas-stg.certora.com/output/20941/913f4cce938641a38c8fe1d37500d6e5?anonymousKey=d6d1bbd7bb0290b863ccd9b33905b96e91ad5373 \ No newline at end of file +[report]: https://vaas-stg.certora.com/output/20941/5deeb346152849f3976f4a68a30c8822?anonymousKey=1bf252ca0e1aae98e20d2daac6c0e6b3a03a0819 \ No newline at end of file From ca9d56bc6df86b0b7b43d203757926c5c06f6d9b Mon Sep 17 00:00:00 2001 From: EyalHochCertora Date: Wed, 28 Jun 2023 19:55:58 +0300 Subject: [PATCH 10/11] change ref --- docs/prover/portal/CallResolutionTable.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/prover/portal/CallResolutionTable.md b/docs/prover/portal/CallResolutionTable.md index ae7412be..661f25f8 100644 --- a/docs/prover/portal/CallResolutionTable.md +++ b/docs/prover/portal/CallResolutionTable.md @@ -34,7 +34,7 @@ For internal calls, the callee will always be resolved by the Prover, while for Here all the cases for unresolved callees are introduced: * Fully resolved callee: In such a case, the summary will be applied if the application policy of the summary is set to `ALL` -(see {ref}`summary-types`). +(see {ref}`summaries`). Note, this does not mean that the call itself is resolved. There could be a case where both the callee contract and the callee sighash are resolved, but the sighash is not found in the contract. This might happen, due to a wrong linking in the configuration, or, due to a wrong low level call (`abi.encodeWithSignature("fdgf()")`), which is resolved in the bytecode level, even though it’s not an existing function signature. @@ -48,7 +48,7 @@ This might happen, due to a wrong linking in the configuration, or, due to a wro Comments ------ -The comments, specify the resolution status of the callee. +The comments specify the resolution status of the callee. In addition, they give more insights about why the Prover failed to resolve the callee. For example, if the callee contract is unresolved due to wrong linking, a hint is given to the user. This hint specifies the slot that should be linked, and what are the possible contracts that should be considered when linking (those that contain a function with the resolved sighash, if it is indeed resolved). Moreover, the comments specify the summary application reason, which may be due to the configuration in the CLI, a summarization written in the spec, or a decision made by the Prover. From 58c4726d33f14dedb079ec4fe151e04e470b165a Mon Sep 17 00:00:00 2001 From: EyalHochCertora Date: Wed, 28 Jun 2023 20:04:46 +0300 Subject: [PATCH 11/11] remove summary types --- docs/cvl/methods.md | 1 - 1 file changed, 1 deletion(-) diff --git a/docs/cvl/methods.md b/docs/cvl/methods.md index 55f808a9..9d92c7e9 100644 --- a/docs/cvl/methods.md +++ b/docs/cvl/methods.md @@ -182,7 +182,6 @@ The `@dontsummarize` tag on method calls is currently undocumented but likely affects the summarization behavior. See {ref}`call-expr`. ``` -(summary-types)= Summary types -------------