Remove a big assertion using equalities propagation

examples/in_progress/multiprecision/lineardecision.mlw

@@ -1773,6 +1773,7 @@ let prop_ctx (l:context') (g:equality') : (context', equality')
   in
   let rec propagate_e (e:expr')
     requires { expr_bound' e m }
+    ensures { expr_bound' result m }
     ensures { forall y z. y=z -> ctx_holds' l y z -> interp_eq' (e,result) y z }
     variant { e }
     raises { OutOfBounds -> true }
@@ -1791,6 +1792,7 @@ let prop_ctx (l:context') (g:equality') : (context', equality')
   in
   let rec propagate_eq (eq:equality')
     requires { eq_bound' eq m }
+    ensures { eq_bound' result m }
     ensures { forall y z. y=z -> interp_ctx' l eq y z <-> interp_ctx' l result y z }
     raises { OutOfBounds -> true }
     requires { valid_eq' eq }
@@ -1801,6 +1803,7 @@ let prop_ctx (l:context') (g:equality') : (context', equality')
   in
   let rec propagate (acc:context') : context'
     requires { ctx_bound' acc m }
+    ensures { ctx_bound' result m }
     requires { ctx_impl_ctx' l acc }
     ensures { ctx_impl_ctx' l result }
     variant { acc }
@@ -1817,7 +1820,8 @@ let prop_ctx (l:context') (g:equality') : (context', equality')
        Cons h' t'
     end
   in
-  propagate l, propagate_eq g
+  propagate (propagate (propagate l)),
+  propagate_eq (propagate_eq (propagate_eq g))
 
   use LinearDecisionRationalMP as R
 
@@ -1835,7 +1839,7 @@ end
 
 module TestMP
 
-use import LinearDecisionIntMP
+use import EqPropMP
 use import mach.int.UInt64
 use import int.Int
 use import int.Power

examples/in_progress/multiprecision/mp2.mlw

@@ -1976,7 +1976,6 @@ module N
     let limb_zero = Limb.of_int 0 in
     let zero = Int32.of_int 0 in
     let one = Int32.of_int 1 in
-    let minus_one = Int32.(-_) one in
     let msb = Int32.(-) sz one in
     let xp = ref (C.incr x msb) in
     let rp = ref (C.incr r msb) in
@@ -2000,7 +1999,7 @@ module N
       invariant { pelts !xp = pelts x }
       invariant { !high <= radix - power 2 (cnt) }
       label StartLoop in
-      xp.contents <- C.incr !xp minus_one;
+      xp.contents <- C.incr !xp (-1);
       low := C.get !xp;
       let l,h = lsld_ext !low cnt in
       assert { !high + h < radix  };
@@ -2008,7 +2007,7 @@ module N
       value_sub_update_no_change (pelts r) (!rp).offset (r.offset + 1 + p2i !i)
                                  (r.offset + p2i sz) v;
       C.set !rp (Limb.(+) !high h);
-      rp.contents <- C.incr !rp minus_one;
+      rp.contents <- C.incr !rp (-1);
       high := l;
       let ghost k = p2i !i in
       i := Int32.(-) !i one;
@@ -2547,7 +2546,6 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
     let zero = Int32.of_int 0 in
     let one = Int32.of_int 1 in
     let msb = Int32.(-) sz one in
-    let minus_one = Int32.(-_) (Int32.of_int 1) in
     let lx = ref limb_zero in
     let xp = ref (C.incr x msb) in
     let qp = ref (C.incr q msb) in
@@ -2652,8 +2650,8 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
                                           (q.offset + sz)
                       * ry
                       + (!r at StartLoop) }; (* previous invariant is still true *)
-        xp.contents <- C.incr !xp minus_one;
-        qp.contents <- C.incr !qp minus_one;
+        xp.contents <- C.incr !xp (-1);
+        qp.contents <- C.incr !qp (-1);
         value_sub_head (pelts x) (x.offset + int32'int !i) (x.offset + p2i sz);
         value_sub_head (pelts q) (q.offset + int32'int !i) (q.offset + p2i sz);
         assert { l + radix * h = mult * !lx }; (*lsld_ext postcondition *)
@@ -2768,8 +2766,8 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
         value_sub_update_no_change (pelts q) (!qp).offset (q.offset + 1 + p2i !i)
                                    (q.offset + p2i sz) qu;
         C.set !qp qu;
-        xp.contents <- C.incr !xp minus_one;
-        qp.contents <- C.incr !qp minus_one;
+        xp.contents <- C.incr !xp (-1);
+        qp.contents <- C.incr !qp (-1);
         i := Int32.(-) !i one;
         value_sub_head (pelts x) (x.offset + k) (x.offset + p2i sz);
         value_sub_head (pelts q) (q.offset + k) (q.offset + p2i sz);
@@ -2815,9 +2813,10 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
     requires { dh >= div radix 2 }
     requires { reciprocal_3by2 v dh dl }
     requires { um + radix * uh < dl + radix * dh }
-    returns { q, rl, rh -> l2i q * (dl + radix * dh) + l2i rl + radix * l2i rh
-                  = ul + radix * (um + radix * uh) }
-    returns { _q, rl, rh -> 0 <= l2i rl + radix * l2i rh < dl + radix * dh }
+    returns { q, rl, rh -> uint64'int q * dl + radix * q * dh
+                           + uint64'int rl + radix * uint64'int rh
+                  = ul + radix * um + radix * radix * uh }
+    returns { _q, rl, rh -> 0 <= uint64'int rl + radix * uint64'int rh < dl + radix * dh }
   =
     let ghost d = l2i dl + radix * l2i dh in
     let ghost u = l2i ul + radix * (l2i um + radix * l2i uh) in
@@ -3617,7 +3616,6 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
     let two = Int32.of_int 2 in
     let limb_zero = Limb.of_int 0 in
     let zero = Int32.of_int 0 in
-    let minus_one = Int32.(-_) (Int32.of_int 1) in
     let uone = Limb.of_int 1 in
     let xp = ref (C.incr x (Int32.(-) sx two)) in
     let qp = ref (C.incr q (Int32.(-) sx sy)) in
@@ -3857,7 +3855,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
       let ghost k = int32'int !i in
       i := Int32.(-) !i one;
       let ghost s = int32'int sy + int32'int !i - 1 in
-      xp.contents <- C.incr !xp minus_one;
+      xp.contents <- C.incr !xp (-1);
       let xd = C.incr !xp mdn in
       let nx0 = C.get_ofs !xp one in
       if [@ex:unlikely] (Limb.(=) !x1 dh && Limb.(=) nx0 dl)
@@ -4026,7 +4024,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
                };
         value_sub_concat (pelts x) x.offset xd.offset (x.offset + s);
         x1 := C.get_ofs !xp one;
-        qp.contents <- C.incr !qp minus_one;
+        qp.contents <- C.incr !qp (-1);
         value_sub_update_no_change (pelts q) (!qp).offset
                             ((!qp).offset + 1)
                             ((!qp).offset + p2i sx - p2i sy - p2i !i)
@@ -4939,7 +4937,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
                    = value (xd at SubProd) sy
                      + power radix sy * (!x1 at StartLoop)
                      - !ql * vy };
-          qp.contents <- C.incr !qp minus_one;
+          qp.contents <- C.incr !qp (-1);
           value_sub_update_no_change (pelts q) (!qp).offset
                             ((!qp).offset + 1)
                             ((!qp).offset + p2i sx - p2i sy - p2i !i)
@@ -5241,7 +5239,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
                };
         end
         else begin
-          qp.contents <- C.incr !qp minus_one;
+          qp.contents <- C.incr !qp (-1);
           value_sub_update_no_change (pelts q) (!qp).offset
                             ((!qp).offset + 1)
                             ((!qp).offset + p2i sx - p2i sy - p2i !i)
@@ -5249,16 +5247,50 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
           C.set !qp !ql;
           value_sub_head (pelts q) (!qp).offset
             ((!qp).offset + p2i sx - p2i sy - p2i !i);
-          value_sub_tail (pelts x) x.offset (x.offset + p2i sy + p2i !i - 1);
+          assert { value !qp (sx - sy - !i) * vy
+                    = !ql * vy + radix *
+                          (value_sub (pelts q) ((!qp).offset + 1)
+                                    ((!qp).offset + sx - sy - !i) * vy) }; (*nonlinear*)
+          assert { value_sub (pelts q) ((!qp).offset + 1)
+                                    ((!qp).offset + sx - sy - !i) * vy
+                   =  (value !qp (sx - sy - !i) * vy at StartLoop) }; (*nonlinear*)
+          value_tail x (sy + !i - 1);
           value_sub_concat (pelts x) x.offset xd.offset (x.offset + s);
           (* todo refl *)
+          assert { cy2 = 0 };
+          assert { value x !i = value (x at SubProd) !i };
+          assert { value x s = value x !i + power radix !i * value xd (sy-1)
+                     by xd.offset = x.offset + !i
+                     so x.offset + s = xd.offset + sy - 1
+                     so pelts x = pelts xd
+                     so x.offset + s - xd.offset = sy - 1
+                     so value_sub (pelts x) xd.offset (x.offset + s)
+                        = value xd (sy - 1)
+                     so value x s
+                        = value_sub (pelts x) x.offset xd.offset
+                          + power radix !i * value_sub (pelts x) xd.offset (x.offset + s)
+                        = value x !i
+                          + power radix !i * value xd (sy - 1)}; (*lifted from assertion*)
+          assert { (value !qp (sx - sy - !i) + qh * power radix (sx - sy - !i))
+                   * vy
+                   = value !qp (sx - sy - !i) * vy
+                     + qh * vy * power radix (sx - sy - !i)  }; (*nonlinear*)
+          assert { ((value !qp (sx - sy - !i) + qh * power radix (sx - sy - !i))
+                   * vy at StartLoop)
+                   = (value !qp (sx - sy - !i) * vy
+                     + qh * vy * power radix (sx - sy - !i) at StartLoop)  }; (*nonlinear*)
+          assert { value x s = value x (sy + !i - 1) };
+          assert { value (xd at SmallDiv) sy =
+                    vlx + power radix (sy - 2) * xp0
+                    + power radix (sy - 1) * xp1 };  (*nonlinear*)
+          assert { value (x at SubProd) (sy + (!i at StartLoop) - 1) = value (x at SubProd) !i + power radix !i * value (xd at SubProd) sy };
           assert { value (old x) sx =
                   (value !qp (sx - sy - !i)
                    + qh * power radix (sx - sy - !i))
                   * vy * power radix !i
                   + value x (sy + !i - 1)
                   + power radix (sy + !i - 1) * !x1
-                 by
+                 (*by
                     value !qp (sx - sy - !i)
                     = !ql + radix *
                           value_sub (pelts q) ((!qp).offset + 1)
@@ -5450,7 +5482,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
                         * vy * power radix k
                       +  value (x at StartLoop) (sy + k - 1)
                       + power radix (sy + k - 1) * (!x1 at StartLoop)
-                    = value (old x) sx
+                    = value (old x) sx *)
                 };
           value_sub_tail (pelts y) y.offset (y.offset + p2i sy - 1);
           value_sub_tail (pelts y) y.offset (y.offset + p2i sy - 2);
@@ -5639,7 +5671,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
     assert { !xp.offset = x.offset + sy - 2 };
     value_sub_update_no_change (pelts x) (!xp.offset + 1)
                                x.offset (!xp.offset) !x1;
-    C.set_ofs !xp one !x1;
+    C.set_ofs !xp 1 !x1;
     assert { value x (sy - 1) =
              value (x at EndLoop) (sy - 1)
              by pelts x = Map.set (pelts x at EndLoop) (x.offset + sy - 1) !x1 };
@@ -5689,7 +5721,6 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
     let one = Int32.of_int 1 in
     let zero = Int32.of_int 0 in
     let two = Int32.of_int 2 in
-    let minus_one = Int32.(-_) (Int32.of_int 1) in
     let uzero = Limb.of_int 0 in
     let uone = Limb.of_int 1 in
     let xp = ref (C.incr x (Int32.(-) sx two)) in
@@ -5777,7 +5808,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
       invariant { !rl + radix * !rh < dl + radix * dh }
       label StartLoop in
       let ghost k = p2i !i in
-      xp.contents <- C.incr !xp minus_one;
+      xp.contents <- C.incr !xp (-1);
       lx := C.get !xp;
       label Got in
       let (qu, r0, r1) = div3by2_inv !rh !rl !lx dh dl dinv in
@@ -6229,7 +6260,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
                    = value q (sx - sy + adjust) * value y sy
                    + value r sy
                  by value r sy = value nx sy
-                 so value (nx at Div_ns) (sx + adjust) < power radix sx
+                 so value (nx at Div_ns) (sx + adjust) = value x sx < power radix sx
                  so value (nx at Div_ns) (sx + adjust)
                     = value (nx at Div_ns) sx
                  so (_qh = 0

src/transform/reification.ml

@@ -503,6 +503,24 @@ let build_vars_map renv prev =
         raise (Exit "vars not matched"));
   if debug then Format.printf "all vars matched@.";
   let prev, prs =
+    (*let rec aux (ds,prs) i =
+      if i >= renv.fr then ds, prs
+      else
+        let vy = Mterm.find i renv.store in
+        let y = Mvs.find vy subst in
+        let et = t_equ
+                   (t_app fs_func_app [y; t_nat_const i]
+                          t.t_ty)
+                   t in
+        if debug then Format.printf "%a %d = %a@."
+                                    Pretty.print_vs vy i Pretty.print_term t;
+        let pr = create_prsymbol (Ident.id_fresh "y_val") in
+        let d = create_prop_decl Paxiom pr et in
+        aux (d::ds, pr::prs) (i+1)
+    in
+    let ds, prs = aux ([],[]) 0 in
+    let prev = List.fold_left Task.add_decl prev ds in
+    prev,prs in*)
     Mterm.fold
       (fun t (vy,i) (prev,prs) ->
         let y = Mvs.find vy subst in
@@ -512,7 +530,8 @@ let build_vars_map renv prev =
                    t in
         if debug then Format.printf "%a %d = %a@."
                                     Pretty.print_vs vy i Pretty.print_term t;
-        let pr = create_prsymbol (Ident.id_fresh "y_val") in
+        let s = Format.sprintf "y_val%d" i in
+        let pr = create_prsymbol (Ident.id_fresh s) in
         let d = create_prop_decl Paxiom pr et in
         Task.add_decl prev d, pr::prs)
       renv.store (prev,prs) in
@@ -602,12 +621,12 @@ open Expr
 open Ity
 
 exception CannotReduce
-exception Raised of string * string
 
 let append l = List.fold_left (fun acc s -> acc^":"^s) "" l
 
 type value =
   | Vconstr of rsymbol * field list
+  | Vtuple of value list
   | Vint of BigInt.t
   | Vbool of bool
   | Vvoid
@@ -617,12 +636,16 @@ type value =
 
 and field = Fimmutable of value | Fmutable of value ref
 
+exception Raised of xsymbol * value option * string
+
 open Format
 
 let rec print_value fmt = function
   | Vvoid -> fprintf fmt "()"
   | Vbool b -> fprintf fmt "%b" b
   | Vint i -> fprintf fmt "%a" Number.print_constant (Number.const_of_big_int i)
+  | Vtuple l -> fprintf fmt "@[<hov 2>(%a)@]"
+                        (Pp.print_list Pp.comma print_value) l
   | Vconstr (rs, lf) -> fprintf fmt "@[<hov 2>(%a@ %a)@]"
                                 Expr.print_rs rs
                                 (Pp.print_list Pp.space print_field) lf
@@ -667,6 +690,7 @@ let translate_module =
       Ident.Hid.add memo name pm;
       pm
 
+exception Tuple
 exception Constructor
 exception Field
 
@@ -675,6 +699,7 @@ let get_decl env mm rs =
   if debug then Format.printf "get_decl@.";
   let id = rs.rs_name in
   if debug then Format.printf "looking for rs %s@." id.id_string;
+  if is_rs_tuple rs then raise Tuple;
   let pm = find_module_id env mm id in
   if debug then Format.printf "pmodule %s@."
                               (pm.Pmodule.mod_theory.Theory.th_name.id_string);
@@ -946,9 +971,8 @@ let rec matching info v pat =
   | Pvar vs -> add_vs vs v info
   | Ptuple pl ->
      begin match v with
-     | Vconstr (rs, l) ->
-        assert (is_rs_tuple rs);
-        List.fold_left2 matching info (List.map field_get l) pl
+     | Vtuple l ->
+        List.fold_left2 matching info l pl
      | _ -> assert false
      end
   | Por (p1, p2) ->
@@ -1031,6 +1055,9 @@ let rec interp_expr info (e:Mltree.expr) : value =
            if is_mutable then Fmutable (ref v) else Fimmutable v
          in
          Vconstr(rs, List.map2 field_of_expr rs.rs_cty.cty_args le)
+      | Tuple ->
+         if debug then Format.printf "tuple@.";
+         Vtuple (List.map (interp_expr info) le)
       | Field ->
          if debug then Format.printf "field@.";
          (* TODO keep field info when applying constructors, use here ?*)
@@ -1127,16 +1154,38 @@ let rec interp_expr info (e:Mltree.expr) : value =
                   (fun info rd -> add_fundecl rd.rec_sym (Dlet ld) info)
                   info rdl in
      interp_expr info e
-  | Eraise (xs,_)  ->
+  | Eraise (xs, oe)  ->
      if debug then Format.printf "Eraise %s@." xs.xs_name.id_string;
-     raise (Raised (xs.xs_name.id_string, append info.cs))
+     let ov = match oe with
+       | None -> None
+       | Some e -> Some (interp_expr info e) in
+     raise (Raised (xs, ov, append info.cs))
   | Eexn  _ -> if debug then Format.printf "Eexn@.";
                          raise CannotReduce
   | Eabsurd -> if debug then Format.printf "Eabsurd@.";
                raise CannotReduce
   | Ehole -> if debug then Format.printf "Ehole@.";
              raise CannotReduce
-  | Etry _-> if debug then Format.printf "Etry@."; raise CannotReduce)
+  | Etry (e,bl) ->
+     try interp_expr info e
+     with (Raised (xs, ov, _)  as e) ->
+          let rec aux = function
+            | [] -> if debug then Format.printf "Etry: uncaught exception@.";
+                    raise e
+            | (xs', pvl, e) :: bl when xs_equal xs xs' ->
+               begin match pvl, ov with
+               | [], None -> interp_expr info e
+               | l, Some (Vtuple l') when (List.length l = List.length l') ->
+                  let info = List.fold_left2 (fun info pv v -> add_pv pv v info)
+                                             info l l' in
+                  interp_expr info e
+               | [pv], Some v ->
+                  interp_expr (add_pv pv v info) e
+               | _ -> if debug then Format.printf "Etry: bad arity@.";
+                      aux bl end
+            | _::bl -> aux bl
+          in
+          aux bl)
 
 let eval_fun decl info = match decl with
   | Dlet (Lsym (_rs, _, _vl, expr)) ->
@@ -1148,8 +1197,11 @@ let rec value_of_term t =
   | Ttrue -> Vbool true
   | Tfalse -> Vbool false
   | Term.Tapp (ls, lp) when ls.ls_constr > 0 ->
-     Vconstr ((restore_rs ls),
-              (List.map (fun t -> Fimmutable (value_of_term t)) lp))
+     let rs = restore_rs ls in
+     if is_rs_tuple rs
+     then Vtuple (List.map value_of_term lp)
+     else Vconstr ((restore_rs ls),
+                   (List.map (fun t -> Fimmutable (value_of_term t)) lp))
   | Tnot t -> begin match value_of_term t with
               | Vbool b -> Vbool (not b)
               | _ -> raise CannotReduce end
@@ -1161,6 +1213,7 @@ let rec term_of_value = function
   | Vbool true -> t_bool_true
   | Vbool false -> t_bool_false
   | Vint i -> t_bigint_const i
+  | Vtuple l -> t_tuple (List.map term_of_value l)
   | Vconstr (rs, lf) ->
      t_app (ls_of_rs rs) (List.map (fun f -> term_of_value (field_get f)) lf)
            (ls_of_rs rs).ls_value
@@ -1256,8 +1309,8 @@ let reflection_by_function do_trans s env = Trans.store (fun task ->
           if debug then Format.printf "eval_fun@.";
           let res =
             try term_of_value (eval_fun decl info)
-            with Raised (s1, s2) ->
-              Format.eprintf "Raised %s %s@." s1 s2;
+            with Raised (xs,_,s) ->
+              Format.eprintf "Raised %s %s@." (xs.xs_name.id_string) s;
               raise (ReductionFail renv) (*(try eval_fun decl info with Raised _ -> Vbool false)*) in
           if debug then Format.printf "res %a@." Pretty.print_term res;
           let rinfo = {renv with subst = Mvs.add vres res renv.subst} in