(* =========================================================== *)
(* Main formal verification functions *)
(* Author: Alexey Solovyev *)
(* Date: 2012-10-27 *)
(* =========================================================== *)
needs "verifier/interval_m/verifier.ml";;
needs "verifier/m_verifier.hl";;
needs "verifier/m_verifier_build.hl";;
needs "taylor/m_taylor_arith2.hl";;
needs "misc/vars.hl";;
#load "unix.cma";;
module M_verifier_main = struct
open Arith_misc;;
open Interval_arith;;
open Eval_interval;;
open More_float;;
open M_verifier;;
open M_verifier_build;;
open M_taylor;;
open M_taylor_arith2;;
open Taylor;;
open Misc_vars;;
open Verifier_options;;
(* Parameters *)
type verification_parameters =
{
(* If true, then monotonicity properties can be used *)
(* to reduce the dimension of a problem *)
allow_derivatives : bool;
(* If true, then convexity can be used *)
(* to reduce the dimension of a problem *)
convex_flag : bool;
(* If true, then verification on internal subdomains can be skipped *)
(* for a monotone function *)
mono_pass_flag : bool;
(* If true, then raw interval arithmetic can be used *)
(* (without Taylor approximations) *)
raw_intervals_flag : bool;
(* If true, then an informal procedure is used to determine *)
(* the optimal precision for the formal verification *)
adaptive_precision : bool;
(* This parameter might be used in cases when the certificate search *)
(* procedure returns a wrong result due to rounding errors *)
(* (this parameter will be eliminated when the search procedure is corrected) *)
eps : float;
};;
let default_params =
{
allow_derivatives = true;
convex_flag = true;
mono_pass_flag = true;
raw_intervals_flag = true;
adaptive_precision = true;
eps = 0.0;
};;
type verification_stats =
{
total_time : float;
formal_verification_time : float;
certificate : Verifier.certificate_stats;
};;
(********************************)
(* Adds a constant approximation to the table of known constants *)
let add_constant_interval int_th =
Eval_interval.add_constant_interval int_th;
Informal_eval_interval.add_constant_interval int_th;;
(* Tests if an expression has only given binary and unary operations *)
let test_expression bin_ops unary_ops =
let rec test =
(* Tests if the expression is in the form `a$i` *)
let test_vector tm =
let var, index = dest_binary "$" tm in
dest_var var, dest_small_numeral index in
(* Tests if the expression is a valid binary operation *)
let test_binary tm =
try
let lhs, rhs = dest_comb tm in
let op, lhs = dest_comb lhs in
let c, _ = dest_const op in
if mem c bin_ops then (test lhs && test rhs) else false
with Failure _ -> false in
(* Tests if the expression is a valid unary operation *)
let test_unary tm =
try
let lhs, rhs = dest_comb tm in
let c, _ = dest_const lhs in
if mem c unary_ops then test rhs else false
with Failure _ -> false in
fun tm ->
frees tm = [] or
can dest_var tm or
can test_vector tm or
test_unary tm or
test_binary tm in
test;;
(* Tests if the given expression is a polynomial expression *)
let is_poly =
let bin_ops = ["real_add"; "real_mul"; "real_sub"; "real_pow"] in
let unary_ops = ["real_neg"] in
test_expression bin_ops unary_ops;;
(**********************************)
(* Creates basic verification functions *)
let rec mk_funs =
(* add *)
let mk_add n (f1, tf1, ti1) (f2, tf2, ti2) =
(fun p1 p2 x ->
let a = f1 p1 p2 x and
b = f2 p1 p2 x in
eval_m_taylor_add2 n p1 p2 a b),
Plus (tf1, tf2),
(fun p1 p2 x ->
let a = ti1 p1 p2 x and
b = ti2 p1 p2 x in
Informal_taylor.eval_m_taylor_add p1 p2 a b) in
(* sub *)
let mk_sub n (f1, tf1, ti1) (f2, tf2, ti2) =
let neg_one = Interval.mk_interval(-1.0, -1.0) in
(fun p1 p2 x ->
let a = f1 p1 p2 x and
b = f2 p1 p2 x in
eval_m_taylor_sub2 n p1 p2 a b),
Plus (tf1, Scale(tf2, neg_one)),
(fun p1 p2 x ->
let a = ti1 p1 p2 x and
b = ti2 p1 p2 x in
Informal_taylor.eval_m_taylor_sub p1 p2 a b) in
(* mul *)
let mk_mul n (f1, tf1, ti1) (f2, tf2, ti2) =
(fun p1 p2 x ->
let a = f1 p1 p2 x and
b = f2 p1 p2 x in
eval_m_taylor_mul2 n p1 p2 a b),
Product (tf1, tf2),
(fun p1 p2 x ->
let a = ti1 p1 p2 x and
b = ti2 p1 p2 x in
Informal_taylor.eval_m_taylor_mul p1 p2 a b) in
(* neg *)
let mk_neg n (f1, tf1, ti1) =
(fun p1 p2 x ->
let a = f1 p1 p2 x in
eval_m_taylor_neg2 n a),
Scale (tf1, Interval.mk_interval (-1.0, -1.0)),
(fun p1 p2 x ->
let a = ti1 p1 p2 x in
Informal_taylor.eval_m_taylor_neg a) in
(* sqrt *)
let mk_sqrt n (f1, tf1, ti1) =
(fun p1 p2 x ->
let a = f1 p1 p2 x in
eval_m_taylor_sqrt2 n p1 p2 a),
Uni_compose (Univariate.usqrt, tf1),
(fun p1 p2 x ->
let a = ti1 p1 p2 x in
Informal_taylor.eval_m_taylor_sqrt p1 p2 a) in
(* inv *)
let mk_inv n (f1, tf1, ti1) =
(fun p1 p2 x ->
let a = f1 p1 p2 x in
eval_m_taylor_inv2 n p1 p2 a),
Uni_compose (Univariate.uinv, tf1),
(fun p1 p2 x ->
let a = ti1 p1 p2 x in
Informal_taylor.eval_m_taylor_inv p1 p2 a) in
(* atn *)
let mk_atn n (f1, tf1, ti1) =
(fun p1 p2 x ->
let a = f1 p1 p2 x in
eval_m_taylor_atn2 n p1 p2 a),
Uni_compose (Univariate.uatan, tf1),
(fun p1 p2 x ->
let a = ti1 p1 p2 x in
Informal_taylor.eval_m_taylor_atn p1 p2 a) in
(* acs *)
let mk_acs n (f1, tf1, ti1) =
(fun p1 p2 x ->
let a = f1 p1 p2 x in
eval_m_taylor_acs2 n p1 p2 a),
Uni_compose (Univariate.uacos, tf1),
(fun p1 p2 x ->
let a = ti1 p1 p2 x in
Informal_taylor.eval_m_taylor_acs p1 p2 a) in
(* binary operations *)
let bin_ops =
["real_add", mk_add;
"real_sub", mk_sub;
"real_mul", mk_mul] in
(* unary operations *)
let unary_ops =
["real_neg", mk_neg;
"sqrt", mk_sqrt;
"atn", mk_atn;
"acs", mk_acs;
"real_inv", mk_inv] in
(* makes a binary operation *)
let mk_bin n pp x_var tm =
let lhs, rhs = dest_comb tm in
let op, lhs = dest_comb lhs in
let mk_f = assoc ((fst o dest_const) op) bin_ops in
let l_funs = mk_funs n pp (mk_abs(x_var, lhs)) and
r_funs = mk_funs n pp (mk_abs(x_var, rhs)) in
mk_f n l_funs r_funs in
(* makes an unary operation *)
let mk_unary n pp x_var tm =
let op, rhs = dest_comb tm in
let mk_f = assoc ((fst o dest_const) op) unary_ops in
let funs = mk_funs n pp (mk_abs(x_var, rhs)) in
mk_f n funs in
(* the main function *)
fun n pp fun_tm ->
let x_var, body_tm = dest_abs fun_tm in
if is_poly body_tm then
let eval_fs, tf, ti = mk_verification_functions_poly pp fun_tm in
eval_fs.taylor, tf, ti.Informal_verifier.taylor
else
try mk_bin n pp x_var body_tm with Failure _ ->
mk_unary n pp x_var body_tm;;
(* Prepares verification functions *)
(* fun_tm must be in the form `\x. f x` *)
let mk_verification_functions =
let dummy_f pp lo hi = failwith "dummy f" and
dummy_df i pp lo hi = failwith "dummy df" and
dummy_ddf i j pp lo hi = failwith "dummy ddf" and
dummy_diff2 lo hi = failwith "dummy diff2" in
fun params pp fun_tm ->
let x_var, body_tm = dest_abs fun_tm in
if is_poly body_tm then
mk_verification_functions_poly pp fun_tm
else
let n = get_dim x_var in
let eval_taylor, tf, eval_ti = mk_funs n pp fun_tm in
let _ = params := {!params with raw_intervals_flag = false; convex_flag = false} in
{taylor = eval_taylor;
f = dummy_f; df = dummy_df; ddf = dummy_ddf; diff2_f = dummy_diff2}, tf,
{Informal_verifier.taylor = eval_ti;
Informal_verifier.f = dummy_f;
Informal_verifier.df = dummy_df;
Informal_verifier.ddf = dummy_ddf};;
(********************************)
let convert_to_float_list pp lo_flag list_tm =
let tms = dest_list list_tm in
let i_funs = map build_interval_fun tms in
let ints = map (fun f -> eval_interval_fun pp f [] []) i_funs in
let extract = (if lo_flag then fst else snd) o dest_pair o rand o concl in
mk_list (map extract ints, real_ty);;
(* Creates a theorem |- interval[xx_tm, zz_tm] SUBSET interval[float(xx_tm), float(zz_tm)]
and two lists: float(xx_tm) and float(zz_tm) *)
let mk_float_domain pp (xx_tm, zz_tm) =
let xx_list = dest_list xx_tm and
zz_list = dest_list zz_tm in
let n = length xx_list in
let get_intervals tms =
let i_funs = map build_interval_fun tms in
map (fun f -> eval_interval_fun pp f [] []) i_funs in
let xx_ints = get_intervals xx_list and
zz_ints = get_intervals zz_list in
let xx_ineqs = map (CONJUNCT1 o ONCE_REWRITE_RULE[interval_arith]) xx_ints and
zz_ineqs = map (CONJUNCT2 o ONCE_REWRITE_RULE[interval_arith]) zz_ints in
let a_vals = map (lhand o concl) xx_ineqs and
b_vals = map (rand o concl) zz_ineqs in
let a_vars = mk_real_vars n "a" and
b_vars = mk_real_vars n "b" and
c_vars = mk_real_vars n "c" and
d_vars = mk_real_vars n "d" in
let th0 = (INST (zip xx_list c_vars) o INST (zip zz_list d_vars) o
INST (zip a_vals a_vars) o INST (zip b_vals b_vars))
subset_interval_thms_array.(n) in
itlist MY_PROVE_HYP (xx_ineqs @ zz_ineqs) th0,
(mk_list (a_vals, real_ty), mk_list (b_vals, real_ty));;
(* Given a term a < b, returns the theorem |- a - b < &0 <=> a < b *)
(* Also, deals with > and / *)
(* A user can provide additional rewrite theorems *)
let mk_standard_ineq =
let lemma = REAL_ARITH `a < b <=> a - b < &0` in
fun thms tm ->
let th0 = (REWRITE_CONV([real_gt; real_div] @ thms) THENC DEPTH_CONV let_CONV) tm in
let rhs = rand (concl th0) in
let th1 = (ONCE_REWRITE_CONV[lemma] THENC PURE_REWRITE_CONV[REAL_NEG_0; REAL_SUB_RZERO; REAL_SUB_LZERO]) rhs in
TRANS th0 th1;;
(* Converts a term in the form `x + y` into the term `\x:real^2. x$1 + x$2` *)
let expr_to_vector_fun =
let comp_op = `$` in
fun expr_tm ->
let vars = List.sort Pervasives.compare (frees expr_tm) in
let n = length vars in
let x_var = mk_var ("x", n_vector_type_array.(if n = 0 then 1 else n)) in
let x_tm = mk_icomb (comp_op, x_var) in
let vars2 = map (fun i -> mk_comb (x_tm, mk_small_numeral i)) (1--n) in
mk_abs (x_var, subst (zip vars2 vars) expr_tm),
(if n = 0 then mk_vector_list [x_var] else mk_vector_list vars);;
(* Given an inequality `P x y`, variable names and the corresponding bounds,
yields `(x0 <= x /\ x <= x1) /\ (y0 <= y /\ y <= y1) ==> P x y` *)
let mk_ineq ineq_tm names dom_tm =
let lo_list = dest_list (fst dom_tm) and
hi_list = dest_list (snd dom_tm) in
let vars = map (fun name -> mk_var (name, real_ty)) names in
let lo_ineqs = map2 (fun tm1 tm2 -> mk_binop le_op_real tm1 tm2) lo_list vars and
hi_ineqs = map2 (fun tm1 tm2 -> mk_binop le_op_real tm1 tm2) vars hi_list in
let ineqs = map2 (fun tm1 tm2 -> mk_conj (tm1, tm2)) lo_ineqs hi_ineqs in
let cond = end_itlist (curry mk_conj) ineqs in
mk_imp (cond, ineq_tm);;
(* Reverts the effect of mk_ineq function *)
let dest_ineq ineq_tm =
if frees ineq_tm = [] then
ineq_tm, [], (real_empty_list, real_empty_list)
else
let tm0 = (rand o concl o PURE_REWRITE_CONV[IMP_IMP; GSYM CONJ_ASSOC]) ineq_tm in
let cond, ineq = dest_imp tm0 in
let conds = striplist dest_conj cond in
let ineqs = ref [] in
let decode_ineq tm =
let lhs, rhs = dest_binop le_op_real tm in
let lo_flag = (frees lhs = []) in
let name = (fst o dest_var) (if lo_flag then rhs else lhs) in
let val_ref =
try assoc name !ineqs
with Failure _ ->
let val_ref = ref (x_var_real, x_var_real) in
ineqs := ((name, val_ref) :: !ineqs); val_ref in
val_ref := if lo_flag then (lhs, snd !val_ref) else (fst !val_ref, rhs) in
let _ = map (fun tm ->
(try decode_ineq tm with Failure _ ->
failwith ("Bad variable bound inequality: "^string_of_term tm))) conds in
let names, bounds0 = unzip !ineqs in
let lo, hi = unzip (map (fun r -> !r) bounds0) in
let test_bounds bounds bound_name =
let _ = map2 (fun tm name -> if frees tm <> [] then
failwith (bound_name^" bound is not defined for "^name) else ())
bounds names in () in
let _ = test_bounds hi "Upper"; test_bounds lo "Lower" in
ineq, names, (mk_real_list lo, mk_real_list hi);;
(*********************************)
(* Normalizes a verification result *)
let normalize_result norm_flag v1 eq_th1 domain_sub_th pass_thm =
let th0 = REWRITE_RULE[m_cell_pass] pass_thm in
let n = (get_dim o fst o dest_forall o concl) th0 in
let th1 = SPEC v1 th0 in
let comp_thms = end_itlist CONJ (Array.to_list comp_thms_array.(n)) in
let th2 = REWRITE_RULE[comp_thms] th1 in
let th3 = (UNDISCH_ALL o REWRITE_RULE[GSYM eq_th1]) th2 in
let dom_th = (UNDISCH_ALL o SPEC v1 o REWRITE_RULE[SUBSET]) domain_sub_th in
let th4 = (DISCH_ALL o MY_PROVE_HYP dom_th) th3 in
let th5 = REWRITE_RULE[IN_INTERVAL; dimindex_array.(n); gen_in_interval n; comp_thms] th4 in
if norm_flag then GEN_ALL th5 else th4;;
(* Verifies the given inequality *)
(* Returns the final theorem and verification statistics *)
let verify_ineq0 params0 norm_flag pp ineq_tm var_names (lo_tm, hi_tm) rewrite_thms =
let total_start = Unix.gettimeofday() in
let eq_th1 = mk_standard_ineq rewrite_thms ineq_tm in
let ineq_tm1 = (lhand o rand o concl) eq_th1 in
if frees ineq_tm1 = [] then
let i_fun = build_interval_fun ineq_tm1 in
let th0 = eval_interval_fun pp i_fun [] [] in
let th1 = float_interval_lt0 th0 in
let total = Unix.gettimeofday() -. total_start in
REWRITE_RULE[GSYM eq_th1] th1,
{total_time = total; formal_verification_time = total; certificate = Verifier.dummy_stats}
else
let fun_tm, v1 = expr_to_vector_fun ineq_tm1 in
let vars = map (fst o dest_var) (dest_vector v1) in
let lo_list = dest_list lo_tm and
hi_list = dest_list hi_tm in
let bounds0 = zip var_names (zip lo_list hi_list) in
let bounds = itlist (fun name list -> assoc name bounds0 :: list) vars [] in
let xx, zz = unzip bounds in
let xx, zz = mk_real_list xx, mk_real_list zz in
let domain_sub_th, (xx1, zz1) = mk_float_domain pp (xx, zz) in
let n = (get_dim o fst o dest_abs) fun_tm in
let xx2 = Informal_taylor.convert_to_float_list pp true xx and
zz2 = Informal_taylor.convert_to_float_list pp false zz in
let xx_float = map float_of_float_tm (dest_list xx1) and
zz_float = map float_of_float_tm (dest_list zz1) in
let params = ref params0 in
let eval_fs, tf, ti = mk_verification_functions params pp fun_tm in
let _ = !info_print_level < 1 or (report0 "Constructing a solution certificate... "; true) in
let certificate = Verifier.run_test tf xx_float zz_float false 0.0
!params.allow_derivatives !params.convex_flag !params.mono_pass_flag
!params.raw_intervals_flag !params.eps in
let stats = Verifier.result_stats certificate in
let _ = !info_print_level < 1 or (report0 " done\n"; true) in
let _ = !info_print_level < 1 or (Verifier.report_stats stats; true) in
let c1 = Verifier.transform_result xx_float zz_float certificate in
let start, finish, result =
if !params.adaptive_precision then
let _ = !info_print_level < 1 or (report0 "Informal verification... "; true) in
let c1p = Informal_verifier.m_verify_list pp 1 pp ti c1 xx2 zz2 in
let _ = !info_print_level < 1 or (report0 " done\n"; true) in
let _ = !info_print_level < 1 or (report0 "Formal verification... "; true) in
let start = Unix.gettimeofday() in
let result = m_p_verify_list n pp eval_fs c1p xx1 zz1 in
let finish = Unix.gettimeofday() in
let _ = !info_print_level < 1 or (report0 " done\n"; true) in
start, finish, result
else
let _ = !info_print_level < 1 or (report0 "Formal verification... "; true) in
let start = Unix.gettimeofday() in
let result = m_verify_list n pp eval_fs c1 xx1 zz1 in
let finish = Unix.gettimeofday() in
let _ = !info_print_level < 1 or (report0 " done\n"; true) in
start, finish, result in
normalize_result norm_flag v1 eq_th1 domain_sub_th result,
{total_time = finish -. total_start; formal_verification_time = finish -. start; certificate = stats};;
(* A simple verification function which accepts
a list of rewrite theorems which are applied to the inequality
before verification *)
let verify_ineq_and_rewrite rewrite_thms params pp ineq_tm =
let ineq, vars, bounds = dest_ineq ineq_tm in
verify_ineq0 params true pp ineq vars bounds rewrite_thms;;
(* The simplest verification function *)
let verify_ineq = verify_ineq_and_rewrite [];;
end;;