The theory behind versioning

Every check in Hopskip’s versioning system is a computation over a precisely defined mathematical object. This page defines those objects, says why each one is the one the checks use, and shows how they fit together. It is the one page in the documentation where the formal vocabulary appears: everywhere else you read event graph, mapping, backfill, and replay check, and this page says what those words denote and why the formal choice is what makes the checks computable.

A convention runs through the page. After every formal expression, the words “in words” give its plain reading. Every section opens with the problem its object solves, so you can read for motivation first and notation second. Nothing operational depends on this page. The versioning concepts page describes the system as an operator meets it, and the formal account in the repository is the authority where this page and it disagree.

The running example

One example runs through the whole page. A workflow type billing moves from version 3 to version 4, with three changes:

• the command type PaymentCmd is renamed to ChargeCmd,
• its payload changes from an integer amount to a record {amount, currency},
• a new event type RiskCheck is added, computed for old runs from data they already recorded.

An execution started under version 3 is mid-flight when version 4 registers: it has recorded a start event, two charge commands, and their results, and it is waiting on a third.

Everything below answers one question: what does it mean, exactly, to move this execution across that change, and how can a machine check the answer before anything is touched.

Event schemas

A workflow version does not record arbitrary bytes. It records events with structure: a charge command determines the order it charges, an auth result determines the command it answers, and chains of those “determines” links carry meaning across the history. The version publishes that structure as its event schema.

A schema has three parts:

• Objects are event types: Start, PaymentCmd, AuthResult, RiskCheck.
• Morphisms are derivations between them. An arrow answers : AuthResult -> PaymentCmd says every auth result determines which charge it answers. Derivations compose: if C derives from B and B derives from A, then C derives from A along the two-step path.
• Path equalities record that two derivation routes compute the same thing: “the total derived per order equals the total derived per line, summed”.

Objects with composable, labeled arrows is a category. In words: the schema is a typed graph plus a composition rule plus a list of “these two routes agree” facts. The formal statement is that an event schema presents a finitely presented category: generators are the types and direct derivations, relations are the path equalities.

Here are the schemas of the two versions in the running example, and the patch’s mapping drawn between them:

Why insist on categories rather than plain graphs? Because the mapping between versions must respect composition. Suppose RiskCheck followed from Start through an intermediate type. After the mapping renames and retypes everything, the translated RiskCheck must still follow from the translated Start through the translated intermediate. A graph homomorphism can map each node and each edge while breaking the chained routes. A functor, the structure-preserving map between categories, cannot: it sends composites to composites by definition. That requirement is the entire content of the translation well-formedness check that runs at patch registration.

Path equalities must normalize

A schema presented by generators and relations carries a question the system has to answer constantly: are these two derivation paths equal? In a general finitely presented category that question is undecidable. It contains the word problem for finitely presented monoids, which Post proved unsolvable in 1947. A versioning system that had to answer it in full could check nothing, and this model refuses to leave any check undecidable.

The fix is to restrict which relations a schema may declare. Each path equality must orient into a rewrite rule that makes paths smaller in a fixed ordering: fewer steps first, then alphabetical (shortlex). The registration checker verifies the decrease for every rule, rule by rule. If every rule decreases the order and every critical pair of rules joins again, the rule set is a terminating, confluent rewriting system. In words: repeatedly applying the rules always stops, and it always stops at the same normal form no matter which order you applied them in. “Are these two paths equal?” then becomes “normalize both and compare”, a computation that always finishes.

Both halves are machine-checked. Termination is proven with an explicit fuel bound: a word over an alphabet of k letters embeds into the naturals in a way that strictly decreases under every rule, so normalization finishes within a bound computed from the word. Confluence follows from checking the finitely many critical pairs, which is what the registration checker does, plus Newman’s lemma. A schema whose equalities do not orient this way is rejected at registration. This is the same restriction categorical database systems (CQL) adopted, for the same reason.

Histories as instances

The data side now has its schema notion. The next object is the data itself: what one recorded execution actually contains.

A recorded execution is not a list of bytes to the model. It is structured data shaped exactly like the schema:

