Changeset 2272 for src/ASM/Status.ma


Ignore:
Timestamp:
Jul 27, 2012, 5:53:25 PM (8 years ago)
Author:
mulligan
Message:

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r2270 r2272  
    700700      set_low_internal_ram … s new_low_internal_ram.
    701701     
    702 definition read_at_stack_pointer ≝
    703   λM: Type[0].
    704   λcode_memory:M.
    705   λs: PreStatus M code_memory.
    706     let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_SP) in
    707     let m ≝ get_index_v ?? nu O ? in
    708     let r1 ≝ get_index_v ?? nu 1 ? in
    709     let r2 ≝ get_index_v ?? nu 2 ? in
    710     let r3 ≝ get_index_v ?? nu 3 ? in
    711     let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
     702definition read_from_internal_ram ≝
     703  λM: Type[0].
     704  λcode_memory:M.
     705  λs: PreStatus M code_memory.
     706  λaddr: Byte.
     707    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
    712708    let memory ≝
    713       if m then
     709      if head' … bit_one then
    714710        (low_internal_ram ?? s)
    715711      else
    716712        (high_internal_ram ?? s)
    717713    in
    718       lookup … address memory (zero 8).
    719   [1,2,3,4:
    720      normalize
    721      repeat (@ le_S_S)
    722      @ le_O_n
    723   ]
    724 qed.
     714      lookup … seven_bits memory (zero 8).
     715
     716definition read_at_stack_pointer ≝
     717  λM: Type[0].
     718  λcode_memory:M.
     719  λs: PreStatus M code_memory.
     720    read_from_internal_ram M code_memory s (get_8051_sfr ?? s SFR_SP).
    725721
    726722definition write_at_stack_pointer ≝
     
    729725  λs: PreStatus M code_memory.
    730726  λv: Byte.
    731     let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ?? s SFR_SP) in
    732     let bit_zero ≝ get_index_v ?? nu O ? in
    733     let bit_1 ≝ get_index_v ?? nu 1 ? in
    734     let bit_2 ≝ get_index_v ?? nu 2 ? in
    735     let bit_3 ≝ get_index_v ?? nu 3 ? in
    736       if bit_zero then
    737         let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    738                               v (high_internal_ram ?? s) in
     727    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr ?? s SFR_SP) in
     728      if head' … 0 bit_one then
     729        let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
    739730          set_high_internal_ram ?? s memory
    740731      else
    741         let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    742                               v (low_internal_ram ?? s) in
     732        let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
    743733          set_low_internal_ram ?? s memory.
    744   [1,2,3,4:
    745      normalize
    746      repeat (@ le_S_S)
    747      @ le_O_n
    748   ]
    749 qed.
    750734
    751735definition set_arg_16': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → Σs':PreStatus M code_memory. clock ?? s = clock ?? s' ≝
     
    971955        match head' … bit_1 with
    972956        [ 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
     957          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     958          let trans ≝ true:::four_bits @@ [[false; false; false]] in
    977959          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
    978             get_index_v … sfr m ?
     960            get_index_v … sfr (nat_of_bitvector … three_bits) ?
    979961        | false ⇒
    980           let address ≝ nat_of_bitvector … seven_bits in
    981           let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     962          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     963          let address' ≝ [[true; false; false]]@@four_bits in
    982964          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    983             get_index_v … t (modulus address 8) ?
     965            get_index_v … t (nat_of_bitvector … three_bits) ?
    984966        ]
    985967      | N_BIT_ADDR n ⇒
     
    988970        match head' … bit_1 with
    989971        [ 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
     972          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     973          let trans ≝ true:::four_bits @@ [[false; false; false]] in
    994974          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
    995             ¬(get_index_v … sfr m ?)
     975            ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?)
    996976        | false ⇒
    997           let address ≝ nat_of_bitvector … seven_bits in
    998           let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     977          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     978          let address' ≝ [[true; false; false]]@@four_bits in
    999979          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    1000             ¬(get_index_v … t (modulus address 8) ?)
     980            ¬(get_index_v … t (nat_of_bitvector … three_bits) ?)
    1001981        ]
    1002982      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
     
    1004984        match other in False with [ ]
    1005985      ] (subaddressing_modein … a).
    1006       @modulus_less_than
     986  //
    1007987qed.
    1008988     
     
    1018998        match head' … bit_1 with
    1019999        [ 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
     1000          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1001          let trans ≝ true:::four_bits @@ [[false; false; false]] in
     1002          let sfr ≝ get_bit_addressable_sfr … s trans true in
     1003          let new_sfr ≝ set_index … sfr (nat_of_bitvector … three_bits) v ? in
     1004            set_bit_addressable_sfr … s new_sfr trans
    10271005        | false ⇒
    1028           let address ≝ nat_of_bitvector … seven_bits in
    1029           let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     1006          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1007          let address' ≝ [[true; false; false]]@@four_bits in
    10301008          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
    1031           let n_bit ≝ set_index … t (modulus address 8) v ? in
     1009          let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in
    10321010          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
    10331011            set_low_internal_ram … s memory
     
    10431021            [ ]
    10441022      ] (subaddressing_modein … a).
    1045   @modulus_less_than
     1023  //
    10461024qed.
    10471025
Note: See TracChangeset for help on using the changeset viewer.