source:src/ASM/Arithmetic.ma@697

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

Merge Clight branch of vectors and friends.
Start making stuff build.

File size: 7.4 KB
Line
1include "cerco/BitVector.ma".
2include "cerco/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
79definition sub_8_with_carry ≝ sub_n_with_carry 8.
80definition sub_16_with_carry ≝ sub_n_with_carry 16.
81
82definition increment ≝
83  λn: nat.
84  λb: BitVector n.
85    \fst (add_with_carries n b (zero n) true).
86
87definition decrement ≝
88  λn: nat.
89  λb: BitVector n.
90    \fst (sub_with_borrows n b (zero n) true).
91
92definition two_complement_negation ≝
93  λn: nat.
94  λb: BitVector n.
95    let new_b ≝ negation_bv n b in
96      increment n new_b.
97
99  λn: nat.
100  λb, c: BitVector n.
101    let 〈res,flags〉 ≝ add_with_carries n b c false in
102      res.
103
104definition subtraction ≝
105  λn: nat.
106  λb, c: BitVector n.
107    addition_n n b (two_complement_negation n c).
108
109definition multiplication ≝
110  λn: nat.
111  λb, c: BitVector n.
112    let b_nat ≝ nat_of_bitvector ? b in
113    let c_nat ≝ nat_of_bitvector ? c in
114    let result ≝ b_nat * c_nat in
115      bitvector_of_nat (n + n) result.
116
117definition division_u ≝
118  λn: nat.
119  λb, c: BitVector n.
120    let b_nat ≝ nat_of_bitvector ? b in
121    let c_nat ≝ nat_of_bitvector ? c in
122    match c_nat with
123    [ O ⇒ None ?
124    | _ ⇒
125      let result ≝ b_nat ÷ c_nat in
126        Some ? (bitvector_of_nat n result)
127    ].
128
129definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
130  λn.
131    match n with
132    [ O ⇒ λb, c. None ?
133    | S p ⇒ λb, c: BitVector (S p).
134        let b_sign_bit ≝ get_index_v ? ? b O ? in
135        let c_sign_bit ≝ get_index_v ? ? c O ? in
136        let b_as_nat ≝ nat_of_bitvector ? b in
137        let c_as_nat ≝ nat_of_bitvector ? c in
138        match c_as_nat with
139        [ O ⇒ None ?
140        | S o ⇒
141          match b_sign_bit with
142          [ true ⇒
143            let temp_b ≝ b_as_nat - (2^p) in
144            match c_sign_bit with
145            [ true ⇒
146              let temp_c ≝ c_as_nat - (2^p) in
147                Some ? (bitvector_of_nat ? (temp_b ÷ temp_c))
148            | false ⇒
149              let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
150                Some ? (bitvector_of_nat ? result)
151            ]
152          | false ⇒
153            match c_sign_bit with
154            [ true ⇒
155              let temp_c ≝ c_as_nat - (2^p) in
156              let result ≝ (b_as_nat ÷ temp_c) + (2^p) in
157                Some ? (bitvector_of_nat ? result)
158            | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
159            ]
160          ]
161        ]
162    ].
163    //
164qed.
165
166definition modulus_u ≝
167  λn.
168  λb, c: BitVector n.
169    let b_nat ≝ nat_of_bitvector ? b in
170    let c_nat ≝ nat_of_bitvector ? c in
171    match c_nat with
172    [ O ⇒ None ?
173    | _ ⇒
174      let result ≝ modulus b_nat c_nat in
175      Some ? (bitvector_of_nat n result)
176    ].
177
178definition modulus_s ≝
179  λn.
180  λb, c: BitVector n.
181    match division_s n b c with
182      [ None ⇒ None ?
183      | Some result ⇒
184          let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
185            Some ? (subtraction n b low_bits)
186      ].
187
188definition lt_u ≝
189  fold_right2_i ???
190    (λ_.λa,b,r.
191      match a with
192      [ true ⇒ b ∧ r
193      | false ⇒ b ∨ r
194      ])
195    false.
196
197definition gt_u ≝ λn, b, c. lt_u n c b.
198
199definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
200
201definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
202
203definition lt_s ≝
204  λn.
205  λb, c: BitVector n.
206    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
207    match borrows with
208    [ VEmpty ⇒ false
209    | VCons _ bwn tl ⇒
210      match tl with
211      [ VEmpty ⇒ false
212      | VCons _ bwpn _ ⇒
213        if exclusive_disjunction bwn bwpn then
214          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
215        else
216          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
217      ]
218    ].
219
220definition gt_s ≝ λn,b,c. lt_s n c b.
221
222definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
223
224definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
225
226alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
227
228definition bitvector_of_bool:
229      ∀n: nat. ∀b: bool. BitVector (S n) ≝
230  λn: nat.
231  λb: bool.
232   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
233  //
234qed.
235
237  λn: nat.
238  λb, c: BitVector n.
239  λd: Bit.
240    fold_right2_i ? ? ? (
241      λn.
242       λb1, b2: bool.
243        λd: Bit × (BitVector n).
244        let 〈c1,r〉 ≝ d in
245          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
246           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
247     〈d, [[ ]]〉 ? b c.
248