---
tags: EVM, precompiles, Ethereum2.0
---
# Verifiable Precompiled contracts (technical, WIP)

Allowing user code (smart contracts) to be executed during block-chain transactions enables tremendous possibilities, however, it can be dangerous, if implemented carelessly. As a more general rule, untrusted code should be executed in a safe way.

It's relatively easy to execute untrusted code using interpreters - code activity can be checked for unsafe behavior, resource consumption (e.g. step counts, memory usage) can be measured and constrained too. However, interpretation and checks inevitably slow down code execution.

While interpretation may be adequate in many cases (e.g. for executing business logic) and computation-hungry code should be normally put off-chain, there are cases where it's highly desired to be able to run heavy code inside block-chain transaction. One example is [Zero Knowledge Contingent Payment](https://en.bitcoin.it/wiki/Zero_Knowledge_Contingent_Payment). pZKP](https://en.wikipedia.org/wiki/Zero-knowledge_proof) code can be reasonably fast when compiled, but quite heavy when interpreted. While in a trust-less setup, ZKP verification should be run as a part of block chain transaction.

Compilation can improve performance tremendously. However, in a trustless environment, it's difficult to assure that both compilation process and compiled code behave in a safe way (JIT bombs). That is especially true in heterogeneous systems, where specialized compilers and optimizations are required. It's arguably very expensive to implement correctly.

One way to solve the problem is to compile only performance-critical parts of code. That can be done in several ways, for example, core execution environment (VM) can be extended with a set of trusted routines, which implementation is highly optimized. In the case of [Ethereum VM](https://github.com/ethereum/wiki/wiki/Ethereum-Virtual-Machine-(EVM)-Awesome-List), they are dubbed precompiled contracts.

However, adding and maintaining such code, which should be trusted, is resource consuming. Thus, it allows optimization of a quite limited set of cryptographic algorithms.

We propose a relatively lightweight way to accelerate execution of such untrusted user-defined code in a safe way. Therefore lowering resources required to extend the core execution environment with high-performance primitives. Our intention is to concentrate on cryptography primitives, however, the same or similar approach can help accelerate algorithms from other domains (e.g. numerical optimization, asset pricing, etc), which can be beneficial to be executed on-chain.

The main idea is to employ modern software verification technology to make sure that a user defined code can actually be trusted. To aid that, a user supplies executable contract specification along with security properties and appropriate proofs. Execution environment then can:
- check that specified security properties are sufficient
- run a proof checker to assure the specification satisfies the properties

The executable contract specification can be compiled then into C or any other target. Additionally, mechanical proofs can be constructed that the compiled code preserves the properties.

In general, the approach can be very resource consuming to implement. However, since we are mostly interested in accelerating cryptography primitives, we can limit expressiveness of the contract specification language, to simplify proof development. As cryptographic meta-parameters (like group/field order, elliptic curve parameters) in practical applications are usually fixed (e.g. standardized), one can require that every possible execution trace to be finite (or even bounded with a reasonable large constant), e.g. require that loops are bounded with small constants. Moreover, in the case of Ethereum VM, smart contract execution steps are bounded with gas limit (to prevent DoS attacks).

If program execution traces are bounded with a reasonable constant, then analysis of such programs can be done automatically. However, it may often be impractical, if such traces are long. So, in general more expressive languages are beneficial in the sense that they require more serious verification technology (e.g. [SMT-solvers](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) instead of [SAT solvers](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem) or bounded model checkers). So developing proofs will typically require human work, but as a result proofs will be shorter. Which approach is better is not clear right now, however, we believe that it's easier to start with a conceptually simpler bounded models and switch to more expressive ones, if needed. Hybrid approaches may be highly desired in practice.

# Preliminary considerations

## Terms and definitions

**Precompiled contact** - ??

**UDPC** - user-defined precompiled contract.

**meta-constant** - known before (any) compilation.

**constant** - known at compile time.

**(read-only) value** - known at runtime.

**variable** - its value can change during runtime.

**resource** - something that can be consumed and limited, e.g. execution steps, memory, storage (we ignore other resources). We assume that UDPC can consume only UDPC gas and memory. Memory usage is bounded by gas, e.g. each step can allocate a constant size memory only.

**fixed (bound) resource model** - resources consumed by a program are bounded by a constant (known at compile time). Static gas precompiled contract - bounded resource model.

**linear (bound) resource model** - resources consumed by a program are bounded by a linear function of its input size (linear combination of input parameters, in general), i.e. $a + b * <input var>$, where $a$ and $b$ are constants, i.e. known at compile time, $<input var>$ is known before invocation). Thus can be calculated before the program is executed. Dynamic gas precompiled contract - linear resource model.

