Changeset 2276 for src/ASM/Test.ma
- Timestamp:
- Jul 30, 2012, 2:36:41 PM (9 years ago)
- File:
-
- 1 edited
-
src/ASM/Test.ma (modified) (47 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2274 r2276 7 7 lemma let_pair_in_status_of_pseudo_status: 8 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') → 9 c' = c → 10 (∀left, right. 11 s' left right c' = status_of_pseudo_status M cm (s left right c') sigma policy) → 11 12 (let 〈left, right〉 ≝ c' in s' left right c') = 12 13 status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy. … … 16 17 lemma let_pair_as_in_status_of_pseudo_status: 17 18 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'. 18 c = c'→19 (∀left, right, H, H'. s tatus_of_pseudo_status M cm (s left right H c) sigma policy = s' left right H' c') →19 c' = c → 20 (∀left, right, H, H'. s' left right H' c' = status_of_pseudo_status M cm (s left right H c) sigma policy) → 20 21 (let 〈left, right〉 as H' ≝ c' in s' left right H' c') = 21 22 status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy. … … 32 33 ∀t, t': bool. 33 34 t = t' → 34 s tatus_of_pseudo_status M cm s sigma policy = s'→35 s tatus_of_pseudo_status M cm s'' sigma policy = s'''→35 s' = status_of_pseudo_status M cm s sigma policy → 36 s''' = status_of_pseudo_status M cm s'' sigma policy → 36 37 if t then 37 38 s' … … 51 52 ∀new_ppc, new_ppc'. 52 53 sigma new_ppc = new_ppc' → 53 s tatus_of_pseudo_status M cm s sigma policy = s'→54 s' = status_of_pseudo_status M cm s sigma policy → 54 55 set_program_counter (BitVectorTrie Byte 16) 55 56 (code_memory_of_pseudo_assembly_program cm sigma policy) … … 57 58 status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy. 58 59 #M #cm #sigma #policy #s #s' #new_ppc #new_ppc' 59 #new_ppc_refl #s_refl <new_ppc_refl <s_refl //60 #new_ppc_refl #s_refl <new_ppc_refl >s_refl // 60 61 qed. 61 62 … … 67 68 ∀s,s'. 68 69 ∀v. 69 s tatus_of_pseudo_status M code_memory s sigma policy = s'→70 s' = status_of_pseudo_status M code_memory s sigma policy → 70 71 set_p1_latch (BitVectorTrie Byte 16) 71 72 (code_memory_of_pseudo_assembly_program code_memory sigma policy) … … 73 74 status_of_pseudo_status M code_memory 74 75 (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy. 75 #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //76 #M #cm #sigma #policy #s #s' #new_ppc #s_refl >s_refl // 76 77 qed. 77 78 … … 83 84 ∀s, s'. 84 85 ∀v. 85 s tatus_of_pseudo_status M code_memory s sigma policy = s'→86 s' = status_of_pseudo_status M code_memory s sigma policy → 86 87 set_p3_latch (BitVectorTrie Byte 16) 87 88 (code_memory_of_pseudo_assembly_program code_memory sigma policy) … … 89 90 status_of_pseudo_status M code_memory 90 91 (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy. 91 #M #code_memory #sigma #policy #s #s' #v #s_refl <s_refl // 92 qed. 93 94 definition map_acc_a_using_internal_pseudo_address_map: 95 ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝ 96 λM, sigma, v. 97 match \snd M with 98 [ None ⇒ v 99 | Some upper_lower_addr ⇒ 100 let 〈upper_lower, addr〉 ≝ upper_lower_addr in 101 if eq_upper_lower upper_lower upper then 102 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in 103 high 104 else 105 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in 106 low 107 ]. 108 109 (*CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... *) 110 definition map_internal_ram_address_using_pseudo_address_map: 111 ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝ 112 λM: internal_pseudo_address_map. 113 λsigma: Word → Word. 114 λaddress: Byte. 115 λvalue: Byte. 116 match lookup_from_internal_ram … address M with 117 [ None ⇒ value 118 | Some upper_lower_word ⇒ 119 let 〈upper_lower, word〉 ≝ upper_lower_word in 120 if eq_upper_lower upper_lower upper then 121 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in 122 high 123 else 124 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in 125 low 126 ]. 92 #M #code_memory #sigma #policy #s #s' #v #s_refl >s_refl // 93 qed. 127 94 128 95 definition map_address_using_internal_pseudo_address_map: … … 277 244 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 278 245 whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta 279 >sndM_refl normalize nodelta 246 >sndM_refl normalize nodelta whd in match map_value_using_opt_address_entry; normalize nodelta 280 247 >eq_upper_lower_refl normalize nodelta 281 248 [1: … … 331 298 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 332 299 whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta 333 >sndM_refl normalize nodelta >high_low_refl normalize nodelta 300 whd in match map_value_using_opt_address_entry; normalize nodelta 301 >sndM_refl normalize nodelta >high_low_refl normalize nodelta 334 302 >eq_upper_lower_refl normalize nodelta 335 303 whd in match (set_8051_sfr ?????); // … … 342 310 lemma set_8051_sfr_status_of_pseudo_status: 343 311 ∀M, code_memory, sigma, policy, s, s', sfr, v,v'. 344 s tatus_of_pseudo_status M code_memory s sigma policy = s'→312 s' = status_of_pseudo_status M code_memory s sigma policy → 345 313 map_address_using_internal_pseudo_address_map M sigma sfr v = v' → 346 314 set_8051_sfr ? (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v' = … … 348 316 (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy. 349 317 #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok 350 <s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/318 >s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/ 351 319 qed. 352 320 … … 374 342 lemma get_8051_sfr_status_of_pseudo_status: 375 343 ∀M, code_memory, sigma, policy, s, s', s'', sfr. 376 s tatus_of_pseudo_status M code_memory s sigma policy = s'→344 s' = status_of_pseudo_status M code_memory s sigma policy → 377 345 map_address_using_internal_pseudo_address_map M sigma sfr 378 346 (get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' → … … 380 348 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 381 349 s' sfr = s''. 382 #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' <s_refl <s_refl'350 #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' >s_refl <s_refl' 383 351 whd in match get_8051_sfr; normalize nodelta 384 352 @get_index_v_status_of_pseudo_status % … … 387 355 lemma get_8052_sfr_status_of_pseudo_status: 388 356 ∀M, code_memory, sigma, policy, s, s', sfr. 389 s tatus_of_pseudo_status M code_memory s sigma policy = s'→357 s' = status_of_pseudo_status M code_memory s sigma policy → 390 358 (get_8052_sfr (BitVectorTrie Byte 16) 391 359 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 392 360 s' sfr = 393 361 (get_8052_sfr pseudo_assembly_program code_memory s sfr)). 394 #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl //362 #M #code_memory #sigma #policy #s #s' #sfr #s_refl >s_refl // 395 363 qed. 396 364 397 365 lemma set_8052_sfr_status_of_pseudo_status: 398 366 ∀M, code_memory, sigma, policy, s, s', sfr, v. 399 s tatus_of_pseudo_status M code_memory s sigma policy = s'→367 s' = status_of_pseudo_status M code_memory s sigma policy → 400 368 (set_8052_sfr (BitVectorTrie Byte 16) 401 369 (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v = 402 370 status_of_pseudo_status M code_memory 403 371 (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy). 404 #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl <s_refl //372 #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl >s_refl // 405 373 qed. 406 374 … … 429 397 ∀s'. 430 398 ∀v'. 431 s tatus_of_pseudo_status M code_memory s sigma policy = s'→399 s' = status_of_pseudo_status M code_memory s sigma policy → 432 400 map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' → 433 401 (set_bit_addressable_sfr (BitVectorTrie Byte 16) … … 457 425 | _ ⇒ set_8051_sfr ?? s sfr v ] 458 426 | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]) 459 normalize nodelta #M #sigma #policy #s' #v' #s_refl <s_refl427 normalize nodelta #M #sigma #policy #s' #v' #s_refl >s_refl 460 428 /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/ 461 429 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta … … 466 434 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte. 467 435 ∀M. ∀sigma. ∀policy. ∀s': Status ?. ∀v'. 468 s tatus_of_pseudo_status M code_memory s sigma policy = s'→436 s' = status_of_pseudo_status M code_memory s sigma policy → 469 437 map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' → 470 438 (set_bit_addressable_sfr (BitVectorTrie Byte 16) … … 479 447 lemma set_low_internal_ram_status_of_pseudo_status: 480 448 ∀cm,sigma,policy,M,s,s',ram. 481 s tatus_of_pseudo_status M cm s sigma policy = s'→449 s' = status_of_pseudo_status M cm s sigma policy → 482 450 set_low_internal_ram (BitVectorTrie Byte 16) 483 451 (code_memory_of_pseudo_assembly_program cm sigma policy) … … 486 454 = status_of_pseudo_status M cm 487 455 (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy. 488 #cm #sigma #policy #M #s #s' #ram #s_refl <s_refl //456 #cm #sigma #policy #M #s #s' #ram #s_refl >s_refl // 489 457 qed. 490 458 … … 607 575 lemma set_register_status_of_pseudo_status: 608 576 ∀M,sigma,policy,cm,s,s',r,v,v'. 609 s tatus_of_pseudo_status M cm s sigma policy = s'→577 s' = status_of_pseudo_status M cm s sigma policy → 610 578 map_internal_ram_address_using_pseudo_address_map M sigma 611 579 (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' → … … 615 583 = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v) 616 584 sigma policy. 617 #M #sigma #policy #cm #s #s' #r #v #v' #s_refl <s_refl #v_ok585 #M #sigma #policy #cm #s #s' #r #v #v' #s_refl >s_refl #v_ok 618 586 whd in match set_register; normalize nodelta 619 587 >bit_address_of_register_status_of_pseudo_status … … 691 659 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]]. 692 660 ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀value'. 693 s tatus_of_pseudo_status M cm ps sigma policy = s'→661 s' = status_of_pseudo_status M cm ps sigma policy → 694 662 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → 695 663 map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' → … … 747 715 match other in False with [ ] 748 716 ] (subaddressing_modein … a)) normalize nodelta 749 #M #sigma #policy #s' #v' #s_refl <s_refl717 #M #sigma #policy #s' #v' #s_refl >s_refl 750 718 whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta 751 719 whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta … … 784 752 ∀M. ∀sigma. ∀policy. ∀s'. ∀value'. 785 753 addr = addr' → 786 s tatus_of_pseudo_status M cm ps sigma policy = s'→754 s' = status_of_pseudo_status M cm ps sigma policy → 787 755 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → 788 756 map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' → … … 804 772 ∀s: PreStatus … code_memory. 805 773 ∀s'. 806 (status_of_pseudo_status M code_memory s sigma policy) = s'→774 s' = status_of_pseudo_status M code_memory s sigma policy → 807 775 (p1_latch (BitVectorTrie Byte 16) 808 776 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 809 777 s' = 810 778 (p1_latch pseudo_assembly_program code_memory s)). 811 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //779 #M #sigma #policy #code_memory #s #s' #s_refl >s_refl // 812 780 qed. 813 781 … … 819 787 ∀s: PreStatus … code_memory. 820 788 ∀s'. 821 (status_of_pseudo_status M code_memory s sigma policy) = s'→789 s' = status_of_pseudo_status M code_memory s sigma policy → 822 790 (p3_latch (BitVectorTrie Byte 16) 823 791 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 824 792 (status_of_pseudo_status M code_memory s sigma policy) = 825 793 (p3_latch pseudo_assembly_program code_memory s)). 826 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //794 #M #sigma #policy #code_memory #s #s' #s_refl >s_refl // 827 795 qed. 828 796 … … 834 802 ∀l: bool. 835 803 Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'. 836 s tatus_of_pseudo_status M code_memory s sigma policy = s'→804 s' = status_of_pseudo_status M code_memory s sigma policy → 837 805 (get_bit_addressable_sfr (BitVectorTrie Byte 16) 838 806 (code_memory_of_pseudo_assembly_program code_memory sigma policy) … … 869 837 ] 870 838 ]) 871 #M #sigma #policy #s' #s_refl <s_refl normalize nodelta839 #M #sigma #policy #s' #s_refl >s_refl normalize nodelta 872 840 /2 by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/ 873 841 qed. … … 882 850 map_address_Byte_using_internal_pseudo_address_map M sigma 883 851 d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' → 884 (status_of_pseudo_status M code_memory s sigma policy) = s'→852 s' = status_of_pseudo_status M code_memory s sigma policy → 885 853 (get_bit_addressable_sfr (BitVectorTrie Byte 16) 886 854 (code_memory_of_pseudo_assembly_program code_memory sigma policy) … … 888 856 #code #s #d #v 889 857 cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant 890 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl <s_refl' @relevant %858 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl >s_refl' @relevant % 891 859 qed. 892 860 … … 898 866 ∀s''. 899 867 sigma (program_counter … s) = s'' → 900 (status_of_pseudo_status M code_memory s sigma policy) = s'→868 s' = status_of_pseudo_status M code_memory s sigma policy → 901 869 program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy) 902 870 s' = s''. 903 #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl <s_refl' //871 #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl >s_refl' // 904 872 qed. 905 873 906 874 lemma get_cy_flag_status_of_pseudo_status: 907 875 ∀M, cm, sigma, policy, s, s'. 908 (status_of_pseudo_status M cm s sigma policy) = s'→876 s' = status_of_pseudo_status M cm s sigma policy → 909 877 (get_cy_flag (BitVectorTrie Byte 16) 910 878 (code_memory_of_pseudo_assembly_program cm sigma policy) 911 879 s' = 912 880 get_cy_flag pseudo_assembly_program cm s). 913 #M #cm #sigma #policy #s #s' #s_refl <s_refl881 #M #cm #sigma #policy #s #s' #s_refl >s_refl 914 882 whd in match get_cy_flag; normalize nodelta 915 883 >(get_index_v_status_of_pseudo_status … (refl …)) % … … 922 890 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]]. 923 891 Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'. 924 (status_of_pseudo_status M cm ps sigma policy) = s'→892 s' = status_of_pseudo_status M cm ps sigma policy → 925 893 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → 926 894 get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) … … 972 940 match other in False with [ ] 973 941 ] (subaddressing_modein … a)) normalize nodelta 974 #M #sigma #policy #s' #s_refl <s_refl942 #M #sigma #policy #s' #s_refl >s_refl 975 943 whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta 976 944 whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta … … 1023 991 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]]. 1024 992 ∀M. ∀sigma. ∀policy. ∀s', s''. 1025 (status_of_pseudo_status M cm ps sigma policy) = s'→993 s' = status_of_pseudo_status M cm ps sigma policy → 1026 994 map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' → 1027 995 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → … … 1039 1007 ∀addr: [[data16]]. 1040 1008 ∀M. ∀sigma. ∀policy. ∀s'. 1041 s tatus_of_pseudo_status M cm ps sigma policy = s'→1009 s' = status_of_pseudo_status M cm ps sigma policy → 1042 1010 get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 1043 1011 s' addr = … … 1052 1020 ∀v,v': Word. 1053 1021 ∀M. ∀sigma. ∀policy. ∀s'. 1054 s tatus_of_pseudo_status M cm ps sigma policy = s'→1022 s' = status_of_pseudo_status M cm ps sigma policy → 1055 1023 v=v' → addr=addr' → 1056 1024 set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 1057 1025 s' v' addr' = 1058 1026 status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy. 1059 #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl <s_refl #addr_refl1027 #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl >s_refl #addr_refl 1060 1028 <addr_refl #v_refl <v_refl 1061 1029 @(subaddressing_mode_elim … addr) … … 1063 1031 whd in match set_arg_16'; normalize nodelta 1064 1032 @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta 1065 @set_8051_sfr_status_of_pseudo_status try % @sym_eq1033 @set_8051_sfr_status_of_pseudo_status try % 1066 1034 @set_8051_sfr_status_of_pseudo_status % 1067 1035 qed. … … 1106 1074 ∀l. 1107 1075 Σb: bool. ∀M. ∀sigma. ∀policy. ∀s'. 1108 s tatus_of_pseudo_status M cm ps sigma policy = s'→1076 s' = status_of_pseudo_status M cm ps sigma policy → 1109 1077 map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l → 1110 1078 get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) … … 1152 1120 ] (subaddressing_modein … a)) normalize nodelta 1153 1121 [4,5,8,9: //] 1154 #M #sigma #policy #s' #s_refl <s_refl1122 #M #sigma #policy #s' #s_refl >s_refl 1155 1123 [1: 1156 1124 #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) % … … 1175 1143 ∀M. ∀sigma. ∀policy. ∀s'. 1176 1144 addr = addr' → 1177 s tatus_of_pseudo_status M cm ps sigma policy = s'→1145 s' = status_of_pseudo_status M cm ps sigma policy → 1178 1146 map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l → 1179 1147 get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) … … 1345 1313 lemma clock_status_of_pseudo_status: 1346 1314 ∀M,cm,sigma,policy,s,s'. 1347 (status_of_pseudo_status M cm s sigma policy) = s'→1315 s' = status_of_pseudo_status M cm s sigma policy → 1348 1316 clock … 1349 1317 (code_memory_of_pseudo_assembly_program cm sigma policy) 1350 1318 s' 1351 1319 = clock … cm s. 1352 #M #cm #sigma #policy #s #s' #s_refl <s_refl //1320 #M #cm #sigma #policy #s #s' #s_refl >s_refl // 1353 1321 qed. 1354 1322 1355 1323 lemma set_clock_status_of_pseudo_status: 1356 1324 ∀M,cm,sigma,policy,s,s',v,v'. 1357 s tatus_of_pseudo_status M cm s sigma policy = s'→1325 s' = status_of_pseudo_status M cm s sigma policy → 1358 1326 v = v' → 1359 1327 set_clock … … … 1361 1329 s' v 1362 1330 = status_of_pseudo_status M cm (set_clock … cm s v') sigma policy. 1363 #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl // 1364 qed. 1365 1366 (*CSC: daemon 1331 #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl >s_refl <v_refl // 1332 qed. 1333 1367 1334 lemma set_flags_status_of_pseudo_status: 1368 1335 ∀M. … … 1378 1345 opt = opt' → 1379 1346 c = c' → 1380 s tatus_of_pseudo_status M code_memory s sigma policy = s'→1347 s' = status_of_pseudo_status M code_memory s sigma policy → 1381 1348 set_flags … s' b opt c = 1382 1349 status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy. 1383 #M #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c' 1384 #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl <s_refl 1385 whd in match status_of_pseudo_status; normalize nodelta 1386 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 1387 cases (\snd M) 1388 [1: 1389 normalize nodelta % 1390 |2: ** #address normalize nodelta 1391 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 1392 whd in ⊢ (??%%); cases opt try #opt' normalize nodelta 1393 @split_eq_status try % whd in match (sfr_8051_index ?); 1394 cases daemon 1395 ] 1396 qed.*) 1350 ** #low #high #accA #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c' 1351 #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl >s_refl 1352 whd in match set_flags; normalize nodelta 1353 @set_8051_sfr_status_of_pseudo_status try % 1354 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 1355 @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 1356 @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 1357 @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 1358 @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 1359 @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 1360 @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 1361 @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 1362 @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 1363 % 1364 qed. 1397 1365 1398 1366 lemma get_ac_flag_status_of_pseudo_status: … … 1403 1371 ∀s: PreStatus ? code_memory. 1404 1372 ∀s'. 1405 s tatus_of_pseudo_status M code_memory s sigma policy = s'→1373 s' = status_of_pseudo_status M code_memory s sigma policy → 1406 1374 get_ac_flag ?? s' = get_ac_flag ? code_memory s. 1407 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl1375 #M #sigma #policy #code_memory #s #s' #s_refl >s_refl 1408 1376 whd in match get_ac_flag; normalize nodelta 1409 1377 whd in match status_of_pseudo_status; normalize nodelta … … 1423 1391 ∀s: PreStatus ? code_memory. 1424 1392 ∀s'. 1425 s tatus_of_pseudo_status M code_memory s sigma policy = s'→1393 s' = status_of_pseudo_status M code_memory s sigma policy → 1426 1394 get_ov_flag ?? s' = get_ov_flag ? code_memory s. 1427 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl1395 #M #sigma #policy #code_memory #s #s' #s_refl >s_refl 1428 1396 whd in match get_ov_flag; normalize nodelta 1429 1397 whd in match status_of_pseudo_status; normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.
