(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* 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/Util.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.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* 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.
    let padding ≝ replicate bool m false in
      append bool m n padding b.
      
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* 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 (exclusive_disjunction) b c.
    
interpretation "BitVector exclusive disjunction"
  'exclusive_disjunction b c = (exclusive_disjunction ? 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_bv ≝
  λn: nat.
  λb, c: BitVector n.
    eq_v bool n (λd, e.
      if (d ∧ e) ∨ ((¬d) ∧ (¬e)) then
        true
      else
        false) b c.

lemma eq_bv_elim: ∀P:bool → Prop. ∀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.
    
axiom bitvector_of_string:
  ∀n: nat.
  ∀s: String.
    BitVector n.
    
axiom string_of_bitvector:
  ∀n: nat.
  ∀b: BitVector n.
    String.