Superoptimization as a service, literature review and feasibility study.

gistfile1.txt

Superoptimization as a service, literature review and feasibility study.

Thesis: SOaaS provides a cloud-based superoptimization service for
reducing the execution and transaction costs of smart
contracts. Paradigmatically, SOaaS would analyze an EVM program and
minimize the resources necessary to execute it. This is generally, but
not always, proportional to code size, as measured in number of EVM
machine instructions.

Potential competitor:

The Supercompiler.xyz [0] team rebranded to Soteria [1], and then
Sec3 [2]. At first, they were pursuing Ethereum smart contract
superoptimization (possibly empoloying supercompilation techniques)
for purposes of minimization resource consumption, under a
justification of environmentalism. Soteria and Sec3 appear to be
focused on security analysis (also following a
cloud-based/as-a-service business model), and while they mention the
GreenCore paper, it does not appear to be central to their work.

[0] https://supercompiler.xyz/greenpaper.pdf

> We introduce a new solution, GreenCore, that alleviates this problem
based on optimization theories of computer programs. GreenCore
analyzes the deployed bytecodes of a smart contract and automatically
optimizes its gas cost on every code path. We discuss its design,
implementation and the opportunities it provides for the future. We
further develop GreenSwap, by optimizing the popular Uniswap protocol,
and find that it significantly reduces transaction fees on Ethereum by
over 30% on average compared to Uniswap.

https://news.ycombinator.com/item?id=28083404
https://web.archive.org/web/20210820143352/http://greenswap.tech/


[1] https://twitter.com/msuiche/status/1485647241100644353

[2] https://www.sec3.dev/blog/soteria-a-vulnerability-scanner-for-solana-smart-contracts
https://medium.com/coinmonks/soteria-a-vulnerability-scanner-for-solana-smart-contracts-cc202cf17c99
https://medium.com/@sec3.dev
https://github.com/sec3dev/pro-action
> This Github action conducts security auditing for Solana smart
contracts using the Sec3 Premium (formerly Soteria) tool.

Superoptimization of smart contracts:

https://www.researchgate.net/publication/344994018_Synthesis_of_Super-Optimized_Smart_Contracts_Using_Max-SMT

> the synthesis of optimized blocks which, by means of an efficient
Max-SMT encoding, finds the bytecode blocks with minimal gas cost
whose stack functional specification is equal (modulo commutativity)
to the extracted one. Our experimental results are very promising: we
are able to optimize 55.41 % of the blocks, and prove that 34.28 %
were already optimal, for more than 61000 blocks from the most called
2500 Ethereum contracts.

https://di.ku.dk/english/event-calendar-2021/coplas-albert-superoptimization-of-optimized-smart-contracts/

> Elvira is professor at Complutense University of Madrid.  See
http://costa.fdi.ucm.es/~elvira/ for more information

https://arxiv.org/pdf/2005.05912.pdf
https://jnagele.net/publications/Nagele-Schett-LOPSTR19.pdf

> Our aim is to superoptimize EVM bytecode by encoding the operational
semantics of EVM instructions as SMT formulas and leveraging a
constraint solver to automatically find cheaper bytecode. We implement
this approach in our EVM Bytecode SuperOptimizer ebso and perform two
large scale evaluations on real-world data sets.

https://arxiv.org/html/1908.06723

> Modelling and Verifying Bitcoin Contracts
> BitML, a high-level DSL for smart contracts with a computationally
sound compiler to Bitcoin transactions.

More formal methods than superopt, BitML may be interesting as a
computational model to optimize.

Cloud-based superoptimization:

https://ieeexplore.ieee.org/document/8906721

> In this paper, we propose a cloud-based super-optimization method as
Software-as-a-Service (SaaS) to reduce the cost of parallel
programming. In addition, it increases the utilization of the
processing capacity of the multi-core processor. As the result, an
intermediate programmer can use the whole processing capacity of
his/her system without knowing anything about writing parallel codes
or super compiler functions by sending the serial code to a cloud
server and receiving the parallel version of the code from the cloud
server. In this paper, an evolutionary algorithm is leveraged to solve
the scheduling problem of tiles. Our proposed super-optimization
method will serve as software and provided as a hybrid (public and
private) deployment model.

