Changeset 2464 for src/joint/lineariseProof.ma
- Timestamp:
- Nov 14, 2012, 5:38:57 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/lineariseProof.ma
r2452 r2464 16 16 include "common/StatusSimulation.ma". 17 17 include "joint/Traces.ma". 18 include "joint/SemanticUtils.ma". 19 20 definition graph_prog_params: 21 ∀p:unserialized_params. 22 (∀F.sem_unserialized_params p F) → 23 joint_program (mk_graph_params p) → 24 prog_params 25 ≝ 26 λp,p',prog. 27 (mk_prog_params 28 (make_sem_graph_params (mk_graph_params p) p') 29 prog). 30 31 definition lin_prog_params: 32 ∀p:unserialized_params. 33 (∀F.sem_unserialized_params p F) → 34 joint_program (mk_lin_params p) → 35 prog_params 36 ≝ 37 λp,p',prog. 38 (mk_prog_params 39 (make_sem_lin_params (mk_lin_params p) p') 40 prog). 41 42 (*CSC: Paolo, come to the rescue*) 43 axiom choose_sigma: 44 ∀p:unserialized_params. 45 (∀F.sem_unserialized_params p F) → 46 joint_program (mk_graph_params p) → 47 identifier LabelTag → option ℕ. 48 49 (*CSC: Paolo, come to the rescue*) 50 axiom linearise_code_spec: 51 ∀p : unserialized_params. 52 ∀p':(∀F.sem_unserialized_params p F). 53 ∀graph_prog:joint_program (mk_graph_params p). 54 ∀graph_fun:joint_closed_internal_function (mk_graph_params p) 55 (globals (graph_prog_params p p' graph_prog)). 56 let sigma ≝ choose_sigma p p' graph_prog in 57 let lin_fun ≝ linearise_int_fun … graph_fun in 58 let g ≝ joint_if_code ?? (pi1 … graph_fun) in 59 let c ≝ joint_if_code ?? (pi1 … lin_fun) in 60 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)). 61 code_closed … c ∧ 62 sigma entry = Some ? 0 ∧ 63 ∀l,n.sigma l = Some ? n → 64 ∃s. lookup … g l = Some ? s ∧ 65 opt_Exists ? 66 (λls.let 〈lopt, ts〉 ≝ ls in 67 opt_All ? (eq ? l) lopt ∧ 68 ts = graph_to_lin_statement … s ∧ 69 opt_All ? 70 (λnext.Or (sigma next = Some ? (S n)) 71 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 72 (stmt_implicit_label … s)) (nth_opt … n c). 73 18 include "joint/semanticsUtils.ma". 19 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). 44 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). 49 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. 55 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 74 78 definition graph_abstract_status: 75 79 ∀p:unserialized_params. 76 80 (∀F.sem_unserialized_params p F) → 77 joint_program (mk_graph_params p) → 81 ∀prog : joint_program (mk_graph_params p). 82 ((Σi.is_internal_function_of_program … prog i) → ℕ) → 78 83 abstract_status 79 84 ≝ 80 λp,p',prog. 81 joint_abstract_status (graph_prog_params p p' prog). 85 λp,p',prog,stack_sizes. 86 joint_abstract_status (graph_prog_params ? p' prog stack_sizes). 87 88 definition lin_prog_params ≝ 89 λp,p',prog,stack_sizes. 90 mk_prog_params (make_sem_lin_params p p') prog stack_sizes. 82 91 83 92 definition lin_abstract_status: 84 93 ∀p:unserialized_params. 85 94 (∀F.sem_unserialized_params p F) → 86 joint_program (mk_lin_params p) → 95 ∀prog : joint_program (mk_lin_params p). 96 ((Σi.is_internal_function_of_program … prog i) → ℕ) → 87 97 abstract_status 88 98 ≝ 89 λp,p',prog. 90 joint_abstract_status (lin_prog_params p p' prog). 91 92 (*CSC: BUG, the natural must be ≤ 2^16! *) 93 (*CSC: already defined? *) 94 definition pointer_of_block_and_lin_offset : 95 ∀b:block. block_region b = Code → nat → cpointer ≝ 96 λb,p,n. «mk_pointer b (mk_offset (bitvector_of_nat … n)), p». 99 λp,p',prog,stack_sizes. 100 joint_abstract_status (lin_prog_params ? p' prog stack_sizes). 101 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). 114 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 120 ≝ 121 λp,p',prog,stack_sizes,sigma,pc. 122 sigma_pc_opt p p' prog stack_sizes sigma pc 123 ≠ None …. 97 124 98 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 *) 133 qed. 134 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 161 lemma sigma_pc_of_status_ok: 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 % 202 qed. 203 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 : 99 238 ∀p,p',graph_prog. 100 ∀sigma: identifier LabelTag → option ℕ. 101 graph_abstract_status p p' graph_prog → Prop 102 ≝ 103 λp,p',graph_prog,sigma,s. 104 sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s)) 105 ≠ None …. 106 107 definition sigma_pc_of_status: 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) 251 qed. 252 253 lemma fetch_function_sigma_commute : 108 254 ∀p,p',graph_prog. 109 ∀sigma: identifier LabelTag → option ℕ. 110 ∀s:graph_abstract_status p p' graph_prog. 111 well_formed_status … sigma s → ℕ 112 ≝ 113 λp,p',prog,sigma,s. 114 match sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s)) 115 return λx. x ≠ None ? → ℕ 116 with 117 [ None ⇒ λprf.⊥ 118 | Some n ⇒ λ_.n ]. 119 @(absurd ?? prf) // 120 qed. 121 122 lemma sigma_pc_of_status_ok: 123 ∀p,p',graph_prog. 124 ∀sigma: identifier LabelTag → option ℕ. 125 ∀s:graph_abstract_status p p' graph_prog. 126 ∀prf:well_formed_status … sigma s. 127 sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s)) 128 = Some … (sigma_pc_of_status … prf). 129 #p #p' #prog #sigma #s whd in ⊢ (% → ?); 130 whd in match sigma_pc_of_status; normalize nodelta cases (sigma ?) // 131 #abs cases (absurd ?? abs) 132 qed. 133 134 definition linearise_status_fun: 135 ∀p,p',graph_prog. 136 ∀sigma: identifier LabelTag → option ℕ. 137 let lin_prog ≝ linearise ? graph_prog in 138 ∀s:graph_abstract_status p p' graph_prog. 139 well_formed_status … sigma s → 140 lin_abstract_status p p' lin_prog 141 ≝ 142 λp,p',graph_prog,sigma,s,prf. 143 mk_state_pc ?? 144 (pointer_of_block_and_lin_offset (pblock (pc ? s)) … 145 (sigma_pc_of_status … sigma … prf)). 146 [2: cases (pc ??) * normalize // 147 | cases daemon (* TODO *) ] 148 qed. 149 150 lemma sigma_pc_commute: 151 ∀p,p',graph_prog,s1,prf. 152 sigma_pc_of_status p p' graph_prog (choose_sigma p p' graph_prog) s1 prf = 153 point_of_pointer (lin_prog_params p p' (linearise p graph_prog)) 154 (lin_prog_params p p' (linearise p graph_prog)) 155 (pc (lin_prog_params p p' (linearise p graph_prog)) 156 (linearise_status_fun p p' graph_prog (choose_sigma p p' graph_prog) s1 prf)). 157 #p #p' #prog #s #prf whd in ⊢ (??%%); change with (? = nat_of_bitvector ??); 158 whd in match (pc … (linearise_status_fun …)); 159 >nat_of_bitvector_bitvector_of_nat_inverse // 160 cases daemon (* CSC: Paolo, you must prove this additional invariant! *) 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 275 qed. 276 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 161 342 qed. 162 343 163 344 definition linearise_status_rel: 164 345 ∀p,p',graph_prog. 165 ∀sigma: identifier LabelTag → option ℕ. 166 let lin_prog ≝ linearise ? graph_prog in 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 → 167 353 status_rel 168 (graph_abstract_status p p' graph_prog) 169 (lin_abstract_status p p' lin_prog) 170 ≝ λp,p',graph_prog,sigma.mk_status_rel … 171 (λs1,s2. 172 ∃prf: well_formed_status … sigma s1. 173 s2 = linearise_status_fun p p' graph_prog sigma s1 prf) …. 174 cases daemon (* TODO *) 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 175 379 qed. 176 380 177 381 (* To be added to common/Globalenvs, it strenghtens 178 382 find_funct_ptr_transf *) 383 (* 179 384 lemma 180 385 find_funct_ptr_transf_eq: … … 189 394 | #f #H >(find_funct_ptr_transf A B … H) // ] 190 395 qed. 191 192 lemma fetch_function_sigma_commute: 396 *) 397 398 399 (*lemma fetch_function_sigma_commute: 193 400 ∀p,p',graph_prog,sigma,st1. 194 401 ∀prf:well_formed_status ??? sigma st1. 195 402 let lin_prog ≝ linearise ? graph_prog in 196 fetch_function 403 fetch_function 197 404 (lin_prog_params p p' lin_prog) 198 405 (globals (lin_prog_params p p' lin_prog)) … … 213 420 cases (find_funct_ptr ???) // * // 214 421 qed. 215 216 lemma stm_at_sigma_commute: 217 ∀p,p',graph_prog,graph_fun,s1. 218 let lin_prog ≝ linearise ? graph_prog in 219 let sigma ≝ choose_sigma p p' graph_prog in 220 ∀prf:well_formed_status ??? sigma s1. 221 stmt_at (lin_prog_params p p' (linearise p graph_prog)) 222 (globals (lin_prog_params p p' (linearise p graph_prog))) 223 (joint_if_code (lin_prog_params p p' (linearise p graph_prog)) 224 (globals (lin_prog_params p p' (linearise p graph_prog))) 225 (linearise_int_fun p (globals (graph_prog_params p p' graph_prog)) graph_fun)) 226 (point_of_pointer (lin_prog_params p p' (linearise p graph_prog)) 227 (lin_prog_params p p' (linearise p graph_prog)) 228 (pc (lin_prog_params p p' (linearise p graph_prog)) 229 (linearise_status_fun p p' graph_prog sigma s1 prf))) 230 = 231 option_map … 232 (graph_to_lin_statement …) 233 (stmt_at (graph_prog_params p p' graph_prog) 234 (globals (graph_prog_params p p' graph_prog)) 235 (joint_if_code (graph_prog_params p p' graph_prog) 236 (globals (graph_prog_params p p' graph_prog)) graph_fun) 237 (point_of_pointer (graph_prog_params p p' graph_prog) 238 (graph_prog_params p p' graph_prog) 239 (pc (graph_prog_params p p' graph_prog) s1))). 240 #p #p' #graph_prog #graph_fun #s1 #prf 241 whd in match (stmt_at ????); 242 whd in match (stmt_at ????); 243 cases (linearise_code_spec … p' graph_prog graph_fun 244 (joint_if_entry … graph_fun)) 245 * #lin_code_closed #sigma_entry_is_zero #sigma_spec 246 lapply (sigma_spec 247 (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1))) 248 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ] 249 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok 250 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec; 251 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] 252 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_ 253 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm 254 <sigma_pc_commute >lin_lookup_ok // 255 qed. 256 257 lemma fetch_statement_sigma_commute: 258 ∀p,p',graph_prog,st1. 259 let sigma ≝ choose_sigma p p' graph_prog in 260 let lin_prog ≝ linearise ? graph_prog in 261 ∀prf. 262 fetch_statement 263 (lin_prog_params p p' lin_prog) 264 (lin_prog_params p p' lin_prog) 265 (globals (lin_prog_params p p' lin_prog)) 266 (ev_genv (lin_prog_params p p' lin_prog)) 267 (pc (lin_prog_params p p' lin_prog) 268 (linearise_status_fun p p' graph_prog sigma st1 prf)) 269 = 270 m_map … 271 (λfun_stm. 272 let 〈fun,stm〉 ≝ fun_stm in 273 〈linearise_int_fun ?? fun, graph_to_lin_statement ?? stm〉) 274 (fetch_statement 275 (graph_prog_params p p' graph_prog) 276 (graph_prog_params p p' graph_prog) 277 (globals (graph_prog_params p p' graph_prog)) 278 (ev_genv (graph_prog_params p p' graph_prog)) 279 (pc (graph_prog_params p p' graph_prog) st1)). 280 #p #p' #graph_prog #s1 #prf 281 whd in match fetch_statement; normalize nodelta 282 >fetch_function_sigma_commute 283 cases (fetch_function ????) [2://] 284 #graph_fun whd in ⊢ (??%%); 285 whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?])); 286 >stm_at_sigma_commute cases (stmt_at ????) // 287 qed. 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). 288 427 289 428 lemma linearise_ok: 290 429 ∀p,p',graph_prog. 291 430 let lin_prog ≝ linearise ? graph_prog in 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. 292 436 status_simulation 293 (graph_abstract_status p p' graph_prog) 294 (lin_abstract_status p p' lin_prog) ≝ 295 λp,p',graph_prog. 296 let sigma ≝ choose_sigma p p' graph_prog in 297 mk_status_simulation … (linearise_status_rel p p' graph_prog sigma) …. 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 298 445 #st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl 299 446 cases cl in classified_st1_cl; -cl #classified_st1_cl whd
Note: See TracChangeset
for help on using the changeset viewer.