[exps] Add tests for split_nn

examples/mnist/splitted_nn.mlw

+theory MNIST
+
+  use caisar.types.Vector
+  use ieee_float.Float64
+  use caisar.types.Float64WithBounds as Feature
+  use caisar.types.IntWithBounds as Label
+  use caisar.model.Model
+  use caisar.dataset.CSV
+  use caisar.robust.ClassRobustCSV
+  use caisar.robust.ClassRobustVector
+
+  constant pre_model_filename: string
+  constant post_model_filename: string
+  constant dataset_filename: string
+
+  constant label_bounds: Label.bounds =
+    Label.{ lower = 0; upper = 9 }
+  
+  constant feature_bounds: Feature.bounds =
+    Feature.{ lower = (0.0:t); upper = (1.0:t) }
+
+  goal pruned:
+    let pre_nn = read_model pre_model_filename in
+    let post_nn = read_model post_model_filename in
+    let dataset = read_dataset dataset_filename in
+    let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
+    CSV.forall_ dataset (fun l e ->
+        forall perturbed_e.
+          has_length perturbed_e (length e) ->
+          FeatureVector.valid feature_bounds perturbed_e ->
+          let perturbation = perturbed_e - e in
+          ClassRobustVector.bounded_by_epsilon perturbation eps ->
+          let out1 = pre_nn@@perturbed_e in
+          let out2 = post_nn@@out1 in
+          forall j. Label.valid label_bounds j -> j <> l ->
+          out2[l] .>= out2[j]
+     )
+
+
+end

tests/dune

 (cram
  (alias local)
- (applies_to * \ nir_to_onnx acasxu_ci arithmetic check_pruning)
+ (applies_to * \ nir_to_onnx acasxu_ci arithmetic check_pruning splited_nn)
  (deps
   (package caisar)
   setup_env.sh
@@ -42,6 +42,21 @@
   )
  (package caisar))
 
+ (cram
+ (alias local)
+ (applies_to splitted_nn)
+ (deps
+  (package caisar)
+  setup_env.sh
+  (glob_files bin/*)
+  filter_tmpdir.sh
+  ../examples/mnist/splitted_nn.mlw
+  ../examples/mnist/nets/dummy_nn/fnn_pre_s42.onnx
+  ../examples/mnist/nets/dummy_nn/fnn_post_s42.onnx
+  ../examples/mnist/csv/single_image.csv
+  )
+ (package caisar))
+
 
 (cram
  (alias ci)

tests/splitted_nn.t

+  $ . ./setup_env.sh
+
+  $ ls ../examples/
+  acasxu
+  mnist
+
+#  $ caisar verify --prover PyRAT  --ltag=StackTrace --define pre_model_filename:nets/dummy_nn/fnn_pre_s42.onnx --define post_model_filename:nets/dummy_nn/fnn_post_s42.onnx --define dataset_filename:csv/single_image.csv ../examples/mnist/splitted_nn.mlw -v