source: src/Cminor/toRTLabsCorrectness.ma

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

Tidy up recent work a little.

File size: 7.0 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
[3081]125(* Build the simulation record for FEMeasurable.  Note that sim_call_label is
126   made up of the single step for the call combined with a single step for the
127   label. *)
128
[3007]129definition cminor_rtlabs_meas_sim : meas_sim ≝
130mk_meas_sim
131  Cminor_pcs
132  RTLabs_pcs
133  (λcmp,rap. cminor_to_rtlabs cmp = rap)
134  cminor_rtlabs_inv
135  cminor_rtlabs_rel
136  ? (* rel_normal *)
137  ? (* rel_labelled *)
138  ? (* rel_classify_call *)
139  ? (* rel_classify_return *)
140  ? (* rel_callee *)
141  ? (* labelled_normal_1 *)
142  ? (* labelled_normal_2 *)
143  ? (* notailcalls *)
144  ? (* sim_normal *)
145  ? (* sim_call_nolabel *)
146  ? (* sim_call_label *)
147  ? (* sim_return *)
148  ? (* sim_cost *)
149  ? (* sim_init *)
150.
151[ (* rel_normal *)
152| (* rel_labelled *)
153  @cminor_rtlabs_rel_labelled
154| (* rel_classify_call *)
155| (* rel_classify_return *)
156| (* rel_callee *)
157| (* labelled_normal_1 *)
158  #g * //
159| (* labelled_normal_2 *)
160  #g * // #f #fs #m whd in ⊢ (?% → ?%); whd in match (pcs_classify ???);
161  cases (next_instruction f) //
162| (* notailcalls *)
163  #g @Cminor_notailcalls
164| (* sim_normal *)
165  #g1 #g2 #INV #s1 #s1' #R1 #N1 #NCS1 #s2 #tr #STEP
166  cases (cminor_rtlabs_normal … R1 N1 NCS1 STEP)
167  #m #AFTER %{m} @(after_n_covariant … AFTER)
168  #tr' #s * * #H1 #H2 #H3 /3/
169| (* sim_call_nolabel *)
170  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP #NCS2 %{0}
171  @(cminor_rtlabs_call_return … R1 … STEP)
172  change with (Cminor_classify ?) in CL1:(??%?); >CL1 %
173| (* sim_call_label *)
174  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #STEP1 #CS2 #STEP2 %{1}
175  lapply (cminor_rtlabs_call_return … R1 … STEP1)
176  [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ]
177  #AFTER1 @(after_n_covariant … AFTER1) #tr' #s' * #E #R' destruct
178  % [ %
179  [  %
180  |  change with (RTLabs_cost s') in ⊢ (?%); <(cminor_rtlabs_rel_labelled … R') @CS2
181  ]| lapply (cminor_rtlabs_cost … R' … CS2 STEP2)
182     #AFTER2 cases (after_1_step … AFTER2)
183     #trx * #sx * * #NFx #STEPx * #E #Rx destruct
184     whd >NFx whd >STEPx whd /3/
185  ]
186| (* sim_return *)
187  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP %{0}
188  lapply (cminor_rtlabs_call_return … R1 … STEP)
189  [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ]
190  >(Cminor_return_E0 … STEP CL1)
191  #AFTER %{(refl ??)} @AFTER
192| (* sim_cost *)
193  #g1 #g2 #INV #s1 #s1' #s2 #tr #R1 #CS1 #STEP
194  @(cminor_rtlabs_cost … R1 … STEP)
195  @CS1
196| (* sim_init *)
197  #p #p' #s #COMPILE destruct #INIT
198  cases (cminor_rtlabs_init … INIT) #INV * #s' * #INIT' #R
199  %{s'} % [ @INIT' | %{INV} @R ]
200] cases daemon qed.
Note: See TracBrowser for help on using the repository browser.