From d5b9081f0a833eadd8282dbc8004df4c83c2b405 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 3 Mar 2026 11:19:35 -0500
Subject: [PATCH 01/10] add plan

---
 PLAN.md | 467 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 467 insertions(+)
 create mode 100644 PLAN.md

diff --git a/PLAN.md b/PLAN.md
new file mode 100644
index 00000000000000..ca2d11941ce56c
--- /dev/null
+++ b/PLAN.md
@@ -0,0 +1,467 @@
+# Constraint-set support tracking and `source_order` removal plan
+
+## Goal
+
+Replace per-interior-node `source_order` tracking with per-constraint-set **support expression** tracking.
+
+The key design principle is:
+
+- During BDD construction, support handling should be **very cheap** (record support operations only).
+- Materialize concrete ordered support (`[ConstraintId]`) **lazily**, only when consumers need it.
+
+This should:
+
+1. Preserve stable, source-like ordering for diagnostics/solutions.
+2. Avoid dependence on global/builder-local `ConstraintId` numeric order.
+3. Enable future switch from quasi-reduced to fully reduced BDD nodes.
+4. Shift CPU work out of hot BDD ops into rarer support-consumption paths.
+
+---
+
+## Scope and staging
+
+- [ ] **Phase 1 (mechanical + behavior-preserving):**
+  - Introduce support-expression infrastructure.
+  - Thread support expressions through `ConstraintSet` operations.
+  - Keep existing node `source_order` fields temporarily.
+  - Add lazy flattening API and migrate consumers where practical.
+- [ ] **Phase 2 (cleanup):**
+  - Remove node-level `source_order`/`max_source_order`.
+  - Remove offset machinery (`*_with_offset`, `with_adjusted_source_order`, etc.).
+- [ ] **Phase 3 (optional follow-up):**
+  - Evaluate switching from quasi-reduced to fully reduced BDDs.
+
+This plan covers Phases 1 and 2.
+
+---
+
+## Data model changes
+
+### 1) Add support-expression IDs and storage
+
+In `crates/ty_python_semantic/src/types/constraints.rs`:
+
+- Add new index type:
+  - `#[newtype_index] struct UnionSupportId;`
+- Add a support-expression identifier enum:
+
+```rust
+enum SupportId {
+    Empty,
+    Singleton(ConstraintId),
+    OrderedUnion(UnionSupportId),
+    // Quantification/abstraction support transform node (details below)
+    Quantified(QuantifiedSupportId),
+}
+```
+
+(Exact naming may vary; `SupportId` can remain module-private.)
+
+```rust
+struct UnionSupportData {
+    lhs: SupportId,
+    rhs: SupportId,
+}
+```
+
+- Extend `ConstraintSetStorage` with:
+  - `union_supports: IndexVec<UnionSupportId, UnionSupportData>`
+  - `quantified_supports: IndexVec<QuantifiedSupportId, QuantifiedSupportData>`
+
+Important initial policy:
+
+- **Do not hash-cons any support-expression nodes** in Phase 1 (including `OrderedUnion` and `Quantified`/quantified nodes).
+- Always append fresh support-expression nodes as operations are recorded.
+
+### 2) Quantification/derived-support node
+
+For existential abstraction and related flows, add a support node kind that records:
+
+- base support expression,
+- removed constraints,
+- derived constraints tied to origin constraints (rank provenance),
+- optional encounter index if needed to stabilize ties.
+
+Proposed payload sketch:
+
+```rust
+struct QuantifiedSupportData {
+    base: SupportId,
+    removed: Box<[ConstraintId]>,
+    derived: Box<[DerivedConstraintRecord]>,
+}
+
+struct DerivedConstraintRecord {
+    origin: ConstraintId,
+    derived: ConstraintId,
+}
+```
+
+Note:
+
+- We may later flatten/simplify `QuantifiedSupportData` and/or `DerivedConstraintRecord` if profiling or implementation experience suggests it.
+
+Invariant:
+
+- Every `origin` used in `derived` **must** appear in the flattened base support (after removals are interpreted per algorithm). If not, treat as programmer error and **hard panic**.
+
+### 3) Make support expression explicit on `ConstraintSet`
+
+- `ConstraintSet` gains `support: SupportId`.
+- `OwnedConstraintSet` stores **materialized** support:
+  - `support: Box<[ConstraintId]>`
+
+`ConstraintSet::from_node` becomes `from_node_and_support(...)`.
+
+---
+
+## Support-expression operations
+
+### 4) Builder helpers
+
+Add methods on `ConstraintSetBuilder`:
+
+- constructors:
+  - `empty_support() -> SupportId`
+  - `singleton_support(c: ConstraintId) -> SupportId`
+  - `ordered_union_support(lhs: SupportId, rhs: SupportId) -> SupportId`
+  - `quantified_support(data: QuantifiedSupportData) -> SupportId`
+
+- flattening/materialization:
+  - `flatten_support(expr: SupportId) -> Box<[ConstraintId]>`
+
+`flatten_support` behavior:
+
+- uses an `FxIndexSet<ConstraintId>` accumulator (type alias over `indexmap::IndexSet`),
+- iterative traversal (no recursive stack growth risk),
+- `OrderedUnion`: flatten lhs then rhs (graph structure defines ordering),
+- dedupe comes from `FxIndexSet` insertion semantics (first occurrence wins),
+- deterministic order,
+- `Quantified`: apply explicit remove/derive operations over the accumulator.
+
+Implementation notes:
+
+- Keep flatten semantics centralized in this one method; each support node maps to a clear accumulator operation.
+- `flatten_support` should rely on `FxIndexSet` for dedupe and order (no bespoke mark/epoch dedupe logic in this path).
+
+### 5) Support creation rules
+
+- Atomic single-constraint set: singleton support.
+- `always` / `never`: empty support.
+- `union` / `intersect` / `iff` / `implies`: record ordered-union support node (`lhs`, `rhs`) only.
+- `negate`: support unchanged.
+- existential/reduction operations:
+  - record a `Quantified` support transform node; do not eagerly compute flattened order.
+
+---
+
+## Thread support through APIs
+
+### 6) Constructors and conversions
+
+Update:
+
+- `ConstraintSet::always/never/from_bool/constrain_typevar/...`
+- `ConstraintSetBuilder::into_owned` and `load`
+
+Rules:
+
+- `into_owned` materializes flattened support and stores `Box<[ConstraintId]>`.
+- `load` remaps stored support constraints through remapped `ConstraintId`s and rebuilds support expression as a left-associated chain of singleton `OrderedUnion` nodes.
+
+### 7) Combinators
+
+Update all combinators to compose support expressions without flattening:
+
+- `union`, `intersect`, `and`, `or`, `implies`, `iff`, `negate`
+- quantification/restriction methods (`reduce_inferable`, `retain_non_inferable`, etc.)
+
+Audit all `ConstraintSet::from_node(...)` sites and convert to support-aware constructor.
+
+---
+
+## Migrate consumers from `source_order` to flattened support rank
+
+### 8) Path and solution ordering
+
+Replace per-node `source_order` sorting with support-rank sorting:
+
+- Build `constraint -> rank` map from `flatten_support(constraint_set.support)`.
+- Sort positives by rank (stable; ties should not normally occur once rank map is built from flattened support).
+
+Apply to:
+
+- `NodeId::solutions`
+- display/simplification code currently sorting by `source_order`
+
+### 9) Simplification and quantification behavior
+
+In abstraction/simplification flows:
+
+- stop synthesizing/propagating node `source_order` values.
+- represent derived-support semantics via `Quantified` support node.
+
+For relative ordering among derived constraints from the same origin:
+
+- use support-graph structure (construction order of support nodes) as the tie-breaker.
+- do not add extra tie-break metadata initially.
+
+### 10) `PathAssignments`
+
+Current `FxIndexMap<ConstraintAssignment, usize>` may remain initially.
+
+- reinterpret `usize` as support rank when populated from flattened support.
+- do not assume rank originates from interior-node metadata.
+
+---
+
+## Remove `source_order` from nodes (Phase 2)
+
+### 11) Interior node shape
+
+Remove from `InteriorNodeData`:
+
+- `source_order`
+- `max_source_order`
+
+Update `Node::new`, `new_constraint`, `new_satisfied_constraint` signatures.
+
+### 12) Remove offset machinery
+
+Delete/replace:
+
+- `with_adjusted_source_order`
+- `max_source_order`
+- `or_with_offset`, `and_with_offset`, `iff_with_offset`
+- cache key dimensions based on `other_offset`
+
+Use normal binary ops at BDD layer; support ordering comes from support expression graph.
+
+### 13) Update docs/comments
+
+Replace references to node-level source-order with support-expression + flatten semantics.
+
+---
+
+## Fully reduced BDD follow-up (Phase 3)
+
+### 14) Toggle reduction behavior
+
+After support migration lands:
+
+- evaluate removing quasi-reduction exception that preserves redundant nodes,
+- benchmark and validate output stability.
+
+Keep as separate PR/commit.
+
+---
+
+## Testing strategy
+
+### 15) Unit tests in `constraints.rs`
+
+Add tests for:
+
+- flatten of ordered-union chains preserves lhs-first semantics,
+- dedupe with first occurrence winning,
+- deterministic flatten for deep trees,
+- deterministic flatten behavior for large/deep support graphs,
+- `Quantified` semantics (remove + derive + tie behavior),
+- panic path when derived origin is missing,
+- `into_owned`/`load` support remap.
+
+### 16) Existing tests
+
+Run focused tests first:
+
+- `cargo nextest run -p ty_python_semantic`
+- mdtests as needed:
+  - `cargo nextest run -p ty_python_semantic --test mdtest -- mdtest::<path>`
+
+Then broader checks per repo conventions.
+
+---
+
+## Performance validation
+
+### 17) Instrumentation and sanity checks
+
+Collect before/after metrics:
+
+- support-expression node counts (`OrderedUnion`, `Quantified`),
+- flattened support lengths at consumption sites,
+- flatten invocation counts,
+- wall time in representative mdtests/code-nav runs,
+- memory impact from non-hash-consed support-expression nodes.
+
+Implementation note:
+
+- add lightweight temporary counters for this validation, and remove them from final landed code unless we decide to keep them as permanent diagnostics.
+
+Expectation:
+
+- lower CPU in BDD construction/hot combinators,
+- potentially higher memory and flatter-consume cost.
+
+---
+
+## Risks and mitigations
+
+1. **Support-expression tree growth (memory)**
+   - Mitigation: intentional Phase-1 tradeoff; measure and revisit with optional memo/hash-consing later.
+2. **Flatten correctness subtleties**
+   - Mitigation: single `flatten_support` implementation + strong unit tests.
+3. **Ordering drift in diagnostics/snapshots**
+   - Mitigation: all ordering consumers rely on flattened rank map.
+4. **Quantification provenance bugs**
+   - Mitigation: explicit invariants; panic on missing origin; dedicated tests.
+5. **Repeated flatten overhead in some paths**
+   - Mitigation: measure with temporary counters; consider flatten memoization follow-up if needed.
+
+---
+
+## Concrete implementation checklist
+
+- [ ] Add `SupportId`, `UnionSupportId`, `QuantifiedSupportId` and storage tables.
+- [ ] Add support-expression constructors on builder (no support-node hash-consing).
+- [ ] Add `flatten_support` with iterative traversal + `FxIndexSet` accumulator dedupe.
+- [ ] Add `support` to `ConstraintSet` and flattened support payload to `OwnedConstraintSet`.
+- [ ] Thread support expressions through constructors/combinators.
+- [ ] Encode abstraction-derived ordering via `Quantified` support node.
+- [ ] Convert ordering consumers to flattened support rank maps.
+- [ ] Remove node `source_order` fields and offset APIs.
+- [ ] Run tests and update snapshots if needed.
+
+---
+
+## Execution order with concrete code touchpoints
+
+### Step A — add support-expression IDs and storage
+
+File: `crates/ty_python_semantic/src/types/constraints.rs`
+
+1. Add `UnionSupportId` and `QuantifiedSupportId` (`#[newtype_index]`).
+2. Add `SupportId` enum (`Empty`, `Singleton`, `OrderedUnion`, `Quantified`).
+3. Extend `ConstraintSetStorage` with:
+   - `union_supports: IndexVec<UnionSupportId, UnionSupportData>`
+   - `quantified_supports: IndexVec<QuantifiedSupportId, QuantifiedSupportData>`
+4. If needed, add lightweight scratch state for iterative flatten traversal (e.g., reusable explicit stack buffers).
+
+### Step B — builder APIs and flatten implementation
+
+File: `crates/ty_python_semantic/src/types/constraints.rs`
+
+1. Add support constructors (`empty`, `singleton`, `ordered_union`, `quantified`).
+2. Implement `flatten_support(expr) -> Box<[ConstraintId]>`:
+   - iterative walk,
+   - `FxIndexSet` accumulator for dedupe/order,
+   - deterministic lhs-before-rhs.
+3. Implement clear per-node accumulator operations (`Empty`, `Singleton`, `OrderedUnion`, `Quantified`).
+4. Add/adjust reusable traversal scratch only if profiling indicates allocation churn in flatten.
+
+### Step C — thread support through structs and constructors
+
+File: `crates/ty_python_semantic/src/types/constraints.rs`
+
+1. Add `support: SupportId` to `ConstraintSet`.
+2. Add `support: Box<[ConstraintId]>` to `OwnedConstraintSet`.
+3. Replace `from_node` with `from_node_and_support`.
+4. Update `always`, `never`, `from_bool`, atomic constructors.
+
+### Step D — update `into_owned` / `load`
+
+File: `crates/ty_python_semantic/src/types/constraints.rs`
+
+1. `into_owned`: flatten and persist support list.
+2. `load`: remap persisted support constraints and rebuild support expression.
+
+### Step E — combinator updates
+
+File: `crates/ty_python_semantic/src/types/constraints.rs`
+
+Update first:
+
+- `union`, `intersect`, `and`, `or`, `implies`, `iff`, `negate`
+
+Rule:
+
+- binary ops create `ordered_union_support(lhs.support, rhs.support)`
+- unary negate keeps support unchanged.
+
+Then audit all remaining `from_node(...)` sites.
+
+### Step F — quantification support node wiring
+
+File: `crates/ty_python_semantic/src/types/constraints.rs`
+
+1. In abstraction/reduction flows, build `Quantified` support nodes rather than eagerly computing ranks.
+2. Record origins and derived constraints; rely on support-graph structure for relative ordering.
+3. Enforce invariant that origins must be present at flatten time (hard panic otherwise).
+
+### Step G — migrate ordering consumers
+
+File: `crates/ty_python_semantic/src/types/constraints.rs`
+
+1. `NodeId::solutions` sorting.
+2. `NodeId::path_assignments` ordering logic.
+3. Any other display/simplify sorting based on `source_order`.
+
+Pattern:
+
+- flatten support once for the set,
+- build rank map,
+- sort by rank then `ConstraintId` fallback.
+
+### Step H — remove source-order fields and offset APIs (Phase 2)
+
+File: `crates/ty_python_semantic/src/types/constraints.rs`
+
+1. Remove `source_order` / `max_source_order` from node data.
+2. Remove `with_adjusted_source_order` and `*_with_offset` APIs + cache keys.
+3. Update all call sites.
+
+### Step I — tests and verification
+
+1. Add/adjust support tests.
+2. Run:
+   - `cargo nextest run -p ty_python_semantic`
+3. Snapshot accept if needed:
+   - `cargo insta accept`
+
+---
+
+## Persisted context / handoff notes
+
+### Confirmed design decisions
+
+1. Support construction should be cheap; defer support calculation until needed.
+2. No support-expression nodes are **hash-consed** in Phase 1 (`OrderedUnion` and `Quantified`/quantified included).
+3. Flattening is centralized in builder (`flatten_support`) and uses an `FxIndexSet<ConstraintId>` accumulator.
+4. `OwnedConstraintSet` persists flattened support, not support-expression graph.
+5. `load` rebuilds support as a left-associated `OrderedUnion` chain of singleton nodes.
+6. Missing origin for derived support is a programmer error (hard panic).
+7. Relative ordering/tie-breaking comes from support-graph structure; no extra tie-break metadata initially.
+
+### Invariants to preserve
+
+For any materialized support list from `flatten_support`:
+
+- each `ConstraintId` appears at most once,
+- ordering is deterministic,
+- ordered union is lhs-first,
+- derived constraints honor origin-rank semantics.
+
+### Suggested quick greps
+
+- `rg -n "ConstraintSetBuilder|ConstraintSetStorage|ConstraintSet::from_node|OwnedConstraintSet|into_owned\(|load\(" crates/ty_python_semantic/src/types/constraints.rs`
+- `rg -n "source_order|max_source_order|_with_offset|other_offset|with_adjusted_source_order" crates/ty_python_semantic/src/types/constraints.rs`
+- `rg -n "solutions\(|path_assignments\(|positive_constraints\(" crates/ty_python_semantic/src/types/constraints.rs`
+
+---
+
+## Notes
+
+- Keep semantic churn minimal in Phase 1: support-expression recording + lazy flatten.
+- Keep fully reduced BDD work separate after migration stabilizes.
+- Keep support-expression ID types private to `constraints.rs`.
+- Consider flatten memoization only if profiling indicates repeated-flatten overhead.

