search

runtimeverification / michelson-semantics

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

Add Liquidity Baking `tokenToXtz` spec #311

Closed nishantjr closed 3 years ago

nishantjr commented 3 years ago

Reopened version of #309

@sskeirik I've pushed another commit that combines the negative cases. We shouldnt need multiple negative cases since we were able to fix the flakiness issue. The new combined negative case uses the negation of the positive case's side conditions as its side condition. This does not go through, implying that the side condition of the positive case is too tight (or possibly that some additional axioms are needed).

sskeirik commented 3 years ago

Given that we already have a working version of this, I'm closing this branch. We can polish the proof later as part of a separate PR, if we still want to.