theory BitVector

  use export bool.Bool
  use int.Int
  use power2.Pow2int

  function size : int
  (* size at least 2 since we need 2-complement representation *)
  axiom size_positive: size > 1

  type bv

  function nth bv int: bool

  function bvzero : bv
  axiom Nth_zero:
    forall n:int. 0 <= n < size -> nth bvzero n = False

  function bvone : bv
  axiom Nth_one:
    forall n:int. 0 <= n < size -> nth bvone n = True

  predicate eq (v1 v2 : bv) =
    forall n:int. 0 <= n < size -> nth v1 n = nth v2 n

  axiom extensionality:
    forall v1 v2 : bv. eq v1 v2 -> v1 = v2

  function bw_and (v1 v2 : bv) : bv
  axiom Nth_bw_and:
    forall v1 v2:bv, n:int. 0 <= n < size ->
      nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n)

  function bw_or (v1 v2 : bv) : bv
  axiom Nth_bw_or:
    forall v1 v2:bv, n:int. 0 <= n < size ->
      nth (bw_or v1 v2) n = orb (nth v1 n) (nth v2 n)

  function bw_xor (v1 v2 : bv) : bv
  axiom Nth_bw_xor:
    forall v1 v2:bv, n:int. 0 <= n < size ->
      nth (bw_xor v1 v2) n = xorb (nth v1 n) (nth v2 n)

  lemma Nth_bw_xor_v1true:
    forall v1 v2:bv, n:int. 0 <= n < size /\ nth v1 n = True ->
      nth (bw_xor v1 v2) n = notb (nth v2 n)

  lemma Nth_bw_xor_v1false:
    forall v1 v2:bv, n:int. 0 <= n < size /\ nth v1 n = False->
      nth (bw_xor v1 v2) n = nth v2 n

  lemma Nth_bw_xor_v2true:
    forall v1 v2:bv, n:int. 0 <= n < size /\ nth v2 n = True->
      nth (bw_xor v1 v2) n = notb (nth v1 n)

  lemma Nth_bw_xor_v2false:
    forall v1 v2:bv, n:int. 0 <= n < size /\ nth v2 n = False->
      nth (bw_xor v1 v2) n = nth v1 n

  function bw_not (v : bv) : bv
  axiom Nth_bw_not:
    forall v:bv, n:int. 0 <= n < size ->
      nth (bw_not v) n = notb (nth v n)

  (* logical shift right *)
  function lsr bv int : bv
(*
  axiom lsr_nth_low:
    forall b:bv, n s:int.
      0 <= n < size -> 0 <= s ->
        n+s < size -> nth (lsr b s) n = nth b (n+s)

  axiom lsr_nth_high:
    forall b:bv, n s:int.
      0 <= n < size -> 0 <= s ->
        n+s >= size -> nth (lsr b s) n = False
*)
  axiom lsr_nth_low:
    forall b:bv, n s:int.
      0 <= n < size /\ 0 <= s<size /\
        n+s < size -> nth (lsr b s) n = nth b (n+s)

  axiom lsr_nth_high:
    forall b:bv, n s:int.
      0 <= n < size /\ 0 <= s<size /\
        n+s >= size -> nth (lsr b s) n = False

  (* arithmetic shift right *)
  function asr bv int : bv

  axiom asr_nth_low:
    forall b:bv, n s:int.
      0 <= n < size -> 0 <= s ->
        n+s < size -> nth (asr b s) n = nth b (n+s)

  axiom asr_nth_high:
    forall b:bv, n s:int.
      0 <= n < size -> 0 <= s ->
        n+s >= size -> nth (asr b s) n = nth b (size-1)

  (* logical shift left *)
  function lsl bv int : bv

  axiom lsl_nth_high:
    forall b:bv, n s:int.
      0 <= n < size -> 0 <= s ->
        0 <= n-s -> nth (lsl b s) n = nth b (n-s)

  axiom lsl_nth_low:
    forall b:bv, n s:int.
      0 <= n < size -> 0 <= s ->
        0 > n-s -> nth (lsl b s) n = False

  (* conversion to/from integers *)

(*

  function to_nat_aux bv int : int
    (* (to_nat_aux b i) returns the non-negative integer whose
       binary repr is b[size-1..i] *)

  axiom to_nat_aux_zero :
    forall b:bv, i:int.
      0 <= i < size ->
        nth b i = False ->
          to_nat_aux b i = 2 * to_nat_aux b (i+1)

  axiom to_nat_aux_one :
    forall b:bv, i:int.
      0 <= i < size ->
        nth b i = True ->
          to_nat_aux b i = 1 + 2 * to_nat_aux b (i+1)

  axiom to_nat_aux_high :
    forall b:bv, i:int.
      i >= size ->
        to_nat_aux b i = 0


*)


  (* generalization : (to_nat_sub b j i) returns the non-negative number represented
     by b[j..i] *)

 function to_nat_sub bv int int : int
    (* (to_nat_sub b j i) returns the non-negative integer whose
       binary repr is b[j..i] *)

