Changeset 2163 for src


Ignore:
Timestamp:
Jul 6, 2012, 11:04:17 PM (8 years ago)
Author:
sacerdot
Message:

Steady progress.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Test.ma

    r2160 r2163  
    185185
    186186lemma set_8051_sfr_status_of_pseudo_status:
     187  ∀M, code_memory, sigma, policy, s, sfr, v,v'.
     188  map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
     189(set_8051_sfr (BitVectorTrie Byte 16)
     190  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     191  (status_of_pseudo_status M code_memory s sigma policy) sfr v'
     192  =status_of_pseudo_status M code_memory
     193   (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
     194  #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok
     195  whd in ⊢ (??%%); @split_eq_status try % /2/
     196qed.
     197
     198lemma set_8052_sfr_status_of_pseudo_status:
    187199  ∀M, code_memory, sigma, policy, s, sfr, v.
    188 (set_8051_sfr (BitVectorTrie Byte 16)
     200(set_8052_sfr (BitVectorTrie Byte 16)
    189201  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    190202  (status_of_pseudo_status M code_memory s sigma policy) sfr v
    191203  =status_of_pseudo_status M code_memory
    192    (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
    193   #M #code_memory #sigma #policy #s #sfr #v
    194   whd in ⊢ (??%%); @split_eq_status try %
     204   (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
     205 //
     206qed.
     207
     208definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
     209  λb: Byte.
     210    let address ≝ nat_of_bitvector … b in
     211      if (eqb address 128) then None ?
     212      else if (eqb address 144) then Some … (inl … SFR_P1)
     213      else if (eqb address 160) then None ?
     214      else if (eqb address 176) then Some … (inl … SFR_P3)
     215      else if (eqb address 153) then Some … (inl … SFR_SBUF)
     216      else if (eqb address 138) then Some … (inl … SFR_TL0)
     217      else if (eqb address 139) then Some … (inl … SFR_TL1)
     218      else if (eqb address 140) then Some … (inl … SFR_TH0)
     219      else if (eqb address 141) then Some … (inl … SFR_TH1)
     220      else if (eqb address 200) then Some … (inr … SFR_T2CON)
     221      else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
     222      else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
     223      else if (eqb address 204) then Some … (inr … SFR_TL2)
     224      else if (eqb address 205) then Some … (inr … SFR_TH2)
     225      else if (eqb address 135) then Some … (inl … SFR_PCON)
     226      else if (eqb address 136) then Some … (inl … SFR_TCON)
     227      else if (eqb address 137) then Some … (inl … SFR_TMOD)
     228      else if (eqb address 152) then Some … (inl … SFR_SCON)
     229      else if (eqb address 168) then Some … (inl … SFR_IE)
     230      else if (eqb address 184) then Some … (inl … SFR_IP)
     231      else if (eqb address 129) then Some … (inl … SFR_SP)
     232      else if (eqb address 130) then Some … (inl … SFR_DPL)
     233      else if (eqb address 131) then Some … (inl … SFR_DPH)
     234      else if (eqb address 208) then Some … (inl … SFR_PSW)
     235      else if (eqb address 224) then Some … (inl … SFR_ACC_A)
     236      else if (eqb address 240) then Some … (inl … SFR_ACC_B)
     237      else None ?.
    195238
    196239definition set_bit_addressable_sfr:
    … …  
    202245  λb: Byte.
    203246  λv: Byte.
    204     let address ≝ nat_of_bitvector … b in
    205       if (eqb address 128) then
    206         match not_implemented in False with [ ]
    207       else if (eqb address 144) then
    208         let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
    209         let status_2 ≝ set_p1_latch ?? s v in
    210           status_2
    211       else if (eqb address 160) then
    212         match not_implemented in False with [ ]
    213       else if (eqb address 176) then
    214         let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
    215         let status_2 ≝ set_p3_latch ?? s v in
    216           status_2
    217       else if (eqb address 153) then
    218         set_8051_sfr ?? s SFR_SBUF v
    219       else if (eqb address 138) then
    220         set_8051_sfr ?? s SFR_TL0 v
    221       else if (eqb address 139) then
    222         set_8051_sfr ?? s SFR_TL1 v
    223       else if (eqb address 140) then
    224         set_8051_sfr ?? s SFR_TH0 v
    225       else if (eqb address 141) then
    226         set_8051_sfr ?? s SFR_TH1 v
    227       else if (eqb address 200) then
    228         set_8052_sfr ?? s SFR_T2CON v
    229       else if (eqb address 202) then
    230         set_8052_sfr ?? s SFR_RCAP2L v
    231       else if (eqb address 203) then
    232         set_8052_sfr ?? s SFR_RCAP2H v
    233       else if (eqb address 204) then
    234         set_8052_sfr ?? s SFR_TL2 v
    235       else if (eqb address 205) then
    236         set_8052_sfr ?? s SFR_TH2 v
    237       else if (eqb address 135) then
    238         set_8051_sfr ?? s SFR_PCON v
    239       else if (eqb address 136) then
    240         set_8051_sfr ?? s SFR_TCON v
    241       else if (eqb address 137) then
    242         set_8051_sfr ?? s SFR_TMOD v
    243       else if (eqb address 152) then
    244         set_8051_sfr ?? s SFR_SCON v
    245       else if (eqb address 168) then
    246         set_8051_sfr ?? s SFR_IE v
    247       else if (eqb address 184) then
    248         set_8051_sfr ?? s SFR_IP v
    249       else if (eqb address 129) then
    250         set_8051_sfr ?? s SFR_SP v
    251       else if (eqb address 130) then
    252         set_8051_sfr ?? s SFR_DPL v
    253       else if (eqb address 131) then
    254         set_8051_sfr ?? s SFR_DPH v
    255       else if (eqb address 208) then
    256         set_8051_sfr ?? s SFR_PSW v
    257       else if (eqb address 224) then
    258         set_8051_sfr ?? s SFR_ACC_A v
    259       else if (eqb address 240) then
    260         set_8051_sfr ?? s SFR_ACC_B v
    261       else
    262         match not_implemented in False with [ ].
    263 
    264 lemma set_bit_addressable_sfr_status_of_pseudo_status:
     247   match sfr_of_Byte b with
     248   [ None ⇒ match not_implemented in False with [ ]
     249   | Some sfr8051_8052 ⇒
     250      match sfr8051_8052 with
     251      [ inl sfr ⇒
     252         match sfr with
     253         [ SFR_P1 ⇒
     254           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
     255           set_p1_latch ?? s v
     256         | SFR_P3 ⇒
     257           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
     258           set_p3_latch ?? s v
     259         | _ ⇒ set_8051_sfr ?? s sfr v ]
     260      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].
     261
     262definition map_address_Byte_using_internal_pseudo_address_map ≝
     263 λM,sigma,d,v.
     264  match sfr_of_Byte d with
     265  [ None ⇒ v
     266  | Some sfr8051_8052 ⇒
     267     match sfr8051_8052 with
     268     [ inl sfr ⇒
     269        map_address_using_internal_pseudo_address_map M sigma sfr v
     270     | inr _ ⇒ v ]].
     271
     272lemma set_bit_addressable_sfr_status_of_pseudo_status':
    265273      let M ≝ pseudo_assembly_program in ∀code_memory: M. ∀s: PreStatus M code_memory. ∀d: Byte. ∀v: Byte.
    266         Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy.
     274        Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy. ∀v'.
     275  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
    267276 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
    268277  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    269   (status_of_pseudo_status M code_memory s sigma policy) d v
     278  (status_of_pseudo_status M code_memory s sigma policy) d v'
    270279  =status_of_pseudo_status M code_memory
    271280   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
    272   whd in match set_bit_addressable_sfr; normalize nodelta
     281  whd in match set_bit_addressable_sfr;
     282  whd in match map_address_Byte_using_internal_pseudo_address_map;
     283  normalize nodelta
    273284  @(let M ≝ pseudo_assembly_program in
    274285  λcode_memory:M.
    … …  
    276287  λb: Byte.
    277288  λv: Byte.
    278     let address ≝ nat_of_bitvector … b in
    279       if (eqb address 128) then
    280         match not_implemented in False with [ ]
    281       else if (eqb address 144) then
    282         let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
    283         let status_2 ≝ set_p1_latch ?? s v in
    284           status_2
    285       else if (eqb address 160) then
    286         match not_implemented in False with [ ]
    287       else if (eqb address 176) then
    288         let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
    289         let status_2 ≝ set_p3_latch ?? s v in
    290           status_2
    291       else if (eqb address 153) then
    292         set_8051_sfr ?? s SFR_SBUF v
    293       else if (eqb address 138) then
    294         set_8051_sfr ?? s SFR_TL0 v
    295       else if (eqb address 139) then
    296         set_8051_sfr ?? s SFR_TL1 v
    297       else if (eqb address 140) then
    298         set_8051_sfr ?? s SFR_TH0 v
    299       else if (eqb address 141) then
    300         set_8051_sfr ?? s SFR_TH1 v
    301       else if (eqb address 200) then
    302         set_8052_sfr ?? s SFR_T2CON v
    303       else if (eqb address 202) then
    304         set_8052_sfr ?? s SFR_RCAP2L v
    305       else if (eqb address 203) then
    306         set_8052_sfr ?? s SFR_RCAP2H v
    307       else if (eqb address 204) then
    308         set_8052_sfr ?? s SFR_TL2 v
    309       else if (eqb address 205) then
    310         set_8052_sfr ?? s SFR_TH2 v
    311       else if (eqb address 135) then
    312         set_8051_sfr ?? s SFR_PCON v
    313       else if (eqb address 136) then
    314         set_8051_sfr ?? s SFR_TCON v
    315       else if (eqb address 137) then
    316         set_8051_sfr ?? s SFR_TMOD v
    317       else if (eqb address 152) then
    318         set_8051_sfr ?? s SFR_SCON v
    319       else if (eqb address 168) then
    320         set_8051_sfr ?? s SFR_IE v
    321       else if (eqb address 184) then
    322         set_8051_sfr ?? s SFR_IP v
    323       else if (eqb address 129) then
    324         set_8051_sfr ?? s SFR_SP v
    325       else if (eqb address 130) then
    326         set_8051_sfr ?? s SFR_DPL v
    327       else if (eqb address 131) then
    328         set_8051_sfr ?? s SFR_DPH v
    329       else if (eqb address 208) then
    330         set_8051_sfr ?? s SFR_PSW v
    331       else if (eqb address 224) then
    332         set_8051_sfr ?? s SFR_ACC_A v
    333       else if (eqb address 240) then
    334         set_8051_sfr ?? s SFR_ACC_B v
    335       else
    336         match not_implemented in False with [ ])
    337   normalize nodelta
    338   #M #sigma #policy
    339   [1,2: //
    340   |3: //
     289   match sfr_of_Byte b with
     290   [ None ⇒ match not_implemented in False with [ ]
     291   | Some sfr8051_8052 ⇒
     292      match sfr8051_8052 with
     293      [ inl sfr ⇒
     294         match sfr with
     295         [ SFR_P1 ⇒
     296           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
     297           set_p1_latch ?? s v
     298         | SFR_P3 ⇒
     299           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
     300           set_p3_latch ?? s v
     301         | _ ⇒ set_8051_sfr ?? s sfr v ]
     302      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
     303 normalize nodelta
     304 /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
     305 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta //
     306qed.
     307
     308lemma set_bit_addressable_sfr_status_of_pseudo_status:
     309 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
     310  ∀M. ∀sigma. ∀policy. ∀v'.
     311  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
     312 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
     313  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     314  (status_of_pseudo_status M code_memory s sigma policy) d v'
     315  =status_of_pseudo_status M code_memory
     316   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
     317 #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
     318 #H @H
     319qed.
     320
     321check status_of_pseudo_status
     322
     323lemma set_low_internal_fram_status_of_pseudo_status:
     324 ∀cm,sigma,policy,M,s,ram.
     325  set_low_internal_ram (BitVectorTrie Byte 16)
     326  (code_memory_of_pseudo_assembly_program cm sigma policy)
     327  (status_of_pseudo_status M cm s sigma policy)
     328  (low_internal_ram_of_pseudo_low_internal_ram M ram)
     329  = status_of_pseudo_status M cm
     330    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
     331 //
     332qed.
     333               
     334lemma set_low_internal_fram_status_of_pseudo_status:
     335 ∀M,cm,sigma,policy,s,addr,v.
     336  insert Byte 7 addr v
     337   (low_internal_ram (BitVectorTrie Byte 16)
     338    (code_memory_of_pseudo_assembly_program cm sigma policy)
     339    (status_of_pseudo_status M cm s sigma policy))
     340  = low_internal_ram_of_pseudo_low_internal_ram M
     341     (insert Byte 7 addr v
     342      (low_internal_ram pseudo_assembly_program cm s)).
     343 #M #cm #sigma #policy #s #addr #v
     344 
     345
     346definition map_address_mode_using_internal_pseudo_address_map ≝
     347 λM,sigma,addr,v.
     348  match addr with
     349  [ DIRECT d ⇒
     350     let 〈 nu, nl 〉 as vsplit_refl ≝ vsplit … 4 4 d in
     351     match get_index_v ? ? nu 0 ? with
     352     [ true ⇒
     353      map_address_Byte_using_internal_pseudo_address_map M sigma d v
     354     | false ⇒ v ]
     355  | _ ⇒ v ].
     356//
     357qed.
    341358
    342359definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
    … …  
    398415  ∀cm.
    399416  ∀ps.
    400   ∀addr.
    401   ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy.
     417  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
     418  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'.
     419   map_address_mode_using_internal_pseudo_address_map M sigma addr value = value' →
    402420    set_arg_8 (BitVectorTrie Byte 16)
    403421      (code_memory_of_pseudo_assembly_program cm sigma policy)
    404422      (status_of_pseudo_status M cm ps sigma policy)
    405       addr value =
     423      addr value' =
    406424    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
     425  whd in match set_arg_8; normalize nodelta
    407426  @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
    408427                                   acc_a ; acc_b ; ext_indirect ;
    … …  
    411430                                                acc_a ; acc_b ; ext_indirect ;
    412431                                                ext_indirect_dptr ]] addr) →
    413                    Σp: PreStatus m cm. ∀M. ∀sigma. ∀policy.
    414     set_arg_8 (BitVectorTrie Byte 16)
    415       (code_memory_of_pseudo_assembly_program cm sigma policy)
    416       (status_of_pseudo_status M cm s sigma policy)
    417       addr v =
    418     status_of_pseudo_status M cm (set_arg_8 … cm s addr v) sigma policy
     432                   Σp.?
    419433            with
    420434      [ DIRECT d ⇒
    421435        λdirect: True.
    422           let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in
     436          deplet 〈 nu, nl 〉 as vsplit_refl ≝ vsplit … 4 4 d in
    423437          let bit_one ≝ get_index_v ? ? nu 0 ? in
    424438          let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
    … …  
    460474        λother: False.
    461475          match other in False with [ ]
    462       ] (subaddressing_modein … a))
    463   [3,6: // ]
    464   [1:
    465     #M #sigma #policy whd in ⊢ (??%(???%??));
    466     @pair_elim #nu #nl #nu_nl_refl normalize nodelta
    467     @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
    468     cases (get_index_v bool ????) normalize nodelta
    469 qed.
     476      ] (subaddressing_modein … a)) normalize nodelta
     477  [3,6: // ] #M #sigma #policy #v' whd in ⊢ (??%? → ?);
     478  [1,2:
     479    <vsplit_refl normalize nodelta >p normalize nodelta
     480    normalize nodelta in p1; >p1 normalize nodelta
     481    [ @set_bit_addressable_sfr_status_of_pseudo_status
     482    | #v_ok <v_ok @set_low_internal_ram_status_of_pseudo_status
     483    ]
     484  |2:   
     485qed.
Note: See TracChangeset for help on using the changeset viewer.