search

runtimeverification / michelson-semantics

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

Add `<operations>` cell for recording expected callbacks in specs #207

Closed ehildenb closed 3 years ago

ehildenb commented 3 years ago

Specs over this cell will always go like this:

<operations> .List => ListItem(op1) ListItem(op2) ... </operations>

The operation #deserializeState should add this list onto the end. If we were really complete, we would start with symbolic OPS on LHS, but we only append to this cell, so we just start with .List.

ehildenb commented 3 years ago

Actually, we should start with symbolic callback list then (not .List), because otherwise the proofs can't be chained together.