Skip to content

Commit 7c601b1

Browse files
author
aaronbojarski
committed
Merge branch 'master' into upstream
2 parents 9a633c3 + 74d17fd commit 7c601b1

21 files changed

+167
-163
lines changed

‎pkg/slayers/path/hopfield_spec.gobra‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -31,13 +31,13 @@ pred (h *HopField) Mem() {
3131
ghost
3232
decreases
3333
pure func ifsToIO_ifs(ifs uint16) option[io.IO_ifs] {
34-
return ifs == 0 ? none[io.IO_ifs] : some(io.IO_ifs(ifs))
34+
return ifs == 0 ? none[io.IO_ifs] : some(io.IO_ifs{ifs})
3535
}
3636

3737
ghost
3838
decreases
3939
pure func IO_ifsToIfs(ifs option[io.IO_ifs]) uint16 {
40-
return ifs == none[io.IO_ifs] ? 0 : uint16(get(ifs))
40+
return ifs == none[io.IO_ifs] ? 0 : uint16(get(ifs).V)
4141
}
4242

4343
ghost
@@ -54,7 +54,7 @@ pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) {
5454
let egif2 := binary.BigEndian.Uint16(raw[middle+4:middle+6]) in
5555
let op_inif2 := ifsToIO_ifs(inif2) in
5656
let op_egif2 := ifsToIO_ifs(egif2) in
57-
io.IO_HF_ {
57+
io.IO_HF {
5858
InIF2: op_inif2,
5959
EgIF2: op_egif2,
6060
HVF: AbsMac(FromSliceToMacArray(raw[middle+6:middle+6+MacLen])),
@@ -109,7 +109,7 @@ func BytesToAbsHopFieldOffsetEq(raw [] byte, offset int) {
109109
ghost
110110
decreases
111111
pure func (h HopField) ToIO_HF() (io.IO_HF) {
112-
return io.IO_HF_ {
112+
return io.IO_HF {
113113
InIF2: ifsToIO_ifs(h.ConsIngress),
114114
EgIF2: ifsToIO_ifs(h.ConsEgress),
115115
HVF: AbsMac(h.Mac),

‎pkg/slayers/path/infofield_spec.gobra‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ pure func Timestamp(raw []byte, currINF int, headerOffset int) io.IO_ainfo {
5858
return let idx := InfoFieldOffset(currINF, headerOffset)+4 in
5959
unfolding sl.Bytes(raw, 0, len(raw)) in
6060
let _ := sl.AssertSliceOverlap(raw, idx, idx+4) in
61-
io.IO_ainfo(binary.BigEndian.Uint32(raw[idx:idx+4]))
61+
io.IO_ainfo{uint(binary.BigEndian.Uint32(raw[idx:idx+4]))}
6262
}
6363

6464
ghost
@@ -93,8 +93,8 @@ decreases
9393
pure func BytesToAbsInfoFieldHelper(raw [] byte, middle int) (io.AbsInfoField) {
9494
return let _ := sl.AssertSliceOverlap(raw, middle+2, middle+4) in
9595
let _ := sl.AssertSliceOverlap(raw, middle+4, middle+8) in
96-
io.AbsInfoField_{
97-
AInfo: io.IO_ainfo(binary.BigEndian.Uint32(raw[middle+4:middle+8])),
96+
io.AbsInfoField {
97+
AInfo: io.IO_ainfo{uint(binary.BigEndian.Uint32(raw[middle+4:middle+8]))},
9898
UInfo: AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[middle+2:middle+4])),
9999
ConsDir: raw[middle] & 0x1 == 0x1,
100100
Peer: raw[middle] & 0x2 == 0x2,
@@ -133,8 +133,8 @@ func BytesToAbsInfoFieldOffsetEq(raw [] byte, middle int) {
133133
ghost
134134
decreases
135135
pure func (inf InfoField) ToAbsInfoField() (io.AbsInfoField) {
136-
return io.AbsInfoField_{
137-
AInfo: io.IO_ainfo(inf.Timestamp),
136+
return io.AbsInfoField {
137+
AInfo: io.IO_ainfo{uint(inf.Timestamp)},
138138
UInfo: AbsUInfoFromUint16(inf.SegID),
139139
ConsDir: inf.ConsDir,
140140
Peer: inf.Peer,

‎pkg/slayers/path/scion/raw_spec.gobra‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -270,7 +270,7 @@ pure func segment(raw []byte,
270270
peer bool,
271271
segLen int) (res io.IO_seg2) {
272272
return let hopfields := hopFields(raw, offset, 0, segLen) in
273-
io.IO_seg3_ {
273+
io.IO_seg3 {
274274
AInfo: ainfo,
275275
UInfo: uinfo,
276276
ConsDir: consDir,
@@ -389,7 +389,7 @@ pure func (s *Raw) absPkt(raw []byte) (res io.IO_pkt2) {
389389
let prevSegLen := segs.LengthOfPrevSeg(currHfIdx) in
390390
let numINF := segs.NumInfoFields() in
391391
let offset := HopFieldOffset(numINF, prevSegLen, MetaLen) in
392-
io.IO_Packet2 {
392+
io.IO_pkt2 {
393393
CurrSeg: CurrSeg(raw, offset, currInfIdx, currHfIdx - prevSegLen, segLen, MetaLen),
394394
LeftSeg: LeftSeg(raw, currInfIdx + 1, segs, MetaLen),
395395
MidSeg: MidSeg(raw, currInfIdx + 2, segs, MetaLen),
@@ -487,7 +487,7 @@ requires oldPkt.LeftSeg != none[io.IO_seg2]
487487
requires oldPkt.PathNotFullyTraversed()
488488
decreases
489489
pure func AbsXover(oldPkt io.IO_pkt2) (newPkt io.IO_pkt2) {
490-
return io.IO_Packet2 {
490+
return io.IO_pkt2 {
491491
get(oldPkt.LeftSeg),
492492
oldPkt.MidSeg,
493493
oldPkt.RightSeg,
@@ -499,7 +499,7 @@ ghost
499499
requires oldPkt.PathNotFullyTraversed()
500500
decreases
501501
pure func AbsIncPath(oldPkt io.IO_pkt2) (newPkt io.IO_pkt2) {
502-
return io.IO_Packet2 {
502+
return io.IO_pkt2 {
503503
absIncPathSeg(oldPkt.CurrSeg),
504504
oldPkt.LeftSeg,
505505
oldPkt.MidSeg,
@@ -511,7 +511,7 @@ ghost
511511
requires len(currseg.Future) > 0
512512
decreases
513513
pure func absIncPathSeg(currseg io.IO_seg3) io.IO_seg3 {
514-
return io.IO_seg3_ {
514+
return io.IO_seg3 {
515515
AInfo: currseg.AInfo,
516516
UInfo: currseg.UInfo,
517517
ConsDir: currseg.ConsDir,

‎router/dataplane_concurrency_model.gobra‎

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -21,12 +21,11 @@ import (
2121
io "verification/io"
2222
)
2323

24-
// Never use `==` for comparisons! Because this is a ghost structure, only the ghost comparison (`===`)
25-
// is meaningful.
26-
type SharedArg struct {
27-
ghost Place gpointer[io.Place] // Existential for the current place
28-
ghost State gpointer[io.IO_dp3s_state_local] // Existential for the current model state
29-
ghost IBufY, OBufY ElemRA // Parameters of the algebra
24+
ghost type SharedArg ghost struct {
25+
Place gpointer[io.Place] // Existential for the current place
26+
State gpointer[io.IO_dp3s_state_local] // Existential for the current model state
27+
IBufY ElemRA // Parameter of the algebra
28+
OBufY ElemRA // Parameter of the algebra
3029
}
3130

3231
pred SharedInv(ghost dp io.DataPlaneSpec, ghost y SharedArg) {
@@ -246,11 +245,11 @@ func multiElemWitnessConvAux(y ElemRA, k Key, es seq[io.IO_val], i int) {
246245
/**** End of MultiElemWitness helper functions ****/
247246

248247
/////////////////////////////////////// RA definitions ///////////////////////////////////////
249-
type Key = option[io.IO_ifs]
250-
type Val = set[io.IO_pkt3]
251-
type Elem = io.IO_pkt3
248+
ghost type Key = option[io.IO_ifs]
249+
ghost type Val = set[io.IO_pkt3]
250+
ghost type Elem = io.IO_pkt3
252251

253-
type ElemRA domain{}
252+
ghost type ElemRA domain{}
254253

255254
pred ElemAuth(ghost m dict[Key]Val, ghost y ElemRA)
256255

‎router/dataplane_spec_test.gobra‎

Lines changed: 45 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -93,8 +93,8 @@ func testRun(
9393
key *[]byte,
9494
metrics *Metrics,
9595
ctx context.Context,
96-
place io.Place,
97-
state io.IO_dp3s_state_local) (d *DataPlane) {
96+
ghost place io.Place,
97+
ghost state io.IO_dp3s_state_local) (d *DataPlane) {
9898
// body similar to foldDataPlaneMem
9999
d = &DataPlane{}
100100

@@ -137,43 +137,46 @@ func testRun(
137137
fold accForwardingMetrics(d.forwardingMetrics)
138138

139139
ensures dp.Valid()
140-
ensures dp === io.DataPlaneSpec_ {
140+
// the following trivial assertion makes sure that `==` matches
141+
// `===` for ghost structs
142+
ensures dp != io.DataPlaneSpec{}
143+
ensures dp == io.DataPlaneSpec {
141144
linkTypes: dict[io.IO_ifs]io.IO_Link{
142-
1: io.IO_ProvCust{},
143-
2: io.IO_ProvCust{},
144-
3: io.IO_ProvCust{},
145+
io.IO_ifs{1}: io.IO_ProvCust{},
146+
io.IO_ifs{2}: io.IO_ProvCust{},
147+
io.IO_ifs{3}: io.IO_ProvCust{},
145148
},
146149
neighborIAs: dict[io.IO_ifs]io.IO_as{
147-
1: 1001,
148-
2: 1002,
149-
3: 1000,
150+
io.IO_ifs{1}: io.IO_as{1001},
151+
io.IO_ifs{2}: io.IO_as{1002},
152+
io.IO_ifs{3}: io.IO_as{1000},
150153
},
151-
localIA: 1000,
154+
localIA: io.IO_as{1000},
152155
links: dict[io.AsIfsPair]io.AsIfsPair {
153-
io.AsIfsPair{1000, 1}: io.AsIfsPair{1001, 7},
154-
io.AsIfsPair{1000, 2}: io.AsIfsPair{1002, 8},
155-
io.AsIfsPair{1000, 3}: io.AsIfsPair{1000, 3},
156-
io.AsIfsPair{1001, 7}: io.AsIfsPair{1000, 1},
157-
io.AsIfsPair{1002, 8}: io.AsIfsPair{1000, 2}}}
156+
io.AsIfsPair{io.IO_as{1000}, io.IO_ifs{1}}: io.AsIfsPair{io.IO_as{1001}, io.IO_ifs{7}},
157+
io.AsIfsPair{io.IO_as{1000}, io.IO_ifs{2}}: io.AsIfsPair{io.IO_as{1002}, io.IO_ifs{8}},
158+
io.AsIfsPair{io.IO_as{1000}, io.IO_ifs{3}}: io.AsIfsPair{io.IO_as{1000}, io.IO_ifs{3}},
159+
io.AsIfsPair{io.IO_as{1001}, io.IO_ifs{7}}: io.AsIfsPair{io.IO_as{1000}, io.IO_ifs{1}},
160+
io.AsIfsPair{io.IO_as{1002}, io.IO_ifs{8}}: io.AsIfsPair{io.IO_as{1000}, io.IO_ifs{2}}}}
158161
outline(
159-
pair1 := io.AsIfsPair{1000, 1}
160-
pair2 := io.AsIfsPair{1000, 2}
161-
pair3 := io.AsIfsPair{1000, 3}
162-
pair4 := io.AsIfsPair{1001, 7}
163-
pair5 := io.AsIfsPair{1002, 8}
162+
pair1 := io.AsIfsPair{io.IO_as{1000}, io.IO_ifs{1}}
163+
pair2 := io.AsIfsPair{io.IO_as{1000}, io.IO_ifs{2}}
164+
pair3 := io.AsIfsPair{io.IO_as{1000}, io.IO_ifs{3}}
165+
pair4 := io.AsIfsPair{io.IO_as{1001}, io.IO_ifs{7}}
166+
pair5 := io.AsIfsPair{io.IO_as{1002}, io.IO_ifs{8}}
164167

165-
dp := io.DataPlaneSpec_ {
168+
dp := io.DataPlaneSpec {
166169
linkTypes: dict[io.IO_ifs]io.IO_Link{
167-
1: io.IO_ProvCust{},
168-
2: io.IO_ProvCust{},
169-
3: io.IO_ProvCust{},
170+
io.IO_ifs{1}: io.IO_ProvCust{},
171+
io.IO_ifs{2}: io.IO_ProvCust{},
172+
io.IO_ifs{3}: io.IO_ProvCust{},
170173
},
171174
neighborIAs: dict[io.IO_ifs]io.IO_as{
172-
1: 1001,
173-
2: 1002,
174-
3: 1000,
175+
io.IO_ifs{1}: io.IO_as{1001},
176+
io.IO_ifs{2}: io.IO_as{1002},
177+
io.IO_ifs{3}: io.IO_as{1000},
175178
},
176-
localIA: 1000,
179+
localIA: io.IO_as{1000},
177180
links: dict[io.AsIfsPair]io.AsIfsPair {
178181
pair1: pair4,
179182
pair2: pair5,
@@ -201,7 +204,7 @@ func testRun(
201204
assert reveal dp.Valid()
202205
)
203206

204-
assert dp.Asid() == 1000
207+
assert dp.Asid().V == 1000
205208
assert d.localIA == 1000
206209
assert d.dpSpecWellConfiguredLocalIA(dp)
207210
assert d.dpSpecWellConfiguredNeighborIAs(dp)
@@ -238,3 +241,16 @@ func allocateBatchConn() (b BatchConn)
238241

239242
ensures u != nil && u.Mem()
240243
func allocateUDPAddr() (u *net.UDPAddr)
244+
245+
// the following trivial assertion makes sure that `==` matches
246+
// `===` for ghost structs
247+
func testEquals() {
248+
assert forall d1 io.DataPlaneSpec, d2 io.DataPlaneSpec :: { dummyTrigger(d1), dummyTrigger(d2) } (d1 == d2) == (d1 === d2)
249+
}
250+
251+
ghost
252+
pure
253+
decreases
254+
func dummyTrigger(d io.DataPlaneSpec) bool {
255+
return true
256+
}

‎router/io-spec-abstract-transitions.gobra‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ ensures newPkt.PathNotFullyTraversed()
4141
ensures len(newPkt.CurrSeg.Future) == len(oldPkt.CurrSeg.Future)
4242
decreases
4343
pure func AbsUpdateNonConsDirIngressSegID(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs]) (newPkt io.IO_pkt2) {
44-
return ingressID == none[io.IO_ifs] ? oldPkt : io.IO_Packet2 {
44+
return ingressID == none[io.IO_ifs] ? oldPkt : io.IO_pkt2 {
4545
io.establishGuardTraversedseg(oldPkt.CurrSeg, !oldPkt.CurrSeg.ConsDir),
4646
oldPkt.LeftSeg,
4747
oldPkt.MidSeg,
@@ -95,7 +95,7 @@ requires oldPkt.PathNotFullyTraversed()
9595
ensures len(newPkt.CurrSeg.Future) >= 0
9696
decreases
9797
pure func AbsProcessEgress(oldPkt io.IO_pkt2) (newPkt io.IO_pkt2) {
98-
return io.IO_Packet2 {
98+
return io.IO_pkt2 {
9999
io.establishGuardTraversedsegInc(oldPkt.CurrSeg, oldPkt.CurrSeg.ConsDir),
100100
oldPkt.LeftSeg,
101101
oldPkt.MidSeg,
@@ -114,7 +114,7 @@ ensures newPkt.RightSeg != none[io.IO_seg2]
114114
ensures len(get(newPkt.RightSeg).Past) > 0
115115
decreases
116116
pure func AbsDoXover(oldPkt io.IO_pkt2) (newPkt io.IO_pkt2) {
117-
return io.IO_Packet2 {
117+
return io.IO_pkt2 {
118118
get(oldPkt.LeftSeg),
119119
oldPkt.MidSeg,
120120
oldPkt.RightSeg,
@@ -146,8 +146,9 @@ pure func AbsVerifyCurrentMACConstraint(pkt io.IO_pkt2, dp io.DataPlaneSpec) boo
146146
let ts := currseg.AInfo in
147147
let hf := currseg.Future[0] in
148148
let uinfo := currseg.UInfo in
149-
dp.hf_valid(d, ts, uinfo, hf)
149+
dp.hf_valid(d, ts.V, uinfo, hf)
150150
}
151+
151152
// This executes the IO enter event whenever a pkt was received
152153
// from a different AS (ingressID != none[io.IO_ifs])
153154
// and will be forwarded to another border router within the AS (egressID == none[io.IO_ifs])

‎router/io-spec-atomic-events.gobra‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ requires dp.dp2_enter_guard(
4343
get(ingressID),
4444
oldPkt.CurrSeg.Future[1:])
4545
requires dp.dp3s_forward(
46-
io.IO_Packet2 {
46+
io.IO_pkt2 {
4747
io.establishGuardTraversedseg(oldPkt.CurrSeg, !oldPkt.CurrSeg.ConsDir),
4848
oldPkt.LeftSeg,
4949
oldPkt.MidSeg,
@@ -116,7 +116,7 @@ requires dp.dp2_xover_guard(
116116
oldPkt.CurrSeg,
117117
get(oldPkt.LeftSeg),
118118
io.establishGuardTraversedsegInc(oldPkt.CurrSeg, !oldPkt.CurrSeg.ConsDir),
119-
io.IO_Packet2 {
119+
io.IO_pkt2 {
120120
get(oldPkt.LeftSeg),
121121
oldPkt.MidSeg,
122122
oldPkt.RightSeg,
@@ -128,7 +128,7 @@ requires dp.dp2_xover_guard(
128128
dp.Asid(),
129129
get(ingressID))
130130
requires dp.dp3s_forward_xover(
131-
io.IO_Packet2 {
131+
io.IO_pkt2 {
132132
get(oldPkt.LeftSeg),
133133
oldPkt.MidSeg,
134134
oldPkt.RightSeg,

‎router/io-spec.gobra‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ pure func absPkt(raw []byte) (res io.IO_pkt2) {
5252
let prevSegLen := segs.LengthOfPrevSeg(currHfIdx) in
5353
let numINF := segs.NumInfoFields() in
5454
let offset := scion.HopFieldOffset(numINF, prevSegLen, headerOffsetWithMetaLen) in
55-
io.IO_Packet2 {
55+
io.IO_pkt2 {
5656
CurrSeg: scion.CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen),
5757
LeftSeg: scion.LeftSeg(raw, currInfIdx + 1, segs, headerOffsetWithMetaLen),
5858
MidSeg: scion.MidSeg(raw, currInfIdx + 2, segs, headerOffsetWithMetaLen),
@@ -106,7 +106,7 @@ ghost
106106
requires acc(&d.localIA)
107107
decreases
108108
pure func (d *DataPlane) dpSpecWellConfiguredLocalIA(dp io.DataPlaneSpec) bool {
109-
return io.IO_as(d.localIA) == dp.Asid()
109+
return io.IO_as{uint(d.localIA)} == dp.Asid()
110110
}
111111

112112
ghost
@@ -115,8 +115,8 @@ requires d.neighborIAs != nil ==> acc(d.neighborIAs)
115115
decreases
116116
pure func (d *DataPlane) dpSpecWellConfiguredNeighborIAs(dp io.DataPlaneSpec) bool {
117117
return forall ifs uint16 :: {ifs in domain(d.neighborIAs)} ifs in domain(d.neighborIAs) ==>
118-
io.IO_ifs(ifs) in domain(dp.GetNeighborIAs()) &&
119-
io.IO_as(d.neighborIAs[ifs]) == dp.GetNeighborIA(io.IO_ifs(ifs))
118+
io.IO_ifs{ifs} in domain(dp.GetNeighborIAs()) &&
119+
io.IO_as{uint(d.neighborIAs[ifs])} == dp.GetNeighborIA(io.IO_ifs{ifs})
120120
}
121121

122122
ghost
@@ -135,8 +135,8 @@ requires d.linkTypes != nil ==> acc(d.linkTypes)
135135
decreases
136136
pure func (d *DataPlane) dpSpecWellConfiguredLinkTypes(dp io.DataPlaneSpec) bool {
137137
return forall ifs uint16 :: {ifs in domain(d.linkTypes)} ifs in domain(d.linkTypes) ==>
138-
io.IO_ifs(ifs) in domain(dp.GetLinkTypes()) &&
139-
absLinktype(d.linkTypes[ifs]) == dp.GetLinkType(io.IO_ifs(ifs))
138+
io.IO_ifs{ifs} in domain(dp.GetLinkTypes()) &&
139+
absLinktype(d.linkTypes[ifs]) == dp.GetLinkType(io.IO_ifs{ifs})
140140
}
141141

142142
ghost
@@ -172,7 +172,7 @@ requires d.DpAgreesWithSpec(dp)
172172
requires d.WellConfigured()
173173
requires egressID in d.getDomExternal()
174174
ensures egressID != 0
175-
ensures io.IO_ifs(egressID) in domain(dp.GetNeighborIAs())
175+
ensures io.IO_ifs{egressID} in domain(dp.GetNeighborIAs())
176176
decreases
177177
func (d *DataPlane) EgressIDNotZeroLemma(egressID uint16, dp io.DataPlaneSpec) {
178178
reveal d.WellConfigured()

‎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
}

0 commit comments

Comments
 (0)