Merge branch 'master' into jcp19-patch-2

viperproject · Jan 7, 2025 · 562f4cf · 562f4cf
2 parents 3999cb0 + 84ea83b
commit 562f4cf
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 27 deletions.
diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go
@@ -223,8 +223,12 @@ func (s *SCION) NetworkFlow() (res gopacket.Flow) {
 // @ ensures   acc(s.Mem(ubuf), R0)
 // @ ensures   sl.Bytes(ubuf, 0, len(ubuf))
 // @ ensures   sl.Bytes(b.UBuf(), 0, len(b.UBuf()))
+// TODO: hide internal spec details
 // @ ensures   e == nil && s.HasOneHopPath(ubuf) ==>
-// @ 	len(b.UBuf()) == old(len(b.UBuf())) + s.MinimalSizeOfUbuf(ubuf)
+// @	len(b.UBuf()) == old(len(b.UBuf())) + unfolding acc(s.Mem(ubuf), R55) in
+// @		(CmnHdrLen + s.AddrHdrLenSpecInternal() + s.Path.LenSpec(ubuf[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen]))
+// @ ensures   e == nil && s.HasOneHopPath(ubuf) ==>
+// @	(unfolding acc(s.Mem(ubuf), R55) in CmnHdrLen + s.AddrHdrLenSpecInternal() + s.Path.LenSpec(ubuf[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen])) <= len(ubuf)
 // @ ensures   e != nil ==> e.ErrorMem()
 // post for IO:
 // @ ensures   e == nil && old(s.EqPathType(ubuf)) ==>

diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra
@@ -762,32 +762,6 @@ pure func (s *SCION) HasOneHopPath(ghost ub []byte) bool {
 	return unfolding acc(s.Mem(ub), _) in typeOf(s.Path) == type[*onehop.Path]
 }
 
-ghost
-requires acc(&s.DstAddrType, _) &&
-	acc(&s.SrcAddrType, _)      &&
-	acc(&s.HdrLen, _)           &&
-	acc(&s.Path, _)
-requires s.DstAddrType.Has3Bits() && s.SrcAddrType.Has3Bits()
-requires 0 <= CmnHdrLen+s.AddrHdrLenSpecInternal() &&
-	CmnHdrLen+s.AddrHdrLenSpecInternal() <= s.HdrLen*LineLen &&
-	s.HdrLen*LineLen <= len(ub)
-requires s.Path != nil
-requires acc(s.Path.Mem(ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen]), _)
-decreases
-pure func (s *SCION) MinimalSizeOfUbufWithOneHopOpenInv(ub []byte) int {
-	return let pathSlice := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
-		let pathLen := s.Path.LenSpec(pathSlice) in
-		CmnHdrLen + s.AddrHdrLenSpecInternal() + pathLen
-}
-
-ghost
-requires acc(s.Mem(ub), _)
-decreases
-pure func (s *SCION) MinimalSizeOfUbuf(ub []byte) int {
-	return unfolding acc(s.Mem(ub), _) in
-		s.MinimalSizeOfUbufWithOneHopOpenInv(ub)
-}
-
 ghost
 requires acc(s.Mem(ub), _)
 requires s.HasOneHopPath(ub)