From d5994db57ec24263e72951aaa4e845590eb3beb9 Mon Sep 17 00:00:00 2001 From: Bastien Rousseau Date: Mon, 22 Jul 2024 13:31:00 +0200 Subject: [PATCH] WIP test replace E-perm by sealed entry --- theories/examples/malloc.v | 18 ++++-- theories/ftlr/Jmp.v | 3 +- theories/ftlr/Jnz.v | 3 +- theories/ftlr/UnSeal.v | 16 +++--- theories/ftlr/interp_weakening.v | 45 ++++++++++----- theories/fundamental.v | 2 +- theories/logrel.v | 97 ++++++++++++++++++++------------ 7 files changed, 117 insertions(+), 67 deletions(-) diff --git a/theories/examples/malloc.v b/theories/examples/malloc.v index a21d3021..4e9472c1 100644 --- a/theories/examples/malloc.v +++ b/theories/examples/malloc.v @@ -207,11 +207,21 @@ Section SimpleMalloc. Qed. Lemma simple_malloc_subroutine_valid N b e : - na_inv logrel_nais N (malloc_inv b e) -∗ - interp (WCap E b e b). + na_inv logrel_nais N (malloc_inv b e) + ∗ seal_pred otype_sentry interp -∗ + interp (WSealed otype_sentry (SCap RX b e b)). Proof. - iIntros "#Hmalloc". - rewrite fixpoint_interp1_eq /=. iIntros (r). iNext. iModIntro. + iIntros "[#Hmalloc #Hsentry]". + rewrite fixpoint_interp1_eq /=. + iExists (interp); rewrite fixpoint_interp1_eq /=. + iSplit. + { iPureIntro; intro; apply interp_persistent. } + iSplit; first done. + (* TODO not working here: + it means that I have to prove that the content of malloc is safe to share, + which is not *) + iSplit; first done. + iIntros (r). iNext. iModIntro. iIntros "(#[% Hregs_valid] & Hregs & Hown)". iDestruct (big_sepM_delete _ _ PC with "Hregs") as "[HPC Hregs]";[rewrite lookup_insert;eauto|]. destruct H with r_t0 as [? ?]. diff --git a/theories/ftlr/Jmp.v b/theories/ftlr/Jmp.v index e3d686e2..92e38fb0 100644 --- a/theories/ftlr/Jmp.v +++ b/theories/ftlr/Jmp.v @@ -95,7 +95,8 @@ Section fundamental. iClear "Hinv". rewrite fixpoint_interp1_eq; simpl. iDestruct (big_sepM_insert _ _ PC with "[$Hmap $HPC]") as "Hmap"; [apply lookup_delete|]. rewrite insert_delete_insert; auto. - iDestruct ("HPCv" with "[$Hmap $Hown]") as "Hcont"; auto. + iDestruct "HPCv" as (Psentry) "(%Hpers & #Hseal_pred & HPsentry & Hcont)"; auto. + iDestruct ("Hcont" $! r with "[$Hmap $Hown]") as "Hcont'"; auto. + (* Not a sentry *) rewrite (_: match sb with | SCap _ _ _ _ | _ => WSealed ot sb end = WSealed ot sb) ; last (by destruct sb). diff --git a/theories/ftlr/Jnz.v b/theories/ftlr/Jnz.v index ae789efe..254fa7b0 100644 --- a/theories/ftlr/Jnz.v +++ b/theories/ftlr/Jnz.v @@ -92,7 +92,8 @@ Section fundamental. } iEval (rewrite fixpoint_interp1_eq) in "HPCv"; simpl. - iDestruct ("HPCv" with "[$Hmap $Hown]") as "Hcont"; auto. + iDestruct "HPCv" as (Psentry) "(%Hpers & #Hseal_pred & HPsentry & Hcont)"; auto. + iDestruct ("Hcont" $! r with "[$Hmap $Hown]") as "Hcont'"; auto. + (* Not a sentry *) rewrite (_: match sb with | SCap _ _ _ _ | _ => WSealed ot sb end = WSealed ot sb) ; last (by destruct sb). diff --git a/theories/ftlr/UnSeal.v b/theories/ftlr/UnSeal.v index 49e54fb0..2d517e88 100644 --- a/theories/ftlr/UnSeal.v +++ b/theories/ftlr/UnSeal.v @@ -25,18 +25,16 @@ Section fundamental. Proof. iIntros (Hpseal Hwb) "#HVsd #HVsr". rewrite (fixpoint_interp1_eq (WSealRange _ _ _ _)) (fixpoint_interp1_eq (WSealed _ _)) /= Hpseal /interp_sb. - iDestruct "HVsr" as "[_ Hss]". + iDestruct "HVsr" as "[_ [Hss Hjmp]]". apply seq_between_dist_Some in Hwb. iDestruct (big_sepL_delete with "Hss") as "[HSa0 _]"; eauto. iDestruct "HSa0" as (P) "[HsealP HWcond]". - destruct (decide (a0 = otype_sentry)) as [?|Hot] ; subst. - + admit. - + - iDestruct "HVsd" as (P') "[% [HsealP' HP']]". - iDestruct (seal_pred_agree with "HsealP HsealP'") as "Hequiv". iSpecialize ("Hequiv" $! (WSealable sb)). - iAssert (▷ P (WSealable sb))%I as "HP". { iNext. by iRewrite "Hequiv". } - by iApply "HWcond". - Admitted. + (* destruct (decide (a0 = otype_sentry)) as [?|Hot] ; subst. *) + iDestruct "HVsd" as (P') "[% [HsealP' [HP' Hjmp']]]". + iDestruct (seal_pred_agree with "HsealP HsealP'") as "Hequiv". iSpecialize ("Hequiv" $! (WSealable sb)). + iAssert (▷ P (WSealable sb))%I as "HP". { iNext. by iRewrite "Hequiv". } + by iApply "HWcond". + Qed. Lemma unseal_case (r : leibnizO Reg) (p : Perm) (b e a : Addr) (w : Word) (dst r1 r2 : RegName) (P:D): diff --git a/theories/ftlr/interp_weakening.v b/theories/ftlr/interp_weakening.v index 0deedef4..e21fb248 100644 --- a/theories/ftlr/interp_weakening.v +++ b/theories/ftlr/interp_weakening.v @@ -3,7 +3,7 @@ From iris.proofmode Require Import proofmode. From iris.program_logic Require Import weakestpre adequacy lifting. From stdpp Require Import base. From cap_machine.ftlr Require Import ftlr_base. -From cap_machine Require Import addr_reg region. +From cap_machine Require Import addr_reg region proofmode register_tactics. Section fundamental. Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealsg: sealStoreG Σ} @@ -89,26 +89,42 @@ Section fundamental. iNext. iModIntro. iIntros "([Hfull Hreg] & Hregs & Hna)". destruct sb as [p b e a |]; cycle 1. + (* PC contains sealrange, it is trivially safe *) - (* rewrite /interp_conf. *) - admit. + wp_instr. + iEval (rewrite /registers_mapsto) in "Hregs". + iExtract "Hregs" PC as "HPC". + iApply (wp_notCorrectPC with "HPC"); eauto; first (intro Hcontra; inversion Hcontra). + iNext ; iIntros "HPC". + wp_pure; wp_end. + iIntros "%" ; done. + iApply ("IH" with "Hfull Hreg Hregs Hna"); auto. - Admitted. + Qed. Lemma sealing_preserves_interp_sentry sb: IH -∗ + seal_pred otype_sentry (fixpoint interp1) -∗ fixpoint interp1 (WSealable sb) -∗ fixpoint interp1 (WSealed otype_sentry sb). Proof. - iIntros "#IH #HVsb". + iIntros "#IH #Hsentry_pred #HVsb". rewrite (fixpoint_interp1_eq (WSealed _ _)) /= /interp_sb. + iExists (fixpoint interp1). + iSplit. + { iPureIntro; intro; apply interp_persistent. } + iSplit; first done. + iSplit; first done. iIntros (r). iNext. iModIntro. iIntros "([Hfull Hreg] & Hregs & Hna)". destruct sb as [p b e a |]; cycle 1. - - (* PC contains sealrange, it is trivially safe *) - (* rewrite /interp_conf. *) - admit. - - iApply ("IH" with "Hfull Hreg Hregs Hna"); auto. - Admitted. + + (* PC contains sealrange, it is trivially safe *) + wp_instr. + iEval (rewrite /registers_mapsto) in "Hregs". + iExtract "Hregs" PC as "HPC". + iApply (wp_notCorrectPC with "HPC"); eauto; first (intro Hcontra; inversion Hcontra). + iNext ; iIntros "HPC". + wp_pure; wp_end. + iIntros "%" ; done. + + iApply ("IH" with "Hfull Hreg Hregs Hna"); auto. + Qed. Lemma safe_to_unseal_weakening b e b' e': @@ -160,10 +176,11 @@ Section fundamental. intros Hb He Hp. iIntros "#HA". rewrite !fixpoint_interp1_eq. cbn. destruct (permit_seal p') eqn:Hseal; [eapply (permit_seal_flowsto _ p) in Hseal as ->; auto | ]. - all: destruct (permit_unseal p') eqn:Hunseal; [eapply (permit_unseal_flowsto _ p) in Hunseal as ->; auto | ]; iDestruct "HA" as "[Hs Hus]". - all: iSplitL "Hs"; - [try iApply (safe_to_seal_weakening with "Hs") | try iApply (safe_to_unseal_weakening with "Hus")]; auto. + all: destruct (permit_unseal p') eqn:Hunseal; [eapply (permit_unseal_flowsto _ p) in Hunseal as + ->; auto | ]; iDestruct "HA" as "[Hs [Hus Hj]]". + all: destruct (permit_call b' e') as [Hjump|Hjump]. + all: iSplitL "Hs"; [try iApply (safe_to_seal_weakening with "Hs") | iSplitL "Hus" ; try iApply (safe_to_unseal_weakening with "Hus")]; auto. + all: destruct (permit_call b e) as [Hjump'|Hjump']; solve_addr. Qed. - End fundamental. diff --git a/theories/fundamental.v b/theories/fundamental.v index 8fcc8fb9..8a413a9e 100644 --- a/theories/fundamental.v +++ b/theories/fundamental.v @@ -212,7 +212,7 @@ Section fundamental. } { destruct Hw as [p [b [e [a ->] ] ] ]. rewrite fixpoint_interp1_eq. cbn -[all_registers_s]. iNext. iIntros (rmap). - iDestruct "Hw" as "[Hw HwP]". + iDestruct "Hw" as (P) "(%HP & HPsentry & HwP & Hw)". iSpecialize ("Hw" $! rmap). iDestruct "Hw" as "#Hw". iIntros "(HPC & Hr & ?)". iApply "Hw". iFrame. } { iNext. iIntros (rmap). iApply fundamental. eauto. } diff --git a/theories/logrel.v b/theories/logrel.v index 4c54828d..73810431 100644 --- a/theories/logrel.v +++ b/theories/logrel.v @@ -81,6 +81,13 @@ Section logrel. Proper (dist n ==> dist n) enter_cond. Proof. solve_proper. Qed. + Program Definition jump_cond (P : D) : D -n> iPropO Σ := + λne interp, (▷ □ ∀ (w : Word), P w -∗ enter_cond w interp)%I. + Solve Obligations with solve_proper. + Global Instance jump_cond_ne n : + Proper (dist n ==> dist n ==> dist n) jump_cond. + Proof. solve_proper. Qed. + (* interp definitions *) Program Definition interp_ref_inv (a : Addr) : D -n> iPropO Σ := λne P, (∃ w, a ↦ₐ w ∗ P w)%I. Solve Obligations with solve_proper. @@ -127,24 +134,20 @@ Section logrel. ([∗ list] a ∈ (finz.seq_between b e), ∃ P : D, ⌜∀ w, Persistent (P w)⌝ ∗ seal_pred a P ∗ write_cond P interp)%I. Definition safe_to_unseal (interp : D) (b e : OType) : iPropO Σ := ([∗ list] a ∈ (finz.seq_between b e), ∃ P : D, seal_pred a P ∗ read_cond P interp)%I. + Definition safe_to_jump (interp : D) : iPropO Σ := + (∃ P : D, seal_pred otype_sentry P ∗ jump_cond P interp)%I. + + Definition permit_call (b e : OType) := decide (b <= otype_sentry < e)%ot. Program Definition interp_sr (interp : D) : D := λne w, (match w with | WSealRange p b e a => (if permit_seal p then safe_to_seal interp b e else True) ∗ (if permit_unseal p then safe_to_unseal interp b e else True) + ∗ (if permit_call b e then safe_to_jump interp else True) | _ => False end ) %I. Solve All Obligations with solve_proper. - (* Program Definition interp_sentry (interp : D) : D := - λne w, - (match w with - | WSealed otype_sentry sb => enter_cond (WSealable sb) interp - | _ => True - end)%I. - Solve All Obligations with solve_proper. *) - - Program Definition interp_sb (o : OType) (interp : D) : D := λne w, (∃ P : Word → iPropI Σ, @@ -157,6 +160,20 @@ Section logrel. )%I. Solve All Obligations with solve_proper. + (* TODO possible alternative: + if sealed with otype_sentry, we only require safe-to-execute, not interp *) + (* Program Definition interp_sb (o : OType) (interp : D) : D := *) + (* λne w, *) + (* (∃ P : Word → iPropI Σ, *) + (* ⌜∀ w', Persistent (P w')⌝ *) + (* ∗ seal_pred o P *) + (* ∗ ▷ P w *) + (* ∗ (if (decide (o = otype_sentry)) *) + (* then enter_cond w interp *) + (* else True) *) + (* )%I. *) + (* Solve All Obligations with solve_proper. *) + Program Definition interp1 (interp : D) : D := (λne w, match w return _ with @@ -168,9 +185,6 @@ Section logrel. | WCap RWX b e a => interp_cap_RWX interp w | WSealRange p b e a => interp_sr interp w | WSealed o sb => interp_sb o interp (WSealable sb) - (* (if (decide (o = otype_sentry)) *) - (* then interp_sentry interp w *) - (* else ) *) end)%I. Global Instance read_cond_contractive : @@ -198,6 +212,11 @@ Section logrel. Proof. solve_contractive. Qed. + Global Instance jump_cond_contractive : + Contractive (jump_cond). + Proof. + solve_contractive. + Qed. Global Instance interp_cap_RX_contractive : Contractive (interp_cap_RX). Proof. @@ -217,17 +236,10 @@ Section logrel. Proof. solve_proper_prepare. destruct_word x0; auto. - destruct (permit_seal sr), (permit_unseal sr); - rewrite /safe_to_seal /safe_to_unseal; - solve_contractive. - Qed. - (* Global Instance interp_sentry_contractive : *) - (* Contractive (interp_sentry). *) - (* Proof. *) - (* solve_proper_prepare. *) - (* destruct_word x0; auto. *) - (* solve_contractive. *) - (* Qed. *) + destruct (permit_seal sr), (permit_unseal sr), (permit_call f f0); + rewrite /safe_to_seal /safe_to_unseal /safe_to_jump. + (* solve_contractive. *) + Admitted. Global Instance interp1_contractive : Contractive (interp1). @@ -256,9 +268,9 @@ Section logrel. Proof. intros. destruct_word w; simpl; rewrite fixpoint_interp1_eq; simpl. - apply _. - destruct c; repeat (apply exist_persistent; intros); try apply _. - - destruct (permit_seal sr), (permit_unseal sr); rewrite /safe_to_seal /safe_to_unseal; apply _ . - - - apply exist_persistent; intros P. + - destruct (permit_seal sr), (permit_unseal sr), (permit_call f f0) + ; rewrite /safe_to_seal /safe_to_unseal /safe_to_jump; apply _ . + - apply exist_persistent; intros P. unfold Persistent. iIntros "(Hpers & #Hs & [HP Hjmp])". iDestruct "Hpers" as %Hpers. iAssert ( ▷ P (WSealable s))%I with "[ HP ]" as "HP". { iApply later_persistently_1. by iApply Hpers. } @@ -618,39 +630,50 @@ Section logrel. Qed. Lemma region_seal_pred_interp E (b e a: OType) b1 b2 : + not (b <= otype_sentry < e)%ot -> ([∗ list] o ∈ finz.seq_between b e, seal_pred o interp) ={E}=∗ interp (WSealRange (b1,b2) b e a). Proof. + intros Hnsentry. remember (finz.seq_between b e) as l eqn:Hgen. rewrite Hgen; revert Hgen. - generalize b e. clear b e. + generalize dependent Hnsentry. + generalize b e. + clear b e. induction l as [|hd tl IH]. - - iIntros (b e Hfinz) "_ !>". + - iIntros (b e Hnsentry Hfinz) "_ !>". rewrite /interp fixpoint_interp1_eq /= /safe_to_seal /safe_to_unseal. - rewrite -Hfinz. destruct b1, b2; iSplit; done. - - iIntros (b e Hfinz). + rewrite -Hfinz. + destruct b1, b2; iSplit; try done. + all: symmetry in Hfinz; apply finz_empty_seq_between in Hfinz. + all: destruct (permit_call b e); iSplit; try done; solve_addr. + - iIntros (b e Hnsentry Hfinz). assert (b < e)%ot as Hlbe. {destruct (decide (b < e)%ot) as [|HF]; first auto. rewrite finz_seq_between_empty in Hfinz; [inversion Hfinz | solve_addr ]. } apply finz_cons_tl in Hfinz as (b' & Hplus & Hfinz). - specialize (IH b' e Hfinz). rewrite (finz_seq_between_split _ b' _). + assert (¬ (b' <= otype_sentry < e)%f) as Hnsentry' by solve_addr. + specialize (IH b' e Hnsentry' Hfinz). rewrite (finz_seq_between_split _ b' _). 2 : split; solve_addr. iIntros "[#Hfirst Hca]". iMod (IH with "Hca") as "Hca". iModIntro. rewrite /interp !fixpoint_interp1_eq /= /safe_to_seal /safe_to_unseal. rewrite !(finz_seq_between_split b b' e). 2: { split ; solve_addr. } - iDestruct "Hca" as "[Hseal Hunseal]". - iSplitL "Hseal"; [destruct b1| destruct b2]; iFrame. + iDestruct "Hca" as "(Hseal & Hunseal & Hcall)". + iSplitL "Hseal" + ; [|iSplitL "Hunseal"] + ; [destruct b1| destruct b2 | destruct (permit_call b e)]; iFrame; try done. all: iApply (big_sepL_mono with "Hfirst"). - all: iIntros (k a' Hk) "H"; cbn. - all: iExists _; iFrame; auto. - iSplit; auto. iPureIntro; apply _. + all: (iIntros (k a' Hk) "H"; cbn). + all: (iExists _; iFrame; auto). + iSplit; auto; iPureIntro; apply _. Qed. (* Get the validity of sealing capabilities if we can allocate an arbitrary predicate, and can hence choose interp itself as the sealing predicate *) Lemma region_can_alloc_interp E (b e a: OType) b1 b2: + not (b <= otype_sentry < e)%ot -> ([∗ list] o ∈ finz.seq_between b e, can_alloc_pred o) ={E}=∗ interp (WSealRange (b1,b2) b e a). Proof. - iIntros "Hca". + iIntros (Hnsentry) "Hca". iDestruct (big_sepL_mono with "Hca") as "Hca". iIntros (k a' Hk) "H". iDestruct (seal_store_update_alloc _ interp with "H") as "H". iExact "H".