qed hist_extend_put

src/Helpers/List.v

@@ -9,7 +9,15 @@ Section list.
   Notation list := (list A).
   Implicit Types l : list.
 
-  (* TODO: upstream. *)
+  Lemma list_filter_singleton (P : A → Prop)
+      `{!∀ x, Decision (P x)} x :
+    (filter P [x] = [] ∧ ¬ P x) ∨ (filter P [x] = [x] ∧ P x).
+  Proof.
+    destruct (decide $ P x).
+    - right. split; [|done]. rewrite filter_cons_True; [naive_solver|done].
+    - left. split; [|done]. rewrite filter_cons_False; [naive_solver|done].
+  Qed.
+
   Lemma list_filter_iff_strong (P1 P2 : A → Prop)
       `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} l :
     (∀ i x, l !! i = Some x → (P1 x ↔ P2 x)) →
@@ -23,7 +31,6 @@ Section list.
     - rewrite !filter_cons_False; [by naive_solver..|]. by rewrite IH.
   Qed.
 
-  (* TODO: upstream. *)
   Lemma list_filter_all (P : A → Prop)
       `{!∀ x, Decision (P x)} l :
     (∀ i x, l !! i = Some x → P x) →
@@ -35,10 +42,12 @@ Section list.
     rewrite filter_cons_True; [done|]. by rewrite IH.
   Qed.
 
-  (* TODO: upstream. *)
   Lemma lookup_snoc l x :
     (l ++ [x]) !! (length l) = Some x.
-  Proof. by opose proof (proj2 (lookup_snoc_Some _ _ (length l) x) _) as ?; [naive_solver|]. Qed.
+  Proof.
+    opose proof (proj2 (lookup_snoc_Some _ _ (length l) x) _) as ?;
+      [naive_solver|done].
+  Qed.
 
   Lemma list_singleton_exists l :
     length l = 1 →

src/program_proof/pav/client.v

@@ -83,9 +83,9 @@ Definition is_my_key cli_γ uid ver ep pk : iProp Σ :=
   ∃ dig sm_γ comm label0 label1,
   "#Hsubmap" ∷ mono_list_idx_own cli_γ (uint.nat ep) (Some (dig, sm_γ)) ∗
   "#Hcomm" ∷ is_comm pk comm ∗
-  "#Hlatest" ∷ (uid, ver) ↪[sm_γ]□ (Some (ep, comm)) ∗
+  "#Hin_map_lat" ∷ (uid, ver) ↪[sm_γ]□ (Some (ep, comm)) ∗
   "#His_label0" ∷ is_vrf uid ver label0 ∗
-  "#Hbound" ∷ (uid, word.add (W64 1) ver) ↪[sm_γ]□ None ∗
+  "#Hnin_map_next" ∷ (uid, word.add (W64 1) ver) ↪[sm_γ]□ None ∗
   "#His_label1" ∷ is_vrf uid (word.add (W64 1) ver) label1.
 
 Lemma wp_Client__Put ptr_c c sl_pk d0 (pk : list w8) :
@@ -114,7 +114,7 @@ Proof. Admitted.
 Definition is_my_bound cli_γ uid ver (ep : w64) : iProp Σ :=
   ∃ dig sm_γ label,
   "#Hsubmap" ∷ mono_list_idx_own cli_γ (uint.nat ep) (Some (dig, sm_γ)) ∗
-  "#Hbound" ∷ (uid, ver) ↪[sm_γ]□ None ∗
+  "#Hnin_map_next" ∷ (uid, ver) ↪[sm_γ]□ None ∗
   "#His_label" ∷ is_vrf uid ver label.
 
 Lemma wp_Client__SelfMon ptr_c c :
@@ -139,7 +139,7 @@ Proof. Admitted.
 Definition is_no_other_key cli_γ uid (ep : epoch_ty) : iProp Σ :=
   ∃ dig sm_γ label,
   "#Hsubmap" ∷ mono_list_idx_own cli_γ (uint.nat ep) (Some (dig, sm_γ)) ∗
-  "#Hbound" ∷ (uid, W64 0) ↪[sm_γ]□ None ∗
+  "#Hnin_map" ∷ (uid, W64 0) ↪[sm_γ]□ None ∗
   "#His_label" ∷ is_vrf uid (W64 0) label.
 
 Definition is_other_key cli_γ uid (ep : epoch_ty) pk : iProp Σ :=
@@ -154,7 +154,7 @@ Definition is_other_key cli_γ uid (ep : epoch_ty) pk : iProp Σ :=
   "#Hcomm" ∷ is_comm pk comm0 ∗
   "#Hlatest" ∷ (uid, ver) ↪[sm_γ]□ (Some (ep0, comm0)) ∗
   "#His_label0" ∷ is_vrf uid ver label0 ∗
-  "#Hbound" ∷ (uid, (word.add ver (W64 1))) ↪[sm_γ]□ None ∗
+  "#Hnin_map_next" ∷ (uid, (word.add ver (W64 1))) ↪[sm_γ]□ None ∗
   "#His_label1" ∷ is_vrf uid (word.add ver (W64 1)) label1.
 
 Lemma wp_Client__Get ptr_c c uid :

src/program_proof/pav/core.v

@@ -137,7 +137,7 @@ Proof.
   iDestruct (mono_list_idx_agree with "Hmap0 Hmap1") as %->. iClear "Hmap0 Hmap1".
   iDestruct (msv_core_agree _ _ vals vals0 with "[$Hmsv_core0 $Hmsv_core1]") as %->.
   destruct lat0 as [[??]|], lat1 as [[??]|], (last vals0) as [[??]|]; [|done..].
-  iNamedSuffix "Hcomm_reln0" "0". iNamedSuffix "Hcomm_reln1" "1".
+  iNamedSuffix "Hpk_comm_reln0" "0". iNamedSuffix "Hpk_comm_reln1" "1".
   iDestruct (is_comm_inj with "His_comm0 His_comm1") as %->. naive_solver.
 Qed.
 

src/program_proof/pav/history.v

@@ -8,7 +8,7 @@ Section hist.
 Context `{!heapGS Σ, !pavG Σ}.
 
 (* TODO: add inv that says every key in cli submap will have a vrf. *)