• to each event type, the finite set of its recorded occurrences;
• to each derivation, the function saying which occurrences of the target were derived from which occurrences of the source.

That assignment respects composition: the two-step derivation function is the composite of the one-step ones. Formally that makes it a functor from the schema category into Set, the category of sets and functions. Such a functor is called a copresheaf, and the model calls each one a history. In words: a history is a small database that conforms to the schema, one database per execution. The event types are its tables, the derivations are its foreign keys, and the path equalities are its integrity constraints.

The running example’s history, drawn as an instance:

Finiteness matters. Because each table is finite, every question the model asks about a history is a computation over finite data. This is what makes per-execution migration checking possible at all: the checks run over one execution’s tables, not over the schema in the abstract.

Translations as functors

A patch from version 3 to version 4 carries a mapping: what each old event type becomes, and what each old derivation becomes. Formally the mapping is a functor P : C -> D from the old schema category to the new one:

• each old event type is sent to a new event type, in the example PaymentCmd maps to ChargeCmd;
• each old derivation is sent to a path of derivations in the new schema, with endpoints matching the mapped source and target;
• composites are sent to composites, and every declared path equality still holds after translation.

In words: the translation is a dictionary that also translates grammar, so that facts derivable before remain derivable after. A dictionary that mapped words but broke sentences would move data without moving meaning. Functoriality is the property that forbids it, and the registration check for it is finite: verify the endpoint rule on each edge and each declared equality on the generators, and composition takes care of the rest.

Old types with no image under P are dropped. New types outside the image, RiskCheck in the example, must be classified explicitly as placeholder or backfilled; an unclassified new type is a registration error.

The plain form gives every old type exactly one new type. Some patches need less: one old type may map to several new ones, or to none. The planned extension is a relation-style mapping, formally a profunctor, a functor D^op x C -> Set. In words: a translation table rather than a function, where each row relates an old type to zero or more new types. Such tables compose by an operation called a coend, which is what makes multi-hop migration (version 3 straight to version 5, skipping the intermediate deploy) a single composed table. The plain functor form embeds into this one without breaking stored patch manifests.

Carry-forward: the left Kan extension

Given the mapping P : C -> D and a history x on C, the migration has to decide what history to record on D. Many answers are possible. The model uses a specific one, and the reason it can call that answer canonical rather than heuristic is the central fact of the data layer.

The answer is the left Kan extension of x along P, written Σ_P x (“sigma”). In words: copy every recorded occurrence across through P, then add whatever the new schema demands that the old data cannot supply, filling those positions with free placeholder values. Nothing else is invented. For the running example: both charge commands and both results copy across under their new names, and the new schema’s demand for one RiskCheck per run gets a placeholder, because the old history recorded nothing of the kind.

Σ_P is characterized by a universal property. For any other way y of putting the old data into the new schema that agrees with P, there is exactly one map Σ_P x -> y commuting with everything. In words: it is the migration that changes nothing you did not ask for, and every other reasonable migration factors uniquely through it. That uniqueness is why the model can call copy-forward-with-placeholders the canonical migration instead of one heuristic among several.

The algorithm that computes Σ_P x is the chase, from database theory: find an unsatisfied demand of the new schema, add the forced elements or merge the forced duplicates, and repeat. When no demands remain, the result is the completed instance. Two facts about this loop are proven, not assumed:

• It terminates, with an explicit bound. The proof supplies a size measure, Phi in the mechanization: the total weight of the instance’s outstanding demands, where each demand is weighted by what discharging it will eventually cause. Every fill step strictly decreases Phi, so the loop finishes within Phi steps.
• The bound is conditioned on acyclicity, and that condition is sharp. The proof requires the schema’s total derivation edges to be acyclic. Without that condition the loop provably does not terminate: a cycle of total edges lets each pass force new elements forever, and the mechanization proves the non-saturation as a control case. In the engine, a step budget proportional to history size turns any schema that violates the condition into a registration-time error instead of a hung migration. Where the total edges are acyclic the budget is a backstop, never the mechanism.

Backfills: toward the right adjoint

