Changeset 2171


Ignore:
Timestamp:
Jul 10, 2012, 11:54:54 AM (5 years ago)
Author:
mulligan
Message:

Finished the commutations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2168 r2171  
    151151      normalize @eq_f @inductive_hypothesis @nmk #relevant
    152152      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
     153    ]
     154  ]
     155qed.
     156
     157(* XXX: move elsewhere *)
     158lemma 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)
    153186    ]
    154187  ]
     
    202235qed.
    203236
     237lemma 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  ]
     274qed.
     275
    204276lemma set_8051_sfr_status_of_pseudo_status:
    205277  ∀M, code_memory, sigma, policy, s, sfr, v,v'.
     
    212284  #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok
    213285  whd in ⊢ (??%%); @split_eq_status try % /2/
     286qed.
     287
     288lemma 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
     298qed.
     299
     300lemma 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  //
    214307qed.
    215308
     
    394487qed.
    395488
    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 #j
    408   [1:
    409     #b #i_proof
    410     cases (lt_to_not_zero … i_proof)
    411   |2:
    412     #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j
    413     lapply i_proof lapply i_neq_j cases i'
    414     [1:
    415       -i_neq_j #i_neq_j -i_proof #i_proof
    416       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_proof
    425       lapply j_proof lapply i_neq_j cases j'
    426       [1:
    427         #_ #j_proof %
    428       |2:
    429         #j' #i_neq_j #j_proof
    430         @inductive_hypothesis @nmk #relevant
    431         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 sfr
    443    (get_8051_sfr … cm s sfr).
    444  #M #cm #s #sigma #policy #sfr whd in ⊢ (??%%);
    445  whd in match status_of_pseudo_status; normalize nodelta
    446  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    447  whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
    448  cases (\snd M) normalize nodelta [cases sfr %]
    449  #map_mem #map_acc @pair_elim #high #low #_ normalize nodelta
    450  cases (eq_upper_lower ??) normalize nodelta cases sfr normalize nodelta
    451  [18,37: @get_index_v_set_index
    452  |*: >get_index_v_set_index_miss % normalize #abs destruct]
    453 qed.
    454 
    455489lemma bit_address_of_register_status_of_pseudo_status:
    456490 ∀M,cm,s,sigma,policy,r.
     
    476510  (lookup Byte 7 addr
    477511   (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 *)
     515axiom 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)).
    478524
    479525lemma get_register_status_of_pseudo_status:
     
    526572
    527573definition 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.
    529575  match addr with
    530576  [ INDIRECT i ⇒
     
    534580     assoc_list_lookup ??
    535581      (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
    536591  | _ ⇒ True ].
    537592
     
    633688  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
    634689  ∀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 →
    636691   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
    637692    set_arg_8 (BitVectorTrie Byte 16)
     
    712767      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
    713768qed.
     769
     770definition 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
     799definition 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
     850lemma 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  //
     861qed.
     862
     863lemma 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  //
     874qed.
     875
     876lemma 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/
     919qed.
     920
     921lemma 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
     935qed.
     936
     937lemma 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  //
     945qed.
     946
     947lemma 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 %
     956qed.
     957
     958lemma 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  ]
     1051qed.
     1052
     1053lemma 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  //
     1062qed.
     1063
     1064lemma 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  //
     1081qed.
     1082
     1083definition 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
     1128qed.
     1129
     1130definition 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
     1167lemma 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  ]
     1235qed.
     1236
     1237lemma 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
     1250qed.
     1251
     1252definition 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 *)
     1292qed.
     1293
     1294definition 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
     1298definition 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
     1327definition 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
     1359qed.
     1360
     1361lemma 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  ]
     1434qed.
Note: See TracChangeset for help on using the changeset viewer.