Library FreeSpec.Core.InstrumentFacts
From ExtLib Require Import StateMonad.
From FreeSpec.Core Require Import Contract HoareFacts SemanticsFacts.
From FreeSpec.Core Require Export Instrument.
Lemma instrument_to_state_eval_morphism `{MayProvide ix i}
`(c : contract i Ω) `(p : impure ix a) (ω : Ω)
: ∀ (sem : semantics ix),
evalState (to_state p) sem
= fst (evalState (runStateT (to_instrument c p) ω) sem).
Proof.
unfold evalState.
revert ω.
induction p.
+ reflexivity.
+ intros ω sem.
cbn -[gen_witness_update].
destruct run_effect; cbn.
now rewrite H0 with (ω := gen_witness_update c ω e β0).
Qed.
Lemma instrument_to_state_exec_morphism `{MayProvide ix i}
`(c : contract i Ω) `(p : impure ix a) (ω : Ω)
: ∀ (sem : semantics ix),
execState (to_state p) sem
= execState (runStateT (to_instrument c p) ω) sem.
Proof.
unfold execState.
revert ω.
induction p.
+ reflexivity.
+ intros ω sem.
cbn -[gen_witness_update].
destruct run_effect; cbn.
now rewrite H0 with (ω := gen_witness_update c ω e β0).
Qed.
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.
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.
∃ (eval_effect sem e).
∃ (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.
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.
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.