[new release] caisar (5.0)

[caisar-platform]

CHANGES:

• [language] Added support for global robustness properties. It is now possible to specify and verify global robustness properties with CAISAR. This opens the possibility to specify properties on a whole input domain. See the manual for more details, including examples.

• [prover] Added the prover-precision option. This option allows to automatically adjust the tradeoff between precision and speed for all of CAISAR supported provers.

• [prover] Support ABCrown configuration file by default.

• [nir] Fix a bug in NNet to ONNX conversion.

• [nir] Support the representation of Radial-Based Function (RBF) kernels for Support Vector Machines.

• [caisarpy] Convert the Python API to emit and send CAISAR-compliant JSON values.

• [dependencies] Bump Why3 version to 1.8.2.

[jmid]

Thanks!

There are lower-bounds errors while compiling why3 on 4.14-5.1 that look ppxlib related:
https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/399db769d84942369e2594b4b1fc7e2b6580322a/variant/compilers,5.1,caisar.5.0,lower-bounds

#=== ERROR while compiling why3.1.8.2 =========================================#
# context              2.5.0 | linux/x86_64 | ocaml-base-compiler.5.1.1 | file:///home/opam/opam-repository
# path                 ~/.opam/5.1/.opam-switch/build/why3.1.8.2
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j71 all byte
# exit-code            2
# env-file             ~/.opam/log/why3-7-7cf6ee.env
# output-file          ~/.opam/log/why3-7-7cf6ee.out
### output ###
# Generate src/util/config.ml
# Ocamllex src/util/rc.mll
# Ocamllex src/util/lexlib.mll
# Menhir src/util/json_parser.mly
[...]
# Ocamlc   plugins/transform/hypothesis_selection.mli
# File "src/util/debug_optim.ml", line 20, characters 2-44:
# 20 |   Ppxlib.Context_free.Rule.special_function'
#        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
# Error: Unbound value Ppxlib.Context_free.Rule.special_function'
# Hint: Did you mean special_function?
# Ocamlc   src/tools/main.mli
# Ocamlc   src/tools/why3config.mli
# Ocamlc   src/tools/why3execute.mli
# make: *** [Makefile:415: src/util/ppx_debug_optim] Error 2
# make: *** Waiting for unfinished jobs....

On Arch there are cram test differences, which look like they are caused by missing SAVer:
https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/399db769d84942369e2594b4b1fc7e2b6580322a/variant/distributions,archlinux-ocaml-4.14,caisar.5.0,tests

#=== ERROR while compiling caisar.5.0 =========================================#
# context              2.5.0 | linux/x86_64 | ocaml-base-compiler.4.14.2 | pinned(https://git.frama-c.com/api/v4/projects/1082/packages/generic/caisar/5.0/caisar-5.0.tbz)
# path                 ~/.opam/4.14/.opam-switch/build/caisar.5.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p caisar -j 255 --promote-install-files=false @install @runtest
# exit-code            1
# env-file             ~/.opam/log/caisar-7-c1b461.env
# output-file          ~/.opam/log/caisar-7-c1b461.out
### output ###
# File "tests/config-json.t", line 1, characters 0-0:
# /usr/sbin/git --no-pager diff --no-index --color=always -u _build/default/tests/config-json.t _build/default/tests/config-json.t.corrected
# diff --git a/_build/default/tests/config-json.t b/_build/default/tests/config-json.t.corrected
# index 62394a4..9f49d8a 100644
# --- a/_build/default/tests/config-json.t
# +++ b/_build/default/tests/config-json.t.corrected
# @@ -49,14 +49,6 @@ Test config-json
#        "paltern": "",
#        "pconf": "'$TESTCASE_ROOT/bin/z3' %f"
#      },
# -    {
# -      "prover": [
# -        "SAVer"
# -      ],
# -      "pversion": "v1.0",
# -      "paltern": "",
# -      "pconf": "'$TESTCASE_ROOT/bin/saver' %{svm} %{dataset} %{abstraction} %{perturbation} %{perturbation_param}"
# -    },
#      {
#        "prover": [
#          "PyRAT"
# File "tests/autodetect.t", line 1, characters 0-0:
# /usr/sbin/git --no-pager diff --no-index --color=always -u _build/default/tests/autodetect.t _build/default/tests/autodetect.t.corrected
# diff --git a/_build/default/tests/autodetect.t b/_build/default/tests/autodetect.t.corrected
# index 7930c27..8520973 100644
# --- a/_build/default/tests/autodetect.t
# +++ b/_build/default/tests/autodetect.t.corrected
# @@ -43,7 +43,6 @@ Test autodetect
#    PyRAT 1.1 (VNNLIB)
#    PyRAT 1.1 (arithmetic)
#    PyRAT 1.1 (confidence)
# -  SAVer v1.0
#    Z3 4.8.12
#    alpha-beta-CROWN dummy-version
#    alpha-beta-CROWN dummy-version (ACAS)
# File "tests/interpretation_fail.t", line 1, characters 0-0:
# /usr/sbin/git --no-pager diff --no-index --color=always -u _build/default/tests/interpretation_fail.t _build/default/tests/interpretation_fail.t.corrected
# diff --git a/_build/default/tests/interpretation_fail.t b/_build/default/tests/interpretation_fail.t.corrected
# index c50ab1e..755d4de 100644
# --- a/_build/default/tests/interpretation_fail.t
# +++ b/_build/default/tests/interpretation_fail.t.corrected
# @@ -159,5 +159,4 @@ which expects input vectors of length 3
#    > EOF
#  
#    $ caisar verify --ltag InterpretGoal --prover SAVer file.mlw
# -  [ERROR] File "file.mlw", line 7, characters 14-24:
# -          unbound function or predicate symbol 'read_model'
# +  [ERROR] No prover corresponds to SAVer

runtest is failing on 32-bit platforms (arm32, x86_32).
Perhaps it should be disabled there?

uunf.17.0.0 fails to compile on 4.14+flambda which is a known issue.

All 4 macOS homebrew workflows timed out.

What do you make of these?

[caisar-platform]

Thanks for the feedback.

1. The lowerbound issue in Why3 comes indeed from 1.8.2, it seemed that when merged in Opam, those were non-blocking for a release. I think we can ignore it.

2. The Archlinux failure is currently investigated. During tests, SAVER is a stub located in tests/bin. The expected behaviour for the end-user is to install the SAVER binary themselves, so this should not be an issue for end-users in a real-life scenario. I think we can ignore this issue as well.

3. We do not plan to support 32 bits architectures with CAISAR, so disabling tests is sensible; we will remove support for those in a future release.

[mseri]

Should we wait for the archlinux investigation results?