From 61502514df0bbed75988fff50fcfb555b9317222 Mon Sep 17 00:00:00 2001
From: Aymeric Varasse <aymeric.varasse@cea.fr>
Date: Thu, 25 Apr 2024 18:36:29 +0200
Subject: [PATCH] [exps] Uniformize, rename and reorganize specs
---
examples/mnist/check_pruning.mlw | 40 ----------------------------
examples/mnist/splitted_nn.mlw | 40 ----------------------------
examples/onnx_rewrite/comparison.mlw | 36 +++++++++++++++++++++++++
examples/onnx_rewrite/sequencing.mlw | 36 +++++++++++++++++++++++++
tests/check_pruning.t | 7 -----
tests/comparison.t | 10 +++++++
tests/dune | 10 +++----
tests/sequencing.t | 10 +++++++
tests/splitted_nn.t | 7 -----
9 files changed, 97 insertions(+), 99 deletions(-)
delete mode 100644 examples/mnist/check_pruning.mlw
delete mode 100644 examples/mnist/splitted_nn.mlw
create mode 100644 examples/onnx_rewrite/comparison.mlw
create mode 100644 examples/onnx_rewrite/sequencing.mlw
delete mode 100644 tests/check_pruning.t
create mode 100644 tests/comparison.t
create mode 100644 tests/sequencing.t
delete mode 100644 tests/splitted_nn.t
diff --git a/examples/mnist/check_pruning.mlw b/examples/mnist/check_pruning.mlw
deleted file mode 100644
index 37f3fc9..0000000
--- 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 6afbfd5..0000000
--- 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 0000000..c56c3d5
--- /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 0000000..a3a03cf
--- /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 a74ec0c..0000000
--- 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 0000000..a901ae8
--- /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 704b446..57ad5a8 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 0000000..90676de
--- /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 611987d..0000000
--- 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
--
GitLab