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 behavio
Hi Dmitry,
>But it should be noted that it is not enough that Bob publishes success_tx
before refund_tx_1 became valid. The success_tx needs to be confirmed
before refund_tx_1 became valid.
Agreed, my write-up would benefit from pointing this out more explicitly.
Cheers,
Ruben
On Thu, May 14, 2
В Thu, 14 May 2020 07:31:13 +0200
Ruben Somsen wrote:
> Hi Dmitry,
>
> >While refund_tx_1 is in the mempool, Bob gives success_tx to the
> >friendly miner
>
> I see, so you're talking about prior to protocol completion, right
> after Alice sends Bob the success_tx. The reason this is not an iss
Hi Dmitry,
>While refund_tx_1 is in the mempool, Bob gives success_tx to the friendly
miner
I see, so you're talking about prior to protocol completion, right after
Alice sends Bob the success_tx. The reason this is not an issue is because
Alice and Bob both had to misbehave in order for this to
В Wed, 13 May 2020 21:03:17 +0200
Ruben Somsen wrote:
> Or perhaps you're referring to the issue ZmnSCPxj pointed out after
> that, where refund transaction #1 and the success transaction could
> both become valid at the same time. It would make sense for the test
> to pick up on that, but I beli
Hi Dmitry,
Thanks for creating a specification for testing, I appreciate the interest!
>The checking of the model encoded in the specification can successfully
detect the violation of 'no mutual secret knowledge' invariant when one of
the participant can bypass mempool and give the transaction di
The Succint Atomic Swap contract presented by Ruben Somsen recently has
drawn much interest.
I personally am interested in the smart contracts realizeable in the
UTXO model, and also interested in applying formal methods to the
design and implementation of such contracts.
I think that having form
