Skip to content

Commit

Permalink
WIP import Griotte
Browse files Browse the repository at this point in the history
  • Loading branch information
@JuneRousseau
JuneRousseau committed Jan 16, 2025
1 parent 684df4a commit 5f421c9
Showing 1 changed file with 69 additions and 161 deletions.
230 changes: 69 additions & 161 deletions theories/ftlr/Restrict.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) "_".
Expand All @@ -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.

0 comments on commit 5f421c9

Please sign in to comment.