Merge branch 'master' into io-spec-in-Run

mlimbeck · Feb 19, 2024 · 9258b54 · 9258b54
2 parents f892030 + 27ea1df
commit 9258b54
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 5 deletions.
diff --git a/verification/io/router.gobra b/verification/io/router.gobra
@@ -126,8 +126,9 @@ decreases
 pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif IO_ifs) bool {
 	return let currseg := m.CurrSeg in
 		let hf1, fut := currseg.Future[0], currseg.Future[1:] in
-		let traversedseg := establishGuardTraversedsegInc(currseg) in
-		dp.dp2_forward_ext_guard(dp.Asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) &&
+		let traversedseg := newpkt.CurrSeg in
+		dp.dp2_forward_ext_guard(dp.Asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) && 
+		(nextif in domain(dp.GetNeighborIAs())) &&
 		let a2 := dp.GetNeighborIA(nextif) in
 		let i2 := dp.Lookup(AsIfsPair{dp.Asid(), nextif}).ifs in
 		dp.is_target(dp.Asid(), nextif, a2, i2)

diff --git a/verification/io/router_events.gobra b/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 &&