Update names of functions according to the changes in the IO-spec (#314)

* minor renaming and merging of functions

* further renaming

router/io-spec-abstract-transitions.gobra

@@ -127,7 +127,7 @@ pure func AbsValidateEgressIDConstraintXover(pkt io.IO_pkt2, dp io.DataPlaneSpec
  return let currseg := pkt.CurrSeg in
  let rightseg := get(pkt.RightSeg) in
  let nextIf := (currseg.ConsDir ? currseg.Future[0].EgIF2 : currseg.Future[0].InIF2) in
- dp.xover_up2down2_link_type_dir(dp.Asid(), rightseg.ConsDir, rightseg.Past[0],
+ dp.xover2_link_type_dir(dp.Asid(), rightseg.ConsDir, rightseg.Past[0],
  currseg.ConsDir, currseg.Future[0]) &&
  nextIf != none[io.IO_ifs] &&
  (get(nextIf) in domain(dp.GetNeighborIAs()))
@@ -231,5 +231,5 @@ func XoverEvent(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], newPkt io.IO_pkt
  if(egressID != none[io.IO_ifs]){
  reveal AbsProcessEgress(intermediatePkt2)
  }
- AtomicXoverUp2Down(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp)
+ AtomicXover(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp)
 }

router/io-spec-atomic-events.gobra

@@ -108,13 +108,7 @@ requires len(oldPkt.CurrSeg.Future) > 0
 requires len(get(oldPkt.LeftSeg).Future) > 0
 requires ingressID != none[io.IO_ifs]
 requires ElemWitness(ioSharedArg.IBufY, ingressID, oldPkt)
-requires dp.xover_up2down2_link_type_dir(
- dp.Asid(),
- oldPkt.CurrSeg.ConsDir,
- oldPkt.CurrSeg.Future[0],
- get(oldPkt.LeftSeg).ConsDir,
- get(oldPkt.LeftSeg).Future[0])
-requires dp.dp2_xover_common_guard(
+requires dp.dp2_xover_guard(
  oldPkt,
  oldPkt.CurrSeg,
  get(oldPkt.LeftSeg),
@@ -140,18 +134,18 @@ requires dp.dp3s_forward_xover(
 preserves acc(ioLock.LockP(), _) && ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>;
 ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
 decreases _
-func AtomicXoverUp2Down(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], newPkt io.IO_pkt2, egressID option[io.IO_ifs], ioLock *sync.Mutex, ioSharedArg SharedArg, dp io.DataPlaneSpec) {
+func AtomicXover(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], newPkt io.IO_pkt2, egressID option[io.IO_ifs], ioLock *sync.Mutex, ioSharedArg SharedArg, dp io.DataPlaneSpec) {
  ghost ioLock.Lock()
  unfold SharedInv!< dp, ioSharedArg !>()
  t, s := *ioSharedArg.Place, *ioSharedArg.State
  ApplyElemWitness(s.ibuf, ioSharedArg.IBufY, ingressID, oldPkt)
  ghost pkt_internal := io.IO_val(io.IO_Internal_val1{oldPkt, get(ingressID), newPkt, egressID})
- assert dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, pkt_internal)
+ assert dp.dp3s_iospec_bio3s_xover_guard(s, t, pkt_internal)
  unfold dp.dp3s_iospec_ordered(s, t)
- unfold dp.dp3s_iospec_bio3s_xover_up2down(s, t)
- io.TriggerBodyIoXoverUp2Down(pkt_internal)
- tN := io.dp3s_iospec_bio3s_xover_up2down_T(t, pkt_internal)
- io.Xover_up2down(t, pkt_internal) //Event
+ unfold dp.dp3s_iospec_bio3s_xover(s, t)
+ io.TriggerBodyIoXover(pkt_internal)
+ tN := io.dp3s_iospec_bio3s_xover_T(t, pkt_internal)
+ io.Xover(t, pkt_internal) //Event
  UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt)
  ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt)
  ghost *ioSharedArg.Place = tN

router/io-spec.gobra

@@ -136,10 +136,10 @@ pure func (d *DataPlane) dpSpecWellConfiguredNeighborIAs(dp io.DataPlaneSpec) bo
 ghost
 decreases
 pure func absLinktype(link topology.LinkType) io.IO_Link {
- return link == topology.Core ? io.IO_Link(io.IO_PeerOrCore{}) :
+ return link == topology.Core ? io.IO_Link(io.IO_Core{}) :
  link == topology.Parent ? io.IO_Link(io.IO_CustProv{}) :
  link == topology.Child ? io.IO_Link(io.IO_ProvCust{}) :
- link == topology.Peer ? io.IO_Link(io.IO_PeerOrCore{}) :
+ link == topology.Peer ? io.IO_Link(io.IO_Core{}) :
  io.IO_Link(io.IO_NoLink{})
 }
 

verification/io/bios.gobra

@@ -20,7 +20,7 @@ package io
 
 type IO_bio3sIN adt {
  IO_bio3s_enter{}
- IO_bio3s_xover_up2down{}
+ IO_bio3s_xover{}
  IO_bio3s_exit{}
 }
 

verification/io/io-spec.gobra

@@ -28,7 +28,7 @@ type BogusTrigger struct{}
 // This is the main IO Specification.
 pred (dp DataPlaneSpec) dp3s_iospec_ordered(s IO_dp3s_state_local, t Place) {
  dp.dp3s_iospec_bio3s_enter(s, t) &&
- dp.dp3s_iospec_bio3s_xover_up2down(s, t) &&
+ dp.dp3s_iospec_bio3s_xover(s, t) &&
  dp.dp3s_iospec_bio3s_exit(s, t) &&
  dp.dp3s_iospec_bio3s_send(s, t) &&
  dp.dp3s_iospec_bio3s_recv(s, t) &&
@@ -143,19 +143,19 @@ ghost
 decreases
 pure func TriggerBodyIoEnter(v IO_val) BogusTrigger { return BogusTrigger{} }
 
-pred CBio_IN_bio3s_xover_up2down(t Place, v IO_val)
+pred CBio_IN_bio3s_xover(t Place, v IO_val)
 
 ghost
-requires CBio_IN_bio3s_xover_up2down(t, v)
+requires CBio_IN_bio3s_xover(t, v)
 decreases
-pure func dp3s_iospec_bio3s_xover_up2down_T(t Place, v IO_val) Place
+pure func dp3s_iospec_bio3s_xover_T(t Place, v IO_val) Place
 
-// This corresponds to the condition of the if statement in the io-spec case for xover_up2down
+// This corresponds to the condition of the if statement in the io-spec case for xover
 ghost
 requires v.isIO_Internal_val1
 requires dp.Valid()
 decreases
-pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
+pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
  return let currseg := v.IO_Internal_val1_1.CurrSeg in
  match v.IO_Internal_val1_1.LeftSeg{
  case none[IO_seg2]:
@@ -167,45 +167,44 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta
  let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in
  let traversedseg := establishGuardTraversedsegInc(currseg, !currseg.ConsDir) in
  let nextfut := nextseg.Future[1:] in
- (dp.xover_up2down2_link_type_dir(dp.Asid(), currseg.ConsDir, hf1, nextseg.ConsDir, hf2) &&
- dp.dp3s_xover_common(
- s,
- v.IO_Internal_val1_1,
- currseg,
- nextseg,
- traversedseg,
- IO_pkt2(IO_Packet2{nextseg, v.IO_Internal_val1_1.MidSeg, v.IO_Internal_val1_1.RightSeg, some(traversedseg)}),
- hf1,
- hf2,
- nextfut,
- v.IO_Internal_val1_2,
- v.IO_Internal_val1_3,
- v.IO_Internal_val1_4,)))
+ dp.dp3s_xover_guard(
+ s,
+ v.IO_Internal_val1_1,
+ currseg,
+ nextseg,
+ traversedseg,
+ IO_pkt2(IO_Packet2{nextseg, v.IO_Internal_val1_1.MidSeg, v.IO_Internal_val1_1.RightSeg, some(traversedseg)}),
+ hf1,
+ hf2,
+ nextfut,
+ v.IO_Internal_val1_2,
+ v.IO_Internal_val1_3,
+ v.IO_Internal_val1_4,))
  }
 }
 
-pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down(s IO_dp3s_state_local, t Place) {
- forall v IO_val :: { TriggerBodyIoXoverUp2Down(v) } (
+pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover(s IO_dp3s_state_local, t Place) {
+ forall v IO_val :: { TriggerBodyIoXover(v) } (
  match v {
  case IO_Internal_val1{_, _, ?newpkt, ?nextif}:
  // Gobra requires the triggering term to occur inside the qtfier body,
- // otherwise we get an error in the call to dp3s_iospec_bio3s_xover_up2down_T.
+ // otherwise we get an error in the call to dp3s_iospec_bio3s_xover_T.
  // We named the variable `_ignored` because using `_` here leads to a strange
  // type error.
- let _ignored := TriggerBodyIoXoverUp2Down(v) in
- (dp.Valid() && dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==>
- (CBio_IN_bio3s_xover_up2down(t, v) &&
+ let _ignored := TriggerBodyIoXover(v) in
+ (dp.Valid() && dp.dp3s_iospec_bio3s_xover_guard(s, t, v) ==>
+ (CBio_IN_bio3s_xover(t, v) &&
  dp.dp3s_iospec_ordered(
  dp3s_add_obuf(s, nextif, newpkt),
- dp3s_iospec_bio3s_xover_up2down_T(t, v))))
+ dp3s_iospec_bio3s_xover_T(t, v))))
  default:
  true
  })
 }
 
 ghost
 decreases
-pure func TriggerBodyIoXoverUp2Down(v IO_val) BogusTrigger { return BogusTrigger{} }
+pure func TriggerBodyIoXover(v IO_val) BogusTrigger { return BogusTrigger{} }
 
 pred CBio_IN_bio3s_exit(t Place, v IO_val)
 
@@ -347,9 +346,9 @@ func Enter(ghost t Place, ghost v IO_val)
 
 ghost
 decreases
-requires token(t) && CBio_IN_bio3s_xover_up2down(t, v)
-ensures token(old(dp3s_iospec_bio3s_xover_up2down_T(t, v)))
-func Xover_up2down(ghost t Place, ghost v IO_val)
+requires token(t) && CBio_IN_bio3s_xover(t, v)
+ensures token(old(dp3s_iospec_bio3s_xover_T(t, v)))
+func Xover(ghost t Place, ghost v IO_val)
 
 ghost
 decreases

verification/io/other_defs.gobra

@@ -108,7 +108,7 @@ func (h IO_HF) Toab() IO_ahi {
 type IO_Link adt {
  IO_CustProv{}
  IO_ProvCust{}
- IO_PeerOrCore{}
+ IO_Core{}
  IO_NoLink{}
 }
 
@@ -137,7 +137,7 @@ 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{}))
+ return dp.egif2_type(hf1, asid, IO_Link(IO_Core{}))
 }
 
 ghost
