updated io-spec

verification/io/router_events.gobra

@@ -50,13 +50,18 @@ pure func (dp DataPlaneSpec) valid_link_types_in2(hf1 IO_HF, a IO_as) bool {
 }
 /* End of Abbreviations */
 
+ghost
+decreases
+pure func (dp DataPlaneSpec) dp2_check_interface(d bool, asid IO_as, hf1 IO_HF, recvif IO_ifs) bool {
+	return (d && hf1.InIF2 === some(recvif)) || (!d && hf1.EgIF2 === some(recvif))
+}
+
 ghost
 requires dp.Valid()
 requires asid == dp.Asid()
 decreases
-pure func (dp DataPlaneSpec) dp2_check_interface(d bool, asid IO_as, hf1 IO_HF, recvif IO_ifs) bool {
-	return (d && hf1.InIF2 === some(recvif) && dp.valid_link_types_in2(hf1, asid)) ||
-		(!d && hf1.EgIF2 === some(recvif) && dp.valid_link_types2(hf1, asid))
+pure func (dp DataPlaneSpec) dp2_check_interface_top(d bool, asid IO_as, hf1 IO_HF) bool {
+	return (d && dp.valid_link_types_in2(hf1, asid)) || (!d && dp.valid_link_types2(hf1, asid))
 }
 
 ghost
@@ -68,12 +73,16 @@ pure func dp2_exit_interface(d bool, asid IO_as, hf1 IO_HF, outif IO_ifs) bool {
 // Takes a packet and forwards it externally, incrementing the segment before doing so.
 ghost
 requires dp.Valid()
+requires dp.Asid() == asid
 decreases
 pure func (dp DataPlaneSpec) dp2_forward_ext_guard(asid IO_as, m IO_pkt2, nextif IO_ifs, currseg, traversedseg IO_seg2, newpkt IO_pkt2, fut seq[IO_HF], hf1 IO_HF) bool {
 	return m.CurrSeg == currseg &&
 		newpkt == IO_pkt2(IO_Packet2{traversedseg, m.LeftSeg, m.MidSeg, m.RightSeg}) &&
 		// The outgoing interface is correct:
 		dp2_exit_interface(currseg.ConsDir, asid, hf1, nextif) &&
+		// Next check topologies of links if we do not come from a switch (in which case history=[])
+		(len(currseg.History) > 0 && dp.dp2_check_interface_top(currseg.ConsDir, asid, hf1) || 
+		len(currseg.History) == 0) &&
 		// Next validate the current hop field with the *original* UInfo field):
 		dp.hf_valid(currseg.ConsDir, currseg.AInfo, currseg.UInfo, hf1) &&
 		hf1.extr_asid() == asid &&