runtimeverification / michelson-semantics

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

Equality check needed for all datatypes for symbolic unit tests #105

Open sskeirik opened 4 years ago

sskeirik commented 4 years ago

For symbolic unit tests, we would like a way to check equality of all data types.

For example, there is no way to check equality between two operation values, which may be needed to successfully run some tests. There is also no convenient way to check equality between maps, lists, sets, etc...

There are two ways to handle this issue:

1) Overload the COMPARE instruction so that is has an extended semantics ONLY when executing in the precondition, postcondition, or invariant contexts. 2) Create a new instruction (for example EQUAL) that performs equality checking over all datatypes.

sskeirik commented 4 years ago

NOTE: these types are becoming comparable in version 7: pair, or, option, unit. chain_id, mutez, key, key_hash, and signature (and possibly others).

Also, note that bytes are always comparable --- this means any packable type can be given a comparison and equality check via this method --- but this approach feels off --- also the bytes conversion only works for EQ or NEQ checks.