diff --git a/typing.v b/typing.v index b1ca2cf2c315cc96af98343509f9a7a10d5c70c8..dbe15b5db002ed69e99b1ff3ca37f375f71fdb07 100644 --- a/typing.v +++ b/typing.v @@ -23,7 +23,7 @@ Section typing. Definition typed_program (Ï : perm) e := ∀ tid, heap_ctx ⊢ {{ Ï tid ★ tl_own tid ⊤ }} e {{ v, False }}. - Lemma typed_step_frame Ï e θ ξ: + Lemma typed_frame Ï e θ ξ: typed_step Ï e θ → typed_step (Ï â˜… ξ) e (λ ν, θ ν ★ ξ)%P. Proof. iIntros (Hwt tid) "#HEAP!#[[?$]?]". iApply (Hwt with "HEAP"). by iFrame. @@ -37,15 +37,15 @@ Section typing. iApply (Hwt with "HEAP"). by iFrame. Qed. - Lemma typed_step_bool Ï (b:Datatypes.bool) : + Lemma typed_bool Ï (b:Datatypes.bool) : typed_step_ty Ï #b bool. Proof. iIntros (tid) "_!#[_$]". wp_value. simpl. eauto. Qed. - Lemma typed_step_int Ï (z:Datatypes.nat) : + Lemma typed_int Ï (z:Datatypes.nat) : typed_step_ty Ï #z int. Proof. iIntros (tid) "_!#[_$]". wp_value. simpl. eauto. Qed. - Lemma typed_step_fn {A n} `{Duplicable _ Ï, Closed (f :b: xl +b+ []) e} θ : + Lemma typed_fn {A n} `{Duplicable _ Ï, Closed (f :b: xl +b+ []) e} θ : length xl = n → (∀ (a : A) (vl : vec val n) (fv : val) e', subst_l xl (map of_val vl) e = Some e' → @@ -64,7 +64,7 @@ Section typing. iNext. iApply (He with "HEAP"). done. by iFrame "★#". Qed. - Lemma typed_step_cont {n} `{Closed (f :b: xl +b+ []) e} Ï Î¸ : + Lemma typed_cont {n} `{Closed (f :b: xl +b+ []) e} Ï Î¸ : length xl = n → (∀ (vl : vec val n) (fv : val) e', subst_l xl (map of_val vl) e = Some e' → @@ -86,7 +86,7 @@ Section typing. iDestruct "Hf'" as %[=<-]. iApply ("IH'" with "Hθ Htl"). Qed. - Lemma typed_step_valuable e ty: + Lemma typed_valuable e ty: typed_step_ty (Valuable.of_expr e â— ty) e ty. Proof. iIntros (tid) "_!#[H$]". @@ -94,7 +94,7 @@ Section typing. by iApply Valuable.of_expr_wp. Qed. - Lemma typed_step_plus e1 e2 Ï1 Ï2: + Lemma typed_plus e1 e2 Ï1 Ï2: typed_step_ty Ï1 e1 int → typed_step_ty Ï2 e2 int → typed_step_ty (Ï1 ★ Ï2) (BinOp PlusOp e1 e2) int. Proof. @@ -106,7 +106,7 @@ Section typing. wp_op. iFrame. by iExists _. Qed. - Lemma typed_step_minus e1 e2 Ï1 Ï2: + Lemma typed_minus e1 e2 Ï1 Ï2: typed_step_ty Ï1 e1 int → typed_step_ty Ï2 e2 int → typed_step_ty (Ï1 ★ Ï2) (BinOp MinusOp e1 e2) int. Proof. @@ -118,7 +118,7 @@ Section typing. wp_op. iFrame. by iExists _. Qed. - Lemma typed_step_le e1 e2 Ï1 Ï2: + Lemma typed_le e1 e2 Ï1 Ï2: typed_step_ty Ï1 e1 int → typed_step_ty Ï2 e2 int → typed_step_ty (Ï1 ★ Ï2) (BinOp LeOp e1 e2) bool. Proof. @@ -130,7 +130,7 @@ Section typing. iFrame. wp_op; intros _; by iExists _. Qed. - Lemma typed_step_newlft Ï: + Lemma typed_newlft Ï: typed_step Ï Newlft (λ _, ∃ α, [α]{1} ★ α ∋ top)%P. Proof. iIntros (tid) "_!#[_$]". wp_value. iMod lft_begin as (α) "[?#?]". done. @@ -138,7 +138,7 @@ Section typing. 2:by iModIntro; iExists α; iFrame. eauto. Qed. - Lemma typed_step_endlft κ Ï: + Lemma typed_endlft κ Ï: typed_step (κ ∋ Ï â˜… [κ]{1}) Endlft (λ _, Ï)%P. Proof. iIntros (tid) "_!#[[Hextr [Htok #Hlft]]$]". @@ -150,7 +150,7 @@ Section typing. by wp_seq. Qed. - Lemma typed_step_alloc Ï (n : nat): + Lemma typed_alloc Ï (n : nat): 0 < n → typed_step_ty Ï (Alloc #n) (own 1 (uninit n)). Proof. iIntros (? tid) "#HEAP!#[_$]". wp_alloc l vl as "H↦" "H†". iIntros "!>". @@ -158,7 +158,7 @@ Section typing. apply (inj Z.of_nat) in H3. iExists _. iFrame. eauto. Qed. - Lemma typed_step_free ty e: + Lemma typed_free ty e: typed_step (Valuable.of_expr e â— own 1 ty) (Free #ty.(ty_size) e) (λ _, top). Proof. iIntros (tid) "#HEAP!#[Hown$]". @@ -242,7 +242,7 @@ Section typing. iMod ("Hclose" with "Htok") as "$". iExists _. eauto. Qed. - Lemma typed_step_deref ty Ï1 Ï2 e: + Lemma typed_deref ty Ï1 Ï2 e: ty.(ty_size) = 1%nat → consumes ty Ï1 Ï2 → typed_step (Ï1 (Valuable.of_expr e)) (!e) (λ v, v â— ty ★ Ï2 (Valuable.of_expr e))%P. Proof. @@ -256,7 +256,7 @@ Section typing. by iApply "Hclose". Qed. - Lemma typed_step_deref_uniq_borrow_own ty e κ κ' q q': + Lemma typed_deref_uniq_borrow_own ty e κ κ' q q': typed_step (Valuable.of_expr e â— &uniq{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q}) (!e) (λ v, v â— &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P. @@ -278,7 +278,7 @@ Section typing. iMod ("Hclose" with "Htok"). iFrame "#★". iIntros "!>". iExists _. eauto. Qed. - Lemma typed_step_deref_shr_borrow_own ty e κ κ' q q': + Lemma typed_deref_shr_borrow_own ty e κ κ' q q': typed_step (Valuable.of_expr e â— &shr{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q}) (!e) (λ v, v â— &shr{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P. @@ -312,7 +312,7 @@ Section typing. iModIntro. iExists _. eauto. Qed. - Lemma typed_step_deref_uniq_borrow_borrow ty e κ κ' κ'' q: + Lemma typed_deref_uniq_borrow_borrow ty e κ κ' κ'' q: typed_step (Valuable.of_expr e â— &uniq{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'') (!e) (λ v, v â— &uniq{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P. @@ -336,7 +336,7 @@ Section typing. iModIntro. iExists _. eauto. Qed. - Lemma typed_step_deref_shr_borrow_borrow ty e κ κ' κ'' q: + Lemma typed_deref_shr_borrow_borrow ty e κ κ' κ'' q: typed_step (Valuable.of_expr e â— &shr{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'') (!e) (λ v, v â— &shr{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P. @@ -380,7 +380,7 @@ Section typing. iMod ("Hclose" with "Htok") as "$". iExists _. eauto. Qed. - Lemma typed_step_assign Ï1 Ï2 ty e1 e2: + Lemma typed_assign Ï1 Ï2 ty e1 e2: ty.(ty_size) = 1%nat → update ty Ï1 Ï2 → typed_step (Ï1 (Valuable.of_expr e1) ★ Valuable.of_expr e2 â— ty) (e1 <- e2) @@ -398,7 +398,7 @@ Section typing. by rewrite heap_mapsto_vec_singleton. Qed. - Lemma typed_step_memcpy Ï1 Ï1' Ï2 Ï2' ty e1 e2: + Lemma typed_memcpy Ï1 Ï1' Ï2 Ï2' ty e1 e2: update ty Ï1' Ï1 → consumes ty Ï2' Ï2 → typed_step (Ï1' (Valuable.of_expr e1) ★ Ï2' (Valuable.of_expr e2)) (e1 <-{ty.(ty_size)} !e2) @@ -416,4 +416,41 @@ Section typing. iMod ("Hcons" with "H↦'") as "[$$]". iApply "Hupd". by iFrame. Qed. + Lemma typed_weaken Ï1 Ï2 e: + typed_program Ï2 e → (Ï1 ⇒ Ï2) → typed_program Ï1 e. + Proof. + iIntros (HÏ2 HÏ12 tid) "#HEAP!#[HÏ1 Htl]". + iMod (HÏ12 with "HÏ1"). iApply (HÏ2 with "HEAP"). by iFrame. + Qed. + + Lemma typed_program_exists {A} Ï Î¸ e: + (∀ x:A, typed_program (Ï â˜… θ x) e) → + typed_program (Ï â˜… ∃ x, θ x) e. + Proof. + iIntros (Hwt tid) "#HEAP!#[[HÏ Hθ]?]". iDestruct "Hθ" as (x) "Hθ". + iApply (Hwt with "HEAP"). by iFrame. + Qed. + + Lemma typed_step_program Ï Î¸ e K: + typed_step Ï e θ → + (∀ v, typed_program (θ (Some v)) (fill K (of_val v))) → + typed_program Ï (fill K e). + Proof. + iIntros (He HK tid) "#HEAP!#[HÏ Htl]". + iApply wp_bind. iApply wp_wand_r. iSplitL. + iApply (He with "HEAP [-]"); by iFrame. + iIntros (v) "[Hθ Htl]". iApply (HK with "HEAP"). by iFrame. + Qed. + + Lemma typed_if Ï e1 e2 e: + typed_program Ï e1 → typed_program Ï e2 → + typed_program (Ï â˜… Valuable.of_expr e â— bool) (if: e then e1 else e2). + Proof. + iIntros (He1 He2 tid) "#HEAP!#[[HÏ Hâ—]Htl]". + destruct (Valuable.of_expr e) eqn:He; try iDestruct "Hâ—" as "[]". + iDestruct "Hâ—" as (b) "Heq". iDestruct "Heq" as %[= ->]. + wp_bind e. iApply Valuable.of_expr_wp. done. wp_if. destruct b; iNext. + iApply (He1 with "HEAP"); by iFrame. iApply (He2 with "HEAP"); by iFrame. + Qed. + End typing.