drnim: tiny progress (#13882)

* drnim: tiny progress
* refactoring complete
* drnim: prove .ensures annotations
* Moved code around to avoid code duplication
* drnim: first implementation of the 'old' property
* drnim: be precise about the assignment statement
* first implementation of --assumeUnique
* progress on forall/exists handling

3 files changed, 61 insertions, 6 deletions

diff --git a/drnim/tests/tbasic_array_index.nim b/drnim/tests/tbasic_array_index.nim
index 3f24ed3bd..8ae019e78 100644
--- a/drnim/tests/tbasic_array_index.nim
+++ b/drnim/tests/tbasic_array_index.nim
@@ -38,6 +38,14 @@ proc xu(a: uint) =
     let chunk = range[1u32..10u32](a)
     ru chunk
 
+proc parse(s: string) =
+  var i = 0
+
+  while i < s.len and s[i] != 'a':
+    inc i
+
+parse("abc")
+
 {.pop.}
 
 p([1, 2, 3], [4, 5])
diff --git a/drnim/tests/tensures.nim b/drnim/tests/tensures.nim
index 1283b493b..f4e8f84e6 100644
--- a/drnim/tests/tensures.nim
+++ b/drnim/tests/tensures.nim
@@ -1,12 +1,19 @@
 discard """
-  nimout: '''tensures.nim(11, 10) Warning: BEGIN [User]
-tensures.nim(20, 5) Warning: cannot prove:
+  nimout: '''tensures.nim(18, 10) Warning: BEGIN [User]
+tensures.nim(27, 5) Warning: cannot prove:
 0 < n [IndexCheck]
-tensures.nim(30, 10) Warning: END [User]'''
+tensures.nim(47, 17) Warning: cannot prove: a < 4; counter example: y -> 2
+a`2 -> 4
+a`1 -> 3
+a -> 2 [IndexCheck]
+tensures.nim(69, 17) Warning: cannot prove: a < 4; counter example: y -> 2
+a`1 -> 4
+a -> 2 [IndexCheck]
+tensures.nim(73, 10) Warning: END [User]'''
   cmd: "drnim $file"
   action: "compile"
 """
-
+import std/logic
 {.push staticBoundChecks: defined(nimDrNim).}
 {.warning: "BEGIN".}
 
@@ -27,5 +34,41 @@ proc main =
 
 main()
 
+proc myinc(x: var int) {.ensures: x == old(x)+1.} =
+  inc x
+  {.assume: old(x)+1 == x.}
+
+proc mainB(y: int) =
+  var a = y
+  if a < 3:
+    myinc a
+    {.assert: a < 4.}
+    myinc a
+    {.assert: a < 4.} # now this is wrong!
+
+mainB(3)
+
+proc a(yy, z: int) {.requires: (yy - z) > 6.} = discard
+# 'requires' must be weaker (or equal)
+# 'ensures'  must be stronger (or equal)
+
+# a 'is weaker than' b iff  b -> a
+# a 'is stronger than' b iff a -> b
+# --> We can use Z3 to compute whether 'var x: T = q' is valid
+
+type
+  F = proc (yy, z3: int) {.requires: z3 < 5 and z3 > -5 and yy > 10.}
+
+var
+  x: F = a # valid?
+
+proc testAsgn(y: int) =
+  var a = y
+  if a < 3:
+    a = a + 2
+    {.assert: a < 4.}
+
+testAsgn(3)
+
 {.warning: "END".}
 {.pop.}
diff --git a/drnim/tests/tsetlen_invalidates.nim b/drnim/tests/tsetlen_invalidates.nim
index 03620af10..f3e595744 100644
--- a/drnim/tests/tsetlen_invalidates.nim
+++ b/drnim/tests/tsetlen_invalidates.nim
@@ -1,12 +1,15 @@
 discard """
-  nimout: '''
-tsetlen_invalidates.nim(15, 12) Warning: cannot prove: 0 <= len(a) + -1; counter example: a.len -> 0 [IndexCheck]
+  nimout: '''tsetlen_invalidates.nim(12, 10) Warning: BEGIN [User]
+tsetlen_invalidates.nim(18, 12) Warning: cannot prove: 0 <= len(a) + -1; counter example: a`1.len -> 0
+a.len -> 1 [IndexCheck]
+tsetlen_invalidates.nim(26, 10) Warning: END [User]
 '''
   cmd: "drnim $file"
   action: "compile"
 """
 
 {.push staticBoundChecks: defined(nimDrNim).}
+{.warning: "BEGIN".}
 
 proc p() =
   var a = newSeq[int](3)
@@ -20,3 +23,4 @@ proc p() =
 {.pop.}
 
 p()
+{.warning: "END".}