diff --git a/pkg/slayers/path/empty/empty.go b/pkg/slayers/path/empty/empty.go
index 8b299de08..d39e0328e 100644
--- a/pkg/slayers/path/empty/empty.go
+++ b/pkg/slayers/path/empty/empty.go
@@ -57,8 +57,14 @@ func RegisterPath() {
 // bytes on the wire and is used for AS internal communication.
 type Path struct{}
 
-// @ ensures  len(r) == 0 ==> (e == nil && o.Mem())
-// @ ensures  len(r) != 0 ==> (e != nil && e.ErrorMem() && o.NonInitMem())
+// @ ensures  len(r) == 0 ==> (
+// @ 	e == nil &&
+// @ 	o.Mem()  &&
+// @ 	o.Valid(r))
+// @ ensures  len(r) != 0 ==> (
+// @ 	e != nil     &&
+// @ 	e.ErrorMem() &&
+// @ 	o.NonInitMem())
 // @ decreases
 func (o Path) DecodeFromBytes(r []byte) (e error) {
 	if len(r) != 0 {
@@ -71,29 +77,27 @@ func (o Path) DecodeFromBytes(r []byte) (e error) {
 
 // @ ensures e == nil
 // @ decreases
-func (o Path) SerializeTo(b []byte /*@, underlyingBuf []byte @*/) (e error) {
+func (o Path) SerializeTo(b []byte /*@, ghost ub []byte @*/) (e error) {
 	return nil
 }
 
-// @ requires o.Mem()
-// @ ensures  p == o
-// @ ensures  p.Mem()
-// @ ensures  e == nil
+// @ ensures   p == o
+// @ ensures   e == nil
 // @ decreases
-func (o Path) Reverse( /*@ ub []byte @*/ ) (p path.Path, e error) {
+func (o Path) Reverse( /*@ ghost ub []byte @*/ ) (p path.Path, e error) {
 	return o, nil
 }
 
 // @ pure
 // @ ensures 0 <= r
 // @ decreases
-func (o Path) Len( /*@ underlyingBuf []byte @*/ ) (r int) {
+func (o Path) Len( /*@ ghost ub []byte @*/ ) (r int) {
 	return PathLen
 }
 
 // @ pure
 // @ ensures r == PathType
 // @ decreases
-func (o Path) Type( /*@ underlyingBuf []byte @*/ ) (r path.Type) {
+func (o Path) Type( /*@ ghost ub []byte @*/ ) (r path.Type) {
 	return PathType
 }
diff --git a/pkg/slayers/path/empty/empty_spec.gobra b/pkg/slayers/path/empty/empty_spec.gobra
index d0ee35b88..0bd49a6b2 100644
--- a/pkg/slayers/path/empty/empty_spec.gobra
+++ b/pkg/slayers/path/empty/empty_spec.gobra
@@ -27,14 +27,12 @@ pred (e Path) Mem() { true }
 pred (e Path) NonInitMem() { true }
 
 ghost
-requires acc(e.Mem(), _)
 decreases
 pure func (e Path) Valid(ghost ub []byte) bool {
 	return len(ub) == 0
 }
 
 ghost
-requires e.Mem()
 ensures  e.NonInitMem()
 decreases
 func (e Path) DowngradePerm(buf []byte) {
@@ -49,8 +47,16 @@ pred (e *Path) Mem() { acc(e) }
 pred (e *Path) NonInitMem() { acc(e) }
 
 ghost
-requires acc(e.Mem(), _)
 decreases
 pure func (e *Path) Valid(ghost ub []byte) bool {
 	return len(ub) == 0
+}
+
+ghost
+requires e.Mem()
+ensures  e.NonInitMem()
+decreases
+func (e *Path) DowngradePerm(buf []byte) {
+	unfold e.Mem()
+	fold e.NonInitMem()
 }
\ No newline at end of file
diff --git a/pkg/slayers/path/path.go b/pkg/slayers/path/path.go
index c12ea2141..77ed74448 100644
--- a/pkg/slayers/path/path.go
+++ b/pkg/slayers/path/path.go
@@ -74,7 +74,7 @@ type Path interface {
 	//@ ghost
 	//@ requires acc(Mem(), _)
 	//@ decreases
-	//@ pure Valid(ghost ub []byte) bool
+	//@ pure Valid(ghost ub []byte) bool // TODO: rename to 'DecodedFrom'
 
 	// SerializeTo serializes the path into the provided buffer.
 	// (VerifiedSCION) There are implementations of this interface that modify the underlying
@@ -98,20 +98,20 @@ type Path interface {
 	//@ requires  Mem() && Valid(ub)
 	//@ preserves sl.AbsSlice_Bytes(ub, 0, len(ub))
 	//@ ensures   e == nil ==> p != nil
-	//@ ensures   e == nil ==> p.Mem()
+	//@ ensures   e == nil ==> p.Mem() && p.Valid(ub)
 	//@ ensures   e != nil ==> e.ErrorMem()
 	//@ decreases
 	Reverse( /*@ ghost ub []byte @*/ ) (p Path, e error)
 	// Len returns the length of a path in bytes.
 	// TODO: make this impure and use LenSpec
 	//@ pure
-	//@ requires acc(Mem(), _)
+	//@ requires acc(Mem(), _) // TODO: do we need Valid?
 	//@ ensures  l >= 0
 	//@ decreases
 	Len( /*@ ghost underlyingBuf []byte @*/ ) (l int) // TODO: drop param
 	// Type returns the type of a path.
 	//@ pure
-	//@ requires acc(Mem(), _)
+	//@ requires acc(Mem(), _) // TODO: do we need Valid?
 	//@ decreases
 	Type( /*@ ghost underlyingBuf []byte @*/ ) Type // TODO: drop param