Skip to content
Snippets Groups Projects
Commit 3ed0c431 authored by François Bobot's avatar François Bobot
Browse files

[Interpretation] EVen if perhaps not needed handle multiple vectors.

parent a335ae4d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/interpretation/interpreter.ml
+ 31
− 8
View file @ 3ed0c431
...@@ -87,7 +87,13 @@ let builtin_of_constant env known_map (name, value) = ...@@ -87,7 +87,13 @@ let builtin_of_constant env known_map (name, value) =
Logging.user_error (fun m -> Logging.user_error (fun m ->
m "'%s' does not appear to be a declared toplevel constant" name) m "'%s' does not appear to be a declared toplevel constant" name)
let rec bounded_quant_aux engine vs ~cond : IRE.bounded_quant_result option = type bounded_quant_result = {
new_quant : Why3.Term.vsymbol list;
substitutions : Why3.Term.term Why3.Term.Mvs.t;
remaining_implication : Why3.Term.term;
}
let rec bounded_quant_aux engine vs ~cond : bounded_quant_result option =
match vs.Why3.Term.vs_ty with match vs.Why3.Term.vs_ty with
| { | {
ty_node = Tyapp ({ ts_name = { id_string = "vector"; _ }; _ }, ty :: _); ty_node = Tyapp ({ ts_name = { id_string = "vector"; _ }; _ }, ty :: _);
...@@ -115,11 +121,10 @@ let rec bounded_quant_aux engine vs ~cond : IRE.bounded_quant_result option = ...@@ -115,11 +121,10 @@ let rec bounded_quant_aux engine vs ~cond : IRE.bounded_quant_result option =
ITypes.Vector (Language.create_vector env n) ITypes.Vector (Language.create_vector env n)
in in
let substitutions = let substitutions =
[ Why3.Term.Mvs.singleton vs
Why3.Term.Mvs.singleton vs (ITypes.term_of_op ~args engine op (Some vs.vs_ty))
(ITypes.term_of_op ~args engine op (Some vs.vs_ty));
]
in in
Some Some
{ new_quant; substitutions; remaining_implication = Why3.Term.t_true } { new_quant; substitutions; remaining_implication = Why3.Term.t_true }
| Tapp ({ ls_name = { id_string = "has_length"; _ }; _ }, _) -> None | Tapp ({ ls_name = { id_string = "has_length"; _ }; _ }, _) -> None
...@@ -152,7 +157,7 @@ let rec bounded_quant_aux engine vs ~cond : IRE.bounded_quant_result option = ...@@ -152,7 +157,7 @@ let rec bounded_quant_aux engine vs ~cond : IRE.bounded_quant_result option =
| _ -> None | _ -> None
(* Only one vector for now *) (* Only one vector for now *)
let rec bounded_quant engine vsl ~cond : IRE.bounded_quant_result option = let rec bounded_quant engine vsl ~cond : bounded_quant_result option =
match vsl with match vsl with
| ({ | ({
Why3.Term.vs_ty = Why3.Term.vs_ty =
...@@ -164,14 +169,32 @@ let rec bounded_quant engine vsl ~cond : IRE.bounded_quant_result option = ...@@ -164,14 +169,32 @@ let rec bounded_quant engine vsl ~cond : IRE.bounded_quant_result option =
} as vs) } as vs)
:: l -> ( :: l -> (
match bounded_quant_aux engine vs ~cond with match bounded_quant_aux engine vs ~cond with
| None -> None | None -> bounded_quant engine l ~cond
| Some r -> Some { r with new_quant = r.new_quant @ l }) | Some r1 -> (
match bounded_quant engine l ~cond:r1.remaining_implication with
| None -> Some { r1 with new_quant = r1.new_quant @ l }
| Some r2 ->
Some
{
new_quant = r1.new_quant @ r2.new_quant;
substitutions =
Why3.Term.Mvs.set_union r1.substitutions r2.substitutions;
remaining_implication = r2.remaining_implication;
}))
| v :: l -> ( | v :: l -> (
match bounded_quant engine l ~cond with match bounded_quant engine l ~cond with
| None -> None | None -> None
| Some r -> Some { r with new_quant = v :: r.new_quant }) | Some r -> Some { r with new_quant = v :: r.new_quant })
| [] -> None | [] -> None
let bounded_quant engine vsl ~cond : IRE.bounded_quant_result option =
Option.map (bounded_quant engine vsl ~cond) ~f:(fun r ->
{
IRE.new_quant = r.new_quant;
substitutions = [ r.substitutions ];
remaining_implication = r.remaining_implication;
})
let declare_language_lsymbols interpreter_env task = let declare_language_lsymbols interpreter_env task =
(* Declare [Language] logic symbols only. *) (* Declare [Language] logic symbols only. *)
Why3.Term.Hls.fold Why3.Term.Hls.fold
......
tests/acasxu.t
+ 202
− 2
View file @ 3ed0c431
...@@ -112,6 +112,19 @@ Test verify on acasxu ...@@ -112,6 +112,19 @@ Test verify on acasxu
> let o2 = (nn_onnx @@ i)[weak_left] in > let o2 = (nn_onnx @@ i)[weak_left] in
> o1, o2 > o1, o2
> >
> let run2v2 (i: input) (j: input)
> requires { has_length i 5 }
> requires { has_length j 5 }
> requires { valid_input i }
> requires { intruder_distant_and_slow i }
> requires { intruder_distant_and_slow j }
> ensures { let o1, o2 = result in o1 .>= o2 /\ o2 .>= o1 } =
> let i_ = normalize_input i in
> let j_ = normalize_input j in
> let o1 = (nn_onnx @@ i_)[clear_of_conflict] in
> let o2 = (nn_onnx @@ j_)[clear_of_conflict] in
> o1, o2
>
> let run3 (j: input) (eps:t) > let run3 (j: input) (eps:t)
> requires { has_length j 5 } > requires { has_length j 5 }
> requires { valid_input j } > requires { valid_input j }
...@@ -344,6 +357,84 @@ Test verify on acasxu ...@@ -344,6 +357,84 @@ Test verify on acasxu
x4 <= 60.0 x4 <= 60.0
y0 <= y1 and y1 <= y0 y0 <= y1 and y1 <= y0
[DEBUG]{InterpretGoal} Interpreted formula for goal 'run2v2'vc':
forall x:t, x1:t, x2:t, x3:t, x4:t, x5:t, x6:t, x7:t, x8:t, x9:t.
((le (0.0:t) x /\ le x (60760.0:t)) /\
(le (neg (3.141592653589793115997963468544185161590576171875:t)) x1 /\
le x1 (3.141592653589793115997963468544185161590576171875:t)) /\
(le (neg (3.141592653589793115997963468544185161590576171875:t)) x2 /\
le x2 (3.141592653589793115997963468544185161590576171875:t)) /\
(le (100.0:t) x3 /\ le x3 (1200.0:t)) /\ le (0.0:t) x4 /\ le x4 (1200.0:t)) /\
(le (55947.6909999999988940544426441192626953125:t) x /\
le (1145.0:t) x3 /\ le x4 (60.0:t)) /\
le (55947.6909999999988940544426441192626953125:t) x5 /\
le (1145.0:t) x8 /\ le x9 (60.0:t) ->
le
(nn_onnx
@@ vector (div RNE (sub RNE x5 (19791.0:t)) (60261.0:t))
(div RNE (sub RNE x6 (0.0:t))
(6.2831853071800001231395071954466402530670166015625:t))
(div RNE (sub RNE x7 (0.0:t))
(6.2831853071800001231395071954466402530670166015625:t))
(div RNE (sub RNE x8 (650.0:t)) (1100.0:t))
(div RNE (sub RNE x9 (600.0:t)) (1200.0:t)))
[0]
(nn_onnx
@@ vector (div RNE (sub RNE x (19791.0:t)) (60261.0:t))
(div RNE (sub RNE x1 (0.0:t))
(6.2831853071800001231395071954466402530670166015625:t))
(div RNE (sub RNE x2 (0.0:t))
(6.2831853071800001231395071954466402530670166015625:t))
(div RNE (sub RNE x3 (650.0:t)) (1100.0:t))
(div RNE (sub RNE x4 (600.0:t)) (1200.0:t)))
[0] /\
le
(nn_onnx
@@ vector (div RNE (sub RNE x (19791.0:t)) (60261.0:t))
(div RNE (sub RNE x1 (0.0:t))
(6.2831853071800001231395071954466402530670166015625:t))
(div RNE (sub RNE x2 (0.0:t))
(6.2831853071800001231395071954466402530670166015625:t))
(div RNE (sub RNE x3 (650.0:t)) (1100.0:t))
(div RNE (sub RNE x4 (600.0:t)) (1200.0:t)))
[0]
(nn_onnx
@@ vector (div RNE (sub RNE x5 (19791.0:t)) (60261.0:t))
(div RNE (sub RNE x6 (0.0:t))
(6.2831853071800001231395071954466402530670166015625:t))
(div RNE (sub RNE x7 (0.0:t))
(6.2831853071800001231395071954466402530670166015625:t))
(div RNE (sub RNE x8 (650.0:t)) (1100.0:t))
(div RNE (sub RNE x9 (600.0:t)) (1200.0:t)))
[0]
nn_onnx,
(Interpreter_types.Model
(Interpreter_types.ONNX, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
nn_ty_elt = t;
nn_filename =
"./../examples/acasxu/nets/onnx/ACASXU_1_1.onnx";
nn_format = <nier> }))
vector,
5
[DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 60760.0
-3.141592653589793115997963468544185161590576171875 <= x1
x1 <= 3.141592653589793115997963468544185161590576171875
-3.141592653589793115997963468544185161590576171875 <= x2
x2 <= 3.141592653589793115997963468544185161590576171875
100.0 <= x3
x3 <= 1200.0
0.0 <= x4
x4 <= 1200.0
55947.6909999999988940544426441192626953125 <= x0
1145.0 <= x3
x4 <= 60.0
55947.6909999999988940544426441192626953125 <= x5
1145.0 <= x8
x9 <= 60.0
y0 <= y1 and y1 <= y0
[DEBUG]{InterpretGoal} Interpreted formula for goal 'run3'vc': [DEBUG]{InterpretGoal} Interpreted formula for goal 'run3'vc':
forall x:t, x1:t, x2:t, x3:t, x4:t, eps:t. forall x:t, x1:t, x2:t, x3:t, x4:t, eps:t.
((le (0.0:t) x /\ le x (60760.0:t)) /\ ((le (0.0:t) x /\ le x (60760.0:t)) /\
...@@ -456,13 +547,14 @@ Test verify on acasxu ...@@ -456,13 +547,14 @@ Test verify on acasxu
(373.9499200000000200816430151462554931640625:t)) (373.9499200000000200816430151462554931640625:t))
(7.51888402010059753166615337249822914600372314453125:t)) (7.51888402010059753166615337249822914600372314453125:t))
(1500.0:t) (1500.0:t)
vector, 5
nn_nnet, nn_nnet,
(Interpreter_types.Model (Interpreter_types.Model
(Interpreter_types.NNet, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5; (Interpreter_types.NNet, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
nn_ty_elt = t; nn_ty_elt = t;
nn_filename = "./TestNetwork.nnet"; nn_filename = "./TestNetwork.nnet";
nn_format = Language.NNet })) nn_format = Language.NNet }))
vector,
5
[DEBUG]{ProverSpec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0 -0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625 x0 <= 0.67985927880386987087746319957659579813480377197265625
...@@ -530,13 +622,14 @@ Test verify on acasxu ...@@ -530,13 +622,14 @@ Test verify on acasxu
(nn_nnet @@ vector x x1 x2 x3 x4)[3]) /\ (nn_nnet @@ vector x x1 x2 x3 x4)[3]) /\
lt (nn_nnet @@ vector x x1 x2 x3 x4)[0] lt (nn_nnet @@ vector x x1 x2 x3 x4)[0]
(nn_nnet @@ vector x x1 x2 x3 x4)[4]) (nn_nnet @@ vector x x1 x2 x3 x4)[4])
vector, 5
nn_nnet, nn_nnet,
(Interpreter_types.Model (Interpreter_types.Model
(Interpreter_types.NNet, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5; (Interpreter_types.NNet, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
nn_ty_elt = t; nn_ty_elt = t;
nn_filename = "./TestNetwork.nnet"; nn_filename = "./TestNetwork.nnet";
nn_format = Language.NNet })) nn_format = Language.NNet }))
vector,
5
[DEBUG]{ProverSpec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0 -0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625 x0 <= 0.67985927880386987087746319957659579813480377197265625
...@@ -560,6 +653,7 @@ Test verify on acasxu ...@@ -560,6 +653,7 @@ Test verify on acasxu
Goal runP1'vc: Unknown () Goal runP1'vc: Unknown ()
Goal runP1v2'vc: Unknown () Goal runP1v2'vc: Unknown ()
Goal run2'vc: Unknown () Goal run2'vc: Unknown ()
Goal run2v2'vc: Unknown ()
Goal run3'vc: Unknown () Goal run3'vc: Unknown ()
Goal P1: Unknown () Goal P1: Unknown ()
Goal P3: Unknown () Goal P3: Unknown ()
...@@ -721,6 +815,72 @@ Test verify on acasxu ...@@ -721,6 +815,72 @@ Test verify on acasxu
;; X_5 ;; X_5
(declare-const X_5 Real) (declare-const X_5 Real)
;; X_6
(declare-const X_6 Real)
;; X_7
(declare-const X_7 Real)
;; X_8
(declare-const X_8 Real)
;; X_9
(declare-const X_9 Real)
;; Requires
(assert (>= X_0 0.0))
(assert (<= X_0 60760.0))
(assert (>= X_1 -3.141592653589793115997963468544185161590576171875))
(assert (<= X_1 3.141592653589793115997963468544185161590576171875))
(assert (>= X_2 -3.141592653589793115997963468544185161590576171875))
(assert (<= X_2 3.141592653589793115997963468544185161590576171875))
(assert (>= X_3 100.0))
(assert (<= X_3 1200.0))
(assert (>= X_4 0.0))
(assert (<= X_4 1200.0))
;; Requires
(assert (>= X_0 55947.6909999999988940544426441192626953125))
(assert (>= X_3 1145.0))
(assert (<= X_4 60.0))
;; Requires
(assert (>= X_5 55947.6909999999988940544426441192626953125))
(assert (>= X_8 1145.0))
(assert (<= X_9 60.0))
;; Y_1
(declare-const Y_1 Real)
;; Y_0
(declare-const Y_0 Real)
;; Goal run2v2'vc
(assert (or (and (>= Y_0 Y_1))
(and (>= Y_1 Y_0))
))
[DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
(declare-const X_0 Real)
;; X_1
(declare-const X_1 Real)
;; X_2
(declare-const X_2 Real)
;; X_3
(declare-const X_3 Real)
;; X_4
(declare-const X_4 Real)
;; X_5
(declare-const X_5 Real)
;; Requires ;; Requires
(assert (>= X_0 0.0)) (assert (>= X_0 0.0))
(assert (<= X_0 60760.0)) (assert (<= X_0 60760.0))
...@@ -923,6 +1083,7 @@ Test verify on acasxu ...@@ -923,6 +1083,7 @@ Test verify on acasxu
Goal runP1'vc: Unknown () Goal runP1'vc: Unknown ()
Goal runP1v2'vc: Unknown () Goal runP1v2'vc: Unknown ()
Goal run2'vc: Unknown () Goal run2'vc: Unknown ()
Goal run2v2'vc: Unknown ()
Goal run3'vc: Unknown () Goal run3'vc: Unknown ()
Goal P1: Unknown () Goal P1: Unknown ()
Goal P3: Unknown () Goal P3: Unknown ()
...@@ -1008,6 +1169,44 @@ Test verify on acasxu ...@@ -1008,6 +1169,44 @@ Test verify on acasxu
x4 <= 60.0 x4 <= 60.0
+y1 -y0 >= 0 +y1 -y0 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 60760.0
x1 >= -3.141592653589793115997963468544185161590576171875
x1 <= 3.141592653589793115997963468544185161590576171875
x2 >= -3.141592653589793115997963468544185161590576171875
x2 <= 3.141592653589793115997963468544185161590576171875
x3 >= 100.0
x3 <= 1200.0
x4 >= 0.0
x4 <= 1200.0
x0 >= 55947.6909999999988940544426441192626953125
x3 >= 1145.0
x4 <= 60.0
x5 >= 55947.6909999999988940544426441192626953125
x8 >= 1145.0
x9 <= 60.0
+y0 -y1 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 60760.0
x1 >= -3.141592653589793115997963468544185161590576171875
x1 <= 3.141592653589793115997963468544185161590576171875
x2 >= -3.141592653589793115997963468544185161590576171875
x2 <= 3.141592653589793115997963468544185161590576171875
x3 >= 100.0
x3 <= 1200.0
x4 >= 0.0
x4 <= 1200.0
x0 >= 55947.6909999999988940544426441192626953125
x3 >= 1145.0
x4 <= 60.0
x5 >= 55947.6909999999988940544426441192626953125
x8 >= 1145.0
x9 <= 60.0
+y1 -y0 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 60760.0 x0 <= 60760.0
...@@ -1086,6 +1285,7 @@ Test verify on acasxu ...@@ -1086,6 +1285,7 @@ Test verify on acasxu
Goal runP1'vc: Unknown () Goal runP1'vc: Unknown ()
Goal runP1v2'vc: Unknown () Goal runP1v2'vc: Unknown ()
Goal run2'vc: Unknown () Goal run2'vc: Unknown ()
Goal run2v2'vc: Unknown ()
Goal run3'vc: Unknown () Goal run3'vc: Unknown ()
Goal P1: Unknown () Goal P1: Unknown ()
Goal P3: Unknown () Goal P3: Unknown ()
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment