proposition: Lemma instrument_satisfies_hoare `{MayProvide ix i} `(c : contract i Ω) `(p : impure ix a) `(comp : compliant_semantics c ω sem) : pre (to_hoare c p) ω -> post (to_hoare c p) ω (fst $ evalState (runStateT (to_instrument c p) ω) sem) (snd $ evalState (runStateT (to_instrument c p) ω) sem).
proof: Proof. revert comp. revert ω. revert sem. induction p; intros sem ω comp. + cbn. intros _. split; reflexivity. + intros pre. cbn -[interface_to_hoare] in pre. destruct pre as [He Hf]. cbn in He. inversion comp; subst. pose proof He as He'. apply o_callee in He. cbn. exists (eval_effect sem e). exists (gen_witness_update c ω e (eval_effect sem e)). split; [split |]. ++ apply He. ++ reflexivity. ++ unfold evalState. cbn. repeat rewrite run_effect_equation. apply H0. +++ apply next. apply He'. +++ apply Hf. cbn. now split. Qed.
imports: ExtLib(StateMonad) FreeSpec.Core(Contract HoareFacts SemanticsFacts)