diff --git a/lib/nnet/nnet.ml b/lib/nnet/nnet.ml
index b0c311af051e3751f75d373493e4aca3703c9a4b..8b626b36d2000e4ad99f078616ce80c0d70d9523 100644
--- a/lib/nnet/nnet.ml
+++ b/lib/nnet/nnet.ml
@@ -8,6 +8,7 @@ open Base
module Format = Caml.Format
module Sys = Caml.Sys
module Filename = Caml.Filename
+module Fun = Caml.Fun
type t = {
n_layers : int;
@@ -132,7 +133,7 @@ let handle_nnet_weights_and_biases in_channel =
(* Retrieves [filename] NNet model metadata and weights wrt NNet format
specification (see https://github.com/sisl/NNet for details). *)
-let parse_cin filename in_channel =
+let parse_in_channel filename in_channel =
let open Result in
try
skip_nnet_header filename in_channel >>= fun () ->
@@ -166,6 +167,6 @@ let parse_cin filename in_channel =
let parse filename =
let in_channel = Stdlib.open_in filename in
- Caml.Fun.protect
+ Fun.protect
~finally:(fun () -> Stdlib.close_in in_channel)
- (fun () -> parse_cin filename in_channel)
+ (fun () -> parse_in_channel filename in_channel)
diff --git a/lib/nnet/nnet.mli b/lib/nnet/nnet.mli
index a68f41cc8f6725e5384de733d0d3f69a88725f6a..a1b5076fefaccfcea806f896708b3d48260d0eeb 100644
--- a/lib/nnet/nnet.mli
+++ b/lib/nnet/nnet.mli
@@ -22,6 +22,3 @@ type t = private {
val parse : string -> (t, string) Result.t
(** Parse an NNet file. *)
-
-val parse_cin : string -> in_channel -> (t, string) Result.t
-(** Parse an NNet file. *)
diff --git a/src/language.ml b/src/language.ml
index cef0c9ff7f3585f8f52c7588cf19f77bf24bfbd1..ee97874283d40ee8769c1899b37d914ea1920784 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -1,35 +1,41 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
open Base
-(** Register Neural network languages *)
-let nnet_parser env _ filename cin =
- let nnet = Why3.Pmodule.read_module env [ "caisar" ] "NNet" in
+(* Register neural network languages *)
+
+let nnet_parser env _ filename _ =
+ let open Why3 in
+ let nnet = Pmodule.read_module env [ "caisar" ] "NNet" in
let nnet_input_type =
- Why3.Ty.ty_app
- Why3.Theory.(ns_find_ts nnet.mod_theory.th_export [ "input_type" ])
- []
+ Ty.ty_app Theory.(ns_find_ts nnet.mod_theory.th_export [ "input_type" ]) []
in
- let header = Nnet.parse_cin filename cin in
+ let header = Nnet.parse filename in
match header with
- | Error s -> Why3.Loc.errorm "%s" s
+ | Error s -> Loc.errorm "%s" s
| Ok header ->
- let id_as_tuple = Why3.Ident.id_fresh "As_tuple" in
- let th_uc = Why3.Pmodule.create_module env id_as_tuple in
- let th_uc = Why3.Pmodule.use_export th_uc nnet in
- let open Why3 in
+ let id_as_tuple = Ident.id_fresh "As_tuple" in
+ let th_uc = Pmodule.create_module env id_as_tuple in
+ let th_uc = Pmodule.use_export th_uc nnet in
let ls_out =
- Term.create_fsymbol (Ident.id_fresh "out")
+ Term.create_fsymbol
+ (Ident.id_fresh "nnet_apply")
(List.init header.n_inputs ~f:(fun _ -> nnet_input_type))
- (Why3.Ty.ty_tuple
+ (Ty.ty_tuple
(List.init header.n_outputs ~f:(fun _ -> nnet_input_type)))
in
let th_uc =
- Why3.Pmodule.add_pdecl ~vc:false th_uc
+ Pmodule.add_pdecl ~vc:false th_uc
(Pdecl.create_pure_decl @@ Decl.create_param_decl ls_out)
in
- Why3.Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
+ Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
let register () =
Why3.Env.(
- register_format ~desc:"NNet format (only RLU)" Why3.Pmodule.mlw_language
+ register_format ~desc:"NNet format (ReLU only)" Why3.Pmodule.mlw_language
"NNet" [ "nnet" ] nnet_parser)
diff --git a/src/main.ml b/src/main.ml
index 18e45dbc088c0a536684b282c24d1add81d8988d..8cda571d7003b06e78164942c268aa84da68db50 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -86,10 +86,10 @@ let config_cmd =
$ const cmdname $ detect $ setup_logs)),
Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man )
-let prove_cmd =
- let cmdname = "prove" in
+let verify_cmd =
+ let cmdname = "verify" in
let files =
- let doc = "Files to prove" in
+ let doc = "Files to verify" in
Arg.(value & pos_all string [] & info [] ~doc)
in
let format =
@@ -100,12 +100,11 @@ let prove_cmd =
let doc = "additional loadpath" in
Arg.(value & opt_all string [] & info [ "L" ] ~doc)
in
- let doc = Format.sprintf "%s configuration." caisar in
+ let doc = "Property verification of neural networks." in
let exits = Term.default_exits in
let man =
[
- `S Manpage.s_description;
- `P (Format.sprintf "Handle the configuration of %s." caisar);
+ `S Manpage.s_description; `P "Property verification via external solvers.";
]
in
( Term.(
@@ -133,6 +132,6 @@ let default_cmd =
Term.info caisar ~version ~doc ~sdocs ~exits:Term.default_exits ~man )
let () =
- match Term.(eval_choice default_cmd [ config_cmd; prove_cmd ]) with
+ match Term.(eval_choice default_cmd [ config_cmd; verify_cmd ]) with
| `Error _ -> Caml.exit 1
| _ -> Caml.exit (if Logs.err_count () > 0 then 1 else 0)
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 0719fd685966903ce04f42ded5bff82f7df1f2cf..09763d9fea2daaf27063263bd4e2ec532a3a23d7 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -1,3 +1,4 @@
theory NNet
- type input_type = int
+ use ieee_float.Float64
+ type input_type = t
end
diff --git a/tests/simple.t b/tests/simple.t
index 8216a65f002ba5758c17a354ac7b7647dfc52a57..b1729081aa728e20fc804ecefaddedfa2c1140c4 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -1,13 +1,14 @@
Test help
- $ caisar prove -L . --format whyml - <<EOF
+ $ caisar verify -L . --format whyml - <<EOF
> theory T
> use TestNetwork.AsTuple
- > use int.Int
+ > use ieee_float.Float64
+ > use real.RealInfix
> use caisar.NNet
>
> goal G: forall x1 x2 x3 x4 x5.
- > let (y1,_,_,_,_) = out x1 x2 x3 x4 x5 in
- > 0 < y1 < 10
+ > let (y1,_,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
+ > 0.0 <. t'real y1 <. 0.1
> end
> EOF
theory Task
@@ -36,19 +37,6 @@ Test help
(* use why3.Unit.Unit *)
- type input_type = int
-
- (* use caisar.NNet *)
-
- type tuple5 'a 'a1 'a2 'a3 'a4 =
- | Tuple5 'a 'a1 'a2 'a3 'a4
-
- (* use why3.Tuple5.Tuple51 *)
-
- function out int int int int int : (int, int, int, int, int)
-
- (* use As_tuple *)
-
constant zero : int = 0
constant one : int = 1
@@ -215,9 +203,1350 @@ Test help
(* use int.Int *)
+ constant zero5 : real = 0.0
+
+ constant one3 : real = 1.0
+
+ function (-'''''_) real : real
+
+ function (+''''') real real : real
+
+ function ( *''''') real real : real
+
+ predicate (<') real real
+
+ predicate (>') (x:real) (y:real) = y <' x
+
+ predicate (<='') (x:real) (y:real) = x <' y \/ x = y
+
+ predicate (>=') (x:real) (y:real) = y <='' x
+
+ Assoc14 :
+ forall x:real, y:real, z:real.
+ ((x +''''' y) +''''' z) = (x +''''' (y +''''' z))
+
+ (* clone algebra.Assoc with type t = real, function op = (+'''''),
+ prop Assoc1 = Assoc14, *)
+
+ Unit_def_l8 : forall x:real. (zero5 +''''' x) = x
+
+ Unit_def_r8 : forall x:real. (x +''''' zero5) = x
+
+ (* clone algebra.Monoid with type t1 = real, constant unit = zero5,
+ function op1 = (+'''''), prop Unit_def_r1 = Unit_def_r8,
+ prop Unit_def_l1 = Unit_def_l8, prop Assoc2 = Assoc14, *)
+
+ Inv_def_l7 : forall x:real. ((-''''' x) +''''' x) = zero5
+
+ Inv_def_r7 : forall x:real. (x +''''' (-''''' x)) = zero5
+
+ (* clone algebra.Group with type t2 = real, function inv = (-'''''_),
+ constant unit1 = zero5, function op2 = (+'''''),
+ prop Inv_def_r1 = Inv_def_r7, prop Inv_def_l1 = Inv_def_l7,
+ prop Unit_def_r2 = Unit_def_r8, prop Unit_def_l2 = Unit_def_l8,
+ prop Assoc3 = Assoc14, *)
+
+ Comm11 : forall x:real, y:real. (x +''''' y) = (y +''''' x)
+
+ (* clone algebra.Comm with type t3 = real, function op3 = (+'''''),
+ prop Comm1 = Comm11, *)
+
+ (* meta AC function (+''''') *)
+
+ (* clone algebra.CommutativeGroup with type t4 = real,
+ function inv1 = (-'''''_), constant unit2 = zero5,
+ function op4 = (+'''''), prop Comm2 = Comm11,
+ prop Inv_def_r2 = Inv_def_r7, prop Inv_def_l2 = Inv_def_l7,
+ prop Unit_def_r3 = Unit_def_r8, prop Unit_def_l3 = Unit_def_l8,
+ prop Assoc4 = Assoc14, *)
+
+ Assoc15 :
+ forall x:real, y:real, z:real.
+ ((x *''''' y) *''''' z) = (x *''''' (y *''''' z))
+
+ (* clone algebra.Assoc with type t = real, function op = ( *'''''),
+ prop Assoc1 = Assoc15, *)
+
+ Mul_distr_l5 :
+ forall x:real, y:real, z:real.
+ (x *''''' (y +''''' z)) = ((x *''''' y) +''''' (x *''''' z))
+
+ Mul_distr_r5 :
+ forall x:real, y:real, z:real.
+ ((y +''''' z) *''''' x) = ((y *''''' x) +''''' (z *''''' x))
+
+ (* clone algebra.Ring with type t5 = real, function ( *') = ( *'''''),
+ function (-'_) = (-'''''_), function (+') = (+'''''),
+ constant zero1 = zero5, prop Mul_distr_r1 = Mul_distr_r5,
+ prop Mul_distr_l1 = Mul_distr_l5, prop Assoc6 = Assoc15,
+ prop Comm3 = Comm11, prop Inv_def_r3 = Inv_def_r7,
+ prop Inv_def_l3 = Inv_def_l7, prop Unit_def_r4 = Unit_def_r8,
+ prop Unit_def_l4 = Unit_def_l8, prop Assoc7 = Assoc14, *)
+
+ Comm12 : forall x:real, y:real. (x *''''' y) = (y *''''' x)
+
+ (* clone algebra.Comm with type t3 = real, function op3 = ( *'''''),
+ prop Comm1 = Comm12, *)
+
+ (* meta AC function ( *''''') *)
+
+ (* clone algebra.CommutativeRing with type t6 = real,
+ function ( *'') = ( *'''''), function (-''_) = (-'''''_),
+ function (+'') = (+'''''), constant zero2 = zero5, prop Comm5 = Comm12,
+ prop Mul_distr_r2 = Mul_distr_r5, prop Mul_distr_l2 = Mul_distr_l5,
+ prop Assoc8 = Assoc15, prop Comm6 = Comm11, prop Inv_def_r4 = Inv_def_r7,
+ prop Inv_def_l4 = Inv_def_l7, prop Unit_def_r5 = Unit_def_r8,
+ prop Unit_def_l5 = Unit_def_l8, prop Assoc9 = Assoc14, *)
+
+ Unitary3 : forall x:real. (one3 *''''' x) = x
+
+ NonTrivialRing3 : not zero5 = one3
+
+ (* clone algebra.UnitaryCommutativeRing with type t7 = real,
+ constant one1 = one3, function ( *''') = ( *'''''),
+ function (-'''_) = (-'''''_), function (+''') = (+'''''),
+ constant zero3 = zero5, prop NonTrivialRing1 = NonTrivialRing3,
+ prop Unitary1 = Unitary3, prop Comm7 = Comm12,
+ prop Mul_distr_r3 = Mul_distr_r5, prop Mul_distr_l3 = Mul_distr_l5,
+ prop Assoc10 = Assoc15, prop Comm8 = Comm11,
+ prop Inv_def_r5 = Inv_def_r7, prop Inv_def_l5 = Inv_def_l7,
+ prop Unit_def_r6 = Unit_def_r8, prop Unit_def_l6 = Unit_def_l8,
+ prop Assoc11 = Assoc14, *)
+
+ function inv2 real : real
+
+ Inverse : forall x:real. not x = zero5 -> (x *''''' inv2 x) = one3
+
+ function (-') (x:real) (y:real) : real = x +''''' (-''''' y)
+
+ function (/) (x:real) (y:real) : real = x *''''' inv2 y
+
+ add_div :
+ forall x:real, y:real, z:real.
+ not z = zero5 -> ((x +''''' y) / z) = ((x / z) +''''' (y / z))
+
+ sub_div :
+ forall x:real, y:real, z:real.
+ not z = zero5 -> ((x -' y) / z) = ((x / z) -' (y / z))
+
+ neg_div :
+ forall x:real, y:real.
+ not y = zero5 -> ((-''''' x) / y) = (-''''' (x / y))
+
+ assoc_mul_div :
+ forall x:real, y:real, z:real.
+ not z = zero5 -> ((x *''''' y) / z) = (x *''''' (y / z))
+
+ assoc_div_mul :
+ forall x:real, y:real, z:real.
+ not y = zero5 /\ not z = zero5 -> ((x / y) / z) = (x / (y *''''' z))
+
+ assoc_div_div :
+ forall x:real, y:real, z:real.
+ not y = zero5 /\ not z = zero5 -> (x / (y / z)) = ((x *''''' z) / y)
+
+ (* clone algebra.Field with type t17 = real, function (/') = (/),
+ function (-'') = (-'), function inv3 = inv2, constant one4 = one3,
+ function ( *'''''') = ( *'''''), function (-''''''_) = (-'''''_),
+ function (+'''''') = (+'''''), constant zero6 = zero5,
+ prop assoc_div_div1 = assoc_div_div, prop assoc_div_mul1 = assoc_div_mul,
+ prop assoc_mul_div1 = assoc_mul_div, prop neg_div1 = neg_div,
+ prop sub_div1 = sub_div, prop add_div1 = add_div,
+ prop Inverse1 = Inverse, prop NonTrivialRing4 = NonTrivialRing3,
+ prop Unitary4 = Unitary3, prop Comm13 = Comm12,
+ prop Mul_distr_r6 = Mul_distr_r5, prop Mul_distr_l6 = Mul_distr_l5,
+ prop Assoc16 = Assoc15, prop Comm14 = Comm11,
+ prop Inv_def_r8 = Inv_def_r7, prop Inv_def_l8 = Inv_def_l7,
+ prop Unit_def_r9 = Unit_def_r8, prop Unit_def_l9 = Unit_def_l8,
+ prop Assoc17 = Assoc14, *)
+
+ (* clone relations.EndoRelation with type t8 = real,
+ predicate rel = (<=''), *)
+
+ Refl6 : forall x:real. x <='' x
+
+ (* clone relations.Reflexive with type t9 = real, predicate rel1 = (<=''),
+ prop Refl1 = Refl6, *)
+
+ (* clone relations.EndoRelation with type t8 = real,
+ predicate rel = (<=''), *)
+
+ Trans6 : forall x:real, y:real, z:real. x <='' y -> y <='' z -> x <='' z
+
+ (* clone relations.Transitive with type t10 = real,
+ predicate rel2 = (<=''), prop Trans1 = Trans6, *)
+
+ (* clone relations.PreOrder with type t11 = real, predicate rel3 = (<=''),
+ prop Trans2 = Trans6, prop Refl2 = Refl6, *)
+
+ (* clone relations.EndoRelation with type t8 = real,
+ predicate rel = (<=''), *)
+
+ Antisymm5 : forall x:real, y:real. x <='' y -> y <='' x -> x = y
+
+ (* clone relations.Antisymmetric with type t12 = real,
+ predicate rel4 = (<=''), prop Antisymm1 = Antisymm5, *)
+
+ (* clone relations.PartialOrder with type t13 = real,
+ predicate rel5 = (<=''), prop Antisymm2 = Antisymm5,
+ prop Trans3 = Trans6, prop Refl3 = Refl6, *)
+
+ (* clone relations.EndoRelation with type t8 = real,
+ predicate rel = (<=''), *)
+
+ Total4 : forall x:real, y:real. x <='' y \/ y <='' x
+
+ (* clone relations.Total with type t14 = real, predicate rel6 = (<=''),
+ prop Total1 = Total4, *)
+
+ (* clone relations.TotalOrder with type t15 = real,
+ predicate rel7 = (<=''), prop Total2 = Total4,
+ prop Antisymm3 = Antisymm5, prop Trans4 = Trans6, prop Refl4 = Refl6, *)
+
+ ZeroLessOne2 : zero5 <='' one3
+
+ CompatOrderAdd2 :
+ forall x:real, y:real, z:real. x <='' y -> (x +''''' z) <='' (y +''''' z)
+
+ CompatOrderMult2 :
+ forall x:real, y:real, z:real.
+ x <='' y -> zero5 <='' z -> (x *''''' z) <='' (y *''''' z)
+
+ (* clone algebra.OrderedField with type t18 = real,
+ predicate (<=''') = (<=''), function (/'') = (/), function (-''') = (-'),
+ function inv4 = inv2, constant one5 = one3,
+ function ( *''''''') = ( *'''''), function (-'''''''_) = (-'''''_),
+ function (+''''''') = (+'''''), constant zero7 = zero5,
+ prop CompatOrderMult3 = CompatOrderMult2,
+ prop CompatOrderAdd3 = CompatOrderAdd2, prop ZeroLessOne3 = ZeroLessOne2,
+ prop Total5 = Total4, prop Antisymm6 = Antisymm5, prop Trans7 = Trans6,
+ prop Refl7 = Refl6, prop assoc_div_div2 = assoc_div_div,
+ prop assoc_div_mul2 = assoc_div_mul, prop assoc_mul_div2 = assoc_mul_div,
+ prop neg_div2 = neg_div, prop sub_div2 = sub_div,
+ prop add_div2 = add_div, prop Inverse2 = Inverse,
+ prop NonTrivialRing5 = NonTrivialRing3, prop Unitary5 = Unitary3,
+ prop Comm15 = Comm12, prop Mul_distr_r7 = Mul_distr_r5,
+ prop Mul_distr_l7 = Mul_distr_l5, prop Assoc18 = Assoc15,
+ prop Comm16 = Comm11, prop Inv_def_r9 = Inv_def_r7,
+ prop Inv_def_l9 = Inv_def_l7, prop Unit_def_r10 = Unit_def_r8,
+ prop Unit_def_l10 = Unit_def_l8, prop Assoc19 = Assoc14, *)
+
+ (* use real.Real *)
+
+ type t19 = <float 11 53>
+
+ function t'real t19 : real
+
+ predicate t'isFinite t19
+
+ constant t'eb : int = 11
+
+ constant t'sb : int = 53
+
+ (* meta float_type type t19, function t'real, predicate t'isFinite *)
+
+ (* meta model_projection function t'real *)
+
+ constant pow2sb : int = 9007199254740992
+
+ constant max_real : real = 0x1.FFFFFFFFFFFFFp1023
+
+ function pow2 int : int
+
+ axiom Power_0 : pow2 0 = 1
+
+ axiom Power_s : forall n:int. n >= 0 -> pow2 (n + 1) = (2 * pow2 n)
+
+ Power_1 : pow2 1 = 2
+
+ Power_sum :
+ forall n:int, m:int. n >= 0 /\ m >= 0 -> pow2 (n + m) = (pow2 n * pow2 m)
+
+ pow2pos : forall i:int. i >= 0 -> pow2 i > 0
+
+ pow2_0 : pow2 0 = 0x1
+
+ pow2_1 : pow2 1 = 0x2
+
+ pow2_2 : pow2 2 = 0x4
+
+ pow2_3 : pow2 3 = 0x8
+
+ pow2_4 : pow2 4 = 0x10
+
+ pow2_5 : pow2 5 = 0x20
+
+ pow2_6 : pow2 6 = 0x40
+
+ pow2_7 : pow2 7 = 0x80
+
+ pow2_8 : pow2 8 = 0x100
+
+ pow2_9 : pow2 9 = 0x200
+
+ pow2_10 : pow2 10 = 0x400
+
+ pow2_11 : pow2 11 = 0x800
+
+ pow2_12 : pow2 12 = 0x1000
+
+ pow2_13 : pow2 13 = 0x2000
+
+ pow2_14 : pow2 14 = 0x4000
+
+ pow2_15 : pow2 15 = 0x8000
+
+ pow2_16 : pow2 16 = 0x10000
+
+ pow2_17 : pow2 17 = 0x20000
+
+ pow2_18 : pow2 18 = 0x40000
+
+ pow2_19 : pow2 19 = 0x80000
+
+ pow2_20 : pow2 20 = 0x100000
+
+ pow2_21 : pow2 21 = 0x200000
+
+ pow2_22 : pow2 22 = 0x400000
+
+ pow2_23 : pow2 23 = 0x800000
+
+ pow2_24 : pow2 24 = 0x1000000
+
+ pow2_25 : pow2 25 = 0x2000000
+
+ pow2_26 : pow2 26 = 0x4000000
+
+ pow2_27 : pow2 27 = 0x8000000
+
+ pow2_28 : pow2 28 = 0x10000000
+
+ pow2_29 : pow2 29 = 0x20000000
+
+ pow2_30 : pow2 30 = 0x40000000
+
+ pow2_31 : pow2 31 = 0x80000000
+
+ pow2_32 : pow2 32 = 0x100000000
+
+ pow2_33 : pow2 33 = 0x200000000
+
+ pow2_34 : pow2 34 = 0x400000000
+
+ pow2_35 : pow2 35 = 0x800000000
+
+ pow2_36 : pow2 36 = 0x1000000000
+
+ pow2_37 : pow2 37 = 0x2000000000
+
+ pow2_38 : pow2 38 = 0x4000000000
+
+ pow2_39 : pow2 39 = 0x8000000000
+
+ pow2_40 : pow2 40 = 0x10000000000
+
+ pow2_41 : pow2 41 = 0x20000000000
+
+ pow2_42 : pow2 42 = 0x40000000000
+
+ pow2_43 : pow2 43 = 0x80000000000
+
+ pow2_44 : pow2 44 = 0x100000000000
+
+ pow2_45 : pow2 45 = 0x200000000000
+
+ pow2_46 : pow2 46 = 0x400000000000
+
+ pow2_47 : pow2 47 = 0x800000000000
+
+ pow2_48 : pow2 48 = 0x1000000000000
+
+ pow2_49 : pow2 49 = 0x2000000000000
+
+ pow2_50 : pow2 50 = 0x4000000000000
+
+ pow2_51 : pow2 51 = 0x8000000000000
+
+ pow2_52 : pow2 52 = 0x10000000000000
+
+ pow2_53 : pow2 53 = 0x20000000000000
+
+ pow2_54 : pow2 54 = 0x40000000000000
+
+ pow2_55 : pow2 55 = 0x80000000000000
+
+ pow2_56 : pow2 56 = 0x100000000000000
+
+ pow2_57 : pow2 57 = 0x200000000000000
+
+ pow2_58 : pow2 58 = 0x400000000000000
+
+ pow2_59 : pow2 59 = 0x800000000000000
+
+ pow2_60 : pow2 60 = 0x1000000000000000
+
+ pow2_61 : pow2 61 = 0x2000000000000000
+
+ pow2_62 : pow2 62 = 0x4000000000000000
+
+ pow2_63 : pow2 63 = 0x8000000000000000
+
+ pow2_64 : pow2 64 = 0x10000000000000000
+
+ (* use bv.Pow2int *)
+
+ function abs (x:real) : real = if x >=' 0.0 then x else -''''' x
+
+ Abs_le :
+ forall x:real, y:real. abs x <='' y <-> (-''''' y) <='' x /\ x <='' y
+
+ Abs_pos : forall x:real. abs x >=' 0.0
+
+ Abs_sum : forall x:real, y:real. abs (x +''''' y) <='' (abs x +''''' abs y)
+
+ Abs_prod : forall x:real, y:real. abs (x *''''' y) = (abs x *''''' abs y)
+
+ triangular_inequality :
+ forall x:real, y:real, z:real.
+ abs (x -' z) <='' (abs (x -' y) +''''' abs (y -' z))
+
+ (* use real.Abs *)
+
+ function from_int int : real
+
+ axiom Zero : from_int 0 = 0.0
+
+ axiom One : from_int 1 = 1.0
+
+ axiom Add :
+ forall x:int, y:int. from_int (x + y) = (from_int x +''''' from_int y)
+
+ axiom Sub :
+ forall x:int, y:int. from_int (x - y) = (from_int x -' from_int y)
+
+ axiom Mul :
+ forall x:int, y:int. from_int (x * y) = (from_int x *''''' from_int y)
+
+ axiom Neg : forall x:int. from_int (- x) = (-''''' from_int x)
+
+ Injective : forall x:int, y:int. from_int x = from_int y -> x = y
+
+ axiom Monotonic : forall x:int, y:int. x <= y -> from_int x <='' from_int y
+
+ (* use real.FromInt *)
+
+ function truncate real : int
+
+ axiom Truncate_int : forall i:int. truncate (from_int i) = i
+
+ axiom Truncate_down_pos :
+ forall x:real.
+ x >=' 0.0 ->
+ from_int (truncate x) <='' x /\ x <' from_int (truncate x + 1)
+
+ axiom Truncate_up_neg :
+ forall x:real.
+ x <='' 0.0 ->
+ from_int (truncate x - 1) <' x /\ x <='' from_int (truncate x)
+
+ axiom Real_of_truncate :
+ forall x:real.
+ (x -' 1.0) <='' from_int (truncate x) /\
+ from_int (truncate x) <='' (x +''''' 1.0)
+
+ axiom Truncate_monotonic :
+ forall x:real, y:real. x <='' y -> truncate x <= truncate y
+
+ axiom Truncate_monotonic_int1 :
+ forall x:real, i:int. x <='' from_int i -> truncate x <= i
+
+ axiom Truncate_monotonic_int2 :
+ forall x:real, i:int. from_int i <='' x -> i <= truncate x
+
+ function floor real : int
+
+ function ceil real : int
+
+ axiom Floor_int : forall i:int. floor (from_int i) = i
+
+ axiom Ceil_int : forall i:int. ceil (from_int i) = i
+
+ axiom Floor_down :
+ forall x:real. from_int (floor x) <='' x /\ x <' from_int (floor x + 1)
+
+ axiom Ceil_up :
+ forall x:real. from_int (ceil x - 1) <' x /\ x <='' from_int (ceil x)
+
+ axiom Floor_monotonic :
+ forall x:real, y:real. x <='' y -> floor x <= floor y
+
+ axiom Ceil_monotonic : forall x:real, y:real. x <='' y -> ceil x <= ceil y
+
+ (* use real.Truncate *)
+
+ function (+.) (x:real) (y:real) : real = x +''''' y
+
+ function (-.) (x:real) (y:real) : real = x -' y
+
+ function ( *.) (x:real) (y:real) : real = x *''''' y
+
+ function (/.) (x:real) (y:real) : real = x / y
+
+ function (-._) (x:real) : real = -''''' x
+
+ function inv5 (x:real) : real = inv2 x
+
+ predicate (<=.) (x:real) (y:real) = x <='' y
+
+ predicate (>=.) (x:real) (y:real) = x >=' y
+
+ predicate (<.) (x:real) (y:real) = x <' y
+
+ predicate (>.) (x:real) (y:real) = x >' y
+
+ (* use real.RealInfix *)
+
+ type mode =
+ | RNE
+ | RNA
+ | RTP
+ | RTN
+ | RTZ
+
+ predicate to_nearest (m:mode) = m = RNE \/ m = RNA
+
+ (* use ieee_float.RoundingMode *)
+
+ constant zeroF : t19
+
+ function add mode t19 t19 : t19
+
+ function sub mode t19 t19 : t19
+
+ function mul mode t19 t19 : t19
+
+ function div mode t19 t19 : t19
+
+ function abs1 t19 : t19
+
+ function neg t19 : t19
+
+ function fma mode t19 t19 t19 : t19
+
+ function sqrt mode t19 : t19
+
+ function (.-_) (x:t19) : t19 = neg x
+
+ function (.+) (x:t19) (y:t19) : t19 = add RNE x y
+
+ function (.-) (x:t19) (y:t19) : t19 = sub RNE x y
+
+ function (.* ) (x:t19) (y:t19) : t19 = mul RNE x y
+
+ function (./) (x:t19) (y:t19) : t19 = div RNE x y
+
+ function roundToIntegral mode t19 : t19
+
+ function min t19 t19 : t19
+
+ function max t19 t19 : t19
+
+ predicate le t19 t19
+
+ predicate lt t19 t19
+
+ predicate ge (x:t19) (y:t19) = le y x
+
+ predicate gt (x:t19) (y:t19) = lt y x
+
+ predicate eq t19 t19
+
+ predicate (.<=) (x:t19) (y:t19) = le x y
+
+ predicate (.<) (x:t19) (y:t19) = lt x y
+
+ predicate (.>=) (x:t19) (y:t19) = ge x y
+
+ predicate (.>) (x:t19) (y:t19) = gt x y
+
+ predicate (.=) (x:t19) (y:t19) = eq x y
+
+ predicate is_normal t19
+
+ predicate is_subnormal t19
+
+ predicate is_zero t19
+
+ predicate is_infinite t19
+
+ predicate is_nan t19
+
+ predicate is_positive t19
+
+ predicate is_negative t19
+
+ predicate is_plus_infinity (x:t19) = is_infinite x /\ is_positive x
+
+ predicate is_minus_infinity (x:t19) = is_infinite x /\ is_negative x
+
+ predicate is_plus_zero (x:t19) = is_zero x /\ is_positive x
+
+ predicate is_minus_zero (x:t19) = is_zero x /\ is_negative x
+
+ predicate is_not_nan (x:t19) = t'isFinite x \/ is_infinite x
+
+ is_not_nan : forall x:t19. is_not_nan x <-> not is_nan x
+
+ is_not_finite :
+ forall x:t19. not t'isFinite x <-> is_infinite x \/ is_nan x
+
+ zeroF_is_positive : is_positive zeroF
+
+ zeroF_is_zero : is_zero zeroF
+
+ zero_to_real :
+ forall x:t19 [is_zero x]. is_zero x <-> t'isFinite x /\ t'real x = 0.0
+
+ function of_int mode int : t19
+
+ function to_int mode t19 : int
+
+ zero_of_int : forall m:mode. zeroF = of_int m 0
+
+ function round mode real : real
+
+ constant max_int : int
+
+ constant emax : int = pow2 (t'eb - 1)
+
+ max_real_int : max_real = from_int max_int
+
+ predicate in_range (x:real) = (-. max_real) <=. x /\ x <=. max_real
+
+ predicate in_int_range (i:int) = (- max_int) <= i /\ i <= max_int
+
+ is_finite : forall x:t19. t'isFinite x -> in_range (t'real x)
+
+ predicate no_overflow (m:mode) (x:real) = in_range (round m x)
+
+ Bounded_real_no_overflow :
+ forall m:mode, x:real. in_range x -> no_overflow m x
+
+ Round_monotonic :
+ forall m:mode, x:real, y:real. x <=. y -> round m x <=. round m y
+
+ Round_idempotent :
+ forall m1:mode, m2:mode, x:real. round m1 (round m2 x) = round m2 x
+
+ Round_to_real :
+ forall m:mode, x:t19. t'isFinite x -> round m (t'real x) = t'real x
+
+ Round_down_le : forall x:real. round RTN x <=. x
+
+ Round_up_ge : forall x:real. round RTP x >=. x
+
+ Round_down_neg : forall x:real. round RTN (-. x) = (-. round RTP x)
+
+ Round_up_neg : forall x:real. round RTP (-. x) = (-. round RTN x)
+
+ predicate in_safe_int_range (i:int) = (- pow2sb) <= i /\ i <= pow2sb
+
+ Exact_rounding_for_integers :
+ forall m:mode, i:int.
+ in_safe_int_range i -> round m (from_int i) = from_int i
+
+ predicate same_sign (x:t19) (y:t19) =
+ is_positive x /\ is_positive y \/ is_negative x /\ is_negative y
+
+ predicate diff_sign (x:t19) (y:t19) =
+ is_positive x /\ is_negative y \/ is_negative x /\ is_positive y
+
+ feq_eq :
+ forall x:t19, y:t19.
+ t'isFinite x -> t'isFinite y -> not is_zero x -> x .= y -> x = y
+
+ eq_feq :
+ forall x:t19, y:t19. t'isFinite x -> t'isFinite y -> x = y -> x .= y
+
+ eq_refl : forall x:t19. t'isFinite x -> x .= x
+
+ eq_sym : forall x:t19, y:t19. x .= y -> y .= x
+
+ eq_trans : forall x:t19, y:t19, z:t19. x .= y -> y .= z -> x .= z
+
+ eq_zero : zeroF .= (.- zeroF)
+
+ eq_to_real_finite :
+ forall x:t19, y:t19.
+ t'isFinite x /\ t'isFinite y -> x .= y <-> t'real x = t'real y
+
+ eq_special :
+ forall x:t19, y:t19.
+ x .= y ->
+ is_not_nan x /\
+ is_not_nan y /\
+ (t'isFinite x /\ t'isFinite y \/
+ is_infinite x /\ is_infinite y /\ same_sign x y)
+
+ lt_finite :
+ forall x:t19, y:t19 [lt x y].
+ t'isFinite x /\ t'isFinite y -> lt x y <-> t'real x <. t'real y
+
+ le_finite :
+ forall x:t19, y:t19 [le x y].
+ t'isFinite x /\ t'isFinite y -> le x y <-> t'real x <=. t'real y
+
+ le_lt_trans : forall x:t19, y:t19, z:t19. x .<= y /\ y .< z -> x .< z
+
+ lt_le_trans : forall x:t19, y:t19, z:t19. x .< y /\ y .<= z -> x .< z
+
+ le_ge_asym : forall x:t19, y:t19. x .<= y /\ x .>= y -> x .= y
+
+ not_lt_ge :
+ forall x:t19, y:t19.
+ not x .< y /\ is_not_nan x /\ is_not_nan y -> x .>= y
+
+ not_gt_le :
+ forall x:t19, y:t19.
+ not x .> y /\ is_not_nan x /\ is_not_nan y -> x .<= y
+
+ le_special :
+ forall x:t19, y:t19 [le x y].
+ le x y ->
+ t'isFinite x /\ t'isFinite y \/
+ is_minus_infinity x /\ is_not_nan y \/
+ is_not_nan x /\ is_plus_infinity y
+
+ lt_special :
+ forall x:t19, y:t19 [lt x y].
+ lt x y ->
+ t'isFinite x /\ t'isFinite y \/
+ is_minus_infinity x /\ is_not_nan y /\ not is_minus_infinity y \/
+ is_not_nan x /\ not is_plus_infinity x /\ is_plus_infinity y
+
+ lt_lt_finite : forall x:t19, y:t19, z:t19. lt x y -> lt y z -> t'isFinite y
+
+ positive_to_real :
+ forall x:t19 [is_positive x| t'real x >=. 0.0].
+ t'isFinite x -> is_positive x -> t'real x >=. 0.0
+
+ to_real_positive :
+ forall x:t19 [is_positive x].
+ t'isFinite x -> t'real x >. 0.0 -> is_positive x
+
+ negative_to_real :
+ forall x:t19 [is_negative x| t'real x <=. 0.0].
+ t'isFinite x -> is_negative x -> t'real x <=. 0.0
+
+ to_real_negative :
+ forall x:t19 [is_negative x].
+ t'isFinite x -> t'real x <. 0.0 -> is_negative x
+
+ negative_xor_positive : forall x:t19. not (is_positive x /\ is_negative x)
+
+ negative_or_positive :
+ forall x:t19. is_not_nan x -> is_positive x \/ is_negative x
+
+ diff_sign_trans :
+ forall x:t19, y:t19, z:t19.
+ diff_sign x y /\ diff_sign y z -> same_sign x z
+
+ diff_sign_product :
+ forall x:t19, y:t19.
+ t'isFinite x /\ t'isFinite y /\ (t'real x *. t'real y) <. 0.0 ->
+ diff_sign x y
+
+ same_sign_product :
+ forall x:t19, y:t19.
+ t'isFinite x /\ t'isFinite y /\ same_sign x y ->
+ (t'real x *. t'real y) >=. 0.0
+
+ predicate product_sign (z:t19) (x:t19) (y:t19) =
+ (same_sign x y -> is_positive z) /\ (diff_sign x y -> is_negative z)
+
+ predicate overflow_value (m:mode) (x:t19) =
+ match m with
+ | RTN ->
+ if is_positive x then t'isFinite x /\ t'real x = max_real
+ else is_infinite x
+ | RTP ->
+ if is_positive x then is_infinite x
+ else t'isFinite x /\ t'real x = (-. max_real)
+ | RTZ ->
+ if is_positive x then t'isFinite x /\ t'real x = max_real
+ else t'isFinite x /\ t'real x = (-. max_real)
+ | RNA | RNE -> is_infinite x
+ end
+
+ predicate sign_zero_result (m:mode) (x:t19) =
+ is_zero x -> match m with
+ | RTN -> is_negative x
+ | _ -> is_positive x
+ end
+
+ add_finite :
+ forall m:mode, x:t19, y:t19 [add m x y].
+ t'isFinite x ->
+ t'isFinite y ->
+ no_overflow m (t'real x +. t'real y) ->
+ t'isFinite (add m x y) /\
+ t'real (add m x y) = round m (t'real x +. t'real y)
+
+ add_finite_rev :
+ forall m:mode, x:t19, y:t19 [add m x y].
+ t'isFinite (add m x y) -> t'isFinite x /\ t'isFinite y
+
+ add_finite_rev_n :
+ forall m:mode, x:t19, y:t19 [add m x y].
+ to_nearest m ->
+ t'isFinite (add m x y) ->
+ no_overflow m (t'real x +. t'real y) /\
+ t'real (add m x y) = round m (t'real x +. t'real y)
+
+ sub_finite :
+ forall m:mode, x:t19, y:t19 [sub m x y].
+ t'isFinite x ->
+ t'isFinite y ->
+ no_overflow m (t'real x -. t'real y) ->
+ t'isFinite (sub m x y) /\
+ t'real (sub m x y) = round m (t'real x -. t'real y)
+
+ sub_finite_rev :
+ forall m:mode, x:t19, y:t19 [sub m x y].
+ t'isFinite (sub m x y) -> t'isFinite x /\ t'isFinite y
+
+ sub_finite_rev_n :
+ forall m:mode, x:t19, y:t19 [sub m x y].
+ to_nearest m ->
+ t'isFinite (sub m x y) ->
+ no_overflow m (t'real x -. t'real y) /\
+ t'real (sub m x y) = round m (t'real x -. t'real y)
+
+ mul_finite :
+ forall m:mode, x:t19, y:t19 [mul m x y].
+ t'isFinite x ->
+ t'isFinite y ->
+ no_overflow m (t'real x *. t'real y) ->
+ t'isFinite (mul m x y) /\
+ t'real (mul m x y) = round m (t'real x *. t'real y)
+
+ mul_finite_rev :
+ forall m:mode, x:t19, y:t19 [mul m x y].
+ t'isFinite (mul m x y) -> t'isFinite x /\ t'isFinite y
+
+ mul_finite_rev_n :
+ forall m:mode, x:t19, y:t19 [mul m x y].
+ to_nearest m ->
+ t'isFinite (mul m x y) ->
+ no_overflow m (t'real x *. t'real y) /\
+ t'real (mul m x y) = round m (t'real x *. t'real y)
+
+ div_finite :
+ forall m:mode, x:t19, y:t19 [div m x y].
+ t'isFinite x ->
+ t'isFinite y ->
+ not is_zero y ->
+ no_overflow m (t'real x /. t'real y) ->
+ t'isFinite (div m x y) /\
+ t'real (div m x y) = round m (t'real x /. t'real y)
+
+ div_finite_rev :
+ forall m:mode, x:t19, y:t19 [div m x y].
+ t'isFinite (div m x y) ->
+ t'isFinite x /\ t'isFinite y /\ not is_zero y \/
+ t'isFinite x /\ is_infinite y /\ t'real (div m x y) = 0.0
+
+ div_finite_rev_n :
+ forall m:mode, x:t19, y:t19 [div m x y].
+ to_nearest m ->
+ t'isFinite (div m x y) ->
+ t'isFinite y ->
+ no_overflow m (t'real x /. t'real y) /\
+ t'real (div m x y) = round m (t'real x /. t'real y)
+
+ neg_finite :
+ forall x:t19 [neg x].
+ t'isFinite x -> t'isFinite (neg x) /\ t'real (neg x) = (-. t'real x)
+
+ neg_finite_rev :
+ forall x:t19 [neg x].
+ t'isFinite (neg x) -> t'isFinite x /\ t'real (neg x) = (-. t'real x)
+
+ abs_finite :
+ forall x:t19 [abs1 x].
+ t'isFinite x ->
+ t'isFinite (abs1 x) /\
+ t'real (abs1 x) = abs (t'real x) /\ is_positive (abs1 x)
+
+ abs_finite_rev :
+ forall x:t19 [abs1 x].
+ t'isFinite (abs1 x) -> t'isFinite x /\ t'real (abs1 x) = abs (t'real x)
+
+ abs_universal : forall x:t19 [abs1 x]. not is_negative (abs1 x)
+
+ fma_finite :
+ forall m:mode, x:t19, y:t19, z:t19 [fma m x y z].
+ t'isFinite x ->
+ t'isFinite y ->
+ t'isFinite z ->
+ no_overflow m ((t'real x *. t'real y) +. t'real z) ->
+ t'isFinite (fma m x y z) /\
+ t'real (fma m x y z) = round m ((t'real x *. t'real y) +. t'real z)
+
+ fma_finite_rev :
+ forall m:mode, x:t19, y:t19, z:t19 [fma m x y z].
+ t'isFinite (fma m x y z) -> t'isFinite x /\ t'isFinite y /\ t'isFinite z
+
+ fma_finite_rev_n :
+ forall m:mode, x:t19, y:t19, z:t19 [fma m x y z].
+ to_nearest m ->
+ t'isFinite (fma m x y z) ->
+ no_overflow m ((t'real x *. t'real y) +. t'real z) /\
+ t'real (fma m x y z) = round m ((t'real x *. t'real y) +. t'real z)
+
+ function sqr (x:real) : real = x *''''' x
+
+ function sqrt1 real : real
+
+ axiom Sqrt_positive : forall x:real. x >=' 0.0 -> sqrt1 x >=' 0.0
+
+ axiom Sqrt_square : forall x:real. x >=' 0.0 -> sqr (sqrt1 x) = x
+
+ axiom Square_sqrt : forall x:real. x >=' 0.0 -> sqrt1 (x *''''' x) = x
+
+ axiom Sqrt_mul :
+ forall x:real, y:real.
+ x >=' 0.0 /\ y >=' 0.0 -> sqrt1 (x *''''' y) = (sqrt1 x *''''' sqrt1 y)
+
+ axiom Sqrt_le :
+ forall x:real, y:real. 0.0 <='' x /\ x <='' y -> sqrt1 x <='' sqrt1 y
+
+ (* use real.Square *)
+
+ sqrt_finite :
+ forall m:mode, x:t19 [sqrt m x].
+ t'isFinite x ->
+ t'real x >=. 0.0 ->
+ t'isFinite (sqrt m x) /\ t'real (sqrt m x) = round m (sqrt1 (t'real x))
+
+ sqrt_finite_rev :
+ forall m:mode, x:t19 [sqrt m x].
+ t'isFinite (sqrt m x) ->
+ t'isFinite x /\
+ t'real x >=. 0.0 /\ t'real (sqrt m x) = round m (sqrt1 (t'real x))
+
+ predicate same_sign_real (x:t19) (r:real) =
+ is_positive x /\ r >. 0.0 \/ is_negative x /\ r <. 0.0
+
+ add_special :
+ forall m:mode, x:t19, y:t19 [add m x y].
+ let r = add m x y in
+ (is_nan x \/ is_nan y -> is_nan r) /\
+ (t'isFinite x /\ is_infinite y -> is_infinite r /\ same_sign r y) /\
+ (is_infinite x /\ t'isFinite y -> is_infinite r /\ same_sign r x) /\
+ (is_infinite x /\ is_infinite y /\ same_sign x y ->
+ is_infinite r /\ same_sign r x) /\
+ (is_infinite x /\ is_infinite y /\ diff_sign x y -> is_nan r) /\
+ (t'isFinite x /\
+ t'isFinite y /\ not no_overflow m (t'real x +. t'real y) ->
+ same_sign_real r (t'real x +. t'real y) /\ overflow_value m r) /\
+ (t'isFinite x /\ t'isFinite y ->
+ (if same_sign x y then same_sign r x else sign_zero_result m r))
+
+ sub_special :
+ forall m:mode, x:t19, y:t19 [sub m x y].
+ let r = sub m x y in
+ (is_nan x \/ is_nan y -> is_nan r) /\
+ (t'isFinite x /\ is_infinite y -> is_infinite r /\ diff_sign r y) /\
+ (is_infinite x /\ t'isFinite y -> is_infinite r /\ same_sign r x) /\
+ (is_infinite x /\ is_infinite y /\ same_sign x y -> is_nan r) /\
+ (is_infinite x /\ is_infinite y /\ diff_sign x y ->
+ is_infinite r /\ same_sign r x) /\
+ (t'isFinite x /\
+ t'isFinite y /\ not no_overflow m (t'real x -. t'real y) ->
+ same_sign_real r (t'real x -. t'real y) /\ overflow_value m r) /\
+ (t'isFinite x /\ t'isFinite y ->
+ (if diff_sign x y then same_sign r x else sign_zero_result m r))
+
+ mul_special :
+ forall m:mode, x:t19, y:t19 [mul m x y].
+ let r = mul m x y in
+ (is_nan x \/ is_nan y -> is_nan r) /\
+ (is_zero x /\ is_infinite y -> is_nan r) /\
+ (t'isFinite x /\ is_infinite y /\ not is_zero x -> is_infinite r) /\
+ (is_infinite x /\ is_zero y -> is_nan r) /\
+ (is_infinite x /\ t'isFinite y /\ not is_zero y -> is_infinite r) /\
+ (is_infinite x /\ is_infinite y -> is_infinite r) /\
+ (t'isFinite x /\
+ t'isFinite y /\ not no_overflow m (t'real x *. t'real y) ->
+ overflow_value m r) /\
+ (not is_nan r -> product_sign r x y)
+
+ div_special :
+ forall m:mode, x:t19, y:t19 [div m x y].
+ let r = div m x y in
+ (is_nan x \/ is_nan y -> is_nan r) /\
+ (t'isFinite x /\ is_infinite y -> is_zero r) /\
+ (is_infinite x /\ t'isFinite y -> is_infinite r) /\
+ (is_infinite x /\ is_infinite y -> is_nan r) /\
+ (t'isFinite x /\
+ t'isFinite y /\
+ not is_zero y /\ not no_overflow m (t'real x /. t'real y) ->
+ overflow_value m r) /\
+ (t'isFinite x /\ is_zero y /\ not is_zero x -> is_infinite r) /\
+ (is_zero x /\ is_zero y -> is_nan r) /\
+ (not is_nan r -> product_sign r x y)
+
+ neg_special :
+ forall x:t19 [neg x].
+ (is_nan x -> is_nan (neg x)) /\
+ (is_infinite x -> is_infinite (neg x)) /\
+ (not is_nan x -> diff_sign x (neg x))
+
+ abs_special :
+ forall x:t19 [abs1 x].
+ (is_nan x -> is_nan (abs1 x)) /\
+ (is_infinite x -> is_infinite (abs1 x)) /\
+ (not is_nan x -> is_positive (abs1 x))
+
+ fma_special :
+ forall m:mode, x:t19, y:t19, z:t19 [fma m x y z].
+ let r = fma m x y z in
+ (is_nan x \/ is_nan y \/ is_nan z -> is_nan r) /\
+ (is_zero x /\ is_infinite y -> is_nan r) /\
+ (is_infinite x /\ is_zero y -> is_nan r) /\
+ (t'isFinite x /\ not is_zero x /\ is_infinite y /\ t'isFinite z ->
+ is_infinite r /\ product_sign r x y) /\
+ (t'isFinite x /\ not is_zero x /\ is_infinite y /\ is_infinite z ->
+ (if product_sign z x y then is_infinite r /\ same_sign r z
+ else is_nan r)) /\
+ (is_infinite x /\ t'isFinite y /\ not is_zero y /\ t'isFinite z ->
+ is_infinite r /\ product_sign r x y) /\
+ (is_infinite x /\ t'isFinite y /\ not is_zero y /\ is_infinite z ->
+ (if product_sign z x y then is_infinite r /\ same_sign r z
+ else is_nan r)) /\
+ (is_infinite x /\ is_infinite y /\ t'isFinite z ->
+ is_infinite r /\ product_sign r x y) /\
+ (t'isFinite x /\ t'isFinite y /\ is_infinite z ->
+ is_infinite r /\ same_sign r z) /\
+ (is_infinite x /\ is_infinite y /\ is_infinite z ->
+ (if product_sign z x y then is_infinite r /\ same_sign r z
+ else is_nan r)) /\
+ (t'isFinite x /\
+ t'isFinite y /\
+ t'isFinite z /\ not no_overflow m ((t'real x *. t'real y) +. t'real z) ->
+ same_sign_real r ((t'real x *. t'real y) +. t'real z) /\
+ overflow_value m r) /\
+ (t'isFinite x /\ t'isFinite y /\ t'isFinite z ->
+ (if product_sign z x y then same_sign r z
+ else ((t'real x *. t'real y) +. t'real z) = 0.0 ->
+ (if m = RTN then is_negative r else is_positive r)))
+
+ sqrt_special :
+ forall m:mode, x:t19 [sqrt m x].
+ let r = sqrt m x in
+ (is_nan x -> is_nan r) /\
+ (is_plus_infinity x -> is_plus_infinity r) /\
+ (is_minus_infinity x -> is_nan r) /\
+ (t'isFinite x /\ t'real x <. 0.0 -> is_nan r) /\
+ (is_zero x -> same_sign r x) /\
+ (t'isFinite x /\ t'real x >. 0.0 -> is_positive r)
+
+ of_int_add_exact :
+ forall m:mode, n:mode, i:int, j:int.
+ in_safe_int_range i ->
+ in_safe_int_range j ->
+ in_safe_int_range (i + j) ->
+ eq (of_int m (i + j)) (add n (of_int m i) (of_int m j))
+
+ of_int_sub_exact :
+ forall m:mode, n:mode, i:int, j:int.
+ in_safe_int_range i ->
+ in_safe_int_range j ->
+ in_safe_int_range (i - j) ->
+ eq (of_int m (i - j)) (sub n (of_int m i) (of_int m j))
+
+ of_int_mul_exact :
+ forall m:mode, n:mode, i:int, j:int.
+ in_safe_int_range i ->
+ in_safe_int_range j ->
+ in_safe_int_range (i * j) ->
+ eq (of_int m (i * j)) (mul n (of_int m i) (of_int m j))
+
+ Min_r : forall x:t19, y:t19. y .<= x -> min x y .= y
+
+ Min_l : forall x:t19, y:t19. x .<= y -> min x y .= x
+
+ Max_r : forall x:t19, y:t19. y .<= x -> max x y .= x
+
+ Max_l : forall x:t19, y:t19. x .<= y -> max x y .= y
+
+ predicate is_int t19
+
+ zeroF_is_int : is_int zeroF
+
+ of_int_is_int : forall m:mode, x:int. in_int_range x -> is_int (of_int m x)
+
+ big_float_is_int :
+ forall m:mode, i:t19.
+ t'isFinite i ->
+ i .<= neg (of_int m pow2sb) \/ of_int m pow2sb .<= i -> is_int i
+
+ roundToIntegral_is_int :
+ forall m:mode, x:t19. t'isFinite x -> is_int (roundToIntegral m x)
+
+ eq_is_int : forall x:t19, y:t19. eq x y -> is_int x -> is_int y
+
+ add_int :
+ forall x:t19, y:t19, m:mode.
+ is_int x -> is_int y -> t'isFinite (add m x y) -> is_int (add m x y)
+
+ sub_int :
+ forall x:t19, y:t19, m:mode.
+ is_int x -> is_int y -> t'isFinite (sub m x y) -> is_int (sub m x y)
+
+ mul_int :
+ forall x:t19, y:t19, m:mode.
+ is_int x -> is_int y -> t'isFinite (mul m x y) -> is_int (mul m x y)
+
+ fma_int :
+ forall x:t19, y:t19, z:t19, m:mode.
+ is_int x ->
+ is_int y -> is_int z -> t'isFinite (fma m x y z) -> is_int (fma m x y z)
+
+ neg_int : forall x:t19. is_int x -> is_int (neg x)
+
+ abs_int : forall x:t19. is_int x -> is_int (abs1 x)
+
+ is_int_of_int :
+ forall x:t19, m:mode, m':mode. is_int x -> eq x (of_int m' (to_int m x))
+
+ is_int_to_int : forall m:mode, x:t19. is_int x -> in_int_range (to_int m x)
+
+ is_int_is_finite : forall x:t19. is_int x -> t'isFinite x
+
+ int_to_real :
+ forall m:mode, x:t19. is_int x -> t'real x = from_int (to_int m x)
+
+ truncate_int : forall m:mode, i:t19. is_int i -> roundToIntegral m i .= i
+
+ truncate_neg :
+ forall x:t19.
+ t'isFinite x ->
+ is_negative x -> roundToIntegral RTZ x = roundToIntegral RTP x
+
+ truncate_pos :
+ forall x:t19.
+ t'isFinite x ->
+ is_positive x -> roundToIntegral RTZ x = roundToIntegral RTN x
+
+ ceil_le : forall x:t19. t'isFinite x -> x .<= roundToIntegral RTP x
+
+ ceil_lest :
+ forall x:t19, y:t19. x .<= y /\ is_int y -> roundToIntegral RTP x .<= y
+
+ ceil_to_real :
+ forall x:t19.
+ t'isFinite x ->
+ t'real (roundToIntegral RTP x) = from_int (ceil (t'real x))
+
+ ceil_to_int :
+ forall m:mode, x:t19.
+ t'isFinite x -> to_int m (roundToIntegral RTP x) = ceil (t'real x)
+
+ floor_le : forall x:t19. t'isFinite x -> roundToIntegral RTN x .<= x
+
+ floor_lest :
+ forall x:t19, y:t19. y .<= x /\ is_int y -> y .<= roundToIntegral RTN x
+
+ floor_to_real :
+ forall x:t19.
+ t'isFinite x ->
+ t'real (roundToIntegral RTN x) = from_int (floor (t'real x))
+
+ floor_to_int :
+ forall m:mode, x:t19.
+ t'isFinite x -> to_int m (roundToIntegral RTN x) = floor (t'real x)
+
+ RNA_down :
+ forall x:t19.
+ (x .- roundToIntegral RTN x) .< (roundToIntegral RTP x .- x) ->
+ roundToIntegral RNA x = roundToIntegral RTN x
+
+ RNA_up :
+ forall x:t19.
+ (x .- roundToIntegral RTN x) .> (roundToIntegral RTP x .- x) ->
+ roundToIntegral RNA x = roundToIntegral RTP x
+
+ RNA_down_tie :
+ forall x:t19.
+ (x .- roundToIntegral RTN x) .= (roundToIntegral RTP x .- x) ->
+ is_negative x -> roundToIntegral RNA x = roundToIntegral RTN x
+
+ RNA_up_tie :
+ forall x:t19.
+ (roundToIntegral RTP x .- x) .= (x .- roundToIntegral RTN x) ->
+ is_positive x -> roundToIntegral RNA x = roundToIntegral RTP x
+
+ to_int_roundToIntegral :
+ forall m:mode, x:t19. to_int m x = to_int m (roundToIntegral m x)
+
+ to_int_monotonic :
+ forall m:mode, x:t19, y:t19.
+ t'isFinite x -> t'isFinite y -> le x y -> to_int m x <= to_int m y
+
+ to_int_of_int :
+ forall m:mode, i:int. in_safe_int_range i -> to_int m (of_int m i) = i
+
+ eq_to_int :
+ forall m:mode, x:t19, y:t19.
+ t'isFinite x -> x .= y -> to_int m x = to_int m y
+
+ neg_to_int :
+ forall m:mode, x:t19. is_int x -> to_int m (neg x) = (- to_int m x)
+
+ roundToIntegral_is_finite :
+ forall m:mode, x:t19. t'isFinite x -> t'isFinite (roundToIntegral m x)
+
+ (* clone ieee_float.GenericFloat with type t20 = t19,
+ predicate is_int1 = is_int, predicate same_sign_real1 = same_sign_real,
+ predicate sign_zero_result1 = sign_zero_result,
+ predicate overflow_value1 = overflow_value,
+ predicate product_sign1 = product_sign, predicate diff_sign1 = diff_sign,
+ predicate same_sign1 = same_sign,
+ predicate in_safe_int_range1 = in_safe_int_range,
+ constant pow2sb1 = pow2sb, predicate no_overflow1 = no_overflow,
+ predicate in_int_range1 = in_int_range, predicate in_range1 = in_range,
+ constant emax1 = emax, constant max_int1 = max_int,
+ constant max_real1 = max_real, function round1 = round,
+ function to_int1 = to_int, function of_int1 = of_int,
+ function to_real = t'real, predicate is_not_nan1 = is_not_nan,
+ predicate is_minus_zero1 = is_minus_zero,
+ predicate is_plus_zero1 = is_plus_zero,
+ predicate is_minus_infinity1 = is_minus_infinity,
+ predicate is_plus_infinity1 = is_plus_infinity,
+ predicate is_finite = t'isFinite, predicate is_negative1 = is_negative,
+ predicate is_positive1 = is_positive, predicate is_nan1 = is_nan,
+ predicate is_infinite1 = is_infinite, predicate is_zero1 = is_zero,
+ predicate is_subnormal1 = is_subnormal, predicate is_normal1 = is_normal,
+ predicate (.=') = (.=), predicate (.>') = (.>), predicate (.>=') = (.>=),
+ predicate (.<') = (.<), predicate (.<=') = (.<=), predicate eq1 = eq,
+ predicate gt1 = gt, predicate ge1 = ge, predicate lt1 = lt,
+ predicate le1 = le, function max1 = max, function min1 = min,
+ function roundToIntegral1 = roundToIntegral, function (./') = (./),
+ function (.*') = (.* ), function (.-') = (.-), function (.+') = (.+),
+ function (.-'_) = (.-_), function sqrt2 = sqrt, function fma1 = fma,
+ function neg1 = neg, function abs2 = abs1, function div1 = div,
+ function mul1 = mul, function sub1 = sub, function add1 = add,
+ constant zeroF1 = zeroF, constant sb = t'sb, constant eb = t'eb,
+ prop roundToIntegral_is_finite1 = roundToIntegral_is_finite,
+ prop neg_to_int1 = neg_to_int, prop eq_to_int1 = eq_to_int,
+ prop to_int_of_int1 = to_int_of_int,
+ prop to_int_monotonic1 = to_int_monotonic,
+ prop to_int_roundToIntegral1 = to_int_roundToIntegral,
+ prop RNA_up_tie1 = RNA_up_tie, prop RNA_down_tie1 = RNA_down_tie,
+ prop RNA_up1 = RNA_up, prop RNA_down1 = RNA_down,
+ prop floor_to_int1 = floor_to_int, prop floor_to_real1 = floor_to_real,
+ prop floor_lest1 = floor_lest, prop floor_le1 = floor_le,
+ prop ceil_to_int1 = ceil_to_int, prop ceil_to_real1 = ceil_to_real,
+ prop ceil_lest1 = ceil_lest, prop ceil_le1 = ceil_le,
+ prop truncate_pos1 = truncate_pos, prop truncate_neg1 = truncate_neg,
+ prop truncate_int1 = truncate_int, prop int_to_real1 = int_to_real,
+ prop is_int_is_finite1 = is_int_is_finite,
+ prop is_int_to_int1 = is_int_to_int, prop is_int_of_int1 = is_int_of_int,
+ prop abs_int1 = abs_int, prop neg_int1 = neg_int,
+ prop fma_int1 = fma_int, prop mul_int1 = mul_int,
+ prop sub_int1 = sub_int, prop add_int1 = add_int,
+ prop eq_is_int1 = eq_is_int,
+ prop roundToIntegral_is_int1 = roundToIntegral_is_int,
+ prop big_float_is_int1 = big_float_is_int,
+ prop of_int_is_int1 = of_int_is_int, prop zeroF_is_int1 = zeroF_is_int,
+ prop Max_l1 = Max_l, prop Max_r1 = Max_r, prop Min_l1 = Min_l,
+ prop Min_r1 = Min_r, prop of_int_mul_exact1 = of_int_mul_exact,
+ prop of_int_sub_exact1 = of_int_sub_exact,
+ prop of_int_add_exact1 = of_int_add_exact,
+ prop sqrt_special1 = sqrt_special, prop fma_special1 = fma_special,
+ prop abs_special1 = abs_special, prop neg_special1 = neg_special,
+ prop div_special1 = div_special, prop mul_special1 = mul_special,
+ prop sub_special1 = sub_special, prop add_special1 = add_special,
+ prop sqrt_finite_rev1 = sqrt_finite_rev, prop sqrt_finite1 = sqrt_finite,
+ prop fma_finite_rev_n1 = fma_finite_rev_n,
+ prop fma_finite_rev1 = fma_finite_rev, prop fma_finite1 = fma_finite,
+ prop abs_universal1 = abs_universal,
+ prop abs_finite_rev1 = abs_finite_rev, prop abs_finite1 = abs_finite,
+ prop neg_finite_rev1 = neg_finite_rev, prop neg_finite1 = neg_finite,
+ prop div_finite_rev_n1 = div_finite_rev_n,
+ prop div_finite_rev1 = div_finite_rev, prop div_finite1 = div_finite,
+ prop mul_finite_rev_n1 = mul_finite_rev_n,
+ prop mul_finite_rev1 = mul_finite_rev, prop mul_finite1 = mul_finite,
+ prop sub_finite_rev_n1 = sub_finite_rev_n,
+ prop sub_finite_rev1 = sub_finite_rev, prop sub_finite1 = sub_finite,
+ prop add_finite_rev_n1 = add_finite_rev_n,
+ prop add_finite_rev1 = add_finite_rev, prop add_finite1 = add_finite,
+ prop same_sign_product1 = same_sign_product,
+ prop diff_sign_product1 = diff_sign_product,
+ prop diff_sign_trans1 = diff_sign_trans,
+ prop negative_or_positive1 = negative_or_positive,
+ prop negative_xor_positive1 = negative_xor_positive,
+ prop to_real_negative1 = to_real_negative,
+ prop negative_to_real1 = negative_to_real,
+ prop to_real_positive1 = to_real_positive,
+ prop positive_to_real1 = positive_to_real,
+ prop lt_lt_finite1 = lt_lt_finite, prop lt_special1 = lt_special,
+ prop le_special1 = le_special, prop not_gt_le1 = not_gt_le,
+ prop not_lt_ge1 = not_lt_ge, prop le_ge_asym1 = le_ge_asym,
+ prop lt_le_trans1 = lt_le_trans, prop le_lt_trans1 = le_lt_trans,
+ prop le_finite1 = le_finite, prop lt_finite1 = lt_finite,
+ prop eq_special1 = eq_special,
+ prop eq_to_real_finite1 = eq_to_real_finite, prop eq_zero1 = eq_zero,
+ prop eq_trans1 = eq_trans, prop eq_sym1 = eq_sym,
+ prop eq_refl1 = eq_refl, prop eq_feq1 = eq_feq, prop feq_eq1 = feq_eq,
+ prop Exact_rounding_for_integers1 = Exact_rounding_for_integers,
+ prop pow2sb = pow2sb1, prop Round_up_neg1 = Round_up_neg,
+ prop Round_down_neg1 = Round_down_neg, prop Round_up_ge1 = Round_up_ge,
+ prop Round_down_le1 = Round_down_le, prop Round_to_real1 = Round_to_real,
+ prop Round_idempotent1 = Round_idempotent,
+ prop Round_monotonic1 = Round_monotonic,
+ prop Bounded_real_no_overflow1 = Bounded_real_no_overflow,
+ prop is_finite1 = is_finite, prop max_real_int1 = max_real_int,
+ prop max_int = max_int1, prop zero_of_int1 = zero_of_int,
+ prop zero_to_real1 = zero_to_real, prop zeroF_is_zero1 = zeroF_is_zero,
+ prop zeroF_is_positive1 = zeroF_is_positive,
+ prop is_not_finite1 = is_not_finite, prop is_not_nan1 = is_not_nan,
+ prop sb_gt_1 = sb_gt_11, prop eb_gt_1 = eb_gt_11, *)
+
+ round_bound_ne :
+ forall x:real [round RNE x].
+ no_overflow RNE x ->
+ ((x -' (0x1.0p-53 *''''' abs x)) -' 0x1.0p-1075) <='' round RNE x /\
+ round RNE x
+ <='' ((x +''''' (0x1.0p-53 *''''' abs x)) +''''' 0x1.0p-1075)
+
+ round_bound :
+ forall m:mode, x:real [round m x].
+ no_overflow m x ->
+ ((x -' (0x1.0p-52 *''''' abs x)) -' 0x1.0p-1074) <='' round m x /\
+ round m x <='' ((x +''''' (0x1.0p-52 *''''' abs x)) +''''' 0x1.0p-1074)
+
+ (* use ieee_float.Float64 *)
+
+ type input_type = t19
+
+ (* use caisar.NNet *)
+
+ type tuple5 'a 'a1 'a2 'a3 'a4 =
+ | Tuple5 'a 'a1 'a2 'a3 'a4
+
+ (* use why3.Tuple5.Tuple51 *)
+
+ function nnet_apply t19 t19 t19 t19 t19 : (t19, t19, t19, t19, t19)
+
+ (* use As_tuple *)
+
goal G :
- forall x1:int, x2:int, x3:int, x4:int, x5:int.
- match out x1 x2 x3 x4 x5 with
- | y1, _, _, _, _ -> 0 < y1 /\ y1 < 10
+ forall x1:t19, x2:t19, x3:t19, x4:t19, x5:t19.
+ match nnet_apply x1 x2 x3 x4 x5 with
+ | y1, _, _, _, _ -> 0.0 <. t'real y1 /\ t'real y1 <. 0.1
end
end