Can reason directly with atomic triples, but is horrible.

theories/examples/external/reloc/paper_example.v

@@ -77,6 +77,88 @@ Hint Extern 4 (_ ≤ _)%nat => apply Nat.le_refl : solve_pure_add.
 
 Global Program Instance incr_counter_spec' (c : val) n :
   SPEC {{ counter c n }} incr_counter' c {{ RET #(); counter c (S n) }}.
+
+Lemma fg_increment_atomic_wp (l : loc) :
+  ⊢ atomic.atomic_wp (fg_increment #l) (TA := [tele_pair Z]) (TB := [tele]) ∅ (tele_app (λ z, l ↦ #z)) 
+      (tele_app (λ z, tele_app (TT := [tele]) (l ↦ #(z + 1))))
+      (tele_app (λ z, tele_app (TT := [tele]) (#z))).
+Proof. iSmash. Qed.
+
+Lemma la_exists e TB E (α : TeleO → iProp Σ) `(α' : A → iProp Σ) β f :
+  (∀.. (tt : TeleO), IntoExistCareful (α tt) α') →
+  (∀.. (tt : TeleO), ∀ a, (α' a ⊢ α tt)) →
+  atomic.atomic_wp e (TA := [tele_pair A]) (TB := TB) E (tele_app α') (λ _, β TargO) (λ _, f TargO) ⊢
+  atomic.atomic_wp e (TA := [tele]) (TB := TB) E α β f.
+Proof. 
+  rewrite /IntoExistCareful /= => Hα Hα2.
+  iStepsS. Transparent atomic.atomic_acc'.
+  rewrite /atomic.atomic_acc' /=. Opaque atomic.atomic_acc'.
+  iMod "H2" as "[Hα Hcl]".
+  rewrite {1}Hα.
+  iReIntro "Hα".
+  iExists ([tele_arg x0]). rewrite /=.
+  iStepS. iIntros "!>" (mtb).
+  iStepS.
+  - iDestruct "Hcl" as "[Hcl _]".
+    iStepS.
+    rewrite Hα2. iStepsS.
+  - iDestruct "H1" as (tb) "[Hβ ->]".
+    iDestruct "Hcl" as "[_ Hcl]".
+    iMod ("Hcl" $! tb with "Hβ") as "$". done.
+Qed.
+
+Lemma la_frame TA TB (α1 α2 : TA -t> iProp Σ) (β' : TA -t> TB -t> iProp Σ) (α : TA → iProp Σ) e E (β : TA → TB → iProp Σ) f  :
+  (∀.. (a : TA), α a ⊢ tele_app α1 a ∗ tele_app α2 a) →
+  (∀.. (a : TA), tele_app α1 a ∗ tele_app α2 a ⊢ α a) →
+  (□ (∀.. (a : TA) (b : TB), tele_app (tele_app β' a) b ∗ tele_app α2 a ={∅}=∗ β a b)) -∗
+  atomic.atomic_wp e E (tele_app α1) (tele_app (tele_map tele_app β')) f -∗
+  atomic.atomic_wp e E α β f.
+Proof.
+  rewrite !tforall_forall => Hα1 Hα2.
+  iStepsS. Transparent atomic.atomic_acc'.
+  rewrite /atomic.atomic_acc' /=. Opaque atomic.atomic_acc'.
+  iMod "H3" as (a) "[Hα Hcl]".
+  rewrite {1}Hα1. iReIntro "Hα".
+  iExists a. iStepS.
+  iIntros "!>" (my) "[[Hl ->]|[%b [Hr ->]]]".
+  - iDestruct "Hcl" as "[Hcl _]". iStepsS. rewrite -Hα2. iStepsS.
+  - iDestruct "Hcl" as "[_ Hcl]".
+    iAssert (|={∅}=> β a b)%I with "[H3 Hr]" as ">Hβ".
+    { iSpecialize ("H1" $! a b). rewrite tele_map_app. iStepsS. }
+    iMod ("Hcl" $! b with "Hβ") as "$". done.
+Qed.
+
+Global Instance incr_counter_spec_horrible (c : val) n :
+  SPEC {{ counter c n }} incr_counter' c {{ RET #(); counter c (S n) }}.
+Proof.
+  iStepS. wp_lam.
+  wp_bind (fg_increment _)%E.
+  iApply (atomic.atomic_wp_seq (TA := [tele]) (TB := [tele_pair Z]) _ _ (λ _, emp)%I (λ _ _, own x (◯ MaxNat (S n))) (λ _, tele_app (λ z, #z)))%I.
+  - iApply (atomic.atomic_wp_inv with "[] H1"); last first.
+    iApply (la_exists _ _ _ _ (λ z : Z, ∃ (n : nat), ⌜Z.of_nat n = z⌝ ∗ ▷ x0 ↦ #n ∗ ▷ own x (● MaxNat n))%I).
+    cbn [tforall tele_fold tele_bind tele_app].
+    { rewrite /IntoExistCareful. by iStepsS. }
+    { simpl. iStepS. iStepS. rewrite right_id. iIntros "!>". by iStepsS. }
+    iApply (la_frame ([tele_pair Z]) ([tele_pair Z]) 
+        (λ z, ▷ x0 ↦ #z) 
+        (λ z, ∃ (n : nat), ⌜Z.of_nat n = z⌝ ∗ ▷ own x (● MaxNat n))
+        (λ z1 z2, ⌜z1 = z2⌝ ∗ x0 ↦ #(z1 + 1)))%I.
+    { by iStepsS. }
+    { by iStepsS. }
+    { by iStepsS. }
+    iApply atomic.atomic_wp_mask_weaken; last first.
+    iApply atomic_wp_strong_mono; [iApply fg_increment_atomic_wp | ].
+    iIntros "!>"; iSplitL; iIntros (z).
+    * iSplit; iStepsS.
+      iMod "H7" as ">H5". iStepsS.
+    * iExists (λ _, [tele_arg z]).
+      iSplit; iStepsS. 
+    * apply empty_subseteq.
+    * reflexivity.
+  - done.
+  - iStepsS.
+  Unshelve. iSolveTC.
+Qed.
 End counter_spec'.