A bit more syntactic sugar. More proof rules for letcall, letalloc.

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq e0789039ed0dcb01b6249fec2d5a36f66e5de21c
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 53fe9f4028ceeb7346a528ad0748fd0f3de3edd5

theories/lang/lang.v

@@ -19,6 +19,13 @@ Inductive binder := BAnon | BNamed : string → binder.
 Delimit Scope lrust_binder_scope with RustB.
 Bind Scope lrust_binder_scope with binder.
 
+Notation "a :: b" := (@cons binder a%RustB b%RustB)
+  (at level 60, right associativity) : lrust_binder_scope.
+Notation "[ x1 ; x2 ; .. ; xn ]" :=
+  (@cons binder x1%RustB (@cons binder x2%RustB
+        (..(@cons binder xn%RustB (@nil binder))..))) : lrust_binder_scope.
+Notation "[ x ]" := (@cons binder x%RustB (@nil binder)) : lrust_binder_scope.
+
 Definition cons_binder (mx : binder) (X : list string) : list string :=
   match mx with BAnon => X | BNamed x => x :: X end.
 Infix ":b:" := cons_binder (at level 60, right associativity).
@@ -477,6 +484,23 @@ Proof. intros. apply is_closed_subst with []; set_solver. Qed.
 Lemma is_closed_of_val X v : is_closed X (of_val v).
 Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
 
