Break consensus RA into two separate RAs

1. The inclusion property is now maintained by the paxos and the txnlog
invariant, rather at the RA level.

2. The specification of paxos and txnlog lookup now additionally takes the
command pool, and gives a proof that the new log is a subset of the command
pool.

3. The RA rule for extending the log no longer requires subsumption between the
log and the command pool, and in exchange lose the subsumption rule.

src/program_proof/tulip/inv.v

@@ -428,6 +428,7 @@ Section alloc.
       rewrite dom_gset_to_gmap.
       assert (Hlip : locked_impl_prepared ∅ (gset_to_gmap O keys_all)).
       { intros k t Ht Hnz. by apply lookup_gset_to_gmap_Some in Ht as [_ <-]. }
+      rewrite /txn_cpool_subsume_log Forall_nil.
       done.
     }
     iAssert ([∗ set] gid ∈ gids_all, [∗ set] rid ∈ rids_all, replica_inv γ gid rid)%I

src/program_proof/tulip/inv_group.v

@@ -334,7 +334,8 @@ Section inv.
       "%Hcm"      ∷ ⌜cm = omap txnst_to_option_bool stm⌝ ∗
       "%Hpil"     ∷ ⌜prepared_impl_locked stm tspreps⌝ ∗
       "%Hlip"     ∷ ⌜locked_impl_prepared stm tspreps⌝ ∗
-      "%Htsnz"    ∷ ⌜stm !! O = None⌝.
+      "%Htsnz"    ∷ ⌜stm !! O = None⌝ ∗
+      "%Hcscincl" ∷ ⌜txn_cpool_subsume_log cpool log⌝.
 
   Definition group_inv_no_log_with_cpool
     γ (gid : u64) (log : dblog) (cpool : gset ccommand) : iProp Σ :=

src/program_proof/tulip/inv_txnlog.v

@@ -29,6 +29,7 @@ Section inv_txnlog.
       "Htcpool"    ∷ own_txn_cpool_half γ gid tcpool ∗
       "Hplog"      ∷ own_log_half π plog ∗
       "Hpcpool"    ∷ own_cpool_half π pcpool ∗
+      "%Hcsincl"   ∷ ⌜txn_cpool_subsume_log tcpool tlog⌝ ∗
       "%Hlogabs"   ∷ ⌜Forall2 (λ tc pc, encode_ccommand tc pc) tlog plog⌝ ∗
       "%Hcpoolabs" ∷ ⌜set_Forall (λ pc, ∃ tc, tc ∈ tcpool ∧ encode_ccommand tc pc) pcpool⌝.
 
@@ -61,7 +62,11 @@ Section alloc.
     rewrite -!big_sepM_sep.
     iApply (big_sepM_mono with "Hall").
     iIntros (gid π Hπ) "[[Htlog Htcpool] [Hplog Hpcpool]]".
-    by iFrame.
+    iFrame.
+    iPureIntro.
+    split.
+    { rewrite /txn_cpool_subsume_log. by apply Forall_nil. }
+    done.
   Qed.
 
 End alloc.

src/program_proof/tulip/invariance/execute_commit.v

@@ -25,8 +25,8 @@ Section execute_commit.
     }
     iAssert (is_txn_pwrs γ gid ts pwrs ∗ ⌜dom pwrs ⊆ keys_all⌝)%I as "[#Hpwrs %Hdompwrs]".
     { do 2 iNamed "Hgroup".
+      rename Hcscincl into Hincl.
       iDestruct (txn_log_prefix with "Hlog Hloglb") as %Hprefix.
-      iDestruct (txn_log_cpool_incl with "Hlog Hcpool") as %Hincl.
       assert (Hin : CmdCommit ts pwrs ∈ cpool).
       { rewrite /txn_cpool_subsume_log Forall_forall in Hincl.
         apply Hincl.

src/program_proof/tulip/invariance/learn_abort.v

@@ -70,6 +70,7 @@ Section inv.
     group_inv_no_log_with_cpool γ gid (log ++ [CmdAbort ts]) cpool.
   Proof.
     iIntros (Hsubsume) "Htxnsys Hkeys Hgroup".
+    pose proof Hsubsume as Hcscincl.
     rewrite /txn_cpool_subsume_log Forall_app Forall_singleton in Hsubsume.
     destruct Hsubsume as [Hsubsume Hc].
     do 2 iNamed "Hgroup".

src/program_proof/tulip/invariance/learn_commit.v

@@ -105,6 +105,7 @@ Section inv.
     group_inv_no_log_with_cpool γ gid (log ++ [CmdCommit ts pwrs]) cpool.
   Proof.
     iIntros (Hsubsume) "Htxnsys Hkeys Hgroup".
+    pose proof Hsubsume as Hcscincl.
     rewrite /txn_cpool_subsume_log Forall_app Forall_singleton in Hsubsume.
     destruct Hsubsume as [Hsubsume Hc].
     do 2 iNamed "Hgroup".

src/program_proof/tulip/invariance/submit.v

@@ -12,6 +12,10 @@ Section inv.
     do 2 iNamed "Hgroup".
     iDestruct (big_sepS_insert_2 with "Hsafe Hsafecp") as "Hsafecp'".
     iFrame "∗ # %".
+    iPureIntro.
+    rewrite /txn_cpool_subsume_log.
+    apply (Forall_impl _ _ _ Hcscincl).
+    set_solver.
   Qed.
 
 End inv.

src/program_proof/tulip/paxos/inv.v

@@ -498,7 +498,9 @@ Section inv.
       "#Hsafepsb"   ∷ ([∗ map] t ↦ v ∈ psb, safe_base_proposal γ nids t v) ∗
       "%Hvp"        ∷ ⌜valid_proposals ps psb⌝ ∗
       "%Hdomtermlm" ∷ ⌜dom termlm = nids⌝ ∗
-      "%Hdompsb"    ∷ ⌜free_terms (dom psb) termlm⌝.
+      "%Hdompsb"    ∷ ⌜free_terms (dom psb) termlm⌝ ∗
+      (* constraint on the external states *)
+      "%Hcsincl"    ∷ ⌜cpool_subsume_log log cpool⌝.
 
   #[global]
   Instance paxos_inv_timeless γ nids :
@@ -632,6 +634,19 @@ End inv_network.
 Section lemma.
   Context `{!paxos_ghostG Σ}.
 
+  Lemma paxos_inv_impl_cpool_subsume_log γ nids log cpool :
+    own_log_half γ log -∗
+    own_cpool_half γ cpool -∗
+    paxos_inv γ nids -∗
+    ⌜cpool_subsume_log log cpool⌝.
+  Proof.
+    iIntros "HlogX HcpoolX Hinv".
+    iNamed "Hinv".
+    iDestruct (log_agree with "Hlog HlogX") as %->.
+    iDestruct (cpool_agree with "Hcpool HcpoolX") as %->.
+    done.
+  Qed.
+
   Lemma equal_latest_longest_proposal_nodedec_prefix dss dsslb t v :
     map_Forall2 (λ _ dslb ds, prefix dslb ds ∧ (t ≤ length dslb)%nat) dsslb dss ->
     equal_latest_longest_proposal_nodedec dsslb t v ->
@@ -1326,12 +1341,14 @@ Section alloc.
     { by rewrite insert_empty /valid_proposals map_Forall2_singleton. }
     split.
     { by rewrite dom_gset_to_gmap. }
+    split.
     { rewrite insert_empty dom_singleton_L.
       split; first apply is_term_of_node_partitioned.
       intros nid terml Hterml t Hton Hlt.
       rewrite not_elem_of_singleton.
       lia.
     }
+    { by rewrite /cpool_subsume_log Forall_nil. }
   Qed.
 
 End alloc.

src/program_proof/tulip/paxos/invariance/commit.v

@@ -92,10 +92,9 @@ Section commit.
       iDestruct (big_sepL_elem_of with "Hpcmds") as "Hc"; first apply Hc'.
       iApply (cpool_lookup with "Hc Hcpool").
     }
-    iMod (log_update with "Hlogcli Hlog Hcpool") as "(Hlogcli & Hlog & Hcpool)".
-    { apply Hsubsume. }
+    iMod (log_update with "Hlogcli Hlog") as "[Hlogcli Hlog]".
     { apply Hext. }
-    by iFrame "∗ # %".
+    by iFrame "∗ #".
   Qed.
 
 End commit.

src/program_proof/tulip/paxos/program/paxos_lookup.v

@@ -9,9 +9,9 @@ Section lookup.
   Theorem wp_Paxos__Lookup (px : loc) (lsn : u64) nidme γ :
     is_paxos px nidme γ -∗
     {{{ True }}}
-    <<< ∀∀ log, own_log_half γ log >>>
+    <<< ∀∀ log cpool, own_consensus_half γ log cpool >>>
       Paxos__Lookup #px #lsn @ ↑paxosNS
-    <<< ∃∃ log', own_log_half γ log' >>>
+    <<< ∃∃ log', own_consensus_half γ log' cpool ∗ ⌜cpool_subsume_log log' cpool⌝ >>>
     {{{ (v : string) (ok : bool), RET (#(LitString v), #ok);
         ⌜if ok then log' !! (uint.nat lsn) = Some v else True⌝
     }}}.
@@ -41,11 +41,15 @@ Section lookup.
         iFrame "∗ # %".
       }
       wp_pures.
-      (* Simply take and give back the same log. *)
+      (* Open the invariant to obtain subsumption property. *)
+      iInv "Hinv" as "> HinvO" "HinvC".
       iMod (ncfupd_mask_subseteq (⊤ ∖ ↑paxosNS)) as "Hclose"; first solve_ndisj.
-      iMod "HAU" as (logcli) "[Hlogcli HAU]".
-      iMod ("HAU" with "Hlogcli") as "HΦ".
+      iMod "HAU" as (logcli cpoolcli) "[[Hlogcli Hcpoolcli] HAU]".
+      iDestruct (paxos_inv_impl_cpool_subsume_log with "Hlogcli Hcpoolcli HinvO") as %Hincl.
+      iMod ("HAU" with "[$Hlogcli $Hcpoolcli]") as "HΦ".
+      { done. }
       iMod "Hclose" as "_".
+      iMod ("HinvC" with "HinvO") as "_".
       by iApply "HΦ".
     }
     rename Heqb into Hlt.
@@ -68,7 +72,7 @@ Section lookup.
     iApply ncfupd_wp.
     iInv "Hinv" as "> HinvO" "HinvC".
     iMod (ncfupd_mask_subseteq (⊤ ∖ ↑paxosNS)) as "Hmask"; first solve_ndisj.
-    iMod "HAU" as (logcli) "[Hlogcli HAU]".
+    iMod "HAU" as (logcli cpoolcli) "[[Hlogcli Hcpoolcli] HAU]".
     set logc := take _ log.
     iNamed "Hnids".
     iMod (paxos_inv_commit logc with "[] Hlogcli Hlogn HinvO") as "(Hlogcli & Hlogn & HinvO)".
@@ -78,7 +82,10 @@ Section lookup.
       iFrame "Hsafe".
     }
     iDestruct "Hlogcli" as (logcli') "[Hlogcli %Hprefix]".
-    iMod ("HAU" with "Hlogcli") as "HΦ".
+    (* Obtain subsumption. *)
+    iDestruct (paxos_inv_impl_cpool_subsume_log with "Hlogcli Hcpoolcli HinvO") as %Hincl.
+    iMod ("HAU" with "[$Hlogcli $Hcpoolcli]") as "HΦ".
+    { done. }
     iMod "Hmask" as "_".
     iMod ("HinvC" with "HinvO") as "_".
     iModIntro.

src/program_proof/tulip/paxos/program/paxos_submit.v

@@ -31,10 +31,15 @@ Section submit.
     iMod ("HAU" with "Hcpoolcli") as "HΦ".
     iMod "Hmask" as "_".
     iMod ("HinvC" with "[-HΦ]") as "_".
-    { iFrame "∗ # %". }
+    { iFrame "∗ # %".
+      iPureIntro.
+      rewrite /cpool_subsume_log.
+      apply (Forall_impl _ _ _ Hcsincl).
+      set_solver.
+    }
     iModIntro.
     (* Some cleanup to avoid name collision. *)
-    iClear "Hsafelog". clear log.
+    iClear "Hsafelog". clear Hcsincl log.
 
     (*@ func (px *Paxos) Submit(v string) (uint64, uint64) {                    @*)
     (*@     px.mu.Lock()                                                        @*)

src/program_proof/tulip/paxos/res.v

@@ -23,6 +23,9 @@ Section res.
     Definition own_cpool_half γ (vs : gset string) : iProp Σ.
     Admitted.
 
+    Definition own_consensus_half γ (l : ledger) (vs : gset string) : iProp Σ :=
+      own_log_half γ l ∗ own_cpool_half γ vs.
+
     Definition is_cmd_receipt γ (c : string) : iProp Σ.
     Admitted.
 
@@ -43,13 +46,11 @@ Section res.
 
     (** Rules. *)
 
-    Lemma log_update {γ} l1 l2 vs :
-      cpool_subsume_log l2 vs ->
+    Lemma log_update {γ} l1 l2 :
       prefix l1 l2 ->
       own_log_half γ l1 -∗
-      own_log_half γ l1 -∗
-      own_cpool_half γ vs ==∗
-      own_log_half γ l2 ∗ own_log_half γ l2 ∗ own_cpool_half γ vs.
+      own_log_half γ l1 ==∗
+      own_log_half γ l2 ∗ own_log_half γ l2.
     Admitted.
 
     Lemma log_agree {γ} l1 l2 :
@@ -100,12 +101,6 @@ Section res.
       ⌜v ∈ vs⌝.
     Admitted.
 
-    Lemma log_cpool_subsume {γ l vs} :
-      own_log_half γ l -∗
-      own_cpool_half γ vs -∗
-      ⌜cpool_subsume_log l vs⌝.
-    Admitted.
-
   End consensus.
 
   Section proposal.

src/program_proof/tulip/program/replica/replica_applier.v

@@ -60,16 +60,17 @@ Section program.
     { iNamed "Hgroup". iFrame. }
     (* Obtain a lower bound before passing it to Paxos. *)
     iDestruct (txn_log_witness with "Hpaxos") as "#Hlb".
-    iExists paxos. iFrame.
-    iIntros (paxos') "Hpaxos".
+    iNamed "Hgroup".
+    iFrame.
+    iIntros (paxos') "[[Hpaxos Hcpool] %Hincl]".
     (* Obtain prefix between the old and new logs. *)
     iDestruct (txn_log_prefix with "Hpaxos Hlb") as %Hpaxos.
     destruct Hpaxos as [cmds Hpaxos].
     (* Obtain inclusion between the command pool and the log. *)
-    iAssert (⌜txn_cpool_subsume_log cpool paxos'⌝)%I as %Hincl.
-    { iNamed "Hgroup".
-      by iDestruct (txn_log_cpool_incl with "Hpaxos Hcpool") as %?.
-    }
+    (* iAssert (⌜txn_cpool_subsume_log cpool paxos'⌝)%I as %Hincl. *)
+    (* { iNamed "Hgroup". *)
+    (*   by iDestruct (txn_log_cpool_incl with "Hpaxos Hcpool") as %?. *)
+    (* } *)
     (* Transfer validity of command input on cpool to log; used when executing @apply. *)
     pose proof (set_Forall_Forall_subsume _ _ _ Hvcmds Hincl) as Hvc.
     (* Obtain prefix between the applied log and the new log; needed later. *)
@@ -80,6 +81,7 @@ Section program.
 
     (*@         // Ghost action: Learn a list of new commands.                  @*)
     (*@                                                                         @*)
+    iAssert (group_inv_no_log_with_cpool γ gid paxos cpool)%I with "[$Hgroup $Hcpool]" as "Hgroup".
     iMod (group_inv_learn with "Htxnsys Hkeys Hgroup") as "(Htxnsys & Hkeys & Hgroup)".
     { apply Hincl. }
     iDestruct (group_inv_merge_log_hide_cpool with "Hpaxos Hgroup") as "Hgroup".

src/program_proof/tulip/program/txnlog/txnlog.v

@@ -23,9 +23,9 @@ Section program.
   Theorem wp_TxnLog__Lookup (log : loc) (lsn : u64) (gid : u64) γ :
     is_txnlog log gid γ -∗
     {{{ True }}}
-    <<< ∀∀ l, own_txn_log_half γ gid l >>>
+    <<< ∀∀ l s, own_txn_consensus_half γ gid l s >>>
       TxnLog__Lookup #log #lsn @ ↑paxosNS ∪ ↑txnlogNS
-    <<< ∃∃ l', own_txn_log_half γ gid l' >>>
+    <<< ∃∃ l', own_txn_consensus_half γ gid l' s ∗ ⌜txn_cpool_subsume_log s l'⌝ >>>
     {{{ (c : ccommand) (ok : bool) (pwrsP : Slice.t), RET (ccommand_to_val pwrsP c, #ok);
         (if ok then own_pwrs_slice pwrsP c else True) ∗
         ⌜if ok then l' !! (uint.nat lsn) = Some c else True⌝
@@ -42,17 +42,15 @@ Section program.
     wp_apply (wp_Paxos__Lookup with "Hpx").
     iInv "Hinv" as "> HinvO" "HinvC".
     rewrite difference_difference_l_L.
-    iMod "HAU" as (tlogX) "[HtlogX HAU]".
+    iMod "HAU" as (tlogX tcpoolX) "[[HtlogX HtcpoolX] HAU]".
     iModIntro.
     iNamed "HinvO".
     (* Witness a lower bound of the paxos log. *)
     iDestruct (log_witness with "Hplog") as "#Hploglb".
     (* Pass the paxos log to the paxos library. *)
-    iFrame "Hplog".
+    iFrame "Hplog Hpcpool".
     (* Get back the updated paxos log. *)
-    iIntros (plog') "Hplog".
-    (* Derive inclusion property between paxos log and cpool. *)
-    iDestruct (log_cpool_subsume with "Hplog Hpcpool") as %Hincl.
+    iIntros (plog') "[[Hplog Hpcool] %Hincl]".
     (* Prove that the new paxos log is an extension of the old one. *)
     iDestruct (log_prefix with "Hplog Hploglb") as %Hprefix.
     destruct Hprefix as [plogext Hplog].
@@ -69,23 +67,26 @@ Section program.
       destruct Hcpoolabs as (tc & Htc & Henc).
       by exists tc.
     }
-    (* Agreement of txn log. *)
+    (* Agreement of txn log and command pool. *)
     iDestruct (txn_log_agree with "Htlog HtlogX") as %->.
+    iDestruct (txn_cpool_agree with "Htcpool HtcpoolX") as %->.
     (* Update the txn log. *)
-    iMod (txn_log_extend tlogext with "Htlog HtlogX Htcpool")
-      as "(Htlog & HtlogX & Htcpool)".
+    iMod (txn_log_extend tlogext with "Htlog HtlogX")
+      as "[Htlog HtlogX]".
+    assert (Hcsincl' : txn_cpool_subsume_log tcpool (tlog ++ tlogext)).
     { rewrite /txn_cpool_subsume_log Forall_forall.
-      intros x Hx.
-      rewrite Forall2_lookup in Hext.
-      apply elem_of_list_lookup in Hx as [i Hx].
-      specialize (Hext i).
-      rewrite Hx in Hext.
-      destruct (plogext !! i) as [y |]; last inv Hext.
-      inv Hext.
-      by destruct H1 as [? _].
+      intros c Hc.
+      apply elem_of_app in Hc.
+      destruct Hc as [Hintlog | Hinext]; last first.
+      { apply elem_of_list_lookup in Hinext as [i Hc].
+        by pose proof (Forall2_lookup_r _ _ _ _ _ Hext Hc) as (x & _ & ? & _).
+      }
+      rewrite /txn_cpool_subsume_log Forall_forall in Hcsincl.
+      by apply Hcsincl.
     }
     (* Apply the view shift. *)
-    iMod ("HAU" with "HtlogX") as "HΦ".
+    iMod ("HAU" with "[$HtlogX $HtcpoolX]") as "HΦ".
+    { done. }
     (* Re-establish the txnlog invariant. *)
     set tlog' := tlog ++ tlogext.
     assert (Hlogabs' : Forall2 (λ tc pc, encode_ccommand tc pc) tlog' plog').
@@ -98,6 +99,7 @@ Section program.
     iMod ("HinvC" with "[-HΦ]") as "_".
     { iFrame.
       iPureIntro.
+      split; first apply Hcsincl'.
       split; [apply Hlogabs' | apply Hcpoolabs].
     }
     iModIntro.
@@ -235,6 +237,11 @@ Section program.
     iMod ("HinvC" with "[-HΦ]") as "_".
     { iFrame.
       iPureIntro.
+      split.
+      { rewrite /txn_cpool_subsume_log.
+        apply (Forall_impl _ _ _ Hcsincl).
+        set_solver.
+      }
       split; first done.
       apply set_Forall_union; last first.
       { apply (set_Forall_impl _ _ _ Hcpoolabs).
@@ -315,6 +322,11 @@ Section program.
     iMod ("HinvC" with "[-HΦ]") as "_".
     { iFrame.
       iPureIntro.
+      split.
+      { rewrite /txn_cpool_subsume_log.
+        apply (Forall_impl _ _ _ Hcsincl).
+        set_solver.
+      }
       split; first done.
       apply set_Forall_union; last first.
       { apply (set_Forall_impl _ _ _ Hcpoolabs).