example for the --contract_extensions_override flag

Author: naftali-g

CVLByExample/ExtensionContracts/OverrideExtended.conf

@@ -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,
+}

CVLByExample/ExtensionContracts/OverrideExtended.sol

@@ -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";
+    }
+}

CVLByExample/ExtensionContracts/OverrideExtended.spec

@@ -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;

CVLByExample/ExtensionContracts/README.md

@@ -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)