From 6ae29eb91e8209550c0dfa6f0e680d4e75bc039d Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 11 Oct 2023 15:12:44 +0200 Subject: [PATCH 01/18] 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/18] 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/18] 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/18] 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/18] 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 ed9ade0744f342087162359f20984729832a68c7 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 12 Oct 2023 23:20:52 +0200 Subject: [PATCH 06/18] providing bodies to abstract functions in IO-spec --- verification/io/dataplane_abstract.gobra | 3 + verification/io/io-spec.gobra | 10 ++- verification/io/other_defs.gobra | 59 +++++++++++----- verification/io/router.gobra | 87 +++++++++++++++++++++--- 4 files changed, 132 insertions(+), 27 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index 69077721a..98186521b 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -38,17 +38,20 @@ type TopologySpec adt { ghost requires ifs in domain(dp.linkTypes) +decreases pure func (dp DataPlaneSpec) getLinkType(ifs IO_ifs) IO_Link { return dp.linkTypes[ifs] } ghost requires ifs in domain(dp.neighborIAs) +decreases pure func (dp DataPlaneSpec) getNeighborIA(ifs IO_ifs) IO_as { return dp.neighborIAs[ifs] } ghost +decreases pure func (dp DataPlaneSpec) getLocalIA() IO_as { return dp.localIA } diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 4ec7edced..0387d65b4 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -87,9 +87,13 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local 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 && + len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let currseg := v.IO_Internal_val1_1.CurrSeg in let hf1, fut := currseg.Future[0], currseg.Future[1:] in - let traversedseg := dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in + let traversedseg := match v.IO_Internal_val1_4{ + case none[IO_ifs] : dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) + default : dp.dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) + } in dp.dp2_enter_guard( v.IO_Internal_val1_1, currseg, @@ -139,6 +143,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta (nextseg.ConsDir && len(nextseg.Future) > 0 && len(currseg.Future) > 0 && + len(v.IO_Internal_val1_3.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) && @@ -187,6 +192,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ currseg.ConsDir == nextseg.ConsDir && len(nextseg.Future) > 0 && len(currseg.Future) > 0 && + len(v.IO_Internal_val1_3.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_core2_link_type(hf1, hf2, dp.asid(), currseg.ConsDir) && @@ -230,6 +236,8 @@ 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) ==> (let ibuf_set := s.ibuf[none[IO_ifs]] in (v.IO_Internal_val2_1 in ibuf_set)) && + len(v.IO_Internal_val2_1.CurrSeg.Future) > 0 && + len(v.IO_Internal_val2_2.CurrSeg.Future) > 0 && dp.dp3s_forward_ext(v.IO_Internal_val2_1, v.IO_Internal_val2_2, v.IO_Internal_val2_3) } diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index 93cd6e31f..f0349ff20 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -37,7 +37,7 @@ type IO_ifs uint16 type IO_as uint // router ids -type IO_rid uint +//type IO_rid uint // msgTerms consist of terms from our term algebra. type IO_msgterm adt { @@ -48,7 +48,7 @@ type IO_msgterm adt { } MsgTerm_Num { - MsgTerm_Num_ int // formallized as nat in Isabelle + MsgTerm_Num_ uint // formallized as nat in Isabelle } MsgTerm_Key { @@ -60,7 +60,7 @@ type IO_msgterm adt { } MsgTerm_FS { - MsgTerm_FS_ seq[IO_msgterm] + MsgTerm_FS_ set[IO_msgterm] } MsgTerm_MPair { @@ -149,41 +149,66 @@ type IO_Link adt { // However, it is not clear at the moment how these should be translated to Gobra and whether they // should have proof obligations attached, or can just be assumed to exist. -ghost -decreases -pure func (dp DataPlaneSpec) rid_as(p IO_rid) IO_as +// ghost +// decreases +// pure func (dp DataPlaneSpec) rid_as(p IO_rid) IO_as +//TODO: should be put p1 == dp.getLocalIA in the precondition? +//There is some freedom in how to define the function ghost decreases -pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link +pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{ + return match p1 { + case dp.getLocalIA() : p2 in domain(dp.linkTypes) ? dp.linkTypes[p2] : IO_NoLink{} + default : IO_NoLink{} + } +} ghost decreases -pure func (dp DataPlaneSpec) egif_prov2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) egif_prov2(hf1 IO_HF, asid IO_as) bool{ + return dp.egif2_type(hf1, asid, IO_Link(IO_CustProv{})) +} + ghost decreases -pure func (dp DataPlaneSpec) egif_core2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) egif_core2(hf1 IO_HF, asid IO_as) bool{ + return dp.egif2_type(hf1, asid, IO_Link(IO_PeerOrCore{})) +} ghost decreases -pure func (dp DataPlaneSpec) egif_cust2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) egif_cust2(hf1 IO_HF, asid IO_as) bool{ + return dp.egif2_type(hf1, asid, IO_Link(IO_ProvCust{})) +} ghost decreases -pure func (dp DataPlaneSpec) inif_cust2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) inif_cust2(hf1 IO_HF, asid IO_as) bool{ + return dp.inif2_type(hf1, asid, IO_Link(IO_ProvCust{})) +} ghost decreases -pure func (dp DataPlaneSpec) inif_core2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) inif_core2(hf1 IO_HF, asid IO_as) bool{ + return dp.inif2_type(hf1, asid, IO_Link(IO_PeerOrCore{})) +} ghost decreases -pure func (dp DataPlaneSpec) inif_prov2(hf1 IO_HF, asid IO_as) bool +pure func (dp DataPlaneSpec) inif_prov2(hf1 IO_HF, asid IO_as) bool{ + return dp.inif2_type(hf1, asid, IO_Link(IO_CustProv{})) +} ghost decreases -pure func (dp DataPlaneSpec) 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{ + return match ifs { + case none[IO_ifs] : false + default : dp.link_type(asid, get(ifs)) == link + } +} type ext2_rec struct { op1 IO_as @@ -213,10 +238,10 @@ type IO_dp2_state adt { // 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 +pure func (m IO_msgterm) extract_asid() IO_as{ + return m.MsgTerm_Hash_.MsgTerm_MPair_1.MsgTerm_Key_.Key_macK_ +} /* End of To clarify */ diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 8995bc745..2ea87d1e2 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -23,29 +23,83 @@ 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_as_set() set[IO_as] { + return dp.topology.core_as_set +} + +ghost +decreases +pure func if2term(ifs option[IO_ifs]) IO_msgterm { + return match ifs { + case none[IO_ifs] : MsgTerm_Empty{} + default : IO_msgterm(MsgTerm_AS{IO_as(get(ifs))}) + } +} + + +ghost +decreases +pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf IO_HF) bool { + return let inif := hf.InIF2 in + let egif := hf.EgIF2 in + let x := hf.HVF in + let l := IO_msgterm(MsgTerm_L{ + seq[IO_msgterm]{ + IO_msgterm(MsgTerm_Num{ts}), + if2term(inif), + if2term(egif), + IO_msgterm(MsgTerm_FS{uinfo})}}) in + x == mac(macKey(asidToKey(dp.asid())), l) +} ghost decreases -pure func (dp DataPlaneSpec) hf_valid(p1 bool, p2 uint, p3 set[IO_msgterm], p4 IO_HF) bool +pure func macKey(key IO_key) IO_msgterm { + return IO_msgterm(MsgTerm_Key{key}) +} + +ghost +decreases +pure func mac(fst IO_msgterm, snd IO_msgterm) IO_msgterm { + return IO_msgterm( MsgTerm_Hash { + MsgTerm_Hash_ : IO_msgterm( MsgTerm_MPair{ + MsgTerm_MPair_1 : fst, + MsgTerm_MPair_2 : snd, + }), + }) +} +// helper func ghost decreases -pure func (dp DataPlaneSpec) upd_uinfo(p1 set[IO_msgterm], p2 IO_HF) set[IO_msgterm] +pure func asidToKey(asid IO_as) IO_key{ + return IO_key(Key_macK{asid}) +} ghost decreases -pure func (dp DataPlaneSpec) rid() IO_rid +pure func (dp DataPlaneSpec) upd_uinfo(segid set[IO_msgterm], hf IO_HF) set[IO_msgterm]{ + return let setHVF := set[IO_msgterm]{hf.HVF} in + (segid union setHVF) setminus (segid intersection setHVF) +} ghost decreases pure func (dp DataPlaneSpec) asid() IO_as { - return dp.rid_as(dp.rid()) + return dp.getLocalIA() } +// TODO: There is some freedom in how to define the function +// Given the router's asid and outgoing interface, there is a neighbor ASID a2 which can be reached via interface i2. +// This makes only sense if nextif == i2. ghost decreases -pure func (dp DataPlaneSpec) 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{ + return asid == dp.getLocalIA() && + nextif == i2 && + i2 in domain(dp.neighborIAs) && + a2 == dp.getNeighborIA(i2) +} ghost decreases @@ -73,16 +127,29 @@ pure func insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k option[IO_ifs], v IO_ buf[k = newSet] } -// TODO: try to remove the existencials here +// TODO: double check that this instantiation of the existential quantifier is correct ghost +requires len(m.CurrSeg.Future) > 0 +requires len(newpkt.CurrSeg.Future) > 0 decreases 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)) + return let currseg := m.CurrSeg in + let hf1, fut := currseg.Future[0], currseg.Future[1:] in + let traversedseg := dp.dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) in + dp.dp2_forward_ext_guard(dp.asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) && + //let i2 := currseg.ConsDir ? hf1.EgIF2 : hf1.InIF2 in //not really necessary since the equality i2 == nextif is already checked in dp2_forward_ext_guard + let a2 := newpkt.CurrSeg.Future[0].extr_asid() in + dp.is_target(dp.asid(), nextif, a2, nextif) + // (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 +requires len(m.CurrSeg.Future) > 0 +requires len(newpkt.CurrSeg.Future) > 0 decreases pure func (dp DataPlaneSpec) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif option[IO_ifs]) bool { return match nextif { @@ -92,6 +159,8 @@ pure func (dp DataPlaneSpec) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif opti } ghost +requires len(intermediatepkt.CurrSeg.Future) > 0 +requires len(newpkt.CurrSeg.Future) > 0 decreases pure func (dp DataPlaneSpec) dp3s_xover_common( s IO_dp3s_state_local, From e4be0b86834ec6da846c6437868dbaaaa0b1bbb5 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 18 Oct 2023 21:44:32 +0200 Subject: [PATCH 07/18] merge problems fix --- verification/io/dataplane_abstract.gobra | 2 +- verification/io/io-spec.gobra | 93 ++++++------------------ verification/io/other_defs.gobra | 14 ++-- verification/io/router.gobra | 17 +++-- 4 files changed, 43 insertions(+), 83 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index f6fda5352..bf438353b 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -32,7 +32,7 @@ type DataPlaneSpec adt { type TopologySpec adt { TopologySpec_{ coreAS set[IO_as] - links dict[IO_as](dict[IO_ifs]IO_as) + links dict[IO_as](dict[IO_ifs]IO_as) } } diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 357518276..75101a1aa 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -32,16 +32,16 @@ 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 CBio_IN_bio3s_enter_T(t Place, v IO_val) Place @@ -92,8 +92,10 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local let currseg := v.IO_Internal_val1_1.CurrSeg in let hf1, fut := currseg.Future[0], currseg.Future[1:] in let traversedseg := match v.IO_Internal_val1_4{ - case none[IO_ifs] : dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) - default : dp.dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) + case none[IO_ifs]: + dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) + default: + dp.dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) } in dp.dp2_enter_guard( v.IO_Internal_val1_1, @@ -129,7 +131,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_enter(s IO_dp3s_state_local, t Place) }) } -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 CBio_IN_bio3s_xover_up2down(t, v) @@ -142,8 +144,10 @@ 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 + 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 && @@ -166,64 +170,15 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta } } -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)) } ( - 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 - }) -} - -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 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 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 - 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 && - len(v.IO_Internal_val1_3.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_core2_link_type(hf1, hf2, dp.asid(), currseg.ConsDir) && - 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) }{ CBio_IN_bio3s_xover_up2down(t, v) } { dp.dp3s_iospec_ordered(dp.dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_up2down_T(t, v)) } ( match v { case IO_Internal_val1{_, _, ?newpkt, ?nextif}: (dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==> (CBio_IN_bio3s_xover_up2down(t, v) && - dp.dp3s_iospec_ordered( - dp.dp3s_add_obuf(s, nextif, newpkt), - dp3s_iospec_bio3s_xover_up2down_T(t, v)))) + dp.dp3s_iospec_ordered( + dp.dp3s_add_obuf(s, nextif, newpkt), + dp3s_iospec_bio3s_xover_up2down_T(t, v)))) default: true }) @@ -237,8 +192,8 @@ 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 +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() && let currseg := v.IO_Internal_val1_1.CurrSeg in @@ -250,8 +205,9 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ currseg.ConsDir == nextseg.ConsDir && len(nextseg.Future) > 0 && len(currseg.Future) > 0 && + len(v.IO_Internal_val1_3.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, @@ -264,7 +220,7 @@ 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,)) }) } @@ -282,8 +238,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core(s IO_dp3s_state_local, t Pl }) } - -pred (dp DataPlaneSpec) CBio_IN_bio3s_exit(t Place, v IO_val) +pred CBio_IN_bio3s_exit(t Place, v IO_val) ghost requires CBio_IN_bio3s_exit(t, v) @@ -316,7 +271,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_exit(s IO_dp3s_state_local, t Place) { } -pred (dp DataPlaneSpec) CBioIO_bio3s_send(t Place, v IO_val) +pred CBioIO_bio3s_send(t Place, v IO_val) ghost requires CBioIO_bio3s_send(t, v) @@ -347,7 +302,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_send(s IO_dp3s_state_local, t Place) { }) } -pred (dp DataPlaneSpec) CBioIO_bio3s_recv(t Place) +pred CBioIO_bio3s_recv(t Place) ghost requires CBioIO_bio3s_recv(t) @@ -370,7 +325,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_recv(s IO_dp3s_state_local, t Place) { }) } -pred (dp DataPlaneSpec) CBio_Skip(t Place) +pred CBio_Skip(t Place) ghost requires CBio_Skip(t) diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index bab284e94..a8a777e83 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -134,14 +134,16 @@ type IO_Link adt { // decreases // pure func (dp DataPlaneSpec) rid_as(p IO_rid) IO_as -//TODO: should be put p1 == dp.getLocalIA in the precondition? +//TODO: should be put p1 == dp.GetLocalIA in the precondition? //There is some freedom in how to define the function ghost decreases pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{ return match p1 { - case dp.getLocalIA() : p2 in domain(dp.linkTypes) ? dp.linkTypes[p2] : IO_NoLink{} - default : IO_NoLink{} + case dp.GetLocalIA(): + p2 in domain(dp.linkTypes) ? dp.linkTypes[p2] : IO_NoLink{} + default: + IO_NoLink{} } } @@ -186,8 +188,10 @@ ghost decreases pure func (dp DataPlaneSpec) if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool{ return match ifs { - case none[IO_ifs] : false - default : dp.link_type(asid, get(ifs)) == link + case none[IO_ifs]: + false + default: + dp.link_type(asid, get(ifs)) == link } } diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 24e14155f..11c4bd164 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -23,20 +23,21 @@ package io // This function corresponds to function 'core' in the IO spec ghost decreases -pure func (dp DataPlaneSpec) core_as_set() set[IO_as] { - return dp.topology.core_as_set +pure func (dp DataPlaneSpec) core() set[IO_as] { + return dp.GetCoreAS() } ghost decreases pure func if2term(ifs option[IO_ifs]) IO_msgterm { return match ifs { - case none[IO_ifs] : MsgTerm_Empty{} - default : IO_msgterm(MsgTerm_AS{IO_as(get(ifs))}) + case none[IO_ifs]: + MsgTerm_Empty{} + default: + IO_msgterm(MsgTerm_AS{IO_as(get(ifs))}) } } - ghost decreases pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf IO_HF) bool { @@ -86,7 +87,7 @@ pure func (dp DataPlaneSpec) upd_uinfo(segid set[IO_msgterm], hf IO_HF) set[IO_m ghost decreases pure func (dp DataPlaneSpec) asid() IO_as { - return dp.getLocalIA() + return dp.GetLocalIA() } // TODO: There is some freedom in how to define the function @@ -95,10 +96,10 @@ pure func (dp DataPlaneSpec) asid() IO_as { ghost decreases pure func (dp DataPlaneSpec) is_target(asid IO_as, nextif IO_ifs, a2 IO_as, i2 IO_ifs) bool{ - return asid == dp.getLocalIA() && + return asid == dp.GetLocalIA() && nextif == i2 && i2 in domain(dp.neighborIAs) && - a2 == dp.getNeighborIA(i2) + a2 == dp.GetNeighborIA(i2) } ghost From 37c7ac6bf220bb9f9e93827b365e230d93ac2ff2 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 18 Oct 2023 21:55:40 +0200 Subject: [PATCH 08/18] cosmetic changes --- verification/io/io-spec.gobra | 68 ++++++++++++++++---------------- verification/io/other_defs.gobra | 21 +--------- verification/io/router.gobra | 9 ++--- 3 files changed, 40 insertions(+), 58 deletions(-) diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 75101a1aa..7e3954a9c 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -124,7 +124,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_enter(s IO_dp3s_state_local, t Place) (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), + dp3s_add_obuf(s, nextif, newpkt), CBio_IN_bio3s_enter_T(t, v)))) default: true @@ -143,41 +143,41 @@ 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 - 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 && - len(v.IO_Internal_val1_3.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 && + len(v.IO_Internal_val1_3.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) }{ 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)) } ( + 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(dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_up2down_T(t, v)) } ( match v { case IO_Internal_val1{_, _, ?newpkt, ?nextif}: (dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==> (CBio_IN_bio3s_xover_up2down(t, v) && dp.dp3s_iospec_ordered( - dp.dp3s_add_obuf(s, nextif, newpkt), + dp3s_add_obuf(s, nextif, newpkt), dp3s_iospec_bio3s_xover_up2down_T(t, v)))) default: true @@ -220,18 +220,18 @@ 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) }{ 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)) } ( + 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(dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_core_T(t, v)) } ( match v { case IO_Internal_val1{_, _, ?newpkt, ?nextif}: (dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) ==> (CBio_IN_bio3s_xover_core(t, v) && dp.dp3s_iospec_ordered( - dp.dp3s_add_obuf(s, nextif, newpkt), + dp3s_add_obuf(s, nextif, newpkt), dp3s_iospec_bio3s_xover_core_T(t, v)))) default: true @@ -257,13 +257,13 @@ 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) }{ 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)) } ( + forall v IO_val :: { dp.dp3s_iospec_bio3s_exit_guard(s, t, v) }{ CBio_IN_bio3s_exit(t, v) }{ dp.dp3s_iospec_ordered(dp3s_add_obuf(s, some(v.IO_Internal_val2_3), v.IO_Internal_val2_2), dp3s_iospec_bio3s_exit_T(t, v)) } ( match v { case IO_Internal_val2{_, ?newpkt, ?nextif}: (dp.dp3s_iospec_bio3s_exit_guard(s, t, v) ==> (CBio_IN_bio3s_exit(t, v) && dp.dp3s_iospec_ordered( - dp.dp3s_add_obuf(s, some(nextif), newpkt), + dp3s_add_obuf(s, some(nextif), newpkt), dp3s_iospec_bio3s_exit_T(t, v)))) default: true @@ -317,7 +317,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_recv(s IO_dp3s_state_local, t Place) { (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)) + 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: diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index a8a777e83..d2d5c3de8 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -34,9 +34,6 @@ type IO_ifs uint16 // type of AS identifiers type IO_as uint -// router ids -//type IO_rid uint - // msgTerms consist of terms from our term algebra. type IO_msgterm adt { MsgTerm_Empty{} @@ -122,20 +119,9 @@ type IO_Link adt { IO_PeerOrCore{} IO_NoLink{} } -/* End of Link Types */ - -/* To clarify, the existence of the following functions seems to be assumed */ -// NOTE: -// The following functions are provided as parameters to various locales in the Isabelle formalization. -// However, it is not clear at the moment how these should be translated to Gobra and whether they -// should have proof obligations attached, or can just be assumed to exist. -// ghost -// decreases -// pure func (dp DataPlaneSpec) rid_as(p IO_rid) IO_as - -//TODO: should be put p1 == dp.GetLocalIA in the precondition? -//There is some freedom in how to define the function +// TODO: should be put p1 == dp.GetLocalIA() in the precondition? +// This function is provided as locale in the Isabelle formalization. ghost decreases pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{ @@ -211,11 +197,8 @@ type IO_dp2_state adt { } } -// extract_asid ghost decreases pure func (m IO_msgterm) extract_asid() IO_as { return m.MsgTerm_Hash_.MsgTerm_MPair_1.MsgTerm_Key_.Key_macK_ } - -/* End of To clarify */ \ No newline at end of file diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 11c4bd164..abd2a5cd5 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -90,9 +90,8 @@ pure func (dp DataPlaneSpec) asid() IO_as { return dp.GetLocalIA() } -// TODO: There is some freedom in how to define the function -// Given the router's asid and outgoing interface, there is a neighbor ASID a2 which can be reached via interface i2. -// This makes only sense if nextif == i2. +// TODO: fix function +// This function is provided as locale in the Isabelle formalization. ghost decreases pure func (dp DataPlaneSpec) is_target(asid IO_as, nextif IO_ifs, a2 IO_as, i2 IO_ifs) bool{ @@ -104,7 +103,7 @@ pure func (dp DataPlaneSpec) is_target(asid IO_as, nextif IO_ifs, a2 IO_as, i2 I 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 { +pure func dp3s_add_ibuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO_dp3s_state_local { return IO_dp3s_state_local_{ ibuf: insert(s.ibuf, i, pkt), obuf: s.obuf, @@ -113,7 +112,7 @@ pure func (dp DataPlaneSpec) dp3s_add_ibuf(s IO_dp3s_state_local, i option[IO_if ghost decreases -pure func (dp DataPlaneSpec) dp3s_add_obuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO_dp3s_state_local { +pure func 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), From a0b37b602177d02395f0b79b44fac5da40e76547 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 18 Oct 2023 22:02:03 +0200 Subject: [PATCH 09/18] IO-spec fix --- verification/io/io-spec.gobra | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 7e3954a9c..f00916c1d 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -85,7 +85,7 @@ 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) ==> + 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 && len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && @@ -249,7 +249,7 @@ 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) ==> + 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)) && len(v.IO_Internal_val2_1.CurrSeg.Future) > 0 && len(v.IO_Internal_val2_2.CurrSeg.Future) > 0 && @@ -282,7 +282,7 @@ 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) ==> + 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)) } From 0c2ee68a8dceb28c484f32a090755861298393ab Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 19 Oct 2023 10:54:43 +0200 Subject: [PATCH 10/18] adding receiving interface to topology --- verification/io/dataplane_abstract.gobra | 40 ++++++++++++++++++++---- 1 file changed, 34 insertions(+), 6 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index bf438353b..f73b2a1a4 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -25,24 +25,37 @@ type DataPlaneSpec adt { } } -// TopologySpec provides information about the entire network topology. +// 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. +// links[a1][x] == (a2,y) means that AS a1 and AS a2 share an edge via interface x and y, respectively. type TopologySpec adt { TopologySpec_{ coreAS set[IO_as] - links dict[IO_as](dict[IO_ifs]IO_as) + links dict[IO_as](dict[IO_ifs]AsIfsPair) } } +type AsIfsPair struct { + asid IO_as + ifs IO_ifs +} + +// TODO: rewrite function when gobra allows accessing two-dimensional arrays ghost decreases pure func (dp DataPlaneSpec) Valid() bool{ - return domain(dp.linkTypes) == domain(dp.neighborIAs) && + return domain(dp.linkTypes) == domain(dp.neighborIAs) && dp.localIA in domain(dp.topology.links) && - dp.neighborIAs == dp.topology.links[dp.localIA] && - (forall core IO_as :: {core in dp.topology.coreAS} core in dp.topology.coreAS ==> core in domain(dp.topology.links)) + domain(dp.neighborIAs) == domain(dictCast(dp.topology.links, dp.localIA)) && + (forall core IO_as :: {core in dp.topology.coreAS} core in dp.topology.coreAS ==> + core in domain(dp.topology.links)) && + (forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} ifs in domain(dp.neighborIAs) ==> + dp.neighborIAs[ifs] == dictCast(dp.topology.links, dp.localIA)[ifs].asid) && + (forall asid IO_as, ifs IO_ifs :: (asid in domain(dp.topology.links) && ifs in domain(dictCast(dp.topology.links, asid))) ==> + dp.lookup(asid, ifs).asid in domain(dp.topology.links) && + dp.lookup(asid, ifs).ifs in domain(dictCast(dp.topology.links, dp.lookup(asid, ifs).asid)) && + dp.lookup(dp.lookup(asid, ifs).asid, dp.lookup(asid, ifs).ifs) == AsIfsPair{asid, ifs}) } ghost @@ -70,3 +83,18 @@ decreases pure func (dp DataPlaneSpec) GetCoreAS() set[IO_as] { return dp.topology.coreAS } + +ghost +requires asid in domain(dp.topology.links) +requires ifs in domain(dictCast(dp.topology.links, asid)) +decreases +pure func(dp DataPlaneSpec) lookup(asid IO_as, ifs IO_ifs) AsIfsPair { + return dictCast(dp.topology.links, asid)[ifs] +} + +ghost +requires idx in domain(m) +decreases +pure func dictCast(m dict[IO_as](dict[IO_ifs]AsIfsPair), idx IO_as) dict[IO_ifs]AsIfsPair{ + return m[idx] +} \ No newline at end of file From 33cb8d59c5863e02c77595778fa81080b47d0406 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 1 Nov 2023 13:52:01 +0100 Subject: [PATCH 11/18] concretize dp3s_forward_ext --- verification/io/dataplane_abstract.gobra | 45 ++++++++++++------------ verification/io/io-spec.gobra | 31 +++++++++------- verification/io/other_defs.gobra | 9 +++++ verification/io/router.gobra | 30 ++++++++-------- verification/io/router_events.gobra | 22 +++++++----- verification/io/segment-defs.gobra | 16 ++++----- verification/io/xover.gobra | 11 ++++-- 7 files changed, 95 insertions(+), 69 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index f73b2a1a4..1b84c87d7 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -28,11 +28,11 @@ 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[a1][x] == (a2,y) means that AS a1 and AS a2 share an edge via interface x and y, respectively. +// links[(a1,x)] == (a2,y) means that AS a1 and AS a2 share an edge via interface x and y, respectively. type TopologySpec adt { TopologySpec_{ coreAS set[IO_as] - links dict[IO_as](dict[IO_ifs]AsIfsPair) + links dict[AsIfsPair]AsIfsPair } } @@ -41,21 +41,18 @@ type AsIfsPair struct { ifs IO_ifs } -// TODO: rewrite function when gobra allows accessing two-dimensional arrays ghost decreases -pure func (dp DataPlaneSpec) Valid() bool{ +pure func (dp DataPlaneSpec) Valid() bool { return domain(dp.linkTypes) == domain(dp.neighborIAs) && - dp.localIA in domain(dp.topology.links) && - domain(dp.neighborIAs) == domain(dictCast(dp.topology.links, dp.localIA)) && - (forall core IO_as :: {core in dp.topology.coreAS} core in dp.topology.coreAS ==> - core in domain(dp.topology.links)) && - (forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} ifs in domain(dp.neighborIAs) ==> - dp.neighborIAs[ifs] == dictCast(dp.topology.links, dp.localIA)[ifs].asid) && - (forall asid IO_as, ifs IO_ifs :: (asid in domain(dp.topology.links) && ifs in domain(dictCast(dp.topology.links, asid))) ==> - dp.lookup(asid, ifs).asid in domain(dp.topology.links) && - dp.lookup(asid, ifs).ifs in domain(dictCast(dp.topology.links, dp.lookup(asid, ifs).asid)) && - dp.lookup(dp.lookup(asid, ifs).asid, dp.lookup(asid, ifs).ifs) == AsIfsPair{asid, ifs}) + (forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} ifs in domain(dp.neighborIAs) ==> + (AsIfsPair{dp.localIA, ifs} in domain(dp.topology.links) && + dp.Lookup(AsIfsPair{dp.localIA, ifs}).asid == dp.neighborIAs[ifs])) && + (forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} AsIfsPair{dp.localIA, ifs} in domain(dp.topology.links) ==> + ifs in domain(dp.neighborIAs)) && + (forall pairs AsIfsPair :: {dp.Lookup(pairs)} pairs in domain(dp.topology.links) ==> + dp.Lookup(pairs) in domain(dp.topology.links) && + dp.Lookup(dp.Lookup(pairs)) == pairs) } ghost @@ -65,6 +62,12 @@ pure func (dp DataPlaneSpec) GetLinkType(ifs IO_ifs) IO_Link { return dp.linkTypes[ifs] } +ghost +decreases +pure func (dp DataPlaneSpec) GetNeighborIAs() dict[IO_ifs]IO_as { + return dp.neighborIAs +} + ghost requires ifs in domain(dp.neighborIAs) decreases @@ -85,16 +88,14 @@ pure func (dp DataPlaneSpec) GetCoreAS() set[IO_as] { } ghost -requires asid in domain(dp.topology.links) -requires ifs in domain(dictCast(dp.topology.links, asid)) decreases -pure func(dp DataPlaneSpec) lookup(asid IO_as, ifs IO_ifs) AsIfsPair { - return dictCast(dp.topology.links, asid)[ifs] +pure func (dp DataPlaneSpec) GetLinks() dict[AsIfsPair]AsIfsPair { + return dp.topology.links } -ghost -requires idx in domain(m) +ghost +requires pair in domain(dp.topology.links) decreases -pure func dictCast(m dict[IO_as](dict[IO_ifs]AsIfsPair), idx IO_as) dict[IO_ifs]AsIfsPair{ - return m[idx] +pure func(dp DataPlaneSpec) Lookup(pair AsIfsPair) AsIfsPair { + return dp.topology.links[pair] } \ No newline at end of file diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index f00916c1d..209d0294d 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -49,9 +49,9 @@ 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 { +pure func dp3s_iospec_bio3s_create_guard_traversedseg(currseg IO_seg3) IO_seg3 { return let uinfo := !currseg.ConsDir ? - dp.upd_uinfo(currseg.UInfo, currseg.Future[0]) : + upd_uinfo(currseg.UInfo, currseg.Future[0]) : currseg.UInfo in IO_seg3_ { AInfo: currseg.AInfo, @@ -66,9 +66,9 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg(currseg ghost requires len(currseg.Future) > 0 decreases -pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg IO_seg3) IO_seg3 { +pure func 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]) : + upd_uinfo(currseg.UInfo, currseg.Future[0]) : currseg.UInfo in IO_seg3_ { AInfo: currseg.AInfo, @@ -83,6 +83,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg_inc(cur // This corresponds to the condition of the if statement in the io-spec case for enter ghost requires v.isIO_Internal_val1 +requires dp.Valid() 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) && @@ -93,9 +94,9 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local let hf1, fut := currseg.Future[0], currseg.Future[1:] in let traversedseg := match v.IO_Internal_val1_4{ case none[IO_ifs]: - dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) + dp3s_iospec_bio3s_create_guard_traversedseg(currseg) default: - dp.dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) + dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) } in dp.dp2_enter_guard( v.IO_Internal_val1_1, @@ -121,7 +122,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_enter(s IO_dp3s_state_local, t Place) 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.Valid() && dp.dp3s_iospec_bio3s_enter_guard(s, t, v) ==> (CBio_IN_bio3s_enter(t, v) && dp.dp3s_iospec_ordered( dp3s_add_obuf(s, nextif, newpkt), @@ -140,6 +141,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 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { return let currseg := v.IO_Internal_val1_1.CurrSeg in @@ -153,7 +155,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta len(currseg.Future) > 0 && len(v.IO_Internal_val1_3.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 := dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) in (dp.xover_up2down2_link_type(dp.asid(), hf1, hf2) && dp.dp3s_xover_common( s, @@ -174,7 +176,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down(s IO_dp3s_state_local, t 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(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.Valid() && dp.dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==> (CBio_IN_bio3s_xover_up2down(t, v) && dp.dp3s_iospec_ordered( dp3s_add_obuf(s, nextif, newpkt), @@ -193,6 +195,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 requires v.isIO_Internal_val1 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { return (dp.asid() in dp.core() && @@ -207,7 +210,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ len(currseg.Future) > 0 && len(v.IO_Internal_val1_3.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 := 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, @@ -228,7 +231,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core(s IO_dp3s_state_local, t Pl 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(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.Valid() && dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) ==> (CBio_IN_bio3s_xover_core(t, v) && dp.dp3s_iospec_ordered( dp3s_add_obuf(s, nextif, newpkt), @@ -247,6 +250,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 +requires dp.Valid() 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) && @@ -260,7 +264,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_exit(s IO_dp3s_state_local, t Place) { forall v IO_val :: { dp.dp3s_iospec_bio3s_exit_guard(s, t, v) }{ CBio_IN_bio3s_exit(t, v) }{ dp.dp3s_iospec_ordered(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.Valid() && dp.dp3s_iospec_bio3s_exit_guard(s, t, v) ==> (CBio_IN_bio3s_exit(t, v) && dp.dp3s_iospec_ordered( dp3s_add_obuf(s, some(nextif), newpkt), @@ -280,6 +284,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 +requires dp.Valid() 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) && @@ -291,7 +296,7 @@ pred (dp DataPlaneSpec) dp3s_iospec_bio3s_send(s IO_dp3s_state_local, t Place) { forall v IO_val :: { dp.dp3s_iospec_bio3s_send_guard(s, t, v) }{ CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(t, v)) }{ CBioIO_bio3s_send(t, v) }{ dp.dp3s_iospec_ordered(s, dp3s_iospec_bio3s_send_T(t, v)) } ( match v { case IO_val_Pkt2{_, _}: - (dp.dp3s_iospec_bio3s_send_guard(s, t, v) ==> + (dp.Valid() && 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{_, _}: diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index d2d5c3de8..cb1a2861c 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -121,8 +121,10 @@ type IO_Link adt { } // TODO: should be put p1 == dp.GetLocalIA() in the precondition? +// Should we put dp.Valid() in precondition? // This function is provided as locale in the Isabelle formalization. ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{ return match p1 { @@ -134,6 +136,7 @@ pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{ } ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) egif_prov2(hf1 IO_HF, asid IO_as) bool{ return dp.egif2_type(hf1, asid, IO_Link(IO_CustProv{})) @@ -141,36 +144,42 @@ pure func (dp DataPlaneSpec) egif_prov2(hf1 IO_HF, asid IO_as) bool{ ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) egif_core2(hf1 IO_HF, asid IO_as) bool{ return dp.egif2_type(hf1, asid, IO_Link(IO_PeerOrCore{})) } ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) egif_cust2(hf1 IO_HF, asid IO_as) bool{ return dp.egif2_type(hf1, asid, IO_Link(IO_ProvCust{})) } ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) inif_cust2(hf1 IO_HF, asid IO_as) bool{ return dp.inif2_type(hf1, asid, IO_Link(IO_ProvCust{})) } ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) inif_core2(hf1 IO_HF, asid IO_as) bool{ return dp.inif2_type(hf1, asid, IO_Link(IO_PeerOrCore{})) } ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) inif_prov2(hf1 IO_HF, asid IO_as) bool{ return dp.inif2_type(hf1, asid, IO_Link(IO_CustProv{})) } ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool{ return match ifs { diff --git a/verification/io/router.gobra b/verification/io/router.gobra index abd2a5cd5..e59c1d58b 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -22,6 +22,7 @@ package io // This function corresponds to function 'core' in the IO spec ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) core() set[IO_as] { return dp.GetCoreAS() @@ -79,7 +80,7 @@ pure func asidToKey(asid IO_as) IO_key{ ghost decreases -pure func (dp DataPlaneSpec) upd_uinfo(segid set[IO_msgterm], hf IO_HF) set[IO_msgterm]{ +pure func upd_uinfo(segid set[IO_msgterm], hf IO_HF) set[IO_msgterm]{ return let setHVF := set[IO_msgterm]{hf.HVF} in (segid union setHVF) setminus (segid intersection setHVF) } @@ -90,15 +91,15 @@ pure func (dp DataPlaneSpec) asid() IO_as { return dp.GetLocalIA() } -// TODO: fix function + // This function is provided as locale in the Isabelle formalization. ghost +requires dp.Valid() decreases -pure func (dp DataPlaneSpec) 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 { return asid == dp.GetLocalIA() && - nextif == i2 && - i2 in domain(dp.neighborIAs) && - a2 == dp.GetNeighborIA(i2) + nextif in domain(dp.GetNeighborIAs()) && + dp.Lookup(AsIfsPair{asid, nextif}) == AsIfsPair{a2, i2} } ghost @@ -127,29 +128,27 @@ pure func insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k option[IO_ifs], v IO_ buf[k = newSet] } -// TODO: double check that this instantiation of the existential quantifier is correct ghost requires len(m.CurrSeg.Future) > 0 requires len(newpkt.CurrSeg.Future) > 0 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif IO_ifs) bool { return let currseg := m.CurrSeg in let hf1, fut := currseg.Future[0], currseg.Future[1:] in - let traversedseg := dp.dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) in + let traversedseg := dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) in dp.dp2_forward_ext_guard(dp.asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) && - //let i2 := currseg.ConsDir ? hf1.EgIF2 : hf1.InIF2 in //not really necessary since the equality i2 == nextif is already checked in dp2_forward_ext_guard - let a2 := newpkt.CurrSeg.Future[0].extr_asid() in - dp.is_target(dp.asid(), nextif, a2, nextif) - // (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)) + let hf2 := newpkt.CurrSeg.Future[0] in + let a2 := dp.GetNeighborIA(nextif) in + let i2 := dp.Lookup(AsIfsPair{dp.asid(), nextif}).ifs in + dp.is_target(dp.asid(), nextif, a2, i2) } // TODO: should we change IO_ifs to being implemented as an option type? ghost requires len(m.CurrSeg.Future) > 0 requires len(newpkt.CurrSeg.Future) > 0 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif option[IO_ifs]) bool { return match nextif { @@ -163,6 +162,7 @@ pure func (dp DataPlaneSpec) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif opti ghost requires len(intermediatepkt.CurrSeg.Future) > 0 requires len(newpkt.CurrSeg.Future) > 0 +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_xover_common( s IO_dp3s_state_local, diff --git a/verification/io/router_events.gobra b/verification/io/router_events.gobra index ea64ce2b7..d277ad3f2 100644 --- a/verification/io/router_events.gobra +++ b/verification/io/router_events.gobra @@ -19,6 +19,7 @@ package io ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs) bool { return d? @@ -28,6 +29,7 @@ pure func (dp DataPlaneSpec) dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs) /* Abbreviations */ ghost +requires dp.Valid() decreases 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)) || @@ -36,6 +38,7 @@ pure func (dp DataPlaneSpec) valid_link_types2(hf1 IO_HF, a IO_as) bool { } ghost +requires dp.Valid() decreases 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)) || @@ -45,6 +48,7 @@ pure func (dp DataPlaneSpec) valid_link_types_in2(hf1 IO_HF, a IO_as) bool { /* End of Abbreviations */ ghost +requires dp.Valid() decreases 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)) || @@ -53,40 +57,42 @@ pure func (dp DataPlaneSpec) dp2_check_interface(d bool, asid IO_as, hf1 IO_HF, ghost decreases -pure func (dp DataPlaneSpec) dp2_exit_interface(d bool, asid IO_as, hf1 IO_HF, outif IO_ifs) bool { +pure func 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 +requires dp.Valid() decreases 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: - dp.dp2_exit_interface(currseg.ConsDir, asid, hf1, nextif) && + dp2_exit_interface(currseg.ConsDir, asid, hf1, nextif) && // Next validate the current hop field with the *original* UInfo field): 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: - dp.inc_seg2(currseg, traversedseg, hf1, fut) && + 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 - dp.update_uinfo(currseg.ConsDir, currseg, traversedseg, hf1) && + update_uinfo(currseg.ConsDir, currseg, traversedseg, hf1) && // Other fields: no update - dp.same_other2(currseg, traversedseg) + same_other2(currseg, traversedseg) } // A packet is received from an ext state (i.e., an inter-AS channel) and is forwarded (either internally or externally) ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp2_enter_guard(m IO_pkt2, currseg IO_seg2, traversedseg IO_seg2, asid IO_as, hf1 IO_HF, recvif IO_ifs, fut seq[IO_HF]) bool { return m.CurrSeg == currseg && currseg.Future == seq[IO_HF]{hf1} ++ fut && dp.dp2_check_interface(currseg.ConsDir, asid, hf1, recvif) && - dp.update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) && - dp.same_segment2(currseg, traversedseg) && - dp.same_other2(currseg, traversedseg) && + update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) && + same_segment2(currseg, traversedseg) && + same_other2(currseg, traversedseg) && dp.hf_valid(currseg.ConsDir, currseg.AInfo, traversedseg.UInfo, hf1) && hf1.extr_asid() == asid } diff --git a/verification/io/segment-defs.gobra b/verification/io/segment-defs.gobra index a89feca0a..5349fe31b 100644 --- a/verification/io/segment-defs.gobra +++ b/verification/io/segment-defs.gobra @@ -23,7 +23,7 @@ package io ghost decreases -pure func (dp DataPlaneSpec) inc_seg2(currseg, traversedseg IO_seg2, hf1 IO_HF, fut seq[IO_HF]) bool { +pure func 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 DataPlaneSpec) inc_seg2(currseg, traversedseg IO_seg2, hf1 IO_HF, ghost decreases -pure func (dp DataPlaneSpec) same_segment2(currseg, traversedseg IO_seg2) bool { +pure func 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 DataPlaneSpec) same_segment2(currseg, traversedseg IO_seg2) bool { ghost decreases -pure func (dp DataPlaneSpec) update_uinfo2(currseg, traversedseg IO_seg2, hf1 IO_HF) bool { - return traversedseg.UInfo === dp.upd_uinfo(currseg.UInfo, hf1) +pure func update_uinfo2(currseg, traversedseg IO_seg2, hf1 IO_HF) bool { + return traversedseg.UInfo === upd_uinfo(currseg.UInfo, hf1) } ghost decreases -pure func (dp DataPlaneSpec) same_uinfo2(currseg, traversedseg IO_seg2) bool { +pure func same_uinfo2(currseg, traversedseg IO_seg2) bool { return currseg.UInfo === traversedseg.UInfo } ghost decreases -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) +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) } ghost decreases -pure func (dp DataPlaneSpec) same_other2(currseg, traversedseg IO_seg3) bool { +pure func 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 f38b5d15e..80e6ee32c 100644 --- a/verification/io/xover.gobra +++ b/verification/io/xover.gobra @@ -35,6 +35,7 @@ package io // remaining hop field into the Past path, and nextseg, which is // the new segment that we are xovering over to. ghost +requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2, currseg IO_seg2, @@ -54,28 +55,31 @@ pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2, nextseg.Future[0] == 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]{}) && + update_uinfo(!currseg.ConsDir, currseg, traversedseg, hf1) && + inc_seg2(currseg, traversedseg, hf1, seq[IO_HF]{}) && dp.hf_valid(currseg.ConsDir, currseg.AInfo, traversedseg.UInfo, hf1) && dp.hf_valid(nextseg.ConsDir, nextseg.AInfo, nextseg.UInfo, hf2) && hf1.extr_asid() == asid && hf2.extr_asid() == asid && - dp.same_other2(currseg, traversedseg) + same_other2(currseg, traversedseg) } ghost +requires dp.Valid() decreases 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 +requires dp.Valid() decreases 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 +requires dp.Valid() 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{})) || @@ -84,6 +88,7 @@ pure func (dp DataPlaneSpec) xover_up2down2_link_type(asid IO_as, hf1 IO_HF, hf2 } ghost +requires dp.Valid() 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{})) || From dc6f540b68b1fc05c0fd9a7fafdd960e28dddeb3 Mon Sep 17 00:00:00 2001 From: Markus Limbeck <92801626+mlimbeck@users.noreply.github.com> Date: Tue, 14 Nov 2023 14:38:52 +0100 Subject: [PATCH 12/18] 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 +++-- verification/io/router.gobra | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index 1b84c87d7..43a0e9441 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -25,10 +25,11 @@ type DataPlaneSpec adt { } } -// TopologySpec provides information about the entire network topology. +// TopologySpec describes the entire network topology. // coreAS: IDs of the core Autonomous Systems // links: representation of the network topology as a graph. -// links[(a1,x)] == (a2,y) means that AS a1 and AS a2 share an edge via interface x and y, respectively. +// `links[(a1,x)] == (a2,y)` means that the interface x of AS a1 is connected +// to the interface y of AS a2. type TopologySpec adt { TopologySpec_{ coreAS set[IO_as] diff --git a/verification/io/router.gobra b/verification/io/router.gobra index e59c1d58b..b9d359e1d 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -71,7 +71,7 @@ pure func mac(fst IO_msgterm, snd IO_msgterm) IO_msgterm { }) } -// helper func +// helper function, not defined in IO spec ghost decreases pure func asidToKey(asid IO_as) IO_key{ From 0203251a4cc5870ea7fdf0f4a178bd66e4f61434 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Tue, 14 Nov 2023 17:06:03 +0100 Subject: [PATCH 13/18] minor improvements --- verification/io/dataplane_abstract.gobra | 2 +- verification/io/io-spec.gobra | 23 ++++++++++++++--------- verification/io/router.gobra | 13 ++++--------- 3 files changed, 19 insertions(+), 19 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index 43a0e9441..77031aef6 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -51,7 +51,7 @@ pure func (dp DataPlaneSpec) Valid() bool { dp.Lookup(AsIfsPair{dp.localIA, ifs}).asid == dp.neighborIAs[ifs])) && (forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} AsIfsPair{dp.localIA, ifs} in domain(dp.topology.links) ==> ifs in domain(dp.neighborIAs)) && - (forall pairs AsIfsPair :: {dp.Lookup(pairs)} pairs in domain(dp.topology.links) ==> + (forall pairs AsIfsPair :: {dp.Lookup(pairs)} pairs in domain(dp.topology.links) ==> dp.Lookup(pairs) in domain(dp.topology.links) && dp.Lookup(dp.Lookup(pairs)) == pairs) } diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 209d0294d..32b3917e0 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -18,6 +18,10 @@ package io +//Unlike the original IO-spec from Isabelle, we need additional information about the network topology. +//To ensure the well-formedness of all map accesses we require an additional conjunction +//for all the events (dp.Valid()) + // This is the main IO Specification. pred (dp DataPlaneSpec) dp3s_iospec_ordered(s IO_dp3s_state_local, t Place) { dp.dp3s_iospec_bio3s_enter(s, t) && @@ -45,11 +49,12 @@ requires CBio_IN_bio3s_enter(t, v) decreases pure func CBio_IN_bio3s_enter_T(t Place, v IO_val) Place - +/*** Helper functions, not in Isabelle ***/ +//Establishes the traversed segment for packets which are not incremented (internal). ghost requires len(currseg.Future) > 0 decreases -pure func dp3s_iospec_bio3s_create_guard_traversedseg(currseg IO_seg3) IO_seg3 { +pure func EstablishGuardTraversedseg(currseg IO_seg3) IO_seg3 { return let uinfo := !currseg.ConsDir ? upd_uinfo(currseg.UInfo, currseg.Future[0]) : currseg.UInfo in @@ -63,10 +68,11 @@ pure func dp3s_iospec_bio3s_create_guard_traversedseg(currseg IO_seg3) IO_seg3 { History: currseg.History} } +//Establishes the traversed segment for packets that are incremented (external). ghost requires len(currseg.Future) > 0 decreases -pure func dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg IO_seg3) IO_seg3 { +pure func EstablishGuardTraversedsegInc(currseg IO_seg3) IO_seg3 { return let uinfo := !currseg.ConsDir ? upd_uinfo(currseg.UInfo, currseg.Future[0]) : currseg.UInfo in @@ -79,6 +85,7 @@ pure func dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg IO_seg3) IO_se Future: currseg.Future[1:], History: seq[IO_ahi]{currseg.Future[0].Toab()} ++ currseg.History} } +/*** End of helper functions, not in Isabelle ***/ // This corresponds to the condition of the if statement in the io-spec case for enter ghost @@ -89,14 +96,13 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local 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 && - len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let currseg := v.IO_Internal_val1_1.CurrSeg in let hf1, fut := currseg.Future[0], currseg.Future[1:] in let traversedseg := match v.IO_Internal_val1_4{ case none[IO_ifs]: - dp3s_iospec_bio3s_create_guard_traversedseg(currseg) + EstablishGuardTraversedseg(currseg) default: - dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) + EstablishGuardTraversedsegInc(currseg) } in dp.dp2_enter_guard( v.IO_Internal_val1_1, @@ -155,7 +161,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta len(currseg.Future) > 0 && len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in - let traversedseg := dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) in + let traversedseg := EstablishGuardTraversedsegInc(currseg) in (dp.xover_up2down2_link_type(dp.asid(), hf1, hf2) && dp.dp3s_xover_common( s, @@ -210,7 +216,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ len(currseg.Future) > 0 && len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in - let traversedseg := dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) in + let traversedseg := EstablishGuardTraversedsegInc(currseg) in (dp.xover_core2_link_type(hf1, hf2, dp.asid(), currseg.ConsDir) && dp.dp3s_xover_common( s, @@ -256,7 +262,6 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_exit_guard(s IO_dp3s_state_local, 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)) && len(v.IO_Internal_val2_1.CurrSeg.Future) > 0 && - len(v.IO_Internal_val2_2.CurrSeg.Future) > 0 && dp.dp3s_forward_ext(v.IO_Internal_val2_1, v.IO_Internal_val2_2, v.IO_Internal_val2_3) } diff --git a/verification/io/router.gobra b/verification/io/router.gobra index b9d359e1d..1574a73d2 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -97,9 +97,8 @@ ghost requires dp.Valid() decreases pure func (dp DataPlaneSpec) is_target(asid IO_as, nextif IO_ifs, a2 IO_as, i2 IO_ifs) bool { - return asid == dp.GetLocalIA() && - nextif in domain(dp.GetNeighborIAs()) && - dp.Lookup(AsIfsPair{asid, nextif}) == AsIfsPair{a2, i2} + return AsIfsPair{asid, nextif} in domain(dp.GetLinks()) && + dp.Lookup(AsIfsPair{asid, nextif}) == AsIfsPair{a2, i2} } ghost @@ -124,21 +123,19 @@ pure func dp3s_add_obuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO 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]) { - return let newSet := (k in domain(buf)? (let pre := buf[k] in pre union set[IO_pkt3]{v}) : set[IO_pkt3]{v}) in + 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] } ghost requires len(m.CurrSeg.Future) > 0 -requires len(newpkt.CurrSeg.Future) > 0 requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif IO_ifs) bool { return let currseg := m.CurrSeg in let hf1, fut := currseg.Future[0], currseg.Future[1:] in - let traversedseg := dp3s_iospec_bio3s_create_guard_traversedseg_inc(currseg) in + let traversedseg := EstablishGuardTraversedsegInc(currseg) in dp.dp2_forward_ext_guard(dp.asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) && - let hf2 := newpkt.CurrSeg.Future[0] in let a2 := dp.GetNeighborIA(nextif) in let i2 := dp.Lookup(AsIfsPair{dp.asid(), nextif}).ifs in dp.is_target(dp.asid(), nextif, a2, i2) @@ -147,7 +144,6 @@ pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif // TODO: should we change IO_ifs to being implemented as an option type? ghost requires len(m.CurrSeg.Future) > 0 -requires len(newpkt.CurrSeg.Future) > 0 requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif option[IO_ifs]) bool { @@ -161,7 +157,6 @@ pure func (dp DataPlaneSpec) dp3s_forward(m IO_pkt3, newpkt IO_pkt3, nextif opti ghost requires len(intermediatepkt.CurrSeg.Future) > 0 -requires len(newpkt.CurrSeg.Future) > 0 requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_xover_common( From 4c87477ae946f05213221e3204afc417be9fe768 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Tue, 14 Nov 2023 21:38:14 +0100 Subject: [PATCH 14/18] minor improvements --- verification/io/dataplane_abstract.gobra | 6 ++++-- verification/io/io-spec.gobra | 8 ++++---- verification/io/other_defs.gobra | 7 +------ verification/io/router.gobra | 16 ++++------------ 4 files changed, 13 insertions(+), 24 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index 77031aef6..d10f1dc7f 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -52,8 +52,9 @@ pure func (dp DataPlaneSpec) Valid() bool { (forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} AsIfsPair{dp.localIA, ifs} in domain(dp.topology.links) ==> ifs in domain(dp.neighborIAs)) && (forall pairs AsIfsPair :: {dp.Lookup(pairs)} pairs in domain(dp.topology.links) ==> - dp.Lookup(pairs) in domain(dp.topology.links) && - dp.Lookup(dp.Lookup(pairs)) == pairs) + let next_pair := dp.Lookup(pairs) in + (next_pair in domain(dp.topology.links)) && + dp.Lookup(next_pair) == pairs) } ghost @@ -82,6 +83,7 @@ pure func (dp DataPlaneSpec) GetLocalIA() IO_as { return dp.localIA } +// This function corresponds to function 'core' in the IO spec ghost decreases pure func (dp DataPlaneSpec) GetCoreAS() set[IO_as] { diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 32b3917e0..34bdd2914 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -108,7 +108,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local v.IO_Internal_val1_1, currseg, traversedseg, - dp.asid(), + dp.GetLocalIA(), hf1, v.IO_Internal_val1_2, fut) && @@ -162,7 +162,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in let traversedseg := EstablishGuardTraversedsegInc(currseg) in - (dp.xover_up2down2_link_type(dp.asid(), hf1, hf2) && + (dp.xover_up2down2_link_type(dp.GetLocalIA(), hf1, hf2) && dp.dp3s_xover_common( s, v.IO_Internal_val1_1, @@ -204,7 +204,7 @@ requires v.isIO_Internal_val1 requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { - return (dp.asid() in dp.core() && + return (dp.GetLocalIA() in dp.GetCoreAS() && let currseg := v.IO_Internal_val1_1.CurrSeg in match v.IO_Internal_val1_1.LeftSeg { case none[IO_seg2]: @@ -217,7 +217,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in let traversedseg := EstablishGuardTraversedsegInc(currseg) in - (dp.xover_core2_link_type(hf1, hf2, dp.asid(), currseg.ConsDir) && + (dp.xover_core2_link_type(hf1, hf2, dp.GetLocalIA(), currseg.ConsDir) && dp.dp3s_xover_common( s, v.IO_Internal_val1_1, diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index cb1a2861c..f17fe56f1 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -127,12 +127,7 @@ ghost requires dp.Valid() decreases pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{ - return match p1 { - case dp.GetLocalIA(): - p2 in domain(dp.linkTypes) ? dp.linkTypes[p2] : IO_NoLink{} - default: - IO_NoLink{} - } + return p2 in domain(dp.linkTypes) ? dp.linkTypes[p2] : IO_NoLink{} } ghost diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 1574a73d2..2aa38bb73 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -20,14 +20,6 @@ package io // TODO: make individual_router an interface type with the following methods -// This function corresponds to function 'core' in the IO spec -ghost -requires dp.Valid() -decreases -pure func (dp DataPlaneSpec) core() set[IO_as] { - return dp.GetCoreAS() -} - ghost decreases pure func if2term(ifs option[IO_ifs]) IO_msgterm { @@ -51,7 +43,7 @@ pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf if2term(inif), if2term(egif), IO_msgterm(MsgTerm_FS{uinfo})}}) in - x == mac(macKey(asidToKey(dp.asid())), l) + x == mac(macKey(asidToKey(dp.GetLocalIA())), l) } ghost @@ -135,10 +127,10 @@ pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif return let currseg := m.CurrSeg in let hf1, fut := currseg.Future[0], currseg.Future[1:] in let traversedseg := EstablishGuardTraversedsegInc(currseg) in - dp.dp2_forward_ext_guard(dp.asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) && + dp.dp2_forward_ext_guard(dp.GetLocalIA(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) && let a2 := dp.GetNeighborIA(nextif) in - let i2 := dp.Lookup(AsIfsPair{dp.asid(), nextif}).ifs in - dp.is_target(dp.asid(), nextif, a2, i2) + let i2 := dp.Lookup(AsIfsPair{dp.GetLocalIA(), nextif}).ifs in + dp.is_target(dp.GetLocalIA(), nextif, a2, i2) } // TODO: should we change IO_ifs to being implemented as an option type? From 193add2ed959584517953a0664e0b49e15a2dc80 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Tue, 14 Nov 2023 21:41:14 +0100 Subject: [PATCH 15/18] adding missing comment --- verification/io/dataplane_abstract.gobra | 1 + 1 file changed, 1 insertion(+) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index d10f1dc7f..a7d73c800 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -77,6 +77,7 @@ pure func (dp DataPlaneSpec) GetNeighborIA(ifs IO_ifs) IO_as { return dp.neighborIAs[ifs] } +// This function corresponds to function 'asid' in the IO spec ghost decreases pure func (dp DataPlaneSpec) GetLocalIA() IO_as { From 6be6ae61d8a0c2724321abc8bdf11f4dfb9d59c2 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Tue, 14 Nov 2023 22:07:12 +0100 Subject: [PATCH 16/18] renaming core and asid function --- verification/io/dataplane_abstract.gobra | 6 ++---- verification/io/io-spec.gobra | 8 ++++---- verification/io/other_defs.gobra | 2 +- verification/io/router.gobra | 10 +++++----- 4 files changed, 12 insertions(+), 14 deletions(-) diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra index a7d73c800..25b9af797 100644 --- a/verification/io/dataplane_abstract.gobra +++ b/verification/io/dataplane_abstract.gobra @@ -77,17 +77,15 @@ pure func (dp DataPlaneSpec) GetNeighborIA(ifs IO_ifs) IO_as { return dp.neighborIAs[ifs] } -// This function corresponds to function 'asid' in the IO spec ghost decreases -pure func (dp DataPlaneSpec) GetLocalIA() IO_as { +pure func (dp DataPlaneSpec) Asid() IO_as { return dp.localIA } -// This function corresponds to function 'core' in the IO spec ghost decreases -pure func (dp DataPlaneSpec) GetCoreAS() set[IO_as] { +pure func (dp DataPlaneSpec) Core() set[IO_as] { return dp.topology.coreAS } diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 34bdd2914..97cbbdfab 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -108,7 +108,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local v.IO_Internal_val1_1, currseg, traversedseg, - dp.GetLocalIA(), + dp.Asid(), hf1, v.IO_Internal_val1_2, fut) && @@ -162,7 +162,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in let traversedseg := EstablishGuardTraversedsegInc(currseg) in - (dp.xover_up2down2_link_type(dp.GetLocalIA(), hf1, hf2) && + (dp.xover_up2down2_link_type(dp.Asid(), hf1, hf2) && dp.dp3s_xover_common( s, v.IO_Internal_val1_1, @@ -204,7 +204,7 @@ requires v.isIO_Internal_val1 requires dp.Valid() decreases pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v IO_val) bool { - return (dp.GetLocalIA() in dp.GetCoreAS() && + return (dp.Asid() in dp.Core() && let currseg := v.IO_Internal_val1_1.CurrSeg in match v.IO_Internal_val1_1.LeftSeg { case none[IO_seg2]: @@ -217,7 +217,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in let traversedseg := EstablishGuardTraversedsegInc(currseg) in - (dp.xover_core2_link_type(hf1, hf2, dp.GetLocalIA(), currseg.ConsDir) && + (dp.xover_core2_link_type(hf1, hf2, dp.Asid(), currseg.ConsDir) && dp.dp3s_xover_common( s, v.IO_Internal_val1_1, diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index f17fe56f1..b08a2dabe 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -120,7 +120,7 @@ type IO_Link adt { IO_NoLink{} } -// TODO: should be put p1 == dp.GetLocalIA() in the precondition? +// TODO: should be put p1 == dp.Asid() in the precondition? // Should we put dp.Valid() in precondition? // This function is provided as locale in the Isabelle formalization. ghost diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 2aa38bb73..19adb7e91 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -43,7 +43,7 @@ pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf if2term(inif), if2term(egif), IO_msgterm(MsgTerm_FS{uinfo})}}) in - x == mac(macKey(asidToKey(dp.GetLocalIA())), l) + x == mac(macKey(asidToKey(dp.Asid())), l) } ghost @@ -80,7 +80,7 @@ pure func upd_uinfo(segid set[IO_msgterm], hf IO_HF) set[IO_msgterm]{ ghost decreases pure func (dp DataPlaneSpec) asid() IO_as { - return dp.GetLocalIA() + return dp.Asid() } @@ -127,10 +127,10 @@ pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif return let currseg := m.CurrSeg in let hf1, fut := currseg.Future[0], currseg.Future[1:] in let traversedseg := EstablishGuardTraversedsegInc(currseg) in - dp.dp2_forward_ext_guard(dp.GetLocalIA(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) && + dp.dp2_forward_ext_guard(dp.Asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) && let a2 := dp.GetNeighborIA(nextif) in - let i2 := dp.Lookup(AsIfsPair{dp.GetLocalIA(), nextif}).ifs in - dp.is_target(dp.GetLocalIA(), nextif, a2, i2) + let i2 := dp.Lookup(AsIfsPair{dp.Asid(), nextif}).ifs in + dp.is_target(dp.Asid(), nextif, a2, i2) } // TODO: should we change IO_ifs to being implemented as an option type? From 6bf40813b38f29ee2038a7b924336959b449f5d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 15 Nov 2023 16:15:01 +0100 Subject: [PATCH 17/18] Update verification/io/io-spec.gobra --- verification/io/io-spec.gobra | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 97cbbdfab..3df197f08 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -18,9 +18,9 @@ package io -//Unlike the original IO-spec from Isabelle, we need additional information about the network topology. -//To ensure the well-formedness of all map accesses we require an additional conjunction -//for all the events (dp.Valid()) +// Unlike the original IO-spec from Isabelle, we need additional information about the network topology. +// To ensure the well-formedness of all map accesses we require an additional conjunction +// for all the events (dp.Valid()) // This is the main IO Specification. pred (dp DataPlaneSpec) dp3s_iospec_ordered(s IO_dp3s_state_local, t Place) { From 59d30196b6a6ed89b36fccb172d15882cb22888e Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 15 Nov 2023 17:13:04 +0100 Subject: [PATCH 18/18] precondition for link_type function --- verification/io/io-spec.gobra | 16 ++++++++-------- verification/io/other_defs.gobra | 12 ++++++++++-- verification/io/router.gobra | 4 ++-- verification/io/router_events.gobra | 5 +++++ verification/io/xover.gobra | 5 +++++ 5 files changed, 30 insertions(+), 12 deletions(-) diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index 3df197f08..07a8af20d 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -50,11 +50,11 @@ decreases pure func CBio_IN_bio3s_enter_T(t Place, v IO_val) Place /*** Helper functions, not in Isabelle ***/ -//Establishes the traversed segment for packets which are not incremented (internal). +// Establishes the traversed segment for packets which are not incremented (internal). ghost requires len(currseg.Future) > 0 decreases -pure func EstablishGuardTraversedseg(currseg IO_seg3) IO_seg3 { +pure func establishGuardTraversedseg(currseg IO_seg3) IO_seg3 { return let uinfo := !currseg.ConsDir ? upd_uinfo(currseg.UInfo, currseg.Future[0]) : currseg.UInfo in @@ -68,11 +68,11 @@ pure func EstablishGuardTraversedseg(currseg IO_seg3) IO_seg3 { History: currseg.History} } -//Establishes the traversed segment for packets that are incremented (external). +// Establishes the traversed segment for packets that are incremented (external). ghost requires len(currseg.Future) > 0 decreases -pure func EstablishGuardTraversedsegInc(currseg IO_seg3) IO_seg3 { +pure func establishGuardTraversedsegInc(currseg IO_seg3) IO_seg3 { return let uinfo := !currseg.ConsDir ? upd_uinfo(currseg.UInfo, currseg.Future[0]) : currseg.UInfo in @@ -100,9 +100,9 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local let hf1, fut := currseg.Future[0], currseg.Future[1:] in let traversedseg := match v.IO_Internal_val1_4{ case none[IO_ifs]: - EstablishGuardTraversedseg(currseg) + establishGuardTraversedseg(currseg) default: - EstablishGuardTraversedsegInc(currseg) + establishGuardTraversedsegInc(currseg) } in dp.dp2_enter_guard( v.IO_Internal_val1_1, @@ -161,7 +161,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_sta len(currseg.Future) > 0 && len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in - let traversedseg := EstablishGuardTraversedsegInc(currseg) in + let traversedseg := establishGuardTraversedsegInc(currseg) in (dp.xover_up2down2_link_type(dp.Asid(), hf1, hf2) && dp.dp3s_xover_common( s, @@ -216,7 +216,7 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_ len(currseg.Future) > 0 && len(v.IO_Internal_val1_3.CurrSeg.Future) > 0 && let hf1, hf2 := currseg.Future[0], nextseg.Future[0] in - let traversedseg := EstablishGuardTraversedsegInc(currseg) in + let traversedseg := establishGuardTraversedsegInc(currseg) in (dp.xover_core2_link_type(hf1, hf2, dp.Asid(), currseg.ConsDir) && dp.dp3s_xover_common( s, diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra index b08a2dabe..807dd9ee7 100644 --- a/verification/io/other_defs.gobra +++ b/verification/io/other_defs.gobra @@ -120,11 +120,12 @@ type IO_Link adt { IO_NoLink{} } -// TODO: should be put p1 == dp.Asid() in the precondition? -// Should we put dp.Valid() in precondition? // This function is provided as locale in the Isabelle formalization. +// This function is only ever called with p1 == dp.Asid(). As a future optimization +// this parameter and precondition can be dropped. ghost requires dp.Valid() +requires p1 == dp.Asid() decreases pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{ return p2 in domain(dp.linkTypes) ? dp.linkTypes[p2] : IO_NoLink{} @@ -132,6 +133,7 @@ pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{ ghost requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) egif_prov2(hf1 IO_HF, asid IO_as) bool{ return dp.egif2_type(hf1, asid, IO_Link(IO_CustProv{})) @@ -140,6 +142,7 @@ pure func (dp DataPlaneSpec) egif_prov2(hf1 IO_HF, asid IO_as) bool{ ghost requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) egif_core2(hf1 IO_HF, asid IO_as) bool{ return dp.egif2_type(hf1, asid, IO_Link(IO_PeerOrCore{})) @@ -147,6 +150,7 @@ pure func (dp DataPlaneSpec) egif_core2(hf1 IO_HF, asid IO_as) bool{ ghost requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) egif_cust2(hf1 IO_HF, asid IO_as) bool{ return dp.egif2_type(hf1, asid, IO_Link(IO_ProvCust{})) @@ -154,6 +158,7 @@ pure func (dp DataPlaneSpec) egif_cust2(hf1 IO_HF, asid IO_as) bool{ ghost requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) inif_cust2(hf1 IO_HF, asid IO_as) bool{ return dp.inif2_type(hf1, asid, IO_Link(IO_ProvCust{})) @@ -161,6 +166,7 @@ pure func (dp DataPlaneSpec) inif_cust2(hf1 IO_HF, asid IO_as) bool{ ghost requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) inif_core2(hf1 IO_HF, asid IO_as) bool{ return dp.inif2_type(hf1, asid, IO_Link(IO_PeerOrCore{})) @@ -168,6 +174,7 @@ pure func (dp DataPlaneSpec) inif_core2(hf1 IO_HF, asid IO_as) bool{ ghost requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) inif_prov2(hf1 IO_HF, asid IO_as) bool{ return dp.inif2_type(hf1, asid, IO_Link(IO_CustProv{})) @@ -175,6 +182,7 @@ pure func (dp DataPlaneSpec) inif_prov2(hf1 IO_HF, asid IO_as) bool{ ghost requires dp.Valid() +requires ifs != none[IO_ifs] ==> asid == dp.Asid() decreases pure func (dp DataPlaneSpec) if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool{ return match ifs { diff --git a/verification/io/router.gobra b/verification/io/router.gobra index 19adb7e91..6be780804 100644 --- a/verification/io/router.gobra +++ b/verification/io/router.gobra @@ -126,7 +126,7 @@ decreases pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif IO_ifs) bool { return let currseg := m.CurrSeg in let hf1, fut := currseg.Future[0], currseg.Future[1:] in - let traversedseg := EstablishGuardTraversedsegInc(currseg) in + let traversedseg := establishGuardTraversedsegInc(currseg) in dp.dp2_forward_ext_guard(dp.Asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) && let a2 := dp.GetNeighborIA(nextif) in let i2 := dp.Lookup(AsIfsPair{dp.Asid(), nextif}).ifs in @@ -168,6 +168,6 @@ pure func (dp DataPlaneSpec) dp3s_xover_common( // this is because of the way math. maps are implemented, we can only obtain a key that is in the map before. return some(recvif) in domain(s.ibuf) && (let lookupRes := s.ibuf[some(recvif)] in (m in lookupRes)) && - dp.dp2_xover_common_guard(m, currseg, nextseg, traversedseg, intermediatepkt, hf1, hf2, hf1.extr_asid(), recvif) && + dp.dp2_xover_common_guard(m, currseg, nextseg, traversedseg, intermediatepkt, hf1, hf2, dp.Asid(), recvif) && dp.dp3s_forward(intermediatepkt, newpkt, nextif) } diff --git a/verification/io/router_events.gobra b/verification/io/router_events.gobra index d277ad3f2..3159fa1dc 100644 --- a/verification/io/router_events.gobra +++ b/verification/io/router_events.gobra @@ -20,6 +20,7 @@ package io ghost requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs) bool { return d? @@ -30,6 +31,7 @@ pure func (dp DataPlaneSpec) dp2_check_recvif(d bool, asid IO_as, recvif IO_ifs) /* Abbreviations */ ghost requires dp.Valid() +requires a == dp.Asid() decreases 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)) || @@ -39,6 +41,7 @@ pure func (dp DataPlaneSpec) valid_link_types2(hf1 IO_HF, a IO_as) bool { ghost requires dp.Valid() +requires a == dp.Asid() decreases 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)) || @@ -49,6 +52,7 @@ pure func (dp DataPlaneSpec) valid_link_types_in2(hf1 IO_HF, a IO_as) bool { ghost requires dp.Valid() +requires asid == dp.Asid() decreases 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)) || @@ -85,6 +89,7 @@ pure func (dp DataPlaneSpec) 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 requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) dp2_enter_guard(m IO_pkt2, currseg IO_seg2, traversedseg IO_seg2, asid IO_as, hf1 IO_HF, recvif IO_ifs, fut seq[IO_HF]) bool { return m.CurrSeg == currseg && diff --git a/verification/io/xover.gobra b/verification/io/xover.gobra index 80e6ee32c..e9cda55ad 100644 --- a/verification/io/xover.gobra +++ b/verification/io/xover.gobra @@ -36,6 +36,7 @@ package io // the new segment that we are xovering over to. ghost requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2, currseg IO_seg2, @@ -66,6 +67,7 @@ pure func (dp DataPlaneSpec) dp2_xover_common_guard(m IO_pkt2, ghost requires dp.Valid() +requires a == dp.Asid() decreases pure func (dp DataPlaneSpec) egif2_type(hf IO_HF, a IO_as, link IO_Link) bool { return dp.if_type(a, hf.EgIF2, link) @@ -73,6 +75,7 @@ pure func (dp DataPlaneSpec) egif2_type(hf IO_HF, a IO_as, link IO_Link) bool { ghost requires dp.Valid() +requires a == dp.Asid() decreases pure func (dp DataPlaneSpec) inif2_type(hf IO_HF, a IO_as, link IO_Link) bool { return dp.if_type(a, hf.InIF2, link) @@ -80,6 +83,7 @@ pure func (dp DataPlaneSpec) inif2_type(hf IO_HF, a IO_as, link IO_Link) bool { ghost requires dp.Valid() +requires asid == dp.Asid() decreases pure func (dp DataPlaneSpec) xover_up2down2_link_type(asid IO_as, hf1 IO_HF, hf2 IO_HF) bool { return (dp.egif2_type(hf1, asid, IO_ProvCust{}) && dp.egif2_type(hf2, asid, IO_ProvCust{})) || @@ -89,6 +93,7 @@ pure func (dp DataPlaneSpec) xover_up2down2_link_type(asid IO_as, hf1 IO_HF, hf2 ghost requires dp.Valid() +requires asid == dp.Asid() 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{})) ||