Changeset 2204 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 Jul 18, 2012, 10:08:37 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2198 r2204 161 161 qed. 162 162 163 lemma set_flags_status_of_pseudo_status:164 ∀M.165 ∀sigma.166 ∀policy.167 ∀code_memory: pseudo_assembly_program.168 ∀s: PreStatus ? code_memory.169 ∀s'.170 ∀b, b': Bit.171 ∀opt, opt': option Bit.172 ∀c, c': Bit.173 b = b' →174 opt = opt' →175 c = c' →176 status_of_pseudo_status M code_memory s sigma policy = s' →177 set_flags … s' b opt c =178 status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy.179 #M #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'180 #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl <s_refl181 whd in match status_of_pseudo_status; normalize nodelta182 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta183 cases (\snd M)184 [1:185 normalize nodelta %186 2:187 * #address normalize nodelta188 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta189 whd in ⊢ (??%%); cases opt try #opt' normalize nodelta190 @split_eq_status try % whd in match (sfr_8051_index ?);191 cases daemon192 ]193 qed.194 195 lemma get_ac_flag_status_of_pseudo_status:196 ∀M: internal_pseudo_address_map.197 ∀sigma: Word → Word.198 ∀policy: Word → bool.199 ∀code_memory: pseudo_assembly_program.200 ∀s: PreStatus ? code_memory.201 ∀s'.202 status_of_pseudo_status M code_memory s sigma policy = s' →203 get_ac_flag ?? s' = get_ac_flag ? code_memory s.204 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl205 whd in match get_ac_flag; normalize nodelta206 whd in match status_of_pseudo_status; normalize nodelta207 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta208 cases (\snd M) try %209 * normalize nodelta #address210 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta211 whd in match sfr_8051_index; normalize nodelta212 >get_index_v_set_index_miss [2,4: /2/] %213 qed.214 215 lemma get_cy_flag_status_of_pseudo_status:216 ∀M: internal_pseudo_address_map.217 ∀sigma: Word → Word.218 ∀policy: Word → bool.219 ∀code_memory: pseudo_assembly_program.220 ∀s: PreStatus ? code_memory.221 ∀s'.222 status_of_pseudo_status M code_memory s sigma policy = s' →223 get_cy_flag ?? s' = get_cy_flag ? code_memory s.224 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl225 whd in match get_cy_flag; normalize nodelta226 whd in match status_of_pseudo_status; normalize nodelta227 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta228 cases (\snd M) try %229 * normalize nodelta #address230 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta231 whd in match sfr_8051_index; normalize nodelta232 >get_index_v_set_index_miss [2,4: /2/] %233 qed.234 235 lemma get_ov_flag_status_of_pseudo_status:236 ∀M: internal_pseudo_address_map.237 ∀sigma: Word → Word.238 ∀policy: Word → bool.239 ∀code_memory: pseudo_assembly_program.240 ∀s: PreStatus ? code_memory.241 ∀s'.242 status_of_pseudo_status M code_memory s sigma policy = s' →243 get_ov_flag ?? s' = get_ov_flag ? code_memory s.244 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl245 whd in match get_ov_flag; normalize nodelta246 whd in match status_of_pseudo_status; normalize nodelta247 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta248 cases (\snd M) try %249 * normalize nodelta #address250 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta251 whd in match sfr_8051_index; normalize nodelta252 >get_index_v_set_index_miss [2,4: /2/] %253 qed.254 255 lemma match_nat_status_of_pseudo_status:256 ∀M, cm, sigma, policy, s, s', s'', s'''.257 ∀n, n': nat.258 n = n' →259 status_of_pseudo_status M cm s' sigma policy = s →260 status_of_pseudo_status M cm s''' sigma policy = s'' →261 match n with [ O ⇒ s  S n' ⇒ s'' ] =262 status_of_pseudo_status M cm (match n' with [ O ⇒ s'  S n'' ⇒ s''']) sigma policy.263 #M #cm #sigma #policy #s #s' #s'' #s''' #n #n'264 #n_refl #s_refl #s_refl' <n_refl <s_refl <s_refl'265 cases n normalize nodelta try % #n' %266 qed.267 268 (* XXX: copied from Test.ma *)269 lemma let_pair_in_status_of_pseudo_status:270 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.271 c = c' →272 (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') →273 let 〈left, right〉 ≝ c' in (s' left right c') =274 status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.275 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta //276 qed.277 278 (* XXX: copied from Test.ma *)279 lemma let_pair_as_in_status_of_pseudo_status:280 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.281 c = c' →282 (∀left, right, H, H'. status_of_pseudo_status M cm (s left right H c) sigma policy = s' left right H' c') →283 let 〈left, right〉 as H' ≝ c' in (s' left right H' c') =284 status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy.285 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta #destruct_refl286 destruct(destruct_refl) /2/287 qed.288 289 163 lemma match_nat_replace: 290 164 ∀l, o, p, r, o', p': nat. … … 301 175 #l #l' #r #r' #l_refl #r_refl <l_refl <r_refl % 302 176 qed. 177 178 (* 179 lemma match_nat_status_of_pseudo_status: 180 ∀M, cm, sigma, policy, s, s', s'', s'''. 181 ∀n, n': nat. 182 n = n' → 183 status_of_pseudo_status M cm s' sigma policy = s → 184 status_of_pseudo_status M cm s''' sigma policy = s'' → 185 match n with [ O ⇒ s  S n' ⇒ s'' ] = 186 status_of_pseudo_status M cm (match n' with [ O ⇒ s'  S n'' ⇒ s''']) sigma policy. 187 #M #cm #sigma #policy #s #s' #s'' #s''' #n #n' 188 #n_refl #s_refl #s_refl' <n_refl <s_refl <s_refl' 189 cases n normalize nodelta try % #n' % 190 qed. 191 *) 303 192 304 193 lemma main_lemma_preinstruction: … … 773 662 whd in ⊢ (??%?); 774 663 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 664 change with (set_arg_8 ????? = ?) 665 @set_arg_8_status_of_pseudo_status try % 666 [ @sym_eq @set_clock_status_of_pseudo_status 667 [ @sym_eq @set_program_counter_status_of_pseudo_status 668 [ 669  670 ] 671  672 ] 673  674  @sym_eq 675 ] 676 cases daemon (* 775 677 whd in ⊢ (??%?); normalize nodelta 776 678 lapply addr_refl @(subaddressing_mode_elim … acc_a) #addr_refl normalize nodelta … … 836 738 ] 837 739 2: 838 ] 740 ]*)] 839 741 4,5,6,7,8,9: (* INC and DEC *) 840 742 cases daemon … … 904 806 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm >EQs >EQticks <instr_refl 905 807 whd in ⊢ (??%?); 808 @let_pair_in_status_of_pseudo_status 809 [1,3: 810 @eq_f3 811 [1,2,4,5: 812 @sym_eq 813 [ @(get_arg_8_status_of_pseudo_status) FOO 814 normalize nodelta >EQs >EQticks <instr_refl % 815 3: % 816 6: normalize nodelta 817 @eq_f @eq_f2 818 [1: >EQs % 819 2: >EQticks @eq_f2 <instr_refl try % >EQs % 820 ] 821 ] 822 823 824 906 825 @(pair_replace ?????????? p) 907 826 [2,4:
Note: See TracChangeset
for help on using the changeset viewer.