From e8fff3b2c680baf7d39f0ec4b7fa45c72e069af7 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Fri, 12 Apr 2024 19:41:06 +0200 Subject: [PATCH 1/2] minor renaming and merging of functions --- router/io-spec-abstract-transitions.gobra | 4 +- router/io-spec-atomic-events.gobra | 20 +++----- verification/io/bios.gobra | 2 +- verification/io/io-spec.gobra | 61 +++++++++++------------ verification/io/router.gobra | 4 +- verification/io/router_events.gobra | 4 +- verification/io/xover.gobra | 11 ++-- 7 files changed, 50 insertions(+), 56 deletions(-) diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra index afd145aa0..2d36d4054 100644 --- a/router/io-spec-abstract-transitions.gobra +++ b/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) } diff --git a/router/io-spec-atomic-events.gobra b/router/io-spec-atomic-events.gobra index b93ae6ede..4b7309caa 100644 --- a/router/io-spec-atomic-events.gobra +++ b/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 diff --git a/verification/io/bios.gobra b/verification/io/bios.gobra index f85bc30db..190e6d5c5 100644 --- a/verification/io/bios.gobra +++ b/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{} } diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 625690554..c5bdfd790 100644 --- a/verification/io/io-spec.gobra +++ b/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,37 +167,36 @@ 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 }) @@ -205,7 +204,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down(s IO_dp3s_state_local, t 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 diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 0bb6d82b8..db9cabaab 100644 --- a/verification/io/router.gobra +++ b/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) } diff --git a/verification/io/router_events.gobra b/verification/io/router_events.gobra index f20449359..c03f05fad 100644 --- a/verification/io/router_events.gobra +++ b/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) && diff --git a/verification/io/xover.gobra b/verification/io/xover.gobra index eff09c6bf..98329b7e2 100644 --- a/verification/io/xover.gobra +++ b/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,7 +81,7 @@ 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{})) @@ -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)) } From 2402f931ae47a56ebcd0ee0a8966455727c388cf Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Fri, 12 Apr 2024 19:51:23 +0200 Subject: [PATCH 2/2] further renaming --- router/io-spec.gobra | 4 ++-- verification/io/other_defs.gobra | 10 +++++----- verification/io/xover.gobra | 4 ++-- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/router/io-spec.gobra b/router/io-spec.gobra index dc1377a00..dde5bc198 100644 --- a/router/io-spec.gobra +++ b/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{}) } diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index b65e70abc..d4eb1df8f 100644 --- a/verification/io/other_defs.gobra +++ b/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 } } diff --git a/verification/io/xover.gobra b/verification/io/xover.gobra index 98329b7e2..8fff431fb 100644 --- a/verification/io/xover.gobra +++ b/verification/io/xover.gobra @@ -83,8 +83,8 @@ requires asid == dp.Asid() decreases 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