From 6ff64954df14d49a72bf8feaa2e561642e6b0cc7 Mon Sep 17 00:00:00 2001 From: June Rousseau Date: Sat, 14 Sep 2024 18:42:13 +0200 Subject: [PATCH] WIP refactor FTRL, proof QED, still need some refactoring --- theories/ftlr/IsUnique.v | 849 +++++++++++++++++++++++---------------- theories/machine_base.v | 7 + theories/stdpp_extra.v | 43 ++ 3 files changed, 553 insertions(+), 346 deletions(-) diff --git a/theories/ftlr/IsUnique.v b/theories/ftlr/IsUnique.v index 105678fc..267e3ff1 100644 --- a/theories/ftlr/IsUnique.v +++ b/theories/ftlr/IsUnique.v @@ -18,55 +18,18 @@ Section fundamental. Local Hint Resolve finz_seq_between_NoDup list_remove_elem_NoDup : core. - Lemma regname_decidable (r1 r2 : RegName) : - Decidable.decidable (r1 = r2). - intros. - unfold Decidable.decidable. - destruct (decide (r1 = r2)) ; [by left |by right]. - 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. + Set Nested Proofs Allowed. - 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; first done. - by apply not_elemof_list_remove_elem. - Qed. + Definition reg_allows_sweep (lregs : LReg) (r : RegName) p b e a v := + lregs !! r = Some (LCap p b e a v) ∧ readAllowed p = true. - 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'. + Lemma reg_allows_sweep_dec lregs p r b e a v: + Decidable.decidable (reg_allows_sweep lregs r p b e a v). 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. - + Admitted. + Lemma lookup_dec (lregs : LReg) src w : + Decidable.decidable (lregs !! src = w). + Admitted. Definition allow_sweep_mask (la : list Addr) (v : Version) (pc_a : Addr) (pc_v : Version) : coPset := @@ -85,21 +48,20 @@ Section fundamental. Definition region_open_resources (pc_a : Addr) (pc_v : Version) (la : list Addr) (v : Version) - (lws : list LWord) (Ps : list D) (b : bool) + (lws : list LWord) (Ps : list D) (has_later : bool) : iProp Σ := let E := ⊤ ∖ ↑logN.@(pc_a, pc_v) in let E' := allow_sweep_mask la v pc_a pc_v in - ([∗ list] lw;Pw ∈ lws;Ps, (if b then ▷ (Pw : D) lw else (Pw : D) lw)) - (* ∗ ( ⌜ Persistent ([∗ list] lw;Pw ∈ lws;Ps, (Pw : D) lw) ⌝ ) *) - ∗ ([∗ list] Pa ∈ Ps, read_cond Pa interp) - ∗ ( (▷ ([∗ list] a_Pa ∈ zip la Ps, (interp_ref_inv a_Pa.1 v a_Pa.2))) - ={E', E }=∗ True). - - Definition reg_allows_sweep (lregs : LReg) (r : RegName) p b e a v := - lregs !! r = Some (LCap p b e a v) ∧ readAllowed p = true. - + ([∗ 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). (* 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 @@ -221,7 +183,7 @@ Section fundamental. (lregs : LReg) (r : RegName) (pc_a : Addr) (pc_v : Version) (pc_lw : LWord) (p : Perm) (b e a : Addr) (v : Version) - (lmem : LMem) (Ps : list D) := + (lmem : LMem) (Ps : list D) (has_later : bool):= let la := (list_remove_elem pc_a (finz.seq_between b e)) in let cond_open := @@ -233,14 +195,14 @@ Section fundamental. then (∃ (lws : list LWord), ⌜length lws = length la⌝ ∗ ⌜lmem = <[(pc_a, pc_v):=pc_lw]> (logical_region_map la lws v)⌝ - ∗ region_open_resources pc_a pc_v la v lws Ps true) + ∗ region_open_resources pc_a pc_v la v lws Ps has_later) else ⌜lmem = <[(pc_a, pc_v):=pc_lw]> ∅⌝)%I. - Lemma sweep_res_implies_mem_map: - ∀ (lregs : leibnizO LReg) - (pc_a : Addr) (pc_v : Version) (pc_lw : LWord) (r : RegName) - (p : Perm) (b e a : Addr) (v : Version) (Ps : list D), + Lemma sweep_res_implies_mem_map + (lregs : leibnizO LReg) + (pc_a : Addr) (pc_v : Version) (pc_lw : LWord) (r : RegName) + (p : Perm) (b e a : Addr) (v : Version) (Ps : list D) : let la := (list_remove_elem pc_a (finz.seq_between b e)) in let E := ⊤ ∖ ↑logN.@(pc_a, pc_v) in @@ -253,126 +215,117 @@ Section fundamental. -∗ (pc_a, pc_v) ↦ₐ pc_lw ={ E ,if cond_open then E' else E}=∗ ∃ lmem : LMem, - allow_sweep_mem lregs r pc_a pc_v pc_lw p b e a v lmem Ps + allow_sweep_mem lregs r pc_a pc_v pc_lw p b e a v lmem Ps true ∗ ▷ ([∗ map] la↦lw ∈ lmem, la ↦ₐ lw). - Admitted. - (* iMod (sweep_res_implies_mem_map with "HSweepRes Ha") *) - (* as (lws) "(%Hlen_lws & Hmem & Hreg_open)". *) - (* Proof. *) - (* intros lregs a a0 v v0 lw r p1 b1 e1. *) - (* iIntros "HStoreRes Ha". *) - (* iDestruct "HStoreRes" as "(% & HStoreRes)". *) - - (* case_decide as Hallows. *) - (* - iMod "HStoreRes" as (lw0) "[Ha0 HStoreRest]". *) - (* iExists _. *) - (* iSplitL "HStoreRest". *) - (* * iFrame "%". *) - (* case_decide; last by exfalso. *) - (* iExists lw0. iSplitR; auto. *) - (* * iModIntro. iNext. *) - (* destruct Hallows as ((Hrinr & Hra & Hwb) & Hne). *) - (* iApply memMap_resource_2ne; auto; iFrame. *) - (* - iExists _. *) - (* iSplitR "Ha". *) - (* + iFrame "%". *) - (* case_decide; first by exfalso. auto. *) - (* + iModIntro. iNext. by iApply memMap_resource_1. *) - (* Qed. *) - - (* Definition allow_sweep_map_or_true (r : RegName) (lregs : LReg) (lmem : LMem):= *) - (* ∃ p b e a v, *) - (* read_reg_inr lregs r p b e a v ∧ *) - (* if decide (reg_allows_sweep lregs r p b e a v) *) - (* then ∃ lw, lmem !! (a, v) = Some lw *) - (* else True. *) + Proof. + intros *. + iIntros "HSweepRes Hpc_a". + iDestruct "HSweepRes" as "(%Hread & HSweepRes)". + subst cond_open. + case_decide as Hallows; cycle 1. + - iExists _. + iSplitR "Hpc_a". + + iFrame "%". + 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 $Hpc_a]") 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. Lemma mem_map_implies_pure_conds: ∀ (lregs : leibnizO LReg) (pc_a : Addr) (pc_v : Version) (pc_lw : LWord) (r : RegName) - (lmem : LMem) (p : Perm) (b e a : Addr) (v : Version) (Ps : list D), - allow_sweep_mem lregs r pc_a pc_v pc_lw p b e a v lmem Ps + (lmem : LMem) (p : Perm) (b e a : Addr) (v : Version) (Ps : list D) + (has_later : bool), + allow_sweep_mem lregs r pc_a pc_v pc_lw p b e a v lmem Ps has_later -∗ ⌜lmem !! (pc_a, pc_v) = Some pc_lw⌝. - (* ∗ ⌜allow_sweep_map_or_true r lregs lmem⌝. *) Proof. - iIntros (lregs pc_a pc_v pc_lw r lmem p b e a v Ps) "HSweepMem". + iIntros (lregs pc_a pc_v pc_lw r lmem p b e a v Ps has_later) "HSweepMem". iDestruct "HSweepMem" as "(% & HSweepRes)". case_decide as Hallows. - pose (Hallows' := Hallows). destruct Hallows' as ((Hreg & Hread) & Hdecide). iDestruct "HSweepRes" as (lws) "(%Hlen & -> & HSweepRest)". by simplify_map_eq. - (* iSplitR. by simplify_map_eq. *) - (* iExists p,b,e,a,v. iSplit;auto. *) - (* case_decide;auto. *) - (* exists lw0. by simplify_map_eq. *) - iDestruct "HSweepRes" as "->". by simplify_map_eq. - (* iSplitR. by simplify_map_eq. *) - (* iExists p,b,e,a0,v0. repeat iSplitR; auto. *) - (* case_decide as Hdec1; last by done. *) - (* apply not_and_l in Hallows as [Hallows | Hallows]; try contradiction. *) - (* assert ((a0, v0) = (a, v)) as ->. *) - (* { f_equal; [apply finz_to_z_eq, Z.eq_dne | apply Nat.eq_dne] *) - (* ; intros Hcontr *) - (* ; apply Hallows *) - (* ; intro ; simplify_eq. *) - (* } *) - (* simplify_map_eq. eauto. *) Qed. - (* Lemma mem_map_recover_res: *) - (* ∀ (lregs : leibnizO LReg) *) - (* (pc_a : Addr) (pc_v : Version) (pc_lw : LWord) *) - (* (r : RegName) *) - (* p (b e a : Addr) (v : Version) *) - (* (lmem : LMem) *) - (* (Ps : list D) *) - (* (lws : list LWord) *) - (* storev loadv, *) - - (* let la := (list_remove_elem pc_a (finz.seq_between b e)) in *) - (* let E := ⊤ ∖ ↑logN.@(pc_a, pc_v) in *) - (* let E' := allow_sweep_mask la v pc_a pc_v in *) - (* let open_cond := decide (reg_allows_sweep lregs r p b e a v /\ (r = PC \/ a ∉ la)) in *) - (* let lws' := *) - - - (* reg_allows_sweep lregs r p b e a v *) - (* (* → lmem !! (a,v) = Some loadv *) *) - (* → allow_sweep_mem lregs r pc_a pc_v pc_lw p b e a v lmem Ps *) - (* -∗ ([∗ map] la↦lw ∈ (<[(a0,v0):=storev]> lmem), la ↦ₐ lw) *) - (* -∗ interp storev *) - - (* ={E', E}=∗ *) - - (* if open_cond *) - (* then (* updated memory *) *) - (* (a,v) ↦ₐ storev *) - (* else (* previous, non-updated memory *) *) - (* (a,v) ↦ₐ lw. *) - - (* Proof. *) - (* intros lregs a v lw src p0 b0 e0 a0 v0 lmem storev loadv Hrar Hloadv. *) - (* iIntros "HLoadMem Hmem Hvalid". *) - (* iDestruct "HLoadMem" as "[% HLoadRes]". *) - (* case_decide as Hdec. destruct Hdec as [Hallows Heq]. *) - (* - destruct Hallows as [Hrinr [Hra Hwb] ]. *) - (* iDestruct "HLoadRes" as (lw0) "[-> [Hval Hcls] ]". *) - (* simplify_map_eq. rewrite insert_insert. *) - (* rewrite memMap_resource_2ne; last auto. iDestruct "Hmem" as "[Ha1 Haw]". *) - (* iMod ("Hcls" with "[Ha1 Hvalid]") as "_";[iNext;iExists storev;iFrame|]. iModIntro. *) - (* rewrite decide_False; [done|]. apply not_and_r. right. auto. *) - (* - apply not_and_r in Hdec as [| <-%dec_stable]. *) - (* * by exfalso. *) - (* * iDestruct "HLoadRes" as "->". *) - (* rewrite insert_insert. *) - (* rewrite -memMap_resource_1. simplify_map_eq. *) - (* by iFrame. *) - (* Qed. *) + Lemma allow_sweep_mem_later + (lregs : leibnizO LReg) + (pc_a : Addr) (pc_v : Version) (pc_lw : LWord) (r : RegName) + (lmem : LMem) (p : Perm) (b e a : Addr) (v : Version) (Ps : list D) : + allow_sweep_mem lregs r pc_a pc_v pc_lw p b e a v lmem Ps true + -∗ ▷ allow_sweep_mem lregs r pc_a pc_v pc_lw p b e a v lmem Ps false. + Proof. + iIntros "HSweepMem". + iDestruct "HSweepMem" as "[% HSweepMem]". + rewrite !/allow_sweep_mem /=. iSplit;[auto|]. + case_decide. + - iApply later_exist_2. iDestruct "HSweepMem" as (lws) "(%&%&HSweepRest)". + iExists lws. iDestruct "HSweepRest" as "(?&?&?&?)". + iFrame "%∗". + iNext ; iFrame. + - iNext; iFrame. + Qed. + Lemma mem_map_recover_res_noup + (lregs : leibnizO LReg) (lmem : LMem) + (pc_a : Addr) (pc_v : Version) (pc_lw : LWord) + (r : RegName) + (p : Perm) (b e a : Addr) (v : Version) + (Ps : list D) : + + let la := (list_remove_elem pc_a (finz.seq_between b e)) in + let E := ⊤ ∖ ↑logN.@(pc_a, pc_v) in + let E' := allow_sweep_mask la v pc_a pc_v in + let cond_open := + decide (reg_allows_sweep lregs r p b e a v /\ (r = PC \/ pc_a ∉ (finz.seq_between b e))) + in + length la = length Ps -> + allow_sweep_mem lregs r pc_a pc_v pc_lw p b e a v lmem Ps false + -∗ ([∗ map] la↦lw ∈ lmem, la ↦ₐ lw) + ={(if cond_open then E' else E), E}=∗ + (pc_a,pc_v) ↦ₐ pc_lw. + Proof. + intros * Hlen_Ps; iIntros "HSweepMem Hmem". + iDestruct "HSweepMem" as "(%Hread & HSweepMem)". + subst cond_open; set (cond_open := decide _). + destruct cond_open as [Hdecide|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_pca; auto. + iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]"; auto. + { + apply logical_region_notin; auto. + apply not_elemof_list_remove_elem; auto. + } + iMod ("Hcls_src" with "[Hmem HPrange]") as "_". + { + iNext. + iApply region_inv_construct; auto. + iExists (lws); iFrame "∗ %". + } + iModIntro; iFrame. + Qed. (* TODO @June redo the proof in the same style as Load or Store *) @@ -409,31 +362,28 @@ Section fundamental. (* 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) "[%HlenPs HSweepRes]" + iDestruct (create_sweep_res with "[$Hreg] [$Hinv] [%]") as (Ps) "[%Hlen_Ps HSweepRes]" ; [ eassumption | by apply elem_of_finz_seq_between |]. - (* Set Nested Proofs Allowed. *) - (* rewrite /allow_sweep_res. *) - - (* 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.@(apc, vpc)). set (E' := allow_sweep_mask (list_remove_elem apc (finz.seq_between bsrc esrc)) vsrc apc vpc). - rewrite /allow_sweep_mem. set (cond_open := decide (reg_allows_sweep (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src psrc bsrc esrc asrc vsrc ∧ (src = PC ∨ apc ∉ finz.seq_between bsrc esrc)) ). - - (* (* Step 3: derive the non-spatial conditions over the memory map*) *) + (* Step 3: derive the non-spatial conditions over the memory map*) iDestruct (mem_map_implies_pure_conds with "HSweepMem") as %HReadPC. - (* as %(HReadPC & HSweepAP); auto. *) - (* iDestruct (mem_map_implies_pure_conds with "HSweepMem") as %(HReadPC & HSweepAP); auto. *) + + (* Step 4: move the later outside, so that we can remove it after applying wp_load *) + iDestruct (allow_sweep_mem_later with "HSweepMem") as "HSweepMem"; auto. + + iApply (wp_isunique with "[$Hmap $HMemRes]") ; eauto @@ -454,212 +404,419 @@ Section fundamental. ; 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. + ; try (cbn in Hlwsrc' ; simplify_eq). - (* TODO So basically, here, the proof of - sweep false, sweep true seal, and sweep fail are very similar, - because it is just about closing the memory resources that DIDN'T change. - *) - { (* Sweep false *) - (* TODO here, it is basically the same proof twice !! *) + { (* Sweep true cap : update *) + + rewrite /allow_sweep_mem. + subst cond_open; set (cond_open := decide (_ /\ _)). iDestruct "HSweepMem" as "(_ & HSweepMem)". destruct cond_open as [Hdecide|Hdecide]; cycle 1. + iDestruct "HSweepMem" as "->". iModIntro. - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]";auto. - iMod ("Hcls" with "[Ha HP]") as "_". - iNext; iExists lwpc ; 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. + rewrite /read_reg_inr Hlwsrc' in HVsrc; simplify_eq. + apply Decidable.not_and in Hdecide; last apply reg_allows_sweep_dec. - + iDestruct "HSweepMem" as (lws Hlen_lws ->) "(HPrange & HPs_read & Hcls_src)". - subst E'; rewrite !allow_sweep_mask_remove_pca; auto. - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]"; auto. + destruct Hdecide as [Hdecide|Hdecide]; cycle 1. { - apply logical_region_notin; auto. - apply not_elemof_list_remove_elem; auto. + exfalso. + apply Decidable.not_or in Hdecide. + destruct Hdecide as [Hsrc_neq_PC Hapc_overlap]. + apply Decidable.not_not in Hapc_overlap. + 2: admit. (* easy *) + clear -Hunique_regs Hapc_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 Hapc_overlap. + destruct (bsrc |Hpsrc_O]; last (destruct psrc ; try done). + assert (src ≠ PC) as Hsrc_ne_pc. + { intro ; subst ; inversion i ; inversion H1 ; cbn in * ; simplify_map_eq. + destruct H8 ; done. + } + assert ( lmem' !! (apc, vpc) = Some lwpc ) as Hmem'_pca. + { eapply is_valid_updated_lmemory_preserves_lmem; cycle 1 ; eauto. } + rewrite -(insert_id lmem' (apc,vpc) lwpc);auto. + iDestruct (big_sepM_insert_delete with "Hmem") as "[Hmem _]". + iMod ("Hcls" with "[Hmem HP]");[iExists lwpc;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 O bsrc esrc asrc (vsrc + 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)); 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. + } + + destruct Hdecide as [ [Hsrc_lregs Hread_src] Hvalid_sweep]. + destruct (decide (src = PC)) as [->|Hsrc_ne_pc]; [clear Hvalid_sweep |]. + - (* src = PC *) + incrementLPC_inv + as (p_pc' & b_pc' & e_pc' &a_pc' &v_pc' & ? & HPC & Z & Hregs') + ; simplify_map_eq. - iMod ("Hcls_src" with "[Hmem HPrange]") as "_". - { - iNext. - iApply region_inv_construct; auto. - iExists (lws); iFrame "∗ %". + iDestruct "HSweepMem" as (lws Hlen_lws ->) "HSweepRest". + subst E'. + rewrite /read_reg_inr in HVsrc; simplify_map_eq. + set (la' := (list_remove_elem asrc (finz.seq_between bsrc esrc)) ). + + assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq); simplify_map_eq. + do 2 (rewrite (insert_commute _ _ PC) //); + rewrite !insert_insert. + + assert (a_pc' ∈ finz.seq_between b_pc' e_pc') as Hapc_in_range. + admit. (* easy, because isCorrectLPC *) + + + assert ( lmem' !! (a_pc', vsrc) = Some lwpc ) as Hmem'_pca. + { eapply is_valid_updated_lmemory_preserves_lmem; cycle 1 ; eauto. + by simplify_map_eq. } - iModIntro. - iMod ("Hcls" with "[Ha HP]") as "_". - iNext; iExists lwpc ; 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 ( lmem' !! (a_pc', vsrc+1) = Some lwpc ) 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. } - iModIntro. - rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. - } - { (* Sweep true : sealed *) - (* TODO here, it is basically the same proof twice !! *) - iDestruct "HSweepMem" as "(_ & HSweepMem)". - destruct cond_open as [Hdecide|Hdecide]; cycle 1. - + iDestruct "HSweepMem" as "->". - iModIntro. - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]";auto. - iMod ("Hcls" with "[Ha HP]") as "_". - iNext; iExists lwpc ; 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). } + assert (logical_region_map la' lws vsrc !! (a_pc', vsrc) = None) + as Hasrc_notin_reg_la'. + { subst la'. + eapply logical_region_notin; eauto. + apply not_elemof_list_remove_elem; eauto. + }. + + + assert ( ((logical_region_map la' lws) ) vsrc ⊆ 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_pc' e_pc')) + ; eauto. + eapply is_valid_updated_lmemory_insert'; eauto. + subst la'. + eapply Forall_forall; intros a Ha. + eapply logical_region_version_neq; eauto ; last lia. } - iModIntro. - rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto. - - + iDestruct "HSweepMem" as (lws Hlen_lws ->) "(HPrange & HPs_read & Hcls_src)". - subst E'; rewrite !allow_sweep_mask_remove_pca; auto. - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]"; auto. + assert ( ((logical_region_map la' lws) ) (vsrc+1) ⊆ lmem' ) + as Hmem'_be_next. { - apply logical_region_notin; auto. - apply not_elemof_list_remove_elem; auto. + eapply map_subseteq_spec; intros [a' v'] lw' Hlw'. + assert (v' = vsrc+1 /\ (a' ∈ la')) + as [? Ha'_in_be] by (subst la' ; eapply logical_region_map_some_inv; eauto) + ; simplify_eq. + destruct Hupd. + eapply lookup_weaken; last eapply H0. + 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 ; subst la'. + apply not_elemof_list_remove_elem in Ha'_in_be ; auto. + } + { subst la'. + 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. + } } - iMod ("Hcls_src" with "[Hmem HPrange]") as "_". + rewrite -(insert_id lmem' (a_pc', vsrc) lwpc); auto. + iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha Hmem]". + + rewrite -(insert_id (_ lmem') (a_pc', vsrc+1) lwpc); 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', vsrc) : LAddr)) in Hmem'_be + ; last (eapply logical_region_notin; eauto). + eapply delete_subseteq_r with (k := ((a_pc', vsrc+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', vsrc) : LAddr)) in Hmem'_be_next + ; last (eapply logical_region_notin ; eauto). + eapply delete_subseteq_r with (k := ((a_pc', vsrc+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, vsrc)) 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 "HSweepRest" as "(HPrange & %Hpers & #Hread_cond & Hcls_src)". + iDestruct "HPrange" as "#HPrange". + iDestruct "HP" as "#HP". + + iMod ("Hcls_src" with "[Hrange HPrange]") as "_". { iNext. - iApply region_inv_construct; auto. - iExists (lws); iFrame "∗ %". + iApply region_inv_construct; try done. + subst la' ; auto. + iExists lws; iSplit ; first done; iFrame "#∗". } - iModIntro. - iMod ("Hcls" with "[Ha HP]") as "_". - iNext; iExists lwpc ; iFrame. + iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame "#∗"). iModIntro. + + iMod (region_valid_alloc' _ b_pc' e_pc' a_pc' (a_pc'::la') (vsrc +1) (lwpc::lws) p_pc' + with "[HPrange HP] [Hrange' Ha_next]") + as "#Hinterp_src_next". + { destruct p_pc' ; cbn in * ; try congruence; done. } + { subst la' ; eapply list_remove_list_region ; auto. + admit. (* easy because a_pc' ∈ .... *) + } + { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_PSRC". + 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. + 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 "_". - 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. + 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. + { 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. } + admit. (* easy *) + admit. + admit. + admit. + + - (* src ≠ PC *) + destruct Hvalid_sweep as [Hcontra|Hapc_notin_src] ; first done. + + 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 lwpc ) as Hmem'_pca. + { eapply is_valid_updated_lmemory_preserves_lmem; eauto. } + + + assert ( logical_range_map bsrc esrc lws vsrc ⊆ lmem' ) + as Hmem'_be. + { + eapply is_valid_updated_lmemory_lmem_incl with + (la := (finz.seq_between bsrc esrc)) (v := vsrc) + ; 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. + } + + assert + (logical_range_map bsrc esrc lws (vsrc + 1) ⊆ lmem') + as Hmem'_be_next. + { clear -Hupd Hlen_lws Hapc_notin_src. + eapply map_subseteq_spec; intros [a' v'] lw' Hlw'. + assert (v' = vsrc+1 /\ (a' ∈ (finz.seq_between bsrc esrc))) + 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') lwpc); 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, vsrc)) (finz.seq_between bsrc esrc)) 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 (region_valid_alloc _ bsrc esrc asrc (vsrc +1) lws psrc + with "[HPrange] [Hrange']") + as "#Hinterp_src_next". + { destruct psrc ; cbn in * ; try congruence; done. } + { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_PSRC". + 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 Hread_PSRC 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_pc 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. } } - { (* Fail *) - iDestruct "HSweepMem" as "(_ & HSweepMem)". - destruct cond_open as [Hdecide|Hdecide]; cycle 1. - + iDestruct "HSweepMem" as "->". - iModIntro. - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]";auto. - iMod ("Hcls" with "[Ha HP]") as "_". - iNext; iExists lwpc ; iFrame. - iModIntro. - iApply wp_pure_step_later; auto. - iNext; iIntros "_"; iApply wp_value; auto. - iIntros; discriminate. - + iDestruct "HSweepMem" as (lws Hlen_lws ->) "(HPrange & HPs_read & Hcls_src)". - subst E'; rewrite !allow_sweep_mask_remove_pca; auto. - iDestruct (big_sepM_insert with "Hmem") as "[Ha Hmem]"; auto. - { - apply logical_region_notin; auto. - apply not_elemof_list_remove_elem; auto. - } - iMod ("Hcls_src" with "[Hmem HPrange]") as "_". - { - iNext. - iApply region_inv_construct; auto. - iExists (lws); iFrame "∗ %". - } - iModIntro. - iMod ("Hcls" with "[Ha HP]") as "_". - iNext; iExists lwpc ; iFrame. - iModIntro. - iApply wp_pure_step_later; auto. - iNext; iIntros "_"; iApply wp_value; auto. - iIntros; discriminate. + + + + { (* Sweep false *) + + iMod (mem_map_recover_res_noup with "HSweepMem Hmem") as "Ha"; auto. + subst E. + iModIntro. + iMod ("Hcls" with "[Ha HP]") as "_"; [iNext; iExists lwpc ; 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 true cap : update *) + { (* Sweep sealed *) + iMod (mem_map_recover_res_noup with "HSweepMem Hmem") as "Ha"; auto. + subst E. + iModIntro. + iMod ("Hcls" with "[Ha HP]") as "_"; [iNext; iExists lwpc ; 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. + } - iDestruct "HSweepMem" as "(_ & HSweepMem)". - destruct cond_open as [Hdecide|Hdecide]; cycle 1. - + iDestruct "HSweepMem" as "->". - iModIntro. - (* !! contradiction here !! *) - exfalso. - rewrite /read_reg_inr Hlwsrc' in HVsrc; simplify_eq. + { (* Fail *) + iMod (mem_map_recover_res_noup with "HSweepMem Hmem") as "Ha"; auto. + subst E. + iModIntro. + iMod ("Hcls" with "[Ha HP]") as "_". + iNext; iExists lwpc ; iFrame. + iModIntro. + iApply wp_pure_step_later; auto. + iNext; iIntros "_"; iApply wp_value; auto. + iIntros; discriminate. + } - apply Decidable.not_and in Hdecide. - 2: admit. (* easy *) - destruct Hdecide as [Hdecide|Hdecide]. - { - rewrite /reg_allows_sweep in Hdecide. - apply Decidable.not_and in Hdecide. - 2: admit. (* easy *) - destruct Hdecide as [Hdecide|Hdecide]. - + by rewrite Hlwsrc' in Hdecide. - + clear -Hp_neq_E Hdecide. - destruct psrc ; auto. - admit. (* obviously wrong, not obvious where to fix this *) - } - { - apply Decidable.not_or in Hdecide. - destruct Hdecide as [Hsrc_neq_PC Hapc_overlap]. - apply Decidable.not_not in Hapc_overlap. - 2: admit. (* easy *) - clear -Hunique_regs Hapc_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 Hapc_overlap. - destruct (bsrc (match p with diff --git a/theories/stdpp_extra.v b/theories/stdpp_extra.v index 8a2797cc..f92fba67 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 ->