weblib/Cerco/ASM/BitVector.ma

   1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
   2 (* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
   3 (*               Most functions are specialised versions of those found in    *)
   4 (*               Vector.ma as a courtesy, or boolean functions lifted into    *)
   5 (*               BitVector variants.                                          *)
   6 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
   7
   8 include "arithmetics/nat.ma".
   9
  10 include "ASM/FoldStuff.ma".
  11 include "ASM/Vector.ma".
  12 include "ASM/String.ma".
  13
  14 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  15 (* Common synonyms.                                                           *)
  16 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  17
  18 definition BitVector ≝ λn: nat. Vector bool n.
  19 definition Bit ≝ bool.
  20 definition Nibble ≝ BitVector 4.
  21 definition Byte7 ≝ BitVector 7.
  22 definition Byte ≝ BitVector 8.
  23 definition Word ≝ BitVector 16.
  24 definition Word11 ≝ BitVector 11.
  25
  26 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  27 (* Inversion                                                                  *)
  28 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  29
  30 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
  31  #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
  32  #n #hd #tl #abs @⊥ destruct (abs)
  33 qed.
  34
  35 lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
  36  ∃hd.∃tl.v ≃ VCons bool n hd tl.
  37  #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
  38  [ #abs @⊥ destruct (abs)
  39  | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
  40 qed.
  41
  42 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  43 (* Lookup.                                                                    *)
  44 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  45
  46 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  47 (* Creating bitvectors from scratch.                                          *)
  48 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  49
  50 definition zero: ∀n:nat. BitVector n ≝
  51   λn: nat. replicate bool n false.
  52
  53 definition maximum: ∀n:nat. BitVector n ≝
  54   λn: nat. replicate bool n true.
  55
  56 definition pad ≝
  57   λm, n: nat.
  58   λb: BitVector n. pad_vector ? false m n b.
  59
  60 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  61 (* Other manipulations.                                                       *)
  62 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  63
  64 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  65 (* Logical operations.                                                        *)
  66 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  67
  68 definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
  69   λn: nat.
  70   λb: BitVector n.
  71   λc: BitVector n.
  72     zip_with ? ? ? n (andb) b c.
  73
  74 interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
  75
  76 definition inclusive_disjunction_bv ≝
  77   λn: nat.
  78   λb: BitVector n.
  79   λc: BitVector n.
  80     zip_with ? ? ? n (orb) b c.
  81
  82 interpretation "BitVector inclusive disjunction"
  83   'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
  84
  85 definition exclusive_disjunction_bv ≝
  86   λn: nat.
  87   λb: BitVector n.
  88   λc: BitVector n.
  89     zip_with ? ? ? n (exclusive_disjunction) b c.
  90
  91 interpretation "BitVector exclusive disjunction"
  92   'exclusive_disjunction b c = (exclusive_disjunction ? b c).
  93
  94 definition negation_bv ≝
  95   λn: nat.
  96   λb: BitVector n.
  97     map bool bool n (notb) b.
  98
  99 interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
 100
 101 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 102 (* Rotates and shifts.                                                        *)
 103 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 104
 105 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 106 (* Conversions to and from lists and natural numbers.                         *)
 107 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 108
 109 definition eq_b ≝
 110   λb, c: bool.
 111     if b then
 112       c
 113     else
 114       notb c.
 115
 116 lemma eq_b_eq:
 117   ∀b, c.
 118     eq_b b c = true → b = c.
 119   #b #c
 120   cases b
 121   cases c
 122   normalize //
 123 qed.
 124
 125 definition eq_bv ≝
 126   λn: nat.
 127   λb, c: BitVector n.
 128     eq_v bool n eq_b b c.
 129
 130 lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
 131   (x = y → P true) →
 132   (x ≠ y → P false) →
 133   P (eq_bv n x y).
 134 #P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf)
 135 #Q * *; normalize /3/
 136 qed.
 137
 138 lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
 139 @eq_v_true * @refl
 140 qed.
 141
 142 lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
 143 #n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
 144 qed.
 145
 146 lemma eq_bv_refl:
 147   ∀n,v. eq_bv n v v = true.
 148   #n #v
 149   elim v
 150   [ //
 151   | #n #hd #tl #ih
 152     normalize
 153     cases hd
 154     [ normalize
 155       @ ih
 156     | normalize
 157       @ ih
 158     ]
 159   ]
 160 qed.
 161
 162 lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
 163  #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
 164 qed.
 165
 166 lemma eq_eq_bv:
 167   ∀n, v, q.
 168     v = q → eq_bv n v q = true.
 169   #n #v
 170   elim v
 171   [ #q #h \ 5h normalize="" %="" |="" #n="" #hd="" #tl="" #ih="" #q="" #h=""\ 6h //
 172   ]
 173 qed.
 174
 175 lemma eq_bv_eq:
 176   ∀n, v, q.
 177     eq_bv n v q = true → v = q.
 178   #n #v #q generalize in match v
 179   elim q
 180   [ #v #h @BitVector_O
 181   | #n #hd #tl #ih #v' #h
 182     cases (BitVector_Sn ? v')
 183     #hd' * #tl' #jmeq >jmeq in h;
 184     #new_h
 185     change in new_h with ((andb ? ?) = ?);
 186     cases(conjunction_true … new_h)
 187     #eq_heads #eq_tails
 188     whd in eq_heads:(??(??(%))?);
 189     cases(eq_b_eq … eq_heads)
 190     whd in eq_tails:(??(?????(%))?);
 191     change in eq_tails with (eq_bv ??? = ?);
 192     <(ih tl') //
 193   ]
 194 qed.
 195
 196 axiom bitvector_of_string:
 197   ∀n: nat.
 198   ∀s: String.
 199     BitVector n.
 200
 201 axiom string_of_bitvector:
 202   ∀n: nat.
 203   ∀b: BitVector n.
 204     String.
 205 \ 5/h\ 6