Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Concretize all abstract functions in the IO-spec #231

Merged
merged 21 commits into from
Nov 15, 2023
Merged

Concretize all abstract functions in the IO-spec #231

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
6ae29eb
making IO-spec dependend on abstract dataplane
mlimbeck Oct 11, 2023
7fec531
renaming Abs_Dataplane to DataPlaneSpec
mlimbeck Oct 12, 2023
ac31b85
removing local state from IO-spec next place functions
mlimbeck Oct 12, 2023
03ec019
rewriting IO-spec with match clause
mlimbeck Oct 12, 2023
491e444
comment out unnecessary functions
mlimbeck Oct 12, 2023
ed9ade0
providing bodies to abstract functions in IO-spec
mlimbeck Oct 12, 2023
34c58ad
Merge branch 'master' into instantiate-IO-Spec-functions
jcp19 Oct 13, 2023
11ca307
Merge remote-tracking branch 'remotescion/master' into instantiate-IO…
mlimbeck Oct 18, 2023
e4be0b8
merge problems fix
mlimbeck Oct 18, 2023
37c7ac6
cosmetic changes
mlimbeck Oct 18, 2023
a0b37b6
IO-spec fix
mlimbeck Oct 18, 2023
0c2ee68
adding receiving interface to topology
mlimbeck Oct 19, 2023
33cb8d5
concretize dp3s_forward_ext
mlimbeck Nov 1, 2023
d1a45a2
Merge branch 'master' into instantiate-IO-Spec-functions
jcp19 Nov 9, 2023
dc6f540
Apply suggestions from code review
mlimbeck Nov 14, 2023
0203251
minor improvements
mlimbeck Nov 14, 2023
4c87477
minor improvements
mlimbeck Nov 14, 2023
193add2
adding missing comment
mlimbeck Nov 14, 2023
6be6ae6
renaming core and asid function
mlimbeck Nov 14, 2023
6bf4081
Update verification/io/io-spec.gobra
jcp19 Nov 15, 2023
59d3019
precondition for link_type function
mlimbeck Nov 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 41 additions & 10 deletions verification/io/dataplane_abstract.gobra
View file
Open in desktop
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])) &&
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
(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
Open in desktop
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) ==>
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
(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) ==>
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
(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
Loading