Add Edo features
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
andNEVER
-
More comparables -
Restriction on FAILWITH
to packables (already on dev) -
promotion of UNPAIR
-
promotion of DUP n
-
KECCAK
andSHA3
-
LEVEL
-
VOTING_POWER
andTOTAL_VOTING_POWER
-
SELF_ADDRESS -
Legacy cleanup (already on dev)
Edited by Raphaël Cauderlier