Free migration is honest but lazy. A placeholder says “the new schema wants a RiskCheck here and the old data does not have one.” A backfill replaces that placeholder with a value computed from the old history: in the example, a function over the recorded start event and charge commands that produces the risk assessment version 4 would have recorded.

Formally, Σ_P is the left adjoint of the translation, and there is a right adjoint Π_P (“pi”): the migration in which every demanded value is actually produced. In words: Σ is “give me the least migration consistent with the mapping”, and Π is “give me the most demanding one.” A backfill is a deliberate step from the first toward the second: for each new type, the patch either supplies a total function over the old history or declines with a stated reason, and the declined runs are reported, never guessed into.

The middle of the triple is the simplest to understand. Δ_P (“delta”) re-tags new-version data as old-version data, without computing anything. In words: it lets an old reader see the migrated history through old eyes. This is what the “view as previous version” operation does, and it is how a migration keeps old readers working during a rolling deploy. The adjoint notation is Σ_P ⊣ Δ_P ⊣ Π_P, read “sigma is left adjoint to delta, delta is left adjoint to pi”.

An adjunction between two operations means each is the best approximation of the other from its side. Round-tripping one way and back is not necessarily the identity, but it is the closest thing to the identity that side admits, and the comparison maps of the round trips are tracked. The one that matters for rollback is the unit of Σ_P ⊣ Δ_P, the comparison map x -> Δ_P Σ_P x. In words: the old history versus its own shadow after migrating forward and re-tagging as old.

Rollback exactness: units and lenses

Rollback through a patch is carry-forward followed by view-as-old. It is exact precisely when that round trip loses nothing: migrating forward and viewing back returns the original history, nothing blurred and nothing lost. Formally: the unit is invertible on that history. In words: the shadow coincides with the thing.

Losslessness is not automatic, and the engine tracks its two conditions separately, per execution:

• R1, the image condition. Every event appended after migration has a preimage type under the mapping and a payload determined through the mapped derivations. The first event without one closes the window.
• R2, the injectivity condition. The mapping sends this execution’s occurrences one-to-one: no two old occurrences land on one new occurrence, and nothing is deleted without archival. A patch that merges events closes the window at migration time, before any new event is recorded.

The pair of forward and backward migrations obeying the round-trip laws is a delta lens, the standard formal object for a bidirectional synchronization that does not lose data. A rollback that has become inexact is a lens whose laws no longer hold at that execution, and the window records the first event that broke them. That event is exactly the “rollback expired at event N” the product surfaces.

Behavior: step functions and their trees

The data side is half the model. The other half is what the code does.

A workflow version is formalized as a coalgebra: a step function that, given the current pending context Γ (gamma; in words: the map of outstanding commands the workflow issued but has not received results for, plus the signal channels it listens on) and a delivered event, produces a reaction: complete, or issue a batch of new commands and keep waiting. Because the environment chooses which event arrives next, a version is nondeterministic from the outside and deterministic from the inside: given the delivered event, the reaction is fixed.

The behavior tree of the running example’s version 3, unfolded from one waiting state, and what remains after the recorded history:

Unfolding the step function along every possible delivery order gives the behavior tree of the version: the tree of all its possible futures, one path per interleaving. The model takes no quotient by interleaving, because code may lawfully branch on arrival order. Formally the tree is the image of the step function in the final coalgebra of the behavior functor. In words: among all objects that behave this way there is a most general one, defined by nothing but “what can happen next”, and the tree is it. For the mathematically inclined: the functor is a dependent polynomial, the pending-context indexing is an indexed container, and the mechanization represents the tree as an interaction tree, a coinductive structure for programs that interact with an environment. Internal nondeterminism, if it ever entered the model, would move the representation to choice trees: a planned revision with a known target, not an open question.

Two versions are bisimilar when no experiment distinguishes them: every future of one is a future of the other. Bisimulation is the witness relation for that fact. Migration needs a one-sided version of it: a simulation from the old behavior to the new, meaning the new version can imitate every step the recorded past took. The patch stores that witness as its replay plan, represented not as a function on all paths but as the composite action of the patch’s verbs applied pointwise along the history. In words: the replay plan is a proof-shaped object showing that every step the old run took has a matching step the new code can take.

