From 196b5fe2a43ed5dbeb737ba36b88a0963f0697d1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 18 Apr 2024 11:33:53 +0200
Subject: [PATCH] [exps] Add tests for arithmetic
---
tests/arithmetic.t | 27 +++++++++++++++++++++++++++
tests/dune | 16 +++++++++++++++-
2 files changed, 42 insertions(+), 1 deletion(-)
create mode 100644 tests/arithmetic.t
diff --git a/tests/arithmetic.t b/tests/arithmetic.t
new file mode 100644
index 0000000..4d8ba2b
--- /dev/null
+++ b/tests/arithmetic.t
@@ -0,0 +1,27 @@
+ $ . ./setup_env.sh
+
+ $ caisar verify --prover PyRAT --ltag=ProverSpec --ltag=StackTrace --ltag=InterpretGoal --goal :runP1\'vc --define model_filename:FNN_s42.onnx ../examples/arithmetic/arithmetic.why
+ [DEBUG]{InterpretGoal} Interpreted formula for goal 'runP1'vc':
+ forall x:t, x1:t, x2:t.
+ (le ((- 5.0):t) x /\ le x (5.0:t)) /\
+ (le ((- 5.0):t) x1 /\ le x1 (5.0:t)) /\ le ((- 5.0):t) x2 /\ le x2 (5.0:t) ->
+ le (add RNE (add RNE (sub RNE (nn_onnx @@ vector x x1 x2)[0] x) x1) x2)
+ (0.5:t)
+ vector, 3
+ nn_onnx,
+ (Interpreter_types.Model
+ (Interpreter_types.ONNX, { Language.nn_nb_inputs = 3; nn_nb_outputs = 1;
+ nn_ty_elt = t;
+ nn_filename =
+ "../examples/arithmetic/FNN_s42.onnx";
+ nn_format = <nir> }))
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ -5.0 <= x0
+ x0 <= 5.0
+ -5.0 <= x1
+ x1 <= 5.0
+ -5.0 <= x2
+ x2 <= 5.0
+ y0 <= 0.5
+
+ Goal runP1'vc: Unknown ()
diff --git a/tests/dune b/tests/dune
index d2e9762..f30bdf7 100644
--- a/tests/dune
+++ b/tests/dune
@@ -10,7 +10,21 @@
(glob_files bin/*)
filter_tmpdir.sh
../lib/xgboost/example/california.csv
- ../lib/xgboost/example/california.json)
+ ../lib/xgboost/example/california.json
+ )
+ (package caisar))
+
+ (cram
+ (alias local)
+ (applies_to arithmetic)
+ (deps
+ (package caisar)
+ setup_env.sh
+ (glob_files bin/*)
+ filter_tmpdir.sh
+ ../examples/arithmetic/arithmetic.why
+ ../examples/arithmetic/FNN_s42.onnx
+ )
(package caisar))
(cram
--
GitLab