[flow analysis] Switch to associative promotion chain join. - #4771
Merged
Merged
Conversation
Changes the flow analysis spec so that the join of promotion chains is now specified to be the maximal common subsequence of the two inputs, as discussed in dart-lang#4757. Adjusts the Lean proofs to establish: - That a maximal common subsequence between any two promotion chains always exists. - That the maximal common subsequence is unique. This justifies calling it "the join" of the two promotion chains, but leaves open the question of how to compute it. - An equivalent procedural definition, based on filtering one chain and retaining those elements that are in the other. This establishes that the join operation is computable, though this definition is `O(m*n)` (where `m` and `n` are the lengths of the two chains); we will do better than that in the actual implementation. - That the new join operation is idempotent, commutative, and associative. I've also renamed several of the Lean theorems to better follow Mathlib conventions, and I've added some additional theorems that I believe will be useful in later proofs. In a follow-up PR, I plan to introduce a correctness proof for the optimized implementation in https://dart-review.googlesource.com/c/sdk/+/543721 (which is `O(m+n)` rather than `O(m*n)`, and avoids unnecessary list allocations).
lrhn
approved these changes
Sep 14, 2026
stereotype441
added a commit
to stereotype441/language
that referenced
this pull request
Sep 17, 2026
Adds a Lean model of the Dart method `PromotionModel.joinPromotedTypes` (as of SDK commit 5651b872ea36c3, with `promotionChainIntersectionJoinEnabled = true`), along with a proof that it computes the join of promotion chains specified in `flow-analysis.md`. This is the follow-up promised in dart-lang#4771: the spec defines the join of two promotion chains as their unique greatest common subsequence, and the Lean model backs that up with a filter-based definition establishing that the join is computable. But that definition is `O(m*n)` (where `m` and `n` are the lengths of the two chains), whereas the SDK uses an `O(m+n)` algorithm that also avoids unnecessary list allocations. This PR proves that the two agree. Details: - `FlowAnalysis/PromotionChain/JoinImpl.lean` contains `joinPromotedTypesImpl` and `joinPromotedTypesImpl'`, which model the Dart algorithm using Lean's imperative `do` notation, so that they track the structure of the Dart code as closely as possible (including the mutable loop indices, the two "advance" flags, and the lazily allocated `result` accumulator). - `joinPromotedTypesImpl_correct` uses Lean's weakest precondition framework (`Std.Do`) to prove that for all promotion chains `c₁` and `c₂`, the model terminates, returns `(c₁.join c₂).val`, and leaves the monadic state unchanged. The proof is by loop invariant; the invariant and the decreasing measure used to establish termination are spelled out in comments. - `FlowAnalysis/PromotionChain/Basic.lean` (renamed from `FlowAnalysis/PromotionChain.lean` to make room for the new file) gains the three recurrence relations for `join` that drive the correctness proof, covering the cases `T₁ = T₂`, `T₁ ≤ T₂`, and `¬T₁ ≤ T₂`. These correspond to the three branches of the loop body in the Dart implementation. - `FlowAnalysis/WP.lean` contains general purpose helpers for reasoning about monadic models of Dart code: `WP_ite` (which allows an `if/then/else` to be split without `simp` rewriting the surrounding monadic code into an unreadable form), `stateIs`, and a simp lemma for `SVal.curry`. - `DartTypeRepr` now extends `Inhabited` (and `SimpleType`'s default is `Never`), so that the models can use Lean's `xs[i]!` notation for list indexing, avoiding the need to clutter them with proofs that the indices are in range. TAG=agy CONV=a3f3022c-cb28-41fe-b867-ab2cdc117925
1 task
stereotype441
added a commit
that referenced
this pull request
Sep 18, 2026
…in. (#4776) Adds a Lean model of the Dart method `PromotionModel.joinPromotedTypes` (as of SDK CL https://dart-review.googlesource.com/c/sdk/+/551800), with `promotionChainIntersectionJoinEnabled = true`), along with a proof that it computes the join of promotion chains specified in `flow-analysis.md`. This is the follow-up promised in #4771: the spec defines the join of two promotion chains as their unique greatest common subsequence, and the Lean model backs that up with a filter-based definition establishing that the join is computable. But that definition is `O(m*n)` (where `m` and `n` are the lengths of the two chains), whereas the SDK uses an `O(m+n)` algorithm that also avoids unnecessary list allocations. This PR proves that the `O(m+n)` algorithm agrees with the other two definitions. Details: - `FlowAnalysis/PromotionChain/JoinImpl.lean` contains `joinPromotedTypesImpl` and `joinPromotedTypesImpl'`, which model the Dart algorithm using Lean's imperative `do` notation, so that they track the structure of the Dart code as closely as possible (including the mutable loop indices, the two "advance" flags, and the lazily allocated `result` accumulator). - `joinPromotedTypesImpl_correct` uses Lean's weakest precondition framework (`Std.Do`) to prove that for all promotion chains `c₁` and `c₂`, the model terminates, returns `(c₁.join c₂).val`, and leaves the monadic state unchanged. The proof is by loop invariant; the invariant and the decreasing measure used to establish termination are spelled out in comments. - `FlowAnalysis/PromotionChain/Basic.lean` (renamed from `FlowAnalysis/PromotionChain.lean` to make room for the new file) gains the three recurrence relations for `join` that drive the correctness proof, covering the cases `T₁ = T₂`, `T₁ ≤ T₂`, and `¬T₁ ≤ T₂`. These correspond to the three branches of the loop body in the Dart implementation. - `FlowAnalysis/WP.lean` contains general purpose helpers for reasoning about monadic models of Dart code: `WP_ite` (which allows an `if/then/else` to be split without `simp` rewriting the surrounding monadic code into an unreadable form), `stateIs`, and a simp lemma for `SVal.curry`. - `DartTypeRepr` now extends `Inhabited` (and `SimpleType`'s default is `Never`), so that the models can use Lean's `xs[i]!` notation for list indexing, avoiding the need to clutter them with proofs that the indices are in range.
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
2 participants
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.
Changes the flow analysis spec so that the join of promotion chains is now specified to be the greatest common subsequence of the two inputs, as discussed in #4757.
Adjusts the Lean proofs to establish:
That a greatest common subsequence between any two promotion chains always exists.
That the greatest common subsequence is unique. This justifies calling it "the join" of the two promotion chains, but leaves open the question of how to compute it.
An equivalent procedural definition, based on filtering one chain and retaining those elements that are in the other. This establishes that the join operation is computable, though this definition is
O(m*n)(wheremandnare the lengths of the two chains); we will do better than that in the actual implementation.That the new join operation is idempotent, commutative, and associative.
I've also renamed several of the Lean theorems to better follow Mathlib conventions, and I've added some additional theorems that I believe will be useful in later proofs.
In a follow-up PR, I plan to introduce a correctness proof for the optimized implementation in
https://dart-review.googlesource.com/c/sdk/+/543721 (which is
O(m+n)rather thanO(m*n), and avoids unnecessary list allocations).Contribution guidelines:
dart format.Many Dart repos have a weekly cadence for reviewing PRs - please allow for some latency before initial review feedback.
Note: The Dart team is trialing Gemini Code Assist. Don't take its comments as final Dart team feedback. Use the suggestions if they're helpful; otherwise, wait for a human reviewer.