Changeset 959 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 15, 2011, 2:22:59 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r951 r959 2209 2209 qed. 2210 2210 2211 lemma program_counter_set_8051_sfr: 2212 ∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s. 2213 // 2214 qed. 2215 2211 2216 lemma eq_rect_Type1_r: 2212 2217 ∀A: Type[1]. … … 2229 2234 // 2230 2235 qed. 2236 2237 axiom pair_elim': 2238 ∀A,B,C: Type[0]. 2239 ∀T: A → B → C. 2240 ∀p. 2241 ∀P: A×B → C → Prop. 2242 (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) → 2243 P p (let 〈lft, rgt〉 ≝ p in T lft rgt). 2244 2245 axiom pair_elim'': 2246 ∀A,B,C,C': Type[0]. 2247 ∀T: A → B → C. 2248 ∀T': A → B → C'. 2249 ∀p. 2250 ∀P: A×B → C → C' → Prop. 2251 (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) → 2252 P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt). 2231 2253 2232 2254 axiom split_elim': … … 2370 2392 #abs @⊥ normalize in abs; destruct (abs) ] 2371 2393 * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?) 2372 generalize in match (refl … (code_memory … ps)) 2373 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta; 2394 generalize in match (refl … (code_memory … ps)) cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta; 2374 2395 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta; 2375 2396 [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ] … … 2509 2530 >clock_write_at_stack_pointer %] 2510 2531 | (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1; 2511 generalize in match 2512 (refl … 2513 (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label)))) 2514 cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1 2515 generalize in match 2516 (refl … 2517 (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps)))) 2518 cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2 2532 @pair_elim' #fst_5_addr #rest_addr #EQ1 2533 @pair_elim' #fst_5_pc #rest_pc #EQ2 2519 2534 generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc)) 2520 2535 cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)] 2521 2536 generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?) 2522 2537 change in ⊢ (? →??%?) with (execute_1_0 ??) 2523 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 2524 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2525 >H2b >(eq_instruction_to_eq … H2a) 2526 generalize in match EQ; -EQ; 2527 whd in ⊢ (???% → ?); 2528 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?) 2538 @pair_elim' * #instr #newppc' #ticks #EQn 2539 * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?) 2540 generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) 2541 @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4 2542 @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5 2543 @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx; 2544 change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc) 2545 @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?) 2546 >get_8051_sfr_set_8051_sfr 2547 2548 whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?) 2529 2549 change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?) 2530 2550 generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
Note: See TracChangeset
for help on using the changeset viewer.