language.v 13 KB
Newer Older
1
From iris.algebra Require Export ofe.
2
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
3

4
Section language_mixin.
5
  Context {expr val state observation : Type}.
6 7
  Context (of_val : val  expr).
  Context (to_val : expr  option val).
Ralf Jung's avatar
Ralf Jung committed
8 9 10
  (** We annotate the reduction relation with observations [κ], which we will
     use in the definition of weakest preconditions to predict future
     observations and assert correctness of the predictions. *)
11
  Context (prim_step : expr  state  list observation  expr  state  list expr  Prop).
12 13 14 15

  Record LanguageMixin := {
    mixin_to_of_val v : to_val (of_val v) = Some v;
    mixin_of_to_val e v : to_val e = Some v  of_val v = e;
16
    mixin_val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs  to_val e = None
17 18 19
  }.
End language_mixin.

20 21 22 23
Structure language := Language {
  expr : Type;
  val : Type;
  state : Type;
24
  observation : Type;
25 26
  of_val : val  expr;
  to_val : expr  option val;
27
  prim_step : expr  state  list observation  expr  state  list expr  Prop;
28
  language_mixin : LanguageMixin of_val to_val prim_step
Ralf Jung's avatar
Ralf Jung committed
29
}.
Janno's avatar
Janno committed
30 31 32
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Bind Scope expr_scope with expr.
33
Bind Scope val_scope with val.
34

35
Arguments Language {_ _ _ _ _ _ _} _.
36 37
Arguments of_val {_} _.
Arguments to_val {_} _.
38
Arguments prim_step {_} _ _ _ _ _ _.
39

40 41 42
Canonical Structure stateO Λ := leibnizO (state Λ).
Canonical Structure valO Λ := leibnizO (val Λ).
Canonical Structure exprO Λ := leibnizO (expr Λ).
43 44

Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
Ralf Jung's avatar
Ralf Jung committed
45

46
Class LanguageCtx {Λ : language} (K : expr Λ  expr Λ) := {
47 48
  fill_not_val e :
    to_val e = None  to_val (K e) = None;
49 50 51 52 53 54
  fill_step e1 σ1 κ e2 σ2 efs :
    prim_step e1 σ1 κ e2 σ2 efs 
    prim_step (K e1) σ1 κ (K e2) σ2 efs;
  fill_step_inv e1' σ1 κ e2 σ2 efs :
    to_val e1' = None  prim_step (K e1') σ1 κ e2 σ2 efs 
     e2', e2 = K e2'  prim_step e1' σ1 κ e2' σ2 efs
55 56
}.

57
Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59
Proof. constructor; naive_solver. Qed.

Ralf Jung's avatar
Ralf Jung committed
60
Inductive atomicity := StronglyAtomic | WeaklyAtomic.
61

62
Section language.
63 64
  Context {Λ : language}.
  Implicit Types v : val Λ.
65 66 67 68 69 70
  Implicit Types e : expr Λ.

  Lemma to_of_val v : to_val (of_val v) = Some v.
  Proof. apply language_mixin. Qed.
  Lemma of_to_val e v : to_val e = Some v  of_val v = e.
  Proof. apply language_mixin. Qed.
71
  Lemma val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs  to_val e = None.
72
  Proof. apply language_mixin. Qed.
Ralf Jung's avatar
Ralf Jung committed
73

74
  Definition reducible (e : expr Λ) (σ : state Λ) :=
75
     κ e' σ' efs, prim_step e σ κ e' σ' efs.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
76 77
  (* Total WP only permits reductions without observations *)
  Definition reducible_no_obs (e : expr Λ) (σ : state Λ) :=
78
     e' σ' efs, prim_step e σ [] e' σ' efs.
79
  Definition irreducible (e : expr Λ) (σ : state Λ) :=
80
     κ e' σ' efs, ¬prim_step e σ κ e' σ' efs.
81 82
  Definition stuck (e : expr Λ) (σ : state Λ) :=
    to_val e = None  irreducible e σ.
Amin Timany's avatar
Amin Timany committed
83 84
  Definition not_stuck (e : expr Λ) (σ : state Λ) :=
    is_Some (to_val e)  reducible e σ.
85

Ralf Jung's avatar
Ralf Jung committed
86
  (* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open
Ralf Jung's avatar
Ralf Jung committed
87 88 89 90
     invariants when WP ensures safety, i.e., programs never can get stuck.  We
     have an example in lambdaRust of an expression that is atomic in this
     sense, but not in the stronger sense defined below, and we have to be able
     to open invariants around that expression.  See `CasStuckS` in
91
     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).
92

Ralf Jung's avatar
Ralf Jung committed
93
     [Atomic StronglyAtomic]: To open invariants with a WP that does not ensure
Ralf Jung's avatar
Ralf Jung committed
94 95 96 97
     safety, we need a stronger form of atomicity.  With the above definition,
     in case `e` reduces to a stuck non-value, there is no proof that the
     invariants have been established again. *)
  Class Atomic (a : atomicity) (e : expr Λ) : Prop :=
98 99
    atomic σ e' κ σ' efs :
      prim_step e σ κ e' σ' efs 
Ralf Jung's avatar
Ralf Jung committed
100
      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
101

102
  Inductive step (ρ1 : cfg Λ) (κ : list (observation Λ)) (ρ2 : cfg Λ) : Prop :=
103
    | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
104
       ρ1 = (t1 ++ e1 :: t2, σ1) 
105
       ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) 
106 107
       prim_step e1 σ1 κ e2 σ2 efs 
       step ρ1 κ ρ2.
Tej Chajed's avatar
Tej Chajed committed
108
  Hint Constructors step : core.
109

110
  Inductive nsteps : nat  cfg Λ  list (observation Λ)  cfg Λ  Prop :=
Ralf Jung's avatar
Ralf Jung committed
111 112 113 114 115
    | nsteps_refl ρ :
       nsteps 0 ρ [] ρ
    | nsteps_l n ρ1 ρ2 ρ3 κ κs :
       step ρ1 κ ρ2 
       nsteps n ρ2 κs ρ3 
116
       nsteps (S n) ρ1 (κ ++ κs) ρ3.
Tej Chajed's avatar
Tej Chajed committed
117
  Hint Constructors nsteps : core.
118

Ralf Jung's avatar
Ralf Jung committed
119
  Definition erased_step (ρ1 ρ2 : cfg Λ) :=  κ, step ρ1 κ ρ2.
120

121 122
  (** [rtc erased_step] and [nsteps] encode the same thing, just packaged
      in a different way. *)
123
  Lemma erased_steps_nsteps ρ1 ρ2 :
124
    rtc erased_step ρ1 ρ2   n κs, nsteps n ρ1 κs ρ2.
125
  Proof.
126
    split.
127 128 129
    - induction 1; firstorder eauto. (* FIXME: [naive_solver eauto] should be able to handle this *)
    - intros (n & κs & Hsteps). unfold erased_step.
      induction Hsteps; eauto using rtc_refl, rtc_l.
130
  Qed.
131

Robbert Krebbers's avatar
Robbert Krebbers committed
132 133
  Lemma of_to_val_flip v e : of_val v = e  to_val e = Some v.
  Proof. intros <-. by rewrite to_of_val. Qed.
134 135 136

  Lemma not_reducible e σ : ¬reducible e σ  irreducible e σ.
  Proof. unfold reducible, irreducible. naive_solver. Qed.
137
  Lemma reducible_not_val e σ : reducible e σ  to_val e = None.
138
  Proof. intros (?&?&?&?&?); eauto using val_stuck. Qed.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
139 140
  Lemma reducible_no_obs_reducible e σ : reducible_no_obs e σ  reducible e σ.
  Proof. intros (?&?&?&?); eexists; eauto. Qed.
141
  Lemma val_irreducible e σ : is_Some (to_val e)  irreducible e σ.
142
  Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed.
143
  Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
144
  Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Amin Timany's avatar
Amin Timany committed
145 146 147 148 149
  Lemma not_not_stuck e σ : ¬not_stuck e σ  stuck e σ.
  Proof.
    rewrite /stuck /not_stuck -not_eq_None_Some -not_reducible.
    destruct (decide (to_val e = None)); naive_solver.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
150

151 152 153
  Lemma strongly_atomic_atomic e a :
    Atomic StronglyAtomic e  Atomic a e.
  Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
154

