# source:Deliverables/D3.1/C-semantics/cerco/Arithmetic.ma@533

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

Make stuff from D4.1 work with my copy of matita.

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      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
114definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
115  λn.
116    match n with
117    [ O ⇒ λb, c. None ?
118    | S p ⇒ λb, c: BitVector (S p).
119        let b_sign_bit ≝ get_index_v ? ? b O ? in
120        let c_sign_bit ≝ get_index_v ? ? c O ? in
121        let b_as_nat ≝ nat_of_bitvector ? b in
122        let c_as_nat ≝ nat_of_bitvector ? c in
123        match c_as_nat with
124        [ O ⇒ None ?
125        | S o ⇒
126          match b_sign_bit with
127          [ true ⇒
128            let temp_b ≝ b_as_nat - (2^p) in
129            match c_sign_bit with
130            [ true ⇒
131              let temp_c ≝ c_as_nat - (2^p) in
132                Some ? (bitvector_of_nat ? (temp_b ÷ temp_c))
133            | false ⇒
134              let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
135                Some ? (bitvector_of_nat ? result)
136            ]
137          | false ⇒
138            match c_sign_bit with
139            [ true ⇒
140              let temp_c ≝ c_as_nat - (2^p) in
141              let result ≝ (b_as_nat ÷ temp_c) + (2^p) in
142                Some ? (bitvector_of_nat ? result)
143            | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
144            ]
145          ]
146        ]
147    ].
148    //
149qed.
150
151definition modulus_u ≝
152  λn.
153  λb, c: BitVector n.
154    let b_nat ≝ nat_of_bitvector ? b in
155    let c_nat ≝ nat_of_bitvector ? c in
156    let result ≝ modulus b_nat c_nat in
157      bitvector_of_nat (n + n) result.
158
159definition modulus_s ≝
160  λn.
161  λb, c: BitVector n.
162    match division_s n b c with
163      [ None ⇒ None ?
164      | Some result ⇒
165          let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
166            Some ? (subtraction n b low_bits)
167      ].
168
169definition lt_u ≝
170  λn.
171  λb, c: BitVector n.
172    let b_nat ≝ nat_of_bitvector ? b in
173    let c_nat ≝ nat_of_bitvector ? c in
174      ltb b_nat c_nat.
175
176definition gt_u ≝ λn, b, c. lt_u n c b.
177
178definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
179
180definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
181
182definition lt_s ≝
183  λn.
184  λb, c: BitVector n.
185    let 〈result, flags〉 ≝ sub_n_with_carry n b c false in
186    let ov_flag ≝ get_index_v ? ? flags 2 ? in
187     if ov_flag then
188       true
189     else
190       ((match n return λn'.BitVector n' → bool with
191       [ O ⇒ λ_.false
192       | S o ⇒
193         λresult'.(get_index_v ? ? result' O ?)
194       ]) result).
195  //
196qed.
197
198definition gt_s ≝ λn,b,c. lt_s n c b.
199
200definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
201
202definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
203
204alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
205
206definition bitvector_of_bool:
207      ∀n: nat. ∀b: bool. BitVector (S n) ≝
208  λn: nat.
209  λb: bool.
210   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
211  //
212qed.
213
215  λn: nat.
216  λb, c: BitVector n.
217  λd: Bit.
218    fold_right2_i ? ? ? (
219      λn.
220       λb1, b2: bool.
221        λd: Bit × (BitVector n).
222        let 〈c1,r〉 ≝ d in
223          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
224           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
225     〈d, [[ ]]〉 ? b c.
226