Skip to content

Commit

Permalink
Dependencies of Run (#234)
Browse files Browse the repository at this point in the history 
* deps of run

* Backup

* backup

* backup

* Update private/underlay/conn/conn.go

* Update verification/dependencies/golang.org/x/net/internal/socket/socket.gobra

* add doc

* backup

* fix errors

* backup

* extract assumptions to separate file

* tiny tweak
  • Loading branch information
@jcp19
jcp19 authored Nov 6, 2023
1 parent 10676f7 commit fee6345
Show file tree
Hide file tree
Showing 16 changed files with 368 additions and 283 deletions.
1 change: 1 addition & 0 deletions .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,3 +100,4 @@ target
*.gobrafied
*.internal
.devcontainer
.metals
53 changes: 23 additions & 30 deletions private/underlay/conn/conn.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,29 +44,29 @@ type Messages []ipv4.Message
type Conn interface {
//@ pred Mem()
// (VerifiedSCION) Reads a message to b. Returns the number of read bytes.
//@ preserves Mem()
//@ requires acc(Mem(), _)
//@ preserves slices.AbsSlice_Bytes(b, 0, len(b))
//@ ensures err == nil ==> 0 <= n && n <= len(b)
//@ ensures err == nil ==> acc(addr.Mem(), _)
//@ ensures err != nil ==> err.ErrorMem()
ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error)
//@ preserves Mem()
//@ requires acc(Mem(), _)
//@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> m[i].Mem(1)
//@ ensures err == nil ==> 0 <= n && n <= len(m)
//@ ensures err != nil ==> err.ErrorMem()
ReadBatch(m Messages) (n int, err error)
//@ preserves Mem()
//@ requires acc(Mem(), _)
//@ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R10)
//@ ensures err == nil ==> 0 <= n && n <= len(b)
//@ ensures err != nil ==> err.ErrorMem()
Write(b []byte) (n int, err error)
//@ requires acc(u.Mem(), _)
//@ preserves Mem()
//@ requires acc(Mem(), _)
//@ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R10)
//@ ensures err == nil ==> 0 <= n && n <= len(b)
//@ ensures err != nil ==> err.ErrorMem()
WriteTo(b []byte, u *net.UDPAddr) (n int, err error)
//@ preserves Mem()
//@ requires acc(Mem(), _)
//@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> acc(m[i].Mem(1), R10)
//@ ensures err == nil ==> 0 <= n && n <= len(m)
//@ ensures err != nil ==> err.ErrorMem()
Expand Down Expand Up @@ -163,25 +163,23 @@ 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.
// @ preserves c.Mem()
// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1)
// @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs)
// @ ensures errRet != nil ==> errRet.ErrorMem()
func (c *connUDPIPv4) ReadBatch(msgs Messages) (nRet int, errRet error) {
//@ unfold c.Mem()
//@ 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 @*/)
//@ fold c.Mem()
return n, err
}

// @ preserves c.Mem()
// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), 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 c.Mem()
//@ defer fold c.Mem()
//@ unfold acc(c.Mem(), _)
// (VerifiedSCION) 1 is the length of the buffers of the messages in msgs
return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/)
}
Expand Down Expand Up @@ -239,25 +237,23 @@ 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.
// @ preserves c.Mem()
// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1)
// @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs)
// @ ensures errRet != nil ==> errRet.ErrorMem()
func (c *connUDPIPv6) ReadBatch(msgs Messages) (nRet int, errRet error) {
//@ unfold c.Mem()
//@ 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 @*/)
//@ fold c.Mem()
return n, err
}

// @ preserves c.Mem()
// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), 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 c.Mem()
//@ defer fold c.Mem()
//@ unfold acc(c.Mem(), _)
// (VerifiedSCION) 1 is the length of the buffers of the messages in msgs
return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/)
}
Expand Down Expand Up @@ -398,38 +394,35 @@ func (cc *connUDPBase) initConnUDP(network string, laddr, raddr *net.UDPAddr, cf
return nil
}

