Disable non-linear arithmetic in 17 verification packages - #435
Draft
jcp19 wants to merge 3 commits into
Draft
Conversation
Records an experiment replaying all 20 Gobra jobs from the CI workflow with --disableNL added to gobra-mod.json. Seventeen pass unchanged; verification, private/underlay/conn and router fail with 15 errors between them. Every error comes from Viper's permission algebra rather than from integer arithmetic in the SCION proofs: folding or unfolding a predicate held with acc(P(), _) whose body also holds acc(..., _) scales one wildcard by another, and Z3 stops discharging the resulting product once smt.arith.nl is off. The note pins this down with a 12-line Viper reproduction and the SMT goal that flips, and evaluates three ways around it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QsWWKHMTrgrprseiCdh59g
Seventeen of the twenty Gobra jobs in the CI workflow verify unchanged with Z3's non-linear arithmetic switched off. Each of them now opts in through a gobra.json holding `--disableNL`. The three that are left alone -- verification, private/underlay/conn and router -- fail without it, in every case because folding or unfolding a predicate held with acc(P(), _) whose body also holds acc(..., _) scales one wildcard by another, and Z3 stops discharging that product. The accompanying note records the analysis. Opting in per package is forced by the option itself: disableNL has no --nodisableNL counterpart and is folded in disjunctively, so a flag set once in gobra-mod.json could not be cleared for the three exceptions. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QsWWKHMTrgrprseiCdh59g
jcp19
commented
Aug 18, 2026
Comment on lines
+44
to
+49
| | `private/topology/underlay` | PASS | PASS | | ||
| | `private/underlay/conn` | PASS 44s | **FAIL — 6 errors** | | ||
| | `private/underlay/sockctrl` | PASS | PASS | | ||
| | `router/bfd` | PASS | PASS | | ||
| | `router/control` | PASS | PASS | | ||
| | `router` | PASS 4157s | **FAIL — 8 errors, 1264s** | |
Collaborator
Author
There was a problem hiding this comment.
This file can be dropped
--unsafeWildcardOptimization also clears the router's 8 errors, so the approach is not limited to the two small jobs. It is not a speed-up though: the router takes 4442s with it against 4157s for the configuration CI runs today, which matches the slayers numbers, where all four configurations landed within noise of each other. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QsWWKHMTrgrprseiCdh59g
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 change disables Gobra's non-linear arithmetic (
--disableNL) for 17 of 20 verification packages by addinggobra.jsonconfiguration files. Three packages (verification,private/underlay/conn, androuter) retain non-linear arithmetic support due to nested wildcard permission patterns in their specifications that require it.Key Changes
Added a comprehensive analysis document (
verification/notes/disabling-nonlinear-arithmetic.md) documenting:Added
gobra.jsonconfiguration files to 17 packages with--disableNLflag:pkg/addr,pkg/experimental/epic,pkg/log,pkg/private/serrors,pkg/scryptopkg/slayersand all its subpackages (path,path/empty,path/epic,path/onehop,path/scion)private/topology,private/topology/underlay,private/underlay/sockctrlrouter/bfd,router/controlverification/dependencies/github.com/google/gopacket/layersImplementation Details
acc(x.f, _)expressions to products of symbolic variables (w1 * w2), which requires non-linear real arithmetic support in Z3disableNLoption lacks a counterpart to re-enable it at the job levelpkg/slayerstreehttps://claude.ai/code/session_01QsWWKHMTrgrprseiCdh59g