Commit 46c24d68 authored by Nguyen Thi Minh Tuyen's avatar Nguyen Thi Minh Tuyen
Browse files

add *.v files

parent 22e8a735
......@@ -341,10 +341,12 @@ theory BitVector
function to_nat (b:bv) : int = to_nat_sub b (size-1) 0
(* this lemma is for TestBv32*)
(*false::: lemma lsr_to_nat_sub:
forall b:bv, n s:int.
0 <= s <size -> to_nat_sub (lsr b s) (size -1) 0 = to_nat_sub b (size-1-s) 0*)
lemma lsr_to_nat_sub:
forall b:bv, n s:int.
0 <= s <size -> to_nat_sub (lsr b s) (size -1) 0 = to_nat_sub b (size-1-s) 0
0 <= s <size -> to_nat_sub (lsr b s) (size -1) 0 = to_nat_sub b (size-1) s
(* 2-complement version *)
......@@ -436,10 +438,12 @@ theory BitVector
axiom nth_sign_positive:
forall n :int. n>=0 -> nth (from_int2c n) (size-1) = False
axiom nth_from_int2c_high_even_positive:
forall n i:int. n>=0 /\ size-1 > i >= 0 /\ mod (div n (pow2 i)) 2 = 0 -> nth (from_int2c n) i = False
forall n i:int. n>=0 /\ size-1 > i >= 0 /\ mod (div n (pow2 i)) 2 = 0
-> nth (from_int2c n) i = False
axiom nth_from_int2c_high_odd_positive:
forall n i:int. n>=0 /\size-1 > i >= 0 /\ mod (div n (pow2 i)) 2 <> 0 -> nth (from_int2c n) i = True
forall n i:int. n>=0 /\size-1 > i >= 0 /\ mod (div n (pow2 i)) 2 <> 0
-> nth (from_int2c n) i = True
lemma nth_from_int2c_low_even_positive:
forall n:int. n>=0 /\ mod n 2 = 0 -> nth (from_int2c n) 0 = False
......@@ -447,6 +451,9 @@ theory BitVector
lemma nth_from_int2c_low_odd_positive:
forall n:int. n>=0 /\ mod n 2 <> 0 -> nth (from_int2c n) 0 = True
lemma nth_from_int2c_0:
forall i:int. size > i >= 0 -> nth (from_int2c 0) i = False
(*********************************************************************)
(* axiom for n is negative *)
(*********************************************************************)
......@@ -655,6 +662,7 @@ theory TestDoubleOfInt
function j : BV32.bv = BV32.from_int 0x43300000
function j' : BV32.bv = BV32.from_int 0x80000000
lemma jp0_30: forall i:int. 0<=i<30 -> BV32.nth j' i = False
(*********************************************************************)
(* definitions: *)
......@@ -722,13 +730,32 @@ theory TestDoubleOfInt
(*********************************************************************)
predicate is_int32(x:int) = - Pow2int.pow2 31 <= x < Pow2int.pow2 31
lemma two_compl_pos: forall x:int. is_int32 x /\ x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = x
lemma two_compl_neg: forall x:int. is_int32 x /\ x < 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = Pow2int.pow2 32 + x
lemma nth_0_30: forall x:int. forall i:int. is_int32(x) /\ 0<=i<=30 ->
BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) i = BV32.nth (BV32.from_int2c x) i
lemma to_nat_sub_0_30: forall x:int. is_int32(x) ->
(BV32.to_nat_sub (BV32.bw_xor j' (BV32.from_int2c x)) 30 0) = (BV32.to_nat_sub (BV32.from_int2c x) 30 0)
lemma jpxorx_pos: forall x:int. x>=0 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = True
(*
lemma from_int2c_to_nat_sub31:
forall x:int. x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = x
*)
lemma from_int2c_to_nat_sub:
forall x:int. is_int32(x) /\ x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 30 0 = x
lemma nth_var31:
forall x:int. (BV32.nth (jpxor x) 31) = notb (BV32.nth (BV32.from_int2c x) 31)
lemma lemma1_pos : forall x:int. is_int32 x /\ x >= 0 -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x
lemma to_nat_sub_0_30_neg: forall x:int. is_int32(x) /\ x<0 ->
(BV32.to_nat_sub (BV32.bw_xor j' (BV32.from_int2c x)) 30 0) = (BV32.to_nat_sub (BV32.from_int2c x) 30 0)
lemma to_nat_sub_0_30_neg1: forall x:int. is_int32(x) /\ x<0 ->
(BV32.to_nat_sub (BV32.from_int2c x) 30 0) = Pow2int.pow2 31 + x
lemma lemma1_neg : forall x:int. is_int32 x /\ x < 0 -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x
lemma lemma1 : forall x:int. is_int32 x -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x
......@@ -738,15 +765,13 @@ theory TestDoubleOfInt
(* lemma 2: for all integer x, mantissa(var(x)) = 2^31 + x *)
(*********************************************************************)
lemma nth_var1: forall x:BV32.bv, j:int. 0 <= j <31 ->
(BV32.nth (BV32.bw_xor j' x) j) = (BV32.nth x j)
lemma nth_var11: forall x:int, j:int. 0 <= j <31 ->
(BV64.nth (var x) j) = (BV32.nth (BV32.from_int2c x) j)
lemma nth_var2:
forall x:int. (BV64.nth (var x) 31) = notb (BV32.nth (BV32.from_int2c x) 31)
lemma nth_var_0_31: forall x:int. forall i:int. is_int32(x) /\ 0<=i<=31->
BV64.nth (var x) i = BV32.nth (jpxor x) i
lemma to_nat_bv32_bv64_aux: forall b1:BV32.bv. forall b2:BV32.bv. forall j:int. 0<=j<32-> BV64.to_nat_sub (BV32_64.concat b1 b2) j 0 = BV32.to_nat_sub b2 j 0
lemma to_nat_bv32_bv64: forall b1:BV32.bv. forall b2:BV32.bv. BV64.to_nat_sub (BV32_64.concat b1 b2) 31 0 = BV32.to_nat_sub b2 31 0
lemma to_nat_var_0_31: forall x:int. is_int32(x) ->
BV64.to_nat_sub (var x) 31 0 = BV32.to_nat_sub (jpxor x) 31 0
lemma nth_var32to63:
forall x k:int. 32 <= k <= 63 -> BV64.nth (var x) k = BV32.nth j (k - 32)
......@@ -777,102 +802,39 @@ theory TestDoubleOfInt
(*********************************************************************)
(* lemma 5: for all integer x, var_as_double(x) = 2^52 + 2^31 + x *)
(*********************************************************************)
lemma lemma5: forall x:int. is_int32 x -> var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 31 +. (from_int x)
(*********************************************************************)
(* main result *)
(*********************************************************************)
function double_of_int32 (x:int) : real = var_as_double(x) -. const_as_double
lemma MainResult: forall x:int. is_int32 x -> double_of_int32 x = from_int x
(****************************************************)
(* dans ce qui suit, reprendre les bouts necessaires et les mettre au-dessus *)
lemma sign_var: forall x:int. sign(var(x)) = False
lemma exp_var: forall x:int. exp(var(x)) = 1075
lemma to_nat_sub_same: forall i:BV64.bv. forall j:BV32.bv. forall m:int.
(forall k:int. 0<=k<=m -> BV64.nth i k = BV32.nth j k) ->
BV64.to_nat_sub i m 0 = BV32.to_nat_sub j m 0
lemma nat_to_sub_x: forall x:int.
BV64.to_nat_sub (var x) 30 0 = BV32.to_nat_sub (BV32.from_int2c x) 30 0
lemma to_nat_sub_var:
forall x:int. BV64.to_nat_sub (var x) 30 0 = BV32.to_nat_sub (BV32.from_int2c x) 30 0
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 x_negative:forall x:int. (BV32.nth (BV32.from_int2c x) 31) = True ->
BV32.to_nat_sub (BV32.from_int2c x) 31 0 = Pow2int.pow2 31 + 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 from_int2c_to_nat_sub_neg:
forall x:int. x < 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = Pow2int.pow2 31 + 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 ->
BV64.to_nat_sub (var x) 30 0 = x
lemma mantissa_var_x_positive:
forall x:int. (BV64.nth (var x) 31) = True ->
mantissa(var(x)) = Pow2int.pow2 31 + x
lemma x_negative1: forall x:int. (BV32.nth (BV32.from_int2c x) 31) = True ->
BV32.to_nat_sub (BV32.from_int2c x) 30 0 = Pow2int.pow2 31 + x
lemma x_negative2: forall x:int. (BV64.nth (var x) 31) = False ->
BV64.to_nat_sub (var x) 30 0 = Pow2int.pow2 31 + x
lemma mantissa_var_x_negative:
forall x:int. (BV64.nth (var x) 31) = False ->
mantissa(var(x)) = Pow2int.pow2 31 + x
lemma mantissa_var: forall x:int. mantissa(var(x)) = Pow2int.pow2 31 + x
(*proved by Coq*)
lemma var_value0: forall x:int. var_as_double(x) =
(*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.
lemma from_int_sum : forall x:int. is_int32(x)->
from_int (Pow2int.pow2 31 + x) = from_int (Pow2int.pow2 31) +. from_int x
lemma var_value3: forall x:int. var_as_double(x) =
lemma var_value3: forall x:int. is_int32(x)->var_as_double(x) =
Pow2real.pow2 52 +. Pow2real.pow2 52 *. (from_int (Pow2int.pow2 31) +. from_int x) *. Pow2real.pow2 (-52)
lemma distr_pow52 : forall x:real.
Pow2real.pow2 52 *. x *. Pow2real.pow2 (-52) = x
lemma var_value4: forall x:int. var_as_double(x) =
lemma var_value4: forall x:int. is_int32(x)->var_as_double(x) =
Pow2real.pow2 52 +. (from_int (Pow2int.pow2 31)) +. from_int x
lemma pow31 : from_int (Pow2int.pow2 31) = Pow2real.pow2 31
lemma var_value: forall x:int. var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 31 +. (from_int x)
lemma lemma5: forall x:int. is_int32(x)-> var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 31 +. (from_int x)
(*********************************************************************)
(* main result *)
(*********************************************************************)
function double_of_int32 (x:int) : real = var_as_double(x) -. const_as_double
lemma MainResult: forall x:int. is_int32 x -> double_of_int32 x = from_int x
end
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
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 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).
Parameter size: Z.
Parameter bv : Type.
Axiom size_positive : (0%Z < size)%Z.
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).
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) = (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) = (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) = (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) = (negb (nth v2 n))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
Open Scope Z_scope.
(* DO NOT EDIT BELOW *)
Theorem 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)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
rewrite Nth_bw_xor.
destruct H.
replace (nth v1 n) with false.
destruct (nth v2 n);auto.
destruct H.
auto.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -2,12 +2,6 @@
(* 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.
......@@ -154,6 +148,8 @@ Parameter size: Z.
Parameter bv : Type.
Axiom size_positive : (0%Z < size)%Z.
Parameter nth: bv -> Z -> bool.
......@@ -222,8 +218,8 @@ Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%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).
(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.
......@@ -250,33 +246,35 @@ Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
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) -> (((nth b j) = false) -> ((to_nat_sub b j i) = (to_nat_sub b
(j - 1%Z)%Z i))).
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) -> (((nth b j) = true) -> ((to_nat_sub b j
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), ((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_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), ((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_zero : 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 i) = 0%Z)).
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
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)).
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)).
((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))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
Open Scope Z_scope.
......@@ -284,15 +282,24 @@ Open Scope Z_scope.
Theorem 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)).
0%Z) = (to_nat_sub b (size - 1%Z)%Z s)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
rewrite to_nat_of_zero2 with (i:=s).
2: auto with *.
cut (0<=s<size);auto.
apply Z_lt_induction with
(P:= fun s=>0 <= s < size ->
to_nat_sub (lsr b s) (size - 1) 0 = to_nat_sub b (size - 1) s);auto with zarith.
intros x Hind Hx.
assert (h:x = 0 \/ x>0) by omega.
destruct h.
subst x.
apply to_nat_sub_footprint;auto with zarith.
intros.
rewrite lsr_nth_low;auto with zarith.
replace (k+0) with k by omega;auto.
(* x > 0 *)
replace x with (x-1+1) by omega.
Qed.
(* DO NOT EDIT BELOW *)
......
......@@ -2,12 +2,6 @@
(* 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.
......@@ -154,6 +148,8 @@ Parameter size: Z.
Parameter bv : Type.
Axiom size_positive : (0%Z < size)%Z.
Parameter nth: bv -> Z -> bool.
......@@ -217,13 +213,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 /\