Scaling families for the program dimensions where verification cost is non-linear

[JonasAlaif]

The scaling suite measured cost as a function of ten program dimensions, all of
them close to linear on main. The earlier performance work found many more
dimensions along which Helium's cost grows faster than the program: enum width,
struct and tuple width, nesting, match width, decision chains, reborrows, aliasing
under the path condition, units per file, method length. None of them had a
generated family, so no later change could show a scaling exponent before and
after, and the perf gate saw no non-linear shape at all. This PR adds a family for
each such dimension, records main's exponents on every family (old and new) as
the baseline, and puts small points of the families whose deterministic counters
grow non-linearly under the perf_regression band.

Branch scaling-families, base origin/main (13091f3). No verifier code changes.

What is added

14 families in benchmarks/scaling/ (generators gen_{enums,match,width,borrows,generic,size,pcalias}.py,
suite.json entries, src/ + committed Prusti vpr/). One knob each, everything else fixed;
sources follow genlib.py's rules (spec-less, no recursion / returned references / arrays / panics).

family (stem)	knob	values	old-branch axis it reproduces
struct_width (struct_w{W})	struct fields	4..96	struct width sw (n^3.39 at the time)
tuple_width (tuple_w{W})	tuple elements	2..20	tuple width tw (n^3.4-3.7)
enum_tag (enum_tag_v{N})	fieldless enum variants (tag match + from int match)	8..128	enum-N ladder (N^2.0-2.28, p_E_snap; itertools, rustls)
enum_fields (enum_fields_n{N})	enum-typed struct fields, each matched	2..32	enum-in-struct / struct-of-enums es/se
option_depth (option_d{D})	Option nesting peeled by nested matches	2..16	Option nesting om
nway (nway_k{K})	arms of one integer match, one join	4..128	n-way match (rustls CipherSuite::from), guard-conjunction depth, disproven equalities on the scrutinee
seqmatch (seqmatch_k{K})	sequential (if builds enum, match takes it apart) pairs	2..32	decision diamonds md (reach DNF; correlated branches)
reborrow (reborrow_n{N})	sequential reborrow-write pairs	4..64	sequential reborrows sb
condmove (condmove_k{K})	sequential conditional moves of one local	1..32	conditional updates per location (base64 ChunkPerm Select trees)
generic (generic_k{K})	round trips through a generic identity	2..64	boxing round trips (make_generic/make_concrete, unicode-ident)
impls (impls_k{K})	impls of one trait (only one used)	2..64	trait impls per trait / dead quantifiers (either, itertools)
units (units_k{K})	independent functions, one struct type each	4..64	units x program (per-unit whole-program work: rand, serde)
straight (straight_k{K})	statements in one straight-line body	16..128	method length / ground size within a method (serde_derive, rustls)
pcalias (pcalias_k{K}, Viper-only)	chunks that alias x only under a branch; K exhales	2..8	pc-alias set size (serde_derive residues)

Already covered on main and not duplicated: payload depth and payload-enum width
(rust/enum_v{N}_p{D}), independent sequential branches (seq_if), struct depth,
call depth/fan-out, argument count, block length (rust/depth, arith, mut_writes).
Not given a family: CFG block count and file size (linear / small constants on the
old branch), disproven-equality pairs (exercised by nway/enum_tag; the syn/ryu
shapes were not reproduced in spec-less Rust).

Also: benchmarks/scaling/expected_failures.txt records the pre-existing loops family's
failures (all 8 points, m_run: write through &mut in a loop, the shape of
loops/mutate_in_loop::m_bump_n). Silicon rejects all 8 at the same postcondition, so they are a
limitation of the encoding, not of main. Every new point verifies on main.
Commit b5840a1 on this branch updates the loops comment in expected_failures.txt to say so.

Design

