Rewinding the Fold: Making Stateful Computations Retractable
Incremental computation seeks to maintain outputs efficiently as inputs evolve, without recomputing from scratch after every change. While much prior work has focused on updating results when new data arrive, supporting \emph{deletion} is fundamentally more difficult: once prior inputs have been folded into a compact summary, the information needed to undo their effect may already have been lost. This paper studies incremental deletion for fold-based stream computations. This setting captures a broad class of data-processing tasks, where a program maintains a running summary of a stream and uses that summary to process future inputs. Given a fold that supports only additions and a policy describing what type of deletion support is required, our method synthesizes a new program that supports deletions by extending the summary state and deriving both the addition and deletion logic. Our synthesis procedure is backed by a new verification framework that decomposes correctness into local obligations over relational invariants. As a result, for every supported sequence of additions and deletions, the synthesized fold is guaranteed to match what full recomputation would produce. We implemented this approach in a new tool called \textsc{Rewind} and evaluated it on 94 benchmark scenarios drawn from real-world aggregations in the Flink framework. \textsc{Rewind} synthesizes deletion support for all 94 benchmarks, including cases that contain bugs in the manually-written deletion implementation.