source: src/Clight/SwitchAndLabel.ma @ 3044

Last change on this file since 3044 was 3044, checked in by campbell, 7 years ago

Start showing combination of switch removal and labelling is OK.
Fix typo in switch removal statement.

File size: 6.2 KB
Line 
1include "Clight/switchRemoval.ma".
2include "Clight/labelSimulation.ma".
3
4axiom switch_final_related : ∀ge1,s1,s2.
5  switch_state_sim ge1 s1 s2 →
6  is_final s1 = is_final s2.
7
8lemma after_aux_result : ∀avs,n,s,tr,P.
9  after_aux avs n s tr P →
10  ∃tr',s'. P tr' s' ∧ after_aux avs n s tr (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
11#avs #n elim n
12[ #s #tr #P #A whd in A; %{tr} %{s} % [ @A | % ]
13| #n' #IH #s #tr #P
14  whd in ⊢ (% → ?);
15  lapply (refl ? (is_final … s))
16  cases (is_final … s) in ⊢ (???% → %);
17  [ #F whd in ⊢ (% → ?);
18    lapply (refl ? (step … s))
19    cases (step … s) in ⊢ (???% → %);
20    [ #o #k #_ *
21    | * #tr1 #s1 #ST whd in ⊢ (% → ?);
22      cases n' in IH ⊢ %;
23      [ #_ whd in ⊢ (% → ?); #p % [2: % [2: %{p} whd >F whd >ST whd % | skip ] | skip ]
24      | #n'' #IH lapply (refl ? (avs_inv avs s1)) cases (avs_inv avs s1) in ⊢ (???% → %);
25        [ #INV #AF
26          cases (IH … AF) #tr' * #s' * #p #AF'
27         % [2: % [2: %{p} whd >F whd >ST whd >INV @AF' | skip ] | skip ]
28        | #_ *
29        ]
30      ]
31    | #m #_ *
32    ]
33  | #r #F *
34  ]
35] qed.
36
37lemma after_n_result : ∀n,O,I,exec,g,s,P,inv.
38  after_n_steps n O I exec g s inv P →
39  ∃tr',s'.
40    P tr' s' ∧
41    after_n_steps n O I exec g s inv (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
42#n #O #I #exec #g #s #P #inv #A
43cases (after_aux_result … A) #tr * #s' * #p #A'
44%{tr} %{s'} %{p} @A'
45qed.
46
47
48lemma after_1_of_n_steps' : ∀n,O,I,exec,g,tr,s',s.
49  after_n_steps (S n) O I exec g s (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr,s'〉) →
50  ∃tr1,tr2,s1.
51  is_final … exec g s = None ? ∧
52  step … exec g s = Value … 〈tr1,s1〉 ∧
53  tr = tr1⧺tr2 ∧
54  after_n_steps n O I exec g s1 (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr2,s'〉).
55#n #O #I #exec #g #tr #s' #s #A
56cases (after_1_of_n_steps … A)
57#tr1 * #s1 * * * #F #ST #_ #A'
58cases (after_n_result … A')
59#tr'' * #s'' * #E #A'' destruct
60% [2: % [2: % [2: % [ % [% [ @F | @ST ] | % ] | @A'' ] | skip ] | skip ] | skip ]
61qed.
62
63theorem steps_with_labels : ∀ge,ge'.
64  related_globals_gen … label_fundef ge ge' →
65  ∀n,s1,s1',tr,s2.
66  state_with_labels s1 s1' →
67  after_n_steps (S n) … clight_exec ge s1 (λ_.true) (λtr',s'.〈tr',s'〉 = 〈tr,s2〉) →
68   ∃m. after_n_steps (S m) … clight_exec ge' s1' (λ_.true)
69   (λtr',s2'. trace_with_extra_labels tr tr' ∧
70              state_with_labels s2 s2').
71#ge #ge' #RG
72#n elim n
73[ #s1 #s1' #tr #s2 #SWL #AFTER
74  cases (after_1_step … AFTER) #tr' * #s' * * #F1 #ST1 #E destruct
75  @(step_with_labels … RG … ST1) //
76| #n #IH #s1 #s1' #tr #s2 #SWL #AFTER
77  cases (after_1_of_n_steps' … AFTER) #tr1 * #tr2 * #s' * * * #F1 #ST1 #E #AFTER'
78  destruct
79  cases (step_with_labels … RG … SWL ST1) #m1 #AF1
80  cases (after_n_result … AF1) #tr2 * #s2' * * #TWEL #SWL' #AF''
81  cases (IH … SWL' AFTER')
82  #m2 #AF2
83  %{(m1+S m2)}
84  @(after_n_m (S m1) (S m2) … AF2) //
85  @(after_n_covariant … AF'')
86 
87  #tr #s #E destruct %{(refl ??)}
88  #tr'' #s'' * #TWEL #SWL % /2/
89] qed.
90
91
92let corec build_exec
93  (ge1,ge2,ge3:genv)
94  (SRG:switch_removal_globals ? fundef_switch_removal ge1 ge2)
95  (RG:related_globals_gen … label_fundef ge2 ge3)
96  (s1,s2,s3:state)
97  (S1:switch_state_sim ge1 s1 s2)
98  (S2:state_with_labels s2 s3)
99  (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
100: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge3 (exec_step ge3 s3)) ≝
101match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
102[ nw_stop tr i s ⇒ ?
103| nw_step tr1 s1' e1 NW1 ⇒ ?
104| nw_interact o k NWk ⇒ ?
105] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))).
106[ #E1
107  cases (exec_inf_stops_at_final ?? clight_fullexec … E1)
108  #EX1 #F1
109  cases (switch_removal_correction … SRG … S1 EX1)
110  #n1 #A1
111  cases (after_n_result … A1) #tr1' * #s1' * * #E destruct #S1' #A1'
112  cases (steps_with_labels … RG … S2 A1')
113  #n2 #A2 cases (after_inv clight_fullexec ????? A2) #tr' * #s' * * #TWL #S'
114  lapply F1 whd in ⊢ (??%? → ?); >(switch_final_related … S1') >(final_related … S') #F3
115    whd in match (is_final … s'); >F3 *
116    #tr2' #S2
117    @(swl_stop … S2 TWL)
118| #E1
119  cases (extract_step ?? clight_fullexec … E1)
120  #EX1 #E1'
121  cases (switch_removal_correction … SRG … S1 EX1)
122  #n1 #A1
123  cases (after_n_result … A1) #tr1' * #s2' * * #E destruct (E) #S1' #A1'
124  cases (steps_with_labels … RG … S2 A1')
125  #n #AF cases (after_inv clight_fullexec ????? AF) #tr' * #s' * * #TWL #S'
126  whd in match (is_final … s'); lapply (refl ? (is_final s'))
127  cases (is_final s') in ⊢ (???% → %);
128  [ #NF #H whd in H; @(swl_steps … H) //
129    @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?])
130    @(build_exec … SRG RG … S1' S') >E1' in NW1; //
131  | #r <(final_related … S') <(switch_final_related … S1') change with (is_final … clight_fullexec ge1 s1') in ⊢ (??%? → ?);
132    >(exec_e_step_not_final ?? clight_fullexec … E1) #E destruct
133  ]
134| #E1
135  cases (extract_interact ?? clight_fullexec … E1)
136  #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk
137  cases (interactive_step_with_labels … RG … EX1 S)
138  #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 ⊢ (??%);
139  @swl_interact
140  #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
141  lapply (NWk i)
142  @(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 ⇒ ?])
143  @(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 ?????);
144  cases (is_final s2')
145  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
146    inversion NW'
147    [ #H1 #H2 #H3 #H4 #H5 destruct
148    | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
149    | #H14 #H15 #H16 #H17 #H18 destruct
150    ]
151  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
152  ]
153] qed.
Note: See TracBrowser for help on using the repository browser.