From ca87c208b48b1223f1b7c24130162d3b0d9b9494 Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jt4767@nyu.edu>
Date: Sun, 8 Dec 2024 18:23:17 -0500
Subject: [PATCH] Finish tulip basic resolve prophecy triples

---
 src/program_proof/tulip/program/txn/proph.v | 24 +++++++++++++++++----
 src/program_proof/tulip/res_txnsys.v        | 15 +++++++++++++
 2 files changed, 35 insertions(+), 4 deletions(-)

diff --git a/src/program_proof/tulip/program/txn/proph.v b/src/program_proof/tulip/program/txn/proph.v
index 7f1bd9c22..c9b1769ed 100644
--- a/src/program_proof/tulip/program/txn/proph.v
+++ b/src/program_proof/tulip/program/txn/proph.v
@@ -49,6 +49,21 @@ Section proph.
     iModIntro. by iApply "HΦ".
   Qed.
 
+  Lemma decode_dbmap_map_val mv (wrs : dbmap) :
+    map.map_val mv = Some (Map.untype wrs) →
+    decode_dbmap mv = wrs.
+  Proof.
+    rewrite /decode_dbmap => ->.
+    rewrite /Map.untype.
+    rewrite -map_fmap_compose.
+    apply map_leibniz.
+    intros k.
+    rewrite ?lookup_fmap.
+    destruct (wrs !! k) as [v|] eqn:Heq; rewrite Heq //=.
+    rewrite /to_dbstring/dbval_to_val.
+    destruct v => //=.
+  Qed.
+
   Lemma wp_ResolveCommit
     p (tid : u64) (ts : nat) (wrsP : loc) q (wrs : dbmap) :
     ⊢
@@ -74,12 +89,13 @@ Section proph.
     iMod ("Hclose" with "[Hp]") as "HΦ".
     { iExists (decode_actions pvs').
       rewrite Hts in Hpvs.
-      iSplit.
-      { admit. (* todo: bad definition of decode dbmap *) }
-      iExists _. by iFrame. }
+      rewrite (decode_dbmap_map_val mv wrs) // in Hpvs.
+      iSplit; first by naive_solver.
+      iExists _. by iFrame.
+    }
     iModIntro. iApply "HΦ".
     iFrame "Hmref".
     eauto.
-  Admitted.
+  Qed.
 
 End proph.
diff --git a/src/program_proof/tulip/res_txnsys.v b/src/program_proof/tulip/res_txnsys.v
index 7b1e818d6..75214d6e7 100644
--- a/src/program_proof/tulip/res_txnsys.v
+++ b/src/program_proof/tulip/res_txnsys.v
@@ -637,12 +637,27 @@ Section res.
     Definition to_dbval (b : bool) (v : string) :=
       if b then Some v else None.
 
+    Definition to_dbstring (v : val) : option string :=
+      match v with
+      | (#true, (#(LitString key), _))%V => Some key
+      | (#false, (#(LitString key), _))%V => None
+      | _ => None
+      end.
+
+    Definition decode_dbmap (v: val) : dbmap :=
+      match @map.map_val _ dbkey (@string_IntoVal grove_op) String.eq_dec String.countable v with
+      | None => ∅
+      | Some (mv, _) => to_dbstring <$> mv
+      end.
+
+    (*
     Fixpoint decode_dbmap (v : val) : dbmap :=
       match v with
       | (#(LitString key), #(LitBool present), #(LitString str'), tail)%V =>
           <[key:=to_dbval present str']> (decode_dbmap tail)
       | _ => ∅
       end.
+     *)
 
     Local Definition decode_ev_read (v : val) : option action :=
       match v with