8.3.0 Release

8.3.0 Release

0e592df020414bb7ba6b69c496735c3d1a7ec492

Author: yoav-el-certora

Public/CITests/testCertoraUtils.py

@@ -362,7 +362,7 @@ def path_test_file(filename: str) -> str:
         ]
     },
 
-    Vf.validate_rule_name: {
+    Vf.validate_evm_rule_name: {
         'valid': ['a', '_a123', '_'],
         'invalid': ['1', 'rule1 rule2', 'rule1,rule2']
     },
@@ -528,7 +528,7 @@ def path_test_file(filename: str) -> str:
         ]
     },
 
-    Vf.validate_method_flag: {
+    Vf.validate_evm_method_flag: {
         'valid': [
             "transfer(address,uint256)",
             "_Simple$.transfer(address,uint256)",
@@ -587,7 +587,7 @@ def get_valid_value(attr: AttrUtil.AttributeDefinition) -> str:
             return tested_object[VALID_KEY][0]
         else:
             raise Util.ImplementationError(f"No valid value for {attr.name}")
-    elif attr == Attrs.EvmAttributes.METHOD:
+    elif attr == Attrs.EvmProverAttributes.METHOD:
         return 'withdraw()'
     else:  # no validation function was defined, default type is used
         if attr.arg_type == AttrUtil.AttrArgType.STRING \

Public/TestEVM/EquivTest/Looping/Default.conf

@@ -0,0 +1,17 @@
+{
+    "equivalence_contracts": "C1=C2",
+    "files": [
+        "./Test.sol:C1",
+        "./Test.sol:C2"
+    ],
+    "loop_iter": 2,
+    "method": [
+        "entry(uint256,uint256,uint128)"
+    ],
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "prover_args": [
+        " -equivalenceCheck true -maxHeuristicFoldingDepth 5"
+    ],
+    "solc": "solc8.29"
+}

Public/TestEVM/EquivTest/Looping/Test.sol

@@ -0,0 +1,29 @@
+contract C1 {
+	event MyLog(uint indexed thing, bytes data);
+
+	function entry(uint count, uint256 a, uint128 b) external returns (uint) {
+		bytes memory cheeky = new bytes(48);
+		for(uint i = 0; i < count; i++) {
+			assembly {
+				mstore(add(cheeky, 0x20), 0)
+				mstore(add(cheeky, 0x30), b)
+				mstore(add(cheeky, 0x20), a)
+			}
+			emit MyLog(a, cheeky);
+		}
+		return count;
+	}
+}
+
+
+contract C2 {
+	event MyLog(uint indexed thing, bytes data);
+
+	function entry(uint count, uint256 a, uint128 b) external returns (uint) {
+		for(uint i = 0; i < count; i++) {
+			bytes memory data = abi.encodePacked(a, b);
+			emit MyLog(a, data);
+		}
+		return count;
+	}
+}

Public/TestEVM/EquivTest/Looping/expectedDefault.json

@@ -0,0 +1,5 @@
+{
+	"rules": {
+		"Equivalence of C1 and C2 on entry(uint256,uint256,uint128)": "SUCCESS"
+	}
+}

Public/TestEVM/Summarization/UnresolvedCallsSummary/C.sol

@@ -0,0 +1,20 @@
+contract C {
+    bytes public foo_returned;
+    int256 public bar_returned;
+    int public other_field;
+    function foo(address target, bytes memory data) external view returns (bytes memory) {
+        (bool success, bytes memory returndata) = target.staticcall(data);
+        require(success);
+        return returndata;
+    }
+    function bar(address target, bytes memory data) external view returns (bytes memory) {
+        (bool success, bytes memory returndata) = target.staticcall(data);
+        require(success);
+        return returndata;
+    }
+    function test(address target) external {
+        foo_returned = this.foo(target, abi.encodeWithSignature("getBytes()"));
+        bytes memory result = this.bar(target, abi.encodeWithSignature("getInt()"));
+        bar_returned = abi.decode(result, (int256));
+    }
+}

Public/TestEVM/Summarization/UnresolvedCallsSummary/Havoc.conf

@@ -0,0 +1,9 @@
+{
+    "files": [
+        "C.sol"
+    ],
+    "verify": "C:Havoc.spec",
+    "optimistic_loop": true,
+    "loop_iter": "3",
+    "solc": "solc8.0",
+}

Public/TestEVM/Summarization/UnresolvedCallsSummary/Havoc.spec

@@ -0,0 +1,16 @@
+methods {
+    unresolved external in foo(address,bytes) => HAVOC_ALL;
+    unresolved external in bar(address,bytes) => HAVOC_ALL;
+}
+
+rule test {
+    int other_fieldBefore = currentContract.other_field;
+    int bar_returnedBefore = currentContract.bar_returned;
+
+    env e;
+    address t;
+    test(e, t);
+
+    satisfy other_fieldBefore != currentContract.other_field
+        && bar_returnedBefore != currentContract.bar_returned;
+}

Public/TestEVM/Summarization/UnresolvedCallsSummary/Nondet.conf

@@ -0,0 +1,9 @@
+{
+    "files": [
+        "C.sol"
+    ],
+    "verify": "C:Nondet.spec",
+    "optimistic_loop": true,
+    "loop_iter": "3",
+    "solc": "solc8.0",
+}

Public/TestEVM/Summarization/UnresolvedCallsSummary/Nondet.spec

@@ -0,0 +1,16 @@
+methods {
+    unresolved external in foo(address,bytes) => NONDET;
+    unresolved external in bar(address,bytes) => NONDET;
+}
+
+rule test {
+    int other_fieldBefore = currentContract.other_field;
+    int bar_returnedBefore = currentContract.bar_returned;
+
+    env e;
+    address t;
+    test(e, t);
+
+    assert other_fieldBefore == currentContract.other_field;
+    satisfy bar_returnedBefore != currentContract.bar_returned;
+}

Public/TestEVM/Summarization/UnresolvedCallsSummary/expectedHavoc.json

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