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

Last change on this file since 719 was 712, checked in by mulligan, 10 years ago

Changes to get things to typecheck.

File size: 8.0 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
117definition 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
124  λn: nat.
125  λb, c: BitVector n.
126    let 〈res,flags〉 ≝ add_with_carries n b c false in
127      res.
128
129definition subtraction ≝
130  λn: nat.
131  λb, c: BitVector n.
132    addition_n n b (two_complement_negation n c).
133
134definition 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
142definition 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
154definition 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    //
189qed.
190
191definition 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
203definition 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
213definition 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
222definition gt_u ≝ λn, b, c. lt_u n c b.
223
224definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
225
226definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
227
228definition 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
245definition gt_s ≝ λn,b,c. lt_s n c b.
246
247definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
248
249definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
250
251alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
252
253definition 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  //
259qed.
260
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