**static memory** - initialized at compile/load time. Can be read. Can be written in theory, but security properties should be preserved then (e.g. static memory usage is bounded across multiple executions, deterministic execution regardless static memory modifications after initialization, etc)

## Execution model assumptions

Many security properties can be achieved by restricting specification language. As our main target is Ethereum VM, where contracts are already sandboxed, we make certain assumptions to accommodate this and simplify further reasoning.

A user defined precompiled contracts (UDPC) is a smart contract that can be called by EVM in the same way as a core precompiled EVM contract and should satisfy the following restrictions:
- there is one input parameter: a byte-array
- UDPC outputs a byte-array
- UDPC can use ephemeral memory, which is destroyed after UDPC execution is finished
- there is a gas consumption formula, which may depend on input size
- UDPC execution is sandboxed, i.e. it cannot affect execution of other contracts
- additionally, UDPC doesn't have contract storage. However, there can be UDPC specific cache (e.g. to store pre-calculated data) as a replacement.
- additionally, UDPC can only call other precompiled contracts (UDPC or EVM precompiles)
- UDPC resource usage (memory and execution steps) should be bounded

An important consequence is that most safety properties can be implicitly proved, if a UDPC can be successfully compiled.

### UDPC-specific cache (static memory)

Contract storage access is costly in EVM and it's hardly possible that it's required for cryptography primitives. A cache with pre-calculated data can be useful, however.
Under assumption that cryptographic meta-parameters are fixed (for a particular UDPC), a UDPC can have a cache of pre-calculated data (similar to C program's static data). Since, UDPC execution steps are to be bounded, it can be constructed during compilation (or when a UDPC is first loaded in memory). It can be accessed in read-only mode by the UDPC.

In general, write access during regular UDPC invocation can be allowed too (e.g. to gather statistics, for self-tuning), however, it complicated out model, so we ignore it for now. One problem with write access to the static cache is that there can be multiple regular UDPC invocations and thus, the static cache can grow unboundedly, in general. So, its memory should be explicitly bounded.

Another problem is that UDPC can change its behavior from invocation to invocation, even with the same input. For cryptography primitives, it's better to have a persistence behavior (any modifiers can be passed via an input parameter).

So, we assume that UDPC may have a static initialization code, which is run once and can allocate memory. Static initialization steps are limited and allocated memory thus is limited too. The memory can be read during UDPC invocation. But can be optionally written in debug mode (by debug code).

### Resource usage

In the Ethereum VM case, only execution steps are explicitly bounded with a gas limit. As a consequence, memory allocation is limited too (by EVM rules). We assume UDPC resources are bounded in a similar way, though UDPC gas can be different from EVM gas, as well as UDPC specification language can (and is highly likely to) be different from EVM.

As a UDPC can call EVM precompiles and UDPCs are to be called by EVM code, gas conversion rule should be defined. That can be done by measuring performance of a set of cryptography primitives implemented as UDPC and correlating it with the appropriate UDPC gas usage.

We assume that each instruction can allocate a memory chunk of a size. bounded by small constant (can be implementation dependent). So, total memory allocation is bounded by a linear function of execution steps (or gas). There can be explicit constructs to allocate large chunks, but they are treated as an implicit cycle, allocating fixed small chunks.

Thus, the only resource we care about is execution steps or gas.

## Fixed- and linear- bound resource models

Many cryptographic constructs accepts variable-size input (e.g. hash functions, ciphers, etc). They are typically defined as an application of fixed-input-size primitives in a loop or recursively. The resulting execution step count is often proportional to the input size, as a result.

While there can be case of quadratic (polynomial) dependency, such constructions are usually impractical, since they are inevitably slow on inputs of a considerably big size.

Since out main interest is accelerating cryptography primitives, we require that UDPC resource consumption is bounded by a linear function of parameters, known before UDPC invocation.

This assumption fits perfectly Ethereum VM gas pricing, where operations and precompiled contracts gas consumption is either fixed per operation or proportional to its input size (plus some constant). Thus, gas consumption can be predicted before operation or precompile execution and if gas limit is exhausted, smart contract execution is aborted. This effectively prevents DoS attacks.

So, in order to incorporate UDPC into EVM seamlessly, UDPC should follow the linear or fixed bound resource model

While linear model is more expressive, one may prefer to constrain oneself with the fixed bound resource model, since they may be easier to analyze, while they are still expressive enough, given that "variable" fragment can be implemented via a regular EVM contract.

In general, as gas usage formula is to be supplied, it dictates the resource constraint model: if gas formula is dynamic, then the linear resource model is used, else - the fixed-bound resource model.

# Safety properties

To allow execution of untrusted UDPC code in a safe way, appropriate safety criteria/properties should be specified. They consist of two categories: sandboxed execution and bounded resource usage. We have already discussed both categories.

Many safety properties can be enforced on a specification language level:
- no recursion or mutual recursion
- UDPC can access only specified set of arrays: input array, own dynamic memory, own static memory, etc
- read-only access to certain arrays, e.g. static memory during regular UDPC invocations, input array can be read-only too
- a UDPC can only invoke other UDPCs or EVM precompiled contracts
- no explicit memory allocation, fixed-size chunks can be implicitly allocated by some instructions (similar to EVM)
- loops bounds can be constrained (e.g. constant bounds or linear formula of input parameters)

So, if a UDPC has been successfully compiled, then certain safety properties are already proved. The user has to supply proofs for remaining properties only. These can be:
- array bounds are respected
- UDPC gas usage formula is an upper bound of (UDPC gas-weighted) execution steps
- auxiliary loop invariants and lemmas (can help proving other properties)

The remaining properties can be enforced in runtime, however, they will inevitably lead to slow down, so mechanically checkable proofs are introduced to avoid these runtime checks.

A hybrid approach can be implemented, where runtime checks are implemented only when no appropriate proof found. E.g. busy loops can have necessary proofs (including gas increment for the whole loop), while top-level loop can be relatively insensitive to additional checks.

In general, gas usage formula is a program and it's evaluation should be bounded too. We are assuming for now that any gas usage formula is linear (affine) relative to input size (e.g. measured in full 32 byte words), analogous to EVM dynamic gas usage formulas.

# Specification and implementations

In heterogeneous environment, processors can have different execution capabilities, which may need specific optimizations to exploit particular hardware instruction sets and memory configurations (e.g. cache sizes).

One example is that for different input parameters, different algorithms can be appropriate (e.g. unroll loops to fit cache size). Some ISA support vector instructions, so vectorized code can be much faster, which can have different flow graph.

One should separate (executable) UPDC specification and implementations. This can be supported in the proposed UDPC framework. For example, initially a direct translation of UDPC specification can be used. Later, optimizations for certain hardware can be proposed.

To allow swapping implementations is a safe way, implementation proposer can supply a proof that the particular implementation is equivalent to the corresponding implementation (including its security properties).

A particular EVM implementation can choose between several optimized implementations, depending on hardware capabilities (can choose, based on performance measurements, for example).

# Implementation considerations

There are several core activities:
- a UDPC submitter should:
- write UDPC code and specification (e.g. gas usage formula, invariants)
- construct proofs
- a proof-checker should:
- verify the proofs
- compile the code

If a UDPC is to be introduced during a blockchain transaction, then proof-checking and compilation to native code should both be resource bounded (which can be a problem, in general).
If a UDPC is to be approved by a committee first, then proof-checking and compilations should be decidable and reasonably practical. Though they can be semi-decidable, in theory, but it's not reasonable (prof-checking is a simpler problem).

Several aspects should be developed in more details, however, we just cover them briefly in the post:
- verification technology:
- formal logic, its fragments
- tools (solvers, proof assistants)
- verification conditions (VCs)
- translation technology
- target language
- compiler(s)
- optimizations
- VC generation
- code specification language
- standalone vs DSL
- macro/templates/compile-time calculations

In general, as we are targeting cryptography primitives domains, less expressive but effectively analyzable are highly preferred at the beginning. Though more expressivity can be added later to support code maintenance and more advanced features, like multiple implementations of one spec.

## Verification technologies

There is a tradeoff between language expressiveness and analyzability. More expressive language in general means it's easier to write programs, but more difficult to reason about its behavior. As pointed out before, at the beginning analyzability is a strong preference in order to make it more accessible to a general audience. A less expressive but fully analyzable language still allows to implement many interesting cryptographic primitives.

### Proof-checking vs proof construction

Proof-checking is a simpler problem then proof construction. It should be decidable and it may be required that proof-checking should be also fast and predictable, i.e. can be done in a linear time regarding proof and code length.

Proof construction can be much more complex problem, which is not decidable, in general. That means manual or semi-automatic proof construction can be required (which will be a problem for a general audience).

### Formal logics and their fragments

[Halting problem](https://en.wikipedia.org/wiki/Halting_problem) is undecidable for a [Turing-complete](https://simple.wikipedia.org/wiki/Turing_complete) languages. Even if some theory is decidable, like [Presburger arithmetic](https://en.wikipedia.org/wiki/Presburger_arithmetic), it may be impractical, in general case, because decision procedure can be extremely slow in worst cases. There exist practical decidable fragments though.

We assume the following "decidability" hierarchy of logics, their fragments and supporting tools:
- decidable and (mostly-)practical, like propositional logics, SAT-solvers and decidable fragments of SMT-solver's logics
- semi-decidable, like First Order Logics, e.g. SMT-solvers, in general
- Higher Order Logics, Type theory, proof assistance are required with manual or semi-automatic proof development

#### Decidable problems

One way to resolve the problem is to choose a fragment which is [decidable](https://en.wikipedia.org/wiki/Decidability_(logic)#Some_decidable_theories) and practical at the same time. For example, one may transform UDPC to a [SAT-problem](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem) or to a decidable fragment supported by [SMT-problem](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) and try to solve it with appropriate solvers.

In many cases, it can work fine. For example, we have already discussed that fixed-length input crypto primitives will be specified using fixed bound resource model, e.g. execution steps are bounded by a constant (known at compile time). Such primitive can be specified using loops with fixed constant bounds and the loops can be unrolled. Many crypto algorithms are designed so that their code can fit processor caches, when loops are unrolled, so it's pretty reasonable assumption.

After loops are unrolled, a control flow graph becomes a (perhaps) big [Directed Acyclic Graph](https://en.wikipedia.org/wiki/Directed_acyclic_graph), which can be traversed within finite steps, though it can required lots of memory/execution steps, in general. A node in the DAG corresponds to a linear block of instructions, without branches, with the exception of the last instruction. If there are several links from a node, that corresponds to a conditional branch.

So, the resulting DAG s of reasonable size, then proof construction can be practical in many cases. E.g. the DAG can be converted to a set of paths from a root to final states. Each path has a set of conditions, that are true, if the path is chosen, and a sequence of simple instructions (without branching ones, because they are eliminated when enumerating paths). As there are no cycles, the set is finite and each path is finite too. So, each path can be checked for array bounds violations, gas limit can be calculated, etc.

Given two control flow DAGs, they can be checked whether they produce compatible results (e.g. an implementation conforms to the specification).

In general, time required to process such DAGs can be huge, so, certain optimizations are required. Thus the approach is attractive, but requires an evaluation.

#### Semi-decidable problems

There are several SMT-solvers, which are practical to analyze real-world problems. The problem is that they are semi-decidable, which means a solver can fail to find an exact answer. That means a user should have quite specific skills and training to investigate the problem and develop as solution: either to re-write code or supply hints/lemmas to the solver.
However, it can turn to be more practical in a mid term, since crypto-primitives can be developed by engineers with appropriate skills.

The same argument applies to [HOL](https://en.wikipedia.org/wiki/Higher-order_logic)/[Type Theory](https://en.wikipedia.org/wiki/Type_theory) approaches, which are even more powerful and arguably require more advanced skills.

## Specification language

Developing a new language and learning it can be a serious problem, so we believe it makes sense to leverage an existing language. [Vyper](https://vyper.readthedocs.io/en/latest/) looks like the best match currently, since it follows very similar philosophy:
> Because of this Vyper provides the following features:
> - Bounds and overflow checking: On array accesses and arithmetic.
> - Support for signed integers and decimal fixed point numbers
> - Decidability: It is possible to compute a precise upper bound for the gas consumption of any Vyper function call.
> - Strong typing
> - Small and understandable compiler code
> - Limited support for pure functions: Anything marked constant is not allowed to change the state.

Therefore, it makes sense to extend Vyper, for example, introduce `@precompiled` or `@precompiled(fixed|linear)` decorators and modify Vyper compiler appropriately.

## Compilation to a target language

For simplicity, we assume that UDPC code will be initially translated to C. Other targets are possible too, e.g. LLVM, Rust, etc.

# Concluding notes

This is a preliminary proposal to formulate a general idea, without digging deep into details. There are many choices to be made, but they require investigation and experimentation. If the idea is decided to be useful, we will conduct further research, e.g. a prototype implementation of a fixed-bound fragment using [Vyper](https://vyper.readthedocs.io/en/latest/) as a base language.

<!--
# Drivel Quarantine (do not read)

### Unbounded loop models

It can be extremely inconvenient to express them in a bounded loop model.
So, we assume that the bounded loop model is appropriate for fixed input cryptographic primitives only. The variable input functions are assumed to be implemented in EVM, invoking fixed-input UDPC. Dynamic gas formula is not needed for fixed input size primitives.

As it may be desired to have variable-input-size UDPC, the model can be extended to have loops bounds which are linear to the input size. That will complicate reasoning and proofs, in general. However, certain restrictions can be applied to simplify reasoning, for example. no nested variable-count loops are allowed. So, if there is only one loop which step count is proportional to the input size, then total execution steps is linear to the input size.

A similar approach can be done with memory allocation, i.e. allocation of memory chucks proportional to the input size is allowed and treated as a variable-size loop, i.e. which cannot be nested inside other veriable-step loop.

Invocation of variable-input-size UDPC is treated as variable-step loop too.

### Resource-model reductions

We assume very simple model, which can be inconvenient to end users. However, certain code transformations can be used to convert syntactic sugar to our model.

We assume no recursion.
We assume there is only one program (an additional program can be used to initialize static memory, though). I.e. any sub-programs are inlined.
Each instruction can allocate only a constant memory chunk.
Array bounds are not implicitly checked and should be proved. A very simple approach is to guard array access with an appropriate check.

There is an input array.
There is UDPC dynamic memory. And read-only static memory.
Output array is a part of UDPC memory (i.e. specified by an offset and a length).
As subprograms are inlined, there is a constant-size stack.
-->