(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* 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 "arithmetics/nat.ma".

include "ASM/FoldStuff.ma".
include "ASM/Vector.ma".
include "ASM/String.ma".

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

definition BitVector ≝ λn: nat. Vector bool n.
definition Bit ≝ bool.
definition Nibble ≝ BitVector 4.
definition Byte7 ≝ BitVector 7.
definition Byte ≝ BitVector 8.
definition Word ≝ BitVector 16.
definition Word11 ≝ BitVector 11.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Inversion                                                                  *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
 #v lapply (refl … 0) cases v in ⊢ (??%? → ?%%??); //
 #n #hd #tl #abs @⊥ destruct (abs)
qed.

lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
 ∃hd.∃tl.v ≃ VCons bool n hd tl.
 #n #v lapply (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
 [ #abs @⊥ destruct (abs)
 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
qed.

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

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

definition zero: ∀n:nat. BitVector n ≝
  λn: nat. replicate bool n false.
    
definition maximum: ∀n:nat. BitVector n ≝
  λn: nat. replicate bool n true.
  
definition pad ≝
  λm, n: nat.
  λb: BitVector n. pad_vector ? false m n b.

(* jpb: we already have bitvector_of_nat and friends in the library, maybe
 * we should unify this in some way *)  
let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝
  match n with
  [ O ⇒ VEmpty ?
  | S n' ⇒
    eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2)
  ].
  
let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝
  match b with
  [ VEmpty ⇒ 0
  | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Other manipulations.                                                       *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Logical operations.                                                        *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
  λn: nat.
  λb: BitVector n.
  λc: BitVector n.
    zip_with ? ? ? n (andb) b c.
    
interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
   
definition inclusive_disjunction_bv ≝
  λn: nat.
  λb: BitVector n.
  λc: BitVector n.
    zip_with ? ? ? n (orb) b c.
    
interpretation "BitVector inclusive disjunction"
  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
         
definition exclusive_disjunction_bv ≝
  λn: nat.
  λb: BitVector n.
  λc: BitVector n.
    zip_with ? ? ? n xorb b c.
    
interpretation "BitVector exclusive disjunction"
  'exclusive_disjunction b c = (xorb b c).
    
definition negation_bv ≝
  λn: nat.
  λb: BitVector n.
    map bool bool n (notb) b.
    
interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Rotates and shifts.                                                        *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Conversions to and from lists and natural numbers.                         *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

definition eq_b ≝
  λb, c: bool.
    if b then
      c
    else
      notb c.

lemma eq_b_eq:
  ∀b, c.
    eq_b b c = true → b = c.
  #b #c
  cases b
  cases c
  normalize //
qed.

definition eq_bv ≝
  λn: nat.
  λb, c: BitVector n.
    eq_v bool n eq_b b c.

lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
  (x = y → P true) →
  (x ≠ y → P false) →
  P (eq_bv n x y).
#P #n #x #y #Ht #Hf whd in ⊢ (?%); @(eq_v_elim … Ht Hf)
#Q * *; normalize /3/
qed.

lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
@eq_v_true * @refl
qed.

lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
qed.

lemma eq_bv_refl:
  ∀n,v. eq_bv n v v = true.
  #n #v
  elim v
  [ //
  | #n #hd #tl #ih
    normalize
    cases hd
    [ normalize
      @ ih
    | normalize
      @ ih
    ]
  ]
qed.

lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
qed.

lemma eq_eq_bv:
  ∀n, v, q.
    v = q → eq_bv n v q = true.
  #n #v
  elim v
  [ #q #h <h normalize %
  | #n #hd #tl #ih #q #h >h //
  ]
qed.

lemma eq_bv_eq:
  ∀n, v, q.
    eq_bv n v q = true → v = q.
  #n #v #q generalize in match v;
  elim q
  [ #v #h @BitVector_O
  | #n #hd #tl #ih #v' #h
    cases (BitVector_Sn ? v')
    #hd' * #tl' #jmeq >jmeq in h;
    #new_h
    change with ((andb ? ?) = ?) in new_h;
    cases(conjunction_true … new_h)
    #eq_heads #eq_tails
    whd in eq_heads:(??(??(%))?);
    cases(eq_b_eq … eq_heads)
    whd in eq_tails:(??(?????(%))?);
    change with (eq_bv ??? = ?) in eq_tails;
    <(ih tl') //
  ]
qed.

corollary refl_iff_eq_bv_true:
  ∀n: nat.
  ∀x: BitVector n.
  ∀y: BitVector n.
    eq_bv n x y = true ↔ x = y.
  #n #x #y whd in match iff; normalize nodelta
  @conj /2/
qed.

axiom bitvector_of_string:
  ∀n: nat.
  ∀s: String.
    BitVector n.
    
axiom string_of_bitvector:
  ∀n: nat.
  ∀b: BitVector n.
    String.