language.v 8.9 KB
 Ralf Jung committed Nov 22, 2016 1 ``````From iris.algebra Require Export ofe. `````` Ralf Jung committed Jan 05, 2017 2 ``````Set Default Proof Using "Type". `````` Ralf Jung committed Jan 04, 2016 3 `````` `````` Robbert Krebbers committed Nov 23, 2017 4 ``````Section language_mixin. `````` 5 `````` Context {expr val state observation : Type}. `````` Robbert Krebbers committed Nov 23, 2017 6 7 `````` Context (of_val : val → expr). Context (to_val : expr → option val). `````` Ralf Jung committed Oct 05, 2018 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 → option observation → expr → state → list expr → Prop). `````` Robbert Krebbers committed Nov 23, 2017 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 `````` Robbert Krebbers committed Nov 23, 2017 17 18 19 `````` }. End language_mixin. `````` Robbert Krebbers committed Feb 01, 2016 20 21 22 23 ``````Structure language := Language { expr : Type; val : Type; state : Type; `````` 24 `````` observation : Type; `````` Robbert Krebbers committed Feb 01, 2016 25 26 `````` of_val : val → expr; to_val : expr → option val; `````` 27 `````` prim_step : expr → state → option observation → expr → state → list expr → Prop; `````` Robbert Krebbers committed Nov 23, 2017 28 `````` language_mixin : LanguageMixin of_val to_val prim_step `````` Ralf Jung committed Jan 04, 2016 29 ``````}. `````` Janno committed Aug 25, 2016 30 31 32 ``````Delimit Scope expr_scope with E. Delimit Scope val_scope with V. Bind Scope expr_scope with expr. `````` Jacques-Henri Jourdan committed Jan 04, 2017 33 ``````Bind Scope val_scope with val. `````` Robbert Krebbers committed Nov 23, 2017 34 `````` `````` 35 ``````Arguments Language {_ _ _ _ _ _ _} _. `````` Robbert Krebbers committed Feb 01, 2016 36 37 ``````Arguments of_val {_} _. Arguments to_val {_} _. `````` 38 ``````Arguments prim_step {_} _ _ _ _ _ _. `````` Robbert Krebbers committed Feb 01, 2016 39 `````` `````` Robbert Krebbers committed Mar 18, 2016 40 41 42 ``````Canonical Structure stateC Λ := leibnizC (state Λ). Canonical Structure valC Λ := leibnizC (val Λ). Canonical Structure exprC Λ := leibnizC (expr Λ). `````` Robbert Krebbers committed Feb 01, 2016 43 44 `````` Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type. `````` Ralf Jung committed Jan 04, 2016 45 `````` `````` Robbert Krebbers committed Nov 23, 2017 46 ``````Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := { `````` Robbert Krebbers committed Mar 15, 2017 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 `````` Robbert Krebbers committed Mar 15, 2017 55 56 ``````}. `````` Robbert Krebbers committed Nov 23, 2017 57 ``````Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)). `````` Robbert Krebbers committed Sep 21, 2017 58 59 ``````Proof. constructor; naive_solver. Qed. `````` Ralf Jung committed Dec 07, 2017 60 ``````Inductive atomicity := StronglyAtomic | WeaklyAtomic. `````` David Swasey committed Nov 09, 2017 61 `````` `````` Robbert Krebbers committed Jan 16, 2016 62 ``````Section language. `````` Robbert Krebbers committed Feb 01, 2016 63 64 `````` Context {Λ : language}. Implicit Types v : val Λ. `````` Robbert Krebbers committed Nov 23, 2017 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. `````` Robbert Krebbers committed Nov 23, 2017 72 `````` Proof. apply language_mixin. Qed. `````` Ralf Jung committed Jan 04, 2016 73 `````` `````` Robbert Krebbers committed Feb 01, 2016 74 `````` Definition reducible (e : expr Λ) (σ : state Λ) := `````` 75 `````` ∃ κ e' σ' efs, prim_step e σ κ e' σ' efs. `````` Ralf Jung committed Oct 05, 2018 76 77 78 `````` (* Total WP only permits reductions without observations *) Definition reducible_no_obs (e : expr Λ) (σ : state Λ) := ∃ e' σ' efs, prim_step e σ None e' σ' efs. `````` 79 `````` Definition irreducible (e : expr Λ) (σ : state Λ) := `````` 80 `````` ∀ κ e' σ' efs, ¬prim_step e σ κ e' σ' efs. `````` David Swasey committed Nov 26, 2017 81 82 `````` Definition stuck (e : expr Λ) (σ : state Λ) := to_val e = None ∧ irreducible e σ. `````` Robbert Krebbers committed Mar 15, 2017 83 `````` `````` Ralf Jung committed Dec 07, 2017 84 `````` (* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open `````` Ralf Jung committed Dec 05, 2017 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 `````` David Swasey committed Nov 09, 2017 89 `````` [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v). `````` Robbert Krebbers committed Mar 15, 2017 90 `````` `````` Ralf Jung committed Dec 07, 2017 91 `````` [Atomic StronglyAtomic]: To open invariants with a WP that does not ensure `````` Ralf Jung committed Dec 05, 2017 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 committed Dec 07, 2017 98 `````` if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e'). `````` Ralf Jung committed Oct 29, 2017 99 `````` `````` 100 `````` Inductive step (ρ1 : cfg Λ) (κ : option (observation Λ)) (ρ2 : cfg Λ) : Prop := `````` Robbert Krebbers committed Aug 08, 2016 101 `````` | step_atomic e1 σ1 e2 σ2 efs t1 t2 : `````` Robbert Krebbers committed Feb 01, 2016 102 `````` ρ1 = (t1 ++ e1 :: t2, σ1) → `````` Robbert Krebbers committed Aug 08, 2016 103 `````` ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) → `````` 104 105 106 `````` prim_step e1 σ1 κ e2 σ2 efs → step ρ1 κ ρ2. `````` Marianna Rapoport committed Oct 05, 2018 107 108 109 110 111 `````` (* 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 := `````` 112 113 114 115 116 `````` | nsteps_refl ρ : nsteps 0 ρ [] ρ | nsteps_l n ρ1 ρ2 ρ3 κ κs : step ρ1 κ ρ2 → nsteps n ρ2 κs ρ3 → `````` Marianna Rapoport committed Oct 05, 2018 117 `````` nsteps (S n) ρ1 (cons_obs κ κs) ρ3. `````` 118 119 120 121 122 123 `````` Definition erased_step (ρ1 ρ2 : cfg Λ) := exists κ, step ρ1 κ ρ2. Hint Constructors step nsteps. Lemma erased_steps_nsteps ρ1 ρ2 : `````` Marianna Rapoport committed Oct 05, 2018 124 `````` rtc erased_step ρ1 ρ2 → `````` 125 126 127 128 `````` ∃ n κs, nsteps n ρ1 κs ρ2. Proof. induction 1; firstorder; eauto. Qed. `````` Robbert Krebbers committed Feb 01, 2016 129 `````` `````` Robbert Krebbers committed Apr 19, 2016 130 131 `````` Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v. Proof. intros <-. by rewrite to_of_val. Qed. `````` Robbert Krebbers committed Mar 15, 2017 132 133 134 `````` Lemma not_reducible e σ : ¬reducible e σ ↔ irreducible e σ. Proof. unfold reducible, irreducible. naive_solver. Qed. `````` Robbert Krebbers committed Jan 19, 2016 135 `````` Lemma reducible_not_val e σ : reducible e σ → to_val e = None. `````` 136 `````` Proof. intros (?&?&?&?&?); eauto using val_stuck. Qed. `````` Ralf Jung committed Oct 05, 2018 137 138 `````` Lemma reducible_no_obs_reducible e σ : reducible_no_obs e σ → reducible e σ. Proof. intros (?&?&?&?); eexists; eauto. Qed. `````` David Swasey committed Nov 08, 2017 139 `````` Lemma val_irreducible e σ : is_Some (to_val e) → irreducible e σ. `````` 140 `````` Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed. `````` Robbert Krebbers committed Aug 08, 2016 141 `````` Global Instance of_val_inj : Inj (=) (=) (@of_val Λ). `````` Robbert Krebbers committed Feb 11, 2016 142 `````` Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. `````` Ralf Jung committed Jan 05, 2016 143 `````` `````` Ralf Jung committed Dec 07, 2017 144 145 146 `````` Lemma strongly_atomic_atomic e a : Atomic StronglyAtomic e → Atomic a e. Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed. `````` Ralf Jung committed Oct 29, 2017 147 `````` `````` Robbert Krebbers committed Mar 15, 2017 148 149 150 `````` Lemma reducible_fill `{LanguageCtx Λ K} e σ : to_val e = None → reducible (K e) σ → reducible e σ. Proof. `````` 151 `````` intros ? (e'&σ'&k&efs&Hstep); unfold reducible. `````` Robbert Krebbers committed Mar 15, 2017 152 153 `````` apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto. Qed. `````` Ralf Jung committed Oct 05, 2018 154 155 156 157 158 159 `````` 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. `````` Robbert Krebbers committed Mar 15, 2017 160 161 162 `````` 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. `````` Robbert Krebbers committed Sep 24, 2017 163 `````` `````` 164 165 `````` 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). `````` Robbert Krebbers committed Sep 24, 2017 166 167 168 169 170 171 172 `````` 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 committed Sep 25, 2017 173 `````` `````` 174 175 176 177 178 179 `````` 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 committed Sep 25, 2017 180 181 `````` Class PureExec (P : Prop) (e1 e2 : expr Λ) := { pure_exec_safe σ : `````` Ralf Jung committed Oct 05, 2018 182 `````` P → reducible_no_obs e1 σ; `````` 183 `````` pure_exec_puredet σ1 κ e2' σ2 efs : `````` Marianna Rapoport committed Oct 05, 2018 184 `````` P → prim_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []; `````` Dan Frumin committed Sep 25, 2017 185 186 `````` }. `````` Robbert Krebbers committed Oct 05, 2017 187 `````` Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) : `````` Dan Frumin committed Sep 25, 2017 188 189 190 `````` (P → PureExec True e1 e2) → PureExec P e1 e2. Proof. intros HPE. split; intros; eapply HPE; eauto. Qed. `````` Dan Frumin committed Sep 25, 2017 191 `````` `````` Ralf Jung committed Nov 24, 2017 192 193 `````` (* We do not make this an instance because it is awfully general. *) Lemma pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ : `````` Ralf Jung committed Nov 24, 2017 194 195 196 197 `````` PureExec φ e1 e2 → PureExec φ (K e1) (K e2). Proof. intros [Hred Hstep]. split. `````` Ralf Jung committed Oct 05, 2018 198 `````` - unfold reducible_no_obs in *. naive_solver eauto using fill_step. `````` 199 200 `````` - intros σ1 κ e2' σ2 efs ? Hpstep. destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|]. `````` Ralf Jung committed Oct 05, 2018 201 `````` + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck. `````` 202 `````` + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto. `````` Ralf Jung committed Nov 24, 2017 203 204 `````` Qed. `````` Dan Frumin committed Sep 25, 2017 205 206 `````` (* This is a family of frequent assumptions for PureExec *) Class IntoVal (e : expr Λ) (v : val Λ) := `````` Ralf Jung committed Jun 18, 2018 207 `````` into_val : of_val v = e. `````` Robbert Krebbers committed Nov 02, 2017 208 `````` `````` Ralf Jung committed Jun 18, 2018 209 `````` Class AsVal (e : expr Λ) := as_val : ∃ v, of_val v = e. `````` Robbert Krebbers committed Nov 02, 2017 210 211 212 213 214 `````` (* 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. `````` Ralf Jung committed Jun 18, 2018 215 `````` rewrite /AsVal /=; eauto. `````` Robbert Krebbers committed Nov 02, 2017 216 `````` Qed. `````` Ralf Jung committed Jun 21, 2018 217 218 219 `````` 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. `````` Robbert Krebbers committed Mar 15, 2017 220 ``End language.``