panproto

panproto compares schema versions, constructs migrations, and applies those migrations to data. Your first diff introduces that workflow with two ATProto Lexicon documents and the structural diff between them.

Choose a path

Choose a path based on the work you need to do:

The vocabulary in plain terms introduces unfamiliar terms. The glossary records their reference definitions.

Find the kind of answer you need

The book follows the four-part Diátaxis structure:

Begin with a tutorial if you need both context and a worked sequence. Use reference pages when you already know the operation and need its exact contract.

Tutorials

Begin with a structural diff. The remaining tutorials extend the same User example from a schema to a migration, a version history, and a conversion between protocols.

Follow the beginner path in order:

1. Your first diff compares two ATProto Lexicon documents from the command line. This is the quick success path.
2. Your first schema builds and validates the same model with the TypeScript SDK.
3. Your first migration renames a field, converts a record, and checks the reverse trip.

The next two tutorials branch from that foundation. Schema version control basics is the intermediate path for commits, branches, and structural merge. Cross-protocol translation is the advanced path for an explicit conversion between schemas registered under different protocols.

Tutorials are learning-oriented: each leaves you with a runnable result and explains only the concepts needed to produce it. The how-to guides collect task-specific procedures, the reference records the complete interfaces, and the explanation chapters develop the theory behind the commands.

Your first diff

This tutorial compares two ATProto Lexicon documents and reports one removed field and one added field.

You will create two versions of a User record and run one structural diff. The inputs remain ordinary Lexicon JSON rather than panproto’s internal schema representation.

Prerequisite

Install the schema binary by following Install the CLI, then confirm that schema --version succeeds.

Create two versions

The following block creates a fresh directory, a small manifest that identifies the document protocol, and both input files:

mkdir -p panproto-first-diff
cd panproto-first-diff

cat > panproto.toml <<'EOF'
[workspace]
name = "first-diff"

[[package]]
name = "lexicons"
path = "."
protocol = "atproto"
EOF

cat > user-v1.json <<'EOF'
{
  "lexicon": 1,
  "id": "com.example.user",
  "defs": {
    "main": {
      "type": "record",
      "key": "tid",
      "record": {
        "type": "object",
        "properties": {
          "name": { "type": "string" },
          "age": { "type": "integer" }
        }
      }
    }
  }
}
EOF

cat > user-v2.json <<'EOF'
{
  "lexicon": 1,
  "id": "com.example.user",
  "defs": {
    "main": {
      "type": "record",
      "key": "tid",
      "record": {
        "type": "object",
        "properties": {
          "name": { "type": "string" },
          "years": { "type": "integer" }
        }
      }
    }
  }
}
EOF

Listing 2.1: A manifest and two complete Lexicon inputs for the first structural diff.

The two files differ by one field name: age became years.

Run the diff

From panproto-first-diff/, run:

schema diff user-v1.json user-v2.json

The command uses panproto.toml to select the ATProto document parser, then compares the resulting schema graphs. Its report includes a removed com.example.user:body.age vertex and an added com.example.user:body.years vertex, together with the corresponding property edges. That report establishes the structural removal/addition pair. The rename interpretation requires the second pass below.

Rename detection is a second pass over that structural result:

schema diff user-v1.json user-v2.json --detect-renames

If a removed and added element clear the detector’s similarity threshold, the command adds them to a Detected renames section with confidence scores. This score is evidence for a possible correspondence. Your first migration later records the correspondence explicitly.

For a compact count rather than the element-by-element report, run:

schema diff user-v1.json user-v2.json --stat

The diff is structural in a precise sense: panproto compares parsed vertices, edges, and constraints rather than changed lines. The shared diff loader also accepts panproto schema JSON, source files supported by the tree-sitter registry, and manifest-backed directories.

Next

Your first schema builds the same User model through the SDK and validates records against it. If the command line is your main interface, Schema version control basics turns these source files into commits and branches. The vocabulary in plain terms defines vertex, edge, migration, and lens when you are ready for those names.

Your first schema

This tutorial builds a small User schema, parses two records, and reports a missing required field.

The walkthrough uses the TypeScript SDK. The Python and Rust how-to guides present the same construction through their native APIs.

Set up the project

Node.js 20 or later is required by @panproto/core. Create a project and install the SDK plus tsx, which runs the TypeScript file directly:

mkdir -p my-first-schema/src
cd my-first-schema
npm init -y
npm install @panproto/core tsx

Build and exercise the schema

Create src/main.ts with the complete program below:

import { Panproto } from '@panproto/core';

const p = await Panproto.init();
const atproto = p.protocol('atproto');

const schema = atproto.schema()
  .vertex('user', 'object')
  .vertex('user.name', 'string')
  .vertex('user.age', 'integer')
  .edge('user', 'user.name', 'prop', { name: 'name' })
  .edge('user', 'user.age', 'prop', { name: 'age' })
  .required('user', [
    { src: 'user', tgt: 'user.name', kind: 'prop', name: 'name' },
  ])
  .build();

const alice = p.parseJson(schema, JSON.stringify({ name: 'Alice', age: 30 }));
const missingName = p.parseJson(schema, JSON.stringify({ age: 30 }));

console.log('Alice:', alice.validate());
console.log('Missing name:', missingName.validate());
console.log('JSON:', new TextDecoder().decode(alice.toJson()));

schema[Symbol.dispose]();
p[Symbol.dispose]();

Listing 3.1: A complete schema construction and required-field check.

Run it:

npx tsx src/main.ts

The first validation passes, the second reports a missing name edge, and the final line emits Alice as JSON. The exact error includes an internal node identifier, but the stable part of the output is:

Alice: { isValid: true, errors: [] }
Missing name: { isValid: false, errors: [ 'MissingRequiredEdge { ... }' ] }
JSON: {"age":30,"name":"Alice"}

Read the program from the outside in

The atproto protocol supplies the permitted vertex kinds and edge rules. From those rules, the program builds a schema with one object vertex, two value vertices, and two property edges, then parses two instances against it. validate() checks those records, including the required-edge condition used here.

SchemaBuilder is immutable in the TypeScript SDK: every call to vertex, edge, or required returns a new builder. build() sends the accumulated operations to the WebAssembly engine and returns a BuiltSchema. The SDK root and the built schema own WebAssembly handles, which is why the program disposes them explicitly. Instance stores encoded bytes rather than a WebAssembly handle and has no Symbol.dispose method.

Next

Your first migration evolves this schema by renaming age to years and moves Alice forward without losing the original record. Define a schema from TypeScript covers additional builder operations, while Schemas as theories explains why panproto represents a schema as a graph.

Your first migration

A structural diff records that age disappeared and years appeared. A migration adds the missing information: those two fields correspond. This tutorial declares that correspondence, checks it, converts Alice, and asserts that the reverse trip restores the original record.

Continue in the my-first-schema/ project from Your first schema.

Build both schemas and the mapping

Create src/migration.ts:

import assert from 'node:assert/strict';
import { Panproto } from '@panproto/core';

const p = await Panproto.init();
const atproto = p.protocol('atproto');

function userSchema(numericField: 'age' | 'years') {
  return atproto.schema()
    .vertex('user', 'object')
    .vertex('user.name', 'string')
    .vertex(`user.${numericField}`, 'integer')
    .edge('user', 'user.name', 'prop', { name: 'name' })
    .edge('user', `user.${numericField}`, 'prop', { name: numericField })
    .required('user', [
      { src: 'user', tgt: 'user.name', kind: 'prop', name: 'name' },
    ])
    .build();
}

const v1 = userSchema('age');
const v2 = userSchema('years');

const mapping = p.migration(v1, v2)
  .map('user', 'user')
  .map('user.name', 'user.name')
  .map('user.age', 'user.years')
  .mapEdge(
    { src: 'user', tgt: 'user.name', kind: 'prop', name: 'name' },
    { src: 'user', tgt: 'user.name', kind: 'prop', name: 'name' },
  )
  .mapEdge(
    { src: 'user', tgt: 'user.age', kind: 'prop', name: 'age' },
    { src: 'user', tgt: 'user.years', kind: 'prop', name: 'years' },
  );

const existence = p.checkExistence(v1, v2, mapping);
if (!existence.valid) {
  throw new Error(JSON.stringify(existence.errors));
}

const compatibility = p.diffFull(v1, v2).classify(atproto);
const migration = mapping.compile();
const original = { name: 'Alice', age: 30 };
const converted = migration.liftJson(original, 'user');
const { view, complement } = migration.getJson(original, 'user');
const restored = migration.putJson(view, complement, 'user');

assert.deepEqual(restored, original);
console.log('existence valid?', existence.valid);
console.log('compatible?', compatibility.isCompatible);
console.log('converted:', converted);
console.log('round trip:', restored);

migration[Symbol.dispose]();
v1[Symbol.dispose]();
v2[Symbol.dispose]();
p[Symbol.dispose]();

Listing 4.1: A checked field rename with forward and reverse data conversion.

Run the program:

npx tsx src/migration.ts

The expected output is:

existence valid? true
compatible? false
converted: { name: 'Alice', years: 30 }
round trip: { age: 30, name: 'Alice' }

What the checks establish

The structural classifier reports incompatibility because it sees a removed age field and an added years field. It does not consult the explicit migration. Every required target edge nevertheless has a source, so existence checking passes and compile() can produce the migration. Round-trip behavior is checked separately: getJson() produces the view and an opaque complement, and putJson() uses both to restore the source record. The assert.deepEqual call checks that result structurally, so JSON object key order does not affect it.

Next

Schema version control basics stores the v1 and v2 schemas as history. Cross-protocol translation carries the explicit-mapping pattern across two registered protocols. For computed field values rather than a rename, continue with Apply field transforms.

Schema version control basics

This tutorial uses the schema CLI to commit a TypeScript interface, create a feature branch, and merge the branch into main.

Prerequisite

Install the schema binary by following Install the CLI. The commands below create a new vcs-tutorial/ directory.

Commit the first version

Create the repository and its first source file:

mkdir -p vcs-tutorial/src
cd vcs-tutorial
schema init

cat > src/user.ts <<'EOF'
export interface User {
  name: string;
  age: number;
}
EOF

schema add src/user.ts
schema commit -m "v1 user schema"
schema log --oneline

Listing 5.1: Initializing a repository and committing a parsed TypeScript schema.

schema add parses src/user.ts through the tree-sitter registry and stages the resulting schema graph. The commit stores that graph under .panproto/. The source file remains an ordinary TypeScript file. Run schema add from the repository root so the command can find .panproto/.

Commit the rename

Replace the file with v2, inspect the staged diff, and commit it:

cat > src/user.ts <<'EOF'
export interface User {
  name: string;
  years: number;
  email: string;
}
EOF

schema add src/user.ts
schema diff --staged
schema commit -m "rename age and add email"
schema log --oneline

Listing 5.2: Staging and committing the second schema state.

The staged diff compares schema structure rather than source lines. Full-AST parsers also preserve syntax-level structure needed for source round trips, so a source edit may produce more graph changes than the two interface fields alone suggest.

Branch and merge

Create and switch to a feature branch, add handle, then merge the branch into main:

schema checkout -b feature/handle

cat > src/user.ts <<'EOF'
export interface User {
  name: string;
  years: number;
  email: string;
  handle: string;
}
EOF

schema add src/user.ts
schema commit -m "add handle"
schema checkout main
schema merge feature/handle
schema log --oneline

Listing 5.3: Creating a feature branch and merging it into main.

main has not moved since the branch was created, so this merge is a fast-forward. The command reports Merge successful. and moves the main ref to the feature commit.

There is one operational difference from git: schema checkout moves the schema-history ref but does not rewrite src/user.ts. Panproto stores and merges parsed schemas. An editor, build system, or explicit emit step remains responsible for working-source files. schema log --graph currently accepts --graph but renders the ordinary log, so the examples use --oneline.

Next

The schema version control how-to covers non-fast-forward merges, data versioning, and the git bridge. Schema version control semantics describes the three-way structural merge and its commuting-cocone check. Pushouts and merge gives the categorical comparison and its limits.

Cross-protocol translation

A migration can connect schemas registered under different protocols when their relevant structure agrees. This tutorial converts a User record from a JSON Schema graph to an OpenAPI schema graph by mapping each object and property explicitly. It is the advanced continuation of Your first migration.

The example is deliberately narrow. JSON Schema and OpenAPI use compatible object, scalar, and property structure in this case. The TypeScript existence check selects the source schema’s registered protocol, so this example does not establish general cross-protocol checking. Protocol pairs with different structural rules require a repository-level bridge. Translate across protocols records the current boundary.

Build both endpoints

Continue in the my-first-schema/ project, where @panproto/core and tsx are already installed. Create src/cross.ts:

import assert from 'node:assert/strict';
import { Panproto } from '@panproto/core';

const p = await Panproto.init();

// Register the source protocol before running its existence check.
p.protocol('json-schema');
const openapi = p.protocol('openapi');

const source = p.parseSchemaDocument('json-schema', {
  title: 'User',
  type: 'object',
  properties: {
    name: { type: 'string' },
    age: { type: 'integer' },
  },
  required: ['name'],
});

const target = openapi.schema()
  .vertex('user', 'object')
  .vertex('user.displayName', 'string')
  .vertex('user.years', 'integer')
  .edge('user', 'user.displayName', 'prop', { name: 'displayName' })
  .edge('user', 'user.years', 'prop', { name: 'years' })
  .build();

const mapping = p.migration(source, target)
  .map('root', 'user')
  .map('root.name', 'user.displayName')
  .map('root.age', 'user.years')
  .mapEdge(
    { src: 'root', tgt: 'root.name', kind: 'prop', name: 'name' },
    {
      src: 'user',
      tgt: 'user.displayName',
      kind: 'prop',
      name: 'displayName',
    },
  )
  .mapEdge(
    { src: 'root', tgt: 'root.age', kind: 'prop', name: 'age' },
    { src: 'user', tgt: 'user.years', kind: 'prop', name: 'years' },
  );

const existence = p.checkExistence(source, target, mapping);
if (!existence.valid) {
  throw new Error(JSON.stringify(existence.errors));
}

const migration = mapping.compile();
const converted = migration.liftJson({ name: 'Alice', age: 30 }, 'root');

assert.deepEqual(converted, { displayName: 'Alice', years: 30 });
console.log('existence valid?', existence.valid);
console.log('converted:', converted);

migration[Symbol.dispose]();
source[Symbol.dispose]();
target[Symbol.dispose]();
p[Symbol.dispose]();

Listing 6.1: An explicit forward migration from a JSON Schema graph to an OpenAPI schema graph.

Run the program:

npx tsx src/cross.ts

The output is:

existence valid? true
converted: { displayName: 'Alice', years: 30 }

What crossed the protocol boundary

parseSchemaDocument('json-schema', ...) uses the JSON Schema document parser and produces a schema rooted at root. The target is built against the registered openapi protocol. The migration maps vertices and edges across those two schema handles, and liftJson() emits the target field names.

The existence report checks the explicit mapping with the source schema’s registered protocol. The assert.deepEqual call separately checks this forward result. Neither check proves that arbitrary JSON Schema and OpenAPI documents can be translated, and the example does not establish a reverse trip.

The target is an OpenAPI schema graph, not a complete emitted OpenAPI document. Document emission and constraint translation add structure beyond this two-field example.

Continue on the advanced path

Translate across protocols covers the operational choices for larger pairs, and Write lenses in the lens DSL covers hand-authored bridges. Composing protocols by colimit explains how shared theories are constructed. For the formal account, continue to Theory DSL: denotational semantics.

How-to guides

How-to guides assume that the goal is settled and the missing piece is a procedure. A first encounter with panproto belongs in the tutorials; an exact flag, signature, or grammar belongs in the reference.

First working path

A reader starting from an existing schema file can follow one short sequence: install a surface, define or load a schema, construct a migration with the migration guide, and convert data. Each guide includes a verification step before the next operation changes data or repository state.

Intermediate entry points

These guides assume that you can already load and validate a schema.

Advanced entry points

These guides cover reusable transformations, language tooling, and protocol extension.

Tasks by area

Setup and schema creation are collected under Install panproto and Define a schema. Migration work begins with Build a migration and extends through field transforms, lenses, protolenses, dependent optics, and the lens DSL.

Data tasks cover conversion, queries, format-preserving round trips, full-AST parsing, and schema decoration. Repository tasks are grouped under Schema version control and Continuous integration; Translate across protocols and Build a custom protocol cover extension across protocol boundaries.

Install panproto

panproto has six user-facing distributions. Install only the command-line or language surface that the project uses.

The CLI and SDK packages are independent; installing one does not install the others.

Every release attaches checksums, a software bill of materials, and build attestations for its binary archives. Verify a release artifact covers checking them.

See also

• Reference: configuration for the panproto.toml manifest.
• Tutorial: your first schema once installed.

Install the CLI

The CLI is a single binary called schema. It is the entry point for the panproto-cli crate.

Prerequisites

A POSIX shell on macOS or Linux, or PowerShell on Windows. The binary releases cover the targets listed in the repository’s cargo-dist configuration. Other targets require a Rust toolchain.

Install

Homebrew (macOS, Linux)

brew install panproto/tap/schema

Shell installer (macOS, Linux, WSL)

curl --proto '=https' -LsSf https://github.com/panproto/panproto/releases/latest/download/panproto-cli-installer.sh | sh

PowerShell installer (Windows)

powershell -ExecutionPolicy ByPass -c "irm https://github.com/panproto/panproto/releases/latest/download/panproto-cli-installer.ps1 | iex"

From source

cargo install panproto-cli

Requires a Rust toolchain (1.85 or newer).

Verification

schema --version

prints the installed version. The full subcommand list is at Reference: CLI, or schema --help.

Common mistakes

• Installing through cargo install without an up-to-date toolchain. panproto requires Rust 1.85 or later.
• Mixing the Homebrew install with a from-source install on the same machine: only one schema ends up first on PATH.

See also

• Tutorial: your first schema.
• Reference: CLI.

Install the Rust SDK

Prerequisites

A Rust toolchain at edition 2024 (toolchain 1.85+).

Install

# Cargo.toml
[dependencies]
panproto-core = "0.72"

The facade has no default features. Enable full-parse, project, git, or tree-sitter only when the application uses that surface; project also enables full-parse, and git enables both.

Verification

use panproto_core::protocols::atproto;
use panproto_core::schema::SchemaBuilder;

fn main() -> Result<(), Box<dyn std::error::Error>> {
    let proto = atproto::protocol();
    let schema = SchemaBuilder::new(&proto)
        .vertex("root", "record", Some("app.example.root"))?
        .entry("root")
        .build()?;
    println!("built {} vertex(es)", schema.vertices.len());
    Ok(())
}

cargo run builds and links against the panproto facade.

Common mistakes

• Pinning a stale toolchain. panproto-core requires Rust 1.85 or later.
• Depending on lower-level crates (panproto-schema, panproto-mig, …) directly without a strong reason. The facade re-exports the canonical surface; reach past it only when you need an internal API.

See also

• Reference: Rust SDK for feature flags and crate selection.
• Define a schema from Rust.
• Crate map.

Install the TypeScript SDK

Prerequisites

Node 20 or newer. A package manager (npm, pnpm, or yarn). A bundler with WASM support if targeting the browser (Vite, Rollup, esbuild, webpack 5+).

Install

npm install @panproto/core
# or
pnpm add @panproto/core
# or
yarn add @panproto/core

Verification

import { Panproto } from '@panproto/core';

const p = await Panproto.init();
console.log(p.listProtocols());

Panproto.init() loads the WASM module and returns the top-level handle. Calling p.listProtocols() enumerates the built-in protocols and confirms the binding is wired up.

Common mistakes

• Forgetting to await Panproto.init(). The WASM load is asynchronous; using the handle before init resolves throws.
• Using a bundler without WebAssembly asset support. Configure the bundler to copy and load the package’s .wasm asset.
• Running under Node earlier than 20. The package metadata requires Node 20 or later.

See also

• Reference: TypeScript SDK.
• Define a schema from TypeScript.
• Tutorial: your first schema.

Install the Python SDK

Prerequisites

Python 3.13 or newer. A virtual environment is recommended.

Install

pip install panproto

The wheel includes native PyO3 bindings and the core tree-sitter grammar group. Additional grammar packs are installed separately:

pip install panproto-grammars-functional   # Haskell, OCaml, Elm, Erlang, Elixir, ...
pip install panproto-grammars-web          # HTML, CSS, Vue, Svelte, ...
pip install panproto-grammars-all          # umbrella package

The full table of packs is in Reference: Python SDK.

Verification

import panproto

print(panproto.list_builtin_protocols()[:3])

The native module loads at import time (no async wrapper, unlike the TypeScript SDK). Listing a few of the built-in protocols confirms the linkage. The full top-level surface is in Reference: Python SDK.

Common mistakes

• Running under Python earlier than 3.13. The package metadata requires Python 3.13 or later.
• Importing each grammar pack manually. AstParserRegistry discovers installed packs through their panproto.grammars entry points.

See also

• Reference: Python SDK.
• Define a schema from Python.
• Tutorial: your first schema.

Install the Haskell SDK

Prerequisites

GHC 9.12.2 and Cabal (the binding builds with cabal-version: 3.8). The FFI backend also needs a Rust toolchain when building libpanproto_c from source; rustup is recommended.

Install

The panproto package currently lives under bindings/haskell/; build it from the repository. The default rust flag links the FFI backend against libpanproto_c, so the library has to be staged first. There are two ways to get it.

Build from source

bootstrap/dev-link.sh builds panproto-c from the workspace with cargo build -p panproto-c --release, compiles the panproto-glue C layer into a standalone libpanproto_glue.a, and stages both under bindings/haskell/.panproto-c/. It then writes a gitignored cabal.project.local carrying the absolute lib and include paths (cabal’s relative extra-lib-dirs propagate into ghc-pkg’s registration metadata, which rejects anything but absolute paths).

git clone https://github.com/panproto/panproto.git
cd panproto/bindings/haskell
./bootstrap/dev-link.sh                # builds panproto-c, stages libs
cabal build
cabal test

Run dev-link.sh again after every change to panproto-c, to the C glue, or to the workspace Cargo.toml.

Prebuilt binaries

bootstrap/fetch-bindist.sh [version] downloads the prebuilt libpanproto_c for the host platform from the corresponding GitHub Release (it detects aarch64-apple-darwin, x86_64-apple-darwin, x86_64-unknown-linux-gnu, and aarch64-unknown-linux-gnu), rebuilds the C glue against the fetched header, and writes the same cabal.project.local. No Rust toolchain is needed on this path.

git clone https://github.com/panproto/panproto.git
cd panproto/bindings/haskell
./bootstrap/fetch-bindist.sh v0.72.0   # pass the release tag that matches this checkout
cabal build
cabal test

Pass the release tag explicitly. The script’s fallback tag can lag the package version in a development checkout.

Native-only (no FFI)

For the pure-Haskell subset, disable the foreign-function interface (FFI) backend. This build needs no libpanproto_c and no Rust toolchain:

cabal build -f-rust

Verification

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DuplicateRecordFields #-}

import qualified Panproto.Schema as S

main :: IO ()
main = do
    let s = S.buildSchema "geojson" $ do
                S.vertex S.Vertex {S.id = "post", S.kind = "record", S.nsid = Nothing}
    print (S.vertexCount s)

Place the example in an executable component or load it in cabal repl. Building a one-vertex structured schema and printing its vertex count exercises the pure value algebra without touching the engine, so the example also works with the FFI backend disabled.

Common mistakes

• Some Python distributions, including Anaconda, put an older ld on PATH. On macOS arm64, that linker cannot read GHC’s response-file syntax and reports ld: file not found: @<tmp>/ghc_tmp_*.rsp. dev-link.sh warns when ld is not the system linker. Prepend /usr/bin to PATH and retry.
• Skipping the bootstrap step on a default (rust-flag) build. Without dev-link.sh or fetch-bindist.sh, no cabal.project.local exists, extra-lib-dirs is unset, and the link fails on the missing libpanproto_c.
• A relative extra-lib-dirs. The path in cabal.project.local is absolute by design; ghc-pkg refuses a relative one during package registration.

See also

• Reference: Haskell SDK for the capability classes, the effect layer, and the cabal flags.
• Crate map for panproto-c and the rest of the workspace.

Install the Swift SDK

Prerequisites

Swift 6.1 or later. The package manifest uses Swift tools 6.1 and Swift 6 language mode.

Building libpanproto_c from source additionally needs a Rust toolchain; rustup is recommended. The prebuilt path below needs neither Rust nor a workspace checkout.

Install

The package is not yet on a registry; it lives at bindings/swift/ in the repository. Engine-backed products link libpanproto_c, the C application binary interface exposed by the panproto-c crate. Stage that library before building an engine-backed target. PanprotoStructural is a pure Swift product and does not call the engine.

Build from source

bootstrap/dev-link.sh runs cargo build -p panproto-c --release, stages the resulting library and header under bindings/swift/.panproto-c/, and syncs the vendored copy of panproto.h that the package compiles against. Package.swift looks in .panproto-c/lib by default, so nothing else needs configuring.

git clone https://github.com/panproto/panproto.git
cd panproto/bindings/swift
./bootstrap/dev-link.sh
swift build
swift test

Run dev-link.sh again after every change to panproto-c or the workspace Cargo.toml. Set PANPROTO_C_LIB_DIR to stage somewhere else.

Prebuilt binaries

bootstrap/fetch-bindist.sh [version] [variant] downloads the prebuilt library for the host platform from the corresponding GitHub Release. It detects aarch64-apple-darwin, x86_64-apple-darwin, x86_64-unknown-linux-gnu, and aarch64-unknown-linux-gnu. Both arguments are optional and are read by shape rather than by position, so either can be given alone: the version defaults to whatever the checkout declares, and the variant (default or full, also spelled --default and --full) defaults to default.

cd panproto/bindings/swift
./bootstrap/fetch-bindist.sh
swift build

XCFramework

iOS builds go through the XCFramework, which carries a macOS-universal slice, an iOS device slice, and a universal simulator slice, together with the headers and a module map.

cd panproto/bindings/swift
./bootstrap/fetch-bindist.sh --xcframework
PANPROTO_SWIFT_XCFRAMEWORK=.panproto-c/panproto_c.xcframework swift build

To depend on the package from another project, point PANPROTO_SWIFT_XCFRAMEWORK_URL and PANPROTO_SWIFT_XCFRAMEWORK_CHECKSUM at the published artifact and its checksum, both of which the release attaches. That mode adds no linker flags of its own, which is what makes the package usable as a dependency; the dev-link.sh mode passes an unsafe -L flag and is for building the package directly.

Products

Feature-gated tiers

The default libpanproto_c omits the parse, project, and git tiers. Using one of those tiers requires a library built with the matching Cargo features and a Swift build that compiles the gated shims:

PANPROTO_C_FEATURES=full ./bootstrap/dev-link.sh
swift build --traits PANPROTO_PARSE,PANPROTO_PROJECT,PANPROTO_GIT

Each tier is a package trait, and a trait defines a compilation condition of its own name, which is what the #if PANPROTO_PARSE blocks in the gated sources read.

The three gated products exist in the package graph either way, so a build that omits the features still resolves; their modules are simply empty. On the prebuilt path, fetch the full variant:

./bootstrap/fetch-bindist.sh full
swift build --traits PANPROTO_PARSE,PANPROTO_PROJECT,PANPROTO_GIT

Verification

import Foundation
import Panproto
import PanprotoStructural

let names = try await ProtocolHandle.builtinNames()
print(names.count, "builtin protocols")

let atproto = try await ProtocolHandle.builtin("atproto")
let lexicon = try Data(contentsOf: URL(fileURLWithPath: "app.bsky.feed.post.json"))
let schema = try await SchemaHandle.parseAtprotoLexicon(lexicon)
let value = try await schema.schema()
print(value.protocolName, value.vertexCount, "vertices")

let messages = try await schema.violations(against: atproto)
print(messages.isEmpty ? "valid" : messages.joined(separator: "\n"))

Engine calls run on the @PanprotoEngine global actor, which is pinned to one thread. Release long-lived handles explicitly when their work is complete.

Verify a release artifact

Every binary archive attached to a panproto release carries two independent claims: a checksum, which says the bytes are the ones that were built, and an attestation, which says which workflow built them and from which source revision. The first catches a truncated or corrupted download. Only the second distinguishes an archive panproto built from one someone else assembled and named the same thing.

Checksums

Each release attaches a SHA256SUMS file covering every .tar.gz and .zip, in the format sha256sum -c reads:

gh release download v0.72.1 --pattern 'panproto-c-*' --pattern 'SHA256SUMS'
sha256sum -c SHA256SUMS

On macOS, shasum -a 256 -c SHA256SUMS.

The Swift XCFramework is verified separately and automatically. Package.swift pins releaseXCFrameworkChecksum, and SwiftPM refuses to resolve if the downloaded artifact does not match, so a consumer adding the package as a dependency gets this check without asking for it.

Attestations

A checksum only says the file matches a hash published beside it. Both come from the same release, so an attacker able to replace one can replace the other. An attestation is signed by the workflow’s own OIDC identity at build time and records the repository, the workflow file, and the commit:

gh attestation verify panproto-c-aarch64-apple-darwin.tar.gz --repo panproto/panproto

This succeeds only for an archive built by this repository’s workflow. It needs no key on your side and no key is stored on ours: signing is keyless, tied to the job’s identity rather than to a secret that could leak.

What is in an archive

Each release also carries panproto-c.cdx.json, a CycloneDX software bill of materials listing every crate the C library was built from, at the versions Cargo.lock pinned. It is itself attested, so the inventory is as verifiable as the binary it describes.

To answer “does this release contain some vulnerable dependency”, read the SBOM rather than rebuilding:

gh release download v0.72.1 --pattern 'panproto-c.cdx.json'
jq -r '.components[] | "\(.name) \(.version)"' panproto-c.cdx.json | sort

Crates, wheels and npm packages

These do not need the steps above. crates.io, PyPI and npm are all published through OIDC Trusted Publishing, so the registry itself records which workflow published each version, and npm additionally carries provenance that npm audit signatures checks. No long-lived publication token exists for any of them.

See also

• Install the CLI for the installer scripts, which verify checksums themselves.
• Install the Swift SDK for the XCFramework pin.

Define a schema

Choose a surface according to where the schema enters the project. The CLI loads and inspects schema files; the five SDKs construct schemas inside an application.

The CLI’s schema-checking commands currently accept panproto’s internal schema JSON and resolve only the atproto protocol. Its shared loaders can parse an ATProto Lexicon when a manifest selects atproto, and its full-AST commands parse supported source files as syntax trees. Use a language SDK’s parseSchemaDocument or parseSchemaSource dispatch for the other external schema languages in the protocol catalog. Start with a language SDK when the application constructs the schema programmatically.

See also

• Reference: protocol catalog for the list of supported protocols.
• Schemas as theories for the model.

Define a schema from the CLI

Prerequisites

The schema binary installed (Install the CLI). A file in panproto’s internal schema JSON format. The current CLI protocol resolver accepts atproto.

The task

Validate an existing schema

schema validate --protocol atproto path/to/schema.json

The command loads panproto schema JSON, checks vertex kinds, edge rules, constraint sorts, required-edge references, and recursion references, then type-checks the registered protocol theories. It exits nonzero if either pass reports an error. It does not parse an ATProto Lexicon or another external schema document at this entry point.

Scaffold from an existing schema

schema scaffold --protocol atproto schemas/post.json

scaffold runs bounded free-model construction over panproto schema JSON and prints sample term assignments. Use --json for machine-readable output, and use --depth and --max-terms to set the bounds. A truncated run is a partial enumeration rather than proof that no other terms exist.

Inspect

schema diff schemas/post-v1.json schemas/post-v2.json

diff reports vertex and edge changes between two schemas. Inside a panproto repository, schema show <ref> resolves a commit, schema, or migration object and prints its contents.

Verification

After validation, run:

schema verify --protocol atproto path/to/schema.json

verify tests assignments for the equations in the registered protocol theories, up to --max-assignments per equation. The current command prints Verification passed even when a theory has type errors or an equation check is incomplete, so use schema validate as the CI gate and inspect the full verify output. A bounded pass is evidence from the checked assignments, not a proof over every possible assignment.

Common mistakes

• Passing an external schema-language document to validate, verify, or scaffold. These commands deserialize panproto’s internal schema JSON. Parse or convert an external document first.
• Running schema validate when you mean schema check (the latter checks a migration, not a schema).

See also

• Reference: CLI for the full subcommand list.
• Tutorial: your first schema.

Define a schema from TypeScript

Prerequisites

@panproto/core installed (Install the TypeScript SDK).

The task

import { Panproto } from '@panproto/core';

const p = await Panproto.init();
const proto = p.protocol('atproto');

const schema = proto.schema()
  .vertex('post', 'record', { nsid: 'app.bsky.feed.post' })
  .vertex('post:body', 'object')
  .vertex('post:body.text', 'string')
  .edge('post', 'post:body', 'record-schema')
  .edge('post:body', 'post:body.text', 'prop', { name: 'text' })
  .build();

p.protocol(name) loads the named protocol. proto.schema() returns an immutable SchemaBuilder: each operation returns a new builder containing the added structure. .build() sends those operations to WebAssembly, where vertex and edge rules are checked, and returns a BuiltSchema handle. Run the separate validation pass below to check constraint sorts and other finished-schema conditions.

Verification

const result = schema.validate(proto);
if (!result.isValid) throw new Error(JSON.stringify(result.issues));

validate(protocol) returns a ValidationResult containing any issues. An empty issue list confirms the schema satisfies the protocol’s edge rules and obj-kinds.

Common mistakes

• Ignoring the builder returned by .vertex() or .edge(). Builders are immutable, so the original value does not acquire the operation.
• Treating .build() as equation verification. It constructs a schema and enforces builder-level checks; schema.validate(proto) is the finished-schema structural validation pass.
• Treating the returned Schema handle as a plain object. It is an opaque handle into the WASM heap; pass it to subsequent SDK calls, do not introspect it directly.

See also

• Reference: TypeScript SDK.
• Build a migration for what to do with the schema next.
• Tutorial: your first schema.

Define a schema from Python

Prerequisites

panproto installed (Install the Python SDK).

The task

import panproto

proto = panproto.get_builtin_protocol("atproto")

b = proto.schema()
b.vertex("user", "object", "app.example.user")
b.vertex("user:name", "string")
b.vertex("user:age", "integer")
b.edge("user", "user:name", "prop", "name")
b.edge("user", "user:age", "prop", "age")
schema = b.build()

panproto.get_builtin_protocol(name) returns the named protocol; .vertex(id, kind, nsid=None) and .edge(src, tgt, kind, name=None) each mutate the SchemaBuilder in place (returning None), and .build() validates and returns a Schema. The TypeScript SDK exposes the same operations as a chainable surface; the Python binding does not.

Call panproto.list_builtin_protocols() to see the registered protocol names. Treat the returned list as the source of truth rather than hard-coding a catalog count.

Verification

issues = schema.validate(proto)
assert not issues, issues

Schema.validate(protocol) returns protocol-level structural validation messages. An empty list means no vertex-kind, edge-rule, constraint-sort, required-edge, or recursion-reference error was found; it does not run equation checking.

Common mistakes

• Chaining the builder calls. The Python SchemaBuilder.vertex(...) / edge(...) / constraint(...) methods mutate in place and return None; hold the builder in a variable and mutate it statement-by-statement, then call .build().
• Using a Python dict where the SDK expects a Schema handle. Conversion is deliberate; to materialize an Instance from bytes against a built Schema, use panproto.IoRegistry().parse(protocol, schema, data).

See also

• Reference: Python SDK.
• Build a migration.
• Tutorial: your first schema.

Define a schema from Rust

Prerequisites

panproto-core in your Cargo.toml (Install the Rust SDK).

The task

use panproto_core::protocols::atproto;
use panproto_core::schema::SchemaBuilder;

fn main() -> Result<(), Box<dyn std::error::Error>> {
    let proto = atproto::protocol();

    let schema = SchemaBuilder::new(&proto)
        .vertex("user", "object", Some("app.example.user"))?
        .vertex("user:name", "string", None)?
        .vertex("user:age", "integer", None)?
        .edge("user", "user:name", "prop", Some("name"))?
        .edge("user", "user:age", "prop", Some("age"))?
        .entry("user")
        .build()?;

    println!("{} vertices, {} edges", schema.vertices.len(), schema.edges.len());
    Ok(())
}

SchemaBuilder::new(&protocol) constructs the builder; each vertex and edge call validates against the protocol’s vertex kinds and edge rules. entry declares a vertex at which an instance may be rooted. build rejects an empty schema or an entry that names no vertex, computes adjacency indexes, and returns an owned Schema. Constraint-sort validation remains a separate pass.

Verification

use panproto_core::schema::{SchemaBuilder, validate};
fn main() -> Result<(), Box<dyn std::error::Error>> {
let proto = panproto_core::protocols::atproto::protocol();
let schema = SchemaBuilder::new(&proto)
    .vertex("user", "object", Some("app.example.user"))?
    .entry("user")
    .build()?;
let errors = validate(&schema, &proto);
assert!(errors.is_empty(), "validation errors: {errors:?}");
Ok(()) }

validate returns a Vec<ValidationError> for protocol-level structural failures such as an unknown vertex kind, invalid edge, unknown constraint sort, or dangling required edge. It does not evaluate theory equations.

Common mistakes

• Reaching past panproto-core to lower-level crates without a reason. The facade re-exports the canonical surface; do not depend on panproto-schema directly unless you need an internal API.
• Assuming build() validates constraints. The builder records constraints without checking their sorts; call validate(&schema, &proto) before using an externally supplied constraint.

See also

• Reference: Rust SDK.
• docs.rs for panproto-core.
• Build a migration.

Define a schema from Haskell

Prerequisites

The panproto package installed and linked against libpanproto_c (Install the Haskell SDK).

The task

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DuplicateRecordFields #-}

import Panproto.Schema (Schema)
import qualified Panproto.Schema as S

postSchema :: Schema
postSchema = S.buildSchema "geojson" $ do
    S.vertex S.Vertex {S.id = "post", S.kind = "record", S.nsid = Nothing}
    S.vertex S.Vertex {S.id = "text", S.kind = "string", S.nsid = Nothing}
    S.vertex S.Vertex {S.id = "title", S.kind = "string", S.nsid = Nothing}
    S.edge S.Edge {S.src = "post", S.tgt = "text", S.kind = "prop", S.name = Just "text"}
    S.edge S.Edge {S.src = "post", S.tgt = "title", S.kind = "prop", S.name = Just "title"}
    S.constraint "title" S.Constraint {S.sort = "maxLength", S.value = "120"}

buildSchema name runs the builder actions in the do block and returns an immutable Schema value. vertex, edge, and constraint add plain Haskell records; no Rust runtime starts during this construction. The protocol name is metadata at this stage, so validation still needs a separate protocol value.

A Schema built this way carries no protocol object of its own. To validate it you pair it with a protocol, which you can take straight from the canonical default with its name set:

{-# LANGUAGE OverloadedStrings #-}

import Panproto.Canonical (CanonicalProtocol (..), defaultProtocol)

geoProtocol :: CanonicalProtocol
geoProtocol = defaultProtocol {name = "geojson"}

fromTheories builds a protocol from explicit schema and instance theories. Use it only when defining a new protocol. Renaming defaultProtocol is enough for this value-level example, but it does not load the GeoJSON rules from the Rust registry.

Verification

Validation runs through the foreign-function interface backend. fromSchema (Proxy @Rust) and fromCanonical (Proxy @Rust) create engine handles; validateSchema returns the protocol-level complaints. An empty list reports that this pass found no structural violations.

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}

import Control.Exception (bracket)
import Data.Proxy (Proxy (..))
import Data.Text (Text)
import Panproto.Class (Rust, ProtocolBackend (..), SchemaBackend (..), SchemaValidate (..))
import Panproto.Rust ()   -- brings the Rust instances into scope

validate :: IO [Text]
validate =
    bracket (fromCanonical (Proxy @Rust) geoProtocol)
            releaseProtocol $ \proto ->
    bracket (fromSchema (Proxy @Rust) postSchema)
            releaseSchema $ \schema ->
        validateSchema schema proto   -- [] means valid

The bracket calls release the slab handles the Rust backend hands back, so the engine’s thread-local allocations are freed once validation returns. To recover the structured Schema from an ingested handle (the round-trip the test suite checks node-for-node), call toSchema on the SchemaRep Rust.

Common mistakes

• Chaining the builder operations as if they returned the schema. vertex, edge, and constraint are SchemaBuilderM () actions sequenced in a do-block; buildSchema returns the Schema, not the individual calls.
• Holding a SchemaRep Rust past its bracket. The Rust representations are u32 slab handles into a thread-local arena; use them inside the bracket and let releaseSchema reclaim them, and do not share a handle across threads.
• Using optional lens-adaptor packages to build structure. Schema construction goes through SchemaBuilderM.

See also

• Reference: Haskell SDK.
• Install the Haskell SDK for the bootstrap scripts and toolchain prerequisites.
• Build a migration.

Define a schema from Swift

Prerequisites

The panproto Swift package, with libpanproto_c staged or pinned (Install the Swift SDK).

The task

Schema in PanprotoStructural is a value. Building one starts nothing, allocates no engine resource, and runs on whatever thread you are already on.

import PanprotoStructural

var post = Schema(protocol: "geojson")
post.addVertex(Vertex(id: "post", kind: "record"))
post.addVertex(Vertex(id: "text", kind: "string"))
post.addVertex(Vertex(id: "title", kind: "string"))
post.addEdge(Edge(src: "post", tgt: "text", kind: "prop", name: "text"))
post.addEdge(Edge(src: "post", tgt: "title", kind: "prop", name: "title"))
post.addConstraint(Constraint(sort: "maxLength", value: "120"), to: "title")
post.addEntry("post")

Every value here is a plain struct. A Vertex carries an id, a kind drawn from the protocol’s recognized vertex kinds, and an optional nsid. An Edge carries its src, tgt, structural kind (prop, item, variant), and an optional name. A Constraint attaches a sort and a value to one vertex, and addEntry declares which vertices an instance may be rooted at.

The three adjacency indices the Rust type precomputes are not stored on the Swift value: they are derivable from the edge set, so they are recomputed on the way to the engine and exposed here as accessors.

for edge in post.outgoingEdges(from: "post") {
    print(edge.name ?? edge.kind, "->", edge.tgt)
}

Validating against a protocol

Validation is engine work, so it needs a handle on each side and it needs an await. SchemaHandle ingests the value; ProtocolHandle.builtin takes a registered codec by name.

import Panproto
import PanprotoStructural

let geojson = try await ProtocolHandle.builtin("geojson")
let handle = try await SchemaHandle.define(post)
let messages = try await handle.violations(against: geojson)

if messages.isEmpty {
    print("valid")
} else {
    for message in messages { print(message) }
}

Both handles free themselves when they go out of scope. Call release() when you want the slab entry back sooner, such as inside a loop over many candidate schemas.

To go the other way, ask a handle for its value:

let roundTripped = try await handle.schema()
precondition(roundTripped.vertexCount == post.vertexCount)

Building through the engine instead

SchemaBuilder accumulates the same operations and compiles them in the engine rather than in Swift, which is what you want when the protocol’s own build rules should be applied as you go rather than checked at the end.

import Panproto

var builder = geojson.schemaBuilder()
builder.vertex("post", kind: "record")
builder.vertex("text", kind: "string")
builder.edge(from: "post", to: "text", kind: "prop", name: "text")
builder.entry("post")

let built = try await builder.build()

Parsing one instead of writing it

Most schemas are not written by hand. An atproto lexicon parses directly:

import Foundation
import Panproto
import PanprotoStructural

let lexicon = try Data(contentsOf: lexiconURL)
let schema = try await SchemaHandle.parseAtprotoLexicon(lexicon)
print(try await schema.schema().vertexCount, "vertices")

Next steps

• Build a migration between two versions of this schema.
• Swift SDK reference for the engine actor, the handle taxonomy, and the error hierarchy.

Build a migration

A migration maps vertices and edges in a source schema to a target schema. Build or derive the mapping, check it, then apply it to representative data.

Prerequisites

Two panproto schema JSON files and the schema CLI. The current CLI protocol resolver supports atproto. The TypeScript SDK can check a narrow explicit mapping between two protocol-tagged schema handles, with the qualifications in Translate across protocols.

Derive a mapping

Inspect the inferred span first:

schema auto-migrate schemas/v1.json schemas/v2.json

Review its coverage and vertex map. Then save the right leg as a migration:

schema auto-migrate schemas/v1.json schemas/v2.json --monic --json \
  > migrations/v1-to-v2.json

--monic prevents two apex vertices from mapping to the same target vertex. Omit it only when the contraction is intentional and a separate value-level rule will combine the values.

The generated file maps the matched apex into v2, not necessarily all of v1. Use --total if partial coverage is unacceptable:

schema auto-migrate schemas/v1.json schemas/v2.json --total --json \
  > migrations/v1-to-v2.json

Check the mapping

schema check \
  --src schemas/v1.json \
  --tgt schemas/v2.json \
  --mapping migrations/v1-to-v2.json \
  --typecheck

The existence check validates the migration against the source, target, and protocol theories. --typecheck also validates the induced GAT morphism. The command exits non-zero when either enabled check reports an error.

A passing check does not establish source-wide coverage. The mapping may omit unmatched source vertices, so retain the auto-migrate report or require --total when all source data must move.

Apply the migration

schema lift \
  --migration migrations/v1-to-v2.json \
  --src-schema schemas/v1.json \
  --tgt-schema schemas/v2.json \
  data/user.json > data/user-v2.json

The default direction is restrict and the default instance type is wtype. In this command, restrict reads a source-shaped record, follows the compiled source-to-target migration, retains the part represented by mapped vertices, and serializes that result with the target schema. It is not the categorical precomposition functor (\Delta_F), which has the opposite instance-level direction, from a target instance to a source instance. Both other modes also run source to target. sigma uses the total extension path. For functor instances, pi forms Cartesian products from the values associated with each target vertex (its fiber). For W-type instances, pi only accepts vertex-injective mappings and relabels the tree; it does not construct the general right Kan extension. The vocabulary in plain terms gives the categorical directions. The command infers the record root from the migration’s mapped source vertices; a mapping with no vertex entries cannot be applied.

Build a mapping in TypeScript

const builder = p
  .migration(srcSchema, tgtSchema)
  .map('user', 'user')
  .map('user:name', 'user:display_name');

const report = p.checkExistence(srcSchema, tgtSchema, builder);
if (!report.valid) throw new Error(JSON.stringify(report.errors));

using migration = builder.compile();
const migrated = migration.liftJson(oldRecord, 'user');

MigrationBuilder supports vertex maps, edge maps, and contraction resolvers. Per-field expressions are not part of this builder; use the field-transform guide for the supported TypeScript lens-document route.

Classify compatibility separately

Migration validity and compatibility answer different questions. To classify the schema change for CI, run:

schema compat schemas/v1.json schemas/v2.json --protocol atproto

The command exits 0 when it finds no breaking change, 1 for a breaking change, and 2 for a usage or load error. Add --format json for machine-readable output.

Limitations

• schema check does not measure how much of the source schema is mapped.
• Automatic alignment ranks candidates; it does not certify that the selected correspondence matches domain intent. Review every generated map.
• A vertex map cannot split one value across several targets or compute a new value. Those operations require field transforms.
• schema lift --direction restrict is named after panproto-mig’s surviving-fragment operation. Do not identify it with panproto-inst::adjunction::w_delta or f_delta, which implement target-to-source precomposition.

See also

• Find a span between two schemas for coverage and search constraints.
• Apply field transforms for value-level rewrites.
• Migrations as morphisms for the model.
• CLI reference for all migration commands.

Find a span between two schemas

Use a span search when a source schema may have only a partial correspondence in a target schema. The result contains an apex, which is the matched part of the source, and a migration from that apex into the target.

Prerequisites

The schema CLI or the Rust panproto-mig crate. Both schemas must name a registered protocol.

Search from the CLI

schema auto-migrate schemas/v1.json schemas/v2.json

The report includes the apex size, vertex coverage, quality, quality bounds, and the right-leg vertex and edge maps. The default command fails when the apex is empty. Add --span when an empty overlap is a useful answer:

schema auto-migrate schemas/v1.json schemas/v2.json --span

Use --total when every source vertex and every mappable source edge must be covered:

schema auto-migrate schemas/v1.json schemas/v2.json --total

--total and --span conflict. A partial optimal span does not show that no total morphism exists, so --total runs the total-morphism search when the first result is partial. It exits non-zero only when that search finds no total morphism or cannot run.

Add --monic when distinct apex vertices must map to distinct target vertices. This constrains vertex injectivity only; it does not promise an injective edge map.

Save the mapping

schema auto-migrate schemas/v1.json schemas/v2.json --json \
  > migrations/v1-to-v2.json

JSON output is the span’s right leg, serialized as a Migration. Its source is the apex. Since apex vertices reuse source identifiers, the map keys are still names from v1; unmatched source vertices are absent. The JSON does not include coverage, quality, or the certificate, so review the human report before saving the mapping.

If the mapping will be lifted directly, combine --json with --monic to avoid a vertex contraction that has no built-in rule for combining two source values:

schema auto-migrate schemas/v1.json schemas/v2.json --monic --json \
  > migrations/v1-to-v2.json

Search from Rust

find_span always returns a span when the search runs. Schemas with no common vertex produce an empty apex.

#![allow(unused)]
fn main() {
use panproto_mig::{SearchOptions, find_span};
use panproto_schema::{Protocol, Schema};

fn search(
    source: &Schema,
    target: &Schema,
    protocol: &Protocol,
) -> Result<(), panproto_mig::SpanError> {
    let options = SearchOptions {
        monic: true,
        ..SearchOptions::default()
    };
    let span = find_span(source, target, protocol, &options)?;

    println!("coverage: {:.1}%", span.apex_coverage * 100.0);
    println!("quality bounds: {:?}", span.quality_bounds);
    println!("total: {}", span.is_total());
    println!("vertex map: {:?}", span.right.vertex_map);
    Ok(())
}
}

Set SearchOptions::hard_pins only for correspondences the search may not reconsider. An incompatible pin can force that source vertex out of the apex. Soft evidence belongs in SpanSearch::with_evidence instead.

Read the result

apex_coverage counts matched source vertices. SchemaSpan::is_total() also checks the relevant source edges, so coverage of 1.0 does not by itself establish totality.

quality ranks alternatives for one fixed source schema. Do not compare it across different source schemas. Equal lower and upper quality bounds mean that the search proved the returned score optimal; otherwise, the interval records the unresolved range.

Before accepting a result, inspect the vertex map and confirm that the coverage matches the intended task. A saved mapping can pass schema check while remaining partial because the existence check validates the entries present in the mapping rather than requiring source-wide coverage.

Limitations

• A schema morphism maps one source vertex to at most one target vertex. Splits, joins, and other value computations require a field transform.
• --monic prevents vertex collisions but does not establish edge injectivity. The overlap discovery used by schema integrate --auto-overlap performs the stronger search required for a pushout.
• --json omits the apex and certificate. Keep the human report if later review needs the coverage or proof status.

See also

• Build a migration for checking and applying the saved mapping.
• Apply field transforms for value-level computations.
• Migrations as morphisms for the underlying model.
• CLI reference for the complete option list.

Apply field transforms

A field transform computes or rewrites values during a lens operation. Use one when a vertex map cannot express the change, such as deriving a field from a sibling or changing a field’s representation.

Prerequisites

The TypeScript SDK and a source BuiltSchema. The current TypeScript lens-document path retains value transforms through compilation and instantiation.

Transform an existing field

This document increments count on get and decrements it on put:

const document = {
  id: 'dev.example.increment-count',
  source: 'v1',
  target: 'v2',
  steps: [
    {
      apply_expr: {
        field: 'count',
        expr: 'add count 1',
        inverse: 'sub count 1',
        coercion: 'iso',
      },
    },
  ],
};

using chain = p.compileLensDocument(document, 'record:body');
using lens = chain.instantiate(sourceSchema);

const { view, complement } = lens.getJson(
  { count: 4 },
  'record:body',
);
const restored = lens.putJson(view, complement, 'record:body');

apply_expr evaluates its expression with the named field bound in the expression environment. An inverse is required only when edits must propagate backward through the transform. Declare coercion: 'iso' only when the forward and inverse expressions round-trip for every accepted value.

Compute a field from its parent record

compute_field evaluates an expression over the scalar fields in the parent fiber and writes the result under target:

const document = {
  id: 'dev.example.double-count',
  source: 'v1',
  target: 'v2',
  steps: [
    {
      compute_field: {
        target: 'double_count',
        expr: 'mul count 2',
        coercion: 'projection',
      },
    },
  ],
};

using chain = p.compileLensDocument(document, 'record:body');
using lens = chain.instantiate(sourceSchema);
const { view, complement } = lens.getJson(
  { count: 4 },
  'record:body',
);

The computed field is derived data. With no inverse, putJson uses the complement to restore the original source fields; edits made only to double_count do not determine a new count.

Verify that compilation retained the transform

const transforms = chain.fieldTransforms();
if ((transforms['record:body'] ?? []).length === 0) {
  throw new Error('field transform was not compiled');
}

const laws = lens.checkLaws(instanceBytes);
if (!laws.holds) throw new Error(laws.violation ?? 'lens law failed');

fieldTransforms() reports transforms by parent vertex. checkLaws accepts an encoded instance, while getJson and putJson provide the record-oriented path shown above.

Current serialization limitation

Value transforms are stored beside the structural ProtolensChain; they are not part of chain.toJson(). Reconstructing a handle with ProtolensChainHandle.fromJson(chain.toJson(), wasm) thus loses them.

The same distinction affects other surfaces. schema lens compile reports only the number of field-transform vertices and writes the structural chain. Python’s ProtolensChain.from_dsl_* constructors, the TypeScript compileLensDocument handle, and Rust’s panproto_lens_dsl::CompiledLens retain the value-level programs and their order relative to structural steps.

Migration mapping JSON has a separate expr_resolvers field, but panproto_mig::compile does not install those expressions as FieldTransform values. Do not place expression source in a migration mapping and expect schema lift to execute it.

Common failures

• Attach a transform to the parent vertex whose fields it reads. A transform anchored at a scalar child cannot see its siblings.
• Keep expressions within the evaluator’s step, depth, and list-length budgets. Evaluation errors fail the transform for that record.
• Classify lossy computations as projection or opaque, not iso.
• Test boundary values for partial operations such as division, parsing, head, and indexing.

See also

• Expression-language reference for syntax, builtins, and evaluator limits.
• Write lenses in the lens DSL for the document structure.
• Use lenses for get, put, and law checking.

Use lenses

The lens API relates a source record to a target-shaped view. get constructs the view, put reconstructs a source-shaped record from an edited view, and the complement retains source data that get did not place in the view.

Prerequisites

A migration (Build a migration) or a hand-written lens via the lens DSL.

The task

A CompiledMigration exposes the lens operations directly. LensHandle represents a concrete auto-generated or DSL-compiled lens, while ProtolensChainHandle represents a schema-parameterized chain.

