Merge branch 'stable/2.0' into 'master'

Release 2.0

See merge request laiser/caisar!142

.gitlab-ci.yml

 variables:
-  CAISAR_VERSION: "1.0.0"
-  TAG: "1.0"
+  CAISAR_VERSION: "2.0.0"
+  TAG: "2.0"
 
 default:
   interruptible: true
@@ -20,7 +20,7 @@ build:
 # Optional and manual full rebuild using a clean docker image
 full_rebuild_and_test:
   stage: build
-  image: ocaml/opam@sha256:013a26ccbaa8344b63274e335e2492c432cec1c3526b9ba888ab151abb2b4c25
+  image: ocaml/opam:ubuntu-22.04-ocaml-4.13
   cache:
     key: $CI_COMMIT_REF_SLUG
     paths:
@@ -31,10 +31,11 @@ full_rebuild_and_test:
     - eval $(opam env --switch=4.13 --set-switch)
     - opam switch
     - sudo apt-get update
-    - sudo apt install -y protobuf-compiler
+    - sudo apt-get install -y protobuf-compiler python3 python3-pip cmake
     - opam repository add remote https://opam.ocaml.org
     - opam depext --yes ocplib-endian base fmt alt-ergo.2.4.0
     - opam install --jobs 2 . --deps-only --with-test --yes
+    - python3 -m pip install onnx
     - make all-ci
     - make test-ci
   tags:

CHANGES.md

+# 2.0 (17-06-2024)
+
+- [interpretation] Add transformations that allow the verification of several
+  neural network at once. Within particular patterns, CAISAR will generate
+  an ONNX file that preserve the semantic of the neural networks
+  while encapsulating parts of the
+  specification directly in the control flow of the neural network.
+  This feature allow the verification of properties with multiple neural
+  networks, including their composition.
+
+- [interpretation] Integrate SVMs into the interpretation engine. Users can
+  expect vector computations and applications on SVMs to be computed similarly
+  as what exists already for neural networks.
+
+- [interpretation] Add support for addition between vectors.
+
+- [interpretation] Add better error reporting for interpretation errors. Users
+  now get better guidance on how to write their specification. For instance,
+  CAISAR now explicitly asks for a predicate constraining the length of a vector
+  after a universal quantifier.
+
+- [language] Unified Support Vector Machines (SVMs) theories.
+  Previously, there was a separate theory for neural networks and SVMs datasets
+  and models. They are now accessible under a single theory.
+
+- [language] Add additional abstraction support for SVMs.
+
+- [language] Simplify CAISAR's Neural Intermediate Representation (NIR) and
+  perform automatic shape inference when creating a new NIR node.
+
+- [language] Add support for the following ONNX operators: `Gather`, `Log`, `Abs`,
+  `RandomNormal`, `ReduceSum`.
+
+- [language] Neural networks in NNet format are now parsed into a NIR.
+
+- [examples] Rework ACAS-Xu specification with a formulation that is closer to
+  the original. In particular, provide explicit normalization and
+  denormalization functions in the test file. Also define explicit function
+  contracts using Why3 pre and post-conditions.
+
+- [examples] Add more examples displaying CAISAR ability to handle several
+  neural networks at once.
+
+- [cmdline] Add command line option `--onnx-out-dir`
+  to output the NIR generated by CAISAR as an ONNX file.
+
+- [logging] Add command line option `--ltag` for fine-grained logging.
+  By providing a logging tag (`ltag`), users can control which part of CAISAR
+  will log its outputs.
+
+- [prover] Add support for Marabou 2.0 via its Python API. Autodetection of
+  Marabou installed through maraboupy is now supported.
+
+- [prover] Update AIMOS configuration to match upstream.
+
+- [prover] Update $\alpha-\beta-$CROWN configuration to match upstream.
+
+- [doc] Clarify the supported ONNX operator set: the ONNX Intermediate
+  Representation is version 8, the supported operator set is version 13.
+
+
 # 1.0 (08-12-2023)
 
 - [language] Extended WhyML for AI systems. It is now possible to model with

doc/conf.py

@@ -21,7 +21,7 @@ sys.path.append(os.path.abspath('./ext'))
 # -- Project information -----------------------------------------------------
 
 project = 'CAISAR'
-copyright = '2023, The CAISAR Development Team'
+copyright = '2024, The CAISAR Development Team'
 author = 'The CAISAR Development Team'
 
 # The version info for the project you're documenting, acts as replacement for
@@ -29,9 +29,9 @@ author = 'The CAISAR Development Team'
 # built documents.
 #
 # The short X.Y version.
-version = '1.0'
+version = '2.0'
 # The full version, including alpha/beta/rc tags.
-release = '1.0'
+release = '2.0'
 
 
 # -- General configuration ---------------------------------------------------

doc/contributing.rst

@@ -27,6 +27,7 @@ The root of the repository has the following folders:
 * ``stdlib/`` contains WhyML files used to define
   theories for the CAISAR interpreted language.
 * ``tests/`` are non-regression tests written in `dune cram test syntax <https://dune.readthedocs.io/en/stable/tests.html>`_.
+* ``utils/`` are helper functions used internally by CAISAR (for instance, logging utilities).
 
 
 Setting up a development environment

doc/index.rst

@@ -18,12 +18,13 @@ The CAISAR Platform
   François Bobot,
   Julien Girard
 
-:Version: |version|, December 2023
-:Copyright: 2020--2023 CEA (Commissariat à l'énergie atomique et aux énergies alternatives)
+:Version: |version|, June 2024
+:Copyright: 2020--2024 CEA (Commissariat à l'énergie atomique et aux énergies alternatives)
 
 .. _Confiance.ai: https://www.confiance.ai/
+.. _DeepGreen: https://www.deepgreen.ai/
 
-This work has been partly supported by the `Confiance.ai`_ program.
+This work has been partly supported by the `Confiance.ai`_ program and the `DeepGreen`_ project.
 
 .. toctree::
    :maxdepth: 2

doc/interpretation.rst

@@ -109,12 +109,12 @@ Functions
 
 .. code-block:: whyml
 
-  (** Returns a symbol for the neural network with filename n. **)
-  function read_model (n: string) : model nn
+  (** Returns a symbol for the machine learning model with filename n. **)
+  function read_model (n: string) : model
 
-  (** Returns a vector that represents the application of neural network
+  (** Returns a vector that represents the application of a model
   on an input vector. **)
-  function (@@) (n: model nn) (v: vector 'a) : vector 'a
+  function (@@) (n: model) (v: vector 'a) : vector 'a
 
 Dataset
 *******

docker/Dockerfile.template

@@ -76,6 +76,10 @@ cmake --build .
 
 ENV PATH "/home/opam/Marabou/build:$PATH"
 
+## Maraboupy
+
+RUN /usr/bin/python3.10 -m pip install maraboupy
+
 ## SAVer
 
 RUN git clone https://github.com/svm-abstract-verifier/saver.git && \

flake.nix

@@ -43,7 +43,7 @@
         caisar = ocamlPkgs.buildDunePackage
           {
             pname = "caisar";
-            version = "1.0.0";
+            version = "2.0.0";
             duneVersion = "3";
             minimalOCamlVersion = "4.13";
             installTargets = "all doc";