Provenance in databases, in Lean 4
A Lean 4 formalization of database provenance in the semiring framework of
Green, Karvounarakis and Tannen: relations whose tuples are annotated with
values from a semiring, an annotated relational algebra with difference and
aggregation, the query rewriting by which
ProvSQL computes provenance inside PostgreSQL, and a
provenance semantics for a large fragment of SQL: aggregation with HAVING,
FILTER and ORDER BY, window functions, nested aggregation, lateral
subqueries and recursion.
The point of the library is to give those constructions a machine-checked semantics, so that a claim made in a paper can be followed to a theorem the Lean kernel has verified. Full API documentation: https://provsql.org/lean-docs/Provenance.html.
Papers
Sen, Maniu & Senellart, ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data, ICDE 2026 links its definitions and results into the API documentation of this library.
Such links live in a PDF and cannot be fixed after the fact, so each published
paper gets a frozen module under Provenance/Papers/, restating its claims and
proving them by applying the declarations it cites: a weakened statement breaks
the build, and the anchors are checked separately by
scripts/check-anchors.sh.
What is formalized
Everything below is proved in the library, whether or not it supports a
published paper. lake build is the test suite: there is no separate one, and
the development is sorry-free.
| Result | Module | Entry point |
|---|---|---|
m-semirings: monus from its Galois connection, the Ξ΄ support operator, homomorphisms | Provenance/SemiringWithMonus.lean | SemiringWithMonus, SemiringWithMonusHom |
fifteen concrete provenance m-semirings: πΉ, πΉ[X], Why[X], Lin[X], β[X], β, tropical, Viterbi, min-max, Εukasiewicz, interval unions, security clearances, and the three non-commutative ones of regular languages, tropical paths and best paths | Provenance/Semirings/ | one file per semiring |
annotated relational algebra with difference, and its provenance-aware rewriting into a plain query over T β K | Provenance/QueryRewriting.lean | Query.rewriting_valid |
query evaluation commutes with any m-semiring homomorphism on RAβΊ(β) β the formal counterpart of ProvSQL's compile-once/evaluate-many architecture | Provenance/QueryAnnotatedDatabaseHom.lean | Query.evaluateAnnotated_hom |
data-part adequacy of the annotated semantics against the plain one, and πΉ-support adequacy with transfer along monus homomorphisms | Provenance/QueryAdequacy.lean, Provenance/SupportAdequacy.lean | Nat.counterexample_diff_adequacy bounds it |
probabilistic query evaluation: random worlds, the possible-worlds reading of πΉ[X] annotations, categorical blocks with deterministic-OR soundness | Provenance/Probability.lean, Provenance/CategoricalBlock.lean | randomWorld_evaluateAnnotated |
| Boolean provenance circuits, read-once and deterministic-decomposable correctness, and the Tseitin CNF encoding | Provenance/Circuit.lean, Provenance/Tseitin.lean | Circuit, tseitin_equisat |
a kind-indexed general query syntax whose three column kinds (regular values, aggregate tokens, provenance values) mirror ProvSQL's regular / agg_token / uuid types, so the scope restrictions on aggregate results are static typing rather than side conditions | Provenance/AggQuery.lean | AggQueryIn |
| symbolic aggregate tokens and their semantics, invariant under permutations of tied group elements | Provenance/AggValue.lean, Provenance/AggValueCongr.lean | AggValue, AggValue.predProv_congr |
the rewriting stated natively on that syntax, the rewriting of a bare GROUP BY, the HAVING site for a predicate mixing aggregate and regular atoms, and their compositional closure over arbitrary token-bearing plans | Provenance/AggQueryRewriting.lean, Provenance/AggQueryGroupRewriting.lean, Provenance/AggQueryClosure.lean | AggQueryIn.rewritesTo_valid |
provenance of HAVING: its possible-world semantics, the algebraic identities behind counting aggregates, the corresponding probability identities under independence, a scan-computable form for MIN/MAX/PICKFIRST, and the enumeration algorithms with their correctness | Provenance/HavingSemantics.lean, Provenance/Having.lean, Provenance/HavingProbability.lean, Provenance/HavingMinMax.lean, Provenance/Algorithms/ | Having.havingProv |
complexity: non-zero HAVING SUM provenance is NP-complete in data complexity, with hardness by a first-order reduction and a size-honest encoding of concrete groups | Provenance/HavingComplexity.lean | havingSumProv_ne_zero_iff, havingSumNonzeroHow_faithful |
the SQL operators beyond grouping: window functions over SQL's frames (single- and multi-frame, percent_rank, cume_dist, ntile), aggregate expressions, FILTER and ORDER BY on aggregates, aggregation of aggregates at any depth, the lateral apply, and bag and set recursion | Provenance/AggQuery.lean, Provenance/Window.lean, Provenance/Frame.lean, Provenance/Nested.lean, Provenance/Derived.lean | AggQueryIn.evaluate |
the metatheory of that semantics: data-part adequacy, commutation with m-semiring homomorphisms, the possible-world reading over πΉ[X] and probabilistic query evaluation | Provenance/AggQueryAdequacy.lean, Provenance/AggQueryHom.lean, Provenance/AggQueryProbability.lean | AggQueryIn.evaluateAnnotated_toPlain, AggQueryIn.evaluateAnnotated_hom, AggQueryIn.boolean_pqe |
which operators a basis of the plain semantics needs: without recursion, a complete classification of the bases; with recursion, in the minimal signature (no functions on values, COUNT as the only aggregate), the same, including the necessity of window functions and the derivation of set recursion and union from bag recursion | Provenance/BasisAssembly.lean, Provenance/RecFreeBasis.lean, Provenance/RecursionBasisTheorem.lean, Provenance/RecursionBases.lean | AggQueryIn.exists_basisOps_plainEquiv, generatesOnRF_iff, basisRecOps_isBasis, generatesOnRec_iff |
the same question for the annotated semantics: a minimal basis over all commutative m-semirings, and a different minimal one, with duplicate elimination in place of set recursion, over a class of semirings that includes β, β[X], Lin[X] and those where Ξ΄ is the identity, both exactly and up to rows annotated π | Provenance/AnnotatedWhyRow.lean, Provenance/AnnotatedBasisClass.lean, Provenance/AnnotatedApproxRows.lean, Provenance/AnnotatedApplyRow.lean | annMuOps_isBasis, annEpsOps_isBasis_in_class, annEpsOps_isBasis_in_class_ren |
graded extensionality: in which m-semirings the annotation of a tuple depends on the query alone and not on its spelling, level by level β every commutative m-semiring for Fβ, the lattice m-semirings for Fβ (with EXISTS and IN), the Boolean m-semirings for Fβ (with EXCEPT and NOT EXISTS), those whose Ξ΄ is the identity for the whole recursion-free algebra; the points of a lattice m-semiring, its homomorphisms onto πΉ, separate its elements | Provenance/Extensionality.lean, Provenance/BooleanSemiring.lean, Provenance/FragQuery.lean, Provenance/FragQueryMeta.lean | extensional_level0, extensional_level1_iff, extensional_level2_iff, extensional_tame_iff, IsLatticeSemiring.eq_of_forall_point |
the same beyond one evaluator: over any semiring, every semantics that follows the clauses of semiring provenance on the positive operators, with nothing asked on negation, is extensional for Fβ only if the semiring is a Boolean algebra | Provenance/SemanticExtensionality.lean | FragQueryIn.ExtendsSemiringProvenance.isBooleanRig_of_level2, exists_semantics_extensional_iff |
Provenance/Example.lean works a full annotated-database computation end to
end, in both the classical and the kind-indexed syntax, and
Provenance/NestedExample.lean and Provenance/DistributionExample.lean do the
same for nested aggregation and for the distribution window functions. They are
built as part of the library, so their checks double as regression tests: the
kind-indexed evaluators are noncomputable (a recursion evaluates to its
fixpoint), so those checks are theorems closed by decide, and the classical
ones are #eval!s.
Layers
The library is layered, and the core ripples downward when touched:
- Algebra β
SemiringWithMonusand the concrete semirings underProvenance/Semirings/. - Data β
Database.lean(tuples, relations, plain databases) andAnnotatedDatabase.lean(the same, annotated in an m-semiringK). - Queries β
Query.lean(the classical syntax and its plain semantics),QueryAnnotatedDatabase.lean(the annotated semantics),QueryRewriting.lean(the rewriting intoT β K). - The general framework β the
AggQuery*family: the kind-indexed syntax, its evaluator, and the aggregation andHAVINGresults. This is the primary interface; the classical layer remains the proven engine several of its results reuse internally. - Metatheory of the SQL semantics β adequacy, homomorphisms, possible
worlds, and the basis theorems (
PlainBasis.lean,Decorrelate.lean,RecursionBasis.lean, theAnnotated*modules); counterexamples showing that the hypotheses are needed are inHavingQueryCounterexamples.lean. - Applications β probability, circuits, algorithms, complexity.
Releases
Version numbers are the library's own and follow
semantic versioning. There is no compatibility contract
to state: nothing depends on this library, and lean-toolchain at each tag is
authoritative for the Mathlib the tag was checked against.
What a tag is for here is freezing a citable state, one that stays reachable after the code has moved on. A citation should name a version DOI below rather than the concept DOI, so that it points at a specific state of the code.
| Tag | Toolchain | Version DOI |
|---|---|---|
v1.3.0 | leanprover/lean4:v4.35.0 | 10.5281/zenodo.23856981 |
v1.2.0 | leanprover/lean4:v4.34.0 | 10.5281/zenodo.22900284 |
v1.1.0 | leanprover/lean4:v4.33.0 | 10.5281/zenodo.21997271 |
v1.0.0 | leanprover/lean4:v4.33.0-rc1 | 10.5281/zenodo.21809152 |
main | see lean-toolchain | β |
Building
The toolchain in lean-toolchain must match the pinned Mathlib version.
lake exe cache get # fetch the Mathlib build cache
lake build # build the whole library; this is the test suite
There is no separate test suite: correctness is the Lean kernel checking the
proofs, and the library is sorry-free.
Building the documentation is a separate project, docbuild/; see its
Makefile.
Use as a dependency
Nothing is expected to depend on this library, but nothing prevents it either.
In a lakefile.lean:
require "provenance" from git
"https://github.com/PierreSenellart/provenance-lean" @ "v1.3.0"
Pin a tag or a commit rather than main, for reproducible builds. Then
import Provenance brings in everything; import individual modules to keep
build times down. Besides Mathlib, the library depends on
descriptive-complexity,
used to state the complexity results; Lake resolves one Mathlib per workspace,
so both must sit on the same pin.
The library is written for Lean's module system. Importing a module gives its
public interface: every definition (the carriers, the semirings, the query
languages and their semantics), every instance, the theorems that the
documentation names or a paper links to, and whatever their statements
mention. Definitions are exposed, so a client can unfold them, and a decide
over a concrete query evaluation reduces in a client module as it does here.
The other lemmas are private to their files and cannot be named from outside the
library; its own modules reach them with import all, which Lake permits within
one package only. A module re-exports (with public import) only what its
statements and definitions need.
One caveat: this package sets backward.isDefEq.respectTransparency false,
because its carriers (Tuple, Relation, Database, β¦) are deliberately
opaque defs that instance search must nevertheless see through. Package
options do not propagate to dependants, so a downstream project that
manipulates those carriers directly may need to set it too.
Lax archive
The formal results of the ICDE 2026 paper are registered in the Lax archive, the archive for machine-checked mathematics, as a submission whose concepts restate the library's definitions and state the paper's results, and whose proofs are the library's own, sliced to what those statements use. The submission is frozen at one commit of the library on the archive's Lean environment of the time, and carries the paper, in its arXiv version, with its statements and examples linked to their formal counterparts.
| Submission | Statements | Library | Environment |
|---|---|---|---|
| lax-392996 | Correctness of the provenance-aware rewriting, rules (R1) to (R4) (RewritingCorrectness); probabilistic query evaluation through provenance, Theorem 12 and Corollary 13 (ProbabilisticEvaluation, ProbabilisticEvaluationByRewriting); Why-provenance is an m-semiring (WhyProvenance); the two semantics and the rewriting rules clause by clause; the paper's running example | six commits after v1.1.0 | Lean v4.33.0 |
The submission lives under lax/provsql/ in this repository, which the
archive reads at a commit and a path. It is generated by
lax-export from its
export.yaml, the concept and bridge modules being written by hand, and the
docstring of a registered theorem names its statement in the archive.
Authorship, sources, and axioms
The definitions follow Green, Karvounarakis and Tannen and the later provenance literature, and the results on query rewriting follow the ProvSQL papers; each module cites the source it follows. The Lean formalization is original throughout. If a result here is traceable to a paper whose citation is missing, that is an oversight: please open an issue.
Part of the Lean code, including proofs and docstrings, was written with the assistance of generative models: some early proofs with models from OpenAI (GPT), and much of the more recent code with models from Anthropic (Claude). Formalization choices, the library architecture, the main definitions and theorems, and their alignment with the standard ones, were designed and written or reviewed by the author. Responsibility for the whole rests with the author.
All proofs are checked by Lean, locally and in continuous integration.
The library does not depend on any axioms apart from standard Lean ones:
propext, Classical.choice and Quot.sound. Neither sorry,
admit, nor native_decide is used.
Citing
Use the metadata in CITATION.cff, and cite the version DOI of
the tag you used rather than the concept DOI, so that the citation names a
specific state of the code.
License
MIT. See LICENSE.
Contact
Pierre Senellart pierre@senellart.com β https://github.com/PierreSenellart/provenance-lean
Bug reports are welcome through GitHub Issues.