const { view, complement } = mig.getJson(oldRecord, "user:body");
const recordView = view as { age: number };

const editedView = { ...recordView, age: recordView.age + 1 };
const updatedOld = mig.putJson(editedView, complement, "user:body") as {
  age: number;
};

mig.getJson returns the forward view together with the complement, which retains data discarded by the forward operation. mig.putJson consumes both values and reconstructs a JavaScript record with the edit applied. The law checks below test the round trip for a supplied instance.

To compose two compiled migrations sequentially:

const composed = p.compose(mig_ab, mig_bc);

To compose two concrete LensHandle values:

const composedLens = p.composeLenses(lensAB, lensBC);

To compose schema-parameterized chains, call the method on the first chain:

const composedChain = chainAB.compose(chainBC);

Panproto.compose and Panproto.composeLenses compose compiled migrations and concrete lenses, respectively. ProtolensChainHandle.compose handles protolens chains. Each operation throws if the intermediate schemas or theory transforms do not chain.

Verification

const result = lens.checkLaws(instanceBytes);
console.log(result.holds, result.violation);

// For individual laws:
const getput = lens.checkGetPut(instanceBytes);
const putget = lens.checkPutGet(instanceBytes);

LensHandle.checkLaws(instance) returns a LawCheckResult { holds, violation } covering GetPut and PutGet together. checkGetPut and checkPutGet test each law individually; the Rust property tests in panproto-lens cover PutPut as well, exercised continuously in CI.

Common mistakes

• Calling put with a complement produced for a different source schema. put compares the complement’s source fingerprint with the lens source and returns ComplementMismatch when they differ. Recompute the complement with this lens.
• Reading get and then mutating the source before calling put. The complement is computed against the source as it was at get time; if you mutate the source, the complement is stale.
• Composing lenses whose intermediate schemas are isomorphic but not equal. The structural-equality check on protolens_composable will reject; rebuild one of the lenses against the other’s schema.

See also

• Reference: lens combinators.
• Lenses and round-trip laws.
• Lens DSL: denotational semantics.
• Use protolenses, Use dependent optics.

Use protolenses

A protolens applies the same transform to several schemas that satisfy one precondition. A single schema-parameterized declaration instantiates a lens for each matching schema.

Prerequisites

The Rust SDK (panproto-lens::protolens) or the lens DSL with parametric declarations enabled.

The task

Declare

A Protolens packages a precondition (a TheoryConstraint on the source theory) with a TheoryTransform. Build elementary protolenses via the elementary helpers, or compose them into a ProtolensChain:

use panproto_lens::protolens::{ProtolensChain, combinators};

fn main() {
let rename_legacy_id: ProtolensChain = combinators::rename_field(
    "user", "user:legacy_id", "legacy_id", "id",
);
let _ = rename_legacy_id;
}

The chain captures a precondition on the source theory and a sequence of transforms. It does not yet know which concrete schema it will run against.

Apply (fused)

use panproto_lens::protolens::{ProtolensChain, combinators};
use panproto_core::schema::{Protocol, Schema, SchemaBuilder};
fn main() -> Result<(), Box<dyn std::error::Error>> {
let rename_legacy_id: ProtolensChain = combinators::rename_field("user", "user:legacy_id", "legacy_id", "id");
let protocol: Protocol = panproto_core::protocols::atproto::protocol();
let user_schema: Schema = SchemaBuilder::new(&protocol)
    .vertex("user", "object", None)?
    .vertex("user:legacy_id", "string", None)?
    .edge("user", "user:legacy_id", "prop", Some("legacy_id"))?
    .entry("user")
    .build()?;
let lens_for_users = rename_legacy_id.instantiate(&user_schema, &protocol)?;
let _ = lens_for_users;
Ok(()) }

The precondition requires the named property edge in addition to the user vertex. Instantiation produces a concrete Lens for any schema containing that structure. For a multi-step chain, the fused path compiles the composed transform in one pass and retains the migration metadata computed for the whole chain.

Apply (sequential)

use panproto_lens::protolens::{ProtolensChain, combinators};
use panproto_core::schema::{Protocol, Schema, SchemaBuilder};
fn main() -> Result<(), Box<dyn std::error::Error>> {
let rename_legacy_id: ProtolensChain = combinators::rename_field("user", "user:legacy_id", "legacy_id", "id");
let protocol: Protocol = panproto_core::protocols::atproto::protocol();
let base_schema: Schema = SchemaBuilder::new(&protocol)
    .vertex("user", "object", None)?
    .vertex("user:legacy_id", "string", None)?
    .edge("user", "user:legacy_id", "prop", Some("legacy_id"))?
    .entry("user")
    .build()?;
let stepwise = rename_legacy_id.instantiate_sequential(&base_schema, &protocol)?;
let _ = stepwise;
Ok(()) }

Sequential instantiation applies each step to the running schema and composes the resulting lenses. It returns one composed Lens, not a list of intermediate lenses. The implementation exists to exercise the stepwise path in tests; it does not expose the intermediate schemas to the caller.

Compose

use panproto_inst::Value;
use panproto_lens::protolens::{Protolens, vertical_compose, elementary};

fn main() -> Result<(), Box<dyn std::error::Error>> {
let first: Protolens = elementary::rename_sort("string", "text");
let second: Protolens = elementary::add_sort("tags", "array", Value::Null);
let composed = vertical_compose(&first, &second)?;
let _ = composed;
Ok(()) }

vertical_compose requires the target endofunctor of first to structurally match the source endofunctor of second. A mismatch returns LensError.

Verification

After instantiate returns a Lens, exercise the round-trip laws on representative data via Lens::get / Lens::put (or use the higher-level lens-law harness in panproto_lens::laws). Property tests in crates/panproto-lens/tests/ are the canonical examples.

Common mistakes

• Composing protolenses whose intermediate schemas only happen to look the same. protolens_composable enforces structural equality, not name equality; build one against the other to be safe.
• Reaching for sequential instantiation in production. Use fused (instantiate) by default; sequential exists for inspection and tests.
• Treating preconditions as pure documentation. The precondition is checked at instantiation time; a schema that does not satisfy it raises LensError::ProtolensError with a message listing the unmet constraints (use Protolens::check_applicability first if you want to surface the reasons separately).

See also

• Reference: lens combinators.
• Protolens composition for the formal model.
• Use lenses for the non-parametric case.

Classify a scoped transform

A scoped transform applies an inner protolens to the sub-schema rooted at one vertex. The edge leading to that vertex determines whether the runtime focus behaves as a lens, traversal, or prism. The name is related to dependent optics (Vertechi 2023), but panproto implements a schema-edge-kind classifier rather than the paper’s indexed-category construction.

Prerequisites

The Rust SDK. The panproto-lens crate (re-exported from panproto-core::lens).

The task

Build the scoped transform

#![allow(unused)]
fn main() {
use panproto_lens::protolens::elementary;

let inner = elementary::rename_edge_name("post", "tags", "tags", "labels");
let scoped = elementary::scoped("post:tags", inner);
}

Because elementary::scoped constructs the protolens without inspecting a schema, scoped.optic_kind() returns the conservative theory-level classification inner_kind.compose(OpticKind::Lens). The incoming edge kind is unavailable at construction time.

Refine the classification

Read the incoming edge from the concrete schema, then pass its kind to refine_scoped_optic:

#![allow(unused)]
fn main() {
use panproto_lens::protolens::Protolens;
use panproto_lens::{OpticKind, refine_scoped_optic};
use panproto_schema::Schema;

fn classify_scoped(schema: &Schema, scoped: &Protolens) -> OpticKind {
    let incoming = schema
        .incoming_edges("post:tags")
        .iter()
        .find(|edge| edge.src.as_ref() == "post")
        .expect("post:tags must have an incoming edge from post");

    refine_scoped_optic(incoming.kind.as_ref(), scoped.optic_kind())
}
}

The result is Lens for a prop carrier, Traversal for an item or items carrier, and Prism for a variant carrier. The classifier does not inspect whether a property edge is required.

refine_scoped_optic uses Lens for prop and unrecognized edge kinds, Traversal for item and items, and Prism for variant. It composes that carrier with the inner kind.

Field-level combinators

The panproto_lens::protolens::combinators module exposes higher-level chains assembled from elementary steps. For instance, combinators::rename_field(parent, field, old_name, new_name) returns a ProtolensChain that renames a JSON property key. Use elementary::scoped or combinators::map_items to apply an inner transform to an array element vertex.

Verification

Instantiate the protolens against a concrete schema, then call panproto_lens::optic::check_optic_laws(kind, &lens, &instance). This checks the obligations implemented for the refined kind. The prism checker cannot test the full review law because this layer does not expose a review operation.

Common mistakes

• Treating Protolens::optic_kind() as schema dependent. It classifies the stored theory transform only. Call refine_scoped_optic with the concrete edge kind for a scoped transform.
• Assuming every non-prop spelling is rejected. The refinement function treats unknown kinds as Lens; validate the schema against its protocol before relying on the classification.
• Treating the classified kind as proof of the laws. Run check_optic_laws on representative instances and handle OpticLawViolation.

See also

• Reference: lens combinators.
• Lens DSL: denotational semantics.
• Use lenses, Use protolenses.

Write lenses in the lens DSL

The lens DSL describes schema-level steps and value-level field transforms in Nickel, JSON, or YAML. Exactly one body variant, such as steps, rules, compose, auto, from_diff, or symmetric, may be present.

Write a document

This JSON document renames one property key:

{
  "id": "dev.example.user-v1-to-v2",
  "description": "Rename the user name property",
  "source": "dev.example.user.v1",
  "target": "dev.example.user.v2",
  "steps": [
    {
      "rename_field": {
        "old": "name",
        "new": "display_name"
      }
    }
  ]
}

Each step is a single-key object. --body-vertex supplies the parent vertex for field-level steps; its default is record:body.

Compile and apply in TypeScript

The TypeScript handle retains both the structural chain and any value transforms:

using chain = p.compileLensDocument(
  document,
  'record:body',
  'json',
);
using lens = chain.instantiate(sourceSchema);

const { view, complement } = lens.getJson(
  inputRecord,
  'record:body',
);
const restored = lens.putJson(view, complement, 'record:body');

compileLensDocument accepts a JavaScript object, text, or UTF-8 bytes. JSON is the default format; pass 'yaml' for YAML. Nickel is not accepted by this WASM entry point because its imports require filesystem resolution.

Use chain.fieldTransforms() to confirm that apply_expr or compute_field steps survived compilation. Those transforms are stored beside the chain and do not appear in chain.toJson().

Compile Nickel or files in Rust

panproto-lens-dsl resolves the bundled Nickel contract and filesystem imports:

#![allow(unused)]
fn main() {
use std::path::Path;

let compiled = panproto_core::lens_dsl::load_and_compile(
    Path::new("lenses/user-v1-to-v2.ncl"),
    "record:body",
)?;

println!("{} structural steps", compiled.chain.steps.len());
println!("{} transform anchors", compiled.field_transforms.len());
Ok::<(), panproto_core::lens_dsl::LensDslError>(())
}

load_and_compile supports .ncl, .json, .yaml, and .yml. Named references in a compose body resolve against sibling documents in the same directory. auto and from_diff require the schema-aware compile_with_schemas entry point.

Compile and apply with the CLI

schema lens compile lenses/user-v1-to-v2.json \
  --body-vertex record:body \
  --out compiled.json

schema lens apply compiled.json user-v1.json \
  --protocol atproto \
  --schema user-v1.schema.json

schema lens compile writes a panproto-compiled-lens-v1 artifact. The file contains the structural chain, the value transforms, and an ordered stages array. The stages determine whether a value expression runs before or after a structural rename. schema lens apply reads this artifact directly and instantiates each stage against the schema produced by the preceding stage.

Raw ProtolensChain JSON remains accepted by schema lens apply, as does a target schema used for automatic lens generation. A file written by schema lens generate --save is a raw structural chain rather than a compiled-lens artifact. It can be applied, but it does not store value transforms derived during automatic generation.

Verification

Instantiate the document against the intended source schema, run get and put on representative instances, and use LensHandle.checkLaws or panproto_lens::laws::check_laws. Compilation validates document shape and expression syntax; it does not show that a value transform is total on production data.

See also

• Apply field transforms for apply_expr and compute_field.
• Use lenses for runtime operations.
• Lens DSL: denotational semantics for the document model.

Query instances

The query engine selects nodes by schema anchor, follows edge kinds, filters with an expression, and returns selected fields. Rust and TypeScript expose the same operation.

Prerequisites

A Schema and a WInstance loaded against it. Predicates use the expression language.

Filter and project

panproto_inst::InstanceQuery uses the field names anchor, predicate, group_by, project, limit, and path. execute_query takes the query first, the instance second, and the schema third.

#![allow(unused)]
fn main() {
use panproto_core::gat::Name;
use panproto_core::inst::{InstanceQuery, QueryMatch, WInstance, execute_query};
use panproto_core::schema::Schema;

fn titles(schema: &Schema, instance: &WInstance) -> Vec<QueryMatch> {
    let query = InstanceQuery {
        anchor: Name::from("post"),
        project: Some(vec!["id".into(), "title".into()]),
        limit: Some(50),
        ..InstanceQuery::default()
    };

    execute_query(&query, instance, schema)
}
}

The anchor selects matching instance nodes. project limits each result’s fields map. It does not change the matched node’s value, identifier, or anchor.

Follow edges

path contains edge kinds, not target vertex names or property labels. The executor first selects nodes matching anchor, then follows each edge kind in order:

#![allow(unused)]
fn main() {
use panproto_core::gat::Name;
use panproto_core::inst::{InstanceQuery, WInstance, execute_query};
use panproto_core::schema::Schema;
fn run(schema: &Schema, instance: &WInstance) {
let query = InstanceQuery {
    anchor: Name::from("user"),
    path: vec![Name::from("authored")],
    project: Some(vec!["title".into()]),
    ..InstanceQuery::default()
};
let posts = execute_query(&query, instance, schema);
let _ = posts;
}
}

Predicates are panproto_expr::Expr values. The evaluator binds a node’s extra fields, scalar child values reached by labeled edges, and the metadata variables _anchor, _id, _value, and _children_count. Instance-aware builtins such as Edge, Children, HasEdge, and EdgeCount receive the current instance and node.

TypeScript boundary

@panproto/core exports executeQuery(query, instance, wasm). The wrapper converts the public groupBy, projection, and nodeId names to and from Rust’s group_by, project, and node_id wire fields. It also supplies the schema handle retained by the Instance, so callers do not encode the schema separately.

The WASM module keeps execute_query(queryBytes, instanceBytes, schemaBytes) for direct byte-oriented callers. SDK code uses execute_query_with_schema_handle to avoid serializing a schema that is already in the WASM resource table.

Verification and limits

execute_query returns a vector and does not return predicate errors. A predicate evaluation that fails or does not produce true excludes that node. The executor accepts a schema argument but does not use it to reject an anchor absent from the schema. The byte-oriented WASM entry point rejects missing or malformed schema bytes, while the handle entry point rejects an invalid or non-schema handle. Neither entry point type-checks the query against the schema after resolving it.

Expression evaluation uses EvalConfig::default(). InstanceQuery exposes no budget field, and the query functions expose no configuration argument, so a caller cannot raise that budget at the query call site.

See also

• Reference: expression language.
• Convert data between formats.

Convert data between schemas

schema data convert auto-generates a lens between two schemas in one protocol and applies it to JSON records.

Prerequisites

The schema CLI, two files in panproto’s internal schema JSON format, and input records rooted at a vertex the CLI can infer from the source schema. The current command resolves only the atproto protocol.

Convert one file

schema data convert --protocol atproto \
  --from schemas/user-v1.json \
  --to schemas/user-v2.json \
  data/user.json \
  -o data/user-v2.json

--from and --to are schema paths. With no --chain, the command generates a lens using AutoLensConfig::default(), parses the input as a W-type instance, runs get, and serializes the view against the target schema.

Defaults use comma-separated key=value pairs:

schema data convert --protocol atproto \
  --from schemas/user-v1.json \
  --to schemas/user-v2.json \
  --defaults status=active,locale=en \
  data/user.json

The CLI parses all default values as strings. A key resolves against an added target vertex ID first, then a unique incoming field label, and finally the vertex kind. The generated lens adds the value only when the source-backed parent does not already carry that field. Generation reports an error when a default is unused, ambiguous, or cannot be placed from the target schema. With --chain, defaults must already be embedded in the serialized chain; --defaults cannot override them.

Convert a directory

Directory mode reads the immediate *.json files and requires an output directory:

schema data convert --protocol atproto \
  --from schemas/user-v1.json \
  --to schemas/user-v2.json \
  data/users \
  -o data/users-v2

Files that fail to load or convert are reported as skipped, and the final line prints converted and skipped counts. Inspect that count in automation; directory mode can finish after skipping individual files.

Convert from TypeScript

using lens = p.lens(srcSchema, tgtSchema);
const { view, complement } = lens.getJson(inputRecord, 'user');
const output = view as Record<string, unknown>;

Retain complement if the application may later call putJson to propagate an edited view backward.

Verify the conversion

Check the actual record with the SDK law checker:

const instance = p.parseJson(srcSchema, JSON.stringify(inputRecord));
const result = lens.checkLaws(instance._bytes);
if (!result.holds) {
  throw new Error(result.violation ?? 'lens law failed');
}

schema lens verify <DATA> <SCHEMA> --protocol <PROTOCOL> parses the data with the supplied schema and runs the concrete GetPut and PutGet checks. A passing result applies to that record. It is not a proof over every instance of the schema.

Backward CLI conversion uses an empty complement. It can reconstruct only lenses that need no captured source data or for which defaults suffice. Use an SDK get/put pair when backward conversion depends on the complement produced from a specific source record.

--chain selects a saved chain instead of automatic lens generation. It still requires --from and --to, since a serialized ProtolensChain does not contain the concrete schemas needed for instantiation. schema lens generate --save writes this round-trippable chain format. The compiled artifact produced by schema lens compile --out also carries ordered value-transform stages and is intended for schema lens apply, not schema convert --chain.

See also

• Use lenses for bidirectional updates.
• Apply field transforms for computed values.
• Translate across protocols for the current cross-protocol limitation.

Round-trip with format preservation

Choose the format-preserving codec for a JSON, YAML, TOML, XML, or CSV round trip that must satisfy emit(parse(bytes)) == bytes. The codec records whitespace, comments, and ordering in a CST complement.

Source-code grammars use emit_pretty instead. Follow Parse full ASTs for that procedure and Source-code emission for its model.

Prerequisites

Format preservation is gated behind the tree-sitter feature flag on panproto-core (or directly on panproto-io). The shipped schema binary does not enable this feature, so its round-trips are not byte-for-byte: a format-preserving parse or emit requested from the default binary returns canonical output with no layout complement and prints a one-line notice to stderr. Byte preservation requires a build that turns the feature on, for instance a tool built against panproto-core with features = ["tree-sitter"], or a direct dependency on panproto-io with the same feature. The snippets below assume such a build.

The task

The format-preserving round-trip is exposed by the codec API, not by the shipped CLI. parse_wtype_preserving returns the instance together with a complement carrying the CST data the schema does not see, and emit_wtype_preserving reconstructs the byte-for-byte original from the pair.

In Rust:

use panproto_core::io::unified_codec::UnifiedCodec;
use panproto_core::schema::{Schema, SchemaBuilder};
fn main() -> Result<(), Box<dyn std::error::Error>> {
let proto = panproto_core::protocols::atproto::protocol();
let schema: Schema = SchemaBuilder::new(&proto).vertex("root", "object", None)?.entry("root").build()?;
let bytes: &[u8] = b"{}\n";
let codec = UnifiedCodec::yaml("atproto")?;
let (instance, complement) = codec.parse_wtype_preserving(&schema, bytes)?;
let out = codec.emit_wtype_preserving(&schema, &instance, &complement)?;
assert_eq!(out, bytes);
Ok(()) }

The complement carries the CST data that the schema does not see. emit_wtype_preserving reconstructs the byte-for-byte original from (instance, complement). Constructors exist for JSON, XML, YAML, TOML, and CSV. UnifiedCodec::tsv additionally requires the table-vertex name.

Without the tree-sitter feature these constructors are compiled out. For code that must run in either build, ProtocolRegistry exposes parse_wtype_preserving_or_canonical and emit_wtype_preserving_or_canonical. With tree-sitter, these methods delegate to the preserving codecs. Without it, they return canonical output. Fallback parsing always prints a notice; fallback emission prints one only when a complement was supplied.

Verification

The byte equality is the verification. Property tests in CI check emit(parse(b)) == b against a corpus of JSON, YAML, TOML, XML, and CSV files.

Common mistakes

• Discarding the complement after modifying the instance. The complement contains layout rather than the authoritative field value. Reusing it preserves the original whitespace and ordering around values supplied by the modified instance.
• Mixing format-preserving codec output with non-preserving codec input. The two pipelines are separate; choose one consistently.

See also

• Reference: protocol catalog.
• Convert data between formats.
• Parse full ASTs for tree-sitter parsing of source code.

Parse full ASTs

Full-AST parsing converts source code into a panproto Schema derived from its tree-sitter syntax tree. The available languages are the grammars compiled into the current binary or SDK package.

Prerequisites

The schema CLI or the Rust SDK with full-parse. The default panproto-parse build enables the eleven-language core grammar group. Feature groups and companion Python packages can add more, up to the full grammar catalog.

Inspect a file from the CLI

schema parse file src/main.rs

The command prints a summary containing the detected language and the vertex and edge counts. It does not serialize the AST schema to stdout.

To inspect a directory:

schema parse project .

This command builds a project schema and prints aggregate counts plus the detected protocol for each recognized path. It also does not emit project-schema JSON. Use the Rust or Python API when the caller needs the Schema value itself.

Check source replay

schema parse emit src/main.rs > /tmp/main.replayed.rs
cmp src/main.rs /tmp/main.replayed.rs

parse emit parses the file and calls the parse-side emitter on the resulting schema. It writes only the emitted bytes to stdout, which makes the cmp check reliable.

Parse from Rust

use std::path::Path;
use panproto_core::parse::ParserRegistry;

fn main() -> Result<(), Box<dyn std::error::Error>> {
    let source = std::fs::read("src/main.rs")?;
    let registry = ParserRegistry::new();

    let schema = registry.parse_file(Path::new("src/main.rs"), &source)?;
    println!("{} vertices", schema.vertex_count());

    let explicit = registry.parse_with_protocol(
        "rust",
        &source,
        "src/main.rs",
    )?;
    assert_eq!(schema.vertex_count(), explicit.vertex_count());
    Ok(())
}

parse_file(path, content) detects the protocol from the path extension and returns ParseError::UnknownLanguage for an unregistered extension. parse_with_protocol(protocol, content, file_path) bypasses extension detection but still requires a registered protocol.

Parse from Python

from pathlib import Path
import panproto

source = Path("src/app.py").read_bytes()
registry = panproto.AstParserRegistry()
schema = registry.parse_file("src/app.py", source)

print(len(schema.vertices), len(schema.edges))
print(registry.protocol_names())

The core Python wheel discovers installed panproto-grammars-* companion packages when panproto.AstParserRegistry() is constructed. Install the group that contains the required language before creating the registry. For instance, panproto-grammars-functional adds Haskell, OCaml, and related grammars.

Read anonymous-token fields

Named tree-sitter children appear as schema edges. When a grammar attaches a field name to an unnamed token alternative, the walker stores the token text as a field:<name> constraint on the parent. The following QVR example requires panproto-grammars-all, which registers the qvr grammar. Use Schema.field_text to read the constraint:

schema = registry.parse_with_protocol(
    "qvr",
    b"let y = log(x)",
    "demo.qvr",
)
let_call = next(v.id for v in schema.vertices if v.kind == "let_call")
assert schema.field_text(let_call, "func") == "log"

The Rust accessor is Schema::field_text(vertex_id, field_name) -> Option<&str>.

Verify pretty emission before relying on it

emit_pretty_with_protocol renders a schema without replaying its original layout. Query the protocol’s verification tier first:

#![allow(unused)]
fn main() {
use panproto_core::parse::{EmitVerificationStatus, ParserRegistry};

let registry = ParserRegistry::new();
match registry.emit_verification_status("rust") {
    EmitVerificationStatus::Verified => {}
    EmitVerificationStatus::Generic => {
        eprintln!("pretty emission has no protocol-specific verification claim");
    }
    EmitVerificationStatus::Unsupported => {
        eprintln!("pretty emission is unavailable for this protocol");
    }
}
}

Verified records coverage by repository tests on representative input or a protocol corpus. It is not a proof over every byte sequence. Use schema parse emit on the actual files that enter a pipeline.

Limitations

• The AST schema contains syntactic structure. It does not add type checking, name resolution, or control-flow information.
• The CLI parse-inspection commands print summaries, not serializable schema values.
• Tree-sitter may include error nodes for malformed source, and panproto’s schema construction can still fail. Do not treat parsing as an unconditional total operation.
• Language availability depends on build features and installed grammar packs. Query protocol_names() rather than relying on the maximum catalog size.

See also

• Decorate an abstract schema for rendering a layout-free schema.
• Source-code emission for replay and pretty-emission paths.
• Rust SDK for feature selection.

Decorate an abstract schema

Decoration renders an AbstractSchema with a grammar and parses the result again. The returned DecoratedSchema carries the layout constraints needed for replay emission.

Prerequisites

The Rust SDK with the full-parse feature. The requested grammar must be compiled into panproto-parse, and the abstract schema’s protocol field must equal the grammar name.

Obtain an abstract schema

SchemaBuilder::build_abstract() is the constructor for a hand-built layout-free schema. It rejects constraints in the layout fiber, such as start-byte, end-byte, interstitial-N, and chose-alt-*.

The following example begins with parsed JSON only to obtain a compact, valid grammar-shaped schema. A hand-built AbstractSchema for the same protocol can be substituted directly.

use panproto_core::parse::{LayoutPolicy, ParserRegistry};
use panproto_core::schema::DecoratedSchema;

fn main() -> Result<(), Box<dyn std::error::Error>> {
    let registry = ParserRegistry::new();
    let parsed = registry.parse_with_protocol(
        "json",
        br#"{"k": 1}"#,
        "input.json",
    )?;
    let abstract_schema = DecoratedSchema::wrap_unchecked(parsed).forget_layout();

    let decorated = registry.decorate(
        "json",
        &abstract_schema,
        &LayoutPolicy::default(),
    )?;
    let bytes = registry.emit_pretty_with_protocol(
        "json",
        decorated.as_schema(),
    )?;

    println!("{}", String::from_utf8(bytes)?);
    Ok(())
}

decorate uses the supplied policy to produce canonical bytes, then parses those bytes to recover byte spans, interstitial text, and grammar-choice constraints. The parse step assigns fresh vertex identifiers.

Render without decoration

If only canonical bytes are needed, call pretty_with_protocol and skip the reparsing step:

#![allow(unused)]
fn main() {
use panproto_core::parse::{LayoutPolicy, ParserRegistry};
use panproto_core::schema::AbstractSchema;

fn render(
    registry: &ParserRegistry,
    schema: &AbstractSchema,
) -> Result<Vec<u8>, panproto_core::parse::ParseError> {
    let policy = LayoutPolicy {
        indent_width: 4,
        newline: "\r\n".into(),
        ..LayoutPolicy::default()
    };
    registry.pretty_with_protocol(schema.protocol(), schema, &policy)
}
}

LayoutPolicy is an alias of FormatPolicy. Its fields are indent_width, separator, newline, line_break_after, indent_open, and indent_close.

Verify the result

