Ignore:
Timestamp:
Feb 16, 2011, 4:25:02 PM (8 years ago)
Author:
campbell
Message:

Minimal integration of bitvectors into Clight semantics

  • does a "round trip" through Z for most operations (slow)
  • a few extra bits for equality on vectors
  • version of reverse that doesn't make matita fall over on size 32 vectors during disambiguation and automation
File:
1 edited

Legend:

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

    r487 r535  
    2020include "extralib.ma".
    2121
     22include "cerco/BitVector.ma".
     23include "cerco/BitVectorZ.ma".
     24include "cerco/Arithmetic.ma".
    2225
    2326(* * * Comparisons *)
     
    8891  integer (type [Z]) plus a proof that it is in the range 0 (included) to
    8992  [modulus] (excluded. *)
    90 (* XXX: hack to prevent normalization of huge proof term. *)
    91 inductive inrange : Z → Prop ≝
    92 | inrg_mod : ∀i:Z. inrange (i \mod modulus)
    93 | inrg_pf : ∀i:Z. (0 ≤ i) ∧ i < modulus → inrange i.
    94 inductive int: Type[0] ≝
    95 | mk_int: ∀i:Z. inrange i → int.
    96 (*
    97 record int: Type ≝ { intval: Z ; intrange: (0 ≤ intval) ∧ intval < modulus }.
    98 *)
    99 definition intval: int → Z ≝ λi.match i with [ mk_int x _ ⇒ x ].
     93
     94definition int : Type[0] ≝ BitVector wordsize.
     95
     96definition intval: int → Z ≝ Z_of_unsigned_bitvector ?.
    10097definition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus.
    101 #i cases i;
    102 #x #H cases H;
    103 [ #x' @modZ_lt_mod //;
    104 | //;
    105 ] qed.
     98#i % whd in ⊢ (?%%)
     99[ @Z_unsigned_min
     100| @Z_unsigned_max
     101] qed.
    106102
    107103(* The [unsigned] and [signed] functions return the Coq integer corresponding
     
    118114(* Conversely, [repr] takes a Coq integer and returns the corresponding
    119115  machine integer.  The argument is treated modulo [modulus]. *)
    120 (*axiom repr : Z → int.*)
    121 (*
    122 definition repr : Z → int := λx.
    123   mk_int (x \mod modulus) (modZ_lt_mod x modulus modulus_pos).
    124 *)
    125 definition repr : Z → int ≝ λx. mk_int (x \mod modulus) (inrg_mod x).
     116
     117definition repr : Z → int ≝ λz. bitvector_of_Z wordsize z.
    126118
    127119definition zero := repr 0.
     
    130122definition iwordsize := repr (Z_of_nat wordsize).
    131123
    132 axiom mk_int_eq:
    133   ∀x,y,Px,Py. x = y → mk_int x Px = mk_int y Py.
    134 (*Proof.
    135   intros. subst y.
    136   generalize (proof_irrelevance _ Px Py); intro.
    137   subst Py. reflexivity.
    138 Qed.*)
    139 
    140 axiom eq_dec: ∀x,y: int. (x = y) + (x ≠ y).
    141 (*Proof.
    142   intros. destruct x; destruct y. case (zeq intval0 intval1); intro.
    143   left. apply mkint_eq. auto.
    144   right. red; intro. injection H. exact n.
    145 Qed.*)
     124lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y).
     125#x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → ?) #E
     126[ %1 lapply E @(eq_bv_elim … x y) [ // | #_ #X destruct ]
     127| %2 lapply E @(eq_bv_elim … x y) [ #_ #X destruct | /2/ ]
     128] qed.
    146129
    147130(* * Arithmetic and logical operations over machine integers *)
    148131
    149 definition eq : int → int → bool ≝ λx,y: int.
    150   if eqZb (unsigned x) (unsigned y) then true else false.
     132definition eq : int → int → bool ≝ eq_bv wordsize.
    151133definition lt : int → int → bool ≝ λx,y:int.
    152134  if Zltb (signed x) (signed y) then true else false.
     
    207189  ]
    208190| neg p ⇒
    209   match p with
     191  match p return λ_.bool × Z with
    210192  [ p1 q ⇒ 〈true, Zpred (neg q)〉
    211193  | p0 q ⇒ 〈false, neg q〉
     
    528510theorem eq_sym:
    529511  ∀x,y. eq x y = eq y x.
    530 #x #y whd in ⊢ (??%%); @eqZb_elim #H
    531 [ >H >(eqZb_z_z …) //
    532 | >(eqZb_false … (sym_neq … H)) //
     512#x #y @eq_bv_elim @eq_bv_elim /2/
     513[ #NE #E @False_ind >E in NE * /2/
     514| #E #NE @False_ind >E in NE * /2/
    533515] qed.
    534516
    535517theorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y).
    536 #x #y whd in ⊢ (??%??); elim (eq_dec x y); #H
    537 [ >H >(eqZb_z_z …) //;
    538 | >(eqZb_false …) //;
    539     elim x in H ⊢ %; elim y;
    540     #x' #Px #y' #Py #H normalize; @(not_to_not … H) @mk_int_eq
    541 ] qed.
     518#x #y @eq_bv_elim #H @H qed.
    542519
    543520theorem eq_true: ∀x. eq x x = true.
     
    735712
    736713theorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus.
    737 #i cases i; #i' #H cases H; /2/;
     714#i @intrange
    738715qed.
    739716
Note: See TracChangeset for help on using the changeset viewer.