TimeReceipts.v 16.8 KB
Newer Older
MEVEL Glen's avatar
MEVEL Glen committed
1
From iris.base_logic Require Import invariants.
2
From iris.proofmode Require Import coq_tactics.
MEVEL Glen's avatar
MEVEL Glen committed
3

4
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
5 6
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
7 8 9 10 11 12

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
13 14 15
Implicit Type m n nmax : nat.
Implicit Type φ ψ : val  Prop.
Implicit Type Σ : gFunctors.
MEVEL Glen's avatar
MEVEL Glen committed
16 17 18



19 20 21 22 23 24
(*
 * 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). *)
25
Definition TR_interface `{irisG heap_lang Σ, Tick}
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
  (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
45 46 47 48 49 50 51 52 53 54 55 56 57 58
(*
 * 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) ;
59
  timeReceiptHeapG_loc :> TickCounter ;
MEVEL Glen's avatar
MEVEL Glen committed
60 61 62 63 64 65
  timeReceiptHeapG_name1 : gname ;
  timeReceiptHeapG_name2 : gname ;
}.

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



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

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

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

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

82
  Context `{timeReceiptHeapG Σ} (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.

140 141 142
  Lemma zero_TR E :
    timeReceiptN  E 
    TR_invariant ={E}= TR 0.
143
  Proof.
144
    iIntros (?) "#Htickinv".
145 146 147 148 149
    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.

150 151 152
  Lemma zero_TRdup E :
    timeReceiptN  E 
    TR_invariant ={E}= TRdup 0.
153
  Proof.
154
    iIntros (?) "#Htickinv".
155 156 157 158 159
    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
160
  Lemma TR_nmax_absurd (E : coPset) :
MEVEL Glen's avatar
MEVEL Glen committed
161
    timeReceiptN  E 
MEVEL Glen's avatar
MEVEL Glen committed
162
    TR_invariant - TR nmax ={E}= False.
MEVEL Glen's avatar
MEVEL Glen committed
163 164 165 166 167 168
  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
169 170 171 172 173 174 175 176 177 178
  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
179

MEVEL Glen's avatar
MEVEL Glen committed
180
  Lemma TRdup_nmax_absurd (E : coPset) :
181
    timeReceiptN  E 
MEVEL Glen's avatar
MEVEL Glen committed
182
    TR_invariant - TRdup nmax ={E}= False.
183 184 185 186 187 188
  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
189 190 191 192 193 194 195 196 197 198
  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.
199

MEVEL Glen's avatar
MEVEL Glen committed
200
  Lemma TR_TRdup (E : coPset) n :
MEVEL Glen's avatar
MEVEL Glen committed
201
    timeReceiptN  E 
MEVEL Glen's avatar
MEVEL Glen committed
202
    TR_invariant - TR n ={E}= TR n  TRdup n.
MEVEL Glen's avatar
MEVEL Glen committed
203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220
  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.

221
  Theorem tick_spec s E (v : val) m :
MEVEL Glen's avatar
MEVEL Glen committed
222
    timeReceiptN  E 
MEVEL Glen's avatar
MEVEL Glen committed
223
    TR_invariant -
224
    {{{ TRdup m }}} tick v @ s ; E {{{ RET v ; TR 1  TRdup (m+1) }}}.
MEVEL Glen's avatar
MEVEL Glen committed
225
  Proof.
226
    intros ?. iIntros "#Inv" (Ψ) "!# Hγ2◯ HΨ".
MEVEL Glen's avatar
MEVEL Glen committed
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 253 254
    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.
255 256
(*         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
257 258 259 260
        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: *)
261
        wp_if. iApply "HΨ" ; by iFrame.
MEVEL Glen's avatar
MEVEL Glen committed
262 263 264 265 266 267
      (* — 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: *)
268
        iApply ("IH" with "Hγ2◯ HΨ").
MEVEL Glen's avatar
MEVEL Glen committed
269 270
  Qed.

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

279
  Lemma TR_implementation : TR_invariant - TR_interface nmax TR TRdup.
280 281 282 283 284 285 286 287 288 289
  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").
290
    - iIntros (v n). by iApply (tick_spec_simple with "Hinv").
291 292
  Qed.

293
End TickSpec.
MEVEL Glen's avatar
MEVEL Glen committed
294 295 296 297



(*
MEVEL Glen's avatar
MEVEL Glen committed
298
 * Soundness
MEVEL Glen's avatar
MEVEL Glen committed
299 300 301 302
 *)

Section Soundness.

MEVEL Glen's avatar
MEVEL Glen committed
303
  Definition adequate_trtranslation__nadequate := adequate_translation__nadequate loop.
304 305 306

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

MEVEL Glen's avatar
MEVEL Glen committed
307
  Lemma spec_trtranslation__adequate_translation {Σ} nmax ψ e :
308
    (0 < nmax)%nat 
309
    ( `{timeReceiptHeapG Σ},
MEVEL Glen's avatar
MEVEL Glen committed
310
      TR_invariant nmax -
311 312
      {{{ True }}} «e» {{{ v, RET v ; ⌜ψ v }}}
    ) 
313
     `{timeReceiptHeapPreG Σ, TickCounter} σ,
314
      adequate NotStuck «e» S«σ,nmax-1» (λ v σ, ψ v).
315 316 317
  Proof.
    intros Inmax Hspec HpreG Hloc σ.
    (* apply the adequacy results. *)
318
    apply (wp_adequacy _ _) ; simpl ; intros HinvG κ.
319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335
    (* … 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
336
    (* packing all those bits, build the heap instance necessary to use time receipts: *)
337 338 339
    pose (Build_timeReceiptHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ h)) _ _ _ γ1 γ2)
      as HtrHeapG.
    (* create the invariant: *)
MEVEL Glen's avatar
MEVEL Glen committed
340
    iAssert (|={}=> TR_invariant nmax)%I with "[Hℓ◯ Hγ1● Hγ2●]" as "> Hinv".
341 342 343 344 345 346 347 348 349
    {
      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: *)
350
    iExists (λ σ _, gen_heap_ctx σ). iFrame "Hh●".
351 352 353
    iApply (Hspec with "Hinv") ; auto.
  Qed.

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

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

MEVEL Glen's avatar
MEVEL Glen committed
383 384 385 386 387 388
End Soundness.

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

389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437
Lemma tac_wp_tick `{timeReceiptHeapG Σ} Δ pe Δ1 Δ2 Δ' i max_tc s E K (v : val) Φ :
  timeReceiptN  E 
  MaybeIntoLaterNEnvs 1 Δ Δ1 

  envs_lookup i Δ = Some (pe, TR_invariant max_tc) 

  ( j pe' p, envs_lookup j Δ1 = Some (pe', TRdup p) 
              envs_simple_replace j pe' (Esnoc Enil j (TRdup (S p))) Δ1 = Some Δ2) 
  Δ1 = Δ2 

  ( j n, envs_lookup j Δ2 = Some (false, TR n) 
          envs_simple_replace j false (Esnoc Enil j (TR (S n))) Δ2 = Some Δ') 
  Δ2 = Δ' 

  envs_entails Δ' (WP fill K v @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_eq=>??? HTRdup HTR HWP.
  iIntros "HΔ".
  iAssert (TR_invariant max_tc) as "#Hinv".
  { destruct pe.
    iDestruct (envs_lookup_sound _ i true with "HΔ") as "[? _]"=>//.
    iDestruct (envs_lookup_sound _ i false with "HΔ") as "[? _]"=>//. }
  iDestruct (into_laterN_env_sound with "HΔ") as "HΔ1"=>//.
  iApply wp_bind.
  destruct HTR as [(j & n & HTR1 & HTR2)| ->],
           HTRdup as [(j' & pe'' & p & HTRDup1 & HTRDup2)| ->].
  - iDestruct (envs_simple_replace_singleton_sound with "HΔ1") as "[HTRdup HΔ2]"=>//.
    rewrite bi.intuitionistically_if_elim -bi.intuitionistically_intuitionistically_if.
    iDestruct "HTRdup" as "#>HTRdup".
    iApply (tick_spec with "[//] HTRdup")=>//. iIntros "!> [HTR #HTRdup']". iApply HWP.
    rewrite Nat.add_comm. iSpecialize ("HΔ2" with "[//]").
    iDestruct (envs_simple_replace_singleton_sound with "HΔ2") as "[HTR' HΔ']"=>//=.
    iCombine "HTR HTR'" as "HTR". iDestruct ("HΔ'" with "HTR") as "$".
  - iMod (zero_TRdup with "Hinv") as "HTRdup"=>//.
    iApply (tick_spec with "[//] HTRdup")=>//. iIntros "!> [HTR _]". iApply HWP.
    iDestruct (envs_simple_replace_singleton_sound with "HΔ1") as "[HTR' HΔ']"=>//=.
    iCombine "HTR HTR'" as "HTR". iDestruct ("HΔ'" with "HTR") as "$".
  - iDestruct (envs_simple_replace_singleton_sound with "HΔ1") as "[HTRdup HΔ']"=>//.
    rewrite bi.intuitionistically_if_elim -bi.intuitionistically_intuitionistically_if.
    iDestruct "HTRdup" as "#>HTRdup".
    iApply (tick_spec with "[//] HTRdup")=>//. iIntros "!> [_ #HTRdup']". iApply HWP.
    rewrite Nat.add_comm. iDestruct ("HΔ'" with "[//]") as "$".
  - iMod (zero_TRdup with "Hinv") as "HTRdup"=>//.
    iApply (tick_spec with "[//] HTRdup")=>//. iIntros "!> [_ #HTRdup']". by iApply HWP.
Qed.

Ltac wp_tick ::=
  iStartProof ;
438
  simpl_trans ;
439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461
  lazymatch goal with
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
      first
        [ reshape_expr false e ltac:(fun K e' =>
            eapply (tac_wp_tick _ _ _ _ _ _ _ _ _ K)
          )
        | fail 1 "wp_tick: cannot find 'tick ?v' in" e ] ;
      [ try solve_ndisj
      | exact _
      | (* lookup invariant: *) (iAssumptionCore || fail "wp_tick: cannot find TR_invariant")
      | (* lookup TRdup: *) (
        left; eexists _, _, _; split;
        [iAssumptionCore | proofmode.reduction.pm_reflexivity]
        || right; reflexivity)
      | (* lookup TR:    *) (
        left; eexists _, _; split;
        [iAssumptionCore | proofmode.reduction.pm_reflexivity]
        || right; reflexivity)
      | wp_expr_simpl ]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
      fail "wp_tick is not implemented for twp"
  | _ => fail "wp_tick: not a 'wp'"
  end.