- Timestamp:
- Jul 16, 2012, 4:59:09 PM (9 years ago)
- Location:
- src
- Files:
-
- 6 edited
- 1 moved
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/RTL_paolo.ma
r2155 r2186 59 59 definition rtl_statement ≝ joint_statement rtl_params. 60 60 61 interpretation "move" 'mov r a = (MOVE ?? (mk_Prod ? rtl_argument r a)).61 interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? rtl_argument r a)). 62 62 63 63 (* aid unification *) -
src/common/StructuredTraces.ma
r2129 r2186 334 334 qed. 335 335 336 (* an uncalling, unreturning and *unjumping*, 337 as well as unlabelled (but possibly for the first and last statuses) 338 possibly empty trace segment *) 339 inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝ 340 | taa_base : 336 (* 337 (* an trace of unlabeled and cl_other states, possibly empty *) 338 inductive trace_no_label_any (S:abstract_status) : S → S → Type[0] ≝ 339 | tna_base : 341 340 ∀start_status: S. 342 trace_any_any S start_status start_status 343 | taa_step : 341 ¬as_costed … start_status → 342 trace_no_label_any S start_status start_status 343 | tna_step : 344 344 ∀status_pre: S. 345 345 ∀status_init: S. 346 346 ∀status_end: S. 347 347 as_execute S status_pre status_init → 348 trace_any_any S status_init status_end →349 348 as_classifier S status_pre cl_other → 350 ¬as_costed … status_init → 351 trace_any_any S status_pre status_end. 352 353 let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝ 349 ¬as_costed … status_pre → 350 trace_no_label_any S status_init status_end → 351 trace_no_label_any S status_pre status_end. 352 353 let rec tna_append_tna S st1 st2 st3 (taa1 : trace_no_label_any S st1 st2) 354 on taa1 : 355 trace_no_label_any S st2 st3 → 356 trace_no_label_any S st1 st3 ≝ 357 match taa1 with 358 [ tna_base st1' H ⇒ λtaa2.taa2 359 | tna_step st1' st2' st3' H G K tl ⇒ 360 λtaa2.tna_step ???? H G K (tna_append_tna … tl taa2) 361 ]. 362 363 definition tna_non_empty ≝ λS,st1,st2.λtna : trace_no_label_any S st1 st2. 364 match tna with 365 [ tna_base _ _ ⇒ false 366 | tna_step _ _ _ _ _ _ _ ⇒ true 367 ]. 368 369 coercion tna_to_bool : ∀S,st1,st2.∀tna:trace_no_label_any S st1 st2.bool ≝ 370 tna_non_empty on _tna : trace_no_label_any ??? to bool. 371 372 lemma tna_unlabelled : ∀S,st1,st2.trace_no_label_any S st1 st2 → ¬as_costed … st1. 373 #S #st1 #st2 * [#st #H @H | #st #st' #st'' #_ #_ #H #_ @H] qed. 374 375 let rec tna_append_tal S st1 fl st2 st3 (tna : trace_no_label_any S st1 st2) 376 on tna : 377 trace_any_label S fl st2 st3 → 378 if tna then Not (as_costed … st2) else True → 379 trace_any_label S fl st1 st3 ≝ 380 match tna return λst1,st2.λx : trace_no_label_any S st1 st2. 381 ∀fl,st3. 382 trace_any_label S fl st2 st3 → 383 if x then Not (as_costed … st2) else True → 384 trace_any_label S fl st1 st3 385 with 386 [ tna_base st1' H ⇒ λfl,st3,taa2,prf.taa2 387 | tna_step st1' st2' st3' H G K tl ⇒ λfl,st3,taa2,prf. 388 tal_step_default ????? H (tna_append_tal ????? tl taa2 ?) G (tna_unlabelled … tl) 389 ] fl st3. 390 cases (tna_non_empty … tl) [@prf|%] 391 qed. 392 *) 393 394 inductive trace_any_any (S : abstract_status) : S → S → Type[0] ≝ 395 | taa_base : ∀st.trace_any_any S st st 396 | taa_step : ∀st1,st2,st3. 397 as_execute S st1 st2 → 398 as_classifier S st1 cl_other → 399 ¬as_costed S st2 → 400 trace_any_any S st2 st3 → 401 trace_any_any S st1 st3. 402 403 definition taa_non_empty ≝ λS,st1,st2.λtaa : trace_any_any S st1 st2. 354 404 match taa with 355 [ taa_base st1' ⇒ [st1']356 | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl405 [ taa_base _ ⇒ false 406 | taa_step _ _ _ _ _ _ _ ⇒ true 357 407 ]. 358 408 359 let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2) 360 on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝ 361 match taa1 362 return λst1,st2.λx : trace_any_any S st1 st2. 363 trace_any_any S st2 st3 → trace_any_any S st1 st3 364 with 365 [ taa_base _ ⇒ λtaa2.taa2 366 | taa_step st1' st2' st3' H tl G K ⇒ λtaa2. 367 taa_step … H (taa_append_taa … tl taa2) G K 368 ]. 369 370 let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2) 371 on taa : 409 coercion taa_to_bool : ∀S,st1,st2.∀taa:trace_any_any S st1 st2.bool ≝ 410 taa_non_empty on _taa : trace_any_any ??? to bool. 411 412 let rec taa_append_tal S st1 fl st2 st3 413 (taa : trace_any_any S st1 st2) on taa : 372 414 trace_any_label S fl st2 st3 → 373 415 trace_any_label S fl st1 st3 ≝ 374 match taa 375 return λst1,st2.λx : trace_any_any S st1 st2. 376 trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3 416 match taa return λst1,st2.λx : trace_any_any S st1 st2. 417 ∀fl,st3. 418 trace_any_label S fl st2 st3 → 419 trace_any_label S fl st1 st3 377 420 with 378 [ taa_base _ ⇒ λtaa2.taa2 379 | taa_step st1' st2' st3' H tl G K ⇒ λtaa2. 380 tal_step_default … H (taa_append_tal … tl taa2) G K 381 ]. 421 [ taa_base st1' ⇒ λfl,st3,tal2.tal2 422 | taa_step st1' st2' st3' H G K tl ⇒ λfl,st3,tal2. 423 tal_step_default ????? H (taa_append_tal ????? tl tal2) G K 424 ] fl st3. 425 426 interpretation "trace any any label append" 'append taa tal = (taa_append_tal ????? taa tal). 382 427 383 428 let rec tlr_rel S1 st1 st1' S2 st2 st2' … … 416 461 fl2 = doesnt_end_with_ret ∧ 417 462 ∃st2mid,taa,H,G,K. 418 tal2 ≃ taa_append_tal ? st2 ? st2mid st2'taa463 tal2 ≃ taa_append_tal ? st2 ??? taa 419 464 (tal_base_not_return ? st2mid st2' H G K) 420 465 | tal_base_return st1 st1' _ _ ⇒ … … 437 482 tal_rel … tl1 tal2 (* <- this makes it many to many *) 438 483 ]. 439 484 440 485 interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2). 441 486 interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2). 442 interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ???????? t1 t2). 443 487 interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ?????? t1 t2). 488 489 let rec taa_rel_inv S1 fl1 st1 st1mid st1' S2 fl2 st2 st2' 490 (taa1 : trace_any_any S1 st1 st1mid) on taa1 : 491 ∀tal1 : trace_any_label S1 fl1 st1mid st1'. 492 ∀tal2 : trace_any_label S2 fl2 st2 st2'. 493 tal_rel … (taa1 @ tal1) tal2 → 494 tal_rel … tal1 tal2 ≝ ?. 495 cases taa1 -taa1 496 [ -taa_rel_inv // 497 | #st #st' #st'' #H #G #K #tl #tal1 #tal2 whd in ⊢ (%→?); 498 @(taa_rel_inv … tl) 499 ] 500 qed. 501 502 let rec tlr_rel_transitive S1 st1 st1' S2 st2 st2' S3 st3 st3' 503 (tlr1 : trace_label_return S1 st1 st1') 504 (tlr2 : trace_label_return S2 st2 st2') 505 (tlr3 : trace_label_return S3 st3 st3') on tlr1 : 506 tlr_rel … tlr1 tlr2 → tlr_rel … tlr2 tlr3 → tlr_rel … tlr1 tlr3 ≝ 507 match tlr1 with 508 [ tlr_base st1' st1'' tll1 ⇒ ? 509 | tlr_step st1' st1'' st1''' tll1 tl1 ⇒ ? 510 ] 511 and tll_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3' 512 (tll1 : trace_label_label S1 fl1 st1 st1') 513 (tll2 : trace_label_label S2 fl2 st2 st2') 514 (tll3 : trace_label_label S3 fl3 st3 st3') on tll1 : 515 tll1 ≈ tll2 → tll2 ≈ tll3 → tll1 ≈ tll3 ≝ 516 match tll1 with 517 [ tll_base fl1' st1' st1'' tal1 H ⇒ ? 518 ] 519 and tal_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3' 520 (tal1 : trace_any_label S1 fl1 st1 st1') 521 (tal2 : trace_any_label S2 fl2 st2 st2') 522 (tal3 : trace_any_label S3 fl3 st3 st3') on tal1 : 523 tal1 ≈ tal2 → tal2 ≈ tal3 → tal1 ≈ tal3 ≝ 524 match tal1 with 525 [ tal_base_not_return st1' st1'' H G K ⇒ ? 526 | tal_base_return st1' st1'' H G ⇒ ? 527 | tal_base_call st1' st1'' st1''' H G K tlr1 L ⇒ ? 528 | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ? 529 | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ? 530 ]. 531 [1,2: cases tlr2 #st2' #st2'' [1,3: #tllhd2 |2,4: #st2''' #tllhd2 #tlrtl2] 532 [2,3: *] normalize in ⊢ (%→?); [ #Rhd12 | * #Rhd12 #Rtl12 ] 533 cases tlr3 #st3' #st3'' [1,3: #tllhd3 |2,4: #st3''' #tllhd3 #tlrtl3] 534 [2,3: *] normalize in ⊢ (%→?); [ #Rhd23 | * #Rhd23 #Rtl23 ] whd 535 [ @(tll_rel_transitive … Rhd12 Rhd23) | 536 %{(tll_rel_transitive … Rhd12 Rhd23)} 537 @(tlr_rel_transitive … Rtl12 Rtl23) 538 ] 539 |3: 540 cases tll2 #fl2' #st2' #st2'' #tal2 #H2 * #G2 #R12 541 cases tll3 #fl3' #st3' #st3'' #tal3 #H3 * #G3 #R23 542 %{(tal_rel_transitive … R12 R23)} // 543 |*: 544 [1,2,3: * #EQ] 545 [5: whd in ⊢ (%→?→%); @tal_rel_transitive] 546 *#st2mid *#taa2 547 [ *#H2 *#G2 *#K2 #R12 548 | *#H2 *#G2 #R12 549 | *#st2' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#R12 #R12' 550 | *#st2' *#st2'' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #R12 #R12' #R12'' 551 ] destruct #R23 lapply (taa_rel_inv … R23) [1,2: // |3: *#EQ destruct] 552 *#st3mid *#taa3 553 [ *#st3' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#R23 #R23' 554 %{(refl …)} %{st3mid} %{taa3} %{st3'} %{H3} %{G3} %{K3} %{tlr3} %{L3} 555 %{R23} @(tlr_rel_transitive … R12' R23') 556 | *#st3' *#st3'' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#tl3 ** #R23 #R23' #R23'' 557 %{st3mid} %{taa3} %{st3'} %{st3''} %{H3} %{G3} %{K3} %{tlr3} %{L3} %{tl3} 558 %{(tal_rel_transitive … R12'' R23'')} 559 %{R23} @(tlr_rel_transitive … R12' R23') 560 ] 561 ] 562 qed. 444 563 445 564 let rec flatten_trace_label_label … … 507 626 S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa : 508 627 ∀tal : trace_any_label S fl st2 st3. 509 flatten_trace_any_label … (taa _append_tal … taatal) =628 flatten_trace_any_label … (taa @ tal) = 510 629 flatten_trace_any_label … tal ≝ ?. 511 630 cases taa -st1 -st2 512 [ #st1 #tal %513 | #st_pre #st_init #st2 #H # taa #G #K#tal514 whd in match ( taa_append_tal ???????);631 [ // 632 | #st_pre #st_init #st2 #H #G #K #taa' #tal 633 whd in match (? @ ?); 515 634 whd in ⊢ (??%?); // 516 635 ] 517 qed. 518 636 qed. 519 637 520 638 let rec tll_rel_to_traces_same_flatten … … 606 724 λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ. 607 725 608 definition lift_cost_map_id : 609 ∀S_in, S_out: abstract_status. 610 (∀l. (∃pc.as_label_of_pc S_out pc = Some … l) + 611 ¬(∃pc.as_label_of_pc S_out pc = Some … l)) → 612 (as_cost_map S_out) → as_cost_map S_in ≝ λS_in,S_out,dec,m,l_sig. 613 match dec l_sig with 614 [ inl prf ⇒ m «l_sig, prf» 615 | inr _ ⇒ 0 (* labels not present in out code get 0 *) 726 definition lift_sigma_map_id : 727 ∀A,B : Type[0].∀P_in,P_out : A → Prop.B → 728 (∀a.P_out a + ¬ P_out a) → 729 ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig. 730 match dec a_sig with 731 [ inl prf ⇒ m «a_sig, prf» 732 | inr _ ⇒ dflt (* labels not present in out code get 0 *) 616 733 ]. 617 734 618 lemma lift_cost_map_id_eq : 619 ∀S_in, S_out, dec, m, l_in, l_out. 620 pi1 ?? l_in = pi1 ?? l_out → lift_cost_map_id S_in S_out dec m l_in = m l_out. 621 #S_in #S_out #dec #m #l_in * #l_out #prf #EQ 622 whd in match lift_cost_map_id; normalize nodelta 623 cases (dec l_in) normalize nodelta >EQ 624 [2: #H @⊥] /2 by refl, absurd/ 735 lemma lift_sigma_map_id_eq : 736 ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out. 737 pi1 ?? a_in = pi1 ?? a_out → 738 lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out. 739 #A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ 740 whd in match lift_sigma_map_id; normalize nodelta 741 cases (dec a_in) normalize nodelta >EQ cases a_out 742 #a #H #G [ % | @⊥ /2 by absurd/ ] 625 743 qed. 626 744 … … 631 749 with precedence 20 632 750 for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}. 751 752 definition lift_cost_map_id : 753 ∀S_in,S_out : abstract_status.? → 754 as_cost_map S_out → as_cost_map S_in 755 ≝ 756 λS_in,S_out : abstract_status. 757 lift_sigma_map_id costlabel ℕ 758 (λl.∃pc.as_label_of_pc S_in pc = Some ? l) 759 (λl.∃pc.as_label_of_pc S_out pc = Some ? l) 760 0. 633 761 634 762 lemma lift_cost_map_same_cost : … … 645 773 #EQ destruct 646 774 whd in ⊢(??%%); 647 >(lift_cost_map_id_eq … e0) 775 whd in match lift_cost_map_id; normalize nodelta 776 >(lift_sigma_map_id_eq ????????? e0) 648 777 >e0 in e1; normalize in ⊢(%→?); #EQ 649 778 >(IH … EQ) % -
src/joint/Joint_paolo.ma
r2182 r2186 181 181 match s with 182 182 [ GOTO l ⇒ Labels … [l] 183 | _ ⇒ Labels … [ ] (* tailcalls will need to be integrated in structured traces *) 183 | tailcall _ ⇒ Call (* tailcalls will need to be integrated in structured traces *) 184 | _ ⇒ Labels … [ ] 184 185 ]. 185 186 -
src/joint/Traces.ma
r1976 r2186 1 1 include "joint/semantics_paolo.ma". 2 include "common/StructuredTraces.ma".3 2 4 definition stmt_classifier : 5 ∀p : params.∀globals. 6 (ext_step p → status_class) → 7 (ext_fin_stmt p → status_class) → 8 joint_statement p globals → status_class 9 ≝ λp,globals,ext_step_classifier,ext_fin_step_classifier,s. 10 match s with 11 [ sequential stp _ ⇒ 12 match stp with 13 [ COND _ _ ⇒ cl_jump 14 | extension ext_s ⇒ ext_step_classifier ext_s 15 | CALL_ID _ _ _ ⇒ cl_call (* Paolo : this does not take into account external calls! *) 16 | _ ⇒ cl_other 17 ] 18 | final stp ⇒ 19 match stp with 20 [ RETURN ⇒ cl_return 21 | extension_fin ext_s ⇒ ext_fin_step_classifier ext_s 22 | _ ⇒ cl_other 23 ] 24 ]. 3 record evaluation_params : Type[1] ≝ 4 { globals: list ident 5 ; sparams:> sem_params 6 ; exit: cpointer 7 ; ev_genv: genv globals sparams 8 ; io_env : state sparams → ∀o:io_out.res (io_in o) 9 } . 10 11 (*record classifier_params : Type[1] ≝ 12 { cl_pars :> evaluation_parameters 13 ; cl_ext_step : ext_step cl_pars → status_class 14 ; cl_ext_fin_stmt : ext_fin_stmt cl_pars → status_class 15 }.*) 16 25 17 26 18 definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?. … … 30 22 ] 31 23 qed. 32 24 25 let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝ 26 match c with 27 [ Value x ⇒ OK … x 28 | Interact o f ⇒ 29 ! i ← env o ; 30 io_evaluate O I X env (f i) 31 | Wrong e ⇒ Error … e 32 ]. 33 34 definition cost_label_of_stmt : 35 ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝ 36 λp,s.match s with 37 [ sequential s _ ⇒ 38 match s with 39 [ step_seq s ⇒ 40 match s with 41 [ COST_LABEL lbl ⇒ Some ? lbl 42 | _ ⇒ None ? 43 ] 44 | _ ⇒ None ? 45 ] 46 | _ ⇒ None ? 47 ]. 48 33 49 definition joint_abstract_status : 34 ∀p : evaluation_parameters. 35 (ext_step p → status_class) → 36 (ext_fin_stmt p → status_class) → 37 abstract_status ≝ 38 λp,ext_step_cl,ext_fin_step_cl. 50 ∀p : evaluation_params. 51 abstract_status ≝ 52 λp. 39 53 mk_abstract_status 40 54 (* as_status ≝ *) (state_pc p) 41 (* as_execute ≝ *) (λs1,s2.eval_state … p (genv2 p) s1 = return s2) 55 (* as_execute ≝ *) 56 (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2) 42 57 (* as_pc ≝ *) cpointerDeq 43 58 (* as_pc_of ≝ *) (pc …) 44 59 (* as_classifier ≝ *) 45 (λs,cl.∃stmt.fetch_statement ? p … ( genv2p) (pc … s) = return stmt ∧46 stmt_classifier … ext_step_cl ext_fin_step_clstmt = cl)60 (λs,cl.∃stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return stmt ∧ 61 stmt_classifier … stmt = cl) 47 62 (* as_label_of_pc ≝ *) 48 63 (λpc. 49 match fetch_statement ? p … (genv2 p) pc with 50 [ OK stmt ⇒ 51 match stmt with 52 [ sequential s _ ⇒ 53 match s with 54 [ COST_LABEL l ⇒ Some ? l 55 | _ ⇒ None ? 56 ] 57 | _ ⇒ None ? 58 ] 64 match fetch_statement ? p … (ev_genv p) pc with 65 [ OK stmt ⇒ cost_label_of_stmt … stmt 59 66 | _ ⇒ None ? 60 67 ]) 61 68 (* as_after_return ≝ *) 62 (λs1,s2. (* Paolo: considering sequential calls, tailcalls are out of the picture for now *) 63 ∃stp,nxt.fetch_statement ? p … (genv2 p) (pc … s1) = return (sequential ?? stp nxt) ∧ 69 (λs1,s2. 70 (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *) 71 ∃stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return (sequential ?? stp nxt) ∧ 64 72 succ_pc p p (pc … s1) nxt = return pc … s2) 65 (* as_final ≝ *) (λs.is_final (globals ?) p ( genv2p) (exit p) s ≠ None ?).73 (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?). -
src/joint/blocks.ma
r2155 r2186 176 176 ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝ 177 177 bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??). 178 179 notation > "x ~❨ B , l ❩~> y 'in' c" with precedence 56 for 180 @{'block_in_code $c $x $B $l $y}. 181 182 notation < "hvbox(x ~❨ B , l ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for 183 @{'block_in_code $c $x $B $l $y}. 184 185 definition step_in_code ≝ 186 λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_step p globals. 187 λdst : code_point p. 188 ∃nxt.stmt_at … c src = Some ? (sequential … s nxt) ∧ 189 point_of_succ … src nxt = dst. 190 191 definition fin_step_in_code ≝ 192 λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_fin_step p. 193 stmt_at … c src = Some ? (final … s). 194 195 let rec seq_list_in_code p globals (c : codeT p globals) 196 (src : code_point p) (B : list (joint_seq p globals)) 197 (l : list (code_point p)) (dst : code_point p) on B : Prop ≝ 198 match B with 199 [ nil ⇒ 200 match l with 201 [ nil ⇒ src = dst 202 | _ ⇒ False 203 ] 204 | cons hd tl ⇒ 205 match l with 206 [ nil ⇒ False 207 | cons mid rest ⇒ 208 step_in_code … c src hd mid ∧ seq_list_in_code … c mid tl rest dst 209 ] 210 ]. 211 212 interpretation "seq list in code" 'block_in_code c x B l y = (seq_list_in_code ?? c x B l y). 213 214 lemma seq_list_in_code_append : 215 ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst. 216 src ~❨B1,l1❩~> mid in c → mid ~❨B2,l2❩~> dst in c → 217 src ~❨B1@B2,l1@l2❩~> dst in c. 218 #p #globals #c #src #B1 lapply src -src elim B1 219 [ #src * [2: #mid' #rest] #mid #B2 #l2 #dst [*] #EQ normalize in EQ; destruct(EQ) 220 #H @H 221 | #hd #tl #IH #src * [2: #mid' #rest] #mid #B2 #l2 #dst * #H1 #H2 222 #H3 %{H1 (IH … H2 H3)} 223 ] 224 qed. 225 226 lemma seq_list_in_code_append_inv : 227 ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst. 228 src ~❨B1@B2,l❩~> dst in c → 229 ∃l1,mid,l2.l = l1 @ l2 ∧ src ~❨B1,l1❩~> mid in c ∧ mid ~❨B2,l2❩~> dst in c. 230 #p #globals #c #src #B1 lapply src -src elim B1 231 [ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % % 232 | #hd #tl #IH #src #B2 * [2: #mid #rest] #dst * #H1 #H2 233 elim (IH … H2) #l1 * #mid' * #l2 ** #G1 #G2 #G3 234 %{(mid::l1)} %{mid'} %{l2} %{G3} >G1 %{(refl …)} 235 %{H1 G2} 236 ] 237 qed. 238 239 definition seq_block_step_in_code ≝ 240 λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst. 241 src ~❨\fst B, \fst l❩~> \snd l in c ∧ step_in_code … c (\snd l) (\snd B) dst. 242 243 definition seq_block_fin_step_in_code ≝ 244 λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit. 245 src ~❨\fst B, \fst l❩~> \snd l in c ∧ fin_step_in_code … c (\snd l) (\snd B). 246 247 (* generates ambiguity even if it shouldn't 248 interpretation "seq block step in code" 'block_in_code c x B l y = (seq_block_step_in_code ?? c x B l y). 249 interpretation "seq block fin step in code" 'block_in_code c x B l y = (seq_block_fin_step_in_code ?? c x B l y). 250 *) 178 251 179 252 (* -
src/joint/semantics_blocks.ma
r2043 r2186 1 1 include "joint/blocks.ma". 2 include "joint/semantics_paolo.ma". 3 4 5 axiom ExecutingInternalCallInBlock : String. 6 7 let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝ 2 include "joint/Traces.ma". 3 4 (* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝ 8 5 match b with 9 6 [ nil ⇒ [ ] 10 7 | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl 11 ]. 12 13 definition step_flow_change_labels : 14 ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) → 15 step_flow p g lbls1 → step_flow p g lbls2 ≝ 16 λp,g,lbls1,lbls2,prf,flow. 17 match flow with 18 [ Redirect l ⇒ Redirect ??? «l, prf ? (pi2 … l)» 19 | Init id b args dest ⇒ Init … id b args dest 20 | Proceed ⇒ Proceed ??? 21 ]. 22 23 coercion step_flow_diff_lbls : 24 ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) → 25 ∀flow : step_flow p g lbls1.step_flow p g lbls2 ≝ 26 step_flow_change_labels on _flow : step_flow ??? to step_flow ???. 27 28 definition monad_step_flow_times_coerc : 29 ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) → 30 monad M ((step_flow p g lbls1) × A) → monad M ((step_flow p g lbls2) × A) ≝ 31 λp,g,lbls1,lbls2,M,A,H,m. 32 ! 〈flow,a〉 ← m ; 33 return 〈(flow : step_flow ?? lbls2),a〉. assumption qed. 34 35 coercion step_flow_monad_times : 36 ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) → 37 ∀m : monad M ((step_flow p g lbls1) × A).monad M ((step_flow p g lbls2) × A) ≝ 38 monad_step_flow_times_coerc on _m : monad ? ((step_flow ???) × ?) to monad ? ((step_flow ???) × ?). 39 40 let rec eval_seq_list globals (p:sem_params) (ge : genv globals p) 41 (st : state p) (b : list (joint_step p globals)) on b : 42 IO io_out io_in ((step_flow p globals (seq_list_labels … b)) × (state p)) ≝ 43 match b return λx.IO ?? ((step_flow ?? (seq_list_labels … x)) × ?) with 44 [ nil ⇒ return 〈Proceed ???, st〉 45 | cons hd tl ⇒ 46 ! 〈flow, st'〉 ← eval_step … ge st hd ; 47 match flow return λ_.IO ?? ((step_flow ?? (seq_list_labels … (hd :: tl))) × ?) with 48 [ Proceed ⇒ eval_seq_list globals p ge st' tl 49 | _ ⇒ return 〈flow, st'〉 50 ] 51 ]. /2 by Exists_append_r, Exists_append_l/ qed. 52 53 definition fin_step_flow_change_labels : 54 ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) → 55 fin_step_flow p g lbls1 → fin_step_flow p g lbls2 ≝ 56 λp,g,lbls1,lbls2,prf,flow. 57 match flow with 58 [ FRedirect l ⇒ FRedirect ??? «l, prf ? (pi2 … l)» 59 | FTailInit id b args ⇒ FTailInit … id b args 60 | FEnd ⇒ FEnd ??? 61 ]. 62 63 coercion fin_step_flow_diff_lbls : 64 ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) → 65 ∀flow : fin_step_flow p g lbls1.fin_step_flow p g lbls2 ≝ 66 fin_step_flow_change_labels on _flow : fin_step_flow ??? to fin_step_flow ???. 67 68 definition monad_fin_step_flow_times_coerc : 69 ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) → 70 monad M ((fin_step_flow p g lbls1) × A) → monad M ((fin_step_flow p g lbls2) × A) ≝ 71 λp,g,lbls1,lbls2,M,A,H,m. 72 ! 〈flow,a〉 ← m ; 73 return 〈(flow : fin_step_flow ?? lbls2),a〉. assumption qed. 74 75 coercion fin_step_flow_monad_times : 76 ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) → 77 ∀m : monad M ((fin_step_flow p g lbls1) × A).monad M ((fin_step_flow p g lbls2) × A) ≝ 78 monad_fin_step_flow_times_coerc on _m : monad ? ((fin_step_flow ???) × ?) to monad ? ((fin_step_flow ???) × ?). 79 80 definition block_cont_labels ≝ λp,g,ty.λb : block_cont p g ty. 81 seq_list_labels … (\fst b) @ 82 match ty return λx.stmt_type_if ? x ??? → ? with 83 [ SEQ ⇒ step_labels … 84 | FIN ⇒ fin_step_labels … 85 ] (\snd b). 86 87 definition eval_block_cont : 88 ∀globals.∀p : sem_params.∀ty.genv globals p → 89 state p → ∀b : block_cont p globals ty. 90 IO io_out io_in ( 91 (stmt_type_if ? ty step_flow fin_step_flow p globals (block_cont_labels … b)) × 92 (state p)) ≝ λglobals,p,ty,ge,st. 93 match ty return λx.∀b : block_cont p globals x. 94 IO io_out io_in ( 95 (stmt_type_if ? x step_flow fin_step_flow p globals (block_cont_labels … b)) × 96 (state p)) 97 with 98 [ SEQ ⇒ λb. 99 ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ; 100 match flow return λ_.IO ?? (step_flow … ((block_cont_labels … b))×?) with 101 [ Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉 102 | Proceed ⇒ eval_step … ge st' (\snd b) 103 | Init _ _ _ _ ⇒ 104 Error … (msg ExecutingInternalCallInBlock) 105 ] 106 | FIN ⇒ λb. 107 ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ; 108 match flow return λ_.IO ?? ((fin_step_flow … (block_cont_labels … b))×?) with 109 [ Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉 110 | Proceed ⇒ eval_fin_step … ge st' (\snd b) 111 | Init _ _ _ _ ⇒ 112 Error … (msg ExecutingInternalCallInBlock) 113 ] 114 ]. try cases l /2 by Exists_append_r, Exists_append_l/ qed. 115 116 (* 117 lemma m_pred 118 119 lemma attach_m_pred_bind : ∀M.∀MP : MonadPred P.∀P,X,Y.m : monad M X. 120 ∀f : X → monad M Y.m_pred MP P … m → 121 ! x ← m ; f x = ! x ← 122 *) 123 124 definition no_init : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝ 125 λp,globals,lbls,A,flp. 126 match \fst flp with 127 [ Init _ _ _ _ ⇒ False 128 | _ ⇒ True 129 ]. 130 131 definition truly_sequential : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝ 132 λp,globals,lbls,A,flp. 133 match \fst flp with 134 [ Proceed ⇒ True 135 | _ ⇒ False 136 ]. 137 138 definition never_calls : ∀p : sem_params.∀globals.genv globals p → joint_step p globals → Prop ≝ 139 λp,globals,ge,s.match s with 140 [ CALL_ID f args dest ⇒ 141 Try 142 ! b ← find_symbol … ge f ; 143 ! fd ← find_funct_ptr … ge b ; 144 match fd with 145 [ Internal _ ⇒ return False 146 | External _ ⇒ return True 147 ] 148 catch ⇒ 149 True 150 | extension c ⇒ 151 ∀st : state p. 152 pred_io … (λ_.True) (no_init …) (exec_extended … ge c st) 153 | _ ⇒ True 154 ]. 155 156 definition unbranching ≝ λp,globals,ge,s.never_calls p globals ge s ∧ step_labels … s = [ ]. 157 158 lemma err_to_io_bind : ∀O,I,X,Y.∀m : res X.∀f : X → res Y. 159 err_to_io O I ? (! x ← m ; f x) = ! x ← m : IO O I X ; f x. 160 #O #I #X #Y * // 161 qed. 162 163 lemma pred_io_True : ∀O,I,X,m.pred_io O I X (λ_.True) (λ_.True) m. 164 #O #I #X #m elim m // qed. 165 166 (* 167 lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m. 168 #X #m elim m // qed. 169 *) 170 171 (* 172 lemma never_calls_no_init : ∀p,globals,ge,s. 173 never_calls p globals ge s → 174 ∀st : state p. 175 pred_io … (λ_.True) (no_init …) (eval_step … ge st s). 176 #p#g#ge * // 177 [10,12: 178 |*: 179 #a #b #c try #d try #e try #f try #g 180 @res_io_pred 181 @(mp_bind … (λ_.True) … (pred_res_True …)) 182 #st * try (@mp_return @I) 183 @(mp_bind … (λ_.True) … (pred_res_True …)) 184 #st * [9: elim st] normalize nodelta try (@mp_return @I) 185 @(mp_bind … (λ_.True) … (pred_res_True …)) 186 #st * try (@mp_return @I) 187 @(mp_bind … (λ_.True) … (pred_res_True …)) 188 #st * [elim (opaccs ????) #by1 #by2 normalize nodelta] 189 @(mp_bind … (λ_.True) … (pred_res_True …)) 190 #st * [2: elim (op2 ?????) #by #bit normalize nodelta] 191 try (@mp_return @I) 192 @(mp_bind … (λ_.True) … (pred_res_True …)) 193 #st * @mp_return @I 194 ] 195 [ #id #args #dest #H whd in H; 196 #st change with (! x ← ? ; ?) in match (eval_step ?????); 197 elim (find_symbol ???) in H ⊢ %; [//] 198 #b >m_return_bind >m_return_bind 199 change with (! x ← ? ; ?) in match (eval_call_block ?????????); 200 elim (find_funct_ptr ???) [//] 201 #fd >m_return_bind >m_return_bind 202 elim fd #fn normalize nodelta * 203 @(mp_bind … (λ_.True)) [//] 204 #st * @(mp_bind … (λ_.True) … (pred_io_True …)) 205 #st * @(mp_bind … (λ_.True) … (pred_io_True …)) 206 #st * @(mp_bind … (λ_.True) … (pred_io_True …)) 207 #st * @mp_return % 208 | #s #H @H 209 ] 210 qed. 211 212 lemma unbranching_truly_sequential : ∀p,globals,ge,s. 213 unbranching p globals ge s → 214 ∀st : state p. 215 pred_io … (λ_.True) (truly_sequential …) (eval_step … ge st s). 216 #p#globals#ge#s * #H #G #st 217 lapply (never_calls_no_init … H st) @m_pred_mp 218 >G * * 219 [ * #lbl * | #id #fd #args #dest ] #st * % 220 qed. 221 *) 222 223 lemma seq_list_labels_append : ∀p,globals,b1,b2. 224 seq_list_labels p globals (b1 @ b2) = 225 seq_list_labels … b1 @ seq_list_labels … b2. 226 #p #g #b1 elim b1 227 [ // 228 | #hd #tl #IH #b2 whd in ⊢ (??%%); 229 >associative_append <IH % 230 ] 231 qed. 232 233 (* 234 lemma eval_seq_list_append : ∀globals,p,ge,st,b1,b2. 235 eval_seq_list globals p ge st (b1@b2) = 236 ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ; 237 match flow with 238 [ Proceed ⇒ 239 ! 〈flow',st''〉 ← eval_seq_list … ge st' b2 ; 240 return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉 241 | _ ⇒ return 〈(flow : step_flow … (seq_list_labels … (b1@b2))), st'〉 242 ]. 243 [2,3,4: 244 #lbl #H >seq_list_labels_append 245 [1,2: @Exists_append_l | @Exists_append_r ] @H ] 246 #globals#p#ge#st#b1 lapply st -st elim b1 247 [ #st #b2 >m_return_bind normalize nodelta 248 <(m_bind_return … (eval_seq_list … b2)) in ⊢ (??%?); 249 @m_bind_ext_eq ** 250 [ * #lbl #H | #id #fd #args #dest ] #st' % 251 | #hd #tl #IH #st #b2 252 whd in match (? @ b2); 253 whd in match (eval_seq_list ?????); 254 whd in match (eval_seq_list ???? (hd :: tl)); 255 >m_bind_bind 256 @m_bind_ext_eq 257 ** [ #lbl | #id #fd #args #dest] #st' normalize nodelta 258 [1,2: @m_return_bind] 259 >m_bind_bind 260 >IH >m_bind_bind 261 @m_bind_ext_eq ** 262 [#lbl | #id #fd #args #dest ] #st' normalize nodelta 263 >m_return_bind 264 [1,2: @m_return_bind ] 265 >m_bind_bind normalize nodelta 266 @m_bind_ext_eq ** 267 [#lbl|#id #fd #args #dest] #st'' >m_return_bind % 268 ] 269 qed. 270 271 lemma eval_seq_list_unbranching : 272 ∀globals,p,ge,st,b. 273 All ? (unbranching … ge) b → 274 pred_io … (λ_.True) (truly_sequential …) 275 (eval_seq_list globals p ge st b). 276 #globals#p#ge#st #b lapply st -st elim b 277 [ #st * % 278 | #hd #tl #IH #st * #hd_ok #tl_ok 279 @mp_bind 280 [2: @(unbranching_truly_sequential … hd_ok st) |] 281 ** [#lbl|#id#fd#args#dest] #st' * 282 normalize nodelta 283 @mp_bind [2: @(IH st' tl_ok)|] 284 ** [#lbl|#id#fd#args#dest] #st'' * % 285 ] 286 qed. 287 288 lemma io_pred_as_rel : ∀O,I,A,Perr,P,v. 289 pred_io O I A Perr P v → 290 rel_io O I (eq …) … (λx,y.x = y ∧ P x) v v. 291 #O #I #A #Perr #P #v elim v 292 [ #o #f #IH whd in ⊢ (%→%); 293 #H %{(refl …)} #i @IH @H 294 |*: /2/ 295 ] 296 qed. 297 298 lemma eval_seq_list_append_unbranching : ∀globals,p,ge,st,b1,b2. 299 All ? (unbranching … ge) b1 → 300 eval_seq_list globals p ge st (b1@b2) = 301 ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ; 302 ! 〈flow', st''〉 ← eval_seq_list … ge st' b2 ; 303 return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉. 304 [2: #lbl #H >seq_list_labels_append @Exists_append_r @H ] 305 #globals #p #ge #st #b1 #b2 #H 306 >eval_seq_list_append 307 @mr_bind 308 [2: @(io_pred_as_rel … (eval_seq_list_unbranching … H)) |] 309 ** [#lbl|#id#fd#args#dest] #st 310 #y * #EQ <EQ -y * @rel_io_eq normalize nodelta % 311 qed. 312 *) 313 lemma block_cont_labels_append : ∀p,globals,ty,b1,b2. 314 block_cont_labels p globals ty (b1 @ b2) = 315 block_cont_labels … b1 @ block_cont_labels … b2. 316 #p #g #ty * #l1 #s1 * #l2 #s2 317 whd in match (〈?,?〉@?); whd in ⊢ (??%?); 318 >seq_list_labels_append 319 >associative_append 320 >associative_append 321 >associative_append % 322 qed. 323 (* 324 lemma eval_block_cont_append : ∀globals.∀p : sem_params.∀ty,ge,st. 325 ∀b1 : block_cont p globals SEQ.∀b2 : block_cont p globals ty. 326 eval_block_cont ??? ge st (b1@b2) = 327 ! 〈flow, st'〉 ← eval_block_cont ??? ge st b1 ; 328 match ty return λx. 329 block_cont p globals x → IO ?? ((stmt_type_if ? x step_flow fin_step_flow ???) × ?) with 330 [ SEQ ⇒ λb2. 331 match flow with 332 [ Proceed ⇒ 333 ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ; 334 return 〈?, st''〉 335 | Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉 336 | _ ⇒ Error … (msg ExecutingInternalCallInBlock) 337 ] 338 | FIN ⇒ λb2. 339 match flow with 340 [ Proceed ⇒ 341 ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ; 342 return 〈?, st''〉 343 | Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉 344 | _ ⇒ Error … (msg ExecutingInternalCallInBlock) 345 ] 346 ] b2. 347 [3,5: whd in flow'; @flow' 348 #lbl >block_cont_labels_append @Exists_append_r 349 |2,4: cases l -l #l >block_cont_labels_append @Exists_append_l 350 ] 351 #globals#p * whd in match stmt_type_if; normalize nodelta 352 #ge#st * #l1 #s1 * #l2 #s2 353 whd in match (〈?,?〉@?); 354 whd in match eval_block_cont; normalize nodelta 355 >m_bind_bind 356 >eval_seq_list_append 357 >m_bind_bind 358 @m_bind_ext_eq 359 360 whd in ⊢ (??%?); 361 match ty return λx.IO ?? ((stmt_type_if ? x ?????) × ?) with 362 [ SEQ ⇒ 363 | FIN ⇒ return 〈FRedirect ??? «l,?», st'〉 364 ] 365 | _ ⇒ Error … (msg ExecutingInternalCallInBlock) 366 ]. 367 #globals#p#ty#ge#st*#l1#s1*#l2#s2 368 whd in match (〈?,?〉@?); 369 whd in match eval_block_cont; normalize nodelta 370 >m_bind_bind 371 >eval_seq_list_append 372 >m_bind_bind 373 @m_bind_ext_eq 374 ** [#l|#id#fd#args#dest] normalize nodelta #st' 375 [1,2:>m_return_bind normalize nodelta 376 [ >m_return_bind ] % ] 377 change with (! x ← ? ; ?) in match (eval_seq_list ???? (?::?)); 378 >m_bind_bind whd in match stmt_type_if; 379 normalize nodelta 380 >m_bind_bind 381 @m_bind_ext_eq 382 **[#l|#id#fd#args#dest] normalize nodelta #st'' 383 [1,2: >m_return_bind normalize nodelta % | % ] 384 qed. 385 *) 386 387 388 (* just like repeat, but without the full_exec infrastructure, and it 389 stops upon a non-proceed flow cmd *) 390 let rec repeat_eval_state_flag n globals (p:sem_params) (ge : genv globals p) 391 (st : state_pc p) on n : 392 IO io_out io_in (bool × (state_pc p)) ≝ 393 match n with 394 [ O ⇒ return 〈false,st〉 395 | S k ⇒ 396 ! 〈flag,st'〉 ← eval_state_flag globals p ge st ; 397 if flag then return 〈true,st'〉 else repeat_eval_state_flag k globals p ge st' 398 ]. 399 400 definition block_size : ∀p,g,ty.block_cont p g ty → ℕ ≝ 401 λp,g,ty,b.S (|\fst b|). 402 403 interpretation "block cont size" 'norm b = (block_size ??? b). 404 405 lemma repeat_eval_state_flag_plus : ∀n1,n2,globals, p, ge, st. 406 repeat_eval_state_flag (n1 + n2) globals p ge st = 407 ! 〈flag,st〉 ← repeat_eval_state_flag n1 globals p ge st ; 408 if flag then return 〈true, st〉 else repeat_eval_state_flag n2 globals p ge st. 409 #n1 elim n1 -n1 [| #n1 #IH] 410 #n2 #globals #p #ge #st 411 [ @m_return_bind 412 | change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????); 413 change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S n1) ????); 414 >m_bind_bind in ⊢ (???%); 415 @m_bind_ext_eq ** #st' normalize nodelta 416 [ % | @IH ] 417 ] 418 qed. 419 420 lemma repeat_eval_state_flag_one : ∀globals, p, ge, st. 421 repeat_eval_state_flag 1 globals p ge st = eval_state_flag globals p ge st. 422 #globals #p #ge #st 423 change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????); 424 <(m_bind_return … (eval_state_flag ????)) in ⊢ (???%); 425 @m_bind_ext_eq ** #st % 426 qed. 427 428 lemma eval_tunnel_step : 429 ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst. 430 fetch_function … ge (pc … st) = OK … fn → 431 point_of_pointer ? p … (pc … st) = OK … src → 432 src ~~> dst in joint_if_code … fn → 433 eval_state_flag g p ge st = 434 return 〈true,set_pc … (pointer_of_point ? p (pc … st) dst) st〉. 435 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #lbl * #EQ1 #EQ2 436 change with (! s ← ? ; ?) in match (eval_state_flag ????); 437 change with (! fn ← ? ; ?) in match (fetch_statement ?????); 438 >pc_pt in ⊢ (??%?); >m_return_bind 439 >fetch_fn in ⊢ (??%?); >m_return_bind 440 >EQ1 in ⊢ (??%?); >m_return_bind 441 >EQ2 in ⊢ (??%?); 442 change with (! st ← ? ; ?) in match (eval_statement ?????); 443 whd in match eval_fin_step; normalize nodelta 444 >m_return_bind 445 whd in match eval_fin_step_flow; normalize nodelta 446 change with (! ptr ← ? ; ?) in match (goto ??????); 447 whd in match pointer_of_label_in_block; normalize nodelta 448 whd in match fetch_function in fetch_fn; 449 normalize nodelta in fetch_fn; 450 >fetch_fn in ⊢ (??%?); >m_return_bind 451 >EQ2 in ⊢ (??%?); >m_return_bind 452 cases st #st' ** #ty ** #id #H #o #EQ destruct(EQ) 453 elim (pointer_compat_from_ind … H) % 454 qed. 455 456 lemma fetch_function_from_block_eq : 457 ∀p,g,ge. 458 ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 → 459 fetch_function p g ge ptr1 = fetch_function p g ge ptr2. 460 #p #g #ge #ptr1 #ptr2 #EQ 461 whd in match fetch_function; normalize nodelta >EQ 462 @m_bind_ext_eq // qed. 463 464 (* 465 lemma eval_tunnel : 466 ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst. 467 fetch_function … ge (pc … st) = OK … fn → 468 point_of_pointer ? p … (pc … st) = OK … src → 469 src ~~>^* dst in joint_if_code … fn → 470 ∃n.repeat_eval_state n g p ge st = 471 return 〈f,set_pc … (pointer_of_point ? p (pc … st) dst) st〉. 472 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #through 473 lapply pc_pt -pc_pt lapply fetch_fn -fetch_fn lapply src -src lapply st -st 474 elim through [2: #hd #tl #IH] 475 #st #src #fetch_fn #pc_pt 476 [2: #EQ <EQ %{0} 477 >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st // ] 478 * #H1 #H2 479 letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) hd) st) 480 elim (IH st' … H2) 481 [3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st'; 482 @pointer_of_point_block 483 |2: 484 whd in match st'; >point_of_pointer_of_point % 485 ] 486 #n' #EQ %{(S n')} 487 change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????); 488 >(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind 489 >EQ % 490 qed. 491 492 lemma eval_tunnel_plus : 493 ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst. 494 fetch_function … ge (pc … st) = OK … fn → 495 point_of_pointer ? p … (pc … st) = OK … src → 496 src ~~>^+ dst in joint_if_code … fn → 497 ∃n.repeat_eval_state (S n) g p ge st = 498 return set_pc … (pointer_of_point ? p (pc … st) dst) st. 499 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #mid * #H1 #H2 500 letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st) 501 elim (eval_tunnel … ge st' … H2) 502 [3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st'; 503 @pointer_of_point_block 504 |2: 505 whd in match st'; >point_of_pointer_of_point % 506 ] 507 #n #EQ %{n} 508 change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????); 509 >(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind 510 >EQ % 511 qed. 512 *) 8 ].*) 513 9 514 10 lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer. … … 522 18 >EQ1 >m_return_bind >EQ3 % 523 19 qed. 524 (* 525 lemma eval_seq_list_in_code : 526 ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst. 527 fetch_function … ge (pc … st) = OK … fn → 528 point_of_pointer ? p … (pc … st) = OK … src → 529 All ? (never_calls … ge) B → 530 seq_list_in_code … (joint_if_code … fn) src B dst → 531 repeat_eval_state_flag (|B|) g p ge st = 532 ! 〈flow,st'〉 ← eval_seq_list g p ge st B ; 533 match flow with 534 [ Redirect l ⇒ 535 ! st'' ← goto ?? ge l st' (pblock … (pc ? st)) ; 536 return 〈true, st''〉 537 | Init id fn args dest ⇒ Error … (msg ExecutingInternalCallInBlock) 538 (* dummy, never happens *) 539 | Proceed ⇒ 540 let nxt_ptr ≝ pointer_of_point p p … (pc … st) dst in 541 return 〈false, mk_state_pc ? st' nxt_ptr〉 542 ]. 543 #p #g #ge #st #fn #src #B lapply src -src 544 lapply st -st elim B [|#hd #tl #IH] 545 #st #src #dst #fetch_fn #pc_pt * [2: #hd_ok #tl_ok] 546 [2: #EQ normalize in EQ; <EQ 547 whd in match (eval_seq_list ???? [ ]); 548 >m_return_bind normalize nodelta 549 >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st // 550 |1: * #n * #EQat #H 551 change with (! st' ← ? ; ?) in match (eval_seq_list ?????); 552 change with (! st' ← ? ; ?) in match (repeat_eval_state_flag ?????); 553 >m_bind_bind 554 >(fetch_statement_eq … fetch_fn pc_pt EQat) >m_return_bind 555 >m_bind_bind >m_bind_bind 556 lapply (never_calls_no_init … hd_ok st) #hd_ok' 557 @(mr_bind … 558 (λfst1,fst2.fst1 = fst2 ∧ no_init … fst1)) 559 [ lapply hd_ok' elim (eval_step ?????) 560 [ #o #f #IH' 561 whd in ⊢ (%→%); #G 562 %{(refl …)} #i @IH' @G 563 |*: #v whd in ⊢ (%→%); #H 564 % [ % ] @H 20 21 include alias "basics/logic.ma". 22 lemma io_evaluate_bind : ∀O,I,X,Y,env. 23 ∀m : IO O I X.∀f : X → IO O I Y. 24 io_evaluate O I Y env (! x ← m ; f x) = 25 ! x ← io_evaluate O I X env m ; 26 io_evaluate O I Y env (f x). 27 #O #I #X #Y #env #m elim m 28 [ #o #g #IH #f whd in match (! x ← Interact ????? ; ?); 29 change with (! y ← ? ; ?) in ⊢ (??%(????%?)); 30 >m_bind_bind @m_bind_ext_eq #i @IH 31 | #x #f % 32 | #e #f % 33 ] 34 qed. 35 36 lemma fetch_function_from_block_eq : 37 ∀p,g,ge. 38 ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 → 39 fetch_function p g ge ptr1 = fetch_function p g ge ptr2. 40 #p #g #ge #ptr1 #ptr2 #EQ 41 whd in match fetch_function; normalize nodelta >EQ 42 @m_bind_ext_eq // qed. 43 44 let rec repeat_eval_seq_no_pc 45 (p : evaluation_params) env 46 (l : list (joint_seq p (globals p))) on l : 47 state p → res (state p) ≝ 48 λst.match l with 49 [ nil ⇒ return st 50 | cons hd tl ⇒ 51 ! st' ← io_evaluate … (env st) (eval_seq_no_pc (globals p) p (ev_genv p) st hd) ; 52 repeat_eval_seq_no_pc p env tl st' 53 ]. 54 55 lemma err_to_io_evaluate : ∀O,I,X,env,m. 56 io_evaluate O I X env (err_to_io … m) = m. 57 #O#I#X#env * // qed. 58 59 definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ]. 60 61 definition no_call_nor_label : ∀p,g.joint_seq p g → bool ≝ 62 λp,g,s.match s with 63 [ COST_LABEL _ ⇒ false 64 | CALL_ID _ _ _ ⇒ false 65 | extension_call _ ⇒ false 66 | _ ⇒ true 67 ]. 68 69 lemma no_call_nor_label_proceed : ∀p : evaluation_params. 70 ∀st : state p. ∀s. 71 no_call_nor_label p (globals p) s → 72 eval_seq_pc (globals p) p (ev_genv p) st s = return Proceed ???. 73 #p #st * // [ #f #args #dest | #c ] * 74 qed. 75 76 lemma no_call_nor_label_other : ∀p : evaluation_params.∀s. 77 no_call_nor_label p (globals p) s → 78 step_classifier … s = cl_other. 79 #p * // [ #f #args #dest | #c ] * 80 qed. 81 82 lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt. 83 no_call_nor_label p (globals p) s → 84 cost_label_of_stmt … (sequential … s nxt) = None ?. 85 #p * // #lbl#next * 86 qed. 87 88 let rec produce_trace_any_any 89 (p : evaluation_params) 90 (st : state_pc p) fd 91 (src : code_point p) 92 (b : list (joint_seq p (globals p))) on b : 93 ∀l : list (code_point p). 94 ∀dst : code_point p. 95 ∀st' : state p. 96 fetch_function p ? (ev_genv p) (pc … st) = return fd → 97 point_of_pointer p p (pc … st) = return src → 98 if list_not_empty ? b then 99 ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ? 100 else 101 True → 102 src ~❨b, l❩~> dst in joint_if_code … fd → 103 All ? (λx.bool_to_Prop (no_call_nor_label … x)) b → 104 repeat_eval_seq_no_pc p (io_env p) b st = return st' → 105 trace_any_any (joint_abstract_status p) st 106 (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ≝ 107 match b 108 return λx.?→?→?→?→?→?→?→?→?→? 109 with 110 [ nil ⇒ 111 λl,dst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1. 112 (taa_base (joint_abstract_status p) st) 113 ⌈trace_any_any (joint_abstract_status p) st st ↦ 114 trace_any_any (joint_abstract_status p) st 115 (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst))⌉ 116 | cons hd tl ⇒ 117 λl. 118 match l return λx.?→?→?→?→?→?→?→?→? with 119 [ nil ⇒ λdst,st',fd_prf,src_prf,dst_prf,in_code.⊥ 120 | cons mid rest ⇒ 121 λdst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1. 122 match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd) 123 return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd) = x → ? 124 with 125 [ OK st_mid ⇒ λEQ2. 126 taa_step (joint_abstract_status p) st ? 127 (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ??? 128 (produce_trace_any_any ? 129 (mk_state_pc ? st_mid (pointer_of_point ? p (pc ? st) mid)) 130 fd mid tl rest dst ???????) 131 | Error _ ⇒ λEQ2.⊥ 132 ] (refl …) 565 133 ] 566 | ** [#lbl | #id #fd #args #dest ] #st' 567 #y * #EQ <EQ -y * normalize nodelta @rel_io_eq 568 whd in match succ_pc; normalize nodelta 569 >pc_pt >m_return_bind 570 letin src' ≝ (point_of_succ p src n) in H ⊢ %; 571 letin pc' ≝ (pointer_of_point p p … (pc ? st) src') #H 572 [>m_return_bind whd in match eval_step_flow; normalize nodelta 573 whd in match (pblock ?); 574 elim (goto … ge lbl st' ?) 575 [ #st'' >m_return_bind % 576 | #e % 577 ] 578 | normalize nodelta in IH ⊢ %; @(IH … tl_ok H) 579 [ @fetch_fn 580 | @point_of_pointer_of_point 134 ]. 135 [ cases l in in_code; [2: #mid #rest *] normalize in ⊢ (%→?); #EQ 136 cases st in src_prf EQ1; -st #st #pc 137 #src_prf normalize in ⊢ (%→?); #EQ1 destruct 138 >(pointer_of_point_of_pointer … src_prf) % 139 | elim in_code 140 |12: lapply EQ1 whd in ⊢ (??%?→?); 141 >EQ2 normalize #ABS destruct(ABS) 142 |*: 143 elim in_code 144 * #nxt * #EQ3 #EQ4 #Hrest 145 elim all_other 146 #hd_other #tl_other 147 [ whd whd in match eval_state; normalize nodelta 148 >(fetch_statement_eq … fd_prf src_prf EQ3) >m_return_bind 149 whd in match eval_statement; normalize nodelta 150 whd in match eval_step; normalize nodelta 151 >m_bind_bind 152 >(no_call_nor_label_proceed … hd_other) >m_return_bind 153 >m_bind_bind 154 >io_evaluate_bind >EQ2 >m_return_bind 155 >m_return_bind 156 whd in match succ_pc; normalize nodelta 157 >m_bind_bind >src_prf >m_return_bind >m_return_bind 158 whd in match eval_step_flow; normalize nodelta 159 whd in ⊢ (??%%); >EQ4 160 >EQ2 % 161 | %{(sequential … hd nxt)} %{(fetch_statement_eq … fd_prf src_prf EQ3)} 162 cases all_other #hd_other #_ 163 whd in match stmt_classifier; normalize nodelta 164 @no_call_nor_label_other assumption 165 | %* #H @H -H whd in ⊢ (??%?); 166 cases tl in Hrest tl_other; 167 [ cases rest [2: #hd' #tl' *] normalize in ⊢ (%→?); #EQ' destruct(EQ') * 168 lapply dst_prf 169 whd in match (as_pc_of ??); 170 whd in match fetch_statement; normalize nodelta 171 whd in match point_of_pointer; normalize nodelta 172 >point_of_offset_of_point 173 >m_return_bind 174 >fetch_function_from_block_eq 175 [ >fd_prf 176 >m_return_bind 177 cases (stmt_at ????) 178 [ #_ % 179 | #stmt #H @H 180 ] 181 | % 182 | 183 ] 184 | #hd' #tl' cases rest [*] #mid' #rest' * * #next' * #EQ5 #EQ6 185 #_ * #hd_other' #_ 186 >fetch_statement_eq try assumption 187 [ @no_call_nor_label_uncosted assumption 188 | whd in match (as_pc_of ??); 189 whd in ⊢ (??%?); 190 >point_of_offset_of_point % 191 ] 581 192 ] 193 | change with (! x ← ?;?) in EQ1 : (??%?); 194 >EQ2 in EQ1; #H @H 195 | assumption 196 | assumption 197 | cases (list_not_empty ??) [ assumption | % ] 198 | @point_of_pointer_of_point 199 | <fd_prf @fetch_function_from_block_eq % 582 200 ] 583 201 ] 584 ] 585 qed. 586 587 definition eval_block_cont_pc : 588 ∀globals.∀p : sem_params.∀ty.genv globals p → 589 state_pc p → block_cont p globals ty → stmt_type_if ? ty (code_point p) unit → 590 IO io_out io_in (bool × (state_pc p)) ≝ 591 λglobals,p,ty,ge,st,b,nxt. 592 ! 〈flow, st'〉 ← eval_block_cont globals p ty ge st b ; 593 match ty return λx.stmt_type_if ? x ?? → stmt_type_if ? x ?? → ? with 594 [ SEQ ⇒ λflow,nxt.eval_step_flow ?? ge st' 595 (pointer_of_point ? p (pc ? st) nxt) flow 596 | FIN ⇒ λflow.λ_. 597 ! st' ← eval_fin_step_flow ?? ge st' (pblock … (pc ? st)) flow ; 598 return 〈true, st'〉 599 ] flow nxt. 600 601 lemma eval_block_cont_in_code : 602 ∀p : sem_params.∀g,ty.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst. 603 fetch_function … ge (pc … st) = OK … fn → 604 point_of_pointer ? p … (pc … st) = OK … src → 605 All ? (never_calls … ge) (\fst B) → 606 src ~❨B❩~> dst in joint_if_code … fn → 607 repeat_eval_state_flag (|B|) g p ge st = 608 eval_block_cont_pc g p ty ge st B dst. 609 #p #g #ty #ge #st #fn #src * #l #s #dst #fetch_fn #pc_pt #l_ok 610 * #mid * #l_in_code #s_in_code 611 change with (1 + |l|) in match (|?|); 612 >commutative_plus 613 >repeat_eval_state_flag_plus 614 change with (! x ← ? ; ?) in ⊢ (???%); 615 >m_bind_bind 616 >(eval_seq_list_in_code … fetch_fn pc_pt l_ok l_in_code) 617 >m_bind_bind 618 @m_bind_ext_eq ** [#lbl | #id #fd #args #dest] #st' 619 normalize nodelta 620 [ -s_in_code lapply dst -dst cases ty 621 whd in match stmt_type_if; normalize nodelta 622 #dst >m_return_bind 623 [whd in match eval_step_flow; | whd in match eval_fin_step_flow; ] 624 normalize nodelta 625 whd in match (pblock ?); 626 elim (goto g p ge lbl st' ?) #x // 627 | % 628 | >m_return_bind normalize nodelta 629 >repeat_eval_state_flag_one 630 >m_bind_bind 631 lapply s_in_code -s_in_code lapply dst -dst lapply s -s cases ty 632 whd in match stmt_type_if; normalize nodelta 633 #s #dst [* #n * ] #s_in_code [ #n_is_dst ] 634 whd in match eval_state_flag; normalize nodelta 635 letin pc' ≝ (pointer_of_point p p (pc ? st) mid) 636 letin st_pc' ≝ (mk_state_pc ? st' pc') 637 >(fetch_statement_eq … ?? s_in_code) 638 [2,5: @point_of_pointer_of_point 639 |3,6: @fetch_fn 640 |*: >m_return_bind 641 whd in match eval_statement; normalize nodelta 642 @m_bind_ext_eq * #flow #st'' >m_return_bind [2:%] 643 whd in match succ_pc; normalize nodelta 644 >point_of_pointer_of_point >m_return_bind 645 >pointer_of_point_of_pointer [2: @refl |*:] 646 [ >point_of_pointer_of_point >n_is_dst % 647 | % 648 ] 649 ] 650 ] 651 qed. 652 cases dst [*] #z @eval_tunnel assumption 653 | cases dst [2: #z *]] 654 * #mid * #tunn [#H | * #n * #H #G ] 655 elim (eval_tunnel … fetch_fn pc_pt tunn) 656 #n 657 letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st) 658 #EQ1 659 cut (point_of_pointer ? p … (pc … st') = OK … mid) 660 [1,3: 661 whd in match st'; >point_of_pointer_of_point % ] #pc_pt' 662 cut (fetch_function p … ge (pc … st') = OK … fn) 663 [1,3: >fetch_function_from_block_eq [1,4:@fetch_fn |*:] whd in match st'; 664 @pointer_of_point_block] #fetch_fn' 665 [ %{(n + 1)} 666 >repeat_eval_state_plus >EQ1 >m_return_bind 667 >repeat_eval_state_one change with (None ?) in match (! x ← None ? ; ?); 668 change with (! 〈flow,tr,st〉 ← ? ; ?) in match (eval_block_cont ??????); 669 change with (! s ← ? ; ?) in match (eval_state ????); 670 >(fetch_statement_eq … fetch_fn' pc_pt' H) >m_return_bind 671 >m_bind_bind 672 change with ( ! x ← ? ; ?) in match (eval_block_cont ???????); 673 cases s * 674 675 @m_bind_ext_eq' ** #flow #tr1 #st1 normalize nodelta 676 >m_bind_bind change with st' in match (set_pc ???); @m_bind_ext_eq 677 change with (! fn ← ? ; ?) in match (fetch_statement ?????); 678 >m_bind_bind in ⊢ (??%?); 679 change with (pointer_of_point ????) in match (pc ??); 680 >point_of_pointer_of_point >m_return_bind 681 >(fetch_function_from_block_eq ???? (pc … st)) 682 [2: @pointer_of_point_block ] 683 >fetch_fn >m_return_bind >H2 >m_return_bind 684 >m_bind_bind 685 change with (! x ← ? ; ?) in ⊢ (???%); 686 >fetch_fn n ⊢ (??(????%?)?); >m_return_bind 687 >(stmt_at_to_safe … src_prf) in ⊢ (??(????%?)?); 688 >H1 in ⊢ (??(????%?)?); 689 whd in ⊢ (??(λ_.???%)); 690 elim b 691 [ #st #dst #fetch_fn #prf #through 692 #H elim (block_cont_to_tunnel … H) #dst' 693 * #EQdst >EQdst >m_return_bind #G 694 elim (eval_tunnel … fetch_fn prf … G) #x #EQ %{x} 695 >EQ % 696 | 697 698 #dst #fetch_fn #prf #through 699 lapply prf -prf lapply fetch_fn -fetch_fn 700 lapply b -b lapply st -st 701 elim through [2: #hd #tl #IH] 702 [2: 703 704 #st * [1,4,7,10:|2,5,8,11:#s|3,6,9,12:#s#b'] #fetch_fn #prf 705 normalize in ⊢(%→?); 706 [8: #EQ1 |*: * [5: |*: *] #lbl [ |*: *] * #H1 #H2 [|*: #H3] #x [ * 707 [ * || * | * #lbl 708 * #lbl * [*] #H1 #H2 [#H3] 709 710 let rec block_cont_in_code (p : sem_params) g (b : block_cont p g) 711 (following : option (succ p)) (c : codeT p g) (at : cpointer) on b : Prop ≝ 712 match b with 713 [ Skip ⇒ 714 match following with 715 [ Some l ⇒ succ_pc p p 716 *) 202 qed. -
src/joint/semantics_paolo.ma
r1999 r2186 16 16 definition xpointer ≝ Σp.ptype p = XData. 17 17 unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code). 18 unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData).18 unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData). 19 19 20 20 record sem_state_params : Type[1] ≝ … … 86 86 λpars,globals,ge,p.function_of_block pars globals ge (pblock p). 87 87 88 inductive step_flow (p : params) (globals : list ident) (labels : list label) : Type[0] ≝ 89 | Redirect : (Σl.In ? labels l) → step_flow p globals labels (* used for goto-like flow alteration *) 90 | Init : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals labels (* call a function with given id, then proceed *) 91 | Proceed : step_flow p globals labels. (* go to implicit successor *) 92 88 inductive step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝ 89 | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p globals (Labels lbls) (* used for goto-like flow alteration *) 90 | Init : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals Call (* call a function with given id, then proceed *) 91 | Proceed : ∀flows.step_flow p globals flows. (* go to implicit successor *) 92 93 (* 93 94 definition step_flow_cons : ∀p,globals,l,lbls. 94 95 step_flow p globals lbls → step_flow p globals (l :: lbls) ≝ … … 120 121 coercion step_flow_r : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1@l2) ≝ 121 122 step_flow_append_r on _flow : step_flow ??? to step_flow ?? (append ???). 122 123 inductive fin_step_flow (p : params) (globals : list ident) (labels : list label): Type[0] ≝ 124 | FRedirect : (Σl.In ? labels l) → fin_step_flow p globals labels 125 | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals labels 126 | FEnd : fin_step_flow p globals labels. (* end flow *) 127 123 *) 124 125 inductive fin_step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝ 126 | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p globals (Labels lbls) 127 | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals Call 128 | FEnd1 : fin_step_flow p globals (Labels [ ]) (* end flow *) 129 | FEnd2 : fin_step_flow p globals Call. (* end flow *) 130 131 (* 128 132 definition fin_step_flow_cons : ∀p,globals,l,lbls. 129 133 fin_step_flow p globals lbls → fin_step_flow p globals (l :: lbls) ≝ … … 155 159 coercion fin_step_flow_r : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1@l2) ≝ 156 160 fin_step_flow_append_r on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???). 161 *) 157 162 158 163 record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝ … … 230 235 serialization and on whether the call is a tail one. *) 231 236 definition eval_call_block: 232 ∀globals.∀p : params.∀p':more_sem_unserialized_params p. ∀lbls.237 ∀globals.∀p : params.∀p':more_sem_unserialized_params p. 233 238 genv globals p → state p' → block → call_args p → call_dest p → 234 IO io_out io_in ((step_flow p globals lbls)×(state p')) ≝235 λglobals,p,p', lbls,ge,st,b,args,dest.239 IO io_out io_in ((step_flow p globals Call)×(state p')) ≝ 240 λglobals,p,p',ge,st,b,args,dest. 236 241 ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge b) : IO ? io_in ?); 237 242 match fd with … … 258 263 let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in 259 264 return set_m … m (set_isp … isp'' st). 260 normalize elim (isp p st) //265 normalize elim (isp p st) #p #H @H 261 266 qed. 262 267 … … 268 273 do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp''); 269 274 OK ? 〈ist,v〉. 270 normalize elim (isp p st) //275 normalize elim (isp p st) #p #H @H 271 276 qed. 272 277 … … 290 295 ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval) 291 296 (* change of pc must be left to *_flow execution *) 292 ; exec_extended: ∀globals.genv globals pp → ∀s : ext_step pp. 297 ; eval_ext_seq: ∀globals.genv globals pp → ext_seq pp → 298 state msu_pars → IO io_out io_in (state msu_pars) 299 ; eval_ext_tailcall : ∀globals.genv globals pp → ext_tailcall pp → 300 state msu_pars → IO io_out io_in ((fin_step_flow pp globals Call)×(state msu_pars)) 301 ; eval_ext_call: ∀globals.genv globals pp →∀s : ext_call pp. 293 302 state msu_pars → 294 IO io_out io_in ((step_flow pp globals (ext_step_labels … s))× (state msu_pars)) 295 ; exec_fin_extended: ∀globals.genv globals pp → ∀s : ext_fin_stmt pp. 296 state msu_pars → 297 IO io_out io_in ((fin_step_flow pp globals (ext_fin_stmt_labels … s))×(state msu_pars)) 303 IO io_out io_in ((step_flow pp globals Call)×(state msu_pars)) 298 304 ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars) 299 305 }. … … 311 317 cpointer→ code_point p → cpointer ≝ 312 318 λp,msp,ptr,pt. 313 mk_pointer Code (pblock ptr) ? (offset_of_point p msp pt). 314 [ elim ptr #ptr' #EQ <EQ @pok 315 | %] qed. 319 mk_pointer (pblock ptr) (offset_of_point p msp pt). 320 elim ptr #ptr' #EQ <EQ % qed. 316 321 317 322 axiom BadOffsetForCodePoint : String. … … 335 340 lemma pointer_of_point_uses_block : 336 341 ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt. 337 #p #msp ** # ty1 #bl1 #H1 #o1 #EQ1338 ** # ty2 #bl2 #H2 #o2 #EQ2342 #p #msp ** #b1 #o1 #EQ1 343 ** #b2 #o2 #EQ2 339 344 #pt #EQ3 destruct normalize // 340 345 qed. … … 344 349 pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt → 345 350 pointer_of_point p msp ptr2 pt = ptr1. 346 #p #msp ** #ty1 #bl1 #H1 #o1 #EQ1 347 ** #ty2 #bl2 #H2 #o2 #EQ2 #pt #EQ 351 #p #msp ** #b1 #o1 #EQ1 352 ** #b2 #o2 #EQ2 353 #pt #EQ3 348 354 destruct 349 355 lapply (offset_of_point_of_offset p msp o1) … … 365 371 opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt). 366 372 367 definition pointer_of_label _in_block: ∀p : params.∀ msp : more_sem_params p.∀globals.368 genv globals p → block→ label → res cpointer ≝369 λp,msp,globals,ge, b,lbl.370 ! fn ← f unction_of_block … ge b;373 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals. 374 genv globals p → cpointer → label → res cpointer ≝ 375 λp,msp,globals,ge,ptr,lbl. 376 ! fn ← fetch_function … ge ptr ; 371 377 ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl] 372 378 (point_of_label … (joint_if_code … fn) lbl) ; 373 return (mk_pointer Code (mk_block Code (block_id b)) ? (offset_of_point p msp pt) : Σp.?). // qed. 374 375 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals. 376 genv globals p → cpointer → label → res cpointer ≝ 377 λp,msp,globals,ge,ptr. 378 pointer_of_label_in_block p msp globals ge (pblock ptr). 379 return (mk_pointer(mk_block Code (block_id (pblock ptr))) 380 (offset_of_point p msp pt) : Σp.?). // qed. 379 381 380 382 definition succ_pc : ∀p : params.∀ msp : more_sem_params p. … … 396 398 397 399 definition goto: ∀globals. ∀p:sem_params. 398 genv globals p → label → state p → block→ res (state_pc p) ≝400 genv globals p → label → state p → cpointer → res (state_pc p) ≝ 399 401 λglobals,p,ge,l,st,b. 400 ! newpc ← pointer_of_label _in_block? p … ge b l ;402 ! newpc ← pointer_of_label ? p … ge b l ; 401 403 return mk_state_pc ? st newpc. 402 404 … … 416 418 axiom SuccessorNotProvided : String. 417 419 418 (* the optional point must be given only for calls *) 419 definition eval_step : 420 definition eval_seq_no_pc : 420 421 ∀globals.∀p:sem_params. genv globals p → state p → 421 ∀s:joint_s tepp globals.422 IO io_out io_in ( (step_flow p globals (step_labels … s))×(state p)) ≝422 ∀s:joint_seq p globals. 423 IO io_out io_in (state p) ≝ 423 424 λglobals,p,ge,st,seq. 424 match seq return λx.IO ?? ((step_flow ?? (step_labels … x) × ?)) with 425 [ extension c ⇒ 426 exec_extended … ge c st 427 | COST_LABEL cl ⇒ 428 return 〈Proceed ???, st〉 429 | COMMENT c ⇒ 430 return 〈Proceed ???, st〉 425 match seq return λx.IO ??? with 426 [ extension_seq c ⇒ 427 eval_ext_seq ??? ge c st 431 428 | LOAD dst addrl addrh ⇒ 432 429 ! vaddrh ← dph_arg_retrieve … st addrh ; … … 434 431 ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉; 435 432 ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr); 436 ! st ← acca_store p … dst v st ; 437 return 〈Proceed ???, st〉 433 acca_store p … dst v st 438 434 | STORE addrl addrh src ⇒ 439 435 ! vaddrh ← dph_arg_retrieve … st addrh; … … 442 438 ! v ← acca_arg_retrieve … st src; 443 439 ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v); 444 return 〈Proceed ???, set_m … m' st〉 445 | COND src ltrue ⇒ 446 ! v ← acca_retrieve … st src; 447 ! b ← bool_of_beval v; 448 if b then 449 return 〈Redirect ??? ltrue, st〉 450 else 451 return 〈Proceed ???, st〉 440 return set_m … m' st 452 441 | ADDRESS ident prf ldest hdest ⇒ 453 442 let addr ≝ opt_safe ? (find_symbol … ge ident) ? in 454 ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ?zero_offset) ;443 ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset) ; 455 444 ! st' ← dpl_store … ldest laddr st; 456 ! st'' ← dph_store … hdest haddr st'; 457 return 〈Proceed ???, st''〉 445 dph_store … hdest haddr st' 458 446 | OP1 op dacc_a sacc_a ⇒ 459 447 ! v ← acca_retrieve … st sacc_a; 460 448 ! v ← Byte_of_val v; 461 449 let v' ≝ BVByte (op1 eval op v) in 462 ! st ← acca_store … dacc_a v' st; 463 return 〈Proceed ???, st〉 450 acca_store … dacc_a v' st 464 451 | OP2 op dacc_a sacc_a src ⇒ 465 452 ! v1 ← acca_arg_retrieve … st sacc_a; … … 472 459 let carry ≝ beval_of_bool carry in 473 460 ! st' ← acca_store … dacc_a v' st; 474 let st'' ≝ set_carry … carry st' in 475 return 〈Proceed ???, st''〉 461 return set_carry … carry st' 476 462 | CLEAR_CARRY ⇒ 477 let st' ≝ set_carry … BVfalse st in 478 return 〈Proceed ???, st'〉 463 return set_carry … BVfalse st 479 464 | SET_CARRY ⇒ 480 let st' ≝ set_carry … BVtrue st in 481 return 〈Proceed ???, st'〉 465 return set_carry … BVtrue st 482 466 | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒ 483 467 ! v1 ← acca_arg_retrieve … st sacc_a_reg; … … 489 473 let v2' ≝ BVByte v2' in 490 474 ! st' ← acca_store … dacc_a_reg v1' st; 491 ! st'' ← accb_store … dacc_b_reg v2' st'; 492 return 〈Proceed ???, st''〉 475 accb_store … dacc_b_reg v2' st' 493 476 | POP dst ⇒ 494 477 ! 〈st',v〉 ← pop p st; 495 ! st'' ← acca_store p p dst v st'; 496 return 〈Proceed ???, st''〉 478 acca_store p p dst v st' 497 479 | PUSH src ⇒ 498 480 ! v ← acca_arg_retrieve … st src; 499 ! st ← push … st v; 500 return 〈Proceed ???, st〉 481 push … st v 501 482 | MOVE dst_src ⇒ 502 ! st ← pair_reg_move … st dst_src ; 503 return 〈Proceed ???, st〉 483 pair_reg_move … st dst_src 504 484 | CALL_ID id args dest ⇒ 505 485 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???; 506 eval_call_block … ge st b args dest 486 ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ; 487 return st' 488 | extension_call s ⇒ 489 !〈flow, st'〉 ← eval_ext_call ??? ge s st ; 490 return st' 491 | _ ⇒ return st 507 492 ]. 508 [ cases addr // 509 | (* TODO: to prove *) 510 elim daemon 511 | %1 % 512 ] qed. 513 514 definition eval_fin_step : ∀globals: list ident.∀p:sem_params. genv globals p → 515 state p → ∀s : joint_fin_step … p globals. 516 IO io_out io_in ((fin_step_flow p globals (fin_step_labels … s))×(state p)) ≝ 493 (* TODO: to prove *) 494 elim daemon 495 qed. 496 497 definition eval_seq_pc : 498 ∀globals.∀p:sem_params. genv globals p → state p → 499 ∀s:joint_seq p globals. 500 IO io_out io_in (step_flow p globals (step_flows … s)) ≝ 501 λg,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with 502 [ CALL_ID id args dest ⇒ 503 ! b ← opt_to_res \ldots [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???; 504 ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ; 505 return flow 506 | extension_call s ⇒ 507 !〈flow, st'〉 ← eval_ext_call ??? ge s st ; 508 return flow 509 | _ ⇒ return Proceed ??? 510 ]. 511 512 definition eval_step : 513 ∀globals.∀p:sem_params. genv globals p → state p → 514 ∀s:joint_step p globals. 515 IO io_out io_in ((step_flow p globals (step_flows … s))×(state p)) ≝ 516 λglobals,p,ge,st,s. 517 match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with 518 [ step_seq s ⇒ 519 ! flow ← eval_seq_pc ?? ge st s ; 520 ! st' ← eval_seq_no_pc ?? ge st s ; 521 return 〈flow,st'〉 522 | COND src ltrue ⇒ 523 ! v ← acca_retrieve … st src; 524 ! b ← bool_of_beval v; 525 if b then 526 return 〈Redirect ??? ltrue, st〉 527 else 528 return 〈Proceed ???, st〉 529 ]. 530 %1 % qed. 531 532 definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv globals p → 533 state p → ∀s : joint_fin_step p. 534 IO io_out io_in (state p) ≝ 517 535 λglobals,p,ge,st,s. 518 match s return λx.IO ?? ((fin_step_flow ?? (fin_step_labels … x)) × ?) with 519 [ GOTO l ⇒ return 〈FRedirect ??? l, st〉 520 | RETURN ⇒ return 〈FEnd ???, st〉 521 | extension_fin c ⇒ exec_fin_extended … ge c st 522 ]. %1 % qed. 523 536 match s return λx.IO ??? with 537 [ tailcall c ⇒ 538 !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ; 539 return st' 540 | _ ⇒ return st 541 ]. 542 543 definition eval_fin_step_pc : 544 ∀globals.∀p:sem_params. genv globals p → state p → 545 ∀s:joint_fin_step p. 546 IO io_out io_in (fin_step_flow p globals (fin_step_flows … s)) ≝ 547 λg,p,ge,st,s. 548 match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with 549 [ tailcall c ⇒ 550 !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ; 551 return flow 552 | GOTO l ⇒ return FRedirect … l 553 | RETURN ⇒ return FEnd1 ?? 554 ]. %1 % qed. 524 555 525 556 definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p → … … 532 563 let l' ≝ joint_if_entry … fn in 533 564 let st' ≝ set_regs p regs st in 534 let pointer_in_fn ≝ mk_pointer Code (mk_block Code id) ? (mk_offset 0) in565 let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in 535 566 let pc ≝ pointer_of_point ? p … pointer_in_fn l' in 536 567 return mk_state_pc ? st' pc. % qed. 537 568 538 (* The pointer provided is the one to the *next* instruction. 539 The boolean tells wether a flow changement has occurred (i.e. 540 a non Proceed cmd was issued). Used in linking block evaluation 541 with regular one *) 569 (* The pointer provided is the one to the *next* instruction. *) 542 570 definition eval_step_flow : 543 ∀globals.∀p:sem_params.∀lbls.genv globals p → 544 state p → cpointer → step_flow p globals lbls → 545 res (bool × (state_pc p)) ≝ 546 λglobals,p,lbls,ge,st,nxt,cmd. 571 ∀globals.∀p:sem_params.∀flows.genv globals p → 572 state p → cpointer → step_flow p globals flows → res (state_pc p) ≝ 573 λglobals,p,flows,ge,st,nxt,cmd. 547 574 match cmd with 548 [ Redirect l ⇒549 ! st ← goto … ge l st (pblock nxt) ; return 〈true, st〉575 [ Redirect _ l ⇒ 576 goto … ge l st nxt 550 577 | Init id fn args dest ⇒ 551 578 let st' ≝ set_frms … (save_frame … nxt dest st) st in 552 ! st ← do_call ?? ge st' id fn args ; 553 return 〈true, st〉 554 | Proceed ⇒ 555 return 〈false, mk_state_pc ? st nxt〉 579 do_call ?? ge st' id fn args 580 | Proceed _ ⇒ 581 return mk_state_pc ? st nxt 556 582 ]. 557 583 558 definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀ lbls. genv globals p →559 state p → block → fin_step_flow p globals lbls → res (state_pc p) ≝560 λglobals,p,lbls,ge,st, b,cmd.584 definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv globals p → 585 state p → cpointer → fin_step_flow p globals flows → res (state_pc p) ≝ 586 λglobals,p,lbls,ge,st,curr,cmd. 561 587 match cmd with 562 [ FRedirect l ⇒ goto … ge l st b588 [ FRedirect _ l ⇒ goto … ge l st curr 563 589 | FTailInit id fn args ⇒ 564 590 do_call … ge st id fn args 565 | FEnd⇒591 | _ ⇒ 566 592 ! 〈st',ra〉 ← fetch_ra … st ; 567 593 ! st'' ← pop_frame … ge st; … … 572 598 ∀globals.∀p:sem_params.genv globals p → 573 599 state_pc p → joint_statement p globals → 574 IO io_out io_in ( bool × (state_pc p)) ≝600 IO io_out io_in (state_pc p) ≝ 575 601 λglobals,p,ge,st,stmt. 576 602 match stmt with 577 603 [ sequential s nxt ⇒ 578 ! 〈flow, 604 ! 〈flow,st'〉 ← eval_step … ge st s ; 579 605 ! nxtptr ← succ_pc ? p (pc … st) nxt ; 580 606 eval_step_flow … ge st' nxtptr flow 581 607 | final s ⇒ 582 ! 〈flow, st'〉 ← eval_fin_step… ge st s ;583 ! st ← eval_fin_step_flow … ge st' (pblock … (pc … st)) flow;584 return 〈true, st〉608 ! st' ← eval_fin_step_no_pc … ge st s ; 609 ! flow ← eval_fin_step_pc … ge st s ; 610 eval_fin_step_flow … ge st' (pc … st) flow 585 611 ]. 586 612 587 definition eval_state _flag: ∀globals: list ident.∀p:sem_params. genv globals p →588 state_pc p → IO io_out io_in ( bool × (state_pc p)) ≝613 definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p → 614 state_pc p → IO io_out io_in (state_pc p) ≝ 589 615 λglobals,p,ge,st. 590 616 ! s ← fetch_statement ? p … ge (pc … st) : IO ???; 591 617 eval_statement … ge st s. 592 593 definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →594 state_pc p → IO io_out io_in (state_pc p) ≝595 λglobals,p,ge,st.596 ! 〈flag,st'〉 ← eval_state_flag … ge st ;597 return st'.598 618 599 619 (* Paolo: what if in an intermediate language main finishes with an external … … 618 638 | _ ⇒ Error ? [ ] 619 639 ]). 620 640 641 (* 621 642 record evaluation_parameters : Type[1] ≝ 622 643 { globals: list ident … … 681 702 ∀pars:sem_params.fullexec io_out io_in ≝ 682 703 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars). 704 *)
Note: See TracChangeset
for help on using the changeset viewer.