2.3. The timed interval has a precise boundary🔗

Once reservation is complete, the profiler samples IO.monoNanosNow and IO.getNumHeartbeats, runs the action, and samples both again. The resulting event stores elapsed monotonic host time and the difference in Lean heartbeats.

These measurements answer different questions. Host time includes waiting, scheduling, operating system work, and synchronous foreign calls. Lean heartbeats are a runtime work counter associated with the current Lean thread. They are not CPU cycles, allocation bytes, or a device timer. A phase whose host time rises while its heartbeat count stays nearly fixed is often waiting or doing work outside ordinary Lean execution; a phase whose two measurements rise together is more likely doing additional Lean-side work.

The action is protected by try/finally. Its event is completed and the thread stack is restored even when it throws. The original exception then continues to the caller. This matters in practice: a partial trace from a failed run is often the clearest record of where the failure occurred.