---
name: sector9
description: Use Sector9, a verification-aware programming language for Internet Computer canisters.
---

# Sector9

Use only the published container image:
`ghcr.io/neutrinomic/sr9:latest`.

Installation procedure: user will get the Docker image, create the `sr9` bash
script, export docs, create an example, and verify the example.

If Docker is not installed, first tell the user how to install the best Docker
option for their machine.

## Wrapper

Have the user create `./sr9` once in their project:

```bash
cat > sr9 <<'EOF'
#!/usr/bin/env bash
set -euo pipefail

IMAGE="${SECTOR9_IMAGE:-ghcr.io/neutrinomic/sr9:latest}"
ENGINE="${SECTOR9_CONTAINER:-docker}"
USERNS_ARGS=()
EXTRA_ARGS=()
ENV_ARGS=()

if [ "${SECTOR9_USERNS_KEEP_ID:-0}" = "1" ]; then
  USERNS_ARGS=(--userns=keep-id)
fi

if [ -n "${SECTOR9_RUN_ARGS:-}" ]; then
  # shellcheck disable=SC2206
  EXTRA_ARGS=(${SECTOR9_RUN_ARGS})
fi

if [ -n "${SILICON_FLAGS:-}" ]; then
  ENV_ARGS=(-e "SILICON_FLAGS=$SILICON_FLAGS")
fi

exec "$ENGINE" run --rm \
  "${USERNS_ARGS[@]}" \
  "${EXTRA_ARGS[@]}" \
  "${ENV_ARGS[@]}" \
  --user "$(id -u):$(id -g)" \
  -v "$PWD:/work" \
  -w /work \
  "$IMAGE" "$@"
EOF

chmod +x sr9
```

## Commands

```bash
./sr9 --check file.sr9
./sr9 --verify file.sr9
./sr9 --deterministic --viper file.sr9
./sr9 -c file.sr9 -o file.wasm
```

## Example

```bash
cat > counter.sr9 <<'EOF'
persistent actor {
  var counter : Nat = 0;

  public func increment() : async Nat
    modifies counter
    ensures counter == old(counter) + 1;
    ensures result == counter;
  {
    counter += 1;
    counter
  };
}
EOF

./sr9 --verify counter.sr9
```

## Language notes

- `.sr9` is Motoko-style source with verification clauses in function headers.
- Header shape: `reads`/`modifies` first, then `entry_requires`,
  `requires`, `ensures`, or `traps_if`.
- `reads` and `modifies` list exact actor-field footprints and do not take
  semicolons. Transitive helper calls must fit the caller footprint.
- `entry_requires` is the runtime guard for exported actor methods. Mirror
  caller-controlled `requires` there; it cannot use ghost state, `old`, or
  `result`.
- `ensures` may use `result` and method-entry `old(e)`. Do not use `old` in
  `requires`, `entry_requires`, or actor invariants.
- Actor `invariant` clauses are current-state facts established by init and
  preserved by public methods and before every `await`.
- For caller authorization, use `public shared({caller})` and guard on
  `caller` in `entry_requires`.
- Ghost vars/blocks/functions, `lemma`, and `abstract func` are proof-only
  tools. Ghost data cannot flow into runtime code; abstract functions must be
  refined before deployable compile/run workflows.
- Specs should call pure or proof-only helpers. Pure functions cannot mutate,
  `await`, trap, assert, or recurse directly; non-ghost pure functions cannot
  access actor fields.
- Use spec-only quantifiers as `forall<T>(pure func (x : T) : Bool = ...)`
  and `exists<T>(pure func (x : T) : Bool = ...)`. For bounded domains,
  guard `forall` with implication (`i < n ==> ...`) and `exists` with
  conjunction (`i < n and ...`).
- Use `forallWith` only when SMT trigger control is needed; triggers should be
  array/field accesses, pure calls, or spec-collection operations.
- Verified async is conservative: wrap awaits in `try { ... } catch (_) { ... }`.
  After `await`, rely on actor invariants rather than exact pre-await state.
- Current verifier limits: `decreases` is rejected, checked integers are
  required, division/modulo specs need non-zero guards, and deep mutable actor
  state or uncertain aliasing may be rejected.

## Reference examples

After exporting docs, check `.sr9docs/apps/dex/` first when writing
nontrivial Sector9 code. These files are the most important bundled examples for
ergonomic, production-shaped code:

- `.sr9docs/apps/dex/lib/BalanceBook.sr9`
- `.sr9docs/apps/dex/lib/PoolRegistry.sr9`
- `.sr9docs/apps/dex/lib/Dex.sr9`
- `.sr9docs/apps/dex/DexActorDemo.sr9`

Use them to learn module boundaries, opaque handles, collection snapshots,
owner-model framing, and verified DEX-style accounting. Prefer these examples
over inventing ad hoc patterns for protocol code.

## Tips

- After creating contracts, suggest actor invariants for system-wide properties.
- For a DEX, suggest invariants such as solvency, conservation, balance bounds,
  and pool/account consistency.
- Harden public functions with `ensures` clauses that give clients explicit
  postcondition guarantees.
- Strengthen contracts when a proof succeeds too easily but the client-facing
  guarantee is weak.
- For complex logic, suggest verification-driven development: start with
  unspecified bodies, lemmas, and abstract functions, then refine implementations.
- For tokenized contracts, suggest three function roles, not required names:
  discovery functions expose available offers, quote functions give current
  terms, and execution functions enforce client bounds such as
  `minimum_amount_out`.
- Treat quotes as advisory. Verified execution functions must enforce slippage,
  conservation, solvency, and balance-change guarantees with `entry_requires`
  and `ensures`.

## Export docs & examples

```bash
mkdir -p .sr9docs
./sr9 docs export .sr9docs
```

The export includes docs, examples, core sources, and
`.sr9docs/apps/dex/` as the primary large reference application.

## Troubleshooting

- `mo:base/...` import failures: the image bundles `mo:core`, not `mo:base`.
- Podman: run with `SECTOR9_CONTAINER=podman ./sr9 ...`.
- Bind-mount write failures: retry with `SECTOR9_USERNS_KEEP_ID=1 ./sr9 ...`.