Relate bytes to IO specification

router/dataplane_spec.gobra

@@ -20,6 +20,9 @@ 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"
 )
@@ -194,7 +197,7 @@ func newOffsetPair(n int) (res seq[offsetPair])
 ghost
 requires acc(MutexInvariant!<d!>(), _)
 ensures  acc(&d.internalNextHops, _)
-ensures  d.internalNextHops != nil  ==> acc(AccAddr(d.internalNextHops), _)
+ensures  d.internalNextHops != nil ==> acc(AccAddr(d.internalNextHops), _)
 decreases
 func (d *DataPlane) getInternalNextHops() {
 	unfold acc(MutexInvariant!<d!>(), _)
@@ -272,7 +275,7 @@ ensures  scrypto.ValidKeyForHash(*d.key)
 ensures  d.macFactory implements MacFactorySpec{d.key}
 decreases
 func (d *DataPlane) getNewPacketProcessorFootprint() {
-    unfold acc(MutexInvariant!<d!>(), _)
+	unfold acc(MutexInvariant!<d!>(), _)
 }
 
 /**** End of acessor methods to avoid unfolding the Mem predicate of the dataplane so much ****/
@@ -343,3 +346,369 @@ 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 0 < seg1Len
+requires 0 <= seg2Len
+requires 0 <= seg3Len
+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 0 < seg1Len
+requires 0 <= seg2Len
+requires 0 <= seg3Len
+requires 0 <= currHF
+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)
+}
+
+ghost
+requires idx + 12 <= len(raw)
+requires 0 <= idx
+requires acc(&raw[idx+2], _) && acc(&raw[idx+3], _) && acc(&raw[idx+4], _) && acc(&raw[idx+5], _)
+ensures  len(res.HVF.MsgTerm_Hash_.MsgTerm_MPair_2.MsgTerm_L_) > 0
+decreases
+pure func getHopField(raw []byte, idx int, beta set[io.IO_msgterm], asid io.IO_as, ainfo io.IO_ainfo) (res io.IO_HF) {
+	return let inif2 := binary.BigEndian.Uint16(raw[idx+2:idx+4]) in
+		let egif2 := binary.BigEndian.Uint16(raw[idx+4:idx+6]) in
+		let op_inif2 := inif2 == 0 ? none[io.IO_ifs] : some(io.IO_ifs(inif2)) in
+		let op_egif2 := egif2 == 0 ? none[io.IO_ifs] : some(io.IO_ifs(egif2)) in
+		let ts := io.IO_msgterm(io.MsgTerm_Num{ainfo}) in
+		let l := io.IO_msgterm(io.MsgTerm_L{seq[io.IO_msgterm]{ts, io.if2term(op_inif2), io.if2term(op_egif2), 
+			io.IO_msgterm(io.MsgTerm_FS{beta})}}) in
+		let hvf := io.mac(io.macKey(io.asidToKey(asid)), l) in
+		io.IO_HF(io.IO_HF_{
+			InIF2 : op_inif2,
+			EgIF2 : op_egif2,
+			HVF : hvf,
+		})
+}
+
+ghost 
+requires  0 <= offset
+requires  0 <= currHFIdx && currHFIdx <= segLen
+requires  offset + 12 * segLen <= len(raw)
+requires  acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+ensures   len(res) == segLen - currHFIdx
+ensures   forall k int :: {res[k]} 0 <= k && k < len(res) ==> 
+	len(res[k].HVF.MsgTerm_Hash_.MsgTerm_MPair_2.MsgTerm_L_) > 0
+decreases segLen - currHFIdx
+pure func getHopfieldsConsDir(
+	raw []byte, 
+	offset int, 
+	currHFIdx int, 
+	segLen int, 
+	beta set[io.IO_msgterm], 
+	asid io.IO_as, 
+	ainfo io.IO_ainfo) (res seq[io.IO_HF]){
+
+	return currHFIdx == segLen ? seq[io.IO_HF]{} : 
+		let hf := (unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in 
+			getHopField(raw, offset + 12 * currHFIdx, beta, asid, ainfo)) in
+		seq[io.IO_HF]{hf} ++ getHopfieldsConsDir(raw, offset, currHFIdx + 1, segLen, (beta union set[io.IO_msgterm]{hf.HVF}), asid, ainfo)
+}
+
+ghost 
+requires  0 <= offset 
+requires  -1 <= currHFIdx
+requires  offset + 12 * currHFIdx + 12 <= len(raw)
+requires  acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+ensures   len(res) == currHFIdx + 1
+ensures   forall k int :: {res[k]} 0 <= k && k < len(res) ==> 
+	len(res[k].HVF.MsgTerm_Hash_.MsgTerm_MPair_2.MsgTerm_L_) > 0
+decreases currHFIdx + 1
+pure func getHopfieldsNotConsDir(
+	raw []byte, 
+	offset int, 
+	currHFIdx int, 
+	beta set[io.IO_msgterm], 
+	asid io.IO_as, 
+	ainfo io.IO_ainfo) (res seq[io.IO_HF]){
+
+	return currHFIdx == -1 ? seq[io.IO_HF]{} : 
+		let hf := (unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in 
+			getHopField(raw, offset + 12 * currHFIdx, beta, asid, ainfo)) in
+		getHopfieldsNotConsDir(raw, offset, currHFIdx -1, (beta union set[io.IO_msgterm]{hf.HVF}), asid, ainfo) ++ seq[io.IO_HF]{hf}
+}
+
+ghost 
+requires -1 <= currHFIdx && currHFIdx < len(hopfields)
+decreases currHFIdx + 1
+pure func getSegPast(hopfields seq[io.IO_HF], currHFIdx int) seq[io.IO_HF]{
+	return currHFIdx == -1  ? seq[io.IO_HF]{} : 
+		seq[io.IO_HF]{hopfields[currHFIdx]} ++ getSegPast(hopfields, currHFIdx - 1)
+}
+
+ghost 
+requires 0 <= currHFIdx && currHFIdx <= len(hopfields)
+decreases len(hopfields) - currHFIdx
+pure func getSegFuture(hopfields seq[io.IO_HF], currHFIdx int) seq[io.IO_HF]{
+	return currHFIdx == len(hopfields) ? seq[io.IO_HF]{} : 
+		seq[io.IO_HF]{hopfields[currHFIdx]} ++ getSegFuture(hopfields, currHFIdx + 1)
+}
+
+ghost 
+requires -1 <= currHFIdx && currHFIdx < len(hopfields)
+decreases currHFIdx + 1
+pure func getSegHistory(hopfields seq[io.IO_HF], currHFIdx int) seq[io.IO_ahi]{
+	return currHFIdx == -1 ? seq[io.IO_ahi]{} : 
+		seq[io.IO_ahi]{hopfields[currHFIdx].Toab()} ++ getSegHistory(hopfields, currHFIdx - 1)
+
+}
+
+ghost 
+requires 0 <= offset
+requires 0 < segLen
+requires offset + 12 * segLen <= len(raw)
+requires 0 <= currHFIdx && currHFIdx <= segLen
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases 
+pure func getSegment(raw []byte, 
+	offset int, 
+	currHFIdx int, 
+	segLen int, 
+	asid io.IO_as, 
+	ainfo io.IO_ainfo, 
+	consDir bool, 
+	peer bool) io.IO_seg2{
+
+	return let hopfields := consDir ?
+		getHopfieldsConsDir(raw, offset, 0, segLen, set[io.IO_msgterm]{}, asid, ainfo) : 
+		getHopfieldsNotConsDir(raw, offset, segLen - 1, set[io.IO_msgterm]{}, asid, ainfo) in
+		let uinfo := getUInfo(hopfields, currHFIdx, consDir) in
+		io.IO_seg2(io.IO_seg3_{
+			AInfo :ainfo,
+			UInfo : uinfo,
+			ConsDir : consDir,
+			Peer : peer,
+			Past : getSegPast(hopfields, currHFIdx - 1),
+			Future : getSegFuture(hopfields, currHFIdx),
+			History : getSegHistory(hopfields, currHFIdx - 1),
+		})
+}
+
+ghost
+requires 4 + 8 * currINFIdx + 8 <= offset
+requires 0 < segLen
+requires offset + 12 * segLen <= len(raw)
+requires 0 <= currHFIdx && currHFIdx <= segLen
+requires 0 <= currINFIdx && currINFIdx < 3
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases 
+pure func getCurrSeg(raw []byte, offset int, currINFIdx int, currHFIdx int, segLen int, asid io.IO_as) io.IO_seg3 {
+	return unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in
+		let ainfo := getTimestamp(raw, currINFIdx) in
+		let consDir := getConsDir(raw, currINFIdx) in
+		let peer := getPeer(raw, currINFIdx) in
+		getSegment(raw, offset, currHFIdx, segLen, asid, ainfo, consDir, peer)
+}
+
+ghost
+requires 0 < seg1Len
+requires 0 <= seg2Len
+requires 0 <= seg3Len
+requires 4 + 8 * numInfoFields(seg1Len, seg2Len, seg3Len) == offset
+requires offset + 12 * (seg1Len + seg2Len + seg3Len) <= len(raw)
+requires 1 <= currINFIdx && currINFIdx < 4
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases 
+pure func getLeftSeg(
+	raw []byte, 
+	offset int, 
+	currINFIdx int, 
+	seg1Len int, 
+	seg2Len int, 
+	seg3Len int, 
+	asid io.IO_as) option[io.IO_seg3] {
+
+	return (currINFIdx == 1 && seg2Len > 0) ? 
+		some(getCurrSeg(raw, offset + 12 * seg1Len, currINFIdx, 0, seg2Len, asid)) : 
+		(currINFIdx == 2 && seg3Len > 0) ? 
+			some(getCurrSeg(raw, offset + 12 * (seg1Len + seg2Len), currINFIdx, 0, seg3Len, asid)) : 
+			none[io.IO_seg3]
+}
+
+ghost
+requires 0 < seg1Len
+requires 0 <= seg2Len
+requires 0 <= seg3Len
+requires 4 + 8 * numInfoFields(seg1Len, seg2Len, seg3Len) == offset
+requires offset + 12 * (seg1Len + seg2Len + seg3Len) <= len(raw)
+requires -1 <= currINFIdx && currINFIdx < 2
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases
+pure func getRightSeg(
+	raw []byte, 
+	offset int, 
+	currINFIdx int, 
+	seg1Len int,
+	seg2Len int, 
+	seg3Len int, 
+	asid io.IO_as) option[io.IO_seg3] {
+
+	return (currINFIdx == 1 && seg3Len > 0 && seg2Len > 0) ? 
+		some(getCurrSeg(raw, offset + 12 * seg1Len, currINFIdx, seg2Len, seg2Len, asid)) :
+		(currINFIdx == 0 && seg2Len > 0) ? 
+			some(getCurrSeg(raw, offset, currINFIdx, seg1Len, seg1Len, asid)) : 
+			none[io.IO_seg3]					
+}
+
+ghost
+requires 0 < seg1Len
+requires 0 <= seg2Len
+requires 0 <= seg3Len
+requires 4 + 8 * numInfoFields(seg1Len, seg2Len, seg3Len) == offset
+requires offset + 12 * (seg1Len + seg2Len + seg3Len) <= len(raw)
+requires 2 <= currINFIdx && currINFIdx < 5
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
+decreases 
+pure func getMidSeg(
+	raw []byte, 
+	offset int, 
+	currINFIdx int, 
+	seg1Len int, 
+	seg2Len int, 
+	seg3Len int, 
+	asid io.IO_as) option[io.IO_seg3] {
+
+	return (currINFIdx == 4 && seg3Len > 0) ? 
+		some(getCurrSeg(raw, offset, 0, seg1Len, seg1Len, asid)) :
+		(currINFIdx == 2 && seg3Len > 0) ? 
+			some(getCurrSeg(raw, offset + 12 * (seg1Len + seg2Len), currINFIdx, 0, seg3Len, asid)) : 
+			none[io.IO_seg3]
+}
+
+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
+	0 <= getCurrINF(hdr) && getCurrINF(hdr) < 3 &&
+	getCurrINF(hdr) + 1 <= numInfoFields(int(getSeg1Len(hdr)), int(getSeg2Len(hdr)), int(getSeg3Len(hdr))) &&
+	0 <= getCurrHF(hdr) && getCurrHF(hdr) < getSeg1Len(hdr) + getSeg2Len(hdr) + getSeg3Len(hdr) &&
+	0 < getSeg1Len(hdr) &&
+	0 <= getSeg2Len(hdr) && 
+	0 <= getSeg3Len(hdr) &&
+	4 + 8 * numInfoFields(int(getSeg1Len(hdr)), int(getSeg2Len(hdr)), int(getSeg3Len(hdr))) + 12 * (int(getSeg1Len(hdr)) + int(getSeg2Len(hdr)) + int(getSeg3Len(hdr))) == len(raw)
+decreases 
+pure func getPkt(raw []byte, asid io.IO_as) io.IO_pkt2{
+	return let hdr := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in binary.BigEndian.Uint32(raw[0:4]) in
+		let currINFIdx := int(getCurrINF(hdr)) in
+		let currHFIdx := int(getCurrHF(hdr)) in
+		let seg1Len := int(getSeg1Len(hdr)) in
+		let seg2Len := int(getSeg2Len(hdr)) in 
+		let seg3Len := int(getSeg3Len(hdr)) in
+		let segLen := computeSeqLen(currHFIdx, seg1Len, seg2Len, seg3Len) in
+		let prevSegLen := computePrevSegLen(currHFIdx, seg1Len, seg2Len, seg3Len) in
+		let numINF := int(numInfoFields(seg1Len, seg2Len, seg3Len)) in
+		let offset := 4 + 8 * numINF in
+		io.IO_pkt2(io.IO_Packet2{
+			CurrSeg : getCurrSeg(raw, offset+prevSegLen, currINFIdx, currHFIdx-prevSegLen, segLen, asid),
+			LeftSeg : getLeftSeg(raw, offset, currINFIdx + 1, seg1Len, seg2Len , seg3Len, asid),
+			MidSeg : getMidSeg(raw, offset, currINFIdx + 2, seg1Len, seg2Len , seg3Len, asid),
+			RightSeg : getRightSeg(raw, offset, currINFIdx - 1, seg1Len, seg2Len , seg3Len, asid),
+		})
+}
+
+ghost
+decreases
+pure func getCurrINF(hdr uint32) uint8{
+	return uint8(hdr >> 30)
+}
+
+ghost
+decreases
+pure func getCurrHF(hdr uint32) uint8{
+	return uint8(hdr >> 24) & 0x3F
+}
+
+ghost
+decreases
+pure func getSeg1Len(hdr uint32) uint8{
+	return uint8(hdr >> 12) & 0x3F
+}
+
+ghost
+decreases
+pure func getSeg2Len(hdr uint32) uint8{
+	return uint8(hdr >> 6) & 0x3F
+}
+
+ghost
+decreases
+pure func getSeg3Len(hdr uint32) uint8{
+	return uint8(hdr) & 0x3F
+}
+
+ghost 
+requires 0 <= offset
+requires infoFieldOffsetSeg(offset) < len(raw)
+requires acc(&raw[infoFieldOffsetSeg(offset)], _)
+decreases
+pure func getConsDir(raw []byte, offset int) bool{
+	return raw[infoFieldOffsetSeg(offset)] & 0x1 == 0x1
+}
+
+ghost 
+requires 0 <= offset
+requires infoFieldOffsetSeg(offset) < len(raw)
+requires acc(&raw[infoFieldOffsetSeg(offset)], _)
+decreases
+pure func getPeer(raw []byte, offset int) bool{
+	return raw[infoFieldOffsetSeg(offset)] & 0x2 == 0x2
+}
+
+ghost 
+requires 0 <= offset
+requires infoFieldOffsetSeg(offset) + 8 < len(raw)
+requires acc(&raw[infoFieldOffsetSeg(offset) + 4], _)
+requires acc(&raw[infoFieldOffsetSeg(offset) + 5], _)
+requires acc(&raw[infoFieldOffsetSeg(offset) + 6], _)
+requires acc(&raw[infoFieldOffsetSeg(offset) + 7], _)
+decreases
+pure func getTimestamp(raw []byte, offset int) io.IO_ainfo{
+	return let idx := infoFieldOffsetSeg(offset) + 4 in 
+		io.IO_ainfo(binary.BigEndian.Uint32(raw[idx : idx + 4]))
+}
+
+ghost
+requires len(hopfield.HVF.MsgTerm_Hash_.MsgTerm_MPair_2.MsgTerm_L_) > 0
+decreases
+pure func getHVFSet(hopfield io.IO_HF) set[io.IO_msgterm]{
+	return let l := hopfield.HVF.MsgTerm_Hash_.MsgTerm_MPair_2.MsgTerm_L_ in
+		l[len(l) - 1].MsgTerm_FS_
+}
+
+ghost
+requires 0 < len(hopfields)
+requires 0 <= currHFIdx && currHFIdx <= len(hopfields)
+requires forall idx int :: 0 <= idx && idx < len(hopfields) ==>
+	len(hopfields[idx].HVF.MsgTerm_Hash_.MsgTerm_MPair_2.MsgTerm_L_) > 0
+decreases
+pure func getUInfo(hopfields seq[io.IO_HF], currHFIdx int, consDir bool) set[io.IO_msgterm]{
+	return currHFIdx == len(hopfields) ? getHVFSet(hopfields[currHFIdx-1]) :
+		currHFIdx == 0 ? getHVFSet(hopfields[currHFIdx]) :
+		consDir ? getHVFSet(hopfields[currHFIdx]) : getHVFSet(hopfields[currHFIdx-1]) 
+}
+
+/** End of io-spec helper functions **/