TimeReceipts.v 13.5 KB
Newer Older
1
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
MEVEL Glen's avatar
MEVEL Glen committed
2 3
From iris.base_logic Require Import invariants.

4 5
From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics.
From iris_time Require Export Translation Simulation.
MEVEL Glen's avatar
MEVEL Glen committed
6 7 8 9 10 11

Implicit Type e : expr.
Implicit Type v : val.
Implicit Type σ : state.
Implicit Type t : list expr.
Implicit Type K : ectx heap_ectx_lang.
MEVEL Glen's avatar
MEVEL Glen committed
12 13 14
Implicit Type m n nmax : nat.
Implicit Type φ ψ : val  Prop.
Implicit Type Σ : gFunctors.
MEVEL Glen's avatar
MEVEL Glen committed
15 16 17



18 19 20 21 22 23
(*
 * Abstract interface of time receipts
 *)

(* Ideally, this would be represented as a record (or a typeclass), but it has
 * to be an Iris proposition (iProp Σ) and not a Coq proposition (Prop). *)
24
Definition TR_interface `{irisG heap_lang Σ, Tick}
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
  (nmax : nat)
  (TR : nat  iProp Σ)
  (TRdup : nat  iProp Σ)
: iProp Σ := (
     n, Timeless (TR n)
    n, Timeless (TRdup n)
    n, Persistent (TRdup n)
   ( n, TR n ={}= TR n  TRdup n)
   (|={}=> TR 0%nat)
(*   ∗ (|={⊤}=> TRdup 0%nat) *)
    m n, TR (m + n)%nat  (TR m  TR n)
    m n, TRdup (m `max` n)  (TRdup m  TRdup n)
(*   ∗ (TR nmax ={⊤}=∗ False) *)
   (TRdup nmax ={}= False)
   ( v n, {{{ TRdup n }}} tick v {{{ RET v ; TR 1%nat  TRdup (n+1)%nat }}})
)%I.



MEVEL Glen's avatar
MEVEL Glen committed
44 45 46 47 48 49 50 51 52 53 54 55 56 57
(*
 * Prerequisites on the global monoid Σ
 *)

Class timeReceiptHeapPreG Σ := {
  timeReceiptHeapPreG_heapPreG :> heapPreG Σ ;
  timeReceiptHeapPreG_inG1 :> inG Σ (authR natUR) ;
  timeReceiptHeapPreG_inG2 :> inG Σ (authR mnatUR) ;
}.

Class timeReceiptHeapG Σ := {
  timeReceiptHeapG_heapG :> heapG Σ ;
  timeReceiptHeapG_inG1 :> inG Σ (authR natUR) ;
  timeReceiptHeapG_inG2 :> inG Σ (authR mnatUR) ;
58
  timeReceiptHeapG_loc :> TickCounter ;
MEVEL Glen's avatar
MEVEL Glen committed
59 60 61 62 63 64
  timeReceiptHeapG_name1 : gname ;
  timeReceiptHeapG_name2 : gname ;
}.

Local Notation γ1 := timeReceiptHeapG_name1.
Local Notation γ2 := timeReceiptHeapG_name2.
65
Local Notation  := tick_counter.
MEVEL Glen's avatar
MEVEL Glen committed
66 67 68 69



(*
70
 * Implementation and specification of `TR` and `tick`
MEVEL Glen's avatar
MEVEL Glen committed
71 72
 *)

73 74
Definition loop : val :=
  rec: "f" <> := "f" #().
MEVEL Glen's avatar
MEVEL Glen committed
75

76
Global Instance receipts_tick `{TickCounter} : Tick :=
77
  generic_tick loop.
MEVEL Glen's avatar
MEVEL Glen committed
78

