Changeset 2203
- Timestamp:
- Jul 17, 2012, 6:57:40 PM (6 years ago)
- Location:
- src
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Cexec.ma
r2176 r2203 551 551 definition clight_fullexec : fullexec io_out io_in ≝ 552 552 mk_fullexec ??? clight_exec make_global make_initial_state. 553 554 555 (* A few lemmas about the semantics. *) 556 557 lemma cl_step_not_final : ∀ge,s1,tr,s2. 558 exec_step ge s1 = OK … 〈tr,s2〉 → 559 is_final s1 = None ?. 560 #ge * // 561 #r #tr #s2 #E 562 whd in E:(??%%); 563 destruct 564 qed. 565 566 (* If you can step in Clight, then you aren't in a final state. Hence we can 567 give nicer constructors for plus. *) 568 lemma cl_plus_one : ∀ge,s1,tr,s2. 569 exec_step ge s1 = OK … 〈tr,s2〉 → 570 plus … clight_exec ge s1 tr s2. 571 #ge #s1 #tr #s2 #EX @(plus_one … EX) /2/ 572 qed. 573 574 lemma cl_plus_succ : ∀ge,s1,tr,s2,tr',s3. 575 exec_step ge s1 = OK … 〈tr,s2〉 → 576 plus … clight_exec ge s2 tr' s3 → 577 plus … clight_exec ge s1 (tr⧺tr') s3. 578 #ge #s1 #tr #s2 #tr' #s3 #EX @plus_succ /2/ @EX 579 qed. 580 -
src/Clight/labelSimulation.ma
r2202 r2203 314 314 . 315 315 316 (* TODO: this (or something like it) ought to be elsewhere. *)317 inductive plus (ge:genv) : state → trace → state → Prop ≝318 | plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2319 | plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3.320 321 316 (* Some details are invariant under labelling. *) 322 317 lemma label_function_return : ∀f. … … 653 648 state_with_labels_partial s1 s1' → 654 649 exec_step ge s1 = Value … 〈tr,s2〉 → 655 ∃tr',s2'. plus ge' s1' tr' s2' ∧650 ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧ 656 651 trace_with_extra_labels tr tr' ∧ 657 652 state_with_labels s2 s2'. … … 669 664 lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?); 670 665 [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))} 671 % [ % [ @ plus_one whd in ⊢ (??%?); >label_function_return >E @refl666 % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E @refl 672 667 | // ] | /3/ ] 673 668 | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct … … 676 671 %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)} 677 672 whd in EX:(??%%); destruct 678 % [ % [ @ plus_one @refl | // ] | /3/ ]673 % [ % [ @cl_plus_one @refl | // ] | /3/ ] 679 674 | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr} 680 675 whd in EX:(??%%); destruct 681 % [ 2: % [ % [ @ plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]676 % [ 2: % [ % [ @cl_plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ] 682 677 | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 683 678 cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem … … 685 680 normalize in EXbrem; destruct 686 681 cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te 687 [ % [ 2: % [ 2: % [ % [ @ plus_one682 [ % [ 2: % [ 2: % [ % [ @cl_plus_one 688 683 whd in ⊢ (??%?); >EXe' in ⊢ (??%?); 689 684 whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?); … … 691 686 | // ] 692 687 | @swl_partial @swl_dowhilestate // ] | skip ] | skip ] 693 | % [ 2: % [ 2: % [ % [ @ plus_succ [688 | % [ 2: % [ 2: % [ % [ @cl_plus_succ [ 694 689 4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?); 695 690 whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?); 696 691 whd in ⊢ (??%?); @refl 697 692 | skip | skip 698 | 5: @ plus_succ [ 4: @refl | skip | skip699 | 5: @ plus_one @refl | skip ] | skip ]693 | 5: @cl_plus_succ [ 4: @refl | skip | skip 694 | 5: @cl_plus_one @refl | skip ] | skip ] 700 695 | <(E0_right tr) @twel_app /2/ ] 701 696 | /3/ ] | skip ] | skip ] … … 703 698 | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 704 699 whd in EX:(??%?); destruct 705 %{E0} % [2: % [ % [ @ plus_one @refl | // ] | /3/ ] | skip ]700 %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ] 706 701 | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 707 702 whd in EX:(??%?); destruct 708 %{E0} % [2: % [ % [ @ plus_one @refl | // ] | /4/ ] | skip ]703 %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ] 709 704 | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 710 705 whd in EX:(??%?); destruct 711 %{E0} % [2: % [ % [ @ plus_one @refl | // ] | /4/ ] | skip ]706 %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ] 712 707 | #k0 #k0' #K #_ #E1 #E2 #E3 destruct 713 708 whd in EX:(??%?); destruct 714 %{E0} % [2: % [ % [ @ plus_one @refl | // ] | /4/ ] | skip ]709 %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ] 715 710 | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct 716 711 whd in EX:(??%?); 717 712 lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?); 718 713 [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct 719 %{E0} % [2: % [ % [ @ plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);714 %{E0} % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?); 720 715 @refl | // ] | /4/ ] | skip ] 721 716 | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct 722 717 ] 723 718 | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 724 % [2: % [2: % [ % [ @ plus_one @refl | // ] | /3/ ]| skip ]| skip ]719 % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ]| skip ]| skip ] 725 720 ] 726 721 | * #a1 #ty1 #a2 #EX … … 734 729 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2 735 730 % [2: % [2: % [ % [ 736 @ plus_one whd in ⊢ (??%?);731 @cl_plus_one whd in ⊢ (??%?); 737 732 >exec_lvalue_labelled >EX1' in ⊢ (??%?); 738 733 whd in ⊢ (??%?); >EX2' in ⊢ (??%?); … … 757 752 [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ] 758 753 % [2,4: % [2,4: % [1,3: % [1,3: 759 @ plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)754 @cl_plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *) 760 755 whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ] 761 756 whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?); … … 766 761 whd in EX:(??%%); destruct 767 762 whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 768 %{E0} % [2: % [ % [ @ plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]763 %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ] 769 764 | #a #st1 #st2 #EX 770 765 cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX … … 777 772 whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7 778 773 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 779 % [2,4: % [2,4: % [1,3: % [1,3: @ plus_succ [ 4,9:774 % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: 780 775 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 781 776 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] 782 777 whd in ⊢ (??%?); @refl 783 778 | 1,2,6,7: skip 784 | 5,10: @ plus_one @refl779 | 5,10: @cl_plus_one @refl 785 780 | *: skip 786 781 ] … … 797 792 >shift_fst 798 793 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 799 % [2,4: % [2,4: % [1,3: % [1,3: @ plus_succ [ 4,9: @refl | 1,2,6,7: skip800 | 5,10: @ plus_succ [ 4,9:794 % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip 795 | 5,10: @cl_plus_succ [ 4,9: 801 796 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 802 797 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] 803 798 whd in ⊢ (??%?); @refl 804 799 | 1,2,6,7: skip 805 | 5: @ plus_one @refl806 | 10: @ plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]800 | 5: @cl_plus_one @refl 801 | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ] 807 802 | *: skip 808 803 ] … … 815 810 whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst 816 811 whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst 817 % [2: % [2: % [ % [ @ plus_succ [ 4: @refl | 1,2: skip818 | 5: @ plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ]812 % [2: % [2: % [ % [ @cl_plus_succ [ 4: @refl | 1,2: skip 813 | 5: @cl_plus_succ [ 4: @refl | 1,2: skip | 5: @cl_plus_one // | skip ] | skip ] 819 814 | /2/ ] | /4/ ] | skip ] | skip ] 820 815 | #st1 #a #st2 #st #EX … … 829 824 normalize in EX; destruct 830 825 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 831 % [2,4: % [2,4: % [1,3: % [1,3: @ plus_succ [ 4,9: @refl | 1,2,6,7: skip832 | 5,10: @ plus_succ [ 4,9:826 % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip 827 | 5,10: @cl_plus_succ [ 4,9: 833 828 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 834 829 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] 835 830 whd in ⊢ (??%?); @refl 836 831 | 1,2,6,7: skip 837 | 5: @ plus_one @refl838 | 10: @ plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]832 | 5: @cl_plus_one @refl 833 | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ] 839 834 | *: skip 840 835 ] … … 842 837 ]| 2,4: /4/ ] | *: skip ] | *: skip ] 843 838 | whd in EX:(??%%); destruct 844 % [2: % [2: %[ %[ @ plus_succ [ 4: @refl | 5: @plus_one839 % [2: % [2: %[ %[ @cl_plus_succ [ 4: @refl | 5: @cl_plus_one 845 840 whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip' 846 841 >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ] … … 861 856 whd in match (label_statement ??); 862 857 % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: % 863 [1,11,13: @ plus_one @refl | 2,12,14: //864 | @ plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/865 | @ plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/866 | @ plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/867 | @ plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/868 ]| *: /3 / ]|*: skip]|*: skip ]858 [1,11,13: @cl_plus_one @refl | 2,12,14: // 859 | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/ 860 | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/ 861 | @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip] | /2/ 862 | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/ 863 ]| *: /3 by swl_partial, swl_state/ ]|*: skip]|*: skip ] 869 864 | #EX inversion KL 870 865 [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct … … 881 876 whd in match (label_statement ??); 882 877 [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: % 883 [1,3,7,9,11: @ plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ]878 [1,3,7,9,11: @cl_plus_one @refl | 5: @cl_plus_succ [4:@refl | 5:@cl_plus_one @refl | *: skip ] 884 879 | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ] 885 880 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX … … 887 882 normalize in EX; destruct 888 883 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1 889 % [2,4: % [2,4: % [1,3: % [1,3: [ @ plus_one | @plus_succ ] [ 1,5:884 % [2,4: % [2,4: % [1,3: % [1,3: [ @cl_plus_one | @cl_plus_succ ] [ 1,5: 890 885 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 891 886 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] 892 887 whd in ⊢ (??%?); @refl 893 | 6: @ plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]888 | 6: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ] 894 889 | // | <(E0_right tr) @twel_app /2/ 895 890 ] … … 911 906 [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ] 912 907 whd in EX:(??%%); destruct 913 % [2,4: % [2,4: % [1,3: %[1,3: @ plus_one908 % [2,4: % [2,4: % [1,3: %[1,3: @cl_plus_one 914 909 whd in ⊢ (??%?); 915 910 [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety'' … … 927 922 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 928 923 whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 929 % [2: % [2: % [ % [ @ plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl924 % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl 930 925 | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/ 931 926 ]|skip ]| skip ] … … 934 929 whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst 935 930 whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst 936 %[2: %[2: %[ %[ @ plus_succ937 [ 4: @refl | 5: @ plus_one @refl | *: skip ]931 %[2: %[2: %[ %[ @cl_plus_succ 932 [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] 938 933 | /2/ ] | /3/ ] |skip ]| skip ] 939 934 | #l #EX … … 946 941 cases (label_find_label_fn … KL F) 947 942 #u' * #cs * #k1' * #F' #K' 948 % [2: %[2: %[ %[ @ plus_succ949 [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @ plus_one @refl | *: skip ]943 % [2: %[2: %[ %[ @cl_plus_succ 944 [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @cl_plus_one @refl | *: skip ] 950 945 | /2/ ] | /3/ ] | skip ] | skip ] 951 946 ] 952 947 | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1 953 % [2: % [2: % [ % [ @ plus_one @refl | // ] | /3/ ] | skip ]| skip ]948 % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ]| skip ] 954 949 ] 955 950 | #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX … … 959 954 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1 960 955 [ % [2: % [2: % [ % [ 961 @ plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);956 @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 962 957 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 963 |5: @ plus_one @refl | *: skip ]964 | <(E0_right tr) /3/ ]| /4 / ]| skip ]| skip ]958 |5: @cl_plus_one @refl | *: skip ] 959 | <(E0_right tr) /3/ ]| /4 by swl_partial, swl_state, cwl_while/ ]| skip ]| skip ] 965 960 | % [2: % [2: % [ % [ 966 @ plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);961 @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 967 962 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 968 | 5: @ plus_succ [4: @refl969 | 5: @ plus_one @refl | *: skip ] | *: skip ]963 | 5: @cl_plus_succ [4: @refl 964 | 5: @cl_plus_one @refl | *: skip ] | *: skip ] 970 965 | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ] 971 966 ] … … 973 968 whd in EX:(??%%); destruct 974 969 % [2: % [2: % [ % [ 975 @ plus_succ [4: % | 5: @plus_one % | *: skip ]970 @cl_plus_succ [4: % | 5: @cl_plus_one % | *: skip ] 976 971 | /2/ ]| /4/ ]| skip ]| skip ] 977 972 | #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX … … 981 976 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1 982 977 [ % [2: % [2: % [ % [ 983 @ plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);978 @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 984 979 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 985 | 5: whd in ⊢ (?? (??%%??)??); @plus_one @refl980 | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_one @refl 986 981 | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ] 987 982 | % [2: % [2: % [ % [ 988 @ plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);983 @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 989 984 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 990 | 5: whd in ⊢ (?? (??%%??)??); @plus_succ [4: @refl991 | 5: @ plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip985 | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_succ [4: @refl 986 | 5: @cl_plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip 992 987 ] 993 988 ] … … 1000 995 lapply (refl ? (label_function f)) whd in ⊢ (???% → ?); 1001 996 @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef 1002 % [2: % [2: % [ % [ @ plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);997 % [2: % [2: % [ % [ @cl_plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?); 1003 998 whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl 1004 | 5: @ plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]999 | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ] 1005 1000 | #id #tys #ty #args #k #k' #m #K #EX 1006 1001 cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX … … 1013 1008 | *: normalize #A try #B try #C destruct 1014 1009 ] 1015 % [2: % [2: % [ % [ @ plus_one @refl | // ]| /2/ ]| skip ]| skip ]1010 % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /2/ ]| skip ]| skip ] 1016 1011 | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %; 1017 1012 [ #EX whd in EX:(??%?); destruct 1018 % [2: % [2: % [ % [ @ plus_one @refl | // ]| /3/ ]| skip ]| skip ]1013 % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /3/ ]| skip ]| skip ] 1019 1014 | * * #b #o #ty #EX 1020 1015 cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX 1021 1016 whd in EX:(??%%); destruct 1022 % [2: % [2: % [ % [ @ plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]1017 % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ] 1023 1018 ] 1024 1019 | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O … … 1034 1029 state_with_labels s1 s1' → 1035 1030 (exec_step ge s1 = Value … 〈tr,s2〉 → 1036 ∃tr',s2'. plus ge' s1' tr' s2' ∧1031 ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧ 1037 1032 trace_with_extra_labels tr tr' ∧ 1038 1033 state_with_labels s2 s2'). … … 1048 1043 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) 1049 1044 #tr' * #s2' * * #P #T #S 1050 % [2: % [2: % [ % [ @ plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]1045 % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ] 1051 1046 (* but for LScase it's just like the cases in step_with_labels_partial *) 1052 1047 | #sz #i #s #ls #k #k' #e #m #K #EX … … 1055 1050 @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?); 1056 1051 whd in EX:(??%?); destruct 1057 % [2: % [2: % [ % [ @ plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]1052 % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ] 1058 1053 ] 1059 1054 ] qed. … … 1188 1183 1189 1184 1190 lemma not_wrong_init : ∀p.1191 not_wrong state (exec_inf … clight_fullexec p) →1192 ∃s. make_initial_state … p = OK ? s.1193 #p whd in ⊢ (??% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);1194 cases (make_initial_state p)1195 [ /2/1196 | normalize #m #NW @⊥1197 inversion NW #H1 #H2 #H3 #H4 try #H5 destruct1198 ] qed.1199 1185 1200 1186 lemma final_related : ∀s1,s2. … … 1204 1190 [ #s1y #s2y * // 1205 1191 | // 1206 ] qed.1207 1208 lemma plus_not_final : ∀ge,s,tr,s'.1209 plus ge s tr s' →1210 is_final s = None ?.1211 #ge #s0 #tr0 #s0' *1212 [ #s1 #tr #s2 #EX | #s1 #tr #s2 #tr' #s3 #EX #PL ]1213 lapply (refl ? (is_final s1))1214 cases (is_final s1) in ⊢ (???% → %);1215 //1216 #r cases s1 in EX ⊢ %;1217 #H9 #H10 #H11 try #H12 try #H13 try #H14 try #H151218 [ 1,5: whd in H15:(??%?); | 2,6: whd in H14:(??%?); | 3,7: whd in H13:(??%?); | 4,8: whd in H11:(??%?); ]1219 destruct1220 normalize in H10;1221 destruct1222 qed.1223 1224 lemma plus_exec : ∀ge,s,tr,s'.1225 plus ge s tr s' →1226 is_final s' = None ? →1227 steps state tr1228 (exec_inf_aux … clight_fullexec ge (exec_step ge s))1229 (exec_inf_aux … clight_fullexec ge (exec_step ge s')).1230 #ge #s0 #tr0 #s0' #P elim P1231 [ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold1232 whd in ⊢ (???%?);1233 whd in match (is_final ?????); >NF1234 %21235 | #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF1236 >exec_inf_aux_unfold >EX11237 whd in ⊢ (???%?);1238 whd in match (is_final ?????); >(plus_not_final … P2)1239 %3 @IH //1240 ] qed.1241 1242 lemma plus_exec_final : ∀ge,s,tr,s',r.1243 plus ge s tr s' →1244 is_final s' = Some ? r →1245 ∃tr'. steps state tr1246 (exec_inf_aux … clight_fullexec ge (exec_step ge s))1247 (e_stop … tr' r s').1248 #ge #s0 #tr0 #s0' #r #P elim P1249 [ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold1250 %{tr} whd in ⊢ (???%?);1251 whd in match (is_final ?????); >F1252 %11253 | #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #F1254 cases (IH … F)1255 #tr' #S' %{tr'}1256 >exec_inf_aux_unfold >EX11257 whd in ⊢ (???%?);1258 whd in match (is_final ?????); >(plus_not_final … P2)1259 %3 @S'1260 1192 ] qed. 1261 1193 … … 1278 1210 #tr2 * #s2' * * #PL #TWL #S' 1279 1211 lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2 1280 cases (plus_ exec_final ?????PL F2)1212 cases (plus_final … clight_fullexec … PL F2) 1281 1213 #tr2' #S2 1282 1214 @(swl_stop … S2 TWL) … … 1286 1218 cases (step_with_labels … RG … S EX1) 1287 1219 #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*) 1288 @(swl_steps … (plus_exec … EX2 ?))1289 [ <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)1220 @(swl_steps … (plus_exec … clight_fullexec … EX2 ?)) 1221 [ whd in ⊢ (??%?); <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1) 1290 1222 | // 1291 1223 | (* Manual rewrite to prevent guardedness condition getting upset. *) … … 1330 1262 #p 1331 1263 #NW 1332 cases (not_wrong_init p NW)1333 #s1 #I11264 cases (not_wrong_init clight_fullexec p NW) 1265 whd in ⊢ (% → ??%? → ?); #s1 #I1 1334 1266 cases (initial_state_in_simulation … I1) 1335 1267 #s2 * #I2 -
src/common/Executions.ma
r2202 r2203 11 11 | steps_steps : ∀tr,s,e,tr',e'. steps state tr e e' → steps state (tr'⧺tr) (e_step … tr' s e) e'. 12 12 13 (* Go from individual steps to part of an execution trace. *) 14 lemma plus_exec : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s'. 15 plus … FE gl s tr s' → 16 is_final … FE gl s' = None ? → 17 steps (state … gl) tr 18 (exec_inf_aux … FE gl (step … FE gl s)) 19 (exec_inf_aux … FE gl (step … FE gl s')). 20 #FE #gl #s0 #tr0 #s0' #P elim P 21 [ #s1 #tr #s2 #NF1 #EX #NF2 >EX >exec_inf_aux_unfold 22 whd in ⊢ (???%?); >NF2 23 %2 24 | #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #NF3 25 >EX1 >exec_inf_aux_unfold 26 whd in ⊢ (???%?); >(plus_not_final … P2) /3/ 27 ] qed. 28 29 lemma plus_final : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s',r. 30 plus … FE gl s tr s' → 31 is_final … FE gl s' = Some ? r → 32 ∃tr'. steps (state … gl) tr 33 (exec_inf_aux … FE gl (step … FE gl s)) 34 (e_stop … tr' r s'). 35 #FE #gl #s0 #tr0 #s0' #r #P elim P 36 [ #s1 #tr #s2 #NF1 #EX #F2 >EX >exec_inf_aux_unfold 37 whd in ⊢ (??(λ_.???%?)); >F2 38 %{tr} %1 39 | #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #F3 40 >EX1 >exec_inf_aux_unfold 41 whd in ⊢ (??(λ_.???%?)); >(plus_not_final … P2) 42 cases (IH F3) #tr'' #S' %{tr''} /2/ 43 ] qed. 44 13 45 (* In some places we do not consider wrong executions. *) 14 46 … … 18 50 | nw_interact : ∀o,k. (∀i. not_wrong state (k i)) → not_wrong state (e_interact … o k). 19 51 52 lemma not_wrong_not_wrong : ∀state,m. 53 ¬ (not_wrong state (e_wrong … m)). 54 #state #m % #NW inversion NW 55 #A #B #C #D #E destruct 56 qed. 57 58 lemma not_wrong_steps : ∀state,e,e',tr. 59 steps state tr e e' → 60 not_wrong state e → 61 not_wrong state e'. 62 #state #e0 #e0' #tr0 #S elim S 63 [ // 64 | #tr #s #e #NW inversion NW 65 #A #B #C #D #E try #F destruct // 66 | #tr #s #e #tr' #e' #S' #IH #NW @IH 67 inversion NW 68 #A #B #C #D #E try #F destruct // 69 ] qed. 70 71 lemma not_wrong_init : ∀FE,p. 72 not_wrong ? (exec_inf … FE p) → 73 ∃s. make_initial_state … p = OK ? s. 74 #FE #p whd in ⊢ (??% → ?); 75 cases (make_initial_state ??? p) 76 [ /2/ 77 | normalize #m #NW @⊥ 78 inversion NW #H1 #H2 #H3 #H4 try #H5 destruct 79 ] qed. 80 81 20 82 (* One execution is simulated by another, but possibly using a different number 21 of steps. *) 83 of steps. Note that we have to allow for several steps at the end to make 84 the trace match up. *) 22 85 23 coinductive simulates ( state:Type[0]) : execution state io_out io_in → execution stateio_out io_in → Prop ≝24 | sim_stop : ∀tr, tr',r,s1,s2,e1,e2.25 steps state tr e1 (e_stop … tr'r s1) →26 steps state tr e2 (e_stop … tr'r s2) →27 simulates statee1 e286 coinductive simulates (S1,S2:Type[0]) : execution S1 io_out io_in → execution S2 io_out io_in → Prop ≝ 87 | sim_stop : ∀tr,r,s1,s2,e1,e2,tr1,tr2. 88 steps S1 tr e1 (e_stop … tr1 r s1) → 89 steps S2 tr e2 (e_stop … tr2 r s2) → 90 simulates S1 S2 e1 e2 28 91 | sim_steps : ∀tr,e1,e1',e2,e2'. 29 steps statetr e1 e1' →30 steps statetr e2 e2' →31 simulates statee1' e2' →32 simulates statee1 e292 steps S1 tr e1 e1' → 93 steps S2 tr e2 e2' → 94 simulates S1 S2 e1' e2' → 95 simulates S1 S2 e1 e2 33 96 | sim_interact : ∀o,k1,k2. 34 (∀i. simulates state(k1 i) (k2 i)) →35 simulates state(e_interact … o k1) (e_interact … o k2).97 (∀i. simulates S1 S2 (k1 i) (k2 i)) → 98 simulates S1 S2 (e_interact … o k1) (e_interact … o k2). 36 99 100 101 (* Result for lifting simulations on states to simulations on execution traces. 102 At the time of writing this hasn't been used in anger yet... 103 104 This probably isn't the best route for the stages of the compiler that have 105 results in terms of structured traces, but it should be good for the 106 front-end. 107 *) 108 109 let corec build_cofix_simulation 110 (FS1,FS2:fullexec io_out io_in) 111 (g1:global … FS1) (g2:global … FS2) 112 (SIM:state … g1 → state … g2 → Prop) 113 (s1:state … g1) (s2:state … g2) 114 (NF:is_final … FS1 g1 s1 = None ?) 115 (S:SIM s1 s2) 116 (SIM_FINAL: ∀x,y. SIM x y → is_final … FS1 g1 x = is_final … FS2 g2 y) 117 (SIM_GOOD: ∀x,y. SIM x y → 118 not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 x)) → 119 is_final … FS1 g1 x = None ? → 120 ∃tr,x',y'. And (plus … FS1 g1 x tr x') (And (plus … FS2 g2 y tr y') (SIM x' y')) ) 121 (NW:not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1))) 122 : simulates ?? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)) (exec_inf_aux ?? FS2 g2 (step … FS2 g2 s2)) ≝ ?. 123 lapply (SIM_GOOD … S NW NF) 124 * #tr * #s1' * #s2' * #P1 * #P2 #S' 125 lapply (refl ? (is_final … FS1 g1 s1')) 126 cases (is_final … s1') in ⊢ (???% → ?); 127 [ #NF1 128 @(sim_steps … tr … (build_cofix_simulation … S' SIM_FINAL SIM_GOOD ?)) 129 [ @(plus_exec … P1) // 130 | @(plus_exec … P2) <SIM_FINAL // 131 | @(not_wrong_steps … (plus_exec … P1 …)) // 132 | // 133 ] 134 | #r #F1 135 cases (plus_final … P1 F1) #tr1' #S1 136 cases (plus_final … P2 ?) [ 3: <SIM_FINAL [ @F1 | // | skip ] | 2: skip ] #tr2' #S2 137 @(sim_stop … S1 S2) 138 ] qed. 139 140 theorem lift_simulation : ∀FE1,FE2:fullexec io_out io_in. 141 ∀p1:program … FE1. ∀p2:program … FE2. 142 let g1 ≝ make_global … p1 in 143 let g2 ≝ make_global … p2 in 144 ∀SIM: state … g1 → state … g2 → Prop. 145 ∀SIM_INIT: ∀s1. make_initial_state … p1 = OK ? s1 → 146 ∃s2. And (make_initial_state … p2 = OK ? s2) (SIM s1 s2). 147 ∀SIM_FINAL: ∀x,y. SIM x y → is_final … FE1 g1 x = is_final … FE2 g2 y. 148 ∀SIM_GOOD: ∀x,y. SIM x y → 149 not_wrong ? (exec_inf_aux … FE1 g1 (step … FE1 g1 x)) → 150 is_final … FE1 g1 x = None ? → 151 ∃tr,x',y'. And (plus … FE1 g1 x tr x') (And (plus … FE2 g2 y tr y') (SIM x' y')). 152 let e1 ≝ exec_inf … FE1 p1 in 153 let e2 ≝ exec_inf … FE2 p2 in 154 not_wrong … e1 → 155 simulates … e1 e2. 156 157 #FE1 #FE2 #p1 #p2 158 letin g1 ≝ (make_global … p1) 159 letin g2 ≝ (make_global … p2) 160 #SIM #SIM_INIT #SIM_FINAL #SIM_GOOD 161 #NW 162 cases (not_wrong_init … p1 NW) 163 #s1 #I1 164 cases (SIM_INIT … I1) #s2 * #I2 #S 165 whd in NW:(??%) ⊢ (???%%); 166 >I1 in NW ⊢ %; >I2 whd in ⊢ (??% → ???%%); 167 change with g1 in match (make_global … p1); 168 change with g2 in match (make_global … p2); 169 170 >exec_inf_aux_unfold whd in ⊢ (??% → ???%?); 171 lapply (SIM_FINAL … S) 172 lapply (refl ? (is_final … s1)) 173 cases (is_final … s1) in ⊢ (???% → %); 174 [ #F1 #F2 >(exec_inf_aux_unfold … FE2) whd in ⊢ (??% → ???%%); 175 <F2 whd in ⊢ (? → ???%%); #NW 176 @(sim_steps … E0 … (build_cofix_simulation … SIM_FINAL SIM_GOOD …)) try assumption 177 [ // | // | inversion NW #A #B #C #D #E try #F destruct assumption ] 178 | #r #F1 #F2 #NW whd in ⊢ (???%%); 179 >exec_inf_aux_unfold whd in ⊢ (???%%); 180 <F2 whd in ⊢ (???%%); 181 @(sim_stop … (steps_stop …) (steps_stop …)) 182 ] qed. 183 -
src/common/SmallstepExec.ma
r2202 r2203 19 19 repeat n' ?? exec g s1 20 20 ]. 21 22 (* We take care here to check that we're not at the final state. It is not 23 necessarily the case that a success step guarantees this (e.g., because 24 there may be no way to stop a processor, so an infinite loop is used 25 instead). *) 26 inductive plus (O) (I) (TS:trans_system O I) (ge:global … TS) : state … TS ge → trace → state … TS ge → Prop ≝ 27 | plus_one : ∀s1,tr,s2. 28 is_final … TS ge s1 = None ? → 29 step … TS ge s1 = OK … 〈tr,s2〉 → 30 plus … ge s1 tr s2 31 | plus_succ : ∀s1,tr,s2,tr',s3. 32 is_final … TS ge s1 = None ? → 33 step … TS ge s1 = OK … 〈tr,s2〉 → 34 plus … ge s2 tr' s3 → 35 plus … ge s1 (tr⧺tr') s3. 36 37 lemma plus_not_final : ∀O,I,FE. ∀gl,s,tr,s'. 38 plus O I FE gl s tr s' → 39 is_final … FE gl s = None ?. 40 #O #I #FE #gl #s0 #tr0 #s0' * // 41 qed. 21 42 22 43 let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
Note: See TracChangeset
for help on using the changeset viewer.