Skip to content

Add Edo features

Raphaël Cauderlier requested to merge proto-proposal into dev

This MR is about bringing the features of the Edo proposal to Mi-Cho-Coq. This will be needed both to reason about contracts using the new Michelson features and to prove invariants of the Michelson language such as the non-duplicability of tickets.

  • Sapling
  • BLS12-381
  • Tickets
  • GET_AND_UPDATE
  • Combs
  • never and NEVER
  • More comparables
  • Restriction on FAILWITH to packables (already on dev)
  • promotion of UNPAIR
  • promotion of DUP n
  • KECCAK and SHA3
  • LEVEL
  • VOTING_POWER and TOTAL_VOTING_POWER
  • SELF_ADDRESS
  • Legacy cleanup (already on dev)
Edited by Raphaël Cauderlier

Merge request reports