From 41d886420ea4480a0deea3605e32864e7f3037d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 9 Feb 2026 17:12:17 +0100 Subject: [PATCH] backup --- router/dataplane.go | 10 +++++++++- router/dataplane_spec.gobra | 7 +++++-- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 6ad2c3181..084eb202b 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -149,6 +149,10 @@ type bfdSession interface { type BatchConn interface { // @ pred Mem() + // @ requires Mem() + // @ decreases + // @ pure Id() uint16 + // @ requires acc(Mem(), _) // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> // @ msgs[i].Mem() @@ -179,11 +183,14 @@ type BatchConn interface { ReadBatch(msgs underlayconn.Messages /*@, ghost ingressID uint16, ghost prophecyM int, ghost place io.Place @*/) (n int, err error) // @ requires acc(addr.Mem(), _) // @ requires acc(Mem(), _) - // @ preserves acc(sl.Bytes(b, 0, len(b)), R10) + // @ requires acc(sl.Bytes(b, 0, len(b)), R10) + // @ requires absIO_val(b, Id()).isValUnsupported + // @ ensures acc(sl.Bytes(b, 0, len(b)), R10) // @ ensures err == nil ==> 0 <= n && n <= len(b) // @ ensures err != nil ==> err.ErrorMem() WriteTo(b []byte, addr *net.UDPAddr) (n int, err error) // @ requires acc(Mem(), _) + // @ requires Id() == egressID // (VerifiedSCION) opted for less reusable spec for WriteBatch for // performance reasons. // @ requires len(msgs) == 1 @@ -410,6 +417,7 @@ func (d *DataPlane) AddInternalInterface(conn BatchConn, ip net.IP) error { // If a connection for the given ID is already set this method will return an // error. This can only be called on a not yet running dataplane. // @ requires conn != nil && conn.Mem() +// @ requires conn.Id() == ifID // @ preserves acc(d.Mem(), OutMutexPerm) // @ preserves !d.IsRunning() // @ preserves d.mtx.LockP() diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index ac0bc14a4..8d2ad015e 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -86,8 +86,10 @@ pred accAddr(addrs map[uint16]*net.UDPAddr) { pred accBatchConn(batchConns map[uint16]BatchConn) { acc(batchConns) && - forall b BatchConn :: { b elem range(batchConns) }{ b.Mem() } b elem range(batchConns) ==> - b!= nil && acc(b.Mem(), _) + (forall b BatchConn :: { b elem range(batchConns) }{ b.Mem() } b elem range(batchConns) ==> + b != nil && acc(b.Mem(), _)) && + (forall i uint16 :: { i elem domain(batchConns) }{ batchConns[i] } i elem domain(batchConns) ==> + BatchConn(batchConns[i]) != nil && BatchConn(batchConns[i]).Id() == i) } pred accBfdSession(bfdSessions map[uint16]bfdSession) { @@ -671,6 +673,7 @@ pred (d *DataPlane) validResult(result processResult, addrAliasesPkt bool) { // EgressID (result.EgressID != 0 ==> result.EgressID elem d.getDomForwardingMetrics()) && // OutConn + // TODO: strengthen here for new cond (result.OutConn != nil ==> acc(result.OutConn.Mem(), _)) && // OutAddr (addrAliasesPkt && result.OutAddr != nil ==> acc(result.OutAddr.Mem(), R15)) &&