Repository navigation
Conversation
Gobra can restrict verification to the members declared on a given line (`-i <file>@<line>`), after which the chopper keeps only the slice of the program that those members need. That is the only practical way to attribute the run time of a package to individual functions, which is what one needs when a package takes hours to verify. The script resolves a member *name* to its declaration line (top-level functions and named closure literals alike) and reconstructs the options that the CI uses from 'gobra-mod.json' and the package's 'gobra.json'. Isolation cannot currently be expressed in the JSON configuration itself: 'input_files' makes Gobra fail with an internal error and '-i' is rejected inside 'other', so the script assembles a full command line instead. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z
Verifying each member on its own (see verification/scripts/verify-member.py) gives, on a 4-core machine: Run 2.8 min, processOHP 5.5 min, processPkt 5.7 min, doXover 12 min, the 'rc' closure of Run 26 min and process 109 min. Gobra's front end accounts for about 2.5 min of each of those. Cutting the body of a member short with TODO() shows that the two worst members are worst for different reasons. About 60% of doXover's solver time goes on its own contract - proving its 26 'ensures' clauses well defined before the body starts, and exhaling them at the single successful exit - while the assertions in the middle of the body are free. process's contract is cheap; its body exchanges 568 specification clauses with the seventeen methods it calls, nine of which repeat eleven literally identical clauses. The 'rc' closure has no postcondition at all: all of its time is in the two nested loops, whose invariants quantify over the 64-message batch. The backend options are not the problem: mce_mode 'od', joining all branches and the greedy QP exhale were each measured and each made things worse than what router/gobra.json already asks for. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z
…iled
Cutting the body short with TODO() localises 'process': four fifths of its
109 minutes are in its last 130 lines - the two egress branches with their
IO-spec events, the reveals of PktUpdate/absIO_val, and the three exits -
which sit after the 'IsXover' branch and are therefore explored once per side
of it.
Six interventions were implemented, verified and timed against that, and none
of them moved the number:
- mce_mode 'od' instead of 'on'
- joining every branch, on doXover and on process
- the greedy QP exhale
- deleting the assertions doXover repeats
- replacing doXover's repeated epic case split by a ghost boolean
- naming repeated (nested) applications in the contracts of doXover and of
the XoverEvent/ExternalEnterOrExitEvent lemmas
The last group is the informative one: Silicon evaluates a heap-dependent
function once per heap snapshot rather than once per mention, so collapsing
repeated applications buys nothing. What is expensive is the size and
fragmentation of the symbolic state, so the remaining candidates are the ones
that shrink it - bundling the resource footprint the validators share, and the
per-message resources in the read closure's loop invariants, into predicates.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z
'process' verifies in 3729 s instead of 7854 s - a paired A/B, both arms reporting 0 errors. Every check that 'process' performs has to carry the last decoded layer, so that it can answer with an SCMP message, even though only 'packSCMP' and 'handleSCMPTraceRouteRequest' look at it. Spelled out, that is four clauses - two of them impure implications, which Silicon branches on and re-joins at every exhale and every inhale - repeated in the contract of fourteen members and exchanged twice at each of the seventeen calls along 'process's path. 'process', 'processSCION' and 'processEPIC' carried the same thing in a worse spelling: an implication nested inside an implication, keyed on an 'llIsNil' flag. 'LastLayerMem' bundles it into a single chunk. Nothing new is proved: the predicate body is the same conjunction, and the 'llIsNil' case split was only a second spelling of 'p.lastLayer.Mem(ubLL)' with 'ubLL == nil' folded into the flag, so the flag is replaced by the buffer itself. The only clause dropped rather than moved is 'startLL == 0 && endLL == len(ub)' in 'process's SCION-layer case, which no caller used. Where the fold goes is the whole trick. Folding inside 'process' costs about 1200 s on its own, because the predicate then has to be re-derived from the ghost parameters, down to a slice identity 'ub[0:len(ub)] === ub'. Folding in 'processPkt' instead, right after 'decodeLayers' produced the layer and while the facts about it are still immediate, is free: 350 s against a 342 s baseline. All eighteen affected members were verified in isolation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z
Every check along 'process's path carries the buffer that an SCMP reply is serialized into, even though only 'packSCMP' writes to it: four clauses - two 'requires' and two 'ensures' - exchanged at each of seventeen members. Collapse the three that describe the buffer itself into a predicate, so that each member states 'preserves p.SCMPBufMem()' instead. The permission to the buffer's bytes deliberately stays outside: postconditions such as respr.OutPkt != nil ==> !slayers.IsSupportedPkt(respr.OutPkt) need 'sl.Bytes(respr.OutPkt, ..)' at write permission to be well-defined, and a predicate cannot frame a clause stated outside it. Restating those under an 'unfolding' would cost more than the bundling saves, so they keep a separate 'preserves' clause, now phrased with the new 'OutBuf' getter rather than by reaching through 'p.buffer'. Verified in isolation: packSCMP, validateHopExpiry and processPkt, 0 errors. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z
Paired A/B on 'process', both arms 0 errors: 2490 s without the predicate against 2497 s with it. The bundling is a wash, and unlike 'LastLayerMem' it cannot be made to pay: the clauses it collapses are plain conjunctions, and what Silicon charges for is the impure implications that 'LastLayerMem' removed. The finding is worth keeping even though the code is not, so PERFORMANCE.md records why the buffer resists the same treatment - the postconditions that describe the SCMP reply need 'sl.Bytes(respr.OutPkt, ..)' framed by the contract itself, so the permission cannot move inside a predicate. This reverts commit d3f01b9. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z
Two findings from the attempt that was just reverted: the bundling is a wash because the clauses it collapses contain no impure implications, and the permission to the buffer's bytes cannot move inside a predicate at all, because the postconditions that describe the SCMP reply are stated over the result and need that permission framed by the contract itself. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z
Cutting inside the two nested loops shows that the invariants are cheap to establish and to inhale - both loops entered with their bodies skipped is still the front-end floor - and that the call to 'processPkt' is free despite its contract. What costs is a single step: exhaling the inner loop's twenty-five invariants on the fall-through path at the end of the body, ~1160 s of the closure's 2186 s. That sharpens the remaining candidate. Bundling the per-message invariants only pays if the predicate is closed by a lemma rather than a fold, so that the quantified reasoning over the 64-message batch happens in a member that holds nothing but the batch, instead of over everything the loop body has accumulated. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z
Half of the packet loop was a single step: exhaling the inner loop's twenty-five invariants on the fall-through path at the end of its body, over everything the body had accumulated by then. Six of those invariants are quantified over the 64-message batch - two permissions and the four pure facts that only those permissions can frame, so they have to travel together - and they are what made that exhale expensive. 'MsgsMem' bundles the six, and the loop exchanges one chunk instead. The batch is opened and closed by lemmas rather than by an 'unfold' and a 'fold' in the body, which is the point: the quantified reasoning then happens in a member whose state holds nothing but the batch. Isolated verification of the closure goes from 1538 s to 384 s in a paired A/B, both arms reporting 0 errors. The 'excl' parameter of 'MsgsMemHole' is what makes putting a message back provable. Both quantified permissions are keyed on 'msgs[i].GetFstBuffer()', so every fold obliges Silicon to show that no two messages share a buffer. Inside the batch that is free, since '--assumeInjectivityOnInhale' asserts it whenever the permission is inhaled, but the message that has been taken out is no longer part of any such inhale. Naming its buffer in the predicate carries the one missing inequality across the hole. Nothing is proved that was not proved before. The predicate bodies are the same six assertions, and 'PutMsg' gives back deliberately less than 'TakeMsg' handed out - the body consumes the message's address and forwards its bytes - which is why the predicate is indexed by the current position. That also retires the assertion marked as crucial for stability: it existed only to re-establish the invariant for the next iteration, which the closing lemma now proves. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z
The paired A/B (1538 s -> 384 s on the rc closure), why the lemmas rather than the predicate are the point, why putting a message back needs its buffer named, and the per-element formulation that fixed the same obligation in the wrong place. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z
Master's #433 renamed 'absPkt' to 'AbsPkt' and 'absIO_val' to 'AbsIO_val' for Go's visibility rules, on the very contract lines that 'LastLayerMem' replaces. The three conflicts are resolved by keeping the predicate and taking master's names. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z
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.
Summary
This PR significantly improves the verification performance of the router package by bundling frequently-exchanged contract clauses into reusable predicates. The changes reduce verification time for critical functions by 2-4x through better state management and reduced quantified reasoning overhead.
Key Changes
Added
MsgsMempredicate (msgs-spec.gobra): Bundles six quantified invariants of the message batch processing loop into a single predicate chunk. This reduces the cost of exhaling invariants at the end of the inner loop body from ~1160s to ~230s by moving quantified reasoning into dedicated lemmas (TakeMsg/PutMsg) that operate on smaller states.Added
LastLayerMempredicate (dataplane_spec.gobra): Consolidates four clauses (including two impure implications) that describe the last decoded layer into a single predicate. This eliminates repeated branching on implications at every exhale/inhale across seventeen method calls. Folding happens inprocessPktimmediately after decoding, where re-deriving facts is cheap, rather than inprocesswhere it would be expensive.Updated
dataplane.go:MsgsMempredicate into the packet processing loop withTakeMsg/PutMsglemma callsllIsNilboolean parameter with explicitubLLbuffer parameter inprocessSCION/processEPICLastLayerMemat strategic pointsAdded verification tooling (
verification/scripts/verify-member.py): New script for measuring individual member verification time in isolation, enabling precise performance profiling and regression detection.Added performance documentation (
verification/PERFORMANCE.md): Comprehensive analysis of router verification costs, including:Performance Impact
rcclosure (packet loop): 1538s → 384s (4.0x faster)processfunction: 7854s → 3729s (2.1x faster)Implementation Details
The optimization strategy focuses on reducing the number of distinct symbolic states in which contract clauses must be framed, rather than reducing clause count. Key insights:
LastLayerMeminprocessPkt(where facts are immediate) costs ~350s vs ~1200s if folded inprocessThe changes are verified to produce identical proofs (0 errors) while dramatically improving solver performance.
https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z