scion.gobra: try to verify method that takes too long

.github/workflows/test.yml

@@ -22,6 +22,6 @@ jobs:
         with:
           imageVersion: verified-scion-preview-without-selective
           packageLocation: gobra
-          globalTimeout: 4h
-          packageTimeout: 2h
+          globalTimeout: 6h
+          packageTimeout: 4h
 

gobra/lib/slayers/scion.gobra

@@ -677,24 +677,33 @@ func (s *SCION) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (errRes
 		return serrors.New("packet is shorter than the common header length",
 			"min", CmnHdrLen, "actual", len(data))
 	}
-	firstLine := binary.BigEndian.Uint32(data[:4])
+	assert &data[0:4][0] == &data[0]
+	assert &data[0:4][1] == &data[1]
+	assert &data[0:4][2] == &data[2]
+	assert &data[0:4][3] == &data[3]
+	firstLine := binary.BigEndian.Uint32(data[0:4])
 	s.Version = uint8(firstLine >> 28)
 	s.TrafficClass = uint8((firstLine >> 20) & 0xFF)
 	s.FlowID = firstLine & 0xFFFFF
 	s.NextHdr = common.L4ProtocolType(data[4])
 	s.HdrLen = data[5]
+	assert &data[6:8][0] == &data[6]
+	assert &data[6:8][1] == &data[7]
 	s.PayloadLen = binary.BigEndian.Uint16(data[6:8])
 	s.PathType = PathType(data[8])
 	s.DstAddrType = AddrType(data[9] >> 6)
 	s.DstAddrLen = AddrLen(data[9] >> 4 & 0x3)
 	s.SrcAddrType = AddrType(data[9] >> 2 & 0x3)
 	s.SrcAddrLen = AddrLen(data[9] & 0x3)
 
+	assume false
 	// Decode address header.
+	assert forall i int :: 0 <= i && i < len(data[CmnHdrLen:]) ==> &data[CmnHdrLen:][i] == &data[CmnHdrLen+i]
 	if err := s.DecodeAddrHdr(data[CmnHdrLen:]); err != nil {
 		df.SetTruncated()
 		return err
 	}
+	/*
 	addrHdrLen := s.AddrHdrLen()
 	offset := CmnHdrLen + addrHdrLen
 
@@ -753,17 +762,20 @@ func (s *SCION) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (errRes
 }
 */
 
-
 // (joao) ignored for now, not used in this file
-/* func decodeSCION(data []byte, pb gopacket.PacketBuilder) error {
+requires pb.Mem()
+requires forall i int :: 0 <= i && i < len(data) ==> acc(&data[i])
+func decodeSCION(data []byte, pb gopacket.PacketBuilder) error /* {
 	scn := &SCION{}
 	err := scn.DecodeFromBytes(data, pb)
 	if err != nil {
 		return err
 	}
 	pb.AddLayer(scn)
 	pb.SetNetworkLayer(scn)
-	return pb.NextDecoder(scionNextLayerType(scn.NextHdr))
+	// rewrote the following
+	// return pb.NextDecoder(scionNextLayerType(scn.NextHdr))
+	return pb.NextDecoder(s.NextLayerType())
 }
 */
 
@@ -861,10 +873,10 @@ func (s *SCION) SetDstAddr(dst net.Addr) (ret error) {
 	return err
 }
 
+// (joao) Verified
 // SetSrcAddr sets the source address and updates the DstAddrLen/Type fields accordingly.
 // SetSrcAddr takes ownership of src and callers should not write to it after calling SetSrcAddr.
 // Changes to src might leave the layer in an inconsistent state.
-// (joao) Verified
 requires s.Mem() && src.Mem()
 ensures ret == nil ==> s.Mem()
 func (s *SCION) SetSrcAddr(src net.Addr) (ret error) {
@@ -923,6 +935,7 @@ func parseAddr(addrType AddrType, addrLen AddrLen, raw []byte) (resAddr net.Addr
 		"type", addrType, "len", addrLen)
 }
 
+// TODO: verify with assumption
 // (joao) Assumed
 // (joao) Verify this next
 // (joao) requires implementation proof that IPAddr implements Addr to verify the body
@@ -1009,14 +1022,14 @@ func (s *SCION) SerializeAddrHdr(buf []byte) (err error) {
 	return nil
 }
 
-// (joao) Assumed
-// (joao) function not present in the original code
+// (joao) verification does not terminate
+// (joao) function introduced for verification purposes
 preserves acc(s.Mem(), 1/1000)
 preserves forall i int :: 0 <= i && i < len(b) ==> acc(&b[i])
 ensures (old(s.getRawPkt()) == s.getRawPkt()) && (old(s.getRawScionPath()) == s.getRawScionPath())
 decreases
 func copyRawDstAddr(s *SCION, b []byte) /* {
-	// (joao) without this assumption, verification does not terminate
+	// (joao) verification does not terminate
 	assume false
 	unfold acc(s.Mem(), 1/1000)
 	unfold acc(verifyutils.BytesAcc(s.RawDstAddr), 1/10000)
@@ -1027,15 +1040,13 @@ func copyRawDstAddr(s *SCION, b []byte) /* {
 }
 */
 
