Polynomial Identity Language
Polynomial Identity Language (PIL) is a domain-specific language (DSL) created to provide developers with a holistic framework for constructing programs through an easy-to-use interface, and abstracting the complexity of proof/verification mechanisms. In the zkEVM context, PIL is the very DNA of verification.
One of the main peculiarities of PIL is its modularity, which allows programmers to define parametrizable programs called
namespaces. Developers can therefore create their own custom namespaces and instantiate them from larger programs or some public library.
The advantage of building modular programs makes for easy testing, reviewing, auditing, and formally verifying even larger and complex programs. Some of the keys features of PIL are:
namespacesfor naming the essential parts that constitute programs
- Denoting whether the polynomials are
- Expressing polynomial relations, including
- Specifying the type of a polynomial, such as
However, recent proof systems such as STARKs have shown that arithmetic circuits might not be the best computational models for all use cases. For example, given a complete programming language, computing a valid proof for a circuit satisfiability problem may result in long proving times due to the overhead of re-used logic.
By opting for deployment of programs with their low-level programming, shorter proving times are attainable, especially with the advent of proof/verification-aiding languages such as PIL. Hence the decision to adopt state machines as the best computational model for the Polygon zkEVM.