TimeCreditsAltProofs.v 14.5 KB
Newer Older
1
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
2 3
From iris.base_logic Require Import invariants.

4
From iris_time Require Import Auth_nat Reduction TimeCredits.
5 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.
Implicit Type m n : nat.
MEVEL Glen's avatar
MEVEL Glen committed
12 13
Implicit Type φ ψ : val  Prop.
Implicit Type Σ : gFunctors.
14 15

Local Notation γ := timeCreditHeapG_name.
16
Local Notation  := tick_counter.
17 18 19 20

(* In general, one can prove:
 *     if the translated program with the counter initialized to m is safe,
 *     then the source program is m-safe.
MEVEL Glen's avatar
MEVEL Glen committed
21
 * This is lemma [adequate_translation__nadequate] in `Simulation.v`.
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
 *
 * Moreover, for time credits, we can prove:
 *     if the translated program with the counter initialized to m is safe,
 *     then the source program computes in at most m steps.
 * This is lemma [safe_tctranslation__bounded] in `TimeCredits.v` (it relies
 * crucially on the unsafe behavior of “tick” for time credits).
 *
 * However, the combination of both results does not imply that the source
 * program is safe, because m-safety only describe sequences of reductions of
 * length strictly less than m, so we cannot tell what happens for sequences
 * of length exactly m.
 *
 * In `TimeCredits.v`, this is solved by proving that (roughly):
 *     if the Hoare triple  { TC m } «e» { φ }  holds,
 *     then FOR ALL m' ≥ m,
 *       the translated program with the counter initialized to m' is safe.
MEVEL Glen's avatar
MEVEL Glen committed
38
 * This is lemma [spec_tctranslation__adequate_translation] in `TimeCredits.v`.
39 40 41 42 43 44 45 46 47 48 49 50 51
 *
 * Hence from the Hoare triple we can deduce that the source program
 *   (1)  computes in at most m steps (by taking m' = m), and
 *   (2)  is (m+1)-safe (by taking m' = m+1),
 * which is enough to conclude that it is completely safe.
 *
 * However, this is not completely natural, because deducing (2) amounts to
 * giving the translated program one credit more than required.
 *
 * In fact, exploiting the unsafe behavior of “tick”, we can prove that:
 *     if the translated program with the counter initialized to m is safe,
 *     then the source program is safe.
 * The proof is given below. It is mostly a copy-paste of the general proof
MEVEL Glen's avatar
MEVEL Glen committed
52
 * of [adequate_translation__nadequate] in `Simulation.v`, with additional calls
53 54 55 56 57 58
 * to [safe_tctranslation__bounded] and one call to [not_safe_tick].
 *)

(* assuming the safety of the translated expression,
 * a proof that the original expression is safe. *)

59
Lemma safe_tctranslation__safe_here {Hloc : TickCounter} m e σ :
60 61 62 63
  loc_fresh_in_expr  e 
  safe «e» S«σ, m» 
  is_Some (to_val e)  reducible e σ.
Proof.
64
  intros Hfresh Hsafe.
65 66 67 68 69 70 71
  (* case analysis on whether e is a value… *)
  destruct (to_val e) as [ v | ] eqn:Hnotval.
  (* — if e is a value, then we get the result immediately: *)
  - left. eauto.
  (* — if e is not a value, then we show that it is reducible: *)
  - right.
    (* we decompose e into a maximal evaluation context K and a head-redex: *)
72 73 74 75 76 77 78 79 80 81 82
    pose proof (not_val_fill_active_item _ Hnotval) as He ; clear Hnotval.
    destruct He as [ (K & x & ->) |
                   [ (K & e1 & ->) |
                   [ (K & f & x & e1 & ->) |
                     (K & ki & v & -> & Hactive) ]]].
    (* — either e = Var x: *)
    + (* then Var x is stuck *)
      exfalso. eapply stuck_not_safe; [|done]. rewrite translation_fill.
      apply stuck_fill, head_stuck_stuck.
      { split; [done|]. intros ???? Hstep. inversion Hstep. }
      apply ectxi_language_sub_redexes_are_values=>-[] //.
83 84
    (* — either e = K[Fork e1]: *)
    + (* then we easily derive a reduction from e: *)
85 86 87 88
      eexists _, _, _, _. apply Ectx_step', ForkS.
    (* — either e = K[Rec f x e1]: *)
    + (* then we easily derive a reduction from e: *)
      eexists _, _, _, _. apply Ectx_step', RecS.
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120
    (* — or e = K[ki[v]] where ki is an active item: *)
    + (* it is enough to show that ki[v] is reducible: *)
      apply loc_fresh_in_expr_fill_inv in Hfresh ;
      rewrite -> translation_fill in Hsafe ; apply safe_fill_inv in Hsafe ;
      apply reducible_fill ;
      clear K.
      (* we deduce the reducibility of ki[v] from that of «ki»[«v»]: *)
      eapply active_item_translation_reducible ; [ done | done | ].
      (* remind that « ki[v] » = «ki»[tick «v»]: *)
      rewrite -> translation_fill_item_active in Hsafe ; last done.
      (* we have that «ki»[tick «v»] reduces to «ki»[«v»]
       * (thanks to the safety hypothesis, m ≥ 1 and ‘tick’ can be run): *)
      assert (
        prim_exec (fill_item Ki«ki» (tick V«v»)) S«σ, m»
                  (fill_item Ki«ki» V«v»)        S«σ, m-1» []
      ) as Hsteps % prim_exec_exec.
      {
        assert (fill [Ki«ki»] = fill_item Ki«ki») as E by reflexivity ; destruct E.
        apply prim_exec_fill. apply safe_fill_inv in Hsafe.
        (* This is where the unsafe behavior of “tick” is used: *)
        destruct m as [ | m ] ; first (exfalso ; eapply not_safe_tick, Hsafe).
        replace (S m - 1)%nat with m by lia.
        apply exec_tick_success.
      }
      (* using the safety of «ki»[tick «v»], we proceed by case analysis… *)
      eapply Hsafe in Hsteps as [ Hisval | Hred ] ; auto using elem_of_list_here.
      (* — either «ki»[«v»] is a value: this is not possible because ki is active. *)
      * simpl in Hisval. rewrite active_item_not_val in Hisval ;
        [ by apply is_Some_None in Hisval | by apply is_active_translationKi ].
      (* — or «ki»[«v»] reduces to something: this is precisely what we need. *)
      * exact Hred.
Qed.
121
Lemma safe_tctranslation__safe {Hloc : TickCounter} m e σ t2 σ2 e2 :
122 123 124
  loc_fresh_in_expr  e2 
  σ2 !!  = None 
  safe «e» S«σ, m» 
125
  rtc erased_step ([e], σ) (t2, σ2) 
126 127 128
  e2  t2 
  is_Some (to_val e2)  reducible e2 σ2.
Proof.
129
  intros He Hℓσ Hsafe [n Hnsteps] % rtc_nsteps He2.
130 131 132 133 134 135 136 137 138 139 140 141 142 143
  assert (n  m)%nat by by eapply safe_tctranslation__bounded.
  assert (safe «e2» S«σ2, m-n») as Hsafe2.
  {
    eapply safe_exec.
    - eapply elem_of_list_fmap_1. eassumption.
    - eassumption.
    - change [«e»] with T«[e]». apply simulation_exec_success' ; auto.
  }
  by eapply safe_tctranslation__safe_here.
Qed.

(* assuming the adequacy of the translated expression,
 * a proof that the original expression has adequate results. *)

MEVEL Glen's avatar
MEVEL Glen committed
144
Lemma adequate_tctranslation__adequate_result {Hloc : TickCounter} m φ e σ t2 σ2 v2 :
145
  σ2 !!  = None 
146
  adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v)) 
