Looped region (@maru/tables-looped-region)

Build with this node

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

@maruaudio/dsp/tables/looped-region reads a bounded region of a host-loaded f32 sample table in play-order frames: forward or reversed, unlooped or looped continuously with a crossfade, with the (integer, fraction) cursor that plays it. Reversal is one subtraction (frames − 1 − index) applied last, at the read, so loop points and the crossfade span stay in play coordinates and mirror with it. A crossfaded loop blends its last span frames into the span frames that precede loopStart, with a smoothstep weight of t = (p + 1) / span that sums the two sides with equal gain, so the frame at loopEnd − 1 is loopStart − 1 itself and the wrap continues it.

Functions

Name	Inputs	Output	Domain as coded
`regionFrame`	`table, base, frames, reverse, index`	one frame	`index` assumed in [0, frames)
`loopedRegionFrameAt`	region, `loopMode, loopStart, loopEnd, crossfade, index`	frame with the crossfade applied	0 at or past `frames`; span clamped to the run-up before `loopStart` and to the loop length
`loopCrossfadeBlend`	`value, tail, position, crossfade`	equal-gain smoothstep blend	Weight reaches exactly 1 at the span's last frame
`loopNextIndex`	`index, loopMode, loopStart, loopEnd`	interpolation partner	In a continuous loop the frame after `loopEnd − 1` is `loopStart`
`lerp`	`a, b, fraction`	`a + (b − a) × fraction`
`reverseReadIndex`	`frames, index`	`frames − 1 − index`
`loopWrapIndex`	`index, loopStart, loopEnd`	index wrapped by whole loop lengths	Unchanged for an empty loop or an index inside it
`advanceLoopedCursor`	cursor arrays, `voice, step, loopMode, loopStart, loopEnd`	writes the voice's index and f32 fraction	Fraction stored through `Math.fround`

Loop modes are LOOPED_REGION_LOOP_NONE (0) and LOOPED_REGION_LOOP_CONTINUOUS (1); ping-pong is deliberately absent.

Lifecycle

None of its own. The caller owns the table, the region bounds and the Uint32Array index and Float32Array fraction cursors, and calls advanceLoopedCursor once per frame per voice. The table is never written.

When to use it

A sampler voice that loops a sustain region of a recording, possibly reversed or repitched, with a seam crossfade. voices/sampler-zone reads its zones through it.

Limits

Mono reads; linear interpolation. Allocation-free with no loops on the sample path: the wrap is one integer division, not a while, so Maru compiler's realtime prover needs no bound.
A loop starting at play frame 0 has no run-up and gets no crossfade; one starting at frame 200 gets at most 200 frames.
The stored fraction is the one f32 boundary; every other value is a double.

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.

21 Lean 4 results: 10 proofs in their stated domains; 8 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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

Show 18 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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

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: 2026-11-08

Proved in exact arithmetic.Linear interpolation satisfies Jensen’s squared-energy inequality throughout the unit interval, with an exact nonnegative deficit t(1-t)(a-b)².Ordered field; arbitrary samples a,b and interpolation fraction 0<=t<=1.

Limits and assumptions: Mathematical theorem over an arbitrary ordered field, with every hypothesis in its Lean type. Exact arithmetic only; IEEE rounding, overflow, non-finites and platform transcendental implementations are outside this theorem. Source bindings identify the reviewed DSP relationship, not a formal translation or a compiled-artifact proof. The inputs are scalar samples and the blend is linear. No claim is made about changing audio inputs across a window or about unguarded extrapolation.
This record also covers MaruLean.SignalBounds.lerp_energy_identity; axioms describe MaruLean.SignalBounds.lerp_energy_convex only.
Theorem: MaruLean.SignalBounds.lerp_energy_convex
Recorded axioms: propext, Classical.choice, Quot.sound
Manifest reviewed: 2026-11-08

Proved in exact arithmetic.The cubic crossfade S(t)=t²(3-2t) is strictly increasing on [0,1], with S(b)-S(a)>=(b-a)³ for every ordered pair of positions.Ordered field; 0<=a<=b<=1, with strict output order when a<b.

Limits and assumptions: Mathematical theorem over an arbitrary ordered field, with every hypothesis in its Lean type. Exact arithmetic only; IEEE rounding, overflow, non-finites and platform transcendental implementations are outside this theorem. Source bindings identify the reviewed DSP relationship, not a formal translation or a compiled-artifact proof. This is a quantified polynomial proof over the whole interval, not a sampled slope test. It concerns the blend weight; varying input audio need not itself be monotone.
This record also covers MaruLean.SignalBounds.smoothstep_increment_bound; axioms describe MaruLean.SignalBounds.smoothstep_strictly_increasing only.
Theorem: MaruLean.SignalBounds.smoothstep_strictly_increasing
Recorded axioms: propext, Classical.choice, Quot.sound
Manifest reviewed: 2026-11-08

Build with this node

Functions

Lifecycle

When to use it

Limits

Algorithm properties and proofs

Dependencies

Dependents

Used by