 Timestamp:
 Sep 26, 2012, 10:17:32 AM (8 years ago)
 Location:
 src
 Files:

 3 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 
src/common/Executions.ma
r2206 r2338 41 41 whd in ⊢ (??(λ_.???%?)); >(plus_not_final … P2) 42 42 cases (IH F3) #tr'' #S' %{tr''} /2/ 43 ] qed. 44 45 (* And similarly for after_n_steps *) 46 47 lemma after_inv : ∀FE:fullexec io_out io_in. 48 ∀n,g,P,s. 49 after_n_steps (S n) … FE g s P → 50 ∃tr,s'. 51 P tr s' ∧ 52 match is_final ?? FE g s' with 53 [ Some r ⇒ ∃tr'. 54 steps ? tr (exec_inf_aux … FE g (step … FE g s)) 55 (e_stop ??? tr' r s') 56  None ⇒ 57 steps ? tr (exec_inf_aux … FE g (step … FE g s)) 58 (exec_inf_aux … FE g (step … FE g s')) 59 ]. 60 #FE #n #g #P 61 (* Rather nasty generalisation *) 62 #s whd in ⊢ (% → ?); cases (is_final … s) [2: #r * ] whd in ⊢ (% → ?); #AW 63 cut (∃tr,s'. P (E0⧺tr) s' ∧ ?) [3: #H @H  skip ] 64 generalize in match E0 in AW ⊢ %; generalize in match s; s 65 elim n 66 [ #s #tr whd in ⊢ (% → %); 67 cases (step … s) [ #o #K *  3: #m * ] 68 * #tr' #s' #AW %{tr'} %{s'} %{AW} 69 lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %); 70 [ #NF whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF @steps_step 71  #r #F whd %{tr'} >exec_inf_aux_unfold whd in ⊢ (???%?); >F whd in ⊢ (???%?); @steps_stop 72 ] 73  #n' #IH #s #tr whd in ⊢ (% → ?); 74 cases (step … s) [ #o #K *  3: #m * ] * #tr1 #s1 75 whd in ⊢ (% → ?); lapply (refl ? (is_final … s1)) cases (is_final … s1) in ⊢ (???% → %); 76 [ 2: #r #_ * ] #NF1 whd in ⊢ (% → ?); #AW1 77 cases (IH s1 ? AW1) 78 #tr' * #s' * #p #H1 %{(tr1⧺tr')} %{s'} 79 lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %); 80 [ #NF <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF1 81 @steps_steps >NF in H1; // 82  #r #F <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (??(λ_.???%?)); >NF1 83 >F in H1; whd in ⊢ (% → ?); * #tr1 #H1 %{tr1} 84 @steps_steps @H1 85 ] 43 86 ] qed. 44 87 
src/common/SmallstepExec.ma
r2203 r2338 17 17 [ O ⇒ Value ??? 〈E0, s〉 18 18  S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s; 19 repeat n' ?? exec g s1 19 ! 〈tn,sn〉 ← repeat n' ?? exec g s1; 20 Value ??? 〈t1⧺tn,sn〉 20 21 ]. 21 22 … … 51 52 ]. 52 53 54 (* A third version of making several steps (!) 55 56 The idea here is to have a computational definition of reducing serveral 57 steps then showing some property about the resulting trace and state. By 58 careful use of let rec we can ensure that reduction stops in a sensible 59 way whenever the number of steps or the step currently being executed is 60 not (reducible to) a value. 61 62 For example, we state a property to prove by something like 63 64 ∃n. after_n_steps n … clight_exec ge s (λtr,s'. <some property>) 65 66 then start reducing by giving the number of steps and reducing the 67 definition 68 69 %{3} whd 70 71 and then whenever the reduction gets stuck, the currently reducing step is 72 the third subterm, which we can reduce and unblock with (for example) 73 rewriting 74 75 whd in ⊢ (??%?); >EXe' 76 77 and at the end reduce with whd to get the property as the goal. 78 79 There's an inversionlike result to get back the information contained in 80 the proof in Executions.ma. 81 82 *) 83 84 record await_value_stuff : Type[2] ≝ { 85 avs_O : Type[0]; 86 avs_I : avs_O → Type[0]; 87 avs_exec : trans_system avs_O avs_I; 88 avs_g : global ?? avs_exec 89 }. 90 91 let rec await_value (avs:await_value_stuff) 92 (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs)))) 93 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝ 94 match v with 95 [ Value ts ⇒ P (\fst ts) (\snd ts) 96  _ ⇒ False 97 ]. 98 99 let rec after_aux (avs:await_value_stuff) 100 (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace) 101 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) 102 on n : Prop ≝ 103 match n with 104 [ O ⇒ P tr s 105  S n' ⇒ 106 match is_final … s with 107 [ None ⇒ 108 await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s. 109 after_aux avs n' s (tr ⧺ tr') P) 110  _ ⇒ False 111 ] 112 ]. 113 114 definition after_n_steps : nat → 115 ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec. 116 state ?? exec g → 117 (trace → state ?? exec g → Prop) → Prop ≝ 118 λn,O,I,exec,g,s,P. after_aux (mk_await_value_stuff O I exec g) n s E0 P. 119 120 lemma after_n_covariant : ∀n,O,I,exec,g,P,Q. 121 (∀tr,s. P tr s → Q tr s) → 122 ∀s. 123 after_n_steps n O I exec g s P → 124 after_n_steps n O I exec g s Q. 125 #n #O #I #exec #g #P #Q #H whd in ⊢ (? → % → %); generalize in match E0; elim n 126 [ normalize /2/ 127  #n' #IH #tr #s 128 normalize cases (is_final … s) normalize [ 2: #_ * ] cases (step O I exec g s) normalize /4/ 129 ] qed. 130 131 (* for joining a couple of these together *) 132 133 lemma after_n_m : ∀n,m,O,I,exec,g,P,Q,s,s'. 134 after_n_steps m O I exec g s' Q → 135 after_n_steps n O I exec g s (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) → 136 after_n_steps (n+m) O I exec g s P. 137 #n #m #O #I #exec #g #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n 138 [ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2 139 whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %; 140 generalize in match s; s 141 elim m 142 [ #s #tr' whd in ⊢ (% → %); @H2 143  #m' #IH #s #tr' whd in ⊢ (% → %); 144 cases (is_final … s) [2: #r * ] 145 whd in ⊢ (% → %); 146 cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %); >Eapp_assoc @IH ] 147  #n' #IH #tr #s #s' #H whd in ⊢ (% → %); 148 cases (is_final … s) [2: #r * ] 149 whd in ⊢ (% → %); 150 cases (step O I exec g s) [1,3: normalize // ] 151 * #tr1 #s1 whd in ⊢ (% → %); @IH @H 152 ] qed. 153 154 53 155 (* A (possibly nonterminating) execution. *) 54 156 coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
Note: See TracChangeset
for help on using the changeset viewer.