Changeset 1954


Ignore:
Timestamp:
May 16, 2012, 2:44:05 PM (7 years ago)
Author:
campbell
Message:

Initial state is in the labelling simulation
(modulo global envs results).

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r1930 r1954  
    77
    88(* TODO: make something general that can live in common/Globalenvs.ma. *)
    9 record related_globals (ge:genv) (ge':genv) : Prop ≝ {
     9record related_globals (F:Type[0]) (t:F → F) (ge:genv_t Genv F) (ge':genv_t Genv F) : Prop ≝ {
    1010  rg_find_symbol: ∀s.
    1111    find_symbol ?? ge s = find_symbol ?? ge' s;
    1212  rg_find_funct: ∀v,f.
    1313    find_funct ?? ge v = Some ? f →
    14     find_funct ?? ge' v = Some ? (label_fundef f)
     14    find_funct ?? ge' v = Some ? (t f);
     15  rg_find_funct_ptr: ∀b,f.
     16    find_funct_ptr ?? ge b = Some ? f →
     17    find_funct_ptr ?? ge' b = Some ? (t f)
    1518}.
     19
     20(* FIXME with a more general result *)
     21axiom transform_program_related : ∀F,V,init,t,p.
     22  related_globals F t (globalenv Genv ? V init p) (globalenv Genv ? V init (transform_program ??? p t)).
     23(*
     24#F #V #init #t * #vars #fns #main
     25whd in match (transform_program ?????);
     26whd in match (transf_program ????);
     27elim fns
     28[ % [ // | * [ | #sz #i | #f | #r | #ptr ] #f #F1 whd in F1:(??%?); destruct
     29             cases (eq_offset ??) in F1; #F1 whd in F1:(??%?);
     30             whd in match (globalenv ?????) in F1;
     31             whd in match (globalenv_allocmem ????) in F1;
     32             elim
     33%
     34[ #s
     35*)
    1636
    1737(* Useful for breaking up the labeling functions, because we don't care about
     
    2242#A #B #C #D * //
    2343qed.
     44
    2445
    2546(* Similarly, lemma to break up label_expr, label_exprs and label_statement in
     
    7192
    7293theorem label_expr_ok : ∀ge,ge',en,m.
    73   related_globals ge ge' →
     94  related_globals ? label_fundef ge ge' →
    7495  (∀e,v,tr.
    7596   exec_expr ge en m e = OK … 〈v,tr〉 →
     
    261282
    262283lemma label_exprs_ok : ∀ge,ge'.
    263    related_globals ge ge' →
     284   related_globals ? label_fundef ge ge' →
    264285   ∀en,m,es,vs,tr.
    265286   exec_exprlist ge en m es = OK … 〈vs,tr〉 →
     
    384405
    385406lemma opt_find_funct : ∀ge,ge',m,vf,fd.
    386   related_globals ge ge' →
     407  related_globals ? label_fundef ge ge' →
    387408  opt_to_io io_out io_in … m (find_funct ?? ge vf) = Value … fd →
    388409  opt_to_io io_out io_in … m (find_funct ?? ge' vf) = Value … (label_fundef fd).
     
    671692   for labeled_statements. *)
    672693lemma step_with_labels_partial : ∀ge,ge'.
    673   related_globals ge ge' →
     694  related_globals ? label_fundef ge ge' →
    674695  ∀s1,s1',tr,s2.
    675696  state_with_labels_partial s1 s1' →
     
    10521073
    10531074theorem step_with_labels : ∀ge,ge'.
    1054   related_globals ge ge' →
     1075  related_globals ? label_fundef ge ge' →
    10551076  ∀s1,s1',tr,s2.
    10561077  state_with_labels s1 s1' →
     
    10811102] qed.
    10821103
    1083 
    1084    
    1085 
    1086 
     1104(* FIXME: to globalenvs and prove *)
     1105axiom transform_program_init_mem : ∀A,B,V,p,f,init.
     1106  init_mem Genv ?? init p = init_mem Genv ?? init (transform_program A B V p f).
     1107
     1108
     1109lemma initial_state_in_simulation : ∀p,s.
     1110  make_initial_state p = OK ? s →
     1111  ∃s'. make_initial_state (clight_label p) = OK ? s' ∧ state_with_labels s s'.
     1112* #vars #fns #main #s
     1113whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
     1114cases (bind_inversion ????? EX) -EX #m * #Em #EX
     1115cases (bind_inversion ????? EX) -EX #b * #Emain #EX
     1116cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
     1117whd in EX:(??%%); destruct
     1118whd in match (make_initial_state ?);
     1119letin ge' ≝ (make_global ?)
     1120cut (related_globals ? label_fundef ge ge')
     1121[ // ] #RG
     1122% [2: %
     1123[ whd in ⊢ (??%?);
     1124  change with (transform_program ??? (mk_program …) label_fundef) in match (mk_program ??? (transf_program ????) ?);
     1125  <transform_program_init_mem >Em in ⊢ (??%?);
     1126  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
     1127  whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain')
     1128  whd in ⊢ (??%?); @refl
     1129| /3/
     1130] | skip ]
     1131qed.
     1132 
     1133
     1134
  • src/common/Errors.ma

    r1949 r1954  
    232232qed.
    233233
     234lemma opt_eq_from_res : ∀T,m,e,v.
     235  opt_to_res T m e = return v →
     236  e = Some T v.
     237#T #m * [ #v #E normalize in E; destruct | #e' #v #E normalize in E; destruct % ]
     238qed.
     239
     240coercion opt_eq_from_res :
     241  ∀T,m,e,v. ∀E:opt_to_res T m e = return v. e = Some T v ≝ opt_eq_from_res
     242  on _E:eq (res ?) ?? to eq (option ?) ??.
     243
    234244(* A variation of bind and its notation that provides an equality proof for
    235245   later use. *)
Note: See TracChangeset for help on using the changeset viewer.