Skip to content

Adapt to new pred expr instance syntax #416

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.

Sign up for GitHub

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

Draft
jcp19 wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Adapt to new pred expr instance syntax #416

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
02f34b7
adapt to new pred expr instance syntax
jcp19 May 4, 2026
6128fe6
change missing file
jcp19 May 5, 2026
a23fd09
adapt ghost mutex
jcp19 May 5, 2026
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
90 changes: 45 additions & 45 deletions router/dataplane.go
View file
Open in desktop

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions router/dataplane_concurrency_model.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ pred SharedInv(ghost dp io.DataPlaneSpec, ghost y SharedArg) {
// initialize the shared invariant:
ghost
requires io.token(p) && dp.dp3s_iospec_ordered(s, p)
ensures m.LockP() && m.LockInv() == SharedInv!< dp, y !>
ensures m.LockP() && m.LockInv() == SharedInv{dp, y}
decreases
func InitSharedInv(
dp io.DataPlaneSpec,
Expand All @@ -51,8 +51,8 @@ func InitSharedInv(
yI := InitElemAuth(s.ibuf)
yO := InitElemAuth(s.obuf)
y := SharedArg{&pE, &sE, yI, yO}
fold SharedInv!< dp, y !>()
m.SetInv(SharedInv!< dp, y !>)
fold SharedInv{dp, y}()
m.SetInv(SharedInv{dp, y})
}

/////////////////////////////////////// Prophecies ///////////////////////////////////////
Expand Down
10 changes: 5 additions & 5 deletions router/dataplane_spec_test.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,9 @@ import (
func foldMem_test() {
d@ := DataPlane{}
fold d.Mem()
fold MutexInvariant!<&d!>()
fold MutexInvariant{&d}()
// testing initialization with the operations from dataplane
d.mtx.SetInv(MutexInvariant!<&d!>)
d.mtx.SetInv(MutexInvariant{&d})
d.AddNeighborIA(uint16(1), addr.IA(10))
d.AddNeighborIA(uint16(2), addr.IA(11))
}
Expand Down Expand Up @@ -218,16 +218,16 @@ func testRun(
assert reveal d.DpAgreesWithSpec(dp)

assert reveal d.PreWellConfigured()
fold MutexInvariant!< d !>()
fold MutexInvariant{d}()
// end of foldDataPlaneMem
assert !d.IsRunning()
assert d.InternalConnIsSet()
assert d.KeyIsSet()
assert d.SvcsAreSet()
assert d.MetricsAreSet()
d.mtx.SetInv(MutexInvariant!<d!>)
d.mtx.SetInv(MutexInvariant{d})
assert d.mtx.LockP()
assert d.mtx.LockInv() == MutexInvariant!<d!>
assert d.mtx.LockInv() == MutexInvariant{d}

// io-spec needs to be inhaled
inhale io.token(place)
Expand Down
6 changes: 3 additions & 3 deletions router/io-spec-abstract-transitions.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ requires AbsValidateIngressIDConstraint(oldPkt, ingressID)
requires AbsVerifyCurrentMACConstraint(newPkt, dp)
requires len(newPkt.CurrSeg.Future) == 1 || AbsValidateEgressIDConstraint(newPkt, true, dp)
preserves acc(ioLock.LockP(), _)
preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>
preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
decreases
func InternalEnterEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
Expand Down Expand Up @@ -194,7 +194,7 @@ requires AbsValidateEgressIDConstraint(AbsUpdateNonConsDirIngressSegID(oldPkt,
requires AbsEgressInterfaceConstraint(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID), egressID)
requires newPkt == AbsProcessEgress(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID))
preserves acc(ioLock.LockP(), _)
preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>
preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
decreases
func ExternalEnterOrExitEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
Expand Down Expand Up @@ -235,7 +235,7 @@ requires egressID == none[io.Ifs] ==>
requires egressID != none[io.Ifs] ==>
newPkt == AbsProcessEgress(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)))
preserves acc(ioLock.LockP(), _)
preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>
preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
decreases
func XoverEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
Expand Down
18 changes: 9 additions & 9 deletions router/io-spec-atomic-events.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,12 +52,12 @@ requires dp.dp3s_forward(
newPkt,
egressID)
preserves acc(ioLock.LockP(), _)
preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>
preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
decreases _
func AtomicEnter(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
ghost ioLock.Lock()
unfold SharedInv!< dp, ioSharedArg !>()
unfold SharedInv{dp, ioSharedArg}()
t, s := *ioSharedArg.Place, *ioSharedArg.State
ApplyElemWitness(s.ibuf, ioSharedArg.IBufY, ingressID, oldPkt)
ghost pkt_internal := io.Val(io.ValInternal1{oldPkt, get(ingressID), newPkt, egressID})
Expand All @@ -70,7 +70,7 @@ func AtomicEnter(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressI
UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt)
ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt)
ghost *ioSharedArg.Place = tN
fold SharedInv!< dp, ioSharedArg !>()
fold SharedInv{dp, ioSharedArg}()
ghost ioLock.Unlock()
}

Expand All @@ -82,12 +82,12 @@ requires len(oldPkt.CurrSeg.Future) > 0
requires ElemWitness(ioSharedArg.IBufY, ingressID, oldPkt)
requires dp.dp3s_forward_ext(oldPkt, newPkt, get(egressID))
preserves acc(ioLock.LockP(), _)
preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>
preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
decreases _
func AtomicExit(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
ghost ioLock.Lock()
unfold SharedInv!< dp, ioSharedArg !>()
unfold SharedInv{dp, ioSharedArg}()
t, s := *ioSharedArg.Place, *ioSharedArg.State
ApplyElemWitness(s.ibuf, ioSharedArg.IBufY, ingressID, oldPkt)
ghost pkt_internal := io.Val(io.ValInternal2{oldPkt, newPkt, get(egressID)})
Expand All @@ -100,7 +100,7 @@ func AtomicExit(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID
UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt)
ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt)
ghost *ioSharedArg.Place = tN
fold SharedInv!< dp, ioSharedArg !>()
fold SharedInv{dp, ioSharedArg}()
ghost ioLock.Unlock()
}

