diff --git a/pkg/slayers/path/scion/raw.go b/pkg/slayers/path/scion/raw.go
index 2772de12a..4d38b812b 100644
--- a/pkg/slayers/path/scion/raw.go
+++ b/pkg/slayers/path/scion/raw.go
@@ -234,11 +234,18 @@ func (s *Raw) ToDecoded( /*@ ghost ubuf []byte @*/ ) (d *Decoded, err error) {
 // @ ensures  r != nil ==> s.NonInitMem()
 // @ ensures  r != nil ==> r.ErrorMem()
 // post for IO:
-// @ ensures  r == nil ==> s.GetBase(ubuf).EqAbsHeader(ubuf) && validPktMetaHdr(ubuf)
+// @ ensures  r == nil ==>
+// @ 	s.GetBase(ubuf).EqAbsHeader(ubuf) && validPktMetaHdr(ubuf)
 // @ ensures  r == nil && old(s.GetBase(ubuf).IsXoverSpec()) ==>
 // @ 	s.absPkt(ubuf) == AbsXover(old(s.absPkt(ubuf)))
 // @ ensures  r == nil && !old(s.GetBase(ubuf).IsXoverSpec()) ==>
 // @ 	s.absPkt(ubuf) == AbsIncPath(old(s.absPkt(ubuf)))
+// (VerifiedSCION) the following post is technically redundant,
+// as it conveys information that could, in principle, be conveyed
+// with the previous posts. We should at some point revisit all
+// abstractions we use for paths and potentially unify them.
+// @ ensures  r == nil ==>
+// @ 	s.GetBase(ubuf) == old(s.GetBase(ubuf).IncPathSpec())
 // @ decreases
 func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) {
 	//@ unfold s.Mem(ubuf)
diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra
index a02bbc7e1..35d836dac 100644
--- a/pkg/slayers/path/scion/raw_spec.gobra
+++ b/pkg/slayers/path/scion/raw_spec.gobra
@@ -290,13 +290,16 @@ requires 0 < segLen
 requires offset + path.HopLen * segLen <= len(raw)
 requires 0 <= currHfIdx && currHfIdx <= segLen
 requires 0 <= currInfIdx && currInfIdx < 3
+ensures  len(res.Future) == segLen - currHfIdx
+ensures  len(res.History) == currHfIdx
+ensures  len(res.Past) == currHfIdx
 decreases
 pure func CurrSeg(raw []byte,
 	offset int,
 	currInfIdx int,
 	currHfIdx int,
 	segLen int,
-	headerOffset int) io.IO_seg3 {
+	headerOffset int) (res io.IO_seg3) {
 	return let ainfo := path.Timestamp(raw, currInfIdx, headerOffset) in
 		let consDir := path.ConsDir(raw, currInfIdx, headerOffset) in
 		let peer := path.Peer(raw, currInfIdx, headerOffset) in
@@ -621,6 +624,8 @@ preserves validPktMetaHdr(ubuf)
 preserves s.GetBase(ubuf).EqAbsHeader(ubuf)
 ensures   s.absPkt(ubuf).LeftSeg != none[io.IO_seg2]
 ensures   len(s.absPkt(ubuf).CurrSeg.Future) == 1
+ensures   len(get(s.absPkt(ubuf).LeftSeg).Future) > 0
+ensures   len(get(s.absPkt(ubuf).LeftSeg).History) == 0
 decreases
 func (s *Raw) XoverLemma(ubuf []byte) {
 	reveal validPktMetaHdr(ubuf)
@@ -640,6 +645,8 @@ func (s *Raw) XoverLemma(ubuf []byte) {
 	assert pkt.LeftSeg == reveal LeftSeg(ubuf, currInfIdx + 1, segs, MetaLen)
 	assert len(pkt.CurrSeg.Future) == 1
 	assert pkt.LeftSeg != none[io.IO_seg2]
+	assert len(get(s.absPkt(ubuf).LeftSeg).History) == 0
+	assert len(get(pkt.LeftSeg).Future) > 0
 }
 
 ghost
diff --git a/router/dataplane.go b/router/dataplane.go
index 3e6325c66..29d4211a6 100644
--- a/router/dataplane.go
+++ b/router/dataplane.go
@@ -3115,8 +3115,8 @@ func (p *scionPacketProcessor) processEgress( /*@ ghost ub []byte @*/ ) (reserr
 // @ 	let ubPath := p.scionLayer.UBPath(ub)   in
 // @ 	(unfolding acc(p.scionLayer.Mem(ub), _) in
 // @ 	p.path === p.scionLayer.GetPath(ub) &&
-// @ 	p.path.GetBase(ubPath) == currBase.IncPathSpec() &&
-// @ 	currBase.IncPathSpec().Valid())
+// @ 	p.path.GetBase(ubPath) == currBase.IncPathSpec())
+// @ ensures  reserr == nil ==> currBase.IncPathSpec().Valid()
 // @ ensures  reserr == nil ==>
 // @ 	p.scionLayer.ValidPathMetaData(ub) == old(p.scionLayer.ValidPathMetaData(ub))
 // @ decreases
@@ -3131,14 +3131,19 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost currBase scio
 	// @ sl.SplitByIndex_Bytes(ub, 0, startP, slayers.CmnHdrLen, R54)
 	// @ sl.Reslice_Bytes(ub, 0, slayers.CmnHdrLen, R54)
 	// @ slayers.IsSupportedPktSubslice(ub, slayers.CmnHdrLen)
+	// @ assert p.path == p.scionLayer.GetPath(ub)
 	// @ p.AbsPktToSubSliceAbsPkt(ub, startP, endP)
+	// @ assert p.path == p.scionLayer.GetPath(ub)
 	// @ p.scionLayer.ValidHeaderOffsetToSubSliceLemma(ub, startP)
+	// @ ghost preAbsPkt := p.path.absPkt(ubPath)
 	// @ p.path.XoverLemma(ubPath)
 	// @ reveal p.EqAbsInfoField(absPkt(ub))
 	// @ reveal p.EqAbsHopField(absPkt(ub))
 	// @ sl.SplitRange_Bytes(ub, startP, endP, HalfPerm)
 	// @ reveal p.scionLayer.ValidHeaderOffset(ub, startP)
 	// @ unfold acc(p.scionLayer.Mem(ub), R55)
+	// @ assert p.path.GetBase(ubPath) == currBase
+	// @ ghost nextBase := currBase.IncPathSpec()
 	if err := p.path.IncPath( /*@ ubPath @*/ ); err != nil {
 		// TODO parameter problem invalid path
 		// (VerifiedSCION) we currently expose a lot of internal information from slayers here. Can we avoid it?
@@ -3150,18 +3155,28 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost currBase scio
 		// @ fold p.scionLayer.NonInitMem()
 		return processResult{}, serrors.WrapStr("incrementing path", err)
 	}
+	// @ assert p.path.GetBase(ubPath) == nextBase
+	// @ assert p.path.absPkt(ubPath) == scion.AbsXover(preAbsPkt)
 	// @ fold acc(p.scionLayer.Mem(ub), R55)
 	// @ assert reveal p.scionLayer.ValidHeaderOffset(ub, startP)
 	// @ ghost sl.CombineRange_Bytes(ub, startP, endP, HalfPerm)
 	// @ slayers.IsSupportedPktSubslice(ub, slayers.CmnHdrLen)
 	// @ sl.Unslice_Bytes(ub, 0, slayers.CmnHdrLen, R54)
 	// @ sl.CombineAtIndex_Bytes(ub, 0, startP, slayers.CmnHdrLen, R54)
+	// @ assert p.path == p.scionLayer.GetPath(ub)
 	// @ p.scionLayer.ValidHeaderOffsetFromSubSliceLemma(ub, startP)
+	// @ assert p.scionLayer.ValidHeaderOffset(ub, len(ub))
+	// @ assert p.path == p.scionLayer.GetPath(ub)
 	// @ p.SubSliceAbsPktToAbsPkt(ub, startP, endP)
+	// @ assert p.scionLayer.ValidHeaderOffset(ub, len(ub))
+	// @ assert p.path == p.scionLayer.GetPath(ub)
+	// @ assert p.path.GetBase(ubPath) == nextBase
 	// @ assert len(get(old(absPkt(ub)).LeftSeg).Future) > 0
 	// @ assert len(get(old(absPkt(ub)).LeftSeg).History) == 0
 	// @ assert slayers.ValidPktMetaHdr(ub) && p.scionLayer.EqAbsHeader(ub)
 	// @ assert absPkt(ub) == reveal AbsDoXover(old(absPkt(ub)))
+	// @ assert p.path == p.scionLayer.GetPath(ub)
+	// @ assert p.path.GetBase(ubPath) == nextBase
 	var err error
 	// (VerifiedSCION) Due to an incompleteness (https://github.com/viperproject/gobra/issues/770),
 	// we introduce a temporary variable to be able to call `path.AbsMacArrayCongruence()`.
@@ -3173,6 +3188,7 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost currBase scio
 		// TODO parameter problem invalid path
 		return processResult{}, err
 	}
+	// @ assert p.path.GetBase(ubPath) == nextBase
 	p.hopField = tmpHopField
 	// @ path.AbsMacArrayCongruence(p.hopField.Mac, tmpHopField.Mac)
 	// @ assert p.hopField.ToIO_HF() == tmpHopField.ToIO_HF()
@@ -3185,15 +3201,18 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost currBase scio
 		// TODO parameter problem invalid path
 		return processResult{}, err
 	}
-	// @ ghost sl.CombineRange_Bytes(ub, startP, endP, HalfPerm)
+	// @ assert p.path.GetBase(ubPath) == nextBase
 	// @ p.SubSliceAbsPktToAbsPkt(ub, startP, endP)
+	// @ ghost sl.CombineRange_Bytes(ub, startP, endP, HalfPerm/2)
 	// @ absPktFutureLemma(ub)
 	// @ p.path.DecodingLemma(ubPath, p.infoField, p.hopField)
 	// @ assert reveal p.path.EqAbsInfoField(p.path.absPkt(ubPath), p.infoField.ToAbsInfoField())
 	// @ assert reveal p.path.EqAbsHopField(p.path.absPkt(ubPath), p.hopField.ToIO_HF())
 	// @ assert reveal p.EqAbsHopField(absPkt(ub))
 	// @ assert reveal p.EqAbsInfoField(absPkt(ub))
+	// @ ghost sl.CombineRange_Bytes(ub, startP, endP, HalfPerm/2)
 	// @ fold acc(p.scionLayer.Mem(ub), 1-R55)
+	// @ assert currBase.IncPathSpec().Valid()
 	return processResult{}, nil
 }
 
diff --git a/router/io-spec-lemmas.gobra b/router/io-spec-lemmas.gobra
index 15c0d4475..85ccc7506 100644
--- a/router/io-spec-lemmas.gobra
+++ b/router/io-spec-lemmas.gobra
@@ -263,6 +263,7 @@ ensures  end == p.scionLayer.PathEndIdx(ub)
 ensures  scion.validPktMetaHdr(ub[start:end])
 ensures  p.path.GetBase(ub[start:end]).EqAbsHeader(ub[start:end])
 ensures  p.scionLayer.ValidHeaderOffset(ub, len(ub))
+ensures  p.path === p.scionLayer.GetPath(ub)
 ensures  absPkt(ub) == p.path.absPkt(ub[start:end])
 decreases
 func (p* scionPacketProcessor) AbsPktToSubSliceAbsPkt(ub []byte, start int, end int) {
@@ -324,7 +325,9 @@ ensures  start == p.scionLayer.PathStartIdx(ub)
 ensures  end == p.scionLayer.PathEndIdx(ub)
 ensures  scion.validPktMetaHdr(ub[start:end])
 ensures  p.scionLayer.EqAbsHeader(ub)
+ensures  p.path === p.scionLayer.GetPath(ub)
 ensures  absPkt(ub) == p.path.absPkt(ub[start:end])
+ensures  p.scionLayer.ValidHeaderOffset(ub, len(ub))
 decreases
 func (p* scionPacketProcessor) SubSliceAbsPktToAbsPkt(ub []byte, start int, end int){
 	unfold acc(sl.Bytes(ub, 0, len(ub)), R56)