diff --git a/theories/logical_mapsto.v b/theories/logical_mapsto.v index 24cca550..35c8726f 100644 --- a/theories/logical_mapsto.v +++ b/theories/logical_mapsto.v @@ -1634,19 +1634,18 @@ Definition update_version_region_vmap (la : list Addr) (v : Version) (vmap : VMap) : VMap := foldr (fun a vm => update_version_addr_vmap a v vm) vmap la. -(* Lemma update_version_addr_lookup *) -(* (glmem llmem : LMem) (a a' : Addr) (v v': Version) (lw' : LWord) : *) -(* llmem !! (a', v') = Some lw' -> *) -(* llmem !! (a, v+1) = None -> *) -(* update_version_addr glmem a v llmem !! (a', v') = Some lw'. *) -(* Proof. *) -(* intros Hlw' Hmax. *) -(* rewrite /update_version_addr. *) -(* destruct (decide ((a', v') = (a,v))); simplify_map_eq. *) -(* rewrite lookup_insert_ne //=; by intro ; simplify_eq ; lia. *) -(* destruct (lmem !! (a,v)) as [lw|] eqn:Hlw; simplify_map_eq; last done. *) -(* rewrite lookup_insert_ne //=; intro ; simplify_eq; by rewrite Hlw' in Hmax. *) -(* Qed. *) +Lemma update_version_addr_lookup + (glmem llmem : LMem) (a a' : Addr) (v v': Version) (lw' : LWord) : + llmem !! (a', v') = Some lw' -> + llmem !! (a, v+1) = None -> + update_version_addr glmem a v llmem !! (a', v') = Some lw'. +Proof. + intros Hlw' Hmax. + rewrite /update_version_addr. + destruct (glmem !! (a,v)) eqn:Hglm;eauto. + destruct (decide ((a', v') = (a,v+1))); simplify_map_eq ; auto. + by rewrite Hmax in Hlw'. +Qed. Lemma update_version_region_vmap_lookup {vmap : VMap} {v la} : NoDup la -> @@ -1658,11 +1657,11 @@ Proof. - by rewrite lookup_insert. - rewrite lookup_insert_ne. + apply IHla; last done. - by apply (NoDup_cons_1_2 a). + by apply (NoDup_cons_1_2 a). + intros <-. apply (NoDup_cons_1_1 a la Hnd Ha'). Qed. - + Lemma update_version_addr_lookup_neq (glmem llmem : LMem) (a a' : Addr) (v v': Version) : a ≠ a' -> @@ -1674,78 +1673,94 @@ Proof. rewrite lookup_insert_ne //=; by intro ; simplify_eq. Qed. - Lemma update_version_region_mono +Lemma update_version_addr_mono + (glmem lmem1 lmem2 : LMem) (a : Addr) (v : Version) : + lmem1 ⊆ lmem2 -> + update_version_addr glmem a v lmem1 ⊆ update_version_addr glmem a v lmem2. +Proof. + intros Hincl. + rewrite /update_version_addr. + destruct (glmem !! (a,v)) as [lw|]; auto. + by apply insert_mono. +Qed. + +Lemma update_version_region_mono (glmem lmem1 lmem2 : LMem) (la : list Addr) (v : Version) : - lmem1 ⊆ lmem2 -> - update_version_region glmem la v lmem1 ⊆ update_version_region glmem la v lmem2. - Proof. - Admitted. - - Lemma update_version_addr_mono - (glmem1 glmem2 lmem1 lmem2 : LMem) (a : Addr) (v : Version) : - lmem1 !! (a,v+1) = None -> - glmem1 ⊆ glmem2 -> - lmem1 ⊆ lmem2 -> - update_version_addr glmem1 a v lmem1 ⊆ update_version_addr glmem2 a v lmem2. - Proof. - intros HlmemN Hglmem Hlmem. - unfold update_version_addr. - destruct (glmem1 !! (a,v)) eqn:Hglm1. - - rewrite (lookup_weaken _ _ _ _ Hglm1 Hglmem). - now eapply insert_mono. - - destruct (glmem2 !! (a,v)); last done. - now eapply insert_subseteq_r. - Qed. - - Lemma update_version_region_preserves_lmem - (glmem llmem : LMem) (la : list Addr) (a : Addr) (v : Version) : - update_version_region glmem la v llmem !! (a, v) = llmem !! (a, v). - Proof. - move: glmem llmem a v. - induction la as [|a' la IHla] ; intros *. - - by cbn in *. - - rewrite - /update_version_region /= - -/(update_version_region glmem la v llmem) - /update_version_addr. - destruct (glmem !! (a', v)) as [lwa|] eqn:Hlwa. - + rewrite lookup_insert_ne //=; last (intro ; simplify_eq ; lia). - + eapply IHla; eauto. - Qed. - - Lemma update_version_region_notin_preserves_lmem - (glmem llmem : LMem) (la : list Addr) (a' : Addr) (v v': Version) : - a' ∉ la -> - update_version_region glmem la v llmem !! (a', v') = llmem !! (a', v'). - Proof. - move: glmem llmem a' v v'. - induction la as [|a la IHla] ; intros * Ha'_notin_la. - - by cbn in *. - - destruct_cons. - rewrite - /update_version_region /= - -/(update_version_region glmem la v llmem) - /update_version_addr. - assert (update_version_region glmem la v llmem !! (a', v') = llmem !! (a', v')) - as IH by (eapply IHla ; eauto). - destruct (glmem !! (a, v)) as [lwa|] eqn:Hlwa; eauto. - rewrite lookup_insert_ne //=; intro ; simplify_eq ; lia. - Qed. - - Lemma update_version_region_mono2 - (glmem1 glmem2 lmem : LMem) (la : list Addr) (v : Version) : - NoDup la -> - Forall (fun a => lmem !! (a,v+1) = None) la -> - glmem1 ⊆ glmem2 -> - update_version_region glmem1 la v lmem ⊆ update_version_region glmem2 la v lmem. - Proof. - intros HNoDup HlmemNone Hglmem. - induction la; first done. - destruct_cons. - simpl. - eapply update_version_addr_mono; eauto. - rewrite update_version_region_notin_preserves_lmem; eauto. - Qed. + lmem1 ⊆ lmem2 -> + update_version_region glmem la v lmem1 ⊆ update_version_region glmem la v lmem2. +Proof. + induction la as [|a la IHla] ; intros Hincl ; cbn in *; eauto. + apply IHla in Hincl; clear IHla ; rename Hincl into IH. + rewrite -/(update_version_region glmem la v lmem1). + rewrite -/(update_version_region glmem la v lmem2). + by apply update_version_addr_mono. +Qed. + +(* Lemma update_version_addr_mono *) +(* (glmem1 glmem2 lmem1 lmem2 : LMem) (a : Addr) (v : Version) : *) +(* lmem1 !! (a,v+1) = None -> *) +(* glmem1 ⊆ glmem2 -> *) +(* lmem1 ⊆ lmem2 -> *) +(* update_version_addr glmem1 a v lmem1 ⊆ update_version_addr glmem2 a v lmem2. *) +(* Proof. *) +(* intros HlmemN Hglmem Hlmem. *) +(* unfold update_version_addr. *) +(* destruct (glmem1 !! (a,v)) eqn:Hglm1. *) +(* - rewrite (lookup_weaken _ _ _ _ Hglm1 Hglmem). *) +(* now eapply insert_mono. *) +(* - destruct (glmem2 !! (a,v)); last done. *) +(* now eapply insert_subseteq_r. *) +(* Qed. *) + +Lemma update_version_region_preserves_lmem + (glmem llmem : LMem) (la : list Addr) (a : Addr) (v : Version) : + update_version_region glmem la v llmem !! (a, v) = llmem !! (a, v). +Proof. + move: glmem llmem a v. + induction la as [|a' la IHla] ; intros *. + - by cbn in *. + - rewrite + /update_version_region /= + -/(update_version_region glmem la v llmem) + /update_version_addr. + destruct (glmem !! (a', v)) as [lwa|] eqn:Hlwa. + + rewrite lookup_insert_ne //=; last (intro ; simplify_eq ; lia). + + eapply IHla; eauto. +Qed. + +Lemma update_version_region_notin_preserves_lmem + (glmem llmem : LMem) (la : list Addr) (a' : Addr) (v v': Version) : + a' ∉ la -> + update_version_region glmem la v llmem !! (a', v') = llmem !! (a', v'). +Proof. + move: glmem llmem a' v v'. + induction la as [|a la IHla] ; intros * Ha'_notin_la. + - by cbn in *. + - destruct_cons. + rewrite + /update_version_region /= + -/(update_version_region glmem la v llmem) + /update_version_addr. + assert (update_version_region glmem la v llmem !! (a', v') = llmem !! (a', v')) + as IH by (eapply IHla ; eauto). + destruct (glmem !! (a, v)) as [lwa|] eqn:Hlwa; eauto. + rewrite lookup_insert_ne //=; intro ; simplify_eq ; lia. +Qed. + +(* Lemma update_version_region_mono2 *) +(* (glmem1 glmem2 lmem : LMem) (la : list Addr) (v : Version) : *) +(* NoDup la -> *) +(* Forall (fun a => lmem !! (a,v+1) = None) la -> *) +(* glmem1 ⊆ glmem2 -> *) +(* update_version_region glmem1 la v lmem ⊆ update_version_region glmem2 la v lmem. *) +(* Proof. *) +(* intros HNoDup HlmemNone Hglmem. *) +(* induction la; first done. *) +(* destruct_cons. *) +(* simpl. *) +(* eapply update_version_addr_mono; eauto. *) +(* rewrite update_version_region_notin_preserves_lmem; eauto. *) +(* Qed. *) (* Lemma update_version_region_preserves_lmem' *) (* (glmem llmem : LMem) (la : list Addr) (a' : Addr) (v v': Version) (lw' : LWord) : *) @@ -2168,12 +2183,77 @@ Proof. - eapply update_version_addr_preserves_mem_vmap_root ; eauto. Qed. +Lemma update_version_addr_preserves_notin_not_access + (lm lm' : LMem) (a : Addr) (vmap vmap': VMap) (v : Version) (a' : Addr) : + a ≠ a' -> + lm ⊆ lm' -> + is_Some (lm !! (a', v)) -> + is_cur_addr (a', v) vmap -> + lm !! (a' , v+1) = None -> + lmem_not_access_addrL lm' vmap' a -> + lmem_not_access_addrL (update_version_addr lm a' v lm') + (update_version_addr_vmap a' v vmap') a. +Proof. + intros Hneq Hincl [lw Hlm] Hcur Hmaxv Hnot_access. + rewrite /update_version_addr /update_version_addr_vmap. + (* assert (lm !! (a', v) = Some lw) as Hlm by (eapply lookup_weaken; eauto). *) + rewrite Hlm. + (* extract as a lemma ? *) + (* rewrite /lmem_not_access_addrL in Hnot_access |- *. *) + (* rewrite map_Forall_insert; eauto. *) + (* split. intro. *) + (* eapply Hnot_access; eauto. eapply lookup_weaken; eauto. *) +Admitted. + +Lemma update_version_addr_expands (lm lm' : LMem) (a : Addr) ( v : Version ) : + lm ⊆ lm' -> + lm !! (a, v + 1) = None -> + lm ⊆ update_version_addr lm a v lm'. +Proof. + intros Hincl Hmaxv. + rewrite /update_version_addr. + destruct (lm !! (a,v)) as [lw|]; eauto. + eapply insert_subseteq_r; eauto. +Qed. + +Lemma update_version_region_expands (lm : LMem) (la : list Addr) (v : Version) : + NoDup la -> + Forall (fun a => lm !! (a , v+1) = None) la -> + lm ⊆ update_version_region lm la v lm. +Proof. + induction la as [|a la IHla] ; cbn in * ; eauto. + intros HNoDup HmaxMap ; destruct_cons. apply IHla in HNoDup_la; eauto. + rewrite -/(update_version_region lm la v lm). + eapply update_version_addr_expands; eauto. +Qed. + +Lemma update_version_region_preserves_notin_not_access + (lm : LMem) (la : list Addr) (vmap : VMap) (v : Version) (a : Addr) : + a ∉ la -> + NoDup la -> + Forall (fun a => is_Some (lm !! (a , v))) la -> + Forall (fun a => is_cur_addr (a , v) vmap) la -> + Forall (fun a => lm !! (a , v+1) = None) la -> + lmem_not_access_addrL lm vmap a -> + lmem_not_access_addrL (update_version_region lm la v lm) + (update_version_region_vmap la v vmap) a. +Proof. + move: a. + induction la as [|a' la]; intros a Hnotin HNoDup Hmap HcurMap HmaxvMap Hnot_access; cbn; auto. + rewrite -/(update_version_region lm la v lm). + rewrite -/(update_version_region_vmap la v vmap). + destruct_cons. + apply IHla in Hnot_access; eauto. + eapply update_version_addr_preserves_notin_not_access; eauto. + apply update_version_region_expands; auto. +Qed. Lemma update_version_region_preserves_mem_corresponds (phm : Mem) (lm lm': LMem) (vmap vmap' : VMap) (la : list Addr) v: vmap' = update_version_region_vmap la v vmap -> lm' = update_version_region lm la v lm -> NoDup la → + Forall (fun a => is_Some (lm !! (a, v))) la -> Forall (fun a => is_cur_addr (a , v) vmap) la -> Forall (fun a => lm !! (a , v+1) = None) la -> Forall (fun a => lmem_not_access_addrL lm vmap a) la → @@ -2181,19 +2261,30 @@ Lemma update_version_region_preserves_mem_corresponds mem_phys_log_corresponds phm lm' vmap'. Proof. move: phm lm lm' vmap vmap'. - induction la as [| a la IH]; intros * -> -> Hno_dup Hcur Hmax Hall_naccess_mem Hmem_corr. + induction la as [| a la IH]; intros * -> -> Hno_dup Hmap Hcur Hmax Hall_naccess_mem Hmem_corr. - by cbn in * ; simplify_eq. - destruct_cons. assert (mem_phys_log_corresponds phm (update_version_region lm la v lm) (update_version_region_vmap la v vmap)) as Hinv by (eapply IH ;eauto). - eapply update_version_addr_preserves_mem_corresponds in Hinv ; eauto. - admit. - admit. - admit. -Admitted. - + eapply update_version_addr_preserves_mem_corresponds + in Hinv + ; eauto. + { erewrite update_version_region_notin_preserves_lmem; eauto. } + { + rewrite /is_cur_addr ; cbn. + erewrite update_version_region_notin_preserves_cur; eauto. + } + { cbn. + rewrite -/(update_version_region lm la v lm). + rewrite /update_version_addr. + rewrite update_version_region_notin_preserves_lmem; eauto. + } + { + eapply update_version_region_preserves_notin_not_access; eauto. + } +Qed. (** Machinery for valid update of the lmemory *) @@ -2253,15 +2344,13 @@ Proof. destruct (decide (a' = a)) as [? | Ha'_neq_a] ; simplify_map_eq. - assert (v' ≠ (v+1)) as Hneq_v by (intro ; simplify_eq). eapply lookup_weaken ; last eapply Hcompatibility. - (* eapply update_version_addr_lookup; eauto. *) - (* erewrite update_version_region_notin_preserves_lmem; eauto. *) - (* rewrite update_version_region_notin_preserves_lmem; eauto. *) - admit. + eapply update_version_addr_lookup; eauto. + all: erewrite update_version_region_notin_preserves_lmem; eauto. - eapply update_version_addr_updated_incl in Hcompatibility; eauto. eapply IHla; eauto. split; eauto. rewrite update_version_region_notin_preserves_lmem; eauto. -Admitted. +Qed. Lemma is_valid_updated_lmemory_lmem_incl (glmem llmem llmem' : LMem) (la : list Addr) (a' : Addr) (v v' : Version) (lw : LWord) : diff --git a/theories/rules/rules_IsUnique.v b/theories/rules/rules_IsUnique.v index 6df88301..46e63d90 100644 --- a/theories/rules/rules_IsUnique.v +++ b/theories/rules/rules_IsUnique.v @@ -56,7 +56,7 @@ Section cap_lang_rules. lregs !! src = Some (LCap p b e a v) -> p ≠ E -> (* we update the region of memory with the new version *) - is_valid_updated_lmemory lmem lmem (finz.seq_between b e) v lmem' -> + (∃ lm, lmem ⊆ lm ∧ is_valid_updated_lmemory lm lmem (finz.seq_between b e) v lmem') -> (* specific instance of unique_in_registers *) unique_in_registersL lregs src (LCap p b e a v) -> incrementLPC (<[ dst := LInt 1 ]> (<[ src := next_version_lword (LCap p b e a v) ]> lregs)) = Some lregs' -> @@ -522,7 +522,6 @@ Section cap_lang_rules. destruct sb; cbn in *; done. destruct l; cbn in *; done. } - iIntros "%Heqlwsrcv %Heqgwsrcv". rewrite updatePC_incrementPC; cbn. @@ -565,6 +564,8 @@ Section cap_lang_rules. ; try done ; inversion Hget_lsrcv; subst. all: eapply IsUnique_success_true_is_sealed; eauto. + + + iDestruct (update_state_interp_transient_next_version with "Hσ") as "(%lmt & %Hlmem_incl & %Hisvalid &Hσ)"; eauto. rewrite (update_state_interp_transient_int (dst := dst) (z := 1%Z)) @@ -601,8 +602,6 @@ Section cap_lang_rules. ; inversion Hget_lsrcv; subst. eapply IsUnique_success_true_cap; eauto. { by intro ; subst. } - (* apply is_valid_updated_lmemory_update_version_region. *) - admit. - iMod (state_interp_transient_intro_nodfracs (lm := lmem) with "[$Hregs $Hσ Hmem Hpca]") as "Hσ". { iCombine "Hpca Hmem" as "Hmem". rewrite -(big_sepM_insert (fun x y => mapsto x (DfracOwn (pos_to_Qp 1)) y)). @@ -655,8 +654,7 @@ Section cap_lang_rules. ; auto ; try done ; eapply IsUnique_success_false; eauto. - (* Qed. *) - Admitted. + Qed. (* Lemma update_state_interp_transient_next_version {σ σt lr lrt} {lm lmt : LMemF} la lw lw' : *) (* (forall cur_map, is_cur_regs lrt cur_map -> is_cur_word lw cur_map) -> *) @@ -1068,6 +1066,7 @@ Section cap_lang_rules. iExtractList "Hrmap" [PC; dst; src] as ["HPC"; "Hdst"; "Hsrc"]. iClear "Hrmap". iFrame. + destruct Hupd as ( lm & Hlm_incl & Hvalid ). assert ( mem' !! (pc_a, pc_v) = Some lw ) as Hmem'_pca by (eapply is_valid_updated_lmemory_notin_preserves_lmem; eauto; by simplify_map_eq). @@ -1075,7 +1074,8 @@ Section cap_lang_rules. assert ( logical_range_map b0 e0 lws v0 ⊆ mem' ) as Hmem'_be. { - eapply is_valid_updated_lmemory_lmem_incl; eauto. + eapply is_valid_updated_lmemory_lmem_incl with (glmem := lm); eauto. + (* destruct Hvalid as (Hupd&_&?). *) (* eapply is_valid_updated_lmemory_insert; eauto. *) admit. (* eapply logical_range_notin; eauto. *) @@ -1085,17 +1085,18 @@ Section cap_lang_rules. assert (logical_range_map b0 e0 lws (v0 + 1) ⊆ mem') as Hmem'_be_next. - { clear -Hupd Hpca_notin Hlen_lws. + { clear -Hlm_incl Hvalid Hpca_notin Hlen_lws. (* TODO extract as a lemma *) 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_range_map_lookup_versions; eauto. - eapply logical_range_version_neq; eauto; lia. + (* erewrite logical_range_map_lookup_versions with (v':=v0) in Hlw'; eauto. *) + (* rewrite /logical_range_map in Hlw'. *) + admit. + (* rewrite update_version_region_preserves_lmem_next; eauto. *) + (* eapply lookup_weaken. ; last eauto. *) + (* all: rewrite lookup_insert_ne //=; last (intro ; set_solver). *) + (* eapply logical_range_version_neq; eauto; lia. *) } rewrite -(insert_id mem' (pc_a, pc_v) lw); auto. @@ -1193,16 +1194,18 @@ Section cap_lang_rules. iExtractList "Hrmap" [PC; dst; src] as ["HPC"; "Hdst"; "Hsrc"]. iClear "Hrmap". iFrame. + destruct Hupd as ( lm & Hlm_incl & Hvalid ). assert ( mem' !! (pc_a, pc_v) = Some lw ) as Hmem'_pca. { eapply is_valid_updated_lmemory_notin_preserves_lmem; eauto; by simplify_map_eq. } + destruct Hvalid as (Hupd&_&?). assert ( exists lws, length lws = length (finz.seq_between b0 e0) /\ logical_range_map b0 e0 lws (v0 + 1) ⊆ mem') as (lws & Hlen_lws & Hmem'_be_next). - { destruct Hupd as (_ & _ &Hupd) ; eapply logical_region_map_inv ; eauto. } + { eapply logical_region_map_inv ; eauto. } rewrite -(insert_id mem' (pc_a, pc_v) lw); auto. iDestruct (big_sepM_insert_delete with "Hmmap") as "[HPC Hmmap]"; iFrame.