Fix for #257; Add small ERC1155 macro (#258)

* Fix for #257; Add small ERC1155 macro * Fix failing tests
Consensys · Feb 1, 2024 · 9a20334 · 9a20334
1 parent 3d449a7
commit 9a20334
Show file tree

Hide file tree

Showing 92 changed files with 3,408 additions and 3,382 deletions.
diff --git a/src/instrumenter/interpose.ts b/src/instrumenter/interpose.ts
@@ -222,7 +222,7 @@ export function interpose(
 
     fun.documentation = undefined;
     stub.documentation = undefined;
-    fun.visibility = FunctionVisibility.Private;
+    fun.visibility = FunctionVisibility.Internal;
     fun.isConstructor = false;
     renameReturns(stub);
 

diff --git a/stdlib/erc1155.scribble.yaml b/stdlib/erc1155.scribble.yaml
@@ -0,0 +1,26 @@
+erc1155:
+    variables:
+    properties:
+        safeTransferFrom(from, to, tokenId, value, data):
+            - msg: "Cannot transfer to 0 address"
+              prop: "#if_succeeds to != address(0);"
+            - msg: "sender must have sufficient balance"
+              prop: "#if_succeeds old(balanceOf(from, tokenId)) >= value;"
+            - msg: "Sender must be properly authorized to transfer"
+              prop: "#if_succeeds msg.sender == from || old(isApprovedForAll(from, msg.sender));"
+            - msg: "Sender lost value tokens"
+              prop: "#if_succeeds balanceOf(from, tokenId) == old(balanceOf(from, tokenId)) - value;"
+            - msg: "Recipient gained value tokens (assuming non-deflationary tokens)"
+              prop: "#if_succeeds balanceOf(to, tokenId) == old(balanceOf(to, tokenId)) + value;"
+        safeBatchTransferFrom(from, to, ids, values, data):
+            - msg: "Cannot transfer to 0 address"
+              prop: "#if_succeeds to != address(0);"
+            - msg: "Ids and values must have equal length"
+              prop: "#if_succeeds values.length == ids.length;"
+            - msg: "sender must have sufficient balance"
+              prop: "#if_succeeds old(forall(uint i in ids) balanceOf(from, ids[i]) >= values[i]);"
+            - msg: "Sender must be properly authorized to transfer"
+              prop: "#if_succeeds msg.sender == from || old(isApprovedForAll(from, msg.sender));"
+        setApprovalForAll(operator, approved):
+            - msg: "setApprovalForAll worked correctly"
+              prop: "#if_succeeds approved == isApprovedForAll(msg.sender, operator);"
diff --git a/test/integration/scribble/run/filtering.spec.ts b/test/integration/scribble/run/filtering.spec.ts
@@ -27,7 +27,7 @@ contract Foo {
         }
     }
 
-    function _original_Foo_foo(uint256 a) private returns (uint256 b) {
+    function _original_Foo_foo(uint256 a) internal returns (uint256 b) {
         return a + 1;
     }
 }
@@ -87,14 +87,14 @@ contract Foo {
         __ScribbleUtilsLib__29.setInContract(!_v.__scribble_check_invs_at_end);
     }
 
