qed much better logical history structure, which allows for easy hist…

…ory -> msv proof

external/Goose/github_com/mit_pdos/pav/kt.v

@@ -1941,11 +1941,11 @@ Definition testAll: val :=
     updAdtrsAll (struct.loadF setupParams "servAddr" "setup") (struct.loadF setupParams "adtrAddrs" "setup");;
     doAudits (struct.loadF alice "cli" "alice") (struct.loadF setupParams "adtrAddrs" "setup") (struct.loadF setupParams "adtrPks" "setup");;
     doAudits (struct.loadF bob "cli" "bob") (struct.loadF setupParams "adtrAddrs" "setup") (struct.loadF setupParams "adtrPks" "setup");;
-    let: ("isReg", "aliceKey") := GetHist (struct.loadF alice "hist" "alice") (struct.loadF bob "epoch" "bob") in
+    let: ("isReg", "alicePk") := GetHist (struct.loadF alice "hist" "alice") (struct.loadF bob "epoch" "bob") in
     control.impl.Assert ("isReg" = (struct.loadF bob "isReg" "bob"));;
     (if: "isReg"
     then
-      control.impl.Assert (std.BytesEqual "aliceKey" (struct.loadF bob "alicePk" "bob"));;
+      control.impl.Assert (std.BytesEqual "alicePk" (struct.loadF bob "alicePk" "bob"));;
       #()
     else #()).
 

src/program_proof/pav/core.v

@@ -47,6 +47,7 @@ Section msv.
 (* maximum sequence of versions. *)
 
 Definition msv_aux (m : fake_map_ty) uid vals :=
+  (* TODO: change to know elem exists there. *)
   (∀ i, i < length vals → m !! (uid, i) = vals !! i).
 
 Definition msv m uid vals :=
@@ -123,9 +124,9 @@ Qed.
 
 End msv.
 
-Section ts_msv.
+Section hist_msv.
 
-(* timeseries and its interaction with msv. *)
+(* history and its interaction with msv. *)
 
 Definition lower_adtr (m : map_adtr_ty) : merkle_map_ty :=
   (λ v, MapValPre.encodesF (MapValPre.mk v.1 v.2)) <$> m.
@@ -149,81 +150,60 @@ Definition maps_epoch_ok (ms : list map_adtr_ty) :=
 
 Definition adtr_inv ms := maps_mono (lower_adtr <$> ms) ∧ maps_epoch_ok ms.
 
-Record ts_ty :=
-  mk_ts {
-    entries: list (fake_epoch_ty * pk_ty);
-    bound: fake_epoch_ty;
-  }.
-
-(* ts_get fetches the seq of pk's through this ep. *)
-Definition ts_get ts ep := filter (λ x, x.1 ≤ ep) ts.(entries).
+(* tmp duplicate adtr invs that use the same map type as below. *)
+Definition maps_mono' (ms : list fake_map_ty) :=
+  ∀ i j mi mj,
+  ms !! i = Some mi →
+  ms !! j = Some mj →
+  i ≤ j →
+  mi ⊆ mj.
 
-Definition ts_epoch_mono (ts : ts_ty) :=
-  ∀ i j ep_i pk_i ep_j pk_j,
-  ts.(entries) !! i = Some (ep_i, pk_i) →
-  ts.(entries) !! j = Some (ep_j, pk_j) →
-  i < j →
-  ep_i < ep_j.
+Definition maps_epoch_ok' (ms : list fake_map_ty) :=
+  ∃ ep m_ep uid ver ep' val,
+  ms !! ep = Some m_ep →
+  m_ep !! (uid, ver) = Some (ep', val) →
+  ep' ≤ ep.
+
+Definition adtr_inv' ms := maps_mono' ms ∧ maps_epoch_ok' ms.
+
+Record hist_entry_ty :=
+  mk_hist_entry {
+    (* TODO: make msv only talk about latest val at some version.
+    this seems to more naturally capture what people care abt with KT.
+    and it'd allow us to only make visible the latest val and version here.
+    do this by proving new msv on top of old one. *)
+    vals: list (nat * list w8);
+  }.
 
-Definition ts_bound_ok0 (ts : ts_ty) :=
-  ∀ i ep pk,
-  ts.(entries) !! i = Some (ep, pk) →
-  ep ≤ ts.(bound).
+Definition know_entry (uid : w64) (ep : nat) (entry : hist_entry_ty) (ms : list fake_map_ty) :=
+  (* vals exist in prior maps. *)
+  (∀ ver val, entry.(vals) !! ver = Some val →
+    (∃ prior m, prior ≤ ep ∧ ms !! prior = Some m ∧ m !! (uid, ver) = Some val)) ∧
+  (* next ver doesn't exist in some future map. *)
+  (∃ bound m, bound ≥ ep ∧ ms !! bound = Some m ∧ m !! (uid, length entry.(vals)) = None).
 
-Definition ts_bound_ok1 (ts : ts_ty) (ms : list fake_map_ty) :=
-  ts.(bound) < length ms.
+Definition know_hist (uid : w64) (hist : list hist_entry_ty) (ms : list fake_map_ty) :=
+  (∀ ep entry, hist !! ep = Some entry → know_entry uid ep entry ms).
 
-Definition ts_entry_know (ts : ts_ty) (ms : list fake_map_ty) uid :=
-  ∀ ver ep pk m,
-  ts.(entries) !! ver = Some (ep, pk) →
+Lemma hist_msv ms uid hist ep m entry :
+  adtr_inv' ms →
+  know_hist uid hist ms →
+  hist !! ep = Some entry →
   ms !! ep = Some m →
-  m !! (uid, ver) = Some (ep, pk) ∧ m !! (uid, S ver) = None.
-
-Definition ts_bound_know (ts : ts_ty) (ms : list fake_map_ty) uid :=
-  ∀ m,
-  ms !! ts.(bound) = Some m →
-  m !! (uid, length ts.(entries)) = None.
-
-(* maintained by client. *)
-Definition ts_inv ts ms uid :=
-  ts_epoch_mono ts ∧
-  ts_bound_ok0 ts ∧
-  ts_bound_ok1 ts ms ∧
-  ts_entry_know ts ms uid ∧
-  ts_bound_know ts ms uid.
-
-  (*
-Lemma ts_interp ts ms uid ep m :
-  ts_inv ts ms uid →
-  adtr_inv ms →
-  ms !! ep = Some m →
-  ep ≤ ts.(bound) →
-  msv m uid (ts_get ts ep).
+  msv m uid entry.(vals).
 Proof.
-  intros Hts Hadtr Hm_look Hbound. split.
-  (* ver memb. should come all from the ts_get entries. *)
-  - admit.
-  (* ver non-memb. the next ver is either in the TS or in the bound. *)
-  - destruct (decide (filter (λ x, ep < x.1) ts.(entries) = [])) as [Hbig|Hbig].
-    (* in the bound. *)
-    + destruct Hts as (_&_&Hok&_&Hknow).
-      list_elem ms (bound ts) as m_bnd; [done|].
-      ospecialize (Hknow m_bnd Hm_bnd_lookup).
-      assert (length (ts_get ts ep) = length (ts.(entries))) as ->.
-      { pose proof (filter_app_complement (λ x, ep < x.1) ts.(entries)) as H.
-        rewrite Hbig in H. list_simplifier. apply Permutation_length in H.
-        rewrite (list_filter_iff _ (λ x, x.1 ≤ ep)) in H; [done|lia]. }
-      destruct Hadtr as (Hmono&_).
-      ospecialize (Hmono _ _ _ _ Hm_look Hm_bnd_lookup Hbound).
-      by eapply lookup_weaken_None.
-    (* in the TS. *)
-    + eapply (proj2 (head_is_Some _)) in Hbig as [xlt Hbig].
-      destruct Hts as (_&_&_&Hent&_).
-      (* prove that next ver is head of remaining TS. *)
-      admit.
-  (* TODO: maybe better approach is defining ts_get as a recursive prefix,
-  then proving (with ts_inv) that it satisfies the list_filter prop. *)
-Admitted.
-  *)
-
-End ts_msv.
+  intros Hadtr Hhist Hlook_entry Hlook_m. split.
+  - intros ver Hlook_ver.
+    specialize (Hhist _ _ Hlook_entry) as [Hhist _].
+    list_elem entry.(vals) ver as val.
+    specialize (Hhist _ _ Hval_lookup) as (?&?&?&Hlook_prior&Hlook_mprior).
+    opose proof ((proj1 Hadtr) _ _ _ _ Hlook_prior Hlook_m _); [lia|].
+    rewrite Hval_lookup.
+    by eapply lookup_weaken.
+  - specialize (Hhist _ _ Hlook_entry).
+    destruct Hhist as [_ (bound&mbound&Hlt_bound&Hlook_bound&Hlook_mbound)].
+    opose proof ((proj1 Hadtr) _ _ _ _ Hlook_m Hlook_bound _); [lia|].
+    by eapply lookup_weaken_None.
+Qed.
+
+End hist_msv.

src/program_proof/pav/history.v

@@ -16,3 +16,48 @@ Definition own (ptr : loc) (obj : t) : iProp Σ :=
   "#Hsl_HistVal" ∷ own_slice_small sl_HistVal byteT DfracDiscarded obj.(HistVal).
 End defs.
 End HistEntry.
+
+(* logical history. this may be the same as the physical history.
+but lets leave it abstract for now, so we can fill in details later
+once we know the use case. *)
+Module hist.
+Definition t : Type. Admitted.
+(* TODO: the core invariant about the logical history. *)
+Definition inv (obj : t) : Prop. Admitted.
+(* relation bw physical and logical st.  *)
+Definition phys_relate (obj : t) (hist : list HistEntry.t) : Prop. Admitted.
+End hist.
+
+Section defs.
+Context `{!heapGS Σ}.
+Definition own_hist sl_hist (hist : list HistEntry.t) : iProp Σ :=
+  ∃ dim0_hist,
+  "Hsl_hist" ∷ own_slice sl_hist ptrT (DfracOwn 1) dim0_hist ∗
+  "Hdim0_hist" ∷ ([∗ list] p;o ∈ dim0_hist;hist, HistEntry.own p o) ∗
+  "Hrelate" ∷ hist.phys_relate log_hist hist ∗
+  "Hhist_inv" ∷ inv hist.
+End defs.
+
+Section wps.
+Context `{!heapGS Σ}.
+Lemma wp_GetHist sl_hist hist (epoch : w64) :
+  {{{
+    "Hown_hist" ∷ own_hist sl_hist hist
+  }}}
+  GetHist (slice_val sl_hist) #epoch
+  {{{
+    (is_reg : bool) sl_lat_val (lat_val : list w8), RET (#is_reg, slice_val sl_lat_val);
+    (* could directly say that lat_val is an element in the hist that corresponds to the max epoch
+    less than the one queried. *)
+    (* or, could say that the output matches whatever is returned by some logical object.
+    ultimately, it's prob easier to reason about the logical object with other things,
+    e.g., msv's, so let's have the output match that. *)
+    (* secondly, what logical state do we wanna use?
+    before, i explicitly made the logical object basically the same thing.
+    and i made the get fn something.
+    can i be more abstract here?
+    there exists some logical object, and this thing is tied into it.
+    and that object has a get fn.
+    *)
+  }}}.
+End wps.

src/program_proof/pav/test.v

@@ -152,10 +152,27 @@ Proof using Type*.
   iRename "Hptr_cli_al" into "Hptr0". iRename "Hptr_cli_bob" into "Hptr1".
   iDestruct "H0" as (?) "H0". iNamed "H0". iNamedSuffix "Hown_al" "_al".
   iDestruct "H1" as (?) "H1". iNamed "H1". iNamedSuffix "Hown_bob" "_bob".
-  Search struct_field_pointsto.
   iDestruct (struct_field_pointsto_agree with "Hptr0 Hptr_cli_al") as %->.
   iDestruct (struct_field_pointsto_agree with "Hptr1 Hptr_cli_bob") as %->.
   iClear "His_wg Hptr0 Hptr1".
+
+  wp_loadField. wp_apply (wp_Client__SelfMon with "Hown_cli_al").
+  iIntros (selfMonEp ? err) "H /=". iNamedSuffix "H" "_al".
+  wp_loadField. iClear "Herr_al".
+  destruct err.(clientErr.err). { wp_apply wp_Assume_false. }
+  wp_apply wp_Assume. iIntros "_ /=". iNamedSuffix "H" "_al".
+  wp_loadField. wp_apply wp_Assume. iIntros "%Hlt_ep".
+  do 2 wp_loadField. wp_apply (wp_updAdtrsAll with "Hsl_adtrAddrs").
+  do 3 wp_loadField.
+  iDestruct (big_sepL2_length with "Hdim0_adtrPks") as %Hlen0.
+  wp_apply (wp_doAudits with "[$Hown_cli_al $Hsl_adtrAddrs $Hsl_adtrPks $Hdim0_adtrPks]").
+  { iPureIntro. lia. }
+  iNamedSuffix 1 "_al". do 3 wp_loadField.
+  wp_apply (wp_doAudits with "[$Hown_cli_bob $Hsl_adtrAddrs $Hsl_adtrPks $Hdim0_adtrPks]").
+  { iPureIntro. lia. }
+  iNamedSuffix 1 "_bob". do 2 wp_loadField.
+
+
 Admitted.
 
 End proof.