one_shot.v 7.12 KB
Newer Older
1
From iris.algebra Require Import one_shot dec_agree.
2
From iris.program_logic Require Import hoare.
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
From iris.heap_lang Require Import heap assert wp_tactics notation.
Import uPred.

Definition one_shot_example : val := λ: <>,
  let: "x" := ref (InjL #0) in (
  (* tryset *) (λ: "n",
    CAS '"x" (InjL #0) (InjR '"n")),
  (* check  *) (λ: <>,
    let: "y" := !'"x" in λ: <>,
    match: '"y" with
      InjL <> => #()
    | InjR "n" =>
       match: !'"x" with
         InjL <> => Assert #false
       | InjR "m" => Assert ('"n" = '"m")
       end
    end)).

Class one_shotG Σ :=
  OneShotG { one_shot_inG :> inG heap_lang Σ (one_shotR (dec_agreeR Z)) }.
Definition one_shotGF : gFunctorList :=
  [GFunctor (constRF (one_shotR (dec_agreeR Z)))].
Instance inGF_one_shotG Σ : inGFs heap_lang Σ one_shotGF  one_shotG Σ.
Proof. intros [? _]; split; apply: inGF_inG. Qed.

Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !one_shotG Σ}.
Context (heapN N : namespace) (HN : heapN  N).
Local Notation iProp := (iPropG heap_lang Σ).