Given a recorded history h, what remains to do is the residual, written ∂_h b and called the Brzozowski derivative of the behavior b: the subtree that starts where the recorded past ends. In words: differentiate a behavior by a history and you get the rest of the run. The migration soundness theorem says a migrated execution’s future is exactly the derivative of the new behavior at the translated history: the past is accounted for, and the future is the new code’s.

The replay check as a commuting square

The per-execution check compares two routes at every step of the recorded history. Route one: replay the old code on the recorded past, then translate the reaction it issues. Route two: translate the recorded past first, then replay the new code on it. The check demands the two routes agree at every position, comparing issued batches as id-indexed maps over decoded values.

That agreement is the commutation of a naturality square for the translation:

In words: translating-then-replaying equals replaying-then-translating, at every position of the history, and the check verifies exactly this, position by position, reporting the first square that fails to commute together with the offending batch diff. There is no generic “nondeterminism detected” outcome anywhere in the system, because divergence is always a square that fails, and a square that fails has a location.

Codecs as prisms

Payloads cross the migration boundary as decoded values, not bytes, and the decoding itself needs a guarantee. A payload codec (JSON, a binary encoding) is a prism in the optics sense: a partial invertible reference into bytes, a pair enc : T -> Bytes and dec : Bytes -> Either DecodeError T. The round-trip law, “what it writes, it reads back”, is the prism law: dec ∘ enc = Right. In words: encoding then decoding is the identity on values the codec accepts, and decoding failure is information, not corruption. The law is not statically checkable in general, so it is property-tested at registration on generated values rather than proven, which is one of the listed assumptions in the trusted base below.

Format versus meaning: the factorization

Every patch factors uniquely, up to isomorphism, into a vertical part that only re-encodes (codec reassignments, no semantic change) and a horizontal part that changes meaning. In words: format changes and meaning changes split the way “renaming a file” and “editing a file” split, and doing them in either order converges to the same result. That convergence is the interchange theorem, and it is proven.

This is why a format-only patch needs no replay check and never interferes with a later meaning change, and why lazy and eager re-encoding are observationally equivalent: the envelope tag, not the timing, decides how bytes are read.

Deploy order: squares and fillers

When two services exchange events, a version change on one side changes what the pair can say to each other mid-rollout. The model arranges versions on a grid: deployed schemas as objects, contracts as horizontal arrows between service-version pairs, patches as vertical arrows upgrading a service. A mid-rollout state, one service upgraded and its counterparty not, is a square in this arrangement. The structure of two kinds of arrows plus compatible squares is called a double category.

“Can these two still talk mid-rollout” is the existence of a square filler: a translation occupying the square that makes both routes around it agree. When either order works, the two canonical fillers are called the companion and the conjoint of the patch. The plan safety theorem states that a deployment plan is valid exactly when every square reachable under the plan, upgrade steps and rollback steps alike, has a filler. In words: the checker’s four verdicts (either order, A first, B first, cut over together) are a complete case analysis of filler availability, so validating the order is a typing question, not a search. The equivalence, both directions, is proven.

What is proven, and what is assumed

The architecture is translation validation, the classical stance from verified compilers: prove the validator correct once, then validate each artifact mechanically. The proof surface is fixed: the registration checker, the verb algebra’s obligations, the rollback tracking, the deploy-order calculus, and the engine’s commit protocol. Individual patches are never proven; they are checked by machinery that is.

The theorems state one invariant, the replay invariant: after every operation (deliver, crash and resume, migrate, rollback, re-encode), replaying the recorded history reproduces it exactly, pending context included. Ten theorems say each operation preserves it, that rollback through an open window is the identity, that no command is resolved twice under any interleaving, that certified patches migrate everything the verb algebra promises, that format-only patches are inert, and that a validated plan never strands a pair without a filler. The behavior layer is mechanized over interaction trees with parameterized coinduction; the data layer, finitary by construction, is mechanized, extracted, and differentially tested against the production kernel in CI, so the two cannot drift.

