Performance

6 measured workloads · Node.js · Apple M4 Pro

Typical processing

0.313 ms

Busier blocks

0.338 ms

Share of the test budget

12.7%

64 voices · With low-pass filter · 48 kHz · 2.667 ms available per block in this test.

Processing cost

Processing time in ms · 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.
All measured cases
VoicesWorkloadTypical · msBusier blocks · msTest budget usedObservations
1 voice0.0240.0271.0%Timing varies
1 voice0.0250.0271.0%Timing varies · Some blocks exceeded the budget
16 voices0.0740.0813.0%—
16 voices0.0960.1023.8%—
64 voices0.2280.2409.0%—
64 voices0.3130.33812.7%—

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 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: 10 proofs in their stated domains; 9 proofs in exact arithmetic; 3 counterexamples.

Explore the mathematics

Move the controls to explore a theorem’s behavior and assumptions. These browser calculations use floating-point numbers to illustrate the mathematical model. They do not run Lean or the audio engine. Lean checks the general statement; a plotted example does not prove it.

Sampler loop wrapping

wrap(i) = start + (i − start) mod length, once i ≥ end

Natural-number indices, a positive loop length and a cursor at or after the loop start. Before the start, the cursor is unchanged and the loop-range theorem does not apply.

Loop start8
Loop length16
Cursor index48

Within theorem assumptions

The lower bound is inclusive and the end is exclusive. The plot includes pre-roll before the start, where the loop-range guarantee does not apply.

Cursor index → Wrapped index. Solid line: numerical example. Dashed lines: loop bounds. Vertical lines: selected positions.
Wrapped cursor
16
Loop start (inclusive)
8
Loop end (exclusive)
24
Read this proof’s domain and limits
Proved in the stated domain.Reversing an in-range frame keeps the read index inside the same region.
Domain
Natural-number region addresses; index below frame count
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.reverse_in_bounds
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.Reversing an in-range frame twice returns its original play index.
Domain
Natural-number region addresses; index below frame count
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.reverse_involution
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.A reversed frame remains inside the arena when the entire region fits in that arena.
Domain
Natural-number base, frame count, index and arena capacity; index < frames and base + frames <= capacity
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.reverse_arena_bound
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.The next interpolation partner of a valid continuous loop remains below the loop end.
Domain
Natural-number continuous-loop addresses; start < end and index < end
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.loop_partner_in_bounds
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in the stated domain.The interpolation partner of the last loop frame is the loop start, not the unlooped frame after the end.
Domain
Natural-number continuous-loop addresses; start < end
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.loop_partner_at_seam
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in the stated domain.Before the loop seam, the interpolation partner is exactly the next frame.
Domain
Natural-number continuous-loop addresses; index + 1 < end
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.loop_partner_before_seam
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.Subtracting the number of whole loop lengths equals taking the integer remainder, with no iterative wrap.
Domain
Natural-number distance and length; exact integer division
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.wrap_division_is_remainder
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.A cursor at or beyond the loop start wraps inside the loop even after overshooting by several lengths.
Domain
Natural-number addresses; start < end and start <= index
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.wrap_in_bounds
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in the stated domain.Wrapping leaves a cursor before the loop end unchanged, including pre-roll frames.
Domain
Natural-number addresses; index < end
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.wrap_inside_unchanged
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.Wrapping a valid cursor a second time cannot move it again.
Domain
Natural-number addresses; start < end and start <= index
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.wrap_idempotent
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.A pre-roll index of 2 stays at 2 for loop [4, 8); the unconditional claim that every cursor is at least the loop start is false.
Domain
One exact integer pre-roll 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.
Theorem
MaruLean.LeafContracts.wrap_preroll_refuses_lower_bound
Manifest reviewed
Proved in exact arithmetic.Linear interpolation at fraction zero selects the first sample and at fraction one selects the second.
Domain
Exact rational samples and fractions zero or one
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. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster.
Theorem
MaruLean.LeafContracts.lerp_endpoints
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Interpolating two bounded samples stays in their common interval when the fraction is between zero and one.
Domain
Exact rationals; ordered finite bounds and stated coefficient guards; fraction in [0, 1]
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. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster.
Theorem
MaruLean.LeafContracts.lerp_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.Interpolation with fraction 2 produces 2 from samples 0 and 1; a bounded-output claim requires the fraction guard.
Domain
One exact rational extrapolation 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.
Theorem
MaruLean.LeafContracts.lerp_extrapolation_refused
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The cubic smoothstep loop-crossfade weight remains between zero and one for a normalized position.
Domain
Exact rational normalized position in [0, 1]
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. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster.
Theorem
MaruLean.LeafContracts.smoothstep_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The cubic crossfade weight is zero at normalized position zero and one at normalized position one.
Domain
Exact rational normalized positions zero and one
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. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster. The first actual crossfade frame uses normalized position 1/span, not zero.
Theorem
MaruLean.LeafContracts.smoothstep_endpoints
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The last frame of a positive crossfade span reaches the incoming run-up material exactly.
Domain
Exact rational samples and positive crossfade span; position = span - 1
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. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster.
Theorem
MaruLean.LeafContracts.crossfade_last
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.A loop crossfade stays in the common interval of both samples throughout its valid span.
Domain
Exact rational bounded samples; span > 0, position >= 0 and position + 1 <= span
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. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster.
Theorem
MaruLean.LeafContracts.crossfade_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The squared velocity curve stays between zero and one for a normalized strike.
Domain
Exact rational normalized velocity in [0, 1]
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. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster.
Theorem
MaruLean.LeafContracts.velocity_square_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Both linear and squared velocity responses stay between the configured floor and unity.
Domain
Exact rational velocity and floor in [0, 1]; linear or squared curve
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. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster.
Theorem
MaruLean.LeafContracts.velocity_response_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.A velocity-response floor of one gives unity gain for either curve.
Domain
Exact rational velocity; floor = 1; linear or squared curve
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. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster.
Theorem
MaruLean.LeafContracts.velocity_response_neutral
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.The sampler cursor fraction 1 - 2^-25 rounds to exactly one at its f32 store, so a strict fraction < 1 invariant is false.
Domain
One binary64-to-binary32 conversion at the sampler cursor store
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. The Lean conversion witness trusts native_decide; the canonical JavaScript cursor reproduces it. This alone does not establish an audible defect.
Theorem
MaruLean.LeafContracts.cursor_fraction_can_round_to_one
Recorded axioms
propext, Classical.choice, Quot.sound, MaruLean.LeafContracts.cursor_fraction_can_round_to_one._native.native_decide.ax_1_1
Manifest reviewed