From 5f421c9d52a104bbb4156595c1e44e645646065c Mon Sep 17 00:00:00 2001 From: June Rousseau Date: Fri, 17 Jan 2025 00:35:52 +0100 Subject: [PATCH] WIP import Griotte --- theories/ftlr/Restrict.v | 230 ++++++++++++--------------------------- 1 file changed, 69 insertions(+), 161 deletions(-) diff --git a/theories/ftlr/Restrict.v b/theories/ftlr/Restrict.v index b68cb034..92674acf 100644 --- a/theories/ftlr/Restrict.v +++ b/theories/ftlr/Restrict.v @@ -78,84 +78,41 @@ Section fundamental. | * Hdst Hz Hpair HPfl HLfl HincrPC | ] ; cycle 2. - { iApply wp_pure_step_later; auto. iNext; iIntros "_". - iApply wp_value; auto. iIntros; discriminate. } - { apply incrementPC_Some_inv in HincrPC as (p''&g''&b''&e''&a''& ? & HPC & Z & Hregs') . - - assert (a'' = a ∧ b'' = b ∧ e'' = e) as (-> & -> & ->). - { destruct (decide (PC = dst)); simplify_map_eq; auto. } - - iApply wp_pure_step_later; auto. - iNext ; iIntros "_". - iDestruct (region_close with "[$Hstate $Hr $Ha $Hmono Hw]") as "Hr"; eauto. - { destruct ρ;auto;[|ospecialize (Hnotmonostatic _)];contradiction. } - simplify_map_eq; map_simpl "Hmap". - - - iApply ("IH" $! _ (<[dst:=_]> _) with "[%] [] [Hmap] [$Hr] [$Hsts] [$Hown]"); eauto. - { cbn. intros. by repeat (rewrite lookup_insert_is_Some'; right). } - { iIntros (ri v Hri Hvs). - destruct (decide (ri = dst)). - { subst ri. - rewrite lookup_insert_ne in Hdst; auto. - rewrite lookup_insert in Hvs; inversion Hvs; simplify_eq. - unshelve iSpecialize ("Hreg" $! dst _ _ Hdst); eauto. - iApply (interp_weakening with "IH Hreg"); auto; solve_addr. } - { repeat (rewrite lookup_insert_ne in Hvs); auto. - iApply "Hreg"; auto. } } - { destruct (reg_eq_dec PC dst) as [Heq | Hne]; simplify_map_eq. - destruct p'',g''; destruct g0; simpl in *; try congruence. - simplify_map_eq. - (* TODO follow the proof from MCerise, - because restricting with dst=PC can lead to the wrong permissions. - *) - all: destruct Hp as [Hp | [ Hp | [Hp Hl] ] ]; subst ; simpl in * ; try congruence. - destruct Hpg as [Hp' | [ Hp' | [Hp' Hg' ] ] ]; subst; simpl in *; simpl; try congruence; auto. } - - auto. by rewrite PermFlowsToReflexive. } - - { - naive_solver. } - { rewrite insert_insert. iApply "Hmap". } - iModIntro. - iApply (interp_weakening with "IH Hinv"); auto; try solve_addr. - { destruct Hp; by subst p. } - { destruct (reg_eq_dec PC dst) as [Heq | Hne]; simplify_map_eq. - auto. by rewrite PermFlowsToReflexive. } - } - - { - match goal with - | H: incrementPC _ = Some _ |- _ => apply incrementPC_Some_inv in H as (p''&g''&b''&e''&a''& ? & HPC & Z & Hregs' & XX) - end. simplify_map_eq. - iApply wp_pure_step_later; auto. iNext. + - iApply wp_pure_step_later; auto. iNext; iIntros "_". + iApply wp_value; auto. iIntros; discriminate. + - apply incrementPC_Some_inv in HincrPC as (p''&g''&b''&e''&a''& ? & HPC & Z & Hregs') . + iApply wp_pure_step_later; auto. iNext; iIntros "_". assert (HPCr0: match r0 with inl _ => True | inr r0 => PC <> r0 end). { destruct r0; auto. - intro; subst r0. simplify_map_eq. } + intro; subst r. simplify_map_eq. } destruct (reg_eq_dec PC dst). { subst dst. repeat rewrite insert_insert. repeat rewrite insert_insert in HPC. rewrite lookup_insert in HPC. inv HPC. - rewrite lookup_insert in H0. inv H0. - rewrite H5 in H3. iDestruct (region_close with "[$Hstate $Hr $Ha $Hmono Hw]") as "Hr"; eauto. - { destruct ρ;auto;[|specialize (Hnotmonostatic g)|specialize (Hnotuninitialized w0)];contradiction. } + (* rewrite lookup_insert in H0. inv H0. *) + (* rewrite H5 in H3. *) + iDestruct (region_close with "[$Hstate $Hr $Ha $Hmono Hw]") as "Hr"; eauto. + { destruct ρ;auto;[|ospecialize (Hnotmonostatic _)];contradiction. } destruct (PermFlowsTo RX p'') eqn:Hpft. - { assert (Hpg: p'' = RX ∨ p'' = RWX ∨ p'' = RWLX ∧ g'' = Directed). + { assert (Hpg: p'' = RX ∨ p'' = RWX ∨ p'' = RWLX ∧ g'' = Local). { destruct p''; simpl in Hpft; eauto; try discriminate. - destruct (andb_true_eq _ _ ltac:(naive_solver)). - simpl in H3, H4. destruct p0; simpl in H3; try discriminate. + destruct p0; simpl in *; try discriminate. + simplify_map_eq. + right;right; split;auto. destruct Hp as [Hp | [Hp | [Hp Hg] ] ]; try discriminate. - subst g0; destruct g''; simpl in H4; auto; discriminate. } - rewrite H5. iApply ("IH" $! _ r with "[%] [] [Hmap] [$Hr] [$Hsts] [$Hown]"); try iClear "IH"; eauto. - iModIntro. iApply (big_sepL_mono with "Hinv"); simpl; intros. + destruct g0 ;destruct g''; simpl in *; auto; try discriminate. } + simplify_map_eq ; map_simpl "Hmap". + iApply ("IH" $! _ regs with "[%] [] [Hmap] [$Hr] [$Hsts] [$Hown]"); try iClear "IH"; eauto. + iModIntro. + iApply (big_sepL_mono with "Hinv"); simpl; intros. iIntros "H". simpl. iDestruct "H" as "[H1 H2]". iSplitL "H1". { destruct (writeAllowed p'') eqn:Hwa. - assert (writeAllowed p0 = true) as ->;auto. - destruct p0;auto;destruct p'';inversion Hwa;inversion H3. + destruct p0;auto;destruct p'';inversion Hwa;inversion HPfl. - destruct (writeAllowed p0). + iExists interp. iFrame. iSplit;[iPureIntro;apply _|]. iSplit;[auto|]. iNext. iModIntro. iIntros (W1 W2 z) "_". @@ -164,112 +121,63 @@ Section fundamental. iExists _;iFrame. } iDestruct "H2" as %?. iPureIntro. - destruct (andb_true_eq _ _ ltac:(naive_solver)); simpl in *. - destruct (locality_eq_dec g'' g0). - * subst g0. destruct Hp as [Hp | [ Hp | [Hp Hl] ] ]; destruct Hpg as [Hp' | [ Hp' | [Hp' Hg' ] ] ]; subst; simpl in *; simpl; try congruence; auto. - * destruct g''; destruct g0; simpl in *; try congruence. - all: destruct Hp as [Hp | [ Hp | [Hp Hl] ] ]; destruct Hpg as [Hp' | [ Hp' | [Hp' Hg' ] ] ]; subst; simpl in *; simpl; try congruence; auto. } + destruct Hp as [Hp | [ Hp | [Hp Hl] ] ] + ; destruct Hpg as [Hp' | [ Hp' | [Hp' Hg' ] ] ] + ; subst; simpl in *; simpl; try congruence; auto + ; inv HPfl ; inv HLfl + ; destruct g'' ; try destruct g0 ; cbn in * ; try done. + cbn in *. + admit. (* TODO fix the model *) + admit. (* TODO fix the model *) + } + { iApply (wp_bind (fill [SeqCtx])). iDestruct ((big_sepM_delete _ _ PC) with "Hmap") as "[HPC Hmap]"; [apply lookup_insert|]. - rewrite H5. iApply (wp_notCorrectPC with "HPC"); [eapply not_isCorrectPC_perm; destruct p''; simpl in Hpft; eauto; discriminate|]. iNext. iIntros "HPC /=". - iApply wp_pure_step_later; auto. - iApply wp_value. - iNext. iIntros. discriminate. } } - - simplify_map_eq. - iDestruct (region_close with "[$Hstate $Hr $Ha $Hmono Hw]") as "Hr"; eauto. - { destruct ρ;auto;[|specialize (Hnotmonostatic g)|specialize (Hnotuninitialized w0)];contradiction. } - iApply ("IH" $! _ (<[dst:=_]> _) with "[%] [] [Hmap] [$Hr] [$Hsts] [$Hown]"); eauto. - - intros; simpl. repeat (rewrite lookup_insert_is_Some'; right); eauto. - - iIntros (ri Hri). rewrite /RegLocate. - destruct (decide (ri = dst)). - + subst ri. rewrite lookup_insert. - destruct (decodePermPair n) as (p1 & g1). - iDestruct ("Hreg" $! dst Hri) as "Hdst". - rewrite H0. iApply PermPairFlows_interp_preserved; eauto. - + repeat rewrite lookup_insert_ne; auto. - iApply "Hreg"; auto. } - Qed. - - - Lemma restrict_case (r : leibnizO Reg) (p : Perm) - (b e a : Addr) (w : Word) (dst : RegName) (r0 : Z + RegName) (P:D): - ftlr_instr r p b e a w (Restrict dst r0) P. - Proof. - intros Hp Hsome i Hbae Hi. - iIntros "#IH #Hinv #Hinva #Hreg #[Hread Hwrite] Hown Ha HP Hcls HPC Hmap". - rewrite delete_insert_delete. - iDestruct ((big_sepM_delete _ _ PC) with "[HPC Hmap]") as "Hmap /="; - [apply lookup_insert|rewrite delete_insert_delete;iFrame|]. simpl. - iApply (wp_Restrict with "[$Ha $Hmap]"); eauto. - { simplify_map_eq; auto. } - { rewrite /subseteq /map_subseteq /set_subseteq_instance. intros rr _. - apply elem_of_dom. apply lookup_insert_is_Some'; eauto. } - - iIntros "!>" (regs' retv). iDestruct 1 as (HSpec) "[Ha Hmap]". - destruct HSpec as [ * Hdst ? Hz Hfl HincrPC | * Hdst Hz Hfl HincrPC | ]. - { apply incrementPC_Some_inv in HincrPC as (p''&b''&e''&a''& ? & HPC & Z & Hregs') . - - assert (a'' = a ∧ b'' = b ∧ e'' = e) as (-> & -> & ->). - { destruct (decide (PC = dst)); simplify_map_eq; auto. } - - iApply wp_pure_step_later; auto. - iMod ("Hcls" with "[HP Ha]");[iExists w;iFrame|iModIntro]. - iNext; iIntros "_". - iApply ("IH" $! regs' with "[%] [] [Hmap] [$Hown]"). - { cbn. intros. subst regs'. by repeat (apply lookup_insert_is_Some'; right). } - { iIntros (ri v Hri Hvs). - destruct (decide (ri = dst)). - { subst ri. - rewrite lookup_insert_ne in Hdst; auto. - rewrite lookup_insert in Hvs; inversion Hvs. simplify_eq. - unshelve iSpecialize ("Hreg" $! dst _ _ Hdst); eauto. - iApply (interp_weakening with "IH Hreg"); auto; solve_addr. } - { repeat (rewrite lookup_insert_ne in Hvs); auto. - iApply "Hreg"; auto. } } - { subst regs'. rewrite insert_insert. iApply "Hmap". } - iModIntro. - iApply (interp_weakening with "IH Hinv"); auto; try solve_addr. - { destruct Hp; by subst p. } - { destruct (reg_eq_dec PC dst) as [Heq | Hne]; simplify_map_eq. - auto. by rewrite PermFlowsToReflexive. } - } - { apply incrementPC_Some_inv in HincrPC as (p''&b''&e''&a''& ? & HPC & Z & Hregs') . - - assert (dst ≠ PC) as Hne. - { destruct (decide (PC = dst)); last auto. simplify_map_eq; auto. } + iApply wp_pure_step_later; auto. iNext ; iIntros "_". + iApply wp_value. iIntros ; discriminate. } + } + { + simplify_map_eq. + iDestruct (region_close with "[$Hstate $Hr $Ha $Hmono Hw]") as "Hr"; eauto. + { destruct ρ;auto;[|specialize (Hnotmonostatic g)];contradiction. } + iApply ("IH" $! _ (<[dst:=_]> _) with "[%] [] [Hmap] [$Hr] [$Hsts] [$Hown]"); eauto. + - intros; simpl. repeat (rewrite lookup_insert_is_Some'; right); eauto. + - iIntros (ri v Hri Hvs). + destruct (decide (ri = dst)). + + subst ri. simplify_map_eq. + destruct (decodePermPair n) as (p1 & g1); simplify_eq. + iDestruct ("Hreg" $! dst _ Hri Hdst) as "Hdst". + iApply PermPairFlows_interp_preserved; eauto. + + simplify_map_eq. iApply "Hreg"; auto. + } + - apply incrementPC_Some_inv in HincrPC as (p''&g''&b''&e''&a''& ? & HPC & Z & Hregs') . + iApply wp_pure_step_later; auto. iNext; iIntros "_". - assert (p'' = p ∧ b'' = b ∧ e'' = e ∧ a'' = a) as (-> & -> & -> & ->). - { simplify_map_eq; auto. } + assert (HPCr0: match r0 with inl _ => True | inr r0 => PC <> r0 end). + { destruct r0; auto. + intro; subst r. simplify_map_eq. } - iApply wp_pure_step_later; auto. - iMod ("Hcls" with "[HP Ha]");[iExists w;iFrame|iModIntro]. - iNext; iIntros "_". - iApply ("IH" $! regs' with "[%] [] [Hmap] [$Hown]"). - { cbn. intros. subst regs'. by repeat (apply lookup_insert_is_Some'; right). } + destruct (reg_eq_dec PC dst). + { subst dst. repeat rewrite insert_insert. + repeat rewrite insert_insert in HPC. + rewrite lookup_insert in HPC. inv HPC. + } + iDestruct (region_close with "[$Hstate $Hr $Ha $Hmono Hw]") as "Hr"; eauto. + { destruct ρ;auto;[|ospecialize (Hnotmonostatic _)];contradiction. } + simplify_map_eq; map_simpl "Hmap". + iApply ("IH" $! _ (<[dst:=WSealRange p' g' b0 e0 a0]> regs) with + "[%] [] [Hmap] [$Hr] [$Hsts] [$Hown]"); eauto. + { intros. by rewrite lookup_insert_is_Some' ; right. } { iIntros (ri v Hri Hvs). - subst regs'. - rewrite lookup_insert_ne in Hvs; auto. destruct (decide (ri = dst)). - { subst ri. - rewrite lookup_insert_ne in Hdst; auto. - rewrite lookup_insert in Hvs; inversion Hvs. simplify_eq. - unshelve iSpecialize ("Hreg" $! dst _ _ Hdst); eauto. - iApply (interp_weakening_ot with "Hreg"); auto; solve_addr. } - { repeat (rewrite lookup_insert_ne in Hvs); auto. - iApply "Hreg"; auto. } } - { subst regs'. rewrite insert_insert. iApply "Hmap". } - iModIntro. - iApply (interp_weakening with "IH Hinv"); auto; try solve_addr. - { destruct Hp; by subst p. } - { by rewrite PermFlowsToReflexive. } - } - { iApply wp_pure_step_later; auto. - iMod ("Hcls" with "[HP Ha]");[iExists w;iFrame|iModIntro]. - iNext; iIntros "_". - iApply wp_value; auto. iIntros; discriminate. } - Qed. + + subst ri. simplify_map_eq. + destruct (decodeSealPermPair n) as (p1 & g1); simplify_eq. + iDestruct ("Hreg" $! dst _ Hri Hdst) as "Hdst". + iApply SealPermPairFlows_interp_preserved; eauto. + + simplify_map_eq. iApply "Hreg"; auto. + } + Admitted. End fundamental.