diff --git a/ci/test/lean-semantics.sh b/ci/test/lean-semantics.sh new file mode 100755 index 0000000000000..a52605a781d63 --- /dev/null +++ b/ci/test/lean-semantics.sh @@ -0,0 +1,41 @@ +#!/usr/bin/env bash + +# Copyright Materialize, Inc. and contributors. All rights reserved. +# +# Use of this software is governed by the Business Source License +# included in the LICENSE file at the root of this repository. +# +# As of the Change Date specified in that file, in accordance with +# the Business Source License, use of this software will be governed +# by the Apache License, Version 2.0. +# +# lean-semantics.sh — build the Lean 4 semantics model in +# `doc/developer/semantics`. The Lean toolchain version is read from +# `lean-toolchain` and forwarded to the Dockerfile in the same +# directory, so the elan toolchain pin used by local developers and the +# CI image stay in lockstep. +# +# The Docker image is built locally on the agent and reused across CI +# runs by Docker's layer cache. There is no registry push; the image is +# cheap to rebuild from cold (≈ apt + elan + one Lean toolchain). + +set -euo pipefail + +cd "$(dirname "$0")/../.." + +semantics_dir="doc/developer/semantics" +lean_toolchain="$(tr -d '[:space:]' < "$semantics_dir/lean-toolchain")" +image_tag="mz-lean-semantics:latest" + +docker build \ + --build-arg "LEAN_TOOLCHAIN=$lean_toolchain" \ + --tag "$image_tag" \ + -f "$semantics_dir/Dockerfile" \ + "$semantics_dir" + +docker run --rm \ + --user "$(id -u):$(id -g)" \ + -v "$PWD/$semantics_dir:/workspace" \ + -w /workspace \ + "$image_tag" \ + lake build diff --git a/ci/test/pipeline.template.yml b/ci/test/pipeline.template.yml index 5a24a620d9940..f2de2388e4635 100644 --- a/ci/test/pipeline.template.yml +++ b/ci/test/pipeline.template.yml @@ -193,6 +193,19 @@ steps: coverage: skip sanitizer: skip + - id: lean-semantics + label: ":lean: Lean semantics" + command: ci/test/lean-semantics.sh + inputs: + - doc/developer/semantics + - ci/test/lean-semantics.sh + depends_on: [] + timeout_in_minutes: 15 + agents: + queue: hetzner-x86-64-4cpu-8gb + coverage: skip + sanitizer: skip + - id: lint-macos label: ":rust: macOS Clippy" # Running on a manually installed macOS agent, so make sure we don't go out of disk diff --git a/doc/developer/design/20260517_error_handling_semantics.md b/doc/developer/design/20260517_error_handling_semantics.md new file mode 100644 index 0000000000000..84ae266309ff2 --- /dev/null +++ b/doc/developer/design/20260517_error_handling_semantics.md @@ -0,0 +1,345 @@ +# Error handling semantics + +* Associated: TBD (no open issue yet; this doc establishes the model) + +## The problem + +Materialize today has two error pathways and a gap between them. +`DataflowError` propagates row-level failures through a parallel error collection, allowing dataflows to surface failed records without halting computation. +`EvalError` describes scalar failures but, when raised, escalates the whole row to `DataflowError::EvalError` and removes the row from the output collection. +There is no first-class representation of a cell-level error inside a `Row`, and there is no representation of a collection-level error attached to a logical operator output. + +The absence of cell-level errors forces ingestion and casting paths to either reject records, coerce values to types they cannot represent, or route columns through `text` and defer parsing. +Concrete cases this hurts include MySQL/TiDB `0000-00-00` zero-dates that cannot be represented as `Datum::Date`, JSON casts that fail mid-row, decimal overflow inside a `SELECT` list, and any user-defined coercion that may fail on a subset of inputs. +A user who wants the rest of the row preserved must today either filter the data upstream or model the column as `text` and reparse it at query time. +This is the same friction that motivated `try_cast`, but applied at the storage layer rather than at the cast site. + +Globally scoped errors — failures whose blast radius is the whole collection rather than a single row — also lack a uniform representation. +A `WHERE` predicate that errors on a single row is a row-level error today, but the same predicate evaluated as part of a join condition or aggregation can produce semantics that escape any single row. +Differential dataflow's natural locus for "this collection is invalid at time `t`" is the `diff` field, which Materialize currently does not use this way. +A spec for global errors is needed so that future work has a consistent target rather than an ad-hoc encoding per operator. + +## Success criteria + +A solution is successful when the following hold. + +* Cell-level failures can be represented inside a `Row` without forcing the row out of the output collection. +* Row-level failures continue to be represented by the existing error collection without behavior change for in-place dataflows. +* Collection-level failures (global errors) have a defined semantics and a defined encoding, even if the encoding is not yet implemented. +* SQL evaluation rules for `NULL`, errors, and short-circuiting are written down in one place and match PostgreSQL where reasonable, with deviations called out explicitly. +* Existing data and existing dataflows continue to read and run after the new variant is added. + +## Out of scope + +The following are intentionally not addressed here. + +* The wire-format migration plan for adding a new `Datum` tag. +This is implementation work whose shape depends on which encoding option is chosen. +* The exact set of operators that should be made error-aware in the first iteration. +That is a planning concern, not a semantic one. +* User-facing SQL syntax for introspecting or filtering on errors (`is_error`, `error_message`, `try_*`). +The semantics defined here support such syntax, but choosing the surface is a separate design. +* Cancellation of in-flight queries due to global errors. +A dataflow exposing a global error is a steady-state concept; cancellation is orthogonal. + +## Solution proposal + +The proposal introduces three error scopes and assigns each a representation. + +### Error scopes + +Errors are classified by the smallest unit of output they invalidate. + +* **Cell-scoped**: the error invalidates a single `Datum` within a single `Row`. +The rest of the row is still well-defined. +Example: cast overflow on a single column inside a `SELECT` list. +* **Row-scoped**: the error invalidates a single row. +No `Datum` in the row is well-defined, but the rest of the collection is. +Example: a decoding error on a Kafka record, or a key-conflict in an upsert envelope. +* **Global-scoped**: the error invalidates the entire output collection at some time `t`. +No row at that time is well-defined. +Example: a `WHERE clause` whose evaluation depends on collection-wide state that has become invalid, or a sink whose downstream contract has been violated. + +Classification is a property of the operator producing the error, not of the underlying `EvalError`. +The same arithmetic overflow is cell-scoped when raised inside a `SELECT` projection and row-scoped when raised inside a `WHERE` predicate. +Operators are responsible for choosing the smallest scope that faithfully represents their semantics. + +### Cell-scoped errors: `Datum::Error` + +A new `Datum::Error(Box)` variant is added. +The variant participates in all `Row` encoding paths and is propagated by expressions according to the rules in the SQL semantics section. +Operators that produce a row may produce `Datum::Error` in any position where a value of any type is expected. +Operators that consume a row must either propagate the error, trap it via an explicit operator (`try_*`, `coalesce`-style), or escalate it to a row-scoped error. + +The type system treats `Datum::Error` as inhabiting every `ScalarType`. +This mirrors the way `NULL` inhabits every nullable type. +The variant carries an `EvalError`, not a string, so that error introspection functions can be added later without a format break. + +### Stream shape: two-diff records + +The unit of denotation is a stream of records of shape + +``` +(row : List Datum, diff : Int, err_diff : Int) +``` + +For each `(row, time)` bucket, `diff` is the multiplicity of `row` as a valid output and `err_diff` is the multiplicity of `row` as an erred output. +Both components are ordinary `Int` diffs that participate in differential dataflow's standard consolidation arithmetic. +Both retract. + +A row with `(diff, err_diff) = (1, 0)` is a normal valid row. +A row with `(0, 1)` is a single erred row that exists in the error collection. +A row with `(1, 1)` exists in both collections (rare but representable). +Retractions are the natural `(−1, 0)` or `(0, −1)`. + +The single-stream two-diff form is denotationally equivalent to the (`data`, `errors`) two-collection form used elsewhere in Materialize today. +The two views are interchangeable via the obvious bijection: `(r, d, e) ↦ (r appears `d` times in `data`, `r` appears `e` times in `errors`)`. +Choosing the single-stream form here means operators have one signature `Stream → Stream` instead of two, and proofs reason about one carrier rather than a pair. + +### Row-scoped errors: `err_diff` and `DataflowError` + +`DataflowError` continues to carry the structured payload of every erred row. +The row content lives in the data field of the stream record; the `err_diff` is its multiplicity in the error side. +`DataflowError::EvalError(EvalError)` is the structured payload for predicate-error / join-predicate-error / aggregate-error escalations; other `DataflowError` variants (source-decoder errors, key-conflict errors, etc.) carry their own structured payloads alongside the row. + +An operator escalates a row to row scope by moving its multiplicity from `diff` to `err_diff`. +Concrete operator rules are listed in *SQL error semantics* below. + +### Cell-scoped errors: `Datum::Error` inside the row + +`Datum::Error(EvalError)` lives inside the row's cells. +A row `[Datum::Int 5, Datum::Error EvalError::DivByZero, Datum::Null]` is a perfectly valid row of width three whose middle column happens to be an error. +The row participates in the stream as a normal `(diff, err_diff) = (1, 0)` record. +Downstream operators that consume the column propagate the error per the strict-function rules in *SQL error semantics*. + +An alternative form extends the diff with a per-`EvalError` multiplicity component (`Diff = Int × (EvalError → Int)`) so that the err side tracks *which* errors caused row escalation at the diff level. +See *Per-error-payload diff component* under Alternatives; the two-diff baseline and the per-payload form are both viable and the choice is not yet settled. + +### Global-scoped errors: absorbing diff marker (specification only) + +A global error at time `t` is encoded as a distinguished record whose `diff` field carries an absorbing element. +The diff field for global-error records carries a value from the extended semiring + +``` +DiffWithGlobal = val(Int) | global +``` + +with `global` absorbing both addition and multiplication: `global + d = global`, `d + global = global`, `global * d = global`, `d * global = global`. +Any sum involving `global` is itself `global`, which is exactly the propagation rule a downstream operator needs. +The `global` marker is terminal: it cannot be retracted, because the claim "this collection is invalid at `t`" is one-way. + +The intent is that any downstream operator observing a `global` record at time `t` treats the entire input collection at `t` as invalid, propagating the global error to its own output. +The natural locus is the diff field, because the data field is per-row and the time field is per-update, and an absorbing monoid extension of the diff semiring captures exactly the propagation rule required. + +The data side and the `DataflowError` side both carry `Int` diffs in the ordinary case; only the global-error pathway uses `DiffWithGlobal`. +Implementation is out of scope. +The spec exists so that future operator work targets this absorbing-marker encoding rather than inventing alternates. + +### SQL error semantics + +The rules below define how `NULL` and `Datum::Error` interact in expression evaluation. +The intent is to match PostgreSQL behavior where PostgreSQL has behavior, and to extend it where PostgreSQL has none because PostgreSQL has no first-class cell error. + +**Scalar function evaluation.** +A strict function applied to any `Datum::Error` argument returns `Datum::Error`. +A strict function applied to `NULL` returns `NULL`, as today. +If a strict function receives both `NULL` and `Datum::Error` arguments, it returns `Datum::Error`. +This rule matches the principle that errors are stronger than `NULL`: `NULL` denotes "unknown value", error denotes "the value cannot exist". + +**Non-strict functions.** +`coalesce(a, b)` returns the first non-`NULL`, non-error argument, evaluating left to right. +If all arguments are `NULL` or error, the result is `NULL` if any argument was `NULL` and all errors were unreached, otherwise the first error. +This generalizes PostgreSQL `coalesce` so that a fallback can rescue an error in the same way it rescues a `NULL`. +Short-circuit boolean operators evaluate per the truth table below. + +**Boolean three-valued logic, extended.** +`AND` and `OR` are extended from PostgreSQL's three-valued logic to four values: `TRUE`, `FALSE`, `NULL`, `ERROR`. +The extension is conservative: any cell that PostgreSQL would have produced as `NULL` is still `NULL`, and `ERROR` participates only when an operand is an actual error. + +| `AND` | TRUE | FALSE | NULL | ERROR | +|---------|-------|-------|-------|-------| +| TRUE | TRUE | FALSE | NULL | ERROR | +| FALSE | FALSE | FALSE | FALSE | FALSE | +| NULL | NULL | FALSE | NULL | NULL | +| ERROR | ERROR | FALSE | NULL | ERROR | + +| `OR` | TRUE | FALSE | NULL | ERROR | +|---------|------|-------|-------|-------| +| TRUE | TRUE | TRUE | TRUE | TRUE | +| FALSE | TRUE | FALSE | NULL | ERROR | +| NULL | TRUE | NULL | NULL | NULL | +| ERROR | TRUE | ERROR | NULL | ERROR | + +`FALSE AND ERROR` is `FALSE`, and `TRUE OR ERROR` is `TRUE`, because the result is determined without inspecting the erroring operand. +`NULL AND ERROR` and `NULL OR ERROR` collapse to `NULL`, preserving PostgreSQL's bias toward `NULL` when ignorance subsumes the question. + +**Predicates.** +A `WHERE` clause acts on a record `(r, diff, err_diff)` according to the value of `eval r pred`: + +* `TRUE` → `(r, diff, err_diff)` unchanged (the row passes through with both multiplicities preserved). +* `FALSE` → `(r, 0, err_diff)` — the data multiplicity drops to zero; the err side is untouched. +* `NULL` → `(r, 0, err_diff)` — same as `FALSE`. +* `ERROR e` → `(r, 0, err_diff + diff)` — the data multiplicity migrates to the err side, added to whatever err multiplicity was already there. + The structured `EvalError` payload `e` is carried via `DataflowError::EvalError(e)` alongside the err-side multiplicity. + +Retractions are the natural negation: a row that was escalated to err side with multiplicity `+1` and is later retracted produces an `err_diff = -1`, cancelling in the consolidated view. +The row content is preserved across the escalation; downstream operators that consume the row see the same `r` whether it lives in the data side or the err side. + +**Comparison.** +`=`, `<`, `>`, etc., applied to `Datum::Error` return `Datum::Error`. +`IS DISTINCT FROM` treats `Datum::Error` as distinct from any other value including another `Datum::Error` carrying the same inner error, on the grounds that the equality of two errors is itself ill-defined. +`IS NULL` returns `FALSE` on `Datum::Error`, mirroring the rule that error and `NULL` are distinct. +A future `IS ERROR` predicate would return `TRUE` on `Datum::Error` and `FALSE` otherwise. + +**Aggregates.** +`COUNT(*)` counts rows regardless of cell contents; `COUNT(expr)` counts rows where `expr` is neither `NULL` nor error. +`SUM`, `AVG`, `MIN`, `MAX`, and similar reductions return `Datum::Error` if any input cell is `Datum::Error`, with the inner `EvalError` chosen by an operator-defined rule (typically the first error in scan order; the rule must be deterministic given a fixed input). +This matches the principle that errors are stronger than `NULL` and the principle that aggregates should not silently hide failures. +An explicit opt-out is provided by future `try_sum`-style aggregates. + +**Grouping.** +`GROUP BY` treats `Datum::Error` as a distinct group key, with the same equality semantics as `IS DISTINCT FROM`: every error is its own group. +This avoids accidentally collapsing unrelated failures into a single aggregate output. + +**Joins.** +Cross product on two-diff records combines multiplicities multiplicatively, applying the standard differential-dataflow rule on each component: + +``` +(rL, dL, eL) × (rR, dR, eR) ⟹ (rL ++ rR, dL · dR, dL · eR + eL · dR + eL · eR) +``` + +Valid×valid produces valid (`dL · dR`). +Valid×err and err×valid produce err (each multiplied by the other side's data count). +Err×err also produces err (an err record crossed with an err record is still err). + +A join predicate evaluating to `ERROR` on a row `(r, d, e)` of the cross product follows the `WHERE` rule: the data multiplicity migrates to the err side, with the structured `EvalError` payload carried via `DataflowError::EvalError`. + +Join keys containing `Datum::Error` do not match any other key, including identical `Datum::Error` values, mirroring the grouping rule. + +**Casts and `try_cast`.** +A cast that would today raise `EvalError` now also has the option of producing `Datum::Error` when invoked from a context that has opted in to cell-scoped failures. +`try_cast` continues to return `NULL` on failure for backward compatibility. +A new variant such as `try_cast_error` could return `Datum::Error`; choosing the surface is out of scope. + +### Operator obligations + +Each operator falls into one of three categories. + +* **Error-transparent**: passes `Datum::Error` through unchanged in the cells where it appears. +Most projection-style operators are transparent. +* **Error-aware**: inspects `Datum::Error` and produces a defined result. +Examples: `coalesce`, `IS NULL`, future `IS ERROR`, `try_*`. +* **Error-escalating**: converts a cell-scoped error to a row-scoped error. +Examples: `WHERE`, join predicates, sink output (a sink cannot emit a row containing `Datum::Error` to a downstream system, so it must escalate). + +Operators document which category they fall into. +Default for a new operator is transparent unless it has a reason to be aware or escalating. + +### Worked example: TiDB zero-date + +MySQL and TiDB allow `0000-00-00` as a fallback when permissive `sql_mode` rejects an invalid date. +The value is not equivalent to `NULL`: a `NOT NULL` column can contain `0000-00-00` alongside `NULL` columns elsewhere. +Materialize's `Date` type cannot represent `0000-00-00` (no year 0, no month 0, no day 0). + +Under the proposed model the MySQL source decodes `Value::Date(0, 0, 0, ...)` into `Datum::Error(EvalError::InvalidDate)` for `SqlScalarType::Date` columns. +The row is emitted intact; downstream queries that touch only other columns succeed. +A query that projects the date column sees `Datum::Error`, which propagates per the rules above. +A user who wants to coalesce can write `coalesce(d, DATE '1970-01-01')` if they have opted into error-aware coalesce, preserving the distinction between zero-date and `NULL` while still producing a usable timestamp downstream. +The TEXT COLUMN escape hatch remains available but is no longer the only correct ingestion path. + +## Minimal viable prototype + +A prototype consists of three steps, none of which require the full migration to land. + +* Add `Datum::Error(Box)` behind a feature flag, wired through `Row` packing and `RowArena` allocation, gated so that existing rows cannot contain the variant. +* Implement the strict-function propagation rule and the extended boolean truth tables in `MirScalarExpr` evaluation, with unit tests covering each cell of each table. +* Wire the MySQL source decoder to emit `Datum::Error` on `Value::Date(0, 0, 0, ...)` for `SqlScalarType::Date` columns, and verify end-to-end that a `SELECT` over an unaffected column returns the row while a `SELECT` over the date column returns the error. + +The prototype intentionally omits global errors, sinks, and aggregates; those land in subsequent PRs with their own tests. + +## Alternatives + +**Status quo plus TEXT COLUMN guidance.** +Document that columns with permissive upstream `sql_mode` must be ingested as `text`. +Cheap, but pushes parsing to query time forever and does not generalize to other cell-failure sources (overflow, JSON cast, decimal precision). + +**Datum-level `NULL` overload.** +Coerce zero-dates to `NULL` at ingestion. +Loses the distinction between user-intended `NULL` and ingestion-rejected value. +Violates the spec rule that error is stronger than `NULL`. +Rejected on correctness grounds. + +**String error wrapper instead of `EvalError`.** +Store `Datum::Error(Box)` rather than `Datum::Error(Box)`. +Simpler to encode but loses structured error information; introspection functions would parse a string. +Rejected on extensibility grounds. + +**Error rows in the data collection rather than a separate variant.** +Tag the row itself with a per-column error bitmask, leaving `Row` as today. +Saves a `Datum` variant but introduces an out-of-band channel that operators must thread through every transformation. +Rejected on uniformity grounds; the `Datum` variant is the same place every existing operator already inspects. + +**Global errors via a sidecar collection rather than the `diff` field.** +Carry global errors in a separate timely stream. +Works, but requires every operator to be aware of two error inputs. +The `diff`-field encoding leverages differential dataflow's existing fan-in and is the natural extension of the semiring. + +**Row-scoped errors via carrier replacement rather than the err-side diff.** +Encode a row-scoped error by replacing the row with an opaque error marker in the data field while keeping a plain `Int` diff. +This is the simplest extension but loses the row's content at the carrier flip, so any downstream operator that needed the original row data (for join, group-by on other columns, or counting) cannot recover it. +The two-diff `(diff, err_diff)` form keeps the row and tracks the err multiplicity in a parallel `Int` component, which preserves both pieces of information and stays retractable through ordinary diff arithmetic. + +**Row-scoped errors via an absorbing diff marker like global errors.** +Use the same absorbing-monoid extension as the global-scoped case. +Rejected because per-row evaluation errors must be retractable: a row that errs on `WHERE 1/(a+b) > 5` at time `t` and is retracted at time `t'` must net to zero in the consolidated view. +An absorbing marker cannot retract. +The two-diff encoding (`Int` data multiplicity + `Int` err multiplicity, with absorbing `global` layered on top) keeps the algebra of each scope faithful to its semantics. + +**Per-error-payload diff component (Diff = Int × ErrCount).** +An earlier iteration of this document proposed extending the diff with a finite map from `EvalError` payloads to multiplicities, so that *which* error caused row escalation would be tracked at the diff level alongside the data multiplicity. +This is an open alternative, not a rejection — the two-diff `(Int, Int)` form is the current working baseline, but the per-payload form has properties the baseline does not, and the choice is not yet settled. + +Properties of the per-payload form that the baseline does not have: + +* `which` error caused row escalation is observable at the diff level rather than only through the `DataflowError` companion payload. + A future SQL surface that wants to filter or aggregate by error kind without joining on `DataflowError` can read the err-count map directly. + +* Multiple errors arising at the same `(row, time)` bucket are distinguished. + Under the baseline, two distinct error events for the same row collapse to `err_diff = 2` and the per-event payload information is recoverable only via `DataflowError`. + Under the per-payload form, they live in separate keys of the `ErrCount` map. + +Properties of the baseline that the per-payload form does not have: + +* The err-side diff is an ordinary `Int`, so every existing diff-semiring lemma and runtime arrangement layout applies without modification. + +* Multiplication has the simple rule `(a, b) * (a', b') = (a·a', a·b' + b·a' + b·b')` per component, and `predicate_pushdown` over `Cross(L, R)` is sound under strict list equality. + +* No stream-equivalence quotient is needed. + Under the per-payload form, the multiplication rule `(a, m) * (b, n) = (a·b, a • n + b • m)` makes several optimizer rewrites change err-count distributions without changing data multiplicities; soundness for those rewrites requires the quotient. + +The Lean mechanization on this branch carried out the `Int × ErrCount` design and surfaced both the equivalence-relation requirement and the `predicate_pushdown` interaction concretely. +That work is preserved as a worked alternative. +Resolving which form to standardize on requires answering the open question about a user-facing error-kind surface (see *Open questions*). + +## Open questions + +* What is the exact set of `EvalError` payloads that operators may produce as `Datum::Error`? +Some `EvalError` variants (out-of-memory, environment errors) make no sense at cell scope. +* How does `Datum::Error` interact with persisted state and version skew? +A reader on an older binary that encounters `Datum::Error` must have a defined behavior; the default proposal is to surface the row as a row-scoped error in the read path. +* Should ordering operators have a defined sort position for `Datum::Error`? +PostgreSQL has no precedent; candidates are "errors sort last", "errors sort like `NULL`", and "errors are unordered and produce a sort-key error". +* What is the storage cost of widening `Row` encoding to include the new tag, and how does it compare to the current cost of routing failures through the error collection? +* For global errors, what is the precise specification of the absorbing element in the `diff` semiring, and how does it interact with consolidation and arrangement? +* The two-diff `(diff, err_diff)` form has the runtime carrying two `Int`s per record where today it carries one. +What is the storage / wire cost, and is it acceptable for collections in which errors are rare? +A sparse representation that omits records with `err_diff = 0` is the obvious optimization. +* For source-decoder errors where the row's columns cannot be fully produced, what row content goes into the data field? +Candidates: a width-zero placeholder row, a width-N row of all-`Datum::Error` cells, or a `DataflowError::DecodeError` payload that lives alongside the err multiplicity but does not require a row at all. +The choice affects whether the data-side carrier is always a `List Datum` or whether the stream needs a sum-type carrier after all. +* Should the err-side multiplicity be a single `Int` (the two-diff baseline) or a per-`EvalError` map `EvalError → Int` (the per-payload alternative)? +This is the question that resolves whether the `Int × ErrCount` alternative is adopted. +The answer turns on a downstream concern: is there a user-facing SQL surface that needs to distinguish error kinds at the row level without joining on `DataflowError`? +If yes, the per-payload form is the natural fit. +If no, the two-diff form is the simpler home. +Until that surface is decided, both forms remain on the table. diff --git a/doc/developer/semantics/.gitignore b/doc/developer/semantics/.gitignore new file mode 100644 index 0000000000000..b914de79dca12 --- /dev/null +++ b/doc/developer/semantics/.gitignore @@ -0,0 +1,2 @@ +# Lake build cache. +.lake/ diff --git a/doc/developer/semantics/Dockerfile b/doc/developer/semantics/Dockerfile new file mode 100644 index 0000000000000..a895b5128b5bc --- /dev/null +++ b/doc/developer/semantics/Dockerfile @@ -0,0 +1,44 @@ +# Copyright Materialize, Inc. and contributors. All rights reserved. +# +# Use of this software is governed by the Business Source License +# included in the LICENSE file at the root of this repository. +# +# As of the Change Date specified in that file, in accordance with +# the Business Source License, use of this software will be governed +# by the Apache License, Version 2.0. +# +# Minimal Lean 4 toolchain image for building the Materialize semantics +# model in this directory. The Lean version is supplied via build arg, +# which `ci/test/lean-semantics.sh` reads from `lean-toolchain`, so the +# elan toolchain pin used by local developers and the CI image stay in +# lockstep. +# +# The image is intentionally small. It installs elan, a single Lean +# toolchain, and the system packages elan needs to download. No Mathlib, +# no editor, no test runners. Adding those is a deliberate future +# decision, not a passive consequence of inheriting a heavier base. + +FROM ubuntu:26.04 + +ARG LEAN_TOOLCHAIN + +# Install elan system-wide so the toolchain is usable by any uid that +# the container may be launched with (CI runs with the agent's uid via +# `--user`). Writes go to `/workspace/.lake/`, which is bind-mounted. +ENV ELAN_HOME=/opt/elan +ENV PATH=$ELAN_HOME/bin:$PATH + +RUN apt-get update \ + && DEBIAN_FRONTEND=noninteractive apt-get install -y --no-install-recommends \ + ca-certificates \ + curl \ + git \ + && rm -rf /var/lib/apt/lists/* + +RUN curl --proto '=https' --tlsv1.2 -sSf \ + https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ + | sh -s -- --default-toolchain "$LEAN_TOOLCHAIN" -y --no-modify-path \ + && chmod -R a+rX "$ELAN_HOME" \ + && lean --version + +WORKDIR /workspace diff --git a/doc/developer/semantics/Mz.lean b/doc/developer/semantics/Mz.lean new file mode 100644 index 0000000000000..a0eb8fdfa08de --- /dev/null +++ b/doc/developer/semantics/Mz.lean @@ -0,0 +1,14 @@ +import Mz.Datum +import Mz.Expr +import Mz.Eval +import Mz.Boolean +import Mz.MightError +import Mz.Strict +import Mz.Coalesce +import Mz.Laws +import Mz.Variadic +import Mz.ExprVariadic +import Mz.Bag +import Mz.Pushdown +import Mz.ColRefs +import Mz.Stream diff --git a/doc/developer/semantics/Mz/Bag.lean b/doc/developer/semantics/Mz/Bag.lean new file mode 100644 index 0000000000000..c32aeddfddbc7 --- /dev/null +++ b/doc/developer/semantics/Mz/Bag.lean @@ -0,0 +1,88 @@ +import Mz.Eval + +/-! +# Bag semantics: filter and project + +A first sliver of relational semantics on top of the per-`Row` +evaluator. A `Relation` is modeled as a `List Row` — a bag of rows +in execution order. The skeleton supports two relational +operators: + +* `filterRel pred rel` keeps the rows whose predicate evaluates to + `.bool true`. Rows that evaluate to `.bool false`, `.null`, or + `.err` are dropped. A real implementation would route `err` rows + to a separate error collection; the skeleton silently drops them + so the laws can be stated without modelling the error stream yet. +* `project es rel` evaluates each expression in `es` against every + row and emits a list of resulting rows. The output schema width + is `es.length`. + +The two laws stated here — filter idempotence and filter +commutativity — are the simplest optimizer-relevant rewrites over +the bag. Both reduce to `List.filter_filter` plus a `Bool` +identity (`and_self`, `and_comm`); the proofs lean entirely on +existing core-library lemmas. More substantial rewrites (predicate +pushdown across projection, predicate combination, etc.) are +follow-ups that this file is intended to grow into. +-/ + +namespace Mz + +/-- A row is a positional list of bound values. Reuses `Env`. -/ +abbrev Row := Env + +/-- A relation is a list of rows. Bag (multiset) semantics; row +order does not matter for filter or project laws. -/ +abbrev Relation := List Row + +/-- Membership-style predicate evaluator used by `filterRel`. Rows +that evaluate to `.bool true` are kept; everything else (including +`.err`) is dropped. -/ +@[inline] def rowPredicate (pred : Expr) (row : Row) : Bool := + match eval row pred with + | .bool true => true + | _ => false + +/-- Filter a relation by a scalar predicate. -/ +def filterRel (pred : Expr) (rel : Relation) : Relation := + rel.filter (rowPredicate pred) + +/-- Project a relation through a list of scalar expressions. +Each output row has width `es.length`. -/ +def project (es : List Expr) (rel : Relation) : Relation := + rel.map (fun row => es.map (eval row)) + +/-! ## Filter laws -/ + +theorem filterRel_idem (pred : Expr) (rel : Relation) : + filterRel pred (filterRel pred rel) = filterRel pred rel := by + unfold filterRel + rw [List.filter_filter] + congr 1 + funext row + exact Bool.and_self _ + +theorem filterRel_comm (p q : Expr) (rel : Relation) : + filterRel p (filterRel q rel) = filterRel q (filterRel p rel) := by + unfold filterRel + rw [List.filter_filter, List.filter_filter] + congr 1 + funext row + exact Bool.and_comm _ _ + +/-! ## Project laws -/ + +theorem project_length (es : List Expr) (rel : Relation) : + (project es rel).length = rel.length := by + unfold project + exact List.length_map _ + +/-- The empty projection collapses every row to the empty row of +width zero, so the relation becomes a list of empty rows whose +length equals the input length. -/ +theorem project_nil (rel : Relation) : + project [] rel = rel.map (fun _ => []) := by + show rel.map (fun row => ([] : List Expr).map (eval row)) = rel.map (fun _ => []) + congr 1 + +end Mz diff --git a/doc/developer/semantics/Mz/Boolean.lean b/doc/developer/semantics/Mz/Boolean.lean new file mode 100644 index 0000000000000..94d22f629d6b4 --- /dev/null +++ b/doc/developer/semantics/Mz/Boolean.lean @@ -0,0 +1,94 @@ +import Mz.PrimEval + +/-! +# Boolean truth tables + +Cell-by-cell proofs that `evalAnd` and `evalOr` realize the truth +tables stated in +`doc/developer/design/20260517_error_handling_semantics.md`. + +Each cell is its own theorem. The redundancy is deliberate: if a +future semantic change touches one cell, exactly one theorem breaks, +making the change reviewable in isolation. + +All proofs reduce to `rfl` because `evalAnd` and `evalOr` are defined +by pattern matching and the cases are exhaustive constructor +applications. The `cases d <;> rfl` form is used where a single cell +quantifies over an arbitrary `Datum` (e.g. `false` absorbs everything). +-/ + +namespace Mz + +/-! ## AND -/ + +theorem and_false_left (d : Datum) : evalAnd (.bool false) d = .bool false := by + cases d <;> rfl + +theorem and_false_right (d : Datum) : evalAnd d (.bool false) = .bool false := by + cases d with + | bool b => cases b <;> rfl + | int _ => rfl + | null => rfl + | err _ => rfl + +theorem and_true_true : evalAnd (.bool true) (.bool true) = .bool true := rfl +theorem and_true_null : evalAnd (.bool true) .null = .null := rfl +theorem and_null_true : evalAnd .null (.bool true) = .null := rfl +theorem and_null_null : evalAnd .null .null = .null := rfl + +theorem and_true_err (e : EvalError) : + evalAnd (.bool true) (.err e) = .err e := rfl +theorem and_err_true (e : EvalError) : + evalAnd (.err e) (.bool true) = .err e := rfl +theorem and_null_err (e : EvalError) : + evalAnd .null (.err e) = .err e := rfl +theorem and_err_null (e : EvalError) : + evalAnd (.err e) .null = .err e := rfl +theorem and_err_err (e₁ e₂ : EvalError) : + evalAnd (.err e₁) (.err e₂) = .err e₁ := rfl + +/-! ## OR -/ + +theorem or_true_left (d : Datum) : evalOr (.bool true) d = .bool true := by + cases d <;> rfl + +theorem or_true_right (d : Datum) : evalOr d (.bool true) = .bool true := by + cases d with + | bool b => cases b <;> rfl + | int _ => rfl + | null => rfl + | err _ => rfl + +theorem or_false_false : evalOr (.bool false) (.bool false) = .bool false := rfl +theorem or_false_null : evalOr (.bool false) .null = .null := rfl +theorem or_null_false : evalOr .null (.bool false) = .null := rfl +theorem or_null_null : evalOr .null .null = .null := rfl + +theorem or_false_err (e : EvalError) : + evalOr (.bool false) (.err e) = .err e := rfl +theorem or_err_false (e : EvalError) : + evalOr (.err e) (.bool false) = .err e := rfl +theorem or_null_err (e : EvalError) : + evalOr .null (.err e) = .err e := rfl +theorem or_err_null (e : EvalError) : + evalOr (.err e) .null = .err e := rfl +theorem or_err_err (e₁ e₂ : EvalError) : + evalOr (.err e₁) (.err e₂) = .err e₁ := rfl + +/-! ## NOT -/ + +theorem not_true : evalNot (.bool true) = .bool false := rfl +theorem not_false : evalNot (.bool false) = .bool true := rfl +theorem not_null : evalNot .null = .null := rfl +theorem not_err (e : EvalError) : evalNot (.err e) = .err e := rfl + +/-- `Not` is involutive on the boolean fragment and a no-op on `null` +and `err`. The latter mirrors the strict propagation rule. -/ +theorem not_not (d : Datum) : evalNot (evalNot d) = d := by + cases d with + | bool b => cases b <;> rfl + | int _ => rfl + | null => rfl + | err _ => rfl + +end Mz diff --git a/doc/developer/semantics/Mz/Coalesce.lean b/doc/developer/semantics/Mz/Coalesce.lean new file mode 100644 index 0000000000000..e51acd97ac57d --- /dev/null +++ b/doc/developer/semantics/Mz/Coalesce.lean @@ -0,0 +1,89 @@ +import Mz.PrimEval + +/-! +# `coalesce` and the error-rescue law + +`coalesce(d₁, …, dₙ)` returns the first operand that is neither +`null` nor `err`, evaluating left to right. The proposed extension +over PostgreSQL is that `err` is rescuable in the same way `null` +is: a later non-error operand can substitute for an earlier one, +whether that earlier one was `null`, `err`, or any combination. + +The evaluator (`evalCoalesce`) and its state-machine helper live in +`Mz/PrimEval.lean`. This file collects the laws. + +When no concrete value is found, the result follows a `null`-beats- +`err` rule: + +* If any operand was `null`, return `null`. +* Otherwise, if any operand was `err`, return the first such `err`. +* Otherwise (the empty list), return `null`. + +The "`null` beats `err`" tiebreaker preserves PostgreSQL's familiar +`coalesce` behavior for the all-`null` case while extending it +cleanly. It is the dual of the strict-function rule documented in +`Mz/Strict.lean`: strict functions promote `err` above `null` in the +result of a per-cell computation; `coalesce` is non-strict and +demotes `err` below `null`. +-/ + +namespace Mz + +/-! ## Base cases -/ + +theorem coalesce_nil : evalCoalesce [] = .null := rfl + +theorem coalesce_singleton_bool (b : Bool) : + evalCoalesce [.bool b] = .bool b := rfl + +theorem coalesce_singleton_null : + evalCoalesce [.null] = .null := rfl + +theorem coalesce_singleton_err (e : EvalError) : + evalCoalesce [.err e] = .err e := rfl + +/-! ## Error-rescue laws + +The defining property of the proposed `coalesce`: a later non-error, +non-null operand rescues an earlier `err` exactly as it rescues an +earlier `null`. -/ + +theorem coalesce_err_rescue_bool (e : EvalError) (b : Bool) : + evalCoalesce [.err e, .bool b] = .bool b := rfl + +theorem coalesce_null_rescue_bool (b : Bool) : + evalCoalesce [.null, .bool b] = .bool b := rfl + +/-! ## `null` beats `err` -/ + +theorem coalesce_null_then_err (e : EvalError) : + evalCoalesce [.null, .err e] = .null := rfl + +theorem coalesce_err_then_null (e : EvalError) : + evalCoalesce [.err e, .null] = .null := rfl + +/-! ## First error wins among errors -/ + +theorem coalesce_first_err_wins (e₁ e₂ : EvalError) : + evalCoalesce [.err e₁, .err e₂] = .err e₁ := rfl + +/-! ## Three-operand examples + +These nail down the interaction between several `err`s, a `null`, +and a concrete value. They are intentionally stated as concrete +equations rather than universal laws so that a regression in +`Coalesce.go` breaks the offending equation in isolation. -/ + +theorem coalesce_err_err_bool (e₁ e₂ : EvalError) (b : Bool) : + evalCoalesce [.err e₁, .err e₂, .bool b] = .bool b := rfl + +theorem coalesce_err_err_null (e₁ e₂ : EvalError) : + evalCoalesce [.err e₁, .err e₂, .null] = .null := rfl + +theorem coalesce_err_null_err (e₁ e₂ : EvalError) : + evalCoalesce [.err e₁, .null, .err e₂] = .null := rfl + +theorem coalesce_null_err_bool (e : EvalError) (b : Bool) : + evalCoalesce [.null, .err e, .bool b] = .bool b := rfl + +end Mz diff --git a/doc/developer/semantics/Mz/ColRefs.lean b/doc/developer/semantics/Mz/ColRefs.lean new file mode 100644 index 0000000000000..f51fc5e009328 --- /dev/null +++ b/doc/developer/semantics/Mz/ColRefs.lean @@ -0,0 +1,690 @@ +import Mz.Eval + +/-! +# Column-reference analysis + +The static analyzer `Expr.colReferencesBoundedBy n` returns `true` +when every `col i` reference in the expression has `i < n`. Used by +the optimizer to decide whether a predicate over a wide schema +mentions only the prefix (or only the suffix) of the row — the +precondition for pushing the predicate to one side of a join. + +The headline theorem `eval_append_left_of_bounded` proves the +soundness side: when a predicate's column references are bounded by +`l.length`, evaluating it against the concatenated row `l ++ r` +agrees with evaluating against `l` alone. The right-side analogue +shifts column indices by `l.length`. + +Both directions feed the join-pushdown theorems: a filter over a +cross product whose predicate touches only one side commutes with +the cross. The skeleton states the agreement here; the +relational-pushdown variant follows in future iterations of +`Mz/Join.lean`. +-/ + +namespace Mz + +/-! ## Column-bound analyzer -/ + +mutual +/-- `Expr.colReferencesBoundedBy n e` returns `true` iff every +`col i` in `e` has `i < n`. -/ +def Expr.colReferencesBoundedBy (n : Nat) : Expr → Bool + | .lit _ => true + | .col i => decide (i < n) + | .not a => a.colReferencesBoundedBy n + | .ifThen c t e => + c.colReferencesBoundedBy n && + t.colReferencesBoundedBy n && + e.colReferencesBoundedBy n + | .andN args => Expr.argsColRefBoundedBy n args + | .orN args => Expr.argsColRefBoundedBy n args + | .coalesce args => Expr.argsColRefBoundedBy n args + | .plus a b => a.colReferencesBoundedBy n && b.colReferencesBoundedBy n + | .minus a b => a.colReferencesBoundedBy n && b.colReferencesBoundedBy n + | .times a b => a.colReferencesBoundedBy n && b.colReferencesBoundedBy n + | .divide a b => a.colReferencesBoundedBy n && b.colReferencesBoundedBy n + | .eq a b => a.colReferencesBoundedBy n && b.colReferencesBoundedBy n + | .lt a b => a.colReferencesBoundedBy n && b.colReferencesBoundedBy n + +/-- Companion fold over operand lists. `argsColRefBoundedBy n args` +returns `true` iff every operand passes the bound. -/ +def Expr.argsColRefBoundedBy (n : Nat) : List Expr → Bool + | [] => true + | e :: rest => e.colReferencesBoundedBy n && Expr.argsColRefBoundedBy n rest +end + +/-! ## Environment-append lemmas -/ + +/-- Reading a column index below `l.length` from `l ++ r` yields +the same value as reading from `l`. Trivial induction. -/ +theorem Env.get_append_left : + ∀ (l r : Env) (i : Nat), i < l.length → + Env.get (l ++ r) i = Env.get l i + | [], _, _, h => absurd h (Nat.not_lt_zero _) + | hd :: _, _, 0, _ => rfl + | _ :: tl, r, n + 1, h => by + show Env.get (tl ++ r) n = Env.get tl n + exact Env.get_append_left tl r n (Nat.lt_of_succ_lt_succ h) + +/-- Reading a column index `l.length + i` from `l ++ r` yields +the i-th value of `r`. The right-side analogue of +`Env.get_append_left`. -/ +theorem Env.get_append_right : + ∀ (l r : Env) (i : Nat), + Env.get (l ++ r) (l.length + i) = Env.get r i + | [], _, _ => by + show Env.get (([] : Env) ++ _) (0 + _) = _ + rw [List.nil_append, Nat.zero_add] + | hd :: tl, r, i => by + show Env.get ((hd :: tl) ++ r) (tl.length + 1 + i) = Env.get r i + show Env.get (hd :: (tl ++ r)) (tl.length + 1 + i) = Env.get r i + have h_rewrite : tl.length + 1 + i = (tl.length + i) + 1 := by omega + rw [h_rewrite] + show Env.get (tl ++ r) (tl.length + i) = Env.get r i + exact Env.get_append_right tl r i + +/-! ## Eval agreement under bound + +If a predicate's column references are all bounded by `l.length`, +evaluating against `l ++ r` agrees with evaluating against `l`. +Joint structural recursion on `Expr` and the operand list. -/ + +mutual +theorem eval_append_left_of_bounded : + ∀ (l r : Env) (e : Expr), + e.colReferencesBoundedBy l.length = true → + eval (l ++ r) e = eval l e + | _, _, .lit _, _ => by simp [eval] + | l, r, .col i, h => by + have h_lt : i < l.length := of_decide_eq_true h + simp only [eval] + exact Env.get_append_left l r i h_lt + | l, r, .not a, h => by + simp only [Expr.colReferencesBoundedBy] at h + simp only [eval] + rw [eval_append_left_of_bounded l r a h] + | l, r, .ifThen c t e, h => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h + simp only [eval] + rw [eval_append_left_of_bounded l r c h.1.1, + eval_append_left_of_bounded l r t h.1.2, + eval_append_left_of_bounded l r e h.2] + | l, r, .andN args, h => by + simp only [Expr.colReferencesBoundedBy] at h + simp only [eval] + rw [eval_append_left_of_bounded_argsMap l r args h] + | l, r, .orN args, h => by + simp only [Expr.colReferencesBoundedBy] at h + simp only [eval] + rw [eval_append_left_of_bounded_argsMap l r args h] + | l, r, .coalesce args, h => by + simp only [Expr.colReferencesBoundedBy] at h + simp only [eval] + rw [eval_append_left_of_bounded_argsMap l r args h] + | l, r, .plus a b, h => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h + simp only [eval] + rw [eval_append_left_of_bounded l r a h.1, + eval_append_left_of_bounded l r b h.2] + | l, r, .minus a b, h => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h + simp only [eval] + rw [eval_append_left_of_bounded l r a h.1, + eval_append_left_of_bounded l r b h.2] + | l, r, .times a b, h => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h + simp only [eval] + rw [eval_append_left_of_bounded l r a h.1, + eval_append_left_of_bounded l r b h.2] + | l, r, .divide a b, h => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h + simp only [eval] + rw [eval_append_left_of_bounded l r a h.1, + eval_append_left_of_bounded l r b h.2] + | l, r, .eq a b, h => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h + simp only [eval] + rw [eval_append_left_of_bounded l r a h.1, + eval_append_left_of_bounded l r b h.2] + | l, r, .lt a b, h => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h + simp only [eval] + rw [eval_append_left_of_bounded l r a h.1, + eval_append_left_of_bounded l r b h.2] + +/-- Operand-list agreement under bound. Mutually defined with the +`Expr` form so structural recursion accepts both. -/ +theorem eval_append_left_of_bounded_argsMap : + ∀ (l r : Env) (args : List Expr), + Expr.argsColRefBoundedBy l.length args = true → + args.map (eval (l ++ r)) = args.map (eval l) + | _, _, [], _ => rfl + | l, r, e :: rest, h => by + simp only [Expr.argsColRefBoundedBy, Bool.and_eq_true] at h + show eval (l ++ r) e :: rest.map (eval (l ++ r)) + = eval l e :: rest.map (eval l) + rw [eval_append_left_of_bounded l r e h.1, + eval_append_left_of_bounded_argsMap l r rest h.2] +end + +/-! ## Bound monotonicity + +A predicate whose column references are bounded by `n` is also +bounded by any `m ≥ n`. Used to lift a tight per-relation bound +(e.g. `pred is bounded by table-A-width`) to a coarser join-env +bound (`bounded by combined-env-width`). -/ + +mutual +theorem Expr.colReferencesBoundedBy_mono : + ∀ {n m : Nat} (e : Expr), + e.colReferencesBoundedBy n = true → n ≤ m → + e.colReferencesBoundedBy m = true + | _, _, .lit _, _, _ => rfl + | n, m, .col i, h, hLe => by + have h_lt : i < n := of_decide_eq_true h + show decide (i < m) = true + exact decide_eq_true (Nat.lt_of_lt_of_le h_lt hLe) + | _, _, .not a, h, hLe => Expr.colReferencesBoundedBy_mono a h hLe + | _, _, .ifThen c t e, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h ⊢ + exact ⟨⟨Expr.colReferencesBoundedBy_mono c h.1.1 hLe, + Expr.colReferencesBoundedBy_mono t h.1.2 hLe⟩, + Expr.colReferencesBoundedBy_mono e h.2 hLe⟩ + | _, _, .andN args, h, hLe => by + simp only [Expr.colReferencesBoundedBy] at h ⊢ + exact Expr.argsColRefBoundedBy_mono args h hLe + | _, _, .orN args, h, hLe => by + simp only [Expr.colReferencesBoundedBy] at h ⊢ + exact Expr.argsColRefBoundedBy_mono args h hLe + | _, _, .coalesce args, h, hLe => by + simp only [Expr.colReferencesBoundedBy] at h ⊢ + exact Expr.argsColRefBoundedBy_mono args h hLe + | _, _, .plus a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesBoundedBy_mono a h.1 hLe, + Expr.colReferencesBoundedBy_mono b h.2 hLe⟩ + | _, _, .minus a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesBoundedBy_mono a h.1 hLe, + Expr.colReferencesBoundedBy_mono b h.2 hLe⟩ + | _, _, .times a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesBoundedBy_mono a h.1 hLe, + Expr.colReferencesBoundedBy_mono b h.2 hLe⟩ + | _, _, .divide a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesBoundedBy_mono a h.1 hLe, + Expr.colReferencesBoundedBy_mono b h.2 hLe⟩ + | _, _, .eq a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesBoundedBy_mono a h.1 hLe, + Expr.colReferencesBoundedBy_mono b h.2 hLe⟩ + | _, _, .lt a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesBoundedBy_mono a h.1 hLe, + Expr.colReferencesBoundedBy_mono b h.2 hLe⟩ + +theorem Expr.argsColRefBoundedBy_mono : + ∀ {n m : Nat} (args : List Expr), + Expr.argsColRefBoundedBy n args = true → n ≤ m → + Expr.argsColRefBoundedBy m args = true + | _, _, [], _, _ => rfl + | _, _, e :: rest, h, hLe => by + simp only [Expr.argsColRefBoundedBy, Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesBoundedBy_mono e h.1 hLe, + Expr.argsColRefBoundedBy_mono rest h.2 hLe⟩ +end + +/-- Convenience: when the predicate's bound `n` is at most the +prefix length, `eval (l ++ r) e = eval l e`. Removes the need for +the predicate to know `l.length` exactly. -/ +theorem eval_append_left_of_bounded_at + (l r : Env) (n : Nat) (e : Expr) + (hP : e.colReferencesBoundedBy n = true) (hLe : n ≤ l.length) : + eval (l ++ r) e = eval l e := + eval_append_left_of_bounded l r e + (Expr.colReferencesBoundedBy_mono e hP hLe) + +/-! ## Column shifting + +`Expr.colShift k e` adds `k` to every `col i` reference in `e`, +leaving other constructors structurally intact. Used to align a +predicate originally written against a right-side schema with the +joined env `l ++ r`: in the combined env, the right side starts at +index `l.length`, so shifting the predicate by `l.length` makes +its references land in the right half. + +The headline `eval_append_right_shift` states agreement: evaluating +the shifted expression against `l ++ r` equals evaluating the +original against `r`. -/ + +mutual +def Expr.colShift (k : Nat) : Expr → Expr + | .lit d => .lit d + | .col i => .col (k + i) + | .not a => .not (a.colShift k) + | .ifThen c t e => .ifThen (c.colShift k) (t.colShift k) (e.colShift k) + | .andN args => .andN (Expr.argsColShift k args) + | .orN args => .orN (Expr.argsColShift k args) + | .coalesce args => .coalesce (Expr.argsColShift k args) + | .plus a b => .plus (a.colShift k) (b.colShift k) + | .minus a b => .minus (a.colShift k) (b.colShift k) + | .times a b => .times (a.colShift k) (b.colShift k) + | .divide a b => .divide (a.colShift k) (b.colShift k) + | .eq a b => .eq (a.colShift k) (b.colShift k) + | .lt a b => .lt (a.colShift k) (b.colShift k) + +def Expr.argsColShift (k : Nat) : List Expr → List Expr + | [] => [] + | e :: rest => e.colShift k :: Expr.argsColShift k rest +end + +/-! ## Eval agreement under right-side shift + +Evaluating the shifted expression against `l ++ r` agrees with +evaluating the original against `r`. The shift compensates for +the `l.length` offset in the combined env. -/ + +mutual +theorem eval_append_right_shift : + ∀ (l r : Env) (e : Expr), + eval (l ++ r) (e.colShift l.length) = eval r e + | _, _, .lit _ => by simp [eval, Expr.colShift] + | l, r, .col i => by + show eval (l ++ r) (.col (l.length + i)) = eval r (.col i) + simp only [eval] + exact Env.get_append_right l r i + | l, r, .not a => by + simp only [Expr.colShift, eval] + rw [eval_append_right_shift l r a] + | l, r, .ifThen c t e => by + simp only [Expr.colShift, eval] + rw [eval_append_right_shift l r c, eval_append_right_shift l r t, + eval_append_right_shift l r e] + | l, r, .andN args => by + simp only [Expr.colShift, eval] + rw [eval_append_right_shift_argsMap l r args] + | l, r, .orN args => by + simp only [Expr.colShift, eval] + rw [eval_append_right_shift_argsMap l r args] + | l, r, .coalesce args => by + simp only [Expr.colShift, eval] + rw [eval_append_right_shift_argsMap l r args] + | l, r, .plus a b => by + simp only [Expr.colShift, eval] + rw [eval_append_right_shift l r a, eval_append_right_shift l r b] + | l, r, .minus a b => by + simp only [Expr.colShift, eval] + rw [eval_append_right_shift l r a, eval_append_right_shift l r b] + | l, r, .times a b => by + simp only [Expr.colShift, eval] + rw [eval_append_right_shift l r a, eval_append_right_shift l r b] + | l, r, .divide a b => by + simp only [Expr.colShift, eval] + rw [eval_append_right_shift l r a, eval_append_right_shift l r b] + | l, r, .eq a b => by + simp only [Expr.colShift, eval] + rw [eval_append_right_shift l r a, eval_append_right_shift l r b] + | l, r, .lt a b => by + simp only [Expr.colShift, eval] + rw [eval_append_right_shift l r a, eval_append_right_shift l r b] + +theorem eval_append_right_shift_argsMap : + ∀ (l r : Env) (args : List Expr), + (Expr.argsColShift l.length args).map (eval (l ++ r)) + = args.map (eval r) + | _, _, [] => rfl + | l, r, e :: rest => by + show eval (l ++ r) (e.colShift l.length) + :: (Expr.argsColShift l.length rest).map (eval (l ++ r)) + = eval r e :: rest.map (eval r) + rw [eval_append_right_shift l r e, + eval_append_right_shift_argsMap l r rest] +end + +/-! ## Column-unused analyzer + +`Expr.colReferencesUnused n e` returns `true` when `e` never reads +column `n`. The eval-invariance theorem uses this to justify +column-pruning rewrites: a projection that drops an unused column +does not change downstream eval results. -/ + +mutual +def Expr.colReferencesUnused (n : Nat) : Expr → Bool + | .lit _ => true + | .col i => decide (i ≠ n) + | .not a => a.colReferencesUnused n + | .ifThen c t e => + c.colReferencesUnused n && + t.colReferencesUnused n && + e.colReferencesUnused n + | .andN args => Expr.argsColRefUnused n args + | .orN args => Expr.argsColRefUnused n args + | .coalesce args => Expr.argsColRefUnused n args + | .plus a b => a.colReferencesUnused n && b.colReferencesUnused n + | .minus a b => a.colReferencesUnused n && b.colReferencesUnused n + | .times a b => a.colReferencesUnused n && b.colReferencesUnused n + | .divide a b => a.colReferencesUnused n && b.colReferencesUnused n + | .eq a b => a.colReferencesUnused n && b.colReferencesUnused n + | .lt a b => a.colReferencesUnused n && b.colReferencesUnused n + +def Expr.argsColRefUnused (n : Nat) : List Expr → Bool + | [] => true + | e :: rest => e.colReferencesUnused n && Expr.argsColRefUnused n rest +end + +/-! ## Env replacement at position + +`Env.replaceAt env n v` swaps the value at index `n` for `v`, +leaving other positions intact. Out-of-bounds indices leave the +environment unchanged (consistent with `Env.get`'s null fallback). -/ + +def Env.replaceAt : Env → Nat → Datum → Env + | [], _, _ => [] + | _ :: tl, 0, v => v :: tl + | hd :: tl, n + 1, v => hd :: Env.replaceAt tl n v + +/-- Reading position `n` from `replaceAt env n v` yields `v` when +in bounds. -/ +theorem Env.get_replaceAt_eq : + ∀ (env : Env) (n : Nat) (v : Datum), n < env.length → + Env.get (Env.replaceAt env n v) n = v + | [], _, _, h => absurd h (Nat.not_lt_zero _) + | _ :: _, 0, _, _ => rfl + | _ :: tl, n + 1, v, h => by + show Env.get (Env.replaceAt tl n v) n = v + exact Env.get_replaceAt_eq tl n v (Nat.lt_of_succ_lt_succ h) + +/-- Reading any other position is unchanged. -/ +theorem Env.get_replaceAt_ne : + ∀ (env : Env) (n i : Nat) (v : Datum), i ≠ n → + Env.get (Env.replaceAt env n v) i = Env.get env i + | [], _, _, _, _ => rfl + | _ :: _, 0, 0, _, h => absurd rfl h + | hd :: _, 0, i + 1, _, _ => by + show Env.get (hd :: _) (i + 1) = Env.get (hd :: _) (i + 1) + rfl + | _ :: _, n + 1, 0, _, _ => rfl + | _ :: tl, n + 1, i + 1, v, h => by + show Env.get (Env.replaceAt tl n v) i = Env.get tl i + exact Env.get_replaceAt_ne tl n i v (fun hEq => h (by rw [hEq])) + +/-! ## Eval invariance under replacement + +If column `n` is unused in `e`, replacing the value at position `n` +does not change `eval`. Mutual structural recursion on `Expr`. -/ + +mutual +theorem eval_replaceAt_of_unused : + ∀ (env : Env) (n : Nat) (v : Datum) (e : Expr), + e.colReferencesUnused n = true → + eval (Env.replaceAt env n v) e = eval env e + | _, _, _, .lit _, _ => by simp [eval] + | env, n, v, .col i, h => by + have h_ne : i ≠ n := of_decide_eq_true h + simp only [eval] + exact Env.get_replaceAt_ne env n i v h_ne + | env, n, v, .not a, h => by + simp only [Expr.colReferencesUnused] at h + simp only [eval] + rw [eval_replaceAt_of_unused env n v a h] + | env, n, v, .ifThen c t e, h => by + simp only [Expr.colReferencesUnused, Bool.and_eq_true] at h + simp only [eval] + rw [eval_replaceAt_of_unused env n v c h.1.1, + eval_replaceAt_of_unused env n v t h.1.2, + eval_replaceAt_of_unused env n v e h.2] + | env, n, v, .andN args, h => by + simp only [Expr.colReferencesUnused] at h + simp only [eval] + rw [eval_replaceAt_of_unused_argsMap env n v args h] + | env, n, v, .orN args, h => by + simp only [Expr.colReferencesUnused] at h + simp only [eval] + rw [eval_replaceAt_of_unused_argsMap env n v args h] + | env, n, v, .coalesce args, h => by + simp only [Expr.colReferencesUnused] at h + simp only [eval] + rw [eval_replaceAt_of_unused_argsMap env n v args h] + | env, n, v, .plus a b, h => by + simp only [Expr.colReferencesUnused, Bool.and_eq_true] at h + simp only [eval] + rw [eval_replaceAt_of_unused env n v a h.1, + eval_replaceAt_of_unused env n v b h.2] + | env, n, v, .minus a b, h => by + simp only [Expr.colReferencesUnused, Bool.and_eq_true] at h + simp only [eval] + rw [eval_replaceAt_of_unused env n v a h.1, + eval_replaceAt_of_unused env n v b h.2] + | env, n, v, .times a b, h => by + simp only [Expr.colReferencesUnused, Bool.and_eq_true] at h + simp only [eval] + rw [eval_replaceAt_of_unused env n v a h.1, + eval_replaceAt_of_unused env n v b h.2] + | env, n, v, .divide a b, h => by + simp only [Expr.colReferencesUnused, Bool.and_eq_true] at h + simp only [eval] + rw [eval_replaceAt_of_unused env n v a h.1, + eval_replaceAt_of_unused env n v b h.2] + | env, n, v, .eq a b, h => by + simp only [Expr.colReferencesUnused, Bool.and_eq_true] at h + simp only [eval] + rw [eval_replaceAt_of_unused env n v a h.1, + eval_replaceAt_of_unused env n v b h.2] + | env, n, v, .lt a b, h => by + simp only [Expr.colReferencesUnused, Bool.and_eq_true] at h + simp only [eval] + rw [eval_replaceAt_of_unused env n v a h.1, + eval_replaceAt_of_unused env n v b h.2] + +theorem eval_replaceAt_of_unused_argsMap : + ∀ (env : Env) (n : Nat) (v : Datum) (args : List Expr), + Expr.argsColRefUnused n args = true → + args.map (eval (Env.replaceAt env n v)) = args.map (eval env) + | _, _, _, [], _ => rfl + | env, n, v, e :: rest, h => by + simp only [Expr.argsColRefUnused, Bool.and_eq_true] at h + show eval (Env.replaceAt env n v) e :: rest.map (eval (Env.replaceAt env n v)) + = eval env e :: rest.map (eval env) + rw [eval_replaceAt_of_unused env n v e h.1, + eval_replaceAt_of_unused_argsMap env n v rest h.2] +end + +/-! ## Bridge between bounded and unused analyzers + +If a predicate's column references are bounded by `n`, then any +column index `i ≥ n` is unused. Used by the optimizer to derive +column-pruning consequences from a tight bound: a predicate that +only reads the first `n` columns leaves the rest unused. -/ + +mutual +theorem Expr.colReferencesUnused_of_bounded : + ∀ {n i : Nat} (e : Expr), + e.colReferencesBoundedBy n = true → n ≤ i → + e.colReferencesUnused i = true + | _, _, .lit _, _, _ => rfl + | n, i, .col j, h, hLe => by + have h_lt : j < n := of_decide_eq_true h + show decide (j ≠ i) = true + have : j ≠ i := fun hEq => Nat.not_lt_of_le hLe (hEq ▸ h_lt) + exact decide_eq_true this + | _, _, .not a, h, hLe => + Expr.colReferencesUnused_of_bounded a h hLe + | _, _, .ifThen c t e, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Expr.colReferencesUnused, + Bool.and_eq_true] at h ⊢ + exact ⟨⟨Expr.colReferencesUnused_of_bounded c h.1.1 hLe, + Expr.colReferencesUnused_of_bounded t h.1.2 hLe⟩, + Expr.colReferencesUnused_of_bounded e h.2 hLe⟩ + | _, _, .andN args, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Expr.colReferencesUnused] at h ⊢ + exact Expr.argsColRefUnused_of_bounded args h hLe + | _, _, .orN args, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Expr.colReferencesUnused] at h ⊢ + exact Expr.argsColRefUnused_of_bounded args h hLe + | _, _, .coalesce args, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Expr.colReferencesUnused] at h ⊢ + exact Expr.argsColRefUnused_of_bounded args h hLe + | _, _, .plus a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Expr.colReferencesUnused, + Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesUnused_of_bounded a h.1 hLe, + Expr.colReferencesUnused_of_bounded b h.2 hLe⟩ + | _, _, .minus a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Expr.colReferencesUnused, + Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesUnused_of_bounded a h.1 hLe, + Expr.colReferencesUnused_of_bounded b h.2 hLe⟩ + | _, _, .times a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Expr.colReferencesUnused, + Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesUnused_of_bounded a h.1 hLe, + Expr.colReferencesUnused_of_bounded b h.2 hLe⟩ + | _, _, .divide a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Expr.colReferencesUnused, + Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesUnused_of_bounded a h.1 hLe, + Expr.colReferencesUnused_of_bounded b h.2 hLe⟩ + | _, _, .eq a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Expr.colReferencesUnused, + Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesUnused_of_bounded a h.1 hLe, + Expr.colReferencesUnused_of_bounded b h.2 hLe⟩ + | _, _, .lt a b, h, hLe => by + simp only [Expr.colReferencesBoundedBy, Expr.colReferencesUnused, + Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesUnused_of_bounded a h.1 hLe, + Expr.colReferencesUnused_of_bounded b h.2 hLe⟩ + +theorem Expr.argsColRefUnused_of_bounded : + ∀ {n i : Nat} (args : List Expr), + Expr.argsColRefBoundedBy n args = true → n ≤ i → + Expr.argsColRefUnused i args = true + | _, _, [], _, _ => rfl + | _, _, e :: rest, h, hLe => by + simp only [Expr.argsColRefBoundedBy, Expr.argsColRefUnused, + Bool.and_eq_true] at h ⊢ + exact ⟨Expr.colReferencesUnused_of_bounded e h.1 hLe, + Expr.argsColRefUnused_of_bounded rest h.2 hLe⟩ +end + +/-! ## Shift composition laws + +`colShift` is the identity at `k = 0` and composes additively: +shifting by `k` then by `m` equals shifting by `k + m`. Useful for +nested joins where each join adds its own offset to the predicate's +column references. -/ + +mutual +theorem Expr.colShift_zero : ∀ (e : Expr), e.colShift 0 = e + | .lit _ => rfl + | .col i => by show Expr.col (0 + i) = .col i; rw [Nat.zero_add] + | .not a => by + show Expr.not (a.colShift 0) = .not a + rw [Expr.colShift_zero a] + | .ifThen c t e => by + show Expr.ifThen (c.colShift 0) (t.colShift 0) (e.colShift 0) + = .ifThen c t e + rw [Expr.colShift_zero c, Expr.colShift_zero t, Expr.colShift_zero e] + | .andN args => by + show Expr.andN (Expr.argsColShift 0 args) = .andN args + rw [Expr.argsColShift_zero args] + | .orN args => by + show Expr.orN (Expr.argsColShift 0 args) = .orN args + rw [Expr.argsColShift_zero args] + | .coalesce args => by + show Expr.coalesce (Expr.argsColShift 0 args) = .coalesce args + rw [Expr.argsColShift_zero args] + | .plus a b => by + show Expr.plus (a.colShift 0) (b.colShift 0) = .plus a b + rw [Expr.colShift_zero a, Expr.colShift_zero b] + | .minus a b => by + show Expr.minus (a.colShift 0) (b.colShift 0) = .minus a b + rw [Expr.colShift_zero a, Expr.colShift_zero b] + | .times a b => by + show Expr.times (a.colShift 0) (b.colShift 0) = .times a b + rw [Expr.colShift_zero a, Expr.colShift_zero b] + | .divide a b => by + show Expr.divide (a.colShift 0) (b.colShift 0) = .divide a b + rw [Expr.colShift_zero a, Expr.colShift_zero b] + | .eq a b => by + show Expr.eq (a.colShift 0) (b.colShift 0) = .eq a b + rw [Expr.colShift_zero a, Expr.colShift_zero b] + | .lt a b => by + show Expr.lt (a.colShift 0) (b.colShift 0) = .lt a b + rw [Expr.colShift_zero a, Expr.colShift_zero b] + +theorem Expr.argsColShift_zero : ∀ (args : List Expr), + Expr.argsColShift 0 args = args + | [] => rfl + | e :: rest => by + show e.colShift 0 :: Expr.argsColShift 0 rest = e :: rest + rw [Expr.colShift_zero e, Expr.argsColShift_zero rest] +end + +mutual +theorem Expr.colShift_add : + ∀ (k m : Nat) (e : Expr), (e.colShift k).colShift m = e.colShift (k + m) + | _, _, .lit _ => rfl + | k, m, .col i => by + show Expr.col (m + (k + i)) = Expr.col (k + m + i) + congr 1; omega + | k, m, .not a => by + show Expr.not ((a.colShift k).colShift m) = .not (a.colShift (k + m)) + rw [Expr.colShift_add k m a] + | k, m, .ifThen c t e => by + show Expr.ifThen ((c.colShift k).colShift m) ((t.colShift k).colShift m) + ((e.colShift k).colShift m) + = .ifThen (c.colShift (k + m)) (t.colShift (k + m)) (e.colShift (k + m)) + rw [Expr.colShift_add k m c, Expr.colShift_add k m t, + Expr.colShift_add k m e] + | k, m, .andN args => by + show Expr.andN (Expr.argsColShift m (Expr.argsColShift k args)) + = .andN (Expr.argsColShift (k + m) args) + rw [Expr.argsColShift_add k m args] + | k, m, .orN args => by + show Expr.orN (Expr.argsColShift m (Expr.argsColShift k args)) + = .orN (Expr.argsColShift (k + m) args) + rw [Expr.argsColShift_add k m args] + | k, m, .coalesce args => by + show Expr.coalesce (Expr.argsColShift m (Expr.argsColShift k args)) + = .coalesce (Expr.argsColShift (k + m) args) + rw [Expr.argsColShift_add k m args] + | k, m, .plus a b => by + show Expr.plus ((a.colShift k).colShift m) ((b.colShift k).colShift m) + = .plus (a.colShift (k + m)) (b.colShift (k + m)) + rw [Expr.colShift_add k m a, Expr.colShift_add k m b] + | k, m, .minus a b => by + show Expr.minus ((a.colShift k).colShift m) ((b.colShift k).colShift m) + = .minus (a.colShift (k + m)) (b.colShift (k + m)) + rw [Expr.colShift_add k m a, Expr.colShift_add k m b] + | k, m, .times a b => by + show Expr.times ((a.colShift k).colShift m) ((b.colShift k).colShift m) + = .times (a.colShift (k + m)) (b.colShift (k + m)) + rw [Expr.colShift_add k m a, Expr.colShift_add k m b] + | k, m, .divide a b => by + show Expr.divide ((a.colShift k).colShift m) ((b.colShift k).colShift m) + = .divide (a.colShift (k + m)) (b.colShift (k + m)) + rw [Expr.colShift_add k m a, Expr.colShift_add k m b] + | k, m, .eq a b => by + show Expr.eq ((a.colShift k).colShift m) ((b.colShift k).colShift m) + = .eq (a.colShift (k + m)) (b.colShift (k + m)) + rw [Expr.colShift_add k m a, Expr.colShift_add k m b] + | k, m, .lt a b => by + show Expr.lt ((a.colShift k).colShift m) ((b.colShift k).colShift m) + = .lt (a.colShift (k + m)) (b.colShift (k + m)) + rw [Expr.colShift_add k m a, Expr.colShift_add k m b] + +theorem Expr.argsColShift_add : + ∀ (k m : Nat) (args : List Expr), + Expr.argsColShift m (Expr.argsColShift k args) + = Expr.argsColShift (k + m) args + | _, _, [] => rfl + | k, m, e :: rest => by + show (e.colShift k).colShift m :: Expr.argsColShift m (Expr.argsColShift k rest) + = e.colShift (k + m) :: Expr.argsColShift (k + m) rest + rw [Expr.colShift_add k m e, Expr.argsColShift_add k m rest] +end + +end Mz diff --git a/doc/developer/semantics/Mz/Datum.lean b/doc/developer/semantics/Mz/Datum.lean new file mode 100644 index 0000000000000..5a9670e2e80e6 --- /dev/null +++ b/doc/developer/semantics/Mz/Datum.lean @@ -0,0 +1,52 @@ +/-! +# `Datum` + +The subset of Materialize's `Datum` modeled by the semantics skeleton. + +Only the variants required to state the boolean truth tables are +present: booleans, `null`, and the proposed `err` variant carrying an +opaque `EvalError` payload. Numeric, string, and temporal types are +intentionally omitted from this skeleton; adding them later does not +affect the proofs in `Mz/Boolean.lean`. + +The Rust counterpart lives in `src/repr/src/row.rs` (`Datum`) and +`src/expr/src/scalar.rs` (`EvalError`). +-/ + +namespace Mz + +/-- Cell-scoped errors raised by `Datum`-level operations. The +skeleton's variants are intentionally small; production +`EvalError` (in `src/expr/src/scalar.rs`) has many more. -/ +inductive EvalError + | divisionByZero + deriving DecidableEq, Inhabited + +/-- A modeled scalar value. + +`bool b` is a boolean literal; `int n` is an integer literal +(skeleton models `Int`, not the full SQL numeric tower); `null` +is the SQL `NULL` value; `err e` is the cell-scoped error +variant whose payload is the `EvalError` raised at the cell. -/ +inductive Datum + | bool (b : Bool) + | int (n : Int) + | null + | err (e : EvalError) + deriving DecidableEq, Inhabited + +/-- Propositional predicate "this datum is an error". + +Stated as `Prop` rather than `Bool` so it composes with `Not` and is +usable as a hypothesis in proofs without first lifting through +`= true`. The recursor over `Datum` collapses each branch to either +`True` or `False`, so `decide` (and `simp`) handles `IsErr` cleanly. -/ +def Datum.IsErr : Datum → Prop + | .err _ => True + | _ => False + +instance : DecidablePred Datum.IsErr := by + intro d + cases d <;> unfold Datum.IsErr <;> infer_instance + +end Mz diff --git a/doc/developer/semantics/Mz/Eval.lean b/doc/developer/semantics/Mz/Eval.lean new file mode 100644 index 0000000000000..1097048106a64 --- /dev/null +++ b/doc/developer/semantics/Mz/Eval.lean @@ -0,0 +1,45 @@ +import Mz.Expr +import Mz.PrimEval + +/-! +# `eval` + +Big-step evaluator. The primitive operations on `Datum` and +`List Datum` live in `Mz/PrimEval.lean`; this file only defines the +`Expr` → `Datum` translation. + +For the variadic constructors `andN`, `orN`, and `coalesce`, the +evaluator first evaluates every operand and then hands the resulting +`List Datum` to the variadic primitive. Operand evaluation uses +`List.attach` so that Lean's structural recursion checker can see +each element of `args` as a subterm of the enclosing `Expr`. + +Modeling note on laziness: in the runtime, the boolean fragment short- +circuits — once a `FALSE` is seen, the rest of the `AND` operands are +not evaluated. In this total skeleton, every `eval env e` is a total +function of its inputs, and the absorption theorems in +`Mz/Variadic.lean` guarantee that strict evaluation produces the same +`Datum` as the lazy runtime would. A future iteration that introduces +effects (resource usage, partiality, observability) will need to +reintroduce the laziness explicitly. +-/ + +namespace Mz + +/-- Big-step evaluation. -/ +def eval (env : Env) : Expr → Datum + | .lit d => d + | .col i => Env.get env i + | .not a => evalNot (eval env a) + | .ifThen c t e => evalIfThen (eval env c) (eval env t) (eval env e) + | .andN args => evalAndN (args.map (eval env)) + | .orN args => evalOrN (args.map (eval env)) + | .coalesce args => evalCoalesce (args.map (eval env)) + | .plus a b => evalPlus (eval env a) (eval env b) + | .minus a b => evalMinus (eval env a) (eval env b) + | .times a b => evalTimes (eval env a) (eval env b) + | .divide a b => evalDivide (eval env a) (eval env b) + | .eq a b => evalEq (eval env a) (eval env b) + | .lt a b => evalLt (eval env a) (eval env b) + +end Mz diff --git a/doc/developer/semantics/Mz/Expr.lean b/doc/developer/semantics/Mz/Expr.lean new file mode 100644 index 0000000000000..b662fd6484b22 --- /dev/null +++ b/doc/developer/semantics/Mz/Expr.lean @@ -0,0 +1,53 @@ +import Mz.Datum + +/-! +# `Expr` + +A minimal subset of `MirScalarExpr` (see `src/expr/src/scalar.rs`). + +Production `MirScalarExpr` carries `VariadicFunc::{And, Or}`; the +skeleton mirrors that with `andN` / `orN` and does not carry a +separate binary `and` / `or`. The binary case is the two-element +variadic, and the four-value truth tables (TRUE / FALSE / NULL / +ERROR) over `evalAnd` / `evalOr` apply at every adjacent pair of +operands through the fold that defines `evalAndN` / `evalOrN` +(see `Mz/PrimEval.lean`). +-/ + +namespace Mz + +/-- Scalar expression syntax. + +* `lit d`: literal datum. +* `col i`: reference to column `i` in the surrounding environment. +* `not a`: logical negation. +* `ifThen c t e`: PostgreSQL-style `CASE` / `If` — the only + user-controllable short-circuit in `MirScalarExpr`. +* `andN args`, `orN args`: variadic logical conjunction and + disjunction. These match `MirScalarExpr::VariadicFunc::{And, Or}` + in the runtime. The binary case is `andN [a, b]` / `orN [a, b]`. +* `coalesce args`: the error-rescuing variant of `COALESCE` proposed + in `doc/developer/design/20260517_error_handling_semantics.md`. -/ +inductive Expr + | lit (d : Datum) + | col (i : Nat) + | not (a : Expr) + | ifThen (c t e : Expr) + | andN (args : List Expr) + | orN (args : List Expr) + | coalesce (args : List Expr) + | plus (a b : Expr) + | minus (a b : Expr) + | times (a b : Expr) + | divide (a b : Expr) + | eq (a b : Expr) + | lt (a b : Expr) + deriving Inhabited + +/-- Sugar: binary AND as the two-element variadic. -/ +@[inline] def Expr.and (a b : Expr) : Expr := Expr.andN [a, b] + +/-- Sugar: binary OR as the two-element variadic. -/ +@[inline] def Expr.or (a b : Expr) : Expr := Expr.orN [a, b] + +end Mz diff --git a/doc/developer/semantics/Mz/ExprVariadic.lean b/doc/developer/semantics/Mz/ExprVariadic.lean new file mode 100644 index 0000000000000..4c621bf646c2b --- /dev/null +++ b/doc/developer/semantics/Mz/ExprVariadic.lean @@ -0,0 +1,132 @@ +import Mz.Eval +import Mz.Variadic +import Mz.Coalesce + +/-! +# `Expr`-level reduction lemmas for the variadic constructors + +The variadic `Expr` constructors (`andN`, `orN`, `coalesce`) evaluate +by mapping `eval env` across the operand list and then handing the +result to the corresponding variadic primitive. These reduction +lemmas state that explicitly so downstream proofs can rewrite without +having to unfold `eval`. + +Each lemma is a single-line `rfl` because the matching clause of +`eval` is structurally identical to the lemma's right-hand side. + +Concrete consequences derived from `Mz/Variadic.lean` follow at the +end of the file: the empty / singleton / two-operand cases of the +variadic `Expr` operators, and absorption by `FALSE` (resp. `TRUE`) +when a literal `FALSE` (resp. `TRUE`) is one of the operands. +-/ + +namespace Mz + +/-! ## eval reduction lemmas -/ + +theorem eval_andN (env : Env) (args : List Expr) : + eval env (.andN args) = evalAndN (args.map (eval env)) := by + simp only [eval] + +theorem eval_orN (env : Env) (args : List Expr) : + eval env (.orN args) = evalOrN (args.map (eval env)) := by + simp only [eval] + +theorem eval_coalesce (env : Env) (args : List Expr) : + eval env (.coalesce args) = evalCoalesce (args.map (eval env)) := by + simp only [eval] + +/-! ## Identity, singleton, and binary equivalence at the `Expr` level + +`andN []`, `orN []`, and `coalesce []` are constants. `andN [a]` and +`orN [a]` reduce to `eval env a`. `andN [a, b]` agrees with `and a b`, +and similarly for `or`. These transport the corresponding `Datum`- +level laws in `Mz/Variadic.lean` through `eval`. -/ + +theorem eval_andN_nil (env : Env) : + eval env (.andN []) = .bool true := by + rw [eval_andN]; rfl + +theorem eval_orN_nil (env : Env) : + eval env (.orN []) = .bool false := by + rw [eval_orN]; rfl + +theorem eval_andN_singleton (env : Env) (a : Expr) : + eval env (.andN [a]) = eval env a := by + rw [eval_andN] + show evalAndN [eval env a] = eval env a + exact evalAndN_singleton (eval env a) + +theorem eval_orN_singleton (env : Env) (a : Expr) : + eval env (.orN [a]) = eval env a := by + rw [eval_orN] + show evalOrN [eval env a] = eval env a + exact evalOrN_singleton (eval env a) + +theorem eval_andN_binary (env : Env) (a b : Expr) : + eval env (.andN [a, b]) = eval env (.and a b) := rfl + +theorem eval_orN_binary (env : Env) (a b : Expr) : + eval env (.orN [a, b]) = eval env (.or a b) := rfl + +/-! ## Coalesce base cases at the `Expr` level -/ + +theorem eval_coalesce_nil (env : Env) : + eval env (.coalesce []) = .null := by + rw [eval_coalesce]; rfl + +theorem eval_coalesce_singleton (env : Env) (a : Expr) : + eval env (.coalesce [a]) = eval env a := by + rw [eval_coalesce] + -- `args.map (eval env) = [eval env a]`; result depends on `eval env a`'s shape. + show evalCoalesce [eval env a] = eval env a + -- Case analysis on the underlying datum. + cases h : eval env a with + | bool b => rw [show evalCoalesce [Datum.bool b] = Datum.bool b from rfl] + | int n => rw [show evalCoalesce [Datum.int n] = Datum.int n from rfl] + | null => rw [show evalCoalesce [Datum.null] = Datum.null from rfl] + | err e => rw [show evalCoalesce [Datum.err e] = Datum.err e from rfl] + +/-! ## Variadic absorption at the `Expr` level + +A single operand that evaluates to `FALSE` (resp. `TRUE`) makes the +whole variadic `AND` (resp. `OR`) evaluate to `FALSE` (resp. `TRUE`), +regardless of the other operands — including those that produce +`err`. These theorems transport `evalAndN_false_absorbs` / +`evalOrN_true_absorbs` (in `Mz/Variadic.lean`) through `eval`, and +are what an optimizer cites when folding `e₁ AND … AND falseᵢ AND …` +to `false`. The `lit` corollary specializes the semantic premise to +the syntactic case where one of the operands is the literal `.bool +false` / `.bool true`. -/ + +theorem eval_andN_false_absorbs {env : Env} {args : List Expr} + (h : ∃ e ∈ args, eval env e = .bool false) : + eval env (.andN args) = .bool false := by + rw [eval_andN] + apply evalAndN_false_absorbs (ds := args.map (eval env)) + obtain ⟨e, he_mem, he_eq⟩ := h + exact List.mem_map.mpr ⟨e, he_mem, he_eq⟩ + +theorem eval_orN_true_absorbs {env : Env} {args : List Expr} + (h : ∃ e ∈ args, eval env e = .bool true) : + eval env (.orN args) = .bool true := by + rw [eval_orN] + apply evalOrN_true_absorbs (ds := args.map (eval env)) + obtain ⟨e, he_mem, he_eq⟩ := h + exact List.mem_map.mpr ⟨e, he_mem, he_eq⟩ + +theorem eval_andN_lit_false_absorbs {env : Env} {args : List Expr} + (h : Expr.lit (.bool false) ∈ args) : + eval env (.andN args) = .bool false := by + apply eval_andN_false_absorbs + refine ⟨Expr.lit (.bool false), h, ?_⟩ + simp only [eval] + +theorem eval_orN_lit_true_absorbs {env : Env} {args : List Expr} + (h : Expr.lit (.bool true) ∈ args) : + eval env (.orN args) = .bool true := by + apply eval_orN_true_absorbs + refine ⟨Expr.lit (.bool true), h, ?_⟩ + simp only [eval] + +end Mz diff --git a/doc/developer/semantics/Mz/Laws.lean b/doc/developer/semantics/Mz/Laws.lean new file mode 100644 index 0000000000000..f996a083aa7a8 --- /dev/null +++ b/doc/developer/semantics/Mz/Laws.lean @@ -0,0 +1,187 @@ +import Mz.Eval +import Mz.MightError + +/-! +# Algebraic laws + +Laws over `evalAnd` and `evalOr` that constrain optimizer rewrites. + +The laws here are deliberately weaker than the unconditional laws of +two-valued boolean algebra. The current Materialize runtime +(`src/expr/src/scalar/func/variadic.rs`) lets `FALSE` absorb `ERR` in +`AND` and `TRUE` absorb `ERR` in `OR`, but does not let either of +`NULL` or another `ERR` absorb `ERR`. Consequently: + +* **Idempotence** holds unconditionally for every cell of the value + lattice, including `err`. The result is *the same* error, not an + arbitrary one — this matters for rewrites that fold `x AND x` to + `x`. +* **Commutativity** holds unless both operands are errors with + distinct payloads, because `evalAnd (.err e₁) (.err e₂)` selects + `e₁` while the swapped form selects `e₂`. The conditional form + guards on `¬IsErr` for at least one operand, which is what an + optimizer that has run `might_error` analysis can prove. + +Associativity is not stated here. It fails over the four-valued +lattice in the presence of distinct errors and would require a +more delicate hypothesis; it is left for a later iteration that +introduces a partial-order on errors. +-/ + +namespace Mz + +/-! ## Identity laws + +`TRUE` is the two-sided identity for `evalAnd`; `FALSE` is the +two-sided identity for `evalOr`. The proofs verify each cell of the +non-identity argument. Identities are the seed values used by the +variadic fold in `Mz/Variadic.lean`. -/ + +theorem evalAnd_true_left (d : Datum) : evalAnd (.bool true) d = d := by + cases d with + | bool b => cases b <;> rfl + | int _ => rfl + | null => rfl + | err _ => rfl + +theorem evalAnd_true_right (d : Datum) : evalAnd d (.bool true) = d := by + cases d with + | bool b => cases b <;> rfl + | int _ => rfl + | null => rfl + | err _ => rfl + +theorem evalOr_false_left (d : Datum) : evalOr (.bool false) d = d := by + cases d with + | bool b => cases b <;> rfl + | int _ => rfl + | null => rfl + | err _ => rfl + +theorem evalOr_false_right (d : Datum) : evalOr d (.bool false) = d := by + cases d with + | bool b => cases b <;> rfl + | int _ => rfl + | null => rfl + | err _ => rfl + +/-! ## Idempotence -/ + +theorem evalAnd_idem (d : Datum) : evalAnd d d = d := by + cases d with + | bool b => cases b <;> rfl + | int n => show (if n = n then Datum.int n else Datum.null) = .int n + rw [if_pos rfl] + | null => rfl + | err _ => rfl + +theorem evalOr_idem (d : Datum) : evalOr d d = d := by + cases d with + | bool b => cases b <;> rfl + | int n => show (if n = n then Datum.int n else Datum.null) = .int n + rw [if_pos rfl] + | null => rfl + | err _ => rfl + +/-! ## Conditional commutativity + +`evalAnd` and `evalOr` commute whenever neither operand is an error. +The premise is stronger than strictly necessary — commutativity also +holds when exactly one operand is an error — but the symmetric form +matches the shape an optimizer typically carries (a `might_error` +flag per operand). A weaker premise can be added later if a transform +demands it. -/ + +theorem evalAnd_comm_of_no_err + {d₁ d₂ : Datum} (h₁ : ¬d₁.IsErr) (h₂ : ¬d₂.IsErr) : + evalAnd d₁ d₂ = evalAnd d₂ d₁ := by + cases d₁ with + | bool b₁ => + cases d₂ with + | bool b₂ => cases b₁ <;> cases b₂ <;> rfl + | int _ => cases b₁ <;> rfl + | null => cases b₁ <;> rfl + | err _ => exact (h₂ trivial).elim + | int n => + cases d₂ with + | bool b₂ => cases b₂ <;> rfl + | int m => + by_cases h : n = m + · subst h; rfl + · have h' : ¬m = n := fun h_eq => h h_eq.symm + show (if n = m then Datum.int n else Datum.null) + = (if m = n then Datum.int m else Datum.null) + rw [if_neg h, if_neg h'] + | null => rfl + | err _ => exact (h₂ trivial).elim + | null => + cases d₂ with + | bool b₂ => cases b₂ <;> rfl + | int _ => rfl + | null => rfl + | err _ => exact (h₂ trivial).elim + | err _ => exact (h₁ trivial).elim + +theorem evalOr_comm_of_no_err + {d₁ d₂ : Datum} (h₁ : ¬d₁.IsErr) (h₂ : ¬d₂.IsErr) : + evalOr d₁ d₂ = evalOr d₂ d₁ := by + cases d₁ with + | bool b₁ => + cases d₂ with + | bool b₂ => cases b₁ <;> cases b₂ <;> rfl + | int _ => cases b₁ <;> rfl + | null => cases b₁ <;> rfl + | err _ => exact (h₂ trivial).elim + | int n => + cases d₂ with + | bool b₂ => cases b₂ <;> rfl + | int m => + by_cases h : n = m + · subst h; rfl + · have h' : ¬m = n := fun h_eq => h h_eq.symm + show (if n = m then Datum.int n else Datum.null) + = (if m = n then Datum.int m else Datum.null) + rw [if_neg h, if_neg h'] + | null => rfl + | err _ => exact (h₂ trivial).elim + | null => + cases d₂ with + | bool b₂ => cases b₂ <;> rfl + | int _ => rfl + | null => rfl + | err _ => exact (h₂ trivial).elim + | err _ => exact (h₁ trivial).elim + +/-! ## Reorder safety on `Expr` + +These corollaries lift the conditional commutativity laws above +through `eval`. They are the precondition an optimizer must check +before swapping conjuncts: both operands must be statically proved +error-free by `might_error`, and the surrounding environment must be +error-free. -/ + +theorem eval_and_comm_of_no_might_error + {a b : Expr} {env : Env} + (ha : ¬(a.might_error = true)) (hb : ¬(b.might_error = true)) + (hEnv : env.ErrFree) : + eval env (.and a b) = eval env (.and b a) := by + have hae := might_error_sound a env ha hEnv + have hbe := might_error_sound b env hb hEnv + show eval env (Expr.andN [a, b]) = eval env (Expr.andN [b, a]) + simp only [eval, List.map_cons, List.map_nil, evalAndN] + rw [evalAnd_true_right, evalAnd_true_right] + exact evalAnd_comm_of_no_err hae hbe + +theorem eval_or_comm_of_no_might_error + {a b : Expr} {env : Env} + (ha : ¬(a.might_error = true)) (hb : ¬(b.might_error = true)) + (hEnv : env.ErrFree) : + eval env (.or a b) = eval env (.or b a) := by + have hae := might_error_sound a env ha hEnv + have hbe := might_error_sound b env hb hEnv + show eval env (Expr.orN [a, b]) = eval env (Expr.orN [b, a]) + simp only [eval, List.map_cons, List.map_nil, evalOrN] + rw [evalOr_false_right, evalOr_false_right] + exact evalOr_comm_of_no_err hae hbe + +end Mz diff --git a/doc/developer/semantics/Mz/MightError.lean b/doc/developer/semantics/Mz/MightError.lean new file mode 100644 index 0000000000000..e05b5f2193879 --- /dev/null +++ b/doc/developer/semantics/Mz/MightError.lean @@ -0,0 +1,874 @@ +import Mz.Eval + +/-! +# `might_error` static analyzer and soundness + +A conservative analyzer that returns `true` when an `Expr` might +evaluate to an `err`, plus the soundness theorem that justifies its +use by the optimizer: if `might_error e` is `false` and the +surrounding environment carries no errors, then `eval env e` is not +an error. + +The analyzer in `src/expr/src/scalar.rs::might_error` is more refined +(it knows about `ErrorIfNull` and literal errors). The skeleton +version is purely structural; tightening it later is additive work +that does not change the soundness statement. +-/ + +namespace Mz + +/-! ## Helper lemmas: error-free inputs yield an error-free output -/ + +theorem evalAnd_not_err + {d₁ d₂ : Datum} (h₁ : ¬d₁.IsErr) (h₂ : ¬d₂.IsErr) : + ¬(evalAnd d₁ d₂).IsErr := by + cases d₁ with + | bool b₁ => + cases d₂ with + | bool b₂ => cases b₁ <;> cases b₂ <;> (intro h; cases h) + | int _ => cases b₁ <;> (intro h; cases h) + | null => cases b₁ <;> (intro h; cases h) + | err _ => exact (h₂ trivial).elim + | int n => + cases d₂ with + | bool b₂ => cases b₂ <;> (intro h; cases h) + | int m => + show ¬(if n = m then Datum.int n else Datum.null).IsErr + split <;> (intro h; cases h) + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | null => + cases d₂ with + | bool b₂ => cases b₂ <;> (intro h; cases h) + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | err _ => exact (h₁ trivial).elim + +theorem evalOr_not_err + {d₁ d₂ : Datum} (h₁ : ¬d₁.IsErr) (h₂ : ¬d₂.IsErr) : + ¬(evalOr d₁ d₂).IsErr := by + cases d₁ with + | bool b₁ => + cases d₂ with + | bool b₂ => cases b₁ <;> cases b₂ <;> (intro h; cases h) + | int _ => cases b₁ <;> (intro h; cases h) + | null => cases b₁ <;> (intro h; cases h) + | err _ => exact (h₂ trivial).elim + | int n => + cases d₂ with + | bool b₂ => cases b₂ <;> (intro h; cases h) + | int m => + show ¬(if n = m then Datum.int n else Datum.null).IsErr + split <;> (intro h; cases h) + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | null => + cases d₂ with + | bool b₂ => cases b₂ <;> (intro h; cases h) + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | err _ => exact (h₁ trivial).elim + +theorem evalNot_not_err + {d : Datum} (h : ¬d.IsErr) : ¬(evalNot d).IsErr := by + cases d with + | bool b => cases b <;> (intro h; cases h) + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h trivial).elim + +theorem evalPlus_not_err + {d₁ d₂ : Datum} (h₁ : ¬d₁.IsErr) (h₂ : ¬d₂.IsErr) : + ¬(evalPlus d₁ d₂).IsErr := by + cases d₁ with + | bool _ => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | int _ => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | null => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | err _ => exact (h₁ trivial).elim + +theorem evalMinus_not_err + {d₁ d₂ : Datum} (h₁ : ¬d₁.IsErr) (h₂ : ¬d₂.IsErr) : + ¬(evalMinus d₁ d₂).IsErr := by + cases d₁ with + | bool _ => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | int _ => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | null => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | err _ => exact (h₁ trivial).elim + +theorem evalTimes_not_err + {d₁ d₂ : Datum} (h₁ : ¬d₁.IsErr) (h₂ : ¬d₂.IsErr) : + ¬(evalTimes d₁ d₂).IsErr := by + cases d₁ with + | bool _ => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | int _ => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | null => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | err _ => exact (h₁ trivial).elim + +theorem evalEq_not_err + {d₁ d₂ : Datum} (h₁ : ¬d₁.IsErr) (h₂ : ¬d₂.IsErr) : + ¬(evalEq d₁ d₂).IsErr := by + cases d₁ with + | bool _ => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | int _ => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | null => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | err _ => exact (h₁ trivial).elim + +theorem evalLt_not_err + {d₁ d₂ : Datum} (h₁ : ¬d₁.IsErr) (h₂ : ¬d₂.IsErr) : + ¬(evalLt d₁ d₂).IsErr := by + cases d₁ with + | bool _ => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | int _ => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | null => + cases d₂ with + | bool _ => intro h; cases h + | int _ => intro h; cases h + | null => intro h; cases h + | err _ => exact (h₂ trivial).elim + | err _ => exact (h₁ trivial).elim + +/-- Division is the canonical erring operation: a right operand +of `.int 0` produces `.err .divisionByZero` even when both +operands are otherwise error-free. So the analyzer's universal +"divide might err" verdict is exactly right; soundness on +`.divide` proceeds via the absurd-premise path. -/ +theorem evalDivide_not_err_of_nonzero + {n m : Int} (hm : m ≠ 0) : + ¬(evalDivide (.int n) (.int m)).IsErr := by + show ¬(if m = 0 then Datum.err EvalError.divisionByZero + else Datum.int (n / m)).IsErr + rw [if_neg hm] + intro h; cases h + +theorem evalDivide_zero (n : Int) : + evalDivide (.int n) (.int 0) = .err .divisionByZero := by + show (if (0 : Int) = 0 then Datum.err EvalError.divisionByZero + else Datum.int (n / 0)) + = Datum.err .divisionByZero + rw [if_pos rfl] + +/-- Generalization: any non-erring dividend divided by a literal +nonzero int does not err. The dividend can be any `Datum`; only +the divisor is constrained. -/ +theorem evalDivide_lit_nonzero + {d : Datum} {n : Int} (h : ¬d.IsErr) (hn : n ≠ 0) : + ¬(evalDivide d (.int n)).IsErr := by + cases d with + | bool _ => intro hRes; cases hRes + | int m => + show ¬(if n = 0 then Datum.err EvalError.divisionByZero + else Datum.int (m / n)).IsErr + rw [if_neg hn] + intro hRes; cases hRes + | null => intro hRes; cases hRes + | err _ => exact (h trivial).elim + +theorem evalIfThen_not_err + {dc dt de : Datum} + (hc : ¬dc.IsErr) (ht : ¬dt.IsErr) (he : ¬de.IsErr) : + ¬(evalIfThen dc dt de).IsErr := by + cases dc with + | bool b => + cases b + · -- false branch: evalIfThen reduces to `de` + simp only [evalIfThen]; exact he + · -- true branch: evalIfThen reduces to `dt` + simp only [evalIfThen]; exact ht + | int _ => + simp only [evalIfThen]; intro h; cases h + | null => + simp only [evalIfThen]; intro h; cases h + | err _ => exact (hc trivial).elim + +/-! ### Short-circuit absorbers + +`AND` absorbs to `.bool false` whenever either operand is +`.bool false`, regardless of what the other operand is. Likewise +`OR` absorbs to `.bool true` on either side. These are the +algebraic facts behind the value-level tightening of +`Expr.might_error`. -/ + +theorem evalAnd_left_false (d : Datum) : evalAnd (.bool false) d = .bool false := rfl + +theorem evalAnd_right_false (d : Datum) : evalAnd d (.bool false) = .bool false := by + cases d with + | bool b => cases b <;> rfl + | int _ => rfl + | null => rfl + | err _ => rfl + +theorem evalOr_left_true (d : Datum) : evalOr (.bool true) d = .bool true := rfl + +theorem evalOr_right_true (d : Datum) : evalOr d (.bool true) = .bool true := by + cases d with + | bool b => cases b <;> rfl + | int _ => rfl + | null => rfl + | err _ => rfl + +/-- Variadic `AND` absorbs to `.bool false` as soon as any operand +is `.bool false`. Stated inline to keep `MightError.lean` +self-contained (the same fact reappears in `Mz/Variadic.lean` +under the name `evalAndN_false_absorbs`, but importing that +module creates a cycle with `Mz/Laws.lean`). -/ +private theorem evalAndN_false_mem_eq + {ds : List Datum} (h : .bool false ∈ ds) : + evalAndN ds = .bool false := by + induction ds with + | nil => exact absurd h List.not_mem_nil + | cons hd tl ih => + rcases List.mem_cons.mp h with hHead | hTail + · subst hHead + show evalAnd (.bool false) (evalAndN tl) = .bool false + rfl + · have hTl := ih hTail + show evalAnd hd (evalAndN tl) = .bool false + rw [hTl] + exact evalAnd_right_false hd + +/-- Dual: variadic `OR` absorbs to `.bool true` as soon as any +operand is `.bool true`. -/ +private theorem evalOrN_true_mem_eq + {ds : List Datum} (h : .bool true ∈ ds) : + evalOrN ds = .bool true := by + induction ds with + | nil => exact absurd h List.not_mem_nil + | cons hd tl ih => + rcases List.mem_cons.mp h with hHead | hTail + · subst hHead + show evalOr (.bool true) (evalOrN tl) = .bool true + rfl + · have hTl := ih hTail + show evalOr hd (evalOrN tl) = .bool true + rw [hTl] + exact evalOr_right_true hd + +/-- List-level analogue of `evalAnd_not_err`: if every operand is +error-free, the variadic AND is error-free. -/ +theorem evalAndN_not_err : + ∀ {ds : List Datum}, (∀ d ∈ ds, ¬d.IsErr) → ¬(evalAndN ds).IsErr + | [], _ => by intro hRes; cases hRes + | hd :: tl, h => by + show ¬(evalAnd hd (evalAndN tl)).IsErr + apply evalAnd_not_err + · exact h hd (List.Mem.head tl) + · exact evalAndN_not_err (fun d hd_mem => h d (List.Mem.tail hd hd_mem)) + +/-- Dual: every error-free operand makes the variadic OR error-free. -/ +theorem evalOrN_not_err : + ∀ {ds : List Datum}, (∀ d ∈ ds, ¬d.IsErr) → ¬(evalOrN ds).IsErr + | [], _ => by intro hRes; cases hRes + | hd :: tl, h => by + show ¬(evalOr hd (evalOrN tl)).IsErr + apply evalOr_not_err + · exact h hd (List.Mem.head tl) + · exact evalOrN_not_err (fun d hd_mem => h d (List.Mem.tail hd hd_mem)) + +/-! ## Static analyzer + +Returns `true` when `e` might evaluate to an `err`. The current +implementation is structural with two pieces of value-level +tightening on binary `AND` and `OR`: + +* `.and (.lit (.bool false)) _` and `.and _ (.lit (.bool false))` + return `false`. The four-valued AND table has `false` as the + dominant absorber (`false AND error = false` from either side), + so a literal-false operand statically rules out an error. +* `.or (.lit (.bool true)) _` and `.or _ (.lit (.bool true))` + return `false` for the dual reason. + +Any literal `err` taints every ancestor. Columns are assumed not +to contain errors (see `Env.ErrFree`). + +For `andN` and `orN`, the analyzer recurses into the operand list +via `Expr.argsMightError`. For `coalesce`, the analyzer fires only +when *every* operand might error. + +The mutual recursion across `Expr.might_error`, +`Expr.argsMightError`, and `Expr.argsAllMightError` keeps Lean's +structural-recursion checker satisfied without an explicit +termination measure. -/ +/-- Top-of-expression literal-false detector. Non-recursive on +`Expr`; matches only the head constructor. Used by `might_error` +to identify the `false`-absorber position of binary / variadic +`AND` and the `false` branch of `IfThen`. -/ +@[simp] def Expr.isLitBoolFalse : Expr → Bool + | .lit (.bool false) => true + | _ => false + +/-- Dual: top-of-expression literal-true detector. -/ +@[simp] def Expr.isLitBoolTrue : Expr → Bool + | .lit (.bool true) => true + | _ => false + +/-- `isLitBoolFalse e = true` exactly characterizes +`e = .lit (.bool false)`. -/ +theorem Expr.eq_of_isLitBoolFalse {e : Expr} + (h : e.isLitBoolFalse = true) : e = .lit (.bool false) := by + cases e with + | lit d => + cases d with + | bool b => cases b with + | false => rfl + | true => simp [Expr.isLitBoolFalse] at h + | _ => simp [Expr.isLitBoolFalse] at h + | _ => simp [Expr.isLitBoolFalse] at h + +/-- Dual characterization. -/ +theorem Expr.eq_of_isLitBoolTrue {e : Expr} + (h : e.isLitBoolTrue = true) : e = .lit (.bool true) := by + cases e with + | lit d => + cases d with + | bool b => cases b with + | true => rfl + | false => simp [Expr.isLitBoolTrue] at h + | _ => simp [Expr.isLitBoolTrue] at h + | _ => simp [Expr.isLitBoolTrue] at h + +/-- Head matcher for "expression is a statically-safe divisor": +literal `.int n` with `n ≠ 0`. Used by `might_error` to detect +divide expressions whose divisor cannot trigger divide-by-zero. -/ +@[simp] def Expr.divisorIsSafe : Expr → Bool + | .lit (.int 0) => false + | .lit (.int _) => true + | _ => false + +/-- Characterization: `divisorIsSafe e = true` iff `e` is a +literal `.int n` with `n ≠ 0`. -/ +theorem Expr.lit_nonzero_int_of_divisorIsSafe {e : Expr} + (h : e.divisorIsSafe = true) : + ∃ n : Int, e = .lit (.int n) ∧ n ≠ 0 := by + cases e with + | lit d => + cases d with + | int n => + by_cases hZ : n = 0 + · subst hZ; simp [Expr.divisorIsSafe] at h + · exact ⟨n, rfl, hZ⟩ + | _ => simp [Expr.divisorIsSafe] at h + | _ => simp [Expr.divisorIsSafe] at h + +mutual +def Expr.might_error : Expr → Bool + | .lit (.err _) => true + | .lit _ => false + | .col _ => false + | .not a => a.might_error + | .ifThen c t e => + if c.isLitBoolTrue then t.might_error + else if c.isLitBoolFalse then e.might_error + else c.might_error || t.might_error || e.might_error + | .andN args => + if args.any (·.isLitBoolFalse) then false + else Expr.argsMightError args + | .orN args => + if args.any (·.isLitBoolTrue) then false + else Expr.argsMightError args + | .coalesce [] => false + | .coalesce (a :: rest) => a.might_error && Expr.argsAllMightError rest + | .plus a b => a.might_error || b.might_error + | .minus a b => a.might_error || b.might_error + | .times a b => a.might_error || b.might_error + | .divide a b => + if b.divisorIsSafe then a.might_error + else true + | .eq a b => a.might_error || b.might_error + | .lt a b => a.might_error || b.might_error + +/-- Bool fold of `might_error` over a list of operands ("does any +operand might-error"), declared mutually with `might_error` so +structural recursion accepts both sides. -/ +def Expr.argsMightError : List Expr → Bool + | [] => false + | e :: rest => e.might_error || Expr.argsMightError rest + +/-- Companion fold for `coalesce`: "do all operands might-error". +The empty-list base case is `true` so that the cons case +`a.might_error && argsAllMightError rest` gives the right answer +for any non-empty list. The pattern match in `Expr.might_error`'s +`.coalesce` arms handles the empty case separately. -/ +def Expr.argsAllMightError : List Expr → Bool + | [] => true + | e :: rest => e.might_error && Expr.argsAllMightError rest +end + +/-- Membership-driven introduction for `argsMightError`. If some +operand in the list might error, the whole list folds to `true`. The +contrapositive is what the soundness proof uses to extract a +per-operand non-erroring hypothesis from the analyzer's verdict on +`andN` / `orN`. -/ +theorem Expr.argsMightError_of_mem + {args : List Expr} {e : Expr} + (h_mem : e ∈ args) (h_err : e.might_error = true) : + Expr.argsMightError args = true := by + induction args with + | nil => cases h_mem + | cons hd tl ih => + show (hd.might_error || Expr.argsMightError tl) = true + cases h_mem with + | head _ => simp [h_err] + | tail _ h' => simp [ih h'] + +/-- If `argsAllMightError args` is not `true`, there is at least one +operand whose `might_error` is not `true`. This is the +"some safe operand exists" extraction used by the `coalesce` case of +soundness. -/ +theorem Expr.exists_safe_of_not_argsAllMightError + {args : List Expr} (h : ¬(Expr.argsAllMightError args = true)) : + ∃ e ∈ args, ¬(e.might_error = true) := by + induction args with + | nil => + -- argsAllMightError [] = true, contradicts h + exact (h rfl).elim + | cons hd tl ih => + -- argsAllMightError (hd :: tl) = hd.might_error && argsAllMightError tl + by_cases hd_me : hd.might_error = true + · -- hd is not safe; the safe one must be in tl. + have htl : ¬(Expr.argsAllMightError tl = true) := by + intro h_tl + apply h + show (hd.might_error && Expr.argsAllMightError tl) = true + simp [hd_me, h_tl] + obtain ⟨e, e_mem, he⟩ := ih htl + exact ⟨e, List.Mem.tail hd e_mem, he⟩ + · -- hd is the safe operand. + exact ⟨hd, List.Mem.head tl, hd_me⟩ + +/-! ## Coalesce safety + +Once `Coalesce.go` is invoked with `seenNull = true`, the result is +never an error: the empty-list base returns `.null`, and every cons +case either short-circuits to a `.bool b`, recurses with +`seenNull = true` unchanged, or updates `firstErr` without ever +flipping `seenNull` back to `false`. + +The combined lemma `Coalesce.go_not_err` strengthens that +observation: if the starting state has either `seenNull = true` or +at least one not-err element in the remaining list, the result is +not an error. -/ + +theorem Coalesce.go_not_err : + ∀ (seenNull : Bool) (firstErr : Option EvalError) (ds : List Datum), + seenNull = true ∨ (∃ d ∈ ds, ¬d.IsErr) → + ¬(Coalesce.go seenNull firstErr ds).IsErr + | true, _, [], _ => by + intro hRes + -- Coalesce.go true _ [] = .null + show False + simp only [Coalesce.go, if_true] at hRes + cases hRes + | false, _, [], h => by + -- Empty + seenNull=false: only the disjunct ∃ d ∈ [] survives, which is False. + cases h with + | inl h_true => cases h_true + | inr h_ex => + obtain ⟨_, hmem, _⟩ := h_ex + cases hmem + | _, _, .bool b :: _, _ => by + intro hRes + -- Coalesce.go _ _ (.bool b :: _) = .bool b + show False + simp only [Coalesce.go] at hRes + cases hRes + | _, _, .int n :: _, _ => by + intro hRes + -- Coalesce.go _ _ (.int n :: _) = .int n + show False + simp only [Coalesce.go] at hRes + cases hRes + | _, firstErr, .null :: rest, _ => by + -- Recurse with seenNull=true. + show ¬(Coalesce.go true firstErr rest).IsErr + exact Coalesce.go_not_err true firstErr rest (Or.inl rfl) + | seenNull, firstErr, .err e :: rest, h => by + -- Push the witness from (.err e :: rest) into rest, since .err e cannot be the witness. + have h_rest : seenNull = true ∨ ∃ d ∈ rest, ¬d.IsErr := by + cases h with + | inl h_true => exact Or.inl h_true + | inr h_ex => + obtain ⟨d, hmem, hsafe⟩ := h_ex + cases hmem with + | head _ => exact (hsafe trivial).elim + | tail _ h_tl => exact Or.inr ⟨d, h_tl, hsafe⟩ + -- Two cases on firstErr; the recursion shape is the same modulo argument. + cases firstErr with + | some firstErr' => + show ¬(Coalesce.go seenNull (some firstErr') rest).IsErr + exact Coalesce.go_not_err seenNull (some firstErr') rest h_rest + | none => + show ¬(Coalesce.go seenNull (some e) rest).IsErr + exact Coalesce.go_not_err seenNull (some e) rest h_rest + +/-- The headline lemma: an `evalCoalesce` call cannot return an +error when at least one operand evaluates to something that is not +an error. The `null`-beats-`err` tiebreak inside `Coalesce.go` does +the work. -/ +theorem evalCoalesce_not_err_of_some_safe + {ds : List Datum} (h : ∃ d ∈ ds, ¬d.IsErr) : + ¬(evalCoalesce ds).IsErr := by + show ¬(Coalesce.go false none ds).IsErr + exact Coalesce.go_not_err false none ds (Or.inr h) + +/-! ## Error-free environments -/ + +/-- An environment is error-free when every bound value is not an `err`. -/ +def Env.ErrFree (env : Env) : Prop := + ∀ d ∈ env, ¬d.IsErr + +theorem Env.get_not_err {env : Env} (hErr : env.ErrFree) (i : Nat) : + ¬(Env.get env i).IsErr := by + induction env generalizing i with + | nil => + -- `Env.get [] i = .null` by definition; `.null` is not an error. + intro h + cases h + | cons hd tl ih => + cases i with + | zero => + -- `Env.get (hd :: tl) 0 = hd`. `hd ∈ hd :: tl`, so `ErrFree` rules out err. + apply hErr hd + exact List.Mem.head tl + | succ n => + -- Reduce to the tail and apply the IH. + apply ih + intro d hd_mem + apply hErr d + exact List.Mem.tail hd hd_mem + +/-! ## Soundness -/ + +/-- If `might_error e` is `false` and the environment carries no +errors, then `eval env e` is not an error. + +The proof is structural recursion on `e`. `induction` cannot be used +on `Expr` because it is a nested inductive type, so the proof is +written as a recursive `theorem` that pattern-matches the constructor +and recurses on subexpressions. For each compound case the hypothesis +`¬e.might_error = true` decomposes into per-subexpression hypotheses, +and the matching helper lemma (`evalAnd_not_err` etc.) concludes. + +The `andN` / `orN` cases extract a per-operand non-erroring witness +through `Expr.argsMightError_of_mem` and then recurse via +`might_error_sound` on the individual operand. The `coalesce` case +is currently vacuous — `might_error` always returns `true` for +`.coalesce`, so the soundness premise is absurd. A future refinement +will tighten that case alongside the analyzer. -/ +theorem might_error_sound : + ∀ (e : Expr) (env : Env), + ¬(e.might_error = true) → env.ErrFree → ¬(eval env e).IsErr + | .lit d, _, hMe, _ => by + intro hRes + simp only [eval] at hRes + cases d with + | bool _ => cases hRes + | int _ => cases hRes + | null => cases hRes + | err _ => + apply hMe + simp only [Expr.might_error] + | .col i, env, _, hEnv => by + intro hRes + simp only [eval] at hRes + exact Env.get_not_err hEnv i hRes + | .not a, env, hMe, hEnv => by + intro hRes + simp only [eval] at hRes + have ha : ¬(a.might_error = true) := fun h => hMe (by simp [Expr.might_error, h]) + exact evalNot_not_err (might_error_sound a env ha hEnv) hRes + | .ifThen c t e, env, hMe, hEnv => by + intro hRes + simp only [eval] at hRes + cases hCT : c.isLitBoolTrue with + | true => + -- c = .lit (.bool true): evalIfThen .bool true dt de = dt + have hEq : c = .lit (.bool true) := by + cases c with + | lit d => + cases d with + | bool b' => cases b' with + | true => rfl + | false => simp [Expr.isLitBoolTrue] at hCT + | _ => simp [Expr.isLitBoolTrue] at hCT + | _ => simp [Expr.isLitBoolTrue] at hCT + rw [hEq] at hRes + simp only [eval] at hRes + -- hRes : (evalIfThen .bool true (eval env t) (eval env e)).IsErr + -- evalIfThen .bool true dt _ = dt by definition + have h_reduce : evalIfThen (.bool true) (eval env t) (eval env e) = eval env t := rfl + rw [h_reduce] at hRes + have ht : ¬(t.might_error = true) := fun h => hMe (by + rw [hEq] + show (if (Expr.lit (.bool true)).isLitBoolTrue then t.might_error + else if (Expr.lit (.bool true)).isLitBoolFalse then e.might_error + else (Expr.lit (.bool true)).might_error || t.might_error || e.might_error) + = true + simp [Expr.isLitBoolTrue, h]) + exact might_error_sound t env ht hEnv hRes + | false => + cases hCF : c.isLitBoolFalse with + | true => + have hEq : c = .lit (.bool false) := by + cases c with + | lit d => + cases d with + | bool b' => cases b' with + | false => rfl + | true => simp [Expr.isLitBoolFalse] at hCF + | _ => simp [Expr.isLitBoolFalse] at hCF + | _ => simp [Expr.isLitBoolFalse] at hCF + rw [hEq] at hRes + simp only [eval] at hRes + have h_reduce : evalIfThen (.bool false) (eval env t) (eval env e) = eval env e := rfl + rw [h_reduce] at hRes + have he : ¬(e.might_error = true) := fun h => hMe (by + rw [hEq] + show (if (Expr.lit (.bool false)).isLitBoolTrue then t.might_error + else if (Expr.lit (.bool false)).isLitBoolFalse then e.might_error + else (Expr.lit (.bool false)).might_error || t.might_error || e.might_error) + = true + simp [Expr.isLitBoolTrue, Expr.isLitBoolFalse, h]) + exact might_error_sound e env he hEnv hRes + | false => + -- Non-short-circuit branch + have hMeReduce : + Expr.might_error (.ifThen c t e) + = (c.might_error || t.might_error || e.might_error) := by + show (if c.isLitBoolTrue then t.might_error + else if c.isLitBoolFalse then e.might_error + else c.might_error || t.might_error || e.might_error) + = (c.might_error || t.might_error || e.might_error) + rw [hCT, hCF] + rfl + rw [hMeReduce] at hMe + have hc : ¬(c.might_error = true) := fun h => hMe (by simp [h]) + have ht : ¬(t.might_error = true) := fun h => hMe (by simp [h]) + have he : ¬(e.might_error = true) := fun h => hMe (by simp [h]) + exact evalIfThen_not_err + (might_error_sound c env hc hEnv) + (might_error_sound t env ht hEnv) + (might_error_sound e env he hEnv) hRes + | .andN args, env, hMe, hEnv => by + intro hRes + cases hAny : args.any (·.isLitBoolFalse) with + | true => + -- Some operand is `.lit (.bool false)`. evalAndN absorbs to `.bool false`. + obtain ⟨e, he_mem, he_lit⟩ := List.any_eq_true.mp hAny + have hEq : e = .lit (.bool false) := Expr.eq_of_isLitBoolFalse he_lit + rw [hEq] at he_mem + have hEvalLit : eval env (.lit (.bool false)) = .bool false := by + simp only [eval] + have hMapMem : (Datum.bool false) ∈ args.map (eval env) := + List.mem_map.mpr ⟨.lit (.bool false), he_mem, hEvalLit⟩ + simp only [eval] at hRes + rw [evalAndN_false_mem_eq hMapMem] at hRes + cases hRes + | false => + have hMeReduce : + Expr.might_error (.andN args) = Expr.argsMightError args := by + show (if args.any (·.isLitBoolFalse) then false + else Expr.argsMightError args) + = Expr.argsMightError args + rw [hAny]; rfl + rw [hMeReduce] at hMe + simp only [eval] at hRes + apply evalAndN_not_err (ds := args.map (eval env)) ?_ hRes + intro d hd_mem + obtain ⟨e, e_mem, h_eq⟩ := List.mem_map.mp hd_mem + subst h_eq + have he : ¬(e.might_error = true) := fun h => hMe + (Expr.argsMightError_of_mem e_mem h) + exact might_error_sound e env he hEnv + | .orN args, env, hMe, hEnv => by + intro hRes + cases hAny : args.any (·.isLitBoolTrue) with + | true => + obtain ⟨e, he_mem, he_lit⟩ := List.any_eq_true.mp hAny + have hEq : e = .lit (.bool true) := Expr.eq_of_isLitBoolTrue he_lit + rw [hEq] at he_mem + have hEvalLit : eval env (.lit (.bool true)) = .bool true := by + simp only [eval] + have hMapMem : (Datum.bool true) ∈ args.map (eval env) := + List.mem_map.mpr ⟨.lit (.bool true), he_mem, hEvalLit⟩ + simp only [eval] at hRes + rw [evalOrN_true_mem_eq hMapMem] at hRes + cases hRes + | false => + have hMeReduce : + Expr.might_error (.orN args) = Expr.argsMightError args := by + show (if args.any (·.isLitBoolTrue) then false + else Expr.argsMightError args) + = Expr.argsMightError args + rw [hAny]; rfl + rw [hMeReduce] at hMe + simp only [eval] at hRes + apply evalOrN_not_err (ds := args.map (eval env)) ?_ hRes + intro d hd_mem + obtain ⟨e, e_mem, h_eq⟩ := List.mem_map.mp hd_mem + subst h_eq + have he : ¬(e.might_error = true) := fun h => hMe + (Expr.argsMightError_of_mem e_mem h) + exact might_error_sound e env he hEnv + | .coalesce args, env, hMe, hEnv => by + intro hRes + simp only [eval] at hRes + -- Empty list: `evalCoalesce [] = .null`, immediately not an error. + match args, hMe, hRes with + | [], _, hRes' => + simp [evalCoalesce, Coalesce.go] at hRes' + cases hRes' + | a :: rest, hMe', hRes' => + -- Non-empty case. `might_error (.coalesce (a :: rest))` reduces to + -- `a.might_error && argsAllMightError rest`, which is exactly + -- `argsAllMightError (a :: rest)`. Negate and extract a safe operand. + have hAll : ¬(Expr.argsAllMightError (a :: rest) = true) := by + intro hAll + apply hMe' + show (a.might_error && Expr.argsAllMightError rest) = true + -- `argsAllMightError (a :: rest)` reduces by definition to the + -- conjunction we need. + exact hAll + obtain ⟨e, e_mem, he_safe⟩ := + Expr.exists_safe_of_not_argsAllMightError hAll + have he : ¬(eval env e).IsErr := might_error_sound e env he_safe hEnv + apply evalCoalesce_not_err_of_some_safe + (ds := (a :: rest).map (eval env)) + ?_ hRes' + exact ⟨eval env e, List.mem_map.mpr ⟨e, e_mem, rfl⟩, he⟩ + | .plus a b, env, hMe, hEnv => by + intro hRes + simp only [eval] at hRes + have ha : ¬(a.might_error = true) := fun h => hMe (by simp [Expr.might_error, h]) + have hb : ¬(b.might_error = true) := fun h => hMe (by simp [Expr.might_error, h]) + exact evalPlus_not_err + (might_error_sound a env ha hEnv) + (might_error_sound b env hb hEnv) hRes + | .minus a b, env, hMe, hEnv => by + intro hRes + simp only [eval] at hRes + have ha : ¬(a.might_error = true) := fun h => hMe (by simp [Expr.might_error, h]) + have hb : ¬(b.might_error = true) := fun h => hMe (by simp [Expr.might_error, h]) + exact evalMinus_not_err + (might_error_sound a env ha hEnv) + (might_error_sound b env hb hEnv) hRes + | .times a b, env, hMe, hEnv => by + intro hRes + simp only [eval] at hRes + have ha : ¬(a.might_error = true) := fun h => hMe (by simp [Expr.might_error, h]) + have hb : ¬(b.might_error = true) := fun h => hMe (by simp [Expr.might_error, h]) + exact evalTimes_not_err + (might_error_sound a env ha hEnv) + (might_error_sound b env hb hEnv) hRes + | .divide a b, env, hMe, hEnv => by + intro hRes + simp only [eval] at hRes + cases hSafe : b.divisorIsSafe with + | true => + -- b is a literal nonzero int: evalDivide _ (.int n) errs only on div0 + obtain ⟨n, hEqB, hNZ⟩ := Expr.lit_nonzero_int_of_divisorIsSafe hSafe + have hMeReduce : + Expr.might_error (.divide a b) = a.might_error := by + show (if b.divisorIsSafe = true then a.might_error else true) + = a.might_error + rw [hSafe]; rfl + rw [hMeReduce] at hMe + have hAe := might_error_sound a env hMe hEnv + rw [hEqB] at hRes + simp only [eval] at hRes + exact evalDivide_lit_nonzero hAe hNZ hRes + | false => + -- conservative branch: might_error returns `true`, premise absurd + have hMeTrue : Expr.might_error (.divide a b) = true := by + show (if b.divisorIsSafe = true then a.might_error else true) = true + rw [hSafe]; rfl + exact hMe hMeTrue + | .eq a b, env, hMe, hEnv => by + intro hRes + simp only [eval] at hRes + have ha : ¬(a.might_error = true) := fun h => hMe (by simp [Expr.might_error, h]) + have hb : ¬(b.might_error = true) := fun h => hMe (by simp [Expr.might_error, h]) + exact evalEq_not_err + (might_error_sound a env ha hEnv) + (might_error_sound b env hb hEnv) hRes + | .lt a b, env, hMe, hEnv => by + intro hRes + simp only [eval] at hRes + have ha : ¬(a.might_error = true) := fun h => hMe (by simp [Expr.might_error, h]) + have hb : ¬(b.might_error = true) := fun h => hMe (by simp [Expr.might_error, h]) + exact evalLt_not_err + (might_error_sound a env ha hEnv) + (might_error_sound b env hb hEnv) hRes + +end Mz diff --git a/doc/developer/semantics/Mz/PrimEval.lean b/doc/developer/semantics/Mz/PrimEval.lean new file mode 100644 index 0000000000000..ee9c74818dcee --- /dev/null +++ b/doc/developer/semantics/Mz/PrimEval.lean @@ -0,0 +1,218 @@ +import Mz.Datum + +/-! +# Primitive scalar evaluators + +This file collects every evaluator that operates on `Datum` (or +`List Datum`) without reference to `Expr`. The split keeps the +defining equations available to both the algebraic-law files +(`Boolean.lean`, `Laws.lean`, `Strict.lean`, etc.) and the +expression-level evaluator (`Eval.lean`) without circular imports. + +The primitives split into three groups: + +* **Binary boolean and ternary if-then**: `evalAnd`, `evalOr`, + `evalNot`, `evalIfThen`. Match the runtime in + `src/expr/src/scalar/func/variadic.rs`. +* **Environment**: `Env`, `Env.get`. Indexed lookups for `Expr.col`. +* **Variadic primitives**: `evalAndN`, `evalOrN`, `evalCoalesce`. + Used directly by `Expr.andN`, `Expr.orN`, `Expr.coalesce` + evaluation in `Eval.lean`. +-/ + +namespace Mz + +/-! ## Binary and ternary boolean evaluators -/ + +/-- AND evaluation table. Pattern order encodes the absorption +hierarchy `FALSE > ERROR > NULL > TRUE`. Non-boolean operands +(`.int _`) are preserved when paired with the identity element +`.bool true` (or another `.int`), so the algebraic laws +`evalAnd_true_left/right` and `evalAnd_idem` hold universally. +SQL would reject `.int` in `AND` at type-check time; the +skeleton's semantics is a coherent total extension. -/ +def evalAnd : Datum → Datum → Datum + | .bool false, _ => .bool false + | _, .bool false => .bool false + | .err e, _ => .err e + | _, .err e => .err e + | .null, _ => .null + | _, .null => .null + | .bool true, .bool true => .bool true + | .bool true, .int n => .int n + | .int n, .bool true => .int n + | .int n, .int m => if n = m then .int n else .null + +/-- OR evaluation table. Mirror of `evalAnd` with `TRUE` as the +dominant absorber: `TRUE > ERROR > NULL > FALSE`. Identity on +`.int` operands paired with the identity element `.bool false`. -/ +def evalOr : Datum → Datum → Datum + | .bool true, _ => .bool true + | _, .bool true => .bool true + | .err e, _ => .err e + | _, .err e => .err e + | .null, _ => .null + | _, .null => .null + | .bool false, .bool false => .bool false + | .bool false, .int n => .int n + | .int n, .bool false => .int n + | .int n, .int m => if n = m then .int n else .null + +/-- NOT evaluation table. Strict on `null` and `err`. Numeric +operands pass through unchanged so that `evalNot` stays +involutive on `.int` even though SQL would type-reject it. -/ +def evalNot : Datum → Datum + | .bool b => .bool (!b) + | .null => .null + | .err e => .err e + | .int n => .int n + +/-- `IfThen` evaluation table. Modeled strictly; see `Mz/Eval.lean` +for the discussion of lazy vs strict in a total skeleton. -/ +def evalIfThen : Datum → Datum → Datum → Datum + | .bool true, dt, _ => dt + | .bool false, _, de => de + | .null, _, _ => .null + | .err e, _, _ => .err e + | _, _, _ => .null + +/-! ## Numeric arithmetic + +Binary integer arithmetic. Strict on `.err` and `.null`. Non- +numeric operands route to `.null` for totality. Division by zero +returns `.err .divisionByZero` — the canonical cell-scoped error +the design doc cites. -/ + +/-- Integer addition. Strict on `.err` (propagates) and `.null` +(propagates). Type-mismatched operands route to `.null`. -/ +def evalPlus : Datum → Datum → Datum + | .err e, _ => .err e + | _, .err e => .err e + | .null, _ => .null + | _, .null => .null + | .int n, .int m => .int (n + m) + | _, _ => .null + +/-- Integer subtraction. Same propagation rules as `evalPlus`. -/ +def evalMinus : Datum → Datum → Datum + | .err e, _ => .err e + | _, .err e => .err e + | .null, _ => .null + | _, .null => .null + | .int n, .int m => .int (n - m) + | _, _ => .null + +/-- Integer multiplication. Same propagation rules. -/ +def evalTimes : Datum → Datum → Datum + | .err e, _ => .err e + | _, .err e => .err e + | .null, _ => .null + | _, .null => .null + | .int n, .int m => .int (n * m) + | _, _ => .null + +/-- Integer division. Strict on `.err` and `.null`. A right +operand of `.int 0` produces `.err .divisionByZero`. -/ +def evalDivide : Datum → Datum → Datum + | .err e, _ => .err e + | _, .err e => .err e + | .null, _ => .null + | _, .null => .null + | .int n, .int m => if m = 0 then .err .divisionByZero else .int (n / m) + | _, _ => .null + +/-! ## Comparison + +Binary comparison primitives. Strict on `.err` (propagates the +left-most err) and `.null` (propagates `.null`). Mixed-type +operands route to `.null` — the skeleton does not model SQL +implicit casts. Booleans compare by SQL's `false < true` ordering; +integers compare by `Int`'s built-in `<` / `=`. + +The output is always a `.bool`, `.null`, or `.err` — never a +numeric or string. This keeps comparisons compatible with the +boolean fragment as a `WHERE` predicate. -/ + +/-- Equality test. `.bool x = .bool y` and `.int n = .int m` use +the decidable equality of the base types; mixed types yield +`.null`. -/ +def evalEq : Datum → Datum → Datum + | .err e, _ => .err e + | _, .err e => .err e + | .null, _ => .null + | _, .null => .null + | .bool x, .bool y => .bool (decide (x = y)) + | .int n, .int m => .bool (decide (n = m)) + | _, _ => .null + +/-- Strict less-than. Booleans compare with `false < true`; +integers compare with `Int`'s `<`. Mixed types yield `.null`. -/ +def evalLt : Datum → Datum → Datum + | .err e, _ => .err e + | _, .err e => .err e + | .null, _ => .null + | _, .null => .null + | .bool x, .bool y => .bool (decide (x < y)) + | .int n, .int m => .bool (decide (n < m)) + | _, _ => .null + +/-! ## Environment -/ + +/-- Environment: a positional list of bindings for `Expr.col`. -/ +abbrev Env := List Datum + +/-- Reading an out-of-bounds column yields `NULL`. Defined by +primitive recursion to keep inductive proofs simple. -/ +def Env.get : Env → Nat → Datum + | [], _ => .null + | d :: _, 0 => d + | _ :: rest, n + 1 => Env.get rest n + +/-! ## Variadic primitives + +Variadic `AND`, `OR`, and `COALESCE` evaluators over `List Datum`. +The fold-style definitions are exposed here so `eval` in +`Mz/Eval.lean` can refer to them by name without a forward +dependency. The theorems for these evaluators live in +`Mz/Variadic.lean` and `Mz/Coalesce.lean`. -/ + +/-- Right-fold variadic AND. Seed value `TRUE` is the identity for +`evalAnd`, giving the cons recurrence by `rfl`. -/ +def evalAndN : List Datum → Datum + | [] => .bool true + | d :: rest => evalAnd d (evalAndN rest) + +/-- Right-fold variadic OR. Dual of `evalAndN`. -/ +def evalOrN : List Datum → Datum + | [] => .bool false + | d :: rest => evalOr d (evalOrN rest) + +/-! ### Coalesce state machine + +`Coalesce.go` carries the `seenNull` sticky bit and the earliest +`err` payload while walking operands. The first concrete value +(`.bool _`) short-circuits the walk. -/ + +def Coalesce.go (seenNull : Bool) (firstErr : Option EvalError) : + List Datum → Datum + | [] => + if seenNull then .null + else + match firstErr with + | some e => .err e + | none => .null + | .bool b :: _ => .bool b + | .int n :: _ => .int n + | .null :: rest => Coalesce.go true firstErr rest + | .err e :: rest => + match firstErr with + | some _ => Coalesce.go seenNull firstErr rest + | none => Coalesce.go seenNull (some e) rest + +/-- `coalesce` returns the first concrete operand, with a +`null`-beats-`err` tiebreak when none exists. See `Mz/Coalesce.lean` +for the laws. -/ +def evalCoalesce : List Datum → Datum := + Coalesce.go false none + +end Mz diff --git a/doc/developer/semantics/Mz/Pushdown.lean b/doc/developer/semantics/Mz/Pushdown.lean new file mode 100644 index 0000000000000..f7b3fdc930a1a --- /dev/null +++ b/doc/developer/semantics/Mz/Pushdown.lean @@ -0,0 +1,176 @@ +import Mz.Eval +import Mz.Bag + +/-! +# Predicate pushdown across projection + +The classical relational rewrite: + + `filterRel p (project es rel) = project es (filterRel (p[es]) rel)` + +where `p[es]` is the substitution that replaces each `Expr.col i` in +`p` with `es.get i` (the i-th scalar of the projection). The +rewrite is the basis for moving a `WHERE` clause through a `SELECT` +clause whenever the predicate's column references can be expressed +in terms of the projection's source. + +This file gives the substitution machinery (`Expr.subst`, +`Expr.substArgs`) and the two theorems an optimizer cites: + +* `eval_subst`: substituting and then evaluating against the + original row equals evaluating against the projected row. +* `filterRel_pushdown_project`: the relational pushdown rewrite. + +`Expr.subst` is mutually recursive with `Expr.substArgs` so Lean's +structural-recursion checker handles the nested-list constructors +(`andN`, `orN`, `coalesce`) without an explicit termination measure. +-/ + +namespace Mz + +/-! ## Substitution -/ + +mutual +/-- Substitute column references in `e` with the i-th scalar of +`es`. Out-of-bounds references are replaced by `.lit .null` so that +the resulting expression evaluates to `.null`, matching `Env.get`'s +fallback. -/ +def Expr.subst (es : List Expr) : Expr → Expr + | .lit d => .lit d + | .col i => es.getD i (.lit .null) + | .not a => .not (a.subst es) + | .ifThen c t e => .ifThen (c.subst es) (t.subst es) (e.subst es) + | .andN args => .andN (Expr.substArgs es args) + | .orN args => .orN (Expr.substArgs es args) + | .coalesce args => .coalesce (Expr.substArgs es args) + | .plus a b => .plus (a.subst es) (b.subst es) + | .minus a b => .minus (a.subst es) (b.subst es) + | .times a b => .times (a.subst es) (b.subst es) + | .divide a b => .divide (a.subst es) (b.subst es) + | .eq a b => .eq (a.subst es) (b.subst es) + | .lt a b => .lt (a.subst es) (b.subst es) + +/-- Pointwise application of `subst` to a list of operands. -/ +def Expr.substArgs (es : List Expr) : List Expr → List Expr + | [] => [] + | e :: rest => e.subst es :: Expr.substArgs es rest +end + +/-! ## Helpers for substitution / map agreement + +`substArgs es args` and `args.map (·.subst es)` produce the same +list. The skeleton uses the explicit recursive `substArgs` form in +the definition so structural recursion is accepted; the proofs +benefit from being able to switch to `List.map` when needed. -/ + +theorem Expr.substArgs_eq_map (es args : List Expr) : + Expr.substArgs es args = args.map (·.subst es) := by + induction args with + | nil => rfl + | cons hd tl ih => simp [Expr.substArgs, ih] + +/-! ## Substitution preserves evaluation -/ + +/-- Reading column `i` from the projected row equals evaluating the +i-th projection scalar on the original row. The proof case-splits on +whether `i` is in bounds. -/ +private theorem Env.get_map_eval (env : Env) (es : List Expr) (i : Nat) : + Env.get (es.map (eval env)) i = eval env (es.getD i (.lit .null)) := by + induction es generalizing i with + | nil => + -- both sides reduce to `.null` + show Env.get [] i = eval env (.lit .null) + simp [Env.get, eval] + | cons hd tl ih => + cases i with + | zero => + -- LHS: Env.get (eval env hd :: tl.map (eval env)) 0 = eval env hd + -- RHS: eval env ((hd :: tl).getD 0 (.lit .null)) = eval env hd + show Env.get ((eval env hd) :: tl.map (eval env)) 0 = eval env hd + rfl + | succ n => + -- recurse on tl + show Env.get (eval env hd :: tl.map (eval env)) (n + 1) + = eval env ((hd :: tl).getD (n + 1) (.lit .null)) + show Env.get (tl.map (eval env)) n = eval env (tl.getD n (.lit .null)) + exact ih n + +/-- The headline theorem: substituting into `e` and evaluating +against the original row equals evaluating the original `e` against +the projected row. + +The proof is structural recursion on `e`, mirroring the structure of +`Expr.subst`. The nested-list constructors recurse through +`Expr.substArgs` and are handled by `eval_substArgs` below. -/ +theorem eval_subst : + ∀ (env : Env) (es : List Expr) (e : Expr), + eval env (e.subst es) = eval (es.map (eval env)) e + | env, es, .lit d => by + simp only [Expr.subst, eval] + | env, es, .col i => by + simp only [Expr.subst, eval] + exact (Env.get_map_eval env es i).symm + | env, es, .not a => by + simp only [Expr.subst, eval] + rw [eval_subst env es a] + | env, es, .ifThen c t e => by + simp only [Expr.subst, eval] + rw [eval_subst env es c, eval_subst env es t, eval_subst env es e] + | env, es, .andN args => by + simp only [Expr.subst, eval, Expr.substArgs_eq_map] + rw [List.map_map] + congr 1 + apply List.map_congr_left + intro e _ + exact eval_subst env es e + | env, es, .orN args => by + simp only [Expr.subst, eval, Expr.substArgs_eq_map] + rw [List.map_map] + congr 1 + apply List.map_congr_left + intro e _ + exact eval_subst env es e + | env, es, .coalesce args => by + simp only [Expr.subst, eval, Expr.substArgs_eq_map] + rw [List.map_map] + congr 1 + apply List.map_congr_left + intro e _ + exact eval_subst env es e + | env, es, .plus a b => by + simp only [Expr.subst, eval] + rw [eval_subst env es a, eval_subst env es b] + | env, es, .minus a b => by + simp only [Expr.subst, eval] + rw [eval_subst env es a, eval_subst env es b] + | env, es, .times a b => by + simp only [Expr.subst, eval] + rw [eval_subst env es a, eval_subst env es b] + | env, es, .divide a b => by + simp only [Expr.subst, eval] + rw [eval_subst env es a, eval_subst env es b] + | env, es, .eq a b => by + simp only [Expr.subst, eval] + rw [eval_subst env es a, eval_subst env es b] + | env, es, .lt a b => by + simp only [Expr.subst, eval] + rw [eval_subst env es a, eval_subst env es b] + +/-! ## Predicate pushdown -/ + +/-- The classical predicate-pushdown rewrite. Filtering after +projecting agrees with substituting the projection scalars into the +predicate and filtering before projecting. -/ +theorem filterRel_pushdown_project (p : Expr) (es : List Expr) (rel : Relation) : + filterRel p (project es rel) = project es (filterRel (p.subst es) rel) := by + unfold filterRel project + rw [List.filter_map] + congr 1 + apply List.filter_congr + intro row _ + -- Goal: (rowPredicate p ∘ (fun row => es.map (eval row))) row = rowPredicate (p.subst es) row + show rowPredicate p (es.map (eval row)) = rowPredicate (p.subst es) row + unfold rowPredicate + rw [eval_subst row es p] + +end Mz diff --git a/doc/developer/semantics/Mz/Stream.lean b/doc/developer/semantics/Mz/Stream.lean new file mode 100644 index 0000000000000..be7579b6ac7d6 --- /dev/null +++ b/doc/developer/semantics/Mz/Stream.lean @@ -0,0 +1,200 @@ +import Mz.Bag +import Mz.Eval + +/-! +# Two-diff stream + +Per the design doc +(`doc/developer/design/20260517_error_handling_semantics.md`, +§"Stream shape: two-diff records"), the unit of denotation is a +stream of records + +``` +(row : List Datum, diff : Int, err_diff : Int) +``` + +`diff` counts valid copies of `row`; `err_diff` counts erred copies. +Both are ordinary `Int` diffs that retract. + +This file is the skeleton's restart after the per-error-payload +diff-component experiment was concluded. The previous attempt +(`Diff = Int × ErrCount`) is preserved in git history on this +branch as a worked alternative. + +The skeleton currently models: + +* Stream record + `Stream` type alias. +* `filter` per the design doc's Predicates rule. +* `project` evaluating each scalar; `Datum::Error` results land in + cells. +* `cross` with the two-component multiplicative rule from the + Joins section. +* `negate`, `unionAll`, basic reduction lemmas. + +Global-scoped errors (absorbing `DiffWithGlobal` marker) and +`DataflowError` structured payloads are deferred to follow-up +files. The current focus is the row-scoped layer: data multiplicity +and err multiplicity, both retractable. -/ + +namespace Mz + +/-- A stream record: a row, its data multiplicity, and its err +multiplicity. Both diffs are ordinary `Int`. A row appearing +`(diff, err_diff) = (1, 0)` is a valid output; `(0, 1)` is an erred +output; `(1, 1)` is both (rare but representable). Retractions are +negative multiplicities. -/ +structure StreamRecord where + row : Row + diff : Int + err_diff : Int + deriving Inhabited + +/-- A stream is a list of stream records. Ordinary differential- +dataflow consolidation sums per `(row, time)` bucket; the time +dimension is not modeled here yet. -/ +abbrev Stream := List StreamRecord + +namespace Stream + +/-! ## Filter + +Per the design doc: + +* `eval r pred = .bool true` → record unchanged. +* `eval r pred = .bool false` → data multiplicity zeroed, err untouched. +* `eval r pred = .null` → data multiplicity zeroed, err untouched. +* `eval r pred = .int n` → data multiplicity zeroed, err untouched. +* `eval r pred = .err e` → data multiplicity migrates to err side; + `e` is the structured payload to be + carried via `DataflowError::EvalError` + (deferred). -/ + +/-- Per-record filter action. -/ +@[inline] def filterOne (pred : Expr) (rec : StreamRecord) : StreamRecord := + match eval rec.row pred with + | .bool true => + rec + | .err _ => + -- Data multiplicity migrates to err side; structured EvalError + -- payload is intentionally not yet modeled — see deferred work. + { row := rec.row, diff := 0, err_diff := rec.err_diff + rec.diff } + | _ => + -- .bool false / .null / .int — data drops, err untouched. + { row := rec.row, diff := 0, err_diff := rec.err_diff } + +/-- Filter a stream by a predicate. -/ +def filter (pred : Expr) (s : Stream) : Stream := + s.map (filterOne pred) + +theorem filter_nil (pred : Expr) : + filter pred [] = [] := rfl + +theorem filter_append (pred : Expr) (a b : Stream) : + filter pred (a ++ b) = filter pred a ++ filter pred b := by + unfold filter + exact List.map_append + +/-! ## Project + +Evaluate each scalar in `es` against the row. The resulting row +is `es.map (eval r)`. A scalar that errs produces `Datum.err _` in +that column — the err lives in the cell, not in the diff. Diffs +pass through unchanged. -/ + +/-- Per-record project action. -/ +@[inline] def projectOne (es : List Expr) (rec : StreamRecord) : StreamRecord := + { row := es.map (eval rec.row) + , diff := rec.diff + , err_diff := rec.err_diff } + +/-- Project a stream through a list of scalar expressions. -/ +def project (es : List Expr) (s : Stream) : Stream := + s.map (projectOne es) + +theorem project_nil_stream (es : List Expr) : + project es [] = [] := rfl + +theorem project_append (es : List Expr) (a b : Stream) : + project es (a ++ b) = project es a ++ project es b := by + unfold project + exact List.map_append + +/-! ## Negate + +Pointwise negation of both diff components. -/ + +def negate (s : Stream) : Stream := + s.map fun rec => { row := rec.row, diff := -rec.diff, err_diff := -rec.err_diff } + +theorem negate_nil : negate [] = [] := rfl + +theorem negate_append (a b : Stream) : + negate (a ++ b) = negate a ++ negate b := by + unfold negate + exact List.map_append + +theorem negate_negate (s : Stream) : + negate (negate s) = s := by + induction s with + | nil => rfl + | cons hd tl ih => + show negate (negate (hd :: tl)) = hd :: tl + show { row := hd.row, diff := - -hd.diff, err_diff := - -hd.err_diff } + :: negate (negate tl) = hd :: tl + rw [ih] + have h1 : - -hd.diff = hd.diff := Int.neg_neg _ + have h2 : - -hd.err_diff = hd.err_diff := Int.neg_neg _ + rw [h1, h2] + +/-! ## UnionAll + +List concatenation. Multiplicities of duplicate rows add via +downstream consolidation. -/ + +def unionAll (a b : Stream) : Stream := a ++ b + +theorem unionAll_nil_left (s : Stream) : unionAll [] s = s := rfl + +theorem unionAll_nil_right (s : Stream) : unionAll s [] = s := + List.append_nil s + +theorem unionAll_assoc (a b c : Stream) : + unionAll (unionAll a b) c = unionAll a (unionAll b c) := + List.append_assoc a b c + +/-! ## Cross product + +Multiplicative combine: `(rL, dL, eL) × (rR, dR, eR) = +(rL ++ rR, dL·dR, dL·eR + eL·dR + eL·eR)`. The err-side combinator +captures valid×err, err×valid, and err×err contributions. -/ + +@[inline] def crossOne (recL recR : StreamRecord) : StreamRecord := + { row := recL.row ++ recR.row + , diff := recL.diff * recR.diff + , err_diff := recL.diff * recR.err_diff + + recL.err_diff * recR.diff + + recL.err_diff * recR.err_diff } + +def cross (l r : Stream) : Stream := + l.flatMap fun recL => r.map (crossOne recL) + +theorem cross_nil_left (r : Stream) : cross [] r = [] := rfl + +theorem cross_nil_right (l : Stream) : cross l [] = [] := by + induction l with + | nil => rfl + | cons _ tl ih => + show List.flatMap _ (_ :: tl) = [] + rw [List.flatMap_cons] + show List.map _ [] ++ List.flatMap _ tl = [] + rw [List.map_nil, List.nil_append] + exact ih + +theorem cross_append_left (a b r : Stream) : + cross (a ++ b) r = cross a r ++ cross b r := by + show (a ++ b).flatMap _ = a.flatMap _ ++ b.flatMap _ + exact List.flatMap_append + +end Stream + +end Mz diff --git a/doc/developer/semantics/Mz/Strict.lean b/doc/developer/semantics/Mz/Strict.lean new file mode 100644 index 0000000000000..3bb9596819a21 --- /dev/null +++ b/doc/developer/semantics/Mz/Strict.lean @@ -0,0 +1,319 @@ +import Mz.PrimEval + +/-! +# Strict propagation + +A scalar function is *err-strict in position k* when supplying `.err` +at that position forces the output to be the same `.err`, regardless +of the other arguments. This is the cell-scoped analogue of +PostgreSQL's `STRICT` qualifier on `NULL`: in the four-valued lattice +of this skeleton, `err` plays the role `NULL` plays in PostgreSQL for +strict functions. + +The boolean fragment exposes exactly one fully strict function +(`evalNot`) and one position-strict function (`evalIfThen`, strict +only in its condition). `evalAnd` and `evalOr` are *not* err-strict in +either position because `FALSE`/`TRUE` short-circuit absorbs the other +operand, including `err`. The corresponding negative results are +stated below; they ensure that the spec does not silently regress to +an "errors > everything" model. + +`NULL`-strictness is captured by a separate predicate. The two +strictness flavors agree for most arithmetic / comparison operators +but disagree for `AND`, `OR`, `IfThen`, and `COALESCE`, which the +spec singles out for special treatment. +-/ + +namespace Mz + +/-! ## Strictness predicates -/ + +/-- `f` is err-strict: an `err` argument forces an `err` output with +the same payload. -/ +def ErrStrictUnary (f : Datum → Datum) : Prop := + ∀ e, f (.err e) = .err e + +/-- `f` is err-strict in each argument position. The two positions +have independent witnesses; a function strict only in its left +argument is captured by `.left` alone. + +This is the *payload-preserving* form: an `err` argument propagates +the *same* payload to the output. The boolean fragment's `evalNot` +satisfies it. Arithmetic operators do not satisfy `right` literally +because `evalPlus (.err e₁) (.err e₂) = .err e₁`, not `.err e₂`. See +`ErrPropagatingBinary` for the strictly weaker form that arithmetic +satisfies. -/ +structure ErrStrictBinary (f : Datum → Datum → Datum) : Prop where + left : ∀ d e, f (.err e) d = .err e + right : ∀ d e, f d (.err e) = .err e + +/-- `f` is err-propagating: an `err` in either argument forces an +`err` output, but the output payload may depend on which input came +first. The four-valued lattice's `err`-absorbs-`null`-absorbs-`int` +ordering means arithmetic operators satisfy this weaker form even +though they break the payload-preserving `ErrStrictBinary`. -/ +structure ErrPropagatingBinary (f : Datum → Datum → Datum) : Prop where + left : ∀ d₁ d₂, d₁.IsErr → (f d₁ d₂).IsErr + right : ∀ d₁ d₂, d₂.IsErr → (f d₁ d₂).IsErr + +/-- `f` is null-strict: a `null` argument forces a `null` output. -/ +def NullStrictUnary (f : Datum → Datum) : Prop := + f .null = .null + +/-- `f` is null-propagating in each position, provided the *other* +argument is not `.err`. The guard is necessary in the four-valued +lattice: `evalPlus .null (.err e) = .err e`, so the unguarded form +"`.null` in either position forces `.null`" would fail. The guard +captures the standard SQL/Materialize rule: in the absence of an +absorbing `err`, a `null` operand makes the result `null`. -/ +structure NullPropagatingBinary (f : Datum → Datum → Datum) : Prop where + left : ∀ d, ¬d.IsErr → f .null d = .null + right : ∀ d, ¬d.IsErr → f d .null = .null + +/-! ## Concrete instances on the boolean fragment -/ + +theorem evalNot_errStrict : ErrStrictUnary evalNot := fun _ => rfl + +theorem evalNot_nullStrict : NullStrictUnary evalNot := rfl + +/-- The condition slot of `IfThen` is err-strict: an `err` condition +forces an `err` output, with the same payload, no matter what the +branches contain. The branch slots are *not* err-strict: when the +condition selects the other branch, the error in the unselected +branch has no effect on the output. -/ +theorem evalIfThen_errStrict_condition (e : EvalError) (dt de : Datum) : + evalIfThen (.err e) dt de = .err e := rfl + +/-! ## Closure under composition + +If both `f` and `g` are err-strict, so is `f ∘ g`. This is the +property an optimizer uses when it fuses a chain of strict scalar +functions into a single MFP expression: strict-in-strict is strict. -/ + +theorem ErrStrictUnary.comp {f g : Datum → Datum} + (hf : ErrStrictUnary f) (hg : ErrStrictUnary g) : + ErrStrictUnary (f ∘ g) := by + intro e + show f (g (.err e)) = .err e + rw [hg e, hf e] + +/-! ## Arithmetic instances + +`evalPlus`, `evalMinus`, `evalTimes`, and `evalDivide` propagate `err` +in both positions and `null` in both positions (when the other +operand is not itself `err`). The four-valued lattice is in force: +`err > null > int`. These instances are the cell-scoped analogue of +SQL's "STRICT in NULL" qualifier, lifted to a setting where `err` +takes the dominant role. -/ + +theorem evalPlus_errPropagating : ErrPropagatingBinary evalPlus where + left := by + intro d₁ d₂ h + match d₁, h with + | .err e, _ => + show (evalPlus (.err e) d₂).IsErr + simp [evalPlus, Datum.IsErr] + right := by + intro d₁ d₂ h + match d₂, h with + | .err e, _ => cases d₁ <;> simp [evalPlus, Datum.IsErr] + +theorem evalPlus_nullPropagating : NullPropagatingBinary evalPlus where + left := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + right := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + +theorem evalMinus_errPropagating : ErrPropagatingBinary evalMinus where + left := by + intro d₁ d₂ h + match d₁, h with + | .err e, _ => + show (evalMinus (.err e) d₂).IsErr + simp [evalMinus, Datum.IsErr] + right := by + intro d₁ d₂ h + match d₂, h with + | .err e, _ => cases d₁ <;> simp [evalMinus, Datum.IsErr] + +theorem evalMinus_nullPropagating : NullPropagatingBinary evalMinus where + left := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + right := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + +theorem evalTimes_errPropagating : ErrPropagatingBinary evalTimes where + left := by + intro d₁ d₂ h + match d₁, h with + | .err e, _ => + show (evalTimes (.err e) d₂).IsErr + simp [evalTimes, Datum.IsErr] + right := by + intro d₁ d₂ h + match d₂, h with + | .err e, _ => cases d₁ <;> simp [evalTimes, Datum.IsErr] + +theorem evalTimes_nullPropagating : NullPropagatingBinary evalTimes where + left := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + right := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + +/-- `evalDivide` propagates `err` from either side. The output may be +`.err .divisionByZero` rather than the input payload when the divisor +is `.int 0`, but the input err always wins when present. -/ +theorem evalDivide_errPropagating : ErrPropagatingBinary evalDivide where + left := by + intro d₁ d₂ h + match d₁, h with + | .err e, _ => + show (evalDivide (.err e) d₂).IsErr + simp [evalDivide, Datum.IsErr] + right := by + intro d₁ d₂ h + match d₂, h with + | .err e, _ => cases d₁ <;> simp [evalDivide, Datum.IsErr] + +theorem evalDivide_nullPropagating : NullPropagatingBinary evalDivide where + left := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + right := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + +/-! ## Comparison instances + +`evalEq` and `evalLt` mirror the arithmetic operators in their +propagation behavior: err-strict in both positions, null-strict in +both positions (when the other side is not err). The output is +always `.bool`, `.null`, or `.err`, so the operators chain cleanly +into the boolean-logic fragment. -/ + +theorem evalEq_errPropagating : ErrPropagatingBinary evalEq where + left := by + intro d₁ d₂ h + match d₁, h with + | .err e, _ => + show (evalEq (.err e) d₂).IsErr + simp [evalEq, Datum.IsErr] + right := by + intro d₁ d₂ h + match d₂, h with + | .err e, _ => cases d₁ <;> simp [evalEq, Datum.IsErr] + +theorem evalEq_nullPropagating : NullPropagatingBinary evalEq where + left := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + right := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + +theorem evalLt_errPropagating : ErrPropagatingBinary evalLt where + left := by + intro d₁ d₂ h + match d₁, h with + | .err e, _ => + show (evalLt (.err e) d₂).IsErr + simp [evalLt, Datum.IsErr] + right := by + intro d₁ d₂ h + match d₂, h with + | .err e, _ => cases d₁ <;> simp [evalLt, Datum.IsErr] + +theorem evalLt_nullPropagating : NullPropagatingBinary evalLt where + left := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + right := by + intro d h + cases d with + | bool b => rfl + | int n => rfl + | null => rfl + | err e => exact absurd (by simp [Datum.IsErr] : (Datum.err e).IsErr) h + +/-! ## Negative results + +`AND` and `OR` are not err-strict in either position. The short +counterexamples below also serve as canonical regression tests: a +future change to `evalAnd` that accidentally promotes +`FALSE AND ERROR` to `ERROR` would break exactly these proofs. -/ + +theorem evalAnd_not_errStrict_left : + ¬ ∀ d e, evalAnd (.err e) d = .err e := by + intro h + have hh := h (.bool false) .divisionByZero + simp [evalAnd] at hh + +theorem evalAnd_not_errStrict_right : + ¬ ∀ d e, evalAnd d (.err e) = .err e := by + intro h + have hh := h (.bool false) .divisionByZero + simp [evalAnd] at hh + +theorem evalOr_not_errStrict_left : + ¬ ∀ d e, evalOr (.err e) d = .err e := by + intro h + have hh := h (.bool true) .divisionByZero + simp [evalOr] at hh + +theorem evalOr_not_errStrict_right : + ¬ ∀ d e, evalOr d (.err e) = .err e := by + intro h + have hh := h (.bool true) .divisionByZero + simp [evalOr] at hh + +end Mz diff --git a/doc/developer/semantics/Mz/Variadic.lean b/doc/developer/semantics/Mz/Variadic.lean new file mode 100644 index 0000000000000..16efd03fed341 --- /dev/null +++ b/doc/developer/semantics/Mz/Variadic.lean @@ -0,0 +1,125 @@ +import Mz.PrimEval +import Mz.Laws + +/-! +# Variadic `AND` and `OR` + +`MirScalarExpr::VariadicFunc::And` and `Or` take an arbitrary number +of operands. This file proves laws about the corresponding +`List Datum → Datum` evaluators (`evalAndN`, `evalOrN`) defined in +`Mz/PrimEval.lean`, and shows that the binary `evalAnd` / `evalOr` +are the two-operand specializations of the variadic forms. + +The variadic forms are defined by right-fold so the cons recurrence +holds by `rfl`. With a left-fold the recurrence would require a +separate associativity argument; the right-fold gives the same final +value because `TRUE`/`FALSE` are two-sided identities for +`evalAnd`/`evalOr` (see `Mz/Laws.lean`). + +A key spec property of `MirScalarExpr` `And`/`Or` is that `FALSE` +(resp. `TRUE`) absorbs every other operand including `err`. Lifted +to the variadic form: if `FALSE` appears anywhere in the list, +`evalAndN` is `FALSE`. The corresponding `evalOrN` theorem holds for +`TRUE`. These absorption theorems justify the runtime's short-circuit +optimization and are what an optimizer cites when it folds +`x AND false` to `false` regardless of `x`'s side effects (which in +this skeleton are limited to producing `err`s). +-/ + +namespace Mz + +/-! ## Cons recurrence -/ + +theorem evalAndN_cons (d : Datum) (ds : List Datum) : + evalAndN (d :: ds) = evalAnd d (evalAndN ds) := rfl + +theorem evalOrN_cons (d : Datum) (ds : List Datum) : + evalOrN (d :: ds) = evalOr d (evalOrN ds) := rfl + +/-! ## Identity cases -/ + +theorem evalAndN_nil : evalAndN [] = .bool true := rfl +theorem evalOrN_nil : evalOrN [] = .bool false := rfl + +theorem evalAndN_singleton (d : Datum) : evalAndN [d] = d := by + show evalAnd d (.bool true) = d + exact evalAnd_true_right d + +theorem evalOrN_singleton (d : Datum) : evalOrN [d] = d := by + show evalOr d (.bool false) = d + exact evalOr_false_right d + +/-! ## Binary equivalence + +The two-operand variadic forms agree with the binary evaluators. +This is the bridge that lets every binary theorem in +`Mz/Boolean.lean` and `Mz/Laws.lean` carry over to the variadic +operators on lists of length two. -/ + +theorem evalAndN_binary (a b : Datum) : + evalAndN [a, b] = evalAnd a b := by + show evalAnd a (evalAnd b (.bool true)) = evalAnd a b + rw [evalAnd_true_right] + +theorem evalOrN_binary (a b : Datum) : + evalOrN [a, b] = evalOr a b := by + show evalOr a (evalOr b (.bool false)) = evalOr a b + rw [evalOr_false_right] + +/-! ## Absorption + +A single `FALSE` anywhere in the operand list collapses `evalAndN` to +`FALSE`. Symmetric statement for `TRUE` and `evalOrN`. The induction +is on the operand list, using the cons recurrence and the fact that +`evalAnd` returns `FALSE` whenever its right argument is `FALSE`. -/ + +private theorem evalAnd_false_right_any (d : Datum) : + evalAnd d (.bool false) = .bool false := by + cases d with + | bool b => cases b <;> rfl + | int _ => rfl + | null => rfl + | err _ => rfl + +private theorem evalOr_true_right_any (d : Datum) : + evalOr d (.bool true) = .bool true := by + cases d with + | bool b => cases b <;> rfl + | int _ => rfl + | null => rfl + | err _ => rfl + +theorem evalAndN_false_absorbs : + ∀ {ds : List Datum}, Datum.bool false ∈ ds → evalAndN ds = .bool false := by + intro ds hmem + induction ds with + | nil => cases hmem + | cons hd tl ih => + cases hmem with + | head _ => + -- `hd` was unified with `.bool false`. Cons recurrence reduces. + show evalAnd (.bool false) (evalAndN tl) = .bool false + rfl + | tail _ hmem' => + have htl : evalAndN tl = .bool false := ih hmem' + show evalAnd hd (evalAndN tl) = .bool false + rw [htl] + exact evalAnd_false_right_any hd + +theorem evalOrN_true_absorbs : + ∀ {ds : List Datum}, Datum.bool true ∈ ds → evalOrN ds = .bool true := by + intro ds hmem + induction ds with + | nil => cases hmem + | cons hd tl ih => + cases hmem with + | head _ => + show evalOr (.bool true) (evalOrN tl) = .bool true + rfl + | tail _ hmem' => + have htl : evalOrN tl = .bool true := ih hmem' + show evalOr hd (evalOrN tl) = .bool true + rw [htl] + exact evalOr_true_right_any hd + +end Mz diff --git a/doc/developer/semantics/README.md b/doc/developer/semantics/README.md new file mode 100644 index 0000000000000..c524e74ad45a6 --- /dev/null +++ b/doc/developer/semantics/README.md @@ -0,0 +1,144 @@ +# Lean 4 semantics skeleton + +A mechanized model of Materialize's scalar evaluation semantics. + +This directory contains the v1 skeleton accompanying the error-handling design document at `../design/20260517_error_handling_semantics.md`. +The goal of the skeleton is not to mechanize all of `MirScalarExpr`. +The goal is to lock in the boolean truth tables for `AND` and `OR` over the four-valued logic `{TRUE, FALSE, NULL, ERROR}` and provide a place to grow from. + +## What is here + +* `Mz/Datum.lean`: `Datum` (`.bool`, `.int`, `.null`, `.err`), `EvalError` (`.placeholder`, `.divisionByZero`), and the `Datum.IsErr` predicate. +* `Mz/Expr.lean`: `Expr` inductive — literals, columns, binary `and`/`or`, `not`, `ifThen`, the list-carrying constructors `andN`, `orN`, `coalesce`, the binary integer arithmetic constructors `plus`, `minus`, `times`, `divide`, and the binary comparison constructors `eq`, `lt`. +* `Mz/PrimEval.lean`: primitive evaluators on `Datum` and `List Datum` — `evalAnd`, `evalOr`, `evalNot`, `evalIfThen`, `Env`, `Env.get`, `evalAndN`, `evalOrN`, `evalCoalesce`, the integer arithmetic primitives `evalPlus`, `evalMinus`, `evalTimes`, `evalDivide`, and the comparison primitives `evalEq`, `evalLt`. Split out so the algebraic-law files and the expression-level evaluator can both import them without circular dependencies. Division strict on `.err` and `.null`; a `.int n / .int 0` divisor produces `.err .divisionByZero` — the canonical cell-scoped error. Comparison is err-strict and null-strict; mixed-type operands route to `.null` (the skeleton does not model SQL implicit casts). +* `Mz/Eval.lean`: the big-step `eval : Env → Expr → Datum`. List-carrying constructors evaluate each operand and hand the result list to the matching primitive. +* `Mz/Boolean.lean`: per-cell truth-table proofs for `AND`, `OR`, and `NOT`, plus involutivity of `NOT`. +* `Mz/MightError.lean`: the `Expr.might_error` static analyzer, the `Env.ErrFree` predicate, and the `might_error_sound` theorem. Binary `AND` / `OR` short-circuit on literal-`.bool false` / literal-`.bool true` operands via `Expr.isLitBoolFalse` / `Expr.isLitBoolTrue`: either position being the absorbing literal makes the analyzer return `false` regardless of the other operand. The same short-circuit fires on variadic `andN` / `orN` when any operand is the absorbing literal. `IfThen` likewise short-circuits when the condition is a literal `.bool` — only the picked branch's analyzer result is consulted, so a known-erring branch on the discarded side cannot taint the result. + `.divide a b` reduces to `a.might_error` when `b` is a literal nonzero int (`Expr.divisorIsSafe`) — the divisor cannot trigger divide-by-zero, so the operator inherits errors only from the dividend. Falls back to `true` when the divisor is unknown or a literal zero. `andN` and `orN` recurse via `Expr.argsMightError` ("any operand might error"); `coalesce` recurses via `Expr.argsAllMightError` ("every operand might error"), special-casing the empty list as safe. Soundness for `coalesce` extracts a statically-safe operand through `Expr.exists_safe_of_not_argsAllMightError` and applies `evalCoalesce_not_err_of_some_safe`, which in turn rests on `Coalesce.go_not_err` — the state-machine lemma that "once one safe operand is in the remaining list, the walk cannot return an error". Companion value-level helpers `evalAnd_{left,right}_false` / `evalOr_{left,right}_true` discharge the short-circuit branches of soundness. +* `Mz/Strict.lean`: strictness predicates — payload-preserving (`ErrStrictUnary`, `ErrStrictBinary`, `NullStrictUnary`) and weaker propagation forms (`ErrPropagatingBinary`, `NullPropagatingBinary`) that match the four-valued lattice's `err > null > int` absorption order. Positive instances for `evalNot` and the condition slot of `evalIfThen`; closure under composition; arithmetic instances (`evalPlus`, `evalMinus`, `evalTimes`, `evalDivide` all err-propagating and null-propagating in both positions); comparison instances (`evalEq`, `evalLt` same); negative results witnessing that `AND` and `OR` are *not* err-strict in either position. +* `Mz/Coalesce.lean`: laws for `evalCoalesce` — error-rescue, null-beats-err tiebreak, first-error stickiness. +* `Mz/Laws.lean`: algebraic laws — two-sided identity (`TRUE` for `AND`, `FALSE` for `OR`), idempotence (unconditional), commutativity (conditional on error-freedom of operands), and `Expr`-level reorder safety as a corollary of soundness. +* `Mz/Variadic.lean`: laws for `evalAndN` and `evalOrN` over `List Datum` — cons recurrence, nil, singleton, binary equivalence with the binary evaluators, and `FALSE`/`TRUE` absorption. +* `Mz/ExprVariadic.lean`: `Expr`-level reduction lemmas connecting `eval env (.andN args)` / `.orN` / `.coalesce` to their primitive counterparts, identity / singleton / binary-equivalence corollaries lifted through `eval`, and variadic-absorption theorems — a single operand evaluating to `FALSE` (resp. `TRUE`) makes the whole `andN` (resp. `orN`) evaluate to `FALSE` (resp. `TRUE`). +* `Mz/Bag.lean`: bag semantics on `List Row`. Defines `filterRel` and `project`, with filter idempotence, filter commutativity, projection length-preservation, and the empty-projection equation. Plain `filterRel` silently drops `err` rows; `Mz/ErrStream.lean` adds the explicit data/error stream pair. +* `Mz/ErrStream.lean`: the dataflow-style `BagStream = (data, errors)` pair. + `BagStream.filter` routes erroring rows into the error collection instead of dropping them, with idempotence proved at both the data and the error level. + `BagStream.filter_comm_data` proves the data-side commutativity unconditionally; `BagStream.filter_comm_no_err` strengthens to full stream equality when neither predicate errors on the input data. + `BagStream.project_filter_pushdown_data` lifts `filterRel_pushdown_project` to the data side of `BagStream`: filtering after projecting agrees with substituting through the projection and filtering before projecting. Holds unconditionally on the data field; the errors collection diverges between the two orderings (filter sees projected vs unprojected rows) and is out of scope for this theorem. + `BagStream.project` projects each row through a list of scalars; a row stays in the data collection only when every scalar succeeds, otherwise its err payloads (one per erroring scalar) are appended to the error collection. + `rowErrs_nil_of_all_safe` and `projectErrs_eq_nil_of_all_safe` show that when no projection errs, `BagStream.project` does not extend the error collection. +* `Mz/Pushdown.lean`: substitution (`Expr.subst`) plus the headline `eval_subst` theorem (substituting then evaluating against the original row equals evaluating against the projected row), and the relational predicate-pushdown rewrite `filterRel p (project es rel) = project es (filterRel (p.subst es) rel)`. +* `Mz/ColRefs.lean`: column-reference analyzer and rewriter. + `Expr.colReferencesBoundedBy n e` returns `true` when every `col i` in `e` has `i < n`. Mutually defined with `Expr.argsColRefBoundedBy` so structural recursion handles the nested-list constructors. Headline theorem `eval_append_left_of_bounded`: when a predicate's column references are bounded by `l.length`, evaluating against `l ++ r` agrees with evaluating against `l` alone — the foundation for pushing a single-side filter through a join's `cross` (where the joined env is `l ++ r`). + `Expr.colShift k e` adds `k` to every column reference, leaving other constructors structurally intact. Right-side analogue of the bounded analyzer: it realigns a predicate written against the right schema with the joined env `l ++ r` (where the right side starts at index `l.length`). Headline `eval_append_right_shift`: `eval (l ++ r) (e.colShift l.length) = eval r e`. + `Expr.colReferencesBoundedBy_mono` (mutual with `Expr.argsColRefBoundedBy_mono`) lifts a tight bound to a coarser one — useful when a predicate's natural bound is a single relation's width but the proof site needs the joined-env width. Convenience `eval_append_left_of_bounded_at` removes the requirement that the predicate's bound match `l.length` exactly: any `n ≤ l.length` suffices. + `Expr.colShift_zero` (identity at `k = 0`) and `Expr.colShift_add` (`(e.colShift k).colShift m = e.colShift (k + m)`) give the shift its monoid laws. Useful for nested joins where each layer adds its own offset to the predicate's column references. + `Expr.colReferencesUnused n e` (mutual with `Expr.argsColRefUnused`) returns `true` when `e` never reads column `n`. Companion `Env.replaceAt env n v` swaps a single position. Headline `eval_replaceAt_of_unused`: when column `n` is unused, replacing its value does not change eval. Supports column-pruning rewrites: a projection that drops unused columns is sound. Supporting `Env.get_replaceAt_eq` and `Env.get_replaceAt_ne` discharge the per-column reductions. + `Expr.colReferencesUnused_of_bounded` (mutual with the operand-list version) bridges the two analyzers: a predicate bounded by `n` has every column `i ≥ n` unused. Lets the optimizer derive column-pruning consequences from a tight bound. + Supporting environment lemmas: `Env.get_append_left` (read from prefix) and `Env.get_append_right` (read from suffix with index shift). +* `Mz/DiffSemiring.lean`: `DiffWithError α` — the diff-field type extension that encodes global (collection-scoped) errors as an absorbing element. Provides `+`, `*`, `-`, `0`, `1`, `min` instances over an arbitrary base diff and proves the absorption / commutativity / associativity / distributivity / negation / min laws that downstream operators must respect. Negation laws (`neg_error`, `neg_val`, `neg_neg_val`, `val_add_neg_val`, `neg_mul`, `mul_neg`, `neg_add`) carry the principle that `.error` is unrecoverable — a collection-scoped error cannot be subtracted away, and that negation distributes through addition and multiplication. Min laws (`error_min_left`, `error_min_right`, `min_val_val`) define the bag-min combinator with `.error` absorbing. The `_int` specializations discharge the base hypotheses at `Int` so downstream code in `Mz/Join.lean`, `Mz/UnifiedConsolidate.lean`, and `Mz/SetOps.lean` can cite the named laws directly. The inversion law `add_eq_error_left_or_right` is the converse of absorption — a sum equal to `.error` forces at least one summand to be `.error` — required for the reverse direction of `consolidate_error_inv`. +* `Mz/UnifiedStream.lean`: unified diff-aware alternative to `BagStream`. `UnifiedStream := List (UnifiedRow × DiffWithError Int)` pairs a carrier (data row or row-scoped err) with a differential-dataflow diff augmented by the absorbing `error` element. Row-scoped errors flow through the carrier; collection-scoped errors flow through diff multiplication / addition. `ofBag` / `split` conversions assign every bag record a diff of `.val 1`; the round-trip theorem `split (ofBag s) = s` holds. The cross-direction is exact only up to multiset equality on `List EvalError` and is lossy for diffs ≠ `.val 1` (split drops diff information). + Error-scope extractors: `errCarriers us` returns the list of row-scoped err payloads (carrier = `.err e`); `errorDiffCarriers us` returns the list of carriers whose diff is collection-scoped `.error`. Theorems: `errCarriers_nil`/`_append`, `errorDiffCarriers_nil`/`_append`. The two sets are independent observable properties — operators that touch one need not touch the other. + Bridge lemmas `mem_errCarriers` and `mem_errorDiffCarriers` convert membership in the extractor lists to record-level carrier / diff membership in the stream, letting downstream proofs reason without unfolding the underlying `filterMap`. + Per-operator error-scope behavior: `filter_errorDiffCarriers` (filter preserves the collection-err set exactly) and `filter_errCarriers_mono` (filter is monotone on row-errs — cell-to-row promotion only adds carriers). Same pair for `project`: `project_errorDiffCarriers` (equality) and `project_errCarriers_mono` (monotone). filter and project are the two cell-to-row promotion sites. + `escalateRowErrs us` is the explicit row-to-collection promotion operator: every `(.err e, _)` record's diff is overwritten to `.error`; `.row r` records untouched. Theorems: `escalateRowErrs_length` (length-preserving), `escalateRowErrs_idem` (idempotent), `escalateRowErrs_errCarriers` (row-err set preserved), `escalateRowErrs_errCarriers_in_errorDiff` (every input row-err appears in the output collection-err set — the observable promotion property). + `UnifiedStream.project` lifts `BagStream.project` to the diff-aware carrier. Records with `.error` diff or `.err` carrier pass through unchanged; a `.row r` record with `.val n` diff is evaluated against `es` — if every scalar succeeds, the row is emitted with diff `.val n`; if any scalar errs, one `(.err e, .val n)` is emitted per erroring scalar (each preserving the original multiplicity). Theorems: `project_preserves_error_diff` (an `.error` diff in the input always reaches the output), `project_no_error` (all-`.val` inputs yield all-`.val` outputs), `project_nil_es` (empty projection list collapses every row to width-zero), `project_nil_stream` (empty stream is empty). +* `Mz/Aggregate.lean`: aggregate reductions over `List Datum`. `aggCountNonNull` for `COUNT(expr)`. `aggStrict` for `SUM`/`MIN`/`MAX`-style aggregates that propagate `err` (first one in scan order wins) and skip `NULL`s. `aggTry` for the proposed `try_sum`/`try_min`/`try_max` variants that swallow `err` into `NULL` instead of propagating, defined as a post-pass on `aggStrict`. Theorems: `aggStrict_err` (any `err` input → `err` output), `aggStrict_no_err` (no-err inputs + no-err reducer → no-err output), `aggTry_no_err` (the non-strict variant never errors), and `aggTry_eq_aggStrict_of_no_err` (strict and non-strict agree on error-free inputs). +* `Mz/Consolidate.lean`: per-key diff summation over `List (DiffWithError α)`. The headline `sumAll_eq_error_of_mem` proves that an `error` diff anywhere in the list absorbs the consolidated sum to `error`, which is the property a differential dataflow `compact` operator cites when propagating global errors through consolidation. Companion `sumAll_val_of_all_val` says an all-`val` list sums to `val` of some base value. +* `Mz/TimedConsolidate.lean`: per-`(row, time)` consolidation. `TimedUnifiedStream := List (UnifiedRow × Nat × DiffWithError Int)` carries records with time. `atTime t` projects to one time slice (dropping the time component); `consolidateAtTime t` chains it with `UnifiedStream.consolidate`. Theorems: `consolidateAtTime_preserves_error` (an `.error` diff at time `t` survives both filter and consolidation), `atTime_length_le` and `consolidateAtTime_length_le` (both non-expanding). Decomposes the joint key into "filter by time, then consolidate by row". + `advanceFrontier f s` advances every record's time to `Nat.max time f` — the differential-dataflow `advance` operator on a scalar frontier. Records originally at time `< f` move to `f`; records at `≥ f` stay. Theorems: `advanceFrontier_nil`, `advanceFrontier_length` (length preserved), `advanceFrontier_zero` (zero frontier is identity), `advanceFrontier_idem` (idempotent on equal frontier), `advanceFrontier_advanceFrontier` (composing by `f` then `g` equals advancing by `Nat.max f g`). Real differential dataflow uses antichains of times; the scalar form is sufficient to state the algebraic laws. + Timed error-scope lift: `TimedUnifiedStream.errCarriers` and `TimedUnifiedStream.errorDiffCarriers` extract the row-err and collection-err sets from a timed stream (ignoring the time component). Reductions: `errCarriers_nil`/`_append`, `errorDiffCarriers_nil`/`_append`. Per-operator: `advanceFrontier_errCarriers` and `advanceFrontier_errorDiffCarriers` (exact — frontier advance only changes times, not carriers/diffs); `atTime_errCarriers_subset` and `atTime_errorDiffCarriers_subset` (errors at slice time `t` are a subset of input errors — time-slice projection loses non-`t` records); `consolidateAtTime_errCarriers_subset` and `consolidateAtTime_errorDiffCarriers_subset` (composition of `atTime` subset with `consolidate` iff). +* `Mz/UnifiedConsolidate.lean`: row-keyed diff summation on `UnifiedStream`. `UnifiedStream.consolidate` buckets records by carrier (via `DecidableEq UnifiedRow`) and sums per-bucket diffs. Theorems cover three properties: + *absorption* — `consolidate_preserves_error` proves an `.error` diff anywhere in the input gives an `.error` diff in the consolidated output for that carrier; + *cardinality* — `consolidate_length_le` bounds the output by the input length (consolidation only merges, never expands); + *no-error preservation* — `consolidate_no_error` proves that if every input diff is a `.val`, every output diff is a `.val`, so `.error` is the only source of absorption. + *strict shrinkage* — `consolidate_strict_length_dup` proves that two adjacent records sharing a carrier compress to one in the output: `(consolidate ((uc, d) :: (uc, d') :: rest)).length ≤ rest.length + 1`, strictly less than the input's `rest.length + 2`. + *carrier uniqueness* — `consolidate_noDup` proves that `consolidate` always produces a `NoDupCarriers` list (`Pairwise` on first-component inequality). Each carrier appears at most once. Supporting `consolidateInto_preserves_noDup` (and a `_general` variant that handles both fresh-key and matching-key cases) carries the invariant through single-step inserts. + *carrier preservation* — `mem_consolidate_of_mem` (forward) and `mem_of_mem_consolidate` (reverse): every input carrier appears in the output, and every output carrier came from an input. The set of carriers is preserved exactly under consolidation (multiplicity may collapse). + *error inversion* — `consolidate_error_inv` (with helper `consolidateInto_error_inv` and DiffSemiring's `add_eq_error_left_or_right`): a `.error` diff in the output must come from a `.error` diff in the input at the same carrier. The reverse of `consolidate_preserves_error`; closes the loop for `consolidate_errorDiffCarriers_iff` (defined here, alongside `consolidate_errCarriers_iff`, so `Mz/TimedConsolidate.lean` can cite them). +* `Mz/Triple.lean`: collection-wide and per-time *flat* consolidation views on `TimedUnifiedStream`. `consolidateAll` sums every diff in the stream; `consolidateAtTimeFlat t` sums every diff at time `t`. Both ignore the carrier — they collapse a time slice (or the whole stream) to one `DiffWithError Int`. Absorption: `consolidateAll_eq_error_of_mem` and `consolidateAtTimeFlat_eq_error_of_mem`. Complementary to `Mz/TimedConsolidate.lean`'s `consolidateAtTime t`, which buckets per `(row, time)` and returns a `UnifiedStream`. +* `Mz/Join.lean`: relational joins on the diff-aware `UnifiedStream`. `cross` is the cartesian product — carriers combine via `combineCarrier` (rows concatenate; err on either side wins, left first), diffs multiply through `DiffWithError`'s `Mul` instance. A `.error` diff on either input therefore absorbs to `.error` on the output via `DiffWithError.error_mul_{left,right}`. `join pred l r` filters the product through a join predicate. Theorems: `cross_length` (`l.length * r.length`), `filter_length_le` (filter is non-expanding), `join_length_le` (corollary). Diff-propagation theorems: `cross_diff_error_{left,right}` (a `.error` diff on either side propagates through every output record), `filter_preserves_error_diff` (a record carrying `.error` diff is never dropped by `filter` — the absorbing marker cannot be filtered away). No-error preservation: `cross_no_error` and `filter_no_error` prove that all-`.val` input diffs yield all-`.val` output diffs, so `.error` is the only source of absorbing diffs in the joint output. Algebraic laws: `combineCarrier_assoc` (carrier combine is associative modulo `List.append_assoc`) and the headline `UnifiedStream.cross_assoc` (`(a × b) × c = a × (b × c)`). The proof rearranges nested `flatMap` / `map` via local list-monad lemmas and closes via `DiffWithError.mul_assoc` plus `combineCarrier_assoc`. + Error-scope propagation through `cross`: `mem_cross_of_mems` is the carrier-level witness — every input pair contributes one output record. `cross_errCarriers_from_left` (left `.err e` paired with any right record yields `.err e` in output via combineCarrier's left-wins rule); `cross_errCarriers_from_right` (right `.err e` paired with a left `.row la` yields `.err e` — right propagates only when left is `.row`); `cross_errorDiffCarriers_from_{left,right}` (`.error` diff on either side absorbs through the product). cross grows both error scopes multiplicatively in the cardinality of the opposite input. +* `Mz/SetOps.lean`: set operations on `UnifiedStream`. `unionAll = (++)` concatenates two streams record-wise; theorems cover length (sum), associativity, nil identities, and error / no-error preservation from each input (`unionAll_preserves_error_diff_left`, `unionAll_preserves_error_diff_right`, `unionAll_no_error`). `union = consolidate ∘ unionAll` derives the set-semantics flavor; theorems lift the consolidation guarantees to `union` (`union_length_le`, `union_preserves_error_diff_left`, `union_preserves_error_diff_right`, `union_no_error`, `union_nil_left`, `union_nil_right`). + `negate` negates every diff (`.error` absorbs negation, `.val n` becomes `.val (-n)`). Theorems: `negate_length` (length preserved), `negate_negate` (involution), `negate_preserves_error_diff`, `negate_no_error`. + `exceptAll l r = consolidate (unionAll l (negate r))` realizes the signed-diff `EXCEPT ALL` (output diffs may be negative, encoding "this carrier has `n` fewer copies in the result than in the input"). Theorems: `exceptAll_length_le` (≤ sum of input lengths), `exceptAll_preserves_error_diff_left`/`exceptAll_preserves_error_diff_right` (errors from either side survive — negation absorbs at `.error`), `exceptAll_no_error`, `exceptAll_nil_left` (`exceptAll [] r = negate (consolidate r)` — bridges to `negate_consolidate`), `exceptAll_nil_right` (`exceptAll l [] = consolidate l`). + `clampPositive` drops records with `.val n` where `n ≤ 0`, keeping `.error` records and records with `.val n > 0`. Theorems: `clampPositive_length_le`, `clampPositive_preserves_error_diff`, `clampPositive_only_positive` (every output `.val` is strictly positive), `clampPositive_no_error`, `clampPositive_idem` (idempotent — filter twice = filter once). + `bagExceptAll = clampPositive ∘ exceptAll` realizes the bag-semantics `EXCEPT ALL` — the signed-diff result is post-processed to drop non-positive multiplicities, producing `max(L - R, 0)` per carrier. Theorems lift the signed flavor: `bagExceptAll_length_le`, `bagExceptAll_preserves_error_diff_left`/`_right`, `bagExceptAll_only_positive`, `bagExceptAll_no_error`. + `clampToOne` collapses surviving multiplicities to one: `.val n > 0` becomes `.val 1`, non-positive `.val` is dropped, `.error` survives. Defined by structural recursion on the list. Theorems: `clampToOne_length_le`, `clampToOne_preserves_error_diff`, `clampToOne_no_error`, `clampToOne_only_one_or_error` (every output diff is `.val 1` or `.error`), `clampToOne_idem` (idempotent — after one pass every `.val` is `.val 1` so a second pass is a no-op). + `distinct = clampToOne ∘ consolidate` realizes SQL `DISTINCT`: each distinct carrier appears at most once with multiplicity one (or `.error` if a collection-scoped error existed). Theorems: `distinct_length_le`, `distinct_preserves_error_diff`, `distinct_only_one_or_error`, `distinct_no_error`. + Distributivity over `unionAll`: `filter_unionAll`, `cross_unionAll_left`, `project_unionAll`, `negate_unionAll`. Each follows from `List.flatMap_append` / `List.map_append` — `flatMap`- and `map`-based operators distribute over concatenation. Lets the optimizer pull a `UNION ALL` tail out of a pipeline and plan per-branch. + `cross_negate_left` proves that negating the left input of a cross product equals negating the cross output: the diff-semiring law `(-a) * b = -(a * b)` (`DiffWithError.neg_mul_int`) carries the proof since `combineCarrier` is unchanged by negation and only the diff arithmetic flips. + `negate_consolidate` proves that negation commutes with consolidation: `negate (consolidate us) = consolidate (negate us)`. The proof recurses via `negate_consolidateInto` (private), which lifts the same property to the single-step insertion. Negation is additive (`neg_add`), so it slides through per-bucket sums. + `intersectAll l r` realizes bag-intersection via lookup: consolidate both inputs, then per left-carrier emit `(uc, min(L_diff, R_diff))` if the carrier exists in the right's consolidate, else drop. Supported by `UnifiedStream.lookup` (return the diff for a carrier in a consolidated stream, or `none`), `UnifiedStream.lookup_isSome_of_mem` (lookup returns `some` when carrier present), `UnifiedStream.mem_of_lookup_eq_some` (converse: lookup success witnesses membership), `UnifiedStream.lookup_eq_of_mem_noDup` (returns the exact diff when the list has unique carriers), and `DiffWithError.min` (the bag-min combinator with `.error` absorbing). Theorems: `intersectAll_length_le` (≤ left.length), `intersectAll_preserves_error_diff_left`/`_right` (`.error` diff for a carrier present in both inputs survives — left case uses left-min absorption, right case uses the no-dup property of `consolidate r`), `intersectAll_no_error` (all-`.val` inputs yield all-`.val` outputs). + `bagIntersectAll = clampPositive ∘ intersectAll` realizes the bag-semantics `INTERSECT ALL` — drops records with non-positive multiplicity, leaving `.error` records untouched. Theorems lift the signed flavor: `bagIntersectAll_length_le`, `bagIntersectAll_preserves_error_diff_left`/`_right`, `bagIntersectAll_no_error`, `bagIntersectAll_only_positive`. + Error-scope characterization of set ops. `unionAll_errCarriers` and `unionAll_errorDiffCarriers` (concat — direct from `errCarriers_append` / `errorDiffCarriers_append`). `negate_errCarriers` and `negate_errorDiffCarriers` (both scopes are invariants of negation since carriers are unchanged and `.error` absorbs negation). Set-level invariance of `consolidate` lives in `Mz/UnifiedConsolidate.lean` (`consolidate_errCarriers_iff`, `consolidate_errorDiffCarriers_iff`) so `Mz/TimedConsolidate.lean` can cite it; `Mz/SetOps.lean` keeps the forward `consolidate_errorDiffCarriers_mono` corollary for symmetry with other set ops. `union_errCarriers_iff` / `union_errorDiffCarriers_iff` and `exceptAll_errCarriers_iff` / `exceptAll_errorDiffCarriers_iff` follow as compositions of `unionAll`, `negate`, and `consolidate` theorems — the error-scope sets of both ops are the disjoint union of the inputs'. `join_errorDiffCarriers` (equals that of `cross`) and `join_errCarriers_mono` (filter is monotone on row-errs over `cross`) compose `cross` and `filter` results. + Clamp / clamp-distinct error-scope. `clampPositive_errorDiffCarriers_iff` and `clampToOne_errorDiffCarriers_iff` are full equivalences — `.error` records always pass through the clamps. Row-err has only the reverse direction: `clampPositive_errCarriers_of_mem` and `clampToOne_errCarriers_of_mem`, because the clamps may drop `(.err e, .val 0)` or `(.err e, .val (-n))` records. Compositions: `distinct_errorDiffCarriers_iff` / `distinct_errCarriers_of_mem` (distinct = clampToOne ∘ consolidate), `bagExceptAll_errorDiffCarriers_iff` / `bagExceptAll_errCarriers_of_mem` (clampPositive ∘ exceptAll). For `intersectAll`, only the reverse direction is available — `intersectAll_errCarriers_of_mem` (an err in the output came from BOTH inputs) and `intersectAll_errorDiffCarriers_of_mem` (a collection-err carrier in the output exists with some diff in both inputs); composed with clamps to give `bagIntersectAll_errCarriers_of_mem`. + `negate` commutes with `filter`: `negate_filter` proves `negate (filter pred us) = filter pred (negate us)` unconditionally. Filter's row arm depends only on `eval r pred`, which is independent of the diff sign, so the negation slides through. Useful for optimizer rewrites that commute negation with filter (EXCEPT ALL paths, retraction reordering). +* `Mz/JoinPushdown.lean`: filter pushdown for cross products. The optimizer's canonical rewrite — `filter pred (cross l r) = cross (filter pred l) r` — when the predicate references only left-input columns. Headline theorem `UnifiedStream.filter_cross_pushdown_left` takes the column bound `pred.colReferencesBoundedBy N = true`, the per-row width invariant `∀ ud ∈ l, ∀ la, ud.1 = .row la → la.length ≥ N`, and the `IsPureData` predicate on `r` (no `.err` carriers, no `.error` diffs). The pure-data hypothesis is essential: without it, `combineCarrier`'s left-wins rule disagrees with filter's cell-to-row promotion on err attribution, and `.error` diff in `r` interacts with filter's first arm to keep records that would be dropped post-pushdown. Auxiliary reduction `UnifiedStream.cross_singleton` flattens `cross [(uc, d)] r` to a per-record map (carrier/diff split to avoid `.fst`/`.snd` projection issues under induction). Per-record helpers handle each left-record shape (`.error` diff, `.err` carrier, `.row` with eval keep/err/drop); main theorem assembles them via structural induction on `l` plus `eval_append_left_of_bounded`. +* `Mz/GroupBy.lean`: two grouping primitives. + `groupBy keyExpr rel` partitions a relation by evaluated key using Lean's derived `DecidableEq Datum` — two `Datum.err e` keys with the same payload collapse into one group. + `groupByErrDistinct keyExpr rel` uses the spec-faithful `Datum.groupKeyEq`, which returns `false` whenever either side is `.err`, so every err key produces its own singleton group. + Theorem `insertIntoDistinct_err` proves the err-key insertion always appends a fresh group; `groupByErrDistinct_length_of_all_err` derives the consequence — every err-keyed row contributes one output group. + Headline cardinality `totalRows_groupBy` (and its err-distinct variant `totalRows_groupByErrDistinct`) state that the sum of group sizes equals the input relation's length — no row is lost or duplicated by partitioning. + Agreement theorem `groupByErrDistinct_eq_groupBy_of_no_err` proves the two variants coincide when no row's key evaluates to `.err`. Supporting invariants `insertInto_preserves_non_err_keys` and `groupBy_keys_non_err` thread the "no err keys in the accumulator" property through the foldr. + Companion `aggregateBy` / `aggregateByErrDistinct` run `aggStrict` per group, modeling `SELECT keyExpr, AGG(valExpr) ... GROUP BY keyExpr`. + +## What is not here + +* No bag semantics, joins, aggregates, or relational operators. +* No bridge to the Rust evaluator. + The model and the runtime are independent; divergences are caught by review, not by tooling. +* No Mathlib dependency. + The skeleton is pure core Lean 4 to keep build time small and bootstrap simple. + +## Build + +``` +cd doc/developer/semantics +lake build +``` + +Toolchain is pinned in `lean-toolchain`. +CI uses the local `Dockerfile` in this directory, which installs elan and reads the same pin via the `LEAN_TOOLCHAIN` build arg. +The elan toolchain used by local developers and the toolchain baked into the CI image therefore stay in lockstep. +Buildkite runs `ci/test/lean-semantics.sh` on every PR that touches `doc/developer/semantics/` (see the `lean-semantics` step in `ci/test/pipeline.template.yml`). + +To reproduce the CI build locally: + +``` +./ci/test/lean-semantics.sh +``` + +To run `lake build` directly outside Docker, install elan via the standard instructions at `https://lean-lang.org/` and run `lake build` in this directory. + +## Workflow + +When a semantic rule changes, the change must land in two places. + +1. Update `Mz/Eval.lean` to reflect the new operational behavior. +2. Update the corresponding theorem in `Mz/Boolean.lean` (or add a new one). + +A semantic change without a Lean diff is incomplete. +A Lean diff without a corresponding Rust diff in `src/expr/` is a spec change that has not yet shipped. +Reviewers should expect both sides of the change in the same PR. + +## Next steps + +The diff-semiring extension is in scope: `UnifiedStream` records carry `(UnifiedRow × DiffWithError Int)` and `filter`, `cross`, `join`, `consolidate`, `consolidateAtTime` preserve / multiply / absorb the diff per the semiring laws. + +### Blocked + +* Full `BagStream.filter` commutativity (no preconditions). The error field requires a notion of multiset equality on `List EvalError`, and even multiset equality fails when both predicates err on the same row — `(p err, q err)` rows record different err payloads depending on filter order. The data side is closed by `filter_comm_data`; the precondition variant by `filter_comm_no_err`. +* Errors-side `BagStream.project` / `BagStream.filter` pushdown. The two orderings collect predicate errors from different row sets; even multiset equality fails when `rowAllSafe` filtering removes rows the predicate would have visited. The data side is closed by `project_filter_pushdown_data`. + +### Additive refinements + +* Tightening `Expr.might_error` further. Short-circuit detection covers binary / variadic `AND` / `OR` and `IfThen` against literal absorbers. Remaining: ground-truth lookups (literal arithmetic, known-null operands, type-driven), all additive against the current soundness proof. +* General `k > 1` strict cardinality bound for `UnifiedConsolidate`. Today's `consolidate_strict_length_dup` covers the case of two adjacent duplicates compressing to one bucket; lifting to "any `k` occurrences of the same carrier shrink the output by `k - 1`" needs a counting-multiplicity argument. +* `UnifiedStream.project` pushdown analogue of `BagStream.project_filter_pushdown_data`. Predicate pushdown across the diff-aware projection is straightforward on the carrier side but the err-split adds asymmetries: filter-after-project sees projected rows; filter-before-project (with substitution) sees originals. +* Lift `ErrPropagatingBinary` / `NullPropagatingBinary` to `Expr` form. Today's predicates work at the `Datum` level; an `Expr.err_propagating` analogue would let the optimizer reason about whole sub-expressions, not just primitives. + +### Material expansions + +* `distinct` idempotence (`distinct ∘ distinct = distinct`) as multiset equality. Consolidate may reorder distinct carriers, so list-equality idempotence is false; needs multiset machinery on `List (UnifiedRow × DiffWithError Int)`. +* Cross-link the spec doc (`../design/20260517_error_handling_semantics.md`) to specific theorem names via `[Mz/...:thm]` cross-references. diff --git a/doc/developer/semantics/lake-manifest.json b/doc/developer/semantics/lake-manifest.json new file mode 100644 index 0000000000000..08f9ce69b1e10 --- /dev/null +++ b/doc/developer/semantics/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "«mz-semantics»", + "lakeDir": ".lake"} diff --git a/doc/developer/semantics/lakefile.lean b/doc/developer/semantics/lakefile.lean new file mode 100644 index 0000000000000..9df38b0726e1e --- /dev/null +++ b/doc/developer/semantics/lakefile.lean @@ -0,0 +1,9 @@ +import Lake +open Lake DSL + +package «mz-semantics» where + -- No options needed yet. + +@[default_target] +lean_lib «Mz» where + -- Library auto-discovers files under `Mz/`. diff --git a/doc/developer/semantics/lean-toolchain b/doc/developer/semantics/lean-toolchain new file mode 100644 index 0000000000000..33e0c088939ad --- /dev/null +++ b/doc/developer/semantics/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.29.1 diff --git a/doc/developer/semantics/transforms.md b/doc/developer/semantics/transforms.md new file mode 100644 index 0000000000000..72fb8335d4b1b --- /dev/null +++ b/doc/developer/semantics/transforms.md @@ -0,0 +1,416 @@ +# Transform catalog + +Mechanized equational and inclusion laws for `UnifiedStream` / `TimedUnifiedStream` operators. +Grouped by algebraic shape so optimizer rewrites have a single index. + +Each entry links theorem name to source file. +`L = R` denotes equality, `L ⊆ R` denotes one-direction membership (forward), `L = R ↔ P` denotes a logical iff over membership. + +## Append / unionAll distribution + +Operators that distribute over concatenation. +Each is direct from `List.flatMap_append` or `List.map_append` on the underlying carrier. + +| Theorem | Statement | File | +| --- | --- | --- | +| `unionAll_assoc` | `(a ⊎ b) ⊎ c = a ⊎ (b ⊎ c)` | `Mz/SetOps.lean` | +| `filter_unionAll` | `filter p (a ⊎ b) = filter p a ⊎ filter p b` | `Mz/SetOps.lean` | +| `project_unionAll` | `project es (a ⊎ b) = project es a ⊎ project es b` | `Mz/SetOps.lean` | +| `negate_unionAll` | `negate (a ⊎ b) = negate a ⊎ negate b` | `Mz/SetOps.lean` | +| `cross_unionAll_left` | `cross (a ⊎ b) r = cross a r ⊎ cross b r` | `Mz/SetOps.lean` | +| `filter_append` | `filter p (a ++ b) = filter p a ++ filter p b` | `Mz/UnifiedStream.lean` | +| `project_append` | `project es (a ++ b) = project es a ++ project es b` | `Mz/UnifiedStream.lean` | +| `negate_append` | `negate (a ++ b) = negate a ++ negate b` | `Mz/SetOps.lean` | +| `cross_append_left` | `cross (a ++ b) r = cross a r ++ cross b r` | `Mz/Join.lean` | +| `errCarriers_append` | `errCarriers (a ++ b) = errCarriers a ++ errCarriers b` | `Mz/UnifiedStream.lean` | +| `errorDiffCarriers_append` | symmetric for collection-err | `Mz/UnifiedStream.lean` | +| `unionAll_errCarriers` | corollary | `Mz/SetOps.lean` | +| `unionAll_errorDiffCarriers` | corollary | `Mz/SetOps.lean` | +| `TimedUnifiedStream.errCarriers_append` | timed lift | `Mz/TimedConsolidate.lean` | +| `TimedUnifiedStream.errorDiffCarriers_append` | timed lift | `Mz/TimedConsolidate.lean` | + +## Commutativity / sliding through + +Two operators commute as `f ∘ g = g ∘ f`. + +| Theorem | Statement | File | +| --- | --- | --- | +| `negate_filter` | `negate (filter p us) = filter p (negate us)` | `Mz/SetOps.lean` | +| `negate_project` | `negate (project es us) = project es (negate us)` | `Mz/SetOps.lean` | +| `negate_consolidate` | `negate (consolidate us) = consolidate (negate us)` | `Mz/SetOps.lean` | +| `negate_consolidateInto` (private) | step lemma for above | `Mz/SetOps.lean` | + +## Pushdown + +Rewrites that move an outer operator inside a join or product. + +| Theorem | Statement | File | +| --- | --- | --- | +| `filter_cross_pushdown_left` | `filter p (cross l r) = cross (filter p l) r` when `p` bounded by left widths and `r` `IsPureData` | `Mz/JoinPushdown.lean` | + +## Bilinearity (cross with negate) + +Negation slides through cross from either side. + +| Theorem | Statement | File | +| --- | --- | --- | +| `cross_negate_left` | `cross (negate l) r = negate (cross l r)` via `(-a) * b = -(a * b)` | `Mz/SetOps.lean` | +| `cross_negate_right` | `cross l (negate r) = negate (cross l r)` via `a * (-b) = -(a * b)` | `Mz/SetOps.lean` | + +## Associativity + +| Theorem | Statement | File | +| --- | --- | --- | +| `cross_assoc` | `cross (cross a b) c = cross a (cross b c)` modulo carrier-append associativity | `Mz/Join.lean` | +| `unionAll_assoc` | concat associative | `Mz/SetOps.lean` | +| `combineCarrier_assoc` | carrier-side associativity for cross | `Mz/Join.lean` | + +## Involution / Idempotence + +Applying an operator twice equals once (or zero times). + +| Theorem | Statement | File | +| --- | --- | --- | +| `negate_negate` | `negate (negate us) = us` (involution) | `Mz/SetOps.lean` | +| `clampPositive_idem` | `clampPositive (clampPositive us) = clampPositive us` | `Mz/SetOps.lean` | +| `clampToOne_idem` | `clampToOne (clampToOne us) = clampToOne us` | `Mz/SetOps.lean` | +| `escalateRowErrs_idem` | `escalateRowErrs (escalateRowErrs us) = escalateRowErrs us` | `Mz/UnifiedStream.lean` | +| `advanceFrontier_idem` | `advanceFrontier f (advanceFrontier f s) = advanceFrontier f s` | `Mz/TimedConsolidate.lean` | +| `advanceFrontier_zero` | `advanceFrontier 0 s = s` (zero-frontier identity) | `Mz/TimedConsolidate.lean` | +| `advanceFrontier_advanceFrontier` | `advanceFrontier g (advanceFrontier f s) = advanceFrontier (max f g) s` | `Mz/TimedConsolidate.lean` | +| `clampPositive_clampToOne` | `clampPositive ∘ clampToOne = clampToOne` | `Mz/SetOps.lean` | + +## Length / cardinality + +Bounds on output cardinality. `_length` is equality, `_length_le` is upper bound. + +| Theorem | Statement | File | +| --- | --- | --- | +| `unionAll_length` | `|a ⊎ b| = |a| + |b|` | `Mz/SetOps.lean` | +| `negate_length` | `|negate us| = |us|` | `Mz/SetOps.lean` | +| `cross_length` | `|cross l r| = |l| * |r|` | `Mz/Join.lean` | +| `filter_length_le` | filter non-expanding | `Mz/Join.lean` | +| `join_length_le` | `|join p l r| ≤ |l| * |r|` | `Mz/Join.lean` | +| `union_length_le` | bound via consolidate | `Mz/SetOps.lean` | +| `exceptAll_length_le` | `≤ |l| + |r|` | `Mz/SetOps.lean` | +| `clampPositive_length_le` | non-expanding | `Mz/SetOps.lean` | +| `clampToOne_length_le` | non-expanding | `Mz/SetOps.lean` | +| `distinct_length_le` | non-expanding | `Mz/SetOps.lean` | +| `intersectAll_length_le` | `≤ |l|` | `Mz/SetOps.lean` | +| `bagExceptAll_length_le` | composed bound | `Mz/SetOps.lean` | +| `bagIntersectAll_length_le` | composed bound | `Mz/SetOps.lean` | +| `consolidate_length_le` | merging never expands | `Mz/UnifiedConsolidate.lean` | +| `consolidate_strict_length_dup` | strict shrink on adjacent duplicate | `Mz/UnifiedConsolidate.lean` | +| `escalateRowErrs_length` | length-preserving | `Mz/UnifiedStream.lean` | +| `advanceFrontier_length` | length-preserving | `Mz/TimedConsolidate.lean` | +| `atTime_length_le` | non-expanding | `Mz/TimedConsolidate.lean` | +| `consolidateAtTime_length_le` | non-expanding | `Mz/TimedConsolidate.lean` | + +## Trivial cases + +Reductions on empty / singleton inputs. + +| Theorem | Statement | File | +| --- | --- | --- | +| `*_nil` | operator applied to `[]` returns `[]` | various | +| `filter_nil`, `project_nil_stream`, `cross_nil_left`, `cross_nil_right`, `negate_nil` (implicit), `consolidate_nil`, `errCarriers_nil`, `errorDiffCarriers_nil`, `clampToOne_nil`, `escalateRowErrs_nil`, `advanceFrontier_nil`, `atTime_nil`, `consolidateAtTime_nil`, `consolidateInto_nil`, `unionAll_nil_left`, `unionAll_nil_right`, `union_nil_left`, `union_nil_right`, `bagExceptAll_nil_left`, `bagExceptAll_nil_right`, `exceptAll_nil_left`, `exceptAll_nil_right`, `lookup_nil` | | various | +| `consolidate_singleton` | `consolidate [(uc, d)] = [(uc, d)]` | `Mz/UnifiedConsolidate.lean` | +| `cross_singleton` | `cross [(uc, d)] r = r.map (combineCarrier uc rd.1, d * rd.2)` | `Mz/JoinPushdown.lean` | +| `project_nil_es` | empty projection list collapses rows | `Mz/UnifiedStream.lean` | + +## Cons / step reductions + +Named per-shape reductions of recursive operators. + +| Theorem | Statement | File | +| --- | --- | --- | +| `cross_cons_left` | cross unfolding on `(hd :: tl)` left | `Mz/Join.lean` | +| `consolidateInto_match` | matching head folds into bucket | `Mz/UnifiedConsolidate.lean` | +| `consolidateInto_skip` | non-matching head recurses | `Mz/UnifiedConsolidate.lean` | +| `consolidateInto_nil` | trivial | `Mz/UnifiedConsolidate.lean` | + +## Error-scope: row-err (`errCarriers`) + +Set of row-scoped error payloads (carrier = `.err e`). +Iff = preserved exactly as set. Mono = forward inclusion only (one direction). `_of_mem` = reverse inclusion only. + +| Theorem | Direction | File | +| --- | --- | --- | +| `unionAll_errCarriers` | `=` concat | `Mz/SetOps.lean` | +| `negate_errCarriers` | `=` | `Mz/SetOps.lean` | +| `consolidate_errCarriers_iff` | `↔` (set) | `Mz/UnifiedConsolidate.lean` | +| `union_errCarriers_iff` | disjoint union | `Mz/SetOps.lean` | +| `exceptAll_errCarriers_iff` | disjoint union | `Mz/SetOps.lean` | +| `filter_errCarriers_mono` | mono (cell→row promotion adds) | `Mz/SetOps.lean` | +| `project_errCarriers_mono` | mono (scalar errs add) | `Mz/UnifiedStream.lean` | +| `cross_errCarriers_from_left` | mono propagation | `Mz/Join.lean` | +| `cross_errCarriers_from_right` | mono propagation (left = `.row`) | `Mz/Join.lean` | +| `join_errCarriers_mono` | mono (filter of cross) | `Mz/SetOps.lean` | +| `clampPositive_errCarriers_of_mem` | reverse (clamps drop) | `Mz/SetOps.lean` | +| `clampToOne_errCarriers_of_mem` | reverse | `Mz/SetOps.lean` | +| `distinct_errCarriers_of_mem` | reverse | `Mz/SetOps.lean` | +| `bagExceptAll_errCarriers_of_mem` | reverse | `Mz/SetOps.lean` | +| `intersectAll_errCarriers_of_mem` | reverse (and: in both) | `Mz/SetOps.lean` | +| `bagIntersectAll_errCarriers_of_mem` | reverse (and: in both) | `Mz/SetOps.lean` | +| `escalateRowErrs_errCarriers` | `=` (carriers untouched) | `Mz/UnifiedStream.lean` | +| `TimedUnifiedStream.advanceFrontier_errCarriers` | `=` (time-only op) | `Mz/TimedConsolidate.lean` | +| `TimedUnifiedStream.atTime_errCarriers_subset` | reverse (slice drops) | `Mz/TimedConsolidate.lean` | +| `TimedUnifiedStream.consolidateAtTime_errCarriers_subset` | reverse | `Mz/TimedConsolidate.lean` | + +## Error-scope: collection-err (`errorDiffCarriers`) + +Carriers whose diff is `.error`. + +| Theorem | Direction | File | +| --- | --- | --- | +| `unionAll_errorDiffCarriers` | `=` concat | `Mz/SetOps.lean` | +| `negate_errorDiffCarriers` | `=` | `Mz/SetOps.lean` | +| `consolidate_errorDiffCarriers_iff` | `↔` exact | `Mz/UnifiedConsolidate.lean` | +| `consolidate_errorDiffCarriers_mono` | forward (corollary) | `Mz/SetOps.lean` | +| `union_errorDiffCarriers_iff` | disjoint union | `Mz/SetOps.lean` | +| `exceptAll_errorDiffCarriers_iff` | disjoint union | `Mz/SetOps.lean` | +| `filter_errorDiffCarriers` | `=` (.error passes through) | `Mz/SetOps.lean` | +| `project_errorDiffCarriers` | `=` | `Mz/UnifiedStream.lean` | +| `cross_errorDiffCarriers_from_left` | forward propagation | `Mz/Join.lean` | +| `cross_errorDiffCarriers_from_right` | forward propagation | `Mz/Join.lean` | +| `join_errorDiffCarriers` | `=` (= cross) | `Mz/SetOps.lean` | +| `clampPositive_errorDiffCarriers_iff` | `↔` exact | `Mz/SetOps.lean` | +| `clampToOne_errorDiffCarriers_iff` | `↔` exact | `Mz/SetOps.lean` | +| `distinct_errorDiffCarriers_iff` | `↔` exact | `Mz/SetOps.lean` | +| `bagExceptAll_errorDiffCarriers_iff` | disjoint union | `Mz/SetOps.lean` | +| `intersectAll_errorDiffCarriers_of_mem` | reverse (in both) | `Mz/SetOps.lean` | +| `escalateRowErrs_errCarriers_in_errorDiff` | forward (promotion) | `Mz/UnifiedStream.lean` | +| `TimedUnifiedStream.advanceFrontier_errorDiffCarriers` | `=` | `Mz/TimedConsolidate.lean` | +| `TimedUnifiedStream.atTime_errorDiffCarriers_subset` | reverse | `Mz/TimedConsolidate.lean` | +| `TimedUnifiedStream.consolidateAtTime_errorDiffCarriers_subset` | reverse | `Mz/TimedConsolidate.lean` | + +## Error-diff record-level absorption (forward) + +`.error` diff survives the operator on the same carrier. + +| Theorem | File | +| --- | --- | +| `consolidate_preserves_error` | `Mz/UnifiedConsolidate.lean` | +| `project_preserves_error_diff` | `Mz/UnifiedStream.lean` | +| `filter_preserves_error_diff` | `Mz/Join.lean` | +| `cross_diff_error_left` / `cross_diff_error_right` | `Mz/Join.lean` | +| `unionAll_preserves_error_diff_left` / `_right` | `Mz/SetOps.lean` | +| `union_preserves_error_diff_left` / `_right` | `Mz/SetOps.lean` | +| `exceptAll_preserves_error_diff_left` / `_right` | `Mz/SetOps.lean` | +| `intersectAll_preserves_error_diff_left` / `_right` | `Mz/SetOps.lean` | +| `bagExceptAll_preserves_error_diff_left` / `_right` | `Mz/SetOps.lean` | +| `bagIntersectAll_preserves_error_diff_left` / `_right` | `Mz/SetOps.lean` | +| `clampPositive_preserves_error_diff` | `Mz/SetOps.lean` | +| `clampToOne_preserves_error_diff` | `Mz/SetOps.lean` | +| `distinct_preserves_error_diff` | `Mz/SetOps.lean` | +| `negate_preserves_error_diff` | `Mz/SetOps.lean` | +| `TimedUnifiedStream.consolidateAtTime_preserves_error` | `Mz/TimedConsolidate.lean` | + +## Error-diff inversion (reverse) + +If output has `.error`, input had `.error` at that carrier. + +| Theorem | File | +| --- | --- | +| `consolidate_error_inv` | `Mz/UnifiedConsolidate.lean` | +| `consolidateInto_error_inv` (private) | `Mz/UnifiedConsolidate.lean` | + +## No-error preservation + +All-`.val` inputs yield all-`.val` outputs (collection-err free). + +| Theorem | File | +| --- | --- | +| `filter_no_error` | `Mz/Join.lean` | +| `project_no_error` | `Mz/UnifiedStream.lean` | +| `cross_no_error` | `Mz/Join.lean` | +| `consolidate_no_error` | `Mz/UnifiedConsolidate.lean` | +| `negate_no_error` | `Mz/SetOps.lean` | +| `unionAll_no_error` | `Mz/SetOps.lean` | +| `union_no_error` | `Mz/SetOps.lean` | +| `exceptAll_no_error` | `Mz/SetOps.lean` | +| `intersectAll_no_error` | `Mz/SetOps.lean` | +| `clampPositive_no_error` | `Mz/SetOps.lean` | +| `clampToOne_no_error` | `Mz/SetOps.lean` | +| `distinct_no_error` | `Mz/SetOps.lean` | +| `bagExceptAll_no_error` | `Mz/SetOps.lean` | +| `bagIntersectAll_no_error` | `Mz/SetOps.lean` | + +## Multiplicity / shape constraints + +| Theorem | Statement | File | +| --- | --- | --- | +| `clampPositive_only_positive` | output `.val` is strictly positive | `Mz/SetOps.lean` | +| `clampToOne_only_one_or_error` | output diff is `.val 1` or `.error` | `Mz/SetOps.lean` | +| `bagExceptAll_only_positive` | composed | `Mz/SetOps.lean` | +| `bagIntersectAll_only_positive` | composed | `Mz/SetOps.lean` | +| `distinct_only_one_or_error` | composed | `Mz/SetOps.lean` | + +## Carrier uniqueness (NoDup) + +| Theorem | File | +| --- | --- | +| `NoDupCarriers.nil` | `Mz/UnifiedConsolidate.lean` | +| `consolidate_noDup` | `Mz/UnifiedConsolidate.lean` | +| `union_noDup` | `Mz/SetOps.lean` | +| `exceptAll_noDup` | `Mz/SetOps.lean` | +| `bagExceptAll_noDup` | `Mz/SetOps.lean` | +| `intersectAll_noDup` | `Mz/SetOps.lean` | +| `bagIntersectAll_noDup` | `Mz/SetOps.lean` | +| `distinct_noDup` | `Mz/SetOps.lean` | +| `clampPositive_noDup` | `Mz/SetOps.lean` | +| `clampToOne_noDup` | `Mz/SetOps.lean` | +| `negate_noDup` | `Mz/SetOps.lean` | + +## Membership bridges + +Convert extractor / structural membership. + +| Theorem | File | +| --- | --- | +| `mem_errCarriers` | `Mz/UnifiedStream.lean` | +| `mem_errorDiffCarriers` | `Mz/UnifiedStream.lean` | +| `mem_consolidate_of_mem` | forward carrier preservation | `Mz/UnifiedConsolidate.lean` | +| `mem_of_mem_consolidate` | reverse | `Mz/UnifiedConsolidate.lean` | +| `mem_cross_of_mems` | pair-membership in cross | `Mz/Join.lean` | +| `lookup_isSome_of_mem` | lookup characterization | `Mz/SetOps.lean` | +| `mem_of_lookup_eq_some` | lookup converse | `Mz/SetOps.lean` | +| `lookup_eq_of_mem_noDup` | exact diff under NoDup | `Mz/SetOps.lean` | +| `TimedUnifiedStream.mem_atTime_of_mem` | timed lift | `Mz/TimedConsolidate.lean` | + +## Round-trip / iff + +Combine forward and reverse direction. + +| Theorem | File | +| --- | --- | +| `split_ofBag` | `BagStream` round-trip | `Mz/UnifiedStream.lean` | +| `split_data_ofBag`, `split_errors_ofBag` | components | `Mz/UnifiedStream.lean` | +| `TimedUnifiedStream.consolidateAll_eq_error_iff` | flat absorption | `Mz/Triple.lean` | +| `TimedUnifiedStream.consolidateAll_eq_error_iff_errorDiffCarriers` | extractor bridge | `Mz/Triple.lean` | +| `TimedUnifiedStream.consolidateAtTimeFlat_eq_error_iff` | per-time | `Mz/Triple.lean` | +| `TimedUnifiedStream.consolidateAll_error_inv` | reverse half | `Mz/Triple.lean` | +| `TimedUnifiedStream.consolidateAtTimeFlat_error_inv` | reverse half | `Mz/Triple.lean` | + +## DiffWithError underlying laws + +The semiring layer that operator proofs cite. + +| Theorem | File | +| --- | --- | +| `error_add_left` / `error_add_right` | `Mz/DiffSemiring.lean` | +| `error_mul_left` / `error_mul_right` | `Mz/DiffSemiring.lean` | +| `error_min_left` / `error_min_right` | `Mz/DiffSemiring.lean` | +| `add_eq_error_left_or_right` | inversion | `Mz/DiffSemiring.lean` | +| `neg_error`, `neg_val`, `neg_neg_val` | negation laws | `Mz/DiffSemiring.lean` | +| `val_add_neg_val` | self-cancellation | `Mz/DiffSemiring.lean` | +| `neg_mul`, `mul_neg`, `neg_add` | distributive negation | `Mz/DiffSemiring.lean` | +| `min_val_val` | min on `.val` | `Mz/DiffSemiring.lean` | +| `mul_add`, `mul_assoc`, `mul_comm` | semiring laws | `Mz/DiffSemiring.lean` | +| `add_comm`, `add_assoc`, `zero_add_val`, `val_add_zero` | additive laws | `Mz/DiffSemiring.lean` | +| `*_int` specializations | base hypotheses discharged at `Int` | `Mz/DiffSemiring.lean` | +| `sumAll_eq_error_of_mem` | forward absorption | `Mz/Consolidate.lean` | +| `sumAll_error_inv` | reverse inversion | `Mz/Consolidate.lean` | +| `sumAll_val_of_all_val` | all-`.val` total | `Mz/Consolidate.lean` | + +## Column-reference analyzers + +Static analyses used by pushdown. + +| Theorem | File | +| --- | --- | +| `colReferencesBoundedBy_mono` | bound is monotone | `Mz/ColRefs.lean` | +| `eval_append_left_of_bounded` | eval-on-left agreement | `Mz/ColRefs.lean` | +| `eval_append_right_shift` | shifted eval on right | `Mz/ColRefs.lean` | +| `colShift` monoid laws | various | `Mz/ColRefs.lean` | + +## Materialize optimizer passes → Lean coverage + +The Rust optimizer in `src/transform/` has 66 passes (41 algebraic rewrites, 13 analyses, 11 stateful planning steps, 1 framework). +This section maps each pass to its status in the Lean spec. + +Status legend: + +* **Modeled** — equivalent theorem (or strong proxy) shipped here. +* **Modelable** — current `UnifiedStream` / `DiffWithError` infra is enough; just write the theorem. +* **Infra gap** — needs a new operator (`Reduce`, `TopK`, `FlatMap`, …) or a new analysis (equivalence classes, monotonicity, column lattice). +* **Out of scope** — physical planning, syntactic plumbing, or user-facing metadata; no place in a denotational spec. + +### Algebraic rewrites — modeled + +| Rust pass | Lean correspondent | +| --- | --- | +| `predicate_pushdown.rs` | `filter_cross_pushdown_left` + `filter_cross_pushdown_right` (bilateral; bound / `colShift` and pure-data hypotheses) | +| `compound/union.rs` (UnionNegateFusion) | `negate_unionAll` + `unionAll_assoc` | +| `fusion/union.rs` (Union fusion) | `unionAll_assoc` + nil identities | +| `fusion/negate.rs` (Negate fusion) | `negate_negate` (involution) | +| `fusion/join.rs` (Join fusion / associativity) | `cross_assoc` | +| `union_cancel.rs` (partial) | `consolidate (unionAll a (negate a))` reduces to `.val 0` records via diff arithmetic; no theorem yet, but ingredients in place | +| `fusion/filter.rs` (filter ∘ filter) | `UnifiedStream.filter_filter_fuse` in `Mz/FilterFusion.lean` plus `filter_idem` (unconditional) and `filter_comm` (under err-freedom). | +| `threshold_elision.rs` | `UnifiedStream.clampPositive_id_of_positive` in `Mz/SetOps.lean`. `clampPositive` is identity when every record's diff is `.error` or a strictly-positive `.val`. | +| `fusion/map.rs` (project ∘ project) | `UnifiedStream.project_project_fuse` in `Mz/ProjectFusion.lean`. Holds under `projsAllSafe` (`es` is safe on every data row). Bridges via `eval_subst`. | +| `demand.rs` | `filter_replaceAtRow_of_unused` (any input) + `project_replaceAtRow_eq_of_unused` (under `IsPureData`) in `Mz/Demand.lean`. Lifts `eval_replaceAt_of_unused` to the stream level. | + +### Algebraic rewrites — modelable (worth shipping) + +| Rust pass | Lean approach | +| --- | --- | +| `fusion/project.rs` / `movement/projection_lifting.rs` / `projection_pushdown.rs` | Have `project_unionAll` + `filter_project_pushdown` (in `Mz/ProjectFusion.lean`). Still need `project_cross_pushdown` (push project through cross when columns split cleanly). | +| `redundant_join.rs` (distinct + join) | Express `distinct` + `cross` commutation when right side is already key-unique. Requires `intersectAll`-style lookup invariants we already have. | +| `semijoin_idempotence.rs` (partial) | A semijoin is `cross` + project + distinct. Idempotence via `distinct_idem` (provable; we have `clampToOne_idem`). | +| `non_null_requirements.rs` (model the strict-null laws) | We already have `evalAnd` / `evalOr` / arithmetic err-/null-strictness. State as `NullPropagatingBinary` / `ErrPropagatingBinary` instances; some exist in `Mz/Strict.lean`. Lift to `UnifiedStream.filter` to characterize when predicates drop vs promote. | +| `canonicalize_mfp.rs` | Establish a canonical form `Project ∘ Filter ∘ Map` and prove every MFP-like composition has a unique canonical equivalent. Needs Map (`UnifiedStream.project` is the analog of MapFilterProject's Project part; we don't have an MFP wrapper). | +| `equivalence_propagation.rs` (use sites only) | The *use* of equivalence is `if a = b then replace a with b`. With a proved `evalEq` characterization we can show `filter (a = b) us` preserves a row iff substituting `b` for `a` in the rest of the predicate gives the same evaluation. Substitution machinery is in `Expr.subst`. | + +### Algebraic rewrites — infra gap + +These need a new operator or analysis before they can be expressed. + +| Rust pass | Missing infra | +| --- | --- | +| `fold_constants.rs` | Constant collections at the `UnifiedStream` level. Could be a singleton `.row r, .val 1` literal stream. Would unlock evaluating constant subqueries during proof. | +| `fusion/reduce.rs`, `reduce_reduction.rs`, `reduce_elision.rs`, `reduction_pushdown.rs` | `Reduce` operator on `UnifiedStream`. Aggregate is at `Mz/Aggregate.lean` but only on `List Datum`; lift to `UnifiedStream` with group-by interface. | +| `fusion/top_k.rs`, `canonicalization/topk_elision.rs` | `TopK` operator (sort + limit-offset) on `UnifiedStream`. Needs an ordering on rows. | +| `canonicalization/flat_map_elimination.rs` | `FlatMap` (table-valued function) operator. The constant-arg elimination piece reduces to existing `cross` with a literal stream. | +| `literal_constraints.rs` | `IndexedFilter` operator (semi-join with constant collection). | +| `literal_lifting.rs` | Map-with-literal-columns recognition. Modelable once `project` distinguishes literal vs computed columns. | +| `column_knowledge.rs` | Per-column lattice (`{literal, nullable, type}`) + propagation. Would be a separate analysis file. | +| `equivalence_propagation.rs` (full pass) | Equivalence-class lattice. | +| `monotonic.rs` (top-level) and `analysis/monotonic.rs` | Logical monotonicity analysis: streams that never retract. Requires a `NoRetraction` predicate on `UnifiedStream` (`∀ rec, ∃ n ≥ 0, rec.2 = .val n` modulo `.error`). | +| `case_literal.rs`, `coalesce_case.rs` | Scalar `Expr` rewrites; we model `Expr` semantics but no rewrite-rule infrastructure. Easy to add as `eval`-equivalence theorems but currently unused. | + +### Out of scope (intentional) + +| Rust pass | Reason | +| --- | --- | +| `join_implementation.rs`, `will_distinct.rs`, `dataflow.rs`, `ordering.rs`, `normalize_lets.rs`, `normalize_ops.rs` | Physical planning, downstream-info-driven, or syntactic canonicalization. The denotational spec is invariant under these. | +| `cse/anf.rs`, `cse/relation_cse.rs` | Common-subexpression / ANF transformations are pure syntactic. The spec treats `MirRelationExpr` modulo CSE by definition. | +| `collect_notices.rs`, `notice/*.rs` | User-facing diagnostics; not part of the semantics. | +| `typecheck.rs` | Type preservation across passes. Our spec is intrinsically typed (Lean's type system), so this property holds by construction. | +| `analysis.rs` | Analysis framework (trait infrastructure). Lean uses theorems directly; no analogue. | +| `canonicalization/projection_extraction.rs` | Identifies projections hiding inside `Map` / `Reduce`. Syntactic, no semantic content. | + +### Priority recommendations + +If a single pass should be modeled next, the highest-value candidates by API consumption density: + +1. **`semijoin_idempotence.rs`** — distinct + cross + project commutation; uses `clampToOne_idem` already in `Mz/SetOps.lean`. +2. **`non_null_requirements.rs`** — lift `Strict.lean` propagation classes to `UnifiedStream.filter` to characterize drop vs promote. +3. **`redundant_join.rs`** — distinct + cross commutation when right side is key-unique; uses existing intersect/lookup invariants. +4. **`canonicalize_mfp.rs`** — canonical `project ∘ filter ∘ map` form. Builds on the three fusion theorems already shipped (filter, map, predicate pushdown). + +Beyond those, the cluster `{Reduce + reduce_elision + reduce_reduction + reduction_pushdown}` is the largest dependency gap. +A `UnifiedStream.reduce` operator would unlock four passes plus the GroupBy semantics already partially in `Mz/GroupBy.lean`. + +## Notes + +* `⊎` denotes `UnifiedStream.unionAll` (defined as `++` on the carrier). +* Extractors / scopes: + * `errCarriers us` — list of row-scoped `.err e` payloads. + * `errorDiffCarriers us` — list of carriers whose diff is `.error`. +* Iff vs forward vs reverse: many operators preserve the *set* of errors but not the multiset. + Forward-only theorems hold when the operator can introduce new errs (cell-to-row promotion in `filter`, `project`). + Reverse-only theorems hold when the operator can drop errs (the clamps). +* The pushdown / commutativity laws are the consumable API for an optimizer. + Length and NoDup laws are invariants needed by cost models and uniqueness reasoning. + Error-scope laws are observable-behavior guarantees for the error model.