Merge pull request #447 from Certora/yoav/safecasting-builtin

docs for safeCasting and uncheckedOverflow builtin rules

Author: yoav-rodeh

docs/cvl/builtin.md

@@ -26,6 +26,8 @@ built_in_rule_name ::=
     | "sanity"
     | "deepSanity"
     | "viewReentrancy"
+    | "safeCasting"
+    | "uncheckedOverflow"
 ```
 
 (built-in-msg-value-in-loop)=
@@ -210,3 +212,39 @@ This ensures that the external call cannot observe `currentContract` in any stat
 called from `currentContract`. 
 
 
+(built-in-safe-casting)=
+Safe Casting — `safeCasting`
+--------------------------------------------------
+
+The `safeCasting` built-in rule is there to catch cases where an explicit cast in solidity is actually out of bounds. 
+For example, if an `uint` is cast to a `uint64`, the rule will fail if there is some external function in the contract, that can be called
+in such a way, that the value being cast is larger than `2^64 - 1`. Casting between signed and unsigned values are also checked. So if an `uint` is cast to an `int`, and the cast value is larger than `2^255 - 1`, the rule will fail.
+
+This rule can be enabled by including
+```cvl
+use builtin rule safeCasting;
+```
+in a spec file. In addition, the line `"safe_casting_builtin" : true` must be added to the conf file.
+
+
+(built-in-unchecked-overflow)=
+Unchecked Overflow — `uncheckedOverflow`
+--------------------------------------------------
+
+The `uncheckedOverflow` built-in looks for cases where any of the operations `+, -, *` appearing within an `unchecked` solidity block can actually overflow.
+
+For example:
+```
+function basicMul(uint128 x, uint128 y) public pure returns (uint)  {
+    unchecked {
+        return x * y;
+    }
+}
+```
+This will fail the builtin rule, because the multiplication is a `uint128` multiplication (even if it's later considered as a `uint`).
+
+This rule can be enabled by including
+```cvl
+use builtin rule uncheckedOverflow;
+```
+In addition, the line `"unchecked_overflow_builtin" : true` must be added to the conf file.