Implementation proof for a pointer to a type fails when a predicate for the type exists

[Dspil]

The code below does not verify throwing a "Permission to ia.Mem() might not suffice." error. When the predicate for just IA is removed it verifies.

package test

// type
type IA uint64

// interfaces
type TextUnmarshaler interface {
	pred Mem()
	
	preserves Mem() && acc(text)
	decreases
	UnmarshalText(text []byte) error
}

type Stringer interface {
	pred Mem()

	preserves acc(Mem())
	decreases
	String() string
}

// functions for implementation
preserves acc(ia)
preserves forall i int :: 0 <= i && i < len(text) ==> acc(&text[i])
decreases
func (ia *IA) UnmarshalText(text []byte) error

decreases
func (ia IA) String() string

// this is needed for the commented out implementation proof but it creates the problem
pred (ia IA) Mem() { true }


//IA implements Stringer {
//	
//	(ia IA) String() string {
//		return ia.String()
//	}
//}

pred (ia *IA) Mem() { acc(ia) }

(*IA) implements TextUnmarshaler {

	(ia *IA) UnmarshalText(text []byte) (err error) {
		// fails with 'Permission to ia.Mem() might not suffice.'
		unfold ia.Mem()
		err = ia.UnmarshalText(text)
		fold ia.Mem()
	}
}

[Felalolf]

That looks like an error in the member resolution since the type *IA has the member Mem twice. You can make the implementation proof by the aliasing feature. The tutorial should have the syntax or point to an example, but you can reasign the predicate in an implementation proof (so you define a predicate with a different name with true as body and then in the commented out implementation proof, you write something similar to Mem := NameOfYourPreviouslyDefinedPredicate).