Unintuitive semantics for mixed non-hyper-predicates and hyper-predicates

[felixlinker]

Hi everyone,

I just tried proving some property using gobra's hypermode, and I'm pretty sure I found a soundness bug. The following code verifies successfully when using gobra at version bc3c90375d672dbc796edb7011b70bc9098eeb21.

// @ requires acc(arr)
// @ ensures !contains && low(t) ==> low(contains)
func Includes(t int, arr []int) (contains bool) {
	contains = false
	// @ invariant acc(arr)
	// @ invariant 0 <= idx && idx <= len(arr)
	// @ invariant !contains && low(t) ==> low(contains)
	for idx := 0; idx < len(arr); idx++ {
		if arr[idx] == t {
			contains = true
		}
	}

	return contains
}

Intuitively, the post-condition specifies that: if two executions are called with the same element t, and t is not included in one array, then t is not included in either array. Clearly, that's not the case.

For example, the following two calls satisfy the left-hand side of the implication, but not the right-hand side:

• Includes(0, []int{1}) // == false
• Includes(0, []int{0}) // == true

I hope I didn't make a mistake in parsing the post-condition! Let me know, if I did.

[felixlinker]

PS: I wrote test cases confirming that the two calls I listed as counter examples indeed return false and true respectively.

[jcp19]

Which mode gives you this behaviour? Extended mode or hyperMode=on?

[ArquintL]

Which mode gives you this behaviour? Extended mode or hyperMode=on?

With 99% certainty, @felixlinker is using --hyperMode extended

[ArquintL]

I can reproduce that the example verifies, and looking at the encoding, Gobra proves the following postcondition:

  ensures (p1 ==> !contains_V0) && (p2 ==> !contains_V0_0) &&
    (p1 && p2 ==> t_V0 == t_V0_0) ==>
    p1 && p2 ==> contains_V0 == contains_V0_0

The encoding translates

• !contains to p1 ==> !contains_V0 and p2 ==> !contains_V0_0
• low(t) to p1 && p2 ==> t_V0 == t_V0_0, and
• low(contains) to p1 && p2 ==> contains_V0 == contains_V0_0

Solely based on the encoding, the postcondition is trivial: prove contains_V0 == contains_V0_0 assuming p1 && p2. The first line of the encoding tells us that in this case !contains_V0 and ! contains_V0_0 holds, which concludes the proof.

---

This encoding, thus, does not express

if two executions are called with the same element t, and t is not included in one array, then t is not included in either array. Clearly, that's not the case.

So, I see the following questions: (1) what would be the postcondition matching the stated property and (2) are the currently used semantics of hyper assertions intuitive?

1. What would be the postcondition matching the stated property

On the level of the encoding, I'd argue this postcondition captures the property in prose:

ensures (p1 && p2) && 
          (!contains_V0 || !contains_V0_0) &&
          (t_V0 == t_V0_0) ==>
            contains_V0 == contains_V0_0

I.e., if both executions are active (line 1), at least one execution does not contain t (line 2), t is the same in both executions (line 3) then contains must be the same in the both executions (line 4), which should not hold for the program above.
This encoding of the postcondition corresponds to the following hyper-postcondition:

ensures (rel(!contains, 0) || rel(!contains, 1)) && low(t) ==> low(contains)

Indeed, verifying the following program fails as the 2nd postcondition does not hold:

package issue996

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

// @ requires acc(arr)
// @ ensures !contains && low(t) ==> low(contains) // holds
// @ ensures  (rel(!contains, 0) || rel(!contains, 1)) && low(t) ==> low(contains) // does not hold
func Includes(t int, arr []int) (contains bool) {
	contains = false
	// @ invariant acc(arr)
	// @ invariant 0 <= idx && idx <= len(arr)
	// @ invariant !contains && low(t) ==> low(contains)
	for idx := 0; idx < len(arr); idx++ {
		if arr[idx] == t {
			contains = true
		}
	}

	return contains
}

2. Are the currently used semantics of hyper assertions intuitive?

Similar to Felix, my own intuition (which might not be entirely independent though) is also that !contains && low(t) ==> low(contains) is not equivalent to true, such that I don't spot the issue just by looking at this issue without consulting the encoding. "Back-translating" the encoding, I'd have expected that the verified property rather corresponds to !contains && low(!contains) && low(t) ==> low(contains), with the intuitive for me that if an execution ends in !contains and the second execution does so too, then the RHS holds (which would be trivial for this example as the RHS is simply low(contains)).

From my point of view, I'm wondering about:

• Are the current semantics those that we want?
• How do we help new users (but also ourselves) to have the right intuition? It seems like my intuition is just off and the only way to understand the encoding currently seems to consider how each conjunction would be encoded

[felixlinker]

To me, the issue seems to stem from the translation of !contains. I would have expected that this is translated to two post-conditions, not one that captures both executions.

Or equivalently, I would have expected that the property is translated to the following:

ensures ((p1 ==> !contains_V0) && (p1 && p2 ==> t_V0 == t_V0_0) ==> p1 && p2 ==> contains_V0 == contains_V0_0)
  && ((p2 ==> !contains_V0_0) && (p1 && p2 ==> t_V0 == t_V0_0) ==> p1 && p2 ==> contains_V0 == contains_V0_0)

[felixlinker]

Maybe more simple, the conjunction seems the issue. Shouldn't there be a disjunction between (p1 ==> !contains_V0) && (p2 ==> !contains_V0_0)?

[ArquintL]

I agree that this would also match my intuition for such a postcondition that mixes unary properties (like !contains) and hyper properties (like low(t) and low(contains)).
Ideally, we don't special case the encoding of a property that mixes unary and hyper properties as this would make the story even more complicated. Thinking about the encoding of a unary property like !contains, I believe the currently used conjunction makes most sense as you want to say that this is a property that holds for all program executions and, thus, also for the first and second execution

[felixlinker]

Not sure. I totally see the implementation issue, but we want the implication to be true for both executions, not the left-hand side. If there are two executions, the implication forces the left-hand side to be true or false in both cases. I don't know the formal semantics, but this does not seem right.

[felixlinker]

@ArquintL Maybe a different idea that requires no special casing. Why not compile each post-condition for p1 and p2? That would be the genreal approach. Afterwards you can do some deduplication on the syntactic level.

[felixlinker]

After further discussion with Linard (who forwarded discussions with Marco), I learned that "unary-statements" (such as !contains) mixed with low-statements are always assumed to apply to both executions, which makes my example indeed sound.