12.02.26 Release

12.02.26 Release

9e6c54f0588d545afa38db49e18043ca5a93310d

Author: yoav-el-certora

.circleci/config.yml

@@ -385,13 +385,6 @@ jobs:
       - attach_workspace:
           at: ~/
       - release_certora_cli
-      - run:
-          name: Create mutation container
-          command: |
-            curl -X POST https://circleci.com/api/v2/project/gh/Certora/mutation-test-container/pipeline \
-            --header "Circle-Token: $CIRCLE_TOKEN" \
-            --header "content-type: application/json" \
-            --data '{"branch":"master"}'
 
   upload_artifact:
       parameters:

Public/TestEVM/AddressFunctionCallsAmbig/Contracts.sol

@@ -0,0 +1,81 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+// Contract A: transfer() returning bool
+contract A {
+    bool public executed;
+
+    function transfer() external returns (bool) {
+        executed = true;
+        return true;
+    }
+}
+
+// Contract B: transfer() returning void
+contract B {
+    bool public executed;
+
+    function transfer() external {
+        executed = true;
+    }
+}
+
+// Contract C: multi() returning (uint, uint)
+contract C {
+    function multi() external pure returns (uint, uint) {
+        return (42, 84);
+    }
+}
+
+// Contract D: multi() returning (uint)
+contract D {
+    function multi() external pure returns (uint) {
+        return (100);
+    }
+}
+
+// Contract E: transfer() returning bool (same as A, tests multiple matching)
+contract E {
+    function transfer() external returns (bool) {
+        return false;
+    }
+}
+
+// Contract F: getValue() returning uint8
+contract F {
+    function getValue() external pure returns (uint8) {
+        return 42;
+    }
+}
+
+// Contract G: getValue() returning uint256
+contract G {
+    function getValue() external pure returns (uint256) {
+        return 100;
+    }
+}
+
+// Contract H: getPair() returning (uint, bool)
+contract H {
+    function getPair() external pure returns (uint, bool) {
+        return (1, true);
+    }
+}
+
+// Contract I: getPair() returning (bool, uint)
+contract I {
+    function getPair() external pure returns (bool, uint) {
+        return (true, 2);
+    }
+}
+
+// Contract J: getTriple() returning (uint, uint, uint)
+contract J {
+    function getTriple() external pure returns (uint, uint, uint) {
+        return (1, 2, 3);
+    }
+}
+
+// Main contract for verification
+contract Main {
+}

Public/TestEVM/AddressFunctionCallsAmbig/Contracts.spec

