1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
From mininix Require Export nix.operational_props.
From stdpp Require Import options.
Definition wp (μ : mode) (e : expr) (Φ : expr → Prop) : Prop :=
∃ e', e -{μ}->* e' ∧ final μ e' ∧ Φ e'.
Lemma Lit_wp μ Φ bl :
base_lit_ok bl →
Φ (ELit bl) →
wp μ (ELit bl) Φ.
Proof. exists (ELit bl). by repeat constructor. Qed.
Lemma Abs_wp μ Φ x e :
Φ (EAbs x e) →
wp μ (EAbs x e) Φ.
Proof. exists (EAbs x e). by repeat constructor. Qed.
Lemma AbsMatch_wp μ Φ ms strict e :
Φ (EAbsMatch ms strict e) →
wp μ (EAbsMatch ms strict e) Φ.
Proof. exists (EAbsMatch ms strict e). by repeat constructor. Qed.
Lemma LetAttr_no_recs_wp μ Φ k αs e :
no_recs αs →
wp μ (subst ((k,.) ∘ attr_expr <$> αs) e) Φ →
wp μ (ELetAttr k (EAttr αs) e) Φ.
Proof.
intros Hαs (e' & Hsteps & ? & HΦ). exists e'. split; [|done].
etrans; [|apply Hsteps]. apply rtc_once. by constructor.
Qed.
Lemma BinOp_wp μ Φ op e1 e2 :
wp SHALLOW e1 (λ e1', ∃ Φop,
sem_bin_op op e1' Φop ∧
wp SHALLOW e2 (λ e2', ∃ e', Φop e2' e' ∧ wp μ e' Φ)) →
wp μ (EBinOp op e1 e2) Φ.
Proof.
intros (e1' & Hsteps1 & ? & Φop & Hop1 & e2' & Hsteps2 & ?
& e' & Hop2 & e'' & Hsteps & ? & HΦ).
exists e''. split; [|done].
etrans; [by apply SBinOpL_rtc|].
etrans; [by eapply SBinOpR_rtc|].
eapply rtc_l; [by econstructor|]. done.
Qed.
Lemma Id_wp μ Φ x k e :
wp μ e Φ →
wp μ (EId x (Some (k,e))) Φ.
Proof.
intros (e' & Hsteps & ? & HΦ). exists e'. split; [|done].
etrans; [|apply Hsteps]. apply rtc_once. constructor.
Qed.
Lemma App_wp μ Φ e1 e2 :
wp SHALLOW e1 (λ e1', wp μ (EApp e1' e2) Φ) ↔
wp μ (EApp e1 e2) Φ.
Proof.
split.
- intros (e1' & Hsteps1 & ? & e' & Hsteps2 & ? & HΦ).
exists e'; split; [|done]. etrans; [|apply Hsteps2].
by apply SAppL_rtc.
- intros (e' & Hsteps & Hfinal & HΦ).
cut (∃ e1', e1 -{SHALLOW}->* e1' ∧ final SHALLOW e1' ∧ EApp e1' e2 -{μ}->* e').
{ intros (e1'&?&?&?). exists e1'. split_and!; [done..|]. by exists e'. }
clear Φ HΦ. apply rtc_nsteps in Hsteps as [n Hsteps].
revert e1 Hsteps. induction n as [|n IH]; intros e1 Hsteps.
{ inv Hsteps. inv Hfinal. }
inv Hsteps. inv H0.
+ eexists; split_and!; [done|by constructor|].
eapply rtc_l; [by constructor|by eapply rtc_nsteps_2].
+ eexists; split_and!; [done|by constructor|].
eapply rtc_l; [by constructor|by eapply rtc_nsteps_2].
+ eexists; split_and!; [done|by constructor|].
eapply rtc_l; [by constructor|by eapply rtc_nsteps_2].
+ inv H2.
* apply IH in H1 as (e'' & Hsteps & ? & ?).
exists e''; split; [|done]. by eapply rtc_l.
* eexists; split_and!; [done|by constructor|].
eapply rtc_l; [by eapply SAppR|]. by eapply rtc_nsteps_2.
Qed.
Lemma Attr_wp_shallow Φ αs :
Φ (EAttr (AttrN ∘ from_attr (subst (indirects αs)) id <$> αs)) →
wp SHALLOW (EAttr αs) Φ.
Proof.
eexists (EAttr (AttrN ∘ _ <$> αs)); split_and!; [ |by constructor|done].
destruct (decide (no_recs αs)); [|apply rtc_once; by constructor].
apply reflexive_eq; f_equal. apply map_eq=> x. rewrite lookup_fmap.
destruct (αs !! x) as [[? e]|] eqn:?; f_equal/=.
by assert (τ = NONREC) as -> by eauto using no_recs_lookup.
Qed.
Lemma β_wp μ Φ x e1 e2 :
wp μ (subst {[x:=(ABS, e2)]} e1) Φ →
wp μ (EApp (EAbs x e1) e2) Φ.
Proof.
intros (e' & Hsteps & ? & ?). exists e'. split; [|done].
eapply rtc_l; [|done]. by constructor.
Qed.
Lemma βMatch_wp μ Φ ms strict e1 αs βs :
no_recs αs →
matches (attr_expr <$> αs) ms strict βs →
wp μ (subst (indirects βs) e1) Φ →
wp μ (EApp (EAbsMatch ms strict e1) (EAttr αs)) Φ.
Proof.
intros ?? (e' & Hsteps & ? & ?). exists e'. split; [|done].
eapply rtc_l; [|done]. by constructor.
Qed.
Lemma Functor_wp μ Φ αs e1 e2 :
no_recs αs →
αs !! "__functor" = Some (AttrN e1) →
wp μ (EApp (EApp e1 (EAttr αs)) e2) Φ →
wp μ (EApp (EAttr αs) e2) Φ.
Proof.
intros ?? (e' & Hsteps & ? & ?). exists e'. split; [|done].
eapply rtc_l; [|done]. by constructor.
Qed.
Lemma If_wp μ Φ e1 e2 e3 :
wp SHALLOW e1 (λ e1', ∃ b : bool,
e1' = ELit (LitBool b) ∧ wp μ (if b then e2 else e3) Φ) →
wp μ (EIf e1 e2 e3) Φ.
Proof.
intros (e1' & Hsteps & ? & b & -> & e' & Hsteps' & ? & HΦ).
exists e'; split; [|done]. etrans; [by apply SIf_rtc|].
eapply rtc_l; [|done]. destruct b; constructor.
Qed.
Lemma wp_mono μ e Φ Ψ :
wp μ e Φ →
(∀ e', Φ e' → Ψ e') →
wp μ e Ψ.
Proof. intros (e' & ? & ? & ?) ?. exists e'. naive_solver. Qed.
Lemma union_kinded_abs {A} mkv (v2 : A) :
union_kinded (pair WITH <$> mkv) (Some (ABS, v2)) = Some (ABS, v2).
Proof. by destruct mkv. Qed.
Lemma union_kinded_with {A} (v : A) mkv2 :
union_kinded (Some (WITH, v)) (pair WITH <$> mkv2) = Some (WITH, v).
Proof. by destruct mkv2. Qed.
|
