diff --git a/external/Goose/github_com/mit_pdos/pav/kt.v b/external/Goose/github_com/mit_pdos/pav/kt.v index 60b501fd5..c950b3e4a 100644 --- a/external/Goose/github_com/mit_pdos/pav/kt.v +++ b/external/Goose/github_com/mit_pdos/pav/kt.v @@ -43,35 +43,38 @@ Definition MapValPreDecode: val := "PkCommit" ::= "a2" ], "b2", #false))). -Definition Auditor__checkOneUpd: val := - rec: "Auditor__checkOneUpd" "a" "nextEpoch" "mapLabel" "mapVal" := - let: ((((<>, <>), "proofTy"), <>), "err0") := merkle.Tree__Get (struct.loadF Auditor "keyMap" "a") "mapLabel" in - (if: "err0" || "proofTy" +(* checkOneUpd from auditor.go *) + +(* checkOneUpd checks that an update is safe, and errs on fail. *) +Definition checkOneUpd: val := + rec: "checkOneUpd" "keys" "nextEp" "mapLabel" "mapVal" := + let: ((((<>, <>), "proofTy"), <>), "err0") := merkle.Tree__Get "keys" "mapLabel" in + (if: "err0" then #true else - let: (("valPre", <>), "err1") := MapValPreDecode "mapVal" in - (if: "err1" || ((struct.loadF MapValPre "Epoch" "valPre") ≠ "nextEpoch") + (if: "proofTy" then #true - else #false)). - -(* checkUpd checks that updates are okay to apply, and errors on fail. *) -Definition Auditor__checkUpd: val := - rec: "Auditor__checkUpd" "a" "upd" := - let: "nextEpoch" := slice.len (struct.loadF Auditor "histInfo" "a") in - let: "err0" := ref (zero_val boolT) in + else + let: (("valPre", "rem"), "err1") := MapValPreDecode "mapVal" in + (if: "err1" + then #true + else + (if: (slice.len "rem") ≠ #0 + then #true + else + (if: (struct.loadF MapValPre "Epoch" "valPre") ≠ "nextEp" + then #true + else #false))))). + +(* checkUpd just runs checkOneUpd for all updates. *) +Definition checkUpd: val := + rec: "checkUpd" "keys" "nextEp" "upd" := + let: "loopErr" := ref (zero_val boolT) in MapIter "upd" (λ: "mapLabel" "mapVal", - (if: Auditor__checkOneUpd "a" "nextEpoch" (StringToBytes "mapLabel") "mapVal" - then "err0" <-[boolT] #true + (if: checkOneUpd "keys" "nextEp" (StringToBytes "mapLabel") "mapVal" + then "loopErr" <-[boolT] #true else #()));; - ![boolT] "err0". - -(* applyUpd applies updates. *) -Definition Auditor__applyUpd: val := - rec: "Auditor__applyUpd" "a" "upd" := - MapIter "upd" (λ: "label" "val", - let: ((<>, <>), "err0") := merkle.Tree__Put (struct.loadF Auditor "keyMap" "a") (StringToBytes "label") "val" in - control.impl.Assert (~ "err0"));; - #(). + ![boolT] "loopErr". (* UpdateProof from serde.go *) @@ -80,6 +83,18 @@ Definition UpdateProof := struct.decl [ "Sig" :: slice.T byteT ]. +(* applyUpd from auditor.go *) + +(* applyUpd applies a valid update. *) +Definition applyUpd: val := + rec: "applyUpd" "keys" "upd" := + MapIter "upd" (λ: "label" "val", + let: ((<>, <>), "err0") := merkle.Tree__Put "keys" (StringToBytes "label") "val" in + control.impl.Assert (~ "err0"));; + #(). + +(* PreSigDig from serde.go *) + Definition PreSigDig := struct.decl [ "Epoch" :: uint64T; "Dig" :: slice.T byteT @@ -102,20 +117,20 @@ Definition AdtrEpochInfo := struct.decl [ "AdtrSig" :: slice.T byteT ]. -(* Update checks new epoch updates, applies them, and rets err on fail. *) +(* Update checks new epoch updates, applies them, and errors on fail. *) Definition Auditor__Update: val := rec: "Auditor__Update" "a" "proof" := Mutex__Lock (struct.loadF Auditor "mu" "a");; - let: "nextEpoch" := slice.len (struct.loadF Auditor "histInfo" "a") in - (if: Auditor__checkUpd "a" (struct.loadF UpdateProof "Updates" "proof") + let: "nextEp" := slice.len (struct.loadF Auditor "histInfo" "a") in + (if: checkUpd (struct.loadF Auditor "keyMap" "a") "nextEp" (struct.loadF UpdateProof "Updates" "proof") then Mutex__Unlock (struct.loadF Auditor "mu" "a");; #true else - Auditor__applyUpd "a" (struct.loadF UpdateProof "Updates" "proof");; + applyUpd (struct.loadF Auditor "keyMap" "a") (struct.loadF UpdateProof "Updates" "proof");; let: "dig" := merkle.Tree__Digest (struct.loadF Auditor "keyMap" "a") in let: "preSig" := struct.new PreSigDig [ - "Epoch" ::= "nextEpoch"; + "Epoch" ::= "nextEp"; "Dig" ::= "dig" ] in let: "preSigByt" := PreSigDigEncode (NewSlice byteT #0) "preSig" in @@ -129,8 +144,7 @@ Definition Auditor__Update: val := Mutex__Unlock (struct.loadF Auditor "mu" "a");; #false). -(* Get returns the auditor's known link for a particular epoch, - and errs on fail. *) +(* Get returns the auditor's dig for a particular epoch, and errors on fail. *) Definition Auditor__Get: val := rec: "Auditor__Get" "a" "epoch" := Mutex__Lock (struct.loadF Auditor "mu" "a");; diff --git a/src/program_proof/pav/auditor.v b/src/program_proof/pav/auditor.v index e4cb4c11e..ce09fe01a 100644 --- a/src/program_proof/pav/auditor.v +++ b/src/program_proof/pav/auditor.v @@ -2,6 +2,7 @@ From Perennial.program_proof Require Import grove_prelude. From Goose.github_com.mit_pdos.pav Require Import kt. From Perennial.program_proof.pav Require Import core cryptoffi merkle serde. +From Perennial.Helpers Require Import Map. Section gs. Context `{!heapGS Σ, !pavG Σ}. @@ -73,7 +74,7 @@ Context `{!heapGS Σ, !pavG Σ}. Lemma wp_NewAuditor : {{{ - True + True }}} NewAuditor #() {{{ @@ -108,71 +109,13 @@ Proof. by iApply own_slice_small_nil. Qed. -Lemma wp_Auditor__Update a ptr_upd upd : - {{{ - "#Hvalid" ∷ Auditor.valid a ∗ - "Hupdate" ∷ UpdateProof.own ptr_upd upd - }}} - Auditor__Update #a #ptr_upd - {{{ - (e : bool), RET #e; True - }}}. -Proof. - iIntros (?) "H HΦ". iNamed "H". - iNamed "Hvalid". - wp_rec. wp_pures. - wp_loadField. - wp_apply (wp_Mutex__Lock with "[$]"). - iIntros "[Hlock Hown]". - iNamed "Hown". - wp_pures. - wp_loadField. - wp_apply wp_slice_len. - wp_pures. - iNamed "Hupdate". - wp_loadField. - - (* XXX: checkUpd only gets called here. Inlining its proof. *) - wp_rec. - wp_pures. - wp_loadField. - wp_apply wp_slice_len. - wp_pures. - wp_apply wp_ref_of_zero. - { done. } - iIntros (?) "Hl". - wp_pures. - wp_apply (wp_MapIter_fold _ _ _ (λ _, - _ - )%I with "[$] [-HΦ]"). - { iNamedAccu. } - { - iIntros "* !# * [Hpre %Hlookup] HΦ". - iNamed "Hpre". - wp_pures. - wp_apply wp_StringToBytes. - iIntros "* ?". - iDestruct (own_slice_to_small with "[$]") as "?". - (* XXX: checkOneUpd only called here so inlining a proof. *) - wp_rec. - wp_pures. - wp_loadField. - wp_apply (wp_Tree_Get with "[$]"). - iIntros "* HGetPost". - iNamed "HGetPost". - (* iNamed "Hreply". *) - wp_pures. - admit. - } -Admitted. - Lemma wp_Auditor__Get a (epoch : u64) : {{{ - "#Hvalid" ∷ Auditor.valid a + "#Hvalid" ∷ Auditor.valid a }}} Auditor__Get #a #epoch {{{ - (b : bool) (p : loc) o, RET (#p, #b); AdtrEpochInfo.own p o + (b : bool) (p : loc) o, RET (#p, #b); AdtrEpochInfo.own p o }}}. Proof. iIntros (?) "H HΦ". iNamed "H". @@ -182,10 +125,8 @@ Proof. wp_apply (wp_Mutex__Lock with "[$]"). iIntros "[Hlock Hown]". iNamed "Hown". - wp_pures. wp_loadField. wp_apply wp_slice_len. - wp_pures. wp_if_destruct. - wp_loadField. wp_apply (wp_Mutex__Unlock with "[-HΦ]"). @@ -221,4 +162,155 @@ Proof. by iFrame "#". Qed. +Definition upd_checks (keys : adtr_map_ty) (nextEp : w64) (label val : list w8) := + ∃ comm, + length label = 32%nat ∧ + keys !! label = None ∧ + val = MapValPre.encodesF (MapValPre.mk nextEp comm). + +Lemma wp_checkOneUpd ptr_keys keys nextEp sl_label dq label sl_val val : + {{{ + "Hown_keys" ∷ own_merkle ptr_keys (lower_map keys) ∗ + "Hsl_label" ∷ own_slice_small sl_label byteT dq label ∗ + "#Hsl_val" ∷ own_slice_small sl_val byteT DfracDiscarded val + }}} + checkOneUpd #ptr_keys #nextEp (slice_val sl_label) (slice_val sl_val) + {{{ + (err : bool), RET #err; + "Hown_keys" ∷ own_merkle ptr_keys (lower_map keys) ∗ + "Hsl_label" ∷ own_slice_small sl_label byteT dq label ∗ + "Herr" ∷ (if err then True else ⌜ upd_checks keys nextEp label val ⌝) + }}}. +Proof. + iIntros (Φ) "H HΦ". iNamed "H". wp_rec. + wp_apply (wp_Tree__Get with "[$Hown_keys $Hsl_label]"). + iIntros "*". iNamedSuffix 1 "_map". + wp_if_destruct. { iApply "HΦ". by iFrame. } + wp_if_destruct. { iApply "HΦ". by iFrame. } + wp_apply (MapValPre.wp_dec with "[$Hsl_val]"). + iIntros "*". iNamedSuffix 1 "_val". + wp_if_destruct. { iApply "HΦ". by iFrame. } + wp_apply wp_slice_len. + wp_if_destruct. { iApply "HΦ". by iFrame. } + iDestruct ("Herr_val" with "[//]") as "H". + iNamedSuffix "H" "_dec". iNamed "Hown_obj_dec". + wp_loadField. + (* TODO: seal up own_merkle so it doesn't get unfolded by iFrame. *) + wp_if_destruct. { iApply "HΦ". by iFrame "Htree_map ∗". } + iApply "HΦ". iFrame "Htree_map ∗". + iNamedSuffix "Herr_map" "_map". + iDestruct (is_merkle_proof_to_entry with "His_proof_map") as "#His_entry". + iDestruct (is_merkle_entry_with_map with "His_entry His_dig_map") as %Hlook_keys. + iDestruct (own_slice_small_sz with "Hsl_tail_dec") as %Hlen_tail. + opose proof (nil_length_inv tail _) as ->; [word|]. + (* TODO: somehow u64_le now gets unfolded by simpl. *) + iPureIntro. eexists. repeat try split; [naive_solver|..]. + { rewrite lookup_fmap in Hlook_keys. by apply fmap_None in Hlook_keys. } + by list_simplifier. +Qed. + +Lemma wp_checkUpd ptr_keys keys ptr_upd upd_refs upd nextEp : + {{{ + "Hown_keys" ∷ own_merkle ptr_keys (lower_map keys) ∗ + "#Hown_upd_refs" ∷ own_map ptr_upd DfracDiscarded upd_refs ∗ + "#Hown_upd" ∷ ([∗ map] sl;v ∈ upd_refs;upd, + own_slice_small sl byteT DfracDiscarded v) + }}} + checkUpd #ptr_keys #nextEp #ptr_upd + {{{ + (err : bool), RET #err; + "Hown_keys" ∷ own_merkle ptr_keys (lower_map keys) ∗ + "Herr" ∷ (if err then True else + ([∗ map] label ↦ val ∈ upd, ⌜ upd_checks keys nextEp label val ⌝)) + }}}. +Proof. + iIntros (Φ) "H HΦ". iNamed "H". wp_rec. + wp_apply wp_ref_of_zero; [done|]. iIntros (ptr_loopErr) "Hptr_loopErr". + wp_apply (wp_MapIter_fold _ _ _ + (λ upd_refs', + ∃ (loopErr : bool), + "Hown_keys" ∷ own_merkle ptr_keys (lower_map keys) ∗ + "Hptr_loopErr" ∷ ptr_loopErr ↦[boolT] #loopErr ∗ + "HloopErr" ∷ (if loopErr then True else + ∃ upd', + "%Hdom" ∷ ⌜ dom upd_refs' = dom upd' ⌝ ∗ + "%Hsub" ∷ ⌜ upd' ⊆ upd ⌝ ∗ + "%Hchecks" ∷ ([∗ map] label ↦ val ∈ upd', ⌜ upd_checks keys nextEp label val ⌝)) + )%I with "Hown_upd_refs [$Hown_keys $Hptr_loopErr]"). + { iExists ∅. repeat try iSplit; try naive_solver. + iPureIntro. eapply map_empty_subseteq. } + { clear. iIntros (? k sl_v Φ) "!> (H&_&%Hlook_ptr) HΦ". iNamed "H". + wp_apply wp_StringToBytes. iIntros (?) "Hsl_label". + iDestruct (own_slice_to_small with "Hsl_label") as "Hsl_label". + iDestruct (big_sepM2_lookup_l_some with "Hown_upd") as %[v Hlook_val]; + [exact Hlook_ptr|]. + iDestruct (big_sepM2_lookup with "Hown_upd") as "#Hsl_val"; + [exact Hlook_ptr|exact Hlook_val|]. + wp_apply (wp_checkOneUpd with "[$Hown_keys $Hsl_label $Hsl_val]"). + iIntros "*". iNamed 1. wp_if_destruct. + { wp_store. iApply "HΦ". by iFrame. } + iDestruct "Herr" as "%Herr". iApply "HΦ". iFrame. + destruct loopErr; [done|]. iNamed "HloopErr". + iExists (<[k:=v]> upd'). iPureIntro. repeat try split. + - set_solver. + - by apply insert_subseteq_l. + - by apply map_Forall_insert_2. } + iIntros "[_ H]". iNamed "H". + wp_load. iApply "HΦ". iFrame. destruct loopErr; [done|]. iNamed "HloopErr". + iDestruct (big_sepM2_dom with "Hown_upd") as %Hdom1. + opose proof (map_subset_dom_eq _ _ _ _ _ Hsub) as ->; [|done]. + by rewrite -Hdom -Hdom1. +Qed. + +Lemma wp_Auditor__Update a ptr_upd upd : + {{{ + "#Hvalid" ∷ Auditor.valid a ∗ + "Hupdate" ∷ UpdateProof.own ptr_upd upd + }}} + Auditor__Update #a #ptr_upd + {{{ + (e : bool), RET #e; True + }}}. +Proof. + iIntros (?) "H HΦ". iNamed "H". iNamed "Hvalid". wp_rec. + wp_loadField. + wp_apply (wp_Mutex__Lock with "[$]"). + iIntros "[Hlock H]". iNamed "H". + wp_loadField. wp_apply wp_slice_len. + iNamed "Hupdate". do 2 wp_loadField. + + (* XXX: checkUpd only gets called here. Inlining its proof. *) + wp_rec. + wp_pures. + wp_loadField. + wp_apply wp_slice_len. + wp_pures. + wp_apply wp_ref_of_zero. + { done. } + iIntros (?) "Hl". + wp_pures. + wp_apply (wp_MapIter_fold _ _ _ (λ _, + _ + )%I with "[$] [-HΦ]"). + { iNamedAccu. } + { + iIntros "* !# * [Hpre %Hlookup] HΦ". + iNamed "Hpre". + wp_pures. + wp_apply wp_StringToBytes. + iIntros "* ?". + iDestruct (own_slice_to_small with "[$]") as "?". + (* XXX: checkOneUpd only called here so inlining a proof. *) + wp_rec. + wp_pures. + wp_loadField. + wp_apply (wp_Tree_Get with "[$]"). + iIntros "* HGetPost". + iNamed "HGetPost". + (* iNamed "Hreply". *) + wp_pures. + admit. + } +Admitted. + End specs. diff --git a/src/program_proof/pav/merkle.v b/src/program_proof/pav/merkle.v index ebf09a337..a988399a7 100644 --- a/src/program_proof/pav/merkle.v +++ b/src/program_proof/pav/merkle.v @@ -1110,18 +1110,18 @@ Proof. admit. Admitted. -Lemma wp_Tree__Put ptr_tr entries sl_label label sl_val val d0 d1 : +Lemma wp_Tree__Put ptr_tr entries sl_label label sl_val val dq0 dq1 : {{{ "Htree" ∷ own_merkle ptr_tr entries ∗ - "Hlabel" ∷ own_slice_small sl_label byteT d0 label ∗ - "Hval" ∷ own_slice_small sl_val byteT d1 val + "Hlabel" ∷ own_slice_small sl_label byteT dq0 label ∗ + "Hval" ∷ own_slice_small sl_val byteT dq1 val }}} Tree__Put #ptr_tr (slice_val sl_label) (slice_val sl_val) {{{ sl_dig sl_proof (err : bool), RET ((slice_val sl_dig), (slice_val sl_proof), #err); - "Hlabel" ∷ own_slice_small sl_label byteT d0 label ∗ - "%Hgenie" ∷ ⌜ length label = hash_len ↔ err = false ⌝ ∗ + "Hlabel" ∷ own_slice_small sl_label byteT dq0 label ∗ + "%Hgenie" ∷ ⌜ err = false ↔ length label = hash_len ⌝ ∗ "Herr" ∷ if negb err then ∃ dig proof, @@ -1233,7 +1233,7 @@ Proof. set (loopInv := (λ (depth : w64), ∃ (currNode_ptr : loc) sub_tree interiors_sl (interiors : list loc), - "Hlabel" ∷ own_slice_small sl_label byteT d0 label ∗ + "Hlabel" ∷ own_slice_small sl_label byteT dq0 label ∗ "Hinteriors_ptr" ∷ interiors_ptr ↦[slice.T ptrT] (slice_val interiors_sl) ∗ "Hinteriors" ∷ own_slice interiors_sl ptrT (DfracOwn 1) interiors ∗ @@ -1821,18 +1821,18 @@ Proof. *) Admitted. -Lemma wp_Tree__Get ptr_tr entries sl_label label d0 : +Lemma wp_Tree__Get ptr_tr entries sl_label label dq0 : {{{ "Htree" ∷ own_merkle ptr_tr entries ∗ - "Hlabel" ∷ own_slice_small sl_label byteT d0 label + "Hlabel" ∷ own_slice_small sl_label byteT dq0 label }}} Tree__Get #ptr_tr (slice_val sl_label) {{{ sl_val sl_dig (proofTy : bool) sl_proof (err : bool), RET (slice_val sl_val, slice_val sl_dig, #proofTy, slice_val sl_proof, #err); "Htree" ∷ own_merkle ptr_tr entries ∗ - "Hlabel" ∷ own_slice_small sl_label byteT d0 label ∗ - "%Hgenie" ∷ ⌜ length label = hash_len ↔ err = false ⌝ ∗ + "Hlabel" ∷ own_slice_small sl_label byteT dq0 label ∗ + "%Hgenie" ∷ ⌜ err = false ↔ length label = hash_len ⌝ ∗ "Herr" ∷ (if err then True else ∃ val dig proof, "#Hsl_val" ∷ own_slice_small sl_val byteT DfracDiscarded val ∗ diff --git a/src/program_proof/pav/serde.v b/src/program_proof/pav/serde.v index 63ac4d615..9a7d94641 100644 --- a/src/program_proof/pav/serde.v +++ b/src/program_proof/pav/serde.v @@ -104,9 +104,9 @@ Lemma wp_dec sl_enc dq enc : is there any way to rewrite the spec to avoid this? *) "Herr" ∷ (⌜ err = false ⌝ -∗ ∃ obj tail, - own ptr_obj obj ∗ - own_slice_small sl_tail byteT dq tail ∗ - ⌜ enc = encodesF obj ++ tail ⌝) + "Hown_obj" ∷ own ptr_obj obj ∗ + "Hsl_tail" ∷ own_slice_small sl_tail byteT dq tail ∗ + "%Henc_obj" ∷ ⌜ enc = encodesF obj ++ tail ⌝) }}}. Proof. Admitted.