Skip to content

Commit 9dfa7e7

Browse files
jcp19jcp19
committed
cleanup, finish last lemma
1 parent 5d5fe46 commit 9dfa7e7

File tree

1 file changed

+90
-101
lines changed

1 file changed

+90
-101
lines changed

‎router/dataplane_concurrency_model.gobra‎

Lines changed: 90 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -297,77 +297,43 @@ decreases
297297
pure func (ra TypeAuthRA) IsValid(e resalgebra.Elem) bool {
298298
return let x := e.(AuthCarrier) in
299299
x.fst === Bottom{} ||
300-
(typeOf(x.fst) == type[Dict] && DictLessThan(x.snd.V, x.fst.(Dict).V))
300+
(typeOf(x.fst) == type[Dict] && dictLessThan(x.snd.V, x.fst.(Dict).V))
301301
}
302302

303303
ghost
304304
decreases
305-
pure func DictLessThan(d1 dict[Key]Val, d2 dict[Key]Val) bool {
305+
pure func dictLessThan(d1 dict[Key]Val, d2 dict[Key]Val) bool {
306306
return (forall k Key :: k elem domain(d1) ==> k elem domain(d2) && AsSet(d1[k]) union AsSet(d2[k]) == AsSet(d2[k]))
307307
}
308308

309309
ghost
310-
requires DictLessThan(d1, d2)
311-
requires DictLessThan(d2, d3)
312-
ensures DictLessThan(d1, d3)
310+
ensures forall d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val :: {dictLessThan(d1, d2), dictLessThan(d2, d3)} dictLessThan(d1, d2) && dictLessThan(d2, d3) ==>
311+
dictLessThan(d1, d3)
313312
decreases
314-
func DictLessThanTransitive(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) {
313+
func dictLessThanTransitiveQ() {
315314
// proven
316315
}
317316

318317
ghost
319-
requires DictLessThan(d1, d2)
320-
requires DictLessThan(d2, d3)
321-
requires !DictLessThan(d2, d1) || !DictLessThan(d3, d2)
322-
ensures DictLessThan(d1, d3)
323-
ensures !DictLessThan(d3, d1)
318+
ensures dictLessThan(d1, d3) && dictLessThan(d2, d3) ==> dictLessThan(dictMax(d1, d2), d3)
324319
decreases
325-
func StrictDictLessThanTransitive(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) {
326-
DictLessThanTransitive(d1, d2, d3)
327-
assert DictLessThan(d1, d3)
328-
assert d1 !== d3
329-
330-
if DictLessThan(d3, d1) {
331-
DictLessEq(d1, d3)
332-
assert false // Unreachable
333-
}
334-
}
335-
336-
ghost
337-
ensures forall d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val :: DictLessThan(d1, d2) && DictLessThan(d2, d3) ==>
338-
DictLessThan(d1, d3)
339-
decreases
340-
func DictLessThanTransitiveQ() {
341-
// proven
320+
pure func dictMaxIsLessThan(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) U {
321+
return dictUnionIsLessThan(d1, d2, d3)
342322
}
343323

344324
ghost
345-
ensures DictLessThan(m, io.insert(m, k, e))
346325
decreases
347-
func DictLessThanInsert(m dict[Key]Val, k Key, e Elem) {
348-
// proven
349-
}
350-
351-
ghost
352-
ensures DictLessThan(d1, d3) && DictLessThan(d2, d3) ==> DictLessThan(DictMax(d1, d2), d3)
353-
decreases
354-
func DictMaxIsLessThan(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) {
355-
DictUnionIsLessThan(d1, d2, d3)
356-
}
357-
358-
ghost
359-
decreases
360-
pure func DictMax(d1 dict[Key]Val, d2 dict[Key]Val) dict[Key]Val {
326+
pure func dictMax(d1 dict[Key]Val, d2 dict[Key]Val) dict[Key]Val {
361327
// logically redundant but it simplifies automated reasoning when
362-
// either DictLessThan(d1, d2) or DictLessThan(d2, d1) is known.
363-
return DictLessThan(d1, d2) ? d2 : DictLessThan(d2, d1) ? d1 : DictUnion(d1, d2)
328+
// either dictLessThan(d1, d2) or dictLessThan(d2, d1) is known.
329+
return dictLessThan(d1, d2) ? d2 : dictLessThan(d2, d1) ? d1 : dictUnion(d1, d2)
364330
}
365331

366332
ghost
367-
requires DictLessThan(d1, d2) && DictLessThan(d2, d1)
333+
requires dictLessThan(d1, d2) && dictLessThan(d2, d1)
368334
ensures d1 === d2
369335
decreases
370-
func DictLessEq(d1 dict[Key]Val, d2 dict[Key]Val) {
336+
func dictLessEq(d1 dict[Key]Val, d2 dict[Key]Val) {
371337
assert forall k Key :: k elem domain(d1) ==> k elem domain(d2) && AsSet(d1[k]) union AsSet(d2[k]) == AsSet(d2[k])
372338
assert forall k Key :: k elem domain(d2) ==> k elem domain(d1) && AsSet(d1[k]) union AsSet(d2[k]) == AsSet(d1[k])
373339
assert domain(d1) == domain(d2)
@@ -380,37 +346,37 @@ pure func keyInDict(d dict[Key]Val, k Key, v io.Pkt) bool {
380346
}
381347

382348
ghost
383-
ensures domain(DictMax(d1, d2)) == domain(d1) union domain(d2)
384-
ensures let d := DictMax(d1, d2) in
349+
ensures domain(dictMax(d1, d2)) == domain(d1) union domain(d2)
350+
ensures let d := dictMax(d1, d2) in
385351
forall k Key, v io.Pkt :: !keyInDict(d, k, v) == !(keyInDict(d1, k, v) || keyInDict(d2, k, v))
386352
decreases
387353
func dictMaxAssocLemma0(d1 dict[Key]Val, d2 dict[Key]Val) {
388-
reveal DictUnion(d1, d2)
354+
reveal dictUnion(d1, d2)
389355
}
390356

391357
ghost
392-
ensures domain(DictMax(d1, DictMax(d2, d3))) == domain(d1) union domain(d2) union domain(d3)
393-
ensures let d := DictMax(d1, DictMax(d2, d3)) in
358+
ensures domain(dictMax(d1, dictMax(d2, d3))) == domain(d1) union domain(d2) union domain(d3)
359+
ensures let d := dictMax(d1, dictMax(d2, d3)) in
394360
forall k Key, v io.Pkt :: keyInDict(d, k, v) == (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v))
395361
decreases
396362
func dictMaxAssocLemma1(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) {
397-
d := DictMax(d1, DictMax(d2, d3))
363+
d := dictMax(d1, dictMax(d2, d3))
398364
assert forall k Key, v io.Pkt :: (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v)) ==> keyInDict(d, k, v)
399365
dictMaxAssocLemma0(d2, d3)
400-
dictMaxAssocLemma0(d1, DictMax(d2, d3))
366+
dictMaxAssocLemma0(d1, dictMax(d2, d3))
401367
assert forall k Key, v io.Pkt :: keyInDict(d, k, v) ==> (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v))
402368
}
403369

404370
ghost
405-
ensures domain(DictMax(DictMax(d1, d2), d3)) == domain(d1) union domain(d2) union domain(d3)
406-
ensures let d := DictMax(DictMax(d1, d2), d3) in
371+
ensures domain(dictMax(dictMax(d1, d2), d3)) == domain(d1) union domain(d2) union domain(d3)
372+
ensures let d := dictMax(dictMax(d1, d2), d3) in
407373
forall k Key, v io.Pkt :: keyInDict(d, k, v) == (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v))
408374
decreases
409375
func dictMaxAssocLemma2(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) {
410-
d := DictMax(DictMax(d1, d2), d3)
376+
d := dictMax(dictMax(d1, d2), d3)
411377
assert forall k Key, v io.Pkt :: (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v)) ==> keyInDict(d, k, v)
412378
dictMaxAssocLemma0(d1, d2)
413-
dictMaxAssocLemma0(DictMax(d1, d2), d3)
379+
dictMaxAssocLemma0(dictMax(d1, d2), d3)
414380
assert forall k Key, v io.Pkt :: keyInDict(d, k, v) ==> (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v))
415381
}
416382

