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 _______________________________________________ bitcoin-dev mailing list bitcoin-dev@lists.linuxfoundation.org https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
