From 84ea83b6a45584e0ed27719dfa05ce5c0cb095ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 7 Jan 2025 16:38:05 +0100 Subject: [PATCH] Revert "simplify post of SCION.SerializeTo" This reverts commit 2fcf7b2c39a1bdba8ad6f02df16a1a51bd438a9a. --- pkg/slayers/scion.go | 6 +++++- pkg/slayers/scion_spec.gobra | 26 -------------------------- 2 files changed, 5 insertions(+), 27 deletions(-) diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index bc3c7d7b1..e3de3e8f3 100644 --- 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 index 4b446e946..a66bce011 100644 --- 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)