Skip to content

GitLab

Commit 03516d00 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

restructure proofs of bitvector1

parent 9e62ead8
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 3845 additions and 942 deletions
tests/bitvector1.why
View file @ 03516d00
......@@ -718,7 +718,24 @@ theory TestDoubleOfInt
function var_as_double(x:int) : real = double_of_bv64 (var x)
(*********************************************************************)
(* next lemma: for all integer x, var_as_double(x) = 2^52 + 2^31 + x *)
(* lemma 1: for all integer x, to_nat(jpxor(x)) = 2^31 + x *)
(*********************************************************************)
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
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_neg : forall x:int. is_int32 x /\ x < 0 -> 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 *)
(*********************************************************************)
lemma nth_var1: forall x:BV32.bv, j:int. 0 <= j <31 ->
......@@ -730,17 +747,61 @@ theory TestDoubleOfInt
lemma nth_var2:
forall x:int. (BV64.nth (var x) 31) = notb (BV32.nth (BV32.from_int2c x) 31)
lemma nth_var30:
lemma nth_var32to63:
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 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_var8: forall x:int. BV64.nth (var x) 62 = True
lemma lemma3 : forall x:int. exp(var(x)) = 1075
(*********************************************************************)
(* lemma 4: for all integer x, sign(var(x)) = false *)
(*********************************************************************)
lemma nth_var9: forall x:int. BV64.nth (var x) 63 = False
lemma lemma4 : forall x:int. sign(var(x)) = False
(*********************************************************************)
(* lemma 5: for all integer x, var_as_double(x) = 2^52 + 2^31 + x *)
(*********************************************************************)
lemma lemma5: forall x:int. is_int32 x -> var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 31 +. (from_int x)
(*********************************************************************)
(* main result *)
(*********************************************************************)
function double_of_int32 (x:int) : real = var_as_double(x) -. const_as_double
lemma MainResult: forall x:int. is_int32 x -> double_of_int32 x = from_int x
(****************************************************)
(* dans ce qui suit, reprendre les bouts necessaires et les mettre au-dessus *)
lemma sign_var: forall x:int. sign(var(x)) = False
lemma exp_var: forall x:int. exp(var(x)) = 1075
......@@ -751,30 +812,40 @@ theory TestDoubleOfInt
lemma nat_to_sub_x: forall x:int.
BV64.to_nat_sub (var x) 30 0 = BV32.to_nat_sub (BV32.from_int2c x) 30 0
lemma to_nat_sub_var:
forall x:int. BV64.to_nat_sub (var x) 30 0 = BV32.to_nat_sub (BV32.from_int2c x) 30 0
lemma x_positive:forall x:int. (BV32.nth (BV32.from_int2c x) 31) = False ->
BV32.to_nat_sub (BV32.from_int2c x) 31 0 = BV32.to_nat_sub (BV32.from_int2c x) 30 0
lemma x_negative:forall x:int. (BV32.nth (BV32.from_int2c x) 31) = True ->
BV32.to_nat_sub (BV32.from_int2c x) 31 0 = Pow2int.pow2 31 + BV32.to_nat_sub (BV32.from_int2c x) 30 0
lemma sign_of_x:
forall x:int. (BV32.nth (BV32.from_int2c x) 31) = False->x>0
lemma from_int2c_to_nat_sub:
forall x:int.x>0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = x
forall x:int. x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = x
lemma from_int2c_to_nat_sub_neg:
forall x:int. x < 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = Pow2int.pow2 31 + x
lemma x_positive1: forall x:int. (BV32.nth (BV32.from_int2c x) 31) = False ->
BV32.to_nat_sub (BV32.from_int2c x) 30 0 = x
lemma x_positive2: forall x:int. (BV64.nth (var x) 31) = True ->
BV64.to_nat_sub (var x) 30 0 = x
lemma mantissa_var_x_positive:
forall x:int. (BV64.nth (var x) 31) = True ->
mantissa(var(x)) = Pow2int.pow2 31 + x
(*a verifier*)
lemma x_negative: forall x:int. (BV64.nth (var x) 31) = False ->
BV64.to_nat_sub (var x) 30 0 = -x
(*a verifier*)
lemma x_negative1: forall x:int. (BV32.nth (BV32.from_int2c x) 31) = True ->
BV32.to_nat_sub (BV32.from_int2c x) 30 0 = Pow2int.pow2 31 + x
lemma x_negative2: forall x:int. (BV64.nth (var x) 31) = False ->
BV64.to_nat_sub (var x) 30 0 = Pow2int.pow2 31 + x
lemma mantissa_var_x_negative:
forall x:int. (BV64.nth (var x) 31) = False ->
mantissa(var(x)) = Pow2int.pow2 31 + x
......@@ -803,14 +874,6 @@ theory TestDoubleOfInt
lemma var_value: forall x:int. var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 31 +. (from_int x)
(*********************************************************************)
(* main result *)
(*********************************************************************)
function double_of_int32 (i:int) : real = var_as_double(i) -. const_as_double
lemma MainResult: forall i:int. double_of_int32 i = from_int i
end
theory TestBv32
......
tests/bitvector1/bitvector1_TestDoubleOfInt_exp_var_2.v
View file @ 03516d00
......@@ -2,6 +2,11 @@
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require real.Real.
Require real.FromInt.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
......@@ -151,6 +156,8 @@ Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
Parameter bv : Type.
Axiom size_positive : (0%Z < 32%Z)%Z.
Parameter nth: bv -> Z -> bool.
......@@ -214,13 +221,13 @@ Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) ->
Parameter lsr: bv -> Z -> bv.
Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 32%Z)%Z -> ((nth (lsr b
s) n) = (nth b (n + s)%Z)))).
Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
(n < 32%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 32%Z)%Z) /\
((n + s)%Z < 32%Z)%Z)) -> ((nth (lsr b s) n) = (nth b (n + s)%Z)).
Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((32%Z <= (n + s)%Z)%Z -> ((nth (lsr b
s) n) = false))).
Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
(n < 32%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 32%Z)%Z) /\
(32%Z <= (n + s)%Z)%Z)) -> ((nth (lsr b s) n) = false).
Parameter asr: bv -> Z -> bv.
......@@ -247,84 +254,114 @@ Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
Parameter to_nat_sub: bv -> Z -> Z -> Z.
Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), ((0%Z <= i)%Z /\
(i <= j)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j i) = (to_nat_sub b
(j - 1%Z)%Z i))).
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) -> (((nth b j) = true) -> ((to_nat_sub b j
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)).
Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z ->
((to_nat_sub b j i) = 0%Z).
Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j: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 0%Z) = (to_nat_sub b i 0%Z))).
Axiom to_nat_of_zero2 : 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
0%Z) = (to_nat_sub b i 0%Z))).
Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j: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_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), ((i <= j)%Z /\
(0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b
k) = true)) -> ((to_nat_sub b j
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 /\
(i <= k)%Z) -> ((nth b k) = true)) -> ((to_nat_sub b j
i) = ((pow2 ((j - i)%Z + 1%Z)%Z) - 1%Z)%Z)).
Axiom to_nat_sub_footprint : forall (b1:bv) (b2:bv) (j:Z) (i:Z),
(forall (k:Z), ((i <= k)%Z /\ (k <= j)%Z) -> ((nth b1 k) = (nth b2 k))) ->
((to_nat_sub b1 j i) = (to_nat_sub b2 j i)).
((j < 32%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((i <= k)%Z /\
(k <= j)%Z) -> ((nth b1 k) = (nth b2 k))) -> ((to_nat_sub b1 j
i) = (to_nat_sub b2 j i))).
Axiom lsr_to_nat_sub : forall (b:bv) (s:Z), (0%Z <= s)%Z ->
((to_nat_sub (lsr b s) (32%Z - 1%Z)%Z 0%Z) = (to_nat_sub b
((32%Z - 1%Z)%Z - s)%Z 0%Z)).
Axiom lsr_to_nat_sub : forall (b:bv) (s:Z), ((0%Z <= s)%Z /\
(s < 32%Z)%Z) -> ((to_nat_sub (lsr b s) (32%Z - 1%Z)%Z
0%Z) = (to_nat_sub b ((32%Z - 1%Z)%Z - s)%Z 0%Z)).
Parameter from_int: Z -> bv.
Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
(x <= y)%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).
Parameter div: Z -> Z -> Z.
Axiom nth_from_int_high_odd : 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) = true).
Axiom nth_from_int_low_even : forall (n:Z), ((int.EuclideanDivision.mod1 n
2%Z) = 0%Z) -> ((nth (from_int n) 0%Z) = false).
Parameter mod1: Z -> Z -> Z.
Axiom nth_from_int_low_odd : forall (n:Z), (~ ((int.EuclideanDivision.mod1 n
2%Z) = 0%Z)) -> ((nth (from_int n) 0%Z) = true).
Axiom pow2i : forall (i:Z), (0%Z <= i)%Z -> ~ ((pow2 i) = 0%Z).
Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x
y))%Z + (mod1 x y))%Z).
Axiom nth_from_int_0 : forall (i:Z), ((i < 32%Z)%Z /\ (0%Z <= i)%Z) ->
((nth (from_int 0%Z) i) = false).
Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z).
Parameter from_int2c: Z -> bv.
Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (mod1 x
y))%Z /\ ((mod1 x y) < (Zabs y))%Z).
Axiom Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z).
Axiom size_from_int2c : (0%Z < (32%Z - 1%Z)%Z)%Z.
Axiom Div_1 : forall (x:Z), ((div x 1%Z) = x).
Axiom nth_sign_positive : forall (n:Z), (0%Z <= n)%Z -> ((nth (from_int2c n)
(32%Z - 1%Z)%Z) = false).
Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\
(0%Z <= i)%Z) /\ ((mod1 (div n (pow2 i)) 2%Z) = 0%Z)) -> ((nth (from_int n)
i) = false).
Axiom nth_from_int2c_high_even_positive : forall (n:Z) (i:Z),
((0%Z <= n)%Z /\ (((i < (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
2%Z) = 0%Z))) -> ((nth (from_int2c n) i) = false).
Axiom nth_from_int_high_odd : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\
(0%Z <= i)%Z) /\ ~ ((mod1 (div n (pow2 i)) 2%Z) = 0%Z)) ->
((nth (from_int n) i) = true).
Axiom nth_from_int2c_high_odd_positive : forall (n:Z) (i:Z), ((0%Z <= n)%Z /\
(((i < (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
2%Z) = 0%Z))) -> ((nth (from_int2c n) i) = true).
Axiom nth_from_int_low_even : forall (n:Z), ((mod1 n 2%Z) = 0%Z) ->
((nth (from_int n) 0%Z) = false).
Axiom nth_from_int2c_low_even_positive : forall (n:Z), ((0%Z <= n)%Z /\
((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth (from_int2c n)
0%Z) = false).
Axiom nth_from_int_low_odd : forall (n:Z), (~ ((mod1 n 2%Z) = 0%Z)) ->
((nth (from_int n) 0%Z) = true).
Axiom nth_from_int2c_low_odd_positive : forall (n:Z), ((0%Z <= n)%Z /\
~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth (from_int2c n)
0%Z) = true).
Axiom pow2i : forall (i:Z), (0%Z <= i)%Z -> ~ ((pow2 i) = 0%Z).
Axiom nth_sign_negative : forall (n:Z), (n < 0%Z)%Z -> ((nth (from_int2c n)
(32%Z - 1%Z)%Z) = true).
Axiom nth_from_int_0 : forall (i:Z), ((i < 32%Z)%Z /\ (0%Z <= i)%Z) ->
((nth (from_int 0%Z) i) = false).
Axiom nth_from_int2c_high_even_negative : forall (n:Z) (i:Z),
((n < 0%Z)%Z /\ (((i < (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
2%Z) = 0%Z))) -> ((nth (from_int2c n) i) = true).
Axiom nth_from_int2c_high_odd_negative : forall (n:Z) (i:Z), ((n < 0%Z)%Z /\
(((i < (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
2%Z) = 0%Z))) -> ((nth (from_int2c n) i) = false).
Axiom nth_from_int2c_low_even_negative : forall (n:Z), ((n < 0%Z)%Z /\
((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth (from_int2c n)
0%Z) = true).
Axiom nth_from_int2c_low_odd_negative : forall (n:Z), ((n < 0%Z)%Z /\
~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth (from_int2c n)
0%Z) = false).
Parameter bv1 : Type.
Axiom size_positive1 : (0%Z < 64%Z)%Z.
Parameter nth1: bv1 -> Z -> bool.
......@@ -391,13 +428,13 @@ Axiom Nth_bw_not1 : forall (v:bv1) (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
Parameter lsr1: bv1 -> Z -> bv1.
Axiom lsr_nth_low1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < 64%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 64%Z)%Z -> ((nth1 (lsr1 b
s) n) = (nth1 b (n + s)%Z)))).
Axiom lsr_nth_low1 : forall (b:bv1) (n:Z) (s:Z), (((0%Z <= n)%Z /\
(n < 64%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 64%Z)%Z) /\
((n + s)%Z < 64%Z)%Z)) -> ((nth1 (lsr1 b s) n) = (nth1 b (n + s)%Z)).
Axiom lsr_nth_high1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < 64%Z)%Z) -> ((0%Z <= s)%Z -> ((64%Z <= (n + s)%Z)%Z -> ((nth1 (lsr1 b
s) n) = false))).
Axiom lsr_nth_high1 : forall (b:bv1) (n:Z) (s:Z), (((0%Z <= n)%Z /\
(n < 64%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 64%Z)%Z) /\
(64%Z <= (n + s)%Z)%Z)) -> ((nth1 (lsr1 b s) n) = false).
Parameter asr1: bv1 -> Z -> bv1.
......@@ -424,60 +461,110 @@ Axiom lsl_nth_low1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
Parameter to_nat_sub1: bv1 -> Z -> Z -> Z.
Axiom to_nat_sub_zero1 : forall (b:bv1) (j:Z) (i:Z), ((0%Z <= i)%Z /\
(i <= j)%Z) -> (((nth1 b j) = false) -> ((to_nat_sub1 b j
Axiom to_nat_sub_zero1 : forall (b:bv1) (j:Z) (i:Z), (((0%Z <= i)%Z /\
(i <= j)%Z) /\ (j < 64%Z)%Z) -> (((nth1 b j) = false) -> ((to_nat_sub1 b j
i) = (to_nat_sub1 b (j - 1%Z)%Z i))).
Axiom to_nat_sub_one1 : forall (b:bv1) (j:Z) (i:Z), ((0%Z <= i)%Z /\
(i <= j)%Z) -> (((nth1 b j) = true) -> ((to_nat_sub1 b j
Axiom to_nat_sub_one1 : forall (b:bv1) (j:Z) (i:Z), (((0%Z <= i)%Z /\
(i <= j)%Z) /\ (j < 64%Z)%Z) -> (((nth1 b j) = true) -> ((to_nat_sub1 b j
i) = ((pow2 (j - i)%Z) + (to_nat_sub1 b (j - 1%Z)%Z i))%Z)).
Axiom to_nat_sub_high1 : forall (b:bv1) (j:Z) (i:Z), (j < i)%Z ->
((to_nat_sub1 b j i) = 0%Z).
Axiom to_nat_of_zero21 : forall (b:bv1) (i:Z) (j: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 0%Z) = (to_nat_sub1 b i 0%Z))).
Axiom to_nat_of_zero21 : 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
0%Z) = (to_nat_sub1 b i 0%Z))).
Axiom to_nat_of_zero1 : forall (b:bv1) (i:Z) (j: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_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), ((i <= j)%Z /\
(0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth1 b
k) = true)) -> ((to_nat_sub1 b j
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 /\
(i <= k)%Z) -> ((nth1 b k) = true)) -> ((to_nat_sub1 b j
i) = ((pow2 ((j - i)%Z + 1%Z)%Z) - 1%Z)%Z)).
Axiom to_nat_sub_footprint1 : forall (b1:bv1) (b2:bv1) (j:Z) (i:Z),
(forall (k:Z), ((i <= k)%Z /\ (k <= j)%Z) -> ((nth1 b1 k) = (nth1 b2
k))) -> ((to_nat_sub1 b1 j i) = (to_nat_sub1 b2 j i)).
((j < 64%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((i <= k)%Z /\
(k <= j)%Z) -> ((nth1 b1 k) = (nth1 b2 k))) -> ((to_nat_sub1 b1 j
i) = (to_nat_sub1 b2 j i))).
Axiom lsr_to_nat_sub1 : forall (b:bv1) (s:Z), (0%Z <= s)%Z ->
((to_nat_sub1 (lsr1 b s) (64%Z - 1%Z)%Z 0%Z) = (to_nat_sub1 b
((64%Z - 1%Z)%Z - s)%Z 0%Z)).
Axiom lsr_to_nat_sub1 : forall (b:bv1) (s:Z), ((0%Z <= s)%Z /\
(s < 64%Z)%Z) -> ((to_nat_sub1 (lsr1 b s) (64%Z - 1%Z)%Z
0%Z) = (to_nat_sub1 b ((64%Z - 1%Z)%Z - s)%Z 0%Z)).
Parameter from_int1: Z -> bv1.
Axiom nth_from_int_high_even1 : forall (n:Z) (i:Z), (((i < 64%Z)%Z /\
(0%Z <= i)%Z) /\ ((mod1 (div n (pow2 i)) 2%Z) = 0%Z)) ->
((nth1 (from_int1 n) i) = false).
(0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n
(pow2 i)) 2%Z) = 0%Z)) -> ((nth1 (from_int1 n) i) = false).
Axiom nth_from_int_high_odd1 : forall (n:Z) (i:Z), (((i < 64%Z)%Z /\
(0%Z <= i)%Z) /\ ~ ((mod1 (div n (pow2 i)) 2%Z) = 0%Z)) ->
((nth1 (from_int1 n) i) = true).
(0%Z <= i)%Z) /\
~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
2%Z) = 0%Z)) -> ((nth1 (from_int1 n) i) = true).
Axiom nth_from_int_low_even1 : forall (n:Z), ((mod1 n 2%Z) = 0%Z) ->
((nth1 (from_int1 n) 0%Z) = false).
Axiom nth_from_int_low_even1 : forall (n:Z), ((int.EuclideanDivision.mod1 n
2%Z) = 0%Z) -> ((nth1 (from_int1 n) 0%Z) = false).
Axiom nth_from_int_low_odd1 : forall (n:Z), (~ ((mod1 n 2%Z) = 0%Z)) ->
((nth1 (from_int1 n) 0%Z) = true).
Axiom nth_from_int_low_odd1 : forall (n:Z), (~ ((int.EuclideanDivision.mod1 n
2%Z) = 0%Z)) -> ((nth1 (from_int1 n) 0%Z) = true).
Axiom pow2i1 : forall (i:Z), (0%Z <= i)%Z -> ~ ((pow2 i) = 0%Z).
Axiom nth_from_int_01 : forall (i:Z), ((i < 64%Z)%Z /\ (0%Z <= i)%Z) ->
((nth1 (from_int1 0%Z) i) = false).
Parameter from_int2c1: Z -> bv1.
Axiom size_from_int2c1 : (0%Z < (64%Z - 1%Z)%Z)%Z.
Axiom nth_sign_positive1 : forall (n:Z), (0%Z <= n)%Z ->
((nth1 (from_int2c1 n) (64%Z - 1%Z)%Z) = false).
Axiom nth_from_int2c_high_even_positive1 : forall (n:Z) (i:Z),
((0%Z <= n)%Z /\ (((i < (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
2%Z) = 0%Z))) -> ((nth1 (from_int2c1 n) i) = false).
Axiom nth_from_int2c_high_odd_positive1 : forall (n:Z) (i:Z),
((0%Z <= n)%Z /\ (((i < (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
2%Z) = 0%Z))) -> ((nth1 (from_int2c1 n) i) = true).
Axiom nth_from_int2c_low_even_positive1 : forall (n:Z), ((0%Z <= n)%Z /\
((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n)
0%Z) = false).
Axiom nth_from_int2c_low_odd_positive1 : forall (n:Z), ((0%Z <= n)%Z /\
~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n)
0%Z) = true).
Axiom nth_sign_negative1 : forall (n:Z), (n < 0%Z)%Z ->
((nth1 (from_int2c1 n) (64%Z - 1%Z)%Z) = true).
Axiom nth_from_int2c_high_even_negative1 : forall (n:Z) (i:Z),
((n < 0%Z)%Z /\ (((i < (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
2%Z) = 0%Z))) -> ((nth1 (from_int2c1 n) i) = true).
Axiom nth_from_int2c_high_odd_negative1 : forall (n:Z) (i:Z),
((n < 0%Z)%Z /\ (((i < (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
2%Z) = 0%Z))) -> ((nth1 (from_int2c1 n) i) = false).
Axiom nth_from_int2c_low_even_negative1 : forall (n:Z), ((n < 0%Z)%Z /\
((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n)
0%Z) = true).
Axiom nth_from_int2c_low_odd_negative1 : forall (n:Z), ((n < 0%Z)%Z /\
~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n)
0%Z) = false).
Parameter concat: bv -> bv -> bv1.
......@@ -498,10 +585,30 @@ Axiom Power_s1 : forall (n:Z), (0%Z <= n)%Z ->
Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z ->
((pow21 (n - 1%Z)%Z) = ((05 / 10)%R * (pow21 n))%R).
Axiom Power_s_all : forall (n:Z),
((pow21 (n + 1%Z)%Z) = (2%R * (pow21 n))%R).
Axiom Power_p_all : forall (n:Z),
((pow21 (n - 1%Z)%Z) = ((05 / 10)%R * (pow21 n))%R).
Axiom Power_1_2 : ((05 / 10)%R = (Rdiv 1%R 2%R)%R).
Axiom Power_11 : ((pow21 1%Z) = 2%R).
Axiom Power_neg1 : ((pow21 (-1%Z)%Z) = (05 / 10)%R).
Axiom Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z -> ~ ((pow21 n) = 0%R).
Axiom Power_neg_aux : forall (n:Z), (0%Z <= n)%Z ->
((pow21 (-n)%Z) = (Rdiv 1%R (pow21 n))%R).