source: src/ASM/Arithmetic.ma @ 861

Last change on this file since 861 was 744, checked in by campbell, 10 years ago

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File size: 10.6 KB
Line 
1include "ASM/BitVector.ma".
2include "ASM/Util.ma".
3
4definition nat_of_bool ≝
5  λb: bool.
6    match b with
7      [ false ⇒ O
8      | true ⇒ S O
9      ].
10
11definition carry_of : bool → bool → bool → bool ≝
12λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ].
13
14definition 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. *)
28definition borrow_of : bool → bool → bool → bool ≝
29λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ].
30
31definition 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   
44definition 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/
59qed.
60
61definition 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/
75qed.
76
77definition 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 *)
82qed.
83
84definition 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 *)
90qed.
91
92definition 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 *)
97qed.
98
99definition 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 *)
105qed.
106
107definition increment ≝
108  λn: nat.
109  λb: BitVector n.
110    \fst (add_with_carries n b (zero n) true).
111       
112definition decrement ≝
113  λn: nat.
114  λb: BitVector n.
115    \fst (sub_with_borrows n b (zero n) true).
116
117let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝
118  match m with
119  [ O ⇒ v
120  | S m' ⇒ bitvector_of_nat_aux n m' (increment n v)
121  ].
122
123definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝
124  λn,m. bitvector_of_nat_aux n m (zero n).
125
126let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝
127match v with
128[ VEmpty ⇒ m
129| VCons n' hd tl ⇒ nat_of_bitvector_aux n' (if hd then 2*m +1 else 2*m) tl
130].
131
132definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
133  λn,v. nat_of_bitvector_aux n O v.
134
135definition two_complement_negation ≝
136  λn: nat.
137  λb: BitVector n.
138    let new_b ≝ negation_bv n b in
139      increment n new_b.
140   
141definition addition_n ≝
142  λn: nat.
143  λb, c: BitVector n.
144    let 〈res,flags〉 ≝ add_with_carries n b c false in
145      res.
146   
147definition subtraction ≝
148  λn: nat.
149  λb, c: BitVector n.
150    addition_n n b (two_complement_negation n c).
151
152let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
153match b with
154[ VEmpty ⇒ acc
155| VCons m' hd tl ⇒
156    let acc' ≝ if hd then addition_n ? c acc else acc in
157    mult_aux m' n tl (shift_right_1 ?? c false) acc'
158].
159
160definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
161  λn: nat.
162  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
163  [ O ⇒ λ_.λ_.[[ ]]
164  | S m ⇒
165    λb, c : BitVector (S m).
166    let c' ≝ pad (S m) (S m) c in
167      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
168  ].
169
170(* Division:  001...000 divided by 000...010
171     Shift the divisor as far left as possible,
172                                  100...000
173      then try subtracting it at each
174      bit position, shifting left as we go.
175              001...000 - 100...000 X ⇒ 0
176              001...000 - 010...000 X ⇒ 0
177              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
178              ...
179      Then pad out the remaining bits at the front
180         00..001...
181*)
182inductive fbs_diff : nat → Type[0] ≝
183| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
184
185let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
186match b return λn.λ_. option (fbs_diff n) with
187[ VEmpty ⇒ None ?
188| VCons m h t ⇒
189    if h then Some ? (fbs_diff' O m)
190    else match first_bit_set m t with
191         [ None ⇒ None ?
192         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
193         ]
194].
195
196let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
197match m with
198[ O ⇒ 〈[[ ]], q〉
199| S m' ⇒
200    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
201    let bit ≝ head' … flags in
202    let q'' ≝ if bit then q' else q in
203    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
204    〈bit:::tl, md〉
205].
206
207definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
208  λn: nat.
209  λb, c: BitVector (S n).
210
211    match first_bit_set ? c with
212    [ None ⇒ None ?
213    | Some fbs' ⇒
214        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
215          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
216          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
217        ]
218    ].
219
220definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
221λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
222     
223definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
224  λn.
225    match n with
226    [ O ⇒ λb, c. None ?
227    | S p ⇒ λb, c: BitVector (S p).
228        let b_sign_bit ≝ get_index_v ? ? b O ? in
229        let c_sign_bit ≝ get_index_v ? ? c O ? in
230        match b_sign_bit with
231        [ true ⇒
232          let neg_b ≝ two_complement_negation ? b in
233          match c_sign_bit with
234          [ true ⇒
235              (* I was worrying slightly about -2^(n-1), whose negation can't
236                 be represented in an n bit signed number.  However, it's
237                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
238                 so it's fine. *)
239              division_u ? neg_b (two_complement_negation ? c)
240          | false ⇒
241              match division_u ? neg_b c with
242              [ None ⇒ None ?
243              | Some r ⇒ Some ? (two_complement_negation ? r)
244              ]
245          ]
246        | false ⇒
247          match c_sign_bit with
248          [ true ⇒
249              match division_u ? b (two_complement_negation ? c) with
250              [ None ⇒ None ?
251              | Some r ⇒ Some ? (two_complement_negation ? r)
252              ]
253          | false ⇒ division_u ? b c
254          ]
255        ]
256   ].
257    //
258qed.
259
260definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
261λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
262           
263definition modulus_s ≝
264  λn.
265  λb, c: BitVector n.
266    match division_s n b c with
267      [ None ⇒ None ?
268      | Some result ⇒
269          let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
270            Some ? (subtraction n b low_bits)
271      ].
272     
273definition lt_u ≝
274  fold_right2_i ???
275    (λ_.λa,b,r.
276      match a with
277      [ true ⇒ b ∧ r
278      | false ⇒ b ∨ r
279      ])
280    false.
281     
282definition gt_u ≝ λn, b, c. lt_u n c b.
283
284definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
285
286definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
287
288definition lt_s ≝
289  λn.
290  λb, c: BitVector n.
291    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
292    match borrows with
293    [ VEmpty ⇒ false
294    | VCons _ bwn tl ⇒
295      match tl with
296      [ VEmpty ⇒ false
297      | VCons _ bwpn _ ⇒
298        if exclusive_disjunction bwn bwpn then
299          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
300        else
301          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
302      ]
303    ].
304   
305definition gt_s ≝ λn,b,c. lt_s n c b.
306
307definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
308
309definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
310     
311alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
312
313definition bitvector_of_bool:
314      ∀n: nat. ∀b: bool. BitVector (S n) ≝
315  λn: nat.
316  λb: bool.
317   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
318  //
319qed.
320
321definition full_add ≝
322  λn: nat.
323  λb, c: BitVector n.
324  λd: Bit.
325    fold_right2_i ? ? ? (
326      λn.
327       λb1, b2: bool.
328        λd: Bit × (BitVector n).
329        let 〈c1,r〉 ≝ d in
330          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
331           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
332     〈d, [[ ]]〉 ? b c.
333   
334definition half_add ≝
335  λn: nat.
336  λb, c: BitVector n.
337    full_add n b c false.
Note: See TracBrowser for help on using the repository browser.