Skip to content

Commit c8de95d

Browse files
jcp19jcp19
committed
pr 354, based on 53f8e30 
1 parent 5323351 commit c8de95d

11 files changed

Lines changed: 40 additions & 45 deletions

File tree

‎pkg/slayers/path/path.go‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,11 +14,6 @@
1414

1515
// +gobra
1616

17-
// @ initEnsures PathPackageMem()
18-
// Skipped the following post-condition due to performance reasons
19-
// initEnsures forall t Type :: 0 <= t && t < maxPathType ==> !Registered(t)
20-
// Instead, we have:
21-
// @ initEnsures !Registered(0) && !Registered(1) && !Registered(2) && !Registered(3)
2217
package path
2318

2419
import (

‎verification/io/bios.gobra‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,19 +18,19 @@
1818

1919
package io
2020

21-
type IO_bio3sIN adt {
21+
ghost type IO_bio3sIN adt {
2222
IO_bio3s_enter{}
2323
IO_bio3s_xover{}
2424
IO_bio3s_exit{}
2525
}
2626

27-
type IO_bio3sIO adt {
27+
ghost type IO_bio3sIO adt {
2828
IO_bio3s_send{}
2929
IO_bio3s_recv{}
3030
}
3131

3232
// defined in Isabelle as (bios3sIN, bios3sIO) events
33-
type IO_bio3s adt {
33+
ghost type IO_bio3s adt {
3434
IO_bio3s_IN {
3535
IN IO_bio3sIN
3636
}

‎verification/io/dataplane_abstract.gobra‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ package io
1919
// links: representation of the network topology as a graph.
2020
// `links[(a1,x)] == (a2,y)` means that the interface x of AS a1 is connected
2121
// to the interface y of AS a2.
22-
type DataPlaneSpec adt {
22+
ghost type DataPlaneSpec adt {
2323
DataPlaneSpec_{
2424
linkTypes dict[IO_ifs]IO_Link
2525
neighborIAs dict[IO_ifs]IO_as
@@ -28,7 +28,7 @@ type DataPlaneSpec adt {
2828
}
2929
}
3030

31-
type AsIfsPair struct {
31+
ghost type AsIfsPair ghost struct {
3232
asid IO_as
3333
ifs IO_ifs
3434
}
@@ -37,14 +37,14 @@ ghost
3737
opaque
3838
decreases
3939
pure func (dp DataPlaneSpec) Valid() bool {
40-
return (forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} ifs in domain(dp.neighborIAs) ==>
41-
(AsIfsPair{dp.localIA, ifs} in domain(dp.links) &&
40+
return (forall ifs IO_ifs :: {ifs elem domain(dp.neighborIAs)} ifs elem domain(dp.neighborIAs) ==>
41+
(AsIfsPair{dp.localIA, ifs} elem domain(dp.links) &&
4242
dp.Lookup(AsIfsPair{dp.localIA, ifs}).asid == dp.neighborIAs[ifs])) &&
43-
(forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} AsIfsPair{dp.localIA, ifs} in domain(dp.links) ==>
44-
ifs in domain(dp.neighborIAs)) &&
45-
(forall pairs AsIfsPair :: {dp.Lookup(pairs)} pairs in domain(dp.links) ==>
43+
(forall ifs IO_ifs :: {ifs elem domain(dp.neighborIAs)} AsIfsPair{dp.localIA, ifs} elem domain(dp.links) ==>
44+
ifs elem domain(dp.neighborIAs)) &&
45+
(forall pairs AsIfsPair :: {dp.Lookup(pairs)} pairs elem domain(dp.links) ==>
4646
let next_pair := dp.Lookup(pairs) in
47-
(next_pair in domain(dp.links)) &&
47+
(next_pair elem domain(dp.links)) &&
4848
dp.Lookup(next_pair) == pairs) &&
4949
domain(dp.linkTypes) == domain(dp.neighborIAs)
5050
}
@@ -57,7 +57,7 @@ pure func (dp DataPlaneSpec) GetLinkTypes() dict[IO_ifs]IO_Link {
5757

5858
ghost
5959
decreases
60-
requires ifs in domain(dp.linkTypes)
60+
requires ifs elem domain(dp.linkTypes)
6161
pure func (dp DataPlaneSpec) GetLinkType(ifs IO_ifs) IO_Link {
6262
return dp.linkTypes[ifs]
6363
}
@@ -69,7 +69,7 @@ pure func (dp DataPlaneSpec) GetNeighborIAs() dict[IO_ifs]IO_as {
6969
}
7070

7171
ghost
72-
requires ifs in domain(dp.neighborIAs)
72+
requires ifs elem domain(dp.neighborIAs)
7373
decreases
7474
pure func (dp DataPlaneSpec) GetNeighborIA(ifs IO_ifs) IO_as {
7575
return dp.neighborIAs[ifs]
@@ -88,7 +88,7 @@ pure func (dp DataPlaneSpec) GetLinks() dict[AsIfsPair]AsIfsPair {
8888
}
8989

9090
ghost
91-
requires pair in domain(dp.links)
91+
requires pair elem domain(dp.links)
9292
decreases
9393
pure func(dp DataPlaneSpec) Lookup(pair AsIfsPair) AsIfsPair {
9494
return dp.links[pair]

‎verification/io/hopfields.gobra‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ package io
2121
// Abstract representation of an HopField
2222
// We consider 0 to be the ID of the internal network in HopField.
2323
// We consider None to be the ID of the internal network in HF.
24-
type IO_HF adt {
24+
ghost type IO_HF adt {
2525
IO_HF_ {
2626
InIF2 option[IO_ifs]
2727
EgIF2 option[IO_ifs]

‎verification/io/io-spec.gobra‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -95,8 +95,8 @@ requires v.isIO_Internal_val1
9595
requires dp.Valid()
9696
decreases
9797
pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
98-
return some(v.IO_Internal_val1_2) in domain(s.ibuf) &&
99-
(let ibuf_set := s.ibuf[some(v.IO_Internal_val1_2)] in (v.IO_Internal_val1_1 in ibuf_set)) &&
98+
return some(v.IO_Internal_val1_2) elem domain(s.ibuf) &&
99+
(let ibuf_set := s.ibuf[some(v.IO_Internal_val1_2)] in (v.IO_Internal_val1_1 elem ibuf_set)) &&
100100
len(v.IO_Internal_val1_1.CurrSeg.Future) > 0 &&
101101
let currseg := v.IO_Internal_val1_1.CurrSeg in
102102
let hf1, fut := currseg.Future[0], currseg.Future[1:] in
@@ -219,8 +219,8 @@ requires v.isIO_Internal_val2
219219
requires dp.Valid()
220220
decreases
221221
pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_exit_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
222-
return none[IO_ifs] in domain(s.ibuf) &&
223-
(let ibuf_set := s.ibuf[none[IO_ifs]] in (v.IO_Internal_val2_1 in ibuf_set)) &&
222+
return none[IO_ifs] elem domain(s.ibuf) &&
223+
(let ibuf_set := s.ibuf[none[IO_ifs]] in (v.IO_Internal_val2_1 elem ibuf_set)) &&
224224
len(v.IO_Internal_val2_1.CurrSeg.Future) > 0 &&
225225
dp.dp3s_forward_ext(v.IO_Internal_val2_1, v.IO_Internal_val2_2, v.IO_Internal_val2_3)
226226
}
@@ -261,8 +261,8 @@ requires v.isIO_val_Pkt2
261261
requires dp.Valid()
262262
decreases
263263
pure func (dp DataPlaneSpec) dp3s_iospec_bio3s_send_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
264-
return v.IO_val_Pkt2_1 in domain(s.obuf) &&
265-
(let obuf_set := s.obuf[v.IO_val_Pkt2_1] in (v.IO_val_Pkt2_2 in obuf_set))
264+
return v.IO_val_Pkt2_1 elem domain(s.obuf) &&
265+
(let obuf_set := s.obuf[v.IO_val_Pkt2_1] in (v.IO_val_Pkt2_2 elem obuf_set))
266266
}
267267

268268
pred (dp DataPlaneSpec) dp3s_iospec_bio3s_send(s IO_dp3s_state_local, t Place) {

‎verification/io/other_defs.gobra‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@
1818

1919
package io
2020

21-
type Unit adt {
21+
ghost type Unit adt {
2222
Unit_{}
2323
}
2424

@@ -29,7 +29,7 @@ type IO_ifs uint16
2929
type IO_as uint
3030

3131
// msgTerms consist of terms from our term algebra.
32-
type IO_msgterm adt {
32+
ghost type IO_msgterm adt {
3333
MsgTerm_Empty{}
3434

3535
MsgTerm_AS {
@@ -67,7 +67,7 @@ type IO_msgterm adt {
6767
}
6868
}
6969

70-
type IO_key adt {
70+
ghost type IO_key adt {
7171
Key_macK {
7272
Key_macK_ IO_as
7373
}
@@ -82,7 +82,7 @@ type IO_key adt {
8282
}
8383

8484
// "authenticated hop information"
85-
type IO_ahi adt {
85+
ghost type IO_ahi adt {
8686
IO_ahi_ {
8787
InIF option[IO_ifs]
8888
EgIF option[IO_ifs]
@@ -105,7 +105,7 @@ func (h IO_HF) Toab() IO_ahi {
105105
}
106106

107107
/* Link Types */
108-
type IO_Link adt {
108+
ghost type IO_Link adt {
109109
IO_CustProv{}
110110
IO_ProvCust{}
111111
IO_Core{}
@@ -120,7 +120,7 @@ requires dp.Valid()
120120
requires p1 == dp.Asid()
121121
decreases
122122
pure func (dp DataPlaneSpec) link_type(p1 IO_as, p2 IO_ifs) IO_Link{
123-
return p2 in domain(dp.GetLinkTypes()) ? dp.GetLinkType(p2) : IO_NoLink{}
123+
return p2 elem domain(dp.GetLinkTypes()) ? dp.GetLinkType(p2) : IO_NoLink{}
124124
}
125125

126126
ghost
@@ -192,7 +192,7 @@ type ext2_rec struct {
192192
op4 IO_as
193193
}
194194

195-
type IO_dp2_state adt {
195+
ghost type IO_dp2_state adt {
196196
IO_dp2_state_ {
197197
// In the Isabelle spec, the following are functions
198198
// instead of mathematical maps

‎verification/io/packets.gobra‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919
package io
2020

2121
// pkt2
22-
type IO_pkt2 adt {
22+
ghost type IO_pkt2 adt {
2323
// Here, we already instantiated the type params
2424
IO_Packet2 {
2525
CurrSeg IO_seg3
@@ -30,4 +30,4 @@ type IO_pkt2 adt {
3030
}
3131

3232
// pkt3 is the same as pkt2 instantiated with type parameters
33-
type IO_pkt3 = IO_pkt2
33+
ghost type IO_pkt3 = IO_pkt2

‎verification/io/router.gobra‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ ghost
8989
requires dp.Valid()
9090
decreases
9191
pure func (dp DataPlaneSpec) is_target(asid IO_as, nextif IO_ifs, a2 IO_as, i2 IO_ifs) bool {
92-
return AsIfsPair{asid, nextif} in domain(dp.GetLinks()) &&
92+
return AsIfsPair{asid, nextif} elem domain(dp.GetLinks()) &&
9393
dp.Lookup(AsIfsPair{asid, nextif}) == AsIfsPair{a2, i2}
9494
}
9595

@@ -115,7 +115,7 @@ pure func dp3s_add_obuf(s IO_dp3s_state_local, i option[IO_ifs], pkt IO_pkt3) IO
115115
ghost
116116
decreases
117117
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]) {
118-
return let newSet := (k in domain(buf) ? (let pre := buf[k] in pre union set[IO_pkt3]{v}) : set[IO_pkt3]{v}) in
118+
return let newSet := (k elem domain(buf) ? (let pre := buf[k] in pre union set[IO_pkt3]{v}) : set[IO_pkt3]{v}) in
119119
buf[k = newSet]
120120
}
121121

@@ -129,7 +129,7 @@ pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif
129129
let hf1, fut := currseg.Future[0], currseg.Future[1:] in
130130
let traversedseg := newpkt.CurrSeg in
131131
dp.dp2_forward_ext_guard(dp.Asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) &&
132-
(nextif in domain(dp.GetNeighborIAs())) &&
132+
(nextif elem domain(dp.GetNeighborIAs())) &&
133133
let a2 := dp.GetNeighborIA(nextif) in
134134
let i2 := dp.Lookup(AsIfsPair{dp.Asid(), nextif}).ifs in
135135
dp.is_target(dp.Asid(), nextif, a2, i2)
@@ -145,7 +145,7 @@ pure func (dp DataPlaneSpec) dp3s_forward_ext_xover(m IO_pkt3, newpkt IO_pkt3, n
145145
let hf1, fut := currseg.Future[0], currseg.Future[1:] in
146146
let traversedseg := newpkt.CurrSeg in
147147
dp.dp2_forward_ext_guard(dp.Asid(), m, nextif, currseg, traversedseg, newpkt, fut, hf1) &&
148-
(nextif in domain(dp.GetNeighborIAs())) &&
148+
(nextif elem domain(dp.GetNeighborIAs())) &&
149149
let a2 := dp.GetNeighborIA(nextif) in
150150
let i2 := dp.Lookup(AsIfsPair{dp.Asid(), nextif}).ifs in
151151
dp.is_target(dp.Asid(), nextif, a2, i2)
@@ -199,8 +199,8 @@ pure func (dp DataPlaneSpec) dp3s_xover_guard(
199199
) bool {
200200
// the first conjunct was added to Gobra, even though it was not in the original isabelle spec.
201201
// this is because of the way math. maps are implemented, we can only obtain a key that is in the map before.
202-
return some(recvif) in domain(s.ibuf) &&
203-
(let lookupRes := s.ibuf[some(recvif)] in (m in lookupRes)) &&
202+
return some(recvif) elem domain(s.ibuf) &&
203+
(let lookupRes := s.ibuf[some(recvif)] in (m elem lookupRes)) &&
204204
dp.dp2_xover_guard(m, currseg, nextseg, traversedseg, intermediatepkt, hf1, hf2, nextfut, dp.Asid(), recvif) &&
205205
dp.dp3s_forward_xover(intermediatepkt, newpkt, nextif)
206206
}

‎verification/io/router_state.gobra‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@
1818

1919
package io
2020

21-
type IO_dp3s_state_local adt {
21+
ghost type IO_dp3s_state_local adt {
2222
IO_dp3s_state_local_ {
2323
ibuf dict[option[IO_ifs]](set[IO_pkt3])
2424
obuf dict[option[IO_ifs]](set[IO_pkt3])

‎verification/io/segments.gobra‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ package io
2020

2121
type IO_ainfo = uint
2222

23-
type IO_seg2 adt {
23+
ghost type IO_seg2 adt {
2424
// Here, we already instantiated the type params
2525
IO_seg3_ {
2626
AInfo IO_ainfo // nat in Isabelle
@@ -34,4 +34,4 @@ type IO_seg2 adt {
3434
}
3535

3636
// seg3 is the same as seg2 instantiated with type parameters
37-
type IO_seg3 = IO_seg2
37+
ghost type IO_seg3 = IO_seg2

0 commit comments

Comments
 (0)