Decoration preserves the abstract structure at the granularity tested by the library: after forget_layout, the vertex-kind and edge-shape multisets should match the input. It does not preserve vertex identifiers.

#![allow(unused)]
fn main() {
use panproto_core::schema::{edge_multiset, kind_multiset};
use panproto_core::schema::{AbstractSchema, DecoratedSchema};
fn check(input: &AbstractSchema, output: &DecoratedSchema) {
let round_trip = output.forget_layout();
assert_eq!(
    kind_multiset(input.as_schema()),
    kind_multiset(round_trip.as_schema()),
);
assert_eq!(
    edge_multiset(input.as_schema()),
    edge_multiset(round_trip.as_schema()),
);
}
}

Run the focused integration test with the grammar features used by the test:

cargo test -p panproto-parse --test decorate_section_law \
  --features lang-json,lang-lilypond

ParserRegistry::emit_verification_status(protocol) reports Verified, Generic, or Unsupported. Verified means the repository has an explicit fixed-point or round-trip test for that protocol. Generic means the grammar-walker path is available but lacks a protocol-specific verification claim. Unsupported means the parser is missing or lacks the grammar data required for pretty emission.

Limitations

• A schema built for atproto cannot be decorated with the json, rust, or lilypond parser. Protocol mismatch returns ParseError::SchemaConstruction.
• build_decorated() and DecoratedSchema::wrap_unchecked() do not validate that a complete layout fiber is present. Reserve them for data produced by parsing or a trusted decoration path.
• The section law concerns abstract structure, not byte equality with an earlier source file. A new LayoutPolicy may produce different canonical bytes.

See also

• Parse full ASTs for parsing source into a decorated schema.
• Source-code emission for the emitter.
• Layout enrichment for the model.

Build a custom protocol

A custom protocol starts with a Protocol value and its schema and instance theories. Parsing, emission, migration, and language bindings are separate integration points. Implement only the surfaces the protocol will expose, and register each one explicitly.

Prerequisites

Familiarity with Schemas as theories and Composing protocols by colimit. The Rust toolchain.

The task

Declare the theory

The theory DSL provides one authoring path:

let T = import "panproto/theory.ncl" in
{
  id = "dev.example.my-proto-schema",
  description = "A directed graph whose edges carry permissions",
  theory = "ThMyProtoSchema",
  sorts = [
    T.simple "Vertex",
    T.simple "Edge",
    T.val_sort "Permission" "string",
  ],
  ops = [
    T.unary "src" "Edge" "Vertex",
    T.unary "tgt" "Edge" "Vertex",
    T.unary "perm_of" "Edge" "Permission",
  ],
  equations = [],
} | T.Theory

This document declares the schema-side theory directly. Give every document a stable id and description; the theory field supplies the name used by registrations and later compositions. Use a compose document when the schema theory should instead be a colimit of existing theories.

For finer control, declare the theory directly in Rust with the class! and inductive! macros from panproto-gat-macros.

From Python, the same DSL document loads via Theory.from_nickel(source), Theory.from_yaml(source), Theory.from_json(source), or Theory.from_path(path) (dispatches by extension). The loaders accept the theory, class, and inductive body variants; multi-body documents (morphism, composition, protocol, bundle) belong in panproto-theory-dsl::load_and_compile directly. For incremental authoring, panproto.TheoryBuilder mirrors class! in a chainable form. Round-trip the flat Theory shape via to_json / to_yaml paired with from_dict_json / from_dict_yaml.

Implement external-format boundaries

panproto-protocols has no common Parser or Emitter trait. Protocol modules expose format-specific free functions. A JSON document parser usually has the shape fn(&serde_json::Value) -> Result<Schema, ProtocolError>; a text-language parser usually accepts &str. Add the parser to parse_schema_document or parse_schema_source in crates/panproto-protocols/src/lib.rs, and add its canonical name to the corresponding document_parser_protocols or source_parser_protocols list.

Emitters are also format-specific functions in their protocol modules. Add one only when the protocol has a defined external representation and the application needs to produce it. Internal schema validation and migration operate on Schema values and do not require an external-format emitter.

Register

Each protocol module exposes protocol() -> Protocol and register_theories(&mut HashMap<String, Theory, _>). The internal module skeleton below is repository code, not a standalone Rust program:

// crates/panproto-protocols/src/my_proto.rs
use std::collections::HashMap;
use panproto_gat::Theory;
use panproto_schema::Protocol;

use crate::theories;

pub fn protocol() -> Protocol {
    Protocol {
        name: "my_proto".into(),
        schema_theory: "ThMyProtoSchema".into(),
        instance_theory: "ThMyProtoInstance".into(),
        ..Protocol::default()
    }
}

pub fn register_theories<S: ::std::hash::BuildHasher>(
    registry: &mut HashMap<String, Theory, S>,
) {
    theories::register_constrained_multigraph_wtype(
        registry,
        "ThMyProtoSchema",
        "ThMyProtoInstance",
    );
}

Pick the theories::register_* helper that matches the intended schema and instance shapes (register_constrained_multigraph_wtype, register_typed_graph_wtype, register_hypergraph_functor, and related helpers). A helper is appropriate only when its constructed theories match the names and operations declared by the protocol.

Registration is surface-specific:

1. Export the module from its category module in panproto-protocols.
2. Add document or source parsing to the dispatch functions in panproto-protocols::lib when the protocol has an external parser.
3. Add the protocol name and constructor to builtin_protocol_names and lookup_builtin_protocol in crates/panproto-wasm/src/api/helpers.rs for the TypeScript SDK. Add theory registration there as well if SDK operations need the theories; that registry currently has arms only for atproto, json-schema, graphql, sql, and protobuf.
4. Add the constructor to crates/panproto-py/src/protocols.rs for the Python SDK.
5. Add the constructor and theory registration to resolve_protocol and build_theory_registry in crates/panproto-cli/src/cmd/helpers.rs for CLI commands. Both tables currently contain only atproto.

Other bindings that expose a fixed built-in table need their own entry. A Rust caller can use the module’s protocol() and register_theories() functions directly without a global lookup.

Verification

cargo test -p panproto-protocols my_proto

Add tests under the new protocol module with names containing my_proto; the command above runs that subset with Cargo alone. Cover every implemented surface. That means theory registration and schema validation for a theory-backed protocol, parsing for an external parser, and a parse/emit round trip only when an emitter exists. Add a migration test when the protocol claims migration support.

Common mistakes

• Declaring extensions before the colimit components are correct. Extensions interact with the colimit structure; if a building-block step is wrong, the extension may not even reach registration.
• Adding a module without updating its dispatch tables. The Rust module remains directly callable, but string-based SDK and CLI lookups will not find it.
• Assuming the CLI uses the same catalog as the language SDKs. Its resolver and theory registry are separate and currently recognize only atproto.
• Requiring an emitter for internal operations. schema validate reads panproto schema JSON directly; it does not call a protocol document parser or emitter.

See also

• Reference: protocol catalog.
• Theory DSL: denotational semantics.
• Composing protocols by colimit.

Schema version control

These guides put schemas, migrations, and associated data under panproto version control. Begin with repository creation and commits; add branching, data migration, or a git bridge only when the project needs that workflow.

See also

• Schema version control semantics for the model.
• Pushouts and merge for the merge construction.
• Reference: CLI for the full subcommand list.

Init and commit

Initialize a panproto repository, stage a schema, and record the first content-addressed commit.

Prerequisites

The schema CLI installed. A directory containing schema files (or a fresh directory you are about to populate).

The task

cd my-schemas/
schema init                 # create .panproto/
schema add user.json
schema commit -m "initial user schema"
schema log                  # show history

init creates a .panproto/ object store and a main branch. It may also generate panproto.toml when package detection finds source packages. add parses or loads the supplied path and stages the resulting schema; commit records the staged schema. A path ending in .json is deserialized directly as panproto’s internal Schema representation. To stage an ATProto Lexicon bundle, point add at a directory whose manifest declares a homogeneous atproto package. Non-JSON source files use the full-AST parser.

To inspect the current state:

schema status
schema diff --staged      # diff the staged schema against HEAD
schema show <commit-hash>

schema diff without --staged requires two file paths. A staged diff also requires an existing commit, so use it after the first commit.

Verification

schema log --oneline

prints one line per commit. The default long format includes the commit ID, schema ID, author, timestamp, and message.

Common mistakes

• Forgetting to schema add before schema commit. Like git, the staging area is explicit; commits only include staged changes.
• Editing inside .panproto/objects/ directly. The store is content-addressed; manual edits break the hash invariants.

See also

• Branch and merge.
• Reference: CLI.
• Schema version control semantics.

Branch and merge

Create a branch to isolate a schema change, then merge it back through panproto’s schema-aware merge operation.

Prerequisites

A panproto repository with at least one commit (Init and commit).

The task

schema branch feature/add-handle
schema checkout feature/add-handle
# edit the schema, add a `handle` field
schema add user.json
schema commit -m "add handle"

schema checkout main
schema merge feature/add-handle

merge uses the current commit, the named branch, and their common ancestor. A fast-forward moves the current branch. A divergent merge performs a three-way structural merge and records a two-parent commit unless --no-commit or --squash changes that behavior. Before it records a normal clean merge commit, the repository verifies that the total migrations from the base through both parents to the result form a commuting cocone. When both branches add the same name with the same definition, structural merge identifies the additions. In that case the result is not a free pushout. The --no-commit and --squash paths do not run this commit-time cocone check.

If both branches make incompatible changes to the same structure, the command prints the detected conflicts and exits nonzero. The current CLI does not persist an editable conflict descriptor.

Resolve the source schemas on one branch, commit that resolution, and rerun the merge:

schema checkout feature/add-handle
# edit user.json to incorporate the intended result
schema add user.json
schema commit -m "resolve merge inputs"
schema checkout main
schema merge feature/add-handle

Verification

schema log

shows a Merge: line for a two-parent merge commit. The --graph option is accepted but currently ignored by the renderer.

Common mistakes

• Expecting checkout to rewrite source files. It moves the repository ref only. Edit or regenerate working files explicitly.
• Looking for a saved conflict object after a failed merge. Capture the printed conflict details; the CLI does not yet provide an interactive continuation flow.

See also

• Pushouts and merge for the categorical comparison.
• Schema version control semantics.
• Init and commit.

Version data alongside schemas

Stage data with its schema when a commit must retain both. Data migration is a separate operation over a commit range.

Prerequisites

A panproto repository with at least one schema and a corresponding data instance.

The task

Data is staged together with its schema via schema add --data:

schema add user.json --data records/
schema commit -m "v1 schema and seed data"

# Evolve the schema and re-stage with the same data directory.
schema add user-v2.json --data records/
schema commit -m "v2 schema"

# Sync the working directory across parent..HEAD.
schema data sync records/

schema add --data <DATA> stages each immediate JSON file in the directory. Each file’s records are parsed and checked against the schema being staged, so a file that is not JSON, or one whose records do not fit the schema, fails at add rather than at whatever later operation first tries to read it. Staging is all or nothing for the data files, so a failure leaves none of them staged. --skip-verify stages without the check and leaves the result pending, which a default commit then refuses; it does not skip reading the file, since a data set records which schema its data belongs to and bytes that cannot be read as records of that schema cannot be recorded under it. schema data sync compares a target commit with its first parent, generates a lens, and rewrites records it can migrate; failed records are reported as skipped.

Preview the default parent..HEAD range and run coverage without writing:

schema data migrate records/ --dry-run --coverage

--dry-run prints the selected plan without attempting the conversions. The coverage pass then tries each immediate JSON file and reports successes and failures. Use --range old..new to select another pair.

schema status --data records/
schema data status records/

Checkout changes only the repository ref. Pass --migrate to request a corresponding on-disk data migration:

schema checkout <commit> --migrate records/

Verification

schema data status records/

prints the number of immediate JSON files, the HEAD schema ID, and the number of data sets tracked by that commit. It does not parse the files or prove conformance.

schema data migrate records/ --dry-run --coverage is the non-writing per-record check.

Common mistakes

• Editing data inside the store directly. Like schemas, data objects are content-addressed.
• Skipping data when committing schema changes. If the v1 commit has no staged data, the later commit-range operation has no stored v1 records to migrate. The v2 commit may thus have no data even when records exist in the working directory.
• Assuming rebase or amend migrates working data. Those commands take no data-directory option. Run an explicit data migration after rewriting history.

See also

• Schema version control semantics.
• Build a migration.
• Use lenses.

Bridge to git

The git bridge stores a panproto repository beside a source repository and can translate history between the two systems.

Prerequisites

A git repository (the host project) and either a .panproto/ directory inside it or a sibling panproto repository.

The task

Sidecar mode

The simplest setup: keep .panproto/ next to .git/. Both are tracked by their own tools; commits to either are independent.

git add .panproto/
git commit -m "snapshot panproto state"

The object names are content hashes, so unchanged objects deduplicate. Git can still report conflicts in refs or other mutable files under .panproto/; do not edit stored object contents by hand.

Bidirectional translation

schema git export writes the current panproto history into a destination git repository:

schema git export path/to/output-git-repo --repo .

schema git import path/to/git-repo HEAD currently imports into an in-memory store, prints the imported count and temporary panproto ID, then exits without updating .panproto/. Use it only as a diagnostic until the command accepts a persistent destination. Export opens --repo, creates or opens the destination, and writes the current HEAD.

git-remote helper

The panproto-git-remote crate ships git-remote-panproto, a remote helper for a panproto node reached over XRPC. After installing that binary, a node URL has the form panproto://did:plc:abc123/repository-name; a local filesystem path is not a valid substitute. See crates/panproto-git-remote.

Merge bridging

A git merge that touches .panproto/ merges files, not schemas. Perform schema-level work with schema merge, then export the resulting history. The CLI has no automatic translation from a git merge to a structural schema merge.

Verification

schema status
git status

Inspect both outputs independently. Panproto status concerns its current branch and staged schema; git status concerns files in the host repository. Either side can be dirty while the other is clean.

Common mistakes

• Three-way text-merging .panproto/objects/ files. Re-run the schema operation in panproto, then export the result.
• Mixing the two modes. Choose sidecar or remote-bridge per project; mixing creates ambiguity about which DAG is the source of truth.

See also

• Schema version control semantics.
• Init and commit.
• Branch and merge.

Translate across protocols

panproto has two different cross-protocol cases. The TypeScript SDK can apply an explicit vertex-and-edge mapping between two protocol-tagged schema handles. It does not construct a shared theory or emit a complete target-language document. The CLI does not expose that limited two-protocol path: each --protocol argument selects one protocol for both schemas, and the current CLI resolver accepts only atproto.

Decide whether the task is supported

Use Convert data between schemas when both schemas use atproto and are already stored as panproto schema JSON. For a small explicit map in TypeScript, build both schema handles, map every relevant vertex and edge, and compile the migration as shown in Cross-protocol translation. checkExistence selects the source schema’s registered protocol, so that report does not establish validity under both protocols. The result of liftJson is target-shaped JSON, not a complete OpenAPI, Protobuf, or other target document.

A general bridge requires repository-level implementation: a shared protocol theory, explicit source and target translations into that theory, and format-specific parsing and emission at the boundaries.

The theory DSL can compile a colimit of building-block theories, but compilation alone does not register a runtime protocol or translate existing JSON Schema, Protobuf, ATProto, or other built-in schemas into the result. Thus a DSL compose document is only one component of a cross-protocol bridge.

Implement a bridge in Rust

The supported building blocks are available in Rust:

1. Define the shared theory and its instance theory, then register both under stable names.
2. Define a Protocol whose schema_theory and instance_theory use those names.
3. Parse each source format with its protocol-specific parser, and write an explicit schema translation into the shared protocol.
4. Build and check a migration between the translated schemas.
5. Parse source records, apply the migration or lens, then serialize with the target format’s emitter.

Each translation in steps 3 and 5 is format-specific code. panproto does not infer those boundary translations from the fact that two protocol theories share sorts with names such as Vertex or Edge.

Verify the bridge

Test the three boundaries separately: source parsing into the shared schema, migration or lens laws over representative instances, and target emission followed by the target protocol’s parser. Constraints with no representation in the shared theory must be reported or handled explicitly; no current generic command detects and reports every such loss.

CLI boundaries

The following patterns do not provide cross-protocol translation:

• schema data convert --protocol <name> accepts one protocol name and loads both schemas under it. The current resolver accepts only atproto.
• schema lens generate --protocol <name> likewise resolves one protocol for the entire lens, again only atproto in the current CLI.
• schema theory compile validates and compiles a theory document but does not add it to the running CLI’s built-in protocol lookup.

See also

• Build a custom protocol for the repository changes needed to register a protocol.
• Composing protocols by colimit for the theory construction.
• Convert data between schemas for the supported single-protocol path.

Continuous integration

Add CI after schemas validate locally. The smallest useful gate classifies compatibility; local hooks and a hosted workflow apply the same checks earlier and on every pull request.

See also

• Schema version control semantics.
• What panproto verifies.

Breaking-change gate

A breaking-change gate fails CI when a pull request introduces a schema change that panproto classifies as breaking. The gate compares the proposed schema with the merge base on main.

Prerequisites

A panproto repository under git. A CI system that can run shell commands.

The task

schema compat classifies the diff between two schema versions and sets its exit code by tier: 0 for a non-breaking change, 1 for a breaking change, and 2 for a usage or load error. Pair it with schema check --typecheck when the repository also stores an explicit migration mapping; that second command checks the mapping’s existence conditions and theory-level types.

# In your CI script.
git fetch origin main
base_commit=$(git merge-base HEAD origin/main)
git show "$base_commit:schemas/user.json" > /tmp/user-base.json

# Classify the change; exit 1 means breaking, exit 2 a usage or load error.
schema compat /tmp/user-base.json schemas/user.json --protocol atproto

# Check the explicit mapping and its theory-level types.
schema check \
  --src /tmp/user-base.json \
  --tgt schemas/user.json \
  --mapping migrations/user.json \
  --typecheck

Either step’s non-zero exit fails the build. To allow an explicit override, gate on a commit-message marker or a PR label:

if git log -1 --format=%B | grep -q '\[breaking-change-acknowledged\]'; then
  schema compat /tmp/user-base.json schemas/user.json --protocol atproto || true
  schema check \
    --src /tmp/user-base.json \
    --tgt schemas/user.json \
    --mapping migrations/user.json \
    --typecheck || true
else
  schema compat /tmp/user-base.json schemas/user.json --protocol atproto
  schema check \
    --src /tmp/user-base.json \
    --tgt schemas/user.json \
    --mapping migrations/user.json \
    --typecheck
fi

For machine-readable output, add --format json to schema compat. The CLI JSON and the Rust and Python reports include a three-way classification field, breaking and non-breaking lists, and a compatible boolean. The TypeScript CompatReport exposes isCompatible, isBreaking, breakingChanges, and nonBreakingChanges; call toJson() when the three-way classification string is needed.

Verification

Open a PR that adds a backward-compatible field, and the gate passes. A PR that drops a required field fails. Adding [breaking-change-acknowledged] to the commit message lets the gate pass with a warning.

Common mistakes

• Running schema check without a maintained mapping file. Compatibility classification needs only the two schemas; mapping checks are an additional gate for repositories that version migrations.
• Comparing against the wrong base. The gate must compare against the merge base of the PR and main, not against main’s tip; otherwise force-pushes to main make every PR look breaking.

See also

• GitHub Actions for a hosted workflow.
• Pre-commit hooks for catching breakage before push.
• Build a migration.

GitHub Actions

Add this workflow to validate schemas and classify compatibility on every pull request.

Prerequisites

