Changeset 2172 for src/ASM/Status.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/Status.ma

    r2160 r2172  
    546546    set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7).
    547547 
    548 definition get_bit_addressable_sfr ≝
    549   λM: Type[0].
    550   λcode_memory:M.
    551   λs: PreStatus M code_memory.
    552   λn: nat.
    553   λb: BitVector n.
     548
     549definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
     550  λb: Byte.
     551    let address ≝ nat_of_bitvector … b in
     552      if (eqb address 128) then None ?
     553      else if (eqb address 144) then Some … (inl … SFR_P1)
     554      else if (eqb address 160) then None ?
     555      else if (eqb address 176) then Some … (inl … SFR_P3)
     556      else if (eqb address 153) then Some … (inl … SFR_SBUF)
     557      else if (eqb address 138) then Some … (inl … SFR_TL0)
     558      else if (eqb address 139) then Some … (inl … SFR_TL1)
     559      else if (eqb address 140) then Some … (inl … SFR_TH0)
     560      else if (eqb address 141) then Some … (inl … SFR_TH1)
     561      else if (eqb address 200) then Some … (inr … SFR_T2CON)
     562      else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
     563      else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
     564      else if (eqb address 204) then Some … (inr … SFR_TL2)
     565      else if (eqb address 205) then Some … (inr … SFR_TH2)
     566      else if (eqb address 135) then Some … (inl … SFR_PCON)
     567      else if (eqb address 136) then Some … (inl … SFR_TCON)
     568      else if (eqb address 137) then Some … (inl … SFR_TMOD)
     569      else if (eqb address 152) then Some … (inl … SFR_SCON)
     570      else if (eqb address 168) then Some … (inl … SFR_IE)
     571      else if (eqb address 184) then Some … (inl … SFR_IP)
     572      else if (eqb address 129) then Some … (inl … SFR_SP)
     573      else if (eqb address 130) then Some … (inl … SFR_DPL)
     574      else if (eqb address 131) then Some … (inl … SFR_DPH)
     575      else if (eqb address 208) then Some … (inl … SFR_PSW)
     576      else if (eqb address 224) then Some … (inl … SFR_ACC_A)
     577      else if (eqb address 240) then Some … (inl … SFR_ACC_B)
     578      else None ?.
     579
     580definition get_bit_addressable_sfr:
     581    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝
     582  λM: Type[0].
     583  λcode_memory:M.
     584  λs: PreStatus M code_memory.
     585  λb: Byte.
    554586  λl: bool.
    555     let address ≝ nat_of_bitvector … b in
    556       if (eqb address 128) then
    557         ?
    558       else if (eqb address 144) then
     587  match sfr_of_Byte b with
     588  [ None ⇒ match not_implemented in False with [ ]
     589  | Some sfr8051_8052 ⇒
     590    match sfr8051_8052 with
     591    [ inl sfr ⇒
     592      match sfr with
     593      [ SFR_P1 ⇒
    559594        if l then
    560           (p1_latch ?? s)
     595          p1_latch … s
    561596        else
    562           (get_8051_sfr ?? s SFR_P1)
    563       else if (eqb address 160) then
    564         ?
    565       else if (eqb address 176) then
     597          get_8051_sfr … s SFR_P1
     598      | SFR_P3 ⇒
    566599        if l then
    567           (p3_latch ?? s)
     600          p3_latch … s
    568601        else
    569           (get_8051_sfr ?? s SFR_P3)
    570       else if (eqb address 153) then
    571         get_8051_sfr ?? s SFR_SBUF
    572       else if (eqb address 138) then
    573         get_8051_sfr ?? s SFR_TL0
    574       else if (eqb address 139) then
    575         get_8051_sfr ?? s SFR_TL1
    576       else if (eqb address 140) then
    577         get_8051_sfr ?? s SFR_TH0
    578       else if (eqb address 141) then
    579         get_8051_sfr ?? s SFR_TH1
    580       else if (eqb address 200) then
    581         get_8052_sfr ?? s SFR_T2CON
    582       else if (eqb address 202) then
    583         get_8052_sfr ?? s SFR_RCAP2L
    584       else if (eqb address 203) then
    585         get_8052_sfr ?? s SFR_RCAP2H
    586       else if (eqb address 204) then
    587         get_8052_sfr ?? s SFR_TL2
    588       else if (eqb address 205) then
    589         get_8052_sfr ?? s SFR_TH2
    590       else if (eqb address 135) then
    591         get_8051_sfr ?? s SFR_PCON
    592       else if (eqb address 136) then
    593         get_8051_sfr ?? s SFR_TCON
    594       else if (eqb address 137) then
    595         get_8051_sfr ?? s SFR_TMOD
    596       else if (eqb address 152) then
    597         get_8051_sfr ?? s SFR_SCON
    598       else if (eqb address 168) then
    599         get_8051_sfr ?? s SFR_IE
    600       else if (eqb address 184) then
    601         get_8051_sfr ?? s SFR_IP
    602       else if (eqb address 129) then
    603         get_8051_sfr ?? s SFR_SP
    604       else if (eqb address 130) then
    605         get_8051_sfr ?? s SFR_DPL
    606       else if (eqb address 131) then
    607         get_8051_sfr ?? s SFR_DPH
    608       else if (eqb address 208) then
    609         get_8051_sfr ?? s SFR_PSW
    610       else if (eqb address 224) then
    611         get_8051_sfr ?? s SFR_ACC_A
    612       else if (eqb address 240) then
    613         get_8051_sfr ?? s SFR_ACC_B
    614       else
    615         ?.
    616       cases not_implemented
    617 qed.
    618 
    619 definition set_bit_addressable_sfr':
    620     ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
    621       Σs':PreStatus M code_memory.
    622         clock … code_memory s = clock … code_memory s' ∧
    623         program_counter … code_memory s = program_counter … code_memory s' ≝
     602          get_8051_sfr … s SFR_P3
     603      | _ ⇒ get_8051_sfr … s sfr
     604      ]
     605    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
     606    ]
     607  ].
     608
     609definition set_bit_addressable_sfr:
     610    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → PreStatus M code_memory ≝
    624611  λM: Type[0].
    625612  λcode_memory:M.
     
    627614  λb: Byte.
    628615  λv: Byte.
    629     let address ≝ nat_of_bitvector … b in
    630       if (eqb address 128) then
    631         match not_implemented in False with [ ]
    632       else if (eqb address 144) then
    633         let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
    634         let status_2 ≝ set_p1_latch ?? s v in
    635           status_2
    636       else if (eqb address 160) then
    637         match not_implemented in False with [ ]
    638       else if (eqb address 176) then
    639         let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
    640         let status_2 ≝ set_p3_latch ?? s v in
    641           status_2
    642       else if (eqb address 153) then
    643         set_8051_sfr ?? s SFR_SBUF v
    644       else if (eqb address 138) then
    645         set_8051_sfr ?? s SFR_TL0 v
    646       else if (eqb address 139) then
    647         set_8051_sfr ?? s SFR_TL1 v
    648       else if (eqb address 140) then
    649         set_8051_sfr ?? s SFR_TH0 v
    650       else if (eqb address 141) then
    651         set_8051_sfr ?? s SFR_TH1 v
    652       else if (eqb address 200) then
    653         set_8052_sfr ?? s SFR_T2CON v
    654       else if (eqb address 202) then
    655         set_8052_sfr ?? s SFR_RCAP2L v
    656       else if (eqb address 203) then
    657         set_8052_sfr ?? s SFR_RCAP2H v
    658       else if (eqb address 204) then
    659         set_8052_sfr ?? s SFR_TL2 v
    660       else if (eqb address 205) then
    661         set_8052_sfr ?? s SFR_TH2 v
    662       else if (eqb address 135) then
    663         set_8051_sfr ?? s SFR_PCON v
    664       else if (eqb address 136) then
    665         set_8051_sfr ?? s SFR_TCON v
    666       else if (eqb address 137) then
    667         set_8051_sfr ?? s SFR_TMOD v
    668       else if (eqb address 152) then
    669         set_8051_sfr ?? s SFR_SCON v
    670       else if (eqb address 168) then
    671         set_8051_sfr ?? s SFR_IE v
    672       else if (eqb address 184) then
    673         set_8051_sfr ?? s SFR_IP v
    674       else if (eqb address 129) then
    675         set_8051_sfr ?? s SFR_SP v
    676       else if (eqb address 130) then
    677         set_8051_sfr ?? s SFR_DPL v
    678       else if (eqb address 131) then
    679         set_8051_sfr ?? s SFR_DPH v
    680       else if (eqb address 208) then
    681         set_8051_sfr ?? s SFR_PSW v
    682       else if (eqb address 224) then
    683         set_8051_sfr ?? s SFR_ACC_A v
    684       else if (eqb address 240) then
    685         set_8051_sfr ?? s SFR_ACC_B v
    686       else
    687         match not_implemented in False with [ ].
    688   /2 by refl, pair_destruct/
    689 qed.
    690 
    691 definition set_bit_addressable_sfr:
    692     ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
    693       PreStatus M code_memory ≝ set_bit_addressable_sfr'.
     616   match sfr_of_Byte b with
     617   [ None ⇒ match not_implemented in False with [ ]
     618   | Some sfr8051_8052 ⇒
     619      match sfr8051_8052 with
     620      [ inl sfr ⇒
     621         match sfr with
     622         [ SFR_P1 ⇒
     623           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
     624           set_p1_latch ?? s v
     625         | SFR_P3 ⇒
     626           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
     627           set_p3_latch ?? s v
     628         | _ ⇒ set_8051_sfr ?? s sfr v ]
     629      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].
    694630
    695631lemma clock_set_bit_addressable_sfr:
     
    697633        clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v).
    698634  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
    699   cases (set_bit_addressable_sfr' ?????) #s' * //
     635  cases (sfr_of_Byte ?)
     636  [1:
     637    normalize nodelta cases not_implemented
     638  |2:
     639    * * normalize nodelta %
     640  ]
    700641qed.
    701642
     
    704645        program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v).
    705646  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
    706   cases (set_bit_addressable_sfr' ?????) #s' * //
     647  cases (sfr_of_Byte ?)
     648  [1:
     649    normalize nodelta cases not_implemented
     650  |2:
     651    * * %
     652  ]
    707653qed.
    708654
     
    863809          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
    864810          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
    865           let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
     811          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
    866812            lookup ? 16 address (external_ram ?? s) (zero 8)
    867813      | ACC_PC ⇒
     
    872818      | DIRECT d ⇒
    873819        λdirect: True.
    874           let 〈 nu, nl 〉 ≝ vsplit ? 4 4 d in
    875           let bit_one ≝ get_index_v ? ? nu 0 ? in
    876           let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
    877             match bit_one with
    878               [ false ⇒
    879                   let address ≝ three_bits @@ nl in
    880                     lookup ? 7 address (low_internal_ram ?? s) (zero 8)
    881               | true ⇒ get_bit_addressable_sfr ?? s 8 d l
    882               ]
     820          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
     821            match head' … hd with
     822            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
     823            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
     824            ]
    883825      | INDIRECT i ⇒
    884826        λindirect: True.
    885           let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_register ?? s [[ false; false; i]]) in
    886           let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    887           let bit_1 ≝ get_index_v ?? bit_one_v O ? in
    888           match  bit_1 with
    889             [ false ⇒
    890                 lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8)
    891             | true ⇒
    892                 lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8)
     827          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
     828            match head' … hd with
     829            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
     830            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
    893831            ]
    894832      | _ ⇒ λother.
    895833        match other in False with [ ]
    896834      ] (subaddressing_modein … a).
    897   [1,2:
    898      normalize
    899      repeat (@ le_S_S)
    900      @ le_O_n
    901   ]
    902 qed.
    903 
    904 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
     835
     836definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
    905837                                   acc_a ; acc_b ; ext_indirect ;
    906                                    ext_indirect_dptr ]]. Byte → Σs':PreStatus M code_memory.
    907                                    clock … code_memory s = clock … code_memory s' ∧
    908                                    (¬(is_a … direct addr) → p1_latch … code_memory s = p1_latch … code_memory s') ∧
    909                                    (¬(is_a … direct addr) → p3_latch … code_memory s = p3_latch … code_memory s') ∧
    910                                    program_counter … code_memory s = program_counter … code_memory s' ∧
    911                                    (¬(is_a … direct addr) → special_function_registers_8052 … code_memory s = special_function_registers_8052 … code_memory s') ≝
     838                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
    912839  λm, cm, s, a, v.
    913840    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    914841                                                acc_a ; acc_b ; ext_indirect ;
    915842                                                ext_indirect_dptr ]] x) →
    916                    Σs':PreStatus m cm. ?
    917                    (*CSC: bug here if one specified the two clock above*)
     843                   PreStatus m cm
    918844            with
    919845      [ DIRECT d ⇒
    920846        λdirect: True.
    921           let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in
    922           let bit_one ≝ get_index_v ? ? nu 0 ? in
    923           let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
    924             match bit_one with
    925               [ true ⇒ set_bit_addressable_sfr ?? s d v
     847          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
     848            match head' … bit_one with
     849              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
    926850              | false ⇒
    927                 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
     851                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
    928852                  set_low_internal_ram ?? s memory
    929853              ]
     
    931855        λindirect: True.
    932856          let register ≝ get_register ?? s [[ false; false; i ]] in
    933           let 〈nu, nl〉 ≝ vsplit ? 4 4 register in
    934           let bit_1 ≝ get_index_v … nu 0 ? in
    935           let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
    936             match bit_1 with
     857          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
     858            match head' … bit_one with
    937859              [ false ⇒
    938                 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
     860                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
    939861                  set_low_internal_ram ?? s memory
    940862              | true ⇒
    941                 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
     863                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
    942864                  set_high_internal_ram ?? s memory
    943865              ]
     
    960882          match other in False with [ ]
    961883      ] (subaddressing_modein … a).
    962   /6 by conj, False_ind/
    963 qed.
    964 
    965 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory ≝
    966  set_arg_8'.
    967884
    968885lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
    969  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
    970  cases (set_arg_8' ?????) #s' * * * * //
     886  cases daemon
    971887qed.
    972888
    973889lemma program_counter_set_arg_8: ∀M,cm,s,x,v. program_counter M cm s = program_counter … (set_arg_8 M cm s x v).
    974  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
    975  cases (set_arg_8' ?????) #s' * * * * //
     890  cases daemon
    976891qed.
    977892
     
    979894  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
    980895  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
    981   cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ]
    982   * * * * #_ #relevant #_ #_ #_ @relevant @I
     896  cases daemon
    983897qed.
    984898
     
    986900  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
    987901  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
    988   cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ]
    989   * * * * #_ #_ #relevant #_ #_ @relevant @I
     902  cases daemon
    990903qed.
    991904
     
    993906  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
    994907  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
    995   cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ]
    996   * * * * #_ #_ #_ #_ #relevant @relevant @I
     908  cases daemon
    997909qed.
    998910
     
    1056968      [ BIT_ADDR b ⇒
    1057969        λbit_addr: True.
    1058           let 〈 nu, nl 〉 ≝ vsplit … 4 4 b in
    1059           let bit_1 ≝ get_index_v ? ? nu 0 ? in
    1060           let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    1061             match bit_1 with
    1062               [ true ⇒
    1063                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1064                 let d ≝ address ÷ 8 in
    1065                 let m ≝ address mod 8 in
    1066                 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1067                 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
    1068                   get_index_v … sfr m ?
    1069               | false ⇒
    1070                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1071                 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1072                 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    1073                   get_index_v … t (modulus address 8) ?
    1074               ]
     970        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
     971        match head' … bit_1 with
     972        [ true ⇒
     973          let address ≝ nat_of_bitvector … seven_bits in
     974          let d ≝ address ÷ 8 in
     975          let m ≝ address mod 8 in
     976          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     977          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
     978            get_index_v … sfr m ?
     979        | false ⇒
     980          let address ≝ nat_of_bitvector … seven_bits in
     981          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     982          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
     983            get_index_v … t (modulus address 8) ?
     984        ]
    1075985      | N_BIT_ADDR n ⇒
    1076986        λn_bit_addr: True.
    1077           let 〈 nu, nl 〉 ≝ vsplit … 4 4 n in
    1078           let bit_1 ≝ get_index_v ? ? nu 0 ? in
    1079           let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    1080             match bit_1 with
    1081               [ true ⇒
    1082                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1083                 let d ≝ address ÷ 8 in
    1084                 let m ≝ address mod 8 in
    1085                 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1086                 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
    1087                   ¬(get_index_v … sfr m ?)
    1088               | false ⇒
    1089                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1090                 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1091                 let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
    1092                   ¬(get_index_v … trans (modulus address 8) ?)
    1093               ]
     987        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
     988        match head' … bit_1 with
     989        [ true ⇒
     990          let address ≝ nat_of_bitvector … seven_bits in
     991          let d ≝ address ÷ 8 in
     992          let m ≝ address mod 8 in
     993          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     994          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
     995            ¬(get_index_v … sfr m ?)
     996        | false ⇒
     997          let address ≝ nat_of_bitvector … seven_bits in
     998          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     999          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
     1000            ¬(get_index_v … t (modulus address 8) ?)
     1001        ]
    10941002      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
    10951003      | _ ⇒ λother.
    10961004        match other in False with [ ]
    10971005      ] (subaddressing_modein … a).
    1098       [3,6:
    1099          normalize
    1100          repeat (@ le_S_S)
    1101          @ le_O_n
    1102       |1,2,4,5:
    1103          @modulus_less_than
    1104       ]
     1006      @modulus_less_than
    11051007qed.
    11061008     
    1107 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'
     1009definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → PreStatus M code_memory
    11081010  λm: Type[0].
    11091011  λcm.
     
    11111013  λa: [[bit_addr; carry]].
    11121014  λv: Bit.
    1113     match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with
     1015    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with
    11141016      [ BIT_ADDR b ⇒ λbit_addr: True.
    1115         let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    1116         let bit_1 ≝ get_index_v ?? nu 0 ? in
    1117         let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
    1118         match bit_1 return λ_. ? with
    1119           [ true ⇒
    1120             let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1121             let d ≝ address ÷ 8 in
    1122             let m ≝ address mod 8 in
    1123             let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1124             let sfr ≝ get_bit_addressable_sfr ?? s ? t true in
    1125             let new_sfr ≝ set_index … sfr m v ? in
    1126               set_bit_addressable_sfr ?? s new_sfr t
    1127           | false ⇒
    1128             let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1129             let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1130             let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
    1131             let n_bit ≝ set_index … t (modulus address 8) v ? in
    1132             let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
    1133               set_low_internal_ram ?? s memory
    1134           ]
     1017        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1018        match head' … bit_1 with
     1019        [ true ⇒
     1020          let address ≝ nat_of_bitvector … seven_bits in
     1021          let d ≝ address ÷ 8 in
     1022          let m ≝ address mod 8 in
     1023          let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     1024          let sfr ≝ get_bit_addressable_sfr … s t true in
     1025          let new_sfr ≝ set_index … sfr m v ? in
     1026            set_bit_addressable_sfr … s new_sfr t
     1027        | false ⇒
     1028          let address ≝ nat_of_bitvector … seven_bits in
     1029          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     1030          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
     1031          let n_bit ≝ set_index … t (modulus address 8) v ? in
     1032          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
     1033            set_low_internal_ram … s memory
     1034        ]
    11351035      | CARRY ⇒
    11361036        λcarry: True.
    1137         let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    1138         let bit_1 ≝ get_index_v… nu 1 ? in
    1139         let bit_2 ≝ get_index_v… nu 2 ? in
    1140         let bit_3 ≝ get_index_v… nu 3 ? in
    1141         let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
     1037        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1038        let new_psw ≝ v:::seven_bits in
    11421039          set_8051_sfr ?? s SFR_PSW new_psw
    11431040      | _ ⇒
     
    11461043            [ ]
    11471044      ] (subaddressing_modein … a).
    1148 try (repeat @le_S_S @le_O_n)
    1149 /by/
    1150 qed.
    1151 
    1152 definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'.
     1045  @modulus_less_than
     1046qed.
    11531047
    11541048lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v).
    1155  #M #cm #s #x #v whd in match set_arg_1; normalize nodelta @pi2
     1049  cases daemon
    11561050qed.
    11571051
Note: See TracChangeset for help on using the changeset viewer.