 Timestamp:
 Jul 31, 2012, 6:08:00 PM (9 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2279 r2282 863 863 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M) 864 864 else 865 match lookup_from_internal_ram … d M with 866 [ None ⇒ 867 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M) 868  Some ul_addr ⇒ 869 Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) ul_addr M) 870 ] 865 Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (lookup_from_internal_ram … d M) M) 871 866  _ ⇒ λother: False. ⊥ 872 867 ] (subaddressing_modein … addr1) 
src/ASM/AssemblyProofSplit.ma
r2279 r2282 1157 1157 ] 1158 1158 ] 1159  *)12: (* JC *)1159 12: (* JC *) 1160 1160 >EQP P normalize nodelta 1161 1161 whd in match assembly_1_pseudoinstruction; normalize nodelta … … 1923 1923 cases bitone #bit_one_seven_bits_refl normalize nodelta 1924 1924 [ @eq_bv_elim #seven_bits_refl normalize nodelta 1925  inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]1925  FUFFA inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry] 1926 1926 #lookup_from_internal_ram_refl ] 1927 @Some_Some_elim #Mrefl destruct(Mrefl)#fetch_many_assm %{1}1927 @Some_Some_elim #Mrefl <Mrefl M' #fetch_many_assm %{1} 1928 1928 whd in ⊢ (??%?); 1929 1929 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1930 whd in ⊢ (??%?); 1931 @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta 1932 @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl)) 1933 [1,3,5,7: 1934 @eq_f2 try % 1935 @(pose … (set_clock ????)) #status #status_refl 1936 @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl status_refl try % 1937 @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl % 1938 *: 1939 >EQs >EQticks <instr_refl 1940 @(write_at_stack_pointer_status_of_pseudo_status 〈low,high,accA〉) 1941 [2,4,6,8: @set_8051_sfr_status_of_pseudo_status try % 1942  >get_8051_sfr_set_8051_sfr 1943 cut (new_sp = (add … (get_8051_sfr … ps SFR_SP) (bitvector_of_nat … 1))) 1944 [ >(pair_destruct_2 ????? (sym_eq … carry_new_sp_refl)) 1945 change with (add ??? = ?); @eq_f2 try % 1946 cases daemon (*CSC: use @get_8051_sfr_status_of_pseudo_status*) ] #EQnew_sp 1947 >EQnew_sp 1948 @internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram 1949 1950 1951 XXX 1952 (*CSC: lemma here*) 1953 cases accA 1954 whd in match overwrite_or_delete_from_internal_ram; normalize nodelta 1955 [ whd whd in match delete_from_internal_ram; normalize nodelta 1956 @pair_elim #bit_one 1957  1958 ] 1959  1960  1961 ] 1930 whd in match execute_1_0; normalize nodelta 1931 whd in match execute_1_preinstruction; normalize nodelta 1932 >bit_one_seven_bits_refl 1933 [ alias id "write_at_stack_pointer_accA" = "cic:/matita/cerco/ASM/Test3/write_at_stack_pointer_accA.def(29)". 1934 >seven_bits_refl 1935 @(write_at_stack_pointer_status_of_pseudo_status_accA … 〈low,high,accA〉) 1936 [ @set_8051_sfr_status_of_pseudo_status >EQs >EQticks <instr_refl @(subaddressing_mode_elim … addr) #y 1937 try % 1938 change with (add ??? = ?); @eq_f2 try % 1939 @(pose … (set_clock ????)) #status #status_refl 1940 @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl % 1941  >EQs /demod nohyps/ >add_commutative % ] 1942  1943  1944  1962 1945 ] 1963 1946 43: (* POP *) 
src/ASM/Test.ma
r2281 r2282 2082 2082  #addr_entry @internal_pseudo_address_map_equal_up_to_address_insert_into_internal_ram ] 2083 2083 qed. 2084 2085 lemma write_at_stack_pointer_status_of_pseudo_status_accA: 2086 ∀M,cm,sigma,policy,ps,s,sp. 2087 let w ≝ bitvector_of_nat 8 224 in 2088 s=status_of_pseudo_status M cm ps sigma policy → 2089 sp=get_8051_sfr pseudo_assembly_program cm ps SFR_SP → 2090 write_at_stack_pointer … 2091 (code_memory_of_pseudo_assembly_program cm sigma policy) s 2092 (get_arg_8 … (code_memory_of_pseudo_assembly_program cm sigma policy) s false (DIRECT w)) 2093 =status_of_pseudo_status 2094 (overwrite_or_delete_from_internal_ram sp (\snd M) M) 2095 cm 2096 (write_at_stack_pointer pseudo_assembly_program cm ps 2097 (get_arg_8 pseudo_assembly_program cm ps false (DIRECT w))) 2098 sigma policy. 2099 try % 2100 ** #low #high #accA #cm #sigma #policy #ps #s #sp #EQs #EQsp >EQsp 2101 @(write_at_stack_pointer_status_of_pseudo_status … 〈low,high,accA〉) try assumption >EQs 2102 @internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram 2103 inversion accA [2:#entry] #EQaccA [2:%] whd in match map_value_using_opt_address_entry; normalize nodelta 2104 whd in ⊢ (??%?); whd in match status_of_pseudo_status; normalize nodelta 2105 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta cases entry * 2106 #addr normalize nodelta @pair_elim #h #l #_ normalize nodelta 2107 change with (get_index_v ??? 17 ? = ?) @get_index_v_set_index 2108 qed. 2109 2110 (*CSC: move elsewhere*) 2111 lemma eq_sfr_of_Byte_accA_to_eq: 2112 ∀w. sfr_of_Byte w = Some … (inl … SFR_ACC_A) → w = bitvector_of_nat 8 224. 2113 #w whd in match sfr_of_Byte; normalize nodelta 2114 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2115 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2116 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2117 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2118 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2119 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2120 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2121 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2122 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2123 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2124 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2125 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2126 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2127 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2128 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2129 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2130 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2131 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2132 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2133 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2134 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2135 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2136 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2137 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)] 2138 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta 2139 [ #EQB #_ <(eqb_true_to_eq … EQB) >bitvector_of_nat_inverse_nat_of_bitvector % ] #_ 2140 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ #abs destruct(abs) 2141 qed. 2142 2143 lemma write_at_stack_pointer_sfr_not_accA: 2144 ∀M,cm,sigma,policy,ps,s,sp,w. 2145 w ≠ bitvector_of_nat 7 224 → 2146 s=status_of_pseudo_status M cm ps sigma policy → 2147 sp=get_8051_sfr pseudo_assembly_program cm ps SFR_SP → 2148 write_at_stack_pointer … 2149 (code_memory_of_pseudo_assembly_program cm sigma policy) s 2150 (get_arg_8 … (code_memory_of_pseudo_assembly_program cm sigma policy) s false (DIRECT (true:::w))) 2151 =status_of_pseudo_status 2152 (delete_from_internal_ram sp M) 2153 cm 2154 (write_at_stack_pointer pseudo_assembly_program cm ps 2155 (get_arg_8 pseudo_assembly_program cm ps false (DIRECT (true:::w)))) 2156 sigma policy. 2157 try % 2158 ** #low #high #accA #cm #sigma #policy #ps #s #sp #w #NEQw #EQs #EQsp >EQsp 2159 @(write_at_stack_pointer_status_of_pseudo_status … 〈low,high,accA〉) try assumption >EQs 2160 @internal_pseudo_address_map_equal_up_to_address_delete_from_internal_ram 2161 whd in ⊢ (??%%); inversion (sfr_of_Byte ?) normalize nodelta 2162 [ cases not_implemented 2163  ** normalize nodelta #H 2164 try (@(get_8051_sfr_status_of_pseudo_status … (refl …)) %) 2165 try (@(get_8052_sfr_status_of_pseudo_status … (refl …)) %) 2166 @⊥ @(absurd ?? NEQw) lapply(eq_sfr_of_Byte_accA_to_eq … H) #K 2167 change with ([[true]]@@w=[[true]]@@bitvector_of_nat 7 224) in K; 2168 cases (bv_append_eq_to_eq … K) #_ #X @X 2169 qed.
Note: See TracChangeset
for help on using the changeset viewer.