diff --git a/src/interpretation.ml b/src/interpretation.ml
index 5886078cad58765d958db1f64d8c4443a61b4178..92469b02985e9578e59b8ba5770a6e5dacc197af 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -300,7 +300,7 @@ let caisar_builtins : caisar_env CRE.built_in_theories list =
in
[
- ( [ "interpretation" ],
+ ( [ "vector" ],
"Vector",
[],
[
@@ -309,17 +309,14 @@ let caisar_builtins : caisar_env CRE.built_in_theories list =
([ "length" ], None, vlength);
([ "mapi" ], None, vmapi);
] );
- ( [ "interpretation" ],
+ ( [ "nn" ],
"NeuralNetwork",
[],
[
([ "read_neural_network" ], None, read_neural_network);
([ Ident.op_infix "@@" ], None, apply_neural_network);
] );
- ( [ "interpretation" ],
- "Dataset",
- [],
- [ ([ "read_dataset" ], None, read_dataset) ] );
+ ([ "dataset" ], "Dataset", [], [ ([ "read_dataset" ], None, read_dataset) ]);
]
let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
diff --git a/src/language.ml b/src/language.ml
index 9e8f400a135ac2d0a1017a0b92db7b3def55ffed..39ea448fdd30a21a0ce535b4ba270c236410dd66 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -165,7 +165,7 @@ let float64_t_ty env =
Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) []
let vector_ty env ty_elt =
- let th = Env.read_theory env [ "interpretation" ] "Vector" in
+ let th = Env.read_theory env [ "vector" ] "Vector" in
Ty.ty_app (Theory.ns_find_ts th.th_export [ "vector" ]) [ ty_elt ]
let create_vector =
@@ -199,7 +199,7 @@ let nets = Term.Hls.create 10
let fresh_nn_ls env name =
let ty =
- let th = Env.read_theory env [ "interpretation" ] "NeuralNetwork" in
+ let th = Env.read_theory env [ "nn" ] "NeuralNetwork" in
Ty.ty_app (Theory.ns_find_ts th.th_export [ "nn" ]) []
in
let id = Ident.id_fresh name in
@@ -270,7 +270,7 @@ let datasets = Term.Hls.create 10
let fresh_dataset_csv_ls env name =
let ty =
let ty_elt = vector_ty env (float64_t_ty env) in
- let th = Env.read_theory env [ "interpretation" ] "Dataset" in
+ let th = Env.read_theory env [ "dataset" ] "Dataset" in
Ty.ty_app
(Theory.ns_find_ts th.th_export [ "dataset" ])
[ Ty.ty_int; ty_elt ]
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 3ee65d62b90286f4ba18d4981f7e1912e1226224..ecae2359d5c639cbe8c76aba4ec1eaff75276f7d 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -83,18 +83,3 @@ theory NN
function relu (a: t): t = if a .> (0.0:t) then a else (0.0:t)
end
-
-theory Interpretation
- use bool.Bool
- use int.Int
-
- type input
- type dataset
-
- function open_dataset string: dataset
- function size dataset: int
-
- function get (i:int) (d:dataset) : input
-
- predicate forall_ (d: dataset) (f: input -> bool) = forall i:int. -1 < i < size d -> f (get i d)
-end
diff --git a/stdlib/dataset.mlw b/stdlib/dataset.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..06aa7bb5592f20fde3bdb5b4254f3fabe8b64bae
--- /dev/null
+++ b/stdlib/dataset.mlw
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* You can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** {1 Datasets} *)
+
+(** {2 Generic Datasets} *)
+
+theory Dataset
+
+ use vector.Vector
+
+ type dataset 'a 'b = vector ('a, 'b)
+ type format = CSV
+
+ function read_dataset (f: string) (k: format) : dataset 'a 'b
+
+ predicate forall_ (d: dataset 'a 'b) (f: 'a -> 'b -> bool) =
+ Vector.forall_ d (fun e -> let a, b = e in f a b)
+
+ function foreach (d: dataset 'a 'b) (f: 'a -> 'b -> 'c) : vector 'c =
+ Vector.foreach d (fun e -> let a, b = e in f a b)
+
+end
diff --git a/stdlib/dune b/stdlib/dune
index 101848f1f63dc2119534b1b5593450ea8a141f2b..eea0f532c6a41e8387a9b848c144a8d0bef64a3f 100644
--- a/stdlib/dune
+++ b/stdlib/dune
@@ -2,5 +2,5 @@
(section
(site
(caisar stdlib)))
- (files caisar.mlw interpretation.mlw)
+ (files caisar.mlw vector.mlw nn.mlw dataset.mlw)
(package caisar))
diff --git a/stdlib/nn.mlw b/stdlib/nn.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..b04f432c5c53612e35b24d4d589e265eb44a0ccb
--- /dev/null
+++ b/stdlib/nn.mlw
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* You can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** {1 Neural Networks} *)
+
+(** {2 Generic Neural Networks} *)
+
+theory NeuralNetwork
+
+ use vector.Vector
+
+ type nn
+ type format = ONNX | NNet
+
+ function read_neural_network (n: string) (f: format) : nn
+ function (@@) (n: nn) (v: vector 'a) : vector 'a
+
+end
\ No newline at end of file
diff --git a/stdlib/robustness.mlw b/stdlib/robustness.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..c0127693e1777708b359cd018f50e8e50026caaf
--- /dev/null
+++ b/stdlib/robustness.mlw
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* You can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** {1 Robustness} *)
+
+(** {2 Dataset Robustness} *)
+
+theory DatasetRobustness
+
+end
\ No newline at end of file
diff --git a/stdlib/interpretation.mlw b/stdlib/vector.mlw
similarity index 81%
rename from stdlib/interpretation.mlw
rename to stdlib/vector.mlw
index 031993d7272b4b2cccfa584985d97ac17a33cac8..993b0da1292475fc7f48b1548ea16c31fb8ffe4e 100644
--- a/stdlib/interpretation.mlw
+++ b/stdlib/vector.mlw
@@ -20,7 +20,16 @@
(* *)
(**************************************************************************)
+(** {1 Vectors} *)
+
+(** {2 Generic Vectors}
+
+A generic vector can be thought of as representing a fixed-length array.
+
+*)
+
theory Vector
+
use int.Int
type vector 'a
@@ -28,7 +37,9 @@ theory Vector
function ([]) (v: vector 'a) (i: index) : 'a
function length (v: vector 'a) : int
+
function (-) (v1: vector 'a) (v2: vector 'a) : vector 'a
+ function (+) (v1: vector 'a) (v2: vector 'a) : vector 'a
predicate has_length (v: vector 'a) (i: int)
predicate valid_index (v: vector 'a) (i: index) = 0 <= i < length v
@@ -40,37 +51,13 @@ theory Vector
predicate forall_ (v: vector 'a) (f: 'a -> bool) =
forall i: index. valid_index v i -> f v[i]
- predicate forall2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> bool) =
- length(v1) = length(v2) -> forall i: index. valid_index v1 i -> f v1[i] v2[i]
-
function foreach (v: vector 'a) (f: 'a -> 'b) : vector 'b =
map v f
+ predicate forall2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> bool) =
+ length(v1) = length(v2) -> forall i: index. valid_index v1 i -> f v1[i] v2[i]
+
function foreach2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c =
map2 v1 v2 f
-end
-
-theory NeuralNetwork
- use Vector
-
- type nn
- type format = ONNX | NNet
-
- function read_neural_network (n: string) (f: format) : nn
- function (@@) (n: nn) (v: vector 'a) : vector 'a
-end
-
-theory Dataset
- use Vector
-
- type dataset 'a 'b = vector ('a, 'b)
- type format = CSV
-
- function read_dataset (f: string) (k: format) : dataset 'a 'b
-
- predicate forall_ (d: dataset 'a 'b) (f: 'a -> 'b -> bool) =
- Vector.forall_ d (fun e -> let a, b = e in f a b)
- function foreach (d: dataset 'a 'b) (f: 'a -> 'b -> 'c) : vector 'c =
- Vector.foreach d (fun e -> let a, b = e in f a b)
-end
+end
\ No newline at end of file
diff --git a/tests/goal.t b/tests/goal.t
index 3a7302e5ab02248573dafd10254908594c760d65..830c03dd737ca13f696a1b84df1e9f584402f875 100644
--- a/tests/goal.t
+++ b/tests/goal.t
@@ -9,8 +9,8 @@ Test verify
> use ieee_float.Float64
> use bool.Bool
> use int.Int
- > use interpretation.Vector
- > use interpretation.NeuralNetwork
+ > use vector.Vector
+ > use nn.NeuralNetwork
>
> constant nn: nn = read_neural_network "TestNetwork.nnet" NNet
>
@@ -36,8 +36,8 @@ Test verify
> use ieee_float.Float64
> use bool.Bool
> use int.Int
- > use interpretation.Vector
- > use interpretation.NeuralNetwork
+ > use vector.Vector
+ > use nn.NeuralNetwork
>
> constant nn: nn = read_neural_network "TestNetwork.nnet" NNet
>
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 11080ff1a14afd138901ecd8cbbd46ca43c04037..a80981939c156d31af70d001e5be233631c16e76 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -9,8 +9,8 @@ Test interpret on acasxu
> use ieee_float.Float64
> use bool.Bool
> use int.Int
- > use interpretation.Vector
- > use interpretation.NeuralNetwork
+ > use vector.Vector
+ > use nn.NeuralNetwork
>
> constant nn: nn = read_neural_network "TestNetwork.nnet" NNet
>
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index 083b106ee2a19626c3ebb5fe0075e09dd45b466b..64786e2ffd05a9885f82a12e4d8ea09b7beb4a4a 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -13,9 +13,9 @@ Test interpret on dataset
> theory T
> use ieee_float.Float64
> use int.Int
- > use interpretation.Vector
- > use interpretation.NeuralNetwork
- > use interpretation.Dataset
+ > use vector.Vector
+ > use nn.NeuralNetwork
+ > use dataset.Dataset
>
> type image = vector t
> type label_ = int
diff --git a/tests/marabou.t b/tests/marabou.t
index e79433ad986881f07570b2d174fe5bca522a49f9..318f5202c863de736505181cc8cf6b3af736e3a8 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -9,8 +9,8 @@ Test verify
> use ieee_float.Float64
> use bool.Bool
> use int.Int
- > use interpretation.Vector
- > use interpretation.NeuralNetwork
+ > use vector.Vector
+ > use nn.NeuralNetwork
>
> constant nn: nn = read_neural_network "TestNetwork.nnet" NNet
>
diff --git a/tests/nier_to_onnx.t b/tests/nier_to_onnx.t
index 08b3a30b0b220d7868561500849e31a62a0c86d6..775bb1467ae3939257ef514bb330f27816fc96cb 100644
--- a/tests/nier_to_onnx.t
+++ b/tests/nier_to_onnx.t
@@ -9,8 +9,8 @@ Test verify
> use ieee_float.Float64
> use bool.Bool
> use int.Int
- > use interpretation.Vector
- > use interpretation.NeuralNetwork
+ > use vector.Vector
+ > use nn.NeuralNetwork
>
> constant nn: nn = read_neural_network "TestNetworkONNX.onnx" ONNX
>
diff --git a/tests/pyrat.t b/tests/pyrat.t
index 85acd3882f06b2b8fa4ca953a9966bb7097e5788..021459cd7c72e8284fb54fa8901b543ec47d4289 100644
--- a/tests/pyrat.t
+++ b/tests/pyrat.t
@@ -10,8 +10,8 @@ Test verify
> use ieee_float.Float64
> use bool.Bool
> use int.Int
- > use interpretation.Vector
- > use interpretation.NeuralNetwork
+ > use vector.Vector
+ > use nn.NeuralNetwork
>
> constant nn: nn = read_neural_network "TestNetwork.nnet" NNet
>
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index 5d2be1db6d59913d4c88db07b36dfaeabb95d0d7..89a35bc4155c2af43f113f87a50d97a90db9260e 100644
--- a/tests/pyrat_onnx.t
+++ b/tests/pyrat_onnx.t
@@ -9,8 +9,8 @@ Test verify
> use ieee_float.Float64
> use bool.Bool
> use int.Int
- > use interpretation.Vector
- > use interpretation.NeuralNetwork
+ > use vector.Vector
+ > use nn.NeuralNetwork
>
> constant nn: nn = read_neural_network "TestNetworkONNX.onnx" ONNX
>