Commit 0a74ba89 by Robbert Krebbers

### Use notation # instead of ' for literals to avoid conflicts.

parent d4aba8ef
 From heap_lang Require Export substitution notation. Definition newbarrier : val := λ: "", ref '0. Definition signal : val := λ: "x", "x" <- '1. Definition newbarrier : val := λ: "", ref #0. Definition signal : val := λ: "x", "x" <- #1. Definition wait : val := rec: "wait" "x" := if: !"x" = '1 then '() else "wait" "x". rec: "wait" "x" := if: !"x" = #1 then #() else "wait" "x". Instance newbarrier_closed : Closed newbarrier. Proof. solve_closed. Qed. Instance signal_closed : Closed signal. Proof. solve_closed. Qed. ... ...
 ... ... @@ -3,20 +3,19 @@ From program_logic Require Import auth sts saved_prop hoare ownership. Import uPred. Definition worker (n : Z) : val := λ: "b" "y", wait "b" ;; !"y" 'n. λ: "b" "y", wait "b" ;; !"y" #n. Definition client : expr := let: "y" := ref '0 in let: "b" := newbarrier '() in let: "y" := ref #0 in let: "b" := newbarrier #() in Fork (Fork (worker 12 "b" "y") ;; worker 17 "b" "y") ;; "y" <- (λ: "z", "z" + '42) ;; signal "b". "y" <- (λ: "z", "z" + #42) ;; signal "b". Section client. Context {Σ : rFunctorG} `{!heapG Σ, !barrierG Σ} (heapN N : namespace). Local Notation iProp := (iPropG heap_lang Σ). Definition y_inv q y : iProp := (∃ f : val, y ↦{q} f ★ □ ∀ n : Z, (* TODO: '() conflicts with '(n + 42)... *) || f 'n {{ λ v, v = LitV (n + 42)%Z }})%I. Definition y_inv q y : iProp := (∃ f : val, y ↦{q} f ★ □ ∀ n : Z, || f #n {{ λ v, v = #(n + 42) }})%I. Lemma y_inv_split q y : y_inv q y ⊑ (y_inv (q/2) y ★ y_inv (q/2) y). ... ... @@ -57,7 +56,7 @@ Section client. wp_seq. (ewp eapply wp_store); eauto with I. strip_later. rewrite assoc [(_ ★ y ↦ _)%I]comm. apply sep_mono_r, wand_intro_l. wp_seq. rewrite -signal_spec right_id assoc sep_elim_l comm. apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", "z" + '42)%L). apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", "z" + #42)%L). apply sep_intro_True_r; first done. apply: always_intro. apply forall_intro=>n. wp_let. wp_op. by apply const_intro. } (* The two spawned threads, the waiters. *) ... ...
 ... ... @@ -32,7 +32,7 @@ Definition ress (I : gset gname) : iProp := (Π★{set I} (λ i, ∃ R, saved_prop_own i (Next R) ★ ▷ R))%I. Coercion state_to_val (s : state) : val := match s with State Low _ => '0 | State High _ => '1 end. match s with State Low _ => #0 | State High _ => #1 end. Arguments state_to_val !_ /. Definition barrier_inv (l : loc) (P : iProp) (s : state) : iProp := ... ... @@ -126,7 +126,7 @@ Qed. Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) : heapN ⊥ N → (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (LocV l)) ⊑ || newbarrier '() {{ Φ }}. ⊑ || newbarrier #() {{ Φ }}. Proof. intros HN. rewrite /newbarrier. wp_seq. rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj. ... ... @@ -140,7 +140,7 @@ Proof. ▷ (barrier_inv l P (State Low {[ i ]})) ★ saved_prop_own i (Next P))). - rewrite -pvs_intro. cancel [heap_ctx heapN]. rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i (Next P)]. rewrite /barrier_inv /waiting -later_intro. cancel [l ↦ '0]%I. rewrite /barrier_inv /waiting -later_intro. cancel [l ↦ #0]%I. rewrite -(exist_intro (const P)) /=. rewrite -[saved_prop_own _ _](left_id True%I (★)%I). by rewrite !big_sepS_singleton /= wand_diag -later_intro. - rewrite (sts_alloc (barrier_inv l P) ⊤ N); last by eauto. ... ... @@ -172,7 +172,7 @@ Proof. Qed. Lemma signal_spec l P (Φ : val → iProp) : (send l P ★ P ★ Φ '()) ⊑ || signal (LocV l) {{ Φ }}. (send l P ★ P ★ Φ #()) ⊑ || signal (LocV l) {{ Φ }}. Proof. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r. apply exist_elim=>γ. rewrite -!assoc. apply const_elim_sep_l=>?. wp_let. ... ... @@ -183,8 +183,8 @@ Proof. apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc. apply const_elim_sep_l=>Hs. destruct p; last done. rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep. eapply wp_store with (v' := '0); eauto with I ndisj. strip_later. cancel [l ↦ '0]%I. eapply wp_store with (v' := #0); eauto with I ndisj. strip_later. cancel [l ↦ #0]%I. apply wand_intro_l. rewrite -(exist_intro (State High I)). rewrite -(exist_intro ∅). rewrite const_equiv /=; last by eauto using signal_step. rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r. ... ... @@ -199,7 +199,7 @@ Proof. Qed. Lemma wait_spec l P (Φ : val → iProp) : (recv l P ★ (P -★ Φ '())) ⊑ || wait (LocV l) {{ Φ }}. (recv l P ★ (P -★ Φ #())) ⊑ || wait (LocV l) {{ Φ }}. Proof. rename P into R. wp_rec. rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r. ... ...
 ... ... @@ -12,7 +12,8 @@ Local Notation iProp := (iPropG heap_lang Σ). Lemma barrier_spec (heapN N : namespace) : heapN ⊥ N → ∃ recv send : loc → iProp -n> iProp, (∀ P, heap_ctx heapN ⊑ {{ True }} newbarrier '() {{ λ v, ∃ l, v = LocV l ★ recv l P ★ send l P }}) ∧ (∀ P, heap_ctx heapN ⊑ {{ True }} newbarrier #() {{ λ v, ∃ l : loc, v = LocV l ★ recv l P ★ send l P }}) ∧ (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ λ _, True }}) ∧ (∀ l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) ∧ (∀ l P Q, recv l (P ★ Q) ={N}=> recv l P ★ recv l Q) ∧ ... ...
 ... ... @@ -62,7 +62,7 @@ Global Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2). Proof. solve_decision. Defined. Delimit Scope lang_scope with L. Bind Scope lang_scope with expr val. Bind Scope lang_scope with expr val base_lit. Fixpoint of_val (v : val) : expr := match v with ... ...
 ... ... @@ -27,10 +27,9 @@ Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : lang_scope. Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" := (Case e0 x1 e1 x2 e2) (e0, x1, e1, x2, e2 at level 200) : lang_scope. Notation "' l" := (Lit l%Z) (at level 8, format "' l"). Notation "' l" := (LitV l%Z) (at level 8, format "' l"). Notation "'()" := (Lit LitUnit) (at level 0). Notation "'()" := (LitV LitUnit) (at level 0). Notation "()" := LitUnit : lang_scope. Notation "# l" := (Lit l%Z%L) (at level 8, format "# l"). Notation "# l" := (LitV l%Z%L) (at level 8, format "# l"). Notation "! e" := (Load e%L) (at level 9, right associativity) : lang_scope. Notation "'ref' e" := (Alloc e%L) (at level 30, right associativity) : lang_scope. ... ...
 ... ... @@ -4,20 +4,20 @@ From heap_lang Require Import wp_tactics heap notation. Import uPred. Section LangTests. Definition add := ('21 + '21)%L. Goal ∀ σ, prim_step add σ ('42) σ None. Definition add := (#21 + #21)%L. Goal ∀ σ, prim_step add σ (#42) σ None. Proof. intros; do_step done. Qed. Definition rec_app : expr := ((rec: "f" "x" := "f" "x") '0). Definition rec_app : expr := ((rec: "f" "x" := "f" "x") #0). Goal ∀ σ, prim_step rec_app σ rec_app σ None. Proof. intros. rewrite /rec_app. (* FIXME: do_step does not work here *) by eapply (Ectx_step _ _ _ _ _ []), (BetaS _ _ _ _ '0). by eapply (Ectx_step _ _ _ _ _ []), (BetaS _ _ _ _ #0). Qed. Definition lam : expr := λ: "x", "x" + '21. Goal ∀ σ, prim_step (lam '21)%L σ add σ None. Definition lam : expr := λ: "x", "x" + #21. Goal ∀ σ, prim_step (lam #21)%L σ add σ None. Proof. intros. rewrite /lam. (* FIXME: do_step does not work here *) by eapply (Ectx_step _ _ _ _ _ []), (BetaS "" "x" ("x" + '21) _ '21). by eapply (Ectx_step _ _ _ _ _ []), (BetaS "" "x" ("x" + #21) _ #21). Qed. End LangTests. ... ... @@ -28,9 +28,9 @@ Section LiftingTests. Implicit Types Φ : val → iPropG heap_lang Σ. Definition heap_e : expr := let: "x" := ref '1 in "x" <- !"x" + '1;; !"x". let: "x" := ref #1 in "x" <- !"x" + #1;; !"x". Lemma heap_e_spec E N : nclose N ⊆ E → heap_ctx N ⊑ || heap_e @ E {{ λ v, v = '2 }}. nclose N ⊆ E → heap_ctx N ⊑ || heap_e @ E {{ λ v, v = #2 }}. Proof. rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //. wp eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l. ... ... @@ -42,11 +42,11 @@ Section LiftingTests. Definition FindPred : val := rec: "pred" "x" "y" := let: "yp" := "y" + '1 in let: "yp" := "y" + #1 in if: "yp" < "x" then "pred" "x" "yp" else "y". Definition Pred : val := λ: "x", if: "x" ≤ '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0. if: "x" ≤ #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0. Instance FindPred_closed : Closed FindPred | 0. Proof. solve_closed. Qed. ... ... @@ -55,7 +55,7 @@ Section LiftingTests. Lemma FindPred_spec n1 n2 E Φ : n1 < n2 → Φ '(n2 - 1) ⊑ || FindPred 'n2 'n1 @ E {{ Φ }}. Φ #(n2 - 1) ⊑ || FindPred #n2 #n1 @ E {{ Φ }}. Proof. revert n1. wp_rec=>n1 Hn. wp_let. wp_op. wp_let. wp_op=> ?; wp_if. ... ... @@ -64,7 +64,7 @@ Section LiftingTests. - assert (n1 = n2 - 1) as -> by omega; auto with I. Qed. Lemma Pred_spec n E Φ : ▷ Φ (LitV (n - 1)) ⊑ || Pred 'n @ E {{ Φ }}. Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊑ || Pred #n @ E {{ Φ }}. Proof. wp_lam. wp_op=> ?; wp_if. - wp_op. wp_op. ... ... @@ -74,7 +74,7 @@ Section LiftingTests. Qed. Lemma Pred_user E : (True : iProp) ⊑ || let: "x" := Pred '42 in Pred "x" @ E {{ λ v, v = '40 }}. (True : iProp) ⊑ || let: "x" := Pred #42 in Pred "x" @ E {{ λ v, v = #40 }}. Proof. intros. ewp apply Pred_spec. wp_let. ewp apply Pred_spec. auto with I. Qed. ... ... @@ -84,7 +84,7 @@ Section ClosedProofs. Definition Σ : rFunctorG := #[ heapGF ]. Notation iProp := (iPropG heap_lang Σ). Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}. Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = #2 }}. Proof. apply ht_alt. rewrite (heap_alloc ⊤ nroot); last by rewrite nclose_nroot. apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment