Skip to content

Commit

Permalink
Update pkg/slayers/scion.go
Browse files Browse the repository at this point in the history
  • Loading branch information
jcp19 authored Jan 7, 2025
1 parent 19bdc60 commit f934d8d
Showing 1 changed file with 0 additions and 10 deletions.
10 changes: 0 additions & 10 deletions pkg/slayers/scion.go
Original file line number Diff line number Diff line change
Expand Up @@ -317,16 +317,6 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO
// @ sl.CombineRange_Bytes(ubuf, startP, endP, HalfPerm)
// @ reveal IsSupportedPkt(uSerBufN)
// @ reveal IsSupportedRawPkt(b.View())

// (VerifiedSCION) to check the proof obligations related
// to the branch "typeOf(s.Path) == type[*onehop.Path]"
// in SCION.Mem():
// ghost if err != nil && typeOf(s.Path) == type[*onehop.Path] {
// s.MinSizeOfUbufWithOneHopOpenInv(ubuf)
// pathLen := s.Path.LenSpec(pathSlice)
// assert CmnHdrLen + s.AddrHdrLenSpecInternal() + pathLen <= len(ubuf)
// assert s.ValidSizeOhpUbOpenInv(ubuf)
// }
return tmp
}

Expand Down

0 comments on commit f934d8d

Please sign in to comment.