*: port last dirty lemma, and delete file

dapp-org · May 5, 2020 · d2a43d4 · d2a43d4
1 parent 3ebae74
commit d2a43d4
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 9 deletions.
diff --git a/config.json b/config.json
@@ -8,9 +8,6 @@
     "rules": [
       "./src/storage.k.md",
       "./src/lemmas.k.md"
-    ],
-    "dirty_rules": [
-      "./src/dirty_lemmas.k.md"
     ]
   },
   "implementations": {

diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md
diff --git a/src/lemmas.k.md b/src/lemmas.k.md
@@ -347,6 +347,20 @@ rule (B |Int (notMaxUInt160 &Int A)) => B
   andBool (#rangeAddress(A) orBool #rangeUInt(256, A))
 ```
 
+## Z3 non-determinism
+
+Sometimes, the result of a Z3 query is non-deterministic. In the case below, Z3
+is sometimes able to deduce that `chop(X) => X`, but other times it isn't.
+
+This lemma ensures that we always drop the `chop`, when the constraints are satisfied.
+
+```k
+rule chop(((pow112 *Int A) /Int B) *Int X) => ((pow112 *Int A) /Int B) *Int X
+        requires A <Int pow112
+        andBool B >Int 0
+        andBool X <Int pow32
+```
+
 ## Packed Words In Memory
 
 Sometimes solidity will try and read a Word from memory containing unaligned data. In that case `K`