[new release] CAISAR (4.0)

[caisar-platform]

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.

[mseri]

Should we disable the tests in 32 bit architectures?
The current failure seem only due to the integer number sizes:

Goal G: Unknown (unknown)
- +  Fatal error: exception Invalid argument: Int.of_float: argument (-5307258338541568.000000) is out of range or NaN
- +  Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
- +  Called from Dune__exe__Utils.real_constant_of_float in file "src/transformations/utils.ml", line 41, characters 14-45
- +  Called from Dune__exe__Utils.term_of_float in file "src/transformations/utils.ml", line 52, characters 20-46

[caisar-platform]

Should we disable the tests in 32 bit architectures? The current failure seem only due to the integer number sizes:

Goal G: Unknown (unknown)
- +  Fatal error: exception Invalid argument: Int.of_float: argument (-5307258338541568.000000) is out of range or NaN
- +  Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
- +  Called from Dune__exe__Utils.real_constant_of_float in file "src/transformations/utils.ml", line 41, characters 14-45
- +  Called from Dune__exe__Utils.term_of_float in file "src/transformations/utils.ml", line 52, characters 20-46

We do not plan to support 32 bits architectures for now, so disabling the test is the best option. The other failed build (Why3 and TexLive) are slightly more concerning, it seems the selected Why3 versions are not compatible with Archlinux and Fedora build toolchains?

[mseri]

The other failed build (Why3 and TexLive) are slightly more concerning, it seems the selected Why3 versions are not compatible with Archlinux and Fedora build toolchains?

These are independent of your PR, they will need to fix the c code to work with the appropriate c compilers:

# src/server/cpulimit-unix.c: In function 'main':
# src/server/cpulimit-unix.c:95:23: error: assignment to '__sighandler_t' {aka 'void (*)(int)'} from incompatible pointer type 'void (*)(void)' [-Wincompatible-pointer-types]
#    95 |         sa.sa_handler = &wallclock_timelimit_reached;
#       |                       ^
# src/server/cpulimit-unix.c:45:6: note: 'wallclock_timelimit_reached' declared here
#    45 | void wallclock_timelimit_reached() {
#       |      ^~~~~~~~~~~~~~~~~~~~~~~~~~~
# In file included from src/server/cpulimit-unix.c:22:
# /usr/include/signal.h:72:16: note: '__sighandler_t' declared here
#    72 | typedef void (*__sighandler_t) (int);
#       |                ^~~~~~~~~~~~~~

Changes in gcc and clang unfortunately are breaking packages every now and then.

[mseri]

Thanks