Contracts and refinements

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 modelCopy Anchor Link

Every claim Sakura Lang makes about a program has exactly one of four statuses (design §1.2):

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 typesCopy Anchor Link

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

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:

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 typeCopy Anchor Link

A value becomes a Percent in one of four ways (design §4.3):

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

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 timeCopy Anchor Link

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.

Validating untrusted inputCopy Anchor Link

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:

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 subsetCopy Anchor Link

Predicates in where, requires, ensures, and property clauses must be pure (! {}), terminating, and deterministic. v0 enforces this syntactically (design §7.1):

• 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 lists every user @total site, like every @trust:

@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 postconditionsCopy Anchor Link

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.

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:

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:

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 checkedCopy Anchor Link

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, 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, the MCP symbol_query tool, and editor hover.

Frozen specs during agent repairCopy Anchor Link

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.

Property tests from contractsCopy Anchor Link

--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.

Not in v0Copy Anchor Link

• 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).
• 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.

NextCopy Anchor Link

Testing: unit tests, property tests, snapshots, and deterministic handlers.