From b7ff363cc7b84b906f58dbde42d3b45dcaad720c Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 16 Nov 2022 18:20:31 +0100
Subject: [PATCH] [verification] Create theory from json config file.
---
src/dataset.ml | 74 ++++++++++++++++++++++++----------
src/dataset.mli | 7 +++-
src/verification.ml | 85 +++++++++++++++++++++++++++++++++++----
src/verification.mli | 2 +-
tests/pyrat_verify_json.t | 18 +++++++++
5 files changed, 153 insertions(+), 33 deletions(-)
create mode 100644 tests/pyrat_verify_json.t
diff --git a/src/dataset.ml b/src/dataset.ml
index 456981e..32dbe5a 100644
--- a/src/dataset.ml
+++ b/src/dataset.ml
@@ -23,6 +23,20 @@
open Why3
open Base
+let real_constant_of_float value =
+ let neg = Float.is_negative value in
+ let value = Fmt.str "%.64f" (Float.abs value) in
+ (* Split into integer and fractional parts. *)
+ let int_frac = String.split value ~on:'.' in
+ let int = List.hd_exn int_frac in
+ let frac =
+ match List.tl_exn int_frac with
+ | [] -> ""
+ | [ s ] -> s
+ | _ -> assert false (* Since every float has one '.' at most. *)
+ in
+ Constant.ConstReal (Number.real_literal ~radix:10 ~neg ~int ~frac ~exp:None)
+
let float_of_real_constant rc =
Float.of_string (Fmt.str "%a" Number.(print_real_constant full_support) rc)
@@ -84,8 +98,39 @@ let interpret_normalization =
| _ -> acc)
[]
+let term_of_normalization env normalization =
+ let th = Pmodule.read_module env [ "caisar" ] "DataSetClassification" in
+ let t_dataset =
+ let ls_dataset = Theory.ns_find_ls th.mod_theory.th_export [ "dataset" ] in
+ Term.t_app_infer ls_dataset []
+ in
+ let ty =
+ let th = Env.read_theory env [ "ieee_float" ] "Float64" in
+ Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) []
+ in
+ match normalization with
+ | MinMax (min, max) ->
+ let t_min = Term.t_const (real_constant_of_float min) ty in
+ let t_max = Term.t_const (real_constant_of_float max) ty in
+ let ls_min_max_scale =
+ Theory.ns_find_ls th.mod_theory.th_export [ "min_max_scale" ]
+ in
+ Term.t_app_infer ls_min_max_scale [ t_min; t_max; t_dataset ]
+ | Znorm (mean, std_dev) ->
+ let t_mean = Term.t_const (real_constant_of_float mean) ty in
+ let t_std_dev = Term.t_const (real_constant_of_float std_dev) ty in
+ let ls_z_norm = Theory.ns_find_ls th.mod_theory.th_export [ "z_norm" ] in
+ Term.t_app_infer ls_z_norm [ t_mean; t_std_dev; t_dataset ]
+
type eps = float [@@deriving yojson, show]
+let string_of_eps eps = Float.to_string eps
+
+let term_of_eps env eps =
+ let th = Env.read_theory env [ "ieee_float" ] "Float64" in
+ let ty = Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) [] in
+ Term.t_const (real_constant_of_float eps) ty
+
type property =
| Correct
| Robust of eps
@@ -99,8 +144,6 @@ type ('a, 'b) predicate = {
property : property;
}
-let string_of_eps eps = Float.to_string eps
-
let string_of_predicate_kind = function
| Correct -> "correct"
| Robust _ -> "robust"
@@ -160,19 +203,6 @@ let clip_value value =
let value = if Float.is_negative value then Float.zero else value in
if Float.(is_negative (one -. value)) then Float.one else value
-let real_constant value =
- (* Split into integer and fractional parts. *)
- let int_frac = String.split Float.(to_string (abs value)) ~on:'.' in
- let int = List.hd_exn int_frac in
- let frac =
- match List.tl_exn int_frac with
- | [] -> ""
- | [ s ] -> s
- | _ -> assert false (* Since every float has one '.' at most. *)
- in
- Constant.ConstReal
- (Number.real_literal ~radix:10 ~neg:false ~int ~frac ~exp:None)
-
let add_axioms ?eps ~clip th task input value =
let eps = Float.(abs (of_string (Option.value eps ~default:"0"))) in
let value = Float.of_string value in
@@ -185,7 +215,7 @@ let add_axioms ?eps ~clip th task input value =
let t_ge =
let value = value -. eps in
let value = if clip then clip_value value else value in
- let cst = real_constant value in
+ let cst = real_constant_of_float value in
Term.(ps_app le [ t_const cst Ty.ty_real; fs_app input [] Ty.ty_real ])
in
let task = Task.add_prop_decl task Decl.Paxiom pr_ge t_ge in
@@ -197,7 +227,7 @@ let add_axioms ?eps ~clip th task input value =
let t_le =
let value = value +. eps in
let value = if clip then clip_value value else value in
- let cst = real_constant value in
+ let cst = real_constant_of_float value in
Term.(ps_app le [ fs_app input [] Ty.ty_real; t_const cst Ty.ty_real ])
in
Task.add_prop_decl task Decl.Paxiom pr_le t_le
@@ -217,16 +247,16 @@ let add_output_decl ~id predicate_kind ~outputs ~record th task =
(* Add goal formula. *)
let class_ = List.hd_exn record in
let goal_fmla =
- let gt = Theory.(ns_find_ls th.th_export [ Ident.op_infix ">" ]) in
- let class_ls = List.nth_exn outputs (Int.of_string class_) in
+ let ls_gt = Theory.(ns_find_ls th.th_export [ Ident.op_infix ">" ]) in
+ let ls_class = List.nth_exn outputs (Int.of_string class_) in
List.fold outputs ~init:Term.t_true ~f:(fun fmla output ->
- if Term.ls_equal class_ls output
+ if Term.ls_equal ls_class output
then fmla
else
let gt_fmla =
Term.(
- ps_app gt
- [ fs_app class_ls [] Ty.ty_real; fs_app output [] Ty.ty_real ])
+ ps_app ls_gt
+ [ fs_app ls_class [] Ty.ty_real; fs_app output [] Ty.ty_real ])
in
Term.t_and fmla gt_fmla)
in
diff --git a/src/dataset.mli b/src/dataset.mli
index e1465f7..f1f2e13 100644
--- a/src/dataset.mli
+++ b/src/dataset.mli
@@ -24,6 +24,9 @@ open Why3
type eps [@@deriving yojson, show]
+val string_of_eps : eps -> string
+val term_of_eps : Env.env -> eps -> Term.term
+
type property = private
| Correct
| Robust of eps
@@ -32,6 +35,8 @@ type property = private
type normalization [@@deriving yojson, show]
+val term_of_normalization : Env.env -> normalization -> Term.term
+
type ('model, 'dataset) predicate = private {
model : 'model;
dataset : 'dataset;
@@ -39,8 +44,6 @@ type ('model, 'dataset) predicate = private {
property : property;
}
-val string_of_eps : eps -> string
-
val interpret_predicate :
Env.env ->
on_model:(Term.lsymbol -> 'model) ->
diff --git a/src/verification.ml b/src/verification.ml
index cbe3b35..c802ac8 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -34,7 +34,7 @@ module File = struct
and property = {
dataset : string;
- normalization : Dataset.normalization list;
+ normalization : Dataset.normalization option;
kind : Dataset.property;
}
[@@deriving yojson, show]
@@ -192,14 +192,83 @@ let call_prover ~limit config env prover config_prover driver dataset_csv task =
additional_info)
let mstr_theory_of_json_config env (json_config : File.json_config) =
- let pmod = Language.nnet_parser env json_config.model in
- let th_pmod = (Wstdlib.Mstr.find "NNasArray" pmod).mod_theory in
- let name = "T" in
+ let model_parser =
+ let extension = Filename.(extension (basename json_config.model)) in
+ match String.lowercase extension with
+ | ".nnet" -> Language.nnet_parser
+ | ".onnx" -> Language.onnx_parser
+ | ".ovo" -> Language.ovo_parser
+ | "" -> invalid_arg "Cannot find model extension"
+ | _ -> invalid_arg (Fmt.str "Unrecognized model extension '%s'" extension)
+ in
+ let th_as_array =
+ let pmod = model_parser env (Unix.realpath json_config.model) in
+ (Wstdlib.Mstr.find "AsArray" pmod).mod_theory
+ in
+ let th_float64 = Env.read_theory env [ "ieee_float" ] "Float64" in
+ let th_ds_classification =
+ Pmodule.read_module env [ "caisar" ] "DataSetClassification"
+ in
+ let th_ds_props = Pmodule.read_module env [ "caisar" ] "DataSetProps" in
+ let name = "JSON_config" in
let th_uc = Theory.create_theory (Ident.id_fresh name) in
- let th_real = Env.read_theory env [ "real" ] "Real" in
- let th_uc = Theory.use_export th_uc th_real in
- let th_uc = Theory.use_export th_uc th_pmod in
- Wstdlib.Mstr.singleton name (Theory.close_theory th_uc)
+ let th_uc = Theory.use_export th_uc th_as_array in
+ let th_uc = Theory.use_export th_uc th_float64 in
+ let th_uc = Theory.use_export th_uc th_ds_classification.mod_theory in
+ let th_uc = Theory.use_export th_uc th_ds_props.mod_theory in
+ let t_dataset =
+ let ls_dataset =
+ Theory.ns_find_ls th_ds_classification.mod_theory.th_export [ "dataset" ]
+ in
+ Term.t_app_infer ls_dataset []
+ in
+ let t_model =
+ let ls_model = Theory.ns_find_ls th_as_array.th_export [ "model" ] in
+ Term.t_app_infer ls_model []
+ in
+ (* Add dataset normalization. *)
+ let t_dataset, th_uc =
+ match json_config.property.normalization with
+ | None -> (t_dataset, th_uc)
+ | Some n ->
+ let t_normalization = Dataset.term_of_normalization env n in
+ let ls_dataset_norm =
+ let ty =
+ Ty.ty_app
+ (Theory.ns_find_ts th_ds_classification.mod_theory.th_export
+ [ "dataset" ])
+ []
+ in
+ Term.create_fsymbol (Ident.id_fresh "dataset'") [] ty
+ in
+ let ld_dataset_norm =
+ Decl.make_ls_defn ls_dataset_norm [] t_normalization
+ in
+ ( Term.t_app_infer ls_dataset_norm [],
+ Theory.add_logic_decl th_uc [ ld_dataset_norm ] )
+ in
+ (* Create goal formula about specified property. *)
+ let th_uc =
+ let t_property =
+ match json_config.property.kind with
+ | Dataset.Correct ->
+ let ls_correct =
+ Theory.ns_find_ls th_ds_props.mod_theory.th_export [ "correct" ]
+ in
+ Term.t_app_infer ls_correct [ t_model; t_dataset ]
+ | Robust eps ->
+ let ls_robust =
+ Theory.ns_find_ls th_ds_props.mod_theory.th_export [ "robust" ]
+ in
+ let t_eps = Dataset.term_of_eps env eps in
+ Term.t_app_infer ls_robust [ t_model; t_dataset; t_eps ]
+ | CondRobust _ -> invalid_arg "Unsupported property"
+ in
+ let prsymbol = Decl.create_prsymbol (Ident.id_fresh "property") in
+ Theory.add_prop_decl th_uc Decl.Pgoal prsymbol t_property
+ in
+ let th = Theory.close_theory th_uc in
+ Wstdlib.Mstr.singleton name th
let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit prover
?dataset_csv file =
diff --git a/src/verification.mli b/src/verification.mli
index 73d5273..d1f2186 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -30,7 +30,7 @@ module File : sig
and property = private {
dataset : string;
- normalization : Dataset.normalization list;
+ normalization : Dataset.normalization option;
kind : Dataset.property;
}
[@@deriving yojson, show]
diff --git a/tests/pyrat_verify_json.t b/tests/pyrat_verify_json.t
new file mode 100644
index 0000000..aace626
--- /dev/null
+++ b/tests/pyrat_verify_json.t
@@ -0,0 +1,18 @@
+Test verify-json
+ $ cat - > test_data.csv << EOF
+ > 1,0,255,200,5,198
+ > EOF
+
+ $ cat - > config.json << EOF
+ > {"prover":["Pyrat"],"model":"TestNetwork.nnet","property":{"dataset":"test_data.csv","normalization":["MinMax",0.0,255.0],"kind":["Robust",0.01]}}
+ > EOF
+
+ $ chmod u+x bin/pyrat.py
+
+ $ bin/pyrat.py --version
+ PyRAT 1.1
+
+ $ PATH=$(pwd)/bin:$PATH
+
+ $ caisar verify-json config.json 2>&1 <<EOF | ./filter_tmpdir.sh
+ [caisar] Goal property: Unknown ()
--
GitLab