Skip to content
This repository has been archived by the owner on May 3, 2024. It is now read-only.

Commit

Permalink
permission fix for dpSpecWellConfigured
Browse files Browse the repository at this point in the history
  • Loading branch information
@mlimbeck
mlimbeck committed Feb 19, 2024
1 parent 7eca4dc commit 67a4d5d
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 17 deletions.
28 changes: 14 additions & 14 deletions router/dataplane_spec.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -200,7 +200,7 @@ func (d *DataPlane) getForwardingMetrics() {
ghost
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand All @@ -212,7 +212,7 @@ pure func (d *DataPlane) getValForwardingMetrics() map[uint16]forwardingMetrics
ghost
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand All @@ -228,7 +228,7 @@ pure func (d *DataPlane) getDomForwardingMetrics() set[uint16] {
ghost
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand All @@ -244,7 +244,7 @@ pure func (d *DataPlane) GetDomInternalNextHops() set[uint16] {
ghost
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand Down Expand Up @@ -343,7 +343,7 @@ func (d *DataPlane) getSvcMem() {
ghost
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand All @@ -355,7 +355,7 @@ pure func (d *DataPlane) getValSvc() *services {
ghost
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand Down Expand Up @@ -418,7 +418,7 @@ requires acc(d.Mem(), _)
requires acc(&d.running, _)
ensures d.IsRunning() == d.running
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand All @@ -431,7 +431,7 @@ ghost
pure
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand All @@ -444,7 +444,7 @@ ghost
pure
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand All @@ -460,7 +460,7 @@ requires acc(d.Mem(), _)
requires acc(&d.internal, _)
ensures d.InternalConnIsSet() == (d.internal != nil)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand All @@ -473,7 +473,7 @@ ghost
pure
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand All @@ -489,7 +489,7 @@ requires acc(d.Mem(), _)
requires acc(&d.macFactory, _)
ensures d.KeyIsSet() == (d.macFactory != nil)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand All @@ -502,7 +502,7 @@ ghost
pure
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand Down Expand Up @@ -734,7 +734,7 @@ pure func (d *DataPlane) domainForwardingMetrics() set[uint16] {
ghost
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// Gobra requires intermediate assertions to make this verify,
// which is not possible to add here.
Expand Down
6 changes: 3 additions & 3 deletions router/io-spec.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -632,14 +632,14 @@ pure func (d *DataPlane) dpSpecWellConfiguredLinkTypes(dp io.DataPlaneSpec) bool
}

ghost
requires acc(MutexInvariant(d), _)
requires acc(d.Mem(), _)
// The termination of this method is assumed. The reason is that the termination
// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
// followed by a fold of the same invariant with the same permission amount.
// As shown in methods SimplifyPermInv and ElaboratePermInv, Gobra requires intermediate
// assertions to make this verify, which is not easy to add here.
decreases _
pure func (d *DataPlane) dpSpecWellConfigured(dp io.DataPlaneSpec) bool {
return unfolding acc(MutexInvariant(d), _) in d.dpSpecWellConfiguredLocalIA(dp) &&
return unfolding acc(d.Mem(), _) in d.dpSpecWellConfiguredLocalIA(dp) &&
d.dpSpecWellConfiguredNeighborIAs(dp) && d.dpSpecWellConfiguredLinkTypes(dp)
}

0 comments on commit 67a4d5d

Please sign in to comment.