proposition: Lemma instrument_preserves_compliance `{MayProvide ix i} `(c : contract i Ω) `(p : impure ix a) `(comp : compliant_semantics c ω sem) : pre (to_hoare c p) ω -> compliant_semantics c (snd $ evalState (runStateT (to_instrument c p) ω) sem) (execState (runStateT (to_instrument c p) ω) sem).
proof: Proof. revert comp. revert ω. revert sem. induction p; intros sem ω comp pre. + auto. + cbn in pre. destruct pre as [He Hn]. specialize Hn with (eval_effect sem e) (gen_witness_update (H := H) c ω e (eval_effect sem e)). inversion comp; subst. assert (Hn' : pre (to_hoare c (f (eval_effect sem e))) (gen_witness_update c ω e (eval_effect sem e))). { apply Hn. split; [| reflexivity]. now apply o_callee. } eapply H0 in Hn'; [| now apply next ]. replace (snd (evalState (runStateT (to_instrument c (request_then e f)) ω) sem)) with (snd (evalState (runStateT (to_instrument c (f (eval_effect sem e))) (gen_witness_update c ω e (eval_effect sem e))) (exec_effect sem e))). replace (execState (runStateT (to_instrument c (request_then e f)) ω) sem) with (execState (runStateT (to_instrument c (f (eval_effect sem e))) (gen_witness_update c ω e (eval_effect sem e))) (exec_effect sem e)). ++ apply Hn'. ++ cbn. unfold execState at 2. cbn. now rewrite run_effect_equation. ++ cbn. unfold evalState at 2. cbn. now rewrite run_effect_equation. Qed.
imports: ExtLib(StateMonad) FreeSpec.Core(Contract HoareFacts SemanticsFacts)