Adapt to new version of z3 (4.16) and Viper (2026.09) - #438
Merged
Conversation
Four lemmas that transfer a property of a byte slice to a prefix of it, or back, stopped verifying with the current Gobra (latest silver/silicon, Z3 4.16). All four hold two overlapping `sl.Bytes` predicates over the same bytes and compare two applications of a pure function that reads those bytes, one through each predicate. The two predicate snapshots are distinct symbolic values, and the backend no longer relates them on the shared locations on its own. `IsSupportedPktSubslice` and `GetPathTypeSubslice` now read each byte the compared functions depend on through both slices while the predicates are unfolded, which forces the snapshots to agree on it: the next header and the path type for the former, the path type for the latter. `ValidPktMetaHdrSublice` already asserted that the meta header bytes are the same locations; it now also asserts that they hold the same values. `ValidHeaderOffsetFromSubSliceLemma` proved its goal only in the postcondition, after re-folding both predicates, whereas its sibling `ValidHeaderOffsetToSubSliceLemma` asserts the revealed goal while they are unfolded. It now mirrors the sibling: it reveals the hypothesis first and asserts the revealed goal inside the unfolded region. Only ghost code and proof annotations change; no specification is weakened and no non-ghost code is touched. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FRnhzUdVyEKN9NFEqKJyEa
jcp19
changed the title
The router is the only package that overrode `mce_mode` to `on`; every other job in the workflow uses the module default `od`. With the current Gobra (latest silver/silicon, Z3 4.16) that override makes Silicon diverge while exhaling the postcondition of `initMetrics`: one Z3 child grows past 11GB until the kernel kills it, and the package aborts with ProverInteractionFailed: Interaction with prover yielded null after about 22 minutes, both in CI and locally. The divergence is in the exhale itself and scales with its size rather than with any particular conjunct. Verifying `initMetrics` in isolation: - the body, up to and including the closing `assert reveal d.DpAgreesWithSpec(dp)`, takes about three minutes; - asserting each pure postcondition individually just before the exhale is cheap, and does not stop the exhale from diverging; - `ensures d.Mem()` together with any three of the remaining conjuncts is fine, and with any four it diverges -- substituting the trivial `d.InternalConnIsSet()` for the set-valued `0 elem d.DomainForwardingMetrics()` diverges just the same; - the unchanged member verifies in 2m35s under `od`. So no annotation on a single member addresses it, and the only proof-level alternative would be weakening the postcondition that `Run` relies on. `od` applies the more complete exhale on demand, when the ordinary one fails, so dropping the override keeps the completeness the package needs. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FRnhzUdVyEKN9NFEqKJyEa
`EstablishEqAbsHeader` and `AbsPktToSubSliceAbsPkt` both assert p.path.GetBase(ub[start:end]).EqAbsHeader(ub[start:end]) after the `if typeOf(p.scionLayer.Path) == *epic.Path` that relates `ub[start:end]` to `ub`, in the EPIC case through the metadata prefix and otherwise directly. Each branch establishes that relation with its own aliasing assertions, and the assertion after the join relied on the verifier carrying enough of them across it. `--mceMode on` did carry them: its summarising snapshots relate the two `sl.Bytes` predicates over the shared bytes on their own. Under the default `od` they are not related, and both asserts fail. Establishing the assertion separately in each branch, where the branch's own aliasing facts are still in scope, discharges it in both. This is the same gap as the four `sl.Bytes` lemmas fixed earlier on this branch: an assertion that compares two readings of the same bytes through two overlapping predicates has to relate them explicitly rather than leave it to the backend. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FRnhzUdVyEKN9NFEqKJyEa
The precondition of `doXover` compares `p.path.GetBase(ubScionPath)` with the
`currBase` captured before `scionLayer.Mem` and, for EPIC packets, the EPIC
path's own `Mem` are folded back:
unfolding acc(p.scionLayer.Mem(ub), _) in
(typeOf(p.scionLayer.Path) == (*epic.Path) ?
unfolding acc(p.scionLayer.Path.Mem(ubPath), _) in
p.path.GetBase(ubScionPath) == currBase :
p.path.GetBase(ubScionPath) == currBase)
The call site folded the EPIC path inside a `ghost if` and `scionLayer.Mem`
after it, leaving that comparison to be discharged once, after the join.
`--mceMode on` related the value read through the re-folded predicates to
`currBase`; the default `od` does not.
Fold `scionLayer.Mem` inside each branch instead and assert the branch's own
half of the precondition there, matching the shape of the two lemmas in
`io-spec-lemmas.gobra`.
Verification of `process` under `od` is still running; if this does not
discharge it, the commit is amended rather than followed by a fix-up.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FRnhzUdVyEKN9NFEqKJyEa
Without a bound, an assertion whose proof the prover cannot find does not fail: the prover grows until the kernel kills it, Silicon reports ProverInteractionFailed: Interaction with prover yielded null and the whole package aborts with no source position, hiding both the culprit and every member after it. That is how the `initMetrics` divergence presented, and it cost a full CI run and about twenty minutes to locate. 45s is far above what the slowest assertions in this repository need -- the router, its heaviest package, verifies every member well inside it -- so the bound catches divergence rather than slow machines. Gobra's own test suite adopted the same guard, at 20s, when it upgraded Z3. This is a guard, not a fix: a bounded assertion that times out still fails verification. It makes the next divergence a localized error in one run instead of an opaque crash. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FRnhzUdVyEKN9NFEqKJyEa
Dropping the router's `mce_mode: on` fixed the `initMetrics` divergence but made the package too slow: CI did not finish it within its 6h budget, and it also cost four proofs elsewhere that the more complete exhale had been discharging on its own. Silicon takes the exhale mode per member, and Gobra can attach it, so the package keeps `mce_mode: on` and `initMetrics` alone asks for the on-demand mode with `#backend[exhaleMode(2)]`. That is the mode under which the method was shown to verify, and it leaves every other member on the setting the router has always used. Reverts the two changes that only existed to support the package-wide switch: the per-branch header equality in `EstablishEqAbsHeader` and `AbsPktToSubSliceAbsPkt`, and the per-branch `doXover` precondition in `process`. Those assertions are discharged by the more complete exhale, which those members keep. The four `sl.Bytes` lemmas fixed earlier on this branch are unaffected: they are in `pkg/slayers` and `pkg/slayers/path/scion`, which never used the more complete exhale, and they fail under every mode without the fix. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FRnhzUdVyEKN9NFEqKJyEa
jcp19
marked this pull request as ready for review
September 4, 2026 08:05
jcp19
pushed a commit
that referenced
this pull request
Sep 4, 2026
Brings in the JSON-config workflow (#429), the bodied ToSeqByte (#432), EPIC packets as supported packets in the IO spec (#436), the explicit processSCION postcondition (#437) and the z3 4.16 / Viper 2026.09 adaptation (#438), and ports them to the view-based specs of this branch: - The workflow adopts the per-package config files; the scion path package keeps its temporarily raised 45m budget. - ToSeqByte stays defined through sl.View, and the subslice lemmas of the scion path and slayers packages keep their seq[byte] form, so the byte-snapshot fixes of #438 do not apply to them. - IsSupportedPkt accepts EPIC packets; the !IsSupportedPkt premise of processEPIC and the matching assert in processPkt are dropped. - The new IsXoverLemma, LastHopNotXoverLemma and AbsIsXoverLemma, the xover clauses of LastHopLen and LocalDstLemma, and the PktUpdate postconditions of processPkt, processSCION, processEPIC and process are expressed over sl.View(ub, 0, len(ub)) instead of the raw bytes. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
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.