Build with this node

Start with a prompt in Studio, or copy it into your own coding agent.

Ask Studio

@maruaudio/dsp/voices/sampler-zone is a zone-mapped sampler over a host-loaded arena: selection by key range, velocity layer and keyswitch window; root-pitch, source-rate playback with fine tune and transpose; per-zone gain, constant-power pan and velocity response; velocity crossfades; a linear AR or optional AHDSR envelope; 12 ms choke fades; round robin; crossfaded loops; release-trigger and one-shot zones; reverse; a per-zone RBJ low-pass. Legato zones, ping-pong loops, other filter types and streaming are refused.

Parameters

samplerZoneApplyParam(state, lane, value), lanes 0..16, clamped as coded:

LaneRangeDefault
0 master level (applied by the caller per frame)0 to 10.8
1 / 2 amp attack / release0 to 10000 ms, every zone0 / 300
3 transpose / 4 bend range−24 to 24 / 0 to 24 semitones0 / 2
5 / 6 mod-wheel / pressure level−24 to 24 dB0 / 0
7 / 8 amp decay / sustain0 to 10000 ms / 0 to 10 / 1
9 / 10 / 11 filter cutoff / Q / env amount20 to 20000 Hz / 0.1 to 20 / ±8 oct20000 / 0.7071 / 0
12, 13, 15 filter attack, decay, release / 14 sustain / 16 velocity0 to 10000 ms / 0 to 1 / 0 to 10

The instrument filter engages below 20 kHz or with a non-zero amount; it refreshes every 16 voice frames.

Lifecycle

Capacities must be finite integers: arena size is nonnegative, while zone and voice counts are positive and no larger than their declared ceilings. Invalid requests throw before allocation. A zero-sized initial arena supports later installation of an adapter-owned sample resource. The adapter keeps that resource alive and clears the bank before refilling, shrinking or releasing it; resource changes and rendering are serialized.

createSamplerZoneState(arenaSamples, zones, voices) allocates at the caller's capacities (at most 1024 zones, 96 voices, 64 active by default) → the host fills state.arena and declares zones with samplerZoneSetZone (30 fields; returns a rejection code) → samplerZoneStartNote / …StopNote → per block samplerZoneUpdateFilterCoefficients, then samplerZoneRenderFrame(state, bus) per frame leaves the pre-master pair in bus. Clear voices, round robin or params keeps the zones; samplerZoneClearZones drops the bank. Optional entries add AHDSR, one-shot, A/B zone flips, glide, bend, wheel, pressure and sustain.

When to use it

Multisampled instruments and kits with splits, layers, keyswitches, alternate takes and loops.

Limits

  • Stereo, sample tick; voices steal oldest-first by serial; zones may route to four buses.
  • A voice never ends on a non-zero sample: releases under 3 ms are lengthened to 3 ms, unlooped regions fade over their last 3 ms, reclaimed voices leave through the 5 ms bus bridge; there is no attack floor.

Algorithm properties and proofs

Lean 4 checks specific properties of this algorithm’s mathematical model. Each model result applies within its stated domain and assumptions.

22 Lean 4 results: 10 proofs in their stated domains; 9 proofs in exact arithmetic; 3 counterexamples.

Proved in the stated domain.Reversing an in-range frame keeps the read index inside the same region.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.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.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
Show 19 more Lean 4 results
Proved in the stated domain.The next interpolation partner of a valid continuous loop remains below the loop end.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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
Explore proofs alongside performance

Dependencies

Dependents

No other node imports this one.

Used by