Simplify specs of decodeLayers

.gitignore

@@ -101,3 +101,5 @@ target
 *.internal
 .devcontainer
 .metals
+.bazelbsp
+.bazel

pkg/slayers/path/scion/raw_spec.gobra

@@ -382,15 +382,15 @@ requires validPktMetaHdr(raw)
 decreases
 pure func (s *Raw) absPkt(raw []byte) (res io.IO_pkt2) {
 	return let _ := reveal validPktMetaHdr(raw) in
-		let metaHdr := RawBytesToMetaHdr(raw) in
+		let metaHdr := RawBytesToMetaHdr(raw)  in
 		let currInfIdx := int(metaHdr.CurrINF) in
-		let currHfIdx := int(metaHdr.CurrHF) in
-		let seg1Len := int(metaHdr.SegLen[0]) in
-		let seg2Len := int(metaHdr.SegLen[1]) in
-		let seg3Len := int(metaHdr.SegLen[2]) in
+		let currHfIdx := int(metaHdr.CurrHF)   in
+		let seg1Len := int(metaHdr.SegLen[0])  in
+		let seg2Len := int(metaHdr.SegLen[1])  in
+		let seg3Len := int(metaHdr.SegLen[2])  in
 		let segs := io.CombineSegLens(seg1Len, seg2Len, seg3Len) in
-		let segLen := segs.LengthOfCurrSeg(currHfIdx) in
-		let prevSegLen := segs.LengthOfPrevSeg(currHfIdx) in
+		let segLen := segs.LengthOfCurrSeg(currHfIdx)            in
+		let prevSegLen := segs.LengthOfPrevSeg(currHfIdx)        in
 		let numINF := segs.NumInfoFields() in
 		let offset := HopFieldOffset(numINF, prevSegLen, MetaLen) in
 		io.IO_Packet2 {
@@ -407,7 +407,7 @@ requires acc(sl.Bytes(raw, 0, len(raw)), R56)
 decreases
 pure func RawBytesToMetaHdr(raw []byte) MetaHdr {
 	return unfolding acc(sl.Bytes(raw, 0, len(raw)), R56) in
-		let hdr := binary.BigEndian.Uint32(raw[:MetaLen])          in
+		let hdr := binary.BigEndian.Uint32(raw[:MetaLen]) in
 		DecodedFrom(hdr)
 }
 
@@ -436,9 +436,8 @@ pure func validPktMetaHdr(raw []byte) bool {
 		let seg3 := int(metaHdr.SegLen[2])    in
 		let segs := io.CombineSegLens(seg1, seg2, seg3) in
 		let base := RawBytesToBase(raw)       in
-		0 < metaHdr.SegLen[0]           &&
-		base.StronglyValid()            &&
-		base.CurrInfMatchesCurrHF()		&&
+		0 < metaHdr.SegLen[0] &&
+		base.FullyValid()     &&
 		PktLen(segs, MetaLen) <= len(raw)
 }
 

pkg/slayers/scion_spec.gobra

@@ -335,8 +335,8 @@ ghost
 requires  0 < p
 preserves acc(s.Mem(ub), p)
 ensures   let start := s.PathStartIdx(ub) in
-		  let end   := s.PathEndIdx(ub) in
-		  0 <= start && start <= end && end <= len(ub)
+	let end := s.PathEndIdx(ub) in
+	0 <= start && start <= end && end <= len(ub)
 decreases
 func LemmaPathIdxStartEnd(s *SCION, ub []byte, p perm) {
 	unfold acc(s.Mem(ub), p)
@@ -461,7 +461,7 @@ pure func ValidPktMetaHdr(raw []byte) bool {
 		let length := GetLength(raw) in
 		length <= len(raw) &&
 		unfolding acc(sl.Bytes(raw, 0, len(raw)), R56) in
-	 	let _ := Asserting(forall k int :: {&rawHdr[k]} 0 <= k && k < scion.MetaLen ==> &rawHdr[k] == &raw[start + k]) 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
 		let seg1 := int(metaHdr.SegLen[0])         in

router/assumptions.gobra

@@ -75,6 +75,16 @@ ensures cannotRoute.ErrorMem()
 decreases _
 func establishCannotRoute()
 
+ghost
+ensures invalidSrcIA.ErrorMem()
+decreases _
+func establishInvalidSrcIA()
+
+ghost
+ensures invalidDstIA.ErrorMem()
+decreases _
+func establishInvalidDstIA()
+
 /**** End of post-init invariants ****/
 
 /**** scmpError ghost members ****/