<!-- Sema documentation — Declarations & Keywords
     Sema is a new AI-native, neurosymbolic programming language most models
     have not been trained on. Full corpus: https://sema.49.12.246.95.sslip.io/llms-full.txt
     Install language support: https://sema.49.12.246.95.sslip.io/install-skill/ -->

# Declarations & Keywords

> When to use what — every Sema declaration form, modifier, and function-body clause, contrasted on one page.

Sema has roughly thirty declaration keywords. That is not vocabulary for its own
sake: each one replaces a piece of harness you would otherwise hand-roll —
a prompt builder, a retry loop, a config loader, a policy check. This page is
the contrast map: what each form declares, when to reach for it, and the
smallest legal spelling of each. Every example on this page parses with
`sema check` and runs under `SEMA_STRICT=1`.

The examples share one cast: a `writer` model, a `Note` struct, and friends —
so you can read any row against the others.

## The 30-second rule of thumb

- **Plain data** → `struct` (product) or `enum` (sum). The struct *is* the wire
  schema — there is no separate schema keyword.
- **A behavior contract over many types** → `trait`, conformed to with `impl`.
- **A computation you can write** → `def`.
- **A computation you can only describe** → `simulate def` — the model is the
  implementation, your contracts are the boundary.
- **Math as math** → `equation`. Pure by construction, `^` means power.
- **A model actor with tools and a budget** → `agent`.
- **Deterministic orchestration of agents** → `circuit`.
- **Authority — who may do what** → `policy`. Effects declare *what code can
  do*; policies decide *what is allowed*.
- **Declarative infrastructure** — prompts, config, DI, telemetry, events,
  remote interfaces — → the suite kinds (`template`, `context`, `config`,
  `container`, `collector`, `event`, `service`, …). Declare it; the runtime
  wires it.
- **Proof it works** → `test`, graded by `assure`.

## Top-level forms

Every cell in the **Minimal example** column is verbatim-verified. Nearly every
form accepts a Python-style one-line body; `equation` is the one exception
(block body required — footnote below).

