search

runtimeverification / michelson-semantics

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

Add `xtz_to_token`, `token_to_xtz` spec #252

Closed sskeirik closed 3 years ago

sskeirik commented 3 years ago

Note: currently this PR only includes the positive case. The negative case is still pending.

All of the main assumptions should be present for the positive case to go through (assuming backend support). The main trick will be adding additional uninterpreted functions to prevent the backend from crashing with DecidePredicateUnknown.

Fixes: #218 Fixes: #248