Skip to content

Adapt according to new visibility rules #433

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
jcp19 wants to merge 8 commits into
base: master
Choose a base branch
from
Draft

Adapt according to new visibility rules #433

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
8a70f93
Export ghost members of verification/io and adapt its clients
claude Aug 13, 2026
79e5c15
Adapt pkg/addr and pkg/slayers to Gobra's visibility rules
claude Aug 13, 2026
ef74b6d
Adapt the third-party stubs in verification/dependencies to the visib…
claude Aug 13, 2026
5b55390
Adapt the router package to Gobra's visibility rules
claude Aug 13, 2026
fba4f92
Fold DataPlane.MtxInv in the dataplane spec test
claude Aug 13, 2026
419b4e6
Address review comments
claude Aug 15, 2026
ebe3cff
Rename io.Token to io.IOToken to avoid a clash with a Gobra built-in
claude Aug 16, 2026
94c8435
Export epic's post-init invariant and mark it closed
claude Aug 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion pkg/addr/fmt.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ func FormatAS(as_ AS, opts ...FormatOption) string {
return s
}

// @ requires as_.inRange()
// @ requires as_.InRange()
// @ decreases
func fmtAS(as_ AS, sep string) string {
if !as_.inRange() {
Expand Down
8 changes: 4 additions & 4 deletions pkg/addr/host.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ const (
HostTypeSVC
)

// @ requires isValidHostAddrType(t)
// @ requires IsValidHostAddrType(t)
// @ decreases
func (t HostAddrType) String() string {
switch t {
Expand Down Expand Up @@ -433,8 +433,8 @@ func (h HostSVC) Network() string {
}

// @ requires acc(b)
// @ requires isValidHostAddrType(htype)
// @ requires len(b) == sizeOfHostAddrType(htype)
// @ requires IsValidHostAddrType(htype)
// @ requires len(b) == SizeOfHostAddrType(htype)
// @ ensures err == nil ==> res.Mem()
// @ decreases
func HostFromRaw(b []byte, htype HostAddrType) (res HostAddr, err error) {
Expand Down Expand Up @@ -502,7 +502,7 @@ func HostFromIPStr(s string) (res HostAddr) {
return HostFromIP(ip)
}

// @ requires isValidHostAddrType(htype)
// @ requires IsValidHostAddrType(htype)
// @ decreases
func HostLen(htype HostAddrType) (uint8, error) {
var length uint8
Expand Down
6 changes: 3 additions & 3 deletions pkg/addr/host_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,21 +51,21 @@ pred (h *HostSVC) Mem() { acc(h) }

ghost
decreases
pure func isValidHostAddrType(htype HostAddrType) bool {
pure func IsValidHostAddrType(htype HostAddrType) bool {
return htype == HostTypeNone ||
htype == HostTypeIPv4 ||
htype == HostTypeIPv6 ||
htype == HostTypeSVC
}

ghost
requires isValidHostAddrType(htype)
requires IsValidHostAddrType(htype)
ensures htype == HostTypeNone ==> res == HostLenNone
ensures htype == HostTypeIPv4 ==> res == HostLenIPv4
ensures htype == HostTypeIPv6 ==> res == HostLenIPv6
ensures htype == HostTypeSVC ==> res == HostLenSVC
decreases
pure func sizeOfHostAddrType(htype HostAddrType) (res int) {
pure func SizeOfHostAddrType(htype HostAddrType) (res int) {
return htype == HostTypeNone ?
HostLenNone : htype == HostTypeIPv4 ?
HostLenIPv4 : htype == HostTypeIPv6 ?
Expand Down
14 changes: 7 additions & 7 deletions pkg/addr/isdas.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,13 +71,13 @@ type AS uint64

// ParseAS parses an AS from a decimal (in the case of the 32bit BGP AS number
// space) or ipv6-style hex (in the case of SCION-only AS numbers) string.
// @ ensures retErr == nil ==> retAs.inRange()
// @ ensures retErr == nil ==> retAs.InRange()
// @ decreases
func ParseAS(_as string) (retAs AS, retErr error) {
return parseAS(_as, ":")
}

// @ ensures retErr == nil ==> retAs.inRange()
// @ ensures retErr == nil ==> retAs.InRange()
// @ decreases
func parseAS(_as string, sep string) (retAs AS, retErr error) {
parts := strings.Split(_as, sep)
Expand Down Expand Up @@ -110,15 +110,15 @@ func parseAS(_as string, sep string) (retAs AS, retErr error) {
return parsed, nil
}

// @ ensures retErr == nil ==> retAs.inRange()
// @ ensures retErr == nil ==> retAs.InRange()
// @ decreases
func asParseBGP(s string) (retAs AS, retErr error) {
_as, err := strconv.ParseUint(s, 10, BGPASBits)
if err != nil {
return 0, serrors.WrapStr("parsing BGP AS", err)
}
// (VerifiedSCION)
// The following assertions are needed to prove retAs.inRange().
// The following assertions are needed to prove retAs.InRange().
// Gobra is not able to infer this automatically from the definition
// of strconv.Exp, unless we put a postcondition saying that the
// result is equal to the body.
Expand All @@ -131,7 +131,7 @@ func asParseBGP(s string) (retAs AS, retErr error) {
return AS(_as), nil
}

// @ requires _as.inRange()
// @ requires _as.InRange()
// @ decreases
func (_as AS) String() string {
return fmtAS(_as, ":")
Expand Down Expand Up @@ -175,7 +175,7 @@ type IA uint64
// MustIAFrom creates an IA from the ISD and AS number. It panics if any error
// is encountered. Callers must ensure that the values passed to this function
// are valid.
// @ requires _as.inRange()
// @ requires _as.InRange()
// @ decreases
func MustIAFrom(isd ISD, _as AS) IA {
ia, err := IAFrom(isd, _as)
Expand All @@ -186,7 +186,7 @@ func MustIAFrom(isd ISD, _as AS) IA {
}

// IAFrom creates an IA from the ISD and AS number.
// @ requires _as.inRange()
// @ requires _as.InRange()
// @ ensures err == nil
// @ decreases
func IAFrom(isd ISD, _as AS) (ia IA, err error) {
Expand Down
9 changes: 9 additions & 0 deletions pkg/addr/isdas_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,3 +67,12 @@ pred (_as *AS) Mem() { acc(_as) }
fold ia.Mem()
}
}

// InRange is the ghost counterpart of the (non-exported) method AS.inRange. It is
// part of the contracts of exported members of this package, which may not
// mention non-exported members.
ghost
decreases
pure func (_as AS) InRange() bool {
return _as <= MaxAS
}
8 changes: 4 additions & 4 deletions pkg/experimental/epic/epic.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@

// +gobra

// @ dup pkgInvariant acc(postInitInvariant(), _)
// @ dup pkgInvariant acc(PostInitInvariant(), _)
package epic

import (
Expand Down Expand Up @@ -51,7 +51,7 @@ var zeroInitVector /*@@@*/ [16]byte
// ghost init
// @ func init() {
// @ fold acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), _)
// @ fold acc(postInitInvariant(), _)
// @ fold acc(PostInitInvariant(), _)
// @ }

// CreateTimestamp returns the epic timestamp, which encodes the current time (now) relative to the
Expand Down Expand Up @@ -216,7 +216,7 @@ func initEpicMac(key []byte) (res cipher.BlockMode, reserr error) {
}

// @ establishPostInitInvariant()
// @ unfold acc(postInitInvariant(), _)
// @ unfold acc(PostInitInvariant(), _)
// CBC-MAC = CBC-Encryption with zero initialization vector
mode := cipher.NewCBCEncrypter(block, zeroInitVector[:])
return mode, nil
Expand Down Expand Up @@ -302,7 +302,7 @@ func prepareMacInput(pktID epic.PktID, s *slayers.SCION, timestamp uint32,
// @ assert forall i int :: { &inputBuffer[offset:inputLength][i] } 0 <= i && i < len(inputBuffer[offset:inputLength]) ==>
// @ acc(&inputBuffer[offset:inputLength][i])
// @ establishPostInitInvariant()
// @ unfold acc(postInitInvariant(), _)
// @ unfold acc(PostInitInvariant(), _)
// @ assert acc(sl.Bytes(zeroInitVector[:], 0, 16), _)
// (VerifiedSCION) From the package invariant, we learn that we have a wildcard access to zeroInitVector.
// Unfortunately, it is not possible to call `copy` with a wildcard amount, even though
Expand Down
6 changes: 4 additions & 2 deletions pkg/experimental/epic/epic_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,15 +18,17 @@ package epic

import sl "github.com/scionproto/scion/verification/utils/slices"

pred postInitInvariant() {
// The body describes the private global state of this package, so the predicate
// is closed: importing packages may hold it, but they cannot unfold it.
closed pred PostInitInvariant() {
acc(&zeroInitVector) &&
len(zeroInitVector[:]) == 16 &&
acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])))
}

// learn the invariant established by init
ghost
ensures acc(postInitInvariant(), _)
ensures acc(PostInitInvariant(), _)
decreases
func establishPostInitInvariant() {
openDupPkgInv
Expand Down
36 changes: 14 additions & 22 deletions pkg/slayers/extn.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -303,7 +303,7 @@ func (h *HopByHopExtn) CanDecode() (res gopacket.LayerClass) {
// @ preserves acc(h.Mem(ubuf), R20)
// @ decreases
func (h *HopByHopExtn) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.LayerType {
return scionNextLayerTypeAfterHBH( /*@ unfolding acc(h.Mem(ubuf), R20) in (unfolding acc(h.extnBase.Mem(ubuf), R20) in @*/ h.NextHdr /*@ ) @*/)
return scionNextLayerTypeAfterHBH( /*@ unfolding acc(h.Mem(ubuf), R20) in @*/ h.NextHdr)
}

// @ preserves acc(h.Mem(ub), R20)
Expand All @@ -313,14 +313,12 @@ func (h *HopByHopExtn) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.Layer
// @ decreases
func (h *HopByHopExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte /*@ , ghost start int, ghost end int @*/) {
// @ unfold acc(h.Mem(ub), R20)
// @ unfold acc(h.extnBase.Mem(ub), R20)
// @ ghost base := &h.extnBase.BaseLayer
// @ ghost base := &h.BaseLayer
// @ unfold acc(base.Mem(ub, h.ActualLen), R20)
tmp := h.Payload
// @ start = h.ActualLen
// @ end = len(ub)
// @ fold acc(base.Mem(ub, h.ActualLen), R20)
// @ fold acc(h.extnBase.Mem(ub), R20)
// @ fold acc(h.Mem(ub), R20)
return tmp /*@ , start, end @*/
}
Expand Down Expand Up @@ -392,8 +390,7 @@ func (h *HopByHopExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
// @ fold tmp.Mem(lenOptions)
// @ lenOptions += 1
}
// @ fold h.extnBase.BaseLayer.Mem(data, h.extnBase.ActualLen)
// @ fold h.extnBase.Mem(data)
// @ fold h.BaseLayer.Mem(data, h.ActualLen)
// @ fold h.Mem(data)
return nil
}
Expand All @@ -411,7 +408,7 @@ func decodeHopByHopExtn(data []byte, p gopacket.PacketBuilder) (res error) {
if err != nil {
return err
}
nextTmp := scionNextLayerTypeAfterHBH(( /*@ unfolding h.Mem(data) in (unfolding h.extnBase.Mem(data) in @*/ h.NextHdr /*@ ) @*/))
nextTmp := scionNextLayerTypeAfterHBH(( /*@ unfolding h.Mem(data) in @*/ h.NextHdr))
// @ fold nextTmp.Mem()
return p.NextDecoder(nextTmp)
}
Expand Down Expand Up @@ -452,7 +449,7 @@ func (e *EndToEndExtn) CanDecode() (res gopacket.LayerClass) {
// @ preserves acc(e.Mem(ubuf), R20)
// @ decreases
func (e *EndToEndExtn) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.LayerType {
return scionNextLayerTypeAfterE2E( /*@ unfolding acc(e.Mem(ubuf), R20) in (unfolding acc(e.extnBase.Mem(ubuf), R20) in @*/ e.NextHdr /*@ ) @*/)
return scionNextLayerTypeAfterE2E( /*@ unfolding acc(e.Mem(ubuf), R20) in @*/ e.NextHdr)
}

// @ preserves acc(e.Mem(ub), R20)
Expand All @@ -462,14 +459,12 @@ func (e *EndToEndExtn) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.Layer
// @ decreases
func (e *EndToEndExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte /*@ , ghost start int, ghost end int @*/) {
// @ unfold acc(e.Mem(ub), R20)
// @ unfold acc(e.extnBase.Mem(ub), R20)
// @ ghost base := &e.extnBase.BaseLayer
// @ ghost base := &e.BaseLayer
// @ unfold acc(base.Mem(ub, e.ActualLen), R20)
tmp := e.Payload
// @ start = e.ActualLen
// @ end = len(ub)
// @ fold acc(base.Mem(ub, e.ActualLen), R20)
// @ fold acc(e.extnBase.Mem(ub), R20)
// @ fold acc(e.Mem(ub), R20)
return tmp /*@ , start, end @*/
}
Expand Down Expand Up @@ -524,8 +519,7 @@ func (e *EndToEndExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
// @ fold tmp.Mem(lenOptions)
// @ lenOptions += 1
}
// @ fold e.extnBase.BaseLayer.Mem(data, e.ActualLen)
// @ fold e.extnBase.Mem(data)
// @ fold e.BaseLayer.Mem(data, e.ActualLen)
// @ fold e.Mem(data)
return nil
}
Expand All @@ -543,7 +537,7 @@ func decodeEndToEndExtn(data []byte, p gopacket.PacketBuilder) (res error) {
if err != nil {
return err
}
nextTmp := scionNextLayerTypeAfterE2E( /*@ unfolding e.Mem(data) in (unfolding e.extnBase.Mem(data) in @*/ e.NextHdr /*@ ) @*/)
nextTmp := scionNextLayerTypeAfterE2E( /*@ unfolding e.Mem(data) in @*/ e.NextHdr)
// @ fold nextTmp.Mem()
return p.NextDecoder(nextTmp)
}
Expand Down Expand Up @@ -617,9 +611,8 @@ func (s *HopByHopExtnSkipper) DecodeFromBytes(data []byte, df gopacket.DecodeFee
// @ fold s.NonInitMem()
return err
}
// @ ghost contentsLen := s.extnBase.ActualLen
// @ fold s.extnBase.BaseLayer.Mem(data, s.ActualLen)
// @ fold s.extnBase.Mem(data)
// @ ghost contentsLen := s.ActualLen
// @ fold s.BaseLayer.Mem(data, s.ActualLen)
// @ fold s.Mem(data)
return nil
}
Expand All @@ -641,7 +634,7 @@ func (s *HopByHopExtnSkipper) CanDecode() (res gopacket.LayerClass) {
// @ preserves acc(h.Mem(ubuf), R20)
// @ decreases
func (h *HopByHopExtnSkipper) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.LayerType {
return scionNextLayerTypeAfterHBH( /*@ unfolding acc(h.Mem(ubuf), R20) in (unfolding acc(h.extnBase.Mem(ubuf), R20) in @*/ h.NextHdr /*@ ) @*/)
return scionNextLayerTypeAfterHBH( /*@ unfolding acc(h.Mem(ubuf), R20) in @*/ h.NextHdr)
}

// EndToEndExtnSkipper is a DecodingLayer which decodes an EndToEnd extension
Expand Down Expand Up @@ -672,9 +665,8 @@ func (s *EndToEndExtnSkipper) DecodeFromBytes(data []byte, df gopacket.DecodeFee
// @ fold s.NonInitMem()
return err
}
// @ ghost contentsLen := s.extnBase.ActualLen
// @ fold s.extnBase.BaseLayer.Mem(data, s.ActualLen)
// @ fold s.extnBase.Mem(data)
// @ ghost contentsLen := s.ActualLen
// @ fold s.BaseLayer.Mem(data, s.ActualLen)
// @ fold s.Mem(data)
return nil
}
Expand All @@ -696,5 +688,5 @@ func (s *EndToEndExtnSkipper) CanDecode() (res gopacket.LayerClass) {
// @ preserves acc(e.Mem(ubuf), R20)
// @ decreases
func (e *EndToEndExtnSkipper) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.LayerType {
return scionNextLayerTypeAfterE2E( /*@ unfolding acc(e.Mem(ubuf), R20) in (unfolding acc(e.extnBase.Mem(ubuf), R20) in @*/ e.NextHdr /*@ ) @*/)
return scionNextLayerTypeAfterE2E( /*@ unfolding acc(e.Mem(ubuf), R20) in @*/ e.NextHdr)
}
Loading
Loading