Iterator libraries for sequential traversal are standard, but efficiently expressing complex joins over associative collections (e.g., sparse intersection, union, triangle queries) without intermediate allocations or specialized compiler infrastructure remains difficult.

The authors implement an indexed stream fusion library for Lean, Morphic, and Rust. Indexed streams generalize iterators by exposing a seek/advance interface keyed by an ordered index, enabling non-sequential traversal and multi-way joins with no intermediate allocations. A mechanized proof of functional correctness is provided in Lean, building on prior indexed stream theory.

The library matches hand-written performance on benchmarks including triangle queries and red-black tree operations. It requires no staged compilation or specialized compiler passes. The Lean correctness proof covers the shallow embedding directly, providing end-to-end guarantees without trusting a custom code generator.