diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra
index 75620a731..6310bdaec 100644
--- a/pkg/slayers/path/scion/base_spec.gobra
+++ b/pkg/slayers/path/scion/base_spec.gobra
@@ -191,57 +191,10 @@ pure func (s Base) IncPathSpec() (res Base) {
 	}
 }
 
-/*************** AbsBase ***************/
-
-// There is a good deal of repition in this section of the file and the similarly
-// named functions for the type `Base`. While for now this is not too big of a problem,
-// we should find ways to streamline the definitions, ideally by having these defs only
-// for the abstraction type only.
-
-type AbsBase adt {
-	AbsBase_ {
-		PathMeta AbsMetaHdr
-		NumINF int
-		NumHops int
-	}
-}
-
-type AbsMetaHdr adt {
-	AbsMetaHdr_ {
-		// we should change the types of CurrINF and CurrHF to wider types,
-		// otherwise we might start getting overflow errors here when they
-		// are fully enabled.
-		CurrINF uint8
-		CurrHF  uint8
-		SegLen  seq[uint8]
-	}
-}
-
-ghost
-decreases
-pure func (b Base) Abs() AbsBase {
-	return AbsBase_{
-		PathMeta: b.PathMeta.Abs(),
-		NumINF: b.NumINF,
-		NumHops: b.NumHops,
-	}
-}
-
-ghost
-decreases
-pure func (b MetaHdr) Abs() AbsMetaHdr {
-	return AbsMetaHdr_{
-		CurrINF: b.CurrINF,
-		CurrHF: b.CurrHF,
-		SegLen: seq[uint8]{ b.SegLen[0], b.SegLen[1], b.SegLen[2] },
-	}
-}
-
 ghost
-requires len(b.PathMeta.SegLen) == 3
 decreases
