include "utilities/binary/Z.ma".
include "ASM/BitVector.ma".
include "ASM/Arithmetic.ma".

let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝
match bv with
[ VEmpty ⇒ OZ
| VCons n' h t ⇒
    if h then pos (fold_left ??? (λacc,b.if b then (p1 acc) else (p0 acc)) one t)
         else (Z_of_unsigned_bitvector ? t)
].

definition Z_of_signed_bitvector ≝
λn.λbv:BitVector n.
match bv with
[ VEmpty ⇒ OZ
| VCons n' h t ⇒
    if h then - (Zsucc (Z_of_unsigned_bitvector ? (negation_bv ? t)))
         else (Z_of_unsigned_bitvector n' t)
].

(* Reverses, so LSB first. *)
let rec bits_of_pos (p:Pos) : list bool ≝
match p with
[ one ⇒ [true]
| p0 p' ⇒ false::(bits_of_pos p')
| p1 p' ⇒  true::(bits_of_pos p')
].

let rec zeroext_reversed (n:nat) (m:nat) (bv:BitVector n) on m : BitVector m ≝
match m with
[ O ⇒ [[ ]]
| S m' ⇒
    match bv with
    [ VEmpty ⇒ zero (S m')
    | VCons n' h t ⇒ VCons ? m' h (zeroext_reversed n' m' t)
    ]
].

let rec bitvector_of_Z (n:nat) (z:Z) on z : BitVector n ≝
match z with
[ OZ ⇒ zero n
| pos p ⇒
  let bits ≝ bits_of_pos p in
  reverse ?? (zeroext_reversed ? n (vector_of_list … bits))
| neg p ⇒
  match p with
  [ one ⇒ maximum ?
  | _ ⇒ 
    let bits ≝ bits_of_pos (pred p) in
    let pz ≝ reverse ?? (zeroext_reversed ? n (vector_of_list … bits)) in
    negation_bv ? pz
  ]
].

theorem bv_Z_unsigned_min : ∀n. ∀bv:BitVector n. OZ ≤ Z_of_unsigned_bitvector n bv.
#n #bv elim bv
[ //
| #m * #t #IH whd in ⊢ (??%) //
] qed.

(* Use bit counting to show the max *)

let rec pos_length (p:Pos) : nat ≝
match p with
[ one ⇒ O
| p0 q ⇒ S (pos_length q)
| p1 q ⇒ S (pos_length q)
].

lemma pos_length_lt: ∀p,q. pos_length p < pos_length q → p < q.
#p elim p
[ * [ normalize #H elim (absurd ? H (not_le_Sn_n 0))
    | #q #_ @(lt_one_S (p0 q))
    | #q #_ >p0_times2 /2/
    ]
| #p' #IH
  * [ normalize #H elim (absurd ? H (not_le_Sn_O ?))
    | #q #H change with (one+ (p0 p') < one+(p0 q)) @monotonic_lt_plus_r
      >p0_times2 >(p0_times2 q)
      @monotonic_lt_times_r @IH
      @le_S_S_to_le @H
    | #q #H change with ((succ one)+ (p0 p') ≤ (p0 q))
      >p0_times2 >(p0_times2 q)
      @monotonic_le_times_r @IH
      @le_S_S_to_le @H
    ]
| #p' #IH
  * [ normalize #H elim (absurd ? H (not_le_Sn_O ?))
    | #q #H change with ((p0 p') < succ (p0 q)) @le_S
      >p0_times2 >(p0_times2 q)
      @monotonic_lt_times_r @IH
      @le_S_S_to_le @H
    | #q #H 
      >p0_times2 >(p0_times2 q)
      @monotonic_lt_times_r @IH
      @le_S_S_to_le @H
    ]
] qed.

lemma bvZ_length : ∀n.∀bv:BitVector n. match Z_of_unsigned_bitvector n bv with
[ OZ ⇒ True | pos p ⇒ pos_length p < n | neg p ⇒ False ].
#n #bv elim bv
[ @I
| #m *
[ 2: #tl normalize cases (Z_of_unsigned_bitvector m tl) normalize /2/ 
| #tl #_ normalize @le_S_S
  change with (? ≤ pos_length one + m)
  generalize in ⊢ (?(?(?????%?))(?(?%)?)) elim tl
  [ // | #o * #t normalize #IH #p <plus_n_Sm
    change with (? ≤ pos_length (p1 p) + o)
    @IH
  ]
] qed.

lemma two_power_length : ∀n. pos_length (two_power_nat n) = n.
#n elim n
[ @refl
| #m #IH normalize > IH @refl
] qed.

theorem bv_Z_unsigned_max : ∀n. ∀bv:BitVector n. Z_of_unsigned_bitvector n bv < Z_two_power_nat n.
#n #bv normalize
lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2/
qed.

lemma Zopp_le: ∀x,y. x ≤ y → -y ≤ -x.
* [ 2,3: #p ] * [ 2,3: #q ] //
qed.

theorem bv_Z_signed_min : ∀n. ∀bv:BitVector n. - Z_two_power_nat n ≤ Z_of_signed_bitvector n bv.
#n *
[ //
| #m *
  [ #bv @Zopp_le @(transitive_Zle … (Z_two_power_nat m))
    [ @Zlt_to_Zle @bv_Z_unsigned_max
    | normalize //
    ]
  | #bv @(transitive_Zle … 0) //
  ]
] qed.

theorem bv_Z_signed_max : ∀n. ∀bv:BitVector (S n). Z_of_signed_bitvector (S n) bv < Z_two_power_nat n.
#n #bv @(vector_inv_n ? (S n) ? bv) *
[ #t whd in ⊢ (?%%) lapply (bv_Z_unsigned_min … (negation_bv n t))
  cases (Z_of_unsigned_bitvector n (negation_bv n t)) //
  #p *
| #t whd in ⊢ (?%?) //
] qed.