Changeset 697 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Mar 18, 2011, 1:28:33 PM (9 years ago)
Author:
campbell
Message:

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

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM

  • src/ASM/Arithmetic.ma

    r690 r697  
    88      | true ⇒ S O
    99      ].
     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.
    1043   
    1144definition add_n_with_carry:
    12       ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
     45      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. n ≥ 5 →
     46      (BitVector n) × (BitVector 3) ≝
    1347  λn: nat.
    1448  λb: BitVector n.
    1549  λc: BitVector n.
    1650  λ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 
    33 definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
     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) ≝
    3463  λn: nat.
    3564  λb: BitVector n.
    3665  λc: BitVector n.
    3766  λ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          
     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
    5377definition add_8_with_carry ≝ add_n_with_carry 8.
    5478definition add_16_with_carry ≝ add_n_with_carry 16.
     
    5983  λn: nat.
    6084  λ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         ].
     85    \fst (add_with_carries n b (zero n) true).
    6786       
    6887definition decrement ≝
    6988  λn: nat.
    7089  λ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         ].
     90    \fst (sub_with_borrows n b (zero n) true).
    7691   
    7792definition two_complement_negation ≝
     
    8499  λn: nat.
    85100  λb, c: BitVector n.
    86     let 〈res,flags〉 ≝ add_n_with_carry n b c false in
     101    let 〈res,flags〉 ≝ add_with_carries n b c false in
    87102      res.
    88103   
     
    111126        Some ? (bitvector_of_nat n result)
    112127    ].
    113    
    114 alias id "option1" = "cic:/matita/basics/sums/option.ind(1,0,1)".
    115      
    116 definition division_s: ∀n. ∀b, c: BitVector n. option1 (BitVector n) ≝
     128     
     129definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
    117130  λn.
    118131    match n with
     
    156169    let b_nat ≝ nat_of_bitvector ? b in
    157170    let c_nat ≝ nat_of_bitvector ? c in
    158     let result ≝ modulus b_nat c_nat in
    159       bitvector_of_nat (n + n) result.
     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    ].
    160177           
    161178definition modulus_s ≝
     
    170187     
    171188definition 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.
     189  fold_right2_i ???
     190    (λ_.λa,b,r.
     191      match a with
     192      [ true ⇒ b ∧ r
     193      | false ⇒ b ∨ r
     194      ])
     195    false.
    177196     
    178197definition gt_u ≝ λn, b, c. lt_u n c b.
     
    181200
    182201definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
    183      
     202
    184203definition lt_s ≝
    185204  λn.
    186205  λ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   //
    198 qed.
    199 
     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   
    200220definition gt_s ≝ λn,b,c. lt_s n c b.
    201221
Note: See TracChangeset for help on using the changeset viewer.