source: src/Cminor/toRTLabsCorrectness.ma @ 3063

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

Remove measure function from FEMeasurable because we're not using it and
it would need to be generalised for clight to cminor. Sketch out rest
of clight to cminor meas_sim record.

File size: 6.8 KB
RevLine 
[2511]1
[2601]2include "Cminor/Cminor_abstract.ma".
3include "RTLabs/RTLabs_abstract.ma".
[2597]4include "Cminor/toRTLabs.ma".
[2511]5
[3007]6record cminor_rtlabs_inv (ge_cm:cm_genv) (ge_ra:RTLabs_genv) : Type[0] ≝ {
[2511]7}.
[3007]8axiom cminor_rtlabs_rel : ∀gc,gr. cminor_rtlabs_inv gc gr → Cminor_state → RTLabs_state → Prop.
[2511]9
[3007]10axiom cminor_rtlabs_rel_labelled : ∀gc,gr,INV,s,s'.
11  cminor_rtlabs_rel gc gr INV s s' →
12  Cminor_labelled s = RTLabs_cost s'.
13
[2511]14(* Conjectured simulation results
15
16   We split these based on the start state:
17   
[3007]18   1. from a ‘normal’ state we simulate a step by [n] normal steps in RTLabs
19      ([n] can be zero if the Cminor program executed an St_skip);
20   2. call and return state steps are simulated by a call/return state step (we
21      don't add anything extra in this stage, it happens in Clight to Cminor);
22      and
[2511]23   3. lone cost label steps are simulates by a lone cost label step
24
[3007]25   Most of the work in this stage is splitting the execution of complex Cminor
26   statements into individual RTLabs steps.  This doesn't contradict 2 above -
27   the expansion of function parameters, return expressions, etc is done for
28   the function call / return *statement*, whereas the call / return *state* is
29   a Callstate / Returnstate that is the second half of the operation.
30
[2511]31   Note that we'll need something more to show that non-termination is
32   preserved (because it isn't obvious that we don't squash a loop to zero
33   instructions).  Options are a traditional measure, or using the soundness of
34   the cost labelling.
35
36   These should allow us to maintain enough structure to identify the RTLabs
37   subtrace corresponding to a measurable Clight/Cminor subtrace.
38 *)
39
40definition cminor_normal : Cminor_state → bool ≝
41λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
42
43definition rtlabs_normal : RTLabs_state → bool ≝
44λs. match RTLabs_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
45
[3007]46axiom cminor_measure : Cminor_state → nat.
47
[2511]48axiom cminor_rtlabs_normal :
[3007]49  ∀ge_cm,ge_ra.
50  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
[2511]51  ∀s1,s1',s2,tr.
[3007]52  cminor_rtlabs_rel … INV s1 s1' →
[2511]53  cminor_normal s1 →
54  ¬ Cminor_labelled s1 →
[3007]55  step ?? Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 →
56  ∃n. after_n_steps n … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'.
[2511]57    tr = tr' ∧
[3007]58    (n = 0 → lt (cminor_measure s2) (cminor_measure s1)) ∧
59    cminor_rtlabs_rel … INV s2 s2'
[2511]60  ).
61
62axiom cminor_rtlabs_call_return :
[3007]63  ∀ge_cm,ge_ra.
64  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
[2511]65  ∀s1,s1',s2,tr.
[3007]66  cminor_rtlabs_rel … INV s1 s1' →
[2511]67  match Cminor_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
[3007]68  step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 →
69  after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'.
[2511]70    tr = tr' ∧
[3007]71    cminor_rtlabs_rel … INV s2 s2'
[2511]72  ).
73
74axiom cminor_rtlabs_cost :
[3007]75  ∀ge_cm,ge_ra.
76  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
[2511]77  ∀s1,s1',s2,tr.
[3007]78  cminor_rtlabs_rel … INV s1 s1' →
[2511]79  Cminor_labelled s1 →
[3007]80  step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 →
81  after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.true) (λtr',s2'.
[2511]82    tr = tr' ∧
[3007]83    cminor_rtlabs_rel … INV s2 s2'
[2511]84  ).
[2597]85
[3007]86axiom cminor_rtlabs_init :
87  ∀p,s.
88  make_initial_state … Cminor_fullexec p = OK … s →
89  let p' ≝ cminor_to_rtlabs p in
90  ∃INV:cminor_rtlabs_inv (make_global … Cminor_fullexec p) (make_global … RTLabs_fullexec p').
91  ∃s'. make_initial_state … RTLabs_fullexec p' = OK … s' ∧
92  cminor_rtlabs_rel … INV s s'.
[2597]93
[3007]94include "common/FEMeasurable.ma".
95include "Cminor/Cminor_classified_system.ma".
96include "RTLabs/RTLabs_classified_system.ma".
[2597]97
[3007]98include "common/ExtraMonads.ma".
99
100lemma Cminor_return_E0 : ∀ge,s,tr,s'.
101  step … Cminor_exec ge s = Value … 〈tr,s'〉 →
102  Cminor_classify s = cl_return →
103  tr = E0.
104#ge *
105[ #f #s #en #H1 #H2 #m #b #k #K #st #tr #s' #STEP #CL whd in CL:(??%?); destruct
106| #id #fd #args #m #st #tr #s' #STEP #CL whd in CL:(??%?); destruct
107| #v #m *
108  [ #tr #s' #STEP #_
109    cases v in STEP; [ #E whd in E:(??%?); destruct ]
110    * [1,3,4: normalize #A try #B destruct ]
111    * #v #STEP whd in STEP:(??%?); destruct %
112  | cases v
113    [ * [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct //
114        | normalize #A #B #C #D #E #F #G #H #I #J #K #L destruct
115        ]
116    | #v' *
117      [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct
118      | #A #B #C #D #E #F #G #H #I #J #K #L whd in L:(??%?); destruct //
119      ]
120    ]
121  ]
122| #r #tr #s' #ST #CL normalize in CL; destruct
123] qed.
124
125definition cminor_rtlabs_meas_sim : meas_sim ≝
126mk_meas_sim
127  Cminor_pcs
128  RTLabs_pcs
129  (λcmp,rap. cminor_to_rtlabs cmp = rap)
130  cminor_rtlabs_inv
131  cminor_rtlabs_rel
132  ? (* rel_normal *)
133  ? (* rel_labelled *)
134  ? (* rel_classify_call *)
135  ? (* rel_classify_return *)
136  ? (* rel_callee *)
137  ? (* labelled_normal_1 *)
138  ? (* labelled_normal_2 *)
139  ? (* notailcalls *)
140  ? (* sim_normal *)
141  ? (* sim_call_nolabel *)
142  ? (* sim_call_label *)
143  ? (* sim_return *)
144  ? (* sim_cost *)
145  ? (* sim_init *)
146.
147[ (* rel_normal *)
148| (* rel_labelled *)
149  @cminor_rtlabs_rel_labelled
150| (* rel_classify_call *)
151| (* rel_classify_return *)
152| (* rel_callee *)
153| (* labelled_normal_1 *)
154  #g * //
155| (* labelled_normal_2 *)
156  #g * // #f #fs #m whd in ⊢ (?% → ?%); whd in match (pcs_classify ???);
157  cases (next_instruction f) //
158| (* notailcalls *)
159  #g @Cminor_notailcalls
160| (* sim_normal *)
161  #g1 #g2 #INV #s1 #s1' #R1 #N1 #NCS1 #s2 #tr #STEP
162  cases (cminor_rtlabs_normal … R1 N1 NCS1 STEP)
163  #m #AFTER %{m} @(after_n_covariant … AFTER)
164  #tr' #s * * #H1 #H2 #H3 /3/
165| (* sim_call_nolabel *)
166  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP #NCS2 %{0}
167  @(cminor_rtlabs_call_return … R1 … STEP)
168  change with (Cminor_classify ?) in CL1:(??%?); >CL1 %
169| (* sim_call_label *)
170  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #STEP1 #CS2 #STEP2 %{1}
171  lapply (cminor_rtlabs_call_return … R1 … STEP1)
172  [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ]
173  #AFTER1 @(after_n_covariant … AFTER1) #tr' #s' * #E #R' destruct
174  % [ %
175  [  %
176  |  change with (RTLabs_cost s') in ⊢ (?%); <(cminor_rtlabs_rel_labelled … R') @CS2
177  ]| lapply (cminor_rtlabs_cost … R' … CS2 STEP2)
178     #AFTER2 cases (after_1_step … AFTER2)
179     #trx * #sx * * #NFx #STEPx * #E #Rx destruct
180     whd >NFx whd >STEPx whd /3/
181  ]
182| (* sim_return *)
183  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP %{0}
184  lapply (cminor_rtlabs_call_return … R1 … STEP)
185  [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ]
186  >(Cminor_return_E0 … STEP CL1)
187  #AFTER %{(refl ??)} @AFTER
188| (* sim_cost *)
189  #g1 #g2 #INV #s1 #s1' #s2 #tr #R1 #CS1 #STEP
190  @(cminor_rtlabs_cost … R1 … STEP)
191  @CS1
192| (* sim_init *)
193  #p #p' #s #COMPILE destruct #INIT
194  cases (cminor_rtlabs_init … INIT) #INV * #s' * #INIT' #R
195  %{s'} % [ @INIT' | %{INV} @R ]
196] cases daemon qed.
Note: See TracBrowser for help on using the repository browser.