Commit ae1d164c authored by MARCHE Claude's avatar MARCHE Claude

Nightly bench: fixed Coq proofs in bitvectors example

parent 621dfd52
......@@ -276,7 +276,6 @@ Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\
k) = false)) -> ((to_nat_sub b j i) = 0%Z)).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 5.
Open Scope Z_scope.
(* Why3 goal *)
......@@ -287,7 +286,7 @@ Theorem to_nat_of_one : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\
intros b i j ((Hj,Hij),Hi).
generalize Hij Hj.
pattern j; apply Zlt_lower_bound_ind with (z:=i); auto.
ae.
why3 "cvc3" timelimit 3.
Qed.
......@@ -266,8 +266,10 @@ Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), (((0%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).
(*
Require Import Why3.
Ltac ae := why3 "Alt-Ergo,0.94" timelimit 5.
Ltac ae := why3 "alt-ergo" timelimit 3.
*)
Open Scope Z_scope.
(* Why3 goal *)
......@@ -278,20 +280,13 @@ Theorem to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\
intros b i j ((Hj,Hij),Hipos).
generalize Hj.
pattern j; apply Zlt_lower_bound_ind with (z:=i); auto.
ae.
(*
clear j Hj.
clear j Hj Hij.
intros j Hind Hij.
assert (h:(i=j \/i < j)) by omega.
destruct h.
subst x; auto.
subst; auto.
intros Hbits Hnth.
rewrite to_nat_sub_zero; auto with zarith.
destruct Hij.
exact H0.
destruct Hij.
exact H.
*)
Qed.
......@@ -169,7 +169,7 @@
loclnum="194" loccnumb="8" loccnume="23"
sum="ddd6fee47a8de55bacf25bea4395fa36"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ato_nat_subV0V2c0ato_nat_subV0V1c0Iainfix =anthV0V3aFalseIainfix &gt;V3V1Aainfix &gt;=V2V3FIainfix &gt;=V1c0Aainfix &gt;=V2V1Aainfix &gt;asizeV2F">
<proof
prover="4"
......@@ -178,7 +178,7 @@
edited="bitvector_BitVector_to_nat_of_zero2_1.v"
obsolete="false"
archived="false">
<result status="valid" time="3.21"/>
<result status="valid" time="0.55"/>
</proof>
</goal>
<goal
......@@ -205,7 +205,7 @@
loclnum="205" loccnumb="8" loccnume="21"
sum="9c6d165a2c55b6b73c6f243c3942c38f"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ato_nat_subV0V2V1ainfix -apow2ainfix +ainfix -V2V1c1c1Iainfix =anthV0V3aTrueIainfix &gt;=V3V1Aainfix &gt;=V2V3FIainfix &gt;=V1c0Aainfix &gt;=V2V1Aainfix &gt;asizeV2F">
<proof
prover="4"
......@@ -214,7 +214,7 @@
edited="bitvector_BitVector_to_nat_of_one_1.v"
obsolete="false"
archived="false">
<result status="valid" time="4.09"/>
<result status="valid" time="0.80"/>
</proof>
</goal>
<goal
......@@ -223,7 +223,7 @@
loclnum="210" loccnumb="8" loccnume="28"
sum="a8a471b72099b8d903352cccd7be8a47"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ato_nat_subV0V2V3ato_nat_subV1V2V3Iainfix =anthV0V4anthV1V4Iainfix &lt;=V4V2Aainfix &lt;=V3V4FIainfix &gt;=V3c0Aainfix &gt;asizeV2F">
<proof
prover="4"
......
(* This file is generated by Why3's Coq 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.
......@@ -9,13 +9,6 @@ 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 +151,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 +206,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.
......@@ -366,13 +374,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.
......@@ -540,9 +550,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.
......@@ -673,22 +683,19 @@ Axiom to_nat_sub_0_30 : forall (x:Z), (is_int32 x) ->
Axiom jpxorx_pos : forall (x:Z), (0%Z <= x)%Z ->
((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = true).
Axiom from_int2c_to_nat_sub_gen : forall (i:Z), ((0%Z <= i)%Z /\
(i <= 30%Z)%Z) -> forall (x:Z), ((0%Z <= x)%Z /\ (x < (pow2 i))%Z) ->
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 from_int2c_to_nat_sub : forall (x:Z), ((is_int32 x) /\ (0%Z <= x)%Z) ->
((to_nat_sub (from_int2c x) 30%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 to_nat_sub_0_30_neg : forall (x:Z), ((is_int32 x) /\ (x < 0%Z)%Z) ->
((to_nat_sub (bw_xor (from_int 2147483648%Z) (from_int2c x)) 30%Z
0%Z) = (to_nat_sub (from_int2c x) 30%Z 0%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 to_nat_sub_0_30_neg1 : forall (x:Z), ((is_int32 x) /\ (x < 0%Z)%Z) ->
((to_nat_sub (from_int2c x) 30%Z 0%Z) = ((pow2 31%Z) + x)%Z).
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_neg : forall (x:Z), ((is_int32 x) /\ (x < 0%Z)%Z) ->
((to_nat_sub (jpxor x) 31%Z 0%Z) = ((pow2 31%Z) + x)%Z).
......@@ -733,7 +740,6 @@ Axiom nth_var7 : forall (x:Z), forall (i:Z), ((58%Z <= i)%Z /\
Axiom nth_var8 : forall (x:Z), ((nth1 (var x) 62%Z) = true).
Open Scope Z_scope.
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
......@@ -766,8 +772,9 @@ rewrite to_nat_sub_zero1; auto with zarith.
2: apply nth_var5; auto with zarith.
rewrite to_nat_sub_zero1; auto with zarith.
2: apply nth_var5; auto with zarith.
rewrite to_nat_sub_one1; auto with zarith.
2: ae.
ae.
Qed.
......@@ -1453,7 +1453,7 @@
edited="double_of_int_DoubleOfInt_lemma3_1.v"
obsolete="false"
archived="false">
<result status="valid" time="2.23"/>
<result status="valid" time="2.64"/>
</proof>
</goal>
<goal
......
Markdown is supported
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