Date: Mon, 1 Jun 2020 16:38:54 +0500
From: Dmitry Petukhov <dp@simplexum.com>
To: Dmitry Petukhov via bitcoin-dev <bitcoin-dev@lists.linuxfoundation.org>
Message-ID: <20200601163854.17594845@simplexum.com>
In-Reply-To: <20200513220222.24953c0a@simplexum.com>
References: <20200513220222.24953c0a@simplexum.com>
Organization: simplexum.com
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Subject: Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap
Precedence: list

I've finished specifying the full Succint Atomic Swap contract in TLA+.

I believe the specification [1] now covers all relevant behaviors of
the participants. It even has an option to enable 'non-rational'
behavior, so that it can be shown that the transactions that are there
to punish bad behavior can actually be used. If you examine the spec
and find that I failed to specify some relevant behavior, please tell.

The specification can be used to exhaustively check safety properties
of the model (such as no participant can take both coins, unless in
explicitly specified circumstances), and temporal properties (such as
contract always end up in an explicitly specified 'finished' state).

The specification can also be used to *show* (but not automatically
check at the moment) the hyperproperties of the model, such as what
transactions can ever be confirmed in at least one the execution path,
max/min/avg values for various stats, etc. The information on these
hyperproperties can be printed out during model checking, and can be
examined manually or with help of additional scripts (if one willing to
write some).

The model has some limitations, like only having one miner, and not
modelling fees and mempool priorities. More than one miner needed to
introduce reorgs in the model, but I believe that reorgs are relevant
only if we cannot say that "one block in the model means 6 bitcoin
blocks" (or whatever reorg safety limit is acceptable). I also believe
that the fees and mempool priorities are a lower-level concern, because
the task to confirm the transaction in time is the same for different
stages of the contract and for different transactions, and therefore
this can be modelled separately.

The goal of creating this specification was to evaluate the suitability
of TLA+ for modelling of the smart contracts in UTXO-based
blockchain systems. I believe that the presented spec shows that it is
indeed feasible to do such modelling and TLA+ is a suitable tool for
specifying and for checking such specifications (Although having ability
to automatically check hyperproperties using TLA+ expressions would be
nice).

I hope that this spec can be used as a basis for specs for other
contracts, and that using TLA+ can make designing safe contracts for
UTXO-based systems easier. I also hope that this will help to increase
interest in using formal methods in this area.

I tried to make the parts of the spec that deal with things like mining
and mempool to not depend on the concrete contract logic, in
expectation that this logic can be reused afterwards for the specs of
other contracts. I did not make specific effort to factor out this
generic logic into separate module though, because I think that more
various contract specifications need to be designed and analyzed to
understand what is really generic and what should lay with concrete
contract logic. When more knowledge is created regarding this, there
could be a module that contract specifications can use to avoid
explicitly specifying the generic blockchain-related logic.

Thanks to Ruben Somsen for designing this contract and
providing helpful description and diagram that made it possible to
create this formal specification.

[1] https://github.com/dgpv/SASwap_TLAplus_spec