-pure func (b AbsBase) ReverseSpec() AbsBase {
-	return AbsBase_ {
+pure func (b Base) ReverseSpec() Base {
+	return Base {
 		PathMeta: b.ReverseMetaHdrSpec(),
 		NumINF: b.NumINF,
 		NumHops: b.NumHops,
@@ -249,10 +202,9 @@ pure func (b AbsBase) ReverseSpec() AbsBase {
 }
 
 ghost
-requires len(b.PathMeta.SegLen) == 3
 decreases
-pure func (b AbsBase) ReverseMetaHdrSpec() AbsMetaHdr {
-	return AbsMetaHdr_ {
+pure func (b Base) ReverseMetaHdrSpec() MetaHdr {
+	return MetaHdr {
 		CurrINF: uint8(b.NumINF) - b.PathMeta.CurrINF - 1,
 		CurrHF: uint8(b.NumHops) - b.PathMeta.CurrHF - 1,
 		SegLen: b.ReverseSegLen(),
@@ -260,83 +212,23 @@ pure func (b AbsBase) ReverseMetaHdrSpec() AbsMetaHdr {
 }
 
 ghost
-requires len(b.PathMeta.SegLen) == 3
 decreases
-pure func (b AbsBase) ReverseSegLen() seq[uint8] {
+pure func (b Base) ReverseSegLen() [3]uint8 {
 	return (match b.NumINF {
-		case 2: seq[uint8]{ b.PathMeta.SegLen[1], b.PathMeta.SegLen[0], b.PathMeta.SegLen[2]}
-		case 3: seq[uint8]{ b.PathMeta.SegLen[2], b.PathMeta.SegLen[1], b.PathMeta.SegLen[0] }
+		case 2: [3]uint8{ b.PathMeta.SegLen[1], b.PathMeta.SegLen[0], b.PathMeta.SegLen[2] }
+		case 3: [3]uint8{ b.PathMeta.SegLen[2], b.PathMeta.SegLen[1], b.PathMeta.SegLen[0] }
 		default: b.PathMeta.SegLen
 	})
 }
 
-ghost
-decreases
-pure func (b AbsBase) ValidCurrIdxsSpec() bool {
-	return 0 <= b.NumINF && b.NumINF <= MaxINFs &&
-		len(b.PathMeta.SegLen) == 3             &&
-		0 <= b.NumHops && b.NumHops <= MaxHops  &&
-		b.ValidCurrHfSpec()  &&
-		b.ValidCurrInfSpec() &&
-		0 <= b.PathMeta.SegLen[0] && b.PathMeta.SegLen[0] < MaxHops &&
-		0 <= b.PathMeta.SegLen[1] && b.PathMeta.SegLen[1] < MaxHops &&
-		0 <= b.PathMeta.SegLen[2] && b.PathMeta.SegLen[2] < MaxHops &&
-		(b.NumINF == 1 ==> b.NumHops == int(b.PathMeta.SegLen[0]))  &&
-		(b.NumINF == 2 ==> b.NumHops == int(b.PathMeta.SegLen[0] + b.PathMeta.SegLen[1])) &&
-		(b.NumINF == 3 ==> b.NumHops == int(b.PathMeta.SegLen[0] + b.PathMeta.SegLen[1] + b.PathMeta.SegLen[2])) &&
-		(forall i int :: { b.PathMeta.SegLen[i] } 0 <= i && i < b.NumINF ==>
-			b.PathMeta.SegLen[i] != 0) &&
-		(forall i int :: { b.PathMeta.SegLen[i] } b.NumINF <= i && i < MaxINFs ==>
-			b.PathMeta.SegLen[i] == 0)
-}
-
-ghost
-opaque
-requires b.ValidCurrIdxsSpec()
-decreases
-pure func (b AbsBase) CurrInfMatchesCurrHF() bool {
-	return b.PathMeta.CurrINF == b.InfForHfSpec(b.PathMeta.CurrHF)
-}
-
-ghost
-decreases
-pure func (b AbsBase) ValidCurrInfSpec() bool {
-	return 0 <= b.PathMeta.CurrINF && b.PathMeta.CurrINF < b.NumINF
-}
-
-ghost
-decreases
-pure func (b AbsBase) ValidCurrHfSpec() bool {
-	return 0 <= b.PathMeta.CurrHF && b.PathMeta.CurrHF < b.NumHops
-}
-
-ghost
-requires len(s.PathMeta.SegLen) == 3
-ensures  0 <= r && r < 3
-decreases
-pure func (s AbsBase) InfForHfSpec(hf uint8) (r uint8) {
-	return hf < s.PathMeta.SegLen[0] ?
-		0 :
-		(hf < s.PathMeta.SegLen[0] + s.PathMeta.SegLen[1] ? 1 : 2)
-}
-
 ghost
 requires b.ValidCurrIdxsSpec()
 ensures  b.ReverseSpec().ValidCurrIdxsSpec()
 decreases
-pure func (b AbsBase) ReversingValidBaseIsValidBase() Lemma {
-	return Lemma{}
-}
-
-ghost
-ensures b.ValidCurrIdxsSpec() == b.Abs().ValidCurrIdxsSpec()
-decreases
-pure func (b Base) ValidBaseHasValidAbs() Lemma {
+pure func (b Base) ReversingValidBaseIsValidBase() Lemma {
 	return Lemma{}
 }
 
-/*************** End of AbsBase ***************/
-
 ghost
 requires b.Mem()
 ensures  b.NonInitMem()
diff --git a/pkg/slayers/path/scion/decoded.go b/pkg/slayers/path/scion/decoded.go
index 764a63f4d..979289781 100644
--- a/pkg/slayers/path/scion/decoded.go
+++ b/pkg/slayers/path/scion/decoded.go
@@ -218,20 +218,17 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
 // @ decreases
 func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) {
 	//@ ghost isValid := s.ValidCurrIdxs(ubuf)
-	/*@
-	ghost base := s.GetBase(ubuf)
-	ghost absBase := base.Abs()
-	ghost absMetaHdrAferReversingSegLen := AbsMetaHdr_ {
-		CurrINF: absBase.PathMeta.CurrINF,
-		CurrHF: absBase.PathMeta.CurrHF,
-		SegLen: absBase.ReverseSegLen(),
-	}
-	ghost absBaseAfterReversingSegLen := AbsBase_ {
-		PathMeta: absMetaHdrAferReversingSegLen,
-		NumINF: absBase.NumINF,
-		NumHops: absBase.NumHops,
-	}
-	@*/
+	//@ ghost base := s.GetBase(ubuf)
+	//@ ghost metaHdrAferReversingSegLen := MetaHdr {
+	//@ 	CurrINF: base.PathMeta.CurrINF,
+	//@ 	CurrHF:  base.PathMeta.CurrHF,
+	//@ 	SegLen:  base.ReverseSegLen(),
+	//@ }
+	//@ ghost baseAfterReversingSegLen := Base {
+	//@ 	PathMeta: metaHdrAferReversingSegLen,
+	//@ 	NumINF:   base.NumINF,
+	//@ 	NumHops:  base.NumHops,
+	//@ }
 	//@ unfold s.Mem(ubuf)
 	//@ unfold s.Base.Mem()
 	if s.NumINF == 0 {
@@ -265,7 +262,7 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) {
 	//@ invariant s.Mem(ubuf)
 	//@ invariant 0 <= i && i <= s.GetNumHops(ubuf)
 	//@ invariant -1 <= j && j < s.GetNumHops(ubuf)
-	//@ invariant s.GetBase(ubuf).Abs() == absBaseAfterReversingSegLen
+	//@ invariant s.GetBase(ubuf) == baseAfterReversingSegLen
 	//@ decreases j-i
 	for i, j := 0, ( /*@ unfolding s.Mem(ubuf) in (unfolding s.Base.Mem() in @*/ s.NumHops - 1 /*@ ) @*/); i < j; i, j = i+1, j-1 {
 		//@ unfold s.Mem(ubuf)
@@ -284,9 +281,9 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) {
 	//@ unfold s.Base.Mem()
 	s.PathMeta.CurrINF = uint8(s.NumINF) - s.PathMeta.CurrINF - 1
 	s.PathMeta.CurrHF = uint8(s.NumHops) - s.PathMeta.CurrHF - 1
-	//@ assert s.Base.Abs() == absBase.ReverseSpec()
-	//@ ghost if isValid { absBase.ReversingValidBaseIsValidBase() }
-	//@ assert isValid ==> s.Base.Abs().ValidCurrIdxsSpec()
+	//@ assert s.Base == base.ReverseSpec()
+	//@ ghost if isValid { base.ReversingValidBaseIsValidBase() }
+	//@ assert isValid ==> s.Base.ValidCurrIdxsSpec()
 	//@ fold s.Base.Mem()
 	//@ fold s.Mem(ubuf)
 	return s, nil