drop access predicates

pkg/scrypto/scrypto_spec.gobra

@@ -27,7 +27,7 @@ import sl "github.com/scionproto/scion/verification/utils/slices"
 // calls to it will also succeed. This behaviour is abstracted using this
 // ghost function.
 ghost
-requires  acc(sl.Bytes(key, 0, len(key)), _)
+requires  sl.Bytes(key, 0, len(key))
 decreases _
 pure func ValidKeyForHash(key []byte) bool
 

pkg/slayers/path/epic/epic.go

@@ -225,7 +225,6 @@ func (p *Path) Len( /*@ ghost ubuf []byte @*/ ) (l int) {
 
 // Type returns the EPIC path type identifier.
 // @ pure
-// @ requires acc(p.Mem(ubuf), _)
 // @ ensures  t == PathType
 // @ decreases
 func (p *Path) Type( /*@ ghost ubuf []byte @*/ ) (t path.Type) {

pkg/slayers/path/epic/epic_spec.gobra

@@ -38,10 +38,10 @@ pred (p *Path) Mem(ubuf []byte) {
 }
 
 ghost
-requires acc(p.Mem(ub), _)
+requires p.Mem(ub)
 decreases
 pure func (p *Path) LenSpec(ghost ub []byte) (l int) {
-	return unfolding acc(p.Mem(ub), _) in
+	return unfolding p.Mem(ub) in
 		(p.ScionPath == nil ?
 			MetadataLen :
 			MetadataLen + p.ScionPath.LenSpec(ub[MetadataLen:]))
@@ -57,39 +57,43 @@ func (p *Path) DowngradePerm(buf []byte) {
 }
 
 ghost
-requires acc(r.Mem(ub), _)
+requires r.Mem(ub)
 decreases
 pure func (r *Path) GetBase(ub []byte) scion.Base {
-	return unfolding acc(r.Mem(ub), _) in
+	return unfolding r.Mem(ub) in
 		r.ScionPath.GetBase(ub[MetadataLen:])
 }
 
 ghost
-requires acc(p.Mem(buf), _)
+requires p.Mem(buf)
 decreases
 pure func (p *Path) getPHVFLen(buf []byte) (l int) {
-	return unfolding acc(p.Mem(buf), _) in len(p.PHVF)
+	return unfolding p.Mem(buf) in
+		len(p.PHVF)
 }
 
 ghost
-requires acc(p.Mem(buf), _)
+requires p.Mem(buf)
 decreases
 pure func (p *Path) getLHVFLen(buf []byte) (l int) {
-	return unfolding acc(p.Mem(buf), _) in len(p.LHVF)
+	return unfolding p.Mem(buf) in
+		len(p.LHVF)
 }
 
 ghost
-requires acc(p.Mem(buf), _)
+requires p.Mem(buf)
 decreases
 pure func (p *Path) hasScionPath(buf []byte) (r bool) {
-	return unfolding acc(p.Mem(buf), _) in p.ScionPath != nil
+	return unfolding p.Mem(buf) in
+		p.ScionPath != nil
 }
 
 ghost
-requires acc(p.Mem(buf), _)
+requires p.Mem(buf)
 decreases
 pure func (p *Path) GetUnderlyingScionPathBuf(buf []byte) []byte {
-	return unfolding acc(p.Mem(buf), _) in buf[MetadataLen:]
+	return unfolding p.Mem(buf) in
+		buf[MetadataLen:]
 }
 
 ghost

pkg/slayers/path/hopfield_spec.gobra

@@ -43,13 +43,13 @@ pure func IO_ifsToIfs(ifs option[io.IO_ifs]) uint16 {
 ghost
 requires 0 <= start && start <= middle
 requires middle + HopLen <= end && end <= len(raw)
-requires acc(sl.Bytes(raw, start, end), _)
+requires sl.Bytes(raw, start, end)
 decreases
 pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) {
 	return let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==> &raw[middle+2:middle+4][k] == &raw[middle + 2 + k]) in
 		let _ := Asserting(forall k int :: {&raw[middle+4:middle+6][k]} 0 <= k && k < 4 ==> &raw[middle+4:middle+6][k] == &raw[middle + 4 + k]) in
 		let _ := Asserting(forall k int :: {&raw[middle+6:middle+6+MacLen][k]} 0 <= k && k < MacLen ==> &raw[middle+6:middle+6+MacLen][k] == &raw[middle + 6 + k]) in
-		unfolding acc(sl.Bytes(raw, start, end), _) in
+		unfolding sl.Bytes(raw, start, end) in
 		let inif2 := binary.BigEndian.Uint16(raw[middle+2:middle+4]) in
 		let egif2 := binary.BigEndian.Uint16(raw[middle+4:middle+6]) in
 		let op_inif2 := ifsToIO_ifs(inif2) in

pkg/slayers/path/infofield_spec.gobra

@@ -32,31 +32,31 @@ pure func InfoFieldOffset(currINF, headerOffset int) int {
 ghost
 requires 0 <= currINF && 0 <= headerOffset
 requires InfoFieldOffset(currINF, headerOffset) < len(raw)
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 decreases
 pure func ConsDir(raw []byte, currINF int, headerOffset int) bool {
-	return unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
+	return unfolding sl.Bytes(raw, 0, len(raw)) in
 		raw[InfoFieldOffset(currINF, headerOffset)] & 0x1 == 0x1
 }
 
 ghost
 requires 0 <= currINF && 0 <= headerOffset
 requires InfoFieldOffset(currINF, headerOffset) < len(raw)
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 decreases
 pure func Peer(raw []byte, currINF int, headerOffset int) bool {
-	return unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
+	return unfolding sl.Bytes(raw, 0, len(raw)) in
 		raw[InfoFieldOffset(currINF, headerOffset)] & 0x2 == 0x2
 }
 
 ghost
 requires 0 <= currINF && 0 <= headerOffset
 requires InfoFieldOffset(currINF, headerOffset) + InfoLen < len(raw)
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 decreases
 pure func Timestamp(raw []byte, currINF int, headerOffset int) io.IO_ainfo {
 	return let idx := InfoFieldOffset(currINF, headerOffset) + 4 in
-		unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
+		unfolding sl.Bytes(raw, 0, len(raw)) in
 		let _ := Asserting(forall i int :: { &raw[idx+i] } { &raw[idx:idx+4][i] } 0 <= i && i < 4 ==>
 			&raw[idx+i] == &raw[idx:idx+4][i]) in
 		io.IO_ainfo(binary.BigEndian.Uint32(raw[idx : idx + 4]))
@@ -65,11 +65,11 @@ pure func Timestamp(raw []byte, currINF int, headerOffset int) io.IO_ainfo {
 ghost
 requires 0 <= currINF && 0 <= headerOffset
 requires InfoFieldOffset(currINF, headerOffset) + InfoLen < len(raw)
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 decreases
 pure func AbsUinfo(raw []byte, currINF int, headerOffset int) set[io.IO_msgterm] {
 	return 	let idx := InfoFieldOffset(currINF, headerOffset) + 2 in
-		unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
+		unfolding sl.Bytes(raw, 0, len(raw)) in
 		let _ := Asserting(forall k int :: {&raw[idx:idx+2][k]} 0 <= k && k < 2 ==>
 			&raw[idx:idx+4][k] == &raw[idx + k]) in
 		AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[idx:idx+2]))
@@ -79,39 +79,39 @@ ghost
 opaque
 requires 0 <= middle
 requires middle+InfoLen <= len(raw)
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 decreases
 pure func BytesToAbsInfoField(raw [] byte, middle int) (io.AbsInfoField) {
-	return unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
+	return unfolding sl.Bytes(raw, 0, len(raw)) in
 		BytesToAbsInfoFieldHelper(raw, middle)
 }
 
 ghost
 requires 0 <= middle
 requires middle+InfoLen <= len(raw)
 requires forall i int :: { &raw[i] } middle <= i && i < len(raw) ==>
-	acc(&raw[i], _)
+	acc(&raw[i])
 decreases
 pure func BytesToAbsInfoFieldHelper(raw [] byte, middle int) (io.AbsInfoField) {
 	return let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==>
 		&raw[middle+2:middle+4][k] == &raw[middle+2 + k]) in
 		let _ := Asserting(forall k int :: {&raw[middle+4:middle+8][k]} 0 <= k && k < 4 ==>
 			&raw[middle+4:middle+8][k] == &raw[middle+4 + k]) in
 		io.AbsInfoField(io.AbsInfoField_{
-			AInfo : io.IO_ainfo(binary.BigEndian.Uint32(raw[middle+4:middle+8])),
-			UInfo : AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[middle+2:middle+4])),
-			ConsDir : raw[middle] & 0x1 == 0x1,
-			Peer : raw[middle] & 0x2  == 0x2,
+			AInfo: io.IO_ainfo(binary.BigEndian.Uint32(raw[middle+4:middle+8])),
+			UInfo: AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[middle+2:middle+4])),
+			ConsDir: raw[middle] & 0x1 == 0x1,
+			Peer: raw[middle] & 0x2  == 0x2,
 		})
 }
 
 ghost
 decreases
 pure func (inf InfoField) ToAbsInfoField() (io.AbsInfoField) {
 	return io.AbsInfoField(io.AbsInfoField_{
-		AInfo : io.IO_ainfo(inf.Timestamp),
-		UInfo : AbsUInfoFromUint16(inf.SegID),
-		ConsDir : inf.ConsDir,
-		Peer : inf.Peer,
+		AInfo: io.IO_ainfo(inf.Timestamp),
+		UInfo: AbsUInfoFromUint16(inf.SegID),
+		ConsDir: inf.ConsDir,
+		Peer: inf.Peer,
 	})
 }

