[Experiment] Enable Go's name visibility rules - #1092
Draft
jcp19 wants to merge 11 commits into
Draft
Conversation
Implements the access-modifiers design (docs/design/access-modifiers.md): - The type checker now enforces Go's visibility rules across packages: non-exported members of imported packages cannot be referenced (lookups yield a dedicated error; the builtin package is exempt, and generated ADT discriminators of exported clauses count as exported). - Contracts of exported members, bodies of fully-public predicates and pure functions, package invariants, and friend-package assertions may only reference exported members. - New `closed` modifier for predicates and pure functions: the body is visible in the declaring package but hidden from importers, which can neither fold/unfold closed predicates nor reveal closed opaque functions. Closed pure methods cannot implement interface methods, as the hidden call-graph edges would break termination checking of dynamic dispatch. Private interface members are rejected. - New `comparable` annotation for type declarations: checked in the declaring package, assumed by importers. Imported struct-backed types without the annotation are not comparable (no ==, no use as map keys). Conversions and positional composite literals that depend on non-exported fields of imported struct types are rejected. - Desugaring skips non-exported members of imported packages entirely and drops the bodies of imported closed members; well-definedness checks of non-exported imported functions, methods, and predicates are skipped (they are checked when their own package is verified). - Fix a crash in the well-definedness check of return statements inside closure implementation proofs whose spec function does not resolve. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- Rename non-exported interface members, spec helpers, and fields that are part of a package's client-facing surface across the regression suite, and adapt cross-package tests to the new rules. - Add regression tests for the new rules under features/visibility/: private-member access, closed members (well-formedness, client restrictions, body hiding), the comparable annotation, conversion and literal restrictions, equality of imported structs, and termination of mutual recursion through an imported interface. - Stubs: export net.IsZeros (used in a public contract); parallel_sum states mutex initialization via ghost equality with the zero value instead of reading sync.Mutex internals. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The previous commit adapted most of the test suite to Go's visibility rules, but 31 tests still failed. This commit fixes the rest: - Propagate renames that were applied to declarations but not to their uses: the `VIsOne`/`IsQuery`/`Answer` predicate constructors in the channel tests, the interface members `Res`, `Inv`, and `Mem`. - Export what importing packages and client-facing specs refer to: `counterImpl.Counter` (and its fields), `cell.Cell`/`cellMem.CellMem`, the fields of `name.Name`, `path.MaxPathType`, `pkg1/subpackage.Test`, the fields of stats_collector's `Rect`/`Circle`, and the interface methods `GetValue` and `M`. - Mark as `closed` the exported predicates and pure functions whose bodies legitimately mention package-private state: the `pkg_init` static invariants, `invallinstances`' `PkgInv`/`Inv`/`Allocated`/`Id`, `byte.ByteValue`, scion's `PkgInv`/`RegisteredTypes`, and issue 697's `Impl.Inv`. - Annotate `pkg.T` of issue 190 as `comparable`, as the test compares values of that imported struct type. - Rename the `token` predicate of declassify-simple1.gobra to `PlaceToken`: `Token` is the identifier of a built-in channel predicate, so exporting the name under `Token` made it a duplicate. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0178ZAqwVnGiPy86mzsZ5aZS
Dropping members from the encoding of imported packages is unsound: Viper only checks for non-terminating (mutual) recursion when it detects a cycle in the call graph, so an omitted body may hide such a cycle from the client. This can happen through a `closed` pure function that calls back into an interface method, even when the implementation of that method is itself neither closed nor private. Following the updated design document: - Desugar: only skip non-exported, *non-pure* functions and methods of imported packages. Non-exported pure members and predicates are encoded again, as their bodies contribute call-graph edges. - Desugar: the body of a `closed` pure function or method of an imported package is no longer dropped. The member is encoded as opaque instead, which keeps the call-graph edges while hiding the body from clients (the type checker already rejects revealing imported closed members). - Desugar: the bodies of `closed` predicates are kept as well. Clients still cannot observe them, as folding and unfolding an imported closed predicate is a type error. - Drop the type check that prevented closed pure methods from implementing interface methods. It was the workaround for the missing call-graph edges, which are now present. - Errors: check the well-definedness of the imported members that are encoded again; only non-exported, non-pure functions and methods remain unchecked. Tests: closed_implements.gobra now checks that a closed pure method may implement an interface method, and the new termination_itf_closed regression test checks that mutual recursion through a closed imported pure function is still detected. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0178ZAqwVnGiPy86mzsZ5aZS
jcp19
pushed a commit
to viperproject/VerifiedSCION
that referenced
this pull request
Aug 16, 2026
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
pushed a commit
to viperproject/VerifiedSCION
that referenced
this pull request
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
…aque The changes to the encoding of imported packages are left for a follow-up. What remains of them is the translation of `closed` pure functions and methods of imported packages as opaque members, which is what hides their bodies from clients. - Desugar: no longer skip any member of an imported package. Every member is encoded again, as on master. - Errors: revert the skipping of the well-definedness checks of non-exported members of imported packages, which was tied to those members not being encoded. The type-check that prevented closed pure methods from implementing interface methods stays removed: the bodies of closed members are encoded, so the call graph on which Viper's termination checks rely is complete. The new acc_private_fields test records that `acc(x)` is permitted in the contract of an exported member (and in the body of a fully-public predicate) even when the type of `x` has non-exported fields, in the declaring as well as in an importing package: unlike `acc(&x.f)`, it does not name a non-exported member. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0178ZAqwVnGiPy86mzsZ5aZS
…fields A composite literal that leaves the non-exported fields of a struct at their default value can be interpreted by an importing package, and is thus allowed in the client-facing parts of a package. This is already the case for the empty literal and for keyed literals whose keys are all exported; keyed literals that name a non-exported field are rejected by the existing check for references to non-exported members. A positional literal, on the other hand, assigns to every field: it constrains the non-exported ones and reveals how many of them there are. Reject it in contracts of exported members, in bodies of fully-public predicates and pure functions, in package invariants, and in friend-package assertions. Note that this only concerns the types declared by the package itself; for imported struct types with non-exported fields, positional literals are rejected everywhere. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0178ZAqwVnGiPy86mzsZ5aZS
Rather than proposing changes to the encoding, the design document now describes how the access modifiers could be used to infer what does not need to be translated from imported packages, and why we do not do it yet: dropping members of imported packages may hide cycles in the call graph and thereby affect the results of termination checking, which is not modular. Also record that the desugarer currently translates every member of the imported packages, and that imported `closed` pure functions and methods are translated as opaque. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0178ZAqwVnGiPy86mzsZ5aZS
`time.Time` is comparable in Go, but importing packages do not decide the comparability of an imported struct type from its non-exported fields, so without the annotation clients could no longer compare timestamps nor use them as map keys. `time.Location` stays unannotated: it holds a slice, so it is not comparable in Go either. The other struct types of the stubs are not comparable in Go, as they hold slices. The design document claimed that clients cannot access the members of private imported types and do not know which interfaces those types implement. Neither matches the implemented behaviour, which is the more useful one: an importing package cannot name a private imported type, but it can use the values of it that exported members hand out, access their public members, and rely on the interfaces they implement -- which is what makes the constructor pattern `func New() *client` work. The document now describes that. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0178ZAqwVnGiPy86mzsZ5aZS
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.