Commit 02c8418b by Dan Frumin

Clean up the bit file

parent 1ff8a563
......@@ -21,8 +21,9 @@ Definition bit_nat : val :=
(** ** Boolean bit *)
Lemma bit_bool_type Γ :
typed Γ bit_bool bitτ.
Proof. unfold bitτ. simpl. unlock. solve_typed.
(* TODO: solve_typed does not solve this one without simplifying/unlocking *)
Proof.
unfold bitτ. simpl. unlock. solve_typed.
(* TODO: solve_typed does not solve this one without simplifying/unlocking *)
Qed.
Hint Resolve bit_bool_type : typeable.
......@@ -117,6 +118,7 @@ Hint Resolve heapify_type : typeable.
Section heapify_refinement.
Context `{logrelG Σ}.
Variable (Δ : list (prodC valC valC -n> iProp Σ)).
Notation D := (prodC valC valC -n> iProp Σ).
Lemma heapify_refinement_ez Γ E1 b1 b2 :
logrelN E1
......@@ -128,89 +130,6 @@ Section heapify_refinement.
iApply binary_fundamental_masked; eauto with typeable.
Qed.
(* 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. *)
(* rel_proj_l. *)
(* rel_rec_l. *)
(* rel_proj_l. rel_proj_l. *)
(* rel_rec_l. *)
(* rel_proj_l. rel_proj_l. *)
(* rel_rec_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_val; 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_val; 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 (#()); iFrame "Hj". eauto. *)
(* - rel_vals; simpl; eauto. *)
(* Qed. *)
End heapify_refinement.
Theorem bit_heapify_ctx_refinement :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment