From fd4f4338f418ff6b7dc22d3519457d201303414d Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 19 Feb 2024 14:41:09 +0100
Subject: [PATCH] [stdlib] Rework organization of stdlib.
---
src/interpretation.ml | 9 ++---
src/language.ml | 6 ++--
stdlib/caisar.mlw | 15 --------
stdlib/dataset.mlw | 42 ++++++++++++++++++++++
stdlib/dune | 2 +-
stdlib/nn.mlw | 37 +++++++++++++++++++
stdlib/robustness.mlw | 29 +++++++++++++++
stdlib/{interpretation.mlw => vector.mlw} | 43 ++++++++---------------
tests/goal.t | 8 ++---
tests/interpretation_acasxu.t | 4 +--
tests/interpretation_dataset.t | 6 ++--
tests/marabou.t | 4 +--
tests/nier_to_onnx.t | 4 +--
tests/pyrat.t | 4 +--
tests/pyrat_onnx.t | 4 +--
15 files changed, 147 insertions(+), 70 deletions(-)
create mode 100644 stdlib/dataset.mlw
create mode 100644 stdlib/nn.mlw
create mode 100644 stdlib/robustness.mlw
rename stdlib/{interpretation.mlw => vector.mlw} (81%)
diff --git a/src/interpretation.ml b/src/interpretation.ml
index 5886078..92469b0 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 9e8f400..39ea448 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 3ee65d6..ecae235 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 0000000..06aa7bb
--- /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 101848f..eea0f53 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 0000000..b04f432
--- /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 0000000..c012769
--- /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 031993d..993b0da 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 3a7302e..830c03d 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 11080ff..a809819 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 083b106..64786e2 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 e79433a..318f520 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 08b3a30..775bb14 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 85acd38..021459c 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 5d2be1d..89a35bc 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
>
--
GitLab