Changeset 15 for C-semantics


Ignore:
Timestamp:
Jul 22, 2010, 4:50:06 PM (10 years ago)
Author:
campbell
Message:

Make some definitions more normalization friendly by a little 'nlet rec'
abuse.

Location:
C-semantics
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Integers.ma

    r14 r15  
    156156ndefinition neg : int → int ≝ λx. repr (- unsigned x).
    157157
     158(*
    158159ndefinition zero_ext : Z → int → int ≝
    159160λn,x. repr (modZ (unsigned x) (two_p n)).
    160161ndefinition sign_ext : Z → int → int ≝
    161162λn,x. repr (let p ≝ two_p n in
     163        let y ≝ modZ (unsigned x) p in
     164        if Zltb y (two_p (n-1)) then y else y - p).
     165*)
     166nlet rec zero_ext (n:Z) (x:int) on x : int ≝
     167  repr (modZ (unsigned x) (two_p n)).
     168nlet rec sign_ext (n:Z) (x:int) on x : int ≝
     169  repr (let p ≝ two_p n in
    162170        let y ≝ modZ (unsigned x) p in
    163171        if Zltb y (two_p (n-1)) then y else y - p).
  • C-semantics/Mem.ma

    r14 r15  
    381381      ##|#Hl2;nwhd in ⊢ (??%?);nrewrite > (? : eqZb q p = false)
    382382         ##[nwhd in ⊢ (??%?);napply IH
    383             ##[//
     383            ##[napply Hl2
    384384            ##|(* Hr *) napply daemon ##]
    385385         ##|(*Hl2*)napply daemon ##]
     
    571571  at the given offset in the given block respects the bounds of the block. *)
    572572
    573 ndefinition in_bounds :
    574   ∀m:mem. ∀chunk:memory_chunk. ∀b:block. ∀ofs:Z.
    575     valid_access m chunk b ofs + (¬ valid_access m chunk b ofs).
    576 #m;#chunk;#b;#ofs;
     573(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
     574nlet rec in_bounds
     575  (m:mem) (chunk:memory_chunk) (b:block) (ofs:Z) on b : 
     576    Sum (valid_access m chunk b ofs) (Not (valid_access m chunk b ofs)) ≝ ?.
    577577napply (Zltb_elim_Type0 b (nextblock m)); #Hnext;
    578578##[ napply (Zleb_elim_Type0 (low_bound m b) ofs); #Hlo;
     
    637637  as a single value [addr], which must be a pointer value. *)
    638638
    639 ndefinition loadv : memory_chunk → mem → val → option val ≝
    640 λchunk,m,addr.
     639nlet rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    641640  match addr with
    642641  [ Vptr b ofs ⇒ load chunk m b (signed ofs)
     
    16741673ncut (load chunk0 m1 b1 ofs0 = Some ? v1);
    16751674##[ nrewrite < Hload; napply sym_eq; napply (load_store_other … Hstore);
    1676     @1;@1; napply nmk; #eq; nrewrite > eq in Hmi0; nrewrite > Hmi; (* XXX: fails to terminate in reasonable time  ndestruct;*) napply grumpydestruct;
     1675    @1;@1; napply nmk; #eq; nrewrite > eq in Hmi0; nrewrite > Hmi; #H; ndestruct;
    16771676##| #Hload'; napply (Hinj … Hmi0 Hload');
    16781677##] nqed.
     
    17471746        ##[ #e;#e0;#e1;#H; (* similar *)
    17481747            nrewrite > e in Hb1; #Hb1;
    1749             nrewrite > CP in Hb1; #Hb1; (* XXX too long ndestruct;*)
     1748            nrewrite > CP in Hb1; #Hb1; (* XXX ndestruct expands proof state too much;*)
    17501749            nelim (grumpydestruct2 ?????? Hb1);
    17511750            #e2;#e3; nrewrite < e0; nrewrite > e2; nrewrite > e3;
    17521751            @ (load_result chunk' v2);@;
    17531752            ##[ napply (load_store_similar … STORE2); //
    1754             ##| nrewrite > LOAD1 in H; #H; nwhd in H:(??%%);
    1755                 nrewrite > (grumpydestruct1 … H); napply Hvalinj;
    1756                 napply sym_eq; //
     1753            ##| nrewrite > LOAD1 in H; #H; nwhd in H:(??%%); ndestruct;
     1754                napply Hvalinj; //;
    17571755            ##]
    17581756         ##| #Hdis; #H; (* disjoint *)
     
    17631761             nrewrite < LOAD2; napply (load_store_other … STORE2);
    17641762             nelim (decidable_eq_Z b1 b1'); #eb1;
    1765              ##[ nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d; 
     1763             ##[ nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d;
    17661764                 nelim (grumpydestruct2 ?????? eb2d); #eb2; #ed;
    17671765                 nelim Hdis; ##[ #Hdis; nelim Hdis;
     
    18911889##| *;*;#A;#B;#C;
    18921890  nrewrite > A in Hbinj' LOAD; #Hbinj'; #LOAD;
    1893   nrewrite > Hbinj in Hbinj'; #bad; (* XXX ndestruct doesn't complete *) nelim (grumpydestruct ?? bad);
     1891  nrewrite > Hbinj in Hbinj'; #bad; ndestruct;
    18941892##] nqed.
    18951893
     
    19141912##| *;*;#A;#B;*;#C;#D;
    19151913    nrewrite > A in Hbinj' LOAD; #Hbinj'; #LOAD; nrewrite > Hbinj in Hbinj';
    1916     #Hbinj'; (* XXX surprised ndestruct can't copy here *) nelim (grumpydestruct2 ?????? Hbinj'); #eb2; #edelta;
     1914    #Hbinj'; (* XXX ndestruct normalizes too much here *) nelim (grumpydestruct2 ?????? Hbinj'); #eb2; #edelta;
    19171915    nrewrite < eb2; nrewrite < edelta;
    19181916    ncut (v1 = Vundef); ##[ napply (load_alloc_same … ALLOC … LOAD) ##]
     
    20172015  ∀m: mem. extends m m.
    20182016#m;@;//;
    2019 nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;nnormalize in ⊢ (%→?);#H;
    2020 (* XXX: *really* suprised ndestruct didn't complete *) nelim (grumpydestruct2 ?????? H); #eb1;#edelta;#LOAD;
     2017nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;nnormalize in ⊢ (%→?);#H; 
     2018(* XXX: ndestruct makes the goal unreadable *) nelim (grumpydestruct2 ?????? H); #eb1;#edelta;#LOAD;
    20212019@ v1; @;
    20222020##[ nrewrite < edelta; nrewrite > (Zplus_z_OZ ofs); //;
     
    20552053##| napply (free_parallel_inj … Hinj);
    20562054  ##[ ##2: //;
    2057   ##| ##3: nnormalize; #b';#delta;#ee;
    2058            nelim (grumpydestruct2 ?????? ee); //
     2055  ##| ##3: nnormalize; #b';#delta;#ee; ndestruct; //
    20592056  ##]
    20602057##] nqed.
     
    21052102    #b';#delta;#einj;nnormalize in einj; ndestruct;
    21062103    nelim Houtside;
    2107     ##[ #lo;@ 2; nrewrite > (Zplus_z_OZ ?); //
    2108     ##| #hi;@ 1;  nrewrite > (Zplus_z_OZ ?); //
     2104    ##[ #lo;@ 2; nrewrite > (Zplus_z_OZ ?); /2/
     2105    ##| #hi;@ 1;  nrewrite > (Zplus_z_OZ ?); /2/
    21092106    ##]
    21102107##] nqed.
     
    21622159    ##| #b';#off; napply load_lessdef; //
    21632160    ##]
    2164 ##| #v;#e;nrewrite > e in LOAD; #LOAD; nwhd in LOAD:(??%?); napply False_ind (* XXX otherwise ndestruct takes 30s *); ndestruct
     2161##| #v;#e;nrewrite > e in LOAD; #LOAD; nwhd in LOAD:(??%?); ndestruct;
    21652162##] nqed.
    21662163
     
    21972194##[ #v; #e1;#e2; nrewrite > e1 in STORE; ncases v;
    21982195    ##[ nwhd in ⊢ ((??%?)→?); #H'; napply False_ind; ndestruct;
    2199     ##| ##2,3: #v'; nwhd in ⊢ ((??%?)→?); #H'; napply False_ind; ndestruct;
     2196    ##| ##2,3: #v'; nwhd in ⊢ ((??%?)→?); #H'; ndestruct;
    22002197    ##| #b';#off; napply store_lessdef; //
    22012198    ##]
    2202 ##| #v;#e;nrewrite > e in STORE; #STORE; nwhd in STORE:(??%?); napply False_ind (* XXX otherwise ndestruct fails *); ndestruct
     2199##| #v;#e;nrewrite > e in STORE; #STORE; nwhd in STORE:(??%?); ndestruct
    22032200##] nqed.
    22042201
     
    25152512(* FIXME: the next two cases are very similar *)
    25162513##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
    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;
    2529         ##[ ##1,3: napply I ##| ##2,4: napply leb_true_to_le; @; ##]
    2530         *)
     2514    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
     2515    ##[ ##2,4: nwhd in ⊢ (??%%); nrewrite > Hz; @
     2516    ##| ##1,3: nwhd in ⊢ (??%%); nrewrite > (sign_ext_equal_if_zero_equal … Hz);
     2517        @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
    25312518    ##]
    2532 
    25332519##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
    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         ##]
     2520    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
     2521    ##[ ##2,4: nwhd in ⊢ (??%%); nrewrite > Hz; @
     2522    ##| ##1,3: nwhd in ⊢ (??%%); nrewrite > (sign_ext_equal_if_zero_equal … Hz);
     2523        @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
    25462524    ##]
    25472525
     
    28112789    nwhd in ⊢ ((??%?)→?→?); napply eqZb_elim; #e; nwhd in ⊢ ((??%?)→?→?);
    28122790    #Hextend;#LOAD;
    2813     ##[ napply False_ind; (* XXX *) napply grumpydestruct; //;
     2791    ##[ ndestruct;
    28142792    ##| nlapply (mi_inj … Hextend LOAD); *; #v2; *; #LOAD2; #VINJ;
    28152793    @ v2; @; //;
     
    29072885    ##| nelim (decidable_eq_Z b1' b2'); #e';
    29082886        ##[ nrewrite < e' in INJb2 ⊢ %; nrewrite < eb1'; nrewrite < eofs1; #INJb2; nlapply (boundmapped … INJb2);
    2909             *; #H; @2; /2/;
     2887            *; #H; @2; ##[ @2 ##| @1 ##] napply H;
    29102888        ##| @1;@1;@1; napply e'
    29112889        ##]
    29122890    ##| nelim (decidable_eq_Z b1' b2'); #e';
    29132891        ##[ nrewrite < e' in INJb2 ⊢ %; #INJb2; nelim (grumpydestruct2 ?????? INJb2); #eb'; #eofs; nrewrite < eb' in INJb1; nrewrite < eofs; #INJb1; nlapply (boundmapped … INJb1);
    2914             *; #H; @2; /2/;
     2892            *; #H; @2; ##[ @1; /2/ ##| @2; napply H; ##]
    29152893        ##| @1;@1;@1; napply e'
    29162894        ##]
     
    30343012  alloc_init_data m id = 〈m', b〉 →
    30353013  mem_inject_neutral m'.
    3036 #m;#id;#m';#b;#Hneutral;#INIT; nwhd in INIT:(??%?); (* XXX: ndestruct too long*)
     3014#m;#id;#m';#b;#Hneutral;#INIT; nwhd in INIT:(??%?); (* XXX: ndestruct makes a bit of a mess *)
    30373015napply (pairdisc_elim … INIT);
    30383016nwhd in ⊢ (??%% → ?);#B;nrewrite < B in ⊢ (??%% → ?);
     
    34493427    napply eqZb_elim; #eb0; nrewrite > eb;
    34503428    ##[ nrewrite > eb0; #ed; nrewrite < (grumpydestruct1 ??? ed);
    3451         nrewrite > (eqZb_z_z ?); /2/;
     3429        nrewrite > (eqZb_z_z ?); /3/;
    34523430    ##| #edelta0; nrewrite > (eqZb_false … eb0);
    34533431        napply ms_range_2; nwhd in edelta0:(??%?); //;
     
    35093487##[ ##1,3,4: //;
    35103488##| #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: // ? *)
     3489    nrewrite > (sign_ext_zero_ext ?? i); ##[ napply refl; (* XXX: // ? *)
    35143490    ##| (* arith *) napply daemon;
    35153491    ##]
  • C-semantics/README

    r14 r15  
    5252ndestruct currently normalizes the goal and every hypothesis that is rewritten.
    5353For ndestruct, getting rid of irrelevant information (e.g., replacing the goal
    54 with False) sometimes helps, or an extra lemma can be used.
     54with False) sometimes helps, an extra lemma can be used, or the definitions
     55can make careful use of 'nlet rec' to prevent reduction.
    5556
    5657Some of the pattern matching in the C syntax has had to be unfolded in
  • C-semantics/binary/Z.ma

    r10 r15  
    151151nqed.
    152152
    153 ndefinition Zle : Z → Z → Prop ≝
    154 λx,y:Z.
     153nlet rec Zle (x:Z) (y:Z) on x : Prop ≝
    155154  match x with
    156155  [ OZ ⇒
     
    173172interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
    174173
    175 ndefinition Zlt : Z → Z → Prop ≝
    176 λx,y:Z.
     174nlet rec Zlt (x:Z) (y:Z) on x : Prop ≝
    177175  match x with
    178176  [ OZ ⇒
     
    306304
    307305(* boolean equality *)
    308 ndefinition eqZb : Z → Z → bool ≝
    309 λx,y:Z.
     306nlet rec eqZb (x:Z) (y:Z) on x : bool ≝
    310307  match x with
    311308  [ OZ ⇒
     
    364361nqed.
    365362
    366 ndefinition Z_compare : Z → Z → compare ≝
    367 λx,y:Z.
     363nlet rec Z_compare (x:Z) (y:Z) : compare ≝
    368364  match x with
    369365  [ OZ ⇒
     
    422418nqed.
    423419
    424 ndefinition Zplus : Z → Z → Z ≝
    425   λx,y. match x with
     420nlet rec Zplus (x:Z) (y:Z) on x : Z ≝
     421  match x with
    426422    [ OZ ⇒ y
    427423    | pos m ⇒
  • C-semantics/extralib.ma

    r14 r15  
    119119nlemma Zmax_l: ∀x,y. x ≤ Zmax x y.
    120120#x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
    121 /3/; nqed.
     121/3/; ncases x; /3/; nqed.
    122122
    123123nlemma Zmax_r: ∀x,y. y ≤ Zmax x y.
    124124#x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
    125 /3/; #H; nrewrite > H; //; nqed.
     125ncases x; /3/; nqed.
    126126
    127127ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
     
    169169interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).
    170170
    171 ndefinition Zleb : Z → Z → bool ≝
    172 λx,y:Z.
     171nlet rec Zleb (x:Z) (y:Z) : bool ≝
    173172  match x with
    174173  [ OZ ⇒
     
    188187    | neg m ⇒ leb m n ]].
    189188   
    190 ndefinition Zltb : Z → Z → bool ≝
    191 λx,y:Z.
     189nlet rec Zltb (x:Z) (y:Z) : bool ≝
    192190  match x with
    193191  [ OZ ⇒
     
    267265##] nqed.
    268266
    269 ndefinition Z_times : Z → Z → Z ≝
    270 λx,y. match x with
     267nlet rec Z_times (x:Z) (y:Z) : Z ≝
     268match x with
    271269[ OZ ⇒ OZ
    272270| pos n ⇒
     
    697695        ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …);
    698696            nrewrite > (pos_compare_lt … l'); //;
    699         ##| /2/;
     697        ##| napply Zminus_Zlt; //;
    700698        ##]
    701699      ##]
Note: See TracChangeset for help on using the changeset viewer.