Timings for setstate_proof.v
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-perennial.dev/./src/program_proof/vrsm/replica/setstate_proof.v.timing
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-perennial.dev/./src/program_proof/vrsm/replica/setstate_proof.v.timing
From Perennial.program_proof Require Import grove_prelude.
From Perennial Require Import marshal_stateless_proof replica.definitions
replica.increasecommit_proof.
From Perennial.program_proof.reconnectclient Require Import proof.
From iris.algebra Require Import mono_list.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.
Section pb_setstate_proof.
Context {params:pbParams.t}.
Context `{!waitgroupG Σ}.
Lemma wp_Clerk__SetState γ γsrv ck args_ptr (prevEpoch epoch committedNextIndex:u64) opsfull snap :
{{{
"#Hck" ∷ is_Clerk ck γ γsrv ∗
"#Hprop_lb" ∷ is_proposal_lb γ.(s_pb) epoch opsfull ∗
"#Hprop_facts" ∷ is_proposal_facts γ.(s_pb) epoch opsfull ∗
"#Hprop_facts_prim" ∷ is_proposal_facts_prim γ.(s_prim) epoch opsfull ∗
"%Henc" ∷ ⌜has_snap_encoding snap (get_rwops opsfull)⌝ ∗
"%Hno_overflow" ∷ ⌜length (get_rwops opsfull) = int.nat (length (get_rwops opsfull))⌝ ∗
"#Hin_conf" ∷ is_in_config γ γsrv epoch ∗
"%Hle" ∷ ⌜int.nat prevEpoch < int.nat epoch⌝ ∗
"#HcommitFacts" ∷ commitIndex_facts γ prevEpoch committedNextIndex ∗
"Hargs" ∷ SetStateArgs.own args_ptr (SetStateArgs.mkC epoch (length (get_rwops opsfull)) committedNextIndex snap)
}}}
Clerk__SetState #ck #args_ptr
{{{
(err:u64), RET #err;
□(if (decide (err = U64 0)) then
is_epoch_lb γsrv.(r_pb) epoch
else
True)
}}}.
wp_apply (wp_ref_of_zero).
wp_apply (SetStateArgs.wp_Encode with "[$Hargs]").
iIntros (enc_args enc_args_sl) "(%Henc_args & Henc_args_sl & Hargs)".
iDestruct (own_slice_to_small with "Henc_args_sl") as "Henc_args_sl".
wp_apply (wp_frame_wand with "HΦ").
rewrite is_pb_rpcs_unfold.
wp_apply (wp_ReconnectingClient__Call2 with "Hcl_rpc [] Henc_args_sl Hrep").
iDestruct "Hsrv" as "[_ [$ _]]".
iFrame "Hprop_lb Hprop_facts Hprop_facts_prim #".
(* No error from RPC, state was accepted *)
iIntros (?) "%Henc_rep Hargs_sl".
iIntros (?) "Hrep Hrep_sl".
(* FIXME: separate lemma *)
wp_apply (wp_ReadInt with "Hrep_sl").
(* SetState was rejected by the server (e.g. stale epoch number) *)
iIntros (err) "%Herr_nz".
wp_apply (wp_ReadInt with "[$]").
Lemma get_epoch_eph γ γsrv st :
own_Server_ghost_eph_f st γ γsrv -∗
is_epoch_lb γsrv.(r_pb) st.(server.epoch)
.
rewrite /own_Server_ghost_eph_f /tc_opaque.
Lemma setstate_primary_eph_step γ γsrv epoch isPrimary canBecomePrimary committedNextIndex epoch' ops ops' :
int.nat epoch < int.nat epoch' →
is_proposal_lb γ.(s_pb) epoch' ops' -∗
is_proposal_facts_prim γ.(s_prim) epoch' ops' -∗
own_tok γsrv.(r_prim) epoch' -∗
own_Primary_ghost_f γ γsrv isPrimary canBecomePrimary epoch committedNextIndex ops -∗
own_Primary_ghost_f γ γsrv true false epoch' committedNextIndex ops'
.
iIntros (Hepoch) "#Hprop_lb #Hprim_facts Htok_in".
rewrite /own_Primary_ghost_f /tc_opaque.
Lemma lease_invalid γ epoch leaseValid leaseExpiration :
is_Server_lease_resource γ epoch leaseValid leaseExpiration -∗
is_Server_lease_resource γ epoch false leaseExpiration
.
Lemma setstate_eph_step γ γsrv st epoch' ops' :
int.nat st.(server.epoch) < int.nat epoch' →
is_proposal_lb γ.(s_pb) epoch' ops' -∗
is_proposal_facts γ.(s_pb) epoch' ops' -∗
is_proposal_facts_prim γ.(s_prim) epoch' ops' -∗
is_in_config γ γsrv epoch' -∗
own_tok γsrv.(r_prim) epoch' -∗
own_Server_ghost_eph_f st γ γsrv ==∗
(is_epoch_lb γsrv.(r_pb) epoch' -∗
is_accepted_lb γsrv.(r_pb) epoch' ops' -∗
own_Server_ghost_eph_f (st <| server.ops_full_eph := ops' |> <| server.epoch := epoch' |>
<| server.sealed := false |> <| server.isPrimary := false |>
<| server.canBecomePrimary := true |>
<| server.leaseValid := false |>
) γ γsrv)
.
iIntros "#Hprop_lb #Hprop_facts #Hprim_facts #Hin_conf' Htok Hghost".
rewrite /own_Server_ghost_eph_f /tc_opaque.
iDestruct (lease_invalid with "[$]") as "$".
iApply (setstate_primary_eph_step with "Hprop_lb Hprim_facts Htok Hprimary").
iDestruct ("Hcommit_fact" with "[] [] Hprop_lb Hprop_facts") as "%".
iApply (fmlist_ptsto_lb_mono with "Hprop_lb").
Lemma setstate_step γ γsrv epoch ops sealed epoch' opsfull':
int.nat epoch < int.nat epoch' →
is_proposal_lb γ.(s_pb) epoch' opsfull' -∗
is_proposal_facts γ.(s_pb) epoch' opsfull' -∗
is_proposal_facts_prim γ.(s_prim) epoch' opsfull' -∗
is_in_config γ γsrv epoch' -∗
own_Server_ghost_f γ γsrv epoch ops sealed ={⊤∖↑pbAofN}=∗
own_Server_ghost_f γ γsrv epoch' (get_rwops opsfull') false ∗
is_epoch_lb γsrv.(r_pb) epoch' ∗
is_accepted_lb γsrv.(r_pb) epoch' opsfull' ∗
own_tok γsrv.(r_prim) epoch'
.
iIntros "#? #? #? #? Hghost".
iMod (ghost_accept_and_unseal with "Hghost [$] [$]") as "Hghost".
iDestruct (ghost_get_epoch_lb with "Hghost") as "#Hepoch_lb".
iDestruct (ghost_get_accepted_lb with "Hghost") as "#Hacc_lb".
iDestruct (ghost_primary_accept_new_epoch with "Hprim_escrow") as "[Hprim_escrow $]".
iCombine "Hepoch_lb Hacc_lb" as "HH".
Lemma wp_Server__SetState γ γsrv s args_ptr args opsfull Φ Ψ :
is_Server s γ γsrv -∗
SetStateArgs.own args_ptr args -∗
(∀ (err:u64), Ψ err -∗ Φ #err) -∗
SetState_core_spec γ γsrv args opsfull Ψ -∗
WP Server__SetState #s #args_ptr {{ Φ }}
.
iIntros "#His_srv Hargs HΦ HΨ".
wp_apply (acquire_spec with "[$HmuInv]").
iIntros "[Hlocked Hown]".
unfold SetState_core_spec.
iDestruct "HΨ" as (?) "(_ & _ & _ & _ & _ & _ & HΨ)".
wp_apply (release_spec with "[-HΨ HΦ]").
iSplitR "HghostEph"; last iFrame.
(* successfully set the state *)
(* state has been set previously. Use is_prop_lb to get agreement. *)
iDestruct (get_epoch_eph with "HghostEph") as "#Heph_lb".
iDestruct "HΨ" as (?) "(_ & _ & _ & _ & _ & _ & _ & _ & HΨ)".
wp_apply (release_spec with "[-HΨ HΦ]").
iSplitR "HghostEph"; last iFrame.
iAssert (_) with "HisSm" as "#HisSm2".
iEval (rewrite /is_StateMachine /tc_opaque) in "HisSm2".
iDestruct "HΨ" as (prevEpoch) "(%Henc_snap & %Hlen_nooverflow & %Hle & #Hprop_lb & #Hprop_facts & #Hprim_facts & #Hin_conf & #HcommitFacts & HΨ)".
replace (args.(SetStateArgs.nextIndex)) with (U64 (length (get_rwops opsfull))) by word.
assert (int.nat st.(server.epoch) < int.nat args.(SetStateArgs.epoch)) as HepochIneq.
(* FIXME: should be trivial, almost `word` proof. Have (a ≠ b) and ¬(a < b) *)
assert (int.nat st.(server.epoch) ≠ int.nat args.(SetStateArgs.epoch)).
unfold is_SetStateAndUnseal_fn.
wp_apply ("HsetStateSpec" with "[$Hstate]").
iMod (setstate_step with "[$] [$] [$] [$] Hghost") as "[$ H]".
iIntros "(Hstate & #Hepoch_lb & #Hacc_lb & Htok)".
iMod (setstate_eph_step with "Hprop_lb Hprop_facts Hprim_facts Hin_conf Htok HghostEph") as "HghostEph".
iDestruct ("HghostEph" with "Hepoch_lb Hacc_lb") as "HghostEph".
(* signal all opApplied condvars *)
wp_apply (wp_MapIter with "HopAppliedConds_map HopAppliedConds_conds").
iFrame "HopAppliedConds_conds".
(* prove one iteration of the map for loop *)
iIntros (?) "!# [_ #Hpre] HΦ".
wp_apply (wp_condSignal with "Hpre").
instantiate (1:=(λ _ _, True)%I).
iIntros "(HopAppliedConds_map & _ & _)".
wp_apply (wp_condBroadcast with "[]").
iIntros (opAppliedConds_loc_new) "Hmapnew".
wp_apply (release_spec with "[-HΨ HΦ Hargs_committed_next_index]").
iSplitR "HghostEph"; last iFrame.
(* FIXME: how to avoid needing to unfold? *)
wp_apply (wp_Server__IncreaseCommit with "[] [-] []").
repeat iExists _; iFrame "#".
instantiate (1:=(λ _, True)%I).
repeat iExists _; iFrame "Hcommit_fact #".
iDestruct (mono_nat_lb_own_le with "Hepoch_lb") as "$".
rewrite fmap_length in HcommitLen.