diff --git a/theories/ftlr/IsUnique.v b/theories/ftlr/IsUnique.v index e9b3ad9a..88e9b93d 100644 --- a/theories/ftlr/IsUnique.v +++ b/theories/ftlr/IsUnique.v @@ -16,761 +16,841 @@ Section fundamental. Implicit Types lw : (leibnizO LWord). Implicit Types interp : (D). - (* TODO @Bastien redo the proof in the same style as Load or Store *) - Lemma isunique_case (lregs : leibnizO LReg) - (p : Perm) (b e a : Addr) (v : Version) - (lw : LWord) (dst src : RegName) (P : D): - ftlr_instr lregs p b e a v lw (IsUnique dst src) P. + Local Hint Resolve finz_seq_between_NoDup list_remove_elem_NoDup : core. + + Definition reg_allows_sweep + (lregs : LReg) (r : RegName) + (p : Perm) (b e a : Addr) (v : Version):= + lregs !! r = Some (LCap p b e a v) ∧ readAllowed p = true. + + Definition allow_sweep_mask + (a_pc : Addr) (v_pc : Version) (la : list Addr) (v : Version): coPset := + compute_mask_region (⊤ ∖ ↑logN.@(a_pc, v_pc)) (list_remove_elem a_pc la) v. + + Lemma allow_sweep_mask_remove_nodup + (a_pc : Addr) (v_pc : Version) (la : list Addr) (v : Version) : + NoDup la -> + allow_sweep_mask a_pc v_pc (list_remove_elem a_pc la) v = + allow_sweep_mask a_pc v_pc la v. Proof. - intros Hp Hsome i Hbae Hi. - iIntros "#IH #Hinv #Hinva #Hreg #(Hread & Hwrite & %HpersP) Hown Ha HP Hcls HPC Hmap". - specialize (HpersP lw). - rewrite delete_insert_delete. - iDestruct ((big_sepM_delete _ _ PC) with "[HPC Hmap]") as "Hmap /="; - [apply lookup_insert|rewrite delete_insert_delete;iFrame|]. simpl. + intros HNoDup. + by rewrite /allow_sweep_mask list_remove_elem_idem. + Qed. - (* To read out PC's name later, and needed when calling wp_load *) - assert(∀ x : RegName, is_Some (<[PC:=LCap p b e a v]> lregs !! x)) as Hsome'. - { - intros. destruct (decide (x = PC)) as [Hx|Hx]. - rewrite Hx lookup_insert; unfold is_Some. by eexists. - by rewrite lookup_insert_ne. + Definition region_open_resources + (a_pc : Addr) (v_pc : Version) + (la : list Addr) (v : Version) + (lws : list LWord) (Ps : list D) + (has_later : bool) + : iProp Σ := + + let E := ⊤ ∖ ↑logN.@(a_pc, v_pc) in + let E' := allow_sweep_mask a_pc v_pc la v in + + ([∗ list] lw;Pw ∈ lws;Ps, (if has_later then ▷ (Pw : D) lw else (Pw : D) lw)) + ∗ ( ⌜ Persistent ([∗ list] lw;Pw ∈ lws;Ps, (Pw : D) lw) ⌝ ) + ∗ ( if has_later + then [∗ list] Pa ∈ Ps, read_cond Pa interp + else [∗ list] Pa ∈ Ps, (□ ∀ (lw : LWord), (Pa : D) lw -∗ interp lw) + )%I + ∗ ( (▷ ([∗ list] a_Pa ∈ zip la Ps, (interp_ref_inv a_Pa.1 v a_Pa.2))) ={E', E }=∗ True). + + Definition sweep_mask_cond + (lregs : LReg) (src : RegName) + (p_src : Perm) (b_src e_src a_src : Addr) (v_src : Version) + (a_pc : Addr) (v_pc : Version) := + decide (reg_allows_sweep lregs src p_src b_src e_src a_src v_src + /\ (src = PC \/ a_pc ∉ (finz.seq_between b_src e_src))). + + (* Description of what the resources are supposed to look like after opening the region *) + (* if we need to, but before closing the region up again*) + Definition allow_sweep_res + (lregs : LReg) (src : RegName) + (a_pc : Addr) (v_pc : Version) + (p_src : Perm) (b_src e_src a_src : Addr) (v_src : Version) + (Ps : list D) + := + + let la := (list_remove_elem a_pc (finz.seq_between b_src e_src)) in + let E := ⊤ ∖ ↑logN.@(a_pc, v_pc) in + let E' := allow_sweep_mask a_pc v_pc la v_src in + + (⌜read_reg_inr lregs src p_src b_src e_src a_src v_src⌝ ∗ + if sweep_mask_cond lregs src p_src b_src e_src a_src v_src a_pc v_pc + then + (|={E, E'}=> + ∃ (lws :list LWord), + ⌜ length lws = length la ⌝ + ∗ ([∗ map] la↦lw ∈ (logical_region_map la lws v_src), la ↦ₐ lw) + ∗ region_open_resources a_pc v_pc la v_src lws Ps true)%I + else True)%I. + + Lemma create_sweep_res + (lregs : LReg) (src : RegName) + (p_pc : Perm) (b_pc e_pc a_pc : Addr) (v_pc : Version) + (p_src : Perm) (b_src e_src a_src : Addr) (v_src : Version) : + + let la := (list_remove_elem a_pc (finz.seq_between b_src e_src)) in + + read_reg_inr (<[PC:=LCap p_pc b_pc e_pc a_pc v_pc]> lregs) src p_src b_src e_src a_src v_src + -> a_pc ∈ finz.seq_between b_pc e_pc + → (∀ (r : RegName) lw, ⌜r ≠ PC⌝ → ⌜lregs !! r = Some lw⌝ → (fixpoint interp1) lw) + -∗ interp (LCap p_pc b_pc e_pc a_pc v_pc) + -∗ (∃ (Ps : list D), + ⌜ length la = length Ps ⌝ + ∗ allow_sweep_res + (<[PC:=LCap p_pc b_pc e_pc a_pc v_pc]> lregs) src + a_pc v_pc + p_src b_src e_src a_src v_src Ps). + Proof. + intros * Hread Hapc_inbounds. + iIntros "#Hreg #Hinterp_pc". + apply list_remove_elem_in in Hapc_inbounds. + destruct Hapc_inbounds as (la' & <- & Hapc_inbounds). + rewrite /allow_sweep_res /sweep_mask_cond. + case_decide as Hallows; cycle 1. + { iExists (repeat (λne _, True%I) (length la)); iFrame "%". + by rewrite repeat_length. } + iFrame "%". + cbn in Hapc_inbounds. + apply bind_Some in Hapc_inbounds. + destruct Hapc_inbounds as (? & Hrem & ?) ; simplify_eq. + rewrite /reg_allows_sweep in Hallows. + destruct Hallows as ( (Hreg & HreadAllowed) & Hdecide). + assert (la ⊆+ finz.seq_between b_src e_src) + as Hla_subseteq by apply list_remove_elem_submsteq. + assert (NoDup la) as Hla_NoDup by (by apply list_remove_elem_NoDup). + rewrite /read_reg_inr in Hread; simplify_map_eq. + + destruct (decide (src = PC)) as [-> | Hneq_src_pc] ; simplify_map_eq. + (* src = PC *) + - rewrite /allow_sweep_mask. + rewrite list_remove_elem_idem; last done. + iDestruct (interp_open_region $ (⊤ ∖ ↑logN.@(a_src, v_src)) with "Hinterp_pc") + as (Ps) "[%Hlen_Ps Hmod]" ; eauto. + { eapply Forall_forall. intros a' Ha'. + subst la. + eapply namespaces.coPset_subseteq_difference_r; auto. + assert (a' ≠ a_src). + { + eapply list_remove_elem_neq; cycle 1 ; eauto. + apply list_remove_Some in Hrem. + setoid_rewrite Hrem; set_solver. + } + solve_ndisj. + } + iExists Ps. + iSplit ; first by subst. + iMod "Hmod". + iDestruct "Hmod" as (lws) "(%Hlws & %Hpers & Hmem & HPs & HPs' & Hclose)". + iExists lws. + iFrame; iFrame "%". + iModIntro. + iIntros "H". + iDestruct ("Hclose" with "H") as "Hclose". + rewrite /allow_sweep_mask. + rewrite list_remove_elem_notin. + subst la. + iFrame. + apply not_elemof_list_remove_elem; done. + + (* src ≠ PC *) + - destruct Hdecide as [Hcontra|Ha_notin_rem] ; first contradiction. + iAssert (interp (LCap p_src b_src e_src a_src v_src)) as "#Hinterp_src" + ; first (iApply "Hreg"; eauto). + iDestruct (interp_open_region $ (⊤ ∖ ↑logN.@(a_pc, v_pc)) with "Hinterp_src") + as (Ps) "[%Hlen_Ps Hmod]" ; eauto. + { apply Forall_forall; intros a' Ha'. + subst la. + assert (a' ≠ a_pc). + { intro ; subst. by apply not_elemof_list_remove_elem in Ha'. } + apply namespaces.coPset_subseteq_difference_r; [solve_ndisj|set_solver]. + } + iExists Ps. + iSplit ; first by subst. + iMod "Hmod". + rewrite allow_sweep_mask_remove_nodup; auto. + iDestruct "Hmod" as (lws) "(%Hlws & %Hpers & Hmem & HPs & HPs' & Hclose)". + iExists lws. + iFrame; iFrame "%". + iModIntro. + iIntros "H". + iDestruct ("Hclose" with "H") as "Hclose". + by rewrite allow_sweep_mask_remove_nodup. + Qed. - (* Initializing the names for the values of Hsrc now, to instantiate the existentials in step 1 *) - assert (∃ p0 b0 e0 a0 v0, read_reg_inr (<[PC:=LCap p b e a v]> lregs) src p0 b0 e0 a0 v0) - as (p0 & b0 & e0 & a0 & v0 & HVsrc). - { - specialize Hsome' with src as Hsrc. - destruct Hsrc as [wsrc Hsomesrc]. - unfold read_reg_inr. rewrite Hsomesrc. - destruct wsrc as [|[ p0 b0 e0 a0 v0|] | ]; try done. - by repeat eexists. - } + Definition allow_sweep_mem + (lmem : LMem) (lregs : LReg) (src : RegName) + (a_pc : Addr) (v_pc : Version) (lw_pc : LWord) + (p_src : Perm) (b_src e_src a_src : Addr) (v_src : Version) + (Ps : list D) (has_later : bool) := + + let la := (list_remove_elem a_pc (finz.seq_between b_src e_src)) in + + (⌜read_reg_inr lregs src p_src b_src e_src a_src v_src⌝ ∗ + if sweep_mask_cond lregs src p_src b_src e_src a_src v_src a_pc v_pc + then (∃ (lws : list LWord), + ⌜length lws = length la⌝ + ∗ ⌜lmem = <[(a_pc, v_pc):=lw_pc]> (logical_region_map la lws v_src)⌝ + ∗ region_open_resources a_pc v_pc la v_src lws Ps has_later) + else ⌜lmem = <[(a_pc, v_pc):=lw_pc]> ∅⌝)%I. + + + Lemma sweep_res_implies_mem_map + (lregs : LReg) (src : RegName) + (a_pc : Addr) (v_pc : Version) (lw_pc : LWord) + (p_src : Perm) (b_src e_src a_src : Addr) (v_src : Version) + (Ps : list D) : + + let la := list_remove_elem a_pc (finz.seq_between b_src e_src) in + let E := ⊤ ∖ ↑logN.@(a_pc, v_pc) in + let E' := allow_sweep_mask a_pc v_pc la v_src in + + allow_sweep_res lregs src a_pc v_pc p_src b_src e_src a_src v_src Ps + -∗ (a_pc, v_pc) ↦ₐ lw_pc + ={ E, + if sweep_mask_cond lregs src p_src b_src e_src a_src v_src a_pc v_pc + then E' + else E + }=∗ + ∃ lmem : LMem, + allow_sweep_mem lmem lregs src a_pc v_pc lw_pc p_src b_src e_src a_src v_src Ps true + ∗ ▷ ([∗ map] la↦lw ∈ lmem, la ↦ₐ lw). + Proof. + intros *. + iIntros "HSweepRes Ha_pc". + iDestruct "HSweepRes" as "(%Hread & HSweepRes)". + subst E'. + rewrite /sweep_mask_cond. + case_decide as Hallows; cycle 1. + - iExists _. + iSplitR "Ha_pc". + + iFrame "%". + rewrite /sweep_mask_cond; case_decide; first by exfalso. auto. + + iModIntro; iNext. by iApply memMap_resource_1. + - iMod "HSweepRes" as (lws) "(%Hlws & Hmem & HSweepRest)". + iExists _. + iSplitL "HSweepRest". + * iFrame "%". + rewrite decide_True; auto. + * iModIntro;iNext. + destruct Hallows as ((Hrinr & Hra) & Hne). + iDestruct (big_sepM_insert with "[$Hmem $Ha_pc]") as "Hmem" ; cycle 1 ; auto. + rewrite /logical_region_map. + apply not_elem_of_list_to_map_1. + rewrite fst_zip. + 2: { rewrite Hlws /logical_region fmap_length; lia. } + rewrite /logical_region. + intro Hcontra. clear -Hcontra. + eapply elem_of_list_fmap_2 in Hcontra. + destruct Hcontra as (a & Heq & Hcontra) ; simplify_eq. + apply not_elemof_list_remove_elem in Hcontra; auto. + Qed. - destruct (decide (PC = src)) as [?|Hsrc_neq_pc]; simplify_map_eq. - - rewrite /read_reg_inr in HVsrc; simplify_map_eq. - assert (readAllowed p0) as Hread_p0 by (destruct p0 ; destruct Hp ; done). - iDestruct (read_allowed_region_inv with "Hinv") as "Hread_pc" ;eauto. + Lemma mem_map_implies_pure_conds + (lmem : LMem) (lregs : LReg) (src : RegName) + (a_pc : Addr) (v_pc : Version) (lw_pc : LWord) + (p_src : Perm) (b_src e_src a_src : Addr) (v_src : Version) + (Ps : list D) (has_later : bool) : + allow_sweep_mem lmem lregs src a_pc v_pc lw_pc p_src b_src e_src a_src v_src Ps has_later + -∗ ⌜lmem !! (a_pc, v_pc) = Some lw_pc⌝. + Proof. + iIntros "(% & HSweepRes)". + rewrite /sweep_mask_cond. + case_decide as Hallows. + - pose (Hallows' := Hallows). + destruct Hallows' as ((Hreg & Hread) & Hdecide). + iDestruct "HSweepRes" as (lws) "(%Hlen & -> & HSweepRest)". + by simplify_map_eq. + - iDestruct "HSweepRes" as "->". + by simplify_map_eq. + Qed. + Lemma allow_sweep_mem_later + (lmem : LMem) (lregs : LReg) (src : RegName) + (a_pc : Addr) (v_pc : Version) (lw_pc : LWord) + (p_src : Perm) (b_src e_src a_src : Addr) (v_src : Version) + (Ps : list D) : + allow_sweep_mem lmem lregs src a_pc v_pc lw_pc p_src b_src e_src a_src v_src Ps true + -∗ ▷ allow_sweep_mem lmem lregs src a_pc v_pc lw_pc p_src b_src e_src a_src v_src Ps false. + Proof. + iIntros "[% HSweepMem]". + rewrite !/allow_sweep_mem /= /sweep_mask_cond. iSplit;[auto|]. + case_decide. + - iApply later_exist_2. iDestruct "HSweepMem" as (lws) "(%&%&HSweepRest)". + iExists lws. + iDestruct "HSweepRest" as "(?&?&?&?)"; iFrame "%∗"; iNext ; iFrame. + - iNext; iFrame. + Qed. - apply le_addr_withinBounds', withinBounds_in_seq_1 in Hbae. - odestruct (list_remove_elem_in _ _ Hbae) as (la' & <- & Hla'). - set (la' := list_remove_elem a0 (finz.seq_between b0 e0)). - assert (NoDup la') as HNoDup_la'. - { eapply list_remove_elem_NoDup; eauto. apply finz_seq_between_NoDup. } - assert (a0 ∉ la') as Ha0_notin_la'. - { eapply not_elemof_list_remove_elem ; cycle 2 ; eauto. - apply finz_seq_between_NoDup. + Lemma mem_map_recover_res_no_update + (lmem : LMem) (lregs : LReg) (src : RegName) + (a_pc : Addr) (v_pc : Version) (lw_pc : LWord) + (p_src : Perm) (b_src e_src a_src : Addr) (v_src : Version) + (Ps : list D) : + + let la := (list_remove_elem a_pc (finz.seq_between b_src e_src)) in + let E := ⊤ ∖ ↑logN.@(a_pc, v_pc) in + let E' := allow_sweep_mask a_pc v_pc la v_src in + + length la = length Ps -> + allow_sweep_mem lmem lregs src a_pc v_pc lw_pc p_src b_src e_src a_src v_src Ps false + -∗ ([∗ map] la↦lw ∈ lmem, la ↦ₐ lw) + ={ if sweep_mask_cond lregs src p_src b_src e_src a_src v_src a_pc v_pc + then E' + else E, E }=∗ + (a_pc,v_pc) ↦ₐ lw_pc. + Proof. + intros * Hlen_Ps; iIntros "(%Hread & HSweepMem) Hmem". + rewrite /sweep_mask_cond. + case_decide as Hdecide; cycle 1. + - iDestruct "HSweepMem" as "->"; iModIntro. + iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]"; auto. + - iDestruct "HSweepMem" as (lws Hlen_lws ->) "(HPrange & _ & _ & Hcls_src)". + subst E'; rewrite !allow_sweep_mask_remove_nodup; auto. + iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]"; auto. + { + apply logical_region_notin; auto. + apply not_elemof_list_remove_elem; auto. } - assert ( la' ⊆+ finz.seq_between b0 e0 ) as Hsubmset_la' - by (by eapply list_remove_list_submsteq). - - (* not_elemof_list_remove_elem *) - iDestruct (interp_open_region $ (⊤ ∖ ↑logN.@(a0, v0)) with "Hinv") - as (Ps) "[%Hlen_Ps Hmod]"; eauto. - { eapply Forall_forall. intros. - assert ((x,v0) ≠ (a0,v0)) by set_solver. - eapply namespaces.coPset_subseteq_difference_r; auto. - solve_ndisj. + iMod ("Hcls_src" with "[Hmem HPrange]") as "_". + { + iNext. + iApply region_inv_construct; auto. + iExists (lws); iFrame "∗ %". } + iModIntro; iFrame. + Qed. - iMod "Hmod" - as (lws) "(%Hlen_lws & %Hpers & Hrange & HPrange & #Hread_cond & Hcls_src)" - ; eauto. - - assert (logical_region_map la' lws v0 !! (a0, v0) = None) as Ha0_notin_reg_la' - by (eapply logical_region_notin; eauto). - iDestruct (big_sepM_insert with "[$Hrange $Ha]") as "Hmem"; auto. - - - iApply (wp_isunique with "[$Hmap $Hmem]") - ; eauto - ; [ by simplify_map_eq - | rewrite /subseteq /map_subseteq /set_subseteq_instance - ; intros rr _; apply elem_of_dom - ; rewrite lookup_insert_is_Some'; - eauto - | by simplify_map_eq - |]. - iNext; iIntros (lregs' lmem' retv) "(%Hspec & Hmem & Hmap)". - destruct Hspec as - [ ? ? ? ? ? Hlwsrc' Hp_neq_E Hupd Hunique_regs Hincr_PC - | ? Hlwsrc Hnot_sealed Hunique_regs Hmem' Hincr_PC - | ? ? ? ? ? ? Hlwsrc Hlwsrc' Hmem' Hincr_PC - | ? ? Hfail] - ; simplify_map_eq - ; try (rewrite Hlwsrc' in Hlregs_src; simplify_eq) - ; try (rewrite Hlwsrc in Hlregs_src; simplify_eq) - ; try (cbn in Hlwsrc' ; simplify_eq) - ; cycle 1. - { (* Sweep false *) - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]"; auto. - iMod ("Hcls_src" with "[Hmem HPrange]") as "_". - { - iNext. - iApply region_inv_construct; auto. + (* If we have a valid sweep, but not opened the invariant, + it necessarily means that the permission of the src word is O *) + Lemma reg_allows_sweep_unique_O + (lregs : LReg) (src : RegName) + (p_pc : Perm) (b_pc e_pc a_pc : Addr) (v_pc : Version) + (p_src : Perm) (b_src e_src a_src : Addr) (v_src : Version): + + p_src ≠ machine_base.E -> + <[PC:=LCap p_pc b_pc e_pc a_pc v_pc]> lregs !! src = Some (LCap p_src b_src e_src a_src v_src) -> + unique_in_registersL + (<[PC:=LCap p_pc b_pc e_pc a_pc v_pc]> lregs) src + (LCap p_src b_src e_src a_src v_src) -> + (b_pc <= a_pc < e_pc)%a -> + ¬ (reg_allows_sweep + (<[PC:=LCap p_pc b_pc e_pc a_pc v_pc]> lregs) src p_src b_src + e_src a_src v_src ∧ (src = PC ∨ a_pc ∉ finz.seq_between b_src e_src)) + -> p_src = O. + Proof. + intros Hp_neq_E Hlwsrc' Hunique_regs Hbae Hdecide. + rewrite /reg_allows_sweep in Hdecide. + apply not_and_r in Hdecide. + destruct Hdecide as [Hdecide|Hdecide]; cycle 1. + - exfalso. + apply not_or in Hdecide. + destruct Hdecide as [Hsrc_neq_PC Ha_pc_overlap]. + apply dec_stable in Ha_pc_overlap. + clear -Hunique_regs Ha_pc_overlap Hsrc_neq_PC Hbae. + rewrite /unique_in_registersL in Hunique_regs. + eapply map_Forall_insert_1_1 in Hunique_regs. + rewrite decide_False in Hunique_regs; auto. + apply Hunique_regs. + rewrite /overlap_wordL /overlap_word //=. + apply elem_of_finz_seq_between in Ha_pc_overlap. + destruct (b_src lregs) in + + length la = length Ps -> + p_src ≠ machine_base.E -> + is_valid_updated_lmemory lmem (finz.seq_between b_src e_src) v_src lmem' -> + unique_in_registersL lregs' src (LCap p_src b_src e_src a_src v_src) -> + lregs' !! src = Some (LCap p_src b_src e_src a_src v_src) -> + isCorrectLPC (LCap p_pc b_pc e_pc a_pc v_pc) -> + Persistent (P lw_pc) -> + + □ (∀ lw : LWord, P lw -∗ fixpoint interp1 lw) + -∗ P lw_pc + -∗ allow_sweep_mem lmem lregs' src a_pc v_pc lw_pc p_src b_src e_src a_src v_src Ps false + -∗ ([∗ map] la↦lw ∈ lmem', la ↦ₐ lw) + ={ if sweep_mask_cond lregs' src p_src b_src e_src a_src v_src a_pc v_pc + then E' + else E, E}=∗ + (a_pc,v_pc) ↦ₐ lw_pc ∗ + (if sweep_mask_cond lregs' src p_src b_src e_src a_src v_src a_pc v_pc + then interp (LCap p_src b_src e_src a_src (v_src+1)) + else emp). + Proof. + intros * Hlen_Ps Hp_ne_E Hvalid_lmem' Hunique_regs Hlwsrc' Hcorrect_pc HpersP + ; iIntros "#Hread #HP (%Hread & HSweepMem) Hmem". + subst lregs'. + assert ( (b_pc <= a_pc < e_pc)%a) as Hbae. + { inversion Hcorrect_pc as [lpc ? ? ? ? Heq HcorrectPC Hlpc] + ; inversion HcorrectPC ; cbn in * ; simplify_map_eq; done. + } + rewrite /sweep_mask_cond. + case_decide as Hdecide ; cycle 1. + - iDestruct "HSweepMem" as "->". + apply reg_allows_sweep_unique_O in Hdecide; auto ; simplify_eq. + all: assert (src ≠ PC) + as Hsrc_ne_pc + by (intro ; subst + ; inversion Hcorrect_pc as [lpc ? ? ? ? Heq HcorrectPC Hlpc] + ; inversion HcorrectPC as [? ? ? ? Hbounds Hperm] + ; cbn in * ; simplify_map_eq + ; by destruct Hperm). + all: assert ( lmem' !! (a_pc, v_pc) = Some lw_pc ) + as Hmem'_apc + by (eapply is_valid_updated_lmemory_preserves_lmem; cycle 1 ; eauto; by simplify_map_eq). + all: rewrite -(insert_id lmem' (a_pc,v_pc) lw_pc);auto. + all: by iDestruct (big_sepM_insert_delete with "Hmem") as "[Hmem _]"; iFrame. + - destruct Hdecide as [ [Hsrc_lregs Hread_src] Hvalid_sweep]. + (* TODO @June: is there any part of the proof that is common + and could be refactored beforehand ? *) + destruct (decide (src = PC)) as [->|Hsrc_ne_pc] + ; [clear Hvalid_sweep |] + ; simplify_map_eq. + + (* r = PC *) + iDestruct "HSweepMem" as (lws Hlen_lws ->) "HSweepRest". + iDestruct "HSweepRest" as "(HPrange & %Hpers & #Hread_cond & Hcls_src)". + subst E'. + subst la ; set (la := (list_remove_elem a_src (finz.seq_between b_src e_src))). + + assert (a_src ∈ finz.seq_between b_src e_src) as Ha_pc_in_range. + { by apply isCorrectLPC_isCorrectPC_iff, isCorrectPC_withinBounds, withinBounds_in_seq + in Hcorrect_pc. } - iModIntro. - iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame). - iModIntro. - iApply wp_pure_step_later; auto. - iNext; iIntros "_". - incrementLPC_inv; simplify_map_eq. - assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq). - simplify_map_eq. - rewrite (insert_commute _ _ PC) // insert_insert. - iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]"); eauto. - { intro; by repeat (rewrite lookup_insert_is_Some'; right). } - { - iIntros (ri ? Hri Hvs). - destruct (decide (ri = dst)); simplify_map_eq. - by rewrite !fixpoint_interp1_eq. - iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto. + + assert ( a_src ∉ la) + as Ha_pc_notin_la' by (by subst la ; apply not_elemof_list_remove_elem). + + assert ( lmem' !! (a_src, v_src) = Some lw_pc ) as Hmem'_apc. + { eapply is_valid_updated_lmemory_preserves_lmem ; cycle 1 ; eauto. + by simplify_map_eq. } - iModIntro. - rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. - } - { (* Sweep false *) - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]";auto. - iMod ("Hcls_src" with "[Hmem HPrange]") as "_". + assert ( lmem' !! (a_src, v_src+1) = Some lw_pc ) as Hmem'_apc_next. + { eapply is_valid_updated_lmemory_preserves_lmem_next; cycle 1 + ; eauto + ; last by simplify_map_eq. + eapply Forall_forall; intros a' Ha'. + rewrite lookup_insert_ne //=; last (intro ; simplify_eq ; lia). + eapply logical_region_version_neq; eauto ; last lia. + } + + assert (logical_region_map la lws v_src !! (a_src, v_src) = None) + as Ha_src_notin_reg_la'. + { subst la ; eapply logical_region_notin; eauto. } + + assert ( ((logical_region_map la lws) ) v_src ⊆ lmem' ) + as Hmem'_be. + { subst la. + eapply is_valid_updated_lmemory_lmem_incl with (la := (finz.seq_between b_src e_src)) + ; eauto. + eapply is_valid_updated_lmemory_insert'; eauto. + eapply Forall_forall; intros a' Ha'. + eapply logical_region_version_neq; eauto ; last lia. + } + + assert ( ((logical_region_map la lws) ) (v_src+1) ⊆ lmem' ) + as Hmem'_be_next. + { eapply map_subseteq_spec; intros [a' v'] lw' Hlw'. + assert (v' = v_src+1 /\ (a' ∈ la)) + as [? Ha'_in_be] by (subst la ; eapply logical_region_map_some_inv; eauto) + ; simplify_eq. + destruct Hvalid_lmem' as [Hupdate_version_region _]. + eapply lookup_weaken; last eapply Hupdate_version_region. + rewrite update_version_region_preserves_lmem_next; eauto. + { rewrite lookup_insert_ne. + erewrite logical_region_map_lookup_versions; eauto. + clear -Ha'_in_be. + intro ; simplify_eq. + apply not_elemof_list_remove_elem in Ha'_in_be ; auto. + } + { eapply elem_of_submseteq; eauto. + eapply list_remove_elem_submsteq. + } + { rewrite lookup_insert_ne //=; last (intro ; simplify_eq ; lia). + eapply logical_region_version_neq; eauto; lia. + } + } + + rewrite -(insert_id lmem' (a_src, v_src) lw_pc); auto. + iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha_pc Hmem]". + rewrite -(insert_id (_ lmem') (a_src, v_src+1) lw_pc); auto. + 2: { rewrite lookup_delete_ne ; first by simplify_map_eq. intro ; simplify_eq ; lia. } + iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha_next Hmem]". + eapply delete_subseteq_r with (k := ((a_src, v_src) : LAddr)) in Hmem'_be + ; last (eapply logical_region_notin; eauto). + eapply delete_subseteq_r with (k := ((a_src, v_src+1) : LAddr)) in Hmem'_be + ; last (eapply logical_region_notin; eauto). + iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange Hmem]" + ; first (eapply Hmem'_be). + eapply delete_subseteq_r with (k := ((a_src, v_src) : LAddr)) in Hmem'_be_next + ; last (eapply logical_region_notin ; eauto). + eapply delete_subseteq_r with (k := ((a_src, v_src+1) : LAddr)) in Hmem'_be_next + ; last (eapply logical_region_notin ; eauto). + eapply delete_subseteq_list_r + with (m3 := list_to_map (zip (map (λ a : Addr, (a, v_src)) la) lws)) + in Hmem'_be_next + ; eauto + ; last (by eapply update_logical_memory_region_disjoint). + iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange' Hmem]" + ; first (eapply Hmem'_be_next); iClear "Hmem". + iDestruct "HPrange" as "#HPrange". + + iMod ("Hcls_src" with "[Hrange HPrange]") as "_". { - iNext. - iApply region_inv_construct; auto. + iNext. subst la. + iApply region_inv_construct; try done; auto. } - iModIntro. - iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame). - iModIntro. - iApply wp_pure_step_later; auto. - iNext; iIntros "_". - incrementLPC_inv; simplify_map_eq. - assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq). - simplify_map_eq. - rewrite (insert_commute _ _ PC) // insert_insert. - iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]"); eauto. - { intro; by repeat (rewrite lookup_insert_is_Some'; right). } + iSplitL "Ha_pc"; first by iFrame. + + iMod (region_valid_alloc' _ p_src b_src e_src a_src (v_src+1) (a_src::la) (lw_pc::lws) + with "[HPrange HP] [Hrange' Ha_next]") + as "#Hinterp__next"; last done. + { destruct p_src ; cbn in * ; try congruence; done. } + { eapply list_remove_list_region ; auto. + apply list_remove_elem_in in Ha_pc_in_range. + subst la. + by destruct Ha_pc_in_range as (la' & -> & ->). + } + { iDestruct (big_sepL2_sep_sepL_r with "[$Hread_cond $HPrange]") as "Hread_Ps". + iDestruct (big_sepL2_alt with "Hread_Ps") as "[_ Hread_Ps']". + iAssert ( + (∀ (k : nat) (x0 : leibnizO LWord * D), + ⌜zip lws Ps !! k = Some x0⌝ + → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1) + )%I as "Hread_Ps_unzip". + { iIntros (? ? ?) "[Ha Hpa]"; by iDestruct ("Hpa" with "Ha") as "?". } + iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "Hread_Ps' Hread_Ps_unzip" + ) as "Hread_Ps_zip". + iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$Hread_Ps_zip]") as "Hinterp_Ps" + ; first by rewrite Hlen_lws. + iSplit. + by iApply "Hread". + by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "Hinterp_Ps") as "[? ?]". + } + { iClear "#". clear -Hlen_Ps Hlen_lws. + iApply big_sepL2_alt. + subst la. + iSplit; first (iPureIntro; rewrite /= map_length; lia). + iDestruct (big_sepM_list_to_map with "Hrange'") as "?" ; last iFrame. + rewrite fst_zip. + apply NoDup_fmap; auto. + { by intros x y Heq ; simplify_eq. } + rewrite /logical_region map_length Hlen_lws ; lia. + } + + + (* r ≠ PC *) + iDestruct "HSweepMem" as (lws Hlen_lws ->) "HSweepRest". + subst E'. + destruct Hvalid_sweep as [Hcontra|Ha_pc_notin_src] ; first done. + subst la. + rewrite !list_remove_elem_notin in Hvalid_lmem', Hlen_Ps, Hlen_lws |- * ; auto. + + assert ( lmem' !! (a_pc, v_pc) = Some lw_pc ) as Hmem'_apc. + { eapply is_valid_updated_lmemory_preserves_lmem; eauto; by simplify_map_eq. } + assert ( logical_range_map b_src e_src lws v_src ⊆ lmem' ) + as Hmem'_be. { - iIntros (ri ? Hri Hvs). - destruct (decide (ri = dst)); simplify_map_eq. - by rewrite !fixpoint_interp1_eq. - iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto. + eapply is_valid_updated_lmemory_lmem_incl with + (la := (finz.seq_between b_src e_src)) (v := v_src) + ; eauto. + eapply is_valid_updated_lmemory_insert; eauto. + eapply logical_range_notin; eauto. + eapply Forall_forall; intros a' Ha'. + eapply logical_range_version_neq; eauto ; last lia. } - iModIntro. - rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. - } - { (* Fail *) - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hrange]"; auto. + assert + (logical_range_map b_src e_src lws (v_src + 1) ⊆ lmem') + as Hmem'_be_next. + { clear -Hvalid_lmem' Hlen_lws Ha_pc_notin_src. + eapply map_subseteq_spec; intros [a' v'] lw' Hlw'. + assert (v' = v_src+1 /\ (a' ∈ (finz.seq_between b_src e_src))) + as [? Ha'_in_be] by (eapply logical_range_map_some_inv; eauto); simplify_eq. + destruct Hvalid_lmem'. + eapply lookup_weaken; last eauto. + rewrite update_version_region_preserves_lmem_next; eauto. + all: rewrite lookup_insert_ne //=; last (intro ; set_solver). + erewrite logical_region_map_lookup_versions; eauto. + eapply logical_region_version_neq; eauto; lia. + } + + rewrite -(insert_id lmem' (a_pc, v_pc) lw_pc); auto. + iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha_pc Hmem]". + eapply delete_subseteq_r with (k := ((a_pc, v_pc) : LAddr)) in Hmem'_be + ; last (eapply logical_region_notin; eauto). + iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange Hmem]" + ; first (eapply Hmem'_be). + eapply delete_subseteq_r with (k := ((a_pc, v_pc) : LAddr)) in Hmem'_be_next + ; last (eapply logical_region_notin ; eauto). + eapply delete_subseteq_list_r + with (m3 := list_to_map (zip (map (λ a : Addr, (a, v_src)) + (finz.seq_between b_src e_src)) lws)) + in Hmem'_be_next + ; eauto + ; last (by eapply update_logical_memory_region_disjoint). + iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange' Hmem]" + ; first (eapply Hmem'_be_next); iClear "Hmem". + iDestruct "HSweepRest" as "(HPrange & %Hpers & #Hread_cond & Hcls_src)". + iDestruct "HPrange" as "#HPrange". iMod ("Hcls_src" with "[Hrange HPrange]") as "_". { iNext. - iApply region_inv_construct; auto. + iApply region_inv_construct; try done; auto. } - iModIntro. - iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame). - iModIntro. - iApply wp_pure_step_later; auto. - iNext; iIntros "_"; iApply wp_value; auto. - iIntros; discriminate. - } + iSplitL "Ha_pc"; first by iFrame. + + iMod (region_valid_alloc _ p_src b_src e_src a_src (v_src +1) lws + with "[HPrange] [Hrange']") + as "#Hinterp__next"; last done. + { destruct p_src ; cbn in * ; try congruence; done. } + { iDestruct ( big_sepL2_sep_sepL_r with "[$Hread_cond $HPrange]") as "Hread_Ps". + iDestruct (big_sepL2_alt with "Hread_Ps") as "[_ Hread_Ps']". + iAssert ( + (∀ (k : nat) (x0 : leibnizO LWord * D), + ⌜zip lws Ps !! k = Some x0⌝ + → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1) + )%I as "Hread_Ps_unzip". + { iIntros (? ? ?) "[Ha Hpa]"; by iDestruct ("Hpa" with "Ha") as "?". } + iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "Hread_Ps' Hread_Ps_unzip" + ) as "Hread_Ps_zip". + iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$Hread_Ps_zip]") + as "Hinterp_Ps" + ; first by rewrite Hlen_lws. + by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "Hinterp_Ps") as "[? ?]". + } + { iClear "#". clear -Hlen_Ps Hlen_lws. + iApply big_sepL2_alt. + iSplit; first (iPureIntro; rewrite map_length; lia). + iDestruct (big_sepM_list_to_map with "Hrange'") as "?" ; last iFrame. + rewrite fst_zip; first (apply NoDup_logical_region). + rewrite /logical_region map_length Hlen_lws ; lia. + } + Qed. - { (* Sweep true cap : update *) + Local Instance if_Persistent + p_pc b_pc e_pc a_pc v_pc lregs src p_src b_src e_src a_src v_src: + Persistent (if decide (reg_allows_sweep (<[PC:=LCap p_pc b_pc e_pc a_pc v_pc]> lregs) + src p_src b_src e_src a_src v_src + ∧ (src = PC ∨ a_pc ∉ finz.seq_between b_src e_src)) + then interp (LCap p_src b_src e_src a_src (v_src + 1)) + else emp)%I. + Proof. intros; case_decide; apply _. Qed. - incrementLPC_inv - as (p_pc' & b_pc' & e_pc' &a_pc' &v_pc' & ? & HPC & Z & Hregs') - ; simplify_map_eq. - assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq); simplify_map_eq. - do 2 (rewrite (insert_commute _ _ PC) //); - rewrite !insert_insert. - assert ( lmem' !! (a_pc', v) = Some lw ) as Hmem'_pca. - { eapply is_valid_updated_lmemory_preserves_lmem; cycle 1 ; eauto. - by simplify_map_eq. - apply finz_seq_between_NoDup. - } + Lemma isunique_case (lregs : leibnizO LReg) + (p_pc : Perm) (b_pc e_pc a_pc : Addr) (v_pc : Version) + (lw_pc : LWord) (dst src : RegName) (P : D): + ftlr_instr lregs p_pc b_pc e_pc a_pc v_pc lw_pc (IsUnique dst src) P. + Proof. + intros Hp Hsome HcorrectLPC Hbae Hi. + iIntros "#IH #Hinv #Hinva #Hreg #(Hread & Hwrite & %HpersP) Hown Ha #HP Hcls HPC Hmap". + specialize (HpersP lw_pc). + rewrite delete_insert_delete. + iDestruct ((big_sepM_delete _ _ PC) with "[HPC Hmap]") as "Hmap /="; + [apply lookup_insert|rewrite delete_insert_delete;iFrame|]. simpl. - assert (NoDup (finz.seq_between b_pc' e_pc')) as HNoDup_pc - by (by apply finz_seq_between_NoDup). + (* To read out PC's name later, and needed when calling wp_load *) + assert(∀ x : RegName, is_Some (<[PC:=LCap p_pc b_pc e_pc a_pc v_pc]> lregs !! x)) as Hsome'. + { + intros. destruct (decide (x = PC)) as [Hx|Hx]. + rewrite Hx lookup_insert; unfold is_Some. by eexists. + by rewrite lookup_insert_ne. + } - assert ( lmem' !! (a_pc', v+1) = Some lw ) as Hmem'_pca_next. - { eapply is_valid_updated_lmemory_preserves_lmem_next; cycle 1 - ; eauto - ; last by simplify_map_eq. - eapply Forall_forall; intros a Ha. - rewrite lookup_insert_ne //=; last (intro ; simplify_eq ; lia). - eapply logical_region_version_neq; eauto ; last lia. - } - - assert ( ((logical_region_map la' lws) ) v ⊆ lmem' ) - as Hmem'_be. - { - eapply is_valid_updated_lmemory_lmem_incl with (la := (finz.seq_between b_pc' e_pc')) - ; eauto. - eapply is_valid_updated_lmemory_insert'; eauto. - eapply Forall_forall; intros a Ha. - eapply logical_region_version_neq; eauto ; last lia. - } - assert ( ((logical_region_map la' lws) ) (v+1) ⊆ lmem' ) - as Hmem'_be_next. - { - eapply map_subseteq_spec; intros [a' v'] lw' Hlw'. - assert (v' = v+1 /\ (a' ∈ la')) as [? Ha'_in_be] - by (eapply logical_region_map_some_inv; eauto) - ; simplify_eq. - simplify_eq. - destruct Hupd. - eapply lookup_weaken; last eapply H0. - rewrite update_version_region_preserves_lmem_next; eauto. - { rewrite lookup_insert_ne ; last (intro ; simplify_eq ; set_solver). - erewrite logical_region_map_lookup_versions; eauto. - } - { subst la'. - eapply elem_of_submseteq; eauto. - } - { rewrite lookup_insert_ne //=; last (intro ; simplify_eq ; lia). - eapply logical_region_version_neq; eauto; lia. - } - } - - rewrite -(insert_id lmem' (a_pc', v) lw); auto. - iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha Hmem]". - - rewrite -(insert_id (_ lmem') (a_pc', v+1) lw); auto. - 2: { rewrite lookup_delete_ne ; first by simplify_map_eq. intro ; simplify_eq ; lia. } - iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha_next Hmem]". - - eapply delete_subseteq_r with (k := ((a_pc', v) : LAddr)) in Hmem'_be - ; last (eapply logical_region_notin; eauto). - eapply delete_subseteq_r with (k := ((a_pc', v+1) : LAddr)) in Hmem'_be - ; last (eapply logical_region_notin; eauto). - iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange Hmem]" - ; first (eapply Hmem'_be). - - eapply delete_subseteq_r with (k := ((a_pc', v) : LAddr)) in Hmem'_be_next - ; last (eapply logical_region_notin ; eauto). - eapply delete_subseteq_r with (k := ((a_pc', v+1) : LAddr)) in Hmem'_be_next - ; last (eapply logical_region_notin ; eauto). - eapply delete_subseteq_list_r - with (m3 := list_to_map (zip (map (λ a : Addr, (a, v)) la') lws)) - in Hmem'_be_next - ; eauto - ; last (by eapply update_logical_memory_region_disjoint). - iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange' Hmem]" - ; first (eapply Hmem'_be_next); iClear "Hmem". - iDestruct "HPrange" as "#HPrange". - iDestruct "HP" as "#HP". - - iMod ("Hcls_src" with "[Hrange HPrange]") as "_". - { - iNext. - iApply region_inv_construct; try done. - iExists lws; iSplit ; first done; iFrame "#∗". - } - iModIntro. - iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame "#∗"). - iModIntro. - - iMod (region_valid_alloc' _ b_pc' e_pc' a_pc' (a_pc'::la') (v +1) (lw::lws) p_pc' - with "[HPrange HP] [Hrange' Ha_next]") - as "#Hinterp_src_next". - { destruct p_pc' ; cbn in * ; try congruence; done. } - { eapply list_remove_list_region ; auto. } - { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_P0". - iSplit ; last iFrame "Hread_cond". - by rewrite Hlen_lws. - cbn. - iDestruct ( big_sepL2_sep_sepL_r with "[$Hread_cond $HPrange]") as "HPs". - iDestruct (big_sepL2_alt with "HPs") as "[_ HPs']". - iAssert ( - (∀ (k : nat) (x0 : leibnizO LWord * D), - ⌜zip lws Ps !! k = Some x0⌝ - → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1) - )%I as "bla". - { iIntros (? ? ?) "[Ha Hpa]"; by iDestruct ("Hpa" with "Ha") as "?". } - iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "HPs' bla" - ) as "blaa". - iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$blaa]") as "blaaa". - by rewrite Hlen_lws. - iSplit. - by iApply "Hread". - by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "blaaa") as "[? ?]". - } - { iClear "#". subst la'. clear -Hlen_Ps Hlen_lws HNoDup_la'. - iApply big_sepL2_alt. - iSplit; first (iPureIntro; rewrite /= map_length; lia). - iDestruct (big_sepM_list_to_map with "Hrange'") as "?" ; last iFrame. - rewrite fst_zip. - apply NoDup_fmap; auto. - { by intros x y Heq ; simplify_eq. } - rewrite /logical_region map_length ; lia. - } - - iApply wp_pure_step_later; auto. - iNext; iIntros "_". - simplify_map_eq. - iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]") - ; eauto. - { intro; by repeat (rewrite lookup_insert_is_Some'; right). } - { iIntros (r1 lw1 Hr1 Hlw1). - destruct (decide (r1 = dst)) as [ |Hr1_dst] - ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=). - iApply "Hreg"; eauto. } - { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; done. } - } - - - pose proof (Hsome src) as [wsrc Hlregs_src]. - rewrite /read_reg_inr in HVsrc; simplify_map_eq. - destruct (decide (is_lcap wsrc)) as [Hcap|Hcap]; cycle 1. - { (* wsrc in not a lcap *) - destruct_lword wsrc ; cbn in HVsrc; try done. - all: rewrite memMap_resource_1. - all: iApply (wp_isunique with "[$Hmap $Ha]") - ; eauto - ; [ by simplify_map_eq - | rewrite /subseteq /map_subseteq /set_subseteq_instance - ; intros rr _; apply elem_of_dom; rewrite lookup_insert_is_Some'; eauto - | by simplify_map_eq - |]. - all: try done. - all: iNext; iIntros (lregs' lmem' retv) "(%Hspec & Hmem & Hmap)". - all: inversion Hspec as [ | | | ? ? Hfail]; simplify_map_eq - ; try (rewrite H0 in Hlregs_src; simplify_eq). - all: rewrite -memMap_resource_1. - all: iMod ("Hcls" with "[Hmem HP]");[iExists lw;iFrame|iModIntro]. - all: iApply wp_pure_step_later; auto. - all: iNext; iIntros "_"; iApply wp_value; auto. - all: iIntros; discriminate. - } + (* Initializing the names for the values of Hsrc now, to instantiate the existentials in step 1 *) + assert (∃ p_src b_src e_src a_src v_src, read_reg_inr (<[PC:=LCap p_pc b_pc e_pc a_pc v_pc]> lregs) src p_src b_src e_src a_src v_src) + as (p_src & b_src & e_src & a_src & v_src & HV_Src). + { + specialize Hsome' with src as Hsrc. + destruct Hsrc as [wsrc Hsome_src]. + unfold read_reg_inr. rewrite Hsome_src. + destruct wsrc as [|[ p_src b_src e_src a_src v_src|] | ]; try done. + by repeat eexists. + } - iAssert (interp wsrc) as "#Hinterp_src" ; first (iApply "Hreg"; eauto). - (* wsrc is a lcap *) - destruct (is_sealed wsrc) eqn:His_sealed. - + (* wsrc is either E-cap or sealed cap *) - rewrite memMap_resource_1. - iApply (wp_isunique with "[$Hmap $Ha]") - ; eauto - ; [ by simplify_map_eq - | rewrite /subseteq /map_subseteq /set_subseteq_instance - ; intros rr _; apply elem_of_dom; rewrite lookup_insert_is_Some'; eauto - | by simplify_map_eq - |]. - iNext; iIntros (lregs' lmem' retv) "(%Hspec & Hmem & Hmap)". - inversion Hspec as [| ? Hlwsrc Hcannot_read Hunique_regs Hmem' Hincr_PC | |] - ; simplify_map_eq. - { (* case sweep success cap : contradiction *) - rewrite H0 in Hlregs_src; simplify_map_eq. - by destruct p0 ; cbn in * ; try congruence. + (* Step 1: open the region, if necessary, + and store all the resources obtained from the region in allow_load_res *) + iDestruct (create_sweep_res with "[$Hreg] [$Hinv]") as (Ps) "[%Hlen_Ps HSweepRes]" + ; [ eassumption + | by apply elem_of_finz_seq_between + |]. + + (* Step 2: derive the concrete map of memory we need, and any spatial predicates holding over it *) + iMod (sweep_res_implies_mem_map with "HSweepRes Ha") as (mem) "[HSweepMem >HMemRes]". + set (E := ⊤ ∖ ↑logN.@(a_pc, v_pc)). + set (E' := allow_sweep_mask a_pc v_pc (list_remove_elem a_pc (finz.seq_between b_src e_src)) v_src ). + + (* Step 3: derive the non-spatial conditions over the memory map*) + iDestruct (mem_map_implies_pure_conds with "HSweepMem") as %HReadPC. + + (* Step 4: move the later outside, so that we can remove it after applying wp_isunique *) + iDestruct (allow_sweep_mem_later with "HSweepMem") as "HSweepMem"; auto. + + iApply (wp_isunique with "[$Hmap $HMemRes]") + ; eauto + ; [ by simplify_map_eq + | rewrite /subseteq /map_subseteq /set_subseteq_instance + ; intros rr _; apply elem_of_dom + ; rewrite lookup_insert_is_Some'; + eauto + |]. + iNext; iIntros (lregs' lmem' retv) "(%Hspec & Hmem & Hmap)". + destruct Hspec as + [ p_src' b_src' e_src' a_src' v_src' Hlwsrc' Hp_neq_E Hupd Hunique_regs Hincr_PC + | ? Hlwsrc Hnot_sealed Hunique_regs Hmem' Hincr_PC + | lwsrc' p_src' b_src' e_src' a_src' v_src' Hlwsrc Hlwsrc' Hmem' Hincr_PC + | ? ? Hfail] + ; simplify_map_eq + ; try (rewrite Hlwsrc' in Hlregs_src; simplify_eq) + ; try (rewrite Hlwsrc in Hlregs_src; simplify_eq) + ; try (cbn in Hlwsrc' ; simplify_eq). + + { (* Sweep true cap : update *) + rewrite /read_reg_inr Hlwsrc' in HV_Src ; simplify_eq. + iMod (mem_map_recover_res_update_version with "Hread HP HSweepMem Hmem") + as "[Ha #Hinterp]"; auto. + + iModIntro. + iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame "#∗"). + iModIntro. + iApply wp_pure_step_later; auto. + iNext; iIntros "_". + simplify_map_eq. + + incrementLPC_inv + as (p_pc' & b_pc' & e_pc' &a_pc' &v_pc' & ? & HPC & Z & Hregs') + ; simplify_map_eq. + assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq); simplify_map_eq. + rewrite /sweep_mask_cond. + set (cond_open := decide ( _ /\ _ )). + destruct cond_open as [Hdecide|Hdecide]; cycle 1. + - (* Case (p_src = O) *) + apply reg_allows_sweep_unique_O in Hdecide; auto ; simplify_eq. + assert (src ≠ PC) + as Hr_ne_pc + by (intro ; subst + ; inversion HcorrectLPC as [lpc ? ? ? ? Heq HcorrectPC Hlpc] + ; inversion HcorrectPC as [? ? ? ? Hbounds Hperm] + ; cbn in * ; simplify_map_eq + ; by destruct Hperm). + do 2 (rewrite (insert_commute _ _ PC) //); rewrite !insert_insert. + simplify_map_eq. + iApply ("IH" $! (<[dst := LInt 1]> (<[src := _]> lregs)) with "[%] [] [Hmap] [$Hown]") + ; eauto. + { intro; by repeat (rewrite lookup_insert_is_Some'; right). } + { iIntros (r1 lw1 Hr1 Hlw1). + destruct (decide (r1 = dst)) as [ |Hr1_dst] + ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=). + destruct (decide (r1 = src)) as [ |Hr1_src] + ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=). + iApply "Hreg"; eauto. } - { (* case sweep success is_sealed *) - cbn in *; simplify_eq. - rewrite -memMap_resource_1. - iMod ("Hcls" with "[Hmem HP]");[iExists lw;iFrame|iModIntro]. - iApply wp_pure_step_later; auto. - iNext; iIntros "_". - incrementLPC_inv; simplify_map_eq. - assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq). - simplify_map_eq. - rewrite (insert_commute _ _ PC) // insert_insert. - iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]"); eauto. + { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; try done. } + - destruct Hdecide as [ [Hsrc_lregs Hread_src] Hwf]. + destruct (decide (src = PC)) as [->|Hsrc_neq_pc] + ; [clear Hwf | destruct Hwf ; simplify_eq] + ; simplify_map_eq + ; do 2 (rewrite (insert_commute _ _ PC) //); rewrite !insert_insert. + + (* src = PC *) + iApply ("IH" $! (<[dst := LInt 1]> lregs) with "[%] [] [Hmap] [$Hown]") + ; eauto. { intro; by repeat (rewrite lookup_insert_is_Some'; right). } - { - iIntros (ri ? Hri Hvs). - destruct (decide (ri = dst)); simplify_map_eq. - by rewrite !fixpoint_interp1_eq. - iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto. + { iIntros (r1 lw1 Hr1 Hlw1). + destruct (decide (r1 = dst)) as [ |Hr1_dst] + ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=). + iApply "Hreg"; eauto. } - iModIntro. - rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. - } - { (* case sweep false*) - cbn in *; simplify_eq. - rewrite -memMap_resource_1. - iMod ("Hcls" with "[Hmem HP]");[iExists lw;iFrame|iModIntro]. - iApply wp_pure_step_later; auto. - iNext; iIntros "_". - incrementLPC_inv; simplify_map_eq. - assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq). - simplify_map_eq. - rewrite (insert_commute _ _ PC) // insert_insert. - iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]"); eauto. + { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; try done. } + + (* src ≠ PC *) + iApply ("IH" $! (<[dst := LInt 1]> ( <[src := _ ]> lregs)) with "[%] [] [Hmap] [$Hown]") + ; eauto. { intro; by repeat (rewrite lookup_insert_is_Some'; right). } - { - iIntros (ri ? Hri Hvs). - destruct (decide (ri = dst)); simplify_map_eq. - by rewrite !fixpoint_interp1_eq. - iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto. - } - iModIntro. - rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. - } - { (* Fail *) - rewrite -memMap_resource_1. - iMod ("Hcls" with "[Hmem HP]");[iExists lw;iFrame|iModIntro]. - iApply wp_pure_step_later; auto. - iNext; iIntros "_"; iApply wp_value; auto. - iIntros; discriminate. - } - + (* wsrc is an actual capability, with at least read permission *) - destruct_lword wsrc ; simplify_eq ; clear Hcap. - destruct (readAllowed p0) eqn:Hread; cycle 1. - { (* Case O-cap *) - destruct p0 eqn:Hp0 ; cbn in His_sealed, Hread ; try congruence. - rewrite memMap_resource_1. - iApply (wp_isunique with "[$Hmap $Ha]") - ; eauto - ; [ by simplify_map_eq - | rewrite /subseteq /map_subseteq /set_subseteq_instance - ; intros rr _; apply elem_of_dom; rewrite lookup_insert_is_Some'; eauto - | by simplify_map_eq - |]. - iNext; iIntros (lregs' lmem' retv) "(%Hspec & Hmem & Hmap)". - inversion Hspec as - [ ? ? ? ? ? Hlwsrc' Hp_neq_E Hupd Hunique_regs Hincr_PC - | ? Hlwsrc Hnot_sealed Hunique_regs Hmem' Hincr_PC - | ? ? ? ? ? ? Hlwsrc Hlwsrc' Hmem' Hincr_PC - | ? ? Hfail] - ; simplify_map_eq - ; try (rewrite Hlregs_src in Hlwsrc ; simplify_eq) - ; cycle 1. - { (* case sweep false*) - cbn in *; simplify_eq. - rewrite -memMap_resource_1. - iMod ("Hcls" with "[Hmem HP]");[iExists lw;iFrame|iModIntro]. - iApply wp_pure_step_later; auto. - iNext; iIntros "_". - incrementLPC_inv; simplify_map_eq. - assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq). - simplify_map_eq. - rewrite (insert_commute _ _ PC) // insert_insert. - iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]"); eauto. - { intro; by repeat (rewrite lookup_insert_is_Some'; right). } - { - iIntros (ri ? Hri Hvs). - destruct (decide (ri = dst)); simplify_map_eq. - by rewrite !fixpoint_interp1_eq. - iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto. - } - iModIntro. - rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. - } - { (* Fail *) - rewrite -memMap_resource_1. - iMod ("Hcls" with "[Hmem HP]");[iExists lw;iFrame|iModIntro]. - iApply wp_pure_step_later; auto. - iNext; iIntros "_"; iApply wp_value; auto. - iIntros; discriminate. - } - { (* case sweep true cap *) - assert ( lmem' !! (a, v) = Some lw ) as Hmem'_pca. - { eapply is_valid_updated_lmemory_preserves_lmem; eauto. - apply finz_seq_between_NoDup. - by simplify_map_eq. - } - rewrite -(insert_id lmem' (a,v) lw). - iDestruct (big_sepM_insert_delete with "Hmem") as "[Hmem _]". - iMod ("Hcls" with "[Hmem HP]");[iExists lw;iFrame|iModIntro]. - iApply wp_pure_step_later; auto. - iNext; iIntros "_". - incrementLPC_inv; simplify_map_eq. - assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq). - simplify_map_eq. - do 2 (rewrite (insert_commute _ _ PC) //) ; rewrite insert_insert. - iApply ("IH" $! (<[dst := (LInt 1)]> (<[src:=LCap p1 b1 e1 a1 (v1 + 1)]> lregs)) - with "[%] [] [Hmap] [$Hown]"); eauto. - { intro; by repeat (rewrite lookup_insert_is_Some'; right). } - { - iIntros (ri ? Hri Hvs). - destruct (decide (ri = dst)) ; simplify_map_eq - ; first by rewrite !fixpoint_interp1_eq. - destruct (decide (ri = src)) ; rewrite Hlwsrc' in Hlregs_src ; simplify_map_eq - ; first by rewrite !fixpoint_interp1_eq. - iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto. - } - rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. - done. - } - } - clear His_sealed. - - assert (NoDup (finz.seq_between b0 e0)) as HNoDup_range by apply finz_seq_between_NoDup. - - destruct (decide (a ∈ finz.seq_between b0 e0)) as [ Ha_in_src | Ha_notin_src ]. - * (* There's no need to open the invariant of the region, - because we know that pc and src overlap *) - rewrite memMap_resource_1. - iApply (wp_isunique with "[$Hmap $Ha]") - ; eauto - ; [ by simplify_map_eq - | rewrite /subseteq /map_subseteq /set_subseteq_instance - ; intros rr _; apply elem_of_dom; rewrite lookup_insert_is_Some'; eauto - | by simplify_map_eq - |]. - iNext; iIntros (lregs' lmem' retv) "(%Hspec & Hmem & Hmap)". - inversion Hspec as - [ ? ? ? ? ? Hlwsrc' Hp_neq_E Hupd Hunique_regs Hincr_PC - | ? Hlwsrc Hnot_sealed Hunique_regs Hmem' Hincr_PC - | ? ? ? ? ? ? Hlwsrc Hlwsrc' Hmem' Hincr_PC - | ? ? Hfail] - ; simplify_map_eq - ; try (rewrite Hlregs_src in Hlwsrc' ; simplify_eq) - ; try (rewrite Hlregs_src in Hlwsrc ; simplify_eq). - { (* case sweep true cap : contradiction *) - exfalso. clear -Hunique_regs Ha_in_src Hsrc_neq_pc Hbae. - apply map_Forall_insert_1_1 in Hunique_regs. - rewrite decide_False //= in Hunique_regs. - apply Hunique_regs. - rewrite elem_of_finz_seq_between in Ha_in_src. - destruct Ha_in_src; cbn. - destruct (b1 lregs) with "[%] [] [Hmap] [$Hown]"); eauto. - { intro; by repeat (rewrite lookup_insert_is_Some'; right). } - { - iIntros (ri ? Hri Hvs). - destruct (decide (ri = dst)); simplify_map_eq. - by rewrite !fixpoint_interp1_eq. - iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto. - } - iModIntro. - rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. - } - { (* case fail *) - rewrite -memMap_resource_1. - iMod ("Hcls" with "[Hmem HP]");[iExists lw;iFrame|iModIntro]. - iApply wp_pure_step_later; auto. - iNext; iIntros "_"; iApply wp_value; auto. - iIntros; discriminate. - } - - * (* src ≠ PC *) - - assert (readAllowed p) as Hread_p by (destruct p ; destruct Hp ; done). - iDestruct (interp_open_region $ (⊤ ∖ ↑logN.@(a, v)) with "Hinterp_src") - as (Ps) "[%Hlen_Ps Hmod]"; eauto. - { apply Forall_forall; intros a' Ha'. - assert (a' ≠ a) by set_solver. - apply namespaces.coPset_subseteq_difference_r; [solve_ndisj|set_solver]. + { iIntros (r1 lw1 Hr1 Hlw1). + destruct (decide (r1 = dst)) as [ |Hr1_dst] + ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=). + destruct (decide (r1 = src)) as [ |Hr1_src] + ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=). + iApply "Hreg"; eauto. } + { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; try done. } + } + { (* Sweep false *) + + iMod (mem_map_recover_res_no_update with "HSweepMem Hmem") as "Ha_pc"; auto. + subst E. + iModIntro. + iMod ("Hcls" with "[Ha_pc HP]") as "_"; [iNext; iExists lw_pc ; iFrame|iModIntro]; auto. + iApply wp_pure_step_later; auto. + iNext; iIntros "_". + incrementLPC_inv; simplify_map_eq. + assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq). + simplify_map_eq. + rewrite (insert_commute _ _ PC) // insert_insert. + iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]"); eauto. + { intro; by repeat (rewrite lookup_insert_is_Some'; right). } + { + iIntros (ri ? Hri Hvs). + destruct (decide (ri = dst)); simplify_map_eq. + by rewrite !fixpoint_interp1_eq. + iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto. + } + iModIntro. + rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. + } - iMod "Hmod" - as (lws) "(%Hlen_lws & %Hpers & Hrange & HPrange & #Hread_cond & Hcls_src)" - ; eauto. + { (* Sweep sealed *) + iMod (mem_map_recover_res_no_update with "HSweepMem Hmem") as "Ha_pc"; auto. + subst E. + iModIntro. + iMod ("Hcls" with "[Ha_pc HP]") as "_"; [iNext; iExists lw_pc ; iFrame|iModIntro]; auto. + iApply wp_pure_step_later; auto. + iNext; iIntros "_". + incrementLPC_inv; simplify_map_eq. + assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq). + simplify_map_eq. + rewrite (insert_commute _ _ PC) // insert_insert. + iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]"); eauto. + { intro; by repeat (rewrite lookup_insert_is_Some'; right). } + { + iIntros (ri ? Hri Hvs). + destruct (decide (ri = dst)); simplify_map_eq. + by rewrite !fixpoint_interp1_eq. + iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto. + } + iModIntro. + rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. + } - assert (forall v', logical_region_map (finz.seq_between b0 e0) lws v' !! (a, v) = None) as Ha_notin_reg_la'. - by (intro; eapply logical_region_notin; eauto). - iDestruct (big_sepM_insert with "[$Hrange $Ha]") as "Hmem"; first done. - - iApply (wp_isunique with "[$Hmap $Hmem]") - ; eauto - ; [ by simplify_map_eq - | rewrite /subseteq /map_subseteq /set_subseteq_instance - ; intros rr _; apply elem_of_dom - ; rewrite lookup_insert_is_Some'; - eauto - | by simplify_map_eq - |]. - iNext; iIntros (lregs' lmem' retv) "(%Hspec & Hmem & Hmap)". - destruct Hspec as - [ ? ? ? ? ? Hlwsrc' Hp_neq_E Hupd Hunique_regs Hincr_PC - | ? Hlwsrc Hnot_sealed Hunique_regs Hmem' Hincr_PC - | ? ? ? ? ? ? Hlwsrc Hlwsrc' Hmem' Hincr_PC - | ? ? Hfail] - ; simplify_map_eq - ; try (rewrite Hlwsrc' in Hlregs_src; simplify_eq) - ; try (rewrite Hlwsrc in Hlregs_src; simplify_eq) - ; try (cbn in Hlwsrc' ; simplify_eq) - ; cycle 1. - { (* Sweep false *) - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]"; first done. - iMod ("Hcls_src" with "[Hmem HPrange]") as "_". - { - iNext. - iApply region_inv_construct; auto. - } - iModIntro. - iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame). - iModIntro. - iApply wp_pure_step_later; auto. - iNext; iIntros "_". - incrementLPC_inv; simplify_map_eq. - assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq). - simplify_map_eq. - rewrite (insert_commute _ _ PC) // insert_insert. - iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]"); eauto. - { intro; by repeat (rewrite lookup_insert_is_Some'; right). } - { - iIntros (ri ? Hri Hvs). - destruct (decide (ri = dst)); simplify_map_eq. - by rewrite !fixpoint_interp1_eq. - iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto. - } - iModIntro. - rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. - } - { (* Sweep false *) - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]"; first done. - iMod ("Hcls_src" with "[Hmem HPrange]") as "_". - { - iNext. - iApply region_inv_construct; auto. - } - iModIntro. - iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame). - iModIntro. - iApply wp_pure_step_later; auto. - iNext; iIntros "_". - incrementLPC_inv; simplify_map_eq. - assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq). - simplify_map_eq. - rewrite (insert_commute _ _ PC) // insert_insert. - iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]"); eauto. - { intro; by repeat (rewrite lookup_insert_is_Some'; right). } - { - iIntros (ri ? Hri Hvs). - destruct (decide (ri = dst)); simplify_map_eq. - by rewrite !fixpoint_interp1_eq. - iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto. - } - iModIntro. - rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. - } - { (* Fail *) - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hrange]"; first done. - iMod ("Hcls_src" with "[Hrange HPrange]") as "_". - { - iNext. - iApply region_inv_construct; auto. - } - iModIntro. - iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame). - iModIntro. - iApply wp_pure_step_later; auto. - iNext; iIntros "_"; iApply wp_value; auto. - iIntros; discriminate. - } + { (* Fail *) + iMod (mem_map_recover_res_no_update with "HSweepMem Hmem") as "Ha_pc"; auto. + subst E. + iModIntro. + iMod ("Hcls" with "[Ha_pc HP]") as "_"; auto. + iModIntro. + iApply wp_pure_step_later; auto. + iNext; iIntros "_"; iApply wp_value; auto. + iIntros; discriminate. + } +Qed. - { (* Sweep true *) - - incrementLPC_inv - as (p_pc' & b_pc' & e_pc' &a_pc' &v_pc' & ? & HPC & Z & Hregs') - ; simplify_map_eq. - assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq); simplify_map_eq. - do 2 (rewrite (insert_commute _ _ PC) //); rewrite insert_insert. - - assert ( lmem' !! (a_pc', v_pc') = Some lw ) as Hmem'_pca. - { eapply is_valid_updated_lmemory_preserves_lmem; eauto. - by simplify_map_eq. - } - - assert ( logical_range_map b0 e0 lws v0 ⊆ lmem' ) - as Hmem'_be. - { - eapply is_valid_updated_lmemory_lmem_incl with (la := (finz.seq_between b0 e0)) - ; eauto. - eapply is_valid_updated_lmemory_insert; eauto. - eapply Forall_forall; intros a Ha. - eapply logical_range_version_neq; eauto ; last lia. - } - assert - (logical_range_map b0 e0 lws (v0 + 1) ⊆ lmem') - as Hmem'_be_next. - { clear -Hupd Hlen_lws HNoDup_range Ha_notin_src. - eapply map_subseteq_spec; intros [a' v'] lw' Hlw'. - assert (v' = v0+1 /\ (a' ∈ (finz.seq_between b0 e0))) as [? Ha'_in_be] - by (eapply logical_range_map_some_inv; eauto); simplify_eq. - destruct Hupd. - eapply lookup_weaken; last eauto. - rewrite update_version_region_preserves_lmem_next; eauto. - all: rewrite lookup_insert_ne //=; last (intro ; set_solver). - erewrite logical_region_map_lookup_versions; eauto. - eapply logical_region_version_neq; eauto; lia. - } - - rewrite -(insert_id lmem' (a_pc', v_pc') lw); auto. - iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha Hmem]". - eapply delete_subseteq_r with (k := ((a_pc', v_pc') : LAddr)) in Hmem'_be - ; last (eapply logical_region_notin; eauto). - iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange Hmem]" - ; first (eapply Hmem'_be). - eapply delete_subseteq_r with (k := ((a_pc', v_pc') : LAddr)) in Hmem'_be_next - ; last (eapply logical_region_notin ; eauto). - eapply delete_subseteq_list_r - with (m3 := list_to_map (zip (map (λ a : Addr, (a, v0)) (finz.seq_between b0 e0)) lws)) - in Hmem'_be_next - ; eauto - ; last (by eapply update_logical_memory_region_disjoint). - iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange' Hmem]" - ; first (eapply Hmem'_be_next); iClear "Hmem". - iDestruct "HPrange" as "#HPrange". - - iMod (region_valid_alloc _ b0 e0 a0 (v0 +1) lws p0 - with "[HPrange] [Hrange']") - as "#Hinterp_src_next". - { destruct p0 ; cbn in * ; try congruence; done. } - { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_P0". - iSplit ; last iFrame "Hread_cond". - by rewrite Hlen_lws. - cbn. - iDestruct ( big_sepL2_sep_sepL_r with "[$Hread_cond $HPrange]") as "HPs". - iClear - "IH Hinv Hinva Hreg Hread Hwrite Hinterp_src Hread_P0 HPrange". - iDestruct (big_sepL2_alt with "HPs") as "[_ HPs']". - iAssert ( - (∀ (k : nat) (x0 : leibnizO LWord * D), - ⌜zip lws Ps !! k = Some x0⌝ - → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1) - )%I as "bla". - { iIntros (? ? ?) "[Ha Hpa]"; by iDestruct ("Hpa" with "Ha") as "?". } - iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "HPs' bla" - ) as "blaa". - iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$blaa]") as "blaaa". - by rewrite Hlen_lws. - by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "blaaa") as "[? ?]". - } - { iClear "#". clear -Hlen_Ps Hlen_lws. - iApply big_sepL2_alt. - iSplit; first (iPureIntro; rewrite map_length; lia). - iDestruct (big_sepM_list_to_map with "Hrange'") as "?" ; last iFrame. - rewrite fst_zip; first (apply NoDup_logical_region). - rewrite /logical_region map_length ; lia. - } - - iMod ("Hcls_src" with "[Hrange HPrange]") as "_". - { - iNext. - iApply region_inv_construct; auto. - } - iModIntro. - iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame). - iModIntro. - - iApply wp_pure_step_later; auto. - iNext; iIntros "_". - simplify_map_eq. - iApply ("IH" $! (<[dst := _]> (<[ src := _ ]> lregs)) with "[%] [] [Hmap] [$Hown]") - ; eauto. - { intro; by repeat (rewrite lookup_insert_is_Some'; right). } - { iIntros (r1 lw1 Hr1 Hlw1). - destruct (decide (r1 = dst)) as [ |Hr1_dst] - ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=). - destruct (decide (r1 = src)) as [ |Hr1_src] - ; simplify_map_eq; first done. - iApply "Hreg"; eauto. } - { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; done. } - } - Qed. End fundamental. diff --git a/theories/ftlr/Store.v b/theories/ftlr/Store.v index f561653d..59a5dbb2 100644 --- a/theories/ftlr/Store.v +++ b/theories/ftlr/Store.v @@ -220,11 +220,12 @@ Section fundamental. exists wsrc. by rewrite Hsomer. } - (* Step 1: open the region, if necessary, and store all the resources obtained from the region in allow_load_res *) + (* Step 1: open the region, if necessary, + and store all the resources obtained from the region in allow_load_res *) iDestruct (create_store_res with "Hreg") as "HStoreRes"; eauto. - - (* Step2: derive the concrete map of memory we need, and any spatial predicates holding over it *) + (* Step2: derive the concrete map of memory we need, + and any spatial predicates holding over it *) iMod (store_res_implies_mem_map with "HStoreRes Ha") as (mem) "[HStoreMem >HMemRes]". (* Step 3: derive the non-spatial conditions over the memory map*) diff --git a/theories/fundamental.v b/theories/fundamental.v index 31508afe..09da132e 100644 --- a/theories/fundamental.v +++ b/theories/fundamental.v @@ -276,13 +276,6 @@ Section fundamental. iFrame. Qed. - (* TODO @Bastien Which formulation ? - 1) ([∗ list] la;lw ∈ (fun a => (a,v)) <$> (finz.seq_between b e);l, la ↦ₐ lw) - 2) ([∗ list] a;lw ∈ finz.seq_between b e;l, (a,v) ↦ₐ lw) - 3) Both - - Also, cf in logrel.v - *) Lemma region_integers_alloc' E (b e a: Addr) (v : Version) l p : Forall (λ lw, is_zL lw = true) l → ([∗ list] la;lw ∈ (fun a => (a,v)) <$> (finz.seq_between b e);l, la ↦ₐ lw) ={E}=∗ @@ -305,7 +298,7 @@ Section fundamental. iIntros "#Hl H". destruct p. { (* O *) rewrite fixpoint_interp1_eq //=. } 4: { (* E *) rewrite fixpoint_interp1_eq /=. - iDestruct (region_valid_alloc _ _ _ a _ _ RX with "Hl H") as ">#H"; auto. + iDestruct (region_valid_alloc _ RX _ _ a _ _ with "Hl H") as ">#H"; auto. iModIntro. iIntros (r). iDestruct (fundamental _ r with "H") as "H'". eauto. } all: iApply (region_valid_alloc with "Hl"); eauto. diff --git a/theories/logrel.v b/theories/logrel.v index 99bacd4d..c1aec4c5 100644 --- a/theories/logrel.v +++ b/theories/logrel.v @@ -451,7 +451,10 @@ Section logrel. Qed. (* Get the validity of a region containing only valid words *) - Lemma region_valid_alloc E (b e a: Addr) v l p : + Lemma region_valid_alloc + (E : coPset) + (p : Perm) (b e a : Addr ) (v : Version) + (l : list LWord) : PermFlowsTo RO p → ([∗ list] w ∈ l, interp w) -∗ ([∗ list] la;lw ∈ (fun a => (a,v)) <$> (finz.seq_between b e);l, la ↦ₐ lw) ={E}=∗ @@ -478,8 +481,9 @@ Section logrel. Qed. Lemma region_valid_alloc' - (E : coPset) ( b e a : Addr ) (la: list Addr) - (v : Version) (l : list LWord) (p : Perm) : + (E : coPset) + (p : Perm) ( b e a : Addr ) (v : Version) + (la: list Addr) (l : list LWord) : PermFlowsTo RO p → finz.seq_between b e ⊆+ la -> ([∗ list] w ∈ l, interp w) -∗ @@ -776,7 +780,7 @@ Section logrel. Definition compute_mask_range (E : coPset) (b e : Addr) (v : Version) : coPset := (compute_mask E (logical_range_set b e v)). - (* TODO @Bastien is there a way to generalize the opening of the list of invariant ? *) + (* TODO @June is there a way to generalize the opening of the list of invariant ? *) (* Lemma for opening invariants of a region *) Lemma open_region_inv (E : coPset) diff --git a/theories/proofmode/proofmode_instr_rules.v b/theories/proofmode/proofmode_instr_rules.v index cae2d4f1..da7c8251 100644 --- a/theories/proofmode/proofmode_instr_rules.v +++ b/theories/proofmode/proofmode_instr_rules.v @@ -126,6 +126,6 @@ Ltac dispatch_instr_rule instr cont := | Halt => cont (@wp_halt) (* not found *) (* TODO @Denis EInit, EDeInit, EStoreId *) - (* TODO @Bastien IsUnique *) + (* TODO @June IsUnique *) | _ => fail "No suitable rule found for instruction" instr end. diff --git a/theories/rules/rules_IsUnique.v b/theories/rules/rules_IsUnique.v index 7fda6760..f8537d75 100644 --- a/theories/rules/rules_IsUnique.v +++ b/theories/rules/rules_IsUnique.v @@ -19,7 +19,7 @@ Section cap_lang_rules. Implicit Types mem : Mem. Implicit Types lmem : LMem. - (* TODO @Bastien: keep the lemma around, + (* TODO @June: keep the lemma around, until doing the proof in a `wp_opt2` style *) Lemma incrementLPC_incrementPC_some regs regs' : diff --git a/theories/stdpp_extra.v b/theories/stdpp_extra.v index 8a2797cc..1dc076b5 100644 --- a/theories/stdpp_extra.v +++ b/theories/stdpp_extra.v @@ -1445,6 +1445,49 @@ Proof. ; by destruct (m2 !! k) as [v2|] eqn:Hk_m2; simplify_map_eq. Qed. +Lemma list_remove_elem_cons + `{A : Type} `{EqDecision A} (a : A) (la : list A) : + a ∉ la -> + (list_remove_elem a (a::la)) = (list_remove_elem a la). +Proof. + intros Hnotin. + apply list_remove_elem_notin in Hnotin. + assert (a ∈ a::la) as Hin by set_solver. + apply list_remove_elem_in in Hin. + destruct Hin as (la' & Hla' & Hin). + rewrite Hnotin Hla'. + cbn in Hin. + rewrite decide_True /= in Hin ; [done|]. + by inversion Hin. +Qed. + +Lemma list_remove_elem_idem + `{A : Type} `{EqDecision A} (a : A) (la : list A) : + NoDup la -> + (list_remove_elem a (list_remove_elem a la)) = + (list_remove_elem a la). +Proof. + intros HNoDup. + rewrite list_remove_elem_notin; last done. + by apply not_elemof_list_remove_elem. +Qed. + +Lemma list_remove_elem_neq + `{A : Type} `{EqDecision A} (a a' : A) (la : list A) : + NoDup la -> + a' ∈ la -> + a ∈ list_remove_elem a' la -> + a ≠ a'. +Proof. + intros HnoDup Hin Hrem. + pose proof (Hin' := Hin). + apply list_remove_elem_in in Hin. + destruct Hin as (la' & Hla' & Hrem'); subst. + apply not_elemof_list_remove_list in Hrem'; auto. + set_solver. +Qed. + + Lemma prod_merge_none_l {K A B} `{Countable K} (m1 : gmap K A) (m2 : gmap K B) (k : K) : m2 !! k = None -> @@ -1494,6 +1537,9 @@ Proof. rewrite lookup_delete_ne in Hprod; auto. Qed. +Lemma not_or {P Q : Prop} : ¬(P \/ Q) ↔ ¬P /\ ¬Q. +Proof. tauto. Qed. + (* TODO: integrate into stdpp? *) Lemma pair_eq_inv {A B} {y u : A} {z t : B} {x} : x = (y, z) -> x = (u, t) ->