store_strong.v 5.34 KB
Newer Older
1 2 3 4 5
From stdpp Require Import namespaces.
From iris_c.vcgen Require Import proofmode.
From iris_c.lib Require Import mset list.
From iris.algebra Require Import frac_auth csum excl agree.

Dan Frumin's avatar
Dan Frumin committed
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
(** This example is meant to demonstrate the usage of atomic rules for
the primitive operations, as well as for function calls.  In this file
we verify the following program:

    #include <stdlib.h>
    #include <stdio.h>
    
    int storeme(int * l) { *l = 10; return 10; }
    
    int main() {
      int * l = calloc(sizeof(int), 1);
      int r = storeme(l) + ( *l = 11 );
      printf("*l = %d, r = %d\n", *l, r);
      return 0;
    }

We prove that the result value r is always 21 and that the value store in l
is either 10 or 11.

To prove this specification we use an invariant that tracks whether the
left/right hand side of the plus operator has been executed. This is achived
using the ghost state variables `γl` and `γr`. The invariant guarantees that
if `γl ≔ b1 ∗ γr ≔ b2`, then we have four possible situations by case-analysis.

    match b1, b2 with
    | false, false => l ↦C #0
    | true, false => l ↦C #10
    | false, true => l ↦C[LLvl] #11
    | true, true => l ↦C #10 ∨ l ↦C[LLvl] #11
    end.

*)

39
Definition storeme : val := λᶜ "l", c_ret "l" =  10.
40

Dan Frumin's avatar
Dan Frumin committed
41
Definition test : val := λᶜ "l",
42 43
  call (c_ret storeme) (c_ret "l") + (c_ret "l" = 11).

Dan Frumin's avatar
Dan Frumin committed
44 45
Section test.
  Context `{cmonadG Σ, !inG Σ (authR (optionUR (exclR boolC)))}.
46

Dan Frumin's avatar
Dan Frumin committed
47
  (** Basic specification for `storeme' *)
