2026-07-22T19:33:58Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16739 2024-03-06T10:58:11Z ddc:004 open_access

Formalizing Algorithmic Bounds in the Query Model in EasyCrypt Stoughton, Alley Chen, Carol Gaboardi, Marco Qu, Weihao query model lower bound upper bound adversary argument EasyCrypt 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alley Stoughton and Carol Chen and Marco Gaboardi and Weihao Qu 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.30 urn:nbn:de:0030-drops-167399 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.30 eng https://creativecommons.org/licenses/by/4.0/legalcode