State invariants

A type can say which fields state contains. An invariant can say which combinations are valid. This example proves 0 <= reserved <= capacity for every state its GenServer can construct through Gale.

A quota state whose reserved amount is always between zero and capacity.

Every constructor and transition is checked by F*/Z3 during compilation. Outside this module, the opaque State can only be obtained from these verified functions. A GenServer can therefore store State without exposing its fields.

module invariants.quota_state

@moduledoc """
A quota state whose reserved amount is always between zero and capacity.

Every constructor and transition is checked by F*/Z3 during compilation.
Outside this module, the opaque State can only be obtained from these verified
functions. A GenServer can therefore store State without exposing its fields.
"""

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) }
}

fn add_nonnegative(a: Integer, b: Integer) -> Integer
requires { b >= 0 }
ensures result { result == a + b } {
  a + b
}

pub fn reserve(state: State, amount: Integer) -> Result<State, :invalid> {
  if amount >= 0 and amount <= state.capacity - state.reserved {
    Ok(state {reserved: add_nonnegative(state.reserved, amount)})
  } else { Error(:invalid) }
}

pub fn release(state: State, amount: Integer) -> Result<State, :invalid> {
  if amount >= 0 and amount <= state.reserved {
    Ok(state {reserved: state.reserved - amount})
  } else { Error(:invalid) }
}

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

A GenServer whose state carries a compile-time quota invariant.

Callbacks handle messages and replies; quota_state owns the pure transitions. Rejected reservations return an error and keep the previous valid state. This proves a property of the state, not delivery, liveness, or crash freedom.

module invariants.quota

@moduledoc """
A GenServer whose state carries a compile-time quota invariant.

Callbacks handle messages and replies; quota_state owns the pure transitions.
Rejected reservations return an error and keep the previous valid state.
This proves a property of the state, not delivery, liveness, or crash freedom.
"""

implements gale_std.gen_server.Server<
  Integer,
  invariants.quota_state.State,
  Request,
  Never,
  Never,
  Never
> as service

pub type Request =
  | Available(reply_to: gale_std.gen_server.ReplyTo<Integer>)
  | Reserve(amount: Integer, reply_to: gale_std.gen_server.ReplyTo<Result<Integer, :invalid>>)
  | Release(amount: Integer, reply_to: gale_std.gen_server.ReplyTo<Result<Integer, :invalid>>)

pub type Service = service
pub type Target = gale_std.gen_server.ServerTarget<Service>

pub fn start_link(capacity: Integer) -> gale_std.gen_server.StartResult<Service> {
  gale_std.gen_server.start_link(invariants.quota, capacity, [])
}

pub fn available(server: Target) -> Integer {
  gale_std.gen_server.call(server, fn(reply_to) => Available(reply_to))
}

pub fn reserve(server: Target, amount: Integer) -> Result<Integer, :invalid> {
  gale_std.gen_server.call(server, fn(reply_to) => Reserve(amount, reply_to))
}

pub fn release(server: Target, amount: Integer) -> Result<Integer, :invalid> {
  gale_std.gen_server.call(server, fn(reply_to) => Release(amount, reply_to))
}

pub fn init(capacity: Integer) -> gale_std.otp.Init<invariants.quota_state.State, Never> {
  match invariants.quota_state.new(capacity) {
    Ok(state) -> (:ok, state)
    Error(reason) -> (:stop, reason)
  }
}

fn finish(
  old: invariants.quota_state.State,
  next: Result<invariants.quota_state.State, :invalid>,
  reply_to: gale_std.gen_server.ReplyTo<Result<Integer, :invalid>>
) -> gale_std.otp.Next<invariants.quota_state.State, Never> {
  match next {
    Ok(state) -> {
      let _ = gale_std.gen_server.reply(reply_to, Ok(invariants.quota_state.available(state)))
      let result: gale_std.otp.Next<invariants.quota_state.State, Never> = (:noreply, state)
      result
    }
    Error(reason) -> {
      let _ = gale_std.gen_server.reply(reply_to, Error(reason))
      let result: gale_std.otp.Next<invariants.quota_state.State, Never> = (:noreply, old)
      result
    }
  }
}

pub fn handle_call<R>(
  build: fn(gale_std.gen_server.ReplyTo<R>) -> Request,
  from: gale_std.gen_server.ReplyTo<R>,
  state: invariants.quota_state.State
) -> gale_std.otp.Next<invariants.quota_state.State, Never> {
  match build(from) {
    Available(reply_to) -> {
      let _ = gale_std.gen_server.reply(reply_to, invariants.quota_state.available(state))
      let result: gale_std.otp.Next<invariants.quota_state.State, Never> = (:noreply, state)
      result
    }
    Reserve(amount, reply_to) -> finish(state, invariants.quota_state.reserve(state, amount), reply_to)
    Release(amount, reply_to) -> finish(state, invariants.quota_state.release(state, amount), reply_to)
  }
}

Remove the capacity check in reserve and compilation fails. Add another ordinary state factory and its result is checked automatically. Construct a raw record in the callback and return it as quota_state.State, and ordinary typechecking fails. The state guarantee therefore survives the boundary between verified pure code and an effectful OTP callback.

Calls may still time out, processes may crash, and foreign code must respect Gale’s typed interface. The proof does not establish liveness, message delivery, or the correctness of handwritten Elixir that bypasses the opaque API.

Proofs cover ordinary functions and effects, including supported recursive helpers. See the proof reference for the supported subset and trust boundary.

Building on dependency contracts

The same project contains a bounded queue. Its invariant observes native list length with builtin.length. Enqueue calls gale_std append using its declared length contract, and reverse uses its length-preservation contract. The application build checks the state transitions against those library interfaces; the native implementations remain trusted externs.

A bounded queue verified against standard-library contracts.

module invariants.queue_state

@moduledoc """
A bounded queue verified against standard-library contracts.
"""

pub opaque type State = { items: List<Integer>, capacity: Integer }
invariant state {
  builtin.length(state.items) <= state.capacity
}

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

pub fn enqueue(state: State, value: Integer) -> Result<State, :full> {
  if builtin.length(state.items) < state.capacity {
    Ok(state {items: gale_std.list.append(state.items, [value])})
  } else { Error(:full) }
}

pub fn reverse(state: State) -> State {
  state {items: gale_std.list.reverse(state.items)}
}

pub fn size(state: State) -> Integer
ensures result { result >= 0 } {
  builtin.length(state.items)
}

pub fn first(state: State) -> Option<Integer> {
  gale_std.list.first(state.items)
}

pub fn enqueue_and_notify(
  state: State,
  value: Integer,
  observer: gale_std.process.Pid<Integer>
) -> Result<State, :full> {
  match enqueue(state, value) {
    Ok(next) -> {
      let _ = gale_std.process.send(observer, size(next))
      Ok(next)
    }
    Error(reason) -> Error(reason)
  }
}

pub fn enqueue_and_reply(
  state: State,
  value: Integer,
  reply_to: gale_std.gen_server.ReplyTo<Result<Integer, :full>>
) -> State
ensures result { result.capacity == state.capacity } {
  match enqueue(state, value) {
    Ok(next) -> {
      let _ = gale_std.gen_server.reply(reply_to, Ok(size(next)))
      next
    }
    Error(reason) -> {
      let _ = gale_std.gen_server.reply(reply_to, Error(reason))
      state
    }
  }
}

enqueue_and_notify and enqueue_and_reply perform real messaging in the same module as the invariant. Their returned states are verified without a purity modifier. The compiler models send attempts and normal return values; it does not infer delivery or eventual response from those attempts.

Changing < state.capacity to <= state.capacity in enqueue fails verification: the additional element could exceed capacity. This also works when the helper library is a separate Gale dependency with its own transitive dependencies.

Note

This chapter is examples/invariants.

cd examples/invariants
mix deps.get
mix test

mix_gale installs the pinned F*/Z3 bundle when needed. The full source blocks above are checked against the example, and the example is tested with real OTP.

Bounded job state

The transition model can also track queued work, an active attempt, and terminal accounting. These ordinary functions are shared by a verified receive loop and a GenServer. The hosts import the same opaque state type and use the same transitions.

A bounded job lifecycle with attempt IDs and verified accounting.

Stale completions, cancellations, and failure reports preserve the entire state. Each current attempt reaches at most one terminal accounting transition. Attempt IDs belong to one initialized state lifetime; restarting begins again.

module invariants.job_state

@moduledoc """
A bounded job lifecycle with attempt IDs and verified accounting.

Stale completions, cancellations, and failure reports preserve the entire state.
Each current attempt reaches at most one terminal accounting transition.
Attempt IDs belong to one initialized state lifetime; restarting begins again.
"""

pub type Phase<A> = Idle | Running(id: Integer, payload: A) | Closed
pub type Worker = gale_std.process.Pid<(Integer, Integer)>

pub type Event = Completed(Integer) | Cancelled(Integer) | Failed(Integer)

fn active(phase: Phase<Integer>) -> Integer
ensures result { result >= 0 and result <= 1 } {
  match phase {
    Running(payload: _) -> 1
    Idle -> 0
    Closed -> 0
  }
}

pub opaque type State = {
  phase: Phase<Integer>,
  pending: List<Integer>,
  capacity: Integer,
  next_id: Integer,
  completed: Integer,
  cancelled: Integer,
  failed: Integer,
  worker: Worker
}
invariant state {
  state.capacity > 0
  and builtin.length(state.pending) + active(state.phase) <= state.capacity
  and state.completed >= 0 and state.cancelled >= 0 and state.failed >= 0
  and state.next_id == state.completed + state.cancelled + state.failed + active(state.phase)
  and match state.phase {
    Running(id, _) -> id >= 0 and id == state.next_id - 1
    Idle -> true
    Closed -> state.pending == []
  }
}

pub type Snapshot = {
  load: Integer,
  completed: Integer,
  cancelled: Integer,
  failed: Integer,
  current: Option<Integer>,
  closed: Boolean
}

pub fn new(capacity: Integer, worker: Worker) -> Result<State, :invalid>
ensures result {
  match result {
    Ok(state) -> state.capacity == capacity and state.worker == worker
      and state.phase == Idle and state.pending == [] and state.next_id == 0
      and state.completed == 0 and state.cancelled == 0 and state.failed == 0
    Error(_) -> capacity <= 0
  }
} {
  if capacity > 0 {
    Ok({phase: Idle, pending: [], capacity: capacity, next_id: 0,
        completed: 0, cancelled: 0, failed: 0, worker: worker})
  } else { Error(:invalid) }
}

pub fn is_closed(state: State) -> Boolean {
  match state.phase { Closed -> true _ -> false }
}

pub fn load(state: State) -> Integer
ensures result { result >= 0 and result <= state.capacity } {
  builtin.length(state.pending) + active(state.phase)
}

fn current(state: State, id: Integer) -> Boolean {
  match state.phase {
    Running(id: attempt) -> attempt == id
    _ -> false
  }
}

pub fn snapshot(state: State) -> Snapshot {
  {load: load(state), completed: state.completed, cancelled: state.cancelled,
   failed: state.failed,
   current: match state.phase { Running(payload: _, id: id) -> Some(id) _ -> None },
   closed: is_closed(state)}
}

pub fn submit(state: State, payload: Integer) -> Result<State, :rejected>
ensures result {
  match result {
    Ok(next) -> load(next) == load(state) + 1 and next.phase == state.phase
      and next.completed == state.completed and next.cancelled == state.cancelled
      and next.failed == state.failed and next.next_id == state.next_id
      and next.capacity == state.capacity and next.worker == state.worker
    Error(_) -> is_closed(state) or load(state) >= state.capacity
  }
} {
  if is_closed(state) or load(state) >= state.capacity { Error(:rejected) }
  else { Ok(state {pending: gale_std.list.append(state.pending, [payload])}) }
}

pub fn start_next(state: State) -> State
ensures result {
  load(result) == load(state) and result.completed == state.completed
  and result.cancelled == state.cancelled and result.failed == state.failed
  and result.capacity == state.capacity and result.worker == state.worker
  and match state.phase {
    Idle -> match state.pending {
      [] -> result == state
      [_ | _] -> current(result, state.next_id) and result.next_id == state.next_id + 1
    }
    _ -> result == state
  }
} {
  match state.phase {
    Idle -> match state.pending {
      [] -> state
      [payload | rest] -> {
        let next: State = state {
          phase: Running(state.next_id, payload), pending: rest, next_id: state.next_id + 1
        }
        let _ = gale_std.process.send(state.worker, (state.next_id, payload))
        next
      }
    }
    _ -> state
  }
}

pub fn complete(state: State, id: Integer) -> State
ensures result {
  if current(state, id) {
    result.completed == state.completed + 1 and result.phase == Idle
    and result.pending == state.pending and result.next_id == state.next_id
    and result.cancelled == state.cancelled and result.failed == state.failed
    and result.capacity == state.capacity and result.worker == state.worker
  } else { result == state }
} {
  if current(state, id) { state {phase: Idle, completed: state.completed + 1} }
  else { state }
}

