Refactor packet parsing to use seq[byte] views instead of slice permissions

.github/workflows/gobra.yml

@@ -46,7 +46,7 @@ jobs:
           recursive: 1
           ## Due to a bug, we cannot use the recursive mode with friend pacakge invariants.
           excludePackages: 'layers'
-          timeout: 5m
+          timeout: 10m
           headerOnly: ${{ env.headerOnly }}
           module: ${{ env.module }}
           includePaths: './dependencies/ ..' # relative to project location
@@ -321,7 +321,9 @@ jobs:
         uses: viperproject/gobra-action@main
         with:
           packages: 'pkg/slayers/path/scion'
-          timeout: 30m
+          # timeout raised while the seq-based proofs are tuned; the goal is
+          # to bring it back to 30m once the annotations are streamlined
+          timeout: 45m
           headerOnly: ${{ env.headerOnly }}
           module: ${{ env.module }}
           includePaths: ${{ env.includePaths }}

pkg/experimental/epic/epic.go

@@ -148,8 +148,8 @@ func CalcMac(auth []byte, pktID epic.PktID, s *slayers.SCION,
 	// @ package (sl.Bytes(result, 0, len(result)) --* sl.Bytes(oldBuffer, 0, len(oldBuffer))) {
 	// @ 	ghost if !allocatesNewBuffer {
 	// @ 		assert oldBuffer === buffer
-	// @ 		sl.CombineRange_Bytes(input, start, end, writePerm)
-	// @ 		sl.CombineRange_Bytes(oldBuffer, 0, inputLength, writePerm)
+	// @ 		sl.CombineRangeNoView_Bytes(input, start, end, writePerm)
+	// @ 		sl.CombineRangeNoView_Bytes(oldBuffer, 0, inputLength, writePerm)
 	// @ 	}
 	// @ }
 	// @ assert (sl.Bytes(result, 0, len(result)) --* sl.Bytes(oldBuffer, 0, len(oldBuffer)))

pkg/slayers/path/hopfield.go

@@ -79,13 +79,15 @@ type HopField struct {
 // @ preserves acc(sl.Bytes(raw, 0, HopLen), R45)
 // @ ensures   h.Mem()
 // @ ensures   err == nil
-// @ ensures  BytesToIO_HF(raw, 0, 0, HopLen) ==
+// @ ensures  BytesToIO_HF(sl.View(raw, 0, HopLen)) ==
 // @ 	unfolding acc(h.Mem(), R10) in h.Abs()
 // @ decreases
 func (h *HopField) DecodeFromBytes(raw []byte) (err error) {
 	if len(raw) < HopLen {
 		return serrors.New("HopField raw too short", "expected", HopLen, "actual", len(raw))
 	}
+	//@ ghost v := sl.View(raw, 0, HopLen)
+	//@ sl.ViewElems(raw, 0, HopLen, R46)
 	//@ unfold acc(sl.Bytes(raw, 0, HopLen), R46)
 	h.EgressRouterAlert = raw[0]&0x1 == 0x1
 	h.IngressRouterAlert = raw[0]&0x2 == 0x2
@@ -100,8 +102,14 @@ func (h *HopField) DecodeFromBytes(raw []byte) (err error) {
 	copy(h.Mac[:], raw[6:6+MacLen] /*@ , R47 @*/)
 	//@ assert forall i int :: {&h.Mac[:][i]} 0 <= i && i < MacLen ==> h.Mac[:][i] == raw[6:6+MacLen][i]
 	//@ assert forall i int :: {&h.Mac[i]} 0 <= i && i < MacLen ==> h.Mac[:][i] == h.Mac[i]
-	//@ EqualBytesImplyEqualMac(raw[6:6+MacLen], h.Mac)
-	//@ assert BytesToIO_HF(raw, 0, 0, HopLen) == h.Abs()
+	//@ assert v[2] == raw[2] && v[3] == raw[3] && v[4] == raw[4] && v[5] == raw[5]
+	//@ assert forall i int :: { v[6:6+MacLen][i] } 0 <= i && i < MacLen ==>
+	//@ 	v[6:6+MacLen][i] == v[6+i]
+	//@ assert forall i int :: { &raw[6+i] } 0 <= i && i < MacLen ==> v[6+i] == raw[6+i]
+	//@ assert forall i int :: { h.Mac[i] } 0 <= i && i < MacLen ==>
+	//@ 	v[6:6+MacLen][i] == h.Mac[i]
+	//@ EqualSeqImplyEqualMac(v[6:6+MacLen], h.Mac)
+	//@ assert BytesToIO_HF(v) == h.Abs()
 	//@ fold acc(sl.Bytes(raw, 0, HopLen), R46)
 	//@ fold h.Mem()
 	return nil
@@ -113,7 +121,7 @@ func (h *HopField) DecodeFromBytes(raw []byte) (err error) {
 // @ preserves acc(h.Mem(), R10)
 // @ preserves sl.Bytes(b, 0, HopLen)
 // @ ensures   err == nil
-// @ ensures  BytesToIO_HF(b, 0, 0, HopLen) ==
+// @ ensures  BytesToIO_HF(sl.View(b, 0, HopLen)) ==
 // @ 	unfolding acc(h.Mem(), R10) in h.Abs()
 // @ decreases
 func (h *HopField) SerializeTo(b []byte) (err error) {
@@ -134,16 +142,43 @@ func (h *HopField) SerializeTo(b []byte) (err error) {
 	binary.BigEndian.PutUint16(b[2:4], h.ConsIngress)
 	//@ assert &b[4:6][0] == &b[4] && &b[4:6][1] == &b[5]
 	binary.BigEndian.PutUint16(b[4:6], h.ConsEgress)
+	//@ assert binary.BigEndian.Uint16Spec(b[2], b[3]) == h.ConsIngress
+	//@ assert binary.BigEndian.Uint16Spec(b[4], b[5]) == h.ConsEgress
 	//@ assert forall i int :: { &b[i] } 0 <= i && i < HopLen ==> acc(&b[i])
 	//@ assert forall i int :: { &h.Mac[:][i] } 0 <= i && i < len(h.Mac) ==>
 	//@ 	&h.Mac[i] == &h.Mac[:][i]
 	//@ sl.AssertSliceOverlap(b, 6, 6+MacLen)
 	copy(b[6:6+MacLen], h.Mac[:] /*@, R47 @*/)
 	//@ assert forall i int :: {&h.Mac[:][i]} 0 <= i && i < MacLen ==> h.Mac[:][i] == b[6:6+MacLen][i]
 	//@ assert forall i int :: {&h.Mac[i]} 0 <= i && i < MacLen ==> h.Mac[:][i] == h.Mac[i]
-	//@ EqualBytesImplyEqualMac(b[6:6+MacLen], h.Mac)
+	//@ assert forall i int :: { &b[6+i] } 0 <= i && i < MacLen ==> b[6:6+MacLen][i] == b[6+i]
+	//@ ghost b2 := b[2]
+	//@ ghost b3 := b[3]
+	//@ ghost b4 := b[4]
+	//@ ghost b5 := b[5]
+	//@ ghost mac := seq[byte]{b[6], b[7], b[8], b[9], b[10], b[11]}
+	//@ assert forall i int :: { mac[i] } 0 <= i && i < MacLen ==> mac[i] == h.Mac[i]
 	//@ fold sl.Bytes(b, 0, HopLen)
-	//@ assert h.Abs() == BytesToIO_HF(b, 0, 0, HopLen)
+	// the GetByte terms instantiate the preservation postconditions of
+	// ViewElems, which carry the byte values across the lemma call
+	//@ assert sl.GetByte(b, 0, HopLen, 2) == b2 && sl.GetByte(b, 0, HopLen, 3) == b3
+	//@ assert sl.GetByte(b, 0, HopLen, 4) == b4 && sl.GetByte(b, 0, HopLen, 5) == b5
+	//@ assert sl.GetByte(b, 0, HopLen, 6) == mac[0] && sl.GetByte(b, 0, HopLen, 7) == mac[1]
+	//@ assert sl.GetByte(b, 0, HopLen, 8) == mac[2] && sl.GetByte(b, 0, HopLen, 9) == mac[3]
+	//@ assert sl.GetByte(b, 0, HopLen, 10) == mac[4] && sl.GetByte(b, 0, HopLen, 11) == mac[5]
+	//@ sl.ViewElems(b, 0, HopLen, writePerm)
+	//@ ghost v := sl.View(b, 0, HopLen)
+	//@ assert v[2] == sl.GetByte(b, 0, HopLen, 2) && v[3] == sl.GetByte(b, 0, HopLen, 3)
+	//@ assert v[4] == sl.GetByte(b, 0, HopLen, 4) && v[5] == sl.GetByte(b, 0, HopLen, 5)
+	//@ assert v[6] == mac[0] && v[7] == mac[1] && v[8] == mac[2]
+	//@ assert v[9] == mac[3] && v[10] == mac[4] && v[11] == mac[5]
+	//@ assert v[2] == b2 && v[3] == b3 && v[4] == b4 && v[5] == b5
+	//@ assert mac[0] == h.Mac[0] && mac[1] == h.Mac[1] && mac[2] == h.Mac[2]
+	//@ assert mac[3] == h.Mac[3] && mac[4] == h.Mac[4] && mac[5] == h.Mac[5]
+	//@ assert v[6:6+MacLen][0] == v[6] && v[6:6+MacLen][1] == v[7] && v[6:6+MacLen][2] == v[8]
+	//@ assert v[6:6+MacLen][3] == v[9] && v[6:6+MacLen][4] == v[10] && v[6:6+MacLen][5] == v[11]
+	//@ EqualSeqImplyEqualMac(v[6:6+MacLen], h.Mac)
+	//@ assert h.Abs() == BytesToIO_HF(v)
 	//@ fold acc(h.Mem(), R11)
 	return nil
 }

pkg/slayers/path/hopfield_spec.gobra

@@ -18,9 +18,7 @@ package path
 
 import (
 	"verification/io"
-	sl "verification/utils/slices"
 	"verification/dependencies/encoding/binary"
-	. "verification/utils/definitions"
 )
 
 pred (h *HopField) Mem() {
@@ -40,72 +38,24 @@ pure func IO_ifsToIfs(ifs option[io.Ifs]) uint16 {
 	return ifs == none[io.Ifs] ? 0 : uint16(get(ifs).V)
 }
 
+// BytesToIO_HF takes the raw bytes of exactly one hop field (obtained
+// by slicing the view of a buffer) and computes its abstract
+// representation. It requires no permissions.
 ghost
-requires 0 <= start && start <= middle
-requires middle + HopLen <= end && end <= len(raw)
-requires sl.Bytes(raw, start, end)
+requires len(raw) == HopLen
 decreases
-pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.HF) {
-	return let _ := sl.AssertSliceOverlap(raw, middle+2, middle+4)     in
-		let _ := sl.AssertSliceOverlap(raw, middle+4, middle+6)        in
-		let _ := sl.AssertSliceOverlap(raw, middle+6, middle+6+MacLen) 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
-		let op_egif2 := ifsToIO_ifs(egif2)                             in
+pure func BytesToIO_HF(raw seq[byte]) (io.HF) {
+	return let inif2 := binary.BigEndian.Uint16Spec(raw[2], raw[3])  in
+		let egif2 := binary.BigEndian.Uint16Spec(raw[4], raw[5])     in
+		let op_inif2 := ifsToIO_ifs(inif2)                           in
+		let op_egif2 := ifsToIO_ifs(egif2)                           in
 		io.HF {
 			InIF2: op_inif2,
 			EgIF2: op_egif2,
-			HVF: AbsMac(FromSliceToMacArray(raw[middle+6:middle+6+MacLen])),
+			HVF: AbsMac(FromSeqToMacArray(raw[6:6+MacLen])),
 		}
 }
 
-// WidenBytesHopField shows the equality between the HF computed
-// from raw bytes in slice 'raw' starting at position `offset` with
-// the HF obtained from the slice 'raw[start:end]`.
-ghost
-requires  0 <= start && start <= offset
-requires  offset + HopLen <= end
-requires  end <= len(raw)
-preserves acc(sl.Bytes(raw, 0, len(raw)), R55)
-preserves acc(sl.Bytes(raw[start:end], 0, len(raw[start:end])), R55)
-ensures   BytesToIO_HF(raw, 0, offset, len(raw)) ==
-	BytesToIO_HF(raw[start:end], 0, offset-start, end-start)
-decreases
-func WidenBytesHopField(raw []byte, offset int, start int, end int) {
-	unfold acc(sl.Bytes(raw, 0, len(raw)), R56)
-	unfold acc(sl.Bytes(raw[start:end], 0, len(raw[start:end])), R56)
-	hfBytes1 := BytesToIO_HF(raw, 0, offset, len(raw))
-	hfBytes2 := BytesToIO_HF(raw[start:end], 0, offset-start, end-start)
-
-	sl.AssertSliceOverlap(raw, start, end)
-	sl.AssertSliceOverlap(raw[start:end], offset-start+2, offset-start+4)
-	assert hfBytes1.InIF2 == hfBytes2.InIF2
-	sl.AssertSliceOverlap(raw[start:end], offset-start+4, offset-start+6)
-	assert hfBytes1.EgIF2 == hfBytes2.EgIF2
-	sl.AssertSliceOverlap(raw[start:end], offset-start+6, offset-start+6+MacLen)
-
-	fold acc(sl.Bytes(raw, 0, len(raw)), R56)
-	fold acc(sl.Bytes(raw[start:end], 0, len(raw[start:end])), R56)
-}
-
-// WidenBytesHopField shows the equality between the HF computed
-// from raw bytes in slice 'raw' starting at position `offset` with
-// the HF obtained from the slice 'raw[offset:offset+HopLen]`.
-// It is a special case of `WidenBytesHopField`.
-ghost
-requires  0 <= offset
-requires  offset+HopLen <= len(raw)
-preserves acc(sl.Bytes(raw, 0, len(raw)), R55)
-preserves acc(sl.Bytes(raw[offset:offset+HopLen], 0, HopLen), R55)
-ensures   BytesToIO_HF(raw, 0, offset, len(raw)) ==
-	BytesToIO_HF(raw[offset:offset+HopLen], 0, 0, HopLen)
-decreases
-func BytesToAbsHopFieldOffsetEq(raw [] byte, offset int) {
-	WidenBytesHopField(raw, offset, offset, offset+HopLen)
-}
-
 ghost
 decreases
 pure func (h HopField) Abs() (io.HF) {

pkg/slayers/path/infofield.go

@@ -64,13 +64,15 @@ type InfoField struct {
 // @ preserves acc(inf)
 // @ preserves acc(slices.Bytes(raw, 0, len(raw)), R45)
 // @ ensures   err == nil
-// @ ensures   BytesToAbsInfoField(raw, 0) ==
+// @ ensures   BytesToAbsInfoField(slices.View(raw, 0, len(raw))[:InfoLen]) ==
 // @	inf.ToAbsInfoField()
 // @ decreases
 func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) {
 	if len(raw) < InfoLen {
 		return serrors.New("InfoField raw too short", "expected", InfoLen, "actual", len(raw))
 	}
+	//@ ghost v := slices.View(raw, 0, len(raw))
+	//@ slices.ViewElems(raw, 0, len(raw), R50)
 	//@ unfold acc(slices.Bytes(raw, 0, len(raw)), R50)
 	inf.ConsDir = raw[0]&0x1 == 0x1
 	inf.Peer = raw[0]&0x2 == 0x2
@@ -79,8 +81,10 @@ func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) {
 	//@ assert &raw[4:8][0] == &raw[4] && &raw[4:8][1] == &raw[5]
 	//@ assert &raw[4:8][2] == &raw[6] && &raw[4:8][3] == &raw[7]
 	inf.Timestamp = binary.BigEndian.Uint32(raw[4:8])
+	//@ assert v[0] == raw[0] && v[2] == raw[2] && v[3] == raw[3]
+	//@ assert v[4] == raw[4] && v[5] == raw[5] && v[6] == raw[6] && v[7] == raw[7]
 	//@ fold acc(slices.Bytes(raw, 0, len(raw)), R50)
-	//@ assert reveal BytesToAbsInfoField(raw, 0) ==
+	//@ assert reveal BytesToAbsInfoField(v[:InfoLen]) ==
 	//@ 	inf.ToAbsInfoField()
 	return nil
 }
@@ -92,7 +96,7 @@ func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) {
 // @ preserves slices.Bytes(b, 0, len(b))
 // @ ensures   err == nil
 // @ ensures   inf.ToAbsInfoField() ==
-// @ 	BytesToAbsInfoField(b, 0)
+// @ 	BytesToAbsInfoField(slices.View(b, 0, len(b))[:InfoLen])
 // @ decreases
 func (inf *InfoField) SerializeTo(b []byte) (err error) {
 	if len(b) < InfoLen {
@@ -105,32 +109,47 @@ func (inf *InfoField) SerializeTo(b []byte) (err error) {
 	if inf.ConsDir {
 		b[0] |= 0x1
 	}
-	//@ ghost tmpInfo1 := BytesToAbsInfoFieldHelper(b, 0)
 	//@ bits.InfoFieldFirstByteSerializationLemmas()
-	//@ assert tmpInfo1.ConsDir == targetAbsInfo.ConsDir
+	//@ assert (b[0] & 0x1 == 0x1) == targetAbsInfo.ConsDir
 	//@ ghost firstByte := b[0]
 	if inf.Peer {
 		b[0] |= 0x2
 	}
-	//@ tmpInfo2 := BytesToAbsInfoFieldHelper(b, 0)
-	//@ assert tmpInfo2.Peer == (b[0] & 0x2 == 0x2)
-	//@ assert tmpInfo2.ConsDir == (b[0] & 0x1 == 0x1)
-	//@ assert tmpInfo2.Peer == targetAbsInfo.Peer
-	//@ assert tmpInfo2.ConsDir == tmpInfo1.ConsDir
-	//@ assert tmpInfo2.ConsDir == targetAbsInfo.ConsDir
+	//@ assert (b[0] & 0x2 == 0x2) == targetAbsInfo.Peer
+	//@ assert (b[0] & 0x1 == 0x1) == (firstByte & 0x1 == 0x1)
+	//@ assert (b[0] & 0x1 == 0x1) == targetAbsInfo.ConsDir
 	b[1] = 0 // reserved
 	//@ assert &b[2:4][0] == &b[2] && &b[2:4][1] == &b[3]
 	binary.BigEndian.PutUint16(b[2:4], inf.SegID)
-	//@ ghost tmpInfo3 := BytesToAbsInfoFieldHelper(b, 0)
-	//@ assert tmpInfo3.UInfo == targetAbsInfo.UInfo
+	//@ assert binary.BigEndian.Uint16Spec(b[2], b[3]) == inf.SegID
 	//@ assert &b[4:8][0] == &b[4] && &b[4:8][1] == &b[5]
 	//@ assert &b[4:8][2] == &b[6] && &b[4:8][3] == &b[7]
 	binary.BigEndian.PutUint32(b[4:8], inf.Timestamp)
-	//@ ghost tmpInfo4 := BytesToAbsInfoFieldHelper(b, 0)
-	//@ assert tmpInfo4.AInfo == targetAbsInfo.AInfo
+	//@ assert binary.BigEndian.Uint32Spec(b[4], b[5], b[6], b[7]) == inf.Timestamp
+	//@ ghost b0 := b[0]
+	//@ ghost b2 := b[2]
+	//@ ghost b3 := b[3]
+	//@ ghost b4 := b[4]
+	//@ ghost b5 := b[5]
+	//@ ghost b6 := b[6]
+	//@ ghost b7 := b[7]
 	//@ fold slices.Bytes(b, 0, len(b))
+	// the GetByte terms instantiate the preservation postconditions of
+	// ViewElems, which carry the byte values across the lemma call
+	//@ assert slices.GetByte(b, 0, len(b), 0) == b0
+	//@ assert slices.GetByte(b, 0, len(b), 2) == b2 && slices.GetByte(b, 0, len(b), 3) == b3
+	//@ assert slices.GetByte(b, 0, len(b), 4) == b4 && slices.GetByte(b, 0, len(b), 5) == b5
+	//@ assert slices.GetByte(b, 0, len(b), 6) == b6 && slices.GetByte(b, 0, len(b), 7) == b7
+	//@ slices.ViewElems(b, 0, len(b), writePerm)
+	//@ ghost v := slices.View(b, 0, len(b))
+	//@ assert v[0] == slices.GetByte(b, 0, len(b), 0)
+	//@ assert v[2] == slices.GetByte(b, 0, len(b), 2) && v[3] == slices.GetByte(b, 0, len(b), 3)
+	//@ assert v[4] == slices.GetByte(b, 0, len(b), 4) && v[5] == slices.GetByte(b, 0, len(b), 5)
+	//@ assert v[6] == slices.GetByte(b, 0, len(b), 6) && v[7] == slices.GetByte(b, 0, len(b), 7)
+	//@ assert v[0] == b0 && v[2] == b2 && v[3] == b3
+	//@ assert v[4] == b4 && v[5] == b5 && v[6] == b6 && v[7] == b7
 	//@ assert inf.ToAbsInfoField() ==
-	//@ 	reveal BytesToAbsInfoField(b, 0)
+	//@ 	reveal BytesToAbsInfoField(v[:InfoLen])
 	return nil
 }