search

runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.
Other
17 stars 6 forks source link

Add Liquidity Baking `tokenToXtz` spec #309

Closed sskeirik closed 3 years ago

sskeirik commented 3 years ago

This should be merged after #306 since it depends on it; i.e. only the last 3 commits are new.

Also, I changed the side-conditions on the tokenToXtz negative cases from what the former proof had, so be aware.

I also added several macros that are useful for calculating the burn fee.

nishantjr commented 3 years ago

I messed something up, and this cant be reopened. Created a new PR