Commit 6cb1f87f by Ralf Jung

### Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 3cffb277 ffa92c50
 ... @@ -21,7 +21,7 @@ Infix "⩪" := minus (at level 40) : C_scope. ... @@ -21,7 +21,7 @@ Infix "⩪" := minus (at level 40) : C_scope. Class ValidN (A : Type) := validN : nat → A → Prop. Class ValidN (A : Type) := validN : nat → A → Prop. Instance: Params (@validN) 3. Instance: Params (@validN) 3. Notation "✓{ n } x" := (validN n x) Notation "✓{ n } x" := (validN n x) (at level 20, n at level 1, format "✓{ n } x"). (at level 20, n at next level, format "✓{ n } x"). Class Valid (A : Type) := valid : A → Prop. Class Valid (A : Type) := valid : A → Prop. Instance: Params (@valid) 2. Instance: Params (@valid) 2. ... @@ -30,7 +30,7 @@ Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x. ... @@ -30,7 +30,7 @@ Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x. Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z. Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z. Notation "x ≼{ n } y" := (includedN n x y) Notation "x ≼{ n } y" := (includedN n x y) (at level 70, format "x ≼{ n } y") : C_scope. (at level 70, n at next level, format "x ≼{ n } y") : C_scope. Instance: Params (@includedN) 4. Instance: Params (@includedN) 4. Hint Extern 0 (_ ≼{_} _) => reflexivity. Hint Extern 0 (_ ≼{_} _) => reflexivity. ... @@ -476,7 +476,7 @@ Section discrete. ... @@ -476,7 +476,7 @@ Section discrete. Qed. Qed. Definition discrete_extend_mixin : CMRAExtendMixin A. Definition discrete_extend_mixin : CMRAExtendMixin A. Proof. Proof. intros n x y1 y2 ??; exists (y1,y2); split_ands; auto. intros n x y1 y2 ??; exists (y1,y2); split_and?; auto. apply (timeless _), dist_le with n; auto with lia. apply (timeless _), dist_le with n; auto with lia. Qed. Qed. Definition discreteRA : cmraT := Definition discreteRA : cmraT := ... ...
 ... @@ -104,13 +104,13 @@ Definition validity_ra : RA (discreteC T). ... @@ -104,13 +104,13 @@ Definition validity_ra : RA (discreteC T). Proof. Proof. split. split. - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq]. - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq]. split; intros (?&?&?); split_ands'; split; intros (?&?&?); split_and!; first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto]. first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto]. - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq. - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq. - intros ?? [??]; naive_solver. - intros ?? [??]; naive_solver. - intros x1 x2 [? Hx] y1 y2 [? Hy]; - intros x1 x2 [? Hx] y1 y2 [? Hy]; split; simpl; [|by intros (?&?&?); rewrite Hx // Hy]. split; simpl; [|by intros (?&?&?); rewrite Hx // Hy]. split; intros (?&?&z&?&?); split_ands'; try tauto. split; intros (?&?&z&?&?); split_and!; try tauto. + exists z. by rewrite -Hy // -Hx. + exists z. by rewrite -Hy // -Hx. + exists z. by rewrite Hx ?Hy; tauto. + exists z. by rewrite Hx ?Hy; tauto. - intros [x px ?] [y py ?] [z pz ?]; split; simpl; - intros [x px ?] [y py ?] [z pz ?]; split; simpl; ... @@ -135,7 +135,7 @@ Lemma validity_update (x y : validityRA) : ... @@ -135,7 +135,7 @@ Lemma validity_update (x y : validityRA) : (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y. (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y. Proof. Proof. intros Hxy. apply discrete_update. intros Hxy. apply discrete_update. intros z (?&?&?); split_ands'; try eapply Hxy; eauto. intros z (?&?&?); split_and!; try eapply Hxy; eauto. Qed. Qed. Lemma to_validity_valid (x : A) : Lemma to_validity_valid (x : A) : ... ...
 ... @@ -156,7 +156,7 @@ Section iprod_cmra. ... @@ -156,7 +156,7 @@ Section iprod_cmra. intros n f f1 f2 Hf Hf12. intros n f f1 f2 Hf Hf12. set (g x := cmra_extend_op n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)). set (g x := cmra_extend_op n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)). exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)). exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)). split_ands; intros x; apply (proj2_sig (g x)). split_and?; intros x; apply (proj2_sig (g x)). Qed. Qed. Canonical Structure iprodRA : cmraT := Canonical Structure iprodRA : cmraT := CMRAT iprod_cofe_mixin iprod_cmra_mixin iprod_cmra_extend_mixin. CMRAT iprod_cofe_mixin iprod_cmra_mixin iprod_cmra_extend_mixin. ... ...
 ... @@ -75,7 +75,7 @@ Proof. ... @@ -75,7 +75,7 @@ Proof. - intros [mz Hmz]. - intros [mz Hmz]. destruct mx as [x|]; [right|by left]. destruct mx as [x|]; [right|by left]. destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz]. destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz]. destruct mz as [z|]; inversion_clear Hmz; split_ands; auto; destruct mz as [z|]; inversion_clear Hmz; split_and?; auto; cofe_subst; eauto using cmra_includedN_l. cofe_subst; eauto using cmra_includedN_l. - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor). - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor). by exists (Some z); constructor. by exists (Some z); constructor. ... ...
 ... @@ -101,7 +101,7 @@ Lemma step_closed s1 s2 T1 T2 S Tf : ... @@ -101,7 +101,7 @@ Lemma step_closed s1 s2 T1 T2 S Tf : step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ∩ Tf ≡ ∅ → step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ∩ Tf ≡ ∅ → s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅. s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅. Proof. Proof. inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto. inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_and?; auto. - eapply Hstep with s1, Frame_step with T1 T2; auto with sts. - eapply Hstep with s1, Frame_step with T1 T2; auto with sts. - set_solver -Hstep Hs1 Hs2. - set_solver -Hstep Hs1 Hs2. Qed. Qed. ... @@ -240,7 +240,7 @@ Proof. ... @@ -240,7 +240,7 @@ Proof. + rewrite (up_closed (up _ _)); auto using closed_up with sts. + rewrite (up_closed (up _ _)); auto using closed_up with sts. + rewrite (up_closed (up_set _ _)); + rewrite (up_closed (up_set _ _)); eauto using closed_up_set, closed_ne with sts. eauto using closed_up_set, closed_ne with sts. - intros x y ?? (z&Hy&?&Hxz); exists (unit (x ⋅ y)); split_ands. - intros x y ?? (z&Hy&?&Hxz); exists (unit (x ⋅ y)); split_and?. + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; set_solver. + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; set_solver. + destruct Hxz; inversion_clear Hy; simpl; + destruct Hxz; inversion_clear Hy; simpl; auto using closed_up_set_empty, closed_up_empty with sts. auto using closed_up_set_empty, closed_up_empty with sts. ... @@ -326,7 +326,7 @@ Lemma sts_op_auth_frag s S T : ... @@ -326,7 +326,7 @@ Lemma sts_op_auth_frag s S T : Proof. Proof. intros; split; [split|constructor; set_solver]; simpl. intros; split; [split|constructor; set_solver]; simpl. - intros (?&?&?); by apply closed_disjoint' with S. - intros (?&?&?); by apply closed_disjoint' with S. - intros; split_ands. set_solver+. done. constructor; set_solver. - intros; split_and?. set_solver+. done. constructor; set_solver. Qed. Qed. Lemma sts_op_auth_frag_up s T : Lemma sts_op_auth_frag_up s T : tok s ∩ T ≡ ∅ → sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T. tok s ∩ T ≡ ∅ → sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T. ... @@ -381,7 +381,7 @@ when we have RAs back *) ... @@ -381,7 +381,7 @@ when we have RAs back *) move:(EQ' Hcl2)=>{EQ'} EQ. inversion_clear EQ as [|? ? ? ? HT HS]. move:(EQ' Hcl2)=>{EQ'} EQ. inversion_clear EQ as [|? ? ? ? HT HS]. destruct Hv as [Hv _]. move:(Hv Hcl2)=>{Hv} [/= Hcl1 [Hclf Hdisj]]. destruct Hv as [Hv _]. move:(Hv Hcl2)=>{Hv} [/= Hcl1 [Hclf Hdisj]]. apply Hvf in Hclf. simpl in Hclf. clear Hvf. apply Hvf in Hclf. simpl in Hclf. clear Hvf. inversion_clear Hdisj. split; last (exists Tf; split_ands); [done..|]. inversion_clear Hdisj. split; last (exists Tf; split_and?); [done..|]. apply (anti_symm (⊆)). apply (anti_symm (⊆)). + move=>s HS2. apply elem_of_intersection. split; first by apply HS. + move=>s HS2. apply elem_of_intersection. split; first by apply HS. by apply subseteq_up_set. by apply subseteq_up_set. ... @@ -392,7 +392,7 @@ when we have RAs back *) ... @@ -392,7 +392,7 @@ when we have RAs back *) - intros (Hcl1 & Tf & Htk & Hf & Hs). - intros (Hcl1 & Tf & Htk & Hf & Hs). exists (sts_frag (up_set S2 Tf) Tf). exists (sts_frag (up_set S2 Tf) Tf). split; first split; simpl;[|done|]. split; first split; simpl;[|done|]. + intros _. split_ands; first done. + intros _. split_and?; first done. * apply closed_up_set; last by eapply closed_ne. * apply closed_up_set; last by eapply closed_ne. move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2). move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2). set_solver +Htk. set_solver +Htk. ... @@ -404,7 +404,7 @@ Lemma sts_frag_included' S1 S2 T : ... @@ -404,7 +404,7 @@ Lemma sts_frag_included' S1 S2 T : closed S2 T → closed S1 T → S2 ≡ S1 ∩ up_set S2 ∅ → closed S2 T → closed S1 T → S2 ≡ S1 ∩ up_set S2 ∅ → sts_frag S1 T ≼ sts_frag S2 T. sts_frag S1 T ≼ sts_frag S2 T. Proof. Proof. intros. apply sts_frag_included; split_ands; auto. intros. apply sts_frag_included; split_and?; auto. exists ∅; split_ands; done || set_solver+. exists ∅; split_and?; done || set_solver+. Qed. Qed. End stsRA. End stsRA.
 ... @@ -143,7 +143,7 @@ Next Obligation. ... @@ -143,7 +143,7 @@ Next Obligation. assert (∃ x2', y ≡{n2}≡ x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?). assert (∃ x2', y ≡{n2}≡ x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?). { destruct Hxy as [z Hy]; exists (x2 ⋅ z); split; eauto using cmra_included_l. { destruct Hxy as [z Hy]; exists (x2 ⋅ z); split; eauto using cmra_included_l. apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. } apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. } clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |]. clear Hxy; cofe_subst y; exists x1, x2'; split_and?; [done| |]. - apply uPred_weaken with n1 x1; eauto using cmra_validN_op_l. - apply uPred_weaken with n1 x1; eauto using cmra_validN_op_l. - apply uPred_weaken with n1 x2; eauto using cmra_validN_op_r. - apply uPred_weaken with n1 x2; eauto using cmra_validN_op_r. Qed. Qed. ... @@ -273,7 +273,7 @@ Global Instance impl_proper : ... @@ -273,7 +273,7 @@ Global Instance impl_proper : Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M). Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M). Proof. Proof. intros P P' HP Q Q' HQ n' x ??; split; intros (x1&x2&?&?&?); cofe_subst x; intros P P' HP Q Q' HQ n' x ??; split; intros (x1&x2&?&?&?); cofe_subst x; exists x1, x2; split_ands; try (apply HP || apply HQ); exists x1, x2; split_and?; try (apply HP || apply HQ); eauto using cmra_validN_op_l, cmra_validN_op_r. eauto using cmra_validN_op_l, cmra_validN_op_r. Qed. Qed. Global Instance sep_proper : Global Instance sep_proper : ... @@ -319,12 +319,13 @@ Proof. intros P1 P2 HP n' x; split; apply HP; eauto using cmra_unit_validN. Qed. ... @@ -319,12 +319,13 @@ Proof. intros P1 P2 HP n' x; split; apply HP; eauto using cmra_unit_validN. Qed. Global Instance always_proper : Global Instance always_proper : Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _. Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _. Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M). Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M). Proof. Proof. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed. by intros a1 a2 Ha n' x; split; intros [a' ?]; exists a'; simpl; first Global Instance ownM_proper: Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _. [rewrite -(dist_le _ _ _ _ Ha); last lia Global Instance valid_ne {A : cmraT} n : |rewrite (dist_le _ _ _ _ Ha); last lia]. Proper (dist n ==> dist n) (@uPred_valid M A). Qed. Proof. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed. Global Instance ownM_proper : Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _. Global Instance valid_proper {A : cmraT} : Proper ((≡) ==> (≡)) (@uPred_valid M A) := ne_proper _. Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M). Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M). Proof. unfold uPred_iff; solve_proper. Qed. Proof. unfold uPred_iff; solve_proper. Qed. Global Instance iff_proper : Global Instance iff_proper : ... @@ -563,17 +564,17 @@ Qed. ... @@ -563,17 +564,17 @@ Qed. Global Instance sep_assoc : Assoc (≡) (@uPred_sep M). Global Instance sep_assoc : Assoc (≡) (@uPred_sep M). Proof. Proof. intros P Q R n x ?; split. intros P Q R n x ?; split. - intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 ⋅ y1), y2; split_ands; auto. - intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 ⋅ y1), y2; split_and?; auto. + by rewrite -(assoc op) -Hy -Hx. + by rewrite -(assoc op) -Hy -Hx. + by exists x1, y1. + by exists x1, y1. - intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 ⋅ x2); split_ands; auto. - intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 ⋅ x2); split_and?; auto. + by rewrite (assoc op) -Hy -Hx. + by rewrite (assoc op) -Hy -Hx. + by exists y2, x2. + by exists y2, x2. Qed. Qed. Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R). Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R). Proof. Proof. intros HPQR n x ?? n' x' ???; apply HPQR; auto. intros HPQR n x ?? n' x' ???; apply HPQR; auto. exists x, x'; split_ands; auto. exists x, x'; split_and?; auto. eapply uPred_weaken with n x; eauto using cmra_validN_op_l. eapply uPred_weaken with n x; eauto using cmra_validN_op_l. Qed. Qed. Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊑ Q. Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊑ Q. ... ...
 ... @@ -146,7 +146,7 @@ Section proof. ... @@ -146,7 +146,7 @@ Section proof. Lemma newchan_spec (P : iProp) (Φ : val → iProp) : Lemma newchan_spec (P : iProp) (Φ : val → iProp) : (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (LocV l)) (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (LocV l)) ⊑ wp ⊤ (newchan '()) Φ. ⊑ || newchan '() {{ Φ }}. Proof. Proof. rewrite /newchan. wp_rec. (* TODO: wp_seq. *) rewrite /newchan. wp_rec. (* TODO: wp_seq. *) rewrite -wp_pvs. wp> eapply wp_alloc; eauto with I ndisj. rewrite -wp_pvs. wp> eapply wp_alloc; eauto with I ndisj. ... @@ -196,7 +196,7 @@ Section proof. ... @@ -196,7 +196,7 @@ Section proof. Qed. Qed. Lemma signal_spec l P (Φ : val → iProp) : Lemma signal_spec l P (Φ : val → iProp) : heapN ⊥ N → (send l P ★ P ★ Φ '()) ⊑ wp ⊤ (signal (LocV l)) Φ. heapN ⊥ N → (send l P ★ P ★ Φ '()) ⊑ || signal (LocV l) {{ Φ }}. Proof. Proof. intros Hdisj. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r. intros Hdisj. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r. apply exist_elim=>γ. wp_rec. (* FIXME wp_let *) apply exist_elim=>γ. wp_rec. (* FIXME wp_let *) ... @@ -226,12 +226,12 @@ Section proof. ... @@ -226,12 +226,12 @@ Section proof. Qed. Qed. Lemma wait_spec l P (Φ : val → iProp) : Lemma wait_spec l P (Φ : val → iProp) : heapN ⊥ N → (recv l P ★ (P -★ Φ '())) ⊑ wp ⊤ (wait (LocV l)) Φ. heapN ⊥ N → (recv l P ★ (P -★ Φ '())) ⊑ || wait (LocV l) {{ Φ }}. Proof. Proof. Abort. Abort. Lemma split_spec l P1 P2 Φ : Lemma split_spec l P1 P2 Φ : (recv l (P1 ★ P2) ★ (recv l P1 ★ recv l P2 -★ Φ '())) ⊑ wp ⊤ Skip Φ. (recv l (P1 ★ P2) ★ (recv l P1 ★ recv l P2 -★ Φ '())) ⊑ || Skip {{ Φ }}. Proof. Proof. Abort. Abort. ... @@ -260,14 +260,14 @@ Section spec. ... @@ -260,14 +260,14 @@ Section spec. Lemma barrier_spec (heapN N : namespace) : Lemma barrier_spec (heapN N : namespace) : heapN ⊥ N → heapN ⊥ N → ∃ (recv send : loc -> iProp -n> iProp), ∃ (recv send : loc -> iProp -n> iProp), (∀ P, heap_ctx heapN ⊑ ({{ True }} newchan '() @ ⊤ {{ λ v, ∃ l, v = LocV l ★ recv l P ★ send l P }})) ∧ (∀ P, heap_ctx heapN ⊑ ({{ True }} newchan '() {{ λ v, ∃ l, v = LocV l ★ recv l P ★ send l P }})) ∧ (∀ l P, {{ send l P ★ P }} signal (LocV l) @ ⊤ {{ λ _, True }}) ∧ (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ λ _, True }}) ∧ (∀ l P, {{ recv l P }} wait (LocV l) @ ⊤ {{ λ _, P }}) ∧ (∀ l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) ∧ (∀ l P Q, {{ recv l (P ★ Q) }} Skip @ ⊤ {{ λ _, recv l P ★ recv l Q }}) ∧ (∀ l P Q, {{ recv l (P ★ Q) }} Skip {{ λ _, recv l P ★ recv l Q }}) ∧ (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)). (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)). Proof. Proof. intros HN. exists (λ l, CofeMor (recv N heapN l)). exists (λ l, CofeMor (send N heapN l)). intros HN. exists (λ l, CofeMor (recv N heapN l)). exists (λ l, CofeMor (send N heapN l)). split_ands; cbn. split_and?; cbn. - intros. apply: always_intro. apply impl_intro_l. rewrite -newchan_spec. - intros. apply: always_intro. apply impl_intro_l. rewrite -newchan_spec. rewrite comm always_and_sep_r. apply sep_mono_r. apply forall_intro=>l. rewrite comm always_and_sep_r. apply sep_mono_r. apply forall_intro=>l. apply wand_intro_l. rewrite right_id -(exist_intro l) const_equiv // left_id. apply wand_intro_l. rewrite right_id -(exist_intro l) const_equiv // left_id. ... ...
 ... @@ -17,44 +17,47 @@ Implicit Types Φ : val → iProp heap_lang Σ. ... @@ -17,44 +17,47 @@ Implicit Types Φ : val → iProp heap_lang Σ. (** Proof rules for the sugar *) (** Proof rules for the sugar *) Lemma wp_lam' E x ef e v Φ : Lemma wp_lam' E x ef e v Φ : to_val e = Some v → ▷ wp E (subst ef x v) Φ ⊑ wp E (App (Lam x ef) e) Φ. to_val e = Some v → ▷ || subst ef x v @ E {{ Φ }} ⊑ || App (Lam x ef) e @ E {{ Φ }}. Proof. intros. by rewrite -wp_rec' ?subst_empty. Qed. Proof. intros. by rewrite -wp_rec' ?subst_empty. Qed. Lemma wp_let' E x e1 e2 v Φ : Lemma wp_let' E x e1 e2 v Φ : to_val e1 = Some v → ▷ wp E (subst e2 x v) Φ ⊑ wp E (Let x e1 e2) Φ. to_val e1 = Some v → ▷ || subst e2 x v @ E {{ Φ }} ⊑ || Let x e1 e2 @ E {{ Φ }}. Proof. apply wp_lam'. Qed. Proof. apply wp_lam'. Qed. Lemma wp_seq E e1 e2 Φ : wp E e1 (λ _, ▷ wp E e2 Φ) ⊑ wp E (Seq e1 e2) Φ. Lemma wp_seq E e1 e2 Φ : || e1 @ E {{ λ _, ▷ || e2 @ E {{ Φ }} }} ⊑ || Seq e1 e2 @ E {{ Φ }}. Proof. Proof. rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v. rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v. by rewrite -wp_let' //= ?to_of_val ?subst_empty. by rewrite -wp_let' //= ?to_of_val ?subst_empty. Qed. Qed. Lemma wp_skip E Φ : ▷ (Φ (LitV LitUnit)) ⊑ wp E Skip Φ. Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊑ || Skip @ E {{ Φ }}. Proof. rewrite -wp_seq -wp_value // -wp_value //. Qed. Proof. rewrite -wp_seq -wp_value // -wp_value //. Qed. Lemma wp_le E (n1 n2 : Z) P Φ : Lemma wp_le E (n1 n2 : Z) P Φ : (n1 ≤ n2 → P ⊑ ▷ Φ (LitV \$ LitBool true)) → (n1 ≤ n2 → P ⊑ ▷ Φ (LitV (LitBool true))) → (n2 < n1 → P ⊑ ▷ Φ (LitV \$ LitBool false)) → (n2 < n1 → P ⊑ ▷ Φ (LitV (LitBool false))) → P ⊑ wp E (BinOp LeOp (Lit \$ LitInt n1) (Lit \$ LitInt n2)) Φ. P ⊑ || BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. Proof. Proof. intros. rewrite -wp_bin_op //; []. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega. destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega. Qed. Qed. Lemma wp_lt E (n1 n2 : Z) P Φ : Lemma wp_lt E (n1 n2 : Z) P Φ : (n1 < n2 → P ⊑ ▷ Φ (LitV \$ LitBool true)) → (n1 < n2 → P ⊑ ▷ Φ (LitV (LitBool true))) → (n2 ≤ n1 → P ⊑ ▷ Φ (LitV \$ LitBool false)) → (n2 ≤ n1 → P ⊑ ▷ Φ (LitV (LitBool false))) → P ⊑ wp E (BinOp LtOp (Lit \$ LitInt n1) (Lit \$ LitInt n2)) Φ. P ⊑ || BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. Proof. Proof. intros. rewrite -wp_bin_op //; []. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 < n2)); by eauto with omega. destruct (bool_decide_reflect (n1 < n2)); by eauto with omega. Qed. Qed. Lemma wp_eq E (n1 n2 : Z) P Φ : Lemma wp_eq E (n1 n2 : Z) P Φ : (n1 = n2 → P ⊑ ▷ Φ (LitV \$ LitBool true)) → (n1 = n2 → P ⊑ ▷ Φ (LitV (LitBool true))) → (n1 ≠ n2 → P ⊑ ▷ Φ (LitV \$ LitBool false)) → (n1 ≠ n2 → P ⊑ ▷ Φ (LitV (LitBool false))) → P ⊑ wp E (BinOp EqOp (Lit \$ LitInt n1) (Lit \$ LitInt n2)) Φ. P ⊑ || BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. Proof. Proof. intros. rewrite -wp_bin_op //; []. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 = n2)); by eauto with omega. destruct (bool_decide_reflect (n1 = n2)); by eauto with omega. ... ...
 ... @@ -65,7 +65,7 @@ Section heap. ... @@ -65,7 +65,7 @@ Section heap. (** Allocation *) (** Allocation *) Lemma heap_alloc E N σ : Lemma heap_alloc E N σ : authG heap_lang Σ heapRA → nclose N ⊆ E → authG heap_lang Σ heapRA → nclose N ⊆ E → ownP σ ⊑ pvs E E (∃ (_ : heapG Σ), heap_ctx N ∧ Π★{map σ} heap_mapsto). ownP σ ⊑ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} heap_mapsto). Proof. Proof. intros. rewrite -{1}(from_to_heap σ). etransitivity. intros. rewrite -{1}(from_to_heap σ). etransitivity. { rewrite [ownP _]later_intro. { rewrite [ownP _]later_intro. ... @@ -100,10 +100,10 @@ Section heap. ... @@ -100,10 +100,10 @@ Section heap. to_val e = Some v → nclose N ⊆ E → to_val e = Some v → nclose N ⊆ E → P ⊑ heap_ctx N → P ⊑ heap_ctx N → P ⊑ (▷ ∀ l, l ↦ v -★ Φ (LocV l)) → P ⊑ (▷ ∀ l, l ↦ v -★ Φ (LocV l)) → P ⊑ wp E (Alloc e) Φ. P ⊑ || Alloc e @ E {{ Φ }}. Proof. Proof. rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP. rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP. transitivity (pvs E E (auth_own heap_name ∅ ★ P))%I. transitivity (|={E}=> auth_own heap_name ∅ ★ P)%I. { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. } { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. } apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e))) apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e))) with N heap_name ∅; simpl; eauto with I. with N heap_name ∅; simpl; eauto with I. ... @@ -127,7 +127,7 @@ Section heap. ... @@ -127,7 +127,7 @@ Section heap. nclose N ⊆ E → nclose N ⊆ E → P ⊑ heap_ctx N → P ⊑ heap_ctx N → P ⊑ (▷ l ↦ v ★ ▷ (l ↦ v -★ Φ v)) → P ⊑ (▷ l ↦ v ★ ▷ (l ↦ v -★ Φ v)) → P ⊑ wp E (Load (Loc l)) Φ. P ⊑ || Load (Loc l) @ E {{ Φ }}. Proof. Proof. rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPΦ. rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPΦ. apply (auth_fsa' heap_inv (wp_fsa _) id) apply (auth_fsa' heap_inv (wp_fsa _) id) ... @@ -146,7 +146,7 @@ Section heap. ... @@ -146,7 +146,7 @@ Section heap. to_val e = Some v → nclose N ⊆ E → to_val e = Some v → nclose N ⊆ E → P ⊑ heap_ctx N → P ⊑ heap_ctx N → P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))) → P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))) → P ⊑ wp E (Store (Loc l) e) Φ. P ⊑ || Store (Loc l) e @ E {{ Φ }}. Proof. Proof. rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPΦ. rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPΦ. apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l)) apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l)) ... @@ -167,7 +167,7 @@ Section heap. ... @@ -167,7 +167,7 @@ Section heap. nclose N ⊆ E → nclose N ⊆ E → P ⊑ heap_ctx N → P ⊑ heap_ctx N → P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v' -★ Φ (LitV (LitBool false)))) → P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v' -★ Φ (LitV (LitBool false)))) → P ⊑ wp E (Cas (Loc l) e1 e2) Φ. P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}. Proof. Proof. rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPΦ. rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPΦ. apply (auth_fsa' heap_inv (wp_fsa _) id) apply (auth_fsa' heap_inv (wp_fsa _) id) ... @@ -187,7 +187,7 @@ Section heap. ... @@ -187,7 +187,7 @@ Section heap. nclose N ⊆ E → nclose N ⊆ E → P ⊑ heap_ctx N → P ⊑ heap_ctx N → P ⊑ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))) → P ⊑ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))) → P ⊑ wp E (Cas (Loc l) e1 e2) Φ. P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}. Proof. Proof. rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPΦ. rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPΦ. apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l)) apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l)) ... ...
 ... @@ -16,18 +16,14 @@ Implicit Types ef : option expr. ... @@ -16,18 +16,14 @@ Implicit Types ef : option expr. (** Bind. *) (** Bind. *) Lemma wp_bind {E e} K Φ : Lemma wp_bind {E e} K Φ : wp E e (λ v, wp E (fill K (of_val v)) Φ) ⊑ wp E (fill K e) Φ. || e @ E {{ λ v, || fill K (of_val v) @ E {{ Φ }}}} ⊑ || fill K e @ E {{ Φ }}. Proof. apply weakestpre.wp_bind. Qed. Lemma wp_bindi {E e} Ki Φ : wp E e (λ v, wp E (fill_item Ki (of_val v)) Φ) ⊑ wp E (fill_item Ki e) Φ. Proof. apply weakestpre.wp_bind. Qed. Proof. apply weakestpre.wp_bind. Qed. (** Base axioms for core primitives of the language: Stateful reductions. *) (** Base axioms for core primitives of the language: Stateful reductions. *) Lemma wp_alloc_pst E σ e v Φ : Lemma wp_alloc_pst E σ e v Φ : to_val e = Some v → to_val e = Some v → (ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l))) (ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l))) ⊑ wp E (Alloc e) Φ. ⊑ || Alloc e @ E {{ Φ }}. Proof. Proof.