Verifying properties of a financial contract in Elixir

Questions / Help
,
1

Hi, I am interested in verifying properties of Elixir code. In particular, I write code for financial institutions and I am exploring if formal verification can be useful for me.

A loan contract starts in a unsigned state, waiting for some party to propose an amount.

When an amount is proposed, the contract enters a state when it waits for signatures from lender and lendee.

Whenever an amount is proposed, both signatures are reset, so that a lendee never has to pay more than he agreed to, because every time the amount is changed, new signatures are needed.

The contract is done when all debt has been paid (and not more).

Is there an easy-to-use solution for verifying this property in the Elixir/Erlang ecossystem?

The answer might rely on property-based testing, as long as it is exhaustive up to a given measure, as in bounded model checking.

My code is:

defmodule Loan do

  def start() do
    spawn(__MODULE__, :main_loop, [:unsigned])
  end

  def main_loop(:done) do
    receive do
      :show ->
        IO.puts("Contract is finished")
        apply(__MODULE__, :main_loop, [:done])
    end
  end

  def main_loop(:unsigned) do
    receive do
      {:propose, amount} ->
        apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: false, lender: false]])
    end
  end

  @spec main_loop(:proposal, any, [{:lendee, any} | {:lender, any}, ...]) :: any
  def main_loop(:proposal, amount, lendee: true, lender: true) do
    IO.puts("Contract is now signed, contract value is #{amount}")
    apply(__MODULE__, :main_loop, [:signed, amount])
  end

  def main_loop(:proposal, amount, lendee: lendee, lender: lender) do
    receive do
      :sign_lendee ->
        apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: true, lender: lender]])

      :sign_lender ->
        apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: lendee, lender: true]])

      {:propose, amount} ->
        apply(__MODULE__, :main_loop, [:proposal, amount, lendee: false, lender: false])

      :show ->
        case {lendee, lender} do
          {false, false} ->
            IO.puts("No one has signed, contract value is #{amount}")

          {false, true} ->
            IO.puts("Lender has signed, contract value is #{amount}")

          {true, false} ->
            IO.puts("Lendee has signed, contract value is #{amount}")

          {true, true} ->
            IO.puts("Both lender and lendee have signed, contract value is #{amount}")
        end

        apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: lendee, lender: lender]])
    end
  end

  def main_loop(:signed, balance) when balance > 0 do
    receive do
      :show ->
        IO.puts(balance)
        apply(__MODULE__, :main_loop, [:signed, balance])

      {:pay, amount} when amount <= balance ->
        IO.puts("Paying #{amount} to lender")
        apply(__MODULE__, :main_loop, [:signed, balance - amount])
    end
  end

  def main_loop(:signed, 0) do
    IO.puts("Contract is finished")
    main_loop(:done)
  end
end
2

You could also store a hash with the details of both parties, the conditions, and the amount, and the version of the manifest, and when signed, you create another hash including the previous hash plus the date of the signing, and the version of the manifest. That way you can check over time the status of contracts without having to read the contents.

3

Definitely not an expert in these areas, but isn’t property testing and formal verification entirely different things? Formal verification assess the “form” of the code in a static sense. Property tests run the code through a bunch of different situations and try to ensure that it always has certain properties. Definitely both contribute to one’s sense that code will behave correctly, but neither is a substitute for the other.

4

Verification is about verifying some property, which depends of course on the domain.

I am not an expert as well, but as far as I know:

Property tests generate random inputs and test if the property is preserved, but it might (and won’t, in practice) generate all possible inputs (or, more precisely, cover all equivalence classes). But they do give you assurance, anyways

Verification is about checking if a property holds for all inputs, or, at least, for all inputs of size < n. In our case inputs might be messages and we would look for all possible execution traces of size < n,

So I wondered if any readily usable verification tool exists for BEAM/Erlang/Elixir, or if I need to hand roll it…

5

There’s a good book about property-based testing in Elixir: Property-Based Testing with PropEr, Erlang, and Elixir: Find Bugs Before Your Users Do by Fred Hebert

A first step for that sort of testing would be cleanly dividing the “business logic” (changing the state etc) from the runtime behavior (receive etc). You’d wind up with a function that takes two arguments: a “world” and a message and produces a new “world” (see also the “update” function in The Elm Architecture).

6

Agreed, the most practical way to test your code would be to build a stateful property test via PropEr. I don’t know of any verification tool for Elixir that can statically verify properties of algorithms in the same way that, for example, Frama-C does for C.

On the topic of stateful property tests, I would encourage you to consider using a higher-level tool to help capture exactly what you wish to model. A language like TLA+ can help you model the rules of your state machine and its model checker will help you find errors in your model, or your understanding of the model, or both. This can often lead to insights into the specific invariants you wish to exercise in your property test. Finally, if you really need to (and you probably don’t) you could use its proof-assistant to prove these invariants hold. But for code, stateful property-testing is realistically as good as it gets right now.

Finally, the advice to separate mechanism (e.g. your receive loop) from your state-transition logic is good, and GenServer and GenStateMachine will do that for you.

1 Like