147
  rtc erased_step ([e], σ) (Val v2 :: t2, σ2) 
148 149
  φ v2.
Proof.
150
  intros Hfresh Hadq [n Hnsteps] % rtc_nsteps.
151 152
  assert (safe «e» S«σ, m») as Hsafe by by eapply safe_adequate.
  assert (n  m)%nat by by eapply safe_tctranslation__bounded.
153
  replace (φ v2) with ((φ  invtranslationV) (translationV v2))
154
    by (simpl ; by rewrite invtranslationV_translationV).
155
  eapply (adequate_result _ _ _ (λ v σ, φ (invtranslationV v))) ; first done.
156
  change [«e»%E] with T«[e]».
157
  replace (Val «v2» :: _) with (T«Val v2 :: t2») by done.
158 159 160 161 162
  eapply simulation_exec_success' ; eauto.
Qed.

(* now let’s combine the two results. *)

MEVEL Glen's avatar
MEVEL Glen committed
163
Lemma adequate_tctranslation__adequate m φ e σ :
164 165
  ( `{TickCounter}, adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v))) 
  adequate NotStuck e σ (λ v σ, φ v).
166
Proof.
167
  intros Hadq.
168 169 170 171
  split.
  (* (1) adequate result: *)
  - intros t2 σ2 v2 Hsteps.
    (* build a location ℓ which is not in the domain of σ2: *)
172
    pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
173 174 175 176 177 178 179 180
    assert (σ2 !!  = None)
      by (simpl ; eapply not_elem_of_dom, is_fresh).
    by eapply adequate_tctranslation__adequate_result.
  (* (2) safety: *)
  - intros t2 σ2 e2 _ Hsteps He2.
    (* build a location ℓ which is fresh in e2 and in the domain of σ2: *)
    pose (set1 := loc_set_of_expr e2 : gset loc).
    pose (set2 := dom (gset loc) σ2 : gset loc).
181
    pose (Build_TickCounter (fresh (set1  set2))) as Hloc.
182 183 184
    eassert (  set1  set2) as [H1 H2] % not_elem_of_union
      by (unfold  ; apply is_fresh).
    assert (loc_fresh_in_expr  e2)
185
      by by apply loc_not_in_set_is_fresh_in_expr.
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247
    assert (σ2 !!  = None)
      by by (simpl ; eapply not_elem_of_dom).
    specialize (Hadq Hloc) as Hsafe % safe_adequate.
    by eapply safe_tctranslation__safe.
Qed.



(* On the contrary, it is possible to get rid of the dependency upon the unsafe
 * behavior of “tick”.
 *
 * The fact that, for time credits, “tick” crashes when the counter is depleted,
 * is essential to prove the operational version of the main result: that the
 * safety of a translated program implies an upper bound on the running time of
 * the source program (lemma [safe_tctranslation__bounded] in `TimeCredits.v`).
 *
 * However, it is redundant from the logical point of view: because we give a
 * time credit to “tick” (in its Hoare specification [tick_spec]), the counter
 * is guaranteed not to be exhausted, and the crashing branch is dead code.
 *
 * Hence we may as well implement “tick” with a mere decrementation, whatever
 * the value of the counter is. If we do so, then we can strenghten the
 * simulation lemma as such:
 *     if (t₁, σ₁) reduces to (t₂, σ₂) in n steps,
 *     then for all (relative) integer m,
 *       («t₁», «σ₁»[ℓ:=m]) reduces to («t₂», «σ₂»[ℓ:=m−n]).
 * In other words, there is no need anymore for the initial value m of the
 * counter to be at least equal to n.
 *
 * Then, for that modified implementation of “tick”, we can prove:
 *     if the Hoare triple  { TC m } «e» { φ }  holds,
 *     then the source program computes in at most m steps.
 *
 * Whereas the proof which relies on the crashing behavior uses [wp_adequacy]
 * (the fact that the WP predicate is sound, that is, implies the safety/adequacy
 * of the program), this proof uses [wp_invariance] instead (the fact that the
 * WP predicate preserves invariants of the program).
 *
 * The idea of the proof is as follows: given a n-step reduction from (t₁, σ₁)
 * to (t₂, σ₂), the strenghtened simulation lemma gives a reduction from
 * («t₁», «σ₁»[ℓ:=m]) to («t₂», «σ₂»[ℓ:=m−n]). The invariant of time credits
 * in the final state implies that m−n is a non-negative integer; otherwise
 * said, n ≤ m.
 *)

Lemma gen_heap_ctx_mapsto {Σ : gFunctors} {Hgen : gen_heapG loc val Σ} (σ : state) (l : loc) (v v' : val) :
  σ !! l = Some v 
  gen_heap_ctx σ -
  l  v' -
  v = v'.
Proof.
  iIntros (Hσ) "Hheap Hl".
  rewrite /gen_heap_ctx /=.
  unfold mapsto ; destruct mapsto_aux as [_->] ; rewrite /mapsto_def /=.
  iDestruct (own_valid_2 with "Hheap Hl") as %H.
  iPureIntro.
  assert (CmraDiscrete (gen_heapUR loc val)) as Hdiscrete by apply _.
  apply ((auth_valid_discrete_2 (H:=Hdiscrete))) in H as [H _].
  apply gen_heap_singleton_included in H.
  pose proof (eq_stepl Hσ H) as E. by injection E.
Qed.

MEVEL Glen's avatar
MEVEL Glen committed
248
Lemma spec_tctranslation__bounded {Σ} m ψ e :
249
  ( `{timeCreditHeapG Σ},
MEVEL Glen's avatar
MEVEL Glen committed
250
    TC_invariant -
251 252
    {{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
  ) 
253
   `{TickCounter} `{timeCreditHeapPreG Σ} σ1 t2 σ2 (z : Z),
254
    rtc erased_step ([«e»], S«σ1, m») (T«t2», S«σ2, z») 
255 256 257 258 259
    0  z.
Proof.
  intros Hspec Hloc HtcPreG σ1 t2 σ2 z Hsteps.
  (* apply the invariance result. *)
  apply (wp_invariance Σ _ NotStuck «e» S«σ1,m» T«t2» S«σ2,z») ; simpl ; last assumption.
260
  intros HinvG κs κs'.
261
  (* … now we have to prove a WP for some state interpretation, for which
MEVEL Glen's avatar
MEVEL Glen committed
262
   * we settle the needed invariant TC_invariant. *)
263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282
  set σ' := S«σ1».
  (* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
  iMod (own_alloc ( to_gen_heap (<[ := #m]> σ')   to_gen_heap {[ := #m]}))
    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 m) as (γ) "[Hγ● Hγ◯]".
  (* packing all those bits, build the heap instance necessary to use time credits: *)
  destruct HtcPreG as [[HinvPreG [HgenHeapPreInG]] HinG] ; simpl ; clear HinvPreG.
  pose (Build_timeCreditHeapG Σ (HeapG Σ HinvG (GenHeapG _ _ Σ _ _ HgenHeapPreInG h)) HinG _ γ)
    as HtcHeapG.
  (* create the invariant: *)
MEVEL Glen's avatar
MEVEL Glen committed
283
  iAssert (|={}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> #Hinv".
284 285 286 287 288 289 290 291
  {
    iApply inv_alloc.
    iExists m.
    unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl.
    unfold to_gen_heap ; rewrite fmap_insert fmap_empty insert_empty.
    by iFrame.
  }
  (* finally, use the user-given specification: *)
292
  iModIntro. iExists (λ σ _ _, gen_heap_ctx σ), (λ _, True)%I. iFrame "Hh●".
293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309
  iSplitL ; first (iApply (Hspec with "Hinv Hγ◯") ; auto).
  (* it remains to prove that the interpretation of the final state, along
   * with the invariant, implies the inequality… *)
  iIntros "Hheap2".
  (* open the invariant: *)
  iInv timeCreditN as (m') ">[Hc Hγ●]" "InvClose".
  (* derive that z = m' (that is, the relative integer is in fact a natural integer): *)
  iDestruct (gen_heap_ctx_mapsto with "Hheap2 Hc") as %Eq ; first (by apply lookup_insert) ;
  injection Eq as ->.
  (* close the invariant (in fact, this is not required): *)
  iMod ("InvClose" with "[-]") as "_" ; first by auto with iFrame.
  (* conclude: *)
  iMod (fupd_intro_mask'  ) as "_" ; first done. iPureIntro.
  lia.
Qed.

(* The simulation lemma with no assumption that m ≤ n. *)
310
Axiom simulation_exec_alt :  {Hloc : TickCounter} m n t1 σ1 t2 σ2,
311
  σ2 !!  = None 
312 313
  nsteps erased_step m (t1, σ1) (t2, σ2) 
  rtc erased_step (T«t1», S«σ1, n») (T«t2», S«σ2, (n-m)%Z»).
314

MEVEL Glen's avatar
MEVEL Glen committed
315
Lemma spec_tctranslation__bounded' {Σ} m ψ e :
316
  ( `{timeCreditHeapG Σ},
MEVEL Glen's avatar
MEVEL Glen committed
317
    TC_invariant -
318 319 320 321 322
    {{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
  ) 
   `{!timeCreditHeapPreG Σ} σ,
    bounded_time e σ m.
Proof.
323
  intros Hspec HtcPreG σ t2 σ2 n Hnsteps.
324
  (* build a location ℓ which is not in the domain of σ2: *)
325
  pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
326 327 328 329 330
  assert (σ2 !!  = None)
    by (unfold  ; eapply not_elem_of_dom, is_fresh).
  eapply simulation_exec_alt in Hnsteps ; auto.
  assert (0  m-n)%Z by by eapply spec_tctranslation__bounded.
  lia.
331
Qed.