Docs · Reference

The vt command

vt checks, hashes, converts and certifies charts, generates TypeScript for the browser, and reshards a stopped cluster. This page lists every subcommand with its real help text and a real run on a chart from the repository.

All outputs on this page come from the vt binary built from the current sources. Commands are run from the repository root unless the text says otherwise. Very long outputs are trimmed, and each trim is marked.

Getting vt

vt is the binary of the vertep-cli crate (crates/vertep-cli). Install it from crates.io with cargo install vertep-cli, or build it from a checkout:

cargo build --release -p vertep-cli
./target/release/vt --version

vt 0.1.0

You can also run it through Cargo without building a release binary: cargo run -p vertep-cli -- validate <chart>. Or install it into ~/.cargo/bin with cargo install --path crates/vertep-cli. The examples below write vt for whichever you use.

vt --help

The vt command line: typecheck, schema, validate, hash, convert and certify

Usage: vt <COMMAND>

Commands:
  typecheck  Type-check a chart and report every error with its location
  schema     Print a projection of the chart's types
  validate   Check well-formedness and SHACL conformance
  hash       Print the chart version IRI
  convert    Convert a chart to another surface, refusing lossy conversions
  certify    Run the Lean checker and print the certificate
  gen        Generate code from a chart
  cluster    Cluster operations
  help       Print this message or the help of the given subcommand(s)

Options:
  -h, --help     Print help
  -V, --version  Print version

How vt reads a chart

Every subcommand that takes a chart accepts any surface. vt picks the reader from the file extension. When the extension is unknown it looks at the content: XML that contains <scxml is SCXML, a line starting with vertep: is YAML, a document starting with @prefix or PREFIX is read as TriG, and anything else as N-Quads. The rules live in crates/vertep-cli/src/surface.rs.

Every command uses the same three exit codes, so scripts and CI jobs can tell a bad chart from a bad invocation:

vt hash no-such-chart.scxml; echo "exit $?"
vt schema examples/typed-order/order.yaml; echo "exit $?"

no-such-chart.scxml: cannot read: No such file or directory (os error 2)
exit 2
error: the following required arguments were not provided:
  --format <FORMAT>

Usage: vt schema --format <FORMAT> <CHART>

For more information, try '--help'.
exit 2

Errors go to standard error, results to standard output. A diagnostic that has a position is written file:line:column: message, the form editors and CI annotations understand.

vt typecheck

Type-check a chart and report every error with its location

Usage: vt typecheck <CHART>

Arguments:
  <CHART>  The chart file

Options:
  -h, --help  Print help

typecheck runs the core type checker with the typer of the chart's datamodel. For a CEL chart it then also checks every CEL expression against the type environment built from the chart's declarations. On success it counts what it checked. A chart that declares no types is reported as untyped, which is not an error.

examples/typed-order/order.yaml is a typed order chart on the CEL datamodel, with three named types, six typed events and three context fields:

vt typecheck examples/typed-order/order.yaml
vt typecheck crates/vertep-dm-rust/tests/charts/order.scxml
vt typecheck crates/vertep-agent/examples/support-agent.scxml

examples/typed-order/order.yaml: ok: 3 named types, 6 typed events, 3 context fields
crates/vertep-dm-rust/tests/charts/order.scxml: ok: 2 named types, 5 typed events, 2 context fields
crates/vertep-agent/examples/support-agent.scxml: ok: untyped

examples/typed-order/order-ill-typed.yaml is the same chart with one deliberate mistake: the add transition assigns the item's sku, a string, to ctx.total, a decimal.

      cart:
        on:
          add:
            - cond: "ev.data.qty > 0"
              actions:
                - assign: { location: ctx.items, expr: "ctx.items + [ev.data]" }
                - assign: { location: ctx.total, expr: "ev.data.sku" }

vt typecheck examples/typed-order/order-ill-typed.yaml; echo "exit $?"