A panproto repository on GitHub. This example assumes schemas/*.json contains panproto’s serialized schema format rather than external schema-language documents.

The task

# .github/workflows/panproto.yml
name: panproto

on:
  pull_request:
    paths:
      - 'schemas/**'
      - 'migrations/**'
      - 'panproto.toml'

jobs:
  validate:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
        with:
          fetch-depth: 0           # need history for the diff base

      - name: Install schema
        run: cargo install panproto-cli --version 0.72.0 --locked

      - name: Validate
        run: |
          for f in schemas/*.json; do
            schema validate --protocol atproto "$f"
          done

      - name: Breaking-change gate
        run: |
          base=$(git merge-base origin/${{ github.base_ref }} HEAD)
          git show "$base:schemas/user.json" > /tmp/base.json
          schema compat /tmp/base.json schemas/user.json --protocol atproto
          schema check --src /tmp/base.json --tgt schemas/user.json \
            --mapping migrations/user.json --typecheck

The --protocol flag is required for every per-file schema validate. There is no --project flag. For an external document such as a Lexicon, use the appropriate parse path before this validation step.

The job has separate validation and breaking-change steps. Validation fails on a malformed schema; schema compat gives the gate its compatibility exit code, and schema check --typecheck rejects an invalid migration mapping.

Verification

After a pull request is pushed, validation exits zero when every schema passes. The compatibility gate prints its classification and exits nonzero for a breaking change.

Common mistakes

• Omitting fetch-depth: 0. Shallow clones make the merge-base lookup fail; the gate then runs against the wrong base.
• Leaving the CLI version unpinned. Update the pinned version deliberately and review any compatibility-classifier changes with the update.

See also

• Breaking-change gate for the underlying mechanic.
• Pre-commit hooks for the local-side equivalent.

Pre-commit hooks

A pre-commit hook rejects malformed staged schemas before they enter the history. This example validates the bytes in the index, so an unstaged working-tree edit cannot change the result.

Prerequisites

The schema CLI installed. A git repository.

The task

Plain git hook

# .git/hooks/pre-commit
#!/usr/bin/env bash
set -euo pipefail

changed=$(git diff --cached --name-only --diff-filter=ACM | grep -E '^schemas/.*\.json$' || true)
[ -z "$changed" ] && exit 0
staged_file=$(mktemp)
base_file=$(mktemp)
trap 'rm -f "$staged_file" "$base_file"' EXIT

while IFS= read -r f; do
  git show ":$f" > "$staged_file"
  schema validate --protocol atproto "$staged_file"

  # Optional warning against the tracked upstream copy.
  if git show "@{u}:$f" > "$base_file" 2>/dev/null && \
     ! schema compat "$base_file" "$staged_file" --protocol atproto; then
    echo "warning: compatibility check failed for $f" >&2
  fi
done <<< "$changed"

chmod +x .git/hooks/pre-commit installs it.

With pre-commit framework

# .pre-commit-config.yaml
repos:
  - repo: local
    hooks:
      - id: schema-validate
        name: panproto schema validate
        entry: schema validate --protocol atproto
        language: system
        files: '^schemas/.*\.json$'

The hook receives the staged file paths as positional arguments; the --protocol flag is required.

pre-commit install activates it.

Verification

Stage a malformed schema and try to commit. The hook rejects it. After the schema is fixed, the next commit passes.

Common mistakes

• Silently skipping a missing schema binary. Prefer a failing hook with an installation message; CI remains the authoritative gate when contributors may bypass hooks.
• Validating every file on every commit. The script above scopes to staged schemas/*.json only; broader scopes are noisy.

See also

• Breaking-change gate for the CI-side equivalent.
• Reference: CLI.

Reference

Use these pages to look up a flag, field, signature, protocol, or grammar. Procedures live in the how-to guides. The mathematical model lives in explanation.

Operational contracts

SDK contracts

Intermediate lookup

The expression-language reference lists the surface grammar, types, builtins, and errors used by queries and field transforms. The lens-combinator reference lists optic kinds, constructor families, complement composition, and protolens instantiation.

Advanced lookup

The crate map groups the panproto-* workspace crates by dependency role and lists the main feature-gated edges. Use it when the facade does not expose the layer an extension needs.

CLI reference

Every schema subcommand, with its full --help text. This page is regenerated from the live binary by xtask/src/bin/gen-cli-docs.rs; edit the CLI, not the page.

To regenerate locally:

cargo run -p xtask --bin gen-cli-docs

CI runs the same command and fails if the result differs from what is checked in.

For the model that the commands operate on, see Schemas as theories, Migrations as morphisms, and Schema version control semantics.

Discovering a migration

schema auto-migrate runs one search over spans. Write the apex as $A$; the two legs have the shape

$$old\stackrel{\ell }{\leftarrow }A\stackrel{r}{\to }new.$$

The apex is the sub-schema of old whose vertices found a target in new. That search never refuses for want of a match: leaving every source vertex out of the apex is always feasible, so two schemas with nothing in common come back with an empty apex rather than with an error. Two of the three flags below thus select which of its answers counts as an answer, and the search underneath is the same one either way; the third constrains the search itself.

--span accepts every answer, the empty apex included. Without it the command accepts a span covering at least one source vertex and reports the empty apex as a failure naming the two files.

--total accepts only a span whose left leg is onto, which is to say a total morphism. Totality is a condition on the edges as well as the vertices, so an apex holding every source vertex is not on its own enough: a source arc that found no image in the target leaves the answer partial at full vertex coverage. The command does not read that off the span alone. An optimal span that drops a vertex is no evidence about whether a total morphism exists, because span quality excludes the drop count while the objective is lexicographic in quality first and drops second, so a span that drops a vertex can score strictly better than a total morphism that keeps it. When the optimal span is not total, the command runs the total-morphism search before giving up. The command fails only when that second search returns no total morphism. Its error includes the coverage reached by the span. --total and --span conflict, and the pair is rejected before either search runs.

--monic constrains the search rather than the acceptance, so it composes with either of the others. It requires the vertex map to be injective, so that no two source vertices land on the same target. Injectivity on vertices does not force injectivity on edges, and a monic answer may still send two parallel source edges to one target edge. When the answer is not injective on vertices, the command says so on stderr, since a migration identifying two source vertices has no well-defined lift without a rule for combining them.

The human report opens with the shape, the score, and the interval the search certified, then sizes the apex:

Found span (quality: 0.812, bounds: [0.812, 0.884]):

Apex: 7 of 9 vertices (77.8% coverage), 6 edges

The bounds collapse to a point exactly when the answer was proved optimal. When they do not, a following line records that the search stopped before it could rule out a better span, which is what separates a quality of 0.812 that nothing beats from a quality of 0.812 the search never got to improve on. Underneath come the right leg’s vertex map and, when it has one, its edge map. A total morphism recovered by the second search prints a shorter report, with no apex line and no bounds, because it carries neither.

--json writes the span’s right leg, a migration out of the apex, to stdout. Warnings stay on stderr, so the output pipes.

schema

Schematic version control: schema migration toolkit based on generalized algebraic theories

Usage: schema [OPTIONS] <COMMAND>

Commands:
  validate      Validate a schema against a protocol
  check         Check existence conditions for a migration between two schemas
  compat        Classify backward-compatibility between two schema versions
  scaffold      Generate minimal test data from a protocol theory using free model construction
  normalize     Simplify a schema by merging equivalent elements
  typecheck     Type-check a migration between two schemas at the GAT level
  verify        Verify that a schema satisfies its protocol theory's equations
  init          Initialize a new panproto repository
  add           Stage a schema for the next commit
  commit        Create a new commit from staged changes
  status        Show repository status
  log           Show commit history
  diff          Diff two schemas or show staged changes
  show          Inspect a commit, schema, or migration object
  branch        Create, list, or delete branches
  tag           Create, list, or delete tags
  checkout      Switch to a branch or commit
  merge         Merge a branch into the current branch
  rebase        Replay current branch onto another
  cherry-pick   Apply a single commit's migration to the current branch
  reset         Move HEAD / unstage / restore
  stash         Save or restore working state
  reflog        Show ref mutation history
  bisect        Binary search for the commit that introduced a breaking change
  blame         Show which commit introduced a schema element
  lift          Apply a migration to a record, transforming it from source to target schema
  integrate     Integrate two schemas by computing their pushout
  auto-migrate  Automatically discover a migration between two schemas
  gc            Garbage collect unreachable objects
  expr          Evaluate, type-check, or interactively explore GAT expressions
  enrich        Add, list, or remove schema enrichments (defaults, coercions, mergers, policies)
  remote        Add, list, or remove remote repositories
  push          Push schemas to a remote repository
  pull          Pull schemas from a remote repository
  fetch         Fetch schemas from a remote repository
  clone         Clone a remote repository
  data          Data operations: migrate, convert, sync, and status
  theory        Theory DSL operations: define theories, morphisms, and protocols from data files
  lens          Bidirectional lens operations
  parse         Parse source files into full-AST schemas via tree-sitter
  git           Import/export between git repositories and panproto-vcs
  help          Print this message or the help of the given subcommand(s)

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help
  -V, --version  Print version

schema validate

Validate a schema against a protocol

Usage: schema validate [OPTIONS] --protocol <PROTOCOL> <SCHEMA>

Arguments:
  <SCHEMA>  Path to the schema JSON file

Options:
      --protocol <PROTOCOL>  The protocol name (e.g., "atproto")
  -v, --verbose              Enable verbose output
  -h, --help                 Print help

schema check

Check existence conditions for a migration between two schemas

Usage: schema check [OPTIONS] --src <SRC> --tgt <TGT> --mapping <MAPPING>

Options:
      --src <SRC>          Path to the source schema JSON file
  -v, --verbose            Enable verbose output
      --tgt <TGT>          Path to the target schema JSON file
      --mapping <MAPPING>  Path to the migration mapping JSON file
      --typecheck          Also type-check the migration morphism at the GAT level
  -h, --help               Print help

schema compat

Classify backward-compatibility between two schema versions.

Runs a structural diff then classifies it against the named protocol, printing the changes grouped by tier. Exit codes: `0` when no breaking changes are found, `1` when at least one breaking change is found, and `2` on a usage or load error (unreadable file, unknown protocol, or bad `--format`).

Usage: schema compat [OPTIONS] --protocol <PROTOCOL> <OLD> <NEW>

Arguments:
  <OLD>
          Path to the old schema JSON file

  <NEW>
          Path to the new schema JSON file

Options:
      --protocol <PROTOCOL>
          The protocol name (e.g., "atproto")

  -v, --verbose
          Enable verbose output

      --format <FORMAT>
          Output format: `text` (default) or `json`
          
          [default: text]

  -h, --help
          Print help (see a summary with '-h')

schema scaffold

Generate minimal test data from a protocol theory using free model construction

Usage: schema scaffold [OPTIONS] --protocol <PROTOCOL> <SCHEMA>

Arguments:
  <SCHEMA>  Path to the schema JSON file

Options:
      --protocol <PROTOCOL>    The protocol name (e.g., "atproto")
  -v, --verbose                Enable verbose output
      --depth <DEPTH>          Maximum term generation depth (default: 3) [default: 3]
      --max-terms <MAX_TERMS>  Maximum terms per sort (default: 1000) [default: 1000]
      --json                   Output as JSON
  -h, --help                   Print help

schema normalize

Simplify a schema by merging equivalent elements

Usage: schema normalize [OPTIONS] --protocol <PROTOCOL> <SCHEMA>

Arguments:
  <SCHEMA>  Path to the schema JSON file

Options:
      --protocol <PROTOCOL>         The protocol name (e.g., "atproto")
  -v, --verbose                     Enable verbose output
      --identify <IDENTIFICATIONS>  Pairs of elements to identify, as "A=B"
      --json                        Output as JSON
  -h, --help                        Print help

schema typecheck

Type-check a migration between two schemas at the GAT level

Usage: schema typecheck [OPTIONS] --src <SRC> --tgt <TGT> --migration <MIGRATION>

Options:
      --src <SRC>              Path to the source schema JSON file
  -v, --verbose                Enable verbose output
      --tgt <TGT>              Path to the target schema JSON file
      --migration <MIGRATION>  Path to the migration mapping JSON file
  -h, --help                   Print help

schema verify

Verify that a schema satisfies its protocol theory's equations

Usage: schema verify [OPTIONS] --protocol <PROTOCOL> <SCHEMA>

Arguments:
  <SCHEMA>
          Path to the schema JSON file

Options:
      --protocol <PROTOCOL>
          The protocol name (e.g., "atproto")

  -v, --verbose
          Enable verbose output

      --max-assignments <MAX_ASSIGNMENTS>
          Maximum assignments to check per equation (default: 10000)
          
          [default: 10000]

      --format <FORMAT>
          Output format: `text` (default) or `json`
          
          [default: text]

      --allow-incomplete
          Exit zero when a theory could not be checked at all.
          
          A theory that does not typecheck, or one whose assignment enumeration exhausted `--max-assignments`, establishes nothing about the schema. By default that is an error, since treating it as a pass reports a schema verified that was never examined. This accepts it for exploratory use; the output still says the run was incomplete.

  -h, --help
          Print help (see a summary with '-h')

schema init

Initialize a new panproto repository

Usage: schema init [OPTIONS] [PATH]

Arguments:
  [PATH]  Directory to initialize (defaults to current dir) [default: .]

Options:
  -b, --initial-branch <INITIAL_BRANCH>  Use the given name for the initial branch
  -v, --verbose                          Enable verbose output
  -h, --help                             Print help

schema add

Stage a schema for the next commit

Usage: schema add [OPTIONS] <SCHEMA>

Arguments:
  <SCHEMA>
          Path to the schema JSON file

Options:
  -n, --dry-run
          Show what would be staged without actually staging

  -v, --verbose
          Enable verbose output

  -f, --force
          Force staging even if validation fails

      --data <DATA>
          Stage data files alongside the schema

      --skip-verify
          Skip GAT migration validation, and the check of staged data against its schema, while staging.
          
          Leaves the stage pending, which a default `commit` refuses; the migration is still recorded, and data files are still parsed, since a data set cannot be recorded under a schema its bytes cannot be read against.

  -h, --help
          Print help (see a summary with '-h')

schema commit

Create a new commit from staged changes

Usage: schema commit [OPTIONS] --message <MESSAGE>

Options:
  -m, --message <MESSAGE>  Commit message
  -v, --verbose            Enable verbose output
      --author <AUTHOR>    Author name [default: anonymous]
      --amend              Amend the previous commit instead of creating a new one
      --allow-empty        Allow creating a commit with no changes
      --skip-verify        Skip GAT equation verification
  -h, --help               Print help

schema status

Show repository status

Usage: schema status [OPTIONS]

Options:
  -s, --short        Show output in short format
  -v, --verbose      Enable verbose output
      --porcelain    Show output in machine-readable format
  -b, --branch       Show branch information
      --data <DATA>  Show data staleness for files in this directory
  -h, --help         Print help

schema log

Show commit history

Usage: schema log [OPTIONS]

Options:
  -n, --limit <LIMIT>    Maximum number of commits to show
  -v, --verbose          Enable verbose output
      --oneline          Show each commit on a single line
      --graph            Show an ASCII graph of the branch structure
      --all              Show all branches
      --format <FORMAT>  Pretty-print commits using a format string
      --author <AUTHOR>  Filter commits by author
      --grep <GREP>      Filter commits whose message matches a pattern
      --data             Show data and complement IDs in commit history
  -h, --help             Print help

schema diff

Diff two schemas or show staged changes

Usage: schema diff [OPTIONS] [OLD] [NEW]

Arguments:
  [OLD]  Path to the old schema (or first ref)
  [NEW]  Path to the new schema (or second ref)

Options:
      --stat            Show a diffstat summary
  -v, --verbose         Enable verbose output
      --name-only       Show only names of changed elements
      --name-status     Show names and status (A/D/M) of changed elements
      --staged          Diff the staged schema against HEAD
      --detect-renames  Detect likely renames between schemas
      --theory          Show theory-level diff (sorts, operations, equations)
      --lens            Also generate a protolens chain between the schemas
      --save <SAVE>     Save the protolens chain to a file (requires --lens)
      --optic-kind      Show the optic classification of the diff
  -h, --help            Print help

schema show

Inspect a commit, schema, or migration object

Usage: schema show [OPTIONS] <TARGET>

Arguments:
  <TARGET>  Ref name or object ID

Options:
      --format <FORMAT>  Pretty-print using a format string
  -v, --verbose          Enable verbose output
      --stat             Show a diffstat summary for commits
  -h, --help             Print help

schema branch

Create, list, or delete branches

Usage: schema branch [OPTIONS] [NAME]

Arguments:
  [NAME]  Branch name to create. Lists branches if omitted

Options:
  -d, --delete         Delete the branch
  -D                   Force-delete the branch even if not fully merged
  -f, --force          Force overwrite if branch already exists
  -m, --move <RENAME>  Rename a branch (value is the new name)
  -v, --verbose        Show commit info for each branch
  -a, --all            List both local and remote-tracking branches
  -h, --help           Print help

schema tag

Create, list, or delete tags

Usage: schema tag [OPTIONS] [NAME]

Arguments:
  [NAME]  Tag name to create. Lists tags if omitted

Options:
  -d, --delete             Delete the tag
  -v, --verbose            Enable verbose output
  -a, --annotate           Create an annotated tag
  -m, --message <MESSAGE>  Tag message (implies --annotate)
  -l, --list               List tags matching a pattern
  -f, --force              Force-replace an existing tag
  -h, --help               Print help

schema checkout

Switch to a branch or commit

Usage: schema checkout [OPTIONS] <TARGET>

Arguments:
  <TARGET>  Branch name or commit ID

Options:
  -b                       Create a new branch with the given name at HEAD and switch to it
  -v, --verbose            Enable verbose output
      --detach             Detach HEAD at the target commit
      --migrate <MIGRATE>  Migrate data in this directory to match the target branch's schema
  -h, --help               Print help

schema merge

Merge a branch into the current branch

Usage: schema merge [OPTIONS] [BRANCH]

Arguments:
  [BRANCH]  Branch to merge

Options:
      --author <AUTHOR>    Author name [default: anonymous]
      --no-commit          Perform the merge but do not commit
      --ff-only            Refuse to merge unless fast-forward is possible
      --no-ff              Create a merge commit even for fast-forward merges
      --squash             Squash the branch into a single change set
      --abort              Abort an in-progress merge
  -m, --message <MESSAGE>  Custom merge commit message
  -v, --verbose            Show pullback-based overlap detection details
      --migrate <MIGRATE>  Migrate data in this directory through the merge
  -h, --help               Print help

schema rebase

Replay current branch onto another

Usage: schema rebase [OPTIONS] [ONTO]

Arguments:
  [ONTO]  Branch or commit to rebase onto

Options:
      --author <AUTHOR>  Author name [default: anonymous]
  -v, --verbose          Enable verbose output
      --abort            Abort the current rebase operation
      --cont             Continue a paused rebase after resolving conflicts
  -h, --help             Print help

schema cherry-pick

Apply a single commit's migration to the current branch

Usage: schema cherry-pick [OPTIONS] [COMMIT]

Arguments:
  [COMMIT]  Commit ID to cherry-pick

Options:
      --author <AUTHOR>  Author name [default: anonymous]
  -v, --verbose          Enable verbose output
  -n, --no-commit        Apply the change without committing
  -x                     Append "(cherry picked from commit ...)" to the message
      --abort            Abort the current cherry-pick operation
  -h, --help             Print help

schema reset

Move HEAD / unstage / restore

Usage: schema reset [OPTIONS] <TARGET>

Arguments:
  <TARGET>  Target ref or commit ID

Options:
      --soft             Soft reset: move HEAD only, keep staged and working changes
  -v, --verbose          Enable verbose output
      --hard             Hard reset: move HEAD, discard all changes
      --author <AUTHOR>  Author name [default: anonymous]
  -h, --help             Print help

schema stash

Save or restore working state

Usage: schema stash [OPTIONS] <COMMAND>

Commands:
  push   Save the current staged schema
  pop    Restore the most recent stash
  list   List all stash entries
  drop   Drop the most recent stash
  apply  Apply a stash entry without removing it
  show   Show the contents of a stash entry
  clear  Remove all stash entries
  help   Print this message or the help of the given subcommand(s)

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema stash push

Save the current staged schema

Usage: schema stash push [OPTIONS]

Options:
  -m, --message <MESSAGE>  Optional stash message
  -v, --verbose            Enable verbose output
      --author <AUTHOR>    Author name [default: anonymous]
  -h, --help               Print help

schema stash pop

Restore the most recent stash

Usage: schema stash pop [OPTIONS]

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema stash list

List all stash entries

Usage: schema stash list [OPTIONS]

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema stash drop

Drop the most recent stash

Usage: schema stash drop [OPTIONS]

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema stash apply

Apply a stash entry without removing it

Usage: schema stash apply [OPTIONS] [INDEX]

Arguments:
  [INDEX]  Stash index to apply [default: 0]

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema stash show

Show the contents of a stash entry

Usage: schema stash show [OPTIONS] [INDEX]

Arguments:
  [INDEX]  Stash index to inspect [default: 0]

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema stash clear

Remove all stash entries

Usage: schema stash clear [OPTIONS]

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema reflog

Show ref mutation history

Usage: schema reflog [OPTIONS] [REF_NAME]

Arguments:
  [REF_NAME]  Ref name (defaults to HEAD) [default: HEAD]

Options:
  -n, --limit <LIMIT>  Maximum entries to show
  -v, --verbose        Enable verbose output
      --all            Show reflogs for all refs
  -h, --help           Print help

schema bisect

Binary search for the commit that introduced a breaking change

Usage: schema bisect [OPTIONS] <GOOD> <BAD>

Arguments:
  <GOOD>  Known good commit
  <BAD>   Known bad commit

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema blame

Show which commit introduced a schema element

Usage: schema blame [OPTIONS] --element-type <ELEMENT_TYPE> <ELEMENT_ID>

Arguments:
  <ELEMENT_ID>  Element identifier (vertex ID, edge `"src->tgt"`, or `"vertex_id:sort"`)

Options:
      --element-type <ELEMENT_TYPE>  Element type: vertex, edge, or constraint
  -v, --verbose                      Enable verbose output
      --reverse                      Walk history from the first commit forward
  -h, --help                         Print help

schema lift

Apply a migration to a record, transforming it from source to target schema

Usage: schema lift [OPTIONS] --migration <MIGRATION> --src-schema <SRC_SCHEMA> --tgt-schema <TGT_SCHEMA> <RECORD>

Arguments:
  <RECORD>  Path to the record JSON file

Options:
      --migration <MIGRATION>          Path to the migration mapping JSON file
  -v, --verbose                        Enable verbose output
      --src-schema <SRC_SCHEMA>        Path to the source schema JSON file
      --tgt-schema <TGT_SCHEMA>        Path to the target schema JSON file
      --direction <DIRECTION>          Migration direction: restrict (default, filtered source-to-target), sigma (source-to-target `Sigma_F`), or pi (source-to-target; W-type `pi` only relabels vertex-injective mappings) [default: restrict]
      --instance-type <INSTANCE_TYPE>  Instance type: wtype (default) or functor [default: wtype]
  -h, --help                           Print help

schema integrate

Integrate two schemas by computing their pushout

Usage: schema integrate [OPTIONS] <LEFT> <RIGHT>

Arguments:
  <LEFT>   Path to the left schema JSON file
  <RIGHT>  Path to the right schema JSON file

Options:
      --auto-overlap  Automatically discover the overlap between schemas
  -v, --verbose       Enable verbose output
      --json          Output the integrated schema as JSON
  -h, --help          Print help

schema auto-migrate

Automatically discover a migration between two schemas

Usage: schema auto-migrate [OPTIONS] <OLD> <NEW>

Arguments:
  <OLD>  Path to the old/source schema JSON file
  <NEW>  Path to the new/target schema JSON file

Options:
      --monic    Require injective (one-to-one) vertex mapping
  -v, --verbose  Enable verbose output
      --total    Require a total morphism; fail on a partial answer
      --span     Report the span even when it covers nothing at all
      --json     Output the span's right leg, a migration out of the apex, as JSON
  -h, --help     Print help

schema gc

Garbage collect unreachable objects

Usage: schema gc [OPTIONS]

Options:
      --dry-run  Show what would be deleted without actually deleting
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema expr

Evaluate, type-check, or interactively explore GAT expressions

Usage: schema expr [OPTIONS] <COMMAND>

Commands:
  gat-eval   Evaluate a JSON-encoded GAT term from a file
  gat-check  Type-check a JSON-encoded GAT term from a file
  repl       Interactive expression REPL
  parse      Parse a Haskell-style expression and print its AST
  eval       Parse and evaluate a Haskell-style expression, printing the result
  fmt        Parse an expression and pretty-print it back in canonical form
  check      Parse an expression and report any syntax errors
  help       Print this message or the help of the given subcommand(s)

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema expr gat-eval

Evaluate a JSON-encoded GAT term from a file

Usage: schema expr gat-eval [OPTIONS] <FILE>

Arguments:
  <FILE>  Path to the JSON file containing a GAT term

Options:
      --env <ENV>  Path to a JSON file with variable bindings
  -v, --verbose    Enable verbose output
  -h, --help       Print help

schema expr gat-check

Type-check a JSON-encoded GAT term from a file

Usage: schema expr gat-check [OPTIONS] <FILE>

Arguments:
  <FILE>  Path to the JSON file containing term, theory, and context

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema expr repl

Interactive expression REPL

Usage: schema expr repl [OPTIONS]

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema expr parse

Parse a Haskell-style expression and print its AST

Usage: schema expr parse [OPTIONS] <SOURCE>

Arguments:
  <SOURCE>  Expression source text

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema expr eval

Parse and evaluate a Haskell-style expression, printing the result

Usage: schema expr eval [OPTIONS] <SOURCE>

Arguments:
  <SOURCE>  Expression source text

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema expr fmt

Parse an expression and pretty-print it back in canonical form

Usage: schema expr fmt [OPTIONS] <SOURCE>

Arguments:
  <SOURCE>  Expression source text

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema expr check

Parse an expression and report any syntax errors

Usage: schema expr check [OPTIONS] <SOURCE>

Arguments:
  <SOURCE>  Expression source text

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema enrich

Add, list, or remove schema enrichments (defaults, coercions, mergers, policies)

Usage: schema enrich [OPTIONS] <COMMAND>

Commands:
  add-default   Add a default value expression to a vertex
  add-coercion  Add a coercion expression between two vertex kinds
  add-merger    Add a merger expression to a vertex
  add-policy    Add a conflict policy to a vertex
  list          List all enrichments on the HEAD schema
  remove        Remove an enrichment by name
  help          Print this message or the help of the given subcommand(s)

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema enrich add-default

Add a default value expression to a vertex

Usage: schema enrich add-default [OPTIONS] --expr <EXPR> <VERTEX>

Arguments:
  <VERTEX>  Vertex name

Options:
      --expr <EXPR>  Default value as JSON
  -v, --verbose      Enable verbose output
  -h, --help         Print help

schema enrich add-coercion

Add a coercion expression between two vertex kinds

Usage: schema enrich add-coercion [OPTIONS] --expr <EXPR> <FROM> <TO>

Arguments:
  <FROM>  Source vertex kind
  <TO>    Target vertex kind

Options:
      --expr <EXPR>  Coercion expression as JSON
  -v, --verbose      Enable verbose output
  -h, --help         Print help

schema enrich add-merger

Add a merger expression to a vertex

Usage: schema enrich add-merger [OPTIONS] --expr <EXPR> <VERTEX>

Arguments:
  <VERTEX>  Vertex name

Options:
      --expr <EXPR>  Merger specification as JSON
  -v, --verbose      Enable verbose output
  -h, --help         Print help

schema enrich add-policy

Add a conflict policy to a vertex

Usage: schema enrich add-policy [OPTIONS] --strategy <STRATEGY> <VERTEX>

Arguments:
  <VERTEX>  Vertex name

Options:
      --strategy <STRATEGY>  Conflict resolution strategy name
  -v, --verbose              Enable verbose output
  -h, --help                 Print help

schema enrich list

List all enrichments on the HEAD schema

Usage: schema enrich list [OPTIONS]

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema enrich remove

Remove an enrichment by name

Usage: schema enrich remove [OPTIONS] <NAME>

Arguments:
  <NAME>  Enrichment name or vertex name to remove enrichments from

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema remote

Add, list, or remove remote repositories

Usage: schema remote [OPTIONS] <COMMAND>

Commands:
  add     Register a new remote
  remove  Remove a remote
  list    List configured remotes
  help    Print this message or the help of the given subcommand(s)

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema remote add

Register a new remote

Usage: schema remote add [OPTIONS] <NAME> <URL>

Arguments:
  <NAME>  Remote name
  <URL>   Remote URL

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema remote remove

Remove a remote

Usage: schema remote remove [OPTIONS] <NAME>

Arguments:
  <NAME>  Remote name to remove

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema remote list

List configured remotes

Usage: schema remote list [OPTIONS]

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema push

Push schemas to a remote repository

Usage: schema push [OPTIONS] [REMOTE] [BRANCH]

Arguments:
  [REMOTE]  Remote name
  [BRANCH]  Branch to push

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema pull

Pull schemas from a remote repository

Usage: schema pull [OPTIONS] [REMOTE] [BRANCH]

Arguments:
  [REMOTE]  Remote name
  [BRANCH]  Branch to pull

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema fetch

Fetch schemas from a remote repository

Usage: schema fetch [OPTIONS] [REMOTE]

Arguments:
  [REMOTE]  Remote name

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema clone

Clone a remote repository

Usage: schema clone [OPTIONS] <URL> [PATH]

Arguments:
  <URL>   Repository URL
  [PATH]  Local path

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema data

Data operations: migrate, convert, sync, and status

Usage: schema data [OPTIONS] <COMMAND>

Commands:
  migrate  Migrate data to match the current schema version
  convert  Convert data between schemas
  sync     Sync data to match a target schema version via VCS
  status   Report data staleness relative to the current schema version
  help     Print this message or the help of the given subcommand(s)

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema data migrate

Migrate data to match the current schema version

Usage: schema data migrate [OPTIONS] <DATA>

Arguments:
  <DATA>  Data directory containing JSON files

Options:
      --protocol <PROTOCOL>  Protocol name (inferred from HEAD commit if omitted)
  -v, --verbose              Enable verbose output
      --range <RANGE>        Migrate between specific commits (default: parent..HEAD)
      --dry-run              Preview without modifying files
  -o, --output <OUTPUT>      Output directory (default: overwrite in place)
      --backward             Migrate backward (requires stored complement)
      --coverage             Apply migration and print coverage statistics
  -h, --help                 Print help

schema data convert

Convert data between schemas

Usage: schema data convert [OPTIONS] --protocol <PROTOCOL> <DATA>

Arguments:
  <DATA>  Data file or directory of JSON files

Options:
      --from <FROM>            Source schema
  -v, --verbose                Enable verbose output
      --to <TO>                Target schema
      --protocol <PROTOCOL>    Protocol name
      --chain <CHAIN>          Pre-built protolens chain JSON to instantiate with --from and --to
  -o, --output <OUTPUT>        Output file or directory
      --direction <DIRECTION>  Direction: "forward" or "backward" [default: forward]
      --defaults <DEFAULTS>    Default values as key=value pairs
  -h, --help                   Print help

schema data sync

Sync data to match a target schema version via VCS

Usage: schema data sync [OPTIONS] <DATA_DIR>

Arguments:
  <DATA_DIR>  Data directory

Options:
      --edits            Store an edit log object in the VCS
  -v, --verbose          Enable verbose output
      --target <TARGET>  Target ref (default: HEAD)
  -h, --help             Print help

schema data status

Report data staleness relative to the current schema version

Usage: schema data status [OPTIONS] <DATA_DIR>

Arguments:
  <DATA_DIR>  Data directory

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema theory

Theory DSL operations: define theories, morphisms, and protocols from data files

Usage: schema theory [OPTIONS] <COMMAND>

Commands:
  validate             Validate a theory document (load + typecheck)
  compile              Compile a theory document and print results
  compile-dir          Compile all theory documents in a directory
  check-morphism       Validate a morphism document
  recompose            Replay a composition and print the resulting theory
  check-coercion-laws  Run sample-based coercion law checks over every directed equation in a theory document. Exits non-zero when any declared coercion class is falsified by a sample
  repl                 Interactive theory REPL with syntax highlighting and history
  help                 Print this message or the help of the given subcommand(s)

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema theory validate

Validate a theory document (load + typecheck)

Usage: schema theory validate [OPTIONS] <FILE>

Arguments:
  <FILE>  Path to the theory document file (.ncl, .json, .yaml)

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema theory compile

Compile a theory document and print results

Usage: schema theory compile [OPTIONS] <FILE>

Arguments:
  <FILE>  Path to the theory document file

Options:
      --json     Output as JSON
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema theory compile-dir

Compile all theory documents in a directory

Usage: schema theory compile-dir [OPTIONS] <DIR>

Arguments:
  <DIR>  Path to the directory

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema theory check-morphism

Validate a morphism document

Usage: schema theory check-morphism [OPTIONS] <FILE>

Arguments:
  <FILE>  Path to the morphism document file

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema theory recompose

Replay a composition and print the resulting theory

Usage: schema theory recompose [OPTIONS] <FILE>

Arguments:
  <FILE>  Path to the composition document file

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema theory check-coercion-laws

Run sample-based coercion law checks over every directed equation in a theory document. Exits non-zero when any declared coercion class is falsified by a sample

Usage: schema theory check-coercion-laws [OPTIONS] <FILE>

Arguments:
  <FILE>  Path to the theory document file

Options:
      --json                 Output the full report as JSON
  -v, --verbose              Enable verbose output
      --var-name <VAR_NAME>  Name under which each sample is bound in the evaluation environment. Defaults to `"x"`; override when a theory's equations bind a different free variable so the checker does not surface "unbound variable" errors on every sample [default: x]
  -h, --help                 Print help

schema theory repl

Interactive theory REPL with syntax highlighting and history

Usage: schema theory repl [OPTIONS]

Options:
      --load <PATH>  Theory documents to load on startup. Same shape accepted by `:load` inside the REPL
  -v, --verbose      Enable verbose output
  -h, --help         Print help

schema lens

Bidirectional lens operations

Usage: schema lens [OPTIONS] <COMMAND>

Commands:
  generate  Generate a lens between two schemas
  compile   Compile a lens DSL document (.ncl/.json/.yaml) to a protolens chain
  apply     Apply a saved lens chain to data
  compose   Compose two protolens chains or schemas
  verify    Verify lens laws on test data
  inspect   Inspect a saved protolens chain
  check     Check applicability of a chain against schemas in a directory
  lift      Lift a chain along a theory morphism
  help      Print this message or the help of the given subcommand(s)

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema lens generate

Generate a lens between two schemas

Usage: schema lens generate [OPTIONS] --protocol <PROTOCOL> <OLD> <NEW>

Arguments:
  <OLD>
          Path to the old/source schema

  <NEW>
          Path to the new/target schema

Options:
      --protocol <PROTOCOL>
          Protocol name

  -v, --verbose
          Enable verbose output

      --json
          Output as JSON

      --chain
          Output a reusable protolens chain (JSON to stdout)

      --try-overlap
          Try overlap-based alignment when direct morphism fails

      --save <SAVE>
          Save the generated protolens chain to a file

      --defaults <DEFAULTS>
          Default values as key=value pairs

      --fuse
          Fuse multi-step chain into single protolens

      --requirements
          Show complement requirements (defaults/data needed)

      --hints <HINTS>
          Path to a JSON hints file for guided auto-lens generation

      --stringency <TIER>
          Stringency tier governing which alignment strategies run.
          
          Accepted case-insensitively for parity with the Python and WASM bindings, both of which trim and lowercase their input.
          
          strict: `Exact`, `ExactSuffix`, and `EdgeLabel`; total morphism only. balanced: adds `Alias`, `TokenSimilarity`, and `DescriptionSimilarity`; total morphism only (default). lenient: adds `WrapUnwrap`, `TypeSignature`, `WlRefinement`, and `Neighborhood`; spans allowed. exploratory: adds `Structural` and `Coerce` proposals; spans allowed.

          Possible values:
          - strict:      `Exact`, `ExactSuffix`, and `EdgeLabel`; total morphism only
          - balanced:    Adds `Alias`, `TokenSimilarity`, and `DescriptionSimilarity` (default)
          - lenient:     Adds `WrapUnwrap`, `TypeSignature`, `WlRefinement`, and `Neighborhood`; spans allowed
          - exploratory: Adds `Structural` and `Coerce` proposals; spans allowed

      --top-n <N>
          Emit up to N ranked candidate lenses instead of the single best one. Output format switches to a JSON array when combined with `--json` or `--chain`
          
          [default: 1]

      --explain
          Print per-step explanations (and confidences) for each emitted candidate

  -h, --help
          Print help (see a summary with '-h')

schema lens compile

Compile a lens DSL document (.ncl/.json/.yaml) to a protolens chain

Usage: schema lens compile [OPTIONS] <DOC>

Arguments:
  <DOC>  Path to the lens DSL document (`.ncl`, `.json`, `.yaml`, or `.yml`)

Options:
      --body-vertex <BODY_VERTEX>  Parent vertex under which field-level steps attach [default: record:body]
  -v, --verbose                    Enable verbose output
      --out <OUT>                  Write the chain JSON to this file instead of stdout
  -h, --help                       Print help

schema lens apply

Apply a saved lens chain to data

Usage: schema lens apply [OPTIONS] --protocol <PROTOCOL> <CHAIN> <DATA>

Arguments:
  <CHAIN>  Path to the protolens chain JSON
  <DATA>   Path to the data file

Options:
      --protocol <PROTOCOL>      Protocol name
  -v, --verbose                  Enable verbose output
      --direction <DIRECTION>    Direction: "forward" or "backward" [default: forward]
      --complement <COMPLEMENT>  Complement data for backward apply
      --schema <SCHEMA>          Schema for chain instantiation
  -h, --help                     Print help

schema lens compose

Compose two protolens chains or schemas

Usage: schema lens compose [OPTIONS] --protocol <PROTOCOL> <CHAIN1> <CHAIN2>

Arguments:
  <CHAIN1>  First chain or schema file
  <CHAIN2>  Second chain or schema file

Options:
      --protocol <PROTOCOL>  Protocol name
  -v, --verbose              Enable verbose output
      --json                 Output as JSON
      --chain                Output in chain format
  -h, --help                 Print help

schema lens verify

Verify lens laws on test data

Usage: schema lens verify [OPTIONS] --protocol <PROTOCOL> <DATA> <SCHEMA>

Arguments:
  <DATA>    Path to test data file
  <SCHEMA>  Schema used to parse the test data

Options:
      --protocol <PROTOCOL>  Protocol name
  -v, --verbose              Enable verbose output
  -h, --help                 Print help

schema lens inspect

Inspect a saved protolens chain

Usage: schema lens inspect [OPTIONS] --protocol <PROTOCOL> <CHAIN>

Arguments:
  <CHAIN>  Path to the protolens chain JSON

Options:
      --protocol <PROTOCOL>  Protocol name
  -v, --verbose              Enable verbose output
  -h, --help                 Print help

schema lens check

Check applicability of a chain against schemas in a directory

Usage: schema lens check [OPTIONS] --protocol <PROTOCOL> <CHAIN> <SCHEMAS_DIR>

Arguments:
  <CHAIN>        Path to the protolens chain JSON
  <SCHEMAS_DIR>  Directory containing schema JSON files

Options:
      --protocol <PROTOCOL>  Protocol name
  -v, --verbose              Enable verbose output
      --dry-run              Report only, do not instantiate
  -h, --help                 Print help

schema lens lift

Lift a chain along a theory morphism

Usage: schema lens lift [OPTIONS] <CHAIN> <MORPHISM>

Arguments:
  <CHAIN>     Path to the protolens chain JSON
  <MORPHISM>  Path to the theory morphism JSON

Options:
      --json     Output as JSON
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema parse

Parse source files into full-AST schemas via tree-sitter

Usage: schema parse [OPTIONS] <COMMAND>

Commands:
  file     Parse a single source file into a full-AST schema
  project  Parse all files in a directory into a unified project schema
  emit     Parse a file and emit it back to source (round-trip test)
  help     Print this message or the help of the given subcommand(s)

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema parse file

Parse a single source file into a full-AST schema

Usage: schema parse file [OPTIONS] <PATH>

Arguments:
  <PATH>  Path to the source file

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema parse project

Parse all files in a directory into a unified project schema

Usage: schema parse project [OPTIONS] [PATH]

Arguments:
  [PATH]  Path to the project directory [default: .]

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema parse emit

Parse a file and emit it back to source (round-trip test)

Usage: schema parse emit [OPTIONS] <PATH>

Arguments:
  <PATH>  Path to the source file

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema git

Import/export between git repositories and panproto-vcs

Usage: schema git [OPTIONS] <COMMAND>

Commands:
  import  Import a git repository's history into panproto-vcs
  export  Export panproto-vcs history to a git repository
  help    Print this message or the help of the given subcommand(s)

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema git import

Import a git repository's history into panproto-vcs

Usage: schema git import [OPTIONS] <REPO> [REVSPEC]

Arguments:
  <REPO>     Path to the git repository
  [REVSPEC]  Git revspec (e.g. "HEAD", "main", "HEAD~10..HEAD") [default: HEAD]

Options:
  -v, --verbose  Enable verbose output
  -h, --help     Print help

schema git export

Export panproto-vcs history to a git repository

Usage: schema git export [OPTIONS] <DEST>

Arguments:
  <DEST>  Destination path for the git repository

Options:
      --repo <REPO>  Path to the panproto repository (default: current directory) [default: .]
  -v, --verbose      Enable verbose output
  -h, --help         Print help

Rust SDK reference

The Rust entry point is the panproto-core facade. Version 0.72 requires Rust 1.85 or later.

[dependencies]
panproto-core = "0.72"

The facade re-exports each component crate as a module. For instance, panproto_core::schema::Schema is the Schema type from panproto-schema. Depending on panproto-schema directly exposes the same type without the facade.

Modules

The crate map lists lower-level workspace crates that are not re-exported from panproto-core.

Feature flags

panproto-core has no default features.

full-parse adds the tree-sitter grammar build dependencies described in the crate manifest. It is separate from the tree-sitter feature on panproto-io.

Instance transport and direction

Let a compiled migration have schema direction (F:S\to T). The functorial data-migration names (\Sigma_F) and (\Delta_F) follow the usual source and target directions (Spivak 2012), but the plain lift API is a separate operation:

Thus panproto_mig::lift_wtype is not (\Delta_F), despite its delegation to wtype_restrict. Instance::restrict has the same source-to-target surviving-fragment direction. Instance::extend is a total source-to-target extension path. The W-type (\Sigma_F) implementation delegates to that path, but the generic method does not establish an adjunction for every Instance variant.

Morphism search

The panproto_core::mig::hom_search module distinguishes partial overlap from total morphisms. A returned SchemaSpan has shape (S\leftarrow A\to T): (A) is the sub-schema of (S) induced by mapped source vertices, the left leg includes (A) into (S), and the right leg maps (A) into (T).

find_span(
    src: &Schema,
    tgt: &Schema,
    protocol: &Protocol,
    opts: &SearchOptions,
) -> Result<SchemaSpan, SpanError>

find_morphisms(
    src: &Schema,
    tgt: &Schema,
    opts: &SearchOptions,
) -> Result<MorphismList, SpanError>

find_best_morphism(
    src: &Schema,
    tgt: &Schema,
    opts: &SearchOptions,
) -> Result<Option<FoundMorphism>, SpanError>

find_span may return an empty apex when the schemas share no vertices. The protocol argument is used to validate the induced apex. Setting SearchOptions::epic is invalid for this partial search and returns SpanError::EpicIsNotASpanProperty.

find_morphisms returns total morphisms that attain the optimum, rather than every morphism or a sequence of lower-quality alternatives. MorphismList::truncated records whether enumeration of tied optima stopped at the engine cap. An empty morphisms vector means that no total morphism exists. A search that could not run returns Err.

SearchOptions::default() leaves monic, epic, and iso false, uses no hard pins, and sets max_results to zero. Here zero requests all optima the implementation will enumerate, subject to its safety cap. Use find_morphisms_budgeted or SpanSearch when the caller must supply a SearchBudget.

Ownership and errors

Rust values follow ordinary ownership and drop semantics. The Rust API does not expose the opaque-handle lifecycle used by foreign-language bindings. Fallible operations return the error type declared by their component crate. panproto-core does not replace those errors with a facade-wide error enum.

See also

• Install the Rust SDK
• Define a schema from Rust
• Find a span between two schemas
• Searching for a morphism

TypeScript SDK reference

The TypeScript package is @panproto/core. It requires Node.js 20 or later when run under Node and loads the engine through WebAssembly.

npm install @panproto/core

Initialization

import { Panproto } from '@panproto/core';

const panproto = await Panproto.init();

The initialization signature is:

static init(input?: string | URL | WasmGlueModule): Promise<Panproto>

With no argument, init loads the glue and WASM binary bundled with the package. A URL identifies the wasm-bindgen JavaScript glue module, rather than the .wasm file itself. Bundlers may instead pass a pre-imported WasmGlueModule.

Principal exports

The generated declaration file in the package is the signature authority. The table below is an index into that surface.

The source export list is bindings/typescript/src/index.ts. Package consumers should import from @panproto/core, since files under src are not package subpath exports.

Selected signatures

class SchemaBuilder {
  vertex(id: string, kind: string, options?: VertexOptions): SchemaBuilder;
  edge(src: string, tgt: string, kind: string, options?: EdgeOptions): SchemaBuilder;
  constraint(vertexId: string, sort: string, value: string): SchemaBuilder;
  build(): BuiltSchema;
}

class MigrationBuilder {
  map(srcVertex: string, tgtVertex: string): MigrationBuilder;
  mapEdge(srcEdge: Edge, tgtEdge: Edge): MigrationBuilder;
  resolve(srcKind: string, tgtKind: string, resolvedEdge: Edge): MigrationBuilder;
  compile(): CompiledMigration;
}

class CompiledMigration {
  lift(record: unknown): LiftResult;
  get(record: unknown): GetResult;
  put(view: unknown, complement: Uint8Array): LiftResult;
}

LiftResult.data is unknown. GetResult contains view: unknown and complement: Uint8Array. The complement must be passed back unchanged unless an operation explicitly returns a replacement.

If the compiled mapping has schema direction (S\to T), lift accepts an (S)-record and returns the surviving fragment as a (T)-record. It calls Rust’s restrict-based lift_wtype. It is neither the left Kan extension (\Sigma_F) nor precomposition (\Delta_F). get has the same source-to-target direction and additionally captures the complement. put takes a (T)-view and that complement and reconstructs an (S)-record.

Resource ownership

Engine-backed wrappers implement Disposable. This includes Protocol, BuiltSchema, CompiledMigration, the three lens-handle classes, IoRegistry, TheoryHandle, Repository, and DataSetHandle. Dispose each owned wrapper after its last use, preferably with an explicit resource-management scope:

using schema = protocol.schema().vertex('root', 'object').build();

Disposal is idempotent. Accessing a disposed handle raises WasmError. A FinalizationRegistry frees a leaked handle as a fallback, but collection time is nondeterministic. Disposing Panproto releases its cached Protocol objects. It does not own every schema, migration, lens, registry, repository, or data-set wrapper created from it.

Instance, result objects, and SpanResponse are plain JavaScript data and do not implement Disposable.

Span search

span(
  from: BuiltSchema,
  to: BuiltSchema,
  hints?: Readonly<Record<string, string>>,
): SpanResponse

The optional hints are fixed source-to-target vertex mappings. SpanResponse contains apex_vertices, apex_edges, vertex_map, quality, quality_bounds, apex_coverage, proven_optimal, is_total, and apex_digest. It contains no engine handle.

The WASM surface exposes span search but not the Rust total-morphism functions find_morphisms and find_best_morphism. Use span.is_total when a caller needs to know whether the returned apex covers the complete source.

Boundary limits

The SDK passes structured payloads through the WASM layer and stores live engine resources behind integer handles. The package does not expose the Rust panproto-parse full-AST registry, multi-file panproto-project builder, or panproto-git bridge. Schema-document and schema-source parsers available through Panproto.parseSchemaDocument and Panproto.parseSchemaSource are separate from that full-AST surface.

The current executeQuery wrapper does not match the current WASM entry point. TypeScript sends only a query and instance, while Rust requires query, instance, and schema payloads. The TypeScript wire fields also use projection, groupBy, and nodeId, while the Rust query types use project, group_by, and node_id. Treat executeQuery as unavailable until the binding and WASM signatures are aligned.

See also

• Install the TypeScript SDK
• Define a schema from TypeScript
• WASM boundary
• Find a span between two schemas

Python SDK reference

The Python package is panproto. It requires Python 3.13 or later and contains a native PyO3 extension.

python -m pip install panproto

Module surface

Public names are re-exported from panproto. There is no umbrella engine class. The package source lists those names in panproto.__all__, and the shipped _native.pyi file is the signature authority for the extension.

Builder contracts

Python builders mutate in place. Their mutation methods return None, except where _native.pyi declares a fluent return type.

class SchemaBuilder:
    def vertex(self, id: str, kind: str, nsid: str | None = ..., /) -> None: ...
    def edge(
        self,
        src: str,
        tgt: str,
        kind: str,
        name: str | None = ...,
    ) -> None: ...
    def constraint(self, vertex_id: str, sort: str, value: str) -> None: ...
    def build(self) -> Schema: ...

TheoryBuilder.sort, TheoryBuilder.op, and TheoryBuilder.eq return the builder and may be chained. Check _native.pyi before assuming that a builder follows either convention.

Migration direction

For a CompiledMigration whose schema mapping is (S\to T), lift(instance) accepts an (S)-instance and returns the surviving fragment as a (T)-instance. The method calls Rust’s restrict-based lift_wtype. It is neither the left Kan extension (\Sigma_F) nor precomposition (\Delta_F). get uses the same source-to-target operation and returns a complement with the view. put accepts the target view and complement and reconstructs a source instance.

Morphism search

find_span(
    src: Schema,
    tgt: Schema,
    protocol: Protocol,
    anchors: dict[str, str] | None = None,
    monic: bool = False,
    epic: bool = False,
    iso: bool = False,
) -> SchemaSpan

find_morphisms(
    src: Schema,
    tgt: Schema,
    anchors: dict[str, str] | None = None,
    monic: bool = False,
    epic: bool = False,
    iso: bool = False,
    max_results: int = 0,
) -> list[FoundMorphism]

find_span returns an empty apex when the schemas share no vertices. It requires a protocol because the induced apex is validated before it is returned. epic=True raises MigrationError for span search. Surjectivity is defined for the total-morphism functions.

find_morphisms returns total morphisms attaining the optimum. An empty list means that no total morphism exists, whereas a search failure raises MigrationError. The Python list does not carry the Rust MorphismList.truncated field, so this binding cannot report whether the engine stopped enumerating tied optima at its cap.

Grammar packs

AstParserRegistry() constructs a native registry and adds grammars advertised through installed panproto.grammars entry points. Discovery occurs when the factory is called. Importing a companion package is not required.

panproto._native.AstParserRegistry bypasses companion discovery and constructs the registry supplied by the core extension alone.

Ownership, errors, and typing

PyO3 objects follow Python reference ownership. The public stub exposes no dispose, release, or close method for schema, migration, lens, theory, repository, parser, or project objects.

PanprotoError is the common exception base. Domain subclasses include SchemaValidationError, MigrationError, LensError, CheckError, ExistenceCheckError, ExprError, GatError, IoError, VcsError, ParseError, ProjectError, and GitBridgeError.

The wheel includes py.typed and _native.pyi. Repository tests compare the stub’s public declarations with the loaded extension and check callable signatures, so generated documentation should follow the stub rather than infer signatures from Rust names.

See also

• Install the Python SDK
• Define a schema from Python
• Find a span between two schemas
• Python binding source

Haskell SDK reference

The Haskell binding is the panproto package under bindings/haskell/. Its Cabal manifest uses GHC2024 and declares GHC 9.12.2 as the tested compiler.

The package links libpanproto_c when the rust flag is active. The repository bootstrap scripts and required library paths are covered in Install the Haskell SDK.

Imports and backends

import Panproto

Panproto re-exports the structural value modules, capability classes, domain modules, and effect adapter. With the default rust flag, it also brings the Rust-backed capability instances into scope.

Operations dispatch through associated representation families such as ProtocolRep back, SchemaRep back, InstanceRep back, and LensRep back. The backend tag is either Rust or Native.

Native has no SchemaValidate, migration, lens, instance, or search instance in the current source. The structural Schema, Migration, ProtolensChain, Theory, and Instance data types remain available as ordinary Haskell values, but a pure value type does not imply a runnable Native capability instance.

The Haskell Instance exchange type mirrors the W-type instance used by the C boundary. It is not the Rust panproto_inst::Instance enum over W-type, relational, and graph representations.

For a compiled schema mapping (S\to T), MigrationBackend.liftRecord accepts an (S)-instance and returns the surviving fragment as a (T)-instance. It wraps pp_mig_lift_record, which calls the restrict-based Rust function mig::lift_wtype. This operation is neither the left Kan extension (\Sigma_F) nor precomposition (\Delta_F). The Haskell capability class does not expose the separate Rust (\Sigma_F) and (\Pi_F) entry points.

Capability lookup

Morphism search

HomBackend declares the following methods:

findMorphisms
    :: SchemaRep back
    -> SchemaRep back
    -> SearchOptions
    -> IO [FoundMorphism]

findBestMorphism
    :: SchemaRep back
    -> SchemaRep back
    -> SearchOptions
    -> IO (Maybe FoundMorphism)

findSpan
    :: SchemaRep back
    -> SchemaRep back
    -> ProtocolRep back
    -> SearchOptions
    -> DomainConstraints
    -> IO FoundSpan

defaultFindOpts sets monic, epic, and iso to False, maxResults to zero, and hardPins to the empty map. defaultDomainConstraints applies no domain restrictions or weight override.

findMorphisms returns total morphisms attaining the optimum, and findBestMorphism returns Nothing when no total morphism exists. The Haskell list omits the engine’s truncation field for tied optima. findSpan may return an empty apex. It rejects epic = True because a span’s right leg is partial.

Handle ownership

Rust-backed representations that own slab entries have matching release* methods on their capability classes. Examples include releaseProtocol, releaseSchema, releaseChain, releaseLens, releaseTheory, releaseModel, releaseRegistry, releaseRepo, and releaseDataSet. Release is idempotent at the C slab boundary.

Use a bracket helper where the binding provides one. Public helpers include withRustProtocol, withRustSchema, withCompiled, withRustTheory, withRepo, and withDataSet. Some exchange representations, including the Rust InstanceRep, carry no slab entry and have a no-op release method. The class method remains the ownership authority.

Errors

FFI failures are exceptions in IO. SomePanprotoError is the root wrapper, PanprotoError is the generic fallback, and the domain exception types include MigrationError, LensError, SchemaValidationError, CheckError, ExistenceCheckError, ExprError, GatError, IoError, VcsError, ParseError, ProjectError, and GitBridgeError. Each error carries a PpStatus and may carry a decoded ErrorEnvelope.

Cabal flags

The parse, project, and git flags must match the features compiled into the linked C library. Enabling a Haskell module does not add missing symbols to libpanproto_c.

See also

• Install the Haskell SDK
• Define a schema from Haskell
• Find a span between two schemas
• Haskell package manifest

Swift SDK reference

The Swift package lives in bindings/swift/. It uses Swift 6 language mode and supports macOS 14 and iOS 17. The engine-backed products call panproto-c. PanprotoStructural has no FFI dependency.

See Install the Swift SDK for package and library setup.

Products

The three gated products remain present when their traits are disabled, but their gated declarations are not compiled. Each trait also requires a libpanproto_c built with the corresponding Rust feature.

Values and handles

PanprotoStructural contains Swift values such as Schema, Instance, Migration, Complement, SchemaSpan, and FoundMorphism. These values use ordinary Swift ownership and do not require release calls.

Engine resources are subclasses of PanprotoHandle:

SchemaBuilder and MigrationBuilder are Swift structs. Their mutating methods update the builder value. MigrationBuilder.build() returns a Migration, which can then be compiled against two schema handles.

Engine isolation

Every operation that consumes a handle is isolated to the PanprotoEngine global actor. The C ABI protects its resource slab and last-error slot with process-global mutexes, so a handle is valid from any thread. The error slot holds only one pending envelope, however, and an interleaved failure can overwrite it before Swift drains it. The actor’s pinned serial executor keeps each call and error drain together and makes the engine’s serial contention visible to Swift concurrency. Calls from outside the actor consequently use await:

let protocolHandle = try await ProtocolHandle.builtin("atproto")
let schema = try await SchemaHandle.parseAtprotoLexicon(lexicon)

PanprotoEngine.run can group several synchronous engine calls in one actor-isolated closure:

let result = try await PanprotoEngine.run {
    try schema.violations(against: protocolHandle)
}

Engine calls perform synchronous work once scheduled. Task cancellation does not interrupt a call already executing in the C ABI.

Migration and lens operations

CompiledMigrationHandle supplies both migration and asymmetric-lens operations:

func lift(_ instance: Instance) throws(PanprotoError) -> Instance
func get(_ source: Instance) throws(PanprotoError) -> LensProjection
func put(view: Instance, complement: Complement) throws(PanprotoError) -> Instance

LensProjection carries the view and the complement captured during get. Pass that complement to put. Complements are tied to the source schema and may conflict when composed.

For a compiled schema mapping (S\to T), lift accepts an (S)-instance and returns the surviving fragment as a (T)-instance. It wraps the restrict-based Rust mig::lift_wtype. It is neither the left Kan extension (\Sigma_F) nor precomposition (\Delta_F). get has the same source-to-target direction and captures the complement. put accepts the target view and complement and reconstructs a source instance.

Law-checking methods return LawCheckResult rather than throwing when a law is false. They can still throw when the operation itself cannot be evaluated. checkLaws checks GetPut and a deterministic two-view PutGet smoke test at the supplied source instance. It is not a proof for all instances or edits.

Morphism and span search

Search methods are defined on SchemaHandle:

func findMorphisms(
    to target: SchemaHandle,
    options: MorphismSearchOptions = MorphismSearchOptions()
) throws(PanprotoError) -> [FoundMorphism]

func findBestMorphism(
    to target: SchemaHandle,
    options: MorphismSearchOptions = MorphismSearchOptions()
) throws(PanprotoError) -> FoundMorphism?

func findSpan(
    to target: SchemaHandle,
    in protocolHandle: ProtocolHandle,
    options: MorphismSearchOptions = MorphismSearchOptions(),
    constraints: MorphismDomainConstraints = MorphismDomainConstraints()
) throws(PanprotoError) -> SchemaSpan

findMorphisms returns total morphisms that attain the optimum. An empty array means that no total morphism exists. The Swift array does not expose the Rust MorphismList.truncated field, so callers cannot distinguish complete enumeration of tied optima from an answer stopped by the engine cap.

findSpan admits a partial match and may return an empty apex. The protocol handle is required because the induced apex is validated as a schema. The span result is a Swift value. Call SchemaSpan.overlap() when the identification pairs for a pushout are needed.

Ownership

Each PanprotoHandle owns one engine slab entry. release() returns that entry early and is idempotent. If a live handle reaches deinitialization, its release is queued onto the engine thread. Do not call engine operations on a handle after releasing it. The engine reports the slab index as invalid or may have reused it for another resource.

Errors

Public engine operations use typed throws with PanprotoError. Its cases identify the operation domain, including parse, migration, lens, schemaValidation, check, existenceCheck, expr, gat, io, vcs, gitBridge, and project. Each case carries a Detail containing the raw status, operation name, optional error envelope, and any recognized structured fault.

Package traits

The linked C library and selected package traits must agree. Enabling a trait while linking a library without the corresponding symbols fails at link time.

Boundary limits

PanprotoStructural can decode, encode, compare, and transform its value types without starting the engine. Validation, migration compilation, lens execution, search, law checks, and other semantic operations require an engine-backed product. The Swift API exposes only operations exported by panproto-c. Rust APIs with no C entry point are not available through this binding.

See also

• Install the Swift SDK
• Define a schema from Swift
• Find a span between two schemas
• Architecture

Protocol catalog

A protocol names a schema language together with its schema and instance theories, structural rules, parser, and emitter. The semantic protocols in panproto-protocols compose reusable generalized algebraic theories (GATs) (Cartmell 1986). Source-code languages use the separate tree-sitter registry described below.

Semantic protocols

The generic dispatch functions accept 54 semantic protocols. Names in this table are the canonical hyphenated strings accepted by parse_schema_document or parse_schema_source. Underscore spellings are normalized before dispatch.

The raw_file module is the text-or-binary fallback used during project assembly. It is a protocol implementation, but is not listed by either generic schema-dispatch function.

Parser dispatch

The exported document_parser_protocols, source_parser_protocols, bundle_parser_protocols, and bundle_project_protocols arrays are the lookup sources for these sets.

Protocol availability also depends on the surface. The current schema CLI resolves protocol theories only for atproto. The C and WebAssembly theory-registry helpers recognize atproto, json-schema, graphql, sql, and protobuf, while their protocol lookup tables expose the 54 names above.

Registration behavior

Each semantic protocol module exposes protocol() and register_theories(). Most registrars call shared theory-group constructors. Those constructors panic if a named pushout fails, rewrite analysis cannot complete, two rewrite paths fail to rejoin (a non-joining critical pair), or the lexicographic-path-order termination check fails. Registration thus treats these outcomes as internal theory-definition defects, not recoverable input errors.

The ATProto registrar is different. It inserts its five component theories first, then inserts each composed schema or instance theory only when the corresponding pushout_by_name call succeeds. Its register_theories() function has no Result, so a failed composition is omitted rather than returned to the caller. What panproto verifies gives the boundary between these construction-time gates and checks on user schemas.

The source tree is the catalog authority:

Source-code grammars

panproto-grammars defines 261 individual lang-* features under group-all. A selected feature contributes a tree-sitter Language and its vendored AST metadata to ParserRegistry. The default group-core is a subset. Callers do not receive all grammars unless their selected feature set includes them.

emit_verification_status reports test coverage for the registered parser, not a proof about all inputs:

The verified set currently contains 255 names. Source-code emission identifies the seven backend cases and the six grammars outside the set.

Defining a protocol

Build a custom protocol covers theory declaration, registration, parsing, and emission. Adding a Rust module to panproto-protocols does not automatically extend the CLI, C, or WebAssembly lookup matches. Each exposed surface needs its own dispatch arm.

See also

• Schemas as theories
• Composing protocols by colimit
• Theory DSL: denotational semantics

Expression-language reference

panproto-expr evaluates a call-by-value expression AST with no I/O operations. Evaluation is bounded and fallible. The default limits are 100,000 reduction steps, recursion depth 256, and 10,000 elements in list literals and selected list-producing paths. Reaching a limit returns an ExprError. It does not establish that every expression terminates before the limit.

Builtin names are first-class values. A lexical environment binding shadows a builtin of the same name, and an unapplied builtin may be partially applied until it receives its declared arity. eval_with_resolver routes context-dependent builtins through the supplied resolver wherever they occur, including inside lambdas, bindings, and comprehensions.

The language is used for field transforms and instance queries. Expression language: denotational semantics gives the model behind the evaluator.

Surface grammar

panproto-expr-parser accepts a Haskell-style syntax and lowers it to Expr.

Open-ended ranges such as [a..] are parse errors. The parser lowers map f xs, filter p xs, and flat_map f xs to an AST with the list first and function last. It lowers fold f z xs to [xs, z, f]. This AST argument order is the serialized compatibility contract.

Operators

From lower to higher precedence, the infix operators are pipe &, ||, &&, comparisons (==, /=, <, <=, >, >=), string concatenation ++, addition and subtraction, then multiplication, division, and remainder (*, /, %, div, mod). Unary - and not bind more tightly. And and Or evaluate both AST arguments before applying the builtin. They do not short-circuit.

Values and type tags

Runtime Literal values include booleans, 64-bit integers and floats, UTF-8 strings, bytes, null, records, lists, and closures. Lists can contain values of different kinds. The lightweight ExprType inference API has fewer tags:

Type inference is best effort. Application, field access, and indexing generally infer as Any, while evaluation still performs runtime type and arity checks.

Builtins

BuiltinOp currently has 60 variants.

Evaluation errors

ExprError is non-exhaustive.

Source

The AST and builtin enum live in expr.rs, builtin implementations in builtin.rs, evaluation and defaults in eval.rs, and the surface grammar in parser.rs.

See also

• Apply field transforms
• Query instances

Resource limits

Reading a schema costs time and memory proportional to what the input asks for, and a public entry point reads input it did not author. Every such surface therefore parses within a budget: an allowance that is checked before work begins and drawn down as it proceeds.

What is bounded

The depth bound matches the walk and extraction depths that already existed, so it governs nothing it did not govern before.

Two properties that make this a policy

Several subsystems already had sound local bounds: parser walk depth, CST extraction depth, expression evaluation steps, morphism search budget, model-check assignment counts. What they were not was a policy. What an input was allowed to cost depended on which door it came through, so the same document could be refused through one surface and accepted through another.

A budget is shared, not per-call. A nested operation draws from the same allowance as the operation containing it. Cloning a Budget shares its counters rather than copying them, so a caller is not charged once for a walk and again for each subwalk, and an oversized input cannot slip past a bound by being processed in pieces. A budget that reset per subsystem would bound each step and nothing overall, which is what several unrelated local limits already achieved.

A failure names the resource and the bound. LimitExceeded carries which allowance ran out and what it was set to. “Too deep” without a number tells a caller nothing about what to pass instead, and with seven separate allowances it does not even say which setting to change.

Defaults, configuration, and opting out

parse_schema_document, parse_schema_source and parse_schema_bundle apply ResourceLimits::defaults(). Every binding calls those, so the CLI, Python, C and WASM all inherit the same policy; none of them selects its own, and none can inherit an unbounded one by accident.

A Rust caller that needs different bounds uses the _within variants:

#![allow(unused)]
fn main() {
use panproto_core::expr::limits::{Budget, ResourceLimits};
use panproto_core::protocols::parse_schema_bundle_within;

let mut limits = ResourceLimits::defaults();
limits.bundle_entries = 32_768;
let budget = Budget::new(limits);

let docs = vec![serde_json::json!({
    "lexicon": 1,
    "id": "com.example.record",
    "defs": { "main": { "type": "object", "properties": { "v": { "type": "string" } } } },
})];
let schema = parse_schema_bundle_within("atproto", &docs, &budget)?;
assert!(schema.vertex_count() > 0);
Ok::<(), Box<dyn std::error::Error>>(())
}

Passing the same budget to several calls has them share one allowance, which is how a caller bounds a whole pipeline rather than each stage of it.

ResourceLimits::unbounded() removes every bound, and a field set to 0 removes that one. This is a legitimate choice for a Rust caller processing input it produced itself. It is deliberately something to ask for: no FFI or command-line entry point selects it, because unbounded behaviour should never be inherited at a boundary that reads input from elsewhere.

See also

• What panproto verifies for the bounded model check, whose assignment budget is configured separately per invocation.

Lens combinator reference

panproto implements asymmetric lenses (Foster et al. 2007) with an explicit complement in the complementary-view tradition (Bancilhon and Spyratos 1981). For a fixed Lens, the data-level operations have the shapes

$$\mathrm{get}:S\to V\times C\mathrm{put}:V\times C\to S.$$

Both Rust functions return Result. get accepts an instance of the source schema and runs the source-to-target restrict pipeline, returning the target-schema view and its Complement. put accepts that target-schema view and complement and reconstructs a source or returns LensError.

Law-checking API

These functions are on-demand checks over their supplied values. Property tests exercise generated lenses, instances, and views, but a passing test run is not a proof for every constructor input. What panproto verifies records the corresponding limits.

Optic kinds

OpticKind is a structural classification derived from TheoryTransform. Classification itself does not run an optic-law checker.

OpticKind::compose uses Iso as the identity and Traversal as an absorbing element. Lens composed with Prism, or either composed with Affine, yields Affine. This table describes the enum’s implementation. It does not certify the full laws of profunctor optics (Pickering et al. 2017).

Constructor modules

The full parameter types are the public Rust signatures in those module indexes. Several elementary constructors accept impl Into<Name>. Checked coercion constructors additionally return Result when their finite honesty samples fail. The elementary pullback constructor stores a supplied TheoryMorphism in TheoryTransform::Pullback. It does not construct a categorical pullback object or return a certificate of a pullback universal property.

Complement composition

ComplementCompose::compose(&left, &right) returns Result<Complement, LensError>. It rejects distinct nonzero source fingerprints with ComplementFingerprintMismatch and conflicting values under a shared key with ComplementConflict. ComplementCompose::is_compatible runs the same predicate without returning the merged value. The trait must be in scope because Complement is defined in panproto-inst.

Protolens composition and instantiation

A Protolens stores source and target theory endofunctors, a schema precondition, and a complement constructor. The intended natural-transformation structure uses the standard categorical definition (Eilenberg and Mac Lane 1945). Constructing a value does not verify naturality over every schema.

protolens_composable(eta, theta) accepts either structurally equal intermediate endofunctors or an identity transform on theta.source. The identity-source case retains theta’s source precondition in the composite. vertical_compose rejects other pairs with CompositionMismatch. horizontal_compose currently returns Ok without an additional compatibility check.

Call check_applicability_with before fused instantiation when preconditions must be enforced. Fused and sequential instantiation are compared in property tests. Neither return value is a proof of the lens laws for all instances.

See also

• Use lenses
• Use protolenses
• Use dependent optics
• Lens DSL: denotational semantics

Configuration reference

The project manifest is panproto.toml in the project root. load_config returns Ok(None) when the file is absent and rejects malformed TOML as ProjectError::InvalidManifest.

Manifest shape

[workspace]
name = "my-project"
exclude = ["target", "build", "**/*.log"]

