zama-ai / bounty-program

Zama Bounty Program: Contribute to the FHE space and Zama's open source libraries and get rewarded 💰
https://zama.ai
244 stars 14 forks source link

Randomized Testing of Concrete Compiler #9

Closed alpaylan closed 1 year ago

alpaylan commented 1 year ago

Zama Bounty Program: Proposition

Description:

Introduction

Compiler correctness is one of the grand challenges of computer science[1]. One approach to correctness is formal verification, yet creation and maintenance of formally verified software is still an active research problem. Another approach is to use random testing techniques such as Property-Based Testing and Fuzzing. These techniques are used to randomly generate and execute programs, effectively discover the input space much better than any human manually could. They have been used in a variety of different applications in different languages; today, all major mainstream programming languages host well-supported libraries for both fuzzing and property-based testing.

Property-Based Testing

Property-Based Testing(PBT) has emerged from Haskell's QuickCheck in 2000, and quickly popularized in many different languages over the years. Today, major projects like pandas, numpy, PyPy uses a Python library for PBT, Hypothesis, to test their programs[3][4].

Property-Based Testing allows for fine grained control over the generated data, expert users can create their own generators, push them into the parts of the input space they find interesting.

Fuzzing

Fuzzing, or Fuzz Testing, is a method for randomly discovering input space of programs, similar to PBT. Popularized by AFL(American Fuzzy Lop)[5], fuzzers have seen a plethora of interest in the last decade. They have been used in compiler testing [2], browser testing, operating system testing... They have been used to successfully discover bugs in virtually all types of software in any domain.

Concrete

Concrete is the TFHE compiler developed by Zama that converts Python programs into FHE equivalents. Right now, Concrete tests are developed as unit tests in the style of expected input-output pairs, or circuit/function equivalence is checked with statically provided inputs.

Proposal

I propose to gradually migrate concrete-python tests into the PBT style, with the possibility to later adopt fuzzing to enhance the effectiveness of testing.

aquint-zama commented 1 year ago

Thanks for this proposal, we want to focus on use-cases and performances improvements for the moment as discussed together. Hope to see you soon with a new proposal.