Changeset 2338 for src/Clight
 Timestamp:
 Sep 26, 2012, 10:17:32 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r2319 r2338 648 648 state_with_labels_partial s1 s1' → 649 649 exec_step ge s1 = Value … 〈tr,s2〉 → 650 ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧ 651 trace_with_extra_labels tr tr' ∧ 652 state_with_labels s2 s2'. 650 ∃n. after_n_steps (S n) … clight_exec ge' s1' 651 (λtr',s2'. 652 trace_with_extra_labels tr tr' ∧ 653 state_with_labels s2 s2'). 653 654 654 655 (* General plan is like the expressions result, except that we do case analysis … … 660 661 [ #g #f #us #s #k #k' #e #m #KL cases s 661 662 [ #EX inversion KL 662 [ #E1 #E2 #_ destruct %{tr}663 [ #E1 #E2 #_ destruct 663 664 whd in EX:(??%?); 664 665 lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?); 665 [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))}666 % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E @refl667  // ]  /3/ ]666 [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct 667 %{0} whd whd in ⊢ (??%?); 668 >label_function_return >E whd % /3/ 668 669  *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct 669 670 ] 670  #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr} 671 %{(State (\fst (label_function g f)) (\fst (label_statement s0 u)) k0' e m)} 672 whd in EX:(??%%); destruct 673 % [ % [ @cl_plus_one @refl  // ]  /3/ ] 674  #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr} 675 whd in EX:(??%%); destruct 676 % [ 2: % [ % [ @cl_plus_one @refl  // ]  @swl_partial @swl_whilestate // ]  skip ] 671  #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0} whd 672 whd in EX:(??%%); destruct /4/ 673  #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0} 674 whd in EX:(??%%); destruct whd /4/ 677 675  #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 678 cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem679 cases (bindIO_inversion ??????? EX rem) * * #EXb #EXbrem EXrem680 normalize in EX brem; destruct676 cases (bindIO_inversion ??????? EX) EX * #ve #tre * #EXe #EX 677 cases (bindIO_inversion ??????? EX) EX * * #EXb #EX 678 normalize in EX; destruct 681 679 cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te 682 [ % [ 2: % [ 2: % [ % [ @cl_plus_one 683 whd in ⊢ (??%?); >EXe' in ⊢ (??%?); 684 whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?); 685 whd in ⊢ (??%?); @refl 686  // ] 687  @swl_partial @swl_dowhilestate // ]  skip ]  skip ] 688  % [ 2: % [ 2: % [ % [ @cl_plus_succ [ 689 4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?); 690 whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?); 691 whd in ⊢ (??%?); @refl 692  skip  skip 693  5: @cl_plus_succ [ 4: @refl  skip  skip 694  5: @cl_plus_one @refl  skip ]  skip ] 695  <(E0_right tr) @twel_app /2/ ] 696  /3/ ]  skip ]  skip ] 680 [ %{0} whd 681 whd in ⊢ (??%?); >EXe' 682 whd in ⊢ (??%?); >label_expr_type >EXb 683 whd % /4/ 684  %{2} whd 685 whd in ⊢ (??%?); >EXe' 686 whd in ⊢ (??%?); >label_expr_type >EXb 687 whd % [ <(E0_right tr) @twel_app /2/  /4/ ] 697 688 ] 698 689  #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 699 690 whd in EX:(??%?); destruct 700 %{ E0} % [2: % [ % [ @cl_plus_one @refl  // ]  /3/ ]  skip ]691 %{0} whd /4/ 701 692  #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 702 693 whd in EX:(??%?); destruct 703 %{ E0} % [2: % [ % [ @cl_plus_one @refl  // ]  /4/ ]  skip ]694 %{0} % /4/ 704 695  #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 705 696 whd in EX:(??%?); destruct 706 %{ E0} % [2: % [ % [ @cl_plus_one @refl  // ]  /4/ ]  skip ]697 %{0} % /4/ 707 698  #k0 #k0' #K #_ #E1 #E2 #E3 destruct 708 699 whd in EX:(??%?); destruct 709 %{ E0} % [2: % [ % [ @cl_plus_one @refl  // ]  /4/ ]  skip ]700 %{0} % /4/ 710 701  #u0 #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct 711 702 whd in EX:(??%?); 712 703 lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?); 713 704 [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct 714 %{ E0} % [2: % [ % [ @cl_plus_onewhd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);715 @refl  // ]  /4/ ]  skip ]705 %{0} whd whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?); 706 whd % /4/ 716 707  *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct 717 708 ] 718 709  #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 719 % [2: % [2: % [ % [ @cl_plus_one @refl  // ]  /3/ ] skip ] skip ]710 %{0} % /4/ 720 711 ] 721 712  * #a1 #ty1 #a2 #EX … … 724 715 cases (bindIO_inversion ??????? EX) EX #m3 * #EX3 #EX 725 716 whd in EX:(??%%); destruct 726 cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 us) #tr1' * #EX1' #T1 727 whd in match (label_statement ??); 728 @label_gen_elim #ua1 @label_gen_elim #ua2 729 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2 730 % [2: % [2: % [ % [ 731 @cl_plus_one whd in ⊢ (??%?); 732 >exec_lvalue_labelled >EX1' in ⊢ (??%?); 733 whd in ⊢ (??%?); >EX2' in ⊢ (??%?); 734 whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?); 735 @refl 736  @twel_app // ]  /3/ ]  skip ]  skip ] 717 @blindly_label #u1 #u2 718 cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 u1) #tr1' * #EX1' #T1 719 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 u2) #tr2' * #EX2' #T2 720 %{0} whd 721 whd in ⊢ (??%?); >exec_lvalue_labelled >EX1' 722 whd in ⊢ (??%?); >EX2' 723 whd in ⊢ (??%?); >label_expr_type >EX3 724 whd % [ whd in ⊢ (??%); @twel_app //  /3/ ] 737 725  * [2: * #er #tyr ] #ef #args #EX 738 726 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 743 731 [ cases (bindIO_inversion ??????? EX) EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ] 744 732 destruct 745 whd in match (label_statement ??); 746 whd in match (label_opt_expr ??); 747 [ @(label_gen_elim … (Expr er tyr)) #u' @breakup_pair  letin u' ≝ us ] 748 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u') #tr1' * #EX1' #T1 749 @label_gen_elim #u1 750 @label_gen_elim #u2 751 cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u1) #tr2' * #EX2' #T2 752 [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ] 753 cases (opt_find_funct … RG … EX3) #ux #EFF 754 % [2,4: % [2,4: % [1,3: % [1,3: 755 @cl_plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?);  >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *) 756 whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?);  >EX2' in ⊢ (??%?); ] 757 whd in ⊢ (??%?); [ >EFF in ⊢ (??%?);  >EFF in ⊢ (??%?); ] 758 whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?);  >EX4 in ⊢ (??%?); ] 759 whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ] 760 whd in ⊢ (??%?); 761 @refl  *: @twel_app /2/ ]  *: @swl_partial @swl_callstate /2/ ]  *: skip ]  *: skip ] 733 @blindly_label #u1 #u2 #u3 734 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u2) #tr1' * #EX1' #T1 735 cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u3) #tr2' * #EX2' #T2 736 [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 u1) #tr5' * #EX5' #T5 ] 737 cases (opt_find_funct … RG … EX3) #ux #EFF 738 %{0} whd 739 whd in ⊢ (??%?); >EX1' 740 whd in ⊢ (??%?); >EX2' 741 whd in ⊢ (??%?); >EFF 742 whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof >EX4 743 whd in ⊢ (??%?); [ whd in match (label_opt_expr ??); @breakup_pair whd in ⊢ (??%?); >exec_lvalue_labelled >EX5' ] 744 whd % [ 1,3: whd in ⊢ (??%); @twel_app /2/  *: @swl_partial @swl_callstate /2/ ] 762 745  #st1 #st2 #EX 763 746 whd in EX:(??%%); destruct 764 747 whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 765 %{ E0} % [2: % [ % [ @cl_plus_one @refl  // ]  @swl_partial @swl_state /2/ ]  skip ]748 %{0} % /4/ 766 749  #a #st1 #st2 #EX 767 750 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 774 757 whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7 775 758 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 776 % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: 777 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?);  >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 778 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?);  >EX2 in ⊢ (??%?); ] 779 whd in ⊢ (??%?); @refl 780  1,2,6,7: skip 781  5,10: @cl_plus_one @refl 782  *: skip 783 ] 784  2,4: <(E0_right tr) @twel_app /2/ 785 ] 2,4: /3/ ]  *: skip ]  *: skip ] 759 %{1} whd 760 whd in ⊢ (??%?); >EX1' 761 whd in ⊢ (??%?); >label_expr_type >EX2 762 whd in ⊢ (??%?); % [1,3: <(E0_right tr) ] /4/ 786 763  #a #st #EX 787 764 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 794 771 >shift_fst 795 772 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 796 % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl  1,2,6,7: skip 797  5,10: @cl_plus_succ [ 4,9: 798 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?);  >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 799 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?);  >EX2 in ⊢ (??%?); ] 800 whd in ⊢ (??%?); @refl 801  1,2,6,7: skip 802  5: @cl_plus_one @refl 803  10: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl  *: skip ] *: skip ] 804  *: skip 805 ] 806  2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/ 807 ] 2,4: /4/ ]  *: skip ]  *: skip ] 773 [ %{2}  %{3} ] whd 774 whd in ⊢ (??%?); >EX1' 775 whd in ⊢ (??%?); >label_expr_type >EX2 776 whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /5/ 808 777  #a #st #EX 809 778 normalize in EX; destruct … … 812 781 whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst 813 782 whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst 814 % [2: % [2: % [ % [ @cl_plus_succ [ 4: @refl  1,2: skip 815  5: @cl_plus_succ [ 4: @refl  1,2: skip  5: @cl_plus_one //  skip ]  skip ] 816  /2/ ]  /4/ ]  skip ]  skip ] 783 %{2} % /4/ 817 784  #st1 #a #st2 #st #EX 818 785 lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip … … 826 793 normalize in EX; destruct 827 794 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 828 % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl  1,2,6,7: skip 829  5,10: @cl_plus_succ [ 4,9: 830 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?);  >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 831 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?);  >EX2 in ⊢ (??%?); ] 832 whd in ⊢ (??%?); @refl 833  1,2,6,7: skip 834  5: @cl_plus_one @refl 835  10: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl  *: skip ] *: skip ] 836  *: skip 837 ] 838  2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/ 839 ] 2,4: /4/ ]  *: skip ]  *: skip ] 795 [ %{2}  %{3} ] whd 796 whd in ⊢ (??%?); >EX1' 797 whd in ⊢ (??%?); >label_expr_type >EX2 798 whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /4/ 840 799  whd in EX:(??%%); destruct 841 % [2: % [2: %[ %[ @cl_plus_succ [ 4: @refl  5: @cl_plus_one 842 whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip' 843 >Eskip' whd in ⊢ (??%?); @refl  *: skip ] // ]  @swl_partial @swl_state /2/ ] 844  skip ]  skip ] 800 %{1} whd 801 whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip' 802 >Eskip' whd in ⊢ (??%?); % /4/ 845 803 ] 846 804  #EX inversion KL … … 857 815 ] 858 816 whd in match (label_statement ??); 859 % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: % 860 [1,11,13: @cl_plus_one @refl  2,12,14: // 861  @cl_plus_succ [ 4: @refl  5: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl *:skip]*:skip]  /2/ 862  @cl_plus_succ [ 4: @refl  5: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl *:skip]*:skip]  /2/ 863  @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl *:skip]  /2/ 864  @cl_plus_succ [ 4: @refl  5: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl *:skip]*:skip]  /2/ 865 ] *: /3 by swl_partial, swl_state/ ]*: skip]*: skip ] 817 [ 1,6,7: %{0} % /3/ 818  2,3,5: %{2} % /3/ 819  %{1} % /3/ 820 ] 866 821  #EX inversion KL 867 822 [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct … … 877 832 ] 878 833 whd in match (label_statement ??); 879 [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: % 880 [1,3,7,9,11: @cl_plus_one @refl  5: @cl_plus_succ [4:@refl  5:@cl_plus_one @refl  *: skip ] 881  *: // ]  *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ] *:skip ] *: skip ] 834 [ 1,2,5,6,7: %{0} % /4/ 835  4: %{1} % /4/ 882 836  cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX 883 837 cases (bindIO_inversion ??????? EX) EX * * #EX2 #EX 884 838 normalize in EX; destruct 885 839 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1 886 % [2,4: % [2,4: % [1,3: % [1,3: [ @cl_plus_one  @cl_plus_succ ] [ 1,5: 887 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?);  >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 888 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?);  >EX2 in ⊢ (??%?); ] 889 whd in ⊢ (??%?); @refl 890  6: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl  *: skip ] *: skip ] 891  //  <(E0_right tr) @twel_app /2/ 892 ] 893  /3/  /3/ ]  *: skip ]  *: skip ] 840 [ %{0}  %{2} ] whd 841 whd in ⊢ (??%?); >EX1' 842 whd in ⊢ (??%?); >label_expr_type >EX2 843 whd in ⊢ (??%?); % [ 3: <(E0_right tr) ] /3/ 894 844 ] 895 845  * [2: #a ] #EX … … 908 858 [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ] 909 859 whd in EX:(??%%); destruct 910 % [2,4: % [2,4: % [1,3: %[1,3: @cl_plus_one 911 whd in ⊢ (??%?); 912 [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety'' 913 whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 914  >label_function_return >Ety in ⊢ (??%?); 915 ] whd in ⊢ (??%?); @refl 916  *: // ] *: @swl_partial @swl_returnstate /2/ ]*:skip]*:skip] 860 %{0} whd 861 whd in ⊢ (??%?); 862 [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety'' 863 whd in ⊢ (??%?); >EX1' 864  >label_function_return >Ety 865 ] whd in ⊢ (??%?); % /4/ 917 866  #a #ls #EX 918 867 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 924 873 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 925 874 whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 926 % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl927  // ] cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/928 ]skip ] skip ]875 %{0} whd 876 whd in ⊢ (??%?); >EX1' % // 877 cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/ 929 878  #l #st #EX 930 879 whd in EX:(??%?); destruct 931 880 whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst 932 881 whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst 933 %[2: %[2: %[ %[ @cl_plus_succ 934 [ 4: @refl  5: @cl_plus_one @refl  *: skip ] 935  /2/ ]  /3/ ] skip ] skip ] 882 %{1} % /3/ 936 883  #l #EX 937 884 whd in EX:(??%?); … … 943 890 cases (label_find_label_fn g … KL F) 944 891 #u' * #cs * #k1' * #F' #K' 945 % [2: %[2: %[ %[ @cl_plus_succ946 [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl  5: @cl_plus_one @refl  *: skip ]947  /2/ ]  /3/ ]  skip ]  skip ]892 %{1} whd 893 whd in ⊢ (??%?); >F' 894 % /3/ 948 895 ] 949 896  #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1 950 % [2: % [2: % [ % [ @cl_plus_one @refl  // ]  /3/ ]  skip ] skip ]897 %{0} % /3/ 951 898 ] 952 899  #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX … … 955 902 whd in EX:(??%%); destruct 956 903 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1 957 [ % [2: % [2: % [ % [ 958 @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 959 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 960 5: @cl_plus_one @refl  *: skip ] 961  <(E0_right tr) /3/ ] /4 by swl_partial, swl_state, cwl_while/ ] skip ] skip ] 962  % [2: % [2: % [ % [ 963 @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 964 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 965  5: @cl_plus_succ [4: @refl 966  5: @cl_plus_one @refl  *: skip ]  *: skip ] 967  <(E0_right tr) /3/ ] /3/ ] skip ] skip ] 968 ] 904 [ %{1}  %{2} ] whd 905 whd in ⊢ (??%?); >EX1' 906 whd in ⊢ (??%?); >label_expr_type >EX2 907 % [ 1,3: <(E0_right tr) ] /4/ 969 908  #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX 970 909 whd in EX:(??%%); destruct 971 % [2: % [2: % [ % [ 972 @cl_plus_succ [4: %  5: @cl_plus_one %  *: skip ] 973  /2/ ] /4/ ] skip ] skip ] 910 %{1} % /4/ 974 911  #u0 #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX 975 912 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 977 914 whd in EX:(??%%); destruct 978 915 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1 979 [ % [2: % [2: % [ % [ 980 @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 981 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 982  5: whd in ⊢ (?????(??%%??)??); @cl_plus_one @refl 983  *: skip ] <(E0_right tr) /3/ ]  /4/ ] skip ] skip ] 984  % [2: % [2: % [ % [ 985 @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 986 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 987  5: whd in ⊢ (?????(??%%??)??); @cl_plus_succ [4: @refl 988  5: @cl_plus_one @refl ] *: skip ] <(E0_right tr) /3/ ] /3/ ] skip ] skip 989 ] 990 ] 916 [ %{1}  %{2} ] whd 917 whd in ⊢ (??%?); >EX1' 918 whd in ⊢ (??%?); >label_expr_type >EX2 919 % [1,3: <(E0_right tr) ] /4/ 991 920  #u0 * 992 921 [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX … … 997 926 lapply (refl ? (\fst (label_function u0 f))) whd in ⊢ (???(???%) → ?); 998 927 @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef 999 % [2: % [2: % [ % [ @cl_plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?); 1000 whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl 1001  5: @cl_plus_one @refl  *: skip ]  /2/ ] <Ef @swl_partial @swl_state @K ] skip ] skip ] 928 %{1} whd 929 whd in ⊢ (??%?); >EX1 930 whd in ⊢ (??%?); >EX2 931 % /4/ 1002 932  #id #tys #ty #args #k #k' #m #K #EX 1003 933 cases (bindIO_inversion ??????? EX) EX #vs * #EX1 #EX … … 1010 940  *: normalize #A try #B try #C destruct 1011 941 ] 1012 % [2: % [2: % [ % [ @cl_plus_one @refl  // ] /2/ ] skip ] skip ]942 %{0} % /2/ 1013 943  9: #u0 #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %; 1014 944 [ #EX whd in EX:(??%?); destruct 1015 % [2: % [2: % [ % [ @cl_plus_one @refl  // ] /3/ ] skip ] skip ]945 %{0} % /3/ 1016 946  * * #b #o #ty #EX 1017 947 cases (bindIO_inversion ??????? EX) EX #m2 * #EX1 #EX 1018 948 whd in EX:(??%%); destruct 1019 % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl  // ] /3/ ] skip ] skip ]949 %{0} whd whd in ⊢ (??%?); >EX1 % /3/ 1020 950 ] 1021 951  *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O … … 1024 954  #r #EX whd in EX:(??%%); destruct 1025 955 ] qed. 1026 1027 956 1028 957 theorem step_with_labels : ∀ge,ge'. … … 1030 959 ∀s1,s1',tr,s2. 1031 960 state_with_labels s1 s1' → 1032 (exec_step ge s1 = Value … 〈tr,s2〉 →1033 ∃ tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧1034 1035 state_with_labels s2 s2').961 exec_step ge s1 = Value … 〈tr,s2〉 → 962 ∃n. after_n_steps (S n) … clight_exec ge' s1' 963 (λtr',s2'. trace_with_extra_labels tr tr' ∧ 964 state_with_labels s2 s2'). 1036 965 #ge #ge' #RG #Xs1 #Xs1' #tr #s2 * 1037 966 [ #s1 #s1' @step_with_labels_partial // … … 1044 973 >shift_fst whd in match (seq_of_labeled_statement ?); 1045 974 cases (step_with_labels_partial … RG (State f s k e m) (State (\fst (label_function u0 f)) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX) 1046 # tr' * #s2' * * #P #T #S1047 % [2: % [2: % [ % [ @cl_plus_succ [4: @refl  5: @P  *: skip ]  /2/ ] @S ] skip ] skip ]975 #n #H %{(S n)} @(after_n_m 1 (S n) … H) % /2/ 976 #trx #sx * /3/ 1048 977 (* but for LScase it's just like the cases in step_with_labels_partial *) 1049 978  #sz #i #s #ls #k #k' #e #m #K #EX … … 1052 981 @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?); 1053 982 whd in EX:(??%?); destruct 1054 % [2: % [2: % [ % [ @cl_plus_succ [4: @refl  5: @cl_plus_one @refl  *: skip ]  /2/ ] /4/ ] skip ] skip ]983 %{1} % /4/ 1055 984 ] 1056 985 ] qed. … … 1211 1140 #EX1 #F1 1212 1141 cases (step_with_labels … RG … S EX1) 1213 # tr2 * #s2' * * #PL#TWL #S'1142 #n #A cases (after_inv clight_fullexec ???? A) #tr' * #s' * * #TWL #S' 1214 1143 lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2 1215 cases (plus_final … clight_fullexec … PL F2)1144 whd in match (is_final … s'); >F2 * 1216 1145 #tr2' #S2 1217 1146 @(swl_stop … S2 TWL) … … 1220 1149 #EX1 #E1' 1221 1150 cases (step_with_labels … RG … S EX1) 1222 #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*) 1223 @(swl_steps … (plus_exec … clight_fullexec … EX2 ?)) 1224 [ whd in ⊢ (??%?); <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1) 1225  // 1226  (* Manual rewrite to prevent guardedness condition getting upset. *) 1151 #n #AF cases (after_inv clight_fullexec ???? AF) #tr' * #s' * * #TWL #S' 1152 whd in match (is_final … s'); lapply (refl ? (is_final s')) 1153 cases (is_final s') in ⊢ (???% → %); 1154 [ #NF #H whd in H; @(swl_steps … H) // 1227 1155 @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?]) 1228 1156 @build_exec // >E1' in NW1; // 1157  #r <(final_related … S') change with (is_final … clight_fullexec ge1 s1') in ⊢ (??%? → ?); 1158 >(exec_e_step_not_final ?? clight_fullexec … E1) #E destruct 1229 1159 ] 1230 1160  #E1
Note: See TracChangeset
for help on using the changeset viewer.