Miscellaneous updates to liquidity baking spec

runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.

Other

17 stars 6 forks source link

Miscellaneous updates to liquidity baking spec #306

Closed sskeirik closed 3 years ago

sskeirik commented 3 years ago

Updates include:

fix entrypoint syntax
add #XtzBurn macro for representing burn fee calculations
add missing burn txns for conversion entrypoints
add kast script for lb specs and kmich support
mark unused variables to quiet warnings

EDIT: In my history, this is on top of #308, but technically, they don't depend on each other at all, so this could be merged first, if that would be more helpful. I am hopeful that, after this latest round of fixes, the updated Dexter specs should pass.

sskeirik commented 3 years ago

So, this PR has slowly grown in time as I have fixed several issues. One thing that I changed in Dexter that I want to change in LB is I renamed #XtzBought to #CurrencyBought since it is used when purchasing tokens or when purchasing XTZ.

As I was doing the token-to-xtz proof, I found I made a mistake in the local entrypoints syntax, which should now be fixed in Dexter in LB.

nishantjr commented 3 years ago

So, this PR has slowly grown in time as I have fixed several issues. One thing that I changed in Dexter that I want to change in LB is I renamed #XtzBought to #CurrencyBought since it is used when purchasing tokens or when purchasing XTZ.

Lets limit the scope of this PR. This should only set up the infrastructure for LB so that we can start working on claims in parallel. I'm OK with merging this after one test claim is working.