source: Deliverables/D4.1/Matita/BitVector.ma @ 343

Last change on this file since 343 was 343, checked in by mulligan, 9 years ago

Fixed Status.ma so that it compiles.

File size: 6.8 KB
RevLine 
[236]1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
[240]3(*               Most functions are specialised versions of those found in    *)
4(*               Vector.ma as a courtesy, or Boolean functions lifted into    *)
5(*               BitVector variants.                                          *)
[236]6(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
7
[246]8include "Universes.ma".
[224]9
[246]10include "Vector.ma".
11include "List.ma".
12include "Nat.ma".
13include "Bool.ma".
[240]14
[236]15(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
16(* Common synonyms.                                                           *)
17(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
18
[228]19ndefinition BitVector ≝ λn: Nat. Vector Bool n.
[263]20ndefinition Bit ≝ Bool.
[230]21ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
22ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
23ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
24ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
[271]25ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))).
[224]26
[236]27(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[240]28(* Lookup.                                                                    *)
29(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
30
[337]31ndefinition get_index_bv ≝
[240]32  λn: Nat.
33  λb: BitVector n.
34  λm: Nat.
[266]35  λp: m < n.
36    get_index Bool n b m p.
[240]37   
38interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
39   
[337]40ndefinition set_index_bv ≝
[240]41  λn: Nat.
42  λb: BitVector n.
43  λm: Nat.
[266]44  λp: m < n.
45  λc: Bool.
[314]46    set_index Bool n b m c.
[240]47   
48ndefinition drop ≝
49  λn: Nat.
50  λb: BitVector n.
51  λm: Nat.
52    drop Bool n b m.
53
54(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[236]55(* Creating bitvectors from scratch.                                          *)
56(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
57
[228]58ndefinition zero ≝
59  λn: Nat.
[260]60    ((replicate Bool n false): BitVector n).
[228]61   
[236]62ndefinition max ≝
63  λn: Nat.
[260]64    ((replicate Bool n true): BitVector n).
[236]65   
[237]66ndefinition append ≝
67  λm, n: Nat.
68  λb: BitVector m.
69  λc: BitVector n.
70    append Bool m n b c.
[240]71   
[237]72ndefinition pad ≝
73  λm, n: Nat.
74  λb: BitVector n.
[260]75    let padding ≝ replicate Bool m false in
[237]76      append Bool m n padding b.
[240]77     
78(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
79(* Other manipulations.                                                       *)
80(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[237]81
[240]82ndefinition reverse ≝
83  λn: Nat.
84  λb: BitVector n.
85    reverse Bool n b.
86
87ndefinition length ≝
88  λn: Nat.
89  λb: BitVector n.
90    length Bool n b.
91
[236]92(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
93(* Logical operations.                                                        *)
94(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
95   
[343]96ndefinition conjunction_bv ≝
[228]97  λn: Nat.
98  λb: BitVector n.
99  λc: BitVector n.
[240]100    zip_with Bool Bool Bool n conjunction b c.
101   
102interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).
[237]103   
[343]104ndefinition inclusive_disjunction_bv ≝
[228]105  λn: Nat.
106  λb: BitVector n.
107  λc: BitVector n.
[240]108    zip_with Bool Bool Bool n inclusive_disjunction b c.
109   
110interpretation "BitVector inclusive disjunction"
111  'inclusive_disjunction b c = (inclusive_disjunction ? b c).
[237]112         
[343]113ndefinition exclusive_disjunction_bv ≝
[228]114  λn: Nat.
115  λb: BitVector n.
116  λc: BitVector n.
[240]117    zip_with Bool Bool Bool n exclusive_disjunction b c.
[232]118   
[240]119interpretation "BitVector exclusive disjunction"
120  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
121   
[337]122ndefinition negation_bv ≝
[234]123  λn: Nat.
124  λb: BitVector n.
125    map Bool Bool n (negation) b.
[240]126   
127interpretation "BitVector negation" 'negation b c = (negation ? b c).
[238]128
129(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
130(* Rotates and shifts.                                                        *)
131(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
132
[337]133ndefinition rotate_left_bv ≝
134  λn, m: Nat.
[238]135  λb: BitVector n.
136    rotate_left Bool n m b.
137
[337]138ndefinition rotate_right_bv ≝
139  λn, m: Nat.
[238]140  λb: BitVector n.
[240]141    rotate_right Bool n m b.
[236]142   
[337]143ndefinition shift_left_bv ≝
144  λn, m: Nat.
[240]145  λb: BitVector n.
146  λc: Bool.
147    shift_left Bool n m b c.
148   
[337]149ndefinition shift_right_bv ≝
150  λn, m: Nat.
[240]151  λb: BitVector n.
152  λc: Bool.
153    shift_right Bool n m b c.
154   
[236]155(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
156(* Conversions to and from lists and natural numbers.                         *)
157(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[232]158
[237]159ndefinition list_of_bitvector ≝
160  λn: Nat.
161  λb: BitVector n.
162    list_of_vector Bool n b.
[236]163   
[237]164ndefinition bitvector_of_list ≝
165  λl: List Bool.
166    vector_of_list Bool l.
[234]167
[235]168nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
[237]169  let divrem ≝ divide_with_remainder n (S (S Z)) in
170  let div ≝ first Nat Nat divrem in
171  let rem ≝ second Nat Nat divrem in
[235]172    match div with
173      [ Z ⇒
174        match rem with
175          [ Z ⇒ Empty Bool
[260]176          | S r ⇒ ? (true :: (bitvector_of_nat_aux Z))
[235]177          ]
178      | S d ⇒
179        match rem with
[260]180          [ Z ⇒ ? (false :: (bitvector_of_nat_aux (S d)))
181          | S r ⇒ ? (true :: (bitvector_of_nat_aux (S d)))
[235]182          ]
[236]183      ].
[237]184      //.
185nqed.
[236]186
[315]187ndefinition eq_bv ≝
188  λn: Nat.
189  λb, c: BitVector n.
190    eq_v Bool n (λd, e.
191      if inclusive_disjunction (conjunction d e) (conjunction (negation d)
192                                                              (negation e)) then
193        true
194      else
195        false) b c.
196
[273]197nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
198  let biglist ≝ reverse ? (bitvector_of_nat_aux m) in
199  let size ≝ length ? biglist in
200  let bitvector ≝ bitvector_of_list biglist in
201  let difference ≝ n - size in
202    match greater_than_b size n with
203      [ true ⇒ max n
204      | false ⇒ ? (pad difference size bitvector)
205      ].
206      nnormalize.
207      nrewrite > (plus_minus_inverse_right n ?).
208      #H.
209      nassumption.
210nqed.
211
[237]212nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
213  match b with
214    [ Empty ⇒ Z
215    | Cons o hd tl ⇒
[260]216      let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
[248]217        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
[260]218    ].
[313]219   
220naxiom full_add:
221  ∀n: Nat.
222  ∀b, c: BitVector n.
223  ∀d: Bit.
224    Bool × (BitVector n).
[320]225   
226ndefinition half_add ≝
227  λn: Nat.
228  λb, c: BitVector n.
229    full_add n b c false.
Note: See TracBrowser for help on using the repository browser.