Ignore:
Timestamp:
Feb 22, 2011, 11:35:16 AM (9 years ago)
Author:
campbell
Message:

Use bit vector operations widely instead of round-trips through Z.
Implement more efficient addition, subtraction and comparison on bit vectors.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Integers.ma

    r547 r582  
    131131
    132132definition eq : int → int → bool ≝ eq_bv wordsize.
    133 definition lt : int → int → bool ≝ λx,y:int.
    134   if Zltb (signed x) (signed y) then true else false.
    135 definition ltu : int → int → bool ≝ λx,y: int.
    136   if Zltb (unsigned x) (unsigned y) then true else false.
    137 
    138 definition neg : int → int ≝ λx. repr (- unsigned x).
     133definition lt : int → int → bool ≝ lt_s wordsize.
     134definition ltu : int → int → bool ≝ lt_u wordsize.
     135
     136definition neg : int → int ≝ negation_bv wordsize.
    139137
    140138let rec zero_ext (n:Z) (x:int) on x : int ≝
     
    145143        if Zltb y (two_p (n-1)) then y else y - p).
    146144
    147 definition add ≝ λx,y: int.
    148   repr (unsigned x + unsigned y).
    149 definition sub ≝ λx,y: int.
    150   repr (unsigned x - unsigned y).
    151 definition mul ≝ λx,y: int.
    152   repr (unsigned x * unsigned y).
     145definition add ≝ addition_n wordsize.
     146definition sub ≝ subtraction wordsize.
     147definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)).
    153148definition Zdiv_round : Z → Z → Z ≝ λx,y: Z.
    154149  if Zltb x 0 then
     
    218213  repr (Z_of_bits wordsize (λi. f (fx i) (fy i))).
    219214
    220 definition i_and : int → int → int ≝ λx,y. bitwise_binop andb x y.
    221 definition or : int → int → int ≝ λx,y. bitwise_binop orb x y.
    222 definition xor : int → int → int ≝ λx,y. bitwise_binop xorb x y.
    223 
    224 definition not : int → int ≝ λx.xor x mone.
     215definition i_and : int → int → int ≝ conjunction_bv wordsize.
     216definition or : int → int → int ≝ inclusive_disjunction_bv wordsize.
     217definition xor : int → int → int ≝ exclusive_disjunction_bv wordsize.
     218
     219definition not : int → int ≝ negation_bv wordsize.
    225220
    226221(* * Shifts and rotates. *)
     
    490485Qed.
    491486*)
    492 axiom one_not_zero: one ≠ zero.
     487theorem one_not_zero: one ≠ zero.
     488% #H
     489lapply (refl ? (get_index' ? 31 0 one))
     490>H in ⊢ (???% → ?)
     491normalize #E destruct
     492qed.
     493
    493494(*
    494 Theorem one_not_zero: one <> zero.
    495 Proof.
    496   assert (unsigned one <> unsigned zero).
    497   rewrite unsigned_one; rewrite unsigned_zero; congruence.
    498   congruence.
    499 Qed.
    500 
    501495Theorem unsigned_repr_wordsize:
    502496  unsigned iwordsize = Z_of_nat wordsize.
Note: See TracChangeset for help on using the changeset viewer.