list.forall and proofs

[BLepers]

@induct
def updateProcLemma(s:SharedState, c:BigInt, u:BigInt, p:Process, l:List[BigInt]):Boolean = {
   l.forall(e => if(e != u) updateProc(s, c, u, p)(e) == s.procs(e) else true);
}.holds;

In another proof:
updateProcLemma(s, c, s.states(c).current_0.get, res.procs(old_current), s.states(c).ready) && // ok
s.states(c).ready.forall(e => if(e != s.states(c).current_0.get) updateProc(s, c, s.states(c).current_0.get, res.procs(old_current))(e) == s.procs(e) else true) // unable to verify, but why?

Stainless is not able to prove the last line. It seems to me that this is a direct search & replace of the content of updateProcLemma. Is there any reason for that?

Sorry if this has been mentioned somewhere else. I remember having read somewhere that the forall() quantifier was treated as a black box, but is list.forall the same?

[BLepers]

import stainless.collection._
import stainless.lang._
import scala.Any
import stainless.annotation._
import stainless.proof._
import stainless.util.Random

object Scheduler {
   case class SharedState(val ready:List[BigInt], val procs:BigInt => BigInt);

   def updateProc(s:SharedState, u:BigInt, p:BigInt)(id:BigInt):BigInt = {
      if (id == u) p else s.procs(id)
   }

   def updateProcLemma(s:SharedState, l:List[BigInt], u:BigInt, p:BigInt):Boolean = {
      l.forall(t => if(t != u) s.procs(t) == updateProc(s, u, p)(t) else true)
   }

   def test(s:SharedState, u:BigInt, p:BigInt):Boolean = {
      require(updateProcLemma(s, s.ready, u, p))
      var res = new SharedState(
         s.ready,
         updateProc(s, u, p)
      );
      //s.ready.forall(t => if(t != u) s.procs(t) == updateProc(s, u, p)(t) else true) // ok
      s.ready.forall(t => if(t != u) s.procs(t) == res.procs(t) else true) // ko
   }.holds;
}

Simple example. Is there a way to prove the last line? :)

[jad-hamza]

I think this is related to the way equality of lambdas is treated in Stainless.
I think the lamdas (t => if(t != u) s.procs(t) == res.procs(t) else true) and (t => if(t != u) s.procs(t) == updateProc(s, u, p)(t) else true) are considered to be different.

I've simplified the example to highlight the issue, and give a possible workaround.
The first assertion shows that similar lambdas can be considered different.
The second assertion is our assumption.
The third assertion is a call to a lemma, that uses our assumption and shows what we want.
The last assertion is what we want to prove.

About List.forall, I don't think it gets a particular treatment. Forall is a construct defined outside the
language, while List.forall is defined in the library as a recursive function over the list. So one way
to prove List.forall statements is to do an induction on the List (what lemma does here).

This workaround is not very pretty, but it works!

import stainless.collection._
import stainless.lang._
import stainless.annotation._

object Scheduler {
  case class SharedState(val procs: BigInt => BigInt)

  @induct
  def lemma(l: List[BigInt], f: BigInt => BigInt) = {
    require(l.forall(t => t == 0) && forall((x: BigInt) => f(x) == 0))

    l.forall(t => t == f(t))
  } holds

  def test(s:SharedState, ready: List[BigInt]) = {
    require(ready.forall(t => t == 0))
    val res = new SharedState(_ => 0) 
    assert(((t: BigInt) => t == 0) != ((t: BigInt) => t == res.procs(t))) // ok
    assert(ready.forall(t => t == 0))                                     // ok
    assert(lemma(ready, res.procs))                                       // ok
    assert(ready.forall(t => t == res.procs(t)))                          // ko without the lemma at the previous line
  }
}

[BLepers]

val res = new SharedState(_ => 0) 
assert(((t: BigInt) => t == 0) != ((t: BigInt) => t == res.procs(t))) // ok

That is a bit strange :) Is there any reason why this is the desirable behaviour? It seems to me that the assert should return false here?

Thanks for the explanations!

[jad-hamza]

Yes I agree; I think this is related to the discussion #62,
where @samarion explained this design choice. Roughly, the goal was to keep the equality between
lambdas decidable, so that the semantics of a formula/statement can be given by the operational
semantics of executing the formula. (So you can always check equality between two functions, and
get true or false.)

[samarion]

The initial example is now proved equal given some new normalizations in epfl-lara/inox@bc386af
The more general question of function equality in Stainless is still on the hook and may or may not change at some point in the future. Closing this particular issue in the meantime.