1 | include "ASM/BitVector.ma". |
---|
2 | include "ASM/Util.ma". |
---|
3 | |
---|
4 | definition nat_of_bool ≝ |
---|
5 | λb: bool. |
---|
6 | match b with |
---|
7 | [ false ⇒ O |
---|
8 | | true ⇒ S O |
---|
9 | ]. |
---|
10 | |
---|
11 | definition carry_of : bool → bool → bool → bool ≝ |
---|
12 | λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ]. |
---|
13 | |
---|
14 | definition add_with_carries : ∀n:nat. BitVector n → BitVector n → bool → |
---|
15 | BitVector n × (BitVector n) ≝ |
---|
16 | λn,x,y,init_carry. |
---|
17 | fold_right2_i ??? |
---|
18 | (λn,b,c,r. |
---|
19 | let 〈lower_bits, carries〉 ≝ r in |
---|
20 | let last_carry ≝ match carries with [ VEmpty ⇒ init_carry | VCons _ cy _ ⇒ cy ] in |
---|
21 | let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_carry in |
---|
22 | let carry ≝ carry_of b c last_carry in |
---|
23 | 〈bit:::lower_bits, carry:::carries〉 |
---|
24 | ) |
---|
25 | 〈[[ ]], [[ ]]〉 n x y. |
---|
26 | |
---|
27 | (* Essentially the only difference for subtraction. *) |
---|
28 | definition borrow_of : bool → bool → bool → bool ≝ |
---|
29 | λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ]. |
---|
30 | |
---|
31 | definition sub_with_borrows : ∀n:nat. BitVector n → BitVector n → bool → |
---|
32 | BitVector n × (BitVector n) ≝ |
---|
33 | λn,x,y,init_borrow. |
---|
34 | fold_right2_i ??? |
---|
35 | (λn,b,c,r. |
---|
36 | let 〈lower_bits, borrows〉 ≝ r in |
---|
37 | let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in |
---|
38 | let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_borrow in |
---|
39 | let borrow ≝ borrow_of b c last_borrow in |
---|
40 | 〈bit:::lower_bits, borrow:::borrows〉 |
---|
41 | ) |
---|
42 | 〈[[ ]], [[ ]]〉 n x y. |
---|
43 | |
---|
44 | definition add_n_with_carry: |
---|
45 | ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. n ≥ 5 → |
---|
46 | (BitVector n) × (BitVector 3) ≝ |
---|
47 | λn: nat. |
---|
48 | λb: BitVector n. |
---|
49 | λc: BitVector n. |
---|
50 | λcarry: bool. |
---|
51 | λpf:n ≥ 5. |
---|
52 | |
---|
53 | let 〈result, carries〉 ≝ add_with_carries n b c carry in |
---|
54 | let cy_flag ≝ get_index_v ?? carries 0 ? in |
---|
55 | let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in |
---|
56 | let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *) |
---|
57 | 〈result, [[ cy_flag; ac_flag; ov_flag ]]〉. |
---|
58 | // @(transitive_le … pf) /2/ |
---|
59 | qed. |
---|
60 | |
---|
61 | definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. n ≥ 5 → |
---|
62 | (BitVector n) × (BitVector 3) ≝ |
---|
63 | λn: nat. |
---|
64 | λb: BitVector n. |
---|
65 | λc: BitVector n. |
---|
66 | λcarry: bool. |
---|
67 | λpf:n ≥ 5. |
---|
68 | |
---|
69 | let 〈result, carries〉 ≝ sub_with_borrows n b c carry in |
---|
70 | let cy_flag ≝ get_index_v ?? carries 0 ? in |
---|
71 | let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in |
---|
72 | let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *) |
---|
73 | 〈result, [[ cy_flag; ac_flag; ov_flag ]]〉. |
---|
74 | // @(transitive_le … pf) /2/ |
---|
75 | qed. |
---|
76 | |
---|
77 | definition add_8_with_carry ≝ |
---|
78 | λb, c: BitVector 8. |
---|
79 | λcarry: bool. |
---|
80 | add_n_with_carry 8 b c carry ?. |
---|
81 | @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *) |
---|
82 | qed. |
---|
83 | |
---|
84 | definition add_16_with_carry ≝ |
---|
85 | λb, c: BitVector 16. |
---|
86 | λcarry: bool. |
---|
87 | add_n_with_carry 16 b c carry ?. |
---|
88 | @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S |
---|
89 | @le_S @le_S @le_n (* ugly: fix using tacticals *) |
---|
90 | qed. |
---|
91 | |
---|
92 | definition sub_8_with_carry ≝ |
---|
93 | λb, c: BitVector 8. |
---|
94 | λcarry: bool. |
---|
95 | sub_n_with_carry 8 b c carry ?. |
---|
96 | @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *) |
---|
97 | qed. |
---|
98 | |
---|
99 | definition sub_16_with_carry ≝ |
---|
100 | λb, c: BitVector 16. |
---|
101 | λcarry: bool. |
---|
102 | sub_n_with_carry 16 b c carry ?. |
---|
103 | @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S |
---|
104 | @le_S @le_S @le_n (* ugly: fix using tacticals *) |
---|
105 | qed. |
---|
106 | |
---|
107 | definition increment ≝ |
---|
108 | λn: nat. |
---|
109 | λb: BitVector n. |
---|
110 | \fst (add_with_carries n b (zero n) true). |
---|
111 | |
---|
112 | definition decrement ≝ |
---|
113 | λn: nat. |
---|
114 | λb: BitVector n. |
---|
115 | \fst (sub_with_borrows n b (zero n) true). |
---|
116 | |
---|
117 | definition two_complement_negation ≝ |
---|
118 | λn: nat. |
---|
119 | λb: BitVector n. |
---|
120 | let new_b ≝ negation_bv n b in |
---|
121 | increment n new_b. |
---|
122 | |
---|
123 | definition addition_n ≝ |
---|
124 | λn: nat. |
---|
125 | λb, c: BitVector n. |
---|
126 | let 〈res,flags〉 ≝ add_with_carries n b c false in |
---|
127 | res. |
---|
128 | |
---|
129 | definition subtraction ≝ |
---|
130 | λn: nat. |
---|
131 | λb, c: BitVector n. |
---|
132 | addition_n n b (two_complement_negation n c). |
---|
133 | |
---|
134 | definition multiplication ≝ |
---|
135 | λn: nat. |
---|
136 | λb, c: BitVector n. |
---|
137 | let b_nat ≝ nat_of_bitvector ? b in |
---|
138 | let c_nat ≝ nat_of_bitvector ? c in |
---|
139 | let result ≝ b_nat * c_nat in |
---|
140 | bitvector_of_nat (n + n) result. |
---|
141 | |
---|
142 | definition division_u ≝ |
---|
143 | λn: nat. |
---|
144 | λb, c: BitVector n. |
---|
145 | let b_nat ≝ nat_of_bitvector ? b in |
---|
146 | let c_nat ≝ nat_of_bitvector ? c in |
---|
147 | match c_nat with |
---|
148 | [ O ⇒ None ? |
---|
149 | | _ ⇒ |
---|
150 | let result ≝ b_nat ÷ c_nat in |
---|
151 | Some ? (bitvector_of_nat n result) |
---|
152 | ]. |
---|
153 | |
---|
154 | definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝ |
---|
155 | λn. |
---|
156 | match n with |
---|
157 | [ O ⇒ λb, c. None ? |
---|
158 | | S p ⇒ λb, c: BitVector (S p). |
---|
159 | let b_sign_bit ≝ get_index_v ? ? b O ? in |
---|
160 | let c_sign_bit ≝ get_index_v ? ? c O ? in |
---|
161 | let b_as_nat ≝ nat_of_bitvector ? b in |
---|
162 | let c_as_nat ≝ nat_of_bitvector ? c in |
---|
163 | match c_as_nat with |
---|
164 | [ O ⇒ None ? |
---|
165 | | S o ⇒ |
---|
166 | match b_sign_bit with |
---|
167 | [ true ⇒ |
---|
168 | let temp_b ≝ b_as_nat - (2^p) in |
---|
169 | match c_sign_bit with |
---|
170 | [ true ⇒ |
---|
171 | let temp_c ≝ c_as_nat - (2^p) in |
---|
172 | Some ? (bitvector_of_nat ? (temp_b ÷ temp_c)) |
---|
173 | | false ⇒ |
---|
174 | let result ≝ (temp_b ÷ c_as_nat) + (2^p) in |
---|
175 | Some ? (bitvector_of_nat ? result) |
---|
176 | ] |
---|
177 | | false ⇒ |
---|
178 | match c_sign_bit with |
---|
179 | [ true ⇒ |
---|
180 | let temp_c ≝ c_as_nat - (2^p) in |
---|
181 | let result ≝ (b_as_nat ÷ temp_c) + (2^p) in |
---|
182 | Some ? (bitvector_of_nat ? result) |
---|
183 | | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat)) |
---|
184 | ] |
---|
185 | ] |
---|
186 | ] |
---|
187 | ]. |
---|
188 | // |
---|
189 | qed. |
---|
190 | |
---|
191 | definition modulus_u ≝ |
---|
192 | λn. |
---|
193 | λb, c: BitVector n. |
---|
194 | let b_nat ≝ nat_of_bitvector ? b in |
---|
195 | let c_nat ≝ nat_of_bitvector ? c in |
---|
196 | match c_nat with |
---|
197 | [ O ⇒ None ? |
---|
198 | | _ ⇒ |
---|
199 | let result ≝ modulus b_nat c_nat in |
---|
200 | Some ? (bitvector_of_nat n result) |
---|
201 | ]. |
---|
202 | |
---|
203 | definition modulus_s ≝ |
---|
204 | λn. |
---|
205 | λb, c: BitVector n. |
---|
206 | match division_s n b c with |
---|
207 | [ None ⇒ None ? |
---|
208 | | Some result ⇒ |
---|
209 | let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in |
---|
210 | Some ? (subtraction n b low_bits) |
---|
211 | ]. |
---|
212 | |
---|
213 | definition lt_u ≝ |
---|
214 | fold_right2_i ??? |
---|
215 | (λ_.λa,b,r. |
---|
216 | match a with |
---|
217 | [ true ⇒ b ∧ r |
---|
218 | | false ⇒ b ∨ r |
---|
219 | ]) |
---|
220 | false. |
---|
221 | |
---|
222 | definition gt_u ≝ λn, b, c. lt_u n c b. |
---|
223 | |
---|
224 | definition lte_u ≝ λn, b, c. ¬(gt_u n b c). |
---|
225 | |
---|
226 | definition gte_u ≝ λn, b, c. ¬(lt_u n b c). |
---|
227 | |
---|
228 | definition lt_s ≝ |
---|
229 | λn. |
---|
230 | λb, c: BitVector n. |
---|
231 | let 〈result, borrows〉 ≝ sub_with_borrows n b c false in |
---|
232 | match borrows with |
---|
233 | [ VEmpty ⇒ false |
---|
234 | | VCons _ bwn tl ⇒ |
---|
235 | match tl with |
---|
236 | [ VEmpty ⇒ false |
---|
237 | | VCons _ bwpn _ ⇒ |
---|
238 | if exclusive_disjunction bwn bwpn then |
---|
239 | match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ] |
---|
240 | else |
---|
241 | match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ] |
---|
242 | ] |
---|
243 | ]. |
---|
244 | |
---|
245 | definition gt_s ≝ λn,b,c. lt_s n c b. |
---|
246 | |
---|
247 | definition lte_s ≝ λn,b,c. ¬(gt_s n b c). |
---|
248 | |
---|
249 | definition gte_s ≝ λn. λb, c. ¬(lt_s n b c). |
---|
250 | |
---|
251 | alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop". |
---|
252 | |
---|
253 | definition bitvector_of_bool: |
---|
254 | ∀n: nat. ∀b: bool. BitVector (S n) ≝ |
---|
255 | λn: nat. |
---|
256 | λb: bool. |
---|
257 | (pad n 1 [[b]])⌈n + 1 ↦ S n⌉. |
---|
258 | // |
---|
259 | qed. |
---|
260 | |
---|
261 | definition full_add ≝ |
---|
262 | λn: nat. |
---|
263 | λb, c: BitVector n. |
---|
264 | λd: Bit. |
---|
265 | fold_right2_i ? ? ? ( |
---|
266 | λn. |
---|
267 | λb1, b2: bool. |
---|
268 | λd: Bit × (BitVector n). |
---|
269 | let 〈c1,r〉 ≝ d in |
---|
270 | 〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)), |
---|
271 | (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉) |
---|
272 | 〈d, [[ ]]〉 ? b c. |
---|
273 | |
---|
274 | definition half_add ≝ |
---|
275 | λn: nat. |
---|
276 | λb, c: BitVector n. |
---|
277 | full_add n b c false. |
---|