transform: add equality-saturation MIR optimizer (mz_transform::eqsat)

Introduce an equality-saturation optimizer that lowers a subset of
MirRelationExpr into an e-graph, applies confluent rewrite rules plus
congruence closure to a bounded fixpoint, and extracts the cheapest
equivalent plan under a two-axis (memory-first, time-second) cost model.

The pass registers in the logical and physical optimizers behind per-phase
feature flags, equivalence- and type-preserving at the live boundary
(adopt_if_type_preserving), with a MAX_PLAN_SIZE guard. It reuses the
production CanonicalizeMfp, Demand, and ProjectionPushdown machinery after
raise, and seeds index availability and literal-filter lookups from the
oracle in the physical phase.

Includes: the Rel IR with opaque bail, lower/raise round-trip, the saturation
engine with budgets and scope peeling for Let/LetRec, lattice e-class analyses
(NonNeg, Keys, Monotonic, Equivalences, ConstantColumns), greedy and ILP
extractors, extraction-time CSE, a build-time rule DSL with per-rule codegen,
a pluggable join orderer (DpSub default, Dpccp, DphypBushy), a Lean 4
soundness-spec emitter, and the architecture reference doc.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019m58NEHNTg4NQ2YuQmrpzQ

Author: antiguru

.superpowers/sdd/e1-report.md

@@ -0,0 +1,67 @@
+# E-T1 Report: Wire CSE into the live path
+
+## Changes
+
+### raise.rs: scope-threaded raise
+
+Refactored `raise(rel, commit_wcoj)` to delegate to `raise_inner(rel, commit_wcoj, scope: &mut BTreeMap<usize, ReprRelationType>)`.
+The `Rel::Let` arm now raises the value, calls `.typ()` on the result, inserts `(id, typ)` into scope, raises the body, and removes the id from scope on exit.
+The `Rel::LocalGet { get: None }` arm now looks up `scope[id]` and emits `MirRelationExpr::Get { id: Id::Local(LocalId::new(u64::cast_from(id))), typ: scope[id].clone(), access_strategy: AccessStrategy::UnknownOrLocal }`.
+The `Rel::LocalGet { get: Some(g) }` arm returns `g.clone()` unchanged (existing behavior preserved).
+Imports added: `std::collections::BTreeMap`, `mz_expr::{AccessStrategy, Id}`.
+
+### cse.rs: fresh ids + closed-subtree guard
+
+Fresh ids: added `max_local_id(rel)` walker that collects the maximum id from all `Rel::Let` and `Rel::LocalGet` nodes; CSE ids now start at `max + 1`.
+
+Closed-subtree guard (the key bug fix): added `is_closed(rel)` which returns false if the subtree contains any `Rel::LocalGet { get: Some(_) }` or `Rel::Let` nodes.
+Updated `worth_binding` to require `is_closed`: CSE only binds subtrees that do not reference lower'd locals.
+Without this guard, CSE would hoist subtrees like `Project(Get l2)` OUTSIDE the scope where `l2` is defined, causing Typecheck to panic with "l2 is unbound".
+
+### eqsat.rs: call CSE in live path
+
+Added `let best = crate::eqsat::cse::eliminate_common_subexpressions(&best);` between extraction and raise in `optimize_inner`, with a comment explaining it subsumes RelationCSE.
+
+## Datadriven witness
+
+Case (j) in `eqsat.spec`: a Union of two identical `Filter(#0 = 1)(Get t0)` branches.
+The extracted plan has the filter as a shared subterm.
+After CSE, the output shows a `With` (Let) binding:
+
+```
+With
+  cte l1 =
+    Filter (#0 = 1)
+      Get t0
+Return
+  Union
+    Get l1
+    Get l1
+```
+
+A `Let` binding appears as expected.
+
+## arithmetic.slt gate result
+
+Command: `bin/sqllogictest --optimized -- test/sqllogictest/arithmetic.slt`
+Wall time: ~3:31
+Pass count: 206/206
+Typecheck panic: none
+Non-positive multiplicity: none
+
+## Test summary
+
+* `cargo test -p mz-transform --lib eqsat`: 53 passed (includes new `raise_cse_let_with_placeholder_local_get` test)
+* `cargo test -p mz-transform --test test_transforms`: 1 passed (datadriven, including CSE witness case (j))
+* `cargo test -p mz-transform --test wcoj_decision`: 6 passed
+* `cargo test -p mz-transform --test roundtrip`: 22 passed
+* `cargo test -p mz-transform --test compare_real`: 1 passed
+* `cargo clippy -p mz-transform`: clean
+* `bin/lint`: failures only for `buf`/`trufflehog` (infra tools not installed, expected)
+
+## Concerns
+
+The `is_closed` guard restricts CSE to subtrees that contain no lowered-local references.
+This is conservative: a shared subtree that references a lower'd local could in principle be bound within its defining scope.
+However, the simpler approach (no scope-aware hoisting) is correct and sufficient for the e-graph use case: the e-graph never produces Let/LocalGet nodes itself (it bails to opaque leaves for LetRec), so the only locals in the extracted tree come from original MIR Lets, which are preserved verbatim.
+The CSE still binds shared compound subterms that are "pure" (no local references), which covers the common case of a shared filtered or projected base table.

Cargo.lock

@@ -319,6 +319,7 @@ cc = "1.2.62"
 cfg-if = "1.0.4"
 chrono = { version = "0.4.39", default-features = false, features = ["clock", "serde", "std"] }
 chrono-tz = { version = "0.8.1", features = ["case-insensitive", "serde"] }
+chumsky = "0.13.0"
 clap = { version = "4.6.1", features = ["derive"] }
 clap_complete = "4.6.2"
 columnar = "0.13.0"
@@ -363,6 +364,7 @@ futures-task = "0.3.32"
 futures-util = "0.3.32"
 gcp_auth = "0.12.6"
 glob = "0.3.3"
+good_lp = { version = "1.15", default-features = false, features = ["microlp"] }
 globset = "0.4.18"
 governor = "0.10.1"
 half = "2"

Cargo.toml

@@ -32,6 +32,7 @@ copyright_files=$(grep -vE \
     -e '(^|/)Cargo\.lock$' \
     -e '(^|/)types\.lock$' \
     -e '(^|/)\.mzprofile$' \
+    -e '(^|/)lean-toolchain$' \
     -e '^src/mz-deploy/src/cli/scaffold/gitignore$' \
     -e '^test/mz-deploy/projects/multi-profile/v1/models/app/core/ambiguous\.sql$' \
     -e '^about\.toml$' \

ci/test/lint-main/checks/check-copyright.sh

@@ -206,6 +206,7 @@ wrappers = [
     "globset",
     "launchdarkly-server-sdk",
     "launchdarkly-server-sdk-evaluation",
+    "microlp",
     "native-tls",
     "opendal",
     "os_info",