language.v 5.6 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
Structure language := Language {
  expr : Type;
  val : Type;
  state : Type;
  of_val : val  expr;
  to_val : expr  option val;
10
  prim_step : expr  state  expr  state  list expr  Prop;
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12
  to_of_val v : to_val (of_val v) = Some v;
  of_to_val e v : to_val e = Some v  of_val v = e;
13
  val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs  to_val e = None
Ralf Jung's avatar
Ralf Jung committed
14
}.
Janno's avatar
Janno committed
15 16 17
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Bind Scope expr_scope with expr.
18
Bind Scope val_scope with val.
19 20 21 22 23
Arguments of_val {_} _.
Arguments to_val {_} _.
Arguments prim_step {_} _ _ _ _ _.
Arguments to_of_val {_} _.
Arguments of_to_val {_} _ _ _.
24
Arguments val_stuck {_} _ _ _ _ _ _.
25

26 27 28
Canonical Structure stateC Λ := leibnizC (state Λ).
Canonical Structure valC Λ := leibnizC (val Λ).
Canonical Structure exprC Λ := leibnizC (expr Λ).
29 30

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

32 33 34 35 36 37 38 39 40 41 42
Class LanguageCtx (Λ : language) (K : expr Λ  expr Λ) := {
  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
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45
Instance language_ctx_id Λ : LanguageCtx Λ id.
Proof. constructor; naive_solver. Qed.

46
Variant stuckness := not_stuck | maybe_stuck.
47

48
Section language.
49 50
  Context {Λ : language}.
  Implicit Types v : val Λ.
Ralf Jung's avatar
Ralf Jung committed
51

52
  Definition reducible (e : expr Λ) (σ : state Λ) :=
53
     e' σ' efs, prim_step e σ e' σ' efs.
54
  Definition irreducible (e : expr Λ) (σ : state Λ) :=
55
     e' σ' efs, ¬prim_step e σ e' σ' efs.
56 57
  Definition progressive (e : expr Λ) (σ : state Λ) :=
    is_Some (to_val e)  reducible e σ.
58

59
  (* [Atomic not_stuck]: This (weak) form of atomicity is enough to open invariants when WP ensures
Ralf Jung's avatar
Ralf Jung committed
60 61 62 63
     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
64
     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).
65

66
     [Atomic maybe_stuck]: To open invariants with a WP that does not ensure safety, we need a
Ralf Jung's avatar
Ralf Jung committed
67 68 69
     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. *)
70 71 72 73
  Class Atomic (s : stuckness) (e : expr Λ) : Prop :=
    atomic σ e' σ' efs :
      prim_step e σ e' σ' efs 
      if s is not_stuck then irreducible e' σ' else is_Some (to_val e').
74

75
  Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
76
    | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
77
       ρ1 = (t1 ++ e1 :: t2, σ1) 
78 79
       ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) 
       prim_step e1 σ1 e2 σ2 efs 
80 81
       step ρ1 ρ2.

Robbert Krebbers's avatar
Robbert Krebbers committed
82 83
  Lemma of_to_val_flip v e : of_val v = e  to_val e = Some v.
  Proof. intros <-. by rewrite to_of_val. Qed.
84 85 86

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

94 95
  Lemma strongly_atomic_atomic e : Atomic maybe_stuck e  Atomic not_stuck e.
  Proof. unfold Atomic. eauto using val_irreducible. Qed.
96

97 98 99 100 101 102 103 104 105
  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.
106 107 108 109 110 111 112 113 114 115

  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
116 117 118 119 120 121 122 123

  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 = [];
  }.

124
  Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) :
Dan Frumin's avatar
Dan Frumin committed
125 126 127
    (P  PureExec True e1 e2) 
    PureExec P e1 e2.
  Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
128 129 130 131

  (* 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
132 133 134 135 136 137 138 139 140

  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.
141
End language.