Prove soundness of Combined.v

theories/Combined.v

-(* TEMPORARY:
- * This file is far from being complete. It only addresses the case when
- * max_tc < max_tr, and soundness is not done yet. Definitions will change.
- * It does provide a (hopefully) workable interface for proving programs with
- * time credits and time receipts, including proof-mode tactics.
- *)
-
 From iris_time.heap_lang Require Import proofmode notation adequacy lang.
 From iris.base_logic Require Import invariants.
 
@@ -65,6 +58,8 @@ Class tctrHeapPreG Σ := {
   tctrHeapPreG_inG_TRdup :> inG Σ (authR mnatUR) ;
 }.
 
+Class UseTC := useTC : bool.
+
 Class tctrHeapG Σ := {
   tctrHeapG_heapG :> heapG Σ ;
   tctrHeapG_inG_TC    :> inG Σ (authR natUR) ;
@@ -74,6 +69,7 @@ Class tctrHeapG Σ := {
   tctrHeapG_name_TC    : gname ;
   tctrHeapG_name_TR    : gname ;
   tctrHeapG_name_TRdup : gname ;
+  tctrHeapG_useTC      :> UseTC ;
 }.
 
 Local Notation γ := tctrHeapG_name_TC.
@@ -89,39 +85,46 @@ Local Notation ℓ := tick_counter.
 
 
 
-(* This code is irrelevant for tick_spec but has to be unsafe for proving
- * the safety theorem: *)
 Definition fail : val :=
   λ: <>, #() #().
 
-Global Instance credits_tick {_:TickCounter} : Tick :=
-  generic_tick fail.
+Definition loop : val :=
+  rec: "f" <> := "f" #().
+
+Global Instance tctr_tick {_:TickCounter} {_:UseTC} : Tick :=
+  generic_tick (if useTC then fail else loop).
 
 
 
 Section Definitions.
 
   Context `{tctrHeapG Σ}.
-  Context (max_tc max_tr : nat).
-  Context {Ineq : max_tc < max_tr}.
 
   Definition TC (n : nat) : iProp Σ :=
-    own γ (◯nat n).
+    if useTC then own γ (◯nat n) else True%I.
 
   Lemma TC_plus m n :
     TC (m + n) ≡ (TC m ∗ TC n)%I.
-  Proof using. by rewrite /TC auth_frag_op own_op. Qed.
+  Proof using.
+    rewrite /TC ; destruct useTC.
+    - by rewrite auth_frag_op own_op.
+    - by iStartProof.
+  Qed.
   Lemma TC_succ n :
     TC (S n) ≡ (TC 1%nat ∗ TC n)%I.
   Proof using. by rewrite (eq_refl : S n = 1 + n)%nat TC_plus. Qed.
   Lemma TC_weaken (n₁ n₂ : nat) :
     (n₂ ≤ n₁)%nat →
     TC n₁ -∗ TC n₂.
-  Proof using. apply own_auth_nat_weaken. Qed.
+  Proof using.
+    rewrite /TC ; destruct useTC.
+    - by apply own_auth_nat_weaken.
+    - done.
+  Qed.
 
   Lemma TC_timeless n :
     Timeless (TC n).
-  Proof using. exact _. Qed.
+  Proof using. rewrite /TC ; destruct useTC ; exact _. Qed.
 
   (* We give higher priorities to the (+) instances so that the (S n)
      instances are not chosen when m is a constant. *)
@@ -156,7 +159,6 @@ Section Definitions.
     Timeless (TR n).
   Proof using. exact _. Qed.
 
-
   (* We give higher priorities to the (+) instances so that the (S n)
      instances are not chosen when m is a constant. *)
   Global Instance into_sep_TR_plus m n : IntoSep (TR (m + n)) (TR m) (TR n) | 0.
@@ -190,20 +192,23 @@ Section Definitions.
 
   Definition tctrN := nroot .@ "combinedTimeCreditTimeReceipt".
 
+  Context (max_tr : nat).
+
   Definition TCTR_invariant : iProp Σ :=
     inv tctrN (
       ∃ (m:nat),
-        ⌜(m ≤ max_tc)%nat⌝
+        ⌜(m < max_tr)%nat⌝
       ∗ ℓ ↦ #m
-      ∗ own γ (●nat m)
-      ∗ own γ1 (●nat (max_tc - m))
-      ∗ own γ2 (●mnat (max_tc - m))
+      ∗ (if useTC then own γ (●nat m) else True)
+      ∗ own γ1 (●nat (max_tr - 1 - m))
+      ∗ own γ2 (●mnat (max_tr - 1 - m))
     )%I.
 
   Lemma zero_TC E:
     ↑tctrN ⊆ E →
     TCTR_invariant ={E}=∗ TC 0.
   Proof using.
+    rewrite /TC /TCTR_invariant ; destruct useTC ; last by auto.
     iIntros (?) "#Htickinv".
     iInv tctrN as (m) ">(? & ? & H● & ?)" "InvClose".
     iDestruct (own_auth_nat_null with "H●") as "[H● $]".
@@ -215,7 +220,7 @@ Section Definitions.
     TCTR_invariant ={E}=∗ TR 0.
   Proof using.
     iIntros (?) "#Htickinv".
-    iInv tctrN as (m) ">(? & ? & ? & Hγ1● & ?)" "InvClose".
+    iInv tctrN as (m) "(>? & >? & ? & >Hγ1● & >?)" "InvClose".
     iDestruct (own_auth_nat_null with "Hγ1●") as "[Hγ1● $]".
     iApply "InvClose" ; eauto with iFrame.
   Qed.
@@ -225,7 +230,7 @@ Section Definitions.
     TCTR_invariant ={E}=∗ TRdup 0.
   Proof using.
     iIntros (?) "#Htickinv".
-    iInv tctrN as (m) ">(? & ? & ? & ? & Hγ2●)" "InvClose".
+    iInv tctrN as (m) "(>? & >? & ? & >? & >Hγ2●)" "InvClose".
     iDestruct (own_auth_mnat_null with "Hγ2●") as "[Hγ2● $]".
     iApply "InvClose" ; eauto with iFrame.
   Qed.
@@ -233,16 +238,16 @@ Section Definitions.
   Lemma TR_nmax_absurd (E : coPset) :
     ↑tctrN ⊆ E →
     TCTR_invariant -∗ TR max_tr ={E}=∗ False.
-  Proof using Ineq.
+  Proof using.
     iIntros (?) "#Inv Hγ1◯".
-    iInv tctrN as (m) ">(I & _ & _ & Hγ1● & _)" "InvClose" ; iDestruct "I" as %I.
+    iInv tctrN as (m) "(>I & _ & _ & >Hγ1● & _)" "InvClose" ; iDestruct "I" as %I.
     iDestruct (own_auth_nat_le with "Hγ1● Hγ1◯") as %I'.
     exfalso ; lia.
   Qed.
   Lemma TR_lt_nmax n (E : coPset) :
     ↑tctrN ⊆ E →
     TCTR_invariant -∗ TR n ={E}=∗ TR n ∗ ⌜n < max_tr⌝%nat.
-  Proof using Ineq.
+  Proof using.
     iIntros (?) "#Inv Hγ1◯".
     destruct (le_lt_dec max_tr n) as [ I | I ] ; last by iFrame.
     iDestruct (TR_weaken n max_tr with "Hγ1◯") as "Hγ1◯" ; first done.
@@ -253,16 +258,16 @@ Section Definitions.
   Lemma TRdup_nmax_absurd (E : coPset) :
     ↑tctrN ⊆ E →
     TCTR_invariant -∗ TRdup max_tr ={E}=∗ False.
-  Proof using Ineq.
+  Proof using.
     iIntros (?) "#Inv Hγ2◯".
-    iInv tctrN as (m) ">(I & _ & _ & _ & Hγ2●)" "InvClose" ; iDestruct "I" as %I.
+    iInv tctrN as (m) "(>I & _ & _ & _ & >Hγ2●)" "InvClose" ; iDestruct "I" as %I.
     iDestruct (own_auth_mnat_le with "Hγ2● Hγ2◯") as %I'.
     exfalso ; lia.
   Qed.
   Lemma TRdup_lt_nmax n (E : coPset) :
     ↑tctrN ⊆ E →
     TCTR_invariant -∗ TRdup n ={E}=∗ TRdup n ∗ ⌜n < max_tr⌝%nat.
-  Proof using Ineq.
+  Proof using.
     iIntros (?) "#Inv Hγ1◯".
     destruct (le_lt_dec max_tr n) as [ I | I ] ; last by iFrame.
     iDestruct (TRdup_weaken n max_tr with "Hγ1◯") as "Hγ1◯" ; first done.
@@ -273,59 +278,77 @@ Section Definitions.
   Lemma TR_TRdup (E : coPset) n :
     ↑tctrN ⊆ E →
     TCTR_invariant -∗ TR n ={E}=∗ TR n ∗ TRdup n.
-  Proof using max_tr.
+  Proof using.
     iIntros (?) "#Inv Hγ1◯".
-    iInv tctrN as (m) ">(I & Hℓ & Hγ● & Hγ1● & Hγ2●)" "InvClose".
+    iInv tctrN as (m) "(>I & >Hℓ & Hγ● & >Hγ1● & >Hγ2●)" "InvClose".
     iDestruct (own_auth_nat_le with "Hγ1● Hγ1◯") as %I'.
     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 (_ : (max_tc-m)%nat = (max_tc-m)%nat `max` n) ; last lia.
+      rewrite (_ : (max_tr-1-m)%nat = (max_tr-1-m)%nat `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.
+
   Theorem tick_spec s E (v : val) n :
     ↑tctrN ⊆ E →
     TCTR_invariant -∗
     {{{ ▷ TC 1 ∗ ▷ TRdup n }}} tick v @ s ; E {{{ RET v ; TR 1 ∗ TRdup (n+1) }}}.
-  Proof using max_tr.
+  Proof using.
     intros ?. iIntros "#Inv" (Ψ) "!# [Hγ◯ Hγ2◯] HΨ".
     iLöb as "IH".
     wp_lam.
     (* open the invariant, in order to read the value m of location ℓ: *)
     wp_bind (! _)%E ;
-    iInv tctrN as (m) ">(I & Hℓ & Hγ● & Hγ1● & Hγ2●)" "InvClose".
+    iInv tctrN as (m) "(>I & >Hℓ & Hγ● & >Hγ1● & >Hγ2●)" "InvClose".
     wp_load.
-    (* deduce that m ≥ 1, because we hold a time credit: *)
-    iDestruct (own_auth_nat_le with "Hγ● Hγ◯") as %J.
+    (* in the case where we are using time credits, deduce that m ≥ 1,
+       because we hold a time credit: *)
+    iAssert (⌜useTC = true⌝ -∗ ⌜1 ≤ m⌝)%I%nat with "[Hγ● Hγ◯]" as "#J".
+    {
+      rewrite /TC ; iIntros "->".
+      by iApply (own_auth_nat_le with "Hγ● Hγ◯").
+    }
     (* close the invariant: *)
     iMod ("InvClose" with "[ I Hℓ Hγ● Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ].
     wp_let.
     (* test whether m ≤ 0: *)
-    wp_op ; destruct (bool_decide (m ≤ 0)) eqn:J' ; wp_if.
-    (* — if m ≤ 0 then this is absurd, because we hold a time credit: *)
-    - apply Is_true_eq_left, bool_decide_spec in J'.
+    wp_op. case_bool_decide as J' ; wp_if.
+    (* — if m ≤ 0: *)
+    - destruct useTC.
+      (* if we use TC, then m ≤ 0 is absurd, because we hold a time credit: *)
+      + iDestruct ("J" with "[//]") as %J.
         exfalso ; lia.
+      (* if we don’t, then we loop indefinitely, which gives us any spec we want
+         (because we are reasoning in partial correctness): *)
+      + iApply loop_spec.
     (* — otherwise: *)
-    - clear J'.
-      wp_op.
+    - wp_op.
       (* open the invariant again, in order to perform CAS on location ℓ: *)
       wp_bind (CAS _ _ _)%E ;
-(*       iInv timeCreditN as (n') ">(Hℓ & Hγ●)" "InvClose". *)
-      iInv tctrN as (m') ">(I & Hℓ & Hγ● & Hγ1● & Hγ2●)" "InvClose".
-      (* test whether the value ℓ is still k, by comparing m with m': *)
+      iInv tctrN as (m') "(>I & >Hℓ & Hγ● & >Hγ1● & >Hγ2●)" "InvClose".
+      (* test whether the value ℓ is still m, by comparing m with m': *)
       destruct (nat_eq_dec m m') as [ <- | Hneq ].
       (* — if it holds, then CAS succeeds and ℓ is decremented: *)
       + wp_cas_suc.
         (* reform the invariant with m−1 instead of m: *)
         replace (Z.of_nat m - 1) with (Z.of_nat (m - 1)%nat) by lia.
-        iMod (auth_nat_update_decr _ _ _ 1 with "Hγ● Hγ◯") as "[Hγ● Hγ◯]" ; first done.
+        iAssert (|==> if useTC then own γ (●nat (m-1)) else True)%I with "[Hγ● Hγ◯]" as ">Hγ●".
+        {
+          rewrite /TC ; destruct useTC ; last done.
+          by iMod (auth_nat_update_decr _ _ _ 1 with "Hγ● Hγ◯") as "[$ _]".
+        }
         iMod (auth_nat_update_incr _ _ 1 with "Hγ1●") as "[Hγ1● Hγ1◯]" ; simpl.
         iMod (auth_mnat_update_incr' _ _ _ 1 with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]" ; simpl.
         iDestruct "I" as %I.
-        replace (max_tc - m + 1)%nat with (max_tc - (m - 1))%nat by lia.
-        assert ((m-1) ≤ max_tc)%nat by lia.
+        replace (max_tr - 1 - m + 1)%nat with (max_tr - 1 - (m - 1))%nat by lia.
+        assert ((m-1) < max_tr)%nat by lia.
         (* close the invariant: *)
         iMod ("InvClose" with "[ Hℓ Hγ● Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ].
         (* finish: *)
@@ -342,13 +365,13 @@ Section Definitions.
   Theorem tick_spec_simple v n :
     TCTR_invariant -∗
     {{{ TC 1 ∗ TRdup n }}} tick v {{{ RET v ; TR 1 ∗ TRdup (n+1) }}}.
-  Proof using max_tr.
+  Proof using.
     iIntros "#Hinv" (Ψ) "!# [ HTC HTR ] HΨ".
     by iApply (tick_spec with "Hinv [$HTC $HTR] HΨ").
   Qed.
 
   Lemma TC_implementation : TCTR_invariant -∗ TCTR_interface TC max_tr TR TRdup.
-  Proof using Ineq.
+  Proof using.
     iIntros "#Hinv". repeat iSplitR.
     - iPureIntro. by apply TC_timeless.
     - by iApply (zero_TC with "Hinv").
@@ -398,7 +421,7 @@ Proof.
     iDestruct (envs_lookup_sound _ i false with "HΔ") as "[? _]"=>//. }
   iDestruct (into_laterN_env_sound with "HΔ") as "HΔ1"=>//.
   iDestruct (envs_simple_replace_singleton_sound with "HΔ1") as "[HTC HΔ2]"=>//=.
-  iDestruct "HTC" as "[>HTC HTC']". iDestruct ("HΔ2" with "HTC'") as "HΔ2".
+  iDestruct "HTC" as "[HTC HTC']". iDestruct ("HΔ2" with "HTC'") as "HΔ2".
   iApply wp_bind.
   destruct HTR as [(j & n' & HTR1 & HTR2)| ->],
            HTRdup as [(j' & pe'' & p & HTRDup1 & HTRDup2)| ->].
@@ -453,13 +476,474 @@ Ltac wp_tick ::=
   | _ => fail "wp_tick: not a 'wp'"
   end.
 
-Example test `{tctrHeapG Σ} :
-  TCTR_invariant 100 -∗
-  TC 37 -∗
-  TRdup 63%nat -∗
-  TR 0 -∗
-  WP tick #0 {{ _, True }}.
-Proof using.
-  iIntros "#Inv HTC HTRdup HTR".
-  wp_tick.
-Abort.
+
+
+(*
+ * Simulation
+ *)
+
+Section Simulation.
+
+  (* Simulation in the “successful” case. *)
+
+  Context {Hloc : TickCounter}.
+  Context {useTC : UseTC}.
+
+  Lemma exec_tick_success n v σ :
+    prim_exec  (tick v) (<[ℓ := #(S n)]> σ)  v (<[ℓ := #n]> σ)  [].
+  Proof. by apply exec_tick_success. Qed.
+
+  Definition simulation_exec_success := simulation_exec_success (if useTC then fail else loop).
+  Definition simulation_exec_success' := simulation_exec_success' (if useTC then fail else loop).
+
+  (* Simulation in the “failing” case. *)
+
+  Context (HuseTC : useTC = true).
+
+  Lemma not_safe_tick v σ :
+    ¬ safe (tick v) (<[ℓ := #0]> σ).
+  Proof.
+    assert (prim_exec  (tick v) (<[ℓ := #0]> σ)  (#() #()) (<[ℓ := #0]> σ)  []) as Hexec.
+    {
+      unlock tick tctr_tick generic_tick fail ; rewrite HuseTC.
+      eapply prim_exec_cons_nofork.
+      { by prim_step. }
+      simpl. eapply prim_exec_cons_nofork.
+      { prim_step. apply lookup_insert. }
+      simpl. eapply prim_exec_cons_nofork.
+      { prim_step. }
+      simpl. eapply prim_exec_cons_nofork.
+      { by prim_step. }
+      simpl. eapply prim_exec_cons_nofork.
+      { by prim_step. }
+      simpl. eapply prim_exec_cons_nofork.
+      { by prim_step. }
+      simpl. eapply prim_exec_cons_nofork.
+      { by prim_step. }
+      simpl. apply prim_exec_nil.
+    }
+    assert (¬ safe (#() #()) (<[ℓ := #0]> σ)) as Hnotsafe.
+    {
+      apply stuck_not_safe, head_stuck_stuck, ectxi_language_sub_redexes_are_values.
+      - split ; first done. inversion 1.
+      - intros [] ; try discriminate 1 ; inversion 1 ; by eauto.
+    }
+    intros Hsafe. eapply Hnotsafe, safe_exec_nofork, prim_exec_exec ; eassumption.
+  Qed.
+
+  Local Ltac not_safe_tick :=
+    lazymatch goal with
+    | |- ¬ safe ?e _ =>
+        reshape_expr false e ltac:(fun K e' =>
+          apply not_safe_fill' with K e' ; first reflexivity ;
+          eapply not_safe_tick
+        )
+    end ;
+    done.
+
+  Lemma simulation_head_step_failure e1 σ1 κ e2 σ2 efs :
+    head_step e1 σ1 κ e2 σ2 efs →
+    ¬ safe «e1» S«σ1, 0».
+  Proof.
+    destruct 1 as
+      [(* RecS *) f x e σ
+      | | | | | | | | | | | |
+      | (* ForkS *) e1 σ
+      | | | | | | ] ;
+    simpl_trans ;
+    try not_safe_tick.
+    (* RecS f x e σ : *)
+    - eapply not_safe_prim_step ; last prim_step.
+      not_safe_tick.
+    (* ForkS e σ : *)
+    - eapply not_safe_prim_step ; last prim_step.
+      not_safe_tick.
+  Qed.
+
+  Lemma simulation_prim_step_failure e1 σ1 κ e2 σ2 efs :
+    prim_step e1 σ1 κ e2 σ2 efs →
+    ¬ safe «e1» S«σ1, 0».
+  Proof.
+    intros [ K e1' e2' -> -> H ].
+    rewrite translation_fill.
+    by eapply not_safe_fill, simulation_head_step_failure.
+  Qed.
+
+  Lemma simulation_step_failure t1 σ1 κ t2 σ2 :
+    step (t1, σ1) κ (t2, σ2) →
+    ∃ e1, e1 ∈ t1 ∧
+    ¬ safe «e1» S«σ1, 0».
+  Proof.
+    intros [e1 σ1_ e2 σ2_ efs t t' E1 E2 Hstep] ;
+    injection E1 as -> <- ; injection E2 as -> <-.
+    exists e1 ; split ; first set_solver.
+    by eapply simulation_prim_step_failure.
+  Qed.
+
+  Local Lemma simulation_exec_failure_now n t1 σ1 t2 σ2 :
+    nsteps erased_step (S n) (t1, σ1) (t2, σ2) →
+    ∃ e1, e1 ∈ t1 ∧
+    ¬ safe «e1» S«σ1, 0».
+  Proof.
+    make_eq (S n) as Sn En.
+    make_eq (t1, σ1) as config1 E1.
+    destruct 1 as [ ? | ? ? [] ? [? ?] _ ], E1.
+    - discriminate En.
+    - by eapply simulation_step_failure.
+  Qed.
+
+  Lemma simulation_exec_failure m n e1 σ1 t2 σ2 :
+    σ2 !! ℓ = None →
+    nsteps erased_step (m + S n) ([e1], σ1) (t2, σ2) →
+    ¬ safe «e1» S«σ1, m».
+  Proof.
+    intros Hℓ Hnsteps.
+    assert (
+      ∃ t3 σ3,
+        rtc erased_step (T«[e1]», S«σ1, m») (T«t3», S«σ3, 0») ∧
+        ∃ e3, e3 ∈ t3 ∧
+        ¬ safe «e3» S«σ3, 0»
+    ) as (t3 & σ3 & Hsteps & e3 & E3 & Hsafe).
+    {
+      apply nsteps_split in Hnsteps as ((t3, σ3) & Hnsteps1to3 & Hnsteps3to2).
+      exists t3, σ3 ; repeat split.
+      - assert (σ3 !! ℓ = None) by (eapply loc_fresh_in_dom_nsteps ; cycle 1 ; eassumption).
+        replace m with (m+0)%nat by lia.
+        apply simulation_exec_success ; assumption.
+      - by eapply simulation_exec_failure_now.
+    }
+    apply (elem_of_list_fmap_1 translation) in E3.
+    eapply not_safe_exec ; eassumption.
+  Qed.
+
+End Simulation.
+
+
+
+(*
+ * Soundness
+ *)
+
+Section Soundness.
+
+(** Part of the proof of soundness which is specific to the case where
+ ** time credits are used (m < max_tr). **)
+
+  (* assuming the safety of the translated expression,
+   * a proof that the computation time of the original expression is bounded. *)
+
+  Local Lemma gt_sum m n :
+    (m > n)%nat → ∃ (k : nat), m = (n + S k)%nat.
+  Proof.
+    intro. exists (m - S n)%nat. lia.
+  Qed.
+
+  Lemma safe_tctranslation__bounded {Hloc : TickCounter} {useTC : UseTC} m e σ t2 σ2 n :
+    useTC = true →
+    σ2 !! ℓ = None →
+    safe «e» S«σ, m» →
+    nsteps erased_step n ([e], σ) (t2, σ2) →
+    (n ≤ m)%nat.
+  Proof.
+    intros HuseTC Hfresh Hsafe Hnsteps.
+    (* reasoning by contradiction: assume (n > m), ie. (n = m + S k) for some k: *)
+    apply not_gt ; intros [k ->] % gt_sum.
+    (* apply the simulation lemma: *)
+    by eapply simulation_exec_failure.
+  Qed.
+
+  (* assuming the safety of the translated expression,
+   * a proof that the original expression is safe. *)
+
+  Lemma safe_tctranslation__safe_here {Hloc : TickCounter} {useTC : UseTC} m e σ :
+    useTC = true →
+    loc_fresh_in_expr ℓ e →
+    safe «e» S«σ, m» →
+    is_Some (to_val e) ∨ reducible e σ.
+  Proof.
+    intros HuseTC Hfresh Hsafe.
+    (* 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: *)
+      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=>-[] //.
+      (* — either e = K[Fork e1]: *)
+      + (* then we easily derive a reduction from e: *)
+        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.
+      (* — 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 ; eassumption).
+          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.
+
+  Lemma safe_tctranslation__safe {Hloc : TickCounter} {useTC : UseTC} m e σ t2 σ2 e2 :
+    useTC = true →
+    loc_fresh_in_expr ℓ e2 →
+    σ2 !! ℓ = None →
+    safe «e» S«σ, m» →
+    rtc erased_step ([e], σ) (t2, σ2) →
+    e2 ∈ t2 →
+    is_Some (to_val e2) ∨ reducible e2 σ2.
+  Proof.
+    intros HuseTC Hℓe Hℓσ Hsafe [n Hnsteps] % rtc_nsteps He2.
+    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. *)
+
+  Lemma adequate_tctranslation__adequate_result {Hloc : TickCounter} {useTC : UseTC} m φ e σ t2 σ2 v2 :
+    useTC = true →
+    σ2 !! ℓ = None →
+    adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v)) →
+    rtc erased_step ([e], σ) (Val v2 :: t2, σ2) →
+    φ v2.
+  Proof.
+    intros HuseTC Hfresh Hadq [n Hnsteps] % rtc_nsteps.
+    assert (safe «e» S«σ, m») as Hsafe by by eapply safe_adequate.
+    assert (n ≤ m)%nat by by eapply safe_tctranslation__bounded.
+    replace (φ v2) with ((φ ∘ invtranslationV) (translationV v2))
+      by (simpl ; by rewrite invtranslationV_translationV).
+    eapply (adequate_result _ _ _ (λ v σ, φ (invtranslationV v))) ; first done.
+    change [«e»%E] with T«[e]».
+    replace (Val «v2» :: _) with (T«Val v2 :: t2») by done.
+    eapply simulation_exec_success' ; eauto.
+  Qed.
+
+  (* now let’s combine the three results. *)
+
+  Lemma adequate_tctranslation__adequate_and_bounded m φ e σ :
+    let useTC : UseTC := true in
+    (∀ `{TickCounter}, adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v))) →
+    adequate NotStuck e σ (λ v σ, φ v)  ∧  bounded_time e σ m.
+  Proof.
+    intros useTC Hadq.
+    split ; first split.
+    (* (1) adequate result: *)
+    - intros t2 σ2 v2 Hsteps.
+      (* build a location ℓ which is not in the domain of σ2: *)
+      pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
+      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).
+      pose (Build_TickCounter (fresh (set1 ∪ set2))) as Hloc.
+      eassert (ℓ ∉ set1 ∪ set2) as [Hℓ1 Hℓ2] % not_elem_of_union
+        by (unfold ℓ ; apply is_fresh).
+      assert (loc_fresh_in_expr ℓ e2)
+        by by apply loc_not_in_set_is_fresh_in_expr.
+      assert (σ2 !! ℓ = None)
+        by by (simpl ; eapply not_elem_of_dom).
+      specialize (Hadq Hloc) as Hsafe % safe_adequate.
+      by eapply safe_tctranslation__safe.
+    (* (3) bounded time: *)
+    - intros t2 σ2 k.
+      (* build a location ℓ which is not in the domain of σ2: *)
+      pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
+      assert (σ2 !! ℓ = None)
+        by (unfold ℓ ; eapply not_elem_of_dom, is_fresh).
+      specialize (Hadq Hloc) as Hsafe % safe_adequate.
+      by eapply safe_tctranslation__bounded.
+  Qed.
+
+(** Part of the proof of soundness which is specific to the case where
+ ** time credits are not used (m ≥ max_tr). **)
+
+  (* assuming the adequacy of the translated expression,
+   * a proof that the original expression is n-adequate. *)
+
+  Definition adequate_trtranslation__nadequate := adequate_translation__nadequate loop.
+
+(** Part of the proof which is common to both cases. **)
+
+  (* from a Hoare triple in Iris,
+   * derive the adequacy of the translated expression. *)
+
+  Lemma spec_tctranslation__adequate_translation {Σ} max_tr m ψ e :
+    (0 < max_tr)%nat →
+    (∀ `{tctrHeapG Σ},
+      TCTR_invariant max_tr -∗
+      {{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v⌝ }}}
+    ) →
+    ∀ `{tctrHeapPreG Σ} `{TickCounter} σ,
+      let useTC : UseTC := bool_decide (m < max_tr)%nat in
+      let M : nat := min m (max_tr-1) in
+      adequate NotStuck «e» S«σ,M» (λ v σ, ψ v).
+  Proof.
+    intros Imax_tr Hspec HpreG Hloc σ useTC M.
+    assert (M ≤ m)%nat by (unfold M ; lia).
+    assert (M < max_tr)%nat by (unfold M ; lia).
+    (* apply the adequacy results. *)
+    apply (wp_adequacy _ _) ; simpl ; intros HinvG.
+    (* … 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 (<[ℓ := #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 ℓ: *)
+    iAssert (|==> ∃ γ,
+        (if useTC then own γ (● M) else True)
+      ∗ (if useTC then own γ (◯ m) else True)
+    )%I as "Hγalloc".
+    {
+      rewrite /useTC ; case_bool_decide ; last done.
+      rewrite (_ : M = m) ; last by (rewrite /M ; lia).
+      iMod (auth_nat_alloc m) as (γ) "[Hγ● Hγ◯]".
+      auto with iFrame.
+    }
+    iMod "Hγalloc" as (γ) "[Hγ● Hγ◯]".