Skip to content

Commit

Permalink
Concretize all abstract functions in the IO-spec (#231)
Browse files Browse the repository at this point in the history 
* making IO-spec dependend on abstract dataplane

* renaming Abs_Dataplane to DataPlaneSpec

* removing local state from IO-spec next place functions

* rewriting IO-spec with match clause

* comment out unnecessary functions

* providing bodies to abstract functions in IO-spec

* merge problems fix

* cosmetic changes

* IO-spec fix

* adding receiving interface to topology

* concretize dp3s_forward_ext

* Apply suggestions from code review

Co-authored-by: João Pereira <[email protected]>

* minor improvements

* minor improvements

* adding missing comment

* renaming core and asid function

* Update verification/io/io-spec.gobra

* precondition for link_type function

---------

Co-authored-by: João Pereira <[email protected]>
  • Loading branch information
@mlimbeck @jcp19
mlimbeck and jcp19 authored Nov 15, 2023
1 parent fee6345 commit c0b039e
Show file tree
Hide file tree
Showing 7 changed files with 273 additions and 102 deletions.
51 changes: 41 additions & 10 deletions verification/io/dataplane_abstract.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,24 +25,36 @@ 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][1] == a2 means that AS a1 has an edge to AS a2 via interface 1.
// `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]
links dict[IO_as](dict[IO_ifs]IO_as)
links dict[AsIfsPair]AsIfsPair
}
}

type AsIfsPair struct {
asid IO_as
ifs IO_ifs
}

ghost
decreases
pure func (dp DataPlaneSpec) Valid() bool{
return domain(dp.linkTypes) == domain(dp.neighborIAs) &&
dp.localIA in domain(dp.topology.links) &&
dp.neighborIAs == dp.topology.links[dp.localIA] &&
(forall core IO_as :: {core in dp.topology.coreAS} core in dp.topology.coreAS ==> core in domain(dp.topology.links))
pure func (dp DataPlaneSpec) Valid() bool {
return domain(dp.linkTypes) == domain(dp.neighborIAs) &&
(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) ==>
let next_pair := dp.Lookup(pairs) in
(next_pair in domain(dp.topology.links)) &&
dp.Lookup(next_pair) == pairs)
}

ghost
Expand All @@ -52,6 +64,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
Expand All @@ -61,12 +79,25 @@ pure func (dp DataPlaneSpec) GetNeighborIA(ifs IO_ifs) IO_as {

ghost
decreases
pure func (dp DataPlaneSpec) GetLocalIA() IO_as {
pure func (dp DataPlaneSpec) Asid() IO_as {
return dp.localIA
}

ghost
decreases
pure func (dp DataPlaneSpec) GetCoreAS() set[IO_as] {
pure func (dp DataPlaneSpec) Core() set[IO_as] {
return dp.topology.coreAS
}

ghost
decreases
pure func (dp DataPlaneSpec) GetLinks() dict[AsIfsPair]AsIfsPair {
return dp.topology.links
}

ghost
requires pair in domain(dp.topology.links)
decreases
pure func(dp DataPlaneSpec) Lookup(pair AsIfsPair) AsIfsPair {
return dp.topology.links[pair]
}
99 changes: 68 additions & 31 deletions verification/io/io-spec.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) &&
Expand Down Expand Up @@ -45,13 +49,14 @@ 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 (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg(currseg IO_seg3) IO_seg3 {
pure func establishGuardTraversedseg(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,
Expand All @@ -63,22 +68,47 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_create_guard_traversedseg(currseg
History: currseg.History}
}

// 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 {
return let uinfo := !currseg.ConsDir ?
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}
}
/*** End of helper functions, not in Isabelle ***/

// 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) ==>
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 := dp.dp3s_iospec_bio3s_create_guard_traversedseg(currseg) in
let traversedseg := match v.IO_Internal_val1_4{
case none[IO_ifs]:
establishGuardTraversedseg(currseg)
default:
establishGuardTraversedsegInc(currseg)
} in
dp.dp2_enter_guard(
v.IO_Internal_val1_1,
currseg,
traversedseg,
dp.asid(),
dp.Asid(),
hf1,
v.IO_Internal_val1_2,
fut) &&
Expand All @@ -98,12 +128,13 @@ 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(
dp.dp3s_add_obuf(s, nextif, newpkt),
dp3s_add_obuf(s, nextif, newpkt),
CBio_IN_bio3s_enter_T(t, v))))
default: true
default:
true
})
}

Expand All @@ -116,6 +147,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
Expand All @@ -127,9 +159,10 @@ 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(currseg) in
(dp.xover_up2down2_link_type(dp.asid(), hf1, hf2) &&
let traversedseg := establishGuardTraversedsegInc(currseg) in
(dp.xover_up2down2_link_type(dp.Asid(), hf1, hf2) &&
dp.dp3s_xover_common(
s,
v.IO_Internal_val1_1,
Expand All @@ -146,14 +179,14 @@ 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) }{ 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) ==>
(dp.Valid() && 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(
dp3s_add_obuf(s, nextif, newpkt),
dp3s_iospec_bio3s_xover_up2down_T(t, v))))
default:
true
})
Expand All @@ -167,10 +200,11 @@ 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
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.Asid() in dp.Core() &&
let currseg := v.IO_Internal_val1_1.CurrSeg in
match v.IO_Internal_val1_1.LeftSeg {
case none[IO_seg2]:
Expand All @@ -180,9 +214,10 @@ 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
(dp.xover_core2_link_type(hf1, hf2, dp.asid(), currseg.ConsDir) &&
let traversedseg := establishGuardTraversedsegInc(currseg) in
(dp.xover_core2_link_type(hf1, hf2, dp.Asid(), currseg.ConsDir) &&
dp.dp3s_xover_common(
s,
v.IO_Internal_val1_1,
Expand All @@ -199,20 +234,19 @@ pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_
}

pred (dp DataPlaneSpec) dp3s_iospec_bio3s_xover_core(s IO_dp3s_state_local, t Place) {
forall v IO_val :: { dp.dp3s_iospec_bio3s_xover_core_guard(s, t, v) }{ CBio_IN_bio3s_xover_core(t, v) }{ dp.dp3s_iospec_ordered(dp.dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3), dp3s_iospec_bio3s_xover_core_T(t, v)) } (
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(
dp.dp3s_add_obuf(s, nextif, newpkt),
dp3s_add_obuf(s, nextif, newpkt),
dp3s_iospec_bio3s_xover_core_T(t, v))))
default:
true
})
}


pred CBio_IN_bio3s_exit(t Place, v IO_val)

ghost
Expand All @@ -222,21 +256,23 @@ 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) ==>
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 &&
dp.dp3s_forward_ext(v.IO_Internal_val2_1, v.IO_Internal_val2_2, v.IO_Internal_val2_3)
}

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) ==>
(dp.Valid() && 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
Expand All @@ -253,9 +289,10 @@ 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) ==>
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))
}

Expand All @@ -264,7 +301,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{_, _}:
Expand All @@ -290,7 +327,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:
Expand Down
Loading

0 comments on commit c0b039e

Please sign in to comment.