From dc0891ea6a03abf6216a87d5d4084b1f4641c8db Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 8 Jul 2019 15:29:54 +0200 Subject: [PATCH] better framing --- theories/sim/body.v | 70 +++++++++++++++++++++++++++++++++++++------ theories/sim/refl.v | 9 +++--- theories/sim/simple.v | 10 ++++++- 3 files changed, 75 insertions(+), 14 deletions(-) diff --git a/theories/sim/body.v b/theories/sim/body.v index f955efb..ca2ac1f 100644 --- a/theories/sim/body.v +++ b/theories/sim/body.v @@ -172,11 +172,11 @@ Proof. Qed. Global Instance: Params (@sim_local_body) 5. -Lemma sim_body_frame' fs ft n (rf r: resUR) es σs et σt Φ : +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': 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'). + (λ r' n' es' σs' et' σt', ∃ r0, r' = r0 ⋅ rf ∧ Φ r0 n' es' σs' et' σt'). Proof. revert n rf r es σs et σt Φ. pcofix CIH. intros n rf r0 es σs et σt Φ SIM r' EQ'. @@ -185,8 +185,9 @@ Proof. rewrite ->EQ', ->(cmra_assoc r_f rf r0) in WSAT. specialize (SIM NT _ WSAT) as [SU TE ST]. split; [done|..]. { intros. destruct (TE _ TERM) as (vs' & σs' & r2 & STEP' & WSAT' & POST). - exists vs', σs', (rf ⋅ r2). - split; last split; [done|by rewrite cmra_assoc|by exists r2]. } + exists vs', σs', (r2 ⋅ rf). + split; last split; [done|by rewrite [r2 ⋅ rf]comm cmra_assoc|by exists r2]. + } inversion ST. - constructor 1. intros. specialize (STEP _ _ STEPT) as (es' & σs' & r2 & idx' & STEPS' & WSAT' & SIM'). @@ -201,11 +202,57 @@ Proof. exists idx'. pclearbot. right. eapply CIH; eauto. by rewrite cmra_assoc. Qed. -Lemma sim_body_frame fs ft n (rf r: resUR) es σs et σt Φ : +(* 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 → - rf ⋅ 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'). -Proof. intros. eapply sim_body_frame'; eauto. Qed. +Proof. + revert n rf r es σs et σt Φ. pcofix CIH. + intros n rf r0 es σs et σt Φ SIM r' EQ'. + pfold. punfold SIM. + intros NT r_f WSAT. + rewrite ->EQ', ->(cmra_assoc r_f rf r0) in WSAT. + specialize (SIM NT _ WSAT) as [SU TE ST]. split; [done|..]. + { intros. destruct (TE _ TERM) as (vs' & σs' & r2 & STEP' & WSAT' & POST). + exists vs', σs', (rf ⋅ r2). + split; last split; [done|by rewrite cmra_assoc|by exists r2]. + } + inversion ST. + - constructor 1. intros. + specialize (STEP _ _ STEPT) as (es' & σs' & r2 & idx' & STEPS' & WSAT' & SIM'). + exists es', σs', (rf ⋅ r2), idx'. + split; last split; [done|by rewrite cmra_assoc|]. + pclearbot. right. by eapply CIH. + - econstructor 2; eauto. + { instantiate (1:= rf ⋅ rc). by rewrite -cmra_assoc (cmra_assoc r_f). } + intros. + specialize (CONT _ _ _ σs' σt' VRET) as [idx' SIM']; [|done|]. + { move : WSAT1. by rewrite 3!cmra_assoc. } + exists idx'. pclearbot. right. eapply CIH; eauto. by rewrite cmra_assoc. +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 ⋅ 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]. + 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') → + rf ⋅ r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ. +Proof. + intros HH. 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} @@ -214,8 +261,7 @@ Lemma sim_body_frame_core fs ft n (r: resUR) es σs et σt Φ : r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ. Proof. intros HH. rewrite -(cmra_core_l r). - eapply sim_local_body_post_mono, sim_body_frame, HH. - intros r' n' rs' σs' rt' σt' [r'' [-> HΦ]]. done. + eapply sim_body_frame_l. done. Qed. Lemma sim_body_val_elim fs ft r n vs σs vt σt Φ : @@ -234,3 +280,9 @@ Proof. - by apply result_tstep_stuck in STEP2. } subst σs' vs'. done. Qed. + +Lemma sim_body_viewshift r2 r1 fs ft n es σs et σt Φ : + r1 |==> r2 → + r2 ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ → + r1 ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ. +Proof. by eapply viewshift_sim_local_body. Qed. diff --git a/theories/sim/refl.v b/theories/sim/refl.v index 1586f9c..19d1120 100644 --- a/theories/sim/refl.v +++ b/theories/sim/refl.v @@ -1,5 +1,5 @@ From stbor.lang Require Import lang subst_map. -From stbor.sim Require Import refl_step simple tactics. +From stbor.sim Require Import refl_step simple tactics viewshift. Set Default Proof Using "Type". @@ -190,12 +190,13 @@ 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. - (* FIXME: viewshift to public call ID, use framing or something to get it to fun_post. *) + eapply (sim_body_viewshift (r ⋅ res_callState _ csPub)). + { eapply vs_call_empty_public. } 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' (-> & ? & ? & Hrrel). + { intros r' n' rs css' rt cst' (-> & Hcss & Hcst & Hrrel). simplify_eq. split. - - eexists. split. subst cst css. rewrite <-Hstacks. congruence. + - eexists. split; first by rewrite Hcst. admit. (* end_call_sat *) - done. } diff --git a/theories/sim/simple.v b/theories/sim/simple.v index 66d6b05..81d1b2e 100644 --- a/theories/sim/simple.v +++ b/theories/sim/simple.v @@ -93,8 +93,16 @@ Proof. eapply sim_local_body_post_mono, Hold; done. Qed. +Lemma sim_simple_viewshift r2 r1 fs ft n es css et cst Φ : + r1 |==> r2 → + r2 ⊨ˢ{n,fs,ft} (es, css) ≥ (et, cst) : Φ → + r1 ⊨ˢ{n,fs,ft} (es, css) ≥ (et, cst) : Φ. +Proof. + intros Hvs Hold σs σt <-<-. eapply viewshift_sim_local_body, Hold; done. +Qed. + (** Simple proof for a function taking one argument. *) -(* TODO: make the two call stacks the same. *) +(* TODO: make the two call stacks the same? *) Lemma sim_fun_simple1 n (esf etf: function) : length (esf.(fun_args)) = 1%nat → length (etf.(fun_args)) = 1%nat → -- GitLab