Changeset 1922 for src/Clight/labelSimulation.ma
 Timestamp:
 May 8, 2012, 3:41:43 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r1920 r1922 322 322 qed. 323 323 324 inductive state_with_labels : state → state → Prop ≝325  swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m)324 inductive state_with_labels_partial : state → state → Prop ≝ 325  swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m) 326 326 (* Extra matching states that we can reach that don't quite correspond to the 327 327 labelling function *) 328 328  swl_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → 329 state_with_labels (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)329 state_with_labels_partial (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) 330 330  swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → 331 state_with_labels (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)331 state_with_labels_partial (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) 332 332  swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → 333 state_with_labels (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) 333 state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) 334 (* and the rest *) 335  swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (label_fundef fd) args k' m) 336  swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m) 337  swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r) 338 . 339 340 (* We handle the switch states after the rest so that we can reuse the partial 341 result. *) 342 inductive state_with_labels : state → state → Prop ≝ 343  swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s' 334 344  swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' → 335 345 state_with_labels (State f (seq_of_labeled_statement ls) k e m) 336 346 (State (label_function f) (seq_of_labeled_statement (\fst (label_lstatements ls u))) k' e m) 337 (* and the rest *)338  swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels (Callstate fd args k m) (Callstate (label_fundef fd) args k' m)339  swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels (Returnstate res k m) (Returnstate res k' m)340  swl_finalstate : ∀r. state_with_labels (Finalstate r) (Finalstate r)341 347 . 342 348 … … 550 556 ] 551 557 ] qed. 558 559 lemma label_fn_params : ∀f. 560 fn_params (label_function f) = fn_params f. 561 * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // 562 qed. 563 564 lemma label_fn_vars : ∀f. 565 fn_vars (label_function f) = fn_vars f. 566 * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // 567 qed. 552 568 553 569 (* Apply induction hypothesis while getting Matita to infer the continuations … … 731 747 qed. 732 748 733 lemma step_with_labels : ∀ge,ge'. 749 (* We show the main simulation in two stages. First, we show it for all states 750 in the relation *except* those for labeled_statements, then we'll show the 751 whole thing. This is so that we can appeal to the other cases in the proof 752 for labeled_statements. *) 753 lemma step_with_labels_partial : ∀ge,ge'. 734 754 related_globals ge ge' → 735 755 ∀s1,s1',tr,s2. 736 state_with_labels s1 s1' →756 state_with_labels_partial s1 s1' → 737 757 exec_step ge s1 = Value … 〈tr,s2〉 → 738 ∃tr',s2'. plus ge' s1' tr' s2' ∧739 trace_with_extra_labels tr tr' ∧740 state_with_labels s2 s2'.758 ∃tr',s2'. plus ge' s1' tr' s2' ∧ 759 trace_with_extra_labels tr tr' ∧ 760 state_with_labels s2 s2'. 741 761 #ge #ge' #RG #Xs1 #Xs1' #tr #s2 * 742 762 [ #f #us #s #k #k' #e #m #KL cases s … … 747 767 [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list ? m (blocks_of_env e)))} 748 768 % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl 749  // ]  / 2/ ]769  // ]  /3/ ] 750 770  *: #A [ 1,3,5,6,7,8: #B  4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct 751 771 ] … … 753 773 %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)} 754 774 whd in EX:(??%%); destruct 755 % [ % [ @plus_one @refl  // ]  / 2/ ]775 % [ % [ @plus_one @refl  // ]  /3/ ] 756 776  #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr} 757 777 whd in EX:(??%%); destruct 758 % [ 2: % [ % [ @plus_one @refl  // ]  @swl_ whilestate // ]  skip ]778 % [ 2: % [ % [ @plus_one @refl  // ]  @swl_partial @swl_whilestate // ]  skip ] 759 779  #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 760 780 cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem … … 767 787 whd in ⊢ (??%?); @refl 768 788  // ] 769  @swl_ dowhilestate // ]  skip ]  skip ]789  @swl_partial @swl_dowhilestate // ]  skip ]  skip ] 770 790  % [ 2: % [ 2: % [ % [ @plus_succ [ 771 791 4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?); … … 776 796  5: @plus_one @refl  skip ]  skip ] 777 797  <(E0_right tr) @twel_app /2/ ] 778  / 2/ ]  skip ]  skip ]798  /3/ ]  skip ]  skip ] 779 799 ] 780 800  #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct … … 783 803  #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 784 804 whd in EX:(??%?); destruct 785 %{E0} % [2: % [ % [ @plus_one @refl  // ]  / 3/ ]  skip ]805 %{E0} % [2: % [ % [ @plus_one @refl  // ]  /4/ ]  skip ] 786 806  #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 787 807 whd in EX:(??%?); destruct 788 %{E0} % [2: % [ % [ @plus_one @refl  // ]  / 3/ ]  skip ]808 %{E0} % [2: % [ % [ @plus_one @refl  // ]  /4/ ]  skip ] 789 809  #k0 #k0' #K #_ #E1 #E2 #E3 destruct 790 810 whd in EX:(??%?); destruct 791 %{E0} % [2: % [ % [ @plus_one @refl  // ]  / 3/ ]  skip ]811 %{E0} % [2: % [ % [ @plus_one @refl  // ]  /4/ ]  skip ] 792 812  #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct 793 813 whd in EX:(??%?); … … 795 815 [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct 796 816 %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?); 797 @refl  // ]  / 3/ ]  skip ]817 @refl  // ]  /4/ ]  skip ] 798 818  *: #A [ 1,3,5,6,7,8: #B  4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct 799 819 ] 800 820  #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 801 % [2: % [2: % [ % [ @plus_one @refl  // ]  / 2/ ] skip ] skip ]821 % [2: % [2: % [ % [ @plus_one @refl  // ]  /3/ ] skip ] skip ] 802 822 ] 803 823  * #a1 #ty1 #a2 #EX … … 816 836 whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?); 817 837 @refl 818  @twel_app // ]  / 2/ ]  skip ]  skip ]838  @twel_app // ]  /3/ ]  skip ]  skip ] 819 839  * [2: * #er #tyr ] #ef #args #EX 820 840 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 839 859 whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?);  >EX4 in ⊢ (??%?); ] 840 860 whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ] 841 @refl  *: @twel_app /2/ ]  *: @swl_ callstate /2/ ]  *: skip ]  *: skip ]861 @refl  *: @twel_app /2/ ]  *: @swl_partial @swl_callstate /2/ ]  *: skip ]  *: skip ] 842 862  #st1 #st2 #EX 843 863 whd in EX:(??%%); destruct 844 864 whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 845 %{E0} % [2: % [ % [ @plus_one @refl  // ]  @swl_ state /2/ ]  skip ]865 %{E0} % [2: % [ % [ @plus_one @refl  // ]  @swl_partial @swl_state /2/ ]  skip ] 846 866  #a #st1 #st2 #EX 847 867 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 863 883 ] 864 884  2,4: <(E0_right tr) @twel_app /2/ 865 ] 2,4: / 2/ ]  *: skip ]  *: skip ]885 ] 2,4: /3/ ]  *: skip ]  *: skip ] 866 886  #a #st #EX 867 887 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 885 905 ] 886 906  2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/ 887 ] 2,4: / 3/ ]  *: skip ]  *: skip ]907 ] 2,4: /4/ ]  *: skip ]  *: skip ] 888 908  #a #st #EX 889 909 normalize in EX; destruct … … 894 914 % [2: % [2: % [ % [ @plus_succ [ 4: @refl  1,2: skip 895 915  5: @plus_succ [ 4: @refl  1,2: skip  5: @plus_one //  skip ]  skip ] 896  /2/ ]  / 3/ ]  skip ]  skip ]916  /2/ ]  /4/ ]  skip ]  skip ] 897 917  #st1 #a #st2 #st #EX 898 918 lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip … … 917 937 ] 918 938  2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/ 919 ] 2,4: / 3/ ]  *: skip ]  *: skip ]939 ] 2,4: /4/ ]  *: skip ]  *: skip ] 920 940  whd in EX:(??%%); destruct 921 941 % [2: % [2: %[ %[ @plus_succ [ 4: @refl  5: @plus_one 922 942 whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip' 923 >Eskip' whd in ⊢ (??%?); @refl  *: skip ] // ]  @swl_ state /2/ ]943 >Eskip' whd in ⊢ (??%?); @refl  *: skip ] // ]  @swl_partial @swl_state /2/ ] 924 944  skip ]  skip ] 925 945 ] … … 943 963  @plus_succ [ 4: @refl  5: @plus_one @refl *:skip]  /2/ 944 964  @plus_succ [ 4: @refl  5: @plus_succ [ 4: @refl  5: @plus_one @refl *:skip]*:skip]  /2/ 945 ] *: / 2/ ]*: skip]*: skip ]965 ] *: /3/ ]*: skip]*: skip ] 946 966  #EX inversion KL 947 967 [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct … … 959 979 [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: % 960 980 [1,3,7,9,11: @plus_one @refl  5: @plus_succ [4:@refl  5:@plus_one @refl  *: skip ] 961  *: // ]  *: /3 by cwl_for3, swl_state, swl_whilestate/ ] *:skip ] *: skip ]981  *: // ]  *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ] *:skip ] *: skip ] 962 982  cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX 963 983 cases (bindIO_inversion ??????? EX) EX * * #EX2 #EX … … 971 991  //  <(E0_right tr) @twel_app /2/ 972 992 ] 973  /3/  / 2/ ]  *: skip ]  *: skip ]993  /3/  /3/ ]  *: skip ]  *: skip ] 974 994 ] 975 995  * [2: #a ] #EX … … 994 1014  >label_function_return >Ety in ⊢ (??%?); 995 1015 ] whd in ⊢ (??%?); @refl 996  *: // ] *: @swl_ returnstate /2/ ]*:skip]*:skip]1016  *: // ] *: @swl_partial @swl_returnstate /2/ ]*:skip]*:skip] 997 1017  #a #ls #EX 998 1018 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 1013 1033 %[2: %[2: %[ %[ @plus_succ 1014 1034 [ 4: @refl  5: @plus_one @refl  *: skip ] 1015  /2/ ]  / 2/ ] skip ] skip ]1035  /2/ ]  /3/ ] skip ] skip ] 1016 1036  #l #EX 1017 1037 whd in EX:(??%?); … … 1025 1045 % [2: %[2: %[ %[ @plus_succ 1026 1046 [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl  5: @plus_one @refl  *: skip ] 1027  /2/ ]  / 2/ ]  skip ]  skip ]1047  /2/ ]  /3/ ]  skip ]  skip ] 1028 1048 ] 1029 1049  #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1 1030 % [2: % [2: % [ % [ @plus_one @refl  // ]  / 2/ ]  skip ] skip ]1050 % [2: % [2: % [ % [ @plus_one @refl  // ]  /3/ ]  skip ] skip ] 1031 1051 ] 1032 1052  #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX … … 1039 1059 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 1040 1060 5: @plus_one @refl  *: skip ] 1041  <(E0_right tr) /3/ ] / 3/ ] skip ] skip ]1061  <(E0_right tr) /3/ ] /4/ ] skip ] skip ] 1042 1062  % [2: % [2: % [ % [ 1043 1063 @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); … … 1045 1065  5: @plus_succ [4: @refl 1046 1066  5: @plus_one @refl  *: skip ]  *: skip ] 1047  <(E0_right tr) /3/ ] / 2/ ] skip ] skip ]1067  <(E0_right tr) /3/ ] /3/ ] skip ] skip ] 1048 1068 ] 1049 1069  #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX … … 1051 1071 % [2: % [2: % [ % [ 1052 1072 @plus_succ [4: %  5: @plus_one %  *: skip ] 1053  /2/ ] / 3/ ] skip ] skip ]1073  /2/ ] /4/ ] skip ] skip ] 1054 1074  #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX 1055 1075 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 1061 1081 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 1062 1082  5: whd in ⊢ (??(??%%??)??); @plus_one @refl 1063  *: skip ] <(E0_right tr) /3/ ]  / 3/ ] skip ] skip ]1083  *: skip ] <(E0_right tr) /3/ ]  /4/ ] skip ] skip ] 1064 1084  % [2: % [2: % [ % [ 1065 1085 @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 1066 1086 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 1067 1087  5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl 1068  5: @plus_one @refl ] *: skip ] <(E0_right tr) /3/ ] /2/ ] skip ] skip 1069 ] 1070 ] 1071  #f #u * [ #s  #sz #i #s #ls ] #k #k' #e #m #K #EX 1072 whd in EX:(??(??(??%???))?); 1088  5: @plus_one @refl ] *: skip ] <(E0_right tr) /3/ ] /3/ ] skip ] skip 1089 ] 1090 ] 1091  * 1092 [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX 1093 cases (bindIO_inversion ??????? EX) EX #m2 * #EX2 #EX 1094 whd in EX:(??%%); destruct 1095 whd in match (label_fundef ?); 1096 whd in match (label_function ?); 1097 lapply (refl ? (label_function f)) whd in ⊢ (???% → ?); 1098 @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef 1099 % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?); 1100 whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl 1101  5: @plus_one @refl  *: skip ]  /2/ ] <Ef @swl_partial @swl_state @K ] skip ] skip ] 1102  #id #tys #ty #args #k #k' #m #K #EX 1103 cases (bindIO_inversion ??????? EX) EX #vs * #EX1 #EX 1104 cases (bindIO_inversion ??????? EX) EX #ety * #EX2 #EX 1105 whd in EX2:(??%%); destruct 1106 ] 1107  #res #k #k' #m #K #EX inversion K 1108 [ #E1 #E2 #E3 destruct cases res in EX ⊢ %; 1109 [ 2: * #i #EX whd in EX:(??%?); destruct 1110  *: normalize #A try #B try #C destruct 1111 ] 1112 % [2: % [2: % [ % [ @plus_one @refl  // ] /2/ ] skip ] skip ] 1113  9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %; 1114 [ #EX whd in EX:(??%?); destruct 1115 % [2: % [2: % [ % [ @plus_one @refl  // ] /3/ ] skip ] skip ] 1116  * * #b #o #ty #EX 1117 cases (bindIO_inversion ??????? EX) EX #m2 * #EX1 #EX 1118 whd in EX:(??%%); destruct 1119 % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl  // ] /3/ ] skip ] skip ] 1120 ] 1121  *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O 1122 destruct whd in EX:(??%?); destruct 1123 ] 1124  #r #EX whd in EX:(??%%); destruct 1125 ] qed. 1126 1127 lemma step_with_labels : ∀ge,ge'. 1128 related_globals ge ge' → 1129 ∀s1,s1',tr,s2. 1130 state_with_labels s1 s1' → 1131 (exec_step ge s1 = Value … 〈tr,s2〉 → 1132 ∃tr',s2'. plus ge' s1' tr' s2' ∧ 1133 trace_with_extra_labels tr tr' ∧ 1134 state_with_labels s2 s2'). 1135 #ge #ge' #RG #Xs1 #Xs1' #tr #s2 * 1136 [ #s1 #s1' @step_with_labels_partial // 1137  #f #u * 1138 (* If we have LSdefault we need to smuggle the execution of the cost label in 1139 before the actual statement. *) 1140 [ #s #k #k' #e #m #K #EX 1141 whd in EX:(??(??(??%???))?); 1142 whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2 1143 >shift_fst whd in match (seq_of_labeled_statement ?); 1144 cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX) 1145 #tr' * #s2' * * #P #T #S 1146 % [2: % [2: % [ % [ @plus_succ [4: @refl  5: @P  *: skip ]  /2/ ] @S ] skip ] skip ] 1147 (* but for LScase it's just like the cases in step_with_labels_partial *) 1148  #sz #i #s #ls #k #k' #e #m #K #EX 1149 whd in EX:(??(??(??%???))?); 1150 whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2 1151 @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?); 1152 whd in EX:(??%?); destruct 1153 % [2: % [2: % [ % [ @plus_succ [4: @refl  5: @plus_one @refl  *: skip ]  /2/ ] /4/ ] skip ] skip ] 1154 ] 1155 ] qed. 1156 1157 1158 1159 1160
Note: See TracChangeset
for help on using the changeset viewer.