Verify core of Run method

pkg/slayers/scion.go

@@ -575,18 +575,18 @@ func scionNextLayerTypeL4(t L4ProtocolType) gopacket.LayerType {
 // from the underlaying layer data. Changing the net.Addr object might lead to inconsistent layer
 // information and thus should be treated read-only. Instead, SetDstAddr should be used to update
 // the destination address.
-// @ requires  acc(&s.DstAddrType, R20) && acc(&s.RawDstAddr, R20)
-// @ requires  s.DstAddrType == T4Svc ==> len(s.RawDstAddr) >= addr.HostLenSVC
-// @ requires  acc(sl.AbsSlice_Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
-// @ ensures   acc(&s.DstAddrType, R20) && acc(&s.RawDstAddr, R20)
-// @ ensures   acc(sl.AbsSlice_Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
-// @ ensures   err == nil ==> (s.DstAddrType == T16Ip ==> typeOf(res) == *net.IPAddr)
-// @ ensures   err == nil ==> (s.DstAddrType == T16Ip ==> (acc(res.(*net.IPAddr)) && s.RawDstAddr === []byte(res.(*net.IPAddr).IP)))
-// @ ensures   err == nil ==> (s.DstAddrType == T4Ip ==>  typeOf(res) == *net.IPAddr)
-// @ ensures   err == nil ==> (s.DstAddrType == T4Ip ==> (acc(res.(*net.IPAddr)) && s.RawDstAddr === []byte(res.(*net.IPAddr).IP)))
-// @ ensures   err == nil ==> (s.DstAddrType == T4Svc ==> typeOf(res) == addr.HostSVC)
-// @ ensures   err == nil == (s.DstAddrType == T4Ip || s.DstAddrType == T4Svc || s.DstAddrType == T16Ip)
-// @ ensures   err != nil ==> err.ErrorMem()
+// @ requires acc(&s.DstAddrType, R20) && acc(&s.RawDstAddr, R20)
+// @ requires s.DstAddrType == T4Svc ==> len(s.RawDstAddr) >= addr.HostLenSVC
+// @ requires acc(sl.AbsSlice_Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R15)
+// @ ensures  acc(&s.DstAddrType, R20) && acc(&s.RawDstAddr, R20)
+// @ ensures  err == nil ==> acc(res.Mem(), R15)
+// @ ensures  err == nil ==> typeOf(res) == *net.IPAddr || typeOf(res) == addr.HostSVC
+// @ ensures  err == nil ==>
+// @ 	let rawDstAddr := s.RawDstAddr in
+// @ 	(acc(res.Mem(), R15) --* acc(sl.AbsSlice_Bytes(rawDstAddr, 0, len(rawDstAddr)), R15))
+// @ ensures  err != nil ==>
+// @ 	acc(sl.AbsSlice_Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R15)
+// @ ensures  err != nil ==> err.ErrorMem()
 // @ decreases
 func (s *SCION) DstAddr() (res net.Addr, err error) {
 	return parseAddr(s.DstAddrType, s.RawDstAddr)
@@ -598,15 +598,15 @@ func (s *SCION) DstAddr() (res net.Addr, err error) {
 // address.
 // @ requires  acc(&s.SrcAddrType, R20) && acc(&s.RawSrcAddr, R20)
 // @ requires  s.SrcAddrType == T4Svc ==> len(s.RawSrcAddr) >= addr.HostLenSVC
-// @ requires  acc(sl.AbsSlice_Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
+// @ requires  acc(sl.AbsSlice_Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R15)
 // @ ensures   acc(&s.SrcAddrType, R20) && acc(&s.RawSrcAddr, R20)
-// @ ensures   acc(sl.AbsSlice_Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
-// @ ensures   err == nil ==> (s.SrcAddrType == T16Ip ==> typeOf(res) == *net.IPAddr)
-// @ ensures   err == nil ==> (s.SrcAddrType == T16Ip ==> (acc(res.(*net.IPAddr)) && s.RawSrcAddr === []byte(res.(*net.IPAddr).IP)))
-// @ ensures   err == nil ==> (s.SrcAddrType == T4Ip ==>  typeOf(res) == *net.IPAddr)
-// @ ensures   err == nil ==> (s.SrcAddrType == T4Ip ==> (acc(res.(*net.IPAddr)) && s.RawSrcAddr === []byte(res.(*net.IPAddr).IP)))
-// @ ensures   err == nil ==> (s.SrcAddrType == T4Svc ==> typeOf(res) == addr.HostSVC)
-// @ ensures   err == nil == (s.SrcAddrType == T4Ip || s.SrcAddrType == T4Svc || s.SrcAddrType == T16Ip)
+// @ ensures   err == nil ==> acc(res.Mem(), R15)
+// @ ensures  err == nil ==> typeOf(res) == *net.IPAddr || typeOf(res) == addr.HostSVC
+// @ ensures   err == nil ==>
+// @ 	let rawSrcAddr := s.RawSrcAddr in
+// @ 	(acc(res.Mem(), R15) --* acc(sl.AbsSlice_Bytes(rawSrcAddr, 0, len(rawSrcAddr)), R15))
+// @ ensures   err != nil ==>
+// @ 	acc(sl.AbsSlice_Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R15)
 // @ ensures   err != nil ==> err.ErrorMem()
 // @ decreases
 func (s *SCION) SrcAddr() (res net.Addr, err error) {
@@ -687,28 +687,43 @@ func (s *SCION) SetSrcAddr(src net.Addr /*@, ghost wildcard bool @*/) (res error
 	return err
 }
 
-// @ requires  addrType == T4Svc ==> len(raw) >= addr.HostLenSVC
-// @ preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R20)
-// @ ensures   err == nil ==> (addrType == T16Ip ==> typeOf(res) == *net.IPAddr)
-// @ ensures   err == nil ==> (addrType == T16Ip ==> (acc(res.(*net.IPAddr)) && raw === []byte(res.(*net.IPAddr).IP)))
-// @ ensures   err == nil ==> (addrType == T4Ip ==> typeOf(res) == *net.IPAddr)
-// @ ensures   err == nil ==> (addrType == T4Ip ==> (acc(res.(*net.IPAddr)) && raw === []byte(res.(*net.IPAddr).IP)))
-// @ ensures   err == nil ==> (addrType == T4Svc ==> typeOf(res) == addr.HostSVC)
-// @ ensures   err == nil == (addrType == T4Ip || addrType == T4Svc || addrType == T16Ip)
-// @ ensures   err != nil ==> err.ErrorMem()
+// @ requires addrType == T4Svc ==> len(raw) >= addr.HostLenSVC
+// @ requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)
+// @ ensures  err == nil ==> acc(res.Mem(), R15)
+// @ ensures  err == nil ==> typeOf(res) == *net.IPAddr || typeOf(res) == addr.HostSVC
+// @ ensures  err == nil ==>
+// @ 	(acc(res.Mem(), R15) --* acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15))
+// @ ensures  err != nil ==> acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)
+// @ ensures  err != nil ==> err.ErrorMem()
 // @ decreases
 func parseAddr(addrType AddrType, raw []byte) (res net.Addr, err error) {
 	switch addrType {
 	case T4Ip:
 		verScionTmp := &net.IPAddr{IP: net.IP(raw)}
+		// @ unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)
+		// @ fold acc(verScionTmp.Mem(), R15)
+		// @ package (acc((net.Addr)(verScionTmp).Mem(), R15) --* acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)) {
+		// @ 	assert acc(&verScionTmp.IP, R50) && verScionTmp.IP === raw
+		// @ 	unfold acc(verScionTmp.Mem(), R15)
+		// @ 	fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)
+		// @ }
 		return verScionTmp, nil
 	case T4Svc:
-		// @ unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R20)
+		// @ unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)
 		verScionTmp := addr.HostSVC(binary.BigEndian.Uint16(raw[:addr.HostLenSVC]))
-		// @ fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R20)
+		// @ fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)
+		// @ fold acc(verScionTmp.Mem(), R15)
+		// @ package (acc((net.Addr)(verScionTmp).Mem(), R15) --* acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)) { }
 		return verScionTmp, nil
 	case T16Ip:
 		verScionTmp := &net.IPAddr{IP: net.IP(raw)}
+		// @ unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)
+		// @ fold acc(verScionTmp.Mem(), R15)
+		// @ package (acc((net.Addr)(verScionTmp).Mem(), R15) --* acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)) {
+		// @ 	assert acc(&verScionTmp.IP, R50) && verScionTmp.IP === raw
+		// @ 	unfold acc(verScionTmp.Mem(), R15)
+		// @ 	fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)
+		// @ }
 		return verScionTmp, nil
 	}
 	return nil, serrors.New("unsupported address type/length combination",

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() && res[i].GetAddr() == nil
 // @ 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() && m[j].GetAddr() == nil
 	//@ 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
 }