Hoare

Declared state transitions as pre/post contracts.

Most records carry a status, and most bugs around one are the same few: a change made from a state it should not have started in, a side effect that happened although the change did not, two requests racing over one record. Hoare makes the transition a declaration, the states it leaves, the state it reaches, the guards that must hold and the effects it performs, and runs every declaration the same way. {from, guards} body {to} is a Hoare triple; running it keeps one law: a run ends in to or leaves the record in from, never between.

check    from ▸ guards                  on the record the caller resolved
perform  effects                        IO; bare = idempotent, {run, undo} = reverted on failure
commit   lock ▸ read ▸ check ▸ body ▸ write to ▸ read ▸ assert to      one transaction

No processes, no DSL beyond two use macros, no dependencies. Results are plain {:ok, value} | {:error, reason} tuples throughout.

Installation

def deps do
  [
    {:hoare, "~> 0.2"}
  ]
end

Add import_deps: [:hoare] to .formatter.exs.

States

A state is a module: the status that tags a record, the reason when it does not, and the properties that refine the tag. Matching a record builds a struct of witnesses, the record plus whatever the properties extracted, so nothing downstream has to look again.

defmodule Invoice.State do
  import Hoare.State, only: [defstate: 2, defstate: 3]

  defstate Draft, status: :draft
  defstate Paid, status: :paid
  defstate Void, status: :void

  defstate Issued, status: :issued, witnesses: [:lines], preloads: [:lines] do
    @impl Hoare.State
    def properties, do: [&billable_lines/1]

    defp billable_lines(%__MODULE__{record: %{lines: []}}), do: {:error, :no_lines}
    defp billable_lines(%__MODULE__{record: %{lines: lines}} = state), do: {:ok, %{state | lines: lines}}
  end
end

Hoare.State.match(Invoice.State.Issued, invoice)
#=> {:ok, %Issued{record: invoice, lines: [...]}} | {:error, :not_issued} | {:error, :no_lines}

:missing defaults to :not_<status>. A state that needs its own file is use Hoare.State, status: ... in a module; one that needs neither macro implements the Hoare.State behaviour and defines the struct itself. The state one transition reaches is the module another leaves, so the graph is nominal and inspectable.

Transitions

defmodule Invoice.Pay do
  use Hoare.Transition,
    from: [Invoice.State.Issued],
    to: Invoice.State.Paid,
    ctx: [:payment_method, :charge]

  import Hoare.Result, only: [ensure: 2]

  @impl Hoare.Transition
  def guards, do: [ensure(&amount_due?/1, :nothing_due), &chargeable_method/1]

  @impl Hoare.Transition
  def effects, do: [&cancel_reminder/1, {&charge/1, &refund/1}]

  @impl Hoare.Transition
  def stranded(ctx, reason), do: Alerts.reminder_cancelled_unpaid(ctx.record, reason)

  defp amount_due?(%{record: invoice}), do: Decimal.positive?(invoice.balance)
  ...
end

The context is the module's struct: record, the record whose status moves; state, filled by matching from; and the :ctx keys. Every arrow is ctx -> {:ok, ctx} | {:error, reason} and may refine the context it returns.

• Guards decide whether the transition may run. Hoare.Result.ensure/2 lifts a predicate into one; a guard that finds something worth keeping puts it in the context.
• Effects are the IO that cannot join a database transaction. A bare effect must be idempotent, because the recovery for a failed run is to run again. An effect paired with an undo is reverted, newest first, when anything after it fails.
• stranded/2 is optional. It is told when a run fails after a bare effect, the one case that leaves something behind: alert, or queue the retry.

The module that owns the records runs the transition, supplying its own writes as the body and the store:

def pay(invoice_id, payment_method) do
  with {:ok, invoice} <- Invoices.fetch(invoice_id, Pay.preloads()),
       {:ok, paid} <- Pay.run(%Pay{record: invoice, payment_method: payment_method}, &record_payment/1, store: Repo),
       do: {:ok, paid.record}
end

defp record_payment(%Pay{record: invoice, charge: charge}), do: Payments.insert(invoice, charge)

Pay.preloads() is what the states and the transition declared, the same list the commit re-reads with. Pay.check/1 runs the precondition alone, to decide whether to offer the action. Pay.from_statuses/0 serves queries.

The commit

In one transaction, under the store's lock on {schema, id} (or opts[:lock]), the commit reads the record again with the declared preloads, runs the whole check on it, runs the body on the re-checked context, writes to's status through the schema's changeset/2, and asserts to on a second read. So:

• Guards run twice, before the effects and again under the lock. A guard is a function of the context alone and writes only keys no effect writes. Whatever the caller resolved into the context is no fresher the second time: a condition that must hold under the lock reads the record, with what it reads named in preloads.
• A record already in to is a concurrent run of the same transition. It converges as {:ok, record} when every completed effect was bare, and is {:error, :status_changed}, with the undos run, otherwise.
• A record in neither is {:error, :status_changed}; one that vanished is {:error, :not_found}. Hoare.Transition.error/1 adds both to a transition's own reasons.
• A body that leaves the record outside to raises, rolling back.

Without the macro

use Hoare.Transition assembles a %Hoare.Transition{} and calls Hoare.Transition.run/4. The struct is the core and can be built or varied directly, a resume path that skips an announcement, say:

Hoare.Transition.run(%{Pay.transition() | effects: [&charge_again/1]}, ctx, body, store: Repo)

Store

Hoare.Store is the three operations the commit needs: transact_with_lock/2, read/3 and update/1. An Ecto.Repo has the last already:

defmodule MyApp.Repo do
  use Ecto.Repo, otp_app: :my_app, adapter: Ecto.Adapters.Postgres
  @behaviour Hoare.Store

  @impl Hoare.Store
  def transact_with_lock(lock, fun) do
    transact(fn ->
      query!("SELECT pg_advisory_xact_lock($1)", [:erlang.phash2(lock)])
      fun.()
    end)
  end

  @impl Hoare.Store
  def read(schema, id, preloads) do
    if record = get(schema, id), do: {:ok, preload(record, preloads)}, else: {:error, :not_found}
  end
end

Nothing in Hoare depends on Ecto: the record is any struct with id and status, whose module has a changeset/2 the store's update/1 accepts.

Testing

Hoare.Store.Memory keeps records in the test process, so a transition's contract is tested without a database:

invoice = Memory.put(%Invoice{id: 1, status: :issued, lines: [line], balance: Decimal.new(10)})

assert {:ok, %Pay{record: %Invoice{status: :paid}}} =
         Pay.run(%Pay{record: invoice, payment_method: card}, &{:ok, &1}, store: Memory)

Guards and properties are plain functions of data: Pay.check/1 and Hoare.State.match/2 need no store at all.

Graph

Hoare.Graph.edges([Invoice.Issue, Invoice.Pay, Invoice.Cancel])
#=> [{Draft, Issue, Issued}, {Issued, Pay, Paid}, {Draft, Cancel, Void}, {Issued, Cancel, Void}]

Hoare.Graph.to_mermaid([Invoice.Issue, Invoice.Pay, Invoice.Cancel])

stateDiagram-v2
    Draft --> Issued: Issue
    Issued --> Paid: Pay
    Draft --> Void: Cancel
    Issued --> Void: Cancel

Assert on edges/1 in a test and a change to the lifecycle becomes a deliberate diff.

Results

Hoare.Result holds the few combinators the runner is built from: bind/2, kleisli/1, ensure/2, tap_ok/2, tap_error/2, map_error/2. Tagged tuples throughout; nothing is wrapped.