Changeset 462


Ignore:
Timestamp:
Jan 20, 2011, 1:32:32 PM (6 years ago)
Author:
mulligan
Message:

Added bitvector arithmetic for Brian.

Location:
Deliverables/D4.1/Matita
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Arithmetic.ma

    r374 r462  
    3131                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
    3232
    33 ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (BitVector three) ≝
    34   λb: BitVector eight.
    35   λc: BitVector eight.
     33ndefinition sub_n_with_carry: ∀n: Nat. ∀b,c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝
     34  λn: Nat.
     35  λb: BitVector n.
     36  λc: BitVector n.
    3637  λcarry: Bool.
    37     let b_as_nat ≝ nat_of_bitvector eight b in
    38     let c_as_nat ≝ nat_of_bitvector eight c in
    39     let carry_as_nat ≝ nat_of_bool carry in
    40     let temporary ≝ b_as_nat mod sixteen - c_as_nat mod sixteen in
    41     let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≲ (c_as_nat mod sixteen)) (temporary ≲ carry_as_nat)) in
    42     let bit_six ≝ negation (conjunction ((b_as_nat mod one_hundred_and_twenty_eight) ≲ (c_as_nat mod one_hundred_and_twenty_eight)) (temporary ≲ carry_as_nat)) in
    43     let old_result_1 ≝ b_as_nat - c_as_nat in
    44     let old_result_2 ≝ old_result_1 - carry_as_nat in
    45     let ov_flag ≝ exclusive_disjunction carry bit_six in
    46       match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with
    47         [ false ⇒
    48            let cy_flag ≝ false in
    49             〈 bitvector_of_nat eight old_result_2, [[ cy_flag ; ac_flag ; ov_flag ]]〉
    50         | true ⇒
    51            let cy_flag ≝ true in
    52            let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in
    53             〈 bitvector_of_nat eight new_result, [[ cy_flag ; ac_flag ; ov_flag ]]〉
    54         ].
     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 (two * n)) - (c_as_nat mod (two * n)) in
     42     let ac_flag ≝ less_than_b (b_as_nat mod (two * n)) ((c_as_nat mod (two * n)) + carry_as_nat) in
     43     let bit_six ≝ less_than_b (b_as_nat mod (two^(n - one))) ((c_as_nat mod (two^(n - one))) + carry_as_nat) in
     44     let 〈b',cy_flag〉 ≝
     45       if greater_than_or_equal_b b_as_nat (c_as_nat + carry_as_nat) then
     46         〈b_as_nat, false〉
     47       else
     48         〈b_as_nat + (two^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 ]]〉.         
    5552         
    5653ndefinition add_8_with_carry ≝ add_n_with_carry eight.
    5754ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
     55ndefinition sub_8_with_carry ≝ sub_n_with_carry eight.
     56ndefinition sub_16_with_carry ≝ sub_n_with_carry sixteen.
    5857
    5958ndefinition increment ≝
     
    7574        | S o ⇒ bitvector_of_nat n o
    7675        ].
    77        
     76   
     77ndefinition 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   
     83ndefinition addition_n ≝
     84  λn: Nat.
     85  λb, c: BitVector n.
     86    let 〈res,flags〉 ≝ add_n_with_carry n b c false in
     87      res.
     88   
     89ndefinition subtraction ≝
     90  λn: Nat.
     91  λb, c: BitVector n.
     92    addition_n n b (two_complement_negation n c).
     93   
     94ndefinition 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     
     102ndefinition 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    [ Z ⇒ Nothing ?
     109    | _ ⇒
     110      let result ≝ b_nat ÷ c_nat in
     111        Just ? (bitvector_of_nat n result)
     112    ].
     113     
     114ndefinition division_s: ∀n. ∀b, c: BitVector n. Maybe (BitVector n) ≝
     115  λn.
     116    match n with
     117    [ Z ⇒ λb, c. Nothing ?
     118    | S p ⇒ λb, c: BitVector (S p).
     119        let b_sign_bit ≝ get_index_v ? ? b Z ? in
     120        let c_sign_bit ≝ get_index_v ? ? c Z ? 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        [ Z ⇒ Nothing ?
     125        | S o ⇒
     126          match b_sign_bit with
     127          [ true ⇒
     128            let temp_b ≝ (b_as_nat - (two^((S p)-one))) in
     129            match c_sign_bit with
     130            [ true ⇒
     131              let temp_c ≝ (c_as_nat - (two^((S p)-one))) in
     132                Just ? (bitvector_of_nat ? (temp_b ÷ temp_c))
     133            | false ⇒
     134              let result ≝ (temp_b ÷ c_as_nat) + (two^((S p)-one)) in
     135                Just ? (bitvector_of_nat ? result)
     136            ]
     137          | false ⇒
     138            match c_sign_bit with
     139            [ true ⇒
     140              let temp_c ≝ (c_as_nat - (two^((S p)-one))) in
     141              let result ≝ (b_as_nat ÷ temp_c) + (two^((S p)-one)) in
     142                Just ? (bitvector_of_nat ? result)
     143            | false ⇒ Just ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
     144            ]
     145          ]
     146        ]
     147    ].
     148    //;
     149nqed.
     150
     151ndefinition 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           
     159ndefinition modulus_s ≝
     160  λn.
     161  λb, c: BitVector n.
     162    match division_s n b c with
     163      [ Nothing ⇒ Nothing ?
     164      | Just result ⇒
     165          let 〈high_bits, low_bits〉 ≝ split Bool ? n (multiplication n result c) in
     166            Just ? (subtraction n b low_bits)
     167      ].
     168     
     169ndefinition 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      less_than_b b_nat c_nat.
     175     
     176ndefinition gt_u ≝ λn, b, c. lt_u n c b.
     177
     178ndefinition lte_u ≝ λn, b, c. negation (gt_u n b c).
     179
     180ndefinition gte_u ≝ λn, b, c. negation (lt_u n b c).
     181     
     182ndefinition 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 two ? in
     187     if ov_flag then
     188       true
     189     else
     190       ((match n return λn'.BitVector n' → Bool with
     191       [ Z ⇒ λ_.false
     192       | S o ⇒
     193         λresult'.(get_index_v ? ? result' Z ?)
     194       ]) result).
     195      //;
     196nqed.
     197
     198ndefinition gt_s ≝ λn,b,c. lt_s n c b.
     199
     200ndefinition lte_s ≝ λn,b,c. negation (gt_s n b c).
     201
     202ndefinition gte_s ≝ λn. λb, c.
     203  negation (lt_s n b c).
     204     
    78205alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop".
    79206
  • Deliverables/D4.1/Matita/BitVectorTrie.ma

    r374 r462  
    2626             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
    2727             ]
    28         | Stub s ⇒ λ_. a
    29         ]
     28        | Stub s ⇒ λ_. afg        ]
    3029    ]) (refl ? n).
    3130 ##[##1,2: ndestruct |##*: napply S_inj; //]
  • Deliverables/D4.1/Matita/depends

    r439 r462  
    77Either.ma Bool.ma
    88DoTest.ma Assembly.ma Interpret.ma Test.ma
     9Debug.ma Interpret.ma Status.ma
    910ASM.ma BitVector.ma Either.ma String.ma
    1011Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
Note: See TracChangeset for help on using the changeset viewer.