Quantified predicate permission over freshly-allocated pointers fails injectivity check, even for provably-fresh allocations

[budney]

Summary

Maintaining a loop invariant of the form forall k :: ... ==> acc(P(buf[k])) over a slice being filled with freshly-allocated pointers (one new allocation per iteration, each carrying its own instance of a predicate P) fails with "Quantified resource ... might not be injective" — even though each buf[k] is populated by a fresh heap allocation from a separate call, which by ordinary Go/Gobra semantics can never alias any pointer already stored in the slice.

This looks like a completeness gap in how Gobra derives quantified-permission injectivity across loop iterations: it doesn't use the fact that a freshly-returned pointer from a function call cannot alias anything the caller already holds permission to.

Minimal reproduction

Gobra 1.1-SNAPSHOT (b4cdf753).

package reproducer

type Box struct {
	V int
}

//@ pred BoxMem(b *Box) {
//@ 	acc(b)
//@ }

//@ ensures b != nil
//@ ensures acc(BoxMem(b))
func newBox(v int) (b *Box) {
	b = &Box{V: v}
	//@ fold acc(BoxMem(b))
	return b
}

//@ requires n >= 0
func buildBoxes(n int) (result []*Box) {
	buf := make([]*Box, n)
	j := 0
	//@ invariant forall k int :: {&buf[k]} 0 <= k && k < len(buf) ==> acc(&buf[k], 1) && (k < j ==> (buf[k] != nil && acc(BoxMem(buf[k]))))
	//@ invariant len(buf) == n
	//@ invariant 0 <= j && j <= n
	for j < n {
		b := newBox(j)
		buf[j] = b
		j++
	}
	result = buf
	return result
}

Output:

Error at: <reproducer.go:30:12> Loop invariant might not be preserved.
Quantified resource acc(BoxMem(buf[k])) might not be injective.

What was tried

• Explicit pairwise-distinctness invariant (forall k1, k2 int :: {buf[k1], buf[k2]} 0 <= k1 && k1 < j && 0 <= k2 && k2 < j && k1 != k2 ==> buf[k1] != buf[k2]) — hits a separate well-formedness failure ("Permission to buf[k1] might not suffice"): a two-free-variable quantifier can't share the read permission granted by the single-variable quantifier above it, since each invariant clause's own body needs self-contained permission to be well-formed. Splitting it out this way doesn't resolve the underlying issue either way.
• Single-pointer freshness inhale (workaround that does work): adding one narrowly-scoped ghost statement right after each allocation —

  //@ inhale forall k int :: {&buf[k]} 0 <= k && k < j ==> b != buf[k]

  — before the assignment buf[j] = b lets the loop invariant verify. This is true by ordinary fresh-allocation semantics, but has to be assumed rather than derived; a caller who forgets it (or gets the bound wrong) gets no help from the verifier distinguishing "this is trivially true" from "this needs justification."

Why this matters

This is not an isolated one-off: it reproduces identically for any predicate-carrying type built via a per-iteration allocation into a growing/pre-sized slice — a very common construction pattern (see the "13-constructor injectivity investigation" noted below, and a second, independent reproduction encountered separately while restructuring an append-based accumulation loop into an index-assignment loop). Both cases needed the same single-pointer inhale workaround, suggesting this gap is hit routinely by idiomatic slice-building code, not just adversarial examples.

A related, likely-connected observation: the same injectivity requirement blocks ordinary multi-element calls into constructors whose own precondition contains a quantified mem()/predicate permission over a parameter slice — e.g. NewSeqn([]Stmt{a, b}, info) fails injectivity even when a and b are two genuinely distinct pointers from two separate, unaliased allocations, for the identical reason: Gobra has no way to relate a's freshness to b's postcondition without an explicit hint.

Environment

• Gobra 1.1-SNAPSHOT, commit b4cdf753
• Backend: Silicon (Z3 4.8.7+)