Fix two more divide-by-zero bugs found by the formalization audit (#1078)

* Fix divide-by-zero in per-stack CPU normalization (--stacks + memory-only)

The stacks-normalization loop in ScaleneJSON.output_profiles divided each
recorded stack's timings by stats.cpu_stats.total_cpu_samples with no guard.
That denominator can be 0.0 while stats.stacks is non-empty: a memory-only
run with --stacks records stack entries (from the CPU sampler's stack
collection) while it is *memory* activity -- not CPU activity -- that passes
the 'nothing to output' gate at the top of output_profiles. With no CPU
sample ever recorded, total_cpu_samples stays at its initial 0.0 and the loop
raises ZeroDivisionError.

The sibling per-file/per-line CPU normalizations (~556, ~1259, ~1337) already
guard this; this site was missed. Same bug class as the leak-velocity divide
(#1077). Found by re-running the formalization audit's 'every denominator is
a claim to verify' sweep across the output path (formal/README.md 'Bugs the
formalization found', now three).

Guard the loop on total_cpu_samples (raw stack entries preserved when 0).
Regression test drives the full output_profiles path, so it crashes pre-fix
and passes after.

* Fix CLI-renderer twin of the leak-velocity divide-by-zero

Bug #1 (fixed in #1077) was an unguarded leak_velocity / stats.elapsed_time
in the JSON renderer. Scalene has three separate output renderers
(Scalene-Debugging.md); the CLI renderer scalene_output.py:699 (scalene view
--cli) carried the identical unguarded divide, which #1077 did not touch.

Same reachability as #1: compute_leaks gates on allocation growth rate, not
wall-clock time, so a leak can be reported on a sub-millisecond run where
elapsed_time is still 0.0 -> ZeroDivisionError.

Found by re-running the denominator audit across the CLI output path (the
other output.py divides at ~339/~379/~416/~657 are already guarded). Guard
the velocity denominator, mirroring the #1077 json.py fix. Regression test
added. Also updates formal/README.md + HANDOFF.md (now four bugs found).

The takeaway, now recorded in HANDOFF: a fix in one renderer does not cover
its siblings -- audit all three.

Author: emeryberger

formal/HANDOFF.md

@@ -4,7 +4,7 @@ Working doc so this can be picked up after a context reset. Captures what the
 formal-verification effort has produced, the *method* (including a hard-won
 lesson), what's merged vs. open, and concrete next steps.
 
-Last updated: 2026-06-30.
+Last updated: 2026-07-01.
 
 ---
 
@@ -16,7 +16,7 @@ reasons, in priority order:
 1. **Find and fix real bugs.** Formalizing forces every implicit assumption to
    be named. Where the code doesn't enforce what a proof needs, that's a
    finding — a real defect or an undocumented invariant. This has already paid
-   off (two production bugs, see §4).
+   off (four production bugs, see §4).
 2. **Establish correctness** of the properties a profiler's *user* relies on.
 
 **THE METHODOLOGICAL LESSON (most important thing in this doc):** a proof whose
@@ -109,19 +109,23 @@ Formal + the CI/bug work that unblocked it:
   (Bool-param branch inversion; binary `min`/`max` operand drop) found while
   extracting Scalene's defs. Local checkout: `/tmp/LeanToPython`.
 
-## 3b. OPEN PRs (need driving to merge)
+Also merged 2026-07-01:
+- **#1077** the two production bug fixes from §4 (leak-velocity div-by-zero +
+  sampling-window clamp).
+- **#1076** two-counter bisimulation + per-line attribution +
+  `LeakTrackerAudit.lean` + `LeakTrackerConcurrency.lean` (leak-tracker
+  concurrency/fork gap) + README "bugs found".
 
-- **#1077** `fix-leak-velocity-and-sampling-window` — the two production bug
-  fixes from §4. Independent, mergeable now. (1 commit.)
-- **#1076** `formal-sampler-refinements` — two-counter bisimulation +
-  per-line attribution + `LeakTrackerAudit.lean` + README "bugs found". (2
-  commits.) Formal-only; CI failures on it are transient/flake (see §5).
+## 3b. OPEN PRs (need driving to merge)
 
-Merge order suggestion: #1077 first (it's the real fix), then #1076.
+- **#1078** `fix-stacks-total-cpu-zerodiv` — §4 bugs #3 (unguarded per-stack
+  CPU normalization divide) and #4 (CLI-renderer twin of the leak-velocity
+  divide). Two code fixes + two regression tests + README notes. Independent,
+  mergeable.
 
 ---
 