[[package]]
name = "user-api"
path = "schemas/user"
protocol = "json-schema"

[[package]]
name = "user-events"
path = "schemas/events"

[workspace]

[[package]]

The top-level package array may be omitted and then defaults to empty.

If an overridden parser rejects a file, project assembly falls back to raw_file. It does not retry ordinary language detection. Package paths supply protocol-prefix overrides, but do not restrict the directory walk to the declared packages.

Generated defaults

schema init [PATH] always initializes .panproto/. When package scanning finds at least one recognized package, it also writes panproto.toml with detected package entries and these exclusions:

exclude = ["target", "node_modules", "__pycache__", "build", "dist", ".git"]

When scanning finds no package markers, schema init does not create a manifest. The package scanner recognizes Cargo, npm, Go, Python, Gradle, Elixir, and CMake project markers. Programmatic callers can use generate_config and serialize_config.

Source

The manifest structs and defaults live in crates/panproto-project/src/config.rs. Project assembly applies them in crates/panproto-project/src/lib.rs.

See also

• Define a schema from the CLI
• Schema version control: init and commit

Crate map

The workspace contains 36 panproto-* crates. This page groups them by dependency role. The repository Cargo.toml is authoritative for membership, and each crate’s manifest is authoritative for features.

Theory, schemas, and migration

