Commit 48265055 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix incorrect error bounds.

Alt-Ergo was actually able to derive an inconsistency from these axioms,
which is kind of incredible.
parent 3a3f35bb
......@@ -837,9 +837,13 @@ theory Float32
(* axiom half_bv: half = from_bv (BV32.of_uint 0x3F00_0000) *)
lemma round_bound : (* /!\ check the impact of the rounding mode /!\ *)
lemma round_bound_ne :
forall x:real [round RNE x].
x - 0x1p-24 * Abs.abs(x) - 0x1p-150 <= round RNE x <= x + 0x1p-24 * Abs.abs(x) + 0x1p-150
lemma round_bound :
forall m:mode, x:real [round m x].
x - 0x1p-24 * Abs.abs(x) - 0x1p-150 <= round m x <= x + 0x1p-24 * Abs.abs(x) + 0x1p-150
x - 0x1p-23 * Abs.abs(x) - 0x1p-149 <= round m x <= x + 0x1p-23 * Abs.abs(x) + 0x1p-149
end
theory Float64
......@@ -862,9 +866,13 @@ theory Float64
(* axiom half_bv: half = from_bv (BV64.of_uint 0x3FE0_0000_0000_0000) *)
axiom round_bound :
lemma round_bound_ne :
forall x:real [round RNE x].
x - 0x1p-53 * Abs.abs(x) - 0x1p-1075 <= round RNE x <= x + 0x1p-53 * Abs.abs(x) + 0x1p-1075
lemma round_bound :
forall m:mode, x:real [round m x].
x - 0x1p-53 * Abs.abs(x) - 0x1p-1075 <= round m x <= x + 0x1p-53 * Abs.abs(x) + 0x1p-1075
x - 0x1p-52 * Abs.abs(x) - 0x1p-1074 <= round m x <= x + 0x1p-52 * Abs.abs(x) + 0x1p-1074
end
theory FloatConverter
......
Supports Markdown
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