48 49 50 51 52 53 54
  Lemma storeme_spec R cl v Φ :
    cl C v - (cl C #10 - Φ #10) -
    CWP storeme (cloc_to_val cl) @ R {{ Φ }}.
  Proof.
    iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H".
  Qed.

Dan Frumin's avatar
Dan Frumin committed
55
  (** Ghost state definitions and lemmas *)
Dan Frumin's avatar
Dan Frumin committed
56 57 58 59 60
  Definition gpointsto γ (b : bool) := own γ ( (Excl' b)).
  Notation "γ '≔' b" := (gpointsto γ b) (at level 80).
  Definition gauth γ b := own γ ( (Excl' b)).
  Lemma gagree γ b1 b2 :
    γ  b1 - gauth γ b2 - b1 = b2.
61
  Proof.
Dan Frumin's avatar
Dan Frumin committed
62 63 64
    iIntros "H1 H2".
    by iDestruct (own_valid_2 with "H2 H1")
      as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
65
  Qed.
Dan Frumin's avatar
Dan Frumin committed
66
  Lemma gnew : (|==>  γ, gauth γ false  γ  false)%I.
67
  Proof.
Dan Frumin's avatar
Dan Frumin committed
68 69 70
    iMod (own_alloc ( (Excl' false)   (Excl' false)))%I as (γ) "[H1 H2]";
      first done;
      eauto with iFrame.
71
  Qed.
Dan Frumin's avatar
Dan Frumin committed
72 73
  Lemma gupdate b3 γ b1 b2 :
    γ  b1 - gauth γ b2 == γ  b3  gauth γ b3.
74
  Proof.
Dan Frumin's avatar
Dan Frumin committed
75 76 77 78 79
    iIntros "H1 H2".
    iMod (own_update_2 with "H2 H1") as "[? ?]".
    { apply auth_update, option_local_update.
      by apply (exclusive_local_update (Excl b2) (Excl b3)). }
    by iFrame.
80 81
  Qed.

Dan Frumin's avatar
Dan Frumin committed
82 83 84 85 86 87 88 89 90
  (** The correctness of the test function. *)
  Definition test_inv cl γl γr : iProp Σ := ( b1 b2, gauth γl b1  gauth γr b2 
    match b1, b2 with
    | false, false => cl C #0
    | true, false => cl C #10
    | false, true => cl C[LLvl] #11
    | _, _ => cl C #10  cl C[LLvl] #11
    end)%I.

Dan Frumin's avatar
Dan Frumin committed
91
  Lemma test_spec R cl `{inG Σ testR, inG Σ fracR} :
92
    cl C #0%nat -
Dan Frumin's avatar
Dan Frumin committed
93
    CWP "x" ←ᶜ test (cloc_to_val cl); c_ret "x" @ R {{ v,  v = #21  
94 95
        (cl C #10  cl C #11) }}.
  Proof.
Dan Frumin's avatar
Dan Frumin committed
96 97 98
    iIntros "Hl". iApply cwp_seq_bind. iApply cwp_fun. simpl.
    iMod gnew as (γl) "[H1 lb]".
    iMod gnew as (γr) "[H2 rb]".
Dan Frumin's avatar
Dan Frumin committed
99
    iApply (cwp_insert_res _ _ (test_inv cl γl γr) with "[H1 H2 Hl]").
Dan Frumin's avatar
Dan Frumin committed
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117
    { iNext. iExists false,false. iFrame. }
    iApply (cwp_bin_op _ _ (λ v, v = #10  γl  true)%I
                           (λ v, v = #11  γr  true)%I
              with "[lb] [rb]").
    - vcg. unfold test_inv. iIntros "[H R]".
      iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
      iDestruct (gagree with "lb H1") as %<-.
      destruct b2; iNext; iModIntro.
      + iMod (gupdate true with "lb H1") as "[lb H1]".
        iApply (storeme_spec with "H").
        iIntros "Hl". iFrame "R".
        iSplitR "lb"; last by (vcg_continue; eauto with iFrame).
        iExists _,_; eauto with iFrame.
      + iMod (gupdate true with "lb H1") as "[lb H1]".
        iApply (storeme_spec with "H").
        iIntros "Hl". iFrame "R".
        iSplitR "lb"; last by (vcg_continue; eauto with iFrame).
        iExists _,_; eauto with iFrame.
Dan Frumin's avatar
Dan Frumin committed
118 119
    - iApply (cwp_store _ _ (λ v, v = cloc_to_val cl)%I
                            (λ v, v = #11)%I).
120
      1,2: vcg; eauto.
Dan Frumin's avatar
Dan Frumin committed
121 122 123
      iIntros (? ? -> ->) "[H R]". unfold test_inv.
      iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
      iDestruct (gagree with "rb H2") as %<-.
Dan Frumin's avatar
Dan Frumin committed
124
      iModIntro.
Dan Frumin's avatar
Dan Frumin committed
125
      destruct b1; iEval (simpl) in "H".
126
      + iExists cl, _. iFrame. iSplit; first done.
Dan Frumin's avatar
Dan Frumin committed
127 128 129 130
        iIntros "Hl".
        iMod (gupdate true with "rb H2") as "[rb H2]".
        iModIntro. iSplitR "rb"; last by eauto with iFrame.
        iExists _,_; eauto with iFrame.
131
      + iExists cl, _. iFrame. iSplit; first done.
Dan Frumin's avatar
Dan Frumin committed
132 133 134 135 136 137 138 139 140 141 142 143 144
        iIntros "Hl".
        iMod (gupdate true with "rb H2") as "[rb H2]".
        iModIntro. iSplitR "rb"; last by eauto with iFrame.
        iExists _,_; eauto with iFrame.
    - iIntros (v1 v2) "[% lb] [% rb]"; simplify_eq/=.
      iExists #21; simpl. iSplit; first done.
      iIntros "H". iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
      do 3 iModIntro.
      iDestruct (gagree with "lb H1") as %<-.
      iDestruct (gagree with "rb H2") as %<-.
      iDestruct "H" as "[H|H]"; iModIntro; vcg; eauto with iFrame.
  Qed.
End test.
145