language.v 9.17 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 stateC Λ := leibnizC (state Λ).
Canonical Structure valC Λ := leibnizC (val Λ).
Canonical Structure exprC Λ := leibnizC (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 σ.
83

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

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

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

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

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

  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.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
133 134
  Lemma reducible_no_obs_reducible e σ : reducible_no_obs e σ  reducible e σ.
  Proof. intros (?&?&?&?); eexists; eauto. Qed.
135
  Lemma val_irreducible e σ : is_Some (to_val e)  irreducible e σ.
136
  Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed.
137
  Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
138
  Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Ralf Jung's avatar
Ralf Jung committed
139

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

144 145 146
  Lemma reducible_fill `{LanguageCtx Λ K} e σ :
    to_val e = None  reducible (K e) σ  reducible e σ.
  Proof.
147
    intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
148 149
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
150 151 152 153 154 155
  Lemma reducible_no_obs_fill `{LanguageCtx Λ K} e σ :
    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.
156 157 158
  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.
159

160 161
  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).
162 163 164 165 166 167 168
  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
169

170 171 172
  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
173
    intros Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.
174 175
  Qed.

176
  Record pure_step (e1 e2 : expr Λ) := {
177 178
    pure_step_safe σ1 : reducible_no_obs e1 σ1;
    pure_step_det σ1 κ e2' σ2 efs :
179
      prim_step e1 σ1 κ e2' σ2 efs  κ = []  σ1 = σ2  e2 = e2'  efs = []
Dan Frumin's avatar
Dan Frumin committed
180 181
  }.

182 183 184
  (* 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 Λ) :=
185
    pure_exec : φ  relations.nsteps pure_step n e1 e2.
186

187 188 189
  Lemma pure_step_ctx K `{LanguageCtx Λ K} e1 e2 :
    pure_step e1 e2 
    pure_step (K e1) (K e2).
190 191
  Proof.
    intros [Hred Hstep]. split.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
192
    - unfold reducible_no_obs in *. naive_solver eauto using fill_step.
193
    - intros σ1 κ e2' σ2 efs Hpstep.
194
      destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
195
      + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
196
      + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
197 198
  Qed.

199
  Lemma pure_step_nsteps_ctx K `{LanguageCtx Λ K} n e1 e2 :
200 201
    relations.nsteps pure_step n e1 e2 
    relations.nsteps pure_step n (K e1) (K e2).
202 203 204 205 206 207 208 209
  Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed.

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

210 211
  (* This is a family of frequent assumptions for PureExec *)
  Class IntoVal (e : expr Λ) (v : val Λ) :=
212
    into_val : of_val v = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
213

214
  Class AsVal (e : expr Λ) := as_val :  v, of_val v = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
215 216 217 218 219
  (* 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.
220
    rewrite /AsVal /=; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
221
  Qed.
Ralf Jung's avatar
Ralf Jung committed
222 223 224
  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.
225
End language.