Provide permission introspection as a library - #434
Draft
jcp19 wants to merge 5 commits into
Draft
Conversation
Several Gobra operations (`copy`, `append`, `range` loops) must be given a permission expression and cannot be applied with a wildcard amount, even though that would be perfectly sound. So far, the codebase worked around this by inhaling a fixed permission amount whenever only a wildcard was held, e.g. `inhale acc(x, R19)` after `assert acc(x, _)`. That assumes strictly more than `acc(x, _)` justifies: it fixes a concrete lower bound on the amount held, and the constant has to be chosen so that it does not clash with the other permissions to `x` that are around. This commit replaces those inhales with permission introspection: given `acc(x, _)`, `PermIntrospectT(x)` names the amount currently held and returns it as a symbolic `p` constrained only by `0 < p`. Callers use `p` wherever a permission expression is required. Introspecting does not give up the wildcard, so no clean-up is needed afterwards to recover it. The functions are axioms, but semantically justified ones: `acc(x, _)` denotes some positive amount, so a positive `p` with `acc(x, p)` always exists; Viper simply cannot bind that amount to a program variable. `permsintrospect` imports nothing, so that any package may import it without introducing an import cycle, which Gobra rejects. Introspection functions whose signature mentions a type or predicate of another package Q therefore live in Q, in a file named `perm-introspect.gobra`: - `verification/utils/slices/perm-introspect.gobra` for the `Bytes` predicate, since `slices` must stay free to introspect permissions itself; - `router/perm-introspect.gobra` for `map[uint16]*net.UDPAddr`, since that map type is specific to the dataplane and `permsintrospect` would otherwise have to import the `net` stubs. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CSKDgMaZVp35UqtekdhKYQ
Add `PermIntrospectBytes` to `permsintrospect`, which introspects the permission held to the elements of a `[]byte` over a range. It is stated with a quantified permission, since that is how access to slice elements is expressed, and returns a single amount for the whole range, which is what makes it usable to introspect a predicate abstracting over such a range. With that primitive in place, `slices.PermIntrospectBytes` no longer has to be an axiom of its own: it unfolds the `Bytes` instance held with a wildcard, introspects the resulting permission to the elements, and folds the predicate back with the amount that was named. One fewer assumption, and the proof obligation now also acts as a check on the primitive. This makes `slices` a client of `permsintrospect`, so importing `slices` from `permsintrospect` would now be a genuine import cycle rather than a hypothetical one; the package documentation is updated accordingly. `router.PermIntrospectAddrsMap` stays an axiom: the permission to a map is atomic, so there is nothing to unfold and introspect at a more primitive level, and Gobra has no generics that would let `permsintrospect` declare one map primitive for arbitrary key and value types. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CSKDgMaZVp35UqtekdhKYQ
Replace the range-shaped `[]byte` axiom with the simpler per-element one: given a wildcard to `&s[idx]`, name the amount held. It is easier to read and to justify than a quantified assumption. Deriving the range version from it is not a one-liner, though. The axiom names an amount for one element, and the amounts it returns for two different elements are unrelated, so a single call cannot establish a uniform amount over a range -- and uniformity is exactly what folding a predicate that abstracts over that range requires. So `PermIntrospectBytesRange` now recurses over the range, introspecting each element and keeping the smallest of the results: holding `acc(&s[i], p_i)` for every `i` implies holding `acc(&s[i], m)` for `m` the minimum of the `p_i`. The recursion is what pays for the simpler axiom. `slices.PermIntrospectBytes` is unchanged in shape: it unfolds the `Bytes` instance, calls the range lemma, and folds back. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CSKDgMaZVp35UqtekdhKYQ
It has no call site, and the permission to a slice header is not something the codebase has needed to name so far. It also sat confusingly next to `PermIntrospectBytes`, which introspects the elements of a byte slice rather than the header. Every axiom here is an assumption, so an unused one is not free. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CSKDgMaZVp35UqtekdhKYQ
jcp19
changed the title
jcp19
commented
Aug 18, 2026
Comment on lines
+308
to
+312
| // Unfortunately, it is not possible to call `copy` with a wildcard amount, even though that would be | ||
| // perfectly fine. Instead of assuming a fixed permission amount, we introspect the one we already | ||
| // hold and pass the resulting symbolic, positive amount to `copy`. | ||
| // @ ghost zeroPerm := sl.PermIntrospectBytes(zeroInitVector[:], 0, len(zeroInitVector[:])) | ||
| // @ unfold acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), zeroPerm) |
Collaborator
Author
There was a problem hiding this comment.
Suggested change
| // Unfortunately, it is not possible to call `copy` with a wildcard amount, even though that would be | |
| // perfectly fine. Instead of assuming a fixed permission amount, we introspect the one we already | |
| // hold and pass the resulting symbolic, positive amount to `copy`. | |
| // @ ghost zeroPerm := sl.PermIntrospectBytes(zeroInitVector[:], 0, len(zeroInitVector[:])) | |
| // @ unfold acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), zeroPerm) | |
| // It is not possible to call `copy` with a wildcard amount. As suuch, we use permission | |
| // introspection to soundly obtain a symbolic positive permission amount for `zeroInitVector`. | |
| // @ ghost zeroPerm := sl.PermIntrospectBytes(zeroInitVector[:], 0, len(zeroInitVector[:])) | |
| // @ unfold acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), zeroPerm) |
| // | ||
| // The functions below have no body; they are axioms. They are semantically | ||
| // justified: `acc(x, _)` denotes *some* positive permission amount, so a positive | ||
| // `p` with `acc(x, p)` always exists. Viper simply has no way of binding that |
Collaborator
Author
There was a problem hiding this comment.
rename file to introspect.gobra
Permission introspection cannot serve a range loop over a map. Gobra desugars such a loop into code that exhales a hard-coded `acc(m, 1/MapExhalePermDenom)` before entering it (Desugar.scala), so the loop demands an amount bounded from below by a concrete constant. Naming the amount held does not establish that bound -- introspection only guarantees the amount is positive -- so no symbolic amount can discharge it, and neither can the wildcard the site actually holds. `processIntraBFD` therefore goes back to its original encoding, byte for byte, with only a comment added recording why the inhale has to stay and why the obvious improvement does not work. `PermIntrospectAddrsMap` is removed along with it, since nothing uses it any more and an unused axiom is not free. The package documentation claimed range loops among the cases introspection serves. That was wrong, so it now carries an explicit limitation section instead. `copy` and `append` are unaffected: they take the amount as an ordinary expression. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CSKDgMaZVp35UqtekdhKYQ
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.
Viper provides permission introspection, but Gobra doesn't yet. This PR introduces a library that encodes permission introspection and drops the use of inhales that were used before to provide a concrete permission value to locations for which we only had wildcard permission, so that we could perform operations such as
copyandappend.