examples/typed-order/order-ill-typed.yaml:44:19: states.shopping.states.cart.on.add[0].actions[1]: state "cart", transition 0 (on add), action 1: the value assigned to `ctx.total` has type string, expected decimal
exit 1

For YAML the error carries two locations: the line and column in the file, and the path through the document (states.shopping.states.cart.on.add[0].actions[1]). Then comes the location in chart terms: state, transition, action.

The same chart converted to SCXML (see convert; conversion only checks structure, so an ill-typed chart converts) reports the error at the <assign> element, followed by a count:

vt convert examples/typed-order/order-ill-typed.yaml --to scxml -o ill.scxml
vt typecheck ill.scxml; echo "exit $?"

ill.scxml:23:9: state "cart", transition 0 (on add), action 1: the value assigned to `ctx.total` has type string, expected decimal
ill.scxml: 1 type error
exit 1

The type language itself, and which datamodels have a typer, are described in Datamodels and types.

vt schema

Print a projection of the chart's types

Usage: vt schema --format <FORMAT> <CHART>

Arguments:
  <CHART>  The chart file

Options:
      --format <FORMAT>  The projection [possible values: rust, jsonschema, shacl, cel]
  -h, --help             Print help

schema type-checks the chart first and prints nothing if that fails (exit 1). Then it prints one projection of the chart's types:

The examples use crates/vertep-dm-rust/tests/charts/order.scxml, a typed chart whose types are declared in a vt:types block:

<vt:types xmlns:vt="https://w3id.org/vertep/vt#">type Pay = { amount: decimal };
type Approval = { by: iri };
event start;
event pay: Pay;
event authorized;
event approve: Approval;
event cancel;
</vt:types>
<datamodel>
  <data id="total" expr="0" vt:type="decimal"/>
  <data id="limit" expr="100" vt:type="decimal"/>
</datamodel>

vt schema crates/vertep-dm-rust/tests/charts/order.scxml --format cel

ctx.total: decimal
ctx.limit: decimal
ev.data[start]: null_type
ev.data[pay]: Pay
ev.data[authorized]: null_type
ev.data[approve]: Approval
ev.data[cancel]: null_type

vt schema crates/vertep-dm-rust/tests/charts/order.scxml --format jsonschema

{
  "context": {
    "$schema": "https://json-schema.org/draft/2020-12/schema",
    "additionalProperties": false,
    "properties": {
      "limit": {
        "anyOf": [
          {
            "type": "number"
          },
          {
            "pattern": "^-?[0-9]+(\\.[0-9]+)?$",
            "type": "string"
          }
        ]
      },
      "total": { … same as limit … }
    },
    "required": [
      "total",
      "limit"
    ],
    "type": "object"
  },
  "events": {
    "approve": {
      "$defs": {
        "Approval": {
          "additionalProperties": false,
          "properties": {
            "by": {
              "pattern": "^[A-Za-z][A-Za-z0-9+.\\-]*:(?:[^\\x00-\\x20\\x7F<>\"{}|\\\\^`%]|%[0-9A-Fa-f]{2})*$",
              "type": "string"
            }
          },
          "required": [
            "by"
          ],
          "title": "Approval",
          "type": "object"
        }
      },
      "$ref": "#/$defs/Approval",
      "$schema": "https://json-schema.org/draft/2020-12/schema"
    },
    "authorized": {
      "$schema": "https://json-schema.org/draft/2020-12/schema",
      "type": "null"
    },
    …
  }
}

A decimal accepts a JSON number or a string of decimal digits. An iri is a string with an IRI pattern. Records are closed ("additionalProperties": false).

vt schema crates/vertep-dm-rust/tests/charts/order.scxml --format shacl

@prefix c: <urn:vertep:chart:sha256:05bdae901f2ef328f81ad649674bac2beab559eac46bae2dbc34db1bdcd2e38f#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix sh: <http://www.w3.org/ns/shacl#> .
@prefix vt: <https://w3id.org/vertep/vt#> .
…
c:context.f.limit a sh:PropertyShape ;
	sh:maxCount 1 ;
	sh:minCount 1 ;
	sh:node c:context.f.limit.t ;
	sh:path <https://w3id.org/vertep/field#limit> .
…
c:context a sh:NodeShape ;
	sh:closed true ;
	sh:nodeKind sh:BlankNode ;
	sh:property c:context.f.limit , c:context.f.total .
c:event.approve a sh:NodeShape ;
	sh:node <urn:vertep:type:sha256:78b8b5724ef01cf7b643dc932acb99c0504f0928315f6e79cc6c0e966ce37d24> .
c:event.pay a sh:NodeShape ;
	sh:node <urn:vertep:type:sha256:41b1c80782c0edf4c066dd3ac0c6235285690642f6ec20b1bb77e8e7e1bd632f> .
…
<urn:vertep:type:sha256:78b8b5724ef01cf7b643dc932acb99c0504f0928315f6e79cc6c0e966ce37d24> a sh:NodeShape , vt:NamedType ;
	sh:closed true ;
	sh:nodeKind sh:BlankNode ;
	sh:property <urn:vertep:type:sha256:78b8b5724ef01cf7b643dc932acb99c0504f0928315f6e79cc6c0e966ce37d24#s.f.by> ;
	vt:definition <urn:vertep:type:sha256:78b8b5724ef01cf7b643dc932acb99c0504f0928315f6e79cc6c0e966ce37d24#t> ;
	vt:typeName "Approval" .

Named types get content-addressed IRIs (urn:vertep:type:sha256:…), so two charts that declare the same Approval type share its shape. The context and event shapes hang off the chart version IRI.

vt schema crates/vertep-dm-rust/tests/charts/order.scxml --format rust; echo "exit $?"

crates/vertep-dm-rust/tests/charts/order.scxml: the Rust projection is generated at compile time by the statechart! and include_chart! macros (vertep-macros); use include_chart!("crates/vertep-dm-rust/tests/charts/order.scxml") to get the typed Rust API
exit 2

vt validate

Check well-formedness and SHACL conformance

Usage: vt validate <CHART>

Arguments:
  <CHART>  The chart file

Options:
  -h, --help  Print help

validate checks the chart's structure, not its types. It runs three checks and reports everything it finds:

1. the core well-formedness rules (unique ids, valid targets and initial states, legal attribute combinations, and so on);
2. the SHACL chart shapes, run against the chart's RDF projection;
3. that the type shapes embedded in the projection parse as SHACL.

On success it prints the chart version IRI.

vt validate crates/vertep-agent/examples/support-agent.scxml
vt validate examples/traffic-light/traffic-light.scxml

crates/vertep-agent/examples/support-agent.scxml: ok: urn:vertep:chart:sha256:b0b8e9574ca25b8572269bf25a2d4e199f7db5dc6b47bd0574a9d662ec2d2462
examples/traffic-light/traffic-light.scxml: ok: urn:vertep:chart:sha256:46431c540d155bee9016c61ee7a8f734890a92342ed9f91188aea25a602f5731

The SCXML reader's test corpus has a chart that uses every SCXML element, crates/vertep-scxml/tests/corpus/all_elements.scxml. One of its <invoke> elements has both namelist and a <param> child, which SCXML forbids:

<invoke type="scxml" id="child" autoforward="true" namelist="counter">
  <param name="a" expr="1"/>
  …
</invoke>

vt validate crates/vertep-scxml/tests/corpus/all_elements.scxml; echo "exit $?"

crates/vertep-scxml/tests/corpus/all_elements.scxml:62:9: ConflictingAttributes { element: "invoke", attributes: "param, namelist" } at Invoke { state: "r2", index: 0 }
crates/vertep-scxml/tests/corpus/all_elements.scxml: shapes: <urn:vertep:chart:sha256:949a45ea97433907f548d026509517254b3a25aab6edf582ff3e3e725d7b6504#s.r2:inv0> = <urn:vertep:chart:sha256:949a45ea97433907f548d026509517254b3a25aab6edf582ff3e3e725d7b6504#s.r2:inv0>: invoke has conflicting attributes (AndConstraintComponent)
exit 1

The same rule is broken twice: once by the Rust well-formedness check, with the element's line and column, and once by the SHACL shapes, with the IRI of the offending node in the projection. The two checks are meant to agree; that agreement is the "shapes equivalence" property described in Verification.

A duplicate state id is caught when the chart is read, before any other check. This two-line chart was written for this page:

<scxml xmlns="http://www.w3.org/2005/07/scxml" version="1.0" initial="a">
  <state id="a"><transition event="go" target="b"/></state>
  <state id="a"/>
  <final id="b"/>
</scxml>

$ vt validate dup.scxml; echo "exit $?"
dup.scxml:3:3: state id `a` is already declared at 2:3
exit 1

vt hash

Print the chart version IRI

Usage: vt hash <CHART>

Arguments:
  <CHART>  The chart file

Options:
  -h, --help  Print help

hash prints the chart version IRI: urn:vertep:chart:sha256: followed by the SHA-256 of the RDFC-1.0 canonical form of the chart's RDF projection. The projection is built from the IR, not from the source text, so the same chart written in SCXML and in YAML has the same version. crates/vertep-dm-rust/tests/charts/ holds the order chart in both surfaces:

vt hash crates/vertep-dm-rust/tests/charts/order.yaml
vt hash crates/vertep-dm-rust/tests/charts/order.scxml

urn:vertep:chart:sha256:05bdae901f2ef328f81ad649674bac2beab559eac46bae2dbc34db1bdcd2e38f
urn:vertep:chart:sha256:05bdae901f2ef328f81ad649674bac2beab559eac46bae2dbc34db1bdcd2e38f

Comments, formatting and attribute order do not change the version. Any change to states, transitions, executable content or declared types does. The runtime records this IRI in every journal entry, so a replay can find the exact chart that produced it. See RDF and versions.

vt convert

Convert a chart to another surface, refusing lossy conversions

Usage: vt convert [OPTIONS] --to <TO> <INPUT>

Arguments:
  <INPUT>  The chart file

Options:
      --to <TO>          The target surface [possible values: scxml, yaml, turtle, trig, nquads]
  -o, --output <OUTPUT>  Write here instead of standard output
  -h, --help             Print help

convert reads a chart in any surface and writes it in another. It reads structure only, without the type checker, so you can convert a chart that does not type-check yet. The traffic light in examples/traffic-light/traffic-light.scxml, as YAML:

vt convert examples/traffic-light/traffic-light.scxml --to yaml

vertep: 1
name: traffic-light
datamodel: "null"
initial: operating
states:
  operating:
    type: parallel
    on:
      fault: flashing
    states:
      light:
        initial: red
        states:
          red:
            entry:
              - send:
                  event: tick
                  id: light-timer
                  delay: "30s"
            exit:
              - cancel:
                  sendid: light-timer
            on:
              tick: green
          …
      crossing:
        initial: dont_walk
        states:
          dont_walk:
            always:
              cond: "In('red')"
              target: walk
          walk:
            always:
              cond: "In('green')"
              target: dont_walk
  flashing:
    on:
      reset: operating

The RDF targets print the chart's projection, the same graph vt hash hashes. Every node IRI is minted under the chart version (c: below), so the projection has no blank nodes:

vt convert examples/traffic-light/traffic-light.scxml --to turtle

@prefix c: <urn:vertep:chart:sha256:46431c540d155bee9016c61ee7a8f734890a92342ed9f91188aea25a602f5731#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix vt: <https://w3id.org/vertep/vt#> .
c:chart:ia0 a vt:TargetRef ;
	vt:order 0 ;
	vt:scope c:chart ;
	vt:state c:s.operating .
