Performance

4 measured workloads · Node.js · Apple M4 Pro

Typical processing

1.58 µs

Busier blocks

1.67 µs

Share of the test budget

0.1%

250.5 ms · feedback 0.7 · 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
375.0 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 · 375.0 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 · -9.52 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.541.710.1%Timing varies
481.581.710.1%—
961.581.880.1%Timing varies
961.581.670.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.

5 Lean 4 results: 3 proofs in their stated domains; 1 proof in exact arithmetic; 1 counterexample.

Proved in the stated domain.Subtracting an admitted whole-sample delay wraps to an in-range fractional-ring tap.
Domain
Natural-number ring addresses; rational interpolation with bounded fraction
Limits and assumptions
  • Hand-written source-reviewed Nat/Rat model, not formal refinement of TypeScript, Rust or compiled output. Whole-file source digests and finite canonical JavaScript vectors are checked. Capacities, clocks, delay and block addresses must be valid nonnegative exactly representable integers. Circular subtraction models the integer tap coordinate; the continuous floor/wrap implementation is linked by dyadic vectors rather than a general floating-point proof. Interpolation bounds omit IEEE rounding, Float32 storage, NaN and infinities; they require a fraction in [0,1]. No proof of initialization, ownership or the allpass-tap path.
Theorem
MaruLean.LeafContracts.circular_subtract_in_bounds
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.A delay that does not cross the ring seam preserves its integer address difference.
Domain
Natural-number ring addresses; rational interpolation with bounded fraction
Limits and assumptions
  • Hand-written source-reviewed Nat/Rat model, not formal refinement of TypeScript, Rust or compiled output. Whole-file source digests and finite canonical JavaScript vectors are checked. Capacities, clocks, delay and block addresses must be valid nonnegative exactly representable integers. Circular subtraction models the integer tap coordinate; the continuous floor/wrap implementation is linked by dyadic vectors rather than a general floating-point proof. Interpolation bounds omit IEEE rounding, Float32 storage, NaN and infinities; they require a fraction in [0,1]. No proof of initialization, ownership or the allpass-tap path.
Theorem
MaruLean.LeafContracts.circular_subtract_no_wrap
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.Both interpolating taps stay inside a prepared ring when the write clock and delay are admitted.
Domain
Natural-number ring addresses; rational interpolation with bounded fraction
Limits and assumptions
  • Hand-written source-reviewed Nat/Rat model, not formal refinement of TypeScript, Rust or compiled output. Whole-file source digests and finite canonical JavaScript vectors are checked. Capacities, clocks, delay and block addresses must be valid nonnegative exactly representable integers. Circular subtraction models the integer tap coordinate; the continuous floor/wrap implementation is linked by dyadic vectors rather than a general floating-point proof. Interpolation bounds omit IEEE rounding, Float32 storage, NaN and infinities; they require a fraction in [0,1]. No proof of initialization, ownership or the allpass-tap path.
Theorem
MaruLean.LeafContracts.fractional_pair_in_bounds
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The exact interpolation of two bounded ring samples stays within their interval.
Domain
Natural-number ring addresses; rational interpolation with bounded fraction
Limits and assumptions
  • Hand-written source-reviewed Nat/Rat model, not formal refinement of TypeScript, Rust or compiled output. Whole-file source digests and finite canonical JavaScript vectors are checked. Capacities, clocks, delay and block addresses must be valid nonnegative exactly representable integers. Circular subtraction models the integer tap coordinate; the continuous floor/wrap implementation is linked by dyadic vectors rather than a general floating-point proof. Interpolation bounds omit IEEE rounding, Float32 storage, NaN and infinities; they require a fraction in [0,1]. No proof of initialization, ownership or the allpass-tap path.
Theorem
MaruLean.LeafContracts.fractional_interpolation_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.An invalid write clock defeats the circular-read bound.
Domain
Natural-number ring addresses; rational interpolation with bounded fraction
Limits and assumptions
  • Hand-written source-reviewed Nat/Rat model, not formal refinement of TypeScript, Rust or compiled output. Whole-file source digests and finite canonical JavaScript vectors are checked. Capacities, clocks, delay and block addresses must be valid nonnegative exactly representable integers. Circular subtraction models the integer tap coordinate; the continuous floor/wrap implementation is linked by dyadic vectors rather than a general floating-point proof. Interpolation bounds omit IEEE rounding, Float32 storage, NaN and infinities; they require a fraction in [0,1]. No proof of initialization, ownership or the allpass-tap path.
Theorem
MaruLean.LeafContracts.fractional_invalid_clock_refuses_bound
Manifest reviewed