Simplify auditor specs

mit-pdos · Oct 24, 2024 · 87cf534 · 87cf534
1 parent 8eb2ccc
commit 87cf534
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 28 deletions.
diff --git a/src/program_proof/pav/auditor.v b/src/program_proof/pav/auditor.v
@@ -31,27 +31,17 @@ Definition adtr_sigpred γ : (list w8 → iProp Σ) :=
 End inv.
 
 Module Auditor.
-Record t :=
-  mk {
-    mu: loc;
-    γ: gname;
-    serv_γ: gname;
-    sl_sk: Slice.t;
-    serv_pk: list w8;
-  }.
 
 Section defs.
 Context `{!heapGS Σ, !pavG Σ}.
-Definition own (ptr : loc) (obj : t) : iProp Σ :=
-  ∃ pk sl_serv_pk key_maps ptr_map last_map sl_hist ptrs_hist hist,
+(* This representation predicate existentially hides the state of the auditor. *)
+Definition own (ptr : loc) : iProp Σ :=
+  ∃ γ pk key_maps ptr_map last_map sl_sk sl_hist ptrs_hist hist,
   (* keys. *)
-  "#Hptr_sk" ∷ ptr ↦[Auditor :: "sk"]□ (slice_val obj.(sl_sk)) ∗
-  "Hown_sk" ∷ own_sk obj.(sl_sk) pk (adtr_sigpred obj.(γ)) ∗
-  "#Hptr_servPk" ∷ ptr ↦[Auditor :: "servSigPk"]□ (slice_val sl_serv_pk) ∗
-  "#Hsl_servPk" ∷ own_slice_small sl_serv_pk byteT DfracDiscarded obj.(serv_pk) ∗
-  "#His_servPk" ∷ is_pk obj.(serv_pk) (serv_sigpred obj.(serv_γ)) ∗
+  "#Hptr_sk" ∷ ptr ↦[Auditor :: "sk"]□ (slice_val sl_sk) ∗
+  "Hown_sk" ∷ own_sk sl_sk pk (adtr_sigpred γ) ∗
   (* maps. *)
-  "Hmaps" ∷ mono_list_auth_own obj.(γ) 1 key_maps ∗
+  "Hmaps" ∷ mono_list_auth_own γ 1 key_maps ∗
   "%Hinv" ∷ ⌜ adtr_inv key_maps ⌝ ∗
   (* merkle tree. *)
   "Hown_map" ∷ own_merkle ptr_map (lower_adtr last_map) ∗
@@ -65,24 +55,27 @@ Definition own (ptr : loc) (obj : t) : iProp Σ :=
   "#Hdigs_hist" ∷ ([∗ list] m;info ∈ key_maps;hist,
     is_dig (lower_adtr m) info.(AdtrEpochInfo.Dig)).
 
-Definition valid (ptr : loc) (obj : t) : iProp Σ :=
-  "#Hptr_mu" ∷ ptr ↦[Auditor :: "mu"]□ #obj.(mu) ∗
-  "#HmuR" ∷ is_lock nroot #obj.(mu) (own ptr obj).
+Definition valid (ptr : loc) : iProp Σ :=
+  ∃ (mu : loc),
+  "#Hptr_mu" ∷ ptr ↦[Auditor :: "mu"]□ #mu ∗
+  "#HmuR" ∷ is_lock nroot #mu (own ptr).
 End defs.
 End Auditor.
 
 Section specs.
 Context `{!heapGS Σ, !pavG Σ}.
-Lemma wp_newAuditor sl_servPk (servPk : list w8) :
+
+Lemma wp_newAuditor :
   {{{
-    "#Hsl_servPk" ∷ own_slice_small sl_servPk byteT DfracDiscarded servPk
+        True
   }}}
-  newAuditor (slice_val sl_servPk)
+  newAuditor #()
   {{{
-    ptr_adtr (adtr : Auditor.t) sl_adtrPk adtrPk adtr_γ, RET (#ptr_adtr, slice_val sl_adtrPk);
-    "Hown_adtr" ∷ Auditor.own ptr_adtr adtr ∗
+    ptr_adtr sl_adtrPk adtrPk adtr_γ, RET (#ptr_adtr, slice_val sl_adtrPk);
+    "Hvalid_adtr" ∷ Auditor.valid ptr_adtr ∗
     "#Hsl_adtrPk" ∷ own_slice_small sl_adtrPk byteT DfracDiscarded adtrPk ∗
     "#His_adtrPk" ∷ is_pk adtrPk (adtr_sigpred adtr_γ)
   }}}.
 Proof. Admitted.
+
 End specs.
diff --git a/src/program_proof/pav/basictest.v b/src/program_proof/pav/basictest.v
@@ -77,8 +77,8 @@ Proof.
     "%Hlen_adtrPks" ∷ ⌜ length doneV = length dim0_adtrPks ⌝)%I
     with "[] [$Hsl_adtrAddrs Hptr_adtrPks]").
   { clear. iIntros "* _". iIntros (Φ) "!>". iIntros "(%&%&%&H) HΦ". iNamed "H".
-    wp_apply (wp_newAuditor with "Hsl_sigPk"). iIntros "*". iNamed 1.
-    wp_apply (wp_newRpcAuditor with "[$Hown_adtr]"). iIntros "*". iNamed 1.
+    wp_apply wp_newAuditor. iIntros "*". iNamed 1.
+    wp_apply (wp_newRpcAuditor with "[$Hvalid_adtr]"). iIntros "*". iNamed 1.
     wp_apply (wp_Server__Serve with "Hown_rpcserv").
     wp_load. wp_apply (wp_SliceAppend with "Hsl_adtrPks"). iIntros "* Hsl_adtrPks".
     wp_store. iApply "HΦ". iFrame.

diff --git a/src/program_proof/pav/rpc.v b/src/program_proof/pav/rpc.v
@@ -16,9 +16,9 @@ Lemma wp_newRpcServer ptr_serv serv :
   }}}.
 Proof. Admitted.
 
-Lemma wp_newRpcAuditor ptr_adtr adtr :
+Lemma wp_newRpcAuditor ptr_adtr :
   {{{
-    "Hown_adtr" ∷ Auditor.own ptr_adtr adtr
+    "Hown_adtr" ∷ Auditor.valid ptr_adtr
   }}}
   newRpcAuditor #ptr_adtr
   {{{