# source:src/ASM/Arithmetic.ma@724

Last change on this file since 724 was 724, checked in by campbell, 9 years ago

More tractable version of bitvector_of_nat / nat_of_bitvector.

File size: 8.5 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
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
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
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
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
152definition multiplication ≝
153  λn: nat.
154  λb, c: BitVector n.
155    let b_nat ≝ nat_of_bitvector ? b in
156    let c_nat ≝ nat_of_bitvector ? c in
157    let result ≝ b_nat * c_nat in
158      bitvector_of_nat (n + n) result.
159
160definition division_u ≝
161  λn: nat.
162  λb, c: BitVector n.
163    let b_nat ≝ nat_of_bitvector ? b in
164    let c_nat ≝ nat_of_bitvector ? c in
165    match c_nat with
166    [ O ⇒ None ?
167    | _ ⇒
168      let result ≝ b_nat ÷ c_nat in
169        Some ? (bitvector_of_nat n result)
170    ].
171
172definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
173  λn.
174    match n with
175    [ O ⇒ λb, c. None ?
176    | S p ⇒ λb, c: BitVector (S p).
177        let b_sign_bit ≝ get_index_v ? ? b O ? in
178        let c_sign_bit ≝ get_index_v ? ? c O ? in
179        let b_as_nat ≝ nat_of_bitvector ? b in
180        let c_as_nat ≝ nat_of_bitvector ? c in
181        match c_as_nat with
182        [ O ⇒ None ?
183        | S o ⇒
184          match b_sign_bit with
185          [ true ⇒
186            let temp_b ≝ b_as_nat - (2^p) in
187            match c_sign_bit with
188            [ true ⇒
189              let temp_c ≝ c_as_nat - (2^p) in
190                Some ? (bitvector_of_nat ? (temp_b ÷ temp_c))
191            | false ⇒
192              let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
193                Some ? (bitvector_of_nat ? result)
194            ]
195          | false ⇒
196            match c_sign_bit with
197            [ true ⇒
198              let temp_c ≝ c_as_nat - (2^p) in
199              let result ≝ (b_as_nat ÷ temp_c) + (2^p) in
200                Some ? (bitvector_of_nat ? result)
201            | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
202            ]
203          ]
204        ]
205    ].
206    //
207qed.
208
209definition modulus_u ≝
210  λn.
211  λb, c: BitVector n.
212    let b_nat ≝ nat_of_bitvector ? b in
213    let c_nat ≝ nat_of_bitvector ? c in
214    match c_nat with
215    [ O ⇒ None ?
216    | _ ⇒
217      let result ≝ modulus b_nat c_nat in
218      Some ? (bitvector_of_nat n result)
219    ].
220
221definition modulus_s ≝
222  λn.
223  λb, c: BitVector n.
224    match division_s n b c with
225      [ None ⇒ None ?
226      | Some result ⇒
227          let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
228            Some ? (subtraction n b low_bits)
229      ].
230
231definition lt_u ≝
232  fold_right2_i ???
233    (λ_.λa,b,r.
234      match a with
235      [ true ⇒ b ∧ r
236      | false ⇒ b ∨ r
237      ])
238    false.
239
240definition gt_u ≝ λn, b, c. lt_u n c b.
241
242definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
243
244definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
245
246definition lt_s ≝
247  λn.
248  λb, c: BitVector n.
249    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
250    match borrows with
251    [ VEmpty ⇒ false
252    | VCons _ bwn tl ⇒
253      match tl with
254      [ VEmpty ⇒ false
255      | VCons _ bwpn _ ⇒
256        if exclusive_disjunction bwn bwpn then
257          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
258        else
259          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
260      ]
261    ].
262
263definition gt_s ≝ λn,b,c. lt_s n c b.
264
265definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
266
267definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
268
269alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
270
271definition bitvector_of_bool:
272      ∀n: nat. ∀b: bool. BitVector (S n) ≝
273  λn: nat.
274  λb: bool.
275   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
276  //
277qed.
278
280  λn: nat.
281  λb, c: BitVector n.
282  λd: Bit.
283    fold_right2_i ? ? ? (
284      λn.
285       λb1, b2: bool.
286        λd: Bit × (BitVector n).
287        let 〈c1,r〉 ≝ d in
288          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
289           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
290     〈d, [[ ]]〉 ? b c.
291