diff --git a/examples/acasxu/acasxu.why b/examples/acasxu/acasxu.why
index e81f0fe6bd15019f59257a62b11e043249d1d732..1c438605cb3ebfb92a6ccf77f2bbf6dbfa6d6c32 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 1ea347b25c742d6ca390ecf8a380826fd3ace9f8..1b87bf70c3b38d7a1bba967b0e99636bb9556750 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 cebfcb73b59cc0674c8d7d689be11a85dd16ae74..456b9c4074e0bb421a8c756049a0200700883c20 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 8ac34c1f78962fbe1879cc81820964ec597f7a04..f5379b1ee2ac01e6f0382368f8d5174beeb56de1 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 36eb79ad5d1f8cc5a5d7ff7bbf6397651b669e39..c91668f83b1396db9a0b5301c2d675a06949861f 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 5b6ffda2752377bed92e86ac964d3c370cf8d66a..a4ec18d989d91c83846b2154a36d96b6c8f94416 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 a5b6cf2e68cf086b5a775e3584a681f7fd946049..d9cc3e609e4ca1f996d48c1510ac24094e564ae2 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 fbb73b12c7e3077efadf75aef7c86240b96aeed5..6a1ebe929952ae3ebe9367506dcc9fc82da46bb8 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 82d489d24e7412c1ca455651d80c05665768156c..7720c47ba3d1cec2b73d6b9eaa4165578aceb8e8 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 625378a25e5715541096df1d340ea6475d30d5bc..4d4b38cdf1956f7211a954b17518de5e16546b63 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 df6db962d3f4670a26e816042780970d5535e7c4..e14070843e20e1ecea65563101d97339ffa3ff7c 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 7cea67f14091095a22033a7e5f5de9b4d38778e5..f95f5e184c7a80eb6d0e5af030680e2f52d9a995 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 92b2b89aa01219d720ac7e05081bfc04ab573c80..b144295313ab27e35c58a52b381dc0bbbaac1b6b 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 a53221efb04d51fcfc177da81410e5a76b547740..602ca57c3a6af1f2c483d59d5a212d884e7ce1aa 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 7fa35114dce7dc6cf673e426a3b4d41b3f813202..7314a569e85713fd9ea92eedec0f9f39963defda 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 78d91f74a47aba6373a7b0c0ef1bb52bebc564e8..61946b96fef743f4714ee9d46e3c4ab7cff6c5d0 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
>