[stdlib] Add basic types to obtain most specification reuse possible.

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
 

examples/mnist/mnist.why

 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

src/interpretation.ml

@@ -375,7 +375,7 @@ let caisar_builtins : caisar_env CRE.built_in_theories list =
   in
 
   [
-    ( [ "vector" ],
+    ( [ "types" ],
       "Vector",
       [],
       [

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 =

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_
 

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))

stdlib/model.mlw

@@ -26,7 +26,7 @@
 
 theory Model
 
-  use vector.Vector
+  use types.Vector
 
   type kind
   type model 'kind

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

stdlib/vector.mlw → 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

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
   > 

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
 

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
   > 

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
   > 

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
   > 

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
   > 

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
   >