finish 717baeab and convert prefixRec to lemma functions

examples/verifythis_PrefixSumRec.mlw

@@ -12,6 +12,7 @@ module PrefixSumRec
    use import int.ComputerDivision
    use import int.Power
 
+   use import map.Map as M
    use import array.Array
    use import array.ArraySum
 
@@ -64,21 +65,29 @@ module PrefixSumRec
   (** frame lemma for "phase1" on fourth argument.
      needed to prove both upsweep, downsweep and compute_sums
    *)
-  lemma phase1_frame:
-    forall left right:int, a0 a a' : array int.
-    (forall i:int. left-(right-left) < i < right ->
-       a[i] = a'[i]) ->
-    phase1 left right a0 a -> phase1 left right a0 a'
-
+  let rec lemma phase1_frame (left right:int) (a0 a a' : array int) : unit variant { right-left }
+    requires { forall i:int. left-(right-left) < i < right ->
+               a[i] = a'[i]}
+    requires { phase1 left right a0 a }
+    ensures { phase1 left right a0 a' } =
+    if right > left + 1 then begin
+       phase1_frame (go_left left right) left a0 a a';
+       phase1_frame (go_right left right) right a0 a a'
+    end
 
   (** frame lemma for "phase1" on third argument.
      needed to prove upsweep and compute_sums
    *)
-  lemma phase1_frame2:
-    forall left right:int, a0 a0' a : array int.
-    (forall i:int. left-(right-left) < i < right ->
-       a0[i] = a0'[i]) ->
-    phase1 left right a0 a -> phase1 left right a0' a
+  let rec lemma phase1_frame2 (left right:int) (a0 a0' a : array int) : unit variant { right-left }
+    requires { forall i:int. left-(right-left) < i < right ->
+               a0[i] = a0'[i]}
+    requires { phase1 left right a0 a }
+    ensures { phase1 left right a0' a } =
+    if right > left + 1 then begin
+       phase1_frame2 (go_left left right) left a0 a0' a;
+       phase1_frame2 (go_right left right) right a0 a0' a
+    end
+
 
 (** {2 The upsweep phase}
 
@@ -142,6 +151,7 @@ module PrefixSumRec
     assert { phase1 (go_right left right) right a0 (at a 'Init) };
     assert { phase1 (go_right left right) right a0 a };
     downsweep (left - div space 2) left a0 a;
+    assert { phase1 (go_right left right) right a0 a };
     downsweep (right - div space 2) right a0 a;
     assert { partial_sum (left - div space 2) left a0 a };
     assert { partial_sum (right - div space 2) right a0 a }

src/whyml/mlw_wp.ml

@@ -849,23 +849,25 @@ and wp_abstract env c_eff c_q c_xq q xq =
   in
   backstep proceed c_q c_xq
 
-and wp_fun_defn env { fun_ps = ps ; fun_lambda = l } =
-  let lab = fresh_mark () and c = l.l_spec in
+and wp_fun_regs ps l = (* regions to refresh at the top of function WP *)
   let add_arg = let seen = ref Sreg.empty in fun sbs pv ->
     (* we only need to "havoc" the regions that occur twice in [l.l_args].
        If a region in an argument is shared with the context, then is it
        already frozen in [ps.ps_subst]. If a region in an argument is not
        shared at all, the last [wp_forall] over [args] will be enough. *)
-    let rec down sbs ity = match ity.ity_node with
-      | Ityapp (_,_,rl) ->
-          let add_reg sbs r =
-            if Sreg.mem r !seen then reg_match sbs r r else
-            (seen := Sreg.add r !seen; down sbs r.reg_ity) in
-          ity_fold down (List.fold_left add_reg sbs rl) ity
-      | _ -> ity_fold down sbs ity in
+    let rec down sbs ity =
+      let rl = match ity.ity_node with
+        | Ityapp (_,_,rl) -> rl | _ -> [] in
+      ity_fold down (List.fold_left add_reg sbs rl) ity
+    and add_reg sbs r =
+      if Sreg.mem r !seen then reg_match sbs r r else
+      (seen := Sreg.add r !seen; down sbs r.reg_ity) in
     down sbs pv.pv_ity in
-  let subst = List.fold_left add_arg ps.ps_subst l.l_args in
-  let regs = Mreg.map (fun _ -> ()) subst.ity_subst_reg in
+  let sbs = List.fold_left add_arg ps.ps_subst l.l_args in
+  Mreg.map (fun _ -> ()) sbs.ity_subst_reg
+
+and wp_fun_defn env { fun_ps = ps ; fun_lambda = l } =
+  let lab = fresh_mark () and c = l.l_spec in
   let args = List.map (fun pv -> pv.pv_vs) l.l_args in
   let env =
     if c.c_letrec = 0 || c.c_variant = [] then env else
@@ -878,7 +880,7 @@ and wp_fun_defn env { fun_ps = ps ; fun_lambda = l } =
   let conv p = old_mark lab (wp_expl expl_xpost p) in
   let f = wp_expr env l.l_expr q (Mexn.map conv c.c_xpost) in
   let f = wp_implies c.c_pre (erase_mark lab f) in
-  wp_forall args (quantify env regs f)
+  wp_forall args (quantify env (wp_fun_regs ps l) f)
 
 and wp_rec_defn env fdl = List.map (wp_fun_defn env) fdl
 
@@ -1966,14 +1968,11 @@ let wp_rec ~wp env kn th fdl =
         Loc.errorm ?loc "lemma functions must return unit";
       let env = mk_env env kn th in
       let lab = fresh_mark () in
-      let add_arg sbs pv = ity_match sbs pv.pv_ity pv.pv_ity in
-      let subst = List.fold_left add_arg ps.ps_subst l.l_args in
-      let regs = Mreg.map (fun _ -> ()) subst.ity_subst_reg in
       let args = List.map (fun pv -> pv.pv_vs) l.l_args in
       let q = old_mark lab spec.c_post in
       let f = wp_expr env e_void q Mexn.empty in
       let f = wp_implies spec.c_pre (erase_mark lab f) in
-      let f = wp_forall args (quantify env regs f) in
+      let f = wp_forall args (quantify env (wp_fun_regs ps l) f) in
       let f = t_forall_close (Mvs.keys f.t_vars) [] f in
       let lkn = Theory.get_known th in
       let f = if Debug.test_flag no_track then f else track_values lkn kn f in