[frankmcsherry]

Replaces #981.

A trace's accumulations are correct only at or beyond its compaction frontier. A reader that starts after the trace has compacted must read every time advanced to a frontier since, as TraceFrontier does for a cursor. The proxy tactics hand batches to a backend, which reads times as stored.

int_proxy::frontier::BackendFrontier<B, T> wraps any proxy join or reduce backend over the same batch types. It reads what the backend draws as of since: Antichain<T>, advancing with Lattice::advance_by and consolidating what then coincides; in a join, a key that nets away on one side also leaves the other. The tactics, traits and instance types are unchanged.

The argument uses only the defining property of advance_by (for t' beyond since, t ≤ t' exactly when advance(t) ≤ t'), so it holds in any lattice, distributive or not:

• Units already beyond since are left alone, and that is exact. A join's output times are already beyond since, and a reduce evaluates only at times beyond its lower bound. This is the steady state, where the wrapper costs one antichain comparison per unit. Only the unit that reads a trace's history pays.
• The unit that reads history agrees with the as-of reading at every time beyond since. It is identical when since has one element, when the inner backend presents stored times, or when since is beyond the unit's bound.
• since must be beyond every frontier the trace compacted by. Reading as of the meet of a multi-element compaction frontier is not that, and is unsafe in a non-distributive lattice.

Tests

tests/int_proxy.rs checks the wrapper in two ways:

• u64 times: a history read through the wrapper, against the same tactic over the rows advanced by hand.
• The pentagon lattice N5, which is not distributive: the join and the reduce run through the wrapper for every frontier of one or two elements, every bound, and every placement of the records. The tests assert identical output wherever the argument promises it, and agreement beyond since otherwise. No case differed exactly. A brute-force search over 9.2 million configurations of small lattices found no exact difference either.

cargo test -p differential-dataflow passes. DDIR's use of it is the next PR.

🤖 Generated with Claude Code

https://claude.ai/code/session_019XsakwFGwtESwZ1gSYwG4o