search

runtimeverification / michelson-semantics

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

Add `token_to_token` spec #250

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: #249

hjorthjort commented 3 years ago

Looks like this runs into ErrorDecidePredicateUnknown on a small non-linear expression. We should get this fixed in the backend (splitting on Z3 reporting unknown rather than throwing an error). In the meanwhile, we should be able to work around it by rewriting the expression(s) in question to an uninterpreted function.

ehildenb commented 3 years ago

Can the tokens here be arbitrary contracts? If so, is that a problem for the entry-point issues? Let's double-check (and document) whether the fact that we aren't verifying entry-points is an issue for these proofs.