Pulse: introduce let rewrite

pulse/src/ml/pulseparser.mly

@@ -294,6 +294,10 @@ optional_norewrite:
   | NOREWRITE { true }
   | { false }
 
+optional_rw:
+  | REWRITE { true }
+  | { false }
+
 while_invariant1:
   | INVARIANT v=pulseSLProp
     { PulseSyntaxExtension_Sugar.LoopInvariant v }
@@ -320,8 +324,8 @@ pulseStmtNoSeq:
     }
   | tm=tmEq args=list(termPulseLambda)
     { PulseSyntaxExtension_Sugar.mk_expr tm args }
-  | norw=optional_norewrite LET q=option(mutOrRefQualifier) p=pulsePattern typOpt=option(preceded(COLON, appTerm)) init=letMutInit
-    { PulseSyntaxExtension_Sugar.mk_let_binding norw q p typOpt init }
+  | norw=optional_norewrite LET rw=optional_rw q=option(mutOrRefQualifier) p=pulsePattern typOpt=option(preceded(COLON, appTerm)) init=letMutInit
+    { PulseSyntaxExtension_Sugar.mk_let_binding norw rw q p typOpt init }
   | s=pulseBindableTerm
     { s }
   | WHILE LPAREN tm=pulseStmt RPAREN inv=while_invariant LBRACE body=pulseStmt RBRACE
@@ -361,7 +365,7 @@ pulseStmtNoSeq:
     {
       let id, fndefn = f in
       let pat = mk_pattern (PatVar (id, None, [])) (rr $loc) in
-      PulseSyntaxExtension_Sugar.mk_let_binding false None pat None (Lambda_initializer fndefn)
+      PulseSyntaxExtension_Sugar.mk_let_binding false false None pat None (Lambda_initializer fndefn)
     }
   | LBRACE s=pulseStmt RBRACE
     { PulseSyntaxExtension_Sugar.mk_block s }

pulse/src/syntax_extension/PulseSyntaxExtension.Desugar.fst

@@ -516,7 +516,21 @@ let rec desugar_stmt' (env:env_t) (s:Sugar.stmt)
         if Cons? attrs then
           fail "Binder attributes are not allowed." (pos (List.hd attrs))
         else return ();!
-        desugar_bind env lb s2 s.range
+        if lb.rw
+        then (
+          (* 'let rewrite x = e' desugars to 'let x = e; assert rewrites_to x e' *)
+          match lb.pat.pat, lb.qualifier, lb.init with
+          | A.PatVar (id, _, _), None, Default_initializer (Some e, []) ->
+            let xtm = A.mk_term (A.Var (Ident.id_as_lid id)) lb.pat.prange A.Expr in
+            let rwt = A.mk_term (A.Var (Ident.lid_of_str "Pulse.Lib.Core.rewrites_to")) lb.pat.prange A.Expr in
+            let prop = A.mk_term (A.App (A.mk_term (A.App (rwt, xtm, A.Nothing)) lb.pat.prange A.Expr, e, A.Nothing)) lb.pat.prange A.Expr in
+            let assert_stmt = { mk_stmt (ProofHintWithBinders { hint_type = ASSERT prop; binders = [] }) s1range with source = false } in
+            let s2' = { mk_stmt (Sequence { s1 = assert_stmt; s2 }) s.range with source = false } in
+            desugar_bind env { lb with rw = false } s2' s.range
+          | _ ->
+            fail "'let rewrite' requires a simple variable binding with a pure initializer" lb.pat.prange
+        )
+        else desugar_bind env lb s2 s.range
       | _ ->
         (* a single-branch pattern match *)
         let id = Ident.id_of_text "_letpattern" in
@@ -532,6 +546,7 @@ let rec desugar_stmt' (env:env_t) (s:Sugar.stmt)
         in
         let lb' =
           { norw = lb.norw;
+            rw = false;
             qualifier = lb.qualifier;
             pat = A.mk_pattern (A.PatVar (id, None, [])) lb.pat.prange;
             typ = lb.typ;

pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst

@@ -132,6 +132,7 @@ type stmt' =
 
   | LetBinding {
       norw:bool; (* add norewrite to the branch if this desugars to a match. *)
+      rw:bool; (* 'let rw x = e': follow the binding with 'assert rewrites_to x e' *)
       qualifier: option mut_or_ref;
       pat:A.pattern;
       typ:option A.term;
@@ -479,8 +480,9 @@ and eq_stmt' (s1 s2:stmt') : ML bool =
   | Expr e1, Expr e2 -> AD.eq_term e1.e e2.e && forall2 eq_lambda e1.args e2.args
   | ArrayAssignment { arr=a1; index=i1; value=v1 }, ArrayAssignment { arr=a2; index=i2; value=v2 } ->
     AD.eq_term a1 a2 && AD.eq_term i1 i2 && AD.eq_term v1 v2
-  | LetBinding { norw=norw1; qualifier=q1; pat=pat1; typ=t1; init=init1 }, LetBinding { norw=norw2; qualifier=q2; pat=pat2; typ=t2; init=init2 } ->
+  | LetBinding { norw=norw1; rw=rw1; qualifier=q1; pat=pat1; typ=t1; init=init1 }, LetBinding { norw=norw2; rw=rw2; qualifier=q2; pat=pat2; typ=t2; init=init2 } ->
     norw1 = norw2 &&
+    rw1 = rw2 &&
     eq_opt eq_mut_or_ref q1 q2 &&
     AD.eq_pattern pat1 pat2 &&
     eq_opt AD.eq_term t1 t2 &&
@@ -714,7 +716,7 @@ let add_decorations d ds =
 let mk_expr e args = Expr { e; args }
 let mk_unit rng = Expr { e = A.mk_term (A.Const FStarC.Const.Const_unit) rng A.Expr; args = [] }
 let mk_array_assignment arr index value = ArrayAssignment { arr; index; value }
-let mk_let_binding norw qualifier pat typ init = LetBinding { norw; qualifier; pat; typ; init }
+let mk_let_binding norw rw qualifier pat typ init = LetBinding { norw; rw; qualifier; pat; typ; init }
 let mk_block stmt = Block { stmt }
 let mk_if head join_slprop then_ else_opt = If { head; join_slprop; then_; else_opt }
 let mk_match head returns_annot branches = Match { head; returns_annot; branches }

pulse/test/RwLet.fst

@@ -0,0 +1,36 @@
+module RwLet
+open Pulse
+#lang-pulse
+
+(* Aliasing a reference with a plain 'let' breaks the proof: Pulse does not
+   know r' and r are interchangeable, so 'r' |-> v' fails to match the
+   context 'r |-> v'. *)
+[@@expect_failure [228]]
+fn alias_plain (r: ref int) (#v:erased int)
+  requires r |-> v
+  ensures r |-> v
+{
+  let r' : ref int = r;
+  assert (r' |-> v);
+}
+
+(* 'let rewrite' fixes it: it adds 'assert rewrites_to r' r', so the matcher
+   replaces r' by r and the proof goes through. *)
+fn alias_rewrite (r: ref int) (#v:erased int)
+  requires r |-> v
+  ensures r |-> v
+{
+  let rewrite r' : ref int = r;
+  assert (r' |-> v);
+}
+
+(* It works in the other direction too: rewriting lets us present the
+   resource under the alias and still satisfy a postcondition stated with
+   the original name. *)
+fn alias_rewrite_post (r: ref int)
+  requires r |-> 0
+  ensures r |-> 0
+{
+  let rewrite r' : ref int = r;
+  r' := 0;
+}