Refactor parts of scion_spec.gobra for proof stability (#389)

* backup * cleanup * Update pkg/slayers/scion.go * Update pkg/slayers/scion_spec.gobra
viperproject · Jan 7, 2025 · ced08ce · ced08ce
1 parent f27ca87
commit ced08ce
Show file tree

Hide file tree

Showing 3 changed files with 46 additions and 11 deletions.
diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go
@@ -223,12 +223,8 @@ 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())) + 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)
+// @ 	len(b.UBuf()) == old(len(b.UBuf())) + s.MinSizeOfUbufWithOneHop(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
@@ -183,7 +183,7 @@ pred (s *SCION) Mem(ubuf []byte) {
 	// helpful facts for other methods:
 	// - for router::updateScionLayer:
 	(typeOf(s.Path) == type[*onehop.Path] ==>
-		CmnHdrLen + s.AddrHdrLenSpecInternal() + s.Path.LenSpec(ubuf[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen]) <= len(ubuf))
+		s.ValidSizeOhpUbOpenInv(ubuf))
 }
 
 ghost
@@ -750,6 +750,7 @@ pure func isHostSVC(a net.Addr) bool {
 
 // invariant established by initialization
 ghost
+trusted // TODO: drop this line after the static init PR
 ensures acc(path.PathPackageMem(), _)
 decreases
 func EstablishPathPkgMem()
@@ -762,14 +763,52 @@ pure func (s *SCION) HasOneHopPath(ghost ub []byte) bool {
 		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 && s.Path.Mem(ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen])
+decreases
+pure func (s *SCION) MinSizeOfUbufWithOneHopOpenInv(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 s.Mem(ub)
+decreases
+pure func (s *SCION) MinSizeOfUbufWithOneHop(ub []byte) int {
+	return unfolding s.Mem(ub) in
+		s.MinSizeOfUbufWithOneHopOpenInv(ub)
+}
+
+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 && s.Path.Mem(ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen])
+decreases
+pure func (s *SCION) ValidSizeOhpUbOpenInv(ub []byte) (b bool) {
+	return s.MinSizeOfUbufWithOneHopOpenInv(ub) <= len(ub)
+}
+
 ghost
 requires s.Mem(ub)
 requires s.HasOneHopPath(ub)
 ensures  b
 decreases
-pure func (s *SCION) InferSizeOHP(ghost ub []byte) (b bool) {
+pure func (s *SCION) ValidSizeOhpUb(ub []byte) (b bool) {
 	return unfolding s.Mem(ub) in
-		let pathSlice := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
-		let pathLen := s.Path.LenSpec(pathSlice) in
-		CmnHdrLen + s.AddrHdrLenSpecInternal() + pathLen <= len(ub)
+		s.ValidSizeOhpUbOpenInv(ub)
 }
diff --git a/router/dataplane.go b/router/dataplane.go
@@ -4324,7 +4324,7 @@ func updateSCIONLayer(rawPkt []byte, s *slayers.SCION, buffer gopacket.Serialize
 	// https://fsnets.slack.com/archives/C8ADBBG0J/p1592805884250700
 	rawContents := buffer.Bytes()
 	// @ assert !(reveal slayers.IsSupportedPkt(rawContents))
-	// @ s.InferSizeOHP(rawPkt)
+	// @ s.ValidSizeOhpUb(rawPkt)
 	// @ assert len(rawContents) <= len(rawPkt)
 	// @ unfold sl.Bytes(rawPkt, 0, len(rawPkt))
 	// @ unfold acc(sl.Bytes(rawContents, 0, len(rawContents)), R20)