panproto-mig::solve implements exact bucket elimination (Dechter 1999), budgeted hybrid search with EDAC* cost propagation [Allouche et al. (2015); Larrosa & Schiex (2004); de et al. (2005)], an all-different constraint for injective mappings (McCreesh and Prosser 2015), and McSplit partitioning for isomorphism requests (McCreesh et al. 2017). Searching for a morphism defines these paths. What panproto verifies states what their certificates establish.

Lenses, expressions, and DSLs

Parsing, I/O, and projects

Version control and transport

Facades and bindings

Feature-gated dependency edges

xtask is a workspace member but not a panproto-* library. It contains repository maintenance commands, including CLI-document generation.

See also

• Architecture
• Rust SDK
• Protocol catalog

Explanation

These chapters explain the representations and checks that underlie panproto. They assume that you can read a schema and a structural diff, but they do not assume category theory. Procedures belong in the how-to guides, while interface details belong in the reference.

Schemas, migrations, and lenses

Begin with What panproto solves, and consult The vocabulary in plain terms when an unfamiliar term appears. Schemas as theories first describes the common representation used for different protocols. Migrations as morphisms then explains a migration and the operations that move data along it. Search may return a partial correspondence as a span. Together, these chapters supply the background needed by the tutorials and most how-to guides.

When a conversion discards information or must support updates in both directions, continue from the glossary definition of a lens to Lenses and round-trip laws. What panproto verifies distinguishes runtime validation and test evidence from properties that the implementation assumes.

Search, composition, and version control

Searching for a morphism describes how panproto searches for a partial or total schema correspondence. Alignment evidence explains how names, types, and other evidence affect that search.

Composing protocols by colimit concerns the colimit construction used to describe protocol structure. Schema version control semantics concerns structural changes to concrete schemas and their histories. The two chapters use related categorical constructions at different levels of the system.

Layout enrichment and Source-code emission address parsing, canonical emission, and preservation of source layout. Architecture identifies the crates that implement these operations and the data that crosses their boundaries.

Denotational semantics

The denotational semantics chapters specify the expression language, both DSLs, protolens composition, merge, and the theory REPL. Begin with Shared notation; the remaining chapters assume familiarity with typed abstract syntax, inference rules, and elementary category theory.

Related work locates these constructions in the literature. It is best read after the chapters on schemas, migrations, and lenses.

Chapter map

What panproto solves

Changing a schema usually creates a corresponding data problem. A renamed field may require only a direct correspondence, while a split record or retired variant may require a default, a value transform, or saved information. When those decisions live only in migration scripts, it can be difficult to compare them with the schemas that they connect.

panproto represents a schema change as structured data. It can compare two schemas, classify their compatibility, compile a migration between them, and apply that migration to schema-typed data. The same representations support histories of schema objects and structural three-way merge. The protocol catalog records the formats for which parsers or other protocol support are registered.

These operations depend on the protocol-theory model. A protocol identifies the theories used to describe its schema and instance structure. A parsed schema supplies the concrete types, fields, constraints, and related metadata governed by those theories. Schemas as theories develops this distinction.

Prerequisites: familiarity with fields, records, and schema versions. No category theory is assumed.

Compare and classify schema changes

A structural diff records additions, removals, renames, and modifications. The compatibility classifier then assigns the report one of three classifications: fully compatible, backward compatible, or breaking. A CompatReport retains the classification together with its breaking and non-breaking findings, which allows a CI job to reject changes under a chosen policy.

Compile and apply migrations

A migration records correspondences from a source schema to a target schema together with any required value transforms. Compilation checks that the correspondence preserves the relevant schema structure before producing the tables used to transform data. If a forward transformation discards source information, a lens may retain that information in a complement for a later backward update. Migrations as morphisms describes compilation and data movement; Lenses and round-trip laws describes complements and the available law checks.

Record and merge schema histories

The version-control layer stores schemas, migrations, data sets, and related metadata as content-addressed objects. Its commands expose commits, branches, tags, diffs, blame, and structural merge over those objects. When two branches make incompatible structural changes, merge returns typed conflict descriptions for explicit resolution. Schema version control semantics gives the details and limits of this construction.

Scope

panproto does not supply application behavior that a schema leaves unspecified, deploy a migration, or replace a database. It operates on schema documents and schema-typed data. Its outputs include structural reports, compiled migrations, converted data, and repository objects.

See also

• Schemas as theories for the common representation used across schema languages.
• Migrations as morphisms for the structure and execution of migrations.
• Schema version control semantics for structural history and merge.

The vocabulary in plain terms

panproto uses mathematical terms to distinguish operations that ordinary migration vocabulary often groups together. This page gives working translations and points to the chapters that define the terms more precisely.

Prerequisites: familiarity with schemas and data migration. This page also supports the intermediate route in the explanation reading guide.

Terms

Tutorials chiefly use schema, migration, lens, and complement. How-to guides also refer to protocols and protolenses. Remaining terms appear in the explanation chapters where their distinctions affect an operation. The glossary provides shorter formal definitions, while Schemas as theories and Migrations as morphisms develop the central representations.

See also

• Glossary for formal definitions.
• What panproto solves for the problem statement.
• Schemas as theories and Migrations as morphisms for the underlying representations.

Schemas as theories

A JSON Schema object, a Protobuf message, and an ATProto Lexicon record use different surface syntax. Once parsed, each identifies types, directed fields between types, and constraints on those elements. panproto stores this information in a common Schema representation that retains graph structure, protocol-specific constraints and metadata, and derived adjacency indices. The linked Schema API gives the complete field inventory. panproto_schema::validate reports structural findings. Callers decide whether those findings reject an operation.

This concrete representation permits a structural comparison between documents from different schema languages. It does not erase their differences. Each schema retains its protocol identifier, and the protocol determines which structures are meaningful and which validation rules apply.

The vocabulary in plain terms introduces the graph terminology used below. The formal account distinguishes a specification from a structure that satisfies it.

Protocol theories and schema models

A registered Protocol names a schema theory and an instance theory. The registry associates those names with generalized algebraic theory (GAT) presentations (Cartmell 1986). A presentation may declare sorts, operations over those sorts, and equations or directed equations. The graph theory ThGraph, for instance, declares the sorts Vertex and Edge and the operations src and tgt from edges to vertices.

The protocols crate defines five foundational theories. ThGraph describes directed graphs, ThConstraint attaches constraints to vertices, and ThMulti adds edge labels. ThMeta describes discriminator and extra-field metadata. These four contain no equations. ThWType describes nodes, arcs, and values and contains two endpoint-coherence equations: an arc’s source and target nodes must be anchored at the endpoints of the schema edge named by that arc. Higher-level theories compose these foundations for particular groups of protocols. Composing protocols by colimit describes that composition.

A parsed schema has the intended mathematical reading of a model of its protocol’s schema theory: concrete vertices and edges interpret the corresponding sorts, while their endpoints interpret src and tgt. The Rust Schema type is a dedicated concrete representation, however, and does not implement panproto_gat::Model. panproto_schema::validate checks the protocol’s structural rules rather than evaluating every theory equation. Equation satisfaction uses a separately constructed finite Model and the bounded checker in panproto-gat.

The distinction also separates two kinds of map. A schema morphism maps the vertices and edges of one concrete schema to those of another while preserving endpoints and other required structure. A theory morphism maps the sorts and operations used to specify a family of structures. Migrations use the former. Cross-protocol theory composition uses the latter.

Representational limits

The theory-model account describes structure that a protocol registration exposes. It does not describe the running time of operations over a large schema or application behavior absent from the schema. Whitespace, comments, and other source-layout details also lie outside the ordinary schema model. The layout-enrichment and format-preserving layers can retain such details when the parser supplies them.

Validation reports consistency findings for the registered structural rules. Application invariants remain unchecked when neither the protocol theory nor the concrete schema represents them.

Related work

The schemas-as-theories account also draws on Spivak’s functorial data model (Spivak 2012), the algebraic-databases program [Schultz & Wisnesky (2017); Schultz et al. (2017)], attributed C-sets (Patterson et al. 2022), and Lu’s work on multi-model unification (Lu 2025). panproto assigns a GAT presentation to each protocol and can combine presentations by colimit. The attributed C-set and algebraic-database approaches instead fix a meta-theory and parameterize schemas within it. Related work develops the comparison.

See also

• Composing protocols by colimit for composition of foundational theories.
• Migrations as morphisms for maps between concrete schemas.
• Theory DSL: denotational semantics for the formal model of a GAT presentation.
• The bibliography entries Cartmell (1986) and Spivak & Wisnesky (2015) for the GAT and functorial-data-migration backgrounds.

Migrations as morphisms

Suppose a source schema contains a field named age and a target schema contains the corresponding field under the name years. A migration records the map from the source field to the target field. If the value also changes representation, the migration may associate that correspondence with an expression that computes the target value.

This representation separates a structural map from its execution. The map can be validated, stored, and composed before it is applied to data. A compiled migration contains the tables and value resolvers needed by the instance layer.

Maps between concrete schemas

Let $S$ and $T$ be concrete schemas. In the functorial account of data migration, a schema morphism $f:S\to T$ maps source structure to target structure and induces operations between their instance categories [Spivak (2012); Spivak & Wisnesky (2015)]. In panproto’s concrete representation, $f$ maps source vertices and edges to target vertices and edges. It must preserve edge endpoints and land in the target schema. The free function panproto_mig::compile checks this mapped fragment and builds the tables used during instance migration. It does not run the separate migration-existence check.

Data can then move along the compiled map. The names lift and restrict are overloaded in the current APIs, so the function and its input direction matter.

• lift_wtype and lift_functor take an $S$-instance and return a $T$-instance containing the fragment that survives the compiled migration. When several source vertices map to one target vertex, lift_functor concatenates their row sets. These functions are forward projections. They are not the categorical restriction ${\Delta }_f$.
• lift_wtype_sigma and lift_functor_sigma also run from $S$ to $T$. The W-type operation requires every source anchor to have an image. The functor operation applies functor_extend and may then run the term-level chase supplied by its caller.
• lift_wtype_pi is implemented only for vertex-injective migrations and relabels rather than constructing a product. lift_functor_pi computes Cartesian products over fibers and enforces its product-size limit.

The schema lift command always parses its input under --src-schema and emits under --tgt-schema. This direction is unchanged by --direction restrict, sigma, or pi. The default restrict label selects the forward surviving-fragment projection described above. It must not be read as ${\Delta }_f$.

The categorical vocabulary organizes a more specific fragment. Given $f:S\to T$, restriction is written

$${\Delta }_f:T\text{-Inst}\to S\text{-Inst},$$

and its left adjoint is written

$${\Sigma }_f:S\text{-Inst}\to T\text{-Inst}.$$

The explicit constructions live in panproto_inst::adjunction. For set-valued FInstances, f_sigma runs from $S$ to $T$ and f_delta runs from $T$ to $S$. The implementation also supplies the unit, counit, and hom-set transposes for total vertex maps, including maps that merge vertices. For WInstance, w_sigma runs from $S$ to $T$, while w_delta runs from $T$ to $S$ and requires vertex- and edge-injective maps whose target anchors lie in the image. Property tests exercise the triangle identities and hom-set transposes in these fragments. They do not prove an adjunction for arbitrary partial migrations.

Migration composition also acts on values. compose combines carried coercion expressions in execution order and uses partial-map semantics for structural elements omitted by the second migration. invert requires bijective coverage of target vertices, edges, and hyperedges, and it refuses a carried coercion without an inverse expression. It reverses the remaining coercions and swaps the recorded schema endpoints. Hand-built expr_resolvers are not inverted and are dropped from the inverse.

Value-level transforms are expressions in the expression language. They determine how a target value is computed when a structural correspondence alone is insufficient.

Partial correspondence as a span

A source schema and a target schema need not admit a total morphism. Search thus returns a span

$$S\stackrel{\ell }{\leftarrow }A\stackrel{r}{\to }T,$$

where $A$ is the apex and the two arrows are its legs (Johnson and Rosebrugh 2014). Johnson and Rosebrugh use peak for the same object.

In panproto, $A$ is the sub-schema of $S$ induced by the source vertices that the search matched. The left leg is the resulting inclusion, and the right leg records the match into $T$. panproto_schema::induce restricts the schema’s element tables and protocol metadata to this sub-schema, rebuilds its derived indices, and validates the result. Copying only the vertex and edge maps would leave other tables referring to removed elements.

The span is total when the inclusion covers all of $S$. SchemaSpan::is_total tests this condition, after which the span can yield a total schema morphism. The empty apex is a feasible match when the schemas share no compatible structure. Search may still report malformed inputs or construction errors, but it does not fail solely because no nonempty match exists.

Classical span equivalence uses an isomorphism between apices that commutes with both legs (Johnson and Rosebrugh 2014). Because panproto’s left leg is an inclusion, the apex is determined by its selected source vertices. A returned span can consequently be represented by that selected sub-schema and its right-leg map, without a separate graph-isomorphism quotient.

The omitted portion of the source resembles a complement in the sense of Bancilhon & Spyratos (1981): it is information outside the selected view that may be needed to recover the source. This analogy motivates a preference for larger apices at equal search quality. It does not transfer the constant-complement results of that work to panproto’s schema spans.

Pushout and the two apices

A span supplies the input to a pushout:

$$\begin{array}{ccc}A& \stackrel{r}{\to }& T\\ \ell \downarrow & & \downarrow j\\ S& \underset{i}{\to }& S{\bigsqcup }_{A}T.\end{array}$$

The schema apex $A$ records shared schema structure. The search returns this schema span. It does not construct pairs of instances that agree on $A$ or establish a model-level pullback theorem; those are separate claims that the current search API does not check.

The implemented schema pushout requires an injective right leg on vertices. A default search result may map two apex vertices to one target vertex, which is a contracting right leg. SchemaSpan::pushout rejects that case. Callers that require a merge can request a monic or isomorphic search result. The underlying schema_pushout closes the supplied vertex and edge identifications to an equivalence relation and returns two SchemaMorphism values. This constructor does not run a separate universal-property checker.

The data-migration adjunction does not by itself construct a symmetric lens for this pushout. Johnson et al. (2012) relate c-lenses to Grothendieck opfibrations and use that structure to formulate universal view updates. panproto checks its scoped adjunction and its lens laws as separate implementation properties; it does not formalize that equivalence.

The length-1 fragment

In the broader functorial account, a schema translation may send a generating source arrow to a path in the target category. SchemaMorphism has a narrower representation: its edge_map maps each source edge to one target edge. Migration uses the same shape. These maps form the length-1 fragment of that account.

A one-to-many value correspondence thus does not appear as a schema morphism. FieldTransform::ComputeField can instead compute a target key with an expression. It may also carry an inverse expression, and its declared CoercionClass records the intended recovery behavior. Because callers supply that class, the presence or absence of an inverse does not by itself determine the classification.

Search also considers only a projection of the full Schema representation when scoring candidates. Other fields participate in feasibility checks or are restricted by induce, but they do not all affect the objective. The weights express a preference over alignments and have not been calibrated against a labeled corpus of correct matches. Searching for a morphism gives the exact objective and constraints.

Compatibility classification

CompatReport records a classification together with separate breaking and non_breaking findings. The classifier uses the following conditions:

These labels classify structural change. They do not by themselves state that every source record can be transformed, since executable migration may also depend on defaults, value expressions, and protocol-specific requirements. The Breaking-change gate shows how to apply a compatibility policy in CI.

See also

• Searching for a morphism for span construction and its certificate.
• Find a span between two schemas for the corresponding command.
• Lenses and round-trip laws for bidirectional updates and complements.
• Pushouts and merge for the merge construction.
• Apply field transforms for value-level transforms.
• What panproto verifies for the scope of runtime checks.

Searching for a morphism

Two schemas may describe corresponding records without using the same vertex names or preserving every field. The morphism search chooses the correspondences that satisfy the structural conditions encoded by the schema pair, and it leaves a source vertex unmatched when no admissible image improves the result. The implementation represents this task as a finite optimization problem with explicit feasibility constraints.

This chapter covers:

• the span returned by the search
• the cost function network built from a schema pair
• the exact and bounded algorithms that solve the network
• the construction and certification of the returned span.

The same implementation supports partial overlaps, total morphisms, injective morphisms, and isomorphisms. These requests share an objective but do not always share an algorithm.

The span returned by the search

A span from a source schema $S$ to a target schema $T$ is a pair of schema morphisms with a common domain $A$,

$$S\stackrel{\ell }{\leftarrow }A\stackrel{r}{\to }T.$$

The common domain $A$ is the apex, and $\ell$ and $r$ are the legs. The SchemaSpan returned by panproto gives these terms a specific implementation: $A$ is the sub-schema of $S$ induced by the source vertices that received target images, $\ell$ includes that sub-schema into $S$, and $r$ carries the images chosen by the search. Migrations as morphisms develops the categorical account. Here the span is the concrete output assembled from a solved assignment.

Consider a source schema with an object vertex post, a string vertex post.text, and an integer vertex post.likes. Suppose the target has an object vertex article and a string vertex article.body, but no integer vertex. The object and string vertices exercise kind and edge constraints; the integer vertex introduces dropping.

The source object may take article as an image because the vertex kinds agree. It may not take article.body, since an object vertex cannot map to a string vertex. Kind equality is enforced before the optimizer sees any costs.

The source string may take article.body. If the source has a prop edge from post to post.text and the target has a prop edge from article to article.body, this pair of choices preserves the edge even when the edge names differ. The name difference affects the score, but it does not make the assignment infeasible.

The integer vertex has no target of the same kind. Its only choice is the distinguished value ${\perp }_D$, which means that the vertex is dropped from the apex. If post and post.text are mapped while post.likes takes ${\perp }_D$, the apex contains the first two source vertices and the edge between them. A required-edge declaration can forbid that partial choice: when post requires the edge to post.likes, keeping post also requires both endpoints of that edge to survive.

The symbol ${\perp }_D$ is the drop value. The subscript distinguishes it from the zero cost sometimes written $\perp$ in the valued-constraint literature. This chapter writes the cheapest cost as $0$ and reserves ${\perp }_D$ for the decision to omit a source vertex.

Building the cost function network

build_cfn converts an ordered pair $(S,T)$ into a Cfn, or cost function network. A cost function network is a finite collection of variables, finite domains, and cost tables over small groups of variables. An assignment chooses one value for every variable. Its total cost is the sum of the selected table entries, except that the distinguished cost $\top$ is absorbing and denotes infeasibility. This is a valued constraint satisfaction problem (Schiex et al. 1995), with a closely related semiring reading (Bistarelli et al. 1997).

The builder creates one variable $x_v$ for every source vertex $v$, ordered by source vertex name. Before caller restrictions are applied, its domain is

$$D_v=\{{\perp }_D\}\cup \{a\in V_T:\mathrm{kind}(a)=\mathrm{kind}(v)\}.$$

Target values are sorted by target vertex name. SearchOptions may replace the same-kind candidates with one hard pin, and DomainConstraints may intersect them with an allowed set or remove source and target vertices. An incompatible hard pin leaves ${\perp }_D$ as the only value. Excluding a source vertex has the same effect. The variable remains present, which keeps variable identifiers and the packed-cost radix functions of the source schema alone.

Every assignment determines a partial vertex map. A value $x_v=a$ maps $v$ to $a$, whereas $x_v={\perp }_D$ omits $v$. The all-drop assignment is feasible for every network produced by this builder, so a successfully built span search always has an answer. A build can still fail if its cost tables exceed the memory budget, and inducing the chosen apex can still report an invalid source fragment. Neither failure means that the schemas have no overlap.

