[2511] | 1 | |
---|
[2601] | 2 | include "Cminor/Cminor_abstract.ma". |
---|
| 3 | include "RTLabs/RTLabs_abstract.ma". |
---|
[2597] | 4 | include "Cminor/toRTLabs.ma". |
---|
[2511] | 5 | |
---|
[3007] | 6 | record cminor_rtlabs_inv (ge_cm:cm_genv) (ge_ra:RTLabs_genv) : Type[0] ≝ { |
---|
[2511] | 7 | }. |
---|
[3007] | 8 | axiom cminor_rtlabs_rel : ∀gc,gr. cminor_rtlabs_inv gc gr → Cminor_state → RTLabs_state → Prop. |
---|
[2511] | 9 | |
---|
[3007] | 10 | axiom 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 | |
---|
| 40 | definition cminor_normal : Cminor_state → bool ≝ |
---|
| 41 | λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
| 42 | |
---|
| 43 | definition rtlabs_normal : RTLabs_state → bool ≝ |
---|
| 44 | λs. match RTLabs_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
| 45 | |
---|
[3007] | 46 | axiom cminor_measure : Cminor_state → nat. |
---|
| 47 | |
---|
[2511] | 48 | axiom 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 | |
---|
| 62 | axiom 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 | |
---|
| 74 | axiom 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] | 86 | axiom 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] | 94 | include "common/FEMeasurable.ma". |
---|
| 95 | include "Cminor/Cminor_classified_system.ma". |
---|
| 96 | include "RTLabs/RTLabs_classified_system.ma". |
---|
[2597] | 97 | |
---|
[3007] | 98 | include "common/ExtraMonads.ma". |
---|
| 99 | |
---|
| 100 | lemma 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] | 129 | definition cminor_rtlabs_meas_sim : meas_sim ≝ |
---|
| 130 | mk_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. |
---|