scry has no analysis budget, timeout, step limit, or fuel. Grepped: the only bound in scry-analyze-core is widening_threshold (max fixpoint iterations per loop header, default 3), which bounds loop convergence — not total work. Nothing bounds a whole-module analysis.
The measurement we already have and haven't tracked
From @avrabe's corpus run in #126, on 468 real-world core modules:
analysed (ok): 281
analyzer error: 82
crash: 2 (fixed in v3.2.5)
timed out at 60s: 103 ← 22.0%
That was explicitly caveated as "timing only, shared machine — not a defect claim", which is fair as a benchmark statement. But it is the only datapoint we have on scry's scaling behaviour, and 22% is not a footnote. It has no issue, so it has never been treated as anything.
Why a timeout is worse than a gap
scry's whole posture is that giving up must be visible: GapKind has four variants — UnsupportedOp, UnmodeledBranch, UnmodeledMemoryAddress, UnmodeledControlFlow — each meaning "we degraded to ⊤ here, soundly, and said so." REQ-017 is "no silent ⊤".
An analysis that runs past the caller's patience satisfies none of that. It returns nothing — not a partial result, not a gap, not an error. It is the same failure as the #125 panic one level up: the consumer gets neither arm of the result, and cannot distinguish "scry is still working" from "scry will never finish."
A sound analyzer that does not terminate is strictly worse than one that degrades to ⊤ and tells you where.
Independent corroboration that this is a wall, not a tuning problem
Chris Fallin (F5) gave a Wasm Research Day talk on AOT-compiling JavaScript to Wasm. Before landing on his shipped design he built Sparta, a sound whole-program points-to + abstract-interpretation analysis — deliberately already dropping flow-sensitivity and call-site-sensitivity for scale.
His numbers:
- On Richards (~300 LOC) it worked, and worked well — 17,000 vs the native JIT's 28,000.
- On the next file he tried, 350k LOC, it OOM'd on a 128 GB workstation.
His conclusion, in his own words: "we're not going to be able to make a sound thing work… That's a research problem. Many people have tried. I had to try myself to convince myself because I'm stubborn." He pivoted to optimistic types plus dynamic guards, which compiles that same 350k LOC in 5 seconds.
Different domain, different language, same shape: sound whole-program analysis has a cliff, and it is nearer than it looks. Ours shows up as a 22% timeout rate rather than an OOM, but a 60-second wall and a 128 GB wall are the same wall.
This is not an argument to abandon soundness — soundness is scry's entire product and the guard escape hatch is not available to us in the same way. It is an argument that the cliff is real, that we are already on it, and that we currently fall off it silently.
Proposed shape, in scry's own idiom
Add an analysis budget, and make exhausting it a first-class sound degradation rather than a hang:
AnalysisConfig grows a budget (step count preferred over wall-clock — deterministic, and reproducible across machines, which a shared-runner timing number is not).- On exhaustion, the affected function's state degrades to ⊤ and a
Gap { kind: BudgetExhausted, .. } is recorded, naming the function and what was abandoned.
analyze() still returns ok(...) — a partial result with honest gaps beats no result. The existing "no silent ⊤" machinery carries it.- The budget is reported in the result, so a consumer can tell "scry proved little here" from "scry was not given enough room."
That turns an unbounded hang into the thing scry is already good at: saying precisely where it stopped knowing things.
What would make this measurable
AnalysisConfig is already threaded through the corpus harness, so a budget sweep would answer the question this issue can't: of the 103, how many finish at 10× the budget, and how many are genuinely unbounded? That separates "slow" from "divergent", and only the second is a design problem.
Related: #126 (the corpus run), #125 (the same "consumer gets neither arm" failure, as a panic), REQ-017.
scry has no analysis budget, timeout, step limit, or fuel. Grepped: the only bound in
scry-analyze-coreiswidening_threshold(max fixpoint iterations per loop header, default 3), which bounds loop convergence — not total work. Nothing bounds a whole-module analysis.The measurement we already have and haven't tracked
From @avrabe's corpus run in #126, on 468 real-world core modules:
That was explicitly caveated as "timing only, shared machine — not a defect claim", which is fair as a benchmark statement. But it is the only datapoint we have on scry's scaling behaviour, and 22% is not a footnote. It has no issue, so it has never been treated as anything.
Why a timeout is worse than a gap
scry's whole posture is that giving up must be visible:
GapKindhas four variants —UnsupportedOp,UnmodeledBranch,UnmodeledMemoryAddress,UnmodeledControlFlow— each meaning "we degraded to ⊤ here, soundly, and said so." REQ-017 is "no silent ⊤".An analysis that runs past the caller's patience satisfies none of that. It returns nothing — not a partial result, not a gap, not an error. It is the same failure as the #125 panic one level up: the consumer gets neither arm of the result, and cannot distinguish "scry is still working" from "scry will never finish."
A sound analyzer that does not terminate is strictly worse than one that degrades to ⊤ and tells you where.
Independent corroboration that this is a wall, not a tuning problem
Chris Fallin (F5) gave a Wasm Research Day talk on AOT-compiling JavaScript to Wasm. Before landing on his shipped design he built Sparta, a sound whole-program points-to + abstract-interpretation analysis — deliberately already dropping flow-sensitivity and call-site-sensitivity for scale.
His numbers:
His conclusion, in his own words: "we're not going to be able to make a sound thing work… That's a research problem. Many people have tried. I had to try myself to convince myself because I'm stubborn." He pivoted to optimistic types plus dynamic guards, which compiles that same 350k LOC in 5 seconds.
Different domain, different language, same shape: sound whole-program analysis has a cliff, and it is nearer than it looks. Ours shows up as a 22% timeout rate rather than an OOM, but a 60-second wall and a 128 GB wall are the same wall.
This is not an argument to abandon soundness — soundness is scry's entire product and the guard escape hatch is not available to us in the same way. It is an argument that the cliff is real, that we are already on it, and that we currently fall off it silently.
Proposed shape, in scry's own idiom
Add an analysis budget, and make exhausting it a first-class sound degradation rather than a hang:
AnalysisConfiggrows a budget (step count preferred over wall-clock — deterministic, and reproducible across machines, which a shared-runner timing number is not).Gap { kind: BudgetExhausted, .. }is recorded, naming the function and what was abandoned.analyze()still returnsok(...)— a partial result with honest gaps beats no result. The existing "no silent ⊤" machinery carries it.That turns an unbounded hang into the thing scry is already good at: saying precisely where it stopped knowing things.
What would make this measurable
AnalysisConfigis already threaded through the corpus harness, so a budget sweep would answer the question this issue can't: of the 103, how many finish at 10× the budget, and how many are genuinely unbounded? That separates "slow" from "divergent", and only the second is a design problem.Related: #126 (the corpus run), #125 (the same "consumer gets neither arm" failure, as a panic), REQ-017.