Skip to content

example for the --contract_extensions_override flag #207

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.

Sign up for GitHub

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

Open
naftali-g wants to merge 1 commit into
base: cli-beta
Choose a base branch
from
Open

example for the --contract_extensions_override flag #207

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 17 additions & 0 deletions CVLByExample/ExtensionContracts/OverrideExtended.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
{
"files": [
"OverrideExtended.sol:Extended",
"OverrideExtended.sol:Extender",
],
"solc": "solc8.25",
"verify": "Extended:OverrideExtended.spec",
"contract_extensions": {
"Extended": [
{
"extension": "Extender",
"exclude": [],
},
],
},
"contract_extensions_override": true,
}
15 changes: 15 additions & 0 deletions CVLByExample/ExtensionContracts/OverrideExtended.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
contract Extended {
function foo() external returns (string memory) {
return "Extended.foo";
}

function bar() external returns (string memory) {
return "Extended.bar";
}
}

contract Extender {
function foo() external returns (string memory) {
return "Extender.foo";
}
}
13 changes: 13 additions & 0 deletions CVLByExample/ExtensionContracts/OverrideExtended.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
using Extended as Extended;

rule overriddenReplaced {
env e;
assert Extended.foo(e) == "Extender.foo";
}

rule notOverriddenNotReplaced {
env e;
assert Extended.bar(e) == "Extended.bar";
}

use builtin rule sanity;
14 changes: 13 additions & 1 deletion CVLByExample/ExtensionContracts/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,4 +56,16 @@ Some more details:
Run this example using:
```certoraRun ExtensionContracts.conf```

[Report of this run](https://vaas-stg.certora.com/output/15800/8de64e410516472cbc8f7d6317059680?anonymousKey=b4b480e8209e59136b4daa281aa5159a1fc66fd1)
[Report of this run](https://vaas-stg.certora.com/output/15800/8de64e410516472cbc8f7d6317059680?anonymousKey=b4b480e8209e59136b4daa281aa5159a1fc66fd1)

## Extension Contracts Override

There are implementations of the proxy pattern in which the base contract actually has implementations for all the functions
that are implemented by the extension contracts - all they do is delegatecall the corresponding function in the extension contract. In this case
an extra flag needs to be set in order to avoid the Prover failing to "transfer" the functions from the extension contract into the
base one: `--contract_extensions_override`.

You can see adn run an example of this with
```certoraRun overrideExtended.conf```

[Report of this run](https://prover.certora.com/output/97560/68336a8a71aa42b2a66b512810b05b14?anonymousKey=f171bc0ba2d337fc4879f3165215904e72fb7416)