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.

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

Concretize all abstract functions in the IO-spec #231

Merged
merged 21 commits into from
Nov 15, 2023
Merged
Changes from 1 commit
Commits
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
Prev Previous commit
Next Next commit
renaming Abs_Dataplane to DataPlaneSpec
mlimbeck committed Oct 12, 2023
commit 7fec5312c7120c223ffee4c2203bdd5ca7289140
40 changes: 16 additions & 24 deletions verification/io/dataplane_abstract.gobra
Original file line number Diff line number Diff line change
@@ -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
}
18 changes: 9 additions & 9 deletions verification/io/other_defs.gobra
Original file line number Diff line number Diff line change
@@ -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
30 changes: 17 additions & 13 deletions verification/io/router.gobra
Original file line number Diff line number Diff line change
@@ -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,29 +68,33 @@ 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]
}

// 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))
}

// 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,
14 changes: 7 additions & 7 deletions verification/io/router_events.gobra
Original file line number Diff line number Diff line change
@@ -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,15 +29,15 @@ 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))
}

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) &&
12 changes: 6 additions & 6 deletions verification/io/segment-defs.gobra
Original file line number Diff line number Diff line change
@@ -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,33 +32,33 @@ 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
}

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
12 changes: 6 additions & 6 deletions verification/io/xover.gobra
Original file line number Diff line number Diff line change
@@ -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{}))
}