local_adequacy.v 9.32 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1 2 3
From Coq Require Import Program.Equality Lia.
From Paco Require Import paco.

4
From stbor.lang Require Import steps_wf steps_inversion.
Hai Dang's avatar
Hai Dang committed
5
From stbor.sim Require Import sflib behavior global local.
Hai Dang's avatar
Hai Dang committed
6
From stbor.sim Require Import invariant refl_step.
Hai Dang's avatar
Hai Dang committed
7 8

Set Default Proof Using "Type".
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
9

Hai Dang's avatar
Hai Dang committed
10
Lemma fill_step_inv_2
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
11 12
      fn K e1 σ1 e2 σ2
      (STEP: (fill (Λ:=bor_ectxi_lang fn) K e1, σ1) ~{fn}~> (e2, σ2)):
Hai Dang's avatar
Hai Dang committed
13 14
  ( e2', e2 = fill K e2'  (e1, σ1) ~{fn}~> (e2', σ2)) 
  ( v, to_result e1 = Some v).
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
15
Proof.
Hai Dang's avatar
Hai Dang committed
16 17
  destruct (to_result e1) eqn:Eq1; [right; by eexists|left; by apply fill_tstep_inv].
Qed.
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
18

Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
19 20 21 22
Section local.
Variable (fns fnt: fn_env).

Record frame: Type := mk_frame {
Hai Dang's avatar
Hai Dang committed
23
  rc: resUR;
Jeehoon Kang's avatar
Jeehoon Kang committed
24
  callids: list nat;
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
25 26 27 28 29
  K_src: list (ectxi_language.ectx_item (bor_ectxi_lang fns));
  K_tgt: list (ectxi_language.ectx_item (bor_ectxi_lang fnt));
}.

Inductive sim_local_frames:
Hai Dang's avatar
Hai Dang committed
30
  forall (r_f: resUR)
Jeehoon Kang's avatar
Jeehoon Kang committed
31
    (callids: list nat)
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
32 33 34 35 36 37
    (K_src: list (ectxi_language.ectx_item (bor_ectxi_lang fns)))
    (K_tgt: list (ectxi_language.ectx_item (bor_ectxi_lang fnt)))
    (frames:list frame),
    Prop :=
| sim_local_frames_nil
    r_f
Jeehoon Kang's avatar
Jeehoon Kang committed
38
  : sim_local_frames r_f nil nil nil nil
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
39
| sim_local_frames_cons
Jeehoon Kang's avatar
Jeehoon Kang committed
40
    r_f cids K_f_src K_f_tgt
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
41
    frame frames
Jeehoon Kang's avatar
Jeehoon Kang committed
42
    (FRAMES: sim_local_frames r_f cids K_f_src K_f_tgt frames)
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
43
    (CONTINUATION:
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
44 45
        r' v_src v_tgt σ_src' σ_tgt'
         (* For any new resource r' that are compatible with
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
46 47 48
             our local resource r and have world satisfaction *)
         (WSAT' : wsat (r_f  (frame.(rc)  r')) σ_src' σ_tgt')
         (* and the returned values are related w.r.t. (r  r'  r_f) *)
Jeehoon Kang's avatar
Jeehoon Kang committed
49 50
         (VRET  : vrel_expr r' (Val v_src) (Val v_tgt))
         (CIDS: σ_tgt'.(scs) = frame.(callids)),
Hai Dang's avatar
Hai Dang committed
51
          idx', sim_local_body wsat vrel_expr fns fnt
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
52 53
                                (frame.(rc)  r') idx'
                                (fill frame.(K_src) (Val v_src)) σ_src'
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
54
                                (fill frame.(K_tgt) (Val v_tgt)) σ_tgt'
Hai Dang's avatar
Hai Dang committed
55
                                (λ r _ vs σs vt σt,
Jeehoon Kang's avatar
Jeehoon Kang committed
56
                                  ( c, σt.(scs) = c :: cids) 
Hai Dang's avatar
Hai Dang committed
57 58
                                  end_call_sat r σs σt 
                                  vrel_expr r (of_result vs) (of_result vt)))
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
59 60
  : sim_local_frames
      (r_f  frame.(rc))
Jeehoon Kang's avatar
Jeehoon Kang committed
61
      frame.(callids)
62 63
      (EndCallCtx :: frame.(K_src) ++ K_f_src)
      (EndCallCtx :: frame.(K_tgt) ++ K_f_tgt)
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
64 65 66 67 68 69
      (frame :: frames)
.

Inductive sim_local_conf:
  forall (idx:nat) (e_src:expr) (σ_src:state) (e_tgt:expr) (σ_tgt:state), Prop :=
| sim_local_conf_intro
Jeehoon Kang's avatar
Jeehoon Kang committed
70
    r_f cids K_src K_tgt frames
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
71 72
    rc idx e_src σ_src e_tgt σ_tgt
    Ke_src Ke_tgt
Jeehoon Kang's avatar
Jeehoon Kang committed
73
    (FRAMES: sim_local_frames r_f cids K_src K_tgt frames)
Hai Dang's avatar
Hai Dang committed
74 75
    (LOCAL: sim_local_body wsat vrel_expr fns fnt rc idx e_src σ_src e_tgt σ_tgt
                           (λ r _ vs σs vt σt,
Jeehoon Kang's avatar
Jeehoon Kang committed
76
                              ( c, σt.(scs) = c :: cids) 
Hai Dang's avatar
Hai Dang committed
77 78
                              end_call_sat r σs σt 
                              vrel_expr r (of_result vs) (of_result vt)))
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
79 80
    (KE_SRC: Ke_src = fill K_src e_src)
    (KE_TGT: Ke_tgt = fill K_tgt e_tgt)
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
81
    (WSAT: wsat (r_f  rc) σ_src σ_tgt)
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
82 83 84
  : sim_local_conf idx Ke_src σ_src Ke_tgt σ_tgt.

Lemma sim_local_conf_sim
Hai Dang's avatar
Hai Dang committed
85
      (FUNS: sim_local_funs wsat vrel_expr fns fnt end_call_sat)
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
86 87 88 89 90 91
      (idx:nat) (e_src:expr) (σ_src:state) (e_tgt:expr) (σ_tgt:state)
      (SIM: sim_local_conf idx e_src σ_src e_tgt σ_tgt)
  : sim fns fnt idx (e_src, σ_src) (e_tgt, σ_tgt)
.
Proof.
  revert idx e_src σ_src e_tgt σ_tgt SIM. pcofix CIH. i.
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
92
  pfold. ii. inv SIM. punfold LOCAL. exploit LOCAL; eauto.
Hai Dang's avatar
Hai Dang committed
93
  { eapply never_stuck_fill_inv; eauto. }
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
94
  clear LOCAL. intro LOCAL. inv LOCAL. econs.
Hai Dang's avatar
Hai Dang committed
95 96 97 98
  - ii. simpl. des; last (right; by eapply tstep_reducible_fill).
    destruct sim_local_body_stuck as [vt Eqvt].
    rewrite -(of_to_result _ _ Eqvt).
    destruct (sim_local_body_terminal _ Eqvt)
Jeehoon Kang's avatar
Jeehoon Kang committed
99
      as (vs' & σs' & r' & idx' & SS' & WSAT' & CALLIDS & ESAT' & VREL).
Hai Dang's avatar
Hai Dang committed
100 101 102 103 104
    have STEPK: (fill (Λ:=bor_ectxi_lang fns) K_src0 e_src0, σ_src)
              ~{fns}~>* (fill (Λ:=bor_ectxi_lang fns) K_src0 vs', σs').
    { apply fill_tstep_rtc. destruct SS' as [|[? Eq]].
      by apply tc_rtc. clear -Eq. simplify_eq. constructor. }
    have NT3:= never_stuck_tstep_rtc _ _ _ _ _ STEPK NEVER_STUCK.
Hai Dang's avatar
Hai Dang committed
105
    clear -STEPK NT3 FRAMES WSAT' VREL.
Hai Dang's avatar
Hai Dang committed
106 107 108 109 110 111 112 113 114
    inversion FRAMES. { left. rewrite to_of_result. by eexists. }
    right. subst K_src0 K_tgt0.
    move : NT3. simpl. intros NT3.
    destruct (NT3 (fill (K_src frame0 ++ K_f_src) (EndCall vs')) σs')
      as [[? TERM]|RED]; [constructor|..].
    { by rewrite fill_not_result in TERM. }
    apply tstep_reducible_fill_inv in RED; [|done].
    apply tstep_reducible_fill.
    destruct RED as [e2 [σ2 Eq2]].
Hai Dang's avatar
Hai Dang committed
115 116
    apply vrel_expr_result in VREL as (v1 & v2 & ? & ? & ?). subst vs' vt.
    move : Eq2. eapply end_call_tstep_src_tgt; eauto.
117 118 119 120 121
  - guardH sim_local_body_stuck.
    s. i. apply fill_result in H. unfold terminal in H. des. subst. inv FRAMES. ss.
    exploit sim_local_body_terminal; eauto. i. des.
    esplits; eauto; ss.
    + rewrite to_of_result. esplits; eauto.
Hai Dang's avatar
Hai Dang committed
122
    + ii. clarify. eapply vrel_expr_to_result; eauto.
123 124 125
  - guardH sim_local_body_stuck.
    i. destruct eσ2_tgt as [e2_tgt σ2_tgt].

Hai Dang's avatar
Hai Dang committed
126
    exploit fill_step_inv_2; eauto. i. des; cycle 1.
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
127
    { (* return *)
128 129 130
      exploit sim_local_body_terminal; eauto. i. des.

      inv FRAMES; ss.
Hai Dang's avatar
Hai Dang committed
131
      { exfalso. apply result_tstep_stuck in H. naive_solver. }
Hai Dang's avatar
Hai Dang committed
132

Hai Dang's avatar
Hai Dang committed
133
      (* Simulatin EndCall *)
Hai Dang's avatar
Hai Dang committed
134
      rename σ_tgt into σt. rename σs' into σs.
Jeehoon Kang's avatar
Jeehoon Kang committed
135
      destruct (vrel_expr_result _ _ _ x4) as (vs1 & vt1 & Eqvs1 & Eqv1 & VREL1).
Hai Dang's avatar
Hai Dang committed
136 137 138
      simplify_eq. have VR: vrel r' vs1 vt1 by apply vrel_expr_vrel.

      set Φ : resUR  nat  result  state  result  state  Prop :=
Hai Dang's avatar
Hai Dang committed
139
        λ r2 _ vs2 σs2 vt2 σt2, vrel_expr r2 vs2 vt2 
Hai Dang's avatar
Hai Dang committed
140 141 142 143
           c1 c2 cids1 cids2, σs.(scs) = c1 :: cids1 
            σt.(scs) = c2 :: cids2 
            σs2 = mkState σs.(shp) σs.(sst) cids1 σs.(snp) σs.(snc) 
            σt2 = mkState σt.(shp) σt.(sst) cids2 σt.(snp) σt.(snc) 
Hai Dang's avatar
Hai Dang committed
144 145 146 147 148
            r2 = ((r'.(rtm),
                    match (r'.(rcm) !! c2) with
                    | Some (Cinl (Excl T)) => <[c2 := to_callStateR csPub]> r'.(rcm)
                    | _ => r'.(rcm)
                    end), r'.(rlm)).
Hai Dang's avatar
Hai Dang committed
149
      have SIMEND : r' {idx',fns,fnt} (EndCall vs1, σs)  (EndCall vt1, σt) : Φ.
Hai Dang's avatar
Hai Dang committed
150 151 152
      { apply sim_body_end_call; auto.
        clear. intros. rewrite /Φ. naive_solver. }

Hai Dang's avatar
Hai Dang committed
153 154 155 156
      have NONE : to_result (EndCall e_tgt0) = None. by done.
      destruct (fill_tstep_inv _ _ _ _ _ _ NONE H) as [et2 [? STEPT2]].
      subst e2_tgt.

Hai Dang's avatar
Hai Dang committed
157 158 159
      have STEPK: (fill (Λ:= bor_ectxi_lang fns)
                        (EndCallCtx :: K_src frame0 ++ K_f_src) e_src0, σ_src)
            ~{fns}~>* (fill (Λ:= bor_ectxi_lang fns)
Hai Dang's avatar
Hai Dang committed
160
                        (EndCallCtx :: K_src frame0 ++ K_f_src) vs1, σs).
Hai Dang's avatar
Hai Dang committed
161 162 163
      { apply fill_tstep_rtc. destruct x as [|[? Eq]].
        by apply tc_rtc. clear -Eq. simplify_eq. constructor. }
      have NT3 := never_stuck_tstep_rtc _ _ _ _ _ STEPK NEVER_STUCK.
Hai Dang's avatar
Hai Dang committed
164 165 166 167 168
      rewrite /= in NT3.
      have NT4 := never_stuck_fill_inv _ _ _ _ NT3.
      rewrite -(of_to_result _ _ x0) in STEPT2.
      destruct (sim_body_end_call_elim' _ _ _ _ _ _ _ _ _ SIMEND _ _ _ x1 NT4 STEPT2)
        as (r2 & idx2 & σs2 & STEPS & ? & HΦ2 & WSAT2). subst et2.
Hai Dang's avatar
Hai Dang committed
169

Jeehoon Kang's avatar
Jeehoon Kang committed
170
      exploit (CONTINUATION r2).
Hai Dang's avatar
Hai Dang committed
171
      { rewrite cmra_assoc; eauto. }
Hai Dang's avatar
Hai Dang committed
172
      { apply HΦ2. }
Jeehoon Kang's avatar
Jeehoon Kang committed
173 174 175
      { exploit tstep_end_call_inv; try exact STEPT2; eauto. i. des. subst. ss.
        rewrite x2 in x7. inv x7. ss.
      }
Hai Dang's avatar
Hai Dang committed
176 177 178 179 180 181 182
      intros [idx3 SIMFR]. rename σ2_tgt into σt2.
      do 2 eexists. split.
      - left. apply fill_tstep_tc. eapply tc_rtc_l; [|apply STEPS].
        apply (fill_tstep_rtc _ [EndCallCtx]).
        clear -x. destruct x as [|[]]. by apply tc_rtc. simplify_eq; constructor.

      - right. apply CIH. econs; eauto.
183 184
        + rewrite fill_app. eauto.
        + rewrite fill_app. eauto.
Hai Dang's avatar
Hai Dang committed
185
        + rewrite <-cmra_assoc in WSAT2; eauto.
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
186
    }
187

Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
188 189 190 191
    subst. clear H. inv sim_local_body_step.
    + (* step *)
      exploit STEP; eauto. intros (es' & σs' & r' & idx' & STEP' & WSAT' & SIM').
      pclearbot. esplits; eauto.
192
      * instantiate (1 := (fill K_src0 es', σs')). revert sim_local_body_stuck.
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
193
        des; [left|right]; esplits; eauto.
Hai Dang's avatar
Hai Dang committed
194
        { apply fill_tstep_tc. ss. }
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
195 196 197
        { inv STEP'0. ss. }
      * right. apply CIH. econs; eauto.
    + (* call *)
Hai Dang's avatar
Hai Dang committed
198
      exploit fill_step_inv_2; eauto. i. des; ss.
199
      exploit tstep_call_inv; try exact x2; eauto. i. des. subst.
Hai Dang's avatar
Hai Dang committed
200 201 202 203
      destruct (FUNS _ _ x3) as ([xls ebs HCss] & Eqfs & Eql & SIMf).
      destruct (subst_l_is_Some xls el_src ebs) as [ess Eqss].
      { by rewrite (Forall2_length _ _ _ VREL) -(subst_l_is_Some_length _ _ _ _ x4). }
      specialize (SIMf _ _ _ _ _ σ1_src σ_tgt VSRC VTGT VREL Eqss x4) as [idx2 SIMf].
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
204 205
      esplits.
      * left. eapply tc_rtc_l.
Hai Dang's avatar
Hai Dang committed
206
        { apply fill_tstep_rtc. eauto. }
Hai Dang's avatar
Hai Dang committed
207 208
        { econs. rewrite -fill_app. eapply (head_step_fill_tstep).
          econs; econs; eauto. }
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
209
      * right. apply CIH. econs.
Jeehoon Kang's avatar
Jeehoon Kang committed
210
        { econs 2; eauto. i. instantiate (1 := mk_frame _ _ _ _). ss.
211
          destruct (CONT _ _ _ σ_src' σ_tgt' VRET).
Jeehoon Kang's avatar
Jeehoon Kang committed
212
          { rewrite CIDS. eauto. }
Hai Dang's avatar
Hai Dang committed
213
          pclearbot. esplits; eauto.
Jeehoon Kang's avatar
Jeehoon Kang committed
214
        }
Hai Dang's avatar
Hai Dang committed
215
        { eapply sim_local_body_post_mono; [|apply SIMf]. simpl. naive_solver. }
Hai Dang's avatar
Hai Dang committed
216
        { done. }
Hai Dang's avatar
Hai Dang committed
217
        { s. rewrite -fill_app. eauto. }
Hai Dang's avatar
Hai Dang committed
218 219
        { ss. rewrite -cmra_assoc; eauto. }
Qed.
Jeehoon Kang's avatar
WIP  
Jeehoon Kang committed
220 221

End local.