diff --git a/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_one_1.v b/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_one_1.v index b31ed15ff545c9ac0d58a197016365557b15aef0..f85c0a9e09d34742f5f853396805ecf2eb9750f4 100644 --- a/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_one_1.v +++ b/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_one_1.v @@ -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. diff --git a/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_zero2_1.v b/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_zero2_1.v index 7aadf2a11e0d8ef28c024b5dccc5b029bbe1aa06..2940b6e4447b0f095ad93f62746a0a765534295d 100644 --- a/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_zero2_1.v +++ b/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_zero2_1.v @@ -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. diff --git a/examples/bitvectors/bitvector/why3session.xml b/examples/bitvectors/bitvector/why3session.xml index ab13694d7ed379391f2b003959ec264e34371d45..93bf476cf715d4dec00f86bdc705efde6cec2518 100644 --- a/examples/bitvectors/bitvector/why3session.xml +++ b/examples/bitvectors/bitvector/why3session.xml @@ -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 >V3V1Aainfix >=V2V3FIainfix >=V1c0Aainfix >=V2V1Aainfix >asizeV2F"> - + - + 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. diff --git a/examples/bitvectors/double_of_int/why3session.xml b/examples/bitvectors/double_of_int/why3session.xml index 9776e99cda2bdebd09bbfb07c2eeb8562a9748ea..bdc6db889897ce89910279ade43f221363ccd6a2 100644 --- a/examples/bitvectors/double_of_int/why3session.xml +++ b/examples/bitvectors/double_of_int/why3session.xml @@ -1453,7 +1453,7 @@ edited="double_of_int_DoubleOfInt_lemma3_1.v" obsolete="false" archived="false"> - +