pub fn cancel(state: State, id: Integer) -> State
ensures result {
  if current(state, id) {
    result.cancelled == state.cancelled + 1 and result.phase == Idle
    and result.pending == state.pending and result.next_id == state.next_id
    and result.completed == state.completed and result.failed == state.failed
    and result.capacity == state.capacity and result.worker == state.worker
  } else { result == state }
} {
  if current(state, id) { state {phase: Idle, cancelled: state.cancelled + 1} }
  else { state }
}

pub fn fail(state: State, id: Integer) -> State
ensures result {
  if current(state, id) {
    result.failed == state.failed + 1 and result.phase == Idle
    and result.pending == state.pending and result.next_id == state.next_id
    and result.completed == state.completed and result.cancelled == state.cancelled
    and result.capacity == state.capacity and result.worker == state.worker
  } else { result == state }
} {
  if current(state, id) { state {phase: Idle, failed: state.failed + 1} }
  else { state }
}

pub fn close(state: State) -> State
ensures result {
  is_closed(result) and load(result) == 0
  and result.completed == state.completed and result.failed == state.failed
  and result.cancelled == state.cancelled + active(state.phase)
  and result.next_id == state.next_id
  and result.capacity == state.capacity and result.worker == state.worker
} {
  state {phase: Closed, pending: [], cancelled: state.cancelled + active(state.phase)}
}

pub fn relevant(state: State, event: Event) -> Boolean {
  match event {
    Completed(id) -> current(state, id)
    Cancelled(id) -> current(state, id)
    Failed(id) -> current(state, id)
  }
}

@doc """
Handles a report and dispatches the next queued job only for a current attempt.
Reports are ordinary typed messages; they do not establish worker provenance.
"""
pub fn handle_event(state: State, event: Event) -> State
ensures result {
  if relevant(state, event) {
    load(result) == load(state) - 1
    and result.next_id >= state.next_id and result.next_id <= state.next_id + 1
    and result.capacity == state.capacity and result.worker == state.worker
    and match event {
      Completed(_) -> result.completed == state.completed + 1
        and result.cancelled == state.cancelled and result.failed == state.failed
      Cancelled(_) -> result.cancelled == state.cancelled + 1
        and result.completed == state.completed and result.failed == state.failed
      Failed(_) -> result.failed == state.failed + 1
        and result.completed == state.completed and result.cancelled == state.cancelled
    }
  } else { result == state }
} {
  if relevant(state, event) {
    let next = match event {
      Completed(id) -> complete(state, id)
      Cancelled(id) -> cancel(state, id)
      Failed(id) -> fail(state, id)
    }
    start_next(next)
  } else { state }
}

Two hosts, the same state

The raw process uses a typed message union and passes valid state to its next recursive call. The GenServer schedules dispatch with an OTP continuation and returns the same state type from its callbacks. Both hosts are selected for verification automatically, including when the state module comes from a separate Gale dependency. The copied code_change default also preserves valid state.

The runtime tests run the same job lifecycle through both hosts, including stale and duplicate reports, rejected submissions, closing, and a GenServer system code change. The contracts check state validity and exact accounting. Reports remain claims supplied by messages; no sender authentication, job execution, delivery, or across-restart guarantee follows from these proofs.

A raw receive loop hosting the same verified job state as invariants.job_server. Replies use typed process IDs; reports are untrusted claims about attempt IDs.

Raw receive loop

module invariants.job_process

@moduledoc """
A raw receive loop hosting the same verified job state as invariants.job_server.
Replies use typed process IDs; reports are untrusted claims about attempt IDs.
"""

pub type Message =
  | Submit(payload: Integer, reply_to: gale_std.process.Pid<Result<:ok, :rejected>>)
  | Report(invariants.job_state.Event)
  | Inspect(gale_std.process.Pid<invariants.job_state.Snapshot>)
  | Close(gale_std.process.Pid<invariants.job_state.Snapshot>)
  | Stop

pub fn start(capacity: Integer, worker: invariants.job_state.Worker) -> Result<gale_std.process.Pid<Message>, :invalid> {
  match invariants.job_state.new(capacity, worker) {
    Ok(state) -> Ok(gale_std.process.spawn(fn() receives Message => loop(state)))
    Error(reason) -> Error(reason)
  }
}

