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
2025-12-28 08:54:53 +00:00 · 2020-04-15 20:03:25 +02:00
parent 04b6e9cf3e
commit 3a2697dd73
17 changed files with 755 additions and 259 deletions
--- a/compiler/ast.nim
+++ b/compiler/ast.nim
@@ -218,7 +218,7 @@ type
    nkEnumFieldDef,       # `ident = expr` in an enumeration
    nkArgList,            # argument list
    nkPattern,            # a special pattern; used for matching
-    nkHiddenTryStmt,      # token used for interpretation
+    nkHiddenTryStmt,      # a hidden try statement
    nkClosure,            # (prc, env)-pair (internally used for code gen)
    nkGotoState,          # used for the state machine (for iterators)
    nkState,              # give a label to a code section (for iterators)
--- a/compiler/cmdlinehelper.nim
+++ b/compiler/cmdlinehelper.nim
@@ -11,10 +11,24 @@

 import
  options, idents, nimconf, extccomp, commands, msgs,
-  lineinfos, modulegraphs, condsyms, os, pathutils
+  lineinfos, modulegraphs, condsyms, os, pathutils, parseopt

 from strutils import normalize

+proc prependCurDir*(f: AbsoluteFile): AbsoluteFile =
+  when defined(unix):
+    if os.isAbsolute(f.string): result = f
+    else: result = AbsoluteFile("./" & f.string)
+  else:
+    result = f
+
+proc addCmdPrefix*(result: var string, kind: CmdLineKind) =
+  # consider moving this to std/parseopt
+  case kind
+  of cmdLongOption: result.add "--"
+  of cmdShortOption: result.add "-"
+  of cmdArgument, cmdEnd: discard
+
 type
  NimProg* = ref object
    suggestMode*: bool
--- a/compiler/guards.nim
+++ b/compiler/guards.nim
@@ -84,8 +84,8 @@ proc interestingCaseExpr*(m: PNode): bool = isLetLocation(m, true)

 type
  Operators* = object
-    opNot, opContains, opLe, opLt, opAnd, opOr, opIsNil, opEq: PSym
-    opAdd, opSub, opMul, opDiv, opLen: PSym
+    opNot*, opContains*, opLe*, opLt*, opAnd*, opOr*, opIsNil*, opEq*: PSym
+    opAdd*, opSub*, opMul*, opDiv*, opLen*: PSym

 proc initOperators*(g: ModuleGraph): Operators =
  result.opLe = createMagic(g, "<=", mLeI)
@@ -156,12 +156,12 @@ proc neg(n: PNode; o: Operators): PNode =
    result[0] = newSymNode(o.opNot)
    result[1] = n

-proc buildCall(op: PSym; a: PNode): PNode =
+proc buildCall*(op: PSym; a: PNode): PNode =
  result = newNodeI(nkCall, a.info, 2)
  result[0] = newSymNode(op)
  result[1] = a

-proc buildCall(op: PSym; a, b: PNode): PNode =
+proc buildCall*(op: PSym; a, b: PNode): PNode =
  result = newNodeI(nkInfix, a.info, 3)
  result[0] = newSymNode(op)
  result[1] = a
@@ -464,7 +464,7 @@ proc hasSubTree(n, x: PNode): bool =
    for i in 0..n.safeLen-1:
      if hasSubTree(n[i], x): return true

-proc invalidateFacts*(m: var TModel, n: PNode) =
+proc invalidateFacts*(s: var seq[PNode], n: PNode) =
  # We are able to guard local vars (as opposed to 'let' variables)!
  # 'while p != nil: f(p); p = p.next'
  # This is actually quite easy to do:
@@ -482,8 +482,11 @@ proc invalidateFacts*(m: var TModel, n: PNode) =
  # The same mechanism could be used for more complex data stored on the heap;
  # procs that 'write: []' cannot invalidate 'n.kind' for instance. In fact, we
  # could CSE these expressions then and help C's optimizer.
-  for i in 0..high(m.s):
-    if m.s[i] != nil and m.s[i].hasSubTree(n): m.s[i] = nil
+  for i in 0..high(s):
+    if s[i] != nil and s[i].hasSubTree(n): s[i] = nil
+
+proc invalidateFacts*(m: var TModel, n: PNode) =
+  invalidateFacts(m.s, n)

 proc valuesUnequal(a, b: PNode): bool =
  if a.isValue and b.isValue:
--- a/compiler/modulegraphs.nim
+++ b/compiler/modulegraphs.nim
@@ -72,9 +72,7 @@ type
    onDefinitionResolveForward*: proc (graph: ModuleGraph; s: PSym; info: TLineInfo) {.nimcall.}
    onUsage*: proc (graph: ModuleGraph; s: PSym; info: TLineInfo) {.nimcall.}
    globalDestructors*: seq[PNode]
-    proofEngine*: proc (graph: ModuleGraph; assumptions: seq[PNode]; toProve: PNode): (bool, string) {.nimcall.}
-    requirementsCheck*: proc (graph: ModuleGraph; assumptions: seq[PNode];
-                             call, requirement: PNode): (bool, string) {.nimcall.}
+    strongSemCheck*: proc (graph: ModuleGraph; owner: PSym; body: PNode) {.nimcall.}
    compatibleProps*: proc (graph: ModuleGraph; formal, actual: PType): bool {.nimcall.}

  TPassContext* = object of RootObj # the pass's context
--- a/compiler/nim.nim
+++ b/compiler/nim.nim
@@ -33,20 +33,6 @@ when defined(profiler) or defined(memProfiler):
  {.hint: "Profiling support is turned on!".}
  import nimprof

-proc prependCurDir(f: AbsoluteFile): AbsoluteFile =
-  when defined(unix):
-    if os.isAbsolute(f.string): result = f
-    else: result = AbsoluteFile("./" & f.string)
-  else:
-    result = f
-
-proc addCmdPrefix*(result: var string, kind: CmdLineKind) =
-  # consider moving this to std/parseopt
-  case kind
-  of cmdLongOption: result.add "--"
-  of cmdShortOption: result.add "-"
-  of cmdArgument, cmdEnd: discard
-
 proc processCmdLine(pass: TCmdLinePass, cmd: string; config: ConfigRef) =
  var p = parseopt.initOptParser(cmd)
  var argsCount = 0
--- a/compiler/pragmas.nim
+++ b/compiler/pragmas.nim
@@ -53,7 +53,7 @@ const
    wDeprecated,
    wFloatChecks, wInfChecks, wNanChecks, wPragma, wEmit, wUnroll,
    wLinearScanEnd, wPatterns, wTrMacros, wEffects, wNoForward, wReorder, wComputedGoto,
