Changeset 834


Ignore:
Timestamp:
May 25, 2011, 12:10:24 AM (8 years ago)
Author:
sacerdot
Message:

Russell at work.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r833 r834  
    1111  ].
    1212
     13(*
    1314definition assembly_specification:
    1415  ∀sigma: Word → Word. ∀assembly_program: pseudo_assembly_program.
     
    5556  ] *)
    5657qed.
     58*)
    5759
    5860axiom sigma: pseudo_assembly_program → Word → Word.
    5961
     62(*
    6063definition status_of_pseudo_status: PseudoStatus → option Status ≝
    6164 λps.
     
    7881           (p3_latch … ps)
    7982           (clock … ps)) ].
     83*)
    8084
    8185(* RUSSEL **)
     
    8993coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
    9094
     95lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
     96 #A #P #p cases p #w #q @q
     97qed.
     98
    9199(* END RUSSELL **)
     100
     101definition write_at_stack_pointer:
     102 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
     103  λM: Type[0].
     104  λs: PreStatus M.
     105  λv: Byte.
     106    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
     107    let bit_zero ≝ get_index_v… nu O ? in
     108    let bit_1 ≝ get_index_v… nu 1 ? in
     109    let bit_2 ≝ get_index_v… nu 2 ? in
     110    let bit_3 ≝ get_index_v… nu 3 ? in
     111      if bit_zero then
     112        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
     113                              v (low_internal_ram ? s) in
     114          set_low_internal_ram ? s memory
     115      else
     116        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
     117                              v (high_internal_ram ? s) in
     118          set_high_internal_ram ? s memory.
     119  [ cases l0 %
     120  |2,3,4,5: cases not_implemented (* CSC: ???? normalize repeat (@ le_S_S) @ le_O_n *)
     121  ]
     122qed.
    92123
    93124definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
     
    100131  let s ≝ set_clock ? s (clock ? s + ticks) in
    101132  let s ≝ set_program_counter ? s pc in
    102   let s ≝
    103133    match instr with
    104134    [ Instruction instr ⇒
    105        Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
    106     | Comment cmt ⇒ Some PseudoStatus s
    107     | Cost cst ⇒ Some PseudoStatus s
    108     | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
     135       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
     136    | Comment cmt ⇒ s
     137    | Cost cst ⇒ s
     138    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
    109139    | Call call ⇒
    110140      let a ≝ address_of_word_labels s call in
     
    116146      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    117147      let s ≝ write_at_stack_pointer ? s pc_bu in
    118         Some PseudoStatus (set_program_counter ? s a)
     148        set_program_counter ? s a
    119149    | Mov dptr ident ⇒
    120        Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
    121     ]
    122   in
    123     s.
     150       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
     151    ].
    124152 [
    125153 |2,3,4: %
    126  | whd % 
     154 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
     155 |
     156 | (*CSC: ??? *)
     157 | (*CSC: ??? *)
     158 | %
     159 ]
     160qed.
    127161
    128162  λticks_of.
Note: See TracChangeset for help on using the changeset viewer.