Commit 9aa4cb8e by ntmtuyen

### missing proofs

parent 63e2334f
 theory Div use import int.Int use export int.EuclideanDivision (* lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0 lemma Mod_0: forall y:int. y <> 0 -> mod 0 y = 0 *) end theory Pow2int use import int.Int ... ... @@ -133,6 +121,33 @@ theory Pow2real end theory Div use import int.Int use export int.EuclideanDivision use import Pow2int lemma Div_inf1: forall x y:int. 0 <= x < y -> div x y = 0 lemma Div_inf_neg: forall x y:int. 0 < x <= y -> div (-x) y = -1 lemma Div_pow: forall x i:int. pow2 (i-1) <= x < pow2 i -> div x (pow2 (i-1)) = 1 lemma Div_pow2: forall x i:int. -pow2 i <= x < -pow2 (i-1) -> div x (pow2 (i-1)) = -2 lemma Mod_01: forall y:int. y <> 0 -> mod 0 y = 0 lemma Mod_1y: forall y:int. y > 1 -> mod 1 y = 1 lemma Mod_neg1y: forall y:int. y > 1 -> mod (-1) y = 1 lemma Mod_pow2: forall x i:int. mod (x + pow2 i) 2 = mod x 2 end theory BitVector use export bool.Bool ... ... @@ -331,7 +346,7 @@ theory BitVector lemma to_nat_of_zero: forall b:bv, i j:int. size > j /\ i >= 0 -> forall b:bv, i j:int. size > j >= i >= 0 -> (forall k:int. j >= k >= i -> nth b k = False) -> to_nat_sub b j i = 0 ... ... @@ -628,13 +643,14 @@ theory TestNegAsXOR use import real.RealInfix function j : bv = from_int 0x8000000000000000 (* lemma Nth_j: forall i:int. 0 <= i <= 62 -> nth j i = False lemma sign_of_j: sign(j) = True lemma mantissa_of_j: mantissa(j) = 0 lemma exp_of_j: exp(j) = 0 lemma int_of_bv: double_of_bv64(j) = 0.0 *) lemma MainResultBits : forall x:bv. forall i:int. 0 <= i < 63 -> nth (bw_xor x j) i = nth x i ... ... @@ -652,6 +668,7 @@ theory TestNegAsXOR lemma sign_neg: forall x:bv. sign_value(notb(sign(x))) = -.sign_value(sign(x)) lemma MainResult : forall x:bv. 0 < exp(x) < 2047 -> double_of_bv64 (bw_xor x j) = -. double_of_bv64 x ... ... @@ -709,10 +726,7 @@ theory TestDoubleOfInt lemma exp_const: exp(const) = 1075 lemma to_nat_mantissa_1: (BV64.to_nat_sub const 30 0) = 0 lemma mantissa_const_nth2: forall i:int. 32 <= i <= 51 -> BV64.nth const i = False lemma to_nat_mantissa: (BV64.to_nat_sub const 30 0) = 0 lemma mantissa_const_to_nat51: BV64.to_nat_sub const 51 0 = BV64.to_nat_sub const 31 0 ... ... @@ -736,9 +750,9 @@ theory TestDoubleOfInt (* var_as_double(x) : real = double_of_bv64(var(x)) *) (*********************************************************************) function jpxor(i:int): BV32.bv = (BV32.bw_xor j' (BV32.from_int2c i)) function jpxor(x:int): BV32.bv = (BV32.bw_xor j' (BV32.from_int2c x)) function var(i:int): BV64.bv = (BV32_64.concat j (jpxor i)) function var(x:int): BV64.bv = (BV32_64.concat j (jpxor x)) function var_as_double(x:int) : real = double_of_bv64 (var x) ... ... @@ -748,57 +762,48 @@ theory TestDoubleOfInt predicate is_int32(x:int) = - Pow2int.pow2 31 <= x < Pow2int.pow2 31 (* lemma two_compl_pos: forall x:int. is_int32 x /\ x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = x lemma two_compl_neg: forall x:int. is_int32 x /\ x < 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = Pow2int.pow2 32 + x *) (* bits of jpxor x *) lemma nth_0_30: forall x:int. forall i:int. is_int32(x) /\ 0<=i<=30 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) i = BV32.nth (BV32.from_int2c x) i BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) i = BV32.nth (BV32.from_int2c x) i lemma nth_jpxor_0_30: forall x:int. forall i:int. is_int32(x) /\ 0<=i<=30 -> BV32.nth (jpxor x) i = BV32.nth (BV32.from_int2c x) i BV32.nth (jpxor x) i = BV32.nth (BV32.from_int2c x) i lemma nth_var31: forall x:int. (BV32.nth (jpxor x) 31) = notb (BV32.nth (BV32.from_int2c x) 31) lemma to_nat_sub_0_30: forall x:int. is_int32(x) -> (BV32.to_nat_sub (BV32.bw_xor j' (BV32.from_int2c x)) 30 0) = (BV32.to_nat_sub (BV32.from_int2c x) 30 0) (BV32.to_nat_sub (BV32.bw_xor j' (BV32.from_int2c x)) 30 0) = (BV32.to_nat_sub (BV32.from_int2c x) 30 0) (* case x >= 0 *) lemma jpxorx_pos: forall x:int. x>=0 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = True (* lemma from_int2c_to_nat_sub31: forall x:int. x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = x *) lemma from_int2c_to_nat_sub_gen: forall i:int. 0 <= i <= 30 -> lemma from_int2c_to_nat_sub_pos: forall i:int. 0 <= i <= 31 -> forall x:int. 0 <= x < Pow2int.pow2 i -> BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = x lemma from_int2c_to_nat_sub: forall x:int. is_int32(x) /\ x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 30 0 = x lemma lemma1_pos : forall x:int. is_int32 x /\ x >= 0 -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x lemma lemma1_pos : forall x:int. is_int32 x /\ x >= 0 -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x (* case x < 0 *) lemma to_nat_sub_0_30_neg: forall x:int. is_int32(x) /\ x<0 -> (BV32.to_nat_sub (BV32.bw_xor j' (BV32.from_int2c x)) 30 0) = (BV32.to_nat_sub (BV32.from_int2c x) 30 0) lemma to_nat_sub_0_30_neg1: forall x:int. is_int32(x) /\ x<0 -> (BV32.to_nat_sub (BV32.from_int2c x) 30 0) = Pow2int.pow2 31 + x lemma jpxorx_neg: forall x:int. x<0 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = False lemma lemma1_neg : forall x:int. is_int32 x /\ x < 0 -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x lemma from_int2c_to_nat_sub_neg: forall i:int. 0 <= i <= 31 -> forall x:int. -Pow2int.pow2 i <= x < 0 -> BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = Pow2int.pow2 i + x lemma lemma1_neg : forall x:int. is_int32 x /\ x < 0 -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x (* final lemma *) lemma lemma1 : forall x:int. is_int32 x -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x lemma lemma1 : forall x:int. is_int32 x -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x (*********************************************************************) (* lemma 2: for all integer x, mantissa(var(x)) = 2^31 + x *) ... ... @@ -806,26 +811,39 @@ theory TestDoubleOfInt lemma nth_var_0_31: forall x:int. forall i:int. is_int32(x) /\ 0<=i<=31-> BV64.nth (var x) i = BV32.nth (jpxor x) i lemma to_nat_bv32_bv64_aux: forall b1:BV32.bv. forall b2:BV32.bv. forall j:int. 0<=j<32-> BV64.to_nat_sub (BV32_64.concat b1 b2) j 0 = BV32.to_nat_sub b2 j 0 lemma to_nat_bv32_bv64: forall b1:BV32.bv. forall b2:BV32.bv. BV64.to_nat_sub (BV32_64.concat b1 b2) 31 0 = BV32.to_nat_sub b2 31 0 lemma to_nat_bv32_bv64_aux: forall b1:BV32.bv. forall b2:BV32.bv. forall j:int. 0<=j<32-> BV64.to_nat_sub (BV32_64.concat b1 b2) j 0 = BV32.to_nat_sub b2 j 0 lemma to_nat_bv32_bv64: forall b1:BV32.bv. forall b2:BV32.bv. BV64.to_nat_sub (BV32_64.concat b1 b2) 31 0 = BV32.to_nat_sub b2 31 0 lemma to_nat_var_0_31: forall x:int. is_int32(x) -> BV64.to_nat_sub (var x) 31 0 = BV32.to_nat_sub (jpxor x) 31 0 BV64.to_nat_sub (var x) 31 0 = BV32.to_nat_sub (jpxor x) 31 0 lemma nth_var32to63: forall x k:int. 32 <= k <= 63 -> BV64.nth (var x) k = BV32.nth j (k - 32) forall x k:int. 32 <= k <= 63 -> BV64.nth (var x) k = BV32.nth j (k - 32) lemma nth_var3: forall x:int. forall i:int. 32 <= i <= 51 -> BV64.nth (var x) i = False lemma nth_var3: forall x:int. forall i:int. 32 <= i <= 51 -> BV64.nth (var x) i = False lemma lemma2 : forall x:int. is_int32 x -> mantissa(var(x)) = Pow2int.pow2 31 + x lemma lemma2 : forall x:int. is_int32 x -> mantissa(var(x)) = Pow2int.pow2 31 + x (*********************************************************************) (* lemma 3: for all integer x, exp(var(x)) = 1075 *) (*********************************************************************) lemma nth_var4: forall x:int. forall i:int. 52 <= i <= 53 -> BV64.nth (var x) i = True lemma nth_var5: forall x:int. forall i:int. 54 <= i <= 55 -> BV64.nth (var x) i = False lemma nth_var6: forall x:int. forall i:int. 56 <= i <= 57 -> BV64.nth (var x) i = True lemma nth_var7: forall x:int. forall i:int. 58 <= i <= 61 -> BV64.nth (var x) i = False lemma nth_var4: forall x:int. forall i:int. 52 <= i <= 53 -> BV64.nth (var x) i = True lemma nth_var5: forall x:int. forall i:int. 54 <= i <= 55 -> BV64.nth (var x) i = False lemma nth_var6: forall x:int. forall i:int. 56 <= i <= 57 -> BV64.nth (var x) i = True lemma nth_var7: forall x:int. forall i:int. 58 <= i <= 61 -> BV64.nth (var x) i = False lemma nth_var8: forall x:int. BV64.nth (var x) 62 = True lemma lemma3 : forall x:int. exp(var(x)) = 1075 ... ... @@ -842,29 +860,29 @@ theory TestDoubleOfInt (* lemma 5: for all integer x, var_as_double(x) = 2^52 + 2^31 + x *) (*********************************************************************) lemma sign_var: forall x:int. sign(var(x)) = False (*proved by Coq*) lemma var_value0: forall x:int. is_int32(x) ->var_as_double(x) = Pow2real.pow2 (1075 - 1023) *. (1.0 +. (from_int (Pow2int.pow2 31 + x)) *. Pow2real.pow2 (-52)) lemma var_value0: forall x:int. is_int32(x) -> var_as_double(x) = Pow2real.pow2 (1075 - 1023) *. (1.0 +. (from_int (Pow2int.pow2 31 + x)) *. Pow2real.pow2 (-52)) lemma from_int_sum : forall x:int. is_int32(x)-> from_int (Pow2int.pow2 31 + x) = from_int (Pow2int.pow2 31) +. from_int x lemma var_value3: forall x:int. is_int32(x)->var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 52 *. (from_int (Pow2int.pow2 31) +. from_int x) *. Pow2real.pow2 (-52) lemma from_int_sum : forall x:int. is_int32(x)-> from_int (Pow2int.pow2 31 + x) = from_int (Pow2int.pow2 31) +. from_int x lemma var_value3: forall x:int. is_int32(x)-> var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 52 *. (from_int (Pow2int.pow2 31) +. from_int x) *. Pow2real.pow2 (-52) lemma distr_pow52 : forall x:real. Pow2real.pow2 52 *. x *. Pow2real.pow2 (-52) = x Pow2real.pow2 52 *. x *. Pow2real.pow2 (-52) = x lemma var_value4: forall x:int. is_int32(x)->var_as_double(x) = Pow2real.pow2 52 +. (from_int (Pow2int.pow2 31)) +. from_int x lemma var_value4: forall x:int. is_int32(x)-> var_as_double(x) = Pow2real.pow2 52 +. (from_int (Pow2int.pow2 31)) +. from_int x lemma pow31 : from_int (Pow2int.pow2 31) = Pow2real.pow2 31 lemma lemma5: forall x:int. is_int32(x)-> var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 31 +. (from_int x) lemma lemma5: forall x:int. is_int32(x)-> var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 31 +. (from_int x) (*********************************************************************) (* main result *) ... ... @@ -874,7 +892,6 @@ theory TestDoubleOfInt lemma MainResult: forall x:int. is_int32 x -> double_of_int32 x = from_int x end (* ... ...
 ... ... @@ -4,7 +4,6 @@ Require Import ZArith. Require Import Rbase. Require int.Int. (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false ... ...
 ... ... @@ -6,10 +6,11 @@ Require int.Int. Require int.Abs. Require int.EuclideanDivision. Require real.Real. (* Require real.RealInfix. *) Require real.FromInt. (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false ... ... @@ -250,6 +251,7 @@ Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\ (j < 32%Z)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j i) = (to_nat_sub b (j - 1%Z)%Z i))). Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\ (j < 32%Z)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j i) = ((pow2 (j - i)%Z) + (to_nat_sub b (j - 1%Z)%Z i))%Z)). ... ... @@ -262,9 +264,9 @@ Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < 32%Z)%Z /\ (i < k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j 0%Z) = (to_nat_sub b i 0%Z))). Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < 32%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j i) = 0%Z)). Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), (((j < 32%Z)%Z /\ (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j i) = 0%Z)). Axiom to_nat_of_one : forall (b:bv) (i:Z) (j:Z), (((j < 32%Z)%Z /\ (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ ... ... @@ -278,6 +280,34 @@ Axiom to_nat_sub_footprint : forall (b1:bv) (b2:bv) (j:Z) (i:Z), Parameter from_int: Z -> bv. Axiom Div_inf1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((int.EuclideanDivision.div x y) = 0%Z). Axiom Div_inf_neg : forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) -> ((int.EuclideanDivision.div (-x)%Z y) = (-1%Z)%Z). Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z). Axiom Mod_01 : forall (y:Z), (~ (y = 0%Z)) -> ((int.EuclideanDivision.mod1 0%Z y) = 0%Z). Axiom Mod_1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 1%Z y) = 1%Z). Axiom Mod_neg1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 (-1%Z)%Z y) = 1%Z). Axiom Mod_pow2 : forall (x:Z) (i:Z), ((int.EuclideanDivision.mod1 (x + (pow2 i))%Z 2%Z) = (int.EuclideanDivision.mod1 x 2%Z)). Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\ (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i)) 2%Z) = 0%Z)) -> ((nth (from_int n) i) = false). ... ... @@ -439,9 +469,9 @@ Axiom to_nat_of_zero21 : forall (b:bv1) (i:Z) (j:Z), (((j < 64%Z)%Z /\ (i < k)%Z) -> ((nth1 b k) = false)) -> ((to_nat_sub1 b j 0%Z) = (to_nat_sub1 b i 0%Z))). Axiom to_nat_of_zero1 : forall (b:bv1) (i:Z) (j:Z), ((j < 64%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth1 b k) = false)) -> ((to_nat_sub1 b j i) = 0%Z)). Axiom to_nat_of_zero1 : forall (b:bv1) (i:Z) (j:Z), (((j < 64%Z)%Z /\ (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth1 b k) = false)) -> ((to_nat_sub1 b j i) = 0%Z)). Axiom to_nat_of_one1 : forall (b:bv1) (i:Z) (j:Z), (((j < 64%Z)%Z /\ (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ ... ...
 ... ... @@ -293,6 +293,14 @@ Axiom Div_inf1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> Axiom Div_inf_neg : forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) -> ((int.EuclideanDivision.div (-x)%Z y) = (-1%Z)%Z). Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z). Axiom Mod_01 : forall (y:Z), (~ (y = 0%Z)) -> ((int.EuclideanDivision.mod1 0%Z y) = 0%Z). ... ... @@ -302,13 +310,9 @@ Axiom Mod_1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 1%Z Axiom Mod_neg1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 (-1%Z)%Z y) = 1%Z). Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Mod_pow2 : forall (x:Z) (i:Z), ((int.EuclideanDivision.mod1 (x + (pow2 i))%Z 2%Z) = (int.EuclideanDivision.mod1 x 2%Z)). Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\ (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n ... ... @@ -667,13 +671,9 @@ Axiom sign_const : ((nth1 (concat (from_int 1127219200%Z) Axiom exp_const : ((to_nat_sub1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) 62%Z 52%Z) = 1075%Z). Axiom to_nat_mantissa_1 : ((to_nat_sub1 (concat (from_int 1127219200%Z) Axiom to_nat_mantissa : ((to_nat_sub1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) 30%Z 0%Z) = 0%Z). Axiom mantissa_const_nth2 : forall (i:Z), ((32%Z <= i)%Z /\ (i <= 51%Z)%Z) -> ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) i) = false). Axiom mantissa_const_to_nat51 : ((to_nat_sub1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) 51%Z 0%Z) = (to_nat_sub1 (concat (from_int 1127219200%Z) ... ... @@ -694,9 +694,9 @@ Axiom const_value0 : ((double_of_bv64 (concat (from_int 1127219200%Z) Axiom const_value : ((double_of_bv64 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))) = ((pow21 52%Z) + (pow21 31%Z))%R). Definition jpxor(i:Z): bv := (bw_xor (from_int 2147483648%Z) (from_int2c i)). Definition jpxor(x:Z): bv := (bw_xor (from_int 2147483648%Z) (from_int2c x)). Definition var(i:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor i)). Definition var(x:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor x)). Definition var_as_double(x:Z): R := (double_of_bv64 (var x)). ... ... @@ -725,6 +725,12 @@ Axiom from_int2c_to_nat_sub_pos : forall (i:Z), ((0%Z <= i)%Z /\ (i <= 31%Z)%Z) -> forall (x:Z), ((0%Z <= x)%Z /\ (x < (pow2 i))%Z) -> ((to_nat_sub (from_int2c x) (i - 1%Z)%Z 0%Z) = x). Axiom lemma1_pos : forall (x:Z), ((is_int32 x) /\ (0%Z <= x)%Z) -> ((to_nat_sub (jpxor x) 31%Z 0%Z) = ((pow2 31%Z) + x)%Z). Axiom jpxorx_neg : forall (x:Z), (x < 0%Z)%Z -> ((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = false). (* YOU MAY EDIT THE CONTEXT BELOW *) Open Scope Z_scope. (* DO NOT EDIT BELOW *) ... ...
 ... ... @@ -293,6 +293,14 @@ Axiom Div_inf1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> Axiom Div_inf_neg : forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) -> ((int.EuclideanDivision.div (-x)%Z y) = (-1%Z)%Z). Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z). Axiom Mod_01 : forall (y:Z), (~ (y = 0%Z)) -> ((int.EuclideanDivision.mod1 0%Z y) = 0%Z). ... ... @@ -302,13 +310,9 @@ Axiom Mod_1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 1%Z Axiom Mod_neg1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 (-1%Z)%Z y) = 1%Z). Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Mod_pow2 : forall (x:Z) (i:Z), ((int.EuclideanDivision.mod1 (x + (pow2 i))%Z 2%Z) = (int.EuclideanDivision.mod1 x 2%Z)). Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\ (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n ... ... @@ -667,13 +671,9 @@ Axiom sign_const : ((nth1 (concat (from_int 1127219200%Z) Axiom exp_const : ((to_nat_sub1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) 62%Z 52%Z) = 1075%Z). Axiom to_nat_mantissa_1 : ((to_nat_sub1 (concat (from_int 1127219200%Z) Axiom to_nat_mantissa : ((to_nat_sub1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) 30%Z 0%Z) = 0%Z). Axiom mantissa_const_nth2 : forall (i:Z), ((32%Z <= i)%Z /\ (i <= 51%Z)%Z) -> ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) i) = false). Axiom mantissa_const_to_nat51 : ((to_nat_sub1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) 51%Z 0%Z) = (to_nat_sub1 (concat (from_int 1127219200%Z) ... ... @@ -694,9 +694,9 @@ Axiom const_value0 : ((double_of_bv64 (concat (from_int 1127219200%Z) Axiom const_value : ((double_of_bv64 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))) = ((pow21 52%Z) + (pow21 31%Z))%R). Definition jpxor(i:Z): bv := (bw_xor (from_int 2147483648%Z) (from_int2c i)). Definition jpxor(x:Z): bv := (bw_xor (from_int 2147483648%Z) (from_int2c x)). Definition var(i:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor i)). Definition var(x:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor x)). Definition var_as_double(x:Z): R := (double_of_bv64 (var x)). ... ...
 ... ... @@ -293,6 +293,14 @@ Axiom Div_inf1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> Axiom Div_inf_neg : forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) -> ((int.EuclideanDivision.div (-x)%Z y) = (-1%Z)%Z). Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z). Axiom Mod_01 : forall (y:Z), (~ (y = 0%Z)) -> ((int.EuclideanDivision.mod1 0%Z y) = 0%Z). ... ... @@ -302,13 +310,9 @@ Axiom Mod_1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 1%Z Axiom Mod_neg1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 (-1%Z)%Z y) = 1%Z). Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z). Axiom Mod_pow2 : forall (x:Z) (i:Z), ((int.EuclideanDivision.mod1 (x + (pow2 i))%Z 2%Z) = (int.EuclideanDivision.mod1 x 2%Z)). Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\ (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n ... ... @@ -667,13 +671,9 @@ Axiom sign_const : ((nth1 (concat (from_int 1127219200%Z) Axiom exp_const : ((to_nat_sub1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) 62%Z 52%Z) = 1075%Z). Axiom to_nat_mantissa_1 : ((to_nat_sub1 (concat (from_int 1127219200%Z) Axiom to_nat_mantissa : ((to_nat_sub1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) 30%Z 0%Z) = 0%Z). Axiom mantissa_const_nth2 : forall (i:Z), ((32%Z <= i)%Z /\ (i <= 51%Z)%Z) -> ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) i) = false). Axiom mantissa_const_to_nat51 : ((to_nat_sub1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) 51%Z 0%Z) = (to_nat_sub1 (concat (from_int 1127219200%Z) ... ... @@ -694,9 +694,9 @@ Axiom const_value0 : ((double_of_bv64 (concat (from_int 1127219200%Z) Axiom const_value : ((double_of_bv64 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))) = ((pow21 52%Z) + (pow21 31%Z))%R). Definition jpxor(i:Z): bv := (bw_xor (from_int 2147483648%Z) (from_int2c i)). Definition jpxor(x:Z): bv := (bw_xor (from_int 2147483648%Z) (from_int2c x)). Definition var(i:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor i)). Definition var(x:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor x)). Definition var_as_double(x:Z): R := (double_of_bv64 (var x)). ... ... @@ -725,13 +725,16 @@ Axiom from_int2c_to_nat_sub_pos : forall (i:Z), ((0%Z <= i)%Z /\ (i <= 31%Z)%Z) -> forall (x:Z), ((0%Z <= x)%Z /\ (x < (pow2 i))%Z) -> ((to_nat_sub (from_int2c x) (i - 1%Z)%Z 0%Z) = x). Axiom lemma1_pos : forall (x:Z), ((is_int32 x) /\ (0%Z <= x)%Z) -> ((to_nat_sub (jpxor x) 31%Z 0%Z) = ((pow2 31%Z) + x)%Z). Axiom jpxorx_neg : forall (x:Z), (x < 0%Z)%Z -> ((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = false). Axiom from_int2c_to_nat_sub_neg : forall (i:Z), ((0%Z <= i)%Z /\ (i <= 31%Z)%Z) -> forall (x:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < 0%Z)%Z) -> ((to_nat_sub (from_int2c x) (i - 1%Z)%Z 0%Z) = ((pow2 i) + x)%Z). Axiom lemma1_pos : forall (x:Z), ((is_int32 x) /\ (0%Z <= x)%Z) -> ((to_nat_sub (jpxor x) 31%Z 0%Z) = ((pow2 31%Z) + x)%Z). (* YOU MAY EDIT THE CONTEXT BELOW *) Open Scope