1 | |
---|
2 | include "binary/Z.ma". |
---|
3 | include "cerco/BitVector.ma". |
---|
4 | include "cerco/Arithmetic.ma". |
---|
5 | |
---|
6 | let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝ |
---|
7 | match bv with |
---|
8 | [ VEmpty ⇒ OZ |
---|
9 | | VCons n' h t ⇒ |
---|
10 | if h then pos (fold_left ??? (λacc,b.if b then (p1 acc) else (p0 acc)) one t) |
---|
11 | else (Z_of_unsigned_bitvector ? t) |
---|
12 | ]. |
---|
13 | |
---|
14 | definition Z_of_signed_bitvector ≝ |
---|
15 | λn.λbv:BitVector n. |
---|
16 | match bv with |
---|
17 | [ VEmpty ⇒ OZ |
---|
18 | | VCons n' h t ⇒ |
---|
19 | if h then - (Zsucc (Z_of_unsigned_bitvector ? (negation_bv ? t))) |
---|
20 | else (Z_of_unsigned_bitvector n' t) |
---|
21 | ]. |
---|
22 | |
---|
23 | (* Reverses, so LSB first. *) |
---|
24 | let rec bits_of_pos (p:Pos) : list bool ≝ |
---|
25 | match p with |
---|
26 | [ one ⇒ [true] |
---|
27 | | p0 p' ⇒ false::(bits_of_pos p') |
---|
28 | | p1 p' ⇒ true::(bits_of_pos p') |
---|
29 | ]. |
---|
30 | |
---|
31 | let rec zeroext_reversed (n:nat) (m:nat) (bv:BitVector n) on m : BitVector m ≝ |
---|
32 | match m with |
---|
33 | [ O ⇒ [[ ]] |
---|
34 | | S m' ⇒ |
---|
35 | match bv with |
---|
36 | [ VEmpty ⇒ zero (S m') |
---|
37 | | VCons n' h t ⇒ VCons ? m' h (zeroext_reversed n' m' t) |
---|
38 | ] |
---|
39 | ]. |
---|
40 | |
---|
41 | let rec bitvector_of_Z (n:nat) (z:Z) on z : BitVector n ≝ |
---|
42 | match z with |
---|
43 | [ OZ ⇒ zero n |
---|
44 | | pos p ⇒ |
---|
45 | let bits ≝ bits_of_pos p in |
---|
46 | reverse ?? (zeroext_reversed ? n (vector_of_list … bits)) |
---|
47 | | neg p ⇒ |
---|
48 | match p with |
---|
49 | [ one ⇒ maximum ? |
---|
50 | | _ ⇒ |
---|
51 | let bits ≝ bits_of_pos (pred p) in |
---|
52 | let pz ≝ reverse ?? (zeroext_reversed ? n (vector_of_list … bits)) in |
---|
53 | negation_bv ? pz |
---|
54 | ] |
---|
55 | ]. |
---|
56 | |
---|
57 | theorem bv_Z_unsigned_min : ∀n. ∀bv:BitVector n. OZ ≤ Z_of_unsigned_bitvector n bv. |
---|
58 | #n #bv elim bv |
---|
59 | [ // |
---|
60 | | #m * #t #IH whd in ⊢ (??%) // |
---|
61 | ] qed. |
---|
62 | |
---|
63 | (* Use bit counting to show the max *) |
---|
64 | |
---|
65 | let rec pos_length (p:Pos) : nat ≝ |
---|
66 | match p with |
---|
67 | [ one ⇒ O |
---|
68 | | p0 q ⇒ S (pos_length q) |
---|
69 | | p1 q ⇒ S (pos_length q) |
---|
70 | ]. |
---|
71 | |
---|
72 | lemma pos_length_lt: ∀p,q. pos_length p < pos_length q → p < q. |
---|
73 | #p elim p |
---|
74 | [ * [ normalize #H elim (absurd ? H (not_le_Sn_n 0)) |
---|
75 | | #q #_ @(lt_one_S (p0 q)) |
---|
76 | | #q #_ >p0_times2 /2/ |
---|
77 | ] |
---|
78 | | #p' #IH |
---|
79 | * [ normalize #H elim (absurd ? H (not_le_Sn_O ?)) |
---|
80 | | #q #H change with (one+ (p0 p') < one+(p0 q)) @monotonic_lt_plus_r |
---|
81 | >p0_times2 >(p0_times2 q) |
---|
82 | @monotonic_lt_times_r @IH |
---|
83 | @le_S_S_to_le @H |
---|
84 | | #q #H change with ((succ one)+ (p0 p') ≤ (p0 q)) |
---|
85 | >p0_times2 >(p0_times2 q) |
---|
86 | @monotonic_le_times_r @IH |
---|
87 | @le_S_S_to_le @H |
---|
88 | ] |
---|
89 | | #p' #IH |
---|
90 | * [ normalize #H elim (absurd ? H (not_le_Sn_O ?)) |
---|
91 | | #q #H change with ((p0 p') < succ (p0 q)) @le_S |
---|
92 | >p0_times2 >(p0_times2 q) |
---|
93 | @monotonic_lt_times_r @IH |
---|
94 | @le_S_S_to_le @H |
---|
95 | | #q #H |
---|
96 | >p0_times2 >(p0_times2 q) |
---|
97 | @monotonic_lt_times_r @IH |
---|
98 | @le_S_S_to_le @H |
---|
99 | ] |
---|
100 | ] qed. |
---|
101 | |
---|
102 | lemma bvZ_length : ∀n.∀bv:BitVector n. match Z_of_unsigned_bitvector n bv with |
---|
103 | [ OZ ⇒ True | pos p ⇒ pos_length p < n | neg p ⇒ False ]. |
---|
104 | #n #bv elim bv |
---|
105 | [ @I |
---|
106 | | #m * |
---|
107 | [ 2: #tl normalize cases (Z_of_unsigned_bitvector m tl) normalize /2/ |
---|
108 | | #tl #_ normalize @le_S_S |
---|
109 | change with (? ≤ pos_length one + m) |
---|
110 | generalize in ⊢ (?(?(?????%?))(?(?%)?)) elim tl |
---|
111 | [ // | #o * #t normalize #IH #p <plus_n_Sm |
---|
112 | change with (? ≤ pos_length (p1 p) + o) |
---|
113 | @IH |
---|
114 | ] |
---|
115 | ] qed. |
---|
116 | |
---|
117 | lemma two_power_length : ∀n. pos_length (two_power_nat n) = n. |
---|
118 | #n elim n |
---|
119 | [ @refl |
---|
120 | | #m #IH normalize > IH @refl |
---|
121 | ] qed. |
---|
122 | |
---|
123 | theorem bv_Z_unsigned_max : ∀n. ∀bv:BitVector n. Z_of_unsigned_bitvector n bv < Z_two_power_nat n. |
---|
124 | #n #bv normalize |
---|
125 | lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2/ |
---|
126 | qed. |
---|
127 | |
---|
128 | lemma Zopp_le: ∀x,y. x ≤ y → -y ≤ -x. |
---|
129 | * [ 2,3: #p ] * [ 2,3: #q ] // |
---|
130 | qed. |
---|
131 | |
---|
132 | theorem bv_Z_signed_min : ∀n. ∀bv:BitVector n. - Z_two_power_nat n ≤ Z_of_signed_bitvector n bv. |
---|
133 | #n * |
---|
134 | [ // |
---|
135 | | #m * |
---|
136 | [ #bv @Zopp_le @(transitive_Zle … (Z_two_power_nat m)) |
---|
137 | [ @Zlt_to_Zle @bv_Z_unsigned_max |
---|
138 | | normalize // |
---|
139 | ] |
---|
140 | | #bv @(transitive_Zle … 0) // |
---|
141 | ] |
---|
142 | ] qed. |
---|
143 | |
---|
144 | theorem bv_Z_signed_max : ∀n. ∀bv:BitVector (S n). Z_of_signed_bitvector (S n) bv < Z_two_power_nat n. |
---|
145 | #n #bv @(vector_inv_n ? (S n) ? bv) * |
---|
146 | [ #t whd in ⊢ (?%%) lapply (bv_Z_unsigned_min … (negation_bv n t)) |
---|
147 | cases (Z_of_unsigned_bitvector n (negation_bv n t)) // |
---|
148 | #p * |
---|
149 | | #t whd in ⊢ (?%?) // |
---|
150 | ] qed. |
---|