- Timestamp:
- Jul 10, 2012, 11:54:54 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2168 r2171 151 151 normalize @eq_f @inductive_hypothesis @nmk #relevant 152 152 >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) % 153 ] 154 ] 155 qed. 156 157 (* XXX: move elsewhere *) 158 lemma get_index_v_set_index_miss: 159 ∀a: Type[0]. 160 ∀n: nat. 161 ∀v: Vector a n. 162 ∀i, j: nat. 163 ∀e: a. 164 ∀i_proof: i < n. 165 ∀j_proof: j < n. 166 i ≠ j → 167 get_index_v a n (set_index a n v i e i_proof) j j_proof = 168 get_index_v a n v j j_proof. 169 #a #n #v elim v 170 [1: 171 #i #j #e #i_proof 172 cases (lt_to_not_zero … i_proof) 173 |2: 174 #n' #hd #tl #inductive_hypothesis #i #j 175 cases i cases j 176 [1: 177 #e #i_proof #j_proof #neq_assm 178 cases (absurd ? (refl … 0) neq_assm) 179 |2,3: 180 #i' #e #i_proof #j_proof #_ % 181 |4: 182 #i' #j' #e #i_proof #j_proof #neq_assm 183 @inductive_hypothesis @nmk #eq_assm 184 >eq_assm in neq_assm; #neq_assm 185 cases (absurd ? (refl ??) neq_assm) 153 186 ] 154 187 ] … … 202 235 qed. 203 236 237 lemma get_index_v_status_of_pseudo_status: 238 ∀M, code_memory, sigma, policy, s, sfr. 239 (get_index_v Byte 19 240 (special_function_registers_8051 (BitVectorTrie Byte 16) 241 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 242 (status_of_pseudo_status M code_memory s sigma policy)) 243 (sfr_8051_index sfr) (sfr8051_index_19 sfr) = 244 map_address_using_internal_pseudo_address_map M sigma sfr 245 (get_index_v Byte 19 246 (special_function_registers_8051 pseudo_assembly_program code_memory s) 247 (sfr_8051_index sfr) (sfr8051_index_19 sfr))). 248 #M #code_memory #sigma #policy #s #sfr 249 whd in match status_of_pseudo_status; normalize nodelta 250 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 251 inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta 252 [1: 253 cases sfr 254 [18: 255 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 256 whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta 257 >sndM_refl % 258 ] 259 % 260 |2: 261 @pair_elim #high #low #high_low_refl normalize nodelta 262 inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta 263 cases sfr 264 [18,37: 265 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 266 whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta 267 >sndM_refl normalize nodelta >high_low_refl normalize nodelta 268 >eq_upper_lower_refl normalize nodelta 269 whd in match (set_8051_sfr ?????); // 270 ] 271 @get_index_v_set_index_miss whd in ⊢ (?(??%%)); 272 @nmk #absurd destruct(absurd) 273 ] 274 qed. 275 204 276 lemma set_8051_sfr_status_of_pseudo_status: 205 277 ∀M, code_memory, sigma, policy, s, sfr, v,v'. … … 212 284 #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok 213 285 whd in ⊢ (??%%); @split_eq_status try % /2/ 286 qed. 287 288 lemma get_8051_sfr_status_of_pseudo_status: 289 ∀M, code_memory, sigma, policy, s, sfr. 290 (get_8051_sfr (BitVectorTrie Byte 16) 291 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 292 (status_of_pseudo_status M code_memory s sigma policy) sfr = 293 map_address_using_internal_pseudo_address_map M sigma sfr 294 (get_8051_sfr pseudo_assembly_program code_memory s sfr)). 295 #M #code_memory #sigma #policy #s #sfr 296 whd in match get_8051_sfr; normalize nodelta 297 @get_index_v_status_of_pseudo_status 298 qed. 299 300 lemma get_8052_sfr_status_of_pseudo_status: 301 ∀M, code_memory, sigma, policy, s, sfr. 302 (get_8052_sfr (BitVectorTrie Byte 16) 303 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 304 (status_of_pseudo_status M code_memory s sigma policy) sfr = 305 (get_8052_sfr pseudo_assembly_program code_memory s sfr)). 306 // 214 307 qed. 215 308 … … 394 487 qed. 395 488 396 (*CSC: Taken from AssemblyProofSplit *)397 lemma get_index_v_set_index_miss:398 ∀T: Type[0].399 ∀n, i, j: nat.400 ∀v: Vector T n.401 ∀b: T.402 ∀i_proof: i < n.403 ∀j_proof: j < n.404 i ≠ j →405 get_index_v T n (set_index T n v i b i_proof) j j_proof =406 get_index_v T n v j j_proof.407 #T #n #i #j #v lapply i lapply j elim v #i #j408 [1:409 #b #i_proof410 cases (lt_to_not_zero … i_proof)411 |2:412 #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j413 lapply i_proof lapply i_neq_j cases i'414 [1:415 -i_neq_j #i_neq_j -i_proof #i_proof416 whd in match (set_index ??????);417 lapply j_proof lapply i_neq_j cases j'418 [1:419 #relevant @⊥ cases relevant -relevant #absurd @absurd %420 |2:421 #j' #_ -j_proof #j_proof %422 ]423 |2:424 #i' -i_neq_j #i_neq_j -i_proof #i_proof425 lapply j_proof lapply i_neq_j cases j'426 [1:427 #_ #j_proof %428 |2:429 #j' #i_neq_j #j_proof430 @inductive_hypothesis @nmk #relevant431 cases i_neq_j #absurd @absurd >relevant %432 ]433 ]434 ]435 qed.436 437 lemma get_8051_sfr_status_of_pseudo_status:438 ∀M,cm,s,sigma,policy,sfr.439 get_8051_sfr …440 (code_memory_of_pseudo_assembly_program cm sigma policy)441 (status_of_pseudo_status M cm s sigma policy) sfr =442 map_address_using_internal_pseudo_address_map M sigma sfr443 (get_8051_sfr … cm s sfr).444 #M #cm #s #sigma #policy #sfr whd in ⊢ (??%%);445 whd in match status_of_pseudo_status; normalize nodelta446 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta447 whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta448 cases (\snd M) normalize nodelta [cases sfr %]449 #map_mem #map_acc @pair_elim #high #low #_ normalize nodelta450 cases (eq_upper_lower ??) normalize nodelta cases sfr normalize nodelta451 [18,37: @get_index_v_set_index452 |*: >get_index_v_set_index_miss % normalize #abs destruct]453 qed.454 455 489 lemma bit_address_of_register_status_of_pseudo_status: 456 490 ∀M,cm,s,sigma,policy,r. … … 476 510 (lookup Byte 7 addr 477 511 (low_internal_ram pseudo_assembly_program cm s) (zero 8)). 512 513 (*CSC: provable using the axiom in AssemblyProof, but this one seems more 514 primitive *) 515 axiom lookup_high_internal_ram_of_pseudo_high_internal_ram: 516 ∀M,sigma,cm,s,addr. 517 lookup Byte 7 addr 518 (high_internal_ram_of_pseudo_high_internal_ram M 519 (high_internal_ram pseudo_assembly_program cm s)) (zero 8) 520 = 521 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) 522 (lookup Byte 7 addr 523 (high_internal_ram pseudo_assembly_program cm s) (zero 8)). 478 524 479 525 lemma get_register_status_of_pseudo_status: … … 526 572 527 573 definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝ 528 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λ addr.574 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr. 529 575 match addr with 530 576 [ INDIRECT i ⇒ … … 534 580 assoc_list_lookup ?? 535 581 (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None … 582 | ACC_DPTR ⇒ 583 (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer 584 in the ACC_A *) 585 map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) = 586 get_8051_sfr … cm s SFR_ACC_A 587 | ACC_PC ⇒ 588 (* XXX: as above *) 589 map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) = 590 get_8051_sfr … cm s SFR_ACC_A ∧ sigma (program_counter … s) = program_counter … s 536 591 | _ ⇒ True ]. 537 592 … … 633 688 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]]. 634 689 ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'. 635 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps addr →690 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → 636 691 map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' → 637 692 set_arg_8 (BitVectorTrie Byte 16) … … 712 767 >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] 713 768 qed. 769 770 definition get_bit_addressable_sfr: 771 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝ 772 λM: Type[0]. 773 λcode_memory:M. 774 λs: PreStatus M code_memory. 775 λb: Byte. 776 λl: bool. 777 match sfr_of_Byte b with 778 [ None ⇒ match not_implemented in False with [ ] 779 | Some sfr8051_8052 ⇒ 780 match sfr8051_8052 with 781 [ inl sfr ⇒ 782 match sfr with 783 [ SFR_P1 ⇒ 784 if l then 785 p1_latch … s 786 else 787 get_8051_sfr … s SFR_P1 788 | SFR_P3 ⇒ 789 if l then 790 p3_latch … s 791 else 792 get_8051_sfr … s SFR_P3 793 | _ ⇒ get_8051_sfr … s sfr 794 ] 795 | inr sfr ⇒ get_8052_sfr M code_memory s sfr 796 ] 797 ]. 798 799 definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ; 800 acc_a ; acc_b ; data ; acc_dptr ; 801 acc_pc ; ext_indirect ; 802 ext_indirect_dptr ]] → Byte ≝ 803 λm, cm, s, l, a. 804 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 805 acc_a ; acc_b ; data ; acc_dptr ; 806 acc_pc ; ext_indirect ; 807 ext_indirect_dptr ]] x) → ? with 808 [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A 809 | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B 810 | DATA d ⇒ λdata: True. d 811 | REGISTER r ⇒ λregister: True. get_register ?? s r 812 | EXT_INDIRECT_DPTR ⇒ 813 λext_indirect_dptr: True. 814 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 815 lookup ? 16 address (external_ram ?? s) (zero 8) 816 | EXT_INDIRECT e ⇒ 817 λext_indirect: True. 818 let address ≝ get_register ?? s [[ false; false; e ]] in 819 let padded_address ≝ pad 8 8 address in 820 lookup ? 16 padded_address (external_ram ?? s) (zero 8) 821 | ACC_DPTR ⇒ 822 λacc_dptr: True. 823 let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 824 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in 825 let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in 826 lookup ? 16 address (external_ram ?? s) (zero 8) 827 | ACC_PC ⇒ 828 λacc_pc: True. 829 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in 830 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in 831 lookup ? 16 address (external_ram ?? s) (zero 8) 832 | DIRECT d ⇒ 833 λdirect: True. 834 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in 835 match head' … hd with 836 [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l 837 | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) 838 ] 839 | INDIRECT i ⇒ 840 λindirect: True. 841 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in 842 match head' … hd with 843 [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …) 844 | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) 845 ] 846 | _ ⇒ λother. 847 match other in False with [ ] 848 ] (subaddressing_modein … a). 849 850 lemma p1_latch_status_of_pseudo_status: 851 ∀M. 852 ∀code_memory: pseudo_assembly_program. 853 ∀s: PreStatus … code_memory. 854 ∀sigma. 855 ∀policy. 856 (p1_latch (BitVectorTrie Byte 16) 857 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 858 (status_of_pseudo_status M code_memory s sigma policy) = 859 (p1_latch pseudo_assembly_program code_memory s)). 860 // 861 qed. 862 863 lemma p3_latch_status_of_pseudo_status: 864 ∀M. 865 ∀code_memory: pseudo_assembly_program. 866 ∀s: PreStatus … code_memory. 867 ∀sigma. 868 ∀policy. 869 (p3_latch (BitVectorTrie Byte 16) 870 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 871 (status_of_pseudo_status M code_memory s sigma policy) = 872 (p3_latch pseudo_assembly_program code_memory s)). 873 // 874 qed. 875 876 lemma get_bit_addressable_sfr_status_of_pseudo_status': 877 let M ≝ pseudo_assembly_program in 878 ∀code_memory: M. 879 ∀s: PreStatus M code_memory. 880 ∀d: Byte. 881 ∀l: bool. 882 Σp: Byte. ∀M. ∀sigma. ∀policy. 883 (get_bit_addressable_sfr (BitVectorTrie Byte 16) 884 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 885 (status_of_pseudo_status M code_memory s sigma policy) d l = 886 map_address_Byte_using_internal_pseudo_address_map M sigma 887 d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)). 888 whd in match get_bit_addressable_sfr; 889 whd in match map_address_Byte_using_internal_pseudo_address_map; 890 normalize nodelta 891 @(let M ≝ pseudo_assembly_program in 892 λcode_memory:M. 893 λs: PreStatus M code_memory. 894 λb: Byte. 895 λl: bool. 896 match sfr_of_Byte b with 897 [ None ⇒ match not_implemented in False with [ ] 898 | Some sfr8051_8052 ⇒ 899 match sfr8051_8052 with 900 [ inl sfr ⇒ 901 match sfr with 902 [ SFR_P1 ⇒ 903 if l then 904 p1_latch … s 905 else 906 get_8051_sfr … s SFR_P1 907 | SFR_P3 ⇒ 908 if l then 909 p3_latch … s 910 else 911 get_8051_sfr … s SFR_P3 912 | _ ⇒ get_8051_sfr … s sfr 913 ] 914 | inr sfr ⇒ get_8052_sfr M code_memory s sfr 915 ] 916 ]) 917 #M #sigma #policy normalize nodelta 918 /by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/ 919 qed. 920 921 lemma get_bit_addressable_sfr_status_of_pseudo_status: 922 let M ≝ pseudo_assembly_program in 923 ∀code_memory: M. 924 ∀s: PreStatus M code_memory. 925 ∀d: Byte. 926 ∀l: bool. 927 ∀M. ∀sigma. ∀policy. 928 (get_bit_addressable_sfr (BitVectorTrie Byte 16) 929 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 930 (status_of_pseudo_status M code_memory s sigma policy) d l = 931 map_address_Byte_using_internal_pseudo_address_map M sigma 932 d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)). 933 #code #s #d #v cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ 934 #H @H 935 qed. 936 937 lemma program_counter_status_of_pseudo_status: 938 ∀code_memory: pseudo_assembly_program. 939 ∀s: PreStatus ? code_memory. 940 ∀M. ∀sigma. ∀policy. 941 program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy) 942 (status_of_pseudo_status M code_memory s sigma policy) = 943 sigma (program_counter … s). 944 // 945 qed. 946 947 lemma get_cy_flag_status_of_pseudo_status: 948 ∀M, cm, sigma, policy, s. 949 (get_cy_flag (BitVectorTrie Byte 16) 950 (code_memory_of_pseudo_assembly_program cm sigma policy) 951 (status_of_pseudo_status M cm s sigma policy) = 952 get_cy_flag pseudo_assembly_program cm s). 953 #M #cm #sigma #policy #s 954 whd in match get_cy_flag; normalize nodelta 955 >get_index_v_status_of_pseudo_status % 956 qed. 957 958 lemma get_arg_8_status_of_pseudo_status: 959 ∀cm. 960 ∀ps. 961 ∀l. 962 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]]. 963 Σp: Byte. ∀M. ∀sigma. ∀policy. 964 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → 965 get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 966 (status_of_pseudo_status M cm ps sigma policy) l addr = 967 map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr). 968 whd in match get_arg_8; normalize nodelta 969 @(let m ≝ pseudo_assembly_program in 970 λcm: m. λs: PreStatus m cm. λl: bool. λa: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr]]. 971 match a return λx. bool_to_Prop (is_in ? [[ direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr ]] x) → Σp. ? with 972 [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A 973 | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B 974 | DATA d ⇒ λdata: True. d 975 | REGISTER r ⇒ λregister: True. get_register ?? s r 976 | EXT_INDIRECT_DPTR ⇒ 977 λext_indirect_dptr: True. 978 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 979 lookup ? 16 address (external_ram ?? s) (zero 8) 980 | EXT_INDIRECT e ⇒ 981 λext_indirect: True. 982 let address ≝ get_register ?? s [[ false; false; e ]] in 983 let padded_address ≝ pad 8 8 address in 984 lookup ? 16 padded_address (external_ram ?? s) (zero 8) 985 | ACC_DPTR ⇒ 986 λacc_dptr: True. 987 let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 988 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in 989 let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in 990 lookup ? 16 address (external_ram ?? s) (zero 8) 991 | ACC_PC ⇒ 992 λacc_pc: True. 993 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in 994 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in 995 lookup ? 16 address (external_ram ?? s) (zero 8) 996 | DIRECT d ⇒ 997 λdirect: True. 998 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in 999 match head' … hd with 1000 [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l 1001 | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) 1002 ] 1003 | INDIRECT i ⇒ 1004 λindirect: True. 1005 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in 1006 match head' … hd with 1007 [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …) 1008 | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) 1009 ] 1010 | _ ⇒ λother: False. 1011 match other in False with [ ] 1012 ] (subaddressing_modein … a)) normalize nodelta 1013 #M #sigma #policy 1014 whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta 1015 whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta 1016 [1: 1017 #_ >p normalize nodelta >p1 normalize nodelta 1018 @get_bit_addressable_sfr_status_of_pseudo_status 1019 |2: 1020 #_>p normalize nodelta >p1 normalize nodelta 1021 @lookup_low_internal_ram_of_pseudo_low_internal_ram 1022 |3,4: 1023 #assoc_list_assm >get_register_status_of_pseudo_status 1024 whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta 1025 >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta 1026 [1: 1027 >(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma) 1028 |2: 1029 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) 1030 ] 1031 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % 1032 |5: 1033 #assoc_list_assm >get_register_status_of_pseudo_status 1034 whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta 1035 >assoc_list_assm normalize nodelta % 1036 |6,7,8,9: 1037 #_ /2/ 1038 |10: 1039 #acc_a_assm >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status 1040 >get_8051_sfr_status_of_pseudo_status 1041 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 1042 >acc_a_assm >p normalize nodelta // 1043 |11: 1044 * #map_acc_a_assm #sigma_assm >get_8051_sfr_status_of_pseudo_status >program_counter_status_of_pseudo_status 1045 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 1046 >sigma_assm >map_acc_a_assm >p normalize nodelta // 1047 |12: 1048 #_ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status 1049 >external_ram_status_of_pseudo_status // 1050 ] 1051 qed. 1052 1053 lemma get_arg_16_status_of_pseudo_status: 1054 ∀cm. 1055 ∀ps. 1056 ∀addr: [[data16]]. 1057 ∀M. ∀sigma. ∀policy. 1058 get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 1059 (status_of_pseudo_status M cm ps sigma policy) addr = 1060 (get_arg_16 … cm ps addr). 1061 // 1062 qed. 1063 1064 lemma set_arg_16_status_of_pseudo_status: 1065 ∀cm. 1066 ∀ps. 1067 ∀addr: [[dptr]]. 1068 ∀v: Word. 1069 ∀M. ∀sigma. ∀policy. 1070 set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 1071 (status_of_pseudo_status M cm ps sigma policy) v addr = 1072 status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy. 1073 #cm #ps #addr #v #M #sigma #policy 1074 @(subaddressing_mode_elim … addr) 1075 whd in match set_arg_16; normalize nodelta 1076 whd in match set_arg_16'; normalize nodelta 1077 @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta 1078 >(set_8051_sfr_status_of_pseudo_status … bu) 1079 [1: >(set_8051_sfr_status_of_pseudo_status … bl) ] 1080 // 1081 qed. 1082 1083 definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] → 1084 bool → bool ≝ 1085 λm, cm, s, a, l. 1086 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; 1087 n_bit_addr ; 1088 carry ]] x) → ? with 1089 [ BIT_ADDR b ⇒ 1090 λbit_addr: True. 1091 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in 1092 match head' … bit_1 with 1093 [ true ⇒ 1094 let address ≝ nat_of_bitvector … seven_bits in 1095 let d ≝ address ÷ 8 in 1096 let m ≝ address mod 8 in 1097 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1098 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 1099 get_index_v … sfr m ? 1100 | false ⇒ 1101 let address ≝ nat_of_bitvector … seven_bits in 1102 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1103 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1104 get_index_v … t (modulus address 8) ? 1105 ] 1106 | N_BIT_ADDR n ⇒ 1107 λn_bit_addr: True. 1108 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in 1109 match head' … bit_1 with 1110 [ true ⇒ 1111 let address ≝ nat_of_bitvector … seven_bits in 1112 let d ≝ address ÷ 8 in 1113 let m ≝ address mod 8 in 1114 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1115 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 1116 ¬(get_index_v … sfr m ?) 1117 | false ⇒ 1118 let address ≝ nat_of_bitvector … seven_bits in 1119 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1120 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1121 ¬(get_index_v … t (modulus address 8) ?) 1122 ] 1123 | CARRY ⇒ λcarry: True. get_cy_flag ?? s 1124 | _ ⇒ λother. 1125 match other in False with [ ] 1126 ] (subaddressing_modein … a). 1127 @modulus_less_than 1128 qed. 1129 1130 definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝ 1131 λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl. 1132 match addr with 1133 [ BIT_ADDR b ⇒ 1134 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in 1135 match head' … bit_1 with 1136 [ true ⇒ 1137 let address ≝ nat_of_bitvector … seven_bits in 1138 let d ≝ address ÷ 8 in 1139 let m ≝ address mod 8 in 1140 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1141 map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l 1142 | false ⇒ 1143 let address ≝ nat_of_bitvector … seven_bits in 1144 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1145 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1146 map_internal_ram_address_using_pseudo_address_map M sigma 1147 (false:::address') t = t 1148 ] 1149 | N_BIT_ADDR b ⇒ 1150 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in 1151 match head' … bit_1 with 1152 [ true ⇒ 1153 let address ≝ nat_of_bitvector … seven_bits in 1154 let d ≝ address ÷ 8 in 1155 let m ≝ address mod 8 in 1156 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1157 map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l 1158 | false ⇒ 1159 let address ≝ nat_of_bitvector … seven_bits in 1160 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1161 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1162 map_internal_ram_address_using_pseudo_address_map M sigma 1163 (false:::address') t = t 1164 ] 1165 | _ ⇒ True ]. 1166 1167 lemma get_arg_1_status_of_pseudo_status': 1168 ∀cm. 1169 ∀ps. 1170 ∀addr: [[bit_addr; n_bit_addr; carry]]. 1171 ∀l. 1172 Σb: bool. ∀M. ∀sigma. ∀policy. 1173 map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l → 1174 get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 1175 (status_of_pseudo_status M cm ps sigma policy) addr l = 1176 (get_arg_1 … cm ps addr l). 1177 whd in match get_arg_1; normalize nodelta 1178 @(let m ≝ pseudo_assembly_program in 1179 λcm: m. λs: PseudoStatus cm. λa:[[bit_addr; n_bit_addr; carry]]. λl. 1180 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; 1181 n_bit_addr ; 1182 carry ]] x) → Σb: bool. ? with 1183 [ BIT_ADDR b ⇒ 1184 λbit_addr: True. 1185 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in 1186 match head' … bit_1 with 1187 [ true ⇒ 1188 let address ≝ nat_of_bitvector … seven_bits in 1189 let d ≝ address ÷ 8 in 1190 let m ≝ address mod 8 in 1191 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1192 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 1193 get_index_v … sfr m ? 1194 | false ⇒ 1195 let address ≝ nat_of_bitvector … seven_bits in 1196 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1197 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1198 get_index_v … t (modulus address 8) ? 1199 ] 1200 | N_BIT_ADDR n ⇒ 1201 λn_bit_addr: True. 1202 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in 1203 match head' … bit_1 with 1204 [ true ⇒ 1205 let address ≝ nat_of_bitvector … seven_bits in 1206 let d ≝ address ÷ 8 in 1207 let m ≝ address mod 8 in 1208 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1209 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 1210 ¬(get_index_v … sfr m ?) 1211 | false ⇒ 1212 let address ≝ nat_of_bitvector … seven_bits in 1213 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1214 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1215 ¬(get_index_v … t (modulus address 8) ?) 1216 ] 1217 | CARRY ⇒ λcarry: True. get_cy_flag ?? s 1218 | _ ⇒ λother. 1219 match other in False with [ ] 1220 ] (subaddressing_modein … a)) normalize nodelta 1221 try @modulus_less_than 1222 #M #sigma #policy 1223 [1: 1224 #_ @get_cy_flag_status_of_pseudo_status 1225 |2,4: 1226 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta 1227 >get_bit_addressable_sfr_status_of_pseudo_status #map_address_assm 1228 >map_address_assm % 1229 |3,5: 1230 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta 1231 whd in match status_of_pseudo_status; normalize nodelta 1232 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) 1233 #map_address_assm >map_address_assm % 1234 ] 1235 qed. 1236 1237 lemma get_arg_1_status_of_pseudo_status: 1238 ∀cm. 1239 ∀ps. 1240 ∀addr: [[bit_addr; n_bit_addr; carry]]. 1241 ∀l. 1242 ∀M. ∀sigma. ∀policy. 1243 map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l → 1244 get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 1245 (status_of_pseudo_status M cm ps sigma policy) addr l = 1246 (get_arg_1 … cm ps addr l). 1247 #cm #ps #addr #l 1248 cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm 1249 @assm 1250 qed. 1251 1252 definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝ 1253 λm: Type[0]. 1254 λcm. 1255 λs: PreStatus m cm. 1256 λa: [[bit_addr; carry]]. 1257 λv: Bit. 1258 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with 1259 [ BIT_ADDR b ⇒ λbit_addr: True. 1260 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in 1261 match head' … bit_1 with 1262 [ true ⇒ 1263 let address ≝ nat_of_bitvector … seven_bits in 1264 let d ≝ address ÷ 8 in 1265 let m ≝ address mod 8 in 1266 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1267 let sfr ≝ get_bit_addressable_sfr … s t true in 1268 let new_sfr ≝ set_index … sfr m v ? in 1269 set_bit_addressable_sfr … s new_sfr t 1270 | false ⇒ 1271 let address ≝ nat_of_bitvector … seven_bits in 1272 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1273 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1274 let n_bit ≝ set_index … t (modulus address 8) v ? in 1275 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1276 set_low_internal_ram … s memory 1277 ] 1278 | CARRY ⇒ 1279 λcarry: True. 1280 let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in 1281 let new_psw ≝ v:::seven_bits in 1282 set_8051_sfr ?? s SFR_PSW new_psw 1283 | _ ⇒ 1284 λother: False. 1285 match other in False with 1286 [ ] 1287 ] (subaddressing_modein … a). 1288 try (repeat @le_S_S @le_O_n) 1289 try @modulus_less_than 1290 /by/ 1291 cases daemon (* XXX: russell type for preservation of clock on set_bit_addressable_sfr *) 1292 qed. 1293 1294 definition set_arg_1: 1295 ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → 1296 Bit → PreStatus M code_memory ≝ set_arg_1'. 1297 1298 definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝ 1299 λM: internal_pseudo_address_map. 1300 λcm: pseudo_assembly_program. 1301 λs: PreStatus ? cm. 1302 λsigma: Word → Word. 1303 λaddr: [[bit_addr; carry]]. 1304 λv: Bit. 1305 match addr with 1306 [ BIT_ADDR b ⇒ 1307 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in 1308 match head' … bit_1 with 1309 [ true ⇒ 1310 let address ≝ nat_of_bitvector … seven_bits in 1311 let d ≝ address ÷ 8 in 1312 let m ≝ address mod 8 in 1313 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1314 let sfr ≝ get_bit_addressable_sfr … s t true in 1315 map_address_Byte_using_internal_pseudo_address_map M sigma t sfr = sfr 1316 | false ⇒ 1317 let address ≝ nat_of_bitvector … seven_bits in 1318 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1319 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1320 map_internal_ram_address_using_pseudo_address_map M sigma 1321 (false:::address') t = t 1322 ] 1323 | CARRY ⇒ True 1324 | _ ⇒ True 1325 ]. 1326 1327 definition map_bit_address_mode_using_internal_pseudo_address_map_set_2 ≝ 1328 λM: internal_pseudo_address_map. 1329 λcm: pseudo_assembly_program. 1330 λs: PreStatus ? cm. 1331 λsigma: Word → Word. 1332 λaddr: [[bit_addr; carry]]. 1333 λv: Bit. 1334 match addr with 1335 [ BIT_ADDR b ⇒ 1336 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in 1337 match head' … bit_1 with 1338 [ true ⇒ 1339 let address ≝ nat_of_bitvector … seven_bits in 1340 let d ≝ address ÷ 8 in 1341 let m ≝ address mod 8 in 1342 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1343 let sfr ≝ get_bit_addressable_sfr … s t true in 1344 let new_sfr ≝ set_index … sfr m v ? in 1345 map_address_Byte_using_internal_pseudo_address_map M sigma new_sfr t = t 1346 | false ⇒ 1347 let address ≝ nat_of_bitvector … seven_bits in 1348 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1349 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1350 let n_bit ≝ set_index … t (modulus address 8) v ? in 1351 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1352 map_internal_ram_address_using_pseudo_address_map M sigma 1353 (false:::address') n_bit = n_bit 1354 ] 1355 | CARRY ⇒ True 1356 | _ ⇒ True 1357 ]. 1358 @modulus_less_than 1359 qed. 1360 1361 lemma set_arg_1_status_of_pseudo_status: 1362 ∀cm: pseudo_assembly_program. 1363 ∀ps: PreStatus pseudo_assembly_program cm. 1364 ∀addr: [[bit_addr; carry]]. 1365 ∀b: Bit. 1366 Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. 1367 map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b → 1368 map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b → 1369 set_arg_1 (BitVectorTrie Byte 16) 1370 (code_memory_of_pseudo_assembly_program cm sigma policy) 1371 (status_of_pseudo_status M cm ps sigma policy) addr b = 1372 status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy. 1373 whd in match set_arg_1; normalize nodelta 1374 whd in match set_arg_1'; normalize nodelta 1375 whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta 1376 whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_2; normalize nodelta 1377 @(let m ≝ pseudo_assembly_program in 1378 λcm. 1379 λs: PreStatus m cm. 1380 λa: [[bit_addr; carry]]. 1381 λv: Bit. 1382 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with 1383 [ BIT_ADDR b ⇒ λbit_addr: True. 1384 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in 1385 match head' … bit_1 with 1386 [ true ⇒ 1387 let address ≝ nat_of_bitvector … seven_bits in 1388 let d ≝ address ÷ 8 in 1389 let m ≝ address mod 8 in 1390 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1391 let sfr ≝ get_bit_addressable_sfr … s t true in 1392 let new_sfr ≝ set_index … sfr m v ? in 1393 set_bit_addressable_sfr … s new_sfr t 1394 | false ⇒ 1395 let address ≝ nat_of_bitvector … seven_bits in 1396 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1397 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1398 let n_bit ≝ set_index … t (modulus address 8) v ? in 1399 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1400 set_low_internal_ram … s memory 1401 ] 1402 | CARRY ⇒ 1403 λcarry: True. 1404 let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in 1405 let new_psw ≝ v:::seven_bits in 1406 set_8051_sfr ?? s SFR_PSW new_psw 1407 | _ ⇒ 1408 λother: False. 1409 match other in False with 1410 [ ] 1411 ] (subaddressing_modein … a)) normalize nodelta 1412 try @modulus_less_than #M #sigma #policy 1413 [1: 1414 #_ #_ >get_8051_sfr_status_of_pseudo_status 1415 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 1416 >p normalize nodelta @set_8051_sfr_status_of_pseudo_status % 1417 |2,3: 1418 >get_8051_sfr_status_of_pseudo_status 1419 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 1420 >p normalize nodelta >p1 normalize nodelta 1421 #map_bit_address_assm_1 #map_bit_address_assm_2 1422 [1: 1423 >get_bit_addressable_sfr_status_of_pseudo_status 1424 >map_bit_address_assm_1 1425 >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) % 1426 |2: 1427 whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta 1428 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) 1429 >map_bit_address_assm_1 1430 >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2) 1431 >set_low_internal_ram_status_of_pseudo_status in ⊢ (??%?); % 1432 ] 1433 ] 1434 qed.
Note: See TracChangeset
for help on using the changeset viewer.