8.4.3 Release

90eb59649f9e84bb4491031326ca3a50e58ac5a1

Author: yoav-el-certora

Public/TestEVM/EquivTest/TransparentCopy/Default.conf

@@ -0,0 +1,15 @@
+{
+    "equivalence_contracts": "V1=V2",
+    "files": [
+        "./Test.sol:V1",
+        "./Test.sol:V2"
+    ],
+    "method": [
+        "impl(address,bytes)"
+    ],
+    "optimistic_hashing": true,
+    "prover_args": [
+        " -equivalenceCheck true -maxHeuristicFoldingDepth 5"
+    ],
+    "solc": "solc8.29"
+}

Public/TestEVM/EquivTest/TransparentCopy/Test.sol

@@ -0,0 +1,12 @@
+contract V1 {
+    function impl(address a, bytes calldata g) external {
+		a.call(g);
+    }
+}
+
+contract V2 {
+    function impl(address a, bytes calldata g) external {
+		bytes memory buf = g;
+		a.call(buf);
+    }
+}

Public/TestEVM/EquivTest/TransparentCopy/expectedDefault.json

@@ -0,0 +1,5 @@
+{
+	"rules": {
+		"Equivalence of V1 and V2 on impl(address,bytes)": "SUCCESS"
+	}
+}

Public/TestEVM/Inlining/LateDelegateCallInlining/Test.conf

@@ -0,0 +1,13 @@
+{
+    "files": [
+        "Test.sol",
+        "Test.sol:Handler",
+        "Test.sol:Manager",
+    ],
+    "link": [
+        "Test:manager=Manager",
+        "Manager:handler=Handler"
+    ],
+    "solc": "solc8.22",
+    "verify": "Test:Test.spec"
+}

Public/TestEVM/Inlining/LateDelegateCallInlining/Test.sol

@@ -0,0 +1,37 @@
+interface ITest {
+	function beep() external returns (uint);
+}
+contract Handler {
+	function whatever() external returns (uint) {
+		return ITest(address(this)).beep();
+	}
+}
+
+contract Manager {
+	address immutable handler;
+
+	constructor(address _handler) {
+		handler = _handler;
+	}
+
+	function getHandler() external returns (address) {
+		return handler;
+	}
+}
+
+contract Test is ITest {
+	Manager manager;
+	function entry() external returns (uint) {
+        // This delegatecall cannot be resolved until after storage analysis, and so must be inlined late, during
+        // summarization.
+		(bool success, bytes memory ret) = address(manager.getHandler()).delegatecall(
+			abi.encodeCall(Handler.whatever, ())
+		);
+		require(success);
+		return abi.decode(ret, (uint));
+	}
+
+	function beep() external override returns (uint) {
+		return 987345;
+	}
+}

Public/TestEVM/Inlining/LateDelegateCallInlining/Test.spec

@@ -0,0 +1,4 @@
+rule test() {
+    env e;
+    assert entry(e) == 987345;
+}

Public/TestEVM/Inlining/LateDelegateCallInlining/expectedTest.json

@@ -0,0 +1,5 @@
+{
+	"rules": {
+		"test": "SUCCESS"
+	}
+}

Public/TestEVM/Regressions/CERT-9656/Default.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "./Test.sol:Test"
+    ],
+    "solc": "solc8.29",
+    "solc_via_ir": true,
+    "verify": "Test:./test.spec"
+}

Public/TestEVM/Regressions/CERT-9656/Test.sol

@@ -0,0 +1,43 @@
+uint constant DOUBLE_CACHE_LENGTH = 2;
+interface Intf {
+    struct SubStruct {
+        uint104 f1;
+        int104 f2;
+        uint48 f3;
+    }
+
+	struct SignedSubStruct {
+        int104 signedF1;
+        int104 f2;
+        uint48 f3;
+    }
+
+    struct Record {
+        SubStruct report;
+        uint96 f1;
+        uint96 f2;
+        SignedSubStruct[2] staticStructs;
+        uint128 postField1;
+        uint128 postField2;
+        uint128 postField3;
+        uint128 postField4;
+    }
+
+	function getRecord() external returns (Record memory);
+}
+
+contract Test {
+	address handler;
+
+	Intf.SignedSubStruct[2] field;
+
+	function entry() external returns (uint) {
+		Intf.Record memory record = Intf(handler).getRecord();
+		field = record.staticStructs;
+		return this.pleaseSummarize(record.postField4);
+	}
+
+    function pleaseSummarize(uint256 a) external returns (uint) {
+        return a + 1;
+    }
+}

Public/TestEVM/Regressions/CERT-9656/expectedDefault.json

@@ -0,0 +1,5 @@
+{
+	"rules": {
+		"basic_rule": "SUCCESS"
+	}
+}