search

runtimeverification / michelson-semantics

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

Proof composability? #221

Open ehildenb opened 3 years ago

ehildenb commented 3 years ago

Currently we lack composability because of the setup/tear-down that happens around each proof (by using abstract <storage> state and push/popping it).

Maybe we can fix this by having the <storage> configuration be a macro which expands out to directly the michelson state.

Maybe something like this?

configuration <storage> .... <code> CODE </code> </storage>

rule <storage> ... </storage> => <michelsonTop> ... </michelsonTop> [macro]

Then write claims as:

claim <storage> .... <code> DEXTER_CODE </code> </storage>
 => <storage> .... <code> .Code </code> </storage>