Schema version control semantics

panproto-vcs stores immutable schema-related objects in a content-addressed directed acyclic graph (DAG). Mutable branch and tag references point into that graph. Its command vocabulary includes familiar operations such as init, add, commit, branch, merge, log, and diff, but the stored objects and merge algorithm operate on parsed schema structure rather than lines of source text.

This distinction changes the form of a conflict. A text merge reports overlapping edits to lines. A schema merge compares vertices, edges, constraints, and the other fields of the common representation, then reports incompatible structural edits as typed conflict values. Syntax and protocol validation still run separately; structural merge alone does not guarantee that every merged schema is valid.

Objects and references

Every object identifier is a BLAKE3 digest of the object’s type-specific canonical serialization. Objects are stored under .panproto/objects/, branch references under .panproto/refs/heads/, and tag references under .panproto/refs/tags/. The filesystem store writes objects and refs through a flushed sibling temporary file followed by a same-directory rename. It recomputes an object’s identifier when reading it and returns ObjectCorrupted if the stored object does not match its path. Ref names must consist only of ordinary relative path components.

A branch is a mutable reference rather than an immutable object. A commit may have more than one parent, so the commit relation forms a DAG rather than a simple sequence.

Validation at stage and commit

Migration validation checks that mapped vertex and edge identifiers exist at both endpoints and that each mapped edge lands between the images of its source endpoints. The same structural obligation is checked during migration compilation, where a failure is reported as NotAMorphism. By default, migration errors make staged content invalid and block commit with VcsError::ValidationFailed.

Verification can be bypassed deliberately at two points, and both have to be taken for unverified material to reach a commit. AddOptions::skip_verify and AddDataOptions::skip_verify permit an object to remain pending at stage time; a default commit then refuses it, because “not checked” and “checked and passed” are different states and only the second is a pass. CommitOptions::skip_verify is what accepts a pending or invalid stage, and the resulting commit records on its unverified field what it accepted, so the bypass is legible in the history rather than only at the moment it was taken. These options weaken the repository invariant and should be treated as explicit overrides rather than ordinary workflow.

When a registered protocol theory contains equations, model validation checks the supplied finite model against them. The evaluator considers at most 10,000 variable assignments for an equation; exceeding that bound returns ModelCheckLimitExceeded instead of accepting the equation. If no theory is registered, validation records an advisory that no equations were checked while retaining the available structural checks. ThWType, used as an instance theory by several protocol groups, contains two equations connecting arc endpoints to schema-edge endpoints. The schema theory and instance theory remain separate, so the presence of those equations does not mean that panproto_schema::validate evaluates them over a Schema.

Structural three-way merge

Let $B$ be a common base and $O$ and $T$ the schemas on the two branches. The categorical account reads merge as a pushout of the divergent changes over their base (Mimram and Giusto 2013):

$$\begin{array}{ccc}B& \to & O\\ \downarrow & & \downarrow \\ T& \to & M.\end{array}$$

The implementation constructs $M$ with a field-by-field structural three-way merge. Compatible additions and modifications are combined. Incompatible edits become MergeConflict variants, and conflicted elements retain their base values until the caller supplies a resolution. apply_resolutions requires a choice of ours or theirs for every reported conflict and then verifies the resulting square.

Combining compatible additions means that two branches adding the same name compatibly contribute one element rather than one each, so $M$ is the pushout quotiented by same-name identification. MergeResult::identified_additions reports every name collapsed this way. Pushouts and merge states what that quotient costs.

The routine verify_pushout checks the generated cocone: both branch vertex maps must be total, every merged vertex must come from a branch, surviving base vertices must remain present, and the two paths from the base must agree on mapped vertices and mapped base edges. A failure returns VcsError::PushoutVerification. This is a cocone check, not a complete runtime proof of the universal property.

verify_pushout_universal provides an additional on-demand check against a caller-supplied alternative cocone. It constructs and checks a mediator on vertices. The current API does not establish edge-level factorization, and ordinary merge does not call this verifier. Pushouts and merge states the distinction formally.

Merge also computes a pullback of theory presentations derived from the base-to-branch diffs. The resulting PullbackOverlap is diagnostic metadata in MergeResult; the field-by-field merge does not use it to decide whether additions are identical or conflicting. If pullback construction fails, the result stores a pullback_error and the CLI reports it. The failure is not interpreted as an empty overlap.

Data associated with history

Commits may reference data sets and migration complements. During a committed merge, data from both parents is lifted to the merged schema, fresh complement objects are recorded, and duplicate migrated data sets are removed. Rebase and cherry-pick similarly lift the replayed commit’s data and call verify_square. Despite its name, that function checks one necessary condition: it migrates the lifted data backward through the saved complement and requires recovery of the original data. This is GetPut for the vertical migration, or the square condition with an identity horizontal edge. It does not compare the two paths around a general data-migration square. These operations follow the schema-evolution account of migrations connected by lenses in Cambria [Litt et al. (2020); Litt et al. (2021)].

Ordinary commit records data that was staged for that commit; it does not automatically copy or migrate all data from the previous commit. Amend preserves existing data identifiers unless the caller stages replacements. A schema change made through either operation thus does not by itself imply that associated data was transformed.

Related work

The categorical account of patches and merge also includes homotopical patch theory (Angiuli et al. 2014) and Darcs (Roundy 2005). Work on schema evolution includes the PRISM workbench and its schema-modification operators (Curino et al. 2008). panproto combines these ideas with content-addressed storage for protocols, schemas, data, migrations, and complements. Related work gives the broader comparison.

See also

• Init and commit for the practical workflow.
• Branch and merge for conflict handling.
• Bridge to git for using panproto-vcs alongside git.
• Pushouts and merge for the formal model.
• What panproto verifies for merge-time checks.