Changeset 14 for C-semantics


Ignore:
Timestamp:
Jul 21, 2010, 3:08:58 PM (10 years ago)
Author:
campbell
Message:

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

Location:
C-semantics
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Integers.ma

    r10 r14  
    8888  integer (type [Z]) plus a proof that it is in the range 0 (included) to
    8989  [modulus] (excluded. *)
    90 
    91 nrecord int: Type ≝ { intval: Z ; intrange: True (*(0 ≤ intval) ∧ intval < modulus*) }.
     90(* XXX: hack to prevent normalization of huge proof term. *)
     91ninductive inrange : Z → Prop ≝
     92| inrg_mod : ∀i:Z. inrange (i \mod modulus)
     93| inrg_pf : ∀i:Z. (0 ≤ i) ∧ i < modulus → inrange i.
     94ninductive int: Type ≝
     95| mk_int: ∀i:Z. inrange i → int.
     96(*
     97nrecord int: Type ≝ { intval: Z ; intrange: (0 ≤ intval) ∧ intval < modulus }.
     98*)
     99ndefinition intval: int → Z ≝ λi.match i with [ mk_int x _ ⇒ x ].
     100ndefinition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus.
     101#i;ncases i;
     102#x H; ncases H;
     103##[ #x'; napply modZ_lt_mod; //;
     104##| //;
     105##] nqed.
    92106
    93107(* The [unsigned] and [signed] functions return the Coq integer corresponding
     
    104118(* Conversely, [repr] takes a Coq integer and returns the corresponding
    105119  machine integer.  The argument is treated modulo [modulus]. *)
    106 (* TODO: prove *)
    107120(*naxiom repr : Z → int.*)
    108 
    109 (*naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus.*)
    110 
     121(*
    111122ndefinition repr : Z → int := λx.
    112   mk_int x I (*x \mod modulus) ?*) (*Z_mod_lt x modulus modulus_pos*).
    113 (*napply repr_ax.
    114 nqed.*)
     123  mk_int (x \mod modulus) (modZ_lt_mod x modulus modulus_pos).
     124*)
     125ndefinition repr : Z → int ≝ λx. mk_int (x \mod modulus) (inrg_mod x).
    115126
    116127ndefinition zero := repr 0.
     
    145156ndefinition neg : int → int ≝ λx. repr (- unsigned x).
    146157
    147 naxiom zero_ext : Z → int → int.
    148 naxiom sign_ext : Z → int → int.
    149 (*
    150 Definition zero_ext (n: Z) (x: int) : int :=
    151   repr (Zmod (unsigned x) (two_p n)).
    152 Definition sign_ext (n: Z) (x: int) : int :=
    153   repr (let p := two_p n in
    154         let y := Zmod (unsigned x) p in
    155         if zlt y (two_p (n-1)) then y else y - p).
    156 *)
     158ndefinition zero_ext : Z → int → int ≝
     159λn,x. repr (modZ (unsigned x) (two_p n)).
     160ndefinition sign_ext : Z → int → int ≝
     161λn,x. repr (let p ≝ two_p n in
     162        let y ≝ modZ (unsigned x) p in
     163        if Zltb y (two_p (n-1)) then y else y - p).
     164
    157165ndefinition add ≝ λx,y: int.
    158166  repr (unsigned x + unsigned y).
     
    254262  (standard behaviour for arithmetic right shift) and
    255263  [shrx] rounds towards zero. *)
    256 naxiom two_p : Z → Z.
     264
    257265ndefinition shr : int → int → int ≝ λx,y.
    258266  repr (signed x / two_p (unsigned y)).
  • C-semantics/Mem.ma

    r10 r14  
    17011701##| #ineq; @1; @1; napply ineq;
    17021702##] nqed.
    1703 (*  XXX: reenable once I've sorted out performance a bit
     1703
     1704(* XXX: use Or rather than ∨ to bring resource usage under control. *)
    17041705ndefinition meminj_no_overlap ≝ λmi: meminj. λm: mem.
    17051706  ∀b1,b1',delta1,b2,b2',delta2.
     
    17071708  mi b1 = Some ? 〈b1', delta1〉 →
    17081709  mi b2 = Some ? 〈b2', delta2〉 →
    1709   b1' ≠ b2'
    1710   ∨ low_bound m b1 ≥ high_bound m b1
    1711   ∨ low_bound m b2 ≥ high_bound m b2
    1712   ∨ (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2
    1713   ∨ high_bound m b2 + delta2 ≤ low_bound m b1 + delta1).
     1710  Or (Or (Or (b1' ≠ b2')
     1711             (low_bound m b1 ≥ high_bound m b1))
     1712         (low_bound m b2 ≥ high_bound m b2))
     1713  (Or (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2)
     1714      (high_bound m b2 + delta2 ≤ low_bound m b1 + delta1)).
    17141715
    17151716(* FIXME *)
     
    22202221##| ##3: nwhd in ⊢ (??%?); //
    22212222##| ##4,5: //;
    2222 ##| ##6: nwhd; #chunk;#_; nwhd; @ O; //;
     2223##| ##6: nwhd; #chunk;#_; ncases chunk;//;
    22232224##] nqed.
    22242225
     
    23532354    nrewrite > (?:repr O = zero); ##[ ##2: // ##]
    23542355    nrewrite > (add_zero ?);
     2356    nrewrite > (Zplus_z_OZ …);
    23552357    //;
    23562358##| (* delta ≠ 0 *)
     
    23872389##] nqed.
    23882390
     2391(* XXX: should use ndestruct, but reduces large definitions *)
     2392nremark vptr_eq: ∀b,b',i,i'. Vptr b i = Vptr b' i' → b = b' ∧ i = i'.
     2393#b b' i i' e; ndestruct; /2/; nqed.
     2394
    23892395nlemma valid_pointer_inject:
    23902396  ∀f,m1,m2,b,ofs,b',ofs'.
     
    23972403##[ ##1,2,4: #x;#H;ndestruct; ##]
    23982404#b0;#i;#b0';#i';#delta;#Hb;#Hi';#eptr;#eptr';
    2399 (* FIXME want ndestruct to sort this out, but get assertion failure *)
    2400   nrewrite > (?:b0 = b) in Hb; ##[ ##2: ndestruct; // ##]
    2401   nrewrite > (?:b0' = b'); ##[ ##2: ndestruct; // ##]
    2402   nrewrite > (?:i = ofs) in Hi'; ##[ ##2: ndestruct; // ##]
    2403   nrewrite > (?:i' = ofs'); ##[ ##2: ndestruct; // ##]
     2405nrewrite < (proj1 … (vptr_eq ???? eptr)) in Hb; nrewrite < (proj1 … (vptr_eq ???? eptr'));
     2406nrewrite < (proj2 … (vptr_eq ???? eptr)) in Hi'; nrewrite < (proj2 … (vptr_eq ???? eptr'));
    24042407  #Hofs; #Hbinj;
    24052408nrewrite > Hofs;
     
    25102513  ##| ncases chunk'; #v;#_;#_; @4;
    25112514  ##]
    2512 (* FIXME: the next two cases are the same *)
     2515(* FIXME: the next two cases are very similar *)
    25132516##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
    2514     nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
    2515     ##[ ##2,4: nrewrite > Hz; @
    2516     ##| ##1,3: nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize;
     2517    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize;
     2518    ##[ ##3,4,5,6,7,10,11,12,13,14: napply False_ind; ndestruct;
     2519    ##| ##2,9: nwhd in ⊢ (??%%); nrewrite > Hz; @
     2520    ##| ##1,8: nwhd in ⊢ (??%%);
     2521        (* XXX: applying the rewrite directly fails with a unification error,
     2522           but establishing the equality then using napplyS works! *)
     2523        nlapply (sign_ext_equal_if_zero_equal … Hz);
     2524        ##[ ##1,3: @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
     2525        ##| ##2,4: #H; napplyS val_inject_int;
     2526        ##]
     2527        (* original version:
     2528        nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize;
    25172529        ##[ ##1,3: napply I ##| ##2,4: napply leb_true_to_le; @; ##]
     2530        *)
    25182531    ##]
    25192532
    25202533##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
    2521     nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
    2522     ##[ ##2,4: nrewrite > Hz; @
    2523     ##| ##1,3: nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize;
    2524         ##[ ##1,3: napply I ##| ##2,4: napply leb_true_to_le; @; ##]
     2534    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize;
     2535    ##[ ##1,2,5,6,7,8,9,12,13,14: napply False_ind; ndestruct;
     2536    ##| ##4,11: nwhd in ⊢ (??%%); nrewrite > Hz; @
     2537    ##| ##3,10: nwhd in ⊢ (??%%);
     2538        (* XXX: actually, napplyS doesn't complete in a reasonable time here;
     2539                but rewriting on one goal at a time giving the exact position
     2540                does! *)
     2541        ##[ nrewrite > (sign_ext_equal_if_zero_equal … Hz) in ⊢ (??(?%)?); @;
     2542          ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
     2543        ##|  nrewrite > (sign_ext_equal_if_zero_equal … Hz) in ⊢ (??(?%)?); @;
     2544          ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
     2545        ##]
    25252546    ##]
    25262547
     
    29202941#Hminj;#ALLOC1;#ALLOC2;#Hlo;#Hhi;
    29212942napply (alloc_mapped_inject … ALLOC1); /2/;
    2922 ##[ nlapply (alloc_right_inject … Hminj ALLOC2); //;
    2923 ##| (* TODO: add to integers *) napply daemon
     2943##[ napply (alloc_right_inject … Hminj ALLOC2);
    29242944##| nrewrite > (low_bound_alloc_same … ALLOC2); //
    29252945##| nrewrite > (high_bound_alloc_same … ALLOC2); //
     
    31353155ncut (f b = Some ? delta);
    31363156##[ nwhd in INJb':(??%?); ncases (f b) in INJb' ⊢ %;
    3137   ##[ #H; ndestruct; ##| #delta'; #H; nelim (grumpydestruct2 ?????? H); // ##]
     3157  ##[ #H; napply (False_ind … (grumpydestruct … H)); ##| #delta'; #H; nelim (grumpydestruct2 ?????? H); // ##]
    31383158##] #INJb;
    31393159nlapply (valid_pointer_shift_no_overflow … VALID INJb); //; #NOOV;
     
    31713191nlapply INJb1; nwhd in ⊢ (??%? → ?);
    31723192nlapply (refl ? (f b1)); ncases (f b1) in ⊢ (???% → %);
    3173 ##[ #_; nwhd in ⊢ (??%? → ?); #H; napply False_ind; ndestruct;
     3193##[ #_; nwhd in ⊢ (??%? → ?); #H; napply False_ind; napply (False_ind … (grumpydestruct … H));
    31743194##| #delta'; #DELTA; nwhd in ⊢ (??%? → ?); #H; nelim (grumpydestruct2 ?????? H);
    31753195    #eb;#edelta;
     
    34353455##]
    34363456nqed.
    3437 *)
     3457
    34383458(* ** Relation between signed and unsigned loads and stores *)
    34393459
     
    34863506nelim (in_bounds m Mint8unsigned b (signed ofs)); /2/;
    34873507#H; nwhd in ⊢ (??%%);
    3488 nelim (getN 0 (signed ofs) (contents (blocks m b))); //;
    3489 #i; nwhd in ⊢ (??(??%)(??%)); nrewrite > (sign_ext_zero_ext …); //;
    3490 (* arith *) napply daemon;
    3491 nqed.
     3508nelim (getN 0 (signed ofs) (contents (blocks m b)));
     3509##[ ##1,3,4: //;
     3510##| #i; nwhd in ⊢ (??(??%)(??%));
     3511     (* XXX: need to specify which side of the equality to rewrite on to avoid
     3512             a unification assertion. *)
     3513    nrewrite > (sign_ext_zero_ext ?? i) in ⊢ (???%); ##[ napply refl; (* XXX: // ? *)
     3514    ##| (* arith *) napply daemon;
     3515    ##]
     3516##]
     3517nqed.
  • C-semantics/README

    r12 r14  
    4848No unfold tactic yet; use reduction or rewriting instead.
    4949
    50 ndestruct often takes too long; getting rid of irrelevant information (e.g.,
    51 replacing the goal with False) sometimes helps, or an extra lemma can be used.
     50Normalization of term containing large definitions (such as some of the
     51Integers library) can be prohibitive.  This is a particular problem because
     52ndestruct currently normalizes the goal and every hypothesis that is rewritten.
     53For ndestruct, getting rid of irrelevant information (e.g., replacing the goal
     54with False) sometimes helps, or an extra lemma can be used.
    5255
    5356Some of the pattern matching in the C syntax has had to be unfolded in
     
    6063The lack of sections has been replaced by duplicating the variables in some
    6164places, and adding a record in others.
     65
     66The meminj_no_overlap definition in Mem.ma uses the logical Or explicitly
     67rather than the ∨ notation to regain reasonable performance. (This is
     68presumably due to disambiguation - the notation is also used for booleans.)
     69
     70There are a couple of places in Mem.ma where rewriting had to be done carefully
     71to avoid assertions during unification; I'm not really sure what the problem
     72is.
    6273
    6374Detail per-file
     
    115126Mem.ma
    116127
    117   Everything except for omega in proofs.  Much of the transformations sections
    118   are commented out until Integers.ma is done properly.
     128  Everything except for omega in proofs.
    119129
    120130Smallstep.ma
  • C-semantics/Values.ma

    r3 r14  
    10071007  ∀chunk,v1,v2.
    10081008  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    1009 #chunk;#v1;#v2;#H; ninversion H; //; ncases chunk; nnormalize; //;
     1009#chunk;#v1;#v2;#H; ninversion H; //; #v e1 e2; ncases chunk; nwhd in ⊢ (?%?); //;
    10101010nqed.
    10111011
  • C-semantics/extralib.ma

    r11 r14  
    649649    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
    650650    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
    651                 match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
     651                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
    652652    ]
    653653  | neg n ⇒
     
    655655    [ OZ ⇒ OZ
    656656    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
    657                 match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
     657                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
    658658    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
    659659    ]
     
    664664interpretation "integer division" 'divide m n = (divZ m n).
    665665interpretation "integer modulus" 'module m n = (modZ m n).
     666
     667nlemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
     668#x y; ncases y;
     669##[ #H; napply (False_ind … H);
     670##| #m; #_; ncases x; //; #n;
     671    nwhd in ⊢ (?%?);
     672    nlapply (pos_compare_to_Prop n m);
     673    ncases (pos_compare n m); /2/;
     674    #lt; nwhd; nrewrite < (minus_Sn_m … lt); /2/;
     675##| #m H; napply (False_ind … H);
     676##] nqed.
     677
     678nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
     679#n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m);
     680##[ //;
     681##| ##2,3: #H; napply False_ind; napply (absurd ? lt ?); /3/;
     682##] nqed.
     683
     684ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
     685#x y; ncases y;
     686##[ #H; napply (False_ind … H);
     687##| #m; #_; ncases x;
     688  ##[ @;//;
     689  ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
     690      ncases (divide n m) in ⊢ (???% → %); #dv md H;
     691      nelim (divide_ok … H); #e l; nelim l; /2/;
     692  ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
     693      ncases (divide n m) in ⊢ (???% → %); #dv md H;
     694      nelim (divide_ok … H); #e l; nelim l;
     695      ##[ /2/;
     696      ##| #md' m' l'; @;
     697        ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …);
     698            nrewrite > (pos_compare_lt … l'); //;
     699        ##| /2/;
     700        ##]
     701      ##]
     702  ##]
     703##| #m H; napply (False_ind … H);
     704##] nqed.
Note: See TracChangeset for help on using the changeset viewer.