https://www.researchgate.net/publication/339443388_Superoptimization_of_WebAssembly_Bytecode
> Motivated by the fast adoption of WebAssembly, we propose the first
functional pipeline to support the superoptimization of Web-Assembly
bytecode. Our pipeline works over LLVM and Souper. We evaluate our
superoptimization pipeline with 12 programs from the Rosetta code
project. Our pipeline improves the code section size of 8 out of 12
programs. We discuss the challenges faced in superoptimization of
WebAssembly with two case studies.

Superoptimization and ML/AI:

https://proceedings.mlsys.org/paper/2021/hash/65ded5353c5ee48d0b7d48c591b8f430-Abstract.html

> This paper presents a novel technique for tensor graph
superoptimization that employs equality saturation to apply all
possible substitutions at once. We show that our approach can find
optimized graphs with up to 16% speedup over state-of-the-art, while
spending on average 48x less time optimizing.

Superoptimization for machine learning.

https://deepai.org/publication/learning-to-superoptimize-real-world-programs

> In this paper, we propose a framework to learn to superoptimize
real-world programs by using neural sequence-to-sequence models. We
introduce the Big Assembly benchmark, a dataset consisting of over 25K
real-world functions mined from open-source projects in x86-64
assembly, which enables experimentation on large-scale optimization of
real-world programs.

https://iitd-plos.github.io/superopt.html

> We are working on an automatic "peephole superoptimizer", an idea
  that is described in detail in this paper on Automatic Generation of
  Peephole Superoptimizers. While this work automatically generated
  peephole optimizations through search-based (AI/ML) techniques,
  later work on binary translation extended these ideas to
  automatically generate translations from one ISA (PowerPC) to
  another (x86).

Superoptimization productization:

https://ossg.bcs.org/blog/tag/superoptimization/

> During the summer of 2014, Innovate UK funded a feasibility study to
see whether any of these techniques were commercially viable. The good
news is that some techniques could now, or with a modest amount of
further industrial R&D, offer exceptional benefit for real-world
software.

Feasibility study ran in the UK in 2014, produced the MAGEEC project.

https://www.embecosm.com/services/superoptimization/
Stated interest in superoptimization is the reduction of energy
consumption.

Superoptimization in general:

https://stackoverflow.com/questions/6092146/where-to-learn-about-bit/6092814#6092814
https://stackoverflow.com/questions/31064370/superoptimization-gcc
https://stackoverflow.com/questions/19245574/how-to-implement-a-superoptimizer
https://codegolf.stackexchange.com/questions/12664/implement-superoptimizer-for-addition
https://stackoverflow.com/questions/44703441/proving-equivalence-of-programs
-Approaches the border between sup-opt and sup-com.
https://blog.regehr.org/archives/923
-Stochastic superoptimization.
https://github.com/twhume/superoptimiser
-Superoptimizer for the JVM, written in Clojure.
https://louisjenkinscs.github.io/survey/Compiler_Optimization_via_Superoptimization.pdf
https://www.deepdyve.com/lp/association-for-computing-machinery/scaling-up-superoptimization-11UXtplHdi

Super{optimization, compilation}

Superoptimization [0] differs from supercompilation [1] insofar as the
former is concerned with maximizing concrete performance, while the
latter is a transformation applied to source code that computes all
values known at compile time, i.e., it produces the maximally reduced
partially evaluated form. Supercompilation may have benefits for
superoptimization, but sup-opt is unconcerned with determining values
at compile time per se, except insofar as doing so affects
performance. Additionally, the models of computation are
conventionally distinct, with sup-opt targeting machine instruction
models, and sup-com abstract syntax trees. Both are examples of the
use of metasystems [2], which encompass the object system under
consideration in order to analyze and manipulate it.

[0] https://en.wikipedia.org/wiki/Superoptimization

[1] https://en.wikipedia.org/wiki/Metacompilation

[2] https://en.wikipedia.org/wiki/Metasystem_transition