Changeset 2145


Ignore:
Timestamp:
Jul 2, 2012, 4:12:12 PM (5 years ago)
Author:
campbell
Message:

Cost labelling doesn't affect interaction.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2134 r2145  
    10611061
    10621062
     1063lemma exec_step_interaction:
     1064  ∀ge,s,o,k. exec_step ge s = Interact … o k  →
     1065  ∃f,argtys,retty,vargs,k',m. s = Callstate (CL_External f argtys retty) vargs k' m.
     1066#ge #s cases s
     1067[ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
     1068  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
     1069  whd in ⊢ (??%? → ?);
     1070  [ 4,6,8,9: #EX destruct ]
     1071  [ cases a
     1072    [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct
     1073    | #a' whd nodelta in ⊢ (??%? → ?); cases (type_eq_dec (fn_return f) Tvoid)
     1074      #x whd in ⊢ (??%? → ?); [2: cases (exec_expr ????) #y ] #EX whd in EX:(??%?); destruct
     1075    ]
     1076  | cases (find_label a (fn_body f) (call_cont kk)) [ 2: * #x #y ] #EX whd in EX:(??%?); destruct
     1077  | @bindIO_res_interact #l #El @bindIO_res_interact #vt #Evt @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct
     1078  | 4,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
     1079  | @bindIO_res_interact * * normalize #A #B #C try #D try #E destruct
     1080  | @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 @bindIO_opt_interact #x5 #x6 @bindIO_res_interact #x7 #x8 cases a
     1081      [ 2: #x9 @bindIO_res_interact #x10 #x11 ] #EX whd in EX:(??%?); destruct
     1082  | cases (is_Sskip a) #H [ @bindIO_res_interact #vt #Evt @bindIO_res_interact #v #Ev ] #EX whd in EX:(??%?); destruct
     1083  | cases kk [ 1,8: cases (fn_return f) normalize #A try #B try #C try #D try #E try #F try #G try #H destruct
     1084    | 2,3,5,6,7: normalize #A #B try #C try #D try #E destruct
     1085    | #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct ]
     1086  | cases kk normalize #A try #B try #C try #D try #E destruct
     1087  | cases kk [ 4: #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct
     1088    | *: normalize #A try #B try #C try #D try #E destruct
     1089    ]
     1090  ]
     1091| #f #args #kk #m #o #k cases f
     1092  [ #f' whd in ⊢ (??%? → ?); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
     1093    #x1 #x2 @bindIO_res_interact #m #Em #EX whd in EX:(??%?); destruct
     1094  (* This is the only case that actually matters! *)
     1095  | #fn #argtys #rty whd in ⊢ (??%? → ?);
     1096    @bindIO_res_interact #vs #Evs
     1097    #EX whd in EX:(??%?); destruct
     1098    %{fn} %{argtys} %{rty} %{args} %{kk} %{m} %
     1099  ]
     1100| #v #kk #m #o #k whd in ⊢ (??%? → ?); cases kk
     1101    [ cases v [2: * ] normalize #A try #B destruct
     1102    | 8: #x1 #x2 #x3 #x4 cases x1
     1103      [ whd in ⊢ (??%? → ?); #EX destruct | #x5 whd in ⊢ (??%? → ?); cases x5
     1104          #x6 #x7 @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct ]
     1105    | *: normalize #A try #B try #C try #D try #E destruct ]
     1106| #r #o #k #EX whd in EX:(??%?); destruct
     1107] qed.
     1108
     1109lemma state_with_labels_call : ∀f,a,k,m,s1.
     1110 state_with_labels (Callstate f a k m) s1 →
     1111 ∃k'. cont_with_labels k k' ∧ s1 = Callstate (label_fundef f) a k' m.
     1112#f #a #k #m #s1 #S inversion S
     1113[ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
     1114  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
     1115  | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct
     1116  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
     1117  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
     1118  | #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % //
     1119  | #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
     1120  | #H72 #H73 #H74 #H75 destruct
     1121  ]
     1122| #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 destruct
     1123] qed.
     1124
     1125lemma interactive_step_with_labels : ∀ge,ge'.
     1126  related_globals … label_fundef ge ge' →
     1127  ∀s1,s1',o,k.
     1128  exec_step ge s1 = Interact … o k →
     1129  state_with_labels s1 s1' →
     1130  ∃k'.
     1131      exec_step ge' s1' = Interact … o k' ∧
     1132  ∀i. ∃tr,s2.
     1133    k i = Value … 〈tr,s2〉 ∧
     1134    ∃tr',s2'.
     1135      k' i = Value … 〈tr',s2'〉 ∧
     1136      trace_with_extra_labels tr tr' ∧
     1137      state_with_labels s2 s2'.
     1138#ge #ge' #RG #s1 #s1' #o #k #EX
     1139cases (exec_step_interaction … EX)
     1140#fn * #argtys * #retty * #vargs * #k' * #m #E
     1141destruct
     1142#S cases (state_with_labels_call … S)
     1143#k'' * #K #E2 destruct
     1144whd in EX:(??%?);
     1145@(bindIO_res_interact ?????????? EX) -EX
     1146#vs #CHECK #EX whd in EX:(??%?); destruct
     1147% [2: %
     1148[ whd in ⊢ (??%?);
     1149  >CHECK in ⊢ (??%?);
     1150  whd in ⊢ (??%?);
     1151  @refl
     1152| #i
     1153  % [2: % [2: %
     1154  [ @refl
     1155  | % [2: % [ 2: % [ %
     1156    [ @refl
     1157    | // ]
     1158    | /3/ ]
     1159    | skip ]| skip ]
     1160  ]| skip ]| skip ]
     1161]| skip
     1162] qed.
     1163
     1164
    10631165lemma initial_state_in_simulation : ∀p,s.
    10641166  make_initial_state p = OK ? s →
     
    10881190
    10891191lemma not_wrong_init : ∀p.
    1090   not_wrong_no_io (exec_inf … clight_fullexec p) →
     1192  not_wrong (exec_inf … clight_fullexec p) →
    10911193  ∃s. make_initial_state … p = OK ? s.
    10921194#p whd in ⊢ (?% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
     
    11621264  (s1,s2:state)
    11631265  (S:state_with_labels s1 s2)
    1164   (NW:not_wrong_no_io (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
     1266  (NW:not_wrong (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
    11651267: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝
    11661268match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
    1167 [ nwni_stop tr i s ⇒ ?
    1168 | nwni_step tr1 s1' e1 NW1 ⇒ ?
     1269[ nw_stop tr i s ⇒ ?
     1270| nw_step tr1 s1' e1 NW1 ⇒ ?
     1271| nw_interact o k NWk ⇒ ?
    11691272] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))).
    11701273[ #E1
     
    11891292    @build_exec // >E1' in NW1; //
    11901293  ]
     1294| #E1
     1295  cases (extract_interact ?? clight_fullexec … E1)
     1296  #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk
     1297  cases (interactive_step_with_labels … RG … EX1 S)
     1298  #k2' * #EX2 #H2 @(match sym_eq … EX2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) (* XXX why is this necessary? *) whd in ⊢ (??%);
     1299  @swl_interact
     1300  #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
     1301  lapply (NWk i)
     1302  @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (?% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])
     1303  @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge2 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????);
     1304  cases (is_final s2')
     1305  [ whd in ⊢ (?% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
     1306    inversion NW'
     1307    [ #H1 #H2 #H3 #H4 #H5 destruct
     1308    | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
     1309    | #H14 #H15 #H16 #H17 #H18 destruct
     1310    ]
     1311  | #r whd in ⊢ (?% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
     1312  ]
    11911313] qed.
    11921314
     
    12381360    [ #tr #i #s #E1 #E2 destruct
    12391361    | #trX #sX #eX #NWX #E1X #E2X destruct //
    1240     ]
    1241   ]
    1242 ] qed.
    1243 
    1244 
    1245 
     1362    | #H1 #H2 #H3 #H4 #H5 destruct
     1363    ]
     1364  ]
     1365] qed.
     1366
     1367
     1368
  • src/Clight/labelSpecification.ma

    r2134 r2145  
    2828    trace_with_extra_labels tr1 tr2 →
    2929    sim_with_labels e1 e2' →
    30     sim_with_labels (e_step … tr1 s1 e1) e2.
     30    sim_with_labels (e_step … tr1 s1 e1) e2
     31| swl_interact : ∀o,k1,k2.
     32    (∀i. sim_with_labels (k1 i) (k2 i)) →
     33    sim_with_labels (e_interact … o k1) (e_interact … o k2).
    3134
    3235(* We do not consider wrong executions or I/O. *)
    3336
    34 coinductive not_wrong_no_io : execution state io_out io_in → Prop ≝
    35 | nwni_stop : ∀tr,i,s. not_wrong_no_io (e_stop … tr i s)
    36 | nwni_step : ∀tr,s,e. not_wrong_no_io e → not_wrong_no_io (e_step … tr s e).
     37coinductive not_wrong : execution state io_out io_in → Prop ≝
     38| nw_stop : ∀tr,i,s. not_wrong (e_stop … tr i s)
     39| nw_step : ∀tr,s,e. not_wrong e → not_wrong (e_step … tr s e)
     40| nw_interact : ∀o,k. (∀i. not_wrong (k i)) → not_wrong (e_interact … o k).
    3741
    3842(* Desired result *)
     
    4246  let e1 ≝ exec_inf … clight_fullexec p in
    4347  let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
    44   not_wrong_no_io e1 →
     48  not_wrong e1 →
    4549  sim_with_labels e1 e2.
  • src/common/IOMonad.ma

    r2044 r2145  
    385385] qed.
    386386
     387lemma bindIO_res_interact : ∀O,I,A,B,e,f,o,k. ∀P:∀o:O. (I o → IO O I B) → Type[0].
     388  (∀v. e = OK A v → f v = Interact … o k → P o k) →
     389  bindIO O I A B (err_to_io … e) f = Interact … o k → P o k.
     390#O #I #A #B *
     391[ #a #f #o #k #P #H #E @(H … E) @refl
     392| #m #f #o #k #P #_ #E whd in E:(??%?); destruct
     393] qed.
     394
     395lemma bindIO_opt_interact : ∀O,I,A,B,m,e,f,o,k. ∀P:∀o:O. (I o → IO O I B) → Type[0].
     396  (∀v. e = Some A v → f v = Interact … o k → P o k) →
     397  bindIO O I A B (opt_to_io … m e) f = Interact … o k → P o k.
     398#O #I #A #B #m *
     399[ #f #o #k #P #_ #E whd in E:(??%?); destruct
     400| #a #f #o #k #P #H #E @(H … E) @refl
     401] qed.
     402
    387403lemma bindIO_inversion: ∀O,I.
    388404  ∀A,B: Type[0]. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
  • src/common/SmallstepExec.ma

    r2118 r2145  
    112112] qed.
    113113
     114lemma extract_interact : ∀O,I,TS,ge,s,o,k.
     115  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
     116  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
     117#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
     118cases (step … s)
     119[ #o' #k' normalize #E destruct %{k'} /2/
     120| * #x #y normalize cases (is_final ?????) normalize
     121  #X try #Y destruct
     122| normalize #m #E destruct
     123] qed.
     124
    114125lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
    115126  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
Note: See TracChangeset for help on using the changeset viewer.