The proof track

Ampersand generates information systems from relation-algebraic specifications. That method carries a promise: the generated system behaves as the specification prescribes. Parts of that promise have been proved, several of them with a proof assistant. This section of the documentation discloses those proofs.

The proof track is organised around two notions. A claim is a single proposition, stated precisely, together with the artifact that establishes it — an Isabelle/HOL or Lean session, or a written proof. A trail is a narrative that answers one reader's question by visiting the claims that settle it. The two are related many-to-many: one claim may serve several trails, and one trail usually visits several claims. Both are recorded in the register below, under identifiers that remain stable for the life of the repository.

The formal sources themselves live in the proofs/ directory of the Ampersand repository, next to the code they speak about. The pages here tell the stories; the repository holds the single authoritative copy of every proof.

How to read the register

Each claim carries one of four statuses.

• machine-checked — a proof assistant has verified the proof from first principles. The entry names the session and states its trust base.
• paper proof — the proof is written out in full and has been reviewed by people, but has not yet been formalised.
• stated — the proposition is formulated precisely; its proof is still outstanding.
• in progress — formalisation is under way.

Two habits keep these statuses honest. A status is recorded only after the build of the proof artifact has actually been observed, never on the strength of a report. And every machine-checked entry states what is not proved — the assumptions, the boundary of the model, the parts covered by testing rather than by the theorem. A proof is a precise instrument, and precision includes knowing where it ends.

Claims

ID	Claim	Status	Artifact	Trails
PRF-1	The runtime re-checks exactly the conjuncts a transaction can have changed	paper proof	From rules to running code, Part III	TRAIL-1, TRAIL-4
PRF-2	The incremental evaluator computes exactly the set semantics of every rule term	machine-checked	proofs/incremental/, session Incremental_Delta	TRAIL-1, TRAIL-2, TRAIL-4
PRF-3	The Kleene rewrite laws are sound, r% is the transitive reduction, and insert-only closure maintenance converges	machine-checked	proofs/kleene/KleeneReduction.thy	TRAIL-3
PRF-4	Incremental deletion from a stored closure is exact, cycles included	machine-checked	proofs/kleene/IncrementalDelete.thy	TRAIL-2, TRAIL-3
PRF-5	A singleton relation is neither total nor surjective in general; the law that assumed so is refuted	machine-checked	proofs/kleene/SingletonSurjective.thy	TRAIL-3
PRF-6	The generated delta SQL and its maintenance protocol keep the violation records equal to full re-evaluation	stated	obligation stated in Correctness of the incremental SQL queries; mathematical core discharged by PRF-7	TRAIL-4
PRF-7	The candidate calculus is complete: every pair whose membership in a rule term changes lies in the candidate set	machine-checked	proofs/incremental/Candidates.thy, session Incremental_Delta	TRAIL-4
PRF-8	A relation stored on a unique key column cannot violate the multiplicity that layout enforces, so its violation query is empty in every database state	stated	obligation stated with the cost gate of issue #1692; carried in code by structurallyEnforced in Ampersand.FSpec.Incremental.CostProfile	TRAIL-4
PRF-10	The anchored-complement rewrite preserves the meaning of a violation term: g ∩ ¬e = g − e, distributed through unions and differences, with the typing invariant kept	machine-checked	proofs/anchoredComplements/AnchoredRewrite.thy, session Ampersand_AnchoredComplements	TRAIL-1
PRF-11	In a system of contexts in which every context has one database, inclusion is a partial order, a reference denotes one thing, a rule of an included context has the same violations in the including context, and the whole is one information system precisely when every included context is consistent	machine-checked	proofs/multicontext/MultiContext.lean, Lean 4	—
PRF-12	For a difference l − r, the left-join translation and the EXCEPT translation select the same set of pairs	machine-checked	proofs/setDifference/SetDifference.lean, Lean 4, theorem same_pairs; carried in code by exceptCase, leftJoinCase and materialises in Ampersand.FSpec.SQL	TRAIL-1
PRF-13	An atom of a concept has a row in the table of every storage component that contains that concept or a generalisation of it, and a concept without a table of its own is the union of the tables of its members	stated	obligation stated with the MULTITABLE storage of issue #1716; the regression tests testing/multitable/validate compare the generated SQL with the compiler's evaluator for both shapes	—

PRF-1

The runtime re-checks exactly the conjuncts a transaction can have changed. The compiler ships, per concept and per relation, the list of conjuncts a change can affect; the back-end unions those lists at commit. The correspondence theorem states that the retrieved set equals the ground truth — every conjunct whose violation set can have changed is re-checked, and no other. The proof observes that both sides denote the same predicate, so equality is definitional; the only order fact used is the reflexivity of the specialisation order.

