left_step.v 7.06 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1
2
3
From iris.algebra Require Import local_updates.

From stbor.lang Require Import steps_progress steps_inversion steps_retag.
Hai Dang's avatar
Hai Dang committed
4
From stbor.sim Require Export instance invariant_access body.
Hai Dang's avatar
Hai Dang committed
5
6
7

Set Default Proof Using "Type".

Ralf Jung's avatar
Ralf Jung committed
8
9
10
11
12
13
14
15
Section left.
Implicit Types Φ: resUR  nat  result  state  result  state  Prop.

Lemma sim_body_let_l fs ft r n x et es1 es2 vs1 σs σt Φ :
  IntoResult es1 vs1 
  r {n,fs,ft} (subst' x es1 es2, σs)  (et, σt) : Φ 
  r {n,fs,ft} (let: x := es1 in es2, σs)  (et, σt) : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
  intros TS%into_result_terminal CONT. pfold.
  intros NT r_f WSAT.
  have STEPS1: ((let: x := es1 in es2)%E, σs) ~{fs}~> (subst' x es1 es2, σs).
  { eapply (head_step_fill_tstep _ []). econstructor. by econstructor. }
  have STEPS: ((let: x := es1 in es2)%E, σs) ~{fs}~>* (subst' x es1 es2, σs).
  { by apply rtc_once. }
  have NT2 := never_stuck_tstep_rtc _ _ _ _ _ STEPS NT.
  have CONT2 := CONT. punfold CONT. specialize (CONT NT2 r_f WSAT) as [RE TE ST].
  split; [done|..].
  { intros. specialize (TE _ TERM) as (vs' & σs' & r' & STEPS' & ?).
    exists vs', σs', r'. split; [|done]. by etrans. }
  inversion ST.
  - constructor 1. intros.
    specialize (STEP _ _ STEPT) as (es' & σs' & r' & n' & SS' & ?).
    exists es', σs', r', n'. split ; [|done]. left.
    destruct SS' as [SS'|[]].
    + eapply tc_rtc_l; eauto.
    + simplify_eq. by apply tc_once.
  - econstructor 2; eauto. by etrans.
Qed.
Ralf Jung's avatar
Ralf Jung committed
36
37
38
39
40
41

Lemma sim_body_deref_l fs ft r n et (rt: result) l t T σs σt Φ :
  IntoResult et rt 
  (Φ r n (PlaceR l t T) σs rt σt) 
  r {n,fs,ft} (Deref #[ScPtr l t] T, σs)  (et, σt) : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
42
43
44
45
46
47
48
49
50
51
52
53
  intros TT POST. pfold.
  intros NT r_f WSAT. split.
  { left. by apply into_result_terminal in TT. }
  { intros. exists (PlaceR l t T), σs, r. split; last split; [|done|].
    - apply rtc_once. eapply (head_step_fill_tstep _ []).
      econstructor. econstructor.
    - rewrite <-into_result in TERM. rewrite to_of_result in TERM.
      by simplify_eq. }
  constructor 1. intros.
  apply result_tstep_stuck in STEPT.
  move : STEPT. rewrite <-into_result. by rewrite to_of_result.
Qed.
Ralf Jung's avatar
Ralf Jung committed
54

Hai Dang's avatar
Hai Dang committed
55
56
57
Lemma sim_body_copy_local_unique_l
  fs ft (r r': resUR) (h: heaplet) n (l: loc) t k T (ss st: scalar) et σs σt Φ
  (LU: k = tkLocal  k = tkUnique) :
Ralf Jung's avatar
Ralf Jung committed
58
  tsize T = 1%nat 
Hai Dang's avatar
Hai Dang committed
59
  r  r'  res_tag t k h 
Hai Dang's avatar
Hai Dang committed
60
61
  h !! l = Some (ss,st) 
  (r {n,fs,ft} (#[ss], σs)  (et, σt) : Φ : Prop) 
Hai Dang's avatar
Hai Dang committed
62
  r {n,fs,ft} (Copy (Place l (Tagged t) T), σs)  (et, σt) : Φ.
Ralf Jung's avatar
Ralf Jung committed
63
Proof.
Hai Dang's avatar
Hai Dang committed
64
65
66
67
68
69
70
71
72
73
74
75
76
77
  intros LenT Eqr Eqs CONT. pfold. intros NT. intros.
  have WSAT1 := WSAT. (* backup *)

  (* making a step *)
  edestruct (NT (Copy (Place l (Tagged t) T)) σs) as [[]|[es' [σs' STEPS]]];
    [done..|].
  destruct (tstep_copy_inv _ (PlaceR _ _ _) _ _ _ STEPS)
      as (l'&t'&T'& vs & α' & EqH & ? & Eqvs & Eqα' & ?).
  symmetry in EqH. simplify_eq.

  rewrite LenT read_mem_equation_1 /= in Eqvs.
  destruct (σs.(shp) !! l) as [s'|] eqn:Eqs'; [|done].
  simpl in Eqvs. simplify_eq.

Hai Dang's avatar
Hai Dang committed
78
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
79
80
  (* some lookup properties *)
  have VALIDr := cmra_valid_op_r _ _ VALID. rewrite ->Eqr in VALIDr.
Hai Dang's avatar
Hai Dang committed
81
  have HLtr: r.(rtm) !! t  Some (to_tgkR k, to_agree <$> h).
Hai Dang's avatar
Hai Dang committed
82
  { rewrite Eqr.
Hai Dang's avatar
Hai Dang committed
83
84
85
86
87
88
89
90
91
    destruct LU; subst k.
    - eapply tmap_lookup_op_local_included; [apply VALIDr|apply cmra_included_r|].
      rewrite res_tag_lookup //.
    - eapply tmap_lookup_op_uniq_included; [apply VALIDr|apply cmra_included_r|].
      rewrite res_tag_lookup //. }
  have HLtrf: (r_f  r).(rtm) !! t  Some (to_tgkR k, to_agree <$> h).
  { destruct LU; subst k.
    - apply tmap_lookup_op_r_local_equiv; [apply VALID|done].
    - apply tmap_lookup_op_r_uniq_equiv; [apply VALID|done]. }
Hai Dang's avatar
Hai Dang committed
92
93
94
95
96
97
98
99
100
101
102

  (* Unique: stack unchanged *)
  destruct (for_each_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 _].
  specialize (EQ1 O) as (stk & stk' & Eqstk & Eqstk' & ACC1); [rewrite LenT; lia|].
  rewrite shift_loc_0_nat in Eqstk, Eqstk'.
  move : ACC1. case access1 as [[n1 stk1]|] eqn:ACC1; [|done].
  simpl. intros Eqs1. symmetry in Eqs1. simplify_eq.

  destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&AREL).
  rewrite Eqst in Eqstk. rewrite Eqcs in ACC1.

Hai Dang's avatar
Hai Dang committed
103
  destruct (local_unique_access_head _ _ _ _ _ _ _ _ _ ss st _ _ WFT LU Eqstk ACC1 PINV HLtrf)
Hai Dang's avatar
Hai Dang committed
104
105
106
107
108
109
110
111
112
113
114
115
    as (it & Eqpit & Eqti & HDi & Eqhp); [by rewrite lookup_fmap Eqs |].

  have ?: α' = σt.(sst).
  { move : Eqα'.
    rewrite LenT /= /memory_read /= /= shift_loc_0_nat Eqst Eqstk /= Eqcs ACC1 /=.
    destruct (tag_unique_head_access σt.(scs) stk (Tagged t) it.(protector) AccessRead)
      as [ns Eqss].
    - destruct HDi as [stk' Eq']. exists stk'. rewrite Eq'. f_equal.
      rewrite -Eqpit -Eqti. by destruct it.
    - rewrite ACC1 in Eqss. simplify_eq. rewrite insert_id //. by inversion 1. }
  subst α'. rewrite Eqstk in Eqstk'. symmetry in Eqstk'. simplify_eq.

Hai Dang's avatar
Hai Dang committed
116
  have TOT: tag_on_top σt.(sst) l t Unique.
Hai Dang's avatar
Hai Dang committed
117
118
119
120
121
122
  { destruct HDi as [stk' Eqstk'].
    rewrite /tag_on_top Eqstk Eqstk' /= -Eqpit -Eqti. destruct it. by eexists. }

  rewrite (_: mkState σs.(shp) σt.(sst) σs.(scs) σs.(snp) σs.(snc) = σs) in STEPS;
    last first. { rewrite -Eqst. by destruct σs. }

Hai Dang's avatar
Hai Dang committed
123
124
125
  (* we read s' from σs(l), we know [ss] is in σs(l), now we have to prove that
    s' = ss *)
  assert (s' = ss).
126
  { specialize (PINV _ _ _ HLtrf) as [? PINV].
Hai Dang's avatar
Hai Dang committed
127
    specialize (PINV l ss st). rewrite lookup_fmap Eqs in PINV.
Hai Dang's avatar
Hai Dang committed
128
129
130
131
    specialize (PINV ltac:(done)) as (?&?&?).
    - destruct LU; subst k; [done|].
      exists stk, Unique, it.(protector). split; last split; [done| |done].
      destruct HDi as [? HDi]. rewrite HDi. rewrite -Eqpit -Eqti.
132
133
134
      destruct it; by left.
    - by simplify_eq. }
  subst s'.
Hai Dang's avatar
Hai Dang committed
135

Hai Dang's avatar
Hai Dang committed
136
  have STEPSS: (Copy (Place l (Tagged t) T), σs) ~{fs}~>* (#[ss]%E, σs)
Hai Dang's avatar
Hai Dang committed
137
138
139
140
141
142
143
144
145
146
147
148
149
150
    by apply rtc_once.
  have NT' := never_stuck_tstep_once _ _ _ _ _ STEPS NT.
  (* TODO: the following is the same in most proofs, generalize it *)
  punfold CONT. specialize (CONT NT' _ WSAT1) as [RE TE ST]. split; [done|..].
  - intros. specialize (TE _ TERM) as (vs' & σs' & r1 & STEPS' & POST).
    exists vs', σs', r1. split; [|done]. etrans; eauto.
  - inversion ST.
    + constructor 1. intros.
      destruct (STEP _ _ STEPT) as (es' & σs' & r1 & n' & STEPS' & POST).
      exists es', σs', r1, n'. split; [|done].
      left. destruct STEPS' as [?|[]].
      * eapply tc_rtc_l; eauto.
      * simplify_eq. by apply tc_once.
    + econstructor 2; eauto. by etrans.
151
Qed.
Ralf Jung's avatar
Ralf Jung committed
152

Hai Dang's avatar
Hai Dang committed
153
154
155
156
157
158
159
160
161
Lemma sim_body_copy_unique_l
  fs ft (r r': resUR) (h: heaplet) n (l: loc) t T (ss st: scalar) et σs σt Φ :
  tsize T = 1%nat 
  r  r'  res_tag t tkUnique h 
  h !! l = Some (ss,st) 
  (r {n,fs,ft} (#[ss], σs)  (et, σt) : Φ : Prop) 
  r {n,fs,ft} (Copy (Place l (Tagged t) T), σs)  (et, σt) : Φ.
Proof. apply sim_body_copy_local_unique_l. by right. Qed.

Hai Dang's avatar
Hai Dang committed
162
Lemma sim_body_copy_local_l fs ft r r' n l tg ty ss st et σs σt Φ :
Ralf Jung's avatar
Ralf Jung committed
163
  tsize ty = 1%nat 
Hai Dang's avatar
Hai Dang committed
164
  r  r'  res_loc l [(ss,st)] tg 
Hai Dang's avatar
Hai Dang committed
165
  (r {n,fs,ft} (#[ss], σs)  (et, σt) : Φ) 
Ralf Jung's avatar
Ralf Jung committed
166
167
168
169
  r {n,fs,ft}
    (Copy (Place l (Tagged tg) ty), σs)  (et, σt)
  : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
170
  intros Hty Hr. eapply sim_body_copy_local_unique_l; [by left|..]; eauto.
Hai Dang's avatar
Hai Dang committed
171
172
  by rewrite lookup_insert.
Qed.
Ralf Jung's avatar
Ralf Jung committed
173

Ralf Jung's avatar
Ralf Jung committed
174
End left.