+Lemma subst_is_closed X x es e :
+  is_closed X es → is_closed (x::X) e → is_closed X (subst x es e).
+Proof.
+  revert e X. fix 1; destruct e=>X //=; repeat (case_bool_decide=>//=);
+    try naive_solver; rewrite ?andb_True; intros.
+  - set_solver.
+  - eauto using is_closed_weaken with set_solver.
+  - eapply is_closed_weaken; first done.
+    destruct (decide (BNamed x = f)), (decide (BNamed x ∈ xl)); set_solver.
+  - split; first naive_solver. induction el; naive_solver.
+  - split; first naive_solver. induction el; naive_solver.
+Qed.
+
+Lemma subst'_is_closed X b es e :
+  is_closed X es → is_closed (b:b:X) e → is_closed X (subst' b es e).
+Proof. destruct b; first done. apply subst_is_closed. Qed.
+
 (* Operations on literals *)
 Lemma lit_eq_state σ1 σ2 l1 l2 :
   (∀ l, σ1 !! l = None ↔ σ2 !! l = None) →

theories/lang/memcpy.v

@@ -9,7 +9,10 @@ Definition memcpy : val :=
          "memcpy" ["dst" +ₗ #1 ; "len" - #1 ; "src" +ₗ #1].
 Global Opaque memcpy.
 
-Notation "e1 <-{ n } ! e2" := (App memcpy [e1%E ; Lit (LitInt n) ; e2%E])
+Notation "e1 <-{ n } ! e2" :=
+  (memcpy (@cons expr e1%E
+          (@cons expr (Lit n)
+          (@cons expr e2%E nil))))
   (at level 80, n at next level, format "e1  <-{ n }  ! e2") : expr_scope.
 
 Notation "e1 <-[ i ]{ n } ! e2" :=

theories/lang/new_delete.v

 From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
-From lrust.lang Require Import heap proofmode.
+From lrust.lang Require Import heap proofmode memcpy.
 
 Definition new : val :=
   λ: ["n"],
@@ -38,4 +38,12 @@ Section specs.
     iIntros (? ? Φ) "(#Hinv & H↦ & [H†|%]) HΦ";
       wp_lam; wp_op; intros ?; try lia; wp_if; try wp_free; by iApply "HΦ".
   Qed.
-End specs.
+End specs.
\ No newline at end of file
+
+(* FIXME : why are these notations not pretty-printed. *)
+Notation "'letalloc:' x := e1 'in' e2" :=
+  ((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
+  (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
+Notation "'letalloc:' x :={ n } ! e1 'in' e2" :=
+  ((Lam (@cons binder x%E%E%E nil) (x <-{ n%Z%V } ! e1 ;; e2)) [new [ #n]%E%E])%E
+  (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.

theories/lang/notation.v

@@ -36,45 +36,50 @@ Notation "e1 <-ˢᶜ e2" := (Write ScOrd e1%E e2%E)
   (at level 80) : expr_scope.
 Notation "e1 <- e2" := (Write Na1Ord e1%E e2%E)
   (at level 80) : expr_scope.
-Notation "'rec:' f [ x1 ; .. ; xn ] := e" :=
-  (Rec f%RustB ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
-  (at level 102, f at level 1, x1 at level 1, xn at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f [ x1 ; .. ; xn ] := e" :=
-  (RecV f%RustB ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
-  (at level 102, f at level 1, x1 at level 1, xn at level 1, e at level 200) : val_scope.
-Notation "'rec:' f [ ] := e" := (Rec f%RustB nil e%E)
-  (at level 102, f at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f [ ] := e" := (RecV f%RustB nil e%E)
-  (at level 102, f at level 1, e at level 200) : val_scope.
+Notation "'rec:' f xl := e" := (Rec f%RustB xl%RustB e%E)
+  (at level 102, f, xl at level 1, e at level 200) : expr_scope.
+Notation "'rec:' f xl := e" := (RecV f%RustB xl%RustB e%E)
+  (at level 102, f, xl at level 1, e at level 200) : val_scope.
 Notation "e1 +ₗ e2" := (BinOp OffsetOp e1%E e2%E)
   (at level 50, left associativity) : expr_scope.
 
-(** Derived notions, in order of declaration. The notations for let and seq
-are stated explicitly instead of relying on the Notations Let and Seq as
-defined above. This is needed because App is now a coercion, and these
+(** Derived notions. The notations for let and seq are stated
+explicitly instead of relying on the Notations Let and Seq as defined
+above. This is needed because App is now a coercion, and these
 notations are otherwise not pretty printed back accordingly. *)
-Notation "λ: [ x1 ; .. ; xn ] , e" :=
-  (Lam ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
-  (at level 102, x1 at level 1, xn at level 1, e at level 200) : expr_scope.
-Notation "λ: [ x1 ; .. ; xn ] , e" :=
-  (LamV ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
-  (at level 102, x1 at level 1, xn at level 1, e at level 200) : val_scope.
-Notation "λ: [ ] , e" := (Lam nil e%E)
-  (at level 102, e at level 200) : expr_scope.
-Notation "λ: [ ] , e" := (LamV nil e%E)
-  (at level 102, e at level 200) : val_scope.
 
-Notation "'let:' x := e1 'in' e2" := (Lam [x%RustB] e2%E [e1%E])
+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
+  (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
+  (only parsing, at level 102, f, xl at level 1, e at level 200) : val_scope.
+
+Notation "'let:' x := e1 'in' e2" :=
+  ((Lam (@cons binder x%RustB nil) e2%E) (@cons expr e1%E nil))
   (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
-Notation "e1 ;; e2" := (Lam [BAnon] e2%E [e1%E])
+Notation "e1 ;; e2" := (let: <> := e1 in e2)%E
   (at level 100, e2 at level 200, format "e1  ;;  e2") : expr_scope.
 (* These are not actually values, but we want them to be pretty-printed. *)
-Notation "'let:' x := e1 'in' e2" := (LamV [x%RustB] e2%E [e1%E])
+Notation "'let:' x := e1 'in' e2" :=
+  (LamV (@cons binder x%RustB nil) e2%E (@cons expr e1%E nil))
   (at level 102, x at level 1, e1, e2 at level 200) : val_scope.
-Notation "e1 ;; e2" := (LamV [BAnon] e2%E [e1%E])
+Notation "e1 ;; e2" := (let: <> := e1 in e2)%V
   (at level 100, e2 at level 200, format "e1  ;;  e2") : val_scope.
 
+Notation "'letcont:' k xl := e1 'in' e2" :=
+  ((Lam (@cons binder k%RustB nil) e2%E) [Rec k%RustB xl%RustB e1%E])
+  (only parsing, at level 102, k, xl at level 1, e1, e2 at level 200) : expr_scope.
+
+Notation "'call:' f args → k" := (f (@cons expr k args))%E
+  (only parsing, at level 102, f, args, k at level 1) : expr_scope.
+Notation "'letcall:' x := f args 'in' e" :=
+  (letcont: "_k" [ x ] := e in call: f args → "_k")%E
+  (at level 102, x, f, args at level 1, e at level 200) : expr_scope.
+
 Notation "e1 <-[ i ] '☇'" := (e1 <- #i)%E
   (only parsing, at level 80) : expr_scope.
-Notation "e1 <-[ i ] e2" := (e1<-[i] ☇ ;; e1+ₗ#1 <- e2)%E
- (at level 80) : expr_scope.
+Notation "e1 <-[ i ] e2" := (e1 <-[i] ☇ ;; e1+ₗ#1 <- e2)%E
+  (at level 80) : expr_scope.

theories/lang/tactics.v

@@ -3,7 +3,7 @@ From lrust.lang Require Export lang.
 
 (** We define an alternative representation of expressions in which the
 embedding of values and closed expressions is explicit. By reification of
-expressions into this type we can implementation substitution, closedness
+expressions into this type we can implement substitution, closedness
 checking, atomic checking, and conversion into values, by computation. *)
 Module W.
 Inductive expr :=

theories/typing/cont.v

@@ -19,12 +19,12 @@ Section typing.
     rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "* Htl HL HT").
   Qed.
 
-  Lemma type_cont L1 {argsb} T' E L2 C T  econt e2 kb :
+  Lemma type_cont argsb L1 T' E L2 C T  econt e2 kb :
     Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
     (∀ k args, typed_body E L1 (k ◁cont(L1, T') :: C) (T' args)
                           (subst_v (kb::argsb) (k:::args) econt)) →
     (∀ k, typed_body E L2 (k ◁cont(L1, T') :: C) T (subst' kb k e2)) →
-    typed_body E L2 C T (let: kb := Rec kb argsb econt in e2).
+    typed_body E L2 C T (letcont: kb argsb := econt in e2).
   Proof.
     iIntros (Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
     { simpl. rewrite decide_left. done. }

theories/typing/function.v

@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import vector.
 From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import programs.
+From lrust.typing Require Import programs cont.
 
 Section fn.
   Context `{typeG Σ} {A : Type} {n : nat}.
@@ -140,11 +140,11 @@ Section typing.
 
   (* 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 :
+                         (tys : A → vec type (length ps)) ty k x :
     elctx_sat E L (E' x) →
     typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ ty x) :: T)]
                ((p ◁ fn E' tys ty) :: zip_with TCtx_hasty ps (tys x) ++ T)
-               (p (of_val k :: ps)).
+               (call: p ps → k).
   Proof.
     iIntros (HE tid qE) "#HEAP #LFT Htl HE HL HC".
     rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
@@ -187,7 +187,7 @@ Section typing.
     tctx_extract_ctx E L (zip_with TCtx_hasty ps (tys x)) T T' →
     (k ◁cont(L, T''))%CC ∈ C →
     (∀ ret : val, tctx_incl E L ((ret ◁ ty x)::T') (T'' [# ret])) →
-    typed_body E L C T (p (of_val k :: ps)).
+    typed_body E L C T (call: p ps → k).
   Proof.
     intros Hfn HE HTT' HC HT'T''.
     rewrite -typed_body_mono /flip; last done; first by eapply type_call.
@@ -197,6 +197,36 @@ Section typing.
       apply copy_elem_of_tctx_incl; last done. apply _.
   Qed.
 
+  Lemma type_letcall {A} x E L E' C T T' p (ps : list path)
+                        (tys : A → vec type (length ps)) ty b e :
+    Closed (b :b: []) e → Closed [] p → Forall (Closed []) ps →
+    (p ◁ fn E' tys ty)%TC ∈ T →
+    elctx_sat E L (E' x) →
+    tctx_extract_ctx E L (zip_with TCtx_hasty ps (tys x)) T T' →
+    (∀ ret : val, typed_body E L C ((ret ◁ ty x)::T') (subst' b ret e)) →
+    typed_body E L C T (letcall: b := p ps in e).
+  Proof.
+    intros ?? Hpsc ????. eapply (type_cont [_] _ (λ r, (r!!!0 ◁ ty x) :: T')%TC).
+    - (* TODO : make [solve_closed] work here. *)
+      eapply is_closed_weaken; first done. set_solver+.
+    - (* TODO : make [solve_closed] work here. *)
+      rewrite /Closed /= !andb_True. split.
+      + by eapply is_closed_weaken, list_subseteq_nil.
+      + eapply Is_true_eq_left, forallb_forall, List.Forall_forall, Forall_impl=>//.
+        intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
+    - intros k ret. inv_vec ret=>ret v0. inv_vec v0. rewrite /subst_v /=.
+      rewrite ->(is_closed_subst []), incl_cctx_incl; first done; try set_solver+.
+      apply subst'_is_closed; last done. apply is_closed_of_val.
+    - intros.
+      (* TODO : make [simpl_subst] work here. *)
+      change (subst' "_k" k (p (Var "_k" :: ps))) with
+             ((subst "_k" k p) (of_val k :: map (subst "_k" k) ps)).
+      rewrite is_closed_nil_subst //.
+      assert (map (subst "_k" k) ps = ps) as ->.
+      { clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
+      eapply type_call'; try done. constructor. done.
+  Qed.
+
   Lemma type_fn {A} E L E' fb kb (argsb : list binder) e
         (tys : A → vec type (length argsb)) ty
         T `{!CopyC T, !SendC T} :
@@ -206,7 +236,7 @@ Section typing.
                    ((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 (Rec fb (kb :: argsb) e) (fn E' tys ty).
+    typed_instruction_ty E L T (funrec: fb argsb → kb := e) (fn E' tys ty).
   Proof.
     iIntros (Hc Hbody tid qE) "#HEAP #LFT $ $ $ #HT". iApply wp_value.
     { simpl. rewrite decide_left. done. }

theories/typing/own.v

@@ -3,6 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.lang Require Export new_delete.
+From lrust.lang Require Import memcpy.
 From lrust.typing Require Export type.
 From lrust.typing Require Import uninit type_context programs.
 
@@ -159,8 +160,11 @@ Section typing.
   Proof.
     iIntros (Hsz p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    rewrite ty'.(ty_size_eq). (* This turns out to be the fastest way to apply a lemma below ▷ -- at least if we're fine throwing away the premise even though the result is persistent, which in this case, we are. *)
-    iDestruct "Hown" as ">%". iModIntro. iExists _, _. iFrame "H↦".
+    (* This turns out to be the fastest way to apply a lemma below ▷ -- at
+    least if we're fine throwing away the premise even though the result
+    is persistent, which in this case, we are. *)
+    rewrite ty'.(ty_size_eq). iDestruct "Hown" as ">%". iModIntro.
+    iExists _, _. iFrame "H↦".
     iSplit; first by rewrite Hsz. iIntros "Hown !>".
     iExists _. iSplit; first done. rewrite Hsz. iFrame.
   Qed.
@@ -186,7 +190,7 @@ Section typing.
     iFrame. iApply uninit_own. auto.
   Qed.
 
-  Lemma type_new E L (n : nat) :
+  Lemma type_new {E L} (n : nat) :
     typed_instruction_ty E L [] (new [ #n ]%E) (own n (uninit n)).
   Proof.
     iIntros (tid eq) "#HEAP #LFT $ $ $ _".
@@ -201,11 +205,11 @@ Section typing.
     - by rewrite uninit_sz freeable_sz_full.
   Qed.
 
-  Lemma type_delete E L n ty p :
-    n = ty.(ty_size) →
+  Lemma type_delete {E L} ty n p :
+    ty.(ty_size) = n →
     typed_instruction E L [p ◁ own n ty] (delete [ #n; p])%E (λ _, []).
   Proof.
-    iIntros (-> tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
+    iIntros (<- tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
     iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". rewrite tctx_interp_nil.
@@ -213,6 +217,58 @@ Section typing.
     iApply (wp_delete with "[-]"); try (by auto); [].
     rewrite freeable_sz_full. by iFrame.
   Qed.
+
+  Lemma type_letalloc_1 {E L} ty C T T' (x : string) p e :
+    ty.(ty_size) = 1%nat →
+    Closed [] p → Closed (x :b: []) e →
+    tctx_extract_hasty E L p ty T T' →
+    (∀ v, typed_body E L C ((v ◁ own 1 ty)::T') (subst x v e)) →
+    typed_body E L C T (letalloc: x := p in e).
+  Proof.
+    intros. eapply type_let'.
+    - rewrite /Closed /=. rewrite !andb_True.
+      eauto 10 using is_closed_weaken with set_solver.
+    - apply (type_new 1).
+    - solve_typing.
+    - move=>xv /=.
+      assert (subst x xv (x <- p ;; e)%E = (xv <- p ;; subst x xv e)%E) as ->.
+      { (* TODO : simpl_subst should be able to do this. *)
+        unfold subst=>/=. repeat f_equal.
+        - by rewrite bool_decide_true.
+        - eapply is_closed_subst. done. set_solver. }
+      eapply type_let'.
+      + apply subst_is_closed; last done. apply is_closed_of_val.
+      + by apply (type_assign ty (own 1 (uninit 1))), write_own.
+      + solve_typing.
+      + move=>//=.
+  Qed.
+
+  Lemma type_letalloc_n {E L} ty ty1 ty2 C T T' (x : string) p e :
+    Closed [] p → Closed (x :b: []) e →
+    typed_read E L ty1 ty ty2 →
+    tctx_extract_hasty E L p ty1 T T' →
+    (∀ v, typed_body E L C ((v ◁ own (ty.(ty_size)) ty)::(p ◁ ty2)::T') (subst x v e)) →
+    typed_body E L C T (letalloc: x :={ty.(ty_size)} !p in e).
+  Proof.
+    intros. eapply type_let'.
+    - rewrite /Closed /=. rewrite !andb_True.
+      eauto 100 using is_closed_weaken with set_solver.
+    - apply type_new.
+    - solve_typing.
+    - move=>xv /=.
+      assert (subst x xv (x <-{ty.(ty_size)} !p ;; e)%E =
+              (xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.
+      { (* TODO : simpl_subst should be able to do this. *)
+        unfold subst=>/=. repeat f_equal.
+        - eapply (is_closed_subst []). done. set_solver.
+        - by rewrite bool_decide_true.
+        - eapply is_closed_subst. done. set_solver. }
+      eapply type_let'.
+      + apply subst_is_closed; last done. apply is_closed_of_val.
+      + eapply type_memcpy; try done. apply write_own, symmetry, uninit_sz.
+      + solve_typing.
+      + move=>//=.
+  Qed.
 End typing.
 
 Hint Resolve own_mono' own_proper' : lrust_typing.

theories/typing/product.v

@@ -245,6 +245,6 @@ Section typing.
 End typing.
 
 
-Hint Resolve product_mono' product_proper' : lrust_type_scope.
-Hint Constructors Forall2 : lrust_type_scope.
-Hint Resolve product2_mono' product2_proper' | 100 : lrust_type_scope.
+Hint Resolve product_mono' product_proper' : lrust_typing.
+Hint Constructors Forall2 : lrust_typing.
+Hint Resolve product2_mono' product2_proper' | 100 : lrust_typing.

theories/typing/sum.v

@@ -235,7 +235,7 @@ End sum.
 (* Σ is commonly used for the current functor. So it cannot be defined
    as Π for products. We stick to the following form. *)
 Notation "Σ[ ty1 ; .. ; tyn ]" :=
-  (sum (cons ty1 (..(cons tyn nil)..))) : lrust_type_scope.
+  (sum (cons ty1 (..(cons tyn nil)..))) : lrust_typing.
 
-Hint Resolve sum_mono' sum_proper' : lrust_type_scope.
-Hint Constructors Forall2 : lrust_type_scope.
+Hint Resolve sum_mono' sum_proper' : lrust_typing.
+Hint Constructors Forall2 : lrust_typing.

theories/typing/type_context.v

@@ -321,10 +321,10 @@ Section type_context.
   Qed.
 End type_context.
 
-Hint Resolve tctx_extract_hasty_here_copy : lrust_tctx_scope.
-Hint Resolve tctx_extract_hasty_here | 50 : lrust_tctx_scope.
-Hint Resolve tctx_extract_hasty_cons | 100 : lrust_tctx_scope.
-Hint Extern 1 (Copy _) => typeclasses eauto : lrust_tctx_scope.
+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_blocked_here tctx_extract_blocked_cons
              tctx_extract_ctx_nil tctx_extract_ctx_hasty
-             tctx_extract_ctx_blocked tctx_extract_ctx_incl : lrust_tctx_scope.
+             tctx_extract_ctx_blocked tctx_extract_ctx_incl : lrust_typing.