make Len impure and add LenSpec (#357)

pkg/slayers/path/empty/empty.go

@@ -71,29 +71,28 @@ func (o Path) DecodeFromBytes(r []byte) (e error) {
 
 // @ ensures e == nil
 // @ decreases
-func (o Path) SerializeTo(b []byte /*@, underlyingBuf []byte @*/) (e error) {
+func (o Path) SerializeTo(b []byte /*@, ub []byte @*/) (e error) {
 	return nil
 }
 
-// @ requires o.Mem(underlyingBuf)
+// @ requires o.Mem(ub)
 // @ ensures  p == o
-// @ ensures  p.Mem(underlyingBuf)
+// @ ensures  p.Mem(ub)
 // @ ensures  e == nil
 // @ decreases
-func (o Path) Reverse( /*@ underlyingBuf []byte @*/ ) (p path.Path, e error) {
+func (o Path) Reverse( /*@ ub []byte @*/ ) (p path.Path, e error) {
 	return o, nil
 }
 
-// @ pure
-// @ ensures 0 <= r
+// @ ensures r == o.LenSpec(ub)
 // @ decreases
-func (o Path) Len( /*@ underlyingBuf []byte @*/ ) (r int) {
+func (o Path) Len( /*@ ub []byte @*/ ) (r int) {
 	return PathLen
 }
 
 // @ pure
 // @ ensures r == PathType
 // @ decreases
-func (o Path) Type( /*@ underlyingBuf []byte @*/ ) (r path.Type) {
+func (o Path) Type( /*@ ub []byte @*/ ) (r path.Type) {
 	return PathType
 }

pkg/slayers/path/empty/empty_spec.gobra

@@ -41,6 +41,13 @@ func (p Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
 	return true
 }
 
+ghost
+pure
+decreases
+func (p Path) LenSpec(ghost ub []byte) (l int) {
+	return PathLen
+}
+
 Path implements path.Path
 
 // Definitions to allow *Path to be treated as a path.Path

pkg/slayers/path/epic/epic.go

@@ -85,7 +85,7 @@ type Path struct {
 // @ preserves sl.Bytes(b, 0, len(b))
 // @ ensures   r != nil ==> r.ErrorMem()
 // @ ensures   !old(p.hasScionPath(ubuf)) ==> r != nil
-// @ ensures   len(b) < old(p.Len(ubuf)) ==> r != nil
+// @ ensures   len(b) < old(p.LenSpec(ubuf)) ==> r != nil
 // @ ensures   old(p.getPHVFLen(ubuf)) != HVFLen ==> r != nil
 // @ ensures   old(p.getLHVFLen(ubuf)) != HVFLen ==> r != nil
 // @ decreases
@@ -211,20 +211,16 @@ func (p *Path) Reverse( /*@ ghost ubuf []byte @*/ ) (ret path.Path, r error) {
 }
 
 // Len returns the length of the EPIC path in bytes.
-// (VerifiedSCION) This is currently not checked here because Gobra
-// does not support statements in pure functions. The proof obligations
-// for this method are discharged in function `len_test` in the file `epic_spec_test.gobra`.
-// @ trusted
-// @ pure
-// @ requires acc(p.Mem(ubuf), _)
-// @ ensures  !p.hasScionPath(ubuf) ==> l == MetadataLen
-// @ ensures  p.hasScionPath(ubuf)  ==> l == MetadataLen + unfolding acc(p.Mem(ubuf), _) in p.ScionPath.Len(ubuf[MetadataLen:])
+// @ preserves acc(p.Mem(ubuf), R50)
+// @ ensures   l == p.LenSpec(ubuf)
 // @ decreases
 func (p *Path) Len( /*@ ghost ubuf []byte @*/ ) (l int) {
+	// @ unfold acc(p.Mem(ubuf), R50)
+	// @ defer fold acc(p.Mem(ubuf), R50)
 	if p.ScionPath == nil {
 		return MetadataLen
 	}
-	return MetadataLen + p.ScionPath.Len( /*@ ubuf @*/ )
+	return MetadataLen + p.ScionPath.Len( /*@ ubuf[MetadataLen:] @*/ )
 }
 
 // Type returns the EPIC path type identifier.

pkg/slayers/path/epic/epic_spec.gobra

@@ -18,6 +18,8 @@ package epic
 
 import (
 	"github.com/scionproto/scion/pkg/slayers/path"
+
+	. "github.com/scionproto/scion/verification/utils/definitions"
 	sl "github.com/scionproto/scion/verification/utils/slices"
 )
 
@@ -35,6 +37,17 @@ pred (p *Path) Mem(ubuf []byte) {
 	p.ScionPath.Mem(ubuf[MetadataLen:])
 }
 
+ghost
+pure
+requires acc(p.Mem(ub), _)
+decreases
+func (p *Path) LenSpec(ghost ub []byte) (l int) {
+	return unfolding acc(p.Mem(ub), _) in
+		(p.ScionPath == nil ?
+			MetadataLen :
+			MetadataLen + p.ScionPath.LenSpec(ub[MetadataLen:]))
+}
+
 ghost
 requires p.Mem(buf)
 ensures  p.NonInitMem()

pkg/slayers/path/epic/epic_spec_test.gobra

@@ -24,21 +24,4 @@ func testAllocateNonInitMem() {
 }
 
 // A test folding Mem(ubuf) is skipped here, as one can just call DesugarFromBytes to get the
-// desired predicate
-
-// (*Path).Len() cannot be currently be verified because Gobra does not allow statements in
-// pure functions, but Len must be pure.
-// This method contains the same exact body and checks that the contract holds.
-ghost
-preserves acc(p.Mem(ubuf), _)
-ensures   !p.hasScionPath(ubuf) ==> l == MetadataLen
-ensures   p.hasScionPath(ubuf)  ==> l == MetadataLen + unfolding acc(p.Mem(ubuf), _) in p.ScionPath.Len(ubuf[MetadataLen:])
-decreases
-func len_test(p *Path, ubuf []byte) (l int) {
-	unfold acc(p.Mem(ubuf), _) // would need to be 'unfolding' in the pure version
-	if p.ScionPath == nil {
-		return MetadataLen
-	}
-	unfold acc(p.ScionPath.Mem(ubuf[MetadataLen:]), _) // would need to be 'unfolding' in the pure version
-	return  MetadataLen + p.ScionPath.Len(ubuf[MetadataLen:])
-}
+// desired predicate.

pkg/slayers/path/onehop/onehop.go

@@ -105,7 +105,7 @@ func (o *Path) DecodeFromBytes(data []byte) (r error) {
 // @ preserves sl.Bytes(b, 0, len(b))
 // @ ensures   (len(b) >= PathLen) == (err == nil)
 // @ ensures   err != nil ==> err.ErrorMem()
-// @ ensures   err == nil ==> o.Len(ubuf) <= len(b)
+// @ ensures   err == nil ==> o.LenSpec(ubuf) <= len(b)
 // @ decreases
 func (o *Path) SerializeTo(b []byte /*@, ubuf []byte @*/) (err error) {
 	if len(b) < PathLen {
@@ -219,8 +219,7 @@ func (o *Path) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, err error) {
 	return sp.Reverse( /*@ ubuf @*/ )
 }
 
-// @ pure
-// @ ensures l == PathLen
+// @ ensures l == o.LenSpec(ubuf)
 // @ decreases
 func (o *Path) Len( /*@ ghost ubuf []byte @*/ ) (l int) {
 	return PathLen

pkg/slayers/path/onehop/onehop_spec.gobra

@@ -48,7 +48,7 @@ requires acc(o.Mem(ub), _)
 ensures  b
 decreases
 pure func (o *Path) InferSizeUb(ghost ub []byte) (b bool) {
-	return unfolding acc(o.Mem(ub), _) in o.Len(ub) <= len(ub)
+	return unfolding acc(o.Mem(ub), _) in o.LenSpec(ub) <= len(ub)
 }
 
 ghost
@@ -58,4 +58,11 @@ func (p *Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
 	return true
 }
 
+ghost
+pure
+decreases
+func (p *Path) LenSpec(ghost ub []byte) (l int) {
+	return PathLen
+}
+
 (*Path) implements path.Path

pkg/slayers/path/path.go

@@ -64,19 +64,19 @@ func (t Type) String() string {
 // Path is the path contained in the SCION header.
 type Path interface {
 	// (VerifiedSCION) Must hold for every valid Path.
-	//@ pred Mem(underlyingBuf []byte)
+	//@ pred Mem(ub []byte)
 	// (VerifiedSCION) Must imply the resources required to initialize
 	// a new instance of a predicate.
 	//@ pred NonInitMem()
 	// SerializeTo serializes the path into the provided buffer.
 	// (VerifiedSCION) There are implementations of this interface that modify the underlying
 	// structure when serializing (e.g. scion.Raw)
-	//@ preserves sl.Bytes(underlyingBuf, 0, len(underlyingBuf))
-	//@ preserves acc(Mem(underlyingBuf), R1)
+	//@ preserves sl.Bytes(ub, 0, len(ub))
+	//@ preserves acc(Mem(ub), R1)
 	//@ preserves sl.Bytes(b, 0, len(b))
 	//@ ensures   e != nil ==> e.ErrorMem()
 	//@ decreases
-	SerializeTo(b []byte /*@, ghost underlyingBuf []byte @*/) (e error)
+	SerializeTo(b []byte /*@, ghost ub []byte @*/) (e error)
 	// DecodesFromBytes decodes the path from the provided buffer.
 	// (VerifiedSCION) There are implementations of this interface (e.g., scion.Raw) that
 	// store b and use it as internal data.
@@ -96,29 +96,35 @@ type Path interface {
 	//@ IsValidResultOfDecoding(b []byte, err error) (res bool)
 	// Reverse reverses a path such that it can be used in the reversed direction.
 	// XXX(shitz): This method should possibly be moved to a higher-level path manipulation package.
-	//@ requires  Mem(underlyingBuf)
-	//@ preserves sl.Bytes(underlyingBuf, 0, len(underlyingBuf))
+	//@ requires  Mem(ub)
+	//@ preserves sl.Bytes(ub, 0, len(ub))
 	//@ ensures   e == nil ==> p != nil
-	//@ ensures   e == nil ==> p.Mem(underlyingBuf)
+	//@ ensures   e == nil ==> p.Mem(ub)
 	//@ ensures   e != nil ==> e.ErrorMem()
 	//@ decreases
-	Reverse( /*@ ghost underlyingBuf []byte @*/ ) (p Path, e error)
-	// Len returns the length of a path in bytes.
+	Reverse( /*@ ghost ub []byte @*/ ) (p Path, e error)
+	//@ ghost
 	//@ pure
-	//@ requires acc(Mem(underlyingBuf), _)
-	//@ ensures  l >= 0
+	//@ requires acc(Mem(ub), _)
+	//@ ensures  0 <= l
+	//@ decreases
+	//@ LenSpec(ghost ub []byte) (l int)
+
+	// Len returns the length of a path in bytes.
+	//@ preserves acc(Mem(ub), R50)
+	//@ ensures   l == LenSpec(ub)
 	//@ decreases
-	Len( /*@ ghost underlyingBuf []byte @*/ ) (l int)
+	Len( /*@ ghost ub []byte @*/ ) (l int)
 	// Type returns the type of a path.
 	//@ pure
-	//@ requires acc(Mem(underlyingBuf), _)
+	//@ requires acc(Mem(ub), _)
 	//@ decreases
-	Type( /*@ ghost underlyingBuf []byte @*/ ) Type
+	Type( /*@ ghost ub []byte @*/ ) Type
 	//@ ghost
-	//@ requires Mem(underlyingBuf)
+	//@ requires Mem(ub)
 	//@ ensures  NonInitMem()
 	//@ decreases
-	//@ DowngradePerm(ghost underlyingBuf []byte)
+	//@ DowngradePerm(ghost ub []byte)
 }
 
 type metadata struct {
@@ -209,18 +215,18 @@ type rawPath struct {
 	pathType Type
 }
 
-// @ preserves acc(p.Mem(underlyingBuf), R10)
-// @ preserves acc(sl.Bytes(underlyingBuf, 0, len(underlyingBuf)), R10)
+// @ preserves acc(p.Mem(ub), R10)
+// @ preserves acc(sl.Bytes(ub, 0, len(ub)), R10)
 // @ preserves sl.Bytes(b, 0, len(b))
 // @ ensures   e == nil
 // @ decreases
-func (p *rawPath) SerializeTo(b []byte /*@, ghost underlyingBuf []byte @*/) (e error) {
+func (p *rawPath) SerializeTo(b []byte /*@, ghost ub []byte @*/) (e error) {
 	//@ unfold sl.Bytes(b, 0, len(b))
-	//@ unfold acc(p.Mem(underlyingBuf), R10)
+	//@ unfold acc(p.Mem(ub), R10)
 	//@ unfold acc(sl.Bytes(p.raw, 0, len(p.raw)), R11)
 	copy(b, p.raw /*@, R11 @*/)
 	//@ fold acc(sl.Bytes(p.raw, 0, len(p.raw)), R11)
-	//@ fold acc(p.Mem(underlyingBuf), R10)
+	//@ fold acc(p.Mem(ub), R10)
 	//@ fold sl.Bytes(b, 0, len(b))
 	return nil
 }
@@ -239,21 +245,20 @@ func (p *rawPath) DecodeFromBytes(b []byte) (e error) {
 
 // @ ensures  e != nil && e.ErrorMem()
 // @ decreases
-func (p *rawPath) Reverse( /*@ ghost underlyingBuf []byte @*/ ) (r Path, e error) {
+func (p *rawPath) Reverse( /*@ ghost ub []byte @*/ ) (r Path, e error) {
 	return nil, serrors.New("not supported")
 }
 
-// @ pure
-// @ requires acc(p.Mem(underlyingBuf), _)
-// @ ensures l >= 0
+// @ preserves acc(p.Mem(ub), R50)
+// @ ensures   l == p.LenSpec(ub)
 // @ decreases
-func (p *rawPath) Len( /*@ ghost underlyingBuf []byte @*/ ) (l int) {
-	return /*@ unfolding acc(p.Mem(underlyingBuf), _) in @*/ len(p.raw)
+func (p *rawPath) Len( /*@ ghost ub []byte @*/ ) (l int) {
+	return /*@ unfolding acc(p.Mem(ub), R50) in @*/ len(p.raw)
 }
 
 // @ pure
-// @ requires acc(p.Mem(underlyingBuf), _)
+// @ requires acc(p.Mem(ub), _)
 // @ decreases
-func (p *rawPath) Type( /*@ ghost underlyingBuf []byte @*/ ) Type {
-	return /*@ unfolding acc(p.Mem(underlyingBuf), _) in @*/ p.pathType
+func (p *rawPath) Type( /*@ ghost ub []byte @*/ ) Type {
+	return /*@ unfolding acc(p.Mem(ub), _) in @*/ p.pathType
 }

pkg/slayers/path/path_spec.gobra

@@ -44,6 +44,15 @@ func (p *rawPath) IsValidResultOfDecoding(b []byte, err error) (res bool) {
 	return true
 }
 
+ghost
+pure
+requires acc(p.Mem(ub), _)
+ensures  0 <= l
+decreases
+func (p *rawPath) LenSpec(ghost ub []byte) (l int) {
+	return unfolding acc(p.Mem(ub), _) in len(p.raw)
+}
+
 (*rawPath) implements Path
 
 /** End of rawPath spec **/

pkg/slayers/path/scion/decoded.go

@@ -153,7 +153,7 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
 	//@ invariant acc(s.Mem(ubuf), R1)
 	//@ invariant sl.Bytes(ubuf, 0, len(ubuf))
 	//@ invariant b !== ubuf ==> sl.Bytes(b, 0, len(b))
-	//@ invariant s.Len(ubuf) <= len(b)
+	//@ invariant s.LenSpec(ubuf) <= len(b)
 	//@ invariant 0 <= i && i <= s.getLenInfoFields(ubuf)
 	//@ invariant offset == MetaLen + i * path.InfoLen
 	//@ invariant MetaLen + s.getLenInfoFields(ubuf) * path.InfoLen + s.getLenHopFields(ubuf) * path.HopLen <= len(b)
@@ -180,7 +180,7 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
 	//@ invariant acc(s.Mem(ubuf), R1)
 	//@ invariant sl.Bytes(ubuf, 0, len(ubuf))
 	//@ invariant b !== ubuf ==> sl.Bytes(b, 0, len(b))
-	//@ invariant s.Len(ubuf) <= len(b)
+	//@ invariant s.LenSpec(ubuf) <= len(b)
 	//@ invariant 0 <= i && i <= s.getLenHopFields(ubuf)
 	//@ invariant offset == MetaLen + s.getLenInfoFields(ubuf) * path.InfoLen + i * path.HopLen
 	//@ invariant MetaLen + s.getLenInfoFields(ubuf) * path.InfoLen + s.getLenHopFields(ubuf) * path.HopLen <= len(b)

pkg/slayers/path/scion/decoded_spec.gobra

@@ -58,16 +58,22 @@ pred (d *Decoded) Mem(ubuf []byte) {
   * Unfortunately, Gobra does not fully support them yet, so we
   * introduced this method which acts as a wrapper.
   */
-  // TODO: can this spec be simplified (by removing the access to d.Mem(...))?
-pure
-requires acc(d.Mem(ubuf), _)
-ensures  unfolding acc(d.Mem(ubuf), _) in l == d.Base.Len()
-ensures  l >= 0
+preserves acc(d.Mem(ubuf), R50)
+ensures   l == d.LenSpec(ubuf)
 decreases
 func (d *Decoded) Len(ghost ubuf []byte) (l int) {
 	return unfolding acc(d.Mem(ubuf), _) in d.Base.Len()
 }
 
+ghost
+pure
+requires acc(d.Mem(ub), _)
+ensures  unfolding acc(d.Mem(ub), _) in l == d.Base.Len()
+decreases
+func (d *Decoded) LenSpec(ghost ub []byte) (l int) {
+	return unfolding acc(d.Mem(ub), _) in d.Base.Len()
+}
+
 /**
   * This method is not part of the original SCION codebase.
   * Instead, `Len` was defined in `*Decoded` via embedded structs.
@@ -106,7 +112,7 @@ func (d *Decoded) IsXover(ghost ubuf []byte) bool {
 requires d.Mem(ubuf)
 ensures  e == nil ==> (
 	d.Mem(ubuf) &&
-	d.Len(ubuf) == old(d.Len(ubuf)) &&
+	d.LenSpec(ubuf) == old(d.LenSpec(ubuf)) &&
 	(old(d.ValidCurrIdxs(ubuf)) ==> d.ValidCurrIdxs(ubuf)))
 ensures  e != nil ==> d.NonInitMem() && e.ErrorMem()
 decreases