-Definition know_hist_val_cliG cli_γ (uid ep : w64) (hist : list map_val_ty) (valid : w64) : iProp Σ :=
+Definition is_hist_ep cli_γ (uid ep : w64) (hist : list map_val_ty) (valid : w64) : iProp Σ :=
   ∃ (vals : list opaque_map_val_ty),
   "#Hpk_comm_reln" ∷
     ([∗ list] pk_val;comm_val ∈ filter (λ x, uint.Z x.1 ≤ uint.Z ep) hist;vals,
@@ -35,10 +35,10 @@ Definition know_hist_val_cliG cli_γ (uid ep : w64) (hist : list map_val_ty) (va
     "%Hgt_bound" ∷ ⌜ uint.Z ep < uint.Z bound ⌝ ∗
     "#Hin_bound" ∷ (uid, W64 $ length vals) ↪[m_γ]□ Some (bound, comm)))).
 
-Definition know_hist_cliG cli_γ (uid : w64) (hist : list map_val_ty) (valid : w64) : iProp Σ :=
+Definition is_hist cli_γ (uid : w64) (hist : list map_val_ty) (valid : w64) : iProp Σ :=
   "%Hhist_valid" ∷ ([∗ list] x ∈ hist, ⌜ uint.Z x.1 ≤ uint.Z valid ⌝) ∗
-  "#Hknow_vals" ∷ (∀ (ep : w64), ⌜ uint.Z ep ≤ uint.Z valid ⌝ -∗
-    know_hist_val_cliG cli_γ uid ep hist valid).
+  "#Hknow_eps" ∷ (∀ (ep : w64), ⌜ uint.Z ep ≤ uint.Z valid ⌝ -∗
+    is_hist_ep cli_γ uid ep hist valid).
 
 End hist.
 
