From 6ae29eb91e8209550c0dfa6f0e680d4e75bc039d Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 11 Oct 2023 15:12:44 +0200 Subject: [PATCH 01/12] making IO-spec dependend on abstract dataplane --- verification/io/dataplane_abstract.gobra | 62 +++++++ verification/io/io-spec.gobra | 212 +++++++++++------------ verification/io/other_defs.gobra | 46 ++--- verification/io/router.gobra | 40 ++--- verification/io/router_events.gobra | 112 ++++++------ verification/io/segment-defs.gobra | 16 +- verification/io/xover.gobra | 145 ++++++++-------- 7 files changed, 348 insertions(+), 285 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..8e6bf2bf2 --- /dev/null +++ b/verification/io/dataplane_abstract.gobra @@ -0,0 +1,62 @@ +// 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 Abs_Dataplane adt { + Abs_Dataplane_ { + //external seq[IO_ifs] + linkTypes dict[IO_ifs]IO_Link + neighborIAs dict[IO_ifs]IO_as + internal IO_ifs //TODO: propably not needed, = 0 + localIA IO_as + running bool //TODO: needed? + } +} + +// ghost +// requires acc(dp, _) +// pure func (dp *Abs_Dataplane) (ifs IO_ifs) seq[IO_ifs] { +// return dp.external +// } + +ghost +//requires acc(dp, _) +requires ifs in domain(dp.linkTypes) +pure func (dp Abs_Dataplane) getLinkType(ifs IO_ifs) IO_Link { + return dp.linkTypes[ifs] +} + +ghost +//requires acc(dp, _) +requires ifs in domain(dp.neighborIAs) +pure func (dp Abs_Dataplane) getNeighborIA(ifs IO_ifs) IO_as { + return dp.neighborIAs[ifs] +} + +ghost +//requires acc(dp, _) +pure func (dp Abs_Dataplane) getLocalIA() IO_as { + return dp.localIA +} + +ghost +//requires acc(dp, _) +pure func (dp Abs_Dataplane) isRunning() bool { + return dp.running +} \ No newline at end of file diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 9d37f7e1e..41bf65012 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -19,40 +19,40 @@ 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 Abs_Dataplane) 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 -pred token(t Place) +pred (dp Abs_Dataplane) token(t Place) ghost decreases -pure func undefined() IO_dp3s_state_local +pure func (dp Abs_Dataplane) undefined() IO_dp3s_state_local -pred CBio_IN_bio3s_enter(t Place, v IO_val) +pred (dp Abs_Dataplane) CBio_IN_bio3s_enter(t Place, v IO_val) ghost -requires CBio_IN_bio3s_enter(t, v) +requires dp.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 (dp Abs_Dataplane) CBio_IN_bio3s_enter_T(s IO_dp3s_state_local, 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 { - return let uinfo := !currseg.ConsDir ? - upd_uinfo(currseg.UInfo, currseg.Future[0]) : - currseg.UInfo in +pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_create_guard_traversedseg(currseg IO_seg3) IO_seg3 { + return let uinfo := !currseg.ConsDir ? + dp.upd_uinfo(currseg.UInfo, currseg.Future[0]) : + currseg.UInfo in IO_seg3_ { AInfo: currseg.AInfo, UInfo: uinfo, @@ -66,22 +66,22 @@ 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 decreases -pure func dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { +pure func (dp Abs_Dataplane) 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,26 +92,26 @@ 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 Abs_Dataplane) 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) ==> - (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))))) + forall v IO_val :: { dp.dp3s_iospec_bio3s_enter_guard(s, t, v) } (v.isIO_Internal_val1 ==> + (dp.dp3s_iospec_bio3s_enter_guard(s, t, v) ==> + (dp.CBio_IN_bio3s_enter(t, v) && + dp.dp3s_iospec_ordered( + dp.dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), + dp.CBio_IN_bio3s_enter_T(s, t, v))))) } -pred CBio_IN_bio3s_xover_up2down(t Place, v IO_val) +pred (dp Abs_Dataplane) 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 +requires dp.CBio_IN_bio3s_xover_up2down(t, v) +pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_xover_up2down_T(s IO_dp3s_state_local, t Place, v IO_val) Place // This corresponds to the condition of the if statement in the io-spec case for xover_up2down ghost decreases -pure func dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { +pure func (dp Abs_Dataplane) 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 @@ -119,9 +119,9 @@ pure func dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_state_local, t Place, 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( + 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, @@ -135,26 +135,26 @@ pure func dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_state_local, t Place, 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 Abs_Dataplane) 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) }{ dp.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), dp.dp3s_iospec_bio3s_xover_up2down_T(s, t, v)) } (v.isIO_Internal_val1 ==> + (dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==> + (dp.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), + dp.dp3s_iospec_bio3s_xover_up2down_T(s, t, v))))) } -pred CBio_IN_bio3s_xover_core(t Place, v IO_val) +pred (dp Abs_Dataplane) 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 +requires dp.CBio_IN_bio3s_xover_core(t, v) +pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_xover_core_T(s IO_dp3s_state_local, 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() && +pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { + return (dp.asid() in dp.core_as_set() && 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 @@ -162,9 +162,9 @@ pure func dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v I 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, @@ -178,102 +178,102 @@ pure func dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v I 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 Abs_Dataplane) 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) }{ dp.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), dp.dp3s_iospec_bio3s_xover_core_T(s, t, v)) } (v.isIO_Internal_val1 ==> + (dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) ==> + (dp.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), + dp.dp3s_iospec_bio3s_xover_core_T(s, t, v))))) } -pred CBio_IN_bio3s_exit(t Place, v IO_val) +pred (dp Abs_Dataplane) 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 +requires dp.CBio_IN_bio3s_exit(t, v) +pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_exit_T(s IO_dp3s_state_local, t Place, v IO_val) Place // This corresponds to the condition of the if statement in the io-spec case for exit ghost decreases -pure func dp3s_iospec_bio3s_exit_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { +pure func (dp Abs_Dataplane) 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 Abs_Dataplane) dp3s_iospec_bio3s_exit(s IO_dp3s_state_local, t Place) { + forall v IO_val :: { dp.dp3s_iospec_bio3s_exit_guard(s, t, v) }{ dp.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), dp.dp3s_iospec_bio3s_exit_T(s, t, v)) } (v.isIO_Internal_val2 ==> + (dp.dp3s_iospec_bio3s_exit_guard(s, t, v) ==> + (dp.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), + dp.dp3s_iospec_bio3s_exit_T(s, t, v))))) } -pred CBioIO_bio3s_send(t Place, v IO_val) +pred (dp Abs_Dataplane) 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 +requires dp.CBioIO_bio3s_send(t, v) +pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_send_T(s IO_dp3s_state_local, t Place, v IO_val) Place // This corresponds to the condition of the if statement in the io-spec case for send ghost decreases -pure func dp3s_iospec_bio3s_send_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { +pure func (dp Abs_Dataplane) 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)))) && +pred (dp Abs_Dataplane) dp3s_iospec_bio3s_send(s IO_dp3s_state_local, t Place) { + forall v IO_val :: { dp.dp3s_iospec_bio3s_send_guard(s, t, v) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(s, t, v)) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(s, t, v)) } (v.isIO_val_Pkt2 ==> + (dp.dp3s_iospec_bio3s_send_guard(s, t, v) ==> + dp.CBioIO_bio3s_send(t, v) && + dp.dp3s_iospec_ordered(s, dp.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))) + dp.CBioIO_bio3s_send(t, v) && + dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(s, t, v))) } -pred CBioIO_bio3s_recv(t Place) +pred (dp Abs_Dataplane) 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 +requires dp.CBioIO_bio3s_recv(t) +pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_recv_T(s IO_dp3s_state_local, 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 - -pred 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( +requires dp.CBioIO_bio3s_recv(t) +pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_recv_R(s IO_dp3s_state_local, t Place) IO_val + +pred (dp Abs_Dataplane) dp3s_iospec_bio3s_recv(s IO_dp3s_state_local, t Place) { + dp.CBioIO_bio3s_recv(t) && + (dp.dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Pkt2 ==> + dp.dp3s_iospec_ordered( + dp.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))) + dp.dp3s_iospec_bio3s_recv_R(s, t).IO_val_Pkt2_1, + dp.dp3s_iospec_bio3s_recv_R(s, t).IO_val_Pkt2_2), + dp.dp3s_iospec_bio3s_recv_T(s, t))) && + (dp.dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Unsupported ==> + dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_recv_T(s, t))) && + ((!dp.dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Pkt2 && !dp.dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Unsupported) ==> + dp.dp3s_iospec_ordered(dp.undefined(), dp.dp3s_iospec_bio3s_recv_T(s, t))) } -pred CBio_Skip(t Place) +pred (dp Abs_Dataplane) CBio_Skip(t Place) ghost -requires CBio_Skip(t) -pure func dp3s_iospec_skip_T(s IO_dp3s_state_local, t Place) Place +requires dp.CBio_Skip(t) +pure func (dp Abs_Dataplane) dp3s_iospec_skip_T(s IO_dp3s_state_local, 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 Abs_Dataplane) dp3s_iospec_skip(s IO_dp3s_state_local, t Place) { + dp.CBio_Skip(t) && dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_skip_T(s, t)) } -pred dp3s_iospec_stop(s IO_dp3s_state_local, t Place) { +pred (dp Abs_Dataplane) 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..fe74908b3 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -18,7 +18,7 @@ package io -import "github.com/scionproto/scion/pkg/slayers/path" +//import "github.com/scionproto/scion/pkg/slayers/path" // used everywhere where the Isabel spec has a type-parameter type TypeParameter = interface{} @@ -120,19 +120,19 @@ func (h IO_HF) Toab() IO_ahi { // 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) +// 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 { @@ -151,39 +151,39 @@ type IO_Link adt { ghost decreases -pure func rid_as(p IO_rid) IO_as +pure func (dp Abs_Dataplane) rid_as(p IO_rid) IO_as ghost decreases -pure func link_type(p1 IO_as, p2 IO_ifs) IO_Link +pure func (dp Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool type ext2_rec struct { op1 IO_as diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 16c78fc8e..04db9105d 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -23,52 +23,52 @@ 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 Abs_Dataplane) core_as_set() set[IO_as] //TODO: how ghost decreases -pure func hf_valid(p1 bool, p2 uint, p3 set[IO_msgterm], p4 IO_HF) bool +pure func (dp Abs_Dataplane) 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 Abs_Dataplane) upd_uinfo(p1 set[IO_msgterm], p2 IO_HF) set[IO_msgterm] ghost decreases -pure func rid() IO_rid +pure func (dp Abs_Dataplane) rid() IO_rid ghost decreases -pure func asid() IO_as { - return rid_as(rid()) +pure func (dp Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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), + ibuf: dp.insert(s.ibuf, i, pkt), obuf: s.obuf, } } 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 Abs_Dataplane) 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), + obuf: dp.insert(s.obuf, i, pkt), } } // helper func ghost decreases -pure func insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k option[IO_ifs], v IO_pkt3) dict[option[IO_ifs]](set[IO_pkt3]) { +pure func (dp Abs_Dataplane) insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k option[IO_ifs], v IO_pkt3) dict[option[IO_ifs]](set[IO_pkt3]) { return let newSet := (k in domain(buf)? (let pre := buf[k] in pre union set[IO_pkt3]{v}) : set[IO_pkt3]{v}) in buf[k = newSet] } @@ -76,21 +76,21 @@ 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 Abs_Dataplane) 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 Abs_Dataplane) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif option[IO_ifs]) bool { + return nextif == none[IO_ifs] ? newpkt == m : dp.dp3s_forward_ext(m, newpkt, get(nextif)) } ghost decreases -pure func dp3s_xover_common( +pure func (dp Abs_Dataplane) dp3s_xover_common( s IO_dp3s_state_local, m IO_pkt3, currseg IO_seg3, @@ -107,6 +107,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..f98949088 100644 --- a/verification/io/router_events.gobra +++ b/verification/io/router_events.gobra @@ -20,112 +20,112 @@ package io ghost decreases -pure func dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs) bool { +pure func (dp Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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) +// 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) -} +// 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 Abs_Dataplane) 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 +// 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..61d87e952 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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 Abs_Dataplane) 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..928af9bb4 100644 --- a/verification/io/xover.gobra +++ b/verification/io/xover.gobra @@ -38,7 +38,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 Abs_Dataplane) dp2_xover_common_guard(m IO_pkt2, currseg IO_seg2, nextseg IO_seg2, traversedseg IO_seg2, @@ -54,98 +54,99 @@ 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) + dp.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 (dp Abs_Dataplane) 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 dp.dp2_in_ext(s, asid, recvif, m) && +// dp.dp2_xover_common_guard(m, currseg, nextseg, traversedseg, newpkt, hf1, hf2, asid, recvif) && +// dp.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) +pure func (dp Abs_Dataplane) egif2_type(hf IO_HF, a IO_as, link IO_Link) bool { + return dp.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) +pure func (dp Abs_Dataplane) 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_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 Abs_Dataplane) 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{})) } -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) -} +// 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 && +// dp.xover_up2down2_link_type(asid, hf1, hf2) && +// dp.dp2_xover_common(s, m, currseg, nextseg, traversedseg, newpkt, hf1, hf2, asid, recvif, sprime) +// } 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 Abs_Dataplane) 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{})) } // 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 +// 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 From 7fec5312c7120c223ffee4c2203bdd5ca7289140 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 12 Oct 2023 12:19:09 +0200 Subject: [PATCH 02/12] renaming Abs_Dataplane to DataPlaneSpec --- verification/io/dataplane_abstract.gobra | 40 ++++++++++-------------- verification/io/other_defs.gobra | 18 +++++------ verification/io/router.gobra | 30 ++++++++++-------- verification/io/router_events.gobra | 14 ++++----- verification/io/segment-defs.gobra | 12 +++---- verification/io/xover.gobra | 12 +++---- 6 files changed, 61 insertions(+), 65 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index 8e6bf2bf2..69077721a 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -18,45 +18,37 @@ package io -type Abs_Dataplane adt { - Abs_Dataplane_ { +type DataPlaneSpec adt { + DataPlaneSpec_{ //external seq[IO_ifs] - linkTypes dict[IO_ifs]IO_Link - neighborIAs dict[IO_ifs]IO_as - internal IO_ifs //TODO: propably not needed, = 0 - localIA IO_as - running bool //TODO: needed? + linkTypes dict[IO_ifs]IO_Link + neighborIAs dict[IO_ifs]IO_as + internal IO_ifs //TODO: propably not needed, = 0 + localIA IO_as + topology TopologySpec } } -// ghost -// requires acc(dp, _) -// pure func (dp *Abs_Dataplane) (ifs IO_ifs) seq[IO_ifs] { -// return dp.external -// } +type TopologySpec adt { + TopologySpec_{ + core_as_set set[IO_as] + links dict[IO_as](dict[IO_ifs]IO_as) + } +} ghost -//requires acc(dp, _) requires ifs in domain(dp.linkTypes) -pure func (dp Abs_Dataplane) getLinkType(ifs IO_ifs) IO_Link { +pure func (dp DataPlaneSpec) getLinkType(ifs IO_ifs) IO_Link { return dp.linkTypes[ifs] } ghost -//requires acc(dp, _) requires ifs in domain(dp.neighborIAs) -pure func (dp Abs_Dataplane) getNeighborIA(ifs IO_ifs) IO_as { +pure func (dp DataPlaneSpec) getNeighborIA(ifs IO_ifs) IO_as { return dp.neighborIAs[ifs] } ghost -//requires acc(dp, _) -pure func (dp Abs_Dataplane) getLocalIA() IO_as { +pure func (dp DataPlaneSpec) getLocalIA() IO_as { return dp.localIA } - -ghost -//requires acc(dp, _) -pure func (dp Abs_Dataplane) isRunning() bool { - return dp.running -} \ No newline at end of file diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index fe74908b3..3dd36df7f 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -151,39 +151,39 @@ type IO_Link adt { ghost decreases -pure func (dp Abs_Dataplane) rid_as(p IO_rid) IO_as +pure func (dp DataPlaneSpec) rid_as(p IO_rid) IO_as ghost decreases -pure func (dp Abs_Dataplane) 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 (dp Abs_Dataplane) 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 (dp Abs_Dataplane) 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 (dp Abs_Dataplane) 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 (dp Abs_Dataplane) 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 (dp Abs_Dataplane) 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 (dp Abs_Dataplane) 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 (dp Abs_Dataplane) 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 diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 04db9105d..943fb4dba 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 (dp Abs_Dataplane) core_as_set() set[IO_as] //TODO: how +pure func (dp DataPlaneSpec) core_as_set() set[IO_as] //TODO: how ghost decreases -pure func (dp Abs_Dataplane) 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 (dp Abs_Dataplane) 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 (dp Abs_Dataplane) rid() IO_rid +pure func (dp DataPlaneSpec) rid() IO_rid ghost decreases -pure func (dp Abs_Dataplane) asid() IO_as { +pure func (dp DataPlaneSpec) asid() IO_as { return dp.rid_as(dp.rid()) } ghost decreases -pure func (dp Abs_Dataplane) 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 (dp Abs_Dataplane) 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: dp.insert(s.ibuf, i, pkt), obuf: s.obuf, @@ -58,7 +58,7 @@ pure func (dp Abs_Dataplane) dp3s_add_ibuf(s IO_dp3s_state_local, i option[IO_if ghost decreases -pure func (dp Abs_Dataplane) 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: dp.insert(s.obuf, i, pkt), @@ -68,7 +68,7 @@ pure func (dp Abs_Dataplane) dp3s_add_obuf(s IO_dp3s_state_local, i option[IO_if // helper func ghost decreases -pure func (dp Abs_Dataplane) insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k option[IO_ifs], v IO_pkt3) dict[option[IO_ifs]](set[IO_pkt3]) { +pure func (dp DataPlaneSpec) insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k option[IO_ifs], v IO_pkt3) dict[option[IO_ifs]](set[IO_pkt3]) { return let newSet := (k in domain(buf)? (let pre := buf[k] in pre union set[IO_pkt3]{v}) : set[IO_pkt3]{v}) in buf[k = newSet] } @@ -76,7 +76,7 @@ pure func (dp Abs_Dataplane) insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k op // TODO: try to remove the existencials here ghost decreases -pure func (dp Abs_Dataplane) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif IO_ifs) bool { +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)) } @@ -84,13 +84,17 @@ pure func (dp Abs_Dataplane) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif // TODO: should we change IO_ifs to being implemented as an option type? ghost decreases -pure func (dp Abs_Dataplane) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif option[IO_ifs]) bool { - return nextif == none[IO_ifs] ? newpkt == m : dp.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)) + } + //nextif == none[IO_ifs] ? newpkt == m : dp.dp3s_forward_ext(m, newpkt, get(nextif)) } ghost decreases -pure func (dp Abs_Dataplane) dp3s_xover_common( +pure func (dp DataPlaneSpec) dp3s_xover_common( s IO_dp3s_state_local, m IO_pkt3, currseg IO_seg3, diff --git a/verification/io/router_events.gobra b/verification/io/router_events.gobra index f98949088..0dd4244f2 100644 --- a/verification/io/router_events.gobra +++ b/verification/io/router_events.gobra @@ -20,7 +20,7 @@ package io ghost decreases -pure func (dp Abs_Dataplane) 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? (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{}) @@ -29,7 +29,7 @@ pure func (dp Abs_Dataplane) dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs) /* Abbreviations */ ghost decreases -pure func (dp Abs_Dataplane) valid_link_types2(hf1 IO_HF, a IO_as) bool { +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)) @@ -37,7 +37,7 @@ pure func (dp Abs_Dataplane) valid_link_types2(hf1 IO_HF, a IO_as) bool { ghost decreases -pure func (dp Abs_Dataplane) valid_link_types_in2(hf1 IO_HF, a IO_as) bool { +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)) @@ -46,21 +46,21 @@ pure func (dp Abs_Dataplane) valid_link_types_in2(hf1 IO_HF, a IO_as) bool { ghost decreases -pure func (dp Abs_Dataplane) dp2_check_interface(d bool, asid IO_as, hf1 IO_HF, recvif IO_ifs) bool { +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 (dp Abs_Dataplane) 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 (dp Abs_Dataplane) 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: @@ -100,7 +100,7 @@ pure func (dp Abs_Dataplane) dp2_forward_ext_guard(asid IO_as, m IO_pkt2, nextif // 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 (dp Abs_Dataplane) 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 && dp.dp2_check_interface(currseg.ConsDir, asid, hf1, recvif) && diff --git a/verification/io/segment-defs.gobra b/verification/io/segment-defs.gobra index 61d87e952..a89feca0a 100644 --- a/verification/io/segment-defs.gobra +++ b/verification/io/segment-defs.gobra @@ -23,7 +23,7 @@ package io ghost decreases -pure func (dp Abs_Dataplane) 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 (dp Abs_Dataplane) inc_seg2(currseg, traversedseg IO_seg2, hf1 IO_HF, ghost decreases -pure func (dp Abs_Dataplane) 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 (dp Abs_Dataplane) same_segment2(currseg, traversedseg IO_seg2) bool { ghost decreases -pure func (dp Abs_Dataplane) update_uinfo2(currseg, traversedseg IO_seg2, hf1 IO_HF) bool { +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 (dp Abs_Dataplane) 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 (dp Abs_Dataplane) update_uinfo(condition bool, currseg, traversedseg IO_seg2, hf1 IO_HF) bool { +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 (dp Abs_Dataplane) 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 928af9bb4..b9db8514f 100644 --- a/verification/io/xover.gobra +++ b/verification/io/xover.gobra @@ -38,7 +38,7 @@ package io // the new segment that we are xovering over to. ghost decreases -pure func (dp Abs_Dataplane) 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, @@ -68,7 +68,7 @@ pure func (dp Abs_Dataplane) dp2_xover_common_guard(m IO_pkt2, // // ghost // decreases -// pure func (dp Abs_Dataplane) dp2_xover_common( +// pure func (dp DataPlaneSpec) dp2_xover_common( // s IO_dp2_state, // m IO_pkt2, // currseg IO_seg2, @@ -87,19 +87,19 @@ pure func (dp Abs_Dataplane) dp2_xover_common_guard(m IO_pkt2, ghost decreases -pure func (dp Abs_Dataplane) egif2_type(hf IO_HF, a IO_as, link IO_Link) bool { +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 (dp Abs_Dataplane) inif2_type(hf IO_HF, a IO_as, link IO_Link) bool { +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 (dp Abs_Dataplane) xover_up2down2_link_type(asid IO_as, hf1 IO_HF, hf2 IO_HF) bool { +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{})) @@ -127,7 +127,7 @@ pure func (dp Abs_Dataplane) xover_up2down2_link_type(asid IO_as, hf1 IO_HF, hf2 ghost decreases -pure func (dp Abs_Dataplane) xover_core2_link_type(hf1 IO_HF, hf2 IO_HF, asid IO_as, d bool) 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{})) } From ac31b85c07e37b1a91f6acef56ac7ab154dfae9d Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 12 Oct 2023 12:23:40 +0200 Subject: [PATCH 03/12] removing local state from IO-spec next place functions --- verification/io/io-spec.gobra | 102 +++++++++++++++++----------------- 1 file changed, 51 insertions(+), 51 deletions(-) diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 41bf65012..47837a78c 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -19,7 +19,7 @@ package io // This is the main IO Specification. -pred (dp Abs_Dataplane) dp3s_iospec_ordered(s IO_dp3s_state_local, t Place) { +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) && @@ -32,24 +32,24 @@ pred (dp Abs_Dataplane) dp3s_iospec_ordered(s IO_dp3s_state_local, t Place) { type Place int -pred (dp Abs_Dataplane) token(t Place) +pred (dp DataPlaneSpec) token(t Place) ghost decreases -pure func (dp Abs_Dataplane) undefined() IO_dp3s_state_local +pure func (dp DataPlaneSpec) undefined() IO_dp3s_state_local -pred (dp Abs_Dataplane) CBio_IN_bio3s_enter(t Place, v IO_val) +pred (dp DataPlaneSpec) CBio_IN_bio3s_enter(t Place, v IO_val) ghost requires dp.CBio_IN_bio3s_enter(t, v) decreases -pure func (dp Abs_Dataplane) CBio_IN_bio3s_enter_T(s IO_dp3s_state_local, t Place, v IO_val) Place +pure func (dp DataPlaneSpec) CBio_IN_bio3s_enter_T(t Place, v IO_val) Place ghost requires len(currseg.Future) > 0 decreases -pure func (dp Abs_Dataplane) 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 ? dp.upd_uinfo(currseg.UInfo, currseg.Future[0]) : currseg.UInfo in @@ -66,7 +66,7 @@ pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_create_guard_traversedseg(currseg // This corresponds to the condition of the if statement in the io-spec case for enter ghost decreases -pure func (dp Abs_Dataplane) 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 && @@ -92,26 +92,26 @@ pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local v.IO_Internal_val1_4) } -pred (dp Abs_Dataplane) 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 :: { dp.dp3s_iospec_bio3s_enter_guard(s, t, v) } (v.isIO_Internal_val1 ==> (dp.dp3s_iospec_bio3s_enter_guard(s, t, v) ==> (dp.CBio_IN_bio3s_enter(t, v) && dp.dp3s_iospec_ordered( dp.dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), - dp.CBio_IN_bio3s_enter_T(s, t, v))))) + dp.CBio_IN_bio3s_enter_T(t, v))))) } -pred (dp Abs_Dataplane) CBio_IN_bio3s_xover_up2down(t Place, v IO_val) +pred (dp DataPlaneSpec) CBio_IN_bio3s_xover_up2down(t Place, v IO_val) ghost requires dp.CBio_IN_bio3s_xover_up2down(t, v) -pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_xover_up2down_T(s IO_dp3s_state_local, t Place, v IO_val) Place +pure func (dp DataPlaneSpec) 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 decreases -pure func (dp Abs_Dataplane) 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_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 @@ -135,25 +135,25 @@ pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta v.IO_Internal_val1_4,))) } -pred (dp Abs_Dataplane) 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) }{ dp.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), dp.dp3s_iospec_bio3s_xover_up2down_T(s, t, v)) } (v.isIO_Internal_val1 ==> +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) }{ dp.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), dp.dp3s_iospec_bio3s_xover_up2down_T(t, v)) } (v.isIO_Internal_val1 ==> (dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==> (dp.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), - dp.dp3s_iospec_bio3s_xover_up2down_T(s, t, v))))) + dp.dp3s_iospec_bio3s_xover_up2down_T(t, v))))) } -pred (dp Abs_Dataplane) CBio_IN_bio3s_xover_core(t Place, v IO_val) +pred (dp DataPlaneSpec) CBio_IN_bio3s_xover_core(t Place, v IO_val) ghost requires dp.CBio_IN_bio3s_xover_core(t, v) -pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_xover_core_T(s IO_dp3s_state_local, t Place, v IO_val) Place +pure func (dp DataPlaneSpec) 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 (dp Abs_Dataplane) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { +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_as_set() && let currseg := v.IO_Internal_val1_1.CurrSeg in (v.IO_Internal_val1_1.LeftSeg == none[IO_seg2] ? false : @@ -178,102 +178,102 @@ pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ v.IO_Internal_val1_4)))) } -pred (dp Abs_Dataplane) 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) }{ dp.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), dp.dp3s_iospec_bio3s_xover_core_T(s, t, v)) } (v.isIO_Internal_val1 ==> +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) }{ dp.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), dp.dp3s_iospec_bio3s_xover_core_T(t, v)) } (v.isIO_Internal_val1 ==> (dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) ==> (dp.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), - dp.dp3s_iospec_bio3s_xover_core_T(s, t, v))))) + dp.dp3s_iospec_bio3s_xover_core_T(t, v))))) } -pred (dp Abs_Dataplane) CBio_IN_bio3s_exit(t Place, v IO_val) +pred (dp DataPlaneSpec) CBio_IN_bio3s_exit(t Place, v IO_val) ghost requires dp.CBio_IN_bio3s_exit(t, v) -pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_exit_T(s IO_dp3s_state_local, t Place, v IO_val) Place +pure func (dp DataPlaneSpec) 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 decreases -pure func (dp Abs_Dataplane) 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)) && dp.dp3s_forward_ext(v.IO_Internal_val2_1, v.IO_Internal_val2_2, v.IO_Internal_val2_3) } -pred (dp Abs_Dataplane) dp3s_iospec_bio3s_exit(s IO_dp3s_state_local, t Place) { - forall v IO_val :: { dp.dp3s_iospec_bio3s_exit_guard(s, t, v) }{ dp.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), dp.dp3s_iospec_bio3s_exit_T(s, t, v)) } (v.isIO_Internal_val2 ==> +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) }{ dp.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), dp.dp3s_iospec_bio3s_exit_T(t, v)) } (v.isIO_Internal_val2 ==> (dp.dp3s_iospec_bio3s_exit_guard(s, t, v) ==> (dp.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), - dp.dp3s_iospec_bio3s_exit_T(s, t, v))))) + dp.dp3s_iospec_bio3s_exit_T(t, v))))) } -pred (dp Abs_Dataplane) CBioIO_bio3s_send(t Place, v IO_val) +pred (dp DataPlaneSpec) CBioIO_bio3s_send(t Place, v IO_val) ghost requires dp.CBioIO_bio3s_send(t, v) -pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_send_T(s IO_dp3s_state_local, t Place, v IO_val) Place +pure func (dp DataPlaneSpec) 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 decreases -pure func (dp Abs_Dataplane) 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 (dp Abs_Dataplane) dp3s_iospec_bio3s_send(s IO_dp3s_state_local, t Place) { - forall v IO_val :: { dp.dp3s_iospec_bio3s_send_guard(s, t, v) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(s, t, v)) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(s, t, v)) } (v.isIO_val_Pkt2 ==> +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) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v)) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v)) } (v.isIO_val_Pkt2 ==> (dp.dp3s_iospec_bio3s_send_guard(s, t, v) ==> dp.CBioIO_bio3s_send(t, v) && - dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(s, t, v)))) && + dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v)))) && (v.isIO_val_Unsupported ==> dp.CBioIO_bio3s_send(t, v) && - dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(s, t, v))) + dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v))) } -pred (dp Abs_Dataplane) CBioIO_bio3s_recv(t Place) +pred (dp DataPlaneSpec) CBioIO_bio3s_recv(t Place) ghost requires dp.CBioIO_bio3s_recv(t) -pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_recv_T(s IO_dp3s_state_local, t Place) Place +pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_recv_T(t Place) Place ghost requires dp.CBioIO_bio3s_recv(t) -pure func (dp Abs_Dataplane) dp3s_iospec_bio3s_recv_R(s IO_dp3s_state_local, t Place) IO_val +pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_recv_R(t Place) IO_val -pred (dp Abs_Dataplane) 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) { dp.CBioIO_bio3s_recv(t) && - (dp.dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Pkt2 ==> + (dp.dp3s_iospec_bio3s_recv_R(t).isIO_val_Pkt2 ==> dp.dp3s_iospec_ordered( dp.dp3s_add_ibuf( s, - dp.dp3s_iospec_bio3s_recv_R(s, t).IO_val_Pkt2_1, - dp.dp3s_iospec_bio3s_recv_R(s, t).IO_val_Pkt2_2), - dp.dp3s_iospec_bio3s_recv_T(s, t))) && - (dp.dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Unsupported ==> - dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_recv_T(s, t))) && - ((!dp.dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Pkt2 && !dp.dp3s_iospec_bio3s_recv_R(s, t).isIO_val_Unsupported) ==> - dp.dp3s_iospec_ordered(dp.undefined(), dp.dp3s_iospec_bio3s_recv_T(s, t))) + dp.dp3s_iospec_bio3s_recv_R(t).IO_val_Pkt2_1, + dp.dp3s_iospec_bio3s_recv_R(t).IO_val_Pkt2_2), + dp.dp3s_iospec_bio3s_recv_T(t))) && + (dp.dp3s_iospec_bio3s_recv_R(t).isIO_val_Unsupported ==> + dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_recv_T(t))) && + ((!dp.dp3s_iospec_bio3s_recv_R(t).isIO_val_Pkt2 && !dp.dp3s_iospec_bio3s_recv_R(t).isIO_val_Unsupported) ==> + dp.dp3s_iospec_ordered(dp.undefined(), dp.dp3s_iospec_bio3s_recv_T(t))) } -pred (dp Abs_Dataplane) CBio_Skip(t Place) +pred (dp DataPlaneSpec) CBio_Skip(t Place) ghost requires dp.CBio_Skip(t) -pure func (dp Abs_Dataplane) dp3s_iospec_skip_T(s IO_dp3s_state_local, t Place) Place +pure func (dp DataPlaneSpec) dp3s_iospec_skip_T(t Place) Place -pred (dp Abs_Dataplane) dp3s_iospec_skip(s IO_dp3s_state_local, t Place) { - dp.CBio_Skip(t) && dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_skip_T(s, t)) +pred (dp DataPlaneSpec) dp3s_iospec_skip(s IO_dp3s_state_local, t Place) { + dp.CBio_Skip(t) && dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_skip_T(t)) } -pred (dp Abs_Dataplane) dp3s_iospec_stop(s IO_dp3s_state_local, t Place) { +pred (dp DataPlaneSpec) dp3s_iospec_stop(s IO_dp3s_state_local, t Place) { true } From 03ec019c9194f432e36208f9c4d27d6c6559e96d Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 12 Oct 2023 13:30:48 +0200 Subject: [PATCH 04/12] rewriting IO-spec with match clause --- verification/io/io-spec.gobra | 152 ++++++++++++++++++++-------------- 1 file changed, 91 insertions(+), 61 deletions(-) diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 47837a78c..4ec7edced 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -63,6 +63,23 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg(currseg History: currseg.History} } +ghost +requires len(currseg.Future) > 0 +decreases +pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg IO_seg3) IO_seg3 { + return let uinfo := !currseg.ConsDir ? + dp.upd_uinfo(currseg.UInfo, currseg.Future[0]) : + currseg.UInfo in + IO_seg3_ { + AInfo: currseg.AInfo, + UInfo: uinfo, + ConsDir: currseg.ConsDir, + Peer: currseg.Peer, + Past: seq[IO_HF]{currseg.Future[0]} ++ currseg.Past, + Future: currseg.Future[1:], + History: seq[IO_ahi]{currseg.Future[0].Toab()} ++ currseg.History} +} + // This corresponds to the condition of the if statement in the io-spec case for enter ghost decreases @@ -94,12 +111,15 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local 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 :: { dp.dp3s_iospec_bio3s_enter_guard(s, t, v) } (v.isIO_Internal_val1 ==> - (dp.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) ==> (dp.CBio_IN_bio3s_enter(t, v) && dp.dp3s_iospec_ordered( - dp.dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), - dp.CBio_IN_bio3s_enter_T(t, v))))) + dp.dp3s_add_obuf(s, nextif, newpkt), + dp.CBio_IN_bio3s_enter_T(t, v)))) + default : true + }) } pred (dp DataPlaneSpec) CBio_IN_bio3s_xover_up2down(t Place, v IO_val) @@ -112,36 +132,41 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_T(t Place, v IO_val ghost decreases 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 - 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 := 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,))) + 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_inc(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 (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) }{ dp.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), dp.dp3s_iospec_bio3s_xover_up2down_T(t, v)) } (v.isIO_Internal_val1 ==> - (dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==> + forall v IO_val :: { dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) }{ dp.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), dp.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) ==> (dp.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), - dp.dp3s_iospec_bio3s_xover_up2down_T(t, v))))) + dp.dp3s_add_obuf(s, nextif, newpkt), + dp.dp3s_iospec_bio3s_xover_up2down_T(t, v)))) + default : true + }) } pred (dp DataPlaneSpec) CBio_IN_bio3s_xover_core(t Place, v IO_val) @@ -156,13 +181,14 @@ 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_as_set() && 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 := dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in + let traversedseg := dp.dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) in (dp.xover_core2_link_type(hf1, hf2, dp.asid(), currseg.ConsDir) && dp.dp3s_xover_common( s, @@ -175,16 +201,20 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ hf2, v.IO_Internal_val1_2, v.IO_Internal_val1_3, - v.IO_Internal_val1_4)))) + v.IO_Internal_val1_4)) + }) } 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) }{ dp.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), dp.dp3s_iospec_bio3s_xover_core_T(t, v)) } (v.isIO_Internal_val1 ==> - (dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) ==> + forall v IO_val :: { dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) }{ dp.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), dp.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) ==> (dp.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), - dp.dp3s_iospec_bio3s_xover_core_T(t, v))))) + dp.dp3s_add_obuf(s, nextif, newpkt), + dp.dp3s_iospec_bio3s_xover_core_T(t, v)))) + default : true + }) } @@ -204,12 +234,15 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_exit_guard(s IO_dp3s_state_local, } 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) }{ dp.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), dp.dp3s_iospec_bio3s_exit_T(t, v)) } (v.isIO_Internal_val2 ==> - (dp.dp3s_iospec_bio3s_exit_guard(s, t, v) ==> - (dp.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), - dp.dp3s_iospec_bio3s_exit_T(t, v))))) + forall v IO_val :: { dp.dp3s_iospec_bio3s_exit_guard(s, t, v) }{ dp.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), dp.dp3s_iospec_bio3s_exit_T(t, v)) } ( + match v { + case IO_Internal_val2{_, ?newpkt, ?nextif} : (dp.dp3s_iospec_bio3s_exit_guard(s, t, v) ==> + (dp.CBio_IN_bio3s_exit(t, v) && + dp.dp3s_iospec_ordered( + dp.dp3s_add_obuf(s, some(nextif), newpkt), + dp.dp3s_iospec_bio3s_exit_T(t, v)))) + default : true + }) } @@ -229,13 +262,15 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_send_guard(s IO_dp3s_state_local, // TODO: annotate WriteBatch, skipped for now 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) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v)) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v)) } (v.isIO_val_Pkt2 ==> - (dp.dp3s_iospec_bio3s_send_guard(s, t, v) ==> - dp.CBioIO_bio3s_send(t, v) && - dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v)))) && - (v.isIO_val_Unsupported ==> - dp.CBioIO_bio3s_send(t, v) && - dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v))) + forall v IO_val :: { dp.dp3s_iospec_bio3s_send_guard(s, t, v) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v)) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v)) } ( + match v { + case IO_val_Pkt2{_, _} : (dp.dp3s_iospec_bio3s_send_guard(s, t, v) ==> + dp.CBioIO_bio3s_send(t, v) && + dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v))) + case IO_val_Unsupported{_, _} : (dp.CBioIO_bio3s_send(t, v) && + dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v))) + default : true + }) } pred (dp DataPlaneSpec) CBioIO_bio3s_recv(t Place) @@ -250,17 +285,12 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_recv_R(t Place) IO_val pred (dp DataPlaneSpec) dp3s_iospec_bio3s_recv(s IO_dp3s_state_local, t Place) { dp.CBioIO_bio3s_recv(t) && - (dp.dp3s_iospec_bio3s_recv_R(t).isIO_val_Pkt2 ==> - dp.dp3s_iospec_ordered( - dp.dp3s_add_ibuf( - s, - dp.dp3s_iospec_bio3s_recv_R(t).IO_val_Pkt2_1, - dp.dp3s_iospec_bio3s_recv_R(t).IO_val_Pkt2_2), - dp.dp3s_iospec_bio3s_recv_T(t))) && - (dp.dp3s_iospec_bio3s_recv_R(t).isIO_val_Unsupported ==> - dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_recv_T(t))) && - ((!dp.dp3s_iospec_bio3s_recv_R(t).isIO_val_Pkt2 && !dp.dp3s_iospec_bio3s_recv_R(t).isIO_val_Unsupported) ==> - dp.dp3s_iospec_ordered(dp.undefined(), dp.dp3s_iospec_bio3s_recv_T(t))) + (match dp.dp3s_iospec_bio3s_recv_R(t) { + case IO_val_Pkt2{?recvif, ?pkt} : dp.dp3s_iospec_ordered( + dp.dp3s_add_ibuf(s, recvif, pkt), dp.dp3s_iospec_bio3s_recv_T(t)) + case IO_val_Unsupported{_, _} : dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_recv_T(t)) + default : dp.dp3s_iospec_ordered(dp.undefined(), dp.dp3s_iospec_bio3s_recv_T(t)) + }) } pred (dp DataPlaneSpec) CBio_Skip(t Place) From 491e444b42b5408cdf06d0067beb69f3f9488345 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 12 Oct 2023 13:35:59 +0200 Subject: [PATCH 05/12] comment out unnecessary functions --- verification/io/other_defs.gobra | 18 +++++++++--------- verification/io/router.gobra | 7 +++---- 2 files changed, 12 insertions(+), 13 deletions(-) diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index 3dd36df7f..93cd6e31f 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -201,17 +201,17 @@ 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_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_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 +// 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 diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 943fb4dba..8995bc745 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -51,7 +51,7 @@ ghost decreases 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: dp.insert(s.ibuf, i, pkt), + ibuf: insert(s.ibuf, i, pkt), obuf: s.obuf, } } @@ -61,14 +61,14 @@ decreases 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: dp.insert(s.obuf, i, pkt), + obuf: insert(s.obuf, i, pkt), } } // helper func ghost decreases -pure func (dp DataPlaneSpec) insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k option[IO_ifs], v IO_pkt3) dict[option[IO_ifs]](set[IO_pkt3]) { +pure func insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k option[IO_ifs], v IO_pkt3) dict[option[IO_ifs]](set[IO_pkt3]) { return let newSet := (k in domain(buf)? (let pre := buf[k] in pre union set[IO_pkt3]{v}) : set[IO_pkt3]{v}) in buf[k = newSet] } @@ -89,7 +89,6 @@ pure func (dp DataPlaneSpec) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif opti case none[IO_ifs] : newpkt == m default : dp.dp3s_forward_ext(m, newpkt, get(nextif)) } - //nextif == none[IO_ifs] ? newpkt == m : dp.dp3s_forward_ext(m, newpkt, get(nextif)) } ghost From 61da1e0afea7c830fc57f124fc410fce25ed20e9 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Mon, 16 Oct 2023 20:34:23 +0200 Subject: [PATCH 06/12] cosmetic changes --- verification/io/dataplane_abstract.gobra | 10 +- verification/io/io-spec.gobra | 208 +++++++++++------------ verification/io/other_defs.gobra | 34 +--- verification/io/router.gobra | 6 +- verification/io/router_events.gobra | 39 ----- verification/io/xover.gobra | 63 +------ 6 files changed, 109 insertions(+), 251 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index 69077721a..6c894bdbb 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -14,16 +14,12 @@ // +gobra - package io - type DataPlaneSpec adt { DataPlaneSpec_{ - //external seq[IO_ifs] linkTypes dict[IO_ifs]IO_Link neighborIAs dict[IO_ifs]IO_as - internal IO_ifs //TODO: propably not needed, = 0 localIA IO_as topology TopologySpec } @@ -38,17 +34,17 @@ type TopologySpec adt { ghost requires ifs in domain(dp.linkTypes) -pure func (dp DataPlaneSpec) getLinkType(ifs IO_ifs) IO_Link { +pure func (dp DataPlaneSpec) GetLinkType(ifs IO_ifs) IO_Link { return dp.linkTypes[ifs] } ghost requires ifs in domain(dp.neighborIAs) -pure func (dp DataPlaneSpec) getNeighborIA(ifs IO_ifs) IO_as { +pure func (dp DataPlaneSpec) GetNeighborIA(ifs IO_ifs) IO_as { return dp.neighborIAs[ifs] } ghost -pure func (dp DataPlaneSpec) getLocalIA() IO_as { +pure func (dp DataPlaneSpec) GetLocalIA() IO_as { return dp.localIA } diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 4ec7edced..8e8b6dd68 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -32,41 +32,24 @@ pred (dp DataPlaneSpec) dp3s_iospec_ordered(s IO_dp3s_state_local, t Place) { type Place int -pred (dp DataPlaneSpec) token(t Place) +pred token(t Place) ghost decreases -pure func (dp DataPlaneSpec) undefined() IO_dp3s_state_local +pure func undefined() IO_dp3s_state_local -pred (dp DataPlaneSpec) CBio_IN_bio3s_enter(t Place, v IO_val) +pred CBio_IN_bio3s_enter(t Place, v IO_val) ghost -requires dp.CBio_IN_bio3s_enter(t, v) +requires CBio_IN_bio3s_enter(t, v) decreases -pure func (dp DataPlaneSpec) CBio_IN_bio3s_enter_T(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 (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg(currseg IO_seg3) IO_seg3 { - return let uinfo := !currseg.ConsDir ? - dp.upd_uinfo(currseg.UInfo, currseg.Future[0]) : - currseg.UInfo in - IO_seg3_ { - AInfo: currseg.AInfo, - UInfo: uinfo, - ConsDir: currseg.ConsDir, - Peer: currseg.Peer, - Past: currseg.Past, - Future: currseg.Future, - History: currseg.History} -} - -ghost -requires len(currseg.Future) > 0 -decreases -pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg IO_seg3) IO_seg3 { return let uinfo := !currseg.ConsDir ? dp.upd_uinfo(currseg.UInfo, currseg.Future[0]) : currseg.UInfo in @@ -75,9 +58,9 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg_inc(cur UInfo: uinfo, ConsDir: currseg.ConsDir, Peer: currseg.Peer, - Past: seq[IO_HF]{currseg.Future[0]} ++ currseg.Past, - Future: currseg.Future[1:], - History: seq[IO_ahi]{currseg.Future[0].Toab()} ++ currseg.History} + Past: currseg.Past, + Future: currseg.Future, + History: currseg.History} } // This corresponds to the condition of the if statement in the io-spec case for enter @@ -113,67 +96,70 @@ 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 :: { 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) ==> - (dp.CBio_IN_bio3s_enter(t, v) && + case IO_Internal_val1{_, _, ?newpkt, ?nextif}: + (dp.dp3s_iospec_bio3s_enter_guard(s, t, v) ==> + (CBio_IN_bio3s_enter(t, v) && dp.dp3s_iospec_ordered( dp.dp3s_add_obuf(s, nextif, newpkt), - dp.CBio_IN_bio3s_enter_T(t, v)))) - default : true + CBio_IN_bio3s_enter_T(t, v)))) + default: true }) } -pred (dp DataPlaneSpec) CBio_IN_bio3s_xover_up2down(t Place, v IO_val) +pred CBio_IN_bio3s_xover_up2down(t Place, v IO_val) ghost -requires dp.CBio_IN_bio3s_xover_up2down(t, v) -pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_T(t Place, v IO_val) Place +requires CBio_IN_bio3s_xover_up2down(t, v) +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 decreases 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_inc(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,))) - } + 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 (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) }{ dp.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), dp.dp3s_iospec_bio3s_xover_up2down_T(t, v)) } ( + 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) ==> - (dp.CBio_IN_bio3s_xover_up2down(t, v) && - dp.dp3s_iospec_ordered( - dp.dp3s_add_obuf(s, nextif, newpkt), - dp.dp3s_iospec_bio3s_xover_up2down_T(t, v)))) - default : true + 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 (dp DataPlaneSpec) CBio_IN_bio3s_xover_core(t Place, v IO_val) +pred CBio_IN_bio3s_xover_core(t Place, v IO_val) ghost -requires dp.CBio_IN_bio3s_xover_core(t, v) -pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_T(t Place, v IO_val) Place +requires CBio_IN_bio3s_xover_core(t, v) +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 @@ -182,13 +168,14 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ return (dp.asid() in dp.core_as_set() && 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 + 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 := dp.dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) in + 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, @@ -206,23 +193,23 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ } 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) }{ dp.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), dp.dp3s_iospec_bio3s_xover_core_T(t, v)) } ( + 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) ==> - (dp.CBio_IN_bio3s_xover_core(t, v) && - dp.dp3s_iospec_ordered( - dp.dp3s_add_obuf(s, nextif, newpkt), - dp.dp3s_iospec_bio3s_xover_core_T(t, v)))) - default : true + 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 }) } -pred (dp DataPlaneSpec) CBio_IN_bio3s_exit(t Place, v IO_val) +pred CBio_IN_bio3s_exit(t Place, v IO_val) ghost -requires dp.CBio_IN_bio3s_exit(t, v) -pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_exit_T(t Place, v IO_val) Place +requires CBio_IN_bio3s_exit(t, v) +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 @@ -234,23 +221,24 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_exit_guard(s IO_dp3s_state_local, } 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) }{ dp.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), dp.dp3s_iospec_bio3s_exit_T(t, v)) } ( + 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) ==> - (dp.CBio_IN_bio3s_exit(t, 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), - dp.dp3s_iospec_bio3s_exit_T(t, v)))) - default : true + dp3s_iospec_bio3s_exit_T(t, v)))) + default: true }) } -pred (dp DataPlaneSpec) CBioIO_bio3s_send(t Place, v IO_val) +pred CBioIO_bio3s_send(t Place, v IO_val) ghost -requires dp.CBioIO_bio3s_send(t, v) -pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_send_T(t Place, v IO_val) Place +requires CBioIO_bio3s_send(t, v) +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 @@ -262,48 +250,52 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_send_guard(s IO_dp3s_state_local, // TODO: annotate WriteBatch, skipped for now 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) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v)) }{ dp.CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v)) } ( + 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) ==> - dp.CBioIO_bio3s_send(t, v) && - dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v))) - case IO_val_Unsupported{_, _} : (dp.CBioIO_bio3s_send(t, v) && - dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_send_T(t, v))) - default : true + 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 (dp DataPlaneSpec) CBioIO_bio3s_recv(t Place) +pred CBioIO_bio3s_recv(t Place) ghost -requires dp.CBioIO_bio3s_recv(t) -pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_recv_T(t Place) Place +requires CBioIO_bio3s_recv(t) +pure func dp3s_iospec_bio3s_recv_T(t Place) Place ghost -requires dp.CBioIO_bio3s_recv(t) -pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_recv_R(t Place) IO_val +requires CBioIO_bio3s_recv(t) +pure func dp3s_iospec_bio3s_recv_R(t Place) IO_val pred (dp DataPlaneSpec) dp3s_iospec_bio3s_recv(s IO_dp3s_state_local, t Place) { - dp.CBioIO_bio3s_recv(t) && - (match dp.dp3s_iospec_bio3s_recv_R(t) { - case IO_val_Pkt2{?recvif, ?pkt} : dp.dp3s_iospec_ordered( - dp.dp3s_add_ibuf(s, recvif, pkt), dp.dp3s_iospec_bio3s_recv_T(t)) - case IO_val_Unsupported{_, _} : dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_bio3s_recv_T(t)) - default : dp.dp3s_iospec_ordered(dp.undefined(), dp.dp3s_iospec_bio3s_recv_T(t)) + CBioIO_bio3s_recv(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 (dp DataPlaneSpec) CBio_Skip(t Place) +pred CBio_Skip(t Place) ghost -requires dp.CBio_Skip(t) -pure func (dp DataPlaneSpec) dp3s_iospec_skip_T(t Place) Place +requires CBio_Skip(t) +pure func dp3s_iospec_skip_T(t Place) Place pred (dp DataPlaneSpec) dp3s_iospec_skip(s IO_dp3s_state_local, t Place) { - dp.CBio_Skip(t) && dp.dp3s_iospec_ordered(s, dp.dp3s_iospec_skip_T(t)) + CBio_Skip(t) && dp.dp3s_iospec_ordered(s, dp3s_iospec_skip_T(t)) } 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 93cd6e31f..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{} @@ -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 8995bc745..f8a463a16 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -86,8 +86,10 @@ ghost decreases 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)) + case none[IO_ifs]: + newpkt == m + default: + dp.dp3s_forward_ext(m, newpkt, get(nextif)) } } diff --git a/verification/io/router_events.gobra b/verification/io/router_events.gobra index 0dd4244f2..ea64ce2b7 100644 --- a/verification/io/router_events.gobra +++ b/verification/io/router_events.gobra @@ -77,26 +77,6 @@ pure func (dp DataPlaneSpec) dp2_forward_ext_guard(asid IO_as, m IO_pkt2, nextif 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 @@ -110,22 +90,3 @@ pure func (dp DataPlaneSpec) dp2_enter_guard(m IO_pkt2, currseg IO_seg2, travers 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/xover.gobra b/verification/io/xover.gobra index b9db8514f..bf64ef4ca 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, @@ -65,26 +63,6 @@ pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2, dp.same_other2(currseg, traversedseg) } -// -// ghost -// decreases -// pure func (dp DataPlaneSpec) 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 dp.dp2_in_ext(s, asid, recvif, m) && -// dp.dp2_xover_common_guard(m, currseg, nextseg, traversedseg, newpkt, hf1, hf2, asid, recvif) && -// dp.dp2_forward(s, sprime, asid, newpkt) -// } - ghost decreases pure func (dp DataPlaneSpec) egif2_type(hf IO_HF, a IO_as, link IO_Link) bool { @@ -105,48 +83,9 @@ pure func (dp DataPlaneSpec) xover_up2down2_link_type(asid IO_as, hf1 IO_HF, hf2 (dp.egif2_type(hf1, asid, IO_PeerOrCore{}) && dp.egif2_type(hf2, asid, IO_ProvCust{})) } -// 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 && -// dp.xover_up2down2_link_type(asid, hf1, hf2) && -// dp.dp2_xover_common(s, m, currseg, nextseg, traversedseg, newpkt, hf1, hf2, asid, recvif, sprime) -// } - ghost decreases 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{})) -} - -// 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 +} \ No newline at end of file From 4ff2211448b38e327738ad884f6b242f026e3d47 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Tue, 17 Oct 2023 12:15:35 +0200 Subject: [PATCH 07/12] documentation for DataPlaneSpec and Valid function --- verification/io/dataplane_abstract.gobra | 33 +++++++++++++++++++++--- 1 file changed, 30 insertions(+), 3 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index 6c894bdbb..8bb797296 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -19,20 +19,39 @@ package io type DataPlaneSpec adt { DataPlaneSpec_{ linkTypes dict[IO_ifs]IO_Link - neighborIAs dict[IO_ifs]IO_as - localIA IO_as + neighborIAs dict[IO_ifs]IO_as + localIA IO_as topology TopologySpec } } +//TopologySpec provides information about the entire network topology because +//the dataplane lacks information needed for the IO-specification. +//core_as_set: set of ASIDs, which are core ASes in the network. +//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_{ - core_as_set set[IO_as] + core_as_set set[IO_as] links dict[IO_as](dict[IO_ifs]IO_as) } } +//A DataPlaneSpec is valid if and only if the domain of linkTypes and neighborIAs +//are equal, i.e., evey link connects to an AS. The entries of neigborIAs and links[localIA] +//are equal, i.e, all local neighbors are part of the network topology. Every core AS +//and localIA must be in the domain of links. 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.core_as_set} core in dp.topology.core_as_set ==> 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] @@ -40,11 +59,19 @@ pure func (dp DataPlaneSpec) GetLinkType(ifs IO_ifs) IO_Link { 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) GetCore_as_set() set[IO_as] { + return dp.topology.core_as_set +} From 4c327d6dd0170c20938e5e38bd050633e5d0f224 Mon Sep 17 00:00:00 2001 From: Markus Limbeck <92801626+mlimbeck@users.noreply.github.com> Date: Wed, 18 Oct 2023 12:27:27 +0200 Subject: [PATCH 08/12] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- verification/io/dataplane_abstract.gobra | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index 8bb797296..405bcf465 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -25,9 +25,8 @@ type DataPlaneSpec adt { } } -//TopologySpec provides information about the entire network topology because -//the dataplane lacks information needed for the IO-specification. -//core_as_set: set of ASIDs, which are core ASes in the network. +// 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 { From 5728d2bb187a15a71791d949850abe2ac2d9959a Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 18 Oct 2023 12:45:11 +0200 Subject: [PATCH 09/12] cosmetic changes --- verification/io/dataplane_abstract.gobra | 14 +++++--------- verification/io/io-spec.gobra | 5 +++-- verification/io/router.gobra | 2 +- verification/io/xover.gobra | 4 ++-- 4 files changed, 11 insertions(+), 14 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index 405bcf465..26e3d6a81 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -26,27 +26,23 @@ type DataPlaneSpec adt { } // TopologySpec provides information about the entire network topology. -// CoreAS: IDs of the core Autonomous Systems +// 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_{ - core_as_set set[IO_as] + coreAS set[IO_as] links dict[IO_as](dict[IO_ifs]IO_as) } } -//A DataPlaneSpec is valid if and only if the domain of linkTypes and neighborIAs -//are equal, i.e., evey link connects to an AS. The entries of neigborIAs and links[localIA] -//are equal, i.e, all local neighbors are part of the network topology. Every core AS -//and localIA must be in the domain of links. 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.core_as_set} core in dp.topology.core_as_set ==> core in domain(dp.topology.links)) + (forall core IO_as :: {core in dp.topology.coreAS} core in dp.topology.coreAS ==> core in domain(dp.topology.links)) } ghost @@ -71,6 +67,6 @@ pure func (dp DataPlaneSpec) GetLocalIA() IO_as { ghost decreases -pure func (dp DataPlaneSpec) GetCore_as_set() set[IO_as] { - return dp.topology.core_as_set +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 8e8b6dd68..4a512ed11 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -165,7 +165,7 @@ pure func dp3s_iospec_bio3s_xover_core_T(t Place, v IO_val) Place ghost 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_as_set() && + 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]: false @@ -195,7 +195,8 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ 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) ==> + 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), diff --git a/verification/io/router.gobra b/verification/io/router.gobra index f8a463a16..3370e716a 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -23,7 +23,7 @@ package io // This function corresponds to function 'core' in the IO spec ghost decreases -pure func (dp DataPlaneSpec) core_as_set() set[IO_as] //TODO: how +pure func (dp DataPlaneSpec) core() set[IO_as] ghost decreases diff --git a/verification/io/xover.gobra b/verification/io/xover.gobra index bf64ef4ca..82a95c0ee 100644 --- a/verification/io/xover.gobra +++ b/verification/io/xover.gobra @@ -79,8 +79,8 @@ ghost decreases 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{})) + (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{})) } ghost From 0116bce005f0b72a86ca823a9234118a9a6fb504 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 18 Oct 2023 12:48:41 +0200 Subject: [PATCH 10/12] fix comment --- verification/io/dataplane_abstract.gobra | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index 26e3d6a81..f6fda5352 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -27,7 +27,7 @@ type DataPlaneSpec adt { // 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: 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_{ From b9f8ba424c469eac786a8e0d4a91d9d86b5c0bad Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 18 Oct 2023 14:30:00 +0200 Subject: [PATCH 11/12] cosmetic changes --- verification/io/io-spec.gobra | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 4a512ed11..5e7ea0d16 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -118,7 +118,8 @@ decreases 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 + case none[IO_seg2]: + false default: let nextseg := get(v.IO_Internal_val1_1.LeftSeg) in (nextseg.ConsDir && @@ -151,7 +152,8 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down(s IO_dp3s_state_local, t dp.dp3s_iospec_ordered( dp.dp3s_add_obuf(s, nextif, newpkt), dp3s_iospec_bio3s_xover_up2down_T(t, v)))) - default: true + default: + true }) } @@ -168,7 +170,8 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ 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]: false + case none[IO_seg2]: + false default: let nextseg := get(v.IO_Internal_val1_1.LeftSeg) in currseg.ConsDir == nextseg.ConsDir && @@ -201,7 +204,8 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core(s IO_dp3s_state_local, t Pl dp.dp3s_iospec_ordered( dp.dp3s_add_obuf(s, nextif, newpkt), dp3s_iospec_bio3s_xover_core_T(t, v)))) - default: true + default: + true }) } @@ -230,7 +234,8 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_exit(s IO_dp3s_state_local, t Place) { dp.dp3s_iospec_ordered( dp.dp3s_add_obuf(s, some(nextif), newpkt), dp3s_iospec_bio3s_exit_T(t, v)))) - default: true + default: + true }) } @@ -260,7 +265,8 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_send(s IO_dp3s_state_local, t Place) { case IO_val_Unsupported{_, _}: (CBioIO_bio3s_send(t, v) && dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(t, v))) - default: true + default: + true }) } From 8586dc8377a69dd958f663d21375dfcfa3b4f8e9 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 18 Oct 2023 15:45:37 +0200 Subject: [PATCH 12/12] guards require correct type --- verification/io/io-spec.gobra | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 5e7ea0d16..652c59a1c 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -65,6 +65,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg(currseg // 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 (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) ==> @@ -114,6 +115,7 @@ 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 (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 @@ -166,6 +168,7 @@ 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 +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 @@ -218,6 +221,7 @@ 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 (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) ==> @@ -248,6 +252,7 @@ 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 (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) ==>