diff --git a/.gitignore b/.gitignore
index 32820925abcdf41a21cd63ab54dbfcb58aab5584..8b16a89f7d3ec3814579c4b4ebb0b6542c743e8d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,6 +9,5 @@
 *.prv
 *.toc
 .#*
-_*
 auto
 *.fmt
diff --git a/coq/sra/_CoqProject b/coq/sra/_CoqProject
new file mode 100644
index 0000000000000000000000000000000000000000..6bff59c6b7c6d57c482dc5a25feeea21f6614103
--- /dev/null
+++ b/coq/sra/_CoqProject
@@ -0,0 +1,4 @@
+-Q . sra
+lang.v
+lifting.v
+inv.v
diff --git a/coq/sra/inv.v b/coq/sra/inv.v
new file mode 100644
index 0000000000000000000000000000000000000000..fe9379dfc2e602e9634a3c595033292f28ea2b8c
--- /dev/null
+++ b/coq/sra/inv.v
@@ -0,0 +1,727 @@
+From iris.program_logic Require Export ectx_language ectxi_language.
+From iris.prelude Require Export strings.
+From iris.prelude Require Import gmap finite fin_maps.
+From iris.prelude Require Import numbers list.
+
+From ra Require Import lang.
+
+From mathcomp Require Import ssrbool eqtype.
+
+Global Generalizable All Variables.
+Global Set Automatic Coercions Import.
+Global Set Asymmetric Patterns.
+
+Inductive lookup_buf_inv_spec : loc -> buf -> event -> Prop :=
+| lookup_buf_inv_spec_head e b :
+    lookup_buf_inv_spec (weloc e) (e :: b) e
+| lookup_buf_inv_spec_tail e0 e b :
+    weloc e0 ≠ weloc e ->
+    lookup_buf_inv_spec (weloc e) b e ->
+    lookup_buf_inv_spec (weloc e) (e0 :: b) e.
+
+Lemma lookup_bufP {b} {l : loc} {e} : b !! l = Some e <-> lookup_buf_inv_spec l b e.
+Proof.
+  split.
+  elim: b => [//|e0 b IHb].
+  rewrite /lookup /buf_ind /=.
+  case: (decide (weloc e0 = l)) => [<- [->]|NE /IHb H] {IHb}.
+  - by constructor.
+  - inversion H; subst; [now econstructor|].
+    now econstructor.
+  induction 1. 
+  - by rewrite /lookup /buf_ind /= decide_True.
+  - by rewrite /lookup /buf_ind /= decide_False.
+Qed.
+
+
+Definition lookup_insert_revb
+   {K : Type} {M : Type → Type}
+   `{FinMap K M}
+   {A : Type} (m : M A) (i j : K) (x : A) :
+       m !! i -> isSome (<[i:=x]>  m !! j) = (isSome (m !! j)).
+Proof.
+  case Q: (<[_:=_]> _ !! _) => [|//].
+  - case: (decide (i = j)) => [HE|HNE]; [subst|].
+    + by case: (_ !! _).
+    + rewrite lookup_insert_ne // in Q. by rewrite Q.
+  - by move/lookup_insert_None : Q => [->].
+Qed.
+
+Definition lookup_insert_rev
+   {K : Type} {M : Type → Type}
+   `{FinMap K M}
+   {A : Type} (m : M A) (i j : K) (x : A) :
+       m !! i -> is_Some (<[i:=x]>  m !! j) -> (is_Some (m !! j)).
+Proof.
+  case Q: (<[_:=_]> _ !! _) => [|//].
+  - case: (decide (i = j)) => [HE|HNE]; [subst|].
+    + case: (_ !! _) => //. by eexists.
+    + rewrite lookup_insert_ne // in Q. by rewrite Q.
+  - by move/lookup_insert_None : Q => [->].
+Qed.
+
+Definition lookup_insert_inclb
+   {K : Type} {M : Type → Type} 
+   `{FinMap K M}
+   {A : Type} (m : M A) (i j : K) (x : A) :
+       m !! j -> <[i:=x]>  m !! j.
+Proof.
+  case Q: (<[_:=_]> _ !! _) => [//|]. by move/lookup_insert_None : Q => [->]. 
+Qed.
+
+Definition lookup_insert_incl
+   {K : Type} {M : Type → Type} 
+   `{FinMap K M}
+   {A : Type} (m : M A) (i j : K) (x : A) :
+       is_Some (m !! j) -> is_Some (<[i:=x]>  m !! j).
+Proof.
+  case Q: (<[_:=_]> _ !! _) => [//|]; first by eexists. by move/lookup_insert_None : Q => [->]. 
+Qed.
+
+Lemma lookup_buf_loc b (l : loc) :
+  ∀ e, ∀ He : b !! l = Some e, weloc e = l.
+Proof.
+  move => e /lookup_bufP. now inversion 1.
+Qed.
+
+Lemma lookup_buf_in b (l : loc) e : b !! l = Some e -> e ∈ b.
+Proof.
+  move => /lookup_bufP Hl.
+  induction Hl; now constructor.
+Qed.
+
+Lemma index_buf_in b i e : b !! i = Some e -> e ∈ b.
+Proof.
+  revert b; induction i => b; destruct b => //=.
+  - rewrite /buf_ind //= => [[->]]; now constructor.
+  - constructor 2. exact: IHi.  
+Qed.
+
+Module PhysicalInvariants.
+
+  Notation "''ts_' r" := (λ e1 e2, weloc e1 = weloc e2 -> r (wetime e1) (wetime e2)) (at level 0, format "''ts_' r").
+  
+  Lemma lookup_buf_recent b (HB : StronglySorted 'ts_Pos.gt b) (l : loc) :
+    ∀ e, ∀ He : b !! l = Some e,
+      ∀ e', ∀ He' : e' ∈ b, 'ts_Pos.ge e e'.
+  Proof.
+    elim: b HB => [//|e0 b IHb] HS.
+    case: (StronglySorted_inv HS) => {HS} [/IHb {IHb} IHb] /Forall_forall HF e Hl.
+    move/lookup_bufP: (Hl); inversion 1; subst => e' /elem_of_cons [->|He'].
+    - move => _. apply: Pos.le_ge; exact: Pos.le_refl.
+    - move => ?. apply: Pos.le_ge; apply: Pos.lt_le_incl; apply: Pos.gt_lt. exact: HF.
+    - move => H. by rewrite H in H2.
+    - apply: IHb => //. exact/lookup_bufP.
+  Qed.
+
+  Definition buf_inv (f : ∀ σ π b, Prop) σ :=
+      ∀ π b, ∀ Hb : sbuf σ !! π = Some b, f σ π b.
+  
+  Definition BuffersMonotone :=
+    buf_inv (λ _ π b, StronglySorted ('ts_Pos.gt : event -> event -> Prop) b).
+
+  Definition LocationsLegal :=
+    buf_inv (λ σ π b, ∀ e (HIn : e ∈ b), is_Some (stime σ !! weloc e)).
+    
+  Definition TimestampsLegal :=
+    buf_inv (λ σ π b,
+             ∀ e (HIn : e ∈ b),
+               ∀ ts, ∀ Hts : stime σ !! (weloc e) = Some ts,
+                 (wetime e) ∈ ts).
+  
+  Definition IndicesLegal (σ : state) :=
+    ∀ π ρ, (π,ρ) ∈ dom (gset (thread*thread)) (sind σ) ↔
+                 π ∈ dom (gset _) (sbuf σ)
+                 ∧ ρ ∈ dom (gset _) (sbuf σ).
+    
+  (* Definition IndicesLegal (σ : state) := *)
+  (*   ∀ π ρ, (sind σ !! (π,ρ)) ↔ (sbuf σ !! π) ∧ (sbuf σ !! ρ).  *)
+
+  Definition futevt (e1 e2 : event) :=
+    weloc e1 = weloc e2 ∧ (wetime e1 >= wetime e2)%positive.
+
+  Instance futevt_Refl : Reflexive futevt.
+  Proof. by firstorder. Qed.
+
+  Instance futevt_Trans : Transitive futevt.
+  Proof.
+    unfold futevt. move => ? ? ? [-> ?] [-> ?]. split => //.
+    apply/Pos.le_ge. etrans; exact/Pos.ge_le.
+  Qed.
+
+  Definition futbuf (b1 b2 : buf) :=
+    ∀ e2, ∀ Hin : e2 ∈ b2, ∃ e1, e1 ∈ b1 ∧ futevt e1 e2.
+
+  Instance futbuf_Trans : Transitive futbuf.
+  Proof.
+    move => ? ? ? H12 H23.
+    move => ? /H23 [? [/H12 [? [? ?]]] ?].
+    by eauto using futevt_Trans.
+  Qed.
+
+  Instance futbuf_Refl : Reflexive futbuf.
+  Proof.
+      do 2!move => *. by eauto using futevt_Refl.
+  Qed.
+
+  Lemma futbuf_compat_cons e b1 b2 : futbuf b1 b2 -> futbuf (e::b1) (e::b2).
+  Proof. 
+    move => H e' /elem_of_cons [<-|/H {H} [e1 [He1 ?]]].
+    - eexists; split; first by left. exact: futevt_Refl.
+    - exists e1; split => //. by right.
+  Qed.
+
+  Lemma futbuf_cons_l e b1 : futbuf (e :: b1) b1.
+  Proof.
+    move => e' He'. exists e'; repeat split; first by right.
+    apply/Pos.le_ge. exact: Pos.le_refl.
+  Qed.
+
+  Lemma futbuf_cons_r e1 e2 b1 b2 :
+    b1 !! weloc e2 = Some e1 ->
+    (wetime e1 >= wetime e2)%positive ->
+    futbuf b1 b2 ->
+    futbuf b1 (e2 :: b2).
+  Proof.
+    move => ? ? ? ? /elem_of_cons [->|]; last by eauto.
+    exists e1; split; first exact: lookup_buf_in.
+    split; first exact: lookup_buf_loc.
+    assumption.
+  Qed.
+
+  Lemma futbuf_drop b1 n : futbuf b1 (drop n b1).
+  Proof.
+    elim: b1 n => [n|a l IHn [//|n]].
+    - by rewrite drop_nil.
+    - etransitivity; first exact: futbuf_cons_l. exact: IHn.
+  Qed.
+  
+  Definition IndicesContained σ :=
+    ∀ π ρ i,
+    ∀ Hi : sind σ !! (π,ρ) = Some i,
+    ∀ bπ, ∀ Hbπ : sbuf σ !! π = Some bπ,
+      ∀ bρ, ∀ Hbρ : sbuf σ !! ρ = Some bρ,
+          i ≤ List.length bρ ∧ futbuf bπ (drop (List.length bρ - i) bρ). 
+
+  Lemma pos_lt_ge_dec (p1 p2 : positive) : ({ p1 < p2 } + {p2 ≤ p1})%positive. 
+  Proof.
+    case: (decide (p1 < p2)%positive); first auto.
+    right. by move/Pos.compare_gt_iff.
+  Qed.
+  
+  Inductive Inv σ : Prop :=
+  | InvS 
+      (HBuf : BuffersMonotone σ)
+      (HL : LocationsLegal σ)
+      (HTS : TimestampsLegal σ)
+      (HIL : IndicesLegal σ)
+      (HIC : IndicesContained σ)
+    :
+      Inv σ
+     .
+    
+  (* Structure Preserving (P : state -> Prop) := *)
+  (*   mkPreserving { pres_action : action *)
+  (*                  ; _ : ∀ (σ σ' : state), P σ -> pres_action σ σ' -> P σ' }. *)
+  (* Arguments mkPreserving {P} _ _. *)
+  (* Arguments pres_action {P} _ _ _. *)
+
+  (* Definition preserving {P} (p : Preserving P) :  ∀ (σ σ' : state), P σ -> pres_action p σ σ' -> P σ'. *)
+  (* Proof. by destruct p. Qed. *)
+  
+  (* Canonical Structure Fork_Inv : Preserving Inv := *)
+  (*   mkPreserving BufferMonotone *)
+    
+  
+  Class Preserving (P : state -> Prop) (action : state -> state -> Prop) :=
+    preserves : ∀ (σ σ' : state), P σ -> action σ σ' -> P σ'.
+
+  Ltac fork_tac :=
+    intros π ρ σ σ' HMon;
+    inversion_clear 1; subst;
+    intros π' b' Hb';
+    case : (decide (π' = ρ)) Hb' => [->|HNE Hb']; 
+    [rewrite lookup_insert => [[<-]]; exact: HMon 
+     | apply: HMon; apply: eq_ind Hb'; by rewrite lookup_insert_ne].
+    
+  Instance Fork_Buf : Preserving BuffersMonotone (fork_succ π ρ) := ltac:(fork_tac).
+  Instance Fork_TSL : Preserving TimestampsLegal (fork_succ π ρ) := ltac:(fork_tac).
+  Instance Fork_LL : Preserving LocationsLegal (fork_succ π ρ) := ltac:(fork_tac).
+
+  Lemma lookup_add_from `{FinMap K M} {A} (l : list (K * A)) `{ND: NoDup (map fst l)} (m : M A) k v :
+    add_from l m !! k = Some v <-> (k,v) ∈ l \/ (k ∈ (l).*1 -> False) /\ m !! k = Some v.
+  Proof.
+    split.
+    - elim: l m k v ND => [|[k v] l IHl] ? ? ? ? /=.
+      + right; split => //. by inversion 1.
+      + move/IHl => [].
+        * exact: NoDup_cons_12.
+        * left; by right.
+        * move => [T1 T2]. apply lookupP in T2.
+          case: T2.
+          { move => [-> ->]. by do 2!left. }
+          { move => [] *. right. split => //. by inversion 1; subst. }
+    - elim: l m k v ND => [|[k v] l IHl] ? ? ? ? /=.
+      + move => [].
+        * by inversion 1.
+        * by intuition.
+      + move => [].
+        * inversion 1; subst.
+          { case: (decide (k ∈ (map fst l))).
+            - move => *. exfalso. exact: NoDup_cons_11.
+            - move => *. apply: IHl; first exact: NoDup_cons_12.
+              right. by eauto using lookup_insert. }
+          { apply: IHl; first exact: NoDup_cons_12. by left. }
+        * move => [T ?]. apply: IHl; first exact: NoDup_cons_12.
+          right; split.
+          { move => *. apply: T; by econstructor. }
+          { rewrite lookup_insert_ne // => ?; subst. apply: T. by econstructor. }
+  Qed. 
+
+  Lemma lookup_add_from_map `{FinMap K M} {A} (m1 : M A) (m : M A) k v :
+    add_from (map_to_list m1) m !! k = Some v <-> m1 !! k = Some v \/ m1 !! k = None /\ m !! k = Some v.
+  Proof.
+    split.
+    - move/lookup_add_from => []; first exact: NoDup_fst_map_to_list.
+      + move/elem_of_map_to_list. by intuition.
+      + move => [/not_elem_of_map_of_list T ?]. right; split => //.
+        by rewrite map_of_to_list in T.
+    - move => [?|[? ?]]; apply/lookup_add_from; try exact: NoDup_fst_map_to_list.
+      + left. exact/elem_of_map_to_list.
+      + right; split => //.
+        apply/not_elem_of_map_of_list_2.
+          by rewrite map_of_to_list.
+  Qed.
+
+  Lemma elem_of_dom_add_from_map  `{FinMapDom K M D} {A} (m1 : M A) (m : M A) (k : K) :
+    (k ∈ dom D (add_from (map_to_list m1) m)) ↔ k ∈ dom D m1 \/ k ∉ dom D m1 /\ k ∈ dom D m.
+  Proof.
+    split.
+    - move/elem_of_dom => [x /lookup_add_from_map [|[]]] *. 
+      + left. apply/elem_of_dom. by econstructor.
+      + right. split; [exact/not_elem_of_dom|apply/elem_of_dom; by econstructor].
+    - move => T. apply/elem_of_dom.
+      move : T => [/elem_of_dom [x Hx]|[/not_elem_of_dom N /elem_of_dom [x Hx]]];
+                    exists x; apply/lookup_add_from_map; by eauto.
+  Qed.
+    
+
+  Lemma lookup_filterP `{FinMap K M} {A} (m : M A) P `{∀ x, Decision (P x)} k v:
+    filter P m !! k = Some v <-> P (k,v) /\ m !! k = Some v.
+  Proof.
+    apply: iff_trans.
+    { symmetry. exact: elem_of_map_to_list. }
+    rewrite /filter /FinMap_Filter.
+    rewrite map_to_of_list; last first.
+    { apply NoDup_fmap_fst.
+      - move => kx x1 x2
+                   /elem_of_list_filter [? /elem_of_map_to_list T1]
+                   /elem_of_list_filter [? /elem_of_map_to_list T2].
+        rewrite T1 in T2. by inversion T2.
+      - apply: NoDup_filter. exact: NoDup_map_to_list.
+    }
+    apply: iff_trans.
+    exact: elem_of_list_filter.
+    apply: and_iff_compat_l.
+    exact: elem_of_map_to_list.
+  Qed.
+
+  Instance comp_fst_Decision {X Y} `{∀ x : X, Decision (P x)} : ∀ x : X * Y, Decision (P (x.1)) :=
+    λ xy, decide (P (xy.1)).
+    
+  Remove Hints uncurry_dec : typeclass_instances.
+  Lemma elem_of_dom_filter  `{FinMapDom K M D} {A} (m : M A) P `{∀ x, Decision (P x)} k: 
+    k ∈ dom D (filter (compose P fst) m) <-> P k /\ k ∈ dom D m.
+  Proof.
+    split.
+    - move/elem_of_dom => [?] /lookup_filterP => [[?]]; split; first by intuition.
+      apply/elem_of_dom. by eauto.
+    - move => [? /elem_of_dom [x ?]].
+      apply/elem_of_dom. exists x. 
+      apply lookup_filterP.
+      apply: (proj2 (lookup_filterP _ _ _)).
+    
+  Instance Fork_IL : Preserving IndicesLegal (fork_succ π ρ).
+  Proof.
+    move => π ρ σ σ' HInv. inversion_clear 1; subst. 
+    move => ? ? /=.
+    rewrite !dom_insert.
+    (* apply: iff_trans. *)
+    (* { exact: elem_of_dom. } *)
+    (* apply: (iff_trans (B:=∃ x, _ = Some x)). *)
+    (* { split => [[x Hx]|]. *)
+    (*   - exists x. exact: Hx. *)
+    (*   - by eauto. *)
+    (* } *)
+    (* apply: (iff_trans (B:=∃ x, _ = Some x \/ _ = None /\ _ = Some x \/ _ = None /\ _ = None /\ _ = Some x)). *)
+    (* { split. *)
+    (*   - move => [x Hx]. exists x. *)
+    (*     case/lookup_add_from_map : Hx => [T|[N] /lookup_add_from_map [T|[M] T]]. *)
+    (*     + left; exact: T. *)
+    (*     + right; left; exact: (conj N T). *)
+    (*     + right; right; exact: (conj N (conj M T)). *)
+    (*   - move => [x [H1|[H2|H3]]]; exists x. *)
+    (*     + apply/lookup_add_from_map. by intuition. *)
+    (*     + apply/lookup_add_from_map. right. intuition. *)
+    (*       apply/lookup_add_from_map. by left. *)
+    (*     + apply/lookup_add_from_map. right. intuition. *)
+    (*       apply/lookup_add_from_map. by right. *)
+    (* }  *)
+      
+    split.
+    - case/elem_of_dom_add_from_map.
+      + move/elem_of_filter.
+    - move/elem_of_dom => [i].
+      case/lookup_add_from_map => [|[] _ /lookup_add_from_map [|]].
+      + move/lookup_filterP => /= [_ T].
+        have := (proj1 (HInv _ _)).
+        move/(_ _ _ (proj2 (elem_of_dom _ _) (mk_is_Some _ _ T))).
+        by set_solver.
+      + move/lookup_filterP => /= [_ T].
+        have := (proj1 (HInv _ _)).
+        move/(_ _ _ (proj2 (elem_of_dom _ _) (mk_is_Some _ _ T))).
+        by set_solver.
+      + move => [_ T]. 
+        have := (proj1 (HInv _ _)).
+        move/(_ _ _ (proj2 (elem_of_dom _ _) (mk_is_Some _ _ T))).
+        by set_solver.
+    - move => [/elem_of_union [/elem_of_singleton ->|T] /elem_of_union [/elem_of_singleton ->|]].
+      + apply/elem_of_dom.
+        eexists. apply/lookup_add_from_map.
+      
+
+  Instance Assemble_Preserving
+           `{Preserving BuffersMonotone a} 
+           `{Preserving TimestampsLegal a}
+           `{Preserving LocationsLegal a}
+           `{Preserving IndicesLegal a}
+           `{Preserving IndicesContained a}
+           : Preserving Inv a.
+  Proof.
+    move => ? ? [? ? ? ? ?] ?. constructor; by eapply preserves.
+  Qed.     
+  
+  Ltac buf_tac HInv :=
+    intros π' bπ' L;
+    (case: (lookupP L) => [[EQ1 EQ2]|[NE1 {L} L]];
+                          [subst|try exact: HInv]).
+
+  Ltac inv_constr :=
+    intros σ σ' [HBuf HL HTS HIL HIC]; inversion 1; subst; simpl;
+    constructor;
+    [have HInv := HBuf
+    |have HInv := HL
+    |have HInv := HTS
+    |have HInv := HIL
+    |have HInv := HIC].
+
+  Lemma drop_cons_pred {A} n (l : list A) a : n > 0 -> drop n (a::l) = drop (Nat.pred n) l.
+  Proof. elim: n => //. by inversion 1. Qed.
+
+  Lemma lookup_cons_pred {A} n (l : list A) a : n > 0 -> (a :: l) !! n = l !! (Nat.pred n).
+  Proof.
+  Proof. elim: n => //. by inversion 1. Qed.
+    
+  
+  Lemma drop_nth {A} i (l : list A) (ai: A) :
+    i < List.length l ->
+    l !! (List.length l - S i) = Some ai ->
+    drop (List.length l - (S i)) l = ai :: drop (List.length l - i) l.
+  Proof.
+    elim: l i ai => [i ai //=|a l IHl i ai /=].
+    case/le_lt_eq_dec => [/lt_S_n|[->]]; last first.
+    - rewrite Nat.sub_diag /= => [[->]].
+      rewrite Nat.sub_succ_l; last exact: Nat.le_refl.
+      by rewrite Nat.sub_diag.
+    - move => Hlt Hai.
+      rewrite Nat.sub_succ_l /=; last exact: Nat.lt_le_incl.
+      rewrite -IHl //.
+      + rewrite Nat.sub_succ_r drop_cons_pred //. by omega.
+      + move: Hai. rewrite Nat.sub_succ_r lookup_cons_pred //. by omega.
+  Qed.
+  
+  Instance Process_Succ_Inv : Preserving Inv (process_succ π).
+  Proof.
+    intros π. inv_constr.
+    - buf_tac HInv; constructor; [exact: HInv|]. apply/Forall_forall => e Heb HEqe.
+      suff/Pos.ge_le H2: (wetime eπ >= wetime e)%positive.
+      + move: Ht => /Pos.gt_lt H1; apply/Pos.lt_gt. exact: Pos.le_lt_trans H2 H1.
+      + apply: lookup_buf_recent => //; [exact: HInv|move: HEqe => <-; exact: lookup_buf_loc].
+    - buf_tac HInv => e /elem_of_cons [->|Hebπ].
+      + by apply: HL; [|exact: index_buf_in].
+      + by apply: HL; [|exact: Hebπ].
+    - buf_tac HInv => e /elem_of_cons [->|Hebπ].
+      + by apply: HTS; [|exact: index_buf_in].
+      + by apply: HTS; [|exact: Hebπ].
+    - move => * /=.
+      by rewrite !lookup_insert_revb ?Hbπ // Hind.
+    - (* Lots of case distinctions coming up:
+         π' =?= π
+         T ρ' =?= π
+         T F ρ =?= ρ
+         F ρ' =?= π 
+       *)
+      move => /= ? ? i' Hi' ? T.
+      case/lookupP: T Hi' => [[->] -> Hi' ? T|[NE ?] Hi'].
+      + case/lookupP: T Hi' => [[->] -> Hi'|[? T] Hi'].
+        * split; [|exact: futbuf_drop]. 
+          rewrite lookup_insert_ne in Hi' => [|[]]; last (by move => *; apply: Hπρ).
+          apply: le_trans; last apply: Nat.le_succ_diag_r.
+          apply: proj1. exact: HInv.
+        * case/lookupP: Hi' T => [[[->] ->]|].
+          { rewrite Hbρ => [[<-]].
+            rewrite (drop_nth _ _ _ Hi Heρ).
+            split; first exact: lt_le_S.
+            apply: futbuf_compat_cons. apply: proj2. exact: HInv.
+          } 
+          { move => [? ?] ?. split.
+            - apply: proj1. exact: HInv.
+            - etransitivity. apply: futbuf_cons_l. apply: proj2. exact: HInv.
+          } 
+      + rewrite lookup_insert_ne in Hi' => [|[T ?]]; last by rewrite T in NE.
+        move => ? T.
+        case/lookupP : T Hi' => [[-> ->] Hi'|[? ?] Hi']; last exact: HInv.
+        split.
+        * apply: le_trans; last apply: Nat.le_succ_diag_r.
+          apply: proj1. exact: HInv.
+        * rewrite Nat.sub_succ_l; last (apply: proj1; exact: HInv).
+          apply: proj2. exact: HInv.
+  Qed.
+  
+  Instance Process_Skip_Inv : Preserving Inv (process_skip π).
+  Proof.
+    intros π. inv_constr; [assumption|assumption|assumption| |].
+    - move => π1 π2 => /=.
+      split => [|[]].
+      + case HS:  {1}(_ !! (_,_)) => [j|//] _.
+        have {HS}: (sind σ !! (π1, π2)).
+        { case/lookupP: HS => [[[-> ->] Hj]|[_ ->] //]. by rewrite Hind. }
+        move/HInv => [HS1 HS2]. by intuition.
+      + move => *. apply: lookup_insert_inclb. exact/HInv.
+    - move => /= ? ? i'.
+      case/lookupP.
+      + move => [[-> ->] ->]. rewrite Hbπ Hbρ => ? [<-] ? [<-].
+        split; first exact: lt_le_S.
+        rewrite (drop_nth _ _ _ Hi Heρ).
+        apply: futbuf_cons_r => //.
+        * exact/Pos.le_ge.
+        * apply: proj2. exact: HInv. 
+      + move => [NE ?] *. exact: HInv.
+  Qed. 
+  
+  Instance Process_Fail_Inv : Preserving Inv (process_fail π).
+  Proof.
+    intros π. inv_constr; by intuition.
+  Qed.
+
+  (* Lemma for Store and CAS *) 
+  Lemma ic_insert_buf σ σ' e π bπ :
+    sbuf σ !! π = Some bπ ->
+    sbuf σ' = <[π := e :: bπ]>(sbuf σ) ->
+    sind σ' = sind σ ->
+    IndicesContained σ ->
+    IndicesContained σ'.
+  Proof.
+    move => ? HB HI HInv ? ? ?.
+    rewrite HB HI.
+    move => Hi ? T.
+    case/lookupP: T Hi.
+    - move => [-> ->] Hi ? T.
+      case/lookupP : T Hi.
+      + move => [-> ->] Hi; split.
+        * etrans; last exact: Nat.le_succ_diag_r.
+          apply: proj1. exact: HInv.
+        * exact: futbuf_drop.
+      + move => [? ?] ?.
+        split.
+        * apply: proj1. exact: HInv.
+        * etrans; first exact: futbuf_cons_l.
+          apply: proj2. exact: HInv.
+    - move => [? ?] Hi ? T.
+      case/lookupP : T Hi.
+      + move => [-> ->] Hi; split.
+        * etrans; last exact: Nat.le_succ_diag_r.
+          apply: proj1. exact: HInv.
+        * simpl. rewrite Nat.sub_succ_l; last (apply: proj1; exact: HInv).
+          apply: proj2. exact: HInv.
+      + move => [? ?] ?.
+        split.
+        * apply: proj1. exact: HInv.
+        * apply: proj2. exact: HInv.
+  Qed.
+          
+  Instance Store_Inv : Preserving Inv (store_action l v π).
+  Proof.
+    intros l v π. inv_constr.
+    - buf_tac HInv. constructor; [exact: HInv|]. apply/Forall_forall => e Heb HEqe.
+      suff/Pos.ge_le H2: (wetime eπ >= wetime e)%positive.
+      + move: Ht => /Pos.gt_lt H1; apply/Pos.lt_gt. exact: Pos.le_lt_trans H2 H1.
+      + apply: lookup_buf_recent => //; [exact: HInv|move: HEqe => <-; exact: lookup_buf_loc].
+    - buf_tac HInv => /=.
+      + move => e /elem_of_cons [->|Hebπ].
+        * rewrite lookup_insert. by eexists. 
+        * apply: lookup_insert_incl. exact: HInv.
+      + move => *. apply: lookup_insert_incl. exact: HInv.
+    - buf_tac HInv => /=.
+      + move => e /elem_of_cons [->|Hebπ] /= ts'.
+        rewrite lookup_insert => [[<-]].
+        * apply/elem_of_union; left; exact/elem_of_singleton.
+        * case/lookupP => [[EQ1 EQ2]|[NE1 Lts']]; [subst|exact: HInv].
+          apply/elem_of_union; right. exact: HInv.
+      + move => e Hebπ /= ts'.
+        * case/lookupP => [[EQ1 EQ2]|[NE2 Lts']]; [subst|exact: HInv].
+          apply/elem_of_union; right. exact: HInv.
+    - move => * /=. apply: iff_trans. exact: HInv.
+        by rewrite !lookup_insert_revb ?Hbπ.
+    - exact: ic_insert_buf.
+  Qed.
+
+  Instance CAS_Succ_Inv : Preserving Inv (scas_succ l v_o v_n π).
+  Proof.
+    intros l v_o v_n π. inv_constr. 
+    - buf_tac HInv. constructor; [exact: HInv|]. apply/Forall_forall => /= e Heb HEqe.
+      suff/Pos.ge_le H2: (wetime eπ >= wetime e)%positive.
+      + apply/Pos.lt_gt. apply: Pos.le_lt_trans H2 _; exact: Pos.lt_add_diag_r. 
+      + apply: lookup_buf_recent => //; [exact: HInv|move: HEqe => <-; exact: lookup_buf_loc].
+    - buf_tac HInv.
+      + move => e /elem_of_cons [->|Hebπ] /=.
+        * rewrite lookup_insert. by eexists.
+        * apply: lookup_insert_incl. exact: HInv.
+      + move => e Hebπ'. apply: lookup_insert_incl. exact: HInv. 
+    - buf_tac HInv.
+      + move => e /elem_of_cons [->|Hebπ] /= ts'.
+        rewrite lookup_insert => [[<-]].
+        * apply/elem_of_union; left; exact/elem_of_singleton.
+        * case/lookupP => [[EQ1 EQ2]|[NE1 Lts']]; [subst|exact: HInv].
+          apply/elem_of_union; right. exact: HInv.
+      + move => e Hebπ' /= ts'.
+        case/lookupP => [[EQ1 EQ2]|[? Lts']]; [subst|exact: HInv].
+        apply/elem_of_union; right. exact: HInv.
+    - move => * /=. apply: iff_trans. exact: HInv.
+      by rewrite !lookup_insert_revb ?Hbπ.
+    - exact: ic_insert_buf.
+  Qed.
+
+  Instance CAS_Fail_Inv : Preserving Inv (scas_fail l v_o π).
+  Proof. 
+    intros l v_o π. inv_constr; by intuition.
+  Qed.
+  Instance CAS_Wait_Inv : Preserving Inv (scas_wait l v_o π).
+  Proof. 
+    intros l v_o π. inv_constr; by intuition.
+  Qed.
+
+  Instance Alloc_Inv : Preserving Inv (alloc_succ π l v).
+  Proof.
+    intros π l v. inv_constr.
+    - buf_tac HInv. constructor; [exact: HInv|]. apply/Forall_forall => /= e Heb HEqe. subst.
+      cut (is_Some (stime σ !! weloc e)); last exact: HL. by rewrite H0 => [[]].
+    - buf_tac HInv => e; [move => /elem_of_cons [->|Hebπ] | move => Hebπ'];
+                        first (by rewrite lookup_insert; eexists);
+                        apply: lookup_insert_incl; exact: HInv.
+    - buf_tac HInv => e; [move => /elem_of_cons [->|Hebπ] /= ts'|move => Hebπ' /= ts'].
+      + rewrite lookup_insert => [[<-]]. by apply elem_of_singleton. 
+      + case/lookupP => [[EQ1 EQ2]|[NE1 Lts']]; [subst|exact: HInv].
+        cut (is_Some (stime σ !! weloc e)); last exact: HL. by rewrite H0 => [[]].
+      + case/lookupP => [[EQ1 EQ2]|[? Lts']]; [subst|exact: HInv].
+        cut (is_Some (stime σ !! weloc e)); last exact: HL. by rewrite H0 => [[]].
+    - move => * /=. apply: iff_trans. exact: HInv.
+      by rewrite !lookup_insert_revb ?Hbπ.
+    - exact: ic_insert_buf.
+  Qed.
+
+  Instance Step_Inv : Preserving Inv (λ σ1 σ2, impure_step e1 σ1 e2 σ2 ef).
+  Proof.
+    move => * σ σ' HInv. inversion 1 => *; subst => //.
+    - exact: Store_Inv.
+    - exact: CAS_Succ_Inv.
+    - exact: CAS_Fail_Inv.
+    - exact: CAS_Wait_Inv.
+    - exact: Alloc_Inv.
+    - exact: Process_Succ_Inv.
+    - exact: Process_Skip_Inv.
+    - exact: Process_Fail_Inv.
+  Qed.
+      
+End PhysicalInvariants.
+
+(* From ra Require Export lifting. *)
+From iris.algebra Require Import upred_big_op frac dec_agree.
+From iris.program_logic Require Export invariants ghost_ownership.
+From iris.program_logic Require Import ownership auth.
+From ra Require Import lang.
+Import uPred.
+ 
+Module CMRAs.
+  
+  
+  (* Histories are lists of buffers *)
+  Definition history := list buf.
+
+  Implicit Type (h : history).
+  
+  Definition hist_sameloc l h := ∀ b, ∀ Hin : b ∈ h, ∀ eh, ∀ Heh : b !! 0 = Some eh, weloc eh = l.
+  
+  Definition futhist h1 h2 :=
+    ∃ h, h1 = h ++ h2.
+
+  Definition histmap := gmap loc history.
+
+  Implicit Type (m : histmap).
+  
+  Definition futhistmap m1 m2 :=
+    ∀ l,
+    ∀ h2,
+    ∀ Hl2 : m2 !! l = Some h2,
+    ∃ h1, m1 !! l = Some h1 ∧ futhist h1 h2.
+
+  Instance evt_dec_eq : ∀ (e1 e2 : event), Decision (e1 = e2).
+  Proof.
+    move => [l1 v1 t1] [l2 v2 t2].
+    case: (decide (l1 = l2)) => [->|]; last right.
+    - case: (decide (v1 = v2)) => [->|]; last right.
+      + case: (decide (t1 = t2)) => [->|]; last right.
+        * by left.
+        * by move => [].
+      + move => [] *. by subst.
+    - move => [] *. by subst. 
+  Qed.
+
+  Instance loc_Equiv : Equiv loc := eq.
+  Instance raval_Equiv : Equiv raval := eq.
+  
+  Instance evt_Equiv : Equiv event :=
+    λ e1 e2,
+    match e1, e2 with
+    | mkevent l1 v1 t1, mkevent l2 v2 t2 =>
+      l1 ≡ l2 /\ v1 ≡ v2 /\ t1 ≡ t2
+    end.
+  
+  (* Instance buf_dec_eq : ∀ (b1 b2 : buf), Decision (b1 = b2). *)
+  (* Proof. *)
+  (*   move => b1. *)
+  (*   elim: b1 => [|e1 b1 IH1] [|e2 b2].  *)
+  (*  - by left. *)
+  (*  - by right. *)
+  (*  - by right. *)
+  (*  - case: (decide (e1 = e2)) => [->|]. *)
+  (*    + case: (IH1 b2) => [->|]. *)
+  (*      * by left. *)
+  (*      * by right => [[]]. *)
+  (*    + by right => [[]]. *)
+  (* Qed. *)
+  
+  Definition heapR : cmraT := gmapR loc (dec_agreeR buf).
+
+  Inductive lower_bound : Type :=
+  | LB (b : buf) : lower_bound
+  | LB_bot : lower_bound.
+
+  Instance lb_Core : Core (list buf) := id.
+  Instance lb_Op : Op (list buf) :=
+    λ b1 b2
+  
+  Definition lower_bound_ra : RA (list buf).
+  
+  
+End CMRAs.
\ No newline at end of file
diff --git a/coq/sra/lang.v b/coq/sra/lang.v
new file mode 100644
index 0000000000000000000000000000000000000000..053e0a2bbd619338a3504cbef6fa83482e77c063
--- /dev/null
+++ b/coq/sra/lang.v
@@ -0,0 +1,1137 @@
+From iris.program_logic Require Export ectx_language ectxi_language.
+From iris.prelude Require Export strings list.
+From iris.prelude Require Import gmap finite co_pset.
+
+
+From mathcomp Require Import ssrbool eqtype seq path.
+
+Global Generalizable All Variables.
+Global Set Automatic Coercions Import.
+Global Set Asymmetric Patterns.
+
+Module sra_lang.
+  (* Open Scope Z_scope. *)
+
+  Definition loc := positive. (* Really, any countable type. *)
+
+  (** Auxilliary Definitions **)
+  Definition timestamp := positive.
+  Definition thread := positive.
+  Definition index := nat.
+  Definition raval := Z.
+  Record event := mkevent { weloc : loc;
+                            weval : raval;
+                            wetime : timestamp
+                          }.
+
+  (* Unsorted Buffer *)
+  Definition buf : Type := seq event.
+  Typeclasses Transparent buf.
+
+  Definition blookup (l : loc) :=
+    fix f (b : buf) :=
+      match b with
+      | nil => None
+      | e :: b => if decide (weloc e = l) then Some e else f b
+      end
+  .
+
+  Instance buf_lookup : Lookup loc event buf := blookup.
+  Instance buf_ind : Lookup nat event buf := list_lookup.
+
+  Inductive nalock : Type :=
+  | wlock
+  | rlock of nat.
+
+  (** The state:
+   * 1. A map from thread IDs to buffers
+   * 2. A map from pairs of thread IDs to buffer indices
+   * 3. A map from locations to finite sets of timestamps
+   **)
+  Definition ind_map := gmap (thread * thread) index.
+  Record state := { sbuf : gmap thread buf;
+                    sind : ind_map;
+                    stime : gmap loc (timestamp*timestamp);
+                    slock : gmap loc nalock }.
+
+  (** Expressions and vals. *)
+
+  Inductive base_lit : Set :=
+  | LitInt (n : Z) | LitBool (b : bool) | LitUnit.
+  Inductive un_op : Set :=
+  | NegOp | MinusUnOp.
+  Inductive bin_op : Set :=
+  | PlusOp | MinusOp | LeOp | LtOp | EqOp.
+
+  Inductive binder := BAnon | BNamed : string → binder.
+  Delimit Scope binder_scope with bind.
+  Bind Scope binder_scope with binder.
+
+  Definition cons_binder (mx : binder) (X : list string) : list string :=
+    match mx with BAnon => X | BNamed x => x :: X end.
+  Infix ":b:" := cons_binder (at level 60, right associativity).
+  Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
+  Proof. solve_decision. Defined.
+
+  Instance set_unfold_cons_binder x mx X P :
+    SetUnfold (x ∈ X) P → SetUnfold (x ∈ mx :b: X) (BNamed x = mx ∨ P).
+  Proof.
+    constructor. rewrite -(set_unfold (x ∈ X) P).
+    destruct mx; rewrite /= ?elem_of_cons; naive_solver.
+  Qed.
+
+  (** A typeclass for whether a variable is bound in a given
+   context. Making this a typeclass means we can use tpeclass search
+   to program solving these constraints, so this becomes extensible.
+   Also, since typeclass search runs *after* unification, Coq has already
+   inferred the X for us; if we were to go for embedded proof terms ot
+   tactics, Coq would do things in the wrong order. *)
+  Class VarBound (x : string) (X : list string) :=
+    var_bound : bool_decide (x ∈ X).
+  (* There is no need to restrict this hint to terms without evars, [vm_compute]
+will fail in case evars are arround. *)
+  Hint Extern 0 (VarBound _ _) => vm_compute; exact I : typeclass_instances. 
+
+  Instance var_bound_proof_irrel x X : ProofIrrel (VarBound x X).
+  Proof. rewrite /VarBound. apply _. Qed.
+  Instance set_unfold_var_bound x X P :
+    SetUnfold (x ∈ X) P → SetUnfold (VarBound x X) P.
+  Proof.
+    constructor. by rewrite /VarBound bool_decide_spec (set_unfold (x ∈ X) P).
+  Qed.
+
+  Inductive read_type :=
+  | read_na | read_at.
+  Inductive write_type :=
+  | write_na | write_at.
+  
+  Structure na_struct := mkNaStruct { na_acc_ty : Type; _ : na_acc_ty }.
+  Definition na_acc_constr  (nas : na_struct) : na_acc_ty nas. Proof. by destruct nas. Qed.
+  Structure at_struct := mkAtStruct { at_acc_ty : Type; _ : at_acc_ty }.
+  Definition at_acc_constr  (ats : at_struct) : at_acc_ty ats. Proof. by destruct ats. Qed.
+  Canonical Structure na_read := mkNaStruct _ read_na.
+  Canonical Structure na_write := mkNaStruct _ write_na.
+  Canonical Structure at_read := mkAtStruct _ read_at.
+  Canonical Structure at_write := mkAtStruct _ write_at.
+  
+  Notation "'na'" := (na_acc_constr _).
+  Notation "'at'" := (at_acc_constr _).
+
+  Definition read_type_beq (rt1 rt2 : read_type) : bool :=
+    match rt1, rt2 with
+    | read_na, read_na | read_at, read_at => true
+    | _, _ => false
+    end.
+  Definition write_type_beq (wt1 wt2 : write_type) : bool :=
+    match wt1, wt2 with
+    | write_na, write_na | write_at, write_at => true
+    | _, _ => false
+    end.
+
+  Lemma read_type_beq_eq rt1 rt2 : read_type_beq rt1 rt2 ↔ rt1 = rt2.
+  Proof. by destruct rt1, rt2. Qed.
+  Lemma write_type_beq_eq wt1 wt2 : write_type_beq wt1 wt2 ↔ wt1 = wt2.
+  Proof. by destruct wt1, wt2. Qed.
+  
+  Instance read_type_dec : ∀ (rt1 rt2 : read_type), Decision (rt1 = rt2).
+  Proof.
+    intros.
+    refine (cast_if (decide (read_type_beq rt1 rt2))); by rewrite -read_type_beq_eq.
+  Qed.
+  Instance write_type_dec : ∀ (wt1 wt2 : write_type), Decision (wt1 = wt2).
+  Proof.
+    intros.
+    refine (cast_if (decide (write_type_beq wt1 wt2))); by rewrite -write_type_beq_eq.
+  Qed.
+  
+  Module BaseExpr.
+    
+    
+    Inductive expr (X : list string) :=
+    (* Base lambda calculus *)
+    (* Var is the only place where the terms contain a proof. The fact that they
+       contain a proof at all is suboptimal, since this means two seeminlgy
+       convertible terms could differ in their proofs. However, this also has
+       some advantages:
+       * We can make the [X] an index, so we can do non-dependent match.
+       * In expr_weaken, we can push the proof all the way into Var, making
+         sure that proofs never block computation. *)
+    | Var (x : string) `{VarBound x X}
+    | Rec (f x : binder) (e : expr (f :b: x :b: X))
+    | App (e1 e2 : expr X)
+    (* Base types and their operations *)
+    | Lit (l : base_lit)
+    | UnOp (op : un_op) (e : expr X)
+    | BinOp (op : bin_op) (e1 e2 : expr X)
+    | If (e0 e1 e2 : expr X)
+    (* Products *)
+    | Pair (e1 e2 : expr X)
+    | Fst (e : expr X)
+    | Snd (e : expr X)
+    (* Sums *)
+    | InjL (e : expr X)
+    | InjR (e : expr X)
+    | Case (e0 : expr X) (e1 : expr X) (e2 : expr X)
+    (* Concurrency *)
+    | Fork (e : expr X)
+    (* Ra *)
+    | Loc (l : loc)
+    | Alloc (e : expr X)
+    | Free (e : expr X)
+    | Load (rt : read_type) (e : expr X)
+    | Store (wt : write_type) (e1 : expr X) (e2 : expr X)
+    | SCAS (e0 : expr X) (e1 : expr X) (e2 : expr X)
+    | Process.
+
+    Bind Scope expr_scope with expr.
+    Delimit Scope expr_scope with E.
+    Arguments Var {_} _ {_}.
+    Arguments Rec {_} _ _ _%E.
+    Arguments App {_} _%E _%E.
+    Arguments Lit {_} _.
+    Arguments UnOp {_} _ _%E.
+    Arguments BinOp {_} _ _%E _%E.
+    Arguments If {_} _%E _%E _%E.
+    Arguments Pair {_} _%E _%E.
+    Arguments Fst {_} _%E.
+    Arguments Snd {_} _%E.
+    Arguments InjL {_} _%E.
+    Arguments InjR {_} _%E.
+    Arguments Case {_} _%E _%E _%E.
+    Arguments Fork {_} _%E.
+    Arguments Loc {_} _.
+    Arguments Alloc {_} _%E.
+    Arguments Free {_} _%E.
+    Arguments Load {_} _ _%E.
+    Arguments Store {_} _ _%E _%E.
+    Arguments SCAS {_} _%E _%E _%E.
+    Arguments Process {_}.
+
+    Inductive val :=
+    | RecV (f x : binder) (e : expr (f :b: x :b: []))
+    | LitV (l : base_lit)
+    | PairV (v1 v2 : val)
+    | InjLV (v : val)
+    | InjRV (v : val)
+    | LocV (l : loc).
+
+    Bind Scope val_scope with val.
+    Delimit Scope val_scope with V.
+    Arguments PairV _%V _%V.
+    Arguments InjLV _%V.
+    Arguments InjRV _%V.
+
+    (* Definition signal : val := RecV BAnon (BNamed "x") (Store (Var "x") (Lit (LitInt 1))). *)
+
+    Fixpoint of_val (v : val) : expr [] :=
+      match v with
+      | RecV f x e => Rec f x e
+      | LitV l => Lit l
+      | PairV v1 v2 => Pair (of_val v1) (of_val v2)
+      | InjLV v => InjL (of_val v)
+      | InjRV v => InjR (of_val v)
+      | LocV l => Loc l
+      end.
+
+    Fixpoint to_val (e : expr []) : option val :=
+      match e with
+      | Rec f x e => Some (RecV f x e)
+      | Lit l => Some (LitV l)
+      | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
+      | InjL e => InjLV <$> to_val e
+      | InjR e => InjRV <$> to_val e
+      | Loc l => Some (LocV l)
+      | _ => None
+      end.
+
+    Lemma wexpr_rec_prf {X Y} (H : X `included` Y) {f x} :
+      f :b: x :b: X `included` f :b: x :b: Y.
+    Proof. set_solver. Qed.
+
+    Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
+      match e return expr Y with
+      | Var x _ => @Var _ x _
+      | Rec f x e => Rec f x (wexpr (wexpr_rec_prf H) e)
+      | App e1 e2 => App (wexpr H e1) (wexpr H e2)
+      | Lit l => Lit l
+      | UnOp op e => UnOp op (wexpr H e)
+      | BinOp op e1 e2 => BinOp op (wexpr H e1) (wexpr H e2)
+      | If e0 e1 e2 => If (wexpr H e0) (wexpr H e1) (wexpr H e2)
+      | Pair e1 e2 => Pair (wexpr H e1) (wexpr H e2)
+      | Fst e => Fst (wexpr H e)
+      | Snd e => Snd (wexpr H e)
+      | InjL e => InjL (wexpr H e)
+      | InjR e => InjR (wexpr H e)
+      | Case e0 e1 e2 => Case (wexpr H e0) (wexpr H e1) (wexpr H e2)
+      | Fork e => Fork (wexpr H e)
+      | Loc l => Loc l
+      | Alloc e => Alloc (wexpr H e)
+      | Free e => Free (wexpr H e)
+      | Load rt  e => Load rt (wexpr H e)
+      | Store wt e1 e2 => Store wt (wexpr H e1) (wexpr H e2)
+      | SCAS e0 e1 e2 => SCAS (wexpr H e0) (wexpr H e1) (wexpr H e2)
+      | Process => Process
+      end.
+    Solve Obligations with set_solver.
+
+    Definition wexpr' {X} (e : expr []) : expr X := wexpr (included_nil _) e.
+
+    Definition of_val' {X} (v : val) : expr X := wexpr (included_nil _) (of_val v).
+
+    Lemma wsubst_rec_true_prf {X Y x} (H : X `included` x :: Y) {f y}
+          (Hfy : BNamed x ≠ f ∧ BNamed x ≠ y) :
+      f :b: y :b: X `included` x :: f :b: y :b: Y.
+    Proof. by set_solver. Qed.
+    Lemma wsubst_rec_false_prf {X Y x} (H : X `included` x :: Y) {f y}
+          (Hfy : ¬(BNamed x ≠ f ∧ BNamed x ≠ y)) :
+      f :b: y :b: X `included` f :b: y :b: Y.
+    Proof. move: Hfy=>/not_and_l [/dec_stable|/dec_stable]; set_solver. Qed.
+
+    Program Fixpoint wsubst {X Y} (x : string) (es : expr [])
+            (H : X `included` x :: Y) (e : expr X)  : expr Y :=
+      match e return expr Y with
+      | Var y _ => if decide (x = y) then wexpr' es else @Var _ y _
+      | Rec f y e =>
+        Rec f y $ match decide (BNamed x ≠ f ∧ BNamed x ≠ y) return _ with
+                  | left Hfy => wsubst x es (wsubst_rec_true_prf H Hfy) e
+                  | right Hfy => wexpr (wsubst_rec_false_prf H Hfy) e
+                  end
+      | App e1 e2 => App (wsubst x es H e1) (wsubst x es H e2)
+      | Lit l => Lit l
+      | UnOp op e => UnOp op (wsubst x es H e)
+      | BinOp op e1 e2 => BinOp op (wsubst x es H e1) (wsubst x es H e2)
+      | If e0 e1 e2 => If (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
+      | Pair e1 e2 => Pair (wsubst x es H e1) (wsubst x es H e2)
+      | Fst e => Fst (wsubst x es H e)
+      | Snd e => Snd (wsubst x es H e)
+      | InjL e => InjL (wsubst x es H e)
+      | InjR e => InjR (wsubst x es H e)
+      | Case e0 e1 e2 =>
+        Case (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
+      | Fork e => Fork (wsubst x es H e)
+      | Loc l => Loc l
+      | Alloc e => Alloc (wsubst x es H e)
+      | Free e => Free (wsubst x es H e)
+      | Load rt e => Load rt (wsubst x es H e)
+      | Store wt e1 e2 => Store wt (wsubst x es H e1) (wsubst x es H e2)
+      | SCAS e0 e1 e2 => SCAS (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
+      | Process => Process
+      end.
+    Solve Obligations with set_solver.
+
+    Definition subst {X} (x : string) (es : expr []) (e : expr (x :: X)) : expr X :=
+      wsubst x es (λ z, id) e.
+    Definition subst' {X} (mx : binder) (es : expr []) : expr (mx :b: X) → expr X :=
+      match mx with BNamed x => subst x es | BAnon => id end.
+
+    (** The stepping relation *)
+    Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
+      match op, l with
+      | NegOp, LitBool b => Some (LitBool (negb b))
+      | MinusUnOp, LitInt n => Some (LitInt (- n))
+      | _, _ => None
+      end.
+
+    Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
+      match op, l1, l2 with
+      | PlusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 + n2)
+      | MinusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 - n2)
+      | LeOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 ≤ n2)%Z
+      | LtOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 < n2)%Z
+      | EqOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 = n2)
+      | _, _, _ => None
+      end.
+
+    Inductive pure_step : expr [] → state → expr [] → state → option (expr []) → Prop :=
+    | BetaS f x e1 e2 v2 e' σ :
+        to_val e2 = Some v2 →
+        e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) →
+        pure_step (App (Rec f x e1) e2) σ e' σ None
+    | UnOpS op l l' σ :
+        un_op_eval op l = Some l' → 
+        pure_step (UnOp op (Lit l)) σ (Lit l') σ None
+    | BinOpS op l1 l2 l' σ :
+        bin_op_eval op l1 l2 = Some l' → 
+        pure_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
+    | IfTrueS e1 e2 σ :
+        pure_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
+    | IfFalseS e1 e2 σ :
+        pure_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
+    | FstS e1 v1 e2 v2 σ :
+        to_val e1 = Some v1 → to_val e2 = Some v2 →
+        pure_step (Fst (Pair e1 e2)) σ e1 σ None
+    | SndS e1 v1 e2 v2 σ :
+        to_val e1 = Some v1 → to_val e2 = Some v2 →
+        pure_step (Snd (Pair e1 e2)) σ e2 σ None
+    | CaseLS e0 v0 e1 e2 σ :
+        to_val e0 = Some v0 →
+        pure_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
+    | CaseRS e0 v0 e1 e2 σ :
+        to_val e0 = Some v0 →
+        pure_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
+    .
+
+    (** Evaluation contexts *)
+    Inductive ectx_item :=
+    | AppLCtx (e2 : BaseExpr.expr [])
+    | AppRCtx (v1 : val)
+    | UnOpCtx (op : un_op)
+    | BinOpLCtx (op : bin_op) (e2 : BaseExpr.expr [])
+    | BinOpRCtx (op : bin_op) (v1 : val)
+    | IfCtx (e1 e2 : BaseExpr.expr [])
+    | PairLCtx (e2 : BaseExpr.expr [])
+    | PairRCtx (v1 : val)
+    | FstCtx
+    | SndCtx
+    | InjLCtx
+    | InjRCtx
+    | CaseCtx (e1 : BaseExpr.expr []) (e2 : BaseExpr.expr [])
+    | AllocCtx
+    | LoadCtx (rt : read_type)
+    | StoreLCtx (wt : write_type) (e2 : BaseExpr.expr [])
+    | StoreRCtx (wt : write_type) (v1 : val)
+    | CasLCtx (e1 : BaseExpr.expr [])  (e2 : BaseExpr.expr [])
+    | CasMCtx (v0 : val) (e2 : BaseExpr.expr [])
+    | CasRCtx (v0 : val) (v1 : val).
+
+    Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
+      match Ki with
+      | AppLCtx e2 => App e e2
+      | AppRCtx v1 => App (of_val v1) e
+      | UnOpCtx op => UnOp op e
+      | BinOpLCtx op e2 => BinOp op e e2
+      | BinOpRCtx op v1 => BinOp op (of_val v1) e
+      | IfCtx e1 e2 => If e e1 e2
+      | PairLCtx e2 => Pair e e2
+      | PairRCtx v1 => Pair (of_val v1) e
+      | FstCtx => Fst e
+      | SndCtx => Snd e
+      | InjLCtx => InjL e
+      | InjRCtx => InjR e
+      | CaseCtx e1 e2 => Case e e1 e2
+      | AllocCtx => Alloc e
+      | LoadCtx rt => Load rt e
+      | StoreLCtx wt e2 => Store wt e e2
+      | StoreRCtx wt v1 => Store wt (of_val v1) e
+      | CasLCtx e1 e2 => SCAS e e1 e2
+      | CasMCtx v0 e2 => SCAS (of_val v0) e e2
+      | CasRCtx v0 v1 => SCAS (of_val v0) (of_val v1) e
+      end.
+    (** Atomic expressions *)
+    Definition atomic (e: expr []) : bool :=
+      match e with
+      | Alloc e => bool_decide (is_Some (to_val e))
+      | Load rt e => bool_decide (is_Some (to_val e))
+      | Store wt e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
+      | SCAS e0 e1 e2 => bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2))
+      | Fork e => true
+      (* Make "skip" atomic *)
+      | App (Rec _ _ (Lit _)) (Lit _)  => true
+      | _ => false
+      end.
+
+    (** Substitution *)
+    Lemma var_proof_irrel X x H1 H2 : @Var X x H1 = @Var X x H2.
+    Proof. f_equal. by apply (proof_irrel _). Qed.
+
+    Lemma wexpr_id X (H : X `included` X) e : wexpr H e = e.
+    Proof. induction e; f_equal/=; auto. by apply (proof_irrel _). Qed.
+    Lemma wexpr_proof_irrel X Y (H1 H2 : X `included` Y) e : wexpr H1 e = wexpr H2 e.
+    Proof.
+      revert Y H1 H2; induction e; simpl; auto using var_proof_irrel with f_equal.
+    Qed.
+    Lemma wexpr_wexpr X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) H3 e :
+      wexpr H2 (wexpr H1 e) = wexpr H3 e.
+    Proof.
+      revert Y Z H1 H2 H3.
+      induction e; simpl; auto using var_proof_irrel with f_equal.
+    Qed.
+    Lemma wexpr_wexpr' X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) e :
+      wexpr H2 (wexpr H1 e) = wexpr (transitivity H1 H2) e.
+    Proof. apply wexpr_wexpr. Qed.
+
+    Lemma wsubst_proof_irrel X Y x es (H1 H2 : X `included` x :: Y) e :
+      wsubst x es H1 e = wsubst x es H2 e.
+    Proof.
+      revert Y H1 H2; induction e; simpl; intros; repeat case_decide;
+        auto using var_proof_irrel, wexpr_proof_irrel with f_equal.
+    Qed.
+    Lemma wexpr_wsubst X Y Z x es (H1: X `included` x::Y) (H2: Y `included` Z) H3 e:
+      wexpr H2 (wsubst x es H1 e) = wsubst x es H3 e.
+    Proof.
+      revert Y Z H1 H2 H3.
+      induction e; intros; repeat (case_decide || simplify_eq/=);
+        unfold wexpr'; auto using var_proof_irrel, wexpr_wexpr with f_equal.
+    Qed.
+    Lemma wsubst_wexpr X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) H3 e:
+      wsubst x es H2 (wexpr H1 e) = wsubst x es H3 e.
+    Proof.
+      revert Y Z H1 H2 H3.
+      induction e; intros; repeat (case_decide || simplify_eq/=);
+        auto using var_proof_irrel, wexpr_wexpr with f_equal.
+    Qed.
+    Lemma wsubst_wexpr' X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) e:
+      wsubst x es H2 (wexpr H1 e) = wsubst x es (transitivity H1 H2) e.
+    Proof. apply wsubst_wexpr. Qed.
+
+    Lemma wsubst_closed X Y x es (H1 : X `included` x :: Y) H2 (e : expr X) :
+      x ∉ X → wsubst x es H1 e = wexpr H2 e.
+    Proof.
+      revert Y H1 H2.
+      induction e; intros; repeat (case_decide || simplify_eq/=);
+        auto using var_proof_irrel, wexpr_proof_irrel with f_equal set_solver.
+      exfalso; set_solver.
+    Qed.
+    Lemma wsubst_closed_nil x es H (e : expr []) : wsubst x es H e = e.
+    Proof.
+      rewrite -{2}(wexpr_id _ (reflexivity []) e).
+      apply wsubst_closed, not_elem_of_nil.
+    Qed.
+
+    (** Basic properties about the language *)
+    Lemma to_of_val v : to_val (of_val v) = Some v.
+    Proof. by induction v; simplify_option_eq. Qed.
+
+    Lemma of_to_val e v : to_val e = Some v → of_val v = e.
+    Proof.
+      revert e v. cut (∀ X (e : expr X) (H : X = ∅) v,
+                          to_val (eq_rect _ expr e _ H) = Some v → of_val v = eq_rect _ expr e _ H).
+      { intros help e v. apply (help ∅ e Logic.eq_refl). }
+      intros X e; induction e; intros HX ??; simplify_option_eq;
+        repeat match goal with
+               | IH : ∀ _ : ∅ = ∅, _ |- _ => specialize (IH Logic.eq_refl); simpl in IH
+                        end; auto with f_equal.
+    Qed.
+
+    Instance of_val_inj : Inj (=) (=) of_val.
+    Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
+
+    Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
+    Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
+
+    Lemma fill_item_val Ki e :
+      is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
+    Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
+
+    Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) → is_Some (to_val e).
+    Proof.
+      intros. destruct Ki; simplify_eq/=; destruct_and?;
+                                      repeat (case_match || contradiction); eauto.
+    Qed.
+
+    Lemma atomic_step e1 σ1 e2 σ2 ef :
+      atomic e1 → pure_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
+    Proof.
+      destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst.
+      unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
+    Qed.
+
+    Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
+      pure_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
+    Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
+    
+    Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
+      to_val e1 = None → to_val e2 = None →
+      fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
+    Proof.
+      destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
+                                                              repeat match goal with
+                                                                     | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
+                                                                     end; auto.
+    Qed.
+
+    Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
+    Proof. solve_decision. Defined.
+    Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
+    Proof. solve_decision. Defined.
+    Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
+    Proof. solve_decision. Defined.
+
+    Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool :=
+      match e, e' with
+      | Var x _, Var x' _ => bool_decide (x = x')
+      | Rec f x e, Rec f' x' e' =>
+        bool_decide (f = f') && bool_decide (x = x') && expr_beq e e'
+      | App e1 e2, App e1' e2' | Pair e1 e2, Pair e1' e2'
+                                 => expr_beq e1 e1' && expr_beq e2 e2'
+
+      | Store wt1 e1 e2, Store wt2 e1' e2' => bool_decide (wt1 = wt2) && expr_beq e1 e1' && expr_beq e2 e2'
+      | Lit l, Lit l' => bool_decide (l = l')
+      | UnOp op e, UnOp op' e' => bool_decide (op = op') && expr_beq e e'
+      | BinOp op e1 e2, BinOp op' e1' e2' =>
+        bool_decide (op = op') && expr_beq e1 e1' && expr_beq e2 e2'
+      | If e0 e1 e2, If e0' e1' e2' | Case e0 e1 e2, Case e0' e1' e2' |
+      SCAS e0 e1 e2, SCAS e0' e1' e2' =>
+      expr_beq e0 e0' && expr_beq e1 e1' && expr_beq e2 e2'
+      | Fst e, Fst e' | Snd e, Snd e' | InjL e, InjL e' | InjR e, InjR e' |
+      Fork e, Fork e' | Alloc e, Alloc e' | Free e, Free e'
+                                            => expr_beq e e'
+      | Load rt1 e, Load rt2 e' => bool_decide (rt1 = rt2) && expr_beq e e'
+      | Loc l, Loc l' => bool_decide (l = l')
+      | Process, Process => true
+      | _, _ => false
+      end.
+    Lemma expr_beq_correct {X} (e1 e2 : expr X) : expr_beq e1 e2 ↔ e1 = e2.
+    Proof.
+      split.
+      * revert e2; induction e1; intros [] * ?; simpl in *;
+          destruct_and?; subst; repeat f_equal/=; auto; try apply proof_irrel.
+      * intros ->. induction e2; naive_solver.
+    Qed.
+    Instance expr_dec_eq {X} (e1 e2 : expr X) : Decision (e1 = e2).
+    Proof.
+      refine (cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
+    Defined.
+    Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
+    Proof.
+      refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
+    Defined.
+
+    Instance expr_inhabited X : Inhabited (expr X) := populate (Lit LitUnit).
+    Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
+  End BaseExpr.
+
+
+  Open Scope expr_scope.
+
+  Export BaseExpr.
+
+  Definition expr X : Set := (BaseExpr.expr X *  thread).
+  Definition val : Set := (BaseExpr.val * thread).
+  Definition bexpr {X} (e : expr X) := e.1.
+  Definition pid {X} (e : expr X) := e.2.
+
+  Definition to_val (e : expr []) : option val := (fun v => (v, e.2)) <$> (to_val (e.1)).
+
+  Definition of_val v : expr [] := (of_val (v.1), v.2).
+
+  Definition atomic (e : expr []) := atomic (e.1).
+
+  (** Substitution *)
+  (** We have [subst e "" v = e] to deal with anonymous binders *)
+  Definition subst {X} (x : string) (es : expr []) (e : expr (x :: X)) : expr X :=
+    (BaseExpr.subst x (bexpr es) (bexpr e), pid e).
+
+  (** The stepping relation *)
+  Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
+    match op, l with
+    | NegOp, LitBool b => Some (LitBool (negb b))
+    | MinusUnOp, LitInt n => Some (LitInt (- n))
+    | _, _ => None
+    end.
+
+  Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
+    match op, l1, l2 with
+    | PlusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 + n2)
+    | MinusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 - n2)
+    | LeOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 ≤ n2)%Z
+    | LtOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 < n2)%Z
+    | EqOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 = n2)
+    | _, _, _ => None
+    end.
+
+
+  Definition incts (ts : (timestamp * timestamp)) :=
+    (ts.1, ts.2).
+    
+  Definition action := state -> state -> Prop.
+  Definition det_action := state -> state.
+
+  Definition lockedR : loc -> state -> Prop := λ l σ, ∃ n, slock σ !! l = Some (rlock (S n)). 
+  Definition lockedW : loc -> state -> Prop := λ l σ, slock σ !! l = Some (wlock). 
+  Definition unlocked : loc -> state -> Prop := λ l σ, slock σ !! l = Some (rlock 0). 
+
+  Definition unlockR l : det_action :=
+    λ σ, match slock σ !! l with
+           | Some (rlock (S n)) => {| sbuf := sbuf σ; sind := sind σ; stime := stime σ;
+                                      slock := <[l := rlock n]> (slock σ) |}
+           | _ => σ
+           end.
+  Lemma unlockRP σ l n : slock σ !! l = Some (rlock (S n)) -> slock (unlockR l σ) !! l = Some (rlock n).
+  Proof. move => H. by rewrite /unlockR H /= lookup_insert. Qed.
+
+  Definition unlockW l : det_action :=
+    λ σ, match slock σ !! l with
+           | Some (wlock) => {| sbuf := sbuf σ; sind := sind σ; stime := stime σ;
+                                      slock := <[l := rlock 0]> (slock σ) |}
+           | _ => σ
+           end.
+  Lemma unlockWP σ l : slock σ !! l = Some (wlock) -> slock (unlockW l σ) !! l = Some (rlock 0).
+  Proof. move => H. by rewrite /unlockW H /= lookup_insert. Qed.
+
+  Definition set_sbuf sb : det_action :=
+    λ σ, {| sbuf := sb; sind := sind σ; stime := stime σ; slock := slock σ |}.
+  
+  Definition set_sind si : det_action :=
+    λ σ, {| sbuf := sbuf σ; sind := si; stime := stime σ; slock := slock σ |}.
+  
+  Definition set_stime st : det_action :=
+    λ σ, {| sbuf := sbuf σ; sind := sind σ; stime := st; slock := slock σ |}.
+  
+  Definition set_slock sl : det_action :=
+    λ σ, {| sbuf := sbuf σ; sind := sind σ; stime := stime σ; slock := sl |}.
+  
+  Definition add_event π evt : det_action :=
+    λ σ, match sbuf σ !! π  with
+         | Some b => set_sbuf (<[π := evt :: b]> $ sbuf σ) σ
+         | _ => σ
+         end.
+  
+  
+  Local Open Scope positive.
+
+  Definition inc_time l : det_action :=
+    λ σ, match stime σ !! l with
+         | Some (ts1, ts2) => set_stime (<[l := (ts1, 1 + ts2)]> $ stime σ) σ
+         | _ => σ
+         end.
+      
+  Instance FinMap_Filter `{FinMap K M} {A} : Filter (K * A) (M A) :=
+    λ P H, map_imap (λ k a, if decide (P (k,a)) then Some a else None). 
+
+  Definition add_from {K A}  `{Insert K A M} (l : list (K * A)) : M -> M :=
+    fold_left (λ m' (xv : _*_), let (x,v) := xv in <[x := v]>m') l.
+  Notation "<( ek := ev | x , v <- m & C )>" :=
+    (add_from (map_to_list (base.filter (λ xv,  match xv with (x,v) => C end ) m)))
+      (at level 0).
+
+  Definition allocatedS (σ_T : gmap loc (timestamp*timestamp)) : gset loc :=
+    dom (gset loc) (base.filter (λ lts, match lts with (l, ts) => ts.1 < ts.2 end) σ_T).
+  Definition initializedS (σ_T : gmap loc (timestamp*timestamp)) : gset loc :=
+    dom (gset loc) (base.filter (λ lts, match lts with (l, ts) => ts.1 + 1 < ts.2 end) σ_T).
+  Definition deallocatedS (σ_T : gmap loc (timestamp*timestamp)) : gset loc :=
+    dom (gset loc) (base.filter (λ lts, match lts with (l, ts) => ts.1 = ts.2 end) σ_T).
+
+  Definition current_ts (σ_T : gmap loc (timestamp*timestamp)) l ts := ∃ ts_p ts', σ_T !! l = Some (ts_p, ts') ∧ ts > ts_p.
+    
+
+  Require Import iris.prelude.co_pset.
+  
+  Definition unusedS (σ_T : gmap loc (timestamp * timestamp)) : coPset := ⊤ ∖ (dom _ σ_T).
+
+  Definition freeS σ_T := (unusedS σ_T) ∪ (of_gset (deallocatedS σ_T)). 
+
+  Definition pre_cond := state -> Prop.
+  Bind Scope pre_cond_scope with pre_cond. 
+  Delimit Scope pre_cond_scope with pre.
+
+  Bind Scope action_scope with action.
+  Delimit Scope action_scope with act.
+
+  Definition with_buf : (thread -> buf -> action) -> thread -> action :=
+    λ A π σ σ', ∀ b, ∀ Hb : sbuf σ !! π = Some b, (A π b σ σ')%act.
+
+  Definition with_ts l : (timestamp -> timestamp -> action) -> action :=
+    λ A σ σ', ∀ ts1 ts2, ∀ Hts : stime σ !! l = Some (ts1, ts2), (A ts1 ts2 σ σ')%act.
+  
+  Definition with_lock l : (nalock -> action) -> action :=
+    λ A σ σ', ∀ lk, ∀ Hts : slock σ !! l = Some lk, (A lk σ σ')%act.
+
+  Definition with_reads b (l : loc) : (event -> action) -> action :=
+    λ A,  λ σ σ', ∀ e, ∀ Heb : b !! l = Some e, A e σ σ'.
+  
+  Infix "∧" := (λ p1 p2 σ, p1 σ ∧ p2 σ) : pre. 
+  
+  Infix ">>" := (λ a a' σ σ', (a σ σ')  ∧ (a' σ σ')) (at level 11). 
+
+  Definition preapp `(x : X) `(f : X -> Y) := f x.
+  Definition assert : list pre_cond -> action := λ P σ _, foldr (∧) True (map (preapp σ) P).
+  Arguments assert _%pre _ _.
+
+  Definition exec : list det_action -> action := λ A σ σ', σ' = foldr (λ a σ, a σ) σ A.
+
+  Definition allocated l : pre_cond := λ σ, l ∈ allocatedS (stime σ). 
+
+  Definition initialized l : pre_cond := λ σ, l ∈ initializedS (stime σ).
+  Definition current l t : pre_cond := λ σ, current_ts (stime σ) l t.
+  
+  Definition store_na (l : loc) (v' : raval) : thread -> action :=
+    with_buf $ λ π _,
+    with_ts l $ λ _ ts2,
+    assert [lockedW l; allocated l]
+           >> exec
+           [ add_event π (mkevent l v' (1 + ts2))
+           ; inc_time l
+           ; unlockW l].
+
+  Definition reads b (e : event) := b !! weloc e = Some e.
+
+  Definition load_na (l : loc) (v : raval) : thread -> action :=
+    with_buf $ λ π b,
+    with_reads b l $ λ e, 
+    assert [lockedR l; current l $ wetime e]
+           >> exec [unlockR l].
+
+  Definition store_at (l : loc) (v' : raval) : thread -> action :=
+    with_buf $ λ π _,
+    with_ts l $ λ _ ts2,
+    assert [unlocked l; allocated l]
+           >> exec
+           [add_event π (mkevent l v' (1 + ts2))
+           ; inc_time l].
+  
+  Definition load_at (l : loc) (v : raval) : thread -> action :=
+    with_buf $ λ π b,
+    with_reads b l $ λ e, 
+    assert [unlocked l; current l $ wetime e].
+
+  Definition pure p : pre_cond := (λ _, p)%pre.
+  
+  Definition scas_wait l (v_o v_n : raval) : thread -> action :=
+    with_buf $ λ π b,
+    with_reads b l $ λ e,
+    with_ts l $ λ _ ts2,
+    assert [initialized l; pure $ (wetime e < ts2) ].
+  
+  Definition scas_fail l (v_o v_n : raval) : thread -> action :=
+    with_buf $ λ π b,
+    with_reads b l $ λ e,
+    with_ts l $ λ _ ts2,
+    assert [initialized l; pure $ (wetime e = ts2); pure $ (weval e ≠ v_o)]
+           >> exec [ inc_time l].
+  
+  Definition scas_succ l v_o v_n : thread -> action :=
+    with_buf $ λ π b,
+    with_reads b l $ λ e,
+    with_ts l $ λ _ ts2,
+    assert [initialized l; pure $ (wetime e = ts2); pure $ (weval e = v_o)]
+           >> exec
+           [ add_event π (mkevent l v_n (1 + ts2))
+           ; inc_time l].
+    
+    
+  
+  Inductive store_na (l : loc) (v' : raval) : thread_action :=
+  | StoreA σ σ' : with_buf () σ σ' -> store_na l v' σ σ'  
+  
+  Inductive store_action (l : loc) (v' : raval) π σ σ'  : Prop :=
+  | StoreA :
+      ∀ bπ, ∀ Hbπ : sbuf σ !! π = Some bπ,
+        ∀ ts, ∀ Hlts : stime σ !! l = Some ts,
+          ∀ Hlk : slock σ !! l = Some 0,
+          ∀ eπ, ∀ He : bπ !! l = Some eπ,
+            ∀ (Ht : (ts.2 > wetime eπ)%positive)
+              (Hσ' : σ' = {|
+                       sbuf := <[π := (mkevent l v' (ts.2)) :: bπ]>(sbuf σ);
+                       sind := sind σ;
+                       stime := <[l := incts ts]>(stime σ);
+                       slock
+                     |}),
+              store_action l v' π σ σ'
+  .
+  Inductive scas_succ l v_o v_n π σ σ' : Prop :=
+  | SCasSucA:
+      ∀ bπ, ∀ Hbπ : sbuf σ !! π = Some bπ,
+        ∀ ts, ∀ Hts : stime σ !! l = Some ts,
+          ∀ eπ, ∀ Heπ : bπ !! l = Some eπ,
+            ∀ (Hv_o : weval eπ = v_o)
+              (Ht : wetime eπ = ts.2),
+              σ' = {|
+                sbuf := <[π := (mkevent l v_n (ts.2 + 1)) :: bπ]>(sbuf σ);
+                sind := sind σ;
+                stime := <[l:= incts ts]>(stime σ)
+              |} ->
+              scas_succ l v_o v_n π σ σ'
+  .
+
+  Inductive scas_fail l v_o π σ σ' : Prop :=
+  | SCasFailA:
+      ∀ bπ, ∀ Hbπ : sbuf σ !! π = Some bπ,
+        ∀ ts, ∀ Hts : stime σ !! l = Some ts,
+          ∀ eπ, ∀ Heπ : bπ !! l = Some eπ,
+            ∀ (Hv_o : weval eπ = v_o)
+              (Ht : wetime eπ = ts.2),
+              weval eπ ≠ v_o ->
+              σ' = σ ->
+              scas_fail l v_o π σ σ'
+  .
+
+  Inductive scas_wait l v_o π σ σ' : Prop :=
+  | SCasWaitA:
+      ∀ bπ, ∀ Hbπ : sbuf σ !! π = Some bπ,
+        ∀ ts, ∀ Hts : stime σ !! l = Some ts,
+          ∀ eπ, ∀ Heπ : bπ !! l = Some eπ,
+            ∀ (Hv_o : weval eπ = v_o)
+              (Ht : wetime eπ < ts.2),
+              σ' = σ ->
+              scas_wait l v_o π σ σ'
+  .
+
+  (* Definition merge_right {A B} `{Countable A} : _ -> _ -> gmap A B := *)
+  (*   base.merge (λ vl vr, if vr is Some _ then vr else vl). *)
+  
+  Lemma lookupP `{FinMap K M} {A} (m : M A) k ki a ai:
+    <[ki := ai]>m !! k = Some a ->
+    k = ki /\ a = ai
+              \/ k ≠ ki /\ m !! k = Some a.
+  Proof.
+    case: (decide (k = ki)) => [->|NE].
+    - rewrite lookup_insert => [[]]; by intuition.
+    - rewrite lookup_insert_ne; by intuition.
+  Qed.
+
+  Lemma lookup_add_from `{FinMap K M} {A} (l : list (K * A)) (m : M A) k v :
+    add_from l m !! k = Some v -> (k,v) ∈ l \/ m !! k = Some v.
+  Proof.
+    elim: l m k v => [|[k v] l IHl] ? ? ? /=; first by intuition.
+    move/IHl => []; first by (left; right).
+    move => T. apply lookupP in T.
+    case: T.
+    - move => [-> ->]. by do 2!left.
+    - by intuition. 
+  Qed.
+
+
+  Definition fork_sind_to (π ρ : thread) (l inds : ind_map) : ind_map :=
+    <( (k.1,ρ) := v | k, v <- l & k.2 = π )> inds.
+  Definition fork_sind_from (π ρ : thread) (l inds : ind_map) : ind_map :=
+    <( (ρ, k.2) := v | k, v <- l & k.1 = π )> inds.
+  
+  (* Definition fork_sind_to π ρ (inds : ind_map) : ind_map := *)
+  (*   let old_foreign := filter (λ kkv, decide ((fst ∘ fst) kkv = π)) (gmap_to_list inds) in *)
+  (*   let new_foreign := map (λ kkv, ((ρ, snd (fst kkv)), snd kkv)) old_foreign in *)
+  (*   merge_right (inds) (map_of_list new_foreign). *)
+
+  (* Definition fork_sind_from π ρ (inds : ind_map) : ind_map := *)
+  (*   let foreign_old := filter (λ kkv, decide ((snd ∘ fst) kkv = π)) (gmap_to_list inds) in *)
+  (*   let foreign_new := map (λ kkv, ((fst (fst kkv), ρ), snd kkv)) foreign_old in *)
+  (*   merge_right (inds) (map_of_list foreign_new). *)
+
+  (* Instance : Insert (thread * thread) index ind_map := λ t i m, <[t := i]>m . *)
+
+  Inductive fork_succ (π ρ : thread) σ σ' : Prop :=
+  | ForkA:
+      ∀ bπ, ∀ Hbπ : sbuf σ !! π = Some bπ,
+          sbuf σ !! ρ = None ->
+          σ' = {| sbuf := <[ρ := bπ]>(sbuf σ)
+                  ; stime := stime σ
+                  ; sind := <( (k.1, p) := v | k, v <- sind σ & k.2 = π )>
+                            (<( (ρ, k.2) := v | k, v <- sind σ & k.1 = π )>
+                            (sind σ))
+               |} ->
+          fork_succ π ρ σ σ'
+  .
+
+
+  Definition open_intv (l : positive) (n : positive) : coPset :=
+    (Pos.iter (λ si, (si.1 ∪ {[si.2]}, si.2 + 1)) (∅, l) n).1.
+  
+  Inductive alloc_succ (l : loc) (n : positive) (σ σ' : state) : Prop :=
+  | AllocA:
+        ∀ (HF : open_intv l n ⊆ free (stime σ)),
+          σ' = {| sbuf := (sbuf σ)
+                  ; stime := <[l := (1,2) ]>(stime σ)
+                  ; sind := sind σ
+               |} ->
+          alloc_succ l n σ σ'.
+
+  Inductive free_succ π (l : loc) : Prop :=
+  | FreeA :
+      ∀ (HA : loc ∈ allocated (stime σ)),
+        
+  
+  Inductive process_succ π σ σ' : Prop :=
+  | ProcessSuccA ρ :
+      ∀ Hπρ : π ≠ ρ,
+      ∀ bπ, ∀ Hbπ : sbuf σ !! π = Some bπ,
+        ∀ bρ, ∀ Hbρ : sbuf σ !! ρ = Some bρ,
+          ∀ i, ∀ Hind : sind σ !! (π, ρ) = Some i,
+            ∀ Hi : (i < List.length bρ)%nat,
+            ∀ eρ, ∀ Heρ : bρ !! (List.length bρ - S i)%nat = Some eρ,
+              ∀ eπ, ∀ Heπ : bπ !! weloc eρ = Some eπ,
+                ∀ Ht : wetime eρ > wetime eπ,
+                ∀ Hσ : σ' = {| sbuf := <[π := eρ :: bπ]>(sbuf σ)
+                               ; sind := <[(π,ρ) := S i]>(sind σ)
+                               ; stime := stime σ
+                            |},
+                  process_succ π σ σ'.
+
+  Inductive process_skip π σ σ' : Prop :=
+  | ProcessSkipA ρ :
+      ∀ bπ, ∀ Hbπ : sbuf σ !! π = Some bπ,
+        ∀ bρ, ∀ Hbρ : sbuf σ !! ρ = Some bρ,
+          ∀ i, ∀ Hind : sind σ !! (π, ρ) = Some i,
+            ∀ Hi : (i < List.length bρ)%nat,
+            ∀ eρ, ∀ Heρ : bρ !! (List.length bρ - S i)%nat = Some eρ,
+              ∀ eπ, ∀ Heπ : bπ !! weloc eρ = Some eπ,
+                ∀ Ht : wetime eρ <= wetime eπ,
+                ∀ Hσ : σ' = {| sbuf := (sbuf σ)
+                               ; sind := <[(π,ρ) := S i]>(sind σ)
+                               ; stime := stime σ
+                            |},
+                  process_skip π σ σ'.
+  
+  Inductive process_fail π σ σ' : Prop :=
+  | ProcessFailA :
+      ∀ HA : (∀ ρ,
+                 ∀ bπ, ∀ Hbπ : sbuf σ !! π = Some bπ,
+                     ∀ bρ, ∀ Hbρ : sbuf σ !! ρ = Some bρ,
+                         ∀ i, ∀ Hind : sind σ !! (π, ρ) = Some i,
+                             (i > size bρ)%nat
+             ),
+      ∀ Hσ : σ' = σ,
+        process_fail π σ σ'.
+  
+
+  Inductive impure_step : expr [] -> state -> expr [] -> state -> option (expr []) -> Prop :=
+  | LoadS π l σ (b : buf) :
+      ∀ b, ∀ Hb : sbuf σ !! π = Some b,
+        ∀ e, ∀ He : b !! l = Some e,
+            impure_step (Load (Loc l), π) σ
+                        (Lit (LitInt (weval e)), π) σ
+                        None
+  | StoreS π e l v' σ σ':
+      ∀ He : e = Lit (LitInt v'),
+      ∀ HAct : store_action l v' π σ σ',
+        impure_step (Store (Loc l) e, π) σ
+                    (Lit LitUnit, π) σ'
+                    None
+  | SCasSucS π e1 e2 l v_o v_n σ σ': 
+      ∀ He1 : e1 = Lit (LitInt v_o),
+      ∀ He2 : e2 = Lit (LitInt v_n),
+      ∀ HAct : scas_succ l v_o v_n π σ σ',
+        impure_step (SCAS (Loc l) e1 e2, π) σ
+                    (Lit $ LitBool true, π) σ'
+                    None
+  | SCasFailS π e1 e2 l (v_o v_n : raval) σ σ':
+      ∀ He1 : e1 = Lit (LitInt v_o),
+      ∀ He2 : e2 = Lit (LitInt v_n),
+      ∀ HAct : scas_fail l v_o π σ σ',
+        impure_step (SCAS (Loc l) e1 e2, π) σ
+                    (Lit $ LitBool true, π) σ'
+                    None
+  | SCasWaitS π e1 e2 l v_o v_n σ σ':
+      ∀ He1 : e1 = Lit (LitInt v_o),
+      ∀ He2 : e2 = Lit (LitInt v_n),
+      ∀ HAct : scas_wait l v_o π σ σ',
+        impure_step (SCAS (Loc l) e1 e2, π) σ
+                    (Lit $ LitBool true, π) σ'
+                    None
+  | ForkS π ρ e (σ σ' : state):
+      ∀ HAct : fork_succ π ρ σ σ',
+        impure_step (Fork e, π) σ (Lit LitUnit, π) σ' (Some (e, ρ))
+  | AllocS e π v σ σ' l :
+      ∀ He : e = (Lit (LitInt v)),
+      ∀ HAct : alloc_succ π l v σ σ',
+        impure_step (Alloc e, π) σ (Loc l, π) σ' None
+  | ProcessS π σ σ':
+      ∀ HAct : process_succ π σ σ',
+        impure_step (Process, π) σ (Lit LitUnit,π) σ' None
+  | ProcessSkip π σ σ':
+      ∀ HAct : process_skip π σ σ',
+        impure_step (Process, π) σ (Lit LitUnit,π) σ' None
+  | ProcessFail π σ σ':
+      ∀ HAct : process_fail π σ σ',
+        impure_step (Process, π) σ (Lit LitUnit,π) σ' None
+  .
+
+
+  Inductive head_step : expr [] -> state -> expr [] -> state -> option (expr []) -> Prop :=
+  | head_pure (i : thread) e1 σ1 e2 σ2 ef (HStep : pure_step e1 σ1 e2 σ2 ef) : head_step (e1, i) σ1 (e2, i) σ1 ((λ e, pair e i) <$> ef)
+  | head_impure e1 σ1 e2 σ2 ef (HStep : impure_step e1 σ1 e2 σ2 ef) : head_step e1 σ1 e2 σ2 ef
+  .
+  Definition ectx_item := BaseExpr.ectx_item.
+  Definition fill_item (Ki : BaseExpr.ectx_item) (e : expr []) : expr [] :=
+    (BaseExpr.fill_item Ki (bexpr e), pid e).
+
+  (** Close reduction under evaluation contexts.
+We could potentially make this a generic construction. *)
+  (* Inductive prim_step *)
+  (*     (e1 : expr) (σ1 : state) (e2 : expr) (σ2: state) (ef: option real_expr) : Prop := *)
+  (*   Ectx_step K e1' e2' : *)
+  (*     e1 = fill K e1' → e2 = fill K e2' → *)
+  (*     head_step e1' σ1 e2' σ2 ef → prim_step e1 σ1 e2 σ2 ef. *)
+
+  (** Basic properties about the language *)
+  Lemma to_of_val v : to_val (of_val v) = Some v.
+  Proof. destruct v; by rewrite /to_val to_of_val. Qed.
+
+  Lemma of_to_val e v : to_val e = Some v → of_val v = e.
+  Proof.
+    rewrite /to_val /of_val; move: e => [] e pid.
+    case H: (BaseExpr.to_val _); [|discriminate].
+      by move : H => /of_to_val /= <- [] <-.
+  Qed.
+
+  Instance: Inj (=) (=) of_val.
+  Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
+
+  Instance fill_item_inj (Ki : ectx_item) : Inj (=) (=) (fill_item Ki).
+  Proof. destruct Ki; intros ???; simplify_eq/=; try destruct x,y; subst; auto with f_equal. Qed.
+
+
+  Lemma fill_item_val Ki e :
+    is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
+  Proof.
+    destruct e; rewrite /to_val => /fmap_is_Some H; apply/fmap_is_Some.
+    exact: fill_item_val H.
+  Qed.
+
+
+  Lemma val_stuck e1 σ1 e2 σ2 ef :
+    head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
+  Proof. destruct 1; destruct HStep; naive_solver. Qed.
+
+  Lemma atomic_not_val e : atomic e → to_val e = None.
+  Proof. by move: e => [[]]. Qed.
+
+  Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) → is_Some (to_val e).
+  Proof.
+    rewrite /atomic /fill_item => H. apply/fmap_is_Some. exact: atomic_fill_item H.  
+  Qed.
+
+  Lemma atomic_step e1 σ1 e2 σ2 ef :
+    atomic e1 → head_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
+  Proof.
+    destruct 2; [apply/fmap_is_Some; exact: atomic_step|]; simpl;
+      destruct HStep; rewrite /to_val /=; now eauto.
+  Qed.
+
+  Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
+    head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
+  Proof.
+    move => H; apply/fmap_is_Some. inversion_clear H; [exact: head_ctx_step_val|].
+    rewrite /fill_item in HStep.
+    destruct e, Ki; simpl in HStep; inversion_clear HStep; subst; eauto.
+  Qed.
+
+  Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
+    to_val e1 = None → to_val e2 = None →
+    fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
+  Proof.
+    move => /fmap_None H1 /fmap_None H2 HK.
+    apply: fill_item_no_val_inj; [exact: H1|exact H2|].
+    rewrite /fill_item in HK.
+    inversion HK.
+    now eauto.
+  Qed.
+
+
+  (** Equality and other typeclass stuff *)
+  Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
+  Proof. solve_decision. Defined.
+  Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
+  Proof. solve_decision. Defined.
+  Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
+  Proof. solve_decision. Defined.
+
+End sra_lang.
+
+(** Language *)
+Program Instance ra_ectxi_lang :
+  EctxiLanguage
+    (sra_lang.expr []) sra_lang.val sra_lang.ectx_item sra_lang.state :=
+  {|
+    of_val := sra_lang.of_val; to_val := sra_lang.to_val;
+    fill_item := sra_lang.fill_item; 
+    atomic := sra_lang.atomic; head_step := sra_lang.head_step;
+  |}.
+Solve Obligations with eauto using sra_lang.to_of_val, sra_lang.of_to_val,
+                       sra_lang.val_stuck, sra_lang.atomic_not_val, sra_lang.atomic_step,
+                       sra_lang.fill_item_val, sra_lang.atomic_fill_item,
+                       sra_lang.fill_item_no_val_inj, sra_lang.head_ctx_step_val.
+
+Canonical Structure sra_lang := ectx_lang (sra_lang.expr []).
+
+(* Prefer heap_lang names over ectx_language names. *)
+Export sra_lang.
\ No newline at end of file
diff --git a/coq/sra/lifting.v b/coq/sra/lifting.v
new file mode 100644
index 0000000000000000000000000000000000000000..3f56e54b9c5e0fb6bdb197e765346dd97742e6aa
--- /dev/null
+++ b/coq/sra/lifting.v
@@ -0,0 +1,54 @@
+From iris.program_logic Require Export ectx_weakestpre.
+From iris.program_logic Require Import ownership. (* for ownP *)
+From ra Require Export lang.
+(* From iris.heap_lang Require Import tactics. *)
+From iris.proofmode Require Import weakestpre.
+Import uPred.
+(* Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2. *)
+
+Section lifting.
+Context {Σ : iFunctor}.
+Implicit Types P Q : iProp ra_lang Σ.
+Implicit Types Φ : val → iProp ra_lang Σ.
+Implicit Types ef : option (expr []).
+
+(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
+Lemma wp_bind {E e} K Φ :
+  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+Proof. exact: wp_ectx_bind. Qed.
+
+Lemma wp_bindi {E e} Ki Φ :
+  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
+     WP fill_item Ki e @ E {{ Φ }}.
+Proof. exact: weakestpre.wp_bind. Qed.
+
+(** Base axioms for core primitives of the language: Stateful reductions. *)
+Lemma wp_alloc_pst E σ π e (v : raval) bπ Φ :
+  e = Lit (LitInt v) →
+  sbuf σ !! π = Some bπ →
+  (▷ ownP σ ★ ▷ (∀ l ts, stime σ !! l = None ∧
+                      ownP ({| sbuf := <[π := (mkevent l v ts) :: bπ]>(sbuf σ);
+                                      sind := sind σ;
+                                      stime := <[l := {[ts]}]>(stime σ) |})
+                      -★ Φ (LocV l, π)))
+  ⊢ WP (Alloc e,π) @ E {{ Φ }}.
+Proof.
+  iIntros {? ?}  "[HP HΦ]".
+  (* TODO: This works around ssreflect bug #22. *)
+  set (φ (e' : expr []) σ' ef := ∃ l ts,
+    ef = None ∧ e' = (Loc l, π) ∧ σ' = {| sbuf := <[π := (mkevent l v ts) :: bπ]>(sbuf σ);
+                                      sind := sind σ;
+                                      stime := <[l := {[ts]}]>(stime σ) |} ∧ stime σ !! l = None).
+  iApply (wp_lift_atomic_head_step (Alloc e,π) φ σ); try (by simpl; eauto).
+  - by rewrite H.
+  - econstructor. eexists. exists None. constructor. econstructor => [//|].
+    econstructor => [//| |//]. instantiate (1 := fresh (dom _ (stime σ))).
+    by apply (not_elem_of_dom (D:=gset _)), is_fresh.
+  - move => ? ? ?. inversion 1; subst; first by inversion HStep.
+    inversion_clear HStep; subst. inversion_clear HAct; subst.
+    exists l, 1%positive. by naive_solver.
+  iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]".
+  (* FIXME: I should not have to refer to "H0". *)
+  destruct H1 as (l & ? & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
+  iSplit; last done. iApply "HΦ"; by iSplit.
+Qed.