README.md
# `Tezos_benchmark_alpha`
This library is dedicated to sampling Michelson values and in particular
Michelson programs.
## Architecture
This library provides a sampling-based interface for well-typed
Michelson generation. Internally, this library is built on a sampler for an
intermediate language called Mikhailsky post-composed with a function to
map Mikhailsky terms to Michelson ones.
### Layer 1: Mikhailsky
Mikhailsky corresponds to "Michelson with typed holes". Mikhailsky terms
are encoded inside Micheline. The library `lib_benchmark_type_inference`
provides the language definition as well as a type inference engine.
### Layer 2: Sampling Mikhailsky terms
We sample Mikhailsky terms using a Markov chain where transitions correspond
to local rewriting rules. The state space of the Markov chain is defined
in `State_space` module. The rewriting infrastructure is provided in the
`Kernel` module by instantiating `lib_micheline_rewriting`.
Rewrites are checked to preserved well-typedness in the Mikhailsky sense
using the type inference engine provided with Mikhailsky. The `Rules`
module defines all rewriting rules, for both Mikhailsky _programs_
(submodule `Rules.Instruction`) and _data_
(submodule `Rules.Data_rewrite_leaves`). The function `Rules.rewriting`
performs the enumeration of possible rewritings.
The Markov chain is biased to sample terms of a specified
size using the Metropolis-Hasting functors provided by `StaTz`.
The instantiation of this Markov chain is defined in the `Sampler`
module.
### Layer 3:
Once we can sample Mikhaislky terms of a specified size, we need
to convert them to Michelson ones. This is performed in two steps.
- In the first step, we use the `Autocomplete` module to fill holes
in Mikhailsky terms (resp. data) with well-typed code (resp. data).
This is a relatively ad-hoc process.
- The last step is to convert Mikhaislky to Michelson using the
`Michelson` module.