3 Search Results for "Reeves, Daniel"


Document
An Axiomatic Characterization of CFMMs and Equivalence to Prediction Markets

Authors: Rafael Frongillo, Maneesha Papireddygari, and Bo Waggoner

Published in: LIPIcs, Volume 287, 15th Innovations in Theoretical Computer Science Conference (ITCS 2024)


Abstract
Constant-function market makers (CFMMs), such as Uniswap, are automated exchanges offering trades among a set of assets. We study their technical relationship to another class of automated market makers, cost-function prediction markets. We first introduce axioms for market makers and show that CFMMs with concave potential functions characterize "good" market makers according to these axioms. We then show that every such CFMM on n assets is equivalent to a cost-function prediction market for events with n outcomes. Our construction directly converts a CFMM into a prediction market, and vice versa. Using this equivalence, we give another construction which can produce any 1-homogenous, increasing, and concave CFMM, as are typically used in practice, from a cost function. Conceptually, our results show that desirable market-making axioms are equivalent to desirable information-elicitation axioms, i.e., markets are good at facilitating trade if and only if they are good at revealing beliefs. For example, we show that every CFMM implicitly defines a proper scoring rule for eliciting beliefs; the scoring rule for Uniswap is unusual, but known. From a technical standpoint, our results show how tools for prediction markets and CFMMs can interoperate. We illustrate this interoperability by showing how liquidity strategies from both literatures transfer to the other, yielding new market designs.

Cite as

Rafael Frongillo, Maneesha Papireddygari, and Bo Waggoner. An Axiomatic Characterization of CFMMs and Equivalence to Prediction Markets. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 51:1-51:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{frongillo_et_al:LIPIcs.ITCS.2024.51,
  author =	{Frongillo, Rafael and Papireddygari, Maneesha and Waggoner, Bo},
  title =	{{An Axiomatic Characterization of CFMMs and Equivalence to Prediction Markets}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{51:1--51:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.51},
  URN =		{urn:nbn:de:0030-drops-195795},
  doi =		{10.4230/LIPIcs.ITCS.2024.51},
  annote =	{Keywords: Convex analysis, Equivalence result, Axiomatic characterization, Market Makers, Prediction markets, Scoring rules, Cost-functions}
}
Document
Short Paper
Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper)

Authors: Daniel Britten, Vilhelm Sjöberg, and Steve Reeves

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)


Abstract
Using the DeepSEA system for smart contract proofs, this paper investigates how to use the Coq theorem prover to enforce that smart contracts follow the Checks-Effects-Interactions Pattern. This pattern is widely understood to mitigate the risks associated with reentrancy. The infamous "The DAO" exploit is an example of the risks of not following the Checks-Effects-Interactions Pattern. It resulted in the loss of over 50 million USD and involved reentrancy - the exploit used would not have been possible if the Checks-Effects-Interactions Pattern had been followed. Remix IDE, for example, already has a tool to check that the Checks-Effects-Interactions Pattern has been followed as part of the Solidity Static Analysis module which is available as a plugin. However, aside from simply replicating the Remix IDE feature, implementing a Checks-Effects-Interactions Pattern checker in the proof assistant Coq also allows us to use the proofs, which are generated in the process, in other proofs related to the smart contract. As an example of this, we will demonstrate an idea for how the modelling of Ether transfer can be simplified by using automatically generated proofs of the property that each smart contract function will call the Ether transfer method at most once (excluding any calls related to invoking other smart contracts). This property is a consequence of following a strict version of the Checks-Effects-Interactions Pattern as given in this paper.

Cite as

Daniel Britten, Vilhelm Sjöberg, and Steve Reeves. Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 3:1-3:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{britten_et_al:OASIcs.FMBC.2021.3,
  author =	{Britten, Daniel and Sj\"{o}berg, Vilhelm and Reeves, Steve},
  title =	{{Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts}},
  booktitle =	{3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
  pages =	{3:1--3:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-209-9},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{95},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.3},
  URN =		{urn:nbn:de:0030-drops-154272},
  doi =		{10.4230/OASIcs.FMBC.2021.3},
  annote =	{Keywords: smart contracts, formal methods, blockchain}
}
Document
Self-Confirming Price Prediction for Bidding in Simultaneous Ascending Auctions

Authors: Anna Osepayshvili, Michael Wellman, Daniel Reeves, and Jeffrey MacKie-Mason

Published in: Dagstuhl Seminar Proceedings, Volume 5011, Computing and Markets (2005)


Abstract
Simultaneous, separate ascending auctions are ubiquitous, even when agents have preferences over combinations of goods, from which arises the emph{exposure problem}. Little is known about strategies that perform well when the exposure problem is important. We present a new family of bidding strategies for this situation, in which agents form and utilize various amounts of information from predictions of the distribution of final prices. The predictor strategies we define differ in their choice of method for generating the initial (pre-auction) prediction. We explore several methods, but focus on emph{self-confirming} predictions. An agents prediction of characteristics of the distribution of closing prices is self-confirming if, when all agents follow the same predictor bidding strategy, the final price distributions that actually result are consistent with the utilized characteristics of the prediction. We extensively analyze an auction environment with five goods, and five agents who each can choose from 53 different bidding strategies (resulting in over 4.2 million distinct strategy combinations). We find that the self-confirming distribution predictor is a highly stable, pure-strategy Nash equilibrium. We have been unable to find any other Nash strategies in this environment. In limited experiments in other environments the self-confirming distribution predictor consistently performs well, but is not generally a pure-strategy Nash equilibrium.

Cite as

Anna Osepayshvili, Michael Wellman, Daniel Reeves, and Jeffrey MacKie-Mason. Self-Confirming Price Prediction for Bidding in Simultaneous Ascending Auctions. In Computing and Markets. Dagstuhl Seminar Proceedings, Volume 5011, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)


Copy BibTex To Clipboard

@InProceedings{osepayshvili_et_al:DagSemProc.05011.14,
  author =	{Osepayshvili, Anna and Wellman, Michael and Reeves, Daniel and MacKie-Mason, Jeffrey},
  title =	{{Self-Confirming Price Prediction for Bidding in Simultaneous Ascending Auctions}},
  booktitle =	{Computing and Markets},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5011},
  editor =	{Daniel Lehmann and Rudolf M\"{u}ller and Tuomas Sandholm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05011.14},
  URN =		{urn:nbn:de:0030-drops-2020},
  doi =		{10.4230/DagSemProc.05011.14},
  annote =	{Keywords: compact representation of games, congestion games, local-effect games, action-graph gamescomputational markets; auctions; bidding strategies}
}
  • Refine by Author
  • 1 Britten, Daniel
  • 1 Frongillo, Rafael
  • 1 MacKie-Mason, Jeffrey
  • 1 Osepayshvili, Anna
  • 1 Papireddygari, Maneesha
  • Show More...

  • Refine by Classification
  • 1 Computer systems organization → Distributed architectures
  • 1 Mathematics of computing → Information theory
  • 1 Security and privacy → Logic and verification
  • 1 Theory of computation → Algorithmic game theory

  • Refine by Keyword
  • 1 Axiomatic characterization
  • 1 Convex analysis
  • 1 Cost-functions
  • 1 Equivalence result
  • 1 Market Makers
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2005
  • 1 2021
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail