Performance

4 measured workloads · Node.js · Apple M4 Pro

Typical processing

3.92 µs

Busier blocks

4.08 µs

Share of the test budget

0.3%

32-tap decaying IR · 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
2.0 KiB
Impulse first arrival
0.00 ms
Peak output
-18.24 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 · 2.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 · -18.24 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 · -21.24 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 · -4.26 dB
Left-channel RMS gain from the measured tone-gain sweep.
All measured cases
Sample rate · kHzWorkloadTypical · µsBusier blocks · µsTest budget usedObservations
4822.2927.251.0%Timing varies
483.964.290.2%Timing varies
9622.7928.462.1%Timing varies
963.924.080.3%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.

6 Lean 4 results: 5 proofs in their stated domains; 1 counterexample.

Proved in the stated domain.Every index processed inside an admitted FIR interval is valid for both source and target.
Domain
Natural-number admitted block intervals and prepared history-ring addresses
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. The ring model uses a conditional backwards step; the canonical 256-slot bit-mask traversal is compared on executable vectors, not formally translated. The interval proof assumes prior fixed-buffer/disjoint-or-identical-span admission. It does not prove backing ownership, IEEE convolution sums, IR loading or all execution paths.
Theorem
MaruLean.LeafContracts.admitted_block_access_in_bounds
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in the stated domain.Each admitted FIR loop step strictly decreases the remaining frame count.
Domain
Natural-number admitted block intervals and prepared history-ring addresses
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. The ring model uses a conditional backwards step; the canonical 256-slot bit-mask traversal is compared on executable vectors, not formally translated. The interval proof assumes prior fixed-buffer/disjoint-or-identical-span admission. It does not prove backing ownership, IEEE convolution sums, IR loading or all execution paths.
Theorem
MaruLean.LeafContracts.admitted_block_step_remaining
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.A backwards history-ring step preserves the prepared ring bound.
Domain
Natural-number admitted block intervals and prepared history-ring addresses
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. The ring model uses a conditional backwards step; the canonical 256-slot bit-mask traversal is compared on executable vectors, not formally translated. The interval proof assumes prior fixed-buffer/disjoint-or-identical-span admission. It does not prove backing ownership, IEEE convolution sums, IR loading or all execution paths.
Theorem
MaruLean.LeafContracts.fir_previous_in_bounds
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.A backwards history step followed by a forward step returns the same admitted index.
Domain
Natural-number admitted block intervals and prepared history-ring addresses
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. The ring model uses a conditional backwards step; the canonical 256-slot bit-mask traversal is compared on executable vectors, not formally translated. The interval proof assumes prior fixed-buffer/disjoint-or-identical-span admission. It does not prove backing ownership, IEEE convolution sums, IR loading or all execution paths.
Theorem
MaruLean.LeafContracts.fir_previous_reverses_step
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.Every tap in a backwards FIR history walk stays inside the prepared ring.
Domain
Natural-number admitted block intervals and prepared history-ring addresses
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. The ring model uses a conditional backwards step; the canonical 256-slot bit-mask traversal is compared on executable vectors, not formally translated. The interval proof assumes prior fixed-buffer/disjoint-or-identical-span admission. It does not prove backing ownership, IEEE convolution sums, IR loading or all execution paths.
Theorem
MaruLean.LeafContracts.fir_walk_in_bounds
Recorded axioms
propext, Quot.sound
Manifest reviewed
Counterexample.A block interval without the source-length guard can address past the source.
Domain
Natural-number admitted block intervals and prepared history-ring addresses
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. The ring model uses a conditional backwards step; the canonical 256-slot bit-mask traversal is compared on executable vectors, not formally translated. The interval proof assumes prior fixed-buffer/disjoint-or-identical-span admission. It does not prove backing ownership, IEEE convolution sums, IR loading or all execution paths.
Theorem
MaruLean.LeafContracts.block_without_length_guard_refuses_bound
Manifest reviewed