@@ -161,7 +161,7 @@ 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{}))
+ return dp.inif2_type(hf1, asid, IO_Link(IO_Core{}))
 }
 
 ghost
@@ -178,9 +178,9 @@ 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 {
- case none[IO_ifs]: 
+ case none[IO_ifs]:
  false
- default: 
+ default:
  dp.link_type(asid, get(ifs)) == link
  }
 }

verification/io/router.gobra

@@ -183,7 +183,7 @@ ghost
 requires len(intermediatepkt.CurrSeg.Future) > 0
 requires dp.Valid()
 decreases
-pure func (dp DataPlaneSpec) dp3s_xover_common(
+pure func (dp DataPlaneSpec) dp3s_xover_guard(
  s IO_dp3s_state_local,
  m IO_pkt3,
  currseg IO_seg3,
@@ -201,6 +201,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, nextfut, dp.Asid(), recvif) &&
+ dp.dp2_xover_guard(m, currseg, nextseg, traversedseg, intermediatepkt, hf1, hf2, nextfut, dp.Asid(), recvif) &&
  dp.dp3s_forward_xover(intermediatepkt, newpkt, nextif)
 }

verification/io/router_events.gobra

@@ -42,7 +42,7 @@ pure func (dp DataPlaneSpec) valid_link_types_in2(hf1 IO_HF, a IO_as) bool {
 
 ghost
 decreases
-pure func (dp DataPlaneSpec) dp2_check_interface(d bool, asid IO_as, hf1 IO_HF, recvif IO_ifs) bool {
+pure func (dp DataPlaneSpec) dp2_enter_interface(d bool, asid IO_as, hf1 IO_HF, recvif IO_ifs) bool {
  return (d && hf1.InIF2 === some(recvif)) || (!d && hf1.EgIF2 === some(recvif))
 }
 
@@ -90,7 +90,7 @@ 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 &&
  currseg.Future == seq[IO_HF]{hf1} ++ fut &&
- dp.dp2_check_interface(currseg.ConsDir, asid, hf1, recvif) &&
+ dp.dp2_enter_interface(currseg.ConsDir, asid, hf1, recvif) &&
  (dp.dp2_check_interface_top(currseg.ConsDir, asid, hf1) || fut == seq[IO_HF]{}) &&
  update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) &&
  same_segment2(currseg, traversedseg) &&

verification/io/xover.gobra

@@ -34,7 +34,7 @@ ghost
 requires dp.Valid()
 requires asid == dp.Asid()
 decreases
-pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2,
+pure func (dp DataPlaneSpec) dp2_xover_guard(m IO_pkt2,
  currseg IO_seg2,
  nextseg IO_seg2,
  traversedseg IO_seg2,
@@ -50,7 +50,8 @@ pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2,
  newpkt == IO_pkt2(IO_Packet2{nextseg, m.MidSeg, m.RightSeg, some(traversedseg)}) &&
  currseg.Future == seq[IO_HF]{hf1} &&
  nextseg.Future == seq[IO_HF]{hf2} ++ nextfut &&
- dp.dp2_check_interface(currseg.ConsDir, asid, hf1, recvif) &&
+ dp.dp2_enter_interface(currseg.ConsDir, asid, hf1, recvif) &&
+ dp.xover2_link_type_dir(dp.Asid(), currseg.ConsDir, hf1, nextseg.ConsDir, hf2) &&
  update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) &&
  inc_seg2(currseg, traversedseg, hf1, seq[IO_HF]{}) &&
  dp.hf_valid(currseg.ConsDir, currseg.AInfo, traversedseg.UInfo, hf1) &&
@@ -80,10 +81,10 @@ 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 {
+pure func (dp DataPlaneSpec) xover2_link_type(asid IO_as, hf1 IO_HF, hf2 IO_HF) bool {
  return (dp.inif2_type(hf1, asid, IO_ProvCust{}) && dp.egif2_type(hf2, asid, IO_ProvCust{})) ||
- (dp.inif2_type(hf1, asid, IO_ProvCust{}) && dp.egif2_type(hf2, asid, IO_PeerOrCore{})) ||
- (dp.inif2_type(hf1, asid, IO_PeerOrCore{}) && dp.egif2_type(hf2, asid, IO_ProvCust{}))
+ (dp.inif2_type(hf1, asid, IO_ProvCust{}) && dp.egif2_type(hf2, asid, IO_Core{})) ||
+ (dp.inif2_type(hf1, asid, IO_Core{}) && dp.egif2_type(hf2, asid, IO_ProvCust{}))
 }
 
 ghost
@@ -100,8 +101,8 @@ ghost
 requires dp.Valid()
 requires asid == dp.Asid()
 decreases
-pure func (dp DataPlaneSpec) xover_up2down2_link_type_dir(asid IO_as, d1 bool, hf1 IO_HF, d2 bool, hf2 IO_HF) bool {
- return dp.xover_up2down2_link_type(asid, swap_if_dir2(hf1, d1), swap_if_dir2(hf2, d2))
+pure func (dp DataPlaneSpec) xover2_link_type_dir(asid IO_as, d1 bool, hf1 IO_HF, d2 bool, hf2 IO_HF) bool {
+ return dp.xover2_link_type(asid, swap_if_dir2(hf1, d1), swap_if_dir2(hf2, d2))
 }