Adapt to stricter type-checker comming soon in Gobra

pkg/addr/fmt.go

@@ -119,9 +119,6 @@ func fmtAS(as_ AS, sep string) string {
 	}
 	// Format BGP ASes as decimal
 	if as_ <= MaxBGPAS {
-		// (VerifiedSCION) the following property is guaranteed by the type system,
-		// but Gobra cannot infer it yet
-		// @ assume 0 <= as_
 		return strconv.FormatUint(uint64(as_), 10)
 	}
 	// Format all other ASes as 'sep'-separated hex.
@@ -131,16 +128,14 @@ func fmtAS(as_ AS, sep string) string {
 	var b /*@@@*/ strings.Builder
 	// @ b.ZeroBuilderIsReadyToUse()
 	b.Grow(maxLen)
+	// @ invariant 0 <= i && i <= asParts
 	// @ invariant b.Mem()
 	// @ decreases asParts - i
 	for i := 0; i < asParts; i++ {
 		if i > 0 {
 			b.WriteString(sep)
 		}
 		shift := uint(asPartBits * (asParts - i - 1))
-		// (VerifiedSCION) the following property is guaranteed by the type system,
-		// but Gobra cannot infer it yet
-		// @ assume 0 <= uint64(as_>>shift)&asPartMask
 		b.WriteString(strconv.FormatUint(uint64(as_>>shift)&asPartMask, asPartBase))
 	}
 	return b.String()

pkg/addr/host.go

@@ -34,6 +34,7 @@ import (
 	"strings"
 
 	"github.com/scionproto/scion/pkg/private/serrors"
+	//@ "math"
 	//@ . "github.com/scionproto/scion/verification/utils/definitions"
 	//@ sl "github.com/scionproto/scion/verification/utils/slices"
 )
@@ -358,7 +359,10 @@ func (h HostSVC) Pack() (res []byte) {
 	return out
 }
 
-// @ requires pad >= 0
+// (VerifiedSCION) the upper bound on 'pad' is needed under the sound bounded-integer
+// semantics: without it, 'HostLenSVC + pad' may overflow and the length passed to 'make'
+// is then not known to be non-negative.
+// @ requires 0 <= pad && pad <= math.MaxInt64 - HostLenSVC
 // @ ensures acc(res)
 // @ decreases
 func (h HostSVC) PackWithPad(pad int) (res []byte) {

pkg/addr/isdas.go

@@ -127,7 +127,7 @@ func asParseBGP(s string) (retAs AS, retErr error) {
 	// @ strconv.Exp2to10(30)
 	// @ strconv.Exp2to10(20)
 	// @ strconv.Exp2to10(10)
-	// @ assert _as < uint64(strconv.Exp(2, BGPASBits))
+	// @ assert integer(_as) < strconv.Exp(2, BGPASBits)
 	return AS(_as), nil
 }
 

pkg/slayers/path/scion/info_hop_setter_lemmas.gobra

@@ -102,7 +102,7 @@ pure func HopfieldsByteSlice(raw []byte, currInfIdx int, segs io.SegLens) ([]byt
 
 // SliceBytesIntoSegments splits the raw bytes of a packet into its hopfield segments
 ghost
-requires 0 < p
+requires noPerm < p
 requires segs.Valid()
 requires PktLen(segs, MetaLen) <= len(raw)
 requires acc(sl.Bytes(raw, 0, len(raw)), p)
@@ -126,7 +126,7 @@ func SliceBytesIntoSegments(raw []byte, segs io.SegLens, p perm) {
 
 // CombineBytesFromSegments combines the three hopfield segments of a packet into a single slice of bytes.
 ghost
-requires 0 < p
+requires noPerm < p
 requires segs.Valid()
 requires PktLen(segs, MetaLen) <= len(raw)
 requires acc(sl.Bytes(raw[:HopfieldsStartIdx(0, segs)], 0, HopfieldsStartIdx(0, segs)), p)
@@ -150,7 +150,7 @@ func CombineBytesFromSegments(raw []byte, segs io.SegLens, p perm) {
 
 // SliceBytesIntoInfoFields splits the raw bytes of a packet into its infofields
 ghost
-requires 0 < p
+requires noPerm < p
 requires segs.Valid()
 requires MetaLen + numInf * path.InfoLen <= len(raw)
 requires numInf == segs.NumInfoFields()
@@ -182,7 +182,7 @@ func SliceBytesIntoInfoFields(raw []byte, numInf int, segs io.SegLens, p perm) {
 
 // CombineBytesFromInfoFields combines the infofields of a packet into a single slice of bytes.
 ghost
-requires 0 < p
+requires noPerm < p
 requires segs.Valid()
 requires MetaLen + numInf * path.InfoLen <= len(raw)
 requires numInf == segs.NumInfoFields()
@@ -623,7 +623,7 @@ func EstablishBytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf
 // to the subslice containing all past hopfields, to the sublice containing the current hopfield,
 // and to another containing all future hopfields.
 ghost
-requires 0 < p
+requires noPerm < p
 requires 0 <= currHfIdx && currHfIdx < segLen
 requires segLen * path.HopLen == len(hopfields)
 requires acc(sl.Bytes(hopfields, 0, len(hopfields)), p)
@@ -647,7 +647,7 @@ func SplitHopfields(hopfields []byte, currHfIdx int, segLen int, p perm) {
 // current hopfield, and future hopfields of a segment into a single permission to the slice
 // containing all hopfields of that segment.
 ghost
-requires 0 < p
+requires noPerm < p
 requires 0 <= currHfIdx && currHfIdx < segLen
 requires segLen * path.HopLen == len(hopfields)
 requires let currHfStart := currHfIdx * path.HopLen in

pkg/slayers/scion_spec.gobra

@@ -332,7 +332,7 @@ pure func (s *SCION) PathScionEndIdx(ub []byte) int {
 }
 
 ghost
-requires  0 < p
+requires  noPerm < p
 preserves acc(s.Mem(ub), p)
 ensures   let start := s.PathStartIdx(ub) in
 	let end := s.PathEndIdx(ub) in

router/dataplane.go

@@ -325,9 +325,9 @@ func (d *DataPlane) SetKey(key []byte) (res error) {
 	// @ unfold MutexInvariant{d}()
 	// @ assert !d.IsRunning()
 	// @ d.isRunningEq()
-	// @ unfold acc(d.Mem(), 1/2)
+	// @ unfold acc(d.Mem(), perm(1, 2))
 	// @ d.keyIsSetEq()
-	// @ unfold acc(d.Mem(), 1/2)
+	// @ unfold acc(d.Mem(), perm(1, 2))
 	// @ unfold macFactoryInv(d.macFactory, d.key)
 	// @ defer fold MutexInvariant{d}()
 	// @ defer fold d.Mem()
@@ -387,9 +387,9 @@ func (d *DataPlane) AddInternalInterface(conn BatchConn, ip net.IP) error {
 	// @ unfold MutexInvariant{d}()
 	// @ assert !d.IsRunning()
 	// @ d.isRunningEq()
-	// @ unfold acc(d.Mem(), 1/2)
+	// @ unfold acc(d.Mem(), perm(1, 2))
 	// @ d.internalIsSetEq()
-	// @ unfold acc(d.Mem(), 1/2)
+	// @ unfold acc(d.Mem(), perm(1, 2))
 	// @ unfold internalInv(d.internal)
 	// @ unfold internalIPInv(d.internalIP)
 	if d.running {
@@ -438,16 +438,16 @@ func (d *DataPlane) AddExternalInterface(ifID uint16, conn BatchConn) error {
 		// @ Unreachable()
 		return emptyValue
 	}
-	// @ ghost if d.external != nil { unfold acc(accBatchConn(d.external), 1/2) }
+	// @ ghost if d.external != nil { unfold acc(accBatchConn(d.external), perm(1, 2)) }
 	if _, existsB := d.external[ifID]; existsB {
 		// @ establishAlreadySet()
-		// @ ghost if d.external != nil { fold acc(accBatchConn(d.external), 1/2) }
+		// @ ghost if d.external != nil { fold acc(accBatchConn(d.external), perm(1, 2)) }
 		// @ fold externalInv(d.external)
 		// @ fold d.Mem()
 		// @ fold MutexInvariant{d}()
 		return serrors.WithCtx(alreadySet, "ifID", ifID)
 	}
-	// @ ghost if d.external != nil { fold acc(accBatchConn(d.external), 1/2) }
+	// @ ghost if d.external != nil { fold acc(accBatchConn(d.external), perm(1, 2)) }
 	if d.external == nil {
 		d.external = make(map[uint16]BatchConn)
 		// @ fold accBatchConn(d.external)

router/dataplane_spec.gobra

@@ -35,9 +35,9 @@ import (
 	sl "github.com/scionproto/scion/verification/utils/slices"
 )
 
-ghost const MutexPerm perm = 1/4
-ghost const OutMutexPerm perm = 3/4
-ghost const runningPerm perm = 1/2
+ghost const MutexPerm perm = perm(1, 4)
+ghost const OutMutexPerm perm = perm(3, 4)
+ghost const runningPerm perm = perm(1, 2)
 
 pred MutexInvariant(d *DataPlane) {
 	acc(&d.running, runningPerm) &&
@@ -67,7 +67,7 @@ pred (d *DataPlane) Mem() {
 	acc(&d.macFactory)                        &&
 	acc(&d.bfdSessions)                       &&
 	acc(&d.localIA)                           &&
-	acc(&d.running, 1/2)                      &&
+	acc(&d.running, perm(1, 2))                      &&
 	acc(&d.Metrics)                           &&
 	acc(&d.forwardingMetrics)                 &&
 	acc(&d.key)                               &&

verification/dependencies/crypto/cipher/cipher.gobra

@@ -94,7 +94,7 @@ type BlockMode interface {
 	// maintains state and does not reset at each CryptBlocks call.
 	requires  len(src) <= len(dst)
 	preserves Mem()
-	preserves acc(sl.Bytes(dst, 0, len(dst)), 1 - R10)
+	preserves acc(sl.Bytes(dst, 0, len(dst)), writePerm - R10)
 	preserves dst !== src ==> acc(sl.Bytes(dst, 0, len(dst)), R10)
 	preserves acc(sl.Bytes(src, 0, len(src)), R10)
 	ensures   BlockSize() == old(BlockSize())

verification/dependencies/github.com/google/gopacket/flows.gobra

@@ -29,13 +29,13 @@ type Flow struct {
 	src, dst   [MaxEndpointSize]byte
 }
 
-preserves acc(sl.Bytes(src, 0, len(src)), 1/10000) && acc(sl.Bytes(dst, 0, len(dst)), 1/10000)
+preserves acc(sl.Bytes(src, 0, len(src)), perm(1, 10000)) && acc(sl.Bytes(dst, 0, len(dst)), perm(1, 10000))
 requires len(src) <= MaxEndpointSize && len(dst) <= MaxEndpointSize
 ensures f.slen == len(src)
 ensures f.dlen == len(dst)
-ensures unfolding acc(sl.Bytes(src, 0, len(src)), 1/10000) in
+ensures unfolding acc(sl.Bytes(src, 0, len(src)), perm(1, 10000)) in
 	forall i int :: { &src[i] } 0 <= i && i < len(src) ==> f.src[i] == src[i]
-ensures unfolding acc(sl.Bytes(dst, 0, len(dst)), 1/10000) in
+ensures unfolding acc(sl.Bytes(dst, 0, len(dst)), perm(1, 10000)) in
 	forall i int :: { &dst[i] } 0 <= i && i < len(dst) ==> f.dst[i] == dst[i]
 ensures f.typ == t
 decreases

verification/dependencies/github.com/google/gopacket/layers/bfd.gobra

@@ -135,7 +135,7 @@ pred (b *BFDAuthHeader) Mem() {
 	acc(b) && sl.Bytes(b.Data, 0, len(b.Data))
 }
 
-preserves acc(h, 1/10000)
+preserves acc(h, perm(1, 10000))
 decreases
 func (h *BFDAuthHeader) Length() int {
 	switch h.AuthType {
@@ -176,7 +176,7 @@ pred (b *BFD) NonInitMem() {
 
 pred (b *BFD) Mem(ub []byte)
 
-preserves acc(d, 1/10000)
+preserves acc(d, perm(1, 10000))
 decreases
 func (d *BFD) Length() int
 

verification/dependencies/github.com/google/gopacket/layers/tcpip.gobra

@@ -18,7 +18,7 @@ type tcpipchecksum struct {
 type tcpipPseudoHeader interface {
 	pred Mem()
 
-	preserves acc(Mem(), 1/10000)
+	preserves acc(Mem(), perm(1, 10000))
 	decreases
 	pseudoheaderChecksum() (uint32, error)
 }

verification/dependencies/hash/hash.gobra

@@ -35,7 +35,7 @@ type Hash interface {
 	// io.Writer // (gobra) Fix: this was changed to be able to re-specify method Write with a stronger spec
 
 	preserves Mem() 
-	preserves acc(p, 1/1000)
+	preserves acc(p, perm(1, 1000))
 	ensures   0 <= n && n <= len(p)
 	// the last conjunct comes from the spec of io.Writer
 	ensures   err == nil && n == len(p)
@@ -45,7 +45,7 @@ type Hash interface {
 
 	// Sum appends the current hash to b and returns the resulting slice.
 	// It does not change the underlying hash state.
-	preserves acc(Mem(), 1/1000)
+	preserves acc(Mem(), perm(1, 1000))
 	requires acc(b)
 	ensures  acc(res) && len(res) == len(b) + Size()
 	decreases

verification/dependencies/io/io.gobra

@@ -72,7 +72,7 @@ type Writer interface {
 	pred Mem()
 
 	preserves Mem() 
-	preserves acc(p, 1/1000)
+	preserves acc(p, perm(1, 1000))
 	ensures 0 <= n && n <= len(p)
 	ensures (n < len(p)) == (err != nil)
 	Write(p []byte) (n int, err error)

verification/dependencies/math/const.gobra

@@ -0,0 +1,32 @@
+// Copyright 2009 The Go Authors. All rights reserved.
+// Use of this source code is governed by a BSD-style
+// license that can be found in the LICENSE file.
+
+// Signatures for the public declarations in file
+// https://github.com/golang/go/blob/master/src/math/const.go
+
+// +gobra
+
+package math
+
+// Integer limit values.
+//
+// (VerifiedSCION) the architecture-dependent limits `MaxInt`, `MinInt`, and
+// `MaxUint` are deliberately not provided: their values depend on the width of
+// the platform `int`/`uint`, which Gobra does not fix, so a proof relying on
+// them would be unsound for some target. Use the limits of a concrete sized
+// type instead.
+const (
+	MaxInt8   = 1<<7 - 1  // 127
+	MinInt8   = -1 << 7   // -128
+	MaxInt16  = 1<<15 - 1 // 32767
+	MinInt16  = -1 << 15  // -32768
+	MaxInt32  = 1<<31 - 1 // 2147483647
+	MinInt32  = -1 << 31  // -2147483648
+	MaxInt64  = 1<<63 - 1 // 9223372036854775807
+	MinInt64  = -1 << 63  // -9223372036854775808
+	MaxUint8  = 1<<8 - 1  // 255
+	MaxUint16 = 1<<16 - 1 // 65535
+	MaxUint32 = 1<<32 - 1 // 4294967295
+	MaxUint64 = 1<<64 - 1 // 18446744073709551615
+)

verification/dependencies/net/iprawsock.gobra

@@ -35,5 +35,5 @@ pred (a *IPAddr) Mem() {
 ensures res == "ip"
 func (a *IPAddr) Network() (res string) { return "ip" }
 
-preserves a != nil ==> acc(a.Mem(), 1/1000)
+preserves a != nil ==> acc(a.Mem(), perm(1, 1000))
 func (a *IPAddr) String() string

verification/dependencies/net/net.gobra

@@ -20,12 +20,12 @@ import (
 type Addr interface {
 	pred Mem()
 
-	requires acc(Mem(), 1/1000)
-	ensures acc(Mem(), 1/1000)
+	requires acc(Mem(), perm(1, 1000))
+	ensures acc(Mem(), perm(1, 1000))
 	Network() string
 
-	requires acc(Mem(), 1/1000)
-	ensures acc(Mem(), 1/1000)
+	requires acc(Mem(), perm(1, 1000))
+	ensures acc(Mem(), perm(1, 1000))
 	String() string
 }
 

verification/dependencies/net/udpsock.gobra

@@ -73,10 +73,10 @@ ensures   err != nil ==> err.ErrorMem()
 func (c *UDPConn) ReadFrom(b []byte) (n int, addr Addr, err error)
 
 // WriteToUDP acts like WriteTo but takes a UDPAddr.
-requires acc(c.Mem(), _) && acc(addr.Mem(), 1/1000)
-requires forall i int :: {&b[i]} 0 <= i && i < len(b) ==> acc(&b[i], 1/1000)
-ensures c.Mem() && acc(addr.Mem(), 1/1000)
-ensures forall i int :: {&b[i]} 0 <= i && i < len(b) ==> acc(&b[i], 1/1000)
+requires acc(c.Mem(), _) && acc(addr.Mem(), perm(1, 1000))
+requires forall i int :: {&b[i]} 0 <= i && i < len(b) ==> acc(&b[i], perm(1, 1000))
+ensures c.Mem() && acc(addr.Mem(), perm(1, 1000))
+ensures forall i int :: {&b[i]} 0 <= i && i < len(b) ==> acc(&b[i], perm(1, 1000))
 func (c *UDPConn) WriteToUDP(b []byte, addr *UDPAddr) (int, error)
 
 // WriteTo implements the PacketConn WriteTo method.

verification/dependencies/strconv/atoi.gobra

@@ -10,10 +10,14 @@
 package strconv
 
 // a to the power of b
+// (VerifiedSCION) 'base', 'exp', and the result are mathematical integers: under the sound
+// bounded-integer semantics, typing them as 'int' would make the repeated multiplication
+// overflow-prone and thus opaque, and 'Exp(2, 64)' (a legal argument of 'ParseUint') is not
+// even representable as an 'int'.
 ghost
 requires exp >= 0
 decreases exp
-pure func Exp(base int, exp int) (res int) {
+pure func Exp(base integer, exp integer) (res integer) {
 	return exp == 0 ? 1 : (base * Exp(base, exp - 1))
 }
 
@@ -22,7 +26,7 @@ ghost
 requires exp >= 10
 ensures  Exp(2, exp) == 1024 * Exp(2, exp - 10)
 decreases
-func Exp2to10(exp int) {
+func Exp2to10(exp integer) {
 	assert Exp(2, exp) == 2 * Exp(2, exp - 1)
 	assert Exp(2, exp) == 4 * Exp(2, exp - 2)
 	assert Exp(2, exp) == 8 * Exp(2, exp - 3)
@@ -37,7 +41,7 @@ func Exp2to10(exp int) {
 // ParseUint is like ParseInt but for unsigned numbers.
 requires base == 0 || (2 <= base && base <= 36)
 requires bitSize > 0 && bitSize <= 64
-ensures retErr == nil ==> (ret >= 0 && ret < uint64(Exp(2, bitSize)))
+ensures retErr == nil ==> integer(ret) < Exp(2, integer(bitSize))
 ensures retErr != nil ==> retErr.ErrorMem()
 decreases _
 func ParseUint(s string, base int, bitSize int) (ret uint64, retErr error)