Performance

4 measured workloads · Node.js · Apple M4 Pro

Typical processing

2.42 µs

Busier blocks

2.54 µs

Share of the test budget

0.2%

Short decay · 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
58.4 KiB
Impulse first arrival
32.25 ms
Peak output
-26.93 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 · 58.4 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 · -26.93 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.00027
Signed mean over the same steady-render channels and final 4096 frames.
Output RMS · -30.09 dBFS
RMS over all channels of the same steady-render window.
Impulse first arrival · 32.25 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 · -73.51 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
482.422.540.1%—
482.422.790.1%Timing varies
962.422.540.2%—
962.422.540.2%—

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.

5 Lean 4 results: 4 proofs in their stated domains; 1 refused rewrite.

Proved in the stated domain.For every in-range index and every power-of-two length, wrapping by mask gives the same next index as wrapping by compare.
Domain
32-bit unsigned words, index below the length, length a power of two below 2^31
Limits and assumptions
  • About a Lean model of boundedIndex, which is not exported and has no hash link to the shipped code. The mask is illegal on non-power-of-two lines such as the Schroeder comb lengths, so it does not apply to the code Maru ships; the proof also trusts bv_decide's checker running as native code.
Theorem
MaruLean.RingWrap.mask_eq_compare
Recorded axioms
propext, Classical.choice, Quot.sound, RingWrap.mask_eq_compare._native.bv_decide.ax_1_7
Manifest reviewed
Proved in the stated domain.For every index below a non-zero length, wrapping by unsigned remainder gives the same next index as wrapping by compare.
Domain
32-bit unsigned words, index below the length
Limits and assumptions
  • About a Lean model of boundedIndex, not linked to the shipped code by a hash check, and it trusts bv_decide's checker running as native code. Once the index has left the line the substitution is refused.
Theorem
MaruLean.RingWrap.mod_eq_compare
Recorded axioms
propext, Classical.choice, Quot.sound, RingWrap.mod_eq_compare._native.bv_decide.ax_1_7
Manifest reviewed
Proved in the stated domain.The 32-bit compare wrap equals the unbounded integer wrap for every in-range index and every length below 2^32.
Domain
natural numbers, index below the length, length below 2^32
Limits and assumptions
  • About a Lean model of boundedIndex; the step from a JavaScript number to a natural number is not proved here.
Theorem
MaruLean.RingWrap.compare_toNat
Recorded axioms
propext, Quot.sound
Manifest reviewed
Rewrite refused.A mask on a length-1000 line, a mask or modulo once the index has left the line, and modulo on a zero length each give a different index than compare.
Domain
one concrete 32-bit input per rewrite
Limits and assumptions
  • Each witness is one input; it shows a guard a compiler rule must keep, not which inputs real modules reach.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
  • This record also covers MaruLean.RingWrap.mask_refused_out_of_range, MaruLean.RingWrap.mod_refused_out_of_range, MaruLean.RingWrap.mod_refused_zero_length; axioms describe MaruLean.RingWrap.mask_refused_non_power_of_two only.
Theorem
MaruLean.RingWrap.mask_refused_non_power_of_two
Manifest reviewed
Proved in the stated domain.In the hand-counted model, the mask ring wrap does not dominate the compare wrap, so the model makes no prediction for that pair.
Domain
counting model
Limits and assumptions
  • Hand-counted operations for C kernels; the model says nothing here, and measurement decides speed.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
Theorem
MaruLean.CostModel.mask_dominates_nothing_against_compare
Manifest reviewed