Adapt according to new visibility rules - #433
Draft
jcp19 wants to merge 13 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{}
- 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
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
The visibility rules are not in a released Gobra yet, so the two new keywords this branch introduced would not parse. Every occurrence is replaced by a '// TODO(gobra#1092): closed' / '// TODO(gobra#1092): comparable' marker directly above the declaration it applied to; re-enabling them is a matter of uncommenting (the grammar accepts both modifiers on their own line). The restructuring they go with -- exported ghost members, predicates split so that the private part sits behind its own predicate, package invariants that only name exported members -- is kept, since it is valid under the current Gobra as well. Also reverts the one change this branch had made to executable code: the SCMP layer in prepareSCMP is built from a keyed struct literal again, as it was before. It only had to be built from its zero value so that a client could establish NonInitMem without folding a closed predicate, which is not a requirement until gobra#1092 lands; a TODO records what to do then. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
master added lemmas and assertions that use the ghost members this branch renamed (absPkt, validPktMetaHdr, io.upd_uinfo, path.ifsToIO_ifs, ...). The conflicting hunks in router/dataplane.go and router/io-spec-lemmas.gobra are resolved in favour of master's content, with this branch's renames re-applied to it; the same renames are applied to the newly added pkg/slayers/path/scion/lemmas.gobra. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
- HiddenPathPoolMemExceptOne now carries the bound on pathType that used to be provided by an earlier conjunct of SCION.Mem; without it, the call to getPathPure in the predicate body has no precondition. - testRun folds the new MtxInv predicate before calling Run. - handleSCMPTraceRouteRequest uses the EstablishNonInitMem lemma, like the other two client-side sites that build an SCMP layer. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
master's #439 relaxed WellConfigured and PreWellConfigured so that a router need only terminate a subset of the interfaces of its AS, and added KnownIfIDLemma and getDomInternalNextHopsLemma alongside them. The conflicting hunks in router/dataplane_spec.gobra and router/dataplane_spec_test.gobra are resolved in favour of master's content, with this branch's renames of the getDom* accessors re-applied to it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
pkg/slayers was never reached by CI on this branch, because an earlier step of the same job failed; these are the two places in the package that the restructuring of the path pool into HiddenPathPoolMem(ExceptOne) broke. ExtractAcc hands out access to the whole layer, so it now also unfolds the predicate that holds the fields of the path pool, and folds it back in the body of the wand it packages. The assertion in that body makes the facts about the layer that unfolding Mem provides available for the permissions that come from the left-hand side of the wand. 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.