c:chart:ia:sel:chart vt:choice c:s.operating .
c:chart:ia:sel:s.operating vt:choice c:chart:ia0 .
c:chart a vt:Chart ;
	vt:binding "early" ;
	vt:bindingExplicit false ;
	vt:child c:s.flashing , c:s.operating ;
	vt:datamodel "null" ;
	vt:datamodelExplicit true ;
	vt:initial c:chart:ia0 ;
	vt:name "traffic-light" .
…

--to trig and --to nquads write the same graph inside the named graph whose name is the version IRI. Conversions go both ways. Here the typed YAML order goes to Turtle, then from Turtle to SCXML, and all three files hash to the same version (run in a scratch directory):

vt convert examples/typed-order/order.yaml --to turtle -o order.ttl
vt convert order.ttl --to scxml -o order.scxml
vt hash examples/typed-order/order.yaml
vt hash order.ttl
vt hash order.scxml

urn:vertep:chart:sha256:ae074948acdd6ec8df8096c10dabea5b2dad1cd94faab314727f02dffb78c6c1
urn:vertep:chart:sha256:ae074948acdd6ec8df8096c10dabea5b2dad1cd94faab314727f02dffb78c6c1
urn:vertep:chart:sha256:ae074948acdd6ec8df8096c10dabea5b2dad1cd94faab314727f02dffb78c6c1

In the SCXML written from YAML, the declared types become a vt:types block and vt:type attributes on <data>:

<?xml version="1.0" encoding="UTF-8"?>
<scxml xmlns="http://www.w3.org/2005/07/scxml" xmlns:vt="https://w3id.org/vertep/vt#" version="1.0" name="order" datamodel="cel" initial="shopping">
  <vt:types xmlns:vt="https://w3id.org/vertep/vt#">type Item = { sku: string, qty: int, price: decimal };
type Pay = { amount: decimal, method: Card { last4: string } | Invoice };
type Ship = { carrier: string, tracking: optional&lt;string&gt; };
event add: Item;
…
</vt:types>
  <datamodel>
    <data id="items" expr="[]" vt:type="list&lt;Item&gt;"/>
    <data id="total" expr="0" vt:type="decimal"/>
    <data id="limit" expr="500" vt:type="decimal"/>
  </datamodel>

Lossy conversions are refused

convert writes nothing when the output would not carry everything the input says. It lists each loss and exits 1. Losses come from two places:

• Reading. The SCXML reader records what it drops: an attribute SCXML does not define, an extension on an element that has no extension slot, ambiguous inline content. Foreign-namespace extensions are kept as opaque nodes, so they are not losses. Comments, whitespace and the XML declaration are formatting and are not reported.
• Writing. The SCXML writer reports text XML 1.0 cannot carry and extension names that are not XML names. The YAML writer reads its own output back and refuses if the result is not the same chart.

This chart, written for this page, has an attribute SCXML does not define:

<scxml xmlns="http://www.w3.org/2005/07/scxml" version="1.0" initial="a" colour="red">
  <state id="a">
    <transition event="go" target="b"/>
  </state>
  <final id="b"/>
</scxml>

vt convert lossy.scxml --to yaml; echo "exit $?"

lossy.scxml: refusing to convert scxml to yaml: it would lose:
  - lossy.scxml:1:1: attribute `colour` is not defined on <scxml>
exit 1

The refusal applies to every target, --to scxml included, because the attribute is already gone once the chart is read.

vt gen ts

Generate code from a chart

Usage: vt gen <COMMAND>

Commands:
  ts    The TypeScript module for @vertep/web: events, context, state ids and a typed actor
  help  Print this message or the help of the given subcommand(s)

Options:
  -h, --help  Print help

The TypeScript module for @vertep/web: events, context, state ids and a typed actor

