(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
(*               Most functions are specialised versions of those found in    *)
(*               Vector.ma as a courtesy, or Boolean functions lifted into    *)
(*               BitVector variants.                                          *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

include "Universes.ma".

include "Vector.ma".
include "List.ma".
include "Nat.ma".
include "Bool.ma".

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Common synonyms.                                                           *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

ndefinition BitVector ≝ λn: Nat. Vector Bool n.
ndefinition Bit ≝ Bool.
ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Lookup.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

ndefinition get_index_bv ≝
  λn: Nat.
  λb: BitVector n.
  λm: Nat.
  λp: m < n.
    get_index Bool n b m p.
    
interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
    
ndefinition set_index_bv ≝
  λn: Nat.
  λb: BitVector n.
  λm: Nat.
  λp: m < n.
  λc: Bool.
    set_index Bool n b m c.
    
ndefinition drop ≝
  λn: Nat.
  λb: BitVector n.
  λm: Nat.
    drop Bool n b m.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Creating bitvectors from scratch.                                          *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

ndefinition zero ≝
  λn: Nat.
    ((replicate Bool n false): BitVector n).
    
ndefinition max ≝
  λn: Nat.
    ((replicate Bool n true): BitVector n).
    
ndefinition append ≝
  λm, n: Nat.
  λb: BitVector m.
  λc: BitVector n.
    append Bool m n b c.
    
ndefinition pad ≝
  λm, n: Nat.
  λb: BitVector n.
    let padding ≝ replicate Bool m false in
      append Bool m n padding b.
      
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Other manipulations.                                                       *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

ndefinition reverse ≝
  λn: Nat.
  λb: BitVector n.
    reverse Bool n b.

ndefinition length ≝
  λn: Nat.
  λb: BitVector n.
    length Bool n b.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Logical operations.                                                        *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
ndefinition conjunction ≝
  λn: Nat.
  λb: BitVector n.
  λc: BitVector n.
    zip_with Bool Bool Bool n conjunction b c.
    
interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).
   
ndefinition inclusive_disjunction ≝
  λn: Nat.
  λb: BitVector n.
  λc: BitVector n.
    zip_with Bool Bool Bool n inclusive_disjunction b c.
    
interpretation "BitVector inclusive disjunction"
  'inclusive_disjunction b c = (inclusive_disjunction ? b c).
         
ndefinition exclusive_disjunction ≝
  λn: Nat.
  λb: BitVector n.
  λc: BitVector n.
    zip_with Bool Bool Bool n exclusive_disjunction b c.
    
interpretation "BitVector exclusive disjunction"
  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
    
ndefinition negation_bv ≝
  λn: Nat.
  λb: BitVector n.
    map Bool Bool n (negation) b.
    
interpretation "BitVector negation" 'negation b c = (negation ? b c).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Rotates and shifts.                                                        *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

ndefinition rotate_left_bv ≝
  λn, m: Nat.
  λb: BitVector n.
    rotate_left Bool n m b.

ndefinition rotate_right_bv ≝
  λn, m: Nat.
  λb: BitVector n.
    rotate_right Bool n m b.
    
ndefinition shift_left_bv ≝
  λn, m: Nat.
  λb: BitVector n.
  λc: Bool.
    shift_left Bool n m b c.
    
ndefinition shift_right_bv ≝
  λn, m: Nat.
  λb: BitVector n.
  λc: Bool.
    shift_right Bool n m b c.
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Conversions to and from lists and natural numbers.                         *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

ndefinition list_of_bitvector ≝
  λn: Nat.
  λb: BitVector n.
    list_of_vector Bool n b.
    
ndefinition bitvector_of_list ≝
  λl: List Bool.
    vector_of_list Bool l.

nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
  let divrem ≝ divide_with_remainder n (S (S Z)) in
  let div ≝ first Nat Nat divrem in
  let rem ≝ second Nat Nat divrem in
    match div with
      [ Z ⇒
        match rem with
          [ Z ⇒ Empty Bool
          | S r ⇒ ? (true :: (bitvector_of_nat_aux Z))
          ]
      | S d ⇒
        match rem with
          [ Z ⇒ ? (false :: (bitvector_of_nat_aux (S d)))
          | S r ⇒ ? (true :: (bitvector_of_nat_aux (S d)))
          ]
      ].
      //.
nqed.

ndefinition eq_bv ≝
  λn: Nat.
  λb, c: BitVector n.
    eq_v Bool n (λd, e.
      if inclusive_disjunction (conjunction d e) (conjunction (negation d)
                                                              (negation e)) then
        true
      else
        false) b c.

nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
  let biglist ≝ reverse ? (bitvector_of_nat_aux m) in
  let size ≝ length ? biglist in
  let bitvector ≝ bitvector_of_list biglist in
  let difference ≝ n - size in
    match greater_than_b size n with
      [ true ⇒ max n
      | false ⇒ ? (pad difference size bitvector)
      ].
      nnormalize.
      nrewrite > (plus_minus_inverse_right n ?).
      #H.
      nassumption.
nqed.

nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
  match b with
    [ Empty ⇒ Z
    | Cons o hd tl ⇒
      let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    ].
    
naxiom full_add:
  ∀n: Nat.
  ∀b, c: BitVector n.
  ∀d: Bit.
    Bool × (BitVector n).
    
ndefinition half_add ≝
  λn: Nat.
  λb, c: BitVector n.
    full_add n b c false.