 Timestamp:
 Jun 6, 2012, 6:27:56 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2018 r2020 860 860 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 861 861 whd in match execute_1_preinstruction; normalize nodelta 862 [30: (* CJNE *) 862 [31: (* DJNZ *) 863 (* XXX: work on the right hand side *) 864 >p normalize nodelta 865 (* XXX: switch to the left hand side *) 866 instr_refl >EQP P normalize nodelta 867 #sigma_increment_commutation #maps_assm #fetch_many_assm 868 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 869 whd in match (expand_relative_jump ????); 870 <EQppc in fetch_many_assm; 871 @pair_elim #result #flags #sub16_refl 872 @pair_elim #upper #lower #split_refl 873 cases (eq_bv ???) normalize nodelta 874 [1: 875 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 876 whd in ⊢ (??%?); 877 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 878 (* XXX: work on the left hand side *) 879 check pair_replace 880 @(pair_replace ?????????? p) normalize nodelta 881 [1: 882 cases daemon 883 ] 884 (* XXX: switch to the right hand side *) 885 normalize nodelta >EQs s >EQticks ticks 886 cases (¬ eq_bv ???) normalize nodelta 887 whd in ⊢ (??%%); 888 (* XXX: finally, prove the equality using sigma commutation *) 889 @split_eq_status try % 890 cases daemon 891 2: 892 >EQppc 893 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 894 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 895 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 896 #fetch_many_assm whd in fetch_many_assm; %{2} 897 change with (execute_1 ?? = ?) 898 @(pose … (execute_1 ? (status_of_pseudo_status …))) 899 #status_after_1 #EQstatus_after_1 900 <(?: ? = status_after_1) 901 [3: 902 >EQstatus_after_1 in ⊢ (???%); 903 whd in ⊢ (???%); 904 <fetch_refl in ⊢ (???%); 905 whd in ⊢ (???%); 906 @(pair_replace ?????????? p) 907 [1: 908 cases daemon 909 2: 910 normalize nodelta 911 whd in match (addr_of_relative ????); 912 cases (¬ eq_bv ???) normalize nodelta 913 >set_clock_mk_Status_commutation 914 whd in ⊢ (???%); 915 change with (add ???) in match (\snd (half_add ???)); 916 >set_arg_8_set_program_counter in ⊢ (???%); 917 [2,4: cases daemon ] 918 >program_counter_set_program_counter in ⊢ (???%); 919 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 920 [2,4: 921 >bitvector_of_nat_sign_extension_equivalence 922 [1,3: 923 >EQintermediate_pc' % 924 *: 925 repeat @le_S_S @le_O_n 926 ] 927 ] 928 [1: % ] 929 ] 930 1: 931 skip 932 ] 933 [2: 934 status_after_1 935 @(pose … (execute_1 ? (mk_PreStatus …))) 936 #status_after_1 #EQstatus_after_1 937 <(?: ? = status_after_1) 938 [3: 939 >EQstatus_after_1 in ⊢ (???%); 940 whd in ⊢ (???%); 941 (* XXX: matita bug with patterns across multiple goals *) 942 <fetch_refl'' in ⊢ (???%); 943 whd in ⊢ (???%); % 944 1: 945 skip 946 ] 947 status_after_1 whd in ⊢ (??%?); 948 (* XXX: switch to the right hand side *) 949 normalize nodelta >EQs s >EQticks ticks 950 cases (¬ eq_bv ???) normalize nodelta 951 whd in ⊢ (??%%); 952 ] 953 (* XXX: finally, prove the equality using sigma commutation *) 954 @split_eq_status XXX try % 955 cases daemon 956 30: (* CJNE *) 863 957 (* XXX: work on the right hand side *) 864 958 cases addr1 addr1 #addr1 normalize nodelta … … 909 1003 #status_after_1 #EQstatus_after_1 910 1004 <(?: ? = status_after_1) 911 [3,6: 1005 [2,5: 1006 inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta 1007 3,6: 912 1008 >EQstatus_after_1 in ⊢ (???%); 913 1009 whd in ⊢ (???%); … … 930 1026 repeat @le_S_S @le_O_n 931 1027 ] 1028 1,5: 1029 % 932 1030 ] 933 [1,3: % ] 1031 1,4: skip 1032 ] 1033 [1,2,3,4: 1034 status_after_1 1035 @(pose … (execute_1 ? (mk_PreStatus …))) 1036 #status_after_1 #EQstatus_after_1 1037 <(?: ? = status_after_1) 1038 [3,6,9,12: 1039 >EQstatus_after_1 in ⊢ (???%); 1040 whd in ⊢ (???%); 1041 (* XXX: matita bug with patterns across multiple goals *) 1042 [1: <fetch_refl'' in ⊢ (???%); 1043 2: <fetch_refl'' in ⊢ (???%); 1044 3: <fetch_refl'' in ⊢ (???%); 1045 4: <fetch_refl'' in ⊢ (???%); 1046 ] % 1047 1,4,7,10: 1048 skip 1049 ] 1050 status_after_1 whd in ⊢ (??%?); 1051 (* XXX: switch to the right hand side *) 1052 normalize nodelta >EQs s >EQticks ticks 1053 whd in ⊢ (??%%); 1054 ] 1055 (* XXX: finally, prove the equality using sigma commutation *) 1056 @split_eq_status try % 1057 [3: 1058 whd in ⊢ (??%?); 1059 cases daemon 1060 *: 1061 cases daemon 934 1062 ] 935 1063 ]
Note: See TracChangeset
for help on using the changeset viewer.