Fix type errors introduced by the latest version of Gobra (#241)

* backup

* add missing termination measures

* fix type error

pkg/addr/host_spec.gobra

@@ -48,7 +48,9 @@ pred (h *HostSVC) Mem() { acc(h) }
 
 (*HostSVC) implements HostAddr
 
-ghost pure func isValidHostAddrType(htype HostAddrType) bool {
+ghost
+decreases
+pure func isValidHostAddrType(htype HostAddrType) bool {
 	return htype == HostTypeNone ||
 		htype == HostTypeIPv4 ||
 		htype == HostTypeIPv6 ||
@@ -61,6 +63,7 @@ ensures htype == HostTypeNone ==> res == HostLenNone
 ensures htype == HostTypeIPv4 ==> res == HostLenIPv4
 ensures htype == HostTypeIPv6 ==> res == HostLenIPv6
 ensures htype == HostTypeSVC ==> res == HostLenSVC
+decreases
 pure func sizeOfHostAddrType(htype HostAddrType) (res int) {
 	return htype == HostTypeNone ?
 		HostLenNone : htype == HostTypeIPv4 ?

pkg/slayers/path/epic/epic_spec.gobra

@@ -100,6 +100,7 @@ func (p *Path) hasScionPath(buf []byte) (r bool) {
 
 ghost
 requires acc(p.Mem(buf), _)
+decreases
 pure func (p *Path) GetUnderlyingScionPathBuf(buf []byte) []byte {
 	return unfolding acc(p.Mem(buf), _) in buf[MetadataLen:]
 }

pkg/slayers/path/path_spec.gobra

@@ -54,20 +54,23 @@ ghost
 requires 0 <= t && t < maxPathType
 requires acc(PathPackageMem(), _)
 ensures  res == unfolding acc(PathPackageMem(), _) in registeredPaths[t].inUse
+decreases
 pure func Registered(t Type) (res bool) {
 	return unfolding acc(PathPackageMem(), _) in registeredPaths[t].inUse
 }
 
 ghost
 requires 0 <= t && t < maxPathType
 requires acc(PathPackageMem(), _)
+decreases
 pure func GetType(t Type) (res Metadata) {
 	return unfolding acc(PathPackageMem(), _) in registeredPaths[t].Metadata
 }
 
 ghost
 requires acc(PathPackageMem(), _)
 ensures  b == unfolding acc(PathPackageMem(), _) in strictDecoding
+decreases
 pure func IsStrictDecoding() (b bool) {
 	return unfolding acc(PathPackageMem(), _) in strictDecoding
 }

router/dataplane_concurrency_model.gobra

@@ -37,6 +37,7 @@ pred SharedInv(ghost dp io.DataPlaneSpec, ghost y SharedArg) {
 ghost 
 requires io.token(p) && dp.dp3s_iospec_ordered(s, p)
 ensures  m.LockP() && m.LockInv() == SharedInv!< dp, y !>;
+decreases
 func InitSharedInv(
   ghost dp io.DataPlaneSpec, 
   ghost p io.Place, 

verification/dependencies/crypto/rand/util.gobra

@@ -26,4 +26,5 @@ ensures acc(max.Mem(), R13)
 ensures err != nil ==> err.ErrorMem()
 ensures err == nil ==> n.Mem()
 ensures err == nil ==> n.toInt() >= 0 && n.toInt() < max.toInt()
+decreases _
 func Int(rand io.Reader, max *big.Int) (n *big.Int, err error)

verification/dependencies/crypto/subtle/constant_time.gobra

@@ -20,5 +20,5 @@ requires acc(slices.AbsSlice_Bytes(y, 0, len(y)), _)
 // ensures unfolding slices.AbsSlice_Bytes(x, 0, len(x)) in (unfolding slices.AbsSlice_Bytes(y, 0, len(y)) in len(x) == len(y) ==> (forall i int :: 0 <= i && i < len(x) ==> x[i] == y[i]) ==> res == 1)
 // ensures unfolding slices.AbsSlice_Bytes(x, 0, len(x)) in (unfolding slices.AbsSlice_Bytes(y, 0, len(y)) in len(x) == len(y) ==> !(forall i int :: 0 <= i && i < len(x) ==> x[i] == y[i]) ==> res == 0)
 ensures len(x) != len(y) ==> res == 0
-decreases
+decreases _
 pure func ConstantTimeCompare(x, y []byte) (res int)

verification/dependencies/golang.org/x/net/internal/socket/socket.gobra

@@ -58,12 +58,14 @@ pred (m *Message) MemWithoutHalf(lenBuffers int) {
 
 ghost
 requires acc(m.Mem(lenBuffers), _)
+decreases
 pure func (m *Message) GetAddr(lenBuffers int) net.Addr {
 	return unfolding acc(m.Mem(lenBuffers), _) in m.Addr
 }
 
 ghost
 requires acc(m.MemWithoutHalf(lenBuffers), _)
+decreases
 pure func (m *Message) GetAddrWithoutHalf(lenBuffers int) net.Addr {
 	return unfolding acc(m.MemWithoutHalf(lenBuffers), _) in m.Addr
 }

verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra

@@ -117,6 +117,7 @@ func NewPacketConn(c net.PacketConn) (p *PacketConn) {
 
 ghost
 requires acc(p.Mem(), _)
+decreases _
 pure func (p *PacketConn) GetUnderlyingConn() (c net.PacketConn)
 
 ghost

verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra

@@ -139,6 +139,7 @@ func NewPacketConn(c net.PacketConn) (p *PacketConn) {
 
 ghost
 requires acc(p.Mem(), _)
+decreases _
 pure func (p *PacketConn) GetUnderlyingConn() (c net.PacketConn)
 
 ghost

verification/dependencies/strings/strings.gobra

@@ -91,18 +91,21 @@ ensures len(elems) == 0 ==> res == ""
 ensures len(elems) == 1 ==> res == elems[0]
 // (joao) Leads to precondition of call might not hold (permission to elems[i] might not suffice)
 // ensures len(elems) > 1 ==> res == elems[0] + sep + Join(elems[1:], sep)
+decreases _
 pure func Join(elems []string, sep string) (res string)
 
 // HasPrefix tests whether the string s begins with prefix.
 pure
 ensures ret == (len(s) >= len(prefix) && s[0:len(prefix)] == prefix)
+decreases
 func HasPrefix(s, prefix string) (ret bool) {
 	return len(s) >= len(prefix) && (s[0:len(prefix)] == prefix)
 }
 
 // HasSuffix tests whether the string s ends with suffix.
 pure
 ensures ret == (len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix)
+decreases
 func HasSuffix(s, suffix string) (ret bool) {
 	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
 }

verification/dependencies/sync/mutex.gobra

@@ -16,6 +16,7 @@ pred (m *Mutex) UnlockP()
 
 ghost
 requires acc(m.LockP(), _)
+decreases _
 pure func (m *Mutex) LockInv() pred()
 
 ghost

verification/dependencies/sync/waitgroup.gobra

@@ -20,6 +20,7 @@ pred (wg *WaitGroup) Token(t pred())
 
 ghost
 requires acc(g.WaitGroupP(), _)
+decreases _
 pure func (g *WaitGroup) WaitMode() bool
 
 ghost
@@ -31,14 +32,15 @@ func (g *WaitGroup) Init()
 ghost
 requires g.WaitGroupP()
 ensures g.WaitGroupP() && !g.WaitMode()
+decreases _
 func (g *WaitGroup) UnsetWaitMode()
 
 ghost
 requires p > 0
 requires acc(g.WaitGroupP(), p)
 requires !g.WaitMode() && g.UnitDebt(P)
 ensures g.UnitDebt(P) && acc(g.WaitGroupStarted(), p)
-decreases
+decreases _
 func (g *WaitGroup) Start(ghost p perm, ghost P pred())
 
 ghost
@@ -48,7 +50,7 @@ requires p + q == 1
 requires acc(g.WaitGroupP(), p)
 requires acc(g.WaitGroupStarted(), q)
 ensures g.WaitGroupP() && g.WaitMode()
-decreases
+decreases _
 func (g *WaitGroup) SetWaitMode(ghost p perm, ghost q perm)
 
 // Simplified version of the debt redistribution rule. The most general version cannot be written in Gobra
@@ -57,20 +59,21 @@ func (g *WaitGroup) SetWaitMode(ghost p perm, ghost q perm)
 ghost
 requires P() && g.UnitDebt(P)
 ensures g.UnitDebt(PredTrue!<!>)
-decreases
+decreases _
 func (g *WaitGroup) PayDebt(ghost P pred())
 
 // Simplified version of the debt redistribution rule, instantiated with P == { PredTrue!<!> } and Q == { R }.
 // This is the only rule that generates a Token.
 ghost
 requires g.UnitDebt(PredTrue!<!>)
 ensures g.UnitDebt(R) && g.Token(R)
-decreases
+decreases _
 func (g *WaitGroup) GenerateTokenAndDebt(ghost R pred())
 
 ghost
 requires R()
 ensures g.Token(R)
+decreases _
 func (g *WaitGroup) GenerateToken(ghost R pred())
 
 // Simplified version of Add as proposed in page 8 of Martin's latest document (as of 21/01/2021)
@@ -83,11 +86,11 @@ ensures (n > 0 && p == 0) ==> g.UnitDebt(P)
 ensures n > 0 ==> acc(g.UnitDebt(PredTrue!<!>), n/1)
 // this is actually necessary, otherwise Gobra cannot prove that Add does not modify the wait mode
 ensures (n > 0 && p > 0) ==> g.WaitMode() == old(g.WaitMode())
-decreases
+decreases _
 func (g *WaitGroup) Add(n int, ghost p perm, ghost P pred())
 
 requires g.UnitDebt(PredTrue!<!>)
-decreases
+decreases _
 func (g *WaitGroup) Done()
 
 requires p > 0
@@ -120,6 +123,7 @@ requires len(Q) == len(permsQ)
 requires g.UnitDebt(CollectFractions!<P ++ Q, permsP ++ permsQ!>)
 requires g.UnitDebt(PredTrue!<!>)
 ensures g.UnitDebt(CollectFractions!<P, permsP!>) && g.UnitDebt(CollectFractions!<Q, permsQ!>)
+decreases _
 func (g *WaitGroup) SplitSequence(ghost P seq[pred()], ghost Q seq[pred()], ghost permsP seq[perm], ghost permsQ seq[perm])
 
 // Special case of the debt redistribution rule
@@ -134,4 +138,5 @@ requires g.UnitDebt(PredTrue!<!>)
 requires forall i int :: 0 <= i && i < len(P) ==> permsP[i] + permsQ[i] == permsR[i]
 ensures g.UnitDebt(CollectFractions!<P, permsP!>)
 ensures g.UnitDebt(CollectFractions!<P, permsQ!>)
+decreases _
 func (g *WaitGroup) SplitFractions(ghost P seq[pred()], ghost permsP seq[perm], ghost permsQ seq[perm], ghost permsR seq[perm])

verification/utils/definitions/definitions.gobra

@@ -81,10 +81,12 @@ const (
 // from the router.
 ghost
 requires false
-func Unreachable()
+decreases
+func Unreachable() {}
 
 ghost
 ensures !res
+decreases
 pure func Uncallable() (res bool) {
 	return false
 }

verification/utils/seqs/seqs.gobra

@@ -28,12 +28,12 @@ ghost
 requires size >= 0
 ensures len(res) == size
 ensures forall i int :: { res[i] } 0 <= i && i < size ==> res[i] == byte(0)
-decreases
+decreases _
 pure func NewSeqByte(size int) (res seq[byte])
 
 ghost
 requires size >= 0
 ensures len(res) == size
 ensures forall i int :: { res[i] } 0 <= i && i < size ==> res[i] == nil
-decreases
+decreases _
 pure func NewSeqByteSlice(size int) (res seq[[]byte])

verification/utils/slices/slices.gobra

@@ -156,6 +156,7 @@ ghost
 requires size >= 0
 ensures len(res) == size
 ensures forall i int :: { res[i] } 0 <= i && i < size ==> res[i] == nil
+decreases _
 pure func NewSeq_Any(size int) (res seq[any])
 
 // TODO: