Prove replica applier

external/Goose/github_com/mit_pdos/tulip/replica.v

@@ -35,15 +35,15 @@ Definition Replica := struct.decl [
 
    Return values:
    @terminated: Whether txn @ts has terminated (committed or aborted). *)
-Definition Replica__queryTxnTermination: val :=
-  rec: "Replica__queryTxnTermination" "rp" "ts" :=
+Definition Replica__terminated: val :=
+  rec: "Replica__terminated" "rp" "ts" :=
     let: (<>, "terminated") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
     "terminated".
 
 Definition Replica__QueryTxnTermination: val :=
   rec: "Replica__QueryTxnTermination" "rp" "ts" :=
     Mutex__Lock (struct.loadF Replica "mu" "rp");;
-    let: "terminated" := Replica__queryTxnTermination "rp" "ts" in
+    let: "terminated" := Replica__terminated "rp" "ts" in
     Mutex__Unlock (struct.loadF Replica "mu" "rp");;
     "terminated".
 
@@ -444,7 +444,7 @@ Definition Replica__release: val :=
 
 Definition Replica__applyCommit: val :=
   rec: "Replica__applyCommit" "rp" "ts" "pwrs" :=
-    let: "committed" := Replica__queryTxnTermination "rp" "ts" in
+    let: "committed" := Replica__terminated "rp" "ts" in
     (if: "committed"
     then #()
     else
@@ -460,7 +460,7 @@ Definition Replica__applyCommit: val :=
 
 Definition Replica__applyAbort: val :=
   rec: "Replica__applyAbort" "rp" "ts" :=
-    let: "aborted" := Replica__queryTxnTermination "rp" "ts" in
+    let: "aborted" := Replica__terminated "rp" "ts" in
     (if: "aborted"
     then #()
     else
@@ -475,24 +475,23 @@ Definition Replica__applyAbort: val :=
 
 Definition Replica__apply: val :=
   rec: "Replica__apply" "rp" "cmd" :=
-    (if: (struct.get txnlog.Cmd "Kind" "cmd") = #0
-    then #()
+    (if: (struct.get txnlog.Cmd "Kind" "cmd") = #1
+    then
+      Replica__applyCommit "rp" (struct.get txnlog.Cmd "Timestamp" "cmd") (struct.get txnlog.Cmd "PartialWrites" "cmd");;
+      #()
     else
-      (if: (struct.get txnlog.Cmd "Kind" "cmd") = #1
+      (if: (struct.get txnlog.Cmd "Kind" "cmd") = #2
       then
-        Replica__applyCommit "rp" (struct.get txnlog.Cmd "Timestamp" "cmd") (struct.get txnlog.Cmd "PartialWrites" "cmd");;
-        #()
-      else
         Replica__applyAbort "rp" (struct.get txnlog.Cmd "Timestamp" "cmd");;
-        #())).
+        #()
+      else #())).
 
 Definition Replica__Start: val :=
   rec: "Replica__Start" "rp" :=
     Mutex__Lock (struct.loadF Replica "mu" "rp");;
     Skip;;
     (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
-      let: "lsn" := std.SumAssumeNoOverflow (struct.loadF Replica "lsna" "rp") #1 in
-      let: ("cmd", "ok") := txnlog.TxnLog__Lookup (struct.loadF Replica "txnlog" "rp") "lsn" in
+      let: ("cmd", "ok") := txnlog.TxnLog__Lookup (struct.loadF Replica "txnlog" "rp") (struct.loadF Replica "lsna" "rp") in
       (if: (~ "ok")
       then
         Mutex__Unlock (struct.loadF Replica "mu" "rp");;
@@ -501,7 +500,7 @@ Definition Replica__Start: val :=
         Continue
       else
         Replica__apply "rp" "cmd";;
-        struct.storeF Replica "lsna" "rp" "lsn";;
+        struct.storeF Replica "lsna" "rp" (std.SumAssumeNoOverflow (struct.loadF Replica "lsna" "rp") #1);;
         Continue));;
     #().
 

src/program_proof/rsm/pure/list.v

@@ -171,4 +171,14 @@ Section lemma.
     (l ++ [x]) !! n = Some x.
   Proof. intros ->. apply lookup_snoc_length. Qed.
 
+  Lemma prefix_singleton l x :
+    l !! O = Some x ->
+    prefix [x] l.
+  Proof.
+    intros Hx.
+    destruct l as [| x' l']; first done.
+    inv Hx.
+    apply prefix_cons, prefix_nil.
+  Qed.
+
 End lemma.

src/program_proof/tulip/base.v

@@ -211,6 +211,12 @@ Definition valid_wrs (wrs : dbmap) := dom wrs ⊆ keys_all.
 
 Definition valid_key (key : dbkey) := key ∈ keys_all.
 
+Definition valid_ccommand gid (c : ccommand) :=
+  match c with
+  | CmdCommit ts pwrs => valid_ts ts ∧ valid_pwrs gid pwrs
+  | CmdAbort ts => valid_ts ts
+  end.
+
 Class tulip_ghostG (Σ : gFunctors).
 
 Record tulip_names := {}.

src/program_proof/tulip/cmd.v

@@ -265,13 +265,18 @@ Section apply_cmds.
 
   Definition not_stuck st := st ≠ Stuck.
 
+  Definition safe_extension (ts : nat) (pwrs : dbmap) (histm : gmap dbkey dbhist) :=
+    map_Forall (λ _ l, (length l ≤ ts)%nat) (filter (λ x, x.1 ∈ dom pwrs) histm).
+
   Definition apply_commit st (tid : nat) (pwrs : dbmap) :=
     match st with
-    | State cm hists =>
+    | State cm histm =>
         match cm !! tid with
         | Some true => st
         | Some false => Stuck
-        | _ => State (<[tid := true]> cm) (multiwrite tid pwrs hists)
+        | _ => if decide (safe_extension tid pwrs histm)
+              then State (<[tid := true]> cm) (multiwrite tid pwrs histm)
+              else Stuck
         end
     | Stuck => Stuck
     end.
@@ -341,7 +346,7 @@ Section apply_cmds.
     destruct x eqn:Hx; rewrite /apply_cmds foldl_snoc apply_cmds_unfold Hrsm1 /= in Hrsm.
     { (* Case [CmdCommit]. *)
       destruct (stm1 !! tid) as [st |]; last first.
-      { inv Hrsm. apply multiwrite_dom. }
+      { case_decide; last done. inv Hrsm. apply multiwrite_dom. }
       by destruct st; inv Hrsm.
     }
     { (* Case [CmdAbort]. *)

src/program_proof/tulip/inv_group.v

@@ -167,6 +167,19 @@ Section inv.
     ⌜valid_ts ts⌝.
   Proof. iIntros "Hsafe". by iDestruct "Hsafe" as (?) "(_ & ? & _ & _ & _)". Qed.
 
+  Lemma safe_txn_pwrs_impl_valid_wrs γ gid ts pwrs :
+    safe_txn_pwrs γ gid ts pwrs -∗
+    ⌜valid_wrs pwrs⌝.
+  Proof.
+    iIntros "Hsafe".
+    iDestruct "Hsafe" as (?) "(_ & _ & %Hvw & _ & %Hpwrs)".
+    iPureIntro.
+    rewrite Hpwrs.
+    rewrite /valid_wrs.
+    etrans; last apply Hvw.
+    apply subseteq_dom, map_filter_subseteq.
+  Qed.
+
   (** The [StAborted] branch says that a transaction is aborted globally if it
   is aborted locally on some group (the other direction is encoded in
   [safe_submit]). This gives contradiction when learning a commit command under
@@ -197,6 +210,7 @@ Section inv.
   Definition safe_commit γ gid ts pwrs : iProp Σ :=
     ∃ wrs, is_txn_committed γ ts wrs ∗
            is_txn_wrs γ ts wrs ∗
+           ⌜valid_ts ts⌝ ∗
            ⌜pwrs = wrs_group gid wrs⌝ ∗
            ⌜gid ∈ ptgroups (dom wrs)⌝ ∗
            ⌜valid_wrs wrs⌝.
@@ -375,6 +389,61 @@ Section lemma.
     apply Hprefixh.
   Qed.
 
+  Definition group_histm_lbs_from_log γ gid log : iProp Σ :=
+    match apply_cmds log with
+    | State _ histm => ([∗ map] k ↦ h ∈ filter_group gid histm, is_repl_hist_lb γ k h)
+    | _ => False
+    end.
+
+  #[global]
+  Instance group_histm_lbs_from_log_persistent γ gid log :
+    Persistent (group_histm_lbs_from_log γ gid log).
+  Proof. rewrite /group_histm_lbs_from_log. destruct (apply_cmds log); apply _. Defined.
+
+  Lemma group_inv_witness_group_histm_lbs_from_log {γ gid} loglb :
+    is_txn_log_lb γ gid loglb -∗
+    group_inv γ gid -∗
+    group_histm_lbs_from_log γ gid loglb.
+  Proof.
+    iIntros "#Hloglb Hgroup".
+    rewrite /group_histm_lbs_from_log.
+    destruct (apply_cmds loglb) as [cmlb histmlb |] eqn:Happly; last first.
+    { do 2 iNamed "Hgroup".
+      iDestruct (txn_log_prefix with "Hlog Hloglb") as %Hprefix.
+      unshelve epose proof (apply_cmds_not_stuck loglb _ Hprefix _) as Hns.
+      { by rewrite Hrsm. }
+      done.
+    }
+    iApply big_sepM_forall.
+    iIntros (k h Hh).
+    apply map_lookup_filter_Some in Hh as [Hh Hgid].
+    iApply (group_inv_witness_repl_hist with "Hloglb Hgroup").
+    { pose proof (apply_cmds_dom _ _ _ Happly) as Hdom.
+      apply elem_of_dom_2 in Hh.
+      set_solver.
+    }
+    { done. }
+    { by rewrite /hist_from_log Happly. }
+  Qed.
+
+  Lemma group_inv_impl_valid_ccommand_cpool {γ gid} cpool :
+    group_inv_no_cpool γ gid cpool -∗
+    ⌜set_Forall (valid_ccommand gid) cpool⌝.
+  Proof.
+    iIntros "Hgroup".
+    do 2 iNamed "Hgroup".
+    iIntros (c Hc).
+    iDestruct (big_sepS_elem_of with "Hsafecp") as "Hsafec"; first apply Hc.
+    destruct c; simpl.
+    { iDestruct "Hsafec" as (wrs) "(_ & _ & %Hvts & %Hwg & %Hgid & %Hvw)".
+      iPureIntro.
+      split; first done.
+      rewrite /valid_pwrs Hwg wrs_group_keys_group_dom.
+      set_solver.
+    }
+    { by iDestruct "Hsafec" as "[_ %Hvts]". }
+  Qed.
+
   Lemma group_inv_extract_log_expose_cpool {γ} gid :
     group_inv γ gid -∗
     ∃ log cpool,

src/program_proof/tulip/invariance/execute_commit.v

@@ -35,7 +35,7 @@ Section execute_commit.
         set_solver.
       }
       iDestruct (big_sepS_elem_of with "Hsafecp") as "Hsafec"; first apply Hin.
-      iDestruct "Hsafec" as (wrs) "(_ & Hwrs & %Hpwrs & %Hgid & %Hvwrs)".
+      iDestruct "Hsafec" as (wrs) "(_ & Hwrs & _ & %Hpwrs & %Hgid & %Hvwrs)".
       assert (Hdompwrs : dom pwrs ⊆ keys_all).
       { rewrite Hpwrs wrs_group_keys_group_dom. set_solver. }
       iFrame "Hwrs %".
@@ -110,6 +110,7 @@ Section execute_commit.
         rewrite Hvl.
         destruct (vl !! t) as [b |] eqn:Hvlt; last done.
         destruct b; last done.
+        clear Hns.
         case_decide as Ht; last done.
         destruct Ht as (Hgelen & Hnz).
         assert (is_Some (ptsm !! k)) as [pts Hpts].
@@ -186,6 +187,7 @@ Section execute_commit.
       rewrite (multiwrite_modified Hv Hh).
       destruct (vl !! t) as [b |] eqn:Hvlt; last done.
       destruct b; last done.
+      clear Hns.
       case_decide as Ht; last done.
       destruct Ht as [Hgelen Hnepts].
       iSpecialize ("Hgabt" $! k t).

src/program_proof/tulip/invariance/learn_commit.v

@@ -105,7 +105,7 @@ Section inv.
     (* Obtain proof that [ts] has committed. *)
     iDestruct (big_sepS_elem_of with "Hsafecp") as "Hc"; first apply Hc.
     simpl.
-    iDestruct "Hc" as (wrs) "(Hcmt & Hwrs & %Hpwrs & %Hgid)".
+    iDestruct "Hc" as (wrs) "(Hcmt & Hwrs & _ & %Hpwrs & %Hgid)".
     rewrite /group_inv_no_log_with_cpool.
     destruct (stm !! ts) as [st |] eqn:Hdup; last first.
     { (* Case: Empty state; contradiction---no prepare before commit. *) 
@@ -213,6 +213,27 @@ Section inv.
     iDestruct (keys_inv_committed with "Hcmt Hkeys Htxnsys") as "[Hkeys Htxnsys]".
     { apply Hdomhistmg. }
     { rewrite Hpwrs. apply map_filter_subseteq. }
+    (* Prove safe extension used later to re-establish the RSM invariant. *)
+    iAssert (⌜safe_extension ts pwrs hists⌝)%I as %Hsafeext.
+    { iIntros (k h Hh).
+      apply map_lookup_filter_Some in Hh as [Hh Hk]. simpl in Hk.
+      assert (Hhistmk : histm !! k = Some h).
+      { clear -Hinclhistmg Hdomhistmg Hh Hk.
+        rewrite -Hdomhistmg elem_of_dom in Hk.
+        destruct Hk as [h' Hh'].
+        unshelve epose proof (lookup_weaken_inv _ _ _ _ _ Hh' _ Hh) as ->.
+        { etrans; [apply Hinclhistmg | apply map_filter_subseteq]. }
+        done.
+      }
+      apply elem_of_dom in Hk as [v Hpwrsk].
+      iDestruct (big_sepM2_lookup with "Hkeys") as "Hkey".
+      { apply Hhistmk. }
+      { apply Hpwrsk. }
+      do 3 iNamed "Hkey".
+      iPureIntro.
+      rewrite /ext_by_cmtd Hv in Hdiffc.
+      by destruct Hdiffc as [_ ?].
+    }
     (* Re-establish keys invariant w.r.t. updated tuples. *)
     iDestruct (keys_inv_learn_commit with "Hkeys") as "Hkeys".
     (* Put ownership of tuples back to keys invariant. *)
@@ -251,7 +272,7 @@ Section inv.
     { iFrame "Hcmt". }
     iFrame "∗ # %".
     iPureIntro.
-    split; first done.
+    split; first by case_decide.
     split.
     { rewrite dom_insert_L.
       apply (map_Forall_impl _ _ _ Hpmstm).

src/program_proof/tulip/program/prelude.v

@@ -76,8 +76,8 @@ Defined.
 
 Definition ccommand_to_val (pwrsS : Slice.t) (c : ccommand) : val :=
   match c with
-  | CmdCommit ts _ => (#(U64 0), (#(U64 ts), (to_val pwrsS, (zero_val stringT, #()))))
-  | CmdAbort ts => (#(U64 1), (#(U64 ts), (Slice.nil, (zero_val stringT, #()))))
+  | CmdCommit ts _ => (#(U64 1), (#(U64 ts), (to_val pwrsS, (zero_val stringT, #()))))
+  | CmdAbort ts => (#(U64 2), (#(U64 ts), (Slice.nil, (zero_val stringT, #()))))
   end.
 
 Section def.