Use new support for invariants - #428
Conversation
Resolves conflicts by keeping the native-invariants approach
(Invariant/EstablishInvariant/critical blocks) while adopting the new
predicate expression instance syntax SharedInv{...} introduced on master
(#416). Also migrates the new processEPIC (#261) from the ghost mutex to
invariants and removes the now-unused ghost_sync package.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012eBw3LWL6qAVMS4aLVW5ks
478cabf to
a923d62
Compare
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RtaS6t2NWpe3WRn6w9gXz4
Gobra does not allow interface methods to be marked as `atomic`, so calls to
`BatchConn.ReadBatch` and `BatchConn.WriteBatch` may not occur inside a critical
region. As a consequence, the caller can no longer perform the transitions of
the IO specification atomically with the physical read/write.
Instead, we now assume that both methods open the shared invariant themselves
and perform the corresponding transitions internally, atomically with the
respective physical operation. Their contracts take `Invariant(SharedInv{...})`
instead of the `io.token` and, in exchange:
- `ReadBatch` returns the sequence of abstract values of the packets that were
received together with a witness for each of them, which makes the prophecy
over the number of received packets unnecessary;
- `WriteBatch` requires the witness that the packet being sent is in the output
buffer of the model, which is what is needed to establish the guard of the
`send` transition.
The `MultiReadBio` definitions are kept, as they specify the effect that
`ReadBatch` is assumed to have on the shared invariant.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RtaS6t2NWpe3WRn6w9gXz4
| // Multi recv event | ||
| // @ ghost ioLock.Lock() | ||
| // @ unfold SharedInv{dp, ioSharedArg}() | ||
| // @ ghost t, s := *ioSharedArg.Place, *ioSharedArg.State | ||
| // @ ghost numberOfReceivedPacketsProphecy := AllocProphecy() | ||
| // @ ExtractMultiReadBio(dp, t, numberOfReceivedPacketsProphecy, s) | ||
| // @ MultiUpdateElemWitness(t, numberOfReceivedPacketsProphecy, ioIngressID, s, ioSharedArg) | ||
| // @ ghost ioValSeq := MultiReadBioIO_val(t, numberOfReceivedPacketsProphecy) | ||
|
|
||
| // @ ghost sN := MultiReadBioUpd(t, numberOfReceivedPacketsProphecy, s) | ||
| // @ ghost tN := MultiReadBioNext(t, numberOfReceivedPacketsProphecy) | ||
| // @ assert dp.dp3s_iospec_ordered(sN, tN) | ||
| // @ BeforeReadBatch: |
There was a problem hiding this comment.
extract this into a lemma that shows that one can always extract the permission to receive various packets from the IO permissions
There was a problem hiding this comment.
Done in ec283f6, as ExtractRecvPermissions in router/dataplane_concurrency_model.gobra.
Note that the block this comment points at no longer exists at the call site: since interface methods cannot be marked atomic, ReadBatch is now assumed to open the shared invariant itself and perform the recv transitions internally, so the critical region around it is gone. I extracted the ghost code into the lemma anyway, because it states exactly the proof obligation underlying that assumption — from the contents of SharedInv{dp, y} for a place t and state s, and for any n, it yields MultiReadBio(t, n), the resulting sN/tN with dp3s_iospec_ordered(sN, tN), the abstract values of the received packets, and a witness for each of them.
The one thing it cannot discharge is advancing the IO token from t to tN, which is the physical reception of the packets; that remains the assumption in ReadBatch's contract. For the same reason the lemma takes the unfolded contents of the invariant rather than Invariant(SharedInv{dp, y}): it cannot close the invariant again, as the token is still at t.
So the lemma is currently a justification rather than something the router applies. If you would rather not carry a lemma with no call site, the alternative is to drop it together with MultiReadBio and friends, which nothing else uses any more — happy to do that instead.
Generated by Claude Code
`ExtractRecvPermissions` shows that the permission to receive an arbitrary number of packets can always be extracted from the IO permissions held by the shared invariant, together with the resulting place and local state and a witness for every received packet. This is the ghost code that used to be inlined in the critical region around `ReadBatch`. It now states the proof obligation underlying the IO specification assumed for `BatchConn.ReadBatch`: everything that `ReadBatch` is assumed to do to the shared invariant follows from the invariant alone, except for advancing the IO token, which is the physical reception of the packets. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RtaS6t2NWpe3WRn6w9gXz4
Conflicts came from #433, which made most of the IO-spec identifiers exported. Resolved by keeping the invariant-based specifications and renaming their identifiers accordingly (io.token -> io.IOToken, dp3s_* -> Dp3s_*, absIO_val -> AbsIO_val, path.ifsToIO_ifs -> path.IfsToIO_ifs, s.ibuf/s.obuf -> s.Ibuf/s.Obuf). verification/utils/ghost_sync stays deleted. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RtaS6t2NWpe3WRn6w9gXz4
The OOB buffers of both the read and the write messages are nil, so all of their Mem() instances and writeMsgInv share the single predicate instance sl.Bytes(nil, 0, 0). After merging master, Gobra stopped being able to add up the shares of that instance held at the end of the loop body and reported that the permission for the fold might not suffice, even though the same fold verifies on both parents of the merge. Provide a fresh instance with sl.NilAcc_Bytes() before the fold, as is already done earlier in the same block. This is sound: the body of sl.Bytes is vacuous for an empty slice, so the instance protects no memory. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RtaS6t2NWpe3WRn6w9gXz4
After merging master, the verification of Run keeps failing on a single permission check, but not always on the same one: first on the fold of writeMsgInv at the end of the loop body, and then, once an extra share of sl.Bytes(nil, 0, 0) was made available there, on the sl.Bytes(ubuf, ...) conjunct of the loop invariant. Making more permission available cannot make a permission check fail, so neither of these is a genuine shortfall; they are assertions that exceed the 45s assert timeout, and which one tips over varies with unrelated perturbations of the proof. Both parents of the merge verify, so raise the timeout for this package rather than weakening any specification. Only assertions that would otherwise be reported as failures are affected, so the effect on the running time of the job is bounded by a couple of minutes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RtaS6t2NWpe3WRn6w9gXz4
|
What happened
Both parents of the merge verify, and the merge is a mechanical resolution: at every conflict I kept the invariant-based side and applied #433's renames, so the code at both failing points is master's modulo The second data point is what settles it. Making more permission available cannot make a permission check fail, so the first error was not a genuine shortfall either — these are assertions exceeding the 45s What I pushed ( Worth noting that this looks like it was already close to the edge on master, so it may flake there too. If you would rather tune Generated by Claude Code |
|
Green on The offer stands to drop the Generated by Claude Code |
2 participants
Supersedes #412