diff --git a/private/underlay/conn/conn.go b/private/underlay/conn/conn.go index dcdaaf045..85a17d824 100644 --- a/private/underlay/conn/conn.go +++ b/private/underlay/conn/conn.go @@ -51,7 +51,7 @@ type Conn interface { //@ ensures err != nil ==> err.ErrorMem() ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error) //@ requires acc(Mem(), _) - //@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> m[i].Mem(1) + //@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> m[i].Mem() //@ ensures err == nil ==> 0 <= n && n <= len(m) //@ ensures err != nil ==> err.ErrorMem() ReadBatch(m Messages) (n int, err error) @@ -67,7 +67,7 @@ type Conn interface { //@ ensures err != nil ==> err.ErrorMem() WriteTo(b []byte, u *net.UDPAddr) (n int, err error) //@ requires acc(Mem(), _) - //@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> acc(m[i].Mem(1), R10) + //@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> acc(m[i].Mem(), R10) //@ ensures err == nil ==> 0 <= n && n <= len(m) //@ ensures err != nil ==> err.ErrorMem() WriteBatch(m Messages, k int) (n int, err error) @@ -164,24 +164,24 @@ func newConnUDPIPv4(listen, remote *net.UDPAddr, cfg *Config) (res *connUDPIPv4, // ReadBatch reads up to len(msgs) packets, and stores them in msgs. // It returns the number of packets read, and an error if any. // @ requires acc(c.Mem(), _) -// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) +// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() // @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs) // @ ensures errRet != nil ==> errRet.ErrorMem() func (c *connUDPIPv4) ReadBatch(msgs Messages) (nRet int, errRet error) { //@ unfold acc(c.Mem(), _) // (VerifiedSCION) 1 is the length of the buffers of the messages in msgs - n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE /*@, 1 @*/) + n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE) return n, err } // @ requires acc(c.Mem(), _) -// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), R10) +// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(), R10) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err != nil ==> err.ErrorMem() func (c *connUDPIPv4) WriteBatch(msgs Messages, flags int) (n int, err error) { //@ unfold acc(c.Mem(), _) // (VerifiedSCION) 1 is the length of the buffers of the messages in msgs - return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/) + return c.pconn.WriteBatch(msgs, flags) } // SetReadDeadline sets the read deadline associated with the endpoint. @@ -238,24 +238,24 @@ func newConnUDPIPv6(listen, remote *net.UDPAddr, cfg *Config) (res *connUDPIPv6, // ReadBatch reads up to len(msgs) packets, and stores them in msgs. // It returns the number of packets read, and an error if any. // @ requires acc(c.Mem(), _) -// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) +// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() // @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs) // @ ensures errRet != nil ==> errRet.ErrorMem() func (c *connUDPIPv6) ReadBatch(msgs Messages) (nRet int, errRet error) { //@ unfold acc(c.Mem(), _) // (VerifiedSCION) 1 is the length of the buffers of the messages in msgs - n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE /*@, 1 @*/) + n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE) return n, err } // @ requires acc(c.Mem(), _) -// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), R10) +// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(), R10) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err != nil ==> err.ErrorMem() func (c *connUDPIPv6) WriteBatch(msgs Messages, flags int) (n int, err error) { //@ unfold acc(c.Mem(), _) // (VerifiedSCION) 1 is the length of the buffers of the messages in msgs - return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/) + return c.pconn.WriteBatch(msgs, flags) } // SetReadDeadline sets the read deadline associated with the endpoint. @@ -463,11 +463,11 @@ func (c *connUDPBase) Close() (err error) { // messages. // @ requires 0 < n // @ ensures len(res) == n -// @ ensures forall i int :: { &res[i] } 0 <= i && i < n ==> res[i].Mem(1) +// @ ensures forall i int :: { &res[i] } 0 <= i && i < n ==> res[i].Mem() // @ decreases func NewReadMessages(n int) (res Messages) { m := make(Messages, n) - //@ invariant forall j int :: { &m[j] } (0 <= j && j < i0) ==> m[j].Mem(1) + //@ invariant forall j int :: { &m[j] } (0 <= j && j < i0) ==> m[j].Mem() //@ invariant forall j int :: { &m[j] } (i0 <= j && j < len(m)) ==> acc(&m[j]) && m[j].N == 0 //@ invariant forall j int :: { m[j].Addr } (i0 <= j && j < len(m)) ==> m[j].Addr == nil //@ invariant forall j int :: { m[j].OOB } (i0 <= j && j < len(m)) ==> m[j].OOB == nil @@ -477,7 +477,7 @@ func NewReadMessages(n int) (res Messages) { m[i].Buffers = make([][]byte, 1) //@ fold slices.AbsSlice_Bytes(m[i].Buffers[0], 0, len(m[i].Buffers[0])) //@ fold slices.AbsSlice_Bytes(m[i].OOB, 0, len(m[i].OOB)) - //@ fold m[i].Mem(1) + //@ fold m[i].Mem() } return m } diff --git a/router/dataplane.go b/router/dataplane.go index 98d55daec..cc0051770 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -115,12 +115,12 @@ type BatchConn interface { // @ requires acc(Mem(), _) // @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> - // @ (msgs[i].Mem(1) && msgs[i].HasActiveBuffers(1)) + // @ (msgs[i].Mem() && msgs[i].HasActiveBuffers()) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err == nil ==> // @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> ( - // @ typeOf(msgs[i].GetAddr(1)) == type[*net.UDPAddr] && - // @ !msgs[i].HasWildcardPermAddr(1)) + // @ typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr] && + // @ !msgs[i].HasWildcardPermAddr()) // @ ensures err == nil ==> // @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) // @ ensures err != nil ==> err.ErrorMem() @@ -133,7 +133,7 @@ type BatchConn interface { WriteTo(b []byte, addr *net.UDPAddr) (n int, err error) // @ requires acc(Mem(), _) // @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> - // @ (acc(msgs[i].Mem(1), R50) && msgs[i].HasActiveBuffers(1)) + // @ (acc(msgs[i].Mem(), R50) && msgs[i].HasActiveBuffers()) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err != nil ==> err.ErrorMem() WriteBatch(msgs underlayconn.Messages, flags int) (n int, err error) @@ -707,25 +707,25 @@ func (d *DataPlane) Run(ctx context.Context) error { msgs := conn.NewReadMessages(inputBatchCnt) // @ socketspec.SplitPermMsgs(msgs) - // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(&msgs[i], 1/2) && msgs[i].MemWithoutHalf(1) - // @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) && msgs[i].HasActiveBuffers(1) + // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(&msgs[i], 1/2) && msgs[i].MemWithoutHalf() + // @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() && msgs[i].HasActiveBuffers() // @ decreases // @ outline ( // @ invariant len(msgs) != 0 ==> 0 <= i0 && i0 <= len(msgs) // @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> i0 <= i && i < len(msgs) ==> acc(&msgs[i], 1/2) - // @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> i0 <= i && i < len(msgs) ==> msgs[i].MemWithoutHalf(1) - // @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> 0 <= i && i < i0 ==> msgs[i].Mem(1) + // @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> i0 <= i && i < len(msgs) ==> msgs[i].MemWithoutHalf() + // @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> 0 <= i && i < i0 ==> msgs[i].Mem() // @ decreases len(msgs) - i0 for _, msg := range msgs /*@ with i0 @*/ { tmp := make([]byte, bufSize) // @ assert forall i int :: { &tmp[i] } 0 <= i && i < len(tmp) ==> acc(&tmp[i]) // @ fold sl.AbsSlice_Bytes(tmp, 0, len(tmp)) // @ assert msgs[i0] === msg - // @ unfold msgs[i0].MemWithoutHalf(1) + // @ unfold msgs[i0].MemWithoutHalf() msg.Buffers[0] = tmp - // @ fold msgs[i0].Mem(1) - // @ assert forall i int :: { &msgs[i] } 0 <= i && i < i0 ==> msgs[i].Mem(1) - // @ assert forall i int :: { &msgs[i] } i0 < i && i < len(msgs) ==> acc(&msgs[i], 1/2) && msgs[i].MemWithoutHalf(1) + // @ fold msgs[i0].Mem() + // @ assert forall i int :: { &msgs[i] } 0 <= i && i < i0 ==> msgs[i].Mem() + // @ assert forall i int :: { &msgs[i] } i0 < i && i < len(msgs) ==> acc(&msgs[i], 1/2) && msgs[i].MemWithoutHalf() } // @ ) // @ ensures writeMsgInv(writeMsgs) @@ -743,7 +743,7 @@ func (d *DataPlane) Run(ctx context.Context) error { // non-wildcard permissions: // @ invariant acc(&scmpErr) - // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) + // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() // @ invariant writeMsgInv(writeMsgs) // wildcard permissions: // @ invariant acc(&d, _) @@ -758,12 +758,12 @@ func (d *DataPlane) Run(ctx context.Context) error { // @ invariant unfolding acc(accBatchConn(d.external), _) in (ingressID in domain(d.external)) // @ invariant d.svc != nil // properties about messages: - // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].HasActiveBuffers(1) + // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].HasActiveBuffers() // properties about packetProcessor: // @ invariant processor.sInit() && processor.sInitD() === d for d.running { pkts, err := rd.ReadBatch(msgs) - // @ assert forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) + // @ assert forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() // @ assert err == nil ==> // @ forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) if err != nil { @@ -775,14 +775,14 @@ func (d *DataPlane) Run(ctx context.Context) error { continue } // @ assert pkts <= len(msgs) - // @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> !msgs[i].HasWildcardPermAddr(1) + // @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> !msgs[i].HasWildcardPermAddr() // @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) // (VerifiedSCION) using regular for loop instead of range loop to avoid unnecessary // complications with permissions // non-wildcard permissions: // @ invariant acc(&scmpErr) - // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) + // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() // @ invariant writeMsgInv(writeMsgs) // wildcard permissions: // @ invariant acc(&d, _) @@ -793,10 +793,10 @@ func (d *DataPlane) Run(ctx context.Context) error { // other properties: // @ invariant pkts <= len(msgs) // @ invariant 0 <= i0 && i0 <= pkts - // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].HasActiveBuffers(1) + // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].HasActiveBuffers() // @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> - // @ !msgs[i].HasWildcardPermAddr(1) - // @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> typeOf(msgs[i].GetAddr(1)) == type[*net.UDPAddr] + // @ !msgs[i].HasWildcardPermAddr() + // @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr] // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) // @ invariant d.forwardingMetrics != nil // @ invariant ingressID in domain(d.forwardingMetrics) @@ -824,7 +824,7 @@ func (d *DataPlane) Run(ctx context.Context) error { inputCounters.InputBytesTotal.Add(float64(p.N)) srcAddr := p.Addr.(*net.UDPAddr) - // @ unfold msgs[:pkts][i0].Mem(1) + // @ unfold msgs[:pkts][i0].Mem() // @ assert p.Buffers === msgs[:pkts][i0].Buffers // @ assert acc(&p.Buffers[0]) // @ assert p.N <= len(p.Buffers[0]) @@ -866,7 +866,7 @@ func (d *DataPlane) Run(ctx context.Context) error { // @ assert sl.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) // @ assert (m.Addr != nil ==> acc(m.Addr.Mem(), _)) // @ assert 0 <= m.N - // @ fold msgs[:pkts][i0].Mem(1) + // @ fold msgs[:pkts][i0].Mem() // @ unfold scmpErr.Mem() log.Debug("Error processing packet", "err", err) // @ assert acc(inputCounters.DroppedPacketsTotal.Mem(), _) @@ -876,7 +876,7 @@ func (d *DataPlane) Run(ctx context.Context) error { } if result.OutConn == nil { // e.g. BFD case no message is forwarded // @ assume false - // @ fold msgs[:pkts][i0].Mem(1) + // @ fold msgs[:pkts][i0].Mem() continue } @@ -887,7 +887,7 @@ func (d *DataPlane) Run(ctx context.Context) error { writeMsgs[0].Buffers[0] = result.OutPkt // @ assert acc(sl.AbsSlice_Bytes(writeMsgs[0].Buffers[0], 0, len(writeMsgs[0].Buffers[0])), 1 - R15) // @ writeMsgs[0].WildcardPerm = !addrAliasesPkt - // TODO: writeMsgs[0].Mem(1) should be an invariant + // TODO: writeMsgs[0].Mem() should be an invariant // @ writeMsgs[0].IsActive = true writeMsgs[0].Addr = nil if result.OutAddr != nil { // don't assign directly to net.Addr, typed nil! @@ -895,12 +895,12 @@ func (d *DataPlane) Run(ctx context.Context) error { } // @ assert acc(sl.AbsSlice_Bytes(writeMsgs[0].Buffers[0], 0, len(writeMsgs[0].Buffers[0])), 1 - R15) // @ assume !addrAliasesPkt - // @ fold acc(writeMsgs[0].Mem(1), R50) + // @ fold acc(writeMsgs[0].Mem(), R50) // @ assert forall i int :: { &writeMsgs[i] } 0 <= i && i < len(writeMsgs) ==> - // @ acc(writeMsgs[i].Mem(1), R50) + // @ acc(writeMsgs[i].Mem(), R50) _, err = result.OutConn.WriteBatch(writeMsgs, syscall.MSG_DONTWAIT) /// -- Checked until here // TODO: drop comment - // @ unfold acc(writeMsgs[0].Mem(1), R50) + // @ unfold acc(writeMsgs[0].Mem(), R50) // @ ghost if addrAliasesPkt { // @ apply acc(result.OutAddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(tmpBuf, 0, len(tmpBuf)), R15) // assert sl.AbsSlice_Bytes(tmpBuf, 0, len(tmpBuf)) @@ -915,7 +915,7 @@ func (d *DataPlane) Run(ctx context.Context) error { // @ assume false // @ fold writeMsgInv(writeMsgs) - // @ fold msgs[:pkts][i0].Mem(1) + // @ fold msgs[:pkts][i0].Mem() // @ assume false if err != nil { // @ requires err != nil && err.ErrorMem() diff --git a/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra index c4baae1ce..7f4b7e153 100644 --- a/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra +++ b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra @@ -1,6 +1,13 @@ // Specification for package "golang.org/x/net/internal/socket" // Based on file https://github.com/golang/net/blob/master/internal/socket/socket.go +// This file is specialized for the case where all instances m of message +// satisfy the property len(m.Buffers) == 1, which is the case in the router. +// The old file (socket.gobra.old) contains more general definitions, +// but this is unnecessary for the SCION router and requires us proving +// many additional lemmas, e.g., that the following is injective: +// forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> acc(&m.Buffers[i]) + // +gobra package socket @@ -42,13 +49,11 @@ type Message struct { WildcardPerm bool } -pred (m *Message) Mem(lenBuffers int) { +pred (m *Message) Mem() { acc(m) && - len(m.Buffers) == lenBuffers && - (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> acc(&m.Buffers[i])) && - (m.IsActive ==> - (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> - sl.AbsSlice_Bytes(m.Buffers[i], 0, len(m.Buffers[i])))) && + len(m.Buffers) == 1 && + acc(&m.Buffers[0]) && + (m.IsActive ==> sl.AbsSlice_Bytes(m.Buffers[0], 0, len(m.Buffers[0]))) && sl.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) && // typeOf(m.Addr) == type[*net.UDPAddr] && ((m.Addr != nil && m.IsActive && !m.WildcardPerm) ==> m.Addr.Mem()) && @@ -56,13 +61,11 @@ pred (m *Message) Mem(lenBuffers int) { 0 <= m.N } -pred (m *Message) MemWithoutHalf(lenBuffers int) { +pred (m *Message) MemWithoutHalf() { acc(m, 1/2) && - len(m.Buffers) == lenBuffers && - (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> acc(&m.Buffers[i])) && - (m.IsActive ==> - (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> - sl.AbsSlice_Bytes(m.Buffers[i], 0, len(m.Buffers[i])))) && + len(m.Buffers) == 1 && + acc(&m.Buffers[0]) && + (m.IsActive ==> sl.AbsSlice_Bytes(m.Buffers[0], 0, len(m.Buffers[0]))) && sl.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) && // typeOf(m.Addr) == type[*net.UDPAddr] && ((m.Addr != nil && m.IsActive && !m.WildcardPerm) ==> m.Addr.Mem()) && @@ -71,106 +74,107 @@ pred (m *Message) MemWithoutHalf(lenBuffers int) { } ghost -requires acc(m.Mem(lenBuffers), _) +requires acc(m.Mem(), _) decreases -pure func (m *Message) HasWildcardPermAddr(lenBuffers int) bool { - return unfolding acc(m.Mem(lenBuffers), _) in m.WildcardPerm +pure func (m *Message) HasWildcardPermAddr() bool { + return unfolding acc(m.Mem(), _) in m.WildcardPerm } ghost -requires acc(m.Mem(lenBuffers), _) +requires acc(m.Mem(), _) decreases -pure func (m *Message) HasActiveBuffers(lenBuffers int) bool { - return unfolding acc(m.Mem(lenBuffers), _) in m.IsActive +pure func (m *Message) HasActiveBuffers() bool { + return unfolding acc(m.Mem(), _) in m.IsActive } ghost -requires acc(m.Mem(lenBuffers), _) +requires acc(m.Mem(), _) decreases -pure func (m *Message) GetAddr(lenBuffers int) net.Addr { - return unfolding acc(m.Mem(lenBuffers), _) in m.Addr +pure func (m *Message) GetAddr() net.Addr { + return unfolding acc(m.Mem(), _) in m.Addr } ghost -requires acc(m.Mem(lenBuffers), _) +requires acc(m.Mem(), _) decreases -pure func (m *Message) GetMessage(lenBuffers int) Message { - return unfolding acc(m.Mem(lenBuffers), _) in *m +pure func (m *Message) GetMessage() Message { + return unfolding acc(m.Mem(), _) in *m } ghost -requires acc(m.MemWithoutHalf(lenBuffers), _) +requires acc(m.MemWithoutHalf(), _) decreases -pure func (m *Message) GetAddrWithoutHalf(lenBuffers int) net.Addr { - return unfolding acc(m.MemWithoutHalf(lenBuffers), _) in m.Addr +pure func (m *Message) GetAddrWithoutHalf() net.Addr { + return unfolding acc(m.MemWithoutHalf(), _) in m.Addr } ghost -requires acc(m.Mem(lenBuffers), _) -requires 0 <= i && i < lenBuffers +requires acc(m.Mem(), _) decreases -pure func (m *Message) GetBuffer(lenBuffers int, i int) []byte { - return unfolding acc(m.Mem(lenBuffers), _) in m.Buffers[i] +pure func (m *Message) GetBuffer() []byte { + return unfolding acc(m.Mem(), _) in m.Buffers[0] } +// TODO: drop // Only defined for the case where lenBuffers == 1 ghost -requires acc(m.Mem(1), _) +requires acc(m.Mem(), _) decreases pure func (m *Message) GetFstBuffer() []byte { - return unfolding acc(m.Mem(1), _) in m.Buffers[0] + return unfolding acc(m.Mem(), _) in m.Buffers[0] } +// TODO: drop // Only defined for the case where lenBuffers == 1 ghost -requires acc(m.Mem(1), _) +requires acc(m.Mem(), _) decreases pure func (m *Message) GetN() int { - return unfolding acc(m.Mem(1), _) in m.N + return unfolding acc(m.Mem(), _) in m.N } ghost -requires m.Mem(1) -ensures acc(m, 1/2) && m.MemWithoutHalf(1) -ensures old(m.GetAddr(1)) === m.GetAddrWithoutHalf(1) -ensures m.N == old(unfolding m.Mem(1) in m.N) -ensures m.Buffers === old(unfolding m.Mem(1) in m.Buffers) -ensures old(m.GetFstBuffer()) === unfolding m.MemWithoutHalf(1) in m.Buffers[0] +requires m.Mem() +ensures acc(m, 1/2) && m.MemWithoutHalf() +ensures old(m.GetAddr()) === m.GetAddrWithoutHalf() +ensures m.N == old(unfolding m.Mem() in m.N) +ensures m.Buffers === old(unfolding m.Mem() in m.Buffers) +ensures old(m.GetFstBuffer()) === unfolding m.MemWithoutHalf() in m.Buffers[0] ensures old(m.GetN()) == m.N -ensures old(m.HasWildcardPermAddr(1)) == m.WildcardPerm -ensures old(m.HasActiveBuffers(1)) == m.IsActive -ensures old(m.GetMessage(1)) === *m +ensures old(m.HasWildcardPermAddr()) == m.WildcardPerm +ensures old(m.HasActiveBuffers()) == m.IsActive +ensures old(m.GetMessage()) === *m decreases func (m *Message) SplitPerm() { - unfold m.Mem(1) - fold m.MemWithoutHalf(1) + unfold m.Mem() + fold m.MemWithoutHalf() } ghost -requires acc(m, 1/2) && m.MemWithoutHalf(1) -ensures m.Mem(1) -ensures m.GetAddr(1) === old(m.GetAddrWithoutHalf(1)) -ensures old(m.N) == unfolding m.Mem(1) in m.N -ensures m.GetFstBuffer() === old(unfolding m.MemWithoutHalf(1) in m.Buffers[0]) -ensures unfolding m.Mem(1) in m.Buffers === old(m.Buffers) +requires acc(m, 1/2) && m.MemWithoutHalf() +ensures m.Mem() +ensures m.GetAddr() === old(m.GetAddrWithoutHalf()) +ensures old(m.N) == unfolding m.Mem() in m.N +ensures m.GetFstBuffer() === old(unfolding m.MemWithoutHalf() in m.Buffers[0]) +ensures unfolding m.Mem() in m.Buffers === old(m.Buffers) ensures m.GetN() == old(m.N) -ensures m.HasWildcardPermAddr(1) == old(m.WildcardPerm) -ensures m.HasActiveBuffers(1) == old(m.IsActive) -ensures m.GetMessage(1) === old(*m) +ensures m.HasWildcardPermAddr() == old(m.WildcardPerm) +ensures m.HasActiveBuffers() == old(m.IsActive) +ensures m.GetMessage() === old(*m) decreases func (m *Message) CombinePerm() { - unfold m.MemWithoutHalf(1) - fold m.Mem(1) + unfold m.MemWithoutHalf() + fold m.Mem() } ghost -requires forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].Mem(1) -ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> acc(&msgs[j], 1/2) && msgs[j].MemWithoutHalf(1) -ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> old(msgs[j].GetMessage(1)) === msgs[j] -ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].WildcardPerm == old(msgs[j].HasWildcardPermAddr(1)) -ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].IsActive == old(msgs[j].HasActiveBuffers(1)) +requires forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].Mem() +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> acc(&msgs[j], 1/2) && msgs[j].MemWithoutHalf() +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> old(msgs[j].GetMessage()) === msgs[j] +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].WildcardPerm == old(msgs[j].HasWildcardPermAddr()) +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].IsActive == old(msgs[j].HasActiveBuffers()) decreases -func SplitPermMsgs(msgs []Message) { +func SplitPermMsgs(msgs []Message) /*{ invariant 0 <= i && i <= len(msgs) invariant forall j int :: { &msgs[j] } i <= j && j < len(msgs) ==> msgs[j].Mem(1) invariant forall j int :: { &msgs[j] } 0 <= j && j < i ==> acc(&msgs[j], 1/2) && msgs[j].MemWithoutHalf(1) @@ -185,4 +189,6 @@ func SplitPermMsgs(msgs []Message) { assert forall j int :: { &msgs[j] } 0 <= j && j < i ==> msgs[j].WildcardPerm == old(msgs[j].HasWildcardPermAddr(1)) assert msgs[i].WildcardPerm == old(msgs[i].HasWildcardPermAddr(1)) } -} \ No newline at end of file +} +*/ +// TODO: adapt \ No newline at end of file diff --git a/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra.old b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra.old new file mode 100644 index 000000000..e61f20e9f --- /dev/null +++ b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra.old @@ -0,0 +1,186 @@ +// Specification for package "golang.org/x/net/internal/socket" +// Based on file https://github.com/golang/net/blob/master/internal/socket/socket.go + +package socket + +import ( + "net" + + sl "github.com/scionproto/scion/verification/utils/slices" +) + + +// A Message represents an IO message. +type Message struct { + // When writing, the Buffers field must contain at least one + // byte to write. + // When reading, the Buffers field will always contain a byte + // to read. + Buffers [][]byte + + // OOB contains protocol-specific control or miscellaneous + // ancillary data known as out-of-band data. + OOB []byte + + // Addr specifies a destination address when writing. + // It can be nil when the underlying protocol of the raw + // connection uses connection-oriented communication. + // After a successful read, it may contain the source address + // on the received packet. + Addr net.Addr + + N int // # of bytes read or written from/to Buffers + NN int // # of bytes read or written from/to OOB + Flags int // protocol-specific information on the received message + + // (VerifiedSCION) the following are, morally, ghost fields: + // is it still ok to read the buffers and Addr of the Message? + IsActive bool + // do we have a fixed amount of perms to the Addr a wildcard amount? + WildcardPerm bool +} + +pred (m *Message) Mem(lenBuffers int) { + acc(m) && + len(m.Buffers) == lenBuffers && + (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> acc(&m.Buffers[i])) && + (m.IsActive ==> + (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> + sl.AbsSlice_Bytes(m.Buffers[i], 0, len(m.Buffers[i])))) && + sl.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) && + // typeOf(m.Addr) == type[*net.UDPAddr] && + ((m.Addr != nil && m.IsActive && !m.WildcardPerm) ==> m.Addr.Mem()) && + ((m.Addr != nil && m.IsActive && m.WildcardPerm) ==> acc(m.Addr.Mem(), _)) && + 0 <= m.N +} + +pred (m *Message) MemWithoutHalf(lenBuffers int) { + acc(m, 1/2) && + len(m.Buffers) == lenBuffers && + (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> acc(&m.Buffers[i])) && + (m.IsActive ==> + (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> + sl.AbsSlice_Bytes(m.Buffers[i], 0, len(m.Buffers[i])))) && + sl.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) && + // typeOf(m.Addr) == type[*net.UDPAddr] && + ((m.Addr != nil && m.IsActive && !m.WildcardPerm) ==> m.Addr.Mem()) && + ((m.Addr != nil && m.IsActive && m.WildcardPerm) ==> acc(m.Addr.Mem(), _)) && + 0 <= m.N +} + +ghost +requires acc(m.Mem(lenBuffers), _) +decreases +pure func (m *Message) HasWildcardPermAddr(lenBuffers int) bool { + return unfolding acc(m.Mem(lenBuffers), _) in m.WildcardPerm +} + +ghost +requires acc(m.Mem(lenBuffers), _) +decreases +pure func (m *Message) HasActiveBuffers(lenBuffers int) bool { + return unfolding acc(m.Mem(lenBuffers), _) in m.IsActive +} + +ghost +requires acc(m.Mem(lenBuffers), _) +decreases +pure func (m *Message) GetAddr(lenBuffers int) net.Addr { + return unfolding acc(m.Mem(lenBuffers), _) in m.Addr +} + +ghost +requires acc(m.Mem(lenBuffers), _) +decreases +pure func (m *Message) GetMessage(lenBuffers int) Message { + return unfolding acc(m.Mem(lenBuffers), _) in *m +} + +ghost +requires acc(m.MemWithoutHalf(lenBuffers), _) +decreases +pure func (m *Message) GetAddrWithoutHalf(lenBuffers int) net.Addr { + return unfolding acc(m.MemWithoutHalf(lenBuffers), _) in m.Addr +} + +ghost +requires acc(m.Mem(lenBuffers), _) +requires 0 <= i && i < lenBuffers +decreases +pure func (m *Message) GetBuffer(lenBuffers int, i int) []byte { + return unfolding acc(m.Mem(lenBuffers), _) in m.Buffers[i] +} + +// Only defined for the case where lenBuffers == 1 +ghost +requires acc(m.Mem(1), _) +decreases +pure func (m *Message) GetFstBuffer() []byte { + return unfolding acc(m.Mem(1), _) in m.Buffers[0] +} + +// Only defined for the case where lenBuffers == 1 +ghost +requires acc(m.Mem(1), _) +decreases +pure func (m *Message) GetN() int { + return unfolding acc(m.Mem(1), _) in m.N +} + +ghost +requires m.Mem(1) +ensures acc(m, 1/2) && m.MemWithoutHalf(1) +ensures old(m.GetAddr(1)) === m.GetAddrWithoutHalf(1) +ensures m.N == old(unfolding m.Mem(1) in m.N) +ensures m.Buffers === old(unfolding m.Mem(1) in m.Buffers) +ensures old(m.GetFstBuffer()) === unfolding m.MemWithoutHalf(1) in m.Buffers[0] +ensures old(m.GetN()) == m.N +ensures old(m.HasWildcardPermAddr(1)) == m.WildcardPerm +ensures old(m.HasActiveBuffers(1)) == m.IsActive +ensures old(m.GetMessage(1)) === *m +decreases +func (m *Message) SplitPerm() { + unfold m.Mem(1) + fold m.MemWithoutHalf(1) +} + +ghost +requires acc(m, 1/2) && m.MemWithoutHalf(1) +ensures m.Mem(1) +ensures m.GetAddr(1) === old(m.GetAddrWithoutHalf(1)) +ensures old(m.N) == unfolding m.Mem(1) in m.N +ensures m.GetFstBuffer() === old(unfolding m.MemWithoutHalf(1) in m.Buffers[0]) +ensures unfolding m.Mem(1) in m.Buffers === old(m.Buffers) +ensures m.GetN() == old(m.N) +ensures m.HasWildcardPermAddr(1) == old(m.WildcardPerm) +ensures m.HasActiveBuffers(1) == old(m.IsActive) +ensures m.GetMessage(1) === old(*m) +decreases +func (m *Message) CombinePerm() { + unfold m.MemWithoutHalf(1) + fold m.Mem(1) +} + +ghost +requires forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].Mem(1) +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> acc(&msgs[j], 1/2) && msgs[j].MemWithoutHalf(1) +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> old(msgs[j].GetMessage(1)) === msgs[j] +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].WildcardPerm == old(msgs[j].HasWildcardPermAddr(1)) +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].IsActive == old(msgs[j].HasActiveBuffers(1)) +decreases +func SplitPermMsgs(msgs []Message) { + invariant 0 <= i && i <= len(msgs) + invariant forall j int :: { &msgs[j] } i <= j && j < len(msgs) ==> msgs[j].Mem(1) + invariant forall j int :: { &msgs[j] } 0 <= j && j < i ==> acc(&msgs[j], 1/2) && msgs[j].MemWithoutHalf(1) + invariant forall j int :: { &msgs[j] } 0 <= j && j < i ==> msgs[j].WildcardPerm == old(msgs[j].HasWildcardPermAddr(1)) + invariant forall j int :: { &msgs[j] } 0 <= j && j < i ==> msgs[j].IsActive == old(msgs[j].HasActiveBuffers(1)) + invariant forall j int :: { &msgs[j] } 0 <= j && j < i ==> msgs[j] === old(msgs[j].GetMessage(1)) + invariant forall j int :: { &msgs[j] } i <= j && j < len(msgs) ==> msgs[j].GetMessage(1) === old(msgs[j].GetMessage(1)) + decreases len(msgs) - i + for i := 0; i < len(msgs); i++ { + assert forall j int :: { &msgs[j] }{ &msgs[j].WildcardPerm } 0 <= j && j < i ==> msgs[j].WildcardPerm == old(msgs[j].HasWildcardPermAddr(1)) + msgs[i].SplitPerm() + assert forall j int :: { &msgs[j] } 0 <= j && j < i ==> msgs[j].WildcardPerm == old(msgs[j].HasWildcardPermAddr(1)) + assert msgs[i].WildcardPerm == old(msgs[i].HasWildcardPermAddr(1)) + } +} \ No newline at end of file diff --git a/verification/dependencies/golang.org/x/net/internal/socket/socket_test.gobra b/verification/dependencies/golang.org/x/net/internal/socket/socket_test.gobra index c045b5147..21b652166 100644 --- a/verification/dependencies/golang.org/x/net/internal/socket/socket_test.gobra +++ b/verification/dependencies/golang.org/x/net/internal/socket/socket_test.gobra @@ -21,5 +21,7 @@ import "github.com/scionproto/scion/verification/utils/slices" func foldMem_test() { var m@ Message fold slices.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) - fold m.Mem(0) + m.Buffers = make([][]byte, 1) + fold slices.AbsSlice_Bytes(m.Buffers[0], 0, len(m.Buffers[0])) + fold m.Mem() } \ No newline at end of file diff --git a/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra b/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra index 39557db4d..38c0cf5e7 100644 --- a/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra +++ b/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra @@ -229,11 +229,11 @@ func NewRawConn(c net.PacketConn) (r *RawConn, err error) { trusted preserves acc(c.Mem(), _) preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> - (&ms[i]).Mem(lenBuffers) + (&ms[i]).Mem() ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> (0 <= n && n <= len(ms)) ensures err != nil ==> err.ErrorMem() -func (c *PacketConn) ReadBatch(ms []socket.Message, flags int, ghost lenBuffers int) (n int, err error) { +func (c *PacketConn) ReadBatch(ms []socket.Message, flags int) (n int, err error) { return c.payloadHandler.ReadBatch(ms, flags) } @@ -242,11 +242,11 @@ func (c *PacketConn) ReadBatch(ms []socket.Message, flags int, ghost lenBuffers // It returns the number of messages written on a successful write. trusted preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> - acc((&ms[i]).Mem(lenBuffers), R10) + acc((&ms[i]).Mem(), R10) preserves acc(c.Mem(), _) ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> 0 <= n && n <= len(ms) ensures err != nil ==> err.ErrorMem() -func (c *PacketConn) WriteBatch(ms []socket.Message, flags int, ghost lenBuffers int) (n int, err error) { +func (c *PacketConn) WriteBatch(ms []socket.Message, flags int) (n int, err error) { return c.payloadHandler.WriteBatch(ms, flags) } \ No newline at end of file diff --git a/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra b/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra index b5744863e..aee3a6c80 100644 --- a/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra +++ b/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra @@ -163,12 +163,12 @@ func (p *PacketConn) ExchangeWildcardPerm() (c net.PacketConn) // to len(ms). trusted preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> - (&ms[i]).Mem(lenBuffers) + (&ms[i]).Mem() preserves acc(c.Mem(), _) ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> (0 <= n && n <= len(ms)) ensures err != nil ==> err.ErrorMem() -func (c *PacketConn) ReadBatch(ms []socket.Message, flags int, ghost lenBuffers int) (n int, err error) { +func (c *PacketConn) ReadBatch(ms []socket.Message, flags int) (n int, err error) { return c.payloadHandler.ReadBatch(ms, flags) } @@ -176,11 +176,11 @@ func (c *PacketConn) ReadBatch(ms []socket.Message, flags int, ghost lenBuffers // WriteBatch writes a batch of messages. // It returns the number of messages written on a successful write. trusted -preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> acc((&ms[i]).Mem(lenBuffers), R10) +preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> acc((&ms[i]).Mem(), R10) preserves acc(c.Mem(), _) ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> 0 <= n && n <= len(ms) ensures err != nil ==> err.ErrorMem() -func (c *PacketConn) WriteBatch(ms []socket.Message, flags int, ghost lenBuffers int) (n int, err error) { +func (c *PacketConn) WriteBatch(ms []socket.Message, flags int) (n int, err error) { return c.payloadHandler.WriteBatch(ms, flags) } \ No newline at end of file