Changeset 2172 for src/ASM/Test.ma


Ignore:
Timestamp:
Jul 10, 2012, 2:39:38 PM (8 years ago)
Author:
mulligan
Message:

Moved new versions of get_ / set_arg_* into Status.ma. Commented out proofs that are no longer working.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Test.ma

    r2171 r2172  
    1 (**************************************************************************)
    2 (*       ___                                                              *)
    3 (*      ||M||                                                             *)
    4 (*      ||A||       A project by Andrea Asperti                           *)
    5 (*      ||T||                                                             *)
    6 (*      ||I||       Developers:                                           *)
    7 (*      ||T||         The HELM team.                                      *)
    8 (*      ||A||         http://helm.cs.unibo.it                             *)
    9 (*      \   /                                                             *)
    10 (*       \ /        This file is distributed under the terms of the       *)
    11 (*        v         GNU General Public License Version 2                  *)
    12 (*                                                                        *)
    13 (**************************************************************************)
    14 
    151include "ASM/Assembly.ma".
    162include "ASM/Interpret.ma".
    … …  
    316302 //
    317303qed.
    318 
    319 definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
    320   λb: Byte.
    321     let address ≝ nat_of_bitvector … b in
    322       if (eqb address 128) then None ?
    323       else if (eqb address 144) then Some … (inl … SFR_P1)
    324       else if (eqb address 160) then None ?
    325       else if (eqb address 176) then Some … (inl … SFR_P3)
    326       else if (eqb address 153) then Some … (inl … SFR_SBUF)
    327       else if (eqb address 138) then Some … (inl … SFR_TL0)
    328       else if (eqb address 139) then Some … (inl … SFR_TL1)
    329       else if (eqb address 140) then Some … (inl … SFR_TH0)
    330       else if (eqb address 141) then Some … (inl … SFR_TH1)
    331       else if (eqb address 200) then Some … (inr … SFR_T2CON)
    332       else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
    333       else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
    334       else if (eqb address 204) then Some … (inr … SFR_TL2)
    335       else if (eqb address 205) then Some … (inr … SFR_TH2)
    336       else if (eqb address 135) then Some … (inl … SFR_PCON)
    337       else if (eqb address 136) then Some … (inl … SFR_TCON)
    338       else if (eqb address 137) then Some … (inl … SFR_TMOD)
    339       else if (eqb address 152) then Some … (inl … SFR_SCON)
    340       else if (eqb address 168) then Some … (inl … SFR_IE)
    341       else if (eqb address 184) then Some … (inl … SFR_IP)
    342       else if (eqb address 129) then Some … (inl … SFR_SP)
    343       else if (eqb address 130) then Some … (inl … SFR_DPL)
    344       else if (eqb address 131) then Some … (inl … SFR_DPH)
    345       else if (eqb address 208) then Some … (inl … SFR_PSW)
    346       else if (eqb address 224) then Some … (inl … SFR_ACC_A)
    347       else if (eqb address 240) then Some … (inl … SFR_ACC_B)
    348       else None ?.
    349 
    350 definition set_bit_addressable_sfr:
    351     ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
    352       PreStatus M code_memory ≝
    353   λM: Type[0].
    354   λcode_memory:M.
    355   λs: PreStatus M code_memory.
    356   λb: Byte.
    357   λv: Byte.
    358    match sfr_of_Byte b with
    359    [ None ⇒ match not_implemented in False with [ ]
    360    | Some sfr8051_8052 ⇒
    361       match sfr8051_8052 with
    362       [ inl sfr ⇒
    363          match sfr with
    364          [ SFR_P1 ⇒
    365            let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
    366            set_p1_latch ?? s v
    367          | SFR_P3 ⇒
    368            let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
    369            set_p3_latch ?? s v
    370          | _ ⇒ set_8051_sfr ?? s sfr v ]
    371       | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].
    372 
     304 
    373305definition map_address_Byte_using_internal_pseudo_address_map ≝
    374306 λM,sigma,d,v.
    … …  
    376308  [ None ⇒ v
    377309  | Some sfr8051_8052 ⇒
    378      match sfr8051_8052 with
    379      [ inl sfr ⇒
    380         map_address_using_internal_pseudo_address_map M sigma sfr v
    381      | inr _ ⇒ v ]].
     310    match sfr8051_8052 with
     311    [ inl sfr ⇒
     312      map_address_using_internal_pseudo_address_map M sigma sfr v
     313    | inr _ ⇒ v
     314    ]
     315  ].
    382316
    383317lemma set_bit_addressable_sfr_status_of_pseudo_status':
    … …  
    390324  =status_of_pseudo_status M code_memory
    391325   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
     326  whd in match map_address_Byte_using_internal_pseudo_address_map;
    392327  whd in match set_bit_addressable_sfr;
    393   whd in match map_address_Byte_using_internal_pseudo_address_map;
    394328  normalize nodelta
    395329  @(let M ≝ pseudo_assembly_program in
    … …  
    412346         | _ ⇒ set_8051_sfr ?? s sfr v ]
    413347      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
    414  normalize nodelta
    415  /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
    416  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta //
     348  normalize nodelta
     349  /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
     350  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta //
    417351qed.
    418352
    … …  
    610544     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
    611545  | _ ⇒ v ].
    612 
    613 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
    614                                    acc_a ; acc_b ; ext_indirect ;
    615                                    ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
    616   λm, cm, s, a, v.
    617     match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    618                                                 acc_a ; acc_b ; ext_indirect ;
    619                                                 ext_indirect_dptr ]] x) →
    620                    PreStatus m cm
    621             with
    622       [ DIRECT d ⇒
    623         λdirect: True.
    624           let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
    625             match head' … bit_one with
    626               [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
    627               | false ⇒
    628                 let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
    629                   set_low_internal_ram ?? s memory
    630               ]
    631       | INDIRECT i ⇒
    632         λindirect: True.
    633           let register ≝ get_register ?? s [[ false; false; i ]] in
    634           let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
    635             match head' … bit_one with
    636               [ false ⇒
    637                 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
    638                   set_low_internal_ram ?? s memory
    639               | true ⇒
    640                 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
    641                   set_high_internal_ram ?? s memory
    642               ]
    643       | REGISTER r ⇒ λregister: True. set_register ?? s r v
    644       | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
    645       | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
    646       | EXT_INDIRECT e ⇒
    647         λext_indirect: True.
    648           let address ≝ get_register ?? s [[ false; false; e ]] in
    649           let padded_address ≝ pad 8 8 address in
    650           let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
    651             set_external_ram ?? s memory
    652       | EXT_INDIRECT_DPTR ⇒
    653         λext_indirect_dptr: True.
    654           let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
    655           let memory ≝ insert ? 16 address v (external_ram ?? s) in
    656             set_external_ram ?? s memory
    657       | _ ⇒
    658         λother: False.
    659           match other in False with [ ]
    660       ] (subaddressing_modein … a).
    661546
    662547(*CSC: move elsewhere*)
    … …  
    767652      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
    768653qed.
    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).
    849654
    850655lemma p1_latch_status_of_pseudo_status:
    … …  
    1081886qed.
    1082887
    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 
    1130888definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝
    1131889 λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl.
    … …  
    12501008qed.
    12511009
    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 
    12981010definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝
    12991011  λM: internal_pseudo_address_map.
    … …  
    13721084        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy.
    13731085  whd in match set_arg_1; normalize nodelta
    1374   whd in match set_arg_1'; normalize nodelta
    13751086  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta
    13761087  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_2; normalize nodelta
    … …  
    14331144  ]
    14341145qed.
     1146
     1147lemma clock_status_of_pseudo_status:
     1148 ∀M,cm,sigma,policy,s.
     1149  clock …
     1150   (code_memory_of_pseudo_assembly_program cm sigma policy)
     1151   (status_of_pseudo_status M cm s sigma policy)
     1152  = clock … cm s.
     1153//
     1154qed.
     1155
     1156lemma set_clock_status_of_pseudo_status:
     1157 ∀M,cm,sigma,policy,s,v.
     1158  set_clock …
     1159   (code_memory_of_pseudo_assembly_program cm sigma policy)
     1160   (status_of_pseudo_status M cm s sigma policy) v
     1161  = status_of_pseudo_status M cm (set_clock … cm s v) sigma policy.
     1162//
     1163qed.
Note: See TracChangeset for help on using the changeset viewer.