Performance

4 measured workloads · Node.js · Apple M4 Pro

Typical processing

1.71 µs

Busier blocks

1.83 µs

Share of the test budget

0.1%

250.5 ms · feedback 0.7 · drive 3 · 96 kHz · 1.333 ms available per block in this test.

Processing cost

Processing time in µs · lower means less work

Select a point to inspect its measurements. Hollow points indicate variable timing. Lines guide the eye; only marked cases were measured.
Retained DSP buffers
93.9 KiB
Impulse first arrival
250.50 ms
Peak output
-13.98 dBFS

Captured energy decay

Remaining energy · dB

Stereo-summed backward squared-energy integration, sampled every 20 ms, normalized to the captured 2 s impulse response. Finite-window curve; no extrapolated RT60 claim.
Measurement details
Retained DSP buffers · 93.9 KiB
Unique backing-buffer capacity reachable from prepared DSP state, including borrowed rings and retained scratch. Excludes JS objects, scalar fields, harness buffers and transient allocation; zero does not mean zero total memory.
Peak output · -13.98 dBFS
Last 4096 frames of a 0.5 s steady render. Effects receive a 0.2-peak 1 kHz sine; sources generate their declared waveform. No automatic musical-quality verdict.
DC offset · 0.00110
Signed mean over the same steady-render channels and final 4096 frames.
Output RMS · -17.00 dBFS
RMS over all channels of the same steady-render window.
Impulse first arrival · 250.50 ms
First channel sample at or above -120 dBFS after a 0.2 impulse, following 250 ms + 127 frames of silence; 2 s observation. Includes configured delay, phase and any dry path. Not device latency or group delay. No detection is unavailable, not zero.
Energy after 1 second · -10.47 dB
Energy in the second second relative to the captured 2 s response. A long decay may extend beyond the capture.
All measured cases
Sample rate · kHzWorkloadTypical · µsBusier blocks · µsTest budget usedObservations
481.711.790.1%—
481.711.830.1%—
961.751.920.1%Timing varies
961.711.830.1%—

Times are per 128-frame audio block. Test budget used divides the p95 time by the block period at that case’s sample rate. Machine and runtime are shared.

Test setup

Node.js · Apple M4 Pro · 48 / 96 kHz · 128 frames per block · 3 repeated tests ·

Typical summarizes the middle measured block times. Busier blocks summarizes the time that 95% of blocks completed within in each repeat. These figures measure DSP processing; application scheduling, loading samples and device output require separate checks. Memory and signal probes run separately from the timing loop.

Lean 4 proofs and optimization limits

Lean 4 checks algorithm properties and candidate optimization rewrites within stated assumptions. A model proof does not establish that an optimization is enabled in this node or on any target. Performance measurements establish speed.

2 Lean 4 results: 1 proof in exact arithmetic; 1 counterexample.

Proved in exact arithmetic.The real rationalTanh, generated from Maru compiler IR, stays within plus or minus 1 for every input.
Domain
exact rational arithmetic
Limits and assumptions
  • False on Float: NaN passes straight through, and an ordinary finite input just below 3 gives 1.0000000000000002.
Theorem
IrToLean.Proof.rationalTanh_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.On Float the real rationalTanh is not bounded by 1: NaN gives NaN, and an input just below 3 gives one unit in the last place over 1.
Domain
concrete binary64 inputs, checked in the kernel on Lean's logical model of Float
Limits and assumptions
  • Concrete inputs only; it does not bound how far over 1 the output can go.
  • This record also covers IrToLean.Proof.rationalTanh_nan_is_nan, IrToLean.Proof.rationalTanh_over_one_on_float; axioms describe IrToLean.Proof.rationalTanh_not_bounded_on_float only.
Theorem
IrToLean.Proof.rationalTanh_not_bounded_on_float
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed