Commit b2003f43 authored by Thi-Minh-Tuyen Nguyen's avatar Thi-Minh-Tuyen Nguyen

add bitvector1/*.v

parent 9bee04c0
......@@ -94,6 +94,10 @@ theory Pow2real
axiom Power_p : forall n: int. n <= 0 -> pow2 (n-1) = 0.5 *. pow2 n
(* axiom Power_s : forall n:int. pow2 (n+1) = 2.0 *. pow2 n
axiom Power_p : forall n:int. pow2 (n-1) = 0.5 *. pow2 n
*)
lemma Power_1 : pow2 1 = 2.0
lemma Power_neg1 : pow2 (-1) = 0.5
......@@ -742,6 +746,12 @@ theory TestDoubleOfInt
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 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
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 ->
......@@ -750,12 +760,13 @@ theory TestDoubleOfInt
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 mantissa_var_x_negative:
forall x:int. (BV64.nth (var x) 31) = False ->
mantissa(var(x)) = Pow2int.pow2 31 - x
mantissa(var(x)) = Pow2int.pow2 31 + x
lemma mantissa_var: forall x:int. mantissa(var(x)) = Pow2int.pow2 31 + x
......
......@@ -2,6 +2,12 @@
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Parameter pow2: Z -> Z.
......@@ -148,6 +154,8 @@ Parameter size: Z.
Parameter bv : Type.
Axiom size_positive : (0%Z < size)%Z.
Parameter nth: bv -> Z -> bool.
......@@ -211,13 +219,13 @@ Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
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 -> (((n + s)%Z < size)%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 < 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 -> ((size <= (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 < 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.
......@@ -263,18 +271,19 @@ 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_one : forall (b:bv) (i:Z) (j:Z), ((j <= i)%Z /\
(0%Z <= j)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b
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
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)).
((i <= j)%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) (size - 1%Z)%Z 0%Z) = (to_nat_sub b
((size - 1%Z)%Z - s)%Z 0%Z)).
Axiom lsr_to_nat_sub : forall (b:bv) (s:Z), ((0%Z <= s)%Z /\
(s < size)%Z) -> ((to_nat_sub (lsr b s) (size - 1%Z)%Z
0%Z) = (to_nat_sub b ((size - 1%Z)%Z - s)%Z 0%Z)).
Parameter from_int: Z -> bv.
......@@ -316,12 +325,24 @@ Axiom nth_from_int_low_odd : forall (n:Z), (~ ((mod1 n 2%Z) = 0%Z)) ->
((nth (from_int n) 0%Z) = true).
(* YOU MAY EDIT THE CONTEXT BELOW *)
Open Scope Z_scope.
(* DO NOT EDIT BELOW *)
Theorem pow2i : forall (i:Z), (0%Z <= i)%Z -> ~ ((pow2 i) = 0%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intros i Hi.
cut (0 <= i); auto with zarith.
apply Z_lt_induction with
(P:= fun i =>
0 <= i -> pow2 i <> 0);auto with zarith.
intros x Hind Hxpos.
assert (hx:x = 0 \/ x >0) by omega.
destruct hx.
subst x.
rewrite Power_0;auto with zarith.
replace (x) with (x-1+1) by omega.
rewrite Power_s;auto with *.
Qed.
(* DO NOT EDIT BELOW *)
......
......@@ -154,6 +154,8 @@ Parameter size: Z.
Parameter bv : Type.
Axiom size_positive : (0%Z < size)%Z.
Parameter nth: bv -> Z -> bool.
......
......@@ -30,29 +30,16 @@ assert (h:(x = 0 \/ x > 0)) by omega.
destruct h.
subst x.
rewrite Power_0.
(*
auto with zarith.
elim n.
replace (0+m) with m by omega.
replace (1* pow2 m) with (pow2 m) by omega.
replace (n+0) with n by omega.
replace (pow2 n * 1) with (pow2 n) by omega.
auto.
intro.
elim p.
3:rewrite Power_1.
3:replace (1+m) with (m+1) by omega.
3:apply Power_s.
3:apply Hmn.
intros p0 Hp0.
rewrite Zpos_xI.
replace (2 * Zpos p0) with (Zpos p0 * 2) by omega.
rewrite<-Zplus_diag_eq_mult_2.
rewrite Power_s.
*)
replace (x) with ((x-1)+1) by omega.
rewrite Power_s;auto with zarith.
replace (n + (x-1+1)) with (n+(x-1)+1) by omega.
rewrite Power_s;auto with zarith.
rewrite Hind;auto with zarith.
rewrite Zmult_permute.
auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
......
......@@ -7,10 +7,9 @@ Parameter pow2: Z -> R.
Axiom Power_0 : ((pow2 0%Z) = 1%R).
Axiom Power_s : forall (n:Z), (0%Z <= n)%Z ->
((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R).
Axiom Power_s : forall (n:Z), ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R).
Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z ->
Axiom Power_p : forall (n:Z),
((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R).
Axiom Power_1 : ((pow2 1%Z) = 2%R).
......@@ -25,17 +24,31 @@ Theorem Power_sum : forall (n:Z) (m:Z),
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
intros n m.
elim n.
replace (0 + m) with m by omega.
assert (hm:m>=0 \/ m <=0) by omega.
destruct hm.
cut (0 <= m); auto with zarith.
apply Z_lt_induction with
(P:= fun m =>
0 <= m ->pow2 (n + m) = (pow2 n * pow2 m)%R);
auto with zarith.
intros x Hind Hxpos.
assert (h:(x = 0 \/ x > 0)) by omega.
destruct h.
subst x.
rewrite Power_0.
rewrite Rmult_1_l.
replace (n+0) with n by omega.
rewrite Rmult_1_r.
auto.
intro.
elim p.
intros p0 Hp0.
3: replace (1+m) with (m+1) by omega.
3:rewrite Power_1.
3:apply Power_s.
replace (x) with ((x-1)+1) by omega.
rewrite Power_s;auto with zarith.
replace (n + (x-1+1)) with (n+(x-1)+1) by omega.
rewrite Power_s;auto with zarith.
rewrite Hind;auto with zarith.
rewrite <-Rmult_assoc.
rewrite <-Rmult_assoc.
rewrite Rmult_comm with (r1:=pow2 n)(r2:=2%R).
auto with zarith.
Qed.
......
......@@ -151,6 +151,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 +216,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.
......@@ -272,12 +274,13 @@ Axiom to_nat_of_one : forall (b:bv) (i:Z) (j:Z), ((i <= j)%Z /\
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)).
((i <= j)%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.
......@@ -323,8 +326,49 @@ Axiom pow2i : forall (i:Z), (0%Z <= i)%Z -> ~ ((pow2 i) = 0%Z).
Axiom nth_from_int_0 : forall (i:Z), ((i < 32%Z)%Z /\ (0%Z <= i)%Z) ->
((nth (from_int 0%Z) i) = false).
Parameter from_int2c: Z -> bv.
Axiom size_from_int2c : (0%Z < (32%Z - 1%Z)%Z)%Z.
Axiom nth_sign_positive : forall (n:Z), (0%Z <= n)%Z -> ((nth (from_int2c n)
(32%Z - 1%Z)%Z) = 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) /\
((mod1 (div n (pow2 i)) 2%Z) = 0%Z))) -> ((nth (from_int2c n) i) = false).
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) /\ ~ ((mod1 (div n (pow2 i))
2%Z) = 0%Z))) -> ((nth (from_int2c n) i) = true).
Axiom nth_from_int2c_low_even_positive : forall (n:Z), ((0%Z <= n)%Z /\
((mod1 n 2%Z) = 0%Z)) -> ((nth (from_int2c n) 0%Z) = false).
Axiom nth_from_int2c_low_odd_positive : forall (n:Z), ((0%Z <= n)%Z /\
~ ((mod1 n 2%Z) = 0%Z)) -> ((nth (from_int2c n) 0%Z) = true).
Axiom nth_sign_negative : forall (n:Z), (0%Z <= n)%Z -> ((nth (from_int2c n)
(32%Z - 1%Z)%Z) = true).
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) /\
((mod1 (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) /\ ~ ((mod1 (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 /\
((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 /\
~ ((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 +435,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.
......@@ -449,12 +493,13 @@ Axiom to_nat_of_one1 : forall (b:bv1) (i:Z) (j:Z), ((i <= j)%Z /\
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)).
((i <= j)%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.
......@@ -478,6 +523,48 @@ 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) /\
((mod1 (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) /\
~ ((mod1 (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 /\
((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 /\
~ ((mod1 n 2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n) 0%Z) = true).
Axiom nth_sign_negative1 : forall (n:Z), (0%Z <= n)%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) /\
((mod1 (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) /\
~ ((mod1 (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 /\
((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 /\
~ ((mod1 n 2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n) 0%Z) = false).
Parameter concat: bv -> bv -> bv1.
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
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