Changeset 2145 for src/Clight
 Timestamp:
 Jul 2, 2012, 4:12:12 PM (8 years ago)
 Location:
 src/Clight
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r2134 r2145 1061 1061 1062 1062 1063 lemma 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 1109 lemma 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 1125 lemma 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 1139 cases (exec_step_interaction … EX) 1140 #fn * #argtys * #retty * #vargs * #k' * #m #E 1141 destruct 1142 #S cases (state_with_labels_call … S) 1143 #k'' * #K #E2 destruct 1144 whd 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 1063 1165 lemma initial_state_in_simulation : ∀p,s. 1064 1166 make_initial_state p = OK ? s → … … 1088 1190 1089 1191 lemma not_wrong_init : ∀p. 1090 not_wrong _no_io(exec_inf … clight_fullexec p) →1192 not_wrong (exec_inf … clight_fullexec p) → 1091 1193 ∃s. make_initial_state … p = OK ? s. 1092 1194 #p whd in ⊢ (?% → ?); change with (make_initial_state p) in match (make_initial_state ??? p); … … 1162 1264 (s1,s2:state) 1163 1265 (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))) 1165 1267 : sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝ 1166 1268 match 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 ⇒ ? 1169 1272 ] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))). 1170 1273 [ #E1 … … 1189 1292 @build_exec // >E1' in NW1; // 1190 1293 ] 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 ] 1191 1313 ] qed. 1192 1314 … … 1238 1360 [ #tr #i #s #E1 #E2 destruct 1239 1361  #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 28 28 trace_with_extra_labels tr1 tr2 → 29 29 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). 31 34 32 35 (* We do not consider wrong executions or I/O. *) 33 36 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). 37 coinductive 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). 37 41 38 42 (* Desired result *) … … 42 46 let e1 ≝ exec_inf … clight_fullexec p in 43 47 let e2 ≝ exec_inf … clight_fullexec (clight_label p) in 44 not_wrong _no_ioe1 →48 not_wrong e1 → 45 49 sim_with_labels e1 e2.
Note: See TracChangeset
for help on using the changeset viewer.