Relate bytes to IO specification

router/dataplane_spec.gobra

@@ -20,9 +20,15 @@ import (
 	"net"
 	"hash"
 	sl "github.com/scionproto/scion/verification/utils/slices"
+	"github.com/scionproto/scion/verification/io"
+
+	"github.com/scionproto/scion/verification/dependencies/encoding/binary"
+	"github.com/scionproto/scion/verification/utils/bitwise"
 	"github.com/scionproto/scion/pkg/scrypto"
 	"github.com/scionproto/scion/pkg/addr"
 )
+//"github.com/scionproto/scion/verification/definitions"
+
 
 // TODO: maybe change interpretation of Mutex depending on whether the
 // dataplane is running or not. This is because, when Run is called and
@@ -343,3 +349,262 @@ func closureSpec2(i uint16, c BatchConn)
 requires true
 func closureSpec3(c BatchConn)
 /** End of closure specs for the Run method **/
+
+
+
+/** Start of io-spec helper functions **/
+
+
+ghost 
+requires seg1Len > 0
+requires seg2Len >= 0
+requires seg3Len >= 0
+requires currHF < seg1Len + seg2Len + seg3Len
+decreases
+pure func computeSeqlen(currHF int, seg1Len int, seg2Len int, seg3Len int) int{
+	return seg1Len > currHF ? seg1Len : ((seg1Len + seg2Len) > currHF ?  seg2Len: seg3Len)
+}
+
+ghost 
+decreases
+pure func infoFieldOffsetSeg(currINF int) int{
+	return 4 + 8 * currINF
+}
+
+ghost 
+decreases 
+pure func numInfoFields(seg1Len int, seg2Len int, seg3Len int) int {
+	return seg3Len > 0 ? 3 : (seg2Len > 0 ? 2 : 1)
+}
+
+ghost 
+requires seg1Len > 0
+requires seg2Len >= 0
+requires seg3Len >= 0
+requires currHF >= 0
+ensures res <= currHF
+decreases
+pure func computeprevSegLen(currHF int, seg1Len int, seg2Len int, seg3Len int) (res int){
+	return seg1Len > currHF ? 0 : ((seg1Len + seg2Len) > currHF ? seg1Len : seg1Len + seg2Len)
+}
+
+//expects the raw bytes of whole path
+ghost
+requires start + 12 <= len(raw)
+requires 0 <= start
+requires acc(&raw[start+2], _) && acc(&raw[start+3], _) && acc(&raw[start+4], _) && acc(&raw[start+5], _)
+decreases
+pure func getHopField(raw []byte, start int) io.IO_HF {
+	return let inif2 := binary.BigEndian.Uint16(raw[start+2:start+4]) == 0 ? none[io.IO_ifs] : some(io.IO_ifs(binary.BigEndian.Uint16(raw[start+2:start+4]))) in
+			let egif2 := binary.BigEndian.Uint16(raw[start+4:start+6])== 0 ? none[io.IO_ifs] : some(io.IO_ifs(binary.BigEndian.Uint16(raw[start+4:start+6]))) in
+				io.IO_HF(io.IO_HF_{
+					InIF2 : inif2,
+					EgIF2 : egif2,
+					HVF : computeMsgTerm(raw, start),
+				})
+}
+
+
+//expects the raw bytes of whole path
+ghost 
+requires 4 + 8 * numINF + offset*12 + 12 <= len(raw)
+requires prevSegLen >= 0 && offset - prevSegLen >= -1
+requires 0 < numINF && numINF < 4
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases offset - prevSegLen + 1
+pure func getSegPast(raw []byte, prevSegLen int, offset int, numINF int) seq[io.IO_HF]{
+	return offset - prevSegLen == -1 ? seq[io.IO_HF]{} : 
+		(unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in 
+			seq[io.IO_HF]{getHopField(raw,4 + 8 * numINF + offset*12)}) ++ getSegPast(raw, prevSegLen, offset-1, numINF)
+}
+
+//expects the raw bytes of whole path
+ghost 
+requires 4 + 8 * numINF + offset*12 + 12 <= len(raw)
+requires offset >= currHF && currHF >= 0
+requires 0 < numINF && numINF < 4
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases offset - currHF
+pure func getSegFuture(raw []byte, currHF int, offset int, numINF int) seq[io.IO_HF]{
+	return offset == currHF ? (unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in seq[io.IO_HF]{getHopField(raw,4 + 8 * numINF + offset*12)}) : 
+		getSegFuture(raw, currHF, offset-1, numINF) ++ (unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in seq[io.IO_HF]{getHopField(raw, 4 + 8 * numINF + offset*12)})
+}
+
+//expects the raw bytes of whole path
+ghost 
+requires 4 + 8 * numINF + offset*12 + 12 <= len(raw)
+requires prevSegLen >= 0 && offset - prevSegLen >= -1
+requires 0 < numINF && numINF < 4
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases offset - prevSegLen + 1
+pure func getSegHistory(raw []byte, prevSegLen int, offset int, numINF int) seq[io.IO_ahi]{
+	return offset - prevSegLen == -1 ? seq[io.IO_ahi]{} : 
+		(unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in 
+			seq[io.IO_ahi]{getHopField(raw,4 + 8 * numINF + offset*12).Toab()}) ++ getSegHistory(raw, prevSegLen, offset-1, numINF)
+}
+
+
+
+ghost 
+//expects the raw bytes of whole path
+requires 4 + 8 * numINF + 12*prevSegLen + 12*segLen <= len(raw)
+requires prevSegLen >= 0 && segLen >= 0
+requires 0 < numINF && numINF < 4
+requires segLen+prevSegLen > currHF && currHF >= prevSegLen
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases 
+pure func getSegment(raw []byte, consDir bool, peer bool, currHF int, prevSegLen int, segLen int, numINF int, currINF int) io.IO_seg2{
+	return io.IO_seg2(io.IO_seg3_{
+				AInfo : computeAInfo(raw, currINF),
+				UInfo : computeUInfo(raw, currINF),
+				ConsDir : consDir,
+				Peer : peer,
+				Past : getSegPast(raw, prevSegLen, currHF - 1, numINF),
+				Future : getSegFuture(raw, currHF, segLen+prevSegLen-1, numINF),
+				History : getSegHistory(raw, prevSegLen, currHF - 1, numINF),
+			})
+}
+
+ghost 
+//expects the raw bytes of whole path
+requires 4 + 8 * numINF + 12*prevSegLen + 12*segLen <= len(raw)
+requires prevSegLen >= 0 && segLen >= 0
+requires 0 < numINF && numINF < 4
+requires segLen+prevSegLen > currHF && currHF >= prevSegLen
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases 
+pure func getPastSegment(raw []byte, consDir bool, peer bool, currHF int, prevSegLen int, segLen int, numINF int, currINF int) io.IO_seg2{
+	return io.IO_seg2(io.IO_seg3_{
+				AInfo : computeAInfo(raw, currINF),
+				UInfo : computeUInfo(raw, currINF),
+				ConsDir : consDir,
+				Peer : peer,
+				Past : getSegPast(raw, prevSegLen, currHF, numINF),
+				Future : seq[io.IO_HF]{},
+				History : getSegHistory(raw, prevSegLen, currHF, numINF),
+			})
+}
+
+
+ghost
+requires seg1Len > 0
+requires seg2Len >= 0
+requires seg3Len >= 0
+requires 4 + 8*numInfoFields(seg1Len, seg2Len, seg3Len) + 12 * seg1Len + 12 * seg2Len + 12 * seg3Len == len(raw)
+requires 0 <= currINF && currINF < 3
+requires 0 <= currHF && currHF < seg1Len + seg2Len + seg3Len
+requires computeSeqlen(currHF, seg1Len, seg2Len, seg3Len) + computeprevSegLen(currHF, seg1Len, seg2Len, seg3Len) > currHF
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases 
+pure func getCurrSeg(raw []byte, currINF int, currHF int, seg1Len int, seg2Len int, seg3Len int) io.IO_seg3 {
+	return let consDir := (unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in raw[infoFieldOffsetSeg(currINF)] & 0x1 == 0x1) in
+			let peer := (unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in raw[infoFieldOffsetSeg(currINF)] & 0x2 == 0x2) in
+			let segLen := computeSeqlen(currHF, seg1Len, seg2Len, seg3Len) in
+			let prevSegLen := computeprevSegLen(currHF, seg1Len, seg2Len, seg3Len) in
+			let numINF := numInfoFields(seg1Len, seg2Len, seg3Len) in
+			getSegment(raw, consDir, peer, currHF, prevSegLen, segLen, numINF, currINF)
+}
+
+
+ghost
+requires seg1Len > 0
+requires seg2Len >= 0
+requires seg3Len >= 0
+requires 4 + 8*numInfoFields(seg1Len, seg2Len, seg3Len) + 12 * seg1Len + 12 * seg2Len + 12 * seg3Len == len(raw)
+requires 0 <= currINF && currINF < 3
+requires 0 <= currHF && currHF < seg1Len + seg2Len + seg3Len
+requires computeSeqlen(currHF, seg1Len, seg2Len, seg3Len) + computeprevSegLen(currHF, seg1Len, seg2Len, seg3Len) > currHF
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases 
+pure func getLeftSeg(raw []byte, currINF int, currHF int, seg1Len int, seg2Len int, seg3Len int) option[io.IO_seg3] {
+	return let newCurrHF := computeSeqlen(currHF, seg1Len, seg2Len, seg3Len) + computeprevSegLen(currHF, seg1Len, seg2Len, seg3Len) in
+		(newCurrHF == seg1Len + seg2Len + seg3Len || currINF == 2) ? none[io.IO_seg3] :
+			some(getCurrSeg(raw, currINF + 1, newCurrHF, seg1Len, seg2Len, seg3Len))
+}
+
+ghost
+requires seg1Len > 0
+requires seg2Len >= 0
+requires seg3Len >= 0
+requires 4 + 8*numInfoFields(seg1Len, seg2Len, seg3Len) + 12 * seg1Len + 12 * seg2Len + 12 * seg3Len == len(raw)
+requires 0 <= currINF && currINF < 3
+requires 0 <= currHF && currHF < seg1Len + seg2Len + seg3Len
+requires computeSeqlen(currHF, seg1Len, seg2Len, seg3Len) + computeprevSegLen(currHF, seg1Len, seg2Len, seg3Len) > currHF
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases 
+pure func getRightSeg(raw []byte, currINF int, currHF int, seg1Len int, seg2Len int, seg3Len int) option[io.IO_seg3] {
+	return (computeprevSegLen(currHF, seg1Len, seg2Len, seg3Len) == 0 || currINF == 0) ? none[io.IO_seg3] :
+			(let newCurrHF := computeprevSegLen(currHF, seg1Len, seg2Len, seg3Len)-1 in
+			let consDir := (unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in raw[infoFieldOffsetSeg(currINF-1)] & 0x1 == 0x1) in
+			let peer := (unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in raw[infoFieldOffsetSeg(currINF-1)] & 0x2 == 0x2) in
+			let segLen := computeSeqlen(newCurrHF, seg1Len, seg2Len, seg3Len) in
+			let prevSegLen := computeprevSegLen(newCurrHF, seg1Len, seg2Len, seg3Len) in
+			let numINF := numInfoFields(seg1Len, seg2Len, seg3Len) in
+			some(getPastSegment(raw, consDir, peer, newCurrHF, prevSegLen, segLen, numINF, currINF)))
+}
+
+
+ghost
+requires seg1Len > 0
+requires seg2Len >= 0
+requires seg3Len >= 0
+requires 4 + 8*numInfoFields(seg1Len, seg2Len, seg3Len) + 12 * seg1Len + 12 * seg2Len + 12 * seg3Len == len(raw)
+requires 0 <= currINF && currINF < 3
+requires 0 <= currHF && currHF < seg1Len + seg2Len + seg3Len
+requires computeSeqlen(currHF, seg1Len, seg2Len, seg3Len) + computeprevSegLen(currHF, seg1Len, seg2Len, seg3Len) > currHF
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases 
+pure func getMidSeg(raw []byte, currINF int, currHF int, seg1Len int, seg2Len int, seg3Len int) option[io.IO_seg3] {
+	return seg3Len == 0 ? none[io.IO_seg3] :
+		(computeprevSegLen(currHF, seg1Len, seg2Len, seg3Len) == seg1Len) ? none[io.IO_seg3] :
+			(computeprevSegLen(currHF, seg1Len, seg2Len, seg3Len) == 0) ? some(getCurrSeg(raw, 2, seg1Len + seg2Len, seg1Len, seg2Len, seg3Len)) : 
+				(let consDir := (unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in raw[infoFieldOffsetSeg(0)] & 0x1 == 0x1) in
+				let peer := (unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in raw[infoFieldOffsetSeg(0)] & 0x2 == 0x2) in
+				let numINF := numInfoFields(seg1Len, seg2Len, seg3Len) in
+				some(getPastSegment(raw, consDir, peer, seg1Len-1, 0, seg1Len, numINF, currINF)))
+}
+
+//TODO improve preconditions
+ghost 
+requires len(raw) > 4
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+requires unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in 
+	let hdr := binary.BigEndian.Uint32(raw[0:4]) in
+	//hdr == (uint32(raw[3]) | uint32(raw[2])<<8 | uint32(raw[1])<<16 | uint32(raw[0])<<24) &&
+	//DeserializingHdr(raw[0], raw[1], raw[2], raw[3], hdr) &&
+	0 <= uint8(hdr >> 30) && uint8(hdr >> 30) < 3 && //currINF
+	0 <= (uint8(hdr >> 24) & 0x3F) && (uint8(hdr >> 24) & 0x3F) < (uint8(hdr >> 12) & 0x3F) + (uint8(hdr >> 6) & 0x3F) + (uint8(hdr) & 0x3F) && //currHF
+	0 <  uint8(hdr >> 12) & 0x3F && //seg1Len
+	0 <= uint8(hdr >> 6) & 0x3F && //seg2Len
+	0 <= uint8(hdr) & 0x3F && //seg3Len
+	4 + 8*numInfoFields(int(uint8(hdr >> 12) & 0x3F), int(uint8(hdr >> 6) & 0x3F), int(uint8(hdr) & 0x3F)) + 12 * int(uint8(hdr >> 12) & 0x3F) + 12 * int(uint8(hdr >> 6) & 0x3F) + 12 * int(uint8(hdr) & 0x3F) == len(raw)
+decreases 
+pure func getPkt(raw []byte) io.IO_pkt2{
+	return let hdr := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in binary.BigEndian.Uint32(raw[0:4]) in
+			let currINF := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in uint8(hdr >> 30) in
+			let currHF := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in uint8(hdr >> 24) & 0x3F in
+			let seg1Len := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in uint8(hdr >> 12) & 0x3F in  
+			let seg2Len := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in uint8(hdr >> 6) & 0x3F in 
+			let seg3Len := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in uint8(hdr) & 0x3F in  
+	io.IO_pkt2(io.IO_Packet2{
+		CurrSeg  : getCurrSeg(raw, int(currINF), int(currHF), int(seg1Len), int(seg2Len), int(seg3Len)),
+		LeftSeg  : getLeftSeg(raw, int(currINF), int(currHF), int(seg1Len), int(seg2Len), int(seg3Len)),
+		MidSeg   : getMidSeg(raw, int(currINF), int(currHF), int(seg1Len), int(seg2Len), int(seg3Len)),
+		RightSeg : getRightSeg(raw, int(currINF), int(currHF), int(seg1Len), int(seg2Len), int(seg3Len)),
+	})
+}
+
+// TODO Do we need a body?
+ghost
+decreases
+pure func computeMsgTerm(raw []byte, start int) io.IO_msgterm
+
+ghost
+decreases
+pure func computeAInfo(raw []byte, currINF int) io.IO_ainfo
+
+ghost 
+decreases
+pure func computeUInfo(raw []byte, currINF int) set[io.IO_msgterm]
+
+/** End of io-spec helper functions **/