// @ preserves c.Mem()
// @ preserves acc(c.Mem(), _)
// @ preserves slices.AbsSlice_Bytes(b, 0, len(b))
// @ preserves unfolding c.Mem() in c.conn == underlyingConn
// @ preserves unfolding acc(c.Mem(), _) in c.conn == underlyingConn
// @ ensures err == nil ==> 0 <= n && n <= len(b)
// @ ensures err == nil ==> acc(addr.Mem(), _)
// @ ensures err != nil ==> err.ErrorMem()
func (c *connUDPBase) ReadFrom(b []byte /*@, ghost underlyingConn *net.UDPConn @*/) (n int, addr *net.UDPAddr, err error) {
//@ unfold c.Mem()
//@ defer fold c.Mem()
//@ unfold acc(c.Mem(), _)
return c.conn.ReadFromUDP(b)
}

// @ preserves c.Mem()
// @ preserves acc(c.Mem(), _)
// @ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
// @ preserves unfolding c.Mem() in c.conn == underlyingConn
// @ preserves unfolding acc(c.Mem(), _) in c.conn == underlyingConn
// @ ensures err == nil ==> 0 <= n && n <= len(b)
// @ ensures err != nil ==> err.ErrorMem()
func (c *connUDPBase) Write(b []byte /*@, ghost underlyingConn *net.UDPConn @*/) (n int, err error) {
//@ unfold c.Mem()
//@ defer fold c.Mem()
//@ unfold acc(c.Mem(), _)
return c.conn.Write(b)
}

// @ requires acc(dst.Mem(), _)
// @ preserves c.Mem()
// @ preserves unfolding c.Mem() in c.conn == underlyingConn
// @ preserves acc(c.Mem(), _)
// @ preserves unfolding acc(c.Mem(), _) in c.conn == underlyingConn
// @ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
// @ ensures err == nil ==> 0 <= n && n <= len(b)
// @ ensures err != nil ==> err.ErrorMem()
func (c *connUDPBase) WriteTo(b []byte, dst *net.UDPAddr /*@, ghost underlyingConn *net.UDPConn @*/) (n int, err error) {
//@ unfold c.Mem()
//@ defer fold c.Mem()
//@ unfold acc(c.Mem(), _)
if c.Remote != nil {
return c.conn.Write(b)
}
Expand Down Expand Up @@ -475,7 +468,7 @@ func (c *connUDPBase) Close() (err error) {
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] } (i0 <= j && j < len(m)) ==> acc(&m[j])
//@ 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
//@ decreases len(m) - i
Expand Down
97 changes: 30 additions & 67 deletions private/underlay/conn/conn_spec.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,74 +65,55 @@ pred (c *Config) Mem() {
/** Lift methods in *connUDPBase to *connUDPIPv4 **/
*connUDPIPv4 implements Conn

preserves c.Mem()
requires acc(c.Mem(), _)
preserves slices.AbsSlice_Bytes(b, 0, len(b))
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err == nil ==> acc(addr.Mem(), _)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv4) ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv4.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, addr1, err1 := c.connUDPBase.ReadFrom(b, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, addr1, err1
}

preserves c.Mem()
preserves acc(c.Mem(), _)
preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv4) Write(b []byte) (n int, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv4.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, err1 := c.connUDPBase.Write(b, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, err1
}

requires acc(dst.Mem(), _)
preserves c.Mem()
preserves acc(c.Mem(), _)
preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv4) WriteTo(b []byte, dst *net.UDPAddr) (n int, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv4.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, err1 := c.connUDPBase.WriteTo(b, dst, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, err1
}

Expand Down Expand Up @@ -169,74 +150,56 @@ func (c *connUDPIPv4) Close() (err error) {
/** Lift methods in *connUDPBase to *connUDPIPv6 **/
*connUDPIPv6 implements Conn

preserves c.Mem()
preserves acc(c.Mem(), _)
preserves slices.AbsSlice_Bytes(b, 0, len(b))
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err == nil ==> acc(addr.Mem(), _)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv6) ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv6.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, addr1, err1 := c.connUDPBase.ReadFrom(b, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, addr1, err1
}

preserves c.Mem()
preserves acc(c.Mem(), _)
preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv6) Write(b []byte) (n int, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv6.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, err1 := c.connUDPBase.Write(b, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, err1
}

requires acc(dst.Mem(), _)
preserves c.Mem()
preserves acc(c.Mem(), _)
preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv6) WriteTo(b []byte, dst *net.UDPAddr) (n int, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv6.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, err1 := c.connUDPBase.WriteTo(b, dst, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, err1
}

Expand Down
Loading

0 comments on commit fee6345

Please sign in to comment.