-    function _original_Foo_foo(uint256 a) private returns (uint256 b) {
+    function _original_Foo_foo(uint256 a) internal returns (uint256 b) {
         return a + 1;
     }
 
     /// Check only the current contract's state invariants
     function __scribble_Foo_check_state_invariants_internal() internal {
         if (!(x == 0)) {
-            emit __ScribbleUtilsLib__29.AssertionFailed("001274:0075:000 1: Medium.P1");
+            emit __ScribbleUtilsLib__29.AssertionFailed("001275:0075:000 1: Medium.P1");
             assert(false);
         }
     }
@@ -137,14 +137,14 @@ contract Foo {
         __ScribbleUtilsLib__29.setInContract(!_v.__scribble_check_invs_at_end);
     }
 
-    function _original_Foo_foo(uint256 a) private returns (uint256 b) {
+    function _original_Foo_foo(uint256 a) internal returns (uint256 b) {
         return a + 1;
     }
 
     /// Check only the current contract's state invariants
     function __scribble_Foo_check_state_invariants_internal() internal {
         if (!(x < 0)) {
-            emit __ScribbleUtilsLib__29.AssertionFailed("001432:0077:000 2: Critical.P2");
+            emit __ScribbleUtilsLib__29.AssertionFailed("001433:0077:000 2: Critical.P2");
             assert(false);
         }
     }

diff --git a/test/multifile_samples/arr_sum/flat.sol.expected b/test/multifile_samples/arr_sum/flat.sol.expected
@@ -16,87 +16,87 @@ contract Foo {
         }
     }
 
-    function _original_Foo_pushA(uint k) private {
+    function _original_Foo_pushA(uint k) internal {
         a.push(k);
     }
 
     function setA(uint k, uint v) public {
         _original_Foo_setA(k, v);
         unchecked {
             if (!((__ScribbleUtilsLib__91.sum_arr_uint256_arr_storage(a) > 10) && (__ScribbleUtilsLib__91.sum_arr_uint256_arr_storage(a) < 20))) {
-                emit __ScribbleUtilsLib__91.AssertionFailed("000933:0066:000 1: ");
+                emit __ScribbleUtilsLib__91.AssertionFailed("000934:0066:000 1: ");
                 assert(false);
             }
         }
     }
 
-    function _original_Foo_setA(uint k, uint v) private {
+    function _original_Foo_setA(uint k, uint v) internal {
         a[k] = v;
     }
 
     function pushB(int8 k) public {
         _original_Foo_pushB(k);
         unchecked {
             if (!((__ScribbleUtilsLib__91.sum_arr_int8_arr_storage(b) > (-10)) && (__ScribbleUtilsLib__91.sum_arr_int8_arr_storage(b) < 10))) {
-                emit __ScribbleUtilsLib__91.AssertionFailed("001394:0066:000 2: ");
+                emit __ScribbleUtilsLib__91.AssertionFailed("001396:0066:000 2: ");
                 assert(false);
             }
         }
     }
 
-    function _original_Foo_pushB(int8 k) private {
+    function _original_Foo_pushB(int8 k) internal {
         b.push(k);
     }
 
     function setB(uint k, int8 v) public {
         _original_Foo_setB(k, v);
         unchecked {
             if (!((__ScribbleUtilsLib__91.sum_arr_int8_arr_storage(b) > (-10)) && (__ScribbleUtilsLib__91.sum_arr_int8_arr_storage(b) < 10))) {
-                emit __ScribbleUtilsLib__91.AssertionFailed("001858:0066:000 3: ");
+                emit __ScribbleUtilsLib__91.AssertionFailed("001861:0066:000 3: ");
                 assert(false);
             }
         }
     }
 
-    function _original_Foo_setB(uint k, int8 v) private {
+    function _original_Foo_setB(uint k, int8 v) internal {
         b[k] = v;
     }
 
     function memArr(int16[] memory c) public {
         _original_Foo_memArr(c);
         unchecked {
             if (!((__ScribbleUtilsLib__91.sum_arr_int16_arr_memory(c) > (-10)) && (__ScribbleUtilsLib__91.sum_arr_int16_arr_memory(c) < 10))) {
-                emit __ScribbleUtilsLib__91.AssertionFailed("002331:0066:000 4: ");
+                emit __ScribbleUtilsLib__91.AssertionFailed("002335:0066:000 4: ");
                 assert(false);
             }
         }
     }
 
-    function _original_Foo_memArr(int16[] memory c) private {}
+    function _original_Foo_memArr(int16[] memory c) internal {}
 
     function calldataArr(int16[] calldata c) external {
         _original_Foo_calldataArr(c);
         unchecked {
             if (!((__ScribbleUtilsLib__91.sum_arr_int16_arr_calldata(c) > (-10)) && (__ScribbleUtilsLib__91.sum_arr_int16_arr_calldata(c) < 10))) {
-                emit __ScribbleUtilsLib__91.AssertionFailed("002803:0066:000 5: ");
+                emit __ScribbleUtilsLib__91.AssertionFailed("002808:0066:000 5: ");
                 assert(false);
             }
         }
     }
 
-    function _original_Foo_calldataArr(int16[] calldata c) private {}
+    function _original_Foo_calldataArr(int16[] calldata c) internal {}
 
     function overflowCheck(uint[] calldata c) external {
         _original_Foo_overflowCheck(c);
         unchecked {
             if (!(__ScribbleUtilsLib__91.sum_arr_uint256_arr_calldata(c) < 10)) {
-                emit __ScribbleUtilsLib__91.AssertionFailed("003219:0066:000 6: ");
+                emit __ScribbleUtilsLib__91.AssertionFailed("003225:0066:000 6: ");
                 assert(false);
             }
         }
     }
 
-    function _original_Foo_overflowCheck(uint[] calldata c) private {}
+    function _original_Foo_overflowCheck(uint[] calldata c) internal {}
 }
 
 library __ScribbleUtilsLib__91 {