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

Last change on this file since 2907 was 2796, checked in by tranquil, 8 years ago
• added global notation for existence in Type[1] (\exists[1] x.P)
• in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
• in joint_semantics, moved out and around some parameters in primitive semantics functions
• fixed all back end semantics
• added skeleton files for single passes correctness proofs
File size: 38.3 KB
Line
1include "ASM/BitVector.ma".
2include "ASM/Util.ma".
3include "arithmetics/exp.ma".
4
6  λpc: Word.
7  λa: Word11.
8  let 〈pc_upper, ignore〉 ≝ vsplit … 8 8 pc in
9  let 〈n1, n2〉 ≝ vsplit … 4 4 pc_upper in
10  let 〈b123, b〉 ≝ vsplit … 3 8 a in
11  let b1 ≝ get_index_v … b123 0 ? in
12  let b2 ≝ get_index_v … b123 1 ? in
13  let b3 ≝ get_index_v … b123 2 ? in
14  let p5 ≝ get_index_v … n2 0 ? in
15    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
16  //
17qed.
18
19definition nat_of_bool ≝
20  λb: bool.
21    match b with
22      [ false ⇒ O
23      | true ⇒ S O
24      ].
25
26definition carry_of : bool → bool → bool → bool ≝
27λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ].
28
29definition add_with_carries : ∀n:nat. BitVector n → BitVector n → bool →
30                                      BitVector n × (BitVector n) ≝
31  λn,x,y,init_carry.
32  fold_right2_i ???
33   (λn,b,c,r.
34     let 〈lower_bits, carries〉 ≝ r in
35     let last_carry ≝ match carries with [ VEmpty ⇒ init_carry | VCons _ cy _ ⇒ cy ] in
36      (* Next if-then-else just to avoid a quadratic blow-up of the whd of an application
38     if last_carry then
39      let bit ≝ xorb (xorb b c) true in
40      let carry ≝ carry_of b c true in
41       〈bit:::lower_bits, carry:::carries〉
42     else
43      let bit ≝ xorb (xorb b c) false in
44      let carry ≝ carry_of b c false in
45       〈bit:::lower_bits, carry:::carries〉
46   )
47   〈[[ ]], [[ ]]〉 n x y.
48
49(* Essentially the only difference for subtraction. *)
50definition borrow_of : bool → bool → bool → bool ≝
51λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ].
52
53definition sub_with_borrows : ∀n:nat. BitVector n → BitVector n → bool →
54                                      BitVector n × (BitVector n) ≝
55  λn,x,y,init_borrow.
56  fold_right2_i ???
57   (λn,b,c,r.
58     let 〈lower_bits, borrows〉 ≝ r in
59     let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in
60     let bit ≝ xorb (xorb b c) last_borrow in
61     let borrow ≝ borrow_of b c last_borrow in
62       〈bit:::lower_bits, borrow:::borrows〉
63   )
64   〈[[ ]], [[ ]]〉 n x y.
65
67      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. n ≥ 5 →
68      (BitVector n) × (BitVector 3) ≝
69  λn: nat.
70  λb: BitVector n.
71  λc: BitVector n.
72  λcarry: bool.
73  λpf:n ≥ 5.
74
75    let 〈result, carries〉 ≝ add_with_carries n b c carry in
76    let cy_flag ≝ get_index_v ?? carries 0 ? in
77    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
78    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
79      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
80// @(transitive_le  … pf) /2/
81qed.
82
83definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. n ≥ 5 →
84                                            (BitVector n) × (BitVector 3) ≝
85  λn: nat.
86  λb: BitVector n.
87  λc: BitVector n.
88  λcarry: bool.
89  λpf:n ≥ 5.
90
91    let 〈result, carries〉 ≝ sub_with_borrows n b c carry in
92    let cy_flag ≝ get_index_v ?? carries 0 ? in
93    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
94    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
95      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
96// @(transitive_le  … pf) /2/
97qed.
98
100  λb, c: BitVector 8.
101  λcarry: bool.
102  add_n_with_carry 8 b c carry ?.
103  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
104qed.
105
107  λb, c: BitVector 16.
108  λcarry: bool.
109  add_n_with_carry 16 b c carry ?.
110  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
111  @le_S @le_S @le_n (* ugly: fix using tacticals *)
112qed.
113
114(* dpm: needed for assembly proof *)
115definition sub_7_with_carry ≝
116  λb, c: BitVector 7.
117  λcarry: bool.
118  sub_n_with_carry 7 b c carry ?.
119  @le_S @le_S @le_n
120qed.
121
122definition sub_8_with_carry ≝
123  λb, c: BitVector 8.
124  λcarry: bool.
125  sub_n_with_carry 8 b c carry ?.
126  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
127qed.
128
129definition sub_16_with_carry ≝
130  λb, c: BitVector 16.
131  λcarry: bool.
132  sub_n_with_carry 16 b c carry ?.
133  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
134  @le_S @le_S @le_n (* ugly: fix using tacticals *)
135qed.
136
137definition increment ≝
138  λn: nat.
139  λb: BitVector n.
140    \fst (add_with_carries n b (zero n) true).
141
142definition decrement ≝
143  λn: nat.
144  λb: BitVector n.
145    \fst (sub_with_borrows n b (zero n) true).
146
147(* The following implementation is extremely inefficient*)
148let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝
149  match m with
150  [ O ⇒ v
151  | S m' ⇒ bitvector_of_nat_aux n m' (increment n v)
152  ].
153
154definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝
155  λn,m. bitvector_of_nat_aux n m (zero n).
156
157(* This one by Paolo is efficient, but it is for the opposite indianess.
158-(* jpb: we already have bitvector_of_nat and friends in the library, maybe
159- * we should unify this in some way *)
160(* Paolo: converted to good endianness *)
161let rec bitvector_of_nat_aux (n_acc : nat) (acc :BitVector n_acc) n (k : nat) on n : BitVector (plus n_acc n) ≝
162  match n return λn.BitVector (plus n_acc n) with
163  [ O ⇒ acc⌈BitVector n_acc ↦ ?⌉
164  | S n' ⇒
165    bitvector_of_nat_aux (S n_acc) (eqb (k mod 2) 1 ::: acc) n' (k ÷ 2)
166      ⌈BitVector (S n_acc + n') ↦ ?⌉
167  ].
168[ cases (plus_n_O ?) | cases (plus_n_Sm ??) ] % qed.
169
170definition bitvector_of_nat : ∀n.ℕ → BitVector n ≝ bitvector_of_nat_aux' ? [[ ]].
171
172-let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝
173-  match b with
174-  [ VEmpty ⇒ 0
175-  | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].
176-
177*)
178
179let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝
180match v with
181[ VEmpty ⇒ m
182| VCons n' hd tl ⇒ nat_of_bitvector_aux n' (if hd then 2*m +1 else 2*m) tl
183].
184
185definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
186  λn,v. nat_of_bitvector_aux n O v.
187
188(* TODO: remove when standard library arithmetics/exp.ma is used in place
189   of definition in ASM/Util.ma *)
190theorem lt_O_exp: ∀n,m:nat. O < n → O < n^m.
191#n #m (elim m) normalize // #a #Hind #posn
192@(le_times 1 ? 1) /2 by / qed.
193theorem le_exp: ∀n,m,p:nat. O < p →
194  n ≤m → p^n ≤ p^m.
195  @nat_elim2 #n #m
196  [#ltm #len @lt_O_exp //
197  |#_ #len @False_ind /2 by absurd/
198  |#Hind #p #posp #lenm normalize @le_times // @Hind /2 by monotonic_pred/
199  ]
200qed.
201
202lemma nat_of_bitvector_aux_lt_bound:
203 ∀n.∀v:BitVector n. ∀m,l:nat.
204  m < 2^l → nat_of_bitvector_aux n m v < 2^(n+l).
205 #n #v elim v normalize // -n
206 #n #hd #tl #IH #m #l #B cases hd normalize nodelta
207 @(transitive_le … (IH ? (S l) …))
208 [2,4: change with (?≤2^(S (n+l))) @le_exp /2 by le_n/
209 |1,3: @(transitive_le … (2 * (S m)))
210  [2,4: whd in ⊢ (??%); /2 by le_plus/
211  |3: // | 1: normalize <plus_n_O <plus_n_Sm // ]]
212qed.
213
214lemma nat_of_bitvector_lt_bound:
215 ∀n: nat. ∀b: BitVector n. nat_of_bitvector n b < 2^n.
216 #n #b lapply (nat_of_bitvector_aux_lt_bound n b 0 0 ?) // <plus_n_O //
217qed.
218
219lemma bitvector_of_nat_ok:
220  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
221 #n elim n -n
222 [ #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
223 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
224 ]
225qed.
226
227lemma bitvector_of_nat_abs:
228  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
229 #n #x #y #Hx #Hy #Heq @notb_elim
230 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
231 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
232 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
233 | #H / by I/
234 ]
235qed.
236
237axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n.
238
239axiom nat_of_bitvector_bitvector_of_nat_inverse:
240  ∀n: nat.
241  ∀b: nat.
242    b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b.
243
244axiom bitvector_of_nat_inverse_nat_of_bitvector:
245  ∀n: nat.
246  ∀b: BitVector n.
247    bitvector_of_nat n (nat_of_bitvector n b) = b.
248
249axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
250
251axiom eq_bitvector_of_nat_to_eq:
252 ∀n,n1,n2.
253  n1 < 2^n → n2 < 2^n →
254   bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2.
255
256lemma nat_of_bitvector_aux_injective:
257  ∀n: nat.
258  ∀l, r: BitVector n.
259  ∀acc_l, acc_r: nat.
260    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
261      acc_l = acc_r ∧ l ≃ r.
262  #n #l
263  elim l #r
264  [1:
265    #acc_l #acc_r normalize
266    >(BitVector_O r) normalize /2/
267  |2:
268    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
269    normalize normalize in inductive_hypothesis;
270    cases (BitVector_Sn … r)
271    #r_hd * #r_tl #r_refl destruct normalize
272    cases hd cases r_hd normalize
273    [1:
274      #relevant
275      cases (inductive_hypothesis … relevant)
276      #acc_assm #tl_assm destruct % //
277      lapply (injective_plus_l ? ? ? acc_assm)
278      -acc_assm #acc_assm
279      change with (2 * acc_l = 2 * acc_r) in acc_assm;
280      lapply (injective_times_r ? ? ? ? acc_assm) /2/
281    |4:
282      #relevant
283      cases (inductive_hypothesis … relevant)
284      #acc_assm #tl_assm destruct % //
285      change with (2 * acc_l = 2 * acc_r) in acc_assm;
286      lapply(injective_times_r ? ? ? ? acc_assm) /2/
287    |2:
288      #relevant
289      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
290        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
291      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
292      [1:
293        #eqb_true_assm
294        lapply (eqb_true_to_refl … eqb_true_assm)
295        #refl_assm
296        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
297      |2:
298        #eqb_false_assm
299        lapply (eqb_false_to_not_refl … eqb_false_assm)
300        #not_refl_assm cases not_refl_assm #absurd_assm
301        cases (inductive_hypothesis … relevant) #absurd
302        cases (absurd_assm absurd)
303      ]
304    |3:
305      #relevant
306      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
307        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
308      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
309      [1:
310        #eqb_true_assm
311        lapply (eqb_true_to_refl … eqb_true_assm)
312        #refl_assm
313        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
314        -refl_assm #refl_assm
315        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
316      |2:
317        #eqb_false_assm
318        lapply (eqb_false_to_not_refl … eqb_false_assm)
319        #not_refl_assm cases not_refl_assm #absurd_assm
320        cases (inductive_hypothesis … relevant) #absurd
321        cases (absurd_assm absurd)
322      ]
323    ]
324  ]
325qed.
326
327lemma nat_of_bitvector_destruct:
328  ∀n: nat.
329  ∀l_hd, r_hd: bool.
330  ∀l_tl, r_tl: BitVector n.
331    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
332      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
333  #n #l_hd #r_hd #l_tl #r_tl
334  normalize
335  cases l_hd cases r_hd
336  normalize
337  [4:
338    /2/
339  |1:
340    #relevant
341    cases (nat_of_bitvector_aux_injective … relevant)
342    #_ #l_r_tl_refl destruct /2/
343  |2,3:
344    #relevant
345    cases (nat_of_bitvector_aux_injective … relevant)
346    #absurd destruct(absurd)
347  ]
348qed.
349
350lemma BitVector_cons_injective:
351  ∀n: nat.
352  ∀l_hd, r_hd: bool.
353  ∀l_tl, r_tl: BitVector n.
354    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
355  #l #l_hd #r_hd #l_tl #r_tl
356  #l_refl #r_refl destruct %
357qed.
358
359lemma refl_nat_of_bitvector_to_refl:
360  ∀n: nat.
361  ∀l, r: BitVector n.
362    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
363  #n
364  elim n
365  [1:
366    #l #r
367    >(BitVector_O l)
368    >(BitVector_O r)
369    #_ %
370  |2:
371    #n' #inductive_hypothesis #l #r
372    lapply (BitVector_Sn ? l) #l_hypothesis
373    lapply (BitVector_Sn ? r) #r_hypothesis
374    cases l_hypothesis #l_hd #l_tail_hypothesis
375    cases r_hypothesis #r_hd #r_tail_hypothesis
376    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
377    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
378    destruct #cons_refl
379    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
380    #hd_refl #tl_refl
381    @BitVector_cons_injective try assumption
382    @inductive_hypothesis assumption
383  ]
384qed.
385
386definition two_complement_negation ≝
387  λn: nat.
388  λb: BitVector n.
389    let new_b ≝ negation_bv n b in
390      increment n new_b.
391
393  λn: nat.
394  λb, c: BitVector n.
395    let 〈res,flags〉 ≝ add_with_carries n b c false in
396      res.
397
398definition subtraction ≝
399  λn: nat.
400  λb, c: BitVector n.
401    addition_n n b (two_complement_negation n c).
402
403let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
404match b with
405[ VEmpty ⇒ acc
406| VCons m' hd tl ⇒
407    let acc' ≝ if hd then addition_n ? c acc else acc in
408    mult_aux m' n tl (shift_right_1 ?? c false) acc'
409].
410
411definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
412  λn: nat.
413  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
414  [ O ⇒ λ_.λ_.[[ ]]
415  | S m ⇒
416    λb, c : BitVector (S m).
417    let c' ≝ pad (S m) (S m) c in
418      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
419  ].
420
421definition short_multiplication : ∀n:nat. BitVector n → BitVector n → BitVector n ≝
422λn,x,y. (\snd (vsplit ??? (multiplication ? x y))).
423
424(* Division:  001...000 divided by 000...010
425     Shift the divisor as far left as possible,
426                                  100...000
427      then try subtracting it at each
428      bit position, shifting left as we go.
429              001...000 - 100...000 X ⇒ 0
430              001...000 - 010...000 X ⇒ 0
431              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
432              ...
433      Then pad out the remaining bits at the front
434         00..001...
435*)
436inductive fbs_diff : nat → Type[0] ≝
437| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
438
439let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
440match b return λn.λ_. option (fbs_diff n) with
441[ VEmpty ⇒ None ?
442| VCons m h t ⇒
443    if h then Some ? (fbs_diff' O m)
444    else match first_bit_set m t with
445         [ None ⇒ None ?
446         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
447         ]
448].
449
450let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
451match m with
452[ O ⇒ 〈[[ ]], q〉
453| S m' ⇒
454    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
455    let bit ≝ head' … flags in
456    let q'' ≝ if bit then q' else q in
457    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
458    〈bit:::tl, md〉
459].
460
461definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
462  λn: nat.
463  λb, c: BitVector (S n).
464
465    match first_bit_set ? c with
466    [ None ⇒ None ?
467    | Some fbs' ⇒
468        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
469          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
470          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
471        ]
472    ].
473
474definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
475λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
476
477definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
478  λn.
479    match n with
480    [ O ⇒ λb, c. None ?
481    | S p ⇒ λb, c: BitVector (S p).
482        let b_sign_bit ≝ get_index_v ? ? b O ? in
483        let c_sign_bit ≝ get_index_v ? ? c O ? in
484        match b_sign_bit with
485        [ true ⇒
486          let neg_b ≝ two_complement_negation ? b in
487          match c_sign_bit with
488          [ true ⇒
489              (* I was worrying slightly about -2^(n-1), whose negation can't
490                 be represented in an n bit signed number.  However, it's
491                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
492                 so it's fine. *)
493              division_u ? neg_b (two_complement_negation ? c)
494          | false ⇒
495              match division_u ? neg_b c with
496              [ None ⇒ None ?
497              | Some r ⇒ Some ? (two_complement_negation ? r)
498              ]
499          ]
500        | false ⇒
501          match c_sign_bit with
502          [ true ⇒
503              match division_u ? b (two_complement_negation ? c) with
504              [ None ⇒ None ?
505              | Some r ⇒ Some ? (two_complement_negation ? r)
506              ]
507          | false ⇒ division_u ? b c
508          ]
509        ]
510   ].
511    //
512qed.
513
514definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
515λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
516
517definition modulus_s ≝
518  λn.
519  λb, c: BitVector n.
520    match division_s n b c with
521      [ None ⇒ None ?
522      | Some result ⇒
523          let 〈high_bits, low_bits〉 ≝ vsplit bool ? n (multiplication n result c) in
524            Some ? (subtraction n b low_bits)
525      ].
526
527definition lt_u ≝
528  fold_right2_i ???
529    (λ_.λa,b,r.
530      match a with
531      [ true ⇒ b ∧ r
532      | false ⇒ b ∨ r
533      ])
534    false.
535
536definition gt_u ≝ λn, b, c. lt_u n c b.
537
538definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
539
540definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
541
542definition lt_s ≝
543  λn.
544  λb, c: BitVector n.
545    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
546    match borrows with
547    [ VEmpty ⇒ false
548    | VCons _ bwn tl ⇒
549      match tl with
550      [ VEmpty ⇒ false
551      | VCons _ bwpn _ ⇒
552        if xorb bwn bwpn then
553          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
554        else
555          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
556      ]
557    ].
558
559definition gt_s ≝ λn,b,c. lt_s n c b.
560
561definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
562
563definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
564
565alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
566
567(* Some properties of addition_n *)
569#n elim n
570[ 1: #a #b #carry
571     lapply (BitVector_O … a) lapply (BitVector_O … b) #H1 #H2 destruct @refl
572| 2: #n' #Hind #a #b #carry
573     lapply (BitVector_Sn … a) lapply (BitVector_Sn … b)
574     * #bhd * #btl #Heqb
575     * #ahd * #atl #Heqa destruct
576     lapply (Hind atl btl carry)
577     whd in match (add_with_carries ????) in ⊢ ((??%%) →  (??%%));
578     normalize in match (rewrite_l ??????);
579     normalize nodelta
580     #Heq >Heq
581     generalize in match (fold_right2_i ????????); * #res #carries
582     normalize nodelta
583     cases ahd cases bhd @refl
584] qed.
585
587#n #a #b whd in match (addition_n ???) in ⊢ (??%%); >commutative_add_with_carries
588@refl
589qed.
590
591(* -------------------------------------------------------------------------- *)
592(* Associativity proof for addition_n. The proof relies on the observation
593 * that the two carries (inner and outer) in the associativity equation are not
594 * independent. In fact, the global carry can be encoded in a three-valued bits
595 * (versus 2 full bits, i.e. 4 possibilites, for two carries). I seriously hope
596 * this proof can be simplified, but now it's proved at least. *)
597
598inductive ternary : Type[0] ≝
599| Zero_carry : ternary
600| One_carry : ternary
601| Two_carry : ternary.
602
603definition carry_0 ≝ λcarry.
604    match carry with
605    [ Zero_carry ⇒ 〈false, Zero_carry〉
606    | One_carry ⇒ 〈true, Zero_carry〉
607    | Two_carry ⇒ 〈false, One_carry〉 ].
608
609definition carry_1 ≝ λcarry.
610    match carry with
611    [ Zero_carry ⇒ 〈true, Zero_carry〉
612    | One_carry ⇒ 〈false, One_carry〉
613    | Two_carry ⇒ 〈true, One_carry〉 ].
614
615definition carry_2 ≝ λcarry.
616    match carry with
617    [ Zero_carry ⇒ 〈false, One_carry〉
618    | One_carry ⇒ 〈true, One_carry〉
619    | Two_carry ⇒ 〈false, Two_carry〉 ].
620
621definition carry_3 ≝ λcarry.
622    match carry with
623    [ Zero_carry ⇒ 〈true, One_carry〉
624    | One_carry ⇒ 〈false, Two_carry〉
625    | Two_carry ⇒ 〈true, Two_carry〉 ].
626
627(* Count the number of true bits in {xa,xb,xc} and compute the new bit along the new carry,
628   according to the last one. *)
629definition ternary_carry_of ≝ λxa,xb,xc,carry.
630if xa then
631  if xb then
632    if xc then
633      carry_3 carry
634    else
635      carry_2 carry
636  else
637    if xc then
638      carry_2 carry
639    else
640      carry_1 carry
641else
642  if xb then
643    if xc then
644      carry_2 carry
645    else
646      carry_1 carry
647  else
648    if xc then
649      carry_1 carry
650    else
651      carry_0 carry.
652
653let rec canonical_add (n : nat) (a,b,c : BitVector n) (init : ternary) on a : (BitVector n × ternary) ≝
654match a in Vector return λsz.λ_. BitVector sz → BitVector sz → (BitVector sz × ternary) with
655[ VEmpty ⇒ λ_,_. 〈VEmpty ?, init〉
656| VCons sz' xa tla ⇒ λb',c'.
657  let xb ≝ head' … b' in
658  let xc ≝ head' … c' in
659  let tlb ≝ tail … b' in
660  let tlc ≝ tail … c' in
661  let 〈bits, last〉 ≝ canonical_add ? tla tlb tlc init in
662  let 〈bit, carry〉 ≝ ternary_carry_of xa xb xc last in
663  〈bit ::: bits, carry〉
664] b c.
665
666(* convert the classical carries (inner and outer) to ternary) *)
667definition carries_to_ternary ≝ λcarry1,carry2.
668  if carry1
669  then if carry2
670       then Two_carry
671       else One_carry
672  else if carry2
673       then One_carry
674       else Zero_carry.
675
676(* Copied back from Clight/casts.ma *)
678  add_with_carries n x y c = fold_right2_i ????? n x y.
679// qed.
680
682  add_with_carries (S n) (a_hd ::: a_tl) (b_hd ::: b_tl) carry =
683   (let 〈lower_bits,carries〉 ≝ add_with_carries n a_tl b_tl carry in
684    let last_carry ≝
685    match carries in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with
686    [VEmpty⇒carry
687    |VCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy]
688    in
689    if last_carry then
690      let bit   ≝ xorb (xorb a_hd b_hd) true in
691      let carry ≝ carry_of a_hd b_hd true in
692      〈bit:::lower_bits,carry:::carries〉
693    else
694      let bit ≝ xorb (xorb a_hd b_hd) false in
695      let carry ≝ carry_of a_hd b_hd false in
696      〈bit:::lower_bits,carry:::carries〉).
697#n #a_hd #a_tl #b_hd #b_tl #carry
699normalize nodelta
701cases (add_with_carries n a_tl b_tl carry)
702#lower_bits #carries normalize nodelta
703elim n in a_tl b_tl lower_bits carries;
704[ 1: #a_tl #b_tl #lower_bits #carries
705     >(BitVector_O … carries) normalize nodelta
706     cases carry normalize nodelta
707     cases a_hd cases b_hd //
708| 2: #n' #Hind #a_tl #b_tl #lower_bits #carries
709     lapply (BitVector_Sn … carries) * #carries_hd * #carries_tl
710     #Heq >Heq normalize nodelta
711     cases carries_hd cases a_hd cases b_hd normalize nodelta
712     //
713] qed.
714
715(* Correction of [canonical_add], left side. Note the invariant on carries. *)
717  let 〈res_ab,flags_ab〉 ≝ add_with_carries n a b carry1 in
718  let 〈res_ab_c,flags_ab_c〉 ≝ add_with_carries n res_ab c carry2 in
719  let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in
720  res_ab_c = res_canonical
721  ∧ (match n return λx. BitVector x → BitVector x → Prop with
722     [ O ⇒ λ_.λ_. True
723     | S _ ⇒ λflags_ab',flags_ab_c'. carries_to_ternary (head' … flags_ab') (head' … flags_ab_c') = last_carry
724     ] flags_ab flags_ab_c).
725#n elim n
726[ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
727| 2: #n' #Hind #carry1 #carry2 #a #b #c
728     elim (BitVector_Sn … a) #xa * #a' #Heq_a
729     elim (BitVector_Sn … b) #xb * #b' #Heq_b
730     elim (BitVector_Sn … c) #xc * #c' #Heq_c
731     lapply (Hind … carry1 carry2 a' b' c') -Hind
733     elim (add_with_carries … a' b' carry1) #Hres_ab #Hflags_ab normalize nodelta
734     lapply Hflags_ab lapply Hres_ab lapply c' lapply b' lapply a'
735     -Hflags_ab -Hres_ab -c' -b' -a'
736     cases n'
737     [ 1: #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta
738          >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c')
739          >(BitVector_O … Hres_ab) >(BitVector_O … Hflags_ab)
740          normalize nodelta #_
741          cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try //
742     | 2: #n' #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta
743          elim (BitVector_Sn … Hflags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
744          normalize nodelta
745          elim (BitVector_Sn … Hres_ab) #hd_res_ab * #tl_res_ab #Heq_res_ab >Heq_res_ab
746          cases hd_flags_ab in Heq_flags_ab; #Heq_flags_ab normalize nodelta
748          elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' carry2) #res_ab_c #flags_ab_c
749          normalize nodelta
750          elim (BitVector_Sn … flags_ab_c) #hd_flags_ab_c * #tl_flags_ab_c #Heq_flags_ab_c >Heq_flags_ab_c
751          normalize nodelta
752          cases hd_flags_ab_c in Heq_flags_ab_c; #Heq_flags_ab_c
753          normalize nodelta
754          whd in match (canonical_add (S (S ?)) ? ? ? ?);
755          whd in match (tail ???); whd in match (tail ???);
756          elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize
757          * #Hres_ab_is_canonical #Hlast_carry <Hlast_carry normalize
758          >Hres_ab_is_canonical
759          cases xa cases xb cases xc try @conj try @refl
760     ]
761] qed.
762
763(* Symmetric. The two sides are most certainly doable in a single induction, but lazyness
764   prevails over style.  *)
766  let 〈res_bc,flags_bc〉 ≝ add_with_carries n b c carry1 in
767  let 〈res_a_bc,flags_a_bc〉 ≝ add_with_carries n a res_bc carry2 in
768  let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in
769  res_a_bc = res_canonical
770  ∧ (match n return λx. BitVector x → BitVector x → Prop with
771     [ O ⇒ λ_.λ_. True
772     | S _ ⇒ λflags_bc',flags_a_bc'. carries_to_ternary (head' … flags_bc') (head' … flags_a_bc') = last_carry
773     ] flags_bc flags_a_bc).
774#n elim n
775[ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
776| 2: #n' #Hind #carry1 #carry2 #a #b #c
777     elim (BitVector_Sn … a) #xa * #a' #Heq_a
778     elim (BitVector_Sn … b) #xb * #b' #Heq_b
779     elim (BitVector_Sn … c) #xc * #c' #Heq_c
780     lapply (Hind … carry1 carry2 a' b' c') -Hind
782     elim (add_with_carries … b' c' carry1) #Hres_bc #Hflags_bc normalize nodelta
783     lapply Hflags_bc lapply Hres_bc lapply c' lapply b' lapply a'
784     -Hflags_bc -Hres_bc -c' -b' -a'
785     cases n'
786     [ 1: #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta
787          >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c')
788          >(BitVector_O … Hres_bc) >(BitVector_O … Hflags_bc)
789          normalize nodelta #_
790          cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try //
791     | 2: #n' #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta
792          elim (BitVector_Sn … Hflags_bc) #hd_flags_bc * #tl_flags_bc #Heq_flags_bc >Heq_flags_bc
793          normalize nodelta
794          elim (BitVector_Sn … Hres_bc) #hd_res_bc * #tl_res_bc #Heq_res_bc >Heq_res_bc
795          cases hd_flags_bc in Heq_flags_bc; #Heq_flags_bc normalize nodelta
797          elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) carry2) #res_a_bc #flags_a_bc
798          normalize nodelta
799          elim (BitVector_Sn … flags_a_bc) #hd_flags_a_bc * #tl_flags_a_bc #Heq_flags_a_bc >Heq_flags_a_bc
800          normalize nodelta
801          cases (hd_flags_a_bc) in Heq_flags_a_bc; #Heq_flags_a_bc
802          whd in match (canonical_add (S (S ?)) ????);
803          whd in match (tail ???); whd in match (tail ???);
804          elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize
805          * #Hres_bc_is_canonical #Hlast_carry <Hlast_carry normalize
806          >Hres_bc_is_canonical
807          cases xa cases xb cases xc try @conj try @refl
808     ]
809] qed.
810
811
812(* Note that we prove a result more general that just associativity: we can vary the carries. *)
814  ∀n,carry1,carry2,a,b,c.
815  (\fst (add_with_carries n a (let 〈res,flags〉 ≝ add_with_carries n b c carry1 in res) carry2))
816   =
817  (\fst (add_with_carries n (let 〈res,flags〉 ≝ add_with_carries n a b carry1 in res) c carry2)).
818#n cases n
819[ 1: #carry1 #carry2 #a #b #c
820      >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c)
821      normalize try @refl
822| 2: #n' #carry1 #carry2 #a #b #c
823     lapply (canonical_add_left … carry1 carry2 a b c)
824     lapply (canonical_add_right … carry1 carry2 a b c)
825     normalize nodelta
826     elim (add_with_carries (S n') b c carry1) #res_bc #flags_bc
827     elim (add_with_carries (S n') a b carry1) #res_ab #flags_ab
828     normalize nodelta
829     elim (add_with_carries (S n') a res_bc carry2) #res_a_bc #flags_a_bc
830     normalize nodelta
831     elim (add_with_carries (S n') res_ab c carry2) #res_ab_c #flags_ab_c
832     normalize nodelta
833     cases (canonical_add ? a b c (carries_to_ternary carry1 carry2)) #canonical_bits #last_carry
834     normalize nodelta
835     * #HA #HB * #HC #HD destruct @refl
836] qed.
837
838(* This closes the proof of associativity for bitvector addition. *)
839
841#n #a #b #c
842whd in match (addition_n ???) in ⊢ (??%%);
843whd in match (addition_n n b c);
844whd in match (addition_n n a b);
845lapply (associative_add_with_carries … false false a b c)
846elim (add_with_carries n b c false) #bc_bits #bc_flags
847elim (add_with_carries n a b false) #ab_bits #ab_flags
848normalize nodelta
849elim (add_with_carries n a bc_bits false) #a_bc_bits #a_bc_flags
850elim (add_with_carries n ab_bits c false) #ab_c_bits #ab_c_flags
851normalize
852#H @H
853qed.
854
855
856
857definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
858definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
859definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
860definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
861
862definition bitvector_of_bool:
863      ∀n: nat. ∀b: bool. BitVector (S n) ≝
864  λn: nat.
865  λb: bool.
866   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
867  //
868qed.
869
871  λn: nat.
872  λb, c: BitVector n.
873  λd: Bit.
874    fold_right2_i ? ? ? (
875      λn.
876       λb1, b2: bool.
877        λd: Bit × (BitVector n).
878        let 〈c1,r〉 ≝ d in
879          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
880           (xorb (xorb b1 b2) c1) ::: r〉)
881     〈d, [[ ]]〉 ? b c.
882
884  λn: nat.
885  λb, c: BitVector n.
886    full_add n b c false.
887
889  λn: nat.
890  λl, r: BitVector n.
891    \snd (half_add n l r).
892
894  ∀n: nat.
895  ∀l: BitVector n.
896  ∀hd: bool.
897    \fst (half_add (S n) (hd:::l) (false:::(zero n))) =
898      andb hd (\fst (half_add n l (zero n))).
899  #n #l elim l
900  [1:
901    #hd normalize cases hd %
902  |2:
903    #n' #hd #tl #inductive_hypothesis #hd'
904    whd in match half_add; normalize nodelta
905    whd in match full_add; normalize nodelta
906    normalize in ⊢ (??%%); cases hd' normalize
907    @pair_elim #c1 #r #c1_r_refl cases c1 %
908  ]
909qed.
910
912  ∀m: nat.
913  ∀b: BitVector m.
914    \fst (half_add m b (zero m)) = false.
915  #m #b elim b try %
916  #n #hd #tl #inductive_hypothesis
917  change with (false:::(zero ?)) in match (zero ?);
918  >half_add_carry_Sn >inductive_hypothesis cases hd %
919qed.
920
922  ∀n: nat.
923  ∀hd, hd': bool.
924  ∀l, r: BitVector n.
925    \fst (half_add (S n) (true:::l) (true:::r)) = true.
926
928  ∀n: nat.
929  ∀hd, hd': bool.
930  ∀l, r: BitVector n.
931    add (S n) (hd:::l) (hd':::r) =
932      xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r.
933  #n #hd #hd' #l elim l
934  [1:
935    #r cases hd cases hd'
936    >(BitVector_O … r) normalize %
937  |2:
938    #n' #hd'' #tl #inductive_hypothesis #r
939    cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct
940    cases hd cases hd' cases hd'' cases hd'''
941    whd in match (xorb ??);
942    cases daemon
943  ]
944qed.
945
947  ∀n: nat.
948  ∀l: BitVector n.
949    l = add n l (zero …).
950  #n #l elim l try %
951  #n' #hd #tl #inductive_hypothesis
952  change with (false:::zero ?) in match (zero ?);
954  cases hd <inductive_hypothesis %
955qed.
956
957axiom most_significant_bit_zero:
958  ∀size, m: nat.
959  ∀size_proof: 0 < size.
960    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
961  normalize in size_proof; normalize @le_S_S assumption
962qed.
963
965  ∀m: nat.
966  ∀tl, hd.
967    (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl).
968
970  ∀m: nat.
971  ∀b: BitVector m.
972    add m (zero m) b = b.
973  #m #b elim b try %
974  #m' #hd #tl #inductive_hypothesis
975  <inductive_hypothesis in ⊢ (???%);
977qed.
978
979axiom bitvector_of_nat_one_Sm:
980  ∀m: nat.
981    ∃b: BitVector m.
982      bitvector_of_nat (S m) 1 ≃ b @@ [[true]].
983
984axiom increment_zero_bitvector_of_nat_1:
985  ∀m: nat.
986  ∀b: BitVector m.
987    increment m b = add m (bitvector_of_nat m 1) b.
988
990  ∀m: nat.
991  ∀l, c, r: BitVector m.
993
994lemma bitvector_of_nat_aux_buffer:
995  ∀m, n: nat.
996  ∀b: BitVector m.
997    bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b.
998  #m #n elim n
999  [1:
1000    #b change with (? = add ? (zero …) b)
1002  |2:
1003    #n' #inductive_hypothesis #b
1004    whd in match (bitvector_of_nat_aux ???);
1005    >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%);
1006    >inductive_hypothesis >increment_zero_bitvector_of_nat_1
1007    >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1))
1009  ]
1010qed.
1011
1012definition sign_extension: Byte → Word ≝
1013  λc.
1014    let b ≝ get_index_v ? 8 c 1 ? in
1015      [[ b; b; b; b; b; b; b; b ]] @@ c.
1016  normalize
1017  repeat (@le_S_S)
1018  @le_O_n
1019qed.
1020
1021lemma bitvector_of_nat_sign_extension_equivalence:
1022  ∀m: nat.
1023  ∀size_proof: m < 128.
1024    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
1025  #m #size_proof whd in ⊢ (??%?);
1026  >most_significant_bit_zero
1027  [1:
1028    elim m
1029    [1:
1030      %
1031    |2:
1032      #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta
1033      whd in match (bitvector_of_nat_aux ???);
1034      whd in match (bitvector_of_nat_aux ???) in ⊢ (???%);
1035      >(bitvector_of_nat_aux_buffer 16 n')
1036      cases daemon
1037    ]
1038  |2:
1039    assumption
1040  ]
1041qed.
1042
1044  ∀n: nat.
1045  ∀l, r: BitVector n.
1047
1049 ∀n,v1,v2.
1050  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
1051   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
1052
1054 ∀n,m1,m2.
1055  bitvector_of_nat n (m1 + m2) =
1056   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
1057
1058(* CSC: corollary of add_bitvector_of_nat *)
1060 ∀n,m,r. m + r = 2^n →
1061  add n (bitvector_of_nat n m) (bitvector_of_nat n r) = zero n.
1062
1064  ∀n: nat.
1065  ∀m: nat.
1066    add n (bitvector_of_nat … m) (bitvector_of_nat … 1) = bitvector_of_nat … (S m).
1067 cases daemon.
1068qed.
1069
1071  ∀n,p,q:nat.
1072    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
1073
1075  ∀n, m: nat.
1076    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
1077      bitvector_of_nat n (S m).
1079qed.
1080
1082  ∀n,v,m1,m2.
1083    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 →
1084      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤
1085      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
1086
1088  ∀n,v,m1,m2.
1089    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
1090      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
1091      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
1092#n #v #m1 #m2 #m2_ok #bounded #H
1093lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
1094#K @(transitive_le … (K H))
1095cases daemon (*CSC: TRUE, complete*)
1096qed.
1097
1098definition sign_bit : ∀n. BitVector n → bool ≝
1099λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
1100
1101definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
1102λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
1103
1104definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
1105λm,n.
1106  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
1107  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
1108  | nat_eq n' ⇒ λv. v
1109  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
1110  ].
1111
1112definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
1113λm,n.
1114  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
1115  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
1116  | nat_eq n' ⇒ λv. v
1117  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
1118  ].
1119
1120example sub_minus_one_seven_eight:
1121  ∀v: BitVector 7.
1122  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
1123  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
1124 cases daemon.
1125qed.
1126
1127axiom sub16_with_carry_overflow:
1128  ∀left, right, result: BitVector 16.
1129  ∀flags: BitVector 3.
1130  ∀upper: BitVector 9.
1131  ∀lower: BitVector 7.
1132    sub_16_with_carry left right false = 〈result, flags〉 →
1133      vsplit bool 9 7 result = 〈upper, lower〉 →
1134        get_index_v bool 3 flags 2 ? = true →
1135          upper = [[true; true; true; true; true; true; true; true; true]].
1136  //
1137qed.
1138