1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
module MultiplicationSingle
use real.RealInfix
use real.Abs
use ufloat.USingle
use ufloat.USingleLemmas
let multiplication_errors_basic (a b c : usingle)
ensures {
let exact = to_real a *. to_real b *. to_real c in
abs (to_real result -. exact) <=.
(2. +. eps) *. eps *. abs exact +. eta *. (abs (to_real c) *. (1. +. eps) +. 1.)
}
= a **. b **. c
let multiplication_errors (a b c d e f: usingle)
ensures {
let t = 1.0 +. eps in
let t3 = eps +. (eps *. t) in
let t4 = to_real d *. (to_real e *. to_real f) in
let t5 = (to_real a *. to_real b) *. to_real c in
let t6 = ((eta *. abs (to_real d)) *. t) +. eta in
let t7 = ((eta *. abs (to_real c)) *. t) +. eta in
let exact = t5 *. t4 in
abs (to_real result -. exact) <=.
(* Relative part of the error *)
(eps +. (t3 +. t3 +. (t3 *. t3)) *. t) *. abs exact +.
(* Absolute part of the error *)
((t6 +. t6 *. t3) *. abs t5 +.
(t7 +. t7 *. t3) *. abs t4 +. t7 *. t6)
*. t +. eta
}
= (a **. b **. c) **. (d **. (e **. f))
end
module MultiplicationDouble
use real.RealInfix
use real.Abs
use ufloat.UDouble
use ufloat.UDoubleLemmas
let multiplication_errors_basic (a b c : udouble)
ensures {
let exact = to_real a *. to_real b *. to_real c in
abs (to_real result -. exact) <=.
(2. +. eps) *. eps *. abs exact +. eta *. (abs (to_real c) *. (1. +. eps) +. 1.)
}
= a **. b **. c
let multiplication_errors (a b c d e f: udouble)
ensures {
let t = 1.0 +. eps in
let t3 = eps +. (eps *. t) in
let t4 = to_real d *. (to_real e *. to_real f) in
let t5 = (to_real a *. to_real b) *. to_real c in
let t6 = ((eta *. abs (to_real d)) *. t) +. eta in
let t7 = ((eta *. abs (to_real c)) *. t) +. eta in
let exact = t5 *. t4 in
abs (to_real result -. exact) <=.
(* Relative part of the error *)
(eps +. (t3 +. t3 +. (t3 *. t3)) *. t) *. abs exact +.
(* Absolute part of the error *)
((t6 +. t6 *. t3) *. abs t5 +.
(t7 +. t7 *. t3) *. abs t4 +. t7 *. t6)
*. t +. eta
}
= (a **. b **. c) **. (d **. (e **. f))
end
|
