renaming core and asid function

viperproject · Nov 14, 2023 · 6be6ae6 · 6be6ae6
1 parent 193add2
commit 6be6ae6
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 14 deletions.
diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra
@@ -77,17 +77,15 @@ pure func (dp DataPlaneSpec) GetNeighborIA(ifs IO_ifs) IO_as {
 	return dp.neighborIAs[ifs]
 }
 
-// This function corresponds to function 'asid' in the IO spec
 ghost
 decreases
-pure func (dp DataPlaneSpec) GetLocalIA() IO_as {
+pure func (dp DataPlaneSpec) Asid() 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] {
+pure func (dp DataPlaneSpec) Core() set[IO_as] {
 	return dp.topology.coreAS
 }
 

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.GetLocalIA(),
+			dp.Asid(),
 			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.GetLocalIA(), hf1, hf2) &&
+				(dp.xover_up2down2_link_type(dp.Asid(), 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.GetLocalIA() in dp.GetCoreAS() &&
+	return (dp.Asid() in dp.Core() &&
 		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.GetLocalIA(), currseg.ConsDir) &&
+				(dp.xover_core2_link_type(hf1, hf2, dp.Asid(), 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
@@ -120,7 +120,7 @@ type IO_Link adt {
 	IO_NoLink{}
 }
 
-// TODO: should be put p1 == dp.GetLocalIA() in the precondition?
+// 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.
 ghost

diff --git a/verification/io/router.gobra b/verification/io/router.gobra
@@ -43,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.GetLocalIA())), l)
+		x == mac(macKey(asidToKey(dp.Asid())), l)
 }
 
 ghost
@@ -80,7 +80,7 @@ pure func upd_uinfo(segid set[IO_msgterm], hf IO_HF) set[IO_msgterm]{
 ghost
 decreases
 pure func (dp DataPlaneSpec) asid() IO_as {
-	return dp.GetLocalIA()
+	return dp.Asid()
 }
 
 
@@ -127,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.GetLocalIA(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) &&
+		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.GetLocalIA(), nextif}).ifs in
-		dp.is_target(dp.GetLocalIA(), nextif, a2, i2)
+		let i2 := dp.Lookup(AsIfsPair{dp.Asid(), nextif}).ifs in
+		dp.is_target(dp.Asid(), nextif, a2, i2)
 }
 
 // TODO: should we change IO_ifs to being implemented as an option type?