pkg/slayers/path/io_msgterm_spec.gobra

@@ -39,7 +39,7 @@ pure func AbsMac(mac [MacLen]byte) (io.IO_msgterm)
 // involved for accessing exclusive arrays.
 ghost
 requires MacLen <= len(mac)
-requires forall i int :: { &mac[i] } 0 <= i && i < MacLen ==> acc(&mac[i], _)
+requires forall i int :: { &mac[i] } 0 <= i && i < MacLen ==> acc(&mac[i])
 ensures  len(res) == MacLen
 ensures  forall i int :: { res[i] } 0 <= i && i < MacLen ==> mac[i] == res[i]
 decreases

pkg/slayers/path/onehop/onehop_spec.gobra

@@ -44,22 +44,23 @@ func (p *Path) DowngradePerm(buf []byte) {
 }
 
 ghost
-requires acc(o.Mem(ub), _)
+requires o.Mem(ub)
 ensures  b
 decreases
 pure func (o *Path) InferSizeUb(ghost ub []byte) (b bool) {
-	return unfolding acc(o.Mem(ub), _) in o.LenSpec(ub) <= len(ub)
+	return unfolding o.Mem(ub) in
+		o.LenSpec(ub) <= len(ub)
 }
 
 ghost
 decreases
-pure func (p *Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+pure func (p *Path) IsValidResultOfDecoding(b []byte, err error) bool {
 	return true
 }
 
 ghost
 decreases
-pure func (p *Path) LenSpec(ghost ub []byte) (l int) {
+pure func (p *Path) LenSpec(ghost ub []byte) int {
 	return PathLen
 }
 

pkg/slayers/path/path.go

@@ -91,7 +91,7 @@ type Path interface {
 	//@ ghost
 	//@ pure
 	//@ requires Mem(b)
-	//@ requires acc(sl.Bytes(b, 0, len(b)), _)
+	//@ requires sl.Bytes(b, 0, len(b))
 	//@ decreases
 	//@ IsValidResultOfDecoding(b []byte, err error) (res bool)
 	// Reverse reverses a path such that it can be used in the reversed direction.
@@ -105,7 +105,7 @@ type Path interface {
 	Reverse( /*@ ghost ub []byte @*/ ) (p Path, e error)
 	//@ ghost
 	//@ pure
-	//@ requires acc(Mem(ub), _)
+	//@ requires Mem(ub)
 	//@ ensures  0 <= l
 	//@ decreases
 	//@ LenSpec(ghost ub []byte) (l int)
@@ -117,7 +117,7 @@ type Path interface {
 	Len( /*@ ghost ub []byte @*/ ) (l int)
 	// Type returns the type of a path.
 	//@ pure
-	//@ requires acc(Mem(ub), _)
+	//@ requires Mem(ub)
 	//@ decreases
 	Type( /*@ ghost ub []byte @*/ ) Type
 	//@ ghost
@@ -257,8 +257,8 @@ func (p *rawPath) Len( /*@ ghost ub []byte @*/ ) (l int) {
 }
 
 // @ pure
-// @ requires acc(p.Mem(ub), _)
+// @ requires p.Mem(ub)
 // @ decreases
 func (p *rawPath) Type( /*@ ghost ub []byte @*/ ) Type {
-	return /*@ unfolding acc(p.Mem(ub), _) in @*/ p.pathType
+	return /*@ unfolding p.Mem(ub) in @*/ p.pathType
 }

pkg/slayers/path/path_spec.gobra

@@ -44,11 +44,12 @@ pure func (p *rawPath) IsValidResultOfDecoding(b []byte, err error) (res bool) {
 }
 
 ghost
-requires acc(p.Mem(ub), _)
+requires p.Mem(ub)
 ensures  0 <= l
 decreases
 pure func (p *rawPath) LenSpec(ghost ub []byte) (l int) {
-	return unfolding acc(p.Mem(ub), _) in len(p.raw)
+	return unfolding p.Mem(ub) in
+		len(p.raw)
 }
 
 (*rawPath) implements Path
@@ -66,26 +67,30 @@ pred PathPackageMem() {
 
 ghost
 requires 0 <= t && t < maxPathType
-requires acc(PathPackageMem(), _)
+requires PathPackageMem()
 decreases
 pure func Registered(t Type) (res bool) {
-	return unfolding acc(PathPackageMem(), _) in registeredPaths[t].inUse
+	return unfolding PathPackageMem() in
+		registeredPaths[t].inUse
 }
 
 ghost
 requires 0 <= t && t < maxPathType
-requires acc(PathPackageMem(), _)
+requires PathPackageMem()
 decreases
 pure func GetType(t Type) (res Metadata) {
-	return unfolding acc(PathPackageMem(), _) in registeredPaths[t].Metadata
+	return unfolding PathPackageMem() in
+		registeredPaths[t].Metadata
 }
 
 ghost
-requires acc(PathPackageMem(), _)
-ensures  b == unfolding acc(PathPackageMem(), _) in strictDecoding
+requires PathPackageMem()
+// TODO: drop
+// ensures  b == unfolding acc(PathPackageMem(), _) in strictDecoding
 decreases
 pure func IsStrictDecoding() (b bool) {
-	return unfolding acc(PathPackageMem(), _) in strictDecoding
+	return unfolding PathPackageMem() in
+		strictDecoding
 }
 
 // without passing `writePerm` explicitely below, we run into

pkg/slayers/path/scion/base.go

@@ -227,11 +227,11 @@ func (s *Base) infIndexForHF(hf uint8) (r uint8) {
 // store it, based on the metadata. The actual number of bytes available to contain it
 // can be inferred from the common header field HdrLen. It may or may not be consistent.
 // @ pure
-// @ requires acc(s.Mem(), _)
+// @ requires s.Mem()
 // @ ensures  r >= MetaLen
 // @ decreases
 func (s *Base) Len() (r int) {
-	return /*@ unfolding acc(s.Mem(), _) in @*/ MetaLen + s.NumINF*path.InfoLen + s.NumHops*path.HopLen
+	return /*@ unfolding s.Mem() in @*/ MetaLen + s.NumINF*path.InfoLen + s.NumHops*path.HopLen
 }
 
 // Type returns the type of the path.