Deep structure updates in non-aliased imperative (was: `computes` to use condition as a more efficient implementation)

[samuelchassot]

Add computes that works as follows:

def f(x: BigInt): BigInt = {
    body(x)
} computes(v(x))

By default, computes behaves as ensuring(_ == v(x)) but with StaticChecks, it inlines v(x) and ignores body(x).

We can also use this to implement a tail pointer on list, with the update to the new value being in the computes, and the recursive traversal in body(...).

[vkuncak]

The question is, if we mean that v(x) is the implementation, why do we not write it the other way round,

def f(x: BigInt): BigInt = {
  v(x)
}.ensuring(_ == body(x))

Our motivation was that body would be defined in a way that passes aliasing restrictions, whereas v(x) would possibly break it. But I do not see how v(x) would be allowed to break it.

[vkuncak]

The idea is basically to implement a form of field constraint analysis in Stainless

http://lara.epfl.ch/~kuncak/papers/WiesETAL06FieldConstraintAnalysis.pdf

which built on

N. Klarlund and M. I. Schwartzbach. Graph types. In Proc. 20th ACM POPL, Charleston, SC, 1993. A. Møller and M. I. Schwartzbach. The Pointer Assertion Logic Engine. In Programming Language Design and Implementation, 2001.

[vkuncak]

What we really seem to need here is encapsulating private state. We can probably introduce this as an abstraction of stateful function pattern

https://github.com/epfl-lara/stainless/blob/92ee79963258a2187b253e0a3f5bec77bf66a878/frontends/benchmarks/imperative/valid/Tutorial.scala#L195

but restricted in both initialization and state change so that the state is not externally observable.

[vkuncak]

To make things more concrete, the code below tries to implement a list with a tail pointer.

  import stainless.lang.*
  import stainless.lang.StaticChecks.*
  import stainless.annotation.*

  @mutable
  sealed abstract class Opt[@mutable T]
  case class NONE[@mutable T]() extends Opt[T]
  case class SOME[@mutable T](value: T) extends Opt[T]

  @ignore
  class pointer extends scala.annotation.Annotation

  final case class Node(var head: Int, var next: Cell[Opt[Node]])

  @extern
  def getLast(n: Node): Node =    
    n.next.v match
      case NONE() => n
      case SOME(next) => getLast(next)

  final case class TList(var first: Node,
                         @pointer var last: Node) {
    require(last == getLast(first))

    def isEmpty: Boolean =
      first.next.v == NONE()

    def popFirst: Int =
      require(!isEmpty)
      n.next.v match
        case SOME(n1) => 
          n1.head
          n.next = Cell(NONE())

    def addToEnd(x: Int): Unit =
      updateLast(last, mkEnd(x))
  }

  def updateLast(last: Node, newOne: Node): Unit =
    last.next.v = SOME(newOne)

  def mkEnd(head: Int): Node = Node(head, Cell(NONE[Node]()))

The idea would be that an invocation updateLast(last, mkEnd(x)) would get rewritten, for the purpose of verification but not code generation, to resolve_last_updateLast(first, mkEnd(x)) where

  def resolve_last_updateLast(n: Node, newOne: Node): Node =    
    n.next.v match
      case NONE() => n
      case SOME(next) =>  // computation of last as in getLast
        last.next.v = SOME(newOne) // the body of the original updateLast      

The @pointer fields need to be exempt from alias checks. All their uses need to be rewritten. Perhaps a bit unusually, we can write to such pointer fields, but in the current getLast is not accepted as it returns a deep pointer.

This suggest that accessors should be written explicitly as accessor mutators, e.g.:

  def applyToLast(n: Node, action: Node => Unit): Unit = 
    decreases(n.len)
    n.next.v match
      case NONE() => action(n)
      case SOME(next) => applyToLast(next, action)

but then it is not clear how to relate the path traversed and the value traversed and how to write class invariants.