Commit 3d60cf9e by Dan Frumin

### `heapify` trasformtion preserves logical refinements

parent 084fb1ac
 ... ... @@ -46,7 +46,6 @@ Hint Resolve bit_nat_type : typeable. Section bit_refinement. Context `{logrelG Σ}. Context `{HagΣ: inG Σ (agreeR natC)}. Variable (Δ : list (prodC valC valC -n> iProp Σ)). Definition bitf (b : bool) : nat := ... ... @@ -55,6 +54,7 @@ Section bit_refinement. | false => 1 end. (* This is the graph of the `bitf` function *) Program Definition bitτi : prodC valC valC -n> iProp Σ := λne vv, (∃ b, ⌜vv.1 = #♭v b⌝ ∗ ⌜vv.2 = #nv (bitf b)⌝)%I. Next Obligation. solve_proper. Qed. ... ... @@ -99,3 +99,125 @@ Proof. eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ]. apply bit_prerefinement. Qed. Definition heapify : val := λ: "b", Unpack "b" \$ λ: "b'", let: "init" := Snd "b'" in let: "flip" := Snd (Fst "b'") in let: "view" := Fst (Fst "b'") in let: "x" := ref "init" in let: "flip_ref" := λ: <>, "x" <- "flip" (!"x") in let: "view_ref" := λ: <>, "view" (!"x") in Pack ("view_ref", "flip_ref", ()). Lemma heapify_type Γ : typed Γ heapify (TArrow bitτ bitτ). Proof. unfold bitτ. unfold heapify. unlock. repeat (econstructor; solve_typed). (* TODO: solve_typed does not work by itself :( *) Qed. Hint Resolve heapify_type : typeable. Section heapify_refinement. Context `{logrelG Σ}. Variable (Δ : list (prodC valC valC -n> iProp Σ)). Lemma heapify_prerefinement Γ E1 (b1 b2 : val) : nclose logrelN ⊆ E1 → □ (interp E1 E1 bitτ Δ (PackV b1, PackV b2)) -∗ {E1,E1;Δ;Γ} ⊨ heapify (Pack b1) ≤log≤ heapify (Pack b2) : bitτ. Proof. simpl. iIntros (?) "#Hlog". iDestruct "Hlog" as ([? ?]) "[% #Hlog]"; simplify_eq. iDestruct "Hlog" as (τi) "[% Hlog]". iDestruct "Hlog" as ([? ?] [init1 init2]) "[% [#Hlog #Hτi]]"; simplify_eq. iDestruct "Hlog" as ([view1 view2] [flip1 flip2]) "[% [#Hview #Hflip]]"; simplify_eq/=. unfold heapify. unlock. rel_rec_l. rel_rec_r. rel_pure_l (Unpack (Pack _) _). rel_pure_r (Unpack (Pack _) _). rel_rec_l. rel_rec_r. repeat rel_pure_l _. repeat rel_pure_r _. rel_alloc_l as x1 "Hx1". rel_alloc_r as x2 "Hx2". repeat rel_pure_l _. repeat rel_pure_r _. iApply (bin_log_related_pack _ (interp_unit [])). iMod (inv_alloc (logN .@ (x1,x2)) _ (interp_ref_inv (x1,x2) τi) with "[-]") as "#Hinv". { iNext. unfold interp_ref_inv. simpl. iExists (init1,init2). simpl. by iFrame. } repeat iApply bin_log_related_pair. - iApply bin_log_related_arrow; try by unlock. iAlways. iIntros ([v1 v2]) "/= #Hi". iDestruct "Hi" as "[% %]"; simplify_eq. rel_rec_l. rel_rec_r. rel_load_l_atomic. iInv (logN .@ (x1,x2)) as ([v1 v2]) "(Hx1 & Hx2 & #Hvv) /=" "Hcl". iExists v1; iFrame. iModIntro. iNext. iIntros "Hx1". rel_load_r. iMod ("Hcl" with "[-]"). { iNext. iExists (_,_). by iFrame. } iSpecialize ("Hview" with "Hvv"). simpl. rewrite bin_log_related_eq /bin_log_related_def. iIntros (vvs ρ) "Hspec HΓ /=". unfold env_subst. rewrite !Closed_subst_p_id. iApply "Hview". - iApply bin_log_related_arrow; try by unlock. iAlways. iIntros ([v1 v2]) "/= #Hi". iDestruct "Hi" as "[% %]"; simplify_eq. rel_rec_l. rel_rec_r. rel_load_l_atomic. iInv (logN .@ (x1,x2)) as ([v1 v2]) "(Hx1 & Hx2 & #Hvv) /=" "Hcl". iExists v1; iFrame. iModIntro. iNext. iIntros "Hx1". rel_load_r. iMod ("Hcl" with "[-]"). { iNext. iExists (_,_). by iFrame. } iSpecialize ("Hflip" with "Hvv"). simpl. iClear "Hvv". rewrite bin_log_related_eq /bin_log_related_def. iIntros (vvs ρ) "Hspec #HΓ /=". unfold env_subst. rewrite !Closed_subst_p_id. iIntros (j K) "Hj /=". tp_bind j (flip2 v2). iMod ("Hflip" with "Hj") as "Hfl". iModIntro. wp_bind (flip1 v1). iApply (wp_wand with "Hfl"). iIntros (v1'). iDestruct 1 as (v2') "[Hj #Hvv']". iInv (logN .@ (x1,x2)) as ([? ?]) "(Hx1 & Hx2 & #Hxs) /=" "Hcl". iApply (wp_store with "Hx1"); eauto using to_of_val. iNext. iIntros "Hx1". tp_store j. iMod ("Hcl" with "[-Hj]"). { iNext. iExists (_,_). by iFrame. } iModIntro. iExists (LitV ()); iFrame "Hj". eauto. - rel_vals; simpl; eauto. Qed. Lemma heapify_refinement_ez Γ E1 b1 b2 : ↑logrelN ⊆ E1 → {E1,E1;Δ;Γ} ⊨ b1 ≤log≤ b2 : bitτ -∗ {E1,E1;Δ;Γ} ⊨ heapify b1 ≤log≤ heapify b2 : bitτ. Proof. iIntros (?) "Hb1b2". iApply bin_log_related_app; eauto. iApply binary_fundamental_masked; eauto with typeable. Qed. End heapify_refinement. Theorem bit_heapify_ctx_refinement : ∅ ⊨ heapify bit_bool ≤ctx≤ heapify bit_nat : bitτ. Proof. eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ]. iStartProof. iApply heapify_refinement_ez; eauto. iApply bit_prerefinement. Qed.
 ... ... @@ -79,6 +79,13 @@ split; intros ?. - intros. by inv_head_step. Qed. Instance pure_unpack e1 e2 v1 `(to_val e1 = Some v1) : PureExec True (Unpack (Pack e1) e2) (e2 e1). Proof. split; intros ?. - intros. do 3 eexists. econstructor; eauto using to_of_val. - intros. by inv_head_step. Qed. Instance pure_if_true e1 e2 : PureExec True (If true e1 e2) e1. ... ...
 ... ... @@ -131,7 +131,7 @@ Tactic Notation "rel_pure_l" open_constr(ef) := |try iNext; simpl_subst/= (* new goal *)]) || fail "rel_pure_l: cannot find the reduct". Tactic Notation "rel_rec_l" := rel_pure_l (App _ _). Tactic Notation "rel_rec_l" := rel_pure_l (App (Rec _ _ _) _) || rel_pure_l (App _ _). Tactic Notation "rel_seq_l" := rel_rec_l. Tactic Notation "rel_let_l" := rel_rec_l. Tactic Notation "rel_fst_l" := rel_pure_l (Fst (Pair _ _)). ... ... @@ -182,7 +182,7 @@ Tactic Notation "rel_pure_r" open_constr(ef) := |try iNext; simpl_subst/= (* new goal *)]) || fail "rel_pure_r: cannot find the reduct". Tactic Notation "rel_rec_r" := rel_pure_r (App _ _). Tactic Notation "rel_rec_r" := rel_pure_r (App (Rec _ _ _) _) || rel_pure_r (App _ _). Tactic Notation "rel_seq_r" := rel_rec_r. Tactic Notation "rel_ret_r" := rel_rec_r. Tactic Notation "rel_fst_r" := rel_pure_r (Fst (Pair _ _)). ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!