Cross execution access bug in `rel()` and `ghost if` blocks

[AkasakaJelos]

Consider the following example:

package exercises

// ##(--hyperMode extended --enableExperimentalHyperFeatures)

// @ ghost
// @ decreases
func GetInt() (res int)

// @ requires rel(t, 0) != rel(t, 1)
func test5_RelationalIndexBug(t uint64) {
	steps := make([]uint64, 20)

	//@ ghost var t0 uint64 = rel(t, 0)
	//@ ghost var t1 uint64 = rel(t, 1)

	//@ idx1 := GetInt()

	//@ assume t0 < t1 ==> 0 <= idx1 && idx1 < rel(len(steps), 0)
	//@ assume t0 < t1 ==> 0<= idx1 && idx1 < len(rel(steps,0))

	/*@
	  ghost if t0 < t1 {
	      ghost var TStar uint64 = rel(steps[idx1], 0)
	  }
	  @*/
}

If we run on Gobra, Gobra will return the following error:

[info] Error at: </.../exercises/relissues8.go:30:18> Assignment might fail.
[info] Permission to steps[idx1] might not suffice.

(Did an initial mistake with analysis, as my example was bad. Please see the comments below.)

[jcp19]

I didn't think so much about this example, but I have a few questions:

1. Why do you introduce the assume acc(steps) in the program? The allocation of steps should already establish the permissions to it.
2. Maybe I'm missing sth, but why do you expect this program to verify? In particular, I don't see how this program is safe for the minor execution (i.e., for the execution whose expressions are evaluated using rel(-, 1)). This program never constraints in any way the value of rel(idx1, 1), and thus, I don't see how the statement ghost var TStar uint64 = rel(steps[idx1], 0) is safe in the 2nd execution.

[AkasakaJelos]

1. I’m working on a similar program that returns an array, which already inherits //@ ensures acc(steps). In that case, I think the statement is redundant. I wasn’t sure whether this was the root cause when analysing the bug, and I forgot to remove it when pasting. But you’re right, it isn’t necessary.

2. Sorry, this is a good catch. You're correct that the current example should not verify.
   I was rather referring to: //@ assume t0 < t1 ==> 0 <= idx1 && idx1 < rel(len(steps), 0) instead of //@ assume t0 < t1 ==> 0 <= rel(idx1, 0) && rel(idx1, 0) < len(rel(steps, 0)). The error remains the same:

[info] Error at: </..../exercises/relissues8.go:31:18> Assignment might fail.
[info] Permission to steps[idx1] might not suffice.

I think the issue is that execution 1 doesn't get the permission to execute execution 0's bound:

  if (p2_1) {
    inhale TStar2_V2_0 == 0
    TStar2_V2_0 := (ShArrayloc((sarray(steps_V1): ShArray[Ref]), sadd((soffset(steps_V1): Int),
      idx1_V1_0)): Ref).Intuint64$$$$_E_$$$$_p
  }

But maybe I’m missing something, or my interpretation of SIF encoding is wrong. Feel free to let me know whether I’m right or not :)