diff --git a/_CoqProject b/_CoqProject index f4938067aa076015e602adf7bfd9ec0638652b36..81cbae1354d3bd9e555bf5fdf7fd912d450ebd36 100644 --- a/_CoqProject +++ b/_CoqProject @@ -44,3 +44,4 @@ theories/typing/cont.v theories/typing/fixpoint.v theories/typing/type_sum.v theories/typing/tests/get_x.v +theories/typing/tests/rebor.v diff --git a/theories/lang/derived.v b/theories/lang/derived.v index a649ab181f49f124497c91ab00b2110513796fcd..c3c5be5e7897feb8d79e9afe7fb57451a236c49f 100644 --- a/theories/lang/derived.v +++ b/theories/lang/derived.v @@ -14,8 +14,8 @@ Notation SeqCtx e2 := (LetCtx BAnon e2). Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)). Coercion lit_of_bool : bool >-> base_lit. Notation If e0 e1 e2 := (Case e0 [e2;e1]). -Definition Newlft := Lit LitUnit. -Definition Endlft := Skip. +Notation Newlft := (Lit LitUnit) (only parsing). +Notation Endlft := Skip (only parsing). Section derived. Context `{ownPG lrust_lang Σ}. diff --git a/theories/lang/notation.v b/theories/lang/notation.v index 1caf26f4563ce4fdbd5295e008f31b95488aa489..915062ba05a8abba8506803f9d0d5a1923667631 100644 --- a/theories/lang/notation.v +++ b/theories/lang/notation.v @@ -58,9 +58,9 @@ Notation "λ: xl , e" := (Lam xl%RustB e%E) (at level 102, xl at level 1, e at level 200) : expr_scope. Notation "λ: xl , e" := (LamV xl%RustB e%E) (at level 102, xl at level 1, e at level 200) : val_scope. -Notation "'funrec:' f xl → k := e" := (rec: f (k::xl) := e)%E +Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%E (only parsing, at level 102, f, xl at level 1, e at level 200) : expr_scope. -Notation "'funrec:' f xl → k := e" := (rec: f (k::xl) := e)%V +Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V (only parsing, at level 102, f, xl at level 1, e at level 200) : val_scope. Notation "'let:' x := e1 'in' e2" := diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v index 3c3dadd9afbc5ea44f881f4bfb6ca3e503b0a141..9cc162d961e2e16b77558dc3d8df4da9ea8e565c 100644 --- a/theories/typing/borrow.v +++ b/theories/typing/borrow.v @@ -25,12 +25,14 @@ Section borrow. by iMod ("Hext" with "H†") as "$". Qed. - Lemma tctx_extract_hasty_borrow E L p n ty κ T : - tctx_extract_hasty E L p (&uniq{κ}ty) ((p â— own n ty)::T) + Lemma tctx_extract_hasty_borrow E L p n ty ty' κ T : + subtype E L ty' ty → + tctx_extract_hasty E L p (&uniq{κ}ty) ((p â— own n ty')::T) ((p â—{κ} own n ty)::T). Proof. - rewrite tctx_extract_hasty_unfold. - apply (tctx_incl_frame_r _ [_] [_;_]), tctx_borrow. + rewrite tctx_extract_hasty_unfold=>Htyty'. + apply (tctx_incl_frame_r _ [_] [_;_]). rewrite subtype_tctx_incl. + by apply tctx_borrow. by f_equiv. Qed. (* See the comment above [tctx_extract_hasty_share] in [uniq_bor.v]. *) @@ -139,5 +141,5 @@ Section borrow. Qed. End borrow. -Hint Resolve tctx_extract_hasty_borrow - tctx_extract_hasty_borrow_share : lrust_typing. +Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share + | 10 : lrust_typing. diff --git a/theories/typing/function.v b/theories/typing/function.v index 9a63ce18d8227f60115d28e7ae54364547415b29..0b97434e0d4952aa69802914c234c331d6b4d359 100644 --- a/theories/typing/function.v +++ b/theories/typing/function.v @@ -155,7 +155,6 @@ Section typing. rewrite /typed_body. iNext. iIntros "*". iApply "Hf". Qed. - (* TODO: Define some syntactic sugar for calling and letrec like we do on paper. *) Lemma type_call' {A} E L E' T p (ps : list path) (tys : A → vec type (length ps)) ty k x : elctx_sat E L (E' x) → @@ -245,37 +244,37 @@ Section typing. eapply type_call; try done. constructor. done. Qed. - Lemma type_rec {A} E L E' fb kb (argsb : list binder) e + Lemma type_rec {A} E L E' fb (argsb : list binder) e (tys : A → vec type (length argsb)) ty T `{!CopyC T, !SendC T} : - Closed (fb :b: kb :b: argsb +b+ []) e → + Closed (fb :b: "return" :b: argsb +b+ []) e → (∀ x (f : val) k (args : vec val (length argsb)), typed_body (E' x) [] [k â—cont([], λ v : vec _ 1, [v!!!0 â— ty x])] ((f â— fn E' tys ty) :: zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T) - (subst_v (fb :: kb :: argsb) (f ::: k ::: args) e)) → - typed_instruction_ty E L T (funrec: fb argsb → kb := e) (fn E' tys ty). + (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) → + typed_instruction_ty E L T (funrec: fb argsb := e) (fn E' tys ty). Proof. iIntros (Hc Hbody) "!# * #HEAP #LFT $ $ $ #HT". iApply wp_value. - { simpl. rewrite decide_left. done. } + { simpl. rewrite ->(decide_left Hc). done. } rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit. { simpl. rewrite decide_left. done. } - iExists fb, kb, argsb, e, _. iSplit. done. iSplit. done. iNext. clear qE. + iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext. clear qE. iIntros (x k args) "!#". iIntros (tid' qE) "_ _ Htl HE HL HC HT'". iApply (Hbody with "* HEAP LFT Htl HE HL HC"). rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH". by iApply sendc_change_tid. Qed. - Lemma type_fn {A} E L E' kb (argsb : list binder) e + Lemma type_fn {A} E L E' (argsb : list binder) e (tys : A → vec type (length argsb)) ty T `{!CopyC T, !SendC T} : - Closed (kb :b: argsb +b+ []) e → + Closed ("return" :b: argsb +b+ []) e → (∀ x k (args : vec val (length argsb)), typed_body (E' x) [] [k â—cont([], λ v : vec _ 1, [v!!!0 â— ty x])] (zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T) - (subst_v (kb :: argsb) (k ::: args) e)) → - typed_instruction_ty E L T (funrec: <> argsb → kb := e) (fn E' tys ty). + (subst_v (BNamed "return" :: argsb) (k ::: args) e)) → + typed_instruction_ty E L T (funrec: <> argsb := e) (fn E' tys ty). Proof. intros. apply type_rec; try done. intros. rewrite -typed_body_mono //=. eapply contains_tctx_incl. by constructor. diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v index 0553b61ccb704997e8daf6c67b48c6b37da09252..e5a4a798016f8559da2edda457347c691e4945ef 100644 --- a/theories/typing/product_split.v +++ b/theories/typing/product_split.v @@ -388,18 +388,14 @@ Section product_split. Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_shr_prod. Qed. End product_split. -(* We make sure that this is applied after [tctx_extract_hasty_here] but before - [tctx_extract_hasty_cons]. *) +(* We make sure that splitting and merging are applied after everything else. *) Hint Resolve tctx_extract_split_own_prod2 tctx_extract_split_uniq_prod2 tctx_extract_split_shr_prod2 tctx_extract_split_own_prod tctx_extract_split_uniq_prod tctx_extract_split_shr_prod - | 60 : lrust_typing. - -(* We make sure that this is applied after everything. *) -Hint Resolve tctx_extract_merge_own_prod2 tctx_extract_merge_uniq_prod2 + tctx_extract_merge_own_prod2 tctx_extract_merge_uniq_prod2 tctx_extract_merge_shr_prod2 tctx_extract_merge_own_prod tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod - | 150 : lrust_typing. + | 100 : lrust_typing. Hint Extern 0 (tctx_extract_hasty _ _ _ _ (hasty_ptr_offsets _ _ _ _) _) => diff --git a/theories/typing/programs.v b/theories/typing/programs.v index 68b0a6d9f5d22668602c525647d8d9fd9e78f04b..8a24832e2b79e771d309b942c7ad747b09d6e3bf 100644 --- a/theories/typing/programs.v +++ b/theories/typing/programs.v @@ -130,13 +130,9 @@ Section typing_rules. tctx_extract_ctx E L T1 T T' → (typed_body E L C (T2 ++ T') e') → typed_body E L C T (e ;; e'). - Proof. - intros ? Hinst ? Hbody. eapply type_let; [done| |done|]. - (* FIXME: done divergese on the remaining goals. *) - exact Hinst. intros. exact Hbody. - Qed. + Proof. intros. by eapply (type_let E L T T' T1 (λ _, T2)). Qed. - Lemma typed_newlft E L C T κs e : + Lemma type_newlft {E L C T} κs e : Closed [] e → (∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) → typed_body E L C T (Newlft ;; e). @@ -151,7 +147,7 @@ Section typing_rules. (* TODO: It should be possible to show this while taking only one step. Right now, we could take two. *) - Lemma typed_endlft E L C T1 T2 κ κs e : + Lemma type_endlft E L C T1 T2 κ κs e : Closed [] e → UnblockTctx κ T1 T2 → typed_body E L C T2 e → typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e). Proof. @@ -163,6 +159,23 @@ Section typing_rules. iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto. Qed. + Lemma type_path_instr {E L} p ty : + typed_instruction_ty E L [p â— ty] p ty. + Proof. + iIntros "!# * _ _ $$$ ?". rewrite tctx_interp_singleton. + iApply (wp_hasty with "[-]"). done. iIntros (v) "_ Hv". + rewrite tctx_interp_singleton. iExists v. iFrame. by rewrite eval_path_of_val. + Qed. + + Lemma type_letpath {E L} ty C T T' x p e : + Closed (x :b: []) e → + tctx_extract_hasty E L p ty T T' → + (∀ (v : val), typed_body E L C ((v â— ty) :: T') (subst' x v e)) → + typed_body E L C T (let: x := p in e). + Proof. + intros. eapply type_let; [done|by apply type_path_instr|solve_typing|by simpl]. + Qed. + Lemma type_assign_instr {E L} ty ty1 ty1' p1 p2 : typed_write E L ty1 ty ty1' → typed_instruction E L [p1 â— ty1; p2 â— ty] (p1 <- p2) (λ _, [p1 â— ty1']%TC). @@ -182,7 +195,7 @@ Section typing_rules. rewrite tctx_interp_singleton tctx_hasty_val' //. Qed. - Lemma type_assign {E L} ty1 C T T' ty ty1' p1 p2 e: + Lemma type_assign {E L} ty1 ty ty1' C T T' p1 p2 e: Closed [] e → tctx_extract_ctx E L [p1 â— ty1; p2 â— ty] T T' → typed_write E L ty1 ty ty1' → @@ -269,7 +282,6 @@ Section typing_rules. typed_body E L C ((p1 â— ty1') :: (p2 â— ty2') :: T') e → typed_body E L C T (p1 <⋯ !{n}p2;; e). Proof. - intros ?? Hwr Hrd ??. eapply type_seq; [done|eapply type_memcpy_instr| |by simpl]; first done. - exact Hwr. exact Hrd. done. + intros. by eapply type_seq; [|by eapply (type_memcpy_instr ty ty1 ty1')|..]. Qed. End typing_rules. diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v index f76f6aa78d181fa469ffccf8b049e1571496949e..61ba2c297d6e59e1bd3e9419ddea226b378395fe 100644 --- a/theories/typing/tests/get_x.v +++ b/theories/typing/tests/get_x.v @@ -1,3 +1,4 @@ +From lrust.lifetime Require Import definitions. From lrust.lang Require Import new_delete. From lrust.typing Require Import programs product product_split own uniq_bor shr_bor int function lft_contexts uninit cont. @@ -7,10 +8,10 @@ Section get_x. Context `{typeG Σ}. Definition get_x := - (funrec: <> ["p"] → "ret" := + (funrec: <> ["p"] := let: "p'" := !"p" in letalloc: "r" := "p'" +â‚— #0 in - delete [ #1; "p"] ;; "ret" ["r":expr])%E. + delete [ #1; "p"] ;; "return" ["r":expr])%E. Lemma get_x_type : typed_instruction_ty [] [] [] get_x @@ -18,14 +19,10 @@ Section get_x. (λ α, own 1 (&shr{α} int))). Proof. apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>p. simpl_subst. - eapply type_deref; try solve_typing. by apply read_own_move. done. - intros p'; simpl_subst. - + intros p'; simpl_subst. eapply (type_letalloc_1 (&shr{α}int)); (try solve_typing)=>r. simpl_subst. - eapply type_delete; try solve_typing. - eapply type_jump with (args := [r]); solve_typing. Qed. End get_x. diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v index bfa53826c49bc651360a543dcee6bf6c401e057d..4e2866597f29ec51814dabae424a301f5631c0a5 100644 --- a/theories/typing/type_context.v +++ b/theories/typing/type_context.v @@ -255,7 +255,7 @@ Section type_context. Global Arguments tctx_extract_hasty _%EL _%LL _%E _%T _%TC _%TC. Definition tctx_extract_hasty_unfold : tctx_extract_hasty = λ E L p ty T T', tctx_incl E L T ((p â— ty)::T') := eq_refl. - Lemma tctx_extract_hasty_cons E L p ty T T' x : + Lemma tctx_extract_hasty_further E L p ty T T' x : tctx_extract_hasty E L p ty T T' → tctx_extract_hasty E L p ty (x::T) (x::T'). Proof. unfold tctx_extract_hasty=>->. apply contains_tctx_incl, submseteq_swap. Qed. @@ -272,6 +272,9 @@ Section type_context. Proof. intros. by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl. Qed. + Lemma tctx_extract_hasty_here_eq E L p ty T : + tctx_extract_hasty E L p ty ((p â— ty)::T) T. + Proof. by apply tctx_extract_hasty_here. Qed. Definition tctx_extract_blocked E L p κ ty T T' : Prop := tctx_incl E L T ((p â—{κ} ty)::T'). @@ -343,10 +346,22 @@ Section type_context. End type_context. Global Opaque tctx_extract_ctx tctx_extract_hasty tctx_extract_blocked. -Hint Resolve tctx_extract_hasty_here_copy : lrust_typing. -Hint Resolve tctx_extract_hasty_here | 50 : lrust_typing. -Hint Resolve tctx_extract_hasty_cons | 100 : lrust_typing. -Hint Extern 1 (Copy _) => typeclasses eauto : lrust_typing. +Hint Resolve tctx_extract_hasty_here_copy 1 : lrust_typing. +Hint Resolve tctx_extract_hasty_here | 20 : lrust_typing. +Hint Resolve tctx_extract_hasty_further | 50 : lrust_typing. Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons tctx_extract_ctx_nil tctx_extract_ctx_hasty tctx_extract_ctx_blocked tctx_extract_ctx_incl : lrust_typing. + +(* In general, we want reborrowing to be tried before subtyping, so + that we get the extraction. However, in the case the types match + exactly, we want to NOT use reborrowing. Therefore, we add + [tctx_extract_hasty_here_eq] as a hint with a very low cost. + + However, we want this hint to be used after + [tctx_extract_hasty_here_copy], so that we keep the typing it in + the environment if the type is copy. But due to a bug in Coq, we + cannot enforce this using [Hint Resolve]. Cf: + https://coq.inria.fr/bugs/show_bug.cgi?id=5299 *) +Hint Extern 2 (tctx_extract_hasty _ _ ?p _ ((?p â— _) :: _) _) => + eapply tctx_extract_hasty_here_eq. diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v index 9e553c7394a554aa818e82c24f29b1d6a3963b05..e20a4f686fd994568680be66400a4c179b702df4 100644 --- a/theories/typing/uniq_bor.v +++ b/theories/typing/uniq_bor.v @@ -255,6 +255,7 @@ Section typing. Qed. End typing. -Hint Resolve uniq_mono' uniq_proper' tctx_extract_hasty_share - tctx_extract_hasty_reborrow : lrust_typing. -Hint Resolve tctx_extract_hasty_share_samelft | 0 : lrust_typing. +Hint Resolve uniq_mono' uniq_proper' : lrust_typing. +Hint Resolve tctx_extract_hasty_reborrow | 10 : lrust_typing. +Hint Resolve tctx_extract_hasty_share | 10 : lrust_typing. +Hint Resolve tctx_extract_hasty_share_samelft | 9 : lrust_typing.