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

Last change on this file since 690 was 690, checked in by mulligan, 9 years ago

Moved new matita files into correct place.

File size: 6.8 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
12      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
13  λn: nat.
14  λb: BitVector n.
15  λc: BitVector n.
16  λcarry: bool.
17    let b_as_nat ≝ nat_of_bitvector n b in
18    let c_as_nat ≝ nat_of_bitvector n c in
19    let carry_as_nat ≝ nat_of_bool carry in
20    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
21    let ac_flag ≝ geb ((modulus b_as_nat (2 * n)) +
22                  (modulus c_as_nat (2 * n)) +
23                  c_as_nat) (2 * n) in
24    let bit_xxx ≝ geb ((modulus b_as_nat (2^(n - 1))) +
25                  (modulus c_as_nat (2^(n - 1))) +
26                  c_as_nat) (2^(n - 1)) in
27    let result ≝ modulus result_old (2^n) in
28    let cy_flag ≝ geb result_old (2^n) in
29    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
30      mk_pair ? ? (bitvector_of_nat n result)
31                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
32
33definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
34  λn: nat.
35  λb: BitVector n.
36  λc: BitVector n.
37  λcarry: bool.
38     let b_as_nat ≝ nat_of_bitvector n b in
39     let c_as_nat ≝ nat_of_bitvector n c in
40     let carry_as_nat ≝ nat_of_bool carry in
41     let temporary ≝ (b_as_nat mod (2 * n)) - (c_as_nat mod (2 * n)) in
42     let ac_flag ≝ ltb (b_as_nat mod (2 * n)) ((c_as_nat mod (2 * n)) + carry_as_nat) in
43     let bit_six ≝ ltb (b_as_nat mod (2^(n - 1))) ((c_as_nat mod (2^(n - 1))) + carry_as_nat) in
44     let 〈b',cy_flag〉 ≝
45       if geb b_as_nat (c_as_nat + carry_as_nat) then
46         〈b_as_nat, false〉
47       else
48         〈b_as_nat + (2^n), true〉
49     in
50       let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
51         〈bitvector_of_nat n ((b' - c_as_nat) - carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉.
52
55definition sub_8_with_carry ≝ sub_n_with_carry 8.
56definition sub_16_with_carry ≝ sub_n_with_carry 16.
57
58definition increment ≝
59  λn: nat.
60  λb: BitVector n.
61    let b_as_nat ≝ (nat_of_bitvector n b) + 1 in
62    let overflow ≝ geb b_as_nat 2^n in
63      match overflow with
64        [ false ⇒ bitvector_of_nat n b_as_nat
65        | true ⇒ zero n
66        ].
67
68definition decrement ≝
69  λn: nat.
70  λb: BitVector n.
71    let b_as_nat ≝ nat_of_bitvector n b in
72      match b_as_nat with
73        [ O ⇒ maximum n
74        | S o ⇒ bitvector_of_nat n o
75        ].
76
77definition two_complement_negation ≝
78  λn: nat.
79  λb: BitVector n.
80    let new_b ≝ negation_bv n b in
81      increment n new_b.
82
84  λn: nat.
85  λb, c: BitVector n.
86    let 〈res,flags〉 ≝ add_n_with_carry n b c false in
87      res.
88
89definition subtraction ≝
90  λn: nat.
91  λb, c: BitVector n.
92    addition_n n b (two_complement_negation n c).
93
94definition multiplication ≝
95  λn: nat.
96  λb, c: BitVector n.
97    let b_nat ≝ nat_of_bitvector ? b in
98    let c_nat ≝ nat_of_bitvector ? c in
99    let result ≝ b_nat * c_nat in
100      bitvector_of_nat (n + n) result.
101
102definition division_u ≝
103  λn: nat.
104  λb, c: BitVector n.
105    let b_nat ≝ nat_of_bitvector ? b in
106    let c_nat ≝ nat_of_bitvector ? c in
107    match c_nat with
108    [ O ⇒ None ?
109    | _ ⇒
110      let result ≝ b_nat ÷ c_nat in
111        Some ? (bitvector_of_nat n result)
112    ].
113
114alias id "option1" = "cic:/matita/basics/sums/option.ind(1,0,1)".
115
116definition division_s: ∀n. ∀b, c: BitVector n. option1 (BitVector n) ≝
117  λn.
118    match n with
119    [ O ⇒ λb, c. None ?
120    | S p ⇒ λb, c: BitVector (S p).
121        let b_sign_bit ≝ get_index_v ? ? b O ? in
122        let c_sign_bit ≝ get_index_v ? ? c O ? in
123        let b_as_nat ≝ nat_of_bitvector ? b in
124        let c_as_nat ≝ nat_of_bitvector ? c in
125        match c_as_nat with
126        [ O ⇒ None ?
127        | S o ⇒
128          match b_sign_bit with
129          [ true ⇒
130            let temp_b ≝ b_as_nat - (2^p) in
131            match c_sign_bit with
132            [ true ⇒
133              let temp_c ≝ c_as_nat - (2^p) in
134                Some ? (bitvector_of_nat ? (temp_b ÷ temp_c))
135            | false ⇒
136              let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
137                Some ? (bitvector_of_nat ? result)
138            ]
139          | false ⇒
140            match c_sign_bit with
141            [ true ⇒
142              let temp_c ≝ c_as_nat - (2^p) in
143              let result ≝ (b_as_nat ÷ temp_c) + (2^p) in
144                Some ? (bitvector_of_nat ? result)
145            | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
146            ]
147          ]
148        ]
149    ].
150    //
151qed.
152
153definition modulus_u ≝
154  λn.
155  λb, c: BitVector n.
156    let b_nat ≝ nat_of_bitvector ? b in
157    let c_nat ≝ nat_of_bitvector ? c in
158    let result ≝ modulus b_nat c_nat in
159      bitvector_of_nat (n + n) result.
160
161definition modulus_s ≝
162  λn.
163  λb, c: BitVector n.
164    match division_s n b c with
165      [ None ⇒ None ?
166      | Some result ⇒
167          let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
168            Some ? (subtraction n b low_bits)
169      ].
170
171definition lt_u ≝
172  λn.
173  λb, c: BitVector n.
174    let b_nat ≝ nat_of_bitvector ? b in
175    let c_nat ≝ nat_of_bitvector ? c in
176      ltb b_nat c_nat.
177
178definition gt_u ≝ λn, b, c. lt_u n c b.
179
180definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
181
182definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
183
184definition lt_s ≝
185  λn.
186  λb, c: BitVector n.
187    let 〈result, flags〉 ≝ sub_n_with_carry n b c false in
188    let ov_flag ≝ get_index_v ? ? flags 2 ? in
189     if ov_flag then
190       true
191     else
192       ((match n return λn'.BitVector n' → bool with
193       [ O ⇒ λ_.false
194       | S o ⇒
195         λresult'.(get_index_v ? ? result' O ?)
196       ]) result).
197  //
198qed.
199
200definition gt_s ≝ λn,b,c. lt_s n c b.
201
202definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
203
204definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
205
206alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
207
208definition bitvector_of_bool:
209      ∀n: nat. ∀b: bool. BitVector (S n) ≝
210  λn: nat.
211  λb: bool.
212   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
213  //
214qed.
215
217  λn: nat.
218  λb, c: BitVector n.
219  λd: Bit.
220    fold_right2_i ? ? ? (
221      λn.
222       λb1, b2: bool.
223        λd: Bit × (BitVector n).
224        let 〈c1,r〉 ≝ d in
225          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
226           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
227     〈d, [[ ]]〉 ? b c.
228