 Timestamp:
 Oct 30, 2012, 4:18:20 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/StatusSimulation.ma
r2413 r2421 15 15 include "common/StructuredTraces.ma". 16 16 17 (* We work with two relations on states in parallel, as well as two derived ones. 18 sem_rel is the classic semantic relation between states, keeping track of 19 memory and how program counters are mapped between languages. 20 call_rel keeps track of what pcs corresponding calls have and just that: 21 this is different than corresponance between program counters in sem_rel when 22 CALL f ↦ instr* CALL f instr* *) 23 17 24 record status_rel 18 25 (S1 : abstract_status) … … 24 31 necessary for as_after_return (typically just the program counter) 25 32 maybe what function is called too? *) 26 ; call_rel : (Σs.∃f.as_classifier S1 s (cl_call f)) →27 (Σs.∃f.as_classifier S2 s (cl_call f)) → Prop33 ; call_rel : ∀f.(Σs.as_classifier S1 s (cl_call f)) → 34 (Σs.as_classifier S2 s (cl_call f)) → Prop 28 35 ; sim_final : 29 36 ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2 30 37 }. 31 38 32 (* if we later genralise, we should move this inside status_rel *) 39 (* The two derived relations are 40 label_rel which tells that the two states are colabelled 41 ret_rel which tells that two return states are in relation: the idea is that 42 it happens when "going back" through as_after_return on one side we get 43 a pair of call_rel related states, then we enjoy as_after_return also on the 44 other. Roughly call_rel will store just enough information so that we can 45 advance locally on a return step and build structured traces any way *) 46 47 (* if we later generalise, we should move this inside status_rel *) 33 48 definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2. 34 49 35 50 definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.λs1,s2. 36 ∀s1_pre,s2_pre.as_after_return S1 s1_pre s1 → call_rel … R s1_pre s2_pre → 37 as_after_return S2 s2_pre s2. 38 39 (* the equivalent of a collapsable trace_any_label where we do not forse 51 ∀f,s1_pre,s2_pre.call_rel … R f s1_pre s2_pre → 52 as_after_return S1 «s1_pre, ex_intro … (pi2 … s1_pre)» s1 → 53 as_after_return S2 «s2_pre, ex_intro … (pi2 … s2_pre)» s2. 54 55 (* the equivalent of a collapsable trace_any_label where we do not force 40 56 costedness of the lookahead status *) 41 57 inductive trace_any_any_free (S : abstract_status) : S → S → Type[0] ≝ … … 51 67 ]. 52 68 53 (* notice: labels and semantic relation between states are not in sync *) 69 (* the base property we ask for simulation to work depends on the status_class 70 S will mark semantic relation, C call relation, L label relation, R return relation *) 71 54 72 record status_simulation 55 73 (S1 : abstract_status) … … 60 78 ∀st1,st1',c,st2.as_execute S1 st1 st1' → 61 79 sim_status_rel st1 st2 → 62 ∀prf : as_classifier S1 st1 c. (* < watch out, different from status_simulation *)80 ∀prf : as_classifier S1 st1 c. 63 81 match c return λc.as_classifier S1 st1 c → ? with 64 [ cl_call _ ⇒ λprf. 65 ∃st2_pre_call.call_rel ?? sim_status_rel «st1, ex_intro … prf» st2_pre_call ∧ 82 [ cl_call f ⇒ λprf. 83 (* 84 st1' S\ 85 ↑ \ \ 86 st1 \L\ \ 87  \ \ \ 88 S \C\ st2_after_call →taa→ st2' 89  \ ↑ 90 st2 →taa→ st2_pre_call 91 *) 92 ∃st2_pre_call.call_rel ?? sim_status_rel f «st1, prf» st2_pre_call ∧ 66 93 ∃st2_after_call,st2'. 67 94 ∃taa2 : trace_any_any … st2 st2_pre_call. … … 71 98 label_rel … st1' st2_after_call 72 99  cl_return ⇒ λ_. 100 (* 101 st1 102 / ↓ 103  st1'S,L\ 104 S \ \ 105 \ \R\  106 \   107 st2 →taa→ st2_ret   108 ↓ /  109 st2_after_ret →taaf→ st2' 110 111 we also ask that st2_after_ret be not labelled if the taaf tail is 112 not empty 113 *) 73 114 ∃st2_ret,st2_after_ret,st2'. 74 115 ∃taa2 : trace_any_any … st2 st2_ret. 75 116 ∃taa2' : trace_any_any_free … st2_after_ret st2'. 76 117 (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ 77 as_classifier … st2_ret cl_return (* is it really important? *)∧118 as_classifier … st2_ret cl_return ∧ 78 119 as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧ 79 120 ret_rel … sim_status_rel st1' st2_after_ret ∧ 80 121 label_rel … st1' st2' 81 122  _ ⇒ λ_. 82 (* this allows to freely exchange cl_other and cl_jump, 123 (* 124 st1 → st1' 125  \ 126 S S,L 127  \ 128 st2 →taaf→ st2' 129 130 the taaf can be empty (e.g. tunneling) but we ask it must not be the 131 case when both st1 and st1' are labelled (we would be able to collapse 132 labels otherwise) 133 also notice that this allows to freely exchange cl_other and cl_jump, 83 134 but if cl_jump imposed labels before, they will be kept afterwards *) 84 135 ∃st2'. 85 136 ∃taa2 : trace_any_any_free … st2 st2'. 86 137 (* we ensure no labels are collapsed. Technicality? *) 87 (if taaf_non_empty … taa2 then True else ¬as_costed … st1) ∧138 (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ 88 139 sim_status_rel st1' st2' ∧ 89 140 label_rel … st1' st2' 90 141 ] prf 91 142 }. 143 144 145 (* some useful lemmas *) 92 146 93 147 let rec taa_append_taa S st1 st2 st3 … … 174 228 qed. 175 229 230 lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2. 231 if taa_non_empty … taa then ¬as_costed … s2 else True. 232 #S #s1 #s2 #taa elim taa s1 s2 normalize nodelta 233 [ #s1 % 234  #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl s2 s3 235 [ #s2 #H #K #_ assumption 236  #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I 237 ] 238 ] 239 qed. 240 176 241 let rec tal_collapsable_to_rel S fl st1 st2 177 242 (tal : trace_any_label S fl st1 st2) on tal : … … 215 280 216 281 let rec status_simulation_produce_tlr S1 S2 (R : status_simulation S1 S2) 282 (* we start from this situation 283 st1 →→→→tlr→→→→ st1' 284  \ 285 L \S\ 286  \ 287 st2_lab →taa→ st2 (the taa preamble is in general either empty or given 288 by the preceding call) 289 290 and we produce 291 st1 →→→→tlr→→→→ st1' 292 \\ / \ 293 // R \L,S\ 294 \\  \ 295 st2_lab →tlr→ st2_mid →taaf→ st2' 296 *) 217 297 st1 st1' st2_lab st2 218 298 (tlr1 : trace_label_return S1 st1 st1') … … 230 310 ] 231 311 and status_simulation_produce_tll S1 S2 (R : status_simulation S1 S2) 312 (* we start from this situation 313 st1 →→→→tll→→→ st1' 314  \ 315 L \S\ 316  \ 317 st2_lab →taa→ st2 318 319 and if the tll is a returning one we produce a diagram like the one for tlr, 320 otherwise a simpler: 321 st1 →→→→tll→→→→ st1' 322 \\  323 // L,S 324 \\  325 st2_lab →→→tll→→→ st2' 326 *) 232 327 fl st1 st1' st2_lab st2 233 328 (tll1 : trace_label_label S1 fl st1 st1') … … 250 345 ] 251 346 and status_simulation_produce_tal S1 S2 (R : status_simulation S1 S2) 347 (* we start from this situation 348 st1 →→tal→→ st1' 349  350 S 351  352 st2 353 354 and if the tal is a returning one we produce a diagram like the one for tlr, 355 otherwise we allow for two possibilities: 356 either 357 358 st1 →→tal→→ st1' 359 \\  360 // L,S 361 \\  362 st2 →→tal→→ st2' 363 364 or we do not advance from st2: 365 366 st1 →→tal→→ st1' collapsable, and st1 uncosted 367 / 368 /L,S/ 369 / 370 st2 371 *) 252 372 fl st1 st1' st2 253 373 (tal1 : trace_any_label S1 fl st1 st1') … … 306 426 #st2' ** st2 st2' 307 427 [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *) 308 ** whd in ⊢ (%→?); #ncost #R' #L' %2 /4 by conj/ 428 ** whd in ⊢ (%→?); * 429 [1,3: #ncost #R' #L' %2 /4 by conj/ 430 *: * #ABS elim (ABS K) 431 ] 309 432 *: #st2 #st2_mid #st2' #taa2 #H2 #I2 *** #st1_R_st2' #st1_L_st2' %1 310 433 %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 (or_intror ?? I2) ?))} … … 323 446  (* tal_base_call *) whd 324 447 elim (sim_execute … R … H st1_R_st2 G) 325 * #st2_pre_call * #f#G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2448 * #st2_pre_call #G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 326 449 #st1_R_st2_mid #st1_L_st2_after_call 327 450 elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call) … … 348 471  (* tal_step_call *) 349 472 elim (sim_execute … R … H st1_R_st2 G) 350 * #st2_pre_call * #f#G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2473 * #st2_pre_call #G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 351 474 #st1_R_st2_mid #st1_L_st2_after_call 352 475 elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call) … … 393 516  (* step_default *) 394 517 elim (sim_execute … R … H st1_R_st2 G) 395 #st2_mid *#taa2 ** # cost #st1_R_st2_mid #st1_L_st2_mid518 #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid 396 519 lapply (status_simulation_produce_tal … tl1 st1_R_st2_mid) 397 520 cases fl1' in tl1; #tl1 * … … 404 527 [2: % [/2 by conj/] @taaf_append_tal_rel @G ] 405 528 ] 406  lapply st1_L_st2_mid lapply st1_R_st2_mid lapply cost 407 cases taa2 st2_mid st2 408 [ #st2 #cost #_ #_ *#H #G %2 %{H cost} ] 409 #st2 #st2_mid' #st2_mid #hd #H2 #I2 * #st1_R_st2_mid #st1_L_st2_mid 410 *** #H #G #K #L %1 411 %[ %{(hd @ tal_base_not_return ??? H2 (or_intror ?? I2) ?)} 412 [2: % [/2 by conj/] @taa_append_tal_rel @tal_collapsable_to_rel assumption 413 1: whd <G @(tal_end_costed … tl1) 414 ]] 529  (* can't happen *) 530 *** #_ #L' elim (absurd ?? K) 531 whd >st1_L_st2_mid <L' @(tal_end_costed … tl1) 415 532 ] 416 533 @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption 417 534 ] 418 535 qed. 536 537 (* finite flat traces, with recursive structure right to left. The list of 538 identifiers represents the call stack *) 539 540 inductive flat_trace (S : abstract_status) (start : S) : S → list ident → Type[0] ≝ 541  ft_start : flat_trace S start start [ ] 542  ft_advance_flat : 543 ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 → 544 (as_classifier ? st1 cl_jump ∨ as_classifier ? st1 cl_other) → 545 flat_trace S start st2 stack 546  ft_advance_call : 547 ∀st1,st2,stack,f.flat_trace S start st1 stack → as_execute S st1 st2 → 548 as_classifier ? st1 (cl_call f) → 549 flat_trace S start st2 (f :: stack) 550  ft_advance_ret : 551 ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 → 552 as_classifier ? st1 cl_return → 553 flat_trace S start st2 stack. 554 555 let rec ft_extend_taa S st1 st2 stack st3 (ft : flat_trace S st1 st2 stack) 556 (taa : trace_any_any S st2 st3) 557 on taa : flat_trace S st1 st3 stack ≝ 558 match taa return λst2,st3,taa.flat_trace ?? st2 ? → flat_trace ?? st3 ? with 559 [ taa_base s ⇒ λacc.acc 560  taa_step st1 st2 st3 H G _ tl ⇒ 561 λacc.ft_extend_taa ????? (ft_advance_flat ????? acc H (or_intror … G)) tl 562 ] ft. 563 564 lemma ft_extend_extend_taa : ∀S,st1,st2,stack,st3,st4,ft,taa1,taa2. 565 ft_extend_taa S st1 st3 stack st4 (ft_extend_taa ?? st2 ?? ft taa1) taa2 = 566 ft_extend_taa … ft (taa_append_taa … taa1 taa2). 567 #S #st1 #st2 #stack #st3 #st4 #ft #taa1 lapply ft elim taa1 st2 st3 normalize 568 /2/ 569 qed. 570 571 definition ft_extend_taaf ≝ λS,st1,st2,stack,st3.λft : flat_trace S st1 st2 stack. 572 λtaaf : trace_any_any_free S st2 st3. 573 match taaf return λst2,st3,taaf.flat_trace ?? st2 ? → flat_trace ?? st3 ? with 574 [ taaf_base s ⇒ λft.ft 575  taaf_step s1 s2 s3 pre H G ⇒ 576 λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_intror … G) 577 ] ft. 578 579 definition option_to_list : ∀A.option A → list A ≝ λA,x. 580 match x with 581 [ Some x ⇒ [x] 582  None ⇒ [ ] 583 ]. 584 585 (* the observables of a flat trace (for the moment, only labels, calls and returns) *) 586 587 inductive intensional_event : Type[0] ≝ 588  IEVcost : costlabel → intensional_event 589  IEVcall : ident → intensional_event 590  IEVret : ident → intensional_event. 591 592 let rec ft_observables_aux acc S st st' stack 593 (ft : flat_trace S st st' stack) on ft : list intensional_event ≝ 594 match ft with 595 [ ft_start ⇒ acc 596  ft_advance_flat st1_mid st1' stack pre1 _ _ ⇒ 597 let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in 598 ft_observables_aux (add @ acc) … pre1 599  ft_advance_call st1_mid st1' stack f pre1 _ _ ⇒ 600 let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in 601 let add ≝ add @ [IEVcall f] in 602 ft_observables_aux (add @ acc) … pre1 603  ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒ 604 let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in 605 let add ≝ add @ [IEVret f] in 606 ft_observables_aux (add @ acc) … pre1 607 ]. 608 609 definition ft_observables ≝ ft_observables_aux [ ]. 610 611 lemma ft_observables_aux_def : ∀acc,S,st1,st2,stack,ft. 612 ft_observables_aux acc S st1 st2 stack ft = ft_observables … ft @ acc. 613 #acc #S #st1 #st2 #stack #ft lapply acc acc elim ft st2 stack 614 [ // ] 615 #st2 #st3 [2,3: #f ] #stack #pre #H #G #IH #acc 616 whd in ⊢ (??%(??%?)); 617 >IH >IH >append_nil // 618 qed. 619 620 lemma ft_extend_taa_obs : ∀S,st1,st2,stack,st3,ft,taa. 621 ft_observables … (ft_extend_taa S st1 st2 stack st3 ft taa) = 622 ft_observables … ft @ 623 if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]. 624 #S #st1 #st2 #stack #st3 #ft #taa lapply ft elim taa st2 st3 625 [ #st2 #ft >append_nil % ] 626 #st2 #st3 #st4 #H #K #G #taa #IH #ft 627 normalize in ⊢ (??(?????%)?); >IH 628 IH lapply G lapply H cases taa st3 st4 normalize nodelta 629 [ #st3 #H #G 630  #st3 #st4 #st5 #ex #H' #G' #taa #H #G 631 whd in match (as_label ? st3); >(not_costed_no_label … G) 632 ] >append_nil whd in ⊢ (??%?); >ft_observables_aux_def >append_nil % 633 qed. 634 635 lemma ft_extend_taa_advance_call_obs : ∀S,st1,st2,stack,st3,st4. 636 ∀ft : flat_trace S st1 st2 stack. 637 ∀taa : trace_any_any S st2 st3. 638 ∀f.∀H : as_execute S st3 st4.∀G. 639 ft_observables … (ft_advance_call … f (ft_extend_taa … ft taa) H G) = 640 ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVcall f]. 641 #S #st1 #st2 #stack #st3 #st4 #ft #taa #f #H #G 642 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil 643 >ft_extend_taa_obs 644 lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa st2 st3 645 [ #st2 * #ft #H >append_nil % 646  #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H 647 whd in match (as_label ? st3); >(not_costed_no_label … K) 648 normalize nodelta // 649 ] 650 qed. 651 652 lemma ft_extend_taa_advance_ret_obs : ∀S,st1,st2,stack,f,st3,st4. 653 ∀ft : flat_trace S st1 st2 (f :: stack). 654 ∀taa : trace_any_any S st2 st3. 655 ∀H : as_execute S st3 st4.∀G. 656 ft_observables … (ft_advance_ret … (ft_extend_taa … ft taa) H G) = 657 ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVret f]. 658 #S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G 659 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil 660 >ft_extend_taa_obs 661 lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa st2 st3 662 [ #st2 * #ft #H >append_nil % 663  #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H 664 whd in match (as_label ? st3); >(not_costed_no_label … K) 665 normalize nodelta // 666 ] 667 qed. 668 669 lemma ft_extend_taa_advance_flat_obs : ∀S,st1,st2,stack,st3,st4. 670 ∀ft : flat_trace S st1 st2 stack. 671 ∀taa : trace_any_any S st2 st3. 672 ∀H : as_execute S st3 st4.∀G. 673 ft_observables … (ft_advance_flat … (ft_extend_taa … ft taa) H G) = 674 ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l). 675 #S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G 676 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil 677 >ft_extend_taa_obs 678 lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa st2 st3 679 [ #st2 * #ft #H >append_nil % 680  #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H 681 whd in match (as_label ? st3); >(not_costed_no_label … K) 682 normalize nodelta >append_nil // 683 ] 684 qed. 685 686 lemma ft_extend_taaf_obs : ∀S,st1,st2,stack,st3,ft,taaf. 687 ft_observables … (ft_extend_taaf S st1 st2 stack st3 ft taaf) = 688 ft_observables … ft @ 689 if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]. 690 #S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa st2 st3 691 [ #st2 #ft >append_nil % ] 692 #st2 #st3 #st4 #taa #H normalize nodelta #G #ft 693 @ft_extend_taa_advance_flat_obs 694 qed. 695 696 (* little helper to avoid splitting equal cases *) 697 lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed. 698 699 theorem status_simulation_produce_ft : 700 (* from 701 702 st1 →→→ft→→→ st1' 703  704 R,L 705  706 st2 707 708 we produce 709 710 st1 →→→ft→→→ st1'\ 711 // \ \ 712 \\ L S 713 //  \ 714 st2 →→→ft→→→ st2_lab →taa→ st2' 715 716 so that from any tlr or tll following st1' we can produce the corresponding 717 structured trace from st2_lab using the previous result 718 *) 719 ∀S1,S2. 720 ∀R : status_simulation S1 S2. 721 ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack. 722 label_rel … st1 st2 → R st1 st2 → 723 ∃st2_lab,st2'. 724 ∃ft2 : flat_trace S2 st2 st2_lab stack. 725 ∃taa : trace_any_any S2 st2_lab st2'. 726 label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2. 727 #S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #H #G elim ft1 st1' stack 728 [ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] % 729 *: #st1_mid #st1' #stack [2,3: #f] #ft1 #ex [3: *] #cl 730 (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S 731 elim (sim_execute … ex G' cl) 732 [1,2: (* jump or other *) 733 #st2' *#taaf ** #ncost #G'' #H'' 734 %{st2'} %{st2'} 735 %[1,3: 736 @(ft_extend_taaf … taaf) 737 @(ft_extend_taa … taa) 738 assumption] 739 %{(taa_base …)} 740 % [1,3: %{H'' G''} ] 741 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil 742 lapply ncost lapply taa lapply H'' cases taaf st2_mid st2' 743 [1,3: #st2' #H'' #taa * #ncost 744 >ft_extend_taa_obs <L' 745 [1,3: whd in match (as_label ? st1_mid); 746 >(not_costed_no_label … ncost) >if_eq >S % 747 *: lapply L' lapply H'' lapply S lapply ft2 cases taa st2_lab st2' 748 [1,3: #st2' #ft2 #S #H'' #L' >append_nil 749 whd in match (as_label ??); >not_costed_no_label 750 [1,3: >append_nil @S ] 751 whd in ⊢ (?%); >L' <H'' assumption 752 *: normalize nodelta #st2_mid #st2_mid' #st2' #_ #_ #_ #taa #ft2 #S #_ #_ 753 >S % 754 ] 755 ] 756 *: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' #_ #taa * 757 whd in ⊢ (???(?????%)); 758 >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs 759 >S >L' % 760 ] 761 3: (* call *) 762 * #st2_pre_call #cl' * #_ * #st2_after_call * #st2' 763 * #taa2 * #taa2' ** #ex' #G'' #H'' 764 %{st2_after_call} %{st2'} 765 %[@(ft_advance_call … ex' cl') 766 @(ft_extend_taa … (taa_append_taa … taa taa2)) 767 assumption] 768 %{taa2'} 769 % [ %{H'' G''} ] 770 >ft_extend_taa_advance_call_obs 771 whd in ⊢ (??%?); 772 >ft_observables_aux_def >append_nil 773 >S >L' % 774 4: (* ret *) 775 #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2' 776 ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'} 777 %[@(ft_extend_taaf … taa2') 778 @(ft_advance_ret … f … ex' cl') 779 @(ft_extend_taa … (taa_append_taa … taa taa2)) 780 assumption] 781 %{(taa_base …)} 782 % [ %{H'' G''} ] 783 >ft_extend_taaf_obs 784 >ft_extend_taa_advance_ret_obs 785 whd in ⊢ (??%?); 786 >ft_observables_aux_def >append_nil 787 lapply ncost cases taa2' st2_after_ret st2' 788 [ #st2' * >append_nil 789  #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' #ncost 790 whd in match (as_label ? st2_after_ret); >(not_costed_no_label … ncost) 791 >if_eq >append_nil 792 ] 793 >S >L' % 794 ] 795 ] 796 qed.
Note: See TracChangeset
for help on using the changeset viewer.