Adapt according to new visibility rules - #433
Draft
jcp19 wants to merge 8 commits into
Draft
Conversation
Gobra now enforces Go's visibility rules (viperproject/gobra#1092): importing packages may only reference exported members, contracts of exported members may only mention exported names, and the bodies of fully-public predicates and pure functions may only reference exported members. verification/io is a purely ghost specification package whose members are all part of the interface used by the router, so every member (and every ghost struct field) is now exported. The redundant DataPlaneSpec.asid() alias for Asid() is dropped. Ghost struct types of the package are annotated as comparable, since importers compare their values with '=='. The same treatment is applied to the ghost helpers of pkg/slayers/path and pkg/slayers/path/scion that the router relies on, and monoset/resalgebra predicates and pure functions whose bodies expose private state are marked closed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
- pkg/addr: export the ghost helpers used in contracts of exported members and add AS.InRange, the ghost counterpart of the non-exported method inRange. - pkg/slayers: spell out the memory of the non-exported extnBase in the predicates of the exported extension headers, so importers can unfold them; wrap the private state of SCMP and of the SCION path pool in closed predicates and expose constructors/lemmas for it; export the ghost address predicates and the ghost counterpart of scmpRawInterfaceLen; mark SCMPTypeCodeMem closed. - Annotate the exported struct types compared with '==' across package boundaries as comparable. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
…ility rules Close the predicates and pure functions whose bodies expose private state (gopacket.PkgMem/Registered, big.Int.Mem), export the members that importing packages rely on (big.Int.ToInt, net.IsZeros), describe gopacket.NewFlow's result through closed accessors instead of the private fields of Flow, give interface members exported names, and annotate gopacket.Flow as comparable. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
The contracts of exported members, and the bodies of fully-public predicates and pure functions, may only reference exported members. In the router this is achieved by closing the predicates and pure functions that describe the private state of the dataplane (Mem, MutexInvariant, the getDom* accessors, ...), by exporting the ghost members that occur in contracts of exported members, and by wrapping the non-exported mutex of the dataplane in the closed predicate MtxInv. The two ghost lemmas whose contracts expose non-exported fields are no longer exported. AuthCarrier's ghost fields are exported because the methods that use them implement resalgebra.RA and can therefore not be closed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
jcp19
commented
Aug 14, 2026
Comment on lines
240
to
252
| // NewSCMP allocates a new SCMP layer with the given type code. Importing | ||
| // packages cannot establish the layer's predicates themselves, because those | ||
| // cover the private state of the layer; this constructor is how they obtain a | ||
| // usable layer. | ||
| // @ ensures s != nil | ||
| // @ ensures s.NonInitMem() | ||
| // @ decreases | ||
| func NewSCMP(typeCode SCMPTypeCode) (s *SCMP) { | ||
| s = &SCMP{TypeCode: typeCode} | ||
| // @ fold s.ChecksumNetworkLayerMem() | ||
| // @ fold s.NonInitMem() | ||
| return s | ||
| } |
Collaborator
Author
There was a problem hiding this comment.
instead, you could add a ghost method that takes permissions to all fields of a &SCMP and establishes s.NonInitMem(), as long as its pre is *s === SCMP{}
Comment on lines
+28
to
+30
| // The predicate is closed because its body mentions a non-exported field; | ||
| // importing packages may hold it, but they can neither fold nor unfold it. They | ||
| // obtain it by allocating a layer with NewSCMP. |
Collaborator
Author
There was a problem hiding this comment.
Suggested change
| // The predicate is closed because its body mentions a non-exported field; | |
| // importing packages may hold it, but they can neither fold nor unfold it. They | |
| // obtain it by allocating a layer with NewSCMP. | |
| // The predicate is closed because its body mentions a non-exported field; | |
| // importing packages may hold it, but they can neither fold nor unfold it. |
Comment on lines
+2206
to
+2208
| // (VerifiedSCION) the layer's predicates cover its private state, so it has | ||
| // to be allocated through the constructor exported by 'slayers'. | ||
| scmpLayer := slayers.NewSCMP(0) |
Collaborator
Author
There was a problem hiding this comment.
This shows a limitation of the design of the current solution: we currently cannot recover the permission to the private fields, which makes it impossible to fold scmpLayer.NonInitMem() on a client. A solution for this is to introduce automatically, for every type *T, where T is a struct type, a notion of "Private-fields Mem" that is implemented as a closed predicate granting access to the private fields. This resource should be established on every allocation / declaration of a new type. Likewise, we should be able to state properties like "the private fields have the default value". Dereferencing a *T would now require access to every field, as well as the "private mem" resource (this is already achieved by the current encoding)
Comment on lines
+5097
to
+5100
| // (VerifiedSCION) the layer's predicates cover its private state, so it has | ||
| // to be allocated through the constructor exported by 'slayers'. | ||
| scmpH := slayers.NewSCMP(typeCode) | ||
| // @ unfold scmpH.NonInitMem() |
- Drop the unused tcpipchecksum/tcpipPseudoHeader stub instead of renaming a non-ghost interface method of gopacket/layers. - Keep PathPoolMem and PathPoolMemExceptOne exported, and give the new closed predicates over the private path pool distinct names. - Do not specify permission amounts in the preconditions and unfolding expressions of the pure functions introduced here. - Replace the NewSCMP constructor by a ghost lemma that turns full permission to a zero-valued SCMP layer into its NonInitMem predicate, and use it at the two call sites in the router. - Reword the comment on SCMP.ChecksumNetworkLayerMem as suggested. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
Gobra reserves the identifier 'Token' for a built-in member predicate
(TokenMPredTag in BuiltInMemberTag.scala), which participates in name
resolution of every package. Exporting the IO-spec's 'token' predicate under
that name therefore made the declaration and all of its uses ambiguous
('got duplicate identifier Token'), and the failure cascaded into every
package importing verification/io.
Found by running the visibility-rules build of Gobra (viperproject/gobra#1092)
over the packages verified in CI.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
jcp19
commented
Aug 16, 2026
| Length uint16 | ||
| Checksum uint16 | ||
| sPort, dPort []byte | ||
| tcpipchecksum |
Collaborator
Author
There was a problem hiding this comment.
maybe add a PrivateFields pointer, as done for other types
Comment on lines
+5098
to
+5104
| // (VerifiedSCION) the layer is built from its zero value, because the lemma | ||
| // that establishes NonInitMem (which covers the private state of the layer, | ||
| // and can thus not be folded by a client) requires it. | ||
| scmpH /*@@@*/ := slayers.SCMP{} | ||
| // @ scmpH.EstablishNonInitMem() | ||
| // @ unfold scmpH.NonInitMem() | ||
| scmpH.TypeCode = typeCode |
Collaborator
Author
There was a problem hiding this comment.
do not change the code. Maybe just make the EstablishNonInitMem() method more general, where it does not need to take the 0 value.
A package invariant is part of a package's public interface, so it may only reference exported members. epic's 'dup pkgInvariant' named the non-exported predicate postInitInvariant; the predicate is now exported, and closed, since its body describes the private global state of the package. Verified with the visibility-rules build of Gobra (viperproject/gobra#1092): pkg/experimental/epic goes from 3 errors on master to 0. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.