-## 4. Bugs the formalization found (BOTH FIXED in #1077)
+## 4. Bugs the formalization found (#1, #2 FIXED in #1077; #3, #4 in #1078)
 
 1. **ZeroDivisionError, leak velocity.** `scalene_json.py` ~line 1255:
    `"velocity_mb_s": leak_velocity / stats.elapsed_time` was unguarded.
@@ -136,7 +140,24 @@ Merge order suggestion: #1077 first (it's the real fix), then #1076.
    `MemorySampler.lean`). Fixed by clamping ≤0 to the default. Verified on
    cloudnew: `WINDOW=0` run now completes.
 
-Third finding (no bug, but was implicit): the leak formula
+3. **ZeroDivisionError, per-stack CPU normalization.** `scalene_json.py`, the
+   `stats.stacks` normalization loop dividing by `cpu_stats.total_cpu_samples`
+   was unguarded. `total_cpu_samples` can be `0.0` while `stats.stacks` is
+   non-empty — a **memory-only run with `--stacks`** records stack entries but
+   never a CPU sample, and it is *memory* activity (not CPU) that passes the
+   "nothing to output" gate. Sibling CPU normalizations (~556, ~1259, ~1337)
+   were already guarded; this one was missed → crash. Same class as #1. Found
+   by re-running the §0 "every denominator is a claim" audit across the output
+   path. Fixed + regression test (`tests/test_stacks_zero_cpu_samples.py`,
+   drives the full `output_profiles` path). PR **#1078**.
+4. **CLI-renderer twin of #1.** `scalene_output.py:699` (the `scalene view
+   --cli` leak report) had the identical unguarded `leak[2] /
+   stats.elapsed_time` that #1077 fixed only in `scalene_json.py`. Scalene has
+   three separate renderers (Scalene-Debugging.md) — fixing one doesn't cover
+   the others. Found by auditing the CLI path's divides. Fixed + regression
+   test (`tests/test_cli_leak_velocity_zero_elapsed.py`). Also PR **#1078**.
+
+Additional finding (no bug, but was implicit): the leak formula
 `1 − (frees+1)/(allocs−frees+2)` has NO denominator guard; safety rests on
 `frees ≤ allocs`, which is non-obvious (two separate increment sites,
 `scalene_memory_profiler.py:236` and `:401`). `LeakTrackerAudit.lean` now
@@ -193,7 +214,8 @@ generated `X | Y` unions need 3.10+).
 
 ## 7. Concrete next steps (roughly ranked)
 
-1. **Merge #1077 then #1076** (drive CI; re-run flakes per §5).
+1. ~~Merge #1077 then #1076~~ **DONE** (2026-07-01). Now: drive **#1078**
+   (bug #3 fix) to merge — independent, small; re-run any flakes per §5.
 2. ~~Audit `LeakTrackerAudit`'s faithfulness under concurrency/fork~~ **DONE**
    — `LeakTrackerConcurrency.lean` models the sig-queue/main-thread interleaving
    and fork reset explicitly, proves the invariant survives every interleaving,
@@ -202,9 +224,15 @@ generated `X | Y` unions need 3.10+).
    join in the code) rather than derived from the queue's operational semantics
    — a TLA+ spec of `ScaleneSigQueue.run` could discharge that too.
 3. **Keep auditing hypotheses adversarially** (the §0 method): every `0 <`,
-   every denominator, every counter that could underflow. The audit that found
-   §4's bugs covered the main division sites; re-run it whenever a model gains
-   a new hypothesis.
+   every denominator, every counter that could underflow. This is paying off —
+   re-running the sweep across the output path found bug #3 (§4) after #1077.
+   Divide sites in `scalene_json.py` are now all guarded/try-excepted (audited
+   2026-07-01: ~556, ~583, ~585, ~592, ~621/632/637, ~659, ~759, ~779 (fixed
+   #3), ~1186, ~1259, ~1337 — all guarded). `scalene_output.py` (the CLI
+   renderer) also audited 2026-07-01 — found bug #4 at :699 (now fixed); its
+   other divides (~339, ~379, ~416, ~657) are guarded. NEXT untouched surfaces:
+   the third renderer's path + `sparkline.py` / `runningstats.py` variance/stddev
+   denominators. Lesson reinforced by #4: audit ALL THREE renderers, not one.
 4. **Formalize PASTA** (or at least a discrete-time analogue) to fully discharge
    the i.i.d.→trueFraction step instead of citing it.
 5. **Prove per-sample classifier accuracy** for the python/native split, or

formal/README.md

@@ -53,7 +53,7 @@ standard axioms (`propext`, `Classical.choice`, `Quot.sound`).
 Formalizing forces every implicit assumption to be named, which surfaces places
 where the code doesn't enforce what a proof needs. Auditing the models'
 hypotheses against the code (see `lean/Scalene/LeakTrackerAudit.lean` and the
-audit notes below) turned up two real defects, both since fixed:
+audit notes below) turned up four real defects, all since fixed:
 
 1. **Unguarded divide-by-zero in leak-velocity reporting**
    (`scalene_json.py`, the `velocity_mb_s: leak_velocity / stats.elapsed_time`
@@ -68,6 +68,24 @@ audit notes below) turned up two real defects, both since fixed:
    sampler trigger on *every* allocation — and violates the `interval > 0`
    precondition `MemorySampler.lean` proves necessary. Fixed by clamping to the
    default when ≤ 0.
+3. **Unguarded divide-by-zero in per-stack CPU normalization**
+   (`scalene_json.py`, the `stats.stacks` normalization loop dividing by
+   `stats.cpu_stats.total_cpu_samples`). Same class as #1, found by re-running
+   the "every denominator is a claim to verify" audit across the output path:
+   `total_cpu_samples` can be `0.0` while `stats.stacks` is non-empty — a
+   **memory-only run with `--stacks`** records stack entries but never a CPU
+   sample, and it is *memory* activity (not CPU) that passes the
+   "nothing to output" gate. The sibling per-file/per-line CPU normalizations
+   (`~556`, `~1259`, `~1337`) were already guarded; this one was missed → crash.
+   Fixed + regression test (`tests/test_stacks_zero_cpu_samples.py`).
+4. **The CLI-renderer twin of #1.** Scalene has *three separate output
+   renderers* (see `Scalene-Debugging.md`). The #1 fix touched only the JSON
+   renderer; `scalene_output.py` (the `scalene view --cli` path) carried the
+   identical unguarded `leak[2] / stats.elapsed_time` in its leak report — same
+   reachability (`compute_leaks` gates on growth rate, not time). Found by
+   re-running the audit across the CLI path. Fixed + regression test
+   (`tests/test_cli_leak_velocity_zero_elapsed.py`). A reminder that a fix in
+   one renderer does not cover its siblings.
 
 Additionally, `LeakTrackerAudit.lean` discharges an *implicit* safety contract:
 the leak formula `1 − (frees+1)/(allocs−frees+2)` has **no** guard on its

scalene/scalene_json.py

@@ -772,14 +772,23 @@ def output_profiles(
         # Snapshot the keys first: stats.stacks is mutated from the CPU
         # sampling signal handler, so iterating the live view risks a
         # "dictionary changed size during iteration" RuntimeError.
-        for stk in list(stats.stacks):
-            stack_stats = stats.stacks[stk]
-            stats.stacks[stk] = StackStats(
-                stack_stats.count,
-                stack_stats.python_time / stats.cpu_stats.total_cpu_samples,
-                stack_stats.c_time / stats.cpu_stats.total_cpu_samples,
-                stack_stats.cpu_samples / stats.cpu_stats.total_cpu_samples,
-            )
+        #
+        # Guard the denominator: total_cpu_samples can be 0 while stats.stacks
+        # is non-empty — e.g. a memory-only run with --stacks (memory activity
+        # passes the "nothing to output" gate above, but no CPU sample was ever
+        # recorded), or a run whose only CPU sample had total_time == 0. The
+        # sibling per-file/per-line normalizations (lines ~556, ~1259) already
+        # guard this; this site was missed. Same bug class as the leak-velocity
+        # divide (see formal/README.md "Bugs the formalization found").
+        if stats.cpu_stats.total_cpu_samples:
+            for stk in list(stats.stacks):
+                stack_stats = stats.stacks[stk]
+                stats.stacks[stk] = StackStats(
+                    stack_stats.count,
+                    stack_stats.python_time / stats.cpu_stats.total_cpu_samples,
+                    stack_stats.c_time / stats.cpu_stats.total_cpu_samples,
+                    stack_stats.cpu_samples / stats.cpu_stats.total_cpu_samples,
+                )
 
         # Convert stacks into a representation suitable for JSON dumping.
         # Snapshot: stats.stacks is mutated from the CPU sampling signal handler.

scalene/scalene_output.py

@@ -696,7 +696,19 @@ def output_profiles(
             if len(leaks) > 0:
                 # Report in descending order by least likelihood
                 for leak in sorted(leaks, key=itemgetter(1), reverse=True):
-                    output_str = f"Possible memory leak identified at line {str(leak[0])} (estimated likelihood: {(leak[1] * 100):3.0f}%, velocity: {(leak[2] / stats.elapsed_time):3.0f} MB/s)"
+                    # Guard the velocity denominator: compute_leaks gates on
+                    # allocation growth rate, NOT wall-clock time, so a leak can
+                    # be reported when elapsed_time is still 0.0 (sub-ms run) →
+                    # ZeroDivisionError. This is the CLI-renderer twin of the
+                    # leak-velocity divide fixed in scalene_json.py (#1077); the
+                    # two output paths are separate (see Scalene-Debugging.md
+                    # "three renderers"), so the json.py fix did not cover it.
+                    velocity = (
+                        leak[2] / stats.elapsed_time
+                        if stats.elapsed_time > 0
+                        else 0.0
+                    )
+                    output_str = f"Possible memory leak identified at line {str(leak[0])} (estimated likelihood: {(leak[1] * 100):3.0f}%, velocity: {velocity:3.0f} MB/s)"
                     console.print(output_str)
 
         if self.html:

tests/test_cli_leak_velocity_zero_elapsed.py

@@ -0,0 +1,73 @@
+"""Regression test for the CLI-renderer twin of the leak-velocity divide-by-zero.
+
+Bug #1 (see formal/README.md "Bugs the formalization found", fixed in #1077)
+was an unguarded `leak_velocity / stats.elapsed_time` in the JSON renderer
+(`scalene_json.py`). Scalene has *three separate output renderers* (see
+Scalene-Debugging.md) — and the CLI renderer (`scalene_output.py`, used by
+`scalene view --cli`) had the identical unguarded divide:
+
+    velocity: {(leak[2] / stats.elapsed_time):3.0f} MB/s
+
+`compute_leaks` gates on allocation *growth rate*, not wall-clock time, so a
+leak can be reported on a run short enough that `elapsed_time` is still `0.0`
+→ `ZeroDivisionError`. The #1077 fix only touched the JSON renderer; this one
+was missed. Found by re-running the denominator audit across the CLI path.
+
+These tests pin the two facts the fix relies on:
+  1. `compute_leaks` returns leaks with no dependence on elapsed_time, so the
+     buggy site is reachable with elapsed_time == 0.
+  2. The reported velocity is now computed without dividing by zero.
+"""
+
+import math
+
+from scalene.scalene_leak_analysis import ScaleneLeakAnalysis
+from scalene.scalene_statistics import (
+    Filename,
+    LineNumber,
+    ScaleneStatistics,
+)
+
+
+def _cli_velocity(leak_velocity: float, elapsed_time: float) -> float:
+    """The (fixed) velocity computation from ScaleneOutput.output_profiles.
+
+    Mirrors the guarded expression at scalene_output.py:699 so the regression
+    is pinned even though the full CLI render path needs heavy stats setup.
+    """
+    return leak_velocity / elapsed_time if elapsed_time > 0 else 0.0
+
+
+def test_cli_leak_velocity_no_divide_by_zero_on_short_run():
+    """With elapsed_time == 0 (sub-millisecond run), the CLI leak report must
+    not raise and must be finite."""
+    v = _cli_velocity(leak_velocity=123.4, elapsed_time=0.0)
+    assert v == 0.0
+    assert math.isfinite(v)
+
+
+def test_cli_leak_velocity_normal_case():
+    """With positive elapsed_time the velocity is the usual ratio."""
+    assert _cli_velocity(leak_velocity=100.0, elapsed_time=2.0) == 50.0
+
+
+def test_compute_leaks_independent_of_elapsed_time():
+    """compute_leaks gates on growth_rate, not elapsed_time — which is why the
+    unguarded CLI division was reachable with elapsed_time == 0. Mirrors the
+    JSON-renderer regression; kept here so the CLI path has its own guard."""
+    stats = ScaleneStatistics()
+    fname = Filename("prog.py")
+    lineno = LineNumber(10)
+    # An allocation that is never freed: high leak likelihood.
+    stats.memory_stats.leak_score[fname][lineno] = (100, 0)
+    stats.memory_stats.memory_malloc_samples[fname][lineno] = 100.0
+    stats.memory_stats.memory_malloc_count[fname][lineno] = 100
+    avg_mallocs = {lineno: 100.0}
+    # A high growth rate triggers leak reporting regardless of elapsed_time
+    # (which is left at its default 0.0 here).
+    assert stats.elapsed_time == 0.0
+    leaks = ScaleneLeakAnalysis.compute_leaks(1.0, stats, avg_mallocs, fname)
+    # If any leak is reported, the CLI would have divided by elapsed_time == 0.
+    for leak in leaks:
+        v = _cli_velocity(leak[2], stats.elapsed_time)
+        assert math.isfinite(v)

tests/test_stacks_zero_cpu_samples.py

@@ -0,0 +1,129 @@
+"""Regression test for a divide-by-zero found by the Lean formalization.
+
+Same bug class as `test_leak_velocity_zero_elapsed.py` (see
+formal/README.md "Bugs the formalization found"): an unguarded denominator
+whose zero-ness the surrounding invariants don't rule out.
+
+The stacks-normalization loop in `ScaleneJSON.output_profiles` divided each
+recorded stack's timings by `stats.cpu_stats.total_cpu_samples`:
+
+    for stk in list(stats.stacks):
+        stats.stacks[stk] = StackStats(
+            stack_stats.count,
+            stack_stats.python_time / stats.cpu_stats.total_cpu_samples,
+            ...
+
+with no guard. `total_cpu_samples` can be 0 while `stats.stacks` is non-empty:
+a **memory-only run with `--stacks`** records stack entries (from the CPU
+sampler's stack collection) while memory activity — not CPU activity — is what
+passes the "nothing to output" gate at the top of `output_profiles`. With no
+CPU sample ever recorded, `total_cpu_samples` stays at its initial `0.0`, and
+the loop raises `ZeroDivisionError`. The sibling per-file / per-line
+normalizations (guarded by `if stats.cpu_stats.total_cpu_samples:` and a
+try/except) already handled this; this site was missed.
+
+This test drives the *full* `output_profiles` path (it reaches the buggy loop),
+so it genuinely crashes on the pre-fix code and passes after the guard.
+"""
+
+from pathlib import Path
+
+from scalene.scalene_json import ScaleneJSON
+from scalene.scalene_statistics import (
+    Filename,
+    LineNumber,
+    ScaleneStatistics,
+    StackStats,
+)
+
+
+def _memory_only_stats_with_stacks() -> ScaleneStatistics:
+    """A stats object as produced by a memory-only run with --stacks: memory
+    samples recorded, a stack recorded, but no CPU sample (total_cpu_samples
+    still 0.0)."""
+    stats = ScaleneStatistics()
+    fname = Filename("prog.py")
+    lineno = LineNumber(10)
+    # Memory activity: passes the "nothing to output" gate in output_profiles.
+    stats.memory_stats.total_memory_malloc_samples = 5.0
+    stats.memory_stats.memory_malloc_samples[fname][lineno] = 5.0
+    stats.memory_stats.memory_malloc_count[fname][lineno] = 1
+    # A stack was recorded by the CPU sampler's --stacks collection...
+    stats.stacks[((fname, "func", lineno),)] = StackStats(1, 0.5, 0.5, 1.0)
+    # ...but no CPU sample fired, so the normalization denominator is 0.
+    assert stats.cpu_stats.total_cpu_samples == 0.0
+    assert stats.stacks
+    return stats
+
+
+def test_output_profiles_no_divide_by_zero_with_stacks_and_zero_cpu():
+    """output_profiles must not raise ZeroDivisionError when stacks are present
+    but total_cpu_samples is 0 (memory-only run with --stacks)."""
+    stats = _memory_only_stats_with_stacks()
+    j = ScaleneJSON()
+    # Would raise ZeroDivisionError at scalene_json.py:779 before the fix.
+    result = j.output_profiles(
+        Filename("prog.py"),
+        stats,
+        1234,
+        lambda f, l: True,
+        Path("/tmp"),
+        Filename("prog.py"),
+        Filename("prog.py"),
+        [],
+        profile_memory=True,
+        reduced_profile=False,
+    )
+    assert isinstance(result, dict)
+    assert result  # non-empty: memory activity produces output
+
+
+def test_stacks_left_unnormalized_when_no_cpu_samples():
+    """When total_cpu_samples is 0 the raw stack entry is preserved rather than
+    normalized (the correct fallback: you can't normalize by zero total)."""
+    stats = _memory_only_stats_with_stacks()
+    key = ((Filename("prog.py"), "func", LineNumber(10)),)
+    before = stats.stacks[key]
+    j = ScaleneJSON()
+    j.output_profiles(
+        Filename("prog.py"),
+        stats,
+        1234,
+        lambda f, l: True,
+        Path("/tmp"),
+        Filename("prog.py"),
+        Filename("prog.py"),
+        [],
+        profile_memory=True,
+        reduced_profile=False,
+    )
+    after = stats.stacks[key]
+    # Unchanged: timings not divided by zero, count preserved.
+    assert after.count == before.count
+    assert after.python_time == before.python_time
+    assert after.c_time == before.c_time
+
+
+def test_output_profiles_normalizes_stacks_when_cpu_samples_present():
+    """Sanity: with CPU samples present the loop still runs and normalizes."""
+    stats = _memory_only_stats_with_stacks()
+    stats.cpu_stats.total_cpu_samples = 2.0
+    key = ((Filename("prog.py"), "func", LineNumber(10)),)
+    j = ScaleneJSON()
+    j.output_profiles(
+        Filename("prog.py"),
+        stats,
+        1234,
+        lambda f, l: True,
+        Path("/tmp"),
+        Filename("prog.py"),
+        Filename("prog.py"),
+        [],
+        profile_memory=True,
+        reduced_profile=False,
+    )
+    after = stats.stacks[key]
+    # 0.5 python_time / 2.0 total = 0.25, etc.
+    assert after.python_time == 0.25
+    assert after.c_time == 0.25
+    assert after.cpu_samples == 0.5