02.02.26 Release

02.02.26 Release

a52bf53a3af588bf44fb096b74d14aa12ce23259

Author: yoav-el-certora

Public/TestEVM/AssumptionFlags/AssumeNoCastingOverflow/C.sol

@@ -0,0 +1,12 @@
+contract C {
+
+    function narrow(int64 x) public pure returns (int32) {
+        int32 y = int32(x);
+        return y;
+    }
+
+    function unsignedToSigned(uint x) public pure returns (int)  {
+        return int(x);
+    }
+
+}

Public/TestEVM/AssumptionFlags/AssumeNoCastingOverflow/C.spec

@@ -0,0 +1,9 @@
+rule check1(int64 x) {
+    env e;
+    assert x == narrow(e, x);
+}
+
+rule check2(uint x) {
+    env e;
+    assert x == unsignedToSigned(e, x);
+}

Public/TestEVM/AssumptionFlags/AssumeNoCastingOverflow/Default.conf

@@ -0,0 +1,7 @@
+{
+    files: [
+        "C.sol",
+    ],
+    verify: "C:C.spec",
+    "solc": "solc8.28",
+}

Public/TestEVM/AssumptionFlags/AssumeNoCastingOverflow/WithAssume.conf

@@ -0,0 +1,8 @@
+{
+    files: [
+        "C.sol",
+    ],
+    verify: "C:C.spec",
+    "solc": "solc8.28",
+    "assume_no_casting_overflow": true
+}

Public/TestEVM/AssumptionFlags/AssumeNoCastingOverflow/expectedDefault.json

@@ -0,0 +1,6 @@
+{
+	"rules": {
+		"check1": "FAIL",
+		"check2": "FAIL"
+	}
+}

Public/TestEVM/AssumptionFlags/AssumeNoCastingOverflow/expectedWithAssume.json

@@ -0,0 +1,6 @@
+{
+	"rules": {
+		"check1": "SUCCESS",
+		"check2": "SUCCESS"
+	}
+}

Public/TestEVM/ExtensionContracts/Base1.sol

@@ -0,0 +1,46 @@
+import "Immutable.sol";
+
+contract Base1 is Immutable {
+    uint inExtension1;
+    uint inExtension2;
+
+    address extension1Address; // Address of contract Extension1
+
+    constructor(address _extension1Address) {
+        extension1Address = _extension1Address;
+    }
+
+    function callSetInExtension1(uint _num) external {
+        address(this).call(abi.encodeWithSignature("setInExtension1(uint256)", _num));
+    }
+
+    function callGetInExtension1() external returns (uint) {
+        (bool success, bytes memory b) = address(this).call(abi.encodeWithSignature("getInExtension1()"));
+        return abi.decode(b, (uint));
+    }
+
+    function callSetInExtension2(uint _num) external {
+        address(this).call(abi.encodeWithSignature("setInExtension2(uint256)", _num));
+    }
+
+    function callGetInExtension2() external returns (uint) {
+        (bool success, bytes memory b) = address(this).call(abi.encodeWithSignature("getInExtension2()"));
+        return abi.decode(b, (uint));
+    }
+
+    // Fallback function will handle all calls that don't match a function signature
+    fallback() external payable {
+        // Delegate the call to contract B
+        (bool success, ) = extension1Address.delegatecall(msg.data);
+        require(success, "Delegatecall failed");
+    }
+
+    function getImmut() public view returns (bytes32) {
+        return IMMUT1;
+    }
+
+    bool b;
+    function flipB() public {
+        b = !b;
+    }
+}

Public/TestEVM/ExtensionContracts/Base2.sol

@@ -0,0 +1,26 @@
+contract Base2 {
+    uint unused;
+    uint inExtension2;
+
+    address extension2Address; // Address of contract Extension1
+
+    constructor(address _extension2Address) {
+        extension2Address = _extension2Address;
+    }
+
+    function callSetInExtension2(uint _num) external {
+        address(this).call(abi.encodeWithSignature("setInExtension2(uint256)", _num));
+    }
+
+    function callGetInExtension2() external returns (uint) {
+        (bool success, bytes memory b) = address(this).call(abi.encodeWithSignature("getInExtension2()"));
+        return abi.decode(b, (uint));
+    }
+
+    // Fallback function will handle all calls that don't match a function signature
+    fallback() external payable {
+        // Delegate the call to contract B
+        (bool success, ) = extension2Address.delegatecall(msg.data);
+        require(success, "Delegatecall failed");
+    }
+}

Public/TestEVM/ExtensionContracts/Default.conf

@@ -0,0 +1,32 @@
+{
+    "files": [
+        "Base1.sol",
+        "Base2.sol",
+        "Extension1.sol",
+        "Extension2.sol",
+    ],
+    "link": [
+        "Extension1:base1=Base1",
+    ],
+    "solc": "solc8.25",
+    "verify": "Base1:test.spec",
+    "contract_extensions": {
+        "Base1": [
+            {
+                "extension": "Extension1",
+                "exclude": ["IMMUT1", "IMMUT2"],
+            },
+            {
+                "extension": "Extension2",
+                "exclude": [],
+            },
+        ],
+        "Base2": [
+            {
+                "extension": "Extension2",
+                "exclude": [],
+            },
+        ],
+    },
+    "rule_sanity": "basic",
+}

Public/TestEVM/ExtensionContracts/Extension1.sol

@@ -0,0 +1,33 @@
+import "Immutable.sol";
+import {Base1} from "Base1.sol";
+
+contract Extension1 is Immutable {
+    Base1 private immutable base1;
+    uint inExtension1;
+    uint inExtension2;
+
+    address extension2Address;
+
+    // Function that the base contract will delegate to
+    function setInExtension1(uint n) public {
+        inExtension1 = n;
+    }
+
+    function getInExtension1() public view returns (uint) {
+        return inExtension1;
+    }
+
+    fallback() external payable {
+        // Delegate the call to contract B
+        (bool success, ) = extension2Address.delegatecall(msg.data);
+        require(success, "Delegatecall failed");
+    }
+
+    function getExtensionImmut() public view returns (bytes32) {
+        return IMMUT1;
+    }
+
+    function callFlipB() public {
+        base1.flipB();
+    }
+}