From 00a85d2d1b2a792d78f84a2225bae87592fb2acc Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Mon, 13 Nov 2023 17:25:52 -0800
Subject: [PATCH] Relaxes type-checker to allow old expressions referring to a
 magic wand's LHS

---
 .../typing/ghost/GhostMiscTyping.scala        |  1 +
 .../resources/regressions/issues/000705.gobra | 75 +++++++++++++++++++
 2 files changed, 76 insertions(+)
 create mode 100644 src/test/resources/regressions/issues/000705.gobra

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala
index ef273194c..29112774b 100644
--- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala
+++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala
@@ -283,6 +283,7 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl =>
 
   private def illegalPreconditionNode(n: PNode): Messages = {
     n match {
+      case PLabeledOld(PLabelUse(PLabelNode.lhsLabel), _) => noMessages
       case n@ (_: POld | _: PLabeledOld) => message(n, s"old not permitted in precondition")
       case n@ (_: PBefore) => message(n, s"old not permitted in precondition")
       case _ => noMessages
diff --git a/src/test/resources/regressions/issues/000705.gobra b/src/test/resources/regressions/issues/000705.gobra
new file mode 100644
index 000000000..1912c34c1
--- /dev/null
+++ b/src/test/resources/regressions/issues/000705.gobra
@@ -0,0 +1,75 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000705
+
+// adapted from Viper tutorial on magic wands
+
+type ListEntry struct {
+    next *ListEntry
+    value int
+}
+
+pred (l *ListEntry) List() {
+    acc(l) && (l.next != nil ==> l.next.List())
+}
+
+ghost
+requires acc(l.List(), _)
+pure func (l *ListEntry) Elems() (res seq[int]) {
+    return unfolding acc(l.List(), _) in (
+        l.next == nil ? seq[int]{ l.value } :
+            seq[int]{ l.value } ++ l.next.Elems())
+}
+
+requires l1.List() && l2.List() && l2 != nil
+ensures  l1.List() && l1.Elems() == old(l1.Elems() ++ l2.Elems())
+func (l1 *ListEntry) append(l2 *ListEntry) {
+    unfold l1.List()
+    if l1.next == nil {
+        l1.next = l2
+        fold l1.List()
+    } else {
+        tmp := l1.next
+        index := 1
+
+        package tmp.List() --* (l1.List() && l1.Elems() == old(l1.Elems()[:index]) ++ old[#lhs](tmp.Elems())) {
+            fold l1.List()
+        }
+
+        newTmp, newIndex := l1.appendSubroutine(tmp, old(l1.Elems()))
+
+        unfold newTmp.List()
+        newTmp.next = l2
+        fold newTmp.List()
+        apply newTmp.List() --* (l1.List() && l1.Elems() == old(l1.Elems()[:newIndex]) ++ old[#lhs](newTmp.Elems()))
+    }
+}
+
+requires tmp.List() && /*acc(l1) && l1.next == tmp &&*/ tmp.Elems() == elems[1:]
+requires tmp.List() --* (l1.List() && l1.Elems() == elems[:1] ++ old[#lhs](tmp.Elems()))
+ensures 0 <= newIndex
+ensures newTmp.List() && newTmp.Elems() == elems[newIndex:]
+ensures unfolding newTmp.List() in newTmp.next == nil
+ensures newTmp.List() --* (l1.List() && l1.Elems() == elems[:newIndex] ++ old[#lhs](newTmp.Elems()))
+func (l1 *ListEntry) appendSubroutine(tmp *ListEntry, ghost elems seq[int]) (newTmp *ListEntry, newIndex int) {
+    index := 1
+
+    invariant 0 <= index
+    invariant tmp.List() && tmp.Elems() == elems[index:]
+    invariant tmp.List() --* (l1.List() && l1.Elems() == elems[:index] ++ old[#lhs](tmp.Elems()))
+    for unfolding tmp.List() in tmp.next != nil {
+        unfold tmp.List()
+        prev := tmp
+        tmp = tmp.next
+        index = index + 1
+        package tmp.List() --* (l1.List() && l1.Elems() == elems[:index] ++ old[#lhs](tmp.Elems())) {
+            fold prev.List()
+            apply prev.List() --* (l1.List() && l1.Elems() == elems[:index-1] ++ old[#lhs](prev.Elems()))
+        }
+    }
+
+    newTmp = tmp
+    newIndex = index
+    return
+}