Changeset 2118

Timestamp:

Jun 27, 2012, 12:04:27 PM (6 years ago)

Author:

campbell

Message:

Labelling preserves behaviour.

Location:

src

Files:

• Clight/labelSimulation.ma (modified) (1 diff)
• common/SmallstepExec.ma (modified) (1 diff)

src/Clight/labelSimulation.ma

@@ -1091 +1091 @@
   
 
-
+inductive steps : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝
+| steps_stop : ∀tr,s,r. steps tr (e_stop … tr s r) (e_stop … tr s r)
+| steps_step : ∀tr,s,e. steps tr (e_step … tr s e) e
+| steps_steps : ∀tr,s,e,tr',e'. steps tr e e' → steps (tr'⧺tr) (e_step … tr' s e) e'.
+
+coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝
+| swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2.
+    steps tr2 e2 (e_stop … tr2' r s2) →
+    trace_with_extra_labels tr1 tr2 →
+    sim_with_labels (e_stop … tr1 r s1) e2
+| swl_steps : ∀tr1,tr2,s1,e1,e2,e2'.
+    steps tr2 e2 e2' →
+    trace_with_extra_labels tr1 tr2 →
+    sim_with_labels e1 e2' →
+    sim_with_labels (e_step … tr1 s1 e1) e2.
+
+coinductive not_wrong_no_io : execution state io_out io_in → Prop ≝
+| nwni_stop : ∀tr,i,s. not_wrong_no_io (e_stop … tr i s)
+| nwni_step : ∀tr,s,e. not_wrong_no_io e → not_wrong_no_io (e_step … tr s e).
+
+lemma not_wrong_init : ∀p.
+  not_wrong_no_io (exec_inf … clight_fullexec p) →
+  ∃s. make_initial_state … p = OK ? s.
+#p whd in ⊢ (?% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
+cases (make_initial_state p)
+[ /2/
+| normalize #m #NW @⊥
+  inversion NW #H1 #H2 #H3 #H4 try #H5 destruct
+] qed.
+
+lemma final_related : ∀s1,s2.
+  state_with_labels s1 s2 →
+  is_final s1 = is_final s2.
+#s1x #s2x *
+[ #s1y #s2y * //
+| //
+] qed.
+
+lemma plus_not_final : ∀ge,s,tr,s'.
+  plus ge s tr s' →
+  is_final s = None ?.
+#ge #s0 #tr0 #s0' * 
+[ #s1 #tr #s2 #EX | #s1 #tr #s2 #tr' #s3 #EX #PL ]
+lapply (refl ? (is_final s1))
+cases (is_final s1) in ⊢ (???% → %);
+//
+#r cases s1 in EX ⊢ %;
+#H9 #H10 #H11 try #H12 try #H13 try #H14 try #H15
+[ 1,5: whd in H15:(??%?); | 2,6: whd in H14:(??%?); | 3,7: whd in H13:(??%?); | 4,8: whd in H11:(??%?); ]
+destruct
+normalize in H10;
+destruct
+qed.
+
+lemma plus_exec : ∀ge,s,tr,s'.
+  plus ge s tr s' →
+  is_final s' = None ? →
+  steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
+           (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
+#ge #s0 #tr0 #s0' #P elim P
+[ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold
+  whd in ⊢ (??%?);
+  whd in match (is_final ?????); >NF
+  %2
+| #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF
+  >exec_inf_aux_unfold >EX1
+  whd in ⊢ (??%?);
+  whd in match (is_final ?????); >(plus_not_final … P2)
+  %3 @IH //
+] qed.
+
+lemma plus_exec_final : ∀ge,s,tr,s',r.
+  plus ge s tr s' →
+  is_final s' = Some ? r →
+  ∃tr'. steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
+                 (e_stop … tr' r s').
+#ge #s0 #tr0 #s0' #r #P elim P
+[ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold
+  %{tr} whd in ⊢ (??%?);
+  whd in match (is_final ?????); >F
+  %1
+| #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #F
+  cases (IH … F)
+  #tr' #S' %{tr'}
+  >exec_inf_aux_unfold >EX1
+  whd in ⊢ (??%?);
+  whd in match (is_final ?????); >(plus_not_final … P2)
+  %3 @S'
+] qed.
+
+let corec build_exec
+  (ge1,ge2:genv)
+  (RG:related_globals … label_fundef ge1 ge2)
+  (s1,s2:state)
+  (S:state_with_labels s1 s2)
+  (NW:not_wrong_no_io (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
+: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝ 
+match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
+[ nwni_stop tr i s ⇒ ?
+| nwni_step tr1 s1' e1 NW1 ⇒ ?
+] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))).
+[ #E1
+  cases (exec_inf_stops_at_final ?? clight_fullexec … E1)
+  #EX1 #F1
+  cases (step_with_labels … RG … S EX1)
+  #tr2 * #s2' * * #PL #TWL #S'
+  lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2
+  cases (plus_exec_final ????? PL F2)
+  #tr2' #S2
+  @(swl_stop … S2 TWL)
+| #E1
+  cases (extract_step ?? clight_fullexec … E1)
+  #EX1 #E1'
+  cases (step_with_labels … RG … S EX1)
+  #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*)
+  @(swl_steps … (plus_exec … EX2 ?))
+  [ <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)
+  | //
+  | (* Manual rewrite to prevent guardedness condition getting upset. *)
+    @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?])
+    @build_exec // >E1' in NW1; //
+  ]
+] qed.
+
+lemma initial_state_is_not_final : ∀p,s.
+  make_initial_state p = OK ? s →
+  is_final s = None ?.
+* #vars #fns #main #s
+whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
+cases (bind_inversion ????? EX) -EX #m * #Em #EX
+cases (bind_inversion ????? EX) -EX #b * #Emain #EX
+cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
+whd in EX:(??%%); destruct //
+qed.
+
+
+theorem labelling_sim : ∀p.
+  let e1 ≝ exec_inf … clight_fullexec p in
+  let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
+  not_wrong_no_io e1 →
+  sim_with_labels e1 e2.
+#p
+#NW
+cases (not_wrong_init p NW)
+#s1 #I1
+cases (initial_state_in_simulation … I1)
+#s2 * #I2
+
+whd in match (exec_inf ??? p) in NW ⊢ %;
+letin ge1 ≝ (make_global ??? p) in NW ⊢ %;
+change with (make_initial_state p) in match (make_initial_state ??? p);
+>I1
+
+whd in match (exec_inf ????);
+letin ge2 ≝ (make_global ?? clight_fullexec (clight_label p))
+change with (make_initial_state (clight_label p)) in match (make_initial_state ?? clight_fullexec (clight_label p));
+>I2
+
+whd in ⊢ (?% → ? → ?%%);
+>exec_inf_aux_unfold
+>exec_inf_aux_unfold
+whd in ⊢ (?% → ? → ?%%);
+whd in match (is_final ?????);
+>(initial_state_is_not_final … I1)
+whd in match (is_final ?????);
+>(initial_state_is_not_final … I2)
+whd in ⊢ (?% → ? → ?%%);
+
+#NW #S
+@(swl_steps E0 E0)
+[ 2: @steps_step | skip | // | @build_exec
+  [ @transform_program_related | // | inversion NW
+    [ #tr #i #s #E1 #E2 destruct
+    | #trX #sX #eX #NWX #E1X #E2X destruct //
+    ]
+  ]
+] qed.
+
+
+

src/common/SmallstepExec.ma

@@ -80 +80 @@
 *)
 
+lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
+  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
+  step … ge s = Value … 〈tr, s'〉 ∧
+  is_final … s' = Some ? r.
+#O #I #TS #ge #s #s' #tr #r
+>exec_inf_aux_unfold
+cases (step … ge s)
+[ 1,3: normalize #H1 #H2 try #H3 destruct
+| * #tr' #s''
+  whd in ⊢ (??%? → ?);
+  lapply (refl ? (is_final … s''))
+  cases (is_final … s'') in ⊢ (???% → %);
+  [ #_ whd in ⊢ (??%? → ?); #E destruct
+  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
+  ]
+] qed.
+
+lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
+  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
+  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
+#O #I #TS #ge #s #s' #tr #e
+>exec_inf_aux_unfold
+cases (step … s)
+[ 1,3: normalize #H1 #H2 try #H3 destruct
+| * #tr' #s''
+  whd in ⊢ (??%? → ?);
+  cases (is_final … s'')
+  [ #E normalize in E; destruct /2/
+  | #r #E normalize in E; destruct
+  ]
+] qed.
+
+lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
+  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
+  is_final … s' = None ?.
+#O #I #TS #ge #s #s' #tr #e
+>exec_inf_aux_unfold
+cases (step … s)
+[ 1,3: normalize #H1 #H2 try #H3 destruct
+| * #tr' #s''
+  whd in ⊢ (??%? → ?);
+  lapply (refl ? (is_final … s''))
+  cases (is_final … s'') in ⊢ (???% → %);
+  [ #F whd in ⊢ (??%? → ?); #E destruct @F
+  | #r' #_ #E whd in E:(??%?);  destruct
+  ]
+] qed.
+
+
+
 record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
 { program : Type[0]