Merge pull request #575 from FStarLang/_nik_while_decreases_examples

Fix lex orderings in pulse decreases clauses + examples

Author: gebner

lib/pulse/lib/Pulse.Lib.InsertionSort.fst

@@ -158,6 +158,7 @@ ensures exists* s'. (a |-> s') **
         sorted (Seq.slice (value_of a) 0 (SZ.v !j)) /\
         permutation s (value_of a)
       )
+    decreases (SZ.v len - SZ.v !j)
   {
     pts_to_len a;
     let vj = !j;
@@ -173,13 +174,14 @@ ensures exists* s'. (a |-> s') **
       invariant live done
       invariant exists* (s':Seq.seq t { inner_invariant ss s' key (!i) vj (!done)}).
           a |-> s'
+      decreases (SZ.v !i)
     {
       let vi = !i;
       with s0. assert (a |-> s0);
       a.(SZ.(vi +^ 1sz)) <- a.(vi);
       with s1. assert (a |-> s1);
       step_inner_invariant ss s0 s1 key vi vj;
-      if (vi = 0sz) { done := true }
+      if (vi = 0sz) { done := true; break }
       else { i := SZ.(vi -^ 1sz); }
     };
     with s0. assert (a |-> s0);

lib/pulse/lib/Pulse.Lib.LinkedList.fst

@@ -47,6 +47,15 @@ let rec is_list #t ([@@@mkey]x:llist t) (l:list t)
         pts_to v { head; tail } **
         is_list tail tl
 
