Formal: HANDOFF bookkeeping — #1078 and #1080 merged, no open formal PRs (#1081)

Clears the stale §3b entry (#1078 was left listed as open) and records #1080
under merged. Supersedes the closed #1079.

Author: emeryberger

formal/HANDOFF.md

@@ -119,13 +119,15 @@ Also merged 2026-07-01:
 - **#1076** two-counter bisimulation + per-line attribution +
   `LeakTrackerAudit.lean` + `LeakTrackerConcurrency.lean` (leak-tracker
   concurrency/fork gap) + README "bugs found".
+- **#1078** §4 bugs #3 (unguarded per-stack CPU normalization divide) and #4
+  (CLI-renderer twin of the leak-velocity divide) + two regression tests.
+- **#1080** PASTA (`PoissonArrivals.lean`) + two metrics end-to-end across the
+  C++/Python boundary (`CopyVolumeWiring.lean`, `MallocFootprintWiring.lean`) +
+  `STATUS.md` + README proof roundup + "why two engines" rationale.
 
 ## 3b. OPEN PRs (need driving to merge)
 
-- **#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.
+None — all formal PRs merged as of 2026-07-01.
 
 ---
 
@@ -218,8 +220,9 @@ generated `X | Y` unions need 3.10+).
 
 ## 7. Concrete next steps (roughly ranked)
 
-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.
+1. ~~Merge #1077, #1076, #1078, #1080~~ **DONE** (2026-07-01). All four bug
+   fixes, the concurrency proof, PASTA, and the two end-to-end wiring modules
+   are on master. No formal PRs open.
 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,