[flow analysis] Prove correctness of the optimized promotion chain join.

[stereotype441]

Adds a Lean model of the Dart method PromotionModel.joinPromotedTypes (as of SDK CL 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.

• Since 551800 is still pending, this PR is split into two commits: b7d6810 models the current state of the SDK implementation (as of SDK commit dart-lang/sdk@503e5b5), and f36e48f adapts it to reflect 551800.

---

• I’ve reviewed the contributor guide and applied the relevant portions to this PR.

Contribution guidelines:

• See our contributor guide for general expectations for PRs.
• Larger or significant changes should be discussed in an issue before creating a PR.
• Contributions to our repos should follow the Dart style guide and use dart format.
• Most changes should add an entry to the changelog and may need to rev the pubspec package version.
• Changes to packages require corresponding tests.

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.

[chloestefantsova]

LGTM, given my current limitations as a lean reviewer we discussed during our meeting.