@maruaudio/dsp/delays/bounded is the non-regenerating sibling of @maru/delays-feedback: a whole-frame Float32Array ring that stores clamp(x, −1, 1) (the shared feedback write with the regeneration term exactly zero) and mixes the delayed sample with the dry input. Each input is heard once. The arithmetic is @maru/delays-primitives.
const state = initBoundedDelayNode(48000, BOUNDED_DELAY_MAX_MILLISECONDS)
setBoundedDelayTime(state, 120)
setBoundedDelayMix(state, 0.5)
const y = boundedDelayNodeTick(state, x)
Parameters
Setter
Range the setter enforces
Default
Unit
setBoundedDelayTime
max(1, round(ms·rate/1000)) frames, capped at the line allocated by init
The init time
ms
setBoundedDelayMix
0 to 1
0 (fully dry)
linear
Lifecycle
initBoundedDelayNode(sampleRate, ms) allocates the line once; pass BOUNDED_DELAY_MAX_MILLISECONDS (2000) to leave room → setters → boundedDelayNodeTick → resetBoundedDelayNode, which zeroes the line and index and keeps the settings. prepareBoundedDelayNodeSampleRate re-derives the length from the stored time without allocating and keeps the history.
When to use it
A single slapback, a doubling offset, or a fixed pre-delay before another effect.
Limits
Mono, whole-frame delay, no interpolation or feedback.
The stored sample is clipped to ±1 even at mix 1.
A time change jumps the read position, with no crossfade.
audio-kernels keeps the PCM16 render entry.
Implementations
Rust Output verified: The build passed and its output matches the reference implementation.
Verified on Apple Silicon macOS native and Node WASM at 8, 44.1, 48, 96 and 192 kHz. Output and state match the TypeScript reference, with no observed allocations, reallocations or deallocations during the tested processing, control and reset calls. Delay storage is prepared for 200 ms at 192 kHz; that prepared capacity is retained at lower rates. Browser hosts, plugins, other operating systems and realtime deadlines have not been verified. Performance has not been measured.
Lean 4 checks specific properties of this algorithm’s mathematical model. Each model result applies within its stated domain and assumptions.
7 Lean 4 results: 2 proofs in their stated domains; 4 proofs in exact arithmetic; 1 counterexample.
Proved in the stated domain.Advancing a ring cursor by compare-and-reset produces an index below every positive active length.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
Proved in the stated domain.The final active ring position advances to zero.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
Counterexample.An empty active ring has no valid in-range cursor, even when compare-and-reset returns zero.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
Show 4 more Lean 4 results
Proved in exact arithmetic.The dry/wet sum and the subtract-then-scale interpolation form are algebraically equal.Exact rational samples and mix coefficient
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. This does not authorize changing the existing floating-point operation order.
Theorem
MaruLean.LeafContracts.drywet_is_lerp
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.A dry/wet mix stays inside the common input interval for a mix between zero and one.Exact rationals; ordered finite bounds and stated coefficient guards; mix 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.drywet_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The clamped feedback write is between minus one and one in exact arithmetic.Exact rational dry sample, delayed sample and feedback
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. This covers only the write stage, not feedback-system stability.
Theorem
MaruLean.LeafContracts.feedback_write_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.At zero feedback the write stage is exactly the clamped dry sample.Exact rational dry and delayed samples; feedback = 0
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.