language.v 8.31 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).
8
  (** We annotate the reduction relation with observations [κ], which we will use in the definition
9 10
     of weakest preconditions to keep track of creating and resolving prophecy variables. *)
  Context (prim_step : expr  state  option observation  expr  state  list expr  Prop).
11 12 13 14

  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;
15
    mixin_val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs  to_val e = None
16 17 18
  }.
End language_mixin.

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

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

39 40 41
Canonical Structure stateC Λ := leibnizC (state Λ).
Canonical Structure valC Λ := leibnizC (val Λ).
Canonical Structure exprC Λ := leibnizC (expr Λ).
42 43

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

45
Class LanguageCtx {Λ : language} (K : expr Λ  expr Λ) := {
46 47
  fill_not_val e :
    to_val e = None  to_val (K e) = None;
48 49 50 51 52 53
  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
54 55
}.

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

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

61
Section language.
62 63
  Context {Λ : language}.
  Implicit Types v : val Λ.
64 65 66 67 68 69
  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.
70
  Lemma val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs  to_val e = None.
71
  Proof. apply language_mixin. Qed.
Ralf Jung's avatar
Ralf Jung committed
72

73
  Definition reducible (e : expr Λ) (σ : state Λ) :=
74
     κ e' σ' efs, prim_step e σ κ e' σ' efs.
75
  Definition irreducible (e : expr Λ) (σ : state Λ) :=
76
     κ e' σ' efs, ¬prim_step e σ κ e' σ' efs.
77 78
  Definition stuck (e : expr Λ) (σ : state Λ) :=
    to_val e = None  irreducible e σ.
79

Ralf Jung's avatar
Ralf Jung committed
80
  (* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open
Ralf Jung's avatar
Ralf Jung committed
81 82 83 84
     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
85
     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).
86

Ralf Jung's avatar
Ralf Jung committed
87
     [Atomic StronglyAtomic]: To open invariants with a WP that does not ensure
Ralf Jung's avatar
Ralf Jung committed
88 89 90 91
     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 :=
92 93
    atomic σ e' κ σ' efs :
      prim_step e σ κ e' σ' efs 
Ralf Jung's avatar
Ralf Jung committed
94
      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
95

96
  Inductive step (ρ1 : cfg Λ) (κ : option (observation Λ)) (ρ2 : cfg Λ) : Prop :=
97
    | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
98
       ρ1 = (t1 ++ e1 :: t2, σ1) 
99
       ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) 
100 101 102
       prim_step e1 σ1 κ e2 σ2 efs 
       step ρ1 κ ρ2.

103 104 105 106 107
  (* TODO (MR) introduce notation ::? for cons_obs and suggest for inclusion to stdpp? *)
  Definition cons_obs {A} (x : option A) (xs : list A) :=
    option_list x ++ xs.

  Inductive nsteps : nat  cfg Λ  list (observation Λ)  cfg Λ  Prop :=
108 109 110 111 112
  | nsteps_refl ρ :
      nsteps 0 ρ [] ρ
  | nsteps_l n ρ1 ρ2 ρ3 κ κs :
      step ρ1 κ ρ2 
      nsteps n ρ2 κs ρ3 
113
      nsteps (S n) ρ1 (cons_obs κ κs) ρ3.
114 115 116 117 118 119

  Definition erased_step (ρ1 ρ2 : cfg Λ) := exists κ, step ρ1 κ ρ2.

  Hint Constructors step nsteps.

  Lemma erased_steps_nsteps ρ1 ρ2 :
120
    rtc erased_step ρ1 ρ2 
121 122 123 124
     n κs, nsteps n ρ1 κs ρ2.
  Proof.
    induction 1; firstorder; eauto.
  Qed.
125

Robbert Krebbers's avatar
Robbert Krebbers committed
126 127
  Lemma of_to_val_flip v e : of_val v = e  to_val e = Some v.
  Proof. intros <-. by rewrite to_of_val. Qed.
128 129 130

  Lemma not_reducible e σ : ¬reducible e σ  irreducible e σ.
  Proof. unfold reducible, irreducible. naive_solver. Qed.
131
  Lemma reducible_not_val e σ : reducible e σ  to_val e = None.
132
  Proof. intros (?&?&?&?&?); eauto using val_stuck. Qed.
133
  Lemma val_irreducible e σ : is_Some (to_val e)  irreducible e σ.
134
  Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed.
135
  Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
136
  Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Ralf Jung's avatar
Ralf Jung committed
137

138 139 140
  Lemma strongly_atomic_atomic e a :
    Atomic StronglyAtomic e  Atomic a e.
  Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
141

142 143 144
  Lemma reducible_fill `{LanguageCtx Λ K} e σ :
    to_val e = None  reducible (K e) σ  reducible e σ.
  Proof.
145
    intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
146 147 148 149 150
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.
  Lemma irreducible_fill `{LanguageCtx Λ K} e σ :
    to_val e = None  irreducible e σ  irreducible (K e) σ.
  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
151

152 153
  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).
154 155 156 157 158 159 160
  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
161

162 163 164 165 166 167
  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.
    intros* Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
168 169 170
  Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
    pure_exec_safe σ :
      P  reducible e1 σ;
171
    pure_exec_puredet σ1 κ e2' σ2 efs :
172
      P  prim_step e1 σ1 κ e2' σ2 efs  κ = None  σ1 = σ2  e2 = e2'  efs = [];
Dan Frumin's avatar
Dan Frumin committed
173 174
  }.

175
  Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) :
Dan Frumin's avatar
Dan Frumin committed
176 177 178
    (P  PureExec True e1 e2) 
    PureExec P e1 e2.
  Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
179

180 181
  (* We do not make this an instance because it is awfully general. *)
  Lemma pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
182 183 184 185
    PureExec φ e1 e2 
    PureExec φ (K e1) (K e2).
  Proof.
    intros [Hred Hstep]. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
    - unfold reducible in *. naive_solver eauto using fill_step.
187 188 189 190
    - intros σ1 κ e2' σ2 efs ? Hpstep.
      destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
      + destruct (Hred σ1) as (? & ? & ? & ? & ?); eauto using val_stuck.
      + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
191 192
  Qed.

193 194
  (* This is a family of frequent assumptions for PureExec *)
  Class IntoVal (e : expr Λ) (v : val Λ) :=
195
    into_val : of_val v = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
196

197
  Class AsVal (e : expr Λ) := as_val :  v, of_val v = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
198 199 200 201 202
  (* 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.
203
    rewrite /AsVal /=; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
  Qed.
Ralf Jung's avatar
Ralf Jung committed
205 206 207
  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.
208
End language.