Add semantics of entrypoints

runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.

Other

17 stars 6 forks source link

Closed sskeirik closed 3 years ago

sskeirik commented 3 years ago

If this is merged after #226, we need to update the update token pool spec to correct how entrypoints are handled.

Fixes: #231

hjorthjort commented 3 years ago

I've created new issues and cards for the 4 different things this PR does:

Changing #DoCompare, with related proof and tests updates
Changing paramtype cell and the SELF instruction, with related proofs and tests updates
Changing knownaddrs and the CONTRACT and TRANSFER_TOKENS instructions, with related proofs and tests updates
Changing the sort structure of Address to not include String, with related proofs and tests updates