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