 Timestamp:
 Jul 18, 2012, 10:08:37 AM (7 years ago)
 Location:
 src/ASM
 Files:

 2 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: 
src/ASM/Test.ma
r2196 r2204 4 4 include alias "arithmetics/nat.ma". 5 5 include "ASM/AssemblyProof.ma". 6 7 lemma let_pair_in_status_of_pseudo_status: 8 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'. 9 c = c' → 10 (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') → 11 (let 〈left, right〉 ≝ c' in s' left right c') = 12 status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy. 13 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta // 14 qed. 15 16 lemma let_pair_as_in_status_of_pseudo_status: 17 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'. 18 c = c' → 19 (∀left, right, H, H'. status_of_pseudo_status M cm (s left right H c) sigma policy = s' left right H' c') → 20 (let 〈left, right〉 as H' ≝ c' in s' left right H' c') = 21 status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy. 22 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta #destruct_refl 23 destruct(destruct_refl) /2/ 24 qed. 25 26 lemma if_then_else_status_of_pseudo_status: 27 ∀M: internal_pseudo_address_map. 28 ∀cm: pseudo_assembly_program. 29 ∀sigma: Word → Word. 30 ∀policy: Word → bool. 31 ∀s, s', s'', s'''. 32 ∀t, t': bool. 33 t = t' → 34 status_of_pseudo_status M cm s sigma policy = s' → 35 status_of_pseudo_status M cm s'' sigma policy = s''' → 36 if t then 37 s' 38 else 39 s''' = 40 status_of_pseudo_status M cm (if t' then s else s'') sigma policy. 41 #M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl 42 >t_refl normalize nodelta >s_refl cases t' normalize nodelta // 43 qed. 6 44 7 45 lemma set_program_counter_status_of_pseudo_status: … … 20 58 #M #cm #sigma #policy #s #s' #new_ppc #new_ppc' 21 59 #new_ppc_refl #s_refl <new_ppc_refl <s_refl // 22 qed.23 24 lemma if_then_else_status_of_pseudo_status_true:25 ∀M: internal_pseudo_address_map.26 ∀cm: pseudo_assembly_program.27 ∀sigma: Word → Word.28 ∀policy: Word → bool.29 ∀s, s', s'', s'''.30 ∀t: bool.31 t = true →32 status_of_pseudo_status M cm s sigma policy = s' →33 if t then34 s'35 else36 s'' =37 status_of_pseudo_status M cm (if t then s else s''') sigma policy.38 #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl39 >t_refl normalize nodelta >s_refl %40 qed.41 42 lemma if_then_else_status_of_pseudo_status_false:43 ∀M: internal_pseudo_address_map.44 ∀cm: pseudo_assembly_program.45 ∀sigma: Word → Word.46 ∀policy: Word → bool.47 ∀s, s', s'', s'''.48 ∀t: bool.49 t = false →50 status_of_pseudo_status M cm s sigma policy = s' →51 if t then52 s''53 else54 s' =55 status_of_pseudo_status M cm (if t then s''' else s) sigma policy.56 #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl57 >t_refl normalize nodelta >s_refl %58 60 qed. 59 61 … … 1301 1303 qed. 1302 1304 1303 lemma let_pair_in_status_of_pseudo_status: 1304 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'. 1305 lemma set_flags_status_of_pseudo_status: 1306 ∀M. 1307 ∀sigma. 1308 ∀policy. 1309 ∀code_memory: pseudo_assembly_program. 1310 ∀s: PreStatus ? code_memory. 1311 ∀s'. 1312 ∀b, b': Bit. 1313 ∀opt, opt': option Bit. 1314 ∀c, c': Bit. 1315 b = b' → 1316 opt = opt' → 1305 1317 c = c' → 1306 (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') → 1307 let 〈left, right〉 ≝ c' in s' left right c' = 1308 status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy. 1309 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta // 1310 qed. 1311 1312 lemma let_pair_as_in_status_of_pseudo_status: 1313 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'. 1314 ∀c_refl: c = c'. 1315 (∀left, right, H. status_of_pseudo_status M cm (s left right H c') sigma policy = s' left right H c) → 1316 let 〈left, right〉 as H ≝ c' in s' left right H c = 1317 status_of_pseudo_status M cm (let 〈left, right〉 as H' ≝ c in s left right ? c) sigma policy. 1318 [2: >H' assumption ] 1319 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' 1320 #destruct_assm destruct(destruct_assm) normalize nodelta 1321 #status_of_pseudo_status_assm >status_of_pseudo_status_assm // 1322 qed. 1323 1324 lemma if_then_else_status_of_pseudo_status: 1318 status_of_pseudo_status M code_memory s sigma policy = s' → 1319 set_flags … s' b opt c = 1320 status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy. 1321 #M #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c' 1322 #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl <s_refl 1323 whd in match status_of_pseudo_status; normalize nodelta 1324 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 1325 cases (\snd M) 1326 [1: 1327 normalize nodelta % 1328 2: 1329 * #address normalize nodelta 1330 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 1331 whd in ⊢ (??%%); cases opt try #opt' normalize nodelta 1332 @split_eq_status try % whd in match (sfr_8051_index ?); 1333 cases daemon 1334 ] 1335 qed. 1336 1337 lemma get_ac_flag_status_of_pseudo_status: 1325 1338 ∀M: internal_pseudo_address_map. 1326 ∀cm: pseudo_assembly_program.1327 1339 ∀sigma: Word → Word. 1328 1340 ∀policy: Word → bool. 1329 ∀s, s', s'', s'''. 1330 ∀t, t': bool. 1331 t = t' → 1332 status_of_pseudo_status M cm s sigma policy = s' → 1333 status_of_pseudo_status M cm s'' sigma policy = s''' → 1334 if t then 1335 s' 1336 else 1337 s''' = 1338 status_of_pseudo_status M cm (if t' then s else s'') sigma policy. 1339 #M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl 1340 >t_refl normalize nodelta >s_refl cases t' normalize nodelta // 1341 qed. 1341 ∀code_memory: pseudo_assembly_program. 1342 ∀s: PreStatus ? code_memory. 1343 ∀s'. 1344 status_of_pseudo_status M code_memory s sigma policy = s' → 1345 get_ac_flag ?? s' = get_ac_flag ? code_memory s. 1346 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl 1347 whd in match get_ac_flag; normalize nodelta 1348 whd in match status_of_pseudo_status; normalize nodelta 1349 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 1350 cases (\snd M) try % 1351 * normalize nodelta #address 1352 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 1353 whd in match sfr_8051_index; normalize nodelta 1354 >get_index_v_set_index_miss [2,4: /2/] % 1355 qed. 1356 1357 lemma get_cy_flag_status_of_pseudo_status: 1358 ∀M: internal_pseudo_address_map. 1359 ∀sigma: Word → Word. 1360 ∀policy: Word → bool. 1361 ∀code_memory: pseudo_assembly_program. 1362 ∀s: PreStatus ? code_memory. 1363 ∀s'. 1364 status_of_pseudo_status M code_memory s sigma policy = s' → 1365 get_cy_flag ?? s' = get_cy_flag ? code_memory s. 1366 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl 1367 whd in match get_cy_flag; normalize nodelta 1368 whd in match status_of_pseudo_status; normalize nodelta 1369 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 1370 cases (\snd M) try % 1371 * normalize nodelta #address 1372 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 1373 whd in match sfr_8051_index; normalize nodelta 1374 >get_index_v_set_index_miss [2,4: /2/] % 1375 qed. 1376 1377 lemma get_ov_flag_status_of_pseudo_status: 1378 ∀M: internal_pseudo_address_map. 1379 ∀sigma: Word → Word. 1380 ∀policy: Word → bool. 1381 ∀code_memory: pseudo_assembly_program. 1382 ∀s: PreStatus ? code_memory. 1383 ∀s'. 1384 status_of_pseudo_status M code_memory s sigma policy = s' → 1385 get_ov_flag ?? s' = get_ov_flag ? code_memory s. 1386 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl 1387 whd in match get_ov_flag; normalize nodelta 1388 whd in match status_of_pseudo_status; normalize nodelta 1389 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 1390 cases (\snd M) try % 1391 * normalize nodelta #address 1392 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 1393 whd in match sfr_8051_index; normalize nodelta 1394 >get_index_v_set_index_miss [2,4: /2/] % 1395 qed.
Note: See TracChangeset
for help on using the changeset viewer.