Artifact: the written proof in From rules to running code, Part III. Not yet formalised: the theorem is a natural first candidate for a Lean formalisation; its statement is small and its ingredients (a partial order, two set comprehensions) are standard.

PRF-2

The incremental evaluator computes exactly the set semantics of every rule term. The Isabelle session Incremental_Delta (parent HOL, no axioms beyond HOL, no sorry) proves the Z-set algebra, the desugaring identities for residuals and complements, the delta rules for the linear, bilinear and distinct operators, and a whole-circuit induction: every state reachable from the empty database by transactions — the loading of the initial population included — yields exactly the set semantics of every term. A QuickCheck suite in stack test states the same lemmas as properties over the actual Haskell functions, so the code is bound to the proofs on every build.

Artifact: proofs/incremental/; the obligation-to-lemma map is in its README.md. Not proved: the shortcuts by which the implementation skips recomputation when nothing changed, the Kleene nodes' reading of their child, and the Haskell code itself — these are covered by the per-transaction oracle and the property suite, not by the theorems. The trail Incremental evaluation walks this claim in full.

PRF-3

The Kleene rewrite laws are sound, r% is the transitive reduction, and insert-only closure maintenance converges. KleeneReduction.thy proves the unfoldings of r+ and r* that replaced four earlier rewrite laws, and refutes the law r* = r;r* that they replaced. It further proves that r% = r − (r;r+) is, for finite acyclic r, the transitive reduction — closure-preserving and minimum — and that the ENFORCE fixpoint c ⊇ r ∪ r;c converges to r+ by Knaster–Tarski, so insert-only maintenance cannot oscillate.

Artifact: proofs/kleene/KleeneReduction.thy. Boundary: minimality of r% is proved for finite acyclic relations; on cyclic input r% is still well-defined but no longer minimum.

PRF-4

Incremental deletion from a stored closure is exact, cycles included. Subtracting the deleted pairs from a stored transitive closure is wrong, and the theory proves it wrong (naive_delete_unsound). The sound procedure confines re-derivation to the affected region r* ; del ; r*: outside it the old closure is reused verbatim, and the recombination (r − del)+ = (safe ∪ (r − del))+ is proved exact for r+, r* and r% alike, with no acyclicity assumption.

Artifact: proofs/kleene/IncrementalDelete.thy. Status in the code: the compiler does not yet apply this procedure; the claim precedes its implementation, which is the intended order.

PRF-5

A singleton relation is neither total nor surjective in general; the law that assumed so is refuted. The compiler once judged the singleton "a"[C] both total and surjective, from which the normaliser concluded V;"a" = V and silently discarded the restriction — a defect that surfaced as unbounded growth of a production database. The theory refutes the assumed properties with explicit witnesses, proves V;"a" ≠ V whenever C has more than one atom, and records the properties a singleton does have (univalent, injective, symmetric, antisymmetric, transitive).

Artifact: proofs/kleene/SingletonSurjective.thy. Scope: the refutation motivated the corrected isTotSur/isTot in Ampersand.Classes.Relational; the correctness of that Haskell code is covered by the regression suite, not by the theorem.

PRF-6

The generated delta SQL and its maintenance protocol keep the violation records equal to full re-evaluation. The route is candidate-based: the compiler derives, per conjunct and touched relation, a candidate query — an ordinary relation-algebra term over the base relations and the transaction's delta tables — and compiles it with the same term-to-SQL translation as the full violation queries. At commit the runtime re-runs the conjunct's violation predicate on the candidate pairs only, updating the materialized violation table with two statements scoped to those pairs; full re-evaluation remains the fallback outside the supported class. The claim is that this maintained table equals, after every commit, the result of the full violation queries. The obligation decomposes into a mathematical core and a protocol statement. The core — no pair can change its violation status without appearing in the candidate set — is PRF-7, machine-checked. What remains is the protocol statement: that the delta tables record exactly the transaction's changes, that the two scoped update statements applied to a correct cache leave it correct, and that the fallback classification and the repair-engine iterations preserve this — the SQL-level counterpart of the circuit induction of PRF-2.

Status: stated — registered before its proof, as the working method requires. Evidence to date: a harness in the style of ampersand validate over the regression suite, and a divergence-free shadow run of 1142 transactions on a production-scale application, documented in the trail Correctness of the incremental SQL queries. Planned vehicle: Isabelle/HOL, extending proofs/incremental/Candidates.thy with the commit-protocol statement.

PRF-7

The candidate calculus is complete: every pair whose membership in a rule term changes lies in the candidate set. The theory Candidates.thy (in session Incremental_Delta, parent HOL, no axioms beyond HOL, no sorry) formalises the candidate calculus of the delta-SQL route: the widened and narrowed envelopes W/N as one recursion with a polarity flag, and the candidate set as a recursion over the supported term class — union, intersection, difference, composition, converse and typed complement over relation leaves and state-independent leaves. Under the single assumption that every changed pair of a base relation is recorded in that relation's delta table, it proves the envelope invariant (W bounds the old and new denotation from above, N from below), one completeness lemma per operator (K1–K6), the whole-term theorem K_complete, and the per-relation decomposition K_per_relation: the union of the per-relation candidate queries — the shape the compiler actually generates — equals the global candidate set whenever untouched relations have empty delta tables. Completeness is the only property the route needs: a too-large candidate set costs time, never correctness. The session extends the existing Isabelle development because the lemmas build directly on the set-level house style of its Desugar.thy; the Lean-first preference stands for standalone new work.

Artifact: proofs/incremental/Candidates.thy; the obligation-to-lemma map is in the session's README.md. Not proved: the Haskell functions widen/narrow/candidateTerms that mirror the calculus — these are bound to the lemmas by a QuickCheck bridge (Ampersand.Test.Incremental.CandidateProperties in stack test, on the delta-sql branch with the code it tests) and exercised by the delta-SQL harness ampersand incremental-bench --sql — the SQL compilation of the candidate terms (shared with the full queries and guarded by ampersand validate), and the delta-table contract itself — that the runtime records every changed pair — which belongs to the protocol half of PRF-6. The constancy of concept populations is an assumption of the theorems, discharged operationally by the concept-affected fallback.

PRF-8

A relation stored on a unique key column cannot violate the multiplicity that layout enforces, so its violation query is empty in every database state. The generated schema stores a univalent relation as a column of a wide table whose key attribute carries the SQL UNIQUE constraint: the key atom occupies at most one row, and that row holds at most one value in the relation's column, so no state the schema admits contains two pairs with the same source. The claim is that, for exactly the storage layouts the predicate structurallyEnforced accepts — a UNI relation stored unflipped on a primary-key column, and dually an INJ relation stored flipped — the violation set of the generated property-rule conjunct is empty in every database state, reachable or not. The cost gate of issue #1692 rests on this claim when it routes such a conjunct as structural and runs no query at all; the runtime may take that route only behind its feature switch, and its sampled self-check keeps covering skipped conjuncts, so a defect in the claim would surface as an alarm rather than as silent drift.

Status: stated — registered with the implementation, before any query is skipped, as the working method requires. Boundary: the claim covers only the accepted layouts; link tables, specialization columns (which carry no SQL uniqueness constraint), and scalar-represented keys are deliberately outside it and keep their query. Planned vehicle: Lean 4 — the statement is small, standalone, and needs only a model of the table shape.

PRF-13

An atom of a concept has a row in the table of every storage component that contains that concept or a generalisation of it, and the population of a concept without a table of its own is the union of the tables of its members. A hierarchy whose root is marked REPRESENT ... TYPE MULTITABLE is stored in several wide tables (issue #1716): the storage graph is the concept graph without the edges into a marked concept, and every component of it with one root is one table. The SQL generator reads I[A] from the table of the component of A, reads a concept that has no table of its own (CLASSIFY C IS A \/ B with the mark) as the union of its members, and joins the tables of a composition on the atom value. The claim is that the queries so generated select the same pairs as the queries over one wide table do, provided the runtime keeps the invariant in the title when it adds and deletes atoms: addAtom inserts the atom in every table listed under conceptTables in concepts.json, and deleteAtom deletes it from those and from the tables of the concept's specialisations. The regression tests testing/multitable/validate compare, for every term of two scripts in both shapes, the pairs the generated SQL selects with the pairs the compiler's own evaluator computes.

Status: stated — registered with the implementation, as the working method requires. Boundary: the claim says nothing about disjointness: an atom that enters two sibling tables through the API is representable, and the claim holds for it as well; what such an atom breaks is the univalence of a relation stored in several tables, which is why the cost gate of PRF-8 excludes those relations from the structural class.

PRF-10

The anchored-complement rewrite preserves the meaning of a violation term. A complement inside a violation term used to be compiled through the closed world V[A*B]: a Cartesian product of two concept tables, probed per row by a correlated NOT EXISTS. The pass anchorComplements (issue #562) flattens each intersection, picks a complement-free member as anchor, and pushes it inward until every reachable complement is absorbed into a difference the SQL generator compiles as an anti-join. The theory AnchoredRewrite.thy (session Ampersand_AnchoredComplements, parent HOL, no axioms beyond HOL, no sorry) proves, over binary relations as sets of pairs with the typing invariant term ⊆ V[A*B], the three rules the pass applies — absorb g ∩ (V − e) = g − e, distribute g ∩ (p ∪ q) = (g ∩ p) ∪ (g ∩ q), push g ∩ (p − q) = (g ∩ p) − q — together with the difference desugaring of the SQL generator, the worked example of the issue, the soundness of folding one anchor through several members ((g ∩ m₁) ∩ m₂ = g ∩ (m₁ ∩ m₂)), and that an anchored difference g − e stays inside V whenever the anchor g does.

Artifact: proofs/anchoredComplements/AnchoredRewrite.thy; the rule-to-lemma map is in the session's README.md. Not proved: termination of the Haskell pass (argued in the code: every step removes a complement or moves the anchor strictly closer to one), the choice of anchor, the typing invariant for the anchors the pass forms after a distribution (a union, by R2) or by intersecting members (the lemma covers the difference only), and the SQL generation of the rewritten term, which remains guarded by ampersand validate; the regression tests in testing/cartesian/ assert anchoredness through the exit code of --fail-on-cartesian-product. Boundary: where an intersection has no complement-free member the product is semantically necessary, and the compiler says so with a warning instead of rewriting.

PRF-11

A system of contexts, each with one database, is one information system from the viewpoint of each context. The statement CONTEXT A INCLUDES B makes the declarations and the population of context B visible in context A, under the name of B or an alias as a prefix. The Lean session models a system of contexts in which every concept, relation and rule has one owner, in which every fact is stored in the database of its owner, and in which a context sees the data of the contexts it reaches. It proves seven results with their lemmas: acyclic inclusion yields a partial order (reach_antisymm); a reference denotes at most one thing of each kind, and every thing of an included context has a reference (local_reference_unambiguous, reference_unambiguous, reference_complete); a rule has the same violations in every view that contains its context (truth_is_imported); a view with all rules that hold in it is one information system precisely when every reached context is consistent (flattening, wellTyped_view_iff); adding an including context changes nothing for the included one (reach_extension, view_extension); a change affects only the contexts that reach what it writes (frame, non_interference, not_affected, preservation); and a migration context that has no violation of the new invariants left leaves the desired system consistent (moment_of_completion). The specification that the compiler is built against is AmpersandData/FormalAmpersand/MultiContext.adl.

Artifact: proofs/multicontext/, core Lean 4 without mathlib; lake-build.txt records the observed build, which uses no sorry and no axioms beyond propext, Quot.sound and, for one theorem, Classical.choice. Bound to the specification by: the populations in memorybank/multi-context/spec-checks/, which ampersand check accepts (a diamond of inclusions, a migration with two contexts of one name) or refuses (a copied concept, a cycle, an ambiguous prefix). Bound to the code by: the regression cases in testing/Travis/testcases/MultiContext/, one per rule of the specification; the property suite Ampersand.Test.MultiContext.QualifyProperties in stack test, which states for arbitrary contexts that an included context contributes its names with the prefix and that a context reached along two paths contributes them once; and the scenarios in test/multi-context of the prototype framework, which run a diamond of four contexts and the migration case of the RAMiCS 2024 paper with one database per context. The compiler uses the theorem on flattening: it joins the compiled context with the contexts it reaches, so that type checking, normalisation and SQL generation work on one context. Not proved: the Haskell code itself, the correspondence between the abstract model and the type checker, the translation of a classification across contexts into a write, and the equality of a query over several databases with the same query on one database.

PRF-12

For a difference l − r, the left-join translation and the EXCEPT translation select the same set of pairs. The SQL generator translates a difference l − r in one of two ways. By default it joins the query of l to the query of r with a left join on both columns and keeps the rows without a partner. When the query of r is one that the database must materialise before it can join it, which is the case when r contains a closure or a union, it generates select src, tgt from (l) except select src, tgt from (r) (issue #1708), because a left join onto a materialised query compares every row of l with every row of an unindexed temporary table. The claim is that both translations denote the set difference of the relations that the queries of l and r denote, provided that neither query yields NULL in its source or target column, and that the result carries no duplicates. Together with PRF-10, which gives g ∩ ¬e = g − e, this makes the choice between the two translations a matter of cost and not of meaning.

Artifact: proofs/setDifference/SetDifference.lean (Lean 4.34.1, core library only, no sorry; lake build in proofs/setDifference). The file models a two-column table as a list of rows, so duplicates count as in SQL, and a left-join row without a partner as a row with NULL in its right-hand columns. The theorem same_pairs states that a pair is selected by the left-join translation exactly when it is selected by the EXCEPT translation; both select the pairs that occur in l and not in r (mem_leftJoinQuery, a calc chain of four steps, and mem_exceptQuery). exceptQuery_nodup states that the EXCEPT result carries no duplicates, and same_pairs_flipped covers the variant in which r is replaced by its converse. Boundary: the claim is about the set of pairs and about tables without NULL. The left-join query can return a pair more than once, and the generated query removes those with select distinct. That the generated subqueries never yield NULL in either column is an invariant of the generator that this claim assumes and does not prove. Not proved: that the Haskell functions produce the SQL the file models, and the choice between the two translations (materialises), which bears on speed and not on meaning. Both are guarded by ampersand validate in the regression suite; the test case testing/Travis/testcases/SetDifference reaches both translations with non-empty results.

Trails

ID	Trail	The question it answers	Narrative	Claims visited
TRAIL-1	From rules to running code	When I write a rule, where does its code end up, and is the enforcement machinery correct?	From rules to running code	PRF-1, PRF-2, PRF-10, PRF-12
TRAIL-2	Incremental evaluation	Can a system that maintains rule violations incrementally ever disagree with full re-evaluation?	Incremental evaluation	PRF-2, PRF-4
TRAIL-3	The Kleene operators	What does Ampersand guarantee about transitive closure — its laws, its reduction, its maintenance?	The Kleene operators	PRF-3, PRF-4, PRF-5
TRAIL-4	Correctness of the incremental SQL queries	When the runtime maintains its violation records by increments, what guarantees they never drift from the full queries that define them?	Correctness of the incremental SQL queries	PRF-1, PRF-2, PRF-6, PRF-7, PRF-8

A trail's narrative need not live on this site. TRAIL-1 is anchored in the reference chapter that contributors already read; a future trail may be anchored in a published article, with the register linking the article to the claims it rests on. What the register guarantees is the connection: from any claim to every story that uses it, and from any story to every claim it stands on.

Tools and trust base

The machine-checked claims are Isabelle/HOL sessions (Isabelle 2025-2), built on the plain HOL heap with no additional axioms and no sorry. Each session builds headless with isabelle build -D proofs/<session>. Where a claim speaks about running code, a bridge binds the two: the QuickCheck properties of stack test state the Isabelle lemmas over the actual Haskell functions, so every build re-checks the correspondence.

For new formalisations the project prefers Lean 4 with the mathlib toolchain. Lean's blueprint culture matches the shape of this proof track — a human-readable narrative in which every statement links to its formalisation, with an explicit status per statement and a dependency graph generated from the sources. The existing Isabelle sessions remain authoritative for their claims; a claim migrates to Lean only when there is a reason beyond the change of tool, and the register records such a migration as a new artifact under the same claim number.

Three further habits are borrowed deliberately from neighbouring cultures: the assumptions discipline of seL4 (every verification statement names its boundary), the per-pass provenance tables of CompCert (each claim entry names its artifact and its bridge to the code), and the permanent tags of the Stacks Project (identifiers below are never renumbered and never reused).

Extending the proof track

The track grows claim by claim and trail by trail. The conventions that keep it coherent:

1. Identifiers are permanent. A claim number (PRF-n) or trail number (TRAIL-n) is assigned once and never renumbered or reused, even if the claim is superseded — a superseded entry keeps its number and points to its successor. Before assigning a number, check the git history as well as the current file.
2. Every proof session appears in the register. A directory under proofs/ that contains an Isabelle ROOT (or a Lean lakefile) has at least one claim entry here. The CI script scripts/check-proof-track.js enforces this, together with the uniqueness of identifiers and the validity of statuses.
3. Ordinary documentation pages refer to a claim with a single line. The fixed form is one italic sentence, for example: Proof track: PRF-2 — the incremental evaluator is exact. No formal notation, no proof sketches, and no further apparatus appear outside this section; readers who have no use for proofs should meet at most that one quiet line.
4. A proof obligation arises with the work, not after it. A change to semantics-bearing code — rewrite laws, the delta calculus, the SQL generation of terms, the typology logic — states its claim in this register in the same change, with status stated until the proof exists. The claim precedes the proof, and the proof precedes the confidence.
5. A trail page follows one template. It opens with the reader's question, answers it in prose, then visits its claims in order — for each: the statement in words, the idea of the proof, and the boundary of what is proved. It closes with instructions to reproduce the builds. The prose is written for publication: unhurried, complete sentences, claims no stronger than their artifacts.