search

runtimeverification / michelson-semantics

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

Proof by induction of safety properties (storage invariants) in the presence of reentrancy #265

Closed ehildenb closed 3 years ago

ehildenb commented 3 years ago

Starting point: https://github.com/runtimeverification/michelson-semantics/blob/master/tests/proofs/dexter/dexter-properties.md#storage-invariant

The proofs will be in the context that (i) arbitrary reentrancy is possible following each function call, (ii) arbitrary order for function calls.

Assumptions are also present for this, which we will document.

daejunpark commented 3 years ago

Done by https://github.com/runtimeverification/michelson-semantics/pull/256