 Timestamp:
 Jun 23, 2011, 2:56:20 AM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1036 r1037 1980 1980 pbu)). 1981 1981 1982 lemma Some_Some_elim: 1983 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P. 1984 #T #x #y #P #H #K @H @option_destruct_Some // 1985 qed. 1986 1982 1987 theorem main_thm: 1983 1988 ∀M,M',ps,pol. … … 2030 2035 change in SAFE with (next_internal_pseudo_address_map0 ???? = ?) <EQ1 in SAFE; 2031 2036 >EQ2 whd in ⊢ (??(??%??)? → ?) #SAFE 2032 2033 XX 2034 2035 whd in match execute_1_pseudo_instruction 2036 2037 whd in match expand_pseudo_instruction normalize nodelta; 2038 whd in match execute_1_pseudo_instruction (*!!! USARE 0 !!!*) normalize nodelta; >EQ0 2039 normalize in match (\snd 〈preamble,instr_list〉); 2040 cases (fetch_pseudo_instruction instr_list (program_counter pseudo_assembly_program ps)) in MAP ⊢ % 2041 #pi #newppc normalize nodelta; #MAP 2042 cases pi in MAP; normalize nodelta; 2043 [2,3: (* Comment, Cost *) #ARG #MAP whd in ⊢ (% → ?) #H2 #EQ %[1,3:@0] 2044 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP <MAP MAP M'; 2045 (* 2046 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 i 2047 n H2; whd in ⊢ (% → ?) 2048 #H2*) >(eq_bv_eq … H2) >EQ % 2037 whd in EQps':(???%); <EQ1 in EQps'; >EQ2 normalize nodelta 2038 generalize in match H1; H1; generalize in match instructions instructions 2039 * #instructions >EQ2 change in match (\fst 〈pi,newppc〉) with pi 2040 whd in match ticks_of normalize nodelta <EQ1 >EQ2 2041 cases pi in SAFE 2042 [2,3: (* Comment, Cost *) #ARG whd in ⊢ (??%? → ???% → ?) 2043 @Some_Some_elim #MAP #EQ3 @(Some_Some_elim ????? EQ3) #EQ3' 2044 whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?) 2045 #H2 #EQ %[1,3:@0] 2046 <MAP >(eq_bv_eq … H2) >EQ % 2049 2047 2050 2048 lemma main_thm0: 
src/ASM/Interpret.ma
r985 r1037 651 651 execute_1_0 s instr_pc_ticks. 652 652 653 definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝ 654 λticks_of. 655 λs. 656 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in 657 let ticks ≝ ticks_of (program_counter ? s) in 653 definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝ 654 λticks,s,instr,pc. 658 655 let s ≝ set_program_counter ? s pc in 659 656 let s ≝ … … 690 687 qed. 691 688 689 definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝ 690 λticks_of,s. 691 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in 692 let ticks ≝ ticks_of (program_counter ? s) in 693 execute_1_pseudo_instruction0 ticks s instr pc. 694 692 695 let rec execute (n: nat) (s: Status) on n: Status ≝ 693 696 match n with
Note: See TracChangeset
for help on using the changeset viewer.