From 10676f7cc136ca60807dd5f8f4b64a6eceaf4993 Mon Sep 17 00:00:00 2001 From: Markus Limbeck <92801626+mlimbeck@users.noreply.github.com> Date: Wed, 18 Oct 2023 18:00:14 +0200 Subject: [PATCH] Adding DataPlaneSpec to the IO-spec (#230) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * making IO-spec dependend on abstract dataplane * renaming Abs_Dataplane to DataPlaneSpec * removing local state from IO-spec next place functions * rewriting IO-spec with match clause * comment out unnecessary functions * cosmetic changes * documentation for DataPlaneSpec and Valid function * Apply suggestions from code review Co-authored-by: João Pereira * cosmetic changes * fix comment * cosmetic changes * guards require correct type --------- Co-authored-by: João Pereira --- verification/io/dataplane_abstract.gobra | 72 +++++++ verification/io/io-spec.gobra | 250 +++++++++++++---------- verification/io/other_defs.gobra | 52 +---- verification/io/router.gobra | 39 ++-- verification/io/router_events.gobra | 93 +++------ verification/io/segment-defs.gobra | 16 +- verification/io/xover.gobra | 100 ++------- 7 files changed, 301 insertions(+), 321 deletions(-) create mode 100644 verification/io/dataplane_abstract.gobra diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra new file mode 100644 index 000000000..f6fda5352 --- /dev/null +++ b/verification/io/dataplane_abstract.gobra @@ -0,0 +1,72 @@ +// Copyright 2022 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package io + +type DataPlaneSpec adt { + DataPlaneSpec_{ + linkTypes dict[IO_ifs]IO_Link + neighborIAs dict[IO_ifs]IO_as + localIA IO_as + topology TopologySpec + } +} + +// TopologySpec provides information about the entire network topology. +// coreAS: IDs of the core Autonomous Systems +// links: representation of the network topology as a graph. +// links[a1][1] == a2 means that AS a1 has an edge to AS a2 via interface 1. +type TopologySpec adt { + TopologySpec_{ + coreAS set[IO_as] + links dict[IO_as](dict[IO_ifs]IO_as) + } +} + +ghost +decreases +pure func (dp DataPlaneSpec) Valid() bool{ + return domain(dp.linkTypes) == domain(dp.neighborIAs) && + dp.localIA in domain(dp.topology.links) && + dp.neighborIAs == dp.topology.links[dp.localIA] && + (forall core IO_as :: {core in dp.topology.coreAS} core in dp.topology.coreAS ==> core in domain(dp.topology.links)) +} + +ghost +decreases +requires ifs in domain(dp.linkTypes) +pure func (dp DataPlaneSpec) GetLinkType(ifs IO_ifs) IO_Link { + return dp.linkTypes[ifs] +} + +ghost +requires ifs in domain(dp.neighborIAs) +decreases +pure func (dp DataPlaneSpec) GetNeighborIA(ifs IO_ifs) IO_as { + return dp.neighborIAs[ifs] +} + +ghost +decreases +pure func (dp DataPlaneSpec) GetLocalIA() IO_as { + return dp.localIA +} + +ghost +decreases +pure func (dp DataPlaneSpec) GetCoreAS() set[IO_as] { + return dp.topology.coreAS +} diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 9d37f7e1e..652c59a1c 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -19,15 +19,15 @@ package io // This is the main IO Specification. -pred dp3s_iospec_ordered(s IO_dp3s_state_local, t Place) { - dp3s_iospec_bio3s_enter(s, t) && - dp3s_iospec_bio3s_xover_up2down(s, t) && - dp3s_iospec_bio3s_xover_core(s, t) && - dp3s_iospec_bio3s_exit(s, t) && - dp3s_iospec_bio3s_send(s, t) && - dp3s_iospec_bio3s_recv(s, t) && - dp3s_iospec_skip(s, t) && - dp3s_iospec_stop(s, t) +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_core(s, t) && + dp.dp3s_iospec_bio3s_exit(s, t) && + dp.dp3s_iospec_bio3s_send(s, t) && + dp.dp3s_iospec_bio3s_recv(s, t) && + dp.dp3s_iospec_skip(s, t) && + dp.dp3s_iospec_stop(s, t) } type Place int @@ -43,15 +43,15 @@ pred CBio_IN_bio3s_enter(t Place, v IO_val) ghost requires CBio_IN_bio3s_enter(t, v) decreases -pure func CBio_IN_bio3s_enter_T(s IO_dp3s_state_local, t Place, v IO_val) Place +pure func CBio_IN_bio3s_enter_T(t Place, v IO_val) Place ghost requires len(currseg.Future) > 0 decreases -pure func dp3s_iospec_bio3s_create_guard_traversedseg(currseg IO_seg3) IO_seg3 { +pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg(currseg IO_seg3) IO_seg3 { return let uinfo := !currseg.ConsDir ? - upd_uinfo(currseg.UInfo, currseg.Future[0]) : + dp.upd_uinfo(currseg.UInfo, currseg.Future[0]) : currseg.UInfo in IO_seg3_ { AInfo: currseg.AInfo, @@ -65,23 +65,24 @@ pure func dp3s_iospec_bio3s_create_guard_traversedseg(currseg IO_seg3) IO_seg3 { // This corresponds to the condition of the if statement in the io-spec case for enter ghost +requires v.isIO_Internal_val1 decreases -pure func dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { +pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { return some(v.IO_Internal_val1_2) in domain(s.ibuf) ==> (let ibuf_set := s.ibuf[some(v.IO_Internal_val1_2)] in (v.IO_Internal_val1_1 in ibuf_set)) && len(v.IO_Internal_val1_1.CurrSeg.Future) > 0 && let currseg := v.IO_Internal_val1_1.CurrSeg in let hf1, fut := currseg.Future[0], currseg.Future[1:] in - let traversedseg := dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in - dp2_enter_guard( + let traversedseg := dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in + dp.dp2_enter_guard( v.IO_Internal_val1_1, currseg, traversedseg, - asid(), + dp.asid(), hf1, v.IO_Internal_val1_2, fut) && - dp3s_forward( + dp.dp3s_forward( IO_pkt2( IO_Packet2{ traversedseg, @@ -92,79 +93,97 @@ pure func dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local, t Place, v IO_val v.IO_Internal_val1_4) } -pred dp3s_iospec_bio3s_enter(s IO_dp3s_state_local, t Place) { +pred (dp DataPlaneSpec) dp3s_iospec_bio3s_enter(s IO_dp3s_state_local, t Place) { // TODO: we may need more triggering terms here - forall v IO_val :: { dp3s_iospec_bio3s_enter_guard(s, t, v) } (v.isIO_Internal_val1 ==> - (dp3s_iospec_bio3s_enter_guard(s, t, v) ==> + forall v IO_val :: { dp.dp3s_iospec_bio3s_enter_guard(s, t, v) } ( + match v { + case IO_Internal_val1{_, _, ?newpkt, ?nextif}: + (dp.dp3s_iospec_bio3s_enter_guard(s, t, v) ==> (CBio_IN_bio3s_enter(t, v) && - dp3s_iospec_ordered( - dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), - CBio_IN_bio3s_enter_T(s, t, v))))) + dp.dp3s_iospec_ordered( + dp.dp3s_add_obuf(s, nextif, newpkt), + CBio_IN_bio3s_enter_T(t, v)))) + default: true + }) } pred CBio_IN_bio3s_xover_up2down(t Place, v IO_val) ghost requires CBio_IN_bio3s_xover_up2down(t, v) -pure func dp3s_iospec_bio3s_xover_up2down_T(s IO_dp3s_state_local, t Place, v IO_val) Place +pure func dp3s_iospec_bio3s_xover_up2down_T(t Place, v IO_val) Place // This corresponds to the condition of the if statement in the io-spec case for xover_up2down ghost +requires v.isIO_Internal_val1 decreases -pure func dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { - return let currseg := v.IO_Internal_val1_1.CurrSeg in - v.IO_Internal_val1_1.LeftSeg == none[IO_seg2] ? false : - let nextseg := get(v.IO_Internal_val1_1.LeftSeg) in - (nextseg.ConsDir && - len(nextseg.Future) > 0 && - len(currseg.Future) > 0 && - let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in - let traversedseg := dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in - (xover_up2down2_link_type(asid(), hf1, hf2) && - 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, - v.IO_Internal_val1_2, - v.IO_Internal_val1_3, - v.IO_Internal_val1_4,))) +pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_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]: + false + default: + let nextseg := get(v.IO_Internal_val1_1.LeftSeg) in + (nextseg.ConsDir && + len(nextseg.Future) > 0 && + len(currseg.Future) > 0 && + let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in + let traversedseg := dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in + (dp.xover_up2down2_link_type(dp.asid(), hf1, 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, + v.IO_Internal_val1_2, + v.IO_Internal_val1_3, + v.IO_Internal_val1_4,))) + } } -pred dp3s_iospec_bio3s_xover_up2down(s IO_dp3s_state_local, t Place) { - forall v IO_val :: { dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) }{ CBio_IN_bio3s_xover_up2down(t, v) } { dp3s_iospec_ordered(dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_up2down_T(s, t, v)) } (v.isIO_Internal_val1 ==> - (dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==> - (CBio_IN_bio3s_xover_up2down(t, v) && - dp3s_iospec_ordered( - dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), - dp3s_iospec_bio3s_xover_up2down_T(s, t, v))))) +pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down(s IO_dp3s_state_local, t Place) { + forall v IO_val :: { dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) }{ CBio_IN_bio3s_xover_up2down(t, v) } { dp.dp3s_iospec_ordered(dp.dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_up2down_T(t, v)) } ( + match v { + case IO_Internal_val1{_, _, ?newpkt, ?nextif}: + (dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==> + (CBio_IN_bio3s_xover_up2down(t, v) && + dp.dp3s_iospec_ordered( + dp.dp3s_add_obuf(s, nextif, newpkt), + dp3s_iospec_bio3s_xover_up2down_T(t, v)))) + default: + true + }) } pred CBio_IN_bio3s_xover_core(t Place, v IO_val) ghost requires CBio_IN_bio3s_xover_core(t, v) -pure func dp3s_iospec_bio3s_xover_core_T(s IO_dp3s_state_local, t Place, v IO_val) Place +pure func dp3s_iospec_bio3s_xover_core_T(t Place, v IO_val) Place // This corresponds to the condition of the if statement in the io-spec case for xover_core ghost decreases -pure func dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { - return (asid() in core_as_set() && +requires v.isIO_Internal_val1 +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() && let currseg := v.IO_Internal_val1_1.CurrSeg in - (v.IO_Internal_val1_1.LeftSeg == none[IO_seg2] ? false : - let nextseg := get(v.IO_Internal_val1_1.LeftSeg) in + match v.IO_Internal_val1_1.LeftSeg { + case none[IO_seg2]: + false + default: + let nextseg := get(v.IO_Internal_val1_1.LeftSeg) in currseg.ConsDir == nextseg.ConsDir && len(nextseg.Future) > 0 && len(currseg.Future) > 0 && let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in - let traversedseg := dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in - (xover_core2_link_type(hf1, hf2, asid(), currseg.ConsDir) && - dp3s_xover_common( + let traversedseg := dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in + (dp.xover_core2_link_type(hf1, hf2, dp.asid(), currseg.ConsDir) && + dp.dp3s_xover_common( s, v.IO_Internal_val1_1, currseg, @@ -175,16 +194,22 @@ pure func dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v I hf2, v.IO_Internal_val1_2, v.IO_Internal_val1_3, - v.IO_Internal_val1_4)))) + v.IO_Internal_val1_4)) + }) } -pred dp3s_iospec_bio3s_xover_core(s IO_dp3s_state_local, t Place) { - forall v IO_val :: { dp3s_iospec_bio3s_xover_core_guard(s, t, v) }{ CBio_IN_bio3s_xover_core(t, v) }{ dp3s_iospec_ordered(dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_core_T(s, t, v)) } (v.isIO_Internal_val1 ==> - (dp3s_iospec_bio3s_xover_core_guard(s, t, v) ==> - (CBio_IN_bio3s_xover_core(t, v) && - dp3s_iospec_ordered( - dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), - dp3s_iospec_bio3s_xover_core_T(s, t, v))))) +pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core(s IO_dp3s_state_local, t Place) { + forall v IO_val :: { dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) }{ CBio_IN_bio3s_xover_core(t, v) }{ dp.dp3s_iospec_ordered(dp.dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_core_T(t, v)) } ( + match v { + case IO_Internal_val1{_, _, ?newpkt, ?nextif}: + (dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) ==> + (CBio_IN_bio3s_xover_core(t, v) && + dp.dp3s_iospec_ordered( + dp.dp3s_add_obuf(s, nextif, newpkt), + dp3s_iospec_bio3s_xover_core_T(t, v)))) + default: + true + }) } @@ -192,24 +217,30 @@ pred CBio_IN_bio3s_exit(t Place, v IO_val) ghost requires CBio_IN_bio3s_exit(t, v) -pure func dp3s_iospec_bio3s_exit_T(s IO_dp3s_state_local, t Place, v IO_val) Place +pure func dp3s_iospec_bio3s_exit_T(t Place, v IO_val) Place // This corresponds to the condition of the if statement in the io-spec case for exit ghost +requires v.isIO_Internal_val2 decreases -pure func dp3s_iospec_bio3s_exit_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { +pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_exit_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { return none[IO_ifs] in domain(s.ibuf) ==> (let ibuf_set := s.ibuf[none[IO_ifs]] in (v.IO_Internal_val2_1 in ibuf_set)) && - dp3s_forward_ext(v.IO_Internal_val2_1, v.IO_Internal_val2_2, v.IO_Internal_val2_3) + dp.dp3s_forward_ext(v.IO_Internal_val2_1, v.IO_Internal_val2_2, v.IO_Internal_val2_3) } -pred dp3s_iospec_bio3s_exit(s IO_dp3s_state_local, t Place) { - forall v IO_val :: { dp3s_iospec_bio3s_exit_guard(s, t, v) }{ CBio_IN_bio3s_exit(t, v) }{ dp3s_iospec_ordered(dp3s_add_obuf(s, some(v.IO_Internal_val2_3), v.IO_Internal_val2_2), dp3s_iospec_bio3s_exit_T(s, t, v)) } (v.isIO_Internal_val2 ==> - (dp3s_iospec_bio3s_exit_guard(s, t, v) ==> - (CBio_IN_bio3s_exit(t, v) && - dp3s_iospec_ordered( - dp3s_add_obuf(s, some(v.IO_Internal_val2_3), v.IO_Internal_val2_2), - dp3s_iospec_bio3s_exit_T(s, t, v))))) +pred (dp DataPlaneSpec) dp3s_iospec_bio3s_exit(s IO_dp3s_state_local, t Place) { + forall v IO_val :: { dp.dp3s_iospec_bio3s_exit_guard(s, t, v) }{ CBio_IN_bio3s_exit(t, v) }{ dp.dp3s_iospec_ordered(dp.dp3s_add_obuf(s, some(v.IO_Internal_val2_3), v.IO_Internal_val2_2), dp3s_iospec_bio3s_exit_T(t, v)) } ( + match v { + case IO_Internal_val2{_, ?newpkt, ?nextif}: + (dp.dp3s_iospec_bio3s_exit_guard(s, t, v) ==> + (CBio_IN_bio3s_exit(t, v) && + dp.dp3s_iospec_ordered( + dp.dp3s_add_obuf(s, some(nextif), newpkt), + dp3s_iospec_bio3s_exit_T(t, v)))) + default: + true + }) } @@ -217,63 +248,66 @@ pred CBioIO_bio3s_send(t Place, v IO_val) ghost requires CBioIO_bio3s_send(t, v) -pure func dp3s_iospec_bio3s_send_T(s IO_dp3s_state_local, t Place, v IO_val) Place +pure func dp3s_iospec_bio3s_send_T(t Place, v IO_val) Place // This corresponds to the condition of the if statement in the io-spec case for send ghost +requires v.isIO_val_Pkt2 decreases -pure func dp3s_iospec_bio3s_send_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { +pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_send_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { return v.IO_val_Pkt2_1 in domain(s.obuf) ==> (let obuf_set := s.obuf[v.IO_val_Pkt2_1] in (v.IO_val_Pkt2_2 in obuf_set)) } // TODO: annotate WriteBatch, skipped for now -pred dp3s_iospec_bio3s_send(s IO_dp3s_state_local, t Place) { - forall v IO_val :: { dp3s_iospec_bio3s_send_guard(s, t, v) }{ CBioIO_bio3s_send(t, v) }{ dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(s, t, v)) }{ CBioIO_bio3s_send(t, v) }{ dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(s, t, v)) } (v.isIO_val_Pkt2 ==> - (dp3s_iospec_bio3s_send_guard(s, t, v) ==> - CBioIO_bio3s_send(t, v) && - dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(s, t, v)))) && - (v.isIO_val_Unsupported ==> - CBioIO_bio3s_send(t, v) && - dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(s, t, v))) +pred (dp DataPlaneSpec) dp3s_iospec_bio3s_send(s IO_dp3s_state_local, t Place) { + forall v IO_val :: { dp.dp3s_iospec_bio3s_send_guard(s, t, v) }{ CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(t, v)) }{ CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(t, v)) } ( + match v { + case IO_val_Pkt2{_, _}: + (dp.dp3s_iospec_bio3s_send_guard(s, t, v) ==> + CBioIO_bio3s_send(t, v) && + dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(t, v))) + case IO_val_Unsupported{_, _}: + (CBioIO_bio3s_send(t, v) && + dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(t, v))) + default: + true + }) } pred CBioIO_bio3s_recv(t Place) ghost requires CBioIO_bio3s_recv(t) -pure func dp3s_iospec_bio3s_recv_T(s IO_dp3s_state_local, t Place) Place +pure func dp3s_iospec_bio3s_recv_T(t Place) Place ghost requires CBioIO_bio3s_recv(t) -pure func dp3s_iospec_bio3s_recv_R(s IO_dp3s_state_local, t Place) IO_val +pure func dp3s_iospec_bio3s_recv_R(t Place) IO_val -pred dp3s_iospec_bio3s_recv(s IO_dp3s_state_local, t Place) { +pred (dp DataPlaneSpec) dp3s_iospec_bio3s_recv(s IO_dp3s_state_local, t Place) { CBioIO_bio3s_recv(t) && - (dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Pkt2 ==> - dp3s_iospec_ordered( - dp3s_add_ibuf( - s, - dp3s_iospec_bio3s_recv_R(s, t).IO_val_Pkt2_1, - dp3s_iospec_bio3s_recv_R(s, t).IO_val_Pkt2_2), - dp3s_iospec_bio3s_recv_T(s, t))) && - (dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Unsupported ==> - dp3s_iospec_ordered(s, dp3s_iospec_bio3s_recv_T(s, t))) && - ((!dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Pkt2 && !dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Unsupported) ==> - dp3s_iospec_ordered(undefined(), dp3s_iospec_bio3s_recv_T(s, t))) + (match dp3s_iospec_bio3s_recv_R(t) { + case IO_val_Pkt2{?recvif, ?pkt}: + dp.dp3s_iospec_ordered( + dp.dp3s_add_ibuf(s, recvif, pkt), dp3s_iospec_bio3s_recv_T(t)) + case IO_val_Unsupported{_, _}: + dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_recv_T(t)) + default: + dp.dp3s_iospec_ordered(undefined(), dp3s_iospec_bio3s_recv_T(t)) + }) } pred CBio_Skip(t Place) ghost requires CBio_Skip(t) -pure func dp3s_iospec_skip_T(s IO_dp3s_state_local, t Place) Place +pure func dp3s_iospec_skip_T(t Place) Place -pred dp3s_iospec_skip(s IO_dp3s_state_local, t Place) { - CBio_Skip(t) && dp3s_iospec_ordered(s, dp3s_iospec_skip_T(s, t)) +pred (dp DataPlaneSpec) dp3s_iospec_skip(s IO_dp3s_state_local, t Place) { + CBio_Skip(t) && dp.dp3s_iospec_ordered(s, dp3s_iospec_skip_T(t)) } -pred dp3s_iospec_stop(s IO_dp3s_state_local, t Place) { +pred (dp DataPlaneSpec) dp3s_iospec_stop(s IO_dp3s_state_local, t Place) { true } - diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index 70c390daf..126361f5c 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -18,8 +18,6 @@ package io -import "github.com/scionproto/scion/pkg/slayers/path" - // used everywhere where the Isabel spec has a type-parameter type TypeParameter = interface{} type TypeParameter1 = interface{} @@ -117,23 +115,6 @@ func (h IO_HF) Toab() IO_ahi { return IO_ahi_{h.InIF2, h.EgIF2, h.HVF.extract_asid()} } -// TODO: move ToHF to another package -// TODO: can we get rid of this assumption? -// We ASSUME the existence of a function that computes the msgTerm of a path.HopField -ghost -decreases -pure func ComputeMsgTerm(h path.HopField) IO_msgterm - -// TODO: should be easy to give a body to this now -ghost -ensures h.ConsIngress == 0 ==> res.InIF2 == none[IO_ifs] -ensures h.ConsIngress != 0 ==> res.InIF2 == some(IO_ifs(h.ConsIngress)) -ensures h.ConsEgress == 0 ==> res.EgIF2 == none[IO_ifs] -ensures h.ConsEgress != 0 ==> res.EgIF2 == some(IO_ifs(h.ConsIngress)) -ensures res.HVF == ComputeMsgTerm(h) -decreases -pure func ToHF(h path.HopField) (res IO_HF) - /* Link Types */ type IO_Link adt { IO_CustProv{} @@ -151,39 +132,39 @@ type IO_Link adt { ghost decreases -pure func rid_as(p IO_rid) IO_as +pure func (dp DataPlaneSpec) rid_as(p IO_rid) IO_as ghost decreases -pure func link_type(p1 IO_as, p2 IO_ifs) IO_Link +pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link ghost decreases -pure func egif_prov2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) egif_prov2(hf1 IO_HF, asid IO_as) bool ghost decreases -pure func egif_core2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) egif_core2(hf1 IO_HF, asid IO_as) bool ghost decreases -pure func egif_cust2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) egif_cust2(hf1 IO_HF, asid IO_as) bool ghost decreases -pure func inif_cust2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) inif_cust2(hf1 IO_HF, asid IO_as) bool ghost decreases -pure func inif_core2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) inif_core2(hf1 IO_HF, asid IO_as) bool ghost decreases -pure func inif_prov2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) inif_prov2(hf1 IO_HF, asid IO_as) bool ghost decreases -pure func if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool +pure func (dp DataPlaneSpec) if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool type ext2_rec struct { op1 IO_as @@ -201,22 +182,9 @@ type IO_dp2_state adt { } } -ghost -decreases -pure func dp2_add_ext(s, sprime IO_dp2_state, asid IO_as, nextif IO_ifs, newpkt IO_pkt2) bool - -ghost -decreases -pure func dp2_add_int(s, sprime IO_dp2_state, asid IO_as, newpkt IO_pkt2) bool - -ghost -decreases -pure func dp2_in_ext(s IO_dp2_state, asid IO_as, ifs IO_ifs, pkt IO_pkt2) bool - -// TODO: how is this defined? // extract_asid ghost decreases pure func (m IO_msgterm) extract_asid() IO_as -/* End of To clarify */ +/* End of To clarify */ \ No newline at end of file diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 16c78fc8e..3370e716a 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -23,33 +23,33 @@ package io // This function corresponds to function 'core' in the IO spec ghost decreases -pure func core_as_set() set[IO_as] +pure func (dp DataPlaneSpec) core() set[IO_as] ghost decreases -pure func hf_valid(p1 bool, p2 uint, p3 set[IO_msgterm], p4 IO_HF) bool +pure func (dp DataPlaneSpec) hf_valid(p1 bool, p2 uint, p3 set[IO_msgterm], p4 IO_HF) bool ghost decreases -pure func upd_uinfo(p1 set[IO_msgterm], p2 IO_HF) set[IO_msgterm] +pure func (dp DataPlaneSpec) upd_uinfo(p1 set[IO_msgterm], p2 IO_HF) set[IO_msgterm] ghost decreases -pure func rid() IO_rid +pure func (dp DataPlaneSpec) rid() IO_rid ghost decreases -pure func asid() IO_as { - return rid_as(rid()) +pure func (dp DataPlaneSpec) asid() IO_as { + return dp.rid_as(dp.rid()) } ghost decreases -pure func is_target(asid IO_as, nextif IO_ifs, a2 IO_as, i2 IO_ifs) bool +pure func (dp DataPlaneSpec) is_target(asid IO_as, nextif IO_ifs, a2 IO_as, i2 IO_ifs) bool ghost decreases -pure func dp3s_add_ibuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO_dp3s_state_local { +pure func (dp DataPlaneSpec) dp3s_add_ibuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO_dp3s_state_local { return IO_dp3s_state_local_{ ibuf: insert(s.ibuf, i, pkt), obuf: s.obuf, @@ -58,7 +58,7 @@ pure func dp3s_add_ibuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO ghost decreases -pure func dp3s_add_obuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO_dp3s_state_local { +pure func (dp DataPlaneSpec) dp3s_add_obuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO_dp3s_state_local { return IO_dp3s_state_local_{ ibuf: s.ibuf, obuf: insert(s.obuf, i, pkt), @@ -76,21 +76,26 @@ pure func insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k option[IO_ifs], v IO_ // TODO: try to remove the existencials here ghost decreases -pure func dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif IO_ifs) bool { - return (exists currseg IO_seg3, traversedseg IO_seg3, fut seq[IO_HF], hf1 IO_HF :: { dp2_forward_ext_guard(asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) } dp2_forward_ext_guard(asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1)) && - (exists a2 IO_as, i2 IO_ifs :: { is_target(asid(), nextif, a2, i2) } is_target(asid(), nextif, a2, i2)) +pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif IO_ifs) bool { + return (exists currseg IO_seg3, traversedseg IO_seg3, fut seq[IO_HF], hf1 IO_HF :: { dp.dp2_forward_ext_guard(dp.asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) } dp.dp2_forward_ext_guard(dp.asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1)) && + (exists a2 IO_as, i2 IO_ifs :: { dp.is_target(dp.asid(), nextif, a2, i2) } dp.is_target(dp.asid(), nextif, a2, i2)) } // TODO: should we change IO_ifs to being implemented as an option type? ghost decreases -pure func dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif option[IO_ifs]) bool { - return nextif == none[IO_ifs] ? newpkt == m : dp3s_forward_ext(m, newpkt, get(nextif)) +pure func (dp DataPlaneSpec) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif option[IO_ifs]) bool { + return match nextif { + case none[IO_ifs]: + newpkt == m + default: + dp.dp3s_forward_ext(m, newpkt, get(nextif)) + } } ghost decreases -pure func dp3s_xover_common( +pure func (dp DataPlaneSpec) dp3s_xover_common( s IO_dp3s_state_local, m IO_pkt3, currseg IO_seg3, @@ -107,6 +112,6 @@ pure func 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)) && - dp2_xover_common_guard(m, currseg, nextseg, traversedseg, intermediatepkt, hf1, hf2, hf1.extr_asid(), recvif) && - dp3s_forward(intermediatepkt, newpkt, nextif) + dp.dp2_xover_common_guard(m, currseg, nextseg, traversedseg, intermediatepkt, hf1, hf2, hf1.extr_asid(), recvif) && + dp.dp3s_forward(intermediatepkt, newpkt, nextif) } diff --git a/verification/io/router_events.gobra b/verification/io/router_events.gobra index ae8a1aae0..ea64ce2b7 100644 --- a/verification/io/router_events.gobra +++ b/verification/io/router_events.gobra @@ -20,112 +20,73 @@ package io ghost decreases -pure func dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs) bool { +pure func (dp DataPlaneSpec) dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs) bool { return d? - (link_type(asid, recvif) == IO_CustProv{} || link_type(asid, recvif) == IO_PeerOrCore{}) : - (link_type(asid, recvif) == IO_ProvCust{} || link_type(asid, recvif) == IO_PeerOrCore{}) + (dp.link_type(asid, recvif) == IO_CustProv{} || dp.link_type(asid, recvif) == IO_PeerOrCore{}) : + (dp.link_type(asid, recvif) == IO_ProvCust{} || dp.link_type(asid, recvif) == IO_PeerOrCore{}) } /* Abbreviations */ ghost decreases -pure func valid_link_types2(hf1 IO_HF, a IO_as) bool { - return (egif_prov2(hf1, a) && inif_cust2(hf1, a)) || - (egif_core2(hf1, a) && inif_core2(hf1, a)) || - (egif_cust2(hf1, a) && inif_prov2(hf1, a)) +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)) || + (dp.egif_core2(hf1, a) && dp.inif_core2(hf1, a)) || + (dp.egif_cust2(hf1, a) && dp.inif_prov2(hf1, a)) } ghost decreases -pure func valid_link_types_in2(hf1 IO_HF, a IO_as) bool { - return (inif_prov2(hf1, a) && egif_cust2(hf1, a)) || - (inif_core2(hf1, a) && egif_core2(hf1, a)) || - (inif_cust2(hf1, a) && egif_prov2(hf1, a)) +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)) || + (dp.inif_core2(hf1, a) && dp.egif_core2(hf1, a)) || + (dp.inif_cust2(hf1, a) && dp.egif_prov2(hf1, a)) } /* End of Abbreviations */ ghost decreases -pure func dp2_check_interface(d bool, asid IO_as, hf1 IO_HF, recvif IO_ifs) bool { - return (d && hf1.InIF2 === some(recvif) && valid_link_types_in2(hf1, asid)) || - (!d && hf1.EgIF2 === some(recvif) && valid_link_types2(hf1, asid)) +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)) || + (!d && hf1.EgIF2 === some(recvif) && dp.valid_link_types2(hf1, asid)) } ghost decreases -pure func dp2_exit_interface(d bool, asid IO_as, hf1 IO_HF, outif IO_ifs) bool { +pure func (dp DataPlaneSpec) dp2_exit_interface(d bool, asid IO_as, hf1 IO_HF, outif IO_ifs) bool { return (d && hf1.EgIF2 == some(outif)) || (!d && hf1.InIF2 == some(outif)) } // Takes a packet and forwards it externally, incrementing the segment before doing so. ghost decreases -pure func dp2_forward_ext_guard(asid IO_as, m IO_pkt2, nextif IO_ifs, currseg, traversedseg IO_seg2, newpkt IO_pkt2, fut seq[IO_HF], hf1 IO_HF) bool { +pure func (dp DataPlaneSpec) dp2_forward_ext_guard(asid IO_as, m IO_pkt2, nextif IO_ifs, currseg, traversedseg IO_seg2, newpkt IO_pkt2, fut seq[IO_HF], hf1 IO_HF) bool { return m.CurrSeg == currseg && newpkt == IO_pkt2(IO_Packet2{traversedseg, m.LeftSeg, m.MidSeg, m.RightSeg}) && // The outgoing interface is correct: - dp2_exit_interface(currseg.ConsDir, asid, hf1, nextif) && + dp.dp2_exit_interface(currseg.ConsDir, asid, hf1, nextif) && // Next validate the current hop field with the *original* UInfo field): - hf_valid(currseg.ConsDir, currseg.AInfo, currseg.UInfo, hf1) && + dp.hf_valid(currseg.ConsDir, currseg.AInfo, currseg.UInfo, hf1) && hf1.extr_asid() == asid && // Segment update: push current hop field into the Past path and History: - inc_seg2(currseg, traversedseg, hf1, fut) && + dp.inc_seg2(currseg, traversedseg, hf1, fut) && // If the current segment is an *down*-segment, then we need to update the // uinfo field *after* validating the hop field - update_uinfo(currseg.ConsDir, currseg, traversedseg, hf1) && + dp.update_uinfo(currseg.ConsDir, currseg, traversedseg, hf1) && // Other fields: no update - same_other2(currseg, traversedseg) + dp.same_other2(currseg, traversedseg) } -ghost -decreases -pure func dp2_forward_ext(s IO_dp2_state, sprime IO_dp2_state, asid IO_as, m IO_pkt2) bool { - return exists nextif IO_ifs, currseg IO_seg2, traversedseg IO_seg2, newpkt IO_pkt2, fut seq[IO_HF], hf1 IO_HF :: { dp2_forward_ext_guard(asid, m, nextif, currseg, traversedseg, newpkt, fut, hf1) }{ dp2_add_ext(s, sprime, asid, nextif, newpkt) } dp2_forward_ext_guard(asid, m, nextif, currseg, traversedseg, newpkt, fut, hf1) && - dp2_add_ext(s, sprime, asid, nextif, newpkt) - -} - -// Non-deterministically forward the packet internally or externally. In the real system, a router -// will forward a packet externally if the interface over which the packet is supposed to leave the -// AS belongs to the router itself. In all other cases, the packet will be forwarded internally. -// In case the packet is forwarded externally, additional processing is required -// (e.g., updating the uinfo field depending on direction, and incrementing the segment). -ghost -decreases -pure func dp2_forward(s IO_dp2_state, sprime IO_dp2_state, asid IO_as, m IO_pkt2) bool { - return dp2_add_int(s, sprime, asid, m) || dp2_forward_ext(s, sprime, asid, m) -} - - // A packet is received from an ext state (i.e., an inter-AS channel) and is forwarded (either internally or externally) ghost decreases -pure func 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 { +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 && - dp2_check_interface(currseg.ConsDir, asid, hf1, recvif) && - update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) && - same_segment2(currseg, traversedseg) && - same_other2(currseg, traversedseg) && - hf_valid(currseg.ConsDir, currseg.AInfo, traversedseg.UInfo, hf1) && + dp.dp2_check_interface(currseg.ConsDir, asid, hf1, recvif) && + dp.update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) && + dp.same_segment2(currseg, traversedseg) && + dp.same_other2(currseg, traversedseg) && + dp.hf_valid(currseg.ConsDir, currseg.AInfo, traversedseg.UInfo, hf1) && hf1.extr_asid() == asid } - -ghost -decreases -pure func dp2_enter(s IO_dp2_state, m IO_pkt2, currseg IO_seg2, traversedseg IO_seg2, asid IO_as, hf1 IO_HF, recvif IO_ifs, fut seq[IO_HF], sprime IO_dp2_state) bool { - return dp2_in_ext(s, asid, recvif, m) && - dp2_enter_guard(m, currseg, traversedseg, asid, hf1, recvif, fut) && - // Action: Update internal state to include packet. - dp2_forward(s, sprime, asid, IO_pkt2(IO_Packet2{traversedseg, m.LeftSeg, m.MidSeg, m.RightSeg})) -} - -ghost -decreases -pure func dp2_exit(s IO_dp2_state, m IO_pkt2, asid IO_as, sprime IO_dp2_state) bool { - // the first conjunct is not in the IO spec document but it is required in Gobra - // to make this function well formed. - return asid in domain(s.int2) && - (let img := s.int2[asid] in (m in img)) && - dp2_forward_ext(s, sprime, asid, m) -} \ No newline at end of file diff --git a/verification/io/segment-defs.gobra b/verification/io/segment-defs.gobra index 2b6dd48f1..a89feca0a 100644 --- a/verification/io/segment-defs.gobra +++ b/verification/io/segment-defs.gobra @@ -23,7 +23,7 @@ package io ghost decreases -pure func inc_seg2(currseg, traversedseg IO_seg2, hf1 IO_HF, fut seq[IO_HF]) bool { +pure func (dp DataPlaneSpec) inc_seg2(currseg, traversedseg IO_seg2, hf1 IO_HF, fut seq[IO_HF]) bool { return currseg.Future === seq[IO_HF]{hf1} ++ fut && traversedseg.Future === fut && traversedseg.Past === seq[IO_HF]{hf1} ++ currseg.Past && @@ -32,7 +32,7 @@ pure func inc_seg2(currseg, traversedseg IO_seg2, hf1 IO_HF, fut seq[IO_HF]) boo ghost decreases -pure func same_segment2(currseg, traversedseg IO_seg2) bool { +pure func (dp DataPlaneSpec) same_segment2(currseg, traversedseg IO_seg2) bool { return traversedseg.Future === currseg.Future && traversedseg.Past === currseg.Past && traversedseg.History === currseg.History @@ -40,25 +40,25 @@ pure func same_segment2(currseg, traversedseg IO_seg2) bool { ghost decreases -pure func update_uinfo2(currseg, traversedseg IO_seg2, hf1 IO_HF) bool { - return traversedseg.UInfo === upd_uinfo(currseg.UInfo, hf1) +pure func (dp DataPlaneSpec) update_uinfo2(currseg, traversedseg IO_seg2, hf1 IO_HF) bool { + return traversedseg.UInfo === dp.upd_uinfo(currseg.UInfo, hf1) } ghost decreases -pure func same_uinfo2(currseg, traversedseg IO_seg2) bool { +pure func (dp DataPlaneSpec) same_uinfo2(currseg, traversedseg IO_seg2) bool { return currseg.UInfo === traversedseg.UInfo } ghost decreases -pure func update_uinfo(condition bool, currseg, traversedseg IO_seg2, hf1 IO_HF) bool { - return condition? update_uinfo2(currseg, traversedseg, hf1) : same_uinfo2(currseg, traversedseg) +pure func (dp DataPlaneSpec) update_uinfo(condition bool, currseg, traversedseg IO_seg2, hf1 IO_HF) bool { + return condition? dp.update_uinfo2(currseg, traversedseg, hf1) : dp.same_uinfo2(currseg, traversedseg) } ghost decreases -pure func same_other2(currseg, traversedseg IO_seg3) bool { +pure func (dp DataPlaneSpec) same_other2(currseg, traversedseg IO_seg3) bool { return traversedseg.AInfo === currseg.AInfo && traversedseg.ConsDir === currseg.ConsDir && traversedseg.Peer === currseg.Peer diff --git a/verification/io/xover.gobra b/verification/io/xover.gobra index 493182138..82a95c0ee 100644 --- a/verification/io/xover.gobra +++ b/verification/io/xover.gobra @@ -18,8 +18,6 @@ package io -// TODO: delete everything except guards - // Xover events are similar to the enter event in that a packet is received form an external // channel and forwarded (internally or externally), but in contrast to the enter event, // additional processing steps are required to switch from the current segment, @@ -38,7 +36,7 @@ package io // the new segment that we are xovering over to. ghost decreases -pure func dp2_xover_common_guard(m IO_pkt2, +pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2, currseg IO_seg2, nextseg IO_seg2, traversedseg IO_seg2, @@ -54,98 +52,40 @@ pure func dp2_xover_common_guard(m IO_pkt2, currseg.Future == seq[IO_HF]{hf1} && len(nextseg.Future) > 0 && nextseg.Future[0] == hf2 && - dp2_check_interface(currseg.ConsDir, asid, hf1, recvif) && - dp2_check_recvif(currseg.ConsDir, asid, recvif) && - update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) && - inc_seg2(currseg, traversedseg, hf1, seq[IO_HF]{}) && - hf_valid(currseg.ConsDir, currseg.AInfo, traversedseg.UInfo, hf1) && - hf_valid(nextseg.ConsDir, nextseg.AInfo, nextseg.UInfo, hf2) && + dp.dp2_check_interface(currseg.ConsDir, asid, hf1, recvif) && + dp.dp2_check_recvif(currseg.ConsDir, asid, recvif) && + dp.update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) && + dp.inc_seg2(currseg, traversedseg, hf1, seq[IO_HF]{}) && + dp.hf_valid(currseg.ConsDir, currseg.AInfo, traversedseg.UInfo, hf1) && + dp.hf_valid(nextseg.ConsDir, nextseg.AInfo, nextseg.UInfo, hf2) && hf1.extr_asid() == asid && hf2.extr_asid() == asid && - same_other2(currseg, traversedseg) -} - -ghost -decreases -pure func dp2_xover_common( - s IO_dp2_state, - m IO_pkt2, - currseg IO_seg2, - nextseg IO_seg2, - traversedseg IO_seg2, - newpkt IO_pkt2, - hf1 IO_HF, - hf2 IO_HF, - asid IO_as, - recvif IO_ifs, - sprime IO_dp2_state) bool { - return dp2_in_ext(s, asid, recvif, m) && - dp2_xover_common_guard(m, currseg, nextseg, traversedseg, newpkt, hf1, hf2, asid, recvif) && - dp2_forward(s, sprime, asid, newpkt) -} - -ghost -decreases -pure func egif2_type(hf IO_HF, a IO_as, link IO_Link) bool { - return if_type(a, hf.EgIF2, link) -} - -ghost -decreases -pure func inif2_type(hf IO_HF, a IO_as, link IO_Link) bool { - return if_type(a, hf.InIF2, link) + dp.same_other2(currseg, traversedseg) } ghost decreases -pure func xover_up2down2_link_type(asid IO_as, hf1 IO_HF, hf2 IO_HF) bool { - return (egif2_type(hf1, asid, IO_ProvCust{}) && egif2_type(hf2, asid, IO_ProvCust{})) || - (egif2_type(hf1, asid, IO_ProvCust{}) && egif2_type(hf2, asid, IO_PeerOrCore{})) || - (egif2_type(hf1, asid, IO_PeerOrCore{}) && egif2_type(hf2, asid, IO_ProvCust{})) +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 decreases -pure func dp2_xover_up2down( - s IO_dp2_state, - m IO_pkt2, - currseg IO_seg2, - nextseg IO_seg2, - traversedseg IO_seg2, - newpkt IO_pkt2, - asid IO_as, - recvif IO_ifs, - hf1 IO_HF, - hf2 IO_HF, - sprime IO_dp2_state) bool { - return !currseg.ConsDir && - nextseg.ConsDir && - xover_up2down2_link_type(asid, hf1, hf2) && - dp2_xover_common(s, m, currseg, nextseg, traversedseg, newpkt, hf1, hf2, asid, recvif, sprime) +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 decreases -pure func xover_core2_link_type(hf1 IO_HF, hf2 IO_HF, asid IO_as, d bool) bool { - return (!d && egif2_type(hf1, asid, IO_ProvCust{}) && inif2_type(hf2, asid, IO_PeerOrCore{})) || - (d && inif2_type(hf1, asid, IO_PeerOrCore{}) && egif2_type(hf2, asid, IO_ProvCust{})) +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{})) || + (dp.egif2_type(hf1, asid, IO_ProvCust{}) && dp.egif2_type(hf2, asid, IO_PeerOrCore{})) || + (dp.egif2_type(hf1, asid, IO_PeerOrCore{}) && dp.egif2_type(hf2, asid, IO_ProvCust{})) } -// TODO: how to formulate "asid in core"? -// TODO: drop ghost decreases -pure func dp2_xover_core( - s IO_dp2_state, - m IO_pkt2, - currseg IO_seg2, - nextseg IO_seg2, - traversedseg IO_seg2, - newpkt IO_pkt2, - asid IO_as, - recvif IO_ifs, - d1 bool, - hf1 IO_HF, - hf2 IO_HF, - nextfut seq[IO_HF], - sprime IO_dp2_state) bool +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{})) || + (d && dp.inif2_type(hf1, asid, IO_PeerOrCore{}) && dp.egif2_type(hf2, asid, IO_ProvCust{})) +} \ No newline at end of file