Performance

4 measured workloads · Node.js · Apple M4 Pro

Typical processing

1.50 µs

Busier blocks

1.58 µs

Share of the test budget

0.1%

6 kHz cutoff · Q 2 · 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.

Timing varied between repeated tests. Treat this case as a guide.

Retained DSP buffers
0 bytes
Impulse first arrival
0.00 ms
Peak output
-13.77 dBFS

Measured tone gain

Gain · dB

Nine separate 0.2-peak sine renders; left-channel RMS gain during 250–500 ms. Includes modulation/envelope behavior; not an LTI error or phase-response measurement.
Measurement details
Retained DSP buffers · 0 bytes
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.77 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.00106
Signed mean over the same steady-render channels and final 4096 frames.
Output RMS · -16.79 dBFS
RMS over all channels of the same steady-render window.
Impulse first arrival · 0.00 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.
Gain at 1 kHz · 0.21 dB
Left-channel RMS gain from the measured tone-gain sweep.
All measured cases
Sample rate · kHzWorkloadTypical · µsBusier blocks · µsTest budget usedObservations
481.501.670.1%Timing varies
481.461.580.1%—
961.541.630.1%—
961.501.580.1%Timing varies

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.

22 Lean 4 results: 4 proofs in their stated domains; 9 proofs in exact arithmetic; 1 refused rewrite; 8 counterexamples.

Proved in exact arithmetic.Direct form I and transposed direct form II give the same output on every input, for every coefficient set and related start state.
Domain
exact arithmetic over any commutative ring
Limits and assumptions
  • Not a theorem about floats, which are not a ring, so it says nothing about bit-exact output; the measured output of the two forms differs, by at most 2.5e-15 on the bench input.
  • This record also covers MaruLean.BiquadForms.step_related; axioms describe MaruLean.BiquadForms.run_eq only.
Theorem
MaruLean.BiquadForms.run_eq
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Rewrite refused.Computing Math.fround(a * b + c), the biquadOutput shape, entirely in binary32 gives different bits from double arithmetic rounded once, so an all-f32 biquad is a sound change and not a lowering.
Domain
binary32 and binary64, one concrete input
Limits and assumptions
  • One witness; native_decide puts the Lean compiler and Float runtime in the trusted base. Whether an all-f32 filter is acceptable as a sound change is a design decision () for measurement and listening, not for this proof.
Theorem
MaruLean.FloatRefusals.all_f32_refused
Recorded axioms
propext, Classical.choice, Quot.sound, FloatRefusals.all_f32_refused._native.native_decide.ax_1_1
Manifest reviewed
Proved in the stated domain.In the hand-counted model, the transposed direct form II biquad kernel uses no more of any operation than the direct form I kernel.
Domain
counting model
Limits and assumptions
  • Hand-counted source-level operations for the C kernels in bench/kernels.c, with no pipeline, vectorizer, cache or branch predictor; measurement decides speed, and the C control measured no clear difference between the two forms.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
Theorem
MaruLean.CostModel.tdf2_dominates_df1
Manifest reviewed
Proved in exact arithmetic.The lowpass, highpass, bandpass and notch coefficients of biquad.ts satisfy the Jury conditions, so their exact poles lie strictly inside the unit circle.
Domain
exact arithmetic in any ordered field, with -1 < cos w0 < 1 and 0 < alpha assumed
Limits and assumptions
  • Exact arithmetic in an ordered field, with the trigonometry assumed: the code rounds the cosine to binary32 first, and the binary32 rounding of a1 and a2 is where the filter really fails, so this does not protect the shipped code (). Frozen settings only; a moving cutoff is a different question.
  • This record also covers MaruLean.FilterStability.rbj_dPlus, MaruLean.FilterStability.rbj_dMinus, MaruLean.FilterStability.jury_real_root, MaruLean.FilterStability.jury_complex_root, MaruLean.FilterStability.w0_in_open_half_turn; axioms describe MaruLean.FilterStability.rbj_jury only.
Theorem
MaruLean.FilterStability.rbj_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The peaking coefficients of biquad.ts satisfy the Jury conditions for every positive gain.
Domain
exact arithmetic in any ordered field, with -1 < cos w0 < 1, 0 < alpha and 0 < A assumed
Limits and assumptions
  • Exact arithmetic in an ordered field, with the trigonometry assumed: the code rounds the cosine to binary32 first, and the binary32 rounding of a1 and a2 is where the filter really fails, so this does not protect the shipped code (). Frozen settings only; a moving cutoff is a different question.
