Alignment delay (@maru/delays-alignment)

Performance

4 measured workloads · Node.js · Apple M4 Pro

Typical processing

1.38 µs

Busier blocks

1.50 µs

Share of the test budget

0.1%

16-frame alignment · 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: 8.0 KiB
Impulse first arrival: 0.17 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 · 8.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.00004: Signed mean over the same steady-render channels and final 4096 frames.
Output RMS · -16.98 dBFS: RMS over all channels of the same steady-render window.
Impulse first arrival · 0.17 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 · -120.00 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 · kHz	Typical · µs	Busier blocks · µs	Test budget used	Observations
48	1.33	1.42	0.1%	Timing varies
48	1.38	1.50	0.1%	—
96	1.33	1.46	0.1%	—
96	1.38	1.50	0.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 · Nov 7, 2026

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.

3 Lean 4 results: 2 proofs in their stated domains; 1 counterexample.

Proved in the stated domain.Advancing a ring cursor by compare-and-reset produces an index below every positive active length.

Domain: Natural-number cursor and positive active length
Limits and assumptions: Hand-written source-reviewed model, not formal refinement of TypeScript or compiled code. Named functions and whole-file source digests are checked; finite canonical JavaScript cases are compared with executable Lean definitions. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer. The read before this update still needs a valid initial cursor and allocated capacity.
Theorem: MaruLean.LeafContracts.ring_step_in_bounds
Recorded axioms: propext, Quot.sound
Manifest reviewed: 2026-11-08

Proved in the stated domain.The final active ring position advances to zero.

Domain: Natural-number positive active length
Limits and assumptions: Hand-written source-reviewed model, not formal refinement of TypeScript or compiled code. Named functions and whole-file source digests are checked; finite canonical JavaScript cases are compared with executable Lean definitions. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer.
Theorem: MaruLean.LeafContracts.ring_step_last
Recorded axioms: propext, Quot.sound
Manifest reviewed: 2026-11-08

Counterexample.An empty active ring has no valid in-range cursor, even when compare-and-reset returns zero.

Domain: One zero-length integer witness
Limits and assumptions: Hand-written source-reviewed model, not formal refinement of TypeScript or compiled code. Named functions and whole-file source digests are checked; finite canonical JavaScript cases are compared with executable Lean definitions. One concrete witness; it refutes the stated unrestricted claim, not every possible guarded implementation. Alignment deliberately bypasses its buffer when frames is zero; this is not a claim that its bypass is unsafe.
Theorem: MaruLean.LeafContracts.ring_empty_refuses_bound
Manifest reviewed: 2026-11-08