The Semaprax Handbook

Ernesto, the Semaprax mascot, guides you from one .spx file to a checked, tested project. This handbook matches Semaprax 0.9.0.

Semaprax is beta software. Syntax, protocols, and binary interfaces can change. Use it to experiment and prototype, not for production or safety-critical work.

Start here

1. Install Semaprax. It has a one-command installer and a Homebrew formula.
2. Write and run your first program.
3. Create a project with modules and tests.

Prefer to watch first? See the recorded walkthrough.

What Semaprax is

Semaprax is a systems language where people and AI agents work on the same program. You write .spx source. The compiler checks it and exposes a semantic graph of declarations, types, contracts, effects, and calls.

The whole loop in one example

module examples.meaning;

@id("math.add")
fn add(left: i64, right: i64) -> i64
    requires left >= 0
    requires right >= 0
    ensures result == left + right
{
    left + right
}

@id("app.main")
fn main() -> i64
    ensures result == 42
{
    add(19, 23)
}

semaprax fmt meaning.spx     # canonical layout
semaprax check meaning.spx   # types, contracts, effects, ownership
semaprax run meaning.spx     # prints 42

What do you want to do?

For implementation details, use the source map and the specifications in docs/.

Get help from the compiler

semaprax help                     # commands you need first
semaprax help all                 # every command
semaprax help language topics     # language topics, one at a time
semaprax help diagnostic SPX-T208 # the fix for one error code

Install

Install a published Semaprax release, then run a first project. You do not need to clone the repository, install Rust, or compile anything for this route, and you do not need a model account, API key, or editor extension.

Pick your download

The current published release is listed at github.com/wavect/semaprax/releases/latest. That address always moves to the newest release, so use it only to find out which version is current. The commands below name one exact tag, v0.8.0, so every download in a session comes from the same release.

Other hosts (Intel macOS, Linux on ARM, older Linux) have no v0.8.0 archive. Use Install from source there. Later releases are planned to target glibc 2.35, but v0.8.0 does not, so check the release notes of the version you pick.

GitHub also shows Source code (zip) and Source code (tar.gz) under every release. Those are automatically generated snapshots of the repository, not Semaprax programs you can run. Download the archive named in the table.

Each archive unpacks to a directory named after itself. It contains semaprax (the full build of the command-line tool), semapraxd (the daemon), LICENSE, README.md, a per-archive release-manifest.json, and a smoke/ program. On Windows the two programs are semaprax.exe and semapraxd.exe.

Homebrew (Apple Silicon macOS)

Apple Silicon only for now; Homebrew installs the same prebuilt archive, it does not compile Semaprax.

brew install wavect/tap/semaprax
semaprax --version

Upgrade and remove with Homebrew:

brew update
brew upgrade wavect/tap/semaprax
brew uninstall semaprax

Homebrew owns semaprax and semapraxd in its bin directory (/opt/homebrew/bin). If you also installed by hand or with the installer, the first semaprax on your PATH wins; check which with command -v semaprax and type -a semaprax. Homebrew never overwrites another manager’s files, so remove or reorder the other entry rather than expecting it to be replaced.

To install without Homebrew, use the archive steps below.

macOS and Linux

The steps below use the Apple Silicon archive. For Linux, replace the target with x86_64-unknown-linux-gnu and shasum -a 256 -c - with sha256sum -c -.

1. Download the one archive for your computer and the checksum list. Do not download the other platforms’ archives.

   TAG=v0.8.0
   TARGET=aarch64-apple-darwin
   BASE=https://github.com/wavect/semaprax/releases/download/$TAG
   curl -fLO "$BASE/semaprax-$TAG-$TARGET.tar.gz"
   curl -fLO "$BASE/SHA256SUMS"
   

2. Verify the archive you downloaded. SHA256SUMS lists every platform, so select only your archive’s line; checking the whole file would report the archives you did not download as missing.

   grep " semaprax-$TAG-$TARGET.tar.gz$" SHA256SUMS | shasum -a 256 -c -
   

   It must print semaprax-v0.8.0-aarch64-apple-darwin.tar.gz: OK. If it prints FAILED or nothing at all, delete the download and start again; do not unpack it.

3. Optional: verify who built it. A checksum only shows that the file matches the list published beside it. If you have the GitHub CLI, this also checks the publisher’s attestation:

   curl -fLO "$BASE/release-attestation-$TARGET.json"
   gh attestation verify "semaprax-$TAG-$TARGET.tar.gz" \
     --bundle "release-attestation-$TARGET.json" --repo wavect/semaprax
   

4. Unpack it somewhere permanent. This example uses ~/.local/opt.

   mkdir -p "$HOME/.local/opt"
   tar -xzf "semaprax-$TAG-$TARGET.tar.gz" -C "$HOME/.local/opt"
   ls "$HOME/.local/opt/semaprax-$TAG-$TARGET"
   

   You should see LICENSE, README.md, release-manifest.json, semaprax, semapraxd, and smoke. If you downloaded the archive in a web browser instead of with curl, macOS may refuse to open the unsigned program; the archives are not notarized, so verify the checksum first and then clear the download flag with xattr -dr com.apple.quarantine "$HOME/.local/opt/semaprax-$TAG-$TARGET".

5. Put that directory on your PATH. For the current terminal only:

   export PATH="$HOME/.local/opt/semaprax-$TAG-$TARGET:$PATH"
   

   To keep it for every new terminal, add the same line, with the tag and target written out, to your shell’s startup file, then open a new terminal:

   Shell	Add this line	To this file
   zsh (the macOS default)	export PATH="$HOME/.local/opt/semaprax-v0.8.0-aarch64-apple-darwin:$PATH"	~/.zshrc
   bash	the same export line	~/.bashrc (and ~/.bash_profile on macOS)
   fish	fish_add_path $HOME/.local/opt/semaprax-v0.8.0-aarch64-apple-darwin	run once; fish remembers it

   A new version unpacks to a new directory, so update this line when you upgrade.

Windows (PowerShell)

1. Download the archive and the checksum list, then verify only that archive. SHA256SUMS lists every platform, so select your archive’s line.

   $Tag = "v0.8.0"
   $Target = "x86_64-pc-windows-msvc"
   $Name = "semaprax-$Tag-$Target.zip"
   $Base = "https://github.com/wavect/semaprax/releases/download/$Tag"
   Invoke-WebRequest "$Base/$Name" -OutFile $Name
   Invoke-WebRequest "$Base/SHA256SUMS" -OutFile SHA256SUMS
   
   $Line = Get-Content SHA256SUMS | Where-Object { $_ -match "  $([regex]::Escape($Name))$" }
   $Expected = ($Line -split "\s+")[0]
   $Actual = (Get-FileHash $Name -Algorithm SHA256).Hash.ToLower()
   if (-not $Expected -or $Actual -ne $Expected) { throw "Checksum mismatch for $Name - do not unpack it" }
   "$Name : OK"
   

2. Optional publisher verification, if the GitHub CLI is installed:

   Invoke-WebRequest "$Base/release-attestation-$Target.json" -OutFile "release-attestation-$Target.json"
   gh attestation verify $Name --bundle "release-attestation-$Target.json" --repo wavect/semaprax
   

3. Unpack it somewhere permanent and add it to PATH:

   $Dest = "$env:LOCALAPPDATA\Programs\semaprax-manual"
   Expand-Archive $Name -DestinationPath $Dest
   $Bin = "$Dest\semaprax-$Tag-$Target"
   Get-ChildItem $Bin   # semaprax.exe and semapraxd.exe are here
   
   # This terminal:
   $env:Path = "$Bin;$env:Path"
   # Every new terminal (your user account only):
   $UserPath = [Environment]::GetEnvironmentVariable("Path", "User")
   if (($UserPath -split ";") -notcontains $Bin) {
     [Environment]::SetEnvironmentVariable("Path", "$UserPath;$Bin".TrimStart(";"), "User")
   }
   

   Windows only reads the saved Path when a terminal starts, so open a new PowerShell window to see it there.

Run your first project

From any directory, with nothing checked out:

semaprax --version
semaprax new first-semaprax
semaprax check first-semaprax/semaprax.toml
semaprax test first-semaprax/semaprax.toml
semaprax run first-semaprax/semaprax.toml

With the v0.8.0 macOS archive these print the version and commit, created calculator project first-semaprax, verified project first-semaprax (sha256:...), project tests passed, and finally 42. new needs a destination that does not exist yet. Continue with your first program or the first project.

semapraxd is the same release’s daemon. You do not start it for the steps in this handbook; keep it beside semaprax.

Fix “command not found”

• Open a new terminal, or run the current-terminal export or $env:Path line from the step above.
• Check which executable your shell finds: command -v semaprax on macOS and Linux, Get-Command semaprax in PowerShell. If it is not the one you unpacked, an earlier directory on PATH is shadowing it.
• version 'GLIBC_2.39' not found on Linux means the host’s C library is older than the v0.8.0 build requires; use the source route below.

Install from source

Choose this to follow the latest main, to contribute, or when no archive fits your computer. It needs Git and Rust/Cargo 1.88 or newer. Clang is needed only when you build native executables, and Node.js 22 or newer only for the web-package tooling. The checker and interpreter path needs neither Clang nor Node.js, and nothing here needs an API key.

git --version
rustc --version
cargo --version

Clone the repository and run the starter example without installing anything:

git clone --branch main https://github.com/wavect/semaprax.git
cd semaprax
cargo run --locked -p semaprax -- check examples/meaning.spx
cargo run --locked -p semaprax -- run examples/meaning.spx

check reports a verified file and run prints 42. The -- separates Cargo’s options from Semaprax’s. Cargo downloads dependencies and compiles on the first run.

To get the short semaprax command, install from the checkout. Each command installs different programs:

A release archive’s semaprax is the full build, the same code as semaprax-full, renamed when packaged. A source-installed semaprax is the standalone build, which has fewer commands; the technical install reference lists the difference. Use semaprax-full from source when a chapter needs a command the standalone build lacks.

Cargo installs into ~/.cargo/bin. If semaprax is not found afterwards, add it for the current terminal:

export PATH="$HOME/.cargo/bin:$PATH"

$env:Path = "$env:USERPROFILE\.cargo\bin;$env:Path"

To reproduce the exact source this edition of the handbook was reviewed against, run the following in a clean clone before installing, and create a branch before you develop:

git switch --detach 508b851a5fda25002ec27453bb559755a6a0d930

Latest main can contain features that no published release has yet. A command absent from semaprax help all may need a newer build or the full toolchain.

Find help for your build

semaprax help run
semaprax help build
semaprax help diagnostic SPX-T208

Use the help of the executable you installed rather than guessing a flag.

Next: Write your first program, or configure VS Code.

See Semaprax in action

You will see a file checked and run, queried by meaning, and a project tested and built for the web. Run the commands from a repository checkout, or copy the examples from the examples folder. Install first.

The animation and still image replay recorded output from an earlier release (v0.6.0). The commands below are unchanged.

Check and run a file

semaprax check examples/meaning.spx
semaprax run examples/meaning.spx

check prints a source revision. run prints 42.

Ask what the compiler knows

semaprax query examples/meaning.spx

function    math.add    fn add(left: i64, right: i64) -> i64
function    app.main    fn main() -> i64

query lists declarations by stable ID. Other views:

Agent workflow explains when to use each.

Test a project and build for the web

semaprax test examples/calculator-project/semaprax.toml
semaprax build examples/calculator-project/semaprax.toml \
  --target web -o target/handbook-demo-web

Results: project tests passed, then built project web package target/handbook-demo-web. The package holds app.wasm, JavaScript bindings, TypeScript declarations, and an export descriptor. The output directory must not exist yet; pick a new one when you rebuild.

With Node.js 22 or newer, call an export by stable ID:

node --input-type=module <<'JS'
import { readFile } from 'node:fs/promises';
import { instantiateBytes } from './target/handbook-demo-web/semaprax.bindings.js';

const runtime = await instantiateBytes(
  await readFile('target/handbook-demo-web/app.wasm')
);
console.log(runtime.call('calculator.add', 19n, 23n));
JS

{ ok: true, value: 42n }

The n marks a JavaScript BigInt, used for i64. The result reports failure as data instead of throwing.

Next

Write your first program, or scaffold a project.

First program

You will write one file, format it, check it, and run it. Install first, then work in an empty directory.

1. Save hello.spx

module app.hello;

@id("app.main")
fn main() -> i64
{
    42
}

The name main is for people. The ID app.main is for tools. For a single-file run, Semaprax uses fn main.

2. Format, check, run

semaprax fmt hello.spx
semaprax check hello.spx
semaprax run hello.spx

42

semaprax fmt hello.spx --check reports formatting drift and leaves the file alone. The printed 42 is the return value, not the process exit status.

3. Change it

Replace 42 with 6 * 7 and run the three commands again. The result is the same. A tail expression is the last expression in a block; its value is the block’s result. There is no return here.

4. Write text

Printing is an effect, so the module must permit it and the function must declare uses. Save this as hello-print.spx:

module app.print_greeting;

permit { process.stdout.write }

@id("app.main")
fn main() -> i64
    uses { process.stdout.write }
{
    let greeting = "Hello, Semaprax!\n";
    let view = string_as_str(greeting);
    let written = stdout_write(str_as_bytes(view));
    if written == 17usize { 0 } else { 1 }
}

semaprax run hello-print.spx

Hello, Semaprax!
0

stdout_write prints the text and returns the byte count (17, including the newline). The runner then prints the return value, 0. string_as_str and str_as_bytes borrow the text; Ownership explains them.

When a command fails

Read the first diagnostic and its help: line, fix that, and run check again. Each SPX- code has a stable fix page:

semaprax help diagnostic SPX-T208
semaprax help language topics

See Debugging for more.

Next: Create a project.

First project

You will create a three-module calculator project, run its checks and tests, build it for the web, and break one test on purpose. The project’s semaprax.toml is its manifest: it lists the modules, tests, and exports.

1. Create it

semaprax new first-semaprax
cd first-semaprax

The destination must not exist. Add --name <project-name> to override the name, or --template library or --template service for another starter.

first-semaprax/
├── semaprax.toml
├── README.md
├── AGENTS.md
└── src/
    ├── app.spx
    ├── core.spx
    └── tests.spx

2. Run it

Run these inside first-semaprax/:

semaprax fmt . --check
semaprax check .
semaprax test .
semaprax run .

verified project first-semaprax (sha256:...)
project tests passed
42

fmt . --check prints nothing when every file is canonical. Every command also accepts semaprax.toml instead of ..

3. Read the files

schema = "semaprax.manifest.v1"

[package]
name = "first-semaprax"
version = "0.1.0"

[modules]
entry = "first_semaprax.app"
sources = ["src/app.spx", "src/core.spx", "src/tests.spx"]
tests = ["first_semaprax.tests"]

[exports]
web = ["first-semaprax.add"]

module first_semaprax.core;

@id("first-semaprax.add")
fn add(left: i64, right: i64) -> i64
{
    left + right
}

src/app.spx imports add by stable ID and calls it:

module first_semaprax.app;
use function @id("first-semaprax.add") from first_semaprax.core as add;

@id("first-semaprax.app.main")
fn main() -> i64
{
    add(19, 23)
}

module first_semaprax.tests;

@id("first-semaprax.tests.main")
fn main() -> i64
{
    if 19 + 23 == 42 { 0 } else { 1 }
}

Three names do three jobs:

use function @id("...") from <module> as <name>; imports by stable ID. See Modules and imports.

4. Inspect and build

semaprax query . --kind function

src/app.spx	function	first-semaprax.app.main	fn main() -> i64
src/core.spx	function	first-semaprax.add	fn add(left: i64, right: i64) -> i64
src/tests.spx	function	first-semaprax.tests.main	fn main() -> i64

semaprax build . --target web -o dist/web

The [exports] table in the manifest picks which functions the web package exposes (first-semaprax.add). Building does not start a server. The output directory must not exist yet. See Targets.

5. Break a test

Open src/tests.spx and change 19 + 23 == 42 to 19 + 23 == 41. Run semaprax test . and read the failure. Restore the line and run it again.

To add named cases, write fn test_<name>() -> i64 functions with an @id that return 0 on success. See Testing.

Add a module

1. Create src/<name>.spx with module first_semaprax.<name>;.
2. Add its path to sources in semaprax.toml. List a test module under tests.
3. Run semaprax check .. Check the whole project, not a single file: a lone file that imports another module reports SPX-G172 or SPX-T105.

When the manifest is rejected

Semaprax accepts one canonical manifest layout. Keep the generated table order, one-line arrays, and blank lines, and follow the first SPX-J100 hint. The manifest guide lists every field.

semaprax project-scaffold --name <name> prints a starter as one JSON capsule without writing files. It is for tools; use new to create a project.

Next: Language essentials, or write your own modules.

Set up VS Code