Theorem
MaruLean.FilterStability.peak_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The low and high shelf coefficients of biquad.ts satisfy the Jury conditions, and each shelf is the shared denominator with a cosine moved toward 1 by a boost.
Domain
exact arithmetic in any ordered field, with -1 < cos w0 < 1, 0 < A and 0 < beta assumed
Limits and assumptions
  • Exact arithmetic in an ordered field, with the trigonometry assumed: the code rounds the cosine to binary32 first, and the binary32 rounding of a1 and a2 is where the filter really fails, so this does not protect the shipped code (). Frozen settings only; a moving cutoff is a different question.
  • This record also covers MaruLean.FilterStability.highShelf_jury, MaruLean.FilterStability.lowShelf_a0_pos, MaruLean.FilterStability.lowShelf_eq_rbj, MaruLean.FilterStability.highShelf_eq_lowShelf; axioms describe MaruLean.FilterStability.lowShelf_jury only.
Theorem
MaruLean.FilterStability.lowShelf_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.If rounding sends the cosine to exactly 1, the exact margin at z = 1 is zero whatever the Q, so the pole is on the unit circle.
Domain
exact arithmetic in any ordered field, cosine exactly 1
Limits and assumptions
  • Shows that the clamps do not give the hypothesis the stability theorems need for the value the code actually uses; the code's binary32 cosine reaches 1 at 10 Hz above about 257 kHz.
Theorem
MaruLean.FilterStability.rbj_dPlus_at_cos_one
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Rounded coefficients still satisfy the Jury conditions when each exact margin is larger than the rounding movement it can suffer.
Domain
exact arithmetic in any ordered field, with a stated rounding budget
Limits and assumptions
  • The budget is a stated bound on the code, not something proved about its floats; at low frequency the margin at z = 1 is the hard one and real settings break it.
  • This record also covers MaruLean.FilterStability.jury_of_budget; axioms describe MaruLean.FilterStability.rbj_rounded_jury only.
Theorem
MaruLean.FilterStability.rbj_rounded_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.If the denominator polynomial is not positive at some g above 1 and a2 is non-negative, the free recursion grows at least like g^n.
Domain
exact arithmetic in any ordered field
Limits and assumptions
  • A lower bound on growth in exact arithmetic; the real rounded filter is measured by bench/filter-stability-sweep.mjs.
  • This record also covers MaruLean.FilterStability.freeRun_ratio; axioms describe MaruLean.FilterStability.freeRun_grows only.
Theorem
MaruLean.FilterStability.freeRun_grows
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.At 384 kHz, 10 Hz and Q 1, the coefficients the real setter stores for the shared RBJ denominator fail the Jury conditions with a margin of -2^-24, and their free recursion grows at least like 1.0001^n.
Domain
exact rational arithmetic on the real stored binary32 coefficients
Limits and assumptions
  • The coefficients are recomputed from the real function by bench/filter-stability-witnesses.mjs; the growth bound is a lower bound, and the real filter overflows sooner, in about 1.4 seconds.
  • This record also covers MaruLean.FilterStability.w384_dPlus, MaruLean.FilterStability.w384_grows; axioms describe MaruLean.FilterStability.w384_rounded_not_jury only.
Theorem
MaruLean.FilterStability.w384_rounded_not_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.A low shelf at 192 kHz, 11.27 Hz, Q 0.0139 and +24 dB is stable with exact coefficients, and rounding each to the nearest binary32 breaks the Jury conditions so the filter grows.
Domain
exact rational arithmetic on the real cosine, beta and stored binary32 coefficients
Limits and assumptions
  • One real setting; the exact theorem is true and does not protect the code. Which modules reach this setting is not shown here.
  • This record also covers MaruLean.FilterStability.w192_exact_jury, MaruLean.FilterStability.w192_rounding_is_small, MaruLean.FilterStability.w192_grows; axioms describe MaruLean.FilterStability.w192_rounded_not_jury only.
Theorem
MaruLean.FilterStability.w192_rounded_not_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.A peaking filter at 96 kHz, 10 Hz, Q 0.0001 and -23.5 dB is stable with exact coefficients, and the rounded pair puts a pole exactly at z = 1.
Domain
exact rational arithmetic on the real stored binary32 coefficients
Limits and assumptions
  • One real setting; which modules reach it is not shown here.
  • This record also covers MaruLean.FilterStability.w96_exact_jury, MaruLean.FilterStability.w96_pole_at_one; axioms describe MaruLean.FilterStability.w96_rounded_not_jury only.
Theorem
MaruLean.FilterStability.w96_rounded_not_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Direct form I has the same trace and determinant as the shipped transposed form under any two-setting alternation, so switching form does not escape alternation growth.
Domain
exact arithmetic over any commutative ring
Limits and assumptions
  • Exact arithmetic with no input; the rounded tick is measured in bench/modulation/time-warp-check.mjs, not proved. Nobody has listened, so it says nothing about which filter sounds better.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
Theorem
MaruLean.ModulationStability.df1_same_alternation
Manifest reviewed
Counterexample.Two real binary32 biquad settings at 48 kHz and Q 0.7071, 9847.8 Hz and 20 kHz, are each stable when frozen, and alternating them on every sample grows.
Domain
exact rational arithmetic on the real stored binary32 coefficients, no input
Limits and assumptions
  • One pair of settings in exact arithmetic; the biquad's modulation limit is measured, not proved.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
  • This record also covers MaruLean.ModulationStability.witness_fast_frozen_stable; axioms describe MaruLean.ModulationStability.witness_fast_grows only.
Theorem
MaruLean.ModulationStability.witness_fast_grows
Manifest reviewed
Counterexample.Moving a Q 5 biquad at 48 kHz by one octave around 100 Hz, holding each setting for 109 samples, grows although each setting is stable when frozen.
Domain
exact rational arithmetic on the real stored binary32 coefficients, no input
Limits and assumptions
  • One pattern in exact arithmetic, checked with native_decide, which trusts the Lean compiler; the real tick's runaway is measured, not proved, and the biquad's modulation limit is measured, not proved.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
  • This record also covers MaruLean.ModulationStability.witness_low_frozen_stable; axioms describe MaruLean.ModulationStability.witness_low_grows only.
Theorem
MaruLean.ModulationStability.witness_low_grows
Manifest reviewed
Proved in exact arithmetic.At a fixed point of the rounded biquad tick on a constant input, the output misses the exact answer by the sum of the three rounding errors divided by 1 + a1 + a2.
Domain
exact arithmetic in an ordered field
Limits and assumptions
  • Nothing connects the values to IEEE rounding beyond real-dc-check.mjs and the half-unit checks in the file.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
Theorem
MaruLean.ErrorBounds.stuck_offset
Manifest reviewed
Counterexample.Real stuck states of the biquad lowpass at 10 Hz and 96 kHz, and at 20 Hz and 48 kHz, miss the exact constant-input answer by more than 0.03 and 0.0028, and the offset comes only from rounding.
Domain
exact rational arithmetic on real stored binary32 states and coefficients
Limits and assumptions
  • Which modules reach these settings, and whether the offset is audible, is unknown; the numbers are checked against the real code by real-dc-check.mjs, not proved about it.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
  • This record also covers MaruLean.ErrorBounds.w10_offset, MaruLean.ErrorBounds.w20_offset, MaruLean.ErrorBounds.w20_offset_is_rounding; axioms describe MaruLean.ErrorBounds.w10_offset_is_rounding only.
Theorem
MaruLean.ErrorBounds.w10_offset_is_rounding
Manifest reviewed
Proved in the stated domain.Over Float, the biquad tick built from Lean generated from Maru compiler IR of biquad.ts is definitionally the hand-written fround model in BiquadForms.lean.
Domain
every Float input, with fround opaque and the same on both sides
Limits and assumptions
  • The tick composition itself is written by hand, because the translator refuses biquadNodeTick; the translator covers only 7.7% of MultiFX hot-path nodes so far.
Theorem
IrToLean.Proof.tick_float_is_hand_model
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The biquad arithmetic generated from biquad.ts gives the direct form I output for any coefficients, input and related start state.
Domain
exact arithmetic over any commutative ring, fround as the identity
Limits and assumptions
  • Says nothing about rounding, and floats are not a ring.
  • This record also covers IrToLean.Proof.tick_exact_is_tdf2, IrToLean.Proof.run_exact_is_tdf2; axioms describe IrToLean.Proof.run_exact_eq_df1 only.
Theorem
IrToLean.Proof.run_exact_eq_df1
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.The clamp in filters/biquad.ts keeps -0 with bounds [0, 1], while the clamp in math/range.ts gives +0.
Domain
one concrete binary64 input, compared by bits
Limits and assumptions
  • One input; whether either difference is reachable or audible in a module is not shown.
Theorem
IrToLean.Proof.clamps_disagree_on_negative_zero
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in the stated domain.The real clamp from biquad.ts returns one of its arguments bit for bit, whatever they are.
Domain
every Float and every instance of the comparison class, with no arithmetic
Limits and assumptions
  • It holds on the running type only because it does no arithmetic; it does not say which argument comes back for -0, which differs between clamps.
Theorem
IrToLean.Proof.clamp_returns_an_input
Recorded axioms
propext
Manifest reviewed
Proved in the stated domain.One concrete biquadOutput generated from Maru compiler IR gives the expected bits, on Lean's Float model with froundModel and through the compiler.
Domain
one concrete binary64 input
Limits and assumptions
  • A single test vector; the model form trusts this package's froundModel, and the native form trusts the Lean compiler through native_decide.
  • This record also covers IrToLean.Proof.biquadOutput_vector_native; axioms describe IrToLean.Proof.biquadOutput_vector_model only.
Theorem
IrToLean.Proof.biquadOutput_vector_model
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed