# Contracts and refinements

URL: /docs/tour/contracts
Markdown: /docs/tour/contracts.md

> Refinement types, requires and ensures clauses, and the honest guarantee model behind them.

> **Pre-alpha**
>
> The source-built compiler runs the core language and much of M3 on JavaScript: contracts, typed effects and failures, std handlers, permissions, LSP and MCP. M3 is still in progress; no release or stable compatibility contract exists. See the [roadmap](/docs/roadmap) for implemented features and remaining gates.

Types say what shape a value has. Refinements and contracts say what is true about it. Both are part of the signature, so both are what a reviewer reads.

## The guarantee model [#the-guarantee-model]

Every claim Sakura Lang makes about a program has exactly one of four statuses ([design §1.2](https://github.com/icantcodefyi/sakura-lang/blob/master/docs/design.md)):

| Status            | Meaning                                                                                | Who establishes it                                                            |
| ----------------- | -------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------- |
| `proved`          | Holds on all executions under the stated assumptions.                                  | The type and effect checker; later, SMT-discharged contracts.                 |
| `runtime_checked` | A violation is detected at the boundary and becomes a defect. The bad value never escapes. | Contract lowering (`requires`, `ensures`, `where`), checked arithmetic.        |
| `tested`          | Held on the inputs that were executed.                                                 | `sakura test` (unit, property, snapshot, simulation).                            |
| `trusted`         | Assumed.                                                                               | FFI declarations, host handlers, `@trust` sites, the toolchain itself.        |

The current build manifest labels contract obligations `runtime_checked`. Scalar literals can already be decided at compile time; this is a bounded evaluator, not the planned SMT verifier. The compiler never prints "verified" for a program that merely compiled.

## Refinement types [#refinement-types]

A refinement is a base type plus a predicate, written with `where`. Inside the predicate, `it` is the value.

```sakura
type Email = String where String.len(it) <= 254 && String.contains(it, "@")
type Percent = Int where it >= 0 && it <= 100
type NonEmpty<T> = List<T> where List.len(it) > 0
```

A refined type is a distinct nominal type with the same representation as its base. It coerces implicitly to the base, so a `Percent` is usable wherever an `Int` is expected. The reverse requires validation or `from`, except for scalar literals in a refined position, described below.

Record fields can carry a refinement inline:

```sakura
type Priority = Low | Normal | High
type Ticket = {
  title: String where String.len(it) > 0 && String.len(it) <= 120,
  priority: Priority,
}
```

Field refinements are checked when the record is constructed.

## How values enter a refined type [#how-values-enter-a-refined-type]

A value becomes a `Percent` in one of four ways ([design §4.3](https://github.com/icantcodefyi/sakura-lang/blob/master/docs/design.md)):

| Entry point                               | On failure                                                        |
| ----------------------------------------- | ----------------------------------------------------------------- |
| `Percent.validate(n) -> Result<Percent, Violation>` | Returns `Err(Violation { type_name, clause, value_summary })`. |
| `Percent.from(n) -> Percent`               | Defect `D010`. Use at trusted boundaries only; [`sakura audit`](/docs/agents/audit) lists explicit calls. |
| `let p: T = Json.decode(text)?` and other schema decoding, with the target named by annotation | Typed `DecodeError`, never a defect. Nested field refinements are checked. |
| A literal, `let p: Percent = 50`          | Decided by the bounded scalar evaluator when possible (`V5004` on rejection); otherwise checked once before `main`, without a warning. |

`validate` is the normal path for input you do not control:

```sakura
type Percent = Int where it >= 0 && it <= 100

fn describe(input: Int) -> String {
  match Percent.validate(input) {
    Ok(p) => "{p}%",
    Err(_) => "out of range",
  }
}
```

Once a value has type `Percent`, nothing downstream re-checks it. Sakura Lang has no aliasable mutation, so a validated value cannot be invalidated later. Record update `Ticket { ..t, title: x }` with `x` already refined needs no re-check.

## Literal refinements at compile time [#literal-refinements-at-compile-time]

The checker evaluates scalar `Int`, `Float`, `String` and `Bool` literals against their target refinement with a deterministic **10,000-step budget per literal** (design §17.87). It supports scalar arithmetic and comparisons, short-circuit booleans, `if`/`let`/blocks, pure functions in that fragment and the string built-ins `len`, `contains`, `starts_with` and `ends_with`. `String.len` counts UTF-8 bytes.

- **True:** the literal is accepted without a startup conversion.
- **False or an evaluable defect:** `V5004`, with the literal and refinement definition identified. For example, `let p: Percent = 150` is rejected.
- **Undecidable:** the literal is checked once at module initialization. A failed predicate produces `D010` before `main`, even when the literal is inside a function that would run later. There is no warning.

The evaluator is deliberately smaller than the contract subset. `match`, collection operations such as `String.split`, and exceeding the step budget leave a runtime check. An intermediate integer beyond JS's safe range but within i64 is also undecidable because backends differ. `V5002` is retired and never emitted; its explain page remains for old reports.

Current audit output omits undecided literal conversions too, although the design requires `reason: "literal"` records. See the [audit limitation](/docs/agents/audit#literal-conversion-limitation).

## Validating untrusted input [#validating-untrusted-input]

`Untrusted.validate` is implemented. Its target must be a known refined type over the wrapped base; an unknown target, plain type, wrong base, or using the function as a value produces `V5003`. Name the target with an annotation:

```sakura
import std/core.{Violation}

type Percent = Int where it >= 0 && it <= 100

fn read_percent(raw: Untrusted<Int>) -> Result<Percent, Violation> {
  Untrusted.validate(raw)
}

test "untrusted input is checked" {
  expect_eq(read_percent(Untrusted.of(50)), Ok(Percent.from(50)))
  expect(read_percent(Untrusted.of(150)).is_err())
}
```

This checks the refinement and returns `Err(Violation)` on failure; it does not silently trust the input.

## The contract subset [#the-contract-subset]

Predicates in `where`, `requires`, `ensures`, and `property` clauses must be pure (`! {}`), terminating, and deterministic. v0 enforces this syntactically ([design §7.1](https://github.com/icantcodefyi/sakura-lang/blob/master/docs/design.md)):

- No loops and no recursion.
- Calls only to functions with row `{}` that are marked `@total` or are themselves in the subset, checked transitively. Anything else is `V5001`.
- Allowed: comparison, checked arithmetic, `&&`, `||`, `!`, field and tuple access, `match` on finite variants, `List.len`, `String.len`, and bounded quantifiers `List.all(xs, fn(x) { … })` and `List.any`.

Arithmetic in a predicate is checked, so a predicate can itself defect. That is reported as `D011` (contract evaluation failed).

`@total` is how a function with recursion or a loop reaches a contract. It is a **trusted** claim that a `{}`-row function terminates on every input; the compiler does not prove it. Std marks a fixed list (`List.len`, `List.get`, `List.all`, `List.any`, `List.contains`, `Map.get`, `String.len`, `String.contains`, `Option.is_some`, `Int.abs`, and a few more). User code may mark its own functions, and [`sakura audit`](/docs/agents/audit) lists every user `@total` site, like every `@trust`:

```sakura
@total   // trusted: n / 10 moves toward 0 on every call
fn digits(n: Int) -> Int {
  if n > -10 && n < 10 { 1 } else { 1 + digits(n / 10) }
}

type Pin = Int where it >= 0 && digits(it) == 4
```

## Preconditions and postconditions [#preconditions-and-postconditions]

`requires` states what must hold for the arguments. `ensures` states what holds for the result, which is bound to `result`. Both go between the signature and the body, and each clause may have a name.

```sakura
fn clamp(x: Int, lo: Int, hi: Int) -> Int
  requires ordered: lo <= hi
  ensures bounded: lo <= result && result <= hi
{
  if x < lo { lo } else if x > hi { hi } else { x }
}
```

- `requires` is checked on entry. A violation is a **caller defect** `D020`, with blame on the call site and the clause name in the report.
- `ensures` is checked once on normal return. A violation is a **callee defect** `D021`. It is never checked when the function fails or defects, because there is no `result`.
- There is no `old(expr)`. Arguments are immutable values, so a parameter named in `ensures` is exactly the value that was passed in.

Contracts compose with typed errors:

```sakura
error Insufficient
error Frozen
type WithdrawError = Insufficient | Frozen

type Account = { id: Uuid, balance: Int, frozen: Bool }

fn withdraw(from: Account, amount: Int) -> Account ! {Fail<WithdrawError>}
  requires positive: amount > 0
  ensures same_account: result.id == from.id
  ensures debited: result.balance == from.balance - amount
  ensures non_negative: result.balance >= 0
{
  if from.frozen { fail Frozen }
  if amount > from.balance { fail Insufficient }
  Account { ..from, balance: from.balance - amount }
}
```

`Frozen` and `Insufficient` are expected failures in the error union. A negative `amount` is a bug in the caller, so it is a precondition, not an error tag.

Bounded quantifiers are allowed in contracts:

```sakura
type NonEmptyScores = List<Int> where List.len(it) > 0

fn top_score(scores: NonEmptyScores) -> Int
  ensures List.all(scores, fn(s) { s <= result })
{
  let first = List.first(scores).expect("NonEmpty has a first element")
  List.fold(scores, first, fn(best, s) { Int.max(best, s) })
}
```

`W5005` warns once per user clause calling `List.all`, `List.any` or `List.contains` on a parameter or `it`. This includes `requires`, `ensures`, `where` and property `requires`; there is no hot-path analysis. Std clauses are exempt. `String.contains` no longer triggers the warning (design §17.90), so the `Email` refinement above is quiet.

## Contracts are always checked [#contracts-are-always-checked]

The current JS build retains runtime contracts; there is no `--release` flag in the CLI. Decided literal introductions need no runtime conversion. Future `sakura verify` (M4) may remove an individual check only with a matching `proved` result.

Contract violations are [defects](/docs/tour/effects), not effects. A defect terminates the current task after resource finalizers run. `try` cannot catch it. `Task.scope` and the test runner observe it as an outcome, and a defect in `main` exits with status 70 and a structured report.

Contracts on `pub` functions are part of the signature shown by [`sakura doc`](/docs/agents/doc), the MCP `symbol_query` tool, and editor hover.

## Frozen specs during agent repair [#frozen-specs-during-agent-repair]

An agent fixing a failing build must not "fix" it by weakening the specification. `sakura fix`, the MCP `apply_patch` tool, and `sakura check --frozen-specs <symbols|all>` reject any patch that changes a frozen symbol's signature, effect row, error union, `requires`/`ensures`/`where` clauses, or any `test` or `property` body. The diagnostic is `V8020` (spec frozen) and names the clause.

Compiler fixes that touch a contract carry `impact: contract_change` and are never `machine_applicable`. See [Diagnostics](/docs/agents/diagnostics).

## Property tests from contracts [#property-tests-from-contracts]

`--contracts` is not present in the current `sakura test --help`. The planned command will synthesize a property test for every `pub` function that has a refined parameter or a `requires` clause. Inputs are generated from the refinements and `requires` together, the function runs under the test handlers, and `ensures` and result refinements are checked. Failures are shrunk and saved. A function with effects other than `Fail`, `Clock`, and `Random` is tested only when it names handlers with `@contract_test(handlers: [Sql.memory(), Log.captured()])`. See [Testing](/docs/tour/testing#property-tests-from-contracts-planned).

## Not in v0 [#not-in-v0]

- **Static proof.** M4 adds `sakura verify`, which sends obligations in the QF_LIA, QF_BV, and EUF fragments to Z3 and reports `proved`, `disproved` (with a counterexample), `unknown`, or `unsupported`. Only `proved` removes a runtime check. Termination is never implied ([design §7.5](https://github.com/icantcodefyi/sakura-lang/blob/master/docs/design.md)).
- **Flow-sensitive refinement.** An `if n >= 0` does not turn `n` into a refined type. Use `validate` or `from`.
- **`old(expr)`** in postconditions. There is no mutation to snapshot.
- **Proof-oriented syntax.** The keywords `verify`, `proof`, and `ghost` are reserved and rejected today with `V0007`.

## Next [#next]

[Testing](/docs/tour/testing): unit tests, property tests, snapshots, and deterministic handlers.