Pure interface method's definitional axiom does not fire through interface dispatch when the method recurses through another interface-typed call

[budney]

Summary

A pure ghost interface method's auto-generated definitional axiom does not fire through interface dispatch when the method's own body recurses through another interface-typed pure call — even though the concrete dispatch on the exact same object verifies fine, and even though a non-recursive interface method verifies fine through interface dispatch.

The underlying claim being asserted is a tautology (comparing a value to itself, reached via two different static types — interface vs. concrete — for the same runtime object), so this looks like a soundness/completeness gap in axiom instantiation rather than a real logic error.

Minimal reproduction

Gobra 1.1-SNAPSHOT (b4cdf753).

package reproducer

type RNode interface {
	//@ pred mem()

	//@ ghost
	//@ pure
	//@ requires mem()
	//@ RContainsCall(target string) bool
}

type RLeaf struct {
	Target string
}

//@ pred (n *RLeaf) mem() {
//@ 	acc(n, 1/2)
//@ }

//@ ghost
//@ pure
//@ requires n.mem()
//@ decreases _
//@ func (n *RLeaf) RContainsCall(target string) bool {
//@ 	return unfolding n.mem() in n.Target == target
//@ }

type RBranch struct {
	A RNode
}

//@ pred (n *RBranch) mem() {
//@ 	acc(n, 1/2) &&
//@ 	(n.A != nil ==> n.A.mem())
//@ }

//@ ghost
//@ pure
//@ requires n.mem()
//@ decreases _
//@ func (n *RBranch) RContainsCall(target string) bool {
//@ 	return unfolding n.mem() in (n.A != nil && n.A.RContainsCall(target))
//@ }

// checkLeaf: non-recursive RContainsCall. Interface-dispatched call equals
// concrete-dispatched call on the same object -- VERIFIES.
//@ requires n != nil ==> n.mem()
//@ ensures  n != nil ==> n.mem()
func checkLeaf(n RNode, target string) {
	if lf, ok := n.(*RLeaf); ok {
		_ = lf
		//@ assert n.RContainsCall(target) == lf.RContainsCall(target)
	}
}

// checkBranch: recursive RContainsCall (calls RContainsCall on the
// interface-typed field n.A). The concrete-dispatch fact verifies fine, but
// the identical equality through the interface-dispatched call FAILS, even
// though br IS n (same object, narrowed by a type assertion immediately
// above), and even with the right-hand side written out by hand (bypassing
// any auto-generated axiom on that side entirely).
//@ requires n != nil ==> n.mem()
//@ ensures  n != nil ==> n.mem()
func checkBranch(n RNode, target string) {
	if br, ok := n.(*RBranch); ok {
		_ = br
		//@ assert br.RContainsCall(target) == (unfolding br.mem() in (br.A != nil && br.A.RContainsCall(target)))
		// verifies

		//@ assert n.RContainsCall(target) == (unfolding n.mem() in (br.A != nil && br.A.RContainsCall(target)))
		// FAILS: "Assertion ... might not hold"
	}
}

Output:

Error at: <reproducer.go:76:3> Assert might fail.
Assertion n.RContainsCall(target) == (unfolding n.mem() in (br.A != nil && br.A.RContainsCall(target))) might not hold.

Isolation matrix

Verified with four variants of checkBranch's assertion (extracted from a wider probe, iface_recursive.go, in a downstream project's test suite):

Assertion	Result
n.RContainsCall(t) == lf.RContainsCall(t) (non-recursive RLeaf)	verifies
n.RContainsCall(t) == br2.RContainsCall(t) (recursive, but the child field is concretely typed *RLeaf, not an interface)	verifies
br.RContainsCall(t) == (unfolding br.mem() in ...) (recursive, interface-typed child field, but compared via the concrete dispatch br)	verifies
n.RContainsCall(t) == (unfolding n.mem() in ...) (recursive, interface-typed child field, compared via the interface dispatch n, where n and br are the same object)	fails

So the gap is specific to the intersection of: (a) the call is made through the interface-typed reference, and (b) the method's own body contains a further interface-typed pure method call. Recursion alone doesn't trigger it (row 2), and interface dispatch alone doesn't trigger it (row 1 and 3).

I also tried wrapping the equality in a standalone lemma function with br/target as explicit parameters (forcing it to be proven once as a generic-instance obligation, rather than an inline assert) — it fails identically, since proving the lemma's own postcondition requires exactly the same interface-dispatch axiom instantiation.

Why this matters

This blocks a class of proofs where a recursive traversal over a Node-shaped interface hierarchy needs to relate an interface-dispatched call (the natural way to state a general postcondition, e.g. on a function parameter typed as the interface) back to what's actually known at a call site after a type-switch/assertion narrows to a concrete type. The workaround space I found (assert vs. lemma, switch vs. explicit assertion, manual RHS vs. opaque call) is exhausted as far as I can tell — nothing routes around it from the call site.

Happy to provide more context or a smaller/larger reproduction if useful.