diff --git a/theories/examples/refinements/derived.v b/theories/examples/refinements/derived.v
index e8ce3e1c39e50c5f518f1cd2776bb168c220e73d..c11627bc88c6921afdcebc7c051f6ec0e330bfe3 100644
--- a/theories/examples/refinements/derived.v
+++ b/theories/examples/refinements/derived.v
@@ -18,6 +18,7 @@ Section derived.
   (at level 20, P, e, Q at level 200, format "⟨⟨  P  ⟩ ⟩  e  ⟨⟨  v ,  Q  ⟩ ⟩") : stdpp_scope.
   Notation "{{ P } } e {{ v , Q } }" := (□ (P -∗ SEQ e ⟨⟨ v, Q ⟩⟩))%I
   (at level 20, P, e, Q at level 200, format "{{  P  } }  e  {{  v ,  Q  } }") : stdpp_scope.
+  Notation "'|==>src' P" := (weak_src_update ⊤ P)%I (at level 99) : stdpp_scope.
 
 
   Lemma Value (v: val): (⊢ {{True}} v {{w, ⌜v = w⌝}})%I.
@@ -114,11 +115,229 @@ Section derived.
     (∀ x :X, {{P x ∗ ▷ (∀ x, {{P x}} e {{v, Q x v}})}} e {{ v, Q x v}})
     ⊢ ∀ x, {{ P x }} e {{v, Q x v}}.
   Proof.
-    iIntros "H". iApply bi.löb.
+    iIntros "#H". iApply bi.löb.
     iIntros "#H1" (x).
-    (*iIntros "H0".*)
-    (*iSpecialize ("H" with x). *)
-    (*iApply ("H"). iModIntro.*)
-  Abort.
+    iModIntro. iIntros "HP". iApply "H".
+    iFrame "#". iFrame.
+  Qed.
+
+
+  (* Extended Refinement Program Logic of Transfinite Iris *)
+  Lemma value_tgt_tpr (v: val): (⊢ {{True}} v {{w, ⌜v = w⌝}})%I.
+  Proof.
+    iIntros "!> _ $". by iApply rwp_value.
+  Qed.
+
+
+  Lemma bind_tgt_tpr (e: expr) K P Q R:
+    ({{P}} e {{v, Q v}} ∗ (∀ v: val, ({{Q v}} fill K (Val v) {{w, R w}}))
+    ⊢ {{P}} fill K e {{v, R v}})%I.
+  Proof.
+    iIntros "[#H1 #H2] !> P Hna".
+    iApply rwp_bind. iSpecialize ("H1" with "P Hna").
+    iApply (rwp_strong_mono with "H1 []"); auto.
+    iIntros (v) "[Hna Q] !>". iApply ("H2" with "Q Hna").
+  Qed.
+
+  Lemma pure_tgt_tpr (e e': expr) P Q: pure_step e e' → ({{P}} e' {{v, Q v}} ⊢ ⟨⟨P⟩⟩ e ⟨⟨v, Q v⟩⟩)%I.
+  Proof.
+    iIntros (Hstep) "#H !> P Hna".
+    iApply (ref_lifting.rswp_pure_step_later _ _ _ _ _ True); [|done|by iApply ("H" with "P Hna")].
+    intros _. apply nsteps_once, Hstep.
+  Qed.
+
+
+  Lemma pure_src_tpr (e e' et: expr) K P Q:
+    to_val et = None
+    → pure_step e e'
+    → (⟨⟨src (fill K e') ∗ P⟩⟩ et ⟨⟨v, Q v⟩⟩ ⊢ {{src (fill K e) ∗ ▷ P}} et {{v, Q v}})%I.
+  Proof.
+    iIntros (Hexp Hstep) "#H !> [Hsrc P] Hna". iApply (rwp_take_step with "[P Hna] [Hsrc]"); first done; last first.
+    - iApply step_pure; last iApply "Hsrc". apply pure_step_ctx; last done. apply _.
+    - iIntros "Hsrc'". iApply rswp_do_step. iNext. iApply ("H" with "[$P $Hsrc'] Hna").
+  Qed.
+
+
+  Lemma store_tgt_tpr l (v1 v2: val): (True ⊢ ⟨⟨l ↦ v1⟩⟩ #l <- v2 ⟨⟨w, ⌜w = #()⌝ ∗ l ↦ v2⟩⟩)%I.
+  Proof.
+    iIntros "_ !> Hl $". iApply (rswp_store with "[$Hl]").
+    by iIntros "$".
+  Qed.
+
+  Lemma store_src_tpr (et: expr) l v1 v2 K P Q:
+    to_val et = None
+    → (⟨⟨src (fill K (Val #())) ∗ l ↦s v2 ∗ P⟩⟩ et ⟨⟨v, Q v⟩⟩
+      ⊢ {{src (fill K (#l <- v2)) ∗ l ↦s v1 ∗ ▷ P}} et {{v, Q v}})%I.
+  Proof.
+    iIntros (Hexp) "#H !> [Hsrc [Hloc P]] Hna". iApply (rwp_take_step with "[P Hna] [Hsrc Hloc]"); first done; last first.
+    - iApply step_store. iFrame.
+    - iIntros "Hsrc'". iApply rswp_do_step. iNext. iApply ("H" with "[$P $Hsrc'] Hna").
+  Qed.
+
+  Lemma load_tgt_tpr l v: (True ⊢ ⟨⟨l ↦ v⟩⟩ ! #l ⟨⟨w, ⌜w = v⌝ ∗ l ↦ v⟩⟩)%I.
+  Proof.
+    iIntros "_ !> Hl $". iApply (rswp_load with "[$Hl]").
+    by iIntros "$".
+  Qed.
+
+  Lemma load_src_tpr (et: expr) l v K P Q:
+    to_val et = None
+    → (⟨⟨src (fill K (Val v)) ∗ l ↦s v ∗ P⟩⟩ et ⟨⟨w, Q w⟩⟩
+      ⊢ {{src (fill K (! #l)) ∗ l ↦s v ∗ ▷ P}} et {{w, Q w}})%I.
+  Proof.
+    iIntros (Hexp) "#H !> [Hsrc [Hloc P]] Hna". iApply (rwp_take_step with "[P Hna] [Hsrc Hloc]"); first done; last first.
+    - iApply step_load. iFrame.
+    - iIntros "Hsrc'". iApply rswp_do_step. iNext. iApply ("H" with "[$P $Hsrc'] Hna").
+  Qed.
+
+  Lemma ref_tgt_tpr (v: val): (True ⊢ ⟨⟨ True ⟩⟩ ref v ⟨⟨w, ∃ l: loc, ⌜w = #l⌝ ∗ l ↦ v⟩⟩)%I.
+  Proof.
+    iIntros "_ !> _ $". iApply (rswp_alloc with "[//]").
+    iIntros (l) "[Hl _]". iExists l. by iFrame.
+  Qed.
+
+  Lemma ref_src_tpr (et: expr) v K P Q:
+    to_val et = None
+    → (⟨⟨∃ l: loc, src (fill K (Val #l)) ∗ l ↦s v ∗ P⟩⟩ et ⟨⟨w, Q w⟩⟩
+      ⊢ {{src (fill K (ref v)) ∗ ▷ P}} et {{w, Q w}})%I.
+  Proof.
+    iIntros (Hexp) "#H !> [Hsrc HP] Hna". iApply (rwp_take_step with "[HP Hna] [Hsrc]"); first done; last first.
+    - iApply step_alloc. iFrame.
+    - iIntros "Hsrc'". iApply rswp_do_step. iNext. iApply ("H" with "[$HP $Hsrc'] Hna").
+  Qed.
+
+
+  Lemma stutter_src_tpr (e: expr) P Q: to_val e = None → (⟨⟨P⟩⟩ e ⟨⟨v, Q v⟩⟩ ⊢ {{P}} e {{v, Q v}})%I.
+  Proof.
+    iIntros (H) "#H !> P Hna". iApply rwp_no_step; first done.
+    by iApply ("H" with "P Hna").
+  Qed.
+
+  Lemma stutter_tgt_tpr (et: expr) P Q :
+    to_val et = None →
+    {{P}} et {{v, Q v}} ⊢ {{ |==>src P }} et {{v, Q v}}.
+  Proof.
+    iIntros (H) "#H !> P Hna".
+    iApply (rwp_weaken' P with "[Hna]"); first done.
+    - iIntros "HP". by wp_apply ("H" with "HP").
+    - done.
+  Qed.
+
+  (* implicit stuttering *)
+  Lemma src_upd_intro P : P ⊢ |==>src P.
+  Proof.
+    iIntros "P". by iApply weak_src_update_return.
+  Qed.
+
+  Lemma src_upd_bind P Q : (|==>src P) ∗ (P -∗ |==>src Q) ⊢ |==>src Q.
+  Proof. eapply weak_src_update_bind. Qed.
+
+  Lemma src_upd_frame P Q : (|==>src P) ∗ Q ⊢ |==>src (P ∗ Q).
+  Proof.
+    iIntros "[HP HQ]". iApply (src_upd_bind with "[$HP HQ]").
+    iIntros "HP". iApply src_upd_intro. iFrame.
+  Qed.
+
+  Lemma src_upd_pure e e' K :
+    pure_step e e' →
+    ((src (fill K e)) ⊢ |==>src (src (fill K e'))).
+  Proof.
+    iIntros (Hstep) "Hsrc". iApply (src_update_weak_src_update).
+    iApply (step_pure with "Hsrc").
+    apply pure_step_ctx; last done. apply _.
+  Qed.
+
+  Lemma src_upd_store (l: loc) (v w: val) K :
+    src (fill K (#l <- w)) ∗ (l ↦s v) ⊢ |==>src src (fill K #()) ∗ (l ↦s w).
+  Proof.
+    iIntros "[Hsrc Hl]". iApply src_update_weak_src_update.
+    iApply step_store. iFrame.
+  Qed.
+
+  Lemma src_upd_load (l: loc) (v: val) K :
+    src (fill K (! #l)) ∗ (l ↦s v) ⊢ |==>src src (fill K v) ∗ (l ↦s v).
+  Proof.
+    iIntros "[Hsrc Hl]". iApply src_update_weak_src_update.
+    iApply step_load. iFrame.
+  Qed.
+
+  Lemma src_upd_alloc (v: val) K :
+    src (fill K (ref v)) ⊢ |==>src ∃ (l: loc), src (fill K #l) ∗ l ↦s v.
+  Proof.
+    iIntros "Hsrc". iApply src_update_weak_src_update.
+    iApply step_alloc. iFrame.
+  Qed.
+
+  (* explicit stuttering *)
+  Lemma src_stutter_cred P et Q :
+    to_val et = None →
+    ⟨⟨ P ⟩⟩ et ⟨⟨ v, Q v ⟩⟩ ⊢  {{ $ 1 ∗ ▷ P}} et {{v, Q v}}.
+  Proof.
+    iIntros (H) "#H !> [Hc P]  Hna". iApply (rwp_take_step with "[Hna P] [Hc]"); first done; last first.
+    - iApply step_stutter. iFrame.
+    - iIntros "_". iApply rswp_do_step. iNext.
+      iApply ("H" with "[$P] Hna").
+  Qed.
+
+  Lemma src_stutter_cred_split n m :
+    $ (n + m) ⊣⊢ $ n ∗ $ m.
+  Proof.
+    rewrite srcF_split //.
+  Qed.
+
+  Lemma pure_src_stutter_tpr (e e' et: expr) (n: nat) K P Q:
+    to_val et = None
+    → pure_step e e'
+    → (⟨⟨src (fill K e') ∗ $ n ∗ P⟩⟩ et ⟨⟨v, Q v⟩⟩ ⊢ {{src (fill K e) ∗ ▷ P}} et {{v, Q v}})%I.
+  Proof.
+    iIntros (Hexp Hstep) "#H !> [Hsrc P] Hna". iApply (rwp_take_step with "[P Hna] [Hsrc]"); first done; last first.
+    - iApply (step_pure_cred with "Hsrc").
+      apply pure_step_ctx; last done. apply _.
+    - iIntros "Hsrc'". iApply rswp_do_step. iNext. iApply ("H" with "[$P $Hsrc'] Hna").
+  Qed.
+
+  Lemma store_src_stutter_tpr (et: expr) l v1 v2 n K P Q:
+    to_val et = None
+    → (⟨⟨src (fill K (Val #())) ∗ l ↦s v2 ∗ $ n ∗ P⟩⟩ et ⟨⟨v, Q v⟩⟩
+      ⊢ {{src (fill K (#l <- v2)) ∗ l ↦s v1 ∗ ▷ P}} et {{v, Q v}})%I.
+  Proof.
+    iIntros (Hexp) "#H !> [Hsrc [Hloc P]] Hna". iApply (rwp_take_step with "[P Hna] [Hsrc Hloc]"); first done; last first.
+    - iApply (step_inv_alloc with "[Hloc] Hsrc").
+      iSplitL. { iIntros "Hl". iApply step_store. iFrame. }
+      iIntros "[Hsrc Hl]". iExists _. iFrame.
+      iPureIntro. intros Heq%(inj (fill K)). simplify_eq.
+    - iIntros "[[Hsrc' Hl] Hc]". iApply rswp_do_step. iNext.
+      iApply ("H" with "[$P $Hsrc' $Hc $Hl] Hna").
+  Qed.
+
+  Lemma load_src_stutter_tpr (et: expr) l v n K P Q:
+    to_val et = None
+    → (⟨⟨src (fill K (Val v)) ∗ l ↦s v ∗ $ n ∗ P⟩⟩ et ⟨⟨w, Q w⟩⟩
+      ⊢ {{src (fill K (! #l)) ∗ l ↦s v ∗ ▷ P}} et {{w, Q w}})%I.
+  Proof.
+    iIntros (Hexp) "#H !> [Hsrc [Hloc P]] Hna". iApply (rwp_take_step with "[P Hna] [Hsrc Hloc]"); first done; last first.
+    - iApply (step_inv_alloc with "[Hloc] Hsrc").
+      iSplitL. { iIntros "Hl". iApply step_load. iFrame. }
+      iIntros "[Hsrc Hl]". iExists _. iFrame.
+      iPureIntro. intros Heq%(inj (fill K)). simplify_eq.
+    - iIntros "[[Hsrc' Hl] Hc]". iApply rswp_do_step. iNext.
+      iApply ("H" with "[$P $Hsrc' $Hc $Hl] Hna").
+  Qed.
+
+  Lemma ref_src_stutter_tpr (et: expr) v n K P Q:
+    to_val et = None
+    → (⟨⟨∃ l: loc, src (fill K (Val #l)) ∗ l ↦s v ∗ $ n ∗ P⟩⟩ et ⟨⟨w, Q w⟩⟩
+      ⊢ {{src (fill K (ref v)) ∗ ▷ P}} et {{w, Q w}})%I.
+  Proof.
+    iIntros (Hexp) "#H !> [Hsrc HP] Hna". iApply (rwp_take_step with "[HP Hna] [Hsrc]"); first done; last first.
+    - iApply (step_inv_alloc with "[] Hsrc").
+      iSplitL. { iIntros "Hl". iApply step_alloc. iFrame. }
+      iDestruct 1 as (l) "[Hsrc Hl]". iExists _. iFrame.
+      iPureIntro. intros Heq%(inj (fill K)). simplify_eq.
+    - iIntros "[Hsrc Hc]". iDestruct "Hsrc" as (l) "[Hsrc Hl]".
+      iApply rswp_do_step. iNext.
+      iApply ("H" with "[HP Hl Hsrc Hc] Hna").
+      iExists _. iFrame.
+  Qed.
 
 End derived.
diff --git a/theories/examples/refinements/refinement.v b/theories/examples/refinements/refinement.v
index a27e0ca1e91d33cb339741a1cd5b7be78cf245e5..a09c8c7f32e3a8216169a2a508a8512f5dd8eaa5 100644
--- a/theories/examples/refinements/refinement.v
+++ b/theories/examples/refinements/refinement.v
@@ -350,8 +350,8 @@ Section heap_lang_source_steps.
     Qed.
 
     (* operational rules *)
-    Lemma step_pure E j (e1 e2: expr):
-      pure_step e1 e2 → j ⤇ e1 ⊢ src_update E (j ⤇ e2).
+    Lemma step_pure_cred k E j (e1 e2: expr):
+      pure_step e1 e2 → j ⤇ e1 ⊢ src_update E (j ⤇ e2 ∗ $ k).
     Proof.
       iIntros (Hp) "Hj"; rewrite /src_update /tpool_mapsto /source_interp //=.
       iIntros ([[tp [h m]] n]) "[[H● Hl] Hnat]".
@@ -361,7 +361,9 @@ Section heap_lang_source_steps.
         by eapply (exclusive_local_update) with (x' := Excl e2). }
       iDestruct "Hl" as (l Htrace) "Hfmlist".
       iMod (fmlist_update_snoc (to_cfg (<[j:= e2]> tp, (h, m))) with "[$]") as "(Hfmlist&_)".
-      iFrame "Hj". iModIntro. iExists (((<[j:= e2]> tp), (h, m)), n).
+      iFrame "Hj". iMod (own_update _ (● n)  (● (n + k)%nat ⋅ ◯ k) with "Hnat") as "[Hnat Hk]".
+      { eapply auth_update_alloc, nat_local_update. rewrite /ε //= /nat_unit. }
+      iFrame "Hk". iModIntro. iExists (((<[j:= e2]> tp), (h, m)), (n + k)).
       rewrite to_tpool_insert'; eauto; iFrame.
       iSplit.
       - iPureIntro.
@@ -374,6 +376,14 @@ Section heap_lang_source_steps.
         apply pure_step_prim_step, Hp.
     Qed.
 
+    Lemma step_pure E j (e1 e2: expr):
+      pure_step e1 e2 → j ⤇ e1 ⊢ src_update E (j ⤇ e2).
+    Proof.
+      intros Hp. iIntros "HP". iApply src_update_mono.
+      iSplitL; first by iApply (step_pure_cred 0).
+      by iIntros "[Hj _]".
+    Qed.
+
     Lemma steps_pure n E j (e1 e2: expr):
       nsteps pure_step (S n) e1 e2 → j ⤇ e1 ⊢ src_update E (j ⤇ e2).
     Proof.
diff --git a/theories/program_logic/refinement/ref_source.v b/theories/program_logic/refinement/ref_source.v
index a85a6828fb7bd254abab7338b00672866f8f6d09..a5e95eb6f95d2f6917b25ce9b6802f5733ec717f 100644
--- a/theories/program_logic/refinement/ref_source.v
+++ b/theories/program_logic/refinement/ref_source.v
@@ -101,6 +101,14 @@ Section src_update.
     by eapply tc_rtc_r.
   Qed.
 
+  Lemma weak_src_update_bind E P Q : weak_src_update E P ∗ (P -∗ weak_src_update E Q) ⊢ weak_src_update E Q.
+  Proof.
+    iIntros "[H1 H2]". rewrite /weak_src_update.
+    iIntros (a) "HS". iMod ("H1" with "HS") as (b Hb) "[HS HP]".
+    iMod ("H2" with "HP HS") as (c Hc) "[HS HQ]". iModIntro.
+    iExists c. iFrame. iPureIntro. by etrans.
+  Qed.
+
   Lemma weak_src_update_mono_fupd E P Q: weak_src_update E P ∗ (P ={E}=∗ Q) ⊢ weak_src_update E Q.
   Proof.
     iIntros "[HP PQ]". iIntros (a) "Hsrc".