source: Deliverables/D3.1/C-semantics/cerco/BitVector.ma @ 535

Last change on this file since 535 was 535, checked in by campbell, 8 years ago

Minimal integration of bitvectors into Clight semantics

  • does a "round trip" through Z for most operations (slow)
  • a few extra bits for equality on vectors
  • version of reverse that doesn't make matita fall over on size 32 vectors during disambiguation and automation
File size: 5.5 KB
Line 
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
8include "arithmetics/nat.ma".
9
10include "cerco/Util.ma".
11include "cerco/Vector.ma".
12include "cerco/String.ma".
13
14(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
15(* Common synonyms.                                                           *)
16(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
17
18definition BitVector ≝ λn: nat. Vector bool n.
19definition Bit ≝ bool.
20definition Nibble ≝ BitVector 4.
21definition Byte7 ≝ BitVector 7.
22definition Byte ≝ BitVector 8.
23definition Word ≝ BitVector 16.
24definition Word11 ≝ BitVector 11.
25
26(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
27(* Lookup.                                                                    *)
28(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
29
30(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
31(* Creating bitvectors from scratch.                                          *)
32(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
33
34definition zero: ∀n:nat. BitVector n ≝
35  λn: nat. replicate bool n false.
36   
37definition maximum: ∀n:nat. BitVector n ≝
38  λn: nat. replicate bool n true.
39 
40definition pad ≝
41  λm, n: nat.
42  λb: BitVector n.
43    let padding ≝ replicate bool m false in
44      append bool m n padding b.
45     
46(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
47(* Other manipulations.                                                       *)
48(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
49
50(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
51(* Logical operations.                                                        *)
52(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
53   
54definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
55  λn: nat.
56  λb: BitVector n.
57  λc: BitVector n.
58    zip_with ? ? ? n (andb) b c.
59   
60interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
61   
62definition inclusive_disjunction_bv ≝
63  λn: nat.
64  λb: BitVector n.
65  λc: BitVector n.
66    zip_with ? ? ? n (orb) b c.
67   
68interpretation "BitVector inclusive disjunction"
69  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
70         
71definition exclusive_disjunction_bv ≝
72  λn: nat.
73  λb: BitVector n.
74  λc: BitVector n.
75    zip_with ? ? ? n (exclusive_disjunction) b c.
76   
77interpretation "BitVector exclusive disjunction"
78  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
79   
80definition negation_bv ≝
81  λn: nat.
82  λb: BitVector n.
83    map bool bool n (notb) b.
84   
85interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
86
87(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
88(* Rotates and shifts.                                                        *)
89(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
90 
91(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
92(* Conversions to and from lists and natural numbers.                         *)
93(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
94
95let rec bitvector_of_nat_aux (n: nat) (bound: nat) on bound ≝
96 match bound with
97  [ O ⇒ [ ] (* IT WILL NOT HAPPEN *)
98  | S bound' ⇒
99    let divrem ≝ divide_with_remainder n (S (S O)) in
100    let div ≝ fst nat nat divrem in
101    let rem ≝ snd nat nat divrem in
102      match div with
103        [ O ⇒
104          match rem with
105            [ O ⇒ [ ]
106            | S r ⇒ true :: (bitvector_of_nat_aux O bound')
107            ]
108        | S d ⇒
109          match rem with
110            [ O ⇒ false :: (bitvector_of_nat_aux (S d) bound')
111            | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound')
112            ]
113        ]
114  ].
115
116definition eq_bv ≝
117  λn: nat.
118  λb, c: BitVector n.
119    eq_v bool n (λd, e.
120      if (d ∧ e) ∨ ((¬d) ∧ (¬e)) then
121        true
122      else
123        false) b c.
124
125lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.
126  (x = y → P true) →
127  (x ≠ y → P false) →
128  P (eq_bv n x y).
129#P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf)
130#Q * *; normalize /3/
131qed.
132
133let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
134  let biglist ≝ rev ? (bitvector_of_nat_aux m m) in
135  let size ≝ length ? biglist in
136  let bitvector ≝ vector_of_list ? biglist in
137  let difference ≝ n - size in
138   less_than_or_equal_b_elim …
139    (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector (difference+size) ↦ BitVector n⌉))
140    (λH:¬(size ≤ n). maximum n).
141  < plus_minus_m_m
142  //
143  assumption
144qed.
145
146let rec nat_of_bitvector (n: nat) (b: BitVector n) on b: nat ≝
147  match b with
148    [ VEmpty ⇒ O
149    | VCons o hd tl ⇒
150      let hdval ≝ match hd with [ true ⇒ S O | false ⇒ O ] in
151        plus ((2^o) * hdval) (nat_of_bitvector o tl)
152    ].
153   
154axiom bitvector_of_string:
155  ∀n: nat.
156  ∀s: String.
157    BitVector n.
158   
159axiom string_of_bitvector:
160  ∀n: nat.
161  ∀b: BitVector n.
162    String.
Note: See TracBrowser for help on using the repository browser.