Changeset 839 for src/ASM/AssemblyProof.ma
- Timestamp:
- May 25, 2011, 1:31:15 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r838 r839 95 95 (* END RUSSELL **) 96 96 97 definition write_at_stack_pointer :97 definition write_at_stack_pointer': 98 98 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝ 99 99 λM: Type[0]. … … 138 138 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 139 139 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 140 let s ≝ write_at_stack_pointer ? s pc_bl in140 let s ≝ write_at_stack_pointer' ? s pc_bl in 141 141 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 142 142 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 143 let s ≝ write_at_stack_pointer ? s pc_bu in143 let s ≝ write_at_stack_pointer' ? s pc_bu in 144 144 set_program_counter ? s a 145 145 | Mov dptr ident ⇒ … … 154 154 | % 155 155 ] 156 qed. 157 158 159 160 156 cases not_implemented 157 qed. 158 159 (* 161 160 lemma execute_code_memory_unchanged: 162 161 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps). … … 188 187 cases not_implemented 189 188 qed. 190 191 lemma foo: 189 *) 190 191 lemma 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: % ] ] 203 qed. 204 205 lemma main_thm: 192 206 ∀ticks_of. 193 207 ∀ps: PseudoStatus. … … 201 215 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd 202 216 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) 217 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps)) 218 203 219 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracChangeset
for help on using the changeset viewer.