-// (joao) Assumed
-// (joao) function not present in the original code
+// (joao) verification does not terminate
+// (joao) function introduced for verification purposes
 preserves acc(s.Mem(), 1/1000)
 preserves forall i int :: 0 <= i && i < len(b) ==> acc(&b[i])
 ensures (old(s.getRawPkt()) == s.getRawPkt()) && (old(s.getRawScionPath()) == s.getRawScionPath())
 decreases
 func copyRawSrcAddr(s *SCION, b []byte) /* {
-	// (joao) without this assumption, verification does not terminate
-	assume false
 	unfold acc(s.Mem(), 1/1000)
 	unfold acc(verifyutils.BytesAcc(s.RawSrcAddr), 1/10000)
 	verifyutils.OutlineMemorySafeCopy(b, s.RawSrcAddr)
@@ -1044,17 +1055,16 @@ func copyRawSrcAddr(s *SCION, b []byte) /* {
 }
 */
 
-// (joao) TODO: remake this spec
-// (joao) Assumed for now
+// (joao) Verification takes too long
 // DecodeAddrHdr decodes the destination and source ISD-AS-Host address triples from the provided
 // buffer. The caller must ensure that the correct address types and lengths are set in the SCION
 // layer, otherwise the results of this method are undefined.
 requires acc(s) && validAddrLen(s.SrcAddrLen) && validAddrLen(s.DstAddrLen)
 requires forall i int :: 0 <= i && i < len(data) ==> acc(&data[i])
 ensures  acc(s) && validAddrLen(s.SrcAddrLen) && validAddrLen(s.DstAddrLen)
-// (joao) uncommenting the following post-condition increases verification time from ~4min to ~26
-// ensures  res == nil ==> (verifyutils.BytesAcc(s.RawSrcAddr) && verifyutils.BytesAcc(s.RawDstAddr) && validSrcAddr(s) && validDstAddr(s))
-func (s *SCION) DecodeAddrHdr(data []byte) (res error) /* {
+ensures  res == nil ==> verifyutils.BytesAcc(s.RawSrcAddr) && len(s.RawSrcAddr) == addrBytes(s.SrcAddrLen)
+ensures  res == nil ==> verifyutils.BytesAcc(s.RawDstAddr) && len(s.RawDstAddr) == addrBytes(s.DstAddrLen)
+func (s *SCION) DecodeAddrHdr(data []byte) (res error) {
 	assert addrBytes(s.DstAddrLen) >= 0
 	assert addrBytes(s.SrcAddrLen) >= 0
 	// (joao) inline calls to s.AddrHdrLen due to missing s.Mem() permission
@@ -1066,9 +1076,7 @@ func (s *SCION) DecodeAddrHdr(data []byte) (res error) /* {
 		return serrors.New("provided buffer is too small", "expected", 2*addr.IABytes + addrBytes(s.DstAddrLen) + addrBytes(s.SrcAddrLen),
 			"actual", len(data))
 	}
-	assume false
 	offset := 0
-	unfold s.Mem()
 	assert len(data[offset:]) == len(data)
 	assert forall i int :: 0 <= i && i < len(data[offset:]) ==> &(data[offset:])[i] == &data[offset + i]
 	s.DstIA = addr.IAFromRaw(data[offset:])
@@ -1080,17 +1088,15 @@ func (s *SCION) DecodeAddrHdr(data []byte) (res error) /* {
 	dstAddrBytes := addrBytes(s.DstAddrLen)
 	srcAddrBytes := addrBytes(s.SrcAddrLen)
 	assert len(data) >= 2 * addr.IABytes + srcAddrBytes + dstAddrBytes
-	assume false
-	assert len(data[offset:]) == len(data) - offset
-	assert forall i int :: 0 <= i && i < len(data[offset:]) ==> &(data[offset:])[i] == &data[offset + i]
+	assert forall i int :: 0 <= i && i < len(data[offset:offset+dstAddrBytes]) ==> &(data[offset:offset+dstAddrBytes])[i] == &data[offset + i]
 	s.RawDstAddr = data[offset : offset+dstAddrBytes]
+	fold verifyutils.BytesAcc(s.RawDstAddr)
 	offset += dstAddrBytes
-	assert len(data[offset:]) == len(data) - offset
-	assert forall i int :: 0 <= i && i < len(data[offset:]) ==> &(data[offset:])[i] == &data[offset + i]
+	assert forall i int :: 0 <= i && i < len(data[offset:offset+srcAddrBytes]) ==> &(data[offset:offset+srcAddrBytes])[i] == &data[offset + i]
 	s.RawSrcAddr = data[offset : offset+srcAddrBytes]
+	fold verifyutils.BytesAcc(s.RawSrcAddr)
 	return nil
 }
-*/
 
 // (joao) Verified
 // computeChecksum computes the checksum with the SCION pseudo header.