Provide optional perm parameter to range loops over maps - #1100
Open
jcp19 wants to merge 4 commits into
Open
Conversation
The encoding of a range loop over a map exhales a fixed, very small,
amount of permission to the map for the duration of the loop body, which
guarantees that the map is not modified while iterating over it. That
fixed amount is sometimes too restrictive: it may exceed the permission
at hand, e.g. when the loop invariant only provides a symbolic amount
`p` that is not known to be greater than 1/MapExhalePermDenom.
Range clauses now accept an optional permission amount:
for k, v := range m, p with visited { ... }
The amount is optional and, when omitted, the previous default is used.
It is checked to be strictly positive (otherwise it would not guarantee
that the range expression stays unmodified), and is only allowed when
ranging over a map, since no other encoding of a range loop exhales
permission to the range expression.
Failing the positivity check is reported as the new error
`non_positive_permission_to_range_expression`.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GYq5KH3pi3UeZLJthDYu4f
The permission amount is a specification-only annotation, but it was
parsed as a plain expression hanging off PRange, which is a PActualMisc.
It therefore sat in no ghost context at all, and nothing checked it for
purity: `for k := range m, impure() { }` (a call to a non-ghost impure
function) was accepted by the type checker and desugared into executable
code in a position that can only ever be specification.
Wrap the amount in a new ghost misc node, PRangePerm, so that
isEnclosingGhost holds for it, and move its well-definedness check to
wellDefGhostMisc, where it now also requires the amount to be a pure
expression. The check that an amount may only be given when ranging over
a map stays on PRange, since it needs the range expression's type.
GhostLessPrinter now drops both ghost annotations of a range clause --
the permission amount and the `with` clause -- neither of which is valid
Go, so neither belongs in the ghost-erased program.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GYq5KH3pi3UeZLJthDYu4f
`for k := range m, _ { }` now exhales a wildcard amount, spelled the same
way as in an `acc` expression. This is the amount to use when all that is
at hand is a wildcard itself: the default fixed fraction is not known to
be smaller than a wildcard, so exhaling it fails.
A wildcard is not routed through the permission variable that holds a
user-provided amount, because Viper needs the literal `wildcard` at the
exhale to pick an amount small enough to be available. Consequently the
amount inhaled after the loop body is a fresh wildcard rather than the
one exhaled before it, so a wildcard amount is only useful for loops
whose invariant holds a wildcard too; both directions are covered by the
new tests. The positivity check is skipped, since wildcards are positive
by construction and cannot be compared to other amounts.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GYq5KH3pi3UeZLJthDYu4f
jcp19
commented
Aug 27, 2026
Review feedback: the extra node was not load-bearing. Its only effect was to make isEnclosingGhost hold for the amount, and the one diagnostic that depended on that -- "call to non-ghost impure function in ghost code" -- is subsumed by the purity check, which does not need a ghost context. The substantive guarantees are unchanged: the amount must be pure and assignable to perm, ghost values and ghost pure calls are still allowed, and ghost erasure still drops it. This also matches how the `with` clause, the range clause's other specification-only annotation, is modelled. The checks move back to wellDefActualMisc, next to the check that an amount may only be given when ranging over a map. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GYq5KH3pi3UeZLJthDYu4f
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.
To prevent mutating the map while it is being traversed by a range loop, Gobra exhales a small but fixed permission to the map before iteration. This prevents us from traversing maps in cases where we only have
_or an amount which is only known to be positive.This PR extends the syntax for
rangeloops over maps, where we can pass an extra optional parameter with a permission amount or_, which stands for the permission amount we exhale when traversing the map (instead of using the default)