+ghost
+fn list_of (#t:Type) (x:llist t) (#y:list t)
+requires is_list x y
+returns z:erased (list t)
+ensures is_list x y ** rewrites_to z (hide y)
+{
+  hide y
+}
+
 let is_list_cases #t ([@@@mkey]x:llist t) (l:list t)
   : Tot slprop
   = match x with
@@ -339,8 +348,6 @@ fn move_next (#t:Type) (x:llist t)
     node.tail
 }
 
-
-
 fn length_iter (#t:Type) (x: llist t)
     preserves is_list x 'l
     returns n:nat
@@ -353,7 +360,7 @@ fn length_iter (#t:Type) (x: llist t)
     let v = Pulse.Lib.Reference.(!cur); 
     Some? v
   )
-  invariant
+  invariant 
   exists* (n:int) ll suffix.
     pts_to ctr n **
     pts_to cur ll **
@@ -365,6 +372,8 @@ fn length_iter (#t:Type) (x: llist t)
     (* ^ Having the bounded_int nat instance in BoundedIntegers means we try to
     to check the subtraction as a nat, which fails without the extra condition.
     We can also just write `n + len suff = len 'l`. *)
+    //Also below, the bounded integer stuff leads to problems
+  decreases  (List.Tot.length 'l `Prims.op_Subtraction` value_of ctr)
   {
     with _n _ll suffix. _;
     let n = Pulse.Lib.Reference.(!ctr);
@@ -509,6 +518,7 @@ fn append_iter (#t:Type) (x y:llist t)
       is_list ll sfx **
       (forall* sfx'. is_list ll sfx' @==> is_list x (pfx @ sfx')) **
       pure (pfx @ sfx == 'l1 /\ Cons? sfx)
+    decreases reveal (list_of (value_of cur))
   {
     with ll pfx sfx. _;
     some_iff_cons ll;
@@ -580,6 +590,7 @@ fn split (#t:Type0) (x:llist t) (n:U32.t) (#xl:erased (list t))
          Some? ll /\
          pfx@sfx == xl
       )
+    decreases reveal (list_of (value_of cur))
   {
     with i ll pfx sfx. _;
     let next = move_next_forall Pulse.Lib.Reference.(!cur);
@@ -660,6 +671,7 @@ fn reverse (#t:Type0) (x:llist t)
     is_list p rev_pfx **
     is_list c suffix **
     pure (List.Tot.rev rev_pfx @ suffix == 'l)
+  decreases reveal (list_of (value_of cur))
   {
     with _p _c _rev_pfx _suffix. _;
     let p = Pulse.Lib.Reference.(!prev);

share/pulse/examples/WhileDecreases.fst

@@ -0,0 +1,59 @@
+module WhileDecreases
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+fn test (x:ref nat)
+requires live x
+ensures x |-> (0<:nat)
+{
+  while (!x > 0)
+  invariant live x
+  decreases (!x)
+  {
+    x := !x - 1;
+  }
+}
+
+fn test2 (x:ref nat)
+requires live x
+ensures x |-> (0<:nat)
+{
+  while (!x > 0)
+  invariant exists* y. pts_to x y
+  decreases (!x)
+  {
+    x := !x - 1;
+  }
+}
+
+fn test3 (x:ref nat)
+requires live x
+ensures x |-> (0<:nat)
+{
+  while (!x > 0)
+  invariant exists* y. pts_to x y
+  decreases reveal (value_of x)
+  {
+    x := !x - 1;
+  }
+}
+
+let rec lex_rec (x y:nat)
+: Tot unit (decreases %[x;y])
+= if x = 0 && y = 0 then ()
+  else if x > 0 then lex_rec (x - 1) y
+  else lex_rec x (y - 1)
+
+fn lex (x y:ref nat)
+requires live x ** live y
+ensures x |-> (0<:nat) ** y |-> (0<:nat)
+{
+  while (!x > 0 || !y > 0)
+  invariant live x
+  invariant live y
+  decreases %[(!x); (!y)]
+  {
+    if (!x = 0) { y := !y - 1; }
+    else { x := !x - 1; }
+  }
+}

src/checker/Pulse.Checker.While.fst

@@ -112,8 +112,41 @@ it directly calls this checker and pass the post as the loop_ensures argument he
 
 *)
 
-#push-options "--fuel 0 --ifuel 0 --z3rlimit_factor 64"
+#push-options "--fuel 0 --ifuel 0 --z3rlimit_factor 72"
 module RT = FStar.Reflection.Typing
+
+#push-options "--fuel 1 --ifuel 1"
+let rec compute_meas_infos (g:env) (pre:term) (ms: list term)
+  : T.Tac (list (term & term & universe))
+  = match ms with
+    | [] -> []
+    | m :: rest ->
+      let m' = purify_term g { ctxt_now = pre; ctxt_old = Some pre } m in
+      let (| _, _, ty, (| u, _ |), _ |) = compute_term_type_and_u g m' in
+      (m, ty, u) :: compute_meas_infos g pre rest
+
+let rec build_tuple_info (infos: list (term & term & universe))
+  : T.Tac (term & term & universe & (term -> term -> term))
+  = match infos with
+    | [(m, ty, u)] -> (m, ty, u, mk_precedes u ty)
+    | (m, ty, u) :: rest ->
+      let (m_rest, ty_rest, u_rest, mk_dec_rest) = build_tuple_info rest in
+      let ty_tup = mk_tuple2 u u_rest ty ty_rest in
+      let m_tup = mk_mktuple2 u u_rest ty ty_rest m m_rest in
+      let mk_dec_tup (new_m: term) (old_m: term) : term =
+        let new_hd = mk_fst u u_rest ty ty_rest new_m in
+        let old_hd = mk_fst u u_rest ty ty_rest old_m in
+        let new_tl = mk_snd u u_rest ty ty_rest new_m in
+        let old_tl = mk_snd u u_rest ty ty_rest old_m in
+        let precedes_hd = mk_precedes u ty new_hd old_hd in
+        let eq_hd = mk_eq2 u ty new_hd old_hd in
+        let rest_dec = mk_dec_rest new_tl old_tl in
+        tm_l_or precedes_hd (tm_l_and eq_hd rest_dec)
+      in
+      (m_tup, ty_tup, u, mk_dec_tup)
+    | _ -> (unit_const, tm_unit, u0, mk_precedes u0 tm_unit)
+#pop-options
+
 let check_while
   (g:env)
   (pre:term)
@@ -156,20 +189,27 @@ let check_while
     if loop_requires `eq_tm` tm_l_true then inv else
     (inv `tm_star` tm_pure (mk_loop_requires_marker loop_requires)) in
   let x_meas: nvar = mk_ppname_no_range "meas", fresh g in
-  let u_meas, ty_meas, meas, is_tot =
+  let u_meas, ty_meas, meas_val, is_tot, mk_dec =
     match meas with
-    | None -> u0, tm_unit, unit_const, false
-    | Some meas ->
+    | [] -> u0, tm_unit, unit_const, false, mk_precedes u0 tm_unit
+    | [meas] ->
       let meas' = purify_term g { ctxt_now = pre; ctxt_old = Some pre } meas in
       let (| _, _, ty, (| u, _ |), _ |) = compute_term_type_and_u g meas' in
-      u, ty, meas, true
+      u, ty, meas, true, mk_precedes u ty
+    | _ ->
+      let meas_infos = compute_meas_infos g pre meas in
+      let (meas_val, _ty_approx, _u_approx, mk_dec) = build_tuple_info meas_infos in
+      let meas_val' = purify_term g { ctxt_now = pre; ctxt_old = Some pre } meas_val in
+      let (| _, _, ty, (| u, _ |), _ |) = compute_term_type_and_u g meas_val' in
+      u, ty, meas_val, true, mk_dec
   in
+  let dec_formula = mk_dec (tm_bvar {bv_index=0;bv_ppname=fst x_meas}) (term_of_nvar x_meas) in
   let inv_range = term_range inv in
   let g_meas = push_binding g (snd x_meas) (fst x_meas) ty_meas in
   let inv = dfst <|
     purify_and_check_spec (push_context "invariant" inv_range g_meas)
       { ctxt_now = pre; ctxt_old = Some pre }
-      (inv `tm_star` tm_pure (mk_eq2 u_meas ty_meas (term_of_nvar x_meas) meas))
+      (inv `tm_star` tm_pure (mk_eq2 u_meas ty_meas (term_of_nvar x_meas) meas_val))
   in
   let loop_pre0 = tm_exists_sl u_meas (as_binder ty_meas) (close_term inv (snd x_meas)) in
   let (| g0, remaining, k |) = Pulse.Checker.Prover.prove t.range g pre loop_pre0 false in
@@ -242,7 +282,7 @@ let check_while
     (| t, c, typ |) in
 
   let body_pre_open = post_cond.post in
-  let body_post_typing : tot_typing g2 (comp_post (comp_while_body u_meas ty_meas is_tot x_meas inv body_pre_open)) tm_slprop = RU.magic () in
+  let body_post_typing : tot_typing g2 (comp_post (comp_while_body u_meas ty_meas is_tot dec_formula x_meas inv body_pre_open)) tm_slprop = RU.magic () in
   let body_ph : post_hint_for_env g2 = inv_as_post_hint body_post_typing in
   assert body_ph.ret_ty == tm_unit;
   let x = fresh g2 in
@@ -258,21 +298,21 @@ let check_while
   let (| cond, comp_cond, cond_typing |) = r_cond in
   let (| body, comp_body, body_typing |) = apply_checker_result_k r_body ppname_default in
   assert (comp_cond == (comp_while_cond inv body_pre_open));
-  assert (comp_post comp_body == comp_post (comp_while_body u_meas ty_meas is_tot x_meas inv body_pre_open));
-  assert (comp_pre comp_body == comp_pre (comp_while_body u_meas ty_meas is_tot x_meas inv body_pre_open));
-  assert (comp_u comp_body == comp_u (comp_while_body u_meas ty_meas is_tot x_meas inv body_pre_open));
-  assert (comp_res comp_body == comp_res (comp_while_body u_meas ty_meas is_tot x_meas inv body_pre_open));
-  assert (comp_body == comp_while_body u_meas ty_meas is_tot x_meas inv body_pre_open);
+  assert (comp_post comp_body == comp_post (comp_while_body u_meas ty_meas is_tot dec_formula x_meas inv body_pre_open));
+  assert (comp_pre comp_body == comp_pre (comp_while_body u_meas ty_meas is_tot dec_formula x_meas inv body_pre_open));
+  assert (comp_u comp_body == comp_u (comp_while_body u_meas ty_meas is_tot dec_formula x_meas inv body_pre_open));
+  assert (comp_res comp_body == comp_res (comp_while_body u_meas ty_meas is_tot dec_formula x_meas inv body_pre_open));
+  assert (comp_body == comp_while_body u_meas ty_meas is_tot dec_formula x_meas inv body_pre_open);
   let inv_typing2 : tot_typing g2 inv tm_slprop = RU.magic () in
 
-  let while = wtag (Some STT) (Tm_While { invariant = inv; loop_requires = tm_unknown; meas = None; condition = cond; body }) in
+  let while = wtag (Some STT) (Tm_While { invariant = inv; loop_requires = tm_unknown; meas = []; condition = cond; body }) in
   let typ_meas: universe_of g1' ty_meas u_meas = RU.magic () in
   assume ~(snd x_meas `Set.mem` freevars_st cond);
   assume ~(snd x_meas `Set.mem` freevars_st body);
   let d: st_typing g1' while (comp_while u_meas ty_meas x_meas inv body_pre_open) =
     let h = RU.magic () in
     T_While g1' inv body_pre_open cond body
-      u_meas ty_meas typ_meas is_tot
+      u_meas ty_meas typ_meas is_tot dec_formula
       x_meas g2
       inv_typing2 h cond_typing body_typing
     in

src/checker/Pulse.Reflection.Util.fst

@@ -105,6 +105,16 @@ let mk_snd (u1 u2:R.universe) (a1 a2 e:R.term) : R.term =
   let t = pack_ln (Tv_App t (a2, Q_Implicit)) in
   pack_ln (Tv_App t (e, Q_Explicit))
 
+let mktuple2_lid = ["FStar"; "Pervasives"; "Native"; "Mktuple2"]
+
+let mk_mktuple2 (u1 u2:R.universe) (a1 a2 v1 v2:R.term) : R.term =
+  let open R in
+  let t = pack_ln (Tv_UInst (pack_fv mktuple2_lid) [u1; u2]) in
+  let t = pack_ln (Tv_App t (a1, Q_Implicit)) in
+  let t = pack_ln (Tv_App t (a2, Q_Implicit)) in
+  let t = pack_ln (Tv_App t (v1, Q_Explicit)) in
+  pack_ln (Tv_App t (v2, Q_Explicit))
+
 let true_tm = R.pack_ln (R.Tv_Const (R.C_True))
 let false_tm = R.pack_ln (R.Tv_Const (R.C_False))
 

src/checker/Pulse.Syntax.Base.fst

@@ -230,7 +230,7 @@ let rec eq_st_term (t1 t2:st_term)
       Tm_While { invariant=inv2; loop_requires=cr2; meas=d2; condition=cond2; body=body2 } ->
       eq_tm inv1 inv2 &&
       eq_tm cr1 cr2 &&
-      eq_tm_opt d1 d2 &&
+      eq_tm_list d1 d2 &&
       eq_st_term cond1 cond2 &&
       eq_st_term body1 body2
 

src/checker/Pulse.Syntax.Base.fsti

@@ -264,7 +264,7 @@ type st_term' =
    | Tm_While {
       invariant:term;
       loop_requires:term;
-      meas:option term;
+      meas:list term;
       condition:st_term;
       body:st_term;
     }

src/checker/Pulse.Syntax.Naming.fst

@@ -179,7 +179,7 @@ let rec close_open_inverse_st'  (t:st_term)
     | Tm_While { invariant; loop_requires; meas; condition; body } ->
       close_open_inverse' invariant x i;
       close_open_inverse' loop_requires x i;
-      (match meas with | Some d -> close_open_inverse' d x i | None -> ());
+      close_open_inverse_list' meas x i;
       close_open_inverse_st' condition x i;
       close_open_inverse_st' body x i
 

src/checker/Pulse.Syntax.Naming.fsti

@@ -127,7 +127,7 @@ let rec freevars_st (t:st_term)
     | Tm_While { invariant; loop_requires; meas; condition; body } ->
       freevars invariant ++
       freevars loop_requires ++
-      freevars_term_opt meas ++
+      freevars_list meas ++
       freevars_st condition ++
       freevars_st body
 
@@ -315,7 +315,7 @@ let rec ln_st' (t:st_term) (i:int)
     | Tm_While { invariant; loop_requires; meas; condition; body } ->
       ln' invariant i &&
       ln' loop_requires i &&
-      ln_opt' ln' meas i &&
+      ln_list' meas i &&
       ln_st' condition i &&
       ln_st' body i
 
@@ -564,7 +564,7 @@ let rec subst_st_term (t:st_term) (ss:subst)
     | Tm_While { invariant; loop_requires; meas; condition; body } ->
       Tm_While { invariant = subst_term invariant ss;
                     loop_requires = subst_term loop_requires ss;
-                    meas = subst_term_opt meas ss;
+                    meas = subst_term_list meas ss;
                     condition = subst_st_term condition ss;
                     body = subst_st_term body ss }
 

src/checker/Pulse.Syntax.Printer.fst

@@ -357,7 +357,7 @@ let rec st_term_to_string' (level:string) (t:st_term)
         level
         (term_to_string invariant)
         level
-        (match meas with | Some d -> sprintf "decreases %s\n%s" (term_to_string d) level | None -> "")
+        (match meas with | [] -> "" | [d] -> sprintf "decreases %s\n%s" (term_to_string d) level | ds -> sprintf "decreases %%[%s]\n%s" (term_list_to_string "; " ds) level)
         (indent level)
         (st_term_to_string' (indent level) body)
         level