Changeset 941 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 11, 2011, 11:37:20 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r940 r941 1962 1962 qed. 1963 1963 1964 lemma split_eq_status: 1965 ∀T. 1966 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10. 1967 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10. 1968 A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 → 1969 mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 = 1970 mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10. 1971 // 1972 qed. 1973 1964 1974 lemma main_thm: 1965 1975 ∀ps,s,s''. … … 2017 2027 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) 2018 2028 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX % 2019  (* short *) 2020  (* medium *) 2021 ] 2029  (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; H1; 2030 generalize in match 2031 (refl ? 2032 (sub_16_with_carry 2033 (sigma 〈preamble,instr_list〉 (program_counter … ps)) 2034 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label)) 2035 false)) 2036 cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta; 2037 generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta; 2038 generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; 2039 #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)] 2040 generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2041 change in ⊢ (? → ??%?) with (execute_1_0 ??) 2042 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 2043 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2044 >H2b >(eq_instruction_to_eq … H2a) 2045 generalize in match EQ; EQ; 2046 whd in ⊢ (???% → ?); 2047 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) 2048 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?) 2049 generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower))) 2050 cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4 2051 @split_eq_status try % change with (newpc = sigma ? (address_of_word_labels ps label)) 2052 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *) 2053  (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; H1; 2054 generalize in match 2055 (refl … 2056 (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label)))) 2057 cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1 2058 generalize in match 2059 (refl … 2060 (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps)))) 2061 cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2 2062 generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc)) 2063 cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)] 2064 generalize in match (option_destruct_Some ??? TEQ) TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?) 2065 change in ⊢ (? →??%?) with (execute_1_0 ??) 2066 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 2067 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2068 >H2b >(eq_instruction_to_eq … H2a) 2069 generalize in match EQ; EQ; 2070 whd in ⊢ (???% → ?); 2071 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?) 2072 change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?) 2073 generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc))) 2074 cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4 2075 generalize in match (refl … (split bool 4 4 pc_bu)) 2076 cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5 2077 generalize in match (refl … (split bool 3 8 rest_addr)) 2078 cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6 2079 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?) 2080 generalize in match 2081 (refl … 2082 (half_add 16 (sigma 〈preamble,instr_list〉 newppc) 2083 ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2))) 2084 cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7 2085 @split_eq_status try % 2086 [ change with (? = sigma ? (address_of_word_labels ps label)) 2087 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *) 2088  whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 2089 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] 2022 2090 5: (* Call *) 2023 2091 6: (* Mov *)
Note: See TracChangeset
for help on using the changeset viewer.