You will connect VS Code to your compiler, see diagnostics when you save a .spx file, and find the commands for navigation and review. The extension is wavect.semaprax. Its README has the full command list.

1. Install a compiler

Install Semaprax first. The extension never downloads or runs a compiler by itself.

2. Select the compiler

1. Open the command palette and run SEMAPRAX: Configure Compiler. Clicking the SEMAPRAX status bar item does the same.
2. Choose Select installed compiler… and pick the semaprax executable.

The list also shows compilers it found in per-user install folders, Homebrew’s folders, and on your PATH. Listing one does not run it. Other choices: Re-check current compiler and Open installation guide.

After you pick a file, the extension runs version --json and help all once to confirm it is Semaprax, then saves the absolute path in your user settings. A failed check or a cancel changes nothing.

The status bar item shows the state:

To set the path by hand, use user settings (not workspace settings, which cannot choose the compiler):

{
  "semaprax.compilerPath": "/absolute/path/to/semaprax"
}

3. Check a file

Save an .spx file and read the Problems panel. Or run SEMAPRAX: Check Project. This needs only the compiler: no manifest, policy, or session.

If a feature is missing, hover the status item. Features follow your compiler’s help all list, so an older compiler offers fewer commands.

4. Navigate by meaning

Save files before you use results that depend on a revision. If the source changed, refresh the session instead of trusting an old location.

5. Review changes in a saved-source session

A session ties the editor to a manifest and a host policy (the file that says what your machine permits). Set both in user settings:

{
  "semaprax.compilerPath": "/absolute/path/to/semaprax",
  "semaprax.manifestPath": "/absolute/project/semaprax.toml",
  "semaprax.hostPolicyPath": "/absolute/path/to/host-policy.json"
}

An empty {} is not a valid policy. The format is in the technical guide. Sessions need a compiler that advertises serve-workspace-mcp.

Then:

1. Start Saved-Source Session, then Open Candidate. A candidate is a proposed revision, held in memory.
2. Select Stable Target ID, then Show Target Change Catalog.
3. Apply Active Typed Intent. A typed intent is a structured edit, not free text.
4. Preview Candidate Source Diff, then Run Candidate Interpreter Tests.

For unfinished code, use the typed-hole commands (Open Typed Hole, New Hole Fill Scratch, Fill Selected Hole from Active Scratch). They show the hole’s context and checked fills for its type.

For a rejected change, Show Compiler-Admitted Repair Catalog lists exact fixes.

Hot reload (opt-in)

Start Hot Reload runs semaprax dev for the interpreter in a trusted local workspace. It checks each change, activates valid code between invocations, and keeps the last good version when a change is invalid. Native and Wasm swapping are not supported.

What the extension does not do

Build, commit, approval, publication, package installation, and native execution stay outside the extension. Finish those with your normal workflow after you review the diff.

Next: Inspect a project visually, or guide a coding agent.

Essentials

After this page you can write a complete Semaprax program: functions, values, if, while, and match. Save each example as a .spx file and run it with semaprax run file.spx.

Write a program

module app.basics;

@id("basics.double")
fn double(value: i64) -> i64
{
    value * 2
}

@id("app.main")
fn main() -> i64
{
    double(21)
}

run prints 42, the value main returns. The rules:

• A file starts with one module dotted.name; line.
• Give every declaration an @id("dotted.name"). It is the declaration’s permanent identity. Without it, check warns SPX-S103, and renaming the function changes its identity.
• The entry point is exactly fn main() -> i64.
• A function body is statements followed by one final expression. That expression is the result. There is no return.
• To use a function from another file, a Project imports it by @id with use function @id("…") from module as name;. See Modules and imports.
• Run semaprax fmt file.spx to apply the one canonical layout. It keeps // comments.

Pick a type

These eight scalar types (everything except string) are Copy: using a value does not consume it. Text and bytes follow ownership rules, see Ownership.

Operators never mix types. If n is a usize, write n < 5usize, not n < 5 (SPX-T208). Write 5i32 when an i32 is expected, because 5 is an i64 (SPX-T232). Integer arithmetic is checked: overflow stops the program with a status such as addition overflow, never wraps.

module app.scalars;

@id("app.main")
fn main() -> i64
{
    let small = 1i32 + 2i32;
    let ratio = 1.5 * 2.0;
    let letter = 'a';
    if small == 3i32 && ratio > 2.5 && letter == 'a' && !(1 > 2) { 3 } else { 0 }
}

Use &&, ||, and ! for booleans. && and || run their right side only when needed, always left to right.

Bind a value

let count = 3; makes an immutable binding. let mut count = 3; lets you assign again with count = count + 1;. Parameters are immutable. There is no +=, and a second let with the same name is an error (SPX-T209).

To ignore a result, bind it to _: let _ = work(1);. A bare work(1); is a syntax error.

Choose a value with if

module app.branch;

@id("app.main")
fn main() -> i64
{
    let score = 42;
    let accepted = if score >= 40 { score } else { 0 };
    if accepted > 100 { 1 } else { if accepted > 10 { accepted } else { 2 } }
}

if is an expression and always has an else. Both branches have the same type. For a third case, nest an if inside the else block. There is no else if.

Repeat with while

module app.counting;

@id("app.main")
fn main() -> i64
{
    let mut next = 1;
    let mut total = 0;
    while next <= 3 {
        total = total + next;
        next = next + 1;
        next <= 3
    }
    total
}

The condition after while is checked before every pass. The body must end with an expression, and while throws its value away. Ending a body with an assignment is SPX-P203. There is no break or continue: put the exit test in the condition. See Loops for for and the loop limits.

Pick a case with match

module app.classification;

@id("app.main")
fn main() -> i64
{
    let value = -2;
    match value { 0 => 0, -1 | -2 => -9, n if n < 0 => -1, _ => 1, }
}

The first matching arm wins. | joins alternatives, if adds a guard, and _ matches anything. A match on numbers or chars needs a last arm without a guard (SPX-T257). Every arm ends with a comma, including the last. Matching variants is in Matching.

Mistakes to skip

When check fails, read the first error: its help: line is usually the fix. For a code, run semaprax help diagnostic SPX-T208.

Next: Types. Exact rules: RFC 0001.

Types: records, variants, Option, Result

After this page you can model your data with records (fields), variants (one of several cases), Option (maybe absent), and Result (value or error). Classes have their own page.

The examples on this page build records and variants. The default interpreter behind semaprax run does not admit those (SPX-F102), so run them with semaprax run file.spx --native, which compiles generated C11. check and fmt need no flag.

Group fields with a record

module app.data;

@id("data.point")
record Point {
    @id("data.point.x")
    x: i64,
    @id("data.point.y")
    y: i64,
}

@id("app.main")
fn main() -> i64
{
    let mut origin = Point { x: 1, y: 2 };
    origin.x = origin.x + 1;
    let moved = origin with { y: 10 };
    moved.x + moved.y
}

• A record literal names every field, in any order. A missing field is SPX-T213.
• origin.x = … changes a field and needs let mut.
• origin with { y: 10 } builds a new record and leaves origin unchanged.
• Give each field its own @id.
• Records have no methods: point.get() is SPX-T203. Call get(point).

Pick one case with a variant

module app.shapes;

@id("data.shape")
variant Shape {
    @id("data.shape.dot")
    Dot,
    @id("data.shape.box")
    Box {
        @id("data.shape.box.width")
        width: i64,
        @id("data.shape.box.height")
        height: i64,
    },
}

@id("data.area")
fn area(shape: Shape) -> i64
{
    match shape { Shape::Dot {} => 0, Shape::Box { width: w, height: h } => w * h, }
}

@id("app.main")
fn main() -> i64
{
    area(Shape::Box { width: 6, height: 7 })
}

A case without data is declared Dot, and written Shape::Dot {} everywhere else. A match must cover every case, so adding a case makes the compiler point at each match you must update. See Matching.

Handle missing values and errors

Option<T> has Some { value } and None {}. Result<T, E> has Ok { value } and Err { error }. Both are ordinary generic variants, so one spelling rule covers them:

Some(1) and bare None do not exist (SPX-T203, SPX-T202). Leaving off the type arguments when you build one is SPX-T221.

module app.checked;

@id("data.checked_div")
fn checked_div(left: i64, right: i64) -> Result<i64, i64>
{
    if right == 0 { Result<i64, i64>::Err { error: 1 } } else { Result<i64, i64>::Ok { value: left / right } }
}

@id("data.half_of_quotient")
fn half_of_quotient(left: i64, right: i64) -> Result<i64, i64>
{
    let quotient = checked_div(left, right)?;
    checked_div(quotient, 2)
}

@id("app.main")
fn main() -> i64
{
    match half_of_quotient(80, 2) { Result::Ok { value: v } => v, Result::Err { error: code } => code, }
}

expr? returns early with the error when expr is an Err. It works only in a function that itself returns a Result (SPX-T218 elsewhere), so main uses match.

An arm cannot build a record or variant (SPX-T258). Pull scalars out of the match, then build the value with if.

Make a type generic

module app.pair;

@id("data.pair")
record Pair<T> {
    @id("data.pair.first")
    first: T,
    @id("data.pair.second")
    second: T,
}

@id("data.swap")
fn swap(pair: Pair<i64>) -> Pair<i64>
{
    Pair<i64> { first: pair.second, second: pair.first }
}

@id("app.main")
fn main() -> i64
{
    let swapped = swap(Pair<i64> { first: 1, second: 2 });
    swapped.first + swapped.second
}

Write the type arguments when you construct a generic value. Generic functions are in Functions.

Choose the boundary before you move a helper

Standalone files accept any of these types in any function. A Project export is stricter: the default profile allows only Copy scalars in public signatures (SPX-G174). Records, variants, Option, and Result can still appear inside a function. Pick a profile before you move a helper to a project.

Return Option or Result instead of a sentinel value such as -1, so callers must handle each case.

Exact rules: RFC 0002.

Ownership, strings, bytes

After this page you can pass text and bytes between functions without ownership errors. The whole idea fits in one rule: passing an owned value moves it, and a borrow only reads it. Using a moved value is a compile-time error (SPX-O101), never a crash.

Why did SPX-O101 fail?

A string or Bytes value has one owner. Passing it to a function, or to string_concat, moves it. The second use below fails:

let s = string_concat("ab", "cd");
size(s) + size(s)        // error[SPX-O101]: use of resource `s` after ownership was moved

Fix it in one of three ways:

Copy scalars (i64, bool, char, and the rest) never move. They copy freely.

Borrow in helpers, own in sinks

module app.bytes;

permit { process.stdout.write }

@id("bytes.count_a")
fn count_a(text: borrow str) -> usize
{
    let view = str_as_bytes(text);
    let length = byte_len(view);
    let mut index = 0usize;
    let mut hits = 0usize;
    while index < length {
        hits = match byte_get(view, index) { Option::Some { value: byte } => if byte == 97u8 { hits + 1usize } else { hits }, Option::None {} => hits, };
        index = index + 1usize;
        index < length
    }
    hits
}

@id("app.main")
fn main() -> i64
    uses { process.stdout.write }
{
    let greeting = string_concat("banana", "!");
    let borrowed = string_as_str(greeting);
    let hits = count_a(borrowed);
    let written = stdout_write(str_as_bytes(borrowed));
    if hits == 3usize && written == 7usize && string_len(greeting) == 7 { 0 } else { 1 }
}

run prints banana! from stdout_write, then 0 from main.

• borrow T reads a value without taking it. Make it the default for helpers.
• own T takes the value. Use it for functions that finish with the value: builders, transfers, destructors.
• own is valid for Bytes, Vec, Box, iterators, and resources. A plain string parameter moves too. Writing own string is SPX-O002.

Convert text to bytes in steps

Text goes down a one-way ladder. Each step is a named call:

string            owned text: "hello", string_concat(a, b), string_from_i64(n)
   | string_as_str(binding)
   v
str (borrowed)    read-only view: pass it to `borrow str` parameters
   | str_as_bytes(view)
   v
Slice<u8>         borrowed bytes: byte_len, byte_get, byte_range, stdout_write

Every conversion takes a named binding, not a literal or a call result.

Going up: bytes_copy(view) makes an owned Bytes. array_as_slice(array) and bytes_as_slice(bytes) give a Slice<u8>. The type table is in Collections.

Build a byte buffer

Allocate with a literal capacity and chain bytes_set. Binding the result freezes it:

module app.buffer;

@id("app.main")
fn main() -> i64
{
    let buffer = bytes_set(bytes_set(bytes_zeroed(2usize), 0usize, 65u8), 1usize, 66u8);
    let view = bytes_as_slice(buffer);
    if byte_len(view) == 2usize { 0 } else { 1 }
}

To fill a buffer in a loop, allocate it outside, then assign the result back to the same let mut binding. This is the only way to re-open a buffer:

module app.buffer_loop;

@id("app.main")
fn main() -> i64
{
    let mut buffer = bytes_zeroed(3usize);
    let mut index = 0usize;
    let mut value = 65u8;
    while index < 3usize {
        buffer = bytes_set(buffer, index, value);
        index = index + 1usize;
        value = value + 1u8;
        0
    }
    let view = bytes_as_slice(buffer);
    if byte_len(view) == 3usize { 0 } else { 1 }
}

Limits: bytes_zeroed takes a usize literal capacity and cannot sit inside a loop (SPX-T267). A literal index past the capacity is SPX-T272. A computed index past the capacity fails at run time before anything is written. Do not hold a view across the reassignment (SPX-T265). You cannot re-open a named buffer any other way (SPX-T271).

Exact rules: RFC 0003, Owned String Borrowed View v1, Owned Bounded Byte Buffer v1.

Contracts and effects

After this page you can state what a function promises (requires, ensures) and what it touches (permit, uses). Both sit in the signature, the compiler checks both, and tools read them without reading the body.

Add a contract

module examples.meaning;

@id("math.add")
fn add(left: i64, right: i64) -> i64
    requires left >= 0
    requires right >= 0
    ensures result == left + right
{
    left + right
}

@id("app.main")
fn main() -> i64
    ensures result == 42
{
    add(19, 23)
}

• requires is what the caller must satisfy. ensures is what the function guarantees. result names the return value.
• Clauses go between the signature and the body. They are part of the function’s meaning, so changing one is a change to the interface.
• Contracts are checked at run time, on every backend. A violation stops the program and names the clause, the function, and the arguments:

SEMAPRAX contract failure
  contract: requires left >= 0 in math.add
  arguments: left = -1, right = 2

Start with bounds (value >= 0), exact results for small pure helpers (result == left + right), and non-empty results for builders.

Contract or Result?

Use requires for something the caller must already have checked. Use a Result for an outcome callers should expect, such as bad user input. A failed contract is a bug report, not control flow. To keep deliberate rejection checks out of the passing suite, see Testing. For a rule with its own identity and solver evidence, see Laws and proofs.

Declare effects

A function that performs an effect, or calls one that does, must say so. The module permits effects first, then each function lists the ones it uses:

module app.hello;

permit { process.stdout.write }

@id("app.main")
fn main() -> i64
    uses { process.stdout.write }
{
    let text = "hi";
    let view = string_as_str(text);
    let written = stdout_write(str_as_bytes(view));
    if written == 2usize { 0 } else { 1 }
}

run prints hi from stdout_write, then 0 from main.

A missing permit is SPX-E101. A missing uses is SPX-E102. Each message names both edits.

Effects pass up through callers. A function that calls an effectful function lists that effect too:

module app.ticking;

permit { audit.log }

@id("flow.tick")
fn tick(value: i64) -> i64
    uses { audit.log }
{
    value + 1
}

@id("app.main")
fn main() -> i64
    uses { audit.log }
{
    tick(41)
}

audit.log is a name you chose. Declaring an effect adds a visible requirement and nothing more. The compiler-owned operations need these exact names:

The operations are in Input and output. Installing the compiler grants no filesystem, process, network, or signing authority. A declared effect still needs a host that provides it. A test host can return fixed answers, and a configured runtime host does the real work. Check the profile before you move an effectful helper to a new target.

Single-file semaprax run evaluates declared effects only for process.stdout.write. Other declared effects stop with SPX-F102; add --native.

Mark an unsafe boundary

unsafe marks code that a reviewer must read. It adds no raw memory access. It needs a module permit { unsafe } and a one-line audit note on each block (SPX-N102, SPX-N103). The body is ordinary checked code:

module app.audited;

permit { unsafe }

@id("app.main")
fn main() -> i64
{
    let mut x = 1;
    @audit("bump the counter")
    unsafe {
        x = x + 3;
        x
    }
    x
}

Each boundary appears as a node in the semantic graph. Status: partial, see Unsafe Boundaries v1.

Resumable effects (preview)

A function can declare yields Request -> Response and yield one request at a time so a driver can answer it later. Only the interpreter engine and a Rust driver run this. Ordinary native and Wasm builds refuse it (SPX-B116, SPX-W126). Read Resumable Effects v1 before you use it.

Ask for contracts and effects

semaprax context examples/meaning.spx math.add --depth 1 --filters contracts
semaprax doc examples/meaning.spx

context returns one declaration’s neighborhood as bounded JSON. doc renders signatures, contracts, and effects as documentation. See Driving Semaprax from an AI agent.

Exact rules: RFC 0001.

Functions, generics, function values

After this page you can write generic functions, pass a function to another function, and capture a value in a closure.

Write a generic function

module app.identity;

@id("generic.identity")
fn identity<T>(value: T) -> T
{
    value
}

@id("app.main")
fn main() -> i64
{
    identity<i64>(41) + 1
}

Type parameters go in angle brackets after the name. At a call, write the type arguments: identity<i64>(41). The compiler can fill them in when the arguments decide them (identity(41) also works), but this is a private profile and not a promise for public signatures. If it cannot decide, you get an error that asks for them (SPX-T225). Always write them for vec_*, box_*, and iter_* calls (SPX-T281).

• A generic function cannot call itself, directly or through other generic functions (SPX-T226).
• Generic records and variants spell their arguments when you build one: Pair<i64> { first: 1, second: 2 }. See Types.
• Generic functions stay inside a module. Public Project signatures take Copy scalars only unless the project profile says more (Profiles).

Pass a function

A parameter of type fn(A) -> B takes a function. Pass a named function, or an unnamed fn literal, which is a function without its name and @id:

module app.callbacks;

@id("iterator.fold")
fn fold<T, A>(input: own Iter<T>, initial: A, combine: fn(A, T) -> A) -> A
{
    let mut accumulator = initial;
    for own item in input {
        accumulator = combine(accumulator, item);
        0
    }
    accumulator
}

@id("fn.twice")
fn twice(value: i64, step: fn(i64) -> i64) -> i64
{
    step(step(value))
}

@id("fn.inc")
fn inc(value: i64) -> i64
{
    value + 1
}

@id("app.main")
fn main() -> i64
{
    let input = vec_push<i64>(vec_push<i64>(vec_with_capacity<i64>(2usize), 5), 5);
    let total = fold<i64, i64>(vec_into_iter<i64>(input), 0, fn(acc: i64, value: i64) -> i64 { acc + value });
    twice(total, inc)
}

A function value has up to eight parameters. Its target must be a local, effect-free, non-generic function, or a literal. A literal takes no trailing comma. Bind one to a name to reuse it: let positive = fn(value: i64) -> bool { value > 0 };

Capture a value in a closure

A literal copies the Copy scalars it reads at the moment it is built. Later changes to the original do not reach the copy:

module app.snapshot;

@id("app.main")
fn main() -> i64
{
    let mut limit = 10;
    let within = fn(value: i64) -> bool { value < limit };
    limit = 0;
    if within(5) { 1 } else { 0 }
}

Closure bodies are ordinary scalar expressions and calls. A closure cannot change what it captured, cannot capture an effect, and cannot sit inside a generic collection position (SPX-T288). The Rust-style |x| x + 1 is SPX-P201.

Move one owned value into a callback

once fn captures one owned Bytes value and carries it in the type FnOnce() -> i64. Calling it consumes it, and so does passing it to an own parameter:

module affine.example;

@id("affine.consume")
fn consume(payload: own Bytes) -> i64
{
    42
}

@id("affine.make")
fn make() -> FnOnce() -> i64
{
    let payload = bytes_zeroed(4usize);
    once fn() -> i64 { consume(payload) }
}

@id("affine.run")
fn run(callback: own FnOnce() -> i64) -> i64
{
    callback()
}

@id("app.main")
fn main() -> i64
{
    let callback = make();
    run(callback)
}

The body is exactly one call that passes the captured buffer to a function fn target(payload: own Bytes) -> i64. Reusing the buffer or the callback after the move is SPX-O101. There are no other captures, parameters, or generics (SPX-T308).

The older own fn() -> i64 { target(payload) } form is in the same family. In 0.9.0, run executes it on all three backends, but check reports SPX-H006. Use once fn. Closures that borrow a borrow str parameter are a narrower profile, see Synchronous Borrowed Text Closures v1.

Pick a name or a literal

Use a named function when the logic has a meaning, a contract, or a second caller: it gets an @id, contracts, and tests. Keep a literal to one short expression.

Exact rules: Function Values v1, v2, Scalar Snapshot Closures, Generic and Loop Closures, Retained Affine Callback v1, Owning-Capture Closures v1.

Loops and iterators

After this page you can repeat work three ways: while for a counter or other scalar state, for to read a vector, and for own to drain an iterator.

Count with while

module app.factorial;

@id("loops.factorial")
fn factorial(value: i64) -> i64
    requires value >= 0
{
    let mut remaining = value;
    let mut total = 1;
    while remaining > 1 {
        total = total * remaining;
        remaining = remaining - 1;
        remaining > 1
    }
    total
}

@id("app.main")
fn main() -> i64
{
    factorial(3)
}

The result is 3 * 2 * 1 = 6. The rules:

• The condition is checked before every pass and must be a bool.
• The body ends with an expression. Its value is discarded, and the condition alone decides repetition. A body that ends after an assignment is SPX-P203.
• There is no break or continue.
• A body may use Copy scalars, calls that return scalars, and the byte_get/Option<u8> pattern. Building a record or variant, or calling a function that returns one, is SPX-T252. Loop over scalars, then build the value after the loop.
• net_recv returns an owned value and is not allowed in a body (SPX-T270). bytes_zeroed stays outside. The one buffer write a body may do is buffer = bytes_set(buffer, index, value), see Ownership.

Visit a vector with for

module app.traverse;

@id("app.main")
fn main() -> i64
{
    let values = vec_push<i64>(vec_push<i64>(vec_with_capacity<i64>(2usize), 20), 22);
    let mut total = 0;
    for item in values {
        total = total + item;
        0
    }
    total
}

for item in values visits the elements of a Vec<T> binding in index order. T is one of the eight Copy scalars. The length is read once, the vector is frozen inside the body, and the body’s value is discarded. The vector must be an immutable binding (SPX-T284 for let mut) and a plain name, not a call. Do not move or change it, or the item, inside the body. Build the vector first with the Vec calls.

Drain an iterator with for own

vec_into_iter<T> moves a vector into an Iter<T>. for own consumes it:

module app.consume;

@id("app.main")
fn main() -> i64
{
    let input = vec_push<i64>(vec_push<i64>(vec_with_capacity<i64>(2usize), 20), 22);
    let iterator = vec_into_iter<i64>(input);
    let mut total = 0;
    for own item in iterator {
        total = total + item;
        0
    }
    total
}

After the loop, input and iterator are both moved. Using either is SPX-O101.

Step by hand

iter_next<T> consumes an iterator and returns an IterStep<T>: Done {} or Yield { item, rest }. Take it apart with match own. item is a Copy value and rest owns the remaining iterator. Pass rest to the next step, or let it go out of scope:

module app.step;

@id("lazy.first_if_step")
fn first_if_step<T>(step: own IterStep<T>, keep: fn(T) -> bool) -> bool
{
    match own step { IterStep::Done {} => false, IterStep::Yield { item, rest } => keep(item), }
}

@id("app.main")
fn main() -> i64
{
    let input = vec_push<i64>(vec_with_capacity<i64>(1usize), 7);
    let found = first_if_step<i64>(iter_next<i64>(vec_into_iter<i64>(input)), fn(value: i64) -> bool { value > 0 });
    if found { 0 } else { 1 }
}

Map, filter, and fold

There is no built-in map. You write these helpers once, as generic functions over for own, and reuse them. Each call spells its type arguments:

module app.pipeline;

@id("iterator.map")
fn map<T, U>(input: own Iter<T>, capacity: usize, transform: fn(T) -> U) -> Vec<U>
{
    let mut output = vec_with_capacity<U>(capacity);
    for own item in input {
        output = vec_push<U>(output, transform(item));
        0
    }
    output
}

@id("iterator.filter")
fn filter<T>(input: own Iter<T>, capacity: usize, keep: fn(T) -> bool) -> Vec<T>
{
    let mut output = vec_with_capacity<T>(capacity);
    for own item in input {
        if keep(item) { output = vec_push<T>(output, item); 0 } else { 0 }
    }
    output
}

@id("iterator.fold")
fn fold<T, A>(input: own Iter<T>, initial: A, combine: fn(A, T) -> A) -> A
{
    let mut accumulator = initial;
    for own item in input {
        accumulator = combine(accumulator, item);
        0
    }
    accumulator
}

@id("app.main")
fn main() -> i64
{
    let input = vec_push<i64>(vec_push<i64>(vec_push<i64>(vec_with_capacity<i64>(3usize), -1), 2), 3);
    let mapped = map<i64, bool>(vec_into_iter<i64>(input), 3usize, fn(value: i64) -> bool { value > 0 });
    let filtered = filter<bool>(vec_into_iter<bool>(mapped), 3usize, fn(value: bool) -> bool { value });
    let count = fold<bool, usize>(vec_into_iter<bool>(filtered), 0usize, fn(count: usize, value: bool) -> usize { if value { count + 1usize } else { count } });
    if count == 2usize { 1 } else { 0 }
}

Elements are the eight Copy scalars and Bytes. Owned items, public iterator signatures, and adapters that build another vector are outside the profile. The lazy adapters, which do their work as the iterator is consumed, are in examples/lazy-iterator-adapters.spx. Run it from a repository checkout:

semaprax run examples/lazy-iterator-adapters.spx

Exact rules: While Loops v1, Vec For Traversal v1, Owning Iterators v1, Owning Iterator Loops v1, Generic Iterator Operations v1, Lazy Iterator Adapters v1.

Collections: Vec, Box, arrays, bytes

After this page you can pick the right container and use it: Vec for lists of scalars, Box for one boxed scalar, [u8; N] for a small fixed byte block, and Bytes for a byte buffer you build.

Every call spells its element type, such as vec_push<i64>. T is one of the eight Copy scalars: i64, i32, u8, usize, char, f32, f64, bool. All capacities are bounded.

Build and read a vector

module app.stats;

@id("stats.sum")
fn sum(readings: borrow Vec<i64>) -> i64
{
    let length = vec_len<i64>(readings);
    let mut position = 0usize;
    let mut total = 0;
    while position < length {
        total = total + vec_get<i64>(readings, position);
        position = position + 1usize;
        position < length
    }
    total
}

@id("app.main")
fn main() -> i64
{
    let mut building = vec_with_capacity<i64>(3usize);
    building = vec_push<i64>(building, 2);
    building = vec_push<i64>(building, 3);
    building = vec_push<i64>(building, 0);
    let readings = building;
    sum(readings)
}

Mutators take the vector and return the next one, so you always assign the result back: building = vec_push<i64>(building, 2);. Build with let mut, then move the finished vector into an immutable binding to traverse it.

Pushing past the capacity stops the program (semaprax.vec.v1 status 1, “vec_push beyond capacity”), and so does an index past the length (status 2, “vector index out of bounds”). Reserve enough room first. A for loop avoids the index bookkeeping: see Loops.

In a Project, Vec needs the owned-data-api.v1 profile and std.collections = "^0.1.0". See Profiles.

Keep a scalar in a Box

module app.boxed;

@id("app.main")
fn main() -> i64
{
    let boxed = box_new<i64>(7);
    let peek = box_get<i64>(boxed);
    box_into_inner<i64>(boxed)
}

box_new<T> makes a uniquely owned Box<T>. box_get<T> copies the value out through a borrow. box_into_inner<T> consumes the box. These three names select the compiler’s box. A record you declare yourself as record Box<T> is an ordinary inline record. The box holds one Copy scalar only, with no shared ownership. See Owned Bounded Box v1.

Use a fixed byte array

[97u8, 98u8] has type [u8; 2]. An array literal holds bytes only. A list of i64 is a Vec<i64>, not [1, 2, 3] (SPX-T262). There is no a[0] (SPX-P106). Borrow a view and read with byte_get, which returns an Option<u8> so you handle the missing case:

module app.lookup;

@id("app.main")
fn main() -> i64
{
    let sample = [97u8, 98u8];
    let view = array_as_slice(sample);
    match byte_get(view, 0usize) { Option::Some { value: b } => if b == 97u8 { 0 } else { 1 }, Option::None {} => 2, }
}

Bytes, slices, and strings

A slice is a view. It borrows and never owns. Each conversion takes a named let binding, not a literal or a call result.

Work with text

== compares string contents. These names are reserved: declaring your own string_len is SPX-S113. The full signatures are in Built-in functions.

Exact rules: Owned Bounded Vec v1, v2, String Operations v1, Portable Indexed Byte Data v1.

Classes and inheritance

After this page you can attach methods to data with a class, extend a class with a subclass, and bind a protocol to a record. Classes are the only values that answer value.method() calls.

Use a record and free functions by default. Use a class when the methods belong to the value, such as a counter or a builder.

The examples on this page build records and classes, so run them with semaprax run file.spx --native. check needs no flag.

Add methods

module example.counter;

@id("example.counter")
class Counter {
    @id("example.counter.value")
    value: i64,

    @id("example.counter.get")
    fn get(self: Counter) -> i64
{
        self.value
    }

    @id("example.counter.bumped")
    fn bumped(self: Counter, amount: i64) -> Counter
{
        Counter { value: self.value + amount }
    }
}

@id("app.main")
fn main() -> i64
{
    let base = Counter { value: 40 };
    let next = base.bumped(2);
    if next.value == 42 && base.get() == 40 { next.value } else { 0 }
}

• The first parameter is self: Counter, written out.
• A method usually returns a changed copy. base stays at 40.
• A class literal names every field. A field changes with counter.value = … on a let mut binding.
• Records have no methods: point.get() is SPX-T203. Calling a method on a number or string is the same error: use string_len(s).

Extend a class

module example.inheritance;

@id("example.animal")
class Animal {
    @id("example.animal.legs")
    legs: i64,

    @id("example.animal.speak")
    fn speak(self: Animal) -> i64
{
        self.legs
    }
}

@id("example.dog")
class Dog : Animal {
    @id("example.dog.bark_count")
    bark_count: i64,

    @id("example.dog.speak")
    fn speak(self: Dog) -> i64
{
        super.speak() + self.bark_count
    }
}

@id("example.main")
fn main() -> i64
{
    let d = Dog { legs: 4, bark_count: 2 };
    let a: Animal = d;
    if d.speak() == 6 && a.speak() == 4 { d.speak() } else { 0 }
}

• class Dog : Animal inherits the fields and methods of Animal. A Dog literal names all fields, inherited ones too.
• super.speak() calls the parent’s method.
• A Dog is an Animal: let a: Animal = d; converts it, and calls through a use the parent’s methods.
• A method with the same name overrides the parent’s for the subclass.

Keep the tree shallow. Every extra level adds fields to every literal. To reuse behavior without substituting types, hold the other value in a field.

Bind a protocol to a record

A protocol lists the functions a type must have. An impl binds each one to a function you already wrote, by @id. The compiler checks that every required function is bound exactly once. The binding is checked and then erased: it adds no dispatch, no protocol value, and no runtime cost.

module geometry.app;

@id("geometry.read-x")
protocol ReadX {
    @id("geometry.read-x.get")
    fn get(self: Self) -> i64;
}

@id("geometry.point")
record Point {
    @id("geometry.point.x")
    x: i64,
}

@id("geometry.point.read-x")
impl "geometry.read-x" for "geometry.point" {
    "geometry.read-x.get" = "geometry.point.get";
}

@id("geometry.point.get")
fn get(point: Point) -> i64
{
    point.x
}

@id("app.main")
fn main() -> i64
{
    get(Point { x: 7 })
}

The receiver must be a local record with an @id. Bound functions are top-level, non-generic, and not main. Projects import protocols with use protocol @id("…") from module as name;.

Exact rules: Class Inheritance v1, Static Protocol Conformance v1.

Matching

After this page you can pick a result with match on numbers, bytes, chars, and variants. Arms are tried in order and the first match wins.

Match numbers, bytes, and chars

module app.sign;

@id("refutable.sign_class")
fn sign_class(value: i64) -> i64
{
    match value { 0 => 0, -1 | -2 => -9, n if n < 0 => -1, n => 1, }
}

@id("app.main")
fn main() -> i64
{
    sign_class(-2)
}

• The last arm must be _ or a binding without a guard. Otherwise you get SPX-T257.
• Order matters. Put specific arms first. In the example, -2 is caught by the alternatives before the guard sees it.
• Chars and bytes work the same way, with their own literals:

module app.route;

@id("refutable.digit_name")
fn digit_name(digit: u8) -> i64
{
    match digit { 0u8 => 10, 9u8 => 90, k if k > 4u8 => 2, _ => 1, }
}

@id("refutable.route")
fn route(code: char) -> i64
{
    match code { 'a' => 1, 'b' | 'c' => 2, _ => 3, }
}

@id("app.main")
fn main() -> i64
{
    digit_name(4u8) + route('c') + digit_name(0u8)
}

A range such as 0..=5 is not a pattern. Use a guard.

Match a variant

Name the case and bind each payload field as field: name. Building a generic variant spells its type arguments. Matching one does not:

module app.pick;

@id("data.first_positive")
fn first_positive(left: i64, right: i64) -> Option<i64>
{
    if left > 0 { Option<i64>::Some { value: left } } else { if right > 0 { Option<i64>::Some { value: right } } else { Option<i64>::None {} } }
}

@id("app.main")
fn main() -> i64
{
    match first_positive(0, 4) { Option::Some { value: v } => v, Option::None {} => 0, }
}

• A case without data is matched as Shape::Dot {}, never bare Dot.
• A match over a variant must cover every case. Add a case and the compiler lists each match to update.
• Some(v) is not a pattern. Write Option::Some { value: v }.
• Arms produce numbers, bools, and calls, not new records or variants (SPX-T258). Match out the scalars first, then build the value with if.
• A missing comma between arms is a syntax error. The last arm needs a comma.
• if let does not exist. Use match.

Matching a call result in main needs semaprax run file.spx --native. The default interpreter reports SPX-F102.

Match an owned value

match own moves the value into the arms. Use it for IterStep from iter_next:

match own step { IterStep::Done {} => false, IterStep::Yield { item, rest } => keep(item), }

Yield gives a Copy item and the owning rest. The full example is in Loops.

Keep arms short

Match where a value arrives, then work with plain scalars. If an arm needs its own match, move it into a named function with its own @id.

Exact rules: Refutable Match v1, RFC 0002.

Input and output

After this page you can print, read arguments and input, touch files, and open a network connection from Semaprax, and you will know what each one needs. Every operation needs three things: the module permits the effect, the function declares it, and the host running the program provides it.

Print a number

module app.print_count;

permit { process.stdout.write }

@id("app.main")
fn main() -> i64
    uses { process.stdout.write }
{
    let count = 42usize;
    let text = string_from_usize(count);
    let view = string_as_str(text);
    let written = stdout_write(str_as_bytes(view));
    if written == 2usize { 0 } else { 1 }
}

run prints 42 from stdout_write, then 0, the value main returns. stdout_write returns the number of bytes written, so compare it and fail loudly on a short write. Use string_from_i64 for signed values.

Read arguments and standard input

module spxgrep_lines.app;

permit { process.args.read, process.stdin.read }

@id("spxgrep-lines.run")
fn run() -> bool
    uses { process.args.read, process.stdin.read }
{
    if args_len() == 1usize {
        let needle = arg_utf8(0usize);
        let data = stdin_read();
        let input = bytes_as_slice(data);
        byte_len(input) > 0usize
    } else {
        false
    }
}

@id("main")
fn main() -> i64
{
    0
}

stdout_append and stderr_append take the same borrow Slice<u8> and return the bytes accepted. They add to the output instead of writing once, so a line command can print many times. All appends share one 65,536-byte budget and appear only when the command ends with a settled result. They belong to the line-command-io.v1 profile.

Bind stdin_read() to a name before you borrow it: bytes_as_slice(stdin_read()) is SPX-T266. A single-file run supports only process.stdout.write. The others need a Project with the useful-data-command.v1 profile built for the native target. See Profiles.

Read and write files

module app.load;

permit { fs.read }

@id("load.size")
fn size() -> usize
    uses { fs.read }
{
    let path = [100u8, 97u8, 116u8, 97u8];
    let bytes = file_read(array_as_slice(path), 4usize, 64usize);
    let view = bytes_as_slice(bytes);
    byte_len(view)
}

@id("app.main")
fn main() -> i64
{
    0
}

Paths are bounded, relative byte strings (here data), resolved under a root the host injects. There is no absolute path and no ambient filesystem. file_write_new creates a new file and never overwrites. file_write_atomic replaces one atomically. Only stat and list accept an empty path for the root. The std.fs package builds typed Path and reader/writer values on top. See Standard library.

Know whether a write landed

file_write_atomic aborts the command when something fails. file_write_atomic_checked returns a classified code instead: 0 published, 1 not published (the target is untouched), 2 uncertain (the replace started and the host cannot say whether it finished). Check for uncertain before you retry. It needs fs.write and the private filesystem-io.v3 profile, so use it through std.fs.write_atomic_checked, which returns a WriteOutcome:

module save.app;

use type @id("std.fs.write-outcome") from std.fs as WriteOutcome;
use type @id("std.io.writer") from std.io as Writer;
use type @id("std.path.value.path") from std.path.value as Path;
use function @id("std.fs.write-atomic-checked") from std.fs as fs_write_atomic_checked;
use function @id("std.io.writer.from-bytes") from std.io as writer_from_bytes;
use function @id("std.io.writer.write-u8") from std.io as writer_write_u8;
use function @id("std.path.value.from-bytes") from std.path.value as path_from_bytes;

permit { fs.write }

@id("save.app.run")
fn run() -> bool
    uses { fs.write }
{
    let name = [110u8, 111u8, 116u8, 101u8];
    let path = path_from_bytes(bytes_copy(array_as_slice(name)));
    let w0 = writer_from_bytes(bytes_zeroed(2usize));
    let w1 = writer_write_u8(w0, 111u8);
    let w2 = writer_write_u8(w1, 107u8);
    match fs_write_atomic_checked(path, w2) { WriteOutcome::Published {} => true, WriteOutcome::NotPublished {} => false, WriteOutcome::Uncertain {} => false, }
}

@id("save.app.main")
fn main() -> i64
{
    0
}

The project around it sets profile = "filesystem-io.v3", [capabilities] required = ["fs.read", "fs.write"], and depends on std.fs, std.io and std.path.value. Its test module needs its own main. This project passes semaprax check and semaprax test. Spec: Host operation outcome v1.

Connect over TCP

module net_http_get.app;

permit { network.connect, network.read, network.write }

@id("net-http-get.fetch")
fn fetch() -> bool
    uses { network.connect, network.read, network.write }
{
    let host = [101u8, 120u8, 97u8, 109u8, 112u8, 108u8, 101u8, 46u8, 111u8, 114u8, 103u8];
    let handle = net_connect(array_as_slice(host), 80usize);
    let sent = net_send(handle, array_as_slice(host));
    let closed = net_close(handle);
    sent == 11usize && closed == 0usize
}

@id("app.main")
fn main() -> i64
{
    0
}

Calls run only through an injected provider, so tests can use a fixed one. net_recv returns an owned value and is not allowed inside a while body (SPX-T270): receive first, then inspect the bytes in the loop.

TLS and listeners

Five more calls open encrypted connections and accept inbound ones:

The call checks the server name and the host owns the certificates; there is no cleartext fallback and no implicit bind address. Handles share the same 8-slot space as net_connect. These calls run only on the interpreter through a hosted provider. Native and Wasm builds reject them before emission, and network-run fixtures (v2) replay them with tls: true and a listeners queue. Spec: Bounded Network Services v1.

HTTPS in one call

https_get(url, max) and https_post(url, body, max) return the whole response as owned bytes, shaped like an HTTP/1.1 message, so the std.http parsers read it. Each needs network.http and the https-command-io.v1 profile. This function checks and builds:

module https_status.app;

permit { network.http }

@id("https-status.fetch")
fn fetch() -> usize
    uses { network.http }
{
    let url = [104u8, 116u8, 116u8, 112u8, 115u8, 58u8, 47u8, 47u8, 101u8, 120u8, 97u8, 109u8, 112u8, 108u8, 101u8, 46u8, 111u8, 114u8, 103u8];
    let reply = https_get(array_as_slice(url), 4096usize);
    byte_len(bytes_as_slice(reply))
}

@id("app.main")
fn main() -> i64
{
    0
}

The URL is HTTPS only, at most 2,048 bytes, with no credentials or fragment. max is 1 to 65,536 and counts the headers. https_post sends a body of up to 65,536 bytes as application/octet-stream, follows no redirects, and only reaches origins the host allow-lists (at most eight). A failure aborts the command and leaves no partial response, and a POST error does not prove the server did nothing, so do not retry blindly. Test against recorded replies with semaprax network-run. Start from examples/https-project.

Wire a standard-library package

The packages std.fs and std.http supply typed values and parsers over these calls. Three steps: depend on the package, set its profile, import by stable id, as in the std.fs example above. Use semaprax help library to list the exact signatures; for example semaprax help library std.fs.read.

Narrow the effects

Declare only the effects a function needs. A tool that prints should not permit the network, and reviewers and the semantic graph both see the difference. Convert I/O bytes to views at the edge, scan them with byte_get and byte_range, and build owned results at the end.

Exact rules: Bounded Language Command I/O v1, Filesystem I/O v1 and v2, Bounded Language Network I/O v1, HTTPS Client I/O v2.

Resources and cleanup

After this page you can declare a value with a defined end of life, a resource, and describe a state machine with a session protocol. The compiler proves that every owned resource is settled exactly once on every exit path. There is no leak, no double free, and no finalizer that fails halfway.

Declare a resource

module buffer.app;

@id("buffer.type")
resource Buffer {
    @id("buffer.type.drop")
    drop trivial;
}

@id("buffer.inspect")
fn inspect(buffer: borrow Buffer) -> i64
{
    1
}

@id("buffer.consume")
fn consume(buffer: own Buffer) -> i64
{
    inspect(buffer)
}

@id("buffer.pipeline")
fn pipeline(buffer: own Buffer) -> i64
    ensures result == 2
{
    inspect(buffer) + consume(buffer)
}

@id("app.main")
fn main() -> i64
{
    0
}

pipeline borrows first (inspect), then transfers (consume). A borrow never changes ownership. The final own transfer settles the value. Using buffer after consume(buffer) is SPX-O101, the same error as for a moved string, see Ownership.

A single-file semaprax run rejects modules that declare resources (SPX-B104). Verify them with check, and run them through a Project’s native or Wasm build or with run file.spx --native.

Choose how a resource ends

An imported finalizer is declared in an interface that states its effect, its failure mode, and the value it consumes:

module platform.app;

@id("platform.token")
resource Token {
    @id("platform.token.drop")
    drop import "platform.token.finalize";
}

@id("platform.token.host")
interface TokenHost
    permits { platform.token.release }
{
    @id("platform.token.finalize")
    import fn finalize(token: own Token) -> unit
        effects { platform.token.release }
        failure infallible
        consumes token always;
}

@id("app.main")
fn main() -> i64
{
    0
}

A finalizer that runs automatically must be infallible and must consume the token. A teardown that can fail is an explicit close function that returns a status for the caller to handle. A destructor never reports an error.

Cleanup runs in a fixed order set by the cleanup plan, once for each owned resource that was not transferred, on every exit. Failure selection is sticky: cleanup cannot replace the status that was already selected.

semaprax context examples/ownership.spx buffer.pipeline --depth 1 --filters ownership

context --filters ownership lists each parameter as own or borrow and where each loan starts and ends.

Describe a state machine

A session protocol names states and the moves between them. It is checked and then erased: native and Wasm output do not change, and it grants no authority.

module app.checkout;

@id("checkout.session")
session protocol "checkout-v1" {
    states { Idle, Open, Committed, Failed }
    initial Idle;
    terminal Committed cleanup {}
    terminal Failed cleanup {}
    on Idle begin: send BeginRequest via "checkout.begin" -> Open;
    on Idle abort: fail Unit -> Failed;
    on Open commit: send CommitRequest via "checkout.commit" -> choice { committed: Committed, refused: Failed };
    on Open lost: fail Unit -> Failed;
}

@id("checkout.begin")
fn begin() -> i64
{
    1
}

@id("checkout.commit")
fn commit() -> i64
{
    2
}

@id("app.main")
fn main() -> i64
{
    0
}

• states lists the states and initial picks the start.
• Each terminal state names its cleanup, and a terminal has no moves out.
• on <state> <label>: <kind> <Payload> … -> <state> is one move. The kind is send, receive, call, return, cancel, timeout, or fail. Use choice { label: state, … } for several outcomes.
• via "<function-id>" ties a move to a function in the same module by @id (SPX-K104).
• Every non-terminal state needs a cancel, timeout, or fail exit. Violations are SPX-K101 to SPX-K106.

A function can opt in with follows session protocol to have its call order checked (SPX-K107 to SPX-K109). Status: local evidence, see Session Protocol Types v1.

Borrow, then own

Helpers borrow. Only sinks, builders, and close own. Structure a consuming function as a borrow phase followed by one transfer.

Exact rules: RFC 0003, Shared Loan Plan v1.

Laws and proofs

After this page you can write a law, which is a rule with its own stable @id, select it in a Project, and list it. A contract describes one function call. A law names a rule so a project can keep it while the code changes, for example during a refactor or an agent-proposed edit.

Write a law

A law lives in a law module, not in a standalone program. The committed examples/native-law-project selects this one:

module native_law.laws;

@id("native-law.add.right-nonnegative")
law contract "native-law.add" requires (right: i64)
    right >= 0
    evidence theorem_proved;

@id("native-law.order.total")
law relational (left: i64, right: i64)
    left <= right || right < left
    evidence smt_proved;

The rule is a pure scalar expression: literals, the variables, and operators. Calls, fields, records, branches, and quantifiers are refused. The evidence kinds are runtime_guarded, compiler_proved, model_checked, smt_proved, and theorem_proved.

Declaring a law records the rule and the evidence it needs. It does not prove anything. Checking a project admits the law and leaves its row open until evidence arrives.

Select the law module

The Project manifest is semaprax.manifest.v2. List the file in both sources and law_sources:

[modules]
entry = "native_law.app"
sources = ["src/LAWS.spx", "src/app.spx", "src/core.spx", "src/tests.spx"]
law_sources = ["src/LAWS.spx"]
tests = ["native_law.tests"]

LAWS.spx is only a naming habit. The explicit law_sources entry is what selects it. See the example manifest.

List the laws

From a repository checkout:

semaprax check examples/native-law-project
semaprax query examples/native-law-project --kind law --json
semaprax project-assurance-manifest examples/native-law-project/semaprax.toml

The query returns both law IDs above. The assurance manifest lists the project’s obligations and the evidence for each. Keep it with the source revision it describes.

More law shapes live in examples/law-packs/ (collection, finite retry, architecture, foreign boundary, money state).

Words you will see

Check a law with an installed solver

project-proof-check runs one selected tool against one law or one function postcondition. It takes an absolute manifest path, the tool, its executable and exact version line, and a host profile. Start with its help:

semaprax help project-proof-check

Replace the angle-bracket values in this template. Do not paste it as is:

semaprax project-proof-check <absolute-manifest> --tool z3 --executable <absolute-z3-path> --version-line <exact-version-line> --host-profile trusted-local --law native-law.order.total

trusted-local means you trust local tool execution. A solver somewhere on PATH does not replace naming the executable and its version. Add --workflow summary or --workflow detail for the strict-law review route. Witness values are hidden unless you pass --show-witness-values.

Keep the rule while you repair the code

When a proof fails, read the subject, the assumptions, and the reported reason. A run-time guard, a test result, and a solver proof answer different questions, so keep the evidence class with the verdict.

The protected-law workflow keeps an independent baseline. A repair changes the implementation and is then checked again. Removing a law, loosening a precondition, or changing the selected set is a specification change and needs its own approval. Cached proof work is reused only when it matches the current source and tool, so an old report never stands in for a new check.

Next: Source map. References: Native Law Declarations v1, Law Set v1, Protected Law Intent v1.

Modules and imports

Split a program into modules: reusable logic in one, main in another, tests in a third. After this page you can build, test and run a three-module project by hand.

Want a ready-made layout instead? Run semaprax new <dir> (see Manifests). To follow along, create a tutorial/ directory with a src/ subdirectory and save each block at its stated path.

1. Describe the project

Save this as tutorial/semaprax.toml:

schema = "semaprax.manifest.v1"

[package]
name = "handbook-demo"
version = "0.1.0"

[modules]
entry = "tutorial.app"
sources = ["src/app.spx", "src/core.spx", "src/tests.spx"]
tests = ["tutorial.tests"]

[exports]
web = ["tutorial.add"]

entry is the module with main. sources lists the files. [exports] web lists the functions a web build exposes, by stable ID.

2. Write the reusable function

Save this as tutorial/src/core.spx:

module tutorial.core;

@id("tutorial.add")
fn add(left: i64, right: i64) -> i64
    requires left >= 0
    requires right >= 0
    ensures result == left + right
{
    left + right
}

This module has no main: it only provides add. Check it through the project, not alone (a single file without main fails with SPX-T105).

3. Import it into the entry module

Save this as tutorial/src/app.spx:

module tutorial.app;
use function @id("tutorial.add") from tutorial.core as add;

@id("tutorial.main")
fn main() -> i64
{
    add(19, 23)
}

Read the import as a sentence: use the function with ID tutorial.add from module tutorial.core, and call it add here. An import names a stable ID, not a file path. Imports come right after the module line, before any permit block.

4. Add tests

Save this as tutorial/src/tests.spx:

module tutorial.tests;
use function @id("tutorial.add") from tutorial.core as add;

@id("tutorial.tests.add")
fn test_add() -> i64
{
    if add(19, 23) == 42 { 0 } else { 1 }
}

@id("tutorial.tests.zero")
fn test_zero() -> i64
{
    if add(0, 0) == 0 { 0 } else { 1 }
}

@id("tutorial.tests.main")
fn main() -> i64
{
    0
}

Each test_* function returns 0 to pass. The manifest’s tests entry tells the runner which module to read. See Testing.

5. Run the project

From inside tutorial/:

semaprax fmt .
semaprax check .
semaprax test .
semaprax run .
semaprax query . --id tutorial.add

test prints project tests passed, run prints 42, and query prints the tutorial.add declaration. A directory operand (.) selects its semaprax.toml.

Keep names and paths separate

src/core.spx          file containing source
    tutorial.core     module declared by that file
        tutorial.add  persistent identity of one function
            add       local name used at a call site

A display rename keeps tutorial.add. Moving a file means updating the manifest path. Renaming a module means updating its imports. Three separate edits, which is why the ID is the stable handle.

Fix common mistakes

Use a standard-library module

Declare the package, then import from it:

semaprax add . std.num "^0.1.0"     # adds one [dependencies] row
semaprax help library std.num       # signatures and stable IDs

add edits only the manifest. Bundled std.* packages are version 0.1.0 and need no download. See the standard library.

Next: Choose a profile for richer data, or learn how the test runner reports failures.

Project manifests

semaprax.toml says which files make up a project, where it starts, which modules hold tests, and what it exports. After this page you can read, edit and add to a manifest without breaking it.

Start from a template

semaprax new my-app                        # calculator (default)
semaprax new my-lib --template library
semaprax new my-svc --template service

new creates the directory, a semaprax.toml, sources, tests, a README.md and an AGENTS.md. It never writes into an existing path. Names are lowercase ([a-z][a-z0-9-]*, SPX-J115 otherwise).

semaprax project-scaffold --name <n> [--template ...] [--layout frozen|tables] prints the same project as one JSON capsule for tools instead of writing files.

Read a manifest

schema = "semaprax.manifest.v1"

[package]
name = "calculator"
version = "0.1.0"

[modules]
entry = "calculator.app"
sources = ["src/app.spx", "src/core.spx", "src/tests.spx"]
tests = ["calculator.tests"]

[exports]
web = ["calculator.add"]

[dependencies]
std.num = "^0.1.0"

A filename is not a module name, and a module name is not a declaration ID. See Modules.

Edit a manifest safely

The loader accepts one canonical byte layout. Keep the table order, one blank line between tables, one-line arrays, and no comments.

New source file: add its path to sources. New test module: add it to sources and tests. A file in src/ is not part of the project until listed.

semaprax fmt . --check       # also reports manifest drift
semaprax add . std.num "^0.1.0"   # appends one [dependencies] row

add edits only the manifest. It fetches nothing. Next steps are in Shipping.

Three kinds of version

A spec named PROJECT-MANIFEST-V18.md describes one project profile. It does not mean you change your manifest schema.

Add laws

Native law files need schema = "semaprax.manifest.v2" and [modules] law_sources. A law file also appears in sources. See Laws and proofs and the native-law example.

Recognize the older frozen layout

Committed examples may use schema = "semaprax.project.v1" (or v2 to v13) with flat keys such as entry, sources, web_exports, tests. Each frozen schema equals one profile of the table layout. Keep its key order. For new projects use semaprax new. add and [dependencies] need the table layout (SPX-J127 otherwise).

Next: Choose a profile, then build a target. References: Package Manifest v1, v2, Project Dependencies v1.

Choose a project profile

A profile fixes which values may cross a function boundary, who owns them, and which targets can build the project. After this page you can pick the profile for your interface and fix SPX-G174.

Pick by interface

A function’s boundary is its parameters and result. Locals inside a function can use records and variants even when the boundary is a single i64.

These profiles are private. They exist for the bundled std packages, have no public ABI and no web exports, and may change. Do not rely on them:

https-command-io.v1 is not in that list. It adds network.http for https_get and https_post, and examples/https-project builds on it (Input and output).

Every row is one bounded contract. A profile name is not a switch you flip on an existing project: change one type, then run check, test and your consumer.

Why did SPX-G174 fire?

A function crosses the boundary with a type the profile does not admit. Read the named signature, then pick one:

1. Keep it private: remove it from [exports].
2. Return a scalar: add a small wrapper.
3. Move the project to a profile that admits the type.

SPX-G174 has more than one cause, so read the whole message.

Scalar boundary (the default)

Parameters and results are Copy scalars (i64, bool, u8, f64, …). The scalar profile builds to web, native and oci (and rust with the full toolchain).

Owned data

An owned boundary says who keeps the bytes and who frees them. A borrowed input stays owned by the caller. An owned input or output has a defined transfer and cleanup. Pick it when JavaScript or Rust calls your code with buffers. The npm target needs a profile that admits it (the scalar profile fails with SPX-W120). Start from the frame-payload project and its web or Rust consumer.

Command I/O

A command profile has a [command] entry point and a fixed [capabilities] required list, so the project declares exactly the authority it uses. The input value is fixed per profile: stdin-bytes+one-utf8-arg.v1 for useful-data-command.v2, argv-utf8+stdin-bytes.v1 for the four -io.v1 profiles.

• semaprax run <project> runs the ordinary project entry, not the command.
• semaprax network-run <project> --fixture f.json [--arg UTF8]... [--stdin path] runs a network-command-io.v1 command against a recorded fixture (semaprax.network-fixture.v1, at most 1 MiB and 8 connections). No real socket opens.
• Build the command with build --target native; see Targets.

See Input and output for the source operations.

Check before you change

1. Which input and output types cross the boundary?
2. Who owns each non-Copy value before and after the call?
3. Which target and host supply external operations?
4. Which committed example covers that combination?

Build that example first, then change one thing at a time.

Next: Integrate with Rust, C or a browser. References: Package Manifest v1 (profile table), Public Owned Data API v1, Public Flat Owned Record API v1, Public Owned UTF-8 API v1, Bounded Language Network I/O v1.

Targets: interpreter, native, web

You can run a program in the interpreter, build it to a native executable, or build it to a WebAssembly package. After this page you can pick one and fix the usual failures.

One checked meaning feeds every target. A safe program behaves the same on each backend that admits the features it uses.

Run it

semaprax check examples/meaning.spx
semaprax run examples/meaning.spx          # interpreter, prints 42
semaprax run examples/meaning.spx --native # generated C11, needs Clang
semaprax run .                             # a project: runs its entry

The interpreter is bounded: --max-steps N limits work, --max-bytes N limits the output envelope, and call depth stops at 256 frames. --json gives a machine-readable result. A single file needs a fn main() -> i64 (SPX-T105 otherwise). If the interpreter refuses a program (SPX-F102), try --native.

Build it

semaprax build examples/meaning.spx --target native -o meaning-native
semaprax build . --target web -o dist/web

Rules that save time:

• -o and --output are the same. The path must be new: an existing one fails with SPX-I307, a bad parent with SPX-I301.
• --json reports status, target, product and output.
• [targets] matrix in the manifest can forbid a target (SPX-J122). web, wasm and npm need wasm32; the rest need native64.
• Run semaprax help build for the exact list on your binary.

Strings in a standalone web module

A source file that passes string values between its own functions needs the internal String profile. Name each exported function:

semaprax build app.spx --target web --profile internal-strings-v1 \
  --export app.length -o app-web

It needs a source file, --target web or wasm, and 1 to 32 --export ids. A project, another target or a missing export is a usage error (exit 2). Strings never cross the exported boundary. Spec: Standalone internal String Web package v1.

Check a web package

semaprax test examples/calculator-project
semaprax build examples/calculator-project --target web -o dist/calculator-web
node scripts/verify-wasm-scalar-exports.mjs dist/calculator-web   # source checkout

semaprax.scalar-exports.json lists the exported functions. A build only writes files. Serving them and loading the module is your app’s job; follow the calculator browser consumer.

Edit and re-run (hot reload)

semaprax dev semaprax.toml --human

dev keeps one checked interpreter session open. It starts only after you send a start frame on stdin, then reads one JSON control frame per line (semaprax.hot-reload-control.v1). Operations are start, status, plan, activate, invoke and stop. Saving a file never runs code; invoke does. A broken revision is rejected and the previous one stays usable.

What must stay compatible before a swap

activate replaces the code only if everything reachable from the entry and test roots still agrees with the running revision:

• entry points and the permit set;
• type and interface records;
• the set of reachable functions, with the same parameter and return types and ownership;
• declared effects;
• pre- and postconditions, and the cleanup and loan plans.

Otherwise the swap is refused (incompatible_closure, policy_changed, identical_revision or unsupported_target) and the old revision keeps running. Functions no entry or test reaches are not compared.

plan only reports what activate would do. Its output says authority: none, and activate rebuilds the plan itself, so a plan you saved cannot be replayed. If a worker panics or an acknowledgement is lost, the session enters terminal_uncertainty: the status shows the flag (a JSONL boolean, or a line in --human), every later operation is refused, and nothing is retried or rolled back. Start a new session.

Frame limits: 64 frames per session, 4 KiB per input frame, 8 KiB per response.

printf '%s\n' \
  '{"schema":"semaprax.hot-reload-control.v1","id":1,"op":"start"}' \
  '{"schema":"semaprax.hot-reload-control.v1","id":2,"op":"invoke"}' \
  '{"schema":"semaprax.hot-reload-control.v1","id":3,"op":"stop"}' |
  semaprax dev semaprax.toml --human

Use --jsonl for tools. The VS Code extension drives this for you (editor setup). Native and Wasm swapping are not supported; --source-agent is refused by the public binary. Specs: Hot Reload Watcher v1, Hot Reload Session v1.

Check the environment

semaprax doctor                      # versions and OS
semaprax doctor --profile <id>       # probe tools through an admitted offline profile
semaprax doctor --target native|web|all --json

doctor never discovers tools on PATH. Without --profile it reports failed profile: an explicit offline profile is required and lists tools (clang, node, rust) as not probed. That is expected. If a native build fails with SPX-B101 failed to start clang, install Clang and put it on PATH.

Richer data, commands, resources

These use the execution route of their profile. A web scalar package and an owned-data npm package are different interfaces, even though both are WebAssembly.

Next: Integrate with another language, or prepare the package for review. References: Interpreter v1, Wasm Scalar Exports v1, OCI Deployable Artifact v1, Native Callable ABI v3.

Use Semaprax from another language

You can call Semaprax from a browser, Rust, C or C++, and you can let Semaprax call Rust. After this page you can choose a route and run its first command. Start with one function (a price calculation, a parser, a validator), not a whole application.

Choose a route

Inspect a C boundary

Pick functions by name or stable ID. Each command is read-only and prints deterministic output.

semaprax c-header examples/meaning.spx --function math.add --emit-header
semaprax abi-report examples/meaning.spx --function math.add
semaprax cxx-shim examples/meaning.spx --function math.add --emit-fragment
semaprax cxx-package examples/meaning.spx --function math.add --max-bytes 1000000
semaprax freestanding-object examples/meaning.spx

A header describes an interface; the link step supplies the implementation. Read the ownership facts before you write a consumer.

Describe functions as OpenAPI

semaprax openapi examples/meaning.spx --function math.add
semaprax openapi-compat base.json candidate.json     # breaking change check

openapi prints an OpenAPI document for the named functions, including the shared failure-status schema. openapi-compat compares two documents and reports whether the candidate breaks the base. Spec: OpenAPI v1.

Call Semaprax from Rust

The calculator example has two packages. The setup package reads Semaprax source and builds the SDK. The consumer package depends on the generated crate as an ordinary Cargo dependency and does not compile the compiler.

Follow the calculator README for tool paths. It names Clang, the archiver (on macOS /usr/bin/libtool), the manifest and output paths. Build the SDK first, then the matching consumer. Keep generated output out of Git.

semaprax build <project> --target rust is a different route. It exists only in the full toolchain built from source. Run semaprax help build and read the matching example first.

In CI, prepare the SDK in its own step so failures separate cleanly: the build-script consumer uses a prepared SDK and never starts the compiler from build.rs.

Call Rust from Semaprax

A Rust import declares one operation Semaprax may call. The generated adapter connects it to your Rust code. Keep input types, result type, effects and failure behavior explicit.

• Indexed route. A prepared Rust API index lists items and signatures. Binding checks package, version, source digest, target, features, path and signature. semaprax context <file.spx> <rust-path> --rust-index <index.json> answers questions about one imported item; add --candidates with a path prefix to list matches.
• Selected bindings. Owned Regex and Url bindings and generated callback adapters exist as starting points.
• Receiver-tied views. A returned view borrows from its owner. Keep the owner alive while you use the view.

Sources: checked Rust bindings, native Rust builder.

Test both sides

Call the generated interface with an ordinary value, a boundary value and an input that hits the documented error path. For owned data, also test an empty value and transfer and cleanup. Keep the consumer in the test: a source-only check cannot catch a consumer wired to the wrong package.

Next: Review and ship the selected package. References: C Header v1, C++ Shim v1, Public Owned Data API v1, Native Callable ABI v3.

Shipping: lock, resolve, review

You can pin a project’s interface, declare and resolve dependencies, preview a change before it touches source, and verify what you ship. After this page you know which command to run at each step. Every command here reads files you name and makes no network call.

Lock the interface

semaprax lock . --write                      # create semaprax.lock
semaprax lock . --verify                     # re-check it
semaprax lock . --compare base.lock          # breaking or not? (CI gate)
semaprax lock . --emit-interface > iface.json
semaprax lock . --compare-interface iface.json

The lock records identity, source digests, interface digest, targets and capabilities. --compare prints a verdict and exits 1 when the change is breaking:

{"changes":[{"classification":"breaking","detail":"a retained export changed its types, ownership, or contracts","kind":"interface-digest"}],"schema":"semaprax.project-lock-compatibility.v1","verdict":"breaking"}

A stale lock fails --verify with SPX-J123; run --write again or restore the sources. --compare-interface takes an interface file made by --emit-interface (SPX-J124 for anything else).

Resolve dependencies

semaprax add . std.num "^0.1.0"                       # declare
mkdir cache
semaprax fetch cache vendor/pkg.subject.json          # verify and file by digest
semaprax resolve . --target wasm32 --cache cache --write
semaprax resolve . --target wasm32 --cache cache --verify

Bundled std.* packages need no fetch. Other packages need a [dependency-sources] row. Nothing discovers a registry or reads the network.

For work outside a project, the package commands take subject files directly:

semaprax package report <file> [--max-bytes N]
semaprax package lock <subject.json>...
semaprax package resolve <subject.json>... --require <pkg>:<range> --target native64|wasm32 [--allow-capability <cap>]...

package report describes one checked file. lock and resolve pin a dependency closure; capabilities are granted only with --allow-capability.

Use a package registry file

A registry is one JSON document. The registry commands read semaprax.package-registry-document.v1 and never write, sign or publish. Schemas v2 and v3 also exist (snapshots that carry artifact manifests and build facts). They are library and host contracts, not read by these commands. What the commands do and do not verify: What Semaprax verifies.

semaprax registry search registry.json num
semaprax registry add registry.json std.num "^0.1.0"   # highest matching version
semaprax registry lock registry.json template.json --raw > registry.lock.json
semaprax registry fetch registry.json my.pkg 1.2.0 --raw > my.pkg.subject.json
semaprax registry verify registry.json snapshot-evidence.json
semaprax registry verify registry.json template.json lock-evidence.json
semaprax registry publish registry.json entry.json     # decide and print only

publish shows the registry document that would result. It publishes nothing. There is no default registry and no search path. A missing coordinate is SPX-Z927; an unreadable file is SPX-Z926; registry rules keep their SPX-PKR6xx codes. Specs: Registry Snapshot v1, Registry-Bound Resolution v1.

Change with review

Look first, then preview, then review. Impact, preview and review are read-only and bound to the exact source bytes: drift fails closed.

semaprax query . impact declaration calculator.add --depth 1 --max-bytes 4096
semaprax query . available-operations calculator.add
semaprax change preview . rename-display-name calculator.add sum
semaprax change preview . add-contract calculator.add ensures predicate.json
semaprax change preview . replace-expression <fn-id> <expression-id> replacement.json
semaprax change preview . add-declaration <anchor-id> declaration.json
semaprax review . transaction.json [--evidence]

A preview is not a transaction. Do not pass change preview output to review: review wants the closed transaction envelope (SPX-G525 otherwise). Evidence carries no authority; a passing verify is proof data, not permission to write.

Single-file patches

For one .spx file, a semantic patch (.spatch) works the same way:

semaprax impact app.spx change.spatch            # read-only blast radius
semaprax review app.spx change.spatch
semaprax patch-evidence app.spx change.spatch > evidence.json
semaprax verify app.spx change.spatch evidence.json
semaprax patch-with-evidence app.spx change.spatch evidence.json   # writes
semaprax patch app.spx change.spatch                               # writes

patch and patch-with-evidence are the only commands in this list that write source. The -v2 forms (patch-evidence-v2, verify-patch-evidence-v2, patch-with-evidence-v2) use the second evidence schema, and target-evidence adds per-target facts.

Change a managed workspace

A managed workspace holds 2 to 32 canonical .spx files under .semaprax-workspace. A successful change publishes one complete generation through a single ACTIVE pivot. It does not rewrite your original files or make the change atomic for Git or editors.

semaprax semantic-workspace-init ws paths.json
semaprax semantic-workspace-change-preview ws proposal.json     # read-only
semaprax semantic-workspace-change-evidence ws proposal.json > ev.json
semaprax verify-semantic-workspace-change-evidence ws proposal.json ev.json
semaprax apply-semantic-workspace-change-evidence ws proposal.json ev.json   # publishes

The order is always preview, evidence, verify, apply. Apply replays the evidence under the workspace lock first; stale or failed input leaves the workspace unchanged. The same four steps exist for structural changes (semantic-workspace-structural-change-*) and for operations derived from a declaration-level change (semantic-workspace-operations-derive, -change-proposal, -evidence). For read-only questions use workspace-snapshot, workspace-graph, workspace-context, workspace-impact and workspace-review. The older .wspatch route (workspace-init, workspace-preview, workspace-apply, workspace-patch-evidence) also remains.

The two workspace kinds are not interchangeable. The workspace-* commands expect a root made by workspace-init. Run workspace-snapshot on a semantic-workspace-init root and it fails with SPX-G150 (wrong ACTIVE schema). Pick one route per root. Specs: Semantic Workspace v1, Workspace Change v1, Operations v1.

Keep candidates and images

For tool builders. A candidate is a proposed project revision kept as data.

Run semaprax help <command> for each exact shape.

Serve a project to tools

semaprax service . [--mcp]                          # JSON-RPC (or MCP) on stdin/stdout
semaprax serve-workspace semaprax.toml host-policy.json
semaprax serve-workspace-mcp semaprax.toml host-policy.json
semaprax serve <file> [--max-request-bytes N]

service authenticates one project at startup and answers queries and transaction validation over line-delimited JSON-RPC 2.0, single client, local only. serve-workspace speaks the image-agent protocol; its closed host-policy file (semaprax.workspace-host-policy.v1) decides whether candidates, diagnostics, builds, tests and Git commits are allowed. The client cannot widen it. serve-image, serve-candidates, serve-test-candidates, serve-diagnostics and serve-diagnostics-tested are narrower variants of the same protocol. Specs: Service Transport v1, Workspace session CLI.

Check assurance and proofs

semaprax assurance-policy app.spx --profile require-static
semaprax assurance-diff base.spx candidate.spx --profile require-static
semaprax assurance-manifest app.spx
semaprax project-assurance-manifest semaprax.toml
semaprax properties app.spx --max-cases 64 --seed 11
semaprax region-report app.spx

assurance-policy checks each obligation against a profile (require-static, allow-runtime-guard, allow-test-evidence, report-only). assurance-diff shows what a candidate changes. properties generates bounded inputs from contracts and evaluates them (scalar, effect-free functions only). project-proof-check runs an external Lean or Z3 you name by absolute path against a project law; it needs --tool, --executable, --version-line and --host-profile. See Laws and proofs.

Verify a release you downloaded

semaprax release verify <release-dir>
semaprax doctor verify-release <release-dir> --trusted-root-sha256 <64-hex>

release verify reads release-manifest.json, release-provenance.json and, if present, release-signature-claim.json. It recomputes the manifest digest and re-hashes every archive the manifest names; nothing a document says about itself is trusted. doctor verify-release requires complete signed material and checks it against the root digest you pass (SPX-Z707 on mismatch). Get that digest from a channel you trust, not from the release directory. Missing manifest: SPX-Z705. Verifying does not install anything; see Install.

Check an audit capsule or a workflow

semaprax audit inspect capsule.json
semaprax audit verify capsule.json objects/ --require-role reviewer
semaprax audit diff a.json b.json
semaprax workflow validate workflow.json
semaprax workflow inspect workflow.json
semaprax workflow checkpoint checkpoint.json
semaprax workflow dispatch policy.json request.json

audit inspects, verifies and diffs evidence capsules offline. Verification can check Ed25519 signatures against a trust roster you supply (--trust-roster); nothing here signs or submits to a log. workflow validate and inspect check a typed workflow graph. workflow checkpoint decodes a checkpoint and prints its state; it never resumes anything. workflow dispatch decides whether a request target is in a declared policy and records the decision. All are read-only. See Audit Capsule v1.

Checklist

1. Commit semaprax.lock beside semaprax.toml.
2. Gate CI on lock --compare <base.lock>.
3. Run query impact, then change preview, then review before you apply.

Exact rules: Project Lock v1, Project Dependency Resolution v1, Semantic Impact v1, Semantic Review v1, Unified CLI v1.

Build an agent as a program

You will learn how a Semaprax agent declaration splits one model-driven task into checked stages, how a proposal differs from permission, and how to pick a model route. This chapter is for people building an agent. To let a coding assistant edit .spx files, read Agent workflow.

Status. Source agents, the runtime, and model routing are partial and beta. The CLI replays recorded transcripts. A live model needs a Rust host that you write and that owns the provider credentials. Routing evidence is local and fixture-based: no live provider, hosted, or billing claim.

What is a turn?

Each turn runs these stages. Your code owns every stage except the model call.

initialize once
     |
observe -> propose (model) -> decode -> authorize -> execute (effect) -> reduce
   ^                                                                       |
   +------------------------------- Continue -----------------------------+
                          or Complete / Suspend / Fail

Authorization runs again on every turn. A grant for one turn never carries over.

Declare an agent

An agent declaration names six types and the stage functions, each with an @id:

@id("example.agent")
agent Example {
    types { type task; type state; type observation;
            type proposal; type outcome; type result; }   // each with an @id
    operations {
        fn initialize;  fn observe;  model fn propose;
        fn authorize;   effect fn execute;  fn reduce;    // each with an @id
    }
    runtime_v1 { canonical_json "..."; }
}

Only propose is model fn. Only execute is effect fn. Missing or duplicate IDs report SPX-P124. The full rules are in Language-native Agent syntax.

Check and inspect the committed examples:

semaprax check examples/everyday-agent-v2-project
semaprax check examples/routed-agent-project
semaprax agent skill        # the agent contract this compiler carries

Run a recorded transcript

The CLI never calls a model. It replays recorded input:

Do not put an API key in a transcript. A live provider connects through the host integration, not these commands.

Give the model only what it needs

The runtime enforces your declared limits on every run:

• It calls only tools the profile allows. Each tool has a closed argument schema and a read effect.
• One run is single-threaded and bounded: at most 16 turns, 32 provider attempts, 32 tool calls, and five minutes. A profile may lower these, never raise them.
• The runtime never retries a tool or an uncertain provider call.
• Cancellation is cooperative, not forced.

See Budgets, checkpoints, and recovery for limits and what happens when one is reached.

Route to a model

Routing picks one approved model profile per task, and can change it between turns. A router names a profile ID only. It cannot add a tool, capability, or limit beyond what the deployment grants.

Rules mode makes zero router calls. An operator pin that fails screening is refused, not replaced. A revoked deployment is refused on resume.

Runnable examples, offline with fixture models:

• examples/routed-agent-project: two approved profiles, a pin, and a re-route.
• examples/support-routing-project: route a support request to one of two agents.
• examples/tool-choice-project: select one of two granted read-only tools.

Run them with cargo test --locked -p semaprax --test agent_runtime_v1 routed_agent_example (or choice_examples). The harness command is in the release archive’s semaprax and in a source-built semaprax-full. A standalone semaprax refuses it. See Harness.

Test it before a model is involved

1. Supply a fixed task and a scripted sequence of proposals.
2. Check the terminal case and its data.
3. Add one denied proposal and confirm authorize refuses it.
4. Set a low turn limit and confirm a broken reducer cannot loop.

The interpreter is the default route. Native C11 and Core Wasm stage routes are explicit host choices with their own requirements.

Next: Budgets, checkpoints, and recovery.

References: Agent Runtime v1, Runtime model routing v1, Iterative lifecycle v2, Typed effects v3.

Budgets, checkpoints, and recovery

You will set limits for an agent, and learn what happens when it stops between asking for an operation and seeing the result. Decide this before an agent does important external work. The question is always: what was authorized, what may have happened, and what can safely happen next?

Status. Local and fixture-based evidence. The recovery routes (semaprax-full source-live) are private tooling, not the public CLI.

What limits does a run have?

Since v0.9.0 the runtime checks the live clock and the remaining allowance before each model call, including routing calls. Each call also gets its remaining deadline as a positive budget. A new turn that has no time or allowance left stops before any provider call.

When no model is both eligible and affordable, the run ends policy_rejected with SPX-G206. It still returns its Trace, Evidence, and accounting receipt for work already done. That terminal is replayable: replaying returns the same result and calls no provider.

How is cost recorded?

A reservation sets money aside before a call. An observation records what the provider reported afterward.

A lost response does not prove the provider did no work, so unknown stays unknown. The accounting receipt reports reserved, observed, and unknown totals. It cannot bill or settle.

What does the journal record?

The journal writes intent before dispatch and keeps the result after.

Since v0.9.0 a routed session journals effect_intent before the host callback that may run tool effects. Only model bytes recovered before any durable intent allow exactly one callback. An uncertain dispatch or effect halts the session for reconciliation. It is never retried with another model.

Do not repeat an uncertain write, message, or payment. Reconcile it first.

What is a checkpoint?

A checkpoint belongs to one execution and one source or deployment. Recovery checks its bindings, limits, and retained results before doing more work. A JSON file with plausible state does not replace the checkpoint producer and the trusted store. A hash identifies bytes but does not stop someone who controls the storage from rolling the whole history back. Protect the store at the host.

Resume after an interruption

RoutedSession::resume restores the journal. Completed turns replay with no route, model, or effect calls. An in-flight turn reuses its recorded route with zero router calls. A revoked deployment is refused and never rebound.

For source agents, the private semaprax-full tool has source-live run, resume, migrate, and repair:

semaprax-full help source-live

It takes a project config, a checkpoint directory, a provider executable, and an empty scratch directory. Start with an injected handler or recorded input, not live credentials. See Source live CLI, Source journal, and Source migration.

Change the agent’s state type

When the State type changes, an old checkpoint may not fit. A migration binds the old and new revisions and checks the transformation. Spending carries across it: a new revision does not reset the budget already used. A mismatched predecessor is refused.

Delegate to a child agent

A child session runs under a grant: an allowance reserved from the parent, a depth limit, one profile, and the parent’s deadline. A child never widens the deadline or overspends. Settling a child never refunds. Delegation is bounded and runs on the same host.

Money-moving operations

A model’s payment proposal is input to a workflow of intent, policy, approval, signing, broadcast, and reconciliation. The host supplies the wallet and the authority. Keep simulations apart from real payments. See Economic agent.

Test recovery

Interrupt a run at each point and check that settled work is never repeated:

1. Before dispatch.
2. After intent is recorded.
3. After the handler returns.
4. After the terminal result.

Then try a changed source revision, a lowered budget, a cancelled task, and a mismatched checkpoint.

Next: Source map.

References: Agent Runtime v1, Runtime model routing v1, Per-operation checkpoints, Model budget policy.

Style guide

fmt and check enforce most style. This page covers what tools cannot decide: identities, naming and layout. After this page you can name things so that agents, queries and patches keep working across renames.

Give every declaration an ID

An @id is a declaration’s permanent address. Renames do not change it, and every query, patch and graph edge uses it.

module calculator.core;

@id("calculator.add")
fn add(left: i64, right: i64) -> i64
{
    left + right
}

Without an @id, check warns SPX-S103: the automatic identity changes when the function is renamed. Assign one by hand, or use semaprax fix --plan (see Debugging).

• Namespace by module: calculator.add, calculator.tests.test_add. Avoid flat global names and trees like a.b.c.d.e.f.
• Name the meaning, not today’s name: math.add survives a rename to plus.
• ID fields, cases and methods too. Queries and patches address them by ID.
• Never reuse an ID for a different declaration. A stale ID with new meaning is worse than none, and nothing can warn about it.

Names

Layout: let fmt do it

semaprax fmt .            # rewrite every file in canonical form
semaprax fmt . --check    # report drift, write nothing

Canonical form: the body’s { on its own line; one statement per line; compact if, match and record literals; a trailing , after every field, case and arm including the last. fmt parses all files before rewriting any, and keeps // comments (placement rules). Workspace transactions do not promise to keep comments, so put durable intent in @id names, contracts and tests. Run fmt before check. A formatting diff is never the interesting part of a review.

Organize files

• One module per file, one concern per module.
• The entry module holds main and wiring. Logic lives in sibling modules imported by ID, right after the module line: use function @id("calculator.add") from calculator.core as add;
• Tests live in their own module, listed under tests in the manifest.
• Keep bodies shallow. Nesting deeper than 128 levels fails with SPX-P207, but a few levels is already a sign to extract a named helper with its own @id and contracts. Then it is queryable and testable.

Put intent in contracts

requires and ensures state what callers may pass and what they get back, and run on every call, including under test. Prefer them to comments. Write the effect list (permit and uses) as narrowly as the code allows. See Contracts and effects.

Keep the manifest canonical

Keep semaprax.toml byte-canonical: table order, one blank line between tables, one-line arrays, no comments. SPX-J100 names the first differing line. See Manifests. Pin what you ship: semaprax lock . --write, then --verify, and --compare <base.lock> in CI (Shipping).

Generate docs from the source

semaprax doc <file> renders declarations, signatures, contracts, effects and comments from the checked graph, so your docs cannot drift from the code (--json for tools). A file given to doc needs a fn main() -> i64.

Testing

A test is a function that returns i64: 0 passes, anything else fails. After this page you can write tests, read a failure, and run the full check ladder before you push.

Run a project’s tests

Save these four files in a new testing-demo/ directory (the src/ files go in testing-demo/src/).

schema = "semaprax.manifest.v1"

[package]
name = "testing-demo"
version = "0.1.0"

[modules]
entry = "demo.app"
sources = ["src/app.spx", "src/core.spx", "src/tests.spx"]
tests = ["demo.tests"]

[exports]
web = ["demo.divide"]

module demo.core;

@id("demo.divide")
fn divide(left: i64, right: i64) -> i64
    requires right != 0
    ensures result * right <= left
{
    left / right
}

module demo.app;
use function @id("demo.divide") from demo.core as divide;

@id("demo.main")
fn main() -> i64
{
    divide(84, 2)
}

module demo.tests;
use function @id("demo.divide") from demo.core as divide;

@id("demo.tests.test_divide")
fn test_divide() -> i64
{
    if divide(84, 2) == 42 { 0 } else { 1 }
}

@id("demo.tests.test_divide_by_one")
fn test_divide_by_one() -> i64
{
    if divide(7, 1) == 7 { 0 } else { 2 }
}

@id("demo.tests.main")
fn main() -> i64
{
    0
}

semaprax test .

project tests passed (2 named cases)

test runs the test module’s main, then every zero-parameter test_* function in that module. Each needs its own @id. The module must be in the manifest’s tests entry. A test_* function with another shape is not a case.

Options: --json for the full case list (semaprax.project-execution.v1), --max-steps N, --max-bytes N. Tests run in the bounded interpreter only. They do not exercise native or Wasm output, so build and test those targets separately.

Read a contract failure

A failed requires or ensures fails the case that triggered it and names the clause and arguments. Change divide(7, 1) to divide(7, 0) and run again:

failed demo.tests.test_divide_by_one: language status {"schema":"semaprax.status.v1","domain_id":"semaprax.contract.v1","code":1,"class":"contract","retryable":false}
  contract: requires right != 0 in demo.divide
  arguments: left = 7, right = 0

Write the contract first, then test valid inputs at the edges: zero, one item, the largest accepted value. Do not keep a deliberately invalid call in the normal suite: it fails the suite. Put it in a separate fixture and assert the failure status from your harness. For expected user-facing errors, return Result and test the error arm. See Contracts and effects.

Prove the test can fail

Change == 42 to == 41, run semaprax test ., confirm it fails, then change it back. A test that cannot fail checks nothing. Keep one purpose per test: test_divide_by_one is easier to diagnose than test_everything.

More test tools

A single file given to properties or interpret needs a fn main() -> i64 (SPX-T105 otherwise).

The check ladder

Run these in order and stop at the first failure:

semaprax fmt . --check        # canonical layout, manifest order
semaprax check .              # types, contracts, effects, ownership
semaprax test .               # executable checks
semaprax build . --target web -o dist/web   # target acceptance
semaprax lock . --compare base.lock         # CI: fail on breaking interfaces

fmt . parses every file before it rewrites any. check, test, build and fmt accept ., a directory, semaprax.toml or --manifest-path.

Check handbook examples

If you edit these docs, run from the repository root:

/usr/bin/python3 scripts/check-handbook.py --compiler /absolute/path/to/semaprax

It formats temporary copies, checks and runs every marked example, compares output, and verifies links and chapter navigation. --structure-only skips the compiler. Unmarked snippets are not run.

References: Project Test Cases v1, Property-Test Generation v1.

Debugging diagnostics

A diagnostic has a stable SPX-... code, a message, a file:line:column location and usually a help: line with the fix. After this page you can find the cause of an error and the smallest fix for it. Match on the code, not the wording: wording changes, codes do not.

error[SPX-P106]: `return` is not admitted; a block's value is its final expression at bad.spx:6:5
  help: delete `return` and the trailing `;` so the value is the block's last expression

The loop

1. semaprax fmt <file>. Many “errors” are layout the formatter fixes.
2. semaprax check <file>. Add --json for one JSON object per diagnostic (code, severity, message, path, location, help).
3. Fix the first diagnostic at its location. Later ones are often knock-on.
4. Still unclear? Look up the code (case-sensitive):

semaprax help diagnostic SPX-T208     # what you wrote, and the fix
semaprax help diagnostic codes        # every indexed code
semaprax explain SPX-T208 [--json]    # the installed explanation

Exit codes: 1 for compile or run failures, 2 for a bad command line. A warning such as SPX-S103 (a function with no @id) still exits 0.

Check the project, not one file

A module without main is a library module. Checking it alone fails with SPX-T105, SPX-G172 or similar. Run semaprax check . from the project. Single-file commands (run, doc, properties, package report, …) need a file with fn main() -> i64.

Apply a one-step repair

Some fixes have a plan. fix --plan lists the repair operations your binary knows. For a function missing its @id (SPX-S103):

semaprax fix --plan
semaprax fix app.spx assign-function-id <automatic-function-id> --plan
semaprax repairs app.spx assign-function-id <automatic-function-id>
semaprax repair app.spx <repair-id> --persistent-id my.namespace.main

--plan changes nothing. repair is the step that writes source.

The top fixes

SPX-F102 (interpreter does not admit the program) is not a source error: use run --native.

Environment and command errors

Every rejected command prints hint: run semaprax <command> --help. Use it.

Ask a smaller question

semaprax help language topics                  # then: help language ownership
semaprax help shapes record                    # smallest declaration example
semaprax help library std.core.compare         # one stdlib entry (~200 bytes)
semaprax skills get language                   # packaged language guidance

The full card is the Agent quick reference, printed offline by semaprax help language. The diagnostics reference lists codes by family.

Cookbook

Copy-paste recipes. After this page you can do the common jobs: print text, loop, match, handle errors, and run the everyday project commands. Language recipes are complete modules: save one as app.spx and semaprax run app.spx. A program that exits 0 prints 0 after its own output.

Print a greeting

module app.greet;

permit { process.stdout.write }

@id("app.main")
fn main() -> i64
    uses { process.stdout.write }
{
    let greeting = string_concat("hello, ", "world");
    let view = string_as_str(greeting);
    let written = stdout_write(str_as_bytes(view));
    if written == 12usize { 0 } else { 1 }
}

stdout_write returns the byte count. Assert it so a truncated write fails loudly. The module needs permit { process.stdout.write } and uses on main exactly as above (SPX-E101, SPX-E102 otherwise).

Sum digits with a loop

module app.sum;

@id("flow.digit_sum")
fn digit_sum(value: i64) -> i64
    requires value >= 0
    ensures result >= 0
{
    let mut remaining = value;
    let mut total = 0;
    while remaining > 0 {
        total = total + remaining % 10;
        remaining = remaining / 10;
        remaining > 0
    }
    total
}

@id("app.main")
fn main() -> i64
{
    if digit_sum(98765) == 35 { 0 } else { 1 }
}

The loop pattern: let mut state, while with scalar updates, continuation condition as the body’s last line, pure scalar result.

Classify with match

module app.sign;

@id("flow.classify")
fn classify(value: i64) -> i64
{
    match value { 0 => 0, -1 | -2 => -9, n if n < 0 => -1, _ => 1, }
}

@id("app.main")
fn main() -> i64
{
    if classify(-2) == -9 { 0 } else { 1 }
}

Order arms from specific to general; the final _ catch-all is mandatory.

Safe division with Result

module app.divide;

@id("data.checked_div")
fn checked_div(left: i64, right: i64) -> Result<i64, i64>
{
    if right == 0 { Result<i64, i64>::Err { error: 1 } } else { Result<i64, i64>::Ok { value: left / right } }
}

@id("app.main")
fn main() -> i64
{
    let ok = match checked_div(8, 2) { Result::Ok { value: v } => v, Result::Err { error: code } => code, };
    let err = match checked_div(8, 0) { Result::Ok { value: v } => v, Result::Err { error: code } => code, };
    if ok == 4 && err == 1 { 0 } else { 1 }
}

Construct with type arguments (Result<i64, i64>::Ok), match without (Result::Ok). Callers handle both arms; the compiler enforces it. The interpreter does not admit this program (SPX-F102), so run it with semaprax run app.spx --native.

Update a record immutably

module app.move_point;

@id("data.point")
record Point {
    @id("data.point.x")
    x: i64,
    @id("data.point.y")
    y: i64,
}

@id("app.main")
fn main() -> i64
{
    let origin = Point { x: 1, y: 2 };
    let moved = origin with { y: 10 };
    if moved.x == 1 && moved.y == 10 { 0 } else { 1 }
}

with builds a new value; the original is untouched. Construction must name every field. Run it with --native (SPX-F102 in the interpreter).

Count bytes in a string

module app.count;

@id("bytes.count_a")
fn count_a(text: borrow str) -> usize
{
    let view = str_as_bytes(text);
    let length = byte_len(view);
    let mut index = 0usize;
    let mut hits = 0usize;
    while index < length {
        hits = match byte_get(view, index) { Option::Some { value: byte } => if byte == 97u8 { hits + 1usize } else { hits }, Option::None {} => hits, };
        index = index + 1usize;
        index < length
    }
    hits
}

@id("app.main")
fn main() -> i64
{
    let word = "banana";
    if count_a(string_as_str(word)) == 3usize { 0 } else { 1 }
}

The byte pattern: borrow the string, view it as bytes, walk with usize indices, destructure byte_get’s Option<u8>. Byte 97u8 is 'a'.

Start a project and run its checks

semaprax new my-app && cd my-app
semaprax fmt . && semaprax check . && semaprax test . && semaprax run .

fmt first, check second. Stop at the first failure.

Add a test

Add a function to your test module and list that module under tests:

@id("my_app.tests.test_add")
fn test_add() -> i64
{
    if add(2, 2) == 4 { 0 } else { 1 }
}

semaprax test . runs every zero-argument test_* function and names failures.

Add a dependency

semaprax add . std.num "^0.1.0"
semaprax help library std.num      # exact signatures and stable IDs

Find who calls a function

semaprax query . --calls my-app.add          # callers
semaprax context . my-app.add --direction both --depth 1 --max-bytes 4096

Rename safely

semaprax change preview . rename-display-name my-app.add sum

Read the preview. It writes nothing. See Shipping.

Ship a web package

semaprax build . --target web -o dist/web
semaprax lock . --write

Gate CI on interface breaks

semaprax fmt . --check && semaprax check . && semaprax test .
semaprax lock . --compare base.lock      # exits 1 when breaking

Run a network command offline

semaprax network-run . --fixture http.fixture.json --arg https://example.test/

This uses a recorded fixture; no real connection opens. See Profiles.

Driving Semaprax from an AI agent

The compiler answers questions about program meaning as small, bounded data. An agent spends tokens on source and decisions, not on dumping a repository. After this page you can set up a coding agent to write, check and change Semaprax safely.

New to the CLI? The visual tour shows the first commands. This page is for an assistant editing your project. An agent program written in Semaprax is a different thing.

Give the agent its instructions

semaprax new writes an AGENTS.md into every project. It lists the commands and the rules that differ from other languages, and points at one language topic instead of the 33 KB card. For other tools:

semaprax skills get agent          # also: language, graph, stdlib, packages, effects
semaprax agent skill               # the installed agent skill: authority classes, verbs
semaprax query --capabilities      # what this binary's query and change commands accept

Each verb in the skill has an authority class: read_only, candidate_only, test_execute, source_write or publication. Grant an agent the lowest class that does its job.

The edit loop

1. Write the file. Run semaprax fmt <file> && semaprax run <file> (one call).
2. On failure, fix the first diagnostic at its line and column. Match the SPX-... code, not the message. Plain output is smaller than --json.
3. Read small .spx files directly. Never fetch graph to look around: on the calculator it is about 40 times the source.

In a project use semaprax check ., semaprax test .. See Debugging.

Ask bounded questions

semaprax query <project> --id <stable-id>        # find a declaration
semaprax query <project> --calls <stable-id>     # who calls it
semaprax query <project> --kind function --effect clock.read
semaprax context <project> <stable-id> --direction both --depth 1 --max-bytes 4096 --max-nodes 16
semaprax context <file> <stable-id> --depth 1 --filters contracts,ownership --max-bytes 4096

Check truncation before treating a result as complete. --max-bytes for context is at least 2048. Project context does not accept --filters. Use graph only when a tool needs the whole expression tree or cleanup plan, and --json only when you need exact revision fields. semaprax doc <file> renders declarations, contracts and effects as text or --json.

Ask for narrow help

semaprax help <command>                         # one command's grammar
semaprax help language topics                   # then: help language <topic>
semaprax help diagnostic <SPX-code>             # one fix
semaprax help shapes <kind|stable-id>           # minimal declaration example
semaprax help library <module|name|stable-id>   # one stdlib entry

help all and the full card are for broad questions. One help library lookup is about 200 bytes; the full catalog is about 22 KB.

Write source an agent can change later

• Put an explicit @id on every declaration, field and case. Later query, context and patches address them by ID, and IDs survive renames.
• Put intent in requires/ensures, tests and ID names. fmt and single-file patch keep // comments, but workspace transactions do not promise to.
• Tell the agent the project’s profile before it changes parameter or result types.

Make checked changes

semaprax query <project> impact declaration <id> --depth 1 --max-bytes 4096
semaprax change preview <project> rename-display-name <id> <new-name>
semaprax review <project> <transaction.json>
semaprax verify <subject> <change> <evidence.json>

Impact, preview and review write nothing and are bound to exact source bytes: drift fails closed. A preview, a review report and an applicable transaction are different objects; do not feed one to a command that wants another. Evidence carries no authority: replay it with verify before you apply anything. The full flow, including managed workspaces, is in Shipping.

Give an agent a live connection

The host decides authority. The client cannot widen the policy. An agent inside VS Code uses saved-source candidate sessions; see Editor setup.

Smaller context

semaprax compact ... and the token report script shrink what a model reads. See Context and performance. For a visual map use the semantic explorer.

A coding agent is not an agent program

Agent programs written in Semaprax have task, state, proposal and authorization roles. Inspect and replay them with semaprax agent inspect|run|replay (Agent programs). The development harness (semaprax harness ...) lets a coding agent propose changes under compiler checks (Harness). The release archive ships the full build as semaprax, so the command works there. A standalone or crates.io semaprax refuses it (exit 2); build semaprax-full from source instead. It is development tooling, so do not build a product on it.

The complete agent contract is the Agent quick reference, printed verbatim by semaprax help language.

Explore a project’s meaning

The semantic explorer turns a checked project into a view you can read, share or compare. After this page you can export one declaration’s neighborhood as HTML, Markdown, JSON or SVG, and answer smaller questions from the terminal.

Export a focused view

Run this in a project directory (the output file must not exist):

semaprax explore semaprax.toml --target calculator.add --depth 1 --format html --output calculator-explorer.html

Open the file in a browser. The view is centered on calculator.add. --depth limits how far the neighborhood extends. Omit --target and --depth for the whole project.

An existing output path fails with SPX-G328. Use one new filename per format and subject. Keep generated reports out of commits unless you version them on purpose, and keep the revision lines when you share one.

Ask smaller questions first

semaprax query . --id calculator.add                  # where is it?
semaprax query . --calls calculator.add               # who calls it?
semaprax query . --called-by calculator.app.main      # what does it call?
semaprax query . available-operations calculator.add  # which typed changes are allowed?
semaprax context . calculator.add --direction both --depth 1 --max-bytes 4096
semaprax doc <file.spx>                               # declarations, contracts, effects

A caller uses the function. A callee is a function it calls. Keep the two directions straight when you estimate the effect of a change.

Preview a rename

semaprax change preview . rename-display-name calculator.add sum

The preview renames the display name and keeps the stable ID. It writes nothing. Next steps are in Shipping.

Review a candidate

Pass a candidate capsule and the exact digest you intend to review:

semaprax explore semaprax.toml --candidate-capsule capsule.json --expect-candidate sha256:<digest> --format markdown --output review.md

If the digest differs, the export fails: you never review a candidate you did not mean to. A capsule is revision-bound candidate data. Make one with project-candidate-export (Shipping). semaprax compact candidate-diff <project> <capsule> gives a compact diff.

Fill a typed hole or take a compiler repair

Use these when a change is half done or was rejected. Both work on a candidate, which is in memory, so source stays unchanged until you commit.

A typed hole marks one expression in a function body that you will fill later. The compiler gives you the hole’s expected type and ownership, the effects allowed there, the names in scope and the calls you may use. A fill becomes a normal typed change and goes through the full checks. There are no placeholder source text, no invalid code and no run. You can open up to 16 holes, and they must not overlap.

semaprax serve-diagnostics semaprax.toml     # JSON-RPC over stdin and stdout

A client sends hole/open-expression, then hole/query (context), hole/fill-suggestions, hole/fill, and finally hole/complete. hole/discard drops the draft. complete refuses while any hole is open (SPX-G232 for a stale or unresolved selection). In VS Code use Open Typed Hole and Fill Selected Hole from Active Scratch (Editor setup).

A repair route is a fix the compiler derived and already admitted. When candidate/attempt rejects a change, the same server keeps the attempt: attempt/repair-catalog lists only proposals that pass every check (or says there are none), and attempt/repair-apply turns one into a new candidate. The compiler never picks or ranks for you. For files rather than candidates, the one repair today is the missing @id fix (SPX-S103): semaprax fix --plan, then repairs and repair (Debugging).

Specs: Expression Holes v1, Image Candidate Diagnostic Protocol v4.

What to ask before you accept a change

Which declaration changed? Which callers are involved? Did contracts or effects change? Which tests cover it? Refresh the report after every edit: an old diagram stays readable long after it stops describing the project.

Next: Use the same workflow from an AI coding agent. References: Semantic Explorer v1, installed command catalog.

Measure context size and reuse checked work

Two things make a tool-driven workflow cheaper: a smaller context to read, and a cache that reuses checked compiler work. After this page you can produce a compact view, measure it, and warm a semantic cache. Measure the two separately so you know which change helped.

Pick the smallest view

1. Source, when the file is small.
2. query to find a declaration, then context for its neighborhood.
3. compact for a model-facing encoding.
4. graph only when a tool needs the whole thing.

compact has five forms. Each takes --encoding text|binary|model-text and --replay <encoded>, which rebuilds from current source and compares with an encoding you already hold:

model-text is the text form meant for models. binary belongs with a binary-aware consumer. From the repository root:

semaprax compact context examples/meaning.spx math.add --max-bytes 4096 --encoding model-text
semaprax compact api-surface examples/frame-payload-project/semaprax.toml --encoding model-text

Measure a real input

scripts/token_report.py compares exact payloads with a local tokenizer. It needs locally installed tiktoken and cached cl100k_base or o200k_base assets, and never downloads anything.

python3 scripts/token_report.py projection \
  --semaprax "$(command -v semaprax)" \
  --input examples/meaning.spx \
  --profile context \
  --selection math.add \
  --encoding model-text \
  --measurement-tokenizer cl100k_base \
  --allow-bytes-only \
  --output target/meaning-token-report.json

python3 scripts/token_report.py show target/meaning-token-report.json --format text

--output must be a new file unless you pass --overwrite. With --allow-bytes-only, missing token counts stay empty while byte counts are reported. Drop the flag when the check must fail without token counts. On Windows, give the absolute path to semaprax.

Other subcommands: compare (two reports) and session (aggregate a recorded event stream; show renders it). The MCP session recorder is a recording example. VS Code shows a snapshot with SEMAPRAX: Show Token Report.

Read a report

A projection report compares the compact payload with the same selected JSON content. That is not the same as comparing a narrow context with a whole repository dump.

Bytes, local token counts and provider-reported usage are different measurements. Planner choices (byte-v1, lexical-v1) are not model-tokenizer counts. Keep the measurement kind with any number you share.

Reuse compiler work with a semantic cache

A semantic cache stores checked HIR (the compiler’s resolved program) so a new process can skip some frontend work on the same project. It carries no source authority. On a supported Unix host, from the repository root:

mkdir -p target
mkdir -m 700 target/handbook-cache
CACHE="$(cd target/handbook-cache && pwd -P)"
semaprax semantic-cache-init "$CACHE"
semaprax semantic-cache-persist examples/calculator-project/semaprax.toml "$CACHE"

The store directory must be new, empty and owner-only. Init creates a private key: keep it protected and out of Git. The persist receipt holds the entry_digest you need next.

semaprax semantic-cache-warm-open <manifest> <absolute-store-root> <entry-digest>
semaprax semantic-cache-refresh <manifest> <absolute-store-root> <entry-digest>
semaprax semantic-cache-cold-open <manifest>
semaprax semantic-cache-load <store-root> <entry-digest>
semaprax semantic-cache-evict <store-root> <entry-digest>
semaprax semantic-cache-lifecycle <manifest> <empty-store-root>

A compiler upgrade can invalidate an entry even when the version string is unchanged: compatibility includes the executable identity. For a fair cold and warm comparison, fix the compiler build, source revision, cache state and task. retention-metadata-* commands manage retention checkpoints for stores; see Semantic Retention Metadata CLI v1.

Benchmark context size

semaprax context-benchmark <benchmark-manifest> measures agent-context sizes from a tab-separated manifest that must start with schema<TAB>semaprax.agent-context-benchmark.v1 (SPX-G005 otherwise). See Agent Context v1 for fixtures.

Next: Configure the editor report view. References: token reporting, Compact Projection v2, Persistent Semantic Cache v1.

Harness: let an agent propose changes under checks

After this page you can set up the development harness, run one agent-proposed repair through compiler checks, and connect it to an outside coding agent such as Claude Code.

The harness is optional tooling around the compiler. Ordinary check, build and run never start it, read its files or need its adapters. The compiler is a service the harness calls; the harness cannot overrule a compiler verdict.

Where it lives. semaprax harness <verb> exists in the release archive’s semaprax and in a source-built semaprax-full. The standalone semaprax build answers harness is unavailable in the standalone crates.io package and exits 2. semaprax-harness <verb> is the same code as its own binary in a checkout.

Status. Development harness. The specs record local macOS arm64 evidence; Linux is untested. Treat model routing as rules-based unless you select a provider yourself (see Routing).

Set up

semaprax harness setup --project . --preset native
semaprax harness setup --project . --preset native --yes

Without --yes, setup prints a plan and changes nothing. With it, setup unpacks the bundled adapters into the harness home ($SEMAPRAX_HARNESS_HOME, default ~/.config/semaprax/harness), adopts and trusts the ones you chose, sets your preference, and writes semaprax.harness.toml into the project if none exists (provider ids only: no paths, no trust). It keeps an existing project file and never overwrites it. Running it twice reports noop. It never scans PATH or $HOME and downloads nothing; pass tools with --path-dirs or --tool graft=/abs/path. Presets: native (built-in context and command view, official skills) and local-efficient (adds RTK and one repository provider, Graft by default). A missing optional tool falls back to the built-in and exits 0.

semaprax harness status [--json] shows what resolved, and explain <kind> says why.

Run one repair

semaprax harness run . --task task.json --proposal proposal.json

run follows one pipeline on one revision: authenticate the source, run check and test, gather context within a byte budget, get a proposal (from your --proposal file or a model you selected), preview it as a candidate, check the candidate in a scratch copy, and stop. It stops at approved-candidate-ready unless you pass --apply-policy policy.json, which publishes the candidate to a local Git repository under that policy.

The harness refuses a proposal that deletes a requires/ensures line, adds a uses effect, or weakens the requirements (SPX-HPD042 to HPD044). A candidate that fails checks is SPX-HPD050, never success. A publication that may have happened is uncertain and is never retried. Exit 0 means approved-candidate-ready, published or no-repair-needed. --disable runs with built-ins only and no external calls. Spec: Harness workflow.

All verbs

Exit codes: 0 success, 1 refused or failed with diagnostics, 2 usage error. Most verbs accept --json.

Project configuration

semaprax.harness.toml sits in the project and holds no paths, secrets or trust grants:

schema = "semaprax.harness-config.v1"

[profile]
enabled = true

[capability."context.repository"]
mode = "auto"            # disabled | auto | required

[budget]
context_max_bytes = 16384

Capability kinds are context.repository, command.view, decision.evaluate, model.generate and skill.catalog. For each, an explicit pin beats a user preference, which beats the single compatible trusted installation, which beats the built-in. required never falls back to a built-in. resolve writes semaprax.harness.lock; --frozen fails on any difference. Permissions in an adapter descriptor are requests. Grants live only in the harness home and are bound to the descriptor, adapter and upstream digests, so a changed or widened adapter loses its grant. Spec: Harness provider host.

Adapters

Bundled under packages/semaprax-harness-adapters/ and embedded in the binary. Each is a separate process on JSON-RPC over stdio, and none enters the compiler build.

To write your own, start from the SDK in packages/semaprax-harness-adapters/sdk/ and check it with semaprax harness conformance. Spec: Adapter SDK.

Routing models

Routing is policy-first. By default simple rules pick the route with zero router calls. Modes are rules (default), pin, experimental and auto; auto is used only for a profile that passed its qualification gate, and none has yet. Every report carries route.explain. semaprax harness status --routing lists profiles; --check validates them without cost, and --probe makes one announced, metered call. The current support table is in Harness decision.

Connect Claude Code

semaprax harness bridge . --setup claude-code            # shows what it would write
semaprax harness bridge . --setup claude-code --write    # writes the host settings
semaprax harness bridge . --stdio                        # protocol over stdin and stdout

The bridge is a host-side surface: LF-delimited JSON-RPC (semaprax.harness-bridge.v1) that begins with a bridge/handshake. The outside agent keeps its own model. Semaprax does not claim to route it, and the handshake says who owns the model. Phase routing applies to Semaprax-owned worker requests only. The bridge adds no authority to semantic methods. Spec: Harness bridge.

Related

• Installed guidance for agents without the harness: Driving Semaprax from an AI agent.
• Serve a project to an agent over MCP: Shipping.
• Measure token use: Context performance.
• Trust limits of grants and evidence: What Semaprax verifies.

Specialist commands

After this page you know the commands that no other chapter teaches, what each one prints, and which ones are not products yet. Most people never need these; they exist for tool builders, CI authors and compiler contributors.

Every analysis below reads one source file, changes nothing, and prints one JSON envelope with a schema, a digest and usually nonclaims that list what the output does not say. The output is data and never grants permission. Add --max-bytes N to cap it; an overflow fails instead of truncating.

Ask about one module

semaprax simd-report examples/meaning.spx

{"schema":"semaprax.simd-report.v1","digest":"sha256:0c7487af...","bytes":2549,"payload":{...}}

For proofs, property tests and assurance policy see Shipping and Laws and proofs.

Describe a module for other systems

WIT and components. The compiler can derive a scalar WIT interface (semaprax:project-scalar@1.0.0) from a project’s web exports, but only as a library call. There is no command for it, and a Component binary exists only behind a private feature that is off by default. For WebAssembly use the Core Wasm web package (Targets). Specs: Public scalar WIT, private WIT boundary.

Java/Kotlin (JNI) and Swift/Apple bridges, and public generic signatures, stay private or unsupported in 0.9.0. The completion matrix gives each row’s status.

Serve one file

semaprax serve examples/meaning.spx

-> {"jsonrpc":"2.0","id":1,"method":"ping"}
<- {"jsonrpc":"2.0","id":1,"result":{"pong":true}}
-> {"jsonrpc":"2.0","id":2,"method":"context","params":{"symbol":"math.add","depth":1}}
<- {"jsonrpc":"2.0","id":2,"result":{"context":{"schema":"semaprax.agent-context.v1",...}}}
-> {"jsonrpc":"2.0","id":3,"method":"shutdown"}
<- {"jsonrpc":"2.0","id":3,"result":{"ok":true}}

serve checks one file once, then answers many newline-delimited JSON-RPC requests on stdin and stdout. Methods: protocol, graph, context, context_v2, ping, shutdown. Each result is byte-identical to the matching CLI command. A request without an id is a notification and gets no reply. For a whole project use semaprax service (Shipping).

Release archives also ship semapraxd. semapraxd --stdio [--manifest-path semaprax.toml] is the older project session: it authenticates one project once and answers graph, context and test requests over the same framing. Prefer service for new work. Specs: Agent Transport, Project Agent Transport v2.

@semaprax/agent-workflow (packages/semaprax-agent-workflow in a checkout) is a Node package that drives one bounded workflow, review then publish a function signature change, over a generated codec and an MCP transport your host supplies. It opens no files, starts no processes and holds no secrets.

Keep derived data

These commands store analysis on disk. Inputs are explicit, and what they restore carries no authority.

Spec: Retention metadata CLI.

Version and contributor gates

semaprax version --json
semaprax quality-plan quick

{"schema":"semaprax.version.v1","version":"0.9.0","commit":null,"maturity":"beta","rust_min":"1.88"}

commit is null for a build that recorded none. quality-plan quick|changed|full [changed-path ...] prints the gate list that the repository’s scripts/quality.sh runs for that profile. It is for people changing the compiler.

Next: What Semaprax verifies and what it does not.

What Semaprax verifies and what it does not

After this page you can read the output of the registry, audit, release and evidence commands without claiming more than they prove.

The commands themselves are in Shipping. This page states their trust limits in one place. The common rule: evidence is data, not permission. A digest binds exact bytes. A passing check says those bytes match what was checked. It never authorizes a write, a publication or a signature.

Table of limits

Read these four words

• authority: false or none. The document is information. Having it changes nothing you may do.
• nonclaims. A list of things the producer states it does not establish. Read it before you quote the result.
• Stale. The source or revision moved since the evidence was made. Re-run the producing command. Do not edit the evidence.
• Fail closed. The command stops with a code and writes nothing rather than guess.

What to say in a review

Say what the command proved, with its scope: “release verify re-hashed all five archives against release-manifest.json”, not “the release is signed”. When a capsule or release is unsigned, say unsigned. Local test evidence is local; hosted or physical-device evidence needs its own record. The same honesty applies to this handbook: where a feature is private, experimental or main-only, the page says so.

Specs: Audit Capsule v1, Release signing policy, Registry trust.

Cheatsheet

The language and the command line of Semaprax 0.9.0 on one page. Each row links to the page that explains it.

The daily loop

Run these in your project directory.

semaprax fmt .            # rewrite source to the one canonical form (--check only reports)
semaprax check .          # parse, resolve, type-check, verify
semaprax test .           # run the project's test functions
semaprax run .            # run main and print its i64 result
semaprax build . --target web -o dist/web

fmt writes files; fmt --check does not. check never runs your code; run and test do. For one file, semaprax fmt f.spx && semaprax run f.spx is the whole loop. Add --json to check, run or test for one JSON object per diagnostic.

Commands by task

Run semaprax help all for the full list, or see the Command catalog.

The language at a glance

Habits that fail: return, else if, x += 1, tuples, a[0], "a" + "b", Some(1), i++, break, as casts, macros. The fix for each is in Diagnostics.

A complete syntax reminder

module app.reminder;

@id("reminder.double")
fn double(value: i64) -> i64
    requires value >= 0
    ensures result == value * 2
{
    value * 2
}

@id("app.main")
fn main() -> i64
{
    let answer = double(21);
    if answer == 42 { answer } else { 0 }
}

Reading a command synopsis

Angle brackets name values to replace, square brackets are optional parts, and | means choose one. Do not paste the brackets into a shell. If a command says <input>, give it a .spx file, a project directory or semaprax.toml.

Need a word explained? Open the glossary.

Command catalog

Every semaprax command in 0.9.0, grouped by what you want to do, with the page that teaches it. semaprax help all prints the exact grammar of each command on your installed build; semaprax help <command> prints one.

<input> means a .spx file, a project directory or semaprax.toml. semaprax harness exists only in release archives and semaprax-full (Harness); everything else is in the standalone build.

Write, check and run

Inspect meaning

Change by meaning

Serve

Agents

Package, lock and ship

How far each of these is trusted: What Semaprax verifies.

Interfaces and analyses

Toolchain

Glossary

Use this page when a word stops you. Each entry says how the handbook uses the term and, where useful, where to learn more.

Return to: Essentials, project profiles or Agent programs.

Standard library

The standard library ships inside the compiler: no checkout, cache or network. You add a dependency, import by stable id, and set the project profile the package requires.

Find a function

Do not memorize names. Ask the installed compiler:

semaprax help library                    # the whole catalog, offline
semaprax help library compare            # one entry, about 200 bytes
semaprax help library std.core.compare   # by stable id

An entry shows the stable id, dependency row, required profile, signature, effects and contracts. The generated catalog is Standard library catalog; the machine-readable form is std/catalog.json.

Use a package in three steps

# 1. semaprax.toml: depend on the package
[dependencies]
std.core = "^0.1.0"

# 2. set the profile the entry requires (omit it for `scalar`)
[package]
profile = "owned-data-api.v1"

// 3. import by stable id, right after the module line
module app.using_std;

use function @id("std.core.min") from std.core as min;

Every bundled package is at version 0.1.0. An unknown package or an unsatisfied range fails with SPX-J121. If you call a standard-library name without importing it, the error prints the exact dependency and use lines to add (for example for min). Spell the type argument of generic calls (vec_push<i64>(...)). Pick the profile with Choose a project profile.

Every package

47 packages, all marked partial in the catalog: each works on the interpreter, native C11 and Core Wasm for its listed profile, and each has a conformance module. “Functions” counts declarations in the catalog entry.

scalar packages work in any project. Other profiles gate what a project may contain, for example std.fs needs filesystem-io.v3 and std.process needs process-io.v1, and those also need the matching effect and a provider that grants it (Input and output).

Traps

• Mutators thread the owner. Write let next = vec_push<i64>(values, x);; there is no in-place mutation.
• Most std.* packages are rule and parsing helpers over byte slices and scalars, not high-level clients. std.http parses messages; it does not open connections. For network access use the compiler-owned net_* and https_* functions (Built-in functions).
• Compiler-owned functions (string_len, byte_get, stdout_write, box_new) are not in the standard library. They are reserved names in every file.
• A stable id is <package>.<name>, for example std.core.min.

Contract: Standard Library v1.

Built-in functions

Compiler-owned functions are reserved names available in every file: no import, no dependency. Declaring your own string_len fails with SPX-S113. Spell every type argument. Every borrowed view takes a plain let binding.

Print the same table from your compiler with semaprax help language builtins. For library functions you import, see Standard library.

Strings

String views

Bytes and buffers

Vectors, iterators and boxes

T is one of the eight Copy scalars (i64, i32, u8, usize, f64, f32, bool, char).

Walk a vector with for item in values { ... } or consume an iterator with for own item in iterator { ... } (Loops).

Command I/O

Each needs its effect in permit and uses.

Single-file run admits stdout_write only. args_len, arg_utf8, stdin_read and stderr_write need a project with the useful-data-command.v1 profile on the native target. stdout_append and stderr_append belong to the line-command profile (line-command-io.v1).

Filesystem

Paths are bounded relative byte prefixes against a provider root the host injects. Writes create new files unless you use the atomic forms.

Network

Effect-gated operations that run only through a provider the host injects. A handle is a usize token valid for one invocation, at most 8 open at once.

The TLS and listener operations run only through the hosted provider on the interpreter; native and Wasm builds reject them before emission. https_get and https_post belong to the https-command-io.v1 profile. Try the network operations against recorded replies with semaprax network-run <project> --fixture fixture.json (Input and output).

Usage patterns for each family are in Ownership, Collections and Input and output. Specs: Network I/O, Network services, HTTPS client I/O.

Diagnostics reference

Every diagnostic carries a stable code, SPX- plus a family letter and digits. Match on the code, not the message wording. The letter says which part of the toolchain refused your input.

error[SPX-U103]: `mut` is only allowed on local `let` bindings; parameters are immutable at u103.spx:4:6
  help: drop `mut` and copy the parameter into a new mutable local: `let mut current = <parameter>;`

The help: line is usually the fix. Fix the first diagnostic first; later ones often follow from it.

Look a code up

help diagnostic indexes 24 codes, the mistakes people make most. For every other code, read the message and its help: line, then the spec for the feature. Codes are case-sensitive.

Common mistakes and fixes

Habits from other languages cause most first errors. The full habit table with runnable examples is in semaprax help language mistakes-code.