Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap
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
Re: [bitcoin-dev] Design for a CoinSwap implementation for massively improving Bitcoin privacy and fungibility
Hi ZmnSCPxj, >If Alice is paying to a non-SAS aware payee Yeah, I agree that this use case is not possible without a third transaction (preferably from the timelocked side, in the case of SAS). My point was merely that you can swap and simultaneously merge some of your outputs into the post-swap non-timelocked output, though perhaps that is not very useful. Cheers, Ruben On Mon, Jun 1, 2020 at 4:34 AM ZmnSCPxj wrote: > Good morning Ruben, > > > > > > That assumes there will be a second transaction. With SAS I believe we > can avoid that, and make it look like this: > > > > +---+ > > Alice ---| |--- Bob > > Alice ---| | > > Bob ---| | > > +---+ > > If Alice is paying to a non-SAS aware payee that just provides an onchain > address (i.e. all current payees today), then the 2-of-2 output it gets > from the swap (both of whose keys it learns at the end of the swap) is > **not** the payee onchain address. > And it cannot just hand over both private keys, because the payee will > still want unambiguous ownership of the entire UTXO. > So it needs a second transaction anyway. > (with Schnorr then Alice and payee Carol can act as a single entity/taker > to Bob, a la Lightning Nodelets using Composable MuSig, but that is a > pretty big increase in protocol complexity) > > If Alice does not want to store the remote-generated privkey as well, and > use only an HD key, then it also has to make the second transaction. > Alice might want to provide the same assurances as current wallets that > memorizing a 12-word or so mnemonic is sufficient backup for all the funds > (other than funds currently being swapped), and so would not want to leave > any funds in a 2-of-2. > > If Bob is operating as a maker, then it also cannot directly use the > 2-of-2 output it gets from the swap, and has to make a new 2-of-2 output, > for the *next* taker that arrives to request its services. > > So there is always going to be a second transaction in a SwapMarket > system, I think. > > > What SAS / private key turnover gets us is that there is not a *third* > transaction to move from a 1-of-1 to the next address that makers and > takers will be moving anyway, and that the protocol does not have to add > communication provisions for special things like adding maker inputs or > specifying all destination addresses for the second stage and so on, > because those can be done unilaterally once the private key is turned over. > > > > >A thing I have been trying to work out is whether SAS can be done with > more than one participant, like in S6 > > > > S6 requires timelocks for each output in order to function, so I doubt > it can be made to work with SAS. > > Hmmm right right. > > Naively it seems both chaining SAS/private key turnover to multiple > makers, and a multi-maker S6 augmented with private key turnover, would > result in the same number of transactions onchain, but I probably have to > go draw some diagrams or something first. > > But S6 has the mild advantage that all the funding transactions paying to > 2-of-2s *can* appear on the same block, whereas chaining swaps will have a > particular order of when the transactions appear onchain, which might be > used to derive the order of swaps. > On the other hand, funds claiming in S6 is also ordered in time, so > someone paying attention to the mempool could guess as well the order of > swaps. > > > Regards, > ZmnSCPxj > ___ bitcoin-dev mailing list bitcoin-dev@lists.linuxfoundation.org https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
Re: [bitcoin-dev] Announcing Bitcoin Wallet Tracker
Hi Antoine, I designed both APIs, so they definitely do share some similarities. It's difficult to compare their performance directly, since esplora-electrs keeps a full index of everything, while bwt tracks your wallet addresses only. If you're only interested in your wallet addresses and don't have a *really* huge number of them, bwt will definitely perform better, as it can avoid a lot of unnecessary indexing work. If you do have a lot of addresses, esplora-electrs will be better suited for the job, as its designed to deal with high volumes of data and does not rely on the bitcoind wallet functionality, which was not designed for this. I'm not sure where the line for "really huge" crosses exactly though, I have not put this to the test. Definitely if you're tracking millions of addresses, probably also for hundreds of thousands, possibly even less? API design wise, the main differences between the two are: - Esplora provides every bit of information one might want to know about transactions/blocks, while bwt intentionally tries to reduce this to the subset useful in the context of app development. - bwt provides wallet-contextual information, like key origins next to addresses and the net change inflicted on the wallet's balance by transactions. - Esplora doesn't provide real-time updates (yet), while bwt provides them using two different mechanisms (SSE and Web Hooks). Nadav On Sun, May 31, 2020 at 5:56 PM darosior wrote: > > Hi, > > I gave a quick look to the http API, and it seems very similar to Esplora's. > So I wonder : how does > bwt compares to Esplora, performance-wise ? > > Thanks! > Antoine > > > ‐‐‐ Original Message ‐‐‐ > Le samedi, mai 30, 2020 4:16 PM, Nadav Ivgi via bitcoin-dev > a écrit : > > Hi all, > > I recently released bwt [0], an HD wallet indexer implemented in Rust, using > a model similar to that of Electrum Personal Server. > > It uses the bitcoind wallet functionality to do the heavy lifting and builds > additional indexes on top of that, which can be queried using the Electrum > RPC protocol, as well as a more modern, developer-friendly HTTP REST API. > > The electrum server can also be used as an electrum plugin [1], which > integrates the server straight into the electrum client. From the user's > perspective, this allows connecting electrum directly to a full node. > > The HTTP API is my take on a modern design for a wallet tracking API aimed > at app developers. Some use-cases include using it as a backend for wallets > (similarly to Samuari's Dojo) or to track deposits to a watch-only xpub > (similarly to BTCPay's NBXplorer). > > Compared to using the bitcoind RPC directly, bwt provides: > > - The ability to track an xpub and automatically have new addresses derived > and imported as needed, according to the gap limit. > > - Two additional indexes, one for looking up the transaction history of > addresses, and another one for looking up txo spends (a map of > funding_txid:vout => spending_txid:vin). > > - Real-time updates using Server-Sent Events [2] (a long-lived streaming HTTP > connection) or Web Hooks [3] (an HTTP request sent to a configured URL). > The updates being sent [4] directly provide information about the funded > and spent wallet txos, instead of the client figuring it out from the tx. > > - Some API conveniences and simplifications, like including key origin > information directly alongside inputs/outputs [5], the ability to specify > key origins in place of addresses (eg. GET /hd/15cb9edc/8/utxos), a compact > history format [6], and an easy way to catch-up with missed events [7]. > Unless explicitly asked for, the API omits information about non-wallet > inputs/outputs and protocol-level details like scriptsig and witnesses, > which are typically not needed for higher-level app development. > > The indexer is designed in a way that minimizes RPC requests to bitcoind. By > using labels to store key origin information, it is able to index incoming > transactions using the information available from `listtransactions` alone > (plus 3 extra rpc requests that don't grow with the number of transactions), > but requires 1 additional rpc call per outgoing transaction (to learn which > prevouts were spent). It can index 10k incoming txs in under a second, or a > mixture of 5k/5k in under 5 seconds. The index is currently entirely in- > memory and does not get persisted. The indexer logic can be seen in [8]. > > One major item on the roadmap that I'm hoping to tackle soon is support for > output script descriptors. > > If anyone is interested in contributing, the README has some useful developer > resources [9] and a handy script for setting up a development environment. > > This is an early alpha release, recommended for use with testnet/regtest. > > All feedback welcome! > > Cheers, > Nadav > > [0] https://github.com/shesek/bwt > [1] https://github.com/shesek/bwt#electrum-plugin > [2]
