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

Last change on this file since 1892 was 1870, checked in by boender, 9 years ago
• changed sigma00 in Assembly to use foldl_strong + proved invariants
• commented out sigma00_append
File size: 13.1 KB
Line
1include "ASM/BitVector.ma".
2include "ASM/Util.ma".
3
5  λpc: Word.
6  λa: Word11.
7  let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
8  let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
9  let 〈b123, b〉 ≝ split … 3 8 a in
10  let b1 ≝ get_index_v … b123 0 ? in
11  let b2 ≝ get_index_v … b123 1 ? in
12  let b3 ≝ get_index_v … b123 2 ? in
13  let p5 ≝ get_index_v … n2 0 ? in
14    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
15  //
16qed.
17
18definition nat_of_bool ≝
19  λb: bool.
20    match b with
21      [ false ⇒ O
22      | true ⇒ S O
23      ].
24
25definition carry_of : bool → bool → bool → bool ≝
26λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ].
27
28definition add_with_carries : ∀n:nat. BitVector n → BitVector n → bool →
29                                      BitVector n × (BitVector n) ≝
30  λn,x,y,init_carry.
31  fold_right2_i ???
32   (λn,b,c,r.
33     let 〈lower_bits, carries〉 ≝ r in
34     let last_carry ≝ match carries with [ VEmpty ⇒ init_carry | VCons _ cy _ ⇒ cy ] in
35      (* Next if-then-else just to avoid a quadratic blow-up of the whd of an application
37     if last_carry then
38      let bit ≝ xorb (xorb b c) true in
39      let carry ≝ carry_of b c true in
40       〈bit:::lower_bits, carry:::carries〉
41     else
42      let bit ≝ xorb (xorb b c) false in
43      let carry ≝ carry_of b c false in
44       〈bit:::lower_bits, carry:::carries〉
45   )
46   〈[[ ]], [[ ]]〉 n x y.
47
48(* Essentially the only difference for subtraction. *)
49definition borrow_of : bool → bool → bool → bool ≝
50λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ].
51
52definition sub_with_borrows : ∀n:nat. BitVector n → BitVector n → bool →
53                                      BitVector n × (BitVector n) ≝
54  λn,x,y,init_borrow.
55  fold_right2_i ???
56   (λn,b,c,r.
57     let 〈lower_bits, borrows〉 ≝ r in
58     let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in
59     let bit ≝ xorb (xorb b c) last_borrow in
60     let borrow ≝ borrow_of b c last_borrow in
61       〈bit:::lower_bits, borrow:::borrows〉
62   )
63   〈[[ ]], [[ ]]〉 n x y.
64
66      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. n ≥ 5 →
67      (BitVector n) × (BitVector 3) ≝
68  λn: nat.
69  λb: BitVector n.
70  λc: BitVector n.
71  λcarry: bool.
72  λpf:n ≥ 5.
73
74    let 〈result, carries〉 ≝ add_with_carries n b c carry in
75    let cy_flag ≝ get_index_v ?? carries 0 ? in
76    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
77    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
78      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
79// @(transitive_le  … pf) /2/
80qed.
81
82definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. n ≥ 5 →
83                                            (BitVector n) × (BitVector 3) ≝
84  λn: nat.
85  λb: BitVector n.
86  λc: BitVector n.
87  λcarry: bool.
88  λpf:n ≥ 5.
89
90    let 〈result, carries〉 ≝ sub_with_borrows n b c carry in
91    let cy_flag ≝ get_index_v ?? carries 0 ? in
92    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
93    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
94      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
95// @(transitive_le  … pf) /2/
96qed.
97
99  λb, c: BitVector 8.
100  λcarry: bool.
101  add_n_with_carry 8 b c carry ?.
102  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
103qed.
104
106  λb, c: BitVector 16.
107  λcarry: bool.
108  add_n_with_carry 16 b c carry ?.
109  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
110  @le_S @le_S @le_n (* ugly: fix using tacticals *)
111qed.
112
113(* dpm: needed for assembly proof *)
114definition sub_7_with_carry ≝
115  λb, c: BitVector 7.
116  λcarry: bool.
117  sub_n_with_carry 7 b c carry ?.
118  @le_S @le_S @le_n
119qed.
120
121definition sub_8_with_carry ≝
122  λb, c: BitVector 8.
123  λcarry: bool.
124  sub_n_with_carry 8 b c carry ?.
125  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
126qed.
127
128definition sub_16_with_carry ≝
129  λb, c: BitVector 16.
130  λcarry: bool.
131  sub_n_with_carry 16 b c carry ?.
132  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
133  @le_S @le_S @le_n (* ugly: fix using tacticals *)
134qed.
135
136definition increment ≝
137  λn: nat.
138  λb: BitVector n.
139    \fst (add_with_carries n b (zero n) true).
140
141definition decrement ≝
142  λn: nat.
143  λb: BitVector n.
144    \fst (sub_with_borrows n b (zero n) true).
145
146let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝
147  match m with
148  [ O ⇒ v
149  | S m' ⇒ bitvector_of_nat_aux n m' (increment n v)
150  ].
151
152definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝
153  λn,m. bitvector_of_nat_aux n m (zero n).
154
155let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝
156match v with
157[ VEmpty ⇒ m
158| VCons n' hd tl ⇒ nat_of_bitvector_aux n' (if hd then 2*m +1 else 2*m) tl
159].
160
161definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
162  λn,v. nat_of_bitvector_aux n O v.
163
164lemma bitvector_of_nat_ok:
165  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
166 #n elim n -n
167 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl
168 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
169 ]
170qed.
171
172lemma bitvector_of_nat_abs:
173  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
174 #n #x #y #Hx #Hy #Heq @notb_elim
175 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
176 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
177 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
178 | #H / by I/
179 ]
180qed.
181
182definition two_complement_negation ≝
183  λn: nat.
184  λb: BitVector n.
185    let new_b ≝ negation_bv n b in
186      increment n new_b.
187
189  λn: nat.
190  λb, c: BitVector n.
191    let 〈res,flags〉 ≝ add_with_carries n b c false in
192      res.
193
194definition subtraction ≝
195  λn: nat.
196  λb, c: BitVector n.
197    addition_n n b (two_complement_negation n c).
198
199let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
200match b with
201[ VEmpty ⇒ acc
202| VCons m' hd tl ⇒
203    let acc' ≝ if hd then addition_n ? c acc else acc in
204    mult_aux m' n tl (shift_right_1 ?? c false) acc'
205].
206
207definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
208  λn: nat.
209  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
210  [ O ⇒ λ_.λ_.[[ ]]
211  | S m ⇒
212    λb, c : BitVector (S m).
213    let c' ≝ pad (S m) (S m) c in
214      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
215  ].
216
217(* Division:  001...000 divided by 000...010
218     Shift the divisor as far left as possible,
219                                  100...000
220      then try subtracting it at each
221      bit position, shifting left as we go.
222              001...000 - 100...000 X ⇒ 0
223              001...000 - 010...000 X ⇒ 0
224              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
225              ...
226      Then pad out the remaining bits at the front
227         00..001...
228*)
229inductive fbs_diff : nat → Type[0] ≝
230| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
231
232let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
233match b return λn.λ_. option (fbs_diff n) with
234[ VEmpty ⇒ None ?
235| VCons m h t ⇒
236    if h then Some ? (fbs_diff' O m)
237    else match first_bit_set m t with
238         [ None ⇒ None ?
239         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
240         ]
241].
242
243let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
244match m with
245[ O ⇒ 〈[[ ]], q〉
246| S m' ⇒
247    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
248    let bit ≝ head' … flags in
249    let q'' ≝ if bit then q' else q in
250    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
251    〈bit:::tl, md〉
252].
253
254definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
255  λn: nat.
256  λb, c: BitVector (S n).
257
258    match first_bit_set ? c with
259    [ None ⇒ None ?
260    | Some fbs' ⇒
261        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
262          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
263          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
264        ]
265    ].
266
267definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
268λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
269
270definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
271  λn.
272    match n with
273    [ O ⇒ λb, c. None ?
274    | S p ⇒ λb, c: BitVector (S p).
275        let b_sign_bit ≝ get_index_v ? ? b O ? in
276        let c_sign_bit ≝ get_index_v ? ? c O ? in
277        match b_sign_bit with
278        [ true ⇒
279          let neg_b ≝ two_complement_negation ? b in
280          match c_sign_bit with
281          [ true ⇒
282              (* I was worrying slightly about -2^(n-1), whose negation can't
283                 be represented in an n bit signed number.  However, it's
284                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
285                 so it's fine. *)
286              division_u ? neg_b (two_complement_negation ? c)
287          | false ⇒
288              match division_u ? neg_b c with
289              [ None ⇒ None ?
290              | Some r ⇒ Some ? (two_complement_negation ? r)
291              ]
292          ]
293        | false ⇒
294          match c_sign_bit with
295          [ true ⇒
296              match division_u ? b (two_complement_negation ? c) with
297              [ None ⇒ None ?
298              | Some r ⇒ Some ? (two_complement_negation ? r)
299              ]
300          | false ⇒ division_u ? b c
301          ]
302        ]
303   ].
304    //
305qed.
306
307definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
308λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
309
310definition modulus_s ≝
311  λn.
312  λb, c: BitVector n.
313    match division_s n b c with
314      [ None ⇒ None ?
315      | Some result ⇒
316          let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
317            Some ? (subtraction n b low_bits)
318      ].
319
320definition lt_u ≝
321  fold_right2_i ???
322    (λ_.λa,b,r.
323      match a with
324      [ true ⇒ b ∧ r
325      | false ⇒ b ∨ r
326      ])
327    false.
328
329definition gt_u ≝ λn, b, c. lt_u n c b.
330
331definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
332
333definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
334
335definition lt_s ≝
336  λn.
337  λb, c: BitVector n.
338    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
339    match borrows with
340    [ VEmpty ⇒ false
341    | VCons _ bwn tl ⇒
342      match tl with
343      [ VEmpty ⇒ false
344      | VCons _ bwpn _ ⇒
345        if xorb bwn bwpn then
346          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
347        else
348          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
349      ]
350    ].
351
352definition gt_s ≝ λn,b,c. lt_s n c b.
353
354definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
355
356definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
357
358alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
359
360definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
361definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
362definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
363definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
364
365definition bitvector_of_bool:
366      ∀n: nat. ∀b: bool. BitVector (S n) ≝
367  λn: nat.
368  λb: bool.
369   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
370  //
371qed.
372
374  λn: nat.
375  λb, c: BitVector n.
376  λd: Bit.
377    fold_right2_i ? ? ? (
378      λn.
379       λb1, b2: bool.
380        λd: Bit × (BitVector n).
381        let 〈c1,r〉 ≝ d in
382          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
383           (xorb (xorb b1 b2) c1) ::: r〉)
384     〈d, [[ ]]〉 ? b c.
385
387  λn: nat.
388  λb, c: BitVector n.
389    full_add n b c false.
390
391definition sign_bit : ∀n. BitVector n → bool ≝
392λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
393
394definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
395λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
396
397definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
398λm,n.
399  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
400  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
401  | nat_eq n' ⇒ λv. v
402  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
403  ].
404
405definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
406λm,n.
407  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
408  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
409  | nat_eq n' ⇒ λv. v
410  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
411  ].
412
Note: See TracBrowser for help on using the repository browser.