79
Section TickSpec.
MEVEL Glen's avatar
MEVEL Glen committed
80 81

  Context `{timeReceiptHeapG Σ}.
MEVEL Glen's avatar
MEVEL Glen committed
82
  Context (nmax : nat).
MEVEL Glen's avatar
MEVEL Glen committed
83 84 85 86 87 88 89 90 91 92 93 94 95 96

  Definition TR (n : nat) : iProp Σ :=
    own γ1 (nat n).

  Definition TRdup (n : mnat) : iProp Σ :=
    own γ2 (mnat n).
  Arguments TRdup _%nat_scope.

  Lemma TR_plus m n :
    TR (m + n)  (TR m  TR n)%I.
  Proof. by rewrite /TR auth_frag_op own_op. Qed.
  Lemma TR_succ n :
    TR (S n)  (TR 1  TR n)%I.
  Proof. by rewrite (eq_refl : S n = 1 + n)%nat TR_plus. Qed.
MEVEL Glen's avatar
MEVEL Glen committed
97 98 99 100
  Lemma TR_weaken (n n : nat) :
    (n  n)%nat 
    TR n - TR n.
  Proof. apply own_auth_nat_weaken. Qed.
MEVEL Glen's avatar
MEVEL Glen committed
101 102 103 104 105

  Lemma TR_timeless n :
    Timeless (TR n).
  Proof. exact _. Qed.

106 107 108 109 110 111 112 113
  Global Instance into_sep_TR_plus m n : IntoSep (TR (m + n)) (TR m) (TR n).
  Proof. by rewrite /IntoSep TR_plus. Qed.
  Global Instance from_sep_TR_plus m n : FromSep (TR (m + n)) (TR m) (TR n).
  Proof. by rewrite /FromSep TR_plus. Qed.
  Global Instance into_sep_TR_succ n : IntoSep (TR (S n)) (TR 1) (TR n).
  Proof. by rewrite /IntoSep TR_succ. Qed.
  Global Instance from_sep_TR_succ n : FromSep (TR (S n)) (TR 1) (TR n).
  Proof. by rewrite /FromSep [TR (S n)] TR_succ. Qed.
MEVEL Glen's avatar
MEVEL Glen committed
114 115 116 117

  Lemma TRdup_max m n :
    TRdup (m `max` n)  (TRdup m  TRdup n)%I.
  Proof. by rewrite /TRdup auth_frag_op own_op. Qed.
MEVEL Glen's avatar
MEVEL Glen committed
118 119 120 121
  Lemma TRdup_weaken (n n : nat) :
    (n  n)%nat 
    TRdup n - TRdup n.
  Proof. apply own_auth_mnat_weaken. Qed.
MEVEL Glen's avatar
MEVEL Glen committed
122 123 124 125

  Lemma TRdup_timeless n :
    Timeless (TRdup n).
  Proof. exact _. Qed.
126 127 128
  Lemma TRdup_persistent n :
    Persistent (TRdup n).
  Proof. exact _. Qed.
MEVEL Glen's avatar
MEVEL Glen committed
129

130 131 132 133
  Global Instance into_sep_TRdup_max m n : IntoSep (TRdup (m `max` n)) (TRdup m) (TRdup n).
  Proof. by rewrite /IntoSep TRdup_max. Qed.
  Global Instance from_sep_TRdup_max m n : FromSep (TRdup (m `max` n)) (TRdup m) (TRdup n).
  Proof. by rewrite /FromSep TRdup_max. Qed.
MEVEL Glen's avatar
MEVEL Glen committed
134 135 136

  Definition timeReceiptN := nroot .@ "timeReceipt".

MEVEL Glen's avatar
MEVEL Glen committed
137
  Definition TR_invariant : iProp Σ :=
MEVEL Glen's avatar
MEVEL Glen committed
138 139
    inv timeReceiptN ( (n:nat),   #(nmax-n-1)  own γ1 (nat n)  own γ2 (mnat n)  (n < nmax)%nat)%I.

MEVEL Glen's avatar
MEVEL Glen committed
140 141
  Lemma zero_TR :
    TR_invariant ={}= TR 0.
142
  Proof.
143
    iIntros "#Htickinv".
144 145 146 147 148
    iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & H)" "Hclose".
    iDestruct (own_auth_nat_null with "Hγ1●") as "[Hγ1● $]".
    iApply "Hclose" ; eauto with iFrame.
  Qed.

MEVEL Glen's avatar
MEVEL Glen committed
149 150
  Lemma zero_TRdup :
    TR_invariant ={}= TRdup 0.
151
  Proof.
152
    iIntros "#Htickinv".
153 154 155 156 157
    iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & Hγ2● & Im)" "Hclose".
    iDestruct (own_auth_mnat_null with "Hγ2●") as "[Hγ2● $]".
    iApply "Hclose" ; eauto with iFrame.
  Qed.

MEVEL Glen's avatar
MEVEL Glen committed
158
  Lemma TR_nmax_absurd (E : coPset) :
MEVEL Glen's avatar
MEVEL Glen committed
159
    timeReceiptN  E 
MEVEL Glen's avatar
MEVEL Glen committed
160
    TR_invariant - TR nmax ={E}= False.
MEVEL Glen's avatar
MEVEL Glen committed
161 162 163 164 165 166
  Proof.
    iIntros (?) "#Inv Hγ1◯".
    iInv timeReceiptN as (n) ">(Hℓ & Hγ1● & Hγ2● & In)" "InvClose" ; iDestruct "In" as %In.
    iDestruct (own_auth_nat_le with "Hγ1● Hγ1◯") as %In'.
    exfalso ; lia.
  Qed.
MEVEL Glen's avatar
MEVEL Glen committed
167 168 169 170 171 172 173 174 175 176
  Lemma TR_lt_nmax n (E : coPset) :
    timeReceiptN  E 
    TR_invariant - TR n ={E}= TR n  n < nmax%nat.
  Proof.
    iIntros (?) "#Inv Hγ1◯".
    destruct (le_lt_dec nmax n) as [ I | I ] ; last by iFrame.
    iDestruct (TR_weaken n nmax with "Hγ1◯") as "Hγ1◯" ; first done.
    iDestruct (TR_nmax_absurd with "Inv Hγ1◯") as ">?" ; first done.
    done.
  Qed.
MEVEL Glen's avatar
MEVEL Glen committed
177

MEVEL Glen's avatar
MEVEL Glen committed
178
  Lemma TRdup_nmax_absurd (E : coPset) :
179
    timeReceiptN  E 
MEVEL Glen's avatar
MEVEL Glen committed
180
    TR_invariant - TRdup nmax ={E}= False.
181 182 183 184 185 186
  Proof.
    iIntros (?) "#Inv Hγ2◯".
    iInv timeReceiptN as (n) ">(Hℓ & Hγ1● & Hγ2● & In)" "InvClose" ; iDestruct "In" as %In.
    iDestruct (own_auth_mnat_le with "Hγ2● Hγ2◯") as %In'.
    exfalso ; lia.
  Qed.
MEVEL Glen's avatar
MEVEL Glen committed
187 188 189 190 191 192 193 194 195 196
  Lemma TRdup_lt_nmax n (E : coPset) :
    timeReceiptN  E 
    TR_invariant - TRdup n ={E}= TRdup n  n < nmax%nat.
  Proof.
    iIntros (?) "#Inv Hγ1◯".
    destruct (le_lt_dec nmax n) as [ I | I ] ; last by iFrame.
    iDestruct (TRdup_weaken n nmax with "Hγ1◯") as "Hγ1◯" ; first done.
    iDestruct (TRdup_nmax_absurd with "Inv Hγ1◯") as ">?" ; first done.
    done.
  Qed.
197

MEVEL Glen's avatar
MEVEL Glen committed
198
  Lemma TR_TRdup (E : coPset) n :
MEVEL Glen's avatar
MEVEL Glen committed
199
    timeReceiptN  E 
MEVEL Glen's avatar
MEVEL Glen committed
200
    TR_invariant - TR n ={E}= TR n  TRdup n.
MEVEL Glen's avatar
MEVEL Glen committed
201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218
  Proof.
    iIntros (?) "#Inv Hγ1◯".
    iInv timeReceiptN as (m) ">(Hℓ & Hγ1● & Hγ2● & Im)" "InvClose".
    iDestruct (own_auth_nat_le with "Hγ1● Hγ1◯") as %In.
    iDestruct (auth_mnat_update_read_auth with "Hγ2●") as ">[Hγ2● Hγ2◯]".
    iAssert (TR n  TRdup n)%I with "[$Hγ1◯ Hγ2◯]" as "$". {
      rewrite (_ : m = m `max` n) ; last lia.
      iDestruct "Hγ2◯" as "[_ $]".
    }
    iApply "InvClose". auto with iFrame.
  Qed.

  Theorem loop_spec s E (Φ : val  iProp Σ) :
    WP loop #() @ s ; E {{ Φ }}%I.
  Proof.
    iLöb as "IH". wp_rec. iExact "IH".
  Qed.

219
  Theorem tick_spec s E (v : val) m :
MEVEL Glen's avatar
MEVEL Glen committed
220
    timeReceiptN  E 
MEVEL Glen's avatar
MEVEL Glen committed
221
    TR_invariant -
222
    {{{ TRdup m }}} tick v @ s ; E {{{ RET v ; TR 1  TRdup (m+1) }}}.
MEVEL Glen's avatar
MEVEL Glen committed
223
  Proof.
224
    intros ?. iIntros "#Inv" (Ψ) "!# Hγ2◯ HΨ".
MEVEL Glen's avatar
MEVEL Glen committed
225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252
    iLöb as "IH".
    wp_lam.
    (* open the invariant, in order to read the value k = nmax−n−1 of location ℓ: *)
    wp_bind (! _)%E ;
    iInv timeReceiptN as (n) ">(Hℓ & Hγ1● & Hγ2● & In)" "InvClose" ; iDestruct "In" as %In.
    wp_load.
    (* close the invariant: *)
    iMod ("InvClose" with "[ Hℓ Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ].
    wp_let.
    (* test whether k ≤ 0: *)
    wp_op ; destruct (bool_decide (nmax - n - 1  0)) eqn:Im ; wp_if.
    (* — if k ≤ 0 then we loop indefinitely, which gives us any spec we want
         (because we are reasoning in partial correctness): *)
    - iApply loop_spec.
    (* — otherwise: *)
    - apply Is_true_false in Im ; rewrite -> bool_decide_spec in Im.
      wp_op.
      (* open the invariant again, in order to perform CAS on location ℓ: *)
      wp_bind (CAS _ _ _)%E ;
      iInv timeReceiptN as (n') ">(Hℓ & Hγ1● & Hγ2● & In')" "InvClose" ; iDestruct "In'" as %In'.
      (* test whether the value ℓ is still k, by comparing n with n': *)
      destruct (nat_eq_dec n n') as [ <- | Hneq ].
      (* — if it holds, then CAS succeeds and ℓ is decremented: *)
      + wp_cas_suc.
        (* reform the invariant with n+1 instead of n, and an additional time
           receipt produced: *)
        replace (nmax - n - 1 - 1) with (nmax - (n+1)%nat - 1) by lia.
        iMod (auth_nat_update_incr _ _ 1 with "Hγ1●") as "[Hγ1● Hγ1◯]" ; simpl.
253 254
(*         iMod (auth_mnat_update_incr _ _ 1 with "Hγ2●") as "Hγ2●" ; simpl. *)
        iMod (auth_mnat_update_incr' _ _ _ 1 with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]" ; simpl.
MEVEL Glen's avatar
MEVEL Glen committed
255 256 257 258
        assert ((n+1) < nmax)%nat by lia.
        (* close the invariant: *)
        iMod ("InvClose" with "[ Hℓ Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ].
        (* finish: *)
259
        wp_if. iApply "HΨ" ; by iFrame.
MEVEL Glen's avatar
MEVEL Glen committed
260 261 262 263 264 265
      (* — otherwise, CAS fails and ℓ is unchanged: *)
      + wp_cas_fail ; first (injection ; lia).
        (* close the invariant as is: *)
        iMod ("InvClose" with "[ Hℓ Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ] ; clear dependent n.
        wp_if.
        (* conclude using the induction hypothesis: *)
266
        iApply ("IH" with "Hγ2◯ HΨ").
MEVEL Glen's avatar
MEVEL Glen committed
267 268
  Qed.

269
  Theorem tick_spec_simple v n :
MEVEL Glen's avatar
MEVEL Glen committed
270
    TR_invariant -
271
    {{{ TRdup n }}} tick v {{{ RET v ; TR 1  TRdup (n+1) }}}.
MEVEL Glen's avatar
MEVEL Glen committed
272 273
  Proof.
    iIntros "#Inv" (Ψ) "!# H HΨ".
274
    by iApply (tick_spec with "Inv H HΨ").
MEVEL Glen's avatar
MEVEL Glen committed
275 276
  Qed.

277
  Lemma TR_implementation : TR_invariant - TR_interface nmax TR TRdup.
278 279 280 281 282 283 284 285 286 287
  Proof.
    iIntros "#Hinv". repeat iSplitR.
    - iPureIntro. by apply TR_timeless.
    - iPureIntro. by apply TRdup_timeless.
    - iPureIntro. by apply TRdup_persistent.
    - iIntros (n). by iApply (TR_TRdup with "Hinv").
    - by iApply (zero_TR with "Hinv").
    - iPureIntro. by apply TR_plus.
    - iPureIntro. by apply TRdup_max.
    - by iApply (TRdup_nmax_absurd with "Hinv").
288
    - iIntros (v n). by iApply (tick_spec_simple with "Hinv").
289 290
  Qed.

291
End TickSpec.
MEVEL Glen's avatar
MEVEL Glen committed
292 293 294 295 296 297 298 299 300



(*
 * Simulation
 *)

Section Soundness.

301
  Definition adequate_trtranslation__adequate := adequate_translation__adequate loop.
302 303 304

  (* derive the adequacy of the translated program from a Hoare triple in Iris. *)

MEVEL Glen's avatar
MEVEL Glen committed
305
  Lemma spec_trtranslation__adequate_translation {Σ} nmax ψ e :
306
    (0 < nmax)%nat 
307
    ( `{timeReceiptHeapG Σ},