From caeec5de65afdaddc0b83fcbbd79a3c152d73249 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 3 Mar 2026 13:02:07 -0500
Subject: [PATCH 02/10] construct supports cheaply

---
 PLAN.md                                       |  40 +-
 .../src/types/constraints.rs                  | 365 ++++++++++++++----
 2 files changed, 312 insertions(+), 93 deletions(-)

diff --git a/PLAN.md b/PLAN.md
index ca2d11941ce56c..d628a6eef5245d 100644
--- a/PLAN.md
+++ b/PLAN.md
@@ -128,9 +128,9 @@ Add methods on `ConstraintSetBuilder`:
   - `quantified_support(data: QuantifiedSupportData) -> SupportId`
 
 - flattening/materialization:
-  - `flatten_support(expr: SupportId) -> Box<[ConstraintId]>`
+  - `build_support(expr: SupportId) -> Box<[ConstraintId]>`
 
-`flatten_support` behavior:
+`build_support` behavior:
 
 - uses an `FxIndexSet<ConstraintId>` accumulator (type alias over `indexmap::IndexSet`),
 - iterative traversal (no recursive stack growth risk),
@@ -142,7 +142,7 @@ Add methods on `ConstraintSetBuilder`:
 Implementation notes:
 
 - Keep flatten semantics centralized in this one method; each support node maps to a clear accumulator operation.
-- `flatten_support` should rely on `FxIndexSet` for dedupe and order (no bespoke mark/epoch dedupe logic in this path).
+- `build_support` should rely on `FxIndexSet` for dedupe and order (no bespoke mark/epoch dedupe logic in this path).
 
 ### 5) Support creation rules
 
@@ -186,7 +186,7 @@ Audit all `ConstraintSet::from_node(...)` sites and convert to support-aware con
 
 Replace per-node `source_order` sorting with support-rank sorting:
 
-- Build `constraint -> rank` map from `flatten_support(constraint_set.support)`.
+- Build `constraint -> rank` map from `build_support(constraint_set.support)`.
 - Sort positives by rank (stable; ties should not normally occur once rank map is built from flattened support).
 
 Apply to:
@@ -310,7 +310,7 @@ Expectation:
 1. **Support-expression tree growth (memory)**
    - Mitigation: intentional Phase-1 tradeoff; measure and revisit with optional memo/hash-consing later.
 2. **Flatten correctness subtleties**
-   - Mitigation: single `flatten_support` implementation + strong unit tests.
+   - Mitigation: single `build_support` implementation + strong unit tests.
 3. **Ordering drift in diagnostics/snapshots**
    - Mitigation: all ordering consumers rely on flattened rank map.
 4. **Quantification provenance bugs**
@@ -322,15 +322,17 @@ Expectation:
 
 ## Concrete implementation checklist
 
-- [ ] Add `SupportId`, `UnionSupportId`, `QuantifiedSupportId` and storage tables.
-- [ ] Add support-expression constructors on builder (no support-node hash-consing).
-- [ ] Add `flatten_support` with iterative traversal + `FxIndexSet` accumulator dedupe.
-- [ ] Add `support` to `ConstraintSet` and flattened support payload to `OwnedConstraintSet`.
-- [ ] Thread support expressions through constructors/combinators.
+- [x] Add `SupportId`, `UnionSupportId`, `QuantifiedSupportId` and storage tables.
+- [x] Add support-expression constructors on builder (no support-node hash-consing).
+- [x] Add `build_support` with `FxIndexSet` accumulator dedupe.
+- [x] Add `support` to `ConstraintSet` and flattened support payload to `OwnedConstraintSet`.
+- [x] Thread support expressions through constructors/combinators.
+- [ ] Update `distributed_or`/`distributed_and` and `when_any`/`when_all` to combine support in balanced-tree order.
+- [ ] Remove temporary `support_from_node` reconstruction path entirely.
 - [ ] Encode abstraction-derived ordering via `Quantified` support node.
 - [ ] Convert ordering consumers to flattened support rank maps.
 - [ ] Remove node `source_order` fields and offset APIs.
-- [ ] Run tests and update snapshots if needed.
+- [x] Run tests and update snapshots if needed.
 
 ---
 
@@ -352,7 +354,7 @@ File: `crates/ty_python_semantic/src/types/constraints.rs`
 File: `crates/ty_python_semantic/src/types/constraints.rs`
 
 1. Add support constructors (`empty`, `singleton`, `ordered_union`, `quantified`).
-2. Implement `flatten_support(expr) -> Box<[ConstraintId]>`:
+2. Implement `build_support(expr) -> Box<[ConstraintId]>`:
    - iterative walk,
    - `FxIndexSet` accumulator for dedupe/order,
    - deterministic lhs-before-rhs.
@@ -390,6 +392,14 @@ Rule:
 
 Then audit all remaining `from_node(...)` sites.
 
+### Step E.1 — restore balanced iterator combining and carry support through it
+
+File: `crates/ty_python_semantic/src/types/constraints.rs`
+
+- Keep `when_any`/`when_all` using `NodeId::distributed_or` / `NodeId::distributed_and` (balanced tree fold behavior).
+- Add support-aware equivalents of distributed folding so support is combined in the same balanced shape (instead of reconstructing via `support_from_node`).
+- `support_from_node` is a strict temporary migration bridge and **must be removed** before final landing.
+
 ### Step F — quantification support node wiring
 
 File: `crates/ty_python_semantic/src/types/constraints.rs`
@@ -436,15 +446,17 @@ File: `crates/ty_python_semantic/src/types/constraints.rs`
 
 1. Support construction should be cheap; defer support calculation until needed.
 2. No support-expression nodes are **hash-consed** in Phase 1 (`OrderedUnion` and `Quantified`/quantified included).
-3. Flattening is centralized in builder (`flatten_support`) and uses an `FxIndexSet<ConstraintId>` accumulator.
+3. Flattening is centralized in builder (`build_support`) and uses an `FxIndexSet<ConstraintId>` accumulator.
 4. `OwnedConstraintSet` persists flattened support, not support-expression graph.
 5. `load` rebuilds support as a left-associated `OrderedUnion` chain of singleton nodes.
 6. Missing origin for derived support is a programmer error (hard panic).
 7. Relative ordering/tie-breaking comes from support-graph structure; no extra tie-break metadata initially.
+8. `support_from_node` is temporary-only and must not remain in the final implementation.
+9. Rationale for (8): support is being separated from BDD structure specifically so we can eventually move to fully reduced BDDs, where node shape cannot be relied on to reconstruct support.
 
 ### Invariants to preserve
 
-For any materialized support list from `flatten_support`:
+For any materialized support list from `build_support`:
 
 - each `ConstraintId` appears at most once,
 - ordering is deterministic,
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index f202659367add9..6b6421cb8b2722 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -182,7 +182,9 @@ where
                 constraint.node
             }),
         );
-        ConstraintSet::from_node(builder, node)
+        // TEMPORARY: support reconstruction from BDD nodes must be removed before finalizing
+        // support migration.
+        ConstraintSet::from_node_and_support(builder, node, builder.support_from_node(node))
     }
 
     fn when_all<'db, 'c>(
@@ -200,7 +202,9 @@ where
                 constraint.node
             }),
         );
-        ConstraintSet::from_node(builder, node)
+        // TEMPORARY: support reconstruction from BDD nodes must be removed before finalizing
+        // support migration.
+        ConstraintSet::from_node_and_support(builder, node, builder.support_from_node(node))
     }
 }
 
@@ -226,6 +230,9 @@ pub struct OwnedConstraintSet<'db> {
     /// The nodes arena for this BDD. This is extracted from the [`ConstraintSetBuilder`] when an
     /// owned constraint set is constructed.
     nodes: IndexVec<NodeId, InteriorNodeData>,
+
+    /// Materialized support for this constraint set, in deterministic order.
+    support: Box<[ConstraintId]>,
 }
 
 /// A set of constraints under which a type property holds.
@@ -243,6 +250,9 @@ pub struct ConstraintSet<'db, 'c> {
     /// The BDD representing this constraint set
     node: NodeId,
 
+    /// Support expression for this constraint set.
+    support: SupportId,
+
     /// A reference to the builder that holds the storage for this constraint set's BDD
     builder: &'c ConstraintSetBuilder<'db>,
 
@@ -251,20 +261,25 @@ pub struct ConstraintSet<'db, 'c> {
 }
 
 impl<'db, 'c> ConstraintSet<'db, 'c> {
-    fn from_node(builder: &'c ConstraintSetBuilder<'db>, node: NodeId) -> Self {
+    fn from_node_and_support(
+        builder: &'c ConstraintSetBuilder<'db>,
+        node: NodeId,
+        support: SupportId,
+    ) -> Self {
         Self {
             node,
+            support,
             builder,
             _invariant: PhantomData,
         }
     }
 
     fn never(builder: &'c ConstraintSetBuilder<'db>) -> Self {
-        Self::from_node(builder, ALWAYS_FALSE)
+        Self::from_node_and_support(builder, ALWAYS_FALSE, SupportId::Empty)
     }
 
     fn always(builder: &'c ConstraintSetBuilder<'db>) -> Self {
-        Self::from_node(builder, ALWAYS_TRUE)
+        Self::from_node_and_support(builder, ALWAYS_TRUE, SupportId::Empty)
     }
 
     pub(crate) fn from_bool(builder: &'c ConstraintSetBuilder<'db>, b: bool) -> Self {
@@ -283,10 +298,8 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         lower: Type<'db>,
         upper: Type<'db>,
     ) -> Self {
-        Self::from_node(
-            builder,
-            Constraint::new_node(db, builder, typevar, lower, upper),
-        )
+        let (node, support) = Constraint::new_node_with_support(db, builder, typevar, lower, upper);
+        Self::from_node_and_support(builder, node, support)
     }
 
     /// Verifies that this constraint set was created by `builder`
@@ -425,7 +438,10 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         rhs: Type<'db>,
     ) -> Self {
         self.verify_builder(builder);
-        Self::from_node(builder, self.node.implies_subtype_of(db, builder, lhs, rhs))
+        let node = self.node.implies_subtype_of(db, builder, lhs, rhs);
+        // TEMPORARY: support reconstruction from BDD nodes must be removed before finalizing
+        // support migration.
+        Self::from_node_and_support(builder, node, builder.support_from_node(node))
     }
 
     /// Returns whether this constraint set is satisfied by all of the typevars that it mentions.
@@ -464,6 +480,7 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
     ) -> Self {
         self.verify_builder(builder);
         self.node = self.node.or_with_offset(builder, other.node);
+        self.support = builder.ordered_union_support(self.support, other.support);
         *self
     }
 
@@ -479,13 +496,14 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
     ) -> Self {
         self.verify_builder(builder);
         self.node = self.node.and_with_offset(builder, other.node);
+        self.support = builder.ordered_union_support(self.support, other.support);
         *self
     }
 
     /// Returns the negation of this constraint set.
     pub(crate) fn negate(self, _db: &'db dyn Db, builder: &'c ConstraintSetBuilder<'db>) -> Self {
         self.verify_builder(builder);
-        Self::from_node(builder, self.node.negate(builder))
+        Self::from_node_and_support(builder, self.node.negate(builder), self.support)
     }
 
     /// Returns the intersection of this constraint set and another. The other constraint set is
@@ -554,7 +572,9 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         other: Self,
     ) -> Self {
         self.verify_builder(builder);
-        Self::from_node(builder, self.node.iff_with_offset(builder, other.node))
+        let node = self.node.iff_with_offset(builder, other.node);
+        let support = builder.ordered_union_support(self.support, other.support);
+        Self::from_node_and_support(builder, node, support)
     }
 
     /// Reduces the set of inferable typevars for this constraint set. You provide an iterator of
@@ -569,7 +589,13 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         to_remove: impl IntoIterator<Item = BoundTypeVarIdentity<'db>>,
     ) -> Self {
         self.verify_builder(builder);
-        Self::from_node(builder, self.node.exists(db, builder, to_remove))
+        let node = self.node.exists(db, builder, to_remove);
+        let support = builder.quantified_support(QuantifiedSupportData {
+            base: self.support,
+            removed: Box::default(),
+            derived: Box::default(),
+        });
+        Self::from_node_and_support(builder, node, support)
     }
 
     pub(crate) fn solutions(
@@ -585,7 +611,7 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
             return Solutions::Unsatisfiable;
         }
 
-        self.node.solutions(db, builder)
+        self.node.solutions(db, builder, self.support)
     }
 
     #[expect(dead_code)] // Keep this around for debugging purposes
@@ -662,6 +688,12 @@ struct ConstraintSetStorage<'db> {
     /// The BDD nodes that appear in any of the constraint sets constructed in this builder.
     nodes: IndexVec<NodeId, InteriorNodeData>,
 
+    /// Support expression nodes that represent ordered unions of supports.
+    union_supports: IndexVec<UnionSupportId, UnionSupportData>,
+
+    /// Support expression nodes that represent quantified support transforms.
+    quantified_supports: IndexVec<QuantifiedSupportId, QuantifiedSupportData>,
+
     // Everything below are the memoization tables for the arenas and for our BDD operations.
     constraint_cache: FxHashMap<Constraint<'db>, ConstraintId>,
     typevar_cache: FxHashMap<BoundTypeVarIdentity<'db>, TypeVarId>,
@@ -700,11 +732,13 @@ impl<'db> ConstraintSetBuilder<'db> {
         // the original builder aren't relevant to the new builder, and don't need to be retained.
         let constraint = f(&self);
         let node = constraint.node;
+        let support = self.build_support(constraint.support);
         let storage = self.storage.into_inner();
         OwnedConstraintSet {
             node,
             constraints: storage.constraints,
             nodes: storage.nodes,
+            support,
         }
     }
 
@@ -757,7 +791,19 @@ impl<'db> ConstraintSetBuilder<'db> {
         // Maps NodeIds in the OwnedConstraintSet to the corresponding NodeIds in this builder.
         let mut cache = FxHashMap::default();
         let node = rebuild_node(db, self, other, &mut cache, other.node);
-        ConstraintSet::from_node(self, node)
+
+        let support =
+            other
+                .support
+                .iter()
+                .copied()
+                .fold(SupportId::Empty, |support, old_constraint| {
+                    let old_constraint_data = other.constraints[old_constraint];
+                    let remapped_constraint = self.intern_constraint(db, old_constraint_data);
+                    self.ordered_union_support(support, SupportId::Singleton(remapped_constraint))
+                });
+
+        ConstraintSet::from_node_and_support(self, node, support)
     }
 
     /// Interns a single typevar, giving it a stable order in this builder
@@ -863,6 +909,109 @@ impl<'db> ConstraintSetBuilder<'db> {
     fn interior_node_data(&self, node: NodeId) -> InteriorNodeData {
         self.storage.borrow().nodes[node]
     }
+
+    fn union_support_data(&self, support: UnionSupportId) -> UnionSupportData {
+        self.storage.borrow().union_supports[support]
+    }
+
+    fn quantified_support_data(
+        &self,
+        support: QuantifiedSupportId,
+    ) -> Ref<'_, QuantifiedSupportData> {
+        Ref::map(self.storage.borrow(), |storage| {
+            &storage.quantified_supports[support]
+        })
+    }
+
+    fn ordered_union_support(&self, lhs: SupportId, rhs: SupportId) -> SupportId {
+        match (lhs, rhs) {
+            (SupportId::Empty, rhs) => rhs,
+            (lhs, SupportId::Empty) => lhs,
+            (lhs, rhs) => {
+                let mut storage = self.storage.borrow_mut();
+                let id = storage.union_supports.push(UnionSupportData { lhs, rhs });
+                SupportId::OrderedUnion(id)
+            }
+        }
+    }
+
+    fn quantified_support(&self, data: QuantifiedSupportData) -> SupportId {
+        let mut storage = self.storage.borrow_mut();
+        let id = storage.quantified_supports.push(data);
+        SupportId::Quantified(id)
+    }
+
+    /// TEMPORARY MIGRATION HELPER.
+    ///
+    /// Reconstructs a support expression from the current BDD node shape by walking constraints
+    /// and ordering them by node `source_order`.
+    ///
+    /// This method **must not** remain in the final implementation. One of the goals of this
+    /// migration is to allow fully reduced BDDs, where the node graph is no longer required to
+    /// retain all constraints that contribute to support ordering. In that world, BDD structure
+    /// and support are intentionally decoupled, so support cannot be reconstructed from nodes.
+    fn support_from_node(&self, node: NodeId) -> SupportId {
+        let mut constraints: SmallVec<[_; 8]> = SmallVec::new();
+        node.for_each_constraint(self, &mut |constraint, source_order| {
+            constraints.push((constraint, source_order));
+        });
+        constraints.sort_unstable_by_key(|(_, source_order)| *source_order);
+        constraints
+            .into_iter()
+            .map(|(constraint, _)| SupportId::Singleton(constraint))
+            .fold(SupportId::Empty, |lhs, rhs| {
+                self.ordered_union_support(lhs, rhs)
+            })
+    }
+
+    fn build_support(&self, support: SupportId) -> Box<[ConstraintId]> {
+        fn build_into(
+            builder: &ConstraintSetBuilder<'_>,
+            support: SupportId,
+            constraints: &mut FxIndexSet<ConstraintId>,
+        ) {
+            match support {
+                SupportId::Empty => {}
+                SupportId::Singleton(constraint) => {
+                    constraints.insert(constraint);
+                }
+                SupportId::OrderedUnion(union_support) => {
+                    let union_support = builder.union_support_data(union_support);
+                    build_into(builder, union_support.lhs, constraints);
+                    build_into(builder, union_support.rhs, constraints);
+                }
+                SupportId::Quantified(quantified_support) => {
+                    let quantified_support = builder.quantified_support_data(quantified_support);
+
+                    let mut quantified_constraints = FxIndexSet::default();
+                    build_into(
+                        builder,
+                        quantified_support.base,
+                        &mut quantified_constraints,
+                    );
+
+                    for removed in &quantified_support.removed {
+                        quantified_constraints.shift_remove(removed);
+                    }
+
+                    for derived in &quantified_support.derived {
+                        assert!(
+                            quantified_constraints.contains(&derived.origin),
+                            "derived support origin {origin:?} not present in flattened quantified support",
+                            origin = derived.origin,
+                        );
+                        quantified_constraints.insert(derived.derived);
+                    }
+
+                    constraints.extend(quantified_constraints);
+                }
+            }
+        }
+
+        let mut constraints = FxIndexSet::default();
+        build_into(self, support, &mut constraints);
+        constraints.into_iter().collect()
+    }
 }
 
 impl<'db> BoundTypeVarInstance<'db> {
@@ -908,6 +1057,41 @@ pub struct TypeVarId;
 #[derive(salsa::Update, get_size2::GetSize)]
 pub struct ConstraintId;
 
+#[newtype_index]
+#[derive(salsa::Update, get_size2::GetSize)]
+struct UnionSupportId;
+
+#[newtype_index]
+#[derive(salsa::Update, get_size2::GetSize)]
+struct QuantifiedSupportId;
+
+#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
+enum SupportId {
+    Empty,
+    Singleton(ConstraintId),
+    OrderedUnion(UnionSupportId),
+    Quantified(QuantifiedSupportId),
+}
+
+#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
+struct UnionSupportData {
+    lhs: SupportId,
+    rhs: SupportId,
+}
+
+#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
+struct QuantifiedSupportData {
+    base: SupportId,
+    removed: Box<[ConstraintId]>,
+    derived: Box<[DerivedConstraintRecord]>,
+}
+
+#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
+struct DerivedConstraintRecord {
+    origin: ConstraintId,
+    derived: ConstraintId,
+}
+
 /// An individual constraint in a constraint set. This restricts a single typevar to be within a
 /// lower and upper bound.
 #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
@@ -941,12 +1125,23 @@ impl<'db> Constraint<'db> {
     ///
     /// Panics if `lower` and `upper` are not both fully static.
     fn new_node(
+        db: &'db dyn Db,
+        builder: &ConstraintSetBuilder<'db>,
+        typevar: BoundTypeVarInstance<'db>,
+        lower: Type<'db>,
+        upper: Type<'db>,
+    ) -> NodeId {
+        let (node, _) = Self::new_node_with_support(db, builder, typevar, lower, upper);
+        node
+    }
+
+    fn new_node_with_support(
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
         typevar: BoundTypeVarInstance<'db>,
         mut lower: Type<'db>,
         mut upper: Type<'db>,
-    ) -> NodeId {
+    ) -> (NodeId, SupportId) {
         // It's not useful for an upper bound to be an intersection type, or for a lower bound to
         // be a union type. Because the following equivalences hold, we can break these bounds
         // apart and create an equivalent BDD with more nodes but simpler constraints. (Fewer,
@@ -957,13 +1152,14 @@ impl<'db> Constraint<'db> {
         //   (α | β) ≤ T   ⇔ (α ≤ T) ∧ (β ≤ T)
         if let Type::Union(lower_union) = lower {
             let mut result = ALWAYS_TRUE;
+            let mut support = SupportId::Empty;
             for lower_element in lower_union.elements(db) {
-                result = result.and_with_offset(
-                    builder,
-                    Constraint::new_node(db, builder, typevar, *lower_element, upper),
-                );
+                let (next_node, next_support) =
+                    Constraint::new_node_with_support(db, builder, typevar, *lower_element, upper);
+                result = result.and_with_offset(builder, next_node);
+                support = builder.ordered_union_support(support, next_support);
             }
-            return result;
+            return (result, support);
         }
         // A negated type ¬α is represented as an intersection with no positive elements, and a
         // single negative element. We _don't_ want to treat that an "intersection" for the
@@ -972,19 +1168,25 @@ impl<'db> Constraint<'db> {
             && !upper_intersection.is_simple_negation(db)
         {
             let mut result = ALWAYS_TRUE;
+            let mut support = SupportId::Empty;
             for upper_element in upper_intersection.iter_positive(db) {
-                result = result.and_with_offset(
-                    builder,
-                    Constraint::new_node(db, builder, typevar, lower, upper_element),
-                );
+                let (next_node, next_support) =
+                    Constraint::new_node_with_support(db, builder, typevar, lower, upper_element);
+                result = result.and_with_offset(builder, next_node);
+                support = builder.ordered_union_support(support, next_support);
             }
             for upper_element in upper_intersection.iter_negative(db) {
-                result = result.and_with_offset(
+                let (next_node, next_support) = Constraint::new_node_with_support(
+                    db,
                     builder,
-                    Constraint::new_node(db, builder, typevar, lower, upper_element.negate(db)),
+                    typevar,
+                    lower,
+                    upper_element.negate(db),
                 );
+                result = result.and_with_offset(builder, next_node);
+                support = builder.ordered_union_support(support, next_support);
             }
-            return result;
+            return (result, support);
         }
 
         // Two identical typevars must always solve to the same type, so it is not useful to have
@@ -1011,12 +1213,11 @@ impl<'db> Constraint<'db> {
                     })
                 }) =>
             {
-                return Node::new_constraint(
-                    builder,
-                    ConstraintId::new(db, builder, typevar, Type::Never, Type::object()),
-                    1,
-                )
-                .negate(builder);
+                let constraint =
+                    ConstraintId::new(db, builder, typevar, Type::Never, Type::object());
+                let node = Node::new_constraint(builder, constraint, 1).negate(builder);
+                let support = SupportId::Singleton(constraint);
+                return (node, support);
             }
             _ => {}
         }
@@ -1041,7 +1242,7 @@ impl<'db> Constraint<'db> {
         // If `lower ≰ upper`, then the constraint cannot be satisfied, since there is no type that
         // is both greater than `lower`, and less than `upper`.
         if !lower.is_constraint_set_assignable_to(db, upper) {
-            return ALWAYS_FALSE;
+            return (ALWAYS_FALSE, SupportId::Empty);
         }
 
         builder.intern_constraint_typevars(db, typevar, lower, upper);
@@ -1060,17 +1261,16 @@ impl<'db> Constraint<'db> {
                 } else {
                     (typevar, lower)
                 };
-                Node::new_constraint(
+                let constraint = ConstraintId::new(
+                    db,
                     builder,
-                    ConstraintId::new(
-                        db,
-                        builder,
-                        typevar,
-                        Type::TypeVar(bound),
-                        Type::TypeVar(bound),
-                    ),
-                    1,
-                )
+                    typevar,
+                    Type::TypeVar(bound),
+                    Type::TypeVar(bound),
+                );
+                let node = Node::new_constraint(builder, constraint, 1);
+                let support = SupportId::Singleton(constraint);
+                (node, support)
             }
 
             // L ≤ T ≤ U == ([L] ≤ T) && (T ≤ [U])
@@ -1078,54 +1278,58 @@ impl<'db> Constraint<'db> {
                 if typevar.can_be_bound_for(db, builder, lower)
                     && typevar.can_be_bound_for(db, builder, upper) =>
             {
-                let lower = Node::new_constraint(
-                    builder,
-                    ConstraintId::new(db, builder, lower, Type::Never, Type::TypeVar(typevar)),
-                    1,
+                let lower_constraint =
+                    ConstraintId::new(db, builder, lower, Type::Never, Type::TypeVar(typevar));
+                let lower = Node::new_constraint(builder, lower_constraint, 1);
+                let upper_constraint =
+                    ConstraintId::new(db, builder, upper, Type::TypeVar(typevar), Type::object());
+                let upper = Node::new_constraint(builder, upper_constraint, 1);
+                let node = lower.and(builder, upper);
+                let support = builder.ordered_union_support(
+                    SupportId::Singleton(lower_constraint),
+                    SupportId::Singleton(upper_constraint),
                 );
-                let upper = Node::new_constraint(
-                    builder,
-                    ConstraintId::new(db, builder, upper, Type::TypeVar(typevar), Type::object()),
-                    1,
-                );
-                lower.and(builder, upper)
+                (node, support)
             }
 
             // L ≤ T ≤ U == ([L] ≤ T) && ([T] ≤ U)
             (Type::TypeVar(lower), _) if typevar.can_be_bound_for(db, builder, lower) => {
-                let lower = Node::new_constraint(
-                    builder,
-                    ConstraintId::new(db, builder, lower, Type::Never, Type::TypeVar(typevar)),
-                    1,
-                );
-                let upper = if upper.is_object() {
-                    ALWAYS_TRUE
+                let lower_constraint =
+                    ConstraintId::new(db, builder, lower, Type::Never, Type::TypeVar(typevar));
+                let lower = Node::new_constraint(builder, lower_constraint, 1);
+                let (upper, upper_support) = if upper.is_object() {
+                    (ALWAYS_TRUE, SupportId::Empty)
                 } else {
-                    Constraint::new_node(db, builder, typevar, Type::Never, upper)
+                    Constraint::new_node_with_support(db, builder, typevar, Type::Never, upper)
                 };
-                lower.and(builder, upper)
+                let node = lower.and(builder, upper);
+                let support = builder
+                    .ordered_union_support(SupportId::Singleton(lower_constraint), upper_support);
+                (node, support)
             }
 
             // L ≤ T ≤ U == (L ≤ [T]) && (T ≤ [U])
             (_, Type::TypeVar(upper)) if typevar.can_be_bound_for(db, builder, upper) => {
-                let lower = if lower.is_never() {
-                    ALWAYS_TRUE
+                let (lower, lower_support) = if lower.is_never() {
+                    (ALWAYS_TRUE, SupportId::Empty)
                 } else {
-                    Constraint::new_node(db, builder, typevar, lower, Type::object())
+                    Constraint::new_node_with_support(db, builder, typevar, lower, Type::object())
                 };
-                let upper = Node::new_constraint(
-                    builder,
-                    ConstraintId::new(db, builder, upper, Type::TypeVar(typevar), Type::object()),
-                    1,
-                );
-                lower.and(builder, upper)
+                let upper_constraint =
+                    ConstraintId::new(db, builder, upper, Type::TypeVar(typevar), Type::object());
+                let upper = Node::new_constraint(builder, upper_constraint, 1);
+                let node = lower.and(builder, upper);
+                let support = builder
+                    .ordered_union_support(lower_support, SupportId::Singleton(upper_constraint));
+                (node, support)
             }
 
-            _ => Node::new_constraint(
-                builder,
-                ConstraintId::new(db, builder, typevar, lower, upper),
-                1,
-            ),
+            _ => {
+                let constraint = ConstraintId::new(db, builder, typevar, lower, upper);
+                let node = Node::new_constraint(builder, constraint, 1);
+                let support = SupportId::Singleton(constraint);
+                (node, support)
+            }
         }
     }
 }
@@ -1694,11 +1898,12 @@ impl NodeId {
         self,
         db: &'db dyn Db,
         builder: &'c ConstraintSetBuilder<'db>,
+        support: SupportId,
     ) -> Solutions<'db, 'c> {
         match self.node() {
             Node::AlwaysTrue => Solutions::Unconstrained,
             Node::AlwaysFalse => Solutions::Unsatisfiable,
-            Node::Interior(interior) => interior.solutions(db, builder),
+            Node::Interior(interior) => interior.solutions(db, builder, support),
         }
     }
 
@@ -2981,6 +3186,7 @@ impl InteriorNode {
         self,
         db: &'db dyn Db,
         builder: &'c ConstraintSetBuilder<'db>,
+        support: SupportId,
     ) -> Solutions<'db, 'c> {
         #[derive(Default)]
         struct Bounds<'db> {
@@ -3158,6 +3364,7 @@ impl InteriorNode {
             Ref::map(storage, |storage| &storage.solutions_cache[&key])
         }
 
+        let _ = support;
         let solutions = solutions_inner(db, builder, self.node());
         if solutions.is_empty() {
             return Solutions::Unsatisfiable;

From 52befefcf847446d3219d66a322b4b05a85cfa22 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 3 Mar 2026 13:41:11 -0500
Subject: [PATCH 03/10] more correct quantified support

---
 .../src/types/constraints.rs                  | 45 ++++++++++++-------
 1 file changed, 29 insertions(+), 16 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 6b6421cb8b2722..50b53d66bebb54 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -972,38 +972,51 @@ impl<'db> ConstraintSetBuilder<'db> {
         ) {
             match support {
                 SupportId::Empty => {}
+
                 SupportId::Singleton(constraint) => {
                     constraints.insert(constraint);
                 }
+
                 SupportId::OrderedUnion(union_support) => {
                     let union_support = builder.union_support_data(union_support);
                     build_into(builder, union_support.lhs, constraints);
                     build_into(builder, union_support.rhs, constraints);
                 }
+
                 SupportId::Quantified(quantified_support) => {
                     let quantified_support = builder.quantified_support_data(quantified_support);
 
-                    let mut quantified_constraints = FxIndexSet::default();
-                    build_into(
-                        builder,
-                        quantified_support.base,
-                        &mut quantified_constraints,
-                    );
+                    // We should not remove any constraints that were already present before
+                    // building this node's base. That happens if e.g. we're going to union the
+                    // result of this quantified node with some other node:
+                    //
+                    //       union([a], quantified([a,b], remove=[a]))
+                    //    -> union([a], [b])
+                    //    -> [a,b]
+                    //
+                    // In this example, the base is [a,b], and we do want to remove [a] from that
+                    // base. But since [a] is already present in the lhs of the union, it will
+                    // still be in the final result.
+                    let base_index = constraints.len();
+                    build_into(builder, quantified_support.base, constraints);
 
                     for removed in &quantified_support.removed {
-                        quantified_constraints.shift_remove(removed);
+                        let removed_index = constraints
+                            .get_index_of(removed)
+                            .expect("constraint should exist in support");
+                        if removed_index >= base_index {
+                            constraints.shift_remove_index(removed_index);
+                        }
                     }
 
-                    for derived in &quantified_support.derived {
-                        assert!(
-                            quantified_constraints.contains(&derived.origin),
-                            "derived support origin {origin:?} not present in flattened quantified support",
-                            origin = derived.origin,
-                        );
-                        quantified_constraints.insert(derived.derived);
+                    for derived in quantified_support.derived.iter().rev() {
+                        let origin_index = constraints
+                            .get_index_of(&derived.origin)
+                            .expect("constraint should exist in support");
+                        if !constraints.contains(&derived.derived) {
+                            constraints.shift_insert(origin_index + 1, derived.derived);
+                        }
                     }
-
-                    constraints.extend(quantified_constraints);
                 }
             }
         }

From 48513472382089d828713e96e98e104d21a0ffe5 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 3 Mar 2026 14:27:36 -0500
Subject: [PATCH 04/10] update plan

---
 PLAN.md | 92 +++++++++++++++++++++++++++++++++------------------------
 1 file changed, 53 insertions(+), 39 deletions(-)

diff --git a/PLAN.md b/PLAN.md
index d628a6eef5245d..c8af267d093e6a 100644
--- a/PLAN.md
+++ b/PLAN.md
@@ -41,8 +41,10 @@ This plan covers Phases 1 and 2.
 
 In `crates/ty_python_semantic/src/types/constraints.rs`:
 
-- Add new index type:
+- Add new index types:
   - `#[newtype_index] struct UnionSupportId;`
+  - `#[newtype_index] struct RemoveSupportId;`
+  - `#[newtype_index] struct AddDerivedSupportId;`
 - Add a support-expression identifier enum:
 
 ```rust
@@ -50,8 +52,8 @@ enum SupportId {
     Empty,
     Singleton(ConstraintId),
     OrderedUnion(UnionSupportId),
-    // Quantification/abstraction support transform node (details below)
-    Quantified(QuantifiedSupportId),
+    Remove(RemoveSupportId),
+    AddDerived(AddDerivedSupportId),
 }
 ```
 
@@ -66,44 +68,40 @@ struct UnionSupportData {
 
 - Extend `ConstraintSetStorage` with:
   - `union_supports: IndexVec<UnionSupportId, UnionSupportData>`
-  - `quantified_supports: IndexVec<QuantifiedSupportId, QuantifiedSupportData>`
+  - `remove_supports: IndexVec<RemoveSupportId, RemoveSupportData>`
+  - `add_derived_supports: IndexVec<AddDerivedSupportId, AddDerivedSupportData>`
 
 Important initial policy:
 
-- **Do not hash-cons any support-expression nodes** in Phase 1 (including `OrderedUnion` and `Quantified`/quantified nodes).
+- **Do not hash-cons any support-expression nodes** in Phase 1 (including `OrderedUnion`, `Remove`, and `AddDerived` nodes).
 - Always append fresh support-expression nodes as operations are recorded.
 
-### 2) Quantification/derived-support node
+### 2) Quantification/derived-support nodes (flattened form)
 
-For existential abstraction and related flows, add a support node kind that records:
-
-- base support expression,
-- removed constraints,
-- derived constraints tied to origin constraints (rank provenance),
-- optional encounter index if needed to stabilize ties.
-
-Proposed payload sketch:
+Replace the single quantified-support payload with two explicit node kinds:
 
 ```rust
-struct QuantifiedSupportData {
+struct RemoveSupportData {
     base: SupportId,
-    removed: Box<[ConstraintId]>,
-    derived: Box<[DerivedConstraintRecord]>,
+    constraint: ConstraintId,
 }
 
-struct DerivedConstraintRecord {
+struct AddDerivedSupportData {
+    base: SupportId,
     origin: ConstraintId,
     derived: ConstraintId,
 }
 ```
 
-Note:
+Semantics:
 
-- We may later flatten/simplify `QuantifiedSupportData` and/or `DerivedConstraintRecord` if profiling or implementation experience suggests it.
+- `Remove`: remove one constraint from the base support (with existing accumulator semantics for duplicates/outer preexisting entries).
+- `AddDerived`: insert `derived` immediately after `origin` in rank order (if not already present).
 
-Invariant:
+Invariants:
 
-- Every `origin` used in `derived` **must** appear in the flattened base support (after removals are interpreted per algorithm). If not, treat as programmer error and **hard panic**.
+- `origin` used by `AddDerived` must exist in support at build time; missing origin is programmer error (hard panic).
+- When constructing multiple `AddDerived` nodes for one abstraction result, create them in **reverse encounter order** so final support order matches intended forward encounter order.
 
 ### 3) Make support expression explicit on `ConstraintSet`
 
@@ -125,7 +123,8 @@ Add methods on `ConstraintSetBuilder`:
   - `empty_support() -> SupportId`
   - `singleton_support(c: ConstraintId) -> SupportId`
   - `ordered_union_support(lhs: SupportId, rhs: SupportId) -> SupportId`
-  - `quantified_support(data: QuantifiedSupportData) -> SupportId`
+  - `remove_support(base: SupportId, constraint: ConstraintId) -> SupportId`
+  - `add_derived_support(base: SupportId, origin: ConstraintId, derived: ConstraintId) -> SupportId`
 
 - flattening/materialization:
   - `build_support(expr: SupportId) -> Box<[ConstraintId]>`
@@ -137,7 +136,8 @@ Add methods on `ConstraintSetBuilder`:
 - `OrderedUnion`: flatten lhs then rhs (graph structure defines ordering),
 - dedupe comes from `FxIndexSet` insertion semantics (first occurrence wins),
 - deterministic order,
-- `Quantified`: apply explicit remove/derive operations over the accumulator.
+- `Remove`: remove the recorded constraint from the accumulator according to node semantics.
+- `AddDerived`: insert derived constraint immediately after origin (if not already present).
 
 Implementation notes:
 
@@ -151,7 +151,8 @@ Implementation notes:
 - `union` / `intersect` / `iff` / `implies`: record ordered-union support node (`lhs`, `rhs`) only.
 - `negate`: support unchanged.
 - existential/reduction operations:
-  - record a `Quantified` support transform node; do not eagerly compute flattened order.
+  - record `Remove` and `AddDerived` transform nodes; do not eagerly compute flattened order.
+  - for multiple derived additions, build `AddDerived` nodes in reverse encounter order.
 
 ---
 
@@ -199,7 +200,7 @@ Apply to:
 In abstraction/simplification flows:
 
 - stop synthesizing/propagating node `source_order` values.
-- represent derived-support semantics via `Quantified` support node.
+- represent derived-support semantics via `Remove`/`AddDerived` support nodes.
 
 For relative ordering among derived constraints from the same origin:
 
@@ -266,7 +267,7 @@ Add tests for:
 - dedupe with first occurrence winning,
 - deterministic flatten for deep trees,
 - deterministic flatten behavior for large/deep support graphs,
-- `Quantified` semantics (remove + derive + tie behavior),
+- `Remove`/`AddDerived` semantics (remove + derive + tie behavior),
 - panic path when derived origin is missing,
 - `into_owned`/`load` support remap.
 
@@ -288,7 +289,7 @@ Then broader checks per repo conventions.
 
 Collect before/after metrics:
 
-- support-expression node counts (`OrderedUnion`, `Quantified`),
+- support-expression node counts (`OrderedUnion`, `Remove`, `AddDerived`),
 - flattened support lengths at consumption sites,
 - flatten invocation counts,
 - wall time in representative mdtests/code-nav runs,
@@ -322,14 +323,15 @@ Expectation:
 
 ## Concrete implementation checklist
 
-- [x] Add `SupportId`, `UnionSupportId`, `QuantifiedSupportId` and storage tables.
+- [x] Add `SupportId` and initial support-node storage tables.
 - [x] Add support-expression constructors on builder (no support-node hash-consing).
 - [x] Add `build_support` with `FxIndexSet` accumulator dedupe.
 - [x] Add `support` to `ConstraintSet` and flattened support payload to `OwnedConstraintSet`.
 - [x] Thread support expressions through constructors/combinators.
+- [ ] NEXT: Replace `Quantified` support payload with flattened `Remove`/`AddDerived` node types and builder APIs.
 - [ ] Update `distributed_or`/`distributed_and` and `when_any`/`when_all` to combine support in balanced-tree order.
 - [ ] Remove temporary `support_from_node` reconstruction path entirely.
-- [ ] Encode abstraction-derived ordering via `Quantified` support node.
+- [ ] Encode abstraction-derived ordering via `Remove`/`AddDerived` support nodes.
 - [ ] Convert ordering consumers to flattened support rank maps.
 - [ ] Remove node `source_order` fields and offset APIs.
 - [x] Run tests and update snapshots if needed.
@@ -342,23 +344,24 @@ Expectation:
 
 File: `crates/ty_python_semantic/src/types/constraints.rs`
 
-1. Add `UnionSupportId` and `QuantifiedSupportId` (`#[newtype_index]`).
-2. Add `SupportId` enum (`Empty`, `Singleton`, `OrderedUnion`, `Quantified`).
+1. Add `UnionSupportId`, `RemoveSupportId`, and `AddDerivedSupportId` (`#[newtype_index]`).
+2. Add `SupportId` enum (`Empty`, `Singleton`, `OrderedUnion`, `Remove`, `AddDerived`).
 3. Extend `ConstraintSetStorage` with:
    - `union_supports: IndexVec<UnionSupportId, UnionSupportData>`
-   - `quantified_supports: IndexVec<QuantifiedSupportId, QuantifiedSupportData>`
+   - `remove_supports: IndexVec<RemoveSupportId, RemoveSupportData>`
+   - `add_derived_supports: IndexVec<AddDerivedSupportId, AddDerivedSupportData>`
 4. If needed, add lightweight scratch state for iterative flatten traversal (e.g., reusable explicit stack buffers).
 
 ### Step B — builder APIs and flatten implementation
 
 File: `crates/ty_python_semantic/src/types/constraints.rs`
 
-1. Add support constructors (`empty`, `singleton`, `ordered_union`, `quantified`).
+1. Add support constructors (`empty`, `singleton`, `ordered_union`, `remove`, `add_derived`).
 2. Implement `build_support(expr) -> Box<[ConstraintId]>`:
    - iterative walk,
    - `FxIndexSet` accumulator for dedupe/order,
    - deterministic lhs-before-rhs.
-3. Implement clear per-node accumulator operations (`Empty`, `Singleton`, `OrderedUnion`, `Quantified`).
+3. Implement clear per-node accumulator operations (`Empty`, `Singleton`, `OrderedUnion`, `Remove`, `AddDerived`).
 4. Add/adjust reusable traversal scratch only if profiling indicates allocation churn in flatten.
 
 ### Step C — thread support through structs and constructors
@@ -400,13 +403,24 @@ File: `crates/ty_python_semantic/src/types/constraints.rs`
 - Add support-aware equivalents of distributed folding so support is combined in the same balanced shape (instead of reconstructing via `support_from_node`).
 - `support_from_node` is a strict temporary migration bridge and **must be removed** before final landing.
 
+### Step E.2 — flatten quantified support representation (**do this next before other pending steps**)
+
+File: `crates/ty_python_semantic/src/types/constraints.rs`
+
+1. Replace `Quantified` support node representation with two node kinds:
+   - `Remove(base, constraint)`
+   - `AddDerived(base, origin, derived)`
+2. Replace corresponding storage/index types and builder constructors.
+3. Update `build_support` operations to handle `Remove` and `AddDerived` directly.
+4. Ensure missing origin is a hard panic in `AddDerived` handling.
+
 ### Step F — quantification support node wiring
 
 File: `crates/ty_python_semantic/src/types/constraints.rs`
 
-1. In abstraction/reduction flows, build `Quantified` support nodes rather than eagerly computing ranks.
-2. Record origins and derived constraints; rely on support-graph structure for relative ordering.
-3. Enforce invariant that origins must be present at flatten time (hard panic otherwise).
+1. In abstraction/reduction flows, build `Remove` and `AddDerived` support nodes rather than eagerly computing ranks.
+2. For multiple derived additions from one transform, create `AddDerived` nodes in reverse encounter order.
+3. Enforce invariant that origins must be present at build time (hard panic otherwise).
 
 ### Step G — migrate ordering consumers
 
@@ -445,7 +459,7 @@ File: `crates/ty_python_semantic/src/types/constraints.rs`
 ### Confirmed design decisions
 
 1. Support construction should be cheap; defer support calculation until needed.
-2. No support-expression nodes are **hash-consed** in Phase 1 (`OrderedUnion` and `Quantified`/quantified included).
+2. No support-expression nodes are **hash-consed** in Phase 1 (`OrderedUnion`, `Remove`, and `AddDerived` included).
 3. Flattening is centralized in builder (`build_support`) and uses an `FxIndexSet<ConstraintId>` accumulator.
 4. `OwnedConstraintSet` persists flattened support, not support-expression graph.
 5. `load` rebuilds support as a left-associated `OrderedUnion` chain of singleton nodes.

From 81085769d371b322b22320ac13002712e76d3b0b Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 3 Mar 2026 14:34:46 -0500
Subject: [PATCH 05/10] break apart quantified support nodes

---
 PLAN.md                                       |   4 +-
 .../src/types/constraints.rs                  | 111 +++++++++++-------
 2 files changed, 68 insertions(+), 47 deletions(-)

diff --git a/PLAN.md b/PLAN.md
index c8af267d093e6a..d803140cc345b8 100644
--- a/PLAN.md
+++ b/PLAN.md
@@ -328,7 +328,7 @@ Expectation:
 - [x] Add `build_support` with `FxIndexSet` accumulator dedupe.
 - [x] Add `support` to `ConstraintSet` and flattened support payload to `OwnedConstraintSet`.
 - [x] Thread support expressions through constructors/combinators.
-- [ ] NEXT: Replace `Quantified` support payload with flattened `Remove`/`AddDerived` node types and builder APIs.
+- [x] Replace `Quantified` support payload with flattened `Remove`/`AddDerived` node types and builder APIs.
 - [ ] Update `distributed_or`/`distributed_and` and `when_any`/`when_all` to combine support in balanced-tree order.
 - [ ] Remove temporary `support_from_node` reconstruction path entirely.
 - [ ] Encode abstraction-derived ordering via `Remove`/`AddDerived` support nodes.
@@ -403,7 +403,7 @@ File: `crates/ty_python_semantic/src/types/constraints.rs`
 - Add support-aware equivalents of distributed folding so support is combined in the same balanced shape (instead of reconstructing via `support_from_node`).
 - `support_from_node` is a strict temporary migration bridge and **must be removed** before final landing.
 
-### Step E.2 — flatten quantified support representation (**do this next before other pending steps**)
+### Step E.2 — flatten quantified support representation (**completed**)
 
 File: `crates/ty_python_semantic/src/types/constraints.rs`
 
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 50b53d66bebb54..f2d6c9df253ff8 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -590,12 +590,8 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
     ) -> Self {
         self.verify_builder(builder);
         let node = self.node.exists(db, builder, to_remove);
-        let support = builder.quantified_support(QuantifiedSupportData {
-            base: self.support,
-            removed: Box::default(),
-            derived: Box::default(),
-        });
-        Self::from_node_and_support(builder, node, support)
+        // TODO: During quantification support wiring, represent this via Remove/AddDerived nodes.
+        Self::from_node_and_support(builder, node, self.support)
     }
 
     pub(crate) fn solutions(
@@ -691,8 +687,11 @@ struct ConstraintSetStorage<'db> {
     /// Support expression nodes that represent ordered unions of supports.
     union_supports: IndexVec<UnionSupportId, UnionSupportData>,
 
-    /// Support expression nodes that represent quantified support transforms.
-    quantified_supports: IndexVec<QuantifiedSupportId, QuantifiedSupportData>,
+    /// Support expression nodes that remove a single constraint from a base support.
+    remove_supports: IndexVec<RemoveSupportId, RemoveSupportData>,
+
+    /// Support expression nodes that add one derived constraint next to an origin.
+    add_derived_supports: IndexVec<AddDerivedSupportId, AddDerivedSupportData>,
 
     // Everything below are the memoization tables for the arenas and for our BDD operations.
     constraint_cache: FxHashMap<Constraint<'db>, ConstraintId>,
@@ -914,13 +913,12 @@ impl<'db> ConstraintSetBuilder<'db> {
         self.storage.borrow().union_supports[support]
     }
 
-    fn quantified_support_data(
-        &self,
-        support: QuantifiedSupportId,
-    ) -> Ref<'_, QuantifiedSupportData> {
-        Ref::map(self.storage.borrow(), |storage| {
-            &storage.quantified_supports[support]
-        })
+    fn remove_support_data(&self, support: RemoveSupportId) -> RemoveSupportData {
+        self.storage.borrow().remove_supports[support]
+    }
+
+    fn add_derived_support_data(&self, support: AddDerivedSupportId) -> AddDerivedSupportData {
+        self.storage.borrow().add_derived_supports[support]
     }
 
     fn ordered_union_support(&self, lhs: SupportId, rhs: SupportId) -> SupportId {
@@ -935,10 +933,29 @@ impl<'db> ConstraintSetBuilder<'db> {
         }
     }
 
-    fn quantified_support(&self, data: QuantifiedSupportData) -> SupportId {
+    #[expect(dead_code)] // Wired in Step F quantification support construction
+    fn remove_support(&self, base: SupportId, constraint: ConstraintId) -> SupportId {
+        let mut storage = self.storage.borrow_mut();
+        let id = storage
+            .remove_supports
+            .push(RemoveSupportData { base, constraint });
+        SupportId::Remove(id)
+    }
+
+    #[expect(dead_code)] // Wired in Step F quantification support construction
+    fn add_derived_support(
+        &self,
+        base: SupportId,
+        origin: ConstraintId,
+        derived: ConstraintId,
+    ) -> SupportId {
         let mut storage = self.storage.borrow_mut();
-        let id = storage.quantified_supports.push(data);
-        SupportId::Quantified(id)
+        let id = storage.add_derived_supports.push(AddDerivedSupportData {
+            base,
+            origin,
+            derived,
+        });
+        SupportId::AddDerived(id)
     }
 
     /// TEMPORARY MIGRATION HELPER.
@@ -983,14 +1000,14 @@ impl<'db> ConstraintSetBuilder<'db> {
                     build_into(builder, union_support.rhs, constraints);
                 }
 
-                SupportId::Quantified(quantified_support) => {
-                    let quantified_support = builder.quantified_support_data(quantified_support);
+                SupportId::Remove(remove_support) => {
+                    let remove_support = builder.remove_support_data(remove_support);
 
                     // We should not remove any constraints that were already present before
                     // building this node's base. That happens if e.g. we're going to union the
-                    // result of this quantified node with some other node:
+                    // result of this remove node with some other node:
                     //
-                    //       union([a], quantified([a,b], remove=[a]))
+                    //       union([a], remove(base=[a,b], constraint=a))
                     //    -> union([a], [b])
                     //    -> [a,b]
                     //
@@ -998,24 +1015,23 @@ impl<'db> ConstraintSetBuilder<'db> {
                     // base. But since [a] is already present in the lhs of the union, it will
                     // still be in the final result.
                     let base_index = constraints.len();
-                    build_into(builder, quantified_support.base, constraints);
-
-                    for removed in &quantified_support.removed {
-                        let removed_index = constraints
-                            .get_index_of(removed)
-                            .expect("constraint should exist in support");
-                        if removed_index >= base_index {
-                            constraints.shift_remove_index(removed_index);
-                        }
+                    build_into(builder, remove_support.base, constraints);
+                    let removed_index = constraints
+                        .get_index_of(&remove_support.constraint)
+                        .expect("constraint should exist in support");
+                    if removed_index >= base_index {
+                        constraints.shift_remove_index(removed_index);
                     }
+                }
 
-                    for derived in quantified_support.derived.iter().rev() {
-                        let origin_index = constraints
-                            .get_index_of(&derived.origin)
-                            .expect("constraint should exist in support");
-                        if !constraints.contains(&derived.derived) {
-                            constraints.shift_insert(origin_index + 1, derived.derived);
-                        }
+                SupportId::AddDerived(add_derived) => {
+                    let add_derived = builder.add_derived_support_data(add_derived);
+                    build_into(builder, add_derived.base, constraints);
+                    let origin_index = constraints
+                        .get_index_of(&add_derived.origin)
+                        .expect("constraint should exist in support");
+                    if !constraints.contains(&add_derived.derived) {
+                        constraints.shift_insert(origin_index + 1, add_derived.derived);
                     }
                 }
             }
@@ -1076,14 +1092,19 @@ struct UnionSupportId;
 
 #[newtype_index]
 #[derive(salsa::Update, get_size2::GetSize)]
-struct QuantifiedSupportId;
+struct RemoveSupportId;
+
+#[newtype_index]
+#[derive(salsa::Update, get_size2::GetSize)]
+struct AddDerivedSupportId;
 
 #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
 enum SupportId {
     Empty,
     Singleton(ConstraintId),
     OrderedUnion(UnionSupportId),
-    Quantified(QuantifiedSupportId),
+    Remove(RemoveSupportId),
+    AddDerived(AddDerivedSupportId),
 }
 
 #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
@@ -1092,15 +1113,15 @@ struct UnionSupportData {
     rhs: SupportId,
 }
 
-#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
-struct QuantifiedSupportData {
+#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
+struct RemoveSupportData {
     base: SupportId,
-    removed: Box<[ConstraintId]>,
-    derived: Box<[DerivedConstraintRecord]>,
+    constraint: ConstraintId,
 }
 
 #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
-struct DerivedConstraintRecord {
+struct AddDerivedSupportData {
+    base: SupportId,
     origin: ConstraintId,
     derived: ConstraintId,
 }

From 2022fa42102ce470f378843834de8e2c4f8e8a11 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 3 Mar 2026 14:49:41 -0500
Subject: [PATCH 06/10] update distributed_and/or

---
 PLAN.md                                       |  2 +-
 .../src/types/constraints.rs                  | 58 ++++++++++---------
 2 files changed, 32 insertions(+), 28 deletions(-)

diff --git a/PLAN.md b/PLAN.md
index d803140cc345b8..55aff31f39fbb2 100644
--- a/PLAN.md
+++ b/PLAN.md
@@ -329,7 +329,7 @@ Expectation:
 - [x] Add `support` to `ConstraintSet` and flattened support payload to `OwnedConstraintSet`.
 - [x] Thread support expressions through constructors/combinators.
 - [x] Replace `Quantified` support payload with flattened `Remove`/`AddDerived` node types and builder APIs.
-- [ ] Update `distributed_or`/`distributed_and` and `when_any`/`when_all` to combine support in balanced-tree order.
+- [x] Update `distributed_or`/`distributed_and` and `when_any`/`when_all` to combine support in balanced-tree order.
 - [ ] Remove temporary `support_from_node` reconstruction path entirely.
 - [ ] Encode abstraction-derived ordering via `Remove`/`AddDerived` support nodes.
 - [ ] Convert ordering consumers to flattened support rank maps.
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index f2d6c9df253ff8..46096031580f8f 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -173,18 +173,16 @@ where
         builder: &'c ConstraintSetBuilder<'db>,
         mut f: impl FnMut(T) -> ConstraintSet<'db, 'c>,
     ) -> ConstraintSet<'db, 'c> {
-        let node = NodeId::distributed_or(
+        let (node, support) = NodeId::distributed_or(
             db,
             builder,
             self.map(|element| {
                 let constraint = f(element);
                 constraint.verify_builder(builder);
-                constraint.node
+                (constraint.node, constraint.support)
             }),
         );
-        // TEMPORARY: support reconstruction from BDD nodes must be removed before finalizing
-        // support migration.
-        ConstraintSet::from_node_and_support(builder, node, builder.support_from_node(node))
+        ConstraintSet::from_node_and_support(builder, node, support)
     }
 
     fn when_all<'db, 'c>(
@@ -193,18 +191,16 @@ where
         builder: &'c ConstraintSetBuilder<'db>,
         mut f: impl FnMut(T) -> ConstraintSet<'db, 'c>,
     ) -> ConstraintSet<'db, 'c> {
-        let node = NodeId::distributed_and(
+        let (node, support) = NodeId::distributed_and(
             db,
             builder,
             self.map(|element| {
                 let constraint = f(element);
                 constraint.verify_builder(builder);
-                constraint.node
+                (constraint.node, constraint.support)
             }),
         );
-        // TEMPORARY: support reconstruction from BDD nodes must be removed before finalizing
-        // support migration.
-        ConstraintSet::from_node_and_support(builder, node, builder.support_from_node(node))
+        ConstraintSet::from_node_and_support(builder, node, support)
     }
 }
 
@@ -2027,11 +2023,11 @@ impl NodeId {
     fn tree_fold<'db>(
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
-        nodes: impl Iterator<Item = Self>,
+        nodes: impl Iterator<Item = (Self, SupportId)>,
         zero: Self,
         is_one: impl Fn(Self, &'db dyn Db, &ConstraintSetBuilder<'db>) -> bool,
         mut combine: impl FnMut(Self, &ConstraintSetBuilder<'db>, Self) -> Self,
-    ) -> Self {
+    ) -> (Self, SupportId) {
         // To implement the "linear" shape described above, we could collect the iterator elements
         // into a vector, and then use the fold at the bottom of this method to combine the
         // elements using the operator.
@@ -2056,40 +2052,48 @@ impl NodeId {
         //
         // We use a SmallVec for the accumulator so that we don't have to spill over to the heap
         // until the iterator passes 256 elements.
-        let mut accumulator: SmallVec<[(NodeId, u8); 8]> = SmallVec::default();
-        for node in nodes {
+        let mut accumulator: SmallVec<[((NodeId, SupportId), u8); 8]> = SmallVec::default();
+        for (node, support) in nodes {
             if is_one(node, db, builder) {
-                return node;
+                return (node, support);
             }
 
-            let (mut node, mut depth) = (node, 0);
+            let (mut node, mut support, mut depth) = (node, support, 0);
             while accumulator
                 .last()
                 .is_some_and(|(_, existing)| *existing == depth)
             {
-                let (existing, _) = accumulator.pop().expect("accumulator should not be empty");
-                node = combine(existing, builder, node);
+                let ((existing_node, existing_support), _) =
+                    accumulator.pop().expect("accumulator should not be empty");
+                node = combine(existing_node, builder, node);
+                support = builder.ordered_union_support(existing_support, support);
                 if is_one(node, db, builder) {
-                    return node;
+                    return (node, support);
                 }
                 depth += 1;
             }
-            accumulator.push((node, depth));
+            accumulator.push(((node, support), depth));
         }
 
         // At this point, we've consumed all of the iterator. The length of the accumulator will be
         // the same as the number of 1 bits in the length of the iterator. We do a final fold to
         // produce the overall result.
-        accumulator
-            .into_iter()
-            .fold(zero, |result, (node, _)| combine(result, builder, node))
+        accumulator.into_iter().fold(
+            (zero, SupportId::Empty),
+            |(result_node, result_support), ((node, support), _)| {
+                (
+                    combine(result_node, builder, node),
+                    builder.ordered_union_support(result_support, support),
+                )
+            },
+        )
     }
 
     fn distributed_or<'db>(
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
-        nodes: impl Iterator<Item = NodeId>,
-    ) -> Self {
+        nodes: impl Iterator<Item = (NodeId, SupportId)>,
+    ) -> (NodeId, SupportId) {
         Self::tree_fold(
             db,
             builder,
@@ -2103,8 +2107,8 @@ impl NodeId {
     fn distributed_and<'db>(
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
-        nodes: impl Iterator<Item = NodeId>,
-    ) -> Self {
+        nodes: impl Iterator<Item = (NodeId, SupportId)>,
+    ) -> (NodeId, SupportId) {
         Self::tree_fold(
             db,
             builder,

From 17c32c3f2076f6345e63161e3bd8cb6ff1d402ec Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 3 Mar 2026 15:07:36 -0500
Subject: [PATCH 07/10] update implies_subtype_of

---
 PLAN.md                                       |  2 +-
 .../src/types/constraints.rs                  | 45 +++++--------------
 2 files changed, 13 insertions(+), 34 deletions(-)

diff --git a/PLAN.md b/PLAN.md
index 55aff31f39fbb2..4b7ae2e4289527 100644
--- a/PLAN.md
+++ b/PLAN.md
@@ -330,7 +330,7 @@ Expectation:
 - [x] Thread support expressions through constructors/combinators.
 - [x] Replace `Quantified` support payload with flattened `Remove`/`AddDerived` node types and builder APIs.
 - [x] Update `distributed_or`/`distributed_and` and `when_any`/`when_all` to combine support in balanced-tree order.
-- [ ] Remove temporary `support_from_node` reconstruction path entirely.
+- [x] Remove temporary `support_from_node` reconstruction path entirely.
 - [ ] Encode abstraction-derived ordering via `Remove`/`AddDerived` support nodes.
 - [ ] Convert ordering consumers to flattened support rank maps.
 - [ ] Remove node `source_order` fields and offset APIs.
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 46096031580f8f..e70f22e80658cb 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -434,10 +434,8 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         rhs: Type<'db>,
     ) -> Self {
         self.verify_builder(builder);
-        let node = self.node.implies_subtype_of(db, builder, lhs, rhs);
-        // TEMPORARY: support reconstruction from BDD nodes must be removed before finalizing
-        // support migration.
-        Self::from_node_and_support(builder, node, builder.support_from_node(node))
+        let (node, support) = self.node.implies_subtype_of(db, builder, lhs, rhs, self.support);
+        Self::from_node_and_support(builder, node, support)
     }
 
     /// Returns whether this constraint set is satisfied by all of the typevars that it mentions.
@@ -954,29 +952,6 @@ impl<'db> ConstraintSetBuilder<'db> {
         SupportId::AddDerived(id)
     }
 
-    /// TEMPORARY MIGRATION HELPER.
-    ///
-    /// Reconstructs a support expression from the current BDD node shape by walking constraints
-    /// and ordering them by node `source_order`.
-    ///
-    /// This method **must not** remain in the final implementation. One of the goals of this
-    /// migration is to allow fully reduced BDDs, where the node graph is no longer required to
-    /// retain all constraints that contribute to support ordering. In that world, BDD structure
-    /// and support are intentionally decoupled, so support cannot be reconstructed from nodes.
-    fn support_from_node(&self, node: NodeId) -> SupportId {
-        let mut constraints: SmallVec<[_; 8]> = SmallVec::new();
-        node.for_each_constraint(self, &mut |constraint, source_order| {
-            constraints.push((constraint, source_order));
-        });
-        constraints.sort_unstable_by_key(|(_, source_order)| *source_order);
-        constraints
-            .into_iter()
-            .map(|(constraint, _)| SupportId::Singleton(constraint))
-            .fold(SupportId::Empty, |lhs, rhs| {
-                self.ordered_union_support(lhs, rhs)
-            })
-    }
-
     fn build_support(&self, support: SupportId) -> Box<[ConstraintId]> {
         fn build_into(
             builder: &ConstraintSetBuilder<'_>,
@@ -2241,24 +2216,25 @@ impl NodeId {
         builder: &ConstraintSetBuilder<'db>,
         lhs: Type<'db>,
         rhs: Type<'db>,
-    ) -> Self {
+        support: SupportId,
+    ) -> (Self, SupportId) {
         // When checking subtyping involving a typevar, we can turn the subtyping check into a
-        // constraint (i.e, "is `T` a subtype of `int` becomes the constraint `T ≤ int`), and then
+        // constraint (i.e, "is `T` a subtype of `int`" becomes the constraint `T ≤ int`), and then
         // check when the BDD implies that constraint.
         //
         // Note that we are NOT guaranteed that `lhs` and `rhs` will always be fully static, since
         // these types are coming in from arbitrary subtyping checks that the caller might want to
         // perform. So we have to take the appropriate materialization when translating the check
         // into a constraint.
-        let constraint = match (lhs, rhs) {
-            (Type::TypeVar(bound_typevar), _) => Constraint::new_node(
+        let (constraint_node, constraint_support) = match (lhs, rhs) {
+            (Type::TypeVar(bound_typevar), _) => Constraint::new_node_with_support(
                 db,
                 builder,
                 bound_typevar,
                 Type::Never,
                 rhs.bottom_materialization(db),
             ),
-            (_, Type::TypeVar(bound_typevar)) => Constraint::new_node(
+            (_, Type::TypeVar(bound_typevar)) => Constraint::new_node_with_support(
                 db,
                 builder,
                 bound_typevar,
@@ -2268,7 +2244,10 @@ impl NodeId {
             _ => panic!("at least one type should be a typevar"),
         };
 
-        self.implies(builder, constraint)
+        (
+            self.implies(builder, constraint_node),
+            builder.ordered_union_support(support, constraint_support),
+        )
     }
 
     fn satisfied_by_all_typevars<'db>(

From d76ead8bb32f7c4b081b6108e96077d370bda841 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 3 Mar 2026 15:39:45 -0500
Subject: [PATCH 08/10] update exists_one

---
 PLAN.md                                       |  13 +-
 .../src/types/constraints.rs                  | 162 +++++++++++-------
 2 files changed, 107 insertions(+), 68 deletions(-)

diff --git a/PLAN.md b/PLAN.md
index 4b7ae2e4289527..e0947b8e1b0140 100644
--- a/PLAN.md
+++ b/PLAN.md
@@ -331,7 +331,7 @@ Expectation:
 - [x] Replace `Quantified` support payload with flattened `Remove`/`AddDerived` node types and builder APIs.
 - [x] Update `distributed_or`/`distributed_and` and `when_any`/`when_all` to combine support in balanced-tree order.
 - [x] Remove temporary `support_from_node` reconstruction path entirely.
-- [ ] Encode abstraction-derived ordering via `Remove`/`AddDerived` support nodes.
+- [x] Encode abstraction-derived ordering via `Remove`/`AddDerived` support nodes.
 - [ ] Convert ordering consumers to flattened support rank maps.
 - [ ] Remove node `source_order` fields and offset APIs.
 - [x] Run tests and update snapshots if needed.
@@ -414,13 +414,18 @@ File: `crates/ty_python_semantic/src/types/constraints.rs`
 3. Update `build_support` operations to handle `Remove` and `AddDerived` directly.
 4. Ensure missing origin is a hard panic in `AddDerived` handling.
 
-### Step F — quantification support node wiring
+### Step F — quantification support node wiring (**completed**)
 
 File: `crates/ty_python_semantic/src/types/constraints.rs`
 
 1. In abstraction/reduction flows, build `Remove` and `AddDerived` support nodes rather than eagerly computing ranks.
 2. For multiple derived additions from one transform, create `AddDerived` nodes in reverse encounter order.
 3. Enforce invariant that origins must be present at build time (hard panic otherwise).
+4. Implementation approach used in landed code:
+   - thread `SupportId` directly through existing `NodeId`/`InteriorNode` quantification methods (instead of adding parallel `*_with_support` APIs),
+   - keep `ConstraintSet` as a thin wrapper,
+   - avoid temporary accumulator structs/collections for support deltas,
+   - in remove paths, record `AddDerived` before `Remove` so `origin` exists when `AddDerived` nodes are created.
 
 ### Step G — migrate ordering consumers
 
@@ -467,6 +472,9 @@ File: `crates/ty_python_semantic/src/types/constraints.rs`
 7. Relative ordering/tie-breaking comes from support-graph structure; no extra tie-break metadata initially.
 8. `support_from_node` is temporary-only and must not remain in the final implementation.
 9. Rationale for (8): support is being separated from BDD structure specifically so we can eventually move to fully reduced BDDs, where node shape cannot be relied on to reconstruct support.
+10. For quantification wiring, prefer updating the existing `NodeId` / `InteriorNode` abstraction methods to return `(NodeId, SupportId)` directly, rather than introducing duplicate `*_with_support` method families.
+11. Avoid allocation-heavy intermediate “support change” aggregators; record support operations (`AddDerived`, `Remove`) inline while walking abstraction paths.
+12. In remove paths, construct derived-support operations before the remove operation so `AddDerived.origin` is guaranteed to be present when each node is created.
 
 ### Invariants to preserve
 
@@ -491,3 +499,4 @@ For any materialized support list from `build_support`:
 - Keep fully reduced BDD work separate after migration stabilizes.
 - Keep support-expression ID types private to `constraints.rs`.
 - Consider flatten memoization only if profiling indicates repeated-flatten overhead.
+- `retain_one_cache` currently appears to be stale/dead state from earlier code paths; dead-field cleanup may require manual audit since compiler/lints may not flag it.
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index e70f22e80658cb..a206603237cabd 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -434,7 +434,9 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         rhs: Type<'db>,
     ) -> Self {
         self.verify_builder(builder);
-        let (node, support) = self.node.implies_subtype_of(db, builder, lhs, rhs, self.support);
+        let (node, support) = self
+            .node
+            .implies_subtype_of(db, builder, lhs, rhs, self.support);
         Self::from_node_and_support(builder, node, support)
     }
 
@@ -583,9 +585,8 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         to_remove: impl IntoIterator<Item = BoundTypeVarIdentity<'db>>,
     ) -> Self {
         self.verify_builder(builder);
-        let node = self.node.exists(db, builder, to_remove);
-        // TODO: During quantification support wiring, represent this via Remove/AddDerived nodes.
-        Self::from_node_and_support(builder, node, self.support)
+        let (node, support) = self.node.exists(db, builder, self.support, to_remove);
+        Self::from_node_and_support(builder, node, support)
     }
 
     pub(crate) fn solutions(
@@ -696,8 +697,8 @@ struct ConstraintSetStorage<'db> {
     or_cache: FxHashMap<(NodeId, NodeId, usize), NodeId>,
     and_cache: FxHashMap<(NodeId, NodeId, usize), NodeId>,
     iff_cache: FxHashMap<(NodeId, NodeId, usize), NodeId>,
-    exists_one_cache: FxHashMap<(NodeId, BoundTypeVarIdentity<'db>), NodeId>,
-    retain_one_cache: FxHashMap<(NodeId, BoundTypeVarIdentity<'db>), NodeId>,
+    exists_one_cache:
+        FxHashMap<(NodeId, SupportId, BoundTypeVarIdentity<'db>), (NodeId, SupportId)>,
     restrict_one_cache: FxHashMap<(NodeId, ConstraintAssignment), (NodeId, bool)>,
     solutions_cache: FxHashMap<NodeId, Vec<Solution<'db>>>,
     simplify_cache: FxHashMap<NodeId, NodeId>,
@@ -927,7 +928,6 @@ impl<'db> ConstraintSetBuilder<'db> {
         }
     }
 
-    #[expect(dead_code)] // Wired in Step F quantification support construction
     fn remove_support(&self, base: SupportId, constraint: ConstraintId) -> SupportId {
         let mut storage = self.storage.borrow_mut();
         let id = storage
@@ -936,7 +936,6 @@ impl<'db> ConstraintSetBuilder<'db> {
         SupportId::Remove(id)
     }
 
-    #[expect(dead_code)] // Wired in Step F quantification support construction
     fn add_derived_support(
         &self,
         base: SupportId,
@@ -2329,12 +2328,13 @@ impl NodeId {
         self,
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
+        support: SupportId,
         bound_typevars: impl IntoIterator<Item = BoundTypeVarIdentity<'db>>,
-    ) -> Self {
+    ) -> (Self, SupportId) {
         bound_typevars
             .into_iter()
-            .fold(self, |abstracted, bound_typevar| {
-                abstracted.exists_one(db, builder, bound_typevar)
+            .fold((self, support), |(node, support), bound_typevar| {
+                node.exists_one(db, builder, support, bound_typevar)
             })
     }
 
@@ -2342,12 +2342,12 @@ impl NodeId {
         self,
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
+        support: SupportId,
         bound_typevar: BoundTypeVarIdentity<'db>,
-    ) -> Self {
+    ) -> (Self, SupportId) {
         match self.node() {
-            Node::AlwaysTrue => ALWAYS_TRUE,
-            Node::AlwaysFalse => ALWAYS_FALSE,
-            Node::Interior(interior) => interior.exists_one(db, builder, bound_typevar),
+            Node::AlwaysTrue | Node::AlwaysFalse => (self, support),
+            Node::Interior(interior) => interior.exists_one(db, builder, support, bound_typevar),
         }
     }
 
@@ -2355,14 +2355,14 @@ impl NodeId {
         self,
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
+        support: SupportId,
         should_remove: &mut dyn FnMut(ConstraintId) -> bool,
         path: &mut PathAssignments,
-    ) -> Self {
+    ) -> (Self, SupportId) {
         match self.node() {
-            Node::AlwaysTrue => ALWAYS_TRUE,
-            Node::AlwaysFalse => ALWAYS_FALSE,
+            Node::AlwaysTrue | Node::AlwaysFalse => (self, support),
             Node::Interior(interior) => {
-                interior.abstract_one_inner(db, builder, should_remove, path)
+                interior.abstract_one_inner(db, builder, support, should_remove, path)
             }
         }
     }
@@ -2976,9 +2976,10 @@ impl InteriorNode {
         self,
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
+        support: SupportId,
         bound_typevar: BoundTypeVarIdentity<'db>,
-    ) -> NodeId {
-        let key = (self.node(), bound_typevar);
+    ) -> (NodeId, SupportId) {
+        let key = (self.node(), support, bound_typevar);
         let storage = builder.storage.borrow();
         if let Some(result) = storage.exists_one_cache.get(&key) {
             return *result;
@@ -2993,6 +2994,7 @@ impl InteriorNode {
         let result = self.abstract_one_inner(
             db,
             builder,
+            support,
             // Remove any node that constrains `bound_typevar`, or that has a lower/upper bound
             // that mentions `bound_typevar`.
             // TODO: This will currently remove constraints that mention a typevar, but the sequent
@@ -3025,9 +3027,10 @@ impl InteriorNode {
         self,
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
+        support: SupportId,
         should_remove: &mut dyn FnMut(ConstraintId) -> bool,
         path: &mut PathAssignments,
-    ) -> NodeId {
+    ) -> (NodeId, SupportId) {
         let self_interior = builder.interior_node_data(self.node());
         if should_remove(self_interior.constraint) {
             // If we should remove constraints involving this typevar, then we replace this node
@@ -3042,110 +3045,137 @@ impl InteriorNode {
             // TODO: This might not be stable enough, if we add more than one derived fact for this
             // constraint. If we still see inconsistent test output, we might need a more complex
             // way of tracking source order for derived facts.
-            let if_true = path
+            let (if_true_node, if_true_support) = path
                 .walk_edge(
                     db,
                     builder,
                     self_interior.constraint.when_true(),
                     self_interior.source_order,
                     |path, new_range| {
-                        let branch = self_interior.if_true.abstract_one_inner(
-                            db,
-                            builder,
-                            should_remove,
-                            path,
-                        );
+                        let (branch_node, branch_support) = self_interior
+                            .if_true
+                            .abstract_one_inner(db, builder, support, should_remove, path);
                         path.assignments[new_range]
                             .iter()
+                            .rev() // add_derived supports are applied in reverse order
                             .filter(|(assignment, _)| {
                                 // Don't add back any derived facts if they are ones that we would have
                                 // removed!
                                 !should_remove(assignment.constraint())
                             })
-                            .fold(branch, |branch, (assignment, source_order)| {
-                                branch.and(
-                                    builder,
-                                    Node::new_satisfied_constraint(
+                            .fold(
+                                (branch_node, branch_support),
+                                |(branch_node, branch_support), (assignment, source_order)| {
+                                    let constraint = Node::new_satisfied_constraint(
                                         builder,
                                         *assignment,
                                         *source_order,
-                                    ),
-                                )
-                            })
+                                    );
+                                    (
+                                        branch_node.and(builder, constraint),
+                                        builder.add_derived_support(
+                                            branch_support,
+                                            self_interior.constraint,
+                                            assignment.constraint(),
+                                        ),
+                                    )
+                                },
+                            )
                     },
                 )
-                .unwrap_or(ALWAYS_FALSE);
-            let if_false = path
+                .unwrap_or((ALWAYS_FALSE, SupportId::Empty));
+            let (if_false_node, if_false_support) = path
                 .walk_edge(
                     db,
                     builder,
                     self_interior.constraint.when_false(),
                     self_interior.source_order,
                     |path, new_range| {
-                        let branch = self_interior.if_false.abstract_one_inner(
-                            db,
-                            builder,
-                            should_remove,
-                            path,
-                        );
+                        let (branch_node, branch_support) = self_interior
+                            .if_false
+                            .abstract_one_inner(db, builder, support, should_remove, path);
                         path.assignments[new_range]
                             .iter()
+                            .rev() // add_derived supports are applied in reverse order
                             .filter(|(assignment, _)| {
                                 // Don't add back any derived facts if they are ones that we would have
                                 // removed!
                                 !should_remove(assignment.constraint())
                             })
-                            .fold(branch, |branch, (assignment, source_order)| {
-                                branch.and(
-                                    builder,
-                                    Node::new_satisfied_constraint(
+                            .fold(
+                                (branch_node, branch_support),
+                                |(branch_node, branch_support), (assignment, source_order)| {
+                                    let constraint = Node::new_satisfied_constraint(
                                         builder,
                                         *assignment,
                                         *source_order,
-                                    ),
-                                )
-                            })
+                                    );
+                                    (
+                                        branch_node.and(builder, constraint),
+                                        builder.add_derived_support(
+                                            branch_support,
+                                            self_interior.constraint,
+                                            assignment.constraint(),
+                                        ),
+                                    )
+                                },
+                            )
                     },
                 )
-                .unwrap_or(ALWAYS_FALSE);
-            if_true.or(builder, if_false)
+                .unwrap_or((ALWAYS_FALSE, SupportId::Empty));
+            let node = if_true_node.or(builder, if_false_node);
+            let support = builder.ordered_union_support(if_true_support, if_false_support);
+            let support = builder.remove_support(support, self_interior.constraint);
+            (node, support)
         } else {
             // Otherwise, we abstract the if_false/if_true edges recursively.
-            let if_true = path
+            let (if_true_node, if_true_support) = path
                 .walk_edge(
                     db,
                     builder,
                     self_interior.constraint.when_true(),
                     self_interior.source_order,
                     |path, _| {
-                        self_interior
-                            .if_true
-                            .abstract_one_inner(db, builder, should_remove, path)
+                        self_interior.if_true.abstract_one_inner(
+                            db,
+                            builder,
+                            support,
+                            should_remove,
+                            path,
+                        )
                     },
                 )
-                .unwrap_or(ALWAYS_FALSE);
-            let if_false = path
+                .unwrap_or((ALWAYS_FALSE, SupportId::Empty));
+            let (if_false_node, if_false_support) = path
                 .walk_edge(
                     db,
                     builder,
                     self_interior.constraint.when_false(),
                     self_interior.source_order,
                     |path, _| {
-                        self_interior
-                            .if_false
-                            .abstract_one_inner(db, builder, should_remove, path)
+                        self_interior.if_false.abstract_one_inner(
+                            db,
+                            builder,
+                            support,
+                            should_remove,
+                            path,
+                        )
                     },
                 )
-                .unwrap_or(ALWAYS_FALSE);
+                .unwrap_or((ALWAYS_FALSE, SupportId::Empty));
             // NB: We cannot use `Node::new` here, because the recursive calls might introduce new
             // derived constraints into the result, and those constraints might appear before this
             // one in the BDD ordering.
-            Node::new_constraint(
+            let constraint = Node::new_constraint(
                 builder,
                 self_interior.constraint,
                 self_interior.source_order,
-            )
-            .ite(builder, if_true, if_false)
+            );
+            let node = constraint.ite(builder, if_true_node, if_false_node);
+            let support = builder.ordered_union_support(if_true_support, if_false_support);
+            let support = builder
+                .ordered_union_support(SupportId::Singleton(self_interior.constraint), support);
+            (node, support)
         }
     }
 

From 61d56b428dc1c7c0219e3f132d61c9c011a89ef8 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 3 Mar 2026 16:10:12 -0500
Subject: [PATCH 09/10] use support instead of source_order

---
 PLAN.md                                       | 16 ++--
 .../src/types/constraints.rs                  | 73 ++++++++++++++-----
 2 files changed, 67 insertions(+), 22 deletions(-)

diff --git a/PLAN.md b/PLAN.md
index e0947b8e1b0140..75f46669cf25c2 100644
--- a/PLAN.md
+++ b/PLAN.md
@@ -127,7 +127,7 @@ Add methods on `ConstraintSetBuilder`:
   - `add_derived_support(base: SupportId, origin: ConstraintId, derived: ConstraintId) -> SupportId`
 
 - flattening/materialization:
-  - `build_support(expr: SupportId) -> Box<[ConstraintId]>`
+  - `build_support(expr: SupportId) -> FxIndexSet<ConstraintId>`
 
 `build_support` behavior:
 
@@ -332,7 +332,7 @@ Expectation:
 - [x] Update `distributed_or`/`distributed_and` and `when_any`/`when_all` to combine support in balanced-tree order.
 - [x] Remove temporary `support_from_node` reconstruction path entirely.
 - [x] Encode abstraction-derived ordering via `Remove`/`AddDerived` support nodes.
-- [ ] Convert ordering consumers to flattened support rank maps.
+- [x] Convert ordering consumers to flattened support rank maps. _(load-bearing consumer complete: `NodeId::solutions`; remaining `source_order` uses are bookkeeping/debug paths removed in Step H)_
 - [ ] Remove node `source_order` fields and offset APIs.
 - [x] Run tests and update snapshots if needed.
 
@@ -357,7 +357,7 @@ File: `crates/ty_python_semantic/src/types/constraints.rs`
 File: `crates/ty_python_semantic/src/types/constraints.rs`
 
 1. Add support constructors (`empty`, `singleton`, `ordered_union`, `remove`, `add_derived`).
-2. Implement `build_support(expr) -> Box<[ConstraintId]>`:
+2. Implement `build_support(expr) -> FxIndexSet<ConstraintId>`:
    - iterative walk,
    - `FxIndexSet` accumulator for dedupe/order,
    - deterministic lhs-before-rhs.
@@ -427,7 +427,7 @@ File: `crates/ty_python_semantic/src/types/constraints.rs`
    - avoid temporary accumulator structs/collections for support deltas,
    - in remove paths, record `AddDerived` before `Remove` so `origin` exists when `AddDerived` nodes are created.
 
-### Step G — migrate ordering consumers
+### Step G — migrate ordering consumers (**completed for load-bearing consumers**)
 
 File: `crates/ty_python_semantic/src/types/constraints.rs`
 
@@ -435,6 +435,12 @@ File: `crates/ty_python_semantic/src/types/constraints.rs`
 2. `NodeId::path_assignments` ordering logic.
 3. Any other display/simplify sorting based on `source_order`.
 
+Current status:
+
+- ✅ `NodeId::solutions` now uses support-aware path traversal (`for_each_path_with_support`) and support-rank ordering.
+- ✅ No additional load-bearing ordering consumers require migration in Step G.
+- ℹ️ Remaining `source_order`-dependent code paths (`PathAssignments` bookkeeping, simplification/display ordering, graph-debug output) are tied to interior-node `source_order` fields and are expected to be removed in Step H.
+
 Pattern:
 
 - flatten support once for the set,
@@ -499,4 +505,4 @@ For any materialized support list from `build_support`:
 - Keep fully reduced BDD work separate after migration stabilizes.
 - Keep support-expression ID types private to `constraints.rs`.
 - Consider flatten memoization only if profiling indicates repeated-flatten overhead.
-- `retain_one_cache` currently appears to be stale/dead state from earlier code paths; dead-field cleanup may require manual audit since compiler/lints may not flag it.
+
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index a206603237cabd..d804357791010e 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -700,7 +700,7 @@ struct ConstraintSetStorage<'db> {
     exists_one_cache:
         FxHashMap<(NodeId, SupportId, BoundTypeVarIdentity<'db>), (NodeId, SupportId)>,
     restrict_one_cache: FxHashMap<(NodeId, ConstraintAssignment), (NodeId, bool)>,
-    solutions_cache: FxHashMap<NodeId, Vec<Solution<'db>>>,
+    solutions_cache: FxHashMap<(NodeId, SupportId), Vec<Solution<'db>>>,
     simplify_cache: FxHashMap<NodeId, NodeId>,
 
     single_sequent_cache: FxHashMap<ConstraintId, SequentMap>,
@@ -726,7 +726,7 @@ impl<'db> ConstraintSetBuilder<'db> {
         // the original builder aren't relevant to the new builder, and don't need to be retained.
         let constraint = f(&self);
         let node = constraint.node;
-        let support = self.build_support(constraint.support);
+        let support = self.build_support(constraint.support).into_iter().collect();
         let storage = self.storage.into_inner();
         OwnedConstraintSet {
             node,
@@ -951,7 +951,7 @@ impl<'db> ConstraintSetBuilder<'db> {
         SupportId::AddDerived(id)
     }
 
-    fn build_support(&self, support: SupportId) -> Box<[ConstraintId]> {
+    fn build_support(&self, support: SupportId) -> FxIndexSet<ConstraintId> {
         fn build_into(
             builder: &ConstraintSetBuilder<'_>,
             support: SupportId,
@@ -1009,7 +1009,7 @@ impl<'db> ConstraintSetBuilder<'db> {
 
         let mut constraints = FxIndexSet::default();
         build_into(self, support, &mut constraints);
-        constraints.into_iter().collect()
+        constraints
     }
 }
 
@@ -1732,31 +1732,33 @@ impl NodeId {
         }
     }
 
-    fn for_each_path<'db>(
+    fn for_each_path_with_support<'db>(
         self,
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
-        mut f: impl FnMut(&PathAssignments),
+        support: SupportId,
+        mut f: impl FnMut(&PathAssignments, SupportId),
     ) {
         match self.node() {
             Node::AlwaysTrue => {}
             Node::AlwaysFalse => {}
             Node::Interior(interior) => {
                 let mut path = interior.path_assignments(builder);
-                self.for_each_path_inner(db, builder, &mut f, &mut path);
+                self.for_each_path_inner_with_support(db, builder, support, &mut f, &mut path);
             }
         }
     }
 
-    fn for_each_path_inner<'db>(
+    fn for_each_path_inner_with_support<'db>(
         self,
         db: &'db dyn Db,
         builder: &ConstraintSetBuilder<'db>,
-        f: &mut dyn FnMut(&PathAssignments),
+        support: SupportId,
+        f: &mut dyn FnMut(&PathAssignments, SupportId),
         path: &mut PathAssignments,
     ) {
         match self.node() {
-            Node::AlwaysTrue => f(path),
+            Node::AlwaysTrue => f(path, support),
             Node::AlwaysFalse => {}
             Node::Interior(_) => {
                 let interior = builder.interior_node_data(self);
@@ -1765,14 +1767,42 @@ impl NodeId {
                     builder,
                     interior.constraint.when_true(),
                     interior.source_order,
-                    |path, _| interior.if_true.for_each_path_inner(db, builder, f, path),
+                    |path, new_range| {
+                        let support = path.assignments[new_range]
+                            .iter()
+                            .rev() // add_derived supports are applied in reverse order
+                            .fold(support, |support, (assignment, _)| {
+                                builder.add_derived_support(
+                                    support,
+                                    interior.constraint,
+                                    assignment.constraint(),
+                                )
+                            });
+                        interior
+                            .if_true
+                            .for_each_path_inner_with_support(db, builder, support, f, path);
+                    },
                 );
                 path.walk_edge(
                     db,
                     builder,
                     interior.constraint.when_false(),
                     interior.source_order,
-                    |path, _| interior.if_false.for_each_path_inner(db, builder, f, path),
+                    |path, new_range| {
+                        let support = path.assignments[new_range]
+                            .iter()
+                            .rev() // add_derived supports are applied in reverse order
+                            .fold(support, |support, (assignment, _)| {
+                                builder.add_derived_support(
+                                    support,
+                                    interior.constraint,
+                                    assignment.constraint(),
+                                )
+                            });
+                        interior
+                            .if_false
+                            .for_each_path_inner_with_support(db, builder, support, f, path);
+                    },
                 );
             }
         }
@@ -3277,8 +3307,9 @@ impl InteriorNode {
             db: &'db dyn Db,
             builder: &'c ConstraintSetBuilder<'db>,
             interior: NodeId,
+            support: SupportId,
         ) -> Ref<'c, Vec<Solution<'db>>> {
-            let key = interior;
+            let key = (interior, support);
             let storage = builder.storage.borrow();
             if let Ok(solutions) =
                 Ref::filter_map(storage, |storage| storage.solutions_cache.get(&key))
@@ -3292,8 +3323,17 @@ impl InteriorNode {
             // "tied" constraints will still be ordered in a stable way. So we need a stable sort to
             // retain that stable per-tie ordering.
             let mut sorted_paths = Vec::new();
-            interior.for_each_path(db, builder, |path| {
-                let mut path: Vec<_> = path.positive_constraints().collect();
+            interior.for_each_path_with_support(db, builder, support, |path, path_support| {
+                let support_order = builder.build_support(path_support);
+                let mut path: Vec<_> = path
+                    .positive_constraints()
+                    .map(|(constraint, _source_order)| {
+                        let source_order = support_order
+                            .get_index_of(&constraint)
+                            .expect("constraint should exist in support order");
+                        (constraint, source_order)
+                    })
+                    .collect();
                 path.sort_by_key(|(_, source_order)| *source_order);
                 sorted_paths.push(path);
             });
@@ -3411,8 +3451,7 @@ impl InteriorNode {
             Ref::map(storage, |storage| &storage.solutions_cache[&key])
         }
 
-        let _ = support;
-        let solutions = solutions_inner(db, builder, self.node());
+        let solutions = solutions_inner(db, builder, self.node(), support);
         if solutions.is_empty() {
             return Solutions::Unsatisfiable;
         }

From 2b07c2c7ee4baded08d2944a6245ea1d8c4583d4 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Wed, 4 Mar 2026 13:34:20 -0500
Subject: [PATCH 10/10] remove finished plan

---
 PLAN.md | 508 --------------------------------------------------------
 1 file changed, 508 deletions(-)
 delete mode 100644 PLAN.md

diff --git a/PLAN.md b/PLAN.md
deleted file mode 100644
index 75f46669cf25c2..00000000000000
--- a/PLAN.md
+++ /dev/null
@@ -1,508 +0,0 @@
-# Constraint-set support tracking and `source_order` removal plan
-
-## Goal
-
-Replace per-interior-node `source_order` tracking with per-constraint-set **support expression** tracking.
-
-The key design principle is:
-
-- During BDD construction, support handling should be **very cheap** (record support operations only).
-- Materialize concrete ordered support (`[ConstraintId]`) **lazily**, only when consumers need it.
-
-This should:
-
-1. Preserve stable, source-like ordering for diagnostics/solutions.
-2. Avoid dependence on global/builder-local `ConstraintId` numeric order.
-3. Enable future switch from quasi-reduced to fully reduced BDD nodes.
-4. Shift CPU work out of hot BDD ops into rarer support-consumption paths.
-
----
-
-## Scope and staging
-
-- [ ] **Phase 1 (mechanical + behavior-preserving):**
-  - Introduce support-expression infrastructure.
-  - Thread support expressions through `ConstraintSet` operations.
-  - Keep existing node `source_order` fields temporarily.
-  - Add lazy flattening API and migrate consumers where practical.
-- [ ] **Phase 2 (cleanup):**
-  - Remove node-level `source_order`/`max_source_order`.
-  - Remove offset machinery (`*_with_offset`, `with_adjusted_source_order`, etc.).
-- [ ] **Phase 3 (optional follow-up):**
-  - Evaluate switching from quasi-reduced to fully reduced BDDs.
-
-This plan covers Phases 1 and 2.
-
----
-
-## Data model changes
-
-### 1) Add support-expression IDs and storage
-
-In `crates/ty_python_semantic/src/types/constraints.rs`:
-
-- Add new index types:
-  - `#[newtype_index] struct UnionSupportId;`
-  - `#[newtype_index] struct RemoveSupportId;`
-  - `#[newtype_index] struct AddDerivedSupportId;`
-- Add a support-expression identifier enum:
-
-```rust
-enum SupportId {
-    Empty,
-    Singleton(ConstraintId),
-    OrderedUnion(UnionSupportId),
-    Remove(RemoveSupportId),
-    AddDerived(AddDerivedSupportId),
-}
-```
-
-(Exact naming may vary; `SupportId` can remain module-private.)
-
-```rust
-struct UnionSupportData {
-    lhs: SupportId,
-    rhs: SupportId,
-}
-```
-
-- Extend `ConstraintSetStorage` with:
-  - `union_supports: IndexVec<UnionSupportId, UnionSupportData>`
-  - `remove_supports: IndexVec<RemoveSupportId, RemoveSupportData>`
-  - `add_derived_supports: IndexVec<AddDerivedSupportId, AddDerivedSupportData>`
-
-Important initial policy:
-
-- **Do not hash-cons any support-expression nodes** in Phase 1 (including `OrderedUnion`, `Remove`, and `AddDerived` nodes).
-- Always append fresh support-expression nodes as operations are recorded.
-
-### 2) Quantification/derived-support nodes (flattened form)
-
-Replace the single quantified-support payload with two explicit node kinds:
-
-```rust
-struct RemoveSupportData {
-    base: SupportId,
-    constraint: ConstraintId,
-}
-
-struct AddDerivedSupportData {
-    base: SupportId,
-    origin: ConstraintId,
-    derived: ConstraintId,
-}
-```
-
-Semantics:
-
-- `Remove`: remove one constraint from the base support (with existing accumulator semantics for duplicates/outer preexisting entries).
-- `AddDerived`: insert `derived` immediately after `origin` in rank order (if not already present).
-
-Invariants:
-
-- `origin` used by `AddDerived` must exist in support at build time; missing origin is programmer error (hard panic).
-- When constructing multiple `AddDerived` nodes for one abstraction result, create them in **reverse encounter order** so final support order matches intended forward encounter order.
-
-### 3) Make support expression explicit on `ConstraintSet`
-
-- `ConstraintSet` gains `support: SupportId`.
-- `OwnedConstraintSet` stores **materialized** support:
-  - `support: Box<[ConstraintId]>`
-
-`ConstraintSet::from_node` becomes `from_node_and_support(...)`.
-
----
-
-## Support-expression operations
-
-### 4) Builder helpers
-
-Add methods on `ConstraintSetBuilder`:
-
-- constructors:
-  - `empty_support() -> SupportId`
-  - `singleton_support(c: ConstraintId) -> SupportId`
-  - `ordered_union_support(lhs: SupportId, rhs: SupportId) -> SupportId`
-  - `remove_support(base: SupportId, constraint: ConstraintId) -> SupportId`
-  - `add_derived_support(base: SupportId, origin: ConstraintId, derived: ConstraintId) -> SupportId`
-
-- flattening/materialization:
-  - `build_support(expr: SupportId) -> FxIndexSet<ConstraintId>`
-
-`build_support` behavior:
-
-- uses an `FxIndexSet<ConstraintId>` accumulator (type alias over `indexmap::IndexSet`),
-- iterative traversal (no recursive stack growth risk),
-- `OrderedUnion`: flatten lhs then rhs (graph structure defines ordering),
-- dedupe comes from `FxIndexSet` insertion semantics (first occurrence wins),
-- deterministic order,
-- `Remove`: remove the recorded constraint from the accumulator according to node semantics.
-- `AddDerived`: insert derived constraint immediately after origin (if not already present).
-
-Implementation notes:
-
-- Keep flatten semantics centralized in this one method; each support node maps to a clear accumulator operation.
-- `build_support` should rely on `FxIndexSet` for dedupe and order (no bespoke mark/epoch dedupe logic in this path).
-
-### 5) Support creation rules
-
-- Atomic single-constraint set: singleton support.
-- `always` / `never`: empty support.
-- `union` / `intersect` / `iff` / `implies`: record ordered-union support node (`lhs`, `rhs`) only.
-- `negate`: support unchanged.
-- existential/reduction operations:
-  - record `Remove` and `AddDerived` transform nodes; do not eagerly compute flattened order.
-  - for multiple derived additions, build `AddDerived` nodes in reverse encounter order.
-
----
-
-## Thread support through APIs
-
-### 6) Constructors and conversions
-
-Update:
-
-- `ConstraintSet::always/never/from_bool/constrain_typevar/...`
-- `ConstraintSetBuilder::into_owned` and `load`
-
-Rules:
-
-- `into_owned` materializes flattened support and stores `Box<[ConstraintId]>`.
-- `load` remaps stored support constraints through remapped `ConstraintId`s and rebuilds support expression as a left-associated chain of singleton `OrderedUnion` nodes.
-
-### 7) Combinators
-
-Update all combinators to compose support expressions without flattening:
-
-- `union`, `intersect`, `and`, `or`, `implies`, `iff`, `negate`
-- quantification/restriction methods (`reduce_inferable`, `retain_non_inferable`, etc.)
-
-Audit all `ConstraintSet::from_node(...)` sites and convert to support-aware constructor.
-
----
-
-## Migrate consumers from `source_order` to flattened support rank
-
-### 8) Path and solution ordering
-
-Replace per-node `source_order` sorting with support-rank sorting:
-
-- Build `constraint -> rank` map from `build_support(constraint_set.support)`.
-- Sort positives by rank (stable; ties should not normally occur once rank map is built from flattened support).
-
-Apply to:
-
-- `NodeId::solutions`
-- display/simplification code currently sorting by `source_order`
-
-### 9) Simplification and quantification behavior
-
-In abstraction/simplification flows:
-
-- stop synthesizing/propagating node `source_order` values.
-- represent derived-support semantics via `Remove`/`AddDerived` support nodes.
-
-For relative ordering among derived constraints from the same origin:
-
-- use support-graph structure (construction order of support nodes) as the tie-breaker.
-- do not add extra tie-break metadata initially.
-
-### 10) `PathAssignments`
-
-Current `FxIndexMap<ConstraintAssignment, usize>` may remain initially.
-
-- reinterpret `usize` as support rank when populated from flattened support.
-- do not assume rank originates from interior-node metadata.
-
----
-
-## Remove `source_order` from nodes (Phase 2)
-
-### 11) Interior node shape
-
-Remove from `InteriorNodeData`:
-
-- `source_order`
-- `max_source_order`
-
-Update `Node::new`, `new_constraint`, `new_satisfied_constraint` signatures.
-
-### 12) Remove offset machinery
-
-Delete/replace:
-
-- `with_adjusted_source_order`
-- `max_source_order`
-- `or_with_offset`, `and_with_offset`, `iff_with_offset`
-- cache key dimensions based on `other_offset`
-
-Use normal binary ops at BDD layer; support ordering comes from support expression graph.
-
-### 13) Update docs/comments
-
-Replace references to node-level source-order with support-expression + flatten semantics.
-
----
-
-## Fully reduced BDD follow-up (Phase 3)
-
-### 14) Toggle reduction behavior
-
-After support migration lands:
-
-- evaluate removing quasi-reduction exception that preserves redundant nodes,
-- benchmark and validate output stability.
-
-Keep as separate PR/commit.
-
----
-
-## Testing strategy
-
-### 15) Unit tests in `constraints.rs`
-
-Add tests for:
-
-- flatten of ordered-union chains preserves lhs-first semantics,
-- dedupe with first occurrence winning,
-- deterministic flatten for deep trees,
-- deterministic flatten behavior for large/deep support graphs,
-- `Remove`/`AddDerived` semantics (remove + derive + tie behavior),
-- panic path when derived origin is missing,
-- `into_owned`/`load` support remap.
-
-### 16) Existing tests
-
-Run focused tests first:
-
-- `cargo nextest run -p ty_python_semantic`
-- mdtests as needed:
-  - `cargo nextest run -p ty_python_semantic --test mdtest -- mdtest::<path>`
-
-Then broader checks per repo conventions.
-
----
-
-## Performance validation
-
-### 17) Instrumentation and sanity checks
-
-Collect before/after metrics:
-
-- support-expression node counts (`OrderedUnion`, `Remove`, `AddDerived`),
-- flattened support lengths at consumption sites,
-- flatten invocation counts,
-- wall time in representative mdtests/code-nav runs,
-- memory impact from non-hash-consed support-expression nodes.
-
-Implementation note:
-
-- add lightweight temporary counters for this validation, and remove them from final landed code unless we decide to keep them as permanent diagnostics.
-
-Expectation:
-
-- lower CPU in BDD construction/hot combinators,
-- potentially higher memory and flatter-consume cost.
-
----
-
-## Risks and mitigations
-
-1. **Support-expression tree growth (memory)**
-   - Mitigation: intentional Phase-1 tradeoff; measure and revisit with optional memo/hash-consing later.
-2. **Flatten correctness subtleties**
-   - Mitigation: single `build_support` implementation + strong unit tests.
-3. **Ordering drift in diagnostics/snapshots**
-   - Mitigation: all ordering consumers rely on flattened rank map.
-4. **Quantification provenance bugs**
-   - Mitigation: explicit invariants; panic on missing origin; dedicated tests.
-5. **Repeated flatten overhead in some paths**
-   - Mitigation: measure with temporary counters; consider flatten memoization follow-up if needed.
-
----
-
-## Concrete implementation checklist
-
-- [x] Add `SupportId` and initial support-node storage tables.
-- [x] Add support-expression constructors on builder (no support-node hash-consing).
-- [x] Add `build_support` with `FxIndexSet` accumulator dedupe.
-- [x] Add `support` to `ConstraintSet` and flattened support payload to `OwnedConstraintSet`.
-- [x] Thread support expressions through constructors/combinators.
-- [x] Replace `Quantified` support payload with flattened `Remove`/`AddDerived` node types and builder APIs.
-- [x] Update `distributed_or`/`distributed_and` and `when_any`/`when_all` to combine support in balanced-tree order.
-- [x] Remove temporary `support_from_node` reconstruction path entirely.
-- [x] Encode abstraction-derived ordering via `Remove`/`AddDerived` support nodes.
-- [x] Convert ordering consumers to flattened support rank maps. _(load-bearing consumer complete: `NodeId::solutions`; remaining `source_order` uses are bookkeeping/debug paths removed in Step H)_
-- [ ] Remove node `source_order` fields and offset APIs.
-- [x] Run tests and update snapshots if needed.
-
----
-
-## Execution order with concrete code touchpoints
-
-### Step A — add support-expression IDs and storage
-
-File: `crates/ty_python_semantic/src/types/constraints.rs`
-
-1. Add `UnionSupportId`, `RemoveSupportId`, and `AddDerivedSupportId` (`#[newtype_index]`).
-2. Add `SupportId` enum (`Empty`, `Singleton`, `OrderedUnion`, `Remove`, `AddDerived`).
-3. Extend `ConstraintSetStorage` with:
-   - `union_supports: IndexVec<UnionSupportId, UnionSupportData>`
-   - `remove_supports: IndexVec<RemoveSupportId, RemoveSupportData>`
-   - `add_derived_supports: IndexVec<AddDerivedSupportId, AddDerivedSupportData>`
-4. If needed, add lightweight scratch state for iterative flatten traversal (e.g., reusable explicit stack buffers).
-
-### Step B — builder APIs and flatten implementation
-
-File: `crates/ty_python_semantic/src/types/constraints.rs`
-
-1. Add support constructors (`empty`, `singleton`, `ordered_union`, `remove`, `add_derived`).
-2. Implement `build_support(expr) -> FxIndexSet<ConstraintId>`:
-   - iterative walk,
-   - `FxIndexSet` accumulator for dedupe/order,
-   - deterministic lhs-before-rhs.
-3. Implement clear per-node accumulator operations (`Empty`, `Singleton`, `OrderedUnion`, `Remove`, `AddDerived`).
-4. Add/adjust reusable traversal scratch only if profiling indicates allocation churn in flatten.
-
-### Step C — thread support through structs and constructors
-
-File: `crates/ty_python_semantic/src/types/constraints.rs`
-
-1. Add `support: SupportId` to `ConstraintSet`.
-2. Add `support: Box<[ConstraintId]>` to `OwnedConstraintSet`.
-3. Replace `from_node` with `from_node_and_support`.
-4. Update `always`, `never`, `from_bool`, atomic constructors.
-
-### Step D — update `into_owned` / `load`
-
-File: `crates/ty_python_semantic/src/types/constraints.rs`
-
-1. `into_owned`: flatten and persist support list.
-2. `load`: remap persisted support constraints and rebuild support expression.
-
-### Step E — combinator updates
-
-File: `crates/ty_python_semantic/src/types/constraints.rs`
-
-Update first:
-
-- `union`, `intersect`, `and`, `or`, `implies`, `iff`, `negate`
-
-Rule:
-
-- binary ops create `ordered_union_support(lhs.support, rhs.support)`
-- unary negate keeps support unchanged.
-
-Then audit all remaining `from_node(...)` sites.
-
-### Step E.1 — restore balanced iterator combining and carry support through it
-
-File: `crates/ty_python_semantic/src/types/constraints.rs`
-
-- Keep `when_any`/`when_all` using `NodeId::distributed_or` / `NodeId::distributed_and` (balanced tree fold behavior).
-- Add support-aware equivalents of distributed folding so support is combined in the same balanced shape (instead of reconstructing via `support_from_node`).
-- `support_from_node` is a strict temporary migration bridge and **must be removed** before final landing.
-
-### Step E.2 — flatten quantified support representation (**completed**)
-
-File: `crates/ty_python_semantic/src/types/constraints.rs`
-
-1. Replace `Quantified` support node representation with two node kinds:
-   - `Remove(base, constraint)`
-   - `AddDerived(base, origin, derived)`
-2. Replace corresponding storage/index types and builder constructors.
-3. Update `build_support` operations to handle `Remove` and `AddDerived` directly.
-4. Ensure missing origin is a hard panic in `AddDerived` handling.
-
-### Step F — quantification support node wiring (**completed**)
-
-File: `crates/ty_python_semantic/src/types/constraints.rs`
-
-1. In abstraction/reduction flows, build `Remove` and `AddDerived` support nodes rather than eagerly computing ranks.
-2. For multiple derived additions from one transform, create `AddDerived` nodes in reverse encounter order.
-3. Enforce invariant that origins must be present at build time (hard panic otherwise).
-4. Implementation approach used in landed code:
-   - thread `SupportId` directly through existing `NodeId`/`InteriorNode` quantification methods (instead of adding parallel `*_with_support` APIs),
-   - keep `ConstraintSet` as a thin wrapper,
-   - avoid temporary accumulator structs/collections for support deltas,
-   - in remove paths, record `AddDerived` before `Remove` so `origin` exists when `AddDerived` nodes are created.
-
-### Step G — migrate ordering consumers (**completed for load-bearing consumers**)
-
-File: `crates/ty_python_semantic/src/types/constraints.rs`
-
-1. `NodeId::solutions` sorting.
-2. `NodeId::path_assignments` ordering logic.
-3. Any other display/simplify sorting based on `source_order`.
-
-Current status:
-
-- ✅ `NodeId::solutions` now uses support-aware path traversal (`for_each_path_with_support`) and support-rank ordering.
-- ✅ No additional load-bearing ordering consumers require migration in Step G.
-- ℹ️ Remaining `source_order`-dependent code paths (`PathAssignments` bookkeeping, simplification/display ordering, graph-debug output) are tied to interior-node `source_order` fields and are expected to be removed in Step H.
-
-Pattern:
-
-- flatten support once for the set,
-- build rank map,
-- sort by rank then `ConstraintId` fallback.
-
-### Step H — remove source-order fields and offset APIs (Phase 2)
-
-File: `crates/ty_python_semantic/src/types/constraints.rs`
-
-1. Remove `source_order` / `max_source_order` from node data.
-2. Remove `with_adjusted_source_order` and `*_with_offset` APIs + cache keys.
-3. Update all call sites.
-
-### Step I — tests and verification
-
-1. Add/adjust support tests.
-2. Run:
-   - `cargo nextest run -p ty_python_semantic`
-3. Snapshot accept if needed:
-   - `cargo insta accept`
-
----
-
-## Persisted context / handoff notes
-
-### Confirmed design decisions
-
-1. Support construction should be cheap; defer support calculation until needed.
-2. No support-expression nodes are **hash-consed** in Phase 1 (`OrderedUnion`, `Remove`, and `AddDerived` included).
-3. Flattening is centralized in builder (`build_support`) and uses an `FxIndexSet<ConstraintId>` accumulator.
-4. `OwnedConstraintSet` persists flattened support, not support-expression graph.
-5. `load` rebuilds support as a left-associated `OrderedUnion` chain of singleton nodes.
-6. Missing origin for derived support is a programmer error (hard panic).
-7. Relative ordering/tie-breaking comes from support-graph structure; no extra tie-break metadata initially.
-8. `support_from_node` is temporary-only and must not remain in the final implementation.
-9. Rationale for (8): support is being separated from BDD structure specifically so we can eventually move to fully reduced BDDs, where node shape cannot be relied on to reconstruct support.
-10. For quantification wiring, prefer updating the existing `NodeId` / `InteriorNode` abstraction methods to return `(NodeId, SupportId)` directly, rather than introducing duplicate `*_with_support` method families.
-11. Avoid allocation-heavy intermediate “support change” aggregators; record support operations (`AddDerived`, `Remove`) inline while walking abstraction paths.
-12. In remove paths, construct derived-support operations before the remove operation so `AddDerived.origin` is guaranteed to be present when each node is created.
-
-### Invariants to preserve
-
-For any materialized support list from `build_support`:
-
-- each `ConstraintId` appears at most once,
-- ordering is deterministic,
-- ordered union is lhs-first,
-- derived constraints honor origin-rank semantics.
-
-### Suggested quick greps
-
-- `rg -n "ConstraintSetBuilder|ConstraintSetStorage|ConstraintSet::from_node|OwnedConstraintSet|into_owned\(|load\(" crates/ty_python_semantic/src/types/constraints.rs`
-- `rg -n "source_order|max_source_order|_with_offset|other_offset|with_adjusted_source_order" crates/ty_python_semantic/src/types/constraints.rs`
-- `rg -n "solutions\(|path_assignments\(|positive_constraints\(" crates/ty_python_semantic/src/types/constraints.rs`
-
----
-
-## Notes
-
-- Keep semantic churn minimal in Phase 1: support-expression recording + lazy flatten.
-- Keep fully reduced BDD work separate after migration stabilizes.
-- Keep support-expression ID types private to `constraints.rs`.
-- Consider flatten memoization only if profiling indicates repeated-flatten overhead.
-