(*  axiom to_nat_sub_zero :
    forall b:bv, j i:int.
      0 <= i <= j ->
        nth b i = False ->
          to_nat_sub b j i = 2 * to_nat_sub b j (i+1)

  axiom to_nat_sub_one :
    forall b:bv, j i:int.
      0 <= i <= j ->
        nth b i = True ->
          to_nat_sub b j i = 1 + 2 * to_nat_sub b j (i+1)

  axiom to_nat_sub_high :
    forall b:bv, j i:int.
      i > j ->
        to_nat_sub b j i = 0
*)

  axiom to_nat_sub_zero :
    forall b:bv, j i:int.
      0 <= i <= j < size ->
        nth b j = False ->
          to_nat_sub b j i = to_nat_sub b (j-1) i

  axiom to_nat_sub_one :
    forall b:bv, j i:int.
      0 <= i <= j < size ->
        nth b j = True ->
          to_nat_sub b j i = (pow2 (j-i)) + to_nat_sub b (j-1) i

  axiom to_nat_sub_high :
    forall b:bv, j i:int.
      i > j ->
        to_nat_sub b j i = 0

(*  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_zero2:
    forall b:bv, i j:int. size > j >= i >= 0 ->
      (forall k:int. j >= k > i -> nth b k = False) ->
      to_nat_sub b j 0 = to_nat_sub b i 0


  lemma to_nat_of_zero:
    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

  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) ->
    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*)
(*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
*)

  (* 2-complement version *)

(*

  function to_int_aux bv int : int
    (* (to_int_aux b i) returns the integer whose
       2-complement binary repr is b[size-1..i] *)

  axiom to_int_aux_zero :
    forall b:bv, i:int.
      0 <= i < size-1 ->
        nth b i = False ->
          to_int_aux b i = 2 * to_int_aux b (i+1)

  axiom to_int_aux_one :
    forall b:bv, i:int.
      0 <= i < size-1 ->
        nth b i = True ->
          to_int_aux b i = 1 + 2 * to_int_aux b (i+1)

  axiom to_int_aux_pos :
    forall b:bv. nth b (size-1) = False ->
         to_int_aux b (size-1) = 0

  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
     integer n on size bits. *)
  function from_int (n:int) : bv

  use int.EuclideanDivision


(*  axiom nth_from_int_high:
     forall n i:int. size>i > 0 -> nth (from_int n) i = nth (from_int (div n 2)) (i-1)
*)


 (*Notice: replace 0 <= i <size by 0 <= i < size-1 because the bit at (size -1) is the sign of i*)
(* axiom from_int_sign_positive:
       forall n:int. n>=0 -> nth (from_int n) (size - 1) = False
 axiom from_int_sign_negative:
       forall n:int. n<0 -> nth (from_int n) (size - 1) = True
*)

  axiom nth_from_int_high_even:
     forall n i:int. size > i >= 0 /\ mod (div n (pow2 i)) 2 = 0 -> nth (from_int n) i = False

  axiom nth_from_int_high_odd:
     forall n i:int. size > i >= 0 /\ mod (div n (pow2 i)) 2 <> 0 -> nth (from_int n) i = True

  lemma nth_from_int_low_even:
    forall n:int. mod n 2 = 0 -> nth (from_int n) 0 = False

  lemma nth_from_int_low_odd:
    forall n:int. mod n 2 <> 0 -> nth (from_int n) 0 = True

  lemma nth_from_int_0:
     forall i:int. size > i >= 0 -> nth (from_int 0) i = False

(*********************************************************************)
(*from_int2c: int -> bv                                              *)
(*        Take an integer as input and returns a bv with 2-complement*)
(*        bit size-1:sign, false if n is non-negative, true otherwise*)
(*********************************************************************)
  function from_int2c (n:int) : bv

(*********************************************************************)
(* axiom for n is non-negative                                       *)
(*********************************************************************)

  axiom nth_sign_positive:
     forall n :int. n>=0 -> nth (from_int2c n) (size-1) = False

(*********************************************************************)
(* axiom for n is negative                                           *)
(*********************************************************************)

  axiom nth_sign_negative:
     forall n:int. n<0 -> nth (from_int2c n) (size-1) = True