Usage: vt gen ts [OPTIONS] <CHART>

Arguments:
  <CHART>  The chart file

Options:
      --name <NAME>  The prefix of the generated names (default: the chart name or file stem)
  -h, --help         Print help

gen ts type-checks the chart and prints a TypeScript module for @vertep/web. The module holds an event union, a context interface, a union of state ids, the chart itself as a typed ChartSpec (its source text, format and version IRI), and a create<Name>Actor function. The name prefix is the chart's name, else the file stem, in PascalCase.

vt gen ts crates/vertep-dm-rust/tests/charts/order.scxml > order.ts

// Generated by `vt gen ts` from chart urn:vertep:chart:sha256:05bdae901f2ef328f81ad649674bac2beab559eac46bae2dbc34db1bdcd2e38f. Do not edit.
import type { ActorRef, ActorSystem, ChartSpec, JsonValue } from "@vertep/web";

export type Pay = { amount: number | string };
export type Approval = { by: string };

export type OrderEvent =
  | { type: "start" }
  | { type: "pay" } & Pay
  | { type: "authorized" }
  | { type: "approve" } & Approval
  | { type: "cancel" };
export interface OrderContext {
  total: number | string;
  limit: number | string;
}
export type OrderStateId = "idle" | "checkout" | "cart" | "payment" | "review" | "paid" | "cancelled";

/** The chart, typed: pass it to `spawn` or `virtual`. */
export const orderChart: ChartSpec<OrderEvent, OrderContext, OrderStateId> = {
  source: "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n<scxml xmlns=…",
  format: "scxml",
  type: "urn:vertep:chart:sha256:05bdae901f2ef328f81ad649674bac2beab559eac46bae2dbc34db1bdcd2e38f",
};

/** The virtual actor of this chart with `key`, typed. */
export function createOrderActor(system: ActorSystem, key: string): ActorRef<OrderEvent, OrderContext, OrderStateId> {
  return system.virtual(orderChart, key);
}

An untyped chart still gets state ids, but events and context fall back to JSON values. --name sets the prefix:

vt gen ts crates/vertep-agent/examples/support-agent.scxml --name Support

// Generated by `vt gen ts` from chart urn:vertep:chart:sha256:b0b8e9574ca25b8572269bf25a2d4e199f7db5dc6b47bd0574a9d662ec2d2462. Do not edit.
import type { ActorRef, ActorSystem, ChartSpec, JsonValue } from "@vertep/web";

export type SupportEvent = { type: string; [field: string]: JsonValue };
export type SupportContext = JsonValue;
export type SupportStateId = "idle" | "triaging" | "decide" | "tooling" | "human" | "done" | "budget_out";

/** The chart, typed: pass it to `spawn` or `virtual`. */
export const supportChart: ChartSpec<SupportEvent, SupportContext, SupportStateId> = {
  format: "scxml",
  type: "urn:vertep:chart:sha256:b0b8e9574ca25b8572269bf25a2d4e199f7db5dc6b47bd0574a9d662ec2d2462",
};

/** The virtual actor of this chart with `key`, typed. */
export function createSupportActor(system: ActorSystem, key: string): ActorRef<SupportEvent, SupportContext, SupportStateId> {
  return system.virtual(supportChart, key);
}

vt certify

Run the Lean checker and print the certificate

Usage: vt certify <CHART>

Arguments:
  <CHART>  The chart file

Options:
  -h, --help  Print help

certify asks the Lean model, not the Rust code, whether a chart is well-formed. vt projects the chart to RDF, writes the canonical N-Quads to a temporary file, and runs the Lean-compiled checker as vt-certify --chart <file.nq>. The checker reads the graph with its own RDF reader, recomputes the chart version, decides the Lean WellFormed predicate and, when it holds, prints a certificate as N-Triples.