• No shared references in the Rust sources. The Prusti used for encoding (rewrite-2023
  b51f8e0, newer than the one behind main's existing encodings) encodes &T with a
  read() fraction, and p_Ref_immutable_snap then fails on main ("insufficient
  permission" at p_Param_snap#requires) in every file that mentions &T.
  Silicon verifies these files: it reads permission amounts in function preconditions as
  wildcards, while main checks the exact write against the read() the predicate holds, so
  this is an incompleteness of main (recorded in design/rebuild/gaps.md). It is constant per
  file and orthogonal to every axis, so reads go through owned values or &mut instead and
  every family verifies clean. (A gap to know about before re-encoding
  the older suites with this Prusti.)
• Conditional ownership as conditional moves. The first attempt (a reborrow chosen by a
  branch, let r = if c { &mut a } else { &mut b }) fails on main already at one step
  (p_Ref_mutable_snap#requires), and Silicon rejects it at the same place (precondition of
  p_Ref_mutable_snap): the encoding, not main, loses the joined borrow's permission. A
  conditional move of one local verifies on both and still makes its ownership path-dependent
  K times over.
• pc-alias is Viper-only: safe Rust never aliases references. The family exhales x.f in
  K fractions under a branch equating x with K references. Writing x.f instead fails on
  main at K=2 (assign does not sum pc-alias partners; it also fails with x == y0 && x == y1
  in the precondition), as does reading x.f and relating it to y1.f; Silicon verifies both
  (probes in scaling_baseline/probes/pa2.vpr), so both are incompletenesses of main (in
  design/rebuild/gaps.md). The exhale form the family uses verifies on both.
• Sizes: the largest point takes seconds to ~15 s on main; points that time out or fail
  were dropped (listed in the baseline README). New encodings: ~21 MB on disk, ~1.1 MB gzipped
  (the existing 74 are ~0.55 MB gzipped); the largest file is 1.35 MB (units_k64).

Baseline: main's exponents (the "before" column)

Full table, raw data and exact commands: design/rebuild/scaling_baseline/
(table.md, points.csv, scaling.json, rust_families.json, cputime.json, README.md).
Binary: main 13091f3, release, codegen-units=1, sha256 d47f387c…9d36b. Time and CPU are net
of the 0.201 s per-process floor (egg's clock calibration); e = log-log slope over all points,
tail = slope between the two largest points. CPU = min of 3 interleaved runs (wall medians
were taken under load up to 40 and agree with CPU within noise). Counter exponents are over
all points. All points verify unless noted.

family	knob	range	max wall (s)	CPU e	CPU tail	rule_apps	nodes_pk	prove	sat_it
pcalias	chunks	2..8	4.3	5.47 (exponential, x4/step at the top)	11.7	5.11	3.89	3.28	3.09
rust/enum	variants (p=1/2/3)	2..8	11/21/28	2.34/2.39/2.50	2.75/2.75/2.87	1.41/1.37/1.32	1.28/1.30/1.32	0.88-0.90	0.83-0.84
enum_tag	variants	8..128	3.6	2.31	2.55	1.47	1.04	0.86	0.78
tuple_width	elements	2..20	2.3	2.06	3.11	1.37	1.42	1.40	0.87
arith	ops	5..80	16.4	2.02	2.28	1.82	1.08	0.85	0.87
enum_fields	fields	2..32	7.4	1.95	2.44	1.24	1.10	0.83	0.81
straight	statements	16..128	14.7	1.92	2.04	0.94	0.99	0.92	0.82
struct_width	fields	4..96	15.9	1.91	3.16	1.13	1.42	0.89	0.76
option_depth	depth	2..16	1.3	1.89	2.39	2.39	1.28	0.70	0.78
seqmatch	decisions	2..32	12.6	1.87	2.16	1.19	1.02	0.85	0.83
units	units	4..64	6.8	1.66	2.35	1.07	0.21	0.96	0.94
reborrow	reborrows	4..64	4.8	1.66	2.02	0.94	0.95	0.86	0.75
impls	impls	2..64	8.0	1.62	2.54	0.80	0.17	0.81	0.79
generic	round trips	2..64	1.8	1.54	1.89	0.71	0.89	0.76	0.73
args_mut	args	1..16	0.5	1.44	1.81	0.83	1.06	0.83	0.77
seq_if	branches	1..16	1.1	1.39	1.90	0.80	0.90	0.78	0.66
struct_depth	depth	1..6	1.0	1.37	3.31	1.72	1.35	0.69	0.66
nway	arms	4..128	2.9	1.33	2.47	1.04	1.31	0.73	0.00
rust/depth	depth (m=5)	2..8	1.8	1.30	1.68	0.58	0.82	0.54	0.50
mut_writes	writes (p=4)	1..32	0.9	1.08	1.81	0.68	0.91	0.74	0.42
args_value	args	1..16	0.3	1.01	1.43	0.84	1.21	0.88	0.90
call_fanout	fanout	1..16	0.5	0.95	0.98	1.06	1.07	0.82	0.75
rust/enum	payload (v=2..8)	1..3	28	0.75-0.94	1.1-1.5	0.46-0.57	0.63-0.67	0.23-0.25	0.09
condmove	moves	1..32	0.3	0.73	1.45	0.36	0.68	0.60	0.39
args_ref	args	1..16	0.3	0.73	1.24	0.76	1.19	0.70	0.76
call_depth	depth	1..16	0.4	0.73	0.94	0.92	0.00	0.70	0.71
loops	nesting (b=5/20)	1..4	0.25	~0.1	-	0	~0.1	0	0

loops is a gap family: all 8 points fail m_run (expected_failures.txt), so its cost is
the cost of failing early.

Readings:

• Exponential: pcalias (every counter x3 per extra chunk; K=10 takes 76 s and fails,
  K=12 >400 s).
• Quadratic or worse in time, with super-linear counters: payload enums in N, enum_tag,
  tuple_width, arith, option_depth (rule applications D^2.4), struct_width (nodes W^1.4,
  CPU tail 3.2), struct_depth.
• Quadratic in time with linear counters (per-operation cost grows with the accumulated
  graph, which no aggregate counter on main measures): straight, seqmatch, units,
  impls, reborrow, enum_fields, and the tails of nway, generic, seq_if.
• Linear: condmove, call_depth, args_*, call_fanout, rust/depth statements.
• Completeness at size: straight_k256 fails (peak 100,096 nodes: the node backstop is hit)
  and pcalias_k10 fails; neither is in the suite, both are recorded in the baseline README.

perf_regression: small points of the non-linear families

tests/perf_regression.rs now also gates SCALING_POINTS: two points (one knob step apart)
of each family whose counters grow non-linearly: pcalias_k4/k5, enum_tag_v8/v16,
option_d2/d4, struct_w4/w8, tuple_w2/w4; baselines in benchmarks/baseline/scaling/.
Same band (1.5x growth / 2x shrink, slack 10). With the larger point one step up, a growth
rate that steepens by more than ~log2(1.5) ≈ 0.6 in the exponent trips the larger point even if
the smaller one stays in band. Debug cost: the test goes from ~1.7 s to 6.4 s locally.
Not gated: families whose counters are linear (their non-linearity is per-operation cost, which
the band cannot see) and points that cost seconds in debug (arith, rust/enum).
A feature that fixes one of these dimensions will (intentionally) trip the 2x-shrink side and
must refresh those baselines with UPDATE_PERF_BASELINE=1.

Note: UPDATE_PERF_BASELINE=1 with main's code also rewrites three existing flat baselines
(division_precond, precond_cascade, spec_ladder_post: small in-band drifts, e.g.
precond_cascade sat_iterations 41→36); they are left untouched here.

Gates (run on this branch)

• cargo fmt --all --check, cargo clippy --locked --all-targets -- -D warnings: clean.
• cargo test --locked --lib --bins: 358 passed; --test suite: 5 passed; --test perf_regression: passed.
• benchmarks/rust/check.sh: 4464 verified, 0 known-failing, 0 regressed, 0 stale.
• benchmarks/panic_free/check.sh: 55 as expected, 10 incomplete, 0 unsound.
• bench check-suites: 0 errors (4 pre-existing mtime warnings).
• No verifier code changed, so verdicts against main cannot move.

Silicon

Checked 2026-10-07 with silicon_cli.py from the crates repo (memguard, Silicon 1.1-SNAPSHOT
6b540aa4, Z3 4.16.0), one JVM at a time. "main" means release verify built from this branch
(no verifier code differs from main 13091f3). A canary file with a partial-permission write
and a false assert was rejected by Silicon with both errors, so the runs do report failures.
Encodings of the Rust probes: Prusti rewrite-2023 b51f8e0, same as the new families.
Probe sources, encodings, Silicon output: design/rebuild/scaling_baseline/probes/
(silicon_2026-10-07/).

shape	member	main	Silicon	reading
loops_n{1..4}_b{5,20} (8 files, pre-existing family)	m_run	FAIL: exhale m_run#ensures, insufficient permission	FAIL: postcondition of m_run, insufficient permission to p_Param(..)	agree: Prusti's inferred loop invariant does not carry the written-through borrow; not our gap
&T (probe shr.rs: fn get(s: &S), fn deref_int(x: &i32))	p_Ref_immutable_snap	FAIL: p_Param_snap#requires @ 1/1, insufficient permission	verifies (whole file)	main incomplete
branch-selected reborrow (probe cb2.rs)	m_joined, m_joined_no_use_after	FAIL: p_Ref_mutable_snap#requires	FAIL: precondition of p_Ref_mutable_snap, insufficient permission to p_Ref_mutable(_3p, ..)	agree: the encoding loses the joined borrow's permission
same probe	m_branch_local, m_cond_move	verify	verify	agree
conditional moves (probe cm.rs)	m_remove, m_pairs	verify	verify	agree
pc-alias write, permission split over aliases (pa2.vpr)	wr_direct (x == y0 && x == y1 in the precondition, x.f := 1)	FAIL: assign, insufficient permission	verifies	main incomplete
pc-alias read related to an alias (pa2.vpr)	read2 (v := x.f; assert v == y1.f under x == y0 && x == y1)	FAIL: assertion	verifies	main incomplete
pc-alias exhales (pa2.vpr)	exh2, exhfull	verify	verify	agree

No member verifies on main that Silicon rejects.

Why &T fails on main: p_Ref_immutable holds acc(p_Param(addr, U), read()), and the body of
the function p_Ref_immutable_snap calls p_Param_snap, whose precondition asks for write.
Silicon treats permission amounts in function preconditions as wildcards (it warns "Function
contains specific permission amount that will be treated like wildcard"), so any positive
amount suffices; main checks the exact amount inside function bodies. The gap is in main, not
in the encoding, and it hits every program that mentions &T once encoded by this Prusti.

The new families are well-formed: Silicon verifies, with no error, the smallest point of every
new family (condmove_k2, enum_fields_n2, enum_tag_v8, generic_k2, impls_k2, nway_k4,
option_d2, reborrow_n4, seqmatch_k2, straight_k16, struct_w4, tuple_w2, units_k4)
and pcalias_k3, pcalias_k8; main verifies all of them too.

Accounting

From the old branch: the probe shapes of eac77b1 (sw, tw, sb, om, es, se, md) as the starting
point for the new generators (re-derived and regenerated, not copied); the synthetic
members/preds probes (work log 2026-08-20) behind units; the fieldless enum ladder (work log
2026-08-25) behind enum_tag. No old-branch code. The old probe families that measured linear
(bc, cd, fc, gw, ne, sd) are not re-added.