Changeset 744 for src/common/Integers.ma


Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (9 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Integers.ma

    r700 r744  
    1717
    1818include "arithmetics/nat.ma".
    19 include "utilities/binary/Z.ma".
    20 include "utilities/extralib.ma".
     19include "utilities/extranat.ma".
    2120
    2221include "ASM/BitVector.ma".
    23 include "ASM/BitVectorZ.ma".
    2422include "ASM/Arithmetic.ma".
    2523
     
    6866
    6967definition wordsize : nat ≝ 32.
     68(*
    7069definition modulus : Z ≝ Z_two_power_nat wordsize.
    7170definition half_modulus : Z ≝ modulus / 2.
     
    8584  modulus > 0.
    8685//; qed.
    87 
     86*)
    8887(* * Representation of machine integers *)
    8988
     
    9392
    9493definition int : Type[0] ≝ BitVector wordsize.
    95 
     94(*
    9695definition intval: int → Z ≝ Z_of_unsigned_bitvector ?.
    9796definition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus.
     
    111110  then unsigned n
    112111  else unsigned n - modulus.
    113 
     112*)
    114113(* Conversely, [repr] takes a Coq integer and returns the corresponding
    115114  machine integer.  The argument is treated modulo [modulus]. *)
    116 
     115(*
    117116definition repr : Z → int ≝ λz. bitvector_of_Z wordsize z.
     117*)
     118definition repr : nat → int ≝ λn. bitvector_of_nat wordsize n.
    118119
    119120definition zero := repr 0.
    120121definition one  := repr 1.
    121 definition mone := repr (-1).
    122 definition iwordsize := repr (Z_of_nat wordsize).
     122definition mone := subtraction ? zero one.
     123definition iwordsize := repr wordsize.
    123124
    124125lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y).
     
    135136
    136137definition neg : int → int ≝ two_complement_negation wordsize.
    137 
    138 let rec zero_ext (n:Z) (x:int) on x : int ≝
    139   repr (modZ (unsigned x) (two_p n)).
    140 let rec sign_ext (n:Z) (x:int) on x : int ≝
    141   repr (let p ≝ two_p n in
    142         let y ≝ modZ (unsigned x) p in
    143         if Zltb y (two_p (n-1)) then y else y - p).
    144 
    145 definition add ≝ addition_n wordsize.
    146 definition sub ≝ subtraction wordsize.
    147 (*definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)).*)
    148 definition mul ≝ λx,y. repr ((unsigned x) * (unsigned y)).
    149 definition Zdiv_round : Z → Z → Z ≝ λx,y: Z.
    150   if Zltb x 0 then
    151     if Zltb y 0 then (-x) / (-y) else - ((-x) / y)
    152   else
    153     if Zltb y 0 then -(x / (-y)) else x / y.
    154 
    155 definition Zmod_round : Z → Z → Z ≝ λx,y: Z.
    156   x - (Zdiv_round x y) * y.
    157 
    158 definition divs : int → int → int ≝ λx,y:int.
    159   repr (Zdiv_round (signed x) (signed y)).
    160 definition mods : int → int → int ≝ λx,y:int.
    161   repr (Zmod_round (signed x) (signed y)).
    162 definition divu : int → int → int ≝ λx,y.
    163   repr (unsigned x / unsigned y).
    164 definition modu : int → int → int ≝ λx,y.
    165   repr (unsigned x \mod unsigned y).
    166 
    167 (* * For bitwise operations, we need to convert between Coq integers [Z]
    168   and their bit-level representations.  Bit-level representations are
    169   represented as characteristic functions, that is, functions [f]
    170   of type [nat -> bool] such that [f i] is the value of the [i]-th bit
    171   of the number.  The values of characteristic functions for [i] greater
    172   than 32 are ignored. *)
    173 
    174 definition Z_shift_add ≝ λb: bool. λx: Z.
    175   if b then 2 * x + 1 else 2 * x.
    176 
    177 definition Z_bin_decomp : Z → bool × Z ≝
    178 λx.match x with
    179 [ OZ ⇒ 〈false, OZ〉
    180 | pos p ⇒
    181   match p with
    182   [ p1 q ⇒ 〈true, pos q〉
    183   | p0 q ⇒ 〈false, pos q〉
    184   | one ⇒ 〈true, OZ〉
    185   ]
    186 | neg p ⇒
    187   match p return λ_.bool × Z with
    188   [ p1 q ⇒ 〈true, Zpred (neg q)〉
    189   | p0 q ⇒ 〈false, neg q〉
    190   | one ⇒ 〈true, neg one〉
    191   ]
    192 ].
    193 
    194 let rec bits_of_Z (n:nat) (x:Z) on n : Z → bool ≝
    195 match n with
    196 [ O ⇒ λi:Z. false
    197 | S m ⇒
    198     match Z_bin_decomp x with [ pair b y ⇒
    199       let f ≝ bits_of_Z m y in
    200       λi:Z. if eqZb i 0 then b else f (Zpred i) ]
    201 ].
    202 
    203 let rec Z_of_bits (n:nat) (f:Z → bool) on n : Z ≝
    204 match n with
    205 [ O ⇒ OZ
    206 | S m ⇒ Z_shift_add (f OZ) (Z_of_bits m (λi. f (Zsucc i)))
    207 ].
     138definition mul ≝ λx,y. \snd (split ? wordsize wordsize (multiplication wordsize x y)).
     139
     140definition zero_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝
     141λw,n.
     142  match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with
     143  [ nat_lt n' w' ⇒ λi.
     144      let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in
     145      switch_bv_plus ??? (pad ?? l)
     146  | _ ⇒ λi.i
     147  ].
     148
     149definition zero_ext : nat → int → int ≝ zero_ext_n wordsize.
     150
     151definition sign_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝
     152λw,n.
     153  match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with
     154  [ nat_lt n' w' ⇒ λi.
     155      let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in
     156      switch_bv_plus ??? (pad_vector ? (match l with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ]) ?? l)
     157  | _ ⇒ λi.i
     158  ].
     159
     160definition sign_ext : nat → int → int ≝ sign_ext_n wordsize.
    208161
    209162(* * Bitwise logical ``and'', ``or'' and ``xor'' operations. *)
    210163
    211 definition bitwise_binop ≝ λf: bool -> bool -> bool. λx,y: int.
    212   let fx ≝ bits_of_Z wordsize (unsigned x) in
    213   let fy ≝ bits_of_Z wordsize (unsigned y) in
    214   repr (Z_of_bits wordsize (λi. f (fx i) (fy i))).
    215164
    216165definition i_and : int → int → int ≝ conjunction_bv wordsize.
     
    222171(* * Shifts and rotates. *)
    223172
    224 definition shl : int → int → int ≝ λx,y.
    225   let fx ≝ bits_of_Z wordsize (unsigned x) in
    226   let vy ≝ unsigned y in
    227   repr (Z_of_bits wordsize (λi. fx (i - vy))).
    228 
    229 definition shru : int → int → int ≝ λx,y.
    230   let fx ≝ bits_of_Z wordsize (unsigned x) in
    231   let vy ≝ unsigned y in
    232   repr (Z_of_bits wordsize (λi. fx (i + vy))).
     173definition shl : int → int → int ≝ λx,y. shift_left ?? (nat_of_bitvector … y) x false.
     174definition shru : int → int → int ≝ λx,y. shift_right ?? (nat_of_bitvector … y) x false.
    233175
    234176(* * Arithmetic right shift is defined as signed division by a power of two.
     
    237179  [shrx] rounds towards zero. *)
    238180
    239 definition shr : int → int → int ≝ λx,y.
    240   repr (signed x / two_p (unsigned y)).
    241 
     181definition shr : int → int → int ≝ λx,y. shift_right ?? (nat_of_bitvector … y) x (head' … x).
    242182definition shrx : int → int → int ≝ λx,y.
    243   divs x (shl one y).
     183  match division_s ? x (shl one y) with [ None ⇒ zero | Some i ⇒ i ].
    244184
    245185definition shr_carry ≝ λx,y: int.
    246   sub (shrx x y) (shr x y).
    247 
    248 definition rol : int → int → int ≝ λx,y.
    249   let fx ≝ bits_of_Z wordsize (unsigned x) in
    250   let vy ≝ unsigned y in
    251   repr (Z_of_bits wordsize
    252          (λi. fx (i - vy \mod Z_of_nat wordsize))).
    253 
    254 definition ror : int → int → int ≝ λx,y.
    255   let fx := bits_of_Z wordsize (unsigned x) in
    256   let vy := unsigned y in
    257   repr (Z_of_bits wordsize
    258          (λi. fx (i + vy \mod Z_of_nat wordsize))).
     186  subtraction ? (shrx x y) (shr x y).
     187
     188definition rol : int → int → int ≝ λx,y. rotate_left ?? (nat_of_bitvector ? y) x.
     189definition ror : int → int → int ≝ λx,y. rotate_right ?? (nat_of_bitvector ? y) x.
    259190
    260191definition rolm ≝ λx,a,m: int. i_and (rol x a) m.
     
    487418*)
    488419theorem one_not_zero: one ≠ zero.
    489 % #H
    490 lapply (refl ? (get_index' ? 31 0 one))
    491 >H in ⊢ (???% → ?)
    492 normalize #E destruct
     420% #H @(match eq_dec one zero return λx.match x with [ inl _ ⇒ True | inr _ ⇒ False ] with [ inl _ ⇒ I | inr p ⇒ ?]) normalize
     421cases p #H' @(H' H)
    493422qed.
    494423
     
    705634Qed.
    706635*)
    707 
     636(*
    708637theorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus.
    709638#i @intrange
     
    27102639
    27112640
     2641*)
Note: See TracChangeset for help on using the changeset viewer.