- Timestamp:
- Jun 9, 2011, 5:06:26 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r925 r926 1607 1607 status_of_pseudo_status ps = Some … s → 1608 1608 status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps) = Some … s'' → 1609 execute_1s = s''.1609 ∃n. execute n s = s''. 1610 1610 #ticks_of #ps #s #s'' 1611 1611 generalize in match (fetch_assembly_pseudo2 (code_memory … ps)) … … 1626 1626 #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2; 1627 1627 change with 1628 (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?) 1628 (∃n. 1629 execute n (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?) 1629 1630 = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory assembled)) ?) 1630 1631 whd in match (\snd 〈preamble,instr_list〉) in H; … … 1635 1636 (* NICE STATEMENT HERE *) 1636 1637 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps' 1638 #K <K generalize in match K; -K; 1639 (* STATEMENT WITH EQUALITY HERE *) 1637 1640 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ normalize nodelta; 1638 1641 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) 1639 #pi #newppc normalize nodelta; * #instructions * 1642 #pi #newppc normalize nodelta; * #instructions *; 1640 1643 cases pi normalize nodelta; 1641 1644 [ (* Instruction *) 1642 | (* Comment *) #comment #H1 #H2 #EQ normalize in H1 generalize in match (option_destruct_Some ??? H1) #K1 1643 >K1 in H2 whd in ⊢ (% → ?) #H2 whd in ⊢ (??%?) 1645 | (* Comment *) #comment #H1 #H2 #EQ %[@0] >EQ 1646 whd in ⊢ (???(???(??%))) 1647 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 1648 >K1 in H2; whd in ⊢ (% → ?) #H2 <(eq_bv_to_eq … H2) 1649 1644 1650 | (* Cost *) 1645 1651 | (* Jmp *)
Note: See TracChangeset
for help on using the changeset viewer.