fact: Definition interface_to_instrument `{MayProvide ix i} `(c : contract i Ω) : ix ~> instrument Ω ix := fun a e => let* x := lift $ interface_to_state _ e in modify (fun ω => gen_witness_update c ω e x);; ret x.
imports: ExtLib(StateMonad MonadTrans) FreeSpec.Core(Interface Semantics Contract)