Changeset 535


Ignore:
Timestamp:
Feb 16, 2011, 4:25:02 PM (6 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
Location:
Deliverables/D3.1/C-semantics
Files:
6 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
  • Deliverables/D3.1/C-semantics/Smallstep.ma

    r487 r535  
    8787    [ @(t'⧺t2)
    8888    | //
    89     | <(Eapp_assoc …) //;
     89    | <(Eapp_assoc …) <H2 @H5
    9090    ]
    9191]
     
    104104  star tr ge s1 t s3.
    105105#tr #ge #s1 #t1 #s2 #t2 #s3 #t #H1 #H2 #H3
    106 @(star_trans … H1 … (star_one … H2)) //;
     106@(star_trans … H1 … (star_one … H2)) @H3
    107107qed.
    108108
     
    124124  ∀tr,ge,s1,t,s2. plus tr ge s1 t s2 -> star tr ge s1 t s2.
    125125#tr #ge #s1 #t #s2 #H elim H; #s1' #t1' #s2' #t2' #s3' #t3' #H1 #H2 #e1
    126 @(star_step … H1 H2 …) //;
     126@(star_step … H1 H2 …) @e1;
    127127qed.
    128128
     
    216216  forever tr ge s1 (t ⧻ T).
    217217#tr #ge #s1 #t1 #s2 #H elim H;
    218 [ #s' #T #H2 //;
     218[ #s' #T #H2 @H2
    219219| #s1' #t1 #s0 #t0 #s2' #t2' #H1 #H2 #e1 #IH #T #H3
    220220    >e1 >(Eappinf_assoc …)
     
    551551    elim (IH ? B); #st3' *; #C #D
    552552    %{ st3'} % //;
    553     @(star_trans ??? tA st2' ? tB) //;
    554     elim A; /2/; *; //;
     553    @(star_trans ??? tA st2' ? tB ?? C Ht)
     554    elim A /2/ * //
    555555] qed.
    556556
  • Deliverables/D3.1/C-semantics/cerco/BitVector.ma

    r475 r535  
    123123        false) b c.
    124124
     125lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.
     126  (x = y → P true) →
     127  (x ≠ y → P false) →
     128  P (eq_bv n x y).
     129#P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf)
     130#Q * *; normalize /3/
     131qed.
     132
    125133let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
    126134  let biglist ≝ rev ? (bitvector_of_nat_aux m m) in
  • Deliverables/D3.1/C-semantics/cerco/Util.ma

    r534 r535  
    1313  ].
    1414   
     15(*
    1516notation "hvbox('if' b 'then' t 'else' f)"
    1617  non associative with precedence 83
    1718  for @{ 'if_then_else $b $t $f }.
     19*)
     20notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
     21notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
    1822
    1923interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
  • Deliverables/D3.1/C-semantics/cerco/Vector.ma

    r534 r535  
    1212include "arithmetics/nat.ma".
    1313
     14include "oldlib/eq.ma".
    1415
    1516(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    319320(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    320321
    321 let rec reverse (A: Type[0]) (n: nat)
    322                  (v: Vector A n) on v ≝
    323   match v return (λm.λv. Vector A m) with
    324     [ VEmpty ⇒ [[ ]]
    325     | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]])
    326     ].
    327     //
    328 qed.
     322(* At some points matita will attempt to reduce reverse with a known vector,
     323   which reduces the equality proof for the cast.  Normalising this proof needs
     324   to be fast enough to keep matita usable. *)
     325let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
     326match n return λn'.∀m.S(n'+m) = n'+S m with
     327[ O ⇒ λm.refl ??
     328| S n' ⇒ λm. ?
     329]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.
     330
     331let rec revapp (A: Type[0]) (n: nat) (m:nat)
     332                (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
     333  match v return λn'.λ_. Vector A (n' + m) with
     334    [ VEmpty ⇒ acc
     335    | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
     336    ].
     337> plus_n_Sm_fast @refl qed.
     338
     339let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
     340  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
     341< plus_n_O @refl qed.
    329342
    330343(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    436449qed.
    437450
     451lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n.
     452  match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with
     453  [ O ⇒ λP.λv.P [[ ]] → P v
     454  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
     455  ] P v.
     456@(λA,n. λP:Vector A n → Prop. λv. match v return
     457?
     458with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P)
     459[ // | // ] qed.
     460(* XXX Proof below fails at qed.
     461#A #n #P * [ #H @H | #m #h #t #H @H ] qed.
     462*)
     463
     464lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
     465  (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
     466  ∀n,x,y.
     467  (x = y → P true) →
     468  (x ≠ y → P false) →
     469  P (eq_v A n f x y).
     470#P #A #f #f_elim #n #x elim x
     471[ #y @(vector_inv_n … y)
     472  normalize /2/
     473| #m #h #t #IH #y @(vector_inv_n … y)
     474  #h' #t' #Ht #Hf whd in ⊢ (?%)
     475  @(f_elim ? h h') #Eh
     476  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
     477  | @Hf % #E' destruct (E') elim Eh /2/
     478  ]
     479] qed.
     480
    438481(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    439482(* Subvectors.                                                                *)
  • Deliverables/D3.1/C-semantics/extralib.ma

    r487 r535  
    331331].
    332332interpretation "integer multiplication" 'times x y = (Z_times x y).
    333 
     333(* Now in cerco/Util.ma
    334334(* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
    335335notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
    336336notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
    337337interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
    338 
     338*)
    339339(* datatypes/list.ma *)
    340340
Note: See TracChangeset for help on using the changeset viewer.