Commit fed183ec authored by Ralf Jung's avatar Ralf Jung

sim_mod_fun_refl proven!

parent d1551a65
......@@ -3,10 +3,13 @@ From stbor.sim Require Export instance.
Set Default Proof Using "Type".
Section body.
Implicit Types Φ: resUR nat result state result state Prop.
Lemma sim_body_valid fs ft r n es σs et σt Φ :
(valid r
r {n,fs,ft} (es, σs) (et, σt) :
(λ r' n' es' σs' et' σt', valid r' Φ r' n' es' σs' et' σt' : Prop))
(λ r' n' es' σs' et' σt', valid r' Φ r' n' es' σs' et' σt'))
r {n,fs,ft} (es, σs) (et, σt) : Φ.
Proof.
revert r n es σs et σt Φ. pcofix CIH.
......@@ -31,6 +34,16 @@ Proof.
exists idx'. pclearbot. right. by eapply CIH; eauto.
Qed.
Lemma sim_body_post_mono_valid fs ft r n es σs et σt Φ Φ' :
( r, r Φ r <5= Φ' r)
r {n,fs,ft} (es, σs) (et, σt) : Φ
r {n,fs,ft} (es, σs) (et, σt) : Φ'.
Proof.
intros HΦ HH. eapply sim_body_valid=>Hval.
eapply sim_local_body_post_mono, HH.
intros. eapply HΦ; done.
Qed.
Lemma sim_body_bind fs ft r n
(Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs)))
(Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) es et σs σt Φ :
......@@ -173,7 +186,7 @@ Qed.
Global Instance: Params (@sim_local_body) 5.
Lemma sim_body_frame_r' fs ft n (rf r: resUR) es σs et σt Φ :
r {n,fs,ft} (es, σs) (et, σt) : Φ : Prop
r {n,fs,ft} (es, σs) (et, σt) : Φ
(r': resUR), r' rf r
r' {n,fs,ft} (es, σs) (et, σt) :
(λ r' n' es' σs' et' σt', r0, r' = r0 rf Φ r0 n' es' σs' et' σt').
......@@ -205,7 +218,7 @@ Qed.
(* So ugly. We just copy the above proof to get the version with the frame added
on the other side. There *probably* is a better way... *)
Lemma sim_body_frame_l' fs ft n (rf r: resUR) es σs et σt Φ :
r {n,fs,ft} (es, σs) (et, σt) : Φ : Prop
r {n,fs,ft} (es, σs) (et, σt) : Φ
(r': resUR), r' rf r
r' {n,fs,ft} (es, σs) (et, σt) :
(λ r' n' es' σs' et' σt', r0, r' = rf r0 Φ r0 n' es' σs' et' σt').
......@@ -237,27 +250,29 @@ Qed.
Lemma sim_body_frame_r fs ft n (rf r: resUR) es σs et σt Φ :
r {n,fs,ft}
(es, σs) (et, σt)
: (λ r' n' es' σs' et' σt', Φ (r' rf) n' es' σs' et' σt')
: (λ r' n' es' σs' et' σt', (r' rf) Φ (r' rf) n' es' σs' et' σt')
r rf {n,fs,ft} (es, σs) (et, σt) : Φ.
Proof.
intros HH. eapply sim_local_body_post_mono, sim_body_frame_r'; [|done|by rewrite comm].
intros HH. eapply sim_body_valid=>_.
eapply sim_local_body_post_mono, sim_body_frame_r'; [|done|by rewrite comm].
simpl. intros r' n' es' σs' et' σt' (rf' & -> & ?). done.
Qed.
Lemma sim_body_frame_l fs ft n (rf r: resUR) es σs et σt Φ :
r {n,fs,ft}
(es, σs) (et, σt)
: (λ r' n' es' σs' et' σt', Φ (rf r') n' es' σs' et' σt')
: (λ r' n' es' σs' et' σt', (rf r') Φ (rf r') n' es' σs' et' σt')
rf r {n,fs,ft} (es, σs) (et, σt) : Φ.
Proof.
intros HH. eapply sim_local_body_post_mono, sim_body_frame_l'; [|done..].
intros HH. eapply sim_body_valid=>_.
eapply sim_local_body_post_mono, sim_body_frame_l'; [|done..].
simpl. intros r' n' es' σs' et' σt' (rf' & -> & ?). done.
Qed.
Lemma sim_body_frame_core fs ft n (r: resUR) es σs et σt Φ :
r {n,fs,ft}
(es, σs) (et, σt)
: (λ r' n' es' σs' et' σt', Φ (core r r') n' es' σs' et' σt')
: (λ r' n' es' σs' et' σt', (core r r') Φ (core r r') n' es' σs' et' σt')
r {n,fs,ft} (es, σs) (et, σt) : Φ.
Proof.
intros HH. rewrite -(cmra_core_l r).
......@@ -286,3 +301,5 @@ Lemma sim_body_viewshift r2 r1 fs ft n es σs et σt Φ :
r2 {n,fs,ft} (es, σs) (et, σt) : Φ
r1 {n,fs,ft} (es, σs) (et, σt) : Φ.
Proof. by eapply viewshift_sim_local_body. Qed.
End body.
......@@ -106,6 +106,18 @@ Definition vrel (r: resUR) (v1 v2: value) := Forall2 (arel r) v1 v2.
Definition end_call_sat (r: resUR) (c: call_id) : Prop :=
r.(rcm) !! c Some (to_callStateR csPub).
Lemma res_end_call_sat r c :
r res_callState c csPub r end_call_sat r c.
Proof.
intros Hval [r' EQ]. rewrite /end_call_sat EQ.
destruct r' as [[tmap' cmap'] lmap'].
rewrite /res_callState. rewrite !pair_op /= /rcm /=.
apply cmap_lookup_op_l_equiv_pub; last by rewrite lookup_insert.
destruct r as [[tmap cmap] lmap].
destruct EQ as [[EQt EQc] EQl]. simplify_eq/=.
apply Hval.
Qed.
Definition init_res : resUR := ((ε, {[O := to_callStateR csPub]}), ε).
Lemma wsat_init_state : wsat init_res init_state init_state.
Proof.
......
......@@ -117,9 +117,9 @@ Proof.
Qed.
Lemma expr_wf_soundness r e :
r expr_wf e sem_wf r e e.
expr_wf e sem_wf r e e.
Proof.
revert r. induction e using expr_ind; simpl; intros r Hvalid.
revert r. induction e using expr_ind; simpl; intros r.
- (* Value *)
move=>Hwf _ _ /=.
apply sim_simple_val.
......@@ -166,12 +166,11 @@ Proof.
move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
eapply sim_simple_frame_core.
eapply sim_simple_post_mono, IHe1; [|by auto..].
intros r' n' rs css' rt cst' (-> & -> & -> & Hrel). simpl.
intros r' n' rs css' rt cst' (-> & -> & -> & Hrel) Hval. simpl.
eapply sim_simple_let; [destruct rs, rt; by eauto..|].
rewrite !subst'_subst_map.
change rs with (fst (rs, rt)). change rt with (snd (rs, rt)) at 2.
rewrite !binder_insert_map.
eapply sim_simple_valid_pre=>Hval.
eapply IHe2; [by auto..|].
destruct b; first exact: srel_frame_core. simpl.
apply map_Forall_insert_2.
......@@ -190,21 +189,21 @@ Proof.
intros vs vt σs σt Hrel Hsubst1 Hsubst2. exists sem_steps.
apply sim_body_init_call=>/=.
set css := snc σs :: scs σs. set cst := snc σt :: scs σt. move=>Hstacks.
eapply (sim_body_viewshift (r res_callState _ csPub)).
{ eapply vs_call_empty_public. }
eapply sim_body_viewshift.
{ eapply viewshift_frame_l. eapply vs_call_empty_public. }
eapply sim_body_frame_r.
eapply sim_local_body_post_mono with
(Φ:=(λ r n vs' σs' vt' σt', sem_post css cst r n vs' σs'.(scs) vt' σt'.(scs))).
{ intros r' n' rs css' rt cst' (-> & Hcss & Hcst & Hrrel). simplify_eq.
{ intros r' n' rs css' rt cst' (-> & Hcss & Hcst & Hrrel) Hval. simplify_eq.
split.
- eexists. split; first by rewrite Hcst.
admit. (* end_call_sat *)
- done.
apply: res_end_call_sat; first done. exact: cmra_included_r.
- eapply rrel_mono; [done| |done]. exact: cmra_included_l.
}
destruct (subst_l_map _ _ _ _ _ _ _ (rrel vrel r) Hsubst1 Hsubst2) as (map & -> & -> & Hmap).
{ clear -Hrel. induction Hrel; eauto using Forall2. }
Fail eapply sim_simplify, expr_wf_soundness; [done..|].
admit. (* resource stuff. *)
Admitted.
eapply sim_simplify, expr_wf_soundness; done.
Qed.
Lemma sim_mod_funs_refl prog :
prog_wf prog
......
......@@ -57,7 +57,7 @@ Qed.
Lemma sim_simple_frame_core Φ r n fs ft es css et cst :
r ⊨ˢ{ n , fs , ft }
(es, css) (et, cst)
: (λ r' n' es' css' et' cst', Φ (core r r') n' es' css' et' cst')
: (λ r' n' es' css' et' cst', (core r r') Φ (core r r') n' es' css' et' cst')
r ⊨ˢ{ n , fs , ft } (es, css) (et, cst) : Φ.
Proof.
intros Hold σs σt <-<-. eapply sim_body_frame_core. auto.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment