diff --git a/examples/mnist/check_pruning.mlw b/examples/mnist/check_pruning.mlw
deleted file mode 100644
index 37f3fc9ceb8ff9858de9b1ef3bb8c69f5b60162a..0000000000000000000000000000000000000000
--- a/examples/mnist/check_pruning.mlw
+++ /dev/null
@@ -1,40 +0,0 @@
-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 model_filename: string
- constant pruned_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 nn = read_model model_filename in
- let pruned_nn = read_model pruned_model_filename 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
- )
-
-
-end
diff --git a/examples/mnist/splitted_nn.mlw b/examples/mnist/splitted_nn.mlw
deleted file mode 100644
index 6afbfd5f364bf279e745d327e1eb23360a63e5d7..0000000000000000000000000000000000000000
--- a/examples/mnist/splitted_nn.mlw
+++ /dev/null
@@ -1,40 +0,0 @@
-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
diff --git a/examples/onnx_rewrite/comparison.mlw b/examples/onnx_rewrite/comparison.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..c56c3d599c6d7f3eb801899b82e0c722ef7c92bd
--- /dev/null
+++ b/examples/onnx_rewrite/comparison.mlw
@@ -0,0 +1,36 @@
+theory COMPARISON
+
+ 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_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) }
+
+ 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_1 = nn_1@@perturbed_e in
+ let out_2 = nn_2@@perturbed_e in
+ .- delta .<= out_1[0] .- out_2[0] .<= delta
+ )
+
+end
diff --git a/examples/onnx_rewrite/sequencing.mlw b/examples/onnx_rewrite/sequencing.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..a3a03cf7ccd0e3bb3747e345f7a08de78bdea117
--- /dev/null
+++ b/examples/onnx_rewrite/sequencing.mlw
@@ -0,0 +1,36 @@
+theory SEQUENCING
+
+ 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_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) }
+
+ 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 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
diff --git a/tests/check_pruning.t b/tests/check_pruning.t
deleted file mode 100644
index a74ec0cd0af6562127da5bb4e7fb0877260fb7e8..0000000000000000000000000000000000000000
--- a/tests/check_pruning.t
+++ /dev/null
@@ -1,7 +0,0 @@
- $ . ./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
diff --git a/tests/comparison.t b/tests/comparison.t
new file mode 100644
index 0000000000000000000000000000000000000000..a901ae8bbbb9a7e9d8dfa9445d0b74c22541048a
--- /dev/null
+++ b/tests/comparison.t
@@ -0,0 +1,10 @@
+ $ . ./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 ()
diff --git a/tests/dune b/tests/dune
index 704b446aa99c0472b0e75b6acf4216e9e64add84..57ad5a8b44642c58d7b71467d5250f22bfb4ae90 100644
--- a/tests/dune
+++ b/tests/dune
@@ -1,6 +1,6 @@
(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
diff --git a/tests/sequencing.t b/tests/sequencing.t
new file mode 100644
index 0000000000000000000000000000000000000000..90676de048b7b3b4230fc3983428cfa4de113361
--- /dev/null
+++ b/tests/sequencing.t
@@ -0,0 +1,10 @@
+ $ . ./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 ()
diff --git a/tests/splitted_nn.t b/tests/splitted_nn.t
deleted file mode 100644
index 611987d8b77d3e8eef7787157005643b99fa8bf0..0000000000000000000000000000000000000000
--- a/tests/splitted_nn.t
+++ /dev/null
@@ -1,7 +0,0 @@
- $ . ./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