Skip to content

Commit

Permalink
qed auditor checkUpd
Browse files Browse the repository at this point in the history
  • Loading branch information
@sanjit-bhat
sanjit-bhat committed Jan 4, 2025
1 parent ee66011 commit 6cb7bef
Show file tree
Hide file tree
Showing 4 changed files with 213 additions and 107 deletions.
76 changes: 45 additions & 31 deletions external/Goose/github_com/mit_pdos/pav/kt.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)

Expand All @@ -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
Expand All @@ -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
Expand All @@ -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");;
Expand Down
218 changes: 155 additions & 63 deletions src/program_proof/pav/auditor.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 Σ}.
Expand Down Expand Up @@ -73,7 +74,7 @@ Context `{!heapGS Σ, !pavG Σ}.

Lemma wp_NewAuditor :
{{{
True
True
}}}
NewAuditor #()
{{{
Expand Down Expand Up @@ -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".
Expand All @@ -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Φ]").
Expand Down Expand Up @@ -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.
Loading

0 comments on commit 6cb7bef

Please sign in to comment.