MEVEL Glen's avatar
MEVEL Glen committed
308
      TR_invariant nmax -
309 310
      {{{ True }}} «e» {{{ v, RET v ; ⌜ψ v }}}
    ) 
311
     `{timeReceiptHeapPreG Σ, TickCounter} σ,
312
      adequate NotStuck «e» S«σ,nmax-1» (λ v σ, ψ v).
313 314 315
  Proof.
    intros Inmax Hspec HpreG Hloc σ.
    (* apply the adequacy results. *)
316
    apply (wp_adequacy _ _) ; simpl ; intros HinvG κ.
317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333
    (* … now we have to prove a WP. *)
    set σ' := S«σ».
    (* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
    iMod (own_alloc ( to_gen_heap (<[ := #(nmax-1)%nat]> σ')   to_gen_heap {[ := #(nmax-1)%nat]}))
      as (h) "[Hh● Hℓ◯]".
    {
      apply auth_valid_discrete_2 ; split.
      - rewrite - insert_delete ; set σ'' := delete  σ'.
        unfold to_gen_heap ; rewrite 2! fmap_insert fmap_empty insert_empty.
        exists (to_gen_heap σ'').
        rewrite (@gmap.insert_singleton_op _ _ _ _ (to_gen_heap σ'')) //.
        rewrite lookup_fmap ; apply fmap_None, lookup_delete.
      - apply to_gen_heap_valid.
    }
    (* allocate the ghost state associated with ℓ: *)
    iMod (auth_nat_alloc 0) as (γ1) "[Hγ1● _]".
    iMod (auth_mnat_alloc 0) as (γ2) "[Hγ2● _]".
MEVEL Glen's avatar
MEVEL Glen committed
334
    (* packing all those bits, build the heap instance necessary to use time receipts: *)
335 336 337
    pose (Build_timeReceiptHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ h)) _ _ _ γ1 γ2)
      as HtrHeapG.
    (* create the invariant: *)
MEVEL Glen's avatar
MEVEL Glen committed
338
    iAssert (|={}=> TR_invariant nmax)%I with "[Hℓ◯ Hγ1● Hγ2●]" as "> Hinv".
339 340 341 342 343 344 345 346 347
    {
      iApply inv_alloc.
      iExists 0%nat. rewrite (_ : nmax - 0 - 1 = Z.of_nat (nmax - 1)) ; last lia.
      unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl.
      unfold to_gen_heap ; rewrite fmap_insert fmap_empty insert_empty.
      by iFrame.
    }
    iModIntro.
    (* finally, use the user-given specification: *)
348
    iExists (λ σ _, gen_heap_ctx σ). iFrame "Hh●".
349 350 351
    iApply (Hspec with "Hinv") ; auto.
  Qed.

MEVEL Glen's avatar
MEVEL Glen committed
352
  Theorem spec_trtranslation__adequate {Σ} nmax φ e :
353
    (0 < nmax)%nat 
354
    ( `{timeReceiptHeapG Σ},
