Commit a10662a0 authored by MARCHE Claude's avatar MARCHE Claude

Fixed proofs of bitvectors examples

parent 5c322c15
......@@ -19,27 +19,19 @@
version="2.4.1"/>
<prover
id="4"
name="CVC4"
version="1.0"/>
<prover
id="5"
name="Coq"
version="8.3pl4"/>
<prover
id="6"
id="5"
name="Z3"
version="2.19"/>
<prover
id="7"
id="6"
name="Z3"
version="3.2"/>
<prover
id="8"
name="Z3"
version="4.2"/>
<file
name="../double.why"
verified="false"
verified="true"
expanded="true">
<theory
name="BV_double"
......@@ -52,63 +44,31 @@
name="TestDouble"
locfile="../double.why"
loclnum="65" loccnumb="7" loccnume="17"
verified="false"
verified="true"
expanded="true">
<goal
name="nth_one1"
locfile="../double.why"
loclnum="73" loccnumb="8" loccnume="16"
sum="68b26f6bd21633cb2cb9250019b673f2"
proved="false"
proved="true"
expanded="true"
shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c51Aainfix &lt;=c0V0F">
<proof
prover="0"
timelimit="60"
memlimit="4000"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="60.46"/>
<result status="valid" time="1.57"/>
</proof>
<proof
prover="1"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="59.78"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.07"/>
</proof>
<proof
prover="6"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="60.56"/>
</proof>
<proof
prover="7"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="61.10"/>
</proof>
<proof
prover="8"
timelimit="60"
memlimit="4000"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="60.25"/>
<result status="valid" time="0.87"/>
</proof>
</goal>
<goal
......@@ -116,56 +76,24 @@
locfile="../double.why"
loclnum="74" loccnumb="8" loccnume="16"
sum="f08cb866a3ab9529aea096452c0c2aba"
proved="false"
proved="true"
expanded="true"
shape="ainfix =anthaoneV0aTrueIainfix &lt;=V0c61Aainfix &lt;=c52V0F">
<proof
prover="0"
timelimit="60"
memlimit="4000"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="60.27"/>
<result status="valid" time="0.56"/>
</proof>
<proof
prover="1"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="59.61"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.07"/>
</proof>
<proof
prover="6"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="60.41"/>
</proof>
<proof
prover="7"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="61.00"/>
</proof>
<proof
prover="8"
timelimit="60"
memlimit="4000"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="60.12"/>
<result status="valid" time="0.34"/>
</proof>
</goal>
<goal
......@@ -218,7 +146,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -226,7 +154,7 @@
<result status="valid" time="0.11"/>
</proof>
<proof
prover="7"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -251,7 +179,7 @@
<result status="valid" time="2.09"/>
</proof>
<proof
prover="5"
prover="4"
timelimit="30"
memlimit="1000"
edited="double_TestDouble_exp_one_1.v"
......@@ -277,7 +205,7 @@
<result status="valid" time="0.09"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -285,7 +213,7 @@
<result status="valid" time="0.69"/>
</proof>
<proof
prover="7"
prover="6"
timelimit="11"
memlimit="1000"
obsolete="false"
......
......@@ -21,6 +21,14 @@ theory DoubleOfInt
function j : BV32.bv = BV32.from_int 0x43300000
lemma nth_j1: forall i:int. 0 <= i <= 19 -> BV32.nth j i = False
lemma nth_j2: forall i:int. 20 <= i <= 21 -> BV32.nth j i = True
lemma nth_j3: forall i:int. 22 <= i <= 23 -> BV32.nth j i = False
lemma nth_j4: forall i:int. 24 <= i <= 25 -> BV32.nth j i = True
lemma nth_j5: forall i:int. 26 <= i <= 29 -> BV32.nth j i = False
lemma nth_j6: BV32.nth j 30 = True
lemma nth_j7: BV32.nth j 31 = False
function j' : BV32.bv = BV32.from_int 0x80000000
lemma jp0_30: forall i:int. 0<=i<30 -> BV32.nth j' i = False
......@@ -187,7 +195,8 @@ theory DoubleOfInt
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 nth_var3: forall x i:int.
is_int32 x /\ 32 <= i <= 51 -> BV64.nth (var x) i = False
lemma lemma2 : forall x:int. is_int32 x -> mantissa(var(x)) = Pow2int.pow2 31 + x
......@@ -195,29 +204,44 @@ theory DoubleOfInt
(* 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 nth_var4: forall x i:int.
is_int32 x /\ 52 <= i <= 53 -> BV64.nth (var x) i = True
lemma nth_var5: forall x i:int.
is_int32 x /\ 54 <= i <= 55 -> BV64.nth (var x) i = False
lemma nth_var6: forall x i:int.
is_int32 x /\ 56 <= i <= 57 -> BV64.nth (var x) i = True
lemma lemma3 : forall x:int. exp(var(x)) = 1075
lemma nth_var7: forall x i:int.
is_int32 x /\ 58 <= i <= 61 -> BV64.nth (var x) i = False
lemma nth_var8: forall x:int.
is_int32 x -> BV64.nth (var x) 62 = True
lemma lemma3 :
forall x:int. is_int32 x -> 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 nth_var9:
forall x:int. is_int32 x -> BV64.nth (var x) 63 = False
lemma lemma4 : forall x:int. sign(var(x)) = False
lemma lemma4 :
forall x:int. is_int32 x -> sign(var(x)) = False
(*********************************************************************)
(* 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 sign_var: forall x:int.
is_int32 x -> 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 from_int_sum : forall x:int. is_int32(x)->
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require bool.Bool.
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
| (_, _) => true
end.
Parameter pow2: Z -> Z.
Axiom Power_0 : ((pow2 0%Z) = 1%Z).
......@@ -158,6 +152,19 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%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_gen : forall (x:Z) (i:Z) (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) ->
((int.EuclideanDivision.mod1 (int.EuclideanDivision.div (x + (pow2 i))%Z
(pow2 k)) 2%Z) = (int.EuclideanDivision.mod1 (int.EuclideanDivision.div x
(pow2 k)) 2%Z)).
Parameter pow21: Z -> R.
Axiom Power_01 : ((pow21 0%Z) = 1%R).
......@@ -200,7 +207,9 @@ Axiom Pow2_int_real : forall (x:Z), (0%Z <= x)%Z ->
Axiom size_positive : (1%Z < 32%Z)%Z.
Parameter bv : Type.
Axiom bv : Type.
Parameter bv_WhyType : WhyType bv.
Existing Instance bv_WhyType.
Parameter nth: bv -> Z -> bool.
......@@ -215,7 +224,7 @@ Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvone
n) = true).
(* Why3 assumption *)
Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
Definition eq (v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((nth v1 n) = (nth v2 n)).
Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
......@@ -366,13 +375,15 @@ Axiom nth_from_int2c_low_odd : forall (n:Z),
Axiom nth_from_int2c_0 : forall (i:Z), ((i < 32%Z)%Z /\ (0%Z <= i)%Z) ->
((nth (from_int2c 0%Z) i) = false).
Axiom nth_from_int2c_plus_pow2 : forall (x:Z) (k:Z) (i:Z), ((0%Z <= k)%Z /\
(k < i)%Z) -> ((nth (from_int2c (x + (pow2 i))%Z) k) = (nth (from_int2c x)
k)).
Axiom nth_from_int2c_plus_pow2 : forall (x:Z) (k:Z) (i:Z), (((0%Z <= k)%Z /\
(k < i)%Z) /\ (k < (32%Z - 1%Z)%Z)%Z) ->
((nth (from_int2c (x + (pow2 i))%Z) k) = (nth (from_int2c x) k)).
Axiom size_positive1 : (1%Z < 64%Z)%Z.
Parameter bv1 : Type.
Axiom bv1 : Type.
Parameter bv1_WhyType : WhyType bv1.
Existing Instance bv1_WhyType.
Parameter nth1: bv1 -> Z -> bool.
......@@ -387,7 +398,7 @@ Axiom Nth_one1 : forall (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
((nth1 bvone1 n) = true).
(* Why3 assumption *)
Definition eq1(v1:bv1) (v2:bv1): Prop := forall (n:Z), ((0%Z <= n)%Z /\
Definition eq1 (v1:bv1) (v2:bv1): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < 64%Z)%Z) -> ((nth1 v1 n) = (nth1 v2 n)).
Axiom extensionality1 : forall (v1:bv1) (v2:bv1), (eq1 v1 v2) -> (v1 = v2).
......@@ -540,9 +551,9 @@ Axiom nth_from_int2c_low_odd1 : forall (n:Z),
Axiom nth_from_int2c_01 : forall (i:Z), ((i < 64%Z)%Z /\ (0%Z <= i)%Z) ->
((nth1 (from_int2c1 0%Z) i) = false).
Axiom nth_from_int2c_plus_pow21 : forall (x:Z) (k:Z) (i:Z), ((0%Z <= k)%Z /\
(k < i)%Z) -> ((nth1 (from_int2c1 (x + (pow2 i))%Z)
k) = (nth1 (from_int2c1 x) k)).
Axiom nth_from_int2c_plus_pow21 : forall (x:Z) (k:Z) (i:Z), (((0%Z <= k)%Z /\
(k < i)%Z) /\ (k < (64%Z - 1%Z)%Z)%Z) ->
((nth1 (from_int2c1 (x + (pow2 i))%Z) k) = (nth1 (from_int2c1 x) k)).
Parameter concat: bv -> bv -> bv1.
......@@ -575,6 +586,25 @@ Axiom double_of_bv64_value : forall (b:bv1), ((0%Z < (to_nat_sub1 b 62%Z
62%Z 52%Z) - 1023%Z)%Z))%R * (1%R + ((IZR (to_nat_sub1 b 51%Z
0%Z)) * (pow21 (-52%Z)%Z))%R)%R)%R).
Axiom nth_j1 : forall (i:Z), ((0%Z <= i)%Z /\ (i <= 19%Z)%Z) ->
((nth (from_int 1127219200%Z) i) = false).
Axiom nth_j2 : forall (i:Z), ((20%Z <= i)%Z /\ (i <= 21%Z)%Z) ->
((nth (from_int 1127219200%Z) i) = true).
Axiom nth_j3 : forall (i:Z), ((22%Z <= i)%Z /\ (i <= 23%Z)%Z) ->
((nth (from_int 1127219200%Z) i) = false).
Axiom nth_j4 : forall (i:Z), ((24%Z <= i)%Z /\ (i <= 25%Z)%Z) ->
((nth (from_int 1127219200%Z) i) = true).
Axiom nth_j5 : forall (i:Z), ((26%Z <= i)%Z /\ (i <= 29%Z)%Z) ->
((nth (from_int 1127219200%Z) i) = false).
Axiom nth_j6 : ((nth (from_int 1127219200%Z) 30%Z) = true).
Axiom nth_j7 : ((nth (from_int 1127219200%Z) 31%Z) = false).
Axiom jp0_30 : forall (i:Z), ((0%Z <= i)%Z /\ (i < 30%Z)%Z) ->
((nth (from_int 2147483648%Z) i) = false).
......@@ -643,16 +673,17 @@ Axiom const_value : ((double_of_bv64 (concat (from_int 1127219200%Z)
(from_int 2147483648%Z))) = ((pow21 52%Z) + (pow21 31%Z))%R).
(* Why3 assumption *)
Definition jpxor(i:Z): bv := (bw_xor (from_int 2147483648%Z) (from_int2c i)).
Definition jpxor (i:Z): bv := (bw_xor (from_int 2147483648%Z)
(from_int2c i)).
(* Why3 assumption *)
Definition var(i:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor i)).
Definition var (i:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor i)).
(* Why3 assumption *)
Definition var_as_double(x:Z): R := (double_of_bv64 (var x)).
Definition var_as_double (x:Z): R := (double_of_bv64 (var x)).
(* Why3 assumption *)
Definition is_int32(x:Z): Prop := ((-(pow2 31%Z))%Z <= x)%Z /\
Definition is_int32 (x:Z): Prop := ((-(pow2 31%Z))%Z <= x)%Z /\
(x < (pow2 31%Z))%Z.
Axiom nth_0_30 : forall (x:Z), forall (i:Z), ((is_int32 x) /\
......@@ -679,12 +710,13 @@ Axiom from_int2c_to_nat_sub_pos : forall (i:Z), ((0%Z <= i)%Z /\
Open Scope Z_scope.
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 5.
Ltac ae := why3 "alt-ergo" timelimit 60.
(* Why3 goal *)
Theorem 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).
(* intros x (h1,h2). *)
intros.
unfold jpxor.
rewrite to_nat_sub_one; auto with zarith.
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require bool.Bool.
Require real.Real.
Require real.RealInfix.
Require real.FromInt.
......@@ -223,7 +224,7 @@ Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvone
n) = true).
(* Why3 assumption *)
Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
Definition eq (v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((nth v1 n) = (nth v2 n)).
Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
......@@ -397,7 +398,7 @@ Axiom Nth_one1 : forall (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
((nth1 bvone1 n) = true).
(* Why3 assumption *)
Definition eq1(v1:bv1) (v2:bv1): Prop := forall (n:Z), ((0%Z <= n)%Z /\
Definition eq1 (v1:bv1) (v2:bv1): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < 64%Z)%Z) -> ((nth1 v1 n) = (nth1 v2 n)).
Axiom extensionality1 : forall (v1:bv1) (v2:bv1), (eq1 v1 v2) -> (v1 = v2).
......@@ -653,16 +654,17 @@ Axiom const_value : ((double_of_bv64 (concat (from_int 1127219200%Z)
(from_int 2147483648%Z))) = ((pow21 52%Z) + (pow21 31%Z))%R).
(* Why3 assumption *)
Definition jpxor(i:Z): bv := (bw_xor (from_int 2147483648%Z) (from_int2c i)).
Definition jpxor (i:Z): bv := (bw_xor (from_int 2147483648%Z)
(from_int2c i)).
(* Why3 assumption *)
Definition var(i:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor i)).
Definition var (i:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor i)).
(* Why3 assumption *)
Definition var_as_double(x:Z): R := (double_of_bv64 (var x)).
Definition var_as_double (x:Z): R := (double_of_bv64 (var x)).
(* Why3 assumption *)
Definition is_int32(x:Z): Prop := ((-(pow2 31%Z))%Z <= x)%Z /\
Definition is_int32 (x:Z): Prop := ((-(pow2 31%Z))%Z <= x)%Z /\
(x < (pow2 31%Z))%Z.
Axiom nth_0_30 : forall (x:Z), forall (i:Z), ((is_int32 x) /\
......@@ -719,26 +721,25 @@ Axiom to_nat_var_0_31 : forall (x:Z), (is_int32 x) -> ((to_nat_sub1 (var x)
Axiom nth_var32to63 : forall (x:Z) (k:Z), ((32%Z <= k)%Z /\ (k <= 63%Z)%Z) ->
((nth1 (var x) k) = (nth (from_int 1127219200%Z) (k - 32%Z)%Z)).
Axiom nth_var3 : forall (x:Z), forall (i:Z), ((32%Z <= i)%Z /\
(i <= 51%Z)%Z) -> ((nth1 (var x) i) = false).
Axiom nth_var3 : forall (x:Z) (i:Z), ((is_int32 x) /\ ((32%Z <= i)%Z /\
(i <= 51%Z)%Z)) -> ((nth1 (var x) i) = false).
Axiom lemma2 : forall (x:Z), (is_int32 x) -> ((to_nat_sub1 (var x) 51%Z
0%Z) = ((pow2 31%Z) + x)%Z).
Axiom nth_var4 : forall (x:Z), forall (i:Z), ((52%Z <= i)%Z /\
(i <= 53%Z)%Z) -> ((nth1 (var x) i) = true).
Axiom nth_var4 : forall (x:Z) (i:Z), ((is_int32 x) /\ ((52%Z <= i)%Z /\
(i <= 53%Z)%Z)) -> ((nth1 (var x) i) = true).
Axiom nth_var5 : forall (x:Z), forall (i:Z), ((54%Z <= i)%Z /\
(i <= 55%Z)%Z) -> ((nth1 (var x) i) = false).
Axiom nth_var5 : forall (x:Z) (i:Z), ((is_int32 x) /\ ((54%Z <= i)%Z /\
(i <= 55%Z)%Z)) -> ((nth1 (var x) i) = false).
Axiom nth_var6 : forall (x:Z), forall (i:Z), ((56%Z <= i)%Z /\
(i <= 57%Z)%Z) -> ((nth1 (var x) i) = true).
Axiom nth_var6 : forall (x:Z) (i:Z), ((is_int32 x) /\ ((56%Z <= i)%Z /\
(i <= 57%Z)%Z)) -> ((nth1 (var x) i) = true).
Axiom nth_var7 : forall (x:Z), forall (i:Z), ((58%Z <= i)%Z /\
(i <= 61%Z)%Z) -> ((nth1 (var x) i) = false).
Axiom nth_var8 : forall (x:Z), ((nth1 (var x) 62%Z) = true).
Axiom nth_var7 : forall (x:Z) (i:Z), ((is_int32 x) /\ ((58%Z <= i)%Z /\
(i <= 61%Z)%Z)) -> ((nth1 (var x) i) = false).
Axiom nth_var8 : forall (x:Z), (is_int32 x) -> ((nth1 (var x) 62%Z) = true).
Open Scope Z_scope.
Require Import Why3.
......@@ -746,10 +747,12 @@ Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem lemma3 : forall (x:Z), ((to_nat_sub1 (var x) 62%Z 52%Z) = 1075%Z).
intro.
Theorem lemma3 : forall (x:Z), (is_int32 x) -> ((to_nat_sub1 (var x) 62%Z
52%Z) = 1075%Z).
(* intros x. *)
intros x H.
rewrite to_nat_sub_one1; auto with zarith.
2: apply nth_var8.
2: apply nth_var8; auto with zarith.
replace (62 - 52) with 10 by omega.
rewrite pow2_10.
rewrite to_nat_sub_zero1; auto with zarith.
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require bool.Bool.
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
| (_, _) => true
end.
Parameter pow2: Z -> Z.
Axiom Power_0 : ((pow2 0%Z) = 1%Z).
......@@ -158,6 +152,19 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%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_gen : forall (x:Z) (i:Z) (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) ->
((int.EuclideanDivision.mod1 (int.EuclideanDivision.div (x + (pow2 i))%Z
(pow2 k)) 2%Z) = (int.EuclideanDivision.mod1 (int.EuclideanDivision.div x
(pow2 k)) 2%Z)).
Parameter pow21: Z -> R.
Axiom Power_01 : ((pow21 0%Z) = 1%R).
......@@ -200,7 +207,9 @@ Axiom Pow2_int_real : forall (x:Z), (0%Z <= x)%Z ->
Axiom size_positive : (1%Z < 32%Z)%Z.
Parameter bv : Type.
Axiom bv : Type.
Parameter bv_WhyType : WhyType bv.
Existing Instance bv_WhyType.
Parameter nth: bv -> Z -> bool.
......@@ -215,7 +224,7 @@ Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvone
n) = true).
(* Why3 assumption *)
Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
Definition eq (v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < 32%Z)%Z) -> ((nth v1 n) = (nth v2 n)).
Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
......@@ -366,13 +375,15 @@ Axiom nth_from_int2c_low_odd : forall (n:Z),
Axiom nth_from_int2c_0 : forall (i:Z), ((i < 32%Z)%Z /\ (0%Z <= i)%Z) ->
((nth (from_int2c 0%Z) i) = false).