Skip to content
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

Jump to bottom

Dependencies of Run #234

Merged
merged 12 commits into from
Nov 6, 2023
Merged

Dependencies of Run #234

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
0053850
deps of run
jcp19 Oct 30, 2023
7fc510d
Backup
jcp19 Oct 31, 2023
ee09594
backup
jcp19 Oct 31, 2023
4dd3a35
backup
jcp19 Oct 31, 2023
9130a53
Update private/underlay/conn/conn.go
jcp19 Oct 31, 2023
c0aed49
Update verification/dependencies/golang.org/x/net/internal/socket/soc…
jcp19 Oct 31, 2023
ccab565
add doc
jcp19 Nov 1, 2023
0d7ecaa
backup
jcp19 Nov 1, 2023
daf35d0
fix errors
jcp19 Nov 3, 2023
860af86
backup
jcp19 Nov 5, 2023
d8e7958
extract assumptions to separate file
jcp19 Nov 5, 2023
7738270
tiny tweak
jcp19 Nov 5, 2023
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
53 changes: 23 additions & 30 deletions private/underlay/conn/conn.go
View file
Open in desktop
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(), _)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A bit of a nitpick but I would change this to requires (and same for similar cases below). I find it a bit confusing since it is not really preserved.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was gonna change this, but decided against. If one expands the definition of _, I would argue that it is preserved:

preserves exists p perm :: 0 < p && p < perm(c.Mem()) && acc(c.Mem(), p)

// @ 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
Open in desktop
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
5 changes: 1 addition & 4 deletions router/dataplane.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,10 +189,7 @@ type scmpError struct {
}

// @ preserves e.ErrorMem()
// (VerifiedSCION): Gobra can't prove termination here because we call Error
// to the result of New and right now it is not able to prove that this will
// not be a new scmpError. We assume it.
// @ decreases _
// @ decreases e.Size()
func (e scmpError) Error() string {
// @ unfold e.ErrorMem()
// @ defer fold e.ErrorMem()
Expand Down
27 changes: 17 additions & 10 deletions router/dataplane_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -151,31 +151,38 @@ pred (err scmpError) ErrorMem() {
err.Cause != nil ==> err.Cause.ErrorMem()
}

// Currently assumed, as Gobra cannot currently prove termination
// of the code below
ghost
trusted
pure
decreases
requires acc(err.ErrorMem(), _)
decreases err.Size()
func (err scmpError) IsDuplicableMem() bool {
return err != nil? err.cause.IsDuplicableMem() : true
return unfolding acc(err.ErrorMem(), _) in
err.Cause == nil || err.Cause.IsDuplicableMem()
}

// Currently assumed, as Gobra cannot currently prove termination
// of the code below
ghost
trusted
preserves err.ErrorMem()
ensures err.IsDuplicableMem() ==> err.ErrorMem()
decreases
decreases err.Size()
func (err scmpError) Duplicate() {
if err.IsDuplicableMem() {
unfold err.ErrorMem()
err.cause.Duplicate()
if err.Cause != nil {
err.Cause.Duplicate()
}
fold err.ErrorMem()
}
}

ghost
requires acc(e.ErrorMem(), _)
ensures 0 <= res
pure func (e scmpError) Size() (res int) {
return unfolding e.ErrorMem() in 1 + (e.Cause == nil ?
0 :
e.Cause.Size())
}

scmpError implements error

type offsetPair struct {
Expand Down
Loading
Loading