From 503b61e4a51323597618d5968df2e6029586ab62 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 18 Aug 2026 10:35:48 +0000 Subject: [PATCH 1/3] Document what breaks when non-linear arithmetic is disabled 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 Claude-Session: https://claude.ai/code/session_01QsWWKHMTrgrprseiCdh59g --- .../notes/disabling-nonlinear-arithmetic.md | 177 ++++++++++++++++++ 1 file changed, 177 insertions(+) create mode 100644 verification/notes/disabling-nonlinear-arithmetic.md diff --git a/verification/notes/disabling-nonlinear-arithmetic.md b/verification/notes/disabling-nonlinear-arithmetic.md new file mode 100644 index 000000000..87f559fb3 --- /dev/null +++ b/verification/notes/disabling-nonlinear-arithmetic.md @@ -0,0 +1,177 @@ +# Disabling non-linear arithmetic (`--disableNL`) + +**Question.** Does VerifiedSCION still verify if we switch off Gobra's non-linear +arithmetic entirely? + +**Answer.** No. 17 of the 20 verification jobs in `.github/workflows/gobra.yml` +pass unchanged, but three fail with 15 errors in total. Every one of those errors +comes from Viper's *permission* algebra, not from the integer arithmetic of the +SCION proofs. + +## How to reproduce + +Append `--disableNL` to `default_job_cfg.other` in `gobra-mod.json`; it is +inherited by every package, since no `gobra.json` overrides it (job-level config +is merged with `orElse` over the module-level one). Then run each job as CI does: + +```sh +java -Xss1g -Xmx4g -jar gobra.jar --config +``` + +The numbers below were produced with Gobra `d5f487c` and Z3 4.8.7 (the version +the CI image pins), on a 4-vCPU/15 GB machine comparable to a GitHub runner, +against VerifiedSCION `7f39fa4`. Jobs were run sequentially; timings are single +samples and should be read as indicative. + +## Results + +| job | baseline | `--disableNL` | +| --- | --- | --- | +| `verification` (recursive) | PASS 121s | **FAIL — 1 error** | +| `verification/dependencies/.../gopacket/layers` | PASS | PASS | +| `pkg/addr` | PASS | PASS | +| `pkg/experimental/epic` | PASS | PASS | +| `pkg/log` | PASS | PASS | +| `pkg/private/serrors` | PASS | PASS | +| `pkg/scrypto` | PASS | PASS | +| `pkg/slayers` | PASS 186s | PASS 188s | +| `pkg/slayers/path` | PASS 60s | PASS 58s | +| `pkg/slayers/path/empty` | PASS 33s | PASS 34s | +| `pkg/slayers/path/epic` | PASS 53s | PASS 52s | +| `pkg/slayers/path/onehop` | PASS 50s | PASS 49s | +| `pkg/slayers/path/scion` | PASS 306s | PASS 313s | +| `private/topology` | PASS | PASS | +| `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** | + +### The 15 errors + +All of them are "might not suffice" on a resource held with a wildcard: + +- `verification/utils/monoset/monoset.gobra:79` — `unfold acc(b.Contains(i), _)` + in `PromoteContains`; `Contains` holds `acc(b.valuesMap[i], _)`. +- `private/underlay/conn/conn_spec.gobra:80,97,115,166,183,201` — all six are + `fold acc(c.connUDPBase.Mem(), _)`; `Mem`/`MemWithoutConn` hold + `acc(c.Listen.Mem(), _)` and `acc(c.Remote.Mem(), _)`. +- `router/dataplane.go:1766,1837,2800,3712,4439,4609` and + `router/dataplane_spec.gobra:128,374` — wildcard folds/unfolds of `d.Mem()`, + `accBatchConn`, `accAddr`, `forwardingMetricsInv`, `macFactoryInv`, and calls + whose preconditions need `acc(..., _)`. + +## Root cause + +Folding or unfolding a predicate held with amount `p` scales every `acc(x.f, q)` +in its body to `PermTimes(q, p)` (`rules/Producer.scala`, `rules/Consumer.scala`). +So: + +- `q` a literal, `p` symbolic gives `1/2 * w` — linear, unaffected. +- `q` and `p` both wildcards gives `w1 * w2` — a product of two symbolic + variables. + +The trigger is therefore *nested* wildcards specifically: holding `acc(P(), _)` +where `P`'s body itself contains `acc(..., _)`. This 12-line Viper file, the +shape of `monoset.PromoteContains`, reproduces the whole thing — it verifies +normally and fails under `--disableNL`: + +```viper +field f: Int +predicate P(x: Ref) { acc(x.f, wildcard) } + +method promote(x: Ref) + requires acc(P(x), wildcard) + ensures acc(P(x)) +{ unfold acc(P(x), wildcard); fold acc(P(x)) } +``` + +`--proverLogFile` shows the goal that flips, and there is no integer in it: + +```smt2 +(assert ($Perm.isReadVar $k@5@04)) ; k5 >= 0 /\ k5 != 0 +(assert ($Perm.isReadVar $k@6@04)) ; k6 >= 0 /\ k6 != 0 +(assert (<= $Perm.No (* $k@6@04 $k@5@04))) +(assert (<= (* $k@6@04 $k@5@04) $Perm.Write)) +(assert (not (not (= (* $k@6@04 $k@5@04) $Perm.No)))) ; refute k6*k5 = 0 +(check-sat) +``` + +Replaying that script gives `unsat` with `smt.arith.nl=true` and `unknown` with +`smt.arith.nl=false`. + +Note that "non-linear *integer* arithmetic", as both Gobra's and Silicon's help +texts put it, is a misnomer. `--disableNL` emits `(set-option :smt.arith.nl +false)`, which Z3 documents as "(incomplete) nonlinear arithmetic support based +on Groebner basis and interval propagation" — a switch on the arithmetic solver +as a whole, with no sort restriction. Silicon declares `(define-sort $Perm () +Real)`, so wildcard products are non-linear *real* arithmetic and fall under the +same switch. Z3 does not lose product reasoning outright: posed standalone, the +goal above is still discharged by cheap sign propagation. What it loses is the +systematic machinery, so in a full query context it no longer finds the proof. + +## Mitigations evaluated + +### Rewrite the specs to avoid nested wildcards — does not work as-is + +Replacing the nested wildcards in `connUDPBase.Mem()`/`MemWithoutConn()` with a +fixed fraction (`R55`) removes all 6 original errors and introduces 3 new ones: + +- `conn.go:431,440` — `LocalAddr`/`RemoteAddr` `unfold acc(c.MemWithoutConn(), + R16)`, `defer fold`, and still `ensures u != nil ==> acc(u.Mem(), _)`. Handing + a copy out *and* folding back works only because the inner wildcard makes the + resource duplicable; a fixed fraction is consumed by the re-fold. +- `conn.go:391` — `fold cc.Mem()` at construction, where `laddr.Mem()` arrives as + a wildcard from the caller and cannot yield a fixed `R55`. + +The nested wildcard encodes "duplicable, no accounting". Substituting a constant +moves the obligation to the producer side, and fixing that propagates outward +through every caller. + +### Silicon's `--unsafeWildcardOptimization` + +`WildcardSimplifyingPermTimes` (`state/Terms.scala`) rewrites `w1 * w2` to +whichever variable has the smaller id and `w * literal` to `w`, so no product +reaches Z3. It keeps exact arithmetic for locations mentioned under `perm(loc)` +(`DefaultMainVerifier.scala`); VerifiedSCION has no Viper-level `perm(loc)` in +its specs, so the unsafe case appears inapplicable here. + +### Permission-product axioms in Silicon's preamble + +The products only need positivity and monotonicity, which can be stated as +quantified assertions and matched on `(* p1 p2)` even with the NL solver off: + +```smt2 +(assert (forall ((p1 $Perm) (p2 $Perm)) (! + (=> (and (< $Perm.No p1) (< $Perm.No p2)) (< $Perm.No (* p1 p2))) + :pattern ((* p1 p2)) :qid |perm-times-pos|))) +``` + +plus `(* p1 p2) <= p2` when `p1 <= 1`, and the symmetric variant. Unlike the +option above this is sound rather than an approximation, and costs nothing when +NL is on. It would belong upstream in Silicon, gated on `disableNL`. + +Both mitigations fix the two smaller jobs under `--disableNL`: + +| job | `--disableNL` | + `unsafeWildcardOptimization` | + preamble axioms | +| --- | --- | --- | --- | +| `private/underlay/conn` | FAIL (6) | PASS 40s | PASS 32s | +| `verification` | FAIL (1) | PASS 98s | PASS 85s | + +## Performance + +Disabling NL neither breaks nor speeds up the `slayers` tree. Sequential runs on +an idle machine, single sample each: + +| package | baseline | `--disableNL` | + `unsafeWildcardOpt` | + axioms | +| --- | --- | --- | --- | --- | +| `pkg/slayers` | 186s | 188s | 187s | 179s | +| `pkg/slayers/path` | 60s | 58s | 58s | 61s | +| `pkg/slayers/path/empty` | 33s | 34s | 33s | 31s | +| `pkg/slayers/path/epic` | 53s | 52s | 54s | 54s | +| `pkg/slayers/path/onehop` | 50s | 49s | 50s | 50s | +| `pkg/slayers/path/scion` | 306s | 313s | 273s | 295s | +| **total** | **688s** | **694s** | **655s** | **670s** | + +All cells pass. The spread is within single-sample noise on this machine. From 71e3d91895d8d0e3bbb2a3deb46feed5b7ee0b93 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 18 Aug 2026 12:47:36 +0000 Subject: [PATCH 2/3] Disable non-linear arithmetic where the proofs do not need it 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 Claude-Session: https://claude.ai/code/session_01QsWWKHMTrgrprseiCdh59g --- pkg/addr/gobra.json | 3 ++ pkg/experimental/epic/gobra.json | 3 ++ pkg/log/gobra.json | 3 ++ pkg/private/serrors/gobra.json | 3 ++ pkg/scrypto/gobra.json | 3 ++ pkg/slayers/gobra.json | 3 ++ pkg/slayers/path/empty/gobra.json | 3 ++ pkg/slayers/path/epic/gobra.json | 3 ++ pkg/slayers/path/gobra.json | 3 ++ pkg/slayers/path/onehop/gobra.json | 3 ++ pkg/slayers/path/scion/gobra.json | 3 ++ private/topology/gobra.json | 3 ++ private/topology/underlay/gobra.json | 3 ++ private/underlay/sockctrl/gobra.json | 3 ++ router/bfd/gobra.json | 3 ++ router/control/gobra.json | 3 ++ .../google/gopacket/layers/gobra.json | 3 ++ .../notes/disabling-nonlinear-arithmetic.md | 29 +++++++++++++++++++ 18 files changed, 80 insertions(+) create mode 100644 pkg/addr/gobra.json create mode 100644 pkg/experimental/epic/gobra.json create mode 100644 pkg/log/gobra.json create mode 100644 pkg/private/serrors/gobra.json create mode 100644 pkg/scrypto/gobra.json create mode 100644 pkg/slayers/gobra.json create mode 100644 pkg/slayers/path/empty/gobra.json create mode 100644 pkg/slayers/path/epic/gobra.json create mode 100644 pkg/slayers/path/gobra.json create mode 100644 pkg/slayers/path/onehop/gobra.json create mode 100644 pkg/slayers/path/scion/gobra.json create mode 100644 private/topology/gobra.json create mode 100644 private/topology/underlay/gobra.json create mode 100644 private/underlay/sockctrl/gobra.json create mode 100644 router/bfd/gobra.json create mode 100644 router/control/gobra.json create mode 100644 verification/dependencies/github.com/google/gopacket/layers/gobra.json diff --git a/pkg/addr/gobra.json b/pkg/addr/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/pkg/addr/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/pkg/experimental/epic/gobra.json b/pkg/experimental/epic/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/pkg/experimental/epic/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/pkg/log/gobra.json b/pkg/log/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/pkg/log/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/pkg/private/serrors/gobra.json b/pkg/private/serrors/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/pkg/private/serrors/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/pkg/scrypto/gobra.json b/pkg/scrypto/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/pkg/scrypto/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/pkg/slayers/gobra.json b/pkg/slayers/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/pkg/slayers/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/pkg/slayers/path/empty/gobra.json b/pkg/slayers/path/empty/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/pkg/slayers/path/empty/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/pkg/slayers/path/epic/gobra.json b/pkg/slayers/path/epic/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/pkg/slayers/path/epic/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/pkg/slayers/path/gobra.json b/pkg/slayers/path/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/pkg/slayers/path/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/pkg/slayers/path/onehop/gobra.json b/pkg/slayers/path/onehop/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/pkg/slayers/path/onehop/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/pkg/slayers/path/scion/gobra.json b/pkg/slayers/path/scion/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/pkg/slayers/path/scion/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/private/topology/gobra.json b/private/topology/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/private/topology/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/private/topology/underlay/gobra.json b/private/topology/underlay/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/private/topology/underlay/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/private/underlay/sockctrl/gobra.json b/private/underlay/sockctrl/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/private/underlay/sockctrl/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/router/bfd/gobra.json b/router/bfd/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/router/bfd/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/router/control/gobra.json b/router/control/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/router/control/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/verification/dependencies/github.com/google/gopacket/layers/gobra.json b/verification/dependencies/github.com/google/gopacket/layers/gobra.json new file mode 100644 index 000000000..7e4388591 --- /dev/null +++ b/verification/dependencies/github.com/google/gopacket/layers/gobra.json @@ -0,0 +1,3 @@ +{ + "other": ["--disableNL"] +} diff --git a/verification/notes/disabling-nonlinear-arithmetic.md b/verification/notes/disabling-nonlinear-arithmetic.md index 87f559fb3..5fe21bfa9 100644 --- a/verification/notes/disabling-nonlinear-arithmetic.md +++ b/verification/notes/disabling-nonlinear-arithmetic.md @@ -175,3 +175,32 @@ an idle machine, single sample each: | **total** | **688s** | **694s** | **655s** | **670s** | All cells pass. The spread is within single-sample noise on this machine. + +## Adopted configuration + +The 17 jobs that pass now opt in individually, through a `gobra.json` next to the +package: + +```json +{ + "other": ["--disableNL"] +} +``` + +`verification`, `private/underlay/conn` and `router` deliberately have no such +entry and keep non-linear arithmetic. + +Opting in per package, rather than setting the flag once in `gobra-mod.json` and +exempting the three, is forced by how the option is defined. `disableNL` is an +`opt[Boolean]` with no `--nodisableNL` counterpart, and it is folded in with +`disableNL || input.disableNL.value.contains(true)`, so once the module config +sets it no job can clear it. The merge itself would allow an override — job and +module configs are combined field-wise with `orElse`, and `toInputConfigOption` +records a value only when the option `isSupplied`, which is also why a job +`other` list does not disturb the module-level options it omits — but there is +no way to *supply* `false`. + +A structured `disable_nl: Option[Boolean]` field in `VerificationJobCfg` would +remove that restriction and shrink this to four files: one `true` in +`gobra-mod.json` and three `false` overrides. That is a Gobra change, so it +cannot land here first. From 95b0fb22cbaf8161adc503be5d78516457781e6d Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 18 Aug 2026 14:13:10 +0000 Subject: [PATCH 3/3] Record the router results for both wildcard mitigations --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 Claude-Session: https://claude.ai/code/session_01QsWWKHMTrgrprseiCdh59g --- .../notes/disabling-nonlinear-arithmetic.md | 23 ++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/verification/notes/disabling-nonlinear-arithmetic.md b/verification/notes/disabling-nonlinear-arithmetic.md index 5fe21bfa9..a79f07fb4 100644 --- a/verification/notes/disabling-nonlinear-arithmetic.md +++ b/verification/notes/disabling-nonlinear-arithmetic.md @@ -152,12 +152,15 @@ plus `(* p1 p2) <= p2` when `p1 <= 1`, and the symmetric variant. Unlike the option above this is sound rather than an approximation, and costs nothing when NL is on. It would belong upstream in Silicon, gated on `disableNL`. -Both mitigations fix the two smaller jobs under `--disableNL`: +Both mitigations fix the two smaller jobs under `--disableNL`, and +`unsafeWildcardOptimization` fixes `router` as well, so the approach is not +limited to small proofs: | job | `--disableNL` | + `unsafeWildcardOptimization` | + preamble axioms | | --- | --- | --- | --- | | `private/underlay/conn` | FAIL (6) | PASS 40s | PASS 32s | | `verification` | FAIL (1) | PASS 98s | PASS 85s | +| `router` | FAIL (8) | PASS 4442s | not measured | ## Performance @@ -176,6 +179,24 @@ an idle machine, single sample each: All cells pass. The spread is within single-sample noise on this machine. +The router tells the same story. Switching non-linear arithmetic off does not +make it cheaper -- the one configuration that both verifies and disables NL is +slightly more expensive than what CI runs today: + +| router config | result | time | +| --- | --- | --- | +| current (NL on) | PASS | 4157s | +| `--disableNL` | FAIL, 8 errors | 1264s (abandons members after the first error) | +| `--disableNL --unsafeWildcardOptimization` | PASS | 4442s | + +Single samples, so +285s is better read as "no faster, perhaps a few percent +slower" than as a precise figure. Either way there is no performance argument +for disabling NL; the reasons to want it would be determinism or a stricter +prover configuration. + +The run is also badly tail-bound: 9 of the 10 chop tasks finish in the first +~20 minutes and one task accounts for the rest, in both configurations. + ## Adopted configuration The 17 jobs that pass now opt in individually, through a `gobra.json` next to the