@@ -0,0 +1,123 @@
+using A as a;
+using B as b;
+using C as c;
+using D as d;
+using E as ee;
+using F as f;
+using G as g;
+using H as h;
+using I as i;
+using J as j;
+
+// TEST 1: Explicit bool type declaration -> dispatches to A (returns bool)
+rule explicitBoolTypeDispatchesToA(env e) {
+    address addr;
+    bool result = addr.transfer(e);
+    assert addr == a || addr == ee, "Explicit bool LHS should dispatch to contract A";
+    assert addr == a => result == true;
+    assert addr == ee => result == false;
+}
+
+// TEST 2: Command form (no LHS) -> should work with A, B, E
+rule commandFormWorksWithVoid(env e) {
+    address addr;
+    addr.transfer(e);  // No return value captured
+    assert addr == a || addr == b || addr == ee, "Command form should accept all";
+}
+
+// TEST 3: Multi-return with two variables -> dispatches to C (uint, uint)
+rule multiReturnTwoVarsDispatchesToC(env e) {
+    address addr;
+    uint x;
+    uint y;
+    x, y = addr.multi(e);
+    assert addr == c, "Two LHS vars should dispatch to C";
+    assert x == 42 && y == 84;
+}
+
+// TEST 4: Single return -> dispatches to D (uint)
+rule singleReturnDispatchesToD(env e) {
+    address addr;
+    uint result = addr.multi(e);
+    assert addr == d, "Single LHS var should dispatch to D";
+    assert result == 100;
+}
+
+// TEST 5: Assignment without type declaration (variable pre-declared)
+rule assignmentToPreDeclaredBoolVar(env e) {
+    address addr;
+    bool existingVar;
+    existingVar = addr.transfer(e);  // No type on this line, but existingVar is bool
+    assert addr == a || addr == ee, "Pre-declared bool var should provide type hint";
+}
+
+// TEST 6: Assignment without type declaration for uint
+rule assignmentToPreDeclaredUintVar(env e) {
+    address addr;
+    uint existingVar;
+    existingVar = addr.multi(e);  // No type on this line
+    assert addr == d, "Pre-declared uint var should dispatch to D";
+}
+
+// TEST 7: Multiple contracts with same return type - both are valid targets
+rule multipleMatchingContractsBool(env e) {
+    address addr;
+    bool result = addr.transfer(e);
+    // Both A and E return bool
+    assert addr == a || addr == ee, "Both A and E should be valid for bool return";
+}
+
+// TEST 8: Subtype - uint8 result assigned to uint256 variable
+rule subtypeUint8ToUint256(env e) {
+    address addr;
+    uint256 result = addr.getValue(e);
+    // G returns uint256 (exact match), F returns uint8 (convertible?)
+    assert addr == g || addr == f, "Check subtype compatibility";
+}
+
+// TEST 9: Tuple order (uint, bool) -> dispatches to H
+rule tupleOrderUintBool(env e) {
+    address addr;
+    uint x;
+    bool y;
+    x, y = addr.getPair(e);
+    assert addr == h, "(uint, bool) order should dispatch to H";
+    assert x == 1 && y == true;
+}
+
+// TEST 10: Tuple order (bool, uint) -> dispatches to I
+rule tupleOrderBoolUint(env e) {
+    address addr;
+    bool x;
+    uint y;
+    x, y = addr.getPair(e);
+    assert addr == i, "(bool, uint) order should dispatch to I";
+    assert x == true && y == 2;
+}
+
+// TEST 11: Triple return value
+rule tripleReturnValues(env e) {
+    address addr;
+    uint x;
+    uint y;
+    uint z;
+    x, y, z = addr.getTriple(e);
+    assert addr == j, "Triple return should dispatch to J";
+    assert x == 1 && y == 2 && z == 3;
+}
+
+// TEST 12: Wildcard with one variable - x, _ = addr.multi(e)
+rule wildcardWithOneVar(env e) {
+    address addr;
+    uint x;
+    x, _ = addr.multi(e);
+    assert addr == c, "One var + wildcard should dispatch to C (uint, uint)";
+    assert x == 42;
+}
+
+// TEST 13: Double wildcard - _, _ = addr.multi(e)
+rule doubleWildcard(env e) {
+    address addr;
+    _, _ = addr.multi(e);
+    assert addr == c, "Double wildcard with 2 positions should dispatch to C";
+}

Public/TestEVM/AddressFunctionCallsAmbig/Default.conf

@@ -0,0 +1,18 @@
+{
+    "files": [
+        "Contracts.sol:Main",
+        "Contracts.sol:A",
+        "Contracts.sol:B",
+        "Contracts.sol:C",
+        "Contracts.sol:D",
+        "Contracts.sol:E",
+        "Contracts.sol:F",
+        "Contracts.sol:G",
+        "Contracts.sol:H",
+        "Contracts.sol:I",
+        "Contracts.sol:J"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc8.25",
+    "verify": "Main:Contracts.spec"
+}

Public/TestEVM/AddressFunctionCallsAmbig/expectedDefault.json

@@ -0,0 +1,17 @@
+{
+	"rules": {
+		"assignmentToPreDeclaredBoolVar": "SUCCESS",
+		"assignmentToPreDeclaredUintVar": "SUCCESS",
+		"commandFormWorksWithVoid": "SUCCESS",
+		"doubleWildcard": "SUCCESS",
+		"explicitBoolTypeDispatchesToA": "SUCCESS",
+		"multiReturnTwoVarsDispatchesToC": "SUCCESS",
+		"multipleMatchingContractsBool": "SUCCESS",
+		"singleReturnDispatchesToD": "SUCCESS",
+		"subtypeUint8ToUint256": "SUCCESS",
+		"tripleReturnValues": "SUCCESS",
+		"tupleOrderBoolUint": "SUCCESS",
+		"tupleOrderUintBool": "SUCCESS",
+		"wildcardWithOneVar": "SUCCESS"
+	}
+}

Public/TestEVM/DuplicateContractNames/A.sol

@@ -0,0 +1,3 @@
+import {B} from "B.sol";
+
+contract A is B {}

Public/TestEVM/DuplicateContractNames/AnotherA.sol

@@ -0,0 +1,3 @@
+contract A {
+    function foo() internal returns (uint) { return 0; }
+}

Public/TestEVM/DuplicateContractNames/B.sol

@@ -0,0 +1,3 @@
+import {A} from "AnotherA.sol";
+
+contract B is A {}

Public/TestEVM/DuplicateContractNames/Default.conf

@@ -0,0 +1,4 @@
+{
+    "files": ["A.sol"],
+    "verify": "A:test.spec"
+}

Public/TestEVM/DuplicateContractNames/expectedDefault.json

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