Changeset 839


Ignore:
Timestamp:
May 25, 2011, 1:31:15 PM (8 years ago)
Author:
sacerdot
Message:

More experiments.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r838 r839  
    9595(* END RUSSELL **)
    9696
    97 definition write_at_stack_pointer:
     97definition write_at_stack_pointer':
    9898 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
    9999  λM: Type[0].
     
    138138      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    139139      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    140       let s ≝ write_at_stack_pointer ? s pc_bl in
     140      let s ≝ write_at_stack_pointer' ? s pc_bl in
    141141      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    142142      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    143       let s ≝ write_at_stack_pointer ? s pc_bu in
     143      let s ≝ write_at_stack_pointer' ? s pc_bu in
    144144        set_program_counter ? s a
    145145    | Mov dptr ident ⇒
     
    154154 | %
    155155 ]
    156 qed.
    157 
    158 
    159 
    160 
     156 cases not_implemented
     157qed.
     158
     159(*
    161160lemma execute_code_memory_unchanged:
    162161 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
     
    188187  cases not_implemented
    189188qed.
    190 
    191 lemma foo:
     189*)
     190
     191lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
     192 ∀ps,ps': PseudoStatus.
     193  code_memory … ps = code_memory … ps' →
     194   match status_of_pseudo_status ps with
     195    [ None ⇒ status_of_pseudo_status ps' = None …
     196    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
     197    ].
     198 #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     199 generalize in match (refl … (assembly (code_memory … ps)))
     200 cases (assembly ?) in ⊢ (???% → %)
     201  [ #K whd whd in ⊢ (??%?) <H >K %
     202  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
     203qed.
     204 
     205lemma main_thm:
    192206 ∀ticks_of.
    193207 ∀ps: PseudoStatus.
     
    201215 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
    202216 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     217 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
     218 
    203219 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracChangeset for help on using the changeset viewer.