Compiling Formality to the EVM
Cost of a beta-reduction: ~200 gas
The initial Ethereum back-end for Formality is deployed on version 0.1.239! That allows you to evaluate high-order, functional programs inside the blockchain. Here, I’ll document this new feature.
Compiling Formality to the EVM
Using the new compiler is simple. First, write a Formality program:
T Nat
| zero
| succ(pred : Nat)double(n : Nat) : Nat
case n
| zero => zero
| succ => succ(succ(double(n.pred)))main : Nat
double(succ(succ(succ(succ(zero)))))
Here, main is a pure function that doubles the natural number 4. Note this is just an example of algebraic datatype manipulation: for actual numbers you’d obviously use native ints instead. To compile this to Ethereum, save it as main.fm, then type fm -E main/main. This will output:
6023600060051b526022600160051b526003600260051b526042600360051b526003600460051b526062600560051b526003600660051b526082600760051b526003600860051b526013600960051b5263ffffffff6002600060005b8063ffffffff1415156106ff5782600f166101a10261007601565b6305f5b9f0505050505b8063ffffffff1415156100c55782600f166002148215166100a3575050506100c0565b6305f5b9f150600191508260041c60010160051b516000826100c6565b610080565b5b6106fa5600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005b6305f5b9f2508260041c60051b518063ffffffff146102415760041c8160041b9060051b52610243565b505b90506001908260041c60010160051b516000826001016106fa56000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005b6305f5b9f3508260041c60051b516305f5b9f45080600f166001146103df5760008261045d565b6305f5b9f5508060041c60051b518063ffffffff1415610405576305f5b9f7505061041f565b6305f5b9f6508460041c60010160051b519060041c60051b525b6305f5b9f85060041c60010160051b51925050508163ffffffff141561044c57806000526000600061045c565b8360041c830160051b5290506000905b5b6106fa56000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005b6305f5b9f95063ffffffff59525960011c8360041c60550261057701565b80607001595280602101595263ffffffff595280604101595280606001595280606201595263ffffffff595263ffffffff595260016106cb560000000000000000000000000000000000000000000000000000005b80603001595280602101595263ffffffff595263ffffffff595260016106cb56000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005b80604001595280602201595280604201595280606101595263ffffffff5952601359528060d0015952806082015952600359528060a2015952600359528060c20159526023595263ffffffff595260016106cb565b6023595280602201595260035952806042015952600359528060620159526003595280608201595260035952601359526002000000000000000000000000000000000000000000000000000000000000000000005b01925050508163ffffffff14156106e95780600052600060006106f9565b8360041c830160051b5290506000905b5b61005b565b00That is an Ethereum bytecode that, when evaluated, will reduce a pure Formality program inside the blockchain and leave, on the contract’s memory, the result of that computation. So, for example, on the program above, it will leave, on the memory, the natural number 8, using Formality’s lambda byte representation.
How much it costs?
The program above costs 37750 gas on Ethereum’s blockchain. For a comparison, when reduced through interaction nets (the optimal algorithm for the reduction of high-order functions), it costs 141 graph-rewrites. That gives us approximately 267 gas per beta-reduction, which is really low: only 33x more than a native MULMOD, and the same as one SLOAD. Note this average includes everything, even the cost of loading the terms to memory: an actual beta-reduction, in isolation, is even cheaper.
Of course, graph-rewrites include more than just beta-reductions, there is also the cost of copying data. As such, the average actually varies from 150 to 400 gas per beta-reduction, depending on the input term. While this isn’t as cheap as Solidity, it does allow us to run formally verified, elegant functional programs with a perfectly acceptable cost. I’d go as far as saying it almost obsoletes the concept of “functional blockchains” (specially when they don’t even include a proper proof language), but I don’t want to start a flame war!
Limitations, future work
Right now, this just evaluates pure programs on Ethereum. There is no smart-contract integration yet. An ABI-compliant, side-effective runtime is needed for that. When that is done, we will make a new blog-post explaining how to deploy formally verified Formality programs to Ethereum. Right now, if you want to use it in a smart-contract, you’ll need to manually do the interface.
This is also only compatible with the fastest subset of Formality, that of affine terms. The type-checker will let you know if your program is eligible by marking its type with an 𝒜. The documentation includes hints on how to make affine programs. Native numbers aren’t available yet, but will be added soon. In a future, elementary and exponential programs might be added too, but those will probably be too slow to be worth anyway.
This feature compiles native Formality programs directly to Ethereum, including full high-order functions and closures. This is, as far as I know, the first time such a thing was done reasonably efficiently. If someone is interested in getting the most performance possible, he/she might not be able to afford evaluating closures inside the blockchain. In that case, a more conservative and faster approach of compiling a formally-verified first-order DSL might be preferred. We’ll explain how to do so in a future.
Example
A complete example is available on this Github repository. It compiles a Formality program to EVM bytecode, runs it inside the EVM and decompiles the memory back to recover the normalized term. Try it!
