Expired
Milestone
Nov 14, 2022鈥揘ov 25, 2022
Michelson without simulations
The goal of this milestone is to have a formalization of Michelson without the use of dependent simulations. Despite being useful to have a formalization of Michelson without cast
, the simulations were hard to maintain to follow the protocol updates. In this milestone, we will attempt to remove all the simulations and replace them with equivalent lemmas/properties directly on the types from OCaml.
We will do these tasks on a branch michelson-without-simulations
that we can merge once we are confident.