fact: Definition store_specs (s : Type) : contract (STORE s) s := {| witness_update := store_update s ; caller_obligation := no_caller_obligation ; callee_obligation := o_callee_store s |}.
imports: Coq(Setoid Morphisms) ExtLib(StateMonad MonadState MonadTrans) FreeSpec.Core(Interface Impure Semantics Component)