formal: relax the pending set to cover over-warning; intra-round compaction lemmas#779
Merged
frankmcsherry merged 2 commits intoJul 2, 2026
Conversation
…action lemmas Two generalizations matching the implementation more closely: * Step's pending_eq (exact) becomes pending_super/pending_confined/ pending_finite: the new pending set need only CONTAIN the deferred and carried times, staying beyond the frontier. reduce.rs warns about more times than the truncated closure defers (joins with already-finalized times kept "to scare future times"); over-warning is harmless, and the theorem now covers it. Step.of_pending_eq recovers the exact choice (TARGETS2.md step 4 as written), used by the scenarios. * acc_mapDomain_sup and sup_advance_eq: TARGETS2.md's join preservation, specialized to the one-element frontier used by reduce.rs's intra-round buffer compaction. Advancing buffer times by the meet of everything still to be examined changes no accumulation the round still reads and no join it still generates, so the intra-round compaction needs no adversary move at the model's granularity. No sorries; goal theorems unchanged and still depend only on the three standard axioms. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Four observations, separable from the Lean: the debt has no memory (compacted input + output determine it; the output is the receipt that makes re-derivation possible); debt is created only above the seeds; seeding on new times and closing against stored times IS the full join closure restricted to where debt can live (absorption); pends are resumption tokens for the suspended closure, carrying no other content. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two generalizations of the model in
formal/Differential/Model.lean, following up on #777. Both bring the model closer to whatreduce.rsactually does; neither changes the goal theorems, which remain proven with nosorryand only the three standard axioms.Relaxed pending set.
Step's exactpending_eqbecomes three fields: the new pending set must contain the deferred and carried times (pending_super), stay beyond the frontier (pending_confined), and be finite (pending_finite). The implementation warns about more times than the truncated closure defers — joins with already-finalized times it keeps around "to scare future times", and synthetic times from cancelled batch updates — and over-warning is harmless: a warned time that owes nothing evaluates to an empty correction when it comes due. The invariant proof only ever used one inclusion or the other, never exactness, so the change is mechanical;Step.of_pending_eqrecovers the exact choice (TARGETS2.md step 4 as originally written) and the sanity scenarios use it. TARGETS2.md gets a dated amendment note.Intra-round compaction is invisible.
reduce.rsalso compacts within a round, advancing its input and output buffers by the meet of every time still to be examined. Two lemmas (acc_mapDomain_sup,sup_advance_eq— TARGETS2.md's join preservation, specialized to a one-element frontier) say this is invisible at the model's granularity: the compacted buffer yields the same accumulation at every remaining evaluation point and the same join against every remaining seed as the uncompacted history would, so the intra-round compaction needs no adversary move at all.🤖 Generated with Claude Code