TLA+ specification for Succint Atomic Swap



Summary:

In an email exchange, Ruben Somsen points out to Dmitry Petukhov that it is important to note that it is not enough for Bob to publish success_tx before refund_tx_1 becomes valid; the former needs to be confirmed before the latter. Dmitry agrees and notes that this is unlikely to be a practical problem unless the original fee of success_tx is too small and Bob messes up CPFP-ing it. Ruben also clarifies that Alice won't give her key until she learns secretBob because step 5 comes before step 6 in the diagram. Dmitry admits that he missed this and that he now made the `signers_map` into variable that can be changed to give Bob the ability to sign for Alice. However, he warns that this will add a bunch of new transactions to the model, each Alice&Bob spend having 'Bob unilateral override' case.


Updated on: 2023-06-14T01:38:45.752393+00:00