 Timestamp:
 Jun 9, 2011, 3:51:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r921 r923 1592 1592 status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps) = Some … s'' → 1593 1593 execute_1 s = s''. 1594 #ticks_of #ps #s #s'' whd in ⊢ (??%? → ??%? → ?) 1594 #ticks_of #ps #s #s'' 1595 generalize in match (fetch_assembly_pseudo2 (code_memory … ps)) 1596 whd in ⊢ (? → ??%? → ??%? → ?) 1595 1597 >execute_1_pseudo_instruction_preserves_code_memory 1596 cases (assembly (code_memory … ps)) [#abs @⊥ normalize in abs; destruct (abs)] 1597 * #assembled #costs whd in ⊢ (??%? → ??%? → ?) 1598 generalize in match (refl … (assembly (code_memory … ps))) 1599 generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?) 1600 cases (build_maps (code_memory … ps)) 1601 [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H 1602 #abs @⊥ normalize in abs; destruct (abs) ] 1603 * #labels #costs cases (code_memory … ps) #preamble #instr_list normalize nodelta; 1604 generalize in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) *; normalize nodelta; 1605 [ #EQ >EQ #_ #abs @⊥ normalize in abs; destruct (abs) ] 1606 * #final_ppc * #final_pc #assembled #EQ >EQ EQ ASS; normalize nodelta; 1607 #H generalize in match (H ??? (refl …) (refl …)) H; #H; 1598 1608 #H1 generalize in match (option_destruct_Some ??? H1) H1; #H1 <H1 H1; 1599 1609 #H2 generalize in match (option_destruct_Some ??? H2) H2; #H2 <H2 H2; … … 1601 1611 (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?) 1602 1612 = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory assembled)) ?) 1613 whd in match (\snd 〈preamble,instr_list〉) in H; 1614 whd in match (\fst 〈preamble,instr_list〉) in H; 1615 whd in match (\snd 〈final_pc,assembled〉) in H; 1616 s s'' labels costs final_ppc final_pc;
Note: See TracChangeset
for help on using the changeset viewer.