Definition one_shot_inv (γ : gname) (l : loc) : iProp :=
  (l  InjLV #0  own γ OneShotPending 
   n : Z, l  InjRV #n  own γ (Shot (DecAgree n)))%I.

Lemma wp_one_shot (Φ : val  iProp) :
  (heap_ctx heapN   f1 f2 : val,
39 40
    ( n : Z,  WP f1 #n {{ λ w, w = #true  w = #false }}) 
     WP f2 #() {{ λ g,  WP g #() {{ λ _, True }} }} - Φ (f1,f2)%V)
41 42 43 44 45 46 47 48 49 50 51
   WP one_shot_example #() {{ Φ }}.
Proof.
  wp_let.
  wp eapply wp_alloc; eauto with I.
  apply forall_intro=> l; apply wand_intro_l.
  eapply sep_elim_True_l; first by apply (own_alloc OneShotPending).
  rewrite !pvs_frame_r; apply wp_strip_pvs.
  rewrite !sep_exist_r; apply exist_elim=>γ.
  (* TODO: this is horrible *)
  trans (heap_ctx heapN  (|==> inv N (one_shot_inv γ l)) 
    ( f1 f2 : val,
52 53
      ( n : Z,  WP f1 #n {{ λ w, w = #true  w = #false }}) 
       WP f2 #() {{ λ g,  WP g #() {{ λ _, True }} }} - Φ (f1, f2)%V))%I.
54 55 56 57 58
  { ecancel [heap_ctx _;  _, _]%I. rewrite -inv_alloc // -later_intro.
    apply or_intro_l'. solve_sep_entails. }
  rewrite pvs_frame_r pvs_frame_l; apply wp_strip_pvs; wp_let.
  rewrite !assoc 2!forall_elim; eapply wand_apply_r'; first done.
  rewrite (always_sep_dup (_  _)); apply sep_mono.
59
  - apply forall_intro=>n. apply: always_intro. wp_let.
60 61 62 63 64 65 66 67 68 69 70
    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
      rewrite /= ?to_of_val; eauto 10 with I.
    rewrite (True_intro (inv _ _)) right_id.
    apply wand_intro_r; rewrite sep_or_l; apply or_elim.
    + rewrite -wp_pvs.
      wp eapply wp_cas_suc; rewrite /= ?to_of_val; eauto with I ndisj.
      rewrite (True_intro (heap_ctx _)) left_id.
      ecancel [l  _]%I; apply wand_intro_l.
      rewrite (own_update); (* FIXME: canonical structures are not working *)
        last by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)).
      rewrite pvs_frame_l; apply pvs_mono, sep_intro_True_r; eauto with I.
71
      rewrite /one_shot_inv -or_intro_r -(exist_intro n).
72 73 74 75 76
      solve_sep_entails.
    + rewrite sep_exist_l; apply exist_elim=>m.
      eapply wp_cas_fail with (v':=InjRV #m) (q:=1%Qp);
        rewrite /= ?to_of_val; eauto with I ndisj; strip_later.
      ecancel [l  _]%I; apply wand_intro_l, sep_intro_True_r; eauto with I.
77
      rewrite /one_shot_inv -or_intro_r -(exist_intro m).
78
      solve_sep_entails.
79
  - apply: always_intro. wp_seq.
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
    wp_focus (Load (%l))%I.
    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
      rewrite /= ?to_of_val; eauto 10 with I.
    apply wand_intro_r.
    trans (heap_ctx heapN  inv N (one_shot_inv γ l)   v, l  v 
      ((v = InjLV #0  own γ OneShotPending) 
        n : Z, v = InjRV #n  own γ (Shot (DecAgree n))))%I.
    { rewrite assoc. apply sep_mono_r, or_elim.
      + rewrite -(exist_intro (InjLV #0)). rewrite -or_intro_l const_equiv //.
        solve_sep_entails.
      + apply exist_elim=> n. rewrite -(exist_intro (InjRV #n)) -(exist_intro n).
        apply sep_mono_r, or_intro_r', sep_intro_True_l; eauto with I. }
    rewrite !sep_exist_l; apply exist_elim=> w.
    eapply wp_load with (q:=1%Qp) (v:=w); eauto with I ndisj.
    rewrite -later_intro; cancel [l  w]%I.
95
    rewrite -later_intro; apply wand_intro_l.
96 97 98 99 100 101 102 103 104 105 106
    trans (heap_ctx heapN  inv N (one_shot_inv γ l)  one_shot_inv γ l 
      (w = InjLV #0  ( n : Z, w = InjRV #n  own γ (Shot (DecAgree n)))))%I.
    { cancel [heap_ctx heapN]. rewrite !sep_or_l; apply or_elim.
      + rewrite -or_intro_l. ecancel [inv _ _]%I.
        rewrite [(_  _)%I]comm -assoc. apply const_elim_sep_l=>->.
        rewrite const_equiv // right_id /one_shot_inv -or_intro_l .
        solve_sep_entails.
      + rewrite -or_intro_r !sep_exist_l; apply exist_elim=> n.
        rewrite -(exist_intro n). ecancel [inv _ _]%I.
        rewrite [(_  _)%I]comm -assoc. apply const_elim_sep_l=>->.
        rewrite const_equiv // left_id /one_shot_inv -or_intro_r.
107
        rewrite -(exist_intro n) {1}(always_sep_dup (own _ _)).
108 109 110
        solve_sep_entails. }
    cancel [one_shot_inv γ l].
    (* FIXME: why aren't laters stripped? *)
111 112
    wp_let. rewrite -later_intro.
    apply: always_intro. wp_seq. rewrite -later_intro.
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
    rewrite !sep_or_l; apply or_elim.
    { rewrite assoc.
      apply const_elim_sep_r=>->. wp_case; wp_seq; eauto with I. }
    rewrite !sep_exist_l; apply exist_elim=> n.
    rewrite [(w=_  _)%I]comm !assoc; apply const_elim_sep_r=>->.
    (* FIXME: why do we need to fold? *)
    wp_case; fold of_val. wp_let. wp_focus (Load (%l))%I.
    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
      rewrite /= ?to_of_val; eauto 10 with I.
    rewrite (True_intro (inv _ _)) right_id.
    apply wand_intro_r; rewrite sep_or_l; apply or_elim.
    + rewrite (True_intro (heap_ctx _)) (True_intro (l  _)) !left_id.
      rewrite -own_op own_valid_l one_shot_validI /= left_absorb.
      apply False_elim.
    + rewrite !sep_exist_l; apply exist_elim=> m.
      eapply wp_load with (q:=1%Qp) (v:=InjRV #m); eauto with I ndisj; strip_later.
      cancel [l  InjRV #m]%I. apply wand_intro_r.
      rewrite (True_intro (heap_ctx heapN)) left_id.
      rewrite -own_op own_valid_l one_shot_validI Shot_op /= discrete_valid.
      rewrite -assoc. apply const_elim_sep_l=> /dec_agree_op_inv [->].
133
      rewrite dec_agree_idemp. apply sep_intro_True_r.
134 135 136 137
      { rewrite /one_shot_inv -or_intro_r -(exist_intro m). solve_sep_entails. }
      wp_case; fold of_val. wp_let. rewrite -wp_assert'.
      wp_op; by eauto using later_intro with I.
Qed.
138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153

Lemma hoare_one_shot (Φ : val  iProp) :
  heap_ctx heapN  {{ True }} one_shot_example #()
    {{ λ ff,
      ( n : Z, {{ True }} Fst ff #n {{ λ w, w = #true  w = #false }}) 
      {{ True }} Snd ff #() {{ λ g, {{ True }} g #() {{ λ _, True }} }}
    }}.
Proof.
  apply: always_intro; rewrite left_id -wp_one_shot /=.
  cancel [heap_ctx heapN].
  apply forall_intro=> f1; apply forall_intro=> f2.
  apply wand_intro_l; rewrite right_id; apply sep_mono.
  - apply forall_mono=>n. apply always_mono; rewrite left_id. by wp_proj.
  - apply always_mono; rewrite left_id. wp_proj.
    apply wp_mono=> v. by apply always_mono; rewrite left_id.
Qed.
154
End proof.