Changeset 2282 for src/ASM/Test.ma
- Timestamp:
- Jul 31, 2012, 6:08:00 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
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.