[exps] Uniformize, rename and reorganize specs

examples/mnist/check_pruning.mlw → examples/onnx_rewrite/comparison.mlw

-theory MNIST
+theory COMPARISON
 
-  use caisar.types.Vector
   use ieee_float.Float64
   use caisar.types.Float64WithBounds as Feature
   use caisar.types.IntWithBounds as Label
+  use caisar.types.Vector
   use caisar.model.Model
   use caisar.dataset.CSV
   use caisar.robust.ClassRobustCSV
   use caisar.robust.ClassRobustVector
 
-  constant model_filename: string
-  constant pruned_model_filename: string
+  constant model_filename_1: string
+  constant model_filename_2: 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) }
+  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 nn = read_model model_filename in
-    let pruned_nn = read_model pruned_model_filename in
+  goal comparison:
+    let nn_1 = read_model model_filename_1 in
+    let nn_2 = read_model model_filename_2 in
     let dataset = read_dataset dataset_filename in
     let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
     let delta = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
     CSV.forall_ dataset (fun _ 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 out = nn@@perturbed_e in
-          let pruned_out = pruned_nn@@perturbed_e in
-          .- delta .<= out[0] .- pruned_out[0] .<= delta
-     )
-
+      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 out_1 = nn_1@@perturbed_e in
+        let out_2 = nn_2@@perturbed_e in
+        .- delta .<= out_1[0] .- out_2[0] .<= delta
+    )
 
 end

examples/mnist/splitted_nn.mlw → examples/onnx_rewrite/sequencing.mlw

-theory MNIST
+theory SEQUENCING
 
-  use caisar.types.Vector
   use ieee_float.Float64
   use caisar.types.Float64WithBounds as Feature
   use caisar.types.IntWithBounds as Label
+  use caisar.types.Vector
   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 model_filename_1: string
+  constant model_filename_2: 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) }
+  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
+  goal sequencing:
+    let nn_1 = read_model model_filename_1 in
+    let nn_2 = read_model model_filename_2 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]
-     )
-
+      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 out_1 = nn_1@@perturbed_e in
+        let out_2 = nn_2@@out_1 in
+        forall j. Label.valid label_bounds j -> j <> l ->
+        out_2[l] .>= out_2[j]
+    )
 
 end

tests/check_pruning.t

-  $ . ./setup_env.sh
-
-  $ ls ../examples/
-  acasxu
-  mnist
-
-#  $ caisar verify --prover PyRAT  --ltag=StackTrace --define model_filename:nets/pruned/FNN_28x28_s42.onnx --define pruned_model_filename:nets/pruned/FNN_28x28_pruned_s42.onnx --define dataset_filename:csv/single_image.csv ../examples/mnist/check_pruning.mlw -v

tests/comparison.t

+  $ . ./setup_env.sh
+
+  $ ls ../examples/
+  acasxu
+  mnist
+  onnx_rewrite
+
+  $ caisar verify --prover PyRAT --define model_filename_1:../mnist/nets/pruned/FNN_28x28_s42.onnx --define model_filename_2:../mnist/nets/pruned/FNN_28x28_pruned_s42.onnx --define dataset_filename:../mnist/csv/single_image.csv ../examples/onnx_rewrite/comparison.mlw -v
+  [INFO] Verification results for theory 'COMPARISON'
+  Goal comparison: Unknown ()

tests/dune

 (cram
  (alias local)
- (applies_to * \ nir_to_onnx acasxu_ci arithmetic check_pruning splited_nn)
+ (applies_to * \ nir_to_onnx acasxu_ci arithmetic comparison sequencing)
  (deps
   (package caisar)
   setup_env.sh
@@ -29,13 +29,13 @@
 
  (cram
  (alias local)
- (applies_to check_pruning)
+ (applies_to comparison)
  (deps
   (package caisar)
   setup_env.sh
   (glob_files bin/*)
   filter_tmpdir.sh
-  ../examples/mnist/check_pruning.mlw
+  ../examples/onnx_rewrite/comparison.mlw
   ../examples/mnist/nets/pruned/FNN_28x28_s42.onnx
   ../examples/mnist/nets/pruned/FNN_28x28_pruned_s42.onnx
   ../examples/mnist/csv/single_image.csv
@@ -44,13 +44,13 @@
 
  (cram
  (alias local)
- (applies_to splitted_nn)
+ (applies_to sequencing)
  (deps
   (package caisar)
   setup_env.sh
   (glob_files bin/*)
   filter_tmpdir.sh
-  ../examples/mnist/splitted_nn.mlw
+  ../examples/onnx_rewrite/sequencing.mlw
   ../examples/mnist/nets/splitted/FNN_28x28_pre_s42.onnx
   ../examples/mnist/nets/splitted/FNN_28x28_post_s42.onnx
   ../examples/mnist/csv/single_image.csv

tests/sequencing.t

+  $ . ./setup_env.sh
+
+  $ ls ../examples/
+  acasxu
+  mnist
+  onnx_rewrite
+
+  $ caisar verify --prover PyRAT --define model_filename_1:../mnist/nets/splitted/FNN_28x28_pre_s42.onnx --define model_filename_2:../mnist/nets/splitted/FNN_28x28_post_s42.onnx --define dataset_filename:../mnist/csv/single_image.csv ../examples/onnx_rewrite/sequencing.mlw -v
+  [INFO] Verification results for theory 'SEQUENCING'
+  Goal sequencing: Unknown ()

tests/splitted_nn.t

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