diff --git a/pkg/scrypto/scrypto_spec.gobra b/pkg/scrypto/scrypto_spec.gobra
index 9244f498b..b33787ac5 100644
--- a/pkg/scrypto/scrypto_spec.gobra
+++ b/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
 
diff --git a/pkg/slayers/path/epic/epic.go b/pkg/slayers/path/epic/epic.go
index b9400a1ca..c9d770163 100644
--- a/pkg/slayers/path/epic/epic.go
+++ b/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) {
diff --git a/pkg/slayers/path/epic/epic_spec.gobra b/pkg/slayers/path/epic/epic_spec.gobra
index 2da93c9b3..9a59f029c 100644
--- a/pkg/slayers/path/epic/epic_spec.gobra
+++ b/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
diff --git a/pkg/slayers/path/hopfield_spec.gobra b/pkg/slayers/path/hopfield_spec.gobra
index 1678090a2..c7de1425b 100644
--- a/pkg/slayers/path/hopfield_spec.gobra
+++ b/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
diff --git a/pkg/slayers/path/infofield_spec.gobra b/pkg/slayers/path/infofield_spec.gobra
index 2b1b245fb..a620318ac 100644
--- a/pkg/slayers/path/infofield_spec.gobra
+++ b/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,10 +79,10 @@ 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)
 }
 
@@ -90,7 +90,7 @@ 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 ==>
@@ -98,10 +98,10 @@ pure func BytesToAbsInfoFieldHelper(raw [] byte, middle int) (io.AbsInfoField) {
 		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,
 		})
 }
 
@@ -109,9 +109,9 @@ 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,
 	})
 }
\ No newline at end of file
diff --git a/pkg/slayers/path/io_msgterm_spec.gobra b/pkg/slayers/path/io_msgterm_spec.gobra
index 601db4004..b356b426e 100644
--- a/pkg/slayers/path/io_msgterm_spec.gobra
+++ b/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
diff --git a/pkg/slayers/path/onehop/onehop_spec.gobra b/pkg/slayers/path/onehop/onehop_spec.gobra
index 1e1e611e2..c0a542a4d 100644
--- a/pkg/slayers/path/onehop/onehop_spec.gobra
+++ b/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
 }
 
diff --git a/pkg/slayers/path/path.go b/pkg/slayers/path/path.go
index 3a6eb5633..e6c336901 100644
--- a/pkg/slayers/path/path.go
+++ b/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
 }
diff --git a/pkg/slayers/path/path_spec.gobra b/pkg/slayers/path/path_spec.gobra
index 0dced72a0..7af361e66 100644
--- a/pkg/slayers/path/path_spec.gobra
+++ b/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
diff --git a/pkg/slayers/path/scion/base.go b/pkg/slayers/path/scion/base.go
index cbd0e2078..1754bd17a 100644
--- a/pkg/slayers/path/scion/base.go
+++ b/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.
diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra
index fbac2790a..764ff6991 100644
--- a/pkg/slayers/path/scion/base_spec.gobra
+++ b/pkg/slayers/path/scion/base_spec.gobra
@@ -110,37 +110,41 @@ pure func (b Base) NumsCompatibleWithSegLen() bool {
 }
 
 ghost
-requires acc(b.Mem(), _)
+requires b.Mem()
 ensures  0 <= res && res <= 3
 decreases
 pure func (b *Base) GetNumINF() (res int) {
-	return unfolding acc(b.Mem(), _) in b.NumINF
+	return unfolding b.Mem() in
+		b.NumINF
 }
 
 ghost
-requires acc(b.Mem(), _)
+requires b.Mem()
 ensures  0 <= res
 decreases
 pure func (b *Base) GetNumHops() (res int) {
-	return unfolding acc(b.Mem(), _) in b.NumHops
+	return unfolding b.Mem() in
+		b.NumHops
 }
 
 ghost
-requires acc(s.Mem(), _)
+requires s.Mem()
 decreases
 pure func (s *Base) GetMetaHdr() MetaHdr {
-	return unfolding acc(s.Mem(), _) in s.PathMeta
+	return unfolding s.Mem() in
+		s.PathMeta
 }
 
 ghost
-requires acc(s.Mem(), _)
+requires s.Mem()
 decreases
 pure func (s *Base) GetBase() Base {
-	return unfolding acc(s.Mem(), _) in *s
+	return unfolding s.Mem() in
+		*s
 }
 
 ghost
-requires acc(s.Mem(), _)
+requires s.Mem()
 decreases
 pure func (s *Base) GetCurrHF() uint8 {
 	return s.GetMetaHdr().CurrHF
@@ -238,7 +242,7 @@ pure func DecodedFrom(line uint32) MetaHdr {
 }
 
 ghost
-requires acc(sl.Bytes(b, 0, len(b)), _)
+requires sl.Bytes(b, 0, len(b))
 decreases
 pure func (m MetaHdr) DecodeFromBytesSpec(b []byte) bool {
 	return MetaLen <= len(b)             &&
@@ -255,11 +259,11 @@ pure func (m MetaHdr) DecodeFromBytesSpec(b []byte) bool {
 }
 
 ghost
-requires acc(s.Mem(), _)
-requires acc(sl.Bytes(b, 0, len(b)), _)
+requires s.Mem()
+requires sl.Bytes(b, 0, len(b))
 decreases
 pure func (s *Base) DecodeFromBytesSpec(b []byte) bool {
-	return unfolding acc(s.Mem(), _) in
+	return unfolding s.Mem() in
 		s.PathMeta.DecodeFromBytesSpec(b)
 }
 
@@ -290,7 +294,7 @@ pure func (m MetaHdr) SerializedToLine() uint32 {
 }
 
 ghost
-requires acc(sl.Bytes(b, 0, len(b)), _)
+requires sl.Bytes(b, 0, len(b))
 decreases
 pure func (m MetaHdr) SerializeToSpec(b []byte) bool {
 	return MetaLen <= len(b)                &&
@@ -304,7 +308,7 @@ pure func (m MetaHdr) SerializeToSpec(b []byte) bool {
 }
 
 ghost
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires sl.Bytes(ub, 0, len(ub))
 decreases
 pure func (s Base) EqAbsHeader(ub []byte) bool {
 	// we compute the sublice ub[:MetaLen] inside this function instead
@@ -316,11 +320,11 @@ pure func (s Base) EqAbsHeader(ub []byte) bool {
 }
 
 ghost
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires sl.Bytes(ub, 0, len(ub))
 decreases
 pure func (s MetaHdr) EqAbsHeader(ub []byte) bool {
 	return MetaLen <= len(ub) &&
-		unfolding acc(sl.Bytes(ub, 0, len(ub)), _) in
+		unfolding sl.Bytes(ub, 0, len(ub)) in
 		s == DecodedFrom(binary.BigEndian.Uint32(ub[:MetaLen]))
 }
 
diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra
index 680aab30a..9d4dc3898 100644
--- a/pkg/slayers/path/scion/decoded_spec.gobra
+++ b/pkg/slayers/path/scion/decoded_spec.gobra
@@ -24,7 +24,7 @@ import (
 
 ghost
 decreases
-pure func (p *Decoded) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+pure func (p *Decoded) IsValidResultOfDecoding(b []byte, err error) bool {
 	return true
 }
 
@@ -65,10 +65,11 @@ func (d *Decoded) Len(ghost ubuf []byte) (l int) {
 }
 
 ghost
-requires acc(d.Mem(ub), _)
+requires d.Mem(ub)
 decreases
-pure func (d *Decoded) LenSpec(ghost ub []byte) (l int) {
-	return unfolding acc(d.Mem(ub), _) in d.Base.Len()
+pure func (d *Decoded) LenSpec(ghost ub []byte) int {
+	return unfolding d.Mem(ub) in
+		d.Base.Len()
 }
 
 /**
@@ -77,10 +78,11 @@ pure func (d *Decoded) LenSpec(ghost ub []byte) (l int) {
   * Unfortunately, Gobra does not fully support them yet, so we
   * introduced this method which acts as a wrapper.
   */
-requires acc(d.Mem(ubuf), _)
+requires d.Mem(ubuf)
 decreases
-pure func (d *Decoded) Type(ghost ubuf []byte) (t path.Type) {
-	return unfolding acc(d.Mem(ubuf), _) in d.Base.Type()
+pure func (d *Decoded) Type(ghost ubuf []byte) path.Type {
+	return unfolding d.Mem(ubuf) in
+		d.Base.Type()
 }
 
 /**
@@ -123,48 +125,53 @@ func (d *Decoded) IncPath(ghost ubuf []byte) (e error) {
 }
 
 ghost
-requires acc(d.Mem(ub), _)
+requires d.Mem(ub)
 decreases
-pure func (d *Decoded) GetNumINF(ub []byte) (res int) {
-	return unfolding acc(d.Mem(ub), _) in d.Base.GetNumINF()
+pure func (d *Decoded) GetNumINF(ub []byte) int {
+	return unfolding d.Mem(ub) in
+		d.Base.GetNumINF()
 }
 
 ghost
-requires acc(d.Mem(ub), _)
+requires d.Mem(ub)
 decreases
-pure func (d *Decoded) GetNumHops(ub []byte) (res int) {
-	return unfolding acc(d.Mem(ub), _) in d.Base.GetNumHops()
+pure func (d *Decoded) GetNumHops(ub []byte) int {
+	return unfolding d.Mem(ub) in
+		d.Base.GetNumHops()
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *Decoded) GetMetaHdr(ub []byte) MetaHdr {
-	return unfolding acc(s.Mem(ub), _) in s.Base.GetMetaHdr()
+	return unfolding s.Mem(ub) in
+		s.Base.GetMetaHdr()
 }
 
 /**** End of Stubs ****/
 
 /**** Auxiliary Functions ****/
 
-requires acc(d.Mem(ubuf), _)
+requires d.Mem(ubuf)
 decreases
 pure func (d *Decoded) getLenInfoFields(ubuf []byte) int {
-	return unfolding acc(d.Mem(ubuf), _) in len(d.InfoFields)
+	return unfolding d.Mem(ubuf) in
+		len(d.InfoFields)
 }
 
-requires acc(d.Mem(ubuf), _)
+requires d.Mem(ubuf)
 decreases
 pure func (d *Decoded) getLenHopFields(ubuf []byte) int {
-	return unfolding acc(d.Mem(ubuf), _) in len(d.HopFields)
+	return unfolding d.Mem(ubuf) in
+		len(d.HopFields)
 }
 
 ghost
-requires acc(d.Mem(ubuf), _)
+requires d.Mem(ubuf)
 decreases
 pure func (d *Decoded) GetBase(ubuf []byte) Base {
-	return unfolding acc(d.Mem(ubuf), _) in
-		(unfolding acc(d.Base.Mem(), _) in d.Base)
+	return unfolding d.Mem(ubuf) in
+		(unfolding d.Base.Mem() in d.Base)
 }
 
 /**** End of Auxiliary Functions ****/
diff --git a/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
index 6b6dcb075..873a2dcf8 100644
--- a/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
+++ b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
@@ -221,7 +221,7 @@ opaque
 requires 0 < SegLen
 requires 0 <= currHfIdx && currHfIdx <= SegLen
 requires SegLen * path.HopLen == len(hopfields)
-requires acc(sl.Bytes(hopfields, 0, len(hopfields)), _)
+requires sl.Bytes(hopfields, 0, len(hopfields))
 decreases
 pure func CurrSegWithInfo(hopfields []byte, currHfIdx int, SegLen int, inf io.AbsInfoField) io.IO_seg3 {
 	return segment(hopfields, 0, currHfIdx, inf.AInfo, inf.UInfo, inf.ConsDir, inf.Peer, SegLen)
@@ -241,7 +241,7 @@ requires (currInfIdx == 1 && segs.Seg2Len > 0) ||
 		let end := HopfieldsEndIdx(currInfIdx, segs) in
 		inf != none[io.AbsInfoField] &&
 		len(hopfields) == end - start &&
-		acc(sl.Bytes(hopfields, 0, len(hopfields)), _)
+		sl.Bytes(hopfields, 0, len(hopfields))
 decreases
 pure func LeftSegWithInfo(
 	hopfields []byte,
@@ -268,7 +268,7 @@ requires (currInfIdx == 0 && segs.Seg2Len > 0) ||
 		let end := HopfieldsEndIdx(currInfIdx, segs) in
 		inf != none[io.AbsInfoField] &&
 		len(hopfields) == end - start &&
-		acc(sl.Bytes(hopfields, 0, len(hopfields)), _)
+		sl.Bytes(hopfields, 0, len(hopfields))
 decreases
 pure func RightSegWithInfo(
 	hopfields []byte,
@@ -295,7 +295,7 @@ requires (segs.Seg2Len > 0 && segs.Seg3Len > 0 &&
 		let end := HopfieldsEndIdx(currInfIdx, segs) in
 		inf != none[io.AbsInfoField] &&
 		len(hopfields) == end - start &&
-		acc(sl.Bytes(hopfields, 0, len(hopfields)), _)
+		sl.Bytes(hopfields, 0, len(hopfields))
 decreases
 pure func MidSegWithInfo(
 	hopfields []byte,
@@ -363,13 +363,13 @@ ghost
 requires segs.Valid()
 requires PktLen(segs, MetaLen) <= len(raw)
 requires 1 <= currInfIdx && currInfIdx < 4
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 requires (currInfIdx == 1 && segs.Seg2Len > 0) ||
 	(currInfIdx == 2 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ==>
 		let infoBytes := InfofieldByteSlice(raw, currInfIdx) in
 		let hopBytes := HopfieldsByteSlice(raw, currInfIdx, segs) in
-		acc(sl.Bytes(infoBytes, 0, path.InfoLen), _) &&
-		acc(sl.Bytes(hopBytes, 0, len(hopBytes)), _)
+		sl.Bytes(infoBytes, 0, path.InfoLen) &&
+		sl.Bytes(hopBytes, 0, len(hopBytes))
 decreases
 pure func LeftSegEqualitySpec(raw []byte, currInfIdx int, segs io.SegLens) bool {
 	return (currInfIdx == 1 && segs.Seg2Len > 0) ||
@@ -424,13 +424,13 @@ ghost
 requires segs.Valid()
 requires PktLen(segs, MetaLen) <= len(raw)
 requires -1 <= currInfIdx && currInfIdx < 2
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 requires (currInfIdx == 0 && segs.Seg2Len > 0) ||
 	(currInfIdx == 1 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ==>
 		let infoBytes := InfofieldByteSlice(raw, currInfIdx) in
 		let hopBytes := HopfieldsByteSlice(raw, currInfIdx, segs) in
-		acc(sl.Bytes(infoBytes, 0, path.InfoLen), _) &&
-		acc(sl.Bytes(hopBytes, 0, len(hopBytes)), _)
+		sl.Bytes(infoBytes, 0, path.InfoLen) &&
+		sl.Bytes(hopBytes, 0, len(hopBytes))
 decreases
 pure func RightSegEqualitySpec(raw []byte, currInfIdx int, segs io.SegLens) bool {
 	return (currInfIdx == 0 && segs.Seg2Len > 0) ||
@@ -485,13 +485,13 @@ ghost
 requires segs.Valid()
 requires PktLen(segs, MetaLen) <= len(raw)
 requires 2 <= currInfIdx && currInfIdx < 5
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 requires (segs.Seg2Len > 0 && segs.Seg3Len > 0 &&
 	(currInfIdx == 2 || currInfIdx == 4)) ==>
 		let infoBytes := InfofieldByteSlice(raw, currInfIdx) in
 		let hopBytes := HopfieldsByteSlice(raw, currInfIdx, segs) in
-		acc(sl.Bytes(infoBytes, 0, path.InfoLen), _) &&
-		acc(sl.Bytes(hopBytes, 0, len(hopBytes)), _)
+		sl.Bytes(infoBytes, 0, path.InfoLen) &&
+		sl.Bytes(hopBytes, 0, len(hopBytes))
 decreases
 pure func MidSegEqualitySpec(raw []byte, currInfIdx int, segs io.SegLens) bool {
 	return (segs.Seg2Len > 0 && segs.Seg3Len > 0 &&
@@ -551,24 +551,24 @@ func MidSegEquality(raw []byte, currInfIdx int, segs io.SegLens) {
 ghost
 requires 0 <= currHfIdx && currHfIdx < segLen
 requires segLen * path.HopLen == len(hopfields)
-requires acc(sl.Bytes(hopfields, 0, len(hopfields)), _)
+requires sl.Bytes(hopfields, 0, len(hopfields))
 requires let currHfStart := currHfIdx * path.HopLen in
-	let currHfEnd := currHfStart + path.HopLen in
-	acc(sl.Bytes(hopfields[:currHfStart], 0, currHfStart), _) &&
-	acc(sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen), _) &&
-	acc(sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen), _)
+	let currHfEnd := currHfStart + path.HopLen      in
+	sl.Bytes(hopfields[:currHfStart], 0, currHfStart)          &&
+	sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen) &&
+	sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen)
 decreases
 pure func BytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf io.AbsInfoField) bool {
 	return let currseg := CurrSegWithInfo(hopfields, currHfIdx, segLen, inf) in
-		let currHfStart := currHfIdx * path.HopLen in
-		let currHfEnd := currHfStart + path.HopLen in
+		let currHfStart := currHfIdx * path.HopLen                           in
+		let currHfEnd := currHfStart + path.HopLen                           in
 		len(currseg.Future) > 0  &&
 		currseg.Future[0] == path.BytesToIO_HF(hopfields[currHfStart:currHfEnd], 0, 0, path.HopLen) &&
-		currseg.Future[1:] == hopFields(hopfields[currHfEnd:], 0, 0, (segLen - currHfIdx - 1)) &&
-		currseg.Past == segPast(hopFields(hopfields[:currHfStart], 0, 0, currHfIdx)) &&
-		currseg.History == segHistory(hopFields(hopfields[:currHfStart], 0, 0, currHfIdx)) &&
-		currseg.AInfo == inf.AInfo &&
-		currseg.UInfo == inf.UInfo &&
+		currseg.Future[1:] == hopFields(hopfields[currHfEnd:], 0, 0, (segLen - currHfIdx - 1))      &&
+		currseg.Past == segPast(hopFields(hopfields[:currHfStart], 0, 0, currHfIdx))                &&
+		currseg.History == segHistory(hopFields(hopfields[:currHfStart], 0, 0, currHfIdx))          &&
+		currseg.AInfo == inf.AInfo     &&
+		currseg.UInfo == inf.UInfo     &&
 		currseg.ConsDir == inf.ConsDir &&
 		currseg.Peer == inf.Peer
 }
diff --git a/pkg/slayers/path/scion/raw.go b/pkg/slayers/path/scion/raw.go
index 259258cd9..05c8f8b48 100644
--- a/pkg/slayers/path/scion/raw.go
+++ b/pkg/slayers/path/scion/raw.go
@@ -628,10 +628,10 @@ func (s *Raw) SetHopField(hop path.HopField, idx int /*@, ghost ubuf []byte @*/)
 
 // IsFirstHop returns whether the current hop is the first hop on the path.
 // @ pure
-// @ requires  acc(s.Mem(ubuf), _)
+// @ requires  s.Mem(ubuf)
 // @ decreases
 func (s *Raw) IsFirstHop( /*@ ghost ubuf []byte @*/ ) bool {
-	return /*@ unfolding acc(s.Mem(ubuf), _) in (unfolding acc(s.Base.Mem(), _) in @*/ s.PathMeta.CurrHF == 0 /*@ ) @*/
+	return /*@ unfolding s.Mem(ubuf) in (unfolding s.Base.Mem() in @*/ s.PathMeta.CurrHF == 0 /*@ ) @*/
 }
 
 // IsPenultimateHop returns whether the current hop is the penultimate hop on the path.
diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra
index f6c718905..09303ba4d 100644
--- a/pkg/slayers/path/scion/raw_spec.gobra
+++ b/pkg/slayers/path/scion/raw_spec.gobra
@@ -42,10 +42,10 @@ pred (s *Raw) Mem(buf []byte) {
 (*Raw) implements path.Path
 
 ghost
-requires  acc(s.Mem(buf), _)
-requires  acc(sl.Bytes(buf, 0, len(buf)), _)
+requires s.Mem(buf)
+requires sl.Bytes(buf, 0, len(buf))
 decreases
-pure func (s *Raw) IsValidResultOfDecoding(buf []byte, err error) (res bool) {
+pure func (s *Raw) IsValidResultOfDecoding(buf []byte, err error) bool {
 	return let base := s.GetBase(buf) in
 		base.EqAbsHeader(buf) &&
 		base.WeaklyValid()
@@ -58,10 +58,11 @@ pure func (s *Raw) IsValidResultOfDecoding(buf []byte, err error) (res bool) {
   * Unfortunately, Gobra does not fully support them yet, so we
   * introduced this wrapper method which acts as a wrapper.
   */
-requires acc(s.Mem(buf), _)
+requires s.Mem(buf)
 decreases
-pure func (s *Raw) Type(ghost buf []byte) (t path.Type) {
-	return unfolding acc(s.Mem(buf), _) in s.Base.Type()
+pure func (s *Raw) Type(ghost buf []byte) path.Type {
+	return unfolding s.Mem(buf) in
+		s.Base.Type()
 }
 
 /**
@@ -78,10 +79,11 @@ func (s *Raw) Len(ghost buf []byte) (l int) {
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
-pure func (s *Raw) LenSpec(ghost ub []byte) (l int) {
-	return unfolding acc(s.Mem(ub), _) in s.Base.Len()
+pure func (s *Raw) LenSpec(ghost ub []byte) int {
+	return unfolding s.Mem(ub) in
+		s.Base.Len()
 }
 
 /**
@@ -145,53 +147,59 @@ func (r *Raw) Widen(ubuf1, ubuf2 []byte) {
 
 /**** Start of helpful pure functions ****/
 ghost
-requires acc(r.Mem(ub), _)
+requires r.Mem(ub)
 decreases
 pure func (r *Raw) GetBase(ub []byte) Base {
-	return unfolding acc(r.Mem(ub), _) in r.Base.GetBase()
+	return unfolding r.Mem(ub) in
+		r.Base.GetBase()
 }
 
 ghost
-requires acc(r.Mem(ub), _)
+requires r.Mem(ub)
 decreases
 pure func (r *Raw) GetNumINF(ghost ub []byte) int {
-	return unfolding acc(r.Mem(ub), _) in (unfolding acc(r.Base.Mem(), _) in r.NumINF)
+	return unfolding r.Mem(ub) in
+		(unfolding r.Base.Mem() in r.NumINF)
 }
 
 ghost
-requires acc(r.Mem(ub), _)
+requires r.Mem(ub)
 decreases
 pure func (r *Raw) GetNumHops(ghost ub []byte) int {
-	return unfolding acc(r.Mem(ub), _) in (unfolding acc(r.Base.Mem(), _) in r.NumHops)
+	return unfolding r.Mem(ub) in
+		(unfolding r.Base.Mem() in r.NumHops)
 }
 
 ghost
-requires acc(r.Mem(ub), _)
+requires r.Mem(ub)
 decreases
 pure func (r *Raw) GetCurrINF(ghost ub []byte) uint8 {
-	return unfolding acc(r.Mem(ub), _) in (unfolding acc(r.Base.Mem(), _) in r.PathMeta.CurrINF)
+	return unfolding r.Mem(ub) in
+		(unfolding r.Base.Mem() in r.PathMeta.CurrINF)
 }
 
 ghost
-requires acc(r.Mem(ub), _)
+requires r.Mem(ub)
 decreases
 pure func (r *Raw) GetCurrHF(ghost ub []byte) uint8 {
-	return unfolding acc(r.Mem(ub), _) in
-		(unfolding acc(r.Base.Mem(), _) in r.PathMeta.CurrHF)
+	return unfolding r.Mem(ub) in
+		(unfolding r.Base.Mem() in r.PathMeta.CurrHF)
 }
 
 ghost
-requires acc(s.Mem(buf), _)
+requires s.Mem(buf)
 decreases
 pure func (s *Raw) RawBufferMem(ghost buf []byte) []byte {
-	return unfolding acc(s.Mem(buf), _) in s.Raw
+	return unfolding s.Mem(buf) in
+		s.Raw
 }
 
 ghost
-requires acc(s.NonInitMem(), _)
+requires s.NonInitMem()
 decreases
 pure func (s *Raw) RawBufferNonInitMem() []byte {
-	return unfolding acc(s.NonInitMem(), _) in s.Raw
+	return unfolding s.NonInitMem() in
+		s.Raw
 }
 /**** End of helpful pure functions ****/
 
@@ -212,7 +220,7 @@ ghost
 requires  0 <= offset
 requires  0 <= currHfIdx && currHfIdx <= segLen
 requires  offset + path.HopLen * segLen <= len(raw)
-requires  acc(sl.Bytes(raw, 0, len(raw)), _)
+requires  sl.Bytes(raw, 0, len(raw))
 ensures   len(res) == segLen - currHfIdx
 decreases segLen - currHfIdx
 pure func hopFields(
@@ -244,11 +252,11 @@ pure func segHistory(hopfields seq[io.IO_HF]) (res seq[io.IO_ahi]) {
 }
 
 ghost
+requires sl.Bytes(raw, 0, len(raw))
 requires 0 <= offset
 requires 0 < segLen
 requires 0 <= currHfIdx && currHfIdx <= segLen
 requires offset + path.HopLen * segLen <= len(raw)
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
 ensures  len(res.Future) == segLen - currHfIdx
 ensures  len(res.History) == currHfIdx
 ensures  len(res.Past) == currHfIdx
@@ -275,13 +283,13 @@ pure func segment(raw []byte,
 
 ghost
 opaque
+requires sl.Bytes(raw, 0, len(raw))
 requires 0 <= headerOffset
 requires path.InfoFieldOffset(currInfIdx, headerOffset) + path.InfoLen <= offset
 requires 0 < segLen
 requires offset + path.HopLen * segLen <= len(raw)
 requires 0 <= currHfIdx && currHfIdx <= segLen
 requires 0 <= currInfIdx && currInfIdx < 3
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
 decreases
 pure func CurrSeg(raw []byte,
 	offset int,
@@ -298,11 +306,11 @@ pure func CurrSeg(raw []byte,
 
 ghost
 opaque
+requires sl.Bytes(raw, 0, len(raw))
 requires 0 <= headerOffset
 requires segs.Valid()
 requires PktLen(segs, headerOffset) <= len(raw)
 requires 1 <= currInfIdx && currInfIdx < 4
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
 decreases
 pure func LeftSeg(
 	raw []byte,
@@ -319,11 +327,11 @@ pure func LeftSeg(
 
 ghost
 opaque
+requires sl.Bytes(raw, 0, len(raw))
 requires 0 <= headerOffset
 requires segs.Valid()
 requires PktLen(segs, headerOffset) <= len(raw)
 requires -1 <= currInfIdx && currInfIdx < 2
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
 decreases
 pure func RightSeg(
 	raw []byte,
@@ -340,11 +348,11 @@ pure func RightSeg(
 
 ghost
 opaque
+requires sl.Bytes(raw, 0, len(raw))
 requires 0 <= headerOffset
 requires segs.Valid()
 requires PktLen(segs, headerOffset) <= len(raw)
 requires 2 <= currInfIdx && currInfIdx < 5
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
 decreases
 pure func MidSeg(
 	raw []byte,
@@ -361,7 +369,7 @@ pure func MidSeg(
 
 ghost
 opaque
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 requires validPktMetaHdr(raw)
 decreases
 pure func (s *Raw) absPkt(raw []byte) (res io.IO_pkt2) {
@@ -387,17 +395,17 @@ pure func (s *Raw) absPkt(raw []byte) (res io.IO_pkt2) {
 
 ghost
 requires MetaLen <= len(raw)
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 decreases
 pure func RawBytesToMetaHdr(raw []byte) MetaHdr {
-	return unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
+	return unfolding sl.Bytes(raw, 0, len(raw)) in
 		let hdr := binary.BigEndian.Uint32(raw[:MetaLen]) in
 		DecodedFrom(hdr)
 }
 
 ghost
 requires MetaLen <= len(raw)
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 decreases
 pure func RawBytesToBase(raw []byte) Base {
 	return let metaHdr := RawBytesToMetaHdr(raw) in
@@ -410,7 +418,7 @@ pure func RawBytesToBase(raw []byte) Base {
 
 ghost
 opaque
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 decreases
 pure func validPktMetaHdr(raw []byte) bool {
 	return MetaLen <= len(raw)  &&
@@ -511,23 +519,23 @@ pure func absIncPathSeg(currseg io.IO_seg3) io.IO_seg3 {
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *Raw) IsLastHopSpec(ub []byte) bool {
-	return unfolding acc(s.Mem(ub), _) in
-		unfolding acc(s.Base.Mem(), _) in
+	return unfolding s.Mem(ub) in
+		unfolding s.Base.Mem() in
 		int(s.PathMeta.CurrHF) == (s.NumHops - 1)
 }
 
 ghost
 opaque
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 requires 0 <= idx && idx < s.GetNumINF(ub)
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires sl.Bytes(ub, 0, len(ub))
 decreases
 pure func (s *Raw) CorrectlyDecodedInfWithIdx(ub []byte, idx int, info path.InfoField) bool {
-	return unfolding acc(s.Mem(ub), _) in
-		unfolding acc(s.Base.Mem(), _) in
+	return unfolding s.Mem(ub) in
+		unfolding s.Base.Mem() in
 		let infOffset := MetaLen + idx*path.InfoLen in
 		infOffset + path.InfoLen <= len(ub) &&
 		info.ToAbsInfoField() ==
@@ -536,13 +544,13 @@ pure func (s *Raw) CorrectlyDecodedInfWithIdx(ub []byte, idx int, info path.Info
 
 ghost
 opaque
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 requires s.GetBase(ub).ValidCurrInfSpec()
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires sl.Bytes(ub, 0, len(ub))
 decreases
 pure func (s *Raw) CorrectlyDecodedInf(ub []byte, info path.InfoField) bool {
-	return unfolding acc(s.Mem(ub), _) in
-		unfolding acc(s.Base.Mem(), _) in
+	return unfolding s.Mem(ub) in
+		unfolding s.Base.Mem() in
 		let infOffset := MetaLen + int(s.Base.PathMeta.CurrINF) * path.InfoLen in
 		infOffset + path.InfoLen <= len(ub) &&
 		info.ToAbsInfoField() ==
@@ -551,13 +559,13 @@ pure func (s *Raw) CorrectlyDecodedInf(ub []byte, info path.InfoField) bool {
 
 ghost
 opaque
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 requires 0 <= idx && idx < s.GetNumHops(ub)
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires sl.Bytes(ub, 0, len(ub))
 decreases
 pure func (s *Raw) CorrectlyDecodedHfWithIdx(ub []byte, idx int, hop path.HopField) bool {
-	return unfolding acc(s.Mem(ub), _) in
-		unfolding acc(s.Base.Mem(), _) in
+	return unfolding s.Mem(ub) in
+		unfolding s.Base.Mem() in
 		let hopOffset := MetaLen + int(s.NumINF) * path.InfoLen + idx * path.HopLen in
 		hopOffset + path.HopLen <= len(ub) &&
 		hop.ToIO_HF() == path.BytesToIO_HF(ub, 0, hopOffset, len(ub))
@@ -565,13 +573,13 @@ pure func (s *Raw) CorrectlyDecodedHfWithIdx(ub []byte, idx int, hop path.HopFie
 
 ghost
 opaque
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 requires s.GetBase(ub).ValidCurrHfSpec()
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires sl.Bytes(ub, 0, len(ub))
 decreases
 pure func (s *Raw) CorrectlyDecodedHf(ub []byte, hop path.HopField) bool {
-	return unfolding acc(s.Mem(ub), _) in
-		unfolding acc(s.Base.Mem(), _) in
+	return unfolding s.Mem(ub) in
+		unfolding s.Base.Mem() in
 		let hopOffset := MetaLen + int(s.NumINF) * path.InfoLen +
 			int(s.Base.PathMeta.CurrHF) * path.HopLen in
 		hopOffset + path.HopLen <= len(ub) &&
@@ -647,8 +655,8 @@ opaque
 decreases
 pure func (s *Raw) EqAbsInfoField(pkt io.IO_pkt2, info io.AbsInfoField) bool {
 	return let currseg := pkt.CurrSeg in
-		info.AInfo == currseg.AInfo &&
-		info.UInfo == currseg.UInfo &&
+		info.AInfo == currseg.AInfo     &&
+		info.UInfo == currseg.UInfo     &&
 		info.ConsDir == currseg.ConsDir &&
 		info.Peer == currseg.Peer
 }
diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra
index f6aac7b92..bd3356b24 100644
--- a/pkg/slayers/scion_spec.gobra
+++ b/pkg/slayers/scion_spec.gobra
@@ -96,27 +96,29 @@ pred PathPoolMemExceptOne(pathPool []path.Path, pathPoolRaw path.Path, pathType
 }
 
 ghost
-requires acc(&s.pathPool, _)
+requires acc(&s.pathPool)
 decreases
 pure func (s *SCION) pathPoolInitialized() bool {
 	return s.pathPool != nil
 }
 
 ghost
-requires acc(s.NonInitMem(), _)
+requires s.NonInitMem()
 decreases
 pure func (s *SCION) PathPoolInitializedNonInitMem() bool {
-	return unfolding acc(s.NonInitMem(), _) in s.pathPool != nil
+	return unfolding s.NonInitMem() in
+		s.pathPool != nil
 }
 
 ghost
 requires 0 <= pathType && pathType < path.MaxPathType
-requires acc(&s.pathPool, _) && acc(&s.pathPoolRaw, _)
+requires acc(&s.pathPool) && acc(&s.pathPoolRaw)
 requires s.pathPool != nil
-requires acc(PathPoolMemExceptOne(s.pathPool, s.pathPoolRaw, pathType), _)
+requires PathPoolMemExceptOne(s.pathPool, s.pathPoolRaw, pathType)
 decreases
 pure func (s *SCION) getPathPure(pathType path.Type) path.Path {
-	return int(pathType) < len(s.pathPool)? (unfolding acc(PathPoolMemExceptOne(s.pathPool, s.pathPoolRaw, pathType), _) in s.pathPool[pathType]) :
+	return int(pathType) < len(s.pathPool)?
+		(unfolding PathPoolMemExceptOne(s.pathPool, s.pathPoolRaw, pathType) in s.pathPool[pathType]) :
 		s.pathPoolRaw
 }
 
@@ -184,10 +186,10 @@ pred (s *SCION) Mem(ubuf []byte) {
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) ValidPathMetaData(ghost ub []byte) bool {
-	return unfolding acc(s.Mem(ub), _) in
+	return unfolding s.Mem(ub) in
 		let ubPath := s.UBPath(ub) in
 		(typeOf(s.Path) == type[*scion.Raw] ==>
 			s.Path.(*scion.Raw).GetBase(ubPath).Valid()) &&
@@ -275,43 +277,45 @@ pure func (a AddrType) Has3Bits() (res bool) {
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) UBPath(ub []byte) []byte {
-	return unfolding acc(s.Mem(ub), _) in
+	return unfolding s.Mem(ub) in
 		ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen]
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) UBScionPath(ub []byte) []byte {
-	return unfolding acc(s.Mem(ub), _) in
+	return unfolding s.Mem(ub) in
 		let ubPath := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
 		typeOf(s.Path) == *epic.Path ?
-			unfolding acc(s.Path.Mem(ubPath), _) in ubPath[epic.MetadataLen:] :
+			unfolding s.Path.Mem(ubPath) in ubPath[epic.MetadataLen:] :
 			ubPath
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) PathStartIdx(ub []byte) int {
-	return unfolding acc(s.Mem(ub), _) in CmnHdrLen+s.AddrHdrLenSpecInternal()
+	return unfolding s.Mem(ub) in
+		CmnHdrLen+s.AddrHdrLenSpecInternal()
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) PathEndIdx(ub []byte) int {
-	return unfolding acc(s.Mem(ub), _) in int(s.HdrLen*LineLen)
+	return unfolding s.Mem(ub) in
+		int(s.HdrLen*LineLen)
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) PathScionStartIdx(ub []byte) int {
-	return unfolding acc(s.Mem(ub), _) in
+	return unfolding s.Mem(ub) in
 		let offset := CmnHdrLen+s.AddrHdrLenSpecInternal() in
 		typeOf(s.Path) == *epic.Path ?
 			offset + epic.MetadataLen :
@@ -319,10 +323,11 @@ pure func (s *SCION) PathScionStartIdx(ub []byte) int {
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) PathScionEndIdx(ub []byte) int {
-	return unfolding acc(s.Mem(ub), _) in int(s.HdrLen*LineLen)
+	return unfolding s.Mem(ub) in
+		int(s.HdrLen*LineLen)
 }
 
 ghost
@@ -338,16 +343,17 @@ func LemmaPathIdxStartEnd(s *SCION, ub []byte, p perm) {
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) GetPath(ub []byte) path.Path {
-	return unfolding acc(s.Mem(ub), _) in s.Path
+	return unfolding s.Mem(ub) in
+		s.Path
 }
 
 ghost
 opaque
-requires acc(s.Mem(ub), _)
-requires acc(sl.Bytes(ub, 0, length), _)
+requires s.Mem(ub)
+requires sl.Bytes(ub, 0, length)
 requires CmnHdrLen <= length
 decreases
 pure func (s *SCION) ValidHeaderOffset(ub []byte, length int) bool {
@@ -397,20 +403,20 @@ func (s *SCION) ValidHeaderOffsetFromSubSliceLemma(ub []byte, length int) {
 
 ghost
 opaque
-requires acc(s.Mem(ub), _)
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires s.Mem(ub)
+requires sl.Bytes(ub, 0, len(ub))
 decreases
 pure func (s *SCION) EqAbsHeader(ub []byte) bool {
-	return unfolding acc(s.Mem(ub), _) in
+	return unfolding s.Mem(ub) in
 		let low := CmnHdrLen+s.AddrHdrLenSpecInternal() in
 		let high := s.HdrLen*LineLen in
-		GetAddressOffset(ub) == low &&
-		GetLength(ub) == int(high)        &&
+		GetAddressOffset(ub) == low  &&
+		GetLength(ub) == int(high)   &&
 		// Might be worth introducing EqAbsHeader as an interface method on Path
 		// to avoid doing these casts, especially when we add support for EPIC.
 		typeOf(s.Path) == (*scion.Raw) &&
-		unfolding acc(s.Path.Mem(ub[low:high]), _) in
-		unfolding acc(sl.Bytes(ub, 0, len(ub)), _) in
+		unfolding s.Path.Mem(ub[low:high]) in
+		unfolding sl.Bytes(ub, 0, len(ub)) in
 		let _ := Asserting(forall k int :: {&ub[low:high][k]} 0 <= k && k < high ==>
 			&ub[low:high][k] == &ub[low + k]) in
 		let _ := Asserting(forall k int :: {&ub[low:high][:scion.MetaLen][k]} 0 <= k && k < scion.MetaLen ==>
@@ -421,16 +427,16 @@ pure func (s *SCION) EqAbsHeader(ub []byte) bool {
 		let seg3 := int(metaHdr.SegLen[2]) in
 		let segs := io.CombineSegLens(seg1, seg2, seg3) in
 		s.Path.(*scion.Raw).Base.GetBase() ==
-		scion.Base{metaHdr, segs.NumInfoFields(), segs.TotalHops()}
+			scion.Base{metaHdr, segs.NumInfoFields(), segs.TotalHops()}
 }
 
 // Describes a SCION packet that was successfully decoded by `DecodeFromBytes`.
 ghost
 opaque
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) ValidScionInitSpec(ub []byte) bool {
-	return unfolding acc(s.Mem(ub), _)                  in
+	return unfolding s.Mem(ub)                          in
 		let low := CmnHdrLen+s.AddrHdrLenSpecInternal() in
 		let high := s.HdrLen*LineLen                    in
 		typeOf(s.Path) == (*scion.Raw) &&
@@ -440,7 +446,7 @@ pure func (s *SCION) ValidScionInitSpec(ub []byte) bool {
 // Checks if the common path header is valid in the serialized scion packet.
 ghost
 opaque
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 decreases
 pure func ValidPktMetaHdr(raw []byte) bool {
 	return CmnHdrLen <= len(raw) &&
@@ -450,7 +456,7 @@ pure func ValidPktMetaHdr(raw []byte) bool {
 		let rawHdr := raw[start:end] in
 		let length := GetLength(raw) in
 		length <= len(raw) &&
-		unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
+		unfolding sl.Bytes(raw, 0, len(raw))       in
 		let _ := Asserting(forall k int :: {&rawHdr[k]} 0 <= k && k < scion.MetaLen ==> &rawHdr[k] == &raw[start + k]) in
 		let hdr := binary.BigEndian.Uint32(rawHdr) in
 		let metaHdr := scion.DecodedFrom(hdr)      in
@@ -466,7 +472,7 @@ pure func ValidPktMetaHdr(raw []byte) bool {
 
 ghost
 opaque
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 decreases
 pure func IsSupportedPkt(raw []byte) bool {
 	return CmnHdrLen <= len(raw) &&
@@ -518,7 +524,7 @@ func (s *SCION) IsSupportedPktLemma(ub []byte, buffer []byte) {
 }
 
 ghost
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires sl.Bytes(ub, 0, len(ub))
 requires CmnHdrLen <= len(ub)
 decreases
 pure func GetAddressOffset(ub []byte) int {
@@ -526,18 +532,18 @@ pure func GetAddressOffset(ub []byte) int {
 }
 
 ghost
-requires acc(sl.Bytes(ub, 0, length), _)
+requires sl.Bytes(ub, 0, length)
 requires CmnHdrLen <= length
 decreases
 pure func GetAddressOffsetWithinLength(ub []byte, length int) int {
-	return unfolding acc(sl.Bytes(ub, 0, length), _) in
+	return unfolding sl.Bytes(ub, 0, length)                  in
 		let dstAddrLen := AddrType(ub[9] >> 4 & 0x7).Length() in
-		let srcAddrLen := AddrType(ub[9] & 0x7).Length() in
+		let srcAddrLen := AddrType(ub[9] & 0x7).Length()      in
 		CmnHdrLen + 2*addr.IABytes + dstAddrLen + srcAddrLen
 }
 
 ghost
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires sl.Bytes(ub, 0, len(ub))
 requires CmnHdrLen <= len(ub)
 decreases
 pure func GetLength(ub []byte) int {
@@ -545,33 +551,36 @@ pure func GetLength(ub []byte) int {
 }
 
 ghost
-requires acc(sl.Bytes(ub, 0, length), _)
+requires sl.Bytes(ub, 0, length)
 requires CmnHdrLen <= length
 decreases
 pure func GetLengthWithinLength(ub []byte, length int) int {
-	return unfolding acc(sl.Bytes(ub, 0, length), _) in int(ub[5])*LineLen
+	return unfolding sl.Bytes(ub, 0, length) in
+		int(ub[5]) * LineLen
 }
 
 ghost
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires sl.Bytes(ub, 0, len(ub))
 requires CmnHdrLen <= len(ub)
 decreases
 pure func GetPathType(ub []byte) int {
-	return unfolding acc(sl.Bytes(ub, 0, len(ub)), _) in int(ub[8])
+	return unfolding sl.Bytes(ub, 0, len(ub)) in
+		int(ub[8])
 }
 
 ghost
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires sl.Bytes(ub, 0, len(ub))
 requires CmnHdrLen <= len(ub)
 decreases
 pure func GetNextHdr(ub []byte) int {
-	return unfolding acc(sl.Bytes(ub, 0, len(ub)), _) in int(ub[4])
+	return unfolding sl.Bytes(ub, 0, len(ub)) in
+		int(ub[4])
 }
 
 ghost
 opaque
-requires acc(s.Mem(ub), _)
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires s.Mem(ub)
+requires sl.Bytes(ub, 0, len(ub))
 decreases
 pure func (s *SCION) EqPathType(ub []byte) bool {
 	return reveal s.EqPathTypeWithBuffer(ub, ub)
@@ -579,44 +588,46 @@ pure func (s *SCION) EqPathType(ub []byte) bool {
 
 ghost
 opaque
-requires acc(s.Mem(ub), _)
-requires acc(sl.Bytes(buffer, 0, len(buffer)), _)
+requires s.Mem(ub)
+requires sl.Bytes(buffer, 0, len(buffer))
 decreases
 pure func (s *SCION) EqPathTypeWithBuffer(ub []byte, buffer []byte) bool {
-	return unfolding acc(s.Mem(ub), _) in
+	return unfolding s.Mem(ub) in
 		CmnHdrLen <= len(buffer) &&
 		path.Type(GetPathType(buffer)) == s.PathType &&
 		L4ProtocolType(GetNextHdr(buffer)) == s.NextHdr
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) GetScionPath(ub []byte) path.Path {
-	return unfolding acc(s.Mem(ub), _) in (
+	return unfolding s.Mem(ub) in (
 	typeOf(s.Path) == *epic.Path ?
 		(let ubPath := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
-			unfolding acc(s.Path.Mem(ubPath), _) in
+			unfolding s.Path.Mem(ubPath) in
 			(path.Path)(s.Path.(*epic.Path).ScionPath)) :
 		s.Path)
 }
 
 ghost
-requires  acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) GetPayloadLen(ghost ub []byte) uint16 {
-	return unfolding acc(s.Mem(ub), _) in s.PayloadLen
+	return unfolding s.Mem(ub) in
+		s.PayloadLen
 }
 
 ghost
-requires  acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) GetPayload(ghost ub []byte) []byte {
-	return unfolding acc(s.Mem(ub), _) in s.Payload
+	return unfolding s.Mem(ub) in
+		s.Payload
 }
 
 ghost
-requires acc(&s.DstAddrType, _) && acc(&s.SrcAddrType, _)
+requires acc(&s.DstAddrType) && acc(&s.SrcAddrType)
 requires s.DstAddrType.Has3Bits() && s.SrcAddrType.Has3Bits()
 ensures  0 <= res
 decreases
@@ -625,12 +636,12 @@ pure func (s *SCION) AddrHdrLenSpecInternal() (res int) {
 }
 
 ghost
-requires acc(s.Mem(ubuf), _)
+requires s.Mem(ubuf)
 ensures  0 <= res
 decreases
 pure func (s *SCION) AddrHdrLenSpec(ubuf []byte) (res int) {
-	return unfolding acc(s.Mem(ubuf), _) in
-		unfolding acc(s.HeaderMem(ubuf[CmnHdrLen:]), _) in
+	return unfolding s.Mem(ubuf) in
+		unfolding s.HeaderMem(ubuf[CmnHdrLen:]) in
 		2*addr.IABytes + s.DstAddrType.Length() + s.SrcAddrType.Length()
 }
 
@@ -699,7 +710,7 @@ ghost
 requires typeOf(a) == *net.IPAddr
 requires acc(&a.(*net.IPAddr).IP, _)
 requires forall i int :: { &a.(*net.IPAddr).IP[i] } 0 <= i && i < len(a.(*net.IPAddr).IP) ==>
-	acc(&a.(*net.IPAddr).IP[i], _)
+	acc(&a.(*net.IPAddr).IP[i])
 requires len(a.(*net.IPAddr).IP) == net.IPv6len
 decreases
 pure func isConvertibleToIPv4(a net.Addr) bool {
@@ -710,7 +721,7 @@ pure func isConvertibleToIPv4(a net.Addr) bool {
 
 ghost
 requires typeOf(a) == *net.IPAddr
-requires acc(&a.(*net.IPAddr).IP, _)
+requires acc(&a.(*net.IPAddr).IP)
 decreases
 pure func isIPv6(a net.Addr) bool {
 	return len(a.(*net.IPAddr).IP) == net.IPv6len
@@ -718,7 +729,7 @@ pure func isIPv6(a net.Addr) bool {
 
 ghost
 requires typeOf(a) == *net.IPAddr
-requires acc(&a.(*net.IPAddr).IP, _)
+requires acc(&a.(*net.IPAddr).IP)
 decreases
 pure func isIPv4(a net.Addr) bool {
 	return len(a.(*net.IPAddr).IP) == net.IPv4len
@@ -743,19 +754,20 @@ decreases
 func EstablishPathPkgMem()
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 decreases
 pure func (s *SCION) HasOneHopPath(ghost ub []byte) bool {
-	return unfolding acc(s.Mem(ub), _) in typeOf(s.Path) == type[*onehop.Path]
+	return unfolding s.Mem(ub) in
+		typeOf(s.Path) == type[*onehop.Path]
 }
 
 ghost
-requires acc(s.Mem(ub), _)
+requires s.Mem(ub)
 requires s.HasOneHopPath(ub)
 ensures  b
 decreases
 pure func (s *SCION) InferSizeOHP(ghost ub []byte) (b bool) {
-	return unfolding acc(s.Mem(ub), _) in
+	return unfolding s.Mem(ub) in
 		let pathSlice := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
 		let pathLen := s.Path.LenSpec(pathSlice) in
 		CmnHdrLen + s.AddrHdrLenSpecInternal() + pathLen <= len(ub)
diff --git a/router/assumptions.gobra b/router/assumptions.gobra
index 6a635c96b..7634e35d6 100644
--- a/router/assumptions.gobra
+++ b/router/assumptions.gobra
@@ -96,10 +96,10 @@ func establishInvalidDstIA()
 
 ghost
 trusted
-requires  acc(err.ErrorMem(), _)
+requires err.ErrorMem()
 decreases err.ErrorMem()
 pure func (err scmpError) IsDuplicableMem() bool {
-	return unfolding acc(err.ErrorMem(), _) in
+	return unfolding err.ErrorMem() in
 		err.Cause.IsDuplicableMem()
 }
 
diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra
index d7dc3a4b4..e1f340217 100644
--- a/router/dataplane_spec.gobra
+++ b/router/dataplane_spec.gobra
@@ -200,72 +200,74 @@ func (d *DataPlane) getForwardingMetrics() {
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) getValForwardingMetrics() map[uint16]forwardingMetrics {
-	return unfolding acc(d.Mem(), _) in d.forwardingMetrics
+	return unfolding d.Mem() in
+		d.forwardingMetrics
 }
 
 ghost
-pure
-requires acc(p.sInit(), _)
+requires p.sInit()
 decreases
-func (p *scionPacketProcessor) getIngressID() uint16 {
-	return unfolding acc(p.sInit(), _) in p.ingressID
+pure func (p *scionPacketProcessor) getIngressID() uint16 {
+	return unfolding p.sInit() in
+		p.ingressID
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) getMacFactory() func() hash.Hash {
-	return unfolding acc(d.Mem(), _) in d.macFactory
+	return unfolding d.Mem() in
+		d.macFactory
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) getDomForwardingMetrics() set[uint16] {
-	return unfolding acc(d.Mem(), _) in
+	return unfolding d.Mem() in
 		d.forwardingMetrics == nil ?
 			set[uint16]{} :
-			(unfolding acc(accForwardingMetrics(d.forwardingMetrics), _) in
+			(unfolding accForwardingMetrics(d.forwardingMetrics) in
 				domain(d.forwardingMetrics))
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) GetDomInternalNextHops() set[uint16] {
-	return unfolding acc(d.Mem(), _) in
+	return unfolding d.Mem() in
 		d.internalNextHops == nil ?
 			set[uint16]{} :
-			(unfolding acc(accAddr(d.internalNextHops), _) in
+			(unfolding accAddr(d.internalNextHops) in
 				domain(d.internalNextHops))
 }
 
 ghost
 opaque
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) getDomExternal() set[uint16] {
-	return unfolding acc(d.Mem(), _) in
+	return unfolding d.Mem() in
 		d.external == nil ?
 			set[uint16]{} :
-			(unfolding acc(accBatchConn(d.external), _) in
+			(unfolding accBatchConn(d.external) in
 				domain(d.external))
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) getDomNeighborIAs() set[uint16] {
-	return unfolding acc(d.Mem(), _) in
+	return unfolding d.Mem() in
 		d.neighborIAs == nil ?
 			set[uint16]{} : domain(d.neighborIAs)
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) getDomLinkTypes() set[uint16] {
 	return unfolding acc(d.Mem(), _) in
@@ -275,7 +277,7 @@ pure func (d *DataPlane) getDomLinkTypes() set[uint16] {
 
 ghost
 opaque
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) WellConfigured() bool {
 	return d.getDomNeighborIAs() == d.getDomExternal() &&
@@ -286,7 +288,7 @@ pure func (d *DataPlane) WellConfigured() bool {
 
 ghost
 opaque
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) PreWellConfigured() bool {
 	return d.getDomNeighborIAs() == d.getDomExternal() &&
@@ -378,17 +380,19 @@ func (d *DataPlane) getRunningMem() {
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) getValSvc() *services {
-	return unfolding acc(d.Mem(), _) in d.svc
+	return unfolding d.Mem() in
+		d.svc
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) SvcsAreSet() bool {
-	return unfolding acc(d.Mem(), _) in d.svc != nil
+	return unfolding d.Mem() in
+		d.svc != nil
 }
 
 ghost
@@ -431,68 +435,76 @@ func (d *DataPlane) getNewPacketProcessorFootprint() {
 type Unit struct{}
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) IsRunning() bool {
-	return unfolding acc(d.Mem(), _) in d.running
+	return unfolding d.Mem() in
+		d.running
 }
 
 ghost
 opaque
-requires acc(d.Mem(), _)
-requires acc(&d.running, _)
+requires d.Mem()
+requires acc(&d.running)
 ensures  d.IsRunning() == d.running
 decreases
 pure func (d *DataPlane) isRunningEq() Unit {
-	return unfolding acc(d.Mem(), _) in Unit{}
+	return unfolding d.Mem() in
+		Unit{}
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) InternalConnIsSet() bool {
-	return unfolding acc(d.Mem(), _) in d.internal != nil
+	return unfolding d.Mem() in
+		d.internal != nil
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) MetricsAreSet() bool {
-	return unfolding acc(d.Mem(), _) in d.Metrics != nil
+	return unfolding d.Mem() in
+		d.Metrics != nil
 }
 
 ghost
 opaque
-requires acc(d.Mem(), _)
-requires acc(&d.internal, _)
+requires d.Mem()
+requires acc(&d.internal)
 ensures  d.InternalConnIsSet() == (d.internal != nil)
 decreases
 pure func (d *DataPlane) internalIsSetEq() Unit {
-	return unfolding acc(d.Mem(), _) in Unit{}
+	return unfolding d.Mem() in
+		Unit{}
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) KeyIsSet() bool {
-	return unfolding acc(d.Mem(), _) in d.macFactory != nil
+	return unfolding d.Mem() in
+		d.macFactory != nil
 }
 
 ghost
 opaque
-requires acc(d.Mem(), _)
-requires acc(&d.macFactory, _)
+requires d.Mem()
+requires acc(&d.macFactory)
 ensures  d.KeyIsSet() == (d.macFactory != nil)
 decreases
 pure func (d *DataPlane) keyIsSetEq() Unit {
-	return unfolding acc(d.Mem(), _) in Unit{}
+	return unfolding d.Mem() in
+		Unit{}
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) LocalIA() addr.IA {
-	return unfolding acc(d.Mem(), _) in d.localIA
+	return unfolding d.Mem() in
+		d.localIA
 }
 
 /**** End of acessor methods to avoid unfolding the Mem predicate of the dataplane so much ****/
@@ -539,10 +551,11 @@ func (s *scmpError) Set(e error) {
 }
 
 ghost
-requires acc(s.Mem(), _)
+requires s.Mem()
 decreases
 pure func (s *scmpError) Get() error {
-	return unfolding acc(s.Mem(), _) in *s
+	return unfolding s.Mem() in
+		*s
 }
 
 ghost
@@ -581,52 +594,59 @@ pred (s* scionPacketProcessor) sInit() {
 // each ghost method on *scionPacketProcessor has, in the name, the state in which it
 // expects to find the packet processor. In the case below, the state `Init` is expected.
 ghost
-requires acc(s.sInit(), _)
+requires s.sInit()
 decreases
 pure func (s* scionPacketProcessor) sInitD() (res *DataPlane) {
-	return unfolding acc(s.sInit(), _) in s.d
+	return unfolding s.sInit() in
+		s.d
 }
 
 ghost
-requires acc(s.sInit(), _)
+requires s.sInit()
 decreases
 pure func (s* scionPacketProcessor) sInitRawPkt() (res []byte) {
-	return unfolding acc(s.sInit(), _) in s.rawPkt
+	return unfolding s.sInit() in
+		s.rawPkt
 }
 
 ghost
-requires acc(s.sInit(), _)
+requires s.sInit()
 decreases
 pure func (s* scionPacketProcessor) sInitPath() (res *scion.Raw) {
-	return unfolding acc(s.sInit(), _) in s.path
+	return unfolding s.sInit() in
+		s.path
 }
 
 ghost
-requires acc(s.sInit(), _)
+requires s.sInit()
 decreases
 pure func (s* scionPacketProcessor) sInitHopField() (res path.HopField) {
-	return unfolding acc(s.sInit(), _) in s.hopField
+	return unfolding s.sInit() in
+		s.hopField
 }
 
 ghost
-requires acc(s.sInit(), _)
+requires s.sInit()
 decreases
 pure func (s* scionPacketProcessor) sInitInfoField() (res path.InfoField) {
-	return unfolding acc(s.sInit(), _) in s.infoField
+	return unfolding s.sInit() in
+		s.infoField
 }
 
 ghost
-requires acc(s.sInit(), _)
+requires s.sInit()
 decreases
 pure func (s* scionPacketProcessor) sInitSegmentChange() (res bool) {
-	return unfolding acc(s.sInit(), _) in s.segmentChange
+	return unfolding s.sInit() in
+		s.segmentChange
 }
 
 ghost
-requires acc(s.sInit(), _)
+requires s.sInit()
 decreases
 pure func (s* scionPacketProcessor) sInitBufferUBuf() (res []byte) {
-	return unfolding acc(s.sInit(), _) in s.buffer.UBuf()
+	return unfolding s.sInit() in
+		s.buffer.UBuf()
 }
 
 /** end spec for newPacketProcessor **/
@@ -699,21 +719,21 @@ func (d *DataPlane) InDomainExternalInForwardingMetrics3(id uint16) {
 }
 
 ghost
-requires acc(&d.forwardingMetrics, _)
-requires acc(accForwardingMetrics(d.forwardingMetrics), _)
+requires acc(&d.forwardingMetrics)
+requires accForwardingMetrics(d.forwardingMetrics)
 decreases
 pure func (d *DataPlane) domainForwardingMetrics() set[uint16] {
-	return unfolding acc(accForwardingMetrics(d.forwardingMetrics), _) in
+	return unfolding accForwardingMetrics(d.forwardingMetrics) in
 		domain(d.forwardingMetrics)
 }
 
 ghost
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) DomainForwardingMetrics() set[uint16] {
-	return unfolding acc(d.Mem(), _) in
+	return unfolding d.Mem() in
 		d.forwardingMetrics != nil ?
-			unfolding acc(accForwardingMetrics(d.forwardingMetrics), _) in
+			unfolding accForwardingMetrics(d.forwardingMetrics) in
 				domain(d.forwardingMetrics) :
 			set[uint16]{}
 }
diff --git a/router/io-spec-lemmas.gobra b/router/io-spec-lemmas.gobra
index d1012543c..15c0d4475 100644
--- a/router/io-spec-lemmas.gobra
+++ b/router/io-spec-lemmas.gobra
@@ -102,28 +102,27 @@ func AbsValidateIngressIDXoverLemma(oldPkt io.IO_pkt2, newPkt io.IO_pkt2, ingres
 
 ghost
 opaque
-requires acc(p.scionLayer.Mem(ub), _)
-requires acc(&p.d, _) && acc(p.d.Mem(), _)
-requires acc(&p.ingressID, _)
+requires p.scionLayer.Mem(ub)
+requires acc(&p.d) && p.d.Mem()
+requires acc(&p.ingressID)
 decreases
 pure func (p *scionPacketProcessor) DstIsLocalIngressID(ub []byte) bool {
-	return (unfolding acc(p.scionLayer.Mem(ub), _) in
-		(unfolding acc(p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]), _) in
-		p.scionLayer.DstIA) == (unfolding acc(p.d.Mem(), _) in p.d.localIA)) ==> p.ingressID != 0
+	return (unfolding p.scionLayer.Mem(ub) in
+		(unfolding p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]) in p.scionLayer.DstIA) == (unfolding p.d.Mem() in p.d.localIA)) ==>
+			p.ingressID != 0
 }
 
 ghost
 opaque
-requires acc(p.scionLayer.Mem(ub), _)
-requires acc(&p.d, _) && acc(p.d.Mem(), _)
-requires acc(&p.ingressID, _)
-requires acc(sl.Bytes(ub, 0, len(ub)), _)
+requires p.scionLayer.Mem(ub)
+requires acc(&p.d) && p.d.Mem()
+requires acc(&p.ingressID)
+requires sl.Bytes(ub, 0, len(ub))
 requires slayers.ValidPktMetaHdr(ub)
 decreases
 pure func (p *scionPacketProcessor) LastHopLen(ub []byte) bool {
-	return (unfolding acc(p.scionLayer.Mem(ub), _) in
-		(unfolding acc(p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]), _) in
-		p.scionLayer.DstIA) == (unfolding acc(p.d.Mem(), _) in p.d.localIA)) ==>
+	return (unfolding p.scionLayer.Mem(ub) in
+		(unfolding p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]) in p.scionLayer.DstIA) == (unfolding p.d.Mem() in p.d.localIA)) ==>
 			len(absPkt(ub).CurrSeg.Future) == 1
 }
 
@@ -153,19 +152,19 @@ func (p* scionPacketProcessor) LocalDstLemma(ub []byte) {
 }
 
 ghost
-requires acc(p.scionLayer.Mem(ub), _)
-requires acc(&p.path, _) && p.path == p.scionLayer.GetPath(ub)
+requires p.scionLayer.Mem(ub)
+requires acc(&p.path) && p.path == p.scionLayer.GetPath(ub)
 decreases
 pure func (p* scionPacketProcessor) GetIsXoverSpec(ub []byte) bool {
 	return let ubPath := p.scionLayer.UBPath(ub) in
-		unfolding acc(p.scionLayer.Mem(ub), _) in
+		unfolding p.scionLayer.Mem(ub)           in
 		p.path.GetBase(ubPath).IsXoverSpec()
 }
 
 ghost
 opaque
-requires acc(&p.d, _) && acc(p.d.Mem(), _)
-requires acc(&p.ingressID, _)
+requires acc(&p.d) && p.d.Mem()
+requires acc(&p.ingressID)
 requires pkt.PathNotFullyTraversed()
 decreases
 pure func (p *scionPacketProcessor) NoBouncingPkt(pkt io.IO_pkt2) bool {
@@ -368,7 +367,7 @@ func (p* scionPacketProcessor) SubSliceAbsPktToAbsPkt(ub []byte, start int, end
 
 ghost
 opaque
-requires acc(&p.hopField, _)
+requires acc(&p.hopField)
 requires pkt.PathNotFullyTraversed()
 decreases
 pure func (p* scionPacketProcessor) EqAbsHopField(pkt io.IO_pkt2) bool {
@@ -379,13 +378,13 @@ pure func (p* scionPacketProcessor) EqAbsHopField(pkt io.IO_pkt2) bool {
 
 ghost
 opaque
-requires acc(&p.infoField, _)
+requires acc(&p.infoField)
 decreases
 pure func (p* scionPacketProcessor) EqAbsInfoField(pkt io.IO_pkt2) bool {
 	return let absInf := p.infoField.ToAbsInfoField() in
-		let currseg := pkt.CurrSeg in
-		absInf.AInfo == currseg.AInfo &&
-		absInf.UInfo == currseg.UInfo &&
+		let currseg := pkt.CurrSeg                    in
+		absInf.AInfo == currseg.AInfo     &&
+		absInf.UInfo == currseg.UInfo     &&
 		absInf.ConsDir == currseg.ConsDir &&
 		absInf.Peer == currseg.Peer
 }
\ No newline at end of file
diff --git a/router/io-spec.gobra b/router/io-spec.gobra
index d76521969..d57819119 100644
--- a/router/io-spec.gobra
+++ b/router/io-spec.gobra
@@ -32,14 +32,14 @@ import (
 
 ghost
 opaque
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 requires slayers.ValidPktMetaHdr(raw)
 decreases
 pure func absPkt(raw []byte) (res io.IO_pkt2) {
 	return let _ := reveal slayers.ValidPktMetaHdr(raw) in
 		let headerOffset := slayers.GetAddressOffset(raw) in
 		let headerOffsetWithMetaLen := headerOffset + scion.MetaLen in
-		let hdr := (unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
+		let hdr := (unfolding sl.Bytes(raw, 0, len(raw)) in
 			binary.BigEndian.Uint32(raw[headerOffset:headerOffset+scion.MetaLen])) in
 		let metaHdr := scion.DecodedFrom(hdr) in
 		let currInfIdx := int(metaHdr.CurrINF) in
@@ -53,20 +53,20 @@ pure func absPkt(raw []byte) (res io.IO_pkt2) {
 		let numINF := segs.NumInfoFields() in
 		let offset := scion.HopFieldOffset(numINF, prevSegLen, headerOffsetWithMetaLen) in
 		io.IO_Packet2 {
-			CurrSeg : scion.CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen),
-			LeftSeg : scion.LeftSeg(raw, currInfIdx + 1, segs, headerOffsetWithMetaLen),
-			MidSeg : scion.MidSeg(raw, currInfIdx + 2, segs, headerOffsetWithMetaLen),
-			RightSeg : scion.RightSeg(raw, currInfIdx - 1, segs, headerOffsetWithMetaLen),
+			CurrSeg: scion.CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen),
+			LeftSeg: scion.LeftSeg(raw, currInfIdx + 1, segs, headerOffsetWithMetaLen),
+			MidSeg: scion.MidSeg(raw, currInfIdx + 2, segs, headerOffsetWithMetaLen),
+			RightSeg: scion.RightSeg(raw, currInfIdx - 1, segs, headerOffsetWithMetaLen),
 		}
 }
 
 ghost
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 ensures val.isIO_val_Unsupported
 ensures val.IO_val_Unsupported_1 == path.ifsToIO_ifs(ingressID)
 decreases
 pure func absIO_val_Unsupported(raw []byte, ingressID uint16) (val io.IO_val) {
-	return io.IO_val(io.IO_val_Unsupported{
+	return io.IO_val(io.IO_val_Unsupported {
 		path.ifsToIO_ifs(ingressID),
 		io.Unit{},
 	})
@@ -74,7 +74,7 @@ pure func absIO_val_Unsupported(raw []byte, ingressID uint16) (val io.IO_val) {
 
 ghost
 opaque
-requires acc(sl.Bytes(raw, 0, len(raw)), _)
+requires sl.Bytes(raw, 0, len(raw))
 ensures val.isIO_val_Pkt2 || val.isIO_val_Unsupported
 decreases
 pure func absIO_val(raw []byte, ingressID uint16) (val io.IO_val) {
@@ -95,7 +95,7 @@ func AbsUnsupportedPktIsUnsupportedVal(raw []byte, ingressID uint16) {
 
 ghost
 requires respr.OutPkt != nil ==>
-	acc(sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)), _)
+	sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt))
 decreases
 pure func absReturnErr(respr processResult) (val io.IO_val) {
 	return respr.OutPkt == nil ? io.IO_val_Unit{} :
@@ -103,14 +103,15 @@ pure func absReturnErr(respr processResult) (val io.IO_val) {
 }
 
 ghost
-requires acc(&d.localIA, _)
+requires acc(&d.localIA)
 decreases
 pure func (d *DataPlane) dpSpecWellConfiguredLocalIA(dp io.DataPlaneSpec) bool {
 	return io.IO_as(d.localIA) == dp.Asid()
 }
 
 ghost
-requires acc(&d.neighborIAs, _) && (d.neighborIAs != nil ==> acc(d.neighborIAs, _))
+requires acc(&d.neighborIAs)
+requires d.neighborIAs != nil ==> acc(d.neighborIAs)
 decreases
 pure func (d *DataPlane) dpSpecWellConfiguredNeighborIAs(dp io.DataPlaneSpec) bool {
 	return forall ifs uint16 :: {ifs in domain(d.neighborIAs)} ifs in domain(d.neighborIAs) ==>
@@ -129,7 +130,8 @@ pure func absLinktype(link topology.LinkType) io.IO_Link {
 }
 
 ghost
-requires acc(&d.linkTypes, _) && (d.linkTypes != nil ==> acc(d.linkTypes, _))
+requires acc(&d.linkTypes)
+requires d.linkTypes != nil ==> acc(d.linkTypes)
 decreases
 pure func (d *DataPlane) dpSpecWellConfiguredLinkTypes(dp io.DataPlaneSpec) bool {
 	return forall ifs uint16 :: {ifs in domain(d.linkTypes)} ifs in domain(d.linkTypes) ==>
@@ -139,10 +141,10 @@ pure func (d *DataPlane) dpSpecWellConfiguredLinkTypes(dp io.DataPlaneSpec) bool
 
 ghost
 opaque
-requires acc(d.Mem(), _)
+requires d.Mem()
 decreases
 pure func (d *DataPlane) DpAgreesWithSpec(dp io.DataPlaneSpec) bool {
-	return unfolding acc(d.Mem(), _) in
+	return unfolding d.Mem() in
 		d.dpSpecWellConfiguredLocalIA(dp)     &&
 		d.dpSpecWellConfiguredNeighborIAs(dp) &&
 		d.dpSpecWellConfiguredLinkTypes(dp)
@@ -198,10 +200,10 @@ func (d *DataPlane) getDomExternalLemma() {
 }
 
 ghost
-requires acc(msg.Mem(), _)
-requires acc(sl.Bytes(msg.GetFstBuffer(), 0, len(msg.GetFstBuffer())), _)
+requires msg.Mem()
+requires sl.Bytes(msg.GetFstBuffer(), 0, len(msg.GetFstBuffer()))
 decreases
 pure func MsgToAbsVal(msg *ipv4.Message, ingressID uint16) (res io.IO_val) {
-	return unfolding acc(msg.Mem(), _) in
+	return unfolding msg.Mem() in
 		absIO_val(msg.Buffers[0], ingressID)
 }
diff --git a/verification/dependencies/bytes/bytes.gobra b/verification/dependencies/bytes/bytes.gobra
index dbfcbc260..667e17534 100644
--- a/verification/dependencies/bytes/bytes.gobra
+++ b/verification/dependencies/bytes/bytes.gobra
@@ -18,8 +18,8 @@ import sl "github.com/scionproto/scion/verification/utils/slices"
 // are the same length and contain the same bytes.
 // A nil argument is equivalent to an empty slice.
 trusted
-requires acc(sl.Bytes(a, 0, len(a)), _)
-requires acc(sl.Bytes(b, 0, len(b)), _)
+requires sl.Bytes(a, 0, len(a))
+requires sl.Bytes(b, 0, len(b))
 decreases
 pure func Equal(a, b []byte) bool {
 	return string(a) == string(b)
diff --git a/verification/dependencies/crypto/cipher/cipher.gobra b/verification/dependencies/crypto/cipher/cipher.gobra
index 1fa8e5ab4..43d4d6656 100644
--- a/verification/dependencies/crypto/cipher/cipher.gobra
+++ b/verification/dependencies/crypto/cipher/cipher.gobra
@@ -25,7 +25,7 @@ type Block interface {
 
 	// BlockSize returns the cipher's block size.
 	pure
-	requires acc(Mem(), _)
+	requires Mem()
 	ensures  0 <= n
 	decreases
 	BlockSize() (n int)
@@ -76,7 +76,7 @@ type BlockMode interface {
 
 	// BlockSize returns the mode's block size.
 	pure
-	requires acc(Mem(), _)
+	requires Mem()
 	ensures  0 <= n
 	decreases
 	BlockSize() (n int)
diff --git a/verification/dependencies/crypto/subtle/constant_time.gobra b/verification/dependencies/crypto/subtle/constant_time.gobra
index 8ecebd1c8..68b411b07 100644
--- a/verification/dependencies/crypto/subtle/constant_time.gobra
+++ b/verification/dependencies/crypto/subtle/constant_time.gobra
@@ -14,11 +14,9 @@ import sl "github.com/scionproto/scion/verification/utils/slices"
 // ConstantTimeCompare returns 1 if the two slices, x and y, have equal contents
 // and 0 otherwise. The time taken is a function of the length of the slices and
 // is independent of the contents.
-requires acc(sl.Bytes(x, 0, len(x)), _)
-requires acc(sl.Bytes(y, 0, len(y)), _)
-// postconditions hidden for now:
-// ensures unfolding sl.Bytes(x, 0, len(x)) in (unfolding sl.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 sl.Bytes(x, 0, len(x)) in (unfolding sl.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 _
+trusted
+requires sl.Bytes(x, 0, len(x))
+requires sl.Bytes(y, 0, len(y))
+ensures  len(x) != len(y) ==> res == 0
+decreases
 pure func ConstantTimeCompare(x, y []byte) (res int)
diff --git a/verification/dependencies/encoding/binary/binary.gobra b/verification/dependencies/encoding/binary/binary.gobra
index af43eb984..d4e99283a 100644
--- a/verification/dependencies/encoding/binary/binary.gobra
+++ b/verification/dependencies/encoding/binary/binary.gobra
@@ -12,18 +12,18 @@ package binary
 // A ByteOrder specifies how to convert byte sequences into
 // 16-, 32-, or 64-bit unsigned integers.
 type ByteOrder interface {
-	requires acc(&b[0], _) && acc(&b[1], _)
+	requires acc(&b[0]) && acc(&b[1])
 	ensures res >= 0
 	decreases
 	pure Uint16(b []byte) (res uint16)
 
-	requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _)
+	requires acc(&b[0]) && acc(&b[1]) && acc(&b[2]) && acc(&b[3])
 	ensures res >= 0
 	decreases
 	pure Uint32(b []byte) (res uint32)
 
-	requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _)
-	requires acc(&b[4], _) && acc(&b[5], _) && acc(&b[6], _) && acc(&b[7], _)
+	requires acc(&b[0]) && acc(&b[1]) && acc(&b[2]) && acc(&b[3])
+	requires acc(&b[4]) && acc(&b[5]) && acc(&b[6]) && acc(&b[7])
 	ensures res >= 0
 	decreases
 	pure Uint64(b []byte) (res uint64)
@@ -62,7 +62,7 @@ type bigEndian int
 (bigEndian) implements ByteOrder
 
 trusted // related to https://github.com/viperproject/gobra/issues/192
-requires acc(&b[0], _) && acc(&b[1], _)
+requires acc(&b[0]) && acc(&b[1])
 ensures res >= 0
 decreases
 pure func (e littleEndian) Uint16(b []byte) (res uint16) {
@@ -77,7 +77,7 @@ func (e littleEndian) PutUint16(b []byte, v uint16) {
 }
 
 trusted // related to https://github.com/viperproject/gobra/issues/192
-requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _)
+requires acc(&b[0]) && acc(&b[1]) && acc(&b[2]) && acc(&b[3])
 ensures  0 <= res
 ensures  res == uint32(b[0]) | uint32(b[1])<<8 | uint32(b[2])<<16 | uint32(b[3])<<24
 decreases
@@ -95,8 +95,8 @@ func (e littleEndian) PutUint32(b []byte, v uint32) {
 }
 
 trusted // related to https://github.com/viperproject/gobra/issues/192
-requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _)
-requires acc(&b[4], _) && acc(&b[5], _) && acc(&b[6], _) && acc(&b[7], _)
+requires acc(&b[0]) && acc(&b[1]) && acc(&b[2]) && acc(&b[3])
+requires acc(&b[4]) && acc(&b[5]) && acc(&b[6]) && acc(&b[7])
 ensures res >= 0
 decreases
 pure func (e littleEndian) Uint64(b []byte) (res uint64) {
@@ -134,7 +134,7 @@ pure func (e bigEndian) Uint16Spec(b0, b1 byte) (res uint16) {
 }
 
 trusted // related to https://github.com/viperproject/gobra/issues/192
-requires acc(&b[0], _) && acc(&b[1], _)
+requires acc(&b[0]) && acc(&b[1])
 ensures  res >= 0
 ensures  res == BigEndian.Uint16Spec(b[0], b[1])
 decreases
@@ -167,7 +167,7 @@ pure func (e bigEndian) Uint32Spec(b0, b1, b2, b3 byte) (res uint32) {
 }
 
 trusted // related to https://github.com/viperproject/gobra/issues/192
-requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _)
+requires acc(&b[0]) && acc(&b[1]) && acc(&b[2]) && acc(&b[3])
 ensures  0 <= res
 ensures  res == BigEndian.Uint32Spec(b[0], b[1], b[2], b[3])
 decreases
@@ -197,8 +197,8 @@ func (e bigEndian) PutUint32(b []byte, v uint32) {
 }
 
 trusted // related to https://github.com/viperproject/gobra/issues/192
-requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _)
-requires acc(&b[4], _) && acc(&b[5], _) && acc(&b[6], _) && acc(&b[7], _)
+requires acc(&b[0]) && acc(&b[1]) && acc(&b[2]) && acc(&b[3])
+requires acc(&b[4]) && acc(&b[5]) && acc(&b[6]) && acc(&b[7])
 ensures  res >= 0
 decreases
 pure func (e bigEndian) Uint64(b []byte) (res uint64) {
diff --git a/verification/dependencies/github.com/google/gopacket/layertype.gobra b/verification/dependencies/github.com/google/gopacket/layertype.gobra
index 10989d675..9afc2f935 100644
--- a/verification/dependencies/github.com/google/gopacket/layertype.gobra
+++ b/verification/dependencies/github.com/google/gopacket/layertype.gobra
@@ -48,7 +48,7 @@ pred LayerTypesMem() {
 }
 
 ghost
-requires acc(LayerTypesMem(), _)
+requires LayerTypesMem()
 decreases
 pure func Registered(t LayerType) (res bool) {
 	return unfolding acc(LayerTypesMem(), _) in
@@ -56,14 +56,22 @@ pure func Registered(t LayerType) (res bool) {
 }
 
 ghost
-requires acc(&ltMeta, _) && acc(&ltMetaMap, _) && acc(ltMetaMap, _) && acc(&DecodersByLayerName, _) && acc(DecodersByLayerName, _)
+requires acc(&ltMeta)         &&
+	acc(&ltMetaMap)           &&
+	acc(ltMetaMap)            &&
+	acc(&DecodersByLayerName) &&
+	acc(DecodersByLayerName)
 decreases
 pure func registeredDuringInit(t LayerType) (res bool) {
 	return (0 <= t && t < MaxLayerType? ltMeta[t].inUse : (t in domain(ltMetaMap) && ltMetaMap[t].inUse))
 }
 
 // cannot be made ghost, even though it is morally so
-requires acc(&ltMeta) && acc(&ltMetaMap) && acc(ltMetaMap) && acc(&DecodersByLayerName, _) && acc(DecodersByLayerName)
+requires acc(&ltMeta) &&
+	acc(&ltMetaMap)   &&
+	acc(ltMetaMap)    &&
+	acc(&DecodersByLayerName, _) &&
+	acc(DecodersByLayerName)
 requires forall t LayerType :: { registeredDuringInit(t) } !registeredDuringInit(t)
 ensures  LayerTypesMem()
 ensures  forall t LayerType :: { Registered(t) } !Registered(t)
diff --git a/verification/dependencies/github.com/prometheus/client_golang/prometheus/lemmas.gobra b/verification/dependencies/github.com/prometheus/client_golang/prometheus/lemmas.gobra
index b7ccc9566..9fb025918 100644
--- a/verification/dependencies/github.com/prometheus/client_golang/prometheus/lemmas.gobra
+++ b/verification/dependencies/github.com/prometheus/client_golang/prometheus/lemmas.gobra
@@ -22,7 +22,7 @@ type Unit struct{}
 // even though the precondition morally implies it. This should be
 // fixed by PR #536 of Gobra.
 ghost
-requires  acc(c.Mem(), _)
+requires  c.Mem()
 ensures   c != nil
 decreases _
 pure func CounterMemImpliesNonNil(c Counter) Unit
\ No newline at end of file
diff --git a/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra
index 1684e668a..bd016a51c 100644
--- a/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra
+++ b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra
@@ -60,54 +60,61 @@ pred (m *Message) Mem() {
 }
 
 ghost
-requires acc(m.Mem(), _)
+requires m.Mem()
 decreases
 pure func (m *Message) HasWildcardPermAddr() bool {
-	return unfolding acc(m.Mem(), _) in m.WildcardPerm
+	return unfolding m.Mem() in
+		m.WildcardPerm
 }
 
 ghost
-requires acc(m.Mem(), _)
+requires m.Mem()
 decreases
 pure func (m *Message) HasActiveAddr() bool {
-	return unfolding acc(m.Mem(), _) in m.IsActive
+	return unfolding m.Mem() in
+		m.IsActive
 }
 
 ghost
-requires acc(m.Mem(), _)
+requires m.Mem()
 decreases
 pure func (m *Message) GetAddr() net.Addr {
-	return unfolding acc(m.Mem(), _) in m.Addr
+	return unfolding m.Mem() in
+		m.Addr
 }
 
 ghost
-requires acc(m.Mem(), _)
+requires m.Mem()
 decreases
 pure func (m *Message) GetMessage() Message {
-	return unfolding acc(m.Mem(), _) in *m
+	return unfolding m.Mem() in
+		*m
 }
 
 
 ghost
-requires acc(m.Mem(), _)
+requires m.Mem()
 decreases
 pure func (m *Message) GetBuffer() []byte {
-	return unfolding acc(m.Mem(), _) in m.Buffers[0]
+	return unfolding m.Mem() in
+		m.Buffers[0]
 }
 
 ghost
-requires acc(m.Mem(), _)
+requires m.Mem()
 decreases
 pure func (m *Message) GetFstBuffer() []byte {
-	return unfolding acc(m.Mem(), _) in m.Buffers[0]
+	return unfolding m.Mem() in
+		m.Buffers[0]
 }
 
 ghost
-requires acc(m.Mem(), _)
+requires m.Mem()
 ensures  0 <= res
 decreases
 pure func (m *Message) GetN() (res int) {
-	return unfolding acc(m.Mem(), _) in m.N
+	return unfolding m.Mem() in
+		m.N
 }
 
 // This function establishes the injectivity of the underlying buffers across
diff --git a/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra b/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra
index b32881ddc..4e309ee71 100644
--- a/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra
+++ b/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra
@@ -83,8 +83,9 @@ decreases _
 func NewPacketConn(c net.PacketConn) (p *PacketConn)
 
 ghost
-requires acc(p.Mem(), _)
-decreases _
+trusted
+requires p.Mem()
+decreases
 pure func (p *PacketConn) GetUnderlyingConn() (c net.PacketConn)
 
 ghost
diff --git a/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra b/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra
index 85061a9e9..5d817ce56 100644
--- a/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra
+++ b/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra
@@ -86,8 +86,9 @@ decreases _
 func NewPacketConn(c net.PacketConn) (p *PacketConn)
 
 ghost
-requires acc(p.Mem(), _)
-decreases _
+trusted
+requires p.Mem()
+decreases
 pure func (p *PacketConn) GetUnderlyingConn() (c net.PacketConn)
 
 ghost
diff --git a/verification/dependencies/math/big/int.gobra b/verification/dependencies/math/big/int.gobra
index 213fabcaf..688e65f5a 100644
--- a/verification/dependencies/math/big/int.gobra
+++ b/verification/dependencies/math/big/int.gobra
@@ -44,13 +44,14 @@ func (x *Int) Uint64() (res uint64)
 
 // TODO: This returns int when it should return a mathematical Integer
 ghost
-requires acc(i.Mem(), _)
+requires i.Mem()
 decreases
 pure func (i *Int) toInt() int {
-	return (unfolding acc(i.Mem(), _) in i.neg) ? -((unfolding acc(i.Mem(), _) in i.abs.toInt())) : (unfolding acc(i.Mem(), _) in i.abs.toInt())
+	return (unfolding i.Mem() in i.neg) ? -((unfolding i.Mem() in i.abs.toInt())) : (unfolding i.Mem() in i.abs.toInt())
 }
 
 // TODO: This returns int when it should return a mathematical Integer
 ghost
+trusted
 decreases
 pure func toInt(n uint64) int
diff --git a/verification/dependencies/math/big/nat.gobra b/verification/dependencies/math/big/nat.gobra
index 0ddce1b55..5f1531124 100644
--- a/verification/dependencies/math/big/nat.gobra
+++ b/verification/dependencies/math/big/nat.gobra
@@ -30,17 +30,17 @@ pred (n nat) Mem() {
 
 // TODO: This returns int when it should return a mathematical Integer
 ghost
-requires acc(n.Mem(), _)
+requires n.Mem()
 decreases
 pure func (n nat) toInt() int {
-	return len(n) == 0 ? int(0) : unfolding acc(n.Mem(), _) in toIntHelper(n, 0)
+	return len(n) == 0 ? int(0) : unfolding n.Mem() in toIntHelper(n, 0)
 }
 
 // TODO: This returns int when it should return a mathematical Integer
 ghost
-requires acc(n, _)
+requires acc(n)
 requires 0 <= i && i < len(n)
-decreases _
+decreases len(n) - i
 pure func toIntHelper (n nat, i int) int {
 	return i == len(n) - 1 ? int(n[i]) : int(n[i]) + _W * toIntHelper(n, i + 1)
 }
diff --git a/verification/dependencies/net/ip.gobra b/verification/dependencies/net/ip.gobra
index e94298261..384edf59a 100644
--- a/verification/dependencies/net/ip.gobra
+++ b/verification/dependencies/net/ip.gobra
@@ -84,7 +84,7 @@ func (ip IP) To4(ghost wildcard bool) (res IP) {
 	return nil
 }
 
-preserves forall i int :: { &s[i] } 0 <= i && i < len(s) ==> acc(&s[i], _)
+preserves forall i int :: { &s[i] } 0 <= i && i < len(s) ==> acc(&s[i])
 decreases
 pure func isZeros(s []byte) bool
 
@@ -131,8 +131,8 @@ func (ip *IP) UnmarshalText(text []byte) error
 // An IPv4 address and that same address in IPv6 form are
 // considered to be equal.
 // (VerifiedSCION) we consider this function to be morally pure
-requires acc(sl.Bytes(ip, 0, len(ip)), _)
-requires acc(sl.Bytes(x, 0, len(x)), _)
+requires sl.Bytes(ip, 0, len(ip))
+requires sl.Bytes(x, 0, len(x))
 decreases _
 pure func (ip IP) Equal(x IP) bool
 
diff --git a/verification/dependencies/strings/strings.gobra b/verification/dependencies/strings/strings.gobra
index 91d8aa7f9..521896b3e 100644
--- a/verification/dependencies/strings/strings.gobra
+++ b/verification/dependencies/strings/strings.gobra
@@ -86,7 +86,7 @@ func Fields(s string) (res []string)
 
 // Join concatenates the elements of its first argument to create a single string. The separator
 // string sep is placed between elements in the resulting string.
-requires forall i int :: { &elems[i] } 0 <= i && i < len(elems) ==> acc(&elems[i], _)
+requires forall i int :: { &elems[i] } 0 <= i && i < len(elems) ==> acc(&elems[i])
 ensures len(elems) == 0 ==> res == ""
 ensures len(elems) == 1 ==> res == elems[0]
 // (VerifiedSCION) Leads to precondition of call might not hold (permission to elems[i] might not suffice)
diff --git a/verification/dependencies/sync/mutex.gobra b/verification/dependencies/sync/mutex.gobra
index 7b18c6566..43d512598 100644
--- a/verification/dependencies/sync/mutex.gobra
+++ b/verification/dependencies/sync/mutex.gobra
@@ -15,25 +15,30 @@ pred (m *Mutex) LockP()
 pred (m *Mutex) UnlockP()
 
 ghost
-requires acc(m.LockP(), _)
-decreases _
+trusted
+requires m.LockP()
+decreases
 pure func (m *Mutex) LockInv() pred()
 
 ghost
+trusted
 requires inv() && acc(m) && *m == Mutex{}
 ensures m.LockP() && m.LockInv() == inv
 decreases
 func (m *Mutex) SetInv(ghost inv pred())
 
 ghost
-decreases _
+trusted
+decreases
 pure func IgnoreBlockingForTermination() bool
 
+trusted
 requires acc(m.LockP(), _)
 ensures  m.LockP() && m.UnlockP() && m.LockInv()()
 decreases _ if IgnoreBlockingForTermination()
 func (m *Mutex) Lock()
 
+trusted
 requires acc(m.LockP(), _) && m.UnlockP() && m.LockInv()()
 ensures m.LockP()
 decreases _
diff --git a/verification/dependencies/syscall/syscall_unix.gobra b/verification/dependencies/syscall/syscall_unix.gobra
index f11d78947..6c88fa6bd 100644
--- a/verification/dependencies/syscall/syscall_unix.gobra
+++ b/verification/dependencies/syscall/syscall_unix.gobra
@@ -64,10 +64,11 @@ func (s *Errno) Set(e error) {
 }
 
 ghost
-requires acc(s.Mem(), _)
+requires s.Mem()
 decreases
 pure func (s *Errno) Get() error {
-	return unfolding acc(s.Mem(), _) in *s
+	return unfolding s.Mem() in
+		*s
 }
 
 ghost
diff --git a/verification/utils/slices/slices.gobra b/verification/utils/slices/slices.gobra
index d0f4dd885..8d1b1a524 100644
--- a/verification/utils/slices/slices.gobra
+++ b/verification/utils/slices/slices.gobra
@@ -32,11 +32,11 @@ pred Bytes(s []byte, start int, end int) {
 	forall i int :: { &s[i] } start <= i && i < end ==> acc(&s[i])
 }
 
-requires acc(Bytes(s, start, end), _)
+requires Bytes(s, start, end)
 requires start <= i && i < end
 decreases
 pure func GetByte(s []byte, start int, end int, i int) byte {
-	return unfolding acc(Bytes(s, start, end), _) in s[i]
+	return unfolding Bytes(s, start, end) in s[i]
 }
 
 ghost