Expand Down Expand Up @@ -137,12 +137,12 @@ requires dp.dp3s_forward_xover(
newPkt,
egressID)
preserves acc(ioLock.LockP(), _)
preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>
preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
decreases _
func AtomicXover(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
ghost ioLock.Lock()
unfold SharedInv!< dp, ioSharedArg !>()
unfold SharedInv{dp, ioSharedArg}()
t, s := *ioSharedArg.Place, *ioSharedArg.State
ApplyElemWitness(s.ibuf, ioSharedArg.IBufY, ingressID, oldPkt)
ghost pkt_internal := io.Val(io.ValInternal1{oldPkt, get(ingressID), newPkt, egressID})
Expand All @@ -155,6 +155,6 @@ func AtomicXover(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressI
UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt)
ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt)
ghost *ioSharedArg.Place = tN
fold SharedInv!< dp, ioSharedArg !>()
fold SharedInv{dp, ioSharedArg}()
ghost ioLock.Unlock()
}
22 changes: 11 additions & 11 deletions router/svc.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,8 @@ type services struct {
// @ decreases
func newServices() (s *services) {
tmp := &services{m: make(map[addr.HostSVC][]*net.UDPAddr)}
//@ fold internalLockInv!<tmp!>()
//@ ghost tmp.mtx.SetInv(internalLockInv!<tmp!>)
//@ fold internalLockInv{tmp}()
//@ ghost tmp.mtx.SetInv(internalLockInv{tmp})
//@ fold tmp.Mem()
return tmp
}
Expand All @@ -48,13 +48,13 @@ func (s *services) AddSvc(svc addr.HostSVC, a *net.UDPAddr) {
s.mtx.Lock()
defer s.mtx.Unlock()

//@ unfold internalLockInv!<s!>()
//@ unfold internalLockInv{s}()
addrs := s.m[svc]
//@ ghost if addrs == nil { fold validMapValue(svc, addrs) }
//@ unfold acc(validMapValue(svc, addrs), R10)
if _, ok := s.index(a, addrs /*@, svc @*/); ok {
//@ fold acc(validMapValue(svc, addrs), R10)
//@ fold internalLockInv!<s!>()
//@ fold internalLockInv{s}()
//@ fold acc(s.Mem(), R50)
return
}
Expand All @@ -64,7 +64,7 @@ func (s *services) AddSvc(svc addr.HostSVC, a *net.UDPAddr) {
//@ ghost tmp := s.m[svc]
//@ fold InjectiveMem(tmp[len(tmp)-1], len(tmp)-1)
//@ fold validMapValue(svc, s.m[svc])
//@ fold internalLockInv!<s!>()
//@ fold internalLockInv{s}()
//@ fold acc(s.Mem(), R50)
}

Expand All @@ -76,13 +76,13 @@ func (s *services) DelSvc(svc addr.HostSVC, a *net.UDPAddr) {
s.mtx.Lock()
defer s.mtx.Unlock()

//@ unfold internalLockInv!<s!>()
//@ unfold internalLockInv{s}()
addrs := s.m[svc]
//@ ghost if addrs == nil { fold validMapValue(svc, addrs) }
//@ assert validMapValue(svc, addrs)
index, ok := s.index(a, addrs /*@, svc @*/)
if !ok {
//@ fold internalLockInv!<s!>()
//@ fold internalLockInv{s}()
//@ fold acc(s.Mem(), R50)
return
}
Expand All @@ -97,7 +97,7 @@ func (s *services) DelSvc(svc addr.HostSVC, a *net.UDPAddr) {
//@ assert forall i int :: { &addrs[:len(addrs)-1][i] }{ &addrs[i] } 0 <= i && i < len(addrs)-1 ==> &addrs[:len(addrs)-1][i] == &addrs[i]
s.m[svc] = addrs[:len(addrs)-1]
//@ fold validMapValue(svc, s.m[svc])
//@ fold internalLockInv!<s!>()
//@ fold internalLockInv{s}()
//@ fold acc(s.Mem(), R50)
}

Expand All @@ -110,15 +110,15 @@ func (s *services) Any(svc addr.HostSVC) (r *net.UDPAddr, b bool) {
s.mtx.Lock()
defer s.mtx.Unlock()

//@ unfold internalLockInv!<s!>()
//@ unfold internalLockInv{s}()
addrs := s.m[svc]
if len(addrs) == 0 {
//@ fold internalLockInv!<s!>()
//@ fold internalLockInv{s}()
return nil, false
}
//@ assert validMapValue(svc, addrs)
//@ unfold acc(validMapValue(svc, addrs))
//@ defer fold internalLockInv!<s!>()
//@ defer fold internalLockInv{s}()
//@ defer fold acc(validMapValue(svc, addrs))
tmpIdx := mrand.Intn(len(addrs))
tmpAddr := addrs[tmpIdx]
Expand Down
2 changes: 1 addition & 1 deletion router/svc_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ import (

pred (s *services) Mem() {
s.mtx.LockP() &&
s.mtx.LockInv() == internalLockInv!<s!>;
s.mtx.LockInv() == internalLockInv{s};
}

pred internalLockInv(s *services) {
Expand Down
4 changes: 2 additions & 2 deletions router/svc_spec_test.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,8 @@ import (

func foldInternalLockInvAndMem_test() {
s := &services{m: make(map[addr.HostSVC][]*net.UDPAddr)}
fold internalLockInv!<s!>()
s.mtx.SetInv(internalLockInv!<s!>)
fold internalLockInv{s}()
s.mtx.SetInv(internalLockInv{s})
fold s.Mem()
}

Expand Down
2 changes: 1 addition & 1 deletion verification/dependencies/context/context.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ type Context interface {

preserves acc(Mem(), _)
ensures acc(c.RecvChannel(), _)
ensures c.RecvGivenPerm() == PredTrue!<!>
ensures c.RecvGivenPerm() == PredTrue{}
decreases
Done() (c <-chan struct{})

Expand Down
4 changes: 2 additions & 2 deletions verification/dependencies/github.com/prometheus/client_golang/prometheus/collector.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ type Collector interface {
// If a Collector encounters an error while executing this method, it
// must send an invalid descriptor (created with NewInvalidDesc) to
// signal the error to the registry.
requires Mem() && acc(c.SendChannel(), _) && c.SendGivenPerm() == (*Desc).Mem!<_!>;
requires Mem() && acc(c.SendChannel(), _) && c.SendGivenPerm() == (*Desc).Mem{_};
ensures Mem()
Describe(c chan<- *Desc)
// Collect is called by the Prometheus registry when collecting
Expand All @@ -59,7 +59,7 @@ type Collector interface {
// implemented in a concurrency safe way. Blocking occurs at the expense
// of total performance of rendering all registered metrics. Ideally,
// Collector implementations support concurrent readers.
requires Mem() && acc(c.SendChannel(), _) && c.SendGivenPerm() == Metric.Mem!<_!>;
requires Mem() && acc(c.SendChannel(), _) && c.SendGivenPerm() == Metric.Mem{_};
ensures Mem()
Collect(c chan<- Metric)
}
2 changes: 1 addition & 1 deletion verification/utils/ghost_sync/ghost-mutex.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ func (m gpointer[GhostMutex]) SetInv(inv pred())
ghost
requires acc(m.LockP(), _)
ensures m.LockP() && m.UnlockP() && m.LockInv()()
decreases _ if sync.IgnoreBlockingForTermination()
decreases _
func (m gpointer[GhostMutex]) Lock()

ghost
Expand Down
16 changes: 8 additions & 8 deletions verification/utils/resalgebra/oneshot_test.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,13 +42,13 @@ func mkOneShot() (o *oneshot, ghost l LocName) {
}

requires m.LockP()
requires m.LockInv() == oneshotInv!<o, l!>
requires m.LockInv() == oneshotInv{o, l}
requires n != 0
func (o *oneshot) trySet(n int, m *sync.Mutex, ghost l LocName) bool {
m.Lock()
defer m.Unlock()
unfold oneshotInv!<o, l!>()
defer fold oneshotInv!<o, l!>()
unfold oneshotInv{o, l}()
defer fold oneshotInv{o, l}()
if o.isInit {
return false
}
Expand All @@ -60,10 +60,10 @@ func (o *oneshot) trySet(n int, m *sync.Mutex, ghost l LocName) bool {
}

requires m.LockP()
requires m.LockInv() == oneshotInv!<o, l!>
requires m.LockInv() == oneshotInv{o, l}
func (o *oneshot) check(m *sync.Mutex, ghost l LocName) {
m.Lock()
unfold oneshotInv!<o, l!>()
unfold oneshotInv{o, l}()
y1 := o.V
ghost e1 := o.e
ghost isInit1 := o.isInit
Expand All @@ -74,11 +74,11 @@ func (o *oneshot) check(m *sync.Mutex, ghost l LocName) {
GhostOp1(l, OneShotRA, e1, e1)
assert GhostLocation(l, OneShotRA, e1) && GhostLocation(l, OneShotRA, e1)
}
fold oneshotInv!<o, l!>()
fold oneshotInv{o, l}()
m.Unlock()

m.Lock()
unfold oneshotInv!<o, l!>()
unfold oneshotInv{o, l}()
y2 := o.V
ghost e2 := o.e
ghost isInit2 := o.isInit
Expand All @@ -97,6 +97,6 @@ func (o *oneshot) check(m *sync.Mutex, ghost l LocName) {
GhostValid(l, OneShotRA, OneShotRA.Compose(e1, e2))
assert e1 == e2
}
fold oneshotInv!<o, l!>()
fold oneshotInv{o, l}()
m.Unlock()
}
Loading