diff --git a/src/program_proof/tulip/base.v b/src/program_proof/tulip/base.v
index 7bed63564..839995456 100644
--- a/src/program_proof/tulip/base.v
+++ b/src/program_proof/tulip/base.v
@@ -1,3 +1,6 @@
+From iris.algebra Require Import mono_nat mono_list gmap_view gset.
+From iris.algebra.lib Require Import dfrac_agree.
+From Perennial.base_logic Require Import ghost_map mono_nat saved_prop.
 From Perennial.program_proof Require Import grove_prelude.
 From Perennial.Helpers Require finite.
 
@@ -287,13 +290,158 @@ Definition valid_ccommand gid (c : ccommand) :=
   | CmdAbort ts => valid_ts ts
   end.
 
-Class tulip_ghostG (Σ : gFunctors).
+Inductive vote :=
+| Accept (d : bool)
+| Reject.
+
+#[global]
+Instance vote_eq_decision :
+  EqDecision vote.
+Proof. solve_decision. Qed.
+
+Definition ballot := list vote.
+
+Canonical Structure dbvalO := leibnizO dbval.
+Definition dbmapR := gmapR dbkey (dfrac_agreeR dbvalO).
+Definition histR := mono_listR dbvalO.
+Definition histmR := gmapR dbkey histR.
+Definition tsmR := gmapR dbkey (dfrac_agreeR natO).
+Canonical Structure dbkmodO := leibnizO dbkmod.
+Definition dbkmodR := gmapR dbkey (dfrac_agreeR dbkmodO).
+Canonical Structure boolO := leibnizO bool.
+Canonical Structure natboolmvR := gmap_viewR nat (agreeR boolO).
+Definition group_natboolmvR := gmapR u64 natboolmvR.
+Canonical Structure ppslmR := gmap_viewR (nat * nat) (agreeR boolO).
+Definition group_ppslmR := gmapR u64 ppslmR.
+Definition replica_tssR := gmapR (u64 * u64) (gmap_viewR nat unitR).
+Definition vdlR := mono_listR boolO.
+Definition replica_kvdlR := gmapR (u64 * u64 * dbkey) vdlR.
+Canonical Structure clogO := leibnizO (list ccommand).
+Definition replica_clogR := gmapR (u64 * u64) (dfrac_agreeR clogO).
+Canonical Structure ilogO := leibnizO (list (nat * icommand)).
+Definition replica_ilogR := gmapR (u64 * u64) (dfrac_agreeR ilogO).
+Canonical Structure voteO := leibnizO vote.
+Definition ballotR := mono_listR voteO.
+Definition ballotmR := gmap_viewR nat ballotR.
+Definition replica_ballotmR := gmapR (u64 * u64) ballotmR.
+Canonical Structure coordidO := leibnizO coordid.
+Definition votemR := gmap_viewR (nat * nat) (agreeR coordidO).
+Definition replica_votemR := gmapR (u64 * u64) votemR.
+Definition tokenmR := gmap_viewR (nat * nat * u64) unitR.
+Definition replica_tokenmR := gmapR (u64 * u64) tokenmR.
+
+Class tulip_ghostG (Σ : gFunctors) :=
+  { (* common resources defined in res.v *)
+    #[global] db_ptstoG :: inG Σ dbmapR;
+    #[global] repl_histG :: inG Σ histmR;
+    #[global] repl_tsG :: inG Σ tsmR;
+    #[global] lnrz_kmodG :: inG Σ dbkmodR;
+    #[global] cmtd_kmodG :: inG Σ dbkmodR;
+    (* txnsys resources defined in res_txnsys.v *)
+    #[global] cmtd_histG :: inG Σ histmR;
+    #[global] lnrz_histG :: inG Σ histmR;
+    #[global] txn_resG :: ghost_mapG Σ nat txnres;
+    #[global] txn_oneshot_wrsG :: ghost_mapG Σ nat (option dbmap);
+    #[global] lnrz_tidG :: ghost_mapG Σ nat unit;
+    #[global] wabt_tidG :: ghost_mapG Σ nat unit;
+    #[global] cmt_tmodG :: ghost_mapG Σ nat dbmap;
+    #[global] excl_tidG :: ghost_mapG Σ nat unit;
+    #[global] txn_client_tokenG :: ghost_mapG Σ (nat * u64) unit;
+    #[global] txn_postcondG :: ghost_mapG Σ nat (dbmap -> Prop);
+    #[global] largest_tsG :: mono_natG Σ;
+    (* TODO: proph *)
+    (* group resources defined in res_group.v *)
+    #[global] group_prepG :: inG Σ group_natboolmvR;
+    #[global] group_ppslG :: inG Σ group_ppslmR;
+    #[global] group_commitG :: inG Σ group_natboolmvR;
+    (* replica resources defined in res_replica.v *)
+    #[global] replica_validated_tsG :: inG Σ replica_tssR;
+    #[global] replica_key_validationG :: inG Σ replica_kvdlR;
+    #[global] replica_clogG :: inG Σ replica_clogR;
+    #[global] replica_ilogG :: inG Σ replica_ilogR;
+    #[global] replica_ballotG :: inG Σ replica_ballotmR;
+    #[global] replica_voteG :: inG Σ replica_votemR;
+    #[global] replica_tokenG :: inG Σ replica_tokenmR;
+  }.
+
+Definition tulip_ghostΣ :=
+  #[ (* res.v *)
+     GFunctor dbmapR;
+     GFunctor histmR;
+     GFunctor tsmR;
+     GFunctor dbkmodR;
+     GFunctor dbkmodR;
+     GFunctor histmR;
+     GFunctor histmR;
+     (* res_txnsys.v *)
+     GFunctor histmR;
+     GFunctor histmR;
+     ghost_mapΣ nat txnres;
+     ghost_mapΣ nat (option dbmap);
+     ghost_mapΣ nat unit;
+     ghost_mapΣ nat unit;
+     ghost_mapΣ nat dbmap;
+     ghost_mapΣ nat unit;
+     ghost_mapΣ (nat * u64) unit;
+     ghost_mapΣ nat (dbmap -> Prop);
+     mono_natΣ;
+     (* TODO: proph *)
+     (* res_group.v *)
+     GFunctor group_natboolmvR;
+     GFunctor group_ppslmR;
+     GFunctor group_natboolmvR;
+     (* res_replica.v *)
+     GFunctor replica_tssR;
+     GFunctor replica_kvdlR;
+     GFunctor replica_clogR;
+     GFunctor replica_ilogR;
+     GFunctor replica_ballotmR;
+     GFunctor replica_votemR;
+     GFunctor replica_tokenmR
+   ].
+
+#[global]
+Instance subG_tulip_ghostG {Σ} :
+  subG tulip_ghostΣ Σ → tulip_ghostG Σ.
+Proof. solve_inG. Qed.
+
+Record tulip_names :=
+  { (* res.v *)
+    db_ptsto : gname;
+    repl_hist : gname;
+    repl_ts : gname;
+    lnrz_kmod : gname;
+    cmtd_kmod : gname;
+    (* res_txnsys.v *)
+    cmtd_hist : gname;
+    lnrz_hist : gname;
+    txn_res : gname;
+    txn_oneshot_wrs : gname;
+    lnrz_tid : gname;
+    wabt_tid : gname;
+    cmt_tmod : gname;
+    excl_tid : gname;
+    txn_client_token : gname;
+    txn_postcond : gname;
+    largest_ts : gname;
+    (* TODO: proph *)
+    (* res_group.v *)
+    group_prep : gname;
+    group_prepare_proposal : gname;
+    group_commit : gname;
+    (* res_replica.v *)
+    replica_validated_ts : gname;
+    replica_key_validation : gname;
+    replica_clog : gname;
+    replica_ilog : gname;
+    replica_ballot : gname;
+    replica_vote : gname;
+    replica_token : gname;
+  }.
 
-Record tulip_names := {}.
 Record replica_names := {}.
 
 Definition sysNS := nroot .@ "sys".
 Definition tulipNS := sysNS .@ "tulip".
 Definition tsNS := sysNS .@ "ts".
 Definition txnlogNS := sysNS .@ "txnlog".
-
diff --git a/src/program_proof/tulip/invariance/propose.v b/src/program_proof/tulip/invariance/propose.v
index 4b2457a57..e105aca55 100644
--- a/src/program_proof/tulip/invariance/propose.v
+++ b/src/program_proof/tulip/invariance/propose.v
@@ -15,8 +15,12 @@ Section propose.
     do 2 iNamed "Hgroup". iNamed "Hpsm".
     destruct (psm !! ts) as [ps |] eqn:Hpsmts; last first.
     { (* Case: [psm !! ts = None]. *)
-      iMod (group_prepare_proposal_init ts {[rk := p]} with "Hpsm") as "Hpsm".
+      iMod (group_prepare_proposal_init ts with "Hpsm") as "Hpsm".
       { apply Hpsmts. }
+      iMod (group_prepare_proposal_insert ts _ rk p with "Hpsm") as "Hpsm".
+      { by rewrite lookup_insert. }
+      { done. }
+      rewrite insert_empty insert_insert.
       iDestruct (group_prepare_proposal_witness ts _ rk p with "Hpsm") as "#Hpsl".
       { by rewrite lookup_insert. }
       { by rewrite lookup_singleton. }
diff --git a/src/program_proof/tulip/paxos/program/paxos_submit.v b/src/program_proof/tulip/paxos/program/paxos_submit.v
index 7cd7c23af..f958ef111 100644
--- a/src/program_proof/tulip/paxos/program/paxos_submit.v
+++ b/src/program_proof/tulip/paxos/program/paxos_submit.v
@@ -12,7 +12,6 @@ Section submit.
     <<< ∀∀ cpool, own_cpool_half γ cpool >>>
       Paxos__Submit #px #(LitString c) @ ↑paxosNS
     <<< own_cpool_half γ ({[c]} ∪ cpool) >>>
-    (* TODO: return a receipt for checking committedness from the client. *)
     {{{ (lsn : u64) (term : u64), RET (#lsn, #term); True }}}.
   Proof.
     iIntros "#Hinv" (Φ) "!> _ HAU".
diff --git a/src/program_proof/tulip/res.v b/src/program_proof/tulip/res.v
index bc6a72c71..835823e75 100644
--- a/src/program_proof/tulip/res.v
+++ b/src/program_proof/tulip/res.v
@@ -1,4 +1,5 @@
-(** Global resources. *)
+From iris.algebra Require Import mono_nat mono_list gmap_view gset.
+From iris.algebra.lib Require Import dfrac_agree.
 From Perennial.program_proof Require Import grove_prelude.
 From Perennial.program_proof.tulip Require Import base.
 From Perennial.program_proof.rsm Require Import big_sep.
@@ -19,8 +20,8 @@ Section res.
     (** Single-value logical database values. One half in the txnsys invariant,
     one half given to the client. *)
 
-    Definition own_db_ptsto γ (k : dbkey) (v : dbval) : iProp Σ.
-    Admitted.
+    Definition own_db_ptsto γ (k : dbkey) (v : dbval) : iProp Σ :=
+      own γ.(db_ptsto) {[ k := (to_dfrac_agree (DfracOwn (1 / 2)) v) ]}.
 
     Definition own_db_ptstos γ (m : dbmap) : iProp Σ :=
       [∗ map] k ↦ v ∈ m, own_db_ptsto γ k v.
@@ -29,13 +30,26 @@ Section res.
       own_db_ptsto γ k v1 -∗
       own_db_ptsto γ k v2 ==∗
       own_db_ptsto γ k v ∗ own_db_ptsto γ k v.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iCombine "Hv1 Hv2" as "Hv".
+      rewrite -own_op singleton_op.
+      iApply (own_update with "Hv").
+      apply singleton_update.
+      apply dfrac_agree_update_2.
+      by rewrite dfrac_op_own Qp.half_half.
+    Qed.
 
     Lemma db_ptsto_agree γ k v1 v2 :
       own_db_ptsto γ k v1 -∗
       own_db_ptsto γ k v2 -∗
       ⌜v2 = v1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iDestruct (own_valid_2 with "Hv1 Hv2") as %Hvalid.
+      rewrite singleton_op singleton_valid dfrac_agree_op_valid_L in Hvalid.
+      by destruct Hvalid as [_ ?].
+    Qed.
 
   End db_ptsto.
 
@@ -44,11 +58,11 @@ Section res.
     (** History generated by replicated transactions for a certain key. One half
     owned by the txnsys invariant, the other by the key invariant. *)
 
-    Definition own_repl_hist_half γ (k : dbkey) (h : dbhist) : iProp Σ.
-    Admitted.
+    Definition own_repl_hist_half γ (k : dbkey) (h : dbhist) : iProp Σ :=
+      own γ.(repl_hist) {[ k := ●ML{#(1 / 2)} h ]}.
 
-    Definition is_repl_hist_lb γ (k : dbkey) (h : dbhist) : iProp Σ.
-    Admitted.
+    Definition is_repl_hist_lb γ (k : dbkey) (h : dbhist) : iProp Σ :=
+      own γ.(repl_hist) {[ k := ◯ML h ]}.
 
     Definition is_repl_hist_at γ (k : dbkey) (ts : nat) (v : dbval) : iProp Σ :=
       ∃ lb, is_repl_hist_lb γ k lb ∗ ⌜lb !! ts = Some v⌝.
@@ -56,21 +70,52 @@ Section res.
     #[global]
     Instance is_repl_hist_lb_persistent α key hist :
       Persistent (is_repl_hist_lb α key hist).
-    Admitted.
+    Proof. apply _. Defined.
+
+    Lemma repl_hist_agree {γ} k h1 h2 :
+      own_repl_hist_half γ k h1 -∗
+      own_repl_hist_half γ k h2 -∗
+      ⌜h2 = h1⌝.
+    Proof.
+      iIntros "Hh1 Hh2".
+      iDestruct (own_valid_2 with "Hh1 Hh2") as %Hvalid.
+      rewrite singleton_op singleton_valid mono_list_auth_dfrac_op_valid_L in Hvalid.
+      by destruct Hvalid as [_ ?].
+    Qed.
 
     Lemma repl_hist_big_agree {γ histm1 histm2} :
       dom histm1 = dom histm2 ->
       ([∗ map] k ↦ ts ∈ histm1, own_repl_hist_half γ k ts) -∗
       ([∗ map] k ↦ ts ∈ histm2, own_repl_hist_half γ k ts) -∗
       ⌜histm2 = histm1⌝.
-    Admitted.
+    Proof.
+      iIntros (Hdom) "Hhistm1 Hhistm2".
+      rewrite map_eq_iff.
+      iIntros (k).
+      destruct (histm1 !! k) as [h1 |] eqn:Hh1, (histm2 !! k) as [h2 |] eqn:Hh2.
+      { iDestruct (big_sepM_lookup with "Hhistm1") as "Hh1"; first apply Hh1.
+        iDestruct (big_sepM_lookup with "Hhistm2") as "Hh2"; first apply Hh2.
+        by iDestruct (repl_hist_agree with "Hh1 Hh2") as %->.
+      }
+      { by rewrite -not_elem_of_dom -Hdom elem_of_dom Hh1 -eq_None_not_Some in Hh2. }
+      { by rewrite -not_elem_of_dom Hdom elem_of_dom Hh2 -eq_None_not_Some in Hh1. }
+      done.
+    Qed.
 
     Lemma repl_hist_update {γ k h1} h2 :
       prefix h1 h2 ->
       own_repl_hist_half γ k h1 -∗
       own_repl_hist_half γ k h1 ==∗
       own_repl_hist_half γ k h2 ∗ own_repl_hist_half γ k h2.
-    Admitted.
+    Proof.
+      iIntros (Hprefix) "Hh1 Hh2".
+      iCombine "Hh1 Hh2" as "Hh".
+      rewrite -own_op singleton_op.
+      iApply (own_update with "Hh").
+      rewrite -mono_list_auth_dfrac_op dfrac_op_own Qp.half_half.
+      apply singleton_update.
+      by apply mono_list_update.
+    Qed.
 
     Lemma repl_hist_big_update {γ hs1} hs2 :
       map_Forall2 (λ _ h1 h2, prefix h1 h2) hs1 hs2 ->
@@ -93,13 +138,24 @@ Section res.
     Lemma repl_hist_witness {γ k h} :
       own_repl_hist_half γ k h -∗
       is_repl_hist_lb γ k h.
-    Admitted.
+    Proof.
+      iApply own_mono.
+      apply singleton_included_mono.
+      apply mono_list_included.
+    Qed.
 
     Lemma repl_hist_prefix {γ k h hlb} :
       own_repl_hist_half γ k h -∗
       is_repl_hist_lb γ k hlb -∗
       ⌜prefix hlb h⌝.
-    Admitted.
+    Proof.
+      iIntros "Hh Hlb".
+      iDestruct (own_valid_2 with "Hh Hlb") as %Hvalid.
+      iPureIntro. revert Hvalid.
+      rewrite singleton_op singleton_valid.
+      rewrite mono_list_both_dfrac_valid_L.
+      by intros [_ ?].
+    Qed.
 
     Definition repl_hist_at γ (k : dbkey) (ts : nat) (v : dbval) : iProp Σ :=
       ∃ hist, is_repl_hist_lb γ k hist ∗ ⌜hist !! ts = Some v⌝.
@@ -119,7 +175,12 @@ Section res.
       prefix hlb2 hlb1 ->
       is_repl_hist_lb γ k hlb1 -∗
       is_repl_hist_lb γ k hlb2.
-    Admitted.
+    Proof.
+      iIntros (Hprefix).
+      iApply own_mono.
+      apply singleton_included_mono.
+      by apply mono_list_lb_mono.
+    Qed.
 
   End repl_hist.
 
@@ -129,27 +190,52 @@ Section res.
     key. One half owned by the txnsys invariant, the other by the key
     invariant. *)
 
-    Definition own_repl_ts_half γ (k : dbkey) (ts : nat) : iProp Σ.
-    Admitted.
+    Definition own_repl_ts_half γ (k : dbkey) (ts : nat) : iProp Σ :=
+      own γ.(repl_ts) {[ k := (to_dfrac_agree (DfracOwn (1 / 2)) ts) ]}.
 
     Lemma repl_ts_agree {γ k ts1 ts2} :
       own_repl_ts_half γ k ts1 -∗
       own_repl_ts_half γ k ts2 -∗
       ⌜ts2 = ts1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iDestruct (own_valid_2 with "Hv1 Hv2") as %Hvalid.
+      rewrite singleton_op singleton_valid dfrac_agree_op_valid_L in Hvalid.
+      by destruct Hvalid as [_ ?].
+    Qed.
 
     Lemma repl_ts_update {γ k ts1 ts2} ts' :
       own_repl_ts_half γ k ts1 -∗
-      own_repl_ts_half γ k ts2 -∗
+      own_repl_ts_half γ k ts2 ==∗
       own_repl_ts_half γ k ts' ∗ own_repl_ts_half γ k ts'.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iCombine "Hv1 Hv2" as "Hv".
+      rewrite -own_op singleton_op.
+      iApply (own_update with "Hv").
+      apply singleton_update.
+      apply dfrac_agree_update_2.
+      by rewrite dfrac_op_own Qp.half_half.
+    Qed.
 
-    Lemma repl_ts_big_agree {γ tss1 tss2} :
-      dom tss1 = dom tss2 ->
-      ([∗ map] k ↦ ts ∈ tss1, own_repl_ts_half γ k ts) -∗
-      ([∗ map] k ↦ ts ∈ tss2, own_repl_ts_half γ k ts) -∗
-      ⌜tss2 = tss1⌝.
-    Admitted.
+    Lemma repl_ts_big_agree {γ tsm1 tsm2} :
+      dom tsm1 = dom tsm2 ->
+      ([∗ map] k ↦ ts ∈ tsm1, own_repl_ts_half γ k ts) -∗
+      ([∗ map] k ↦ ts ∈ tsm2, own_repl_ts_half γ k ts) -∗
+      ⌜tsm2 = tsm1⌝.
+    Proof.
+      iIntros (Hdom) "Htsm1 Htsm2".
+      rewrite map_eq_iff.
+      iIntros (k).
+      destruct (tsm1 !! k) as [h1 |] eqn:Hh1, (tsm2 !! k) as [h2 |] eqn:Hh2.
+      { iDestruct (big_sepM_lookup with "Htsm1") as "Hh1"; first apply Hh1.
+        iDestruct (big_sepM_lookup with "Htsm2") as "Hh2"; first apply Hh2.
+        by iDestruct (repl_ts_agree with "Hh1 Hh2") as %->.
+      }
+      { by rewrite -not_elem_of_dom -Hdom elem_of_dom Hh1 -eq_None_not_Some in Hh2. }
+      { by rewrite -not_elem_of_dom Hdom elem_of_dom Hh2 -eq_None_not_Some in Hh1. }
+      done.
+    Qed.
 
     Lemma repl_ts_big_update {γ tss} tss' :
       dom tss = dom tss' ->
@@ -157,7 +243,15 @@ Section res.
       ([∗ map] k ↦ t ∈ tss, own_repl_ts_half γ k t) ==∗
       ([∗ map] k ↦ t ∈ tss', own_repl_ts_half γ k t) ∗
       ([∗ map] k ↦ t ∈ tss', own_repl_ts_half γ k t).
-    Admitted.
+    Proof.
+      iIntros (Hdom) "Hhs1x Hhs1y".
+      iCombine "Hhs1x Hhs1y" as "Hhs1".
+      rewrite -2!big_sepM_sep.
+      iApply big_sepM_bupd.
+      iApply (big_sepM_impl_dom_eq with "Hhs1"); first done.
+      iIntros (k h1 h2 Hh1 Hh2) "!> [Hh1x Hh1y]".
+      iApply (repl_ts_update with "Hh1x Hh1y").
+    Qed.
 
   End repl_ts.
 
@@ -168,44 +262,6 @@ Section res.
     Definition own_repl_tuple_half γ (k : dbkey) (t : dbtpl) : iProp Σ :=
       own_repl_hist_half γ k t.1 ∗ own_repl_ts_half γ k t.2.
 
-    Lemma tuple_repl_agree {γ k t1 t2} :
-      own_repl_tuple_half γ k t1 -∗
-      own_repl_tuple_half γ k t2 -∗
-      ⌜t2 = t1⌝.
-    Admitted.
-
-    Lemma tuple_repl_big_agree {γ tpls1 tpls2} :
-      dom tpls1 = dom tpls2 ->
-      ([∗ map] k ↦ t ∈ tpls1, own_repl_tuple_half γ k t) -∗
-      ([∗ map] k ↦ t ∈ tpls2, own_repl_tuple_half γ k t) -∗
-      ⌜tpls2 = tpls1⌝.
-    Admitted.
-
-    Lemma tuple_repl_update {γ k t1} t2 :
-      prefix t1.1 t2.1 ->
-      own_repl_tuple_half γ k t1 -∗
-      own_repl_tuple_half γ k t1 ==∗
-      own_repl_tuple_half γ k t2 ∗ own_repl_tuple_half γ k t2.
-    Admitted.
-
-    Lemma tuple_repl_big_update {γ tpls1} tpls2 :
-      dom tpls1 = dom tpls2 ->
-      (∀ k tpl1 tpl2, tpls1 !! k = Some tpl1 -> tpls2 !! k = Some tpl2 -> prefix tpl1.1 tpl2.1) ->
-      ([∗ map] k ↦ t ∈ tpls1, own_repl_tuple_half γ k t) -∗
-      ([∗ map] k ↦ t ∈ tpls1, own_repl_tuple_half γ k t) ==∗
-      ([∗ map] k ↦ t ∈ tpls2, own_repl_tuple_half γ k t) ∗
-      ([∗ map] k ↦ t ∈ tpls2, own_repl_tuple_half γ k t).
-    Proof.
-      iIntros (Hdom Hprefix) "H1 H2".
-      iCombine "H1 H2" as "Htpls1".
-      rewrite -2!big_sepM_sep.
-      iApply big_sepM_bupd.
-      iApply (big_sepM_impl_dom_eq with "Htpls1"); first done.
-      iIntros (k tpl1 tpl2 Htpl1 Htpl2)"!> [H1 H2]".
-      iApply (tuple_repl_update with "H1 H2").
-      by eapply Hprefix.
-    Qed.
-
   End repl_tuple.
 
   Section lnrz_kmod.
@@ -213,14 +269,19 @@ Section res.
     (** Key-modification made by linearized transactions. One half owned by the
     txnsys invariant, and the other half by the group invariant. *)
 
-    Definition own_lnrz_kmod_half γ (k : dbkey) (kmod : dbkmod) : iProp Σ.
-    Admitted.
+    Definition own_lnrz_kmod_half γ (k : dbkey) (kmod : dbkmod) : iProp Σ :=
+      own γ.(lnrz_kmod) {[ k := (to_dfrac_agree (DfracOwn (1 / 2)) kmod) ]}.
 
     Lemma lnrz_kmod_agree {γ k m1 m2} :
       own_lnrz_kmod_half γ k m1 -∗
       own_lnrz_kmod_half γ k m2 -∗
       ⌜m2 = m1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iDestruct (own_valid_2 with "Hv1 Hv2") as %Hvalid.
+      rewrite singleton_op singleton_valid dfrac_agree_op_valid_L in Hvalid.
+      by destruct Hvalid as [_ ?].
+    Qed.
 
     Lemma lnrz_kmod_vslice_agree {γ k m im} :
       k ∈ keys_all ->
@@ -237,7 +298,15 @@ Section res.
       own_lnrz_kmod_half γ k kmod1 -∗
       own_lnrz_kmod_half γ k kmod2 ==∗
       own_lnrz_kmod_half γ k kmod ∗ own_lnrz_kmod_half γ k kmod.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iCombine "Hv1 Hv2" as "Hv".
+      rewrite -own_op singleton_op.
+      iApply (own_update with "Hv").
+      apply singleton_update.
+      apply dfrac_agree_update_2.
+      by rewrite dfrac_op_own Qp.half_half.
+    Qed.
 
     Lemma lnrz_kmod_big_agree {γ keys kmods f} :
       dom kmods = keys ->
@@ -282,14 +351,19 @@ Section res.
     (** Key-modification made by committed transactions. One half owned by the
     txnsys invariant, and the other half by the group invariant. *)
 
-    Definition own_cmtd_kmod_half γ (k : dbkey) (kmod : dbkmod) : iProp Σ.
-    Admitted.
+    Definition own_cmtd_kmod_half γ (k : dbkey) (kmod : dbkmod) : iProp Σ :=
+      own γ.(cmtd_kmod) {[ k := (to_dfrac_agree (DfracOwn (1 / 2)) kmod) ]}.
 
     Lemma cmtd_kmod_agree {γ k m1 m2} :
       own_cmtd_kmod_half γ k m1 -∗
       own_cmtd_kmod_half γ k m2 -∗
       ⌜m2 = m1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iDestruct (own_valid_2 with "Hv1 Hv2") as %Hvalid.
+      rewrite singleton_op singleton_valid dfrac_agree_op_valid_L in Hvalid.
+      by destruct Hvalid as [_ ?].
+    Qed.
 
     Lemma cmtd_kmod_vslice_agree {γ k m im} :
       k ∈ keys_all ->
@@ -306,7 +380,15 @@ Section res.
       own_cmtd_kmod_half γ k kmod1 -∗
       own_cmtd_kmod_half γ k kmod2 ==∗
       own_cmtd_kmod_half γ k kmod ∗ own_cmtd_kmod_half γ k kmod.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iCombine "Hv1 Hv2" as "Hv".
+      rewrite -own_op singleton_op.
+      iApply (own_update with "Hv").
+      apply singleton_update.
+      apply dfrac_agree_update_2.
+      by rewrite dfrac_op_own Qp.half_half.
+    Qed.
 
     Lemma cmtd_kmod_big_agree {γ keys kmods f} :
       dom kmods = keys ->
@@ -518,6 +600,7 @@ Section alloc.
       (* per-replica logs | replica lock *)
       ([∗ set] g ∈ gids_all, [∗ set] r ∈ rids_all,
          own_replica_clog_half γ g r [] ∗ own_replica_ilog_half γ g r []).
+  Proof.
   Admitted.
 
 End alloc.
diff --git a/src/program_proof/tulip/res_group.v b/src/program_proof/tulip/res_group.v
index 9fe3934b7..506505db7 100644
--- a/src/program_proof/tulip/res_group.v
+++ b/src/program_proof/tulip/res_group.v
@@ -1,4 +1,5 @@
-(** Global resources. *)
+From iris.algebra Require Import mono_nat mono_list gmap_view gset.
+From iris.algebra.lib Require Import dfrac_agree.
 From Perennial.program_proof Require Import grove_prelude.
 From Perennial.program_proof.tulip Require Import base.
 
@@ -12,16 +13,20 @@ Section res.
 
     (** Mapping from transaction IDs to preparedness of transactions on a group. *)
 
-    Definition own_group_prepm γ (gid : u64) (pm : gmap nat bool) : iProp Σ.
-    Admitted.
+    Definition is_group_prep γ (gid : u64) (ts : nat) (p : bool) : iProp Σ :=
+      own γ.(group_prep) {[ gid := gmap_view_frag ts DfracDiscarded (to_agree p) ]}.
 
-    Definition is_group_prep γ (gid : u64) (ts : nat) (p : bool) : iProp Σ.
-    Admitted.
+    Definition own_group_prepm_auth γ (gid : u64) (pm : gmap nat bool) : iProp Σ :=
+      own γ.(group_prep) {[ gid := gmap_view_auth (DfracOwn 1) (to_agree <$> pm) ]}.
+
+    Definition own_group_prepm γ (gid : u64) (pm : gmap nat bool) : iProp Σ :=
+      own_group_prepm_auth γ gid pm ∗
+      ([∗ map] ts ↦ p ∈ pm, is_group_prep γ gid ts p).
 
     #[global]
     Instance is_group_prep_persistent γ gid ts p :
       Persistent (is_group_prep γ gid ts p).
-    Admitted.
+    Proof. apply _. Defined.
 
     Definition is_group_prepared γ gid ts :=
       is_group_prep γ gid ts true.
@@ -33,25 +38,57 @@ Section res.
       is_group_prep γ gid ts p1 -∗
       is_group_prep γ gid ts p2 -∗
       ⌜p2 = p1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hfrag1 Hfrag2".
+      iDestruct (own_valid_2 with "Hfrag1 Hfrag2") as %Hvalid.
+      rewrite singleton_op singleton_valid in Hvalid.
+      apply gmap_view_frag_op_valid in Hvalid as [_ Hvalid].
+      by apply to_agree_op_inv_L in Hvalid.
+    Qed.
 
     Lemma group_prep_insert {γ gid pm} ts p :
       pm !! ts = None ->
       own_group_prepm γ gid pm ==∗
       own_group_prepm γ gid (<[ts := p]> pm) ∗ is_group_prep γ gid ts p.
-    Admitted.
+    Proof.
+      iIntros (Hnotin) "[Hauth #Hfrags]".
+      iAssert (own_group_prepm_auth γ gid (<[ts := p]> pm) ∗ is_group_prep γ gid ts p)%I
+        with "[> Hauth]" as "[Hauth #Hfrag]".
+      { iRevert "Hauth".
+        rewrite -own_op.
+        iApply own_update.
+        rewrite singleton_op.
+        apply singleton_update.
+        rewrite fmap_insert. apply: gmap_view_alloc; [|done..].
+        by rewrite lookup_fmap Hnotin.
+      }
+      iFrame "∗ #".
+      by iApply big_sepM_insert_2.
+    Qed.
 
     Lemma group_prep_lookup γ gid pm ts p :
       own_group_prepm γ gid pm -∗
       is_group_prep γ gid ts p -∗
       ⌜pm !! ts = Some p⌝.
-    Admitted.
+    Proof.
+      iIntros "[Hauth _] Hfrag".
+      iDestruct (own_valid_2 with "Hauth Hfrag") as %Hvalid.
+      rewrite singleton_op singleton_valid in Hvalid.
+      apply gmap_view_both_dfrac_valid_discrete_total in Hvalid.
+      destruct Hvalid as (v' & _ & _ & Hlookup & _ & Hincl).
+      apply lookup_fmap_Some in Hlookup as (b & <- & Hb).
+      apply to_agree_included_L in Hincl.
+      by subst b.
+    Qed.
 
     Lemma group_prep_witness γ gid pm ts p :
       pm !! ts = Some p ->
       own_group_prepm γ gid pm -∗
       is_group_prep γ gid ts p.
-    Admitted.
+    Proof.
+      iIntros (Hp) "[_ Hfrags]".
+      by iApply (big_sepM_lookup with "Hfrags").
+    Qed.
 
   End group_prep.
 
@@ -59,23 +96,58 @@ Section res.
 
     (** Mapping from transaction IDs to proposals (i.e., pairs of rank and bool). *)
 
-    Definition own_group_prepare_proposals_map
-      γ (gid : u64) (psm : gmap nat (gmap nat bool)) : iProp Σ.
-    Admitted.
+    Definition is_group_prepare_proposal γ (gid : u64) (ts : nat) (rk : nat) (p : bool) : iProp Σ :=
+      own γ.(group_prepare_proposal)
+              {[ gid := (gmap_view_frag (ts, rk) DfracDiscarded (to_agree p)) ]}.
 
-    Definition is_group_prepare_proposal γ (gid : u64) (ts : nat) (rk : nat) (p : bool) : iProp Σ.
-    Admitted.
+    Definition own_group_ppsl_auth γ (gid : u64) (psm : gmap (nat * nat) bool) : iProp Σ :=
+      own γ.(group_prepare_proposal) {[ gid := (gmap_view_auth (DfracOwn 1) (to_agree <$> psm)) ]}.
+
+    Definition own_group_prepare_proposals_map
+      γ (gid : u64) (psm : gmap nat (gmap nat bool)) : iProp Σ :=
+      ∃ m : gmap (nat * nat) bool,
+        own_group_ppsl_auth γ gid m ∗
+        ([∗ map] tr ↦ p ∈ m, is_group_prepare_proposal γ gid tr.1 tr.2 p) ∗
+        (⌜∀ t r p, m !! (t, r) = Some p ↔ ∃ im, psm !! t = Some im ∧ im !! r = Some p⌝).
 
     #[global]
     Instance is_group_prepare_proposal_persistent γ gid ts rk p :
       Persistent (is_group_prepare_proposal γ gid ts rk p).
-    Admitted.
+    Proof. apply _. Defined.
 
-    Lemma group_prepare_proposal_init {γ gid psm} ts ps :
+    (* TODO: this doesn't need an update modality *)
+    Lemma group_prepare_proposal_init {γ gid psm} ts :
       psm !! ts = None ->
       own_group_prepare_proposals_map γ gid psm ==∗
-      own_group_prepare_proposals_map γ gid (<[ts := ps]> psm).
-    Admitted.
+      own_group_prepare_proposals_map γ gid (<[ts := ∅]> psm).
+    Proof.
+      iIntros (Hnotin) "Hauth".
+      iDestruct "Hauth" as (m) "(Hauth & Hppsl & %Heq)".
+      iExists m.
+      iFrame.
+      iPureIntro.
+      intros t r p.
+      split.
+      { intros Hp.
+        specialize (Heq t r p).
+        destruct Heq as [Hincl _].
+        specialize (Hincl Hp).
+        destruct Hincl as (im & Him & Himr).
+        destruct (decide (t = ts)) as [-> | Hne]; first congruence.
+        exists im.
+        by rewrite lookup_insert_ne.
+      }
+      { intros (im & Him & Hp).
+        specialize (Heq t r p).
+        destruct Heq as [_ Hincl].
+        apply Hincl.
+        destruct (decide (ts = t)) as [-> | Hne].
+        { rewrite lookup_insert in Him. inv Him. }
+        { rewrite lookup_insert_ne in Him; last done.
+          by eauto.
+        }
+      }
+    Qed.
 
     Lemma group_prepare_proposal_insert {γ gid psm} ts ps rk p :
       let ps' := <[rk := p]> ps in
@@ -83,20 +155,114 @@ Section res.
       ps !! rk = None ->
       own_group_prepare_proposals_map γ gid psm ==∗
       own_group_prepare_proposals_map γ gid (<[ts := ps']> psm).
-    Admitted.
+    Proof.
+      iIntros (ps' Hps Hnotin) "Hauth".
+      iDestruct "Hauth" as (m) "(Hauth & Hppsl & %Heq)".
+      iAssert (own_group_ppsl_auth γ gid (<[(ts, rk) := p]> m) ∗
+               is_group_prepare_proposal γ gid ts rk p)%I
+        with "[> Hauth]" as "[Hauth #Hfrag]".
+      { iRevert "Hauth".
+        rewrite -own_op.
+        iApply own_update.
+        rewrite singleton_op.
+        apply singleton_update.
+        rewrite fmap_insert. apply: gmap_view_alloc; [|done..].
+        rewrite lookup_fmap.
+        destruct (m !! (ts, rk)) as [p' |] eqn:Hin; last done.
+        specialize (Heq ts rk p').
+        destruct Heq as [Hincl _].
+        specialize (Hincl Hin).
+        destruct Hincl as (im & Him & Hp').
+        rewrite Hps in Him. inv Him.
+      }
+      iExists (<[(ts, rk) := p]> m).
+      iFrame.
+      iModIntro.
+      iSplit.
+      { by iApply big_sepM_insert_2. }
+      iPureIntro.
+      intros t r p'.
+      split.
+      { intros Hp'.
+        destruct (decide (t = ts)) as [-> | Hne].
+        { rewrite lookup_insert.
+          exists ps'.
+          split; first done.
+          subst ps'.
+          destruct (decide (r = rk)) as [-> | Hner].
+          { rewrite lookup_insert.
+            by rewrite lookup_insert in Hp'.
+          }
+          { rewrite lookup_insert_ne; last done.
+            rewrite lookup_insert_ne in Hp'; last first.
+            { intros Hcontra. inv Hcontra. }
+            specialize (Heq ts r p').
+            destruct Heq as [Hincl _].
+            specialize (Hincl Hp').
+            destruct Hincl as (im & Him & Himr).
+            rewrite Hps in Him. by inv Him.
+          }
+        }
+        { rewrite lookup_insert_ne; last done.
+          rewrite lookup_insert_ne in Hp'; last first.
+          { intros Hcontra. inv Hcontra. }
+          by apply Heq.
+        }
+      }
+      { intros Him.
+        destruct Him as (im & Him & Hp').
+        destruct (decide (t = ts)) as [-> | Hne].
+        { rewrite lookup_insert in Him. inv Him.
+          destruct (decide (r = rk)) as [-> | Hner].
+          { rewrite lookup_insert.
+            rewrite lookup_insert in Hp'. by inv Hp'.
+          }
+          { rewrite lookup_insert_ne; last first.
+            { intros Hcontra. inv Hcontra. }
+            rewrite lookup_insert_ne in Hp'; last done.
+            apply Heq.
+            by eauto.
+          }
+        }
+        { rewrite lookup_insert_ne; last first.
+          { intros Hcontra. inv Hcontra. }
+          rewrite lookup_insert_ne in Him; last done.
+          apply Heq.
+          by eauto.
+        }
+      }
+    Qed.
 
     Lemma group_prepare_proposal_witness {γ gid psm} ts ps rk p :
       psm !! ts = Some ps ->
       ps !! rk = Some p ->
       own_group_prepare_proposals_map γ gid psm -∗
       is_group_prepare_proposal γ gid ts rk p.
-    Admitted.
+    Proof.
+      iIntros (Hps Hp) "Hauth".
+      iDestruct "Hauth" as (im) "(_ & Hfrags & %Heq)".
+      iApply (big_sepM_lookup _ _ (ts, rk) with "Hfrags").
+      apply Heq.
+      by eauto.
+    Qed.
 
     Lemma group_prepare_proposal_lookup γ gid psm ts rk p :
       is_group_prepare_proposal γ gid ts rk p -∗
       own_group_prepare_proposals_map γ gid psm -∗
       ∃ ps, ⌜psm !! ts = Some ps ∧ ps !! rk = Some p⌝.
-    Admitted.
+    Proof.
+      iIntros "Hfrag Hauth".
+      iDestruct "Hauth" as (im) "(Hauth & _ & %Heq)".
+      iDestruct (own_valid_2 with "Hauth Hfrag") as %Hvalid.
+      rewrite singleton_op singleton_valid in Hvalid.
+      apply gmap_view_both_dfrac_valid_discrete_total in Hvalid.
+      destruct Hvalid as (v' & _ & _ & Hlookup & _ & Hincl).
+      apply lookup_fmap_Some in Hlookup as (b & <- & Hb).
+      apply to_agree_included_L in Hincl.
+      subst b.
+      iPureIntro.
+      by apply Heq.
+    Qed.
 
   End group_prepare_proposal.
 
@@ -104,16 +270,20 @@ Section res.
 
     (** Mapping from transaction IDs to committedness of transactions on a group. *)
 
-    Definition own_group_commit_map γ (gid : u64) (pm : gmap nat bool) : iProp Σ.
-    Admitted.
+    Definition is_group_commit γ (gid : u64) (ts : nat) (c : bool) : iProp Σ :=
+      own γ.(group_commit) {[ gid := (gmap_view_frag ts DfracDiscarded (to_agree c)) ]}.
+
+    Definition own_group_commit_map_auth γ (gid : u64) (cm : gmap nat bool) : iProp Σ :=
+      own γ.(group_commit) {[ gid := (gmap_view_auth (DfracOwn 1) (to_agree <$> cm)) ]}.
 
-    Definition is_group_commit γ (gid : u64) (ts : nat) (c : bool) : iProp Σ.
-    Admitted.
+    Definition own_group_commit_map γ (gid : u64) (cm : gmap nat bool) : iProp Σ :=
+      own_group_commit_map_auth γ gid cm ∗
+      ([∗ map] ts ↦ c ∈ cm, is_group_commit γ gid ts c).
 
     #[global]
     Instance is_group_commit_persistent γ gid ts c :
       Persistent (is_group_commit γ gid ts c).
-    Admitted.
+    Proof. apply _. Defined.
 
     Definition is_group_committed γ gid ts :=
       is_group_commit γ gid ts true.
@@ -125,25 +295,57 @@ Section res.
       is_group_commit γ gid ts c1 -∗
       is_group_commit γ gid ts c2 -∗
       ⌜c2 = c1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hfrag1 Hfrag2".
+      iDestruct (own_valid_2 with "Hfrag1 Hfrag2") as %Hvalid.
+      rewrite singleton_op singleton_valid in Hvalid.
+      apply gmap_view_frag_op_valid in Hvalid as [_ Hvalid].
+      by apply to_agree_op_inv_L in Hvalid.
+    Qed.
 
     Lemma group_commit_insert {γ gid pm} ts c :
       pm !! ts = None ->
       own_group_commit_map γ gid pm ==∗
       own_group_commit_map γ gid (<[ts := c]> pm) ∗ is_group_commit γ gid ts c.
-    Admitted.
+    Proof.
+      iIntros (Hnotin) "[Hauth #Hfrags]".
+      iAssert (own_group_commit_map_auth γ gid (<[ts := c]> pm) ∗ is_group_commit γ gid ts c)%I
+        with "[> Hauth]" as "[Hauth #Hfrag]".
+      { iRevert "Hauth".
+        rewrite -own_op.
+        iApply own_update.
+        rewrite singleton_op.
+        apply singleton_update.
+        rewrite fmap_insert. apply: gmap_view_alloc; [|done..].
+        by rewrite lookup_fmap Hnotin.
+      }
+      iFrame "∗ #".
+      by iApply big_sepM_insert_2.
+    Qed.
 
     Lemma group_commit_witness γ gid pm ts c :
       pm !! ts = Some c ->
       own_group_commit_map γ gid pm -∗
       is_group_commit γ gid ts c.
-    Admitted.
+    Proof.
+      iIntros (Hp) "[_ Hfrags]".
+      by iApply (big_sepM_lookup with "Hfrags").
+    Qed.
 
     Lemma group_commit_lookup γ gid pm ts c :
       own_group_commit_map γ gid pm -∗
       is_group_commit γ gid ts c -∗
       ⌜pm !! ts = Some c⌝.
-    Admitted.
+    Proof.
+      iIntros "[Hauth _] Hfrag".
+      iDestruct (own_valid_2 with "Hauth Hfrag") as %Hvalid.
+      rewrite singleton_op singleton_valid in Hvalid.
+      apply gmap_view_both_dfrac_valid_discrete_total in Hvalid.
+      destruct Hvalid as (v' & _ & _ & Hlookup & _ & Hincl).
+      apply lookup_fmap_Some in Hlookup as (b & <- & Hb).
+      apply to_agree_included_L in Hincl.
+      by subst b.
+    Qed.
 
   End group_commit.
 
diff --git a/src/program_proof/tulip/res_replica.v b/src/program_proof/tulip/res_replica.v
index 5d237b9db..a7f31cfe6 100644
--- a/src/program_proof/tulip/res_replica.v
+++ b/src/program_proof/tulip/res_replica.v
@@ -1,5 +1,8 @@
-(** Global resources. *)
+From iris.algebra Require Import mono_nat mono_list gmap_view gset.
+From iris.algebra.lib Require Import dfrac_agree.
 From Perennial.program_proof Require Import grove_prelude.
+From Perennial.program_proof.rsm Require Import big_sep.
+From Perennial.program_proof.rsm.pure Require Import fin_maps.
 From Perennial.program_proof.tulip Require Import base stability.
 
 Section res.
@@ -11,33 +14,72 @@ Section res.
 
     (** Set of transaction IDs that are validated on a replica in a group. *)
 
-    Definition own_replica_validated_tss γ (gid rid : u64) (vtss : gset nat) : iProp Σ.
-    Admitted.
+    Definition is_replica_validated_ts γ (gid rid : u64) (vts : nat) : iProp Σ :=
+      own γ.(replica_validated_ts) {[ (gid, rid) := gmap_view_frag vts DfracDiscarded tt ]}.
 
-    Definition is_replica_validated_ts γ (gid rid : u64) (vts : nat) : iProp Σ.
-    Admitted.
+    Definition own_replica_validated_tss_auth
+      γ (gid rid : u64) (vtss : gset nat) : iProp Σ :=
+      own γ.(replica_validated_ts) {[ (gid, rid) := gmap_view_auth (DfracOwn 1) (gset_to_gmap tt vtss) ]}.
+
+    Definition own_replica_validated_tss γ (gid rid : u64) (vtss : gset nat) : iProp Σ :=
+      own_replica_validated_tss_auth γ gid rid vtss ∗
+      ([∗ set] t ∈ vtss, is_replica_validated_ts γ gid rid t).
 
     #[global]
     Instance is_replica_validated_persistent γ gid rid ts :
       Persistent (is_replica_validated_ts γ gid rid ts).
-    Admitted.
+    Proof. apply _. Defined.
 
     Lemma replica_validated_ts_insert {γ gid rid vtss} vts :
       own_replica_validated_tss γ gid rid vtss ==∗
       own_replica_validated_tss γ gid rid ({[vts]} ∪ vtss).
-    Admitted.
+    Proof.
+      destruct (decide (vts ∈ vtss)) as [Hin | Hnotin].
+      { replace (_ ∪ _) with vtss by set_solver.
+        by iIntros.
+      }
+      iIntros "[Hauth #Hfrags]".
+      set vtss' := _ ∪ _.
+      iAssert (own_replica_validated_tss_auth γ gid rid vtss' ∗
+               is_replica_validated_ts γ gid rid vts)%I
+        with "[> Hauth]" as "[Hauth #Hfrag]".
+      { iRevert "Hauth".
+        rewrite -own_op.
+        iApply own_update.
+        rewrite singleton_op.
+        apply singleton_update.
+        rewrite gset_to_gmap_union_singleton.
+        apply: gmap_view_alloc; last done; last done.
+        by rewrite lookup_gset_to_gmap_None.
+      }
+      iFrame.
+      iModIntro.
+      by iApply big_sepS_insert_2.
+    Qed.
 
     Lemma replica_validated_ts_witness {γ gid rid vtss} vts :
       vts ∈ vtss ->
       own_replica_validated_tss γ gid rid vtss -∗
       is_replica_validated_ts γ gid rid vts.
-    Admitted.
+    Proof.
+      iIntros (Hin) "[_ Hfrags]".
+      by iApply (big_sepS_elem_of with "Hfrags").
+    Qed.
 
     Lemma replica_validated_ts_elem_of γ gid rid vtss vts :
       is_replica_validated_ts γ gid rid vts -∗
       own_replica_validated_tss γ gid rid vtss -∗
       ⌜vts ∈ vtss⌝.
-    Admitted.
+    Proof.
+      iIntros "Hfrag [Hauth _]".
+      iDestruct (own_valid_2 with "Hauth Hfrag") as %Hvalid.
+      rewrite singleton_op singleton_valid in Hvalid.
+      apply gmap_view_both_dfrac_valid_discrete_total in Hvalid.
+      destruct Hvalid as (v' & _ & _ & Hlookup & _ & _).
+      apply elem_of_dom_2 in Hlookup.
+      rewrite dom_gset_to_gmap in Hlookup.
+      done.
+    Qed.
 
   End replica_validated_ts.
 
@@ -47,12 +89,12 @@ Section res.
     validated at a particular timestamp. *)
 
     Definition own_replica_key_validation
-      γ (gid rid : u64) (key : dbkey) (l : list bool) : iProp Σ.
-    Admitted.
+      γ (gid rid : u64) (key : dbkey) (l : list bool) : iProp Σ :=
+      own γ.(replica_key_validation) {[ (gid, rid, key) := ●ML{#1} l ]}.
 
     Definition is_replica_key_validation_lb
-      γ (gid rid : u64) (key : dbkey) (l : list bool) : iProp Σ.
-    Admitted.
+      γ (gid rid : u64) (key : dbkey) (l : list bool) : iProp Σ :=
+      own γ.(replica_key_validation) {[ (gid, rid, key) := ◯ML l ]}.
 
     Definition is_replica_key_validation_length_lb
       γ (gid rid : u64) (key : dbkey) (n : nat) : iProp Σ :=
@@ -73,24 +115,40 @@ Section res.
     #[global]
     Instance is_replica_key_validation_lb_persistent γ gid rid key l :
       Persistent (is_replica_key_validation_lb γ gid rid key l).
-    Admitted.
+    Proof. apply _. Defined.
 
     Lemma replica_key_validation_update {γ gid rid key l} l' :
       prefix l l' ->
       own_replica_key_validation γ gid rid key l ==∗
       own_replica_key_validation γ gid rid key l'.
-    Admitted.
+    Proof.
+      intros Hprefix.
+      iApply own_update.
+      apply singleton_update.
+      by apply mono_list_update.
+    Qed.
 
     Lemma replica_key_validation_witness γ gid rid key l :
       own_replica_key_validation γ gid rid key l -∗
       is_replica_key_validation_lb γ gid rid key l.
-    Admitted.
+    Proof.
+      iApply own_mono.
+      apply singleton_included_mono.
+      apply mono_list_included.
+    Qed.
 
     Lemma replica_key_validation_prefix γ gid rid key l lb :
       is_replica_key_validation_lb γ gid rid key lb -∗
       own_replica_key_validation γ gid rid key l -∗
       ⌜prefix lb l⌝.
-    Admitted.
+    Proof.
+      iIntros "Hh Hlb".
+      iDestruct (own_valid_2 with "Hh Hlb") as %Hvalid.
+      iPureIntro. revert Hvalid.
+      rewrite singleton_op singleton_valid.
+      rewrite cmra_comm mono_list_both_dfrac_valid_L.
+      by intros [_ ?].
+    Qed.
 
     Lemma replica_key_validation_lookup γ gid rid key l ts b :
       is_replica_key_validation_at γ gid rid key ts b -∗
@@ -108,13 +166,26 @@ Section res.
       is_replica_key_validation_at γ gid rid key ts b -∗
       is_replica_key_validation_lb γ gid rid key l -∗
       ⌜l !! ts = Some b⌝.
-    Admitted.
+    Proof.
+      iIntros (Hlen) "(%lb & #Hlb & %Hv) #Hl".
+      iDestruct (own_valid_2 with "Hl Hlb") as %Hvalid.
+      iPureIntro.
+      rewrite singleton_op singleton_valid mono_list_lb_op_valid_L in Hvalid.
+      destruct Hvalid as [Hprefix | Hprefix].
+      { by rewrite (prefix_lookup_lt _ _ _ Hlen Hprefix). }
+      { by eapply prefix_lookup_Some. }
+    Qed.
 
     Lemma replica_key_validation_lb_weaken {γ gid rid key l} l' :
       prefix l' l ->
       is_replica_key_validation_lb γ gid rid key l -∗
       is_replica_key_validation_lb γ gid rid key l'.
-    Admitted.
+    Proof.
+      iIntros (Hprefix).
+      iApply own_mono.
+      apply singleton_included_mono.
+      by apply mono_list_lb_mono.
+    Qed.
 
     Lemma replica_key_validation_at_length γ gid rid key ts b :
       is_replica_key_validation_at γ gid rid key ts b -∗
@@ -131,7 +202,16 @@ Section res.
       map_Forall2 (λ _ l1 l2, prefix l1 l2) kvdm kvdm' ->
       ([∗ map] k ↦ l ∈ kvdm, own_replica_key_validation γ gid rid k l) ==∗
       ([∗ map] k ↦ l ∈ kvdm', own_replica_key_validation γ gid rid k l).
-    Admitted.
+    Proof.
+      iIntros (Hprefix) "Hkvdlm".
+      rewrite -big_sepM_bupd.
+      iApply (big_sepM_impl_dom_eq with "Hkvdlm").
+      { by apply map_Forall2_dom_L in Hprefix. }
+      iIntros (k l1 l2 Hl1 Hl2) "!>".
+      iApply replica_key_validation_update.
+      apply map_Forall2_forall in Hprefix as [Hprefix _].
+      by eapply Hprefix.
+    Qed.
 
   End replica_key_validation.
 
@@ -139,21 +219,34 @@ Section res.
 
     (** Per-replica consistent log. *)
 
-    Definition own_replica_clog_half γ (gid rid : u64) (l : list ccommand) : iProp Σ.
-    Admitted.
+    Definition own_replica_clog_half γ (gid rid : u64) (l : list ccommand) : iProp Σ :=
+      own γ.(replica_clog) {[ (gid, rid) := (to_dfrac_agree (A:=clogO) (DfracOwn (1 / 2)) l) ]}.
 
     Lemma replica_clog_update {γ gid rid l1 l2} l' :
       own_replica_clog_half γ gid rid l1 -∗
       own_replica_clog_half γ gid rid l2 ==∗
       own_replica_clog_half γ gid rid l' ∗
       own_replica_clog_half γ gid rid l'.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iCombine "Hv1 Hv2" as "Hv".
+      rewrite -own_op singleton_op.
+      iApply (own_update with "Hv").
+      apply singleton_update.
+      apply dfrac_agree_update_2.
+      by rewrite dfrac_op_own Qp.half_half.
+    Qed.
 
     Lemma replica_clog_agree {γ gid rid l1 l2} :
       own_replica_clog_half γ gid rid l1 -∗
       own_replica_clog_half γ gid rid l2 -∗
       ⌜l2 = l1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iDestruct (own_valid_2 with "Hv1 Hv2") as %Hvalid.
+      rewrite singleton_op singleton_valid dfrac_agree_op_valid_L in Hvalid.
+      by destruct Hvalid as [_ ?].
+    Qed.
 
   End replica_clog.
 
@@ -161,21 +254,34 @@ Section res.
 
     (** Per-replica inconsistent log. *)
 
-    Definition own_replica_ilog_half γ (gid rid : u64) (l : list (nat * icommand)) : iProp Σ.
-    Admitted.
+    Definition own_replica_ilog_half γ (gid rid : u64) (l : list (nat * icommand)) : iProp Σ :=
+      own γ.(replica_ilog) {[ (gid, rid) := (to_dfrac_agree (A:=ilogO) (DfracOwn (1 / 2)) l) ]}.
 
     Lemma replica_ilog_update {γ gid rid l1 l2} l' :
       own_replica_ilog_half γ gid rid l1 -∗
       own_replica_ilog_half γ gid rid l2 ==∗
       own_replica_ilog_half γ gid rid l' ∗
       own_replica_ilog_half γ gid rid l'.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iCombine "Hv1 Hv2" as "Hv".
+      rewrite -own_op singleton_op.
+      iApply (own_update with "Hv").
+      apply singleton_update.
+      apply dfrac_agree_update_2.
+      by rewrite dfrac_op_own Qp.half_half.
+    Qed.
 
     Lemma replica_ilog_agree {γ gid rid l1 l2} :
       own_replica_ilog_half γ gid rid l1 -∗
       own_replica_ilog_half γ gid rid l2 -∗
       ⌜l2 = l1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iDestruct (own_valid_2 with "Hv1 Hv2") as %Hvalid.
+      rewrite singleton_op singleton_valid dfrac_agree_op_valid_L in Hvalid.
+      by destruct Hvalid as [_ ?].
+    Qed.
 
   End replica_ilog.
 
@@ -184,16 +290,26 @@ Section res.
     (** Mapping from transaction IDs to booleans indicating whether they are
     prepared on a replica in a group at a certain rank. *)
 
-    Definition own_replica_ballot_map γ (gid rid : u64) (bs : gmap nat ballot) : iProp Σ.
-    Admitted.
+    Definition own_replica_ballot_map_auth γ (gid rid : u64) (bs : gmap nat ballot) : iProp Σ :=
+      let f := (λ l : list vote, mono_list_auth (A:=voteO) (DfracOwn 1) l) in
+      own γ.(replica_ballot) {[ (gid, rid) := gmap_view_auth (DfracOwn 1) (f <$> bs) ]}.
 
-    Definition is_replica_ballot_lb γ (gid rid : u64) (ts : nat) (blt : ballot) : iProp Σ.
-    Admitted.
+    Definition own_replica_ballot_map_frag γ (gid rid : u64) (ts : nat) (blt : ballot) : iProp Σ :=
+      let f := (λ l : list vote, mono_list_auth (A:=voteO) (DfracOwn 1) l) in
+      own γ.(replica_ballot) {[ (gid, rid) := gmap_view_frag ts (DfracOwn 1) (f blt) ]}.
+
+    Definition own_replica_ballot_map γ (gid rid : u64) (bs : gmap nat ballot) : iProp Σ :=
+      own_replica_ballot_map_auth γ gid rid bs ∗
+      ([∗ map] t ↦ l ∈ bs, own_replica_ballot_map_frag γ gid rid t l).
+
+    Definition is_replica_ballot_lb γ (gid rid : u64) (ts : nat) (blt : ballot) : iProp Σ :=
+      let f := (λ l : list vote, mono_list_lb (A:=voteO) l) in
+      own γ.(replica_ballot) {[ (gid, rid) := gmap_view_frag ts DfracDiscarded (f blt) ]}.
 
     #[global]
     Instance is_replica_ballot_lb_persistent γ gid rid ts blt :
       Persistent (is_replica_ballot_lb γ gid rid ts blt).
-    Admitted.
+    Proof. apply _. Defined.
 
     Definition is_replica_pdec_at_rank γ (gid rid : u64) (ts rank : nat) (p : bool) : iProp Σ :=
       ∃ blt, is_replica_ballot_lb γ gid rid ts blt ∧ ⌜blt !! rank = Some (Accept p)⌝.
@@ -202,19 +318,66 @@ Section res.
       bs !! ts = None ->
       own_replica_ballot_map γ gid rid bs ==∗
       own_replica_ballot_map γ gid rid (<[ts := l]> bs).
-    Admitted.
+    Proof.
+      intros Hnotin.
+      iIntros "[Hauth Hfrags]".
+      iAssert (own_replica_ballot_map_auth γ gid rid (<[ts:=l]> bs) ∗
+               own_replica_ballot_map_frag γ gid rid ts l)%I
+        with "[> Hauth]" as "[Hauth Hfrag]".
+      { iRevert "Hauth".
+        rewrite -own_op.
+        iApply own_update.
+        rewrite singleton_op.
+        apply singleton_update.
+        rewrite fmap_insert.
+        apply: gmap_view_alloc.
+        { by rewrite lookup_fmap Hnotin /=. }
+        { apply dfrac_valid_own_1. }
+        { apply mono_list_auth_valid. }
+      }
+      iFrame.
+      iModIntro.
+      iApply (big_sepM_insert_2 with "Hfrag Hfrags").
+    Qed.
 
     Lemma replica_ballot_update {γ gid rid bs} ts l l' :
       bs !! ts = Some l ->
       prefix l l' ->
       own_replica_ballot_map γ gid rid bs ==∗
       own_replica_ballot_map γ gid rid (<[ts := l']> bs).
-    Admitted.
+    Proof.
+      iIntros (Hl Hprefix) "[Hauth Hfrags]".
+      iDestruct (big_sepM_delete with "Hfrags") as "[Hfrag Hfrags]".
+      { apply Hl. }
+      iAssert (own_replica_ballot_map_auth γ gid rid (<[ts := l']> bs) ∗
+               own_replica_ballot_map_frag γ gid rid ts l')%I
+        with "[> Hauth Hfrag]" as "[Hauth Hfrag]".
+      { iCombine "Hauth Hfrag" as "Hauthfrag".
+        iRevert "Hauthfrag".
+        rewrite -!own_op.
+        iApply own_update.
+        rewrite singleton_op.
+        apply singleton_update.
+        rewrite fmap_insert.
+        apply gmap_view_replace.
+        apply mono_list_auth_valid.
+      }
+      iFrame.
+      iDestruct (big_sepM_insert_2 with "Hfrag Hfrags") as "Hfrags".
+      by rewrite insert_delete_insert.
+    Qed.
 
     Lemma replica_ballot_witness {γ gid rid bs} ts l :
       bs !! ts = Some l ->
       own_replica_ballot_map γ gid rid bs -∗
       is_replica_ballot_lb γ gid rid ts l.
+    Proof.
+      iIntros (Hl) "[Hauth Hfrags]".
+      iDestruct (big_sepM_lookup with "Hfrags") as "Hfrag".
+      { apply Hl. }
+      iRevert "Hfrag".
+      iApply own_mono.
+      apply singleton_included_mono.
     Admitted.
 
     Lemma replica_ballot_lookup {γ gid rid bs} ts lb :
@@ -238,74 +401,243 @@ Section res.
     of the transaction ID and rank is casted by this replica. This is used to
     ensure no two replicas could serve as the coordinator in the same term. *)
 
-    Definition own_replica_backup_vote_map
-      γ (gid rid : u64) (bvm : gmap nat (gmap nat coordid)) : iProp Σ.
-    Admitted.
-
     Definition is_replica_backup_vote
-      γ (gid rid : u64) (ts rank : nat) (cid : coordid) : iProp Σ.
-    Admitted.
+      γ (gid rid : u64) (ts rank : nat) (cid : coordid) : iProp Σ :=
+      own γ.(replica_vote)
+              {[ (gid, rid) := (gmap_view_frag (ts, rank) DfracDiscarded (to_agree cid)) ]}.
+
+    Definition own_replica_backup_vote_map_auth
+      γ (gid rid : u64) (m : gmap (nat * nat) coordid) : iProp Σ :=
+      own γ.(replica_vote) {[ (gid, rid) := (gmap_view_auth (DfracOwn 1) (to_agree <$> m)) ]}.
+
+    Definition own_replica_backup_vote_map
+      γ (gid rid : u64) (bvm : gmap nat (gmap nat coordid)) : iProp Σ :=
+      ∃ m : gmap (nat * nat) coordid,
+        own_replica_backup_vote_map_auth γ gid rid m ∗
+        (⌜∀ t r c, m !! (t, r) = Some c -> ∃ im, bvm !! t = Some im ∧ im !! r = Some c⌝).
 
     #[global]
     Instance is_replica_backup_vote_persistent γ gid rid ts rank cid :
       Persistent (is_replica_backup_vote γ gid rid ts rank cid).
-    Admitted.
+    Proof. apply _. Defined.
 
+    (* TODO: doesn't need update modality *)
     Lemma replica_backup_vote_init {γ gid rid bvm} ts :
       bvm !! ts = None ->
       own_replica_backup_vote_map γ gid rid bvm ==∗
       own_replica_backup_vote_map γ gid rid (<[ts := ∅]> bvm).
-    Admitted.
+    Proof.
+      iIntros (Hnotin) "Hauth".
+      iDestruct "Hauth" as (m) "[Hauth %Hincl]".
+      iExists m.
+      iFrame.
+      iPureIntro.
+      intros t r c Hc.
+      destruct (decide (t = ts)) as [-> | Hne].
+      { specialize (Hincl _ _ _ Hc).
+        destruct Hincl as (im & Him & _).
+        by rewrite Hnotin in Him.
+      }
+      rewrite lookup_insert_ne; last done.
+      by apply Hincl.
+    Qed.
 
-    Lemma replica_backup_vote_insert {γ gid rid bvm m} ts rank cid :
-      bvm !! ts = Some m ->
-      m !! rank = None ->
+    Lemma replica_backup_vote_insert {γ gid rid bvm vm} ts rank cid :
+      bvm !! ts = Some vm ->
+      vm !! rank = None ->
       own_replica_backup_vote_map γ gid rid bvm ==∗
-      own_replica_backup_vote_map γ gid rid (<[ts := (<[rank := cid]> m)]> bvm) ∗
+      own_replica_backup_vote_map γ gid rid (<[ts := (<[rank := cid]> vm)]> bvm) ∗
       is_replica_backup_vote γ gid rid ts rank cid.
-    Admitted.
+    Proof.
+      iIntros (Hm Hnotin) "Hauth".
+      iDestruct "Hauth" as (m) "[Hauth %Hincl]".
+      iAssert (own_replica_backup_vote_map_auth γ gid rid (<[(ts, rank) := cid]> m) ∗
+               is_replica_backup_vote γ gid rid ts rank cid)%I
+        with "[> Hauth]" as "[Hauth #Hfrag]".
+      { iRevert "Hauth".
+        rewrite -own_op.
+        iApply own_update.
+        rewrite singleton_op.
+        apply singleton_update.
+        rewrite fmap_insert. apply: gmap_view_alloc; [|done..].
+        rewrite lookup_fmap.
+        destruct (m !! (ts, rank)) as [c' |] eqn:Hin; last done.
+        specialize (Hincl _ _ _ Hin).
+        destruct Hincl as (im & Him & Hc').
+        rewrite Hm in Him. inv Him.
+      }
+      iFrame "∗ #".
+      iPureIntro.
+      intros t r c Hc.
+      destruct (decide (t = ts)) as [-> | Hne].
+      { rewrite lookup_insert.
+        destruct (decide (r = rank)) as [-> | Hner].
+        { rewrite lookup_insert in Hc. inv Hc.
+          exists (<[rank := c]> vm).
+          split; first done.
+          by rewrite lookup_insert.
+        }
+        { rewrite lookup_insert_ne in Hc; last first.
+          { intros Hcontra. congruence. }
+          specialize (Hincl _ _ _ Hc).
+          destruct Hincl as (im & Him & Himr).
+          rewrite Hm in Him. inv Him.
+          exists (<[rank := cid]> im).
+          split; first done.
+          by rewrite lookup_insert_ne.
+        }
+      }
+      { rewrite lookup_insert_ne in Hc; last first.
+        { intros Hcontra. congruence. }
+        rewrite lookup_insert_ne; last done.
+        by apply Hincl.
+      }
+    Qed.
 
     Lemma replica_backup_vote_agree γ gid rid ts rank cid1 cid2 :
       is_replica_backup_vote γ gid rid ts rank cid1 -∗
       is_replica_backup_vote γ gid rid ts rank cid2 -∗
       ⌜cid2 = cid1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hv1 Hv2".
+      iDestruct (own_valid_2 with "Hv1 Hv2") as %Hvalid.
+      rewrite singleton_op singleton_valid gmap_view_frag_op_valid in Hvalid.
+      destruct Hvalid as [_ Hagree].
+      by apply to_agree_op_inv_L in Hagree.
+    Qed.
 
   End replica_backup_vote.
 
   Section replica_backup_token.
 
     (** Mappings from transaction IDs and ranks to sets of groups IDs. This is
-    used to ensure that the same replica proposes become the coordinator at a
-    certain rank for a certain group at most once. *)
+    used to ensure that the same replica can become the coordinator at a certain
+    rank for a certain group at most once. *)
+
+    Definition own_replica_backup_tokens_map_auth
+      γ (gid rid : u64) (s : gset (nat * nat * u64)) : iProp Σ :=
+      own γ.(replica_token) {[ (gid, rid) := gmap_view_auth (DfracOwn 1) (gset_to_gmap tt s) ]}.
 
     Definition own_replica_backup_tokens_map
-      γ (gid rid : u64) (btm : gmap nat (gmap nat (gset u64))) : iProp Σ.
-    Admitted.
+      γ (gid rid : u64) (bvm : gmap nat (gmap nat (gset u64))) : iProp Σ :=
+      ∃ s : gset (nat * nat * u64),
+        own_replica_backup_tokens_map_auth γ gid rid s ∗
+        (⌜∀ t r g, (t, r, g) ∈ s -> ∃ im, bvm !! t = Some im ∧ ∃ ix, im !! r = Some ix ∧ g ∈ ix⌝).
 
     Definition own_replica_backup_token
-      γ (gid rid : u64) (ts rank : nat) (tgid : u64) : iProp Σ.
-    Admitted.
+      γ (gid rid : u64) (ts rank : nat) (tgid : u64) : iProp Σ :=
+      own γ.(replica_token)
+              {[ (gid, rid) := gmap_view_frag (ts, rank, tgid) (DfracOwn 1) tt ]}.
 
+    (* TODO: doesn't need update modality *)
     Lemma replica_backup_token_init {γ gid rid btm} ts :
       btm !! ts = None ->
       own_replica_backup_tokens_map γ gid rid btm ==∗
       own_replica_backup_tokens_map γ gid rid (<[ts := ∅]> btm).
-    Admitted.
+    Proof.
+      iIntros (Hnotin) "Hauth".
+      iDestruct "Hauth" as (m) "[Hauth %Hincl]".
+      iExists m.
+      iFrame.
+      iPureIntro.
+      intros t r c Hc.
+      destruct (decide (t = ts)) as [-> | Hne].
+      { specialize (Hincl _ _ _ Hc).
+        destruct Hincl as (im & Him & _).
+        by rewrite Hnotin in Him.
+      }
+      rewrite lookup_insert_ne; last done.
+      by apply Hincl.
+    Qed.
 
-    Lemma replica_backup_token_insert {γ gid rid btm m} ts rank tgids :
-      btm !! ts = Some m ->
-      m !! rank = None ->
+    Lemma replica_backup_token_insert {γ gid rid btm tm} ts rank tgids :
+      btm !! ts = Some tm ->
+      tm !! rank = None ->
       own_replica_backup_tokens_map γ gid rid btm ==∗
-      own_replica_backup_tokens_map γ gid rid (<[ts := (<[rank := tgids]> m)]> btm) ∗
+      own_replica_backup_tokens_map γ gid rid (<[ts := (<[rank := tgids]> tm)]> btm) ∗
       ([∗ set] tgid ∈ tgids, own_replica_backup_token γ gid rid ts rank tgid).
+    Proof.
+      iIntros (Htm Hnotin) "Hauth".
+      iDestruct "Hauth" as (s) "[Hauth %Hincl]".
+      set tksnew : gset (nat * nat * u64) := set_map (λ g, (ts, rank, g)) tgids.
+      iAssert (own_replica_backup_tokens_map_auth γ gid rid (tksnew ∪ s) ∗
+               ([∗ set] g ∈ tgids, own_replica_backup_token γ gid rid ts rank g))%I
+        with "[> Hauth]" as "[Hauth Hfrags]".
+      { iRevert "Hauth".
+        rewrite -big_opS_own_1 -own_op.
+        iApply own_update.
+        etrans.
+        { apply singleton_update.
+          apply: (gmap_view_alloc_big _ (gset_to_gmap () tksnew) (DfracOwn 1)).
+          { rewrite map_disjoint_dom 2!dom_gset_to_gmap.
+            subst tksnew.
+            intros [[t r] g] Hin1 Hin2.
+            specialize (Hincl _ _ _ Hin2).
+            apply elem_of_map in Hin1.
+            destruct Hin1 as (g' & Heq & Hg').
+            inv Heq.
+            destruct Hincl as (im & Him & Hix).
+            rewrite Htm in Him. inv Him.
+            destruct Hix as (ix & Hix & Hinix).
+            by rewrite Hnotin in Hix.
+          }
+          { done. }
+          { done. }
+        }
+        admit.
+      }
+      iFrame.
+      iPureIntro.
+      intros t r g Hin.
+      destruct (decide (t = ts)) as [-> | Hne]; last first.
+      { rewrite lookup_insert_ne; last done.
+        apply Hincl.
+        apply elem_of_union in Hin.
+        destruct Hin as [Hin | ?]; last done.
+        apply elem_of_map in Hin.
+        destruct Hin as (g' & Heq & _).
+        inv Heq.
+      }
+      rewrite lookup_insert.
+      exists (<[rank:=tgids]> tm).
+      split; first done.
+      destruct (decide (r = rank)) as [-> | Hne]; last first.
+      { rewrite lookup_insert_ne; last done.
+        apply elem_of_union in Hin.
+        destruct Hin as [Hin | Hin]; last first.
+        { specialize (Hincl _ _ _ Hin).
+          destruct Hincl as (im & Him & Hix).
+          rewrite Htm in Him. by inv Him.
+        }
+        apply elem_of_map in Hin.
+        destruct Hin as (g' & Heq & _).
+        inv Heq.
+      }
+      rewrite lookup_insert.
+      exists tgids.
+      split; first done.
+      apply elem_of_union in Hin as [Hin | Hin]; last first.
+      { specialize (Hincl _ _ _ Hin).
+        destruct Hincl as (im & Him & Hix).
+        rewrite Htm in Him. inv Him.
+        destruct Hix as (ix & Hix & _).
+        by rewrite Hnotin in Hix.
+      }
+      apply elem_of_map in Hin as (g' & Heq & Hg').
+      by inv Heq.
     Admitted.
 
     Lemma replica_backup_token_excl γ gid rid ts rank tgid :
       own_replica_backup_token γ gid rid ts rank tgid -∗
       own_replica_backup_token γ gid rid ts rank tgid -∗
       False.
-    Admitted.
+    Proof.
+      iIntros "Ht1 Ht2".
+      iDestruct (own_valid_2 with "Ht1 Ht2") as %Hvalid.
+      rewrite singleton_op singleton_valid gmap_view_frag_op_valid in Hvalid.
+      destruct Hvalid as [Hcontra _].
+      by apply dfrac_valid_own_r in Hcontra.
+    Qed.
 
   End replica_backup_token.
 
diff --git a/src/program_proof/tulip/res_txnsys.v b/src/program_proof/tulip/res_txnsys.v
index 10e66b83f..e6c1f2c8d 100644
--- a/src/program_proof/tulip/res_txnsys.v
+++ b/src/program_proof/tulip/res_txnsys.v
@@ -1,4 +1,6 @@
-(** Global resources. *)
+From iris.algebra Require Import mono_nat mono_list gmap_view gset.
+From iris.algebra.lib Require Import dfrac_agree.
+From Perennial.base_logic Require Import ghost_map mono_nat saved_prop.
 From Perennial.program_proof Require Import grove_prelude.
 From Perennial.program_proof.rsm Require Import big_sep.
 From Perennial.program_proof.rsm.pure Require Import vslice fin_maps.
@@ -13,16 +15,16 @@ Section res.
 
     (** History generated by committed transactions for a certain key. *)
 
-    Definition own_cmtd_hist γ (k : dbkey) (h : dbhist) : iProp Σ.
-    Admitted.
+    Definition own_cmtd_hist γ (k : dbkey) (h : dbhist) : iProp Σ :=
+      own γ.(cmtd_hist) {[ k := ●ML{#1} h ]}.
 
-    Definition is_cmtd_hist_lb γ (k : dbkey) (h : dbhist) : iProp Σ.
-    Admitted.
+    Definition is_cmtd_hist_lb γ (k : dbkey) (h : dbhist) : iProp Σ :=
+      own γ.(cmtd_hist) {[ k := ◯ML h ]}.
 
     #[global]
-      Instance is_cmtd_hist_lb_persistent α key hist :
+    Instance is_cmtd_hist_lb_persistent α key hist :
       Persistent (is_cmtd_hist_lb α key hist).
-    Admitted.
+    Proof. apply _. Defined.
 
     Definition is_cmtd_hist_length_lb γ key n : iProp Σ :=
       ∃ lb, is_cmtd_hist_lb γ key lb ∗ ⌜(n ≤ length lb)%nat⌝.
@@ -31,18 +33,34 @@ Section res.
       prefix h1 h2 ->
       own_cmtd_hist γ k h1 ==∗
       own_cmtd_hist γ k h2.
-    Admitted.
+    Proof.
+      intros Hprefix.
+      iApply own_update.
+      apply singleton_update.
+      by apply mono_list_update.
+    Qed.
 
     Lemma cmtd_hist_witness {γ k h} :
       own_cmtd_hist γ k h -∗
       is_cmtd_hist_lb γ k h.
-    Admitted.
+    Proof.
+      iApply own_mono.
+      apply singleton_included_mono.
+      apply mono_list_included.
+    Qed.
 
     Lemma cmtd_hist_prefix {γ k h hlb} :
       own_cmtd_hist γ k h -∗
       is_cmtd_hist_lb γ k hlb -∗
       ⌜prefix hlb h⌝.
-    Admitted.
+    Proof.
+      iIntros "Hh Hlb".
+      iDestruct (own_valid_2 with "Hh Hlb") as %Hvalid.
+      iPureIntro. revert Hvalid.
+      rewrite singleton_op singleton_valid.
+      rewrite mono_list_both_dfrac_valid_L.
+      by intros [_ ?].
+    Qed.
 
   End cmtd_hist.
 
@@ -50,33 +68,49 @@ Section res.
 
     (** History generated by linearized transactions for a certain key. *)
 
-    Definition own_lnrz_hist γ (k : dbkey) (l : dbhist) : iProp Σ.
-    Admitted.
+    Definition own_lnrz_hist γ (k : dbkey) (h : dbhist) : iProp Σ :=
+      own γ.(lnrz_hist) {[ k := ●ML{#1} h ]}.
 
-    Definition is_lnrz_hist_lb γ (k : dbkey) (l : dbhist) : iProp Σ.
-    Admitted.
+    Definition is_lnrz_hist_lb γ (k : dbkey) (h : dbhist) : iProp Σ :=
+      own γ.(lnrz_hist) {[ k := ◯ML h ]}.
 
     #[global]
-      Instance is_lnrz_hist_lb_persistent α key hist :
+    Instance is_lnrz_hist_lb_persistent α key hist :
       Persistent (is_lnrz_hist_lb α key hist).
-    Admitted.
+    Proof. apply _. Defined.
 
     Lemma lnrz_hist_update {γ k l} l' :
       prefix l l' ->
       own_lnrz_hist γ k l ==∗
       own_lnrz_hist γ k l'.
-    Admitted.
+    Proof.
+      intros Hprefix.
+      iApply own_update.
+      apply singleton_update.
+      by apply mono_list_update.
+    Qed.
 
     Lemma lnrz_hist_witness γ k l :
       own_lnrz_hist γ k l -∗
       is_lnrz_hist_lb γ k l.
-    Admitted.
+    Proof.
+      iApply own_mono.
+      apply singleton_included_mono.
+      apply mono_list_included.
+    Qed.
 
     Lemma lnrz_hist_prefix {γ k h hlb} :
       own_lnrz_hist γ k h -∗
       is_lnrz_hist_lb γ k hlb -∗
       ⌜prefix hlb h⌝.
-    Admitted.
+    Proof.
+      iIntros "Hh Hlb".
+      iDestruct (own_valid_2 with "Hh Hlb") as %Hvalid.
+      iPureIntro. revert Hvalid.
+      rewrite singleton_op singleton_valid.
+      rewrite mono_list_both_dfrac_valid_L.
+      by intros [_ ?].
+    Qed.
 
     Definition is_lnrz_hist_at γ (k : dbkey) (ts : nat) (v : dbval) : iProp Σ :=
       ∃ lb, is_lnrz_hist_lb γ k lb ∗ ⌜lb !! ts = Some v⌝.
@@ -99,16 +133,17 @@ Section res.
     (** Mapping from transaction IDs to results (i.e., committed or aborted) of
     the transactions. *)
 
-    Definition own_txn_resm γ (resm : gmap nat txnres) : iProp Σ.
-    Admitted.
+    Definition own_txn_resm γ (resm : gmap nat txnres) : iProp Σ :=
+      ghost_map_auth γ.(txn_res) 1 resm ∗
+      ([∗ map] ts ↦ res ∈ resm, ghost_map_elem γ.(txn_res) ts DfracDiscarded res).
 
-    Definition is_txn_res γ (ts : nat) (res : txnres) : iProp Σ.
-    Admitted.
+    Definition is_txn_res γ (ts : nat) (res : txnres) : iProp Σ :=
+      ghost_map_elem γ.(txn_res) ts DfracDiscarded res.
 
     #[global]
     Instance is_txn_res_persistent γ ts res :
       Persistent (is_txn_res γ ts res).
-    Admitted.
+    Proof. apply _. Defined.
 
     Definition is_txn_committed γ ts wrs :=
       is_txn_res γ ts (ResCommitted wrs).
@@ -120,19 +155,33 @@ Section res.
       resm !! ts = None ->
       own_txn_resm γ resm ==∗
       own_txn_resm γ (<[ts := res]> resm).
-    Admitted.
+    Proof.
+      iIntros (Hnotin) "[Hauth Hfrags]".
+      iMod (ghost_map_insert ts res with "Hauth") as "[Hauth Hfrag]".
+      { apply Hnotin. }
+      iMod (ghost_map_elem_persist with "Hfrag") as "#Hfrag".
+      iFrame.
+      iModIntro.
+      by iApply (big_sepM_insert_2 with "[Hfrag] Hfrags").
+    Qed.
 
     Lemma txn_res_witness {γ resm} ts res :
       resm !! ts = Some res ->
       own_txn_resm γ resm -∗
       is_txn_res γ ts res.
-    Admitted.
+    Proof.
+      iIntros (Hres) "[Hauth Hfrags]".
+      by iDestruct (big_sepM_lookup with "Hfrags") as "Hfrag".
+    Qed.
 
     Lemma txn_res_lookup γ resm ts res :
       own_txn_resm γ resm -∗
       is_txn_res γ ts res -∗
       ⌜resm !! ts = Some res⌝.
-    Admitted.
+    Proof.
+      iIntros "[Hauth _] Hfrag".
+      iApply (ghost_map_lookup with "Hauth Hfrag").
+    Qed.
 
   End txn_res.
 
@@ -144,11 +193,11 @@ Section res.
     commit under an aborted state is impossible, as a non-participant group
     could have received [CmdPrep] and aborted. *)
 
-    Definition own_txn_oneshot_wrsm γ (wrsm : gmap nat (option dbmap)) : iProp Σ.
-    Admitted.
+    Definition own_txn_oneshot_wrsm γ (wrsm : gmap nat (option dbmap)) : iProp Σ :=
+      ghost_map_auth γ.(txn_oneshot_wrs) 1 wrsm.
 
-    Definition own_txn_oneshot_wrs γ (ts : nat) (dq : dfrac) (owrs : option dbmap) : iProp Σ.
-    Admitted.
+    Definition own_txn_oneshot_wrs γ (ts : nat) (dq : dfrac) (owrs : option dbmap) : iProp Σ :=
+      ghost_map_elem γ.(txn_oneshot_wrs) ts dq owrs.
 
     Definition own_txn_reserved_wrs γ (ts : nat) :=
       own_txn_oneshot_wrs γ ts (DfracOwn 1) None.
@@ -162,40 +211,57 @@ Section res.
     #[global]
     Instance txn_wrs_cancel_persistent γ ts :
       Persistent (is_txn_canceled_wrs γ ts).
-    Admitted.
+    Proof. apply _. Defined.
 
     #[global]
     Instance is_txn_wrs_persistent γ ts wrs :
       Persistent (is_txn_wrs γ ts wrs).
-    Admitted.
+    Proof. apply _. Defined.
 
     Lemma txn_oneshot_wrs_allocate γ wrsm ts :
       wrsm !! ts = None ->
       own_txn_oneshot_wrsm γ wrsm ==∗
       own_txn_oneshot_wrsm γ (<[ts := None]> wrsm) ∗ own_txn_reserved_wrs γ ts.
-    Admitted.
+    Proof.
+      iIntros (Hnone) "Hauth".
+      by iApply (ghost_map_insert with "Hauth").
+    Qed.
 
     Lemma txn_oneshot_wrs_cancel γ ts :
       own_txn_reserved_wrs γ ts ==∗ is_txn_canceled_wrs γ ts.
-    Admitted.
+    Proof.
+      iIntros "Hfrag".
+      iApply (ghost_map_elem_persist with "Hfrag").
+    Qed.
 
     Lemma txn_oneshot_wrs_update γ wrsm ts wrs :
       own_txn_reserved_wrs γ ts -∗
       own_txn_oneshot_wrsm γ wrsm ==∗
       own_txn_oneshot_wrsm γ (<[ts := Some wrs]> wrsm) ∗ is_txn_wrs γ ts wrs.
-    Admitted.
+    Proof.
+      iIntros "Hfrag Hauth".
+      iMod (ghost_map_update (Some wrs) with "Hauth Hfrag") as "[Hauth Hfrag]".
+      iMod (ghost_map_elem_persist with "Hfrag") as "#Hfrag".
+      by iFrame "∗ #".
+    Qed.
 
     Lemma txn_oneshot_wrs_lookup γ wrsm ts dq owrs :
       own_txn_oneshot_wrs γ ts dq owrs -∗
       own_txn_oneshot_wrsm γ wrsm -∗
       ⌜wrsm !! ts = Some owrs⌝.
-    Admitted.
+    Proof.
+      iIntros "Hfrag Hauth".
+      iApply (ghost_map_lookup with "Hauth Hfrag").
+    Qed.
 
     Lemma txn_oneshot_wrs_agree γ ts dq1 dq2 owrs1 owrs2 :
       own_txn_oneshot_wrs γ ts dq1 owrs1 -∗
       own_txn_oneshot_wrs γ ts dq2 owrs2 -∗
       ⌜owrs2 = owrs1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hfrag1 Hfrag2".
+      by iDestruct (ghost_map_elem_agree with "Hfrag1 Hfrag2") as %?.
+    Qed.
 
     Lemma txn_wrs_lookup γ wrsm ts wrs :
       is_txn_wrs γ ts wrs -∗
@@ -217,7 +283,11 @@ Section res.
       is_txn_wrs γ ts wrs1 -∗
       is_txn_wrs γ ts wrs2 -∗
       ⌜wrs2 = wrs1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hfrag1 Hfrag2".
+      iDestruct (ghost_map_elem_agree with "Hfrag1 Hfrag2") as %Heq.
+      by inv Heq.
+    Qed.
 
   End txn_oneshot_wrs.
 
@@ -225,28 +295,39 @@ Section res.
 
     (** Timestamps of transactions that have linearized. *)
 
-    Definition own_lnrz_tids γ (tids : gset nat) : iProp Σ.
-    Admitted.
+    Definition own_lnrz_tids γ (tids : gset nat) : iProp Σ :=
+      ghost_map_auth γ.(lnrz_tid) 1 (gset_to_gmap tt tids).
 
-    Definition is_lnrz_tid γ (tid : nat) : iProp Σ.
-    Admitted.
+    Definition is_lnrz_tid γ (tid : nat) : iProp Σ :=
+      ghost_map_elem γ.(lnrz_tid) tid DfracDiscarded tt.
 
     #[global]
-      Instance is_lnrz_tid_persistent γ tid :
+    Instance is_lnrz_tid_persistent γ tid :
       Persistent (is_lnrz_tid γ tid).
-    Admitted.
+    Proof. apply _. Defined.
 
     Lemma lnrz_tid_insert γ tids tid :
       tid ∉ tids ->
       own_lnrz_tids γ tids ==∗
       own_lnrz_tids γ ({[ tid ]} ∪ tids) ∗ is_lnrz_tid γ tid.
-    Admitted.
+    Proof.
+      iIntros (Hnotin) "Hauth".
+      iMod (ghost_map_insert tid tt with "Hauth") as "[Hauth Hfrag]".
+      { by rewrite lookup_gset_to_gmap_None. }
+      rewrite -gset_to_gmap_union_singleton.
+      iMod (ghost_map_elem_persist with "Hfrag") as "Hfrag".
+      by iFrame.
+    Qed.
 
     Lemma lnrz_tid_elem_of γ tids tid :
       own_lnrz_tids γ tids -∗
       is_lnrz_tid γ tid -∗
       ⌜tid ∈ tids⌝.
-    Admitted.
+    Proof.
+      iIntros "Hauth Hfrag".
+      iDestruct (ghost_map_lookup with "Hauth Hfrag") as %Hlookup.
+      by apply lookup_gset_to_gmap_Some in Hlookup as [? _].
+    Qed.
 
   End lnrz_tid.
 
@@ -254,29 +335,43 @@ Section res.
 
     (** Timestamps of transactions predicted to abort. *)
 
-    Definition own_wabt_tids γ (tids : gset nat) : iProp Σ.
-    Admitted.
+    Definition own_wabt_tids γ (tids : gset nat) : iProp Σ :=
+      ghost_map_auth γ.(wabt_tid) 1 (gset_to_gmap tt tids).
 
-    Definition own_wabt_tid γ (tid : nat) : iProp Σ.
-    Admitted.
+    Definition own_wabt_tid γ (tid : nat) : iProp Σ :=
+      ghost_map_elem γ.(wabt_tid) tid (DfracOwn 1) tt.
 
     Lemma wabt_tid_insert {γ tids} tid :
       tid ∉ tids ->
       own_wabt_tids γ tids ==∗
       own_wabt_tids γ ({[ tid ]} ∪ tids) ∗ own_wabt_tid γ tid.
-    Admitted.
+    Proof.
+      iIntros (Hnotin) "Hauth".
+      iMod (ghost_map_insert tid tt with "Hauth") as "[Hauth Hfrag]".
+      { by rewrite lookup_gset_to_gmap_None. }
+      rewrite -gset_to_gmap_union_singleton.
+      by iFrame.
+    Qed.
 
     Lemma wabt_tid_delete {γ tids} tid :
       own_wabt_tid γ tid -∗
       own_wabt_tids γ tids ==∗
       own_wabt_tids γ (tids ∖ {[ tid ]}).
-    Admitted.
+    Proof.
+      iIntros "Hfrag Hauth".
+      iMod (ghost_map_delete with "Hauth Hfrag") as "Hauth".
+      by rewrite -gset_to_gmap_difference_singleton.
+    Qed.
 
     Lemma wabt_tid_elem_of γ tids tid :
       own_wabt_tids γ tids -∗
       own_wabt_tid γ tid -∗
       ⌜tid ∈ tids⌝.
-    Admitted.
+    Proof.
+      iIntros "Hauth Hfrag".
+      iDestruct (ghost_map_lookup with "Hauth Hfrag") as %Hlookup.
+      by apply lookup_gset_to_gmap_Some in Hlookup as [? _].
+    Qed.
 
   End wabt_tid.
 
@@ -285,23 +380,29 @@ Section res.
     (** Pairs of timestamp and write-set of transactions predicted to commit or
     has committed. *)
 
-    Definition own_cmt_tmods γ (tmods : gmap nat dbmap) : iProp Σ.
-    Admitted.
+    Definition own_cmt_tmods γ (tmods : gmap nat dbmap) : iProp Σ :=
+      ghost_map_auth γ.(cmt_tmod) 1 tmods.
 
-    Definition own_cmt_tmod γ (tid : nat) (wrs : dbmap) : iProp Σ.
-    Admitted.
+    Definition own_cmt_tmod γ (tid : nat) (wrs : dbmap) : iProp Σ :=
+       ghost_map_elem γ.(cmt_tmod) tid (DfracOwn 1) wrs.
 
     Lemma cmt_tmod_insert {γ tmods} tid wrs :
       tmods !! tid = None ->
       own_cmt_tmods γ tmods ==∗
       own_cmt_tmods γ (<[tid := wrs]> tmods) ∗ own_cmt_tmod γ tid wrs.
-    Admitted.
+    Proof.
+      iIntros (Hnotin) "Hauth".
+      by iApply (ghost_map_insert with "Hauth").
+    Qed.
 
     Lemma cmt_tmod_lookup γ tmods tid wrs :
       own_cmt_tmods γ tmods -∗
       own_cmt_tmod γ tid wrs -∗
       ⌜tmods !! tid = Some wrs⌝.
-    Admitted.
+    Proof.
+      iIntros "Hauth Hfrag".
+      by iApply (ghost_map_lookup with "Hauth Hfrag").
+    Qed.
 
   End cmt_tmod.
 
@@ -309,23 +410,32 @@ Section res.
 
     (** Exclusive tokens of transaction IDs. *)
 
-    Definition own_excl_tids γ (tids : gset nat) : iProp Σ.
-    Admitted.
+    Definition own_excl_tids γ (tids : gset nat) : iProp Σ :=
+      ghost_map_auth γ.(excl_tid) 1 (gset_to_gmap tt tids).
 
-    Definition own_excl_tid γ (tid : nat) : iProp Σ.
-    Admitted.
+    Definition own_excl_tid γ (tid : nat) : iProp Σ :=
+      ghost_map_elem γ.(excl_tid) tid (DfracOwn 1) tt.
 
     Lemma excl_tid_insert γ tids tid :
       tid ∉ tids ->
       own_excl_tids γ tids ==∗
       own_excl_tids γ ({[ tid ]} ∪ tids) ∗ own_excl_tid γ tid.
-    Admitted.
+    Proof.
+      iIntros (Hnotin) "Hauth".
+      iMod (ghost_map_insert tid tt with "Hauth") as "[Hauth Hfrag]".
+      { by rewrite lookup_gset_to_gmap_None. }
+      rewrite -gset_to_gmap_union_singleton.
+      by iFrame.
+    Qed.
 
     Lemma excl_tid_ne γ tid1 tid2 :
       own_excl_tid γ tid1 -∗
       own_excl_tid γ tid2 -∗
       ⌜tid2 ≠ tid1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hfrag1 Hfrag2".
+      iApply (ghost_map_elem_ne with "Hfrag2 Hfrag1").
+    Qed.
 
     Lemma excl_tid_not_elem_of γ tids tid :
       ([∗ set] t ∈ tids, own_excl_tid γ t) -∗
@@ -345,24 +455,86 @@ Section res.
     (** Exclusive tokens of transaction clients used in proving freshness of
     slow-path prepare decision proposal. *)
 
-    Definition own_txn_client_tokens γ (ctm : gmap nat (gset u64)) : iProp Σ.
-    Admitted.
+    Definition own_txn_client_tokens γ (ctm : gmap nat (gset u64)) : iProp Σ :=
+      ∃ tgs : gset (nat * u64),
+        ghost_map_auth γ.(txn_client_token) 1 (gset_to_gmap tt tgs) ∧
+        ⌜(∀ t g, (t, g) ∈ tgs -> ∃ gs, ctm !! t = Some gs ∧ g ∈ gs)⌝.
 
-    Definition own_txn_client_token γ (tid : nat) (gid : u64) : iProp Σ.
-    Admitted.
+    Definition own_txn_client_token γ (tid : nat) (gid : u64) : iProp Σ :=
+      ghost_map_elem γ.(txn_client_token) (tid, gid) (DfracOwn 1) tt.
 
     Lemma txn_client_token_insert {γ ctm} ts gids :
       ctm !! ts = None ->
       own_txn_client_tokens γ ctm ==∗
       own_txn_client_tokens γ (<[ts := gids]> ctm) ∗
       ([∗ set] gid ∈ gids, own_txn_client_token γ ts gid).
-    Admitted.
+    Proof.
+      iIntros (Hnotin) "Hauth".
+      iDestruct "Hauth" as (tgs) "[Hauth %Hincl]".
+      set tgsx : gset (nat * u64) := set_map (λ g, (ts, g)) gids.
+      iMod (ghost_map_insert_big (gset_to_gmap tt tgsx) with "Hauth") as "[Hauth Hfrags]".
+      { rewrite map_disjoint_dom 2!dom_gset_to_gmap.
+        intros [t g] Hin1 Hin2.
+        specialize (Hincl _ _ Hin2).
+        destruct Hincl as (gs & Hin & Hg).
+        apply elem_of_map in Hin1 as (g' & Heq & _).
+        inv Heq.
+      }
+      iModIntro.
+      iSplitL "Hauth".
+      { iExists (tgsx ∪ tgs).
+        iSplit.
+        { replace (_ ∪ _) with (gset_to_gmap () (tgsx ∪ tgs)); first done.
+          apply map_eq.
+          intros tg.
+          rewrite lookup_union.
+          rewrite 3!lookup_gset_to_gmap.
+          destruct (decide (tg ∈ tgsx)) as [Htgin | Htgnotin].
+          { rewrite option_guard_True.
+            { rewrite option_guard_True; last done.
+              by rewrite union_Some_l.
+            }
+            set_solver.
+          }
+          rewrite (option_guard_False (tg ∈ tgsx)); last done.
+          rewrite option_union_left_id.
+          destruct (decide (tg ∈ tgs)) as [Htgin' | Htgnotin'].
+          { rewrite option_guard_True.
+            { by rewrite option_guard_True. }
+            set_solver.
+          }
+          { rewrite option_guard_False.
+            { by rewrite option_guard_False. }
+            set_solver.
+          }
+        }
+        iPureIntro.
+        intros t g Htg.
+        apply elem_of_union in Htg.
+        destruct Htg as [Hintgsx | Hintgs]; last first.
+        { specialize (Hincl _ _ Hintgs).
+          destruct Hincl as (gs & Ht & Hin).
+          destruct (decide (t = ts)) as [-> | Hne]; first congruence.
+          exists gs.
+          by rewrite lookup_insert_ne.
+        }
+        subst tgsx.
+        apply elem_of_map in Hintgsx as (g' & Heq & Hin).
+        inv Heq.
+        exists gids.
+        by rewrite lookup_insert.
+      }
+      { by rewrite big_sepM_gset_to_gmap big_opS_set_map. }
+    Qed.
 
     Lemma txn_client_token_excl γ ts gid :
       own_txn_client_token γ ts gid -∗
       own_txn_client_token γ ts gid -∗
       False.
-    Admitted.
+    Proof.
+      iIntros "Hfrag1 Hfrag2".
+      by iDestruct (ghost_map_elem_ne with "Hfrag1 Hfrag2") as %?.
+    Qed.
 
   End txn_client_token.
 
@@ -370,34 +542,46 @@ Section res.
 
     (** Transaction post-conditions. Might need a [ghost_map nat gname] and a [saved_prop]? *)
 
-    Definition own_txn_postconds γ (posts : gmap nat (dbmap -> Prop)) : iProp Σ.
-    Admitted.
+    Definition own_txn_postconds γ (posts : gmap nat (dbmap -> Prop)) : iProp Σ :=
+      ghost_map_auth γ.(txn_postcond) 1 posts.
 
-    Definition is_txn_postcond γ (tid : nat) (post : dbmap -> Prop) : iProp Σ.
-    Admitted.
+    Definition is_txn_postcond γ (tid : nat) (post : dbmap -> Prop) : iProp Σ :=
+      ghost_map_elem γ.(txn_postcond) tid DfracDiscarded post.
 
     #[global]
-      Instance is_txn_postcond_persistent γ tid post :
+    Instance is_txn_postcond_persistent γ tid post :
       Persistent (is_txn_postcond γ tid post).
-    Admitted.
+    Proof. apply _. Defined.
 
     Lemma txn_postcond_insert γ posts tid post :
       posts !! tid = None ->
       own_txn_postconds γ posts ==∗
       own_txn_postconds γ (<[tid := post]> posts) ∗ is_txn_postcond γ tid post.
-    Admitted.
+    Proof.
+      iIntros (Hnotin) "Hauth".
+      iMod (ghost_map_insert tid post with "Hauth") as "[Hauth Hfrag]".
+      { apply Hnotin. }
+      iMod (ghost_map_elem_persist with "Hfrag") as "Hfrag".
+      by iFrame.
+    Qed.
 
     Lemma txn_postcond_elem_of γ posts tid post :
       own_txn_postconds γ posts -∗
       is_txn_postcond γ tid post -∗
       ⌜posts !! tid = Some post⌝.
-    Admitted.
+    Proof.
+      iIntros "Hauth Hfrag".
+      by iApply (ghost_map_lookup with "Hauth Hfrag").
+    Qed.
 
     Lemma txn_postcond_agree γ tid post1 post2 :
       is_txn_postcond γ tid post1 -∗
       is_txn_postcond γ tid post2 -∗
       ⌜post2 = post1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hfrag1 Hfrag2".
+      iApply (ghost_map_elem_agree with "Hfrag2 Hfrag1").
+    Qed.
 
   End txn_postcond.
 
@@ -405,33 +589,36 @@ Section res.
 
     (** Largest timestamp assigned. *)
 
-    Definition own_largest_ts γ (ts : nat) : iProp Σ.
-    Admitted.
+    Definition own_largest_ts γ (ts : nat) : iProp Σ :=
+      mono_nat_auth_own γ.(largest_ts) 1 ts.
 
-    Definition is_largest_ts_lb γ (ts : nat) : iProp Σ.
-    Admitted.
+    Definition is_largest_ts_lb γ (ts : nat) : iProp Σ :=
+      mono_nat_lb_own γ.(largest_ts) ts.
+
+    #[global]
+    Instance is_largest_ts_lb_persistent γ ts :
+      Persistent (is_largest_ts_lb γ ts).
+    Proof. apply _. Defined.
 
     Lemma largest_ts_le γ tslb ts :
       is_largest_ts_lb γ tslb -∗
       own_largest_ts γ ts -∗
       ⌜(tslb ≤ ts)%nat⌝.
-    Admitted.
+    Proof.
+      iIntros "Hlb Hauth".
+      by iDestruct (mono_nat_lb_own_valid with "Hauth Hlb") as %[_ Hle].
+    Qed.
 
     Lemma largest_ts_witness γ ts :
       own_largest_ts γ ts -∗
       is_largest_ts_lb γ ts.
-    Admitted.
+    Proof. iApply mono_nat_lb_own_get. Qed.
 
     Lemma largest_ts_lb_weaken {γ ts} ts' :
       (ts' ≤ ts)%nat ->
       is_largest_ts_lb γ ts -∗
       is_largest_ts_lb γ ts'.
-    Admitted.
-
-    #[global]
-      Instance is_largest_ts_lb_persistent γ ts :
-      Persistent (is_largest_ts_lb γ ts).
-    Admitted.
+    Proof. iIntros (Hle) "Hlb". by iApply mono_nat_lb_own_le. Qed.
 
   End largest_ts.
 
diff --git a/src/program_proof/tulip/stability.v b/src/program_proof/tulip/stability.v
index 188d79c95..f68b51684 100644
--- a/src/program_proof/tulip/stability.v
+++ b/src/program_proof/tulip/stability.v
@@ -6,17 +6,6 @@ Local Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.
 
 Definition proposals := gmap nat bool.
 
-Inductive vote :=
-| Accept (d : bool)
-| Reject.
-
-#[global]
-Instance vote_eq_decision :
-  EqDecision vote.
-Proof. solve_decision. Qed.
-
-Definition ballot := list vote.
-
 Section def.
   Context `{Countable A}.
   Implicit Type r : nat.