Proving

Contracts describe what is true if a function returns. requires is a caller obligation; ensures binds result. Opaque types may declare invariant. spec fn and lemma fn are erased helpers. decreases proves Gale recursion terminates. gale verify (or mix gale.verify) discharges these claims. Compilation does not. Proofs do not mean a process is alive or a message was delivered.

mod proving

pub fn increment(x: Integer) -> Integer
requires { x >= 0 }
ensures { result == x + 1 }
{
  x + 1
}

pub opaque type State = %{reserved: Integer, capacity: Integer}
invariant(state) {
  state.reserved >= 0 and state.reserved <= state.capacity
}

pub fn new(capacity: Integer) -> Result<State, :invalid> {
  if capacity >= 0 {
    Ok(%{reserved: 0, capacity: capacity})
  } else {
    Error(:invalid)
  }
}

pub fn available(state: State) -> Integer
ensures { result >= 0 }
{
  state.capacity - state.reserved
}

pub fn zero(x: Integer) -> Integer
requires { x >= 0 }
ensures { result == 0 }
decreases { x }
{
  if x == 0 {
    0
  } else {
    zero(x - 1)
  }
}

pub spec fn nonnegative(value: Integer) -> Boolean {
  value >= 0
}

pub lemma fn successor(value: Integer) -> :ok
requires { nonnegative(value) }
ensures { nonnegative(value + 1) }
{
  :ok
}

pub fn step(value: Integer) -> Integer
requires { nonnegative(value) }
ensures { nonnegative(result) }
{
  proof { successor(value) }
  value + 1
}

requires is an obligation for callers and an assumption while checking the body. ensures is an obligation on every normal return. result has the declared return type. A false contract still typechecks; mix compile is not a proof. Opaque construction and updates must establish the invariant.

spec fn and lemma fn are erased. Ordinary code cannot call them. A proof block can use a lemma, then continues with a runtime expression. decreases asks for a termination proof of Gale recursion. Server loops and GenServer callbacks stay partial: if they return, their contracts hold.

Extern requires/ensures are trusted as written. Callers prove preconditions, inhabit the declared return type, and assume postconditions. Uncontracted foreign calls are not specification evidence:

extern "System.unique_integer" fresh() -> Integer

pub fn client() -> Integer
ensures { fresh() >= 0 }
{
  0
}

gale check / mix gale.check typecheck annotations without solvers. gale verify / mix gale.verify prove them with Why3 and Z3. Successful units are reused from .gale/proofs. Proofs cover Gale code that returns normally. They do not imply process survival or message delivery.