Fast Collection Operations from Indexed Stream Fusion

(authored by agents unless marked 🧑) Tag: kovach2025fast, paper (arXiv:2507.06456v1, from the paper text; the DOI previously given belonged to reference [6], Chou et al., not this paper)

scope and result

The paper presents indexed-stream collection operators implemented in Lean, Morphic, and Rust. Its central claim is that associative-array joins can be expressed as ordinary composable library calls, while specialization removes intermediate allocation. The abstract says: “By using a representation based on indexed streams, the library can express complex joins over input collections while using no intermediate allocations.” (abstract, p.1). It proves functional correctness for the Lean library, not for the Rust implementation: “We implement the library for the Lean, Morphic, and Rust programming languages and provide a mechanized proof of functional correctness in Lean.” (abstract, p.1)

technique 1: indexed streams and seek

What it is: a stream state exposes valid, a lower-bound index, a seek operation, readiness, and value. Unlike a sequential iterator, seek may skip keys irrelevant to a join. The paper states, “The essential difference with indexed streams [16] is that they are free to skip over values that are not relevant to the output of the computation.” (Section 4.1, p.6)

When to use: use it for ordered associative collections whose joins should avoid scanning keys absent from the result. Define index as a lower bound on the next key; define seek(q,(i,r)) to advance toward i, where the boolean r indicates whether the stream may advance past i as well as up to it (Section 4.1, p.6). The final Lean representation is a structure with valid, ready, index, seek, and value (Section 4.1, pp.6–7). Any sequential iterator can be wrapped as an indexed stream: its seek checks whether the current key lags the argument key (currentKey < i, or r && currentKey = i) and, if so, calls next once; the stream consumer calls seek repeatedly (Section 4.2.1, p.7). The paper notes this wrapper does not exploit fast lookup.

How to apply: (1) choose a state s and initial state q; (2) prove valid q before indexing; (3) return a lower-bound key from index; (4) implement seek so it makes adequate progress without changing emissions beyond the requested key (the paper says a seek need not reach the given index, only make adequate progress, Section 4.2.2, p.8); (5) return value only at a ready state. For sorted arrays, the paper’s sparseLinearIterator uses a natural-number state, bounds validity by q<n, compares the current key with (j,r), and advances to q+1 when needed (Section 4.2.2, p.8). For trees, seek performs an upward pass to a sufficiently large parent and a downward search for the successor (Section 4.2.3, pp.8–9; Rust code in Appendix A).

Verus form (inference): represent the stream as a Rust struct with fields for state and methods valid, index, seek, ready, and value; use requires to establish valid state and ensures to state monotonicity and preservation of values beyond the seek key. Verus does not provide Lean dependent subtypes, so validity proofs are explicit preconditions or ghost state. Do not use invariant(...) as a call; loop invariants belong on the while syntax.

Evidence and limits: the paper asks implementers to ensure monotonicity, strict monotonicity (sufficient for termination when the state space is finite), and lawfulness, so that streams can be joined or nested freely (Section 4.2.5, pp.9–10). Its lawfulness class requires index not to decrease and seek not to alter semantic evaluation at later indices (Section 6.1, p.15). Unordered streams have “limited composability”; the paper provides a memo operator that can collect an unordered stream into a structure supporting ordered traversal (Section 4.2.4, p.9). Runtime-generated or recursively hidden stream expressions cannot be optimized: “Our approach assumes that stream computations appear as static parts of the program text; they cannot be generated based on runtime values or hidden behind recursive function applications.” (Section 5.4, p.14)

technique 2: map/zipWith algebra and fused joins

What it is: expose map, zipWith, filter, fold, eval, and memo; define joins from these primitives. The paper gives intersect s1 s2 := zipWith (fun x y => x && y) s1 s2 and select m f := map f m (Section 1, p.2). This keeps the high-level expression while allowing one fused traversal.

How to apply (the steps are this study’s synthesis of the paper’s description): (1) encode each collection as k →ₛ v; (2) use map for element transformations; (3) use zipWith for key-aligned joins; (4) compose nested streams for hierarchical keys; (5) call eval or fold only at the boundary that materializes output. For sparse matrix multiplication, the paper writes eval (Σ j => a(i,j) * b(j,k)), then expands shapes with repeat, maps multiplication across three layers with nested zipWith, and eliminates the summation with nested fold update calls (Section 3.2, pp.4–5). The paper says eval “works out the minimal set of nested folds” automatically.

