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

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.