Changeset 2118


Ignore:
Timestamp:
Jun 27, 2012, 12:04:27 PM (5 years ago)
Author:
campbell
Message:

Labelling preserves behaviour.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2107 r2118  
    10911091 
    10921092
    1093 
     1093inductive steps : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝
     1094| steps_stop : ∀tr,s,r. steps tr (e_stop … tr s r) (e_stop … tr s r)
     1095| steps_step : ∀tr,s,e. steps tr (e_step … tr s e) e
     1096| steps_steps : ∀tr,s,e,tr',e'. steps tr e e' → steps (tr'⧺tr) (e_step … tr' s e) e'.
     1097
     1098coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝
     1099| swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2.
     1100    steps tr2 e2 (e_stop … tr2' r s2) →
     1101    trace_with_extra_labels tr1 tr2 →
     1102    sim_with_labels (e_stop … tr1 r s1) e2
     1103| swl_steps : ∀tr1,tr2,s1,e1,e2,e2'.
     1104    steps tr2 e2 e2' →
     1105    trace_with_extra_labels tr1 tr2 →
     1106    sim_with_labels e1 e2' →
     1107    sim_with_labels (e_step … tr1 s1 e1) e2.
     1108
     1109coinductive not_wrong_no_io : execution state io_out io_in → Prop ≝
     1110| nwni_stop : ∀tr,i,s. not_wrong_no_io (e_stop … tr i s)
     1111| nwni_step : ∀tr,s,e. not_wrong_no_io e → not_wrong_no_io (e_step … tr s e).
     1112
     1113lemma not_wrong_init : ∀p.
     1114  not_wrong_no_io (exec_inf … clight_fullexec p) →
     1115  ∃s. make_initial_state … p = OK ? s.
     1116#p whd in ⊢ (?% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
     1117cases (make_initial_state p)
     1118[ /2/
     1119| normalize #m #NW @⊥
     1120  inversion NW #H1 #H2 #H3 #H4 try #H5 destruct
     1121] qed.
     1122
     1123lemma final_related : ∀s1,s2.
     1124  state_with_labels s1 s2 →
     1125  is_final s1 = is_final s2.
     1126#s1x #s2x *
     1127[ #s1y #s2y * //
     1128| //
     1129] qed.
     1130
     1131lemma plus_not_final : ∀ge,s,tr,s'.
     1132  plus ge s tr s' →
     1133  is_final s = None ?.
     1134#ge #s0 #tr0 #s0' *
     1135[ #s1 #tr #s2 #EX | #s1 #tr #s2 #tr' #s3 #EX #PL ]
     1136lapply (refl ? (is_final s1))
     1137cases (is_final s1) in ⊢ (???% → %);
     1138//
     1139#r cases s1 in EX ⊢ %;
     1140#H9 #H10 #H11 try #H12 try #H13 try #H14 try #H15
     1141[ 1,5: whd in H15:(??%?); | 2,6: whd in H14:(??%?); | 3,7: whd in H13:(??%?); | 4,8: whd in H11:(??%?); ]
     1142destruct
     1143normalize in H10;
     1144destruct
     1145qed.
     1146
     1147lemma plus_exec : ∀ge,s,tr,s'.
     1148  plus ge s tr s' →
     1149  is_final s' = None ? →
     1150  steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
     1151           (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
     1152#ge #s0 #tr0 #s0' #P elim P
     1153[ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold
     1154  whd in ⊢ (??%?);
     1155  whd in match (is_final ?????); >NF
     1156  %2
     1157| #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF
     1158  >exec_inf_aux_unfold >EX1
     1159  whd in ⊢ (??%?);
     1160  whd in match (is_final ?????); >(plus_not_final … P2)
     1161  %3 @IH //
     1162] qed.
     1163
     1164lemma plus_exec_final : ∀ge,s,tr,s',r.
     1165  plus ge s tr s' →
     1166  is_final s' = Some ? r →
     1167  ∃tr'. steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
     1168                 (e_stop … tr' r s').
     1169#ge #s0 #tr0 #s0' #r #P elim P
     1170[ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold
     1171  %{tr} whd in ⊢ (??%?);
     1172  whd in match (is_final ?????); >F
     1173  %1
     1174| #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #F
     1175  cases (IH … F)
     1176  #tr' #S' %{tr'}
     1177  >exec_inf_aux_unfold >EX1
     1178  whd in ⊢ (??%?);
     1179  whd in match (is_final ?????); >(plus_not_final … P2)
     1180  %3 @S'
     1181] qed.
     1182
     1183let corec build_exec
     1184  (ge1,ge2:genv)
     1185  (RG:related_globals … label_fundef ge1 ge2)
     1186  (s1,s2:state)
     1187  (S:state_with_labels s1 s2)
     1188  (NW:not_wrong_no_io (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
     1189: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝
     1190match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
     1191[ nwni_stop tr i s ⇒ ?
     1192| nwni_step tr1 s1' e1 NW1 ⇒ ?
     1193] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))).
     1194[ #E1
     1195  cases (exec_inf_stops_at_final ?? clight_fullexec … E1)
     1196  #EX1 #F1
     1197  cases (step_with_labels … RG … S EX1)
     1198  #tr2 * #s2' * * #PL #TWL #S'
     1199  lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2
     1200  cases (plus_exec_final ????? PL F2)
     1201  #tr2' #S2
     1202  @(swl_stop … S2 TWL)
     1203| #E1
     1204  cases (extract_step ?? clight_fullexec … E1)
     1205  #EX1 #E1'
     1206  cases (step_with_labels … RG … S EX1)
     1207  #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*)
     1208  @(swl_steps … (plus_exec … EX2 ?))
     1209  [ <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)
     1210  | //
     1211  | (* Manual rewrite to prevent guardedness condition getting upset. *)
     1212    @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?])
     1213    @build_exec // >E1' in NW1; //
     1214  ]
     1215] qed.
     1216
     1217lemma initial_state_is_not_final : ∀p,s.
     1218  make_initial_state p = OK ? s →
     1219  is_final s = None ?.
     1220* #vars #fns #main #s
     1221whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
     1222cases (bind_inversion ????? EX) -EX #m * #Em #EX
     1223cases (bind_inversion ????? EX) -EX #b * #Emain #EX
     1224cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
     1225whd in EX:(??%%); destruct //
     1226qed.
     1227
     1228
     1229theorem labelling_sim : ∀p.
     1230  let e1 ≝ exec_inf … clight_fullexec p in
     1231  let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
     1232  not_wrong_no_io e1 →
     1233  sim_with_labels e1 e2.
     1234#p
     1235#NW
     1236cases (not_wrong_init p NW)
     1237#s1 #I1
     1238cases (initial_state_in_simulation … I1)
     1239#s2 * #I2
     1240
     1241whd in match (exec_inf ??? p) in NW ⊢ %;
     1242letin ge1 ≝ (make_global ??? p) in NW ⊢ %;
     1243change with (make_initial_state p) in match (make_initial_state ??? p);
     1244>I1
     1245
     1246whd in match (exec_inf ????);
     1247letin ge2 ≝ (make_global ?? clight_fullexec (clight_label p))
     1248change with (make_initial_state (clight_label p)) in match (make_initial_state ?? clight_fullexec (clight_label p));
     1249>I2
     1250
     1251whd in ⊢ (?% → ? → ?%%);
     1252>exec_inf_aux_unfold
     1253>exec_inf_aux_unfold
     1254whd in ⊢ (?% → ? → ?%%);
     1255whd in match (is_final ?????);
     1256>(initial_state_is_not_final … I1)
     1257whd in match (is_final ?????);
     1258>(initial_state_is_not_final … I2)
     1259whd in ⊢ (?% → ? → ?%%);
     1260
     1261#NW #S
     1262@(swl_steps E0 E0)
     1263[ 2: @steps_step | skip | // | @build_exec
     1264  [ @transform_program_related | // | inversion NW
     1265    [ #tr #i #s #E1 #E2 destruct
     1266    | #trX #sX #eX #NWX #E1X #E2X destruct //
     1267    ]
     1268  ]
     1269] qed.
     1270
     1271
     1272
  • src/common/SmallstepExec.ma

    r1599 r2118  
    8080*)
    8181
     82lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
     83  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
     84  step … ge s = Value … 〈tr, s'〉 ∧
     85  is_final … s' = Some ? r.
     86#O #I #TS #ge #s #s' #tr #r
     87>exec_inf_aux_unfold
     88cases (step … ge s)
     89[ 1,3: normalize #H1 #H2 try #H3 destruct
     90| * #tr' #s''
     91  whd in ⊢ (??%? → ?);
     92  lapply (refl ? (is_final … s''))
     93  cases (is_final … s'') in ⊢ (???% → %);
     94  [ #_ whd in ⊢ (??%? → ?); #E destruct
     95  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
     96  ]
     97] qed.
     98
     99lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
     100  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
     101  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
     102#O #I #TS #ge #s #s' #tr #e
     103>exec_inf_aux_unfold
     104cases (step … s)
     105[ 1,3: normalize #H1 #H2 try #H3 destruct
     106| * #tr' #s''
     107  whd in ⊢ (??%? → ?);
     108  cases (is_final … s'')
     109  [ #E normalize in E; destruct /2/
     110  | #r #E normalize in E; destruct
     111  ]
     112] qed.
     113
     114lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
     115  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
     116  is_final … s' = None ?.
     117#O #I #TS #ge #s #s' #tr #e
     118>exec_inf_aux_unfold
     119cases (step … s)
     120[ 1,3: normalize #H1 #H2 try #H3 destruct
     121| * #tr' #s''
     122  whd in ⊢ (??%? → ?);
     123  lapply (refl ? (is_final … s''))
     124  cases (is_final … s'') in ⊢ (???% → %);
     125  [ #F whd in ⊢ (??%? → ?); #E destruct @F
     126  | #r' #_ #E whd in E:(??%?);  destruct
     127  ]
     128] qed.
     129
     130
     131
    82132record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
    83133{ program : Type[0]
Note: See TracChangeset for help on using the changeset viewer.