@@ -427,9 +393,9 @@ func dictExtensionality(d1 dict[Key]Val, d2 dict[Key]Val) {
427393
lemmaSubSet()
428394
assert forall k Key :: k elem domain(d1) ==> AsSet(d1[k]) union AsSet(d2[k]) == AsSet(d2[k])
429395
assert forall k Key :: k elem domain(d2) ==> AsSet(d2[k]) union AsSet(d1[k]) == AsSet(d1[k])
430-
assert DictLessThan(d1, d2)
431-
assert DictLessThan(d2, d1)
432-
DictLessEq(d1, d2)
396+
assert dictLessThan(d1, d2)
397+
assert dictLessThan(d2, d1)
398+
dictLessEq(d1, d2)
433399
}
434400

435401
ghost
@@ -440,27 +406,27 @@ func lemmaSubSet() {
440406
}
441407

442408
ghost
443-
ensures DictMax(d1, DictMax(d2, d3)) === DictMax(DictMax(d1, d2), d3)
409+
ensures dictMax(d1, dictMax(d2, d3)) === dictMax(dictMax(d1, d2), d3)
444410
decreases
445-
func DictMaxAssoc(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) {
411+
func dictMaxAssoc(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) {
446412
dictMaxAssocLemma1(d1, d2, d3)
447413
dictMaxAssocLemma2(d1, d2, d3)
448-
dictExtensionality(DictMax(d1, DictMax(d2, d3)), DictMax(DictMax(d1, d2), d3))
414+
dictExtensionality(dictMax(d1, dictMax(d2, d3)), dictMax(dictMax(d1, d2), d3))
449415
}
450416

451417
ghost
452-
ensures DictMax(d1, d2) == DictMax(d2, d1)
418+
ensures dictMax(d1, d2) == dictMax(d2, d1)
453419
decreases
454-
func DictMaxIsComm(d1 dict[Key]Val, d2 dict[Key]Val) {
455-
if DictLessThan(d1, d2) && DictLessThan(d2, d1) {
456-
DictLessEq(d1, d2)
420+
func dictMaxIsComm(d1 dict[Key]Val, d2 dict[Key]Val) {
421+
if dictLessThan(d1, d2) && dictLessThan(d2, d1) {
422+
dictLessEq(d1, d2)
457423
}
458-
assert d1 != d2 && DictLessThan(d1, d2) ==> !DictLessThan(d2, d1)
459-
assert DictLessThan(d1, d2) ==> DictMax(d1, d2) == d2
460-
assert DictLessThan(d1, d2) ==> DictMax(d2, d1) == d2
461-
assert DictLessThan(d2, d1) ==> DictMax(d1, d2) == d1
462-
assert DictLessThan(d2, d1) ==> DictMax(d2, d1) == d1
463-
DictUnionIsComm(d1, d2)
424+
assert d1 != d2 && dictLessThan(d1, d2) ==> !dictLessThan(d2, d1)
425+
assert dictLessThan(d1, d2) ==> dictMax(d1, d2) == d2
426+
assert dictLessThan(d1, d2) ==> dictMax(d2, d1) == d2
427+
assert dictLessThan(d2, d1) ==> dictMax(d1, d2) == d1
428+
assert dictLessThan(d2, d1) ==> dictMax(d2, d1) == d1
429+
dictUnionIsComm(d1, d2)
464430
}
465431

466432
ghost
@@ -480,10 +446,10 @@ pure func (ra TypeAuthRA) Compose(e1 resalgebra.Elem, e2 resalgebra.Elem) (res r
480446
return let c1 := e1.(AuthCarrier) in
481447
let c2 := e2.(AuthCarrier) in
482448
(c1.fst === Bottom{} ?
483-
AuthCarrier{c2.fst, Dict{DictMax(c1.snd.V, c2.snd.V)}} :
449+
AuthCarrier{c2.fst, Dict{dictMax(c1.snd.V, c2.snd.V)}} :
484450
(c2.fst === Bottom{} ?
485-
AuthCarrier{c1.fst, Dict{DictMax(c1.snd.V, c2.snd.V)}} :
486-
AuthCarrier{Top{}, Dict{DictMax(c1.snd.V, c2.snd.V)}}))
451+
AuthCarrier{c1.fst, Dict{dictMax(c1.snd.V, c2.snd.V)}} :
452+
AuthCarrier{Top{}, Dict{dictMax(c1.snd.V, c2.snd.V)}}))
487453
}
488454

489455
ghost
@@ -499,7 +465,7 @@ func (ra TypeAuthRA) ComposeAssoc(e1 resalgebra.Elem, e2 resalgebra.Elem, e3 res
499465
comp2 := ra.Compose(e1, ra.Compose(e2, e3)).(AuthCarrier)
500466

501467
assert comp1.fst === comp2.fst
502-
DictMaxAssoc(c1.snd.V, c2.snd.V, c3.snd.V)
468+
dictMaxAssoc(c1.snd.V, c2.snd.V, c3.snd.V)
503469
}
504470

505471
ghost
@@ -509,7 +475,7 @@ decreases
509475
func (ra TypeAuthRA) ComposeComm(e1 resalgebra.Elem, e2 resalgebra.Elem) {
510476
c1 := e1.(AuthCarrier)
511477
c2 := e2.(AuthCarrier)
512-
DictMaxIsComm(c1.snd.V, c2.snd.V)
478+
dictMaxIsComm(c1.snd.V, c2.snd.V)
513479
}
514480

515481
ghost
@@ -557,8 +523,8 @@ func (ra TypeAuthRA) ValidOp(e1 resalgebra.Elem, e2 resalgebra.Elem) {
557523
if (c1.fst !== Bottom{}) {
558524
fst := c.fst.(Dict).V
559525
snd := c.snd.V
560-
assert DictLessThan(snd, fst)
561-
assert snd === DictMax(c1.snd.V, c2.snd.V)
526+
assert dictLessThan(snd, fst)
527+
assert snd === dictMax(c1.snd.V, c2.snd.V)
562528
}
563529
}
564530

@@ -608,18 +574,39 @@ func UpdateElemWitness(m dict[Key]Val, y ElemRA, k Key, e Elem) {
608574
fold ElemWitness(y, k, e)
609575
}
610576

577+
// by far, the slowest lemma to prove atm
611578
ghost
612579
ensures let d := Dict{dict[Key]Val{k: set[io.Pkt]{e}}} in
613580
let c := (TypeAuthRA{}).Compose(AuthView(Dict{io.insert(m, k, e)}), FragView(d)) in
614581
resalgebra.IsFramePreservingUpdate(TypeAuthRA{}, AuthView(Dict{m}), c)
615582
decreases
616583
func updateElemWitnessAuxLemma(m dict[Key]Val, k Key, e Elem) {
584+
ra := TypeAuthRA{}
585+
a := AuthView(Dict{m})
617586
d := Dict{dict[Key]Val{k: set[io.Pkt]{e}}}
618-
c := (TypeAuthRA{}).Compose(AuthView(Dict{io.insert(m, k, e)}), FragView(d))
619-
assert (TypeAuthRA{}).IsValid(AuthView(Dict{m})) ==>
620-
(TypeAuthRA{}).IsValid(c)
621-
//assert forall e resalgebra.Elem :: (TypeAuthRA{}).IsValid(AuthView(Dict{m}))
622-
assume false
587+
c := ra.Compose(AuthView(Dict{io.insert(m, k, e)}), FragView(d))
588+
assert ra.IsValid(a) ==> ra.IsValid(c)
589+
assert forall ee resalgebra.Elem :: ra.IsElem(ee) && ra.IsValid(ra.Compose(a, ee)) ==>
590+
(let ae := ra.Compose(a, ee).(AuthCarrier) in
591+
(ae.fst == Bottom{} || dictLessThan(ae.snd.V, m)))
592+
dictLessThanTransitiveQ()
593+
assert forall ee resalgebra.Elem :: ra.IsElem(ee) && ra.IsValid(ra.Compose(a, ee)) ==>
594+
ee.(AuthCarrier).fst === Bottom{} &&
595+
dictLessThan(ee.(AuthCarrier).snd.V, m) &&
596+
dictLessThan(m, io.insert(m, k, e)) &&
597+
dictLessThan(ee.(AuthCarrier).snd.V, io.insert(m, k, e))
598+
assert forall ee resalgebra.Elem :: ra.IsElem(ee) && ra.IsValid(ra.Compose(a, ee)) ==>
599+
ee.(AuthCarrier).fst === Bottom{} &&
600+
let ce := ra.Compose(c, ee).(AuthCarrier) in
601+
ce.fst.(Dict).V === io.insert(m, k, e)
602+
assert forall ee resalgebra.Elem :: ra.IsElem(ee) && ra.IsValid(ra.Compose(a, ee)) ==>
603+
ee.(AuthCarrier).fst === Bottom{} &&
604+
let ce := ra.Compose(c, ee).(AuthCarrier) in
605+
ce.snd.V == dictMax(d.V, ee.(AuthCarrier).snd.V) &&
606+
dictLessThan(d.V, io.insert(m, k, e)) &&
607+
dictLessThan(ee.(AuthCarrier).snd.V, io.insert(m, k, e)) &&
608+
let _ := dictMaxIsLessThan(d.V, ee.(AuthCarrier).snd.V, io.insert(m, k, e)) in
609+
true
623610
}
624611

625612
ghost
@@ -635,9 +622,9 @@ func InitElemAuth(m dict[Key]Val) (y ElemRA) {
635622

636623
ghost
637624
opaque
638-
ensures DictLessThan(d1, res) && DictLessThan(d2, res)
625+
ensures dictLessThan(d1, res) && dictLessThan(d2, res)
639626
decreases
640-
pure func DictUnion(d1 dict[Key]Val, d2 dict[Key]Val) (res dict[Key]Val) {
627+
pure func dictUnion(d1 dict[Key]Val, d2 dict[Key]Val) (res dict[Key]Val) {
641628
return dictUnionAux(d1, d2)
642629
}
643630

@@ -664,32 +651,33 @@ decreases len((domain(d1) union domain(d2)) setminus visitedKeys)
664651
pure func dictUnionAuxIter(d1 dict[Key]Val, d2 dict[Key]Val, visitedKeys set[Key]) (res dict[Key]Val) {
665652
return visitedKeys === (domain(d1) union domain(d2)) ?
666653
dict[Key]Val{} :
667-
let _ := LemmaSetInclusion(visitedKeys, domain(d1) union domain(d2)) in
654+
let _ := lemmaSetInclusion(visitedKeys, domain(d1) union domain(d2)) in
668655
let c := choose((domain(d1) union domain(d2)) setminus visitedKeys) in
669656
let v := (c elem domain(d1) && c elem domain(d2) ? AsSet(d1[c]) union AsSet(d2[c]) : (c elem domain(d1) ? d1[c] : d2[c])) in
670657
let d := dictUnionAuxIter(d1, d2, visitedKeys union set[Key]{c}) in
671658
d[c = v]
672659
}
673660

674661
ghost
675-
ensures DictUnion(d1, d2) === DictUnion(d2, d1)
662+
ensures dictUnion(d1, d2) === dictUnion(d2, d1)
676663
decreases
677-
func DictUnionIsComm(d1 dict[Key]Val, d2 dict[Key]Val) {
678-
u1 := reveal DictUnion(d1, d2)
679-
u2 := reveal DictUnion(d2, d1)
664+
func dictUnionIsComm(d1 dict[Key]Val, d2 dict[Key]Val) {
665+
u1 := reveal dictUnion(d1, d2)
666+
u2 := reveal dictUnion(d2, d1)
680667
assert domain(u1) === domain(u2)
681668
assert forall k Key :: k elem domain(u1) ==> u1[k] == u2[k]
682669
}
683670

684-
// DictUnion(d1, d2) is the smallest dict that is bigger than both d1 and d2
671+
// dictUnion(d1, d2) is the smallest dict that is bigger than both d1 and d2
685672
ghost
686-
ensures DictLessThan(d1, d3) && DictLessThan(d2, d3) ==> DictLessThan(DictUnion(d1, d2), d3)
673+
ensures dictLessThan(d1, d3) && dictLessThan(d2, d3) ==> dictLessThan(dictUnion(d1, d2), d3)
687674
decreases
688-
func DictUnionIsLessThan(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) {
689-
u1 := reveal DictUnion(d1, d2)
690-
u2 := reveal DictUnion(d2, d1)
691-
assert domain(u1) === domain(u2)
692-
assert forall k Key :: k elem domain(u1) ==> u1[k] == u2[k]
675+
pure func dictUnionIsLessThan(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) U {
676+
return let u1 := reveal dictUnion(d1, d2) in
677+
let u2 := reveal dictUnion(d2, d1) in
678+
let _ := domain(u1) === domain(u2) in
679+
let _ := forall k Key :: k elem domain(u1) ==> u1[k] == u2[k] in
680+
U{}
693681
}
694682

695683
/////////////////////////////////////// Utility ///////////////////////////////////////
@@ -706,13 +694,14 @@ ghost
706694
requires (s1 union s2) === s2 && s1 !== s2
707695
ensures 0 < len(s2 setminus s1)
708696
decreases
709-
pure func LemmaSetInclusion(s1 set[Key], s2 set[Key]) U {
697+
pure func lemmaSetInclusion(s1 set[Key], s2 set[Key]) U {
710698
return U{}
711699
}
712700

713701

714702
// Hilbert's choice operator, cannot be proven in Gobra yet.
715703
ghost
704+
trusted
716705
requires 0 < len(s)
717706
ensures res elem s
718707
decreases

0 commit comments

Comments
 (0)