Formal: literal two-counter sampler reduction + per-line attribution under sampling (#1076)

* Formal: close two modeling gaps — literal two-counter sampler + per-line attribution under sampling

Follow-up closing the two gaps flagged in the memory-sampler work.

(1) §1b MemorySampler.lean — the one-counter model faithfully reduces the
LITERAL two-counter C++. Previously the 'faithful to thresholdsampler.hpp'
claim rested on collapsing _increments/_decrements into bal = incr - decr in
prose. Now proved: St2 models the literal two-counter machine (separate ℕ
counters, trigger incr ≥ decr+I / decr ≥ incr+I, reset both to 0); step_bisim
/ run_bisim prove it bisimilar to the one-counter model under
abs(incr,decr)=incr-decr; threshold2_conserves transfers exact conservation to
the two-counter machine as written. 'Faithful to the C++' is now a theorem.

(2) §10 PerLineAttribution.lean — ties the byte sampler back to §6's per-line
fraction story. A profiler reports recorded[ℓ]/Σrecorded, a ratio of unbiased
estimators (not exactly unbiased since E[X/Y]≠E[X]/E[Y]). Proved what actually
holds: fraction_of_expectations (the window cancels ⇒ no systematic scale bias
in the breakdown), recorded_fraction_exact (proportional/large-sample limit ⇒
reported fraction = true fraction exactly, rate-independent), and that the
per-line memory breakdown is a probability distribution (sums to 1), like §6.

Full formal/lean build clean (8568 jobs); no sorry; standard axioms only.
README updated (§1b note, new §10, boundary bullet).

* Formal: audit models vs code — leak-tracker safety proof + bugs-found writeup

Adds LeakTrackerAudit.lean: the leak formula 1-(frees+1)/(allocs-frees+2)
(scalene_leak_analysis.py:31) divides with NO guard, relying entirely on the
implicit invariant frees<=allocs — and allocs/frees are incremented at separate
code sites (scalene_memory_profiler.py:236,401), so it's not obvious. We model
the raw two-counter increment discipline (single-shot armed trigger) and PROVE
frees<=allocs (run_frees_le_allocs), hence allocs-frees+2>=2>0
(denom_pos_reachable). The MetricCorrectness leak model had *assumed* this
(unfreed,frees:ℕ with allocs=unfreed+frees), so it could never have caught a
violation; this discharges the assumption against the actual dynamics.

README gains a 'Bugs the formalization found' section documenting the two real
defects the audit surfaced (both fixed in the companion code PR): the
leak-velocity ZeroDivisionError and the atol sampling-window=0 case.

Full formal/lean build clean (8569 jobs); no sorry; standard axioms only.

* Formal: add HANDOFF.md — follow-up notes for the formalization effort

Captures the method (audit hypotheses, don't assume them), what's proven, what's
merged vs open (#1076/#1077), the two bugs found, CI/flake notes, known modeling
gaps, and ranked next steps — so the effort can resume after a context reset.

* Formal: close the leak-tracker concurrency/fork gap

LeakTrackerAudit proved frees <= allocs only for a sequential event
stream. In the code the two increment sites run on a background
sig-queue thread while the shutdown drain runs on the main thread, and
the tracker state is duplicated across fork -- the biggest remaining
'assumed not proven' gap (HANDOFF sec 6/7).

Add LeakTrackerConcurrency.lean, which models the real discipline and,
per the audit method, proves it is *necessary* rather than just present:

- interleave_preserves_inv / sigqueue_then_drain_safe: with each
  process_malloc_free_samples call atomic (the sigqueue RLock), every
  interleaving of the sig-queue thread's steps with the main-thread
  drain preserves frees <= allocs -- scheduler order is irrelevant.
- torn_free_breaks_inv: the lost-disarm race that dropping the lock
  would permit double-credits one armed trigger (frees = allocs + 1),
  so the RLock is load-bearing.
- fork_reset_inv / partial_fork_reset_breaks_inv: the full fork reset
  (clear() zeros leak_score AND last_malloc_triggered together) starts
  the child safe; a partial reset that left the trigger armed breaks
  the invariant -- so resetting both fields together is required.

No sorry; standard axioms only. Full lake build green. Updates README
(new sec 11) and HANDOFF (gap closed).

Author: emeryberger

formal/HANDOFF.md

@@ -0,0 +1,240 @@
+# Formalizing Scalene — handoff / follow-up notes
+
+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.
+
+---
+
+## 0. The point of this effort (don't lose this framing)
+
+We formalize Scalene's guarantees in Lean 4 (+ TLA+ for interleavings) for two
+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).
+2. **Establish correctness** of the properties a profiler's *user* relies on.
+
+**THE METHODOLOGICAL LESSON (most important thing in this doc):** a proof whose
+hypotheses mirror the code's *implicit* assumptions validates the **model**, not
+the **code**. Early models did exactly this and were therefore blind to real
+bugs. Example: the leak model used `unfreed, frees : ℕ` with
+`allocs = unfreed + frees`, which *hardcodes* `frees ≤ allocs` — so it could
+never have caught the unguarded divide-by-zero that assumption protects against.
+
+**Rule going forward:** treat every modeling hypothesis (`0 < total`,
+`frees ≤ allocs`, `interval > 0`, `pythonTime + cTime = total`, every
+denominator) as a *claim to verify against the implementation*. If the code
+doesn't enforce it → that's a finding, not something to assume away. Audit
+models adversarially, don't just prove them.
+
+---
+
+## 1. Where the artifacts live
+
+```
+formal/
+  README.md              # full writeup: §1–§10, source mappings, boundaries, repro
+  HANDOFF.md             # this file
+  tla/                   # TLA+ specs (model-checked with TLC)
+    SignalSafety.tla + _Fix.cfg / _Bug.cfg
+    Deadlock.tla + .cfg
+  lean/                  # Lean 4 project (lake); Mathlib dep; toolchain v4.31.0
+    Scalene.lean         # top-level: imports all modules below
+    Scalene/*.lean       # see §2
+  extract/
+    ScaleneExtract.lean          # extraction-friendly defs (built under LeanToPython, Lean 4.12)
+    scalene_verified_core.py     # GENERATED Python oracle (committed)
+tests/
+  test_verified_space_saving.py       # differential test: prod vs verified oracle
+  test_leak_velocity_zero_elapsed.py  # regression for bug #1 (§4)
+```
+
+**Build:** `cd formal/lean && lake exe cache get && lake build` (needs
+`~/.elan/bin` on PATH; Mathlib cache ~7GB, gitignored).
+**TLC:** Java + `tla2tools.jar`. Ran on the `cloudnew` box (has Java 21);
+`java -cp tla2tools.jar tlc2.TLC -config X.cfg X.tla`.
+**All Lean proofs: no `sorry`; depend only on `propext, Classical.choice,
+Quot.sound`** (verify with `#print axioms <thm>`).
+
+`cloudnew` = a Linux dev box (192 cores) reachable via `ssh cloudnew`. Used for:
+TLC model-checking (Java there), building the C++ native ext, and reproducing
+free-threaded (3.13t/3.14t) behavior. Has `~/scalene-debug` checkout + uv venvs
+`.venv-313t` / `.venv-314t`, and `~/tla/tla2tools.jar`. LeanToPython checkout is
+at `/tmp/LeanToPython` locally (Lean 4.12).
+
+---
+
+## 2. What's proven (Lean modules) — each maps to real code in README
+
+| Module | Property | Key theorems |
+|---|---|---|
+| `Attribution.lean` | CPU/mem bookkeeping conserved; fractions in [0,1] | `totalTime_eq_split`, `cpu_distribution_conserved`, `pythonFraction_le_one`, `footprint_conserved` |
+| `SignalSafety.lean` | `list(...)` snapshot decouples output-iteration from concurrent inserts | `snapshot_stable`, `snapshot_sound` (no axioms) |
+| `SpaceSaving.lean` | `combined_stacks` table never exceeds capacity; evicts min | `step_withinCap`, `fold_withinCap`, `minCount_le` |
+| `ProfilerCorrectness.lean` | **headline**: reported per-line profile is unbiased + consistent | `estimator_unbiased`, `jointVariance_eq` (=p(1−p)/N), `jointExpect_pair` |
+| `ExponentialSampler.lean` | sampler is Poisson ⇒ discharges the i.i.d. hypothesis | `sample_le_iff` (inverse-CDF), `survival_memoryless` |
+| `MetricCorrectness.lean` | GPU/copy/python-split (weighted-avg) + leak detection (Bayesian test) | `gpuFraction_bounds`, `python_c_fraction_sums_one`, `leakScore_*`, `reportsLeak_iff`, `no_leak_without_evidence` |
+| `MemorySampler.lean` | threshold sampler conserves net exactly; Poisson unbiased; **two-counter bisimulation** | `threshold_conserves`, `threshold_residual_bounded`, `threshold2_conserves`, `step_bisim`, `poisson_unbiased` |
+| `PerLineAttribution.lean` | per-line byte fraction faithful under sampling | `fraction_of_expectations`, `recorded_fraction_exact` |
+| `LeakTrackerAudit.lean` | proves the leak formula's *unguarded* denominator is safe (`frees ≤ allocs`) | `run_frees_le_allocs`, `denom_pos_reachable` |
+| `LeakTrackerConcurrency.lean` | `frees ≤ allocs` survives sig-queue/main-thread interleaving + fork; RLock atomicity & joint fork-reset shown *necessary* | `interleave_preserves_inv`, `torn_free_breaks_inv`, `fork_reset_inv`, `partial_fork_reset_breaks_inv` |
+| TLA+ `SignalSafety` | the combined_stacks race is reachable (bug cfg) / impossible (fix cfg) | 4-state counterexample; 99 states clean |
+| TLA+ `Deadlock` | no deadlock; handler never blocks on a lock; output liveness | 72 states clean |
+
+The "profiler correctness" chain: **faithful per-sample attribution ⇒ unbiased,
+consistent reported profile**. Faithfulness is delivered by (a) the exponential
+sampler (§`ExponentialSampler`, Poisson + PASTA), (b) synchronous C++ stamping
+(`whereInPython`, `pywhere.cpp` — engineering, not yet Lean-proven), and (c) the
+conservation invariants (`Attribution`).
+
+---
+
+## 3. Merged to master (all green)
+
+Formal + the CI/bug work that unblocked it:
+- **#1068** formal models (TLA+ + Lean core)
+- **#1070** SpaceSaving capacity proof + proof→production extraction pipeline
+- **#1072** profiler-correctness desideratum (unbiased + consistent)
+- **#1073** regenerate oracle w/ upstream-fixed LeanToPython (dropped `min2`)
+- **#1075** Poisson sampler + GPU/copy/python-split/leak + memory-sampler
+- Enabling fixes: **#1066** (test `sys.executable` leak — the original
+  root-cause), **#1067** (combined_stacks race), **#1069/#1071/#1074** (CI
+  timing flakes), **#1065** (`_scalene_unwind` GIL declaration).
+- **emeryberger/LeanToPython#1** (MERGED): fixed two transpiler bugs
+  (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)
+
+- **#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).
+
+Merge order suggestion: #1077 first (it's the real fix), then #1076.
+
+---
+
+## 4. Bugs the formalization found (BOTH FIXED in #1077)
+
+1. **ZeroDivisionError, leak velocity.** `scalene_json.py` ~line 1255:
+   `"velocity_mb_s": leak_velocity / stats.elapsed_time` was unguarded.
+   `compute_leaks` (`scalene_leak_analysis.py`) 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) → crash. Sibling `elapsed_time` divides
+   (~637, ~1186) were already guarded. Fixed + regression test.
+2. **Sampling window = 0 from bad env var.** `sampleheap.hpp`:
+   `atol(getenv("SCALENE_ALLOCATION_SAMPLING_WINDOW"))` returns 0 for `"0"` /
+   unparseable → ThresholdSampler triggers on *every* alloc (`incr >= decr+0`),
+   catastrophic overhead. Violates `interval > 0` (proved necessary in
+   `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
+`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
+*proves* it from the single-shot armed-trigger discipline.
+
+---
+
+## 5. CI notes (so flakes don't waste a session)
+
+Matrix uses `fail-fast: true`, so one red job cancels the rest. Four wall-clock/
+signal timing flakes were hardened at the source (#1069/#1071/#1074) — parity
+contention-ratio (now non-gating), HyperLogLog hash-seed (now deterministic ints),
+`test_mac_sampler` (poll-not-sleep), `test_off_then_on_via_signal` (placeholder
+SIGILL handler + retry). Remaining transient: `vendor/libunwind` download can
+500. **When a formal-only PR shows red: check whether the failing step is
+`Build scalene` (transient download) or a known flake test — if so, just re-run
+`gh run rerun <id> --failed`.** `ubuntu-latest, 3.13t` runs ~40 min (compiles
+deps from source; no cp313t wheels) — near the 45-min cap but passes.
+
+Oracle test (`test_verified_space_saving.py`) skips on Python < 3.10 (the
+generated `X | Y` unions need 3.10+).
+
+---
+
+## 6. Known modeling gaps / caveats (be honest about these)
+
+- **Faithful sampling is assumed, not proven.** §ProfilerCorrectness proves
+  "faithful sampling ⇒ correct profile". It does NOT prove the C++ stamping
+  *establishes* faithful sampling (needs modeling signal delivery + CPython
+  loop). Discharged by engineering + §Attribution, not Lean.
+- **PASTA is cited, not formalized** (needs continuous-time stochastic-process
+  dev). It's the step connecting Poisson sampling to the `trueFraction`
+  distribution.
+- **`LeakTrackerAudit` models the increment *discipline*, not the literal
+  code.** It assumes single-shot arm/disarm. The sig-queue/main-thread
+  interleaving and `fork` gap that was flagged here is now **closed** by
+  `LeakTrackerConcurrency.lean` (§2, §11 in README): interleaving safety under
+  the RLock, plus proofs that RLock atomicity and joint fork-reset are
+  *necessary* (`torn_free_breaks_inv`, `partial_fork_reset_breaks_inv`). What
+  remains assumed: that each `process_malloc_free_samples` call really is atomic
+  w.r.t. the others (the RLock + join discipline the code implements) — the
+  model takes step-atomicity as given rather than deriving it from the queue's
+  operational semantics.
+- **Python/native split**: only the *conservation* (fractions sum to 1) is
+  proven, NOT the per-sample *accuracy* of the CALL-opcode/signal-deferral
+  classifier heuristic.
+- **The extraction oracle is a differential guard, not a drop-in.** Production
+  still has its own `_space_saving_increment`; the test checks they agree.
+- **C++→Python wiring** (native counters → `ScaleneStatistics`) is not modeled.
+- TLC results are bounded (`Keys={k1,k2,k3}`, `N=3`, `MaxHandler=2`) — exhaustive
+  within bounds, not a general proof.
+
+---
+
+## 7. Concrete next steps (roughly ranked)
+
+1. **Merge #1077 then #1076** (drive CI; re-run 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,
+   and proves the RLock atomicity + joint fork-reset are *necessary*. Residual:
+   step-atomicity is taken as a modeling axiom (justified by the RLock + thread
+   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.
+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
+   document precisely why it's a heuristic with bounded error.
+6. **Wire the verified oracle into production directly** (have
+   `_space_saving_increment` call the extracted core) rather than only
+   differential-testing it — closes the proof→production loop tighter.
+7. **Model one more column end-to-end** (e.g. GPU or copy-volume) under the
+   unbiased-estimator frame, including the C++→Python wiring.
+
+---
+
+## 8. Repro cheatsheet
+
+```bash
+# Lean (local)
+cd formal/lean && lake exe cache get && lake build          # 0 sorry
+echo 'import Scalene
+#print axioms Scalene.ProfilerCorrectness.Truth.estimator_unbiased' > /tmp/a.lean
+lake env lean /tmp/a.lean                                    # standard axioms only
+
+# TLA+ (on cloudnew, has Java)
+scp formal/tla/* cloudnew:~/tla/scalene/
+ssh cloudnew 'cd ~/tla/scalene && java -cp ~/tla/tla2tools.jar tlc2.TLC \
+  -config SignalSafety_Fix.cfg SignalSafety.tla'            # no error, 99 states
+
+# Regenerate the extracted oracle (needs /tmp/LeanToPython, Lean 4.12)
+cp formal/extract/ScaleneExtract.lean /tmp/LeanToPython/
+cd /tmp/LeanToPython && lake env lean ScaleneExtract.lean > scalene_verified_core.py
+
+# The bug-finding regression test
+python3 -m pytest tests/test_leak_velocity_zero_elapsed.py -q
+```