MEVEL Glen's avatar
MEVEL Glen committed
355
      TR_invariant nmax -
356 357 358
      {{{ True }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
    ) 
     `{!timeReceiptHeapPreG Σ} σ,
MEVEL Glen's avatar
MEVEL Glen committed
359
      nadequate NotStuck (nmax-1) e σ φ.
360
  Proof.
361 362
    intros Inmax Hspec HpreG σ.
    eapply adequate_trtranslation__adequate.
363 364
    intros Hloc. by eapply spec_trtranslation__adequate_translation.
  Qed.
MEVEL Glen's avatar
MEVEL Glen committed
365

MEVEL Glen's avatar
MEVEL Glen committed
366
  Theorem abstract_spec_trtranslation__adequate {Σ} nmax φ e :
367
    (0 < nmax)%nat 
368 369
    ( `{heapG Σ, Tick} (TR TRdup : nat  iProp Σ),
      TR_interface nmax TR TRdup -
370
      {{{ True }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
371 372
    ) 
     {_ : timeReceiptHeapPreG Σ} σ,
MEVEL Glen's avatar
MEVEL Glen committed
373
      nadequate NotStuck (nmax-1) e σ φ.
374
  Proof.
375 376
    intros Inmax Hspec HpreG σ.
    eapply spec_trtranslation__adequate; try done.
377 378 379 380
    clear HpreG. iIntros (HtrHeapG) "#Hinv".
    iApply Hspec. by iApply TR_implementation.
  Qed.

MEVEL Glen's avatar
MEVEL Glen committed
381 382 383 384 385 386 387 388 389 390 391 392 393 394 395
End Soundness.



(*
 * Proof-mode tactics for proving WP of translated expressions
 *)

Section Tactics.

  (* TODO *)

End Tactics.

Ltac wp_tock :=
396
  idtac.