doc/semantics: Lean 4 mechanization of UnifiedStream error semantics#36614
Draft
antiguru wants to merge 119 commits into
Draft
doc/semantics: Lean 4 mechanization of UnifiedStream error semantics#36614antiguru wants to merge 119 commits into
antiguru wants to merge 119 commits into
Conversation
Add design doc proposing per-cell `Datum::Error`, row-scoped errors via
the existing `DataflowError`, and a diff-semiring sketch for
collection-scoped errors. Define the four-valued AND/OR truth tables
({TRUE, FALSE, NULL, ERROR}) that the rest of the spec rests on.
Add a v1 Lean 4 mechanization of the boolean fragment at
doc/developer/semantics/. The skeleton models `Datum`, `Expr`,
`evalAnd`/`evalOr`, and proves all 32 cells of the AND/OR truth tables.
The pattern order in `evalAnd`/`evalOr` matches the current Rust
runtime in src/expr/src/scalar/func/variadic.rs; deviating from that
runtime requires a corresponding diff in Boolean.lean.
CI runs lake build in a self-built Docker image (ubuntu:26.04 + elan +
lean-toolchain pin), gated on changes under doc/developer/semantics/.
No Mathlib dependency.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Expand the Lean skeleton with a small set of follow-up theorems that
the optimizer roadmap depends on.
* `Datum.IsErr` propositional predicate plus `DecidablePred` instance,
for use as a hypothesis in algebraic laws.
* `Expr.not` constructor and `evalNot`, with the 4-cell `NOT` truth
table and `not_not` (involution on the boolean fragment, no-op on
`null` and `err`).
* New `Mz/Laws.lean`:
- `evalAnd_idem`, `evalOr_idem`: idempotence holds unconditionally,
including on `err` (same error preserved).
- `evalAnd_comm_of_no_err`, `evalOr_comm_of_no_err`: commutativity
conditional on neither operand being an error. This is the law an
optimizer that has run `might_error` analysis can use to justify
conjunct reordering. Unconditional commutativity fails over
`(err e₁, err e₂)` with distinct payloads.
Associativity and `might_error` soundness are deferred.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Land the optimizer-facing theorem the previous commit's roadmap called
out as priority one.
* Switch `eval` for `.ifThen` to a strict `evalIfThen` helper. The
observable `Datum` is identical to the lazy form in this total
skeleton (both branches are total functions); strictness collapses
the ifThen proof case to a single `cases` on the condition.
* Redefine `Env.get` by primitive recursion so inductive proofs can
`cases` on the defining equations directly without going through
`List.getD`.
* New `Mz/MightError.lean`:
- Per-operator helper lemmas: `evalAnd_not_err`, `evalOr_not_err`,
`evalNot_not_err`, `evalIfThen_not_err`.
- `Expr.might_error` conservative analyzer (literal err taints
every ancestor; columns assumed err-free).
- `Env.ErrFree` predicate and `Env.get_not_err` lemma.
- `might_error_sound`: if `¬e.might_error` and `env.ErrFree` then
`¬(eval env e).IsErr`. Structural induction on `e`, one helper
per Expr constructor.
* `Mz/Laws.lean`: lift `evalAnd_comm_of_no_err` and
`evalOr_comm_of_no_err` through `eval` via `might_error_sound`,
giving `Expr`-level reorder-safety theorems
`eval_and_comm_of_no_might_error` and
`eval_or_comm_of_no_might_error`. These are the laws an optimizer
would cite when reordering conjuncts in the boolean fragment.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* `ErrStrictUnary`, `ErrStrictBinary`, `NullStrictUnary` predicates capturing per-position strictness. The cell-scoped analogue of PostgreSQL's `STRICT` qualifier on `NULL`, applied to `err`. * Positive instances: `evalNot` is both err-strict and null-strict; the condition slot of `evalIfThen` is err-strict. * Closure: `ErrStrictUnary.comp` proves strictness is preserved under function composition, which is the property an optimizer relies on when fusing chains of strict scalar functions into a single MFP expression. * Negative results: `evalAnd` and `evalOr` are not err-strict in either argument position. The counterexamples (`FALSE AND ERR`, `TRUE OR ERR`) are also canonical regression tests — a future change to AND/OR that promoted these cells to `ERR` would break exactly these proofs. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add `evalCoalesce : List Datum → Datum` and prove the laws that characterize the proposed cell-scoped coalesce. Semantics: walk operands left to right; return the first concrete value. When none exists, apply a `null`-beats-`err` tiebreak — if any operand was `null`, return `null`; otherwise, return the first `err`. The state machine in `Coalesce.go` tracks a `seenNull` sticky bit and a first-`err` payload. The defining error-rescue property (`coalesce_err_rescue_bool`) and its symmetric null-rescue (`coalesce_null_rescue_bool`) together establish that a later concrete operand rescues an earlier `err` exactly as it rescues an earlier `null`. This is the explicit, user-controllable error trap referenced in the design doc. The `null`-beats-`err` tiebreak (`coalesce_null_then_err`, `coalesce_err_then_null`) preserves the PostgreSQL behavior users expect when all operands are NULL, and is dual to the strict-function rule documented in `Mz/Strict.lean`: strict functions promote `err` above `null` in per-cell results; `coalesce` is non-strict and demotes `err` below `null` in the tiebreak. Defer wiring `evalCoalesce` into `Expr` as a `.coalesce` constructor until the variadic `And`/`Or` ctors land — the termination story is shared between them. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add the missing identity laws and the variadic-fold counterparts of
the binary AND/OR evaluators.
* `Mz/Laws.lean`: `TRUE` is the two-sided identity for `evalAnd` and
`FALSE` is the two-sided identity for `evalOr`. The proofs verify
each cell of the non-identity argument. These identities are also
the seed values used by the variadic folds.
* `Mz/Variadic.lean`: `evalAndN`, `evalOrN : List Datum → Datum`
defined by right-fold. Right-fold gives the cons recurrence by
`rfl` and avoids the associativity argument a left-fold would
require.
- Cons recurrence, nil, singleton, and binary equivalence with
`evalAnd` / `evalOr`. The binary equivalence is the bridge that
transports every binary truth-table cell and algebraic law to
the variadic form on lists of length two.
- Absorption theorems: a single `FALSE` anywhere in the operand
list forces `evalAndN` to `FALSE`; symmetric statement for
`TRUE` and `evalOrN`. These justify the runtime short-circuit
optimization.
Wiring `evalAndN`, `evalOrN`, and `evalCoalesce` into `Expr` as
list-carrying constructors is deferred — the termination story for
the nested inductive is shared between them and is best landed in a
single commit once it's been validated.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add `.andN`, `.orN`, and `.coalesce` to `Expr` as variadic constructors carrying `List Expr`, with the corresponding `eval` clauses and Expr-level reduction lemmas. The variadic primitives (`evalAndN`, `evalOrN`, `evalCoalesce`) move to a new `Mz/PrimEval.lean` to avoid the circular dependency that would otherwise arise between `Mz/Eval.lean` and the variadic-law files. File reorganization: * New `Mz/PrimEval.lean`: every evaluator that operates on `Datum` or `List Datum` without referring to `Expr` — the binary boolean primitives, the environment, and the variadic primitives. * `Mz/Eval.lean` shrinks to the `eval : Env → Expr → Datum` definition. * `Mz/Variadic.lean` and `Mz/Coalesce.lean` drop their now-moved evaluator definitions and keep only the theorems. * `Mz/Boolean.lean` and `Mz/Strict.lean` switch their imports to `Mz.PrimEval` since they never used the Expr-level evaluator. `might_error_sound`: * `induction` cannot be used on the now-nested-inductive `Expr`, so the soundness proof is rewritten as a recursive `theorem` that pattern-matches the constructor and recurses on subexpressions. The signature also makes `env` explicit so the recursive calls in compound cases stay readable. * The list-carrying constructors are handled vacuously: the conservative `might_error` for them returns `true` unconditionally, so the soundness premise is absurd in those cases. A future refinement will tighten the analyzer to inspect operands. New `Mz/ExprVariadic.lean`: * `eval_andN`, `eval_orN`, `eval_coalesce` connect the Expr-level evaluator to the variadic primitives. * Empty / singleton cases for all three. * Binary equivalence: `eval env (.andN [a, b]) = eval env (.and a b)` and the dual for `.orN`, transporting `Mz/Variadic.lean`'s binary laws through `eval`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ness Refine `Expr.might_error` for the `andN` and `orN` list-carrying constructors so the analyzer is no longer maximally conservative for them. The analyzer now recurses into the operand list via `Expr.argsMightError`, declared mutually with `Expr.might_error` so Lean's structural-recursion checker accepts both sides without an explicit termination measure. `Expr.argsMightError_of_mem` is the membership-driven introduction form needed by the soundness proof — it turns "some operand might error" into the bool fold. Its contrapositive is what extracts a per-operand non-erroring hypothesis from the analyzer's verdict on the whole list. `might_error_sound` for the `.andN` and `.orN` constructors now performs real work: * Reduce `eval env (.andN args)` to `evalAndN (args.map (eval env))` via the existing `simp only [eval]` pattern. * Apply the list-level `evalAndN_not_err` (also added in this commit) with a per-operand non-erroring hypothesis. * Extract that per-operand hypothesis by destructuring `List.mem_map` and applying `Expr.argsMightError_of_mem` contrapositively against `hMe`. * Recurse via `might_error_sound` on the individual operand. `.coalesce` is still tainted unconditionally — the rescue analysis is a separate follow-up since the helper `evalCoalesce_not_err` needs a different list induction (state-machine over `Coalesce.go`). `Expr.might_error` and `Expr.argsMightError` are now mutually recursive, which forces well-founded compilation. Existing `simp only [Expr.might_error]` patterns in the proof are unaffected because they target equation lemmas, not definitional reduction. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Refine `Expr.might_error` for the `.coalesce` constructor so the analyzer captures the rescue rule: `coalesce` might error only when every operand might error (and the operand list is non-empty). A single statically-safe operand makes the whole expression safe. Analyzer changes (mutual block): * `Expr.argsAllMightError`: companion fold to `argsMightError`, empty-list base `true`, cons case `e.might_error && rest...`. * `.coalesce []` returns `false` (empty coalesce is `.null`, never errors). * `.coalesce (a :: rest)` returns `a.might_error && argsAllMightError rest`, which is equal by definition to `argsAllMightError (a :: rest)`. Soundness chain for the `.coalesce` case: 1. `Expr.exists_safe_of_not_argsAllMightError` extracts a statically-safe operand from the negation of the analyzer. 2. `might_error_sound` recurses on that operand and produces a not-`IsErr` witness on its evaluated value. 3. `Coalesce.go_not_err` (new) is the state-machine lemma: any `Coalesce.go` invocation whose remaining list contains at least one non-erroring datum (or whose `seenNull` is already set) does not return an error. Proof is structural recursion on the list, plumbing the safety witness through the `.null` and `.err` arms. 4. `evalCoalesce_not_err_of_some_safe` packages the above into the surface lemma soundness invokes. `Coalesce.go` is made non-private in `Mz/PrimEval.lean` so the state-machine lemma can reference it. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add the `Expr`-level absorption theorems that an optimizer cites when folding a variadic `AND` containing a `FALSE` operand to `FALSE` (symmetric for `OR` with `TRUE`). Two forms each: * Semantic premise: `(∃ e ∈ args, eval env e = .bool false) → eval env (.andN args) = .bool false`. Sufficient for any operand the optimizer has reduced to a constant boolean. * Syntactic premise: `Expr.lit (.bool false) ∈ args → eval env (.andN args) = .bool false`. The corollary specialized to the case where a literal `.bool false` is syntactically present in the operand list. Useful for simple constant folding. Each proof reduces `eval env (.andN args)` to `evalAndN (args.map (eval env))` via `eval_andN`, then witnesses membership of `.bool false` in the mapped list through `List.mem_map`, then invokes `evalAndN_false_absorbs` from `Mz/Variadic.lean`. The `Or`/`True` direction is symmetric. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Model relations as `List Row` and define the two basic relational operators on top of the per-row evaluator. * `filterRel pred rel` keeps rows whose predicate evaluates to `.bool true`. Rows evaluating to `.bool false`, `.null`, or `.err` are dropped. The skeleton silently drops `err` rows; a real implementation would route them to a separate error collection. Noted in the docstring as a known modelling gap. * `project es rel` evaluates each scalar in `es` against every row and produces a relation whose row width is `es.length`. Laws: * `filterRel_idem`: applying the same predicate twice is the same as applying it once. Proof: `List.filter_filter` + `Bool.and_self`. * `filterRel_comm`: filter commutes with filter. Proof: `List.filter_filter` twice + `Bool.and_comm`. * `project_length`: projection preserves cardinality. Direct consequence of `List.length_map`. * `project_nil`: the empty projection collapses every row to `[]`. All proofs are one-liners over Lean core's list lemmas; the laws themselves are the first relational-level rewrites an optimizer cites. Predicate pushdown across projection, joins, and aggregates remain follow-ups. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Model the dataflow's data and error collections as a pair carried together through operators, mirroring the structure of the real Materialize dataflow where erroring rows are routed to a separate collection rather than silently dropped. * `BagStream` is a structure with `data : Relation` and `errors : List EvalError`. * `BagStream.ofRelation` injects a plain relation with no accumulated errors. * `BagStream.filter pred s` evaluates `pred` on every row of `s.data`. Survivors (`.bool true`) stay in the data field; erroring rows contribute their payloads to the error field via `errorRows`; everything else is dropped. Two helper lemmas carry the structural fact "predicate evaluated to `.bool true` on every survivor of `filterRel`": * `rows_in_filterRel_eval_to_true` unfolds the survival condition. * `errorRows_eq_nil_of_all_true` says a relation where every row evaluates to `.bool true` contributes no errors. `errorRows_filterRel` combines them and is the key fact behind `BagStream.filter_idem` — the second pass of an idempotent filter sees only survivors of the first, so it contributes no new errors. The overall stream is therefore unchanged on the second filter, at both the data and the error level. `BagStream.project` and stream-level filter commutativity follow in later iterations; commutativity at the error level requires multiset equality on `List EvalError` since list order differs across permutations. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add the classical relational rewrite: filterRel p (project es rel) = project es (filterRel (p.subst es) rel) The rewrite lets an optimizer move a `WHERE` clause through a `SELECT` clause by substituting the projection's source scalars into the predicate's column references. * `Expr.subst es e` replaces each `Expr.col i` in `e` with the i-th scalar of `es`, with out-of-bounds references defaulting to `.lit .null` so the result still evaluates to `.null`. Defined mutually with `Expr.substArgs` for the nested-list constructors (`andN`, `orN`, `coalesce`). * `Expr.substArgs_eq_map` bridges the recursive helper to the more ergonomic `args.map (·.subst es)` form for use in proofs. * `Env.get_map_eval` is the column-lookup compatibility lemma: reading column `i` from the projected row equals evaluating the i-th projection scalar against the original row. * `eval_subst` is the headline correctness theorem: substituting and then evaluating against the original row equals evaluating the unsubstituted expression against the projected row. Proof is structural pattern recursion mirroring `Expr.subst`. * `filterRel_pushdown_project` packages `eval_subst` plus `List.filter_map` + `List.filter_congr` into the relational form an optimizer cites. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Model the diff-field encoding of collection-scoped (global) errors proposed in the design doc. The standard differential dataflow diff type (typically `ℤ` for multiset counts) is extended with an absorbing `error` element; any sum or product involving `error` yields `error`, encoding "this collection is invalid at time `t`". * `DiffWithError α` is a two-constructor inductive: `val (x : α)` for ordinary diffs, `error` for the absorbing marker. * `Add`, `Mul`, `Zero`, `One` instances lift the underlying operations and respect the absorbing behavior. * Absorption laws (`error_add_left`, `error_add_right`, `error_mul_left`, `error_mul_right`) are the defining property. * Commutativity, associativity, and left-distributivity are proved parameterically over the underlying `α`: each lemma takes the corresponding law on `α` as a hypothesis and discharges the `DiffWithError` version by case analysis. The lemmas are not packaged as `Semiring`/`CommRing` typeclass instances because the skeleton avoids depending on Mathlib for build-time reasons. Adding the typeclass wiring is straightforward once Mathlib is on the dependency list. Tying `DiffWithError` to an actual `(Row, Time, Diff)` triple stream and proving the operator-level propagation theorems is the next step; the present file lays the algebraic groundwork those theorems rely on. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Model the spec's preferred encoding where data rows and errors flow through one collection rather than the `(data, errors)` pair carried by `BagStream`. The split form in `Mz/ErrStream.lean` mirrors the current Materialize runtime; the unified form mirrors what the diff-semiring extension naturally produces (any record with an `error` diff is a row-scoped error, and the same encoding extends to collection-scoped errors). * `UnifiedRow` is a sum type — `row (r : Row)` or `err (e : EvalError)`. The bare `err` variant preserves the current property that errors carry no row context. * `UnifiedStream := List UnifiedRow`. * `UnifiedStream.ofBag` packs a `BagStream` (data rows first, errors second). `UnifiedStream.split` is its inverse, splitting the carrier back via `filterMap pickRow` / `filterMap pickErr`. * `UnifiedStream.filter` runs the predicate per record, routing erroring rows to `.err` records in place. Existing `err` records pass through unchanged — the carrier handles error propagation without per-operator boilerplate. Round-trip theorem `UnifiedStream.split_ofBag : split (ofBag s) = s` proved at both the data and error field level, using four private filterMap-over-tagged-list helpers and structural induction. The cross-direction `filter ∘ ofBag ≈ ofBag ∘ filter` is left for future work — equivalence is only up to multiset equality on errors because `ofBag` fixes a concat order between data and errors, while filters that interleave the two would produce a different list order. `@[ext]` added to `BagStream` so the round-trip proof can use `apply BagStream.ext`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`List.filterMap` was passed to four `simp` invocations in the filterMap-of-mapped-list helpers but never actually used in the rewriting — the cons recurrence and the `pickRow` / `pickErr` arms combined with the IH are enough. Drop the unused arg; the linter-clean.
Model the spec rule that SQL aggregates such as `SUM`, `MIN`, `MAX`, and `AVG` propagate `err` like strict scalar functions. NULLs are skipped (matching PostgreSQL's "ignore NULLs" reading); errors are propagated, with the first one in scan order winning. * `aggCountNonNull`: `COUNT(expr)` — counts rows whose value is neither `NULL` nor `err`. Matches PostgreSQL. * `aggStrict f`: variadic strict reduction parametric over the combiner `f`. Empty list (or list of only `NULL`s) returns `NULL`; any `err` returns the first `err`; non-`NULL`/`err` values are combined via `f`. Two propagation theorems: * `aggStrict_err`: any `err` input forces an `err` output. Proof by structural recursion on the list; the `.bool` case branches on `aggStrict f rest` and shows the `err` arm of the inner match is the one that fires. * `aggStrict_no_err`: dual statement under the additional hypothesis that the combiner preserves "no-err". Captures the precondition an aggregate operator can use to guarantee its output is not an error when its column is error-free. `try_*` aggregates (the non-strict variants that swallow `err` into `NULL`) are future work; they satisfy a coalesce-style law rather than strict propagation and warrant their own file once the spec side is clearer. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Model the proposed `try_sum`, `try_min`, etc. that swallow `err`
into `NULL` instead of propagating. Defined as a post-pass coalesce
on `aggStrict`:
aggTry f xs = match aggStrict f xs with
| err _ => null
| r => r
Equivalent reading via the existing `evalCoalesce`:
aggTry f xs = evalCoalesce [aggStrict f xs, .null]
The defining property `aggTry_no_err` says the result is never an
`err`. The companion `aggTry_eq_aggStrict_of_no_err` says the
non-strict variant agrees with the strict one whenever the strict
one would not have erred — so an optimizer that has already proved
the inputs error-free can swap `aggTry` for `aggStrict` (and vice
versa). Both lemmas reduce to case analysis on `aggStrict f xs`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Model the diff-only slice of differential dataflow's `compact` / consolidation operation: summing a list of `DiffWithError α` values and showing that an `error` diff absorbs the consolidated sum. * `DiffWithError.sumAll` sums a list of diffs starting from `0`, right-associative. The result lives in `DiffWithError α` for any base `α` with `Zero` and `Add` instances. * `sumAll_eq_error_of_mem`: the headline absorption theorem. If `error` appears anywhere in the list, the consolidated sum is `error`. Proof walks the list and uses the absorption laws from `Mz/DiffSemiring.lean` at the matching cons. * `sumAll_val_of_all_val`: companion no-error-preservation theorem. An all-`val` list sums to `val` of some `α`. The full `compact` operator also buckets records by `(row, time)`; that bucketing is orthogonal to the absorption argument and would require `DecidableEq Row` plus a time model, both follow-ups. The per-bucket inner sum modeled here is what an operator-level proof would invoke once those pieces are in place. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add `TimedRecord` and `TimedStream` to model differential dataflow's record format with errors. `Time := Nat`; the diff is `DiffWithError α` parametric in the base diff type. Operations: * `TimedStream.consolidateAll` sums every diff in the stream, ignoring row and time. The collection-wide diff. * `TimedStream.consolidateAt t` sums every diff at time `t`, ignoring row. The per-time collection diff. Both reduce to `DiffWithError.sumAll`, so the absorption laws from `Mz/Consolidate.lean` transport: * `consolidateAll_eq_error_of_mem`: any `error`-carrying record forces the all-stream consolidation to `error`. * `consolidateAt_eq_error_of_mem`: any `error`-carrying record at time `t` forces the per-time consolidation at `t` to `error`. Per-`(row, time)` bucketing — the form `compact` actually uses in the runtime — is the next refinement and requires `DecidableEq` on `Row`. The current sums are the collection-global diffs at each time slice, which is what operator-level proofs invoke once the bucketing is layered on. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…Stream Two-input relational join modeled on the unified single-collection stream. Cross product is the building block; predicate join is cross followed by `UnifiedStream.filter`. * `UnifiedStream.cross l r` produces one output record per `(lu, ru)` pair: both rows ⇒ concatenated row; either side `err` ⇒ that side's `err` (left wins on conflict, matching the binary AND's first-error rule). * `UnifiedStream.join pred l r := (cross l r).filter pred`. Error propagation falls out of the carrier: an `err` record on either side contributes one `err` to the output per record on the other side, matching the diff-semiring's `error * diff = error` intuition. Theorems: `cross_nil_left` and `cross_nil_right` cover the empty cases (joining anything with the empty stream is empty). The cardinality theorem `(cross l r).length = l.length * r.length` is deferred — needs `List.length_flatMap` + Nat arithmetic that the current skeleton's lemma toolkit handles awkwardly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Partition a relation by an evaluated key expression and aggregate per group. Closes the SQL `SELECT k, AGG(v) FROM r GROUP BY k` shape the rest of the algebra implies. * `Datum` derives `DecidableEq` (via the already-decidable `EvalError` payload) so keys can be compared at runtime. * `groupBy keyExpr rel` walks rows, evaluates the key on each, and inserts into the existing group with that key or starts a new one. Output is `List (Datum × Relation)`. * `aggregateBy keyExpr valExpr f rel` applies `aggStrict` to each group's evaluated value column, producing `List (Datum × Datum)` — one aggregated value per group. Spec divergence on `err` keys documented inline: the skeleton uses standard `DecidableEq Datum`, so two `Datum.err e` values with the same payload collapse into one group. The spec requires every err key to be its own group. The natural refinement is a custom `Datum.groupKeyEq` that returns `false` whenever either side is an err; left for future work. Theorems for now cover the trivial cases (empty, singleton). Cardinality (`sum of group sizes = rel.length`) is the next concrete law and is deferred until the lemma toolkit picks up the needed Nat / List arithmetic helpers. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add `Datum.groupKeyEq` — group-key equivalence that returns `false` whenever either side is `.err`, so two error keys never coalesce even if their payloads happen to match. Build `groupByErrDistinct` and `aggregateByErrDistinct` on top, leaving the existing `groupBy` / `aggregateBy` (which use derived `DecidableEq Datum`) in place as the more permissive variant. Theorems: * `Datum.groupKeyEq_err_left`: simp lemma reducing the err-left case to `false`. * `insertIntoDistinct_err`: inserting an err-keyed row into any group list appends a fresh singleton group at the end. * `groupByErrDistinct_length_of_all_err`: when every row's key evaluates to err, the output has one group per row — closes the spec-divergence note from the previous commit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`BagStream.project es s` projects each row in `s.data` through the list of scalar expressions `es`. A row stays in the data collection only when every scalar succeeds on it; otherwise the row's err payloads (one per erroring scalar) are appended to the error collection. Helpers: * `rowAllSafe`: every projected scalar succeeds on a row. * `rowErrs`: collect every err payload from one row's projections. * `projectErrs`: aggregate `rowErrs` across the relation. Laws: * `BagStream.project_data` / `_errors` — per-field reductions. * `BagStream.project_nil_es` — empty projection list keeps every row and produces width-zero output rows. * `BagStream.project_empty_data` — empty data collection projects to empty data, preserving input errors. * `rowErrs_nil_of_all_safe` and `projectErrs_eq_nil_of_all_safe` — when every scalar succeeds on every row, the error collection is unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`UnifiedStream.cross_length` proves the headline relational identity `(cross l r).length = l.length * r.length`. Cross product on the unified carrier produces exactly one output record per `(l, r)` pair regardless of which side carries an error — every err contributes one err record per element of the other side, matching the diff-semiring's `error * d = error`. Companion `UnifiedStream.filter_length_le` proves the predicate filter on the unified stream is non-expanding (each input produces zero or one output). Composing the two gives the corollary `UnifiedStream.join_length_le`: a join's output length is bounded above by `l.length * r.length`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`totalRows g = sum of g.rows.length` is the metric. Theorems: * `totalRows_insertInto`: a single insert adds exactly one row, whether the key matches an existing group or creates a new one. * `totalRows_insertIntoDistinct`: same bookkeeping for the err-distinct variant. * `totalRows_groupBy`: sum of group sizes equals the input relation's length — partitioning loses and duplicates nothing. * `totalRows_groupByErrDistinct`: the err-distinct variant preserves the same invariant. Use an explicit recursive `totalRows` definition instead of `((map ·.2.length).sum`. The latter trips `omega` because the elaborator and the simp set produce two syntactically distinct forms (`(·.2.length)` vs `List.length ·.snd`) that omega treats as independent atoms. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Promote `UnifiedStream` from `List UnifiedRow` to
`List (UnifiedRow × DiffWithError Int)`. Every record now carries
a differential-dataflow diff augmented with the absorbing `.error`
marker. Row-scoped errors still propagate through the `UnifiedRow`
carrier; collection-scoped errors propagate through diff
multiplication / addition.
Changes:
* `UnifiedStream.ofBag` tags every bag record with diff `.val 1`.
* `UnifiedStream.split` discards the diff component (round trip
still goes through because `ofBag` only emits `.val 1` diffs;
the cross-direction loses information for diffs ≠ `.val 1`).
* `UnifiedStream.filter` preserves the diff of survivors; rerouted
rows (predicate errs) keep their multiplicity.
* `UnifiedStream.cross` combines carriers via the new
`combineCarrier` helper and multiplies diffs through
`DiffWithError`'s `Mul` instance. A `.error` diff on either
side absorbs the product diff via
`DiffWithError.error_mul_{left,right}`.
New theorem `cross_diff_error_left` witnesses the absorption:
crossing a left-side `.error` diff with any record on the right
produces a `.error` diff in the output. Existing theorems
(`cross_length`, `filter_length_le`, `join_length_le`,
`split_ofBag`) carry through to the new representation.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Tighten diff propagation in `UnifiedStream.filter` and add the symmetric `cross` absorption theorem. `filter` now special-cases records carrying a `.error` diff, passing them through unconditionally regardless of predicate outcome. The previous version dropped such records when the predicate evaluated to `.bool false` or `.null`, which violates the semiring law that `.error` must absorb every downstream operator. `filter_length_le` still holds — each input still produces at most one output. Three new theorems witness the absorption: * `cross_diff_error_right`: symmetric counterpart to the existing `cross_diff_error_left` — a `.error` diff on the right side forces the output diff to `.error` for every record on the left. * `filter_preserves_error_diff`: a record `(uc, .error)` in the input survives the filter as `(uc, .error)` in the output, no matter what the predicate is. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`UnifiedStream.consolidate` buckets unified-stream records by carrier (data row or row-scoped err) and sums per-bucket diffs. Headline theorem `consolidate_preserves_error` lifts the diff-semiring absorption rule from `Mz/Consolidate.lean` to the unified stream: an `.error` diff anywhere in the input forces a `.error` diff in the consolidated output for that carrier. Required: * `deriving DecidableEq` on `UnifiedRow` (Row already has it via `Datum`, EvalError too). * Two helper lemmas — `consolidateInto_error_diff` (inserting an `.error` diff yields `.error` for the bucket) and `consolidateInto_preserves_error_mem` (a pre-existing `.error` record survives every subsequent insert). Adding times reduces to running `consolidate` inside each time slice; that lifting is mechanical and left for the per-`(row, time)` follow-up alongside `Mz/Triple.lean`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two companion theorems for `UnifiedStream.consolidate`. `consolidate_length_le`: bucketing only merges, never expands. The output has at most as many records as the input. Helper `consolidateInto_length_le_succ` bounds a single insert at `us.length + 1`. `consolidate_no_error`: if every input diff is `.val n`, every output diff is `.val m`. The diff-semiring's `.val + .val = .val (· + ·)` keeps the consolidated buckets in the ordinary `Int` slice, so `.error` is the only source of absorption. Together with the existing `consolidate_preserves_error`, the three theorems pin down the consolidation operator: absorption on errors, non-expansion on cardinality, and stability on error-free input. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add per-file documentation for the new error-scope work. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add Mz/JoinPushdown.lean with the optimizer's canonical
join-pushdown rewrite:
filter pred (cross l r) = cross (filter pred l) r
when pred references only left-input columns. Earlier abandoned
attempt at this proof failed on the show-tactic pattern matching;
this retry succeeds via:
* IsPureData predicate on r (no .err carriers, no .error diffs)
— required because combineCarrier's left-wins rule and the
absorbing .error * d = .error rule disagree across the two
sides without it.
* cross_singleton reduction lemma with carrier/diff split out
(avoids .fst/.snd projections that block later rfls under
induction).
* Per-record helpers for each left-record shape:
- filter_map_error_diff: .error diff passes through.
- filter_map_err_carrier: .err e left, .val diff.
- filter_map_row_val_keep: .row la, eval = .bool true.
- filter_map_row_val_err: .row la, eval = .err — cell-to-row
promotion site.
- filter_map_row_val_drop: .row la, eval rejects.
Main theorem filter_cross_pushdown_left assembles these via
structural induction on l plus eval_append_left_of_bounded.
Caveats encoded in the hypotheses:
* hLWidth (∀ row la in l, la.length ≥ N) — needed because
eval_append_left_of_bounded requires bounded by la.length.
* hRPure (IsPureData r) — without it, attribution conflicts
arise (left .row pred-errs vs right .err records;
.error diff in r interacts with filter's first arm).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add UnifiedStream.negate_filter: negate (filter pred us) = filter pred (negate us) Earlier abandoned attempt failed on pattern-match shows; this retry succeeds via per-record case analysis with computed reduction lemmas for each filter branch. Holds unconditionally — no hypothesis on pred or stream content. Filter's row arm depends on eval r pred which is independent of diff sign, so the negate slides through. Cases handled: * (uc, .error): filter passes through, .error negates to .error. * (.err e, .val n): filter passes through, both orderings give (.err e, .val -n). * (.row r, .val n) with eval = .bool true: keep, diff flips. * (.row r, .val n) with eval = .err e_pred: cell-to-row promotion preserved by negate. * (.row r, .val n) with eval drops: both orderings give []. Enables optimizer rewrites that commute negation with filter (EXCEPT ALL paths, retraction reordering). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ptAll corollaries Partial error-scope characterization for the clamp operators: * clampPositive_errorDiffCarriers_iff: equality. .error records always pass through (isPositiveDiff .error = true), so the collection-err set is preserved exactly. * clampPositive_errCarriers_of_mem: reverse direction only. clampPositive may drop (.err e, .val 0) records, so the row-err set may shrink. Forward direction fails. Same shape for clampToOne, with the case analysis tracking clampToOne's three branches (.error keep, .val n>0 collapse, .val n≤0 drop). clampToOne_error_inv: a (uc, .error) in clampToOne output came from a (uc, .error) input. The .val arms never emit .error. Composed corollaries: * distinct_errorDiffCarriers_iff / distinct_errCarriers_of_mem: distinct = clampToOne ∘ consolidate. * bagExceptAll_errorDiffCarriers_iff / bagExceptAll_errCarriers_of_mem: bagExceptAll = clampPositive ∘ exceptAll. bagIntersectAll deferred — intersectAll's lookup-based definition needs separate analysis before composition. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three reverse-direction theorems for intersectAll-family: * intersectAll_errCarriers_of_mem: an err in the intersectAll output appears in BOTH inputs (consolidate carrier preservation for the left side; lookup-witness for the right). * intersectAll_errorDiffCarriers_of_mem: a .error-diff carrier in the output exists (with some diff) in BOTH inputs. The min combinator only yields .error when at least one side has .error, but the carrier must be present on both for intersectAll to emit anything. * bagIntersectAll_errCarriers_of_mem: composition with clampPositive. Forward direction (errors in both inputs propagate to output) holds for collection-err on left via existing intersectAll_preserves_error_diff_left, with side conditions. Full iff theorems for intersectAll are out of scope — would need to characterize min combinator results per-bucket. Proofs use a hF restate via defeq (.fst/.snd projection reduction) before cases on lookup; otherwise rw [hLookup] fails to find the lookup expression syntactically. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Lift error-scope extractors to TimedUnifiedStream: * TimedUnifiedStream.errCarriers / errorDiffCarriers * _nil / _append reductions matching UnifiedStream's Per-operator theorems: * advanceFrontier_errCarriers / advanceFrontier_errorDiffCarriers: exact equality. advanceFrontier only changes times; carriers and diffs untouched. * atTime_errCarriers_subset / atTime_errorDiffCarriers_subset: errs in atTime t slice came from input s (subset direction). Time-slice projection loses records at other times, so this cannot be an iff. * consolidateAtTime_errCarriers_subset / consolidateAtTime_errorDiffCarriers_subset: composition of atTime subset with consolidate iff. Restructured: moved consolidate_errCarriers_iff / consolidate_errorDiffCarriers_iff from Mz/SetOps.lean to Mz/UnifiedConsolidate.lean. Mz/TimedConsolidate.lean cites them but the import chain has SetOps downstream of TimedConsolidate. SetOps continues to use them via its UnifiedConsolidate import. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Document new error-scope coverage: * Clamp/clamp-distinct error-scope (clampPositive, clampToOne, distinct, bagExceptAll, intersectAll, bagIntersectAll): full iff for collection-err, reverse-only for row-err (clamp drops). * negate_filter commutativity. * Timed error-scope lift (errCarriers / errorDiffCarriers on TimedUnifiedStream; advanceFrontier exact; atTime / consolidateAtTime subset). * JoinPushdown.lean entry: filter_cross_pushdown_left, IsPureData hypothesis, cross_singleton reduction. * Note relocation of consolidate iff theorems to UnifiedConsolidate.lean (TimedConsolidate citation chain). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
DiffWithError.sumAll_error_inv: converse of absorption. A sum equal to .error witnesses at least one .error summand. Proof peels via add_eq_error_left_or_right (DiffSemiring inversion law) on each cons step; nil case rules out via .val 0 ≠ .error. Triple.lean reverse-direction theorems: * consolidateAll_error_inv: .error total → ∃ record in stream with .error diff. * consolidateAtTimeFlat_error_inv: .error total at time t → ∃ record at time t with .error diff. Both are direct corollaries — extract the map preimage and filter conditions from sumAll_error_inv's witness. The consolidateAtTimeFlat version decodes the decide-wrapped time predicate via of_decide_eq_true. Closes the round-trip on flat consolidations: forward absorption + reverse inversion makes consolidateAll = .error iff some record has .error diff (and similarly per-time). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three new theorems in Mz/Triple.lean: * consolidateAll_eq_error_iff: forward + reverse combined. consolidateAll s = .error ↔ ∃ r ∈ s, r.2.2 = .error. * consolidateAtTimeFlat_eq_error_iff: same shape, restricted to time-t slice. * consolidateAll_eq_error_iff_errorDiffCarriers: bridges the flat consolidation to the timed error-scope extractor. consolidateAll s = .error ↔ errorDiffCarriers s ≠ []. The bridge connects two views of the same observation: the diff-semiring total (single .error or .val value) and the extractor list (carrier-level collection-err set). They agree exactly on whether the stream has any .error diff anywhere. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
negate commutes with project unconditionally: negate (project es us) = project es (negate us) Mirror of negate_filter. project's row arm produces rowProjectRecords es d r which preserves the input diff d on every emitted record; negation flips d uniformly, sliding through. Helper negate_rowProjectRecords: negation slides through the row-project helper. Uses List.map_map for the err-branch case. rowProjectRecords promoted from private to public so the cross-file commute theorem can cite it directly. Enables optimizer rewrites that commute negation with projection (EXCEPT ALL through projection, retraction propagation). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Symmetric counterpart to cross_negate_left: cross l (negate r) = negate (cross l r) Uses DiffWithError.mul_neg_int (a * -b = -(a * b)) on the diff arithmetic; combineCarrier carrier is unchanged by negation. Proof structure mirrors cross_negate_left: induction on l with hL/hR reduction lemmas to expose flatMap output, then map_congr on the per-record body. Together with cross_negate_left, gives the bilinear law for cross: negate slides through from either side. Useful for optimizer rewrites where retractions on either input propagate through cross. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Single index of every equational / inclusion law on UnifiedStream and TimedUnifiedStream. Grouped by algebraic shape: * Append / unionAll distribution * Commutativity (negate slides through) * Pushdown (filter_cross_pushdown_left) * Bilinearity (cross-negate) * Associativity (cross, unionAll, combineCarrier) * Involution / idempotence (negate_negate, clamp/escalate/advance idem) * Length / cardinality bounds * Trivial cases (nil / singleton reductions) * Cons / step reductions (cross_cons, consolidateInto match/skip) * Error-scope: row-err (errCarriers) * Error-scope: collection-err (errorDiffCarriers) * Error-diff record absorption (forward) and inversion (reverse) * No-error preservation * Multiplicity / shape constraints * NoDup carrier-uniqueness * Membership bridges * Round-trip / iff * DiffWithError underlying laws * Column-reference analyzers Each row links theorem name to source file. Optimizer rewrites should index here first; ~190 theorems total. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add 'Materialize optimizer passes → Lean coverage' section in transforms.md. Inventories all 66 passes in src/transform/ and classifies each as: * Modeled — equivalent theorem shipped (6 passes). * Modelable — current UnifiedStream / DiffWithError infra is sufficient; just write the theorem (11 passes incl. filter/map fusion, right-side pushdown, threshold elision, redundant_join, semijoin_idempotence, demand, canonicalize_mfp, equivalence_propagation use sites). * Infra gap — needs new operator or analysis (10 passes: Reduce family, TopK, FlatMap, IndexedFilter, monotonicity, column lattice). * Out of scope — physical planning, syntactic canonicalization, user-facing notices, type checking (~14 passes). Closes with priority recommendations: filter_cross_pushdown_right, filter/map fusion, threshold_elision as easy next ships. Reduce operator is the largest single infra gap (unlocks 4+ passes). Catalog derived via Explore-agent enumeration of src/transform/. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Mirror of filter_cross_pushdown_left. Predicate references only right-input columns (pred = pred'.colShift M, every left row of width M), left input is pure data. Bridges via eval_append_right_shift; symmetric to the left version's colReferencesBoundedBy + width-monotone setup. Single per-record helper filter_map_pure_data_right covers the .row+.val case; .error diff / .err carrier rows on the left are ruled out by IsPureData l. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Move predicate_pushdown.rs entry from "left-only pending" to bilateral. Drop redundant Modelable row. Rotate the priority list — top-of-list slot now goes to filter ∘ filter fusion. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`filter p (filter q us) = filter (.and q p) us` under per-row err-freedom: neither predicate may evaluate to .err on any data row of the input. Side condition is sharp — without it, the ordering between filter's err-promotion and evalAnd's `.bool false` absorption clause disagrees, e.g. on `(eval r q, eval r p) = (.err e, .bool false)`. Side condition lives in new `UnifiedStream.predNoRowErr`. Carrier- err records and `.error`-diff records pass through both pipelines unchanged; the hypothesis is only needed at `.row` records. Mirrors fusion/filter.rs in the Rust optimizer. New module Mz/FilterFusion.lean. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Move fusion/filter.rs from Modelable to Modeled, cite filter_filter_fuse in Mz/FilterFusion.lean. Rotate priority list: project fusion now top of queue. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
clampPositive_id_of_positive: clampPositive is identity on streams where every record's diff is .error or .val n with n > 0. Models threshold_elision.rs — drop the post-pass when input is already sign-normalized. transforms.md: move to Modeled, rotate priority list. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`project es' ∘ project es = project (es'.map (·.subst es))` when `es` is safe on every data row of the input. Side condition is sharp: if `es` errors on a row, step 1 emits one err record per erroring scalar of `es`; the fused form instead emits one err record per `e' ∈ es'` whose substituted form errors. Those err sets only agree in the safe-input case. Row-level fusion lemma `rowProjectRecords_substList` is unconditional; the stream-level theorem `project_project_fuse` lifts it under `projsAllSafe`. Bridges via `eval_subst` from `Mz/Pushdown.lean`. Mirrors fusion/map.rs in the Rust optimizer. New module Mz/ProjectFusion.lean. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Move fusion/map.rs from Modelable to Modeled. Rotate priority list: semijoin_idempotence now top. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`UnifiedStream.filter_replaceAtRow_of_unused`: filter and `replaceAtRow n v` commute when the predicate doesn't reference column `n`. Lifts `eval_replaceAt_of_unused` from `Mz/ColRefs.lean` to the stream level. Models the row-side of demand.rs: a column that nothing downstream reads can be overwritten arbitrarily without changing the operator's output. New module Mz/Demand.lean. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`project_replaceAtRow_eq_of_unused`: when every expression in `es` has column `n` unused and the input is pure data, replacing column `n` of every input row leaves the project output equal. Asymmetry vs filter: filter preserves the row content of surviving records, so demand admits replacement on both input and output sides; project rewrites row content via `es.map (eval r)`, so column `n` of the output is unrelated to column `n` of the input, and the simpler invariance form requires ruling out `.err`/ `.error` passthrough — hence the `IsPureData` hypothesis. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Move demand.rs from Modelable to Modeled. Cite both filter_replaceAtRow_of_unused (full input) and project_replaceAtRow_eq_of_unused (under IsPureData). Rotate priority list; canonicalize_mfp now reachable on top of three fusion theorems. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`UnifiedStream.filter_idem`: filter pred (filter pred us) = filter pred us. Holds without err-freedom — when both filters share a predicate, the err-promotion / evalAnd ordering mismatch that forces predNoRowErr in filter_filter_fuse cannot arise. Special case of filter_filter_fuse + evalAnd_idem, but proved directly to avoid the unnecessary hypothesis. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`UnifiedStream.filter_comm`: filter p (filter q us) = filter q (filter p us) when neither predicate errors on the input's data rows. Reduces to `filter_filter_fuse` applied both ways, then equates `.and q p` and `.and p q` via `evalAnd_comm_of_no_err`. New helper `filter_eval_eq`: two filters with eval-equivalent predicates on every data row produce equal outputs. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Cite filter_idem (unconditional) and filter_comm (under err-freedom) alongside filter_filter_fuse. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`UnifiedStream.filter_project_pushdown`: filter p ∘ project es = project es ∘ filter (p.subst es), under projsAllSafe es us. Lifts BagStream.project_filter_pushdown_data (data-side only) to the unified stream — errs flow through both pipelines symmetrically under the safety hypothesis, so no data/error asymmetry remains. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Note filter_project_pushdown in the Modelable row for projection-lifting passes. Still missing: project_cross_pushdown (harder — depends on column-split semantics). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`clampToOne_id_of_one`: clampToOne is identity when every record's diff is already .val 1 or .error. Companion to clampPositive_id_of_positive — same threshold-elision pattern, but for the set-semantics post-pass instead of the bag-semantics one. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Member
Author
Foundational gapsRanked by what's currently blocking further coverage. Tier 1: blocks most remaining modelable passes
Tier 2: specific pass clusters
Tier 3: correctness reach
Recommendation orderTier 1 stream-equivalence + Reduce + separate Map unlocks the most. Schema enables a different class of analyses cleanly. Bridge to |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Lean 4 mechanization of Materialize's error-handling design at
doc/developer/semantics/, modeling the unified-stream proposal where:UnifiedRow.err);Datum.err;DiffWithError.error).Skeleton proves the algebraic laws an optimizer pass cites. 32 lean build jobs, all green. No
sorry.Coverage of
src/transform/: 13 of ~66 optimizer passes have correspondents inMz/*.lean(filter / project / negate / union fusion, bilateral predicate pushdown, threshold elision, demand, filter idem / comm). Seedoc/developer/semantics/transforms.mdfor the full mapping plus modelable / infra-gap / out-of-scope buckets.Build:
ci/test/lean-semantics.sh(docker, lean v4.29.1, lake).