language.v 6.61 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 5 6 7 8 9 10 11 12 13 14 15 16
Section language_mixin.
  Context {expr val state : Type}.
  Context (of_val : val  expr).
  Context (to_val : expr  option val).
  Context (prim_step : expr  state  expr  state  list expr  Prop).

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

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

Arguments Language {_ _ _ _ _ _} _.
32 33 34 35
Arguments of_val {_} _.
Arguments to_val {_} _.
Arguments prim_step {_} _ _ _ _ _.

36 37 38
Canonical Structure stateC Λ := leibnizC (state Λ).
Canonical Structure valC Λ := leibnizC (val Λ).
Canonical Structure exprC Λ := leibnizC (expr Λ).
39 40

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

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

53
Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55
Proof. constructor; naive_solver. Qed.

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

68
  Definition reducible (e : expr Λ) (σ : state Λ) :=
69
     e' σ' efs, prim_step e σ e' σ' efs.
70
  Definition irreducible (e : expr Λ) (σ : state Λ) :=
71 72
     e' σ' efs, ¬prim_step e σ e' σ' efs.

73
  (* This (weak) form of atomicity is enough to open invariants when WP ensures
Ralf Jung's avatar
Ralf Jung committed
74 75 76 77
     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
78 79 80
     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v). *)
  Class Atomic (e : expr Λ) : Prop :=
    atomic σ e' σ' efs : prim_step e σ e' σ' efs  irreducible e' σ'.
81

82
  (* To open invariants with a WP that does not ensure safety, we need a
Ralf Jung's avatar
Ralf Jung committed
83 84 85
     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. *)
86 87
  Class StronglyAtomic (e : expr Λ) : Prop :=
    strongly_atomic σ e' σ' efs : prim_step e σ e' σ' efs  is_Some (to_val e').
88

89
  Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
90
    | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
91
       ρ1 = (t1 ++ e1 :: t2, σ1) 
92 93
       ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) 
       prim_step e1 σ1 e2 σ2 efs 
94 95
       step ρ1 ρ2.

Robbert Krebbers's avatar
Robbert Krebbers committed
96 97
  Lemma of_to_val_flip v e : of_val v = e  to_val e = Some v.
  Proof. intros <-. by rewrite to_of_val. Qed.
98 99 100

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

108 109
  Lemma strongly_atomic_atomic e : StronglyAtomic e  Atomic e.
  Proof. unfold StronglyAtomic, Atomic. eauto using val_irreducible. Qed.
110

111 112 113 114 115 116 117 118 119
  Lemma reducible_fill `{LanguageCtx Λ K} e σ :
    to_val e = None  reducible (K e) σ  reducible e σ.
  Proof.
    intros ? (e'&σ'&efs&Hstep); unfold reducible.
    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.
120 121 122 123 124 125 126 127 128 129

  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).
  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
130 131 132 133 134 135 136 137

  Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
    pure_exec_safe σ :
      P  reducible e1 σ;
    pure_exec_puredet σ1 e2' σ2 efs :
      P  prim_step e1 σ1 e2' σ2 efs  σ1 = σ2  e2 = e2'  efs = [];
  }.

138
  Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) :
Dan Frumin's avatar
Dan Frumin committed
139 140 141
    (P  PureExec True e1 e2) 
    PureExec P e1 e2.
  Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
142

143 144 145 146 147 148 149 150 151 152 153 154 155
  Global Instance pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
    PureExec φ e1 e2 
    PureExec φ (K e1) (K e2).
  Proof.
    intros [Hred Hstep]. split.
    - intros σ ?. destruct (Hred σ) as (? & ? & ? & ?); first done.
      do 3 eexists. eapply fill_step. done.
    - intros σ ???? Hpstep. edestruct fill_step_inv as (? & ? & ?); [|exact Hpstep|].
      + destruct (Hred σ) as (? & ? & ? & ?); first done.
        eapply val_stuck. done.
      + edestruct Hstep as (? & ? & ?); [done..|]. by subst.
  Qed.

156 157 158
  (* This is a family of frequent assumptions for PureExec *)
  Class IntoVal (e : expr Λ) (v : val Λ) :=
    into_val : to_val e = Some v.
Robbert Krebbers's avatar
Robbert Krebbers committed
159 160 161 162 163 164 165 166 167

  Class AsVal (e : expr Λ) := as_val : is_Some (to_val e).
  (* 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.
    rewrite /AsVal /= to_of_val; eauto.
  Qed.
168
End language.