fn loop(state: invariants.job_state.State) receives Message -> :ok {
  receive {
    Submit(payload, reply_to) -> {
      match invariants.job_state.submit(state, payload) {
        Ok(queued) -> {
          let next = invariants.job_state.start_next(queued)
          let _ = gale_std.process.send(reply_to, Ok(:ok))
          loop(next)
        }
        Error(reason) -> {
          let _ = gale_std.process.send(reply_to, Error(reason))
          loop(state)
        }
      }
    }
    Report(event) -> loop(invariants.job_state.handle_event(state, event))
    Inspect(reply_to) -> {
      let _ = gale_std.process.send(reply_to, invariants.job_state.snapshot(state))
      loop(state)
    }
    Close(reply_to) -> {
      let next = invariants.job_state.close(state)
      let _ = gale_std.process.send(reply_to, invariants.job_state.snapshot(next))
      loop(next)
    }
    Stop -> :ok
  }
}

A GenServer hosting job_state with a continuation for initial dispatch. The ordinary process and this server share every state transition.

GenServer callbacks

module invariants.job_server

@moduledoc """
A GenServer hosting job_state with a continuation for initial dispatch.
The ordinary process and this server share every state transition.
"""

implements gale_std.gen_server.Server<Args, invariants.job_state.State, Request, Never, invariants.job_state.Event, :dispatch> as service

pub type Args = (Integer, invariants.job_state.Worker)
pub type Request =
  | Submit(payload: Integer, reply_to: gale_std.gen_server.ReplyTo<Result<:ok, :rejected>>)
  | Inspect(gale_std.gen_server.ReplyTo<invariants.job_state.Snapshot>)
  | Close(gale_std.gen_server.ReplyTo<invariants.job_state.Snapshot>)
pub type Service = service
pub type Target = gale_std.gen_server.ServerTarget<Service>

pub fn start_link(args: Args) -> gale_std.gen_server.StartResult<Service> {
  gale_std.gen_server.start_link(invariants.job_server, args, [])
}

pub fn init(args: Args) -> gale_std.otp.Init<invariants.job_state.State, :dispatch> {
  let (capacity, worker) = args
  match invariants.job_state.new(capacity, worker) {
    Ok(state) -> (:ok, state, (:continue, :dispatch))
    Error(reason) -> (:stop, reason)
  }
}

pub fn submit(server: Target, payload: Integer) -> Result<:ok, :rejected> {
  gale_std.gen_server.call(server, fn(reply_to) => Submit(payload, reply_to))
}

pub fn snapshot(server: Target) -> invariants.job_state.Snapshot {
  gale_std.gen_server.call(server, fn(reply_to) => Inspect(reply_to))
}

pub fn close(server: Target) -> invariants.job_state.Snapshot {
  gale_std.gen_server.call(server, fn(reply_to) => Close(reply_to))
}

pub fn handle_call<R>(
  build: fn(gale_std.gen_server.ReplyTo<R>) -> Request,
  from: gale_std.gen_server.ReplyTo<R>,
  state: invariants.job_state.State
) -> gale_std.otp.Next<invariants.job_state.State, :dispatch> {
  match build(from) {
    Submit(payload, reply_to) -> {
      match invariants.job_state.submit(state, payload) {
        Ok(queued) -> {
          let _ = gale_std.gen_server.reply(reply_to, Ok(:ok))
          let next: gale_std.otp.Next<invariants.job_state.State, :dispatch> = (:noreply, queued, (:continue, :dispatch))
          next
        }
        Error(reason) -> {
          let _ = gale_std.gen_server.reply(reply_to, Error(reason))
          let next: gale_std.otp.Next<invariants.job_state.State, :dispatch> = (:noreply, state)
          next
        }
      }
    }
    Inspect(reply_to) -> {
      let _ = gale_std.gen_server.reply(reply_to, invariants.job_state.snapshot(state))
      let next: gale_std.otp.Next<invariants.job_state.State, :dispatch> = (:noreply, state)
      next
    }
    Close(reply_to) -> {
      let closed = invariants.job_state.close(state)
      let _ = gale_std.gen_server.reply(reply_to, invariants.job_state.snapshot(closed))
      let next: gale_std.otp.Next<invariants.job_state.State, :dispatch> = (:noreply, closed)
      next
    }
  }
}

pub fn handle_info(event: invariants.job_state.Event, state: invariants.job_state.State) -> gale_std.otp.Next<invariants.job_state.State, :dispatch> {
  (:noreply, invariants.job_state.handle_event(state, event))
}

pub fn handle_continue(value: :dispatch, state: invariants.job_state.State) -> gale_std.otp.Next<invariants.job_state.State, :dispatch> {
  (:noreply, invariants.job_state.start_next(state))
}