EasyCrypt Framework for Proving Algorithmic Bounds in Query Model

This repository contains a general EasyCrypt framework for expressing computational problems in the query model, and for proving worst case lower bounds for computational problems using the adversarial method (adversary arguments), and proving worst case upper bounds for algorithms solving the computational problems.

This is joint work between Boston University faculty

• Mark Bun ([email protected])
• Marco Gaboardi ([email protected])
• Alley Stoughton ([email protected])

in collaboration with Boston University doctoral student and now Monmouth University faculty member

• Weihao Qu ([email protected])

and Stuyvesant High School student, BU RISE program intern, and now MIT undergraduate

• Carol Chen ([email protected])

Our preliminary work was reported in the 13th International Conference on Interactive Theorem Proving (ITP 2022) paper "Formalizing Algorithmic Bounds in the Query Model in EasyCrypt".

Our bounds framework is

• Bounds.eca - lower and upper bounds framework

and is supplemented by

• IntLog.ec - working with bounds involving integer logarithms
• FSetAux.ec - auxiliary lemmas on finite sets
• FRange.ec - finite ranges as sets
• AllLists.ec - generating all lists of given length over finite universe

We have applied our bounds framework to

• proving a lower bound for computing the or (disjunction) function of a list of booleans

• proving a lower bound for searching for the least index into an ordered list (in which duplicate elements are allowed) where a given element is located, as well as proving an identical upper bound for the binary search algorithm for this problem

• proving a lower bound for determining how a list of distinct elements must be permuted in order to be sorted, as well as proving an upper bound for the merge sort algorithm, where an algorithm may only query how elements are related, but not the elements' values themselves

There is also a shell script check-all-scripts for checking all theories using two SMT provers: Alt-Ergo and Z3. It uses a default SMT timeout of 2 seconds, but takes the timeout as an optional command line argument. The scripts check using versions 2.6.0 of Alt-Ergo and 4.15.3 of Z3. If you use later versions of these provers and an up-to-date version of EasyCrypt, feel free to report any script failures.