Failure in proving subtyping on recursive error implementations

[jcp19]

TODO: elaborate

package p

type scmpError struct {
	TypeCode int
	Cause    error
}

preserves e.ErrorMem()
ensures   e.Size() == old(e.Size())
decreases e.Size()
func (e scmpError) Error() string /*{
	unfold e.ErrorMem()
	defer fold e.ErrorMem()
	res := newErr(e)
    assume res.Size() == 1 + e.Cause.Size()
	return res.Error()
}*/

preserves e != nil && e.ErrorMem()
ensures   res != nil && res.ErrorMem()
ensures   e.Size() == old(e.Size())
ensures   res.Size() == 1 + e.Size()
decreases _
func newErr(e error) (res error)

pred (err scmpError) ErrorMem() {
	err.Cause != nil ==> err.Cause.ErrorMem()
}

ghost
pure
requires  acc(err.ErrorMem(), _)
decreases err.Size()
func (err scmpError) IsDuplicableMem() bool {
	return unfolding acc(err.ErrorMem(), _) in
		err.Cause == nil || err.Cause.IsDuplicableMem()
}

ghost
preserves err.ErrorMem()
ensures   err.IsDuplicableMem() ==> err.ErrorMem()
ensures   err.Size() == old(err.Size())
decreases err.Size()
func (err scmpError) Duplicate() /*{
	if err.IsDuplicableMem() {
		unfold err.ErrorMem()
        if err.Cause != nil {
            assert err.Cause.ErrorMem()
            assert err.Cause.IsDuplicableMem()
		    err.Cause.Duplicate()
		    assert err.Cause.ErrorMem() && err.Cause.ErrorMem()
        }
		fold err.ErrorMem()
		fold err.ErrorMem()
	}
}*/

ghost
requires acc(e.ErrorMem(), _)
ensures  0 < res
pure func (e scmpError) Size() (res int) {
	return 2 + (unfolding acc(e.ErrorMem(), _) in
        e.Cause == nil ?
            0 : 
		    (let _ := Asserting(0 <= e.Cause.Size()) in e.Cause.Size()))
}

ghost
pure
requires b
decreases _
func Asserting(b bool) bool

scmpError implements error