@@ -47,33 +47,33 @@ Context `{!heapGS Σ, !pavG Σ}.
 
 Lemma hist_val_extend_valid γ uid ep hist valid new_valid :
   uint.Z valid ≤ uint.Z new_valid →
-  know_hist_val_cliG γ uid ep hist valid -∗
-  know_hist_val_cliG γ uid ep hist new_valid.
+  is_hist_ep γ uid ep hist valid -∗
+  is_hist_ep γ uid ep hist new_valid.
 Proof.
   intros ?. iNamed 1. iNamed "Hbound". iExists vals. iFrame "#".
-  iDestruct "Hbound" as "[Hbound|Hbound]"; iNamed "Hbound"; iPureIntro; word.
+  iDestruct "Hbound" as "[H|H]"; iNamed "H"; iPureIntro; word.
 Qed.
 
 Lemma hist_extend_selfmon cli_γ uid hist valid new_valid :
   uint.Z valid ≤ uint.Z new_valid →
-  ("#Hknow_hist" ∷ know_hist_cliG cli_γ uid hist valid ∗
+  ("#His_hist" ∷ is_hist cli_γ uid hist valid ∗
   "#His_bound" ∷ is_my_bound cli_γ uid (W64 $ length hist) new_valid) -∗
-  "#Hknow_hist" ∷ know_hist_cliG cli_γ uid hist new_valid.
+  "#His_hist" ∷ is_hist cli_γ uid hist new_valid.
 Proof.
-  intros ?. iNamed 1. iNamed "Hknow_hist". iSplit.
+  intros ?. iNamed 1. iNamed "His_hist". iSplit.
   { iApply big_sepL_forall. iPureIntro. simpl. intros * Hlook.
     specialize (Hhist_valid _ _ Hlook). word. }
   iIntros (ep ?). destruct (decide (uint.Z ep ≤ uint.Z valid)).
-  { iSpecialize ("Hknow_vals" $! ep with "[]"). { iPureIntro. word. }
-    iApply (hist_val_extend_valid with "Hknow_vals"). word. }
-  iSpecialize ("Hknow_vals" $! valid with "[]"). { iPureIntro. lia. }
-  iNamed "Hknow_vals". iExists vals. iSplit; [|iSplit].
+  (* case 1: ep ≤ valid. *)
+  { iSpecialize ("Hknow_eps" $! ep with "[]"). { iPureIntro. word. }
+    iApply (hist_val_extend_valid with "Hknow_eps"). word. }
+  (* case 2: valid < ep ≤ new_valid. *)
+  iSpecialize ("Hknow_eps" $! valid with "[]"). { iPureIntro. lia. }
+  iNamed "Hknow_eps". iExists vals. iSplit; [|iSplit].
   - rewrite (list_filter_iff_strong
       (λ x, uint.Z x.1 ≤ uint.Z ep)
-      (λ x, uint.Z x.1 ≤ uint.Z valid) hist); last first.
-    { intros ?[??] Hlook. ospecialize (Hhist_valid _ _ Hlook).
-      naive_solver word. }
-    iFrame "#".
+      (λ x, uint.Z x.1 ≤ uint.Z valid) hist); [iFrame "#"|].
+    intros ?[??] Hlook. ospecialize (Hhist_valid _ _ Hlook). naive_solver word.
   - iFrame "#".
   - iClear "Hhist Hbound".
     iDestruct (big_sepL2_length with "Hpk_comm_reln") as %Hlen_vals.
@@ -82,21 +82,77 @@ Proof.
     iNamed "His_bound". rewrite Hlen_vals. by iFrame "#%".
 Qed.
 
+Lemma hist_extend_put cli_γ uid hist valid new_valid pk :
+  uint.Z valid < uint.Z new_valid →
+  ("#His_hist" ∷ is_hist cli_γ uid hist valid ∗
+  "#His_my_key" ∷ is_my_key cli_γ uid (W64 $ length hist) new_valid pk) -∗
+  "#His_hist" ∷ is_hist cli_γ uid (hist ++ [(new_valid, pk)]) new_valid.
+Proof.
+  intros ?. iNamed 1. iNamed "His_hist". iSplit.
+  { iApply big_sepL_forall. iPureIntro. simpl. intros * Hlook.
+    apply lookup_app_Some in Hlook as [Hlook|[_ Hlook]].
+    - specialize (Hhist_valid _ _ Hlook). word.
+    - apply list_lookup_singleton_Some in Hlook as [_ ?]. by simplify_eq/=. }
+  iIntros (ep ?). destruct (decide (uint.Z ep < uint.Z new_valid)).
+  - iEval (rewrite /is_hist_ep). rewrite filter_app.
+    opose proof (list_filter_singleton (λ x, uint.Z x.1 ≤ uint.Z ep)
+      (new_valid, pk)) as [[->_]|[_?]]. 2: { exfalso. simpl in *. word. }
+    list_simplifier. destruct (decide (uint.Z ep ≤ uint.Z valid)).
+    (* case 1: ep ≤ valid. *)
+    + iSpecialize ("Hknow_eps" $! ep with "[]"). { iPureIntro. word. }
+      iNamed "Hknow_eps". iExists (vals). iNamed "Hbound". iFrame "#".
+      iDestruct "Hbound" as "[H|H]"; iNamed "H"; iPureIntro; word.
+    (* case 2: valid < ep < new_valid. *)
+    + iSpecialize ("Hknow_eps" $! valid with "[//]").
+      iNamed "Hknow_eps". iExists (vals). iFrame "#". iSplit.
+      * rewrite (list_filter_iff_strong
+          (λ x, uint.Z x.1 ≤ uint.Z ep)
+          (λ x, uint.Z x.1 ≤ uint.Z valid) hist); [iFrame "#"|].
+        intros ?[??] Hlook. ospecialize (Hhist_valid _ _ Hlook). naive_solver word.
+      * iNamed "His_my_key". iFrame "#".
+        iDestruct (big_sepL2_length with "Hpk_comm_reln") as %Hlen_vals.
+        rewrite list_filter_all in Hlen_vals; last first.
+        { intros ?[??] Hlook. ospecialize (Hhist_valid _ _ Hlook).
+          simpl in *. word. }
+        rewrite Hlen_vals. iFrame "#". iSplit; [done|]. iRight. iPureIntro. word.
+  (* case 3: ep = new_valid. *)
+  - iSpecialize ("Hknow_eps" $! valid with "[//]").
+    iNamed "Hknow_eps". iNamed "His_my_key".
+    iDestruct (big_sepL2_length with "Hpk_comm_reln") as %Hlen_vals.
+    iExists (vals ++ [(new_valid, comm)]).
+    rewrite list_filter_all in Hlen_vals; last first.
+    { intros ?[??] Hlook. ospecialize (Hhist_valid _ _ Hlook). simpl in *. word. }
+    rewrite Hlen_vals. iSplit; [|iSplit].
+    + rewrite filter_app.
+      opose proof (list_filter_singleton (λ x, uint.Z x.1 ≤ uint.Z ep)
+        (new_valid, pk)) as [[_?]|[->_]]. { exfalso. simpl in *. word. }
+      iApply big_sepL2_snoc. iSplit.
+      * rewrite (list_filter_iff_strong
+          (λ x, uint.Z x.1 ≤ uint.Z ep)
+          (λ x, uint.Z x.1 ≤ uint.Z valid) hist); [iFrame "#"|].
+        intros ?[??] Hlook. ospecialize (Hhist_valid _ _ Hlook). naive_solver word.
+      * simpl in *. by iFrame "#".
+    + iApply big_sepL_snoc. iFrame "#".
+    + rewrite length_app. simpl.
+      replace (W64 (length vals + 1)%nat) with (word.add (W64 1) (W64 $ length vals)) by word.
+      iFrame "#". iSplit; [done|]. iLeft. iPureIntro. word.
+Qed.
+
 Definition get_lat (hist : list map_val_ty) (ep : w64) : lat_val_ty :=
   last $ filter (λ x, uint.Z x.1 ≤ uint.Z ep) hist.
 
 Lemma hist_audit_msv cli_γ uid hist valid adtr_γ aud_ep (ep : w64) :
   uint.Z ep ≤ uint.Z valid →
   uint.Z valid < uint.Z aud_ep →
-  ("#Hknow_hist" ∷ know_hist_cliG cli_γ uid hist valid ∗
+  ("#His_hist" ∷ is_hist cli_γ uid hist valid ∗
   "#His_audit" ∷ is_audit cli_γ adtr_γ aud_ep) -∗
   "#Hmsv" ∷ msv adtr_γ ep uid (get_lat hist ep).
 Proof.
   intros ??. iNamed 1.
-  iNamed "Hknow_hist". iSpecialize ("Hknow_vals" $! ep with "[//]").
+  iNamed "His_hist". iSpecialize ("Hknow_eps" $! ep with "[//]").
   iNamed "His_audit". list_elem ms (uint.nat ep) as m.
   iDestruct (mono_list_idx_own_get _ _ Hm_lookup with "Hadtr_maps") as "Hadtr_map".
-  iFrame "Hadtr_map". iNamed "Hknow_vals". iExists vals. iSplit.
+  iFrame "Hadtr_map". iNamed "Hknow_eps". iExists vals. iSplit.
   { iClear "Hhist Hbound".
     iDestruct (big_sepL2_length with "Hpk_comm_reln") as %Hlen_vals.
     destruct (get_lat hist ep) as [[??]|] eqn:Hlat_pk, (last vals) as [[??]|]
@@ -107,7 +163,9 @@ Proof.
       iFrame "#".
     + apply lookup_lt_Some in Hlat_pk. apply lookup_ge_None in Hlat_comm. lia.
     + apply lookup_ge_None in Hlat_pk. apply lookup_lt_Some in Hlat_comm. lia. }
-  iNamedSuffix "Hbound" "_bnd". iFrame "#". iSplit.
+  iNamedSuffix "Hbound" "_bnd". iFrame "#".
+  list_elem ms (uint.nat bound) as mbound.
+  iSplit; [|iClear "Hhist"; iDestruct "Hbound" as "[H|H]"; iNamed "H"].
   - iClear "Hbound". iApply (big_sepL_impl with "Hhist").
     iIntros (?[prior ?]) "!> %Hlook_vals". iNamed 1. iFrame "#".
     (* tedious: need prior ep < adtr_bound to get prior adtr map for map transf.
@@ -122,21 +180,19 @@ Proof.
     iNamed "H". iPureIntro.
     opose proof ((proj1 Hinv_adtr) _ _ _ _ Hmprior_lookup Hm_lookup _); [word|].
     by eapply lookup_weaken.
-  - iClear "Hhist". list_elem ms (uint.nat bound) as mbound.
-    iDestruct "Hbound" as "[Hbound|Hbound]"; iNamed "Hbound".
-    + iSpecialize ("Hmap_transf" with "[$Hsubmap_bnd $Hin_bound $His_label_bnd]").
-      { iPureIntro. exact Hmbound_lookup. }
-      iNamed "Hmap_transf". iPureIntro.
-      opose proof ((proj1 Hinv_adtr) _ _ _ _ Hm_lookup Hmbound_lookup _); [word|].
-      by eapply lookup_weaken_None.
-    + iSpecialize ("Hmap_transf" with "[$Hsubmap_bnd $Hin_bound $His_label_bnd]").
-      { iPureIntro. exact Hmbound_lookup. }
-      iNamed "Hmap_transf". iPureIntro.
-      destruct (decide $ is_Some $ m !! label) as [[? Hlook_mkey]|]; last first.
-      { by eapply eq_None_not_Some. }
-      opose proof ((proj1 Hinv_adtr) _ _ _ _ Hm_lookup Hmbound_lookup _); [word|].
-      opose proof (lookup_weaken _ _ _ _ Hlook_mkey _); [done|]. simplify_eq/=.
-      opose proof ((proj2 Hinv_adtr) _ _ _ _ _ Hm_lookup Hlook_mkey) as ?. word.
+  - iSpecialize ("Hmap_transf" with "[$Hsubmap_bnd $Hin_bound $His_label_bnd]").
+    { iPureIntro. exact Hmbound_lookup. }
+    iNamed "Hmap_transf". iPureIntro.
+    opose proof ((proj1 Hinv_adtr) _ _ _ _ Hm_lookup Hmbound_lookup _); [word|].
+    by eapply lookup_weaken_None.
+  - iSpecialize ("Hmap_transf" with "[$Hsubmap_bnd $Hin_bound $His_label_bnd]").
+    { iPureIntro. exact Hmbound_lookup. }
+    iNamed "Hmap_transf". iPureIntro.
+    destruct (decide $ is_Some $ m !! label) as [[? Hlook_mkey]|]; last first.
+    { by eapply eq_None_not_Some. }
+    opose proof ((proj1 Hinv_adtr) _ _ _ _ Hm_lookup Hmbound_lookup _); [word|].
+    opose proof (lookup_weaken _ _ _ _ Hlook_mkey _); [done|]. simplify_eq/=.
+    opose proof ((proj2 Hinv_adtr) _ _ _ _ _ Hm_lookup Hlook_mkey) as ?. word.
 Qed.
 
 End hist_derived.
@@ -154,7 +210,7 @@ Definition own_hist cli_γ uid sl_hist hist valid : iProp Σ :=
   ∃ dim0_hist,
   "Hsl_hist" ∷ own_slice sl_hist ptrT (DfracOwn 1) dim0_hist ∗
   "Hdim0_hist" ∷ ([∗ list] p;o ∈ dim0_hist;hist, own_HistEntry p o) ∗
-  "#Hknow_hist" ∷ know_hist_cliG cli_γ uid hist valid.
+  "#His_hist" ∷ is_hist cli_γ uid hist valid.
 
 Lemma wp_put_hist cli_γ uid sl_hist hist ptr_e e :
   match last hist with