diff --git a/src/program_proof/tulip/base.v b/src/program_proof/tulip/base.v index 9ce58a5c3..11c359d67 100644 --- a/src/program_proof/tulip/base.v +++ b/src/program_proof/tulip/base.v @@ -15,78 +15,6 @@ Inductive txnres := | ResCommitted (wrs : dbmap) | ResAborted. -Definition dbval_to_val (v : dbval) : val := - match v with - | Some s => (#true, (#(LitString s), #())) - | None => (#false, (zero_val stringT, #())) - end. - -Definition dbval_from_val (v : val) : option dbval := - match v with - | (#(LitBool b), (#(LitString s), #()))%V => if b then Some (Some s) else Some None - | _ => None - end. - -#[global] -Instance dbval_into_val : IntoVal dbval. -Proof. - refine {| - to_val := dbval_to_val; - from_val := dbval_from_val; - IntoVal_def := None; - |}. - intros v. - by destruct v. -Defined. - -#[global] -Instance dbval_into_val_for_type : IntoValForType dbval (boolT * (stringT * unitT)%ht). -Proof. constructor; [done | done | intros [v |]; by auto]. Defined. - -Definition dbmod_to_val (x : dbmod) : val := - (#(LitString x.1), (dbval_to_val x.2, #())). - -Definition dbmod_from_val (v : val) : option dbmod := - match v with - | (#(LitString k), (dbv, #()))%V => match dbval_from_val dbv with - | Some x => Some (k, x) - | _ => None - end - | _ => None - end. - -#[global] -Instance dbmod_into_val : IntoVal dbmod. -Proof. - refine {| - to_val := dbmod_to_val; - from_val := dbmod_from_val; - IntoVal_def := ("", None); - |}. - intros [k v]. - by destruct v. -Defined. - -Definition ppsl_to_val (v : ppsl) : val := (#v.1, (#v.2, #())). - -Definition ppsl_from_val (v : val) : option ppsl := - match v with - | (#(LitInt n), (#(LitBool b), #()))%V => Some (n, b) - | _ => None - end. - -#[global] -Instance ppsl_into_val : IntoVal ppsl. -Proof. - refine {| - to_val := ppsl_to_val; - from_val := ppsl_from_val; - IntoVal_def := (W64 0, false); - |}. - intros v. - by destruct v. -Defined. - Definition fstring := {k : string | (String.length k < 2 ^ 64)%nat}. #[local] diff --git a/src/program_proof/tulip/inv.v b/src/program_proof/tulip/inv.v index f5fe62131..35b8ddb08 100644 --- a/src/program_proof/tulip/inv.v +++ b/src/program_proof/tulip/inv.v @@ -12,6 +12,7 @@ Section inv. Definition sysNS := nroot .@ "sys". Definition tulipNS := sysNS .@ "tulip". Definition tsNS := sysNS .@ "ts". + Definition txnlogN := sysNS .@ "txnlog". Definition tulip_inv_with_proph γ p : iProp Σ := (* txn invariants *) diff --git a/src/program_proof/tulip/program/prelude.v b/src/program_proof/tulip/program/prelude.v new file mode 100644 index 000000000..d78183d44 --- /dev/null +++ b/src/program_proof/tulip/program/prelude.v @@ -0,0 +1,89 @@ +From Perennial.program_proof.tulip Require Export prelude. +From Goose.github_com.mit_pdos.tulip Require Export + backup gcoord index params quorum replica tulip tuple txn txnlog util. + +Definition dbval_to_val (v : dbval) : val := + match v with + | Some s => (#true, (#(LitString s), #())) + | None => (#false, (zero_val stringT, #())) + end. + +Definition dbval_from_val (v : val) : option dbval := + match v with + | (#(LitBool b), (#(LitString s), #()))%V => if b then Some (Some s) else Some None + | _ => None + end. + +#[global] +Instance dbval_into_val : IntoVal dbval. +Proof. + refine {| + to_val := dbval_to_val; + from_val := dbval_from_val; + IntoVal_def := None; + |}. + intros v. + by destruct v. +Defined. + +#[global] +Instance dbval_into_val_for_type : IntoValForType dbval (boolT * (stringT * unitT)%ht). +Proof. constructor; [done | done | intros [v |]; by auto]. Defined. + +Definition dbmod_to_val (x : dbmod) : val := + (#(LitString x.1), (dbval_to_val x.2, #())). + +Definition dbmod_from_val (v : val) : option dbmod := + match v with + | (#(LitString k), (dbv, #()))%V => match dbval_from_val dbv with + | Some x => Some (k, x) + | _ => None + end + | _ => None + end. + +#[global] +Instance dbmod_into_val : IntoVal dbmod. +Proof. + refine {| + to_val := dbmod_to_val; + from_val := dbmod_from_val; + IntoVal_def := ("", None); + |}. + intros [k v]. + by destruct v. +Defined. + +Definition ppsl_to_val (v : ppsl) : val := (#v.1, (#v.2, #())). + +Definition ppsl_from_val (v : val) : option ppsl := + match v with + | (#(LitInt n), (#(LitBool b), #()))%V => Some (n, b) + | _ => None + end. + +#[global] +Instance ppsl_into_val : IntoVal ppsl. +Proof. + refine {| + to_val := ppsl_to_val; + from_val := ppsl_from_val; + IntoVal_def := (W64 0, false); + |}. + intros v. + by destruct v. +Defined. + +Definition ccommand_to_val (pwrsS : Slice.t) (c : ccommand) : val := + match c with + | CmdCommit ts _ => (#(U64 0), (#(U64 ts), (to_val pwrsS, (zero_val stringT, #())))) + | CmdAbort ts => (#(U64 1), (#(U64 ts), (Slice.nil, (zero_val stringT, #())))) + end. + +Section def. + Context `{!heapGS Σ, !tulip_ghostG Σ}. + + Definition own_dbmap_in_slice s (l : list dbmod) (m : dbmap) : iProp Σ := + own_slice s (struct.t WriteEntry) (DfracOwn 1) l ∗ ⌜map_to_list m = l⌝. + +End def. diff --git a/src/program_proof/tulip/program/replica/replica.v b/src/program_proof/tulip/program/replica/replica.v index 4caab8f0a..3a3bd47c7 100644 --- a/src/program_proof/tulip/program/replica/replica.v +++ b/src/program_proof/tulip/program/replica/replica.v @@ -1,124 +1,16 @@ -From Perennial.program_proof.tulip Require Import prelude. From Perennial.program_proof.tulip.invariance Require Import validate execute accept. -From Perennial.program_proof Require Import std_proof. -From Perennial.program_proof.tulip.program Require Import tuple index txnlog. -From Goose.github_com.mit_pdos.tulip Require Import tulip replica. - -Inductive rpres := -| ReplicaOK -| ReplicaCommittedTxn -| ReplicaAbortedTxn -| ReplicaStaleCoordinator -| ReplicaFailedValidation -| ReplicaInvalidRank -| ReplicaWrongLeader. - -Definition rpres_to_u64 (r : rpres) := - match r with - | ReplicaOK => (U64 0) - | ReplicaCommittedTxn => (U64 1) - | ReplicaAbortedTxn => (U64 2) - | ReplicaStaleCoordinator => (U64 3) - | ReplicaFailedValidation => (U64 4) - | ReplicaInvalidRank => (U64 5) - | ReplicaWrongLeader => (U64 6) - end. +From Perennial.program_proof.tulip.program Require Import prelude. +From Perennial.program_proof.tulip.program.replica Require Import + replica_repr replica_accept replica_acquire replica_bump_key replica_finalized + replica_last_proposal replica_lowest_rank replica_readable_key replica_release_key + replica_writable_key. +From Perennial.program_proof.tulip.program.tuple Require Import tuple. +From Perennial.program_proof.tulip.program.txnlog Require Import txnlog. +From Perennial.program_proof.tulip.program.index Require Import index. Section replica. Context `{!heapGS Σ, !tulip_ghostG Σ}. - (*@ type Replica struct { @*) - (*@ // Mutex. @*) - (*@ mu *sync.Mutex @*) - (*@ // Replica ID. @*) - (*@ rid uint64 @*) - (*@ // Replicated transaction log. @*) - (*@ txnlog *txnlog.TxnLog @*) - (*@ // @*) - (*@ // Fields below are application states. @*) - (*@ // @*) - (*@ // LSN up to which all commands have been applied. @*) - (*@ lsna uint64 @*) - (*@ // Write sets of validated transactions. @*) - (*@ prepm map[uint64][]tulip.WriteEntry @*) - (*@ // Participant groups of validated transactions. @*) - (*@ ptgsm map[uint64][]uint64 @*) - (*@ // Prepare status table. @*) - (*@ pstbl map[uint64]PrepareStatusEntry @*) - (*@ // Transaction status table; mapping from transaction timestamps to their @*) - (*@ // commit/abort status. @*) - (*@ txntbl map[uint64]bool @*) - (*@ // Mapping from keys to their prepare timestamps. @*) - (*@ ptsm map[string]uint64 @*) - (*@ // Mapping from keys to their smallest preparable timestamps. @*) - (*@ sptsm map[string]uint64 @*) - (*@ // Index. @*) - (*@ idx *index.Index @*) - (*@ // @*) - (*@ // Fields below are group info initialized after creation of all replicas. @*) - (*@ // @*) - (*@ // Replicas in the same group. Read-only. @*) - (*@ rps map[uint64]grove_ffi.Address @*) - (*@ // ID of the replica believed to be the leader of this group. Used to @*) - (*@ // initialize backup coordinators. @*) - (*@ leader uint64 @*) - (*@ } @*) - Definition own_replica_cm (rp : loc) (cm : gmap nat bool) : iProp Σ := - ∃ (txntblP : loc) (txntbl : gmap u64 bool), - "HtxntblP" ∷ rp ↦[Replica :: "txntbl"] #txntblP ∗ - "Htxntbl" ∷ own_map txntblP (DfracOwn 1) txntbl ∗ - "%Hcmabs" ∷ ⌜(kmap Z.of_nat cm : gmap Z bool) = kmap uint.Z txntbl⌝. - - Definition own_replica_cpm (rp : loc) (cpm : gmap nat dbmap) : iProp Σ := - ∃ (prepmP : loc) (prepmS : gmap u64 Slice.t) (prepm : gmap u64 dbmap), - "HprepmP" ∷ rp ↦[Replica :: "prepm"] #prepmP ∗ - "HprepmS" ∷ own_map prepmP (DfracOwn 1) prepmS ∗ - "Hprepm" ∷ ([∗ map] s; m ∈ prepmS; prepm, ∃ l, own_dbmap_in_slice s l m) ∗ - "%Hcpmabs" ∷ ⌜(kmap Z.of_nat cpm : gmap Z dbmap) = kmap uint.Z prepm⌝. - - Definition absrel_ptsm (ptsm : gmap dbkey nat) (ptsmM : gmap dbkey u64) := - ∀ k, - k ∈ keys_all -> - match ptsmM !! k with - | Some ptsW => ptsm !! k = Some (uint.nat ptsW) - | _ => ptsm !! k = Some O - end. - - Definition own_replica_ptsm_sptsm - (rp : loc) (ptsm sptsm : gmap dbkey nat) : iProp Σ := - ∃ (ptsmP : loc) (sptsmP : loc) (ptsmM : gmap dbkey u64) (sptsmM : gmap dbkey u64), - "HptsmP" ∷ rp ↦[Replica :: "ptsm"] #ptsmP ∗ - "HsptsmP" ∷ rp ↦[Replica :: "sptsm"] #sptsmP ∗ - "HptsmM" ∷ own_map ptsmP (DfracOwn 1) ptsmM ∗ - "HsptsmM" ∷ own_map sptsmP (DfracOwn 1) sptsmM ∗ - "%Hptsmabs" ∷ ⌜absrel_ptsm ptsm ptsmM⌝ ∗ - "%Hsptsmabs" ∷ ⌜absrel_ptsm sptsm sptsmM⌝. - - Lemma own_replica_ptsm_sptsm_dom rp ptsm sptsm : - own_replica_ptsm_sptsm rp ptsm sptsm -∗ - ⌜keys_all ⊆ dom ptsm ∧ keys_all ⊆ dom sptsm⌝. - Proof. - iNamed 1. - iPureIntro. - split. - - intros k Hk. specialize (Hptsmabs _ Hk). - apply elem_of_dom. by destruct (ptsmM !! k). - - intros k Hk. specialize (Hsptsmabs _ Hk). - apply elem_of_dom. by destruct (sptsmM !! k). - Qed. - - Definition ppsl_to_nat_bool (psl : ppsl) := (uint.nat psl.1, psl.2). - - Definition own_replica_psm_rkm - (rp : loc) (psm : gmap nat (nat * bool)) (rkm : gmap nat nat) : iProp Σ := - ∃ (pstblP : loc) (rktblP : loc) (pstbl : gmap u64 ppsl) (rktbl : gmap u64 u64), - "HpstblP" ∷ rp ↦[Replica :: "pstbl"] #pstblP ∗ - "HrktblP" ∷ rp ↦[Replica :: "rktbl"] #rktblP ∗ - "Hpstbl" ∷ own_map pstblP (DfracOwn 1) pstbl ∗ - "Hrktbl" ∷ own_map rktblP (DfracOwn 1) rktbl ∗ - "%Hpsmabs" ∷ ⌜(kmap Z.of_nat psm : gmap Z (nat * bool)) = kmap uint.Z (fmap ppsl_to_nat_bool pstbl)⌝ ∗ - "%Hrkmabs" ∷ ⌜(kmap Z.of_nat rkm : gmap Z nat) = kmap uint.Z (fmap (λ x, uint.nat x) rktbl)⌝. - Definition own_replica (rp : loc) (gid rid : u64) γ α : iProp Σ := ∃ (lsna : u64) (cm : gmap nat bool) (histm : gmap dbkey dbhist) (cpm : gmap nat dbmap) (ptgsm : gmap nat (gset u64)) @@ -150,521 +42,6 @@ Section replica. "#Hidx" ∷ is_index idx α ∗ "%Hgid" ∷ ⌜gid ∈ gids_all⌝. - Definition key_writable_ptsm (ptsm : gmap dbkey nat) (key : dbkey) := - match ptsm !! key with - | Some pts => pts = O - | _ => False - end. - - Definition key_writable_sptsm (sptsm : gmap dbkey nat) (ts : nat) (key : dbkey) := - match sptsm !! key with - | Some spts => (spts < ts)%nat - | _ => False - end. - - Definition key_writable (ptsm sptsm : gmap dbkey nat) (ts : nat) (key : dbkey) := - key_writable_ptsm ptsm key ∧ key_writable_sptsm sptsm ts key. - - Theorem wp_Replica__writableKey rp (ts : u64) key ptsm sptsm : - key ∈ keys_all -> - {{{ own_replica_ptsm_sptsm rp ptsm sptsm }}} - Replica__writableKey #rp #ts #(LitString key) - {{{ (ok : bool), RET #ok; - own_replica_ptsm_sptsm rp ptsm sptsm ∗ - ⌜if ok then key_writable ptsm sptsm (uint.nat ts) key else True⌝ - }}}. - Proof. - iIntros (Hkey Φ) "Hrp HΦ". - wp_rec. - - (*@ func (rp *Replica) writableKey(ts uint64, key string) bool { @*) - (*@ // The default of prepare timestamps are 0, so no need to check existence. @*) - (*@ pts := rp.ptsm[key] @*) - (*@ if pts != 0 { @*) - (*@ return false @*) - (*@ } @*) - (*@ @*) - iNamed "Hrp". - wp_loadField. - wp_apply (wp_MapGet with "HptsmM"). - iIntros (pts okpts) "[%Hpts HptsmM]". - wp_pures. - case_bool_decide as Hptsz; wp_pures; last first. - { iApply "HΦ". by iFrame. } - - (*@ // Even though the default of smallest preparable timestamps are 1, using @*) - (*@ // the fact that @ts is positive also means no need to check existence. @*) - (*@ spts := rp.sptsm[key] @*) - - (*@ if ts <= spts { @*) - (*@ return false @*) - (*@ } @*) - (*@ @*) - wp_loadField. - wp_apply (wp_MapGet with "HsptsmM"). - iIntros (spts okspts) "[%Hspts HsptsmM]". - wp_pures. - case_bool_decide as Hgespts; wp_pures. - { iApply "HΦ". by iFrame "HptsmP HsptsmP ∗". } - - (*@ return true @*) - (*@ } @*) - iApply "HΦ". - assert (Hwritable : key_writable ptsm sptsm (uint.nat ts) key). - { inv Hptsz. - split. - { specialize (Hptsmabs _ Hkey). - destruct okpts. - { apply map_get_true in Hpts. - rewrite Hpts uint_nat_W64_0 in Hptsmabs. - by rewrite /key_writable_ptsm Hptsmabs. - } - apply map_get_false in Hpts as [Hpts _]. - rewrite Hpts in Hptsmabs. - by rewrite /key_writable_ptsm Hptsmabs. - } - { specialize (Hsptsmabs _ Hkey). - destruct okspts. - { apply map_get_true in Hspts. - rewrite Hspts in Hsptsmabs. - rewrite /key_writable_sptsm Hsptsmabs. - clear -Hgespts. word. - } - apply map_get_false in Hspts as [Hspts _]. - rewrite Hspts in Hsptsmabs. - rewrite /key_writable_sptsm Hsptsmabs. - clear -Hgespts. word. - } - } - by iFrame "HptsmP HsptsmP ∗". - Qed. - - Definition key_readable (ptsm : gmap dbkey nat) (ts : nat) (key : dbkey) := - match ptsm !! key with - | Some pts => pts = O ∨ (ts < pts)%nat - | _ => False - end. - - Theorem wp_Replica__readableKey rp (ts : u64) key ptsm sptsm : - key ∈ keys_all -> - {{{ own_replica_ptsm_sptsm rp ptsm sptsm }}} - Replica__readableKey #rp #ts #(LitString key) - {{{ (ok : bool), RET #ok; - own_replica_ptsm_sptsm rp ptsm sptsm ∗ - ⌜if ok then key_readable ptsm (uint.nat ts) key else True⌝ - }}}. - Proof. - iIntros (Hkey Φ) "Hrp HΦ". - wp_rec. - - (*@ func (rp *Replica) readableKey(ts uint64, key string) bool { @*) - (*@ pts := rp.ptsm[key] @*) - (*@ if pts != 0 && pts <= ts { @*) - (*@ return false @*) - (*@ } @*) - (*@ @*) - iNamed "Hrp". - wp_loadField. - wp_apply (wp_MapGet with "HptsmM"). - iIntros (pts ok) "[%Hpts HptsmM]". - wp_apply wp_and_pure. - { wp_pures. by rewrite -bool_decide_not. } - { iIntros (_). by wp_pures. } - case_bool_decide as Hcond; wp_pures. - { iApply "HΦ". by iFrame. } - - (*@ return true @*) - (*@ } @*) - iApply "HΦ". - apply Classical_Prop.not_and_or in Hcond. - assert (Hreadable : key_readable ptsm (uint.nat ts) key). - { specialize (Hptsmabs _ Hkey). - destruct ok. - { apply map_get_true in Hpts. - rewrite Hpts in Hptsmabs. - rewrite /key_readable Hptsmabs. - destruct Hcond as [Hz | Hlt]. - { left. apply dec_stable in Hz. inv Hz. by rewrite uint_nat_W64_0. } - { right. clear -Hlt. word. } - } - apply map_get_false in Hpts as [Hpts _]. - rewrite Hpts in Hptsmabs. - rewrite /key_readable Hptsmabs. - by left. - } - by iFrame. - Qed. - - Theorem wp_Replica__acquireKey rp (ts : u64) key ptsm sptsm : - {{{ own_replica_ptsm_sptsm rp ptsm sptsm }}} - Replica__acquireKey #rp #ts #(LitString key) - {{{ RET #(); - own_replica_ptsm_sptsm rp (<[key := uint.nat ts]> ptsm) (<[key := uint.nat ts]> sptsm) - }}}. - Proof. - iIntros (Φ) "Hrp HΦ". - wp_rec. - - (*@ func (rp *Replica) acquireKey(ts uint64, key string) { @*) - (*@ rp.ptsm[key] = ts @*) - (*@ rp.sptsm[key] = ts @*) - (*@ } @*) - iNamed "Hrp". - wp_loadField. - wp_apply (wp_MapInsert with "HptsmM"); first done. - iIntros "HptsmM". - wp_loadField. - wp_apply (wp_MapInsert with "HsptsmM"); first done. - iIntros "HsptsmM". - wp_pures. - iApply "HΦ". - iFrame "HptsmP HsptsmP ∗". - iPureIntro. - split. - { intros k Hk. - destruct (decide (k = key)) as [-> | Hne]; last first. - { do 2 (rewrite lookup_insert_ne; last done). - by apply Hptsmabs. - } - by rewrite 2!lookup_insert. - } - { intros k Hk. - destruct (decide (k = key)) as [-> | Hne]; last first. - { do 2 (rewrite lookup_insert_ne; last done). - by apply Hsptsmabs. - } - by rewrite 2!lookup_insert. - } - Qed. - - Theorem wp_Replica__releaseKey rp key ptsm sptsm : - {{{ own_replica_ptsm_sptsm rp ptsm sptsm }}} - Replica__releaseKey #rp #(LitString key) - {{{ RET #(); - own_replica_ptsm_sptsm rp (<[key := O]> ptsm) sptsm - }}}. - Proof. - iIntros (Φ) "Hrp HΦ". - wp_rec. - (*@ func (rp *Replica) releaseKey(key string) { @*) - (*@ delete(rp.ptsm, key) @*) - (*@ } @*) - iNamed "Hrp". - wp_loadField. - wp_apply (wp_MapDelete with "HptsmM"). - iIntros "HptsmM". - wp_pures. - iApply "HΦ". - iFrame "∗ %". - iPureIntro. - intros k Hk. - destruct (decide (k = key)) as [-> | Hne]; last first. - { rewrite lookup_delete_ne; last done. - rewrite lookup_insert_ne; last done. - by apply Hptsmabs. - } - by rewrite lookup_delete lookup_insert. - Qed. - - Theorem wp_Replica__bumpKey rp (ts : u64) key ptsm sptsm : - uint.Z ts ≠ 0 -> - key ∈ keys_all -> - {{{ own_replica_ptsm_sptsm rp ptsm sptsm }}} - Replica__bumpKey #rp #ts #(LitString key) - {{{ (spts : nat), RET #(bool_decide (spts < pred (uint.nat ts))%nat); - own_replica_ptsm_sptsm rp ptsm (<[key := (spts `max` pred (uint.nat ts))%nat]> sptsm) ∗ - ⌜sptsm !! key = Some spts⌝ - }}}. - Proof. - iIntros (Htsnz Hkey Φ) "Hrp HΦ". - wp_rec. - - (*@ func (rp *Replica) bumpKey(ts uint64, key string) bool { @*) - (*@ spts := rp.sptsm[key] @*) - (*@ if ts - 1 <= spts { @*) - (*@ return false @*) - (*@ } @*) - (*@ rp.sptsm[key] = ts - 1 @*) - (*@ return true @*) - (*@ } @*) - iNamed "Hrp". - wp_loadField. - wp_apply (wp_MapGet with "HsptsmM"). - iIntros (sptsW ok) "[%Hspts HsptsmM]". - wp_pures. - case_bool_decide as Hcond; wp_pures. - { rewrite word.unsigned_sub_nowrap in Hcond; last word. - destruct ok. - { apply map_get_true in Hspts. - iSpecialize ("HΦ" $! (uint.nat sptsW)). - case_bool_decide as Hts; first word. - iApply "HΦ". - iFrame "HptsmP HsptsmP ∗ %". - iPureIntro. - split; last first. - { specialize (Hsptsmabs _ Hkey). - by rewrite Hspts in Hsptsmabs. - } - intros k Hk. - destruct (decide (k = key)) as [-> | Hne]; last first. - { rewrite lookup_insert_ne; last done. - by apply Hsptsmabs. - } - rewrite lookup_insert Hspts. - f_equal. - clear -Hts. word. - } - { apply map_get_false in Hspts as [Hspts ->]. - simpl in Hcond. - iSpecialize ("HΦ" $! O). - case_bool_decide as Hts; first word. - assert (uint.Z ts = 1) by word. - iApply "HΦ". - iFrame "HptsmP HsptsmP ∗ %". - iPureIntro. - assert (Hz : sptsm !! key = Some O). - { specialize (Hsptsmabs _ Hkey). - by rewrite Hspts in Hsptsmabs. - } - split; last apply Hz. - replace (_ `max` _)%nat with O; last word. - by rewrite insert_id. - } - } - rewrite word.unsigned_sub_nowrap in Hcond; last word. - wp_loadField. - wp_apply (wp_MapInsert with "HsptsmM"); first done. - iIntros "HsptsmM". - wp_pures. - destruct ok. - { apply map_get_true in Hspts. - iSpecialize ("HΦ" $! (uint.nat sptsW)). - case_bool_decide as Hts; last word. - iApply "HΦ". - iFrame "HptsmP HsptsmP ∗ %". - iPureIntro. - split; last first. - { specialize (Hsptsmabs _ Hkey). - by rewrite Hspts in Hsptsmabs. - } - intros k Hk. - destruct (decide (k = key)) as [-> | Hne]; last first. - { do 2 (rewrite lookup_insert_ne; last done). - by apply Hsptsmabs. - } - rewrite 2!lookup_insert. - f_equal. - clear -Hcond. word. - } - { apply map_get_false in Hspts as [Hspts ->]. - simpl in Hcond. - iSpecialize ("HΦ" $! O). - case_bool_decide as Hts; last word. - { iApply "HΦ". - assert (Hsptsmkey : sptsm !! key = Some O). - { specialize (Hsptsmabs _ Hkey). - by rewrite Hspts in Hsptsmabs. - } - iFrame "HptsmP HsptsmP ∗ %". - iPureIntro. - intros k Hk. - destruct (decide (k = key)) as [-> | Hne]; last first. - { do 2 (rewrite lookup_insert_ne; last done). - by apply Hsptsmabs. - } - rewrite 2!lookup_insert. - f_equal. - word. - } - } - Qed. - - Theorem wp_Replica__acquire rp (tsW : u64) pwrsS pwrsL pwrs ptsm sptsm : - valid_wrs pwrs -> - let ts := uint.nat tsW in - {{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica_ptsm_sptsm rp ptsm sptsm }}} - Replica__acquire #rp #tsW (to_val pwrsS) - {{{ (acquired : bool), RET #acquired; - own_dbmap_in_slice pwrsS pwrsL pwrs ∗ - if acquired - then own_replica_ptsm_sptsm rp (acquire ts pwrs ptsm) (acquire ts pwrs sptsm) ∗ - ⌜validated_ptsm ptsm pwrs⌝ ∗ - ⌜validated_sptsm sptsm ts pwrs⌝ - else own_replica_ptsm_sptsm rp ptsm sptsm - }}}. - Proof. - iIntros (Hvw ts Φ) "[[HpwrsS %HpwrsL] Hrp] HΦ". - wp_rec. - iDestruct (own_replica_ptsm_sptsm_dom with "Hrp") as %[Hdomptsm Hdomsptsm]. - - (*@ func (rp *Replica) acquire(ts uint64, pwrs []tulip.WriteEntry) bool { @*) - (*@ // Check if all keys are writable. @*) - (*@ var pos uint64 = 0 @*) - (*@ @*) - wp_apply (wp_ref_to); first by auto. - iIntros (posP) "HposP". - wp_pures. - - (*@ for pos < uint64(len(pwrs)) { @*) - (*@ ent := pwrs[pos] @*) - (*@ writable := rp.writableKey(ts, ent.Key) @*) - (*@ if !writable { @*) - (*@ break @*) - (*@ } @*) - (*@ pos++ @*) - (*@ } @*) - (*@ @*) - iDestruct (own_slice_sz with "HpwrsS") as %Hlen. - iDestruct (own_slice_small_acc with "HpwrsS") as "[HpwrsS HpwrsC]". - set P := (λ (cont : bool), ∃ (pos : u64), - let pwrs' := list_to_map (take (uint.nat pos) pwrsL) in - "HpwrsS" ∷ own_slice_small pwrsS (struct.t WriteEntry) (DfracOwn 1) pwrsL ∗ - "HposP" ∷ posP ↦[uint64T] #pos ∗ - "Hrp" ∷ own_replica_ptsm_sptsm rp ptsm sptsm ∗ - "%Hptsm" ∷ ⌜validated_ptsm ptsm pwrs'⌝ ∗ - "%Hsptsm" ∷ ⌜validated_sptsm sptsm ts pwrs'⌝)%I. - wp_apply (wp_forBreak_cond P with "[] [HpwrsS HposP Hrp]"); last first; first 1 last. - { (* Loop entry. *) - iExists (W64 0). - rewrite uint_nat_W64_0 take_0 list_to_map_nil. - iFrame. - iPureIntro. - (* split; first done. *) - split. - { rewrite /validated_ptsm dom_empty_L. - intros k n Hn. - by apply map_lookup_filter_Some in Hn as [_ ?]. - } - { rewrite /validated_sptsm dom_empty_L. - intros k n Hn. - by apply map_lookup_filter_Some in Hn as [_ ?]. - } - } - { (* Loop body. *) - clear Φ. iIntros (Φ) "!> HP HΦ". iNamed "HP". - wp_load. - wp_apply (wp_slice_len). - wp_if_destruct; last first. - { (* Exit from the loop condition. *) - iApply "HΦ". - iExists pos. - by iFrame "∗ %". - } - wp_load. - destruct (lookup_lt_is_Some_2 pwrsL (uint.nat pos)) as [[k v] Hwr]; first word. - wp_apply (wp_SliceGet with "[$HpwrsS]"); first done. - iIntros "HpwrsL". - wp_pures. - wp_apply (wp_Replica__writableKey with "Hrp"). - { rewrite -HpwrsL in Hwr. - apply elem_of_list_lookup_2, elem_of_map_to_list, elem_of_dom_2 in Hwr. - clear -Hvw Hwr. set_solver. - } - iIntros (ok) "[Hrp %Hwritable]". - wp_pures. - destruct ok; wp_pures; last first. - { iApply "HΦ". - by iFrame "∗ %". - } - wp_load. - wp_store. - iApply "HΦ". - iFrame "∗ %". - iPureIntro. - rewrite uint_nat_word_add_S; last word. - rewrite (take_S_r _ _ _ Hwr) list_to_map_snoc; last first. - { by eapply map_to_list_not_elem_of_take_key. } - split. - { intros x n Hn. - apply map_lookup_filter_Some in Hn as [Hn Hx]. - rewrite /= dom_insert_L elem_of_union in Hx. - destruct Hx as [Hx | Hx]; last first. - { specialize (Hptsm x n). simpl in Hptsm. - apply Hptsm. - by apply map_lookup_filter_Some. - } - rewrite elem_of_singleton in Hx. subst x. - destruct Hwritable as [Hwritable _]. - by rewrite /key_writable_ptsm Hn in Hwritable. - } - { intros x n Hn. - apply map_lookup_filter_Some in Hn as [Hn Hx]. - rewrite /= dom_insert_L elem_of_union in Hx. - destruct Hx as [Hx | Hx]; last first. - { specialize (Hsptsm x n). simpl in Hsptsm. - apply Hsptsm. - by apply map_lookup_filter_Some. - } - rewrite elem_of_singleton in Hx. subst x. - destruct Hwritable as [_ Hwritable]. - by rewrite /key_writable_sptsm Hn in Hwritable. - } - } - iNamed 1. clear P. - - (*@ // Report error if some key cannot be locked. @*) - (*@ if pos < uint64(len(pwrs)) { @*) - (*@ return false @*) - (*@ } @*) - (*@ @*) - wp_load. - wp_apply wp_slice_len. - wp_if_destruct. - { iDestruct ("HpwrsC" with "HpwrsS") as "HpwrsS". - iApply "HΦ". - by iFrame "∗ %". - } - rewrite take_ge in Hptsm, Hsptsm; last word. - rewrite -HpwrsL list_to_map_to_list in Hptsm, Hsptsm. - - (*@ // Acquire locks for each key. @*) - (*@ for _, ent := range(pwrs) { @*) - (*@ rp.acquireKey(ts, ent.Key) @*) - (*@ } @*) - (*@ @*) - set P := (λ (i : u64), - let pwrs' := list_to_map (take (uint.nat i) pwrsL) in - own_replica_ptsm_sptsm rp (acquire ts pwrs' ptsm) (acquire ts pwrs' sptsm))%I. - wp_apply (wp_forSlice P with "[] [$HpwrsS Hrp]"); last first; first 1 last. - { (* Loop entry. *) - subst P. simpl. - by rewrite uint_nat_W64_0 take_0 list_to_map_nil /acquire 2!setts_empty. - } - { (* Loop body. *) - clear Φ. - iIntros (i [k v]) "!>". - iIntros (Φ) "(Hrp & %Hbound & %Hi) HΦ". - subst P. simpl. - wp_pures. - wp_apply (wp_Replica__acquireKey with "Hrp"). - iIntros "Hrp". - iApply "HΦ". - rewrite uint_nat_word_add_S; last word. - rewrite (take_S_r _ _ _ Hi) list_to_map_snoc; last first. - { by eapply map_to_list_not_elem_of_take_key. } - rewrite /acquire setts_insert; last first. - { rewrite -HpwrsL in Hi. - apply elem_of_list_lookup_2, elem_of_map_to_list, elem_of_dom_2 in Hi. - clear -Hvw Hi Hdomptsm. set_solver. - } - rewrite /acquire setts_insert; last first. - { rewrite -HpwrsL in Hi. - apply elem_of_list_lookup_2, elem_of_map_to_list, elem_of_dom_2 in Hi. - clear -Hvw Hi Hdomsptsm. set_solver. - } - done. - } - iIntros "[HP HpwrsS]". - iNamed "HP". clear P. - rewrite -Hlen firstn_all -HpwrsL list_to_map_to_list in Hptsmabs, Hsptsmabs. - - (*@ return true @*) - (*@ } @*) - wp_pures. - iDestruct ("HpwrsC" with "HpwrsS") as "HpwrsS". - iApply "HΦ". - by iFrame "HptsmP HsptsmP ∗ %". - Qed. Definition finalized_outcome γ ts res : iProp Σ := match res with @@ -931,128 +308,6 @@ Section replica. by rewrite /execute_cmds foldl_snoc execute_cmds_unfold Hexec /=. Qed. - Theorem wp_Replica__accept (rp : loc) (tsW : u64) (rankW : u64) (dec : bool) psm rkm : - let ts := uint.nat tsW in - let rank := uint.nat rankW in - {{{ own_replica_psm_rkm rp psm rkm }}} - Replica__accept #rp #tsW #rankW #dec - {{{ RET #(); own_replica_psm_rkm rp (<[ts := (rank, dec)]> psm) (<[ts := S rank]> rkm) }}}. - Proof. - iIntros (ts rank Φ) "Hrp HΦ". - wp_rec. - - (*@ func (rp *Replica) accept(ts uint64, rank uint64, dec bool) { @*) - (*@ pp := PrepareProposal{ @*) - (*@ rank : rank, @*) - (*@ dec : dec, @*) - (*@ } @*) - (*@ rp.pstbl[ts] = pp @*) - (*@ rp.rktbl[ts] = std.SumAssumeNoOverflow(rank, 1) @*) - (*@ } @*) - iNamed "Hrp". - wp_loadField. - wp_apply (wp_MapInsert _ _ (rankW, dec) with "Hpstbl"); first done. - iIntros "Hpstbl". - wp_apply wp_SumAssumeNoOverflow. - iIntros (Hnoof). - wp_loadField. - wp_apply (wp_MapInsert with "Hrktbl"); first done. - iIntros "Hrktbl". - wp_pures. - iApply "HΦ". - iFrame. - iPureIntro. - split. - { rewrite fmap_insert 2!kmap_insert. f_equal; [word | done]. } - { rewrite fmap_insert 2!kmap_insert. f_equal; [word | word | done]. } - Qed. - - Theorem wp_Replica__lowestRank rp (tsW : u64) psm rkm : - let ts := uint.nat tsW in - {{{ own_replica_psm_rkm rp psm rkm }}} - Replica__lowestRank #rp #tsW - {{{ (rank : u64) (ok : bool), RET (#rank, #ok); - own_replica_psm_rkm rp psm rkm ∗ - ⌜if ok then rkm !! ts = Some (uint.nat rank) else rkm !! ts = None⌝ - }}}. - Proof. - iIntros (ts Φ) "Hrp HΦ". - wp_rec. - - (*@ func (rp *Replica) lowestRank(ts uint64) (uint64, bool) { @*) - (*@ rank, ok := rp.rktbl[ts] @*) - (*@ return rank, ok @*) - (*@ } @*) - iNamed "Hrp". - wp_loadField. - wp_apply (wp_MapGet with "Hrktbl"). - iIntros (rankW ok) "[%Hok Hrktbl]". - wp_pures. - iApply "HΦ". - iFrame "∗ %". - iPureIntro. - destruct ok. - { apply map_get_true in Hok. - assert (Hrktbl : fmap (λ x, uint.nat x) rktbl !! tsW = Some (uint.nat rankW)). - { by rewrite lookup_fmap Hok. } - symmetry in Hrkmabs. - pose proof (lookup_kmap_eq_Some _ _ _ _ _ _ Hrkmabs Hrktbl) as (ts' & Hts' & Hrkmts). - assert (ts' = ts) as ->. - { subst ts. rewrite Hts'. lia. } - done. - } - { apply map_get_false in Hok as [Hnone _]. - assert (Hrktbl : fmap (λ x, uint.nat x) rktbl !! tsW = None). - { by rewrite lookup_fmap Hnone. } - symmetry in Hrkmabs. - apply (lookup_kmap_eq_None _ _ _ _ _ Hrkmabs Hrktbl). - word. - } - Qed. - - Theorem wp_Replica__lastProposal rp (tsW : u64) psm rkm : - let ts := uint.nat tsW in - {{{ own_replica_psm_rkm rp psm rkm }}} - Replica__lastProposal #rp #tsW - {{{ (rank : u64) (pdec : bool) (ok : bool), RET (#rank, #pdec, #ok); - own_replica_psm_rkm rp psm rkm ∗ - ⌜if ok then psm !! ts = Some (uint.nat rank, pdec) else psm !! ts = None⌝ - }}}. - Proof. - iIntros (ts Φ) "Hrp HΦ". - wp_rec. - - (*@ func (rp *Replica) lastProposal(ts uint64) (uint64, bool, bool) { @*) - (*@ ps, ok := rp.pstbl[ts] @*) - (*@ return ps.rank, ps.dec, ok @*) - (*@ } @*) - iNamed "Hrp". - wp_loadField. - wp_apply (wp_MapGet with "Hpstbl"). - iIntros (psl ok) "[%Hok Hpstbl]". - wp_pures. - iApply "HΦ". - iFrame "∗ %". - iPureIntro. - destruct ok. - { apply map_get_true in Hok. - assert (Hpstbl : fmap ppsl_to_nat_bool pstbl !! tsW = Some (uint.nat psl.1, psl.2)). - { by rewrite lookup_fmap Hok. } - symmetry in Hpsmabs. - pose proof (lookup_kmap_eq_Some _ _ _ _ _ _ Hpsmabs Hpstbl) as (ts' & Hts' & Hpsmts). - assert (ts' = ts) as ->. - { subst ts. rewrite Hts'. lia. } - done. - } - { apply map_get_false in Hok as [Hnone _]. - assert (Hpstbl : fmap ppsl_to_nat_bool pstbl !! tsW = None). - { by rewrite lookup_fmap Hnone. } - symmetry in Hpsmabs. - apply (lookup_kmap_eq_None _ _ _ _ _ Hpsmabs Hpstbl). - word. - } - Qed. - Definition try_accept_outcome γ gid rid ts rank pdec res : iProp Σ := match res with | ReplicaOK => is_replica_pdec_at_rank γ gid rid ts rank pdec diff --git a/src/program_proof/tulip/program/replica/replica_accept.v b/src/program_proof/tulip/program/replica/replica_accept.v new file mode 100644 index 000000000..926b09226 --- /dev/null +++ b/src/program_proof/tulip/program/replica/replica_accept.v @@ -0,0 +1,43 @@ +From Perennial.program_proof.tulip.program Require Import prelude replica_repr. +From Perennial.program_proof Require Import std_proof. + +Section program. + Context `{!heapGS Σ, !tulip_ghostG Σ}. + + Theorem wp_Replica__accept (rp : loc) (tsW : u64) (rankW : u64) (dec : bool) psm rkm : + let ts := uint.nat tsW in + let rank := uint.nat rankW in + {{{ own_replica_psm_rkm rp psm rkm }}} + Replica__accept #rp #tsW #rankW #dec + {{{ RET #(); own_replica_psm_rkm rp (<[ts := (rank, dec)]> psm) (<[ts := S rank]> rkm) }}}. + Proof. + iIntros (ts rank Φ) "Hrp HΦ". + wp_rec. + + (*@ func (rp *Replica) accept(ts uint64, rank uint64, dec bool) { @*) + (*@ pp := PrepareProposal{ @*) + (*@ rank : rank, @*) + (*@ dec : dec, @*) + (*@ } @*) + (*@ rp.pstbl[ts] = pp @*) + (*@ rp.rktbl[ts] = std.SumAssumeNoOverflow(rank, 1) @*) + (*@ } @*) + iNamed "Hrp". + wp_loadField. + wp_apply (wp_MapInsert _ _ (rankW, dec) with "Hpstbl"); first done. + iIntros "Hpstbl". + wp_apply wp_SumAssumeNoOverflow. + iIntros (Hnoof). + wp_loadField. + wp_apply (wp_MapInsert with "Hrktbl"); first done. + iIntros "Hrktbl". + wp_pures. + iApply "HΦ". + iFrame. + iPureIntro. + split. + { rewrite fmap_insert 2!kmap_insert. f_equal; [word | done]. } + { rewrite fmap_insert 2!kmap_insert. f_equal; [word | word | done]. } + Qed. + +End program. diff --git a/src/program_proof/tulip/program/replica/replica_acquire.v b/src/program_proof/tulip/program/replica/replica_acquire.v new file mode 100644 index 000000000..aaf9c92d8 --- /dev/null +++ b/src/program_proof/tulip/program/replica/replica_acquire.v @@ -0,0 +1,196 @@ +From Perennial.program_proof.tulip.invariance Require Import validate. +From Perennial.program_proof.tulip.program Require Import prelude replica_repr. +From Perennial.program_proof.tulip.program.replica Require Import + replica_writable_key replica_readable_key replica_acquire_key. + +Section program. + Context `{!heapGS Σ, !tulip_ghostG Σ}. + + Theorem wp_Replica__acquire rp (tsW : u64) pwrsS pwrsL pwrs ptsm sptsm : + valid_wrs pwrs -> + let ts := uint.nat tsW in + {{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica_ptsm_sptsm rp ptsm sptsm }}} + Replica__acquire #rp #tsW (to_val pwrsS) + {{{ (acquired : bool), RET #acquired; + own_dbmap_in_slice pwrsS pwrsL pwrs ∗ + if acquired + then own_replica_ptsm_sptsm rp (acquire ts pwrs ptsm) (acquire ts pwrs sptsm) ∗ + ⌜validated_ptsm ptsm pwrs⌝ ∗ + ⌜validated_sptsm sptsm ts pwrs⌝ + else own_replica_ptsm_sptsm rp ptsm sptsm + }}}. + Proof. + iIntros (Hvw ts Φ) "[[HpwrsS %HpwrsL] Hrp] HΦ". + wp_rec. + iDestruct (own_replica_ptsm_sptsm_dom with "Hrp") as %[Hdomptsm Hdomsptsm]. + + (*@ func (rp *Replica) acquire(ts uint64, pwrs []tulip.WriteEntry) bool { @*) + (*@ // Check if all keys are writable. @*) + (*@ var pos uint64 = 0 @*) + (*@ @*) + wp_apply (wp_ref_to); first by auto. + iIntros (posP) "HposP". + wp_pures. + + (*@ for pos < uint64(len(pwrs)) { @*) + (*@ ent := pwrs[pos] @*) + (*@ writable := rp.writableKey(ts, ent.Key) @*) + (*@ if !writable { @*) + (*@ break @*) + (*@ } @*) + (*@ pos++ @*) + (*@ } @*) + (*@ @*) + iDestruct (own_slice_sz with "HpwrsS") as %Hlen. + iDestruct (own_slice_small_acc with "HpwrsS") as "[HpwrsS HpwrsC]". + set P := (λ (cont : bool), ∃ (pos : u64), + let pwrs' := list_to_map (take (uint.nat pos) pwrsL) in + "HpwrsS" ∷ own_slice_small pwrsS (struct.t WriteEntry) (DfracOwn 1) pwrsL ∗ + "HposP" ∷ posP ↦[uint64T] #pos ∗ + "Hrp" ∷ own_replica_ptsm_sptsm rp ptsm sptsm ∗ + "%Hptsm" ∷ ⌜validated_ptsm ptsm pwrs'⌝ ∗ + "%Hsptsm" ∷ ⌜validated_sptsm sptsm ts pwrs'⌝)%I. + wp_apply (wp_forBreak_cond P with "[] [HpwrsS HposP Hrp]"); last first; first 1 last. + { (* Loop entry. *) + iExists (W64 0). + rewrite uint_nat_W64_0 take_0 list_to_map_nil. + iFrame. + iPureIntro. + (* split; first done. *) + split. + { rewrite /validated_ptsm dom_empty_L. + intros k n Hn. + by apply map_lookup_filter_Some in Hn as [_ ?]. + } + { rewrite /validated_sptsm dom_empty_L. + intros k n Hn. + by apply map_lookup_filter_Some in Hn as [_ ?]. + } + } + { (* Loop body. *) + clear Φ. iIntros (Φ) "!> HP HΦ". iNamed "HP". + wp_load. + wp_apply (wp_slice_len). + wp_if_destruct; last first. + { (* Exit from the loop condition. *) + iApply "HΦ". + iExists pos. + by iFrame "∗ %". + } + wp_load. + destruct (lookup_lt_is_Some_2 pwrsL (uint.nat pos)) as [[k v] Hwr]; first word. + wp_apply (wp_SliceGet with "[$HpwrsS]"); first done. + iIntros "HpwrsL". + wp_pures. + wp_apply (wp_Replica__writableKey with "Hrp"). + { rewrite -HpwrsL in Hwr. + apply elem_of_list_lookup_2, elem_of_map_to_list, elem_of_dom_2 in Hwr. + clear -Hvw Hwr. set_solver. + } + iIntros (ok) "[Hrp %Hwritable]". + wp_pures. + destruct ok; wp_pures; last first. + { iApply "HΦ". + by iFrame "∗ %". + } + wp_load. + wp_store. + iApply "HΦ". + iFrame "∗ %". + iPureIntro. + rewrite uint_nat_word_add_S; last word. + rewrite (take_S_r _ _ _ Hwr) list_to_map_snoc; last first. + { by eapply map_to_list_not_elem_of_take_key. } + split. + { intros x n Hn. + apply map_lookup_filter_Some in Hn as [Hn Hx]. + rewrite /= dom_insert_L elem_of_union in Hx. + destruct Hx as [Hx | Hx]; last first. + { specialize (Hptsm x n). simpl in Hptsm. + apply Hptsm. + by apply map_lookup_filter_Some. + } + rewrite elem_of_singleton in Hx. subst x. + destruct Hwritable as [Hwritable _]. + by rewrite /key_writable_ptsm Hn in Hwritable. + } + { intros x n Hn. + apply map_lookup_filter_Some in Hn as [Hn Hx]. + rewrite /= dom_insert_L elem_of_union in Hx. + destruct Hx as [Hx | Hx]; last first. + { specialize (Hsptsm x n). simpl in Hsptsm. + apply Hsptsm. + by apply map_lookup_filter_Some. + } + rewrite elem_of_singleton in Hx. subst x. + destruct Hwritable as [_ Hwritable]. + by rewrite /key_writable_sptsm Hn in Hwritable. + } + } + iNamed 1. clear P. + + (*@ // Report error if some key cannot be locked. @*) + (*@ if pos < uint64(len(pwrs)) { @*) + (*@ return false @*) + (*@ } @*) + (*@ @*) + wp_load. + wp_apply wp_slice_len. + wp_if_destruct. + { iDestruct ("HpwrsC" with "HpwrsS") as "HpwrsS". + iApply "HΦ". + by iFrame "∗ %". + } + rewrite take_ge in Hptsm, Hsptsm; last word. + rewrite -HpwrsL list_to_map_to_list in Hptsm, Hsptsm. + + (*@ // Acquire locks for each key. @*) + (*@ for _, ent := range(pwrs) { @*) + (*@ rp.acquireKey(ts, ent.Key) @*) + (*@ } @*) + (*@ @*) + set P := (λ (i : u64), + let pwrs' := list_to_map (take (uint.nat i) pwrsL) in + own_replica_ptsm_sptsm rp (acquire ts pwrs' ptsm) (acquire ts pwrs' sptsm))%I. + wp_apply (wp_forSlice P with "[] [$HpwrsS Hrp]"); last first; first 1 last. + { (* Loop entry. *) + subst P. simpl. + by rewrite uint_nat_W64_0 take_0 list_to_map_nil /acquire 2!setts_empty. + } + { (* Loop body. *) + clear Φ. + iIntros (i [k v]) "!>". + iIntros (Φ) "(Hrp & %Hbound & %Hi) HΦ". + subst P. simpl. + wp_pures. + wp_apply (wp_Replica__acquireKey with "Hrp"). + iIntros "Hrp". + iApply "HΦ". + rewrite uint_nat_word_add_S; last word. + rewrite (take_S_r _ _ _ Hi) list_to_map_snoc; last first. + { by eapply map_to_list_not_elem_of_take_key. } + rewrite /acquire setts_insert; last first. + { rewrite -HpwrsL in Hi. + apply elem_of_list_lookup_2, elem_of_map_to_list, elem_of_dom_2 in Hi. + clear -Hvw Hi Hdomptsm. set_solver. + } + rewrite /acquire setts_insert; last first. + { rewrite -HpwrsL in Hi. + apply elem_of_list_lookup_2, elem_of_map_to_list, elem_of_dom_2 in Hi. + clear -Hvw Hi Hdomsptsm. set_solver. + } + done. + } + iIntros "[HP HpwrsS]". + iNamed "HP". clear P. + rewrite -Hlen firstn_all -HpwrsL list_to_map_to_list in Hptsmabs, Hsptsmabs. + + (*@ return true @*) + (*@ } @*) + wp_pures. + iDestruct ("HpwrsC" with "HpwrsS") as "HpwrsS". + iApply "HΦ". + by iFrame "HptsmP HsptsmP ∗ %". + Qed. + +End program. diff --git a/src/program_proof/tulip/program/replica/replica_acquire_key.v b/src/program_proof/tulip/program/replica/replica_acquire_key.v new file mode 100644 index 000000000..0cb4da4ce --- /dev/null +++ b/src/program_proof/tulip/program/replica/replica_acquire_key.v @@ -0,0 +1,49 @@ +From Perennial.program_proof.tulip.program Require Import prelude. +From Perennial.program_proof.tulip.program Require Import replica_repr. + +Section program. + Context `{!heapGS Σ, !tulip_ghostG Σ}. + + Theorem wp_Replica__acquireKey rp (ts : u64) key ptsm sptsm : + {{{ own_replica_ptsm_sptsm rp ptsm sptsm }}} + Replica__acquireKey #rp #ts #(LitString key) + {{{ RET #(); + own_replica_ptsm_sptsm rp (<[key := uint.nat ts]> ptsm) (<[key := uint.nat ts]> sptsm) + }}}. + Proof. + iIntros (Φ) "Hrp HΦ". + wp_rec. + + (*@ func (rp *Replica) acquireKey(ts uint64, key string) { @*) + (*@ rp.ptsm[key] = ts @*) + (*@ rp.sptsm[key] = ts @*) + (*@ } @*) + iNamed "Hrp". + wp_loadField. + wp_apply (wp_MapInsert with "HptsmM"); first done. + iIntros "HptsmM". + wp_loadField. + wp_apply (wp_MapInsert with "HsptsmM"); first done. + iIntros "HsptsmM". + wp_pures. + iApply "HΦ". + iFrame "HptsmP HsptsmP ∗". + iPureIntro. + split. + { intros k Hk. + destruct (decide (k = key)) as [-> | Hne]; last first. + { do 2 (rewrite lookup_insert_ne; last done). + by apply Hptsmabs. + } + by rewrite 2!lookup_insert. + } + { intros k Hk. + destruct (decide (k = key)) as [-> | Hne]; last first. + { do 2 (rewrite lookup_insert_ne; last done). + by apply Hsptsmabs. + } + by rewrite 2!lookup_insert. + } + Qed. + +End program. diff --git a/src/program_proof/tulip/program/replica/replica_bump_key.v b/src/program_proof/tulip/program/replica/replica_bump_key.v new file mode 100644 index 000000000..0dd4921dd --- /dev/null +++ b/src/program_proof/tulip/program/replica/replica_bump_key.v @@ -0,0 +1,120 @@ +From Perennial.program_proof.tulip.program Require Import prelude. +From Perennial.program_proof.tulip.program Require Import replica_repr. + +Section program. + Context `{!heapGS Σ, !tulip_ghostG Σ}. + + Theorem wp_Replica__bumpKey rp (ts : u64) key ptsm sptsm : + uint.Z ts ≠ 0 -> + key ∈ keys_all -> + {{{ own_replica_ptsm_sptsm rp ptsm sptsm }}} + Replica__bumpKey #rp #ts #(LitString key) + {{{ (spts : nat), RET #(bool_decide (spts < pred (uint.nat ts))%nat); + own_replica_ptsm_sptsm rp ptsm (<[key := (spts `max` pred (uint.nat ts))%nat]> sptsm) ∗ + ⌜sptsm !! key = Some spts⌝ + }}}. + Proof. + iIntros (Htsnz Hkey Φ) "Hrp HΦ". + wp_rec. + + (*@ func (rp *Replica) bumpKey(ts uint64, key string) bool { @*) + (*@ spts := rp.sptsm[key] @*) + (*@ if ts - 1 <= spts { @*) + (*@ return false @*) + (*@ } @*) + (*@ rp.sptsm[key] = ts - 1 @*) + (*@ return true @*) + (*@ } @*) + iNamed "Hrp". + wp_loadField. + wp_apply (wp_MapGet with "HsptsmM"). + iIntros (sptsW ok) "[%Hspts HsptsmM]". + wp_pures. + case_bool_decide as Hcond; wp_pures. + { rewrite word.unsigned_sub_nowrap in Hcond; last word. + destruct ok. + { apply map_get_true in Hspts. + iSpecialize ("HΦ" $! (uint.nat sptsW)). + case_bool_decide as Hts; first word. + iApply "HΦ". + iFrame "HptsmP HsptsmP ∗ %". + iPureIntro. + split; last first. + { specialize (Hsptsmabs _ Hkey). + by rewrite Hspts in Hsptsmabs. + } + intros k Hk. + destruct (decide (k = key)) as [-> | Hne]; last first. + { rewrite lookup_insert_ne; last done. + by apply Hsptsmabs. + } + rewrite lookup_insert Hspts. + f_equal. + clear -Hts. word. + } + { apply map_get_false in Hspts as [Hspts ->]. + simpl in Hcond. + iSpecialize ("HΦ" $! O). + case_bool_decide as Hts; first word. + assert (uint.Z ts = 1) by word. + iApply "HΦ". + iFrame "HptsmP HsptsmP ∗ %". + iPureIntro. + assert (Hz : sptsm !! key = Some O). + { specialize (Hsptsmabs _ Hkey). + by rewrite Hspts in Hsptsmabs. + } + split; last apply Hz. + replace (_ `max` _)%nat with O; last word. + by rewrite insert_id. + } + } + rewrite word.unsigned_sub_nowrap in Hcond; last word. + wp_loadField. + wp_apply (wp_MapInsert with "HsptsmM"); first done. + iIntros "HsptsmM". + wp_pures. + destruct ok. + { apply map_get_true in Hspts. + iSpecialize ("HΦ" $! (uint.nat sptsW)). + case_bool_decide as Hts; last word. + iApply "HΦ". + iFrame "HptsmP HsptsmP ∗ %". + iPureIntro. + split; last first. + { specialize (Hsptsmabs _ Hkey). + by rewrite Hspts in Hsptsmabs. + } + intros k Hk. + destruct (decide (k = key)) as [-> | Hne]; last first. + { do 2 (rewrite lookup_insert_ne; last done). + by apply Hsptsmabs. + } + rewrite 2!lookup_insert. + f_equal. + clear -Hcond. word. + } + { apply map_get_false in Hspts as [Hspts ->]. + simpl in Hcond. + iSpecialize ("HΦ" $! O). + case_bool_decide as Hts; last word. + { iApply "HΦ". + assert (Hsptsmkey : sptsm !! key = Some O). + { specialize (Hsptsmabs _ Hkey). + by rewrite Hspts in Hsptsmabs. + } + iFrame "HptsmP HsptsmP ∗ %". + iPureIntro. + intros k Hk. + destruct (decide (k = key)) as [-> | Hne]; last first. + { do 2 (rewrite lookup_insert_ne; last done). + by apply Hsptsmabs. + } + rewrite 2!lookup_insert. + f_equal. + word. + } + } + Qed. + +End program. diff --git a/src/program_proof/tulip/program/replica/replica_finalized.v b/src/program_proof/tulip/program/replica/replica_finalized.v new file mode 100644 index 000000000..e69de29bb diff --git a/src/program_proof/tulip/program/replica/replica_last_proposal.v b/src/program_proof/tulip/program/replica/replica_last_proposal.v new file mode 100644 index 000000000..6e7e25bd6 --- /dev/null +++ b/src/program_proof/tulip/program/replica/replica_last_proposal.v @@ -0,0 +1,49 @@ +From Perennial.program_proof.tulip.program Require Import prelude replica_repr. + +Section program. + Context `{!heapGS Σ, !tulip_ghostG Σ}. + + Theorem wp_Replica__lastProposal rp (tsW : u64) psm rkm : + let ts := uint.nat tsW in + {{{ own_replica_psm_rkm rp psm rkm }}} + Replica__lastProposal #rp #tsW + {{{ (rank : u64) (pdec : bool) (ok : bool), RET (#rank, #pdec, #ok); + own_replica_psm_rkm rp psm rkm ∗ + ⌜if ok then psm !! ts = Some (uint.nat rank, pdec) else psm !! ts = None⌝ + }}}. + Proof. + iIntros (ts Φ) "Hrp HΦ". + wp_rec. + + (*@ func (rp *Replica) lastProposal(ts uint64) (uint64, bool, bool) { @*) + (*@ ps, ok := rp.pstbl[ts] @*) + (*@ return ps.rank, ps.dec, ok @*) + (*@ } @*) + iNamed "Hrp". + wp_loadField. + wp_apply (wp_MapGet with "Hpstbl"). + iIntros (psl ok) "[%Hok Hpstbl]". + wp_pures. + iApply "HΦ". + iFrame "∗ %". + iPureIntro. + destruct ok. + { apply map_get_true in Hok. + assert (Hpstbl : fmap ppsl_to_nat_bool pstbl !! tsW = Some (uint.nat psl.1, psl.2)). + { by rewrite lookup_fmap Hok. } + symmetry in Hpsmabs. + pose proof (lookup_kmap_eq_Some _ _ _ _ _ _ Hpsmabs Hpstbl) as (ts' & Hts' & Hpsmts). + assert (ts' = ts) as ->. + { subst ts. rewrite Hts'. lia. } + done. + } + { apply map_get_false in Hok as [Hnone _]. + assert (Hpstbl : fmap ppsl_to_nat_bool pstbl !! tsW = None). + { by rewrite lookup_fmap Hnone. } + symmetry in Hpsmabs. + apply (lookup_kmap_eq_None _ _ _ _ _ Hpsmabs Hpstbl). + word. + } + Qed. + +End program. diff --git a/src/program_proof/tulip/program/replica/replica_lowest_rank.v b/src/program_proof/tulip/program/replica/replica_lowest_rank.v new file mode 100644 index 000000000..d7b01802c --- /dev/null +++ b/src/program_proof/tulip/program/replica/replica_lowest_rank.v @@ -0,0 +1,49 @@ +From Perennial.program_proof.tulip.program Require Import prelude replica_repr. + +Section program. + Context `{!heapGS Σ, !tulip_ghostG Σ}. + + Theorem wp_Replica__lowestRank rp (tsW : u64) psm rkm : + let ts := uint.nat tsW in + {{{ own_replica_psm_rkm rp psm rkm }}} + Replica__lowestRank #rp #tsW + {{{ (rank : u64) (ok : bool), RET (#rank, #ok); + own_replica_psm_rkm rp psm rkm ∗ + ⌜if ok then rkm !! ts = Some (uint.nat rank) else rkm !! ts = None⌝ + }}}. + Proof. + iIntros (ts Φ) "Hrp HΦ". + wp_rec. + + (*@ func (rp *Replica) lowestRank(ts uint64) (uint64, bool) { @*) + (*@ rank, ok := rp.rktbl[ts] @*) + (*@ return rank, ok @*) + (*@ } @*) + iNamed "Hrp". + wp_loadField. + wp_apply (wp_MapGet with "Hrktbl"). + iIntros (rankW ok) "[%Hok Hrktbl]". + wp_pures. + iApply "HΦ". + iFrame "∗ %". + iPureIntro. + destruct ok. + { apply map_get_true in Hok. + assert (Hrktbl : fmap (λ x, uint.nat x) rktbl !! tsW = Some (uint.nat rankW)). + { by rewrite lookup_fmap Hok. } + symmetry in Hrkmabs. + pose proof (lookup_kmap_eq_Some _ _ _ _ _ _ Hrkmabs Hrktbl) as (ts' & Hts' & Hrkmts). + assert (ts' = ts) as ->. + { subst ts. rewrite Hts'. lia. } + done. + } + { apply map_get_false in Hok as [Hnone _]. + assert (Hrktbl : fmap (λ x, uint.nat x) rktbl !! tsW = None). + { by rewrite lookup_fmap Hnone. } + symmetry in Hrkmabs. + apply (lookup_kmap_eq_None _ _ _ _ _ Hrkmabs Hrktbl). + word. + } + Qed. + +End program. diff --git a/src/program_proof/tulip/program/replica/replica_readable_key.v b/src/program_proof/tulip/program/replica/replica_readable_key.v new file mode 100644 index 000000000..1fdabe7e0 --- /dev/null +++ b/src/program_proof/tulip/program/replica/replica_readable_key.v @@ -0,0 +1,63 @@ +From Perennial.program_proof.tulip.program Require Import prelude. +From Perennial.program_proof.tulip.program Require Import replica_repr. + +Section program. + Context `{!heapGS Σ, !tulip_ghostG Σ}. + + Definition key_readable (ptsm : gmap dbkey nat) (ts : nat) (key : dbkey) := + match ptsm !! key with + | Some pts => pts = O ∨ (ts < pts)%nat + | _ => False + end. + + Theorem wp_Replica__readableKey rp (ts : u64) key ptsm sptsm : + key ∈ keys_all -> + {{{ own_replica_ptsm_sptsm rp ptsm sptsm }}} + Replica__readableKey #rp #ts #(LitString key) + {{{ (ok : bool), RET #ok; + own_replica_ptsm_sptsm rp ptsm sptsm ∗ + ⌜if ok then key_readable ptsm (uint.nat ts) key else True⌝ + }}}. + Proof. + iIntros (Hkey Φ) "Hrp HΦ". + wp_rec. + + (*@ func (rp *Replica) readableKey(ts uint64, key string) bool { @*) + (*@ pts := rp.ptsm[key] @*) + (*@ if pts != 0 && pts <= ts { @*) + (*@ return false @*) + (*@ } @*) + (*@ @*) + iNamed "Hrp". + wp_loadField. + wp_apply (wp_MapGet with "HptsmM"). + iIntros (pts ok) "[%Hpts HptsmM]". + wp_apply wp_and_pure. + { wp_pures. by rewrite -bool_decide_not. } + { iIntros (_). by wp_pures. } + case_bool_decide as Hcond; wp_pures. + { iApply "HΦ". by iFrame. } + + (*@ return true @*) + (*@ } @*) + iApply "HΦ". + apply Classical_Prop.not_and_or in Hcond. + assert (Hreadable : key_readable ptsm (uint.nat ts) key). + { specialize (Hptsmabs _ Hkey). + destruct ok. + { apply map_get_true in Hpts. + rewrite Hpts in Hptsmabs. + rewrite /key_readable Hptsmabs. + destruct Hcond as [Hz | Hlt]. + { left. apply dec_stable in Hz. inv Hz. by rewrite uint_nat_W64_0. } + { right. clear -Hlt. word. } + } + apply map_get_false in Hpts as [Hpts _]. + rewrite Hpts in Hptsmabs. + rewrite /key_readable Hptsmabs. + by left. + } + by iFrame. + Qed. + +End program. diff --git a/src/program_proof/tulip/program/replica/replica_release_key.v b/src/program_proof/tulip/program/replica/replica_release_key.v new file mode 100644 index 000000000..7e05cedd7 --- /dev/null +++ b/src/program_proof/tulip/program/replica/replica_release_key.v @@ -0,0 +1,36 @@ +From Perennial.program_proof.tulip.program Require Import prelude. +From Perennial.program_proof.tulip.program Require Import replica_repr. + +Section program. + Context `{!heapGS Σ, !tulip_ghostG Σ}. + + Theorem wp_Replica__releaseKey rp key ptsm sptsm : + {{{ own_replica_ptsm_sptsm rp ptsm sptsm }}} + Replica__releaseKey #rp #(LitString key) + {{{ RET #(); + own_replica_ptsm_sptsm rp (<[key := O]> ptsm) sptsm + }}}. + Proof. + iIntros (Φ) "Hrp HΦ". + wp_rec. + (*@ func (rp *Replica) releaseKey(key string) { @*) + (*@ delete(rp.ptsm, key) @*) + (*@ } @*) + iNamed "Hrp". + wp_loadField. + wp_apply (wp_MapDelete with "HptsmM"). + iIntros "HptsmM". + wp_pures. + iApply "HΦ". + iFrame "∗ %". + iPureIntro. + intros k Hk. + destruct (decide (k = key)) as [-> | Hne]; last first. + { rewrite lookup_delete_ne; last done. + rewrite lookup_insert_ne; last done. + by apply Hptsmabs. + } + by rewrite lookup_delete lookup_insert. + Qed. + +End program. diff --git a/src/program_proof/tulip/program/replica/replica_repr.v b/src/program_proof/tulip/program/replica/replica_repr.v new file mode 100644 index 000000000..d3a33b6ec --- /dev/null +++ b/src/program_proof/tulip/program/replica/replica_repr.v @@ -0,0 +1,118 @@ +From Perennial.program_proof.tulip.program Require Import prelude. + +Inductive rpres := +| ReplicaOK +| ReplicaCommittedTxn +| ReplicaAbortedTxn +| ReplicaStaleCoordinator +| ReplicaFailedValidation +| ReplicaInvalidRank +| ReplicaWrongLeader. + +Definition rpres_to_u64 (r : rpres) := + match r with + | ReplicaOK => (U64 0) + | ReplicaCommittedTxn => (U64 1) + | ReplicaAbortedTxn => (U64 2) + | ReplicaStaleCoordinator => (U64 3) + | ReplicaFailedValidation => (U64 4) + | ReplicaInvalidRank => (U64 5) + | ReplicaWrongLeader => (U64 6) + end. + +Section repr. + Context `{!heapGS Σ, !tulip_ghostG Σ}. + + (*@ type Replica struct { @*) + (*@ // Mutex. @*) + (*@ mu *sync.Mutex @*) + (*@ // Replica ID. @*) + (*@ rid uint64 @*) + (*@ // Replicated transaction log. @*) + (*@ txnlog *txnlog.TxnLog @*) + (*@ // @*) + (*@ // Fields below are application states. @*) + (*@ // @*) + (*@ // LSN up to which all commands have been applied. @*) + (*@ lsna uint64 @*) + (*@ // Write sets of validated transactions. @*) + (*@ prepm map[uint64][]tulip.WriteEntry @*) + (*@ // Participant groups of validated transactions. @*) + (*@ ptgsm map[uint64][]uint64 @*) + (*@ // Prepare status table. @*) + (*@ pstbl map[uint64]PrepareStatusEntry @*) + (*@ // Transaction status table; mapping from transaction timestamps to their @*) + (*@ // commit/abort status. @*) + (*@ txntbl map[uint64]bool @*) + (*@ // Mapping from keys to their prepare timestamps. @*) + (*@ ptsm map[string]uint64 @*) + (*@ // Mapping from keys to their smallest preparable timestamps. @*) + (*@ sptsm map[string]uint64 @*) + (*@ // Index. @*) + (*@ idx *index.Index @*) + (*@ // @*) + (*@ // Fields below are group info initialized after creation of all replicas. @*) + (*@ // @*) + (*@ // Replicas in the same group. Read-only. @*) + (*@ rps map[uint64]grove_ffi.Address @*) + (*@ // ID of the replica believed to be the leader of this group. Used to @*) + (*@ // initialize backup coordinators. @*) + (*@ leader uint64 @*) + (*@ } @*) + Definition own_replica_cm (rp : loc) (cm : gmap nat bool) : iProp Σ := + ∃ (txntblP : loc) (txntbl : gmap u64 bool), + "HtxntblP" ∷ rp ↦[Replica :: "txntbl"] #txntblP ∗ + "Htxntbl" ∷ own_map txntblP (DfracOwn 1) txntbl ∗ + "%Hcmabs" ∷ ⌜(kmap Z.of_nat cm : gmap Z bool) = kmap uint.Z txntbl⌝. + + Definition own_replica_cpm (rp : loc) (cpm : gmap nat dbmap) : iProp Σ := + ∃ (prepmP : loc) (prepmS : gmap u64 Slice.t) (prepm : gmap u64 dbmap), + "HprepmP" ∷ rp ↦[Replica :: "prepm"] #prepmP ∗ + "HprepmS" ∷ own_map prepmP (DfracOwn 1) prepmS ∗ + "Hprepm" ∷ ([∗ map] s; m ∈ prepmS; prepm, ∃ l, own_dbmap_in_slice s l m) ∗ + "%Hcpmabs" ∷ ⌜(kmap Z.of_nat cpm : gmap Z dbmap) = kmap uint.Z prepm⌝. + + Definition absrel_ptsm (ptsm : gmap dbkey nat) (ptsmM : gmap dbkey u64) := + ∀ k, + k ∈ keys_all -> + match ptsmM !! k with + | Some ptsW => ptsm !! k = Some (uint.nat ptsW) + | _ => ptsm !! k = Some O + end. + + Definition own_replica_ptsm_sptsm + (rp : loc) (ptsm sptsm : gmap dbkey nat) : iProp Σ := + ∃ (ptsmP : loc) (sptsmP : loc) (ptsmM : gmap dbkey u64) (sptsmM : gmap dbkey u64), + "HptsmP" ∷ rp ↦[Replica :: "ptsm"] #ptsmP ∗ + "HsptsmP" ∷ rp ↦[Replica :: "sptsm"] #sptsmP ∗ + "HptsmM" ∷ own_map ptsmP (DfracOwn 1) ptsmM ∗ + "HsptsmM" ∷ own_map sptsmP (DfracOwn 1) sptsmM ∗ + "%Hptsmabs" ∷ ⌜absrel_ptsm ptsm ptsmM⌝ ∗ + "%Hsptsmabs" ∷ ⌜absrel_ptsm sptsm sptsmM⌝. + + Lemma own_replica_ptsm_sptsm_dom rp ptsm sptsm : + own_replica_ptsm_sptsm rp ptsm sptsm -∗ + ⌜keys_all ⊆ dom ptsm ∧ keys_all ⊆ dom sptsm⌝. + Proof. + iNamed 1. + iPureIntro. + split. + - intros k Hk. specialize (Hptsmabs _ Hk). + apply elem_of_dom. by destruct (ptsmM !! k). + - intros k Hk. specialize (Hsptsmabs _ Hk). + apply elem_of_dom. by destruct (sptsmM !! k). + Qed. + + Definition ppsl_to_nat_bool (psl : ppsl) := (uint.nat psl.1, psl.2). + + Definition own_replica_psm_rkm + (rp : loc) (psm : gmap nat (nat * bool)) (rkm : gmap nat nat) : iProp Σ := + ∃ (pstblP : loc) (rktblP : loc) (pstbl : gmap u64 ppsl) (rktbl : gmap u64 u64), + "HpstblP" ∷ rp ↦[Replica :: "pstbl"] #pstblP ∗ + "HrktblP" ∷ rp ↦[Replica :: "rktbl"] #rktblP ∗ + "Hpstbl" ∷ own_map pstblP (DfracOwn 1) pstbl ∗ + "Hrktbl" ∷ own_map rktblP (DfracOwn 1) rktbl ∗ + "%Hpsmabs" ∷ ⌜(kmap Z.of_nat psm : gmap Z (nat * bool)) = kmap uint.Z (fmap ppsl_to_nat_bool pstbl)⌝ ∗ + "%Hrkmabs" ∷ ⌜(kmap Z.of_nat rkm : gmap Z nat) = kmap uint.Z (fmap (λ x, uint.nat x) rktbl)⌝. + +End repr. diff --git a/src/program_proof/tulip/program/replica/replica_validate.v b/src/program_proof/tulip/program/replica/replica_validate.v new file mode 100644 index 000000000..e69de29bb diff --git a/src/program_proof/tulip/program/replica/replica_writable_key.v b/src/program_proof/tulip/program/replica/replica_writable_key.v new file mode 100644 index 000000000..c29ec3a76 --- /dev/null +++ b/src/program_proof/tulip/program/replica/replica_writable_key.v @@ -0,0 +1,96 @@ +From Perennial.program_proof.tulip.program Require Import prelude. +From Perennial.program_proof.tulip.program Require Import replica_repr. + +Section program. + Context `{!heapGS Σ, !tulip_ghostG Σ}. + + Definition key_writable_ptsm (ptsm : gmap dbkey nat) (key : dbkey) := + match ptsm !! key with + | Some pts => pts = O + | _ => False + end. + + Definition key_writable_sptsm (sptsm : gmap dbkey nat) (ts : nat) (key : dbkey) := + match sptsm !! key with + | Some spts => (spts < ts)%nat + | _ => False + end. + + Definition key_writable (ptsm sptsm : gmap dbkey nat) (ts : nat) (key : dbkey) := + key_writable_ptsm ptsm key ∧ key_writable_sptsm sptsm ts key. + + Theorem wp_Replica__writableKey rp (ts : u64) key ptsm sptsm : + key ∈ keys_all -> + {{{ own_replica_ptsm_sptsm rp ptsm sptsm }}} + Replica__writableKey #rp #ts #(LitString key) + {{{ (ok : bool), RET #ok; + own_replica_ptsm_sptsm rp ptsm sptsm ∗ + ⌜if ok then key_writable ptsm sptsm (uint.nat ts) key else True⌝ + }}}. + Proof. + iIntros (Hkey Φ) "Hrp HΦ". + wp_rec. + + (*@ func (rp *Replica) writableKey(ts uint64, key string) bool { @*) + (*@ // The default of prepare timestamps are 0, so no need to check existence. @*) + (*@ pts := rp.ptsm[key] @*) + (*@ if pts != 0 { @*) + (*@ return false @*) + (*@ } @*) + (*@ @*) + iNamed "Hrp". + wp_loadField. + wp_apply (wp_MapGet with "HptsmM"). + iIntros (pts okpts) "[%Hpts HptsmM]". + wp_pures. + case_bool_decide as Hptsz; wp_pures; last first. + { iApply "HΦ". by iFrame. } + + (*@ // Even though the default of smallest preparable timestamps are 1, using @*) + (*@ // the fact that @ts is positive also means no need to check existence. @*) + (*@ spts := rp.sptsm[key] @*) + + (*@ if ts <= spts { @*) + (*@ return false @*) + (*@ } @*) + (*@ @*) + wp_loadField. + wp_apply (wp_MapGet with "HsptsmM"). + iIntros (spts okspts) "[%Hspts HsptsmM]". + wp_pures. + case_bool_decide as Hgespts; wp_pures. + { iApply "HΦ". by iFrame "HptsmP HsptsmP ∗". } + + (*@ return true @*) + (*@ } @*) + iApply "HΦ". + assert (Hwritable : key_writable ptsm sptsm (uint.nat ts) key). + { inv Hptsz. + split. + { specialize (Hptsmabs _ Hkey). + destruct okpts. + { apply map_get_true in Hpts. + rewrite Hpts uint_nat_W64_0 in Hptsmabs. + by rewrite /key_writable_ptsm Hptsmabs. + } + apply map_get_false in Hpts as [Hpts _]. + rewrite Hpts in Hptsmabs. + by rewrite /key_writable_ptsm Hptsmabs. + } + { specialize (Hsptsmabs _ Hkey). + destruct okspts. + { apply map_get_true in Hspts. + rewrite Hspts in Hsptsmabs. + rewrite /key_writable_sptsm Hsptsmabs. + clear -Hgespts. word. + } + apply map_get_false in Hspts as [Hspts _]. + rewrite Hspts in Hsptsmabs. + rewrite /key_writable_sptsm Hsptsmabs. + clear -Hgespts. word. + } + } + by iFrame "HptsmP HsptsmP ∗". + Qed. + +End program. diff --git a/src/program_proof/tulip/program/tuple/tuple.v b/src/program_proof/tulip/program/tuple/tuple.v index 5ba8f6277..084e8e662 100644 --- a/src/program_proof/tulip/program/tuple/tuple.v +++ b/src/program_proof/tulip/program/tuple/tuple.v @@ -1,5 +1,4 @@ -From Perennial.program_proof.tulip Require Import prelude. -From Goose.github_com.mit_pdos.tulip Require Import tuple. +From Perennial.program_proof.tulip.program Require Import prelude. Section res. Context `{!tulip_ghostG Σ}. diff --git a/src/program_proof/tulip/program/txnlog/txnlog.v b/src/program_proof/tulip/program/txnlog/txnlog.v index ad6609330..8dbd4db62 100644 --- a/src/program_proof/tulip/program/txnlog/txnlog.v +++ b/src/program_proof/tulip/program/txnlog/txnlog.v @@ -1,26 +1,14 @@ -From Perennial.program_proof.tulip Require Import prelude. -From Goose.github_com.mit_pdos.tulip Require Import tulip txnlog. +From Perennial.program_proof.tulip.program Require Import prelude. Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Definition txnlogN := nroot .@ "txnlog". - - Definition ccommand_to_val (pwrsS : Slice.t) (c : ccommand) : val := - match c with - | CmdCommit ts _ => (#(U64 0), (#(U64 ts), (to_val pwrsS, (zero_val stringT, #())))) - | CmdAbort ts => (#(U64 1), (#(U64 ts), (Slice.nil, (zero_val stringT, #())))) - end. - - Definition own_dbmap_in_slice s (l : list dbmod) (m : dbmap) : iProp Σ := - own_slice s (struct.t WriteEntry) (DfracOwn 1) l ∗ ⌜map_to_list m = l⌝. - Definition own_pwrs_slice (pwrsS : Slice.t) (c : ccommand) : iProp Σ := match c with | CmdCommit _ pwrs => (∃ pwrsL : list dbmod, own_dbmap_in_slice pwrsS pwrsL pwrs) | _ => True end. - + Definition is_txnlog (txnlog : loc) (gid : u64) (γ : tulip_names) : iProp Σ. Admitted.