Labinetix

Living. Kept current and swept at every release.

An execution platform: define → analyze → compile → deploy → execute models on embedded control hardware, behind one stable ABI — one binary interface that does not move under the code already running on a device.

A control model — a filter, a state-space system, a supervisory rule — usually starts life on an engineer’s workstation and ends it as hand-written code on a controller, with nothing but a changelog connecting the two. Labinetix closes that gap. The model is written down once, as data. Everything that reaches the hardware is derived from that one description. And what the device actually did can be put side by side with what was predicted before it shipped.

What it is not

Not an operating system. On the controller, Labinetix is a shared library that an existing control runtime loads and calls. It runs inside that runtime’s cycle, on the schedule the runtime decides, and hands control back on time.

Not a modelling tool. Models come from wherever you already build them. Labinetix takes the description, not the tool.

Not a cloud service. Everything here runs on a workstation you own and on the controller in front of you.

The six stages

Everything the platform does is one of six verbs, and the command line has one subcommand per verb, so the tool grows leaves and never re-roots. The sixth is observe, and it is the one most tools leave out: what comes back off a device matters as much as what went out to it.

The loop closes: observe feeds back into analyze, and the comparison is done by the same code that made the prediction. “It behaves as designed” is a result, not an opinion.

What runs where

On the workstation live the tools: the definition store, the analyses, the compilers, the deployment planner, the reader for evidence that comes back. They may be as large and as convenient as they like.

On the device lives as little as possible: the numerical kernels, a thin runtime that calls them, and one small library at the boundary where the control runtime calls in. Nothing that exists only for a developer’s convenience is allowed near the hardware — and that is a rule the build refuses to let anyone break, not a habit someone has to remember.

What the platform holds to

Seven promises. They are the reason the rest can be trusted.

1. Nothing developer-only reaches the device. Code that ships to hardware cannot depend on code that exists only on a workstation.
2. The maths is separate, and pure. The numerical kernels have no operating system beneath them, no memory to allocate, no files to read and no knowledge of the platform calling them. That is why the same kernel can be exercised on a laptop and trusted on a controller.
3. Code that must trust the outside world is a short, named list. Where the platform has to accept memory it did not allocate, every such place is written down with its reason. There is no unlisted place that nobody remembers.
4. The parts that name things do not compute things. Numerics live in the kernels; the layer that gives values names and shapes does nothing but that.
5. The control loop holds no surprises. Everything that could take an unpredictable amount of time — parsing, validating, resolving, reserving memory — happens once at start-up. Inside the cycle there is arithmetic and nothing else.
6. What is generated is never edited. Files derived from a model definition are written by the generator and by nothing else, and every artifact refers to a definition by its content, never by a name that could quietly come to mean something different.
7. Facts learned from real hardware are not tidied away. A behaviour proven on a device — an interface layout, a system library version a controller pins us to, an activation sequence — changes only for a written-down reason, and only with another run on real hardware.

Where this stands today

Early, and this page says so plainly.

The source tree builds and its tests pass on every change. The command line exists and all six stages have their place in it; two of them, analyze and run, have no library behind them yet and say so when you invoke them instead of pretending. Model definitions, their generated views and the deployment planner are real and exercised. Several controller platforms are described in the platform library, and one of them has a committed record from a real device behind that description.

No release has been cut, and there is nothing to download yet.

Nothing anywhere in this documentation is written in the present tense unless it exists. A sentence that describes unbuilt capability as though it were running is treated as a bug and fixed like one.

Start here

• Getting started — about five minutes on your own machine: build the command line, read a model out of the definition store, read a target’s description, produce a deployment plan without touching a device, and hear the two unwired stages say so. Every command on that page is run automatically on every change to the platform, so it cannot describe a tool that does not exist.
• CLI reference — every command, option and argument, walked off the command line itself rather than written by hand.

Licence

Not yet declared.

Getting started

Executed by the tutorial harness. Every tagged command on this page runs on every pull request.

Executed. Every fenced command on this page is run by CI — the docs-tutorial step of the docs workflow (docs-lint L5) — in document order, in one shell session, on the host. A command that stops working turns the build red, so this page cannot describe a CLI that does not exist. Three kinds of block are not ordinary steps and say so in their fence: exec:expect-fail (the honest answer today is an error), exec:hardware (needs a real device; the harness reports it as skipped and never runs it in a pull request) and untagged fences, which are prose.

In about five minutes you build the one command surface of the platform, read a contract out of the contract store, read the target contract, produce a deployment plan without touching a device, and hear the two stages that are not wired yet say so. Nothing here cross-compiles and nothing here talks to hardware.