The checker is a separate program. vt looks for it in the VT_CERTIFY environment variable first, then as vt-certify on PATH. Building it needs the Lean toolchain (install elan; the version is pinned in lean/vertep-lean/lean-toolchain). Without it, certify says how to build it:

vt certify examples/traffic-light/traffic-light.scxml; echo "exit $?"

vt certify: the Lean checker `vt-certify` is not installed.
Build it from the Lean model and put it on PATH, or point VT_CERTIFY at it:
  cd lean/vertep-lean && lake build && export VT_CERTIFY=$PWD/.lake/build/bin/vt-certify
No certificate was produced.
exit 1

With the checker built:

export VT_CERTIFY=$PWD/lean/vertep-lean/.lake/build/bin/vt-certify
vt certify examples/traffic-light/traffic-light.scxml

<urn:vertep:chart:sha256:46431c540d155bee9016c61ee7a8f734890a92342ed9f91188aea25a602f5731> <https://w3id.org/vertep/vt#certifiedBy> <urn:vertep:cert:sha256:f9ce05505e1b9b6783c7566d05cc8cabf7140e680d99da4025cc884aeb18a632> .
<urn:vertep:cert:sha256:f9ce05505e1b9b6783c7566d05cc8cabf7140e680d99da4025cc884aeb18a632> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://w3id.org/vertep/vt#Certificate> .
<urn:vertep:cert:sha256:f9ce05505e1b9b6783c7566d05cc8cabf7140e680d99da4025cc884aeb18a632> <https://w3id.org/vertep/vt#theorem> "Vertep.checkWF_iff" .
<urn:vertep:cert:sha256:f9ce05505e1b9b6783c7566d05cc8cabf7140e680d99da4025cc884aeb18a632> <https://w3id.org/vertep/vt#theorem> "Vertep.violations_eq_nil_iff" .
<urn:vertep:cert:sha256:f9ce05505e1b9b6783c7566d05cc8cabf7140e680d99da4025cc884aeb18a632> <https://w3id.org/vertep/vt#theorem> "Vertep.Rdf.fromRDF_sound" .
<urn:vertep:cert:sha256:f9ce05505e1b9b6783c7566d05cc8cabf7140e680d99da4025cc884aeb18a632> <https://w3id.org/vertep/vt#theorem> "Vertep.step_deterministic" .
<urn:vertep:cert:sha256:f9ce05505e1b9b6783c7566d05cc8cabf7140e680d99da4025cc884aeb18a632> <https://w3id.org/vertep/vt#theorem> "Vertep.transition_selection" .
<urn:vertep:cert:sha256:f9ce05505e1b9b6783c7566d05cc8cabf7140e680d99da4025cc884aeb18a632> <https://w3id.org/vertep/vt#theorem> "Vertep.step_requests_declared" .
<urn:vertep:cert:sha256:f9ce05505e1b9b6783c7566d05cc8cabf7140e680d99da4025cc884aeb18a632> <https://w3id.org/vertep/vt#leanToolchain> "leanprover/lean4:v4.35.0" .
<urn:vertep:cert:sha256:f9ce05505e1b9b6783c7566d05cc8cabf7140e680d99da4025cc884aeb18a632> <https://w3id.org/vertep/vt#leanRdfRevision> "b407b97424150fec25a1ade514c71ea7abc61b42" .
<urn:vertep:cert:sha256:f9ce05505e1b9b6783c7566d05cc8cabf7140e680d99da4025cc884aeb18a632> <https://w3id.org/vertep/vt#checkerHash> "sha256:0d7f7bd4fcd09ba11157f1090afff34b79f9d86ab0f3b6443454eb9c309d988d" .

The certificate hangs off the chart version IRI with vt:certifiedBy. It names the theorems it relies on, the Lean toolchain, the LeanRDF revision and the hash of the checker binary, so anyone can rebuild the same checker and check the claim. Because certificates sit outside the chart's projection, attaching one never changes the chart's version.

The checker's exit codes follow vt's: 1 when the chart is not well-formed, 2 when the graph is not the projection of a chart.

vt certify crates/vertep-scxml/tests/corpus/all_elements.scxml; echo "exit $?"

<urn:vertep:chart:sha256:949a45ea97433907f548d026509517254b3a25aab6edf582ff3e3e725d7b6504> is not well-formed; violated rules: state rules (r2)
exit 1

$ vt certify crates/vertep-dm-rust/tests/charts/order.scxml
<urn:vertep:chart:sha256:05bdae901f2ef328f81ad649674bac2beab559eac46bae2dbc34db1bdcd2e38f> <https://w3id.org/vertep/vt#certifiedBy> <urn:vertep:cert:sha256:b9adf42734b3ce2e71ac4d6a6cd87569d41aee090031360b377534e298d9665e> .
<urn:vertep:cert:sha256:b9adf427…> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://w3id.org/vertep/vt#Certificate> .
<urn:vertep:cert:sha256:b9adf427…> <https://w3id.org/vertep/vt#theorem> "Vertep.checkWF_iff" .
…  (trimmed: five more theorems, the toolchain, the LeanRDF revision and the checker hash)

vt cluster reshard

Cluster operations

Usage: vt cluster <COMMAND>

Commands:
  reshard  Double the shard count of a stopped cluster (offline)
  help     Print this message or the help of the given subcommand(s)

Options:
  -h, --help  Print help

Double the shard count of a stopped cluster (offline)

Usage: vt cluster reshard <DIR> <OUT>

Arguments:
  <DIR>  The cluster data directory: `cluster.meta`, the shard files and `leases`
  <OUT>  Where to write the resharded files and metadata

Options:
  -h, --help  Print help

A cluster places actors by hashing their IRI to one of a fixed number of shards (see Cluster and federation). Changing that number moves actors between shards, so it is done offline, and only by doubling. reshard reads DIR:

• cluster.meta: key = value lines for cluster, shard_count, hash_version and replication_factor;
• the tiramemsu shard files, named shard-0000-of-0004.db and so on;
• leases: the leases still live, one <node> <shard> <epoch> line each, dumped from the lease authority before you start. An absent or empty file means no node holds a lease.

It refuses while any lease is live and names the nodes that hold them. Otherwise it writes twice as many shard files and the new metadata to OUT, copies every actor's journal to the shard its IRI now hashes to, and checks each copied journal against the original. Your original files stay where they are, so rolling back means keeping DIR.

The run below uses a four-shard cluster directory made for this page, with no actors in it, and a leases file left over from two running nodes:

cat data/cluster.meta
cat data/leases
vt cluster reshard data data-8; echo "exit $?"

cluster = prod
shard_count = 4
hash_version = 1
replication_factor = 1
node-b 1 7
node-a 0 3
resharding refused: the cluster is running, nodes node-a, node-b still hold shard leases
exit 1

Nothing is written to data-8. Once the nodes are stopped and the lease dump is empty:

rm data/leases
vt cluster reshard data data-8; echo "exit $?"
ls data-8
cat data-8/cluster.meta

resharded 4 to 8 shards: 0 actors, 0 entries copied to data-8
exit 0
cluster.meta
shard-0000-of-0008.db
shard-0001-of-0008.db
shard-0002-of-0008.db
shard-0003-of-0008.db
shard-0004-of-0008.db
shard-0005-of-0008.db
shard-0006-of-0008.db
shard-0007-of-0008.db
cluster = prod
shard_count = 8
hash_version = 1
replication_factor = 1

The end-to-end test crates/vertep-cli/tests/reshard.rs runs the same command on a cluster of 40 actors and checks that each one's journal is in the shard it hashes to after doubling.

vt as a library

Every subcommand is also a function in the vertep_cli::commands module, which returns an Outcome holding standard output, standard error and the exit code. The runnable examples use it to compare recorded command output with the real one, so documented output that drifts fails the build. See the examples.