[stdlib] Rework stdlib to have a DataSet theory.

src/verification.ml

@@ -80,38 +80,33 @@ let answer_saver limit config env config_prover dataset_csv task =
       | None -> invalid_arg "No dataset provided for SAVer"
       | Some s -> s
     in
+    let robust_predicate =
+      let dataset_th = Pmodule.read_module env [ "caisar" ] "DataSet" in
+      Theory.ns_find_ls dataset_th.mod_theory.th_export [ "robust" ]
+    in
     let goal = Task.task_goal_fmla task in
     let eps, svm_filename =
       match goal.t_node with
-      | Tquant (Tforall, b) -> (
-        let _, _, pred = Term.t_open_quant b in
-        let svm_t = Pmodule.read_module env [ "caisar" ] "SVM" in
-        let robust_to_predicate =
-          let open Theory in
-          ns_find_ls svm_t.mod_theory.th_export [ "robust_to" ]
-        in
-        match pred.t_node with
-        | Term.Tapp
-            ( ls,
-              [
-                { t_node = Tapp (svm_app_sym, _); _ };
-                _;
-                { t_node = Tconst e; _ };
-              ] ) ->
-          if Term.ls_equal ls robust_to_predicate
-          then
-            let eps = Fmt.str "%a" Constant.print_def e in
-            let svm_filename =
-              match Language.lookup_loaded_svms svm_app_sym with
-              | Some t -> t.filename
-              | None -> invalid_arg "No SVM model found in task"
-            in
-            (eps, svm_filename)
-          else failwith "Wrong predicate found"
-        | _ ->
-          (* no other predicate than robust_to is supported *)
-          failwith "Unsupported predicate by SAVer")
-      | _ -> failwith "Unsupported predicate by SAVer"
+      | Term.Tapp
+          ( ls,
+            [
+              { t_node = Tapp (ls_svm_apply, _); _ };
+              _dataset;
+              { t_node = Tconst e; _ };
+            ] ) ->
+        if Term.ls_equal ls robust_predicate
+        then
+          let eps = Fmt.str "%a" Constant.print_def e in
+          let svm_filename =
+            match Language.lookup_loaded_svms ls_svm_apply with
+            | Some t -> t.filename
+            | None -> invalid_arg "No SVM model found in task"
+          in
+          (eps, svm_filename)
+        else failwith "Wrong predicate found"
+      | _ ->
+        (* no other predicate than robust_to is supported *)
+        failwith "Unsupported predicate by SAVer"
     in
     let svm_file = Unix.realpath svm_filename in
     let dataset_file = Unix.realpath dataset_filename in
@@ -141,27 +136,24 @@ let answer_saver limit config env config_prover dataset_csv task =
       ~printing_info:Printer.default_printing_info (Buffer.create 10)
   in
   let prover_result = Call_provers.wait_on_call prover_call in
-  let answer =
-    match prover_result.pr_answer with
-    | Call_provers.HighFailure -> (
-      let pr_output = prover_result.pr_output in
-      let matcher =
-        Re__Pcre.regexp
-          "\\[SUMMARY\\]\\s*(\\d+)\\s*[0-9.]+\\s*[0-9.]+\\s*\\d+\\s*(\\d+)\\s*\\d"
-      in
-      match Re__Core.exec_opt matcher pr_output with
-      | Some g ->
-        if Int.of_string (Re__Core.Group.get g 1)
-           = Int.of_string (Re__Core.Group.get g 2)
-        then Call_provers.Valid
-        else Call_provers.Invalid
-      | None -> Call_provers.HighFailure)
-    | _ ->
-      (* Any other answer than HighFailure should never happen as we do not
-         define anything in SAVer's driver. *)
-      assert false
-  in
-  answer
+  match prover_result.pr_answer with
+  | Call_provers.HighFailure -> (
+    let pr_output = prover_result.pr_output in
+    let matcher =
+      Re__Pcre.regexp
+        "\\[SUMMARY\\]\\s*(\\d+)\\s*[0-9.]+\\s*[0-9.]+\\s*\\d+\\s*(\\d+)\\s*\\d"
+    in
+    match Re__Core.exec_opt matcher pr_output with
+    | Some g ->
+      if Int.of_string (Re__Core.Group.get g 1)
+         = Int.of_string (Re__Core.Group.get g 2)
+      then Call_provers.Valid
+      else Call_provers.Invalid
+    | None -> Call_provers.HighFailure)
+  | _ ->
+    (* Any other answer than HighFailure should never happen as we do not define
+       anything in SAVer's driver. *)
+    assert false
 
 let answer_generic limit config prover config_prover driver task =
   let task_prepared = Driver.prepare_task driver task in

stdlib/caisar.mlw

@@ -25,22 +25,50 @@ theory NN
   type input_type = t
 end
 
-theory SVM
+theory Model
   use ieee_float.Float64
   use int.Int
+  use array.Array
+
+  type model = {
+    nb_inputs: int;
+    nb_outputs: int;
+  }
 
-  type input_type = int -> t
-  type output_type = int
+  function predict: model -> array t -> int
+end
+
+theory DataSet
+  use ieee_float.Float64
+  use int.Int
+  use array.Array
+  use Model
 
-  type svm = {
-    apply : input_type -> output_type;
-    nb_inputs : int;
-    nb_classes : int;
+  type features = array t
+  type class = int
+
+  type datum = (features, class)
+
+  type dataset = {
+    nb_features: int;
+    nb_classes: int;
+    data: array datum
   }
 
-  predicate linfty_distance (a: input_type) (b: input_type) (eps:t) (n: int) =
-    forall i. 0 <= i < n -> .- eps .< a i .- b i .< eps
+  constant dataset: dataset
+
+  predicate linfty_distance (n: int) (a: features) (b: features) (eps: t) =
+    forall i: int. 0 <= i < n -> .- eps .< a[i] .- b[i] .< eps
 
-  predicate robust_to (svm: svm) (a: input_type) (eps: t) =
-    forall b. linfty_distance a b eps svm.nb_inputs -> svm.apply a = svm.apply b
+  predicate robust (m: model) (d: dataset) (eps: t) =
+    forall i: int. 0 <= i < d.data.length ->
+      forall x': features.
+        let (x, _) = d.data[i] in
+        linfty_distance d.nb_features x x' eps ->
+        predict m x = predict m x'
+end
+
+theory SVM
+  use Model
+  type svm = model
 end

tests/simple_ovo.t

@@ -29,9 +29,9 @@ Test verify
   > theory T
   >   use TestSVM.SVMasArray
   >   use ieee_float.Float64
-  >   use caisar.SVM
+  >   use caisar.DataSet
   > 
-  >   goal G: forall a : input_type. robust_to svm_apply a (8.0:t)
+  >   goal G: robust svm_apply dataset (8.0:t)
   > end
   > EOF
   [caisar] Goal G: High failure