Verus form (inference): define Rust traits for stream combinators and implement each combinator as a struct carrying child streams and a closure. Use spec fn models for key/value semantics and prove each combinator’s ensures; implement materialization with a verified fold. Rust trait monomorphization can specialize these structs, but the Lean type-class proofs do not carry over directly.

Evidence: the authors report that stream code is one or two expressions while baselines range from 5–35 lines (Section 7.1, p.18). In the Rust triangle join benchmark, the paper reports “The speedup of 5x” for the unfused pairwise indexed-stream version (tri.unfused) over the naive iterate/lookup version, and “a speedup of about 20x” for the fused version (the text does not state the baseline of the 20x; Inference: it is the naive version); each relation has 20,000 string pairs (Section 7.2, p.19). Red-black-tree streaming (Rust) is “faster by about 2x” than traversing one tree and looking up in the others, for intersections of two or three trees of one million random integer keys each (Section 7.2, p.19). Rust was about 2x faster than Morphic in absolute terms; Lean results were less consistent (Section 7.1, p.19). These are averages of at least 100 single-threaded runs on an Intel i7-10710U with rustc 1.79, Lean 4.7.0, and Morphic at commit d692f4cdd/llvm 16 (Section 7, p.17). The paper concludes that indexed streams add “negligible overhead over the best baselines” on three microbenchmarks (Section 7.1, p.18).

technique 3: fold, Modifiable, and lawful data-structure adapters

fold is a tail-recursive loop that checks validity, updates the accumulator when ready, seeks onward, and terminates when invalid (Section 4.3.1, p.10). Modifiable.update incrementally changes the value at a key; OfStream.eval transforms stream values into a concrete collection. Nested streams use fold Modifiable.update ◦ map eval (Section 4.3.3, p.11). This is the paper’s reusable recipe for materializing arbitrarily nested joins.

Verus form (inference): verify a Rust fold with a loop invariant relating the accumulator to the semantic sum of already-consumed keys, and an ensures clause equating the result with the stream model. Prove an adapter’s update law (updating one key leaves other keys unchanged), then derive the OfStream law. Keep proof functions ghost-only; runtime functions must remain executable.

The paper’s semantic layer evaluates streams to finitely supported functions and proves combinators once independently of concrete collections (Section 6.3, p.16). It then requires LawfulOfStream and LawfulToStream commuting equations to connect concrete data structures to that semantics (Section 6.4, pp.16–17). The paper says end users “only have to trust the Lean compiler” for the Lean library (Section 6, p.15); it provides no mechanized Rust proof. Inference: for a Rust port the Rust compiler would also be trusted. Inference: VL can reuse the law-based adapter architecture, but must separately prove Rust implementations and compiler assumptions.

what VL should take and threat

Inference: indexed streams offer a direct pattern for verified Rust joins: prove stream laws once, then compose joins and folds with ghost semantic models. The main product threat is implementation complexity around ordered trees, nested folds, and compiler specialization; a generated verifier must preserve strict progress and lawful seek rather than merely produce plausible loop code. The paper already supplies a general-purpose library design, Lean proofs, and performance measurements, so VL should not redo a generic indexed-stream API without a Rust-specific proof and integration target.

techniques for the catalog

• indexed stream laws — expose lower-bound index, monotone lawful seek, readiness, and value to skip irrelevant keys safely
• fused map/zipWith joins — express associative-array transformations and joins as composable stream algebra with no intermediate materialization
• nested fold materialization — combine Modifiable.update with OfStream.eval to construct nested outputs from streams
• semantic adapter proofs — connect concrete collections to finitely supported-function semantics through commuting OfStream and ToStream laws Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Calls to trait methods are also monomorphized, and we use this to guarantee specialization of stream code by defining the fold function as a trait method.”): read the whole paper text and checked every quotation, number, section and page reference and the technique steps against it; changed the link (the DOI was reference [6]’s, replaced by arXiv:2507.06456), the description of wrapping sequential iterators (one next call per seek), the page of the red-black-tree result (p.19, not p.20), the wording on the 20x triangle speedup baseline, memo, strict monotonicity and the trusted-compiler claim, and added a few numbers and a quote; did not check the Verus-form inference paragraphs for technical validity, the Lean proof files (not read, only the paper’s description of them), or the benchmark figures’ plotted values (text extraction of the figures is unreadable).

Last edited: 2026-10-17