minor improvements

viperproject · Nov 14, 2023 · 4c87477 · 4c87477
1 parent 0203251
commit 4c87477
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 24 deletions.
diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra
@@ -52,8 +52,9 @@ pure func (dp DataPlaneSpec) Valid() bool {
 		(forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} AsIfsPair{dp.localIA, ifs} in domain(dp.topology.links) ==>
 			ifs in domain(dp.neighborIAs)) &&
 		(forall pairs AsIfsPair :: {dp.Lookup(pairs)} pairs in domain(dp.topology.links) ==>  
-			dp.Lookup(pairs) in domain(dp.topology.links) &&
-			dp.Lookup(dp.Lookup(pairs)) == pairs)
+			let next_pair := dp.Lookup(pairs) in
+			(next_pair in domain(dp.topology.links)) &&
+			dp.Lookup(next_pair) == pairs)
 }
 
 ghost
@@ -82,6 +83,7 @@ pure func (dp DataPlaneSpec) GetLocalIA() IO_as {
 	return dp.localIA
 }
 
+// This function corresponds to function 'core' in the IO spec
 ghost
 decreases
 pure func (dp DataPlaneSpec) GetCoreAS() set[IO_as] {

diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra
@@ -108,7 +108,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local
 			v.IO_Internal_val1_1,
 			currseg,
 			traversedseg,
-			dp.asid(),
+			dp.GetLocalIA(),
 			hf1,
 			v.IO_Internal_val1_2,
 			fut) &&
@@ -162,7 +162,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta
 				len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 &&
 				let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in
 				let traversedseg := EstablishGuardTraversedsegInc(currseg) in
-				(dp.xover_up2down2_link_type(dp.asid(), hf1, hf2) &&
+				(dp.xover_up2down2_link_type(dp.GetLocalIA(), hf1, hf2) &&
 					dp.dp3s_xover_common(
 						s,
 						v.IO_Internal_val1_1,
@@ -204,7 +204,7 @@ requires v.isIO_Internal_val1
 requires dp.Valid()
 decreases
 pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
-	return (dp.asid() in dp.core() &&
+	return (dp.GetLocalIA() in dp.GetCoreAS() &&
 		let currseg := v.IO_Internal_val1_1.CurrSeg in
 		match v.IO_Internal_val1_1.LeftSeg {
 			case none[IO_seg2]: 
@@ -217,7 +217,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_
 				len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 &&
 				let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in
 				let traversedseg := EstablishGuardTraversedsegInc(currseg) in
-				(dp.xover_core2_link_type(hf1, hf2, dp.asid(), currseg.ConsDir) &&
+				(dp.xover_core2_link_type(hf1, hf2, dp.GetLocalIA(), currseg.ConsDir) &&
 					dp.dp3s_xover_common(
 						s,
 						v.IO_Internal_val1_1,

diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra
@@ -127,12 +127,7 @@ ghost
 requires dp.Valid()
 decreases
 pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{
-	return match p1 {
-		case dp.GetLocalIA(): 
-			p2 in domain(dp.linkTypes) ? dp.linkTypes[p2] : IO_NoLink{}
-		default:
-			IO_NoLink{}
-	}
+	return p2 in domain(dp.linkTypes) ? dp.linkTypes[p2] : IO_NoLink{}
 }
 
 ghost

diff --git a/verification/io/router.gobra b/verification/io/router.gobra
@@ -20,14 +20,6 @@ package io
 
 // TODO: make individual_router an interface type with the following methods
 
-// This function corresponds to function 'core' in the IO spec
-ghost
-requires dp.Valid()
-decreases
-pure func (dp DataPlaneSpec) core() set[IO_as] {
-	return dp.GetCoreAS()
-}
-
 ghost 
 decreases
 pure func if2term(ifs option[IO_ifs]) IO_msgterm {
@@ -51,7 +43,7 @@ pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf
 				if2term(inif), 
 				if2term(egif), 
 				IO_msgterm(MsgTerm_FS{uinfo})}}) in 
-		x == mac(macKey(asidToKey(dp.asid())), l)
+		x == mac(macKey(asidToKey(dp.GetLocalIA())), l)
 }
 
 ghost
@@ -135,10 +127,10 @@ pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif
 	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) &&
+		dp.dp2_forward_ext_guard(dp.GetLocalIA(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) &&
 		let a2 := dp.GetNeighborIA(nextif) in
-		let i2 := dp.Lookup(AsIfsPair{dp.asid(), nextif}).ifs in
-		dp.is_target(dp.asid(), nextif, a2, i2)
+		let i2 := dp.Lookup(AsIfsPair{dp.GetLocalIA(), nextif}).ifs in
+		dp.is_target(dp.GetLocalIA(), nextif, a2, i2)
 }
 
 // TODO: should we change IO_ifs to being implemented as an option type?