[new release] caisar (4.0)

CHANGES:

- [nir] Add support for Double datatype for ONNX.

- [nir] Add quantized operators support for ONNX. This allows parsing and
  specifying properties on quantized networks within CAISAR.

- [api] Offers serialization of CAISAR to verification and configuration
  queries. It is now possible to call CAISAR using JSON values and collect
  CAISAR outputs from the outside. This lays the foundations for developping
  APIs in different languages, or to call CAISAR remotely.

- [interpretation] Add supports computing substractions of same-length
  vectors.

- [interpretation] Add better handling of vectorization. This allows for writing more compact specifications.

- [interpretation] Add support for computing the length of a vector which
  was computed on the application of a neural network.

- [prover] Add support for timeouts in nnenum.

- [svm] Allows fully transforming Support Vector Machines as a NIR, allowing to
  leverage the full range of CAISAR supported provers to verify specifications
  with SVMs.

- [doc] Updating documentation with examples on checking a property on SVMs.

Author: caisar-platform

packages/caisar/caisar.4.0/opam

@@ -0,0 +1,65 @@
+opam-version: "2.0"
+synopsis:
+  "A platform for characterizing the safety and robustness of artificial intelligence based software"
+maintainer: ["AISER team, Software Safety and Security Laboratory, CEA-List"]
+authors: ["AISER team, Software Safety and Security Laboratory, CEA-List"]
+license: "LGPL-2.1-only"
+homepage: "https://git.frama-c.com/pub/caisar"
+doc: "https://git.frama-c.com/pub/caisar"
+bug-reports: "https://git.frama-c.com/pub/caisar/issues"
+depends: [
+  "dune" {>= "3.12"}
+  "ocaml" {>= "4.14"}
+  "dune-site" {>= "2.9.0"}
+  "zarith" {>= "1.7"}
+  "ocplib-endian" {>= "1.0"}
+  "base" {>= "v0.16.0"}
+  "stdio" {>= "v0.14.0"}
+  "cmdliner" {>= "1.1.1"}
+  "fmt" {>= "0.8.9"}
+  "logs" {>= "0.7.0"}
+  "yojson" {>= "1.7.0"}
+  "menhirLib" {>= "20210310"}
+  "csv" {>= "2.4"}
+  "why3" {>= "1.7.0" & < "1.8.0"}
+  "re" {>= "1.12.0"}
+  "fpath" {>= "0.7.3"}
+  "yaml" {>= "3.1.0"}
+  "ocaml-protoc-plugin" {>= "4.2.0"}
+  "stdio" {>= "v0.14.0"}
+  "ocamlgraph" {>= "1.8.8"}
+  "ppx_deriving" {>= "5.1"}
+  "ppx_inline_test" {>= "0.12.0"}
+  "conf-jq" {>= "1" & with-test}
+  "conf-texlive" {>= "1" & with-test}
+  "conf-python-3" {>= "9.0.0" & with-test}
+  "ppx_deriving_yojson" {>= "3.6.1"}
+  "ppx_deriving_yaml" {>= "0.3.0"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+dev-repo: "git+https://git.frama-c.com/pub/caisar.git"
+url {
+  src:
+    "https://git.frama-c.com/api/v4/projects/1082/packages/generic/caisar/4.0/caisar-4.0.tbz"
+  checksum: [
+    "sha256=58ba1e38721795b306c860b56aaeba971be586cd55fb96e3ec8af72dd005101b"
+    "sha512=f1b3b9899660745598cebe7ecb52a39e9e16dcb7352381ea75a80d2afa988437130c00bf66355991421d4cb3dc06b02c185f7d4bdcc1c86dfcde8084bd01a654"
+  ]
+}
+x-commit-hash: "7ef52531d6274266c979cb9d4bf643f96c49dc2d"