| Form | Declares | Use when | Minimal example (one line) |
| --- | --- | --- | --- |
| **Callable** | | | |
| `def` | A function with typed params, effect row, contracts | Any computation you can write out | `def slug(title: str) -> str !{}: return title.strip().lower()` |
| `simulate def` | A function whose body a model provides | You can specify it, not implement it | `simulate def headline(article: str) -> str by writer: sem "A short, faithful headline"` |
| `stream def` | A generator producing `Stream[T]` via `yield` | Data that must never be resident at once | `stream def beats() -> Stream[int] !{}: yield 1` |
| `provide` | A DI factory with a lifetime (`transient`, `scoped(x)`, `singleton`) | Constructing a dependency for a `container` | `provide default_note() -> Note lifetime singleton: return Note(body="")` |
| `operator` | Overload of a fixed operator token for your types | Your type has a natural algebra | `operator +(a: Note, b: Note) -> Note !{}: return Note(body=a.body + b.body)` |
| `operator infix` | A custom string-named infix operator with a precedence class | The algebra has no built-in token | `operator infix "<~>" precedence add (a: str, b: str) -> str !{}: return a + " " + b` |
| `simulate operator` | An operator whose semantics a model provides | Semantic algebra — compose, remove meaning | `simulate operator -(a: str, b: str) -> str by writer: sem "Remove the meaning of b from a"` |
| `equation` | Pure math — `^` is power, no effects, CAS-backed | Formulas, symbolic work, `argmin`, proofs | `equation kinetic(m: any, v: any) -> any:` † |
| **Data & types** | | | |
| `struct` | A product type; doubles as the wire schema | Records, payloads, model output shapes | `struct Note: body: str` |
| `enum` | A sum type with variants | Closed sets of alternatives | `enum Grade: bronze \| silver \| gold` |
| `trait` | A behavior contract (methods + optional `law`s) | Shared behavior over unrelated types | `trait Renderer: def render(self) -> str` |
| `impl` | Conformance (`impl Trait for Type`) or inherent methods (`impl Type`) | Making a type satisfy a trait | `impl Renderer for Note: def render(self) -> str !{}: return self.body` |
| **Agents & orchestration** | | | |
| `agent` | A model actor: `sem` mission, `use tools`, `budget` | One model doing one job with bounded authority | `agent triager(note: str) -> str by writer: sem "Route the note to the right queue"` |
| `circuit` | Deterministic multi-agent orchestration with a shared budget | Fan-out/fan-in over agents, durable workflows | `circuit fan_out(notes: list[str]) -> list[str] !{model.invoke}: return parallel [triager(n) for n in notes]` |
| **Declarative suites** | | | |
| `policy` | Named authority: allow/forbid rules over effects | Confining what code (and models) may do | `policy Confined: allow clock` |
| `monitor` | Distribution tracking on a function's inputs/outputs | Keeping `statistical(α)` guarantees honest | `monitor headline_drift on headline: capture article, result` |
| `collector` | Typed telemetry channels fed by the `\|>` tap | Metrics without logging noise | `collector Metrics: latency: f32 mode series retention ring(1000)` |
| `protocol` | A session-type state machine | Legal orderings of a multi-turn exchange | `protocol Handshake: hello: str -> done` |
| `template` | A typed prompt builder returning `Prompt[T]` | Reusable prompts with roles and provenance | `template terse() -> Prompt[str]: role system: text "Be terse."` |
| `context` | A stateful prompt state machine over slots | Multi-turn model state with auditable diffs | `context Session: model writer` |
| `args` | The CLI as typed data | Flags and options without argparse plumbing | `args Cli: dry_run: bool = flag("--dry-run")` |
| `config` | A typed config tree with ordered sources | Files/env/CLI merged with validation | `config Limits: source env prefix "APP_"` |
| `container` | The dependency graph: `bind`, `expose` | Wiring providers to entrypoints | `container App: bind Runtime` |
| `component` | An injectable object with field injection | A bundle of dependencies passed as one value | `component Runtime: lifetime scoped(run)` |
| `service` | A typed remote interface at a named endpoint | Cross-process calls with visible remoteness | `service Scorer at endpoints.scorer: def score(text: str) -> f32` |
| `worker` | An execution profile for `parallel … by` | Tuning lanes and batching, not logic | `worker Pool: lane best_effort` |
| `event` | A typed domain signal | Decoupled reactions, journaled delivery | `event Spike: value: f64` |
| `subscriber` | A handler for an event with a queue policy | Reacting to events off the hot path | `subscriber log_spike on Spike: handle event: pass` |
| `bridge` | A membrane to foreign code (`python.inline`, `python.isolated`, `js.component`, `js.host`, `node.host`, `c.abi`, `cpp.abi`) | Calling Python/JS/C with contracts at the edge | `bridge python.inline features from "foreign/features.py": expose def word_count(text: str) -> int !{ffi.call}` |
| `model` | A pinned model binding as a first-class value | Naming the model a `by` clause refers to | `model writer = model("qwen3-4b-instruct", role=generator)` |
| **Verification** | | | |
| `test` | An executable spec run by `sema assure` | Every observable contract you rely on | `test "slug lowercases": ensure slug("A B") == "a b"` |
| `assure` | The module's verification grade (`bronze`/`silver`/`gold`) | Setting how much proof this module owes — at `silver` the checker starts *requiring* things, e.g. an `agent` must declare `budget model_calls=…` | `assure silver` |
| `policy attach` | Module-wide policy attachment | Confining a whole module at once | `policy attach Confined` |
| **Imports & constants** | | | |
| `import` | A Sema module, optionally aliased | Using another module's public names | `import std.cache as cache` |
| `from … import` | Selected names, optionally aliased | You want two names, not a namespace | `from std.collections import join_str` |
| `native import` | A bound foreign library — never translated | NumPy-class ecosystem dependencies | `native import python.isolated.json as pyjson` |
| `ported def` | Foreign source translated to Sema, gated by differential tests | Small self-contained algorithms worth owning | `ported def count_words(text: str) -> int from "vendor/wc.py": ensure result >= 0` |
| *(bare)* `NAME = expr` | A module constant | Shared literals | `MAX_RETRIES = 3` |

† `equation` is the only form that refuses a one-line body — the indented block
*is* the construct:

```sema
equation kinetic(m: any, v: any) -> any:
    return 1 / 2 * m * v^2
```

## Modifiers

| Modifier | Means | Legal on |
| --- | --- | --- |
| `pub` | Exported from the module; module-private is the default | Any top-level declaration (`pub def`, `pub struct`, `pub trait`, …) |
| `mut` | A rebindable local: `mut best = xs[0]` | Local bindings only. **`mut def` does not parse** — mutability is a property of bindings, not functions |
| `simulate` | The model is the implementation | `def`, `stream def`, `operator` |
| `stream` | The body is a generator; `yield` produces elements | `def` (also combined: `simulate stream def`) |
| `native` | Bind foreign code as-is over the C-ABI / embedded host — never translated | `import` |
| `ported` | Translate foreign source into Sema; the source stays the differential oracle | `def … from "path"`, `import "path" as name` |

## Inside a function body

### Contracts — four words, four different promises

```sema
def clipped(scores: list[f64], cap: f64) -> list[f64] !{}:
    require len(scores) > 0
    ensure len(result) == len(scores)
    out = [s if s < cap else cap for s in scores]
    ensure len(out) == len(scores)
    return out

struct Reading:
    celsius: f64 sem "Sensor temperature"
    invariant celsius >= -273.15
```

| Clause | Checked | On failure | Use for |
| --- | --- | --- | --- |
| `require` | At the **call boundary**, before the body runs. Boundary-only — it cannot appear mid-body | Blames the **caller**; typed `ContractViolation` | Preconditions on inputs |
| `ensure` | In signature position, over `result` after the body; mid-body, a sound assertion over locals | Blames the **callee**; the failed value cannot flow onward | Postconditions and mid-body proofs |
| `invariant` | On a `struct`, at every construction boundary | Construction fails, typed | Datatype invariants that must always hold |
| `check` | Evaluated, **never blocks** — graded evidence carried with the value | Nothing fails; the `Sim` verdict feeds `assure`, monitors, and repair | Soft properties; `check semantics("…")` for NL predicates |

The mnemonic: `require` guards the door, `ensure` signs the receipt,
`invariant` lives with the data, `check` takes notes.

Two `ensure`-position forms are **interpreted by the toolchain** rather than
evaluated as expressions. `ensure semantics("…", x, alpha=…)` is the calibrated
semantic postcondition (hard — fails as a `ContractViolation` carrying the
judge's evidence). `ensure total` is a signature-position **totality claim**:
for every argument satisfying the `require` clauses, the body terminates and
yields a value of the return type. It is for exact-arithmetic kernels —
arbitrary-precision `int`/`bool`/`str` and exact collections, an explicit `!{}`
row, no floats, no `while`, no recursion — with `//`, `%`, and indexing
licensed by `require` facts. `sema check` verifies the claim and module load
re-verifies it, both fail-closed: an unprovable claim is a loud **error**,
never a silent acceptance. A verified claim is statically discharged — `total`
is not a runtime value.

```sema
def mean_floor(xs: list[int]) -> int !{}:
    require len(xs) > 0      # domain refinement — licenses // len(xs)
    ensure total             # verified claim, statically discharged
    return sum(xs) // len(xs)

def main() -> int !{}:
    return mean_floor([3, 4, 8])   # 5
```

### Generative clauses — inside `simulate def` / `agent`

```sema
simulate def tag(note: str) -> str by writer:
    sem "A one-word topic tag for the note"
    use template terse()
    budget tokens=32, time="1s"
    repair retries=2, patch=fields
    ensure len(result) >= 1
    check semantics("tag names the dominant topic of the note")
```

| Clause | Does |
| --- | --- |
| `sem "…"` | The behavior specification the model implements — compiled prompt material, not a comment |
| `by <model>` | Binds the site to a declared `model` (header position) |
| `budget k=v, …` | Hard resource bounds: `tokens`, `time`, `model_calls`, `deadline`, … |
| `use template t(…)` / `use context C` / `use protocol P` / `use tools [f, g]` | Attach a prompt builder, stateful context, session type, or tool set |
| `repair retries=N, patch=fields` | The decode-and-repair ladder: feed typed defects back instead of resampling blind |

### Robustness

```sema
def robust(x: int) -> int !{code.patch}:
    supervise quick_cycle:
        restart limit=2
        fallback 0
        heal budget=1:
            require x > 0
            rollout shadow -> canary -> full
        return x * 2
    return 0

def parsed(raw: str) -> int !{}:
    expect value = int(raw):
        return value
    except ValueError as error:
        return -1
```

| Construct | Does |
| --- | --- |
| `supervise <scope>:` | A named recovery scope around the work; the triage ladder is language semantics |
| `restart limit=N` | Clean-state retry first — the cheapest honest recovery. `window="…"` is accepted and journaled but **not yet enforced**; `sema check` warns |
| `fallback <expr>` | Contract-declared degraded mode when restarts are exhausted — evaluated and journaled, its value is discarded, and execution continues after the block |
| `heal budget=N:` | Model-synthesized patch as the **last** rung. `budget=N` is **enforced**: at most N gauntlet attempts per scope entry (non-positive or non-integer budgets are a typed error). `window=`/`scope=` are journaled but not yet enforced — `sema check` warns. Gates are ordinary boolean `require` expressions |
| `rollout a -> b -> c` | Journal-recorded deployment stages of an accepted patch — meaningful only inside `heal:` (`sema check` warns elsewhere) |
| `expect …: / except E as x:` | Typed failure handling — consume a `ContractViolation`, `SemanticsViolation`, `BudgetExceeded` without a bare `try` |
| `scope:` | A structured nursery: every `spawn`ed child must finish inside it |

`lane` is a `worker`-profile clause (`worker Pool: lane best_effort` in the
top-level table), not supervise vocabulary. Neither `lane` nor `enter` has any
semantics inside a `def` body — they used to be silently accepted, and
`sema check` now flags both as unrecognized statements.

### Flow

```sema
def refine(query: str) -> str !{}:
    mut state = query
    mut confidence = 0.0
    loop until confidence >= 0.9 max_iters 8:
        state = state + "."
        confidence = confidence + 0.2
    return state

def pick_pair() -> int !{}:
    solve:
        var x in range(1, 10)
        var y in range(1, 10)
        constraint x + y == 10
        constraint x < y
    return x * y

def fan_out_pair(article: str) -> list[str] !{agent.spawn}:
    scope:
        a = spawn slug(article)
        b = spawn slug(article + "!")
    return [a.join()?, b.join()?]

def vetted(feedback: str) -> str !{}:
    note = validate f"Feedback: {feedback}":
        check len(value) > 0
    return note

def metered() -> int !{model.invoke}:
    mut calls = 0
    with meter as u:
        tag("solar output rose")
        calls = u.total_calls
    return calls
```

| Construct | Does |
| --- | --- |
| `loop until <cond> max_iters N:` | A convergence loop with an explicit bound — no unbounded agent loops |
| `parallel [f(x) for x in xs]` | Structured fan-out, fail-fast, ordered merge; variants: `parallel xs map x => x * 2 by Pool ordered`, `unordered`, `limit`, `on_error collect` |
| `spawn f(…)` | One structured child task; returns a `Task[T]` handle — consume with `.join()?`, stop with `.cancel()`. Needs `!{agent.spawn}` |
| `solve:` with `var x in <domain>` / `constraint <expr>` | Native finite-domain constraint search; `solve all:` enumerates into `solutions` |
| `validate <expr>:` | Gate a value through inline checks; the checked value is `value` |
| `breakpoint when <cond>` | Inert marker unless a debug session attaches — zero effect-row impact |
| `emit Spike(value=v)` | Publish a typed event to the journaled bus (effect `event.emit`) |
| `yield <expr>` | Produce the next stream element (only in `stream def`) |
| `with meter as u:` / `with budget(calls=1) as b:` / `with policy(P):` | Scoped observation, scoped hard cap, scoped authority shrink |
| `inject T` | Resolve a dependency from the active `container` (entrypoint decorated `@App`) |

## Suite-body directives

### `policy`

```sema
policy Scratch:
    allow:
        fs.read("config/**")
        clock
    forbid cap:
        code.exec, proc.spawn
        net.connect except "metrics.internal:443"
    examples:
        deny:
            code.exec("rm -rf /")
        allow:
            read_config("config/app.yaml")
    justification "Scratch data must never become execution authority."
    budget model_calls <= 100
```

| Directive | Does |
| --- | --- |
| `allow` | Grant effects, inline (`allow clock`) or block form with path/endpoint scopes |
| `forbid cap:` | Deny capabilities; `except "…"` carves out named endpoints |
| `examples:` with `allow:` / `deny:` | Executable documentation of intent — concrete calls that must (not) pass |
| `justification "…"` | The human reason, attached to every denial |
| `budget <dim> <= <lit>` | A policy-level resource ceiling |

### `monitor`

```sema
monitor tag_drift on tag:
    capture note, result
    baseline from assure
    test conformal_martingale(alpha=0.01)
    on drifted:
        alert("tag distribution drifted")
    on undecided:
        pass
```

| Directive | Does |
| --- | --- |
| `on <fn>` | (header) which function's call stream to watch |
| `capture a, b, result.path` | Which inputs/outputs feed the statistic |
| `baseline from assure` / `baseline "calsets/…@v2"` | Where the reference distribution comes from |
| `test conformal_martingale(alpha=…)` | The drift statistic and its confidence level |
| `on drifted:` / `on undecided:` | Deterministic reactions — emit an event, alert, degrade |

### `bridge`

```sema
bridge python.isolated title_glue:
    deps "python>=3.12,<3.13"
    expose def normalize_title(raw: str) -> str !{ffi.call}:
        sem "Normalize title whitespace"
        ensure len(result) > 0
    begin python
        def normalize_title(raw):
            return " ".join(raw.split())
    end python
```

| Directive | Does |
| --- | --- |
| `expose def …` | The only callable surface — full Sema types, effects, contracts at the membrane |
| `begin <lang> … end <lang>` | Inline foreign source (alternative: `from "path"` in the header) |
| `deps "…"` | Foreign dependency pins |
| `symbol "…"` | Foreign symbol name mapping — **`c.abi` bridges only** (the runtime rejects it elsewhere) |
| `link "…" / checksum` | Prebuilt-artifact binding for `c.abi`, SHA-256 verified (§5.10) |

### `container`

```sema
container QuickApp:
    args QuickCli
    config QuickConfig
    bind QuickRuntime lifetime scoped(run)
    expose app_entry
```

| Directive | Does |
| --- | --- |
| `args A` / `config C` | Attach the typed CLI and config tree |
| `bind T [named "…"] [lifetime …] [= provider(…)]` | One binding per `(type, qualifier)`; ambiguity is a compile error |
| `expose f` | Which entrypoints this container serves (`@QuickApp def app_entry…`) |

### `template`

```sema
template quick_system(domain: str) -> Prompt[str]:
    role system:
        text f"You are a precise assistant for {domain}."
```

| Directive | Does |
| --- | --- |
| `role <name>:` | A typed role block (`system`, `developer`, `user`, `assistant`, `tool`, `data`) |
| `text <expr>` | A line of prompt content; f-strings, `if`/`for`/`match` allowed around it |

## Common confusions

- **`require` vs `check`** — `require` is a hard gate at the call boundary:
  fail and the call never runs. `check` never blocks anything; it records
  graded evidence. If a violation must stop the program, it is not a `check`.
- **`ensure` vs `test`** — `ensure` lives *in* the function and guards every
  call at runtime. `test` lives *outside* and proves behavior at `assure`
  time. `ensure` is a seatbelt; `test` is the crash test.
- **`policy` vs the effect row** — `!{fs.read}` declares what a function *can
  do*; `policy` decides what is *allowed*. Rows are facts, policies are law:
  the same code can be legal under one policy and denied under another.
- **`agent` vs `circuit` vs `service`** — an `agent` is one model actor with a
  mission and budget. A `circuit` is deterministic code that orchestrates
  agents under a shared budget. A `service` is not generative at all — it is a
  typed interface to another process. Model work goes in agents; control flow
  in circuits; process boundaries behind services.
- **`template` vs `context`** — a `template` is a pure, stateless prompt
  builder. A `context` is a state machine over prompt slots with typed
  transitions. One render vs a conversation.
- **`struct` vs `config`** — both are typed records, but `config` adds ordered
  sources (files, env, CLI), provenance, and redaction. Data your program
  computes is a `struct`; data your deployment supplies is a `config`.
- **`def` vs `provide`** — `provide` is a `def` with a lifetime, registered
  for injection. If callers should say `inject T` rather than call you, you
  are a `provide`.
- **`monitor` vs `collector`** — a `monitor` answers "has this distribution
  shifted?" and can demote guarantees when unwatched. A `collector` just
  records typed telemetry via the `|>` tap. Monitors have verdicts; collectors
  have retention.
- **`event`/`subscriber` vs calling a function** — `emit` decouples in time
  and authority: delivery is queued, journaled, and policy-checked. If the
  reaction must happen before the next line runs, call the function.
- **`native import` vs `ported def` vs `bridge`** — `native import` binds a
  living ecosystem library; `ported def` *translates* a small algorithm into
  Sema (differential-tested against its source, then it is ordinary Sema);
  `bridge` is the general membrane when you author the foreign side yourself.

## Next

- [Cheat Sheet](/quick/cheat-sheet/) — the whole surface at a glance.
- [Architecture & Best Practices](/quick/architecture/) — how these forms
  compose into a program.
- [Construct catalog](/reference/language-spec/05-construct-catalog/) — the
  full specification per construct.