Using `rel(t,0) < rel(t,1)` with implication in SIF mode causes an error.

[AkasakaJelos]

Consider the following example:

package exercises

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

// @ requires rel(t,0) != rel(t,1)
func test_ghostIfandImplication(t uint64) {

    //@ assume rel(t,0) < rel(t,1)

    //Let's do logic table!

    //@ assert rel(t,0) < rel(t,1) ==> true     //T ==> T
    //@ refute rel(t,0) < rel(t,1) ==> false     //T ==> F
    //@ assert rel(t,0) > rel(t,1) ==> true     //F ==> T
    //@ assert rel(t,0) > rel(t,1) ==> false     //F ==> F
}

The program should verify, based on the logic truth table of implication. However, the truth is:

[info] Error at: </.../relissue12.go:15:2> Assert might fail.
[info] Assertion rel(t,0) > rel(t,1) ==> false might not hold.
[info] Gobra found 1 error.

If we dig into the SIF encoding, we have in the last assert:

 assert (p1 ==> p1 && p2 ==> t_V0_CN0 > t_V0_CN0_0) && (p2 ==> true) ==>
      (p1 ==> false) && (p2 ==> false)

If we set p1 to T and p2 to F, we end up with T ==> F (if we do with p2 == F, we get the same implication), which means we won't verify the stuff regardless of p2. According to Linard, the issue lies in the semantics of //@ assert rel(t,0) > rel(t,1) ==> false , which are completely unclear if we have only a single execution.

Changing it to:

//@ assert !(rel(t,0) > rel(t,1)) || false //F ==> F

will verify the statement, nevertheless.

[ArquintL]

The encoding shows it nicely that the LHS is trivially satisfied if one of the two executions is inactive (i.e. !p1 or !p2 holds).
Thus, if we restrict us to the cases in which both executions are active, we obtain the expected behavior (obviously, lowContext() could also be made a precondition instead):

package exercises

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

// @ requires rel(t,0) < rel(t,1)
func test_ghostIfandImplication(t uint64) {
    //@ refute rel(t,0) < rel(t,1) ==> false     				//T ==> F
    //@ assert lowContext() && rel(t,0) > rel(t,1) ==> false	//F ==> F
}

[ArquintL]

Thus, I feel like this issue is more about what are the expected semantics of SIF expressions in contexts where only one of the two executions is active. Given that Gobra simply adopts the same semantics as the SIF plugin there's not much we can do and I'm convinced there were strong reasons for going with this design.
From the top of my head, the semantics that this issue requests would make it annoying to state pre- and postconditions for methods that are called in non-low-context as one would have to state each relational precondition as an implication with lowContext() as its LHS. Instead, Viper decided to go with relational expressions that evaluate to true in non-low-context and one can use a single lowContext() precondition to state that such non-low-contexts are not permitted