From e0f14dfec256ca03a1a29b2ffe0e39774baf71cf Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 15 Mar 2024 09:39:48 +0100
Subject: [PATCH] [stdlib] Add basic types to obtain most specification reuse
possible.
---
examples/acasxu/acasxu.why | 3 +-
examples/mnist/mnist.why | 21 ++++-----
src/interpretation.ml | 2 +-
src/language.ml | 2 +-
stdlib/dataset.mlw | 19 +++-----
stdlib/dune | 2 +-
stdlib/model.mlw | 2 +-
stdlib/robust.mlw | 41 ++++++++---------
stdlib/{vector.mlw => types.mlw} | 75 +++++++++++++++++++++++++++++++-
tests/acasxu.t | 3 +-
tests/dataset.t | 19 +++-----
tests/goal.t | 8 +---
tests/marabou.t | 4 +-
tests/nier_to_onnx.t | 4 +-
tests/pyrat.t | 5 +--
tests/pyrat_onnx.t | 4 +-
16 files changed, 127 insertions(+), 87 deletions(-)
rename stdlib/{vector.mlw => types.mlw} (70%)
diff --git a/examples/acasxu/acasxu.why b/examples/acasxu/acasxu.why
index e81f0fe..1c43860 100644
--- a/examples/acasxu/acasxu.why
+++ b/examples/acasxu/acasxu.why
@@ -9,9 +9,8 @@ theory ACASXU
*)
use ieee_float.Float64
- use bool.Bool
use int.Int
- use vector.Vector
+ use types.Vector
use model.Model
use model.NN
diff --git a/examples/mnist/mnist.why b/examples/mnist/mnist.why
index 1ea347b..1b87bf7 100644
--- a/examples/mnist/mnist.why
+++ b/examples/mnist/mnist.why
@@ -1,7 +1,8 @@
theory MNIST
use ieee_float.Float64
- use int.Int
+ use types.Float64WithBounds as Feature
+ use types.IntWithBounds as Label
use model.Model
use model.NN
use dataset.CSV
@@ -10,22 +11,16 @@ theory MNIST
constant model_filename: string
constant dataset_filename: string
- constant min_feature_value: t = (0.0:t)
- constant max_feature_value: t = (1.0:t)
-
- constant min_label : label_ = 0
- constant max_label : label_ = 9
-
- predicate valid_features (e: features) =
- CSV.valid_features min_feature_value max_feature_value e
-
- predicate valid_label (l: label_) =
- CSV.valid_label min_label max_label l
+ 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 robustness:
let nn = read_model model_filename in
let dataset = read_dataset dataset_filename in
let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
- robust valid_features valid_label nn dataset eps
+ robust feature_bounds label_bounds nn dataset eps
end
diff --git a/src/interpretation.ml b/src/interpretation.ml
index cebfcb7..456b9c4 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -375,7 +375,7 @@ let caisar_builtins : caisar_env CRE.built_in_theories list =
in
[
- ( [ "vector" ],
+ ( [ "types" ],
"Vector",
[],
[
diff --git a/src/language.ml b/src/language.ml
index 8ac34c1..f5379b1 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -165,7 +165,7 @@ let ty_float64_t env =
Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) []
let ty_vector env ty_elt =
- let th = Env.read_theory env [ "vector" ] "Vector" in
+ let th = Env.read_theory env [ "types" ] "Vector" in
Ty.ty_app (Theory.ns_find_ts th.th_export [ "vector" ]) [ ty_elt ]
let create_vector =
diff --git a/stdlib/dataset.mlw b/stdlib/dataset.mlw
index 36eb79a..c91668f 100644
--- a/stdlib/dataset.mlw
+++ b/stdlib/dataset.mlw
@@ -26,7 +26,7 @@
theory Dataset
- use vector.Vector
+ use types.Vector
type a
type b
@@ -52,23 +52,14 @@ A dataset in CSV format is such that each element is given as:
theory CSV
- use int.Int
- use ieee_float.Float64
- use vector.Vector
+ use types.IntWithBounds as Label
+ use types.VectorFloat64 as FeatureVector
- type label_ = int
- type features = vector t
+ type label_ = Label.t
+ type features = FeatureVector.t
clone export Dataset with type a = label_, type b = features
- predicate valid_label (min_label: label_) (max_label: label_) (l: label_) =
- min_label <= l <= max_label
-
- predicate valid_features (min_feature_value: t) (max_feature_value: t)
- (e: features) =
- forall v: index. valid_index e v ->
- min_feature_value .<= e[v] .<= max_feature_value
-
function infer_min_label (d: dataset) : label_
function infer_max_label (d: dataset) : label_
diff --git a/stdlib/dune b/stdlib/dune
index 5b6ffda..a4ec18d 100644
--- a/stdlib/dune
+++ b/stdlib/dune
@@ -2,5 +2,5 @@
(section
(site
(caisar stdlib)))
- (files caisar.mlw robust.mlw vector.mlw model.mlw dataset.mlw)
+ (files caisar.mlw types.mlw robust.mlw model.mlw dataset.mlw)
(package caisar))
diff --git a/stdlib/model.mlw b/stdlib/model.mlw
index a5b6cf2..d9cc3e6 100644
--- a/stdlib/model.mlw
+++ b/stdlib/model.mlw
@@ -26,7 +26,7 @@
theory Model
- use vector.Vector
+ use types.Vector
type kind
type model 'kind
diff --git a/stdlib/robust.mlw b/stdlib/robust.mlw
index fbb73b1..6a1ebe9 100644
--- a/stdlib/robust.mlw
+++ b/stdlib/robust.mlw
@@ -27,31 +27,31 @@
theory ClassRobustVector
use ieee_float.Float64
- use int.Int
- use vector.Vector
use model.Model
+ use types.Float64WithBounds as Feature
+ use types.IntWithBounds as Label
+ use types.Vector
+ use types.VectorFloat64 as FeatureVector
- type features = vector t
- type label_ = int
-
- predicate bounded_by_epsilon (e: features) (eps: t) =
+ predicate bounded_by_epsilon (e: FeatureVector.t) (eps: t) =
forall i: index. valid_index e i -> .- eps .<= e[i] .<= eps
- predicate advises (valid_label_: label_ -> bool)
- (m: model 'm) (e: features) (l: label_) =
- valid_label_ l ->
- forall j. valid_label_ j -> j <> l ->
+ predicate advises (label_bounds: Label.bounds) (m: model 'm)
+ (e: FeatureVector.t) (l: Label.t) =
+ Label.valid label_bounds l ->
+ forall j. Label.valid label_bounds j -> j <> l ->
(m @@ e)[l] .>= (m @@ e)[j]
- predicate robust (valid_features: features -> bool)
- (valid_label_: label_ -> bool)
- (m: model 'm) (eps: t) (l: label_) (e: features) =
- forall perturbed_e: vector t.
+ predicate robust (feature_bounds: Feature.bounds)
+ (label_bounds: Label.bounds)
+ (m: model 'm) (eps: t)
+ (l: Label.t) (e: FeatureVector.t) =
+ forall perturbed_e: FeatureVector.t.
has_length perturbed_e (length e) ->
- valid_features perturbed_e ->
+ FeatureVector.valid feature_bounds perturbed_e ->
let perturbation = perturbed_e - e in
bounded_by_epsilon perturbation eps ->
- advises valid_label_ m perturbed_e l
+ advises label_bounds m perturbed_e l
end
@@ -60,14 +60,15 @@ end
theory ClassRobustCSV
use ieee_float.Float64
- use int.Int
+ use types.Float64WithBounds as Feature
+ use types.IntWithBounds as Label
use model.Model
use dataset.CSV
use ClassRobustVector
- predicate robust (valid_features: features -> bool)
- (valid_label: label_ -> bool)
+ predicate robust (feature_bounds: Feature.bounds)
+ (label_bounds: Label.bounds)
(m: model 'a) (d: dataset) (eps: t) =
- CSV.forall_ d (ClassRobustVector.robust valid_features valid_label m eps)
+ CSV.forall_ d (ClassRobustVector.robust feature_bounds label_bounds m eps)
end
diff --git a/stdlib/vector.mlw b/stdlib/types.mlw
similarity index 70%
rename from stdlib/vector.mlw
rename to stdlib/types.mlw
index 82d489d..7720c47 100644
--- a/stdlib/vector.mlw
+++ b/stdlib/types.mlw
@@ -20,7 +20,52 @@
(* *)
(**************************************************************************)
-(** {1 Vectors} *)
+(** {1 Basic Types} *)
+
+(** {2 Generic Types with Bounds}
+
+A generic type with bounds determining minimal and maximal value.
+
+*)
+
+theory WithBounds
+
+ type t
+ type bounds = { lower: t; upper: t }
+
+ predicate le (t1: t) (t2: t)
+
+ predicate valid (b: bounds) (t: t) =
+ le b.lower t /\ le t b.upper
+
+end
+
+(** {2 Int with Bounds} *)
+
+theory IntWithBounds
+
+ use int.Int
+
+ type t = int
+ clone export WithBounds with
+ type t = t, predicate le = (<=)
+
+end
+
+(** {2 IEEE Float64 with Bounds} *)
+
+theory Float64WithBounds
+
+ use ieee_float.Float64
+
+ type t = Float64.t
+ clone export WithBounds with
+ type t = t, predicate le = (.<=)
+
+end
+
+
+(** {1 Vector Types} *)
(** {2 Generic Vectors}
@@ -61,3 +106,31 @@ theory Vector
map2 v1 v2 f
end
+
+(** {2 Vectors of Int} *)
+
+theory VectorInt
+
+ use IntWithBounds
+ use Vector
+
+ type t = vector IntWithBounds.t
+
+ predicate valid (b: IntWithBounds.bounds) (v: t) =
+ Vector.forall_ v (IntWithBounds.valid b)
+
+end
+
+(** {2 Vectors of IEEE Float64} *)
+
+theory VectorFloat64
+
+ use Float64WithBounds
+ use Vector
+
+ type t = vector Float64WithBounds.t
+
+ predicate valid (b: Float64WithBounds.bounds) (v: t) =
+ Vector.forall_ v (Float64WithBounds.valid b)
+
+end
diff --git a/tests/acasxu.t b/tests/acasxu.t
index 625378a..4d4b38c 100644
--- a/tests/acasxu.t
+++ b/tests/acasxu.t
@@ -7,9 +7,8 @@ Test verify on acasxu
$ cat > file.mlw <<EOF
> theory T
> use ieee_float.Float64
- > use bool.Bool
> use int.Int
- > use vector.Vector
+ > use types.Vector
> use model.Model
> use model.NN
>
diff --git a/tests/dataset.t b/tests/dataset.t
index df6db96..e140708 100644
--- a/tests/dataset.t
+++ b/tests/dataset.t
@@ -15,28 +15,23 @@ Test verify on dataset
$ cat > file.mlw << EOF
> theory T
> use ieee_float.Float64
- > use int.Int
+ > use types.Float64WithBounds as Feature
+ > use types.IntWithBounds as Label
> use model.NN
> use dataset.CSV
> use robust.ClassRobustCSV
>
- > constant min_feature_value: t = (0.0:t)
- > constant max_feature_value: t = (1.0:t)
+ > constant label_bounds: Label.bounds =
+ > Label.{ lower = 0; upper = 4 }
>
- > constant min_label: label_ = 0
- > constant max_label: label_ = 4
- >
- > predicate valid_features (e: features) =
- > CSV.valid_features min_feature_value max_feature_value e
- >
- > predicate valid_label (l: label_) =
- > CSV.valid_label min_label max_label l
+ > constant feature_bounds: Feature.bounds =
+ > Feature.{ lower = (0.0:t); upper = (1.0:t) }
>
> goal H:
> let nn = read_model "TestNetwork.nnet" in
> let dataset = read_dataset "dataset.csv" in
> let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
- > robust valid_features valid_label nn dataset eps
+ > robust feature_bounds label_bounds nn dataset eps
> end
> EOF
diff --git a/tests/goal.t b/tests/goal.t
index 7cea67f..f95f5e1 100644
--- a/tests/goal.t
+++ b/tests/goal.t
@@ -7,9 +7,7 @@ Test verify
$ cat > file.mlw <<EOF
> theory T1
> use ieee_float.Float64
- > use bool.Bool
- > use int.Int
- > use vector.Vector
+ > use types.Vector
> use model.Model
> use model.NN
>
@@ -35,9 +33,7 @@ Test verify
> end
> theory T2
> use ieee_float.Float64
- > use bool.Bool
- > use int.Int
- > use vector.Vector
+ > use types.Vector
> use model.Model
> use model.NN
>
diff --git a/tests/marabou.t b/tests/marabou.t
index 92b2b89..b144295 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -7,9 +7,7 @@ Test verify
$ caisar verify --format whyml --prover=Marabou --ltag=ProverSpec - <<EOF
> theory T
> use ieee_float.Float64
- > use bool.Bool
- > use int.Int
- > use vector.Vector
+ > use types.Vector
> use model.Model
> use model.NN
>
diff --git a/tests/nier_to_onnx.t b/tests/nier_to_onnx.t
index a53221e..602ca57 100644
--- a/tests/nier_to_onnx.t
+++ b/tests/nier_to_onnx.t
@@ -7,9 +7,7 @@ Test verify
$ caisar verify --format whyml --prover=PyRAT --ltag=NIER --onnx-out-dir="out" - 2>&1 <<EOF
> theory NIER_to_ONNX
> use ieee_float.Float64
- > use bool.Bool
- > use int.Int
- > use vector.Vector
+ > use types.Vector
> use model.Model
> use model.NN
>
diff --git a/tests/pyrat.t b/tests/pyrat.t
index 7fa3511..7314a56 100644
--- a/tests/pyrat.t
+++ b/tests/pyrat.t
@@ -6,11 +6,8 @@ Test verify
$ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - <<EOF
> theory PyRAT
- > use TestNetwork.AsTuple
> use ieee_float.Float64
- > use bool.Bool
- > use int.Int
- > use vector.Vector
+ > use types.Vector
> use model.Model
> use model.NN
>
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index 78d91f7..61946b9 100644
--- a/tests/pyrat_onnx.t
+++ b/tests/pyrat_onnx.t
@@ -7,9 +7,7 @@ Test verify
$ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - <<EOF
> theory PyRAT_ONNX
> use ieee_float.Float64
- > use bool.Bool
- > use int.Int
- > use vector.Vector
+ > use types.Vector
> use model.Model
> use model.NN
>
--
GitLab