21.01.26 Release

21.01.26 Release

8bb19eca78af40b4f8b8003eaa399f18410cd2da

Author: yoav-el-certora

Public/CITests/testCertoraClient.py

@@ -787,6 +787,10 @@ def rem_quotes(string: str) -> str:
                 self.fail(f"test_jar_flag: failed for {args} - {e}")
 
     def test_validation_funcs(self) -> None:
+        VYPER_FILE = _p("V.vy")
+        with open(VYPER_FILE, "w") as file:
+                file.write("")
+
         attrs_with_validation: List[AttrUtil.AttributeDefinition] = []  # type: ignore
         for attr in Attrs.EvmProverAttributes.attribute_list():
             if attr.attr_validation_func != AttrUtil.default_validation:
@@ -816,6 +820,10 @@ def test_validation_funcs(self) -> None:
             if TestUtil.INVALID_KEY in tested_object:
                 TestUtil.validate_invalid_values(attr, tested_object[TestUtil.INVALID_KEY])
 
+
+        Path(VYPER_FILE).unlink(missing_ok=True)
+
+
     def test_package_file(self) -> None:
         def check_run(expect: List[str]) -> None:
             packages_attr = getattr(result, 'packages', None)

Public/CITests/testCertoraUtils.py

@@ -293,6 +293,16 @@ def path_test_file(filename: str) -> str:
         ]
     },
 
+    Vf.validate_vyper_custom_std_json_in_map: {
+        'valid': [
+            {path_test_file('V.vy'): path_test_file('erc20.json')}
+        ],
+        'invalid': [
+            {path_test_file('V.vy'): path_test_file('not_exist.json')},
+            {'notexist.vy': path_test_file('erc20.json')}
+        ]
+    },
+
     Vf.validate_solc_optimize_map: {
         'valid': [
             {'A': '15', 'B': '15', 'C.sol': '0'}

Public/TestEVM/Builtin/UncheckedOverflow/C.sol

@@ -0,0 +1,46 @@
+contract C {
+
+    function basicMul(uint x, uint y) public pure returns (uint)  {
+        unchecked {
+            return x * y;
+        }
+    }
+
+    function byConst(uint x) public pure returns (uint) {
+        unchecked {
+            return x * 7;
+        }
+    }
+
+    function mixed(uint x, uint y) public pure returns (int)  {
+        unchecked {
+            return int256(uint128(y) * x) + 7;
+        }
+    }
+
+    function twoMuls(uint x, uint y) public pure returns (uint)  {
+        unchecked {
+            return x * y * x;
+        }
+    }
+
+    function shouldPass(uint x, uint y)  public pure returns (uint)  {
+        require(x < 1000 && y < 1000);
+        unchecked {
+            return x * y;
+        }
+    }
+
+    function minus_fail(uint x, uint y) public pure returns (uint)  {
+        unchecked {
+            return x - y;
+        }
+    }
+
+    function minus_pass(uint x, uint y) public pure returns (uint)  {
+        require(x >= y);
+        unchecked {
+            return x - y;
+        }
+    }
+}

Public/TestEVM/Builtin/UncheckedOverflow/C.spec

@@ -0,0 +1 @@
+use builtin rule uncheckedOverflows;

Public/TestEVM/Builtin/UncheckedOverflow/Default.conf

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

Public/TestEVM/Builtin/UncheckedOverflow/expectedDefault.json

@@ -0,0 +1,23 @@
+{
+	"rules": {
+		"uncheckedOverflows": {
+			"FAIL": [
+				"basicMul(uint256,uint256)",
+				"byConst(uint256)",
+				"minus_fail(uint256,uint256)"
+			],
+			"SUCCESS": [
+				"minus_pass(uint256,uint256)",
+				"shouldPass(uint256,uint256)"
+			],
+			"mixed(uint256,uint256)": [
+				"FAIL",
+				"FAIL"
+			],
+			"twoMuls(uint256,uint256)": [
+				"FAIL",
+				"FAIL"
+			]
+		}
+	}
+}

Public/TestEVM/CVLCompilation/ArrayComparison/Default.conf

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

Public/TestEVM/CVLCompilation/ArrayComparison/Test.sol

@@ -0,0 +1,42 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+contract Test {
+    // Simple struct (no arrays)
+    struct SimpleStruct {
+        uint256 x;
+        int128 y;
+    }
+
+    // Struct with array field
+    struct StructWithArray {
+        uint256 id;
+        uint256[] values;
+    }
+
+    // Struct with nested struct and array
+    struct StructWithNestedAndArray {
+        SimpleStruct inner;
+        uint256[] arr;
+    }
+
+    // For testing array of structs
+    function createSimpleStruct(uint256 x, int128 y) external pure returns (SimpleStruct memory) {
+        return SimpleStruct(x, y);
+    }
+
+    function createIntArray(uint256 a, uint256 b, uint256 c) external pure returns (uint256[] memory) {
+        uint256[] memory arr = new uint256[](3);
+        arr[0] = a;
+        arr[1] = b;
+        arr[2] = c;
+        return arr;
+    }
+
+    function createStructWithArray(uint256 id, uint256 a, uint256 b) external pure returns (StructWithArray memory) {
+        uint256[] memory values = new uint256[](2);
+        values[0] = a;
+        values[1] = b;
+        return StructWithArray(id, values);
+    }
+}

Public/TestEVM/CVLCompilation/ArrayComparison/Test.spec

@@ -0,0 +1,89 @@
+using Test as test;
+
+methods {
+    function createSimpleStruct(uint256 x, int128 y) external returns (Test.SimpleStruct memory) envfree;
+    function createIntArray(uint256 a, uint256 b, uint256 c) external returns (uint256[] memory) envfree;
+    function createStructWithArray(uint256 id, uint256 a, uint256 b) external returns (Test.StructWithArray memory) envfree;
+}
+
+// Test 1: Compare primitive arrays (uint256[])
+rule comparePrimitiveArrays {
+    uint256[] arr1; uint256[] arr2;
+
+    // Can't use `<=>` here because that causes double polarity of the quantifier and breaks grounding
+    assert arr1 == arr2 => (arr1.length == arr2.length && (forall uint256 i. i < arr1.length => arr1[i] == arr2[i]));
+    assert (arr1.length == arr2.length && (forall uint256 i. i < arr1.length => arr1[i] == arr2[i])) => arr1 == arr2;
+}
+
+// Test 2: Reflexivity of array comparison
+rule arrayComparisonReflexive {
+    uint256[] arr;
+    assert arr == arr;
+}
+
+// Test 3: Symmetry of array comparison
+rule arrayComparisonSymmetric {
+    uint256[] arr1; uint256[] arr2;
+    assert (arr1 == arr2) == (arr2 == arr1);
+}
+
+// Test 4: Compare function return array
+rule compareFunctionReturnArray {
+    uint256 a; uint256 b; uint256 c;
+    uint256[] arr;
+    require arr.length == 3;
+    require arr[0] == a && arr[1] == b && arr[2] == c;
+    assert createIntArray(a, b, c) == arr;
+}
+
+// Test 5: Compare structs containing arrays
+rule compareStructsWithArrays {
+    Test.StructWithArray s1; Test.StructWithArray s2;
+    assert s1 == s2 <=> (s1.id == s2.id && s1.values == s2.values);
+}
+
+// Test 6: Compare structs with array - reflexive
+rule structWithArrayReflexive {
+    Test.StructWithArray s;
+    assert s == s;
+}
+
+// Test 7: Function returning struct with array
+rule compareFunctionReturnStructWithArray {
+    uint256 id; uint256 a; uint256 b;
+    Test.StructWithArray s;
+    require s.id == id;
+    require s.values.length == 2;
+    require s.values[0] == a && s.values[1] == b;
+    assert createStructWithArray(id, a, b) == s;
+}
+
+// Test 8: Different lengths means not equal
+rule differentLengthsNotEqual {
+    uint256[] arr1; uint256[] arr2;
+    require arr1.length != arr2.length;
+    assert arr1 != arr2;
+}
+
+// Test 9: Empty arrays are equal
+rule emptyArraysEqual {
+    uint256[] arr1; uint256[] arr2;
+    require arr1.length == 0;
+    require arr2.length == 0;
+    assert arr1 == arr2;
+}
+
+// Test 10: Compare int256 arrays
+rule compareIntArrays {
+    int256[] arr1; int256[] arr2;
+
+    // Can't use `<=>` here because that causes double polarity of the quantifier and breaks grounding
+    assert arr1 == arr2 => (arr1.length == arr2.length && (forall uint256 i. i < arr1.length => arr1[i] == arr2[i]));
+    assert (arr1.length == arr2.length && (forall uint256 i. i < arr1.length => arr1[i] == arr2[i])) => arr1 == arr2;
+}
+
+// Test 11: Compare struct with nested struct and array field
+rule compareStructWithNestedAndArray {
+    Test.StructWithNestedAndArray s1; Test.StructWithNestedAndArray s2;
+    assert s1 == s2 <=> (s1.inner.x == s2.inner.x && s1.inner.y == s2.inner.y && s1.arr == s2.arr);
+}

Public/TestEVM/CVLCompilation/ArrayComparison/expectedDefault.json

@@ -0,0 +1,22 @@
+{
+	"rules": {
+		"arrayComparisonReflexive": "SUCCESS",
+		"arrayComparisonSymmetric": "SUCCESS",
+		"compareFunctionReturnArray": "SUCCESS",
+		"compareFunctionReturnStructWithArray": "SUCCESS",
+		"compareIntArrays": "SUCCESS",
+		"comparePrimitiveArrays": "SUCCESS",
+		"compareStructWithNestedAndArray": "SUCCESS",
+		"compareStructsWithArrays": "SUCCESS",
+		"differentLengthsNotEqual": "SUCCESS",
+		"emptyArraysEqual": "SUCCESS",
+		"envfreeFuncsStaticCheck": {
+			"SUCCESS": [
+				"createIntArray(uint256,uint256,uint256)",
+				"createSimpleStruct(uint256,int128)",
+				"createStructWithArray(uint256,uint256,uint256)"
+			]
+		},
+		"structWithArrayReflexive": "SUCCESS"
+	}
+}