OTP

OTP is standard library, not extra compiler syntax. A server is an ordinary module that implements gale_std.gen_server.Server. Gale emits the native callback module with @behaviour Elixir.GenServer and explicit @impl Elixir.GenServer attributes. It does not emit use GenServer.

mod example_otp.counter

alias gale_std.gen_server
alias gale_std.otp

implements gen_server.Server<
Integer,
Integer,
CounterCall,
CounterCast,
Never,
Never
> as service

pub type CounterCall<R> =
| Value : CounterCall<Integer>
| Add(amount: Integer) : CounterCall<Integer>

pub type CounterCast = Reset | Increment
pub type CounterTarget = gen_server.ServerTarget<service>

pub fn start_link(initial: Integer) -> gen_server.StartResult<service> {
  gen_server.start_link(example_otp.counter, initial, [{:name, :counter}])
}

pub fn child_spec(initial: Integer) -> ChildSpec<service> {
  gen_server.child_spec(example_otp.counter, initial, [{:id, :counter}])
}

pub fn value(server: CounterTarget) -> Integer {
  gen_server.call(server, Value)
}

pub fn add(server: CounterTarget, amount: Integer) -> Integer {
  gen_server.call(server, Add(amount))
}

pub fn reset(server: CounterTarget) -> :ok {
  gen_server.cast(server, Reset)
}

pub fn increment(server: CounterTarget) -> :ok {
  gen_server.cast(server, Increment)
}

pub fn init(initial: Integer) -> otp.Init<Integer, Never> {
  {:ok, initial}
}

pub fn handle_call<R>(
  request: CounterCall<R>,
  from: gen_server.ReplyTo<R>,
  state: Integer
) -> otp.Next<Integer, Never> {
  case request {
    Value -> {
      gen_server.reply(from, state)
      {:noreply, state}
    }
    Add(amount) -> {
      next = state + amount
      gen_server.reply(from, next)
      {:noreply, next}
    }
  }
}

pub fn handle_cast(
  message: CounterCast,
  state: Integer
) -> otp.Next<Integer, Never> {
  case message {
    Reset -> {:noreply, 0}
    Increment -> {:noreply, state + 1}
  }
}

Calls return their native reply directly and exit on timeout or server failure. Each request constructor fixes its reply index. Matching the request refines R, so the branch’s ReplyTo<R> accepts only that constructor’s reply type.

gale_std.supervisor.Supervisor<Args> is Elixir.Supervisor. The callback returns the same native init value as Elixir. There is no macro or extra runtime supervisor module.

mod example_otp.tree

alias example_otp.counter
alias gale_std.supervisor

implements supervisor.Supervisor<:ok> as root

pub fn start_link() -> supervisor.SupervisorStartResult<mod supervisor.Supervisor<:ok>> {
  supervisor.start_link(example_otp.tree, :ok, [])
}

pub fn child_spec(args: :ok) -> ChildSpec<mod supervisor.Supervisor<:ok>> {
  supervisor.child_spec(example_otp.tree, args)
}

pub fn init(args: :ok) -> supervisor.SupervisorInit {
  supervisor.init(
    [supervisor.any_child(counter.child_spec(0))],
    [{:strategy, :one_for_one}]
  )
}

An opaque type can hide state fields so only the owning module constructs and updates them. This quota keeps 0 <= reserved <= capacity for every state its GenServer can construct through Gale. The proving chapter covers invariant, ensures, and gale verify.

A quota whose reserved amount stays between zero and capacity.

Outside this module, opaque State can only come from these functions. A GenServer can store State without exposing its fields.

mod example_otp.quota_state

@moduledoc """
A quota whose reserved amount stays between zero and capacity.

Outside this module, opaque `State` can only come from these functions.
A GenServer can 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)
  }
}

pub fn reserve(state: State, amount: Integer) -> Result<State, :invalid> {
  if amount >= 0 and amount <= state.capacity - state.reserved {
    Ok(%{state | reserved: 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 >= 0 }
{
  state.capacity - state.reserved
}

A GenServer whose state is an opaque quota.

Callbacks handle messages and replies. quota_state owns the pure transitions. A rejected reserve returns an error and keeps the previous valid state. The type does not prove delivery, liveness, or crash freedom.

mod example_otp.quota

@moduledoc """
A GenServer whose state is an opaque quota.

Callbacks handle messages and replies. `quota_state` owns the pure
transitions. A rejected reserve returns an error and keeps the previous
valid state. The type does not prove delivery, liveness, or crash freedom.
"""

alias example_otp.quota_state
alias gale_std.gen_server
alias gale_std.otp

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

pub type Request<R> =
| Available: Request<Integer>
| Reserve(amount: Integer): Request<Result<Integer, :invalid>>
| Release(amount: Integer): Request<Result<Integer, :invalid>>

pub type Target = gen_server.ServerTarget<service>

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

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

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

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

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

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

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

If a callback builds a raw record and returns it as quota_state.State, the compiler rejects it. Opacity does not prove liveness, delivery, or that handwritten Elixir respects the opaque API.

Note

This chapter is examples/otp.

cd examples/otp
mix test