(*********************************************************************)
(* axioms for any n                                          *)
(*********************************************************************)

  axiom nth_from_int2c_high_even:
     forall n i:int. size-1 > i >= 0 /\ mod (div n (pow2 i)) 2 = 0
                             -> nth (from_int2c n) i = False

  axiom nth_from_int2c_high_odd:
     forall n i:int. size-1 > i >= 0 /\ mod (div n (pow2 i)) 2 <> 0
                             -> nth (from_int2c n) i = True

  lemma nth_from_int2c_low_even:
    forall n:int. mod n 2 = 0 -> nth (from_int2c n) 0 = False

  lemma nth_from_int2c_low_odd:
    forall n:int. 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

  lemma nth_from_int2c_plus_pow2:
      forall x k i:int. 0 <= k < i /\ k < size-1 ->
        nth (from_int2c (x+pow2 i)) k = nth (from_int2c x) k

end


theory BV32

  function size : int = 32

  clone export BitVector with function size, lemma size_positive, axiom .

end


theory BV64

  function size : int = 64

  clone export BitVector with function size, lemma size_positive, axiom .

end

theory BV32_64

  use int.Int

  use BV32 as BV32
  use BV64 as BV64

  function concat BV32.bv BV32.bv : BV64.bv

  axiom concat_low: forall b1 b2:BV32.bv.
    forall i:int. 0 <= i < 32 -> BV64.nth (concat b1 b2) i = BV32.nth b2 i

  axiom concat_high: forall b1 b2:BV32.bv.
    forall i:int. 32 <= i < 64 -> BV64.nth (concat b1 b2) i = BV32.nth b1 (i-32)

end


theory TestBv32

  use BV32
  use int.Int

  goal Test1:
    let b = bw_and bvzero bvone in nth b 1 = False

  goal Test2:
    let b = lsr bvone 16 in nth b 15 = True

  goal Test3:
    let b = lsr bvone 16 in nth b 16 = False

  goal Test4:
    let b = asr bvone 16 in nth b 15 = True

  goal Test5:
    let b = asr bvone 16 in nth b 16 = True

  goal Test6:
    let b = asr (lsr bvone 1) 16 in nth b 16 = False

  goal to_nat_0x00000000:
    to_nat bvzero = 0

  goal to_nat_0x00000001:
    to_nat (lsr bvone 31) = 1

  goal to_nat_0x00000003:
    to_nat (lsr bvone 30) = 3

  goal to_nat_0x00000007:
    to_nat (lsr bvone 29) = 7

  goal to_nat_0x0000000F:
    to_nat (lsr bvone 28) = 15

  goal to_nat_0x0000001F:
    to_nat (lsr bvone 27) = 31

  goal to_nat_0x0000003F:
    to_nat (lsr bvone 26) = 63

  goal to_nat_0x0000007F:
    to_nat (lsr bvone 25) = 127

  goal to_nat_0x000000FF:
    to_nat (lsr bvone 24) = 255

  goal to_nat_0x000001FF:
    to_nat (lsr bvone 23) = 511

  goal to_nat_0x000003FF:
    to_nat (lsr bvone 22) = 1023

  goal to_nat_0x000007FF:
    to_nat (lsr bvone 21) = 2047

  goal to_nat_0x00000FFF:
    to_nat (lsr bvone 20) = 4095

  goal to_nat_0x00001FFF:
    to_nat (lsr bvone 19) = 8191

  goal to_nat_0x00003FFF:
    to_nat (lsr bvone 18) = 16383

  goal to_nat_0x00007FFF:
    to_nat (lsr bvone 17) = 32767

  goal to_nat_0x0000FFFF:
    to_nat (lsr bvone 16) = 65535

(*
  goal to_nat_smoke:
    to_nat (lsr bvone 16) = 65536
*)

  goal to_nat_0x0001FFFF:
    to_nat (lsr bvone 15) = 131071

  goal to_nat_0x0003FFFF:
    to_nat (lsr bvone 14) = 262143

  goal to_nat_0x0007FFFF:
    to_nat (lsr bvone 13) = 524287

  goal to_nat_0x000FFFFF:
    to_nat (lsr bvone 12) = 1048575

  goal to_nat_0x00FFFFFF:
    to_nat (lsr bvone 8) = 16777215

  goal to_nat_0xFFFFFFFF:
    to_nat bvone = 4294967295

(*
  goal to_int_0x00000000:
    to_int bvzero = 0

  goal to_int_0xFFFFFFFF:
    to_int bvone = -1

  goal to_int_0x7FFFFFFF:
    to_int (lsr bvone 1) = 2147483647

  goal to_int_0x80000000:
    to_int (lsl bvone 31) = -2147483648

  goal to_int_0x0000FFFF:
    to_int (lsr bvone 16) = 65535

  goal to_int_smoke:
    to_int (lsr bvone 16) = 65536

*)

end

(*
Local Variables:
compile-command: "why3 ide -L . bitvector.why"
End:
*)