License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.30
URN: urn:nbn:de:0030-drops-167399
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16739/
Go to the corresponding LIPIcs Volume Portal

Stoughton, Alley ; Chen, Carol ; Gaboardi, Marco ; Qu, Weihao

Formalizing Algorithmic Bounds in the Query Model in EasyCrypt

pdf-format:
LIPIcs-ITP-2022-30.pdf (0.7 MB)

Abstract

We use the EasyCrypt proof assistant to formalize the adversarial approach to proving lower bounds for computational problems in the query model. This is done using a lower bound game between an algorithm and adversary, in which the adversary answers the algorithm’s queries in a way that makes the algorithm issue at least the desired number of queries. A complementary upper bound game is used for proving upper bounds of algorithms; here the adversary incrementally and adaptively realizes an algorithm’s input. We prove a natural connection between the lower and upper bound games, and apply our framework to three computational problems, including searching in an ordered list and comparison-based sorting, giving evidence for the generality of our notion of algorithm and the usefulness of our framework.

BibTeX - Entry

@InProceedings{stoughton_et_al:LIPIcs.ITP.2022.30,
  author =	{Stoughton, Alley and Chen, Carol and Gaboardi, Marco and Qu, Weihao},
  title =	{{Formalizing Algorithmic Bounds in the Query Model in EasyCrypt}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{30:1--30:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16739},
  URN =		{urn:nbn:de:0030-drops-167399},
  doi =		{10.4230/LIPIcs.ITP.2022.30},
  annote =	{Keywords: query model, lower bound, upper bound, adversary argument, EasyCrypt}
}

Keywords: query model, lower bound, upper bound, adversary argument, EasyCrypt
Collection: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue Date: 2022
Date of publication: 03.08.2022
Supplementary Material: EasyCrypt Frameworks for Proving Algorithmic Bounds:
Software (Source Code): https://github.com/alleystoughton/AlgorithmicBounds

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI