From d0df5e92dff9e66cfdf798ec85e6b8e8f6fdb1c9 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 6 Sep 2026 12:45:59 +0000 Subject: [PATCH 01/10] Add a script to verify a single member of a package Gobra can restrict verification to the members declared on a given line (`-i @`), 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 Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z --- verification/scripts/verify-member.py | 200 ++++++++++++++++++++++++++ 1 file changed, 200 insertions(+) create mode 100755 verification/scripts/verify-member.py diff --git a/verification/scripts/verify-member.py b/verification/scripts/verify-member.py new file mode 100755 index 000000000..fc9ff7e99 --- /dev/null +++ b/verification/scripts/verify-member.py @@ -0,0 +1,200 @@ +#!/usr/bin/env python3 +"""Verify a single member of a package, instead of the whole package. + +Gobra can be told to verify only the members declared on a given line of a file +(``-i @``); the chopper then keeps only the slice of the program that +those members need. That is the only practical way of attributing the run time +of a package to individual functions, which is what one needs when a package +takes hours to verify. + +The line numbers are a poor interface, so this script resolves a member *name* +to the line on which it is declared, and reconstructs the options that the CI +uses from ``gobra-mod.json`` and the package's ``gobra.json``. + + ./verification/scripts/verify-member.py router doXover + ./verification/scripts/verify-member.py router rc # a closure of Run + ./verification/scripts/verify-member.py --list router + +Note that isolation cannot currently be expressed in the JSON configuration: +``input_files`` makes Gobra fail with an internal error and ``-i`` is rejected +inside ``other``. The script therefore assembles a full command line itself, +mirroring what the configuration files say. + +The Gobra binary is taken from ``$GOBRA``; it may be either an executable or a +``.jar`` (in which case it is run with ``java -jar``). ``$Z3_EXE`` is forwarded +to Gobra when it is set. +""" + +import argparse +import json +import os +import re +import shlex +import subprocess +import sys +import time +from pathlib import Path + +REPO = Path(__file__).resolve().parents[2] +MODULE_CFG = REPO / "gobra-mod.json" +JOB_CFG_NAME = "gobra.json" + +# Files that Gobra reads for a package: the sources with a `// +gobra` header +# plus the specification files. Test files are skipped, exactly as Gobra's own +# package resolver does. +SOURCE_SUFFIXES = (".go", ".gobra") + + +def package_files(pkg: Path): + files = [] + for f in sorted(pkg.iterdir()): + if f.suffix not in SOURCE_SUFFIXES or f.name.endswith("_test.go"): + continue + head = f.read_text(errors="replace")[:4096] + if re.search(r"^//\s*\+gobra\s*$", head, re.M): + files.append(f) + return files + + +# A top-level declaration, e.g. +# func (p *scionPacketProcessor) doXover( ... ) +# func newPacketProcessor( ... ) +# or a named function literal, e.g. +# func /*@ rc @*/ (ingressID uint16, ...) +DECL = re.compile(r"^\s*func\s+(?:\([^)]*\)\s*)?(\w+)\s*[({]") +CLOSURE = re.compile(r"^\s*func\s*/\*@\s*(\w+)\s*@\*/") + + +def members(files): + """Map member name -> list of (file, line number).""" + found = {} + for f in files: + for n, line in enumerate(f.read_text(errors="replace").split("\n"), start=1): + m = CLOSURE.match(line) or DECL.match(line) + if m: + found.setdefault(m.group(1), []).append((f, n)) + return found + + +def merged_config(pkg: Path): + """Merge the module-level defaults with the package's own job config. + + Mirrors Gobra's precedence: the job config wins over the module config. + Relative paths are resolved against the directory of the file that + declares them. + """ + module = json.loads(MODULE_CFG.read_text()).get("default_job_cfg", {}) + job_path = pkg / JOB_CFG_NAME + job = json.loads(job_path.read_text()) if job_path.exists() else {} + + def resolve(cfg, base): + cfg = dict(cfg) + if "includes" in cfg: + cfg["includes"] = [str((base / p).resolve()) for p in cfg["includes"]] + return cfg + + merged = resolve(module, MODULE_CFG.parent) + merged.update(resolve(job, pkg)) + # `other` is concatenated rather than overwritten, like Gobra's merge does. + merged["other"] = module.get("other", []) + job.get("other", []) + return merged + + +# JSON field -> how it becomes a command-line option. +FLAGS = { + "assert_timeout": lambda v: ["--assertTimeout", str(v)], + "backend": lambda v: ["--backend", v], + "chop": lambda v: ["--chop", str(v)], + "mce_mode": lambda v: ["--mceMode", v], + "module": lambda v: ["-m", v], + "more_joins": lambda v: ["--moreJoins", v], + "includes": lambda v: ["-I"] + list(v), + "assume_injectivity_inhale": lambda v: ["--assumeInjectivityOnInhale" if v + else "--noassumeInjectivityOnInhale"], + "overflow": lambda v: ["--overflow" if v else "--nooverflow"], + "check_consistency": lambda v: ["--checkConsistency"] if v else [], + "conditionalize_permissions": lambda v: ["--conditionalizePermissions"] if v else [], + "only_files_with_header": lambda v: ["--onlyFilesWithHeader"] if v else [], + "parallelize_branches": lambda v: ["--parallelizeBranches"] if v else [], + "print_vpr": lambda v: ["--printVpr"] if v else [], + "require_triggers": lambda v: ["--requireTriggers"] if v else [], +} + + +def options(cfg): + opts = [] + for key, value in cfg.items(): + if key == "other": + opts += list(value) + elif key in FLAGS: + opts += FLAGS[key](value) + # `project_root` is deliberately dropped: Gobra rejects it together with + # `-i`, and it would withdraw the friend permissions granted to + # `pkg/slayers`. + return opts + + +def gobra_command(): + binary = os.environ.get("GOBRA") + if not binary: + sys.exit("Set $GOBRA to the Gobra executable or to gobra.jar.") + if binary.endswith(".jar"): + return ["java", "-Xss1g", "-Xmx8g", "-jar", binary] + return [binary] + + +def main(): + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("package", help="package directory, e.g. 'router'") + parser.add_argument("member", nargs="?", + help="name of the member to verify; the whole package if omitted") + parser.add_argument("--list", action="store_true", help="list the members and exit") + parser.add_argument("--dry-run", action="store_true", help="print the command and exit") + parser.add_argument("rest", nargs=argparse.REMAINDER, + help="further options, passed on to Gobra verbatim") + args = parser.parse_args() + + pkg = (REPO / args.package).resolve() + if not pkg.is_dir(): + sys.exit("no such package: %s" % pkg) + files = package_files(pkg) + if not files: + sys.exit("no files with a '+gobra' header in %s" % pkg) + + declared = members(files) + if args.list: + for name in sorted(declared): + for f, line in declared[name]: + print("%-40s %s:%d" % (name, f.relative_to(REPO), line)) + return + + inputs = [str(f) for f in files] + if args.member: + hits = declared.get(args.member) + if not hits: + sys.exit("no member named %r; use --list to see the candidates" + % args.member) + if len(hits) > 1: + sys.exit("%r is declared %d times: %s" % + (args.member, len(hits), + ", ".join("%s:%d" % (f.relative_to(REPO), l) for f, l in hits))) + target, line = hits[0] + inputs = [str(f) + ("@%d" % line if f == target else "") for f in files] + + cmd = gobra_command() + ["-i"] + inputs + options(merged_config(pkg)) + if os.environ.get("Z3_EXE"): + cmd += ["--z3Exe", os.environ["Z3_EXE"]] + cmd += [a for a in args.rest if a != "--"] + + print(" ".join(shlex.quote(c) for c in cmd), flush=True) + if args.dry_run: + return + start = time.time() + rc = subprocess.call(cmd, cwd=REPO) + print("\nfinished in %.0f s (exit code %d)" % (time.time() - start, rc)) + sys.exit(rc) + + +if __name__ == "__main__": + main() From d160acf7835c1cb2cf08afccedc58f073ee18204 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 6 Sep 2026 15:13:55 +0000 Subject: [PATCH 02/10] Record where the router's verification time goes 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 Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z --- verification/PERFORMANCE.md | 174 ++++++++++++++++++++++++++++++++++++ 1 file changed, 174 insertions(+) create mode 100644 verification/PERFORMANCE.md diff --git a/verification/PERFORMANCE.md b/verification/PERFORMANCE.md new file mode 100644 index 000000000..a043f0ca4 --- /dev/null +++ b/verification/PERFORMANCE.md @@ -0,0 +1,174 @@ +# Where the router's verification time goes + +`router/` is by far the most expensive package to verify: the CI gives it a six +hour budget, while every other package gets between five and thirty minutes. +Most of that budget is consumed by a handful of members. This note records how +the cost is distributed, what was measured, and which changes are likely to pay +off, so that the next person to look at this does not have to rediscover it. + +Everything below was measured with `verification/scripts/verify-member.py`, +which verifies **one member at a time** using Gobra's isolation +(`-i router/dataplane.go@`, after which the chopper keeps only the slice +of the program that the member needs) and the options that the CI uses. Numbers +are wall clock for the whole Gobra run on a 4-core machine; roughly 140 s of +each of them is Gobra's front end, which the isolated runs cannot avoid. + +## Cost per member + +| member | isolated run | of which: the contract alone | +|---|---|---| +| `Run` itself, for reference | 2.8 min | — | +| `processOHP` | 5.5 min | — | +| `processPkt` | 5.7 min | — | +| `doXover` | 12 min | 6 min | +| the `rc` closure of `Run` (`closureCall$rc_Run…`) | 26 min | 2.5 min | +| `process` | 109 min | 4 min | + +The "contract alone" column comes from cutting the body at its first statement +(see below): it is what the run still costs when the member has no body left. +Since the front end alone is ~2.5 min, `Run` and `processPkt`/`processOHP` are +in fact only a couple of minutes of solving each; the cost is concentrated in +`process`, in the `rc` closure and, to a lesser extent, in `doXover`. That `Run` +itself is cheap while the closure it declares is not is expected: `Run`'s body +is broken up by seven `outline` blocks, and the packet loop lives in `rc`. + +## The backend options are not the problem + +Every deviation from what `router/gobra.json` already asks for made things +worse, so the slowness is not a misconfiguration: + +| change | effect | +|---|---| +| `mce_mode: "od"` instead of `"on"` (the module default) | `processOHP` still running when the baseline had finished | +| `#backend[moreJoins()]` on `doXover`, i.e. join every branch | more than twice as slow | +| `#backend[exhaleModeQP(2)]` on `doXover` | no improvement | + +`mce_mode: "on"` in particular is not a leftover: with on-demand exhale, Silicon +first tries a greedy exhale and only retries with the complete one when that +fails. In this package the greedy attempt fails often enough that the retries +cost more than always being complete. Note also that Gobra never passes +`--exhaleModeQP`, and Silicon's default for it is the complete mode regardless +of `--exhaleMode`, so quantified permissions are always exhaled completely. + +## Where the time goes inside a member + +The body of a member can be cut short by inserting `TODO()` (which is +`ensures false`), making everything after the cut unreachable. Timing a sequence +of cuts gives a profile of the member. For `doXover`: + +| what runs | s | +|---|---| +| nothing (contract only) | 351 | +| … up to the range splits and `XoverLemma` | 417 | +| … up to and including `IncPath` | 465 | +| … including the block of 14 assertions | 464 | +| … including both hop/info field decodings | 458 | +| the whole body, without the final `return` | 566 | +| the whole member | 707 | + +Two things stand out. The block of assertions in the middle and the two field +decodings are free — the facts they restate are already in the path condition. +And after subtracting the front end, roughly 60 % of the remaining time is spent +on `doXover`'s *own contract*: ~210 s proving that its 26 `ensures` clauses are +well defined before the body starts, and at least ~140 s exhaling them at the +single successful exit. Dropping any one clause changes little (removing the +largest one saves 4 %); the cost is spread evenly over clauses that each mention +`absPkt(ub)` or `old(absPkt(ub))` and therefore drag in +`CurrSeg`/`LeftSeg`/`MidSeg`/`RightSeg` → `segment` → the recursive `hopFields`, +all of which have to be framed against the current `sl.Bytes(ub, …)` snapshot. + +`process` is expensive for the opposite reason: its contract costs about 100 s +of solver time out of 109 minutes. Its body calls seventeen methods whose +specifications total +**568 clauses**, each of which is exhaled and then inhaled again over a heap +that holds `p.scionLayer.Mem(ub)`, a fragmented `sl.Bytes(ub, …)` and the +`absPkt(ub)` function stack. Nine of those callees share eleven *literally +identical* clauses (permission to `p.d`, `p.path`, `p.buffer`, +`p.buffer.UBuf()`, `p.lastLayer`, and `p.d.validResult`). + +The `rc` closure has no postcondition at all, and cutting its body away brings +its run down to the front end alone (152 s): all 26 minutes are the two +nested loops, whose invariants carry quantified assertions over the 64-message +batch — including `forall i :: MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]`, +which unfolds the whole packet abstraction for every message — and are +re-established on every iteration. + +## Contributing factors + +* **Permission fragmentation.** `p.scionLayer.Mem(..)` is used at 18 distinct + permission amounts in `dataplane.go`, `p.scionLayer.Path.Mem(..)` at 11, + `d.Mem(..)` at 8. There are 136 calls to the `sl.*_Bytes` split/combine + lemmas at 11 distinct amounts. Each of them folds or unfolds a predicate whose + body is a quantified `forall i :: acc(&s[i])`, so each creates or consumes + quantified-permission chunks. Under the complete exhale that this package + needs, every subsequent heap lookup summarises all of them. +* **Branches are not joined.** `more_joins: "impure"` only joins impure + conditionals inside assertions; `if` statements are only joined under + `moreJoins(all)`, which `Run` and `rc` opt into and the others do not. So + `process`'s seventeen error exits each exhale its postcondition (25 `ensures` + plus 11 `preserves`, so 36 clauses once encoded) separately. Turning joining + on is worse, though — see the table above. +* **`old(...)` in leaf contracts.** The contracts of the members that `process` + calls contain 61 `old(...)` applications and 88 applications of `absPkt`, + which forces Silicon to keep querying the pre-state heap as well. + +## What is worth trying + +Roughly in decreasing order of expected value per unit of work. + +1. **Thread the abstract packet through ghost parameters instead of naming + `absPkt(ub)` in leaf contracts.** `process` and `processPkt` already do this + (`ghost newAbsPkt io.Val`); `doXover` and the validators do not, and pay for + it: `doXover` alone mentions `absPkt` nine times and `old(...)` nine times in + its contract. Passing the abstract packet in as a ghost parameter and out as + a ghost result would reduce that to two mentions and remove the `old` + applications entirely. +2. **Bundle the resource footprint that the validators share into a predicate.** + The eleven clauses common to nine of `process`'s callees can become a single + predicate that each of them `preserves`, unfolding it once on entry. That + replaces ~17 × 2 × 8 clause exchanges along `process`'s path by a predicate + chunk each way. This is the same transformation that #424 applied to + `DataPlane.Mem()`. +3. **Bundle the per-message resources in `rc`'s loop invariants** in the same + way, so that an iteration exchanges one predicate instead of six quantified + assertions over `msgs`. +4. **Hide the `(typeOf(…) == *epic.Path ? unfolding … in X : X)` idiom behind an + opaque pure function.** Both branches of that conditional denote the same + value; the case split exists only to frame the path's bytes. It appears in + the contracts of `doXover` and `process` and eight times inside `doXover`'s + body. Note that hoisting it into a local ghost boolean inside `doXover` was + measured and did not help (841 s, against a 707 s baseline that had the + machine to itself), so the win has to come from removing the expression from + the contracts, not from the body. +5. **Outline the branches of `process`.** `Run` uses seven `outline` blocks; + `process` and `processPkt` use none. Outlining the inbound, xover and egress + branches would give each of them a small contract of its own instead of + re-exhaling `process`'s 36-clause postcondition on every path. +6. **Delete assertions that restate something already proved.** `doXover` + repeats `assert p.path === p.scionLayer.GetScionPath(ub)` six times and + `assert p.path.GetBase(ubScionPath) == nextBase` five times. The profile + above shows these are nearly free, so this is housekeeping rather than a + speed-up — but it makes the proofs easier to read and to re-time. + +## Reproducing + +```sh +export GOBRA=/path/to/gobra.jar Z3_EXE=/path/to/z3 +./verification/scripts/verify-member.py --list router # member -> line +./verification/scripts/verify-member.py router doXover +./verification/scripts/verify-member.py router rc # a closure of Run +``` + +Two Gobra limitations get in the way and are worth fixing upstream: + +* Member isolation cannot be expressed in the JSON configuration that the CI now + uses. `input_files` makes Gobra abort with + `Logic error: the configuration mode should be one of file, package, recursive + or config` (`InputConfig.fromVerificationJobCfg` fills in `input` but not + `cutInputWithIdxs`, which is what `InputConfig.rawConfig` dispatches on), and + `-i` inside `other` is rejected outright. Hence the script builds a full + command line instead. +* `gobra --config router` from the repository root fails with + `Could not find module configuration file gobra-mod.json …`, because the + search for the module config walks `getParentFile()` on the *relative* path + and stops immediately. An absolute path works. From b9184a8765982ee3b9eec1d1db448099891b5340 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 6 Sep 2026 21:41:43 +0000 Subject: [PATCH 03/10] Record the profile of 'process' and six optimisation attempts that failed 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 Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z --- verification/PERFORMANCE.md | 131 +++++++++++++++++++++++++----------- 1 file changed, 91 insertions(+), 40 deletions(-) diff --git a/verification/PERFORMANCE.md b/verification/PERFORMANCE.md index a043f0ca4..1ef49f3d2 100644 --- a/verification/PERFORMANCE.md +++ b/verification/PERFORMANCE.md @@ -41,8 +41,14 @@ worse, so the slowness is not a misconfiguration: |---|---| | `mce_mode: "od"` instead of `"on"` (the module default) | `processOHP` still running when the baseline had finished | | `#backend[moreJoins()]` on `doXover`, i.e. join every branch | more than twice as slow | +| `#backend[moreJoins()]` on `process` | ≥ 8446 s against a 7737 s baseline under the same load | | `#backend[exhaleModeQP(2)]` on `doXover` | no improvement | +Joining is the interesting one, because the profile below says `process` explores +its whole tail once per side of the `IsXover` branch. Joining does remove that +duplication — and still loses, because merging two copies of a heap this +fragmented costs more than exploring it twice. + `mce_mode: "on"` in particular is not a leftover: with on-demand exhale, Silicon first tries a greedy exhale and only retries with the complete one when that fails. In this package the greedy attempt fails often enough that the retries @@ -66,8 +72,28 @@ of cuts gives a profile of the member. For `doXover`: | the whole body, without the final `return` | 566 | | the whole member | 707 | -Two things stand out. The block of assertions in the middle and the two field -decodings are free — the facts they restate are already in the path condition. +And for `process`: + +| what runs | s | +|---|---| +| nothing (contract only) | 237 | +| … `parsePath` | 307 | +| … the next four validators | 446 | +| … `verifyCurrentMAC`, `handleIngressRouterAlert` | 487 | +| … the whole inbound branch, `InternalEnterEvent` included | 630 | +| … the whole xover branch, `doXover` included | 1319 | +| the whole member | 6548 | + +Four fifths of `process` is therefore in its last 130 lines: `validateEgressUp`, +`egressInterface`, the two egress branches with their IO-spec events, the three +`reveal PktUpdate(…)`/`reveal absIO_val(…)`, and the three exits. That tail sits +after the `if p.path.IsXover(…)` branch, which *rejoins*; since `more_joins: +"impure"` does not join `if` statements, everything in the tail is explored once +per side of that branch, and again per side of each `ghost if +slayers.IsSupportedPkt(ub)` and `ghost if !p.segmentChange` inside it. + +Back to `doXover`: two things stand out. The block of assertions in the middle +and the two field decodings are free — the facts they restate are already in the path condition. And after subtracting the front end, roughly 60 % of the remaining time is spent on `doXover`'s *own contract*: ~210 s proving that its 26 `ensures` clauses are well defined before the body starts, and at least ~140 s exhaling them at the @@ -106,49 +132,74 @@ re-established on every iteration. conditionals inside assertions; `if` statements are only joined under `moreJoins(all)`, which `Run` and `rc` opt into and the others do not. So `process`'s seventeen error exits each exhale its postcondition (25 `ensures` - plus 11 `preserves`, so 36 clauses once encoded) separately. Turning joining - on is worse, though — see the table above. + plus 11 `preserves`, so 36 clauses once encoded) separately, and — far more + expensive — its whole tail is explored once per side of the `IsXover` branch + that precedes it. Joining is not a free win: on `doXover` it was more than + twice as slow. * **`old(...)` in leaf contracts.** The contracts of the members that `process` calls contain 61 `old(...)` applications and 88 applications of `absPkt`, which forces Silicon to keep querying the pre-state heap as well. -## What is worth trying - -Roughly in decreasing order of expected value per unit of work. - -1. **Thread the abstract packet through ghost parameters instead of naming - `absPkt(ub)` in leaf contracts.** `process` and `processPkt` already do this - (`ghost newAbsPkt io.Val`); `doXover` and the validators do not, and pay for - it: `doXover` alone mentions `absPkt` nine times and `old(...)` nine times in - its contract. Passing the abstract packet in as a ghost parameter and out as - a ghost result would reduce that to two mentions and remove the `old` - applications entirely. -2. **Bundle the resource footprint that the validators share into a predicate.** - The eleven clauses common to nine of `process`'s callees can become a single - predicate that each of them `preserves`, unfolding it once on entry. That - replaces ~17 × 2 × 8 clause exchanges along `process`'s path by a predicate - chunk each way. This is the same transformation that #424 applied to - `DataPlane.Mem()`. -3. **Bundle the per-message resources in `rc`'s loop invariants** in the same +## What was tried, and did not work + +Rewriting the specifications locally does not help either. Each of these was +implemented, verified (0 errors) and timed: + +| change | result | +|---|---| +| delete the assertions `doXover` repeats (`p.path === …GetScionPath(ub)` 6×, `…GetBase(ubScionPath) == nextBase` 5×) | no change; the profile says they were already free | +| replace `doXover`'s eight repeated `ghost if typeOf(…) == *epic.Path` by one local ghost boolean | 841 s against a 707 s solo baseline — worse | +| thread the abstract packet through ghost parameters in `doXover`, removing nine `absPkt(ub)` and five `old(absPkt(ub))` from its contract | 892 s vs 915 s in a fair A/B — a wash | +| give `XoverEvent` and `ExternalEnterOrExitEvent` the intermediate abstract packets as parameters, instead of writing `AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)` nine times and `AbsDoXover(…)` five times inside it | `process` 7537 s with the machine to itself, against a 6548 s baseline that shared it — no gain | + +The last two are the informative failures. Silicon evaluates a heap-dependent +function once per heap snapshot, not once per mention, so collapsing repeated +applications buys nothing; what the contract costs is the *number of distinct +states* in which its clauses have to be framed, and the `unfolding`-heavy +accessors (`UBPath`, `UBScionPath`, `GetPath`, `GetScionPath`, +`ValidPathMetaData`, `EqAbsHeader`, …) that each open `p.scionLayer.Mem(ub)` +again. + +Taken together with the backend options above: six interventions, none of which +moved the number. The cost is spread thinly over a very large number of +individually expensive queries, and it is the *size and fragmentation of the +symbolic state* that makes each of them expensive. Anything that leaves the +state alone — reordering clauses, naming subterms, deleting assertions, changing +how branches are explored — leaves the cost alone too. + +A corollary worth keeping in mind before the next attempt: measure in pairs. +Several of the differences above are smaller than the effect of sharing the +machine with a second Gobra run (a second run inflates a `process` measurement +from 6548 s to 7737 s), so a variant timed on its own against a baseline timed +under load will look like a win that is not there. + +## What is left to try + +That points at the changes that make the state itself smaller. They are real +refactors rather than annotations, which is why they were not attempted here. + +1. **Bundle the resource footprint that the validators share into a predicate.** + The eleven clauses common to nine of `process`'s callees — permission to + `p.d`, `p.path`, `p.buffer`, `p.buffer.UBuf()`, `p.lastLayer`, plus + `p.d.validResult` and two impure implications about `p.lastLayer` — can + become a single predicate that each of them `preserves` and unfolds only on + the paths that build an SCMP reply. That replaces roughly 17 × 2 × 8 clause + exchanges along `process`'s path by one predicate chunk in each direction. + This is the transformation that #424 applied to `DataPlane.Mem()`, and it + attacks the state size rather than the specification text. +2. **Bundle the per-message resources in `rc`'s loop invariants** in the same way, so that an iteration exchanges one predicate instead of six quantified - assertions over `msgs`. -4. **Hide the `(typeOf(…) == *epic.Path ? unfolding … in X : X)` idiom behind an - opaque pure function.** Both branches of that conditional denote the same - value; the case split exists only to frame the path's bytes. It appears in - the contracts of `doXover` and `process` and eight times inside `doXover`'s - body. Note that hoisting it into a local ghost boolean inside `doXover` was - measured and did not help (841 s, against a 707 s baseline that had the - machine to itself), so the win has to come from removing the expression from - the contracts, not from the body. -5. **Outline the branches of `process`.** `Run` uses seven `outline` blocks; - `process` and `processPkt` use none. Outlining the inbound, xover and egress - branches would give each of them a small contract of its own instead of - re-exhaling `process`'s 36-clause postcondition on every path. -6. **Delete assertions that restate something already proved.** `doXover` - repeats `assert p.path === p.scionLayer.GetScionPath(ub)` six times and - `assert p.path.GetBase(ubScionPath) == nextBase` five times. The profile - above shows these are nearly free, so this is housekeeping rather than a - speed-up — but it makes the proofs easier to read and to re-time. + assertions over the 64-message batch. This needs a range predicate with + take/put lemmas, since the body still has to get at one message at a time. +3. **Reduce the number of distinct permission amounts.** `p.scionLayer.Mem(..)` + is currently used at 18 of them, and the `unfold acc(P, 1-R55)` / + `unfold acc(P, R55)` idiom exists only so that a pure function can be + evaluated in between. Every extra fraction is another chunk for the complete + exhale to summarise. +4. **Outline the branches of `process`.** `Run` uses seven `outline` blocks; + `process` and `processPkt` use none. An outlined block is verified as its own + Viper method, so the state that the rest of `process` carries past it is + whatever the outline's contract says, not everything the branch touched. ## Reproducing From 8180cd9b2ea89f02a2305cc8cb3642d61458db76 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 7 Sep 2026 02:12:15 +0000 Subject: [PATCH 04/10] Bundle the last decoded layer into a predicate: 'process' 2.1x faster '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 Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z --- router/dataplane.go | 162 ++++++++------------------ router/dataplane_spec.gobra | 22 ++++ verification/PERFORMANCE.md | 74 +++++++++--- verification/scripts/verify-member.py | 6 +- 4 files changed, 130 insertions(+), 134 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 87074e4cd..ad47677ed 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1736,7 +1736,13 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ assert reveal p.scionLayer.EqPathType(p.rawPkt) // @ assert path.Type(slayers.GetPathType(p.rawPkt)) != epic.PathType // @ assert absIO_val(p.rawPkt, p.ingressID) == oldAbsVal - v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processSCION( /*@ p.rawPkt, ub == nil, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) + // (VerifiedSCION) pack the last layer away for the whole of 'process': + // it is folded here, where it was just decoded and the facts about it are + // still immediate, rather than inside 'process', where re-deriving them + // from the ghost parameters costs far more than it saves. + // @ fold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) + v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processSCION( /*@ p.rawPkt, ub, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) + // @ unfold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() return v1, v2 /*@, addrAliasesPkt, newAbsPkt @*/ @@ -1756,7 +1762,13 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ assert unfolding acc(p.scionLayer.Mem(p.rawPkt), R56) in slayers.CmnHdrLen <= len(p.rawPkt) // @ assert typeOf(p.scionLayer.GetPath(p.rawPkt)) == *epic.Path ==> // @ p.scionLayer.EqAbsHeader(p.rawPkt) && p.scionLayer.ValidScionInitSpec(p.rawPkt) - v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processEPIC( /*@ p.rawPkt, ub == nil, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) + // (VerifiedSCION) pack the last layer away for the whole of 'process': + // it is folded here, where it was just decoded and the facts about it are + // still immediate, rather than inside 'process', where re-deriving them + // from the ghost parameters costs far more than it saves. + // @ fold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) + v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processEPIC( /*@ p.rawPkt, ub, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) + // @ unfold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() return v1, v2 /*@, addrAliasesPkt, newAbsPkt @*/ @@ -1892,14 +1904,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.ingressID, R10) // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) -// @ preserves acc(&p.lastLayer, R10) -// @ preserves p.lastLayer != nil -// @ preserves (p.lastLayer !== &p.scionLayer && llIsNil) ==> -// @ acc(p.lastLayer.Mem(nil), R10) -// @ preserves (p.lastLayer !== &p.scionLayer && !llIsNil) ==> -// @ acc(p.lastLayer.Mem(ub[startLL:endLL]), R10) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ !llIsNil && startLL == 0 && endLL == len(ub) +// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() @@ -1954,7 +1959,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ path.ifsToIO_ifs(p.ingressID), // @ newAbsPkt.ValPkt_1) // @ decreases 0 if sync.IgnoreBlockingForTermination() -func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { +func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { var ok bool // @ unfold acc(p.scionLayer.Mem(ub), R20) @@ -1968,7 +1973,7 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil return processResult{}, malformedPath /*@ , false, io.ValUnit{} @*/ } // @ assert p.path === p.scionLayer.GetScionPath(ub) - return p.process( /*@ ub, llIsNil, startLL, endLL , ioLock, ioSharedArg, dp @*/ ) + return p.process( /*@ ub, ubLL, startLL, endLL , ioLock, ioSharedArg, dp @*/ ) } // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) @@ -1985,14 +1990,7 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.ingressID, R10) // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) -// @ preserves acc(&p.lastLayer, R10) -// @ preserves p.lastLayer != nil -// @ preserves (p.lastLayer !== &p.scionLayer && llIsNil) ==> -// @ acc(p.lastLayer.Mem(nil), R10) -// @ preserves (p.lastLayer !== &p.scionLayer && !llIsNil) ==> -// @ acc(p.lastLayer.Mem(ub[startLL:endLL]), R10) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ !llIsNil && startLL == 0 && endLL == len(ub) +// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() @@ -2049,7 +2047,7 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil // @ path.ifsToIO_ifs(p.ingressID), // @ newAbsPkt.ValPkt_1) // @ decreases 0 if sync.IgnoreBlockingForTermination() -func (p *scionPacketProcessor) processEPIC( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { +func (p *scionPacketProcessor) processEPIC( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { // @ unfold acc(p.scionLayer.Mem(ub), R10) epicPath, ok := p.scionLayer.Path.(*epic.Path) if !ok { @@ -2085,7 +2083,7 @@ func (p *scionPacketProcessor) processEPIC( /*@ ghost ub []byte, ghost llIsNil b // @ assert p.path === p.scionLayer.GetScionPath(ub) // @ assert p.scionLayer.UBPath(ub) === ubPath - result, err /*@ , addrAliases, newAbsPkt0 @*/ := p.process( /*@ ub, llIsNil, startLL, endLL, ioLock, ioSharedArg, dp @*/ ) + result, err /*@ , addrAliases, newAbsPkt0 @*/ := p.process( /*@ ub, ubLL, startLL, endLL, ioLock, ioSharedArg, dp @*/ ) if err != nil { return result, err /*@ , addrAliases, newAbsPkt0 @*/ } @@ -2217,12 +2215,7 @@ type macBuffersT struct { // @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires cause != nil ==> cause.ErrorMem() -// @ preserves ubLL == nil || ubLL === ub[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ub === ubLL +// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.Bytes(ub, 0, len(ub)) @@ -2246,6 +2239,10 @@ func (p *scionPacketProcessor) packSCMP( // @ ghost startLL int, // @ ghost endLL int, ) (respr processResult, reserr error) { + // (VerifiedSCION) this member reads the last layer, so it opens the + // predicate that carries it; the checks that only hand it on do not. + // @ unfold p.LastLayerMem(ub, ubLL, startLL, endLL) + // @ defer fold p.LastLayerMem(ub, ubLL, startLL, endLL) // @ ghost llIsScmp := false // @ ghost scmpPldIsNil := false // @ ghost maybeStartPld := 0 @@ -2419,12 +2416,7 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce // pres for IO: // @ requires slayers.ValidPktMetaHdr(ubScionL) && p.scionLayer.EqAbsHeader(ubScionL) // @ requires absPkt(ubScionL).PathNotFullyTraversed() -// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ubScionL === ubLL +// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) // @ preserves acc(&p.infoField, R20) // @ preserves acc(&p.hopField, R20) // @ preserves acc(&p.ingressID, R20) @@ -2508,12 +2500,7 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho // @ requires acc(&p.hopField, R20) // @ requires acc(&p.infoField, R20) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) -// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ubScionL === ubLL +// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) // @ ensures acc(&p.d, R50) // @ ensures acc(&p.path, R20) // @ ensures acc(&p.infoField, R20) @@ -2585,12 +2572,7 @@ func (p *scionPacketProcessor) validateIngressID( /*@ ghost ubScionL []byte, gho // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R21) -// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ubScionL === ubLL +// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) // @ ensures acc(p.scionLayer.Mem(ubScionL), R2) // @ ensures acc(&p.path, R20) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) @@ -2698,12 +2680,7 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghos // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R40) -// @ preserves ubLL == nil || ubLL === ub[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ub === ubLL +// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(&p.path, R20) // @ ensures acc(p.scionLayer.Mem(ub), R3) @@ -2748,12 +2725,7 @@ func (p *scionPacketProcessor) invalidSrcIA( // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R40) -// @ preserves ubLL == nil || ubLL === ub[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ub === ubLL +// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(&p.path, R20) // @ ensures acc(p.scionLayer.Mem(ub), R3) @@ -2883,12 +2855,7 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @ // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) -// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ubScionL === ubLL +// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) // @ ensures acc(&p.infoField, R20) // @ ensures acc(&p.hopField, R20) // @ ensures acc(&p.ingressID, R21) @@ -3208,12 +3175,7 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ preserves acc(&p.macBuffers.scionInput, R20) // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) -// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ubScionL === ubLL +// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) // @ ensures acc(&p.path, R20) // @ ensures acc(&p.infoField, R20) // @ ensures acc(&p.hopField, R20) @@ -3313,12 +3275,7 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ requires slayers.ValidPktMetaHdr(ubScionL) && p.scionLayer.EqAbsHeader(ubScionL) // @ requires absPkt(ubScionL).PathNotFullyTraversed() // @ preserves acc(&p.ingressID, R40) -// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ubScionL === ubLL +// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) // @ ensures acc(&p.d, R15) && acc(p.d.Mem(), _) // @ requires p.d.getValSvc() != nil // @ ensures p.d.validResult(respr, addrAliasesUb) @@ -3739,12 +3696,7 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.Pkt @*/ ) (e // @ requires absPkt(ub).PathNotFullyTraversed() // @ requires p.EqAbsInfoField(absPkt(ub)) // @ requires p.EqAbsHopField(absPkt(ub)) -// @ preserves ubLL == nil || ubLL === ub[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ub === ubLL +// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ ensures acc(&p.infoField, R20) // @ ensures acc(&p.hopField, R20) // @ ensures acc(&p.ingressID, R21) @@ -3823,12 +3775,7 @@ func (p *scionPacketProcessor) validateEgressUp( // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) // @ ensures p.cachedMac === old(p.cachedMac) -// @ preserves ubLL == nil || ubLL === ub[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ub === ubLL +// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ ensures acc(&p.ingressID, R21) // @ ensures acc(&p.path, R20) // @ ensures acc(&p.infoField, R20) @@ -3959,12 +3906,7 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) // @ ensures p.cachedMac === old(p.cachedMac) -// @ preserves ubLL == nil || ubLL === ub[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ub === ubLL +// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ ensures acc(&p.ingressID, R21) // @ ensures acc(&p.path, R20) // @ ensures acc(&p.infoField, R20) @@ -4096,12 +4038,7 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) { // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) // @ ensures p.cachedMac === old(p.cachedMac) -// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ubScionL === ubLL +// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) // @ ensures acc(&p.path, R20) // @ ensures acc(&p.infoField, R20) // @ ensures acc(&p.hopField, R20) @@ -4131,16 +4068,23 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) { // @ decreases func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( interfaceID uint16 /*@, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/) (respr processResult, reserr error) { + // (VerifiedSCION) this member reads the last layer, so it opens the + // predicate that carries it; the checks that only hand it on do not. It is + // closed again as soon as the two reads below are done - the pure facts it + // carries stay known, and 'packSCMP' wants it folded. + // @ unfold p.LastLayerMem(ubScionL, ubLL, startLL, endLL) // @ ghost llIsScmp := false // @ ghost scionPldIsNil := false // @ ghost maybeStartPld := 0 // @ ghost maybeEndPld := 0 if p.lastLayer.NextLayerType( /*@ ubLL @*/ ) != slayers.LayerTypeSCMP { log.Debug("Packet with router alert, but not SCMP") + // @ fold p.LastLayerMem(ubScionL, ubLL, startLL, endLL) // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } scionPld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ ubLL @*/ ) + // @ fold p.LastLayerMem(ubScionL, ubLL, startLL, endLL) // @ sl.SplitRange_Bytes(ubScionL, startLL, endLL, R1) // @ maybeStartPld = start // @ maybeEndPld = end @@ -4212,12 +4156,7 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R20) -// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL] -// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil -// @ preserves &p.scionLayer !== p.lastLayer ==> -// @ acc(p.lastLayer.Mem(ubLL), R15) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ ubScionL === ubLL +// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(&p.path, R20) // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) @@ -4277,13 +4216,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ requires acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) -// @ preserves acc(&p.lastLayer, R10) -// @ preserves p.lastLayer != nil -// @ preserves p.lastLayer !== &p.scionLayer ==> -// @ (llIsNil ==> acc(p.lastLayer.Mem(nil), R10)) && -// @ (!llIsNil ==> acc(p.lastLayer.Mem(ub[startLL:endLL]), R10)) -// @ preserves &p.scionLayer === p.lastLayer ==> -// @ !llIsNil && startLL == 0 && endLL == len(ub) +// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() @@ -4344,14 +4277,13 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ #backend[stateConsolidationMode(6)] func (p *scionPacketProcessor) process( // @ ghost ub []byte, -// @ ghost llIsNil bool, +// @ ghost ubLL []byte, // @ ghost startLL int, // @ ghost endLL int, // @ ghost ioLock gpointer[gsync.GhostMutex], // @ ghost ioSharedArg SharedArg, // @ ghost dp io.DataPlaneSpec, ) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { - // @ ghost ubLL := llIsNil ? ([]byte)(nil) : ub[startLL:endLL] // @ assert p.path === p.scionLayer.GetScionPath(ub) if r, err := p.parsePath( /*@ ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index f0c8d1d1e..e1958684a 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -189,6 +189,28 @@ func liftForwardingMetricsNonInjectiveMem(v forwardingMetrics, id uint16) { fold acc(forwardingMetricsMem(v, id), _) } +// (VerifiedSCION) The last layer that was decoded out of the packet, which is +// what 'packSCMP' reads when a check answers with an SCMP message. Every check +// that 'process' performs has to carry it, even though almost none of them look +// at it: they only hand it on to 'packSCMP'. +// +// Spelled out, this 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. As a predicate it is a single chunk, +// and only the two members that read it - 'packSCMP' and +// 'handleSCMPTraceRouteRequest' - ever unfold it. +// +// 'ubLL' is the last layer's buffer, 'nil' when there is none; it is a slice of +// 'ub' and coincides with it when the last layer is the SCION layer itself. +pred (p *scionPacketProcessor) LastLayerMem(ub []byte, ubLL []byte, startLL int, endLL int) { + 0 <= startLL && startLL <= endLL && endLL <= len(ub) && + acc(&p.lastLayer, R10) && p.lastLayer != nil && + (ubLL == nil || ubLL === ub[startLL:endLL]) && + (&p.scionLayer !== p.lastLayer ==> acc(p.lastLayer.Mem(ubLL), R10)) && + (&p.scionLayer === p.lastLayer ==> ub === ubLL) +} + pred (p *scionPacketProcessor) initMem() { acc(&p.d) && acc(&p.ingressID) && diff --git a/verification/PERFORMANCE.md b/verification/PERFORMANCE.md index 1ef49f3d2..223a1bb3d 100644 --- a/verification/PERFORMANCE.md +++ b/verification/PERFORMANCE.md @@ -24,6 +24,9 @@ each of them is Gobra's front end, which the isolated runs cannot avoid. | the `rc` closure of `Run` (`closureCall$rc_Run…`) | 26 min | 2.5 min | | `process` | 109 min | 4 min | +(`process` is now 62 min — see *What did work* below. The rest of the table, and +the whole analysis, describes the state before that change.) + The "contract alone" column comes from cutting the body at its first statement (see below): it is what the run still costs when the member has no body left. Since the front end alone is ~2.5 min, `Run` and `processPkt`/`processOHP` are @@ -165,7 +168,8 @@ moved the number. The cost is spread thinly over a very large number of individually expensive queries, and it is the *size and fragmentation of the symbolic state* that makes each of them expensive. Anything that leaves the state alone — reordering clauses, naming subterms, deleting assertions, changing -how branches are explored — leaves the cost alone too. +how branches are explored — leaves the cost alone too. The next section is what +happens when the state itself gets smaller. A corollary worth keeping in mind before the next attempt: measure in pairs. Several of the differences above are smaller than the effect of sharing the @@ -173,24 +177,60 @@ machine with a second Gobra run (a second run inflates a `process` measurement from 6548 s to 7737 s), so a variant timed on its own against a baseline timed under load will look like a win that is not there. +## What did work: `LastLayerMem` + +Shrinking the state does move the number. `process` went from **7854 s to +3729 s — 2.1× — in a paired A/B**, both arms reporting 0 errors. + +The change is `(p *scionPacketProcessor).LastLayerMem(ub, ubLL, startLL, endLL)` +in `dataplane_spec.gobra`. It bundles the description of the last decoded layer, +which used to be spelled out as four clauses in the contract of fourteen +members: + +``` +preserves ubLL == nil || ubLL === ubScionL[startLL:endLL] +preserves acc(&p.lastLayer, R55) && p.lastLayer != nil +preserves &p.scionLayer !== p.lastLayer ==> acc(p.lastLayer.Mem(ubLL), R15) +preserves &p.scionLayer === p.lastLayer ==> ubScionL === ubLL +``` + +Two of those are impure implications, which Silicon branches on and re-joins at +every exhale and every inhale. `process` carries the same thing in an even +worse spelling — an implication nested inside an implication, keyed on a +`llIsNil` flag — and exchanges it twice at each of the seventeen calls along its +path. As a predicate it is one chunk each way, and only `packSCMP`, the one +member that actually reads the last layer, ever unfolds it. + +Nothing is proved that was not proved before: 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. The one clause +that was 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` — the +obvious place, since that is who holds the resources across the calls — costs +about 1200 s on its own, because the predicate then has to be re-derived from +the `llIsNil` parameterisation, including a slice identity `ub[0:len(ub)] === ub`. +Folding in `processPkt` instead, right after `decodeLayers` has produced the +layer and the facts about it are still immediate, is free (350 s against a +342 s baseline). `process`, `processSCION` and `processEPIC` then just take the +predicate as a parameter and never open it. + ## What is left to try -That points at the changes that make the state itself smaller. They are real -refactors rather than annotations, which is why they were not attempted here. - -1. **Bundle the resource footprint that the validators share into a predicate.** - The eleven clauses common to nine of `process`'s callees — permission to - `p.d`, `p.path`, `p.buffer`, `p.buffer.UBuf()`, `p.lastLayer`, plus - `p.d.validResult` and two impure implications about `p.lastLayer` — can - become a single predicate that each of them `preserves` and unfolds only on - the paths that build an SCMP reply. That replaces roughly 17 × 2 × 8 clause - exchanges along `process`'s path by one predicate chunk in each direction. - This is the transformation that #424 applied to `DataPlane.Mem()`, and it - attacks the state size rather than the specification text. -2. **Bundle the per-message resources in `rc`'s loop invariants** in the same - way, so that an iteration exchanges one predicate instead of six quantified - assertions over the 64-message batch. This needs a range predicate with - take/put lemmas, since the body still has to get at one message at a time. +Same recipe, other resources. + +1. **Bundle the rest of the footprint the validators share.** Three more clauses + are common to all of them — `acc(&p.buffer, R50) && p.buffer != nil && + p.buffer.Mem()`, `sl.Bytes(p.buffer.UBuf(), …)` and `respr !== + processResult{} ==> respr.OutPkt === p.buffer.UBuf()` — plus permission to + `p.d` and `p.path`. The buffer is harder than the last layer, because that + last clause mentions `p.buffer.UBuf()` and would need an `unfolding` or an + opaque getter. +2. **Bundle the per-message resources in `rc`'s loop invariants**, so that an + iteration exchanges one predicate instead of six quantified assertions over + the 64-message batch. This needs a range predicate with take/put lemmas, + since the body still has to get at one message at a time. 3. **Reduce the number of distinct permission amounts.** `p.scionLayer.Mem(..)` is currently used at 18 of them, and the `unfold acc(P, 1-R55)` / `unfold acc(P, R55)` idiom exists only so that a pure function can be diff --git a/verification/scripts/verify-member.py b/verification/scripts/verify-member.py index fc9ff7e99..d949f684a 100755 --- a/verification/scripts/verify-member.py +++ b/verification/scripts/verify-member.py @@ -22,7 +22,9 @@ The Gobra binary is taken from ``$GOBRA``; it may be either an executable or a ``.jar`` (in which case it is run with ``java -jar``). ``$Z3_EXE`` is forwarded -to Gobra when it is set. +to Gobra when it is set, and ``$GOBRA_HEAP`` overrides the JVM heap size (8g by +default) - useful when running several members at once, since each of them can +take several gigabytes. """ import argparse @@ -139,7 +141,7 @@ def gobra_command(): if not binary: sys.exit("Set $GOBRA to the Gobra executable or to gobra.jar.") if binary.endswith(".jar"): - return ["java", "-Xss1g", "-Xmx8g", "-jar", binary] + return ["java", "-Xss1g", "-Xmx" + os.environ.get("GOBRA_HEAP", "8g"), "-jar", binary] return [binary] From d3f01b92958989824c66847ea2b86cad8de99701 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 7 Sep 2026 06:26:18 +0000 Subject: [PATCH 05/10] Bundle the SCMP reply buffer into a predicate 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 Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z --- router/dataplane.go | 151 +++++++++++++++--------------------- router/dataplane_spec.gobra | 27 +++++++ 2 files changed, 89 insertions(+), 89 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index ad47677ed..e2244fa2f 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1741,7 +1741,9 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // still immediate, rather than inside 'process', where re-deriving them // from the ghost parameters costs far more than it saves. // @ fold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) + // @ fold p.SCMPBufMem() v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processSCION( /*@ p.rawPkt, ub, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) + // @ unfold p.SCMPBufMem() // @ unfold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() @@ -1767,7 +1769,9 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // still immediate, rather than inside 'process', where re-deriving them // from the ghost parameters costs far more than it saves. // @ fold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) + // @ fold p.SCMPBufMem() v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processEPIC( /*@ p.rawPkt, ub, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) + // @ unfold p.SCMPBufMem() // @ unfold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() @@ -1900,8 +1904,8 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ requires p.scionLayer.Mem(ub) // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.segmentChange) && !p.segmentChange -// @ requires acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.ingressID, R10) // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) @@ -1922,12 +1926,10 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ respr.OutAddr != nil && // @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.Bytes(ub, 0, len(ub)), R15))) // @ ensures !addrAliasesPkt ==> acc(sl.Bytes(ub, 0, len(ub)), R15) -// @ ensures acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() // @ ensures reserr == nil ==> p.scionLayer.Mem(ub) // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr.OutPkt != nil ==> -// @ (respr.OutPkt === ub || respr.OutPkt === p.buffer.UBuf()) +// @ (respr.OutPkt === ub || respr.OutPkt === p.OutBuf()) // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires p.d.DpAgreesWithSpec(dp) @@ -1986,8 +1988,8 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost ubLL []b // @ requires p.scionLayer.Mem(ub) // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.segmentChange) && !p.segmentChange -// @ requires acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.ingressID, R10) // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) @@ -2010,12 +2012,10 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost ubLL []b // @ respr.OutAddr != nil && // @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.Bytes(ub, 0, len(ub)), R15))) // @ ensures !addrAliasesPkt ==> acc(sl.Bytes(ub, 0, len(ub)), R15) -// @ ensures acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() // @ ensures reserr == nil ==> p.scionLayer.Mem(ub) // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr.OutPkt != nil ==> -// @ (respr.OutPkt === ub || respr.OutPkt === p.buffer.UBuf()) +// @ (respr.OutPkt === ub || respr.OutPkt === p.OutBuf()) // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires p.scionLayer.EqPathType(p.rawPkt) @@ -2212,8 +2212,8 @@ type macBuffersT struct { // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R45) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires cause != nil ==> cause.ErrorMem() // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) @@ -2221,10 +2221,8 @@ type macBuffersT struct { // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R45) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures respr.OutPkt != nil ==> // @ !slayers.IsSupportedPkt(respr.OutPkt) @@ -2239,10 +2237,13 @@ func (p *scionPacketProcessor) packSCMP( // @ ghost startLL int, // @ ghost endLL int, ) (respr processResult, reserr error) { - // (VerifiedSCION) this member reads the last layer, so it opens the - // predicate that carries it; the checks that only hand it on do not. + // (VerifiedSCION) this member reads the last layer and writes the SCMP + // buffer, so it opens both predicates; the checks that only hand them on do + // not. // @ unfold p.LastLayerMem(ub, ubLL, startLL, endLL) // @ defer fold p.LastLayerMem(ub, ubLL, startLL, endLL) + // @ unfold p.SCMPBufMem() + // @ defer fold p.SCMPBufMem() // @ ghost llIsScmp := false // @ ghost scmpPldIsNil := false // @ ghost maybeStartPld := 0 @@ -2411,8 +2412,8 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // pres for IO: // @ requires slayers.ValidPktMetaHdr(ubScionL) && p.scionLayer.EqAbsHeader(ubScionL) // @ requires absPkt(ubScionL).PathNotFullyTraversed() @@ -2425,10 +2426,8 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -2494,8 +2493,8 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.hopField, R20) // @ requires acc(&p.infoField, R20) @@ -2513,10 +2512,8 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -2568,8 +2565,8 @@ func (p *scionPacketProcessor) validateIngressID( /*@ ghost ubScionL []byte, gho // @ requires acc(p.scionLayer.Mem(ubScionL), R2) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R21) // @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) @@ -2578,10 +2575,8 @@ func (p *scionPacketProcessor) validateIngressID( /*@ ghost ubScionL []byte, gho // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -2676,8 +2671,8 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghos // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetScionPath(ub) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R40) // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) @@ -2686,10 +2681,8 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghos // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported @@ -2721,8 +2714,8 @@ func (p *scionPacketProcessor) invalidSrcIA( // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetScionPath(ub) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R40) // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) @@ -2731,10 +2724,8 @@ func (p *scionPacketProcessor) invalidSrcIA( // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported @@ -2849,8 +2840,8 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @ // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.segmentChange, R20) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -2865,10 +2856,8 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @ // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3165,8 +3154,8 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -3183,10 +3172,8 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3268,8 +3255,8 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.d, R15) && acc(p.d.Mem(), _) // pres for IO: // @ requires slayers.ValidPktMetaHdr(ubScionL) && p.scionLayer.EqAbsHeader(ubScionL) @@ -3288,10 +3275,8 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ ensures acc(&p.path, R20) // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures acc(sl.Bytes(ubScionL, 0, len(ubScionL)), 1-R15) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3685,8 +3670,8 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.Pkt @*/ ) (e // @ requires acc(p.scionLayer.Mem(ub), R2) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetScionPath(ub) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) @@ -3705,10 +3690,8 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.Pkt @*/ ) (e // @ ensures acc(p.scionLayer.Mem(ub), R2) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3764,8 +3747,8 @@ func (p *scionPacketProcessor) validateEgressUp( // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetScionPath(ub) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -3784,10 +3767,8 @@ func (p *scionPacketProcessor) validateEgressUp( // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3895,8 +3876,8 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetScionPath(ub) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -3915,10 +3896,8 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -4023,8 +4002,8 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) { // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) @@ -4046,10 +4025,8 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) { // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -4152,8 +4129,8 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R20) // @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) @@ -4162,10 +4139,8 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) -// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.buffer.UBuf() +// @ respr.OutPkt === p.OutBuf() // @ ensures reserr == nil ==> // @ int(p.scionLayer.GetPayloadLen(ubScionL)) == len(p.scionLayer.GetPayload(ubScionL)) // @ ensures reserr != nil ==> reserr.ErrorMem() @@ -4213,8 +4188,8 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R15) // @ requires acc(&p.segmentChange) && !p.segmentChange -// @ requires acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() -// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ preserves p.SCMPBufMem() +// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ preserves acc(&p.infoField) @@ -4234,16 +4209,14 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ respr.OutAddr != nil && // @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.Bytes(ub, 0, len(ub)), R15))) // @ ensures !addrAliasesPkt ==> acc(sl.Bytes(ub, 0, len(ub)), R15) -// @ ensures acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() // @ ensures reserr == nil ==> p.scionLayer.Mem(ub) // @ ensures reserr == nil ==> p.path === p.scionLayer.GetScionPath(ub) // @ ensures reserr == nil ==> p.scionLayer.GetPath(ub) === old(p.scionLayer.GetPath(ub)) // @ ensures reserr == nil ==> p.scionLayer.UBPath(ub) === old(p.scionLayer.UBPath(ub)) // @ ensures reserr == nil ==> sl.Bytes(p.cachedMac, 0, len(p.cachedMac)) // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr.OutPkt != nil ==> -// @ (respr.OutPkt === ub || respr.OutPkt === p.buffer.UBuf()) +// @ (respr.OutPkt === ub || respr.OutPkt === p.OutBuf()) // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires p.d.DpAgreesWithSpec(dp) @@ -4946,13 +4919,13 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { // @ requires acc(&p.ingressID, R50) // @ requires acc(&p.buffer, R55) && p.buffer != nil && p.buffer.Mem() // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +// @ ensures acc(&p.buffer, R55) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires cause != nil ==> cause.ErrorMem() // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R50) -// @ ensures acc(&p.buffer, R55) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures result != nil ==> // @ result === p.buffer.UBuf() // @ ensures reserr != nil && reserr.ErrorMem() diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index e1958684a..77676210a 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -211,6 +211,33 @@ pred (p *scionPacketProcessor) LastLayerMem(ub []byte, ubLL []byte, startLL int, (&p.scionLayer === p.lastLayer ==> ub === ubLL) } +// (VerifiedSCION) The buffer that an SCMP reply is serialized into. Like the +// last layer, every check along 'process's path has to carry it even though only +// 'packSCMP' writes to it, so the three assertions that describe it travel in +// both directions across each of the seventeen calls. +// +// The permission to the buffer's *bytes* deliberately stays outside: the results +// that alias them are described by postconditions such as +// 'absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported', whose +// well-definedness needs 'sl.Bytes(respr.OutPkt, ..)' to be framed by the +// contract itself. Hiding it inside the predicate would make those clauses +// ill-defined, and stating them under an 'unfolding' would cost more than the +// bundling saves. +pred (p *scionPacketProcessor) SCMPBufMem() { + acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() +} + +// The bytes of that buffer. A check that answers with an SCMP message returns a +// result that aliases them, and says so with this function rather than by +// opening the predicate. It mirrors 'sInitBufferUBuf', which does the same one +// level up, through 'sInit'. +ghost +requires acc(p.SCMPBufMem(), _) +decreases +pure func (p *scionPacketProcessor) OutBuf() []byte { + return unfolding acc(p.SCMPBufMem(), _) in p.buffer.UBuf() +} + pred (p *scionPacketProcessor) initMem() { acc(&p.d) && acc(&p.ingressID) && From e0d004bd0d092d1e0c02fe8d5c70b290cfed43b2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 7 Sep 2026 07:33:36 +0000 Subject: [PATCH 06/10] Revert the SCMP buffer predicate: no measurable gain 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 Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z --- router/dataplane.go | 151 +++++++++++++++++++++--------------- router/dataplane_spec.gobra | 27 ------- 2 files changed, 89 insertions(+), 89 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index e2244fa2f..ad47677ed 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1741,9 +1741,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // still immediate, rather than inside 'process', where re-deriving them // from the ghost parameters costs far more than it saves. // @ fold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) - // @ fold p.SCMPBufMem() v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processSCION( /*@ p.rawPkt, ub, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) - // @ unfold p.SCMPBufMem() // @ unfold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() @@ -1769,9 +1767,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // still immediate, rather than inside 'process', where re-deriving them // from the ghost parameters costs far more than it saves. // @ fold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) - // @ fold p.SCMPBufMem() v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processEPIC( /*@ p.rawPkt, ub, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) - // @ unfold p.SCMPBufMem() // @ unfold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() @@ -1904,8 +1900,8 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ requires p.scionLayer.Mem(ub) // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.segmentChange) && !p.segmentChange -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.ingressID, R10) // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) @@ -1926,10 +1922,12 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ respr.OutAddr != nil && // @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.Bytes(ub, 0, len(ub)), R15))) // @ ensures !addrAliasesPkt ==> acc(sl.Bytes(ub, 0, len(ub)), R15) +// @ ensures acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() // @ ensures reserr == nil ==> p.scionLayer.Mem(ub) // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr.OutPkt != nil ==> -// @ (respr.OutPkt === ub || respr.OutPkt === p.OutBuf()) +// @ (respr.OutPkt === ub || respr.OutPkt === p.buffer.UBuf()) // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires p.d.DpAgreesWithSpec(dp) @@ -1988,8 +1986,8 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost ubLL []b // @ requires p.scionLayer.Mem(ub) // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.segmentChange) && !p.segmentChange -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.ingressID, R10) // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) @@ -2012,10 +2010,12 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost ubLL []b // @ respr.OutAddr != nil && // @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.Bytes(ub, 0, len(ub)), R15))) // @ ensures !addrAliasesPkt ==> acc(sl.Bytes(ub, 0, len(ub)), R15) +// @ ensures acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() // @ ensures reserr == nil ==> p.scionLayer.Mem(ub) // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr.OutPkt != nil ==> -// @ (respr.OutPkt === ub || respr.OutPkt === p.OutBuf()) +// @ (respr.OutPkt === ub || respr.OutPkt === p.buffer.UBuf()) // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires p.scionLayer.EqPathType(p.rawPkt) @@ -2212,8 +2212,8 @@ type macBuffersT struct { // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R45) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires cause != nil ==> cause.ErrorMem() // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) @@ -2221,8 +2221,10 @@ type macBuffersT struct { // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R45) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures respr.OutPkt != nil ==> // @ !slayers.IsSupportedPkt(respr.OutPkt) @@ -2237,13 +2239,10 @@ func (p *scionPacketProcessor) packSCMP( // @ ghost startLL int, // @ ghost endLL int, ) (respr processResult, reserr error) { - // (VerifiedSCION) this member reads the last layer and writes the SCMP - // buffer, so it opens both predicates; the checks that only hand them on do - // not. + // (VerifiedSCION) this member reads the last layer, so it opens the + // predicate that carries it; the checks that only hand it on do not. // @ unfold p.LastLayerMem(ub, ubLL, startLL, endLL) // @ defer fold p.LastLayerMem(ub, ubLL, startLL, endLL) - // @ unfold p.SCMPBufMem() - // @ defer fold p.SCMPBufMem() // @ ghost llIsScmp := false // @ ghost scmpPldIsNil := false // @ ghost maybeStartPld := 0 @@ -2412,8 +2411,8 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // pres for IO: // @ requires slayers.ValidPktMetaHdr(ubScionL) && p.scionLayer.EqAbsHeader(ubScionL) // @ requires absPkt(ubScionL).PathNotFullyTraversed() @@ -2426,8 +2425,10 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -2493,8 +2494,8 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.hopField, R20) // @ requires acc(&p.infoField, R20) @@ -2512,8 +2513,10 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -2565,8 +2568,8 @@ func (p *scionPacketProcessor) validateIngressID( /*@ ghost ubScionL []byte, gho // @ requires acc(p.scionLayer.Mem(ubScionL), R2) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R21) // @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) @@ -2575,8 +2578,10 @@ func (p *scionPacketProcessor) validateIngressID( /*@ ghost ubScionL []byte, gho // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -2671,8 +2676,8 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghos // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetScionPath(ub) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R40) // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) @@ -2681,8 +2686,10 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghos // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported @@ -2714,8 +2721,8 @@ func (p *scionPacketProcessor) invalidSrcIA( // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetScionPath(ub) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R40) // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) @@ -2724,8 +2731,10 @@ func (p *scionPacketProcessor) invalidSrcIA( // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported @@ -2840,8 +2849,8 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @ // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.segmentChange, R20) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -2856,8 +2865,10 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @ // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3154,8 +3165,8 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -3172,8 +3183,10 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3255,8 +3268,8 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R15) && acc(p.d.Mem(), _) // pres for IO: // @ requires slayers.ValidPktMetaHdr(ubScionL) && p.scionLayer.EqAbsHeader(ubScionL) @@ -3275,8 +3288,10 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ ensures acc(&p.path, R20) // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures acc(sl.Bytes(ubScionL, 0, len(ubScionL)), 1-R15) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3670,8 +3685,8 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.Pkt @*/ ) (e // @ requires acc(p.scionLayer.Mem(ub), R2) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetScionPath(ub) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) @@ -3690,8 +3705,10 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.Pkt @*/ ) (e // @ ensures acc(p.scionLayer.Mem(ub), R2) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3747,8 +3764,8 @@ func (p *scionPacketProcessor) validateEgressUp( // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetScionPath(ub) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -3767,8 +3784,10 @@ func (p *scionPacketProcessor) validateEgressUp( // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -3876,8 +3895,8 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ requires acc(p.scionLayer.Mem(ub), R3) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires p.path == p.scionLayer.GetScionPath(ub) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(&p.ingressID, R21) // @ requires acc(&p.infoField, R20) @@ -3896,8 +3915,10 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ ensures acc(p.scionLayer.Mem(ub), R3) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -4002,8 +4023,8 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) { // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) @@ -4025,8 +4046,10 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) { // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr == nil ==> // @ respr === processResult{} @@ -4129,8 +4152,8 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( // @ requires acc(p.scionLayer.Mem(ubScionL), R3) // @ requires p.scionLayer.ValidPathMetaData(ubScionL) // @ requires p.path == p.scionLayer.GetScionPath(ubScionL) -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R20) // @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL) @@ -4139,8 +4162,10 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( // @ ensures acc(p.scionLayer.Mem(ubScionL), R3) // @ ensures sl.Bytes(ubScionL, 0, len(ubScionL)) // @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr !== processResult{} ==> -// @ respr.OutPkt === p.OutBuf() +// @ respr.OutPkt === p.buffer.UBuf() // @ ensures reserr == nil ==> // @ int(p.scionLayer.GetPayloadLen(ubScionL)) == len(p.scionLayer.GetPayload(ubScionL)) // @ ensures reserr != nil ==> reserr.ErrorMem() @@ -4188,8 +4213,8 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ requires sl.Bytes(ub, 0, len(ub)) // @ requires acc(&p.ingressID, R15) // @ requires acc(&p.segmentChange) && !p.segmentChange -// @ preserves p.SCMPBufMem() -// @ preserves sl.Bytes(p.OutBuf(), 0, len(p.OutBuf())) +// @ requires acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() +// @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL) // @ preserves acc(&p.infoField) @@ -4209,14 +4234,16 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ respr.OutAddr != nil && // @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.Bytes(ub, 0, len(ub)), R15))) // @ ensures !addrAliasesPkt ==> acc(sl.Bytes(ub, 0, len(ub)), R15) +// @ ensures acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() // @ ensures reserr == nil ==> p.scionLayer.Mem(ub) // @ ensures reserr == nil ==> p.path === p.scionLayer.GetScionPath(ub) // @ ensures reserr == nil ==> p.scionLayer.GetPath(ub) === old(p.scionLayer.GetPath(ub)) // @ ensures reserr == nil ==> p.scionLayer.UBPath(ub) === old(p.scionLayer.UBPath(ub)) // @ ensures reserr == nil ==> sl.Bytes(p.cachedMac, 0, len(p.cachedMac)) // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures respr.OutPkt != nil ==> -// @ (respr.OutPkt === ub || respr.OutPkt === p.OutBuf()) +// @ (respr.OutPkt === ub || respr.OutPkt === p.buffer.UBuf()) // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires p.d.DpAgreesWithSpec(dp) @@ -4919,13 +4946,13 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { // @ requires acc(&p.ingressID, R50) // @ requires acc(&p.buffer, R55) && p.buffer != nil && p.buffer.Mem() // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) -// @ ensures acc(&p.buffer, R55) && p.buffer != nil && p.buffer.Mem() -// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires cause != nil ==> cause.ErrorMem() // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R50) +// @ ensures acc(&p.buffer, R55) && p.buffer != nil && p.buffer.Mem() +// @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures result != nil ==> // @ result === p.buffer.UBuf() // @ ensures reserr != nil && reserr.ErrorMem() diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index 77676210a..e1958684a 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -211,33 +211,6 @@ pred (p *scionPacketProcessor) LastLayerMem(ub []byte, ubLL []byte, startLL int, (&p.scionLayer === p.lastLayer ==> ub === ubLL) } -// (VerifiedSCION) The buffer that an SCMP reply is serialized into. Like the -// last layer, every check along 'process's path has to carry it even though only -// 'packSCMP' writes to it, so the three assertions that describe it travel in -// both directions across each of the seventeen calls. -// -// The permission to the buffer's *bytes* deliberately stays outside: the results -// that alias them are described by postconditions such as -// 'absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported', whose -// well-definedness needs 'sl.Bytes(respr.OutPkt, ..)' to be framed by the -// contract itself. Hiding it inside the predicate would make those clauses -// ill-defined, and stating them under an 'unfolding' would cost more than the -// bundling saves. -pred (p *scionPacketProcessor) SCMPBufMem() { - acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() -} - -// The bytes of that buffer. A check that answers with an SCMP message returns a -// result that aliases them, and says so with this function rather than by -// opening the predicate. It mirrors 'sInitBufferUBuf', which does the same one -// level up, through 'sInit'. -ghost -requires acc(p.SCMPBufMem(), _) -decreases -pure func (p *scionPacketProcessor) OutBuf() []byte { - return unfolding acc(p.SCMPBufMem(), _) in p.buffer.UBuf() -} - pred (p *scionPacketProcessor) initMem() { acc(&p.d) && acc(&p.ingressID) && From 4b7947f78a34a5ac4ce67874f9e19c841760ab56 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 7 Sep 2026 08:15:31 +0000 Subject: [PATCH 07/10] Record why the SCMP buffer resists the LastLayerMem treatment 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 Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z --- verification/PERFORMANCE.md | 73 ++++++++++++++++++++++++++++++------- 1 file changed, 59 insertions(+), 14 deletions(-) diff --git a/verification/PERFORMANCE.md b/verification/PERFORMANCE.md index 223a1bb3d..2d886dc31 100644 --- a/verification/PERFORMANCE.md +++ b/verification/PERFORMANCE.md @@ -216,27 +216,72 @@ layer and the facts about it are still immediate, is free (350 s against a 342 s baseline). `process`, `processSCION` and `processEPIC` then just take the predicate as a parameter and never open it. +## The same recipe on the SCMP buffer: no gain, and why + +The obvious next target was the other thing every validator carries and almost +none of them touches: the buffer that `packSCMP` serialises an SCMP reply into. +It is four clauses — two `requires`, two `ensures` — in the contract of +seventeen members: + +``` +requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() +ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) +``` + +This was implemented as `SCMPBufMem()` plus an `OutBuf()` getter, all seventeen +members verified with 0 errors, and it bought **nothing**: 2497 s against 2490 s +for `process` in a paired A/B. It was reverted (`e0d004b`). Two things are worth +knowing before anyone tries it again. + +**Only the implications were ever the cost.** `LastLayerMem` won because two of +the four clauses it absorbed were impure implications, which Silicon branches on +and re-joins at every exhale *and* every inhale. The buffer clauses are plain +conjunctions: one field chunk, one predicate chunk. Turning them into a single +predicate chunk changes the constant, not the shape, and the measurement says +the constant is not where the time is. This is the same lesson as the failures +above, in a case where the change did shrink the contract: the number of clauses +is not the cost — the number of *branches* is. + +**The permission to the bytes cannot move into a predicate at all.** Postconditions +such as + +``` +ensures respr.OutPkt != nil ==> !slayers.IsSupportedPkt(respr.OutPkt) +ensures reserr != nil && respr.OutPkt != nil ==> + absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +``` + +are stated over the *result*, which aliases the buffer, and both `IsSupportedPkt` +and `absIO_val` require `sl.Bytes(raw, 0, len(raw))` at write permission. A +predicate cannot frame a clause stated outside itself, so hiding +`sl.Bytes(p.buffer.UBuf(), …)` inside `SCMPBufMem()` makes those clauses +ill-defined at fifteen sites — which is what the first attempt did, and it fails +with `Precondition of call slayers.IsSupportedPkt(respr.OutPkt) might not hold`. +Restating each of them under `unfolding p.SCMPBufMem() in …` would work and +would cost more than the bundling saves. The permission therefore has to stay a +contract clause, which by itself caps how much of the buffer's footprint can be +bundled. + ## What is left to try -Same recipe, other resources. - -1. **Bundle the rest of the footprint the validators share.** Three more clauses - are common to all of them — `acc(&p.buffer, R50) && p.buffer != nil && - p.buffer.Mem()`, `sl.Bytes(p.buffer.UBuf(), …)` and `respr !== - processResult{} ==> respr.OutPkt === p.buffer.UBuf()` — plus permission to - `p.d` and `p.path`. The buffer is harder than the last layer, because that - last clause mentions `p.buffer.UBuf()` and would need an `unfolding` or an - opaque getter. -2. **Bundle the per-message resources in `rc`'s loop invariants**, so that an - iteration exchanges one predicate instead of six quantified assertions over +1. **Bundle the per-message resources in `rc`'s loop invariants**, so that an + iteration exchanges one predicate instead of seven quantified assertions over the 64-message batch. This needs a range predicate with take/put lemmas, - since the body still has to get at one message at a time. -3. **Reduce the number of distinct permission amounts.** `p.scionLayer.Mem(..)` + since the body still has to get at one message at a time. Note that the same + framing wall is waiting: the invariants + `forall i :: i0 <= i && i < pkts ==> typeOf(msgs[i].GetAddr()) == …` and + `forall i :: MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]` are pure facts + framed by the `msgs[i].Mem()` in the invariant next to them, so they have to + enter the predicate together with it, and the body's assertions over the + `i0 < i < pkts` range then need a way to see them again. +2. **Reduce the number of distinct permission amounts.** `p.scionLayer.Mem(..)` is currently used at 18 of them, and the `unfold acc(P, 1-R55)` / `unfold acc(P, R55)` idiom exists only so that a pure function can be evaluated in between. Every extra fraction is another chunk for the complete exhale to summarise. -4. **Outline the branches of `process`.** `Run` uses seven `outline` blocks; +3. **Outline the branches of `process`.** `Run` uses seven `outline` blocks; `process` and `processPkt` use none. An outlined block is verified as its own Viper method, so the state that the rest of `process` carries past it is whatever the outline's contract says, not everything the branch touched. From 9c09e83f64c6ed96d64fb3a17f5577169beab2b2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 7 Sep 2026 08:41:12 +0000 Subject: [PATCH 08/10] Localise the rc closure: half of it is one invariant exhale 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 Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z --- verification/PERFORMANCE.md | 69 ++++++++++++++++++++++++++++++------- 1 file changed, 56 insertions(+), 13 deletions(-) diff --git a/verification/PERFORMANCE.md b/verification/PERFORMANCE.md index 2d886dc31..0743a7b68 100644 --- a/verification/PERFORMANCE.md +++ b/verification/PERFORMANCE.md @@ -116,11 +116,42 @@ identical* clauses (permission to `p.d`, `p.path`, `p.buffer`, `p.buffer.UBuf()`, `p.lastLayer`, and `p.d.validResult`). The `rc` closure has no postcondition at all, and cutting its body away brings -its run down to the front end alone (152 s): all 26 minutes are the two -nested loops, whose invariants carry quantified assertions over the 64-message -batch — including `forall i :: MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]`, -which unfolds the whole packet abstraction for every message — and are -re-established on every iteration. +its run down to the front end alone (152 s), so all of its time is in the two +nested loops. Cutting inside them says exactly where: + +| what runs | s | +|---|---| +| the outer loop entered, its body skipped | 178 | +| the outer body, up to the inner loop entered with its body skipped | 177 | +| … the inner body up to the `processPkt` call | 229 | +| … including the `processPkt` call | 230 | +| … up to `WriteBatch` | 432 | +| the whole inner body, but not the invariant exhale that follows it | 1027 | +| the whole closure | 2186 | + +Three things follow, and the first two are the opposite of what one would guess. + +**The invariants are cheap to establish and cheap to inhale.** The outer loop's +eighteen and the inner loop's twenty-five together cost nothing measurable: the +run with both loops entered and both bodies skipped is still at the front-end +floor. So is the whole read-batch block, with its prophecy variable, its +`MultiReadBio` unfoldings and its four quantified assertions over the batch. + +**The call to `processPkt` is free** — 229 s before it, 230 s after it — even +though its contract is one of the largest in the package. Inhaling a big +postcondition into a state this small is not what costs. + +**One exhale accounts for half of the closure.** The difference between the last +two rows, ~1160 s, is a single step: exhaling the inner loop's twenty-five +invariants on the fall-through path at the end of the body. The same exhale on +the four `continue` paths, which happen earlier and in a smaller state, is +included in the rows above it and is far cheaper. Seven of those invariants are +quantified over the 64-message batch — `msgs[i].Mem()`, +`sl.Bytes(msgs[i].GetFstBuffer(), …)`, and five pure facts about `msgs[i]` +including `MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]`, which unfolds the +whole packet abstraction for every message — and they have to be re-established +over everything the body has accumulated by then: the packet's byte ranges split +and recombined, the write-message permissions, the IO-spec place and state. ## Contributing factors @@ -266,16 +297,28 @@ bundled. ## What is left to try -1. **Bundle the per-message resources in `rc`'s loop invariants**, so that an - iteration exchanges one predicate instead of seven quantified assertions over - the 64-message batch. This needs a range predicate with take/put lemmas, - since the body still has to get at one message at a time. Note that the same - framing wall is waiting: the invariants +1. **Bundle the per-message resources in `rc`'s loop invariants**, so that the + one expensive exhale hands over a single predicate instead of seven + quantified assertions over the 64-message batch. The profile above makes this + the best-motivated candidate left in the package: half of `rc` is that one + step. + + The bundling only pays if the predicate is *not* folded in the loop body, + because a `fold` would re-do the same quantified work in the same large + state. It has to be closed by a lemma — `MsgsMemHole(msgs, i0, …)` plus the + one message that was taken out, giving back `MsgsMem(msgs, i0+1, …)` — so + that the quantified reasoning happens once, inside a member whose state holds + nothing but the batch. The body then pays two predicate chunks per iteration. + + The framing wall from the buffer is waiting here too: the invariants `forall i :: i0 <= i && i < pkts ==> typeOf(msgs[i].GetAddr()) == …` and `forall i :: MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]` are pure facts - framed by the `msgs[i].Mem()` in the invariant next to them, so they have to - enter the predicate together with it, and the body's assertions over the - `i0 < i < pkts` range then need a way to see them again. + framed by the `msgs[i].Mem()` next to them, so they have to enter the + predicate together with it. That is affordable here, unlike in the buffer + case: the one body assertion that reads them back — the `forall i :: i0 < i + && i < pkts ==> MsgToAbsVal(…) == ioValSeq[i]` marked as "crucial to keep + verification stable" — exists only to re-establish the invariant for the next + iteration, which is exactly what the closing lemma would prove instead. 2. **Reduce the number of distinct permission amounts.** `p.scionLayer.Mem(..)` is currently used at 18 of them, and the `unfold acc(P, 1-R55)` / `unfold acc(P, R55)` idiom exists only so that a pure function can be From 783973ab68609394a79e8158530c5f550f1b22d7 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 7 Sep 2026 19:29:29 +0000 Subject: [PATCH 09/10] Bundle the read batch into a predicate: the 'rc' closure 4x faster 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 Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z --- router/dataplane.go | 32 +++++----- router/msgs-spec.gobra | 134 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 150 insertions(+), 16 deletions(-) create mode 100644 router/msgs-spec.gobra diff --git a/router/dataplane.go b/router/dataplane.go index ad47677ed..19307e4b1 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1021,13 +1021,16 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) // @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> // @ MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i] + // @ fold MsgsMem(msgs, 0, pkts, ingressID, ioValSeq) // (VerifiedSCION) using regular for loop instead of range loop to avoid unnecessary // complications with permissions // @ invariant acc(&scmpErr) - // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() - // @ invariant forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> - // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) + // (VerifiedSCION) the six quantified invariants that described the batch + // - two permissions and the four pure facts only they can frame - are + // bundled into this predicate, so that the exhale at the end of the body + // hands over one chunk. 'TakeMsg' and 'PutMsg' open and close it. + // @ invariant MsgsMem(msgs, i0, pkts, ingressID, ioValSeq) // @ invariant writeMsgInv(writeMsgs) // @ invariant acc(dPtr, _) && *dPtr === d // @ invariant acc(d.Mem(), _) && d.WellConfigured() @@ -1038,12 +1041,6 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ invariant acc(rd.Mem(), _) // @ invariant pkts <= len(msgs) // @ invariant 0 <= i0 && i0 <= pkts - // @ invariant forall i int :: { &msgs[i] } i0 <= i && i < len(msgs) ==> - // @ msgs[i].HasActiveAddr() - // @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> - // @ typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr] - // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> - // @ msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) // @ invariant processor.sInit() && processor.sInitD() === d // @ invariant let ubuf := processor.sInitBufferUBuf() in // @ acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm) @@ -1054,12 +1051,14 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ invariant ioIngressID == path.ifsToIO_ifs(ingressID) // @ invariant acc(ioLock.LockP(), _) // @ invariant ioLock.LockInv() == SharedInv{dp, ioSharedArg} - // @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> - // @ MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i] // @ invariant MultiElemWitnessWithIndex(ioSharedArg.IBufY, ioIngressID, ioValSeq, i0) // @ decreases pkts - i0 for i0 := 0; i0 < pkts; i0++ { // @ assert &msgs[:pkts][i0] == &msgs[i0] + // (VerifiedSCION) take this message out of the batch. Doing it with a + // lemma rather than an 'unfold' keeps the quantified reasoning over the + // batch out of this body, which is the whole point of the predicate. + // @ ghost excl := TakeMsg(msgs, i0, pkts, ingressID, ioValSeq) // @ preserves 0 <= i0 && i0 < pkts && pkts <= len(msgs) // @ preserves acc(msgs[i0].Mem(), R1) // @ ensures p === msgs[:pkts][i0].GetMessage() @@ -1105,11 +1104,6 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ assert sl.Bytes(tmpBuf, 0, p.N) // @ assert sl.Bytes(tmpBuf, 0, len(tmpBuf)) result, err /*@ , addrAliasesPkt, newAbsPkt @*/ := processor.processPkt(tmpBuf, srcAddr /*@, ioLock, ioSharedArg, dp @*/) - // (VerifiedSCION) This assertion is crucial to keep verification stable. Without it, - // the fold operation in the branch protected by the condition `result.OutConn == nil` - // may fail non-deterministically. - // @ assert forall i int :: { &msgs[i] } i0 < i && i < pkts ==> - // @ MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i] // @ fold scmpErr.Mem() switch { @@ -1141,6 +1135,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ assert 0 <= m.N // @ msgs[:pkts][i0].IsActive = false // @ fold msgs[:pkts][i0].Mem() + // @ PutMsg(msgs, i0, pkts, ingressID, ioValSeq, excl) log.Debug("Error processing packet", "err", err) // @ assert acc(inputCounters.DroppedPacketsTotal.Mem(), _) // @ prometheus.CounterMemImpliesNonNil(inputCounters.DroppedPacketsTotal) @@ -1156,6 +1151,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ sl.CombineRange_Bytes(p.Buffers[0], 0, p.N, writePerm) // @ msgs[:pkts][i0].IsActive = false // @ fold msgs[:pkts][i0].Mem() + // @ PutMsg(msgs, i0, pkts, ingressID, ioValSeq, excl) continue } @@ -1207,6 +1203,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ sl.CombineRange_Bytes(p.Buffers[0], 0, p.N, writePerm) // @ msgs[:pkts][i0].IsActive = false // @ fold msgs[:pkts][i0].Mem() + // @ PutMsg(msgs, i0, pkts, ingressID, ioValSeq, excl) // @ fold writeMsgInv(writeMsgs) if err != nil { // @ requires err != nil && err.ErrorMem() @@ -1246,6 +1243,9 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta outputCounters.OutputBytesTotal.Add(float64(len(result.OutPkt))) // @ ) } + // (VerifiedSCION) the batch goes back to the outer loop, and to the next + // ReadBatch, as the two quantified permissions they are stated with. + // @ unfold MsgsMem(msgs, pkts, pkts, ingressID, ioValSeq) } } // @ unfold acc(d.Mem(), R1) diff --git a/router/msgs-spec.gobra b/router/msgs-spec.gobra new file mode 100644 index 000000000..532637665 --- /dev/null +++ b/router/msgs-spec.gobra @@ -0,0 +1,134 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package router + +import ( + "net" + + "golang.org/x/net/ipv4" + + "verification/io" + sl "verification/utils/slices" + . "verification/utils/definitions" +) + +// (VerifiedSCION) The per-message resources of one read batch, as the loop that +// processes the batch carries them. +// +// Measuring the packet loop says that half of its cost is a single step: +// exhaling the twenty-five invariants of the inner loop on the fall-through +// path at the end of its body, over everything that body has accumulated by +// then. Six of those invariants are quantified over the whole 64-message batch, +// and they are what make that exhale expensive: two carry permission, and the +// other four are pure facts that only the first two can frame, so they have to +// travel together. Bundled here, the exhale hands over one chunk. +// +// 'i0' is the index the loop is about to process. Messages before it have been +// consumed - their address is no longer guaranteed live, and their abstraction +// no longer has to agree with the IO specification - while messages from 'i0' +// on are still exactly as 'ReadBatch' left them. +pred MsgsMem(msgs []ipv4.Message, i0 int, pkts int, ingressID uint16, ioValSeq seq[io.Val]) { + 0 <= i0 && i0 <= pkts && pkts <= len(msgs) && pkts <= len(ioValSeq) && + (forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> + msgs[i].Mem()) && + (forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> + sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer()))) && + (forall i int :: { &msgs[i] } i0 <= i && i < len(msgs) ==> + msgs[i].HasActiveAddr()) && + (forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> + typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr]) && + (forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> + msgs[i].GetN() <= len(msgs[i].GetFstBuffer())) && + (forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> + MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]) +} + +// The same, with message 'i0' taken out. This is what the body of the loop +// holds on to while it works on that one message. +// +// 'excl' is that message's buffer, and the last conjunct is the only reason the +// predicate needs it. Both quantified permissions above are keyed on +// 'msgs[i].GetFstBuffer()', so folding either one obliges Silicon to show that +// no two messages share a buffer. Inside the batch that fact comes for free - +// '--assumeInjectivityOnInhale' asserts it every time the quantified permission +// is inhaled - but the message that has been taken out is no longer part of any +// such inhale, so putting it back would leave its buffer unrelated to the rest. +// Naming the buffer here carries the one missing inequality across the hole. +pred MsgsMemHole(msgs []ipv4.Message, i0 int, pkts int, ingressID uint16, ioValSeq seq[io.Val], excl []byte) { + 0 <= i0 && i0 < pkts && pkts <= len(msgs) && pkts <= len(ioValSeq) && + (forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) && i != i0 ==> + msgs[i].Mem()) && + (forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) && i != i0 ==> + sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer()))) && + (forall i int :: { &msgs[i] } i0 <= i && i < len(msgs) && i != i0 ==> + msgs[i].HasActiveAddr()) && + (forall i int :: { &msgs[i] } i0 <= i && i < pkts && i != i0 ==> + typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr]) && + (forall i int :: { &msgs[i] } 0 <= i && i < pkts && i != i0 ==> + msgs[i].GetN() <= len(msgs[i].GetFstBuffer())) && + (forall i int :: { &msgs[i] } i0 <= i && i < pkts && i != i0 ==> + MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]) && + (forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) && i != i0 ==> + msgs[i].GetFstBuffer() !== excl) +} + +// Take message 'i0' out of the batch. +// +// The point of doing this in a lemma rather than with an 'unfold' in the loop +// body is that the quantified reasoning then happens here, in a member whose +// state holds nothing but the batch, instead of in the body, where it would run +// over the packet's split byte ranges, the write-message permissions and the +// IO-spec place and state as well. Unfolding the predicate in the body would +// give back exactly the six invariants this is meant to replace. +ghost +requires MsgsMem(msgs, i0, pkts, ingressID, ioValSeq) +requires 0 <= i0 && i0 < pkts && pkts <= len(msgs) && pkts <= len(ioValSeq) +ensures MsgsMemHole(msgs, i0, pkts, ingressID, ioValSeq, excl) +ensures msgs[i0].Mem() +ensures sl.Bytes(msgs[i0].GetFstBuffer(), 0, len(msgs[i0].GetFstBuffer())) +ensures excl === msgs[i0].GetFstBuffer() +ensures msgs[i0].HasActiveAddr() +ensures typeOf(msgs[i0].GetAddr()) == type[*net.UDPAddr] +ensures msgs[i0].GetN() <= len(msgs[i0].GetFstBuffer()) +ensures MsgToAbsVal(&msgs[i0], ingressID) == ioValSeq[i0] +decreases +func TakeMsg(msgs []ipv4.Message, i0 int, pkts int, ingressID uint16, ioValSeq seq[io.Val]) (excl []byte) { + unfold MsgsMem(msgs, i0, pkts, ingressID, ioValSeq) + excl = msgs[i0].GetFstBuffer() + fold MsgsMemHole(msgs, i0, pkts, ingressID, ioValSeq, excl) +} + +// Put message 'i0' back and move on to the next one. +// +// What comes back is deliberately weaker than what 'TakeMsg' handed out: the +// loop body consumes the message's address and forwards its bytes, so neither +// 'HasActiveAddr' nor the agreement with 'ioValSeq' still holds for 'i0'. That +// is exactly why the predicate is indexed by 'i0': those two facts are only +// claimed from the current index on. +ghost +requires MsgsMemHole(msgs, i0, pkts, ingressID, ioValSeq, excl) +requires 0 <= i0 && i0 < pkts && pkts <= len(msgs) && pkts <= len(ioValSeq) +requires msgs[i0].Mem() +requires sl.Bytes(msgs[i0].GetFstBuffer(), 0, len(msgs[i0].GetFstBuffer())) +requires excl === msgs[i0].GetFstBuffer() +requires msgs[i0].GetN() <= len(msgs[i0].GetFstBuffer()) +ensures MsgsMem(msgs, i0+1, pkts, ingressID, ioValSeq) +decreases +func PutMsg(msgs []ipv4.Message, i0 int, pkts int, ingressID uint16, ioValSeq seq[io.Val], excl []byte) { + unfold MsgsMemHole(msgs, i0, pkts, ingressID, ioValSeq, excl) + fold MsgsMem(msgs, i0+1, pkts, ingressID, ioValSeq) +} From 30c58febe5dac74d3a11be3109dc5c5cd5769492 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 7 Sep 2026 20:27:21 +0000 Subject: [PATCH 10/10] Record the MsgsMem result and what made it work 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 Claude-Session: https://claude.ai/code/session_018j1geecD2ctEGUunysNv5z --- verification/PERFORMANCE.md | 78 ++++++++++++++++++++++++------------- 1 file changed, 52 insertions(+), 26 deletions(-) diff --git a/verification/PERFORMANCE.md b/verification/PERFORMANCE.md index 0743a7b68..ec80290f3 100644 --- a/verification/PERFORMANCE.md +++ b/verification/PERFORMANCE.md @@ -24,8 +24,9 @@ each of them is Gobra's front end, which the isolated runs cannot avoid. | the `rc` closure of `Run` (`closureCall$rc_Run…`) | 26 min | 2.5 min | | `process` | 109 min | 4 min | -(`process` is now 62 min — see *What did work* below. The rest of the table, and -the whole analysis, describes the state before that change.) +(`process` and `rc` are now 62 min and 6.4 min — see the two *What did work* +sections below. The rest of the table, and the whole analysis, describes the +state before those changes.) The "contract alone" column comes from cutting the body at its first statement (see below): it is what the run still costs when the member has no body left. @@ -295,36 +296,61 @@ would cost more than the bundling saves. The permission therefore has to stay a contract clause, which by itself caps how much of the buffer's footprint can be bundled. +## What did work: `MsgsMem` + +Same recipe, applied where the profile said the money was, and it paid: the `rc` +closure went from **1538 s to 384 s - 4.0x - in a paired A/B**, both arms +reporting 0 errors. + +`MsgsMem(msgs, i0, pkts, ingressID, ioValSeq)` in `msgs-spec.gobra` bundles the +six invariants of the inner loop that are quantified over the 64-message batch: +the two permissions, `msgs[i].Mem()` and `sl.Bytes(msgs[i].GetFstBuffer(), ...)`, +and the four pure facts that only those permissions can frame. The one expensive +exhale now hands over a single chunk. + +**The lemmas are the point, not the predicate.** Opening the batch with an +`unfold` at the top of the loop body and closing it with a `fold` at the bottom +would buy nothing: the fold would re-do the same quantified work in the same +large state, which is precisely what the invariant exhale was doing. `TakeMsg` +and `PutMsg` are lemmas, so the loop body exchanges two predicate chunks and the +quantified reasoning happens inside members whose state holds nothing but the +batch. Entering and leaving the loop is a plain `fold`/`unfold`, which is free - +the profile above shows the whole region around `ReadBatch` at the front-end +floor. + +**`PutMsg` gives back less than `TakeMsg` handed out.** The body consumes the +message's address and forwards its bytes, so neither `HasActiveAddr` nor the +agreement with `ioValSeq` still holds for that message. That is what the index +`i0` is for: those two facts are claimed only from the current position on, and +`PutMsg` closes the predicate at `i0+1`. It also retires the assertion that was +marked "crucial to keep verification stable" - it existed only to re-establish +the invariant for the next iteration, which `PutMsg` now proves. + +**Taking a message out breaks buffer injectivity, and that has to be repaired +explicitly.** 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 fact is free, because `--assumeInjectivityOnInhale` +asserts it whenever the quantified permission is inhaled - but the message that +has been taken out is no longer part of any such inhale, so putting it back +leaves its buffer unrelated to the rest and `PutMsg`'s fold fails with +`Quantified resource ... might not be injective`. `MsgsMemHole` therefore takes +the extracted buffer as a parameter and carries the one missing inequality +across the hole. + +An earlier attempt keyed the permissions on `&msgs[i]` instead, by bundling +`Mem()` and the bytes into a per-element `MsgAndBuf` predicate. That is injective +by construction and `PutMsg` goes through - but the obligation simply moves to +the lemma that has to convert back for the next `ReadBatch`, which is stated in +terms of the buffer-keyed quantifiers. Naming the buffer is the shorter way out. + ## What is left to try -1. **Bundle the per-message resources in `rc`'s loop invariants**, so that the - one expensive exhale hands over a single predicate instead of seven - quantified assertions over the 64-message batch. The profile above makes this - the best-motivated candidate left in the package: half of `rc` is that one - step. - - The bundling only pays if the predicate is *not* folded in the loop body, - because a `fold` would re-do the same quantified work in the same large - state. It has to be closed by a lemma — `MsgsMemHole(msgs, i0, …)` plus the - one message that was taken out, giving back `MsgsMem(msgs, i0+1, …)` — so - that the quantified reasoning happens once, inside a member whose state holds - nothing but the batch. The body then pays two predicate chunks per iteration. - - The framing wall from the buffer is waiting here too: the invariants - `forall i :: i0 <= i && i < pkts ==> typeOf(msgs[i].GetAddr()) == …` and - `forall i :: MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]` are pure facts - framed by the `msgs[i].Mem()` next to them, so they have to enter the - predicate together with it. That is affordable here, unlike in the buffer - case: the one body assertion that reads them back — the `forall i :: i0 < i - && i < pkts ==> MsgToAbsVal(…) == ioValSeq[i]` marked as "crucial to keep - verification stable" — exists only to re-establish the invariant for the next - iteration, which is exactly what the closing lemma would prove instead. -2. **Reduce the number of distinct permission amounts.** `p.scionLayer.Mem(..)` +1. **Reduce the number of distinct permission amounts.** `p.scionLayer.Mem(..)` is currently used at 18 of them, and the `unfold acc(P, 1-R55)` / `unfold acc(P, R55)` idiom exists only so that a pure function can be evaluated in between. Every extra fraction is another chunk for the complete exhale to summarise. -3. **Outline the branches of `process`.** `Run` uses seven `outline` blocks; +2. **Outline the branches of `process`.** `Run` uses seven `outline` blocks; `process` and `processPkt` use none. An outlined block is verified as its own Viper method, so the state that the rest of `process` carries past it is whatever the outline's contract says, not everything the branch touched.