155
  Lemma reducible_fill `{!@LanguageCtx Λ K} e σ :
156 157
    to_val e = None  reducible (K e) σ  reducible e σ.
  Proof.
158
    intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
159 160
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.
161
  Lemma reducible_no_obs_fill `{!@LanguageCtx Λ K} e σ :
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
162 163 164 165 166
    to_val e = None  reducible_no_obs (K e) σ  reducible_no_obs e σ.
  Proof.
    intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs.
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.
167
  Lemma irreducible_fill `{!@LanguageCtx Λ K} e σ :
168 169
    to_val e = None  irreducible e σ  irreducible (K e) σ.
  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
170

Hai Dang's avatar
Hai Dang committed
171 172
  Lemma stuck_fill `{!@LanguageCtx Λ K} e σ :
    stuck e σ  stuck (K e) σ.
Hai Dang's avatar
Hai Dang committed
173
  Proof. intros [??]. split. by apply fill_not_val. by apply irreducible_fill. Qed.
Hai Dang's avatar
Hai Dang committed
174

175 176
  Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) κ σ1 σ2 :
    t1  t1'  step (t1,σ1) κ (t2,σ2)   t2', t2  t2'  step (t1',σ1) κ (t2',σ2).
177 178 179 180 181 182 183
  Proof.
    intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=.
    move: Ht; rewrite -Permutation_middle (symmetry_iff ()).
    intros (tl'&tr'&->&Ht)%Permutation_cons_inv.
    exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
    by rewrite -!Permutation_middle !assoc_L Ht.
  Qed.
Dan Frumin's avatar
Dan Frumin committed
184

Amin Timany's avatar
Amin Timany committed
185 186 187 188 189 190 191 192 193 194 195 196
  Lemma step_insert i t2 σ2 e κ e' σ3 efs :
    t2 !! i = Some e 
    prim_step e σ2 κ e' σ3 efs 
    step (t2, σ2) κ (<[i:=e']>t2 ++ efs, σ3).
  Proof.
    intros.
    edestruct (elem_of_list_split_length t2) as (t21&t22&?&?);
      first (by eauto using elem_of_list_lookup_2); simplify_eq.
    econstructor; eauto.
    by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
  Qed.

197 198 199
  Lemma erased_step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
    t1  t1'  erased_step (t1,σ1) (t2,σ2)   t2', t2  t2'  erased_step (t1',σ1) (t2',σ2).
  Proof.
Ralf Jung's avatar
Ralf Jung committed
200
    intros Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.
Ralf Jung's avatar
Ralf Jung committed
201
     (* FIXME: [naive_solver] should be able to handle this *)
202 203
  Qed.

204
  Record pure_step (e1 e2 : expr Λ) := {
205 206
    pure_step_safe σ1 : reducible_no_obs e1 σ1;
    pure_step_det σ1 κ e2' σ2 efs :
207
      prim_step e1 σ1 κ e2' σ2 efs  κ = []  σ2 = σ1  e2' = e2  efs = []
Dan Frumin's avatar
Dan Frumin committed
208 209
  }.

Amin Timany's avatar
Amin Timany committed
210 211
  Notation pure_steps_tp := (Forall2 (rtc pure_step)).

212 213 214
  (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
  succeeding when it did not actually do anything. *)
  Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
215
    pure_exec : φ  relations.nsteps pure_step n e1 e2.
216

217
  Lemma pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
218 219
    pure_step e1 e2 
    pure_step (K e1) (K e2).
220 221
  Proof.
    intros [Hred Hstep]. split.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
222
    - unfold reducible_no_obs in *. naive_solver eauto using fill_step.
223
    - intros σ1 κ e2' σ2 efs Hpstep.
224
      destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
225
      + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
226
      + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
227 228
  Qed.

229
  Lemma pure_step_nsteps_ctx K `{!@LanguageCtx Λ K} n e1 e2 :
230 231
    relations.nsteps pure_step n e1 e2 
    relations.nsteps pure_step n (K e1) (K e2).
Amin Timany's avatar
Amin Timany committed
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
  Proof. eauto using nsteps_congruence, pure_step_ctx. Qed.

  Lemma rtc_pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
    rtc pure_step e1 e2  rtc pure_step (K e1) (K e2).
  Proof. eauto using rtc_congruence, pure_step_ctx. Qed.

  Lemma not_stuck_under_ectx K `{!@LanguageCtx Λ K} e σ :
    not_stuck (K e) σ  not_stuck e σ.
  Proof.
    rewrite /not_stuck /reducible /=.
    intros [[? HK]|(?&?&?&?&Hstp)]; simpl in *.
    - left. apply not_eq_None_Some; intros ?%fill_not_val; simplify_eq.
    - destruct (to_val e) eqn:?; first by left; eauto.
      apply fill_step_inv in Hstp; naive_solver.
  Qed.
247 248

  (* We do not make this an instance because it is awfully general. *)
249
  Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 :
250 251 252 253
    PureExec φ n e1 e2 
    PureExec φ n (K e1) (K e2).
  Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.

254 255
  (* This is a family of frequent assumptions for PureExec *)
  Class IntoVal (e : expr Λ) (v : val Λ) :=
256
    into_val : of_val v = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
257

258
  Class AsVal (e : expr Λ) := as_val :  v, of_val v = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
259 260 261 262 263
  (* There is no instance [IntoVal → AsVal] as often one can solve [AsVal] more
  efficiently since no witness has to be computed. *)
  Global Instance as_vals_of_val vs : TCForall AsVal (of_val <$> vs).
  Proof.
    apply TCForall_Forall, Forall_fmap, Forall_true=> v.
264
    rewrite /AsVal /=; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
265
  Qed.
Amin Timany's avatar
Amin Timany committed
266

Ralf Jung's avatar
Ralf Jung committed
267 268 269
  Lemma as_val_is_Some e :
    ( v, of_val v = e)  is_Some (to_val e).
  Proof. intros [v <-]. rewrite to_of_val. eauto. Qed.
Amin Timany's avatar
Amin Timany committed
270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317

  Lemma prim_step_not_stuck e σ κ e' σ' efs :
    prim_step e σ κ e' σ' efs  not_stuck e σ.
  Proof. rewrite /not_stuck /reducible. eauto 10. Qed.

  Lemma rtc_pure_step_val `{!Inhabited (state Λ)} v e :
    rtc pure_step (of_val v) e  to_val e = Some v.
  Proof.
    intros ?; rewrite <- to_of_val.
    f_equal; symmetry; eapply rtc_nf; first done.
    intros [e' [Hstep _]].
    destruct (Hstep inhabitant) as (?&?&?&Hval%val_stuck).
    by rewrite to_of_val in Hval.
  Qed.

  (** Let thread pools [t1] and [t3] be such that each thread in [t1] makes
   (zero or more) pure steps to the corresponding thread in [t3]. Furthermore,
   let [t2] be a thread pool such that [t1] under state [σ1] makes a (single)
   step to thread pool [t2] and state [σ2]. In this situation, either the step
   from [t1] to [t2] corresponds to one of the pure steps between [t1] and [t3],
   or, there is an [i] such that [i]th thread does not participate in the
   pure steps between [t1] and [t3] and [t2] corresponds to taking a step in
   the [i]th thread starting from [t1]. *)
  Lemma erased_step_pure_step_tp t1 σ1 t2 σ2 t3 :
    erased_step (t1, σ1) (t2, σ2) 
    pure_steps_tp t1 t3 
    (σ1 = σ2  pure_steps_tp t2 t3) 
    ( i e efs e' κ,
      t1 !! i = Some e  t3 !! i = Some e 
      t2 = <[i:=e']>t1 ++ efs 
      prim_step e σ1 κ e' σ2 efs).
  Proof.
    intros [κ [e σ e' σ' ? t11 t12 ?? Hstep]] Hps; simplify_eq/=.
    apply Forall2_app_inv_l in Hps
      as (t31&?&Hpsteps&(e''&t32&Hps&?&->)%Forall2_cons_inv_l&->).
    destruct Hps as [e|e1 e2 e3 [_ Hprs]].
    - right.
      exists (length t11), e, efs, e', κ; split_and!; last done.
      + by rewrite lookup_app_r // Nat.sub_diag.
      + apply Forall2_length in Hpsteps.
        by rewrite lookup_app_r Hpsteps // Nat.sub_diag.
      + by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
    - edestruct Hprs as (?&?&?&?); first done; simplify_eq.
      left; split; first done.
      rewrite right_id_L.
      eauto using Forall2_app.
  Qed.

318
End language.
Amin Timany's avatar
Amin Timany committed
319 320

Notation pure_steps_tp := (Forall2 (rtc pure_step)).