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-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.

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
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.