From fdd385baf3adfbe737d5834650327839bf8bd88a Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Fri, 25 May 2018 13:35:30 +0200 Subject: [PATCH] bitvectors: removed some Coq proofs --- examples/bitvectors/bitvector.why | 12 +- .../bitvector_BitVector_to_nat_of_one_1.v | 308 ----------------- .../bitvector_BitVector_to_nat_of_zero_1.v | 309 ----------------- ...tvector_BitVector_to_nat_sub_footprint_1.v | 326 ------------------ examples/bitvectors/bitvector/why3session.xml | 99 ++++-- examples/bitvectors/bitvector/why3shapes.gz | Bin 1556 -> 1982 bytes 6 files changed, 71 insertions(+), 983 deletions(-) delete mode 100644 examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_one_1.v delete mode 100644 examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_zero_1.v delete mode 100644 examples/bitvectors/bitvector/bitvector_BitVector_to_nat_sub_footprint_1.v diff --git a/examples/bitvectors/bitvector.why b/examples/bitvectors/bitvector.why index 9e7e3155a..31e36d2ae 100644 --- a/examples/bitvectors/bitvector.why +++ b/examples/bitvectors/bitvector.why @@ -198,14 +198,16 @@ theory BitVector lemma to_nat_of_zero: - forall b:bv, i j:int. size > j /\ i >= 0 -> + forall b:bv, j i:int. size > j /\ i >= 0 -> (forall k:int. j >= k >= i -> nth b k = False) -> to_nat_sub b j i = 0 - lemma to_nat_of_one: - forall b:bv, i j:int. size > j >= i >= 0 -> - (forall k:int. j >= k >= i -> nth b k = True) -> - to_nat_sub b j i = pow2 (j-i+1) - 1 + let rec lemma to_nat_of_one (b: bv) i j + requires { size > j >= i >= 0 } + requires { forall k:int. j >= k >= i -> nth b k = True } + ensures { to_nat_sub b j i = pow2 (j-i+1) - 1 } + variant { j - i } + = if j > i then to_nat_of_one b i (j-1) lemma to_nat_sub_footprint: forall b1 b2:bv, j i:int. size > j /\ i >=0 -> (forall k:int. i <= k <= j -> nth b1 k = nth b2 k) -> 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 deleted file mode 100644 index 35c16e9e1..000000000 --- a/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_one_1.v +++ /dev/null @@ -1,308 +0,0 @@ -(* This file is generated by Why3's Coq driver *) -(* Beware! Only edit allowed sections below *) -Require Import BuiltIn. -Require BuiltIn. -Require bool.Bool. -Require int.Int. -Require int.Abs. -Require int.EuclideanDivision. - -Parameter pow2: Z -> Z. - -Axiom Power_0 : ((pow2 0%Z) = 1%Z). - -Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> - ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z). - -Axiom Power_1 : ((pow2 1%Z) = 2%Z). - -Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) -> - ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z). - -Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z. - -Axiom pow2_0 : ((pow2 0%Z) = 1%Z). - -Axiom pow2_1 : ((pow2 1%Z) = 2%Z). - -Axiom pow2_2 : ((pow2 2%Z) = 4%Z). - -Axiom pow2_3 : ((pow2 3%Z) = 8%Z). - -Axiom pow2_4 : ((pow2 4%Z) = 16%Z). - -Axiom pow2_5 : ((pow2 5%Z) = 32%Z). - -Axiom pow2_6 : ((pow2 6%Z) = 64%Z). - -Axiom pow2_7 : ((pow2 7%Z) = 128%Z). - -Axiom pow2_8 : ((pow2 8%Z) = 256%Z). - -Axiom pow2_9 : ((pow2 9%Z) = 512%Z). - -Axiom pow2_10 : ((pow2 10%Z) = 1024%Z). - -Axiom pow2_11 : ((pow2 11%Z) = 2048%Z). - -Axiom pow2_12 : ((pow2 12%Z) = 4096%Z). - -Axiom pow2_13 : ((pow2 13%Z) = 8192%Z). - -Axiom pow2_14 : ((pow2 14%Z) = 16384%Z). - -Axiom pow2_15 : ((pow2 15%Z) = 32768%Z). - -Axiom pow2_16 : ((pow2 16%Z) = 65536%Z). - -Axiom pow2_17 : ((pow2 17%Z) = 131072%Z). - -Axiom pow2_18 : ((pow2 18%Z) = 262144%Z). - -Axiom pow2_19 : ((pow2 19%Z) = 524288%Z). - -Axiom pow2_20 : ((pow2 20%Z) = 1048576%Z). - -Axiom pow2_21 : ((pow2 21%Z) = 2097152%Z). - -Axiom pow2_22 : ((pow2 22%Z) = 4194304%Z). - -Axiom pow2_23 : ((pow2 23%Z) = 8388608%Z). - -Axiom pow2_24 : ((pow2 24%Z) = 16777216%Z). - -Axiom pow2_25 : ((pow2 25%Z) = 33554432%Z). - -Axiom pow2_26 : ((pow2 26%Z) = 67108864%Z). - -Axiom pow2_27 : ((pow2 27%Z) = 134217728%Z). - -Axiom pow2_28 : ((pow2 28%Z) = 268435456%Z). - -Axiom pow2_29 : ((pow2 29%Z) = 536870912%Z). - -Axiom pow2_30 : ((pow2 30%Z) = 1073741824%Z). - -Axiom pow2_31 : ((pow2 31%Z) = 2147483648%Z). - -Axiom pow2_32 : ((pow2 32%Z) = 4294967296%Z). - -Axiom pow2_33 : ((pow2 33%Z) = 8589934592%Z). - -Axiom pow2_34 : ((pow2 34%Z) = 17179869184%Z). - -Axiom pow2_35 : ((pow2 35%Z) = 34359738368%Z). - -Axiom pow2_36 : ((pow2 36%Z) = 68719476736%Z). - -Axiom pow2_37 : ((pow2 37%Z) = 137438953472%Z). - -Axiom pow2_38 : ((pow2 38%Z) = 274877906944%Z). - -Axiom pow2_39 : ((pow2 39%Z) = 549755813888%Z). - -Axiom pow2_40 : ((pow2 40%Z) = 1099511627776%Z). - -Axiom pow2_41 : ((pow2 41%Z) = 2199023255552%Z). - -Axiom pow2_42 : ((pow2 42%Z) = 4398046511104%Z). - -Axiom pow2_43 : ((pow2 43%Z) = 8796093022208%Z). - -Axiom pow2_44 : ((pow2 44%Z) = 17592186044416%Z). - -Axiom pow2_45 : ((pow2 45%Z) = 35184372088832%Z). - -Axiom pow2_46 : ((pow2 46%Z) = 70368744177664%Z). - -Axiom pow2_47 : ((pow2 47%Z) = 140737488355328%Z). - -Axiom pow2_48 : ((pow2 48%Z) = 281474976710656%Z). - -Axiom pow2_49 : ((pow2 49%Z) = 562949953421312%Z). - -Axiom pow2_50 : ((pow2 50%Z) = 1125899906842624%Z). - -Axiom pow2_51 : ((pow2 51%Z) = 2251799813685248%Z). - -Axiom pow2_52 : ((pow2 52%Z) = 4503599627370496%Z). - -Axiom pow2_53 : ((pow2 53%Z) = 9007199254740992%Z). - -Axiom pow2_54 : ((pow2 54%Z) = 18014398509481984%Z). - -Axiom pow2_55 : ((pow2 55%Z) = 36028797018963968%Z). - -Axiom pow2_56 : ((pow2 56%Z) = 72057594037927936%Z). - -Axiom pow2_57 : ((pow2 57%Z) = 144115188075855872%Z). - -Axiom pow2_58 : ((pow2 58%Z) = 288230376151711744%Z). - -Axiom pow2_59 : ((pow2 59%Z) = 576460752303423488%Z). - -Axiom pow2_60 : ((pow2 60%Z) = 1152921504606846976%Z). - -Axiom pow2_61 : ((pow2 61%Z) = 2305843009213693952%Z). - -Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z). - -Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z). - -Axiom Div_mult_inst : forall (x:Z) (z:Z), (0%Z < x)%Z -> - ((int.EuclideanDivision.div ((x * 1%Z)%Z + z)%Z - x) = (1%Z + (int.EuclideanDivision.div z x))%Z). - -Axiom Div_double : forall (x:Z) (y:Z), ((0%Z < y)%Z /\ ((y <= x)%Z /\ - (x < (2%Z * y)%Z)%Z)) -> ((int.EuclideanDivision.div x y) = 1%Z). - -Axiom Div_pow : forall (x:Z) (i:Z), (0%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_double_neg : forall (x:Z) (y:Z), ((((-2%Z)%Z * y)%Z <= x)%Z /\ - ((x < (-y)%Z)%Z /\ ((-y)%Z < 0%Z)%Z)) -> ((int.EuclideanDivision.div x - y) = (-2%Z)%Z). - -Axiom Div_pow2 : forall (x:Z) (i:Z), (0%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 size: Z. - -Axiom size_positive : (1%Z < size)%Z. - -Axiom bv : Type. -Parameter bv_WhyType : WhyType bv. -Existing Instance bv_WhyType. - -Parameter nth: bv -> Z -> bool. - -Parameter bvzero: bv. - -Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvzero - n) = false). - -Parameter bvone: bv. - -Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone - n) = true). - -(* Why3 assumption *) -Definition eq (v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth v1 n) = (nth v2 n)). - -Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2). - -Parameter bw_and: bv -> bv -> bv. - -Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth (bw_and v1 v2) n) = (Init.Datatypes.andb (nth v1 - n) (nth v2 n))). - -Parameter bw_or: bv -> bv -> bv. - -Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth (bw_or v1 v2) n) = (Init.Datatypes.orb (nth v1 - n) (nth v2 n))). - -Parameter bw_xor: bv -> bv -> bv. - -Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (Init.Datatypes.xorb (nth v1 - n) (nth v2 n))). - -Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2) - n) = (Init.Datatypes.negb (nth v2 n))). - -Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2 - n)). - -Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2) - n) = (Init.Datatypes.negb (nth v1 n))). - -Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1 - n)). - -Parameter bw_not: bv -> bv. - -Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> - ((nth (bw_not v) n) = (Init.Datatypes.negb (nth v n))). - -Parameter lsr: bv -> Z -> bv. - -Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\ - ((n + s)%Z < size)%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 < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\ - (size <= (n + s)%Z)%Z)) -> ((nth (lsr b s) n) = false). - -Parameter asr: bv -> Z -> bv. - -Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < size)%Z -> ((nth (asr b s) - n) = (nth b (n + s)%Z)))). - -Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (asr b s) - n) = (nth b (size - 1%Z)%Z)))). - -Parameter lsl: bv -> Z -> bv. - -Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s) - n) = (nth b (n - s)%Z)))). - -Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s) - n) = false))). - -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 /\ (j < size)%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 < size)%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), ((j < size)%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), ((j < size)%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)). - -Require Import Why3. -Ltac cvc := why3 "CVC3,2.4.1," timelimit 5; admit. -Open Scope Z_scope. - -(* Why3 goal *) -Theorem to_nat_of_one : forall (b:bv) (i:Z) (j:Z), ((j < size)%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)). -(* Why3 intros b i j (h1,(h2,h3)) h4. *) -intros b i j (Hj,(Hij,Hi)). -generalize Hij Hj. -pattern j; apply Zlt_lower_bound_ind with (z:=i); auto. -cvc. -Admitted. - diff --git a/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_zero_1.v b/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_zero_1.v deleted file mode 100644 index 66ceafa55..000000000 --- a/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_zero_1.v +++ /dev/null @@ -1,309 +0,0 @@ -(* This file is generated by Why3's Coq driver *) -(* Beware! Only edit allowed sections below *) -Require Import BuiltIn. -Require BuiltIn. -Require bool.Bool. -Require int.Int. -Require int.Abs. -Require int.EuclideanDivision. - -Parameter pow2: Z -> Z. - -Axiom Power_0 : ((pow2 0%Z) = 1%Z). - -Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> - ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z). - -Axiom Power_1 : ((pow2 1%Z) = 2%Z). - -Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) -> - ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z). - -Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z. - -Axiom pow2_0 : ((pow2 0%Z) = 1%Z). - -Axiom pow2_1 : ((pow2 1%Z) = 2%Z). - -Axiom pow2_2 : ((pow2 2%Z) = 4%Z). - -Axiom pow2_3 : ((pow2 3%Z) = 8%Z). - -Axiom pow2_4 : ((pow2 4%Z) = 16%Z). - -Axiom pow2_5 : ((pow2 5%Z) = 32%Z). - -Axiom pow2_6 : ((pow2 6%Z) = 64%Z). - -Axiom pow2_7 : ((pow2 7%Z) = 128%Z). - -Axiom pow2_8 : ((pow2 8%Z) = 256%Z). - -Axiom pow2_9 : ((pow2 9%Z) = 512%Z). - -Axiom pow2_10 : ((pow2 10%Z) = 1024%Z). - -Axiom pow2_11 : ((pow2 11%Z) = 2048%Z). - -Axiom pow2_12 : ((pow2 12%Z) = 4096%Z). - -Axiom pow2_13 : ((pow2 13%Z) = 8192%Z). - -Axiom pow2_14 : ((pow2 14%Z) = 16384%Z). - -Axiom pow2_15 : ((pow2 15%Z) = 32768%Z). - -Axiom pow2_16 : ((pow2 16%Z) = 65536%Z). - -Axiom pow2_17 : ((pow2 17%Z) = 131072%Z). - -Axiom pow2_18 : ((pow2 18%Z) = 262144%Z). - -Axiom pow2_19 : ((pow2 19%Z) = 524288%Z). - -Axiom pow2_20 : ((pow2 20%Z) = 1048576%Z). - -Axiom pow2_21 : ((pow2 21%Z) = 2097152%Z). - -Axiom pow2_22 : ((pow2 22%Z) = 4194304%Z). - -Axiom pow2_23 : ((pow2 23%Z) = 8388608%Z). - -Axiom pow2_24 : ((pow2 24%Z) = 16777216%Z). - -Axiom pow2_25 : ((pow2 25%Z) = 33554432%Z). - -Axiom pow2_26 : ((pow2 26%Z) = 67108864%Z). - -Axiom pow2_27 : ((pow2 27%Z) = 134217728%Z). - -Axiom pow2_28 : ((pow2 28%Z) = 268435456%Z). - -Axiom pow2_29 : ((pow2 29%Z) = 536870912%Z). - -Axiom pow2_30 : ((pow2 30%Z) = 1073741824%Z). - -Axiom pow2_31 : ((pow2 31%Z) = 2147483648%Z). - -Axiom pow2_32 : ((pow2 32%Z) = 4294967296%Z). - -Axiom pow2_33 : ((pow2 33%Z) = 8589934592%Z). - -Axiom pow2_34 : ((pow2 34%Z) = 17179869184%Z). - -Axiom pow2_35 : ((pow2 35%Z) = 34359738368%Z). - -Axiom pow2_36 : ((pow2 36%Z) = 68719476736%Z). - -Axiom pow2_37 : ((pow2 37%Z) = 137438953472%Z). - -Axiom pow2_38 : ((pow2 38%Z) = 274877906944%Z). - -Axiom pow2_39 : ((pow2 39%Z) = 549755813888%Z). - -Axiom pow2_40 : ((pow2 40%Z) = 1099511627776%Z). - -Axiom pow2_41 : ((pow2 41%Z) = 2199023255552%Z). - -Axiom pow2_42 : ((pow2 42%Z) = 4398046511104%Z). - -Axiom pow2_43 : ((pow2 43%Z) = 8796093022208%Z). - -Axiom pow2_44 : ((pow2 44%Z) = 17592186044416%Z). - -Axiom pow2_45 : ((pow2 45%Z) = 35184372088832%Z). - -Axiom pow2_46 : ((pow2 46%Z) = 70368744177664%Z). - -Axiom pow2_47 : ((pow2 47%Z) = 140737488355328%Z). - -Axiom pow2_48 : ((pow2 48%Z) = 281474976710656%Z). - -Axiom pow2_49 : ((pow2 49%Z) = 562949953421312%Z). - -Axiom pow2_50 : ((pow2 50%Z) = 1125899906842624%Z). - -Axiom pow2_51 : ((pow2 51%Z) = 2251799813685248%Z). - -Axiom pow2_52 : ((pow2 52%Z) = 4503599627370496%Z). - -Axiom pow2_53 : ((pow2 53%Z) = 9007199254740992%Z). - -Axiom pow2_54 : ((pow2 54%Z) = 18014398509481984%Z). - -Axiom pow2_55 : ((pow2 55%Z) = 36028797018963968%Z). - -Axiom pow2_56 : ((pow2 56%Z) = 72057594037927936%Z). - -Axiom pow2_57 : ((pow2 57%Z) = 144115188075855872%Z). - -Axiom pow2_58 : ((pow2 58%Z) = 288230376151711744%Z). - -Axiom pow2_59 : ((pow2 59%Z) = 576460752303423488%Z). - -Axiom pow2_60 : ((pow2 60%Z) = 1152921504606846976%Z). - -Axiom pow2_61 : ((pow2 61%Z) = 2305843009213693952%Z). - -Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z). - -Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z). - -Axiom Div_mult_inst : forall (x:Z) (z:Z), (0%Z < x)%Z -> - ((int.EuclideanDivision.div ((x * 1%Z)%Z + z)%Z - x) = (1%Z + (int.EuclideanDivision.div z x))%Z). - -Axiom Div_double : forall (x:Z) (y:Z), ((0%Z < y)%Z /\ ((y <= x)%Z /\ - (x < (2%Z * y)%Z)%Z)) -> ((int.EuclideanDivision.div x y) = 1%Z). - -Axiom Div_pow : forall (x:Z) (i:Z), (0%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_double_neg : forall (x:Z) (y:Z), ((((-2%Z)%Z * y)%Z <= x)%Z /\ - ((x < (-y)%Z)%Z /\ ((-y)%Z < 0%Z)%Z)) -> ((int.EuclideanDivision.div x - y) = (-2%Z)%Z). - -Axiom Div_pow2 : forall (x:Z) (i:Z), (0%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 size: Z. - -Axiom size_positive : (1%Z < size)%Z. - -Axiom bv : Type. -Parameter bv_WhyType : WhyType bv. -Existing Instance bv_WhyType. - -Parameter nth: bv -> Z -> bool. - -Parameter bvzero: bv. - -Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvzero - n) = false). - -Parameter bvone: bv. - -Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone - n) = true). - -(* Why3 assumption *) -Definition eq (v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth v1 n) = (nth v2 n)). - -Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2). - -Parameter bw_and: bv -> bv -> bv. - -Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth (bw_and v1 v2) n) = (Init.Datatypes.andb (nth v1 - n) (nth v2 n))). - -Parameter bw_or: bv -> bv -> bv. - -Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth (bw_or v1 v2) n) = (Init.Datatypes.orb (nth v1 - n) (nth v2 n))). - -Parameter bw_xor: bv -> bv -> bv. - -Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (Init.Datatypes.xorb (nth v1 - n) (nth v2 n))). - -Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2) - n) = (Init.Datatypes.negb (nth v2 n))). - -Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2 - n)). - -Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2) - n) = (Init.Datatypes.negb (nth v1 n))). - -Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1 - n)). - -Parameter bw_not: bv -> bv. - -Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> - ((nth (bw_not v) n) = (Init.Datatypes.negb (nth v n))). - -Parameter lsr: bv -> Z -> bv. - -Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\ - ((n + s)%Z < size)%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 < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\ - (size <= (n + s)%Z)%Z)) -> ((nth (lsr b s) n) = false). - -Parameter asr: bv -> Z -> bv. - -Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < size)%Z -> ((nth (asr b s) - n) = (nth b (n + s)%Z)))). - -Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (asr b s) - n) = (nth b (size - 1%Z)%Z)))). - -Parameter lsl: bv -> Z -> bv. - -Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s) - n) = (nth b (n - s)%Z)))). - -Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s) - n) = false))). - -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 /\ (j < size)%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 < size)%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), ((j < size)%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))). - -Require Import Why3. -Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 5; admit. -Ltac cvc := why3 "CVC3,2.4.1," timelimit 5; admit. -Open Scope Z_scope. - - -(* Why3 goal *) -Theorem to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < size)%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)). -(* Why3 intros b i j (h1,h2) h3. *) -(* intros b i j (h1,h2) h3. *) -intros b i j (Hj & Hi). -assert (h:(i>j)\/(i<=j)) by omega; destruct h. -ae. -generalize Hj. -pattern j. -apply Zlt_lower_bound_ind with (z:=i); auto. -cvc. -Admitted. - diff --git a/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_sub_footprint_1.v b/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_sub_footprint_1.v deleted file mode 100644 index 756b06920..000000000 --- a/examples/bitvectors/bitvector/bitvector_BitVector_to_nat_sub_footprint_1.v +++ /dev/null @@ -1,326 +0,0 @@ -(* This file is generated by Why3's Coq driver *) -(* Beware! Only edit allowed sections below *) -Require Import BuiltIn. -Require BuiltIn. -Require bool.Bool. -Require int.Int. -Require int.Abs. -Require int.EuclideanDivision. - -Parameter pow2: Z -> Z. - -Axiom Power_0 : ((pow2 0%Z) = 1%Z). - -Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> - ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z). - -Axiom Power_1 : ((pow2 1%Z) = 2%Z). - -Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) -> - ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z). - -Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z. - -Axiom pow2_0 : ((pow2 0%Z) = 1%Z). - -Axiom pow2_1 : ((pow2 1%Z) = 2%Z). - -Axiom pow2_2 : ((pow2 2%Z) = 4%Z). - -Axiom pow2_3 : ((pow2 3%Z) = 8%Z). - -Axiom pow2_4 : ((pow2 4%Z) = 16%Z). - -Axiom pow2_5 : ((pow2 5%Z) = 32%Z). - -Axiom pow2_6 : ((pow2 6%Z) = 64%Z). - -Axiom pow2_7 : ((pow2 7%Z) = 128%Z). - -Axiom pow2_8 : ((pow2 8%Z) = 256%Z). - -Axiom pow2_9 : ((pow2 9%Z) = 512%Z). - -Axiom pow2_10 : ((pow2 10%Z) = 1024%Z). - -Axiom pow2_11 : ((pow2 11%Z) = 2048%Z). - -Axiom pow2_12 : ((pow2 12%Z) = 4096%Z). - -Axiom pow2_13 : ((pow2 13%Z) = 8192%Z). - -Axiom pow2_14 : ((pow2 14%Z) = 16384%Z). - -Axiom pow2_15 : ((pow2 15%Z) = 32768%Z). - -Axiom pow2_16 : ((pow2 16%Z) = 65536%Z). - -Axiom pow2_17 : ((pow2 17%Z) = 131072%Z). - -Axiom pow2_18 : ((pow2 18%Z) = 262144%Z). - -Axiom pow2_19 : ((pow2 19%Z) = 524288%Z). - -Axiom pow2_20 : ((pow2 20%Z) = 1048576%Z). - -Axiom pow2_21 : ((pow2 21%Z) = 2097152%Z). - -Axiom pow2_22 : ((pow2 22%Z) = 4194304%Z). - -Axiom pow2_23 : ((pow2 23%Z) = 8388608%Z). - -Axiom pow2_24 : ((pow2 24%Z) = 16777216%Z). - -Axiom pow2_25 : ((pow2 25%Z) = 33554432%Z). - -Axiom pow2_26 : ((pow2 26%Z) = 67108864%Z). - -Axiom pow2_27 : ((pow2 27%Z) = 134217728%Z). - -Axiom pow2_28 : ((pow2 28%Z) = 268435456%Z). - -Axiom pow2_29 : ((pow2 29%Z) = 536870912%Z). - -Axiom pow2_30 : ((pow2 30%Z) = 1073741824%Z). - -Axiom pow2_31 : ((pow2 31%Z) = 2147483648%Z). - -Axiom pow2_32 : ((pow2 32%Z) = 4294967296%Z). - -Axiom pow2_33 : ((pow2 33%Z) = 8589934592%Z). - -Axiom pow2_34 : ((pow2 34%Z) = 17179869184%Z). - -Axiom pow2_35 : ((pow2 35%Z) = 34359738368%Z). - -Axiom pow2_36 : ((pow2 36%Z) = 68719476736%Z). - -Axiom pow2_37 : ((pow2 37%Z) = 137438953472%Z). - -Axiom pow2_38 : ((pow2 38%Z) = 274877906944%Z). - -Axiom pow2_39 : ((pow2 39%Z) = 549755813888%Z). - -Axiom pow2_40 : ((pow2 40%Z) = 1099511627776%Z). - -Axiom pow2_41 : ((pow2 41%Z) = 2199023255552%Z). - -Axiom pow2_42 : ((pow2 42%Z) = 4398046511104%Z). - -Axiom pow2_43 : ((pow2 43%Z) = 8796093022208%Z). - -Axiom pow2_44 : ((pow2 44%Z) = 17592186044416%Z). - -Axiom pow2_45 : ((pow2 45%Z) = 35184372088832%Z). - -Axiom pow2_46 : ((pow2 46%Z) = 70368744177664%Z). - -Axiom pow2_47 : ((pow2 47%Z) = 140737488355328%Z). - -Axiom pow2_48 : ((pow2 48%Z) = 281474976710656%Z). - -Axiom pow2_49 : ((pow2 49%Z) = 562949953421312%Z). - -Axiom pow2_50 : ((pow2 50%Z) = 1125899906842624%Z). - -Axiom pow2_51 : ((pow2 51%Z) = 2251799813685248%Z). - -Axiom pow2_52 : ((pow2 52%Z) = 4503599627370496%Z). - -Axiom pow2_53 : ((pow2 53%Z) = 9007199254740992%Z). - -Axiom pow2_54 : ((pow2 54%Z) = 18014398509481984%Z). - -Axiom pow2_55 : ((pow2 55%Z) = 36028797018963968%Z). - -Axiom pow2_56 : ((pow2 56%Z) = 72057594037927936%Z). - -Axiom pow2_57 : ((pow2 57%Z) = 144115188075855872%Z). - -Axiom pow2_58 : ((pow2 58%Z) = 288230376151711744%Z). - -Axiom pow2_59 : ((pow2 59%Z) = 576460752303423488%Z). - -Axiom pow2_60 : ((pow2 60%Z) = 1152921504606846976%Z). - -Axiom pow2_61 : ((pow2 61%Z) = 2305843009213693952%Z). - -Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z). - -Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z). - -Axiom Div_mult_inst : forall (x:Z) (z:Z), (0%Z < x)%Z -> - ((int.EuclideanDivision.div ((x * 1%Z)%Z + z)%Z - x) = (1%Z + (int.EuclideanDivision.div z x))%Z). - -Axiom Div_double : forall (x:Z) (y:Z), ((0%Z < y)%Z /\ ((y <= x)%Z /\ - (x < (2%Z * y)%Z)%Z)) -> ((int.EuclideanDivision.div x y) = 1%Z). - -Axiom Div_pow : forall (x:Z) (i:Z), (0%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_double_neg : forall (x:Z) (y:Z), ((((-2%Z)%Z * y)%Z <= x)%Z /\ - ((x < (-y)%Z)%Z /\ ((-y)%Z < 0%Z)%Z)) -> ((int.EuclideanDivision.div x - y) = (-2%Z)%Z). - -Axiom Div_pow2 : forall (x:Z) (i:Z), (0%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 size: Z. - -Axiom size_positive : (1%Z < size)%Z. - -Axiom bv : Type. -Parameter bv_WhyType : WhyType bv. -Existing Instance bv_WhyType. - -Parameter nth: bv -> Z -> bool. - -Parameter bvzero: bv. - -Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvzero - n) = false). - -Parameter bvone: bv. - -Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone - n) = true). - -(* Why3 assumption *) -Definition eq (v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth v1 n) = (nth v2 n)). - -Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2). - -Parameter bw_and: bv -> bv -> bv. - -Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth (bw_and v1 v2) n) = (Init.Datatypes.andb (nth v1 - n) (nth v2 n))). - -Parameter bw_or: bv -> bv -> bv. - -Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth (bw_or v1 v2) n) = (Init.Datatypes.orb (nth v1 - n) (nth v2 n))). - -Parameter bw_xor: bv -> bv -> bv. - -Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (Init.Datatypes.xorb (nth v1 - n) (nth v2 n))). - -Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2) - n) = (Init.Datatypes.negb (nth v2 n))). - -Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2 - n)). - -Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2) - n) = (Init.Datatypes.negb (nth v1 n))). - -Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1 - n)). - -Parameter bw_not: bv -> bv. - -Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> - ((nth (bw_not v) n) = (Init.Datatypes.negb (nth v n))). - -Parameter lsr: bv -> Z -> bv. - -Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\ - (n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\ - ((n + s)%Z < size)%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 < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\ - (size <= (n + s)%Z)%Z)) -> ((nth (lsr b s) n) = false). - -Parameter asr: bv -> Z -> bv. - -Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < size)%Z -> ((nth (asr b s) - n) = (nth b (n + s)%Z)))). - -Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (asr b s) - n) = (nth b (size - 1%Z)%Z)))). - -Parameter lsl: bv -> Z -> bv. - -Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s) - n) = (nth b (n - s)%Z)))). - -Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ - (n < size)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s) - n) = false))). - -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 /\ (j < size)%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 < size)%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), ((j < size)%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), ((j < size)%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 < size)%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)). - -Require Import Why3. -Ltac ae := why3 "alt-ergo" timelimit 15; admit. -Open Scope Z_scope. - -(* Why3 goal *) -Theorem to_nat_sub_footprint : forall (b1:bv) (b2:bv) (j:Z) (i:Z), - ((j < size)%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))). -(* Why3 intros b1 b2 j i (h1,h2) h3. *) -(* intros b1 b2 j i (h1,h2) h3. *) -intros b1 b2 j i (Hij,Hipos). -assert (h:(j < i \/ i <= j)) by omega; destruct h. -ae. -generalize Hij. -pattern j; apply Zlt_lower_bound_ind with (z:=i); auto. -clear j Hij H. -intros j Hind Hij Hj Hfootprint. -assert (h:i=j \/ i - - + @@ -48,13 +47,48 @@ - + + + + + + + + + + + + - - + + + + + + + + + + + + + + + - + + + + + + + + + + + + @@ -86,7 +120,7 @@ - + @@ -138,83 +172,78 @@ - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - + diff --git a/examples/bitvectors/bitvector/why3shapes.gz b/examples/bitvectors/bitvector/why3shapes.gz index a28489978be6e586d8b23f3dbab27d7d08c66d06..e1a3048aa0bad9be2ecbb1bb366b9ee62ae59ed4 100644 GIT binary patch literal 1982 zcmV;v2SNBBiwFP!00000|GiktYGg+e-QTaM{V))b8TkUYVHglJG@i{++a@wHgHg{| z)ktdF`0M9fJzBR^Qb}Ie2t6vRZbW1}&N(6NV@xvA*;*@O9ZPBuDPU~!=xZXJeCyaG;<$qc=z*;A8$?1 zz4JS7-K<;b!Nf>ZRW$V!TCOx^ja2E4TfgY{UAJZpi9(#Mhat$ikS6k~X;f<@8^^bY z&sTc;`Q}?+-Jv^<4%p~<-s61)kH=_mkVYkvm10lN;?ch6lX!T) z=>Cnr z>(|4t;o-&K9uLT@@`U)j_^nJ>0;aU zNBAR~k1i~fdkDQvAmqqvaui@)i-RLFn*A5OzJ$}=n07s%s`$hA8y)oW``=&matp%S z^Th!jD-wwkI44c3fjMcjP@8 z;3b#TBU1ycn7w59q0#iecX?c(0n+RVY*=O-Rcj%u4Y)+TmDa}Y>*411)W&fmZ}RX` zmDdlfRR+|@H0L_ZgS%)17e>jH+w>J!?KN5gxNQ!2J$Md(@<5RC@p~0e?(kF-w3=)u zC!PQxxJdF~a3*fgDQYM*EVU*UBG)wR6#(RQl#fordh%?v8MAQr2by{lBp%)bN$(hM z)Rr}ZF2ozLatDV(z8m5thbhLo#E0vKw9?LerKK%Uo^6GZAbqwAg^ykCCF}N1oI#TzFd99G135^D* zf$~nXKo1I)Ge++K@28iHj?j{q=soqoMWCn)XxovC;aS3b*(fw3ozTolCibw;nVj>` ziFg}yGiimmvRHacv&~mB5$ugz#Hv=I$SF}YWs$YS5^Lea9L3L?eLWkE0khnSKu0!< z2?0V+vO`wYh_-mm?ECYvs%m(lI<(Q6=h(^^R;;2mH1TU59uX0KR)D;t)#q2+H0_2p zSI@>zdY`wLW@|SuFh7RlvJ`9()+raqpEMeCXf5xKuCc;!gLaWn%1n+0MWtaWC^>lO z&{b7W9>|;;s)cQ);@(i#oEaUa$~t<9_2}Bj+=Gbuw5~LIHMIZo`@BBj7j(vwumWje zzyUb7=Z;E&7XzEa;w*k*?4I#I!Q%D33FEw2Ym>mJ;uTViVu2u^QLQm3*14Tn$&WD| znaSYGC>3dNm29K7MA#VEr(!WRdo>u{T1kUMERPwZ1A@_Nv5I39U4hbZyb#O_Rv_16 zuC4?c2bW_>P0^s+Ajf^=d>YI5E3IZW*SZVIOloszzUD=c*fDvwF&&b}`;_NQ_D~}% zCBu_M!ZLw?P7luw>~@*G!^kF$fB5Q7I0Jz~c=LX2ojDUC8t_POoz zWN~pwFhe(M&o&if?BFyX9oaGLC+GYJM7rc8qlP930@%p5%DXTCTrn%~{G9&)W=#uK zPe7;GbwcL%5xUJ1QozREC#LJ10gwjfE6`*EEJwgZXLoI5k?5ob&z43C&o!Dw`oL4a0tDLkBPmRk#uJ1GH7Lsy4N zLndk#3`Lkja)SRt=!SC^BBJJndX6QNc#cV}qjwavp$)YGgOsyrz#0I*ODf!{S`MLv zNwdQY494a%7~f}uz_v(I7L~L@1jpdSnC&<^fCr+VGMa(HITK_;EiKY&U0r5Ww}8UC zBc_zH$&{jWE}7h{a^qzN84zpT2B(!U6nerl`lX1iLgSnXG-U>XEu%m%d2X2zKnBdU zD466fmNeU`INjQSk5F=13UHwTDgpe^WFb_+x>K>fV%65{XRm_ROerEAxmCb-CIt}+ z1dSB1cIXu=gi=3y7j!4Klfp}2^s>y{I{2T~|A9;}H}C_ToyEsFBWTbZSkN9?2r>uc z)o>D0X-bxn>1>|5o$D}0j|KtMEFiVaXj#)pl+a%}we^2I1MjC+&NT?HZ7MYtj7uHR zhrywhEN1|bgMfjf8V7#Oa>mM9-vT+mLQlYISO(Zx!VnMBK?12k93ifmPE&ht0V#m+ Q2S}&o|IH?WG3FHj0P~04+yDRo literal 1556 zcmV+v2J87BiwFP!00000|D9LCZX`Djz4ur6z6c;vqC^65fV~VbK(MDpUk4N=Azp0k z!1g3TzJ6bM>~VYAu5lI(v|Z||CyIRUk>!1inIic#%f)(^!9l}{@G2?RgUQz*^fvs?{_oq*^Pi8aKjQlC>aXYP%fKxk4nv!g zP0{GwRp(lB8tIrK(VTd1^SAc>;Qzh*?#5c1)XFn)8D-@rdCrKnhK<$N{>D$IPT%fM z?>x0dkJdR#q~h+yr3+itG^XaH={u)>b>DZLnw%wZp4NF3WW6MpwA5v2SSlwQ-`{+? z_WMtFpZm5Q*zsb4B7K|p{3U{?<)4oENKf1Uba~`s{_yen5&$oLe7^M|?uR7x(s-oa zd!SC4sxTs-D_Ilj$zO}ryZ`4!tXQ~;bTFOa%sK|XmhqtMOMA()q7alXy5G%plC$?TpX2cUQmvZDcMUjsw@mY4~z7H5D%eol4H}R+-*Y zm&^AT=4&bP>Xm{`a;MQ|wYgX(w?u|dD{sg1_`?tW+sz;Rc=3;?#fO0LIS+Xg(fsM(4Q|eKAeXV@bAbrM23I<~QTdrwg<#d>d_#EHKMafdgDLn88Ii0moWZ}vwNu+()x3f_wn?-A4!;+6= zIr-{_ShGu={ub=}^Pwh|zyS86b3IXfYjut2 zqmC`qFBEP-hP1yss~yn@}MZ46ro4L=?COGAtlBRXDIb4rWY_F zTPIs+JK7zC2gtKgTuL4VHt%l+((k!lLdI_DhWolxZjqemkKJyGku=Tl^)p%NkllV{X~ z(V`SY+?Awe0_x854D}ztQNv6T1$6GSJ1nI_449?Sn^xhy=M@D$tfY`Lp>DdsGF29m zHXE;zVO6^T4LLYe%pC%1SEEupW&~n|z7lVQ0NNfvjhYX=t%1X$>tNzC$PENVB$z!? zF2mLyfCOtcbYJOWYbgK zLjd=Q4l;cqfI1qau51Va({ApJX{FYF*5^+V&|+}!L0B;zwgxr|7=&WPXm~9slu#tu zJqAW3bjO2N%=2pS$40qhMl8|mG`K{C+H{vrDM~WI0JsV|Ew9yNF3g$eE*QNm6P9bY z9SAa{&Ioojwl}D>y5|fz=ApAd7!3Ogk+YfY6au8IS@R)xm>eA5Gh)fGY*mzEfn%6X z``SweftQTw>HuluC1X1V5HQF>l$B~x2yDVAcH;mwMY0^g%4n%HQ9HJL$nI>!3DFvOZ?SX7GEtnDIkX5Ri(593aEK1&c z#p@%(@}}&OeXB1T55sye663YsS?fp**