-    wInjectStmt, wExperimental, wThis, wUsed, wInvariant, wAssume}
+    wInjectStmt, wExperimental, wThis, wUsed, wInvariant, wAssume, wAssert}
  lambdaPragmas* = declPragmas + {FirstCallConv..LastCallConv,
    wNoSideEffect, wSideEffect, wNoreturn, wNosinks, wDynlib, wHeader,
    wThread, wAsmNoStackFrame,
--- a/compiler/semmagic.nim
+++ b/compiler/semmagic.nim
@@ -429,15 +429,29 @@ proc turnFinalizerIntoDestructor(c: PContext; orig: PSym; info: TLineInfo): PSym
  result.typ.addParam newParam

 proc semQuantifier(c: PContext; n: PNode): PNode =
-  checkMinSonsLen(n, 2, c.config)
+  checkSonsLen(n, 2, c.config)
  openScope(c)
-  for i in 0..n.len-2:
-    let v = newSymS(skForVar, n[i], c)
-    styleCheckDef(c.config, v)
-    onDef(n.info, v)
-    n[i] = newSymNode(v)
-    addDecl(c, v)
-  n[^1] = forceBool(c, semExprWithType(c, n[^1]))
+  result = newNodeIT(n.kind, n.info, n.typ)
+  result.add n[0]
+  let args = n[1]
+  assert args.kind == nkArgList
+  for i in 0..args.len-2:
+    let it = args[i]
+    var valid = false
+    if it.kind == nkInfix:
+      let op = considerQuotedIdent(c, it[0])
+      if op.id == ord(wIn):
+        let v = newSymS(skForVar, it[1], c)
+        styleCheckDef(c.config, v)
+        onDef(it[1].info, v)
+        let domain = semExprWithType(c, it[2], {efWantIterator})
+        v.typ = domain.typ
+        valid = true
+        addDecl(c, v)
+        result.add newTree(nkInfix, it[0], newSymNode(v), domain)
+    if not valid:
+      localError(c.config, n.info, "<quantifier> 'in' <range> expected")
+  result.add forceBool(c, semExprWithType(c, args[^1]))
  closeScope(c)

 proc semOld(c: PContext; n: PNode): PNode =
--- a/compiler/semparallel.nim
+++ b/compiler/semparallel.nim
@@ -25,7 +25,7 @@ import
  ast, astalgo, idents, lowerings, magicsys, guards, sempass2, msgs,
  renderer, types, modulegraphs, options, spawn, lineinfos

-from trees import getMagic
+from trees import getMagic, isTrue, getRoot
 from strutils import `%`

 discard """
--- a/compiler/sempass2.nim
+++ b/compiler/sempass2.nim
@@ -433,7 +433,8 @@ proc isForwardedProc(n: PNode): bool =
 proc trackPragmaStmt(tracked: PEffects, n: PNode) =
  for i in 0..<n.len:
    var it = n[i]
-    if whichPragma(it) == wEffects:
+    let pragma = whichPragma(it)
+    if pragma == wEffects:
      # list the computed effects up to here:
      listEffects(tracked)

@@ -664,10 +665,6 @@ proc trackBlock(tracked: PEffects, n: PNode) =
  else:
    track(tracked, n)

-proc isTrue*(n: PNode): bool =
-  n.kind == nkSym and n.sym.kind == skEnumField and n.sym.position != 0 or
-    n.kind == nkIntLit and n.intVal != 0
-
 proc paramType(op: PType, i: int): PType =
  if op != nil and i < op.len: result = op[i]

@@ -676,14 +673,6 @@ proc cstringCheck(tracked: PEffects; n: PNode) =
      a.typ.kind == tyString and a.kind notin {nkStrLit..nkTripleStrLit}):
    message(tracked.config, n.info, warnUnsafeCode, renderTree(n))

-proc prove(c: PEffects; prop: PNode): bool =
-  if c.graph.proofEngine != nil:
-    let (success, m) = c.graph.proofEngine(c.graph, c.guards.s,
-      canon(prop, c.guards.o))
-    if not success:
-      message(c.config, prop.info, warnStaticIndexCheck, "cannot prove: " & $prop & m)
-    result = success
-
 proc patchResult(c: PEffects; n: PNode) =
  if n.kind == nkSym and n.sym.kind == skResult:
    let fn = c.owner
@@ -695,45 +684,18 @@ proc patchResult(c: PEffects; n: PNode) =
    for i in 0..<safeLen(n):
      patchResult(c, n[i])

-when defined(drnim):
-  proc requiresCheck(c: PEffects; call: PNode; op: PType) =
-    assert op.n[0].kind == nkEffectList
-    if requiresEffects < op.n[0].len:
-      let requires = op.n[0][requiresEffects]
-      if requires != nil and requires.kind != nkEmpty:
-        # we need to map the call arguments to the formal parameters used inside
-        # 'requires':
-        let (success, m) = c.graph.requirementsCheck(c.graph, c.guards.s, call, canon(requires, c.guards.o))
-        if not success:
-          message(c.config, call.info, warnStaticIndexCheck, "cannot prove: " & $requires & m)
-
-else:
-  template requiresCheck(c, n, op) = discard
-
 proc checkLe(c: PEffects; a, b: PNode) =
-  if c.graph.proofEngine != nil:
-    var cmpOp = mLeI
-    if a.typ != nil:
-      case a.typ.skipTypes(abstractInst).kind
-      of tyFloat..tyFloat128: cmpOp = mLeF64
-      of tyChar, tyUInt..tyUInt64: cmpOp = mLeU
-      else: discard
-
-    let cmp = newTree(nkInfix, newSymNode createMagic(c.graph, "<=", cmpOp), a, b)
-    cmp.info = a.info
-    discard prove(c, cmp)
-  else:
-    case proveLe(c.guards, a, b)
-    of impUnknown:
-      #for g in c.guards.s:
-      #  if g != nil: echo "I Know ", g
-      message(c.config, a.info, warnStaticIndexCheck,
-        "cannot prove: " & $a & " <= " & $b)
-    of impYes:
-      discard
-    of impNo:
-      message(c.config, a.info, warnStaticIndexCheck,
-        "can prove: " & $a & " > " & $b)
+  case proveLe(c.guards, a, b)
+  of impUnknown:
+    #for g in c.guards.s:
+    #  if g != nil: echo "I Know ", g
+    message(c.config, a.info, warnStaticIndexCheck,
+      "cannot prove: " & $a & " <= " & $b)
+  of impYes:
+    discard
+  of impNo:
+    message(c.config, a.info, warnStaticIndexCheck,
+      "can prove: " & $a & " > " & $b)

 proc checkBounds(c: PEffects; arr, idx: PNode) =
  checkLe(c, lowBound(c.config, arr), idx)
@@ -831,7 +793,6 @@ proc track(tracked: PEffects, n: PNode) =
        mergeEffects(tracked, effectList[exceptionEffects], n)
        mergeTags(tracked, effectList[tagEffects], n)
        gcsafeAndSideeffectCheck()
-      requiresCheck(tracked, n, op)
    if a.kind != nkSym or a.sym.magic != mNBindSym:
      for i in 1..<n.len: trackOperand(tracked, n[i], paramType(op, i), a)
    if a.kind == nkSym and a.sym.magic in {mNew, mNewFinalize, mNewSeq}:
@@ -929,7 +890,6 @@ proc track(tracked: PEffects, n: PNode) =
  of nkWhen, nkIfStmt, nkIfExpr: trackIf(tracked, n)
  of nkBlockStmt, nkBlockExpr: trackBlock(tracked, n[1])
  of nkWhileStmt:
-    track(tracked, n[0])
    # 'while true' loop?
    if isTrue(n[0]):
      trackBlock(tracked, n[1])
@@ -938,6 +898,7 @@ proc track(tracked: PEffects, n: PNode) =
      let oldState = tracked.init.len
      let oldFacts = tracked.guards.s.len
      addFact(tracked.guards, n[0])
+      track(tracked, n[0])
      track(tracked, n[1])
      setLen(tracked.init, oldState)
      setLen(tracked.guards.s, oldFacts)
@@ -1027,12 +988,6 @@ proc track(tracked: PEffects, n: PNode) =
        enforcedGcSafety = true
      elif pragma == wNoSideEffect:
        enforceNoSideEffects = true
-      when defined(drnim):
-        if pragma == wAssume:
-          addFact(tracked.guards, pragmaList[i][1])
-        elif pragma == wInvariant or pragma == wAssert:
-          if prove(tracked, pragmaList[i][1]):
-            addFact(tracked.guards, pragmaList[i][1])

    if enforcedGcSafety: tracked.inEnforcedGcSafe = true
    if enforceNoSideEffects: tracked.inEnforcedNoSideEffects = true
@@ -1181,7 +1136,10 @@ proc initEffects(g: ModuleGraph; effects: PNode; s: PSym; t: var TEffects; c: PC
  t.init = @[]
  t.guards.s = @[]
  t.guards.o = initOperators(g)
-  t.currOptions = g.config.options + s.options
+  when defined(drnim):
+    t.currOptions = g.config.options + s.options - {optStaticBoundsCheck}
+  else:
+    t.currOptions = g.config.options + s.options
  t.guards.beSmart = optStaticBoundsCheck in t.currOptions
  t.locked = @[]
  t.graph = g
@@ -1237,7 +1195,6 @@ proc trackProc*(c: PContext; s: PSym, body: PNode) =
  if not isNil(ensuresSpec):
    patchResult(t, ensuresSpec)
    effects[ensuresEffects] = ensuresSpec
-    discard prove(t, ensuresSpec)

  if sfThread in s.flags and t.gcUnsafe:
    if optThreads in g.config.globalOptions and optThreadAnalysis in g.config.globalOptions:
@@ -1262,6 +1219,8 @@ proc trackProc*(c: PContext; s: PSym, body: PNode) =
    message(g.config, s.info, warnLockLevel,
      "declared lock level is $1, but real lock level is $2" %
        [$s.typ.lockLevel, $t.maxLockLevel])
+  when defined(drnim):
+    if c.graph.strongSemCheck != nil: c.graph.strongSemCheck(c.graph, s, body)
  when defined(useDfa):
    if s.name.s == "testp":
      dataflowAnalysis(s, body)
@@ -1277,3 +1236,5 @@ proc trackStmt*(c: PContext; module: PSym; n: PNode, isTopLevel: bool) =
  initEffects(g, effects, module, t, c)
  t.isTopLevel = isTopLevel
  track(t, n)
+  when defined(drnim):
+    if c.graph.strongSemCheck != nil: c.graph.strongSemCheck(c.graph, module, n)
--- a/compiler/spawn.nim
+++ b/compiler/spawn.nim
@@ -11,7 +11,7 @@

 import ast, types, idents, magicsys, msgs, options, modulegraphs,
  lowerings
-from trees import getMagic
+from trees import getMagic, getRoot

 proc callProc(a: PNode): PNode =
  result = newNodeI(nkCall, a.info)
@@ -74,7 +74,7 @@ proc addLocalVar(g: ModuleGraph; varSection, varInit: PNode; owner: PSym; typ: P
        varInit.add call
      else:
        varInit.add newFastAsgnStmt(newSymNode(result), v)
-    else:      
+    else:
      if useShallowCopy and typeNeedsNoDeepCopy(typ) or optTinyRtti in g.config.globalOptions:
        varInit.add newFastAsgnStmt(newSymNode(result), v)
      else:
@@ -196,7 +196,7 @@ proc createCastExpr(argsParam: PSym; objType: PType): PNode =
  result.typ = newType(tyPtr, objType.owner)
  result.typ.rawAddSon(objType)

-proc setupArgsForConcurrency(g: ModuleGraph; n: PNode; objType: PType; 
+proc setupArgsForConcurrency(g: ModuleGraph; n: PNode; objType: PType;
                             owner: PSym; scratchObj: PSym,
                             castExpr, call,
                             varSection, varInit, result: PNode) =
@@ -221,23 +221,6 @@ proc setupArgsForConcurrency(g: ModuleGraph; n: PNode; objType: PType;
                           indirectAccess(castExpr, field, n.info))
    call.add(newSymNode(temp))

-proc getRoot*(n: PNode): PSym =
-  ## ``getRoot`` takes a *path* ``n``. A path is an lvalue expression
-  ## like ``obj.x[i].y``. The *root* of a path is the symbol that can be
-  ## determined as the owner; ``obj`` in the example.
-  case n.kind
-  of nkSym:
-    if n.sym.kind in {skVar, skResult, skTemp, skLet, skForVar}:
-      result = n.sym
-  of nkDotExpr, nkBracketExpr, nkHiddenDeref, nkDerefExpr,
-      nkObjUpConv, nkObjDownConv, nkCheckedFieldExpr:
-    result = getRoot(n[0])
-  of nkHiddenStdConv, nkHiddenSubConv, nkConv:
-    result = getRoot(n[1])
-  of nkCallKinds:
-    if getMagic(n) == mSlice: result = getRoot(n[1])
-  else: discard
-
 proc setupArgsForParallelism(g: ModuleGraph; n: PNode; objType: PType;
                             owner: PSym; scratchObj: PSym;
                             castExpr, call,
@@ -344,7 +327,7 @@ proc wrapProcForSpawn*(g: ModuleGraph; owner: PSym; spawnExpr: PNode; retType: P
    if {tfThread, tfNoSideEffect} * n[0].typ.flags == {}:
      localError(g.config, n.info, "'spawn' takes a GC safe call expression")

-  var fn = n[0] 
+  var fn = n[0]
  let
    name = (if fn.kind == nkSym: fn.sym.name.s else: genPrefix) & "Wrapper"
    wrapperProc = newSym(skProc, getIdent(g.cache, name), owner, fn.info, g.config.options)
--- a/compiler/trees.nim
+++ b/compiler/trees.nim
@@ -169,3 +169,24 @@ proc flattenStmts*(n: PNode): PNode =
 proc extractRange*(k: TNodeKind, n: PNode, a, b: int): PNode =
  result = newNodeI(k, n.info, b-a+1)
  for i in 0..b-a: result[i] = n[i+a]
+
+proc isTrue*(n: PNode): bool =
+  n.kind == nkSym and n.sym.kind == skEnumField and n.sym.position != 0 or
+    n.kind == nkIntLit and n.intVal != 0
+
+proc getRoot*(n: PNode): PSym =
+  ## ``getRoot`` takes a *path* ``n``. A path is an lvalue expression
+  ## like ``obj.x[i].y``. The *root* of a path is the symbol that can be
+  ## determined as the owner; ``obj`` in the example.
+  case n.kind
+  of nkSym:
+    if n.sym.kind in {skVar, skResult, skTemp, skLet, skForVar, skParam}:
+      result = n.sym
+  of nkDotExpr, nkBracketExpr, nkHiddenDeref, nkDerefExpr,
+      nkObjUpConv, nkObjDownConv, nkCheckedFieldExpr:
+    result = getRoot(n[0])
+  of nkHiddenStdConv, nkHiddenSubConv, nkConv:
+    result = getRoot(n[1])
+  of nkCallKinds:
+    if getMagic(n) == mSlice: result = getRoot(n[1])
+  else: discard
--- a/doc/contributing.rst
+++ b/doc/contributing.rst
@@ -265,7 +265,7 @@ the first is preferred.


 Best practices
-=============
+==============

 Note: these are general guidelines, not hard rules; there are always exceptions.
 Code reviews can just point to a specific section here to save time and
@@ -361,8 +361,10 @@ General commit rules

 1. Important, critical bugfixes that have a tiny chance of breaking
   somebody's code should be backported to the latest stable release
-   branch (currently 1.0.x). The commit message should contain ``[backport]``
-   then.
+   branch (currently 1.2.x) and maybe also to the 1.0 branch.
+   The commit message should contain the tag ``[backport]`` for "backport to all
+   stable releases" and the tag ``[backport:$VERSION]`` for backporting to the
+   given $VERSION.

 2. If you introduce changes which affect backwards compatibility,
   make breaking changes, or have PR which is tagged as ``[feature]``,
--- a/doc/drnim.rst
+++ b/doc/drnim.rst
@@ -120,8 +120,7 @@ you assume.
 Example: insertionSort
 ======================

-**Note**: This example does not yet work with DrNim. ``forall`` and ``exists``
-are not implemented.
+**Note**: This example does not yet work with DrNim.

 .. code-block:: nim

--- a/drnim/drnim.nim
+++ b/drnim/drnim.nim
@@ -9,53 +9,21 @@

 #[

- Most important bug:
-
-  while i < x.len and use(s[i]): inc i # is safe
-
+- the analysis has to take 'break', 'continue' and 'raises' into account
 - We need to map arrays to Z3 and test for something like 'forall(i, (i in 3..4) -> (a[i] > 3))'
- forall/exists need syntactic sugar as the manual
 - We need teach DrNim what 'inc', 'dec' and 'swap' mean, for example
  'x in n..m; inc x' implies 'x in n+1..m+1'

- We need an ``old`` annotation:
-
-proc f(x: var int; y: var int) {.ensures: x == old(x)+1 and y == old(y)+1 .} =
-  inc x
-  inc y
-
-var x = 3
-var y: range[N..M]
-f(x, y)
-{.assume: y in N+1 .. M+1.}
-# --> y in N+1..M+1
-
-proc myinc(x: var int) {.ensures: x-1 == old(x).} =
-  inc x
-
-facts(x) # x < 3
-myinc x
-facts(x+1)
-
-We handle state transitions in this way:
-
-  for every f in facts:
-    replace 'x' by 'old(x)'
-  facts.add ensuresClause
-
-  # then we know: old(x) < 3; x-1 == old(x)
-  # we can conclude:  x-1 < 3 but leave this task to Z3
-
 ]#

 import std / [
-  parseopt, strutils, os, tables, times
+  parseopt, strutils, os, tables, times, intsets, hashes
 ]

 import ".." / compiler / [
-  ast, types, renderer,
+  ast, astalgo, types, renderer,
  commands, options, msgs,
-  platform,
+  platform, trees, wordrecg, guards,
  idents, lineinfos, cmdlinehelper, modulegraphs, condsyms,
  pathutils, passes, passaux, sem, modules
 ]
@@ -91,42 +59,174 @@ proc helpOnError(conf: ConfigRef) =
 type
  CannotMapToZ3Error = object of ValueError
  Z3Exception = object of ValueError
+  VersionScope = distinct int
+  DrnimContext = ref object
+    z3: Z3_context
+    graph: ModuleGraph
+    facts: seq[(PNode, VersionScope)]
+    varVersions: seq[int] # this maps variable IDs to their current version.
+    o: Operators
+    hasUnstructedCf: int
+    currOptions: TOptions
+    owner: PSym
+    mangler: seq[PSym]

  DrCon = object
-    z3: Z3_context
    graph: ModuleGraph
    mapping: Table[string, Z3_ast]
    canonParameterNames: bool
+    assumeUniqueness: bool
+    up: DrnimContext

-proc stableName(result: var string; n: PNode) =
+var
+  assumeUniqueness: bool
+
+proc echoFacts(c: DrnimContext) =
+  echo "FACTS:"
+  for i in 0 ..< c.facts.len:
+    let f = c.facts[i]
+    echo f[0], " version ", int(f[1])
+
+proc isLoc(m: PNode; assumeUniqueness: bool): bool =
+  # We can reason about "locations" and map them to Z3 constants.
+  # For code that is full of "ref" (e.g. the Nim compiler itself) that
+  # is too limiting
+  proc isLet(n: PNode): bool =
+    if n.kind == nkSym:
+      if n.sym.kind in {skLet, skTemp, skForVar}:
+        result = true
+      elif n.sym.kind == skParam and skipTypes(n.sym.typ,
+                                               abstractInst).kind != tyVar:
+        result = true
+
+  var n = m
+  while true:
+    case n.kind
+    of nkDotExpr, nkCheckedFieldExpr, nkObjUpConv, nkObjDownConv, nkHiddenDeref:
+      n = n[0]
+    of nkDerefExpr:
+      n = n[0]
+      if not assumeUniqueness: return false
+    of nkBracketExpr:
+      if isConstExpr(n[1]) or isLet(n[1]) or isConstExpr(n[1].skipConv):
+        n = n[0]
+      else: return
+    of nkHiddenStdConv, nkHiddenSubConv, nkConv:
+      n = n[1]
+    else:
+      break
+  if n.kind == nkSym:
+    case n.sym.kind
+    of skLet, skTemp, skForVar, skParam:
+      result = true
+    #of skParam:
+    #  result = skipTypes(n.sym.typ, abstractInst).kind != tyVar
+    of skResult, skVar:
+      result = {sfAddrTaken} * n.sym.flags == {}
+    else:
+      discard
+
+proc varVersion(c: DrnimContext; s: PSym; begin: VersionScope): int =
+  result = 0
+  for i in countdown(int(begin)-1, 0):
+    if c.varVersions[i] == s.id: inc result
+
+proc disamb(c: DrnimContext; s: PSym): int =
+  # we group by 's.name.s' to compute the stable name ID.
+  result = 0
+  for i in 0 ..< c.mangler.len:
+    if s == c.mangler[i]: return result
+    if s.name.s == c.mangler[i].name.s: inc result
+  c.mangler.add s
+
+proc stableName(result: var string; c: DrnimContext; n: PNode; version: VersionScope;
+                isOld: bool) =
  # we can map full Nim expressions like 'f(a, b, c)' to Z3 variables.
-  # We must be carefult to select a unique, stable name for these expressions
+  # We must be careful to select a unique, stable name for these expressions
  # based on structural equality. 'stableName' helps us with this problem.
+  # In the future we will also use this string for the caching mechanism.
  case n.kind
  of nkEmpty, nkNilLit, nkType: discard
  of nkIdent:
    result.add n.ident.s
  of nkSym:
    result.add n.sym.name.s
-    result.add '_'
-    result.addInt n.sym.id
+    if n.sym.magic == mNone:
+      let d = disamb(c, n.sym)
+      if d != 0:
+        result.add "`scope="
+        result.addInt d
+      let v = c.varVersion(n.sym, version) - ord(isOld)
+      assert v >= 0
+      if v > 0:
+        result.add '`'
+        result.addInt v
+    else:
+      result.add "`magic="
+      result.addInt ord(n.sym.magic)
+
  of nkCharLit..nkUInt64Lit:
    result.addInt n.intVal
  of nkFloatLit..nkFloat64Lit:
    result.addFloat n.floatVal
  of nkStrLit..nkTripleStrLit:
    result.add strutils.escape n.strVal
+  of nkDotExpr:
+    stableName(result, c, n[0], version, isOld)
+    result.add '.'
+    stableName(result, c, n[1], version, isOld)
+  of nkBracketExpr:
+    stableName(result, c, n[0], version, isOld)
+    result.add '['
+    stableName(result, c, n[1], version, isOld)
+    result.add ']'
+  of nkCallKinds:
+    if n.len == 2:
+      stableName(result, c, n[1], version, isOld)
+      result.add '.'
+      case getMagic(n)
+      of mLengthArray, mLengthOpenArray, mLengthSeq, mLengthStr:
+        result.add "len"
+      of mHigh:
+        result.add "high"
+      of mLow:
+        result.add "low"
+      else:
+        stableName(result, c, n[0], version, isOld)
+    elif n.kind == nkInfix and n.len == 3:
+      result.add '('
+      stableName(result, c, n[1], version, isOld)
+      result.add ' '
+      stableName(result, c, n[0], version, isOld)
+      result.add ' '
+      stableName(result, c, n[2], version, isOld)
+      result.add ')'
+    else:
+      stableName(result, c, n[0], version, isOld)
+      result.add '('
+      for i in 1..<n.len:
+        if i > 1: result.add ", "
+        stableName(result, c, n[i], version, isOld)
+      result.add ')'
  else:
    result.add $n.kind
    result.add '('
    for i in 0..<n.len:
      if i > 0: result.add ", "
-      stableName(result, n[i])
+      stableName(result, c, n[i], version, isOld)
    result.add ')'

-proc stableName(n: PNode): string = stableName(result, n)
+proc stableName(c: DrnimContext; n: PNode; version: VersionScope;
+                isOld = false): string =
+  stableName(result, c, n, version, isOld)
+
+template allScopes(c): untyped = VersionScope(c.varVersions.len)
+template currentScope(c): untyped = VersionScope(c.varVersions.len)

 proc notImplemented(msg: string) {.noinline.} =
+  when defined(debug):
+    writeStackTrace()
+    echo msg
  raise newException(CannotMapToZ3Error, "; cannot map to Z3: " & msg)

 proc translateEnsures(e, x: PNode): PNode =
@@ -138,7 +238,7 @@ proc translateEnsures(e, x: PNode): PNode =
      result[i] = translateEnsures(e[i], x)

 proc typeToZ3(c: DrCon; t: PType): Z3_sort =
-  template ctx: untyped = c.z3
+  template ctx: untyped = c.up.z3
  case t.skipTypes(abstractInst+{tyVar}).kind
  of tyEnum, tyInt..tyInt64:
    result = Z3_mk_int_sort(ctx)
@@ -156,42 +256,64 @@ template binary(op, a, b): untyped =
  var arr = [a, b]
  op(ctx, cuint(2), addr(arr[0]))

-proc nodeToZ3(c: var DrCon; n: PNode; vars: var seq[PNode]): Z3_ast
+proc nodeToZ3(c: var DrCon; n: PNode; scope: VersionScope; vars: var seq[PNode]): Z3_ast
+
+proc nodeToDomain(c: var DrCon; n, q: PNode; opAnd: PSym): PNode =
+  assert n.kind == nkInfix
+  let opLe = createMagic(c.graph, "<=", mLeI)
+  case $n[0]
+  of "..":
+    result = buildCall(opAnd, buildCall(opLe, n[1], q), buildCall(opLe, q, n[2]))
+  of "..<":
+    let opLt = createMagic(c.graph, "<", mLtI)
+    result = buildCall(opAnd, buildCall(opLe, n[1], q), buildCall(opLt, q, n[2]))
+  else:
+    notImplemented($n)

 template quantorToZ3(fn) {.dirty.} =
-  template ctx: untyped = c.z3
+  template ctx: untyped = c.up.z3

-  var bound = newSeq[Z3_app](n.len-1)
-  for i in 0..n.len-2:
-    doAssert n[i].kind == nkSym
-    let v = n[i].sym
+  var bound = newSeq[Z3_app](n.len-2)
+  let opAnd = createMagic(c.graph, "and", mAnd)
+  var known: PNode
+  for i in 1..n.len-2:
+    let it = n[i]
+    doAssert it.kind == nkInfix
+    let v = it[1].sym
    let name = Z3_mk_string_symbol(ctx, v.name.s)
    let vz3 = Z3_mk_const(ctx, name, typeToZ3(c, v.typ))
-    c.mapping[stableName(n[i])] = vz3
-    bound[i] = Z3_to_app(ctx, vz3)
+    c.mapping[stableName(c.up, it[1], allScopes(c.up))] = vz3
+    bound[i-1] = Z3_to_app(ctx, vz3)
+    let domain = nodeToDomain(c, it[2], it[1], opAnd)
+    if known == nil:
+      known = domain
+    else:
+      known = buildCall(opAnd, known, domain)

  var dummy: seq[PNode]
-  let x = nodeToZ3(c, n[^1], dummy)
+  assert known != nil
+  let x = nodeToZ3(c, buildCall(createMagic(c.graph, "->", mImplies),
+                   known, n[^1]), scope, dummy)
  result = fn(ctx, 0, bound.len.cuint, addr(bound[0]), 0, nil, x)

-proc forallToZ3(c: var DrCon; n: PNode): Z3_ast = quantorToZ3(Z3_mk_forall_const)
-proc existsToZ3(c: var DrCon; n: PNode): Z3_ast = quantorToZ3(Z3_mk_exists_const)
+proc forallToZ3(c: var DrCon; n: PNode; scope: VersionScope): Z3_ast = quantorToZ3(Z3_mk_forall_const)
+proc existsToZ3(c: var DrCon; n: PNode; scope: VersionScope): Z3_ast = quantorToZ3(Z3_mk_exists_const)

-proc paramName(n: PNode): string =
+proc paramName(c: DrnimContext; n: PNode): string =
  case n.sym.kind
  of skParam: result = "arg" & $n.sym.position
  of skResult: result = "result"
-  else: result = stableName(n)
+  else: result = stableName(c, n, allScopes(c))

-proc nodeToZ3(c: var DrCon; n: PNode; vars: var seq[PNode]): Z3_ast =
-  template ctx: untyped = c.z3
-  template rec(n): untyped = nodeToZ3(c, n, vars)
+proc nodeToZ3(c: var DrCon; n: PNode; scope: VersionScope; vars: var seq[PNode]): Z3_ast =
+  template ctx: untyped = c.up.z3
+  template rec(n): untyped = nodeToZ3(c, n, scope, vars)
  case n.kind
  of nkSym:
-    let key = if c.canonParameterNames: paramName(n) else: stableName(n)
+    let key = if c.canonParameterNames: paramName(c.up, n) else: stableName(c.up, n, scope)
    result = c.mapping.getOrDefault(key)
    if pointer(result) == nil:
-      let name = Z3_mk_string_symbol(ctx, n.sym.name.s)
+      let name = Z3_mk_string_symbol(ctx, key)
      result = Z3_mk_const(ctx, name, typeToZ3(c, n.sym.typ))
      c.mapping[key] = result
      vars.add n
@@ -222,17 +344,23 @@ proc nodeToZ3(c: var DrCon; n: PNode; vars: var seq[PNode]): Z3_ast =
      result = Z3_mk_lt(ctx, rec n[1], rec n[2])
    of mLengthOpenArray, mLengthStr, mLengthArray, mLengthSeq:
      # len(x) needs the same logic as 'x' itself
-      if n[1].kind == nkSym:
-        let key = stableName(n)
-        let sym = n[1].sym
+      if isLoc(n[1], c.assumeUniqueness):
+        let key = stableName(c.up, n, scope)
        result = c.mapping.getOrDefault(key)
        if pointer(result) == nil:
-          let name = Z3_mk_string_symbol(ctx, sym.name.s & ".len")
+          let name = Z3_mk_string_symbol(ctx, key)
          result = Z3_mk_const(ctx, name, Z3_mk_int_sort(ctx))
          c.mapping[key] = result
          vars.add n
      else:
        notImplemented(renderTree(n))
+    of mHigh:
+      let addOpr = createMagic(c.graph, "+", mAddI)
+      let lenOpr = createMagic(c.graph, "len", mLengthOpenArray)
+      let asLenExpr = addOpr.buildCall(lenOpr.buildCall(n[1]), nkIntLit.newIntNode(-1))
+      result = rec asLenExpr
+    of mLow:
+      result = rec lowBound(c.graph.config, n[1])
    of mAddI, mSucc:
      result = binary(Z3_mk_add, rec n[1], rec n[2])
    of mSubI, mPred:
@@ -256,9 +384,12 @@ proc nodeToZ3(c: var DrCon; n: PNode; vars: var seq[PNode]): Z3_ast =
    of mLtU:
      result = Z3_mk_bvult(ctx, rec n[1], rec n[2])
    of mAnd:
-      result = binary(Z3_mk_and, rec n[1], rec n[2])
+      # 'a and b' <=> ite(a, b, false)
+      result = Z3_mk_ite(ctx, rec n[1], rec n[2], Z3_mk_false(ctx))
+      #result = binary(Z3_mk_and, rec n[1], rec n[2])
    of mOr:
-      result = binary(Z3_mk_or, rec n[1], rec n[2])
+      result = Z3_mk_ite(ctx, rec n[1], Z3_mk_true(ctx), rec n[2])
+      #result = binary(Z3_mk_or, rec n[1], rec n[2])
    of mXor:
      result = Z3_mk_xor(ctx, rec n[1], rec n[2])
    of mNot:
@@ -268,9 +399,9 @@ proc nodeToZ3(c: var DrCon; n: PNode; vars: var seq[PNode]): Z3_ast =
    of mIff:
      result = Z3_mk_iff(ctx, rec n[1], rec n[2])
    of mForall:
-      result = forallToZ3(c, n)
+      result = forallToZ3(c, n, scope)
    of mExists:
-      result = existsToZ3(c, n)
+      result = existsToZ3(c, n, scope)
    of mLeF64:
      result = Z3_mk_fpa_leq(ctx, rec n[1], rec n[2])
    of mLtF64:
@@ -299,11 +430,12 @@ proc nodeToZ3(c: var DrCon; n: PNode; vars: var seq[PNode]): Z3_ast =
    of mOrd, mChr:
      result = rec n[1]
    of mOld:
-      let key = (if c.canonParameterNames: paramName(n[1]) else: stableName(n[1])) & ".old"
+      let key = if c.canonParameterNames: (paramName(c.up, n[1]) & ".old")
+                else: stableName(c.up, n[1], scope, isOld = true)
      result = c.mapping.getOrDefault(key)
      if pointer(result) == nil:
-        let name = Z3_mk_string_symbol(ctx, $n)
-        result = Z3_mk_const(ctx, name, typeToZ3(c, n.typ))
+        let name = Z3_mk_string_symbol(ctx, key)
+        result = Z3_mk_const(ctx, name, typeToZ3(c, n[1].typ))
        c.mapping[key] = result
        # XXX change the logic in `addRangeInfo` for this
        #vars.add n
@@ -318,10 +450,10 @@ proc nodeToZ3(c: var DrCon; n: PNode; vars: var seq[PNode]): Z3_ast =
          ensuresEffects < op.n[0].len:
        let ensures = op.n[0][ensuresEffects]
        if ensures != nil and ensures.kind != nkEmpty:
-          let key = stableName(n)
+          let key = stableName(c.up, n, scope)
          result = c.mapping.getOrDefault(key)
          if pointer(result) == nil:
-            let name = Z3_mk_string_symbol(ctx, $n)
+            let name = Z3_mk_string_symbol(ctx, key)
            result = Z3_mk_const(ctx, name, typeToZ3(c, n.typ))
            c.mapping[key] = result
            vars.add n
@@ -333,15 +465,24 @@ proc nodeToZ3(c: var DrCon; n: PNode; vars: var seq[PNode]): Z3_ast =
    for i in 0..n.len-2:
      isTrivial = isTrivial and n[i].kind in {nkEmpty, nkCommentStmt}
    if isTrivial:
-      result = nodeToZ3(c, n[^1], vars)
+      result = rec n[^1]
    else:
      notImplemented(renderTree(n))
  of nkHiddenDeref:
    result = rec n[0]
  else:
-    notImplemented(renderTree(n))
+    if isLoc(n, c.assumeUniqueness):
+      let key = stableName(c.up, n, scope)
+      result = c.mapping.getOrDefault(key)
+      if pointer(result) == nil:
+        let name = Z3_mk_string_symbol(ctx, key)
+        result = Z3_mk_const(ctx, name, typeToZ3(c, n.typ))
+        c.mapping[key] = result
+        vars.add n
+    else:
+      notImplemented(renderTree(n))

-proc addRangeInfo(c: var DrCon, n: PNode, res: var seq[Z3_ast]) =
+proc addRangeInfo(c: var DrCon, n: PNode; scope: VersionScope, res: var seq[Z3_ast]) =
  var cmpOp = mLeI
  if n.typ != nil:
    cmpOp =
@@ -393,15 +534,15 @@ proc addRangeInfo(c: var DrCon, n: PNode, res: var seq[Z3_ast]) =
      let ensures = op.n[0][ensuresEffects]
      if ensures != nil and ensures.kind != nkEmpty:
        var dummy: seq[PNode]
-        res.add nodeToZ3(c, translateEnsures(ensures, n), dummy)
+        res.add nodeToZ3(c, translateEnsures(ensures, n), scope, dummy)
    return

  let x = newTree(nkInfix, newSymNode createMagic(c.graph, "<=", cmpOp), lowBound, n)
  let y = newTree(nkInfix, newSymNode createMagic(c.graph, "<=", cmpOp), n, highBound)

  var dummy: seq[PNode]
-  res.add nodeToZ3(c, x, dummy)
-  res.add nodeToZ3(c, y, dummy)
+  res.add nodeToZ3(c, x, scope, dummy)
+  res.add nodeToZ3(c, y, scope, dummy)

 proc on_err(ctx: Z3_context, e: Z3_error_code) {.nimcall.} =
  #writeStackTrace()
@@ -423,18 +564,18 @@ proc conj(ctx: Z3_context; conds: seq[Z3_ast]): Z3_ast =
  else:
    result = Z3_mk_true(ctx)

-proc proofEngineAux(c: var DrCon; assumptions: seq[PNode]; toProve: PNode): (bool, string) =
-  c.mapping = initTable[string, Z3_ast]()
+proc setupZ3(): Z3_context =
  let cfg = Z3_mk_config()
-  Z3_set_param_value(cfg, "model", "true");
-  let ctx = Z3_mk_context(cfg)
-  c.z3 = ctx
-  Z3_del_config(cfg)
-  Z3_set_error_handler(ctx, on_err)
-
  when false:
    Z3_set_param_value(cfg, "timeout", "1000")
+  Z3_set_param_value(cfg, "model", "true")
+  result = Z3_mk_context(cfg)
+  Z3_del_config(cfg)
+  Z3_set_error_handler(result, on_err)

+proc proofEngineAux(c: var DrCon; assumptions: seq[(PNode, VersionScope)];
+                    toProve: (PNode, VersionScope)): (bool, string) =
+  c.mapping = initTable[string, Z3_ast]()
  try:

    #[
@@ -455,20 +596,21 @@ proc proofEngineAux(c: var DrCon; assumptions: seq[PNode]; toProve: PNode): (boo

    var collectedVars: seq[PNode]

+    template ctx(): untyped = c.up.z3
+
    let solver = Z3_mk_solver(ctx)
    var lhs: seq[Z3_ast]
-    for assumption in assumptions:
-      if assumption != nil:
-        try:
-          let za = nodeToZ3(c, assumption, collectedVars)
-          #Z3_solver_assert ctx, solver, za
-          lhs.add za
-        except CannotMapToZ3Error:
-          discard "ignore a fact we cannot map to Z3"
+    for assumption in items(assumptions):
+      try:
+        let za = nodeToZ3(c, assumption[0], assumption[1], collectedVars)
+        #Z3_solver_assert ctx, solver, za
+        lhs.add za
+      except CannotMapToZ3Error:
+        discard "ignore a fact we cannot map to Z3"

-    let z3toProve = nodeToZ3(c, toProve, collectedVars)
+    let z3toProve = nodeToZ3(c, toProve[0], toProve[1], collectedVars)
    for v in collectedVars:
-      addRangeInfo(c, v, lhs)
+      addRangeInfo(c, v, toProve[1], lhs)

    # to make Z3 produce nice counterexamples, we try to prove the
    # negation of our conjecture and see if it's Z3_L_FALSE
@@ -476,7 +618,8 @@ proc proofEngineAux(c: var DrCon; assumptions: seq[PNode]; toProve: PNode): (boo

    #Z3_mk_not(ctx, forall(ctx, collectedVars, conj(ctx, lhs), z3toProve))

-    #echo "toProve: ", Z3_ast_to_string(ctx, fa), " ", c.graph.config $ toProve.info
+    when defined(dz3):
+      echo "toProve: ", Z3_ast_to_string(ctx, fa), " ", c.graph.config $ toProve[0].info, " ", int(toProve[1])
    Z3_solver_assert ctx, solver, fa

    let z3res = Z3_solver_check(ctx, solver)
@@ -489,18 +632,22 @@ proc proofEngineAux(c: var DrCon; assumptions: seq[PNode]; toProve: PNode): (boo
  except ValueError:
    result[0] = false
    result[1] = getCurrentExceptionMsg()
-  finally:
-    Z3_del_context(ctx)

-proc proofEngine(graph: ModuleGraph; assumptions: seq[PNode]; toProve: PNode): (bool, string) =
+proc proofEngine(ctx: DrnimContext; assumptions: seq[(PNode, VersionScope)];
+                 toProve: (PNode, VersionScope)): (bool, string) =
  var c: DrCon
-  c.graph = graph
+  c.graph = ctx.graph
+  c.assumeUniqueness = assumeUniqueness
+  c.up = ctx
  result = proofEngineAux(c, assumptions, toProve)

+proc skipAddr(n: PNode): PNode {.inline.} =
+  (if n.kind == nkHiddenAddr: n[0] else: n)
+
 proc translateReq(r, call: PNode): PNode =
  if r.kind == nkSym and r.sym.kind == skParam:
    if r.sym.position+1 < call.len:
-      result = call[r.sym.position+1]
+      result = call[r.sym.position+1].skipAddr
    else:
      notImplemented("no argument given for formal parameter: " & r.sym.name.s)
  else:
@@ -508,11 +655,11 @@ proc translateReq(r, call: PNode): PNode =
    for i in 0 ..< safeLen(r):
      result[i] = translateReq(r[i], call)

-proc requirementsCheck(graph: ModuleGraph; assumptions: seq[PNode];
-                      call, requirement: PNode): (bool, string) {.nimcall.} =
+proc requirementsCheck(ctx: DrnimContext; assumptions: seq[(PNode, VersionScope)];
+                      call, requirement: PNode): (bool, string) =
  try:
    let r = translateReq(requirement, call)
-    result = proofEngine(graph, assumptions, r)
+    result = proofEngine(ctx, assumptions, (r, ctx.currentScope))
  except ValueError:
    result[0] = false
    result[1] = getCurrentExceptionMsg()
@@ -552,24 +699,347 @@ proc compatibleProps(graph: ModuleGraph; formal, actual: PType): bool {.nimcall.
      var c: DrCon
      c.graph = graph
      c.canonParameterNames = true
-      if not frequires.isEmpty:
-        result = not arequires.isEmpty and proofEngineAux(c, @[frequires], arequires)[0]
+      try:
+        c.up = DrnimContext(z3: setupZ3(), o: initOperators(graph), graph: graph, owner: nil)
+        template zero: untyped = VersionScope(0)
+        if not frequires.isEmpty:
+          result = not arequires.isEmpty and proofEngineAux(c, @[(frequires, zero)], (arequires, zero))[0]

-      if result:
-        if not fensures.isEmpty:
-          result = not aensures.isEmpty and proofEngineAux(c, @[aensures], fensures)[0]
+        if result:
+          if not fensures.isEmpty:
+            result = not aensures.isEmpty and proofEngineAux(c, @[(aensures, zero)], (fensures, zero))[0]
+      finally:
+        Z3_del_context(c.up.z3)
    else:
      # formal has requirements but 'actual' has none, so make it
      # incompatible. XXX What if the requirement only mentions that
      # we already know from the type system?
      result = frequires.isEmpty and fensures.isEmpty

+template config(c: typed): untyped = c.graph.config
+
+proc addFact(c: DrnimContext; n: PNode) =
+  let v = c.currentScope
+  if n[0].kind == nkSym and n[0].sym.magic in {mOr, mAnd}:
+    c.facts.add((n[1], v))
+  c.facts.add((n, v))
+
+proc addFactNeg(c: DrnimContext; n: PNode) =
+  var neg = newNodeI(nkCall, n.info, 2)
+  neg[0] = newSymNode(c.o.opNot)
+  neg[1] = n
+  addFact(c, neg)
+
+proc prove(c: DrnimContext; prop: PNode): bool =
+  let (success, m) = proofEngine(c, c.facts, (prop, c.currentScope))
+  if not success:
+    message(c.config, prop.info, warnStaticIndexCheck, "cannot prove: " & $prop & m)
+  result = success
+
+proc traversePragmaStmt(c: DrnimContext, n: PNode) =
+  for it in n:
+    if it.kind == nkExprColonExpr:
+      let pragma = whichPragma(it)
+      if pragma == wAssume:
+        addFact(c, it[1])
+      elif pragma == wInvariant or pragma == wAssert:
+        if prove(c, it[1]):
+          addFact(c, it[1])
+
+proc requiresCheck(c: DrnimContext, call: PNode; op: PType) =
+  assert op.n[0].kind == nkEffectList
+  if requiresEffects < op.n[0].len:
+    let requires = op.n[0][requiresEffects]
+    if requires != nil and requires.kind != nkEmpty:
+      # we need to map the call arguments to the formal parameters used inside
+      # 'requires':
+      let (success, m) = requirementsCheck(c, c.facts, call, requires)
+      if not success:
+        message(c.config, call.info, warnStaticIndexCheck, "cannot prove: " & $requires & m)
+
+proc freshVersion(c: DrnimContext; arg: PNode) =
+  let v = getRoot(arg)
+  if v != nil:
+    c.varVersions.add v.id
+
+proc translateEnsuresFromCall(c: DrnimContext, e, call: PNode): PNode =
+  if e.kind in nkCallKinds and e[0].kind == nkSym and e[0].sym.magic == mOld:
+    assert e[1].kind == nkSym and e[1].sym.kind == skParam
+    let param = e[1].sym
+    let arg = call[param.position+1].skipAddr
+    result = buildCall(e[0].sym, arg)
+  elif e.kind == nkSym and e.sym.kind == skParam:
+    let param = e.sym
+    let arg = call[param.position+1].skipAddr
+    result = arg
+  else:
+    result = shallowCopy(e)
+    for i in 0 ..< safeLen(e): result[i] = translateEnsuresFromCall(c, e[i], call)
+
+proc collectEnsuredFacts(c: DrnimContext, call: PNode; op: PType) =
+  assert op.n[0].kind == nkEffectList
+  for i in 1 ..< min(call.len, op.len):
+    if op[i].kind == tyVar:
+      freshVersion(c, call[i].skipAddr)
+
+  if ensuresEffects < op.n[0].len:
+    let ensures = op.n[0][ensuresEffects]
+    if ensures != nil and ensures.kind != nkEmpty:
+      addFact(c, translateEnsuresFromCall(c, ensures, call))
+
+proc checkLe(c: DrnimContext, a, b: PNode) =
+  var cmpOp = mLeI
+  if a.typ != nil:
+    case a.typ.skipTypes(abstractInst).kind
+    of tyFloat..tyFloat128: cmpOp = mLeF64
+    of tyChar, tyUInt..tyUInt64: cmpOp = mLeU
+    else: discard
+
+  let cmp = newTree(nkInfix, newSymNode createMagic(c.graph, "<=", cmpOp), a, b)
+  cmp.info = a.info
+  discard prove(c, cmp)
+
+proc checkBounds(c: DrnimContext; arr, idx: PNode) =
+  checkLe(c, lowBound(c.config, arr), idx)
+  checkLe(c, idx, highBound(c.config, arr, c.o))
+
+proc checkRange(c: DrnimContext; value: PNode; typ: PType) =
+  let t = typ.skipTypes(abstractInst - {tyRange})
+  if t.kind == tyRange:
+    let lowBound = copyTree(t.n[0])
+    lowBound.info = value.info
+    let highBound = copyTree(t.n[1])
+    highBound.info = value.info
+    checkLe(c, lowBound, value)
+    checkLe(c, value, highBound)
+
+proc addAsgnFact*(c: DrnimContext, key, value: PNode) =
+  var fact = newNodeI(nkCall, key.info, 3)
+  fact[0] = newSymNode(c.o.opEq)
+  fact[1] = key
+  fact[2] = value
+  c.facts.add((fact, c.currentScope))
+
+proc traverse(c: DrnimContext; n: PNode)
+
+proc traverseTryStmt(c: DrnimContext; n: PNode) =
+  traverse(c, n[0])
+  let oldFacts = c.facts.len
+  for i in 1 ..< n.len:
+    traverse(c, n[i].lastSon)
+  setLen(c.facts, oldFacts)
+
+proc traverseCase(c: DrnimContext; n: PNode) =
+  traverse(c, n[0])
+  let oldFacts = c.facts.len
+  for i in 1 ..< n.len:
+    traverse(c, n[i].lastSon)
+  # XXX make this as smart as 'if elif'
+  setLen(c.facts, oldFacts)
+
+proc traverseIf(c: DrnimContext; n: PNode) =
+  traverse(c, n[0][0])
+  let oldFacts = c.facts.len
+  addFact(c, n[0][0])
+
+  traverse(c, n[0][1])
+
+  for i in 1..<n.len:
+    let branch = n[i]
+    setLen(c.facts, oldFacts)
+    for j in 0..i-1:
+      addFactNeg(c, n[j][0])
+    if branch.len > 1:
+      addFact(c, branch[0])
+    for i in 0..<branch.len:
+      traverse(c, branch[i])
+  setLen(c.facts, oldFacts)
+
+proc traverseBlock(c: DrnimContext; n: PNode) =
+  traverse(c, n)
+
+proc addFactLe(c: DrnimContext; a, b: PNode) =
+  c.addFact c.o.opLe.buildCall(a, b)
+
+proc addFactLt(c: DrnimContext; a, b: PNode) =
+  c.addFact c.o.opLt.buildCall(a, b)
+
+proc ensuresCheck(c: DrnimContext; owner: PSym) =
+  if owner.typ != nil and owner.typ.kind == tyProc and owner.typ.n != nil:
+    let n = owner.typ.n
+    if n.len > 0 and n[0].kind == nkEffectList and ensuresEffects < n[0].len:
+      let ensures = n[0][ensuresEffects]
+      if ensures != nil and ensures.kind != nkEmpty:
+        discard prove(c, ensures)
+
+proc traverseAsgn(c: DrnimContext; n: PNode) =
+  traverse(c, n[0])
+  traverse(c, n[1])
+
+  proc replaceByOldParams(fact, le: PNode): PNode =
+    if guards.sameTree(fact, le):
+      result = newNodeIT(nkCall, fact.info, fact.typ)
+      result.add newSymNode createMagic(c.graph, "old", mOld)
+      result.add fact
+    else:
+      result = shallowCopy(fact)
+      for i in 0 ..< safeLen(fact):
+        result[i] = replaceByOldParams(fact[i], le)
+
+  freshVersion(c, n[0])
+  addAsgnFact(c, n[0], replaceByOldParams(n[1], n[0]))
+  when defined(debug):
+    echoFacts(c)
+
+proc traverse(c: DrnimContext; n: PNode) =
+  case n.kind
+  of nkEmpty..nkNilLit:
+    discard "nothing to do"
+  of nkRaiseStmt, nkBreakStmt, nkContinueStmt:
+    inc c.hasUnstructedCf
+    for i in 0..<n.safeLen:
+      traverse(c, n[i])
+  of nkReturnStmt:
+    for i in 0 ..< n.safeLen:
+      traverse(c, n[i])
+    ensuresCheck(c, c.owner)
+  of nkCallKinds:
+    # p's effects are ours too:
+    var a = n[0]
+    let op = a.typ
+    if op != nil and op.kind == tyProc and op.n[0].kind == nkEffectList:
+      requiresCheck(c, n, op)
+      collectEnsuredFacts(c, n, op)
+    if a.kind == nkSym:
+      case a.sym.magic
+      of mNew, mNewFinalize, mNewSeq:
+        # may not look like an assignment, but it is:
+        let arg = n[1]
+        freshVersion(c, arg)
+        traverse(c, arg)
+        addAsgnFact(c, arg, newNodeIT(nkObjConstr, arg.info, arg.typ))
+      of mArrGet, mArrPut:
+        #if optStaticBoundsCheck in c.currOptions: checkBounds(c, n[1], n[2])
+        discard
+      else:
+        discard
+
+    for i in 0..<n.safeLen:
+      traverse(c, n[i])
+  of nkDotExpr:
+    #guardDotAccess(c, n)
+    for i in 0..<n.len: traverse(c, n[i])
+  of nkCheckedFieldExpr:
+    traverse(c, n[0])
+    #checkFieldAccess(c.facts, n, c.config)
+  of nkTryStmt: traverseTryStmt(c, n)
+  of nkPragma: traversePragmaStmt(c, n)
+  of nkAsgn, nkFastAsgn: traverseAsgn(c, n)
+  of nkVarSection, nkLetSection:
+    for child in n:
+      let last = lastSon(child)
+      if last.kind != nkEmpty: traverse(c, last)
+      if child.kind == nkIdentDefs and last.kind != nkEmpty:
+        for i in 0..<child.len-2:
+          addAsgnFact(c, child[i], last)
+      elif child.kind == nkVarTuple and last.kind != nkEmpty:
+        for i in 0..<child.len-1:
+          if child[i].kind == nkEmpty or
+              child[i].kind == nkSym and child[i].sym.name.s == "_":
+            discard "anon variable"
+          elif last.kind in {nkPar, nkTupleConstr}:
+            addAsgnFact(c, child[i], last[i])
+  of nkConstSection:
+    for child in n:
+      let last = lastSon(child)
+      traverse(c, last)
+  of nkCaseStmt: traverseCase(c, n)
+  of nkWhen, nkIfStmt, nkIfExpr: traverseIf(c, n)
+  of nkBlockStmt, nkBlockExpr: traverseBlock(c, n[1])
+  of nkWhileStmt:
+    # 'while true' loop?
+    if isTrue(n[0]):
+      traverseBlock(c, n[1])
+    else:
+      let oldFacts = c.facts.len
+      addFact(c, n[0])
+      traverse(c, n[0])
+      traverse(c, n[1])
+      setLen(c.facts, oldFacts)
+  of nkForStmt, nkParForStmt:
+    # we are very conservative here and assume the loop is never executed:
+    let oldFacts = c.facts.len
+    let iterCall = n[n.len-2]
+    if optStaticBoundsCheck in c.currOptions and iterCall.kind in nkCallKinds:
+      let op = iterCall[0]
+      if op.kind == nkSym and fromSystem(op.sym):
+        let iterVar = n[0]
+        case op.sym.name.s
+        of "..", "countup", "countdown":
+          let lower = iterCall[1]
+          let upper = iterCall[2]
+          # for i in 0..n   means  0 <= i and i <= n. Countdown is
+          # the same since only the iteration direction changes.
+          addFactLe(c, lower, iterVar)
+          addFactLe(c, iterVar, upper)
+        of "..<":
+          let lower = iterCall[1]
+          let upper = iterCall[2]
+          addFactLe(c, lower, iterVar)
+          addFactLt(c, iterVar, upper)
+        else: discard
+
+    for i in 0..<n.len-2:
+      let it = n[i]
+      traverse(c, it)
+    let loopBody = n[^1]
+    traverse(c, iterCall)
+    traverse(c, loopBody)
+    setLen(c.facts, oldFacts)
+  of nkTypeSection, nkProcDef, nkConverterDef, nkMethodDef, nkIteratorDef,
+      nkMacroDef, nkTemplateDef, nkLambda, nkDo, nkFuncDef:
+    discard
+  of nkCast:
+    if n.len == 2:
+      traverse(c, n[1])
+  of nkHiddenStdConv, nkHiddenSubConv, nkConv:
+    if n.len == 2:
+      traverse(c, n[1])
+      if optStaticBoundsCheck in c.currOptions:
+        checkRange(c, n[1], n.typ)
+  of nkObjUpConv, nkObjDownConv, nkChckRange, nkChckRangeF, nkChckRange64:
+    if n.len == 1:
+      traverse(c, n[0])
+      if optStaticBoundsCheck in c.currOptions:
+        checkRange(c, n[0], n.typ)
+  of nkBracketExpr:
+    if optStaticBoundsCheck in c.currOptions and n.len == 2:
+      if n[0].typ != nil and skipTypes(n[0].typ, abstractVar).kind != tyTuple:
+        checkBounds(c, n[0], n[1])
+    for i in 0 ..< n.len: traverse(c, n[i])
+  else:
+    for i in 0 ..< n.len: traverse(c, n[i])
+
+proc strongSemCheck(graph: ModuleGraph; owner: PSym; n: PNode) =
+  var c = DrnimContext()
+  c.currOptions = graph.config.options + owner.options
+  if optStaticBoundsCheck in c.currOptions:
+    c.z3 = setupZ3()
+    c.o = initOperators(graph)
+    c.graph = graph
+    c.owner = owner
+    try:
+      traverse(c, n)
+      ensuresCheck(c, owner)
+    finally:
+      Z3_del_context(c.z3)
+
+
 proc mainCommand(graph: ModuleGraph) =
  let conf = graph.config
  conf.lastCmdTime = epochTime()

-  graph.proofEngine = proofEngine
-  graph.requirementsCheck = requirementsCheck
+  graph.strongSemCheck = strongSemCheck
  graph.compatibleProps = compatibleProps

  graph.config.errorMax = high(int)  # do not stop after first error
@@ -600,20 +1070,6 @@ proc mainCommand(graph: ModuleGraph) =
      "output", output,
      ])

-proc prependCurDir(f: AbsoluteFile): AbsoluteFile =
-  when defined(unix):
-    if os.isAbsolute(f.string): result = f
-    else: result = AbsoluteFile("./" & f.string)
-  else:
-    result = f
-
-proc addCmdPrefix(result: var string, kind: CmdLineKind) =
-  # consider moving this to std/parseopt
-  case kind
-  of cmdLongOption: result.add "--"
-  of cmdShortOption: result.add "-"
-  of cmdArgument, cmdEnd: discard
-
 proc processCmdLine(pass: TCmdLinePass, cmd: string; config: ConfigRef) =
  var p = parseopt.initOptParser(cmd)
  var argsCount = 1
@@ -638,7 +1094,11 @@ proc processCmdLine(pass: TCmdLinePass, cmd: string; config: ConfigRef) =
        p.key = "-"
        if processArgument(pass, p, argsCount, config): break
      else:
-        processSwitch(pass, p, config)
+        case p.key.normalize
+        of "assumeunique":
+          assumeUniqueness = true
+        else:
+          processSwitch(pass, p, config)
    of cmdArgument:
      config.commandLine.add " "
      config.commandLine.add p.key.quoteShell
--- 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])
--- 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.}
--- 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".}