No honest proof is unconditional. The trusted base is exhaustive and short:

• storage provides the atomic write the commit protocol uses, bridged by a model-checked refinement of the implemented protocol against its atomic specification, and exercised by fault injection on a real system;
• codec round-trip laws hold beyond the sampled generator, property-tested, not proven;
• workflow code is deterministic given delivered events, enforced by the sandbox, not by convention;
• the production kernel agrees with the extracted proofs’ kernel, an empirical fact maintained by differential testing.

Everything else is a theorem. A soundness claim conditioned on an enumerated base like this is the strongest form of “proven correct” there is; the model says so explicitly and declines to claim more.

The dictionary

The surface vocabulary used everywhere else, and the formal object each names:

Surface term	Formal object
event graph	finitely presented category: event types as objects, derivations as morphisms, declared path equalities
history	finite instance: a Set-valued functor (copresheaf) on the schema category, one per execution
mapping (in a patch)	functor between schema categories; the relation-style extension is a profunctor, composed by coends
carry data forward	left Kan extension Σ_P along the mapping, computed by the chase, terminating with the explicit bound
placeholder	the free element Σ_P introduces where the target schema demands structure the source cannot supply
backfill	refinement of the free migration toward the right adjoint Π_P: every demanded value produced
view as previous version	the pullback Δ_P, middle of the adjoint triple Σ_P ⊣ Δ_P ⊣ Π_P
rollback available	invertibility of the unit of Σ_P ⊣ Δ_P on this instance; the R1/R2 tracking is a delta-lens discipline
behavior of a version	coalgebra of a dependent polynomial functor over pending contexts; its behavior tree is the image in the final coalgebra
replay plan	simulation of the old behavior by the new, stored as the composite action of the patch’s verbs
replay check	commutation of the naturality square between old-code replay and new-code replay on the translated history
what remains after a history	the Brzozowski derivative ∂_h b of the behavior tree
format change vs meaning change	the vertical/horizontal factorization: patches fiber over semantic schemas, and the two never interfere
codec	a prism onto bytes; the round-trip law is the prism law, property-tested at registration
deploy-order check	square fillers in a double category whose objects are deployed schemas, horizontal arrows are contracts, vertical arrows are patches; the two canonical routes are companion and conjoint translations
the checker itself	translation validation: the validator is proven correct once, each patch validated mechanically at registration and migration time

Reading list

The load-bearing references, in reading order, each with what to read it for:

• Spivak, Functorial data migration (2012). The Δ/Σ/Π triple for data migration; the shape of the whole data layer.
• Fagin, Kolaitis, Miller, Popa, Data exchange (2005). The chase as used here, in schema-mapping form.
• Schultz, Spivak, Vasilakopoulou, Wisnesky, Algebraic databases (2017). The CQL system, whose decidability restrictions this model shares.
• Rutten, Universal coalgebra (2000). Step functions, final coalgebras, bisimulation: the vocabulary of the behavior layer.
• Milner, Communication and Concurrency (1989). Simulation as the witness of “can imitate”.
• Brzozowski, Derivatives of regular expressions (1964). The derivative, read here as “remaining futures”.
• Xia, Zakowski, He, Hur, Malecha, Pierce, Zdancewic, Interaction trees (2020). The coinductive representation the mechanization uses for behaviors.
• Hur, Neis, Dreyer, Vafeiadis, The power of parameterization in coinductive proof (2013). The coinductive proof technique behind the behavior theorems.
• Diskin, Xiong, Czarnecki (2011) and Johnson, Rosebrugh (2013), on delta lenses. The rollback round-trip laws.
• Wood, Abstract pro arrows I (1982) and Grandis, Paré (1999). Equipments and double categories: the deploy grid’s squares, companions, and conjoints.
• Pickering, Gibbons, Wu, Profunctor optics (2017). Prisms, the formal packaging of codecs.
• Pnueli, Siegel, Singerman, Translation validation (1998) and Tristan, Leroy (2008). Prove the validator once, check every run: the verification stance of the whole model.

Each reference backs a specific claim in the model; the formal account in the repository carries the exact mapping.