[2442] | 1 | (**************************************************************************) |
---|
| 2 | (* ___ *) |
---|
| 3 | (* ||M|| *) |
---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
---|
| 5 | (* ||T|| *) |
---|
| 6 | (* ||I|| Developers: *) |
---|
| 7 | (* ||T|| The HELM team. *) |
---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 9 | (* \ / *) |
---|
| 10 | (* \ / This file is distributed under the terms of the *) |
---|
| 11 | (* v GNU General Public License Version 2 *) |
---|
| 12 | (* *) |
---|
| 13 | (**************************************************************************) |
---|
| 14 | |
---|
| 15 | include "joint/linearise.ma". |
---|
| 16 | include "common/StatusSimulation.ma". |
---|
| 17 | include "joint/Traces.ma". |
---|
[2464] | 18 | include "joint/semanticsUtils.ma". |
---|
[2442] | 19 | |
---|
[2464] | 20 | definition good_local_sigma : |
---|
| 21 | ∀p:unserialized_params. |
---|
| 22 | ∀p':(∀F.sem_unserialized_params p F). |
---|
| 23 | ∀globals. |
---|
| 24 | joint_closed_internal_function (mk_graph_params p) globals → |
---|
| 25 | (label → option ℕ) → Prop ≝ |
---|
| 26 | λp,p',globals,graph_fun,sigma. |
---|
| 27 | let lin_fun ≝ linearise_int_fun … graph_fun in |
---|
| 28 | let g ≝ joint_if_code ?? (pi1 … graph_fun) in |
---|
| 29 | let c ≝ joint_if_code ?? (pi1 … lin_fun) in |
---|
| 30 | ∀entry : (Σl.bool_to_Prop (code_has_label … g l)). |
---|
| 31 | code_closed … c ∧ |
---|
| 32 | sigma entry = Some ? 0 ∧ |
---|
| 33 | ∀l,n.sigma l = Some ? n → |
---|
| 34 | lt n 2^offset_size → |
---|
| 35 | ∃s. lookup … g l = Some ? s ∧ |
---|
| 36 | opt_Exists ? |
---|
| 37 | (λls.let 〈lopt, ts〉 ≝ ls in |
---|
| 38 | opt_All ? (eq ? l) lopt ∧ |
---|
| 39 | ts = graph_to_lin_statement … s ∧ |
---|
| 40 | opt_All ? |
---|
| 41 | (λnext.Or (sigma next = Some ? (S n)) |
---|
| 42 | (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) |
---|
| 43 | (stmt_implicit_label … s)) (nth_opt … n c). |
---|
[2445] | 44 | |
---|
[2464] | 45 | axiom prog_if_of_function : |
---|
| 46 | ∀p.∀prog : joint_program p. |
---|
| 47 | (Σi.is_internal_function_of_program … prog i) → |
---|
| 48 | joint_closed_internal_function p (prog_var_names … prog). |
---|
[2446] | 49 | |
---|
[2464] | 50 | definition if_in_global_env_to_if_in_prog : |
---|
| 51 | ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i. |
---|
| 52 | Σi.is_internal_function_of_program ? (prog prog_pars) i ≝ |
---|
| 53 | λprog_pars,f.pi1 ?? f. |
---|
| 54 | @is_internal_function_of_program_ok @(pi2 … f) qed. |
---|
[2446] | 55 | |
---|
[2464] | 56 | coercion if_in_prog_from_if_in_global_env nocomposites : |
---|
| 57 | ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i. |
---|
| 58 | Σi.is_internal_function_of_program ? (prog prog_pars) i ≝ |
---|
| 59 | if_in_global_env_to_if_in_prog |
---|
| 60 | on _f : Sig ident (λi.is_internal_function ??? i) |
---|
| 61 | to Sig ident (λi.is_internal_function_of_program ?? i). |
---|
| 62 | |
---|
| 63 | definition good_sigma : |
---|
| 64 | ∀p:unserialized_params. |
---|
| 65 | ∀p':(∀F.sem_unserialized_params p F). |
---|
| 66 | ∀prog : joint_program (mk_graph_params p). |
---|
| 67 | ((Σi.is_internal_function_of_program … prog i) → label → option ℕ) → Prop ≝ |
---|
| 68 | λp,p',graph_prog,sigma. |
---|
| 69 | ∀i. |
---|
| 70 | let graph_fun ≝ prog_if_of_function ?? i in |
---|
| 71 | let sigma_local ≝ sigma i in |
---|
| 72 | good_local_sigma ? p' ? graph_fun sigma_local. |
---|
| 73 | |
---|
| 74 | definition graph_prog_params ≝ |
---|
| 75 | λp,p',prog,stack_sizes. |
---|
| 76 | mk_prog_params (make_sem_graph_params p p') prog stack_sizes. |
---|
| 77 | |
---|
[2442] | 78 | definition graph_abstract_status: |
---|
| 79 | ∀p:unserialized_params. |
---|
[2443] | 80 | (∀F.sem_unserialized_params p F) → |
---|
[2464] | 81 | ∀prog : joint_program (mk_graph_params p). |
---|
| 82 | ((Σi.is_internal_function_of_program … prog i) → ℕ) → |
---|
[2442] | 83 | abstract_status |
---|
| 84 | ≝ |
---|
[2464] | 85 | λp,p',prog,stack_sizes. |
---|
| 86 | joint_abstract_status (graph_prog_params ? p' prog stack_sizes). |
---|
[2442] | 87 | |
---|
[2464] | 88 | definition lin_prog_params ≝ |
---|
| 89 | λp,p',prog,stack_sizes. |
---|
| 90 | mk_prog_params (make_sem_lin_params p p') prog stack_sizes. |
---|
| 91 | |
---|
[2442] | 92 | definition lin_abstract_status: |
---|
| 93 | ∀p:unserialized_params. |
---|
[2443] | 94 | (∀F.sem_unserialized_params p F) → |
---|
[2464] | 95 | ∀prog : joint_program (mk_lin_params p). |
---|
| 96 | ((Σi.is_internal_function_of_program … prog i) → ℕ) → |
---|
[2442] | 97 | abstract_status |
---|
| 98 | ≝ |
---|
[2464] | 99 | λp,p',prog,stack_sizes. |
---|
| 100 | joint_abstract_status (lin_prog_params ? p' prog stack_sizes). |
---|
[2442] | 101 | |
---|
[2464] | 102 | definition sigma_pc_opt: |
---|
| 103 | ∀p,p',graph_prog,stack_sizes. |
---|
| 104 | ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
| 105 | code_point (mk_graph_params p) → option ℕ) → |
---|
| 106 | cpointer → option cpointer |
---|
| 107 | ≝ |
---|
| 108 | λp,p',prog,stack_sizes,sigma,pc. |
---|
| 109 | let pars ≝ graph_prog_params p p' prog stack_sizes in |
---|
| 110 | let ge ≝ ev_genv pars in |
---|
| 111 | ! f ← int_funct_of_block ?? ge (pblock pc) ; |
---|
| 112 | ! lin_point ← sigma f (point_of_pointer … pars pc) ; |
---|
| 113 | res_to_opt … (pointer_of_point ? (make_sem_lin_params ? p') pc lin_point). |
---|
[2445] | 114 | |
---|
[2464] | 115 | definition well_formed_pc: |
---|
| 116 | ∀p,p',graph_prog,stack_sizes. |
---|
| 117 | ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
| 118 | label → option ℕ) → |
---|
| 119 | cpointer → Prop |
---|
[2445] | 120 | ≝ |
---|
[2464] | 121 | λp,p',prog,stack_sizes,sigma,pc. |
---|
| 122 | sigma_pc_opt p p' prog stack_sizes sigma pc |
---|
[2445] | 123 | ≠ None …. |
---|
| 124 | |
---|
[2464] | 125 | definition well_formed_status: |
---|
| 126 | ∀p,p',graph_prog,stack_sizes. |
---|
| 127 | ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
| 128 | label → option ℕ) → |
---|
| 129 | state_pc (make_sem_graph_params p p') → Prop ≝ |
---|
| 130 | λp,p',prog,stack_sizes,sigma,st. |
---|
| 131 | well_formed_pc p p' prog stack_sizes sigma (pc … st) ∧ ?. |
---|
| 132 | cases daemon (* TODO *) |
---|
[2445] | 133 | qed. |
---|
[2446] | 134 | |
---|
[2464] | 135 | (* |
---|
| 136 | lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?. |
---|
| 137 | [ #p #s #st #prf |
---|
| 138 | whd in match sigma_pc_of_status; normalize nodelta |
---|
| 139 | @opt_safe_elim |
---|
| 140 | #n |
---|
| 141 | lapply (refl … (int_funct_of_block (joint_closed_internal_function p) (globals p) |
---|
| 142 | (ev_genv p) (pblock (pc p st)))) |
---|
| 143 | elim (int_funct_of_block (joint_closed_internal_function p) (globals p) |
---|
| 144 | (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%); |
---|
| 145 | [ #_ #ABS normalize in ABS; destruct(ABS) ] |
---|
| 146 | #f #EQ >m_return_bind |
---|
| 147 | *) |
---|
| 148 | |
---|
| 149 | |
---|
| 150 | (* |
---|
| 151 | lemma wf_status_to_wf_pc : |
---|
| 152 | ∀p,p',graph_prog,stack_sizes. |
---|
| 153 | ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
| 154 | code_point (mk_graph_params p) → option ℕ). |
---|
| 155 | ∀st. |
---|
| 156 | well_formed_status p p' graph_prog stack_sizes sigma st → |
---|
| 157 | well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st). |
---|
| 158 | #p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H |
---|
| 159 | qed. |
---|
| 160 | |
---|
[2446] | 161 | lemma sigma_pc_of_status_ok: |
---|
[2464] | 162 | ∀p,p',graph_prog,stack_sizes. |
---|
| 163 | ∀sigma. |
---|
| 164 | ∀st. |
---|
| 165 | ∀prf:well_formed_status p p' graph_prog stack_sizes sigma st. |
---|
| 166 | sigma_pc_opt p p' graph_prog stack_sizes sigma (pc ? st) = |
---|
| 167 | Some … (sigma_pc_of_status p p' graph_prog stack_sizes sigma st prf). |
---|
| 168 | #p #p' #graph_prog #stack_sizes #sigma #st #prf @opt_to_opt_safe qed. |
---|
| 169 | |
---|
| 170 | *) |
---|
| 171 | |
---|
| 172 | definition sigma_pc : |
---|
| 173 | ∀p,p',graph_prog,stack_sizes. |
---|
| 174 | ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
| 175 | label → option ℕ). |
---|
| 176 | ∀pc. |
---|
| 177 | ∀prf : well_formed_pc p p' graph_prog stack_sizes sigma pc. |
---|
| 178 | cpointer ≝ |
---|
| 179 | λp,p',graph_prog,stack_sizes,sigma,st.opt_safe …. |
---|
| 180 | |
---|
| 181 | definition sigma_state : |
---|
| 182 | ∀p. |
---|
| 183 | ∀p':∀F.sem_unserialized_params p F. |
---|
| 184 | ∀graph_prog,stack_sizes. |
---|
| 185 | ∀sigma. |
---|
| 186 | (* let lin_prog ≝ linearise ? graph_prog in *) |
---|
| 187 | ∀s:state_pc (p' ?). (* = graph_abstract_status p p' graph_prog stack_sizes *) |
---|
| 188 | well_formed_status p p' graph_prog stack_sizes sigma s → |
---|
| 189 | state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) |
---|
| 190 | ≝ |
---|
| 191 | λp,p',graph_prog,stack_sizes,sigma,s,prf. |
---|
| 192 | let pc' ≝ sigma_pc … (proj1 … prf) in |
---|
| 193 | mk_state_pc ? ? pc'. |
---|
| 194 | cases daemon (* TODO *) qed. |
---|
| 195 | |
---|
| 196 | lemma sigma_pc_commute: |
---|
| 197 | ∀p,p',graph_prog,stack_sizes,sigma,st. |
---|
| 198 | ∀prf : well_formed_status p p' graph_prog stack_sizes sigma st. |
---|
| 199 | sigma_pc … (pc ? st) (proj1 … prf) = |
---|
| 200 | pc ? (sigma_state … st prf). |
---|
| 201 | #p #p' #prog #stack_sizes #sigma #st #prf % |
---|
[2446] | 202 | qed. |
---|
| 203 | |
---|
[2464] | 204 | lemma res_eq_from_opt : |
---|
| 205 | ∀A,m,v.res_to_opt A m = return v → m = return v. |
---|
| 206 | #A * #x #v normalize #EQ destruct % qed. |
---|
| 207 | |
---|
| 208 | lemma if_propagate : |
---|
| 209 | ∀pars_in, pars_out : sem_params. |
---|
| 210 | ∀trans : ∀globals.joint_closed_internal_function pars_in globals → |
---|
| 211 | joint_closed_internal_function pars_out globals. |
---|
| 212 | ∀prog_in : program (joint_function pars_in) ℕ. |
---|
| 213 | let prog_out ≝ |
---|
| 214 | transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in |
---|
| 215 | ∀i.is_internal_function_of_program … prog_in i → |
---|
| 216 | is_internal_function_of_program … prog_out i. |
---|
| 217 | cases daemon (* TODO by paolo *) qed. |
---|
| 218 | |
---|
| 219 | definition stack_sizes_lift : |
---|
| 220 | ∀pars_in, pars_out : sem_params. |
---|
| 221 | ∀trans : ∀globals.joint_closed_internal_function pars_in globals → |
---|
| 222 | joint_closed_internal_function pars_out globals. |
---|
| 223 | ∀prog_in : program (joint_function pars_in) ℕ. |
---|
| 224 | let prog_out ≝ |
---|
| 225 | transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in |
---|
| 226 | ((Σi.is_internal_function_of_program … prog_out i) → ℕ) → |
---|
| 227 | ((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝ |
---|
| 228 | λpars_in,pars_out,prog_in,trans,stack_sizes. |
---|
| 229 | λi.stack_sizes «i, if_propagate … (pi2 … i)». |
---|
| 230 | |
---|
| 231 | axiom ok_is_internal_function_of_program : |
---|
| 232 | ∀p.∀prog:joint_program p.∀i. |
---|
| 233 | is_internal_function_of_program p prog i → |
---|
| 234 | is_internal_function ?? (globalenv_noinit ? prog) i. |
---|
| 235 | |
---|
| 236 | |
---|
| 237 | definition sigma_function_name : |
---|
[2445] | 238 | ∀p,p',graph_prog. |
---|
[2464] | 239 | let lin_prog ≝ linearise p graph_prog in |
---|
| 240 | ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. |
---|
| 241 | let graph_stack_sizes ≝ |
---|
| 242 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
| 243 | ? graph_prog lin_stack_sizes in |
---|
| 244 | (Σf.is_internal_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) f) → |
---|
| 245 | (Σf.is_internal_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) f) ≝ |
---|
| 246 | λp,p',graph_prog,lin_stack_sizes,f.pi1 … f. |
---|
| 247 | @ok_is_internal_function_of_program |
---|
| 248 | @(if_propagate (make_sem_graph_params p p') (make_sem_lin_params p p')) |
---|
| 249 | @is_internal_function_of_program_ok |
---|
| 250 | @(pi2 … f) |
---|
[2445] | 251 | qed. |
---|
| 252 | |
---|
[2464] | 253 | lemma fetch_function_sigma_commute : |
---|
| 254 | ∀p,p',graph_prog. |
---|
| 255 | let lin_prog ≝ linearise p graph_prog in |
---|
| 256 | ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. |
---|
| 257 | let graph_stack_sizes ≝ |
---|
| 258 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
| 259 | ? graph_prog lin_stack_sizes in |
---|
| 260 | ∀sigma,pc,f. |
---|
| 261 | ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc. |
---|
| 262 | fetch_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc = |
---|
| 263 | return f |
---|
| 264 | → fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) (sigma_pc … pc prf) = |
---|
| 265 | return sigma_function_name … f. |
---|
| 266 | #p #p' #graph_prog #stack_sizes #sigma #pc #f #prf |
---|
| 267 | (* whd in match fetch_function; normalize nodelta |
---|
| 268 | whd in match function_of_block; normalize nodelta |
---|
| 269 | #H elim (bind_inversion ????? H) -H #fn * |
---|
| 270 | #H lapply (opt_eq_from_res ???? H) -H |
---|
| 271 | #H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H) |
---|
| 272 | -H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%); |
---|
| 273 | destruct // *) |
---|
| 274 | cases daemon |
---|
[2447] | 275 | qed. |
---|
[2446] | 276 | |
---|
[2464] | 277 | lemma if_of_function_commute: |
---|
| 278 | ∀p,p',graph_prog,stack_sizes. |
---|
| 279 | ∀graph_fun. |
---|
| 280 | let graph_fd ≝ if_of_function ??? graph_fun in |
---|
| 281 | let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in |
---|
| 282 | let lin_fd ≝ if_of_function … lin_fun in |
---|
| 283 | lin_fd = linearise_int_fun … graph_fd. |
---|
| 284 | (* usare match_opt_prf_elim ? *) |
---|
| 285 | cases daemon qed. |
---|
| 286 | |
---|
| 287 | lemma stmt_at_sigma_commute: |
---|
| 288 | ∀p,p',graph_prog,stack_sizes,graph_fun,lbl. |
---|
| 289 | let lin_prog ≝ linearise ? graph_prog in |
---|
| 290 | let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in |
---|
| 291 | ∀sigma.good_sigma p p' graph_prog sigma → |
---|
| 292 | ∀prf:sigma graph_fun lbl ≠ None …. |
---|
| 293 | ∃stmt. |
---|
| 294 | stmt_at … |
---|
| 295 | (joint_if_code ?? (if_of_function ??? graph_fun)) |
---|
| 296 | lbl = Some ? stmt ∧ |
---|
| 297 | stmt_at … |
---|
| 298 | (joint_if_code ?? (if_of_function ??? lin_fun)) |
---|
| 299 | (opt_safe … (sigma graph_fun lbl) prf) = Some ? (graph_to_lin_statement … stmt). |
---|
| 300 | #p #p' #graph_prog #stack_sizes #graph_fun #lbl #sigma #good #prf |
---|
| 301 | @opt_safe_elim -prf #n #prf |
---|
| 302 | (* |
---|
| 303 | whd in match (stmt_at ????); |
---|
| 304 | whd in match (stmt_at ????); |
---|
| 305 | cases (linearise_code_spec … p' graph_prog graph_fun |
---|
| 306 | (joint_if_entry … graph_fun)) |
---|
| 307 | * #lin_code_closed #sigma_entry_is_zero #sigma_spec |
---|
| 308 | lapply (sigma_spec |
---|
| 309 | (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1))) |
---|
| 310 | -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ] |
---|
| 311 | -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok |
---|
| 312 | whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec; |
---|
| 313 | inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] |
---|
| 314 | * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_ |
---|
| 315 | #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm |
---|
| 316 | <sigma_pc_commute >lin_lookup_ok // *) |
---|
| 317 | cases daemon |
---|
| 318 | qed. |
---|
| 319 | |
---|
| 320 | lemma fetch_statement_sigma_commute: |
---|
| 321 | ∀p,p',graph_prog,lin_stack_sizes,pc,fn,stmt. |
---|
| 322 | let lin_prog ≝ linearise ? graph_prog in |
---|
| 323 | let graph_stack_sizes ≝ |
---|
| 324 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
| 325 | ? graph_prog lin_stack_sizes in |
---|
| 326 | ∀sigma.good_sigma p p' graph_prog sigma → |
---|
| 327 | ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc. |
---|
| 328 | fetch_statement ? (make_sem_graph_params p p') … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc = |
---|
| 329 | return 〈fn,stmt〉 → |
---|
| 330 | fetch_statement ? (make_sem_lin_params p p') … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) |
---|
| 331 | (sigma_pc … pc prf) = |
---|
| 332 | return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉. |
---|
| 333 | #p #p' #graph_prog #stack_sizes #pc #fn #stmt #good #prf |
---|
| 334 | (* @opt_safe_elim -prf #n #prf |
---|
| 335 | whd in match fetch_statement; normalize nodelta |
---|
| 336 | >fetch_function_sigma_commute |
---|
| 337 | cases (fetch_function ????) [2://] |
---|
| 338 | #graph_fun whd in ⊢ (??%%); |
---|
| 339 | whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?])); |
---|
| 340 | >stm_at_sigma_commute cases (stmt_at ????) // *) |
---|
| 341 | cases daemon |
---|
| 342 | qed. |
---|
| 343 | |
---|
[2442] | 344 | definition linearise_status_rel: |
---|
| 345 | ∀p,p',graph_prog. |
---|
[2464] | 346 | let lin_prog ≝ linearise p graph_prog in |
---|
| 347 | ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. |
---|
| 348 | let stack_sizes' ≝ |
---|
| 349 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
| 350 | ? graph_prog stack_sizes in |
---|
| 351 | ∀sigma. |
---|
| 352 | good_sigma p p' graph_prog sigma → |
---|
[2442] | 353 | status_rel |
---|
[2464] | 354 | (graph_abstract_status p p' graph_prog stack_sizes') |
---|
| 355 | (lin_abstract_status p p' lin_prog stack_sizes) |
---|
| 356 | ≝ λp,p',graph_prog,stack_sizes,sigma,good. |
---|
| 357 | let stack_sizes' ≝ |
---|
| 358 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
| 359 | ? graph_prog ? in |
---|
| 360 | mk_status_rel … |
---|
| 361 | (* sem_rel ≝ *) (λs1,s2. |
---|
| 362 | ∃prf: well_formed_status p p' graph_prog stack_sizes' sigma s1. |
---|
| 363 | s2 = sigma_state … s1 prf) |
---|
| 364 | (* call_rel ≝ *) (λs1,s2. |
---|
| 365 | ∃prf:well_formed_status p p' graph_prog stack_sizes' sigma s1. |
---|
| 366 | pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf)) |
---|
| 367 | (* sim_final ≝ *) ?. |
---|
| 368 | #st1 #st2 * #prf #EQ2 |
---|
| 369 | % |
---|
| 370 | whd in ⊢ (%→%); |
---|
| 371 | #H lapply (opt_to_opt_safe … H) |
---|
| 372 | @opt_safe_elim -H |
---|
| 373 | #res #_ |
---|
| 374 | #H lapply (res_eq_from_opt ??? H) -H |
---|
| 375 | #H elim (bind_inversion ????? H) |
---|
| 376 | * #f #stmt * |
---|
| 377 | whd in ⊢ (??%?→?); |
---|
| 378 | cases daemon |
---|
[2442] | 379 | qed. |
---|
| 380 | |
---|
[2447] | 381 | (* To be added to common/Globalenvs, it strenghtens |
---|
| 382 | find_funct_ptr_transf *) |
---|
[2464] | 383 | (* |
---|
[2447] | 384 | lemma |
---|
| 385 | find_funct_ptr_transf_eq: |
---|
| 386 | ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). |
---|
| 387 | ∀b: block. |
---|
| 388 | find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = |
---|
| 389 | m_map ??? |
---|
| 390 | (transf …) |
---|
| 391 | (find_funct_ptr ? (globalenv … iV p) b). |
---|
| 392 | #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%); |
---|
| 393 | [ cases daemon (* TODO in Globalenvs.ma *) |
---|
| 394 | | #f #H >(find_funct_ptr_transf A B … H) // ] |
---|
| 395 | qed. |
---|
[2464] | 396 | *) |
---|
[2447] | 397 | |
---|
[2464] | 398 | |
---|
| 399 | (*lemma fetch_function_sigma_commute: |
---|
[2445] | 400 | ∀p,p',graph_prog,sigma,st1. |
---|
| 401 | ∀prf:well_formed_status ??? sigma st1. |
---|
| 402 | let lin_prog ≝ linearise ? graph_prog in |
---|
[2464] | 403 | fetch_function |
---|
[2445] | 404 | (lin_prog_params p p' lin_prog) |
---|
| 405 | (globals (lin_prog_params p p' lin_prog)) |
---|
| 406 | (ev_genv (lin_prog_params p p' lin_prog)) |
---|
| 407 | (pc (lin_prog_params p p' lin_prog) |
---|
| 408 | (linearise_status_fun p p' graph_prog sigma st1 prf)) |
---|
| 409 | = |
---|
| 410 | m_map … |
---|
| 411 | (linearise_int_fun ??) |
---|
| 412 | (fetch_function |
---|
| 413 | (graph_prog_params p p' graph_prog) |
---|
| 414 | (globals (graph_prog_params p p' graph_prog)) |
---|
| 415 | (ev_genv (graph_prog_params p p' graph_prog)) |
---|
| 416 | (pc (graph_prog_params p p' graph_prog) st1)). |
---|
[2447] | 417 | #p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta |
---|
| 418 | whd in match function_of_block; normalize nodelta |
---|
| 419 | >(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …) |
---|
| 420 | cases (find_funct_ptr ???) // * // |
---|
| 421 | qed. |
---|
[2464] | 422 | *) |
---|
| 423 | |
---|
| 424 | inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ |
---|
| 425 | ex1_intro: ∀ x:A. P x → ex_Type1 A P. |
---|
| 426 | interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x). |
---|
[2445] | 427 | |
---|
[2442] | 428 | lemma linearise_ok: |
---|
| 429 | ∀p,p',graph_prog. |
---|
| 430 | let lin_prog ≝ linearise ? graph_prog in |
---|
[2464] | 431 | ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. |
---|
| 432 | let graph_stack_sizes ≝ |
---|
| 433 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
| 434 | ? graph_prog lin_stack_sizes in |
---|
| 435 | ∃R. |
---|
[2442] | 436 | status_simulation |
---|
[2464] | 437 | (graph_abstract_status p p' graph_prog graph_stack_sizes) |
---|
| 438 | (lin_abstract_status p p' lin_prog lin_stack_sizes) R. |
---|
| 439 | #p #p' #graph_prog |
---|
| 440 | cut (∃sigma.good_sigma p p' graph_prog sigma) |
---|
| 441 | [ cases daemon (* TODO by Paolo *) ] * #sigma #good |
---|
| 442 | #lin_stack_sizes |
---|
| 443 | %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)} |
---|
| 444 | whd |
---|
[2445] | 445 | #st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl |
---|
| 446 | cases cl in classified_st1_cl; -cl #classified_st1_cl whd |
---|
| 447 | [4: |
---|
[2446] | 448 | cases rel_st1_st2 -rel_st1_st2 #wf_st1 #rel_st1_st2 >rel_st1_st2 -st2 |
---|
[2445] | 449 | whd in move_st1_st1'; |
---|
| 450 | letin lin_prog ≝ (linearise ? graph_prog) |
---|
[2452] | 451 | |
---|
| 452 | cut (joint_closed_internal_function (mk_graph_params p) (globals (graph_prog_params p p' graph_prog))) [cases daemon (*???*)] #graph_fun |
---|
| 453 | |
---|
| 454 | cases (linearise_code_spec … p' graph_prog graph_fun |
---|
| 455 | (joint_if_entry … graph_fun)) |
---|
| 456 | * #lin_code_closed #sigma_entry_is_zero #sigma_spec |
---|
| 457 | lapply (sigma_spec |
---|
| 458 | (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … st1))) |
---|
| 459 | -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … wf_st1) |2: skip ] |
---|
| 460 | -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec whd in sigma_spec; |
---|
| 461 | inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] |
---|
| 462 | * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved |
---|
| 463 | #related_lin_stm_graph_stm |
---|
| 464 | inversion (stmt_implicit_label ???) |
---|
| 465 | [ whd in match (opt_All ???); #stmt_implicit_spec #_ |
---|
| 466 | letin st2_opt' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) … |
---|
[2445] | 467 | (ev_genv (lin_prog_params p p' lin_prog)) |
---|
[2446] | 468 | (linearise_status_fun … sigma st1 wf_st1)) |
---|
[2452] | 469 | check st2_opt' |
---|
| 470 | cut (∃st2': lin_abstract_status p p' lin_prog. st2_opt' = return st2') |
---|
| 471 | [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec' |
---|
| 472 | normalize nodelta in st2_spec'; -st2_opt' |
---|
| 473 | %{st2'} %{(taaf_step … (taa_base …) …)} |
---|
| 474 | [ cases daemon (* TODO, together with the previous one? *) |
---|
| 475 | | @st2_spec' ] |
---|
| 476 | %[%] [%] |
---|
| 477 | [ whd |
---|
| 478 | whd in st2_spec':(??%?); >fetch_statement_sigma_commute in st2_spec'; |
---|
| 479 | whd in move_st1_st1':(??%?); |
---|
| 480 | cut (fetch_statement (graph_prog_params p p' graph_prog) (graph_prog_params … graph_prog) … (ev_genv (graph_prog_params … graph_prog)) … (pc … st1) = OK ? 〈graph_fun,graph_stmt〉) |
---|
| 481 | [ cases daemon (* TODO once and for all, consequence of graph_lookup_ok *) ] |
---|
| 482 | #fetch_statement_ok >fetch_statement_ok in move_st1_st1'; |
---|
| 483 | whd in ⊢ (??%? → ??%? → ?); normalize nodelta |
---|
| 484 | inversion graph_stmt in stmt_implicit_spec; normalize nodelta |
---|
| 485 | [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ] |
---|
| 486 | XXXXXXXXXX siamo qua, caso GOTO e RETURN |
---|
| 487 | | cases daemon (* TODO, after the definition of label_rel, trivial *) ] |
---|
| 488 | ] |
---|
| 489 | | .... |
---|
[2447] | 490 | qed. |
---|