For the vertex-and-edge fragment, forbidding ${\perp }_D$ turns feasibility into the usual homomorphism question: each source vertex receives a same-kind target, and each source edge receives a same-kind target edge between the chosen endpoint images. Constraint satisfaction and homomorphism provide two formulations of this decision problem (Feder and Vardi 1998). Its dependence on the structure of the source side, including treewidth modulo homomorphic equivalence, is studied by Grohe (2007). The panproto network adds constraints for schema annotations that a bare graph homomorphism does not carry.

Hard constraints and apex closure

A finite cost ranks an assignment. A $\top$ entry rejects it. The builder enforces seven constraint families. Kind equality is encoded by domain membership, while the other six use $\top$ entries.

The sixth row concerns a span annotation stored inside one schema. It is distinct from the result span $S\stackrel{\ell }{\leftarrow }A\stackrel{r}{\to }T$. A schema-span annotation is a pair of internal vertex references. The result span is the output of comparing two schemas.

The last five constraints make the chosen vertex set closed under source annotations that would otherwise dangle. Hyper-edge signatures are encoded as a clique of pairwise constraints, since partial survival occurs exactly when some pair disagrees about whether to survive. Recursion points and schema-span annotations can also connect variables that share no source edge. The graph used to choose a solver must thus be built after these constraints have been added.

Edge preservation and edge-name scoring share one lookup. For a source edge $e:p\to q$ and mapped endpoint images $a$ and $b$, the builder first seeks a target edge from $a$ to $b$ with the same kind and name. If none exists, it takes the least same-kind edge in the target’s stable edge order. The first case pays no edge penalty, the second pays the full share of the edge component, and the absence of any same-kind edge yields $\top$. When either endpoint takes ${\perp }_D$, the source edge leaves the induced apex and pays the full edge penalty rather than $\top$.

Several source edges may constrain the same pair of variables. CfnBuilder merges their tables pointwise, so the finished network has at most one cost function for each scope. Self-loops are folded into the corresponding unary table. Scope uniqueness is needed by the fallback consistency algorithm as well as by the representation, since cost projection can oscillate when overlapping cost functions offer competing destinations for the same shifted cost (Lee and Leung 2012).

The objective

The network minimizes structural dissimilarity. Three components are unary, one is attached to source edges, and optional alignment evidence adds a fifth unary component.

All denominators depend only on $S$. We call this property source-fixed normalization (SFN). Without SFN, dropping a poorly matched vertex would remove it from an assignment-dependent denominator and could improve the average merely by shrinking the apex. Under SFN, a dropped vertex still occupies its share of the source normalization and receives the worst finite unary penalty for every component that applies to it.

The outgoing-name denominator needs separate treatment. Let $C_S$ be the source vertices with at least one named outgoing edge. The corresponding sum ranges over $C_S$ and divides by $|C_S|$. A source leaf is thus outside that component regardless of whether its target image has children. This prevents the denominator from favoring a childless target for a reason unrelated to the correspondence.

Alignment evidence enters only through the last row. The builder validates every confidence as a number in $[0,1]$, then adds

$$w_{\mathrm{anchor}}\frac{1-\mathrm{confidence}(v,a)}{|V_S|}$$

to the unary entry for mapping $v$ to $a$. Evidence does not alter domains, produce $\top$, choose a variable order, or change a budget. It can change the optimum only when the anchor weight is nonzero. The default weight is zero, so the direct default search is structurally scored even when evidence is present. Alignment evidence describes how strategies produce and aggregate the confidence table.

Each local table entry is assembled in floating point while the network is built, then rounded once to integer units of $10^{-9}$. Every subsequent operation uses the Cost integer. This boundary makes later solver transformations independent of summation order, and it lets the fallback move cost between tables by exact subtraction. Projection and extension rely on that exact difference to preserve the cost of every assignment (Cooper and Schiex 2004).

One integer also carries the secondary preference for coverage. If $q$ is the quality cost in fixed-point units and $\delta$ is the number of dropped source vertices, the stored value is

$$c=q\rho +\delta ,\rho =\mathrm{nextPowerOfTwo}(|V_S|+1).$$

Because $\delta <\rho$, ordinary integer order is lexicographic order on $(q,\delta )$. The search first minimizes quality cost, then chooses the assignment with fewer dropped vertices among assignments tied on quality. The reported quality is $1-q/10^9$ and excludes $\delta$. The separate apex_coverage field reports $|V_A|/|V_S|$, with value one for an empty source.

The primal graph and dispatch

The solver does not branch over complete maps. It first studies how the local tables connect the variables. The primal graph has one node for each variable and an edge between any two variables that occur in one cost-function scope. On the default path, each connected component can be solved independently because no table joins it to another component.

An elimination order processes the primal-graph nodes one at a time. When a node is eliminated, its remaining neighbors are joined into a clique. The largest number of such neighbors encountered along the order is the induced width. This width controls the arity of the intermediate tables created by bucket elimination (Dechter 1999), and it also characterizes the consistency needed for backtrack-free search on sparse constraint graphs [Freuder (1982); Dechter & Pearl (1987)].

For each component, the dispatcher compares descending source-name order with min-fill. Descending order tends to remove dotted-path leaves first; min-fill chooses the variable whose elimination adds the fewest edges. Smaller induced width wins, with descending order retained on a tie so that decoding proceeds in ascending source-name order.

Width selects an order, but the budget check uses the actual domain sizes. For a bucket that eliminates $X$ and sends a message over variables $U$, the implementation prices ${\prod }_{v\in U}|D_v|$ stored entries and $|D_X|{\prod }_{v\in U}|D_v|$ combine operations. These products are summed over the chosen order. Exact inference runs only when both the message memory and operation estimates fit the SearchBudget. Otherwise the component is routed to bounded search. A separate, earlier memory check covers the network’s original unary and local cost tables. Exceeding that build limit is an error because no in-memory network exists for either solver to consume.

Exact inference by bucket elimination

Bucket elimination is the ordinary path when its messages fit. Each original cost function is placed in the bucket of the first variable in its scope under the elimination order. To eliminate $X$, the solver combines every function in $X$’s bucket and minimizes over $D_X$. The resulting message is a table over the other variables in those functions, and it is placed in the next bucket that can consume it. A message with empty scope contributes to the constant cost.

After the last variable is eliminated, the constant is the optimum. Decoding then visits the elimination order in reverse. At each step it selects the least-cost value consistent with the values already decoded. The stored messages guarantee that each such choice extends to a global optimum, so decoding neither branches nor backtracks. This is the (min, sum) instance of the bucket-elimination scheme described by Dechter (1999).

The implementation allocates only the outgoing message for a bucket. It iterates over assignments to the message scope on the outside and values of the eliminated variable on the inside, so it never materializes the full join table. Argmin values are recomputed during decoding rather than stored beside every message cell. This trades a second scan of the domains for lower resident memory.

Exact inference does not consult the node budget and does not prune. The dispatcher has already established that its full tables and loop nests fit the memory and operation budgets before it begins. Completion thus proves optimality. Ties are broken by target name with ${\perp }_D$ ordered after every target, read in decode order. SpanSearch::optima can enumerate further assignments attaining the same optimum while the message tables are available.

The bounded fallback

A component whose elimination messages exceed the budget goes to hybrid best-first search. The outer search keeps a priority queue of unexplored subtrees, each with a certified lower bound. It removes the subtree with the lowest bound and explores it depth first for a bounded number of backtracks, then returns the unexplored branches to the queue. The least bound still present in the queue is a lower bound on the global optimum. This is the hybrid best-first scheme of Allouche et al. (2015).

The fallback maintains one mutable working network. An open node stores its decisions and bound, so revisiting that node resets the network and replays the decisions. Domains are copied at a branch, while changes to cost cells are recorded on a trail and restored to a mark. Local-consistency operations move cost from binary tables into unary tables and then into the zero-arity constant without changing the cost of any complete assignment. The constant is consequently a lower bound for every completion below the node. The default level is existential directional arc consistency, written ${\mathrm{EDAC}}^{\ast }$. The implementation also provides node, arc, directional arc, and full directional arc consistency. These levels and their cost-shifting operations follow the weighted-CSP treatments in Larrosa (2002), Larrosa & Schiex (2004), Cooper et al. (2010), and de et al. (2005).

Branch and bound closes a node when its lower bound reaches the incumbent cost. Before an incumbent exists, value order is determined by the bound obtained after propagating each candidate. Afterward the search tries the incumbent’s saved value first. Variable order uses domain size divided by weighted degree, with additional weight assigned to cost functions that contributed most to a bound failure. These choices affect how soon a solution is found, but they do not change the objective or the certified bounds.

The fallback is bounded by elementary consistency operations and by search nodes. A caller may also set a wall-clock limit, though none is set by default. When a limit is reached, the outcome records the incumbent, the global lower bound, and the limit that stopped the search. A span can thus report a feasible answer without claiming it is optimal. A total-morphism search reports an error if it stops before finding any complete assignment, preserving the distinction between “no total morphism exists” and “the search did not finish.” What panproto verifies describes the property and oracle tests behind these claims. The external toulbar2 solver provides a useful point of comparison for the same family of cost-function-network algorithms.

Injective, surjective, and induced searches

The default network permits two source vertices to share a target. Search options that restrict the whole assignment cannot always be expressed by another local cost table, so they select specialized paths.

The monic option requires distinct surviving source vertices to take distinct target vertices. It runs the same bounded search with a counting Hall-set propagator (McCreesh and Prosser 2015). Variables whose domains still contain ${\perp }_D$ are excluded from the pigeonhole count because they may escape by dropping. Once variables must take target values, the propagator can detect an insufficient union of targets and can remove a saturated Hall set from other domains. A matching-based propagator could enforce stronger generalized arc consistency (Régin 1994), but the implementation does not maintain that additional state. The monic option concerns vertex injectivity only. Parallel source edges may still share one target edge.

The epic option requires a total morphism whose vertex map covers every target vertex. find_span rejects this option because a span deliberately permits a partial right leg. Total-morphism entry points first reject impossible cardinalities, then use branch and bound with surjectivity checked on complete assignments. The check occurs inside optimization rather than after it. Filtering the unconstrained optimum could miss a more expensive assignment that is surjective.

The iso option asks the span search for a common induced sub-schema that is optimal under the packed objective, rather than under cardinality alone. This requires the right leg to reflect arcs as well as preserve them: between mapped vertex pairs, source and target arcs must agree as multisets of direction and edge kind. The implementation adapts the partitioning algorithm of McCreesh et al. (2017) to the network objective. Initial classes use vertex kind and self-loop descriptors. Each mapped pair refines the remaining classes by the multiset of incoming and outgoing edge kinds relative to that pair. Edge names stay out of the labels because they belong to the approximate score rather than structural feasibility.

The induced search measures reward relative to the all-drop assignment and maximizes that reward, which is equivalent to minimizing the original packed cost after its preconditions have been checked. It also reads hard apex constraints when a drop decision makes a required partner unavailable. The use of ${\perp }_D$ and its consequences for propagation are closely related to the constraint model analyzed by McCreesh et al. (2016). For a total isomorphism request, the public entry point additionally requires full coverage of both vertex sets and constructs a bijective edge map.

Assembling the result

Once a solver returns an assignment, SpanSearch collects every source vertex assigned a target and calls induce_on_vertices. Induction restricts all schema fields to the chosen vertex set and validates the result against the supplied protocol. The left leg is the identity on the apex’s vertices and edges. The right leg uses the assignment for vertices and the same edge-selection function used by naturality and edge scoring.

The ordinary right leg chooses an exact kind-and-name edge when one exists and otherwise the least same-kind edge. The iso path instead constructs a kind-preserving bijection within each pair of mapped endpoints, preferring equal names before pairing the remaining parallel edges. This distinction is recorded because injectivity on vertices does not imply injectivity on edges.

The span carries both measurements and a certificate. quality reads the assignment’s primary cost, including the alignment-evidence component when its weight is nonzero. It does not include the packed secondary reward for retaining more vertices. apex_coverage records the fraction of source vertices retained. quality_bounds converts the solver’s lower and upper primary-cost bounds into the corresponding interval on the higher-is-better quality scale.

The certificate records whether optimality was proved, which solver path ran, and which limit was reached. Its shape distinguishes vertex injectivity from edge-image injectivity and records whether the left inclusion covers the whole source. Both legs are checked for functoriality. Separate existence reports are computed for the two codomains, conditional obligations being available when the caller supplied the relevant theory registry. The certificate also records whether the induced apex has an entry vertex, a content digest of the apex, and the decode order used for exact tie-breaking. Find a span between two schemas shows how these fields are read through the public interface.

Boundaries of the implementation

The search maps each source edge to one target edge. It does not map an edge to a target path, so it implements the length-one fragment of the functorial schema translations described by Spivak (2012). A correspondence that requires an intermediate target vertex or several target fields belongs in a value-level transform rather than in this vertex assignment. Migrations as morphisms develops that boundary.

The objective reads vertex identifiers, vertex kinds, outgoing edges, and edges between candidate endpoint images. Required edges, variants, recursion points, schema-span annotations, and hyper-edge signatures affect feasibility without affecting the finite score. Other schema fields, including value constraints, usage modes, defaults, and policies, are restricted during induction or checked later but do not distinguish two feasible assignments here. An existence report may consequently mark a selected leg invalid even when another equally scored assignment would have passed.

The five component weights have not been fitted to labeled correspondences. Work on schema and ontology matching shows that aggregation and extraction choices can materially change the resulting alignment [Do & Rahm (2002); Meilicke & Stuckenschmidt (2007); Faria et al. (2013)]. Exact optimization guarantees an argmin of the stated cost function. It does not establish that the cost function ranks the intended correspondence first.

The remaining input to that cost function is the confidence table. Alignment evidence explains how panproto constructs it and where hard pins still differ from soft evidence.

Alignment evidence

Automatic alignment begins with candidate pairs of source and target vertices. panproto calls each candidate an anchor. An anchor records the pair, a confidence, a strategy tag, the provenance of the comparison, and an explanation. The search has not accepted the pair merely because an anchor names it.

The implementation has two routes from anchors to a search. The EvidenceTable API can score every candidate pair and pass those scores to a span search. The automatic lens generator currently takes a different route: it selects a one-to-one seed map, places those pairs in SearchOptions::hard_pins, and then compares that pinned search with a second search in which the strategy pins have been released. The evidence-table route supplies soft scores, whereas auto-lens temporarily restricts the search with provisional pins and then compares the pinned and released results.

Active proposal strategies

The auto-lens pipeline calls twelve strategy emitters. Their schedule is fixed by Stringency.

Three details qualify this table. First, ExactSuffix and EdgeLabel run even at Strict; strict mode thus runs more than exact identifier equality. Second, Coerce emits proposals and witness metadata, but the morphism-search domains still exclude kind-mismatched targets. A coerce proposal cannot steer the current search, though callers can inspect it in AutoLensResult::coerce_proposals. Third, neighborhood propagation is a second pass. Auto-lens aggregates and selects the other strategies to obtain parent seeds, emits neighborhood anchors from those seeds, and then aggregates the full pool again.

The StrategyTag enum has fourteen variants because it also reserves UserHint and Llm. Neither variant names an auto-lens strategy emitter. The hint-taking auto-lens APIs put caller mappings directly into hard_pins; after the search, they construct UserHint anchors for the returned explanations and candidate metadata. Llm is an extension point. No production function emits that tag, and no auto-lens configuration field accepts language-model proposals. A caller can still construct either kind of anchor and use the public evidence API directly.

From anchors to scores

The reducer in panproto_mig::align::evidence produces one score for each pair mentioned by at least one anchor. It discards anchors with a NaN confidence. Every other raw confidence is clamped to the unit interval and capped by its Provenance.

Under the default StrictPriority aggregation policy, the fourteen tags occupy priority bands of width $1/14$. Let $r$ be the tag’s rank, with zero denoting UserHint and thirteen denoting Llm, and let $c$ be the clamped, provenance-capped confidence. The effective value is

$$e=\frac{13-r+c}{14}.$$

The implementation performs this as one division. Adjacent bands share an endpoint, so a tag’s weakest value can equal the strongest value in the band immediately below it. The ordering is thus non-strict at those boundaries. The alternative ConfidenceFirst policy omits the bands and uses $c$ directly.

The reducer next groups anchors by the input from which they were computed. For each family it retains the largest effective value.

Alias is the one branch-sensitive case. A leaf alias compares identifiers and belongs to the identifier family. A composite alias compares outgoing edge labels and belongs to the edge-label family. The anchor’s provenance distinguishes these branches.

If $f_j$ is the maximum for family $j$, with zero for a family that emitted nothing, the ordinary family mean is

$$m=\frac{1}{6}\sum _{j=1}^6{f}_j.$$

The fixed divisor makes this mean monotone under literal pool inclusion: adding an anchor can increase a family maximum or leave it unchanged. A divisor that counted only the families that fired could fall when a weak new family appeared.

User hints receive one additional rule. If $h$ is the largest capped confidence among UserHint anchors for the pair, the reported score is

$$s=\max (m,h).$$

Thus the often useful $k/6$ bound applies only to a pair without the hint override. Evidence from $k$ ordinary families cannot exceed $k/6$, while one full-confidence UserHint anchor yields a score of $1.0$. The unit tests assert both cases.

Before neighborhood propagation, auto-lens also adjusts the confidences already in the pool by required-set agreement. It adds $0.05$ when both vertices are required, subtracts $0.05$ when only one is required, and clamps the result. UserHint anchors are exempt. Neighborhood anchors are appended after this adjustment and thus do not receive it.

Selection

Aggregation and selection are separate public operations. EvidenceTable::select accepts a configurable RowFilter and Cardinality rule. A row filter first applies an absolute threshold, then retains candidates within a relative delta of the best score for the same source. Strict permits one selected pair at each endpoint. Permissive admits a conflict when no previously accepted conflict has a strictly better score. Hybrid uses that permissive rule at lower confidence and permits up to card + 1 selected pairs at an endpoint above high_conf. The final greedy pass is deterministic because it sorts by score and then by the two identifiers.

Auto-lens does not expose those choices through AutoLensConfig. Both of its seed-selection passes use Cardinality::Strict with RowFilter::relative_only(). The resulting seed map has at most one pair at either endpoint, the absolute threshold is zero, and the relative delta is the library default of $0.02$. The default absolute floor and the hybrid cardinality constants do not govern auto-lens seed selection.

Selection is also absent from the evidence-aware network builder. A caller that passes an evidence table to a span search gives the builder all pair scores; the solver chooses a complete assignment under the structural constraints and objective.

The evidence-aware span API

SpanSearch::with_evidence attaches an evidence table to the cost-function network. For source vertex $v$, target vertex $a$, and source vertex set $V_S$, the builder adds the unary term

$$C_{\mathrm{anchor}}(v,a)=w_{\mathrm{anchor}}\frac{1-s(v,a)}{|V_S|}.$$

This term does not remove a target from a domain, add a hard constraint, or change the variable set. A score outside $[0,1]$ is rejected when the network is built. For a fixed non-negative weight, increasing a pair’s score can only lower the cost of assignments that use that pair.

The shipped anchor weight is $0.0$. With the default CostWeights, every evidence table thus contributes the same zero-weight term and cannot change the selected span. Callers can supply a non-zero weight through SpanSearch::with_weights; the tier and monotonicity tests do so to exercise the evidence term.

This path is public, but it is not the route used by current production code in the repository. The ordinary find_span helpers construct SpanSearch with NoEvidence, and the auto-lens source does not call with_evidence. Current production behavior should thus be described through provisional pins, not through the reward-only term.

The auto-lens route

The single-result auto-lens pipeline resolves the strategy pool to a strict seed map and merges those seeds into SearchOptions::hard_pins without replacing caller pins. A hard pin collapses one source vertex’s domain to the named target, plus the option to drop that vertex. The first search thus gives selected strategy proposals the force of domain restrictions.

Auto-lens then runs a released search whenever the strategies added at least one pin. This second search retains the caller’s original pins and removes the strategy pins. The single-result APIs compare the two answers by the search objective: higher alignment quality wins, followed by more mapped source vertices. The pinned answer remains when both measures tie. Since releasing strategy pins adds domain values, the released search ranges over a superset of the pinned search when all other options are fixed.

The multi-candidate APIs use a different comparison. They choose between the pinned and released candidate lists by their best coverage, and they return a fully covering pinned list without running the released comparison. Claims about objective-based comparison should thus be limited to auto_generate and auto_generate_with_hints.

Caller hints remain hard on both attempts. The public hint parameter and SearchOptions::hard_pins express fixed correspondences in current auto-lens behavior. A soft user hint exists at the evidence-table level, but production auto-lens does not route hints there.

Monotonicity and stringency

Evidence aggregation is monotone under pool inclusion. If pool $P^{\prime }$ contains every anchor in $P$, then every score produced from $P^{\prime }$ is at least the corresponding score from $P$. This property follows from the per-family maxima, the fixed divisor, and the maximum with the hint confidence.

An evidence-aware network has the same feasible assignments for every evidence table. Under a non-zero anchor weight, pointwise domination of one evidence table by another gives a non-increasing cost for every assignment and hence for the optimum. Under the shipped zero weight, all such costs are equal.

Stringency tiers do not guarantee pool inclusion. WlRefinement uses two iterations at Lenient and three at Exploratory; another refinement round can split a color class and withdraw an earlier anchor. Neighborhood depends on a selected seed map, so a larger first-pass pool can change the seeds and withdraw propagated anchors. The integration tests include a concrete Lenient-to-Exploratory case in which a neighborhood anchor disappears, the evidence score falls, and an anchor-weighted optimum becomes worse. General tier monotonicity is thus false. The tests assert monotonicity only when the higher tier’s evidence table dominates pointwise, and they separately check that any shortfall comes from WlRefinement or Neighborhood.

Production auto-lens adds further tier-dependent behavior: Strict and Balanced ask for total morphisms, Lenient and Exploratory permit spans, and the latter tiers enable overlap retries by default. The pool-inclusion theorem for aggregate does not extend to the full auto-lens tier ladder.

Defaults and evidence for the design

panproto has no labeled corpus of intended schema correspondences. The priority order, family partition, provenance ceilings, strategy thresholds, scoring coefficients, and objective weights have not been fitted to panproto data.

The align::defaults module centralizes the provenance ceilings, the general selection defaults, and the shipped anchor weight. It does not contain every numeric choice in the alignment pipeline. Tier thresholds live in auto_lens.rs, while the required-set adjustment lives in align/mod.rs. Strategy-specific mixture weights, confidence floors, and fixed confidences live with their emitters. An audit of all alignment numbers thus spans several files.

Prior work supplies design precedents rather than a validation of these settings. COMA evaluated composite similarity aggregation and matrix-selection rules (Do and Rahm 2002). The analysis of mapping extraction by Meilicke & Stuckenschmidt (2007) supports treating selection as a separate stage. AgreementMakerLight supplies precedents for provenance weights and cardinality-aware selection, though panproto’s constants are not corpus fits (Faria et al. 2013). The reducer also avoids Dempster-Shafer combination because several strategies are deterministic readings of the same input rather than independent sources, the condition required by that combination rule (Dempster 1967). None of these results establishes that panproto’s current family partition or parameter values are optimal.

The evidence-aware span API provides the soft scoring route. Current auto-lens behavior still passes through selected provisional pins, which is why Searching for a morphism treats evidence and domain restrictions separately.

See also

• Searching for a morphism for the objective and span-search constraints.
• Find a span between two schemas for the public span-search interface.
• Migrations as morphisms for the morphisms produced by the search.
• What panproto verifies for the mechanically checked properties.
• CLI reference for the user-facing stringency and hint options.

Lenses and round-trip laws

Suppose a source record contains name and age, while a view exposes only name. Reading the view discards age, but a later update to name should preserve it. A lens coordinates this forward observation and backward reconstruction (Foster et al. 2007). In panproto, the forward operation returns both the view and a complement, a record of information needed to reconstruct the source. This explicit complement is related to the constant-complement view-update account and later symmetric lenses [Bancilhon & Spyratos (1981); Hofmann et al. (2011)].

A concrete Lens stores a compiled migration together with its source and target schemas. Its operations are fallible because migration execution or reconstruction may reject a concrete input. For a fixed lens, their mathematical shape is

$$get:S\to V\times Cput:V\times C\to S.$$

In Rust, get returns a WInstance view and a Complement, and put consumes the edited view and complement to reconstruct a source WInstance. The complement represents the original source; callers do not pass it separately to put.

Round-trip laws

Three equations describe the expected interaction between these operations. Writing $get(s)=(v,c)$, GetPut requires $put(v,c)=s$. If $put(v^{\prime },c)=s^{\prime }$, PutGet requires the view component of $get(s^{\prime })$ to equal $v^{\prime }$. PutPut requires a later update to supersede an earlier update, with the intermediate complement threaded according to the lens.

The implementation provides checks with different scopes. check_laws runs GetPut and PutGet for a supplied lens and source instance. Its PutGet check uses the original view and one fixed scalar mutation, so it is a deterministic smoke check rather than a universal quantification over edits. panproto_lens::laws::check_put_put is a separate operation. It gets the original complement, performs an initial put, gets the complement of that intermediate source, and compares a sequential second put with a direct second put from the original complement.

Property tests exercise the equations over generated lens and instance families. These tests can reveal failures within those families, but they do not prove lawfulness for every migration or input. Constructing a Lens also does not run every law check automatically. What panproto verifies distinguishes these forms of evidence.

Complement composition

Composed lenses must also combine their complements. The ComplementCompose extension trait defines a checked partial composition through compose and is_compatible. Two nonzero source-schema fingerprints must agree; zero represents an unspecified fingerprint. Conflicting nonzero fingerprints produce ComplementFingerprintMismatch. If both complements store a value for the same key, those values must agree or composition returns ComplementConflict. Collection-valued fields are combined without duplicate elements.

These conditions prevent composition from selecting arbitrarily between incompatible saved states. They establish compatibility of the concrete complements being composed, rather than lawfulness of the underlying lenses.

Lens construction

Migrations as morphisms describes the compiled migration that supplies a concrete lens’s transformation tables. A migration and its endpoint schemas can be assembled into a Lens, after which callers may run the law checks above. This construction does not imply that every migration is lawful.

The panproto-lens-dsl crate compiles declarative Nickel, JSON, or YAML descriptions into lens combinators. The panproto-lens::protolens module describes schema-parameterized transformations that can be instantiated when their structural preconditions hold. Edge kinds select optic forms such as lenses, prisms, affine traversals, and traversals; this dispatch follows the profunctor-optics account of Pickering et al. (2017) and its categorical formulation in Clarke et al. (2024). The representation of schema migrations as a graph of lenses is related to Cambria (Litt et al. 2020).

EditLens::put_edit translates a view edit back to the source and updates the stored complement at the same time. Edit lenses model changes through edit monoids and actions (Hofmann et al. 2012). The subtree-complement rules here are panproto-specific: deleting a subtree clears its complement entries, while inserts, relabels, and field updates maintain the relevant saved state. The edit-law helpers compare this incremental result with whole-state get and put for one supplied edit.

SymmetricLens::from_span requires its two asymmetric legs to share a middle schema. The current equality check compares the protocol, vertices, edges, hyperedges, constraints, required edges, variants, orderings, recursion points, and nominal flags. It deliberately omits byte-layout constraints and usage modes, and it also does not compare NSIDs, entry lists, schema-span annotations, coercions, mergers, defaults, policies, or derived adjacency indices. Acceptance by this constructor is thus equality under that implemented projection, not complete Schema equality.