ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

cleaning

Browse Source
This commit is contained in:
Claude Marche
2025-11-24 11:22:11 +01:00
parent 9c60b5f0d6
commit 13410bfc8f
4 changed files with 269 additions and 278 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
examples/numeric/log-sum-exp.mlw
View File

@@ -423,7 +423,7 @@ module SLSE
begin ensures {
abs (to_real u_a -. a) <=. 2. *. eps *. a'
}
UFloatLemmas.usub_double_error_propagation (uadd x rho) y u_a
UFloatLemmas.usub_error_propagation (uadd x rho) y u_a
(to_real x +. to_real rho) (abs (to_real x +. to_real rho))
eps 0.0 (to_real y) (abs (to_real y)) 0.0 0.0;
end;
@@ -434,7 +434,7 @@ module SLSE
begin ensures {
abs (to_real u_b -. b) <=. 2.0 *. a_eps *. b' +. eta
}
UFloatLemmas.umul_double_error_propagation u_a u_a u_b
UFloatLemmas.umul_error_propagation u_a u_a u_b
a a' (2. *. eps) 0.0 a a' (2. *. eps) 0.0
end;
let c = b /. 2.0 in
@@ -444,7 +444,7 @@ module SLSE
begin ensures {
abs (to_real u_c -. c) <=. a_eps *. c' +. 1.5 *. eta
}
UFloatLemmas.udiv_exact_double_error_propagation u_b utwo u_c b b' (2.0 *. a_eps) eta
UFloatLemmas.udiv_exact_error_propagation u_b utwo u_c b b' (2.0 *. a_eps) eta
end;
let d = -. c in
let u_d = uminus u_c in
@@ -458,10 +458,11 @@ module SLSE
begin ensures { d' <=. sqr (2.0 *. a_max +. abs (to_real rho)) }
sqr_ge a' (2.0 *. a_max +. abs (to_real rho))
end;
assert { (0.5 +. a_eps) *. d' <=. (0.5 +. a_eps) *. sqr (2.0 *. a_max +. abs (to_real rho)) };
assert { abs (to_real u_d)
<=. abs d +. a_eps *. d' +. 1.5 *. eta
<=. (0.5 +. a_eps) *. d' +. 1.5 *. eta
<=. (0.5 +. a_eps) *. sqr (2.0 *. a_max +. abs (to_real rho)) +. 1.5 *. eta
<=. (0.5 +. a_eps) *. sqr (2.0 *. a_max +. abs (to_real rho)) +. 1.5 *. eta
<=. exp_max_value
};
()
@@ -473,7 +474,7 @@ module SLSE
begin ensures {
abs (to_real u_e -. e) <=. error *. e
}
UFloatLemmas.exp_double_error_propagation u_e u_d d d' exp_error 0.0 a_eps (1.5 *. eta);
UFloatLemmas.exp_error_propagation u_e u_d d d' exp_error 0.0 a_eps (1.5 *. eta);
end;
assert { u_g x y rho = u_e };
assert { g x y rho = e }
@@ -635,7 +636,7 @@ let ghost slse_accuracy (a:int -> u) (n:int) (rho:u) (a_max:real)
by slse_hypothesis rho a_max n }
end
end;
UFloatLemmas.log2_double_error_propagation_simple
UFloatLemmas.log2_error_propagation_simple
(u_log2 (u_sum (u_gi a rho i) n))
(u_sum (u_gi a rho i) n)
(sum (gi a rho i) 0 n)

463
examples/numeric/log-sum-exp/why3session.xml
View File

File diff suppressed because it is too large Load Diff

BIN
examples/numeric/log-sum-exp/why3shapes.gz
View File

Binary file not shown.

71
stdlib/ufloat.mlw
View File

@@ -387,7 +387,7 @@ module UFloatLemmas
use real.Abs
use UFloat
let lemma uadd_double_error_propagation (x_f y_f r : u) (x x_factor x_rel x_abs y y_factor y_rel y_abs : real)
let lemma uadd_error_propagation (x_f y_f r : u) (x x_factor x_rel x_abs y y_factor y_rel y_abs : real)
requires {
abs (to_real x_f -. x) <=. x_rel *. x_factor +. x_abs
}
@@ -459,49 +459,8 @@ module UFloatLemmas
}
end
end
(*
assert {
0. <=. x_rel /\ 0. <=. y_rel ->
delta <=.
(eps +. y_rel) *. x_factor +. (eps +. x_rel) *. y_factor
+. (x_rel +. eps) *. y_abs +. (y_rel +. eps) *. x_abs
by
(delta <=. x_factor *. x_rel +. x_abs +. x_factor
so
x_factor +. x_abs <=. eps *. (y_factor +. y_abs) ->
delta <=. (eps +. x_rel) *. y_factor
+. (eps +. y_rel) *. x_factor
+. (y_rel +. eps) *. x_abs +. (x_rel +. eps) *. y_abs
by
delta <=. eps *. (y_factor +. y_abs) *. x_rel
+. (eps *. (y_factor +. y_abs)))
/\
(delta <=. y_factor *. y_rel +. y_abs +. y_factor
so
abs y_factor +. y_abs <=. eps *. (x_factor +. x_abs) ->
delta <=. (eps +. y_rel) *. x_factor
+. (eps +. x_rel) *. y_factor
+. (x_rel +. eps) *. y_abs +. (y_rel +. eps) *. x_abs
by
delta <=. eps *. (x_factor +. x_abs) *. y_rel
+. (eps *. (x_factor +. x_abs)))
/\
(
(eps *. (x_factor +. x_abs) <. abs y_factor +. y_abs /\
eps *. (y_factor +. y_abs) <. abs x_factor +. x_abs) ->
(delta <=.
(eps +. y_rel) *. x_factor +. (eps +. x_rel) *. y_factor
+. (x_rel +. eps) *. y_abs +. (y_rel +. eps) *. x_abs
by
abs (to_real x_f +. to_real y_f) <=.
abs (to_real x_f -. x) +. x_factor +. (abs (to_real y_f -. y) +. y_factor)
so
x_factor *. x_rel <=. (y_factor +. y_abs) /. eps *. x_rel /\
y_factor *. y_rel <=. (x_factor +. x_abs) /. eps *. y_rel))
}
*)
let lemma usub_double_error_propagation (x_f y_f r : u) (x x_factor x_rel x_abs y y_factor y_rel y_abs : real)
let lemma usub_error_propagation (x_f y_f r : u) (x x_factor x_rel x_abs y y_factor y_rel y_abs : real)
requires {
abs (to_real x_f -. x) <=. x_rel *. x_factor +. x_abs
}
@@ -520,11 +479,11 @@ module UFloatLemmas
<=. (x_rel +. y_rel +. eps) *. (x_factor +. y_factor)
+. ((1. +. eps +. y_rel) *. x_abs +. (1. +. eps +. x_rel) *. y_abs)
}
= uadd_double_error_propagation x_f (--. y_f) r x x_factor x_rel x_abs (-. y) y_factor y_rel y_abs
= uadd_error_propagation x_f (--. y_f) r x x_factor x_rel x_abs (-. y) y_factor y_rel y_abs
use HelperLemmas
let lemma umul_double_error_propagation (x_f y_f r : u)
let lemma umul_error_propagation (x_f y_f r : u)
(x x_factor x_rel x_abs : real) (y y_factor y_rel y_abs : real) : unit
requires {
abs (to_real x_f -. x) <=. x_rel *. x_factor +. x_abs
@@ -558,7 +517,7 @@ module UFloatLemmas
use real.ExpLog
let lemma log_double_error_propagation (logx_f x_f : u)
let lemma log_error_propagation (logx_f x_f : u)
(x_exact x_factor log_rel log_abs x_rel x_abs : real)
requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs }
requires {
@@ -581,7 +540,7 @@ module UFloatLemmas
<=. (abs (log (x_exact)) -. log (1.0 -. (((x_rel *. x_factor) +. x_abs) /. x_exact))) *. log_rel
}
let lemma log2_double_error_propagation (log2x_f x_f : u)
let lemma log2_error_propagation (log2x_f x_f : u)
(x_exact x_factor log_rel log_abs x_rel x_abs : real)
requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs }
requires {
@@ -604,7 +563,7 @@ module UFloatLemmas
<=. (abs (log2 (x_exact)) -. log2 (1.0 -. (((x_rel *. x_factor) +. x_abs) /. x_exact))) *. log_rel
}
let lemma log2_double_error_propagation_simple (log2x_f x_f : u)
let lemma log2_error_propagation_simple (log2x_f x_f : u)
(x_exact log_rel x_rel : real)
requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_exact }
requires {
@@ -619,9 +578,9 @@ module UFloatLemmas
<=. log_rel *. abs (log2 x_exact) -. log2 (1. -. x_rel) *. (1. +. log_rel)
}
=
log2_double_error_propagation log2x_f x_f x_exact x_exact log_rel 0.0 x_rel 0.0
log2_error_propagation log2x_f x_f x_exact x_exact log_rel 0.0 x_rel 0.0
let lemma log10_double_error_propagation (log10x_f x_f : u)
let lemma log10_error_propagation (log10x_f x_f : u)
(x_exact x_factor log_rel log_abs x_rel x_abs : real)
requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs }
requires {
@@ -644,7 +603,7 @@ module UFloatLemmas
<=. (abs (log10 (x_exact)) -. log10 (1.0 -. (((x_rel *. x_factor) +. x_abs) /. x_exact))) *. log_rel
}
let lemma exp_double_error_propagation (expx_f x_f : u)
let lemma exp_error_propagation (expx_f x_f : u)
(x_exact x_factor exp_rel exp_abs x_rel x_abs : real)
requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs }
requires {
@@ -680,7 +639,7 @@ module UFloatLemmas
use real.Trigonometry
let lemma sin_double_error_propagation (sinx_f x_f : u)
let lemma sin_error_propagation (sinx_f x_f : u)
(x_exact x_factor sin_rel sin_abs x_rel x_abs : real)
requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs }
requires {
@@ -700,7 +659,7 @@ module UFloatLemmas
<=. (abs (sin x_exact) +. (x_rel *. x_factor +. x_abs)) *. sin_rel
}
let lemma cos_double_error_propagation (cosx_f x_f : u)
let lemma cos_error_propagation (cosx_f x_f : u)
(x_exact x_factor cos_rel cos_abs x_rel x_abs : real)
requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs }
requires {
@@ -726,7 +685,7 @@ module UFloatLemmas
function real_fun (f:int -> u) : int -> real = fun i -> to_real (f i)
let lemma sum_double_error_propagation (x : u)
let lemma sum_error_propagation (x : u)
(f : int -> u) (f_exact f_factor f_factor' : int -> real) (n:int)
(sum_rel sum_abs f_rel f_abs : real)
requires {
@@ -757,7 +716,7 @@ module UFloatLemmas
}
(* We don't have an error on y_f because in practice we won't have an exact division with an approximate divisor *)
let lemma udiv_exact_double_error_propagation (x_f y_f r: u) (x x_factor x_rel x_abs : real)
let lemma udiv_exact_error_propagation (x_f y_f r: u) (x x_factor x_rel x_abs : real)
requires {
abs (to_real x_f -. x) <=. x_rel *. x_factor +. x_abs
}
@@ -804,6 +763,8 @@ module UFloatLemmas
in ()
end
(** {2 Single propagation lemmas} *)
module USingleLemmas