precondition for link_type function

mlimbeck · Nov 15, 2023 · 59d3019 · 59d3019
1 parent 6bf4081
commit 59d3019
Show file tree

Hide file tree

Showing 5 changed files with 30 additions and 12 deletions.
diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra
@@ -50,11 +50,11 @@ decreases
 pure func CBio_IN_bio3s_enter_T(t Place, v IO_val) Place
 
 /*** Helper functions, not in Isabelle ***/
-//Establishes the traversed segment for packets which are not incremented (internal).
+// Establishes the traversed segment for packets which are not incremented (internal).
 ghost
 requires len(currseg.Future) > 0
 decreases
-pure func EstablishGuardTraversedseg(currseg IO_seg3) IO_seg3 {
+pure func establishGuardTraversedseg(currseg IO_seg3) IO_seg3 {
 	return let uinfo := !currseg.ConsDir ?
 		upd_uinfo(currseg.UInfo, currseg.Future[0]) :
 		currseg.UInfo in
@@ -68,11 +68,11 @@ pure func EstablishGuardTraversedseg(currseg IO_seg3) IO_seg3 {
 			History: currseg.History}
 }
 
-//Establishes the traversed segment for packets that are incremented (external).
+// Establishes the traversed segment for packets that are incremented (external).
 ghost
 requires len(currseg.Future) > 0
 decreases
-pure func EstablishGuardTraversedsegInc(currseg IO_seg3) IO_seg3 {
+pure func establishGuardTraversedsegInc(currseg IO_seg3) IO_seg3 {
 	return let uinfo := !currseg.ConsDir ?
 		upd_uinfo(currseg.UInfo, currseg.Future[0]) :
 		currseg.UInfo in
@@ -100,9 +100,9 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local
 		let hf1, fut := currseg.Future[0], currseg.Future[1:] in
 		let traversedseg := match v.IO_Internal_val1_4{
 			case none[IO_ifs]: 
-				EstablishGuardTraversedseg(currseg)
+				establishGuardTraversedseg(currseg)
 			default: 
-				EstablishGuardTraversedsegInc(currseg)
+				establishGuardTraversedsegInc(currseg)
 		} in
 		dp.dp2_enter_guard(
 			v.IO_Internal_val1_1,
@@ -161,7 +161,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta
 				len(currseg.Future) > 0 &&
 				len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 &&
 				let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in
-				let traversedseg := EstablishGuardTraversedsegInc(currseg) in
+				let traversedseg := establishGuardTraversedsegInc(currseg) in
 				(dp.xover_up2down2_link_type(dp.Asid(), hf1, hf2) &&
 					dp.dp3s_xover_common(
 						s,
@@ -216,7 +216,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_
 				len(currseg.Future) > 0 &&
 				len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 &&
 				let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in
-				let traversedseg := EstablishGuardTraversedsegInc(currseg) in
+				let traversedseg := establishGuardTraversedsegInc(currseg) in
 				(dp.xover_core2_link_type(hf1, hf2, dp.Asid(), currseg.ConsDir) &&
 					dp.dp3s_xover_common(
 						s,

diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra
@@ -120,18 +120,20 @@ type IO_Link adt {
 	IO_NoLink{}
 }
 
-// TODO: should be put p1 == dp.Asid() in the precondition?
-// Should we put dp.Valid() in precondition?
 // This function is provided as locale in the Isabelle formalization.
+// This function is only ever called with p1 == dp.Asid(). As a future optimization
+// this parameter and precondition can be dropped.
 ghost
 requires dp.Valid()
+requires p1 == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{
 	return p2 in domain(dp.linkTypes) ? dp.linkTypes[p2] : IO_NoLink{}
 }
 
 ghost
 requires dp.Valid()
+requires asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) egif_prov2(hf1 IO_HF, asid IO_as) bool{
 	return dp.egif2_type(hf1, asid, IO_Link(IO_CustProv{}))
@@ -140,41 +142,47 @@ pure func (dp DataPlaneSpec) egif_prov2(hf1 IO_HF, asid IO_as) bool{
 
 ghost
 requires dp.Valid()
+requires asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) egif_core2(hf1 IO_HF, asid IO_as) bool{
 	return dp.egif2_type(hf1, asid, IO_Link(IO_PeerOrCore{}))
 }
 
 ghost
 requires dp.Valid()
+requires asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) egif_cust2(hf1 IO_HF, asid IO_as) bool{
 	return dp.egif2_type(hf1, asid, IO_Link(IO_ProvCust{}))
 }
 
 ghost
 requires dp.Valid()
+requires asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) inif_cust2(hf1 IO_HF, asid IO_as) bool{
 	return dp.inif2_type(hf1, asid, IO_Link(IO_ProvCust{}))
 }
 
 ghost
 requires dp.Valid()
+requires asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) inif_core2(hf1 IO_HF, asid IO_as) bool{
 	return dp.inif2_type(hf1, asid, IO_Link(IO_PeerOrCore{}))
 }
 
 ghost
 requires dp.Valid()
+requires asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) inif_prov2(hf1 IO_HF, asid IO_as) bool{
 	return dp.inif2_type(hf1, asid, IO_Link(IO_CustProv{}))
 }
 
 ghost
 requires dp.Valid()
+requires ifs != none[IO_ifs] ==> asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool{
 	return match ifs {

diff --git a/verification/io/router.gobra b/verification/io/router.gobra
@@ -126,7 +126,7 @@ 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
+		let traversedseg := establishGuardTraversedsegInc(currseg) in
 		dp.dp2_forward_ext_guard(dp.Asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) &&
 		let a2 := dp.GetNeighborIA(nextif) in
 		let i2 := dp.Lookup(AsIfsPair{dp.Asid(), nextif}).ifs in
@@ -168,6 +168,6 @@ pure func (dp DataPlaneSpec) dp3s_xover_common(
 		// this is because of the way math. maps are implemented, we can only obtain a key that is in the map before.
 		return some(recvif) in domain(s.ibuf) &&
 			(let lookupRes := s.ibuf[some(recvif)] in (m in lookupRes)) &&
-			dp.dp2_xover_common_guard(m, currseg, nextseg, traversedseg, intermediatepkt, hf1, hf2, hf1.extr_asid(), recvif) &&
+			dp.dp2_xover_common_guard(m, currseg, nextseg, traversedseg, intermediatepkt, hf1, hf2, dp.Asid(), recvif) &&
 			dp.dp3s_forward(intermediatepkt, newpkt, nextif)
 }
diff --git a/verification/io/router_events.gobra b/verification/io/router_events.gobra
@@ -20,6 +20,7 @@ package io
 
 ghost
 requires dp.Valid()
+requires asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs) bool {
 	return d?
@@ -30,6 +31,7 @@ pure func (dp DataPlaneSpec) dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs)
 /* Abbreviations */
 ghost
 requires dp.Valid()
+requires a == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) valid_link_types2(hf1 IO_HF, a IO_as) bool {
 	return  (dp.egif_prov2(hf1, a) && dp.inif_cust2(hf1, a)) ||
@@ -39,6 +41,7 @@ pure func (dp DataPlaneSpec) valid_link_types2(hf1 IO_HF, a IO_as) bool {
 
 ghost
 requires dp.Valid()
+requires a == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) valid_link_types_in2(hf1 IO_HF, a IO_as) bool {
 	return  (dp.inif_prov2(hf1, a) && dp.egif_cust2(hf1, a)) ||
@@ -49,6 +52,7 @@ pure func (dp DataPlaneSpec) valid_link_types_in2(hf1 IO_HF, a IO_as) bool {
 
 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)) ||
@@ -85,6 +89,7 @@ pure func (dp DataPlaneSpec) dp2_forward_ext_guard(asid IO_as, m IO_pkt2, nextif
 // A packet is received from an ext state (i.e., an inter-AS channel) and is forwarded (either internally or externally)
 ghost
 requires dp.Valid()
+requires asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) dp2_enter_guard(m IO_pkt2, currseg IO_seg2, traversedseg IO_seg2, asid IO_as, hf1 IO_HF, recvif IO_ifs, fut seq[IO_HF]) bool {
 	return m.CurrSeg == currseg &&

diff --git a/verification/io/xover.gobra b/verification/io/xover.gobra
@@ -36,6 +36,7 @@ package io
 // the new segment that we are xovering over to.
 ghost
 requires dp.Valid()
+requires asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2,
 	currseg IO_seg2,
@@ -66,20 +67,23 @@ pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2,
 
 ghost
 requires dp.Valid()
+requires a == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) egif2_type(hf IO_HF, a IO_as, link IO_Link) bool {
 	return dp.if_type(a, hf.EgIF2, link)
 }
 
 ghost
 requires dp.Valid()
+requires a == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) inif2_type(hf IO_HF, a IO_as, link IO_Link) bool {
 	return dp.if_type(a, hf.InIF2, link)
 }
 
 ghost
 requires dp.Valid()
+requires asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) xover_up2down2_link_type(asid IO_as, hf1 IO_HF, hf2 IO_HF) bool {
 	return (dp.egif2_type(hf1, asid, IO_ProvCust{}) && dp.egif2_type(hf2, asid, IO_ProvCust{})) ||
@@ -89,6 +93,7 @@ pure func (dp DataPlaneSpec) xover_up2down2_link_type(asid IO_as, hf1 IO_HF, hf2
 
 ghost
 requires dp.Valid()
+requires asid == dp.Asid()
 decreases
 pure func (dp DataPlaneSpec) xover_core2_link_type(hf1 IO_HF, hf2 IO_HF, asid IO_as, d bool) bool {
 	return (!d && dp.egif2_type(hf1, asid, IO_ProvCust{}) && dp.inif2_type(hf2, asid, IO_PeerOrCore{})) ||