bitvector1.why

tests/bitvector1.why

@@ -143,6 +143,7 @@ theory BitVector
       0 <= n < size -> 0 <= s ->
         n+s >= size -> nth (lsr b s) n = False
 
+
   (* arithmetic shift right *)
   function asr bv int : bv
 
@@ -192,7 +193,9 @@ theory BitVector
       i >= size ->
         to_nat_aux b i = 0
 
-  function to_nat (b:bv) : int = to_nat_aux b 0
+
+
+
 
   (* generalization : (to_nat_sub b j i) returns the non-negative number represented
      by b[j..i] *)
@@ -236,12 +239,12 @@ theory BitVector
       i > j ->
         to_nat_sub b j i = 0
 
-  lemma to_nat_sub_low_true :
+(*  lemma to_nat_sub_low_true :
     forall b:bv, j:int.nth b j = True -> to_nat_sub b j j = 1
 
   lemma to_nat_sub_low_false :
     forall b:bv, j:int.nth b j = False -> to_nat_sub b j j = 0
-
+*)
   lemma to_nat_of_zero:
     forall b:bv, i j:int.
       (forall k:int. j >= k >= i -> nth b k = False) ->
@@ -255,6 +258,21 @@ theory BitVector
   lemma to_nat_sub_footprint: forall b1 b2:bv, j i:int.
     (forall k:int. i <= k <= j -> nth b1 k = nth b2 k) ->
     to_nat_sub b1 j i = to_nat_sub b2 j i
+(*
+  lemma to_nat_sub_of_zero_ij:
+    forall b:bv, i j:int.
+      (forall k:int. j >= k >= i -> nth b k = False) ->
+      to_nat_sub b j i = 0
+*)
+
+(*  function to_nat (b:bv) : int = to_nat_aux b 0*)
+  function to_nat (b:bv) : int = to_nat_sub b (size-1) 0
+
+(* this lemma is for TestBv32*)
+  lemma lsr_to_nat_sub:
+    forall b:bv, n s:int.
+      0 <= s -> to_nat_sub (lsr b s) (size -1) 0 = to_nat_sub b (size-1-s) 0
+
 
   (* 2-complement version *)
 
@@ -281,7 +299,14 @@ theory BitVector
   axiom to_int_aux_neg :
     forall b:bv. nth b (size-1) = True ->
          to_int_aux b (size-1) = -1
-
+  lemma to_int_zero:
+    forall b:bv. (forall i:int. 0 <= i <size-1-> nth b i = False) 
+                  -> to_int_aux b 0 = 0
+  lemma to_int_one:
+    forall b:bv. (forall i:int. 0 <= i <size-> nth b i = True) 
+                  -> to_int_aux b 0 = -1
+
+ 
   function to_int (b:bv) : int = to_int_aux b 0
 
   (* (from_uint n) returns the bitvector representing the non-negative
@@ -333,10 +358,10 @@ theory TestNatSub
 
   use import BV64
 
+
   function b:bv = from_int 7
 
   lemma to_nat_sub_b: (to_nat_sub b 4 0) = 7
-
 end
 
 theory BV32_64
@@ -489,6 +514,7 @@ theory TestDoubleOfInt
   use import real.RealInfix
   use import real.FromInt
   use import real.Power
+  use import int.Int
 
   function j : BV32.bv = BV32.from_int 0x43300000
 
@@ -497,7 +523,21 @@ theory TestDoubleOfInt
   function const : BV64.bv = BV32_64.concat j j'
 
   lemma sign_const: sign(const) = False
+     
+
   lemma exp_const: exp(const) = 1075
+  
+  lemma mantissa_const_nth:
+    forall i:int. 0 <=i <=30 -> BV64.nth const i = False
+  lemma mantissa_const_31th:
+    BV64.nth const 31 = True
+
+  lemma to_nat_mantissa_1: (BV64.to_nat_sub const 30 0) = 0
+
+  lemma mantissa_const_to_nat:
+    BV64.to_nat_sub const 31 0 = pow_of2 31 
+  lemma mantissa_const_to_nat51:
+    BV64.to_nat_sub const 51 0 = BV64.to_nat_sub const 31 0
   lemma mantissa_const: mantissa(const) = pow_of2 31
 
   function const_as_double : real = double_of_bv64 const
@@ -545,7 +585,7 @@ theory TestBv32
     to_nat bvzero = 0
 
   goal to_nat_0x0000000F:
-    to_nat (lsr bvone 28) = 15
+    to_nat (lsr bvone 28) = 15  
 
   goal to_nat_0x0000001F:
     to_nat (lsr bvone 27) = 31