Before you start

A clone of this repository, git, and the Rust toolchain it pins. The pin is an exact compiler version, never stable, and it lives in a rust-toolchain.toml at the root of the clone; rustup reads that file, so rustup toolchain install in the clone gets you the exact compiler CI uses. Python 3.11+ if you also want to run the lints. No cross-compiler, no device, no credentials.

1. Build the CLI

CI sets REPO_ROOT to the checkout; on your machine it is your clone (export REPO_ROOT="$(pwd)" from the repository root). Everything below uses the binary this step builds.

cd "$REPO_ROOT"
cargo build -p labinetix
export PATH="$PWD/target/debug:$PATH"

labinetix is one crate in a workspace of many. Building the whole workspace needs two ordered pre-steps first (the C++ static archives, then libLxPlant.so) and the pinned zig; that is what just check and the ci workflow do, and this page deliberately does not.

2. The six stages

labinetix --help

Define, analyze, build, ship, run and observe models on embedded control hardware

Usage: labinetix <COMMAND>

Commands:
  define   Author, verify and release contracts in the CADB (`crates/studio/define-cli`)
  analyze  Predict on the host what `run` will do — goldens, simulation, the compliance check
  build    Turn the target contract into the inputs a cross build needs (`crates/studio/build-toolchains`)
  ship     Stage, activate and roll back artifacts on a target (`crates/studio/ship-deploy`)
  run      Execute a model on the target engine
  observe  Record what real hardware did — on-target runs, evidence with provenance (`crates/studio/observe-cli`)

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

The root is exactly the six stages of the spine, in spine order, and nothing else. Later work adds leaves under a stage; the six roots do not move. Four of them — define, build, ship and observe — call the studio crate that owns the stage as an ordinary in-process library call. Two of them, analyze and run, have their place in the tree and no library behind them yet; §5 and §7 show exactly what they do about that today.

3. define — the contract store

The contract store (the CADB) is the capabilities/ directory: one directory per capability, each with its authoring file, its generated views and a lockfile that pins every one of them by content hash. Every define leaf takes --repo-root, which defaults to the working directory, so from the repository root you point it at the store.

labinetix define list --repo-root capabilities

One tab-separated row per entity: type, id, contract version, ipo_id (- where the type has none), content hash, lockfile path. Tab-separated because the output is for a script as much as for you.

One entity in full:

labinetix define show interface/tutorial_adder --repo-root capabilities

The authoring file and every generated view — the C header, the Rust view, the validator — each pinned by its own hash. Nothing under a generated/ directory is ever hand-edited; the emitter writes it and the lockfile pins it.

That claim is checkable, and checking it is a leaf:

labinetix define verify --all --repo-root capabilities

verify recomputes every hash and compares it against the lockfiles. It writes nothing, prints nothing and exits zero: silence is the pass. A view edited by hand fails here, which is the whole point of the stage.

4. build — the target contract

build turns hardware/targets/*.toml into the inputs a cross build needs. It compiles nothing itself.

labinetix build target

validated 3 target(s): cepe, cpxe, host-linux

Called with no name it validates the whole contract and lists it. Called with one name it prints that entry — here the host, which is the only one this page uses:

labinetix build target host-linux

The CI level and the rest come from hardware/targets/host-linux.toml and from nowhere else: a build fact that is not in the contract does not exist. The triple is the one thing that file does not write down — host-linux names the machine in front of you, so its triple is resolved from the toolchain that is running, and the line above will say x86_64 or aarch64 depending on where you ran it. The two embedded entries in that list, cepe and cpxe, need the pinned zig and a CMake toolchain file, which is labinetix build cmake-toolchain and is out of scope here.

5. analyze — not wired yet

analyze is the host-side prediction stage: goldens, simulation, the compliance check. The subcommand exists and the crate that will back it exists, but that crate has no library target to call, so the stage refuses instead of pretending:

labinetix analyze

It exits non-zero and prints one line naming what will back it. That is deliberate: a stage with a place in the tree and nothing behind it is recorded, not stubbed.

6. ship — a deployment plan without a device

ship plan resolves a deployment offline. It opens no socket, so you can run it here:

labinetix ship plan \
  --manifest crates/studio/ship-deploy/tests/fixtures/manifests/valid-pair.json \
  --artifact-dir crates/studio/ship-deploy/tests/fixtures/artifacts \
  --site-profile crates/studio/ship-deploy/tests/fixtures/profiles/sites/example.site.toml \
  --platform-profile crates/studio/ship-deploy/profiles/platforms/cpxe.toml

The manifest, the artifacts and the site profile are the synthetic fixtures the ship tests use, so the plan is real and the plant is not. Read the output for two things: the compatible set — libExternalIPO.so and libLxPlant.so, the pair that is the product’s artifact, each with its hash and its deploy path — and the redaction. The address and the username come back as <redacted-addr:…> and <redacted-user:…>, which is why a plan is safe to paste into an issue.

Staging and activating that plan is the same command surface against a real target, and it is never run by a pull request:

labinetix ship stage --transport cpxe \
  --manifest "$MANIFEST" --artifact-dir "$ARTIFACTS" \
  --site-profile "$SITE_PROFILE" --platform-profile "$PLATFORM_PROFILE"
labinetix ship activate --transport cpxe --confirm-reboot \
  --manifest "$MANIFEST" --artifact-dir "$ARTIFACTS" \
  --site-profile "$SITE_PROFILE" --platform-profile "$PLATFORM_PROFILE"

Activation reboots the target, which is why it demands --confirm-reboot; labinetix ship rollback restores the pair that was there before. The address and the username live in the site profile, never on the command line, and the password never anywhere either — ship reads it from the environment or from a credential agent.

7. run — not wired yet

run is the device stage: the engine executing a model on the target. Like analyze, it has its root and no library behind it today:

labinetix run

8. observe — what the hardware actually did

observe records. It is the only stage whose output carries authority about a real target, and it needs the lab:

labinetix observe --help

One leaf, run: scenario → deploy → remote → compare → evidence. Against a real CPX-E it is a long command because every input is pinned explicitly — the scenario and the lockfile from the store, both manifests, both artifact directories, the exact SHA-256 of the test executable, and where the evidence goes:

labinetix observe run \
  --scenario-json "$SCENARIO_JSON" \
  --lock-json "$LOCK_JSON" \
  --lx-core-root "$LX_CORE_ROOT" \
  --plant-manifest "$PLANT_MANIFEST" \
  --plant-artifact-dir "$PLANT_ARTIFACTS" \
  --executable-manifest "$EXECUTABLE_MANIFEST" \
  --executable-artifact-dir "$EXECUTABLE_ARTIFACTS" \
  --executable-sha256 "$EXECUTABLE_SHA256" \
  --site-profile "$SITE_PROFILE" \
  --output-dir "$OUTPUT_DIR" \
  --transport cpxe --confirm-real-remote --confirm-plant --confirm-place

CI reports that block as skipped and moves on. That asymmetry is the design: analyze predicts on the host on every pull request, observe records on real hardware and produces the evidence a release is not a release without.

Where to go next

• The CLI reference on this site lists every command, subcommand and option of the surface this page walked through. It is walked off the command tree by the CLI itself and byte-compared against that tree on every pull request, so it cannot describe a flag that does not exist.
• just check runs, in workflow order, exactly what the two CI workflows run, and just build the three ordered build steps alone. Each check is its own recipe under the name CI reports it by — boundary-lint, cargo-fmt, cargo-clippy, cargo-build, cargo-test, kernels-no-std, generated-check, docs-tutorial and the rest — so a check that went red is a recipe you can run by that name.
• The layers, the six stages, the machine checks that hold them and the working rules a change has to satisfy are documented with the source, in the clone you started from, rather than on this site.

Generated by cli-reference. Never hand-edited; docs-lint L3 re-renders it and byte-compares.

CLI reference

Generated. Walked off the clap::Command tree by the CLI itself and byte-compared against this file on every pull request (docs-lint L3). The command tree is the only source of these pages: change the command, regenerate, never edit this file.

The root is exactly the six stages of the spine — define analyze build ship run observe — and later work adds leaves under a stage rather than a seventh root. Four stages call the studio crate that owns them as an in-process library call; two, analyze and run, have their place in the tree and no library behind them yet and say so when invoked. Hidden commands are tooling and are not listed here.

Commands

labinetix

Define, analyze, build, ship, run and observe models on embedded control hardware

Usage: labinetix <COMMAND>

Subcommands

Options

labinetix define

Author, verify and release contracts in the CADB (crates/studio/define-cli)

Usage: labinetix define <COMMAND>

Subcommands

Options

labinetix define sync

Regenerate views and lockfiles for one or more entities.

Emitter generation defaults SOURCE_DATE_EPOCH to 0 when unset.

Usage: labinetix define sync [OPTIONS] [SELECTOR]

Arguments

Options

labinetix define verify

Recompute hashes and compare against lockfiles without writing files

Usage: labinetix define verify [OPTIONS] [SELECTOR]

Arguments

Options

labinetix define reindex

Rebuild the aggregate store index contracts.lock.json from the entity lockfiles.

The index is a walk of the capability tree, so this runs no emitter and touches no entity. Placement is checked while walking: an entity that does not sit where its reference chain puts it fails here exactly as it fails verify (DESIGN.md D36).

Usage: labinetix define reindex [OPTIONS]

Options

labinetix define check

CI integrity gate: emitter drift, lockfile pins, references, and policy checks

Usage: labinetix define check [OPTIONS]

Options

labinetix define manifests

Schema-validate every capabilities/<id>/capability.toml in the store.

The manifest is the one hand-authored file in a capability directory, and its shape is fixed by crates/studio/define-cadb/schema/capability.schema.json: the three-rung status ladder, the language vocabulary, evidence.runs, no unknown key, and status = "supported" only with a committed evidence artefact (DESIGN.md D15 rule 1). That each claim is true of the tree is a different question, answered by contract-cli/tests/capability_manifest.rs.

Usage: labinetix define manifests [OPTIONS]

Options

labinetix define doctor

Preflight: every declared emitter is one this binary links; the aggregate lock parses.

An emitter is a linked crate named by a builtin: token, so there is nothing to probe and nothing to install (DESIGN.md D20, D40). For each adapters/<type>.toml that declares an [emitter], this asks the same resolver labinetix define sync dispatches on whether the declared token names an emitter this binary links and one that writes views for that contract type — so a token this accepts is a token sync can call. Then contracts.lock.json is read: a missing or unparseable aggregate lock fails.

emitter.version is reported, never compared for pass/fail. It records which emitter version wrote that type’s committed views, which need not be what the linked emitter would write today, so a stale number is printed with its repair — re-emit with labinetix define sync — instead of refusing the store (DESIGN.md D40 rule 5).

Intended for CI / local checks before full drift regen (labinetix define check).

Usage: labinetix define doctor [OPTIONS]

Options

labinetix define list

List every entity row in the aggregate lockfile (tab-separated, script-friendly).

Output format: one row per entity, columns separated by TAB: type, id, contract_version, content_hash, lock_path. Rows are sorted by type then id (as stored in contracts.lock.json).

Usage: labinetix define list [OPTIONS]

Options

labinetix define show

Show one entity’s aggregate row and key lockfile fields (tab-separated key/value lines).

Output format: one field per line as key<TAB>value. Includes aggregate index fields plus emitter, authoring, views, references, and source pins from the entity lockfile.

Usage: labinetix define show [OPTIONS] <SELECTOR>

Arguments

Options

labinetix define get

Resolve a generated view path for a consumer (fail-closed hash verify by default).

Prints the absolute (or repo-resolved) view path on success. With --verify-hash (documented happy path; verification is on unless --no-verify), recomputes the view byte hash and compares it to the entity lockfile — mismatch exits non-zero. --out <path> copies the verified bytes to the destination.

Usage: labinetix define get [OPTIONS] --view <VIEW> <SELECTOR>

Arguments

Options

labinetix define diff

Semantic IR diff between two git refs of an entity (diagnostic; not the release baseline)

Usage: labinetix define diff [OPTIONS] <SELECTOR> <REF_A> <REF_B>

Arguments

Options

labinetix define new

Scaffold a new entity: authoring skeleton, initial lockfile, aggregate row.

For an interface, --band is required and the ipo_id is allocated: the lowest id the band has never handed out, written into the authoring TOML and appended to ipo-allocations.toml as one change. An ipo_id is never chosen by hand and never reused (DESIGN.md D39).

Usage: labinetix define new [OPTIONS] <CONTRACT_TYPE> <ID>

Arguments

Options

labinetix define publish

Author happy path: sync → verify → classify → version → commit.

Classifies against the release baseline (latest namespaced tag, else first-release from 0.0.0). Proposes the minimum SemVer unless --set overrides. Emitter generation defaults SOURCE_DATE_EPOCH to 0 when unset.

--dry-run prints the plan and never mutates authoring, lockfiles, commits, or tags.

Usage: labinetix define publish [OPTIONS] <SELECTOR>

Arguments

Options

labinetix define tag

Tag the current authoring contract_version at HEAD (no SemVer bump).

Use for first cut / backfill when authoring already carries the intended version. Maintainer-only for --push.

Usage: labinetix define tag [OPTIONS] <SELECTOR>

Arguments

Options

labinetix define release

Declare a contract version, enforce the minimum SemVer bump, refresh lockfiles, and optionally tag.

Classifies the semantic IR diff since the last namespaced tag (<type>/<id>/vX.Y.Z) and refuses under-bumps. Updates contract_version in authoring and lockfiles via sync. Prefer labinetix define publish for the author happy path.

--dry-run prints the plan and never mutates. --no-commit still writes authoring/lockfiles (tests / power users); do not use it as a dry-run.

Tag gate: git tags are never created unless you pass --create-tag (maintainer-only). CI and just check do not invoke this command. Agents must not pass --create-tag or --push-tag without explicit maintainer instruction.

Usage: labinetix define release [OPTIONS] --set <SET> <SELECTOR>

Arguments

Options

labinetix analyze

Predict on the host what run will do — goldens, simulation, the compliance check.

Not wired yet. The stage has its place in the tree and no library behind it: it will be backed by crates/studio/analyze-host-smoke, which has no library target to call today, so this command exits non-zero and names that crate rather than pretending. Host-side prediction is slice 2’s declared hard point (DESIGN.md Q21).

Usage: labinetix analyze

Options

labinetix build

Turn the target contract into the inputs a cross build needs (crates/studio/build-toolchains)

Usage: labinetix build <COMMAND>

Subcommands

Options

labinetix build target

Validate hardware/targets/.toml and print one target.

With no TARGET_NAME this validates every target file and prints a summary.

Usage: labinetix build target [OPTIONS] [TARGET_NAME]

Arguments

Options

labinetix build cmake-toolchain

Generate a zig-cc CMake toolchain file from hardware/targets/.toml.

With -o this also writes the executable zig-cc / zig-c++ wrappers beside it.

Usage: labinetix build cmake-toolchain [OPTIONS] <TARGET_NAME>

Arguments

Options

labinetix build verify-profile

Validate hardware/targets/verify-profiles.toml and print one profile.

The default PROFILE_NAME is the profile marked default = true.

Usage: labinetix build verify-profile [OPTIONS] [PROFILE_NAME]

Arguments

Options

labinetix ship

Stage, activate and roll back artifacts on a target (crates/studio/ship-deploy)

Usage: labinetix ship [OPTIONS] [COMMAND]

Subcommands

Options

labinetix ship plan

Validate inputs and print a redacted offline deploy plan (no network)

Usage: labinetix ship plan [OPTIONS]

Options

labinetix ship stage

Upload + independently verify both libraries under unique staging names (live untouched)

Usage: labinetix ship stage [OPTIONS]

Options

labinetix ship activate

Install a staged pair to live paths, verify, reboot, reconnect, and post-boot verify (requires --confirm-reboot)

Usage: labinetix ship activate [OPTIONS] --transaction <TRANSACTION>

Options

labinetix ship rollback

Restore the captured prior pair, reboot, reconnect, and post-verify (requires --confirm-reboot)

Usage: labinetix ship rollback [OPTIONS] --transaction <TRANSACTION>

Options

labinetix ship place-executable

Place typed test_executable artifacts under /ffx/bin_dev (no reboot; requires --confirm).

Producer manifests may declare role = "test_executable" (additive field; bridge v0.3.0 plant manifests omit it — use a sidecar/overlay manifest). Destination defaults to /ffx/bin_dev/<basename> when deploy_path is empty. Never starts the binary.

Usage: labinetix ship place-executable [OPTIONS]

Options

labinetix run

Execute a model on the target engine.

Not wired yet. The engine (crates/device/engine-opc) runs on the device under its own supervisor and exposes no library target a host command can call, so this command exits non-zero and names it. What a real target did is read back through observe.

Usage: labinetix run

Options

labinetix observe

Record what real hardware did — on-target runs, evidence with provenance (crates/studio/observe-cli)

Usage: labinetix observe [COMMAND]

Subcommands

Options

labinetix observe run

Run software acceptance (scenario → deploy → remote → compare → evidence)

Usage: labinetix observe run [OPTIONS] --scenario-json <SCENARIO_JSON> --lock-json <LOCK_JSON> --lx-core-root <LX_CORE_ROOT> --plant-manifest <PLANT_MANIFEST> --plant-artifact-dir <PLANT_ARTIFACT_DIR> --executable-manifest <EXECUTABLE_MANIFEST> --executable-artifact-dir <EXECUTABLE_ARTIFACT_DIR> --executable-sha256 <EXECUTABLE_SHA256> --site-profile <SITE_PROFILE> --output-dir <OUTPUT_DIR>

Options

labinetix observe engine-run

Validate an OPC engine run record and file it as evidence

Usage: labinetix observe engine-run [OPTIONS] --record <RECORD>

Options