Adapt to use the new integer type and to pass stricter overflow checks

.github/workflows/gobra.yml

@@ -19,7 +19,7 @@ env:
   assumeInjectivityOnInhale: '1'
   parallelizeBranches: '0'
   checkConsistency: '1'
-  imageVersion: 'latest'
+  imageVersion: 'ghcr.io/viperproject/gobra:fix-overflow-checks'
   mceMode: 'od'
   # disabled for now, as it is unclear which triggers to
   # provide to monoset in a way that it does not severely
@@ -98,7 +98,7 @@ jobs:
       #   with:
       #     path: ${{ runner.workspace }}/.gobra/cache.json
       #     key: ${{ env.cache-name }}
-    
+
       # We split the verification of the entire repository into
       # multiple steps. This provides a more fine-grained log in
       # Github Workflow's interface and it allows more fine-grained

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
+	// @ decreases integer(asParts) - integer(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

@@ -100,12 +100,14 @@ type HostAddr interface {
 	Type() HostAddrType
 
 	//@ requires acc(Mem(), R13)
-	//@ ensures forall i int :: { &res[i] } 0 <= i && i < len(res) ==> acc(&res[i], R13)
+	//@ ensures forall i int :: { &res[i] } int(0) <= i && i < len(res) ==>
+	//@ 	acc(&res[i], R13)
 	//@ decreases
 	Pack() (res []byte)
 
 	//@ requires acc(Mem(), R13)
-	//@ ensures forall i int :: { &res[i] } 0 <= i && i < len(res) ==> acc(&res[i], R13)
+	//@ ensures forall i int :: { &res[i] } int(0) <= i && i < len(res) ==>
+	//@ 	acc(&res[i], R13)
 	//@ decreases
 	IP() (res net.IP)
 
@@ -281,6 +283,7 @@ func (h HostIPv6) IP() (res net.IP) {
 func (h HostIPv6) Copy() (res HostAddr) {
 	//@ unfold acc(h.Mem(), R13)
 	//@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
+	//@ assert len(net.IP(nil)) + len(h) <= MAX_INT
 	tmp := HostIPv6(append( /*@ R13, @*/ net.IP(nil), h...))
 	//@ fold acc(sl.Bytes(h, 0, len(h)), R13)
 	//@ fold sl.Bytes(tmp, 0, len(tmp))
@@ -358,7 +361,7 @@ func (h HostSVC) Pack() (res []byte) {
 	return out
 }
 
-// @ requires pad >= 0
+// @ requires 0 <= pad && pad <= 1000
 // @ ensures acc(res)
 // @ decreases
 func (h HostSVC) PackWithPad(pad int) (res []byte) {

pkg/addr/host_spec.gobra

@@ -23,20 +23,20 @@ import (
 	"github.com/scionproto/scion/verification/utils/slices"
 )
 
-pred (h HostNone) Mem() { len(h) == HostLenNone }
+pred (h HostNone) Mem() { len(h) == int(HostLenNone) }
 
 HostNone implements HostAddr
 
 pred (h HostIPv4) Mem() {
-	len(h) == HostLenIPv4 &&
-	slices.Bytes(h, 0, len(h))
+	len(h) == int(HostLenIPv4) &&
+	slices.Bytes(h, int(0), len(h))
 }
 
 HostIPv4 implements HostAddr
 
 pred (h HostIPv6) Mem() {
-	len(h) == HostLenIPv6 &&
-	slices.Bytes(h, 0, len(h))
+	len(h) == int(HostLenIPv6) &&
+	slices.Bytes(h, int(0), len(h))
 }
 
 HostIPv6 implements HostAddr

pkg/addr/isdas.go

@@ -25,6 +25,7 @@ import (
 	"strings"
 
 	"github.com/scionproto/scion/pkg/private/serrors"
+	// @ "github.com/scionproto/scion/verification/utils/bitwise"
 )
 
 const (
@@ -54,6 +55,15 @@ func ParseISD(s string) (ISD, error) {
 	if err != nil {
 		return 0, serrors.WrapStr("parsing ISD", err)
 	}
+	// @ strconv.Exp2to10(16)
+	// @ assert strconv.Exp(2, 16) == 1024 * strconv.Exp(2, 6)
+	// @ assert strconv.Exp(2, 6) == 2 * strconv.Exp(2, 5)
+	// @ assert strconv.Exp(2, 5) == 2 * strconv.Exp(2, 4)
+	// @ assert strconv.Exp(2, 4) == 2 * strconv.Exp(2, 3)
+	// @ assert strconv.Exp(2, 3) == 2 * strconv.Exp(2, 2)
+	// @ assert strconv.Exp(2, 2) == 2 * strconv.Exp(2, 1)
+	// @ assert strconv.Exp(2, 1) == 2 * strconv.Exp(2, 0)
+	// @ assert 0 <= isd && isd < strconv.Exp(2, 16)
 	return ISD(isd), nil
 }
 
@@ -216,6 +226,7 @@ func ParseIA(ia string) (IA, error) {
 
 // @ decreases
 func (ia IA) ISD() ISD {
+	// @ bitwise.ShiftRight48Bits(uint64(ia))
 	return ISD(ia >> ASBits)
 }
 

pkg/slayers/extn.go

@@ -48,6 +48,7 @@ type tlvOption struct {
 	OptAlign     [2]uint8 // Xn+Y = [2]uint8{X, Y}
 }
 
+// @ requires false
 // @ preserves acc(o, R20)
 // @ ensures   0 < res
 // @ ensures   o.OptType == OptTypePad1 ==> res == 1
@@ -62,16 +63,17 @@ func (o *tlvOption) length(fixLengths bool) (res int) {
 	if fixLengths {
 		return len(o.OptData) + 2
 	}
-	// (VerifiedSCION) gobra cannot prove this yet, even though it must hold
-	//                 as the type of o.OptDataLen is uint8
-	// @ assume 0 <= o.OptDataLen
+	// @ assert 0 <= o.OptDataLen
 	return int(o.OptDataLen) + 2
 }
 
 // @ requires  2 <= len(data)
-// @ preserves acc(o)
-// @ preserves acc(sl.Bytes(o.OptData, 0, len(o.OptData)), R20)
+// @ requires  acc(o)
+// @ requires  acc(sl.Bytes(o.OptData, 0, len(o.OptData)), R20)
+// @ requires  fixLengths ==> len(o.OptData) <= 255
 // @ preserves sl.Bytes(data, 0, len(data))
+// @ ensures   acc(o)
+// @ ensures   acc(sl.Bytes(o.OptData, 0, len(o.OptData)), R20)
 // @ decreases
 func (o *tlvOption) serializeTo(data []byte, fixLengths bool) {
 	dryrun := data == nil
@@ -103,7 +105,7 @@ func (o *tlvOption) serializeTo(data []byte, fixLengths bool) {
 // @ ensures   err == nil ==> acc(res)
 // @ ensures   (err == nil && res.OptType != OptTypePad1) ==> (
 // @ 	2 <= res.ActualLength && res.ActualLength <= len(data) && res.OptData === data[2:res.ActualLength])
-// @ ensures   err == nil ==> 0 < res.ActualLength
+// @ ensures   err == nil ==> 0 < res.ActualLength && res.ActualLength <= 258
 // @ ensures   err != nil ==> err.ErrorMem()
 // @ decreases
 func decodeTLVOption(data []byte) (res *tlvOption, err error) {
@@ -118,8 +120,7 @@ func decodeTLVOption(data []byte) (res *tlvOption, err error) {
 		return nil, serrors.New("buffer too short", "expected", 2, "actual", len(data))
 	}
 	o.OptDataLen = data[1]
-	// (VerifiedSCION) Gobra cannot prove this even though it must hold, given the type of o.OptDataLen
-	// @ assume 0 <= o.OptDataLen
+	// @ assert 0 <= o.OptDataLen
 	o.ActualLength = int(o.OptDataLen) + 2
 	if len(data) < o.ActualLength {
 		return nil, serrors.New("buffer too short", "expected", o.ActualLength, "actual", len(data))
@@ -131,8 +132,8 @@ func decodeTLVOption(data []byte) (res *tlvOption, err error) {
 }
 
 // serializeTLVOptionPadding adds an appropriate PadN extension.
-// @ requires  padLength == 1 ==> 1 <= len(data)
-// @ requires  1 < padLength  ==> 2 <= len(data)
+// @ requires  padLength == int(1) ==> 1 <= len(data)
+// @ requires  int(1) < padLength  ==> 2 <= len(data)
 // @ preserves sl.Bytes(data, 0, len(data))
 // @ decreases
 func serializeTLVOptionPadding(data []byte, padLength int) {
@@ -249,7 +250,8 @@ func (e *extnBase) serializeToWithTLVOptions(b gopacket.SerializeBuffer,
 // @ 	2 <= len(data) &&
 // @ 	0 <= res.ActualLen && res.ActualLen <= len(data) &&
 // @ 	res.BaseLayer.Contents === data[:res.ActualLen] &&
-// @ 	res.BaseLayer.Payload === data[res.ActualLen:])
+// @ 	res.BaseLayer.Payload === data[res.ActualLen:]  &&
+// @ 	res.ActualLen <= MAX_INT - 258)
 // @ decreases
 func decodeExtnBase(data []byte, df gopacket.DecodeFeedback) (res extnBase, resErr error) {
 	e := extnBase{}
@@ -268,9 +270,7 @@ func decodeExtnBase(data []byte, df gopacket.DecodeFeedback) (res extnBase, resE
 		return extnBase{}, serrors.New(fmt.Sprintf("invalid extension header. "+
 			"Length %d less than specified length %d", len(data), e.ActualLen))
 	}
-	// (VerifiedSCION) assumed because of Gobra's limitations. Nonetheless, we should know from the the type
-	// of e.ExtLen that this property always holds.
-	// @ assume 0 <= e.ExtLen
+	// @ assert 0 <= e.ExtLen
 	// @ assert 0 <= e.ActualLen
 	e. /*@ BaseLayer. @*/ Contents = data[:e.ActualLen]
 	e. /*@ BaseLayer. @*/ Payload = data[e.ActualLen:]
@@ -369,8 +369,9 @@ func (h *HopByHopExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
 
 	// @ invariant 2 <= offset
 	// @ invariant acc(h)
-	// @ invariant 0 <= h.ActualLen && h.ActualLen <= len(data)
+	// @ invariant 0 <= h.ActualLen && h.ActualLen <= len(data) && h.ActualLen <= MAX_INT - 258
 	// @ invariant len(h.Options) == lenOptions
+	// @ invariant lenOptions < offset
 	// @ invariant forall i int :: { &h.Options[i] } 0 <= i && i < lenOptions ==>
 	// @ 	(acc(&h.Options[i]) && h.Options[i].Mem(i))
 	// @ invariant acc(sl.Bytes(data, 0, len(data)), R40)
@@ -501,8 +502,9 @@ func (e *EndToEndExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
 
 	// @ invariant 2 <= offset
 	// @ invariant acc(e)
-	// @ invariant 0 <= e.ActualLen && e.ActualLen <= len(data)
+	// @ invariant 0 <= e.ActualLen && e.ActualLen <= len(data) && e.ActualLen <= MAX_INT - 258
 	// @ invariant len(e.Options) == lenOptions
+	// @ invariant lenOptions < offset
 	// @ invariant forall i int :: { &e.Options[i] } 0 <= i && i < lenOptions ==>
 	// @ 	(acc(&e.Options[i]) && e.Options[i].Mem(i))
 	// @ invariant acc(sl.Bytes(data, 0, len(data)), R40)

pkg/slayers/extn_spec.gobra

@@ -46,7 +46,7 @@ pred (h *HopByHopExtn) NonInitMem() {
 pred (h *HopByHopExtn) Mem(ubuf []byte) {
 	h.extnBase.Mem(ubuf) &&
 	acc(&h.Options) &&
-	forall i int :: { &h.Options[i] } 0 <= i && i < len(h.Options) ==>
+	forall i int :: { &h.Options[i] } int(0) <= i && i < len(h.Options) ==>
 		(acc(&h.Options[i]) && h.Options[i].Mem(i))
 }
 
@@ -94,8 +94,8 @@ func (h *HopByHopExtnSkipper) LayerContents() (res []byte) {
 // Gobra is not able to infer that HopByHopExtnSkipper is "inheriting"
 // the implementation of LayerPayload from extnBase.
 preserves acc(h.Mem(ub), R20)
-ensures   0 <= start && start <= end && end <= len(ub)
-ensures   len(res) == end - start
+ensures   int(0) <= start && start <= end && end <= len(ub)
+ensures   integer(len(res)) == integer(end - start)
 ensures   res === ub[start:end]
 decreases
 func (h *HopByHopExtnSkipper) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) {
@@ -134,7 +134,7 @@ pred (e *EndToEndExtn) NonInitMem() {
 pred (e *EndToEndExtn) Mem(ubuf []byte) {
 	e.extnBase.Mem(ubuf) &&
 	acc(&e.Options) &&
-	forall i int :: { &e.Options[i] } 0 <= i && i < len(e.Options) ==>
+	forall i int :: { &e.Options[i] } int(0) <= i && i < len(e.Options) ==>
 		(acc(&e.Options[i]) && e.Options[i].Mem(i))
 }
 
@@ -184,7 +184,7 @@ func (e *EndToEndExtnSkipper) LayerContents() (res []byte) {
 // Gobra is not able to infer that EndToEndExtnSkipper is "inheriting"
 // the implementation of LayerPayload from extnBase.
 preserves acc(e.Mem(ub), R20)
-ensures   0 <= start && start <= end && end <= len(ub)
+ensures   int(0) <= start && start <= end && end <= len(ub)
 ensures   len(res) == end - start
 ensures   res === ub[start:end]
 decreases

pkg/slayers/path/empty/empty.go

@@ -85,12 +85,12 @@ func (o Path) Reverse( /*@ ub []byte @*/ ) (p path.Path, e error) {
 // @ ensures r == o.LenSpec(ub)
 // @ decreases
 func (o Path) Len( /*@ ub []byte @*/ ) (r int) {
-	return PathLen
+	return int(PathLen)
 }
 
 // @ pure
 // @ ensures r == PathType
 // @ decreases
 func (o Path) Type( /*@ ub []byte @*/ ) (r path.Type) {
-	return PathType
+	return path.Type(PathType)
 }

pkg/slayers/path/empty/empty_spec.gobra

@@ -21,7 +21,7 @@ import (
 	"github.com/scionproto/scion/verification/utils/slices"
 )
 
-pred (e Path) Mem(buf []byte) { len(buf) == 0 }
+pred (e Path) Mem(buf []byte) { len(buf) == int(0) }
 
 pred (e Path) NonInitMem() { true }
 
@@ -43,12 +43,19 @@ pure func (p Path) IsValidResultOfDecoding(b []byte) bool {
 ghost
 decreases
 pure func (p Path) LenSpec(ghost ub []byte) (l int) {
-	return PathLen
+	return int(PathLen)
+}
+
+ghost
+requires p.Mem(b)
+decreases
+pure func (p Path) MayReversePath(b []byte) bool {
+	return true
 }
 
 Path implements path.Path
 
 // Definitions to allow *Path to be treated as a path.Path
-pred (e *Path) Mem(buf []byte) { acc(e) && len(buf) == 0 }
+pred (e *Path) Mem(buf []byte) { acc(e) && len(buf) == int(0) }
 pred (e *Path) NonInitMem() { true }
 (*Path) implements path.Path

pkg/slayers/path/epic/epic.go

@@ -180,6 +180,7 @@ func (p *Path) DecodeFromBytes(b []byte) (r error) {
 // Reverse reverses the EPIC path. In particular, this means that the SCION path type subheader
 // is reversed.
 // @ requires p.Mem(ubuf)
+// @ requires p.MayReversePath(ubuf)
 // @ preserves sl.Bytes(ubuf, 0, len(ubuf))
 // @ ensures  r == nil ==> ret != nil
 // @ ensures  r == nil ==> ret.Mem(ubuf)
@@ -218,6 +219,7 @@ func (p *Path) Len( /*@ ghost ubuf []byte @*/ ) (l int) {
 	if p.ScionPath == nil {
 		return MetadataLen
 	}
+	// @ assert p.ScionPath.LenSpec(ubuf[MetadataLen:]) + MetadataLen <= MAX_INT
 	return MetadataLen + p.ScionPath.Len( /*@ ubuf[MetadataLen:] @*/ )
 }
 
@@ -226,7 +228,7 @@ func (p *Path) Len( /*@ ghost ubuf []byte @*/ ) (l int) {
 // @ ensures  t == PathType
 // @ decreases
 func (p *Path) Type( /*@ ghost ubuf []byte @*/ ) (t path.Type) {
-	return PathType
+	return path.Type(PathType)
 }
 
 // PktID denotes the EPIC packet ID.
@@ -258,9 +260,9 @@ func (i *PktID) DecodeFromBytes(raw []byte) {
 // @ decreases
 func (i *PktID) SerializeTo(b []byte) {
 	//@ unfold sl.Bytes(b, 0, len(b))
-	//@ assert forall j int :: { &b[:4][j] } 0 <= 4 ==> &b[:4][j] == &b[j]
+	//@ assert forall j int :: { &b[:4][j] } 0 <= j && j < 4 ==> &b[:4][j] == &b[j]
 	binary.BigEndian.PutUint32(b[:4], i.Timestamp)
-	//@ assert forall j int :: { &b[4:8][j] } 0 <= 4 ==> &b[4:8][j] == &b[4 + j]
+	//@ assert forall j int :: { &b[4:8][j] } 0 <= 4 && j < 4 ==> &b[4:8][j] == &b[4 + j]
 	binary.BigEndian.PutUint32(b[4:8], i.Counter)
 	//@ fold sl.Bytes(b, 0, len(b))
 }

pkg/slayers/path/epic/epic_spec.gobra

@@ -29,8 +29,8 @@ pred (p *Path) NonInitMem() {
 
 pred (p *Path) Mem(ubuf []byte) {
 	acc(&p.PktID) &&
-	acc(&p.PHVF) && sl.Bytes(p.PHVF, 0, len(p.PHVF)) &&
-	acc(&p.LHVF) && sl.Bytes(p.LHVF, 0, len(p.LHVF)) &&
+	acc(&p.PHVF) && sl.Bytes(p.PHVF, int(0), len(p.PHVF)) &&
+	acc(&p.LHVF) && sl.Bytes(p.LHVF, int(0), len(p.LHVF)) &&
 	acc(&p.ScionPath) &&
 	p.ScionPath != nil &&
 	MetadataLen <= len(ubuf) &&
@@ -43,8 +43,16 @@ decreases
 pure func (p *Path) LenSpec(ghost ub []byte) (l int) {
 	return unfolding p.Mem(ub) in
 		(p.ScionPath == nil ?
-			MetadataLen :
-			MetadataLen + p.ScionPath.LenSpec(ub[MetadataLen:]))
+			int(MetadataLen) :
+			int(MetadataLen) + p.ScionPath.LenSpec(ub[MetadataLen:]))
+}
+
+ghost
+requires p.Mem(b)
+decreases
+pure func (p *Path) MayReversePath(b []byte) bool {
+	return unfolding p.Mem(b) in
+		p.ScionPath.MayReversePath(b[MetadataLen:])
 }
 
 ghost